我们开发了一种用通用自动定理证明器证明群上满足某些条件的序的不存在性的方法，其基本逻辑如下。第一，我们可以利用通用自动定理证明器自动得到一些一阶公理系统的不自洽性。第二，我们证明某些一阶公理系统的自洽性或者不自恰性可以推得对应的群的一些性质。第三，我们可以从这些群论性质可以得到群的不可排序性。这个工作与 Alexei Lisitsa 和 Alexei Vernitski 合作完成。