如何关闭快速和肮脏的包含替换步骤

Question

当我打断我的证明时，它已经出去吃午饭了，我在回溯中看到quick-and-dirty-subsumption-replacement-step。 如何禁用该启发式？

Answer 1

在接受以下两种形式后，再次尝试您的证明：

(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)