; Milawa - A Reflective Theorem Prover
; Copyright (C) 2005-2009 Kookamara LLC
;
; Contact:
;
;   Kookamara LLC
;   11410 Windermere Meadows
;   Austin, TX 78759, USA
;   http://www.kookamara.com/
;
; License: (An MIT/X11-style license)
;
;   Permission is hereby granted, free of charge, to any person obtaining a
;   copy of this software and associated documentation files (the "Software"),
;   to deal in the Software without restriction, including without limitation
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
;   and/or sell copies of the Software, and to permit persons to whom the
;   Software is furnished to do so, subject to the following conditions:
;
;   The above copyright notice and this permission notice shall be included in
;   all copies or substantial portions of the Software.
;
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
;   DEALINGS IN THE SOFTWARE.
;
; Original author: Jared Davis <jared@kookamara.com>


; Proof Sizes Script
;
; This script measures the proof sizes of some sample proofs when emitted at
; the various levels.  You must run this script with the proof-sizes-acl2
; executable, which can be generated by running proof-sizes-acl2.lsp in
; level2/symmetry.

(in-package "MILAWA")
(%interactive)


; Now we introduce the %reprove command.  This takes the name of the theorem to
; reprove, and perhaps some additional hints that will be necessary to fix the
; issues with "local" theory changes, etc.  It then tries to redo the proof by
; reusing the theory and hints and so forth that our modified %autoprove has
; built.  Finally, if everything is successful, it saves the UNCOMPILED PROOF
; SKELETON so that it can be compiled at various levels and the proof sizes
; compared.

(ACL2::table reprove 'goalworlds nil)
(ACL2::table reprove 'skeletons nil)
(ACL2::table reprove 'sizes nil)

(defun reprove->goalworlds (world)
  (declare (xargs :mode :program))
  (cdr (lookup 'goalworlds (ACL2::table-alist 'reprove world))))

(defun reprove->skeletons (world)
  (declare (xargs :mode :program))
  (cdr (lookup 'skeletons (ACL2::table-alist 'reprove world))))

(defun reprove->sizes (world)
  (declare (xargs :mode :program))
  (cdr (lookup 'sizes (ACL2::table-alist 'reprove world))))


(ACL2::table reprove 'full-world (tactic.harness->world acl2::world))


(defun reprove->fullworld (world)
  (declare (xargs :mode :program))
  (cdr (lookup 'full-world (ACL2::table-alist 'reprove world))))

(defmacro %reprove (name &rest rhints)
  `(ACL2::make-event (%reprove-fn ',name ',rhints (ACL2::w ACL2::state))))

;; stupid god damn embeddable events and time$...
(defun start-timer ()
  (declare (xargs :guard t))
  (acl2::cw "start-timer not redefined.~%"))

(defun end-timer ()
  (declare (xargs :guard t))
  (acl2::cw "end-timer not redefined.~%"))


(defun %reprove-fn (name rhints world)
  (declare (xargs :mode :program))
  (let* ((rule          (tactic.find-rule name (reprove->fullworld world)))
         (hints-tuple   (lookup name (get-autoprove-hints world)))
         (hints         (second hints-tuple))
         (initial-world (third hints-tuple)))
    (ACL2::prog2$
     (ACL2::cw "%reprove-fn> size of initial-world is ~x0.~%" (rank initial-world))
     `(ACL2::encapsulate
       ()

; This is basically like %prove.  We need to load the goalrule, goalworld, and
; set up an empty, initial skeleton with the appropriate goals.

       (ACL2::value-triple (ACL2::cw "[%Reprove]> Submitting ~x0.~%" ',name))
       (ACL2::table tactic-harness 'goalrule ',rule)
       (ACL2::table tactic-harness 'goalworld ',initial-world)
       (ACL2::table tactic-harness 'world ',initial-world)

       (local (ACL2::table tactic-harness 'skeleton (tactic.initial-skeleton (list ',(rw.rule-clause rule)))))

; This is basically like %autoprove.  We get the hints that were given when the
; proof was submitted, preceded by any extra hints that we might want to give
; to fix up theories, etc., then finally give %auto.

       (ACL2::value-triple (ACL2::cw "[%Reprove]> Trying to replay the proof.~%"))
       (acl2::value-triple (start-timer))
       (local (ACL2::progn ,@rhints ,@hints (%auto)))
       (acl2::value-triple (end-timer))

       (ACL2::value-triple (ACL2::cw "[%Reprove]> Checking for success and saving skeleton.~%"))
       (ACL2::make-event (%reprove-save-skelly-fn ACL2::state))))))


(defun %reprove-save-skelly-fn (ACL2::state)
  (declare (xargs :mode :program :stobjs ACL2::state))

; Here we save the skeleton, world, and definitions that were used during the
; proof.  We will need these in order to compile the skeleton and build the
; level-N proof.

  (let* ((world     (ACL2::w ACL2::state))
         (skeleton  (tactic.harness->skeleton world))
         (goals     (tactic.skeleton->goals skeleton))
         (goalrule  (tactic.harness->goalrule world))
         (goalworld (tactic.harness->goalworld world))
         (name      (rw.rule->name goalrule)))
    (if (consp goals)
        (ACL2::er soft '%reprove "Outstanding goals remain for ~s0.~%" name)
      (ACL2::mv nil
                `(ACL2::progn
                  (ACL2::table reprove 'skeletons
                               (cons (cons ',name ',skeleton) (reprove->skeletons ACL2::world)))
                  (ACL2::table reprove 'goalworlds
                               (cons (cons ',name ',goalworld) (reprove->goalworlds ACL2::world))))
                ACL2::state))))

(defmacro %reprove-compile (name)
  `(ACL2::progn
    (local (ACL2::memoize 'rank))
    (ACL2::make-event (ACL2::time$ (%reprove-compile-fn ',name ACL2::state)))
    (local (ACL2::unmemoize 'rank))
    (local (ACL2::value-triple (ACL2::clear-memoize-tables)))))

(defun static-analysis (proof)
  ;; We return (STATIC-RANK . DYNAMIC-RANK) where these count the static and dynamic
  ;; sizes of the proof.
  (declare (xargs :mode :program))
  (let ((method (logic.method proof))
        (extras (logic.extras proof)))
    (acl2::prog2$
     (acl2::cw "static analysis for proof of type ~x0. total rank is ~x1. #extras = ~x2~%"
               method
               (rank proof)
               (len extras))
     (let ((result (cond ((equal method 'level8.proofp)
                          (acl2::prog2$
                           (or (equal (len extras) 2)
                               (acl2::er hard? 'static-analysis "level8 format changed?"))
                           (list (rank (first extras)) (rank (second extras)))))
                         ((or (equal method 'level9.proofp)
                              (equal method 'level10.proofp)
                              (equal method 'level11.proofp))
                          (acl2::prog2$
                           (or (equal (len extras) 3)
                               (acl2::er hard? 'static-analysis "level9-11 format changed?"))
                           (list (+ (rank (first extras)) (rank (second extras)))
                                 (rank (third extras)))))
                         (t
                          (list 0 (rank proof))))))
       (acl2::prog2$
        (acl2::cw "static analysis yields: ~x0.~%" result)
        result)))))

(defun %time-and-check-proof (proofp-name thm-name proof axioms thms atbl)
  (declare (xargs :guard t)
           (ignore proofp-name thm-name proof axioms thms atbl))
  (acl2::cw "%time-and-check-proof has not been redefined!~%"))

(defun %time-proof-building (proofp-name thm-name skelly init-world)
  (declare (xargs :guard t)
           (ignore proofp-name thm-name skelly init-world))
  (acl2::cw "%time-proof-building has not been redefined!~%"))

(acl2::defttag time-and-check-proof)

(ACL2::progn!
 (ACL2::set-raw-mode t)

 (acl2::defparameter *time-and-check-table* nil)
 (acl2::defparameter *time-building-table* nil)

 (acl2::defparameter *timer-for-start/end-timer* 0)

 (acl2::defun start-timer ()
              (acl2::setf *timer-for-start/end-timer* (acl2::get-internal-real-time)))

 (acl2::defun end-timer ()
              (let* ((start   *timer-for-start/end-timer*)
                     (end     (acl2::get-internal-real-time))
                     (elapsed (ACL2::/ (ACL2::coerce (ACL2::- end start) 'ACL2::float)
                               ACL2::internal-time-units-per-second)))
                (acl2::progn
                 (ACL2::format t "Elapsed time from start/end-timer: ~a.~%" elapsed)
                 nil)))

 (acl2::defun %time-and-check-proof (proofp-name thm-name proof axioms thms atbl)
   (let* ((start-time (ACL2::get-internal-real-time))
          (result     (%current-proofp proof axioms thms atbl))
          (end-time   (ACL2::get-internal-real-time))
          (elapsed    (ACL2::/ (ACL2::coerce (ACL2::- end-time start-time) 'ACL2::float)
                               ACL2::internal-time-units-per-second)))
     (ACL2::progn
      (ACL2::format t "~a checks ~a in ~a seconds.~%" proofp-name thm-name elapsed)
      (acl2::push (list proofp-name thm-name elapsed) *time-and-check-table*)
      result)))

 (acl2::defun %time-proof-building (proofp-name thm-name skelly init-world)
   (let* ((start-time (ACL2::get-internal-real-time))
          (worlds (ACL2::prog2$
                   (ACL2::cw "; Compiling worlds for ~x0...~%" thm-name)
                   (tactic.compile-worlds skelly init-world)))
          (proof  (%current-adapter
                   (ACL2::prog2$ (ACL2::cw "Compiling skeleton for ~x0.~%" thm-name)
                                 (car (ACL2::time$ (tactic.compile-skeleton skelly worlds nil))))
                   (tactic.world->defs init-world)
                   init-world
                   worlds))
          (end-time   (ACL2::get-internal-real-time))
          (elapsed    (ACL2::/ (ACL2::coerce (ACL2::- end-time start-time) 'ACL2::float)
                               ACL2::internal-time-units-per-second)))
     (ACL2::progn
      (ACL2::format t "built ~a for ~a in ~a seconds.~%" thm-name proofp-name elapsed)
      (acl2::push (list proofp-name thm-name elapsed) *time-building-table*)
      proof))))

(defun %reprove-compile-fn (name ACL2::state)
  (declare (xargs :mode :program :stobjs ACL2::state))
  (let* ((world      (ACL2::w ACL2::state))
         (skelly     (cdr (lookup name (reprove->skeletons world))))
         (init-world (cdr (lookup name (reprove->goalworlds world)))))
    (if (not skelly)
        (ACL2::er soft '%reprove-compile "Unable to find skeleton for ~s0.~%" name)

; This is basically like %qed-check-fn.  We have the goalworld and skeleton,
; and we just need to compile it and apply the adapter.

      (let* ((proof (%time-proof-building (tactic.harness->current-proofp world)
                                          name
                                          skelly
                                          init-world))
             (check  (ACL2::prog2$
                      (ACL2::cw "Checking the proof...~%")
                      (or (%time-and-check-proof (tactic.harness->current-proofp world)
                                                 name
                                                 proof
                                                 (tactic.harness->axioms world)
                                                 (tactic.harness->thms world)
                                                 (tactic.harness->atbl world))
                          (ACL2::er hard? '%reprove-compile-fn "Proof was rejected.~%")))))
        (declare (ignore check))
        (ACL2::prog2$
         (ACL2::cw "Total size: ~s0~s1 conses~s2.~%" *blue* (STR::pretty-number (rank proof)) *black*)
         (ACL2::mv nil
                   `(ACL2::table reprove 'sizes
                                 (cons (list (tactic.harness->current-proofp ACL2::world)
                                             ',name
                                             ',(static-analysis proof))
                                       (reprove->sizes ACL2::world)))
                   ACL2::state))))))



(include-book "level2/level2")
(include-book "level3/level3")
(include-book "level4/level4")
(include-book "level5/level5")
(include-book "level6/level6")
(include-book "level7/level7")
(include-book "level8/level8")
(include-book "level9/level9")
(include-book "level10/level10")
(i-am-here)

;; reprove fresh here for fast-urewrite
(include-book "level10/level10")

;; reprove fresh here for fast-crewrite
(include-book "level11/level11")

;; probably reprove fresh here for good measure

(%reprove forcing-logic.proofp-of-build.disjoined-transitivity-of-iff
          (%enable default
                   theorem-transitivity-of-iff
                   theorem-transitivity-of-iff
                   theorem-transitivity-of-iff
                   build.disjoined-transitivity-of-iff))

(%reprove-compile forcing-logic.proofp-of-build.disjoined-transitivity-of-iff)


8 compile
6 static-checks
2 skeletonp
147 skeleton-okp

288s atblp -- this is the one to fix, suppose 10s
0s env-okp
---------
(+ 8 6 2 147) 163

(set-verify-guards-eagerness 2)
(set-case-split-limitations nil)
(set-well-founded-relation ord<)
(set-measure-function rank)




:redef

(defund tactic.compile-skeleton-okp (x worlds axioms thms atbl)
  (declare (xargs :guard (and (logic.appealp x)
                              (tactic.world-listp worlds)
                              (logic.formula-listp axioms)
                              (logic.formula-listp thms)
                              (logic.arity-tablep atbl))))
  (let ((method     (logic.method x))
        (conclusion (logic.conclusion x))
        (subproofs  (logic.subproofs x))
        (extras     (logic.extras x)))
    (and (equal method 'tactic.compile-skeleton)
         (acl2::time$ (tactic.skeletonp extras))
         (acl2::time$ (tactic.skeleton-okp extras worlds))
         (acl2::time$ (tactic.fast-skeleton-atblp extras atbl))
         (acl2::time$ (tactic.skeleton-env-okp extras worlds axioms thms atbl))
         (memberp conclusion
                  (clause.clause-list-formulas (tactic.original-conclusions extras)))
         (equal (logic.strip-conclusions subproofs)
                (clause.clause-list-formulas (tactic.skeleton->goals extras))))))












(%reprove lemma-for-forcing-logic.proofp-of-generic-evaluator-bldr
          ;(%enable default iff iff iff)
          )

(%reprove-compile lemma-for-forcing-logic.proofp-of-generic-evaluator-bldr)


;; --- we are missing some rules from this, somehow ??
;(include-book "level10/crewrite-local-settings")
(encapsulate
 ()

 (%rwn 1000)

 (%cheapen default rw.trace-list-rhses-when-not-consp)
; (%cheapen default rw.crewrite-core-list-when-not-consp)

 (%create-theory my-disables-for-extra-speed)
 (%enable my-disables-for-extra-speed
          consp-when-memberp-of-logic.sigmap
          consp-when-memberp-of-logic.sigmap-alt
          consp-when-memberp-of-logic.sigma-atblp
          consp-when-memberp-of-logic.sigma-atblp-alt
          consp-when-memberp-of-logic.arity-tablep
          consp-when-memberp-of-logic.arity-tablep-alt
          ;;consp-when-memberp-of-logic.callmapp
          ;;consp-when-memberp-of-logic.callmapp-alt
          ;;consp-when-memberp-of-logic.callmap-atblp
          ;;consp-when-memberp-of-logic.callmap-atblp-alt
;          consp-when-memberp-of-rw.cachemapp
;          consp-when-memberp-of-rw.cachemapp-alt
          consp-when-memberp-of-none-consp
          consp-when-memberp-of-none-consp-alt
          consp-when-memberp-of-cons-listp
          consp-when-memberp-of-cons-listp-alt
          same-length-prefixes-equal-cheap
          car-when-not-consp
          cdr-when-not-consp
          consp-when-natp-cheap
          forcing-logic.groundp-of-logic.substitute
          consp-when-logic.lambdap-cheap
          consp-when-logic.functionp-cheap
          consp-when-nonempty-subset-cheap
          consp-when-memberp-cheap
          logic.substitute-when-malformed-cheap
          logic.constant-listp-when-not-consp
          subsetp-when-not-consp
          subsetp-when-not-consp-two
          cons-listp-when-not-consp
          none-consp-when-not-consp
          forcing-logic.substitute-of-empty-sigma
          not-equal-when-less
          trichotomy-of-<
          natp-of-len-free
          transitivity-of-<
          transitivity-of-<-three
          transitivity-of-<-two
          less-completion-left
          less-of-one-right)
 (%disable default my-disables-for-extra-speed)

 (%disable default zp min)

 (%disable default
           formula-decomposition
           expensive-term/formula-inference
           expensive-arithmetic-rules
           expensive-arithmetic-rules-two
           type-set-like-rules
           unusual-consp-rules
           unusual-memberp-rules
           unusual-subsetp-rules
           same-length-prefixes-equal-cheap
           ;; ---
           lookup-when-not-consp
           rw.trace-list-rhses-when-not-consp
           forcing-logic.function-of-logic.function-name-and-logic.function-args-free)

 (%disable default
           logic.substitute-when-logic.lambdap-cheap
           logic.substitute-when-logic.variablep
           logic.substitute-when-logic.constantp
           logic.substitute-when-logic.functionp-cheap
           forcing-logic.substitute-list-of-empty-sigma
           logic.substitute-list-when-not-consp
           logic.substitute-list-of-cons-gross)


 ;; SPECIAL THEORIES FOR THE OPENING MOVE.

 (%create-theory splitters)
 (%enable splitters
          ;; These are all of the rules that introduce an "if" on the
          ;; right-hand side (and hence may cause case splits).
          (gather from default (not (clause.simple-termp rhs))))
 (%disable default splitters)


 (%create-theory special-disables-for-fast-pruning)
 (%enable special-disables-for-fast-pruning
          ;; These are rules which %profile said were useless and
          ;; expensive during the initial phase.  Disabling them helps to
          ;; speed up the rewriting.
          rw.trace-list-rhses-when-not-consp
          logic.termp-when-not-consp-cheap
          rank-when-not-consp
          rw.trace-listp-when-not-consp
;          forcing-rw.assmsp-of-rw.assume-left
          logic.term-listp-when-not-consp
          ord<-when-naturals
          logic.sigmap-when-not-consp
          logic.constant-listp-of-logic.function-args-when-logic.base-evaluablep
          forcing-logic.term-listp-of-rw.trace-list-rhses
          cdr-when-true-listp-with-len-free-past-the-end
          forcing-logic.groundp-when-logic.constant-listp-of-logic.function-args
          minus-when-zp-left-cheap
          minus-when-zp-right-cheap
          minus-when-not-less
          forcing-logic.groundp-when-logic.constant-listp-of-logic.lambda-actuals
          logic.variable-listp-of-cdr-when-logic.variable-listp
          forcing-logic.termp-of-logic.substitute
          logic.variablep-of-car-when-logic.variable-listp
          rw.rule-listp-of-cdr-when-rw.rule-listp
          cdr-of-cdr-when-true-listp-with-len-free-past-the-end
          cdr-of-cdr-with-len-free-past-the-end
          logic.groundp-when-logic.constantp
          forcing-logic.function-args-of-logic.substitute
          forcing-logic.lambda-actuals-of-logic.substitute
          logic.constant-listp-of-cdr-when-logic.constant-listp
;          rw.typed-rulemapp-when-not-consp
          memberp-when-not-consp ordp-when-natp
          memberp-when-memberp-of-cdr
          rw.rulep-of-car-when-rw.rule-listp
          logic.sigmap-of-car-when-logic.sigma-listp
;          forcing-rw.cachep-of-rw.set-blockedp
          logic.sigma-listp-of-cdr-when-logic.sigma-listp
          )
 (%disable default special-disables-for-fast-pruning)

 )


(%reprove lemma-for-rw.trace-fast-image-of-rw.crewrite-core)




; You can now choose a theorem to try.  It gets the previous hints
; automatically, but you can give more hints to set up whatever local
; environment you need, e.g., with theories, etc.


; I choose a few proofs by running
;
;    grep -B 2 "Proof size" *.pcert.out
;
; in each directory and looking for large proofs.  (Actually you can
; automatically choose only the multi-million cons proofs like this):
;
;    grep -B 2 "Proof size" *.pcert.out | grep -B 2 "[0-9][0-9][0-9],[0-9][0-9][0-9],[0-9][0-9][0-9]"
;
; I picked a few proofs from each directory.  I tried to get some level of
; diversity in the type of proof.

(acl2::trace$ (TACTIC.CREWRITE-ALL-TAC
               :entry (list :theoryname (second acl2::arglist)
                            :fastp (third acl2::arglist))))

(acl2::trace$ rw.fast-transitivity-trace)

(%reprove forcing-logic.proofp-of-build.disjoined-transitivity-of-iff
          (%enable default
                   theorem-transitivity-of-iff
                   build.disjoined-transitivity-of-iff))

(%reprove forcing-logic.proofp-of-build.disjoined-negative-lit-from-pequal-nil
          (%enable default
                   build.disjoined-negative-lit-from-pequal-nil
                   theorem-not-when-nil))

(%reprove forcing-logic.proofp-of-clause.aux-split-double-negate
          (%splitlimit 8) ;; from level5/level5
          (%enable default
                   logic.term-formula
                   clause.aux-split-goal
                   clause.aux-split-double-negate))

(%reprove build.disjoined-equal-by-args-aux-okp-removal)

(%reprove forcing-logic.proofp-of-clause.disjoined-substitute-iff-into-literal-bldr
          (%enable default clause.disjoined-substitute-iff-into-literal-bldr))

(%reprove forcing-logic.conclusion-of-clause.disjoined-aux-split-negative-bldr
           (%enable default
                    clause.disjoined-aux-split-negative-bldr
                    clause.theorem-aux-split-negative))

(%reprove lemma-for-forcing-logic.appealp-of-clause.aux-update-clause-bldr)
e
(%reprove lemma-for-forcing-logic.proofp-of-generic-evaluator-bldr)

(%reprove lemma-for-forcing-logic.appealp-of-clause.factor-bldr)



; The reprove command above creates the skeleton, but doesn't compile
; it.  We can now compile it with the %reprove-compile command.

(defmacro do-compilations ()
  `(acl2::progn
    (%reprove-compile forcing-logic.proofp-of-build.disjoined-transitivity-of-iff)
    (%reprove-compile forcing-logic.proofp-of-build.disjoined-negative-lit-from-pequal-nil)
    (%reprove-compile forcing-logic.proofp-of-clause.aux-split-double-negate)
    (%reprove-compile build.disjoined-equal-by-args-aux-okp-removal)
    (%reprove-compile forcing-logic.proofp-of-clause.disjoined-substitute-iff-into-literal-bldr)
    (%reprove-compile forcing-logic.conclusion-of-clause.disjoined-aux-split-negative-bldr)
    (%reprove-compile lemma-for-forcing-logic.appealp-of-clause.aux-update-clause-bldr)
    (%reprove-compile lemma-for-forcing-logic.proofp-of-generic-evaluator-bldr)
    (%reprove-compile lemma-for-forcing-logic.appealp-of-clause.factor-bldr)
    ))




(do-compilations)

; To see what the proof is like at later levels, we can include-book the
; next level up and call reprove-compile again.  This time the compilation
; is done using the newly-switched builders.

(include-book "level2/level2")
(do-compilations)

; And so on, for the other levels.  The sizes for the proofs are saved
; into a the reprove->sizes table, so you can summarize them at the end.

(include-book "level3/level3")
(do-compilations)

(include-book "level4/level4")
(do-compilations)

(include-book "level5/level5")
(do-compilations)

(include-book "level6/level6")
(do-compilations)

(include-book "level7/level7")
(do-compilations)

(include-book "level8/level8")
(do-compilations)

(include-book "level9/level9")
(do-compilations)

(include-book "level10/level10")
(do-compilations)

(include-book "level11/level11")
(do-compilations)

; To see a summary, we run reprove->sizes.

(reprove->sizes (ACL2::w ACL2::state))



(include-book "level2/level2")
(include-book "level3/level3")
(include-book "level4/level4")
(include-book "level5/level5")
(include-book "level6/level6")
(include-book "level7/level7")
(include-book "level8/level8")
(include-book "level9/level9")
(include-book "level10/level10")


(do-compilations)

(include-book "level10/level10")
(do-compilations)

(include-book "level11/level11")




(i-am-here)

:q

(acl2::cw "~x0~%"
          (acl2::sort (reprove->sizes (acl2::w acl2::*the-live-state*))
                      (lambda (x y)
                        (or (symbol-< (second x) (second y))
                            (and (equal (second x) (second y))
                                 (symbol-< (first x) (first y)))))))

(acl2::dolist (elem (acl2::sort *time-and-check-table*
                          (lambda (x y)
                            (or (symbol-< (second x) (second y))
                                (and (equal (second x) (second y))
                                     (symbol-< (first x) (first y)))))))
  (acl2::format t "~a~%" elem))

;; ((LEVEL10.PROOFP BUILD.DISJOINED-EQUAL-BY-ARGS-AUX-OKP-REMOVAL
;;                  404290)
;;  (LEVEL11.PROOFP BUILD.DISJOINED-EQUAL-BY-ARGS-AUX-OKP-REMOVAL
;;                  394081)
;;  (LEVEL2.PROOFP BUILD.DISJOINED-EQUAL-BY-ARGS-AUX-OKP-REMOVAL
;;                 4487648)
;;  (LEVEL3.PROOFP BUILD.DISJOINED-EQUAL-BY-ARGS-AUX-OKP-REMOVAL
;;                 2376969)
;;  (LEVEL4.PROOFP BUILD.DISJOINED-EQUAL-BY-ARGS-AUX-OKP-REMOVAL
;;                 1212457)
;;  (LEVEL5.PROOFP BUILD.DISJOINED-EQUAL-BY-ARGS-AUX-OKP-REMOVAL
;;                 929253)
;;  (LEVEL6.PROOFP BUILD.DISJOINED-EQUAL-BY-ARGS-AUX-OKP-REMOVAL
;;                 782922)
;;  (LEVEL7.PROOFP BUILD.DISJOINED-EQUAL-BY-ARGS-AUX-OKP-REMOVAL
;;                 705301)
;;  (LEVEL8.PROOFP BUILD.DISJOINED-EQUAL-BY-ARGS-AUX-OKP-REMOVAL
;;                 406863)
;;  (LEVEL9.PROOFP BUILD.DISJOINED-EQUAL-BY-ARGS-AUX-OKP-REMOVAL
;;                 403202)
;;  (LOGIC.PROOFP BUILD.DISJOINED-EQUAL-BY-ARGS-AUX-OKP-REMOVAL
;;                37671049)
;;  (LEVEL10.PROOFP
;;       FORCING-LOGIC.CONCLUSION-OF-CLAUSE.DISJOINED-AUX-SPLIT-NEGATIVE-BLDR
;;       53612318)
;;  (LEVEL11.PROOFP
;;       FORCING-LOGIC.CONCLUSION-OF-CLAUSE.DISJOINED-AUX-SPLIT-NEGATIVE-BLDR
;;       52341246)
;;  (LEVEL2.PROOFP
;;       FORCING-LOGIC.CONCLUSION-OF-CLAUSE.DISJOINED-AUX-SPLIT-NEGATIVE-BLDR
;;       1126851329)
;;  (LEVEL3.PROOFP
;;       FORCING-LOGIC.CONCLUSION-OF-CLAUSE.DISJOINED-AUX-SPLIT-NEGATIVE-BLDR
;;       615153460)
;;  (LEVEL4.PROOFP
;;       FORCING-LOGIC.CONCLUSION-OF-CLAUSE.DISJOINED-AUX-SPLIT-NEGATIVE-BLDR
;;       104945672)
;;  (LEVEL5.PROOFP
;;       FORCING-LOGIC.CONCLUSION-OF-CLAUSE.DISJOINED-AUX-SPLIT-NEGATIVE-BLDR
;;       82338572)
;;  (LEVEL6.PROOFP
;;       FORCING-LOGIC.CONCLUSION-OF-CLAUSE.DISJOINED-AUX-SPLIT-NEGATIVE-BLDR
;;       37956239)
;;  (LEVEL7.PROOFP
;;       FORCING-LOGIC.CONCLUSION-OF-CLAUSE.DISJOINED-AUX-SPLIT-NEGATIVE-BLDR
;;       33735165)
;;  (LEVEL8.PROOFP
;;       FORCING-LOGIC.CONCLUSION-OF-CLAUSE.DISJOINED-AUX-SPLIT-NEGATIVE-BLDR
;;       53725739)
g;;  (LEVEL9.PROOFP
;;       FORCING-LOGIC.CONCLUSION-OF-CLAUSE.DISJOINED-AUX-SPLIT-NEGATIVE-BLDR
;;       53541935)
;;  (LOGIC.PROOFP
;;       FORCING-LOGIC.CONCLUSION-OF-CLAUSE.DISJOINED-AUX-SPLIT-NEGATIVE-BLDR
;;       9728218760)
;;  (LEVEL10.PROOFP
;;       FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-NEGATIVE-LIT-FROM-PEQUAL-NIL
;;       586569)
;;  (LEVEL11.PROOFP
;;       FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-NEGATIVE-LIT-FROM-PEQUAL-NIL
;;       600090)
;;  (LEVEL2.PROOFP
;;       FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-NEGATIVE-LIT-FROM-PEQUAL-NIL
;;       1465619)
;;  (LEVEL3.PROOFP
;;       FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-NEGATIVE-LIT-FROM-PEQUAL-NIL
;;       721025)
;;  (LEVEL4.PROOFP
;;       FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-NEGATIVE-LIT-FROM-PEQUAL-NIL
;;       365949)
;;  (LEVEL5.PROOFP
;;       FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-NEGATIVE-LIT-FROM-PEQUAL-NIL
;;       334504)
;;  (LEVEL6.PROOFP
;;       FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-NEGATIVE-LIT-FROM-PEQUAL-NIL
;;       334504)
;;  (LEVEL7.PROOFP
;;       FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-NEGATIVE-LIT-FROM-PEQUAL-NIL
;;       334504)
;;  (LEVEL8.PROOFP
;;       FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-NEGATIVE-LIT-FROM-PEQUAL-NIL
;;       592816)
;;  (LEVEL9.PROOFP
;;       FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-NEGATIVE-LIT-FROM-PEQUAL-NIL
;;       586376)
;;  (LOGIC.PROOFP
;;       FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-NEGATIVE-LIT-FROM-PEQUAL-NIL
;;       10345413)
;;  (LEVEL10.PROOFP FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-TRANSITIVITY-OF-IFF
;;                  58643629)
;;  (LEVEL11.PROOFP FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-TRANSITIVITY-OF-IFF
;;                  58670026)
;;  (LEVEL2.PROOFP FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-TRANSITIVITY-OF-IFF
;;                 408753676)
;;  (LEVEL3.PROOFP FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-TRANSITIVITY-OF-IFF
;;                 218777972)
;;  (LEVEL4.PROOFP FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-TRANSITIVITY-OF-IFF
;;                 52578550)
;;  (LEVEL5.PROOFP FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-TRANSITIVITY-OF-IFF
;;                 44103994)
;;  (LEVEL6.PROOFP FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-TRANSITIVITY-OF-IFF
;;                 29091881)
;;  (LEVEL7.PROOFP FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-TRANSITIVITY-OF-IFF
;;                 27036162)
;;  (LEVEL8.PROOFP FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-TRANSITIVITY-OF-IFF
;;                 58661507)
;;  (LEVEL9.PROOFP FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-TRANSITIVITY-OF-IFF
;;                 58639725)
;;  (LOGIC.PROOFP FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-TRANSITIVITY-OF-IFF
;;                3491784272)
;;  (LEVEL10.PROOFP FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;;                  2002070)
;;  (LEVEL11.PROOFP FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;;                  1927685)
;;  (LEVEL2.PROOFP FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;;                 63495138)
;;  (LEVEL3.PROOFP FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;;                 33861782)
;;  (LEVEL4.PROOFP FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;;                 6806516)
;;  (LEVEL5.PROOFP FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;;                 4845556)
;;  (LEVEL6.PROOFP FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;;                 2257161)
;;  (LEVEL7.PROOFP FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;;                 2024643)
;;  (LEVEL8.PROOFP FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;;                 2029213)
;;  (LEVEL9.PROOFP FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;;                 1988318)
;;  (LOGIC.PROOFP FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;;                548911438)
;;  (LEVEL10.PROOFP
;;     FORCING-LOGIC.PROOFP-OF-CLAUSE.DISJOINED-SUBSTITUTE-IFF-INTO-LITERAL-BLDR
;;     10548888)
;;  (LEVEL11.PROOFP
;;     FORCING-LOGIC.PROOFP-OF-CLAUSE.DISJOINED-SUBSTITUTE-IFF-INTO-LITERAL-BLDR
;;     10490631)
;;  (LEVEL2.PROOFP
;;     FORCING-LOGIC.PROOFP-OF-CLAUSE.DISJOINED-SUBSTITUTE-IFF-INTO-LITERAL-BLDR
;;     1537111835)
;;  (LEVEL3.PROOFP
;;     FORCING-LOGIC.PROOFP-OF-CLAUSE.DISJOINED-SUBSTITUTE-IFF-INTO-LITERAL-BLDR
;;     862118740)
;;  (LEVEL4.PROOFP
;;     FORCING-LOGIC.PROOFP-OF-CLAUSE.DISJOINED-SUBSTITUTE-IFF-INTO-LITERAL-BLDR
;;     135627663)
;;  (LEVEL5.PROOFP
;;     FORCING-LOGIC.PROOFP-OF-CLAUSE.DISJOINED-SUBSTITUTE-IFF-INTO-LITERAL-BLDR
;;     103002504)
;;  (LEVEL6.PROOFP
;;     FORCING-LOGIC.PROOFP-OF-CLAUSE.DISJOINED-SUBSTITUTE-IFF-INTO-LITERAL-BLDR
;;     33821445)
;;  (LEVEL7.PROOFP
;;     FORCING-LOGIC.PROOFP-OF-CLAUSE.DISJOINED-SUBSTITUTE-IFF-INTO-LITERAL-BLDR
;;     25821804)
;;  (LEVEL8.PROOFP
;;     FORCING-LOGIC.PROOFP-OF-CLAUSE.DISJOINED-SUBSTITUTE-IFF-INTO-LITERAL-BLDR
;;     10573491)
;;  (LEVEL9.PROOFP
;;     FORCING-LOGIC.PROOFP-OF-CLAUSE.DISJOINED-SUBSTITUTE-IFF-INTO-LITERAL-BLDR
;;     10535724)
;;  (LOGIC.PROOFP
;;     FORCING-LOGIC.PROOFP-OF-CLAUSE.DISJOINED-SUBSTITUTE-IFF-INTO-LITERAL-BLDR
;;     13175548486)
;;  (LEVEL10.PROOFP
;;       LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-UPDATE-CLAUSE-BLDR
;;       288974)
;;  (LEVEL11.PROOFP
;;       LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-UPDATE-CLAUSE-BLDR
;;       269611)
;;  (LEVEL2.PROOFP
;;       LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-UPDATE-CLAUSE-BLDR
;;       11644)
;;  (LEVEL3.PROOFP
;;       LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-UPDATE-CLAUSE-BLDR
;;       2233102)
;;  (LEVEL4.PROOFP
;;       LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-UPDATE-CLAUSE-BLDR
;;       1044698)
;;  (LEVEL5.PROOFP
;;       LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-UPDATE-CLAUSE-BLDR
;;       831077)
;;  (LEVEL6.PROOFP
;;       LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-UPDATE-CLAUSE-BLDR
;;       603458)
;;  (LEVEL7.PROOFP
;;       LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-UPDATE-CLAUSE-BLDR
;;       420481)
;;  (LEVEL8.PROOFP
;;       LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-UPDATE-CLAUSE-BLDR
;;       320978)
;;  (LEVEL9.PROOFP
;;       LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-UPDATE-CLAUSE-BLDR
;;       288405)
;;  (LOGIC.PROOFP
;;       LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-UPDATE-CLAUSE-BLDR
;;       73072)
;;  (LEVEL10.PROOFP LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-GENERIC-EVALUATOR-BLDR
;;                  359554)
;;  (LEVEL11.PROOFP LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-GENERIC-EVALUATOR-BLDR
;;                  271017)
;;  (LEVEL2.PROOFP LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-GENERIC-EVALUATOR-BLDR
;;                 19653560)
;;  (LEVEL3.PROOFP LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-GENERIC-EVALUATOR-BLDR
;;                 9142242)
;;  (LEVEL4.PROOFP LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-GENERIC-EVALUATOR-BLDR
;;                 3088482)
;;  (LEVEL5.PROOFP LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-GENERIC-EVALUATOR-BLDR
;;                 2370091)
;;  (LEVEL6.PROOFP LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-GENERIC-EVALUATOR-BLDR
;;                 1314330)
;;  (LEVEL7.PROOFP LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-GENERIC-EVALUATOR-BLDR
;;                 462773)
;;  (LEVEL8.PROOFP LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-GENERIC-EVALUATOR-BLDR
;;                 448562)
;;  (LEVEL9.PROOFP LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-GENERIC-EVALUATOR-BLDR
;;                 359258)
;;  (LOGIC.PROOFP LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-GENERIC-EVALUATOR-BLDR
;;                164627444))