CMU Common Lisp 19f (19F), running on nemesis.cs.utexas.edu
With core: /v/filer4b/v11q002/acl2space/jared/Milawa/Sources/level5.nemesis-cmucl
Dumped on: Thu, 2009-10-29 11:19:34-05:00 on nemesis.cs.utexas.edu
See for support information.
Loaded subsystems:
Python 1.1, target Intel x86
CLOS based on Gerd's PCL 2008-11-12 16:36:41
Milawa Proof Checker.
8082> DEFINE CLAUSE.FLAG-SIMPLE-TERMP
;; Reading from Proofs/level6/admit-clause.flag-simple-termp.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.28 seconds
; Compiling LAMBDA (FLAG X):
; Compiling Top-Level Form:
;; DEFINE took 0.34 seconds
8083> VERIFY CLAUSE.FLAG-SIMPLE-TERMP
;; Reading from Proofs/level6/thm-clause.flag-simple-termp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8084> DEFINE CLAUSE.SIMPLE-TERMP
;; Reading from Proofs/level6/admit-clause.simple-termp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.00 seconds
8085> VERIFY CLAUSE.SIMPLE-TERMP
;; Reading from Proofs/level6/thm-clause.simple-termp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.03 seconds
8086> DEFINE CLAUSE.SIMPLE-TERM-LISTP
;; Reading from Proofs/level6/admit-clause.simple-term-listp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8087> VERIFY CLAUSE.SIMPLE-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.simple-term-listp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.03 seconds
8088> VERIFY DEFINITION-OF-CLAUSE.SIMPLE-TERMP
;; Reading from Proofs/level6/thm-definition-of-clause.simple-termp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.37 seconds
;; VERIFY took 0.43 seconds
8089> VERIFY DEFINITION-OF-CLAUSE.SIMPLE-TERM-LISTP
;; Reading from Proofs/level6/thm-definition-of-clause.simple-term-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.09 seconds
8090> VERIFY CLAUSE.FLAG-SIMPLE-TERMP-OF-TERM-REMOVAL
;; Reading from Proofs/level6/thm-clause.flag-simple-termp-of-term-removal.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8091> VERIFY CLAUSE.FLAG-SIMPLE-TERMP-OF-LIST-REMOVAL
;; Reading from Proofs/level6/thm-clause.flag-simple-termp-of-list-removal.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8092> VERIFY CLAUSE.SIMPLE-TERMP-WHEN-LOGIC.VARIABLEP
;; Reading from Proofs/level6/thm-clause.simple-termp-when-logic.variablep.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.06 seconds
8093> VERIFY CLAUSE.SIMPLE-TERMP-WHEN-LOGIC.CONSTANTP
;; Reading from Proofs/level6/thm-clause.simple-termp-when-logic.constantp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8094> VERIFY CLAUSE.SIMPLE-TERMP-WHEN-NON-IF-LOGIC.FUNCTIONP
;; Reading from Proofs/level6/thm-clause.simple-termp-when-non-if-logic.functionp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.12 seconds
8095> VERIFY CLAUSE.SIMPLE-TERMP-WHEN-BAD-ARGS-LOGIC.FUNCTIONP
;; Reading from Proofs/level6/thm-clause.simple-termp-when-bad-args-logic.functionp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.12 seconds
8096> VERIFY CLAUSE.SIMPLE-TERMP-WHEN-IF-LOGIC.FUNCTIONP
;; Reading from Proofs/level6/thm-clause.simple-termp-when-if-logic.functionp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.07 seconds
8097> VERIFY CLAUSE.SIMPLE-TERMP-WHEN-LOGIC.LAMBDAP
;; Reading from Proofs/level6/thm-clause.simple-termp-when-logic.lambdap.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.16 seconds
8098> VERIFY CLAUSE.SIMPLE-TERMP-WHEN-DEGENERATE
;; Reading from Proofs/level6/thm-clause.simple-termp-when-degenerate.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.09 seconds
8099> VERIFY CLAUSE.SIMPLE-TERM-LISTP-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-clause.simple-term-listp-when-not-consp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 seconds
8100> VERIFY CLAUSE.SIMPLE-TERM-LISTP-OF-CONS
;; Reading from Proofs/level6/thm-clause.simple-term-listp-of-cons.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8101> VERIFY LEMMA-FOR-BOOLEANP-OF-CLAUSE.SIMPLE-TERMP
;; Reading from Proofs/level6/thm-lemma-for-booleanp-of-clause.simple-termp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.97 seconds
;; VERIFY took 1.07 seconds
8102> VERIFY BOOLEANP-OF-CLAUSE.SIMPLE-TERMP
;; Reading from Proofs/level6/thm-booleanp-of-clause.simple-termp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.07 seconds
8103> VERIFY BOOLEANP-OF-CLAUSE.SIMPLE-TERM-LISTP
;; Reading from Proofs/level6/thm-booleanp-of-clause.simple-term-listp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.06 seconds
8104> VERIFY CLAUSE.SIMPLE-TERM-LISTP-OF-LIST-FIX
;; Reading from Proofs/level6/thm-clause.simple-term-listp-of-list-fix.proof
;; Reading the file took 0.01 seconds
; [GC threshold exceeded with 12,015,800 bytes in use. Commencing GC.]
; [GC completed with 757,416 bytes retained and 11,258,384 bytes freed.]
; [GC will next occur when at least 12,757,416 bytes are in use.]
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.22 seconds
8105> VERIFY CLAUSE.SIMPLE-TERM-LISTP-OF-APP
;; Reading from Proofs/level6/thm-clause.simple-term-listp-of-app.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.30 seconds
;; VERIFY took 0.33 seconds
8106> VERIFY CLAUSE.SIMPLE-TERM-LISTP-OF-REV
;; Reading from Proofs/level6/thm-clause.simple-term-listp-of-rev.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.24 seconds
8107> VERIFY CLAUSE.SIMPLE-TERMP-OF-CAR-WHEN-CLAUSE.SIMPLE-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.simple-termp-of-car-when-clause.simple-term-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.07 seconds
8108> VERIFY CLAUSE.SIMPLE-TERM-LISTP-OF-CDR-WHEN-CLAUSE.SIMPLE-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.simple-term-listp-of-cdr-when-clause.simple-term-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.07 seconds
8109> VERIFY CLAUSE.SIMPLE-TERMP-WHEN-MEMBERP-OF-CLAUSE.SIMPLE-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.simple-termp-when-memberp-of-clause.simple-term-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.17 seconds
8110> VERIFY CLAUSE.SIMPLE-TERMP-WHEN-MEMBERP-OF-CLAUSE.SIMPLE-TERM-LISTP-ALT
;; Reading from Proofs/level6/thm-clause.simple-termp-when-memberp-of-clause.simple-term-listp-alt.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.06 seconds
8111> VERIFY CLAUSE.SIMPLE-TERM-LISTP-OF-REMOVE-ALL-WHEN-CLAUSE.SIMPLE-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.simple-term-listp-of-remove-all-when-clause.simple-term-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.17 seconds
8112> VERIFY CLAUSE.SIMPLE-TERM-LISTP-OF-REMOVE-DUPLICATES
;; Reading from Proofs/level6/thm-clause.simple-term-listp-of-remove-duplicates.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.24 seconds
8113> VERIFY CLAUSE.SIMPLE-TERM-LISTP-OF-DIFFERENCE-WHEN-CLAUSE.SIMPLE-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.simple-term-listp-of-difference-when-clause.simple-term-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.17 seconds
8114> VERIFY CLAUSE.SIMPLE-TERM-LISTP-OF-SUBSETP-WHEN-CLAUSE.SIMPLE-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.simple-term-listp-of-subsetp-when-clause.simple-term-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.18 seconds
8115> VERIFY CLAUSE.SIMPLE-TERM-LISTP-OF-SUBSETP-WHEN-CLAUSE.SIMPLE-TERM-LISTP-ALT
;; Reading from Proofs/level6/thm-clause.simple-term-listp-of-subsetp-when-clause.simple-term-listp-alt.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
8116> VERIFY CLAUSE.SIMPLE-TERM-LISTP-OF-REPEAT
;; Reading from Proofs/level6/thm-clause.simple-term-listp-of-repeat.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.21 seconds
8117> VERIFY CLAUSE.SIMPLE-TERM-LISTP-WHEN-LENGTH-THREE
;; Reading from Proofs/level6/thm-clause.simple-term-listp-when-length-three.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.23 seconds
8118> DEFINE CLAUSE.SIMPLE-TERM-LIST-LISTP
;; Reading from Proofs/level6/admit-clause.simple-term-list-listp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.09 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.10 seconds
8119> VERIFY CLAUSE.SIMPLE-TERM-LIST-LISTP
;; Reading from Proofs/level6/thm-clause.simple-term-list-listp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.03 seconds
8120> VERIFY CLAUSE.SIMPLE-TERM-LIST-LISTP-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-clause.simple-term-list-listp-when-not-consp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8121> VERIFY CLAUSE.SIMPLE-TERM-LIST-LISTP-OF-CONS
;; Reading from Proofs/level6/thm-clause.simple-term-list-listp-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8122> VERIFY BOOLEANP-OF-CLAUSE.SIMPLE-TERM-LIST-LISTP
;; Reading from Proofs/level6/thm-booleanp-of-clause.simple-term-list-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.13 seconds
8123> VERIFY CLAUSE.SIMPLE-TERM-LIST-LISTP-OF-LIST-FIX
;; Reading from Proofs/level6/thm-clause.simple-term-list-listp-of-list-fix.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.20 seconds
8124> VERIFY CLAUSE.SIMPLE-TERM-LIST-LISTP-OF-APP
;; Reading from Proofs/level6/thm-clause.simple-term-list-listp-of-app.proof
; [GC threshold exceeded with 12,819,728 bytes in use. Commencing GC.]
; [GC completed with 288,384 bytes retained and 12,531,344 bytes freed.]
; [GC will next occur when at least 12,288,384 bytes are in use.]
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.30 seconds
;; VERIFY took 0.34 seconds
8125> VERIFY CLAUSE.SIMPLE-TERM-LIST-LISTP-OF-REV
;; Reading from Proofs/level6/thm-clause.simple-term-list-listp-of-rev.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.21 seconds
8126> VERIFY CLAUSE.SIMPLE-TERM-LISTP-OF-CAR-WHEN-CLAUSE.SIMPLE-TERM-LIST-LISTP
;; Reading from Proofs/level6/thm-clause.simple-term-listp-of-car-when-clause.simple-term-list-listp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.06 seconds
8127> VERIFY CLAUSE.SIMPLE-TERM-LIST-LISTP-OF-CDR-WHEN-CLAUSE.SIMPLE-TERM-LIST-LISTP
;; Reading from Proofs/level6/thm-clause.simple-term-list-listp-of-cdr-when-clause.simple-term-list-listp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8128> VERIFY CLAUSE.SIMPLE-TERM-LISTP-WHEN-MEMBERP-OF-CLAUSE.SIMPLE-TERM-LIST-LISTP
;; Reading from Proofs/level6/thm-clause.simple-term-listp-when-memberp-of-clause.simple-term-list-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.19 seconds
8129> VERIFY CLAUSE.SIMPLE-TERM-LISTP-WHEN-MEMBERP-OF-CLAUSE.SIMPLE-TERM-LIST-LISTP-ALT
;; Reading from Proofs/level6/thm-clause.simple-term-listp-when-memberp-of-clause.simple-term-list-listp-alt.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8130> VERIFY CLAUSE.SIMPLE-TERM-LIST-LISTP-OF-REMOVE-ALL-WHEN-CLAUSE.SIMPLE-TERM-LIST-LISTP
;; Reading from Proofs/level6/thm-clause.simple-term-list-listp-of-remove-all-when-clause.simple-term-list-listp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.20 seconds
8131> VERIFY CLAUSE.SIMPLE-TERM-LIST-LISTP-OF-REMOVE-DUPLICATES
;; Reading from Proofs/level6/thm-clause.simple-term-list-listp-of-remove-duplicates.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.23 seconds
8132> VERIFY CLAUSE.SIMPLE-TERM-LIST-LISTP-OF-DIFFERENCE-WHEN-CLAUSE.SIMPLE-TERM-LIST-LISTP
;; Reading from Proofs/level6/thm-clause.simple-term-list-listp-of-difference-when-clause.simple-term-list-listp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.16 seconds
8133> VERIFY CLAUSE.SIMPLE-TERM-LIST-LISTP-OF-SUBSETP-WHEN-CLAUSE.SIMPLE-TERM-LIST-LISTP
;; Reading from Proofs/level6/thm-clause.simple-term-list-listp-of-subsetp-when-clause.simple-term-list-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.20 seconds
8134> VERIFY CLAUSE.SIMPLE-TERM-LIST-LISTP-OF-SUBSETP-WHEN-CLAUSE.SIMPLE-TERM-LIST-LISTP-ALT
;; Reading from Proofs/level6/thm-clause.simple-term-list-listp-of-subsetp-when-clause.simple-term-list-listp-alt.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8135> VERIFY CLAUSE.SIMPLE-TERM-LIST-LISTP-OF-REPEAT
;; Reading from Proofs/level6/thm-clause.simple-term-list-listp-of-repeat.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.21 seconds
8136> DEFINE CLAUSE.LIFTED-TERMP
;; Reading from Proofs/level6/admit-clause.lifted-termp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.23 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.25 seconds
8137> VERIFY CLAUSE.LIFTED-TERMP
;; Reading from Proofs/level6/thm-clause.lifted-termp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8138> VERIFY CLAUSE.LIFTED-TERMP-WHEN-LOGIC.CONSTANTP
;; Reading from Proofs/level6/thm-clause.lifted-termp-when-logic.constantp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.07 seconds
8139> VERIFY CLAUSE.LIFTED-TERMP-WHEN-LOGIC.VARIABLEP
;; Reading from Proofs/level6/thm-clause.lifted-termp-when-logic.variablep.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.08 seconds
8140> VERIFY CLAUSE.LIFTED-TERMP-WHEN-NOT-IF
;; Reading from Proofs/level6/thm-clause.lifted-termp-when-not-if.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.16 seconds
8141> VERIFY CLAUSE.LIFTED-TERMP-WHEN-BAD-ARGS-LOGIC.FUNCTIONP
;; Reading from Proofs/level6/thm-clause.lifted-termp-when-bad-args-logic.functionp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.17 seconds
8142> VERIFY CLAUSE.LIFTED-TERMP-WHEN-IF-LOGIC.FUNCTIONP
;; Reading from Proofs/level6/thm-clause.lifted-termp-when-if-logic.functionp.proof
;; Reading the file took 0.01 seconds
; [GC threshold exceeded with 12,301,248 bytes in use. Commencing GC.]
; [GC completed with 1,057,048 bytes retained and 11,244,200 bytes freed.]
; [GC will next occur when at least 13,057,048 bytes are in use.]
;; Checking the proof took 0.36 seconds
;; VERIFY took 0.40 seconds
8143> VERIFY CLAUSE.LIFTED-TERMP-WHEN-IF-LOGIC.LAMBDAP
;; Reading from Proofs/level6/thm-clause.lifted-termp-when-if-logic.lambdap.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.25 seconds
8144> VERIFY CLAUSE.LIFTED-TERMP-WHEN-DEGENERATE
;; Reading from Proofs/level6/thm-clause.lifted-termp-when-degenerate.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.10 seconds
8145> VERIFY CLAUSE.LIFTED-TERMP-WHEN-CLAUSE.SIMPLE-TERMP
;; Reading from Proofs/level6/thm-clause.lifted-termp-when-clause.simple-termp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.65 seconds
;; VERIFY took 0.73 seconds
8146> VERIFY BOOLEANP-OF-CLAUSE.LIFTED-TERMP
;; Reading from Proofs/level6/thm-booleanp-of-clause.lifted-termp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.38 seconds
;; VERIFY took 0.42 seconds
8147> DEFINE CLAUSE.LIFTED-TERM-LISTP
;; Reading from Proofs/level6/admit-clause.lifted-term-listp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.08 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.09 seconds
8148> VERIFY CLAUSE.LIFTED-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.lifted-term-listp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.03 seconds
8149> VERIFY CLAUSE.LIFTED-TERM-LISTP-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-clause.lifted-term-listp-when-not-consp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 seconds
8150> VERIFY CLAUSE.LIFTED-TERM-LISTP-OF-CONS
;; Reading from Proofs/level6/thm-clause.lifted-term-listp-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8151> VERIFY BOOLEANP-OF-CLAUSE.LIFTED-TERM-LISTP
;; Reading from Proofs/level6/thm-booleanp-of-clause.lifted-term-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.13 seconds
8152> VERIFY CLAUSE.LIFTED-TERM-LISTP-OF-LIST-FIX
;; Reading from Proofs/level6/thm-clause.lifted-term-listp-of-list-fix.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.20 seconds
8153> VERIFY CLAUSE.LIFTED-TERM-LISTP-OF-APP
;; Reading from Proofs/level6/thm-clause.lifted-term-listp-of-app.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.30 seconds
;; VERIFY took 0.33 seconds
8154> VERIFY CLAUSE.LIFTED-TERM-LISTP-OF-REV
;; Reading from Proofs/level6/thm-clause.lifted-term-listp-of-rev.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.21 seconds
8155> VERIFY CLAUSE.LIFTED-TERMP-OF-CAR-WHEN-CLAUSE.LIFTED-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.lifted-termp-of-car-when-clause.lifted-term-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.07 seconds
8156> VERIFY CLAUSE.LIFTED-TERM-LISTP-OF-CDR-WHEN-CLAUSE.LIFTED-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.lifted-term-listp-of-cdr-when-clause.lifted-term-listp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.06 seconds
8157> VERIFY CLAUSE.LIFTED-TERMP-WHEN-MEMBERP-OF-CLAUSE.LIFTED-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.lifted-termp-when-memberp-of-clause.lifted-term-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.17 seconds
8158> VERIFY CLAUSE.LIFTED-TERMP-WHEN-MEMBERP-OF-CLAUSE.LIFTED-TERM-LISTP-ALT
;; Reading from Proofs/level6/thm-clause.lifted-termp-when-memberp-of-clause.lifted-term-listp-alt.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8159> VERIFY CLAUSE.LIFTED-TERM-LISTP-OF-REMOVE-ALL-WHEN-CLAUSE.LIFTED-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.lifted-term-listp-of-remove-all-when-clause.lifted-term-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.17 seconds
8160> VERIFY CLAUSE.LIFTED-TERM-LISTP-OF-REMOVE-DUPLICATES
;; Reading from Proofs/level6/thm-clause.lifted-term-listp-of-remove-duplicates.proof
; [GC threshold exceeded with 13,067,720 bytes in use. Commencing GC.]
; [GC completed with 828,392 bytes retained and 12,239,328 bytes freed.]
; [GC will next occur when at least 12,828,392 bytes are in use.]
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.25 seconds
8161> VERIFY CLAUSE.LIFTED-TERM-LISTP-OF-DIFFERENCE-WHEN-CLAUSE.LIFTED-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.lifted-term-listp-of-difference-when-clause.lifted-term-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.16 seconds
8162> VERIFY CLAUSE.LIFTED-TERM-LISTP-OF-SUBSETP-WHEN-CLAUSE.LIFTED-TERM-LISTP
;; Reading from Proofs/level6/thm-clause.lifted-term-listp-of-subsetp-when-clause.lifted-term-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.19 seconds
8163> VERIFY CLAUSE.LIFTED-TERM-LISTP-OF-SUBSETP-WHEN-CLAUSE.LIFTED-TERM-LISTP-ALT
;; Reading from Proofs/level6/thm-clause.lifted-term-listp-of-subsetp-when-clause.lifted-term-listp-alt.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
8164> VERIFY CLAUSE.LIFTED-TERM-LISTP-OF-REPEAT
;; Reading from Proofs/level6/thm-clause.lifted-term-listp-of-repeat.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.21 seconds
8165> VERIFY LEMMA-SPLIT-UP-LIST-OF-QUOTED-NIL
;; Reading from Proofs/level6/thm-lemma-split-up-list-of-quoted-nil.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.10 seconds
8166> DEFINE CLAUSE.SIMPLE-NEGATIVEP
;; Reading from Proofs/level6/admit-clause.simple-negativep.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.00 seconds
8167> VERIFY CLAUSE.SIMPLE-NEGATIVEP
;; Reading from Proofs/level6/thm-clause.simple-negativep.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8168> DEFINE CLAUSE.SIMPLE-NEGATIVE-GUTS
;; Reading from Proofs/level6/admit-clause.simple-negative-guts.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8169> VERIFY CLAUSE.SIMPLE-NEGATIVE-GUTS
;; Reading from Proofs/level6/thm-clause.simple-negative-guts.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.03 seconds
8170> VERIFY BOOLEANP-OF-CLAUSE.SIMPLE-NEGATIVEP
;; Reading from Proofs/level6/thm-booleanp-of-clause.simple-negativep.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.07 seconds
8171> VERIFY FORCING-LOGIC.TERMP-OF-CLAUSE.SIMPLE-NEGATIVE-GUTS
;; Reading from Proofs/level6/thm-forcing-logic.termp-of-clause.simple-negative-guts.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.06 seconds
8172> VERIFY FORCING-LOGIC.TERM-ATBLP-OF-CLAUSE.SIMPLE-NEGATIVE-GUTS
;; Reading from Proofs/level6/thm-forcing-logic.term-atblp-of-clause.simple-negative-guts.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.07 seconds
8173> VERIFY CLAUSE.SIMPLE-NEGATIVEP-OF-LOGIC.FUNCTION-OF-NOT
;; Reading from Proofs/level6/thm-clause.simple-negativep-of-logic.function-of-not.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.06 seconds
8174> VERIFY CLAUSE.NEGATIVE-TERMP-WHEN-CLAUSE.SIMPLE-NEGATIVEP
;; Reading from Proofs/level6/thm-clause.negative-termp-when-clause.simple-negativep.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.28 seconds
;; VERIFY took 0.31 seconds
8175> VERIFY CLAUSE.SIMPLE-NEGATIVE-GUTS-OF-LOGIC.FUNCTION-OF-NOT
;; Reading from Proofs/level6/thm-clause.simple-negative-guts-of-logic.function-of-not.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8176> VERIFY CLAUSE.SIMPLE-NEGATIVE-GUTS-IDENTITY
;; Reading from Proofs/level6/thm-clause.simple-negative-guts-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.08 seconds
8177> VERIFY FORCING-CLAUSE.SIMPLE-NEGATIVE-GUTS-UNDER-IFF
;; Reading from Proofs/level6/thm-forcing-clause.simple-negative-guts-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 seconds
8178> DEFINE CLAUSE.DOUBLE-NEGATIVE-FREE-LISTP
;; Reading from Proofs/level6/admit-clause.double-negative-free-listp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.11 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.11 seconds
8179> VERIFY CLAUSE.DOUBLE-NEGATIVE-FREE-LISTP
;; Reading from Proofs/level6/thm-clause.double-negative-free-listp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8180> VERIFY CLAUSE.DOUBLE-NEGATIVE-FREE-LISTP-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-clause.double-negative-free-listp-when-not-consp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8181> VERIFY CLAUSE.DOUBLE-NEGATIVE-FREE-LISTP-OF-CONS
;; Reading from Proofs/level6/thm-clause.double-negative-free-listp-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.11 seconds
8182> VERIFY BOOLEANP-OF-CLAUSE.DOUBLE-NEGATIVE-FREE-LISTP
;; Reading from Proofs/level6/thm-booleanp-of-clause.double-negative-free-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.13 seconds
8183> VERIFY CLAUSE.DOUBLE-NEGATIVE-FREE-LISTP-OF-LIST-FIX
;; Reading from Proofs/level6/thm-clause.double-negative-free-listp-of-list-fix.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.23 seconds
8184> VERIFY CLAUSE.DOUBLE-NEGATIVE-FREE-LISTP-OF-APP
;; Reading from Proofs/level6/thm-clause.double-negative-free-listp-of-app.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.34 seconds
;; VERIFY took 0.38 seconds
8185> VERIFY CLAUSE.DOUBLE-NEGATIVE-FREE-LISTP-OF-REV
;; Reading from Proofs/level6/thm-clause.double-negative-free-listp-of-rev.proof
; [GC threshold exceeded with 12,840,336 bytes in use. Commencing GC.]
; [GC completed with 1,193,840 bytes retained and 11,646,496 bytes freed.]
; [GC will next occur when at least 13,193,840 bytes are in use.]
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.25 seconds
8186> DEFINE CLAUSE.COMPLEMENT-TERM
;; Reading from Proofs/level6/admit-clause.complement-term.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A):
; Compiling Top-Level Form:
;; DEFINE took 0.00 seconds
8187> VERIFY CLAUSE.COMPLEMENT-TERM
;; Reading from Proofs/level6/thm-clause.complement-term.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8188> VERIFY LOGIC.TERMP-OF-CLAUSE.COMPLEMENT-TERM
;; Reading from Proofs/level6/thm-logic.termp-of-clause.complement-term.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.08 seconds
8189> VERIFY CLAUSE.COMPLEMENT-TERM-OF-CLAUSE.COMPLEMENT-TERM
;; Reading from Proofs/level6/thm-clause.complement-term-of-clause.complement-term.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.10 seconds
8190> DEFINE CLAUSE.FIND-COMPLEMENTARY-LITERAL
;; Reading from Proofs/level6/admit-clause.find-complementary-literal.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.09 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.09 seconds
8191> VERIFY CLAUSE.FIND-COMPLEMENTARY-LITERAL
;; Reading from Proofs/level6/thm-clause.find-complementary-literal.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8192> VERIFY CLAUSE.FIND-COMPLEMENTARY-LITERAL-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-clause.find-complementary-literal-when-not-consp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 seconds
8193> VERIFY CLAUSE.FIND-COMPLEMENTARY-LITERAL-OF-CONS
;; Reading from Proofs/level6/thm-clause.find-complementary-literal-of-cons.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.07 seconds
8194> VERIFY FORCING-MEMBERP-OF-CLAUSE.FIND-COMPLEMENTARY-LITERAL
;; Reading from Proofs/level6/thm-forcing-memberp-of-clause.find-complementary-literal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 0.26 seconds
8195> VERIFY FORCING-MEMBERP-OF-NOT-OF-CLAUSE.FIND-COMPLEMENTARY-LITERAL
;; Reading from Proofs/level6/thm-forcing-memberp-of-not-of-clause.find-complementary-literal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.28 seconds
8196> VERIFY CLAUSE.FIND-COMPLEMENTARY-LITERAL-OF-LIST-FIX
;; Reading from Proofs/level6/thm-clause.find-complementary-literal-of-list-fix.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.12 seconds
8197> VERIFY FORCING-CLAUSE.FIND-COMPLEMENTARY-LITERAL-OF-APP-ONE
;; Reading from Proofs/level6/thm-forcing-clause.find-complementary-literal-of-app-one.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.28 seconds
;; VERIFY took 0.32 seconds
8198> VERIFY LEMMA-FOR-CLAUSE.FIND-COMPLEMENTARY-LITERAL-OF-REV
;; Reading from Proofs/level6/thm-lemma-for-clause.find-complementary-literal-of-rev.proof
;; Reading the file took 0.08 seconds
; [GC threshold exceeded with 13,200,744 bytes in use. Commencing GC.]
; [GC completed with 2,094,416 bytes retained and 11,106,328 bytes freed.]
; [GC will next occur when at least 14,094,416 bytes are in use.]
;; Checking the proof took 3.23 seconds
;; VERIFY took 3.61 seconds
8199> VERIFY CLAUSE.FIND-COMPLEMENTARY-LITERAL-OF-REV
;; Reading from Proofs/level6/thm-clause.find-complementary-literal-of-rev.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.72 seconds
;; VERIFY took 0.80 seconds
8200> DEFINE CLAUSE.REMOVE-COMPLEMENT-CLAUSES
;; Reading from Proofs/level6/admit-clause.remove-complement-clauses.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.13 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.15 seconds
8201> VERIFY CLAUSE.REMOVE-COMPLEMENT-CLAUSES
;; Reading from Proofs/level6/thm-clause.remove-complement-clauses.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.03 seconds
8202> VERIFY CLAUSE.REMOVE-COMPLEMENT-CLAUSES-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-clause.remove-complement-clauses-when-not-consp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
8203> VERIFY CLAUSE.REMOVE-COMPLEMENT-CLAUSES-OF-CONS
;; Reading from Proofs/level6/thm-clause.remove-complement-clauses-of-cons.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.12 seconds
8204> VERIFY FORCING-LOGIC.TERM-LIST-LISTP-OF-CLAUSE.REMOVE-COMPLEMENT-CLAUSES
;; Reading from Proofs/level6/thm-forcing-logic.term-list-listp-of-clause.remove-complement-clauses.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.18 seconds
8205> VERIFY FORCING-LOGIC.TERM-LIST-LIST-ATBLP-OF-CLAUSE.REMOVE-COMPLEMENT-CLAUSES
;; Reading from Proofs/level6/thm-forcing-logic.term-list-list-atblp-of-clause.remove-complement-clauses.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.19 seconds
8206> VERIFY CONS-LISTP-OF-CLAUSE.REMOVE-COMPLEMENT-CLAUSES
;; Reading from Proofs/level6/thm-cons-listp-of-clause.remove-complement-clauses.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 0.26 seconds
8207> VERIFY TRUE-LISTP-OF-CLAUSE.REMOVE-COMPLEMENT-CLAUSES
;; Reading from Proofs/level6/thm-true-listp-of-clause.remove-complement-clauses.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.13 seconds
8208> VERIFY CLAUSE.REMOVE-COMPLEMENT-CLAUSES-OF-LIST-FIX
;; Reading from Proofs/level6/thm-clause.remove-complement-clauses-of-list-fix.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.13 seconds
8209> VERIFY CLAUSE.REMOVE-COMPLEMENT-CLAUSES-OF-APP
;; Reading from Proofs/level6/thm-clause.remove-complement-clauses-of-app.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.16 seconds
8210> VERIFY REV-OF-CLAUSE.REMOVE-COMPLEMENT-CLAUSES
;; Reading from Proofs/level6/thm-rev-of-clause.remove-complement-clauses.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.18 seconds
8211> VERIFY CLAUSE.REMOVE-COMPLEMENT-CLAUSES-OF-REV
;; Reading from Proofs/level6/thm-clause.remove-complement-clauses-of-rev.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 seconds
8212> DEFINE CLAUSE.COMPLEMENT-CLAUSE-BLDR
;; Reading from Proofs/level6/admit-clause.complement-clause-bldr.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A X):
; Compiling Top-Level Form:
;; DEFINE took 0.00 seconds
8213> VERIFY CLAUSE.COMPLEMENT-CLAUSE-BLDR
;; Reading from Proofs/level6/thm-clause.complement-clause-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.03 seconds
8214> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.COMPLEMENT-CLAUSE-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.appealp-of-clause.complement-clause-bldr.proof
; [GC threshold exceeded with 14,104,616 bytes in use. Commencing GC.]
; [GC completed with 2,708,568 bytes retained and 11,396,048 bytes freed.]
; [GC will next occur when at least 14,708,568 bytes are in use.]
;; Reading the file took 0.08 seconds
;; Checking the proof took 9.12 seconds
;; VERIFY took 9.67 seconds
8215> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.COMPLEMENT-CLAUSE-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.conclusion-of-clause.complement-clause-bldr.proof
; [GC threshold exceeded with 15,676,328 bytes in use. Commencing GC.]
; [GC completed with 2,114,856 bytes retained and 13,561,472 bytes freed.]
; [GC will next occur when at least 14,114,856 bytes are in use.]
;; Reading the file took 0.10 seconds
;; Checking the proof took 9.23 seconds
;; VERIFY took 9.79 seconds
8216> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.COMPLEMENT-CLAUSE-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.proofp-of-clause.complement-clause-bldr.proof
;; Reading the file took 0.08 seconds
; [GC threshold exceeded with 14,125,016 bytes in use. Commencing GC.]
; [GC completed with 2,877,904 bytes retained and 11,247,112 bytes freed.]
; [GC will next occur when at least 14,877,904 bytes are in use.]
;; Checking the proof took 10.02 seconds
;; VERIFY took 10.62 seconds
8217> DEFINE CLAUSE.REMOVE-COMPLEMENT-CLAUSES-BLDR
;; Reading from Proofs/level6/admit-clause.remove-complement-clauses-bldr.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.14 seconds
; Compiling LAMBDA (X PROOFS):
; Compiling Top-Level Form:
;; DEFINE took 0.14 seconds
8218> VERIFY CLAUSE.REMOVE-COMPLEMENT-CLAUSES-BLDR
;; Reading from Proofs/level6/thm-clause.remove-complement-clauses-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8219> VERIFY FORCING-LOGIC.APPEAL-LISTP-OF-CLAUSE.REMOVE-COMPLEMENT-CLAUSES-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.appeal-listp-of-clause.remove-complement-clauses-bldr.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 1.78 seconds
;; VERIFY took 1.98 seconds
8220> VERIFY FORCING-LOGIC.STRIP-CONCLUSIONS-OF-CLAUSE.REMOVE-COMPLEMENT-CLAUSES-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.strip-conclusions-of-clause.remove-complement-clauses-bldr.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 2.20 seconds
;; VERIFY took 2.42 seconds
8221> VERIFY FORCING-LOGIC.PROOF-LISTP-OF-CLAUSE.REMOVE-COMPLEMENT-CLAUSES-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.proof-listp-of-clause.remove-complement-clauses-bldr.proof
; [GC threshold exceeded with 14,890,224 bytes in use. Commencing GC.]
; [GC completed with 2,606,240 bytes retained and 12,283,984 bytes freed.]
; [GC will next occur when at least 14,606,240 bytes are in use.]
;; Reading the file took 0.07 seconds
;; Checking the proof took 2.40 seconds
;; VERIFY took 2.75 seconds
8222> VERIFY (zp (+ 1 a))
;; Reading from Proofs/level6/thm-_lp_zp_sp__lp_+_sp_1_sp_a_rp__rp_.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8223> DEFINE CLAUSE.SPLIT-COUNT
;; Reading from Proofs/level6/admit-clause.split-count.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.24 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.27 seconds
8224> VERIFY CLAUSE.SPLIT-COUNT
;; Reading from Proofs/level6/thm-clause.split-count.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8225> VERIFY NATP-OF-CLAUSE.SPLIT-COUNT
;; Reading from Proofs/level6/thm-natp-of-clause.split-count.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.16 seconds
8226> VERIFY (< 0 (clause.split-count x))
;; Reading from Proofs/level6/thm-_lp__lt__sp_0_sp__lp_clause.split-count_sp_x_rp__rp_.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.18 seconds
8227> VERIFY CLAUSE.SPLIT-COUNT-WHEN-CLAUSE.NEGATIVE-TERMP
;; Reading from Proofs/level6/thm-clause.split-count-when-clause.negative-termp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.06 seconds
8228> VERIFY CLAUSE.SPLIT-COUNT-WHEN-IF
;; Reading from Proofs/level6/thm-clause.split-count-when-if.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.16 seconds
8229> DEFINE CLAUSE.SPLIT-COUNT-LIST
;; Reading from Proofs/level6/admit-clause.split-count-list.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.08 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.10 seconds
8230> VERIFY CLAUSE.SPLIT-COUNT-LIST
;; Reading from Proofs/level6/thm-clause.split-count-list.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.03 seconds
8231> VERIFY CLAUSE.SPLIT-COUNT-LIST-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-clause.split-count-list-when-not-consp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 seconds
8232> VERIFY CLAUSE.SPLIT-COUNT-LIST-OF-CONS
;; Reading from Proofs/level6/thm-clause.split-count-list-of-cons.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8233> VERIFY NATP-OF-CLAUSE.SPLIT-COUNT-LIST
;; Reading from Proofs/level6/thm-natp-of-clause.split-count-list.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8234> DEFINE CLAUSE.AUX-SPLIT-TRIVIAL-BRANCHP
;; Reading from Proofs/level6/admit-clause.aux-split-trivial-branchp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y REST DONE):
; Compiling Top-Level Form:
;; DEFINE took 0.02 seconds
8235> VERIFY CLAUSE.AUX-SPLIT-TRIVIAL-BRANCHP
;; Reading from Proofs/level6/thm-clause.aux-split-trivial-branchp.proof
; [GC threshold exceeded with 14,669,112 bytes in use. Commencing GC.]
; [GC completed with 3,083,456 bytes retained and 11,585,656 bytes freed.]
; [GC will next occur when at least 15,083,456 bytes are in use.]
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
8236> VERIFY BOOLEANP-OF-CLAUSE.AUX-SPLIT-TRIVIAL-BRANCHP
;; Reading from Proofs/level6/thm-booleanp-of-clause.aux-split-trivial-branchp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.17 seconds
8237> DEFINE CLAUSE.AUX-SPLIT-TRIVIAL-BRANCH-BLDR
;; Reading from Proofs/level6/admit-clause.aux-split-trivial-branch-bldr.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y REST DONE):
; Compiling Top-Level Form:
;; DEFINE took 0.03 seconds
8238> VERIFY CLAUSE.AUX-SPLIT-TRIVIAL-BRANCH-BLDR
;; Reading from Proofs/level6/thm-clause.aux-split-trivial-branch-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8239> VERIFY LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TRIVIAL-BRANCH-BLDR
;; Reading from Proofs/level6/thm-logic.appealp-of-clause.aux-split-trivial-branch-bldr.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 3.75 seconds
;; VERIFY took 4.15 seconds
8240> VERIFY LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-TRIVIAL-BRANCH-BLDR
;; Reading from Proofs/level6/thm-logic.conclusion-of-clause.aux-split-trivial-branch-bldr.proof
; [GC threshold exceeded with 15,369,200 bytes in use. Commencing GC.]
; [GC completed with 3,386,128 bytes retained and 11,983,072 bytes freed.]
; [GC will next occur when at least 15,386,128 bytes are in use.]
;; Reading the file took 0.19 seconds
; [GC threshold exceeded with 15,401,112 bytes in use. Commencing GC.]
; [GC completed with 3,995,168 bytes retained and 11,405,944 bytes freed.]
; [GC will next occur when at least 15,995,168 bytes are in use.]
;; Checking the proof took 13.24 seconds
;; VERIFY took 14.78 seconds
8241> VERIFY LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-TRIVIAL-BRANCH-BLDR
;; Reading from Proofs/level6/thm-logic.proofp-of-clause.aux-split-trivial-branch-bldr.proof
;; Reading the file took 0.10 seconds
; [GC threshold exceeded with 16,246,472 bytes in use. Commencing GC.]
; [GC completed with 6,259,856 bytes retained and 9,986,616 bytes freed.]
; [GC will next occur when at least 18,259,856 bytes are in use.]
; [GC threshold exceeded with 18,271,680 bytes in use. Commencing GC.]
; [GC completed with 6,737,776 bytes retained and 11,533,904 bytes freed.]
; [GC will next occur when at least 18,737,776 bytes are in use.]
;; Checking the proof took 20.82 seconds
;; VERIFY took 24.22 seconds
8242> DEFINE CLAUSE.AUX-SPLIT
;; Reading from Proofs/level6/admit-clause.aux-split.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 4.26 seconds
; [GC threshold exceeded with 18,751,912 bytes in use. Commencing GC.]
; [GC completed with 7,740,624 bytes retained and 11,011,288 bytes freed.]
; [GC will next occur when at least 19,740,624 bytes are in use.]
; Compiling LAMBDA (TODO DONE):
; Compiling Top-Level Form:
;; DEFINE took 4.66 seconds
8243> VERIFY CLAUSE.AUX-SPLIT
;; Reading from Proofs/level6/thm-clause.aux-split.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 seconds
8244> VERIFY TRUE-LISTP-OF-CLAUSE.AUX-SPLIT
;; Reading from Proofs/level6/thm-true-listp-of-clause.aux-split.proof
; [GC threshold exceeded with 20,875,504 bytes in use. Commencing GC.]
; [GC completed with 13,668,408 bytes retained and 7,207,096 bytes freed.]
; [GC will next occur when at least 25,668,408 bytes are in use.]
;; Reading the file took 0.24 seconds
;; Checking the proof took 42.61 seconds
;; VERIFY took 49.55 seconds
8245> VERIFY FORCING-TERM-LIST-LISTP-OF-CLAUSE.AUX-SPLIT
;; Reading from Proofs/level6/thm-forcing-term-list-listp-of-clause.aux-split.proof
; [GC threshold exceeded with 25,940,712 bytes in use. Commencing GC.]
; [GC completed with 6,855,496 bytes retained and 19,085,216 bytes freed.]
; [GC will next occur when at least 18,855,496 bytes are in use.]
; [GC threshold exceeded with 22,558,712 bytes in use. Commencing GC.]
; [GC completed with 12,451,280 bytes retained and 10,107,432 bytes freed.]
; [GC will next occur when at least 24,451,280 bytes are in use.]
;; Reading the file took 0.53 seconds
; [GC threshold exceeded with 25,600,608 bytes in use. Commencing GC.]
; [GC completed with 16,721,056 bytes retained and 8,879,552 bytes freed.]
; [GC will next occur when at least 28,721,056 bytes are in use.]
; [GC threshold exceeded with 28,734,480 bytes in use. Commencing GC.]
; [GC completed with 17,189,096 bytes retained and 11,545,384 bytes freed.]
; [GC will next occur when at least 29,189,096 bytes are in use.]
;; Checking the proof took 122.79 seconds
;; VERIFY took 137.74 seconds
8246> VERIFY FORCING-TERM-LIST-LIST-ATBLP-OF-CLAUSE.AUX-SPLIT
;; Reading from Proofs/level6/thm-forcing-term-list-list-atblp-of-clause.aux-split.proof
; [GC threshold exceeded with 29,204,224 bytes in use. Commencing GC.]
; [GC completed with 7,685,488 bytes retained and 21,518,736 bytes freed.]
; [GC will next occur when at least 19,685,488 bytes are in use.]
; [GC threshold exceeded with 20,778,872 bytes in use. Commencing GC.]
; [GC completed with 12,616,064 bytes retained and 8,162,808 bytes freed.]
; [GC will next occur when at least 24,616,064 bytes are in use.]
; [GC threshold exceeded with 33,158,208 bytes in use. Commencing GC.]
; [GC completed with 19,391,720 bytes retained and 13,766,488 bytes freed.]
; [GC will next occur when at least 31,391,720 bytes are in use.]
;; Reading the file took 1.02 seconds
; [GC threshold exceeded with 31,403,032 bytes in use. Commencing GC.]
; [GC completed with 31,241,224 bytes retained and 161,808 bytes freed.]
; [GC will next occur when at least 43,241,224 bytes are in use.]
; [GC threshold exceeded with 43,254,696 bytes in use. Commencing GC.]
; [GC completed with 31,730,104 bytes retained and 11,524,592 bytes freed.]
; [GC will next occur when at least 43,730,104 bytes are in use.]
; [GC threshold exceeded with 43,743,616 bytes in use. Commencing GC.]
; [GC completed with 32,014,112 bytes retained and 11,729,504 bytes freed.]
; [GC will next occur when at least 44,014,112 bytes are in use.]
; [GC threshold exceeded with 44,023,712 bytes in use. Commencing GC.]
; [GC completed with 23,796,064 bytes retained and 20,227,648 bytes freed.]
; [GC will next occur when at least 35,796,064 bytes are in use.]
;; Checking the proof took 244.14 seconds
;; VERIFY took 272.65 seconds
8247> VERIFY FORCING-CONS-LISTP-OF-CLAUSE.AUX-SPLIT
;; Reading from Proofs/level6/thm-forcing-cons-listp-of-clause.aux-split.proof
; [GC threshold exceeded with 35,851,720 bytes in use. Commencing GC.]
; [GC completed with 27,869,720 bytes retained and 7,982,000 bytes freed.]
; [GC will next occur when at least 39,869,720 bytes are in use.]
;; Reading the file took 0.28 seconds
; [GC threshold exceeded with 39,884,920 bytes in use. Commencing GC.]
; [GC completed with 31,221,424 bytes retained and 8,663,496 bytes freed.]
; [GC will next occur when at least 43,221,424 bytes are in use.]
;; Checking the proof took 59.92 seconds
;; VERIFY took 68.74 seconds
8248> VERIFY LEN-WHEN-NOT-CONSP-OF-CDR-CHEAP
;; Reading from Proofs/level6/thm-len-when-not-consp-of-cdr-cheap.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.08 seconds
8249> DEFINE CLAUSE.SIMPLE-SPLIT
;; Reading from Proofs/level6/admit-clause.simple-split.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (CLAUSE):
; Compiling Top-Level Form:
;; DEFINE took 0.00 seconds
8250> VERIFY CLAUSE.SIMPLE-SPLIT
;; Reading from Proofs/level6/thm-clause.simple-split.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8251> VERIFY TRUE-LISTP-OF-CLAUSE.SIMPLE-SPLIT
;; Reading from Proofs/level6/thm-true-listp-of-clause.simple-split.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8252> VERIFY FORCING-TERM-LIST-LISTP-OF-CLAUSE.SIMPLE-SPLIT
;; Reading from Proofs/level6/thm-forcing-term-list-listp-of-clause.simple-split.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8253> VERIFY FORCING-TERM-LIST-LIST-ATBLP-OF-CLAUSE.SIMPLE-SPLIT
;; Reading from Proofs/level6/thm-forcing-term-list-list-atblp-of-clause.simple-split.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 seconds
8254> VERIFY FORCING-CONS-LISTP-OF-CLAUSE.SIMPLE-SPLIT
;; Reading from Proofs/level6/thm-forcing-cons-listp-of-clause.simple-split.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8255> DEFINE CLAUSE.STANDARDIZE-DOUBLE-NEGATIVE-TERM-UNDER-IFF-BLDR
;; Reading from Proofs/level6/admit-clause.standardize-double-negative-term-under-iff-bldr.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8256> VERIFY CLAUSE.STANDARDIZE-DOUBLE-NEGATIVE-TERM-UNDER-IFF-BLDR
;; Reading from Proofs/level6/thm-clause.standardize-double-negative-term-under-iff-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8257> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.STANDARDIZE-DOUBLE-NEGATIVE-TERM-UNDER-IFF-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.appealp-of-clause.standardize-double-negative-term-under-iff-bldr.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 1.19 seconds
;; VERIFY took 1.27 seconds
8258> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.STANDARDIZE-DOUBLE-NEGATIVE-TERM-UNDER-IFF-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.conclusion-of-clause.standardize-double-negative-term-under-iff-bldr.proof
; [GC threshold exceeded with 43,561,464 bytes in use. Commencing GC.]
; [GC completed with 32,185,456 bytes retained and 11,376,008 bytes freed.]
; [GC will next occur when at least 44,185,456 bytes are in use.]
;; Reading the file took 0.04 seconds
;; Checking the proof took 1.83 seconds
;; VERIFY took 1.98 seconds
8259> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.STANDARDIZE-DOUBLE-NEGATIVE-TERM-UNDER-IFF-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.proofp-of-clause.standardize-double-negative-term-under-iff-bldr.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 2.70 seconds
;; VERIFY took 2.90 seconds
8260> DEFINE CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;; Reading from Proofs/level6/admit-clause.aux-split-double-negate.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (T1 T2-TN DONE PROOF):
; Compiling Top-Level Form:
;; DEFINE took 0.00 seconds
8261> VERIFY CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;; Reading from Proofs/level6/thm-clause.aux-split-double-negate.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8262> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;; Reading from Proofs/level6/thm-forcing-logic.appealp-of-clause.aux-split-double-negate.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 2.67 seconds
;; VERIFY took 2.97 seconds
8263> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;; Reading from Proofs/level6/thm-forcing-logic.conclusion-of-clause.aux-split-double-negate.proof
; [GC threshold exceeded with 44,205,392 bytes in use. Commencing GC.]
; [GC completed with 1,280,416 bytes retained and 42,924,976 bytes freed.]
; [GC will next occur when at least 13,280,416 bytes are in use.]
;; Reading the file took 0.13 seconds
;; Checking the proof took 3.16 seconds
;; VERIFY took 3.56 seconds
8264> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-DOUBLE-NEGATE
;; Reading from Proofs/level6/thm-forcing-logic.proofp-of-clause.aux-split-double-negate.proof
;; Reading the file took 0.09 seconds
; [GC threshold exceeded with 13,292,736 bytes in use. Commencing GC.]
; [GC completed with 3,475,552 bytes retained and 9,817,184 bytes freed.]
; [GC will next occur when at least 15,475,552 bytes are in use.]
;; Checking the proof took 5.86 seconds
;; VERIFY took 6.69 seconds
8265> DEFINE CLAUSE.AUX-SPLIT-NEGATED-IF
;; Reading from Proofs/level6/admit-clause.aux-split-negated-if.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (T1 T2-TN DONE PROOF1 PROOF2):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8266> VERIFY CLAUSE.AUX-SPLIT-NEGATED-IF
;; Reading from Proofs/level6/thm-clause.aux-split-negated-if.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.03 seconds
8267> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-NEGATED-IF
;; Reading from Proofs/level6/thm-forcing-logic.appealp-of-clause.aux-split-negated-if.proof
; [GC threshold exceeded with 15,487,352 bytes in use. Commencing GC.]
; [GC completed with 6,327,488 bytes retained and 9,159,864 bytes freed.]
; [GC will next occur when at least 18,327,488 bytes are in use.]
; [GC threshold exceeded with 20,945,336 bytes in use. Commencing GC.]
; [GC completed with 11,664,216 bytes retained and 9,281,120 bytes freed.]
; [GC will next occur when at least 23,664,216 bytes are in use.]
; [GC threshold exceeded with 28,312,600 bytes in use. Commencing GC.]
; [GC completed with 17,139,408 bytes retained and 11,173,192 bytes freed.]
; [GC will next occur when at least 29,139,408 bytes are in use.]
;; Reading the file took 0.86 seconds
; [GC threshold exceeded with 29,154,808 bytes in use. Commencing GC.]
; [GC completed with 29,025,832 bytes retained and 128,976 bytes freed.]
; [GC will next occur when at least 41,025,832 bytes are in use.]
; [GC threshold exceeded with 41,035,736 bytes in use. Commencing GC.]
; [GC completed with 7,069,072 bytes retained and 33,966,664 bytes freed.]
; [GC will next occur when at least 19,069,072 bytes are in use.]
; [GC threshold exceeded with 19,078,472 bytes in use. Commencing GC.]
; [GC completed with 7,121,072 bytes retained and 11,957,400 bytes freed.]
; [GC will next occur when at least 19,121,072 bytes are in use.]
; [GC threshold exceeded with 19,129,928 bytes in use. Commencing GC.]
; [GC completed with 7,482,928 bytes retained and 11,647,000 bytes freed.]
; [GC will next occur when at least 19,482,928 bytes are in use.]
;; Checking the proof took 127.95 seconds
;; VERIFY took 143.60 seconds
8268> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-NEGATED-IF
;; Reading from Proofs/level6/thm-forcing-logic.conclusion-of-clause.aux-split-negated-if.proof
; [GC threshold exceeded with 19,493,936 bytes in use. Commencing GC.]
; [GC completed with 10,549,304 bytes retained and 8,944,632 bytes freed.]
; [GC will next occur when at least 22,549,304 bytes are in use.]
; [GC threshold exceeded with 22,781,568 bytes in use. Commencing GC.]
; [GC completed with 9,975,504 bytes retained and 12,806,064 bytes freed.]
; [GC will next occur when at least 21,975,504 bytes are in use.]
; [GC threshold exceeded with 23,671,312 bytes in use. Commencing GC.]
; [GC completed with 15,236,960 bytes retained and 8,434,352 bytes freed.]
; [GC will next occur when at least 27,236,960 bytes are in use.]
; [GC threshold exceeded with 34,951,536 bytes in use. Commencing GC.]
; [GC completed with 21,807,448 bytes retained and 13,144,088 bytes freed.]
; [GC will next occur when at least 33,807,448 bytes are in use.]
;; Reading the file took 0.92 seconds
; [GC threshold exceeded with 33,817,432 bytes in use. Commencing GC.]
; [GC completed with 21,980,752 bytes retained and 11,836,680 bytes freed.]
; [GC will next occur when at least 33,980,752 bytes are in use.]
; [GC threshold exceeded with 33,990,704 bytes in use. Commencing GC.]
; [GC completed with 22,254,328 bytes retained and 11,736,376 bytes freed.]
; [GC will next occur when at least 34,254,328 bytes are in use.]
; [GC threshold exceeded with 34,268,040 bytes in use. Commencing GC.]
; [GC completed with 22,389,400 bytes retained and 11,878,640 bytes freed.]
; [GC will next occur when at least 34,389,400 bytes are in use.]
;; Checking the proof took 142.50 seconds
;; VERIFY took 159.84 seconds
8269> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-NEGATED-IF
;; Reading from Proofs/level6/thm-forcing-logic.proofp-of-clause.aux-split-negated-if.proof
; [GC threshold exceeded with 34,400,376 bytes in use. Commencing GC.]
; [GC completed with 22,830,072 bytes retained and 11,570,304 bytes freed.]
; [GC will next occur when at least 34,830,072 bytes are in use.]
; [GC threshold exceeded with 34,843,144 bytes in use. Commencing GC.]
; [GC completed with 28,677,544 bytes retained and 6,165,600 bytes freed.]
; [GC will next occur when at least 40,677,544 bytes are in use.]
; [GC threshold exceeded with 44,139,960 bytes in use. Commencing GC.]
; [GC completed with 33,293,424 bytes retained and 10,846,536 bytes freed.]
; [GC will next occur when at least 45,293,424 bytes are in use.]
; [GC threshold exceeded with 58,264,496 bytes in use. Commencing GC.]
; [GC completed with 45,125,384 bytes retained and 13,139,112 bytes freed.]
; [GC will next occur when at least 57,125,384 bytes are in use.]
;; Reading the file took 1.11 seconds
; [GC threshold exceeded with 57,139,968 bytes in use. Commencing GC.]
; [GC completed with 45,223,664 bytes retained and 11,916,304 bytes freed.]
; [GC will next occur when at least 57,223,664 bytes are in use.]
; [GC threshold exceeded with 57,236,936 bytes in use. Commencing GC.]
; [GC completed with 45,259,552 bytes retained and 11,977,384 bytes freed.]
; [GC will next occur when at least 57,259,552 bytes are in use.]
; [GC threshold exceeded with 57,272,728 bytes in use. Commencing GC.]
; [GC completed with 45,291,024 bytes retained and 11,981,704 bytes freed.]
; [GC will next occur when at least 57,291,024 bytes are in use.]
; [GC threshold exceeded with 57,299,864 bytes in use. Commencing GC.]
; [GC completed with 45,582,720 bytes retained and 11,717,144 bytes freed.]
; [GC will next occur when at least 57,582,720 bytes are in use.]
; [GC threshold exceeded with 57,596,208 bytes in use. Commencing GC.]
; [GC completed with 45,777,776 bytes retained and 11,818,432 bytes freed.]
; [GC will next occur when at least 57,777,776 bytes are in use.]
;; Checking the proof took 175.39 seconds
;; VERIFY took 199.98 seconds
8270> DEFINE CLAUSE.AUX-SPLIT-POSITIVE-IF
;; Reading from Proofs/level6/admit-clause.aux-split-positive-if.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (T1 T2-TN DONE PROOF1 PROOF2):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8271> VERIFY CLAUSE.AUX-SPLIT-POSITIVE-IF
;; Reading from Proofs/level6/thm-clause.aux-split-positive-if.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8272> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-POSITIVE-IF
;; Reading from Proofs/level6/thm-forcing-logic.appealp-of-clause.aux-split-positive-if.proof
; [GC threshold exceeded with 57,787,992 bytes in use. Commencing GC.]
; [GC completed with 49,900,160 bytes retained and 7,887,832 bytes freed.]
; [GC will next occur when at least 61,900,160 bytes are in use.]
; [GC threshold exceeded with 67,983,432 bytes in use. Commencing GC.]
; [GC completed with 10,961,800 bytes retained and 57,021,632 bytes freed.]
; [GC will next occur when at least 22,961,800 bytes are in use.]
;; Reading the file took 0.54 seconds
; [GC threshold exceeded with 22,971,840 bytes in use. Commencing GC.]
; [GC completed with 11,036,520 bytes retained and 11,935,320 bytes freed.]
; [GC will next occur when at least 23,036,520 bytes are in use.]
;; Checking the proof took 44.13 seconds
;; VERIFY took 49.25 seconds
8273> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-POSITIVE-IF
;; Reading from Proofs/level6/thm-forcing-logic.conclusion-of-clause.aux-split-positive-if.proof
; [GC threshold exceeded with 23,049,320 bytes in use. Commencing GC.]
; [GC completed with 15,415,144 bytes retained and 7,634,176 bytes freed.]
; [GC will next occur when at least 27,415,144 bytes are in use.]
; [GC threshold exceeded with 31,897,040 bytes in use. Commencing GC.]
; [GC completed with 21,072,872 bytes retained and 10,824,168 bytes freed.]
; [GC will next occur when at least 33,072,872 bytes are in use.]
;; Reading the file took 0.44 seconds
; [GC threshold exceeded with 33,081,752 bytes in use. Commencing GC.]
; [GC completed with 15,728,640 bytes retained and 17,353,112 bytes freed.]
; [GC will next occur when at least 27,728,640 bytes are in use.]
;; Checking the proof took 49.09 seconds
;; VERIFY took 54.56 seconds
8274> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-POSITIVE-IF
;; Reading from Proofs/level6/thm-forcing-logic.proofp-of-clause.aux-split-positive-if.proof
; [GC threshold exceeded with 27,744,560 bytes in use. Commencing GC.]
; [GC completed with 19,839,200 bytes retained and 7,905,360 bytes freed.]
; [GC will next occur when at least 31,839,200 bytes are in use.]
; [GC threshold exceeded with 37,487,168 bytes in use. Commencing GC.]
; [GC completed with 25,911,288 bytes retained and 11,575,880 bytes freed.]
; [GC will next occur when at least 37,911,288 bytes are in use.]
;; Reading the file took 0.48 seconds
; [GC threshold exceeded with 37,925,336 bytes in use. Commencing GC.]
; [GC completed with 26,060,040 bytes retained and 11,865,296 bytes freed.]
; [GC will next occur when at least 38,060,040 bytes are in use.]
;; Checking the proof took 50.12 seconds
;; VERIFY took 56.20 seconds
8275> DEFINE CLAUSE.AUX-SPLIT-NEGATIVE-DEFAULT
;; Reading from Proofs/level6/admit-clause.aux-split-negative-default.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (T1 T2-TN DONE PROOF):
; Compiling Top-Level Form:
;; DEFINE took 0.00 seconds
8276> VERIFY CLAUSE.AUX-SPLIT-NEGATIVE-DEFAULT
;; Reading from Proofs/level6/thm-clause.aux-split-negative-default.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8277> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-NEGATIVE-DEFAULT
;; Reading from Proofs/level6/thm-forcing-logic.appealp-of-clause.aux-split-negative-default.proof
; [GC threshold exceeded with 38,461,048 bytes in use. Commencing GC.]
; [GC completed with 13,103,200 bytes retained and 25,357,848 bytes freed.]
; [GC will next occur when at least 25,103,200 bytes are in use.]
;; Reading the file took 0.14 seconds
;; Checking the proof took 7.44 seconds
;; VERIFY took 8.29 seconds
8278> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-NEGATIVE-DEFAULT
;; Reading from Proofs/level6/thm-forcing-logic.conclusion-of-clause.aux-split-negative-default.proof
;; Reading the file took 0.11 seconds
; [GC threshold exceeded with 25,344,560 bytes in use. Commencing GC.]
; [GC completed with 17,267,280 bytes retained and 8,077,280 bytes freed.]
; [GC will next occur when at least 29,267,280 bytes are in use.]
;; Checking the proof took 8.30 seconds
;; VERIFY took 9.20 seconds
8279> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-NEGATIVE-DEFAULT
;; Reading from Proofs/level6/thm-forcing-logic.proofp-of-clause.aux-split-negative-default.proof
; [GC threshold exceeded with 31,028,424 bytes in use. Commencing GC.]
; [GC completed with 19,461,072 bytes retained and 11,567,352 bytes freed.]
; [GC will next occur when at least 31,461,072 bytes are in use.]
;; Reading the file took 0.18 seconds
;; Checking the proof took 13.21 seconds
;; VERIFY took 14.93 seconds
8280> DEFINE CLAUSE.AUX-SPLIT-POSITIVE-DEFAULT
;; Reading from Proofs/level6/admit-clause.aux-split-positive-default.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (T1 T2-TN DONE PROOF):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8281> VERIFY CLAUSE.AUX-SPLIT-POSITIVE-DEFAULT
;; Reading from Proofs/level6/thm-clause.aux-split-positive-default.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8282> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-POSITIVE-DEFAULT
;; Reading from Proofs/level6/thm-forcing-logic.appealp-of-clause.aux-split-positive-default.proof
; [GC threshold exceeded with 31,552,736 bytes in use. Commencing GC.]
; [GC completed with 22,546,144 bytes retained and 9,006,592 bytes freed.]
; [GC will next occur when at least 34,546,144 bytes are in use.]
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.79 seconds
;; VERIFY took 0.88 seconds
8283> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-POSITIVE-DEFAULT
;; Reading from Proofs/level6/thm-forcing-logic.conclusion-of-clause.aux-split-positive-default.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 2.55 seconds
;; VERIFY took 2.79 seconds
8284> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-POSITIVE-DEFAULT
;; Reading from Proofs/level6/thm-forcing-logic.proofp-of-clause.aux-split-positive-default.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.82 seconds
;; VERIFY took 0.91 seconds
8285> DEFINE CLAUSE.AUX-SPLIT-BLDR
;; Reading from Proofs/level6/admit-clause.aux-split-bldr.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 2.73 seconds
; [GC threshold exceeded with 34,556,432 bytes in use. Commencing GC.]
; [GC completed with 23,809,424 bytes retained and 10,747,008 bytes freed.]
; [GC will next occur when at least 35,809,424 bytes are in use.]
; Compiling LAMBDA (TODO DONE PROOFS):
; Compiling Top-Level Form:
;; DEFINE took 3.00 seconds
8286> VERIFY CLAUSE.AUX-SPLIT-BLDR
;; Reading from Proofs/level6/thm-clause.aux-split-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 seconds
8287> VERIFY LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-BLDR
;; Reading from Proofs/level6/thm-lemma-for-forcing-logic.appealp-of-clause.aux-split-bldr.proof
; [GC threshold exceeded with 35,825,328 bytes in use. Commencing GC.]
; [GC completed with 29,377,880 bytes retained and 6,447,448 bytes freed.]
; [GC will next occur when at least 41,377,880 bytes are in use.]
; [GC threshold exceeded with 41,386,504 bytes in use. Commencing GC.]
; [GC completed with 24,918,552 bytes retained and 16,467,952 bytes freed.]
; [GC will next occur when at least 36,918,552 bytes are in use.]
; [GC threshold exceeded with 36,933,376 bytes in use. Commencing GC.]
; [GC completed with 32,182,896 bytes retained and 4,750,480 bytes freed.]
; [GC will next occur when at least 44,182,896 bytes are in use.]
; [GC threshold exceeded with 44,193,664 bytes in use. Commencing GC.]
; [GC completed with 36,739,944 bytes retained and 7,453,720 bytes freed.]
; [GC will next occur when at least 48,739,944 bytes are in use.]
; [GC threshold exceeded with 50,242,440 bytes in use. Commencing GC.]
; [GC completed with 41,499,416 bytes retained and 8,743,024 bytes freed.]
; [GC will next occur when at least 53,499,416 bytes are in use.]
; [GC threshold exceeded with 66,470,480 bytes in use. Commencing GC.]
; [GC completed with 47,396,184 bytes retained and 19,074,296 bytes freed.]
; [GC will next occur when at least 59,396,184 bytes are in use.]
; [GC threshold exceeded with 65,139,568 bytes in use. Commencing GC.]
; [GC completed with 65,141,576 bytes retained and -2,008 bytes freed.]
; [GC will next occur when at least 77,141,576 bytes are in use.]
; [GC threshold exceeded with 91,755,216 bytes in use. Commencing GC.]
; [GC completed with 74,011,856 bytes retained and 17,743,360 bytes freed.]
; [GC will next occur when at least 86,011,856 bytes are in use.]
; [GC threshold exceeded with 113,930,800 bytes in use. Commencing GC.]
; [GC completed with 113,932,808 bytes retained and -2,008 bytes freed.]
; [GC will next occur when at least 125,932,808 bytes are in use.]
;; Reading the file took 3.57 seconds
; [GC threshold exceeded with 125,946,160 bytes in use. Commencing GC.]
; [GC completed with 114,056,336 bytes retained and 11,889,824 bytes freed.]
; [GC will next occur when at least 126,056,336 bytes are in use.]
; [GC threshold exceeded with 126,065,944 bytes in use. Commencing GC.]
; [GC completed with 114,347,152 bytes retained and 11,718,792 bytes freed.]
; [GC will next occur when at least 126,347,152 bytes are in use.]
; [GC threshold exceeded with 126,358,600 bytes in use. Commencing GC.]
; [GC completed with 87,870,960 bytes retained and 38,487,640 bytes freed.]
; [GC will next occur when at least 99,870,960 bytes are in use.]
; [GC threshold exceeded with 99,881,744 bytes in use. Commencing GC.]
; [GC completed with 88,001,352 bytes retained and 11,880,392 bytes freed.]
; [GC will next occur when at least 100,001,352 bytes are in use.]
; [GC threshold exceeded with 100,009,832 bytes in use. Commencing GC.]
; [GC completed with 88,191,488 bytes retained and 11,818,344 bytes freed.]
; [GC will next occur when at least 100,191,488 bytes are in use.]
; [GC threshold exceeded with 100,201,896 bytes in use. Commencing GC.]
; [GC completed with 88,379,384 bytes retained and 11,822,512 bytes freed.]
; [GC will next occur when at least 100,379,384 bytes are in use.]
; [GC threshold exceeded with 100,395,312 bytes in use. Commencing GC.]
; [GC completed with 88,309,928 bytes retained and 12,085,384 bytes freed.]
; [GC will next occur when at least 100,309,928 bytes are in use.]
; [GC threshold exceeded with 100,318,656 bytes in use. Commencing GC.]
; [GC completed with 88,907,928 bytes retained and 11,410,728 bytes freed.]
; [GC will next occur when at least 100,907,928 bytes are in use.]
; [GC threshold exceeded with 100,922,888 bytes in use. Commencing GC.]
; [GC completed with 88,791,416 bytes retained and 12,131,472 bytes freed.]
; [GC will next occur when at least 100,791,416 bytes are in use.]
; [GC threshold exceeded with 100,805,168 bytes in use. Commencing GC.]
; [GC completed with 88,888,408 bytes retained and 11,916,760 bytes freed.]
; [GC will next occur when at least 100,888,408 bytes are in use.]
; [GC threshold exceeded with 100,901,200 bytes in use. Commencing GC.]
; [GC completed with 89,056,280 bytes retained and 11,844,920 bytes freed.]
; [GC will next occur when at least 101,056,280 bytes are in use.]
; [GC threshold exceeded with 101,068,592 bytes in use. Commencing GC.]
; [GC completed with 89,346,216 bytes retained and 11,722,376 bytes freed.]
; [GC will next occur when at least 101,346,216 bytes are in use.]
; [GC threshold exceeded with 101,357,360 bytes in use. Commencing GC.]
; [GC completed with 89,352,648 bytes retained and 12,004,712 bytes freed.]
; [GC will next occur when at least 101,352,648 bytes are in use.]
; [GC threshold exceeded with 101,368,952 bytes in use. Commencing GC.]
; [GC completed with 89,387,440 bytes retained and 11,981,512 bytes freed.]
; [GC will next occur when at least 101,387,440 bytes are in use.]
; [GC threshold exceeded with 101,403,616 bytes in use. Commencing GC.]
; [GC completed with 89,631,368 bytes retained and 11,772,248 bytes freed.]
; [GC will next occur when at least 101,631,368 bytes are in use.]
;; Checking the proof took 837.02 seconds
;; VERIFY took 924.53 seconds
8288> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.appealp-of-clause.aux-split-bldr.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.35 seconds
;; VERIFY took 0.42 seconds
8289> VERIFY LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-BLDR
;; Reading from Proofs/level6/thm-lemma-for-forcing-logic.proofp-of-clause.aux-split-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.33 seconds
;; VERIFY took 0.37 seconds
8290> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.proofp-of-clause.aux-split-bldr.proof
; [GC threshold exceeded with 101,647,616 bytes in use. Commencing GC.]
; [GC completed with 94,418,320 bytes retained and 7,229,296 bytes freed.]
; [GC will next occur when at least 106,418,320 bytes are in use.]
; [GC threshold exceeded with 106,431,920 bytes in use. Commencing GC.]
; [GC completed with 96,595,688 bytes retained and 9,836,232 bytes freed.]
; [GC will next occur when at least 108,595,688 bytes are in use.]
; [GC threshold exceeded with 109,302,600 bytes in use. Commencing GC.]
; [GC completed with 104,300,832 bytes retained and 5,001,768 bytes freed.]
; [GC will next occur when at least 116,300,832 bytes are in use.]
; [GC threshold exceeded with 116,315,184 bytes in use. Commencing GC.]
; [GC completed with 108,740,576 bytes retained and 7,574,608 bytes freed.]
; [GC will next occur when at least 120,740,576 bytes are in use.]
; [GC threshold exceeded with 120,753,112 bytes in use. Commencing GC.]
; [GC completed with 113,452,872 bytes retained and 7,300,240 bytes freed.]
; [GC will next occur when at least 125,452,872 bytes are in use.]
; [GC threshold exceeded with 125,464,968 bytes in use. Commencing GC.]
; [GC completed with 121,972,424 bytes retained and 3,492,544 bytes freed.]
; [GC will next occur when at least 133,972,424 bytes are in use.]
; [GC threshold exceeded with 133,985,288 bytes in use. Commencing GC.]
; [GC completed with 126,526,088 bytes retained and 7,459,200 bytes freed.]
; [GC will next occur when at least 138,526,088 bytes are in use.]
; [GC threshold exceeded with 142,932,912 bytes in use. Commencing GC.]
; [GC completed with 127,686,168 bytes retained and 15,246,744 bytes freed.]
; [GC will next occur when at least 139,686,168 bytes are in use.]
; [GC threshold exceeded with 147,400,752 bytes in use. Commencing GC.]
; [GC completed with 139,518,112 bytes retained and 7,882,640 bytes freed.]
; [GC will next occur when at least 151,518,112 bytes are in use.]
; [GC threshold exceeded with 157,261,488 bytes in use. Commencing GC.]
; [GC completed with 145,431,584 bytes retained and 11,829,904 bytes freed.]
; [GC will next occur when at least 157,431,584 bytes are in use.]
; [GC threshold exceeded with 172,045,192 bytes in use. Commencing GC.]
; [GC completed with 172,047,200 bytes retained and -2,008 bytes freed.]
; [GC will next occur when at least 184,047,200 bytes are in use.]
; [GC threshold exceeded with 211,966,176 bytes in use. Commencing GC.]
; [GC completed with 83,825,408 bytes retained and 128,140,768 bytes freed.]
; [GC will next occur when at least 95,825,408 bytes are in use.]
; [GC threshold exceeded with 143,702,344 bytes in use. Commencing GC.]
; [GC completed with 143,704,352 bytes retained and -2,008 bytes freed.]
; [GC will next occur when at least 155,704,352 bytes are in use.]
;; Reading the file took 6.16 seconds
; [GC threshold exceeded with 155,714,616 bytes in use. Commencing GC.]
; [GC completed with 144,753,992 bytes retained and 10,960,624 bytes freed.]
; [GC will next occur when at least 156,753,992 bytes are in use.]
; [GC threshold exceeded with 156,768,048 bytes in use. Commencing GC.]
; [GC completed with 145,378,984 bytes retained and 11,389,064 bytes freed.]
; [GC will next occur when at least 157,378,984 bytes are in use.]
; [GC threshold exceeded with 157,388,024 bytes in use. Commencing GC.]
; [GC completed with 144,281,208 bytes retained and 13,106,816 bytes freed.]
; [GC will next occur when at least 156,281,208 bytes are in use.]
; [GC threshold exceeded with 156,294,920 bytes in use. Commencing GC.]
; [GC completed with 144,787,264 bytes retained and 11,507,656 bytes freed.]
; [GC will next occur when at least 156,787,264 bytes are in use.]
; [GC threshold exceeded with 156,796,904 bytes in use. Commencing GC.]
; [GC completed with 145,045,280 bytes retained and 11,751,624 bytes freed.]
; [GC will next occur when at least 157,045,280 bytes are in use.]
; [GC threshold exceeded with 157,054,960 bytes in use. Commencing GC.]
; [GC completed with 146,291,560 bytes retained and 10,763,400 bytes freed.]
; [GC will next occur when at least 158,291,560 bytes are in use.]
; [GC threshold exceeded with 158,306,536 bytes in use. Commencing GC.]
; [GC completed with 146,064,152 bytes retained and 12,242,384 bytes freed.]
; [GC will next occur when at least 158,064,152 bytes are in use.]
; [GC threshold exceeded with 158,080,200 bytes in use. Commencing GC.]
; [GC completed with 147,037,864 bytes retained and 11,042,336 bytes freed.]
; [GC will next occur when at least 159,037,864 bytes are in use.]
; [GC threshold exceeded with 159,049,872 bytes in use. Commencing GC.]
; [GC completed with 146,724,104 bytes retained and 12,325,768 bytes freed.]
; [GC will next occur when at least 158,724,104 bytes are in use.]
; [GC threshold exceeded with 158,738,000 bytes in use. Commencing GC.]
; [GC completed with 147,494,864 bytes retained and 11,243,136 bytes freed.]
; [GC will next occur when at least 159,494,864 bytes are in use.]
; [GC threshold exceeded with 159,509,048 bytes in use. Commencing GC.]
; [GC completed with 147,794,784 bytes retained and 11,714,264 bytes freed.]
; [GC will next occur when at least 159,794,784 bytes are in use.]
; [GC threshold exceeded with 159,804,184 bytes in use. Commencing GC.]
; [GC completed with 148,688,864 bytes retained and 11,115,320 bytes freed.]
; [GC will next occur when at least 160,688,864 bytes are in use.]
; [GC threshold exceeded with 160,702,104 bytes in use. Commencing GC.]
; [GC completed with 147,551,512 bytes retained and 13,150,592 bytes freed.]
; [GC will next occur when at least 159,551,512 bytes are in use.]
; [GC threshold exceeded with 159,564,040 bytes in use. Commencing GC.]
; [GC completed with 148,928,384 bytes retained and 10,635,656 bytes freed.]
; [GC will next occur when at least 160,928,384 bytes are in use.]
; [GC threshold exceeded with 160,938,248 bytes in use. Commencing GC.]
; [GC completed with 147,736,624 bytes retained and 13,201,624 bytes freed.]
; [GC will next occur when at least 159,736,624 bytes are in use.]
; [GC threshold exceeded with 159,744,992 bytes in use. Commencing GC.]
; [GC completed with 149,336,664 bytes retained and 10,408,328 bytes freed.]
; [GC will next occur when at least 161,336,664 bytes are in use.]
;; Checking the proof took 491.29 seconds
;; VERIFY took 632.67 seconds
8291> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.conclusion-of-clause.aux-split-bldr.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.29 seconds
;; VERIFY took 0.34 seconds
8292> DEFINE CLAUSE.SIMPLE-SPLIT-BLDR
;; Reading from Proofs/level6/admit-clause.simple-split-bldr.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (CLAUSE PROOFS):
; Compiling Top-Level Form:
;; DEFINE took 0.03 seconds
8293> VERIFY CLAUSE.SIMPLE-SPLIT-BLDR
;; Reading from Proofs/level6/thm-clause.simple-split-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.03 seconds
8294> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.SIMPLE-SPLIT-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.appealp-of-clause.simple-split-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.07 seconds
8295> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.SIMPLE-SPLIT-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.conclusion-of-clause.simple-split-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.09 seconds
8296> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.SIMPLE-SPLIT-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.proofp-of-clause.simple-split-bldr.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.28 seconds
8297> DEFINE CLAUSE.SIMPLE-SPLIT-BLDR-OKP
;; Reading from Proofs/level6/admit-clause.simple-split-bldr-okp.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL):
; Compiling Top-Level Form:
;; DEFINE took 0.06 seconds
8298> VERIFY CLAUSE.SIMPLE-SPLIT-BLDR-OKP
;; Reading from Proofs/level6/thm-clause.simple-split-bldr-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8299> DEFINE CLAUSE.SIMPLE-SPLIT-BLDR-HIGH
;; Reading from Proofs/level6/admit-clause.simple-split-bldr-high.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (CLAUSE PROOFS):
; Compiling Top-Level Form:
;; DEFINE took 0.00 seconds
8300> VERIFY CLAUSE.SIMPLE-SPLIT-BLDR-HIGH
;; Reading from Proofs/level6/thm-clause.simple-split-bldr-high.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8301> VERIFY BOOLEANP-OF-CLAUSE.SIMPLE-SPLIT-BLDR-OKP
;; Reading from Proofs/level6/thm-booleanp-of-clause.simple-split-bldr-okp.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.22 seconds
8302> VERIFY CLAUSE.SIMPLE-SPLIT-BLDR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level6/thm-clause.simple-split-bldr-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.06 seconds
8303> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-CLAUSE.SIMPLE-SPLIT-BLDR-OKP
;; Reading from Proofs/level6/thm-lemma-1-for-soundness-of-clause.simple-split-bldr-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.08 seconds
8304> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-CLAUSE.SIMPLE-SPLIT-BLDR-OKP
;; Reading from Proofs/level6/thm-lemma-2-for-soundness-of-clause.simple-split-bldr-okp.proof
;; Reading the file took 0.01 seconds
; [GC threshold exceeded with 161,348,400 bytes in use. Commencing GC.]
; [GC completed with 147,931,400 bytes retained and 13,417,000 bytes freed.]
; [GC will next occur when at least 159,931,400 bytes are in use.]
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.26 seconds
8305> VERIFY FORCING-SOUNDNESS-OF-CLAUSE.SIMPLE-SPLIT-BLDR-OKP
;; Reading from Proofs/level6/thm-forcing-soundness-of-clause.simple-split-bldr-okp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 1.27 seconds
;; VERIFY took 1.44 seconds
8306> DEFINE CLAUSE.AUX-LIMSPLIT
;; Reading from Proofs/level6/admit-clause.aux-limsplit.proofs
;; Reading the file took 0.08 seconds
;; Checking the proofs took 4.32 seconds
; Compiling LAMBDA (TODO DONE N):
; Compiling Top-Level Form:
;; DEFINE took 4.75 seconds
8307> VERIFY CLAUSE.AUX-LIMSPLIT
;; Reading from Proofs/level6/thm-clause.aux-limsplit.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8308> VERIFY TRUE-LISTP-OF-CLAUSE.AUX-LIMSPLIT
;; Reading from Proofs/level6/thm-true-listp-of-clause.aux-limsplit.proof
; [GC threshold exceeded with 159,946,736 bytes in use. Commencing GC.]
; [GC completed with 148,909,024 bytes retained and 11,037,712 bytes freed.]
; [GC will next occur when at least 160,909,024 bytes are in use.]
; [GC threshold exceeded with 161,810,504 bytes in use. Commencing GC.]
; [GC completed with 154,592,920 bytes retained and 7,217,584 bytes freed.]
; [GC will next occur when at least 166,592,920 bytes are in use.]
;; Reading the file took 0.37 seconds
; [GC threshold exceeded with 166,604,744 bytes in use. Commencing GC.]
; [GC completed with 159,941,944 bytes retained and 6,662,800 bytes freed.]
; [GC will next occur when at least 171,941,944 bytes are in use.]
;; Checking the proof took 73.89 seconds
;; VERIFY took 84.76 seconds
8309> VERIFY FORCING-TERM-LIST-LISTP-OF-CLAUSE.AUX-LIMSPLIT
;; Reading from Proofs/level6/thm-forcing-term-list-listp-of-clause.aux-limsplit.proof
; [GC threshold exceeded with 171,952,624 bytes in use. Commencing GC.]
; [GC completed with 15,209,248 bytes retained and 156,743,376 bytes freed.]
; [GC will next occur when at least 27,209,248 bytes are in use.]
; [GC threshold exceeded with 28,022,624 bytes in use. Commencing GC.]
; [GC completed with 19,794,152 bytes retained and 8,228,472 bytes freed.]
; [GC will next occur when at least 31,794,152 bytes are in use.]
; [GC threshold exceeded with 36,442,536 bytes in use. Commencing GC.]
; [GC completed with 25,311,224 bytes retained and 11,131,312 bytes freed.]
; [GC will next occur when at least 37,311,224 bytes are in use.]
;; Reading the file took 0.80 seconds
; [GC threshold exceeded with 37,320,256 bytes in use. Commencing GC.]
; [GC completed with 26,027,032 bytes retained and 11,293,224 bytes freed.]
; [GC will next occur when at least 38,027,032 bytes are in use.]
; [GC threshold exceeded with 38,042,480 bytes in use. Commencing GC.]
; [GC completed with 25,507,480 bytes retained and 12,535,000 bytes freed.]
; [GC will next occur when at least 37,507,480 bytes are in use.]
;; Checking the proof took 184.63 seconds
;; VERIFY took 207.26 seconds
8310> VERIFY FORCING-TERM-LIST-LIST-ATBLP-OF-CLAUSE.AUX-LIMSPLIT
;; Reading from Proofs/level6/thm-forcing-term-list-list-atblp-of-clause.aux-limsplit.proof
; [GC threshold exceeded with 37,516,576 bytes in use. Commencing GC.]
; [GC completed with 30,695,512 bytes retained and 6,821,064 bytes freed.]
; [GC will next occur when at least 42,695,512 bytes are in use.]
; [GC threshold exceeded with 42,704,536 bytes in use. Commencing GC.]
; [GC completed with 35,270,224 bytes retained and 7,434,312 bytes freed.]
; [GC will next occur when at least 47,270,224 bytes are in use.]
; [GC threshold exceeded with 53,262,664 bytes in use. Commencing GC.]
; [GC completed with 42,166,560 bytes retained and 11,096,104 bytes freed.]
; [GC will next occur when at least 54,166,560 bytes are in use.]
; [GC threshold exceeded with 61,881,144 bytes in use. Commencing GC.]
; [GC completed with 39,777,456 bytes retained and 22,103,688 bytes freed.]
; [GC will next occur when at least 51,777,456 bytes are in use.]
; [GC threshold exceeded with 57,520,840 bytes in use. Commencing GC.]
; [GC completed with 57,522,848 bytes retained and -2,008 bytes freed.]
; [GC will next occur when at least 69,522,848 bytes are in use.]
;; Reading the file took 1.68 seconds
; [GC threshold exceeded with 69,532,024 bytes in use. Commencing GC.]
; [GC completed with 58,114,096 bytes retained and 11,417,928 bytes freed.]
; [GC will next occur when at least 70,114,096 bytes are in use.]
; [GC threshold exceeded with 70,122,936 bytes in use. Commencing GC.]
; [GC completed with 59,074,384 bytes retained and 11,048,552 bytes freed.]
; [GC will next occur when at least 71,074,384 bytes are in use.]
; [GC threshold exceeded with 71,084,192 bytes in use. Commencing GC.]
; [GC completed with 57,636,896 bytes retained and 13,447,296 bytes freed.]
; [GC will next occur when at least 69,636,896 bytes are in use.]
; [GC threshold exceeded with 69,649,072 bytes in use. Commencing GC.]
; [GC completed with 57,839,664 bytes retained and 11,809,408 bytes freed.]
; [GC will next occur when at least 69,839,664 bytes are in use.]
; [GC threshold exceeded with 69,852,488 bytes in use. Commencing GC.]
; [GC completed with 57,754,416 bytes retained and 12,098,072 bytes freed.]
; [GC will next occur when at least 69,754,416 bytes are in use.]
;; Checking the proof took 369.89 seconds
;; VERIFY took 414.18 seconds
8311> VERIFY FORCING-CONS-LISTP-OF-CLAUSE.AUX-LIMSPLIT
;; Reading from Proofs/level6/thm-forcing-cons-listp-of-clause.aux-limsplit.proof
; [GC threshold exceeded with 69,997,816 bytes in use. Commencing GC.]
; [GC completed with 60,824,952 bytes retained and 9,172,864 bytes freed.]
; [GC will next occur when at least 72,824,952 bytes are in use.]
; [GC threshold exceeded with 76,200,072 bytes in use. Commencing GC.]
; [GC completed with 66,041,520 bytes retained and 10,158,552 bytes freed.]
; [GC will next occur when at least 78,041,520 bytes are in use.]
;; Reading the file took
; [GC threshold exceeded with 79,186,712 bytes in use. Commencing GC.]
; [GC completed with 73,932,248 bytes retained and 5,254,464 bytes freed.]
; [GC will next occur when at least 85,932,248 bytes are in use.]
0.58 seconds
; [GC threshold exceeded with 85,941,648 bytes in use. Commencing GC.]
; [GC completed with 74,147,096 bytes retained and 11,794,552 bytes freed.]
; [GC will next occur when at least 86,147,096 bytes are in use.]
;; Checking the proof took 116.04 seconds
;; VERIFY took 132.01 seconds
8312> DEFINE CLAUSE.SIMPLE-LIMSPLIT
;; Reading from Proofs/level6/admit-clause.simple-limsplit.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (CLAUSE N):
; Compiling Top-Level Form:
;; DEFINE took 0.03 seconds
8313> VERIFY CLAUSE.SIMPLE-LIMSPLIT
;; Reading from Proofs/level6/thm-clause.simple-limsplit.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8314> VERIFY TRUE-LISTP-OF-CLAUSE.SIMPLE-LIMSPLIT
;; Reading from Proofs/level6/thm-true-listp-of-clause.simple-limsplit.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
8315> VERIFY FORCING-TERM-LIST-LISTP-OF-CLAUSE.SIMPLE-LIMSPLIT
;; Reading from Proofs/level6/thm-forcing-term-list-listp-of-clause.simple-limsplit.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8316> VERIFY FORCING-TERM-LIST-LIST-ATBLP-OF-CLAUSE.SIMPLE-LIMSPLIT
;; Reading from Proofs/level6/thm-forcing-term-list-list-atblp-of-clause.simple-limsplit.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8317> VERIFY FORCING-CONS-LISTP-OF-CLAUSE.SIMPLE-LIMSPLIT
;; Reading from Proofs/level6/thm-forcing-cons-listp-of-clause.simple-limsplit.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8318> DEFINE CLAUSE.AUX-LIMSPLIT-BLDR
;; Reading from Proofs/level6/admit-clause.aux-limsplit-bldr.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 2.80 seconds
; [GC threshold exceeded with 86,159,288 bytes in use. Commencing GC.]
; [GC completed with 76,188,296 bytes retained and 9,970,992 bytes freed.]
; [GC will next occur when at least 88,188,296 bytes are in use.]
; Compiling LAMBDA (TODO DONE PROOFS N):
; Compiling Top-Level Form:
;; DEFINE took 3.08 seconds
8319> VERIFY CLAUSE.AUX-LIMSPLIT-BLDR
;; Reading from Proofs/level6/thm-clause.aux-limsplit-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 seconds
8320> VERIFY LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-LIMSPLIT-BLDR
;; Reading from Proofs/level6/thm-lemma-for-forcing-logic.appealp-of-clause.aux-limsplit-bldr.proof
; [GC threshold exceeded with 88,198,776 bytes in use. Commencing GC.]
; [GC completed with 79,958,128 bytes retained and 8,240,648 bytes freed.]
; [GC will next occur when at least 91,958,128 bytes are in use.]
; [GC threshold exceeded with 93,818,824 bytes in use. Commencing GC.]
; [GC completed with 84,762,968 bytes retained and 9,055,856 bytes freed.]
; [GC will next occur when at least 96,762,968 bytes are in use.]
; [GC threshold exceeded with 109,734,032 bytes in use. Commencing GC.]
; [GC completed with 92,793,848 bytes retained and 16,940,184 bytes freed.]
; [GC will next occur when at least 104,793,848 bytes are in use.]
;; Reading the file took 0.98 seconds
; [GC threshold exceeded with 104,807,136 bytes in use. Commencing GC.]
; [GC completed with 93,001,984 bytes retained and 11,805,152 bytes freed.]
; [GC will next occur when at least 105,001,984 bytes are in use.]
; [GC threshold exceeded with 105,013,568 bytes in use. Commencing GC.]
; [GC completed with 92,912,168 bytes retained and 12,101,400 bytes freed.]
; [GC will next occur when at least 104,912,168 bytes are in use.]
; [GC threshold exceeded with 104,924,704 bytes in use. Commencing GC.]
; [GC completed with 93,173,632 bytes retained and 11,751,072 bytes freed.]
; [GC will next occur when at least 105,173,632 bytes are in use.]
; [GC threshold exceeded with 105,189,576 bytes in use. Commencing GC.]
; [GC completed with 93,228,000 bytes retained and 11,961,576 bytes freed.]
; [GC will next occur when at least 105,228,000 bytes are in use.]
; [GC threshold exceeded with 105,236,880 bytes in use. Commencing GC.]
; [GC completed with 93,527,536 bytes retained and 11,709,344 bytes freed.]
; [GC will next occur when at least 105,527,536 bytes are in use.]
; [GC threshold exceeded with 105,538,240 bytes in use. Commencing GC.]
; [GC completed with 93,350,376 bytes retained and 12,187,864 bytes freed.]
; [GC will next occur when at least 105,350,376 bytes are in use.]
; [GC threshold exceeded with 105,358,960 bytes in use. Commencing GC.]
; [GC completed with 93,722,048 bytes retained and 11,636,912 bytes freed.]
; [GC will next occur when at least 105,722,048 bytes are in use.]
; [GC threshold exceeded with 105,734,224 bytes in use. Commencing GC.]
; [GC completed with 93,719,016 bytes retained and 12,015,208 bytes freed.]
; [GC will next occur when at least 105,719,016 bytes are in use.]
; [GC threshold exceeded with 105,728,144 bytes in use. Commencing GC.]
; [GC completed with 93,771,872 bytes retained and 11,956,272 bytes freed.]
; [GC will next occur when at least 105,771,872 bytes are in use.]
; [GC threshold exceeded with 105,782,696 bytes in use. Commencing GC.]
; [GC completed with 94,013,688 bytes retained and 11,769,008 bytes freed.]
; [GC will next occur when at least 106,013,688 bytes are in use.]
; [GC threshold exceeded with 106,022,968 bytes in use. Commencing GC.]
; [GC completed with 94,093,264 bytes retained and 11,929,704 bytes freed.]
; [GC will next occur when at least 106,093,264 bytes are in use.]
; [GC threshold exceeded with 106,106,320 bytes in use. Commencing GC.]
; [GC completed with 94,224,496 bytes retained and 11,881,824 bytes freed.]
; [GC will next occur when at least 106,224,496 bytes are in use.]
; [GC threshold exceeded with 106,237,352 bytes in use. Commencing GC.]
; [GC completed with 94,634,320 bytes retained and 11,603,032 bytes freed.]
; [GC will next occur when at least 106,634,320 bytes are in use.]
; [GC threshold exceeded with 106,645,040 bytes in use. Commencing GC.]
; [GC completed with 94,618,128 bytes retained and 12,026,912 bytes freed.]
; [GC will next occur when at least 106,618,128 bytes are in use.]
; [GC threshold exceeded with 106,631,512 bytes in use. Commencing GC.]
; [GC completed with 94,646,616 bytes retained and 11,984,896 bytes freed.]
; [GC will next occur when at least 106,646,616 bytes are in use.]
; [GC threshold exceeded with 106,653,568 bytes in use. Commencing GC.]
; [GC completed with 36,527,808 bytes retained and 70,125,760 bytes freed.]
; [GC will next occur when at least 48,527,808 bytes are in use.]
; [GC threshold exceeded with 48,536,920 bytes in use. Commencing GC.]
; [GC completed with 36,763,680 bytes retained and 11,773,240 bytes freed.]
; [GC will next occur when at least 48,763,680 bytes are in use.]
; [GC threshold exceeded with 48,772,192 bytes in use. Commencing GC.]
; [GC completed with 36,713,408 bytes retained and 12,058,784 bytes freed.]
; [GC will next occur when at least 48,713,408 bytes are in use.]
;; Checking the proof took 357.58 seconds
;; VERIFY took 386.81 seconds
8321> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-LIMSPLIT-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.appealp-of-clause.aux-limsplit-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.41 seconds
;; VERIFY took 0.46 seconds
8322> VERIFY LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-LIMSPLIT-BLDR
;; Reading from Proofs/level6/thm-lemma-for-forcing-logic.proofp-of-clause.aux-limsplit-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.37 seconds
;; VERIFY took 0.43 seconds
8323> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-LIMSPLIT-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.proofp-of-clause.aux-limsplit-bldr.proof
; [GC threshold exceeded with 49,278,848 bytes in use. Commencing GC.]
; [GC completed with 40,098,368 bytes retained and 9,180,480 bytes freed.]
; [GC will next occur when at least 52,098,368 bytes are in use.]
; [GC threshold exceeded with 52,113,368 bytes in use. Commencing GC.]
; [GC completed with 44,639,424 bytes retained and 7,473,944 bytes freed.]
; [GC will next occur when at least 56,639,424 bytes are in use.]
; [GC threshold exceeded with 56,692,816 bytes in use. Commencing GC.]
; [GC completed with 49,295,960 bytes retained and 7,396,856 bytes freed.]
; [GC will next occur when at least 61,295,960 bytes are in use.]
; [GC threshold exceeded with 64,947,240 bytes in use. Commencing GC.]
; [GC completed with 54,484,960 bytes retained and 10,462,280 bytes freed.]
; [GC will next occur when at least 66,484,960 bytes are in use.]
; [GC threshold exceeded with 74,199,544 bytes in use. Commencing GC.]
; [GC completed with 66,316,904 bytes retained and 7,882,640 bytes freed.]
; [GC will next occur when at least 78,316,904 bytes are in use.]
; [GC threshold exceeded with 84,060,280 bytes in use. Commencing GC.]
; [GC completed with 72,230,376 bytes retained and 11,829,904 bytes freed.]
; [GC will next occur when at least 84,230,376 bytes are in use.]
; [GC threshold exceeded with 98,843,984 bytes in use. Commencing GC.]
; [GC completed with 98,845,992 bytes retained and -2,008 bytes freed.]
; [GC will next occur when at least 110,845,992 bytes are in use.]
;; Reading the file took 2.07 seconds
; [GC threshold exceeded with 110,858,784 bytes in use. Commencing GC.]
; [GC completed with 75,681,488 bytes retained and 35,177,296 bytes freed.]
; [GC will next occur when at least 87,681,488 bytes are in use.]
; [GC threshold exceeded with 87,693,888 bytes in use. Commencing GC.]
; [GC completed with 75,829,784 bytes retained and 11,864,104 bytes freed.]
; [GC will next occur when at least 87,829,784 bytes are in use.]
; [GC threshold exceeded with 87,839,776 bytes in use. Commencing GC.]
; [GC completed with 75,838,424 bytes retained and 12,001,352 bytes freed.]
; [GC will next occur when at least 87,838,424 bytes are in use.]
; [GC threshold exceeded with 87,851,328 bytes in use. Commencing GC.]
; [GC completed with 76,054,304 bytes retained and 11,797,024 bytes freed.]
; [GC will next occur when at least 88,054,304 bytes are in use.]
; [GC threshold exceeded with 88,065,272 bytes in use. Commencing GC.]
; [GC completed with 76,101,824 bytes retained and 11,963,448 bytes freed.]
; [GC will next occur when at least 88,101,824 bytes are in use.]
; [GC threshold exceeded with 88,118,000 bytes in use. Commencing GC.]
; [GC completed with 76,292,664 bytes retained and 11,825,336 bytes freed.]
; [GC will next occur when at least 88,292,664 bytes are in use.]
; [GC threshold exceeded with 88,307,768 bytes in use. Commencing GC.]
; [GC completed with 76,327,088 bytes retained and 11,980,680 bytes freed.]
; [GC will next occur when at least 88,327,088 bytes are in use.]
; [GC threshold exceeded with 88,342,536 bytes in use. Commencing GC.]
; [GC completed with 76,461,672 bytes retained and 11,880,864 bytes freed.]
; [GC will next occur when at least 88,461,672 bytes are in use.]
; [GC threshold exceeded with 88,472,168 bytes in use. Commencing GC.]
; [GC completed with 76,595,672 bytes retained and 11,876,496 bytes freed.]
; [GC will next occur when at least 88,595,672 bytes are in use.]
; [GC threshold exceeded with 88,604,000 bytes in use. Commencing GC.]
; [GC completed with 76,695,688 bytes retained and 11,908,312 bytes freed.]
; [GC will next occur when at least 88,695,688 bytes are in use.]
; [GC threshold exceeded with 88,708,296 bytes in use. Commencing GC.]
; [GC completed with 77,098,976 bytes retained and 11,609,320 bytes freed.]
; [GC will next occur when at least 89,098,976 bytes are in use.]
; [GC threshold exceeded with 89,111,320 bytes in use. Commencing GC.]
; [GC completed with 77,119,040 bytes retained and 11,992,280 bytes freed.]
; [GC will next occur when at least 89,119,040 bytes are in use.]
; [GC threshold exceeded with 89,129,656 bytes in use. Commencing GC.]
; [GC completed with 77,265,272 bytes retained and 11,864,384 bytes freed.]
; [GC will next occur when at least 89,265,272 bytes are in use.]
; [GC threshold exceeded with 89,277,200 bytes in use. Commencing GC.]
; [GC completed with 77,766,496 bytes retained and 11,510,704 bytes freed.]
; [GC will next occur when at least 89,766,496 bytes are in use.]
; [GC threshold exceeded with 89,778,464 bytes in use. Commencing GC.]
; [GC completed with 77,541,280 bytes retained and 12,237,184 bytes freed.]
; [GC will next occur when at least 89,541,280 bytes are in use.]
; [GC threshold exceeded with 89,557,432 bytes in use. Commencing GC.]
; [GC completed with 77,710,320 bytes retained and 11,847,112 bytes freed.]
; [GC will next occur when at least 89,710,320 bytes are in use.]
; [GC threshold exceeded with 89,723,368 bytes in use. Commencing GC.]
; [GC completed with 75,797,632 bytes retained and 13,925,736 bytes freed.]
; [GC will next occur when at least 87,797,632 bytes are in use.]
; [GC threshold exceeded with 87,810,184 bytes in use. Commencing GC.]
; [GC completed with 76,268,608 bytes retained and 11,541,576 bytes freed.]
; [GC will next occur when at least 88,268,608 bytes are in use.]
; [GC threshold exceeded with 88,278,856 bytes in use. Commencing GC.]
; [GC completed with 76,113,008 bytes retained and 12,165,848 bytes freed.]
; [GC will next occur when at least 88,113,008 bytes are in use.]
; [GC threshold exceeded with 88,124,728 bytes in use. Commencing GC.]
; [GC completed with 76,302,456 bytes retained and 11,822,272 bytes freed.]
; [GC will next occur when at least 88,302,456 bytes are in use.]
; [GC threshold exceeded with 88,315,112 bytes in use. Commencing GC.]
; [GC completed with 76,198,704 bytes retained and 12,116,408 bytes freed.]
; [GC will next occur when at least 88,198,704 bytes are in use.]
;; Checking the proof took 501.94 seconds
;; VERIFY took 557.52 seconds
8324> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-LIMSPLIT-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.conclusion-of-clause.aux-limsplit-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.32 seconds
;; VERIFY took 0.36 seconds
8325> DEFINE CLAUSE.SIMPLE-LIMSPLIT-BLDR
;; Reading from Proofs/level6/admit-clause.simple-limsplit-bldr.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (CLAUSE PROOFS N):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8326> VERIFY CLAUSE.SIMPLE-LIMSPLIT-BLDR
;; Reading from Proofs/level6/thm-clause.simple-limsplit-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8327> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.SIMPLE-LIMSPLIT-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.appealp-of-clause.simple-limsplit-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.08 seconds
8328> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.SIMPLE-LIMSPLIT-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.conclusion-of-clause.simple-limsplit-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.11 seconds
8329> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.SIMPLE-LIMSPLIT-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.proofp-of-clause.simple-limsplit-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 0.30 seconds
8330> DEFINE CLAUSE.SIMPLE-LIMSPLIT-BLDR-OKP
;; Reading from Proofs/level6/admit-clause.simple-limsplit-bldr-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8331> VERIFY CLAUSE.SIMPLE-LIMSPLIT-BLDR-OKP
;; Reading from Proofs/level6/thm-clause.simple-limsplit-bldr-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8332> DEFINE CLAUSE.SIMPLE-LIMSPLIT-BLDR-HIGH
;; Reading from Proofs/level6/admit-clause.simple-limsplit-bldr-high.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (CLAUSE PROOFS N):
; Compiling Top-Level Form:
;; DEFINE took 0.00 seconds
8333> VERIFY CLAUSE.SIMPLE-LIMSPLIT-BLDR-HIGH
;; Reading from Proofs/level6/thm-clause.simple-limsplit-bldr-high.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.03 seconds
8334> VERIFY BOOLEANP-OF-CLAUSE.SIMPLE-LIMSPLIT-BLDR-OKP
;; Reading from Proofs/level6/thm-booleanp-of-clause.simple-limsplit-bldr-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 0.30 seconds
8335> VERIFY CLAUSE.SIMPLE-LIMSPLIT-BLDR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level6/thm-clause.simple-limsplit-bldr-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.07 seconds
8336> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-CLAUSE.SIMPLE-LIMSPLIT-BLDR-OKP
;; Reading from Proofs/level6/thm-lemma-1-for-soundness-of-clause.simple-limsplit-bldr-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.12 seconds
8337> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-CLAUSE.SIMPLE-LIMSPLIT-BLDR-OKP
;; Reading from Proofs/level6/thm-lemma-2-for-soundness-of-clause.simple-limsplit-bldr-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.28 seconds
8338> VERIFY FORCING-SOUNDNESS-OF-CLAUSE.SIMPLE-LIMSPLIT-BLDR-OKP
;; Reading from Proofs/level6/thm-forcing-soundness-of-clause.simple-limsplit-bldr-okp.proof
;; Reading the file took 0.02 seconds
; [GC threshold exceeded with 88,210,072 bytes in use. Commencing GC.]
; [GC completed with 77,116,016 bytes retained and 11,094,056 bytes freed.]
; [GC will next occur when at least 89,116,016 bytes are in use.]
;; Checking the proof took 1.24 seconds
;; VERIFY took 1.39 seconds
8339> DEFINE CLAUSE.FLAG-FACTOR
;; Reading from Proofs/level6/admit-clause.flag-factor.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.66 seconds
; Compiling LAMBDA (FLAG X ASSIGNMENT):
; Compiling Top-Level Form:
;; DEFINE took 0.70 seconds
8340> VERIFY CLAUSE.FLAG-FACTOR
;; Reading from Proofs/level6/thm-clause.flag-factor.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8341> DEFINE CLAUSE.FACTOR
;; Reading from Proofs/level6/admit-clause.factor.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ASSIGNMENT):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8342> VERIFY CLAUSE.FACTOR
;; Reading from Proofs/level6/thm-clause.factor.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8343> DEFINE CLAUSE.FACTOR-LIST
;; Reading from Proofs/level6/admit-clause.factor-list.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ASSIGNMENT):
; Compiling Top-Level Form:
;; DEFINE took 0.00 seconds
8344> VERIFY CLAUSE.FACTOR-LIST
;; Reading from Proofs/level6/thm-clause.factor-list.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8345> VERIFY DEFINITION-OF-CLAUSE.FACTOR
;; Reading from Proofs/level6/thm-definition-of-clause.factor.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 1.00 seconds
;; VERIFY took 1.11 seconds
8346> VERIFY DEFINITION-OF-CLAUSE.FACTOR-LIST
;; Reading from Proofs/level6/thm-definition-of-clause.factor-list.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.14 seconds
8347> VERIFY CLAUSE.FLAG-FACTOR-OF-TERM-REMOVAL
;; Reading from Proofs/level6/thm-clause.flag-factor-of-term-removal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8348> VERIFY CLAUSE.FLAG-FACTOR-OF-LIST-REMOVAL
;; Reading from Proofs/level6/thm-clause.flag-factor-of-list-removal.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 seconds
8349> VERIFY CLAUSE.FACTOR-LIST-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-clause.factor-list-when-not-consp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
8350> VERIFY CLAUSE.FACTOR-LIST-OF-CONS
;; Reading from Proofs/level6/thm-clause.factor-list-of-cons.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8351> VERIFY TRUE-LISTP-OF-CLAUSE.FACTOR-LIST
;; Reading from Proofs/level6/thm-true-listp-of-clause.factor-list.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.12 seconds
8352> VERIFY LEN-OF-CLAUSE.FACTOR-LIST
;; Reading from Proofs/level6/thm-len-of-clause.factor-list.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.15 seconds
8353> VERIFY CONSP-OF-CLAUSE.FACTOR-LIST
;; Reading from Proofs/level6/thm-consp-of-clause.factor-list.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.18 seconds
8354> VERIFY CAR-OF-CLAUSE.FACTOR-LIST
;; Reading from Proofs/level6/thm-car-of-clause.factor-list.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.07 seconds
8355> VERIFY CDR-OF-CLAUSE.FACTOR-LIST
;; Reading from Proofs/level6/thm-cdr-of-clause.factor-list.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8356> VERIFY CLAUSE.FACTOR-LIST-UNDER-IFF
;; Reading from Proofs/level6/thm-clause.factor-list-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8357> VERIFY CLAUSE.FACTOR-LIST-OF-LIST-FIX
;; Reading from Proofs/level6/thm-clause.factor-list-of-list-fix.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.13 seconds
8358> VERIFY CLAUSE.FACTOR-LIST-OF-APP
;; Reading from Proofs/level6/thm-clause.factor-list-of-app.proof
; [GC threshold exceeded with 89,125,848 bytes in use. Commencing GC.]
; [GC completed with 76,584,624 bytes retained and 12,541,224 bytes freed.]
; [GC will next occur when at least 88,584,624 bytes are in use.]
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.15 seconds
8359> VERIFY REV-OF-CLAUSE.FACTOR-LIST
;; Reading from Proofs/level6/thm-rev-of-clause.factor-list.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.18 seconds
8360> VERIFY CLAUSE.FACTOR-LIST-OF-REV
;; Reading from Proofs/level6/thm-clause.factor-list-of-rev.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8361> VERIFY FIRSTN-OF-CLAUSE.FACTOR-LIST
;; Reading from Proofs/level6/thm-firstn-of-clause.factor-list.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 0.29 seconds
8362> VERIFY RESTN-OF-CLAUSE.FACTOR-LIST
;; Reading from Proofs/level6/thm-restn-of-clause.factor-list.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.16 seconds
8363> VERIFY MEMBERP-OF-CLAUSE.FACTOR-IN-CLAUSE.FACTOR-LIST-WHEN-MEMBERP
;; Reading from Proofs/level6/thm-memberp-of-clause.factor-in-clause.factor-list-when-memberp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.18 seconds
8364> VERIFY SUBSETP-OF-CLAUSE.FACTOR-LISTS-WHEN-SUBSETP
;; Reading from Proofs/level6/thm-subsetp-of-clause.factor-lists-when-subsetp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.19 seconds
8365> VERIFY CLAUSE.FACTOR-LIST-WHEN-LEN-THREE
;; Reading from Proofs/level6/thm-clause.factor-list-when-len-three.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 0.25 seconds
8366> VERIFY CLAUSE.FACTOR-WHEN-LOGIC.CONSTANTP
;; Reading from Proofs/level6/thm-clause.factor-when-logic.constantp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.09 seconds
8367> VERIFY CLAUSE.FACTOR-WHEN-LOGIC.VARIABLEP
;; Reading from Proofs/level6/thm-clause.factor-when-logic.variablep.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.11 seconds
8368> VERIFY CLAUSE.FACTOR-WHEN-NON-IF-LOGIC.FUNCTIONP
;; Reading from Proofs/level6/thm-clause.factor-when-non-if-logic.functionp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.22 seconds
8369> VERIFY CLAUSE.FACTOR-WHEN-BAD-ARGS-LOGIC.FUNCTIONP
;; Reading from Proofs/level6/thm-clause.factor-when-bad-args-logic.functionp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.25 seconds
8370> VERIFY CLAUSE.FACTOR-WHEN-IF-EXPRESSION
;; Reading from Proofs/level6/thm-clause.factor-when-if-expression.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 1.10 seconds
;; VERIFY took 1.22 seconds
8371> VERIFY CLAUSE.FACTOR-WHEN-LOGIC.LAMBDAP
;; Reading from Proofs/level6/thm-clause.factor-when-logic.lambdap.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 0.35 seconds
8372> VERIFY CLAUSE.FACTOR-WHEN-DEGENERATE
;; Reading from Proofs/level6/thm-clause.factor-when-degenerate.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.16 seconds
8373> VERIFY LEMMA-FOR-FORCING-LOGIC.TERMP-OF-CLAUSE.FACTOR
;; Reading from Proofs/level6/thm-lemma-for-forcing-logic.termp-of-clause.factor.proof
; [GC threshold exceeded with 88,876,240 bytes in use. Commencing GC.]
; [GC completed with 77,736,456 bytes retained and 11,139,784 bytes freed.]
; [GC will next occur when at least 89,736,456 bytes are in use.]
;; Reading the file took 0.08 seconds
;; Checking the proof took 2.91 seconds
;; VERIFY took 3.21 seconds
8374> VERIFY FORCING-LOGIC.TERMP-OF-CLAUSE.FACTOR
;; Reading from Proofs/level6/thm-forcing-logic.termp-of-clause.factor.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.09 seconds
8375> VERIFY FORCING-LOGIC.TERM-LISTP-OF-CLAUSE.FACTOR-LIST
;; Reading from Proofs/level6/thm-forcing-logic.term-listp-of-clause.factor-list.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.09 seconds
8376> VERIFY LEMMA-FOR-FORCING-LOGIC.TERM-ATBLP-OF-CLAUSE.FACTOR
;; Reading from Proofs/level6/thm-lemma-for-forcing-logic.term-atblp-of-clause.factor.proof
; [GC threshold exceeded with 91,472,648 bytes in use. Commencing GC.]
; [GC completed with 81,364,232 bytes retained and 10,108,416 bytes freed.]
; [GC will next occur when at least 93,364,232 bytes are in use.]
;; Reading the file took 0.17 seconds
;; Checking the proof took 9.91 seconds
;; VERIFY took 10.84 seconds
8377> VERIFY FORCING-LOGIC.TERM-ATBLP-OF-CLAUSE.FACTOR
;; Reading from Proofs/level6/thm-forcing-logic.term-atblp-of-clause.factor.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.11 seconds
8378> VERIFY FORCING-LOGIC.TERM-LIST-ATBLP-OF-CLAUSE.FACTOR-LIST
;; Reading from Proofs/level6/thm-forcing-logic.term-list-atblp-of-clause.factor-list.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.12 seconds
8379> VERIFY LEMMA-FOR-CLAUSE.FACTOR-WHEN-NOT-CONSP-OF-ASSIGNMENT
;; Reading from Proofs/level6/thm-lemma-for-clause.factor-when-not-consp-of-assignment.proof
; [GC threshold exceeded with 93,990,824 bytes in use. Commencing GC.]
; [GC completed with 85,330,016 bytes retained and 8,660,808 bytes freed.]
; [GC will next occur when at least 97,330,016 bytes are in use.]
;; Reading the file took 0.12 seconds
;; Checking the proof took 3.87 seconds
;; VERIFY took 4.30 seconds
8380> VERIFY CLAUSE.FACTOR-WHEN-NOT-CONSP-OF-ASSIGNMENT
;; Reading from Proofs/level6/thm-clause.factor-when-not-consp-of-assignment.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.12 seconds
8381> VERIFY CLAUSE.FACTOR-LIST-WHEN-NOT-CONSP-OF-ASSIGNMENT
;; Reading from Proofs/level6/thm-clause.factor-list-when-not-consp-of-assignment.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.12 seconds
8382> DEFINE CLAUSE.MULTIFACTOR
;; Reading from Proofs/level6/admit-clause.multifactor.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.08 seconds
; Compiling LAMBDA (TERM X):
; Compiling Top-Level Form:
;; DEFINE took 0.10 seconds
8383> VERIFY CLAUSE.MULTIFACTOR
;; Reading from Proofs/level6/thm-clause.multifactor.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8384> DEFINE CLAUSE.FAST-MULTIFACTOR$
;; Reading from Proofs/level6/admit-clause.fast-multifactor$.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.09 seconds
; Compiling LAMBDA (TERM X ACC):
; Compiling Top-Level Form:
;; DEFINE took 0.09 seconds
8385> VERIFY CLAUSE.FAST-MULTIFACTOR$
;; Reading from Proofs/level6/thm-clause.fast-multifactor$.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8386> VERIFY CLAUSE.MULTIFACTOR-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-clause.multifactor-when-not-consp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8387> VERIFY CLAUSE.MULTIFACTOR-OF-CONS
;; Reading from Proofs/level6/thm-clause.multifactor-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8388> VERIFY TRUE-LISTP-OF-CLAUSE.MULTIFACTOR
;; Reading from Proofs/level6/thm-true-listp-of-clause.multifactor.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.12 seconds
8389> VERIFY LEN-OF-CLAUSE.MULTIFACTOR
;; Reading from Proofs/level6/thm-len-of-clause.multifactor.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.14 seconds
8390> VERIFY CONSP-OF-CLAUSE.MULTIFACTOR
;; Reading from Proofs/level6/thm-consp-of-clause.multifactor.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.19 seconds
8391> VERIFY CAR-OF-CLAUSE.MULTIFACTOR
;; Reading from Proofs/level6/thm-car-of-clause.multifactor.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8392> VERIFY CDR-OF-CLAUSE.MULTIFACTOR
;; Reading from Proofs/level6/thm-cdr-of-clause.multifactor.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8393> VERIFY CLAUSE.MULTIFACTOR-UNDER-IFF
;; Reading from Proofs/level6/thm-clause.multifactor-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8394> VERIFY CLAUSE.MULTIFACTOR-OF-LIST-FIX
;; Reading from Proofs/level6/thm-clause.multifactor-of-list-fix.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.13 seconds
8395> VERIFY CLAUSE.MULTIFACTOR-OF-APP
;; Reading from Proofs/level6/thm-clause.multifactor-of-app.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.13 seconds
8396> VERIFY REV-OF-CLAUSE.MULTIFACTOR
;; Reading from Proofs/level6/thm-rev-of-clause.multifactor.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.18 seconds
8397> VERIFY CLAUSE.MULTIFACTOR-OF-REV
; [GC threshold exceeded with 97,338,616 bytes in use. Commencing GC.]
; [GC completed with 76,157,376 bytes retained and 21,181,240 bytes freed.]
; [GC will next occur when at least 88,157,376 bytes are in use.]
;; Reading from Proofs/level6/thm-clause.multifactor-of-rev.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.07 seconds
8398> VERIFY FIRSTN-OF-CLAUSE.MULTIFACTOR
;; Reading from Proofs/level6/thm-firstn-of-clause.multifactor.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 0.29 seconds
8399> VERIFY RESTN-OF-CLAUSE.MULTIFACTOR
;; Reading from Proofs/level6/thm-restn-of-clause.multifactor.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.16 seconds
8400> VERIFY MEMBERP-OF-CLAUSE.FACTOR-IN-CLAUSE.MULTIFACTOR-WHEN-MEMBERP
;; Reading from Proofs/level6/thm-memberp-of-clause.factor-in-clause.multifactor-when-memberp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.19 seconds
8401> VERIFY SUBSETP-OF-CLAUSE.MULTIFACTORS-WHEN-SUBSETP
;; Reading from Proofs/level6/thm-subsetp-of-clause.multifactors-when-subsetp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.18 seconds
8402> VERIFY CLAUSE.FAST-MULTIFACTOR$-REMOVAL
;; Reading from Proofs/level6/thm-clause.fast-multifactor$-removal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.24 seconds
8403> VERIFY FORCING-LOGIC.TERM-LISTP-OF-CLAUSE.MULTIFACTOR
;; Reading from Proofs/level6/thm-forcing-logic.term-listp-of-clause.multifactor.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.15 seconds
8404> DEFINE BINDING-FORMULA
;; Reading from Proofs/level6/admit-binding-formula.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8405> VERIFY BINDING-FORMULA
;; Reading from Proofs/level6/thm-binding-formula.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8406> DEFINE ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/admit-assignment-formulas.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.09 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.09 seconds
8407> VERIFY ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-assignment-formulas.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8408> DEFINE FAST-ASSIGNMENT-FORMULAS$
;; Reading from Proofs/level6/admit-fast-assignment-formulas$.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.09 seconds
; Compiling LAMBDA (X ACC):
; Compiling Top-Level Form:
;; DEFINE took 0.09 seconds
8409> VERIFY FAST-ASSIGNMENT-FORMULAS$
;; Reading from Proofs/level6/thm-fast-assignment-formulas$.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8410> VERIFY ASSIGNMENT-FORMULAS-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-assignment-formulas-when-not-consp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8411> VERIFY ASSIGNMENT-FORMULAS-OF-CONS
;; Reading from Proofs/level6/thm-assignment-formulas-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8412> VERIFY TRUE-LISTP-OF-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-true-listp-of-assignment-formulas.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.12 seconds
8413> VERIFY LEN-OF-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-len-of-assignment-formulas.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.14 seconds
8414> VERIFY CONSP-OF-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-consp-of-assignment-formulas.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.18 seconds
8415> VERIFY CAR-OF-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-car-of-assignment-formulas.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.06 seconds
8416> VERIFY CDR-OF-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-cdr-of-assignment-formulas.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.07 seconds
8417> VERIFY ASSIGNMENT-FORMULAS-UNDER-IFF
;; Reading from Proofs/level6/thm-assignment-formulas-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8418> VERIFY ASSIGNMENT-FORMULAS-OF-LIST-FIX
;; Reading from Proofs/level6/thm-assignment-formulas-of-list-fix.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.13 seconds
8419> VERIFY ASSIGNMENT-FORMULAS-OF-APP
;; Reading from Proofs/level6/thm-assignment-formulas-of-app.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.14 seconds
8420> VERIFY REV-OF-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-rev-of-assignment-formulas.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.16 seconds
8421> VERIFY ASSIGNMENT-FORMULAS-OF-REV
;; Reading from Proofs/level6/thm-assignment-formulas-of-rev.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8422> VERIFY FIRSTN-OF-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-firstn-of-assignment-formulas.proof
; [GC threshold exceeded with 88,173,328 bytes in use. Commencing GC.]
; [GC completed with 76,649,624 bytes retained and 11,523,704 bytes freed.]
; [GC will next occur when at least 88,649,624 bytes are in use.]
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 0.31 seconds
8423> VERIFY RESTN-OF-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-restn-of-assignment-formulas.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.16 seconds
8424> VERIFY MEMBERP-OF-BINDING-FORMULA-IN-ASSIGNMENT-FORMULAS-WHEN-MEMBERP
;; Reading from Proofs/level6/thm-memberp-of-binding-formula-in-assignment-formulas-when-memberp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.19 seconds
8425> VERIFY SUBSETP-OF-ASSIGNMENT-FORMULASS-WHEN-SUBSETP
;; Reading from Proofs/level6/thm-subsetp-of-assignment-formulass-when-subsetp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.19 seconds
8426> VERIFY FAST-ASSIGNMENT-FORMULAS$-REMOVAL
;; Reading from Proofs/level6/thm-fast-assignment-formulas$-removal.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.23 seconds
8427> VERIFY FORCING-LOGIC.FORMULAP-LISTP-OF-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-forcing-logic.formulap-listp-of-assignment-formulas.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.24 seconds
8428> VERIFY FORCING-LOGIC.FORMULA-ATBLP-LISTP-OF-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-forcing-logic.formula-atblp-listp-of-assignment-formulas.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.22 seconds
8429> DEFINE CLAUSE.FLAG-FACTOR-BLDR
;; Reading from Proofs/level6/admit-clause.flag-factor-bldr.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.69 seconds
; Compiling LAMBDA (FLAG X ASSIGNMENT HYPS HYPS-FORMULA):
; Compiling Top-Level Form:
;; DEFINE took 0.74 seconds
8430> VERIFY CLAUSE.FLAG-FACTOR-BLDR
;; Reading from Proofs/level6/thm-clause.flag-factor-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8431> DEFINE CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/admit-clause.factor-bldr.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ASSIGNMENT):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8432> VERIFY CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-clause.factor-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.03 seconds
8433> DEFINE CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/admit-clause.factor-list-bldr.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ASSIGNMENT):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8434> VERIFY CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-clause.factor-list-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8435> VERIFY DEFINITION-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-definition-of-clause.factor-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.56 seconds
;; VERIFY took 0.65 seconds
8436> VERIFY DEFINITION-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-definition-of-clause.factor-list-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 seconds
8437> VERIFY FORCING-CLAUSE.FLAG-FACTOR-BLDR-OF-TERM-REMOVAL
;; Reading from Proofs/level6/thm-forcing-clause.flag-factor-bldr-of-term-removal.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8438> VERIFY CLAUSE.FLAG-FACTOR-BLDR-OF-LIST-REMOVAL
;; Reading from Proofs/level6/thm-clause.flag-factor-bldr-of-list-removal.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8439> VERIFY CLAUSE.FACTOR-LIST-BLDR-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-clause.factor-list-bldr-when-not-consp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8440> VERIFY CLAUSE.FACTOR-LIST-BLDR-OF-CONS
;; Reading from Proofs/level6/thm-clause.factor-list-bldr-of-cons.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8441> VERIFY LEMMA-FOR-NIL-PRESERVINGP-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-lemma-for-nil-preservingp-of-clause.factor-list-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8442> VERIFY TRUE-LISTP-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-true-listp-of-clause.factor-list-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.13 seconds
8443> VERIFY LEN-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-len-of-clause.factor-list-bldr.proof
; [GC threshold exceeded with 88,667,800 bytes in use. Commencing GC.]
; [GC completed with 76,565,280 bytes retained and 12,102,520 bytes freed.]
; [GC will next occur when at least 88,565,280 bytes are in use.]
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.14 seconds
8444> VERIFY CONSP-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-consp-of-clause.factor-list-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.17 seconds
8445> VERIFY CAR-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-car-of-clause.factor-list-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8446> VERIFY CDR-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-cdr-of-clause.factor-list-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8447> VERIFY CLAUSE.FACTOR-LIST-BLDR-UNDER-IFF
;; Reading from Proofs/level6/thm-clause.factor-list-bldr-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
8448> VERIFY CLAUSE.FACTOR-LIST-BLDR-OF-LIST-FIX
;; Reading from Proofs/level6/thm-clause.factor-list-bldr-of-list-fix.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.13 seconds
8449> VERIFY CLAUSE.FACTOR-LIST-BLDR-OF-APP
;; Reading from Proofs/level6/thm-clause.factor-list-bldr-of-app.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.13 seconds
8450> VERIFY REV-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-rev-of-clause.factor-list-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.18 seconds
8451> VERIFY CLAUSE.FACTOR-LIST-BLDR-OF-REV
;; Reading from Proofs/level6/thm-clause.factor-list-bldr-of-rev.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8452> VERIFY FIRSTN-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-firstn-of-clause.factor-list-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 0.27 seconds
8453> VERIFY RESTN-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-restn-of-clause.factor-list-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.16 seconds
8454> VERIFY MEMBERP-OF-CLAUSE.FACTOR-BLDR-IN-CLAUSE.FACTOR-LIST-BLDR-WHEN-MEMBERP
;; Reading from Proofs/level6/thm-memberp-of-clause.factor-bldr-in-clause.factor-list-bldr-when-memberp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.19 seconds
8455> VERIFY SUBSETP-OF-CLAUSE.FACTOR-LIST-BLDRS-WHEN-SUBSETP
;; Reading from Proofs/level6/thm-subsetp-of-clause.factor-list-bldrs-when-subsetp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.19 seconds
8456> VERIFY NTH-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-nth-of-clause.factor-list-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.22 seconds
8457> VERIFY LEMMA-FORCING-MEMBERP-OF-PEQUAL-A-NIL-IN-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-lemma-forcing-memberp-of-pequal-a-nil-in-assignment-formulas.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.55 seconds
;; VERIFY took 0.60 seconds
8458> VERIFY LEMMA-FORCING-MEMBERP-OF-LOGIC.PNOT-PEQUAL-A-NIL-IN-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-lemma-forcing-memberp-of-logic.pnot-pequal-a-nil-in-assignment-formulas.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.58 seconds
;; VERIFY took 0.64 seconds
8459> VERIFY LEMMA-1-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-lemma-1-for-forcing-logic.appealp-of-clause.factor-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8460> VERIFY LEMMA-2-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-lemma-2-for-forcing-logic.appealp-of-clause.factor-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8461> VERIFY LEMMA-3-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-lemma-3-for-forcing-logic.appealp-of-clause.factor-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.10 seconds
8462> VERIFY LEMMA-1-FOR-FORCING-LOGIC.CONCLUSION-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-lemma-1-for-forcing-logic.conclusion-of-clause.factor-bldr.proof
; [GC threshold exceeded with 88,641,248 bytes in use. Commencing GC.]
; [GC completed with 76,744,384 bytes retained and 11,896,864 bytes freed.]
; [GC will next occur when at least 88,744,384 bytes are in use.]
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.11 seconds
8463> VERIFY LEMMA-2-FOR-FORCING-LOGIC.CONCLUSION-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-lemma-2-for-forcing-logic.conclusion-of-clause.factor-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.23 seconds
8464> VERIFY LEMMA-3-FOR-FORCING-LOGIC.CONCLUSION-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-lemma-3-for-forcing-logic.conclusion-of-clause.factor-bldr.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.35 seconds
;; VERIFY took 0.39 seconds
8465> VERIFY CLAUSE.FACTOR-BLDR-WHEN-LOGIC.CONSTANTP
;; Reading from Proofs/level6/thm-clause.factor-bldr-when-logic.constantp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.13 seconds
8466> VERIFY CLAUSE.FACTOR-BLDR-WHEN-LOGIC.VARIABLEP
;; Reading from Proofs/level6/thm-clause.factor-bldr-when-logic.variablep.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.18 seconds
8467> VERIFY CLAUSE.FACTOR-BLDR-WHEN-NON-IF-LOGIC.FUNCTIONP
;; Reading from Proofs/level6/thm-clause.factor-bldr-when-non-if-logic.functionp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.26 seconds
;; VERIFY took 0.29 seconds
8468> VERIFY CLAUSE.FACTOR-BLDR-WHEN-BAD-ARGS-LOGIC.FUNCTIONP
;; Reading from Proofs/level6/thm-clause.factor-bldr-when-bad-args-logic.functionp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 0.35 seconds
8469> VERIFY CLAUSE.FACTOR-BLDR-WHEN-IF
;; Reading from Proofs/level6/thm-clause.factor-bldr-when-if.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 1.41 seconds
;; VERIFY took 1.58 seconds
8470> VERIFY CLAUSE.FACTOR-BLDR-WHEN-LOGIC.LAMBDAP
;; Reading from Proofs/level6/thm-clause.factor-bldr-when-logic.lambdap.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.43 seconds
;; VERIFY took 0.50 seconds
8471> VERIFY CLAUSE.FACTOR-BLDR-WHEN-DEGENERATE
;; Reading from Proofs/level6/thm-clause.factor-bldr-when-degenerate.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.10 seconds
8472> VERIFY LEMMA-FOR-FORCING-LOGIC.APPEALP-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-lemma-for-forcing-logic.appealp-of-clause.factor-bldr.proof
; [GC threshold exceeded with 88,758,784 bytes in use. Commencing GC.]
; [GC completed with 79,861,768 bytes retained and 8,897,016 bytes freed.]
; [GC will next occur when at least 91,861,768 bytes are in use.]
; [GC threshold exceeded with 92,339,608 bytes in use. Commencing GC.]
; [GC completed with 84,510,792 bytes retained and 7,828,816 bytes freed.]
; [GC will next occur when at least 96,510,792 bytes are in use.]
; [GC threshold exceeded with 105,052,936 bytes in use. Commencing GC.]
; [GC completed with 91,339,880 bytes retained and 13,713,056 bytes freed.]
; [GC will next occur when at least 103,339,880 bytes are in use.]
;; Reading the file took 0.90 seconds
; [GC threshold exceeded with 103,351,192 bytes in use. Commencing GC.]
; [GC completed with 103,185,336 bytes retained and 165,856 bytes freed.]
; [GC will next occur when at least 115,185,336 bytes are in use.]
; [GC threshold exceeded with 115,197,072 bytes in use. Commencing GC.]
; [GC completed with 36,755,448 bytes retained and 78,441,624 bytes freed.]
; [GC will next occur when at least 48,755,448 bytes are in use.]
; [GC threshold exceeded with 48,763,880 bytes in use. Commencing GC.]
; [GC completed with 36,867,848 bytes retained and 11,896,032 bytes freed.]
; [GC will next occur when at least 48,867,848 bytes are in use.]
; [GC threshold exceeded with 48,880,056 bytes in use. Commencing GC.]
; [GC completed with 36,883,232 bytes retained and 11,996,824 bytes freed.]
; [GC will next occur when at least 48,883,232 bytes are in use.]
; [GC threshold exceeded with 48,892,856 bytes in use. Commencing GC.]
; [GC completed with 37,340,760 bytes retained and 11,552,096 bytes freed.]
; [GC will next occur when at least 49,340,760 bytes are in use.]
; [GC threshold exceeded with 49,354,568 bytes in use. Commencing GC.]
; [GC completed with 37,185,192 bytes retained and 12,169,376 bytes freed.]
; [GC will next occur when at least 49,185,192 bytes are in use.]
; [GC threshold exceeded with 49,196,032 bytes in use. Commencing GC.]
; [GC completed with 37,416,304 bytes retained and 11,779,728 bytes freed.]
; [GC will next occur when at least 49,416,304 bytes are in use.]
; [GC threshold exceeded with 49,427,432 bytes in use. Commencing GC.]
; [GC completed with 37,564,048 bytes retained and 11,863,384 bytes freed.]
; [GC will next occur when at least 49,564,048 bytes are in use.]
; [GC threshold exceeded with 49,578,648 bytes in use. Commencing GC.]
; [GC completed with 37,713,544 bytes retained and 11,865,104 bytes freed.]
; [GC will next occur when at least 49,713,544 bytes are in use.]
; [GC threshold exceeded with 49,723,792 bytes in use. Commencing GC.]
; [GC completed with 37,993,024 bytes retained and 11,730,768 bytes freed.]
; [GC will next occur when at least 49,993,024 bytes are in use.]
; [GC threshold exceeded with 50,007,928 bytes in use. Commencing GC.]
; [GC completed with 38,391,536 bytes retained and 11,616,392 bytes freed.]
; [GC will next occur when at least 50,391,536 bytes are in use.]
; [GC threshold exceeded with 50,402,752 bytes in use. Commencing GC.]
; [GC completed with 38,334,904 bytes retained and 12,067,848 bytes freed.]
; [GC will next occur when at least 50,334,904 bytes are in use.]
; [GC threshold exceeded with 50,347,136 bytes in use. Commencing GC.]
; [GC completed with 38,513,840 bytes retained and 11,833,296 bytes freed.]
; [GC will next occur when at least 50,513,840 bytes are in use.]
; [GC threshold exceeded with 50,525,376 bytes in use. Commencing GC.]
; [GC completed with 38,526,776 bytes retained and 11,998,600 bytes freed.]
; [GC will next occur when at least 50,526,776 bytes are in use.]
; [GC threshold exceeded with 50,536,728 bytes in use. Commencing GC.]
; [GC completed with 38,620,632 bytes retained and 11,916,096 bytes freed.]
; [GC will next occur when at least 50,620,632 bytes are in use.]
;; Checking the proof took 330.55 seconds
;; VERIFY took 364.64 seconds
8473> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.appealp-of-clause.factor-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.27 seconds
8474> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.conclusion-of-clause.factor-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.21 seconds
8475> VERIFY FORCING-LOGIC.APPEAL-LISTP-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.appeal-listp-of-clause.factor-list-bldr.proof
;; Reading the file took 0.01 seconds
; [GC threshold exceeded with 50,642,288 bytes in use. Commencing GC.]
; [GC completed with 37,032,368 bytes retained and 13,609,920 bytes freed.]
; [GC will next occur when at least 49,032,368 bytes are in use.]
;; Checking the proof took 0.26 seconds
;; VERIFY took 0.29 seconds
8476> VERIFY FORCING-LOGIC.STRIP-CONCLUSIONS-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.strip-conclusions-of-clause.factor-list-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.21 seconds
8477> VERIFY LEMMA-1-FOR-FORCING-LOGIC.PROOFP-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-lemma-1-for-forcing-logic.proofp-of-clause.factor-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 seconds
8478> VERIFY LEMMA-2-FOR-FORCING-LOGIC.PROOFP-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-lemma-2-for-forcing-logic.proofp-of-clause.factor-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8479> VERIFY LEMMA-3-FOR-FORCING-LOGIC.PROOFP-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-lemma-3-for-forcing-logic.proofp-of-clause.factor-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.10 seconds
8480> VERIFY LEMMA-FOR-FORCING-LOGIC.PROOFP-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-lemma-for-forcing-logic.proofp-of-clause.factor-bldr.proof
; [GC threshold exceeded with 49,041,784 bytes in use. Commencing GC.]
; [GC completed with 42,310,832 bytes retained and 6,730,952 bytes freed.]
; [GC will next occur when at least 54,310,832 bytes are in use.]
; [GC threshold exceeded with 57,292,744 bytes in use. Commencing GC.]
; [GC completed with 47,596,664 bytes retained and 9,696,080 bytes freed.]
; [GC will next occur when at least 59,596,664 bytes are in use.]
; [GC threshold exceeded with 72,567,728 bytes in use. Commencing GC.]
; [GC completed with 59,428,624 bytes retained and 13,139,104 bytes freed.]
; [GC will next occur when at least 71,428,624 bytes are in use.]
;; Reading the file took 0.88 seconds
; [GC threshold exceeded with 71,443,096 bytes in use. Commencing GC.]
; [GC completed with 59,814,416 bytes retained and 11,628,680 bytes freed.]
; [GC will next occur when at least 71,814,416 bytes are in use.]
; [GC threshold exceeded with 71,825,856 bytes in use. Commencing GC.]
; [GC completed with 59,932,440 bytes retained and 11,893,416 bytes freed.]
; [GC will next occur when at least 71,932,440 bytes are in use.]
; [GC threshold exceeded with 71,946,944 bytes in use. Commencing GC.]
; [GC completed with 55,894,824 bytes retained and 16,052,120 bytes freed.]
; [GC will next occur when at least 67,894,824 bytes are in use.]
;; Checking the proof took 66.15 seconds
;; VERIFY took 74.26 seconds
8481> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.FACTOR-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.proofp-of-clause.factor-bldr.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.44 seconds
;; VERIFY took 0.51 seconds
8482> VERIFY FORCING-LOGIC.PROOF-LISTP-OF-CLAUSE.FACTOR-LIST-BLDR
;; Reading from Proofs/level6/thm-forcing-logic.proof-listp-of-clause.factor-list-bldr.proof
; [GC threshold exceeded with 67,968,224 bytes in use. Commencing GC.]
; [GC completed with 56,467,128 bytes retained and 11,501,096 bytes freed.]
; [GC will next occur when at least 68,467,128 bytes are in use.]
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.45 seconds
;; VERIFY took 0.51 seconds
8483> DEFINE LOGIC.DISJOIN-FORMULAS-OF-SMART-NEGATE-FORMULAS-OF-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/admit-logic.disjoin-formulas-of-smart-negate-formulas-of-assignment-formulas.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.08 seconds
; Compiling LAMBDA (X):
; Compiling Top-Level Form:
;; DEFINE took 0.10 seconds
8484> VERIFY LOGIC.DISJOIN-FORMULAS-OF-SMART-NEGATE-FORMULAS-OF-ASSIGNMENT-FORMULAS
;; Reading from Proofs/level6/thm-logic.disjoin-formulas-of-smart-negate-formulas-of-assignment-formulas.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8485> VERIFY LOGIC.DISJOIN-FORMULAS-OF-SMART-NEGATE-FORMULAS-OF-ASSIGNMENT-FORMULAS-REMOVAL
;; Reading from Proofs/level6/thm-logic.disjoin-formulas-of-smart-negate-formulas-of-assignment-formulas-removal.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.92 seconds
;; VERIFY took 1.00 seconds
8486> DEFINE CLAUSE.FACTOR-BLDR-OKP
;; Reading from Proofs/level6/admit-clause.factor-bldr-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8487> VERIFY CLAUSE.FACTOR-BLDR-OKP
;; Reading from Proofs/level6/thm-clause.factor-bldr-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8488> DEFINE CLAUSE.FACTOR-BLDR-HIGH
;; Reading from Proofs/level6/admit-clause.factor-bldr-high.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ASSIGNMENT):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8489> VERIFY CLAUSE.FACTOR-BLDR-HIGH
;; Reading from Proofs/level6/thm-clause.factor-bldr-high.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8490> VERIFY BOOLEANP-OF-CLAUSE.FACTOR-BLDR-OKP
;; Reading from Proofs/level6/thm-booleanp-of-clause.factor-bldr-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.37 seconds
;; VERIFY took 0.40 seconds
8491> VERIFY CLAUSE.FACTOR-BLDR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level6/thm-clause.factor-bldr-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.08 seconds
8492> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-CLAUSE.FACTOR-BLDR-OKP
;; Reading from Proofs/level6/thm-lemma-1-for-soundness-of-clause.factor-bldr-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.15 seconds
8493> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-CLAUSE.FACTOR-BLDR-OKP
;; Reading from Proofs/level6/thm-lemma-2-for-soundness-of-clause.factor-bldr-okp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.29 seconds
8494> VERIFY FORCING-SOUNDNESS-OF-CLAUSE.FACTOR-BLDR-OKP
;; Reading from Proofs/level6/thm-forcing-soundness-of-clause.factor-bldr-okp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 1.93 seconds
;; VERIFY took 2.10 seconds
8495> DEFINE LEVEL6.STEP-OKP
;; Reading from Proofs/level6/admit-level6.step-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X AXIOMS THMS ATBL):
; Compiling Top-Level Form:
;; DEFINE took 0.00 seconds
8496> VERIFY LEVEL6.STEP-OKP
;; Reading from Proofs/level6/thm-level6.step-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
8497> VERIFY SOUNDNESS-OF-LEVEL6.STEP-OKP
;; Reading from Proofs/level6/thm-soundness-of-level6.step-okp.proof
;; Reading the file took 0.01 seconds
; [GC threshold exceeded with 68,475,736 bytes in use. Commencing GC.]
; [GC completed with 56,485,264 bytes retained and 11,990,472 bytes freed.]
; [GC will next occur when at least 68,485,264 bytes are in use.]
;; Checking the proof took 0.44 seconds
;; VERIFY took 0.55 seconds
8498> VERIFY LEVEL6.STEP-OKP-WHEN-LEVEL5.STEP-OKP
;; Reading from Proofs/level6/thm-level6.step-okp-when-level5.step-okp.proof
; [GC threshold exceeded with 69,778,720 bytes in use. Commencing GC.]
; [GC completed with 62,716,896 bytes retained and 7,061,824 bytes freed.]
; [GC will next occur when at least 74,716,896 bytes are in use.]
;; Reading the file took
; [GC threshold exceeded with 75,375,488 bytes in use. Commencing GC.]
; [GC completed with 66,350,880 bytes retained and 9,024,608 bytes freed.]
; [GC will next occur when at least 78,350,880 bytes are in use.]
0.43 seconds
;; Checking the proof took 6.99 seconds
;; VERIFY took 10.46 seconds
8499> VERIFY LEVEL6.STEP-OKP-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-level6.step-okp-when-not-consp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.08 seconds
8500> DEFINE LEVEL6.FLAG-PROOFP-AUX
;; Reading from Proofs/level6/admit-level6.flag-proofp-aux.proofs
;;
; [GC threshold exceeded with 78,393,016 bytes in use. Commencing GC.]
; [GC completed with 66,858,424 bytes retained and 11,534,592 bytes freed.]
; [GC will next occur when at least 78,858,424 bytes are in use.]
Reading the file took 0.01 seconds
;; Checking the proofs took 0.39 seconds
; Compiling LAMBDA (FLAG X AXIOMS THMS ATBL):
; Compiling Top-Level Form:
;; DEFINE took 0.44 seconds
8501> VERIFY LEVEL6.FLAG-PROOFP-AUX
;; Reading from Proofs/level6/thm-level6.flag-proofp-aux.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8502> DEFINE LEVEL6.PROOFP-AUX
;; Reading from Proofs/level6/admit-level6.proofp-aux.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X AXIOMS THMS ATBL):
; Compiling Top-Level Form:
;; DEFINE took 0.00 seconds
8503> VERIFY LEVEL6.PROOFP-AUX
;; Reading from Proofs/level6/thm-level6.proofp-aux.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8504> DEFINE LEVEL6.PROOF-LISTP-AUX
;; Reading from Proofs/level6/admit-level6.proof-listp-aux.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X AXIOMS THMS ATBL):
; Compiling Top-Level Form:
;; DEFINE took 0.00 seconds
8505> VERIFY LEVEL6.PROOF-LISTP-AUX
;; Reading from Proofs/level6/thm-level6.proof-listp-aux.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8506> VERIFY DEFINITION-OF-LEVEL6.PROOFP-AUX
;; Reading from Proofs/level6/thm-definition-of-level6.proofp-aux.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.05 seconds
8507> VERIFY DEFINITION-OF-LEVEL6.PROOF-LISTP-AUX
;; Reading from Proofs/level6/thm-definition-of-level6.proof-listp-aux.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.09 seconds
8508> VERIFY LEVEL6.PROOFP-AUX-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-level6.proofp-aux-when-not-consp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.06 seconds
8509> VERIFY LEVEL6.PROOF-LISTP-AUX-WHEN-NOT-CONSP
;; Reading from Proofs/level6/thm-level6.proof-listp-aux-when-not-consp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 seconds
8510> VERIFY LEVEL6.PROOF-LISTP-AUX-OF-CONS
;; Reading from Proofs/level6/thm-level6.proof-listp-aux-of-cons.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.06 seconds
8511> VERIFY LEMMA-FOR-BOOLEANP-OF-LEVEL6.PROOFP-AUX
;; Reading from Proofs/level6/thm-lemma-for-booleanp-of-level6.proofp-aux.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.58 seconds
;; VERIFY took 0.64 seconds
8512> VERIFY BOOLEANP-OF-LEVEL6.PROOFP-AUX
;; Reading from Proofs/level6/thm-booleanp-of-level6.proofp-aux.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.07 seconds
8513> VERIFY BOOLEANP-OF-LEVEL6.PROOF-LISTP-AUX
;; Reading from Proofs/level6/thm-booleanp-of-level6.proof-listp-aux.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.07 seconds
8514> VERIFY LEVEL6.PROOF-LISTP-AUX-OF-LIST-FIX
;; Reading from Proofs/level6/thm-level6.proof-listp-aux-of-list-fix.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.21 seconds
8515> VERIFY LEVEL6.PROOF-LISTP-AUX-OF-APP
;; Reading from Proofs/level6/thm-level6.proof-listp-aux-of-app.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 0.35 seconds
8516> VERIFY LEVEL6.PROOF-LISTP-AUX-OF-REV
;; Reading from Proofs/level6/thm-level6.proof-listp-aux-of-rev.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.22 seconds
8517> VERIFY LEVEL6.PROOFP-AUX-OF-CAR-WHEN-LEVEL6.PROOF-LISTP-AUX
;; Reading from Proofs/level6/thm-level6.proofp-aux-of-car-when-level6.proof-listp-aux.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.09 seconds
8518> VERIFY LEVEL6.PROOF-LISTP-AUX-OF-CDR-WHEN-LEVEL6.PROOF-LISTP-AUX
;; Reading from Proofs/level6/thm-level6.proof-listp-aux-of-cdr-when-level6.proof-listp-aux.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.07 seconds
8519> VERIFY LEVEL6.PROOFP-AUX-WHEN-MEMBERP-OF-LEVEL6.PROOF-LISTP-AUX
;; Reading from Proofs/level6/thm-level6.proofp-aux-when-memberp-of-level6.proof-listp-aux.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.20 seconds
8520> VERIFY LEVEL6.PROOFP-AUX-WHEN-MEMBERP-OF-LEVEL6.PROOF-LISTP-AUX-ALT
;; Reading from Proofs/level6/thm-level6.proofp-aux-when-memberp-of-level6.proof-listp-aux-alt.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.07 seconds
8521> VERIFY LEVEL6.PROOF-LISTP-AUX-OF-REMOVE-ALL-WHEN-LEVEL6.PROOF-LISTP-AUX
;; Reading from Proofs/level6/thm-level6.proof-listp-aux-of-remove-all-when-level6.proof-listp-aux.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.18 seconds
8522> VERIFY LEVEL6.PROOF-LISTP-AUX-OF-REMOVE-DUPLICATES
;; Reading from Proofs/level6/thm-level6.proof-listp-aux-of-remove-duplicates.proof
; [GC threshold exceeded with 78,905,744 bytes in use. Commencing GC.]
; [GC completed with 56,773,880 bytes retained and 22,131,864 bytes freed.]
; [GC will next occur when at least 68,773,880 bytes are in use.]
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.27 seconds
8523> VERIFY LEVEL6.PROOF-LISTP-AUX-OF-DIFFERENCE-WHEN-LEVEL6.PROOF-LISTP-AUX
;; Reading from Proofs/level6/thm-level6.proof-listp-aux-of-difference-when-level6.proof-listp-aux.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.17 seconds
8524> VERIFY LEVEL6.PROOF-LISTP-AUX-OF-SUBSETP-WHEN-LEVEL6.PROOF-LISTP-AUX
;; Reading from Proofs/level6/thm-level6.proof-listp-aux-of-subsetp-when-level6.proof-listp-aux.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.20 seconds
8525> VERIFY LEVEL6.PROOF-LISTP-AUX-OF-SUBSETP-WHEN-LEVEL6.PROOF-LISTP-AUX-ALT
;; Reading from Proofs/level6/thm-level6.proof-listp-aux-of-subsetp-when-level6.proof-listp-aux-alt.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8526> VERIFY LEVEL6.PROOF-LISTP-AUX-OF-REPEAT
;; Reading from Proofs/level6/thm-level6.proof-listp-aux-of-repeat.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.23 seconds
8527> VERIFY LEMMA-FOR-LOGIC.PROVABLEP-WHEN-LEVEL6.PROOFP-AUX
;; Reading from Proofs/level6/thm-lemma-for-logic.provablep-when-level6.proofp-aux.proof
; [GC threshold exceeded with 68,783,680 bytes in use. Commencing GC.]
; [GC completed with 61,536,488 bytes retained and 7,247,192 bytes freed.]
; [GC will next occur when at least 73,536,488 bytes are in use.]
; [GC threshold exceeded with 76,788,024 bytes in use. Commencing GC.]
; [GC completed with 67,858,488 bytes retained and 8,929,536 bytes freed.]
; [GC will next occur when at least 79,858,488 bytes are in use.]
; [GC threshold exceeded with 92,829,552 bytes in use. Commencing GC.]
; [GC completed with 79,690,448 bytes retained and 13,139,104 bytes freed.]
; [GC will next occur when at least 91,690,448 bytes are in use.]
;; Reading the file took 0.83 seconds
; [GC threshold exceeded with 91,706,560 bytes in use. Commencing GC.]
; [GC completed with 80,071,040 bytes retained and 11,635,520 bytes freed.]
; [GC will next occur when at least 92,071,040 bytes are in use.]
; [GC threshold exceeded with 92,085,472 bytes in use. Commencing GC.]
; [GC completed with 80,576,600 bytes retained and 11,508,872 bytes freed.]
; [GC will next occur when at least 92,576,600 bytes are in use.]
;; Checking the proof took 55.98 seconds
;; VERIFY took 66.94 seconds
8528> VERIFY LOGIC.PROVABLEP-WHEN-LEVEL6.PROOFP-AUX
;; Reading from Proofs/level6/thm-logic.provablep-when-level6.proofp-aux.proof
; [GC threshold exceeded with 94,001,592 bytes in use. Commencing GC.]
; [GC completed with 39,940,088 bytes retained and 54,061,504 bytes freed.]
; [GC will next occur when at least 51,940,088 bytes are in use.]
;; Reading the file took 0.15 seconds
;; Checking the proof took 6.04 seconds
;; VERIFY took 7.42 seconds
8529> VERIFY LOGIC.PROVABLE-LISTP-WHEN-LEVEL6.PROOF-LISTP-AUX
;; Reading from Proofs/level6/thm-logic.provable-listp-when-level6.proof-listp-aux.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 6.07 seconds
;; VERIFY took 7.41 seconds
8530> VERIFY LEMMA-FOR-LEVEL6.PROOFP-AUX-WHEN-LOGIC.PROOFP
;; Reading from Proofs/level6/thm-lemma-for-level6.proofp-aux-when-logic.proofp.proof
; [GC threshold exceeded with 52,074,536 bytes in use. Commencing GC.]
; [GC completed with 40,864,472 bytes retained and 11,210,064 bytes freed.]
; [GC will next occur when at least 52,864,472 bytes are in use.]
;; Reading the file took 0.13 seconds
;; Checking the proof took 0.77 seconds
;; VERIFY took 0.95 seconds
8531> VERIFY LEVEL6.PROOFP-AUX-WHEN-LOGIC.PROOFP
;; Reading from Proofs/level6/thm-level6.proofp-aux-when-logic.proofp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.07 seconds
8532> VERIFY LEVEL6.PROOF-LISTP-AUX-WHEN-LOGIC.PROOF-LISTP
;; Reading from Proofs/level6/thm-level6.proof-listp-aux-when-logic.proof-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.08 seconds
8533> VERIFY FORCING-LEVEL6.PROOFP-AUX-OF-LOGIC.PROVABLE-WITNESS
;; Reading from Proofs/level6/thm-forcing-level6.proofp-aux-of-logic.provable-witness.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 seconds
8534> DEFINE LEVEL6.PROOFP
;; Reading from Proofs/level6/admit-level6.proofp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X AXIOMS THMS ATBL):
; Compiling Top-Level Form:
;; DEFINE took 0.01 seconds
8535> VERIFY LEVEL6.PROOFP
;; Reading from Proofs/level6/thm-level6.proofp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 seconds
8536> VERIFY BOOLEANP-OF-LEVEL6.PROOFP
;; Reading from Proofs/level6/thm-booleanp-of-level6.proofp.proof
; [GC threshold exceeded with 54,704,824 bytes in use. Commencing GC.]
; [GC completed with 44,454,952 bytes retained and 10,249,872 bytes freed.]
; [GC will next occur when at least 56,454,952 bytes are in use.]
;; Reading the file took 0.25 seconds
; [GC threshold exceeded with 56,469,688 bytes in use. Commencing GC.]
; [GC completed with 48,636,792 bytes retained and 7,832,896 bytes freed.]
; [GC will next occur when at least 60,636,792 bytes are in use.]
;; Checking the proof took 10.80 seconds
;; VERIFY took 13.68 seconds
8537> VERIFY LOGIC.PROVABLEP-WHEN-LEVEL6.PROOFP
;; Reading from Proofs/level6/thm-logic.provablep-when-level6.proofp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.39 seconds
;; VERIFY took 0.46 seconds
8538> VERIFY INSTALL-NEW-PROOFP-LEVEL6.PROOFP
;; Reading from Proofs/level6/thm-install-new-proofp-level6.proofp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.04 seconds
8539 > SWITCH LEVEL6.PROOFP
;; SWITCH took 0.00 seconds
8540 > FINISH level6
[Doing purification: Done.]
[Undoing binding stack... done]
[Saving current lisp image into level6.nemesis-cmucl:
Writing 28028304 bytes from the Read-Only space at 0x10000000.
Writing 9198400 bytes from the Static space at 0x28000000.
Writing 8192 bytes from the Dynamic space at 0x58100000.
done.]
real 88m37.639s
user 88m12.763s
sys 0m4.212s