The rue theorem-proving system: The complete set of LIM+ challenge problems

In this paper we discuss the successful execution of the LIM+ challenge problems as proposed by Bledsoe. This problem set ranges from a 12-step nonequality proof to a complex 41-step paramodulation proof. Our theorem prover is based on RUE resolution, which incorporates the axioms of equality into the definition of resolution. We apply hyperresolution as a restriction strategy and produce RUE hyper-refutations without the use of paramodulation. We present an extensive treatment of the heuristics applied to find proofs, both standalone and interactive.This work was supported by the National Science Foundation Grant CCR-9024953.