anchor.diff:  	   result))
           ((eq (car wff) 'true/0) nil)		;if wff is tautology 2005-07-21
   	(t (list wff))))
  --
  -;; PROLOG BUILT-IN PREDICATES
  -
  -;; AUXILIARY VARIABLE !NSUBGOALS! WITH VALUE '(0 NIL) NECESSARY FOR PROOF PRINTING
  -;; DUE TO BUG IN DBG:FRAME-LOCAL-VALUE THAT CAUSES AN ERROR IF NAMED VARIABLE ISN'T FOUND
  -
  -(defun call/1 (x !level! !continuation! #+SYMBOLICS &AUX #+SYMBOLICS (!NSUBGOALS! '(1 NIL)))
  -  #+SYMBOLICS (DECLARE (IGNORE !NSUBGOALS!))
  +
  +;; Prolog built-in predicates
  +
  +;; Auxiliary variable !NSUBGOALS! with value '(0 NIL) necessary for proof
  +;; printing due to bug in DBG:FRAME-LOCAL-VALUE that causes an error if named
  +;; variable isn't found
  +
  +(defun call/1 (x !level! !continuation!
  +               #+SYMBOLICS &aux #+SYMBOLICS (!nsubgoals! '(1 nil)))
  +  #+SYMBOLICS (declare (ignore !nsubgoals!))
     (incf !level!)
     (dereference x
  -	       :if-variable  (error "CALL was given non-compound argument ~A" x)
  -	       :if-constant  (error "CALL was given non-compound argument ~A" x)
  -	       :if-compound  (apply (car x) (append (cdr x) (list !level! !continuation!)))))	; inefficient
  -
  -(defun not/1 (x !level! !continuation! #+SYMBOLICS &AUX #+SYMBOLICS (!NSUBGOALS! '(0 NIL)))
  -  #+SYMBOLICS (DECLARE (IGNORE !NSUBGOALS!))
  +    :if-variable (error "CALL was given non-compound argument ~A" x)
  +    :if-constant (error "CALL was given non-compound argument ~A" x)
  +    :if-compound (apply (car x)
  +                        ;; inefficient
  +                        (append (cdr x) (list !level! !continuation!)))))
  +
  +(defun not/1 (x !level! !continuation!
  +              #+SYMBOLICS &aux #+SYMBOLICS (!nsubgoals! '(0 nil)))
  +  #+SYMBOLICS (declare (ignore !nsubgoals!))
     (not-solvable x 1000000 !level! !continuation!))
   
  -(defun not/2 (x y !level! !continuation! #+SYMBOLICS &AUX #+SYMBOLICS (!NSUBGOALS! '(0 NIL)))
  -  #+SYMBOLICS (DECLARE (IGNORE !NSUBGOALS!))
  +(defun not/2 (x y !level! !continuation!
  +              #+SYMBOLICS &aux #+SYMBOLICS (!nsubgoals! '(0 nil)))
  +  #+SYMBOLICS (declare (ignore !nsubgoals!))
     (not-solvable x y !level! !continuation!))
   
  -(defun y-or-n-p/0 (!level! !continuation! #+SYMBOLICS &AUX #+SYMBOLICS (!NSUBGOALS! '(0 NIL)))
  -  #+SYMBOLICS (DECLARE (IGNORE !NSUBGOALS!))
  +(defun y-or-n-p/0 (!level! !continuation!
  +                   #+SYMBOLICS &aux #+SYMBOLICS (!nsubgoals! '(0 nil)))
  +  #+SYMBOLICS (declare (ignore !nsubgoals!))
     (incf !level!)
     (if (y-or-n-p)
         (funcall !continuation! !level!)
         nil))
   
  -(defun y-or-n-p/1 (x !level! !continuation! #+SYMBOLICS &AUX #+SYMBOLICS (!NSUBGOALS! '(0 NIL)))
  -  #+SYMBOLICS (DECLARE (IGNORE !NSUBGOALS!))
  +(defun y-or-n-p/1 (x !level! !continuation!
  +                   #+SYMBOLICS &aux #+SYMBOLICS (!nsubgoals! '(0 nil)))
  +  #+SYMBOLICS (declare (ignore !nsubgoals!))
     (incf !level!)
     (fresh-line) (write-term x) (princ "? ")
     (if (y-or-n-p)
         (funcall !continuation! !level!)
         nil))
   
  -(defun atomic/1 (x !level! !continuation! #+SYMBOLICS &AUX #+SYMBOLICS (!NSUBGOALS! '(0 NIL)))
  +(defun atomic/1 (x !level! !continuation!
  +                 #+SYMBOLICS &aux #+SYMBOLICS (!nsubgoals! '(0 nil)))
  +  #+SYMBOLICS (declare (ignore !nsubgoals!))
  +  (incf !level!)
  +  (and (dereference x) (funcall !continuation! !level!)))
  +
  +(defun atom/1 (x !level! !continuation!
  +               #+SYMBOLICS &aux #+SYMBOLICS (!nsubgoals! '(0 nil)))
  +  #+SYMBOLICS (declare (ignore !nsubgoals!))
  +  (incf !level!)
  +  (and (dereference x) (symbolp x) (funcall !continuation! !level!)))
  +
  +(defun integer/1 (x !level! !continuation!
  +                  #+SYMBOLICS &aux #+SYMBOLICS (!nsubgoals! '(0 nil)))
  +  #+SYMBOLICS (declare (ignore !nsubgoals!))
  +  (incf !level!)
  +  (and (dereference x) (integerp x) (funcall !continuation! !level!)))
  +
  +(defun var/1 (x !level! !continuation!
  +              #+SYMBOLICS &aux #+SYMBOLICS (!nsubgoals! '(0 nil)))
  +  #+SYMBOLICS (declare (ignore !nsubgoals!))
  +  (incf !level!)
  +  (dereference x
  +    :if-constant  nil
  +    :if-variable  (funcall !continuation! !level!)
  +    :if-compound  nil))
  +
  +(defun nonvar/1 (x !level! !continuation!
  +                 #+SYMBOLICS &aux #+SYMBOLICS (!nsubgoals! '(0 nil)))
     #+SYMBOLICS (DECLARE (IGNORE !NSUBGOALS!))
     (incf !level!)
  -  (and (dereference x) (funcall !continuation! !level!)))
  -
  -(defun atom/1 (x !level! !continuation! #+SYMBOLICS &AUX #+SYMBOLICS (!NSUBGOALS! '(0 NIL)))
  -  #+SYMBOLICS (DECLARE (IGNORE !NSUBGOALS!))
  -  (incf !level!)
  -  (and (dereference x) (symbolp x) (funcall !continuation! !level!)))
  -
  -(defun integer/1 (x !level! !continuation! #+SYMBOLICS &AUX #+SYMBOLICS (!NSUBGOALS! '(0 NIL)))
  -  #+SYMBOLICS (DECLARE (IGNORE !NSUBGOALS!))
  -  (incf !level!)
  -  (and (dereference x) (integerp x) (funcall !continuation! !level!)))
  -
  -(defun var/1 (x !level! !continuation! #+SYMBOLICS &AUX #+SYMBOLICS (!NSUBGOALS! '(0 NIL)))
  -  #+SYMBOLICS (DECLARE (IGNORE !NSUBGOALS!))
  -  (incf !level!)
     (dereference x
  -	       :if-constant  nil
  -	       :if-variable  (funcall !continuation! !level!)
  -	       :if-compound  nil))
  -
  -(defun nonvar/1 (x !level! !continuation! #+SYMBOLICS &AUX #+SYMBOLICS (!NSUBGOALS! '(0 NIL)))
  -  #+SYMBOLICS (DECLARE (IGNORE !NSUBGOALS!))
  -  (incf !level!)
  -  (dereference x
  -	       :if-constant  (funcall !continuation! !level!)
  -	       :if-variable  nil
  -	       :if-compound  (funcall !continuation! !level!)))
  -
  -(defun functor/3 (term functor arity !level! !continuation! &aux (!old-trail! *trail*) #+SYMBOLICS (!NSUBGOALS! '(0 NIL)))
  -  #+SYMBOLICS (DECLARE (IGNORE !NSUBGOALS!))
  +    :if-constant  (funcall !continuation! !level!)
  +    :if-variable  nil
  +    :if-compound  (funcall !continuation! !level!)))
  +
  +(defun functor/3 (term functor arity !level! !continuation!
  +                  &aux (!old-trail! *trail*)
  +                       #+SYMBOLICS (!nsubgoals! '(0 nil)))
  +  #+SYMBOLICS (declare (ignore !nsubgoals!))
     (incf !level!)
     (dereference
  -    term
  +      term
       :if-variable
       (when (and (dereference functor) (dereference arity))
         (case arity
   	(0 (progn (bind-variable-to-term term functor :trail)
   		  (funcall !continuation! !level!)
   		  (undo-bindings)))
  +        ;; (new-variable '_)
   	(1 (stack-let ((struct (list functor
  -				     (list* !level! nil #+include-name-in-variable 'z1))))	; (new-variable '_)
  +				     (list* !level! nil
  +                                            #+include-name-in-variable 'z1))))	
   	     (progn (bind-variable-to-term term struct :trail)
   		    (funcall !continuation! !level!)
   		    (undo-bindings))))
  
positive.code: (defmacro with-n-subgoals (n form)
    `(let ((*remaining-depth* (- *remaining-depth* ,n)))
       (cond ((minusp *remaining-depth*)
  	    (if (> *remaining-depth* *minus-next-depth-increment*) (setq *minus-next-depth-increment* *remaining-depth*))
  	    nil)
  	   (t ,form))))
  
  
negative.code: 
  (defun cputime/0 nil
    (get-internal-run-time))
  
  
  ;; PROOF PRINTING FACILITY
  ;; this works only on Symbolics machines because it examines the stack to find
  ;; goals and subgoals if including variable names in variables is turned off
  ;; for speed, variable names printed in proof may be ambiguous
  
  #+SYMBOLICS
  (scl:defflavor print-proof () (scl:condition))
  
  #+SYMBOLICS
  (scl:defmethod (dbg:report print-proof) (stream)
    (declare (ignore stream)) nil)
  
  #+SYMBOLICS
  (defun print-proof (condition-object)
  