!
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (MAKE-TREE (AND-LEVEL TREE)
              (DELETE-OR-NODE-WITH-CUT FORMULA (OR-LEVELS TREE))))
SET
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (LET* ((EXPANDED-VAR (LOOKUP (SECOND FORMULA)
                                   (UNIFICATION-ENV (AND-LEVEL TREE))))
              (EXPANDED-ARGS (LOOKUP (THIRD FORMULA)
                                    (UNIFICATION-ENV (AND-LEVEL TREE))))
              (RESULT (COND ((LISTP EXPANDED-ARGS)
                             (APPLY (CAR EXPANDED-ARGS)
                                    (CDR EXPANDED-ARGS)))
                            (T (EVAL EXPANDED-ARGS))))
              (NEWENV (UNIFY EXPANDED-VAR RESULT (UNIFICATION-ENV (AND-LEVEL TREE)))))
             (COND ((FAILEDP NEWENV)
                    (CLEAR-AND-LEVEL TREE))
                   (T (UPDATE-ENV NEWENV TREE)))))
PRINT
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (LET ((EXPANDED-CDR-FORMULA (LOOKUP (SECOND FORMULA)
                                          (UNIFICATION-ENV (AND-LEVEL TREE)))))
            (FORMAT T "~S ~%" EXPANDED-CDR-FORMULA)
            TREE))
EVAL&PRINT
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (LET ((EXPANDED-CDR-FORMULA (LOOKUP (SECOND FORMULA)
                                          (UNIFICATION-ENV (AND-LEVEL TREE)))))
            (FORMAT T "~S ~%" (EVAL EXPANDED-CDR-FORMULA))
            TREE))
RETRACT-THEORY
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (LET ((THEORY-NAME (LOOKUP (SECOND FORMULA)
                                          (UNIFICATION-ENV (AND-LEVEL TREE)))))
         (PROGN
            (SETF (GET-AND-NODE-THEORIES (AND-LEVEL TREE)) 
                  (DELETE THEORY-NAME (GET-AND-NODE-THEORIES (AND-LEVEL TREE)) 
          						  :TEST (FUNCTION EQUAL))) 
	 	  TREE)))
SAVE-THEORY
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (LET ((THEORY-NAME (LOOKUP (SECOND FORMULA)
                                          (UNIFICATION-ENV (AND-LEVEL TREE)))))
         (PROGN
            (SAVE-THEORY THEORY-NAME WINDOW) 
	 	  TREE)))
LOAD-THEORY
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (LET ((THEORY-NAME (LOOKUP (SECOND FORMULA)
                                          (UNIFICATION-ENV (AND-LEVEL TREE)))))
         (PROGN
            (LOAD-THEORY THEORY-NAME WINDOW) 
	 	  TREE)))
USE-THEORY
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (LET ((THEORY-NAME (LOOKUP (SECOND FORMULA)
                                          (UNIFICATION-ENV (AND-LEVEL TREE)))))
         (PROGN
            (SETF (GET-AND-NODE-THEORIES (AND-LEVEL TREE)) 
                  (APPEND (GET-AND-NODE-THEORIES (AND-LEVEL TREE)) 
					(LIST THEORY-NAME))) 
	 	  TREE)))
MERGE-THEORIES
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (LET ((THEORY-NAME (LOOKUP (SECOND FORMULA)
                                          (UNIFICATION-ENV (AND-LEVEL TREE))))
		  (LIST-OF-THEORIES (LOOKUP (REST (REST FORMULA))
								(UNIFICATION-ENV (AND-LEVEL TREE)))))
         (PROGN 
		  (OR (AND WINDOW 
				(MERGE-THEORIES-DEVEL WINDOW THEORY-NAME LIST-OF-THEORIES))
			(APPLY 'MERGE-THEORIES (CONS THEORY-NAME LIST-OF-THEORIES)))
	 	  TREE)))

FAIL
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (CLEAR-AND-LEVEL TREE))
TRUE
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       TREE)
WFF
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (LET* ((ANDLEVEL (AND-LEVEL TREE))
              (EXPANDED-CDR-FORMULA (LOOKUP (SECOND FORMULA)
                                           (UNIFICATION-ENV ANDLEVEL))))
            (SOLVE TREE EXPANDED-CDR-FORMULA
					(FIND-CLAUSES 
						(PREDICATE EXPANDED-CDR-FORMULA)
                               (GET-AND-NODE-THEORIES ANDLEVEL)
                               WINDOW))))
LOGIC-ADD
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (LET* ((ANDLEVEL (AND-LEVEL TREE))
              (EXPANDED-FORMULA (LOOKUP FORMULA (UNIFICATION-ENV ANDLEVEL))))
            (PROGN (LOGIC-ADD  (SECOND EXPANDED-FORMULA)
						(THIRD EXPANDED-FORMULA)
						(FOURTH EXPANDED-FORMULA) WINDOW)
                   TREE)))
LOGIC-ASSERT
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (LET* ((ANDLEVEL (AND-LEVEL TREE))
              (EXPANDED-FORMULA (LOOKUP FORMULA (UNIFICATION-ENV ANDLEVEL))))
            (PROGN (LOGIC-ASSERT  (SECOND EXPANDED-FORMULA)
						   (THIRD EXPANDED-FORMULA)
						   (FOURTH EXPANDED-FORMULA) WINDOW)
                   TREE)))
LOGIC-DELETE
(LAMBDA (TREE FORMULA CLAUSES WINDOW)
       (LET* ((ANDLEVEL (AND-LEVEL TREE))
              (EXPANDED-FORMULA (LOOKUP FORMULA (UNIFICATION-ENV ANDLEVEL))))
            (PROGN (LOGIC-DELETE  (SECOND EXPANDED-FORMULA)
						   (THIRD EXPANDED-FORMULA)
						   WINDOW)
                   TREE)))
THEORY-END