;;; -*- Mode: LISP; Syntax: Common-lisp; Package: CL-USER -*-

;;; Questions: Why is bond-1 faster than bond, I would have thought the reverse.
;;; (With delay-sat off in both cases.)

;;; Complete logic-based truth maintenance system, version 4 of 7/6/91

;;; Modified: forbus, on 4/27/95
;;; Got rid of annoying compiler warnings.

;;; Copyright (c) 1986, 1987, 1988, 1989, 1990 Kenneth D. Forbus, 
;;; University of Illinois, Johan de Kleer and Xerox Corporation.  
;;; All rights reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.

(in-package :cl-user)

(defun test-explain ()
  (setq *ltms* (create-ltms "Explain Example"))
  (tms-create-node *ltms* "x" :assumptionp t)
  (compile-formula *ltms* `(:or "x" "y"))
  (compile-formula *ltms* `(:or (:not "y") "z"))
  (compile-formula *ltms* `(:or (:not "z") "r"))	
  (enable-assumption (find-node *ltms* "x") :false)
  (explain-node (find-node *ltms* "r")))

(defun test-formula (&optional complete)
	(declare (special r s tt u))
  (setq *ltms* (create-ltms "Formula" :complete complete)
	r (tms-create-node *ltms* "r")
	s (tms-create-node *ltms* "s")
	tt (tms-create-node *ltms* "t")
	u (tms-create-node *ltms* "u"))
  (compile-formula *ltms* `(:implies (:and ,r (:implies ,s ,tt)) ,u)))

(defun run-tests ()
  (test-ask)
  (test-avoid-all)
  (test-bug)
  (test-bug1)
  (test-tax 3)
  (test-tax1 3))

(defun test-ask ()
	(declare (special n1 n2))
  (setq *ltms* (create-ltms "Testing asking")
	n1 (tms-create-node *ltms* "N1" :assumptionp t)
	n2 (tms-create-node *ltms* "N2" :assumptionp t))
  (enable-assumption n1 :false)
  (enable-assumption n2 :false)
  (compile-formula *ltms* `(:or ,n1 ,n2))
  (why-nodes *ltms*))

(defun test-avoid-all ()
	(declare (special n1 n2))
  (setq *ltms* (create-ltms "Testing avoid all"
			    :contradiction-handler 'AVOID-ALL))
  (setq n1 (tms-create-node *ltms* "N1" :assumptionp t)
	n2 (tms-create-node *ltms* "N2" :assumptionp t))
  (enable-assumption n1 :false)
  (enable-assumption n2 :false)
  (compile-formula *ltms* `(:or ,n1 ,n2))
  (why-nodes *ltms*))

(defun test1 (&optional (complete t))
	(declare (special x y))
  (setq *ltms* (create-ltms "TEST1" :complete complete)
	x (tms-create-node *ltms* "x")
	y (tms-create-node *ltms* "y"))
  (add-formula *ltms* `(:or ,x ,y))
  (add-formula *ltms* `(:or ,x (:not ,y)))
  (complete-ltms *ltms*)
  (unless (true-node? x)
    (error "TEST1 failed")))

(defun test-bug ()
	(declare (special x y z))
  (setq *ltms* (create-ltms "BUG check"))
  (setq x (tms-create-node *ltms* "x" :assumptionp t)
	y (tms-create-node *ltms* "y" :assumptionp t)
	z (tms-create-node *ltms* "z"))
  (compile-formula *ltms* `(:or ,x ,z))
  (compile-formula *ltms* `(:or ,y ,z))
  (enable-assumption x :false)
  (enable-assumption y :false)
  (why-nodes *ltms*)
  (retract-assumption x)
  ;; The original LTMS used to not label z!?!?!?!
  (why-nodes *ltms*))

(defun test-bug1 (&optional (complete t))
	(declare (special x y z))
  (setq *ltms* (create-ltms "BUG check" :complete complete))
  (setq x (tms-create-node *ltms* "x" :assumptionp t)
	y (tms-create-node *ltms* "y" :assumptionp t)
	z (tms-create-node *ltms* "z"))
  (compile-formula *ltms* `(:or ,x ,z))
  (compile-formula *ltms* `(:or ,y ,z))
  (enable-assumption x :false)
  (enable-assumption y :false)
  (why-nodes *ltms*)
  (retract-assumption x)
  ;; The original LTMS used to not label z!?!?!?!
  (why-nodes *ltms*))

(defun test-tax (n &optional (complete t) &aux nodes)
  (setq *ltms* (create-ltms "taxing" :complete complete))
  (dotimes (i n) (push (tms-create-node *ltms* i) nodes))
  (add-formula *ltms* `(:taxonomy ,@nodes))
  (format t "~% ~D prime implicates" (ltms-clause-counter *ltms*)))

(defun test-tax1 (n &aux nodes)
  (setq *ltms* (create-ltms "taxing"))
  (dotimes (i n) (push (tms-create-node *ltms* i) nodes))
  (add-formula *ltms* `(:taxonomy ,@nodes))
  (format t "~% ~D prime implicates" (ltms-clause-counter *ltms*)))

(defun test-e (&optional (complete t))
	(declare (special a b c d e))
  (setq *ltms* (create-ltms "example" :complete complete :debugging t)	
	a (tms-create-node *ltms* "a" :assumptionp t)
	b (tms-create-node *ltms* "b" :assumptionp t)
	c (tms-create-node *ltms* "c" :assumptionp t)	
	d (tms-create-node *ltms* "d" :assumptionp t)
	e (tms-create-node *ltms* "e" :assumptionp t))
  (compile-formula *ltms* `(:or (:not ,a) ,b))
  (compile-formula *ltms* `(:or (:not ,c) ,d))
  (compile-formula *ltms* `(:or (:not ,c) ,e))
  (compile-formula *ltms* `(:or (:not ,b) (:not ,d) (:not ,e))))

(defun test-remove ()
	(declare (special a b c))
  (setq *ltms* (create-ltms "Delay" :complete t :debugging t)
	a (tms-create-node *ltms* "a" :assumptionp t)
	b (tms-create-node *ltms* "b" :assumptionp t)
	c (tms-create-node *ltms* "c" :assumptionp t))
  (compile-formula *ltms* `(:or ,a ,b ,c))
  (enable-assumption a :false)
  (enable-assumption b :false)
  (why-nodes *ltms*)
  (compile-formula *ltms* `(:or ,a ,b))
  (why-nodes *ltms*))

(defun test-delay ()
	(declare (special a b c))
  (setq *ltms* (create-ltms "Delay" :complete t :debugging t)
	a (tms-create-node *ltms* "a" :assumptionp t)
	b (tms-create-node *ltms* "b" :assumptionp t)
	c (tms-create-node *ltms* "c" :assumptionp t))
  (enable-assumption a :false)
  (enable-assumption b :false)

  (compile-formula *ltms* `(:or ,a (:not ,b)))
  (compile-formula *ltms* `(:or ,b ,c))
  (pretty-print-clauses *ltms*)

  (why-nodes *ltms*)
  (retract-assumption b)
  (pretty-print-clauses *ltms*)
  (why-nodes *ltms*))


(defun qop (op x y)
  (case op
    (+ (case x
	 (+ (if (or (eq y '+) (eq y '0)) '+))
	 (0 y)
	 (- (if (or (eq y '-) (eq y '0)) '-))))
    (- (case x
	 (+ (if (or (eq y '-) (eq y '0)) '+))
	 (0 (case y (0 '0) (- '+) (+ '-)))
	 (- (if (or (eq y '+) (eq y '0)) '-))))))


(defun confluence (confluence) (confluence1 (car confluence) 0 nil (cdr confluence)))

(defun confluence1 (variables base support rhs &aux op name qvar result)
  (cond ((null variables)
	 (unless (or (equal base rhs) (if (listp rhs) (member base rhs)))
	   (add-clause nil support '(CONFLUENCE))))
	(t (cond ((atom (car variables)) (setq op '+ name (car variables)))
		 (t (setq op (caar variables)) (setq name (cdar variables))))
	   (setq qvar (lookup-qvar name))
	   (dolist (value (cdr qvar))
	     (setq result (qop op base (cdr (tms-node-datum value))))
	     (if result (confluence1 (cdr variables) result (cons value support) rhs))))))

(defvar *qvars* nil)

(defun find-ltre-class (name) 
  (dolist (qvar *qvars*) (if (eq name (car qvar)) (return qvar))))

(defun lookup-qnode (name value)
  (dolist (symbol (cdr (find-ltre-class name)))
    (if (eq value (cdr (tms-node-datum symbol))) (return symbol))))

(defun lookup-qvar (name &aux qvar symbol symbols)
  (setq qvar (find-ltre-class name))
  (if qvar (return-from lookup-qvar qvar))
  (dolist (value '(- 0 +))
    (setq symbol (tms-create-node *ltms* (cons name value) :assumptionp t))
    (push symbol symbols))
  (add-formula *ltms* `(:taxonomy ,@symbols) '(QVAR DEFINITION))
  (setq qvar (cons name symbols))
  (push qvar *qvars*)
  qvar)

(defun encode-confluences (confluences)
  (dolist (confluence confluences) (confluence confluence)))

(proclaim (special *qvars*))

(defun qp (confluences)
  (setq *ltms* (create-ltms "QP" :complete :DELAY)
	*qvars* nil)
  (encode-confluences confluences)
  (format t "~% Performing resolutions on ~D clauses" (length (collect *ltms*)))
  (pretty-print-clauses *ltms*)
  (time (complete-ltms *ltms*))
;  (pretty-print-clauses *ltms*)
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  )

(defun easy ()
  (qp `(((dpa (- . dpb) (- . dqab)) . 0))))

(defun two ()
  (qp `(((dpa (- . dpb) (- . dqab)) . 0)
	((dpb (- . dpc) (- .dqbc)) . 0)
	((dqab (- . dqbc)) . 0))))

(defun old-twos ()
  (qp `(((dpa (- . dpb) (- . dqab)) . 0)
	((dpb (- . dpc) (- . x)) . 0)
	((dqab (- . dqbc)) . 0)
	)))

(defun twos ()
  (qp `(((dpa (- . dpb) (- . dqab)) . 0)
	((dpb (- . dpc) (- . dqbc)) . 0)
	((dqab (- . dqbc)) . 0)
	)))

(defun two-pipes ()
  (setq *ltms* (create-ltms "QP" :complete :DELAY)
	*qvars* nil)
  (encode-confluences `(((dpa (- . dpb) (- . dqab)) . 0)	; Model of pipe ab
			((dpb (- . dpc) (- . dqbc)) . 0)	; Model of pipe bc
			((dqab (- . dqbc)) . 0)	                ; Flows are equal.
 			))
  (format t "~% Initially there are ~D clauses" (length (collect *ltms*)))
  (enable-assumption (lookup-qnode 'dpc 0) :true)	; Right end is held down.
  (enable-assumption (lookup-qnode 'dpa '+) :true)      ; Left end is rising.
  (pretty-print-clauses *ltms*)
  (time (complete-ltms *ltms*))
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  (explain-node (lookup-qnode 'dpb '+)))
  

(defun twos1 ()
  (setq *ltms* (create-ltms "QP" :complete :DELAY)
	*qvars* nil)
  (encode-confluences `(((dpa (- . dpb) (- . dqab)) . 0)
			((dpb (- . dpc) (- . dqbc)) . 0)
			((dqab (- . dqbc)) . 0)
			))

  (enable-assumption (lookup-qnode 'dpa '+) :true)
  (time (complete-ltms *ltms*))
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  (retract-assumption (lookup-qnode 'dpa '+))
  (print (ltms-queue *ltms*))
  (dirty-clauses? *ltms*)
  (time (complete-ltms *ltms*))
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  (unless (= 638. (length (collect *ltms*))) (error "Can't happen"))


  (format t "~% There should now be no dirty clauses")
  (dirty-clauses? *ltms*)

  ;;; Just repeat for safety.
  (time (complete-ltms *ltms*))
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  (format t "~% There should now be no dirty clauses")
  (dirty-clauses? *ltms*)
  (print (ltms-queue *ltms*))
  (enable-assumption (lookup-qnode 'dpa '+) :true)
  (print (ltms-queue *ltms*))
  (dirty-clauses? *ltms*)
  (time (complete-ltms *ltms*))
  (dirty-clauses? *ltms*)
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  (retract-assumption (lookup-qnode 'dpa '+))
  (dirty-clauses? *ltms*)
  (time (complete-ltms *ltms*))
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  )

(defun dirty-clauses? (ltms &aux (count 0))
  (walk-clauses #'(lambda (cl) (if (clause-dirty cl) (incf count)))
	     (ltms-clauses ltms))
  (format t "~% There are now ~D dirty clauses." count))

(defun ex1 ()
  (qp '(((x y) . 0))))

(defun ex2 ()
  (qp '(((x y) . 0)
	(((- . x) z) . 0))))

;;; Pressure regulator
(defun ex3 ()
  (qp '(
	((p1 (- . p2) (- . q)) . 0)
	((p2 (- . p3) (- . q) a) . 0)
	((p3 (- . p4) (- . q)) . 0)
	((p4 (- . p5) (- . q)) . 0)
	((p4 a) . 0))))

(defun ex4 ()
  (qp `((((- . a) (- . p1) (- . p5)) . 0))))


(defun test-and ()
  (setq *ltms* (create-ltms "LTMS")
	ok (tms-create-node *ltms* "ok" :assumptionp t)
	z (tms-create-node *ltms* "z" :assumptionp t)
	x (tms-create-node *ltms* "x" :assumptionp t)
	y (tms-create-node *ltms* "y" :assumptionp t))
  (add-formula *ltms* `(:implies ,ok (:iff ,z (:and ,x ,y))))
  (pretty-print-clauses *ltms*))

(defun test-andc ()
  (setq *ltms* (create-ltms "LTMS" :complete t)
	ok (tms-create-node *ltms* "ok" :assumptionp t)
	z (tms-create-node *ltms* "z" :assumptionp t)
	x (tms-create-node *ltms* "x" :assumptionp t)
	y (tms-create-node *ltms* "y" :assumptionp t))
  (add-formula *ltms* `(:implies ,ok (:iff ,z (:and ,x ,y))))
  (pretty-print-clauses *ltms*))

(defun test-and1 ()
  (setq *ltms* (create-ltms "LTMS")
	ok (tms-create-node *ltms* "ok" :assumptionp t)
	z=1 (tms-create-node *ltms* "z=1" :assumptionp t)
	z=0 (tms-create-node *ltms* "z=0" :assumptionp t)
	x=1 (tms-create-node *ltms* "x=1" :assumptionp t)
	x=0 (tms-create-node *ltms* "x=0" :assumptionp t)
	y=1 (tms-create-node *ltms* "y=1" :assumptionp t)
	y=0 (tms-create-node *ltms* "y=0" :assumptionp t)
	)
  (add-formula *ltms* `(:taxonomy ,z=1 ,z=0))
  (add-formula *ltms* `(:taxonomy ,x=1 ,x=0))
  (add-formula *ltms* `(:taxonomy ,y=1 ,y=0))
  
;  (add-formula *ltms* `(:implies ,ok (:iff ,z=1 (:and ,x=1 ,y=1))))
  (add-formula *ltms* `(:iff ,z=1 (:and ,x=1 ,y=1)))

  (pretty-print-clauses *ltms*))

(defun test-and1c ()
  (setq *ltms* (create-ltms "LTMS" :complete t)
	ok (tms-create-node *ltms* "ok" :assumptionp t)
	z=1 (tms-create-node *ltms* "z=1" :assumptionp t)
	z=0 (tms-create-node *ltms* "z=0" :assumptionp t)
	x=1 (tms-create-node *ltms* "x=1" :assumptionp t)
	x=0 (tms-create-node *ltms* "x=0" :assumptionp t)
	y=1 (tms-create-node *ltms* "y=1" :assumptionp t)
	y=0 (tms-create-node *ltms* "y=0" :assumptionp t)
	)
  (add-formula *ltms* `(:taxonomy ,z=1 ,z=0))
  (add-formula *ltms* `(:taxonomy ,x=1 ,x=0))
  (add-formula *ltms* `(:taxonomy ,y=1 ,y=0))
  
;  (add-formula *ltms* `(:implies ,ok (:iff ,z=1 (:and ,x=1 ,y=1))))
  (add-formula *ltms* `(:iff ,z=1 (:and ,x=1 ,y=1)))
  (pretty-print-clauses *ltms*))

(defun test-xor (complete)
  (setq *ltms* (create-ltms "LTMS" :complete complete)
	ok (tms-create-node *ltms* "ok" :assumptionp t)
	z=1 (tms-create-node *ltms* "z=1" :assumptionp t)
	z=0 (tms-create-node *ltms* "z=0" :assumptionp t)
	x=1 (tms-create-node *ltms* "x=1" :assumptionp t)
	x=0 (tms-create-node *ltms* "x=0" :assumptionp t)
	y=1 (tms-create-node *ltms* "y=1" :assumptionp t)
	y=0 (tms-create-node *ltms* "y=0" :assumptionp t)
	)
  (add-formula *ltms* `(:taxonomy ,z=1 ,z=0))
  (add-formula *ltms* `(:taxonomy ,x=1 ,x=0))
  (add-formula *ltms* `(:taxonomy ,y=1 ,y=0))
  
;  (add-formula *ltms* `(:implies ,ok (:iff ,z=1 (:and ,x=1 ,y=1))))
;  (add-formula *ltms* `(:iff ,z=1 (:taxonomy ,x=1 ,y=1)))


  (pretty-print-clauses *ltms*))

(defun build-xor (complete)
  (setq *ltms* (create-ltms "LTMS" :complete complete)
	x (tms-create-node *ltms* "x" :assumptionp t)
	y (tms-create-node *ltms* "y" :assumptionp t)
	z (tms-create-node *ltms* "z" :assumptionp t)
	a (tms-create-node *ltms* "a" :assumptionp t)
	b (tms-create-node *ltms* "b" :assumptionp t)
	c (tms-create-node *ltms* "c" :assumptionp t))
  (install-nand x y a)
  (install-nand x a b)
  (install-nand b c z)
  (install-nand a y c)
  (pretty-print-clauses *ltms*))

(defun install-nand (i1 i2 o)
  (add-formula *ltms* `(:iff (:not ,o) (:and ,i1 ,i2))))

(defun history-ex (&aux db)
  (setq *ltms* (create-ltms "History Example" :complete :delay))
  (setq db '((:or (:not x1) x4 a p1)    
	     (:or (:not x1) x4 a p2)    
	     (:or (:not x1) x4 a p3)    
	     (:or (:not x1) x4 a p4)    
	     (:or (:not x1) x4 a p5)    
	     (:or (:not x2) a c)         
	     (:or (:not x3) b1)           
	     (:or (:not x3) b2)           
	     (:or (:not x3) b3)           
	     (:or (:not x3) b4)           
	     (:or (:not x3) b5)           
	     (:or (:not x4) x1 a1)       
	     (:or (:not x4) x1 a2)       
	     (:or (:not x4) x1 a3)       
	     (:or (:not x4) x1 a4)       
	     (:or (:not x4) x1 a5)))
  (dolist (f db)
    (add-formula *ltms* f))
  (complete-ltms *ltms*)
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  (print subsumed)
  (add-formula *ltms* '(:or x1 x2 x3 x4))
  (complete-ltms *ltms*)
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  (print subsumed)
  )

(defun kean-adder ()
  (setq *ltms* (create-ltms "Kean Adder" :complete :delay))
  (setq db
        `((:or (:not k=0) (:not l=0) (:not n=0) (:not ab(x1)) )
	  (:or (:not n=0) (:not m=0) (:not r=0) (:not ab(x2)) )
	  (:or (:not k=0) (:not l=1) (:not n=1) (:not ab(x1)) )
	  (:or (:not n=0) (:not m=1) (:not r=1) (:not ab(x2)) )
	  (:or (:not k=1) (:not l=0) (:not n=1) (:not ab(x1)) )
	  (:or (:not n=1) (:not m=0) (:not r=1) (:not ab(x2)) )
	  (:or (:not k=1) (:not l=1) (:not n=0) (:not ab(x1)) )
	  (:or (:not n=1) (:not m=1) (:not r=0) (:not ab(x2)) )
	  (:or (:not k=1) (:not l=1) (:not q=1) (:not ab(a1)) )
	  (:or (:not m=1) (:not n=1) (:not p=1) (:not ab(a2)) )
	  (:or (:not k=0) (:not q=0) (:not ab(a1)) )
	  (:or (:not m=0) (:not p=0) (:not ab(a2)) )
	  (:or (:not l=0) (:not q=0) (:not ab(a1)) )
	  (:or (:not n=0) (:not p=0) (:not ab(a2)) )
	  (:or (:not p=0) (:not q=0) (:not s=0) (:not ab(o1)) )
	  (:or (:not p=1) (:not s=1) (:not ab(o1)) )
	  (:or (:not q=1) (:not s=1) (:not ab(o1)) )
	  (:or (:not k=0) (:not l=0) (:not n=1) ab(x1) )
	  (:or (:not n=0) (:not m=0) (:not r=1) ab(x2) )
	  (:or (:not k=0) (:not l=1) (:not n=0) ab(x1) )
	  (:or (:not n=0) (:not m=1) (:not r=0) ab(x2) )
	  (:or (:not k=1) (:not l=0) (:not n=0) ab(x1) )
	  (:or (:not n=1) (:not m=0) (:not r=0) ab(x2) )
	  (:or (:not k=1) (:not l=1) (:not n=1) ab(x1) )
	  (:or (:not n=1) (:not m=1) (:not r=1) ab(x2) )
	  (:or (:not k=1) (:not l=1) (:not q=0) ab(a1) )
	  (:or (:not m=1) (:not n=1) (:not p=0) ab(a2) )
	  (:or (:not k=0) (:not q=1) ab(a1) )
	  (:or (:not m=0) (:not p=1) ab(a2) )
	  (:or (:not l=0) (:not q=1) ab(a1) )
	  (:or (:not n=0) (:not p=1) ab(a2) )
	  (:or (:not p=0) (:not q=0) (:not s=1) ab(o1) )
	  (:or (:not p=1) (:not s=0) ab(o1) )
	  (:or (:not q=1) (:not s=0) ab(o1) )
	  (:or (:not k=0) (:not k=1) )
	  (:or k=0 k=1 )
	  (:or (:not l=0) (:not l=1) )
	  (:or l=0 l=1 )
	  (:or (:not m=0) (:not m=1) )
	  (:or m=0 m=1 )
	  (:or (:not n=0) (:not n=1) )
	  (:or n=0 n=1 )
	  (:or (:not p=0) (:not p=1) )
	  (:or p=0 p=1 )
	  (:or (:not q=0) (:not q=1) )
	  (:or q=0 q=1 )
	  (:or (:not r=0) (:not r=1) )
	  (:or r=0 r=1 )
	  (:or (:not s=0) (:not s=1) )
	  (:or s=0 s=1 )))
  (dolist (f db)
    (add-formula *ltms* f))
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  (time (complete-ltms *ltms*))
  (format t "~% There now are ~D clauses" (length (collect *ltms*))))

(defun selenoid ()
  (setq *ltms* (create-ltms "Selenoid" :complete :delay))
  (add-formula *ltms* '(:taxonomy (= ?a ok) (= ?a stuck_out) (= ?a stuck_in)))
  (add-formula *ltms* '(:taxonomy (= ?b dc_com) (= ?b v24dc) (= ?b float)))
  (add-formula *ltms* '(:taxonomy (= ?c v24dc) (= ?c dc_com) (= ?c float)))
  (add-formula *ltms* '(:taxonomy (= ?d in) (= ?d out)))

  
  (add-formula *ltms* '(:or
		   (:and (= ?a ok) (= ?b dc_com) (= ?c v24dc) (= ?d in) )
		   (:and (= ?a ok) (= ?b dc_com) (= ?c dc_com) (= ?d out) )
		   (:and (= ?a ok) (= ?b dc_com) (= ?c float) (= ?d out) )
		   (:and (= ?a ok) (= ?b v24dc) (= ?c v24dc) (= ?d out) )
		   (:and (= ?a ok) (= ?b v24dc) (= ?c dc_com) (= ?d out) )
		   (:and (= ?a ok) (= ?b v24dc) (= ?c float) (= ?d out) )
		   (:and (= ?a ok) (= ?b float) (= ?c v24dc) (= ?d out) )
		   (:and (= ?a ok) (= ?b float) (= ?c dc_com) (= ?d out) )
		   (:and (= ?a ok) (= ?b float) (= ?c float) (= ?d out) )
		   (:and (= ?a stuck_out) (= ?d out) )
		   (:and (= ?a stuck_in) (= ?d in) )
		   ))
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  (time (complete-ltms *ltms*))
  (format t "~% There now are ~D clauses" (length (collect *ltms*))))

(defun valve ()
  (setq *ltms* (create-ltms "Valve" :complete :delay))
  (add-formula *ltms* '(:and
		  (:taxonomy (= ?a ok) (= ?a stuck_open) (= ?a stuck_closed))
		  (:taxonomy (= ?b in) (= ?b out))
		  (:taxonomy (= ?c low) (= ?c normal) (= ?c high) (= ?c none))
		  (:taxonomy (= ?d none) (= ?d low) (= ?d normal) (= ?d high))
		  (:or
		    (:and (= ?a ok) (= ?b in) (= ?c low) (= ?d low) )
		    (:and (= ?a ok) (= ?b in) (= ?c normal) (= ?d normal) )
		    (:and (= ?a ok) (= ?b in) (= ?c high) (= ?d high) )
		    (:and (= ?a ok) (= ?b out) (= ?c low) (= ?d low) )
		    (:and (= ?a ok) (= ?b out) (= ?c normal) (= ?d low) )
		    (:and (= ?a ok) (= ?b out) (= ?c high) (= ?d low) )
		    (:and (= ?c none) (= ?d none) )
		    (:and (= ?a stuck_open) (= ?c low) (= ?d low) )
		    (:and (= ?a stuck_open) (= ?c normal) (= ?d normal) )
		    (:and (= ?a stuck_open) (= ?c high) (= ?d high) )
		    (:and (= ?a stuck_closed) (= ?c low) (= ?d low) )
		    (:and (= ?a stuck_closed) (= ?c normal) (= ?d low) )
		    (:and (= ?a stuck_closed) (= ?c high) (= ?d low) )
		    )))
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  (pretty-print-clauses *ltms*)
  (time (complete-ltms *ltms*))
  (format t "~% There now are ~D clauses" (length (collect *ltms*))))

(defun print-horn-clauses ()
  (walk-clauses *ltms*
		#'(lambda (l)
		    (when (definite? l)
		      (format t "~% ")
		      (pretty-string-clause l)))))

(defun print-new-rules ()
  (walk-clauses *ltms*
		#'(lambda (l)
		 (when (and (horn? l)
			    (not (member (car (clause-informant l)) '(:implied-by ))))
		   (format t "~% ")
		   (pretty-string-rule l)))))

(defun pretty-string-rule (clause &aux pos)
  (dolist (lit (clause-literals clause))
    (if (eq (cdr lit) :false)
	(format t "~A " (node-string (car lit)))
	(setq pos (car lit))))
  (format t "==>> ~A" (if pos (node-string pos) "CONTRADICTION")))

(defun horn? (cl &aux pos)
  (dolist (lit (clause-literals cl) t)
    (cond ((eq (cdr lit) :false))
	  (pos (return nil))
	  (t (setq pos t)))))

(defun keanp (m k &aux as)
  (setq *ltms* (create-ltms "Kean Problem" :complete :delay :delay-sat t))
  (setq as (kean-setup m k))
;  (complete-ltms *ltms*)
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  (add-formula *ltms* as)
  (pretty-print-clauses *ltms*)
  (time (complete-ltms *ltms*))
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  )

(defun kean-setup (m k &aux as)
  (do ((i 1 (1+ i)))
      ((> i k) (cons :or as))
    (push `(:not (a ,i)) as)
    (do ((j 1 (1+ j)))
	((> j m))
      (add-formula *ltms* `(:or (a ,i) (:not (s ,i ,j)))))))

(defun teow (n &aux f1 f2)
  (setq *ltms* (create-ltms "Teow Problem" :complete :delay))
  (push `(:and (A 1) (A 2)) f2)
  (do ((i 3 (+ i 2)))
      ((> i n))
    (push `(:implies (A ,i) (A 1)) f1)
    (push `(:implies (A ,(1+ i)) (A 2)) f1)
    (push `(:and (A ,i) (A ,(1+ i))) f2))
  (add-formula *ltms*
	       `(:and ,@(nreverse f1) (:or .,(nreverse f2))))
  ;; Of course this does nothing:
  (time (complete-ltms *ltms*))
  (format t "~% There now are ~D clauses" (length (collect *ltms*)))
  )

(defun teow-bug-1 ()
  (setq *ltms* (create-ltms "Teow bug 1" :complete :delay))
  (add-formula *ltms* `(:and (:or x) (:or (:not x)))))

;;; On 9/11/91 this generated 3241 "PIs"(BCP conditioned) in 676 seconds.  Why did
;;; this take so long?
(defun bond ()
  (setq *ltms* (create-ltms "Bond bug" :complete :delay :delay-sat nil)
	x 
	'((:or k) (:or (:not l)) (:or m) (:or (:not r)) (:or s) (:or k  l  (:not n)  ek  el  en) (:or k  n  (:not l)  ek  el  en)
    (:or l  n  (:not k)  ek  el  en) (:or (:not n)  (:not l)  (:not k)  ek  el  en)
    (:or (:not k)  (:not l)  n  (:not ek)  en) (:or (:not k)  l  (:not n)  (:not ek)  en)
    (:or k  (:not l)  (:not n)  (:not ek)  en) (:or k  l  n  (:not ek)  en)
    (:or (:not k)  (:not l)  n  (:not el)  en) (:or (:not k)  l  (:not n)  (:not el)  en)
    (:or k  (:not l)  (:not n)  (:not el)  en) (:or k  l  n  (:not el)  en) (:or (:not k)  (:not l)  n  (:not exa))
    (:or (:not k)  l  (:not n)  (:not exa)) (:or k  (:not l)  (:not n)  (:not exa)) (:or k  l  n  (:not exa))
    (:or k  l  (:not n)  exa) (:or k  n  (:not l)  exa) (:or l  n  (:not k)  exa)
    (:or (:not n)  (:not l)  (:not k)  exa) (:or (:not k)  (:not l)  n  (:not en)  ek  el  ma)
    (:or (:not k)  l  (:not n)  (:not en)  ek  el  ma) (:or k  (:not l)  (:not n)  (:not en)  ek  el  ma)
    (:or k  l  n  (:not en)  ek  el  ma) (:or k  l  (:not n)  (:not ma)) (:or k  n  (:not l)  (:not ma))
    (:or l  n  (:not k)  (:not ma)) (:or (:not n)  (:not l)  (:not k)  (:not ma)) (:or en  (:not ma)) (:or (:not ek)  (:not ma))
    (:or (:not el)  (:not ma)) (:or n  m  (:not r)  en  em  er) (:or n  r  (:not m)  en  em  er)
    (:or m  r  (:not n)  en  em  er) (:or (:not r)  (:not m)  (:not n)  en  em  er)
    (:or (:not n)  (:not m)  r  (:not en)  er) (:or (:not n)  m  (:not r)  (:not en)  er) (:or n  (:not m)  (:not r)  (:not en)  er)
    (:or n  m  r  (:not en)  er) (:or (:not n)  (:not m)  r  (:not em)  er) (:or (:not n)  m  (:not r)  (:not em)  er)
    (:or n  (:not m)  (:not r)  (:not em)  er) (:or n  m  r  (:not em)  er) (:or (:not n)  (:not m)  r  (:not exb))
    (:or (:not n)  m  (:not r)  (:not exb)) (:or n  (:not m)  (:not r)  (:not exb)) (:or n  m  r  (:not exb))
    (:or n  m  (:not r)  exb) (:or n  r  (:not m)  exb) (:or m  r  (:not n)  exb)
    (:or (:not r)  (:not m)  (:not n)  exb) (:or (:not n)  (:not m)  r  (:not er)  en  em  mb)
    (:or (:not n)  m  (:not r)  (:not er)  en  em  mb) (:or n  (:not m)  (:not r)  (:not er)  en  em  mb)
    (:or n  m  r  (:not er)  en  em  mb) (:or n  m  (:not r)  (:not mb)) (:or n  r  (:not m)  (:not mb))
    (:or m  r  (:not n)  (:not mb)) (:or (:not r)  (:not m)  (:not n)  (:not mb)) (:or er  (:not mb)) (:or (:not en)  (:not mb))
    (:or (:not em)  (:not mb)) (:or k  (:not q)  ek  el  eq) (:or l  (:not q)  ek  el  eq) (:or q  (:not l)  (:not k)  ek  el  eq)
    (:or (:not k)  (:not l)  (:not q)  (:not ek)  eq) (:or (:not k)  l  q  (:not ek)  eq) (:or k  (:not l)  q  (:not ek)  eq)
    (:or k  l  q  (:not ek)  eq) (:or (:not k)  (:not l)  (:not q)  (:not el)  eq) (:or (:not k)  l  q  (:not el)  eq)
    (:or k  (:not l)  q  (:not el)  eq) (:or k  l  q  (:not el)  eq) (:or (:not k)  (:not l)  (:not q)  (:not exc))
    (:or (:not k)  l  q  (:not exc)) (:or k  (:not l)  q  (:not exc)) (:or k  l  q  (:not exc))
    (:or k  (:not q)  exc) (:or l  (:not q)  exc) (:or q  (:not l)  (:not k)  exc)
    (:or (:not k)  (:not l)  (:not q)  (:not eq)  ek  el  mc) (:or (:not k)  l  q  (:not eq)  ek  el  mc)
    (:or k  (:not l)  q  (:not eq)  ek  el  mc)  (:or k  l  q  (:not eq)  ek  el  mc)
    (:or k  (:not q)  (:not mc)) (:or l  (:not q)  (:not mc)) (:or q  (:not l)  (:not k)  (:not mc)) (:or eq  (:not mc))
    (:or (:not ek)  (:not mc)) (:or (:not el)  (:not mc)) (:or m  (:not p)  em  en  ep) (:or n  (:not p)  em  en  ep)
    (:or p  (:not n)  (:not m)  em  en  ep) (:or (:not m)  (:not n)  (:not p)  (:not em)  ep) (:or (:not m)  n  p  (:not em)  ep)
    (:or m  (:not n)  p  (:not em)  ep) (:or m  n  p  (:not em)  ep) (:or (:not m)  (:not n)  (:not p)  (:not en)  ep)
    (:or (:not m)  n  p  (:not en)  ep) (:or m  (:not n)  p  (:not en)  ep) (:or m  n  p  (:not en)  ep)
    (:or (:not m)  (:not n)  (:not p)  (:not exd)) (:or (:not m)  n  p  (:not exd)) (:or m  (:not n)  p  (:not exd))
    (:or m  n  p  (:not exd)) (:or m  (:not p)  exd) (:or n  (:not p)  exd)
    (:or p  (:not n)  (:not m)  exd) (:or (:not m)  (:not n)  (:not p)  (:not ep)  em  en  md)
    (:or (:not m)  n  p  (:not ep)  em  en  md) (:or m  (:not n)  p  (:not ep)  em  en  md)
    (:or m  n  p  (:not ep)  em  en  md) (:or m  (:not p)  (:not md)) (:or n  (:not p)  (:not md))
    (:or p  (:not n)  (:not m)  (:not md)) (:or ep  (:not md)) (:or (:not em)  (:not md)) (:or (:not en)  (:not md))
    (:or p  q  (:not s)  ep  eq  es) (:or s  (:not p)  ep  eq  es) (:or s  (:not q)  ep  eq  es)
    (:or (:not p)  (:not q)  (:not s)  (:not ep)  es) (:or (:not p)  q  (:not s)  (:not ep)  es) (:or p  (:not q)  (:not s)  (:not ep)  es)
    (:or p  q  s  (:not ep)  es) (:or (:not p)  (:not q)  (:not s)  (:not eq)  es) (:or (:not p)  q  (:not s)  (:not eq)  es)
    (:or p  (:not q)  (:not s)  (:not eq)  es) (:or p  q  s  (:not eq)  es) (:or (:not p)  (:not q)  (:not s)  (:not exf))
    (:or (:not p)  q  (:not s)  (:not exf)) (:or p  (:not q)  (:not s)  (:not exf)) (:or p  q  s  (:not exf)) (:or p  q  (:not s)  exf)
    (:or s  (:not p)  exf) (:or s  (:not q)  exf) (:or (:not p)  (:not q)  (:not s)  (:not es)  ep  eq  mf)
    (:or (:not p)  q  (:not s)  (:not es)  ep  eq  mf) (:or p  (:not q)  (:not s)  (:not es)  ep  eq  mf)
    (:or p  q  s  (:not es)  ep  eq  mf) (:or p  q  (:not s) (:not mf)) (:or s  (:not p)  (:not mf)) (:or s  (:not q)  (:not mf))
    (:or es  (:not mf)) (:or (:not ep)  (:not mf)) (:or (:not eq)  (:not mf))))

  (dolist (c x) (add-formula *ltms* c))

  (time (complete-ltms *ltms*))
  (format t "~% There now are ~D clauses" (length (collect *ltms*))))

;;; On 9/11/91 this generated 3241 PIs in 218 seconds.
(defun bond-1 ()
  (setq *ltms* (create-ltms "Bond bug" :complete :delay :delay-sat nil)
	x 
	'((:or k) (:or (:not l)) (:or m) (:or (:not r)) (:or s) (:or k  l  (:not n)  ek  el  en) (:or k  n  (:not l)  ek  el  en)
    (:or l  n  (:not k)  ek  el  en) (:or (:not n)  (:not l)  (:not k)  ek  el  en)
    (:or (:not k)  (:not l)  n  (:not ek)  en) (:or (:not k)  l  (:not n)  (:not ek)  en)
    (:or k  (:not l)  (:not n)  (:not ek)  en) (:or k  l  n  (:not ek)  en)
    (:or (:not k)  (:not l)  n  (:not el)  en) (:or (:not k)  l  (:not n)  (:not el)  en)
    (:or k  (:not l)  (:not n)  (:not el)  en) (:or k  l  n  (:not el)  en) (:or (:not k)  (:not l)  n  (:not exa))
    (:or (:not k)  l  (:not n)  (:not exa)) (:or k  (:not l)  (:not n)  (:not exa)) (:or k  l  n  (:not exa))
    (:or k  l  (:not n)  exa) (:or k  n  (:not l)  exa) (:or l  n  (:not k)  exa)
    (:or (:not n)  (:not l)  (:not k)  exa) (:or (:not k)  (:not l)  n  (:not en)  ek  el  ma)
    (:or (:not k)  l  (:not n)  (:not en)  ek  el  ma) (:or k  (:not l)  (:not n)  (:not en)  ek  el  ma)
    (:or k  l  n  (:not en)  ek  el  ma) (:or k  l  (:not n)  (:not ma)) (:or k  n  (:not l)  (:not ma))
    (:or l  n  (:not k)  (:not ma)) (:or (:not n)  (:not l)  (:not k)  (:not ma)) (:or en  (:not ma)) (:or (:not ek)  (:not ma))
    (:or (:not el)  (:not ma)) (:or n  m  (:not r)  en  em  er) (:or n  r  (:not m)  en  em  er)
    (:or m  r  (:not n)  en  em  er) (:or (:not r)  (:not m)  (:not n)  en  em  er)
    (:or (:not n)  (:not m)  r  (:not en)  er) (:or (:not n)  m  (:not r)  (:not en)  er) (:or n  (:not m)  (:not r)  (:not en)  er)
    (:or n  m  r  (:not en)  er) (:or (:not n)  (:not m)  r  (:not em)  er) (:or (:not n)  m  (:not r)  (:not em)  er)
    (:or n  (:not m)  (:not r)  (:not em)  er) (:or n  m  r  (:not em)  er) (:or (:not n)  (:not m)  r  (:not exb))
    (:or (:not n)  m  (:not r)  (:not exb)) (:or n  (:not m)  (:not r)  (:not exb)) (:or n  m  r  (:not exb))
    (:or n  m  (:not r)  exb) (:or n  r  (:not m)  exb) (:or m  r  (:not n)  exb)
    (:or (:not r)  (:not m)  (:not n)  exb) (:or (:not n)  (:not m)  r  (:not er)  en  em  mb)
    (:or (:not n)  m  (:not r)  (:not er)  en  em  mb) (:or n  (:not m)  (:not r)  (:not er)  en  em  mb)
    (:or n  m  r  (:not er)  en  em  mb) (:or n  m  (:not r)  (:not mb)) (:or n  r  (:not m)  (:not mb))
    (:or m  r  (:not n)  (:not mb)) (:or (:not r)  (:not m)  (:not n)  (:not mb)) (:or er  (:not mb)) (:or (:not en)  (:not mb))
    (:or (:not em)  (:not mb)) (:or k  (:not q)  ek  el  eq) (:or l  (:not q)  ek  el  eq) (:or q  (:not l)  (:not k)  ek  el  eq)
    (:or (:not k)  (:not l)  (:not q)  (:not ek)  eq) (:or (:not k)  l  q  (:not ek)  eq) (:or k  (:not l)  q  (:not ek)  eq)
    (:or k  l  q  (:not ek)  eq) (:or (:not k)  (:not l)  (:not q)  (:not el)  eq) (:or (:not k)  l  q  (:not el)  eq)
    (:or k  (:not l)  q  (:not el)  eq) (:or k  l  q  (:not el)  eq) (:or (:not k)  (:not l)  (:not q)  (:not exc))
    (:or (:not k)  l  q  (:not exc)) (:or k  (:not l)  q  (:not exc)) (:or k  l  q  (:not exc))
    (:or k  (:not q)  exc) (:or l  (:not q)  exc) (:or q  (:not l)  (:not k)  exc)
    (:or (:not k)  (:not l)  (:not q)  (:not eq)  ek  el  mc) (:or (:not k)  l  q  (:not eq)  ek  el  mc)
    (:or k  (:not l)  q  (:not eq)  ek  el  mc)  (:or k  l  q  (:not eq)  ek  el  mc)
    (:or k  (:not q)  (:not mc)) (:or l  (:not q)  (:not mc)) (:or q  (:not l)  (:not k)  (:not mc)) (:or eq  (:not mc))
    (:or (:not ek)  (:not mc)) (:or (:not el)  (:not mc)) (:or m  (:not p)  em  en  ep) (:or n  (:not p)  em  en  ep)
    (:or p  (:not n)  (:not m)  em  en  ep) (:or (:not m)  (:not n)  (:not p)  (:not em)  ep) (:or (:not m)  n  p  (:not em)  ep)
    (:or m  (:not n)  p  (:not em)  ep) (:or m  n  p  (:not em)  ep) (:or (:not m)  (:not n)  (:not p)  (:not en)  ep)
    (:or (:not m)  n  p  (:not en)  ep) (:or m  (:not n)  p  (:not en)  ep) (:or m  n  p  (:not en)  ep)
    (:or (:not m)  (:not n)  (:not p)  (:not exd)) (:or (:not m)  n  p  (:not exd)) (:or m  (:not n)  p  (:not exd))
    (:or m  n  p  (:not exd)) (:or m  (:not p)  exd) (:or n  (:not p)  exd)
    (:or p  (:not n)  (:not m)  exd) (:or (:not m)  (:not n)  (:not p)  (:not ep)  em  en  md)
    (:or (:not m)  n  p  (:not ep)  em  en  md) (:or m  (:not n)  p  (:not ep)  em  en  md)
    (:or m  n  p  (:not ep)  em  en  md) (:or m  (:not p)  (:not md)) (:or n  (:not p)  (:not md))
    (:or p  (:not n)  (:not m)  (:not md)) (:or ep  (:not md)) (:or (:not em)  (:not md)) (:or (:not en)  (:not md))
    (:or p  q  (:not s)  ep  eq  es) (:or s  (:not p)  ep  eq  es) (:or s  (:not q)  ep  eq  es)
    (:or (:not p)  (:not q)  (:not s)  (:not ep)  es) (:or (:not p)  q  (:not s)  (:not ep)  es) (:or p  (:not q)  (:not s)  (:not ep)  es)
    (:or p  q  s  (:not ep)  es) (:or (:not p)  (:not q)  (:not s)  (:not eq)  es) (:or (:not p)  q  (:not s)  (:not eq)  es)
    (:or p  (:not q)  (:not s)  (:not eq)  es) (:or p  q  s  (:not eq)  es) (:or (:not p)  (:not q)  (:not s)  (:not exf))
    (:or (:not p)  q  (:not s)  (:not exf)) (:or p  (:not q)  (:not s)  (:not exf)) (:or p  q  s  (:not exf)) (:or p  q  (:not s)  exf)
    (:or s  (:not p)  exf) (:or s  (:not q)  exf) (:or (:not p)  (:not q)  (:not s)  (:not es)  ep  eq  mf)
    (:or (:not p)  q  (:not s)  (:not es)  ep  eq  mf) (:or p  (:not q)  (:not s)  (:not es)  ep  eq  mf)
    (:or p  q  s  (:not es)  ep  eq  mf) (:or p  q  (:not s) (:not mf)) (:or s  (:not p)  (:not mf)) (:or s  (:not q)  (:not mf))
    (:or es  (:not mf)) (:or (:not ep)  (:not mf)) (:or (:not eq)  (:not mf))))

  (add-formula *ltms* `(:and .,x) 'BOND-1)

  (complete-ltms *ltms*)
  (format t "~% There now are ~D clauses" (length (collect *ltms*))))

(defun bond-2 ()
  (pi '(:and (:or k) (:or (:not l)) (:or m) (:or (:not r)) (:or s) (:or k  l  (:not n)  ek  el  en) (:or k  n  (:not l)  ek  el  en)
    (:or l  n  (:not k)  ek  el  en) (:or (:not n)  (:not l)  (:not k)  ek  el  en)
    (:or (:not k)  (:not l)  n  (:not ek)  en) (:or (:not k)  l  (:not n)  (:not ek)  en)
    (:or k  (:not l)  (:not n)  (:not ek)  en) (:or k  l  n  (:not ek)  en)
    (:or (:not k)  (:not l)  n  (:not el)  en) (:or (:not k)  l  (:not n)  (:not el)  en)
    (:or k  (:not l)  (:not n)  (:not el)  en) (:or k  l  n  (:not el)  en) (:or (:not k)  (:not l)  n  (:not exa))
    (:or (:not k)  l  (:not n)  (:not exa)) (:or k  (:not l)  (:not n)  (:not exa)) (:or k  l  n  (:not exa))
    (:or k  l  (:not n)  exa) (:or k  n  (:not l)  exa) (:or l  n  (:not k)  exa)
    (:or (:not n)  (:not l)  (:not k)  exa) (:or (:not k)  (:not l)  n  (:not en)  ek  el  ma)
    (:or (:not k)  l  (:not n)  (:not en)  ek  el  ma) (:or k  (:not l)  (:not n)  (:not en)  ek  el  ma)
    (:or k  l  n  (:not en)  ek  el  ma) (:or k  l  (:not n)  (:not ma)) (:or k  n  (:not l)  (:not ma))
    (:or l  n  (:not k)  (:not ma)) (:or (:not n)  (:not l)  (:not k)  (:not ma)) (:or en  (:not ma)) (:or (:not ek)  (:not ma))
    (:or (:not el)  (:not ma)) (:or n  m  (:not r)  en  em  er) (:or n  r  (:not m)  en  em  er)
    (:or m  r  (:not n)  en  em  er) (:or (:not r)  (:not m)  (:not n)  en  em  er)
    (:or (:not n)  (:not m)  r  (:not en)  er) (:or (:not n)  m  (:not r)  (:not en)  er) (:or n  (:not m)  (:not r)  (:not en)  er)
    (:or n  m  r  (:not en)  er) (:or (:not n)  (:not m)  r  (:not em)  er) (:or (:not n)  m  (:not r)  (:not em)  er)
    (:or n  (:not m)  (:not r)  (:not em)  er) (:or n  m  r  (:not em)  er) (:or (:not n)  (:not m)  r  (:not exb))
    (:or (:not n)  m  (:not r)  (:not exb)) (:or n  (:not m)  (:not r)  (:not exb)) (:or n  m  r  (:not exb))
    (:or n  m  (:not r)  exb) (:or n  r  (:not m)  exb) (:or m  r  (:not n)  exb)
    (:or (:not r)  (:not m)  (:not n)  exb) (:or (:not n)  (:not m)  r  (:not er)  en  em  mb)
    (:or (:not n)  m  (:not r)  (:not er)  en  em  mb) (:or n  (:not m)  (:not r)  (:not er)  en  em  mb)
    (:or n  m  r  (:not er)  en  em  mb) (:or n  m  (:not r)  (:not mb)) (:or n  r  (:not m)  (:not mb))
    (:or m  r  (:not n)  (:not mb)) (:or (:not r)  (:not m)  (:not n)  (:not mb)) (:or er  (:not mb)) (:or (:not en)  (:not mb))
    (:or (:not em)  (:not mb)) (:or k  (:not q)  ek  el  eq) (:or l  (:not q)  ek  el  eq) (:or q  (:not l)  (:not k)  ek  el  eq)
    (:or (:not k)  (:not l)  (:not q)  (:not ek)  eq) (:or (:not k)  l  q  (:not ek)  eq) (:or k  (:not l)  q  (:not ek)  eq)
    (:or k  l  q  (:not ek)  eq) (:or (:not k)  (:not l)  (:not q)  (:not el)  eq) (:or (:not k)  l  q  (:not el)  eq)
    (:or k  (:not l)  q  (:not el)  eq) (:or k  l  q  (:not el)  eq) (:or (:not k)  (:not l)  (:not q)  (:not exc))
    (:or (:not k)  l  q  (:not exc)) (:or k  (:not l)  q  (:not exc)) (:or k  l  q  (:not exc))
    (:or k  (:not q)  exc) (:or l  (:not q)  exc) (:or q  (:not l)  (:not k)  exc)
    (:or (:not k)  (:not l)  (:not q)  (:not eq)  ek  el  mc) (:or (:not k)  l  q  (:not eq)  ek  el  mc)
    (:or k  (:not l)  q  (:not eq)  ek  el  mc)  (:or k  l  q  (:not eq)  ek  el  mc)
    (:or k  (:not q)  (:not mc)) (:or l  (:not q)  (:not mc)) (:or q  (:not l)  (:not k)  (:not mc)) (:or eq  (:not mc))
    (:or (:not ek)  (:not mc)) (:or (:not el)  (:not mc)) (:or m  (:not p)  em  en  ep) (:or n  (:not p)  em  en  ep)
    (:or p  (:not n)  (:not m)  em  en  ep) (:or (:not m)  (:not n)  (:not p)  (:not em)  ep) (:or (:not m)  n  p  (:not em)  ep)
    (:or m  (:not n)  p  (:not em)  ep) (:or m  n  p  (:not em)  ep) (:or (:not m)  (:not n)  (:not p)  (:not en)  ep)
    (:or (:not m)  n  p  (:not en)  ep) (:or m  (:not n)  p  (:not en)  ep) (:or m  n  p  (:not en)  ep)
    (:or (:not m)  (:not n)  (:not p)  (:not exd)) (:or (:not m)  n  p  (:not exd)) (:or m  (:not n)  p  (:not exd))
    (:or m  n  p  (:not exd)) (:or m  (:not p)  exd) (:or n  (:not p)  exd)
    (:or p  (:not n)  (:not m)  exd) (:or (:not m)  (:not n)  (:not p)  (:not ep)  em  en  md)
    (:or (:not m)  n  p  (:not ep)  em  en  md) (:or m  (:not n)  p  (:not ep)  em  en  md)
    (:or m  n  p  (:not ep)  em  en  md) (:or m  (:not p)  (:not md)) (:or n  (:not p)  (:not md))
    (:or p  (:not n)  (:not m)  (:not md)) (:or ep  (:not md)) (:or (:not em)  (:not md)) (:or (:not en)  (:not md))
    (:or p  q  (:not s)  ep  eq  es) (:or s  (:not p)  ep  eq  es) (:or s  (:not q)  ep  eq  es)
    (:or (:not p)  (:not q)  (:not s)  (:not ep)  es) (:or (:not p)  q  (:not s)  (:not ep)  es) (:or p  (:not q)  (:not s)  (:not ep)  es)
    (:or p  q  s  (:not ep)  es) (:or (:not p)  (:not q)  (:not s)  (:not eq)  es) (:or (:not p)  q  (:not s)  (:not eq)  es)
    (:or p  (:not q)  (:not s)  (:not eq)  es) (:or p  q  s  (:not eq)  es) (:or (:not p)  (:not q)  (:not s)  (:not exf))
    (:or (:not p)  q  (:not s)  (:not exf)) (:or p  (:not q)  (:not s)  (:not exf)) (:or p  q  s  (:not exf)) (:or p  q  (:not s)  exf)
    (:or s  (:not p)  exf) (:or s  (:not q)  exf) (:or (:not p)  (:not q)  (:not s)  (:not es)  ep  eq  mf)
    (:or (:not p)  q  (:not s)  (:not es)  ep  eq  mf) (:or p  (:not q)  (:not s)  (:not es)  ep  eq  mf)
    (:or p  q  s  (:not es)  ep  eq  mf) (:or p  q  (:not s) (:not mf)) (:or s  (:not p)  (:not mf)) (:or s  (:not q)  (:not mf))
    (:or es  (:not mf)) (:or (:not ep)  (:not mf)) (:or (:not eq)  (:not mf)))))

(defun check (ltms)
  (walk-clauses ltms
		#'(lambda (cl) (unless (find-tree cl ltms) (error "Can't find ~A" cl)))))

(defun check-tree (tree &aux (last 0))
  (unless (atom tree)
    (dolist (entry tree) (unless (<= last (setq last (tms-node-index (caar entry))))
			   (error "Tree out of order"))
	    (check-tree (cddr entry))
	    )))


;;; Temporary.
(defun find-tree (cl ltms)
  (find-tree-1 (clause-literals cl) (clause-length cl) (ltms-clauses ltms)))

;;;***** length is not sued here.
(defun find-tree-1 (lits length tree)
  (cond ((null lits) (if (atom tree) tree))
	((atom tree) nil)
	(t (dolist (subtree tree)
	     (if (eq (car lits) (car subtree))
		 (return (find-tree-1 (cdr lits) length (cdr subtree))))))))


;;; Temporary diagnostics? Needed for printing?

(defun find-clause (literals &aux cl)
  (setq literals (simplify-clause literals)
	cl (subsumed? literals (ltms-clauses *ltms*)))
  cl)


(defun print-envs (ltms)
  (maphash #'(lambda (ignore node)
	       (format t "~% ~A has label ~A" node (tms-env node :true))
	       (format t "~% (:not ~A) has label ~A" node (tms-env node :false))	       )
	   (ltms-nodes ltms)))

(defun justify-node (informant consequent antecedents)
  (add-clause (list consequent) antecedents informant))

(defun nogood-nodes (informant nodes)
  (add-clause nil nodes informant))

(defun step-1 ()
  (setq *ltms* (create-ltms "Step-1" :complete t :block? nil)
	a (tms-create-node *ltms* "A" :assumptionp t)
	b (tms-create-node *ltms* "B" :assumptionp t)
	c (tms-create-node *ltms* "C" :assumptionp t)
	x=1 (tms-create-node *ltms* "x=1")
	y=x (tms-create-node *ltms* "y=x")
	x=z (tms-create-node *ltms* "x=z")
	y=1 (tms-create-node *ltms* "y=1")
	z=1 (tms-create-node *ltms* "z=1") )
  (justify-node 'j1 x=1 (list a))
  (justify-node 'j2 y=x (list b))
  (justify-node 'j3 x=z (list c))
  (why-nodes *ltms*)
  (print-envs *ltms*)

  (format t "~2%Now register nogood{A,B}")
  (nogood-nodes 'NOGOOD (list a b))
  (why-nodes *ltms*)
  (print-envs *ltms*)

  (format t "~2%x=1, y=x => y=1")
  (justify-node 'j4 y=1 (list x=1 y=x))
  (why-nodes *ltms*)
  (print-envs *ltms*)

  (format t "~2%We have a premise z=1")
  (justify-node 'Premise z=1 nil)
  (why-nodes *ltms*)
  (print-envs *ltms*)

  (format t "~2%z=1, x=z => x=1")
  (justify-node 'j5 x=1 (list z=1 x=z))
  (why-nodes *ltms*)
  (print-envs *ltms*) )

(defun print-statistics (&optional (ltms *ltms*) &aux lengths)
  (setq lengths (make-array 100. :initial-element 0))
  (format t "~% There are ~D propositional symbols" (ltms-node-counter ltms))
  (walk-clauses ltms
		#'(lambda (cl)
		    (incf (aref lengths (clause-length cl)))))
  (dotimes (i 100)
    (unless (= (aref lengths i) 0)
      (format t "~% There are ~D prime implicates of size ~D"
	      (aref lengths i)
	      i)))
  )