Worst Case Exponential Lower Bounds for Input Resolution with Paramodulation
Rick Statman · SIAM Journal on Computing · 1980
Input resolution with paramodulation is a theorem proving procedure complete for sets of unit clauses with equality. This procedure recommends itself because it is easy to implement, and several implementations are in use in more general theorem proving programs. In this note we show that input resolution with paramodulation requires, in the worst case, proofs of exponential length even though the satisfiability problem for sets of unit clauses can be solved in polynomial time.