anchor.diff:                          (if negate
                             (cnf-wff (defwff 'not (list goal)))
                             goal)))
  -  (progn (format t "Resolvent: ~a~%~%" goal-negation)
  +  "Start and recurse the resolution refutation process until nil is found.
  +  Return the list of substitutions carried out at each step."
  +  (progn (format t "Resolvent: ~a~%" goal-negation)
  +         (format t "Substitution: ~a~%~%" (car (last ans)))
     (if (and (wff-p goal-negation) (not (wff-wffs goal-negation)))
       ans
       (loop for wff in (append facts rules)
  
positive.code:            (pairlis ewff-1 ewff-2))))
  
  (defun get-substitutions (ewff-1 ewff-2)
    (let* ((resolved (set-difference ewff-1 ewff-2 :test 'equal))
           (resolved-wff (remove-if-not #'(lambda (x) (equal (car x) 'not)) resolved))
           (resolved-fact (remove-if #'(lambda (x) (equal (car x) 'not)) resolved)))
  
negative.code:       (get-substitutions-helper (car resolved-wff) (list 'not (car resolved-fact))))))
  
  (defun get-substitutions-helper (ewff-1 ewff-2)
    "Helper to get-substitutions."
    (if (= (length ewff-1) (length ewff-2))
      (remove nil
              (mapcar #'(lambda (pair)
  