#| This requires OSCAR_3.31.  This is based on non-linear planner 43.  Lots of little changes. |#

(proclaim '(special *operators* *plan-trace* *initial-state* *goal-state* **premises** *start-time* *inputs*
                  *empty-inference-queue* *msg* *plans* *plan-node-number* *finish*
                  *plan-nodes* *start* *display-time* *causal-links* *causal-link-number* *planner*
                  *planning-problems* *plan-comparison-log* *display-plans* protoplan *plans-decided*
                  *solutions* *defeater-priority*))

(setf *planner* "Non-Linear-Planner-44")

(setf *test-log* nil)

(setf *time-limit* nil)

(setf *display-plans* nil)

(setf *defeater-priority* 1.0)

(defunction show-plans () (setf *display-plans* (not *display-plans*)))

(defstruct (plan-node (:print-function print-plan-node) (:conc-name nil))
    (plan-node-number 0)
    (plan-node-action nil))

(defunction print-plan-node (node stream depth)
    (declare (ignore depth))
    (cond ((eql (plan-node-number node) 0) (princ "*start*" stream))
              ((eql (plan-node-number node) -1) (princ "*finish*" stream))
              (t
                (princ "<pn" stream)
                (princ (plan-node-number node) stream)
                (princ ": " stream)
                (princ (plan-node-action node) stream)
                (princ ">" stream))))

(defparameter *start* (make-plan-node))

(defparameter *finish* (make-plan-node :plan-node-number -1))

(defstruct (plan (:print-function print-plan) (:conc-name nil))
    (plan-number 0)
    (plan-steps nil)
    (plan-goal nil)
    (causal-links nil)
    (before-nodes nil)
    (not-between nil)
    (supporting-inference-nodes nil)
    (live-causal-links nil)
    (live-links? nil)   ;; t if live-causal-links has been computed
    (fixed-links nil)
    )

;; This lexically-orders before-nodes.
(defunction before-< (x y)
    (or (< (plan-node-number (car x)) (plan-node-number (car y)))
          (and (eql (plan-node-number (car x)) (plan-node-number (car y)))
                   (< (plan-node-number (cdr x)) (plan-node-number (cdr y))))))

;; This lexically-orders not-between.
(defunction not-between-< (x y)
    (or (< (plan-node-number (car x)) (plan-node-number (car y)))
          (and (eql (plan-node-number (car x)) (plan-node-number (car y)))
                   (< (plan-node-number (cadr x)) (plan-node-number (cadr y))))
          (and (eql (plan-node-number (car x)) (plan-node-number (car y)))
                   (eql (plan-node-number (cadr x)) (plan-node-number (cadr y)))
                   (< (plan-node-number (cddr x)) (plan-node-number (cddr y))))))

(defunction print-plan (plan stream depth)
    (declare (ignore depth))
    (princ "<plan " stream)
    (princ (plan-number plan) stream)
    (princ ">" stream))

(defunction plan-node (n)
    (find-if #'(lambda (x) (eql (plan-node-number x) n)) *plan-nodes*))

(defstruct (causal-link (:print-function print-causal-link) (:conc-name nil))
    (causal-link-number 0)
    (causal-link-root nil)
    (causal-link-goal nil)
    (causal-link-target nil))

(defunction print-causal-link (link stream depth)
    (declare (ignore depth))
    (princ "<" stream)
    (princ (plan-node-number (causal-link-root link)) stream) (princ " --" stream)
    (prinp (causal-link-goal link) stream) (princ "--> " stream)
    (if (eq (causal-link-target link) *finish*)
      (princ "*finish*" stream)
      (princ (plan-node-number (causal-link-target link)) stream))
    (princ ">" stream))

(defunction build-causal-link (root goal target)
    (let ((link
              (find-if
                #'(lambda (L)
                      (and (eq (causal-link-root L) root)
                               (eq (causal-link-target L) target)
                               (equal (causal-link-goal L) goal)))
                *causal-links*)))
      (when (null link)
           (setf link
                   (make-causal-link
                     :causal-link-number (incf *causal-link-number*)
                     :causal-link-root root
                     :causal-link-goal goal
                     :causal-link-target target))
           (push link *causal-links*))
      link))

(defunction call-set (node plan)
    (subset #'(lambda (L) (equal (causal-link-target L) node)) (causal-links plan)))

(defunction causal-link (n)
    (find-if #'(lambda (x) (eql (causal-link-number x) n)) *causal-links*))

(defunction plan (n)
    (find-if #'(lambda (p) (eql (plan-number p) n)) *plans*))

(defunction subplan (plan1 plan2)
    (and (subsetp (plan-steps plan1) (plan-steps plan2))
             (every #'(lambda (x)
                               (or (eq (cdr x) *finish*)
                                     (mem (car x) (preceding-nodes (cdr x) plan2 (before-nodes plan2)))))
                         (before-nodes plan1))
             (every #'(lambda (x)
                               (or (not (member (car x) (plan-steps plan1)))
                                     (not (member (cdr x) (plan-steps plan1)))
                                     (eq (cdr x) *finish*)
                                     (mem (car x) (preceding-nodes (cdr x) plan1 (before-nodes plan1)))))
                         (before-nodes plan2))
             (every #'(lambda (x)
                               (or (eq (cddr x) *finish*)
                                     (mem x (not-between plan2))))
                         (not-between plan1))
             (every #'(lambda (x)
                               (or (not (member (car x) (plan-steps plan1)))
                                     (not (member (cadr x) (plan-steps plan1)))
                                     (not (member (cddr x) (plan-steps plan1)))
                                     (eq (cddr x) *finish*)
                                     (mem x (not-between plan1))))
                         (not-between plan2))))

(defunction temporally-projectible (P)
    (or (literal P)
          (and (conjunctionp P)
                   (every #'(lambda (Q) (literal Q))
                               (conjuncts P)))))

(defun print-interest (x stream depth)
    (declare (ignore depth))
    (princ "#<" stream) (princ "Interest " stream)
    (princ (interest-number x) stream)
   ; (princ ": " stream) (prinp-sequent (interest-sequent x) stream)
    (princ ">" stream))

;;=============== substitution into plan formulas =============================

(defunction before-order (x y)
    (or (< (inference-number (car x)) (inference-number (car y)))
          (and (eql (inference-number (car x)) (inference-number (car y)))
                   (< (inference-number (cdr x)) (inference-number (cdr y))))))

(defunction not-between-order (x y)
    (or (< (inference-number (car x)) (inference-number (car y)))
          (and (eql (inference-number (car x)) (inference-number (car y)))
                   (< (inference-number (cadr x)) (inference-number (cadr y))))
          (and (eql (inference-number (car x)) (inference-number (car y)))
                   (eq (inference-number (cadr x)) (inference-number (cadr y)))
                   (< (inference-number (cddr x)) (inference-number (cddr y))))))

(defun match-sublis (m x &key (test 'eq))
   (cond ((eq m t) x)
             (t (plan-sublis m x :test test))))

(defunction plan-sublis (m x &key test)
   ; (setf m* m x* x) (break)
    (cond
      ((consp x)
        (cons (plan-sublis m (car x) :test test) (plan-sublis m (cdr x) :test test)))
      ((plan-p x)
        (let* ((plan-steps (plan-sublis m (plan-steps x) :test test))
                  (before-nodes (before-nodes x))
                  (not-between (not-between x))
                  (causal-links (causal-links x)))
          (cond
            ((equal plan-steps (plan-steps x)) x)
            (t
              (let ((node-match (mapcar #'(lambda (x y) (cons x y)) (plan-steps x) plan-steps)))
                (setf before-nodes (sublis node-match before-nodes))
                (setf not-between (sublis node-match not-between))
                (setf causal-links (sublis node-match causal-links))
                (build-plan plan-steps (plan-goal x) causal-links before-nodes not-between))))))
      ((plan-node-p x)
        (let ((action (plan-sublis m (plan-node-action x) :test test)))
          (if (not (equal action (plan-node-action x)))
            (let ((node
                      (make-plan-node
                        :plan-node-number (plan-node-number x)
                        :plan-node-action action)))
              (draw-conclusion `(plan-node ,node) nil :given nil 1.0 1 nil nil)
              node)
            x)))
      (t (let ((assoc (assoc x m :test test)))
            (if assoc (cdr assoc) x)))))

(defunction plan-subst (x y p &key (test 'eq))
    (cond
      ((consp p)
        (cons (plan-subst x y (car p) :test test) (plan-subst x y (cdr p) :test test)))
      ((plan-p p)
        (let* ((plan-steps (plan-subst x y (plan-steps p) :test test))
                  (before-nodes (before-nodes p))
                  (not-between (not-between p))
                  (causal-links (causal-links p)))
          (cond
            ((equal plan-steps (plan-steps p)) p)
            (t
              (let ((node-match (mapcar #'(lambda (x y) (cons x y)) (plan-steps x) plan-steps)))
                (setf before-nodes (sublis node-match before-nodes))
                (setf not-between (sublis node-match not-between))
                (setf causal-links (sublis node-match causal-links))
                (build-plan plan-steps (plan-goal p) causal-links before-nodes not-between))))))
      ((plan-node-p p)
        (let ((action (plan-subst x y (plan-node-action p) :test test)))
          (if (not (equal action (plan-node-action p)))
            (let ((node
                      (make-plan-node
                        :plan-node-number (plan-node-number p)
                        :plan-node-action action)))
              (draw-conclusion `(plan-node ,node) nil :given nil 1.0 1 nil nil)
              node)
            p)))
      (t (if (funcall test y p) x p))))

(defunction variable-correspondence (P Q P-vars Q-vars terms)
    (cond
      ((equal P Q) terms)
      ((member P P-vars)
        (let ((quantifier-variables (mem3 terms)))
          (cond ((rassoc Q quantifier-variables) (throw 'unifier nil))
                    (t (list (cons P (mem1 terms)) (cons Q (mem2 terms)) quantifier-variables)))))
      ((member Q Q-vars)
        (cond ((assoc P (mem3 terms)) (throw 'unifier nil))
                  (t (list (cons P (mem1 terms)) (cons Q (mem2 terms)) (mem3 terms)))))
      ((null P)
        (cond ((null Q) terms)
                    (t (throw 'unifier nil))))
      ((null Q) (throw 'unifier nil))
      ((plan-p P)
        (cond ((plan-p Q) (throw 'unifier nil))
                  ((member Q Q-vars)
                     (cond ((assoc P (mem3 terms)) (throw 'unifier nil))
                                 (t (list (cons P (mem1 terms)) (cons Q (mem2 terms)) (mem3 terms)))))
                    (t (throw 'unifier nil))))
      ((plan-node-p P)
      (cond ((member Q Q-vars)
                 (cond ((assoc P (mem3 terms)) (throw 'unifier nil))
                          (t (list (cons P (mem1 terms)) (cons Q (mem2 terms)) (mem3 terms)))))
               (t (throw 'unifier nil))))
      ((not (listp P))
        (cond ((not (listp Q))
                      (cond ((member Q Q-vars)
                                   (list (cons P (mem1 terms)) (cons Q (mem2 terms)) (mem3 terms)))
                                  ((eql P Q) terms)
                                  ((eql (cdr (assoc P (mem3 terms))) Q) terms)
                                  (t (throw 'unifier nil))))
                    (t (throw 'unifier nil))))
      ((not (listp Q)) (throw 'unifier nil))
      ((or (eq (car P) 'all) (eq (car P) 'some))
        (cond ((eql (car P) (car Q))
                     (variable-correspondence
                       (mem3 P) (mem3 Q) P-vars Q-vars
                       (list (mem1 terms) (mem2 terms)
                               (cons (cons (mem2 P) (mem2 Q)) (mem3 terms)))))
                    (t (throw 'unifier nil))))
      (t
        (variable-correspondence
          (cdr P) (cdr Q) P-vars Q-vars
          (variable-correspondence (car P) (car Q) P-vars Q-vars terms)))))

(defunction sequential-sublis (m X)
    (cond ((eq (length m) 1)
                 (plan-subst (cdr (mem1 m)) (mem1 (mem1 m)) X))
                (t (plan-subst (cdr (mem1 m)) (mem1 (mem1 m)) (sequential-sublis (cdr m) X)))))

;;======================= planning problems =================================

(defmacro make-planning-problem (&rest body)
    (let* ((newbody (make-clauses body))
              (number (cadr (find-if #'(lambda (x) (eq (car x) :number)) newbody)))
              (start-time (cadr (find-if #'(lambda (x) (eq (car x) :start-time)) newbody)))
              (msg (cadr (find-if #'(lambda (x) (eq (car x) :message)) newbody)))
              (reasons
                (mapcar 'eval (cdr (find-if #'(lambda (x) (eq (car x) :reasons)) newbody))))
              (forwards-reasons (subset #'forwards-reason-p reasons))
              (backwards-reasons (subset #'backwards-reason-p reasons))
              (inputs
                (mapcar #'(lambda (x) (list (car x) (reform-if-string (mem2 x)) (mem3 x)))
                               (cdr (find-if #'(lambda (x) (eq (car x) :inputs)) newbody))))
              (premises (cdr (find-if #'(lambda (x) (eq (car x) :premises)) newbody)))
              (goal (reform (cadr (find-if #'(lambda (x) (eq (car x) :goal)) newbody)))))
      (when premises
            (setf premises
                       (mapcar #'(lambda (p) (list (mem1 p) (mem2 p) (mem3 p) (mem4 p))) premises)))
      `(progn
           (setf *problem-number* ',number)
           (setf *msg* ,msg)
           (setf *start-time* (or ,start-time 0))
           (setf *forwards-substantive-reasons* ',forwards-reasons)
           (setf *backwards-substantive-reasons* ',backwards-reasons)
           (setf *inputs* ',inputs)
           (setf **premises** ',premises)
           (setf *goal-state* ',goal)
           (setf *fixed-ultimate-epistemic-interests* (list (plan-interest  ',goal)))
           (dolist (R *forwards-substantive-reasons*) (setf (undercutting-defeaters R) nil))
           (dolist (R *backwards-substantive-reasons*) (setf (undercutting-defeaters R) nil))
           (dolist (d *backwards-substantive-reasons*)
               (dolist (R (reason-defeatees d)) (push d (undercutting-defeaters R))))
           )))

(defunction plan-interest (goal)
    (make-query
      :query-number 1
      :query-formula `(? plan (plan-for plan ,goal))
      :query-strength 0.1
      :positive-query-instructions
      (list #'(lambda (c)
                   (cond ((and (or *display-plans* *display?*) (eql (old-undefeated-degree-of-support c) 0.0))
                               (reinstate-plan (mem2 (node-formula c))))
                             ((and *display-plans* (not *display?*)) (display-plan (mem2 (node-formula c)))))))
      :negative-query-instructions
      (list #'(lambda (c)
                   (when (or *display-plans* *display?*)
                        (let* ((formula (node-formula c))
                                  (plan (mem2 formula)))
                          (retract-plan plan)))))
      ))

(defunction display-planning-settings ()
    (terpri)
    (princ "(") (terpri)
    (princ "======================================================================")
    (terpri) (terpri)
    (princ "                                 ") (princ *version*) (princ "          ")
    (let ((time (multiple-value-list (get-decoded-time))))
       (princ (mem5 time)) (princ "/") (princ (mem4 time)) (princ "/")
       (princ (mem6 time)) (princ "          ") (princ (mem3 time))
       (princ ":") (if (< (mem2 time) 10) (princ "0")) (princ (mem2 time))
       (princ ":") (if (< (mem2 time) 10) (princ "0")) (princ (mem1 time))
       (terpri))
    (princ "                                           ") (princ *planner*) (terpri) (terpri)
    (let ((message 
                (if *problem-number*
                  (if (and *msg* (read-from-string *msg* nil)) 
                    (cat-list (list "Problem number " (write-to-string *problem-number*) ":  " *msg*))
                       (cat-list (list "Problem number " (write-to-string *problem-number*) ":  ")))
                     *msg*)))
      (when message (princ message) (terpri) (terpri)))
    (princ "Forwards-substantive-reasons:") (terpri)
    (dolist (R *forwards-substantive-reasons*)
        (princ "          ") (princ R) (terpri))
    (terpri)
    (princ "Backwards-substantive-reasons:") (terpri)
    (dolist (R *backwards-substantive-reasons*)
        (princ "          ") (princ R) (terpri))
    (terpri)
    (when (not (zerop *start-time*))
         (princ "Start reasoning at cycle ") (princ *start-time*) (terpri) (terpri))
    (princ "Goal-state:") (terpri)
    (dolist (p (conjuncts *goal-state*))
        (princ "          ") (princ (pretty p)) (terpri))
    (terpri)
    (princ "Inputs:") (terpri)
    (dolist (x *inputs*)
        (princ "          ") (prinp (mem2 x)) (princ " : at cycle ") (princ (mem1 x))
        (princ " with justification ") (princ (mem3 x)) (terpri))
    (terpri)
    (when **premises**
         (setf **premises** (mapcar #'(lambda (x) (cons (reform-if-string (car x)) (cdr x))) **premises**))
         (princ "Given:") (terpri)
         (dolist (P **premises**)
             (princ "          ") (prinp (mem1 P)) (princ "  : ")
             (when (mem3 P) (princ " at cycle ") (princ (mem3 P)))
             (princ " with justification = ") (princ (mem2 P)) (terpri))
         (terpri))
   ; (setf *ultimate-epistemic-interests* *fixed-ultimate-epistemic-interests*)
    (setf *query-number* 0)
    (princ "======================================================================")
    (terpri) (terpri))

(setf *reform-list* nil)
(let ((P (gensym)) (Q (gensym)))
;  (pushnew `((,P is a plan for ,Q) (plan-for ,P ,Q) (,P ,Q)) *reform-list* :test 'equal)
  (pushnew `((,P => ,Q) (=> ,P ,Q) (,P ,Q)) *reform-list* :test 'equal)
  )

#|
(defunction complexity (x)
    (cond ((null X) 0)
              ((stringp x) 1)
              ((atom x) 1)
              ((listp x) 
                (cond ((skolem-function (car x))
                            (cond ((null (cdr x)) 1)
                                      ((and (not (listp (cadr x))) (not (eq (cadr x) '=)))
                                        *skolem-multiplier*)
                                      ((and (listp (cadr x)) (skolem-function (caar (cdr x))))
                                        (* *skolem-multiplier* (1+ (complexity (cdr x)))))
                                      (t (apply #'+ (mapcar #'complexity x)))))
                          ((or (u-genp x) (e-genp x)) (* *quantifier-discount* (complexity (q-matrix x))))
                          ((eq (car x) 'plan-for) (+ 2 (complexity (mem3 x))))
                          ((eq (car x) 'protoplan-for) (+ 2 (complexity (mem3 x))))
                          ((eq (car x) 'embellished-plan-for) (+ 2 (complexity (mem3 x))))
                          ((consp (cdr x)) (apply #'+ (mapcar #'complexity x)))
                          (t (+ (complexity (car x)) (complexity (cdr x))))))))
|#

(defunction complexity (x)
    (cond ((null X) 0)
              ((stringp x) 1)
              ; ((plan-p x) (length (plan-steps x)))
              ((plan-p x) (length (plan-steps x)))
              ((atom x) 1)
              ((listp x) 
                (cond ((skolem-function (car x))
                            (cond ((null (cdr x)) 1)
                                      ((and (not (listp (cadr x))) (not (eq (cadr x) '=)))
                                        *skolem-multiplier*)
                                      ((and (listp (cadr x)) (skolem-function (caar (cdr x))))
                                        (* *skolem-multiplier* (1+ (complexity (cdr x)))))
                                      (t (apply #'+ (mapcar #'complexity x)))))
                          ((or (u-genp x) (e-genp x)) (* *quantifier-discount* (complexity (q-matrix x))))
                          ;   ((eq (car x) 'protoplan-for)
                          ;    (+ 1 
                          ;        (if (plan-p (mem2 x)) (length (plan-steps (mem2 x))) 1)
                          ;        (complexity (mem3 x))))
                          ;  ((eq (car x) 'plan-for)
                          ;    (+ 1 
                          ;        (if (plan-p (mem2 x)) (length (plan-steps (mem2 x))) 1)
                          ;        (complexity (mem3 x))))
                          
                          ((eq (car x) '=>) 1)
                          ((eq (car x) 'protoplan-for)
                           ; (-
                              (+ 1 
                                   (if (plan-p (mem2 x)) (length (plan-steps (mem2 x))) 1)
                                   ; (complexity (mem3 x))
                                   (length (mem4 x))))
                             ; (+ (length (mem5 x)) (length (mem6 x)))))
                          ((eq (car x) 'plan-for)
                            (+ 1 
                                 (if (plan-p (mem2 x)) (length (plan-steps (mem2 x))) 1)
                                 ))
                          ; (complexity (mem3 x))))
                          
                          ((eq (car x) 'embellished-plan-for)
                            (+ 2 (length (plan-steps (mem3 x)))))
                          ((eq (car x) 'embellished-protoplan-for)
                            (+ 2 (length (plan-steps (mem3 x)))))
                           ((eq (car x) 'plan-undermines-causal-link) 1)
                           ((eq (car x) 'plan-undermines-causal-links) 2)
                            ; (1+ (complexity (list (mem2 x) (mem3 x) (mem4 x) (mem5 x)))))
                            ; (+ 4 (if (plan-p (mem2 x)) (length (plan-steps (mem2 x))) 1))
                           ((eq (car x) 'plan-node) .1)
                          (t (+ (complexity (car x)) (complexity (cdr x))))))
              ((consp (cdr x)) (apply #'+ (mapcar #'complexity x)))
              (t 1)))

(defunction make-new-conclusion
    (sequent deductive-only reductio-ancestors non-reductio-supposition)
    (let* ((c-vars (formula-node-variables (sequent-formula sequent)))
              (sup (sequent-supposition sequent))
              (i-vars (supposition-variables sup))
              (node
                (make-inference-node
                  :inference-number (incf *inference-number*)
                  :node-sequent sequent
                  :node-formula (sequent-formula sequent)
                  :node-supposition sup
                  :node-kind :inference
                  :deductive-only deductive-only
                  :node-variables c-vars
                  :node-supposition-variables i-vars
                  :non-reductio-supposition non-reductio-supposition
                  :reductio-ancestors reductio-ancestors
                  )))
      (when (and (listp (sequent-formula sequent))
                       (or (equal (car (sequent-formula sequent)) 'plan-for)
                             (equal (car (sequent-formula sequent)) 'protoplan-for)
                             (equal (car (sequent-formula sequent)) 'embellished-protoplan-for)
                             (equal (car (sequent-formula sequent)) 'embellished-plan-for)))
         (push node (supporting-inference-nodes (mem2 (sequent-formula sequent))))
         (when *display?*
             (display-plan (mem2 (sequent-formula sequent)))))
       node))

(defunction display-query (Q)
    (princ "  Interest in ") (prinp (query-formula Q)) (terpri)
    (cond ((null (answered? Q))
                 (princ "  is unsatisfied.")
                 (when (null (query-answers Q)) (princ "  NO ARGUMENT WAS FOUND."))
                 (terpri))
              ((or (whether-query-p Q) (?-query-p Q))
            (dolist (C (query-answers Q))
           ; (let ((C (car (query-answers Q))))
                      (when (>= (compute-undefeated-degree-of-support C) (query-strength Q))
                           (princ "  is answered by node ")
                           (princ (inference-number C)) (princ ":  ")
                           (princ (pretty (node-formula C))) (terpri)
                           (when (plan-p (mem2 (node-formula C)))
                         (show-plan (mem2 (node-formula C)) nil))
                           (let ((skolem-functions (skolem-functions (node-formula C))))
                              (when skolem-functions
                                   (let* ((sf (mem1 skolem-functions))
                                             (support-link
                                               (find-if #'(lambda (SL)
                                                                 (and (eq (support-link-rule SL) EI)
                                                                           (occur sf (node-formula (support-link-target SL)))
                                                                           (not (occur sf (node-formula (mem1 (support-link-basis SL)))))))
                                                            (ancestral-links C))))
                                      (when support-link
                                           (let* ((node (mem1 (support-link-basis support-link)))
                                                     (formula (node-formula node))
                                                     (var (q-variable formula)))
                                              (princ "  where ") (princ sf) (princ " is any ") (princ var)
                                              (princ " such that ") (princ (q-matrix formula)) (princ ",") (terpri)
                                              (princ "  and the existence of such")
                                              (if (equal var "x") (princ " an ") (princ " a ")) (princ var)
                                              (princ " is guaranteed by node ") (princ (inference-number node)) (terpri))))))
                           )))
                (t (dolist (C (query-answers Q))
                       (when (>= (compute-undefeated-degree-of-support C) (query-strength Q))
                            (princ "  is answered affirmatively by node ")
                            (princ (inference-number C)) (terpri)))))
    (princ "---------------------------------------------------") (terpri))

(defunction display-node
    (n proof-nodes nodes-used interests-used interests-discharged nodes-displayed)
   ; (setf nn n pn proof-nodes nu nodes-used iu interests-used id interests-discharged nd nodes-displayed) ; (break)
    ;; (step (display-node nn pn nu iu id nd))
    (when (eq (node-kind n) :percept)
         (princ "|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||")
         (terpri) (princ "It appears to me that ") (prinp (node-formula n)) (terpri)
         (princ "|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||")
         (terpri))
    (princ "  # ") (princ (inference-number n))
    (when (member n *not-strictly-relevant-nodes*) (princ "   NOT STRICTLY RELEVANT"))
    (terpri)
    (princ "  ") (when (eq (node-kind n) :percept) (princ "It appears to me that "))
    (prin-pretty (node-formula n))
    (when (node-supposition n)
         (princ "    supposition: ") (set-prinp (node-supposition n)))
    (if (zerop (undefeated-degree-of-support n)) (princ "                  DEFEATED"))
    (when (and (member n nodes-used)
                          (not (member n proof-nodes)))
         (princ "   --  NOT USED IN PROOF"))
    (terpri)
    (cond ((keywordp (node-justification n)) (princ "  ") (princ (node-justification n)) (terpri))
                ((support-links n)
                  (princ "  Inferred by:") (terpri)
                  (dolist (L* (support-links n))
                      (when (subsetp (support-link-basis L*) nodes-displayed)
                           (princ "                support-link #") (princ (support-link-number L*))
                           (princ " from ") (princ-set (mapcar #'inference-number (support-link-basis L*)))
                           (princ " by ") (princ (support-link-rule L*))
                           (when (support-link-clues L*)
                         (princ " with clues ")
                         (princ-set (mapcar #'inference-number (support-link-clues L*))))
                           (when (support-link-defeaters L*)
                                (princ "  defeaters: ")
                                (princ-set (mapcar #'inference-number (support-link-defeaters L*))))
                           (when (defeating-assignment-trees L*) (princ "   DEFEATED"))
                           (terpri)))))
    (when (node-defeatees n)
         (princ "  defeatees: ")
         (princ "{ ")
         (let ((L (car (node-defeatees n))))
            (princ "link ")
            (princ (support-link-number L)) (princ " for node ")
            (princ (inference-number (support-link-target L))))
         (dolist (L (cdr (node-defeatees n)))
             (princ " , ")
            (princ "link ")
             (princ (support-link-number L)) (princ " for node ")
             (princ (inference-number (support-link-target L))))
         (princ " }") (terpri))
    ; (princ " by ") (princ (node-justification n))
    (let ((generating-interests (intersection (generating-interests n) interests-used)))
       (cond ((> (length generating-interests) 1)
                    (princ " generated by interests ")
                    (print-list (mapcar #'interest-number generating-interests) 40))
                   ((eq (length generating-interests) 1)
                     (princ "  generated by interest ")
                     (princ (interest-number (mem1 generating-interests)))))
       (when generating-interests (terpri)))
    (let ((DI (enabling-interests n)))
       (cond
         ((> (length DI) 1)
           (princ "  This node is inferred by discharging links to interests ")
           (princ (mapcar #'interest-number DI)) (terpri))
         (DI
           (princ "  This node is inferred by discharging a link to interest #")
           (princ (interest-number (car DI)))
           (let ((SL (find-if #'(lambda (SL) (equal (support-link-rule SL) :reductio)) (support-links n))))
              (when SL
                   (let* ((node* (mem1 (support-link-basis SL)))
                             (rs (find-if
                                    #'(lambda (sup)
                                          (and
                                            (member (car DI) (generating-interests sup))
                                            ;; 
                                            (mem sup (a-range (reductio-ancestors node*)))
                                            (not (mem sup (a-range (reductio-ancestors n))))))
                                    (a-range (reductio-ancestors node*)))))
                                    ;; (generated-suppositions (car DI)))))
                      (when rs
                           (princ " as a result of inferring node #") (princ (inference-number node*))
                           (princ " from") (terpri) (princ "  reductio-supposition #")
                           (princ (inference-number rs)) (princ ", which was generated by interest #")
                           (princ (interest-number (car DI)))))))
           (terpri)))
       (let ((interests
                 (subset
                   #'(lambda (in)
                         (and
                           (member n (discharging-nodes in))
                           (or
                             (some
                               #'(lambda (dr)
                                     (some
                                       #'(lambda (pn)
                                             (some
                                               #'(lambda (SL)
                                                     (and (equal (support-link-rule SL) :reductio)
                                                               (member n (support-link-basis SL))
                                                               (member (car dr) (support-link-basis SL))))
                                               (support-links pn)))
                                       proof-nodes))
                               (direct-reductio-interest in))
                             (some #'(lambda (L)
                                              (and
                                                (discharged-link L)
                                                (or
                                                  (equal (link-rule L) :answer)
                                                  (some
                                                    #'(lambda (pn)
                                                          (and
                                                            (member (resultant-interest L) (enabling-interests pn))
                                                            (some
                                                              #'(lambda (SL)
                                                                    (member n (support-link-basis SL)))
                                                              (support-links pn))))
                                                    proof-nodes))))
                                          (right-links in)))))
                   (set-difference interests-used DI))))
          (cond ((> (length interests) 1)
                       (princ "  This discharges interests ") (print-list (mapcar #'interest-number interests) 40))
                      ((eq (length interests) 1)
                        (princ "  This discharges interest ") (princ (interest-number (mem1 interests))))
                      (t
                        (setf interests
                                 (subset
                                   #'(lambda (in)
                                         (and
                                           (member n (discharging-nodes in))
                                           (not
                                             (some
                                               #'(lambda (dn)
                                                     (strongly-discharging-node dn in proof-nodes interests-discharged))
                                               (discharging-nodes in)))))
                                   (set-difference interests-used DI)))
                        (cond
                          ((> (length interests) 1)
                            (princ "  This discharges interests ") (print-list (mapcar #'interest-number interests) 40)
                            (princ " but no inference made by discharging these interests is used in the solution."))
                          ((eq (length interests) 1)
                            (princ "  This discharges interest ") (princ (interest-number (mem1 interests)))
                            (princ " but no inference made by discharging this interest is used in the solution.")))))
          (when interests (terpri))))
    (when (and (listp (node-formula n))
                     (or (eq (car (node-formula n)) 'plan-for)
                           (eq (car (node-formula n)) 'protoplan-for)
                           (eq (car (node-formula n)) 'embellished-protoplan-for)))
       (display-plan (mem2 (node-formula n))))
   (when *graphics-pause* (pause-graphics))  ;; wait for a character to be typed in the Listener
    (when (and *graph-log* (member n proof-nodes))
         (push n *nodes-displayed*)
         (draw-n n *og* nodes-displayed)))

(defunction display-used-interest
    (interest proof-nodes used-nodes used-interests enabling-interests interests-used-in-proof)
    ; (when (eq interest (interest 6)) (setf i interest pn proof-nodes un used-nodes ui used-interests ein enabling-interests iun interests-used-in-proof) (break))
    ;; (step (display-used-interest i pn un ui ein iun))
    (princ "                                        # ") (princ (interest-number interest))
    (when (not (member interest interests-used-in-proof))
         (princ "               NOT USED IN PROOF"))
    (terpri)
    (princ "                                        ")
    (when (deductive-interest interest) (princ "deductive "))
    (when (reductio-interest interest) (princ "reductio "))
    (princ "interest: ") (prin-pretty (interest-formula interest))
    (when (interest-supposition interest)
         (princ "    supposition: ")
         (set-prinp (interest-supposition interest)))
    (terpri)
    (when
         (some #'(lambda (L) (query-p (resultant-interest L)))
                     (right-links interest))
         (princ "                                        This is of ultimate interest") (terpri))
    (dolist (L (right-links interest))
        (when (and (not (query-p (resultant-interest L))) (discharged-link L)
                            (member (resultant-interest L) used-interests))
             (princ "                                        For ")
             (when (reductio-interest (resultant-interest L)) (princ "reductio "))
             (princ "interest ")
             (princ (interest-number (resultant-interest L)))
             (princ " by ") (princ (link-rule L))
             (let ((nodes (supporting-nodes L)))
               (when nodes
                    (cond ((equal (length nodes) 1)
                                (princ " using node ")
                                (princ (inference-number (mem1 nodes))))
                              (t
                                (princ " using nodes ")
                                (print-list (mapcar
                                                  #'(lambda (conclusion)
                                                        (inference-number conclusion))
                                                  nodes) 40)))))
             (let ((nodes (link-clues L)))
               (when nodes
                    (cond ((equal (length nodes) 1)
                                (princ " with clue ")
                                (princ (inference-number (mem1 nodes))))
                              (t
                                (princ " with clues ")
                                (print-list (mapcar
                                                  #'(lambda (conclusion)
                                                        (inference-number conclusion))
                                                  nodes) 40)))))
             (terpri)))
    (let ((direct-reductio-interest
              (subset #'(lambda (n) (assoc n (direct-reductio-interest interest)))
                            used-nodes)))
      (cond ((> (length direct-reductio-interest) 1)
                  (princ "                                        Reductio interest generated by nodes ")
                  (print-list (mapcar #'(lambda (n) (inference-number n))
                                                 direct-reductio-interest) 40) (terpri))
                ((= (length direct-reductio-interest) 1)
                  (princ "                                        Reductio interest generated by node ")
                  (princ (inference-number (mem1 direct-reductio-interest))) (terpri))))
    (let ((discharging-nodes
              (subset
                #'(lambda (dn)
                      (strongly-discharging-node dn interest proof-nodes enabling-interests))
                (intersection (discharging-nodes interest) used-nodes)))
            (defeatees
                (subset #'(lambda (L)
                                   (member (support-link-target L) proof-nodes))
                              (interest-defeatees interest))))
      (when defeatees
           (princ "                                        Of interest as a defeater for ")
           (cond ((cdr defeatees)
                       (princ "support-links: ")
                       (princ "{ ")
                       (let ((L (car defeatees)))
                         (princ "link ")
                         (princ (support-link-number L)) (princ " for node ")
                         (princ (inference-number (support-link-target L))))
                       (dolist (L (cdr defeatees))
                           (princ " , ")
                           (princ "link ")
                           (princ (support-link-number L)) (princ " for node ")
                           (princ (inference-number (support-link-target L))))
                       (princ " }"))
                     (t
                       (princ "support-link ")
                       (let ((L (car defeatees)))
                         (princ (support-link-number L)) (princ " for node ")
                         (princ (inference-number (support-link-target L))))))
           (terpri))
      (cond
        (discharging-nodes
          (princ "                                        This interest is discharged by")
          (cond ((> (length discharging-nodes) 1) (princ " nodes ")
                      (princ (mapcar #'inference-number discharging-nodes)))
                    (t (princ " node ") (princ (inference-number (mem1 discharging-nodes)))))
          (terpri))
        ((not (some #'(lambda (L) (and (query-p (resultant-interest L)) (discharged-link L)))
                             (right-links interest)))
          (setf discharging-nodes
                   (intersection (discharging-nodes interest) used-nodes))
          (cond
            (discharging-nodes
              (princ "                                        This interest is discharged by")
              (cond ((> (length discharging-nodes) 1) (princ " nodes ")
                          (princ (mapcar #'inference-number discharging-nodes)))
                        (t (princ " node ") (princ (inference-number (mem1 discharging-nodes)))))
              (terpri)
              (when
                   (and (null defeatees) (member interest interests-used-in-proof))
                   (princ "                                        but no inference made by discharging this interest is used in the solution.")
                   (terpri)))
            ((and (null defeatees) (member interest interests-used-in-proof))
              (princ "                                        No inference made by discharging this interest is used in the solution.") (terpri)))
          )))
    (when (and *graph-interests* *graph-log*)
         (when *graphics-pause* (pause-graphics))  ;; wait for a character to be typed in the Listener
         (draw-i interest *og*)))

(defunction display-belief-changes  (links new-beliefs new-retractions)
   ; (setf l links nb new-beliefs nr new-retractions)
    ; (when (member (support-link 12) links) (setf l links nb new-beliefs nr new-retractions) (break))
    ;; (step (display-belief-changes l  nb nr))
    (when *monitor-assignment-tree* (monitor-assignment-tree links))
   ; (when (and (not (complete-tree *assignment-tree*)) (null *deductive-only*))
   ;      (princ links) (terpri) (break))
    (when (or *display?* *log-on*)
         (cond
           ((and (not *deductive-only*) (or new-beliefs new-retractions))
             (when (and *display?*
                                 (some #'(lambda (n) (not (some #'(lambda (L) (eq n (support-link-target L))) links)))
                                             (append new-beliefs new-retractions)))
                  (princ "---------------------------------------------------------------------------") (terpri)
                  (princ "Affected-nodes:") (terpri)
                  (princ *affected-nodes*) (terpri)
                  (princ "---------------------------------------------------------------------------") (terpri)
                  (when *discards*
                       (princ "discarding:  ") (dolist (d *discards*) (princ d) (princ "  ")) (terpri))
                  (when *creations*
                       (princ "creating:  ") (dolist (d *creations*) (princ d) (princ "  ")) (terpri))
                  (when (or *discards* *creations*)
                       (princ "---------------------------------------------------------------------------")
                       (terpri))
                  (princ "Recomputed assignment-tree:") (terpri)
                  (display-assignment-tree))
             (when (and *display?* *graphics-on*)
                  (when *graphics-pause* (pause-graphics))
                  (dolist (link links) (draw-n (support-link-target link) *og* *nodes-displayed*))
                      (when
                           (set-difference (append new-beliefs new-retractions) (mapcar #'support-link-target links))
                           (flash-nodes *affected-nodes* *og* *yellow-color* 5)))
             (when
                  new-retractions
                  (when *log-on*
                       (push "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv" *reasoning-log*))
                  (when *display?* (princ "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv") (terpri)))
             (dolist (N new-retractions)
                 (cond ((or (not (some #'(lambda (L) (eq N (support-link-target L))) links))
                                  (> (length (support-links N)) 1))
                              (cond
                                ((zerop (undefeated-degree-of-support N))
                                  (when *log-on*
                                       (push (list :defeated N) *reasoning-log*))
                                  (when *display?*
                                       (princ "               ") (princ N) (princ " has become defeated.") (terpri)
                                       (princ "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv") (terpri))
                                  (when (and *display?* *graphics-on*)
                                       (let ((posi (node-position N *og*)))
                                          (when posi
                                               (when (and (boundp '*speak*) *speak*)
                                                    (speak-text "Node ")
                                                    (speak-text (write-to-string (inference-number N)))
                                                    (speak-text "has become defeated."))
                                               (draw-just-defeated-node posi *og* N)))))
                                (t
                                  (when *log-on*
                                       (push (list :decreased-support N (undefeated-degree-of-support N))
                                                   *reasoning-log*))
                                  (when *display?*
                                       (princ "               The undefeated-degree-of-support of ") (princ N)
                                       (princ " has decreased to ") (princ (undefeated-degree-of-support N)) (terpri)
                                       (princ "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv") (terpri)))))
                             ((zerop (undefeated-degree-of-support N))
                               (when *log-on*
                                    (push (list :defeated N) *reasoning-log*))
                               (when *display?*
                                    (princ "               ") (princ N) (princ " is defeated.") (terpri)
                                    (princ "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv") (terpri))
                               (when (and *display?* *graphics-on*)
                                    (when (and (boundp '*speak*) *speak*)
                                         (speak-text "Node ")
                                         (speak-text (write-to-string (inference-number N)))
                                         (speak-text "is defeated."))
                                    (let ((posi (node-position n *og*)))
                                       (cond (posi (draw-just-defeated-node posi *og* n))
                                                     (t
                                                       (draw-n n *og* *nodes-displayed*)
                                                       (push n *nodes-displayed*)
                                                       (setf posi (node-position n *og*))
                                                       (draw-just-defeated-node posi *og* n)))))))
                 ))
           ((and *display?* *graphics-on*)
             (when *graphics-pause* (pause-graphics))
             (dolist (link links) (draw-n (support-link-target link) *og* *nodes-displayed*)))))
    (when (and *display?* *graphics-on*)
         (setf *nodes-displayed* (union (mapcar #'support-link-target links) *nodes-displayed*))))

(defunction display-peripherals (x boundary nodes-used)
    (cond
      ((equal x "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv") (setf boundary t))
      ((listp x)
        (cond ((and (equal (mem1 x) :increased-support) (member (mem2 x) nodes-used))
                     (when (equal boundary t)
                          (princ "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv") (terpri)
                          (setf boundary nil))
                     (princ "               The undefeated-degree-of-support of ") (princ (mem2 x))
                     (princ " has increased to ") (princ (mem3 x))
                     (terpri) (princ "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv") (terpri)
                     (when *graph-log*
                          (let ((posi (node-position (mem2 x) *og*)))
                            (when posi
                                 (when (and (boundp '*speak*) *speak*)
                                      (speak-text "The undefeeted-degree-of-support of node ")
                                      (speak-text (write-to-string (inference-number (mem2 x))))
                                      (speak-text "has increased to")
                                      (speak-text (write-to-string (mem3 x))))
                                 (draw-just-undefeated-node posi *og* (mem2 x))))))
                  ((and (equal (mem1 x) :new-support) (member (mem2 x) nodes-used)
                            (not (eql (mem3 x) 1.0)))
                     (when (equal boundary t)
                          (princ "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv") (terpri)
                          (setf boundary nil))
                     (princ "               The undefeated-degree-of-support of ") (princ (mem2 x))
                     (princ " is ") (princ (mem3 x))
                     (terpri) (princ "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv") (terpri)
                     (when *graph-log*
                          (let ((posi (node-position (mem2 x) *og*)))
                            (when posi
                                 (when (and (boundp '*speak*) *speak*)
                                      (speak-text "The undefeeted-degree-of-support of node ")
                                      (speak-text (write-to-string (inference-number (mem2 x))))
                                      (speak-text "is")
                                      (speak-text (write-to-string (mem3 x))))
                                 (draw-just-undefeated-node posi *og* (mem2 x))))))
                  ((and (equal (mem1 x) :defeated) (member (mem2 x) nodes-used))
                    (when (equal boundary t)
                         (princ "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv") (terpri)
                         (setf boundary nil))
                    (princ "               ") (princ (mem2 x)) (princ " has become defeated.") (terpri)
                    (princ "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv") (terpri)
                    (when *graph-log*
                         (let ((posi (node-position (mem2 x) *og*)))
                           (when posi
                                (when (and (boundp '*speak*) *speak*)
                                     (speak-text "Node ")
                                     (speak-text (write-to-string (inference-number (mem2 x))))
                                     (speak-text "has become defeated."))
                                (draw-just-defeated-node posi *og* (mem2 x))))))
                    ((and (equal (mem1 x) :decreased-support) (member (mem2 x) nodes-used))
                      (when (equal boundary t)
                           (princ "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv") (terpri)
                           (setf boundary nil))
                      (princ "               The undefeated-degree-of-support of ") (princ (mem2 x))
                      (princ " has decreased to ") (princ (mem3 x))
                      (terpri) (princ "               vvvvvvvvvvvvvvvvvvvvvvvvvvvvvv") (terpri))
                    ((and (equal (mem1 x) :answer-query) (member (mem2 x) nodes-used))
                      (princ "               ")
                      (princ "=========================================") (terpri)
                      (princ "               ") (princ "Justified belief in ")
                      (prinp (node-formula (mem2 x))) (terpri)
                     (princ "               with undefeated-degree-of-support ") (princ (mem4 x)) (terpri)
                      (princ "               ") (princ "answers ") (princ (mem3 x))
                      (terpri) (princ "               ")
                      (princ "=========================================") (terpri)
                      (when (equal (mem1 (node-formula (mem2 x))) 'protoplan-for)
                           (adopt-plan (mem2 (node-formula (mem2 x)))))
                      (when (equal (mem1 (node-formula (mem2 x))) 'plan-for)
                           (adopt-plan (mem2 (node-formula (mem2 x)))))
                      (when (and (boundp '*speak*) *speak*)
                           (speak-text "Node ")
                           (speak-text (write-to-string (inference-number (mem2 x))))
                           (speak-text "answers query ")
                           (speak-text (write-to-string (query-number (mem3 x))))))
                    ((and (equal (mem1 x) :retract-answer) (member (mem2 x) nodes-used))
                      (princ "               ")
                      (princ "=========================================") (terpri)
                      (princ "               ") (princ "Lowering the undefeated-degree-of-support of ")
                      (prinp (node-formula (mem2 x))) (terpri)
                      (princ "               ") (princ "retracts the previous answer to ")
                      (princ (mem3 x)) (terpri) (princ "               ")
                      (princ "=========================================") (terpri)
                      (when (equal (mem1 (node-formula (mem2 x))) 'plan-for)
                           (retract-plan (mem2 (node-formula (mem2 x)))))
                      (when (equal (mem1 (node-formula (mem2 x))) 'protoplan-for)
                           (retract-plan (mem2 (node-formula (mem2 x)))))
                      (when (and (boundp '*speak*) *speak*)
                           (speak-text "Node ")
                           (speak-text (write-to-string (inference-number (mem2 x))))
                           (speak-text "no longer answers query ")
                           (speak-text (write-to-string (query-number (mem3 x)))))))))
    boundary)

(defunction display-interest (interest)
    (if (numberp interest) (setf interest (interest interest)))
    (princ "                                        # ") (princ (interest-number interest)) (princ "  ")
    (when (deductive-interest interest) (princ "deductive "))
    (when (reductio-interest interest) (princ "reductio "))
    (princ "interest:")
    (terpri)
    (princ "                                           ") (prin-pretty  (interest-formula interest))
    (when (interest-supposition interest)
         (princ "    supposition: ")
         (set-prinp (interest-supposition interest)))
    (terpri)
    (when
         (some #'(lambda (L) (query-p (resultant-interest L)))
                     (right-links interest))
         (princ "                                        This is of ultimate interest") (terpri))
    (let ((L (lastmember (right-links interest))))
      (when (and L (not (query-p (resultant-interest L))))
           (princ "                                        For ")
           (when (reductio-interest (resultant-interest L)) (princ "reductio "))
           (princ "interest ")
           (princ (interest-number (resultant-interest L)))
           (princ " by ") (princ (link-rule L))
           (let ((nodes (supporting-nodes L)))
             (when nodes
                  (cond ((equal (length nodes) 1)
                              (princ " using node ")
                              (princ (inference-number (mem1 nodes))))
                            (t
                              (princ " using nodes ")
                              (print-list (mapcar
                                                #'(lambda (conclusion)
                                                      (inference-number conclusion))
                                                nodes) 40)))))
           (when (or (eq (link-rule L) goal-regression)
                             (eq (link-rule L) embedded-goal-regression)
                             (eq (link-rule L) reuse-node))
                (let ((action (e-assoc 'action (link-binding L))))
                  (when (not (interest-variable action))
                       (princ " and action ") (princ (e-assoc 'action (link-binding L))))))
           (let ((nodes (link-clues L)))
             (when nodes
                  (cond ((equal (length nodes) 1)
                              (princ " with clue ")
                              (princ (inference-number (mem1 nodes))))
                            (t
                              (princ " with clues ")
                              (print-list (mapcar
                                                #'(lambda (conclusion)
                                                      (inference-number conclusion))
                                                nodes) 40)))))
           (terpri))
      (when (discharge-condition interest)
           (princ "                                        Discharge condition: ") (terpri)
           (princ "                                             ")
           (display-discharge-condition interest L) (terpri)))
    (terpri))

(defunction display-support-link (L)
   (if (numberp L) (setf L (support-link L)))
    (let ((n (support-link-target L)))
     (princ "  # ") (princ (inference-number n)) (princ "   ")
     (when (not (equal (node-kind n) :inference)) (princ (node-kind n)) (princ "         "))
     (prin-pretty (node-formula n))
     (when (node-supposition n)
         (princ "    supposition: ") (set-prinp (node-supposition n)))
     (terpri) 
     (princ "  Inferred by support-link #") (princ (support-link-number L))
     (princ " from ") (princ-set (mapcar #'inference-number (support-link-basis L)))
     (princ " by ") (princ (support-link-rule L))
     (when (support-link-clues L)
         (princ " with clues ")
         (princ-set (mapcar #'inference-number (support-link-clues L))))
     (when (support-link-defeaters L)
         (princ "  defeaters: ") (princ-set (mapcar #'inference-number (support-link-defeaters L))))
     (terpri)
     (when (and (reason-p (support-link-rule L)) (reason-description (support-link-rule L)))
         (princ "  ") (princ (reason-description (support-link-rule L))) (terpri))
     (let ((links (remove L (support-links n))))
       (when links
           (princ "  Previously inferred by:") (terpri)
           (dolist (L* links)
              (princ "                support-link #") (princ (support-link-number L*))
              (princ " from ") (princ-set (mapcar #'inference-number (support-link-basis L*)))
              (princ " by ") (princ (support-link-rule L*))
              (when (support-link-clues L*)
                  (princ " with clues ")
                  (princ-set (mapcar #'inference-number (support-link-clues L*))))
              (when (support-link-defeaters L*)
                  (princ "  defeaters: ")
                        (princ-set (mapcar #'inference-number (support-link-defeaters L*))))
              (terpri))))
    ; (princ "  nearest-defeasible-ancestors: ")
    ; (princ (nearest-defeasible-ancestors n)) (terpri)
      (when (node-defeatees n)
           (princ "  defeatees: ")
           (princ "{ ")
           (let ((L (car (node-defeatees n))))
              (princ "link ")
              (princ (support-link-number L)) (princ " for node ")
              (princ (inference-number (support-link-target L))))
           (dolist (L (cdr (node-defeatees n)))
               (princ " , ")
               (princ "link ")
                (princ (support-link-number L)) (princ " for node ")
                (princ (inference-number (support-link-target L))))
           (princ " }") (terpri)))
    (terpri))

(defunction prin-pretty (P &optional stream)
    (cond
      ((listp P)
        (cond ((member (car P) '(plan-for protoplan-for embellished-plan-for embellished-protoplan-for
                                             plan-undermines-causal-links plan-undermines-causal-link))
                    (print-pretty P))
                  ((negationp P) (princ '~ stream) (prin-pretty (negand P) stream))
                  ((eq (car P) '@) (print-pretty (list (mem2 P) '@ (mem3 P))))
                  (t (princ (pretty P) stream))))
      (t (princ (pretty P) stream))))

;;============================ relativized quantifiers=================================

(defunction resolve-variable-conflicts (p &optional variables (reset-counter? t))
    (when reset-counter? (setf *gensym-counter* 1))
    (cond ((or (u-genp p) (e-genp p))
                (let ((var (q-variable p)))
                  (cond ((eq (mem3 p) :type)
                              (cond ((mem var variables)
                                          (let ((var* (gensym (string var))))
                                            (list (mem1 p) var* (mem3 p) (mem4 p)
                                                   (=subst var* var
                                                                 (resolve-variable-conflicts (mem5 p) variables nil)))))
                                        (t 
                                          (list (mem1 p) var (mem3 p) (mem4 p)
                                                 (resolve-variable-conflicts (mem5 p) (cons var variables) nil)))))
                            (t
                              (cond ((mem var variables)
                                          (let ((var* (gensym (string var))))
                                            (list (mem1 p) var*
                                                   (=subst var* var
                                                                 (resolve-variable-conflicts (mem3 p) variables nil)))))
                                        (t 
                                          (list (mem1 p) var
                                                 (resolve-variable-conflicts (mem3 p) (cons var variables) nil))))))))
                ((negationp p) (tilde (resolve-variable-conflicts (negand p) variables nil)))
                ((conjunctionp p)
                  (conj (resolve-variable-conflicts (conjunct1 p) variables nil)
                            (resolve-variable-conflicts (conjunct2 p) variables nil)))
                ((disjunctionp p)
                  (disj (resolve-variable-conflicts (disjunct1 p) variables nil)
                            (resolve-variable-conflicts (disjunct2 p) variables nil)))
                ((conditionalp p)
                  (condit (resolve-variable-conflicts (antecedent p) variables nil)
                            (resolve-variable-conflicts (consequent p) variables nil)))
                ((biconditionalp p)
                  (bicondit (resolve-variable-conflicts (bicond1 p) variables nil)
                            (resolve-variable-conflicts (bicond2 p) variables nil)))
                (t p)))

(defunction convert-to-prefix-form (P)
    (let ((P* nil))
      (cond ((listp P)
                  (cond 
                    ((equal (mem1 P) "~")
                      (list '~ (convert-to-prefix-form (mem2 P))))
                    ((equal (mem1 P) "?")
                      (list '? (convert-to-prefix-form (mem2 P))))
                    ((equal (mem1 P) "&")
                      (gen-conjunction (mapcar #'convert-to-prefix-form (cdr P))))
                    ((equal (mem1 P) "v")
                      (gen-disjunction (mapcar #'convert-to-prefix-form (cdr P))))
                    (t
                      (let ((mem2 (mem2 p)))
                        (cond
                          ((equal mem2 "v")
                            (list 'v (convert-to-prefix-form (mem1 P)) (convert-to-prefix-form (mem3 P))))
                          ((equal mem2 "&")
                            (list '& (convert-to-prefix-form (mem1 P)) (convert-to-prefix-form (mem3 P))))
                          ((equal mem2 "->")
                            (list '-> (convert-to-prefix-form (mem1 P)) (convert-to-prefix-form (mem3 P))))
                          ((equal mem2 "<->")
                            (list '<-> (convert-to-prefix-form (mem1 P)) (convert-to-prefix-form (mem3 P))))
                          ((equal mem2 "@")
                            (list '@ (convert-to-prefix-form (mem1 P)) (convert-to-prefix-form (mem3 P))))
                          ;;========================================================
                          ((some
                             #'(lambda (rf)
                                   (let ((m (match (mem1 rf) P (mem3 rf))))
                                     (when m
                                          (when (listp m)
                                               (setf m
                                                        (mapcar
                                                          #'(lambda (x)
                                                                (if (consp x)
                                                                  (cons (car x) (convert-to-prefix-form (cdr x)))
                                                                  (cdr x)))
                                                          m)))
                                          (setf P* (match-sublis m (mem2 rf))))))
                             *reform-list*)
                            P*)
                          ;;========================================================
                          ((listp (mem1 P))
                            (cond ((equal (mem1 (mem1 P)) "all")
                                        (cond ((eq (mem3 (mem1 P)) :type)
                                                    (list 'all (mem2 (mem1 P)) (mem3 (mem1 P)) (mem4 (mem1 P))
                                                           (convert-to-prefix-form (mem2 P))))
                                                  (t (list 'all (mem2 (mem1 P)) (convert-to-prefix-form (mem2 P))))))
                                      ((equal (mem1 (mem1 P)) "some")
                                        (cond ((eq (mem3 (mem1 P)) :type)
                                                    (list 'some (mem2 (mem1 P)) (mem3 (mem1 P)) (mem4 (mem1 P))
                                                           (convert-to-prefix-form (mem2 P))))
                                                  (t (list 'some (mem2 (mem1 P)) (convert-to-prefix-form (mem2 P))))))
                                      ((equal (mem1 (mem1 P)) "?")
                                        (list '? (mem2 (mem1 P)) (convert-to-prefix-form (mem2 P))))
                                      (t (mapcar #'convert-to-prefix-form P))))
                          (t (mapcar #'convert-to-prefix-form P)))))))
                (t P))))

(defunction pretty (p)
    (let ((p* nil))
      (cond ((stringp p) p)
                ((symbolp p) (convert-to-string p))
                ; ((identityp p) (imp (list "(" (pretty (iden1 p)) " = " (pretty (iden2 p)) ")")))
                ((negationp p) (imp (list "~" (pretty (negand p)))))
                ((u-genp p)
                  (implode
                    (cond ((eq (mem3 P) :type)
                                (list "(all" " " (convert-to-string (mem2 p)) " " (convert-to-string (mem3 p))
                                        " " (convert-to-string (mem4 p)) ")" (pretty (mem5 p))))
                              (t (list "(all" " " (convert-to-string (mem2 p))
                                         ")" (pretty (mem3 p)))))))
                ((e-genp p)
                  (implode
                    (cond ((eq (mem3 P) :type)
                                (list "(some" " " (convert-to-string (mem2 p)) " " (convert-to-string (mem3 p))
                                        " " (convert-to-string (mem4 p)) ")" (pretty (mem5 p))))
                              (t (list "(some" " " (convert-to-string (mem2 p))
                                         ")" (pretty (mem3 p)))))))
                ((?-genp p)
                  (implode
                    (list "(?" " " (convert-to-string (mem2 p))
                           ")" (pretty (mem3 p)))))
                ((and (listp p) (not (listp (cdr p)))) (write-to-string p))
                ((listp p)
                  (let ((mem1 (mem1 p)))
                    (cond
                      ((equal mem1 'v)
                        (imp (list "(" (pretty (mem2 P)) " " "v" " " (pretty (mem3 P)) ")")))
                      ((equal mem1 '&)
                        (imp (list "(" (pretty (mem2 P)) " " "&" " " (pretty (mem3 P)) ")")))
                      ((equal mem1 '->)
                        (imp (list "(" (pretty (mem2 P)) " " "->" " " (pretty (mem3 P)) ")")))
                      ((equal mem1 '<->)
                        (imp (list "(" (pretty (mem2 P)) " " "<->" " " (pretty (mem3 P)) ")")))
                      ((equal mem1 '@)
                        (imp (list "(" (pretty (mem2 P)) " " "@" " " (pretty (mem3 P)) ")")))
                      ((equal mem1 '?) (imp (list "(? " (pretty (mem2 P)) ")")))
                  ;    ((equal mem1 'open) (imp (list "(" (pretty (mem2 P)) " " (pretty (mem3 P)) ")")))
                  ;    ((equal mem1 'closed) (imp (list "[" (pretty (mem2 P)) " " (pretty (mem3 P)) "]")))
                  ;    ((equal mem1 'clopen) (imp (list "(" (pretty (mem2 P)) " " (pretty (mem3 P)) "]")))
                    ;  ((equal mem1 'protoplan-for)
                    ;    (imp (list "(protoplan-for " (pretty (mem2 P)) " " (pretty (mem3 P)) ")")))
                         ; (append (list "(protoplan-for " (pretty (mem2 P)) " " (pretty (mem3 P)) " { ")
                         ;                (unionmapcar #'(lambda (x) (list (pretty x) " ")) (mem4 P)) '("})"))))
                    ; ((equal mem1 'embellished-protoplan-for)
                    ;   (imp 
                    ;     (append (list "(embellished-protoplan-for " (pretty (mem2 P)) " { ")
                    ;                     (unionmapcar #'(lambda (x) (list (pretty x) " ")) (mem3 P)) '("} ")
                    ;                     (list (pretty (mem4 P)) ")"))))
                                       ;  " { ")
                                       ;  (unionmapcar #'(lambda (x) (list (pretty x) " ")) (mem5 P)) '("})"))))
                      ;;========================================================
                      ((some #'(lambda (rf)
                                         (let ((m (match (mem2 rf) P (mem3 rf))))
                                           (when m
                                                (when (listp m)
                                                     (setf m
                                                              (mapcar
                                                                #'(lambda (x) (if (consp x) (cons (car x) (pretty (cdr x))) (cdr x))) m)))
                                                (setf P* (match-sublis m (mem1 rf))))))
                                   *reform-list*)
                        (remove-if-equal #\" (pretty P*)))
                      ;;========================================================
                      (t
                        (imp (cons "(" (append (pretty-cons p) (list ")"))))))))
                (t (write-to-string p))
                )))

(def-forwards-reason RELATIVIZED-UI
    :conclusions P*
    :forwards-premises
        "(all x :type type) P)"
        "(:type object type)"
        "(define P* (subst object x P))"
    :variables  x type object P P*)

;;============================ interest priorities ====================================
(proclaim '(special *answered-priority*))

(setf *answered-priority* .005)

(defunction affected-items
    (new-beliefs new-retractions altered-interests altered-queries &optional display)
    ;; (affected-items nb nr ai aq t)
    (let* ((affected-nodes (append new-beliefs new-retractions))
              (affected-interests
                (union altered-interests (mapcar #'query-interest altered-queries)))
              (new-affected-nodes affected-nodes)
              (new-affected-interests affected-interests))
      (when display
         (princ "affected-nodes: ") (princ affected-nodes) (terpri)
         (princ "affected-interests: ") (princ affected-interests) (terpri))
      (dolist (query altered-queries)
          (pushnew (query-interest query) altered-interests))
      (loop
        (when display (princ "=======") (terpri))
        (dolist (node new-affected-nodes)
            (pull node new-affected-nodes)
            (when display (terpri) (princ "from ") (princ node) (terpri))
            (dolist (n (node-consequences node))
                (when (not (member n affected-nodes))
                (when display (princ "     ") (princ n) (princ " node-consequence") (terpri))
                      (push n affected-nodes)
                      (push n new-affected-nodes)))
            (dolist (in (generated-interests node))
                (when (not (member in affected-interests))
                (when display (princ "     ") (princ in) (princ " generated-interest") (terpri))
                      (push in affected-interests)
                      (push in new-affected-interests)))
            (when (and (listp (node-formula node))
                                (or (eq (car (node-formula node)) 'plan-for)
                                      (eq (car (node-formula node)) 'embellished-plan-for)))
                 (dolist (x (discharged-interests node))
                     (let ((in (car x)))
                       (when (not (member in affected-interests))
                            (when display (princ "     ") (princ in) (princ " discharged protoplan interest") (terpri))
                            (push in affected-interests)
                            (push in new-affected-interests)))))
            (dolist (in (generated-defeat-interests node))
                (when (not (member in affected-interests))
                (when display (princ "     ") (princ in) (princ " generated-defeat-interest") (terpri))
                      (push in affected-interests)
                      (push in new-affected-interests)))
            (when (eq (node-justification node) :reductio-supposition)
                 (dolist (in *direct-reductio-interests*)
                     (when (not (member in affected-interests))
                          (when display (princ "     ") (princ in) (princ " direct reductio interest") (terpri))
                          (push in affected-interests)
                          (push in new-affected-interests)))))
        (dolist (interest new-affected-interests)
            (pull interest new-affected-interests)
            (when display (terpri) (princ "from ") (princ interest) (terpri))
            (dolist (L (left-links interest))
                (let ((in (link-interest L)))
                  (when (not (member in affected-interests))
                 (when display (princ "     ") (princ in) (princ " from left link") (terpri))
                       (push in affected-interests)
                       (push in new-affected-interests))))
            (dolist (n (generated-suppositions interest))
                (when (not (member n affected-nodes))
                (when display (princ "     ") (princ n) (princ " generated-supposition") (terpri))
                      (push n affected-nodes)
                      (push n new-affected-nodes))))
        (when (and (null new-affected-nodes) (null new-affected-interests))
                (when display (princ "Affected-nodes: ") (princ affected-nodes) (terpri))
                (when display (princ "Affected-interests: ") (princ affected-interests) (terpri) (terpri))
             (return (list affected-nodes affected-interests))))))

#|
(find-if #'(lambda (i)
                  (some #'(lambda (L)
                                   (some #'(lambda (link) (equal (resultant-interest link) i))
                                               (right-links (resultant-interest L))))
                              (right-links i)))
            af)
|#

(defunction i-preferred (node1 node2)
    (or (and (eq (item-kind node2) :interest)
                  (eql (interest-priority (enqued-item node2)) *answered-priority*))
          (> (degree-of-preference node1) (degree-of-preference node2))
          (and (eql (degree-of-preference node1) (degree-of-preference node2))
                   (eq (item-kind node1) :conclusion) (eq (item-kind node2) :interest))))

(defunction recompute-priorities (new-beliefs new-retractions altered-interests altered-queries  &optional display)
    ; (when (eql *cycle* 79) (setf nb new-beliefs nr new-retractions ai altered-interests aq altered-queries)  (break))
    ;; (step (recompute-priorities nb nr ai aq))
     ;; (recompute-priorities nb nr ai aq t)
    (let* ((affected-items (affected-items new-beliefs new-retractions altered-interests altered-queries display))
              (affected-nodes (mem1 affected-items))
              (affected-interests (mem2 affected-items))
              (altered-queue nil))
      (dolist (query altered-queries)
          (let ((interest (query-interest query)))
            (pull interest affected-interests)
            (cond ((and (answered? query)
                                (not (member query *permanent-ultimate-epistemic-interests*)))
                        (setf (interest-priority interest) *answered-priority*)
                        (when display (princ "soft-cancelling query interest ")
                             (princ interest) (terpri)))
                      (t (setf (interest-priority interest) (maximum-degree-of-interest interest))
                          (when display (princ "reinstating query interest ")
                             (princ interest) (terpri))))))
      ; (dolist (N new-retractions)
      (dolist (N affected-nodes)
          (when (every
                       #'(lambda (L)
                             (some
                               #'(lambda (d)
                                     (and (not (equal (node-formula d) (neg (node-formula N))))
                                              (or (null (support-link-strength L))
                                                    (<= (support-link-strength L)
                                                           (undefeated-degree-of-support d)))))
                               (support-link-defeaters L)))
                       (support-links N))
               (pull N affected-nodes)
            (when display (princ "soft-cancelling undercut node ")
                       (princ N) (terpri))
               (setf (discounted-node-strength N) *answered-priority*)
               (let ((Q (node-queue-node N)))
                 (when Q (pushnew Q altered-queue))))
          (when (zerop (undefeated-degree-of-support N))
               (dolist (in (generated-defeat-interests N))
                   (when (member in affected-interests)
                        (pull in affected-interests)
                        (setf (interest-priority in) *answered-priority*)
                        (when display (princ "soft-cancelling generated-defeat-interest ")
                             (princ in) (terpri))
                        (let ((Q (interest-queue-node in)))
                          (when Q (pushnew Q altered-queue)))))))
      (dolist (node affected-nodes)
       (when display (terpri) (princ "from ") (princ node) (terpri))
          (when (listp (node-formula node))
               (cond ((zerop (undefeated-degree-of-support node))
                           (when (or (eq (car (node-formula node)) 'plan-for)
                                             (eq (car (node-formula node)) 'embellished-plan-for))
                                (dolist (x (discharged-interests node))
                                    (let ((in (car x)))
                                      (when (and (member in affected-interests)
                                                          (every
                                                            #'(lambda (n) (zerop (undefeated-degree-of-support n)))
                                                            (discharging-nodes in)))
                                           (pull in affected-interests)
                                           (when display
                                     (princ "     requeueing no longer discharged plan interest ")
                                     (princ in) (terpri))
                                           (let ((Q (interest-queue-node in)))
                                             (when Q (pushnew Q altered-queue))))))))
                         ((or (eq (car (node-formula node)) 'plan-for)
                                (eq (car (node-formula node)) 'embellished-plan-for))
                           (dolist (x (discharged-interests node))
                               (let ((in (car x)))
                                 (when (not (eql (interest-priority in) *answered-priority*))
                                      (pull in affected-interests)
                                      (setf (interest-priority in) *answered-priority*)
                             (when display
                                 (princ "     requeueing newly discharged plan interest ")
                                 (princ in) (terpri))
                                       (let ((Q (interest-queue-node in)))
                                         (when Q (pushnew Q altered-queue)))))))))
          (cond ((zerop (undefeated-degree-of-support node))
                      ;; If a node is defeated, its discounted-node-strength is *base-priority*.
                      (pull node affected-nodes)
                 (when display
                     (princ "     requeueing defeated node ") (princ node)
                     (princ " with discounted-node-strength ")
                     (princ (discounted-node-strength node)) (terpri))
                      (setf (discounted-node-strength node) *base-priority*)
                      (let ((Q (node-queue-node node)))
                        (when Q (pushnew Q altered-queue))))
                    ((null (generating-interests node))
                      ;; If an undefeated node has an empty list of generating-interests, its 
                      ;; discounted-node-strength is the maximum  (over its node-arguments) 
                      ;; of the product of the discount-factor of the support-link-rule of the last 
                      ;; support-link in the argument and the strength of the argument.  
                      ;; (This case includes all non-suppositional nodes.)
                      (pull node affected-nodes)
                 (when display
                     (princ "     requeueing undefeated affected node with no generating-interests ")
                     (princ node) (princ " with discounted-node-strength ")
                     (princ (discounted-node-strength node)) (terpri))
                      (let ((Q (node-queue-node node)))
                        (when Q (pushnew Q altered-queue))))))
      ;---------------------------------
      (loop
        (when display (princ "=======") (terpri))
        ; (when (eql *cycle* 89) (setf af affected-interests) (break))
        ; (p-print (setf af affected-interests))
        (when (and (null affected-nodes) (null affected-interests)) (return))
        (let ((changes? nil))
          ; ===============
          ;; For each altered-node or altered-interest whose discounted-node-strength 
          ;; or interest-priority can be computed without appealing to any other altered-nodes 
          ;; or altered-interests, we do so and remove them from the lists of altered-nodes 
          ;; and altered-interests.  Repeat this step until no further nodes or interests can be 
          ;; removed.  If there are no generation-cycles, this will get them all, but if there are 
          ;; cycles, some may remain.
          (loop
            (when display (princ "          ===============") (terpri))
            (setf changes? nil)
            (dolist (node affected-nodes)
                (let ((reductio-interests (generating-reductio-interests node))
                        (non-reductio-interests (generating-non-reductio-interests node)))
                  (when (and (not (some #'(lambda (in) (member in affected-interests))
                                                          reductio-interests))
                                      (not (some #'(lambda (in) (member in affected-interests))
                                                          non-reductio-interests)))
                       (setf changes? t)
                       (pull node affected-nodes)
                       ;; If a node is a supposition, its discounted-node-strength is the maximum of:
                       ;;  (1)  the product of *reductio-discount* and the maximum of the 
                       ;;  interest-priorities of the generating-interests for which it is a 
                       ;;  reductio-supposition; and
                       ;;  (2)  the interest-priorities of the generating-interests for which it is 
                       ;;  not a reductio-supposition.
                       (setf (discounted-node-strength node)
                                (max
                                  (* *reductio-discount*
                                       (maximum0 (mapcar #'interest-priority reductio-interests)))
                                  (maximum0 (mapcar #'interest-priority non-reductio-interests))))
                       (let ((Q (node-queue-node node)))
                         (when display (princ "               requeuing supposition ") (princ node)
                             (princ " with discounted-node-strength ")
                             (princ (discounted-node-strength node)) (terpri))
                         (when Q (pushnew Q altered-queue))))))
            (dolist (interest affected-interests)
                (let ((GN (broadly-generating-nodes interest))
                        (links (subset #'(lambda (L) (null (link-defeat-status L))) (right-links interest))))
                  (cond ((and (null GN) (null links))
                              ;; If an interest has neither generating-nodes nor undefeated right-links,
                              ;;  its interest-priority is *defeater-priority*  (This includes interest in defeaters.)
                              (setf changes? t)
                              (pull interest affected-interests)
                              (setf (interest-priority interest) *defeater-priority*)
                              (when display
                           (princ "               requeuing interest with broadly generating nodes but not undefeated right links ")
                           (princ interest) (princ " with interest-priority ")
                           (princ (interest-priority interest)) (terpri))
                              (let ((Q (interest-queue-node interest)))
                                (when Q (pushnew Q altered-queue))))
                            ((and (not (some #'(lambda (n) (member n affected-nodes)) GN))
                                      (not (some #'(lambda (link) (member (resultant-interest link) affected-interests)) links)))
                              ;; Otherwise, the interest-priority is the maximum of:
                              ;;  (1)  the discounted-node-strengths of its generating-nodes that are 
                              ;;  not reductio-suppositions;
                              ;;  (2)  the product of *reductio-interest* and the maximum of the 
                              ;;  discounted-node-strengths of its generating-nodes that are 
                              ;;  reductio-suppositions;
                              ;;  (3)  for each of its right-links, the product 
                              ;;  of the discount-factor of the link-rule and the interest-priority of the 
                              ;;  resultant-interest.
                              (setf changes? t)
                              (pull interest affected-interests)
                              (setf (interest-priority interest)
                                       (maximum
                                         (append
                                           (mapcar
                                             #'(lambda (n)
                                                   (if (eq (node-justification n) :reductio-supposition)
                                                     (* *reductio-interest* (compute-discounted-node-strength n))
                                                     (compute-discounted-node-strength n)))
                                             GN)
                                           (mapcar
                                             #'(lambda (L)
                                                   (if (eq (link-rule L) :answer)
                                                     (query-strength (resultant-interest L))
                                                     (* (discount-factor (link-rule L))
                                                          (interest-priority (resultant-interest L)))))
                                             links))))
                              (when display
                           (princ "               requeuing interest with no affected broadly generating odes and no undefeated right links with affected resultant interests ")
                           (princ interest) (princ " with interest-priority ")
                           (princ (interest-priority interest)) (terpri))
                              (let ((Q (interest-queue-node interest)))
                                (when Q (pushnew Q altered-queue)))))))
            (when (and (null affected-nodes) (null affected-interests)) (return))
            (when (null changes?) (return)))
          ; ===============
          (when (and (null affected-nodes) (null affected-interests)) (return))
          ;; For any remaining nodes or interests, we want to compute their discounted-
          ;; nodes-strengths and interest-priorities just in terms of the nodes and interests 
          ;; not involved in the cycles.  Cycles arise from direct-reductio-interests that also 
          ;; have other sources and reductio-suppositions that are also non-reductio-
          ;; suppositions.  So for any such interests and suppositions, compute their 
          ;; interest-priorities and discounted-node-strengths just in terms of those of their 
          ;; sources that are no longer contained in the lists of altered-nodes or altered-interests.
          (dolist (node affected-nodes)
              (let ((reductio-interests (generating-reductio-interests node))
                      (non-reductio-interests (generating-non-reductio-interests node)))
                (when (not (some #'(lambda (in) (member in affected-interests))
                                               non-reductio-interests))
                     (setf changes? t)
                     (pull node affected-nodes)
                     ;; If a node is a supposition, its discounted-node-strength is the maximum of:
                     ;;  (1)  the product of *reductio-discount* and the maximum of the 
                     ;;  interest-priorities of the generating-interests for which it is a 
                     ;;  reductio-supposition; and
                     ;;  (2)  the interest-priorities of the generating-interests for which it is 
                     ;;  not a reductio-supposition.
                     (setf (discounted-node-strength node)
                              (max
                                (* *reductio-discount*
                                     (maximum0
                                       (mapcar #'interest-priority
                                                      (subset #'(lambda (in) (not (member in affected-interests)))
                                                                    reductio-interests))))
                                (maximum0 (mapcar #'interest-priority non-reductio-interests))))
                 (when display
                     (princ "     requeueing supposition ")
                     (princ node) (princ " with discounted-node-strength ")
                     (princ (discounted-node-strength node)) (terpri))
                     (let ((Q (node-queue-node node)))
                       (when Q (pushnew Q altered-queue))))))
          (dolist (interest affected-interests)
              (let ((GN (broadly-generating-nodes interest))
                      (links (subset #'(lambda (L) (null (link-defeat-status L))) (right-links interest))))
                (when (and (direct-reductio-interest interest)
                                    (not (some #'(lambda (n)
                                                             (and (not (eq (node-justification n) :reductio-supposition))
                                                                      (member n affected-nodes))) GN))
                                    (not (some #'(lambda (in) (member in affected-interests)) links)))
                     (setf changes? t)
                     (pull interest affected-interests)
                     ;; If an interest has either generating-nodes or undefeated right-links
                     ;;  the interest-priority is the maximum of:
                     ;;  (1)  the discounted-node-strengths of its generating-nodes that are 
                     ;;  not reductio-suppositions;
                     ;;  (2)  the product of *reductio-interest* and the maximum of the 
                     ;;  discounted-node-strengths of its generating-nodes that are 
                     ;;  reductio-suppositions;
                     ;;  (3)  for each of its right-links, the product 
                     ;;  of the discount-factor of the link-rule and the interest-priority of the 
                     ;;  resultant-interest.
                     (setf (interest-priority interest)
                              (maximum
                                (cons
                                  (* *reductio-interest*
                                       (maximum0
                                         (mapcar #'compute-discounted-node-strength
                                                        (subset
                                                          #'(lambda (n)
                                                                (and (eq (node-justification n) :reductio-supposition)
                                                                         (not (member n affected-nodes)))) GN))))
                                  (append
                                    (mapcar #'compute-discounted-node-strength
                                                   (subset
                                                     #'(lambda (n)
                                                           (not (eq (node-justification n) :reductio-supposition)))
                                                     GN))
                                    (mapcar
                                      #'(lambda (L)
                                            (if (eq (link-rule L) :answer)
                                              (query-strength (resultant-interest L))
                                              (* (discount-factor (link-rule L))
                                                   (interest-priority (resultant-interest L)))))
                                      links)))))
                 (when display
                     (princ "     requeueing interest with broadly-generating-nodes or undefeated right links ")
                     (princ interest) (princ " with interest-priority ")
                     (princ (interest-priority interest)) (terpri))
                     (let ((Q (interest-queue-node interest)))
                       (when Q (pushnew Q altered-queue))))))))
      ;---------------------------------
     (when display (princ "----------------") (terpri))
      (dolist (Q altered-queue)
          (cond ((eq (item-kind Q) :conclusion)
                      (setf (discounted-strength Q)
                               (compute-discounted-node-strength (enqued-item Q)))
                      (setf (degree-of-preference Q)
                               (/ (discounted-strength Q) (item-complexity Q)))
                      (let ((n (enqued-item Q)))
                        (cond ((and (listp (node-formula n))
                                            (or (eq (car (node-formula n)) 'embellished-protoplan-for)
                                                  (eq (car (node-formula n)) 'embellished-plan-for)
                                                  (eq (car (node-formula n)) 'plan-undermines-causal-links)
                                                  ))
                                    (cond ((and (every #'(lambda (in) (equal (interest-priority in) *answered-priority*))
                                                                    (enabling-interests n))
                                                        (every #'(lambda (L)
                                                                          (let ((R (support-link-rule L)))
                                                                            (and (backwards-reason-p R) (backwards-premises R))))
                                                                    (support-link n)))
                                    (when display
                                        (princ "     unqueueing plan node with softly-cancelled enabling interests ")
                                        (princ n) (terpri))
                                                (pull Q *inference-queue*))
                                              (t
                                    (when display
                                        (princ "     requeueing plan node ") (princ n) (terpri))
                                                (setf *inference-queue*
                                                         (ordered-insert Q (remove Q *inference-queue*) #'i-preferred)))))
                                  (t
                           (when display
                               (princ "     requeueing non-plan node ") (princ n) (terpri))
                                    (setf *inference-queue*
                                             (ordered-insert Q (remove Q *inference-queue*) #'i-preferred))))))
                    ((not (cancelled-interest (enqued-item Q)))
                      (setf (discounted-strength Q) (interest-priority (enqued-item Q)))
                      (setf (degree-of-preference Q)
                               (/ (discounted-strength Q) (item-complexity Q)))
                      (let ((n (enqued-item Q)))
                        (cond ((and (listp (interest-formula n))
                                            (or (eq (car (interest-formula n)) 'protoplan-for)
                                                  (eq (car (interest-formula n)) 'embellished-protoplan-for)
                                                  (eq (car (interest-formula n)) 'embellished-plan-for)
                                                  (eq (car (interest-formula n)) 'plan-undermines-causal-links)
                                                  ))
                                    (cond ((eql (interest-priority n) *answered-priority*)
                                    (when display
                                        (princ "     unqueueing softly-cancelled plan interest ")
                                        (princ n) (terpri))
                                                (pull Q *inference-queue*))
                                              (t
                                    (when display
                                        (princ "     requeueing plan interest ") (princ n) (terpri))
                                                (setf *inference-queue*
                                                         (ordered-insert Q (remove Q *inference-queue*) #'i-preferred)))))
                                  (t
                           (when display
                               (princ "     requeueing non-plan interest ") (princ n) (terpri))
                                    (setf *inference-queue*
                                             (ordered-insert Q (remove Q *inference-queue*) #'i-preferred))))))))))

;;=============================== decided-plans =============================

;(defunction decided-node (node)
;    (every
;      #'(lambda (in)
;            (and (processed-interest in)
;                     (every #'decided-node (discharging-nodes in))))
;      (generated-defeat-interests node)))
;
;(defunction processed-interest (interest)
;    (and (null (interest-queue-node interest))
;             (every #'(lambda (L) (processed-interest (link-interest L)))
;                         (left-links interest))))

(defstruct (interest (:print-function print-interest)
                                    (:conc-name nil))   ; "An interest-graph-node"
    (interest-number 0)
    (interest-sequent nil)
    (interest-formula nil)
    (interest-supposition nil)
    (right-links nil)
    (left-links nil)
    (degree-of-interest *base-priority*)
    (last-processed-degree-of-interest nil)
    (interest-defeat-status nil)
    (discharged-degree nil)  ;; used in computing priorities
    (deductive-interest nil)
    (cancelled-interest nil)
    (interest-queue-node nil)
    (interest-i-list nil)
    (maximum-degree-of-interest 0)
    (interest-defeatees nil)
    (reductio-interest nil)
    (direct-reductio-interest nil)
    (generated-suppositions nil)
    (generating-nodes nil)
    (interest-priority 0)
    (interest-variables nil)
    (discharge-condition nil)  ;;a function of node, unifier, and interest-link
    (interest-supposition-variables nil)
    (cancelling-node nil)
    (discharging-nodes nil)
    (interest-supposition-nodes nil)
    (generated-interest-schemes nil)
    (defeater-binding nil)
    (generating-defeat-nodes nil)
    (cancelled-left-links nil)
   (non-reductio-interest t)
    (anchored-nodes nil)
    (text-discharge-condition nil)  ;; a text statement of the discharge condition
    (enabled-nodes nil)  ;; the nodes for which this is an enabling-interest
    (decision-plans nil)  ;; the nodes this interest is relevant to deciding on
    )

(defunction make-undercutting-defeater (base formula supposition antecedent* link reverse-binding)
    ; (when (eql link 64) (setf b base f formula s supposition a antecedent* l link rb reverse-binding) (break))
    ; (setf b base f formula s supposition a antecedent* l link rb reverse-binding) (break)
    ;; (step (make-undercutting-defeater b f s a l rb))
    (let* ((defeater (make-@ (gen-conjunction base) formula))
              (undercutting-defeater
                (cond (antecedent* (conj defeater antecedent*))
                          (t defeater)))
              (undercutting-variables
                (formula-node-variables undercutting-defeater)))
      (multiple-value-bind
           (undercutting-interest i-list)
           (interest-for (list supposition undercutting-defeater)
                                 undercutting-variables nil nil)
           (cond ((null undercutting-interest)
                       (setf undercutting-interest
                                (make-interest
                                  :interest-number (incf *interest-number*)
                                  :interest-sequent (list supposition undercutting-defeater)
                                  :interest-formula undercutting-defeater
                                  :interest-supposition supposition
                                  :interest-variables undercutting-variables
                                  :interest-supposition-variables (supposition-variables supposition)
                                  :interest-defeatees (list link)
                                  :interest-priority *defeater-priority*
                                  :defeater-binding (support-link-binding link)
                                  :generating-defeat-nodes (list (support-link-target link))
                                  :decision-plans
                                  (when (eq (support-link-rule link) protoplan)
                                       (list (mem2 (node-formula (support-link-target link)))))
                                  ))
                       (store-interest undercutting-interest i-list)
                       (pushnew undercutting-interest (generated-defeat-interests (support-link-target link)))
                       (when *display?* 
                            (display-interest undercutting-interest)
                            (princ 
                              "                                        Of interest as defeater for support-link ")
                            (princ (support-link-number link)) (terpri) (terpri))
                       (when *log-on* (push undercutting-interest *reasoning-log*))
                       (when (and *display?* *graphics-on* *graph-interests*)
                            (draw-i undercutting-interest *og*))
                       (instantiate-defeater
                         undercutting-interest defeater antecedent* link reverse-binding))
                     (t 
                       (readopt-interest undercutting-interest (list link))
                       (push undercutting-interest (generated-defeat-interests (support-link-target link)))
                       (push (support-link-target link) (generating-defeat-nodes undercutting-interest))
                       (when (eq (support-link-rule link) protoplan)
                            (push (mem2 (node-formula (support-link-target link)))
                                      (decision-plans undercutting-interest)))
                       (dolist (in (discharged-interests (support-link-target link)))
                           (dolist (p (decision-plans (car in)))
                               (pushnew p (decision-plans undercutting-interest))))
                       (setf (interest-defeatees undercutting-interest)
                                (cons link (interest-defeatees undercutting-interest)))))
           (dolist (node (unifying-nodes undercutting-interest))
               (when (subsetp= (node-supposition node) supposition)
                    (when *display?*
                         (princ "  Node # ") (princ (inference-number node))
                         (princ " defeats link # ")
                         (princ (support-link-number link)) (terpri))
                    (pushnew node (support-link-defeaters link))
                    (pushnew node (discharging-nodes undercutting-interest))
                    (pushnew link (node-defeatees node)))))))

(defunction make-rebutting-defeater (variables base formula supposition antecedent* link)
    (let ((rebutting-defeater
              (cond (antecedent* (conj antecedent* (conj (gen-conjunction base) (neg formula))))
                        (variables (conj (gen-conjunction base) (neg formula)))
                        (t (neg formula))))
            (rebutting-variables
              (node-variables (support-link-target link))))
      (multiple-value-bind
           (rebutting-interest i-list)
           (interest-for (list supposition rebutting-defeater) rebutting-variables nil nil)
           (cond ((null rebutting-interest)
                       (setf rebutting-interest
                                (make-interest
                                  :interest-number (incf *interest-number*)
                                  :interest-sequent (list supposition rebutting-defeater)
                                  :interest-formula rebutting-defeater
                                  :interest-supposition supposition
                                  :interest-variables rebutting-variables
                                  :interest-supposition-variables (supposition-variables supposition)
                                  :interest-defeatees (list link)
                                  :interest-priority *defeater-priority*
                                  :generating-defeat-nodes (list (support-link-target link))
                                  :decision-plans
                                  (when (eq (support-link-rule link) protoplan)
                                       (list (mem2 (node-formula (support-link-target link)))))))
                       (store-interest rebutting-interest i-list)
                       (pushnew rebutting-interest (generated-defeat-interests (support-link-target link)))
                       (when *display?* 
                            (display-interest rebutting-interest)
                            (princ 
                              "                                        Of interest as defeater for support-link ")
                            (princ (support-link-number link)) (terpri) (terpri))
                       (when *log-on* (push rebutting-interest *reasoning-log*))
                       (when (and *display?* *graphics-on* *graph-interests*)
                            (draw-i rebutting-interest *og*))
                       (queue-interest
                         rebutting-interest *defeater-priority*))
                     (t 
                       (readopt-interest rebutting-interest (list link))
                       (push rebutting-interest (generated-defeat-interests (support-link-target link)))
                       (push (support-link-target link) (generating-defeat-nodes rebutting-interest))
                       (when (eq (support-link-rule link) protoplan)
                                       (push (mem2 (node-formula (support-link-target link)))
                                                 (decision-plans rebutting-interest)))
                       (dolist (in (discharged-interests (support-link-target link)))
                           (dolist (p (decision-plans (car in)))
                               (pushnew p (decision-plans rebutting-interest))))
                       (setf (interest-defeatees rebutting-interest)
                                (cons link (interest-defeatees rebutting-interest)))))
           (dolist (node (unifying-nodes rebutting-interest))
               (when (subsetp= (node-supposition node) supposition)
                    (when *display?*
                         (princ "  Node # ") (princ (inference-number node))
                         (princ " defeats link # ")
                         (princ (support-link-number link)) (terpri))
                    (pushnew node (support-link-defeaters link))
                    (pushnew node (discharging-nodes rebutting-interest))
                    (pushnew link (node-defeatees node)))))))

(defunction defeater-priority (interest)
    (declare (ignore interest))
    *defeater-priority*)

(defunction instantiate-defeater (undercutting-interest defeater antecedent* link reverse-binding)
   ; (setf u undercutting-interest d defeater a antecedent* l link r reverse-binding) (break)
    ;; (step (instantiate-defeater u d a l r))
    (let ((binding (match-sublis reverse-binding (support-link-binding link) :test 'equal)))
      (cond
        (antecedent*
          (let*
            ((i-link
               (construct-initial-interest-link
                 nil nil adjunction undercutting-interest 0 *defeater-priority*
                 (list (cons 'p defeater) (cons 'q antecedent*)) (interest-supposition undercutting-interest)))
              (interest (link-interest i-link)))
            (dolist (reason (undercutting-defeaters (support-link-rule link)))
                (when (and (member reason *backwards-reasons*) (funcall* (reason-condition reason) binding))
                     (let ((supposition (interest-supposition interest)))
                       (cond
                         ((forwards-premises reason)
                           (construct-interest-scheme
                             reason nil interest binding nil (forwards-premises reason) nil 1
                             *defeater-priority* supposition))
                         (t (make-backwards-inference 
                               reason binding interest 1 *defeater-priority* nil nil nil supposition))))))))
        (t
          (dolist (reason (undercutting-defeaters (support-link-rule link)))
              (when (and (member reason *backwards-reasons*) (funcall* (reason-condition reason) binding))
                   (let ((supposition (interest-supposition undercutting-interest)))
                     (cond
                       ((forwards-premises reason)
                         (construct-interest-scheme
                           reason nil undercutting-interest binding nil (forwards-premises reason) nil 1
                           *defeater-priority* supposition))
                       (t (make-backwards-inference 
                             reason binding undercutting-interest 1 *defeater-priority* nil nil nil supposition))))))))))

(defunction compute-link-interest
    (link condition1 condition2 degree max-degree depth priority &optional new-vars text-condition)
    (declare (ignore new-vars))
    ; (setf l link c1 condition1 c2 condition2 d degree md max-degree dp depth p priority nv new-vars) ; (break))
    ;; (step (compute-link-interest l c1 c2 d md dp p nv))
    (let* ((interest-priority
                (if priority
                  (* priority (discount-factor (link-rule link)))
                  (interest-priority (resultant-interest link))))
              (vars (formula-node-variables (link-interest-formula link))))
      (multiple-value-bind
           (interest i-list match match*)
           (interest-for (list (link-supposition link) (link-interest-formula link)) vars condition1 link)
           (cond
             (interest
               (setf (degree-of-interest interest) (min (degree-of-interest interest) degree))
               (setf (maximum-degree-of-interest interest)
                        (max (maximum-degree-of-interest interest) max-degree))
               (when (not (reductio-interest interest))
                    (setf (reductio-interest interest) (reductio-interest (resultant-interest link))))
               (setf (interest-priority interest) (max (interest-priority interest) interest-priority))
               (let ((gn (link-generating-node link)))
                 (when gn
                      (pushnew gn (generating-nodes interest))
                      (push interest (generated-interests gn))))
               (if (right-links interest)
                 (setf (right-links interest) (reverse (cons link (reverse (right-links interest)))))
                 (setf (right-links interest) (list link)))
             ;  (setf (interest-depth interest)
             ;           (min (interest-depth interest) (1+ (interest-depth (resultant-interest link)))))
               (setf (interest-match link) match)
               (setf (interest-reverse-match link) match*)
               (readopt-interest interest nil))
             (t
               (setf interest
                        (construct-new-interest-for
                          link vars condition2 degree max-degree depth i-list text-condition))

               ;; (when *display?* (terpri) (princ (car (link-instantiations link))) (terpri) (terpri))

              ; (let ((i-depth (interest-depth (resultant-interest link))))
              ;   (setf (interest-depth interest) (1+ i-depth))
              ;   (setf (interest-priority interest) (* interest-priority (/  i-depth (1+ i-depth)))))
               
               (setf (interest-priority interest) interest-priority)
               ))
           (setf (link-interest link) interest)
           (dolist (p (decision-plans (resultant-interest link)))
               (pushnew p (decision-plans interest)))
           )))

(defunction decided-node (node)
    (and (every #'decided-interest (generated-defeat-interests node))
             (every #'(lambda (L)
                               (every #'decided-node (support-link-defeaters L)))
                         (support-links node))))

(defunction decided-interest (interest)
    (and (null (interest-queue-node interest))
             (every #'decided-node (discharging-nodes interest))
             (every #'(lambda (L)
                               (decided-interest (link-interest L)))
                         (left-links interest))))

(defunction SOLVE-PLANNING-PROBLEM ()
    (let ((pp *print-pretty*)
            (red *use-reductio*))
      (setf *print-pretty* nil)
      (setf *use-reductio* nil)
      (gc)
      (unwind-protect
          (progn
              (display-planning-settings)
              (setf *premises* **premises**)
              (setf *plan-number* 0)
              (setf *plan-node-number* 0)
              (setf *start* (make-plan-node))
              (setf *plans* nil)
              (setf *plan-nodes* (list *start*))
              (setf *causal-link-number* 0)
              (setf *causal-links* nil)
              (initialize-reasoner)
              (setf *empty-inference-queue* nil)
              (setf *cycle* *start-time*)
              (setf *display-time* 0)
              (setf *plans-decided* nil)
              (let* (;(max-input-cycle
                     ;     (maximum0 (union= (domain *inputs*) (remove nil (mapcar #'caddr *premises*)))))
                        (time (get-internal-run-time))
                        (abort-time (if *time-limit* (+ (* *time-limit* internal-time-units-per-second 60) time))))
                ; (when (not *display?*) (gc))
                (catch 'die 
                   (dolist (query *ultimate-epistemic-interests*)
                       (reason-backwards-from-query query (query-strength query) 0))
                   (loop
                     (cond ;((and *inference-queue*
                       ;             (every
                       ;               #'(lambda (q)
                       ;                     (and (interest-p (enqued-item q))
                       ;                              (<= (interest-priority (enqued-item q)) *answered-priority*)))
                       ;               *inference-queue*))
                       ;     (return))
                       ; ((eq *cycle* 114) (break))
                       ((null *inference-queue*) (return))
                       ((some
                                  #'(lambda (c)
                                        (and (decided-node c)
                                                 (>= (compute-undefeated-degree-of-support C) (query-strength (query 1)))))
                                       (query-answers (query 1)))
                                 (return))
                     ;  (*inference-queue*
                     ;    (if *empty-inference-queue* (setf *empty-inference-queue* nil)))
                     ;  ((and (not (zerop max-input-cycle)) (> *cycle* max-input-cycle)) (return))
                     ;  ((not *empty-inference-queue*)
                     ;    (setf *empty-inference-queue* t)
                     ;    ; (when *display?*
                     ;    (terpri) (terpri)
                     ;    (princ "-------------------------------------------------") (terpri) (terpri)
                     ;    (princ "                    Waiting for input") (terpri) (terpri)
                     ;    (princ "-------------------------------------------------") (terpri)
                     ;    (terpri) (terpri)))
                     )
                     (incf *cycle*)
                    ; (when (eql *cycle* 30) (break))
                     (update-percepts)
                     (dolist (percept *percepts*)
                         (pull percept *percepts*)
                         (queue-percept percept))
                     (dolist (premise *premises*)
                         (when (eq (mem4 premise) *cycle*)
                              (pull premise *premises*)
                              (queue-premise premise)))
                     (think)
                     (when (and abort-time (> (get-internal-run-time) abort-time))
                          (princ "NO PROOF WAS FOUND WITHIN ") (princ *time-limit*) (princ " MINUTES.")
                          (throw 'die nil))
                     ; (initiate-actions)
                     ))
                (setf time (- (- (get-internal-run-time) time) *display-time*))
                (display-queries) (terpri)
                (when (not *display?*)
                     (princ "Elapsed time = ") (display-run-time-in-seconds time) (terpri))
                (let ((nodes nil))
                  (dolist (query *ultimate-epistemic-interests*)
                      (dolist (N (query-answers query))
                          (pushnew N nodes)))
                  (compute-strictly-relevant-nodes nodes)
                  (let ((argument-length (length *strictly-relevant-nodes*)))
                    (cond (*proofs?* (terpri) (show-arguments))
                              (t (princ "Cumulative size of arguments = ") (princ argument-length) (terpri)
                                  (princ "Size of inference-graph = ") (princ *inference-number*)
                                  (princ " of which ") (princ *unused-suppositions*)
                                  (princ " were unused suppositions.") (terpri)
                                  (princ (truncate (* argument-length 100) *inference-number*))
                                  (princ "% of the inference-graph was used in the argument.") (terpri)))
                    (princ *interest-number*) (princ " interests were adopted.") (terpri)
                    (let ((ri (length (subset 
                                               #'(lambda (in)
                                                     (some #'(lambda (N) (member N *strictly-relevant-nodes*))
                                                                 (discharging-nodes in)))
                                               *interests*))))
                      (princ ri) (princ " interests were discharged by nodes used in the solution.") (terpri)
                      (princ (truncate (* ri 100) *interest-number*))
                      (princ "% of the interests were used directly in finding the solution.") (terpri)
                      (when (not (zerop ri))
                           (princ "The branching factor = ")
                           ; (princ (/ (truncate (* 100 (log *interest-number*)) (log ri)) 100.0)) (terpri))
                           (princ (/ (truncate (* 100 (expt *interest-number* (/ 1 ri)))) 100.0)) (terpri)))
                    (princ *interest-scheme-number*) (princ " interest-schemes were constructed.") (terpri)
                    (princ (- *ip-number* (length *forwards-logical-reasons*)))
                    (princ " instantiated-premises were constructed.") (terpri)
                    (princ *cycle*) (princ " cycles of reasoning occurred.") (terpri)
                    (princ (length *plans*)) (princ " plans were constructed.") (terpri)
                    (analyze-schemes)
                    (when *display?*
                         (princ "The following nodes were used in the arguments:") (terpri)
                         (print-list (order (mapcar #'inference-number *strictly-relevant-nodes*) #'<) 40))
                    (terpri)
                    (push (list *problem-number* time argument-length
                                     (- *inference-number* *unused-suppositions*) (length *plans*)
                                     (answered? (mem1 *ultimate-epistemic-interests*))) *test-log*)))
                (when *log-on* (terpri) (display-reasoning) (display-queries))
                (princ ")") (terpri)))
          (setf *print-pretty* pp)
        (setf *use-reductio* red))))

(defunction think ()
    (when (some
                 #'(lambda (p)
                       (and
                         (some #'(lambda (n)
                                          (and (eq (car (node-formula n)) 'plan-for)
                                                   (not (zerop (undefeated-degree-of-support n)))))
                                     (supporting-inference-nodes p))
                         (every
                           #'(lambda (Q)
                                 (or (not (eq (item-kind Q) :interest))
                                       (not (member p (decision-plans (enqued-item Q))))))
                           *inference-queue*)))
                 *plans-decided*)
         (throw 'die nil))
    ; (when (read-char-no-hang) (clear-input) (throw 'die nil))
    (when (and *display-inference-queue* *display?*) (display-inference-queue))
    (when (eql *cycle* *start-trace*)
         (trace-on)
         (menu-item-disable (oscar-menu-item "Trace on"))
         (menu-item-enable (oscar-menu-item "Trace off"))
         (menu-item-enable (oscar-menu-item "Trace from")))
    (when (eql *cycle* *start-display*)
         (display-on)
         (menu-item-disable (oscar-menu-item "Display on"))
         (menu-item-enable (oscar-menu-item "Display off"))
         (menu-item-enable (oscar-menu-item "Display from")))
    (when *inference-queue*
         (let ((Q (mem1 *inference-queue*)))
           (setf *inference-queue* (cdr *inference-queue*))
           (when *display?*
                (princ "---------------------------------------------------------------------------") (terpri)
                (princ *cycle*) (princ ":    ")
                (princ "Retrieving ") (princ (enqued-item Q))
                (princ " from the inference-queue.")
                (terpri) (terpri))
           (pause)
           (cond ((eq (item-kind Q) :conclusion)
                       (setf *plans-decided* nil)
                       (let ((node (enqued-item Q)))
                         (when (eq (node-kind node) :inference)
                              (store-processed-inference-node node)
                              (setf (node-queue-node node) nil))
                         (reason-forwards-from node 0)))
                     (t
                       (let ((priority
                                 (retrieved-interest-priority
                                   (degree-of-preference Q) (item-complexity Q))))
                         (cond ((eq (item-kind Q) :query)
                                     (setf *plans-decided* nil)
                                     (let ((query (enqued-item Q)))
                                       (setf (query-queue-node query) nil)
                                       (reason-backwards-from-query query priority 0)))
                                   ((eq (item-kind Q) :interest)
                                     (let ((interest (enqued-item Q)))
                                       (setf *plans-decided* (decision-plans interest))
                                       (setf (interest-queue-node interest) nil)
                                       (reason-backwards-from interest priority 0)
                                       (form-epistemic-desires-for interest)))))))))
    (when *new-links*
         (update-beliefs)
         (setf *new-links* nil)))

(defunction display-query (Q)
    (setf *solutions* nil)
    (princ "  Interest in ") (prinp (query-formula Q)) (terpri)
    (cond ((null (answered? Q))
                 (princ "  is unsatisfied.")
                 (when (null (query-answers Q)) (princ "  NO ARGUMENT WAS FOUND."))
                 (terpri))
              ((or (whether-query-p Q) (?-query-p Q))
                (dolist (C (query-answers Q))
                    (when (and (>= (compute-undefeated-degree-of-support C) (query-strength Q))
                                        (let ((p (mem2 (node-formula C))))
                                          (or (not (plan-p p))
                                                (every
                                                  #'(lambda (Q)
                                                        (or (not (eq (item-kind Q) :interest))
                                                              (not (member p (decision-plans (enqued-item Q))))))