anchor.diff:    (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)
  -  (dbg:with-erring-frame (frame-ptr condition-object)
  -    (let (goals)
  -      (do ((frame-ptr frame-ptr (dbg:frame-previous-interesting-active-frame frame-ptr)))
  -	  ((null frame-ptr))
  -	(let* ((l (dbg:get-frame-function-and-args frame-ptr))
  -	       (n (and (symbolp (car l))
  -		       (not (invisible-functor-p (car l)))
  -		       (not (getf (get (car l) 'compiled-parameters) :split-procedure))
  -		       (get (car l) 'arity))))
  -	  (when n
  -	    (let ((k (dbg:frame-local-value frame-ptr '!nsubgoals! t)))
  -	      ;; Symbolics bug: above results in an error if there is no
  -	      ;; !nsubgoals! variable in the stack frame
  -	      (push (if k
  -			(list n l (car k) (cadr k))
  -			(list n l 0 nil))
  -		    goals)))))
  -      (format t "~2&Proof:~%Goal#  Wff#  Wff Instance~%-----  ----  ------------")
  -      (print-proof1 goals 0 1 0)
  -      nil)))
  -
  -#+SYMBOLICS
  -(defun print-proof1 (goals goalnum ngoals level)
  -  (dotimes (i ngoals)
  -    (declare (ignore i))
  -    (let ((arity (caar goals))
  -          (goal (cadar goals))
  -          (nsubgoals (caddar goals))
  -          (number (cadddr (car goals))))
  -      (format t "~&(~3D)" goalnum)
  -      (cond ((consp number) (format t "~5D~A  " (car number) (cdr number)))
  -	    (number (format t "~5D   " number))
  -	    (t (princ "        ")))
  -      (dotimes (i level) (declare (ignore i)) (princ "   "))
  -      (write-functor-and-arguments (car goal) (subseq goal 1 (1+ arity)))
  -      (cond ((= nsubgoals 0)
  -             (princ ".")
  -             (setq goalnum (1+ goalnum))
  -             (setq goals (cdr goals)))
  -	    (t (princ " <-")
  -	       (let ((first t))
  -		 (dolist (subgoal (collect-goals (cdr goals) nsubgoals))
  -		   (cond (first (princ " ") (setq first nil))
  -			 (t (princ " , ")))
  -		   (write-functor-and-arguments
  -                    (car subgoal) 
  -                    (subseq subgoal 1 (1+ (get (car subgoal) 'arity))))))
  -	       (princ ".")
  -	       (multiple-value-setq (goals goalnum)
  -                 (print-proof1 (cdr goals) (1+ goalnum) nsubgoals (1+ level)))))))
  -  (values goals goalnum))
  -
  -#+SYMBOLICS
  -(defun collect-goals (goals ngoals)
  -  (let (w)
  -    (dotimes (i ngoals)
  -      (declare (ignore i))
  -      (push (cadar goals) w)
  -      (setq goals (skip-goals (cdr goals) (caddar goals))))
  -    (nreverse w)))
  -
  -#+SYMBOLICS
  -(defun skip-goals (goals ngoals)
  -  (dotimes (i ngoals)
  -    (declare (ignore i))
  -    (setq goals (skip-goals (cdr goals) (caddar goals))))
  -  goals)
  +;;; Proof Printing Facility
  +;;;
  +;;; This was a Symbolics-only feature and will have to be re-implemented in a
  +;;; portable manner.
   
   (defun numbered-letter (n)
     (case n
  
positive.code:     :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
  
negative.code:         (undo-bindings)))))
  
  (defun =/2 (x y !level! !continuation!
              &aux (!old-trail! *trail*))
    (incf !level!)
    (when (always-trails-unify x y !old-trail!)
      (funcall !continuation! !level!)
      (undo-bindings)))
  
  (defun \\=/2 (x y !level! !continuation! &aux (!old-trail! *trail*))
    (incf !level!)
    (if (always-trails-unify x y !old-trail!)
        (undo-bindings)
        (funcall !continuation! !level!)))
  
  (defun unsafe-=/2 (x y !level! !continuation! &aux (!old-trail! *trail*))
    (incf !level!)
    (when (unsafe-always-trails-unify x y !old-trail!)
      (funcall !continuation! !level!)
      (undo-bindings)))
  
  (defun unsafe-\\=/2 (x y !level! !continuation! &aux (!old-trail! *trail*))
    (incf !level!)
    (if (unsafe-always-trails-unify x y !old-trail!)
        (undo-bindings)
        (funcall !continuation! !level!)))
  
  (defun ==/2 (x y !level! !continuation!)
    (incf !level!)
    (and (identical x y)
         (funcall !continuation! !level!)))
  
  (defun \\==/2 (x y !level! !continuation!)
    (incf !level!)
    (and (not (identical x y))
         (funcall !continuation! !level!)))
  
  (defun >/2 (x y !level! !continuation!)
    (incf !level!)
    (and (dereference x)
         (dereference y)
         (> x y)
         (funcall !continuation! !level!)))
  
  (defun </2 (x y !level! !continuation!)
    (incf !level!)
    (and (dereference x)
         (dereference y)
         (< x y)
         (funcall !continuation! !level!)))
  
  (defun >=/2 (x y !level! !continuation!)
    (incf !level!)
    (and (dereference x)
         (dereference y)
         (>= x y)
         (funcall !continuation! !level!)))
  
  (defun =</2 (x y !level! !continuation!)
    (incf !level!)
    (and (dereference x)
         (dereference y)
  