一阶一阶逻辑，其中所有谓词都只有一个参数，是一阶逻辑的已知可判定片段。测试一个公式在这个逻辑中是否可满足是可判定的，并且存在基于分辨率的方法来判定这一点。
我处于需要测试一些一阶一阶逻辑语句的可满足性的情况。我意识到我将达到复杂性的理论极限，但我希望我能在常见情况下获得合理的性能。
目前，存在大量的定理证明器，它们为解决一阶逻辑问题提供了快速的方法。这些包括Vampire、SPASS、E，以及Z3和CVC4的量词扩展。但是，由于不确定性，它们不能保证停止。
我的问题
在现有的定理证明者中，当给定一元公式作为输入时，是否有任何人可以保证停止？或者有没有办法使用它们（在某种程度上）有效地测试一元公式的可满足性？