anchor.diff:      (:constructor defwff (operator wffs)))
     operator wffs)
   
  -(defstruct
  -  (cnf
  -    (:constructor defcnf (operator wffs &aux
  -                                   (cnf (cnf-wff (defwff operator wffs))))))
  -  operator wffs cnf)
  -
   (defun cnf-rule (facts-wff implications-wff)
  -  (defwff 'or (list (demorgan (defwff 'not facts-wff))
  -                    (demorgan implications-wff))))
  +  (cnf-wff (defwff 'or (list (demorgan (defwff 'not facts-wff))
  +                             (demorgan implications-wff)))))
   
   (defun cnf-wff (wff)
     (let ((dwff (demorgan wff)))
  
positive.code:      (let ((dwff (demorgan wff)))
         (append (list (wff-operator dwff))
                 (mapcar #'(lambda (x) (evaluate x)) (wff-wffs dwff)))))))
  
  
  (defun demorgan (wff &aux
                       (operator (if (wff-p wff) (wff-operator wff)))
  
negative.code:            (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))))
    ())
  