CMU Common Lisp 19f (19F), running on nemesis.cs.utexas.edu
With core: /v/filer4b/v11q002/acl2space/jared/Milawa/Sources/logic.nemesis-cmucl
Dumped on: Wed, 2009-10-28 23:11:13-05:00 on nemesis.cs.utexas.edu
See <http://www.cons.org/cmucl/> 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.
4010> DEFINE BUILD.AXIOM
;; Reading from Proofs/level2/admit-build.axiom.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A): 
; Compiling Top-Level Form: 
;; DEFINE took 0.04 seconds
4011> VERIFY BUILD.AXIOM
;; Reading from Proofs/level2/thm-build.axiom.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
4012> VERIFY BUILD.AXIOM-UNDER-IFF
;; Reading from Proofs/level2/thm-build.axiom-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
4013> VERIFY LOGIC.METHOD-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.method-of-build.axiom.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4014> VERIFY LOGIC.CONCLUSION-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.axiom.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4015> VERIFY LOGIC.SUBPROOFS-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.axiom.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4016> VERIFY LOGIC.EXTRAS-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.extras-of-build.axiom.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4017> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.axiom.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.07 seconds
4018> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.axiom.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.32 seconds
4019> DEFINE BUILD.THEOREM
;; Reading from Proofs/level2/admit-build.theorem.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.01 seconds
4020> VERIFY BUILD.THEOREM
;; Reading from Proofs/level2/thm-build.theorem.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4021> VERIFY BUILD.THEOREM-UNDER-IFF
;; Reading from Proofs/level2/thm-build.theorem-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4022> VERIFY LOGIC.METHOD-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.method-of-build.theorem.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4023> VERIFY LOGIC.CONCLUSION-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.theorem.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4024> VERIFY LOGIC.SUBPROOFS-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.theorem.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4025> VERIFY LOGIC.EXTRAS-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.extras-of-build.theorem.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4026> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.theorem.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.07 seconds
4027> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.theorem.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.32 seconds
4028> DEFINE BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/admit-build.propositional-schema.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
4029> VERIFY BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-build.propositional-schema.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4030> VERIFY BUILD.PROPOSITIONAL-SCHEMA-UNDER-IFF
;; Reading from Proofs/level2/thm-build.propositional-schema-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4031> VERIFY LOGIC.METHOD-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-logic.method-of-build.propositional-schema.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
4032> VERIFY LOGIC.CONCLUSION-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.propositional-schema.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 seconds
4033> VERIFY LOGIC.SUBPROOFS-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.propositional-schema.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4034> VERIFY LOGIC.EXTRAS-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-logic.extras-of-build.propositional-schema.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4035> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.propositional-schema.proof
; [GC threshold exceeded with 12,101,488 bytes in use.  Commencing GC.]
; [GC completed with 577,896 bytes retained and 11,523,592 bytes freed.]
; [GC will next occur when at least 12,577,896 bytes are in use.]
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.10 seconds
4036> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.propositional-schema.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.36 seconds
4037> DEFINE BUILD.CUT
;; Reading from Proofs/level2/admit-build.cut.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4038> VERIFY BUILD.CUT
;; Reading from Proofs/level2/thm-build.cut.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4039> VERIFY BUILD.CUT-UNDER-IFF
;; Reading from Proofs/level2/thm-build.cut-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4040> VERIFY LOGIC.METHOD-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-logic.method-of-build.cut.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4041> VERIFY LOGIC.CONCLUSION-OF-CUT
;; Reading from Proofs/level2/thm-logic.conclusion-of-cut.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
4042> VERIFY LOGIC.SUBPROOFS-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.cut.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.07 seconds
4043> VERIFY LOGIC.EXTRAS-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-logic.extras-of-build.cut.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4044> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.cut.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 0.49 seconds
4045> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.cut.proof
; [GC threshold exceeded with 13,599,408 bytes in use.  Commencing GC.]
; [GC completed with 2,778,144 bytes retained and 10,821,264 bytes freed.]
; [GC will next occur when at least 14,778,144 bytes are in use.]
;; Reading the file took 0.15 seconds
;; Checking the proof took 1.20 seconds
;; VERIFY took 1.98 seconds
4046> DEFINE BUILD.CONTRACTION
;; Reading from Proofs/level2/admit-build.contraction.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
4047> VERIFY BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-build.contraction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4048> VERIFY BUILD.CONTRACTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.contraction-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4049> VERIFY LOGIC.METHOD-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.method-of-build.contraction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4050> VERIFY LOGIC.CONCLUSION-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.contraction.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4051> VERIFY LOGIC.SUBPROOFS-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.contraction.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
4052> VERIFY LOGIC.EXTRAS-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.extras-of-build.contraction.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.02 seconds
4053> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.contraction.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.21 seconds
4054> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.contraction.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.38 seconds
;; VERIFY took 0.62 seconds
4055> DEFINE BUILD.EXPANSION
;; Reading from Proofs/level2/admit-build.expansion.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4056> VERIFY BUILD.EXPANSION
;; Reading from Proofs/level2/thm-build.expansion.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
4057> VERIFY BUILD.EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.expansion-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
4058> VERIFY LOGIC.METHOD-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.method-of-build.expansion.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4059> VERIFY LOGIC.CONCLUSION-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.expansion.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4060> VERIFY LOGIC.SUBPROOFS-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.expansion.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
4061> VERIFY LOGIC.EXTRAS-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.extras-of-build.expansion.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4062> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.expansion.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.13 seconds
4063> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.expansion.proof
; [GC threshold exceeded with 15,005,880 bytes in use.  Commencing GC.]
; [GC completed with 3,687,640 bytes retained and 11,318,240 bytes freed.]
; [GC will next occur when at least 15,687,640 bytes are in use.]
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 0.45 seconds
4064> DEFINE BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.associativity.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.02 seconds
4065> VERIFY BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4066> VERIFY BUILD.ASSOCIATIVITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.associativity-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4067> VERIFY LOGIC.METHOD-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.method-of-build.associativity.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4068> VERIFY LOGIC.CONCLUSION-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.associativity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 seconds
4069> VERIFY LOGIC.SUBPROOFS-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.associativity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 seconds
4070> VERIFY LOGIC.EXTRAS-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.extras-of-build.associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4071> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.associativity.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 0.41 seconds
4072> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.associativity.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.75 seconds
;; VERIFY took 1.12 seconds
4073> DEFINE BUILD.INSTANTIATION
;; Reading from Proofs/level2/admit-build.instantiation.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X SIGMA): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4074> VERIFY BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-build.instantiation.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4075> VERIFY BUILD.INSTANTIATION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.instantiation-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4076> VERIFY LOGIC.METHOD-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.method-of-build.instantiation.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.17 seconds
4077> VERIFY LOGIC.CONCLUSION-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.instantiation.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.10 seconds
4078> VERIFY LOGIC.SUBPROOFS-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.instantiation.proof
; [GC threshold exceeded with 15,695,688 bytes in use.  Commencing GC.]
; [GC completed with 459,144 bytes retained and 15,236,544 bytes freed.]
; [GC will next occur when at least 12,459,144 bytes are in use.]
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.38 seconds
;; VERIFY took 0.66 seconds
4079> VERIFY LOGIC.EXTRAS-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.extras-of-build.instantiation.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.18 seconds
4080> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.instantiation.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.31 seconds
4081> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.instantiation.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.62 seconds
;; VERIFY took 1.02 seconds
4082> DEFINE BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/admit-build.functional-equality.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (FN TI SI): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4083> VERIFY BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-build.functional-equality.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4084> VERIFY BUILD.FUNCTIONAL-EQUALITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.functional-equality-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4085> VERIFY LOGIC.METHOD-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-logic.method-of-build.functional-equality.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4086> VERIFY LOGIC.CONCLUSION-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.functional-equality.proof
; [GC threshold exceeded with 12,488,432 bytes in use.  Commencing GC.]
; [GC completed with 1,051,456 bytes retained and 11,436,976 bytes freed.]
; [GC will next occur when at least 13,051,456 bytes are in use.]
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4087> VERIFY LOGIC.SUBPROOFS-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.functional-equality.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4088> VERIFY LOGIC.EXTRAS-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-logic.extras-of-build.functional-equality.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4089> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.functional-equality.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.22 seconds
4090> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.functional-equality.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.66 seconds
;; VERIFY took 1.07 seconds
4091> DEFINE BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/admit-build.beta-reduction.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (FORMALS BODY ACTUALS): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4092> VERIFY BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-build.beta-reduction.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4093> VERIFY BUILD.BETA-REDUCTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.beta-reduction-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4094> VERIFY LOGIC.METHOD-OF-BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-logic.method-of-build.beta-reduction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4095> VERIFY LOGIC.CONCLUSION-OF-BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.beta-reduction.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.06 seconds
4096> VERIFY LOGIC.SUBPROOFS-OF-BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.beta-reduction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4097> VERIFY LOGIC.EXTRAS-OF-BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-logic.extras-of-build.beta-reduction.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
4098> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.beta-reduction.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.36 seconds
;; VERIFY took 0.54 seconds
4099> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.beta-reduction.proof
; [GC threshold exceeded with 13,064,256 bytes in use.  Commencing GC.]
; [GC completed with 1,434,120 bytes retained and 11,630,136 bytes freed.]
; [GC will next occur when at least 13,434,120 bytes are in use.]
;; Reading the file took 0.14 seconds
;; Checking the proof took 1.05 seconds
;; VERIFY took 1.72 seconds
4100> DEFINE BUILD.BASE-EVAL
;; Reading from Proofs/level2/admit-build.base-eval.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A): 
; Compiling Top-Level Form: 
;; DEFINE took 0.02 seconds
4101> VERIFY BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-build.base-eval.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4102> VERIFY BUILD.BASE-EVAL-UNDER-IFF
;; Reading from Proofs/level2/thm-build.base-eval-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4103> VERIFY LOGIC.METHOD-OF-BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-logic.method-of-build.base-eval.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4104> VERIFY LOGIC.CONCLUSION-OF-BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.base-eval.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4105> VERIFY LOGIC.SUBPROOFS-OF-BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.base-eval.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4106> VERIFY LOGIC.EXTRAS-OF-BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-logic.extras-of-build.base-eval.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.02 seconds
4107> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.base-eval.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.12 seconds
4108> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.base-eval.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.28 seconds
;; VERIFY took 0.46 seconds
4109> DEFINE BUILD.INSTANTIATION-LIST
;; Reading from Proofs/level2/admit-build.instantiation-list.proofs
; [GC threshold exceeded with 13,475,744 bytes in use.  Commencing GC.]
; [GC completed with 2,359,480 bytes retained and 11,116,264 bytes freed.]
; [GC will next occur when at least 14,359,480 bytes are in use.]
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.08 seconds
; Compiling LAMBDA (X SIGMA): 
; Compiling Top-Level Form: 
;; DEFINE took 0.13 seconds
4110> VERIFY BUILD.INSTANTIATION-LIST
;; Reading from Proofs/level2/thm-build.instantiation-list.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4111> VERIFY BUILD.INSTANTIATION-LIST-WHEN-NOT-CONSP
;; Reading from Proofs/level2/thm-build.instantiation-list-when-not-consp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.07 seconds
4112> VERIFY BUILD.INSTANTIATION-LIST-OF-CONS
;; Reading from Proofs/level2/thm-build.instantiation-list-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.07 seconds
4113> VERIFY FORCING-LOGIC.APPEAL-LISTP-OF-BUILD.INSTANTIATION-LIST
;; Reading from Proofs/level2/thm-forcing-logic.appeal-listp-of-build.instantiation-list.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.91 seconds
;; VERIFY took 1.38 seconds
4114> VERIFY FORCING-LOGIC.STRIP-CONCLUSIONS-OF-BUILD.INSTANTIATION-LIST
;; Reading from Proofs/level2/thm-forcing-logic.strip-conclusions-of-build.instantiation-list.proof
; [GC threshold exceeded with 14,935,920 bytes in use.  Commencing GC.]
; [GC completed with 3,620,872 bytes retained and 11,315,048 bytes freed.]
; [GC will next occur when at least 15,620,872 bytes are in use.]
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.83 seconds
;; VERIFY took 1.28 seconds
4115> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.INSTANTIATION-LIST
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.instantiation-list.proof
; [GC threshold exceeded with 18,137,224 bytes in use.  Commencing GC.]
; [GC completed with 10,784,872 bytes retained and 7,352,352 bytes freed.]
; [GC will next occur when at least 22,784,872 bytes are in use.]
;; Reading the file took 0.23 seconds
;; Checking the proof took 1.19 seconds
;; VERIFY took 1.93 seconds
4116> DEFINE BUILD.INDUCTION
;; Reading from Proofs/level2/admit-build.induction.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (F M QS ALL-SIGMAS PROOFS): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4117> VERIFY BUILD.INDUCTION
;; Reading from Proofs/level2/thm-build.induction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4118> VERIFY BUILD.INDUCTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.induction-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
4119> VERIFY LOGIC.METHOD-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-logic.method-of-build.induction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4120> VERIFY LOGIC.CONCLUSION-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.induction.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
4121> VERIFY LOGIC.SUBPROOFS-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.induction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4122> VERIFY LOGIC.EXTRAS-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-logic.extras-of-build.induction.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.12 seconds
4123> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.induction.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.12 seconds
4124> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.induction.proof
; [GC threshold exceeded with 24,373,504 bytes in use.  Commencing GC.]
; [GC completed with 11,343,976 bytes retained and 13,029,528 bytes freed.]
; [GC will next occur when at least 23,343,976 bytes are in use.]
;; Reading the file took 0.24 seconds
;; Checking the proof took 2.49 seconds
;; VERIFY took 4.23 seconds
4125> DEFINE BUILD.COMMUTE-OR
;; Reading from Proofs/level2/admit-build.commute-or.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
4126> VERIFY BUILD.COMMUTE-OR
;; Reading from Proofs/level2/thm-build.commute-or.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4127> VERIFY BUILD.COMMUTE-OR-UNDER-IFF
;; Reading from Proofs/level2/thm-build.commute-or-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4128> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.COMMUTE-OR
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.commute-or.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.25 seconds
4129> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.COMMUTE-OR
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.commute-or.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.07 seconds
4130> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.COMMUTE-OR
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.commute-or.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.29 seconds
4131> DEFINE BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/admit-build.commute-or-okp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4132> VERIFY BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-build.commute-or-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4133> VERIFY BOOLEANP-OF-BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.commute-or-okp.proof
; [GC threshold exceeded with 24,020,392 bytes in use.  Commencing GC.]
; [GC completed with 15,572,568 bytes retained and 8,447,824 bytes freed.]
; [GC will next occur when at least 27,572,568 bytes are in use.]
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.61 seconds
;; VERIFY took 1.00 seconds
4134> VERIFY BUILD.COMMUTE-OR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.commute-or-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.27 seconds
4135> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.commute-or-okp.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 5.19 seconds
;; VERIFY took 8.00 seconds
4136> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.commute-or-okp.proof
; [GC threshold exceeded with 28,472,720 bytes in use.  Commencing GC.]
; [GC completed with 2,829,232 bytes retained and 25,643,488 bytes freed.]
; [GC will next occur when at least 14,829,232 bytes are in use.]
;; Reading the file took 0.16 seconds
;; Checking the proof took 3.35 seconds
;; VERIFY took 5.16 seconds
4137> VERIFY FORCING-SOUNDNESS-OF-BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.commute-or-okp.proof
; [GC threshold exceeded with 15,240,912 bytes in use.  Commencing GC.]
; [GC completed with 9,968,664 bytes retained and 5,272,248 bytes freed.]
; [GC will next occur when at least 21,968,664 bytes are in use.]
;; Reading the file took 0.28 seconds
;; Checking the proof took 1.94 seconds
;; VERIFY took 3.23 seconds
4138> DEFINE BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/admit-build.right-expansion.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X B): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4139> VERIFY BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-build.right-expansion.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4140> VERIFY BUILD.RIGHT-EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.right-expansion-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4141> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.right-expansion.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.12 seconds
4142> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.right-expansion.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.34 seconds
;; VERIFY took 0.51 seconds
4143> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.right-expansion.proof
; [GC threshold exceeded with 22,190,168 bytes in use.  Commencing GC.]
; [GC completed with 5,186,584 bytes retained and 17,003,584 bytes freed.]
; [GC will next occur when at least 17,186,584 bytes are in use.]
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.21 seconds
4144> DEFINE BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/admit-build.right-expansion-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.00 seconds
4145> VERIFY BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-build.right-expansion-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4146> VERIFY BOOLEANP-OF-BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.right-expansion-okp.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.41 seconds
;; VERIFY took 0.64 seconds
4147> VERIFY BUILD.RIGHT-EXPANSION-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.right-expansion-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.19 seconds
4148> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.right-expansion-okp.proof
; [GC threshold exceeded with 17,734,992 bytes in use.  Commencing GC.]
; [GC completed with 10,251,872 bytes retained and 7,483,120 bytes freed.]
; [GC will next occur when at least 22,251,872 bytes are in use.]
;; Reading the file took 0.24 seconds
;; Checking the proof took 7.90 seconds
;; VERIFY took 12.23 seconds
4149> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.right-expansion-okp.proof
;; Reading the file took 0.12 seconds
; [GC threshold exceeded with 22,260,096 bytes in use.  Commencing GC.]
; [GC completed with 8,034,968 bytes retained and 14,225,128 bytes freed.]
; [GC will next occur when at least 20,034,968 bytes are in use.]
;; Checking the proof took 1.82 seconds
;; VERIFY took 2.83 seconds
4150> VERIFY FORCING-SOUNDNESS-OF-BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.right-expansion-okp.proof
;; Reading the file took 0.20 seconds
; [GC threshold exceeded with 20,387,304 bytes in use.  Commencing GC.]
; [GC completed with 13,863,408 bytes retained and 6,523,896 bytes freed.]
; [GC will next occur when at least 25,863,408 bytes are in use.]
;; Checking the proof took 1.40 seconds
;; VERIFY took 2.35 seconds
4151> DEFINE BUILD.MODUS-PONENS
;; Reading from Proofs/level2/admit-build.modus-ponens.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4152> VERIFY BUILD.MODUS-PONENS
;; Reading from Proofs/level2/thm-build.modus-ponens.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4153> VERIFY BUILD.MODUS-PONENS-UNDER-IFF
;; Reading from Proofs/level2/thm-build.modus-ponens-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4154> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MODUS-PONENS
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.modus-ponens.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.60 seconds
;; VERIFY took 0.90 seconds
4155> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.MODUS-PONENS
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.modus-ponens.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.77 seconds
;; VERIFY took 1.19 seconds
4156> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.MODUS-PONENS
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.modus-ponens.proof
; [GC threshold exceeded with 26,351,632 bytes in use.  Commencing GC.]
; [GC completed with 6,585,424 bytes retained and 19,766,208 bytes freed.]
; [GC will next occur when at least 18,585,424 bytes are in use.]
;; Reading the file took 0.17 seconds
;; Checking the proof took 7.08 seconds
;; VERIFY took 10.67 seconds
4157> DEFINE BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/admit-build.modus-ponens-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
4158> VERIFY BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-build.modus-ponens-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4159> VERIFY BOOLEANP-OF-BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.modus-ponens-okp.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.73 seconds
;; VERIFY took 1.12 seconds
4160> VERIFY BUILD.MODUS-PONENS-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.modus-ponens-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.31 seconds
4161> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.modus-ponens-okp.proof
; [GC threshold exceeded with 18,595,056 bytes in use.  Commencing GC.]
; [GC completed with 9,544,064 bytes retained and 9,050,992 bytes freed.]
; [GC will next occur when at least 21,544,064 bytes are in use.]
;; Reading the file took 0.23 seconds
;; Checking the proof took 9.62 seconds
;; VERIFY took 14.49 seconds
4162> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.modus-ponens-okp.proof
; [GC threshold exceeded with 21,553,008 bytes in use.  Commencing GC.]
; [GC completed with 9,105,824 bytes retained and 12,447,184 bytes freed.]
; [GC will next occur when at least 21,105,824 bytes are in use.]
;; Reading the file took 0.16 seconds
;; Checking the proof took 4.62 seconds
;; VERIFY took 6.90 seconds
4163> VERIFY FORCING-SOUNDNESS-OF-BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.modus-ponens-okp.proof
; [GC threshold exceeded with 21,121,344 bytes in use.  Commencing GC.]
; [GC completed with 13,303,256 bytes retained and 7,818,088 bytes freed.]
; [GC will next occur when at least 25,303,256 bytes are in use.]
; [GC threshold exceeded with 27,011,504 bytes in use.  Commencing GC.]
; [GC completed with 18,061,400 bytes retained and 8,950,104 bytes freed.]
; [GC will next occur when at least 30,061,400 bytes are in use.]
;; Reading the file took 0.51 seconds
;; Checking the proof took 6.04 seconds
;; VERIFY took 9.58 seconds
4164> DEFINE BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/admit-build.modus-ponens-2.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.02 seconds
4165> VERIFY BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/thm-build.modus-ponens-2.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4166> VERIFY BUILD.MODUS-PONENS-2-UNDER-IFF
;; Reading from Proofs/level2/thm-build.modus-ponens-2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4167> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.modus-ponens-2.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.67 seconds
;; VERIFY took 1.02 seconds
4168> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.modus-ponens-2.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.12 seconds
4169> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.modus-ponens-2.proof
; [GC threshold exceeded with 30,074,928 bytes in use.  Commencing GC.]
; [GC completed with 24,030,064 bytes retained and 6,044,864 bytes freed.]
; [GC will next occur when at least 36,030,064 bytes are in use.]
;; Reading the file took 0.18 seconds
;; Checking the proof took 7.98 seconds
;; VERIFY took 11.97 seconds
4170> DEFINE BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/admit-build.modus-ponens-2-okp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4171> VERIFY BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-build.modus-ponens-2-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4172> VERIFY BOOLEANP-OF-BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.modus-ponens-2-okp.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.71 seconds
;; VERIFY took 1.08 seconds
4173> VERIFY BUILD.MODUS-PONENS-2-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.modus-ponens-2-okp-of-logic.appeal-identity.proof
; [GC threshold exceeded with 36,045,944 bytes in use.  Commencing GC.]
; [GC completed with 4,733,608 bytes retained and 31,312,336 bytes freed.]
; [GC will next occur when at least 16,733,608 bytes are in use.]
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.35 seconds
4174> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.modus-ponens-2-okp.proof
; [GC threshold exceeded with 17,754,712 bytes in use.  Commencing GC.]
; [GC completed with 11,225,168 bytes retained and 6,529,544 bytes freed.]
; [GC will next occur when at least 23,225,168 bytes are in use.]
;; Reading the file took 0.24 seconds
;; Checking the proof took 9.65 seconds
;; VERIFY took 14.48 seconds
4175> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.modus-ponens-2-okp.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 5.61 seconds
;; VERIFY took 8.35 seconds
4176> VERIFY FORCING-SOUNDNESS-OF-BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.modus-ponens-2-okp.proof
; [GC threshold exceeded with 23,235,544 bytes in use.  Commencing GC.]
; [GC completed with 8,006,360 bytes retained and 15,229,184 bytes freed.]
; [GC will next occur when at least 20,006,360 bytes are in use.]
; [GC threshold exceeded with 23,309,144 bytes in use.  Commencing GC.]
; [GC completed with 13,850,912 bytes retained and 9,458,232 bytes freed.]
; [GC will next occur when at least 25,850,912 bytes are in use.]
;; Reading the file took 0.50 seconds
;; Checking the proof took 5.91 seconds
;; VERIFY took 9.41 seconds
4177> DEFINE BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.right-associativity.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
4178> VERIFY BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.right-associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4179> VERIFY BUILD.RIGHT-ASSOCIATIVITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.right-associativity-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
4180> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.right-associativity.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 2.53 seconds
;; VERIFY took 3.57 seconds
4181> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.right-associativity.proof
; [GC threshold exceeded with 25,856,200 bytes in use.  Commencing GC.]
; [GC completed with 10,710,592 bytes retained and 15,145,608 bytes freed.]
; [GC will next occur when at least 22,710,592 bytes are in use.]
; [GC threshold exceeded with 26,110,416 bytes in use.  Commencing GC.]
; [GC completed with 17,818,528 bytes retained and 8,291,888 bytes freed.]
; [GC will next occur when at least 29,818,528 bytes are in use.]
;; Reading the file took 0.35 seconds
;; Checking the proof took 22.54 seconds
;; VERIFY took 31.09 seconds
4182> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.right-associativity.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 4.02 seconds
;; VERIFY took 5.70 seconds
4183> DEFINE BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/admit-build.right-associativity-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.02 seconds
4184> VERIFY BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-build.right-associativity-okp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
4185> VERIFY BOOLEANP-OF-BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.right-associativity-okp.proof
; [GC threshold exceeded with 30,138,624 bytes in use.  Commencing GC.]
; [GC completed with 6,710,264 bytes retained and 23,428,360 bytes freed.]
; [GC will next occur when at least 18,710,264 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 1.68 seconds
;; VERIFY took 2.67 seconds
4186> VERIFY BUILD.RIGHT-ASSOCIATIVITY-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.right-associativity-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.35 seconds
;; VERIFY took 0.48 seconds
4187> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.right-associativity-okp.proof
; [GC threshold exceeded with 19,837,544 bytes in use.  Commencing GC.]
; [GC completed with 14,065,496 bytes retained and 5,772,048 bytes freed.]
; [GC will next occur when at least 26,065,496 bytes are in use.]
;; Reading the file took 0.20 seconds
;; Checking the proof took 13.33 seconds
;; VERIFY took 20.33 seconds
4188> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.right-associativity-okp.proof
; [GC threshold exceeded with 28,433,616 bytes in use.  Commencing GC.]
; [GC completed with 13,843,400 bytes retained and 14,590,216 bytes freed.]
; [GC will next occur when at least 25,843,400 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 7.66 seconds
;; VERIFY took 11.71 seconds
4189> VERIFY FORCING-SOUNDNESS-OF-BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.right-associativity-okp.proof
; [GC threshold exceeded with 28,163,256 bytes in use.  Commencing GC.]
; [GC completed with 20,849,168 bytes retained and 7,314,088 bytes freed.]
; [GC will next occur when at least 32,849,168 bytes are in use.]
;; Reading the file took 0.35 seconds
;; Checking the proof took 3.67 seconds
;; VERIFY took 5.85 seconds
4190> DEFINE BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/admit-build.disjoined-left-expansion.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X B): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4191> VERIFY BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/thm-build.disjoined-left-expansion.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4192> VERIFY BUILD.DISJOINED-LEFT-EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-left-expansion-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
4193> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-left-expansion.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 0.48 seconds
4194> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-left-expansion.proof
; [GC threshold exceeded with 32,957,888 bytes in use.  Commencing GC.]
; [GC completed with 3,679,752 bytes retained and 29,278,136 bytes freed.]
; [GC will next occur when at least 15,679,752 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 3.28 seconds
;; VERIFY took 4.63 seconds
4195> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-left-expansion.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.52 seconds
;; VERIFY took 0.81 seconds
4196> DEFINE BUILD.DISJOINED-LEFT-EXPANSION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-left-expansion-okp.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.05 seconds
4197> VERIFY BUILD.DISJOINED-LEFT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-build.disjoined-left-expansion-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4198> VERIFY BOOLEANP-OF-BUILD.DISJOINED-LEFT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-left-expansion-okp.proof
; [GC threshold exceeded with 15,689,016 bytes in use.  Commencing GC.]
; [GC completed with 6,541,768 bytes retained and 9,147,248 bytes freed.]
; [GC will next occur when at least 18,541,768 bytes are in use.]
;; Reading the file took 0.16 seconds
;; Checking the proof took 1.36 seconds
;; VERIFY took 2.19 seconds
4199> VERIFY BUILD.DISJOINED-LEFT-EXPANSION-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-left-expansion-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.29 seconds
;; VERIFY took 0.39 seconds
4200> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.DISJOINED-LEFT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.disjoined-left-expansion-okp.proof
; [GC threshold exceeded with 18,552,920 bytes in use.  Commencing GC.]
; [GC completed with 9,411,576 bytes retained and 9,141,344 bytes freed.]
; [GC will next occur when at least 21,411,576 bytes are in use.]
;; Reading the file took 
; [GC threshold exceeded with 21,514,848 bytes in use.  Commencing GC.]
; [GC completed with 13,667,976 bytes retained and 7,846,872 bytes freed.]
; [GC will next occur when at least 25,667,976 bytes are in use.]
0.33 seconds
;; Checking the proof took 18.74 seconds
;; VERIFY took 28.83 seconds
4201> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.DISJOINED-LEFT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.disjoined-left-expansion-okp.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 4.84 seconds
;; VERIFY took 7.43 seconds
4202> VERIFY FORCING-SOUNDNESS-OF-BUILD.DISJOINED-LEFT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.disjoined-left-expansion-okp.proof
; [GC threshold exceeded with 25,880,096 bytes in use.  Commencing GC.]
; [GC completed with 13,242,864 bytes retained and 12,637,232 bytes freed.]
; [GC will next occur when at least 25,242,864 bytes are in use.]
; [GC threshold exceeded with 27,146,016 bytes in use.  Commencing GC.]
; [GC completed with 19,089,624 bytes retained and 8,056,392 bytes freed.]
; [GC will next occur when at least 31,089,624 bytes are in use.]
;; Reading the file took 0.42 seconds
;; Checking the proof took 3.38 seconds
;; VERIFY took 5.48 seconds
4203> DEFINE BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/admit-build.disjoined-right-expansion.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X B): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4204> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-build.disjoined-right-expansion.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4205> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-right-expansion-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4206> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-right-expansion.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 1.22 seconds
;; VERIFY took 1.81 seconds
4207> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-right-expansion.proof
; [GC threshold exceeded with 31,098,472 bytes in use.  Commencing GC.]
; [GC completed with 7,049,448 bytes retained and 24,049,024 bytes freed.]
; [GC will next occur when at least 19,049,448 bytes are in use.]
; [GC threshold exceeded with 21,425,976 bytes in use.  Commencing GC.]
; [GC completed with 13,657,048 bytes retained and 7,768,928 bytes freed.]
; [GC will next occur when at least 25,657,048 bytes are in use.]
;; Reading the file took 0.32 seconds
;; Checking the proof took 6.04 seconds
;; VERIFY took 8.66 seconds
4208> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-right-expansion.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 2.12 seconds
;; VERIFY took 3.13 seconds
4209> DEFINE BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-right-expansion-okp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.02 seconds
4210> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-build.disjoined-right-expansion-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4211> VERIFY BOOLEANP-OF-BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-right-expansion-okp.proof
; [GC threshold exceeded with 26,181,920 bytes in use.  Commencing GC.]
; [GC completed with 13,190,880 bytes retained and 12,991,040 bytes freed.]
; [GC will next occur when at least 25,190,880 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 1.38 seconds
;; VERIFY took 2.24 seconds
4212> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-right-expansion-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.28 seconds
;; VERIFY took 0.38 seconds
4213> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.disjoined-right-expansion-okp.proof
; [GC threshold exceeded with 27,598,872 bytes in use.  Commencing GC.]
; [GC completed with 19,998,864 bytes retained and 7,600,008 bytes freed.]
; [GC will next occur when at least 31,998,864 bytes are in use.]
;; Reading the file took 0.31 seconds
;; Checking the proof took 19.04 seconds
;; VERIFY took 29.07 seconds
4214> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.disjoined-right-expansion-okp.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 4.97 seconds
;; VERIFY took 7.55 seconds
4215> VERIFY FORCING-SOUNDNESS-OF-BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.disjoined-right-expansion-okp.proof
; [GC threshold exceeded with 32,007,784 bytes in use.  Commencing GC.]
; [GC completed with 6,696,424 bytes retained and 25,311,360 bytes freed.]
; [GC will next occur when at least 18,696,424 bytes are in use.]
; [GC threshold exceeded with 20,802,648 bytes in use.  Commencing GC.]
; [GC completed with 13,624,568 bytes retained and 7,178,080 bytes freed.]
; [GC will next occur when at least 25,624,568 bytes are in use.]
;; Reading the file took 0.42 seconds
;; Checking the proof took 3.38 seconds
;; VERIFY took 5.51 seconds
4216> DEFINE BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/admit-build.disjoined-contraction.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
4217> VERIFY BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/thm-build.disjoined-contraction.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
4218> VERIFY BUILD.DISJOINED-CONTRACTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-contraction-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4219> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-contraction.proof
; [GC threshold exceeded with 25,641,208 bytes in use.  Commencing GC.]
; [GC completed with 11,628,784 bytes retained and 14,012,424 bytes freed.]
; [GC will next occur when at least 23,628,784 bytes are in use.]
;; Reading the file took 0.14 seconds
;; Checking the proof took 3.19 seconds
;; VERIFY took 4.64 seconds
4220> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-contraction.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.79 seconds
;; VERIFY took 1.20 seconds
4221> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-contraction.proof
; [GC threshold exceeded with 25,627,856 bytes in use.  Commencing GC.]
; [GC completed with 16,361,384 bytes retained and 9,266,472 bytes freed.]
; [GC will next occur when at least 28,361,384 bytes are in use.]
;; Reading the file took 0.21 seconds
;; Checking the proof took 12.59 seconds
;; VERIFY took 18.18 seconds
4222> DEFINE BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-contraction-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.02 seconds
4223> VERIFY BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/thm-build.disjoined-contraction-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4224> VERIFY BOOLEANP-OF-BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-contraction-okp.proof
; [GC threshold exceeded with 28,376,384 bytes in use.  Commencing GC.]
; [GC completed with 14,112,496 bytes retained and 14,263,888 bytes freed.]
; [GC will next occur when at least 26,112,496 bytes are in use.]
;; Reading the file took 0.14 seconds
;; Checking the proof took 1.36 seconds
;; VERIFY took 2.11 seconds
4225> VERIFY BUILD.DISJOINED-CONTRACTION-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-contraction-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.33 seconds
;; VERIFY took 0.47 seconds
4226> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.disjoined-contraction-okp.proof
; [GC threshold exceeded with 26,426,024 bytes in use.  Commencing GC.]
; [GC completed with 19,919,480 bytes retained and 6,506,544 bytes freed.]
; [GC will next occur when at least 31,919,480 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 13.77 seconds
;; VERIFY took 20.79 seconds
4227> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.disjoined-contraction-okp.proof
;; Reading the file took 
; [GC threshold exceeded with 32,312,688 bytes in use.  Commencing GC.]
; [GC completed with 13,369,152 bytes retained and 18,943,536 bytes freed.]
; [GC will next occur when at least 25,369,152 bytes are in use.]
0.16 seconds
;; Checking the proof took 10.41 seconds
;; VERIFY took 15.65 seconds
4228> VERIFY FORCING-SOUNDNESS-OF-BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.disjoined-contraction-okp.proof
; [GC threshold exceeded with 26,635,536 bytes in use.  Commencing GC.]
; [GC completed with 19,924,800 bytes retained and 6,710,736 bytes freed.]
; [GC will next occur when at least 31,924,800 bytes are in use.]
;; Reading the file took 0.44 seconds
;; Checking the proof took 6.11 seconds
;; VERIFY took 9.58 seconds
4229> DEFINE BUILD.CANCEL-NEG-NEG
; [GC threshold exceeded with 31,935,024 bytes in use.  Commencing GC.]
; [GC completed with 13,379,992 bytes retained and 18,555,032 bytes freed.]
; [GC will next occur when at least 25,379,992 bytes are in use.]
;; Reading from Proofs/level2/admit-build.cancel-neg-neg.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
4230> VERIFY BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/thm-build.cancel-neg-neg.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4231> VERIFY BUILD.CANCEL-NEG-NEG-UNDER-IFF
;; Reading from Proofs/level2/thm-build.cancel-neg-neg-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4232> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.cancel-neg-neg.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.41 seconds
;; VERIFY took 0.63 seconds
4233> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.cancel-neg-neg.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 2.23 seconds
;; VERIFY took 3.15 seconds
4234> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.cancel-neg-neg.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.54 seconds
;; VERIFY took 0.78 seconds
4235> DEFINE BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/admit-build.cancel-neg-neg-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
4236> VERIFY BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-build.cancel-neg-neg-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4237> VERIFY BOOLEANP-OF-BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.cancel-neg-neg-okp.proof
; [GC threshold exceeded with 25,391,392 bytes in use.  Commencing GC.]
; [GC completed with 14,012,096 bytes retained and 11,379,296 bytes freed.]
; [GC will next occur when at least 26,012,096 bytes are in use.]
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.48 seconds
;; VERIFY took 0.71 seconds
4238> VERIFY BUILD.CANCEL-NEG-NEG-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.cancel-neg-neg-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.23 seconds
4239> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.cancel-neg-neg-okp.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 4.51 seconds
;; VERIFY took 6.78 seconds
4240> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.cancel-neg-neg-okp.proof
; [GC threshold exceeded with 26,106,112 bytes in use.  Commencing GC.]
; [GC completed with 14,733,040 bytes retained and 11,373,072 bytes freed.]
; [GC will next occur when at least 26,733,040 bytes are in use.]
;; Reading the file took 0.13 seconds
;; Checking the proof took 3.87 seconds
;; VERIFY took 5.79 seconds
4241> VERIFY FORCING-SOUNDNESS-OF-BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.cancel-neg-neg-okp.proof
; [GC threshold exceeded with 27,177,616 bytes in use.  Commencing GC.]
; [GC completed with 20,846,752 bytes retained and 6,330,864 bytes freed.]
; [GC will next occur when at least 32,846,752 bytes are in use.]
;; Reading the file took 0.32 seconds
;; Checking the proof took 3.12 seconds
;; VERIFY took 4.95 seconds
4242> DEFINE BUILD.INSERT-NEG-NEG
;; Reading from Proofs/level2/admit-build.insert-neg-neg.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
4243> VERIFY BUILD.INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-build.insert-neg-neg.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4244> VERIFY BUILD.INSERT-NEG-NEG-UNDER-IFF
;; Reading from Proofs/level2/thm-build.insert-neg-neg-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 seconds
4245> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.insert-neg-neg.proof
;; Reading the file took 0.04 seconds
; [GC threshold exceeded with 32,908,064 bytes in use.  Commencing GC.]
; [GC completed with 1,329,936 bytes retained and 31,578,128 bytes freed.]
; [GC will next occur when at least 13,329,936 bytes are in use.]
;; Checking the proof took 0.32 seconds
;; VERIFY took 0.45 seconds
4246> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.insert-neg-neg.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 1.04 seconds
;; VERIFY took 1.38 seconds
4247> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.insert-neg-neg.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.40 seconds
;; VERIFY took 0.59 seconds
4248> DEFINE BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/admit-build.insert-neg-neg-okp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4249> VERIFY BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-build.insert-neg-neg-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4250> VERIFY BOOLEANP-OF-BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.insert-neg-neg-okp.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 0.44 seconds
;; VERIFY took 0.72 seconds
4251> VERIFY BUILD.INSERT-NEG-NEG-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.insert-neg-neg-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.22 seconds
4252> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.insert-neg-neg-okp.proof
; [GC threshold exceeded with 13,343,192 bytes in use.  Commencing GC.]
; [GC completed with 2,832,848 bytes retained and 10,510,344 bytes freed.]
; [GC will next occur when at least 14,832,848 bytes are in use.]
; [GC threshold exceeded with 18,535,328 bytes in use.  Commencing GC.]
; [GC completed with 9,577,512 bytes retained and 8,957,816 bytes freed.]
; [GC will next occur when at least 21,577,512 bytes are in use.]
;; Reading the file took 0.37 seconds
;; Checking the proof took 7.45 seconds
;; VERIFY took 11.34 seconds
4253> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.insert-neg-neg-okp.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 1.91 seconds
;; VERIFY took 2.91 seconds
4254> VERIFY FORCING-SOUNDNESS-OF-BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.insert-neg-neg-okp.proof
; [GC threshold exceeded with 21,940,592 bytes in use.  Commencing GC.]
; [GC completed with 13,146,856 bytes retained and 8,793,736 bytes freed.]
; [GC will next occur when at least 25,146,856 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 0.99 seconds
;; VERIFY took 1.65 seconds
4255> DEFINE BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/admit-build.lhs-insert-neg-neg.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
4256> VERIFY BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4257> VERIFY BUILD.LHS-INSERT-NEG-NEG-UNDER-IFF
;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4258> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.lhs-insert-neg-neg.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.60 seconds
;; VERIFY took 0.86 seconds
4259> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.lhs-insert-neg-neg.proof
; [GC threshold exceeded with 27,108,304 bytes in use.  Commencing GC.]
; [GC completed with 12,675,456 bytes retained and 14,432,848 bytes freed.]
; [GC will next occur when at least 24,675,456 bytes are in use.]
;; Reading the file took 0.20 seconds
;; Checking the proof took 3.34 seconds
;; VERIFY took 4.60 seconds
4260> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.lhs-insert-neg-neg.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 1.13 seconds
;; VERIFY took 1.62 seconds
4261> DEFINE BUILD.LHS-INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/admit-build.lhs-insert-neg-neg-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; [GC threshold exceeded with 24,683,808 bytes in use.  Commencing GC.]
; [GC completed with 13,377,416 bytes retained and 11,306,392 bytes freed.]
; [GC will next occur when at least 25,377,416 bytes are in use.]
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.02 seconds
4262> VERIFY BUILD.LHS-INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4263> VERIFY BOOLEANP-OF-BUILD.LHS-INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.lhs-insert-neg-neg-okp.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 1.25 seconds
;; VERIFY took 1.93 seconds
4264> VERIFY BUILD.LHS-INSERT-NEG-NEG-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 0.41 seconds
4265> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.LHS-INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.lhs-insert-neg-neg-okp.proof
; [GC threshold exceeded with 25,603,608 bytes in use.  Commencing GC.]
; [GC completed with 5,079,424 bytes retained and 20,524,184 bytes freed.]
; [GC will next occur when at least 17,079,424 bytes are in use.]
; [GC threshold exceeded with 18,947,200 bytes in use.  Commencing GC.]
; [GC completed with 10,810,176 bytes retained and 8,137,024 bytes freed.]
; [GC will next occur when at least 22,810,176 bytes are in use.]
; [GC threshold exceeded with 27,458,560 bytes in use.  Commencing GC.]
; [GC completed with 15,849,776 bytes retained and 11,608,784 bytes freed.]
; [GC will next occur when at least 27,849,776 bytes are in use.]
;; Reading the file took 0.75 seconds
;; Checking the proof took 25.46 seconds
;; VERIFY took 38.61 seconds
4266> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.LHS-INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.lhs-insert-neg-neg-okp.proof
;; Reading the file took 0.15 seconds
;; Checking the proof took 5.04 seconds
;; VERIFY took 7.62 seconds
4267> VERIFY FORCING-SOUNDNESS-OF-BUILD.LHS-INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.lhs-insert-neg-neg-okp.proof
; [GC threshold exceeded with 28,208,648 bytes in use.  Commencing GC.]
; [GC completed with 19,061,448 bytes retained and 9,147,200 bytes freed.]
; [GC will next occur when at least 31,061,448 bytes are in use.]
;; Reading the file took 0.32 seconds
; [GC threshold exceeded with 31,380,232 bytes in use.  Commencing GC.]
; [GC completed with 8,709,920 bytes retained and 22,670,312 bytes freed.]
; [GC will next occur when at least 20,709,920 bytes are in use.]
;; Checking the proof took 2.36 seconds
;; VERIFY took 3.86 seconds
4268> DEFINE BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/admit-build.merge-negatives.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4269> VERIFY BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/thm-build.merge-negatives.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4270> VERIFY BUILD.MERGE-NEGATIVES-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-negatives-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4271> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.merge-negatives.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 15.16 seconds
;; VERIFY took 21.55 seconds
4272> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.merge-negatives.proof
; [GC threshold exceeded with 20,726,000 bytes in use.  Commencing GC.]
; [GC completed with 12,387,448 bytes retained and 8,338,552 bytes freed.]
; [GC will next occur when at least 24,387,448 bytes are in use.]
; [GC threshold exceeded with 25,792,776 bytes in use.  Commencing GC.]
; [GC completed with 17,015,352 bytes retained and 8,777,424 bytes freed.]
; [GC will next occur when at least 29,015,352 bytes are in use.]
;; Reading the file took 0.40 seconds
;; Checking the proof took 37.38 seconds
;; VERIFY took 53.16 seconds
4273> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.merge-negatives.proof
; [GC threshold exceeded with 29,241,648 bytes in use.  Commencing GC.]
; [GC completed with 23,821,576 bytes retained and 5,420,072 bytes freed.]
; [GC will next occur when at least 35,821,576 bytes are in use.]
;; Reading the file took 0.14 seconds
;; Checking the proof took 21.14 seconds
;; VERIFY took 30.77 seconds
4274> DEFINE BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/admit-build.merge-negatives-okp.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.03 seconds
4275> VERIFY BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/thm-build.merge-negatives-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4276> VERIFY BOOLEANP-OF-BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.merge-negatives-okp.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 1.32 seconds
;; VERIFY took 2.00 seconds
4277> VERIFY BUILD.MERGE-NEGATIVES-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.merge-negatives-okp-of-logic.appeal-identity.proof
; [GC threshold exceeded with 35,832,968 bytes in use.  Commencing GC.]
; [GC completed with 23,021,016 bytes retained and 12,811,952 bytes freed.]
; [GC will next occur when at least 35,021,016 bytes are in use.]
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.32 seconds
;; VERIFY took 0.45 seconds
4278> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.merge-negatives-okp.proof
; [GC threshold exceeded with 36,498,416 bytes in use.  Commencing GC.]
; [GC completed with 29,441,560 bytes retained and 7,056,856 bytes freed.]
; [GC will next occur when at least 41,441,560 bytes are in use.]
;; Reading the file took 0.27 seconds
;; Checking the proof took 11.85 seconds
;; VERIFY took 17.73 seconds
4279> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.merge-negatives-okp.proof
; [GC threshold exceeded with 42,618,528 bytes in use.  Commencing GC.]
; [GC completed with 14,176,904 bytes retained and 28,441,624 bytes freed.]
; [GC will next occur when at least 26,176,904 bytes are in use.]
;; Reading the file took 0.21 seconds
;; Checking the proof took 5.74 seconds
;; VERIFY took 8.60 seconds
4280> VERIFY FORCING-SOUNDNESS-OF-BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.merge-negatives-okp.proof
; [GC threshold exceeded with 26,269,424 bytes in use.  Commencing GC.]
; [GC completed with 21,572,808 bytes retained and 4,696,616 bytes freed.]
; [GC will next occur when at least 33,572,808 bytes are in use.]
; [GC threshold exceeded with 36,422,400 bytes in use.  Commencing GC.]
; [GC completed with 26,388,528 bytes retained and 10,033,872 bytes freed.]
; [GC will next occur when at least 38,388,528 bytes are in use.]
;; Reading the file took 0.48 seconds
;; Checking the proof took 4.57 seconds
;; VERIFY took 7.23 seconds
4281> DEFINE BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/admit-build.merge-implications-lemma-1.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X A): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4282> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-1.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4283> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-1-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 seconds
4284> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.merge-implications-lemma-1.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 14.47 seconds
;; VERIFY took 20.46 seconds
4285> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.merge-implications-lemma-1.proof
; [GC threshold exceeded with 38,403,344 bytes in use.  Commencing GC.]
; [GC completed with 29,471,808 bytes retained and 8,931,536 bytes freed.]
; [GC will next occur when at least 41,471,808 bytes are in use.]
; [GC threshold exceeded with 45,158,632 bytes in use.  Commencing GC.]
; [GC completed with 17,413,648 bytes retained and 27,744,984 bytes freed.]
; [GC will next occur when at least 29,413,648 bytes are in use.]
;; Reading the file took 0.57 seconds
; [GC threshold exceeded with 30,562,976 bytes in use.  Commencing GC.]
; [GC completed with 25,308,512 bytes retained and 5,254,464 bytes freed.]
; [GC will next occur when at least 37,308,512 bytes are in use.]
;; Checking the proof took 44.83 seconds
;; VERIFY took 63.44 seconds
4286> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.merge-implications-lemma-1.proof
;; Reading the file took 0.13 seconds
; [GC threshold exceeded with 37,319,008 bytes in use.  Commencing GC.]
; [GC completed with 27,158,344 bytes retained and 10,160,664 bytes freed.]
; [GC will next occur when at least 39,158,344 bytes are in use.]
;; Checking the proof took 24.80 seconds
;; VERIFY took 35.62 seconds
4287> DEFINE BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/admit-build.merge-implications-lemma-2.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4288> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-2.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
4289> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-2-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4290> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.merge-implications-lemma-2.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 11.84 seconds
;; VERIFY took 16.89 seconds
4291> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.merge-implications-lemma-2.proof
; [GC threshold exceeded with 39,173,152 bytes in use.  Commencing GC.]
; [GC completed with 31,270,248 bytes retained and 7,902,904 bytes freed.]
; [GC will next occur when at least 43,270,248 bytes are in use.]
;; Reading the file took 0.34 seconds
; [GC threshold exceeded with 43,281,592 bytes in use.  Commencing GC.]
; [GC completed with 31,558,680 bytes retained and 11,722,912 bytes freed.]
; [GC will next occur when at least 43,558,680 bytes are in use.]
;; Checking the proof took 52.11 seconds
;; VERIFY took 76.05 seconds
4292> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.merge-implications-lemma-2.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 14.76 seconds
;; VERIFY took 21.41 seconds
4293> DEFINE BUILD.MERGE-IMPLICATIONS
;; Reading from Proofs/level2/admit-build.merge-implications.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4294> VERIFY BUILD.MERGE-IMPLICATIONS
;; Reading from Proofs/level2/thm-build.merge-implications.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4295> VERIFY BUILD.MERGE-IMPLICATIONS-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-implications-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
4296> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MERGE-IMPLICATIONS
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.merge-implications.proof
; [GC threshold exceeded with 44,043,680 bytes in use.  Commencing GC.]
; [GC completed with 33,118,024 bytes retained and 10,925,656 bytes freed.]
; [GC will next occur when at least 45,118,024 bytes are in use.]
;; Reading the file took 0.08 seconds
;; Checking the proof took 1.26 seconds
;; VERIFY took 1.83 seconds
4297> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.MERGE-IMPLICATIONS
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.merge-implications.proof
; [GC threshold exceeded with 47,200,872 bytes in use.  Commencing GC.]
; [GC completed with 32,086,472 bytes retained and 15,114,400 bytes freed.]
; [GC will next occur when at least 44,086,472 bytes are in use.]
;; Reading the file took 0.39 seconds
;; Checking the proof took 20.78 seconds
;; VERIFY took 30.30 seconds
4298> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.MERGE-IMPLICATIONS
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.merge-implications.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 1.63 seconds
;; VERIFY took 2.40 seconds
4299> DEFINE BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/admit-build.merge-implications-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.02 seconds
4300> VERIFY BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/thm-build.merge-implications-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4301> VERIFY BOOLEANP-OF-BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.merge-implications-okp.proof
; [GC threshold exceeded with 44,101,192 bytes in use.  Commencing GC.]
; [GC completed with 36,096,944 bytes retained and 8,004,248 bytes freed.]
; [GC will next occur when at least 48,096,944 bytes are in use.]
; [GC threshold exceeded with 48,809,960 bytes in use.  Commencing GC.]
; [GC completed with 42,371,912 bytes retained and 6,438,048 bytes freed.]
; [GC will next occur when at least 54,371,912 bytes are in use.]
;; Reading the file took 0.35 seconds
;; Checking the proof took 5.19 seconds
;; VERIFY took 8.13 seconds
4302> VERIFY BUILD.MERGE-IMPLICATIONS-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.merge-implications-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.70 seconds
;; VERIFY took 0.90 seconds
4303> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.merge-implications-okp.proof
; [GC threshold exceeded with 54,386,488 bytes in use.  Commencing GC.]
; [GC completed with 49,936,152 bytes retained and 4,450,336 bytes freed.]
; [GC will next occur when at least 61,936,152 bytes are in use.]
; [GC threshold exceeded with 65,704,632 bytes in use.  Commencing GC.]
; [GC completed with 34,800,032 bytes retained and 30,904,600 bytes freed.]
; [GC will next occur when at least 46,800,032 bytes are in use.]
;; Reading the file took 0.51 seconds
;; Checking the proof took 44.59 seconds
;; VERIFY took 66.48 seconds
4304> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.merge-implications-okp.proof
; [GC threshold exceeded with 48,277,216 bytes in use.  Commencing GC.]
; [GC completed with 41,439,848 bytes retained and 6,837,368 bytes freed.]
; [GC will next occur when at least 53,439,848 bytes are in use.]
;; Reading the file took 0.25 seconds
;; Checking the proof took 19.72 seconds
;; VERIFY took 29.32 seconds
4305> VERIFY FORCING-SOUNDNESS-OF-BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.merge-implications-okp.proof
; [GC threshold exceeded with 53,455,016 bytes in use.  Commencing GC.]
; [GC completed with 40,661,968 bytes retained and 12,793,048 bytes freed.]
; [GC will next occur when at least 52,661,968 bytes are in use.]
; [GC threshold exceeded with 57,393,384 bytes in use.  Commencing GC.]
; [GC completed with 46,389,432 bytes retained and 11,003,952 bytes freed.]
; [GC will next occur when at least 58,389,432 bytes are in use.]
;; Reading the file took 0.73 seconds
;; Checking the proof took 13.47 seconds
;; VERIFY took 20.63 seconds
4306> DEFINE BUILD.DISJOINED-COMMUTE-OR-LEMMA-1
;; Reading from Proofs/level2/admit-build.disjoined-commute-or-lemma-1.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
4307> VERIFY BUILD.DISJOINED-COMMUTE-OR-LEMMA-1
;; Reading from Proofs/level2/thm-build.disjoined-commute-or-lemma-1.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4308> VERIFY BUILD.DISJOINED-COMMUTE-OR-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-commute-or-lemma-1-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4309> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-COMMUTE-OR-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-commute-or-lemma-1.proof
; [GC threshold exceeded with 58,480,008 bytes in use.  Commencing GC.]
; [GC completed with 35,771,400 bytes retained and 22,708,608 bytes freed.]
; [GC will next occur when at least 47,771,400 bytes are in use.]
;; Reading the file took 0.11 seconds
;; Checking the proof took 10.49 seconds
;; VERIFY took 14.96 seconds
4310> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-COMMUTE-OR-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-commute-or-lemma-1.proof
; [GC threshold exceeded with 48,143,552 bytes in use.  Commencing GC.]
; [GC completed with 41,555,128 bytes retained and 6,588,424 bytes freed.]
; [GC will next occur when at least 53,555,128 bytes are in use.]
;; Reading the file took 0.31 seconds
;; Checking the proof took 26.52 seconds
;; VERIFY took 37.39 seconds
4311> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-COMMUTE-OR-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-commute-or-lemma-1.proof
; [GC threshold exceeded with 53,565,360 bytes in use.  Commencing GC.]
; [GC completed with 38,793,144 bytes retained and 14,772,216 bytes freed.]
; [GC will next occur when at least 50,793,144 bytes are in use.]
;; Reading the file took 0.13 seconds
;; Checking the proof took 16.61 seconds
;; VERIFY took 23.83 seconds
4312> DEFINE BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/admit-build.disjoined-commute-or.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
4313> VERIFY BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/thm-build.disjoined-commute-or.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4314> VERIFY BUILD.DISJOINED-COMMUTE-OR-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-commute-or-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 seconds
4315> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-commute-or.proof
; [GC threshold exceeded with 51,850,512 bytes in use.  Commencing GC.]
; [GC completed with 41,718,192 bytes retained and 10,132,320 bytes freed.]
; [GC will next occur when at least 53,718,192 bytes are in use.]
;; Reading the file took 0.16 seconds
;; Checking the proof took 14.41 seconds
;; VERIFY took 20.13 seconds
4316> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-commute-or.proof
; [GC threshold exceeded with 55,341,528 bytes in use.  Commencing GC.]
; [GC completed with 45,089,072 bytes retained and 10,252,456 bytes freed.]
; [GC will next occur when at least 57,089,072 bytes are in use.]
;; Reading the file took 0.26 seconds
;; Checking the proof took 57.91 seconds
;; VERIFY took 78.38 seconds
4317> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-commute-or.proof
; [GC threshold exceeded with 58,379,336 bytes in use.  Commencing GC.]
; [GC completed with 47,940,392 bytes retained and 10,438,944 bytes freed.]
; [GC will next occur when at least 59,940,392 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 17.56 seconds
;; VERIFY took 24.81 seconds
4318> DEFINE BUILD.DISJOINED-COMMUTE-OR-OKP
;; Reading from Proofs/level2/admit-build.disjoined-commute-or-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
4319> VERIFY BUILD.DISJOINED-COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-build.disjoined-commute-or-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4320> VERIFY BOOLEANP-OF-BUILD.DISJOINED-COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-commute-or-okp.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 1.81 seconds
;; VERIFY took 2.75 seconds
4321> VERIFY BUILD.DISJOINED-COMMUTE-OR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-commute-or-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.38 seconds
;; VERIFY took 0.51 seconds
4322> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.DISJOINED-COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.disjoined-commute-or-okp.proof
; [GC threshold exceeded with 59,950,104 bytes in use.  Commencing GC.]
; [GC completed with 2,160,776 bytes retained and 57,789,328 bytes freed.]
; [GC will next occur when at least 14,160,776 bytes are in use.]
;; Reading the file took 0.22 seconds
;; Checking the proof took 14.43 seconds
;; VERIFY took 21.47 seconds
4323> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.DISJOINED-COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.disjoined-commute-or-okp.proof
; [GC threshold exceeded with 14,173,896 bytes in use.  Commencing GC.]
; [GC completed with 5,495,840 bytes retained and 8,678,056 bytes freed.]
; [GC will next occur when at least 17,495,840 bytes are in use.]
;; Reading the file took 0.20 seconds
;; Checking the proof took 8.27 seconds
;; VERIFY took 12.34 seconds
4324> VERIFY FORCING-SOUNDNESS-OF-BUILD.DISJOINED-COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.disjoined-commute-or-okp.proof
; [GC threshold exceeded with 17,510,048 bytes in use.  Commencing GC.]
; [GC completed with 6,300,128 bytes retained and 11,209,920 bytes freed.]
; [GC will next occur when at least 18,300,128 bytes are in use.]
; [GC threshold exceeded with 19,702,752 bytes in use.  Commencing GC.]
; [GC completed with 13,035,344 bytes retained and 6,667,408 bytes freed.]
; [GC will next occur when at least 25,035,344 bytes are in use.]
;; Reading the file took 0.36 seconds
;; Checking the proof took 3.87 seconds
;; VERIFY took 6.06 seconds
4325> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-1A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-1a.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (B C X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4326> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1A
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1a.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4327> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1A-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1a-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 seconds
4328> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-1A
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-1a.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 7.74 seconds
;; VERIFY took 10.96 seconds
4329> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-ASSOC-LEMMA-1A
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-assoc-lemma-1a.proof
; [GC threshold exceeded with 25,045,216 bytes in use.  Commencing GC.]
; [GC completed with 11,001,896 bytes retained and 14,043,320 bytes freed.]
; [GC will next occur when at least 23,001,896 bytes are in use.]
; [GC threshold exceeded with 27,060,216 bytes in use.  Commencing GC.]
; [GC completed with 18,552,592 bytes retained and 8,507,624 bytes freed.]
; [GC will next occur when at least 30,552,592 bytes are in use.]
;; Reading the file took 0.38 seconds
;; Checking the proof took 42.85 seconds
;; VERIFY took 60.26 seconds
4330> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-ASSOC-LEMMA-1A
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-assoc-lemma-1a.proof
; [GC threshold exceeded with 31,008,088 bytes in use.  Commencing GC.]
; [GC completed with 6,806,024 bytes retained and 24,202,064 bytes freed.]
; [GC will next occur when at least 18,806,024 bytes are in use.]
;; Reading the file took 0.11 seconds
;; Checking the proof took 13.40 seconds
;; VERIFY took 19.34 seconds
4331> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-1.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A B C D): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4332> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4333> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4334> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-1.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 2.88 seconds
;; VERIFY took 4.01 seconds
4335> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-assoc-lemma-1.proof
; [GC threshold exceeded with 18,821,808 bytes in use.  Commencing GC.]
; [GC completed with 11,038,072 bytes retained and 7,783,736 bytes freed.]
; [GC will next occur when at least 23,038,072 bytes are in use.]
;; Reading the file took 0.28 seconds
; [GC threshold exceeded with 23,639,200 bytes in use.  Commencing GC.]
; [GC completed with 15,190,840 bytes retained and 8,448,360 bytes freed.]
; [GC will next occur when at least 27,190,840 bytes are in use.]
;; Checking the proof took 13.49 seconds
;; VERIFY took 18.61 seconds
4336> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-assoc-lemma-1.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 5.60 seconds
;; VERIFY took 8.01 seconds
4337> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-2a.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A D X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4338> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2a.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4339> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2A-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2a-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4340> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-2a.proof
;; Reading the file took 0.07 seconds
; [GC threshold exceeded with 27,439,424 bytes in use.  Commencing GC.]
; [GC completed with 16,985,952 bytes retained and 10,453,472 bytes freed.]
; [GC will next occur when at least 28,985,952 bytes are in use.]
;; Checking the proof took 9.47 seconds
;; VERIFY took 13.58 seconds
4341> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-assoc-lemma-2a.proof
; [GC threshold exceeded with 30,234,096 bytes in use.  Commencing GC.]
; [GC completed with 11,676,768 bytes retained and 18,557,328 bytes freed.]
; [GC will next occur when at least 23,676,768 bytes are in use.]
;; Reading the file took 0.38 seconds
; [GC threshold exceeded with 23,686,616 bytes in use.  Commencing GC.]
; [GC completed with 16,943,480 bytes retained and 6,743,136 bytes freed.]
; [GC will next occur when at least 28,943,480 bytes are in use.]
;; Checking the proof took 28.95 seconds
;; VERIFY took 41.26 seconds
4342> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-assoc-lemma-2a.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 16.55 seconds
;; VERIFY took 24.10 seconds
4343> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-2
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-2.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A B C D): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4344> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4345> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4346> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-2.proof
; [GC threshold exceeded with 29,167,376 bytes in use.  Commencing GC.]
; [GC completed with 18,442,912 bytes retained and 10,724,464 bytes freed.]
; [GC will next occur when at least 30,442,912 bytes are in use.]
;; Reading the file took 0.07 seconds
;; Checking the proof took 2.96 seconds
;; VERIFY took 4.11 seconds
4347> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-ASSOC-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-assoc-lemma-2.proof
; [GC threshold exceeded with 32,418,200 bytes in use.  Commencing GC.]
; [GC completed with 25,190,656 bytes retained and 7,227,544 bytes freed.]
; [GC will next occur when at least 37,190,656 bytes are in use.]
;; Reading the file took 0.28 seconds
;; Checking the proof took 13.56 seconds
;; VERIFY took 18.71 seconds
4348> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-ASSOC-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-assoc-lemma-2.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 5.63 seconds
;; VERIFY took 8.08 seconds
4349> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-3A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-3a.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A B C D): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4350> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-3A
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-3a.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4351> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-3A-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-3a-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4352> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-3A
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-3a.proof
; [GC threshold exceeded with 37,205,240 bytes in use.  Commencing GC.]
; [GC completed with 17,932,232 bytes retained and 19,273,008 bytes freed.]
; [GC will next occur when at least 29,932,232 bytes are in use.]
;; Reading the file took 0.13 seconds
;; Checking the proof took 2.35 seconds
;; VERIFY took 3.27 seconds
4353> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-ASSOC-LEMMA-3A
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-assoc-lemma-3a.proof
; [GC threshold exceeded with 30,171,128 bytes in use.  Commencing GC.]
; [GC completed with 22,275,600 bytes retained and 7,895,528 bytes freed.]
; [GC will next occur when at least 34,275,600 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 4.40 seconds
;; VERIFY took 6.09 seconds
4354> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-ASSOC-LEMMA-3A
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-assoc-lemma-3a.proof
; [GC threshold exceeded with 34,400,456 bytes in use.  Commencing GC.]
; [GC completed with 21,979,056 bytes retained and 12,421,400 bytes freed.]
; [GC will next occur when at least 33,979,056 bytes are in use.]
;; Reading the file took 0.18 seconds
;; Checking the proof took 5.31 seconds
;; VERIFY took 7.68 seconds
4355> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-3
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-3.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
4356> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-3
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-3.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4357> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-3-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-3-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4358> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-3
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-3.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 2.28 seconds
;; VERIFY took 3.09 seconds
4359> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-ASSOC-LEMMA-3
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-assoc-lemma-3.proof
; [GC threshold exceeded with 33,994,808 bytes in use.  Commencing GC.]
; [GC completed with 24,680,824 bytes retained and 9,313,984 bytes freed.]
; [GC will next occur when at least 36,680,824 bytes are in use.]
; [GC threshold exceeded with 38,637,136 bytes in use.  Commencing GC.]
; [GC completed with 23,727,232 bytes retained and 14,909,904 bytes freed.]
; [GC will next occur when at least 35,727,232 bytes are in use.]
;; Reading the file took 0.38 seconds
;; Checking the proof took 20.81 seconds
;; VERIFY took 28.86 seconds
4360> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-ASSOC-LEMMA-3
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-assoc-lemma-3.proof
; [GC threshold exceeded with 35,750,088 bytes in use.  Commencing GC.]
; [GC completed with 29,693,256 bytes retained and 6,056,832 bytes freed.]
; [GC will next occur when at least 41,693,256 bytes are in use.]
;; Reading the file took 0.09 seconds
;; Checking the proof took 2.98 seconds
;; VERIFY took 4.12 seconds
4361> DEFINE BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.disjoined-right-associativity.proofs
;; Reading the file took 0.13 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.13 seconds
4362> VERIFY BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.disjoined-right-associativity.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4363> VERIFY BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-right-associativity-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4364> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-right-associativity.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 4.35 seconds
;; VERIFY took 5.98 seconds
4365> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-right-associativity.proof
; [GC threshold exceeded with 42,089,576 bytes in use.  Commencing GC.]
; [GC completed with 32,300,736 bytes retained and 9,788,840 bytes freed.]
; [GC will next occur when at least 44,300,736 bytes are in use.]
;; 
; [GC threshold exceeded with 44,742,520 bytes in use.  Commencing GC.]
; [GC completed with 36,578,264 bytes retained and 8,164,256 bytes freed.]
; [GC will next occur when at least 48,578,264 bytes are in use.]
Reading the file took 0.27 seconds
;; Checking the proof took 53.43 seconds
;; VERIFY took 73.52 seconds
4366> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-right-associativity.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 5.65 seconds
;; VERIFY took 7.85 seconds
4367> DEFINE BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/admit-build.disjoined-right-associativity-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.02 seconds
4368> VERIFY BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-build.disjoined-right-associativity-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4369> VERIFY BOOLEANP-OF-BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-right-associativity-okp.proof
; [GC threshold exceeded with 48,590,864 bytes in use.  Commencing GC.]
; [GC completed with 29,796,800 bytes retained and 18,794,064 bytes freed.]
; [GC will next occur when at least 41,796,800 bytes are in use.]
; [GC threshold exceeded with 44,971,400 bytes in use.  Commencing GC.]
; [GC completed with 37,228,720 bytes retained and 7,742,680 bytes freed.]
; [GC will next occur when at least 49,228,720 bytes are in use.]
;; Reading the file took 0.27 seconds
;; Checking the proof took 4.11 seconds
;; VERIFY took 6.36 seconds
4370> VERIFY BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-right-associativity-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.61 seconds
;; VERIFY took 0.78 seconds
4371> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.disjoined-right-associativity-okp.proof
; [GC threshold exceeded with 50,989,016 bytes in use.  Commencing GC.]
; [GC completed with 40,762,664 bytes retained and 10,226,352 bytes freed.]
; [GC will next occur when at least 52,762,664 bytes are in use.]
;; Reading the file took 0.22 seconds
;; Checking the proof took 30.40 seconds
;; VERIFY took 44.92 seconds
4372> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.disjoined-right-associativity-okp.proof
; [GC threshold exceeded with 53,538,088 bytes in use.  Commencing GC.]
; [GC completed with 46,918,984 bytes retained and 6,619,104 bytes freed.]
; [GC will next occur when at least 58,918,984 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 16.71 seconds
;; VERIFY took 24.68 seconds
4373> VERIFY FORCING-SOUNDNESS-OF-BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.disjoined-right-associativity-okp.proof
; [GC threshold exceeded with 60,189,192 bytes in use.  Commencing GC.]
; [GC completed with 7,876,608 bytes retained and 52,312,584 bytes freed.]
; [GC will next occur when at least 19,876,608 bytes are in use.]
;; Reading the file took 0.45 seconds
; [GC threshold exceeded with 19,886,752 bytes in use.  Commencing GC.]
; [GC completed with 13,143,256 bytes retained and 6,743,496 bytes freed.]
; [GC will next occur when at least 25,143,256 bytes are in use.]
;; Checking the proof took 6.59 seconds
;; VERIFY took 10.06 seconds
4374> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-4
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-4.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
4375> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-4
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-4.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4376> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-4-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-4-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4377> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-4
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-4.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 1.40 seconds
;; VERIFY took 1.93 seconds
4378> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-ASSOC-LEMMA-4
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-assoc-lemma-4.proof
; [GC threshold exceeded with 25,414,592 bytes in use.  Commencing GC.]
; [GC completed with 18,000,984 bytes retained and 7,413,608 bytes freed.]
; [GC will next occur when at least 30,000,984 bytes are in use.]
;; Reading the file took 0.27 seconds
;; Checking the proof took 22.90 seconds
;; VERIFY took 31.56 seconds
4379> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-ASSOC-LEMMA-4
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-assoc-lemma-4.proof
; [GC threshold exceeded with 30,117,168 bytes in use.  Commencing GC.]
; [GC completed with 22,557,432 bytes retained and 7,559,736 bytes freed.]
; [GC will next occur when at least 34,557,432 bytes are in use.]
;; Reading the file took 0.06 seconds
;; Checking the proof took 1.81 seconds
;; VERIFY took 2.53 seconds
4380> DEFINE BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.disjoined-associativity.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
4381> VERIFY BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.disjoined-associativity.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4382> VERIFY BUILD.DISJOINED-ASSOCIATIVITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-associativity-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4383> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-associativity.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 3.67 seconds
;; VERIFY took 5.13 seconds
4384> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-associativity.proof
; [GC threshold exceeded with 34,571,584 bytes in use.  Commencing GC.]
; [GC completed with 25,377,664 bytes retained and 9,193,920 bytes freed.]
; [GC will next occur when at least 37,377,664 bytes are in use.]
; [GC threshold exceeded with 42,763,656 bytes in use.  Commencing GC.]
; [GC completed with 31,582,944 bytes retained and 11,180,712 bytes freed.]
; [GC will next occur when at least 43,582,944 bytes are in use.]
;; Reading the file took 0.38 seconds
;; Checking the proof took 31.01 seconds
;; VERIFY took 43.09 seconds
4385> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-associativity.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 4.79 seconds
;; VERIFY took 6.75 seconds
4386> DEFINE BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/admit-build.disjoined-associativity-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.02 seconds
4387> VERIFY BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-build.disjoined-associativity-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4388> VERIFY BOOLEANP-OF-BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-associativity-okp.proof
; [GC threshold exceeded with 45,136,304 bytes in use.  Commencing GC.]
; [GC completed with 16,775,496 bytes retained and 28,360,808 bytes freed.]
; [GC will next occur when at least 28,775,496 bytes are in use.]
;; Reading the file took 0.26 seconds
;; Checking the proof took 4.19 seconds
;; VERIFY took 6.43 seconds
4389> VERIFY BUILD.DISJOINED-ASSOCIATIVITY-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-associativity-okp-of-logic.appeal-identity.proof
; [GC threshold exceeded with 28,783,928 bytes in use.  Commencing GC.]
; [GC completed with 17,510,296 bytes retained and 11,273,632 bytes freed.]
; [GC will next occur when at least 29,510,296 bytes are in use.]
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.64 seconds
;; VERIFY took 0.82 seconds
4390> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.disjoined-associativity-okp.proof
; [GC threshold exceeded with 30,776,904 bytes in use.  Commencing GC.]
; [GC completed with 24,218,896 bytes retained and 6,558,008 bytes freed.]
; [GC will next occur when at least 36,218,896 bytes are in use.]
;; Reading the file took 0.22 seconds
;; Checking the proof took 30.67 seconds
;; VERIFY took 45.20 seconds
4391> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.disjoined-associativity-okp.proof
; [GC threshold exceeded with 36,994,160 bytes in use.  Commencing GC.]
; [GC completed with 30,326,792 bytes retained and 6,667,368 bytes freed.]
; [GC will next occur when at least 42,326,792 bytes are in use.]
;; Reading the file took 0.20 seconds
;; Checking the proof took 16.63 seconds
;; VERIFY took 24.59 seconds
4392> VERIFY FORCING-SOUNDNESS-OF-BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.disjoined-associativity-okp.proof
; [GC threshold exceeded with 43,596,696 bytes in use.  Commencing GC.]
; [GC completed with 19,542,752 bytes retained and 24,053,944 bytes freed.]
; [GC will next occur when at least 31,542,752 bytes are in use.]
;; Reading the file took 0.43 seconds
; [GC threshold exceeded with 31,557,104 bytes in use.  Commencing GC.]
; [GC completed with 24,809,592 bytes retained and 6,747,512 bytes freed.]
; [GC will next occur when at least 36,809,592 bytes are in use.]
;; Checking the proof took 6.66 seconds
;; VERIFY took 10.12 seconds
4393> DEFINE BUILD.DISJOINED-CUT-LEMMA-1
;; Reading from Proofs/level2/admit-build.disjoined-cut-lemma-1.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4394> VERIFY BUILD.DISJOINED-CUT-LEMMA-1
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-1.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4395> VERIFY BUILD.DISJOINED-CUT-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-1-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4396> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-CUT-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-cut-lemma-1.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 3.35 seconds
;; VERIFY took 4.80 seconds
4397> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-CUT-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-cut-lemma-1.proof
; [GC threshold exceeded with 36,825,768 bytes in use.  Commencing GC.]
; [GC completed with 28,921,200 bytes retained and 7,904,568 bytes freed.]
; [GC will next occur when at least 40,921,200 bytes are in use.]
; [GC threshold exceeded with 46,252,008 bytes in use.  Commencing GC.]
; [GC completed with 35,242,272 bytes retained and 11,009,736 bytes freed.]
; [GC will next occur when at least 47,242,272 bytes are in use.]
;; Reading the file took 0.40 seconds
;; Checking the proof took 24.06 seconds
;; VERIFY took 35.22 seconds
4398> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-CUT-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-cut-lemma-1.proof
; [GC threshold exceeded with 48,766,816 bytes in use.  Commencing GC.]
; [GC completed with 36,060,232 bytes retained and 12,706,584 bytes freed.]
; [GC will next occur when at least 48,060,232 bytes are in use.]
;; Reading the file took 0.22 seconds
;; Checking the proof took 50.50 seconds
;; VERIFY took 74.07 seconds
4399> DEFINE BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/admit-build.disjoined-cut-lemma-2.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4400> VERIFY BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-2.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4401> VERIFY BUILD.DISJOINED-CUT-LEMMA-2-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4402> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-cut-lemma-2.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 1.21 seconds
;; VERIFY took 1.74 seconds
4403> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-cut-lemma-2.proof
; [GC threshold exceeded with 48,073,768 bytes in use.  Commencing GC.]
; [GC completed with 40,178,304 bytes retained and 7,895,464 bytes freed.]
; [GC will next occur when at least 52,178,304 bytes are in use.]
; [GC threshold exceeded with 53,211,536 bytes in use.  Commencing GC.]
; [GC completed with 33,448,328 bytes retained and 19,763,208 bytes freed.]
; [GC will next occur when at least 45,448,328 bytes are in use.]
;; Reading the file took 0.47 seconds
;; Checking the proof took 49.85 seconds
;; VERIFY took 72.25 seconds
4404> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-cut-lemma-2.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 1.56 seconds
;; VERIFY took 2.25 seconds
4405> DEFINE BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/admit-build.disjoined-cut.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4406> VERIFY BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/thm-build.disjoined-cut.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4407> VERIFY BUILD.DISJOINED-CUT-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-cut-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4408> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-cut.proof
; [GC threshold exceeded with 45,463,624 bytes in use.  Commencing GC.]
; [GC completed with 39,565,192 bytes retained and 5,898,432 bytes freed.]
; [GC will next occur when at least 51,565,192 bytes are in use.]
;; Reading the file took 0.15 seconds
;; Checking the proof took 4.11 seconds
;; VERIFY took 5.93 seconds
4409> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-cut.proof
; [GC threshold exceeded with 53,018,760 bytes in use.  Commencing GC.]
; [GC completed with 41,972,616 bytes retained and 11,046,144 bytes freed.]
; [GC will next occur when at least 53,972,616 bytes are in use.]
; [GC threshold exceeded with 55,752,608 bytes in use.  Commencing GC.]
; [GC completed with 47,343,568 bytes retained and 8,409,040 bytes freed.]
; [GC will next occur when at least 59,343,568 bytes are in use.]
; [GC threshold exceeded with 63,991,952 bytes in use.  Commencing GC.]
; [GC completed with 38,616,168 bytes retained and 25,375,784 bytes freed.]
; [GC will next occur when at least 50,616,168 bytes are in use.]
;; Reading the file took 0.70 seconds
;; Checking the proof took 57.74 seconds
;; VERIFY took 83.79 seconds
4410> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-cut.proof
; [GC threshold exceeded with 53,120,448 bytes in use.  Commencing GC.]
; [GC completed with 44,516,864 bytes retained and 8,603,584 bytes freed.]
; [GC will next occur when at least 56,516,864 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 5.98 seconds
;; VERIFY took 8.74 seconds
4411> DEFINE BUILD.DISJOINED-CUT-OKP
;; Reading from Proofs/level2/admit-build.disjoined-cut-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.03 seconds
4412> VERIFY BUILD.DISJOINED-CUT-OKP
;; Reading from Proofs/level2/thm-build.disjoined-cut-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4413> VERIFY BOOLEANP-OF-BUILD.DISJOINED-CUT-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-cut-okp.proof
; [GC threshold exceeded with 57,444,744 bytes in use.  Commencing GC.]
; [GC completed with 44,090,968 bytes retained and 13,353,776 bytes freed.]
; [GC will next occur when at least 56,090,968 bytes are in use.]
;; Reading the file took 0.31 seconds
; [GC threshold exceeded with 56,753,672 bytes in use.  Commencing GC.]
; [GC completed with 49,357,632 bytes retained and 7,396,040 bytes freed.]
; [GC will next occur when at least 61,357,632 bytes are in use.]
;; Checking the proof took 7.11 seconds
;; VERIFY took 10.79 seconds
4414> VERIFY BUILD.DISJOINED-CUT-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-cut-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.85 seconds
;; VERIFY took 1.07 seconds
4415> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.DISJOINED-CUT-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.disjoined-cut-okp.proof
; [GC threshold exceeded with 62,795,440 bytes in use.  Commencing GC.]
; [GC completed with 56,145,008 bytes retained and 6,650,432 bytes freed.]
; [GC will next occur when at least 68,145,008 bytes are in use.]
;; Reading the file took 0.35 seconds
; [GC threshold exceeded with 68,158,888 bytes in use.  Commencing GC.]
; [GC completed with 61,411,904 bytes retained and 6,746,984 bytes freed.]
; [GC will next occur when at least 73,411,904 bytes are in use.]
;; Checking the proof took 68.45 seconds
;; VERIFY took 99.33 seconds
4416> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.DISJOINED-CUT-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.disjoined-cut-okp.proof
; [GC threshold exceeded with 74,501,344 bytes in use.  Commencing GC.]
; [GC completed with 45,697,376 bytes retained and 28,803,968 bytes freed.]
; [GC will next occur when at least 57,697,376 bytes are in use.]
;; Reading the file took 0.28 seconds
;; Checking the proof took 29.77 seconds
;; VERIFY took 43.30 seconds
4417> VERIFY FORCING-SOUNDNESS-OF-BUILD.DISJOINED-CUT-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.disjoined-cut-okp.proof
; [GC threshold exceeded with 57,708,336 bytes in use.  Commencing GC.]
; [GC completed with 53,630,096 bytes retained and 4,078,240 bytes freed.]
; [GC will next occur when at least 65,630,096 bytes are in use.]
; [GC threshold exceeded with 67,453,520 bytes in use.  Commencing GC.]
; [GC completed with 58,636,248 bytes retained and 8,817,272 bytes freed.]
; [GC will next occur when at least 70,636,248 bytes are in use.]
; [GC threshold exceeded with 75,284,632 bytes in use.  Commencing GC.]
; [GC completed with 66,525,880 bytes retained and 8,758,752 bytes freed.]
; [GC will next occur when at least 78,525,880 bytes are in use.]
;; Reading the file took 0.90 seconds
; [GC threshold exceeded with 78,537,192 bytes in use.  Commencing GC.]
; [GC completed with 32,026,888 bytes retained and 46,510,304 bytes freed.]
; [GC will next occur when at least 44,026,888 bytes are in use.]
;; Checking the proof took 21.05 seconds
;; VERIFY took 31.48 seconds
4418> DEFINE BUILD.DISJOINED-MODUS-PONENS
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4419> VERIFY BUILD.DISJOINED-MODUS-PONENS
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4420> VERIFY BUILD.DISJOINED-MODUS-PONENS-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4421> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-MODUS-PONENS
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-modus-ponens.proof
; [GC threshold exceeded with 45,156,040 bytes in use.  Commencing GC.]
; [GC completed with 37,481,432 bytes retained and 7,674,608 bytes freed.]
; [GC will next occur when at least 49,481,432 bytes are in use.]
;; Reading the file took 0.18 seconds
;; Checking the proof took 32.65 seconds
;; VERIFY took 46.20 seconds
4422> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-MODUS-PONENS
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-modus-ponens.proof
; [GC threshold exceeded with 49,490,168 bytes in use.  Commencing GC.]
; [GC completed with 36,418,360 bytes retained and 13,071,808 bytes freed.]
; [GC will next occur when at least 48,418,360 bytes are in use.]
; [GC threshold exceeded with 49,857,376 bytes in use.  Commencing GC.]
; [GC completed with 41,559,648 bytes retained and 8,297,728 bytes freed.]
; [GC will next occur when at least 53,559,648 bytes are in use.]
; [GC threshold exceeded with 60,544,280 bytes in use.  Commencing GC.]
; [GC completed with 47,891,768 bytes retained and 12,652,512 bytes freed.]
; [GC will next occur when at least 59,891,768 bytes are in use.]
;; Reading the file took 1.00 seconds
; [GC threshold exceeded with 59,903,024 bytes in use.  Commencing GC.]
; [GC completed with 59,729,032 bytes retained and 173,992 bytes freed.]
; [GC will next occur when at least 71,729,032 bytes are in use.]
;; Checking the proof took 75.21 seconds
;; VERIFY took 108.42 seconds
4423> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-MODUS-PONENS
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-modus-ponens.proof
; [GC threshold exceeded with 72,762,136 bytes in use.  Commencing GC.]
; [GC completed with 64,622,032 bytes retained and 8,140,104 bytes freed.]
; [GC will next occur when at least 76,622,032 bytes are in use.]
;; Reading the file took 0.26 seconds
;; Checking the proof took 66.56 seconds
;; VERIFY took 95.31 seconds
4424> DEFINE BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-okp.proofs
; [GC threshold exceeded with 76,665,808 bytes in use.  Commencing GC.]
; [GC completed with 68,300,768 bytes retained and 8,365,040 bytes freed.]
; [GC will next occur when at least 80,300,768 bytes are in use.]
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.03 seconds
4425> VERIFY BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4426> VERIFY BOOLEANP-OF-BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-modus-ponens-okp.proof
; [GC threshold exceeded with 82,330,032 bytes in use.  Commencing GC.]
; [GC completed with 38,711,304 bytes retained and 43,618,728 bytes freed.]
; [GC will next occur when at least 50,711,304 bytes are in use.]
;; Reading the file took 0.22 seconds
;; Checking the proof took 3.68 seconds
;; VERIFY took 5.50 seconds
4427> VERIFY BUILD.DISJOINED-MODUS-PONENS-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.61 seconds
;; VERIFY took 0.77 seconds
4428> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.disjoined-modus-ponens-okp.proof
; [GC threshold exceeded with 51,221,112 bytes in use.  Commencing GC.]
; [GC completed with 45,376,368 bytes retained and 5,844,744 bytes freed.]
; [GC will next occur when at least 57,376,368 bytes are in use.]
;; Reading the file took 0.29 seconds
;; Checking the proof took 41.11 seconds
;; VERIFY took 59.52 seconds
4429> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.disjoined-modus-ponens-okp.proof
; [GC threshold exceeded with 57,385,152 bytes in use.  Commencing GC.]
; [GC completed with 41,989,800 bytes retained and 15,395,352 bytes freed.]
; [GC will next occur when at least 53,989,800 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 18.31 seconds
;; VERIFY took 26.30 seconds
4430> VERIFY FORCING-SOUNDNESS-OF-BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.disjoined-modus-ponens-okp.proof
; [GC threshold exceeded with 54,001,496 bytes in use.  Commencing GC.]
; [GC completed with 45,325,192 bytes retained and 8,676,304 bytes freed.]
; [GC will next occur when at least 57,325,192 bytes are in use.]
; [GC threshold exceeded with 58,541,496 bytes in use.  Commencing GC.]
; [GC completed with 40,231,984 bytes retained and 18,309,512 bytes freed.]
; [GC will next occur when at least 52,231,984 bytes are in use.]
; [GC threshold exceeded with 59,216,624 bytes in use.  Commencing GC.]
; [GC completed with 48,121,640 bytes retained and 11,094,984 bytes freed.]
; [GC will next occur when at least 60,121,640 bytes are in use.]
;; Reading the file took 0.81 seconds
; [GC threshold exceeded with 60,132,952 bytes in use.  Commencing GC.]
; [GC completed with 52,077,488 bytes retained and 8,055,464 bytes freed.]
; [GC will next occur when at least 64,077,488 bytes are in use.]
;; Checking the proof took 15.93 seconds
;; VERIFY took 23.84 seconds
4431> DEFINE BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-2.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4432> VERIFY BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4433> VERIFY BUILD.DISJOINED-MODUS-PONENS-2-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4434> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-modus-ponens-2.proof
; [GC threshold exceeded with 64,699,904 bytes in use.  Commencing GC.]
; [GC completed with 57,394,408 bytes retained and 7,305,496 bytes freed.]
; [GC will next occur when at least 69,394,408 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 29.42 seconds
;; VERIFY took 41.60 seconds
4435> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-modus-ponens-2.proof
; [GC threshold exceeded with 69,406,304 bytes in use.  Commencing GC.]
; [GC completed with 56,357,512 bytes retained and 13,048,792 bytes freed.]
; [GC will next occur when at least 68,357,512 bytes are in use.]
; [GC threshold exceeded with 69,601,120 bytes in use.  Commencing GC.]
; [GC completed with 61,449,472 bytes retained and 8,151,648 bytes freed.]
; [GC will next occur when at least 73,449,472 bytes are in use.]
; [GC threshold exceeded with 80,434,104 bytes in use.  Commencing GC.]
; [GC completed with 67,750,600 bytes retained and 12,683,504 bytes freed.]
; [GC will next occur when at least 79,750,600 bytes are in use.]
;; Reading the file took 1.04 seconds
; [GC threshold exceeded with 79,761,792 bytes in use.  Commencing GC.]
; [GC completed with 79,587,784 bytes retained and 174,008 bytes freed.]
; [GC will next occur when at least 91,587,784 bytes are in use.]
;; Checking the proof took 71.52 seconds
;; VERIFY took 102.84 seconds
4436> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-modus-ponens-2.proof
; [GC threshold exceeded with 92,426,056 bytes in use.  Commencing GC.]
; [GC completed with 84,617,320 bytes retained and 7,808,736 bytes freed.]
; [GC will next occur when at least 96,617,320 bytes are in use.]
;; Reading the file took 0.26 seconds
;; Checking the proof took 59.92 seconds
;; VERIFY took 85.75 seconds
4437> DEFINE BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-2-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; [GC threshold exceeded with 96,625,608 bytes in use.  Commencing GC.]
; [GC completed with 88,612,936 bytes retained and 8,012,672 bytes freed.]
; [GC will next occur when at least 100,612,936 bytes are in use.]
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.04 seconds
4438> VERIFY BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4439> VERIFY BOOLEANP-OF-BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-modus-ponens-2-okp.proof
; [GC threshold exceeded with 102,228,600 bytes in use.  Commencing GC.]
; [GC completed with 19,593,376 bytes retained and 82,635,224 bytes freed.]
; [GC will next occur when at least 31,593,376 bytes are in use.]
;; Reading the file took 0.29 seconds
;; Checking the proof took 3.61 seconds
;; VERIFY took 5.47 seconds
4440> VERIFY BUILD.DISJOINED-MODUS-PONENS-2-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.60 seconds
;; VERIFY took 0.75 seconds
4441> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.disjoined-modus-ponens-2-okp.proof
; [GC threshold exceeded with 32,103,080 bytes in use.  Commencing GC.]
; [GC completed with 26,189,992 bytes retained and 5,913,088 bytes freed.]
; [GC will next occur when at least 38,189,992 bytes are in use.]
;; Reading the file took 0.28 seconds
;; Checking the proof took 41.08 seconds
;; VERIFY took 59.30 seconds
4442> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.disjoined-modus-ponens-2-okp.proof
; [GC threshold exceeded with 38,203,224 bytes in use.  Commencing GC.]
; [GC completed with 22,901,336 bytes retained and 15,301,888 bytes freed.]
; [GC will next occur when at least 34,901,336 bytes are in use.]
;; Reading the file took 0.18 seconds
;; Checking the proof took 20.50 seconds
;; VERIFY took 29.55 seconds
4443> VERIFY FORCING-SOUNDNESS-OF-BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.disjoined-modus-ponens-2-okp.proof
; [GC threshold exceeded with 34,916,904 bytes in use.  Commencing GC.]
; [GC completed with 26,197,568 bytes retained and 8,719,336 bytes freed.]
; [GC will next occur when at least 38,197,568 bytes are in use.]
; [GC threshold exceeded with 39,477,856 bytes in use.  Commencing GC.]
; [GC completed with 31,040,512 bytes retained and 8,437,344 bytes freed.]
; [GC will next occur when at least 43,040,512 bytes are in use.]
; [GC threshold exceeded with 50,025,144 bytes in use.  Commencing GC.]
; [GC completed with 38,930,160 bytes retained and 11,094,984 bytes freed.]
; [GC will next occur when at least 50,930,160 bytes are in use.]
;; Reading the file took 0.78 seconds
; [GC threshold exceeded with 50,941,472 bytes in use.  Commencing GC.]
; [GC completed with 42,886,016 bytes retained and 8,055,456 bytes freed.]
; [GC will next occur when at least 54,886,016 bytes are in use.]
;; Checking the proof took 15.91 seconds
;; VERIFY took 23.72 seconds
4444> DEFINE BUILD.LHS-COMMUTE-OR-THEN-RASSOC
;; Reading from Proofs/level2/admit-build.lhs-commute-or-then-rassoc.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
4445> VERIFY BUILD.LHS-COMMUTE-OR-THEN-RASSOC
;; Reading from Proofs/level2/thm-build.lhs-commute-or-then-rassoc.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4446> VERIFY BUILD.LHS-COMMUTE-OR-THEN-RASSOC-UNDER-IFF
;; Reading from Proofs/level2/thm-build.lhs-commute-or-then-rassoc-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4447> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.LHS-COMMUTE-OR-THEN-RASSOC
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.lhs-commute-or-then-rassoc.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 1.33 seconds
;; VERIFY took 1.81 seconds
4448> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.LHS-COMMUTE-OR-THEN-RASSOC
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.lhs-commute-or-then-rassoc.proof
; [GC threshold exceeded with 55,452,048 bytes in use.  Commencing GC.]
; [GC completed with 47,501,400 bytes retained and 7,950,648 bytes freed.]
; [GC will next occur when at least 59,501,400 bytes are in use.]
;; Reading the file took 0.15 seconds
;; Checking the proof took 11.72 seconds
;; VERIFY took 15.66 seconds
4449> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.LHS-COMMUTE-OR-THEN-RASSOC
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.lhs-commute-or-then-rassoc.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 1.84 seconds
;; VERIFY took 2.53 seconds
4450> DEFINE BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP
;; Reading from Proofs/level2/admit-build.lhs-commute-or-then-rassoc-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
4451> VERIFY BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP
;; Reading from Proofs/level2/thm-build.lhs-commute-or-then-rassoc-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4452> VERIFY BOOLEANP-OF-BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.lhs-commute-or-then-rassoc-okp.proof
; [GC threshold exceeded with 59,514,784 bytes in use.  Commencing GC.]
; [GC completed with 20,670,336 bytes retained and 38,844,448 bytes freed.]
; [GC will next occur when at least 32,670,336 bytes are in use.]
;; Reading the file took 0.14 seconds
;; Checking the proof took 1.91 seconds
;; VERIFY took 2.85 seconds
4453> VERIFY BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.lhs-commute-or-then-rassoc-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.40 seconds
;; VERIFY took 0.50 seconds
4454> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.lhs-commute-or-then-rassoc-okp.proof
; [GC threshold exceeded with 33,398,488 bytes in use.  Commencing GC.]
; [GC completed with 25,126,008 bytes retained and 8,272,480 bytes freed.]
; [GC will next occur when at least 37,126,008 bytes are in use.]
;; Reading the file took 0.17 seconds
;; Checking the proof took 15.39 seconds
;; VERIFY took 22.36 seconds
4455> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.lhs-commute-or-then-rassoc-okp.proof
; [GC threshold exceeded with 38,196,624 bytes in use.  Commencing GC.]
; [GC completed with 25,631,120 bytes retained and 12,565,504 bytes freed.]
; [GC will next occur when at least 37,631,120 bytes are in use.]
;; Reading the file took 0.15 seconds
;; Checking the proof took 8.90 seconds
;; VERIFY took 12.91 seconds
4456> VERIFY FORCING-SOUNDNESS-OF-BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.lhs-commute-or-then-rassoc-okp.proof
; [GC threshold exceeded with 37,758,928 bytes in use.  Commencing GC.]
; [GC completed with 32,353,016 bytes retained and 5,405,912 bytes freed.]
; [GC will next occur when at least 44,353,016 bytes are in use.]
;; Reading the file took 0.30 seconds
;; Checking the proof took 4.19 seconds
;; VERIFY took 6.32 seconds
4457> DEFINE RW.CREWRITE-TWIDDLE-BLDR
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle-bldr.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
4458> VERIFY RW.CREWRITE-TWIDDLE-BLDR
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4459> VERIFY RW.CREWRITE-TWIDDLE-BLDR-UNDER-IFF
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4460> VERIFY FORCING-LOGIC.APPEALP-OF-RW.CREWRITE-TWIDDLE-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-rw.crewrite-twiddle-bldr.proof
; [GC threshold exceeded with 44,383,248 bytes in use.  Commencing GC.]
; [GC completed with 20,459,528 bytes retained and 23,923,720 bytes freed.]
; [GC will next occur when at least 32,459,528 bytes are in use.]
;; Reading the file took 0.06 seconds
;; Checking the proof took 1.36 seconds
;; VERIFY took 1.86 seconds
4461> VERIFY FORCING-LOGIC.CONCLUSION-OF-RW.CREWRITE-TWIDDLE-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-rw.crewrite-twiddle-bldr.proof
; [GC threshold exceeded with 33,407,664 bytes in use.  Commencing GC.]
; [GC completed with 26,418,840 bytes retained and 6,988,824 bytes freed.]
; [GC will next occur when at least 38,418,840 bytes are in use.]
;; Reading the file took 0.16 seconds
;; Checking the proof took 11.85 seconds
;; VERIFY took 15.82 seconds
4462> VERIFY FORCING-LOGIC.PROOFP-OF-RW.CREWRITE-TWIDDLE-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-rw.crewrite-twiddle-bldr.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 1.85 seconds
;; VERIFY took 2.54 seconds
4463> DEFINE RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle-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
4464> VERIFY RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4465> VERIFY BOOLEANP-OF-RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-rw.crewrite-twiddle-bldr-okp.proof
; [GC threshold exceeded with 39,331,296 bytes in use.  Commencing GC.]
; [GC completed with 23,930,912 bytes retained and 15,400,384 bytes freed.]
; [GC will next occur when at least 35,930,912 bytes are in use.]
;; Reading the file took 0.14 seconds
;; Checking the proof took 1.92 seconds
;; VERIFY took 2.86 seconds
4466> VERIFY RW.CREWRITE-TWIDDLE-BLDR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.41 seconds
;; VERIFY took 0.52 seconds
4467> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-rw.crewrite-twiddle-bldr-okp.proof
; [GC threshold exceeded with 36,798,536 bytes in use.  Commencing GC.]
; [GC completed with 29,961,032 bytes retained and 6,837,504 bytes freed.]
; [GC will next occur when at least 41,961,032 bytes are in use.]
;; Reading the file took 0.18 seconds
;; Checking the proof took 15.36 seconds
;; VERIFY took 22.35 seconds
4468> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-rw.crewrite-twiddle-bldr-okp.proof
;; Reading the file took 0.14 seconds
; [GC threshold exceeded with 42,005,104 bytes in use.  Commencing GC.]
; [GC completed with 29,360,200 bytes retained and 12,644,904 bytes freed.]
; [GC will next occur when at least 41,360,200 bytes are in use.]
;; Checking the proof took 8.85 seconds
;; VERIFY took 12.87 seconds
4469> VERIFY FORCING-SOUNDNESS-OF-RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-rw.crewrite-twiddle-bldr-okp.proof
; [GC threshold exceeded with 43,667,944 bytes in use.  Commencing GC.]
; [GC completed with 36,650,160 bytes retained and 7,017,784 bytes freed.]
; [GC will next occur when at least 48,650,160 bytes are in use.]
;; Reading the file took 0.31 seconds
;; Checking the proof took 4.17 seconds
;; VERIFY took 6.30 seconds
4470> DEFINE RW.CREWRITE-TWIDDLE2-LEMMA
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-lemma.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
4471> VERIFY RW.CREWRITE-TWIDDLE2-LEMMA
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-lemma.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4472> VERIFY RW.CREWRITE-TWIDDLE2-LEMMA-UNDER-IFF
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-lemma-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4473> VERIFY FORCING-LOGIC.APPEALP-OF-RW.CREWRITE-TWIDDLE2-LEMMA
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-rw.crewrite-twiddle2-lemma.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 10.76 seconds
;; VERIFY took 14.55 seconds
4474> VERIFY FORCING-LOGIC.CONCLUSION-OF-RW.CREWRITE-TWIDDLE2-LEMMA
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-rw.crewrite-twiddle2-lemma.proof
; [GC threshold exceeded with 50,572,264 bytes in use.  Commencing GC.]
; [GC completed with 24,051,912 bytes retained and 26,520,352 bytes freed.]
; [GC will next occur when at least 36,051,912 bytes are in use.]
; [GC threshold exceeded with 38,153,296 bytes in use.  Commencing GC.]
; [GC completed with 29,176,336 bytes retained and 8,976,960 bytes freed.]
; [GC will next occur when at least 41,176,336 bytes are in use.]
;; Reading the file took 0.40 seconds
; [GC threshold exceeded with 41,182,920 bytes in use.  Commencing GC.]
; [GC completed with 30,726,360 bytes retained and 10,456,560 bytes freed.]
; [GC will next occur when at least 42,726,360 bytes are in use.]
;; Checking the proof took 87.26 seconds
;; VERIFY took 118.43 seconds
4475> VERIFY FORCING-LOGIC.PROOFP-OF-RW.CREWRITE-TWIDDLE2-LEMMA
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-rw.crewrite-twiddle2-lemma.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 17.20 seconds
;; VERIFY took 23.39 seconds
4476> DEFINE RW.CREWRITE-TWIDDLE2-BLDR
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-bldr.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4477> VERIFY RW.CREWRITE-TWIDDLE2-BLDR
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4478> VERIFY RW.CREWRITE-TWIDDLE2-BLDR-UNDER-IFF
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-bldr-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4479> VERIFY FORCING-LOGIC.APPEALP-OF-RW.CREWRITE-TWIDDLE2-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-rw.crewrite-twiddle2-bldr.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 6.60 seconds
;; VERIFY took 8.91 seconds
4480> VERIFY FORCING-LOGIC.CONCLUSION-OF-RW.CREWRITE-TWIDDLE2-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-rw.crewrite-twiddle2-bldr.proof
; [GC threshold exceeded with 42,734,296 bytes in use.  Commencing GC.]
; [GC completed with 30,966,384 bytes retained and 11,767,912 bytes freed.]
; [GC will next occur when at least 42,966,384 bytes are in use.]
; [GC threshold exceeded with 44,197,856 bytes in use.  Commencing GC.]
; [GC completed with 27,557,928 bytes retained and 16,639,928 bytes freed.]
; [GC will next occur when at least 39,557,928 bytes are in use.]
;; Reading the file took 0.44 seconds
; [GC threshold exceeded with 39,567,728 bytes in use.  Commencing GC.]
; [GC completed with 32,820,496 bytes retained and 6,747,232 bytes freed.]
; [GC will next occur when at least 44,820,496 bytes are in use.]
;; Checking the proof took 95.16 seconds
;; VERIFY took 128.83 seconds
4481> VERIFY FORCING-LOGIC.PROOFP-OF-RW.CREWRITE-TWIDDLE2-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-rw.crewrite-twiddle2-bldr.proof
;; Reading the file took 0.07 seconds
; [GC threshold exceeded with 44,829,888 bytes in use.  Commencing GC.]
; [GC completed with 34,611,512 bytes retained and 10,218,376 bytes freed.]
; [GC will next occur when at least 46,611,512 bytes are in use.]
;; Checking the proof took 9.07 seconds
;; VERIFY took 12.37 seconds
4482> DEFINE RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-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.02 seconds
4483> VERIFY RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-bldr-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4484> VERIFY BOOLEANP-OF-RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-rw.crewrite-twiddle2-bldr-okp.proof
; [GC threshold exceeded with 47,407,680 bytes in use.  Commencing GC.]
; [GC completed with 40,126,000 bytes retained and 7,281,680 bytes freed.]
; [GC will next occur when at least 52,126,000 bytes are in use.]
;; Reading the file took 0.24 seconds
;; Checking the proof took 4.36 seconds
;; VERIFY took 6.56 seconds
4485> VERIFY RW.CREWRITE-TWIDDLE2-BLDR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-bldr-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.64 seconds
;; VERIFY took 0.80 seconds
4486> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-rw.crewrite-twiddle2-bldr-okp.proof
; [GC threshold exceeded with 52,135,872 bytes in use.  Commencing GC.]
; [GC completed with 38,102,368 bytes retained and 14,033,504 bytes freed.]
; [GC will next occur when at least 50,102,368 bytes are in use.]
;; Reading the file took 0.22 seconds
;; Checking the proof took 31.44 seconds
;; VERIFY took 45.69 seconds
4487> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-rw.crewrite-twiddle2-bldr-okp.proof
; [GC threshold exceeded with 50,849,496 bytes in use.  Commencing GC.]
; [GC completed with 41,600,856 bytes retained and 9,248,640 bytes freed.]
; [GC will next occur when at least 53,600,856 bytes are in use.]
;; Reading the file took 0.18 seconds
;; Checking the proof took 17.36 seconds
;; VERIFY took 25.23 seconds
4488> VERIFY FORCING-SOUNDNESS-OF-RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-rw.crewrite-twiddle2-bldr-okp.proof
; [GC threshold exceeded with 53,886,848 bytes in use.  Commencing GC.]
; [GC completed with 36,099,240 bytes retained and 17,787,608 bytes freed.]
; [GC will next occur when at least 48,099,240 bytes are in use.]
; [GC threshold exceeded with 50,533,992 bytes in use.  Commencing GC.]
; [GC completed with 42,217,888 bytes retained and 8,316,104 bytes freed.]
; [GC will next occur when at least 54,217,888 bytes are in use.]
;; Reading the file took 0.43 seconds
;; Checking the proof took 6.94 seconds
;; VERIFY took 10.35 seconds
4489> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle-lemma-1.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4490> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-lemma-1.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4491> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-lemma-1-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 seconds
4492> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle-lemma-1.proof
;; Reading the file took 0.07 seconds
; [GC threshold exceeded with 54,230,616 bytes in use.  Commencing GC.]
; [GC completed with 39,577,824 bytes retained and 14,652,792 bytes freed.]
; [GC will next occur when at least 51,577,824 bytes are in use.]
;; Checking the proof took 27.20 seconds
;; VERIFY took 37.41 seconds
4493> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-clause.aux-split-twiddle-lemma-1.proof
; [GC threshold exceeded with 51,774,408 bytes in use.  Commencing GC.]
; [GC completed with 45,162,976 bytes retained and 6,611,432 bytes freed.]
; [GC will next occur when at least 57,162,976 bytes are in use.]
; [GC threshold exceeded with 59,551,048 bytes in use.  Commencing GC.]
; [GC completed with 42,920,840 bytes retained and 16,630,208 bytes freed.]
; [GC will next occur when at least 54,920,840 bytes are in use.]
;; Reading the file took 0.57 seconds
;; Checking the proof took 58.37 seconds
;; VERIFY took 82.60 seconds
4494> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-clause.aux-split-twiddle-lemma-1.proof
; [GC threshold exceeded with 56,611,056 bytes in use.  Commencing GC.]
; [GC completed with 48,325,360 bytes retained and 8,285,696 bytes freed.]
; [GC will next occur when at least 60,325,360 bytes are in use.]
;; Reading the file took 0.23 seconds
; [GC threshold exceeded with 60,338,504 bytes in use.  Commencing GC.]
; [GC completed with 49,902,064 bytes retained and 10,436,440 bytes freed.]
; [GC will next occur when at least 61,902,064 bytes are in use.]
;; Checking the proof took 143.36 seconds
;; VERIFY took 199.95 seconds
4495> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle.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
4496> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4497> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 seconds
4498> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle.proof
; [GC threshold exceeded with 63,370,704 bytes in use.  Commencing GC.]
; [GC completed with 55,201,272 bytes retained and 8,169,432 bytes freed.]
; [GC will next occur when at least 67,201,272 bytes are in use.]
;; Reading the file took 0.16 seconds
;; Checking the proof took 9.35 seconds
;; VERIFY took 12.87 seconds
4499> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-TWIDDLE
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-clause.aux-split-twiddle.proof
; [GC threshold exceeded with 67,466,488 bytes in use.  Commencing GC.]
; [GC completed with 55,090,984 bytes retained and 12,375,504 bytes freed.]
; [GC will next occur when at least 67,090,984 bytes are in use.]
;; Reading the file took 0.25 seconds
;; Checking the proof took 14.12 seconds
;; VERIFY took 19.82 seconds
4500> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-TWIDDLE
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-clause.aux-split-twiddle.proof
; [GC threshold exceeded with 67,877,448 bytes in use.  Commencing GC.]
; [GC completed with 61,748,128 bytes retained and 6,129,320 bytes freed.]
; [GC will next occur when at least 73,748,128 bytes are in use.]
;; Reading the file took 0.25 seconds
; [GC threshold exceeded with 73,760,008 bytes in use.  Commencing GC.]
; [GC completed with 50,125,176 bytes retained and 23,634,832 bytes freed.]
; [GC will next occur when at least 62,125,176 bytes are in use.]
;; Checking the proof took 76.48 seconds
;; VERIFY took 106.74 seconds
4501> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE-OKP
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle-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.02 seconds
4502> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-OKP
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4503> VERIFY BOOLEANP-OF-CLAUSE.AUX-SPLIT-TWIDDLE-OKP
;; Reading from Proofs/level2/thm-booleanp-of-clause.aux-split-twiddle-okp.proof
; [GC threshold exceeded with 62,139,752 bytes in use.  Commencing GC.]
; [GC completed with 53,525,376 bytes retained and 8,614,376 bytes freed.]
; [GC will next occur when at least 65,525,376 bytes are in use.]
;; Reading the file took 0.18 seconds
;; Checking the proof took 3.50 seconds
;; VERIFY took 5.20 seconds
4504> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.58 seconds
;; VERIFY took 0.73 seconds
4505> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-CLAUSE.AUX-SPLIT-TWIDDLE-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-clause.aux-split-twiddle-okp.proof
; [GC threshold exceeded with 65,734,624 bytes in use.  Commencing GC.]
; [GC completed with 53,677,272 bytes retained and 12,057,352 bytes freed.]
; [GC will next occur when at least 65,677,272 bytes are in use.]
;; Reading the file took 0.20 seconds
;; Checking the proof took 31.56 seconds
;; VERIFY took 45.58 seconds
4506> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-CLAUSE.AUX-SPLIT-TWIDDLE-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-clause.aux-split-twiddle-okp.proof
; [GC threshold exceeded with 66,953,632 bytes in use.  Commencing GC.]
; [GC completed with 57,330,328 bytes retained and 9,623,304 bytes freed.]
; [GC will next occur when at least 69,330,328 bytes are in use.]
;; Reading the file took 0.18 seconds
;; Checking the proof took 21.72 seconds
;; VERIFY took 31.32 seconds
4507> VERIFY FORCING-SOUNDNESS-OF-CLAUSE.AUX-SPLIT-TWIDDLE-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-clause.aux-split-twiddle-okp.proof
; [GC threshold exceeded with 69,725,120 bytes in use.  Commencing GC.]
; [GC completed with 22,799,576 bytes retained and 46,925,544 bytes freed.]
; [GC will next occur when at least 34,799,576 bytes are in use.]
; [GC threshold exceeded with 38,511,304 bytes in use.  Commencing GC.]
; [GC completed with 28,443,832 bytes retained and 10,067,472 bytes freed.]
; [GC will next occur when at least 40,443,832 bytes are in use.]
;; Reading the file took 
; [GC threshold exceeded with 41,589,024 bytes in use.  Commencing GC.]
; [GC completed with 32,687,008 bytes retained and 8,902,016 bytes freed.]
; [GC will next occur when at least 44,687,008 bytes are in use.]
0.52 seconds
;; Checking the proof took 10.42 seconds
;; VERIFY took 15.49 seconds
4508> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1A
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-lemma-1a.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X P B): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4509> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1A
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-1a.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4510> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1A-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-1a-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4511> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1A
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle2-lemma-1a.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 2.65 seconds
;; VERIFY took 3.67 seconds
4512> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1A
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-clause.aux-split-twiddle2-lemma-1a.proof
; [GC threshold exceeded with 44,696,128 bytes in use.  Commencing GC.]
; [GC completed with 36,711,736 bytes retained and 7,984,392 bytes freed.]
; [GC will next occur when at least 48,711,736 bytes are in use.]
; [GC threshold exceeded with 54,668,904 bytes in use.  Commencing GC.]
; [GC completed with 43,258,904 bytes retained and 11,410,000 bytes freed.]
; [GC will next occur when at least 55,258,904 bytes are in use.]
;; Reading the file took 0.45 seconds
;; Checking the proof took 23.95 seconds
;; VERIFY took 33.24 seconds
4513> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1A
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-clause.aux-split-twiddle2-lemma-1a.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 4.41 seconds
;; VERIFY took 6.28 seconds
4514> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-lemma-1.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X P B): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4515> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-1.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4516> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-1-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4517> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle2-lemma-1.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 8.24 seconds
;; VERIFY took 11.11 seconds
4518> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-clause.aux-split-twiddle2-lemma-1.proof
; [GC threshold exceeded with 55,263,672 bytes in use.  Commencing GC.]
; [GC completed with 43,304,960 bytes retained and 11,958,712 bytes freed.]
; [GC will next occur when at least 55,304,960 bytes are in use.]
; [GC threshold exceeded with 56,557,280 bytes in use.  Commencing GC.]
; [GC completed with 31,384,232 bytes retained and 25,173,048 bytes freed.]
; [GC will next occur when at least 43,384,232 bytes are in use.]
;; Reading the file took 0.48 seconds
; [GC threshold exceeded with 43,394,184 bytes in use.  Commencing GC.]
; [GC completed with 36,650,904 bytes retained and 6,743,280 bytes freed.]
; [GC will next occur when at least 48,650,904 bytes are in use.]
;; Checking the proof took 80.31 seconds
;; VERIFY took 111.59 seconds
4519> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-clause.aux-split-twiddle2-lemma-1.proof
; [GC threshold exceeded with 49,093,664 bytes in use.  Commencing GC.]
; [GC completed with 41,263,352 bytes retained and 7,830,312 bytes freed.]
; [GC will next occur when at least 53,263,352 bytes are in use.]
;; Reading the file took 0.27 seconds
; [GC threshold exceeded with 53,277,672 bytes in use.  Commencing GC.]
; [GC completed with 44,777,976 bytes retained and 8,499,696 bytes freed.]
; [GC will next occur when at least 56,777,976 bytes are in use.]
;; Checking the proof took 96.01 seconds
;; VERIFY took 135.07 seconds
4520> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-lemma-2a.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X A Q): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4521> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2a.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4522> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2a-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
4523> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle2-lemma-2a.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 10.43 seconds
;; VERIFY took 14.53 seconds
4524> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-clause.aux-split-twiddle2-lemma-2a.proof
; [GC threshold exceeded with 58,932,992 bytes in use.  Commencing GC.]
; [GC completed with 27,921,632 bytes retained and 31,011,360 bytes freed.]
; [GC will next occur when at least 39,921,632 bytes are in use.]
; [GC threshold exceeded with 41,493,504 bytes in use.  Commencing GC.]
; [GC completed with 32,996,528 bytes retained and 8,496,976 bytes freed.]
; [GC will next occur when at least 44,996,528 bytes are in use.]
;; Reading the file took 0.41 seconds
;; Checking the proof took 31.62 seconds
;; VERIFY took 44.01 seconds
4525> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-clause.aux-split-twiddle2-lemma-2a.proof
; [GC threshold exceeded with 45,781,040 bytes in use.  Commencing GC.]
; [GC completed with 31,183,416 bytes retained and 14,597,624 bytes freed.]
; [GC will next occur when at least 43,183,416 bytes are in use.]
;; Reading the file took 0.13 seconds
;; Checking the proof took 18.17 seconds
;; VERIFY took 25.78 seconds
4526> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-lemma-2.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X A Q): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4527> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4528> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4529> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle2-lemma-2.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 8.34 seconds
;; VERIFY took 11.24 seconds
4530> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-clause.aux-split-twiddle2-lemma-2.proof
; [GC threshold exceeded with 43,192,952 bytes in use.  Commencing GC.]
; [GC completed with 34,808,256 bytes retained and 8,384,696 bytes freed.]
; [GC will next occur when at least 46,808,256 bytes are in use.]
;; Reading the file took 0.31 seconds
; [GC threshold exceeded with 46,823,768 bytes in use.  Commencing GC.]
; [GC completed with 38,680,256 bytes retained and 8,143,512 bytes freed.]
; [GC will next occur when at least 50,680,256 bytes are in use.]
;; Checking the proof took 96.98 seconds
;; VERIFY took 131.27 seconds
4531> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-clause.aux-split-twiddle2-lemma-2.proof
; [GC threshold exceeded with 51,135,856 bytes in use.  Commencing GC.]
; [GC completed with 40,691,168 bytes retained and 10,444,688 bytes freed.]
; [GC will next occur when at least 52,691,168 bytes are in use.]
;; Reading the file took 0.10 seconds
;; Checking the proof took 12.65 seconds
;; VERIFY took 17.40 seconds
4532> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2.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
4533> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4534> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4535> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle2.proof
; [GC threshold exceeded with 54,918,712 bytes in use.  Commencing GC.]
; [GC completed with 35,245,016 bytes retained and 19,673,696 bytes freed.]
; [GC will next occur when at least 47,245,016 bytes are in use.]
;; Reading the file took 0.20 seconds
;; Checking the proof took 16.49 seconds
;; VERIFY took 22.05 seconds
4536> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-clause.aux-split-twiddle2.proof
; [GC threshold exceeded with 48,659,152 bytes in use.  Commencing GC.]
; [GC completed with 41,088,112 bytes retained and 7,571,040 bytes freed.]
; [GC will next occur when at least 53,088,112 bytes are in use.]
;; Reading the file took 0.35 seconds
; [GC threshold exceeded with 53,101,992 bytes in use.  Commencing GC.]
; [GC completed with 44,572,408 bytes retained and 8,529,584 bytes freed.]
; [GC will next occur when at least 56,572,408 bytes are in use.]
;; Checking the proof took 21.86 seconds
;; VERIFY took 29.68 seconds
4537> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-clause.aux-split-twiddle2.proof
; [GC threshold exceeded with 56,925,960 bytes in use.  Commencing GC.]
; [GC completed with 50,480,056 bytes retained and 6,445,904 bytes freed.]
; [GC will next occur when at least 62,480,056 bytes are in use.]
;; Reading the file took 0.40 seconds
; [GC threshold exceeded with 63,142,760 bytes in use.  Commencing GC.]
; [GC completed with 38,848,480 bytes retained and 24,294,280 bytes freed.]
; [GC will next occur when at least 50,848,480 bytes are in use.]
;; Checking the proof took 85.91 seconds
;; VERIFY took 118.12 seconds
4538> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-OKP
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-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.02 seconds
4539> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-OKP
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4540> VERIFY BOOLEANP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-OKP
;; Reading from Proofs/level2/thm-booleanp-of-clause.aux-split-twiddle2-okp.proof
; [GC threshold exceeded with 52,288,376 bytes in use.  Commencing GC.]
; [GC completed with 42,464,280 bytes retained and 9,824,096 bytes freed.]
; [GC will next occur when at least 54,464,280 bytes are in use.]
;; Reading the file took 0.24 seconds
;; Checking the proof took 4.51 seconds
;; VERIFY took 6.72 seconds
4541> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-okp-of-logic.appeal-identity.proof
; [GC threshold exceeded with 54,480,408 bytes in use.  Commencing GC.]
; [GC completed with 40,480,432 bytes retained and 13,999,976 bytes freed.]
; [GC will next occur when at least 52,480,432 bytes are in use.]
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.66 seconds
;; VERIFY took 0.84 seconds
4542> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-clause.aux-split-twiddle2-okp.proof
; [GC threshold exceeded with 53,738,744 bytes in use.  Commencing GC.]
; [GC completed with 47,507,176 bytes retained and 6,231,568 bytes freed.]
; [GC will next occur when at least 59,507,176 bytes are in use.]
;; Reading the file took 0.22 seconds
;; Checking the proof took 32.30 seconds
;; VERIFY took 46.53 seconds
4543> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-clause.aux-split-twiddle2-okp.proof
; [GC threshold exceeded with 60,271,464 bytes in use.  Commencing GC.]
; [GC completed with 46,642,936 bytes retained and 13,628,528 bytes freed.]
; [GC will next occur when at least 58,642,936 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 17.85 seconds
;; VERIFY took 25.65 seconds
4544> VERIFY FORCING-SOUNDNESS-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-clause.aux-split-twiddle2-okp.proof
; [GC threshold exceeded with 59,912,712 bytes in use.  Commencing GC.]
; [GC completed with 53,164,536 bytes retained and 6,748,176 bytes freed.]
; [GC will next occur when at least 65,164,536 bytes are in use.]
;; Reading the file took 0.40 seconds
; [GC threshold exceeded with 65,178,784 bytes in use.  Commencing GC.]
; [GC completed with 56,328,856 bytes retained and 8,849,928 bytes freed.]
; [GC will next occur when at least 68,328,856 bytes are in use.]
;; Checking the proof took 7.16 seconds
;; VERIFY took 10.55 seconds
4545> DEFINE CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR
;; Reading from Proofs/level2/admit-clause.aux-split-default-3-bldr.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
4546> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4547> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4548> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-default-3-bldr.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 2.04 seconds
;; VERIFY took 2.71 seconds
4549> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-clause.aux-split-default-3-bldr.proof
; [GC threshold exceeded with 68,737,688 bytes in use.  Commencing GC.]
; [GC completed with 61,347,304 bytes retained and 7,390,384 bytes freed.]
; [GC will next occur when at least 73,347,304 bytes are in use.]
;; Reading the file took 0.27 seconds
;; Checking the proof took 18.07 seconds
;; VERIFY took 24.47 seconds
4550> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-clause.aux-split-default-3-bldr.proof
; [GC threshold exceeded with 73,363,016 bytes in use.  Commencing GC.]
; [GC completed with 40,096,232 bytes retained and 33,266,784 bytes freed.]
; [GC will next occur when at least 52,096,232 bytes are in use.]
;; Reading the file took 0.18 seconds
;; Checking the proof took 15.65 seconds
;; VERIFY took 21.18 seconds
4551> DEFINE CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/admit-clause.aux-split-default-3-bldr-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; [GC threshold exceeded with 52,110,792 bytes in use.  Commencing GC.]
; [GC completed with 43,061,552 bytes retained and 9,049,240 bytes freed.]
; [GC will next occur when at least 55,061,552 bytes are in use.]
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.03 seconds
4552> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4553> VERIFY BOOLEANP-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-clause.aux-split-default-3-bldr-okp.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 2.01 seconds
;; VERIFY took 2.95 seconds
4554> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.42 seconds
;; VERIFY took 0.54 seconds
4555> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-clause.aux-split-default-3-bldr-okp.proof
; [GC threshold exceeded with 55,988,104 bytes in use.  Commencing GC.]
; [GC completed with 45,798,136 bytes retained and 10,189,968 bytes freed.]
; [GC will next occur when at least 57,798,136 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 16.13 seconds
;; VERIFY took 23.19 seconds
4556> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-clause.aux-split-default-3-bldr-okp.proof
; [GC threshold exceeded with 58,324,984 bytes in use.  Commencing GC.]
; [GC completed with 49,037,832 bytes retained and 9,287,152 bytes freed.]
; [GC will next occur when at least 61,037,832 bytes are in use.]
;; Reading the file took 0.15 seconds
;; Checking the proof took 9.26 seconds
;; VERIFY took 13.31 seconds
4557> VERIFY FORCING-SOUNDNESS-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-clause.aux-split-default-3-bldr-okp.proof
; [GC threshold exceeded with 61,048,240 bytes in use.  Commencing GC.]
; [GC completed with 4,145,528 bytes retained and 56,902,712 bytes freed.]
; [GC will next occur when at least 16,145,528 bytes are in use.]
;; Reading the file took 0.35 seconds
; [GC threshold exceeded with 17,029,104 bytes in use.  Commencing GC.]
; [GC completed with 8,934,336 bytes retained and 8,094,768 bytes freed.]
; [GC will next occur when at least 20,934,336 bytes are in use.]
;; Checking the proof took 4.34 seconds
;; VERIFY took 6.55 seconds
4558> DEFINE CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR
;; Reading from Proofs/level2/admit-clause.aux-limsplit-cutoff-step-bldr.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
4559> VERIFY CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR
;; Reading from Proofs/level2/thm-clause.aux-limsplit-cutoff-step-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4560> VERIFY CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-limsplit-cutoff-step-bldr-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4561> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-limsplit-cutoff-step-bldr.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 1.42 seconds
;; VERIFY took 1.91 seconds
4562> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-clause.aux-limsplit-cutoff-step-bldr.proof
; [GC threshold exceeded with 21,982,232 bytes in use.  Commencing GC.]
; [GC completed with 9,964,976 bytes retained and 12,017,256 bytes freed.]
; [GC will next occur when at least 21,964,976 bytes are in use.]
;; Reading the file took 0.16 seconds
;; Checking the proof took 12.35 seconds
;; VERIFY took 16.31 seconds
4563> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-clause.aux-limsplit-cutoff-step-bldr.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 1.97 seconds
;; VERIFY took 2.65 seconds
4564> DEFINE CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-OKP
;; Reading from Proofs/level2/admit-clause.aux-limsplit-cutoff-step-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.03 seconds
4565> VERIFY CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-OKP
;; Reading from Proofs/level2/thm-clause.aux-limsplit-cutoff-step-bldr-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4566> VERIFY BOOLEANP-OF-CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-clause.aux-limsplit-cutoff-step-bldr-okp.proof
; [GC threshold exceeded with 22,617,832 bytes in use.  Commencing GC.]
; [GC completed with 14,300,200 bytes retained and 8,317,632 bytes freed.]
; [GC will next occur when at least 26,300,200 bytes are in use.]
;; Reading the file took 0.14 seconds
;; Checking the proof took 2.03 seconds
;; VERIFY took 2.97 seconds
4567> VERIFY CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-clause.aux-limsplit-cutoff-step-bldr-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.42 seconds
;; VERIFY took 0.53 seconds
4568> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-clause.aux-limsplit-cutoff-step-bldr-okp.proof
; [GC threshold exceeded with 27,427,944 bytes in use.  Commencing GC.]
; [GC completed with 18,224,016 bytes retained and 9,203,928 bytes freed.]
; [GC will next occur when at least 30,224,016 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 16.13 seconds
;; VERIFY took 23.18 seconds
4569> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-clause.aux-limsplit-cutoff-step-bldr-okp.proof
; [GC threshold exceeded with 32,592,608 bytes in use.  Commencing GC.]
; [GC completed with 26,015,832 bytes retained and 6,576,776 bytes freed.]
; [GC will next occur when at least 38,015,832 bytes are in use.]
;; Reading the file took 0.17 seconds
;; Checking the proof took 9.45 seconds
;; VERIFY took 13.52 seconds
4570> VERIFY FORCING-SOUNDNESS-OF-CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-clause.aux-limsplit-cutoff-step-bldr-okp.proof
; [GC threshold exceeded with 40,336,008 bytes in use.  Commencing GC.]
; [GC completed with 12,086,752 bytes retained and 28,249,256 bytes freed.]
; [GC will next occur when at least 24,086,752 bytes are in use.]
;; Reading the file took 0.35 seconds
;; Checking the proof took 4.40 seconds
;; VERIFY took 6.58 seconds
4571> DEFINE LEVEL2.STEP-OKP
;; Reading from Proofs/level2/admit-level2.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.02 seconds
4572> VERIFY LEVEL2.STEP-OKP
;; Reading from Proofs/level2/thm-level2.step-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4573> VERIFY SOUNDNESS-OF-LEVEL2.STEP-OKP
;; Reading from Proofs/level2/thm-soundness-of-level2.step-okp.proof
; [GC threshold exceeded with 24,581,056 bytes in use.  Commencing GC.]
; [GC completed with 20,186,384 bytes retained and 4,394,672 bytes freed.]
; [GC will next occur when at least 32,186,384 bytes are in use.]
;; Reading the file took 0.20 seconds
;; Checking the proof took 3.20 seconds
;; VERIFY took 4.97 seconds
4574> VERIFY LEVEL2.STEP-OKP-WHEN-LOGIC.APPEAL-STEP-OKP
;; Reading from Proofs/level2/thm-level2.step-okp-when-logic.appeal-step-okp.proof
; [GC threshold exceeded with 32,199,168 bytes in use.  Commencing GC.]
; [GC completed with 19,632,272 bytes retained and 12,566,896 bytes freed.]
; [GC will next occur when at least 31,632,272 bytes are in use.]
; [GC threshold exceeded with 35,358,328 bytes in use.  Commencing GC.]
; [GC completed with 25,327,040 bytes retained and 10,031,288 bytes freed.]
; [GC will next occur when at least 37,327,040 bytes are in use.]
;; Reading the file took 0.65 seconds
; [GC threshold exceeded with 38,476,368 bytes in use.  Commencing GC.]
; [GC completed with 18,975,328 bytes retained and 19,501,040 bytes freed.]
; [GC will next occur when at least 30,975,328 bytes are in use.]
;; Checking the proof took 17.39 seconds
;; VERIFY took 26.96 seconds
4575> VERIFY LEVEL2.STEP-OKP-WHEN-NOT-CONSP
;; Reading from Proofs/level2/thm-level2.step-okp-when-not-consp.proof
; [GC threshold exceeded with 31,871,376 bytes in use.  Commencing GC.]
; [GC completed with 24,792,576 bytes retained and 7,078,800 bytes freed.]
; [GC will next occur when at least 36,792,576 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 3.51 seconds
;; VERIFY took 4.89 seconds
4576> DEFINE LEVEL2.FLAG-PROOFP
;; Reading from Proofs/level2/admit-level2.flag-proofp.proofs
;; 
; [GC threshold exceeded with 36,853,744 bytes in use.  Commencing GC.]
; [GC completed with 22,204,968 bytes retained and 14,648,776 bytes freed.]
; [GC will next occur when at least 34,204,968 bytes are in use.]
Reading the file took 0.14 seconds
;; Checking the proofs took 1.26 seconds
; Compiling LAMBDA (FLAG X AXIOMS THMS ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 1.84 seconds
4577> VERIFY LEVEL2.FLAG-PROOFP
;; Reading from Proofs/level2/thm-level2.flag-proofp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4578> DEFINE LEVEL2.PROOFP
;; Reading from Proofs/level2/admit-level2.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
4579> VERIFY LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-level2.proofp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4580> DEFINE LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/admit-level2.proof-listp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X AXIOMS THMS ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4581> VERIFY LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proof-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4582> VERIFY DEFINITION-OF-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-definition-of-level2.proofp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.11 seconds
4583> VERIFY DEFINITION-OF-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-definition-of-level2.proof-listp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.31 seconds
4584> VERIFY LEVEL2.PROOFP-WHEN-NOT-CONSP
;; Reading from Proofs/level2/thm-level2.proofp-when-not-consp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.08 seconds
4585> VERIFY LEVEL2.PROOF-LISTP-WHEN-NOT-CONSP
;; Reading from Proofs/level2/thm-level2.proof-listp-when-not-consp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.08 seconds
4586> VERIFY LEVEL2.PROOF-LISTP-OF-CONS
;; Reading from Proofs/level2/thm-level2.proof-listp-of-cons.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.13 seconds
4587> VERIFY LEMMA-FOR-BOOLEANP-OF-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-lemma-for-booleanp-of-level2.proofp.proof
; [GC threshold exceeded with 34,217,096 bytes in use.  Commencing GC.]
; [GC completed with 25,693,016 bytes retained and 8,524,080 bytes freed.]
; [GC will next occur when at least 37,693,016 bytes are in use.]
; [GC threshold exceeded with 43,435,480 bytes in use.  Commencing GC.]
; [GC completed with 31,761,008 bytes retained and 11,674,472 bytes freed.]
; [GC will next occur when at least 43,761,008 bytes are in use.]
;; Reading the file took 0.39 seconds
;; Checking the proof took 3.14 seconds
;; VERIFY took 4.49 seconds
4588> VERIFY BOOLEANP-OF-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-booleanp-of-level2.proofp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.17 seconds
4589> VERIFY BOOLEANP-OF-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-booleanp-of-level2.proof-listp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.17 seconds
4590> VERIFY LEVEL2.PROOF-LISTP-OF-LIST-FIX
;; Reading from Proofs/level2/thm-level2.proof-listp-of-list-fix.proof
; [GC threshold exceeded with 46,027,328 bytes in use.  Commencing GC.]
; [GC completed with 37,366,336 bytes retained and 8,660,992 bytes freed.]
; [GC will next occur when at least 49,366,336 bytes are in use.]
;; Reading the file took 0.19 seconds
;; Checking the proof took 1.17 seconds
;; VERIFY took 1.79 seconds
4591> VERIFY LEVEL2.PROOF-LISTP-OF-APP
;; Reading from Proofs/level2/thm-level2.proof-listp-of-app.proof
; [GC threshold exceeded with 51,646,184 bytes in use.  Commencing GC.]
; [GC completed with 26,048,648 bytes retained and 25,597,536 bytes freed.]
; [GC will next occur when at least 38,048,648 bytes are in use.]
;; Reading the file took 0.37 seconds
;; Checking the proof took 2.37 seconds
;; VERIFY took 3.77 seconds
4592> VERIFY LEVEL2.PROOF-LISTP-OF-REV
;; Reading from Proofs/level2/thm-level2.proof-listp-of-rev.proof
; [GC threshold exceeded with 39,492,656 bytes in use.  Commencing GC.]
; [GC completed with 34,355,160 bytes retained and 5,137,496 bytes freed.]
; [GC will next occur when at least 46,355,160 bytes are in use.]
;; Reading the file took 0.18 seconds
;; Checking the proof took 1.24 seconds
;; VERIFY took 1.88 seconds
4593> VERIFY LEVEL2.PROOFP-OF-CAR-WHEN-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proofp-of-car-when-level2.proof-listp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.28 seconds
4594> VERIFY LEVEL2.PROOF-LISTP-OF-CDR-WHEN-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proof-listp-of-cdr-when-level2.proof-listp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.18 seconds
4595> VERIFY LEVEL2.PROOFP-WHEN-MEMBERP-OF-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proofp-when-memberp-of-level2.proof-listp.proof
; [GC threshold exceeded with 46,370,288 bytes in use.  Commencing GC.]
; [GC completed with 31,771,768 bytes retained and 14,598,520 bytes freed.]
; [GC will next occur when at least 43,771,768 bytes are in use.]
;; Reading the file took 0.14 seconds
;; Checking the proof took 0.93 seconds
;; VERIFY took 1.39 seconds
4596> VERIFY LEVEL2.PROOFP-WHEN-MEMBERP-OF-LEVEL2.PROOF-LISTP-ALT
;; Reading from Proofs/level2/thm-level2.proofp-when-memberp-of-level2.proof-listp-alt.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.16 seconds
4597> VERIFY LEVEL2.PROOF-LISTP-OF-REMOVE-ALL-WHEN-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proof-listp-of-remove-all-when-level2.proof-listp.proof
; [GC threshold exceeded with 45,445,136 bytes in use.  Commencing GC.]
; [GC completed with 34,839,440 bytes retained and 10,605,696 bytes freed.]
; [GC will next occur when at least 46,839,440 bytes are in use.]
;; Reading the file took 0.13 seconds
;; Checking the proof took 0.84 seconds
;; VERIFY took 1.22 seconds
4598> VERIFY LEVEL2.PROOF-LISTP-OF-REMOVE-DUPLICATES
;; Reading from Proofs/level2/thm-level2.proof-listp-of-remove-duplicates.proof
;; Reading the file took 0.18 seconds
; [GC threshold exceeded with 47,269,984 bytes in use.  Commencing GC.]
; [GC completed with 8,772,480 bytes retained and 38,497,504 bytes freed.]
; [GC will next occur when at least 20,772,480 bytes are in use.]
;; Checking the proof took 1.40 seconds
;; VERIFY took 2.07 seconds
4599> VERIFY LEVEL2.PROOF-LISTP-OF-DIFFERENCE-WHEN-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proof-listp-of-difference-when-level2.proof-listp.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.81 seconds
;; VERIFY took 1.16 seconds
4600> VERIFY LEVEL2.PROOF-LISTP-OF-SUBSETP-WHEN-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proof-listp-of-subsetp-when-level2.proof-listp.proof
; [GC threshold exceeded with 22,322,064 bytes in use.  Commencing GC.]
; [GC completed with 11,527,728 bytes retained and 10,794,336 bytes freed.]
; [GC will next occur when at least 23,527,728 bytes are in use.]
;; Reading the file took 0.14 seconds
;; Checking the proof took 1.04 seconds
;; VERIFY took 1.51 seconds
4601> VERIFY LEVEL2.PROOF-LISTP-OF-SUBSETP-WHEN-LEVEL2.PROOF-LISTP-ALT
;; Reading from Proofs/level2/thm-level2.proof-listp-of-subsetp-when-level2.proof-listp-alt.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.07 seconds
4602> VERIFY LEVEL2.PROOF-LISTP-OF-REPEAT
;; Reading from Proofs/level2/thm-level2.proof-listp-of-repeat.proof
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.92 seconds
;; VERIFY took 1.30 seconds
4603> VERIFY LEMMA-FOR-LOGIC.PROVABLEP-WHEN-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-lemma-for-logic.provablep-when-level2.proofp.proof
; [GC threshold exceeded with 23,537,200 bytes in use.  Commencing GC.]
; [GC completed with 12,035,144 bytes retained and 11,502,056 bytes freed.]
; [GC will next occur when at least 24,035,144 bytes are in use.]
; [GC threshold exceeded with 24,043,880 bytes in use.  Commencing GC.]
; [GC completed with 16,862,856 bytes retained and 7,181,024 bytes freed.]
; [GC will next occur when at least 28,862,856 bytes are in use.]
; [GC threshold exceeded with 29,781,696 bytes in use.  Commencing GC.]
; [GC completed with 21,111,528 bytes retained and 8,670,168 bytes freed.]
; [GC will next occur when at least 33,111,528 bytes are in use.]
; [GC threshold exceeded with 46,082,592 bytes in use.  Commencing GC.]
; [GC completed with 32,943,480 bytes retained and 13,139,112 bytes freed.]
; [GC will next occur when at least 44,943,480 bytes are in use.]
; [GC threshold exceeded with 50,686,864 bytes in use.  Commencing GC.]
; [GC completed with 38,856,944 bytes retained and 11,829,920 bytes freed.]
; [GC will next occur when at least 50,856,944 bytes are in use.]
;; Reading the file took 1.34 seconds
;; Checking the proof took 14.26 seconds
;; VERIFY took 21.03 seconds
4604> VERIFY LOGIC.PROVABLEP-WHEN-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-logic.provablep-when-level2.proofp.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.38 seconds
;; VERIFY took 0.60 seconds
4605> VERIFY LOGIC.PROVABLE-LISTP-WHEN-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-logic.provable-listp-when-level2.proof-listp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.39 seconds
;; VERIFY took 0.58 seconds
4606> VERIFY LEMMA-FOR-LEVEL2.PROOFP-WHEN-LOGIC.PROOFP
;; Reading from Proofs/level2/thm-lemma-for-level2.proofp-when-logic.proofp.proof
; [GC threshold exceeded with 50,868,168 bytes in use.  Commencing GC.]
; [GC completed with 42,042,496 bytes retained and 8,825,672 bytes freed.]
; [GC will next occur when at least 54,042,496 bytes are in use.]
; [GC threshold exceeded with 57,211,816 bytes in use.  Commencing GC.]
; [GC completed with 17,612,448 bytes retained and 39,599,368 bytes freed.]
; [GC will next occur when at least 29,612,448 bytes are in use.]
;; Reading the file took 0.57 seconds
;; Checking the proof took 4.48 seconds
;; VERIFY took 6.65 seconds
4607> VERIFY LEVEL2.PROOFP-WHEN-LOGIC.PROOFP
;; Reading from Proofs/level2/thm-level2.proofp-when-logic.proofp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.27 seconds
4608> VERIFY LEVEL2.PROOF-LISTP-WHEN-LOGIC.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proof-listp-when-logic.proof-listp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.28 seconds
4609> VERIFY FORCING-LEVEL2.PROOFP-OF-LOGIC.PROVABLE-WITNESS
;; Reading from Proofs/level2/thm-forcing-level2.proofp-of-logic.provable-witness.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 seconds
4610> VERIFY INSTALL-NEW-PROOFP-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-install-new-proofp-level2.proofp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.07 seconds
4611 > SWITCH LEVEL2.PROOFP
;; SWITCH took 0.00 seconds
4612 > FINISH level2
[Doing purification: Done.]
[Undoing binding stack... done]
[Saving current lisp image into level2.nemesis-cmucl:
Writing 23630696 bytes from the Read-Only space at 0x10000000.
Writing 4743112 bytes from the Static space at 0x28000000.
Writing 8192 bytes from the Dynamic space at 0x58100000.
done.]

real	87m47.664s
user	87m14.815s
sys	0m4.976s