Automated reasoning for proving non-orderability of groups

We demonstrate how a generic automated theorem prover can be applied to establish the non-orderability of groups. Our approach incorporates various tools such as positive cones, torsions, generalised torsions and cofinal elements.