Milawa Proof Checker.
4010> DEFINE BUILD.AXIOM
;; Reading from Proofs/level2/admit-build.axiom.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4011> VERIFY BUILD.AXIOM
;; Reading from Proofs/level2/thm-build.axiom.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.02 seconds
4013> VERIFY LOGIC.METHOD-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.method-of-build.axiom.proof
;; Reading the file took 0.01 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.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4016> VERIFY LOGIC.EXTRAS-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.extras-of-build.axiom.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 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.08 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.20 seconds
;; VERIFY took 0.30 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
;; DEFINE took 0.00 seconds
4020> VERIFY BUILD.THEOREM
;; Reading from Proofs/level2/thm-build.theorem.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4023> VERIFY LOGIC.CONCLUSION-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.theorem.proof
;; Reading the file took 0.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.01 seconds
;; Checking the proof took 0.02 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.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4026> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.theorem.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.08 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.07 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.30 seconds
4028> DEFINE BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/admit-build.propositional-schema.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4029> VERIFY BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-build.propositional-schema.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4030> VERIFY BUILD.PROPOSITIONAL-SCHEMA-UNDER-IFF
;; Reading from Proofs/level2/thm-build.propositional-schema-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4031> VERIFY LOGIC.METHOD-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-logic.method-of-build.propositional-schema.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.03 seconds
;; VERIFY took 0.04 seconds
4033> VERIFY LOGIC.SUBPROOFS-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.propositional-schema.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 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.03 seconds
4035> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.propositional-schema.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.12 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.06 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 0.35 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
;; DEFINE took 0.01 seconds
4038> VERIFY BUILD.CUT
;; Reading from Proofs/level2/thm-build.cut.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4039> VERIFY BUILD.CUT-UNDER-IFF
;; Reading from Proofs/level2/thm-build.cut-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4040> VERIFY LOGIC.METHOD-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-logic.method-of-build.cut.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4041> VERIFY LOGIC.CONCLUSION-OF-CUT
;; Reading from Proofs/level2/thm-logic.conclusion-of-cut.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
4042> VERIFY LOGIC.SUBPROOFS-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.cut.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.10 seconds
4043> VERIFY LOGIC.EXTRAS-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-logic.extras-of-build.cut.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 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.09 seconds
;; Checking the proof took 0.34 seconds
;; VERIFY took 0.50 seconds
4045> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.cut.proof
;; Reading the file took 0.31 seconds
;; Checking the proof took 1.06 seconds
;; VERIFY took 1.66 seconds
4046> DEFINE BUILD.CONTRACTION
;; Reading from Proofs/level2/admit-build.contraction.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4047> VERIFY BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-build.contraction.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4048> VERIFY BUILD.CONTRACTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.contraction-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4049> VERIFY LOGIC.METHOD-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.method-of-build.contraction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4050> VERIFY LOGIC.CONCLUSION-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.contraction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4051> VERIFY LOGIC.SUBPROOFS-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.contraction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 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.03 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.05 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.23 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.12 seconds
;; Checking the proof took 0.40 seconds
;; VERIFY took 0.59 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
;; DEFINE took 0.00 seconds
4056> VERIFY BUILD.EXPANSION
;; Reading from Proofs/level2/thm-build.expansion.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4057> VERIFY BUILD.EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.expansion-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.02 seconds
4058> VERIFY LOGIC.METHOD-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.method-of-build.expansion.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4059> VERIFY LOGIC.CONCLUSION-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.expansion.proof
;; Reading the file took 0.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.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
4061> VERIFY LOGIC.EXTRAS-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.extras-of-build.expansion.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4062> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.expansion.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.12 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
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.31 seconds
;; VERIFY took 0.44 seconds
4064> DEFINE BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.associativity.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4065> VERIFY BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.associativity.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4066> VERIFY BUILD.ASSOCIATIVITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.associativity-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4067> VERIFY LOGIC.METHOD-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.method-of-build.associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.02 seconds
4068> VERIFY LOGIC.CONCLUSION-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
4069> VERIFY LOGIC.SUBPROOFS-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.06 seconds
4070> VERIFY LOGIC.EXTRAS-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.extras-of-build.associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4071> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.associativity.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.32 seconds
;; VERIFY took 0.44 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.17 seconds
;; Checking the proof took 0.73 seconds
;; VERIFY took 1.04 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
;; DEFINE took 0.00 seconds
4074> VERIFY BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-build.instantiation.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4075> VERIFY BUILD.INSTANTIATION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.instantiation-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.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.05 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.18 seconds
4077> VERIFY LOGIC.CONCLUSION-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.instantiation.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.11 seconds
4078> VERIFY LOGIC.SUBPROOFS-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.instantiation.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.40 seconds
;; VERIFY took 0.60 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.12 seconds
;; VERIFY took 0.18 seconds
4080> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.instantiation.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.33 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.22 seconds
;; Checking the proof took 0.63 seconds
;; VERIFY took 0.98 seconds
4082> DEFINE BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/admit-build.functional-equality.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4083> VERIFY BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-build.functional-equality.proof
;; Reading the file took 0.00 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.02 seconds
4086> VERIFY LOGIC.CONCLUSION-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.functional-equality.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.02 seconds
4087> VERIFY LOGIC.SUBPROOFS-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.functional-equality.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4088> VERIFY LOGIC.EXTRAS-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-logic.extras-of-build.functional-equality.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4089> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.functional-equality.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.24 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.22 seconds
;; Checking the proof took 0.68 seconds
;; VERIFY took 1.03 seconds
4091> DEFINE BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/admit-build.beta-reduction.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4092> VERIFY BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-build.beta-reduction.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4093> VERIFY BUILD.BETA-REDUCTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.beta-reduction-under-iff.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.12 seconds
4094> VERIFY LOGIC.METHOD-OF-BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-logic.method-of-build.beta-reduction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4095> VERIFY LOGIC.CONCLUSION-OF-BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.beta-reduction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.06 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.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 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.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 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.10 seconds
;; Checking the proof took 0.40 seconds
;; VERIFY took 0.56 seconds
4099> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.beta-reduction.proof
;; Reading the file took 0.30 seconds
;; Checking the proof took 1.02 seconds
;; VERIFY took 1.56 seconds
4100> DEFINE BUILD.BASE-EVAL
;; Reading from Proofs/level2/admit-build.base-eval.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4101> VERIFY BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-build.base-eval.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4102> VERIFY BUILD.BASE-EVAL-UNDER-IFF
;; Reading from Proofs/level2/thm-build.base-eval-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.02 seconds
4103> VERIFY LOGIC.METHOD-OF-BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-logic.method-of-build.base-eval.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4104> VERIFY LOGIC.CONCLUSION-OF-BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.base-eval.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 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.02 seconds
;; VERIFY took 0.04 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.02 seconds
;; VERIFY took 0.03 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.04 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.14 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.31 seconds
;; VERIFY took 0.44 seconds
4109> DEFINE BUILD.INSTANTIATION-LIST
;; Reading from Proofs/level2/admit-build.instantiation-list.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.11 seconds
;; DEFINE took 0.15 seconds
4110> VERIFY BUILD.INSTANTIATION-LIST
;; Reading from Proofs/level2/thm-build.instantiation-list.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4111> VERIFY BUILD.INSTANTIATION-LIST-WHEN-NOT-CONSP
;; Reading from Proofs/level2/thm-build.instantiation-list-when-not-consp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 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.07 seconds
;; VERIFY took 0.09 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.39 seconds
;; Checking the proof took 1.08 seconds
;; VERIFY took 1.62 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
;; Reading the file took 0.35 seconds
;; Checking the proof took 0.98 seconds
;; VERIFY took 1.47 seconds
4115> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.INSTANTIATION-LIST
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.instantiation-list.proof
;; Reading the file took 0.48 seconds
;; Checking the proof took 1.40 seconds
;; VERIFY took 2.10 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
;; DEFINE took 0.00 seconds
4117> VERIFY BUILD.INDUCTION
;; Reading from Proofs/level2/thm-build.induction.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4118> VERIFY BUILD.INDUCTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.induction-under-iff.proof
;; Reading the file took 0.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.03 seconds
;; VERIFY took 0.04 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.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 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.13 seconds
;; VERIFY took 0.16 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.04 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.16 seconds
4124> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.induction.proof
;; Reading the file took 0.63 seconds
;; Checking the proof took 2.12 seconds
;; VERIFY took 3.41 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
;; DEFINE took 0.00 seconds
4126> VERIFY BUILD.COMMUTE-OR
;; Reading from Proofs/level2/thm-build.commute-or.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4127> VERIFY BUILD.COMMUTE-OR-UNDER-IFF
;; Reading from Proofs/level2/thm-build.commute-or-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 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.07 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.02 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.09 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.09 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 0.36 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
;; DEFINE took 0.02 seconds
4132> VERIFY BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-build.commute-or-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4133> VERIFY BOOLEANP-OF-BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.commute-or-okp.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.61 seconds
;; VERIFY took 0.91 seconds
4134> VERIFY BUILD.COMMUTE-OR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.commute-or-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.26 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.43 seconds
;; Checking the proof took 4.80 seconds
;; VERIFY took 6.45 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
;; Reading the file took 0.31 seconds
;; Checking the proof took 3.09 seconds
;; VERIFY took 4.17 seconds
4137> VERIFY FORCING-SOUNDNESS-OF-BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.commute-or-okp.proof
;; Reading the file took 0.71 seconds
;; Checking the proof took 2.12 seconds
;; VERIFY took 3.30 seconds
4138> DEFINE BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/admit-build.right-expansion.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4139> VERIFY BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-build.right-expansion.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.03 seconds
4141> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.right-expansion.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.14 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.14 seconds
;; Checking the proof took 0.46 seconds
;; VERIFY took 0.65 seconds
4143> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.right-expansion.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.22 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
;; DEFINE took 0.01 seconds
4145> VERIFY BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-build.right-expansion-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4146> VERIFY BOOLEANP-OF-BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.right-expansion-okp.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 0.44 seconds
;; VERIFY took 0.66 seconds
4147> VERIFY BUILD.RIGHT-EXPANSION-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.right-expansion-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.21 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
;; Reading the file took 0.64 seconds
;; Checking the proof took 7.47 seconds
;; VERIFY took 9.96 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.31 seconds
;; Checking the proof took 1.78 seconds
;; VERIFY took 2.49 seconds
4150> VERIFY FORCING-SOUNDNESS-OF-BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.right-expansion-okp.proof
;; Reading the file took 0.61 seconds
;; Checking the proof took 1.50 seconds
;; VERIFY took 2.43 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
;; DEFINE took 0.00 seconds
4152> VERIFY BUILD.MODUS-PONENS
;; Reading from Proofs/level2/thm-build.modus-ponens.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4153> VERIFY BUILD.MODUS-PONENS-UNDER-IFF
;; Reading from Proofs/level2/thm-build.modus-ponens-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4154> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MODUS-PONENS
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.modus-ponens.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.68 seconds
;; VERIFY took 0.91 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.23 seconds
;; Checking the proof took 0.79 seconds
;; VERIFY took 1.17 seconds
4156> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.MODUS-PONENS
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.modus-ponens.proof
;; Reading the file took 0.40 seconds
;; Checking the proof took 7.05 seconds
;; VERIFY took 9.05 seconds
4157> DEFINE BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/admit-build.modus-ponens-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4158> VERIFY BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-build.modus-ponens-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4159> VERIFY BOOLEANP-OF-BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.modus-ponens-okp.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.71 seconds
;; VERIFY took 1.02 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.25 seconds
;; VERIFY took 0.30 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
;; Reading the file took 0.61 seconds
;; Checking the proof took 8.62 seconds
;; VERIFY took 11.36 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
;; Reading the file took 0.35 seconds
;; Checking the proof took 4.28 seconds
;; VERIFY took 5.61 seconds
4163> VERIFY FORCING-SOUNDNESS-OF-BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.modus-ponens-okp.proof
;; Reading the file took 1.48 seconds
;; Checking the proof took 6.18 seconds
;; VERIFY took 9.04 seconds
4164> DEFINE BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/admit-build.modus-ponens-2.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4165> VERIFY BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/thm-build.modus-ponens-2.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4166> VERIFY BUILD.MODUS-PONENS-2-UNDER-IFF
;; Reading from Proofs/level2/thm-build.modus-ponens-2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4167> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.modus-ponens-2.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.78 seconds
;; VERIFY took 1.02 seconds
4168> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.modus-ponens-2.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.13 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.41 seconds
;; Checking the proof took 7.93 seconds
;; VERIFY took 10.14 seconds
4170> DEFINE BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/admit-build.modus-ponens-2-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4171> VERIFY BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-build.modus-ponens-2-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4172> VERIFY BOOLEANP-OF-BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.modus-ponens-2-okp.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 0.69 seconds
;; VERIFY took 1.00 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.02 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 0.30 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
;; Reading the file took 0.61 seconds
;; Checking the proof took 8.56 seconds
;; VERIFY took 11.26 seconds
4175> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.modus-ponens-2-okp.proof
;; Reading the file took 0.35 seconds
;; Checking the proof took 5.10 seconds
;; VERIFY took 6.66 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
;; Reading the file took 1.46 seconds
;; Checking the proof took 6.03 seconds
;; VERIFY took 8.89 seconds
4177> DEFINE BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.right-associativity.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4178> VERIFY BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.right-associativity.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4179> VERIFY BUILD.RIGHT-ASSOCIATIVITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.right-associativity-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 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.13 seconds
;; Checking the proof took 2.94 seconds
;; VERIFY took 3.50 seconds
4181> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.right-associativity.proof
;; Reading the file took 0.79 seconds
;; Checking the proof took 25.76 seconds
;; VERIFY took 30.34 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.15 seconds
;; Checking the proof took 4.67 seconds
;; VERIFY took 5.54 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
;; DEFINE took 0.03 seconds
4184> VERIFY BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-build.right-associativity-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4185> VERIFY BOOLEANP-OF-BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.right-associativity-okp.proof
;; Reading the file took 0.40 seconds
;; Checking the proof took 1.52 seconds
;; VERIFY took 2.29 seconds
4186> VERIFY BUILD.RIGHT-ASSOCIATIVITY-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.right-associativity-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.36 seconds
;; VERIFY took 0.44 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
;; Reading the file took 0.49 seconds
;; Checking the proof took 11.74 seconds
;; VERIFY took 15.41 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.42 seconds
;; Checking the proof took 6.79 seconds
;; VERIFY took 8.99 seconds
4189> VERIFY FORCING-SOUNDNESS-OF-BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.right-associativity-okp.proof
;; Reading the file took 0.96 seconds
;; Checking the proof took 3.67 seconds
;; VERIFY took 5.47 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
;; DEFINE took 0.00 seconds
4191> VERIFY BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/thm-build.disjoined-left-expansion.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4192> VERIFY BUILD.DISJOINED-LEFT-EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-left-expansion-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4193> VERIFY FORCING-LOGIC

;;; Starting full GC,     556,007,424 bytes allocated.
;;; Finished full GC.     532,417,232 bytes freed in 0.342663 s

;;; 14083 soft faults, 0 faults, 0 pageins

.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.09 seconds
;; Checking the proof took 0.38 seconds
;; VERIFY took 0.52 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
;; Reading the file took 0.76 seconds
;; Checking the proof took 3.67 seconds
;; VERIFY took 4.96 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.12 seconds
;; Checking the proof took 0.60 seconds
;; VERIFY took 0.81 seconds
4196> DEFINE BUILD.DISJOINED-LEFT-EXPANSION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-left-expansion-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 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
;; Reading the file took 0.40 seconds
;; Checking the proof took 1.23 seconds
;; VERIFY took 1.93 seconds
4199> VERIFY BUILD.DISJOINED-LEFT-EXPANSION-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-left-expansion-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.28 seconds
;; VERIFY took 0.34 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
;; Reading the file took 0.79 seconds
;; Checking the proof took 16.30 seconds
;; VERIFY took 21.53 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.44 seconds
;; Checking the proof took 4.26 seconds
;; VERIFY took 5.82 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
;; Reading the file took 1.04 seconds
;; Checking the proof took 3.30 seconds
;; VERIFY took 5.11 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
;; DEFINE took 0.00 seconds
4204> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-build.disjoined-right-expansion.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4205> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-right-expansion-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4206> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-right-expansion.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 1.38 seconds
;; VERIFY took 1.73 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
;; Reading the file took 0.70 seconds
;; Checking the proof took 6.89 seconds
;; VERIFY took 8.67 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.15 seconds
;; Checking the proof took 2.38 seconds
;; VERIFY took 2.98 seconds
4209> DEFINE BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-right-expansion-okp.proofs
;; Reading the file took 0.03 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.04 seconds
4210> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-build.disjoined-right-expansion-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4211> VERIFY BOOLEANP-OF-BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-right-expansion-okp.proof
;; Reading the file took 0.39 seconds
;; Checking the proof took 1.25 seconds
;; VERIFY took 1.95 seconds
4212> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-right-expansion-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.29 seconds
;; VERIFY took 0.35 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
;; Reading the file took 0.80 seconds
;; Checking the proof took 16.76 seconds
;; VERIFY took 22.05 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.41 seconds
;; Checking the proof took 4.50 seconds
;; VERIFY took 6.02 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
;; Reading the file took 1.12 seconds
;; Checking the proof took 3.57 seconds
;; VERIFY took 5.46 seconds
4216> DEFINE BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/admit-build.disjoined-contraction.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4217> VERIFY BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/thm-build.disjoined-contraction.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4218> VERIFY BUILD.DISJOINED-CONTRACTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-contraction-under-iff.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.08 seconds
4219> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-contraction.proof
;; Reading the file took 0.27 seconds
;; Checking the proof took 3.43 seconds
;; VERIFY took 4.32 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.21 seconds
;; Checking the proof took 0.82 seconds
;; VERIFY took 1.17 seconds
4221> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-contraction.proof
;; Reading the file took 0.55 seconds
;; Checking the proof took 12.80 seconds
;; VERIFY took 15.84 seconds
4222> DEFINE BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-contraction-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 seconds
4223> VERIFY BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/thm-build.disjoined-contraction-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4224> VERIFY BOOLEANP-OF-BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-contraction-okp.proof
;; Reading the file took 0.29 seconds
;; Checking the proof took 1.22 seconds
;; VERIFY took 1.79 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.03 seconds
;; Checking the proof took 0.32 seconds
;; VERIFY took 0.39 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
;; Reading the file took 0.45 seconds
;; Checking the proof took 11.99 seconds
;; VERIFY took 15.57 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 0.42 seconds
;; Checking the proof took 8.95 seconds
;; VERIFY took 11.68 seconds
4228> VERIFY FORCING-SOUNDNESS-OF-BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.disjoined-contraction-okp.proof
;; Reading the file took 1.15 seconds
;; Checking the proof took 5.82 seconds
;; VERIFY took 8.35 seconds
4229> DEFINE BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/admit-build.cancel-neg-neg.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4230> VERIFY BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/thm-build.cancel-neg-neg.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4231> VERIFY BUILD.CANCEL-NEG-NEG-UNDER-IFF
;; Reading from Proofs/level2/thm-build.cancel-neg-neg-under-iff.proof
;; Reading the file took 0.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.08 seconds
;; Checking the proof took 0.50 seconds
;; VERIFY took 0.65 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.26 seconds
;; Checking the proof took 2.47 seconds
;; VERIFY took 3.09 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.11 seconds
;; Checking the proof took 0.63 seconds
;; VERIFY took 0.83 seconds
4235> DEFINE BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/admit-build.cancel-neg-neg-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4236> VERIFY BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-build.cancel-neg-neg-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4237> VERIFY BOOLEANP-OF-BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.cancel-neg-neg-okp.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 0.48 seconds
;; VERIFY took 0.68 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.02 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.24 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.31 seconds
;; Checking the proof took 4.19 seconds
;; VERIFY took 5.48 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
;; Reading the file took 0.29 seconds
;; Checking the proof took 3.60 seconds
;; VERIFY took 4.72 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
;; Reading the file took 0.89 seconds
;; Checking the proof took 3.23 seconds
;; VERIFY took 4.83 seconds
4242> DEFINE BUILD.INSERT-NEG-NEG
;; Reading from Proofs/level2/admit-build.insert-neg-neg.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4243> VERIFY BUILD.INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-build.insert-neg-neg.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.02 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 0.07 seconds
;; Checking the proof took 0.37 seconds
;; VERIFY took 0.49 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.15 seconds
;; Checking the proof took 1.31 seconds
;; VERIFY took 1.60 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.09 seconds
;; Checking the proof took 0.48 seconds
;; VERIFY took 0.64 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
;; DEFINE took 0.01 seconds
4249> VERIFY BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-build.insert-neg-neg-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4250> VERIFY BOOLEANP-OF-BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.insert-neg-neg-okp.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 0.44 seconds
;; VERIFY took 0.64 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.03 seconds
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.24 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
;; Reading the file took 0.94 seconds
;; Checking the proof took 7.07 seconds
;; VERIFY took 9.66 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.28 seconds
;; Checking the proof took 1.80 seconds
;; VERIFY took 2.47 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
;; Reading the file took 0.42 seconds
;; Checking the proof took 1.07 seconds
;; VERIFY took 1.70 seconds
4255> DEFINE BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/admit-build.lhs-insert-neg-neg.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4256> VERIFY BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg.proof
;; Reading the file took 0.00 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.11 seconds
;; Checking the proof took 0.69 seconds
;; VERIFY took 0.89 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
;; Reading the file took 0.67 seconds
;; Checking the proof took 4.07 seconds
;; VERIFY took 5.24 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.13 seconds
;; Checking the proof took 1.33 seconds
;; VERIFY took 1.65 seconds
4261> DEFINE BUILD.LHS-INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/admit-build.lhs-insert-neg-neg-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4262> VERIFY BUILD.LHS-INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4263> VERIFY BOOLEANP-OF-BUILD.LHS-INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.lhs-insert-neg-neg-okp.proof
;; Reading the file took 0.29 seconds
;; Checking the proof took 1.15 seconds
;; VERIFY took 1.70 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.03 seconds
;; Checking the proof took 0.32 seconds
;; VERIFY took 0.39 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
;; Reading the file took 1.72 seconds
;; Checking the proof took 22.27 seconds
;; VERIFY took 29.71 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.38 seconds
;; Checking the proof took 4.48 seconds
;; VERIFY took 5.99 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
;; Reading the file took 0.72 seconds
;; Checking the proof took 2.33 seconds
;; VERIFY took 3.57 seconds
4268> DEFINE BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/admit-build.merge-negatives.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4269> VERIFY BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/thm-build.merge-negatives.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4270> VERIFY BUILD.MERGE-NEGATIVES-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-negatives-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4271> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.merge-negatives.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 15.43 seconds
;; VERIFY took 18.50 seconds
4272> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.merge-negatives.proof
;; Reading the file took 1.00 seconds
;; Checking the proof took 39.25 seconds
;; VERIFY took 47.30 seconds
4273> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.merge-negatives.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 22.05 seconds
;; VERIFY took 26.64 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
;; DEFINE took 0.02 seconds
4275> VERIFY BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/thm-build.merge-negatives-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4276> VERIFY BOOLEANP-OF-BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.merge-negatives-o

;;; Starting full GC,     560,201,728 bytes allocated.
;;; Finished full GC.     539,220,704 bytes freed in 0.324848 s

;;; 227 soft faults, 0 faults, 0 pageins

kp.proof
;; Reading the file took 0.29 seconds
;; Checking the proof took 1.21 seconds
;; VERIFY took 1.76 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
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.33 seconds
;; VERIFY took 0.41 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
;; Reading the file took 1.02 seconds
;; Checking the proof took 10.53 seconds
;; VERIFY took 14.16 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
;; Reading the file took 0.42 seconds
;; Checking the proof took 5.21 seconds
;; VERIFY took 6.89 seconds
4280> VERIFY FORCING-SOUNDNESS-OF-BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.merge-negatives-okp.proof
;; Reading the file took 1.22 seconds
;; Checking the proof took 4.65 seconds
;; VERIFY took 6.87 seconds
4281> DEFINE BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/admit-build.merge-implications-lemma-1.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4282> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-1.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4283> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-1-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 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.21 seconds
;; Checking the proof took 14.66 seconds
;; VERIFY took 17.56 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
;; Reading the file took 1.46 seconds
;; Checking the proof took 46.44 seconds
;; VERIFY took 56.18 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.27 seconds
;; Checking the proof took 24.60 seconds
;; VERIFY took 29.69 seconds
4287> DEFINE BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/admit-build.merge-implications-lemma-2.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 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.01 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.20 seconds
;; Checking the proof took 11.74 seconds
;; VERIFY took 14.19 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
;; Reading the file took 0.91 seconds
;; Checking the proof took 50.04 seconds
;; VERIFY took 61.91 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.26 seconds
;; Checking the proof took 14.66 seconds
;; VERIFY took 17.98 seconds
4293> DEFINE BUILD.MERGE-IMPLICATIONS
;; Reading from Proofs/level2/admit-build.merge-implications.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4294> VERIFY BUILD.MERGE-IMPLICATIONS
;; Reading from Proofs/level2/thm-build.merge-implications.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4295> VERIFY BUILD.MERGE-IMPLICATIONS-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-implications-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4296> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MERGE-IMPLICATIONS
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.merge-implications.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 1.29 seconds
;; VERIFY took 1.72 seconds
4297> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.MERGE-IMPLICATIONS
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.merge-implications.proof
;; Reading the file took 0.94 seconds
;; Checking the proof took 20.06 seconds
;; VERIFY took 25.20 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.18 seconds
;; Checking the proof took 1.71 seconds
;; VERIFY took 2.20 seconds
4299> DEFINE BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/admit-build.merge-implications-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.04 seconds
4300> VERIFY BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/thm-build.merge-implications-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4301> VERIFY BOOLEANP-OF-BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.merge-implications-okp.proof
;; Reading the file took 0.78 seconds
;; Checking the proof took 4.31 seconds
;; VERIFY took 6.34 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.63 seconds
;; VERIFY took 0.76 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
;; Reading the file took 0.99 seconds
;; Checking the proof took 36.67 seconds
;; VERIFY took 47.42 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
;; Reading the file took 0.61 seconds
;; Checking the proof took 16.48 seconds
;; VERIFY took 21.38 seconds
4305> VERIFY FORCING-SOUNDNESS-OF-BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.merge-implications-okp.proof
;; Reading the file took 2.14 seconds
;; Checking the proof took 12.47 seconds
;; VERIFY took 17.57 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.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4307> VERIFY BUILD.DISJOINED-COMMUTE-OR-LEMMA-1
;; Reading from Proofs/level2/thm-build.disjoined-commute-or-lemma-1.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4308> VERIFY BUILD.DISJOINED-COMMUTE-OR-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-commute-or-lemma-1-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.06 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
;; Reading the file took 0.21 seconds
;; Checking the proof took 10.57 seconds
;; VERIFY took 12.76 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
;; Reading the file took 0.80 seconds
;; Checking the proof took 27.43 seconds
;; VERIFY took 33.04 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
;; Reading the file took 0.22 seconds
;; Checking the proof took 16.53 seconds
;; VERIFY took 19.97 seconds
4312> DEFINE BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/admit-build.disjoined-commute-or.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4313> VERIFY BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/thm-build.disjoined-commute-or.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4314> VERIFY BUILD.DISJOINED-COMMUTE-OR-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-commute-or-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
4315> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-commute-or.proof
;; Reading the file took 0.28 seconds
;; Checking the proof took 15.46 seconds
;; VERIFY took 18.27 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
;; Reading the file took 0.51 seconds
;; Checking the proof took 65.38 seconds
;; VERIFY took 75.17 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
;; Reading the file took 0.34 seconds
;; Checking the proof took 18.97 seconds
;; VERIFY took 22.54 seconds
4318> DEFINE BUILD.DISJOINED-COMMUTE-OR-OKP
;; Reading from Proofs/level2/admit-build.disjoined-commute-or-okp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 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.02 seconds
4320> VERIFY BOOLEANP-OF-BUILD.DISJOINED-COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-commute-or-okp.proof
;; Reading the file took 0.38 seconds
;; Checking the proof took 1.61 seconds
;; VERIFY took 2.37 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.07 seconds
;; Checking the proof took 0.38 seconds
;; VERIFY took 0.49 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
;; Reading the file took 0.53 seconds
;; Checking the proof took 12.56 seconds
;; VERIFY took 16.33 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
;; Reading the file took 0.42 seconds
;; Checking the proof took 7.28 seconds
;; VERIFY took 9.49 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
;; Reading the file took 0.95 seconds
;; Checking the proof took 3.93 seconds
;; VERIFY took 5.72 seconds
4325> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-1A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-1a.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4326> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1A
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1a.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4327> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1A-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1a-under-iff.proof
;; Reading the file took 0.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.20 seconds
;; Checking the proof took 8.19 seconds
;; VERIFY took 9.80 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
;; Reading the file took 0.97 seconds
;; Checking the proof took 45.99 seconds
;; VERIFY took 54.72 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
;; Reading the file took 0.26 seconds
;; Checking the proof took 13.92 seconds
;; VERIFY took 16.81 seconds
4331> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-1.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4332> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4333> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took

;;; Starting full GC,     555,876,352 bytes allocated.
;;; Finished full GC.     529,510,176 bytes freed in 0.305233 s

;;; 0 soft faults, 0 faults, 0 pageins

 0.02 seconds
;; VERIFY took 0.04 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.16 seconds
;; Checking the proof took 3.37 seconds
;; VERIFY took 4.01 seconds
4335> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-assoc-lemma-1.proof
;; Reading the file took 1.11 seconds
;; Checking the proof took 15.89 seconds
;; VERIFY took 19.19 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.20 seconds
;; Checking the proof took 6.00 seconds
;; VERIFY took 7.24 seconds
4337> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-2a.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4338> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2a.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4339> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2A-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2a-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4340> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-2a.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 10.05 seconds
;; VERIFY took 12.09 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
;; Reading the file took 1.07 seconds
;; Checking the proof took 31.05 seconds
;; VERIFY took 37.73 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.25 seconds
;; Checking the proof took 16.66 seconds
;; VERIFY took 20.27 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
;; DEFINE took 0.00 seconds
4344> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.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.01 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
;; Reading the file took 0.16 seconds
;; Checking the proof took 3.34 seconds
;; VERIFY took 3.98 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
;; Reading the file took 0.79 seconds
;; Checking the proof took 15.69 seconds
;; VERIFY took 18.67 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.20 seconds
;; Checking the proof took 5.96 seconds
;; VERIFY took 7.20 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
;; 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.02 seconds
;; Checking the proof took 0.00 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.02 seconds
;; VERIFY took 0.04 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
;; Reading the file took 0.33 seconds
;; Checking the proof took 2.89 seconds
;; VERIFY took 3.60 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
;; Reading the file took 0.55 seconds
;; Checking the proof took 5.19 seconds
;; VERIFY took 6.44 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
;; Reading the file took 0.52 seconds
;; Checking the proof took 5.57 seconds
;; VERIFY took 7.06 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
;; DEFINE took 0.01 seconds
4356> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-3
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-3.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.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.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 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.14 seconds
;; Checking the proof took 2.65 seconds
;; VERIFY took 3.14 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
;; Reading the file took 1.00 seconds
;; Checking the proof took 22.16 seconds
;; VERIFY took 26.84 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
;; Reading the file took 0.18 seconds
;; Checking the proof took 3.33 seconds
;; VERIFY took 4.00 seconds
4361> DEFINE BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.disjoined-right-associativity.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4362> VERIFY BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.disjoined-right-associativity.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.14 seconds
;; Checking the proof took 4.88 seconds
;; VERIFY took 5.75 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
;; Reading the file took 0.78 seconds
;; Checking the proof took 58.74 seconds
;; VERIFY took 68.63 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.31 seconds
;; Checking the proof took 6.35 seconds
;; VERIFY took 7.64 seconds
4367> DEFINE BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/admit-build.disjoined-right-associativity-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.04 seconds
4368> VERIFY BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-build.disjoined-right-associativity-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4369> VERIFY BOOLEANP-OF-BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-right-associativity-okp.proof
;; Reading the file took 0.69 seconds
;; Checking the proof took 3.63 seconds
;; VERIFY took 5.23 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.04 seconds
;; Checking the proof took 0.62 seconds
;; VERIFY took 0.73 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
;; Reading the file took 0.64 seconds
;; Checking the proof took 26.15 seconds
;; VERIFY took 33.62 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
;; Reading the file took 0.50 seconds
;; Checking the proof took 14.22 seconds
;; VERIFY took 18.30 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
;; Reading the file took 1.24 seconds
;; Checking the proof took 6.53 seconds
;; VERIFY took 9.17 seconds
4374> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-4
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-4.proofs
;; Reading the file took 0.06 seconds
;; Checking the proofs took 0.00 seconds
;; 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.06 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.07 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.07 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.10 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.17 seconds
;; Checking the proof took 2.01 seconds
;; VERIFY took 2.41 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
;; Reading the file took 0.96 seconds
;; Checking the proof took 25.93 seconds
;; VERIFY took 30.76 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
;; Reading the file took 0.13 seconds
;; Checking the proof took 2.23 seconds
;; VERIFY took 2.67 seconds
4380> DEFINE BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.disjoined-associativity.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4381> VERIFY BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.disjoined-associativity.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.02 seconds
;; VERIFY took 0.04 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.15 seconds
;; Checking the proof took 4.24 seconds
;; VERIFY took 5.05 seconds
4384> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-associativity.proof
;; Reading the file took 1.10 seconds
;; Checking the proof took 33.92 seconds
;; VERIFY took 40.53 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 5.32 seconds
;; VERIFY took 6.40 seconds
4386> DEFINE BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/admit-build.disjoined-associativity-okp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.04 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.01 seconds
;; VERIFY took 0.02 seconds
4388> VERIFY BOOLEANP-OF-BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-associativity-okp.proof
;; Reading the file took 0.69 seconds
;; Checking the proof took 3.69 seconds
;; VERIFY took 5.29 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
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.61 seconds
;; VERIFY took 0.74 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
;; Reading the file took 0.66 seconds
;; Checking the proof took 27.26 seconds
;; VERIFY took 34.56 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
;; Reading the file took 0.51 seconds
;; Checking the proof took 14.44 seconds
;; VERIFY took 18.53 seconds
4392> VERIFY FORCING-SOUNDNESS-OF-BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.disjoined-associativity-okp.proof
;; Reading the file took 1.17 seconds
;; Checking the proof took 6.65 seconds
;; VERIFY took 9.27 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
;; DEFINE took 0.00 seconds
4394> VERIFY BUILD.DISJOINED-CUT-LEMMA-1
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-1.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4395> VERIFY BUILD.DISJOINED-CUT-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-1-under-iff.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.06 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.20 seconds
;; Checking the proof took 3.40 seconds
;; VERIFY took 4.24 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
;; Reading the file took 1.11 seconds
;; Checking the proof took 22.64 seconds
;; VERIFY took 28.70 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
;; Reading the file took 0.65 seconds
;; Checking the proof took 48.29 seconds
;; VERIFY took 59.76 seconds
4399> DEFINE BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/admit-build.disjoined-cut-lemma-2.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4400> VERIFY BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-2.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4401> VERIFY BUILD.DISJOINED-CUT-LEMMA-2-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 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.14 seconds
;; Checking the proof took 1.26 seconds
;; VERIFY took 1.61 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
;; Reading the file took 1.22 seconds
;; Checking the proof took 47.25 seconds
;; VERIFY took 58.58 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.17 seconds
;; Checking the proof took 1.58 seconds
;; VERIFY took 2.05 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
;; DEFINE took 0.01 seconds
4406> VERIFY BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/thm-build.disjoined-cut.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 sec

;;; Starting full GC,     563,216,384 bytes allocated.
;;; Finished full GC.     539,162,448 bytes freed in 0.285307 s

;;; 134 soft faults, 0 faults, 0 pageins

onds
;; VERIFY took 0.01 seconds
4407> VERIFY BUILD.DISJOINED-CUT-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-cut-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4408> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-cut.proof
;; Reading the file took 0.74 seconds
;; Checking the proof took 4.08 seconds
;; VERIFY took 5.59 seconds
4409> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-cut.proof
;; Reading the file took 1.74 seconds
;; Checking the proof took 54.51 seconds
;; VERIFY took 68.01 seconds
4410> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-cut.proof
;; Reading the file took 0.48 seconds
;; Checking the proof took 6.24 seconds
;; VERIFY took 7.92 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
;; 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.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4413> VERIFY BOOLEANP-OF-BUILD.DISJOINED-CUT-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-cut-okp.proof
;; Reading the file took 1.20 seconds
;; Checking the proof took 6.15 seconds
;; VERIFY took 8.91 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 0.84 seconds
;; VERIFY took 0.99 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
;; Reading the file took 1.09 seconds
;; Checking the proof took 58.63 seconds
;; VERIFY took 74.04 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
;; Reading the file took 0.67 seconds
;; Checking the proof took 25.26 seconds
;; VERIFY took 32.16 seconds
4417> VERIFY FORCING-SOUNDNESS-OF-BUILD.DISJOINED-CUT-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.disjoined-cut-okp.proof
;; Reading the file took 2.53 seconds
;; Checking the proof took 19.75 seconds
;; VERIFY took 26.59 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
;; 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4420> VERIFY BUILD.DISJOINED-MODUS-PONENS-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 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
;; Reading the file took 0.52 seconds
;; Checking the proof took 32.46 seconds
;; VERIFY took 39.20 seconds
4422> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-MODUS-PONENS
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-modus-ponens.proof
;; Reading the file took 2.85 seconds
;; Checking the proof took 72.36 seconds
;; VERIFY took 90.18 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
;; Reading the file took 0.66 seconds
;; Checking the proof took 65.59 seconds
;; VERIFY took 79.46 seconds
4424> DEFINE BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.04 seconds
4425> VERIFY BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4426> VERIFY BOOLEANP-OF-BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-modus-ponens-okp.proof
;; Reading the file took 0.60 seconds
;; Checking the proof took 3.29 seconds
;; VERIFY took 4.62 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.60 seconds
;; VERIFY took 0.71 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
;; Reading the file took 0.83 seconds
;; Checking the proof took 36.06 seconds
;; VERIFY took 45.43 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
;; Reading the file took 0.55 seconds
;; Checking the proof took 16.20 seconds
;; VERIFY took 20.53 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
;; Reading the file took 2.32 seconds
;; Checking the proof took 15.75 seconds
;; VERIFY took 21.33 seconds
4431> DEFINE BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-2.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4432> VERIFY BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4433> VERIFY BUILD.DISJOINED-MODUS-PONENS-2-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 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
;; Reading the file took 0.53 seconds
;; Checking the proof took 29.48 seconds
;; VERIFY took 35.47 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
;; Reading the file took 2.84 seconds
;; Checking the proof took 71.96 seconds
;; VERIFY took 89.40 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
;; Reading the file took 0.66 seconds
;; Checking the proof took 59.44 seconds
;; VERIFY took 71.71 seconds
4437> DEFINE BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-2-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.04 seconds
4438> VERIFY BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4439> VERIFY BOOLEANP-OF-BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-modus-ponens-2-okp.proof
;; Reading the file took 0.60 seconds
;; Checking the proof took 3.35 seconds
;; VERIFY took 4.72 seconds


;;; Starting full GC,     559,415,296 bytes allocated.
;;; Finished full GC.     531,818,256 bytes freed in 0.352469 s

;;; 16 soft faults, 0 faults, 0 pageins

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.03 seconds
;; Checking the proof took 0.63 seconds
;; VERIFY took 0.73 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
;; Reading the file took 1.22 seconds
;; Checking the proof took 35.97 seconds
;; VERIFY took 45.47 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
;; Reading the file took 0.53 seconds
;; Checking the proof took 18.37 seconds
;; VERIFY took 23.11 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
;; Reading the file took 2.28 seconds
;; Checking the proof took 15.85 seconds
;; VERIFY took 21.34 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
;; DEFINE took 0.00 seconds
4445> VERIFY BUILD.LHS-COMMUTE-OR-THEN-RASSOC
;; Reading from Proofs/level2/thm-build.lhs-commute-or-then-rassoc.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.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.01 seconds
;; Checking the proof took 0.03 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.11 seconds
;; Checking the proof took 1.69 seconds
;; VERIFY took 2.00 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
;; Reading the file took 0.42 seconds
;; Checking the proof took 14.24 seconds
;; VERIFY took 16.42 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.12 seconds
;; Checking the proof took 2.26 seconds
;; VERIFY took 2.68 seconds
4450> DEFINE BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP
;; Reading from Proofs/level2/admit-build.lhs-commute-or-then-rassoc-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4451> VERIFY BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP
;; Reading from Proofs/level2/thm-build.lhs-commute-or-then-rassoc-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4452> VERIFY BOOLEANP-OF-BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.lhs-commute-or-then-rassoc-okp.proof
;; Reading the file took 0.38 seconds
;; Checking the proof took 1.80 seconds
;; VERIFY took 2.56 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.42 seconds
;; VERIFY took 0.49 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
;; Reading the file took 0.49 seconds
;; Checking the proof took 13.84 seconds
;; VERIFY took 17.46 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
;; Reading the file took 0.45 seconds
;; Checking the proof took 8.24 seconds
;; VERIFY took 10.51 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
;; Reading the file took 0.95 seconds
;; Checking the proof took 4.54 seconds
;; VERIFY took 6.34 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
;; 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.00 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.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 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
;; Reading the file took 0.11 seconds
;; Checking the proof took 1.77 seconds
;; VERIFY took 2.08 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
;; Reading the file took 0.42 seconds
;; Checking the proof took 14.74 seconds
;; VERIFY took 16.93 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.18 seconds
;; Checking the proof took 2.30 seconds
;; VERIFY took 2.77 seconds
4463> DEFINE RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle-bldr-okp.proofs
;; Reading the file took 0.06 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.08 seconds
4464> VERIFY RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr-okp.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.06 seconds
4465> VERIFY BOOLEANP-OF-RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-rw.crewrite-twiddle-bldr-okp.proof
;; Reading the file took 0.45 seconds
;; Checking the proof took 1.83 seconds
;; VERIFY took 2.67 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.05 seconds
;; Checking the proof took 0.44 seconds
;; VERIFY took 0.53 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
;; Reading the file took 0.51 seconds
;; Checking the proof took 14.33 seconds
;; VERIFY took 18.06 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.50 seconds
;; Checking the proof took 8.32 seconds
;; VERIFY took 10.68 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
;; Reading the file took 0.97 seconds
;; Checking the proof took 4.39 seconds
;; VERIFY took 6.21 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
;; DEFINE took 0.00 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.00 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.03 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.17 seconds
;; Checking the proof took 12.99 seconds
;; VERIFY took 14.87 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
;; Reading the file took 1.16 seconds
;; Checking the proof took 98.96 seconds
;; VERIFY took 114.34 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.19 seconds
;; Checking the proof took 19.60 seconds
;; VERIFY took 22.59 seconds
4476> DEFINE RW.CREWRITE-TWIDDLE2-BLDR
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-bldr.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4477> VERIFY RW.CREWRITE-TWIDDLE2-BLDR
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.03 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.15 seconds
;; Checking the proof took 7.74 seconds
;; VERIFY took 8.94 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
;; Reading the file took 1.22 seconds
;; Checking the proof took 105.53 seconds
;; VERIFY took 122.25 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.18 seconds
;; Checking the proof took 10.36 seconds
;; VERIFY took 12.01 seconds
4482> DEFINE RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-bldr-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.04 seconds
4483> VERIFY RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-bldr-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4484> VERIFY BOOLEANP-OF-RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-rw.crewrite-twiddle2-bldr-okp.proof
;; Reading the file took 0.68 seconds
;; Checking the proof took 3.81 seconds
;; VERIFY took 5.40 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.63 seconds
;; VERIFY took 0.74 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
;; Reading the file took 0.64 seconds
;; Checking the proof took 27.85 seconds
;; VERIFY took 34.95 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
;; Reading the file took 0.52 seconds
;; Checking the proof took 15.11 seconds
;; VERIFY took 19.16 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
;; Reading the file took 1.28 seconds
;; Checking the proof took 6.91 seconds
;; VERIFY took 9.57 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
;; DEFINE took 0.01 seconds
4490> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-lemma-1.proof
;; Reading the file took 0.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.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 seconds
4492> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle-lemma-1.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 28.80 seconds
;; VERIFY took 33.64 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
;; Reading the file took 1.28 seconds
;; Checking the proof took 60.08 seconds
;; VERIFY took 72.33 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
;; Reading the file took 0.68 seconds
;; Checking the proof took 149.36 seconds
;; VERIFY took 176.31 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
;; DEFINE took 0.01 seconds
4496> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4497> VERIFY CLAUSE.AUX-SPLIT-TWID

;;; Starting full GC,     564,527,104 bytes allocated.
;;; Finished full GC.     538,046,240 bytes freed in 0.338685 s

;;; 23 soft faults, 0 faults, 0 pageins

DLE-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 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
;; Reading the file took 0.45 seconds
;; Checking the proof took 10.34 seconds
;; VERIFY took 12.38 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
;; Reading the file took 1.14 seconds
;; Checking the proof took 14.67 seconds
;; VERIFY took 18.43 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
;; Reading the file took 0.71 seconds
;; Checking the proof took 78.77 seconds
;; VERIFY took 93.47 seconds
4501> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE-OKP
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle-okp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; 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.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4503> VERIFY BOOLEANP-OF-CLAUSE.AUX-SPLIT-TWIDDLE-OKP
;; Reading from Proofs/level2/thm-booleanp-of-clause.aux-split-twiddle-okp.proof
;; Reading the file took 0.59 seconds
;; Checking the proof took 3.16 seconds
;; VERIFY took 4.45 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.03 seconds
;; Checking the proof took 0.60 seconds
;; VERIFY took 0.70 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
;; Reading the file took 0.62 seconds
;; Checking the proof took 28.37 seconds
;; VERIFY took 35.82 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
;; Reading the file took 0.50 seconds
;; Checking the proof took 19.66 seconds
;; VERIFY took 24.66 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
;; Reading the file took 1.47 seconds
;; Checking the proof took 10.43 seconds
;; VERIFY took 13.97 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
;; 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.01 seconds
;; Checking the proof took 0.03 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.14 seconds
;; Checking the proof took 3.01 seconds
;; VERIFY took 3.59 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
;; Reading the file took 1.25 seconds
;; Checking the proof took 27.16 seconds
;; VERIFY took 32.48 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.18 seconds
;; Checking the proof took 4.85 seconds
;; VERIFY took 5.83 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
;; DEFINE took 0.00 seconds
4515> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-1.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.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.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 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.17 seconds
;; Checking the proof took 10.15 seconds
;; VERIFY took 11.59 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
;; Reading the file took 1.22 seconds
;; Checking the proof took 84.99 seconds
;; VERIFY took 100.33 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
;; Reading the file took 0.75 seconds
;; Checking the proof took 101.50 seconds
;; VERIFY took 119.77 seconds
4520> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-lemma-2a.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4521> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2a.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4522> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2a-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 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.20 seconds
;; Checking the proof took 11.52 seconds
;; VERIFY took 13.55 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
;; Reading the file took 1.05 seconds
;; Checking the proof took 35.20 seconds
;; VERIFY took 41.79 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
;; Reading the file took 0.29 seconds
;; Checking the proof took 19.19 seconds
;; VERIFY took 22.88 seconds
4526> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-lemma-2.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4527> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.03 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.16 seconds
;; Checking the proof took 10.63 seconds
;; VERIFY took 12.12 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
;; Reading the file took 0.94 seconds
;; Checking the proof took 111.39 seconds
;; VERIFY took 128.33 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
;; Reading the file took 0.21 seconds
;; Checking the proof took 15.20 seconds
;; VERIFY took 17.51 seconds
4532> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4533> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4534> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 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
;; Reading the file took 0.50 seconds
;; Checking the proof took 18.97 seconds
;; VERIFY took 21.95 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
;; Reading the file took 0.97 seconds
;; Checking the proof took 24.02 seconds
;; VERIFY took 28.44 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
;; Reading the file took 1.20 seconds
;; Checking the proof took 93.76 seconds
;; VERIFY took 109.73 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
;; DEFINE took 0.04 seconds
4539> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-OKP
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4540> VERIFY BOOLEANP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-OKP
;; Reading from Proofs/level2/thm-booleanp-of-clause.aux-split-twiddle2-okp.proof
;; Reading the file took 0.68 seconds
;; Checking the proof took 3.98 seconds
;; VERIFY took 5.56 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
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.68 seconds
;; VERIFY took 0.79 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
;; Reading the file took 0.66 seconds
;; Checking the proof took 28.86 seconds
;; VERIFY took 35.97 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
;; Reading the file took 0.51 seconds
;; Checking the proof took 15.83 seconds
;; VERIFY took 19.86 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
;; Reading the file took 1.16 seconds
;; Checking the proof took 7.31 seconds
;; VERIFY took 9.86 seconds
4545> DEFINE CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR
;; Reading from Proofs/level2/admit-clause.aux-split-default-3-bldr.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4546> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4547> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr-under-iff.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.11 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.12 seconds
;; Checking the proof took 2.52 seconds
;; VERIFY took 2.94 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
;; Reading the file took 0.75

;;; Starting full GC,     563,478,528 bytes allocated.
;;; Finished full GC.     541,589,216 bytes freed in 0.296795 s

;;; 0 soft faults, 0 faults, 0 pageins

 seconds
;; Checking the proof took 20.73 seconds
;; VERIFY took 24.44 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
;; Reading the file took 0.47 seconds
;; Checking the proof took 18.49 seconds
;; VERIFY took 21.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
;; DEFINE took 0.02 seconds
4552> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4553> VERIFY BOOLEANP-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-clause.aux-split-default-3-bldr-okp.proof
;; Reading the file took 0.38 seconds
;; Checking the proof took 1.93 seconds
;; VERIFY took 2.68 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.07 seconds
;; Checking the proof took 0.47 seconds
;; VERIFY took 0.60 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
;; Reading the file took 0.50 seconds
;; Checking the proof took 14.98 seconds
;; VERIFY took 18.64 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
;; Reading the file took 0.42 seconds
;; Checking the proof took 8.58 seconds
;; VERIFY took 10.79 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
;; Reading the file took 0.94 seconds
;; Checking the proof took 4.72 seconds
;; VERIFY took 6.52 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
;; DEFINE took 0.00 seconds
4559> VERIFY CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR
;; Reading from Proofs/level2/thm-clause.aux-limsplit-cutoff-step-bldr.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.01 seconds
;; Checking the proof took 0.03 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.11 seconds
;; Checking the proof took 1.84 seconds
;; VERIFY took 2.15 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
;; Reading the file took 0.42 seconds
;; Checking the proof took 15.10 seconds
;; VERIFY took 17.28 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.13 seconds
;; Checking the proof took 2.52 seconds
;; VERIFY took 2.95 seconds
4564> DEFINE CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-OKP
;; Reading from Proofs/level2/admit-clause.aux-limsplit-cutoff-step-bldr-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 seconds
4565> VERIFY CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-OKP
;; Reading from Proofs/level2/thm-clause.aux-limsplit-cutoff-step-bldr-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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
;; Reading the file took 0.39 seconds
;; Checking the proof took 1.94 seconds
;; VERIFY took 2.72 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.48 seconds
;; VERIFY took 0.56 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
;; Reading the file took 0.52 seconds
;; Checking the proof took 15.34 seconds
;; VERIFY took 19.06 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
;; Reading the file took 0.42 seconds
;; Checking the proof took 8.78 seconds
;; VERIFY took 11.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
;; Reading the file took 0.97 seconds
;; Checking the proof took 4.80 seconds
;; VERIFY took 6.60 seconds
4571> DEFINE LEVEL2.STEP-OKP
;; Reading from Proofs/level2/admit-level2.step-okp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4572> VERIFY LEVEL2.STEP-OKP
;; Reading from Proofs/level2/thm-level2.step-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4573> VERIFY SOUNDNESS-OF-LEVEL2.STEP-OKP
;; Reading from Proofs/level2/thm-soundness-of-level2.step-okp.proof
;; Reading the file took 0.61 seconds
;; Checking the proof took 3.47 seconds
;; VERIFY took 4.86 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
;; Reading the file took 2.09 seconds
;; Checking the proof took 16.83 seconds
;; VERIFY took 22.79 seconds
4575> VERIFY LEVEL2.STEP-OKP-WHEN-NOT-CONSP
;; Reading from Proofs/level2/thm-level2.step-okp-when-not-consp.proof
;; Reading the file took 0.52 seconds
;; Checking the proof took 3.72 seconds
;; VERIFY took 4.76 seconds
4576> DEFINE LEVEL2.FLAG-PROOFP
;; Reading from Proofs/level2/admit-level2.flag-proofp.proofs
;; Reading the file took 0.45 seconds
;; Checking the proofs took 1.53 seconds
;; DEFINE took 2.16 seconds
4577> VERIFY LEVEL2.FLAG-PROOFP
;; Reading from Proofs/level2/thm-level2.flag-proofp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4578> DEFINE LEVEL2.PROOFP
;; Reading from Proofs/level2/admit-level2.proofp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 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.01 seconds
;; Checking the proofs took 0.00 seconds
;; 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.05 seconds
;; Checking the proof took 0.16 seconds
;; VERIFY took 0.22 seconds
4583> VERIFY DEFINITION-OF-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-definition-of-level2.proof-listp.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.28 seconds
;; VERIFY took 0.40 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.09 seconds
;; VERIFY took 0.12 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.02 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.10 seconds
4586> VERIFY LEVEL2.PROOF-LISTP-OF-CONS
;; Reading from Proofs/level2/thm-level2.proof-listp-of-cons.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.13 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
;; Reading the file took 1.01 seconds
;; Checking the proof took 3.98 seconds
;; VERIFY took 5.42 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.19 seconds
;; VERIFY took 0.24 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.17 seconds
;; VERIFY took 0.23 seconds
4590> VERIFY LEVEL2.PROOF-LISTP-OF-LIST-FIX
;; Reading from Proofs/level2/thm-level2.proof-listp-of-list-fix.proof
;; Reading the file took 0.47 seconds
;; Checking the proof took 1.47 seconds
;; VERIFY took 2.12 seconds
4591> VERIFY LEVEL2.PROOF-LISTP-OF-APP
;; Reading from Proofs/level2/thm-level2.proof-listp-of-app.proof
;; Reading the file took 0.98 seconds
;; Checking the proof took 2.84 seconds
;; VERIFY took 4.26 seconds
4592> VERIFY LEVEL2.PROOF-LISTP-OF-REV
;; Reading from Proofs/level2/thm-level2.proof-listp-of-rev.proof
;; Reading the file took 0.49 seconds
;; Checking the proof took 1.60 seconds
;; VERIFY took 2.28 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.10 seconds
;; Checking the proof took 0.29 seconds
;; VERIFY took 0.41 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.19 seconds
;; VERIFY took 0.27 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
;; Reading the file took 0.36 seconds
;; Checking the proof took 1.27 seconds
;; VERIFY took 1.76 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.08 seconds
;; Checking the proof took 0.14 seconds
;; VERIFY took 0.24 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
;; Reading the file took 0.30 seconds
;; Checking the proof took 1.14 seconds
;; VERIFY took 1.55 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.62 seconds
;; Checking the proof took 1.76 seconds
;; VERIFY took 2.61 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.31 seconds
;; Checking the proof took 1.16 seconds
;; VERIFY took 1.58 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
;; Reading the file took 0.40 seconds
;; Checking the proof took 1.39 seconds
;; VERIFY took 1.95 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.03 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.11 seconds
4602> VERIFY LEVEL2.PROOF-LISTP-OF-REPEAT
;; Reading from Proofs/level2/thm-level2.proof-listp-of-repeat.proof
;; Reading the file took 0.32 seconds
;; Checking the proof took 1.23 seconds
;; VERIFY took 1.68 seconds
4603> VERIFY LEMMA-FOR-LOGIC.PROVABLEP-WHEN-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-lemma-for-logic.provablep-when-level2.proofp.proof
;; Reading the file took 42.84 seconds
;; Checking the proof took 16.79 seconds
;; VERIFY took 62.05 seconds
4604> VERIFY LOGIC.PROVABLEP-WHEN-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-logic.provablep-when-level2.proofp.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 0.48 seconds
;; VERIFY took 0.69 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.13 seconds
;; Checking the proof took 0.49 seconds
;; VERIFY took 0.69 seconds
4606> VERIFY LEMMA-FOR-LEVEL2.PROOFP-WHEN-LOGIC.PROOFP
;; Reading from Proofs/level2/thm-lemma-for-level2.proofp-when-logic.proofp.proof
;; Reading the file took 1.45 seconds
;; Checking the proof took 5.33 seconds
;; VERIFY took 7.49 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.25 seconds
;; VERIFY took 0.34 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.06 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 0.34 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.02 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.09 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.07 seconds
;; VERIFY took 0.10 seconds
4611 > SWITCH LEVEL2.PROOFP
;; SWITCH took 0.00 seconds
4612 > FINISH level2


;;; Starting full GC,     537,919,488 bytes allocated.
;;; Finished full GC.     517,930,816 bytes freed in 0.286724 s

;;; 38 soft faults, 0 faults, 0 pageins



;;; Starting full GC,      19,988,672 bytes allocated.
;;; Finished full GC.               0 bytes freed in 0.070074 s

;;; 0 soft faults, 0 faults, 0 pageins


real	77m23.201s
user	76m49.912s
sys	0m2.108s