How do I turn off quick-and-dirty-subsumption-replacement-step

Question

When I interrupt my proof, which has gone out to lunch, I see quick-and-dirty-subsumption-replacement-step in the backtrace. How do I disable that heuristic?

Answer 1

Try your proof again after admitting the following two forms:

(defun quick-and-dirty-srs-off (cl1 ac)
  (declare (ignore cl1 ac)
           (xargs :mode :logic :guard t))
  nil)

(defattach quick-and-dirty-srs quick-and-dirty-srs-off)