  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.
