anchor.diff:             (defwff operator (mapcar #'(lambda (x) (demorgan x)) operand)))
             ('else wff))))
   
  -(defun resolve (facts rules goal &aux
  -                      (goal-negation (cnf-wff (defwff 'not (list goal))))
  -                      (ans-literal (deffact 'ans (goal-vars goal))))
  -  ())
  +(defun flatten (wff &aux
  +                    (dwff (demorgan wff))
  +                    (operator (if (wff-p dwff) (wff-operator dwff)))
  +                    (operand (if (wff-p dwff) (wff-wffs dwff))))
  +  (if (or (fact-p dwff) (every #'fact-p operand))
  +    dwff
  +    (cond ((equal operator 'not)
  +           (defwff 'not (mapcar #'flatten operand)))
  +          ((equal operator 'or)
  +           (defwff 'or (apply #'append
  +                              (mapcar #'(lambda (x)
  +                                          (if (wff-p x)
  +                                            (if (equal (wff-operator x) 'or)
  +                                              (mapcar #'flatten (wff-wffs x))
  +                                              (list (flatten x)))
  +                                            (list x)))
  +                                      operand))))
  +          ((equal operator 'and)
  +           (defwff 'and (apply #'append
  +                               (mapcar #'(lambda (x)
  +                                           (if (wff-p x)
  +                                             (list (flatten x))
  +                                             (list x)))
  +                                       operand)))))))
  +
  +(defun resolve (facts rules goal &optional (negate t) (ans '()) &aux
  +                      (goal-negation
  +                        (if negate
  +                          (cnf-wff (defwff 'not (list goal)))
  +                          goal)))
  +  (if (and (wff-p goal-negation) (not (wff-wffs goal-negation)))
  +    ans
  +    (loop for wff in (append facts rules)
  +          for cnf = (demorgan
  +                      (flatten
  +                        (defwff
  +                          'or
  +                          (cond ((or (fact-p wff) (wff-p wff))
  +                                 (append (list goal-negation) (list wff)))
  +                                ((rule-p wff) (append (list goal-negation)
  +                                                      (list (rule-cnf wff))))))))
  +          for ecnf = (cnf-wff cnf)
  +          when (not (fequal (evaluate cnf) (evaluate ecnf)))
  +          return (resolve facts rules (cnf-wff (flatten ecnf)) nil
  +                          (append ans (get-substitutions
  +                                        (evaluate (flatten cnf))
  +                                        (evaluate (flatten ecnf))))))))
  +
  
positive.code:       ((equal (wff-operator dwff) 'not) dwff))))
  
  (defun fequal (ewff-1 ewff-2)
    (every #'(lambda (pair)
               (if (typep (car pair) 'list)
                 (fequal (car pair) (cdr pair))
                 (or (equal (car pair) (cdr pair))
                     (or (var-p (car pair)) (var-p (cdr pair))))))
           (pairlis ewff-1 ewff-2)))
  
  (defun isnegation (wff-1 wff-2)
    (cond ((and (fact-p wff-1) (wff-p wff-2))
  
negative.code:   operator wffs)
  
  (defun cnf-rule (facts-wff implications-wff)
    (cnf-wff (defwff 'or (list (cnf-wff (defwff 'not (list facts-wff)))
                               (cnf-wff implications-wff)))))
  
  (defun cnf-wff (wff)
    (let ((dwff (flatten (demorgan wff))))
      (cond
        ((fact-p dwff) dwff)
        ((equal (wff-operator dwff) 'or)
  