We introduce a methodology for proving the non-existence of certain orders on groups using a generic automated theorem prover. First, we automatically obtain the inconsistency of certain first-order theories using a generic automated theorem prover. Second, we prove that the consistency or inconsistency of certain first-order theories implies some properties of the corresponding groups. Third, from these group-theoretic properties, we deduce the non-orderability for these groups. This work was done in collaboration with Alexei Lisitsa and Alexei Vernitski.