anchor.diff:         for i from 0 below max
          for sat = (funcall fun i)
          when sat
  -       do (return-from circuit-sat-brute (values t i v)))
  -    (values nil 0 v)))
  +       do (return-from circuit-sat-brute (values i v)))
  +    (values 0 v)))
   
   (defun prop-join (e)
     (labels ((join (op args)
  
positive.code:                (gethash `(not ,x) hash)  (concatenate 'string "-" s)))
      ;; header
      (format stream "~&p cnf ~D ~D~&"
              (length v) (length e))
      (format stream "~&c variables ~{~A~^, ~}~&" v)
      ;; clauses
      (assert (eq (car e) 'and))
      (dolist (x (cdr e))
      (assert (eq (car x) 'or))
        (format stream "~&~{~A ~}0~&" (loop for y in (cdr x)
                                         collect (gethash y hash))))))
  
  
  (defun horn-clase (body &optional head)
    "Or of body implies head"
    (flet ((helper (clause b)
             `(or (not ,b)
  
negative.code:     (fixup (visit e))))
  
  (defun prop->dimacs (e &optional (stream *standard-output*))
    "Convert E to dimacs format and return a list of the variables"
    (let* ((e (prop-join (prop->cnf e)))
           (v (finite-set-list (logic-variables e)))
           (hash (make-hash-table :test #'equal)))
  