CMU Common Lisp 19f (19F), running on lhug-3.cs.utexas.edu
With core: /v/filer4b/v11q002/acl2space/jared/Milawa/Sources/logic.lhug-cmucl
Dumped on: Wed, 2009-10-28 23:26:43-05:00 on lhug-3.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.12 seconds
4011> VERIFY BUILD.AXIOM
;; Reading from Proofs/level2/thm-build.axiom.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.01 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.02 seconds
4014> VERIFY LOGIC.CONCLUSION-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.axiom.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4015> VERIFY LOGIC.SUBPROOFS-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.axiom.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 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.02 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.13 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.07 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 0.44 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4021> VERIFY BUILD.THEOREM-UNDER-IFF
;; Reading from Proofs/level2/thm-build.theorem-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4022> VERIFY LOGIC.METHOD-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.method-of-build.theorem.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4023> VERIFY LOGIC.CONCLUSION-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.theorem.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4024> VERIFY LOGIC.SUBPROOFS-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.theorem.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4025> VERIFY LOGIC.EXTRAS-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.extras-of-build.theorem.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 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.04 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.12 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.05 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 0.40 seconds
4028> DEFINE BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/admit-build.propositional-schema.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.04 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.01 seconds
;; VERIFY took 0.02 seconds
4030> VERIFY BUILD.PROPOSITIONAL-SCHEMA-UNDER-IFF
;; Reading from Proofs/level2/thm-build.propositional-schema-under-iff.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.14 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 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.08 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.06 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.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 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,103,376 bytes in use.  Commencing GC.]
; [GC completed with 584,752 bytes retained and 11,518,624 bytes freed.]
; [GC will next occur when at least 12,584,752 bytes are in use.]
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.25 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.08 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 0.51 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.04 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.02 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.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4042> VERIFY LOGIC.SUBPROOFS-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.cut.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.17 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.02 seconds
;; VERIFY took 0.02 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.08 seconds
;; Checking the proof took 0.40 seconds
;; VERIFY took 0.64 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,603,312 bytes in use.  Commencing GC.]
; [GC completed with 2,940,048 bytes retained and 10,663,264 bytes freed.]
; [GC will next occur when at least 14,940,048 bytes are in use.]
;; Reading the file took 0.31 seconds
;; Checking the proof took 1.54 seconds
;; VERIFY took 2.61 seconds
4046> DEFINE BUILD.CONTRACTION
;; Reading from Proofs/level2/admit-build.contraction.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.09 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.05 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.03 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.02 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.02 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.08 seconds
4052> VERIFY LOGIC.EXTRAS-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.extras-of-build.contraction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 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.17 seconds
;; VERIFY took 0.28 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.09 seconds
;; Checking the proof took 0.51 seconds
;; VERIFY took 0.81 seconds
4055> DEFINE BUILD.EXPANSION
;; Reading from Proofs/level2/admit-build.expansion.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4056> VERIFY BUILD.EXPANSION
;; Reading from Proofs/level2/thm-build.expansion.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4057> VERIFY BUILD.EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.expansion-under-iff.proof
;; Reading the file took 0.03 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.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4059> VERIFY LOGIC.CONCLUSION-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.expansion.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
4060> VERIFY LOGIC.SUBPROOFS-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.expansion.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.13 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.04 seconds
;; VERIFY took 0.07 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.11 seconds
;; VERIFY took 0.17 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,167,184 bytes in use.  Commencing GC.]
; [GC completed with 3,827,712 bytes retained and 11,339,472 bytes freed.]
; [GC will next occur when at least 15,827,712 bytes are in use.]
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.36 seconds
;; VERIFY took 0.58 seconds
4064> DEFINE BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.associativity.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.03 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.02 seconds
4066> VERIFY BUILD.ASSOCIATIVITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.associativity-under-iff.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 seconds
4067> VERIFY LOGIC.METHOD-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.method-of-build.associativity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.08 seconds
4068> VERIFY LOGIC.CONCLUSION-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.07 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.03 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.06 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.09 seconds
;; Checking the proof took 0.35 seconds
;; VERIFY took 0.57 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.10 seconds
;; Checking the proof took 0.95 seconds
;; VERIFY took 1.46 seconds
4073> DEFINE BUILD.INSTANTIATION
;; Reading from Proofs/level2/admit-build.instantiation.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X SIGMA): 
; Compiling Top-Level Form: 
;; DEFINE took 0.00 seconds
4074> VERIFY BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-build.instantiation.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.04 seconds
4076> VERIFY LOGIC.METHOD-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.method-of-build.instantiation.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.25 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.08 seconds
;; VERIFY took 0.13 seconds
4078> VERIFY LOGIC.SUBPROOFS-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.instantiation.proof
; [GC threshold exceeded with 15,840,320 bytes in use.  Commencing GC.]
; [GC completed with 643,648 bytes retained and 15,196,672 bytes freed.]
; [GC will next occur when at least 12,643,648 bytes are in use.]
;; Reading the file took 0.15 seconds
;; Checking the proof took 0.49 seconds
;; VERIFY took 0.89 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.13 seconds
;; VERIFY took 0.21 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.08 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 0.39 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.19 seconds
;; Checking the proof took 0.80 seconds
;; VERIFY took 1.35 seconds
4082> DEFINE BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/admit-build.functional-equality.proofs
;; Reading the file took 0.01 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.03 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,667,672 bytes in use.  Commencing GC.]
; [GC completed with 1,418,048 bytes retained and 11,249,624 bytes freed.]
; [GC will next occur when at least 13,418,048 bytes are in use.]
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 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.05 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 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.02 seconds
;; Checking the proof took 0.01 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.09 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.30 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.18 seconds
;; Checking the proof took 0.87 seconds
;; VERIFY took 1.40 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.07 seconds
4092> VERIFY BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-build.beta-reduction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 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.06 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.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 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.05 seconds
;; VERIFY took 0.07 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.05 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.10 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.02 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.06 seconds
;; Checking the proof took 0.46 seconds
;; VERIFY took 0.68 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,428,552 bytes in use.  Commencing GC.]
; [GC completed with 1,612,432 bytes retained and 11,816,120 bytes freed.]
; [GC will next occur when at least 13,612,432 bytes are in use.]
;; Reading the file took 0.30 seconds
;; Checking the proof took 1.39 seconds
;; VERIFY took 2.34 seconds
4100> DEFINE BUILD.BASE-EVAL
;; Reading from Proofs/level2/admit-build.base-eval.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
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.02 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.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 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.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 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.04 seconds
;; VERIFY took 0.11 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 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.07 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.22 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.08 seconds
;; Checking the proof took 0.37 seconds
;; VERIFY took 0.59 seconds
4109> DEFINE BUILD.INSTANTIATION-LIST
;; Reading from Proofs/level2/admit-build.instantiation-list.proofs
; [GC threshold exceeded with 13,653,784 bytes in use.  Commencing GC.]
; [GC completed with 2,549,656 bytes retained and 11,104,128 bytes freed.]
; [GC will next occur when at least 14,549,656 bytes are in use.]
;; Reading the file took 0.07 seconds
;; Checking the proofs took 0.10 seconds
; Compiling LAMBDA (X SIGMA): 
; Compiling Top-Level Form: 
;; DEFINE took 0.20 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.04 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.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.09 seconds
4112> VERIFY BUILD.INSTANTIATION-LIST-OF-CONS
;; Reading from Proofs/level2/thm-build.instantiation-list-of-cons.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.10 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.20 seconds
;; Checking the proof took 1.16 seconds
;; VERIFY took 1.76 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 15,125,968 bytes in use.  Commencing GC.]
; [GC completed with 3,804,408 bytes retained and 11,321,560 bytes freed.]
; [GC will next occur when at least 15,804,408 bytes are in use.]
;; Reading the file took 0.25 seconds
;; Checking the proof took 1.07 seconds
;; VERIFY took 1.70 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,320,872 bytes in use.  Commencing GC.]
; [GC completed with 10,966,200 bytes retained and 7,354,672 bytes freed.]
; [GC will next occur when at least 22,966,200 bytes are in use.]
;; Reading the file took 0.41 seconds
;; Checking the proof took 1.53 seconds
;; VERIFY took 2.55 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.06 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.05 seconds
4118> VERIFY BUILD.INDUCTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.induction-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 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.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4121> VERIFY LOGIC.SUBPROOFS-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.induction.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 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.11 seconds
;; VERIFY took 0.14 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.06 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.21 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,555,528 bytes in use.  Commencing GC.]
; [GC completed with 11,521,936 bytes retained and 13,033,592 bytes freed.]
; [GC will next occur when at least 23,521,936 bytes are in use.]
;; Reading the file took 0.39 seconds
;; Checking the proof took 3.21 seconds
;; VERIFY took 5.37 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.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.06 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.02 seconds
;; VERIFY took 0.05 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.03 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.30 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.06 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.15 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.23 seconds
;; VERIFY took 0.40 seconds
4131> DEFINE BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/admit-build.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
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.02 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,196,144 bytes in use.  Commencing GC.]
; [GC completed with 15,615,792 bytes retained and 8,580,352 bytes freed.]
; [GC will next occur when at least 27,615,792 bytes are in use.]
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.81 seconds
;; VERIFY took 1.29 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.06 seconds
;; Checking the proof took 0.26 seconds
;; VERIFY took 0.39 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.21 seconds
;; Checking the proof took 6.73 seconds
;; VERIFY took 10.09 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,516,096 bytes in use.  Commencing GC.]
; [GC completed with 2,840,176 bytes retained and 25,675,920 bytes freed.]
; [GC will next occur when at least 14,840,176 bytes are in use.]
;; Reading the file took 0.38 seconds
;; Checking the proof took 4.27 seconds
;; VERIFY took 6.64 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,251,792 bytes in use.  Commencing GC.]
; [GC completed with 9,981,120 bytes retained and 5,270,672 bytes freed.]
; [GC will next occur when at least 21,981,120 bytes are in use.]
;; Reading the file took 0.43 seconds
;; Checking the proof took 2.53 seconds
;; VERIFY took 4.16 seconds
4138> DEFINE BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/admit-build.right-expansion.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X B): 
; Compiling Top-Level Form: 
;; DEFINE took 0.10 seconds
4139> VERIFY BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-build.right-expansion.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 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.02 seconds
;; VERIFY took 0.04 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.08 seconds
;; VERIFY took 0.13 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.13 seconds
;; Checking the proof took 0.45 seconds
;; VERIFY took 0.71 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,204,528 bytes in use.  Commencing GC.]
; [GC completed with 5,398,064 bytes retained and 16,806,464 bytes freed.]
; [GC will next occur when at least 17,398,064 bytes are in use.]
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.33 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.05 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.02 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.08 seconds
;; Checking the proof took 0.55 seconds
;; VERIFY took 0.82 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.06 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.30 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,946,984 bytes in use.  Commencing GC.]
; [GC completed with 10,451,720 bytes retained and 7,495,264 bytes freed.]
; [GC will next occur when at least 22,451,720 bytes are in use.]
;; Reading the file took 0.39 seconds
;; Checking the proof took 10.28 seconds
;; VERIFY took 15.55 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.17 seconds
; [GC threshold exceeded with 22,460,792 bytes in use.  Commencing GC.]
; [GC completed with 8,226,200 bytes retained and 14,234,592 bytes freed.]
; [GC will next occur when at least 20,226,200 bytes are in use.]
;; Checking the proof took 2.41 seconds
;; VERIFY took 3.66 seconds
4150> VERIFY FORCING-SOUNDNESS-OF-BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.right-expansion-okp.proof
;; 
; [GC threshold exceeded with 20,568,208 bytes in use.  Commencing GC.]
; [GC completed with 11,758,328 bytes retained and 8,809,880 bytes freed.]
; [GC will next occur when at least 23,758,328 bytes are in use.]
Reading the file took 0.42 seconds
;; Checking the proof took 1.82 seconds
;; VERIFY took 3.20 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.02 seconds
;; VERIFY took 0.04 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.07 seconds
;; Checking the proof took 0.78 seconds
;; VERIFY took 1.14 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.19 seconds
;; Checking the proof took 1.00 seconds
;; VERIFY took 1.61 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 24,255,032 bytes in use.  Commencing GC.]
; [GC completed with 6,390,624 bytes retained and 17,864,408 bytes freed.]
; [GC will next occur when at least 18,390,624 bytes are in use.]
;; Reading the file took 0.29 seconds
;; Checking the proof took 9.15 seconds
;; VERIFY took 13.48 seconds
4157> DEFINE BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/admit-build.modus-ponens-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
4158> VERIFY BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-build.modus-ponens-okp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.10 seconds
;; Checking the proof took 1.01 seconds
;; VERIFY took 1.54 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.02 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 0.43 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,401,432 bytes in use.  Commencing GC.]
; [GC completed with 9,345,728 bytes retained and 9,055,704 bytes freed.]
; [GC will next occur when at least 21,345,728 bytes are in use.]
;; Reading the file took 0.37 seconds
;; Checking the proof took 12.43 seconds
;; VERIFY took 18.43 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,354,736 bytes in use.  Commencing GC.]
; [GC completed with 8,899,048 bytes retained and 12,455,688 bytes freed.]
; [GC will next occur when at least 20,899,048 bytes are in use.]
;; Reading the file took 0.25 seconds
;; Checking the proof took 5.96 seconds
;; VERIFY took 8.81 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 20,914,104 bytes in use.  Commencing GC.]
; [GC completed with 13,100,728 bytes retained and 7,813,376 bytes freed.]
; [GC will next occur when at least 25,100,728 bytes are in use.]
; [GC threshold exceeded with 32,065,168 bytes in use.  Commencing GC.]
; [GC completed with 21,701,384 bytes retained and 10,363,784 bytes freed.]
; [GC will next occur when at least 33,701,384 bytes are in use.]
;; Reading the file took 0.93 seconds
;; Checking the proof took 7.78 seconds
;; VERIFY took 12.32 seconds
4164> DEFINE BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/admit-build.modus-ponens-2.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.09 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.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 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.11 seconds
;; Checking the proof took 0.86 seconds
;; VERIFY took 1.30 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.08 seconds
;; VERIFY took 0.14 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
;; Reading the file took 0.22 seconds
; [GC threshold exceeded with 34,275,224 bytes in use.  Commencing GC.]
; [GC completed with 24,547,648 bytes retained and 9,727,576 bytes freed.]
; [GC will next occur when at least 36,547,648 bytes are in use.]
;; Checking the proof took 10.29 seconds
;; VERIFY took 15.18 seconds
4170> DEFINE BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/admit-build.modus-ponens-2-okp.proofs
;; Reading the file took 0.10 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.15 seconds
4171> VERIFY BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-build.modus-ponens-2-okp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.10 seconds
;; Checking the proof took 0.94 seconds
;; VERIFY took 1.42 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
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.30 seconds
;; VERIFY took 0.46 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 36,562,152 bytes in use.  Commencing GC.]
; [GC completed with 7,862,456 bytes retained and 28,699,696 bytes freed.]
; [GC will next occur when at least 19,862,456 bytes are in use.]
;; Reading the file took 0.40 seconds
;; Checking the proof took 12.21 seconds
;; VERIFY took 18.12 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
; [GC threshold exceeded with 20,738,960 bytes in use.  Commencing GC.]
; [GC completed with 10,670,440 bytes retained and 10,068,520 bytes freed.]
; [GC will next occur when at least 22,670,440 bytes are in use.]
;; Reading the file took 0.30 seconds
;; Checking the proof took 7.18 seconds
;; VERIFY took 10.59 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,180,768 bytes in use.  Commencing GC.]
; [GC completed with 13,524,920 bytes retained and 9,655,848 bytes freed.]
; [GC will next occur when at least 25,524,920 bytes are in use.]
; [GC threshold exceeded with 27,912,992 bytes in use.  Commencing GC.]
; [GC completed with 18,786,392 bytes retained and 9,126,600 bytes freed.]
; [GC will next occur when at least 30,786,392 bytes are in use.]
;; Reading the file took 0.90 seconds
;; Checking the proof took 7.69 seconds
;; VERIFY took 12.12 seconds
4177> DEFINE BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.right-associativity.proofs
;; Reading the file took 0.09 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.12 seconds
4178> VERIFY BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.right-associativity.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.09 seconds
4179> VERIFY BUILD.RIGHT-ASSOCIATIVITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.right-associativity-under-iff.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.11 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.09 seconds
;; Checking the proof took 3.26 seconds
;; VERIFY took 4.54 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 31,034,248 bytes in use.  Commencing GC.]
; [GC completed with 23,031,080 bytes retained and 8,003,168 bytes freed.]
; [GC will next occur when at least 35,031,080 bytes are in use.]
;; Reading the file took 0.55 seconds
; [GC threshold exceeded with 35,045,080 bytes in use.  Commencing GC.]
; [GC completed with 26,545,608 bytes retained and 8,499,472 bytes freed.]
; [GC will next occur when at least 38,545,608 bytes are in use.]
;; Checking the proof took 28.78 seconds
;; VERIFY took 38.96 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.11 seconds
;; Checking the proof took 5.14 seconds
;; VERIFY took 7.18 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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 39,348,648 bytes in use.  Commencing GC.]
; [GC completed with 11,194,688 bytes retained and 28,153,960 bytes freed.]
; [GC will next occur when at least 23,194,688 bytes are in use.]
;; Reading the file took 0.31 seconds
;; Checking the proof took 2.21 seconds
;; VERIFY took 3.51 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.02 seconds
;; Checking the proof took 0.45 seconds
;; VERIFY took 0.64 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 24,061,936 bytes in use.  Commencing GC.]
; [GC completed with 17,369,424 bytes retained and 6,692,512 bytes freed.]
; [GC will next occur when at least 29,369,424 bytes are in use.]
;; Reading the file took 0.40 seconds
;; Checking the proof took 17.37 seconds
;; VERIFY took 26.01 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
;; Reading the file took 0.23 seconds
; [GC threshold exceeded with 29,412,608 bytes in use.  Commencing GC.]
; [GC completed with 16,609,792 bytes retained and 12,802,816 bytes freed.]
; [GC will next occur when at least 28,609,792 bytes are in use.]
;; Checking the proof took 10.05 seconds
;; VERIFY took 14.96 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 30,918,288 bytes in use.  Commencing GC.]
; [GC completed with 23,578,504 bytes retained and 7,339,784 bytes freed.]
; [GC will next occur when at least 35,578,504 bytes are in use.]
;; Reading the file took 0.59 seconds
;; Checking the proof took 4.71 seconds
;; VERIFY took 7.50 seconds
4190> DEFINE BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/admit-build.disjoined-left-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.06 seconds
4191> VERIFY BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/thm-build.disjoined-left-expansion.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.07 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 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.06 seconds
;; Checking the proof took 0.40 seconds
;; VERIFY took 0.60 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 35,684,808 bytes in use.  Commencing GC.]
; [GC completed with 3,679,784 bytes retained and 32,005,024 bytes freed.]
; [GC will next occur when at least 15,679,784 bytes are in use.]
;; Reading the file took 0.34 seconds
;; Checking the proof took 4.21 seconds
;; VERIFY took 5.91 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.15 seconds
;; Checking the proof took 0.67 seconds
;; VERIFY took 1.10 seconds
4196> DEFINE BUILD.DISJOINED-LEFT-EXPANSION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-left-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.03 seconds
4197> VERIFY BUILD.DISJOINED-LEFT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-build.disjoined-left-expansion-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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,693,160 bytes in use.  Commencing GC.]
; [GC completed with 6,641,608 bytes retained and 9,051,552 bytes freed.]
; [GC will next occur when at least 18,641,608 bytes are in use.]
;; Reading the file took 0.30 seconds
;; Checking the proof took 1.80 seconds
;; VERIFY took 2.89 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.07 seconds
;; Checking the proof took 0.35 seconds
;; VERIFY took 0.54 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,651,800 bytes in use.  Commencing GC.]
; [GC completed with 9,442,592 bytes retained and 9,209,208 bytes freed.]
; [GC will next occur when at least 21,442,592 bytes are in use.]
;; 
; [GC threshold exceeded with 21,538,568 bytes in use.  Commencing GC.]
; [GC completed with 13,645,888 bytes retained and 7,892,680 bytes freed.]
; [GC will next occur when at least 25,645,888 bytes are in use.]
Reading the file took 0.51 seconds
;; Checking the proof took 24.30 seconds
;; VERIFY took 36.62 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.26 seconds
;; Checking the proof took 6.27 seconds
;; VERIFY took 9.41 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,861,248 bytes in use.  Commencing GC.]
; [GC completed with 13,260,056 bytes retained and 12,601,192 bytes freed.]
; [GC will next occur when at least 25,260,056 bytes are in use.]
; [GC threshold exceeded with 27,160,264 bytes in use.  Commencing GC.]
; [GC completed with 18,362,680 bytes retained and 8,797,584 bytes freed.]
; [GC will next occur when at least 30,362,680 bytes are in use.]
;; Reading the file took 0.89 seconds
;; Checking the proof took 4.34 seconds
;; VERIFY took 7.26 seconds
4203> DEFINE BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/admit-build.disjoined-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.04 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.00 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.04 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.08 seconds
;; Checking the proof took 1.58 seconds
;; VERIFY took 2.26 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 30,376,656 bytes in use.  Commencing GC.]
; [GC completed with 7,261,336 bytes retained and 23,115,320 bytes freed.]
; [GC will next occur when at least 19,261,336 bytes are in use.]
; [GC threshold exceeded with 21,629,696 bytes in use.  Commencing GC.]
; [GC completed with 13,862,480 bytes retained and 7,767,216 bytes freed.]
; [GC will next occur when at least 25,862,480 bytes are in use.]
;; Reading the file took 0.53 seconds
;; Checking the proof took 7.76 seconds
;; VERIFY took 10.99 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.10 seconds
;; Checking the proof took 2.74 seconds
;; VERIFY took 3.99 seconds
4209> DEFINE BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-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.06 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.01 seconds
;; VERIFY took 0.02 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,386,768 bytes in use.  Commencing GC.]
; [GC completed with 13,343,280 bytes retained and 13,043,488 bytes freed.]
; [GC will next occur when at least 25,343,280 bytes are in use.]
;; Reading the file took 0.28 seconds
;; Checking the proof took 1.82 seconds
;; VERIFY took 2.88 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.05 seconds
;; Checking the proof took 0.36 seconds
;; VERIFY took 0.52 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,751,224 bytes in use.  Commencing GC.]
; [GC completed with 20,147,664 bytes retained and 7,603,560 bytes freed.]
; [GC will next occur when at least 32,147,664 bytes are in use.]
;; Reading the file took 0.55 seconds
;; Checking the proof took 24.62 seconds
;; VERIFY took 36.80 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.21 seconds
;; Checking the proof took 6.31 seconds
;; VERIFY took 9.42 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,160,576 bytes in use.  Commencing GC.]
; [GC completed with 6,705,888 bytes retained and 25,454,688 bytes freed.]
; [GC will next occur when at least 18,705,888 bytes are in use.]
; [GC threshold exceeded with 20,808,024 bytes in use.  Commencing GC.]
; [GC completed with 13,570,888 bytes retained and 7,237,136 bytes freed.]
; [GC will next occur when at least 25,570,888 bytes are in use.]
;; Reading the file took 0.77 seconds
;; Checking the proof took 4.36 seconds
;; VERIFY took 7.14 seconds
4216> DEFINE BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/admit-build.disjoined-contraction.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.10 seconds
4217> VERIFY BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/thm-build.disjoined-contraction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 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.02 seconds
;; VERIFY took 0.04 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,587,320 bytes in use.  Commencing GC.]
; [GC completed with 11,634,216 bytes retained and 13,953,104 bytes freed.]
; [GC will next occur when at least 23,634,216 bytes are in use.]
;; Reading the file took 0.22 seconds
;; Checking the proof took 4.07 seconds
;; VERIFY took 5.87 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.15 seconds
;; Checking the proof took 1.00 seconds
;; VERIFY took 1.52 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,633,344 bytes in use.  Commencing GC.]
; [GC completed with 16,354,248 bytes retained and 9,279,096 bytes freed.]
; [GC will next occur when at least 28,354,248 bytes are in use.]
;; Reading the file took 0.30 seconds
;; Checking the proof took 16.09 seconds
;; VERIFY took 22.80 seconds
4222> DEFINE BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-contraction-okp.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.09 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.00 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,368,528 bytes in use.  Commencing GC.]
; [GC completed with 14,112,640 bytes retained and 14,255,888 bytes freed.]
; [GC will next occur when at least 26,112,640 bytes are in use.]
;; Reading the file took 0.20 seconds
;; Checking the proof took 1.74 seconds
;; VERIFY took 2.66 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.41 seconds
;; VERIFY took 0.59 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,280 bytes in use.  Commencing GC.]
; [GC completed with 19,980,816 bytes retained and 6,445,464 bytes freed.]
; [GC will next occur when at least 31,980,816 bytes are in use.]
;; Reading the file took 0.32 seconds
;; Checking the proof took 17.75 seconds
;; VERIFY took 26.21 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,373,352 bytes in use.  Commencing GC.]
; [GC completed with 13,240,720 bytes retained and 19,132,632 bytes freed.]
; [GC will next occur when at least 25,240,720 bytes are in use.]
0.24 seconds
;; Checking the proof took 13.33 seconds
;; VERIFY took 19.69 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,507,488 bytes in use.  Commencing GC.]
; [GC completed with 19,802,024 bytes retained and 6,705,464 bytes freed.]
; [GC will next occur when at least 31,802,024 bytes are in use.]
;; Reading the file took 0.72 seconds
;; Checking the proof took 7.85 seconds
;; VERIFY took 12.18 seconds
4229> DEFINE BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/admit-build.cancel-neg-neg.proofs
; [GC threshold exceeded with 31,814,376 bytes in use.  Commencing GC.]
; [GC completed with 13,258,808 bytes retained and 18,555,568 bytes freed.]
; [GC will next occur when at least 25,258,808 bytes are in use.]
;; Reading the file took 0.06 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.08 seconds
4230> VERIFY BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/thm-build.cancel-neg-neg.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.01 seconds
;; Checking the proof took 0.02 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.06 seconds
;; Checking the proof took 0.54 seconds
;; VERIFY took 0.76 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.27 seconds
;; Checking the proof took 2.87 seconds
;; VERIFY took 4.08 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.09 seconds
;; Checking the proof took 0.69 seconds
;; VERIFY took 1.03 seconds
4235> DEFINE BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/admit-build.cancel-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.04 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.01 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,270,688 bytes in use.  Commencing GC.]
; [GC completed with 13,880,856 bytes retained and 11,389,832 bytes freed.]
; [GC will next occur when at least 25,880,856 bytes are in use.]
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.62 seconds
;; VERIFY took 0.91 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.07 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.36 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.20 seconds
;; Checking the proof took 5.85 seconds
;; VERIFY took 8.63 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 25,975,576 bytes in use.  Commencing GC.]
; [GC completed with 14,643,184 bytes retained and 11,332,392 bytes freed.]
; [GC will next occur when at least 26,643,184 bytes are in use.]
;; Reading the file took 0.26 seconds
;; Checking the proof took 4.99 seconds
;; VERIFY took 7.38 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,087,640 bytes in use.  Commencing GC.]
; [GC completed with 20,775,152 bytes retained and 6,312,488 bytes freed.]
; [GC will next occur when at least 32,775,152 bytes are in use.]
;; Reading the file took 0.61 seconds
;; Checking the proof took 3.99 seconds
;; VERIFY took 6.43 seconds
4242> DEFINE BUILD.INSERT-NEG-NEG
;; Reading from Proofs/level2/admit-build.insert-neg-neg.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.07 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.00 seconds
;; VERIFY took 0.05 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 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 
; [GC threshold exceeded with 32,827,752 bytes in use.  Commencing GC.]
; [GC completed with 946,432 bytes retained and 31,881,320 bytes freed.]
; [GC will next occur when at least 12,946,432 bytes are in use.]
0.05 seconds
;; Checking the proof took 0.36 seconds
;; VERIFY took 0.65 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.09 seconds
;; Checking the proof took 1.33 seconds
;; VERIFY took 1.76 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.14 seconds
;; Checking the proof took 0.50 seconds
;; VERIFY took 0.83 seconds
4248> DEFINE BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/admit-build.insert-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.06 seconds
4249> VERIFY BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-build.insert-neg-neg-okp.proof
;; Reading the file took 0.02 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.08 seconds
;; Checking the proof took 0.56 seconds
;; VERIFY took 0.83 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.05 seconds
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.31 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 12,955,792 bytes in use.  Commencing GC.]
; [GC completed with 2,554,344 bytes retained and 10,401,448 bytes freed.]
; [GC will next occur when at least 14,554,344 bytes are in use.]
; [GC threshold exceeded with 18,269,192 bytes in use.  Commencing GC.]
; [GC completed with 9,113,040 bytes retained and 9,156,152 bytes freed.]
; [GC will next occur when at least 21,113,040 bytes are in use.]
;; Reading the file took 0.69 seconds
;; Checking the proof took 9.65 seconds
;; VERIFY took 14.54 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.19 seconds
;; Checking the proof took 2.43 seconds
;; VERIFY took 3.66 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,476,064 bytes in use.  Commencing GC.]
; [GC completed with 12,641,016 bytes retained and 8,835,048 bytes freed.]
; [GC will next occur when at least 24,641,016 bytes are in use.]
;; Reading the file took 0.30 seconds
;; Checking the proof took 1.27 seconds
;; VERIFY took 2.13 seconds
4255> DEFINE BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/admit-build.lhs-insert-neg-neg.proofs
;; Reading the file took 0.07 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.09 seconds
4256> VERIFY BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.04 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.08 seconds
;; Checking the proof took 0.75 seconds
;; VERIFY took 1.12 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 26,602,976 bytes in use.  Commencing GC.]
; [GC completed with 12,219,528 bytes retained and 14,383,448 bytes freed.]
; [GC will next occur when at least 24,219,528 bytes are in use.]
;; Reading the file took 0.37 seconds
;; Checking the proof took 4.27 seconds
;; VERIFY took 5.91 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.12 seconds
;; Checking the proof took 1.45 seconds
;; VERIFY took 2.08 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.01 seconds
;; Checking the proofs took 0.00 seconds
; [GC threshold exceeded with 24,233,736 bytes in use.  Commencing GC.]
; [GC completed with 12,943,752 bytes retained and 11,289,984 bytes freed.]
; [GC will next occur when at least 24,943,752 bytes are in use.]
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.07 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.03 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.16 seconds
;; Checking the proof took 1.64 seconds
;; VERIFY took 2.46 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.06 seconds
;; Checking the proof took 0.41 seconds
;; VERIFY took 0.59 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,159,736 bytes in use.  Commencing GC.]
; [GC completed with 4,880,720 bytes retained and 20,279,016 bytes freed.]
; [GC will next occur when at least 16,880,720 bytes are in use.]
; [GC threshold exceeded with 18,753,384 bytes in use.  Commencing GC.]
; [GC completed with 10,616,296 bytes retained and 8,137,088 bytes freed.]
; [GC will next occur when at least 22,616,296 bytes are in use.]
; [GC threshold exceeded with 27,264,680 bytes in use.  Commencing GC.]
; [GC completed with 15,651,760 bytes retained and 11,612,920 bytes freed.]
; [GC will next occur when at least 27,651,760 bytes are in use.]
;; Reading the file took 1.33 seconds
;; Checking the proof took 32.71 seconds
;; VERIFY took 48.97 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.30 seconds
;; Checking the proof took 6.47 seconds
;; VERIFY took 9.63 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,006,088 bytes in use.  Commencing GC.]
; [GC completed with 18,866,056 bytes retained and 9,140,032 bytes freed.]
; [GC will next occur when at least 30,866,056 bytes are in use.]
;; 
; [GC threshold exceeded with 31,185,880 bytes in use.  Commencing GC.]
; [GC completed with 8,164,968 bytes retained and 23,020,912 bytes freed.]
; [GC will next occur when at least 20,164,968 bytes are in use.]
Reading the file took 0.56 seconds
;; Checking the proof took 3.03 seconds
;; VERIFY took 5.11 seconds
4268> DEFINE BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/admit-build.merge-negatives.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 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.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.06 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.15 seconds
;; Checking the proof took 19.40 seconds
;; VERIFY took 27.09 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,180,736 bytes in use.  Commencing GC.]
; [GC completed with 11,458,104 bytes retained and 8,722,632 bytes freed.]
; [GC will next occur when at least 23,458,104 bytes are in use.]
; [GC threshold exceeded with 24,869,680 bytes in use.  Commencing GC.]
; [GC completed with 16,267,728 bytes retained and 8,601,952 bytes freed.]
; [GC will next occur when at least 28,267,728 bytes are in use.]
;; Reading the file took 0.76 seconds
;; Checking the proof took 47.87 seconds
;; VERIFY took 66.98 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 28,494,024 bytes in use.  Commencing GC.]
; [GC completed with 23,122,944 bytes retained and 5,371,080 bytes freed.]
; [GC will next occur when at least 35,122,944 bytes are in use.]
;; Reading the file took 0.30 seconds
;; Checking the proof took 27.45 seconds
;; VERIFY took 39.18 seconds
4274> DEFINE BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/admit-build.merge-negatives-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.05 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.16 seconds
;; Checking the proof took 1.72 seconds
;; VERIFY took 2.58 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,132,824 bytes in use.  Commencing GC.]
; [GC completed with 22,288,112 bytes retained and 12,844,712 bytes freed.]
; [GC will next occur when at least 34,288,112 bytes are in use.]
;; Reading the file took 0.11 seconds
;; Checking the proof took 0.42 seconds
;; VERIFY took 0.66 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 35,764,464 bytes in use.  Commencing GC.]
; [GC completed with 28,717,088 bytes retained and 7,047,376 bytes freed.]
; [GC will next occur when at least 40,717,088 bytes are in use.]
;; Reading the file took 0.47 seconds
;; Checking the proof took 15.33 seconds
;; VERIFY took 22.52 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 41,894,224 bytes in use.  Commencing GC.]
; [GC completed with 13,636,464 bytes retained and 28,257,760 bytes freed.]
; [GC will next occur when at least 25,636,464 bytes are in use.]
;; Reading the file took 0.41 seconds
;; Checking the proof took 7.45 seconds
;; VERIFY took 11.08 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 25,729,072 bytes in use.  Commencing GC.]
; [GC completed with 21,041,728 bytes retained and 4,687,344 bytes freed.]
; [GC will next occur when at least 33,041,728 bytes are in use.]
; [GC threshold exceeded with 35,891,320 bytes in use.  Commencing GC.]
; [GC completed with 25,841,208 bytes retained and 10,050,112 bytes freed.]
; [GC will next occur when at least 37,841,208 bytes are in use.]
;; Reading the file took 0.92 seconds
;; Checking the proof took 5.93 seconds
;; VERIFY took 9.45 seconds
4281> DEFINE BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/admit-build.merge-implications-lemma-1.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X A): 
; Compiling Top-Level Form: 
;; DEFINE took 0.03 seconds
4282> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-1.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.12 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.02 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.11 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.15 seconds
;; Checking the proof took 18.31 seconds
;; VERIFY took 25.44 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 37,851,736 bytes in use.  Commencing GC.]
; [GC completed with 28,931,680 bytes retained and 8,920,056 bytes freed.]
; [GC will next occur when at least 40,931,680 bytes are in use.]
; [GC threshold exceeded with 44,621,944 bytes in use.  Commencing GC.]
; [GC completed with 16,867,120 bytes retained and 27,754,824 bytes freed.]
; [GC will next occur when at least 28,867,120 bytes are in use.]
;; Reading the file took 1.09 seconds
; [GC threshold exceeded with 30,016,448 bytes in use.  Commencing GC.]
; [GC completed with 24,761,984 bytes retained and 5,254,464 bytes freed.]
; [GC will next occur when at least 36,761,984 bytes are in use.]
;; Checking the proof took 57.10 seconds
;; VERIFY took 79.87 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.18 seconds
; [GC threshold exceeded with 36,772,352 bytes in use.  Commencing GC.]
; [GC completed with 26,627,080 bytes retained and 10,145,272 bytes freed.]
; [GC will next occur when at least 38,627,080 bytes are in use.]
;; Checking the proof took 32.41 seconds
;; VERIFY took 46.53 seconds
4287> DEFINE BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/admit-build.merge-implications-lemma-2.proofs
;; Reading the file took 0.07 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.12 seconds
4288> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-2.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 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.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 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.15 seconds
;; Checking the proof took 15.06 seconds
;; VERIFY took 21.16 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 38,639,992 bytes in use.  Commencing GC.]
; [GC completed with 30,945,656 bytes retained and 7,694,336 bytes freed.]
; [GC will next occur when at least 42,945,656 bytes are in use.]
;; Reading the file took 0.59 seconds
; [GC threshold exceeded with 42,955,768 bytes in use.  Commencing GC.]
; [GC completed with 34,535,544 bytes retained and 8,420,224 bytes freed.]
; [GC will next occur when at least 46,535,544 bytes are in use.]
;; Checking the proof took 67.17 seconds
;; VERIFY took 95.94 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.16 seconds
;; Checking the proof took 19.04 seconds
;; VERIFY took 27.15 seconds
4293> DEFINE BUILD.MERGE-IMPLICATIONS
;; Reading from Proofs/level2/admit-build.merge-implications.proofs
;; Reading the file took 0.01 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.02 seconds
4295> VERIFY BUILD.MERGE-IMPLICATIONS-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-implications-under-iff.proof
;; Reading the file took 0.01 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 47,026,640 bytes in use.  Commencing GC.]
; [GC completed with 36,088,528 bytes retained and 10,938,112 bytes freed.]
; [GC will next occur when at least 48,088,528 bytes are in use.]
;; Reading the file took 0.11 seconds
;; Checking the proof took 1.59 seconds
;; VERIFY took 2.29 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 50,171,336 bytes in use.  Commencing GC.]
; [GC completed with 31,527,816 bytes retained and 18,643,520 bytes freed.]
; [GC will next occur when at least 43,527,816 bytes are in use.]
;; Reading the file took 0.71 seconds
;; Checking the proof took 26.92 seconds
;; VERIFY took 38.41 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.12 seconds
;; Checking the proof took 2.10 seconds
;; VERIFY took 3.05 seconds
4299> DEFINE BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/admit-build.merge-implications-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.09 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.00 seconds
;; VERIFY took 0.03 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 43,538,464 bytes in use.  Commencing GC.]
; [GC completed with 35,555,824 bytes retained and 7,982,640 bytes freed.]
; [GC will next occur when at least 47,555,824 bytes are in use.]
; [GC threshold exceeded with 48,272,064 bytes in use.  Commencing GC.]
; [GC completed with 41,814,016 bytes retained and 6,458,048 bytes freed.]
; [GC will next occur when at least 53,814,016 bytes are in use.]
;; Reading the file took 0.52 seconds
;; Checking the proof took 6.78 seconds
;; VERIFY took 10.36 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.04 seconds
;; Checking the proof took 0.88 seconds
;; VERIFY took 1.13 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 53,823,512 bytes in use.  Commencing GC.]
; [GC completed with 49,376,640 bytes retained and 4,446,872 bytes freed.]
; [GC will next occur when at least 61,376,640 bytes are in use.]
; [GC threshold exceeded with 65,150,152 bytes in use.  Commencing GC.]
; [GC completed with 34,774,616 bytes retained and 30,375,536 bytes freed.]
; [GC will next occur when at least 46,774,616 bytes are in use.]
;; Reading the file took 0.92 seconds
;; Checking the proof took 57.37 seconds
;; VERIFY took 83.89 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,251,912 bytes in use.  Commencing GC.]
; [GC completed with 41,423,288 bytes retained and 6,828,624 bytes freed.]
; [GC will next occur when at least 53,423,288 bytes are in use.]
;; Reading the file took 0.46 seconds
;; Checking the proof took 25.57 seconds
;; VERIFY took 37.34 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,437,608 bytes in use.  Commencing GC.]
; [GC completed with 40,635,240 bytes retained and 12,802,368 bytes freed.]
; [GC will next occur when at least 52,635,240 bytes are in use.]
; [GC threshold exceeded with 57,367,472 bytes in use.  Commencing GC.]
; [GC completed with 46,357,856 bytes retained and 11,009,616 bytes freed.]
; [GC will next occur when at least 58,357,856 bytes are in use.]
;; Reading the file took 1.17 seconds
;; Checking the proof took 17.47 seconds
;; VERIFY took 26.26 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.03 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.12 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.06 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.07 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.01 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,449,040 bytes in use.  Commencing GC.]
; [GC completed with 35,738,456 bytes retained and 22,710,584 bytes freed.]
; [GC will next occur when at least 47,738,456 bytes are in use.]
;; Reading the file took 0.24 seconds
;; Checking the proof took 13.40 seconds
;; VERIFY took 18.83 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,110,520 bytes in use.  Commencing GC.]
; [GC completed with 41,528,848 bytes retained and 6,581,672 bytes freed.]
; [GC will next occur when at least 53,528,848 bytes are in use.]
;; Reading the file took 0.60 seconds
;; Checking the proof took 34.07 seconds
;; VERIFY took 47.31 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,538,376 bytes in use.  Commencing GC.]
; [GC completed with 38,757,832 bytes retained and 14,780,544 bytes freed.]
; [GC will next occur when at least 50,757,832 bytes are in use.]
;; Reading the file took 0.22 seconds
;; Checking the proof took 21.23 seconds
;; VERIFY took 30.01 seconds
4312> DEFINE BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/admit-build.disjoined-commute-or.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.05 seconds
4313> VERIFY BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/thm-build.disjoined-commute-or.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 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,817,856 bytes in use.  Commencing GC.]
; [GC completed with 41,678,944 bytes retained and 10,138,912 bytes freed.]
; [GC will next occur when at least 53,678,944 bytes are in use.]
;; Reading the file took 0.29 seconds
;; Checking the proof took 18.41 seconds
;; VERIFY took 25.34 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,302,248 bytes in use.  Commencing GC.]
; [GC completed with 45,064,080 bytes retained and 10,238,168 bytes freed.]
; [GC will next occur when at least 57,064,080 bytes are in use.]
;; Reading the file took 0.38 seconds
;; Checking the proof took 74.38 seconds
;; VERIFY took 98.62 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,354,400 bytes in use.  Commencing GC.]
; [GC completed with 47,872,528 bytes retained and 10,481,872 bytes freed.]
; [GC will next occur when at least 59,872,528 bytes are in use.]
;; Reading the file took 0.31 seconds
;; Checking the proof took 22.40 seconds
;; VERIFY took 31.18 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.08 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.00 seconds
;; VERIFY took 0.05 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.18 seconds
;; Checking the proof took 2.36 seconds
;; VERIFY took 3.53 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.48 seconds
;; VERIFY took 0.66 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,882,432 bytes in use.  Commencing GC.]
; [GC completed with 1,771,368 bytes retained and 58,111,064 bytes freed.]
; [GC will next occur when at least 13,771,368 bytes are in use.]
;; Reading the file took 0.38 seconds
;; Checking the proof took 18.57 seconds
;; VERIFY took 27.23 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 13,782,320 bytes in use.  Commencing GC.]
; [GC completed with 5,099,688 bytes retained and 8,682,632 bytes freed.]
; [GC will next occur when at least 17,099,688 bytes are in use.]
;; Reading the file took 0.37 seconds
;; Checking the proof took 10.72 seconds
;; VERIFY took 15.74 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,109,696 bytes in use.  Commencing GC.]
; [GC completed with 5,110,256 bytes retained and 11,999,440 bytes freed.]
; [GC will next occur when at least 17,110,256 bytes are in use.]
; [GC threshold exceeded with 18,516,456 bytes in use.  Commencing GC.]
; [GC completed with 12,591,968 bytes retained and 5,924,488 bytes freed.]
; [GC will next occur when at least 24,591,968 bytes are in use.]
;; Reading the file took 0.67 seconds
;; Checking the proof took 5.03 seconds
;; VERIFY took 7.87 seconds
4325> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-1A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-1a.proofs
;; Reading the file took 0.09 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (B C X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.13 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.01 seconds
;; VERIFY took 0.02 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.01 seconds
;; Checking the proof took 0.03 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.17 seconds
;; Checking the proof took 9.87 seconds
;; VERIFY took 13.76 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 24,608,064 bytes in use.  Commencing GC.]
; [GC completed with 9,813,800 bytes retained and 14,794,264 bytes freed.]
; [GC will next occur when at least 21,813,800 bytes are in use.]
; [GC threshold exceeded with 25,864,864 bytes in use.  Commencing GC.]
; [GC completed with 17,346,648 bytes retained and 8,518,216 bytes freed.]
; [GC will next occur when at least 29,346,648 bytes are in use.]
;; Reading the file took 0.71 seconds
;; Checking the proof took 55.20 seconds
;; VERIFY took 76.20 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 29,802,088 bytes in use.  Commencing GC.]
; [GC completed with 6,417,752 bytes retained and 23,384,336 bytes freed.]
; [GC will next occur when at least 18,417,752 bytes are in use.]
;; Reading the file took 0.31 seconds
;; Checking the proof took 17.23 seconds
;; VERIFY took 24.46 seconds
4331> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-1.proofs
;; Reading the file took 0.06 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A B C D): 
; Compiling Top-Level Form: 
;; DEFINE took 0.10 seconds
4332> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 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.00 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.09 seconds
;; Checking the proof took 3.72 seconds
;; VERIFY took 5.09 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,432,760 bytes in use.  Commencing GC.]
; [GC completed with 10,645,256 bytes retained and 7,787,504 bytes freed.]
; [GC will next occur when at least 22,645,256 bytes are in use.]
;; 
; [GC threshold exceeded with 23,237,536 bytes in use.  Commencing GC.]
; [GC completed with 12,628,512 bytes retained and 10,609,024 bytes freed.]
; [GC will next occur when at least 24,628,512 bytes are in use.]
Reading the file took 0.52 seconds
;; Checking the proof took 17.26 seconds
;; VERIFY took 23.56 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.14 seconds
;; Checking the proof took 7.16 seconds
;; VERIFY took 10.09 seconds
4337> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-2a.proofs
;; Reading the file took 0.06 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (A D X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.11 seconds
4338> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2a.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 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
;; 
; [GC threshold exceeded with 24,888,936 bytes in use.  Commencing GC.]
; [GC completed with 14,135,048 bytes retained and 10,753,888 bytes freed.]
; [GC will next occur when at least 26,135,048 bytes are in use.]
Reading the file took 0.12 seconds
;; Checking the proof took 12.19 seconds
;; VERIFY took 17.23 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 27,385,584 bytes in use.  Commencing GC.]
; [GC completed with 10,954,944 bytes retained and 16,430,640 bytes freed.]
; [GC will next occur when at least 22,954,944 bytes are in use.]
;; Reading the file took 0.69 seconds
; [GC threshold exceeded with 22,968,824 bytes in use.  Commencing GC.]
; [GC completed with 16,221,656 bytes retained and 6,747,168 bytes freed.]
; [GC will next occur when at least 28,221,656 bytes are in use.]
;; Checking the proof took 37.28 seconds
;; VERIFY took 52.38 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.14 seconds
;; Checking the proof took 21.31 seconds
;; VERIFY took 30.51 seconds
4343> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-2
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-2.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.03 seconds
4344> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 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 28,441,936 bytes in use.  Commencing GC.]
; [GC completed with 17,938,568 bytes retained and 10,503,368 bytes freed.]
; [GC will next occur when at least 29,938,568 bytes are in use.]
;; Reading the file took 0.17 seconds
;; Checking the proof took 3.75 seconds
;; VERIFY took 5.21 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 31,913,928 bytes in use.  Commencing GC.]
; [GC completed with 24,514,368 bytes retained and 7,399,560 bytes freed.]
; [GC will next occur when at least 36,514,368 bytes are in use.]
;; Reading the file took 0.54 seconds
;; Checking the proof took 17.41 seconds
;; VERIFY took 23.76 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.17 seconds
;; Checking the proof took 7.22 seconds
;; VERIFY took 10.21 seconds
4349> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-3A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-3a.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
4350> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-3A
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-3a.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.03 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 36,522,600 bytes in use.  Commencing GC.]
; [GC completed with 16,877,176 bytes retained and 19,645,424 bytes freed.]
; [GC will next occur when at least 28,877,176 bytes are in use.]
;; Reading the file took 0.30 seconds
;; Checking the proof took 3.03 seconds
;; VERIFY took 4.28 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 29,128,360 bytes in use.  Commencing GC.]
; [GC completed with 21,204,104 bytes retained and 7,924,256 bytes freed.]
; [GC will next occur when at least 33,204,104 bytes are in use.]
;; Reading the file took 0.42 seconds
;; Checking the proof took 5.69 seconds
;; VERIFY took 7.88 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 33,328,928 bytes in use.  Commencing GC.]
; [GC completed with 20,926,336 bytes retained and 12,402,592 bytes freed.]
; [GC will next occur when at least 32,926,336 bytes are in use.]
;; Reading the file took 0.38 seconds
;; Checking the proof took 6.86 seconds
;; VERIFY took 9.90 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 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.11 seconds
;; Checking the proof took 2.92 seconds
;; VERIFY took 3.96 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 32,936,440 bytes in use.  Commencing GC.]
; [GC completed with 23,622,000 bytes retained and 9,314,440 bytes freed.]
; [GC will next occur when at least 35,622,000 bytes are in use.]
; [GC threshold exceeded with 37,585,832 bytes in use.  Commencing GC.]
; [GC completed with 23,006,648 bytes retained and 14,579,184 bytes freed.]
; [GC will next occur when at least 35,006,648 bytes are in use.]
;; Reading the file took 0.77 seconds
;; Checking the proof took 27.10 seconds
;; VERIFY took 37.09 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,029,352 bytes in use.  Commencing GC.]
; [GC completed with 28,975,760 bytes retained and 6,053,592 bytes freed.]
; [GC will next occur when at least 40,975,760 bytes are in use.]
;; Reading the file took 0.17 seconds
;; Checking the proof took 3.85 seconds
;; VERIFY took 5.28 seconds
4361> DEFINE BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.disjoined-right-associativity.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.09 seconds
4362> VERIFY BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.disjoined-right-associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.02 seconds
;; VERIFY took 0.03 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.09 seconds
;; Checking the proof took 5.57 seconds
;; VERIFY took 7.54 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 41,368,280 bytes in use.  Commencing GC.]
; [GC completed with 31,779,688 bytes retained and 9,588,592 bytes freed.]
; [GC will next occur when at least 43,779,688 bytes are in use.]
;; Reading the file took 
; [GC threshold exceeded with 44,227,992 bytes in use.  Commencing GC.]
; [GC completed with 36,105,808 bytes retained and 8,122,184 bytes freed.]
; [GC will next occur when at least 48,105,808 bytes are in use.]
0.59 seconds
;; Checking the proof took 69.61 seconds
;; VERIFY took 93.86 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.18 seconds
;; Checking the proof took 7.26 seconds
;; VERIFY took 10.06 seconds
4367> DEFINE BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/admit-build.disjoined-right-associativity-okp.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.14 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.01 seconds
;; VERIFY took 0.02 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,115,368 bytes in use.  Commencing GC.]
; [GC completed with 29,081,424 bytes retained and 19,033,944 bytes freed.]
; [GC will next occur when at least 41,081,424 bytes are in use.]
; [GC threshold exceeded with 44,260,360 bytes in use.  Commencing GC.]
; [GC completed with 36,438,312 bytes retained and 7,822,048 bytes freed.]
; [GC will next occur when at least 48,438,312 bytes are in use.]
;; Reading the file took 0.64 seconds
;; Checking the proof took 5.44 seconds
;; VERIFY took 8.51 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.05 seconds
;; Checking the proof took 0.79 seconds
;; VERIFY took 1.07 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,198,640 bytes in use.  Commencing GC.]
; [GC completed with 39,350,496 bytes retained and 10,848,144 bytes freed.]
; [GC will next occur when at least 51,350,496 bytes are in use.]
;; Reading the file took 0.49 seconds
;; Checking the proof took 39.46 seconds
;; VERIFY took 57.34 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 52,125,896 bytes in use.  Commencing GC.]
; [GC completed with 45,488,576 bytes retained and 6,637,320 bytes freed.]
; [GC will next occur when at least 57,488,576 bytes are in use.]
;; Reading the file took 0.37 seconds
;; Checking the proof took 21.53 seconds
;; VERIFY took 31.35 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 58,758,656 bytes in use.  Commencing GC.]
; [GC completed with 7,510,288 bytes retained and 51,248,368 bytes freed.]
; [GC will next occur when at least 19,510,288 bytes are in use.]
;; Reading the file took 0.82 seconds
; [GC threshold exceeded with 19,520,432 bytes in use.  Commencing GC.]
; [GC completed with 12,776,936 bytes retained and 6,743,496 bytes freed.]
; [GC will next occur when at least 24,776,936 bytes are in use.]
;; Checking the proof took 8.67 seconds
;; VERIFY took 13.12 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.06 seconds
4375> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-4
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-4.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 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.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 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.08 seconds
;; Checking the proof took 1.81 seconds
;; VERIFY took 2.50 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,050,424 bytes in use.  Commencing GC.]
; [GC completed with 17,616,192 bytes retained and 7,434,232 bytes freed.]
; [GC will next occur when at least 29,616,192 bytes are in use.]
;; Reading the file took 0.62 seconds
;; Checking the proof took 29.56 seconds
;; VERIFY took 40.14 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 29,732,320 bytes in use.  Commencing GC.]
; [GC completed with 22,157,720 bytes retained and 7,574,600 bytes freed.]
; [GC will next occur when at least 34,157,720 bytes are in use.]
;; Reading the file took 0.14 seconds
;; Checking the proof took 2.33 seconds
;; VERIFY took 3.27 seconds
4380> DEFINE BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.disjoined-associativity.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.05 seconds
4381> VERIFY BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.disjoined-associativity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
4382> VERIFY BUILD.DISJOINED-ASSOCIATIVITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-associativity-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.08 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.10 seconds
;; Checking the proof took 4.79 seconds
;; VERIFY took 6.63 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,168,848 bytes in use.  Commencing GC.]
; [GC completed with 24,990,088 bytes retained and 9,178,760 bytes freed.]
; [GC will next occur when at least 36,990,088 bytes are in use.]
; [GC threshold exceeded with 42,382,056 bytes in use.  Commencing GC.]
; [GC completed with 31,190,480 bytes retained and 11,191,576 bytes freed.]
; [GC will next occur when at least 43,190,480 bytes are in use.]
;; Reading the file took 0.75 seconds
;; Checking the proof took 40.60 seconds
;; VERIFY took 55.39 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.17 seconds
;; Checking the proof took 6.25 seconds
;; VERIFY took 8.74 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.05 seconds
4387> VERIFY BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-build.disjoined-associativity-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 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 44,742,872 bytes in use.  Commencing GC.]
; [GC completed with 16,411,640 bytes retained and 28,331,232 bytes freed.]
; [GC will next occur when at least 28,411,640 bytes are in use.]
;; Reading the file took 0.55 seconds
;; Checking the proof took 5.50 seconds
;; VERIFY took 8.47 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,420,184 bytes in use.  Commencing GC.]
; [GC completed with 17,146,576 bytes retained and 11,273,608 bytes freed.]
; [GC will next occur when at least 29,146,576 bytes are in use.]
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.81 seconds
;; VERIFY took 1.21 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,412,632 bytes in use.  Commencing GC.]
; [GC completed with 23,836,824 bytes retained and 6,575,808 bytes freed.]
; [GC will next occur when at least 35,836,824 bytes are in use.]
;; Reading the file took 0.51 seconds
;; Checking the proof took 39.75 seconds
;; VERIFY took 57.49 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,611,912 bytes in use.  Commencing GC.]
; [GC completed with 29,964,568 bytes retained and 6,647,344 bytes freed.]
; [GC will next occur when at least 41,964,568 bytes are in use.]
;; Reading the file took 0.42 seconds
;; Checking the proof took 21.73 seconds
;; VERIFY took 31.57 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,234,496 bytes in use.  Commencing GC.]
; [GC completed with 19,101,728 bytes retained and 24,132,768 bytes freed.]
; [GC will next occur when at least 31,101,728 bytes are in use.]
;; Reading the file took 0.75 seconds
; [GC threshold exceeded with 31,115,960 bytes in use.  Commencing GC.]
; [GC completed with 24,368,448 bytes retained and 6,747,512 bytes freed.]
; [GC will next occur when at least 36,368,448 bytes are in use.]
;; Checking the proof took 8.74 seconds
;; VERIFY took 13.13 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.08 seconds
4394> VERIFY BUILD.DISJOINED-CUT-LEMMA-1
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-1.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 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.16 seconds
;; Checking the proof took 4.36 seconds
;; VERIFY took 6.16 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,379,920 bytes in use.  Commencing GC.]
; [GC completed with 28,478,136 bytes retained and 7,901,784 bytes freed.]
; [GC will next occur when at least 40,478,136 bytes are in use.]
; [GC threshold exceeded with 45,817,376 bytes in use.  Commencing GC.]
; [GC completed with 35,677,168 bytes retained and 10,140,208 bytes freed.]
; [GC will next occur when at least 47,677,168 bytes are in use.]
;; Reading the file took 0.87 seconds
;; Checking the proof took 31.11 seconds
;; VERIFY took 44.95 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 49,201,736 bytes in use.  Commencing GC.]
; [GC completed with 35,614,368 bytes retained and 13,587,368 bytes freed.]
; [GC will next occur when at least 47,614,368 bytes are in use.]
;; Reading the file took 0.64 seconds
;; Checking the proof took 64.37 seconds
;; VERIFY took 92.18 seconds
4399> DEFINE BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/admit-build.disjoined-cut-lemma-2.proofs
;; Reading the file took 0.03 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.03 seconds
4400> VERIFY BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-2.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 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.17 seconds
;; Checking the proof took 1.53 seconds
;; VERIFY took 2.31 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 47,622,848 bytes in use.  Commencing GC.]
; [GC completed with 39,737,768 bytes retained and 7,885,080 bytes freed.]
; [GC will next occur when at least 51,737,768 bytes are in use.]
; [GC threshold exceeded with 52,779,128 bytes in use.  Commencing GC.]
; [GC completed with 33,025,624 bytes retained and 19,753,504 bytes freed.]
; [GC will next occur when at least 45,025,624 bytes are in use.]
;; Reading the file took 0.83 seconds
;; Checking the proof took 64.20 seconds
;; VERIFY took 90.94 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.24 seconds
;; Checking the proof took 2.00 seconds
;; VERIFY took 3.04 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.06 seconds
4406> VERIFY BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/thm-build.disjoined-cut.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4407> VERIFY BUILD.DISJOINED-CUT-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-cut-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 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,036,304 bytes in use.  Commencing GC.]
; [GC completed with 38,955,280 bytes retained and 6,081,024 bytes freed.]
; [GC will next occur when at least 50,955,280 bytes are in use.]
;; Reading the file took 0.27 seconds
;; Checking the proof took 5.23 seconds
;; VERIFY took 7.54 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 52,417,248 bytes in use.  Commencing GC.]
; [GC completed with 41,546,232 bytes retained and 10,871,016 bytes freed.]
; [GC will next occur when at least 53,546,232 bytes are in use.]
; [GC threshold exceeded with 55,326,224 bytes in use.  Commencing GC.]
; [GC completed with 47,142,888 bytes retained and 8,183,336 bytes freed.]
; [GC will next occur when at least 59,142,888 bytes are in use.]
; [GC threshold exceeded with 63,791,272 bytes in use.  Commencing GC.]
; [GC completed with 38,170,168 bytes retained and 25,621,104 bytes freed.]
; [GC will next occur when at least 50,170,168 bytes are in use.]
;; Reading the file took 1.40 seconds
;; Checking the proof took 75.07 seconds
;; VERIFY took 107.14 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 52,674,488 bytes in use.  Commencing GC.]
; [GC completed with 44,071,000 bytes retained and 8,603,488 bytes freed.]
; [GC will next occur when at least 56,071,000 bytes are in use.]
;; Reading the file took 0.40 seconds
;; Checking the proof took 7.80 seconds
;; VERIFY took 11.29 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.05 seconds
4412> VERIFY BUILD.DISJOINED-CUT-OKP
;; Reading from Proofs/level2/thm-build.disjoined-cut-okp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 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 56,999,320 bytes in use.  Commencing GC.]
; [GC completed with 43,592,920 bytes retained and 13,406,400 bytes freed.]
; [GC will next occur when at least 55,592,920 bytes are in use.]
;; Reading the file took 0.56 seconds
; [GC threshold exceeded with 56,255,624 bytes in use.  Commencing GC.]
; [GC completed with 48,859,584 bytes retained and 7,396,040 bytes freed.]
; [GC will next occur when at least 60,859,584 bytes are in use.]
;; Checking the proof took 9.37 seconds
;; VERIFY took 14.01 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.04 seconds
;; Checking the proof took 1.11 seconds
;; VERIFY took 1.40 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,297,112 bytes in use.  Commencing GC.]
; [GC completed with 55,883,944 bytes retained and 6,413,168 bytes freed.]
; [GC will next occur when at least 67,883,944 bytes are in use.]
;; Reading the file took 0.74 seconds
; [GC threshold exceeded with 67,893,792 bytes in use.  Commencing GC.]
; [GC completed with 61,150,760 bytes retained and 6,743,032 bytes freed.]
; [GC will next occur when at least 73,150,760 bytes are in use.]
;; Checking the proof took 88.50 seconds
;; VERIFY took 126.23 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,244,416 bytes in use.  Commencing GC.]
; [GC completed with 45,243,736 bytes retained and 29,000,680 bytes freed.]
; [GC will next occur when at least 57,243,736 bytes are in use.]
;; Reading the file took 0.51 seconds
;; Checking the proof took 38.46 seconds
;; VERIFY took 54.84 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,258,608 bytes in use.  Commencing GC.]
; [GC completed with 53,186,944 bytes retained and 4,071,664 bytes freed.]
; [GC will next occur when at least 65,186,944 bytes are in use.]
; [GC threshold exceeded with 67,006,272 bytes in use.  Commencing GC.]
; [GC completed with 58,137,776 bytes retained and 8,868,496 bytes freed.]
; [GC will next occur when at least 70,137,776 bytes are in use.]
; [GC threshold exceeded with 74,786,160 bytes in use.  Commencing GC.]
; [GC completed with 66,027,408 bytes retained and 8,758,752 bytes freed.]
; [GC will next occur when at least 78,027,408 bytes are in use.]
;; Reading the file took 1.57 seconds
; [GC threshold exceeded with 78,038,720 bytes in use.  Commencing GC.]
; [GC completed with 31,661,640 bytes retained and 46,377,080 bytes freed.]
; [GC will next occur when at least 43,661,640 bytes are in use.]
;; Checking the proof took 27.06 seconds
;; VERIFY took 40.14 seconds
4418> DEFINE BUILD.DISJOINED-MODUS-PONENS
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.01 seconds
4419> VERIFY BUILD.DISJOINED-MODUS-PONENS
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.08 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 44,793,512 bytes in use.  Commencing GC.]
; [GC completed with 36,958,288 bytes retained and 7,835,224 bytes freed.]
; [GC will next occur when at least 48,958,288 bytes are in use.]
;; Reading the file took 0.33 seconds
;; Checking the proof took 41.74 seconds
;; VERIFY took 57.95 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 48,970,720 bytes in use.  Commencing GC.]
; [GC completed with 36,018,464 bytes retained and 12,952,256 bytes freed.]
; [GC will next occur when at least 48,018,464 bytes are in use.]
; [GC threshold exceeded with 49,453,752 bytes in use.  Commencing GC.]
; [GC completed with 41,192,424 bytes retained and 8,261,328 bytes freed.]
; [GC will next occur when at least 53,192,424 bytes are in use.]
; [GC threshold exceeded with 60,177,056 bytes in use.  Commencing GC.]
; [GC completed with 47,471,176 bytes retained and 12,705,880 bytes freed.]
; [GC will next occur when at least 59,471,176 bytes are in use.]
;; Reading the file took 1.74 seconds
; [GC threshold exceeded with 59,486,504 bytes in use.  Commencing GC.]
; [GC completed with 59,308,480 bytes retained and 178,024 bytes freed.]
; [GC will next occur when at least 71,308,480 bytes are in use.]
;; Checking the proof took 97.65 seconds
;; VERIFY took 137.67 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,337,648 bytes in use.  Commencing GC.]
; [GC completed with 64,206,784 bytes retained and 8,130,864 bytes freed.]
; [GC will next occur when at least 76,206,784 bytes are in use.]
;; Reading the file took 0.43 seconds
;; Checking the proof took 86.29 seconds
;; VERIFY took 120.73 seconds
4424> DEFINE BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-okp.proofs
; [GC threshold exceeded with 76,250,768 bytes in use.  Commencing GC.]
; [GC completed with 67,886,304 bytes retained and 8,364,464 bytes freed.]
; [GC will next occur when at least 79,886,304 bytes are in use.]
;; 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.07 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.01 seconds
;; VERIFY took 0.02 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 81,916,072 bytes in use.  Commencing GC.]
; [GC completed with 37,976,208 bytes retained and 43,939,864 bytes freed.]
; [GC will next occur when at least 49,976,208 bytes are in use.]
;; Reading the file took 0.36 seconds
;; Checking the proof took 4.88 seconds
;; VERIFY took 7.17 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.03 seconds
;; Checking the proof took 0.80 seconds
;; VERIFY took 1.01 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 52,822,008 bytes in use.  Commencing GC.]
; [GC completed with 44,986,288 bytes retained and 7,835,720 bytes freed.]
; [GC will next occur when at least 56,986,288 bytes are in use.]
;; Reading the file took 0.76 seconds
;; Checking the proof took 53.75 seconds
;; VERIFY took 76.48 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,783,064 bytes in use.  Commencing GC.]
; [GC completed with 42,972,344 bytes retained and 14,810,720 bytes freed.]
; [GC will next occur when at least 54,972,344 bytes are in use.]
;; Reading the file took 0.31 seconds
;; Checking the proof took 23.57 seconds
;; VERIFY took 33.29 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,984,776 bytes in use.  Commencing GC.]
; [GC completed with 49,635,112 bytes retained and 5,349,664 bytes freed.]
; [GC will next occur when at least 61,635,112 bytes are in use.]
; [GC threshold exceeded with 65,566,848 bytes in use.  Commencing GC.]
; [GC completed with 55,263,848 bytes retained and 10,303,000 bytes freed.]
; [GC will next occur when at least 67,263,848 bytes are in use.]
; [GC threshold exceeded with 80,234,920 bytes in use.  Commencing GC.]
; [GC completed with 67,095,808 bytes retained and 13,139,112 bytes freed.]
; [GC will next occur when at least 79,095,808 bytes are in use.]
;; Reading the file took 1.34 seconds
;; Checking the proof took 20.74 seconds
;; VERIFY took 30.47 seconds
4431> DEFINE BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-2.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X Y): 
; Compiling Top-Level Form: 
;; DEFINE took 0.02 seconds
4432> VERIFY BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.08 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 79,904,144 bytes in use.  Commencing GC.]
; [GC completed with 18,226,392 bytes retained and 61,677,752 bytes freed.]
; [GC will next occur when at least 30,226,392 bytes are in use.]
;; Reading the file took 0.49 seconds
;; Checking the proof took 38.10 seconds
;; VERIFY took 52.91 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 30,239,736 bytes in use.  Commencing GC.]
; [GC completed with 24,819,160 bytes retained and 5,420,576 bytes freed.]
; [GC will next occur when at least 36,819,160 bytes are in use.]
; [GC threshold exceeded with 38,061,176 bytes in use.  Commencing GC.]
; [GC completed with 29,869,272 bytes retained and 8,191,904 bytes freed.]
; [GC will next occur when at least 41,869,272 bytes are in use.]
; [GC threshold exceeded with 48,853,904 bytes in use.  Commencing GC.]
; [GC completed with 37,758,920 bytes retained and 11,094,984 bytes freed.]
; [GC will next occur when at least 49,758,920 bytes are in use.]
;; Reading the file took 1.87 seconds
; [GC threshold exceeded with 49,774,256 bytes in use.  Commencing GC.]
; [GC completed with 41,706,464 bytes retained and 8,067,792 bytes freed.]
; [GC will next occur when at least 53,706,464 bytes are in use.]
;; Checking the proof took 93.56 seconds
;; VERIFY took 131.83 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 54,540,664 bytes in use.  Commencing GC.]
; [GC completed with 46,638,712 bytes retained and 7,901,952 bytes freed.]
; [GC will next occur when at least 58,638,712 bytes are in use.]
;; Reading the file took 0.38 seconds
;; Checking the proof took 78.37 seconds
;; VERIFY took 109.46 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.01 seconds
;; Checking the proofs took 0.00 seconds
; [GC threshold exceeded with 58,653,104 bytes in use.  Commencing GC.]
; [GC completed with 21,077,760 bytes retained and 37,575,344 bytes freed.]
; [GC will next occur when at least 33,077,760 bytes are in use.]
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.09 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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 34,689,776 bytes in use.  Commencing GC.]
; [GC completed with 27,610,736 bytes retained and 7,079,040 bytes freed.]
; [GC will next occur when at least 39,610,736 bytes are in use.]
;; Reading the file took 0.35 seconds
;; Checking the proof took 4.81 seconds
;; VERIFY took 7.06 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.04 seconds
;; Checking the proof took 0.79 seconds
;; VERIFY took 1.01 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 40,120,208 bytes in use.  Commencing GC.]
; [GC completed with 27,962,560 bytes retained and 12,157,648 bytes freed.]
; [GC will next occur when at least 39,962,560 bytes are in use.]
;; Reading the file took 0.46 seconds
;; Checking the proof took 53.61 seconds
;; VERIFY took 75.89 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 39,974,808 bytes in use.  Commencing GC.]
; [GC completed with 34,732,664 bytes retained and 5,242,144 bytes freed.]
; [GC will next occur when at least 46,732,664 bytes are in use.]
;; Reading the file took 0.40 seconds
;; Checking the proof took 27.11 seconds
;; VERIFY took 38.32 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 46,743,976 bytes in use.  Commencing GC.]
; [GC completed with 23,913,864 bytes retained and 22,830,112 bytes freed.]
; [GC will next occur when at least 35,913,864 bytes are in use.]
; [GC threshold exceeded with 37,199,192 bytes in use.  Commencing GC.]
; [GC completed with 28,919,872 bytes retained and 8,279,320 bytes freed.]
; [GC will next occur when at least 40,919,872 bytes are in use.]
; [GC threshold exceeded with 47,904,504 bytes in use.  Commencing GC.]
; [GC completed with 35,185,696 bytes retained and 12,718,808 bytes freed.]
; [GC will next occur when at least 47,185,696 bytes are in use.]
;; Reading the file took 1.39 seconds
; [GC threshold exceeded with 47,197,008 bytes in use.  Commencing GC.]
; [GC completed with 47,031,136 bytes retained and 165,872 bytes freed.]
; [GC will next occur when at least 59,031,136 bytes are in use.]
;; Checking the proof took 20.98 seconds
;; VERIFY took 30.90 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 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.12 seconds
;; Checking the proof took 1.76 seconds
;; VERIFY took 2.41 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 59,599,896 bytes in use.  Commencing GC.]
; [GC completed with 51,458,016 bytes retained and 8,141,880 bytes freed.]
; [GC will next occur when at least 63,458,016 bytes are in use.]
;; Reading the file took 0.33 seconds
;; Checking the proof took 15.35 seconds
;; VERIFY took 20.23 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.07 seconds
;; Checking the proof took 2.39 seconds
;; VERIFY took 3.22 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.03 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.05 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.04 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 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 63,467,688 bytes in use.  Commencing GC.]
; [GC completed with 54,868,904 bytes retained and 8,598,784 bytes freed.]
; [GC will next occur when at least 66,868,904 bytes are in use.]
;; Reading the file took 0.23 seconds
;; Checking the proof took 2.51 seconds
;; VERIFY took 3.73 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.03 seconds
;; Checking the proof took 0.53 seconds
;; VERIFY took 0.67 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 67,601,696 bytes in use.  Commencing GC.]
; [GC completed with 31,608,816 bytes retained and 35,992,880 bytes freed.]
; [GC will next occur when at least 43,608,816 bytes are in use.]
;; Reading the file took 0.41 seconds
;; Checking the proof took 19.86 seconds
;; VERIFY took 28.48 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 44,679,328 bytes in use.  Commencing GC.]
; [GC completed with 38,862,672 bytes retained and 5,816,656 bytes freed.]
; [GC will next occur when at least 50,862,672 bytes are in use.]
;; Reading the file took 0.26 seconds
;; Checking the proof took 11.45 seconds
;; VERIFY took 16.42 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 50,990,472 bytes in use.  Commencing GC.]
; [GC completed with 38,335,680 bytes retained and 12,654,792 bytes freed.]
; [GC will next occur when at least 50,335,680 bytes are in use.]
;; Reading the file took 0.50 seconds
;; Checking the proof took 5.35 seconds
;; VERIFY took 8.02 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.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 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 50,367,408 bytes in use.  Commencing GC.]
; [GC completed with 42,464,864 bytes retained and 7,902,544 bytes freed.]
; [GC will next occur when at least 54,464,864 bytes are in use.]
;; Reading the file took 0.13 seconds
;; Checking the proof took 1.73 seconds
;; VERIFY took 2.39 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 55,412,360 bytes in use.  Commencing GC.]
; [GC completed with 32,718,152 bytes retained and 22,694,208 bytes freed.]
; [GC will next occur when at least 44,718,152 bytes are in use.]
;; Reading the file took 0.43 seconds
;; Checking the proof took 15.21 seconds
;; VERIFY took 20.11 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.08 seconds
;; Checking the proof took 2.37 seconds
;; VERIFY took 3.21 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.03 seconds
4464> VERIFY RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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 45,630,640 bytes in use.  Commencing GC.]
; [GC completed with 36,064,936 bytes retained and 9,565,704 bytes freed.]
; [GC will next occur when at least 48,064,936 bytes are in use.]
;; Reading the file took 0.23 seconds
;; Checking the proof took 2.55 seconds
;; VERIFY took 3.76 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.04 seconds
;; Checking the proof took 0.53 seconds
;; VERIFY took 0.68 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 48,932,240 bytes in use.  Commencing GC.]
; [GC completed with 38,785,776 bytes retained and 10,146,464 bytes freed.]
; [GC will next occur when at least 50,785,776 bytes are in use.]
;; Reading the file took 0.30 seconds
;; Checking the proof took 19.92 seconds
;; VERIFY took 28.38 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.26 seconds
; [GC threshold exceeded with 50,829,624 bytes in use.  Commencing GC.]
; [GC completed with 44,200,056 bytes retained and 6,629,568 bytes freed.]
; [GC will next occur when at least 56,200,056 bytes are in use.]
;; Checking the proof took 11.51 seconds
;; VERIFY took 16.42 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 58,507,736 bytes in use.  Commencing GC.]
; [GC completed with 45,702,928 bytes retained and 12,804,808 bytes freed.]
; [GC will next occur when at least 57,702,928 bytes are in use.]
;; Reading the file took 0.52 seconds
;; Checking the proof took 5.39 seconds
;; VERIFY took 8.06 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.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 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.15 seconds
;; Checking the proof took 13.83 seconds
;; VERIFY took 18.45 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 59,625,480 bytes in use.  Commencing GC.]
; [GC completed with 52,315,120 bytes retained and 7,310,360 bytes freed.]
; [GC will next occur when at least 64,315,120 bytes are in use.]
; [GC threshold exceeded with 66,416,496 bytes in use.  Commencing GC.]
; [GC completed with 40,953,448 bytes retained and 25,463,048 bytes freed.]
; [GC will next occur when at least 52,953,448 bytes are in use.]
;; Reading the file took 0.76 seconds
; [GC threshold exceeded with 52,964,128 bytes in use.  Commencing GC.]
; [GC completed with 46,220,120 bytes retained and 6,744,008 bytes freed.]
; [GC will next occur when at least 58,220,120 bytes are in use.]
;; Checking the proof took 113.03 seconds
;; VERIFY took 150.42 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.18 seconds
;; Checking the proof took 21.74 seconds
;; VERIFY took 29.19 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 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.10 seconds
;; Checking the proof took 8.52 seconds
;; VERIFY took 11.34 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 58,267,568 bytes in use.  Commencing GC.]
; [GC completed with 46,286,352 bytes retained and 11,981,216 bytes freed.]
; [GC will next occur when at least 58,286,352 bytes are in use.]
; [GC threshold exceeded with 59,477,808 bytes in use.  Commencing GC.]
; [GC completed with 52,703,984 bytes retained and 6,773,824 bytes freed.]
; [GC will next occur when at least 64,703,984 bytes are in use.]
;; Reading the file took 0.71 seconds
; [GC threshold exceeded with 64,718,024 bytes in use.  Commencing GC.]
; [GC completed with 25,281,424 bytes retained and 39,436,600 bytes freed.]
; [GC will next occur when at least 37,281,424 bytes are in use.]
;; Checking the proof took 122.39 seconds
;; VERIFY took 162.87 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.13 seconds
; [GC threshold exceeded with 37,293,792 bytes in use.  Commencing GC.]
; [GC completed with 27,032,624 bytes retained and 10,261,168 bytes freed.]
; [GC will next occur when at least 39,032,624 bytes are in use.]
;; Checking the proof took 11.58 seconds
;; VERIFY took 15.56 seconds
4482> DEFINE RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-bldr-okp.proofs
;; Reading the file took 0.09 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.12 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.01 seconds
;; VERIFY took 0.02 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 39,823,464 bytes in use.  Commencing GC.]
; [GC completed with 30,784,240 bytes retained and 9,039,224 bytes freed.]
; [GC will next occur when at least 42,784,240 bytes are in use.]
;; Reading the file took 0.40 seconds
;; Checking the proof took 5.71 seconds
;; VERIFY took 8.47 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.04 seconds
;; Checking the proof took 0.82 seconds
;; VERIFY took 1.04 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 42,796,112 bytes in use.  Commencing GC.]
; [GC completed with 37,722,896 bytes retained and 5,073,216 bytes freed.]
; [GC will next occur when at least 49,722,896 bytes are in use.]
;; Reading the file took 0.37 seconds
;; Checking the proof took 40.97 seconds
;; VERIFY took 58.29 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,467,824 bytes in use.  Commencing GC.]
; [GC completed with 37,568,232 bytes retained and 12,899,592 bytes freed.]
; [GC will next occur when at least 49,568,232 bytes are in use.]
;; Reading the file took 0.31 seconds
;; Checking the proof took 22.49 seconds
;; VERIFY took 32.07 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 49,854,208 bytes in use.  Commencing GC.]
; [GC completed with 41,029,056 bytes retained and 8,825,152 bytes freed.]
; [GC will next occur when at least 53,029,056 bytes are in use.]
; [GC threshold exceeded with 55,463,616 bytes in use.  Commencing GC.]
; [GC completed with 33,820,016 bytes retained and 21,643,600 bytes freed.]
; [GC will next occur when at least 45,820,016 bytes are in use.]
;; Reading the file took 0.74 seconds
;; Checking the proof took 9.00 seconds
;; VERIFY took 13.29 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.00 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.05 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.08 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.16 seconds
; [GC threshold exceeded with 45,834,680 bytes in use.  Commencing GC.]
; [GC completed with 41,027,056 bytes retained and 4,807,624 bytes freed.]
; [GC will next occur when at least 53,027,056 bytes are in use.]
;; Checking the proof took 34.65 seconds
;; VERIFY took 47.06 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 53,222,360 bytes in use.  Commencing GC.]
; [GC completed with 44,718,160 bytes retained and 8,504,200 bytes freed.]
; [GC will next occur when at least 56,718,160 bytes are in use.]
; [GC threshold exceeded with 59,106,232 bytes in use.  Commencing GC.]
; [GC completed with 49,979,640 bytes retained and 9,126,592 bytes freed.]
; [GC will next occur when at least 61,979,640 bytes are in use.]
;; Reading the file took 0.78 seconds
;; Checking the proof took 75.39 seconds
;; VERIFY took 104.62 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 63,669,912 bytes in use.  Commencing GC.]
; [GC completed with 30,751,264 bytes retained and 32,918,648 bytes freed.]
; [GC will next occur when at least 42,751,264 bytes are in use.]
;; Reading the file took 0.44 seconds
; [GC threshold exceeded with 42,760,120 bytes in use.  Commencing GC.]
; [GC completed with 34,265,800 bytes retained and 8,494,320 bytes freed.]
; [GC will next occur when at least 46,265,800 bytes are in use.]
;; Checking the proof took 185.46 seconds
;; VERIFY took 252.96 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.00 seconds
;; VERIFY took 0.02 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.06 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 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 47,737,264 bytes in use.  Commencing GC.]
; [GC completed with 39,667,128 bytes retained and 8,070,136 bytes freed.]
; [GC will next occur when at least 51,667,128 bytes are in use.]
;; Reading the file took 0.29 seconds
;; Checking the proof took 12.01 seconds
;; VERIFY took 16.29 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 53,489,792 bytes in use.  Commencing GC.]
; [GC completed with 47,570,624 bytes retained and 5,919,168 bytes freed.]
; [GC will next occur when at least 59,570,624 bytes are in use.]
;; Reading the file took 0.43 seconds
;; Checking the proof took 18.19 seconds
;; VERIFY took 25.05 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 59,585,032 bytes in use.  Commencing GC.]
; [GC completed with 45,510,584 bytes retained and 14,074,448 bytes freed.]
; [GC will next occur when at least 57,510,584 bytes are in use.]
;; Reading the file took 0.42 seconds
; [GC threshold exceeded with 57,521,768 bytes in use.  Commencing GC.]
; [GC completed with 49,352,352 bytes retained and 8,169,416 bytes freed.]
; [GC will next occur when at least 61,352,352 bytes are in use.]
;; Checking the proof took 99.41 seconds
;; VERIFY took 135.56 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.04 seconds
4502> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-OKP
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 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 61,483,304 bytes in use.  Commencing GC.]
; [GC completed with 38,145,168 bytes retained and 23,338,136 bytes freed.]
; [GC will next occur when at least 50,145,168 bytes are in use.]
;; Reading the file took 0.41 seconds
;; Checking the proof took 4.59 seconds
;; VERIFY took 6.82 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.04 seconds
;; Checking the proof took 0.74 seconds
;; VERIFY took 0.94 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 50,155,736 bytes in use.  Commencing GC.]
; [GC completed with 43,832,488 bytes retained and 6,323,248 bytes freed.]
; [GC will next occur when at least 55,832,488 bytes are in use.]
;; Reading the file took 0.32 seconds
;; Checking the proof took 40.70 seconds
;; VERIFY took 57.51 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 56,407,824 bytes in use.  Commencing GC.]
; [GC completed with 43,685,992 bytes retained and 12,721,832 bytes freed.]
; [GC will next occur when at least 55,685,992 bytes are in use.]
;; Reading the file took 0.37 seconds
;; Checking the proof took 28.13 seconds
;; VERIFY took 39.82 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 56,083,880 bytes in use.  Commencing GC.]
; [GC completed with 46,973,456 bytes retained and 9,110,424 bytes freed.]
; [GC will next occur when at least 58,973,456 bytes are in use.]
; [GC threshold exceeded with 62,681,944 bytes in use.  Commencing GC.]
; [GC completed with 9,449,880 bytes retained and 53,232,064 bytes freed.]
; [GC will next occur when at least 21,449,880 bytes are in use.]
;; Reading the file took 1.05 seconds
; [GC threshold exceeded with 22,599,208 bytes in use.  Commencing GC.]
; [GC completed with 17,344,744 bytes retained and 5,254,464 bytes freed.]
; [GC will next occur when at least 29,344,744 bytes are in use.]
;; Checking the proof took 13.42 seconds
;; VERIFY took 19.87 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.00 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.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 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.09 seconds
;; Checking the proof took 3.37 seconds
;; VERIFY took 4.64 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 29,361,088 bytes in use.  Commencing GC.]
; [GC completed with 21,579,192 bytes retained and 7,781,896 bytes freed.]
; [GC will next occur when at least 33,579,192 bytes are in use.]
; [GC threshold exceeded with 39,524,480 bytes in use.  Commencing GC.]
; [GC completed with 28,292,584 bytes retained and 11,231,896 bytes freed.]
; [GC will next occur when at least 40,292,584 bytes are in use.]
;; Reading the file took 0.76 seconds
;; Checking the proof took 30.82 seconds
;; VERIFY took 42.01 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.12 seconds
;; Checking the proof took 5.66 seconds
;; VERIFY took 7.90 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 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.18 seconds
;; Checking the proof took 10.59 seconds
;; VERIFY took 14.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 40,339,072 bytes in use.  Commencing GC.]
; [GC completed with 17,426,640 bytes retained and 22,912,432 bytes freed.]
; [GC will next occur when at least 29,426,640 bytes are in use.]
; [GC threshold exceeded with 30,638,944 bytes in use.  Commencing GC.]
; [GC completed with 23,938,696 bytes retained and 6,700,248 bytes freed.]
; [GC will next occur when at least 35,938,696 bytes are in use.]
;; Reading the file took 0.76 seconds
; [GC threshold exceeded with 35,948,528 bytes in use.  Commencing GC.]
; [GC completed with 27,356,256 bytes retained and 8,592,272 bytes freed.]
; [GC will next occur when at least 39,356,256 bytes are in use.]
;; Checking the proof took 103.77 seconds
;; VERIFY took 141.16 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 39,799,208 bytes in use.  Commencing GC.]
; [GC completed with 31,980,744 bytes retained and 7,818,464 bytes freed.]
; [GC will next occur when at least 43,980,744 bytes are in use.]
;; Reading the file took 0.53 seconds
; [GC threshold exceeded with 43,994,904 bytes in use.  Commencing GC.]
; [GC completed with 24,632,952 bytes retained and 19,361,952 bytes freed.]
; [GC will next occur when at least 36,632,952 bytes are in use.]
;; Checking the proof took 124.39 seconds
;; VERIFY took 170.68 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.01 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 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.14 seconds
;; Checking the proof took 13.42 seconds
;; VERIFY took 18.37 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 38,793,064 bytes in use.  Commencing GC.]
; [GC completed with 27,794,568 bytes retained and 10,998,496 bytes freed.]
; [GC will next occur when at least 39,794,568 bytes are in use.]
; [GC threshold exceeded with 41,366,440 bytes in use.  Commencing GC.]
; [GC completed with 32,796,320 bytes retained and 8,570,120 bytes freed.]
; [GC will next occur when at least 44,796,320 bytes are in use.]
;; Reading the file took 0.60 seconds
;; Checking the proof took 40.45 seconds
;; VERIFY took 55.30 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,580,688 bytes in use.  Commencing GC.]
; [GC completed with 40,164,208 bytes retained and 5,416,480 bytes freed.]
; [GC will next occur when at least 52,164,208 bytes are in use.]
;; Reading the file took 0.22 seconds
;; Checking the proof took 23.26 seconds
;; VERIFY took 32.39 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.01 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 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.41 seconds
;; Checking the proof took 10.73 seconds
;; VERIFY took 14.50 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 52,172,968 bytes in use.  Commencing GC.]
; [GC completed with 41,679,280 bytes retained and 10,493,688 bytes freed.]
; [GC will next occur when at least 53,679,280 bytes are in use.]
;; Reading the file took 0.53 seconds
; [GC threshold exceeded with 53,691,216 bytes in use.  Commencing GC.]
; [GC completed with 45,773,936 bytes retained and 7,917,280 bytes freed.]
; [GC will next occur when at least 57,773,936 bytes are in use.]
;; Checking the proof took 124.68 seconds
;; VERIFY took 165.31 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 58,238,616 bytes in use.  Commencing GC.]
; [GC completed with 26,670,128 bytes retained and 31,568,488 bytes freed.]
; [GC will next occur when at least 38,670,128 bytes are in use.]
;; Reading the file took 0.24 seconds
;; Checking the proof took 16.04 seconds
;; VERIFY took 21.81 seconds
4532> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2.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.02 seconds
4533> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 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.04 seconds
;; VERIFY took 0.06 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 40,899,824 bytes in use.  Commencing GC.]
; [GC completed with 32,440,344 bytes retained and 8,459,480 bytes freed.]
; [GC will next occur when at least 44,440,344 bytes are in use.]
;; Reading the file took 0.29 seconds
;; Checking the proof took 20.60 seconds
;; VERIFY took 27.19 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 45,854,536 bytes in use.  Commencing GC.]
; [GC completed with 32,551,064 bytes retained and 13,303,472 bytes freed.]
; [GC will next occur when at least 44,551,064 bytes are in use.]
;; Reading the file took 0.68 seconds
; [GC threshold exceeded with 44,565,048 bytes in use.  Commencing GC.]
; [GC completed with 37,817,736 bytes retained and 6,747,312 bytes freed.]
; [GC will next occur when at least 49,817,736 bytes are in use.]
;; Checking the proof took 28.00 seconds
;; VERIFY took 37.67 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 51,728,520 bytes in use.  Commencing GC.]
; [GC completed with 44,384,720 bytes retained and 7,343,800 bytes freed.]
; [GC will next occur when at least 56,384,720 bytes are in use.]
;; Reading the file took 0.70 seconds
; [GC threshold exceeded with 56,398,632 bytes in use.  Commencing GC.]
; [GC completed with 49,651,432 bytes retained and 6,747,200 bytes freed.]
; [GC will next occur when at least 61,651,432 bytes are in use.]
;; Checking the proof took 109.93 seconds
;; VERIFY took 148.38 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.03 seconds
4539> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-OKP
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-okp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 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 62,182,528 bytes in use.  Commencing GC.]
; [GC completed with 21,007,536 bytes retained and 41,174,992 bytes freed.]
; [GC will next occur when at least 33,007,536 bytes are in use.]
;; Reading the file took 0.51 seconds
;; Checking the proof took 5.83 seconds
;; VERIFY took 8.71 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 33,015,944 bytes in use.  Commencing GC.]
; [GC completed with 21,742,048 bytes retained and 11,273,896 bytes freed.]
; [GC will next occur when at least 33,742,048 bytes are in use.]
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.84 seconds
;; VERIFY took 1.09 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 35,007,968 bytes in use.  Commencing GC.]
; [GC completed with 28,952,728 bytes retained and 6,055,240 bytes freed.]
; [GC will next occur when at least 40,952,728 bytes are in use.]
;; Reading the file took 0.39 seconds
;; Checking the proof took 41.74 seconds
;; VERIFY took 58.93 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 41,717,104 bytes in use.  Commencing GC.]
; [GC completed with 35,054,456 bytes retained and 6,662,648 bytes freed.]
; [GC will next occur when at least 47,054,456 bytes are in use.]
;; Reading the file took 0.34 seconds
;; Checking the proof took 22.94 seconds
;; VERIFY took 32.47 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 48,324,040 bytes in use.  Commencing GC.]
; [GC completed with 35,206,424 bytes retained and 13,117,616 bytes freed.]
; [GC will next occur when at least 47,206,424 bytes are in use.]
;; Reading the file took 0.64 seconds
; [GC threshold exceeded with 47,216,784 bytes in use.  Commencing GC.]
; [GC completed with 40,473,136 bytes retained and 6,743,648 bytes freed.]
; [GC will next occur when at least 52,473,136 bytes are in use.]
;; Checking the proof took 9.19 seconds
;; VERIFY took 13.38 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.01 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X): 
; Compiling Top-Level Form: 
;; DEFINE took 0.02 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.00 seconds
;; Checking the proof took 0.01 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.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 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.09 seconds
;; Checking the proof took 2.55 seconds
;; VERIFY took 3.39 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 52,888,032 bytes in use.  Commencing GC.]
; [GC completed with 26,244,944 bytes retained and 26,643,088 bytes freed.]
; [GC will next occur when at least 38,244,944 bytes are in use.]
;; Reading the file took 0.53 seconds
;; Checking the proof took 22.92 seconds
;; VERIFY took 30.71 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 38,259,384 bytes in use.  Commencing GC.]
; [GC completed with 30,732,024 bytes retained and 7,527,360 bytes freed.]
; [GC will next occur when at least 42,732,024 bytes are in use.]
;; Reading the file took 0.31 seconds
;; Checking the proof took 19.88 seconds
;; VERIFY took 26.45 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 42,741,408 bytes in use.  Commencing GC.]
; [GC completed with 30,266,152 bytes retained and 12,475,256 bytes freed.]
; [GC will next occur when at least 42,266,152 bytes are in use.]
; Compiling LAMBDA (X ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.06 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.18 seconds
;; Checking the proof took 2.63 seconds
;; VERIFY took 3.77 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.03 seconds
;; Checking the proof took 0.55 seconds
;; VERIFY took 0.69 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 43,200,488 bytes in use.  Commencing GC.]
; [GC completed with 33,627,552 bytes retained and 9,572,936 bytes freed.]
; [GC will next occur when at least 45,627,552 bytes are in use.]
;; Reading the file took 0.27 seconds
;; Checking the proof took 20.75 seconds
;; VERIFY took 29.17 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 46,154,336 bytes in use.  Commencing GC.]
; [GC completed with 20,476,752 bytes retained and 25,677,584 bytes freed.]
; [GC will next occur when at least 32,476,752 bytes are in use.]
;; Reading the file took 0.32 seconds
;; Checking the proof took 11.91 seconds
;; VERIFY took 16.87 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 32,489,816 bytes in use.  Commencing GC.]
; [GC completed with 23,785,384 bytes retained and 8,704,432 bytes freed.]
; [GC will next occur when at least 35,785,384 bytes are in use.]
;; Reading the file took 0.51 seconds
; [GC threshold exceeded with 36,665,584 bytes in use.  Commencing GC.]
; [GC completed with 28,203,928 bytes retained and 8,461,656 bytes freed.]
; [GC will next occur when at least 40,203,928 bytes are in use.]
;; Checking the proof took 5.63 seconds
;; VERIFY took 8.35 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.01 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.02 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.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 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.07 seconds
;; Checking the proof took 1.82 seconds
;; VERIFY took 2.44 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 41,253,744 bytes in use.  Commencing GC.]
; [GC completed with 33,124,600 bytes retained and 8,129,144 bytes freed.]
; [GC will next occur when at least 45,124,600 bytes are in use.]
;; Reading the file took 0.27 seconds
;; Checking the proof took 15.91 seconds
;; VERIFY took 20.74 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.07 seconds
;; Checking the proof took 2.50 seconds
;; VERIFY took 3.33 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.01 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.01 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 45,779,464 bytes in use.  Commencing GC.]
; [GC completed with 22,482,752 bytes retained and 23,296,712 bytes freed.]
; [GC will next occur when at least 34,482,752 bytes are in use.]
;; Reading the file took 0.24 seconds
;; Checking the proof took 2.64 seconds
;; VERIFY took 3.84 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.03 seconds
;; Checking the proof took 0.55 seconds
;; VERIFY took 0.69 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 35,610,448 bytes in use.  Commencing GC.]
; [GC completed with 29,844,472 bytes retained and 5,765,976 bytes freed.]
; [GC will next occur when at least 41,844,472 bytes are in use.]
;; Reading the file took 0.31 seconds
;; Checking the proof took 20.97 seconds
;; VERIFY took 29.46 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 44,213,040 bytes in use.  Commencing GC.]
; [GC completed with 29,503,072 bytes retained and 14,709,968 bytes freed.]
; [GC will next occur when at least 41,503,072 bytes are in use.]
;; Reading the file took 0.28 seconds
;; Checking the proof took 12.05 seconds
;; VERIFY took 17.00 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 43,823,200 bytes in use.  Commencing GC.]
; [GC completed with 36,479,800 bytes retained and 7,343,400 bytes freed.]
; [GC will next occur when at least 48,479,800 bytes are in use.]
;; Reading the file took 0.53 seconds
;; Checking the proof took 5.65 seconds
;; VERIFY took 8.34 seconds
4571> DEFINE LEVEL2.STEP-OKP
;; Reading from Proofs/level2/admit-level2.step-okp.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
; Compiling LAMBDA (X AXIOMS THMS ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 0.03 seconds
4572> VERIFY LEVEL2.STEP-OKP
;; Reading from Proofs/level2/thm-level2.step-okp.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 seconds
4573> VERIFY SOUNDNESS-OF-LEVEL2.STEP-OKP
;; Reading from Proofs/level2/thm-soundness-of-level2.step-okp.proof
; [GC threshold exceeded with 48,977,520 bytes in use.  Commencing GC.]
; [GC completed with 25,137,240 bytes retained and 23,840,280 bytes freed.]
; [GC will next occur when at least 37,137,240 bytes are in use.]
;; Reading the file took 0.35 seconds
;; Checking the proof took 4.08 seconds
;; VERIFY took 6.27 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 37,148,104 bytes in use.  Commencing GC.]
; [GC completed with 31,478,184 bytes retained and 5,669,920 bytes freed.]
; [GC will next occur when at least 43,478,184 bytes are in use.]
; [GC threshold exceeded with 47,206,160 bytes in use.  Commencing GC.]
; [GC completed with 37,264,768 bytes retained and 9,941,392 bytes freed.]
; [GC will next occur when at least 49,264,768 bytes are in use.]
;; Reading the file took 1.14 seconds
; [GC threshold exceeded with 50,414,096 bytes in use.  Commencing GC.]
; [GC completed with 45,159,632 bytes retained and 5,254,464 bytes freed.]
; [GC will next occur when at least 57,159,632 bytes are in use.]
;; Checking the proof took 22.22 seconds
;; VERIFY took 33.66 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 58,055,480 bytes in use.  Commencing GC.]
; [GC completed with 50,929,320 bytes retained and 7,126,160 bytes freed.]
; [GC will next occur when at least 62,929,320 bytes are in use.]
;; Reading the file took 0.34 seconds
;; Checking the proof took 4.51 seconds
;; VERIFY took 6.24 seconds
4576> DEFINE LEVEL2.FLAG-PROOFP
;; Reading from Proofs/level2/admit-level2.flag-proofp.proofs
;; Reading the file took 0.22 seconds
; [GC threshold exceeded with 63,000,304 bytes in use.  Commencing GC.]
; [GC completed with 54,038,456 bytes retained and 8,961,848 bytes freed.]
; [GC will next occur when at least 66,038,456 bytes are in use.]
;; Checking the proofs took 1.67 seconds
; Compiling LAMBDA (FLAG X AXIOMS THMS ATBL): 
; Compiling Top-Level Form: 
;; DEFINE took 2.35 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.02 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.04 seconds
4579> VERIFY LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-level2.proofp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4580> DEFINE LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/admit-level2.proof-listp.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
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.03 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.14 seconds
4583> VERIFY DEFINITION-OF-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-definition-of-level2.proof-listp.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.28 seconds
;; VERIFY took 0.42 seconds
4584> VERIFY LEVEL2.PROOFP-WHEN-NOT-CONSP
;; Reading from Proofs/level2/thm-level2.proofp-when-not-consp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.11 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.04 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.12 seconds
4586> VERIFY LEVEL2.PROOF-LISTP-OF-CONS
;; Reading from Proofs/level2/thm-level2.proof-listp-of-cons.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.18 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 66,048,936 bytes in use.  Commencing GC.]
; [GC completed with 30,983,968 bytes retained and 35,064,968 bytes freed.]
; [GC will next occur when at least 42,983,968 bytes are in use.]
; [GC threshold exceeded with 48,719,280 bytes in use.  Commencing GC.]
; [GC completed with 37,244,872 bytes retained and 11,474,408 bytes freed.]
; [GC will next occur when at least 49,244,872 bytes are in use.]
;; Reading the file took 0.63 seconds
;; Checking the proof took 4.04 seconds
;; VERIFY took 5.80 seconds
4588> VERIFY BOOLEANP-OF-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-booleanp-of-level2.proofp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.23 seconds
4589> VERIFY BOOLEANP-OF-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-booleanp-of-level2.proof-listp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.24 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 51,510,848 bytes in use.  Commencing GC.]
; [GC completed with 37,387,328 bytes retained and 14,123,520 bytes freed.]
; [GC will next occur when at least 49,387,328 bytes are in use.]
;; Reading the file took 0.28 seconds
;; Checking the proof took 1.51 seconds
;; VERIFY took 2.30 seconds
4591> VERIFY LEVEL2.PROOF-LISTP-OF-APP
;; Reading from Proofs/level2/thm-level2.proof-listp-of-app.proof
; [GC threshold exceeded with 51,666,952 bytes in use.  Commencing GC.]
; [GC completed with 43,883,472 bytes retained and 7,783,480 bytes freed.]
; [GC will next occur when at least 55,883,472 bytes are in use.]
;; Reading the file took 0.54 seconds
;; Checking the proof took 3.02 seconds
;; VERIFY took 4.77 seconds
4592> VERIFY LEVEL2.PROOF-LISTP-OF-REV
;; Reading from Proofs/level2/thm-level2.proof-listp-of-rev.proof
; [GC threshold exceeded with 57,327,320 bytes in use.  Commencing GC.]
; [GC completed with 30,579,952 bytes retained and 26,747,368 bytes freed.]
; [GC will next occur when at least 42,579,952 bytes are in use.]
;; Reading the file took 0.30 seconds
;; Checking the proof took 1.59 seconds
;; VERIFY took 2.43 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.13 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 0.44 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.06 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.26 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 42,589,136 bytes in use.  Commencing GC.]
; [GC completed with 31,252,328 bytes retained and 11,336,808 bytes freed.]
; [GC will next occur when at least 43,252,328 bytes are in use.]
;; Reading the file took 0.40 seconds
;; Checking the proof took 1.19 seconds
;; VERIFY took 1.95 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.03 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.21 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 44,930,616 bytes in use.  Commencing GC.]
; [GC completed with 33,627,712 bytes retained and 11,302,904 bytes freed.]
; [GC will next occur when at least 45,627,712 bytes are in use.]
;; Reading the file took 0.21 seconds
;; Checking the proof took 1.07 seconds
;; VERIFY took 1.56 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.28 seconds
; [GC threshold exceeded with 46,057,744 bytes in use.  Commencing GC.]
; [GC completed with 39,349,424 bytes retained and 6,708,320 bytes freed.]
; [GC will next occur when at least 51,349,424 bytes are in use.]
;; Checking the proof took 1.78 seconds
;; VERIFY took 2.64 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.17 seconds
;; Checking the proof took 1.04 seconds
;; VERIFY took 1.49 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 52,899,800 bytes in use.  Commencing GC.]
; [GC completed with 36,366,360 bytes retained and 16,533,440 bytes freed.]
; [GC will next occur when at least 48,366,360 bytes are in use.]
;; Reading the file took 0.23 seconds
;; Checking the proof took 1.33 seconds
;; VERIFY took 1.94 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.05 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.12 seconds
4602> VERIFY LEVEL2.PROOF-LISTP-OF-REPEAT
;; Reading from Proofs/level2/thm-level2.proof-listp-of-repeat.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 1.15 seconds
;; VERIFY took 1.65 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 48,377,040 bytes in use.  Commencing GC.]
; [GC completed with 39,647,424 bytes retained and 8,729,616 bytes freed.]
; [GC will next occur when at least 51,647,424 bytes are in use.]
; [GC threshold exceeded with 51,658,088 bytes in use.  Commencing GC.]
; [GC completed with 44,155,048 bytes retained and 7,503,040 bytes freed.]
; [GC will next occur when at least 56,155,048 bytes are in use.]
; [GC threshold exceeded with 57,070,848 bytes in use.  Commencing GC.]
; [GC completed with 48,660,400 bytes retained and 8,410,448 bytes freed.]
; [GC will next occur when at least 60,660,400 bytes are in use.]
; [GC threshold exceeded with 73,631,464 bytes in use.  Commencing GC.]
; [GC completed with 51,197,368 bytes retained and 22,434,096 bytes freed.]
; [GC will next occur when at least 63,197,368 bytes are in use.]
; [GC threshold exceeded with 68,940,752 bytes in use.  Commencing GC.]
; [GC completed with 68,942,760 bytes retained and -2,008 bytes freed.]
; [GC will next occur when at least 80,942,760 bytes are in use.]
;; Reading the file took 2.19 seconds
;; Checking the proof took 18.26 seconds
;; VERIFY took 26.84 seconds
4604> VERIFY LOGIC.PROVABLEP-WHEN-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-logic.provablep-when-level2.proofp.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.50 seconds
;; VERIFY took 0.79 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.08 seconds
;; Checking the proof took 0.50 seconds
;; VERIFY took 0.77 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 80,958,008 bytes in use.  Commencing GC.]
; [GC completed with 72,119,288 bytes retained and 8,838,720 bytes freed.]
; [GC will next occur when at least 84,119,288 bytes are in use.]
; [GC threshold exceeded with 87,283,712 bytes in use.  Commencing GC.]
; [GC completed with 78,393,792 bytes retained and 8,889,920 bytes freed.]
; [GC will next occur when at least 90,393,792 bytes are in use.]
;; Reading the file took 0.81 seconds
;; Checking the proof took 5.76 seconds
;; VERIFY took 8.43 seconds
4607> VERIFY LEVEL2.PROOFP-WHEN-LOGIC.PROOFP
;; Reading from Proofs/level2/thm-level2.proofp-when-logic.proofp.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.36 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.05 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.35 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.05 seconds
;; VERIFY took 0.07 seconds
4610> VERIFY INSTALL-NEW-PROOFP-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-install-new-proofp-level2.proofp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.09 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.lhug-cmucl:
Writing 23625600 bytes from the Read-Only space at 0x10000000.
Writing 4741880 bytes from the Static space at 0x28000000.
Writing 8192 bytes from the Dynamic space at 0x58100000.
done.]

real	111m36.536s
user	110m44.243s
sys	0m7.756s