Milawa Proof Checker.
4010> DEFINE BUILD.AXIOM
;; Reading from Proofs/level2/admit-build.axiom.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4011> VERIFY BUILD.AXIOM
;; Reading from Proofs/level2/thm-build.axiom.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.004 seconds
4012> VERIFY BUILD.AXIOM-UNDER-IFF
;; Reading from Proofs/level2/thm-build.axiom-under-iff.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4013> VERIFY LOGIC.METHOD-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.method-of-build.axiom.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4014> VERIFY LOGIC.CONCLUSION-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.axiom.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4015> VERIFY LOGIC.SUBPROOFS-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.axiom.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4016> VERIFY LOGIC.EXTRAS-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.extras-of-build.axiom.proof
;; Reading the file took 0.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4017> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.axiom.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 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.02 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.28 seconds
4019> DEFINE BUILD.THEOREM
;; Reading from Proofs/level2/admit-build.theorem.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.003 seconds
4020> VERIFY BUILD.THEOREM
;; Reading from Proofs/level2/thm-build.theorem.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.003 seconds
4021> VERIFY BUILD.THEOREM-UNDER-IFF
;; Reading from Proofs/level2/thm-build.theorem-under-iff.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4022> VERIFY LOGIC.METHOD-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.method-of-build.theorem.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.005 seconds
;; VERIFY took 0.01 seconds
4023> VERIFY LOGIC.CONCLUSION-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.theorem.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4024> VERIFY LOGIC.SUBPROOFS-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.theorem.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4025> VERIFY LOGIC.EXTRAS-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.extras-of-build.theorem.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4026> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.theorem.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 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.03 seconds
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.29 seconds
4028> DEFINE BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/admit-build.propositional-schema.proofs
;; Reading the file took 0.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.004 seconds
4029> VERIFY BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-build.propositional-schema.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.004 seconds
4030> VERIFY BUILD.PROPOSITIONAL-SCHEMA-UNDER-IFF
;; Reading from Proofs/level2/thm-build.propositional-schema-under-iff.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.003 seconds
;; Checking the proof took 0.005 seconds
;; VERIFY took 0.01 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.004 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.02 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.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.07 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.02 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.32 seconds
4037> DEFINE BUILD.CUT
;; Reading from Proofs/level2/admit-build.cut.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.005 seconds
4038> VERIFY BUILD.CUT
;; Reading from Proofs/level2/thm-build.cut.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.005 seconds
4039> VERIFY BUILD.CUT-UNDER-IFF
;; Reading from Proofs/level2/thm-build.cut-under-iff.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4040> VERIFY LOGIC.METHOD-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-logic.method-of-build.cut.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4041> VERIFY LOGIC.CONCLUSION-OF-CUT
;; Reading from Proofs/level2/thm-logic.conclusion-of-cut.proof
;; Reading the file took 0.004 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4042> VERIFY LOGIC.SUBPROOFS-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.cut.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 seconds
4043> VERIFY LOGIC.EXTRAS-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-logic.extras-of-build.cut.proof
;; Reading the file took 0.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4044> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.cut.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.29 seconds
;; VERIFY took 0.46 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.10 seconds
;; Checking the proof took 1.15 seconds
;; VERIFY took 1.90 seconds
4046> DEFINE BUILD.CONTRACTION
;; Reading from Proofs/level2/admit-build.contraction.proofs
;; Reading the file took 0.003 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4047> VERIFY BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-build.contraction.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.002 seconds
4048> VERIFY BUILD.CONTRACTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.contraction-under-iff.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4049> VERIFY LOGIC.METHOD-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.method-of-build.contraction.proof
;; Reading the file took 0.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4050> VERIFY LOGIC.CONCLUSION-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.contraction.proof
;; Reading the file took 0.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4051> VERIFY LOGIC.SUBPROOFS-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.contraction.proof
;; Reading the file took 0.004 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4052> VERIFY LOGIC.EXTRAS-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.extras-of-build.contraction.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.02 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.17 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.05 seconds
;; Checking the proof took 0.36 seconds
;; VERIFY took 0.57 seconds
4055> DEFINE BUILD.EXPANSION
;; Reading from Proofs/level2/admit-build.expansion.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4056> VERIFY BUILD.EXPANSION
;; Reading from Proofs/level2/thm-build.expansion.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.004 seconds
4057> VERIFY BUILD.EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.expansion-under-iff.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4058> VERIFY LOGIC.METHOD-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.method-of-build.expansion.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4059> VERIFY LOGIC.CONCLUSION-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.expansion.proof
;; Reading the file took 0.005 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4060> VERIFY LOGIC.SUBPROOFS-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.expansion.proof
;; Reading the file took 0.004 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4061> VERIFY LOGIC.EXTRAS-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.extras-of-build.expansion.proof
;; Reading the file took 0.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4062> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.expansion.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.13 seconds
4063> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.expansion.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.25 seconds
;; VERIFY took 0.38 seconds
4064> DEFINE BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.associativity.proofs
;; Reading the file took 0.003 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.01 seconds
;; Checking the proof took 0.001 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4067> VERIFY LOGIC.METHOD-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.method-of-build.associativity.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4068> VERIFY LOGIC.CONCLUSION-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.associativity.proof
;; Reading the file took 0.005 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 seconds
4069> VERIFY LOGIC.SUBPROOFS-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.associativity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4070> VERIFY LOGIC.EXTRAS-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.extras-of-build.associativity.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.03 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 0.36 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.06 seconds
;; Checking the proof took 0.71 seconds
;; VERIFY took 1.08 seconds
4073> DEFINE BUILD.INSTANTIATION
;; Reading from Proofs/level2/admit-build.instantiation.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.005 seconds
4074> VERIFY BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-build.instantiation.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.005 seconds
4075> VERIFY BUILD.INSTANTIATION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.instantiation-under-iff.proof
;; Reading the file took 0.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4076> VERIFY LOGIC.METHOD-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.method-of-build.instantiation.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.15 seconds
4077> VERIFY LOGIC.CONCLUSION-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.instantiation.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.07 seconds
4078> VERIFY LOGIC.SUBPROOFS-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.instantiation.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.36 seconds
;; VERIFY took 0.58 seconds
4079> VERIFY LOGIC.EXTRAS-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.extras-of-build.instantiation.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.14 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.03 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.25 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.07 seconds
;; Checking the proof took 0.58 seconds
;; VERIFY took 0.95 seconds
4082> DEFINE BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/admit-build.functional-equality.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.004 seconds
4083> VERIFY BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-build.functional-equality.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.003 seconds
4084> VERIFY BUILD.FUNCTIONAL-EQUALITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.functional-equality-under-iff.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4085> VERIFY LOGIC.METHOD-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-logic.method-of-build.functional-equality.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.02 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.17 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.07 seconds
;; Checking the proof took 0.62 seconds
;; VERIFY took 1.00 seconds
4091> DEFINE BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/admit-build.beta-reduction.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.003 seconds
4092> VERIFY BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-build.beta-reduction.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.003 seconds
4093> VERIFY BUILD.BETA-REDUCTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.beta-reduction-under-iff.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.03 seconds
;; VERIFY took 0.04 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.01 seconds
;; VERIFY took 0.02 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.05 seconds
;; Checking the proof took 0.34 seconds
;; VERIFY took 0.53 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.12 seconds
;; Checking the proof took 1.01 seconds
;; VERIFY took 1.67 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.004 seconds
4101> VERIFY BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-build.base-eval.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.005 seconds
4102> VERIFY BUILD.BASE-EVAL-UNDER-IFF
;; Reading from Proofs/level2/thm-build.base-eval-under-iff.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.10 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.05 seconds
;; Checking the proof took 0.26 seconds
;; VERIFY took 0.41 seconds
4109> DEFINE BUILD.INSTANTIATION-LIST
;; Reading from Proofs/level2/admit-build.instantiation-list.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.07 seconds
;; DEFINE took 0.10 seconds
4110> VERIFY BUILD.INSTANTIATION-LIST
;; Reading from Proofs/level2/thm-build.instantiation-list.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.003 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.005 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4112> VERIFY BUILD.INSTANTIATION-LIST-OF-CONS
;; Reading from Proofs/level2/thm-build.instantiation-list-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 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.13 seconds
;; Checking the proof took 0.79 seconds
;; VERIFY took 1.26 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.10 seconds
;; Checking the proof took 0.75 seconds
;; VERIFY took 1.18 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.16 seconds
;; Checking the proof took 1.07 seconds
;; VERIFY took 1.75 seconds
4116> DEFINE BUILD.INDUCTION
;; Reading from Proofs/level2/admit-build.induction.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.004 seconds
4117> VERIFY BUILD.INDUCTION
;; Reading from Proofs/level2/thm-build.induction.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.004 seconds
4118> VERIFY BUILD.INDUCTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.induction-under-iff.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4119> VERIFY LOGIC.METHOD-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-logic.method-of-build.induction.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4120> VERIFY LOGIC.CONCLUSION-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.induction.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4121> VERIFY LOGIC.SUBPROOFS-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.induction.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4122> VERIFY LOGIC.EXTRAS-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-logic.extras-of-build.induction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.09 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.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.09 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.21 seconds
;; Checking the proof took 2.46 seconds
;; VERIFY took 4.21 seconds
4125> DEFINE BUILD.COMMUTE-OR
;; Reading from Proofs/level2/admit-build.commute-or.proofs
;; Reading the file took 0.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.005 seconds
4126> VERIFY BUILD.COMMUTE-OR
;; Reading from Proofs/level2/thm-build.commute-or.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.003 seconds
4127> VERIFY BUILD.COMMUTE-OR-UNDER-IFF
;; Reading from Proofs/level2/thm-build.commute-or-under-iff.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.05 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.24 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.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.05 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.03 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.25 seconds
4131> DEFINE BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/admit-build.commute-or-okp.proofs
;; Reading the file took 0.004 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4132> VERIFY BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-build.commute-or-okp.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.003 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.08 seconds
;; Checking the proof took 0.58 seconds
;; VERIFY took 0.93 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.01 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.24 seconds
4135> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.commute-or-okp.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 5.02 seconds
;; VERIFY took 7.92 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.12 seconds
;; Checking the proof took 3.18 seconds
;; VERIFY took 5.02 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.26 seconds
;; Checking the proof took 1.81 seconds
;; VERIFY took 3.11 seconds
4138> DEFINE BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/admit-build.right-expansion.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.004 seconds
4139> VERIFY BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-build.right-expansion.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.003 seconds
4140> VERIFY BUILD.RIGHT-EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.right-expansion-under-iff.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.01 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.08 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.04 seconds
;; Checking the proof took 0.30 seconds
;; VERIFY took 0.44 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.02 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.15 seconds
4144> DEFINE BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/admit-build.right-expansion-okp.proofs
;; Reading the file took 0.001 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.002 seconds
;; Checking the proof took 0.002 seconds
;; VERIFY took 0.005 seconds
4146> VERIFY BOOLEANP-OF-BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.right-expansion-okp.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.39 seconds
;; VERIFY took 0.64 seconds
4147> VERIFY BUILD.RIGHT-EXPANSION-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.right-expansion-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.17 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.23 seconds
;; Checking the proof took 7.64 seconds
;; VERIFY took 12.12 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.11 seconds
;; Checking the proof took 1.72 seconds
;; VERIFY took 2.76 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.21 seconds
;; Checking the proof took 1.29 seconds
;; VERIFY took 2.24 seconds
4151> DEFINE BUILD.MODUS-PONENS
;; Reading from Proofs/level2/admit-build.modus-ponens.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.004 seconds
4152> VERIFY BUILD.MODUS-PONENS
;; Reading from Proofs/level2/thm-build.modus-ponens.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.003 seconds
4153> VERIFY BUILD.MODUS-PONENS-UNDER-IFF
;; Reading from Proofs/level2/thm-build.modus-ponens-under-iff.proof
;; Reading the file took 0.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.04 seconds
;; Checking the proof took 0.55 seconds
;; VERIFY took 0.84 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.10 seconds
;; Checking the proof took 0.72 seconds
;; VERIFY took 1.16 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.14 seconds
;; Checking the proof took 6.72 seconds
;; VERIFY took 10.41 seconds
4157> DEFINE BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/admit-build.modus-ponens-okp.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4158> VERIFY BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-build.modus-ponens-okp.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.003 seconds
;; VERIFY took 0.01 seconds
4159> VERIFY BOOLEANP-OF-BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.modus-ponens-okp.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.71 seconds
;; VERIFY took 1.10 seconds
4160> VERIFY BUILD.MODUS-PONENS-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.modus-ponens-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.23 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.22 seconds
;; Checking the proof took 9.37 seconds
;; VERIFY took 14.43 seconds
4162> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.modus-ponens-okp.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 4.41 seconds
;; VERIFY took 6.78 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 0.49 seconds
;; Checking the proof took 5.60 seconds
;; VERIFY took 9.20 seconds
4164> DEFINE BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/admit-build.modus-ponens-2.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.004 seconds
4165> VERIFY BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/thm-build.modus-ponens-2.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.003 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.04 seconds
;; Checking the proof took 0.59 seconds
;; VERIFY took 0.90 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.01 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.09 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.14 seconds
;; Checking the proof took 7.51 seconds
;; VERIFY took 11.59 seconds
4170> DEFINE BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/admit-build.modus-ponens-2-okp.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4171> VERIFY BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-build.modus-ponens-2-okp.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.003 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.07 seconds
;; Checking the proof took 0.70 seconds
;; VERIFY took 1.07 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.01 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.28 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.25 seconds
;; Checking the proof took 9.25 seconds
;; VERIFY took 14.30 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.14 seconds
;; Checking the proof took 5.38 seconds
;; VERIFY took 8.19 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 0.55 seconds
;; Checking the proof took 5.56 seconds
;; VERIFY took 9.19 seconds
4177> DEFINE BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.right-associativity.proofs
;; Reading the file took 0.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.004 seconds
4178> VERIFY BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.right-associativity.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.003 seconds
4179> VERIFY BUILD.RIGHT-ASSOCIATIVITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.right-associativity-under-iff.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.04 seconds
;; Checking the proof took 2.23 seconds
;; VERIFY took 3.27 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.31 seconds
;; Checking the proof took 20.54 seconds
;; VERIFY took 29.59 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.06 seconds
;; Checking the proof took 3.70 seconds
;; VERIFY took 5.45 seconds
4183> DEFINE BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/admit-build.right-associativity-okp.proofs
;; Reading the file took 0.005 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.06 seconds
4184> VERIFY BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-build.right-associativity-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.004 seconds
;; VERIFY took 0.02 seconds
4185> VERIFY BOOLEANP-OF-BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.right-associativity-okp.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 1.71 seconds
;; VERIFY took 2.69 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.01 seconds
;; Checking the proof took 0.33 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.18 seconds
;; Checking the proof took 13.14 seconds
;; VERIFY took 20.45 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.17 seconds
;; Checking the proof took 7.55 seconds
;; VERIFY took 11.76 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.34 seconds
;; Checking the proof took 3.42 seconds
;; VERIFY took 5.66 seconds
4190> DEFINE BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/admit-build.disjoined-left-expansion.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4191> VERIFY BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/thm-build.disjoined-left-expansion.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.005 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.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4193> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-left-expansion.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 0.42 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.17 seconds
;; Checking the proof took 2.92 seconds
;; VERIFY took 4.30 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.04 seconds
;; Checking the proof took 0.47 seconds
;; VERIFY took 0.74 seconds
4196> DEFINE BUILD.DISJOINED-LEFT-EXPANSION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-left-expansion-okp.proofs
;; Reading the file took 0.001 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.002 seconds
;; Checking the proof took 0.004 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.13 seconds
;; Checking the proof took 1.34 seconds
;; VERIFY took 2.16 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.01 seconds
;; Checking the proof took 0.26 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.35 seconds
;; Checking the proof took 18.50 seconds
;; VERIFY took 28.96 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.14 seconds
;; Checking the proof took 4.68 seconds
;; VERIFY took 7.33 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 0.40 seconds
;; Checking the proof took 3.12 seconds
;; VERIFY took 5.25 seconds
4203> DEFINE BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/admit-build.disjoined-right-expansion.proofs
;; Reading the file took 0.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.005 seconds
4204> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-build.disjoined-right-expansion.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.004 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.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
4206> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-right-expansion.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 1.08 seconds
;; VERIFY took 1.64 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.25 seconds
;; Checking the proof took 5.32 seconds
;; VERIFY took 7.92 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.05 seconds
;; Checking the proof took 1.91 seconds
;; VERIFY took 2.94 seconds
4209> DEFINE BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-right-expansion-okp.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4210> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-build.disjoined-right-expansion-okp.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.003 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.13 seconds
;; Checking the proof took 1.33 seconds
;; VERIFY took 2.15 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.01 seconds
;; Checking the proof took 0.26 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.33 seconds
;; Checking the proof took 18.65 seconds
;; VERIFY took 29.13 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.14 seconds
;; Checking the proof took 4.77 seconds
;; VERIFY took 7.42 seconds
4215> VERIFY FORCING-SOUNDNESS-OF-BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-build.disjoined-right-expansion-okp.proof
;; Reading the file took 0.39 seconds
;; Checking the proof took 3.21 seconds
;; VERIFY took 5.35 seconds
4216> DEFINE BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/admit-build.disjoined-contraction.proofs
;; Reading the file took 0.002 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.002 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.005 seconds
4218> VERIFY BUILD.DISJOINED-CONTRACTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-contraction-under-iff.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 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.09 seconds
;; Checking the proof took 2.93 seconds
;; VERIFY took 4.39 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.08 seconds
;; Checking the proof took 0.72 seconds
;; VERIFY took 1.12 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.18 seconds
;; Checking the proof took 11.78 seconds
;; VERIFY took 17.61 seconds
4222> DEFINE BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-contraction-okp.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4223> VERIFY BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/thm-build.disjoined-contraction-okp.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.004 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.12 seconds
;; Checking the proof took 1.30 seconds
;; VERIFY took 2.05 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.01 seconds
;; Checking the proof took 0.30 seconds
;; VERIFY took 0.40 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.16 seconds
;; Checking the proof took 13.51 seconds
;; VERIFY took 20.81 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.16 seconds
;; Checking the proof took 10.03 seconds
;; VERIFY took 15.44 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 0.46 seconds
;; Checking the proof took 5.70 seconds
;; VERIFY took 9.25 seconds
4229> DEFINE BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/admit-build.cancel-neg-neg.proofs
;; Reading the file took 0.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.005 seconds
4230> VERIFY BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/thm-build.cancel-neg-neg.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.003 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.005 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.03 seconds
;; Checking the proof took 0.36 seconds
;; VERIFY took 0.54 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.09 seconds
;; Checking the proof took 2.00 seconds
;; VERIFY took 2.92 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.04 seconds
;; Checking the proof took 0.47 seconds
;; VERIFY took 0.70 seconds
4235> DEFINE BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/admit-build.cancel-neg-neg-okp.proofs
;; Reading the file took 0.001 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.001 seconds
;; Checking the proof took 0.002 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.04 seconds
;; Checking the proof took 0.44 seconds
;; VERIFY took 0.66 seconds
4238> VERIFY BUILD.CANCEL-NEG-NEG-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.cancel-neg-neg-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.28 seconds
4239> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.cancel-neg-neg-okp.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 4.33 seconds
;; VERIFY took 6.68 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.09 seconds
;; Checking the proof took 3.69 seconds
;; VERIFY took 5.63 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.31 seconds
;; Checking the proof took 2.85 seconds
;; VERIFY took 4.69 seconds
4242> DEFINE BUILD.INSERT-NEG-NEG
;; Reading from Proofs/level2/admit-build.insert-neg-neg.proofs
;; Reading the file took 0.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.005 seconds
4243> VERIFY BUILD.INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-build.insert-neg-neg.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.005 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.02 seconds
;; Checking the proof took 0.24 seconds
;; VERIFY took 0.36 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.07 seconds
;; Checking the proof took 0.87 seconds
;; VERIFY took 1.25 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.03 seconds
;; Checking the proof took 0.34 seconds
;; VERIFY took 0.51 seconds
4248> DEFINE BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/admit-build.insert-neg-neg-okp.proofs
;; Reading the file took 0.001 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.001 seconds
;; Checking the proof took 0.002 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.04 seconds
;; Checking the proof took 0.41 seconds
;; VERIFY took 0.61 seconds
4251> VERIFY BUILD.INSERT-NEG-NEG-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.insert-neg-neg-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.21 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.37 seconds
;; Checking the proof took 7.20 seconds
;; VERIFY took 11.25 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.12 seconds
;; Checking the proof took 1.80 seconds
;; VERIFY took 2.83 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.15 seconds
;; Checking the proof took 0.89 seconds
;; VERIFY took 1.54 seconds
4255> DEFINE BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/admit-build.lhs-insert-neg-neg.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4256> VERIFY BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.005 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4258> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.lhs-insert-neg-neg.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.52 seconds
;; VERIFY took 0.77 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.23 seconds
;; Checking the proof took 2.97 seconds
;; VERIFY took 4.32 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.05 seconds
;; Checking the proof took 1.00 seconds
;; VERIFY took 1.48 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.003 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.003 seconds
;; Checking the proof took 0.004 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.10 seconds
;; Checking the proof took 1.20 seconds
;; VERIFY took 1.88 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.29 seconds
;; VERIFY took 0.41 seconds
4265> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.LHS-INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.lhs-insert-neg-neg-okp.proof
;; Reading the file took 0.66 seconds
;; Checking the proof took 24.64 seconds
;; VERIFY took 38.25 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.16 seconds
;; Checking the proof took 4.86 seconds
;; VERIFY took 7.52 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.34 seconds
;; Checking the proof took 2.16 seconds
;; VERIFY took 3.65 seconds
4268> DEFINE BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/admit-build.merge-negatives.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4269> VERIFY BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/thm-build.merge-negatives.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.03 seconds
4270> VERIFY BUILD.MERGE-NEGATIVES-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-negatives-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 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.08 seconds
;; Checking the proof took 13.91 seconds
;; VERIFY took 20.54 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 0.44 seconds
;; Checking the proof took 34.65 seconds
;; VERIFY took 50.97 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.11 seconds
;; Checking the proof took 19.90 seconds
;; VERIFY took 29.94 seconds
4274> DEFINE BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/admit-build.merge-negatives-okp.proofs
;; Reading the file took 0.005 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.003 seconds
;; Checking the proof took 0.003 seconds
;; VERIFY took 0.01 seconds
4276> VERIFY BOOLEANP-OF-BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.merge-negatives-okp.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 1.29 seconds
;; VERIFY took 2.01 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.01 seconds
;; Checking the proof took 0.33 seconds
;; VERIFY took 0.42 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 0.26 seconds
;; Checking the proof took 11.71 seconds
;; VERIFY took 17.86 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.20 seconds
;; Checking the proof took 5.65 seconds
;; VERIFY took 8.64 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 0.50 seconds
;; Checking the proof took 4.35 seconds
;; VERIFY took 7.09 seconds
4281> DEFINE BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/admit-build.merge-implications-lemma-1.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.005 seconds
4282> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-1.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.12 seconds
4283> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-1-under-iff.proof
;; Reading the file took 0.004 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 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.07 seconds
;; Checking the proof took 13.24 seconds
;; VERIFY took 19.31 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 0.53 seconds
;; Checking the proof took 41.41 seconds
;; VERIFY took 60.56 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.08 seconds
;; Checking the proof took 22.99 seconds
;; VERIFY took 34.11 seconds
4287> DEFINE BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/admit-build.merge-implications-lemma-2.proofs
;; Reading the file took 0.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4288> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-2.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.001 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.005 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4290> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.merge-implications-lemma-2.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 11.06 seconds
;; VERIFY took 16.32 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.32 seconds
;; Checking the proof took 49.36 seconds
;; VERIFY took 73.97 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.11 seconds
;; Checking the proof took 13.78 seconds
;; VERIFY took 20.73 seconds
4293> DEFINE BUILD.MERGE-IMPLICATIONS
;; Reading from Proofs/level2/admit-build.merge-implications.proofs
;; Reading the file took 0.001 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.002 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.005 seconds
4295> VERIFY BUILD.MERGE-IMPLICATIONS-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-implications-under-iff.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 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.05 seconds
;; Checking the proof took 1.15 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.34 seconds
;; Checking the proof took 19.93 seconds
;; VERIFY took 29.85 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.05 seconds
;; Checking the proof took 1.51 seconds
;; VERIFY took 2.29 seconds
4299> DEFINE BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/admit-build.merge-implications-okp.proofs
;; Reading the file took 0.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.06 seconds
4300> VERIFY BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/thm-build.merge-implications-okp.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4301> VERIFY BOOLEANP-OF-BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.merge-implications-okp.proof
;; Reading the file took 0.30 seconds
;; Checking the proof took 5.15 seconds
;; VERIFY took 8.14 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.02 seconds
;; Checking the proof took 0.67 seconds
;; VERIFY took 0.87 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.42 seconds
;; Checking the proof took 43.94 seconds
;; VERIFY took 66.65 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.26 seconds
;; Checking the proof took 19.49 seconds
;; VERIFY took 29.43 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 0.80 seconds
;; Checking the proof took 13.03 seconds
;; VERIFY took 20.52 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.001 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.001 seconds
;; Checking the proof took 0.001 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.004 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 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.09 seconds
;; Checking the proof took 9.77 seconds
;; VERIFY took 14.38 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.34 seconds
;; Checking the proof took 24.47 seconds
;; VERIFY took 35.80 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.09 seconds
;; Checking the proof took 15.30 seconds
;; VERIFY took 22.75 seconds
4312> DEFINE BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/admit-build.disjoined-commute-or.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4313> VERIFY BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/thm-build.disjoined-commute-or.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.004 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.02 seconds
;; VERIFY took 0.04 seconds
4315> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-commute-or.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 13.17 seconds
;; VERIFY took 19.05 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.26 seconds
;; Checking the proof took 53.06 seconds
;; VERIFY took 74.48 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.31 seconds
;; Checking the proof took 16.16 seconds
;; VERIFY took 23.81 seconds
4318> DEFINE BUILD.DISJOINED-COMMUTE-OR-OKP
;; Reading from Proofs/level2/admit-build.disjoined-commute-or-okp.proofs
;; Reading the file took 0.001 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.001 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 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.13 seconds
;; Checking the proof took 1.78 seconds
;; VERIFY took 2.76 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.04 seconds
;; Checking the proof took 0.36 seconds
;; VERIFY took 0.51 seconds
4322> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.DISJOINED-COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.disjoined-commute-or-okp.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 14.19 seconds
;; VERIFY took 21.55 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.16 seconds
;; Checking the proof took 8.20 seconds
;; VERIFY took 12.42 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.41 seconds
;; Checking the proof took 3.69 seconds
;; VERIFY took 5.98 seconds
4325> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-1A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-1a.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.004 seconds
4326> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1A
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1a.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.005 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.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 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.06 seconds
;; Checking the proof took 7.09 seconds
;; VERIFY took 10.38 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.43 seconds
;; Checking the proof took 39.70 seconds
;; VERIFY took 58.00 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.10 seconds
;; Checking the proof took 12.57 seconds
;; VERIFY took 18.72 seconds
4331> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-1.proofs
;; Reading the file took 0.005 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4332> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.001 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 0.01 seconds
;; VERIFY took 0.03 seconds
4334> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-1.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 2.61 seconds
;; VERIFY took 3.81 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 0.31 seconds
;; Checking the proof took 12.00 seconds
;; VERIFY took 17.38 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.15 seconds
;; Checking the proof took 5.13 seconds
;; VERIFY took 7.74 seconds
4337> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-2a.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.04 seconds
4338> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2a.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.05 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.04 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.07 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.13 seconds
;; Checking the proof took 8.92 seconds
;; VERIFY took 13.24 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 0.36 seconds
;; Checking the proof took 27.04 seconds
;; VERIFY took 39.88 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.07 seconds
;; Checking the proof took 15.71 seconds
;; VERIFY took 23.57 seconds
4343> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-2
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-2.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4344> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.001 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.01 seconds
;; VERIFY took 0.03 seconds
4346> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-2.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 2.63 seconds
;; VERIFY took 3.83 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.33 seconds
;; Checking the proof took 12.27 seconds
;; VERIFY took 17.70 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.06 seconds
;; Checking the proof took 5.23 seconds
;; VERIFY took 7.75 seconds
4349> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-3A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-3a.proofs
;; Reading the file took 0.002 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.002 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.005 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4352> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-3A
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-3a.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 2.12 seconds
;; VERIFY took 3.07 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.24 seconds
;; Checking the proof took 3.95 seconds
;; VERIFY took 5.75 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.19 seconds
;; Checking the proof took 4.99 seconds
;; VERIFY took 7.46 seconds
4355> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-3
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-3.proofs
;; Reading the file took 0.001 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.001 seconds
;; Checking the proof took 0.002 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.003 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4358> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-3
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-3.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 2.04 seconds
;; VERIFY took 2.93 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 0.40 seconds
;; Checking the proof took 19.25 seconds
;; VERIFY took 27.72 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.07 seconds
;; Checking the proof took 2.69 seconds
;; VERIFY took 3.87 seconds
4361> DEFINE BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.disjoined-right-associativity.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.003 seconds
4362> VERIFY BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.disjoined-right-associativity.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.005 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4364> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-right-associativity.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 3.93 seconds
;; VERIFY took 5.62 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.28 seconds
;; Checking the proof took 49.70 seconds
;; VERIFY took 70.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.09 seconds
;; Checking the proof took 5.14 seconds
;; VERIFY took 7.46 seconds
4367> DEFINE BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/admit-build.disjoined-right-associativity-okp.proofs
;; Reading the file took 0.002 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.003 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.26 seconds
;; Checking the proof took 4.11 seconds
;; VERIFY took 6.44 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.01 seconds
;; Checking the proof took 0.59 seconds
;; VERIFY took 0.77 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.24 seconds
;; Checking the proof took 30.08 seconds
;; VERIFY took 45.31 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.22 seconds
;; Checking the proof took 16.37 seconds
;; VERIFY took 24.64 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 0.43 seconds
;; Checking the proof took 6.62 seconds
;; VERIFY took 10.20 seconds
4374> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-4
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-4.proofs
;; Reading the file took 0.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.04 seconds
4375> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-4
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-4.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4377> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-4
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-4.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 1.29 seconds
;; VERIFY took 1.85 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.27 seconds
;; Checking the proof took 21.34 seconds
;; VERIFY took 30.48 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.07 seconds
;; Checking the proof took 1.64 seconds
;; VERIFY took 2.42 seconds
4380> DEFINE BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.disjoined-associativity.proofs
;; Reading the file took 0.003 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.002 seconds
;; Checking the proof took 0.001 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.05 seconds
;; Checking the proof took 3.50 seconds
;; VERIFY took 5.04 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 0.38 seconds
;; Checking the proof took 29.36 seconds
;; VERIFY took 42.04 seconds
4385> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-associativity.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 4.47 seconds
;; VERIFY took 6.51 seconds
4386> DEFINE BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/admit-build.disjoined-associativity-okp.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.05 seconds
4387> VERIFY BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-build.disjoined-associativity-okp.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4388> VERIFY BOOLEANP-OF-BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-associativity-okp.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 4.20 seconds
;; VERIFY took 6.54 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.01 seconds
;; Checking the proof took 0.59 seconds
;; VERIFY took 0.76 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.28 seconds
;; Checking the proof took 30.37 seconds
;; VERIFY took 45.53 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.17 seconds
;; Checking the proof took 16.68 seconds
;; VERIFY took 24.98 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 0.52 seconds
;; Checking the proof took 6.44 seconds
;; VERIFY took 10.11 seconds
4393> DEFINE BUILD.DISJOINED-CUT-LEMMA-1
;; Reading from Proofs/level2/admit-build.disjoined-cut-lemma-1.proofs
;; Reading the file took 0.005 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4394> VERIFY BUILD.DISJOINED-CUT-LEMMA-1
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-1.proof
;; Reading the file took 0.005 seconds
;; Checking the proof took 0.001 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4396> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-CUT-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-cut-lemma-1.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 3.20 seconds
;; VERIFY took 4.71 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 0.37 seconds
;; Checking the proof took 23.35 seconds
;; VERIFY took 35.01 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.25 seconds
;; Checking the proof took 48.63 seconds
;; VERIFY took 72.81 seconds
4399> DEFINE BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/admit-build.disjoined-cut-lemma-2.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.003 seconds
4400> VERIFY BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-2.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.001 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.002 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4402> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-cut-lemma-2.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 1.13 seconds
;; VERIFY took 1.67 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 0.48 seconds
;; Checking the proof took 48.70 seconds
;; VERIFY took 72.15 seconds
4404> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.disjoined-cut-lemma-2.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 1.45 seconds
;; VERIFY took 2.18 seconds
4405> DEFINE BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/admit-build.disjoined-cut.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.003 seconds
4406> VERIFY BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/thm-build.disjoined-cut.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.001 seconds
;; 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4408> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-cut.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 3.88 seconds
;; VERIFY took 5.81 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 0.67 seconds
;; Checking the proof took 56.24 seconds
;; VERIFY took 83.63 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.17 seconds
;; Checking the proof took 5.76 seconds
;; VERIFY took 8.68 seconds
4411> DEFINE BUILD.DISJOINED-CUT-OKP
;; Reading from Proofs/level2/admit-build.disjoined-cut-okp.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.10 seconds
4412> VERIFY BUILD.DISJOINED-CUT-OKP
;; Reading from Proofs/level2/thm-build.disjoined-cut-okp.proof
;; Reading the file took 0.002 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 0.37 seconds
;; Checking the proof took 7.21 seconds
;; VERIFY took 11.08 seconds
4414> VERIFY BUILD.DISJOINED-CUT-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-cut-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.83 seconds
;; VERIFY took 1.06 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 0.48 seconds
;; Checking the proof took 67.68 seconds
;; VERIFY took 100.35 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.26 seconds
;; Checking the proof took 29.60 seconds
;; VERIFY took 43.55 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 0.99 seconds
;; Checking the proof took 20.39 seconds
;; VERIFY took 31.04 seconds
4418> DEFINE BUILD.DISJOINED-MODUS-PONENS
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens.proofs
;; Reading the file took 0.001 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.001 seconds
;; Checking the proof took 0.001 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.004 seconds
;; Checking the proof took 0.03 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.20 seconds
;; Checking the proof took 31.23 seconds
;; VERIFY took 45.38 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 1.10 seconds
;; Checking the proof took 72.87 seconds
;; VERIFY took 107.40 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.27 seconds
;; Checking the proof took 63.56 seconds
;; VERIFY took 93.65 seconds
4424> DEFINE BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-okp.proofs
;; Reading the file took 0.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 seconds
4425> VERIFY BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4426> VERIFY BOOLEANP-OF-BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-modus-ponens-okp.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 3.74 seconds
;; VERIFY took 5.63 seconds
4427> VERIFY BUILD.DISJOINED-MODUS-PONENS-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.60 seconds
;; VERIFY took 0.78 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.30 seconds
;; Checking the proof took 40.86 seconds
;; VERIFY took 60.14 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.21 seconds
;; Checking the proof took 17.92 seconds
;; VERIFY took 26.24 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 0.81 seconds
;; Checking the proof took 15.27 seconds
;; VERIFY took 23.31 seconds
4431> DEFINE BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-2.proofs
;; Reading the file took 0.003 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.002 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.004 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.004 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4434> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-modus-ponens-2.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 27.93 seconds
;; VERIFY took 40.64 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 1.09 seconds
;; Checking the proof took 69.11 seconds
;; VERIFY took 101.81 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.31 seconds
;; Checking the proof took 57.55 seconds
;; VERIFY took 84.48 seconds
4437> DEFINE BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-2-okp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.06 seconds
4438> VERIFY BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4439> VERIFY BOOLEANP-OF-BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-modus-ponens-2-okp.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 3.62 seconds
;; VERIFY took 5.47 seconds
4440> VERIFY BUILD.DISJOINED-MODUS-PONENS-2-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.58 seconds
;; VERIFY took 0.75 seconds
4441> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.disjoined-modus-ponens-2-okp.proof
;; Reading the file took 0.31 seconds
;; Checking the proof took 40.50 seconds
;; VERIFY took 59.52 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.35 seconds
;; Checking the proof took 20.47 seconds
;; VERIFY took 30.15 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 0.89 seconds
;; Checking the proof took 15.34 seconds
;; VERIFY took 23.46 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.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.004 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.001 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.005 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.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4447> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.LHS-COMMUTE-OR-THEN-RASSOC
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.lhs-commute-or-then-rassoc.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 1.20 seconds
;; VERIFY took 1.69 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.18 seconds
;; Checking the proof took 10.64 seconds
;; VERIFY took 14.83 seconds
4449> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.LHS-COMMUTE-OR-THEN-RASSOC
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.lhs-commute-or-then-rassoc.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 1.65 seconds
;; VERIFY took 2.35 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.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 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.002 seconds
;; Checking the proof took 0.004 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.14 seconds
;; Checking the proof took 1.88 seconds
;; VERIFY took 2.87 seconds
4453> VERIFY BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.lhs-commute-or-then-rassoc-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.38 seconds
;; VERIFY took 0.50 seconds
4454> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP
;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.lhs-commute-or-then-rassoc-okp.proof
;; Reading the file took 0.23 seconds
;; Checking the proof took 15.06 seconds
;; VERIFY took 22.42 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.15 seconds
;; Checking the proof took 8.62 seconds
;; VERIFY took 12.79 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.35 seconds
;; Checking the proof took 3.93 seconds
;; VERIFY took 6.16 seconds
4457> DEFINE RW.CREWRITE-TWIDDLE-BLDR
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle-bldr.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.003 seconds
4458> VERIFY RW.CREWRITE-TWIDDLE-BLDR
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.001 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4460> VERIFY FORCING-LOGIC.APPEALP-OF-RW.CREWRITE-TWIDDLE-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-rw.crewrite-twiddle-bldr.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 1.22 seconds
;; VERIFY took 1.71 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.14 seconds
;; Checking the proof took 10.82 seconds
;; VERIFY took 14.95 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.06 seconds
;; Checking the proof took 1.71 seconds
;; VERIFY took 2.45 seconds
4463> DEFINE RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle-bldr-okp.proofs
;; Reading the file took 0.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4464> VERIFY RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr-okp.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.004 seconds
;; VERIFY took 0.01 seconds
4465> VERIFY BOOLEANP-OF-RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-rw.crewrite-twiddle-bldr-okp.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 1.92 seconds
;; VERIFY took 2.89 seconds
4466> VERIFY RW.CREWRITE-TWIDDLE-BLDR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.39 seconds
;; VERIFY took 0.50 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.18 seconds
;; Checking the proof took 15.29 seconds
;; VERIFY took 22.66 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.15 seconds
;; Checking the proof took 8.75 seconds
;; VERIFY took 12.97 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.34 seconds
;; Checking the proof took 4.02 seconds
;; VERIFY took 6.25 seconds
4470> DEFINE RW.CREWRITE-TWIDDLE2-LEMMA
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-lemma.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4471> VERIFY RW.CREWRITE-TWIDDLE2-LEMMA
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-lemma.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.005 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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4473> VERIFY FORCING-LOGIC.APPEALP-OF-RW.CREWRITE-TWIDDLE2-LEMMA
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-rw.crewrite-twiddle2-lemma.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 9.95 seconds
;; VERIFY took 13.93 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 0.49 seconds
;; Checking the proof took 81.82 seconds
;; VERIFY took 114.91 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.09 seconds
;; Checking the proof took 15.56 seconds
;; VERIFY took 22.06 seconds
4476> DEFINE RW.CREWRITE-TWIDDLE2-BLDR
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-bldr.proofs
;; Reading the file took 0.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.003 seconds
4477> VERIFY RW.CREWRITE-TWIDDLE2-BLDR
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.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.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4479> VERIFY FORCING-LOGIC.APPEALP-OF-RW.CREWRITE-TWIDDLE2-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-rw.crewrite-twiddle2-bldr.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 6.17 seconds
;; VERIFY took 8.62 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 0.45 seconds
;; Checking the proof took 89.08 seconds
;; VERIFY took 124.77 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.08 seconds
;; Checking the proof took 8.31 seconds
;; VERIFY took 11.78 seconds
4482> DEFINE RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-bldr-okp.proofs
;; Reading the file took 0.001 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.001 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.31 seconds
;; Checking the proof took 4.34 seconds
;; VERIFY took 6.72 seconds
4485> VERIFY RW.CREWRITE-TWIDDLE2-BLDR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-bldr-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.61 seconds
;; VERIFY took 0.79 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.25 seconds
;; Checking the proof took 31.28 seconds
;; VERIFY took 46.22 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.20 seconds
;; Checking the proof took 17.12 seconds
;; VERIFY took 25.27 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 0.47 seconds
;; Checking the proof took 6.61 seconds
;; VERIFY took 10.22 seconds
4489> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle-lemma-1.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; 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.001 seconds
;; VERIFY took 0.01 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.03 seconds
;; VERIFY took 0.05 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.09 seconds
;; Checking the proof took 25.15 seconds
;; VERIFY took 35.72 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 0.52 seconds
;; Checking the proof took 55.77 seconds
;; VERIFY took 80.81 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.26 seconds
;; Checking the proof took 137.05 seconds
;; VERIFY took 195.98 seconds
4495> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle.proofs
;; Reading the file took 0.003 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.005 seconds
4496> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.01 seconds
4497> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-under-iff.proof
;; Reading the file took 0.003 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.22 seconds
;; Checking the proof took 8.73 seconds
;; VERIFY took 12.43 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 0.28 seconds
;; Checking the proof took 13.45 seconds
;; VERIFY took 19.36 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.33 seconds
;; Checking the proof took 73.26 seconds
;; VERIFY took 104.86 seconds
4501> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE-OKP
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle-okp.proofs
;; Reading the file took 0.001 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.002 seconds
;; Checking the proof took 0.005 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.23 seconds
;; Checking the proof took 3.51 seconds
;; VERIFY took 5.33 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.01 seconds
;; Checking the proof took 0.56 seconds
;; VERIFY took 0.71 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.25 seconds
;; Checking the proof took 31.09 seconds
;; VERIFY took 45.63 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.25 seconds
;; Checking the proof took 21.38 seconds
;; VERIFY took 31.39 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 0.62 seconds
;; Checking the proof took 10.05 seconds
;; VERIFY took 15.33 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.005 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4509> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1A
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-1a.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.004 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.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.05 seconds
;; Checking the proof took 2.45 seconds
;; VERIFY took 3.52 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 0.52 seconds
;; Checking the proof took 22.41 seconds
;; VERIFY took 32.19 seconds
4513> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1A
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-clause.aux-split-twiddle2-lemma-1a.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 4.19 seconds
;; VERIFY took 6.09 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.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.004 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.004 seconds
;; Checking the proof took 0.001 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.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4517> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle2-lemma-1.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 7.63 seconds
;; VERIFY took 10.66 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 0.55 seconds
;; Checking the proof took 76.27 seconds
;; VERIFY took 108.88 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.31 seconds
;; Checking the proof took 92.00 seconds
;; VERIFY took 132.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.05 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.06 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.03 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.04 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.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 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.10 seconds
;; Checking the proof took 10.08 seconds
;; VERIFY took 14.38 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 0.42 seconds
;; Checking the proof took 29.34 seconds
;; VERIFY took 42.21 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.12 seconds
;; Checking the proof took 17.46 seconds
;; VERIFY took 25.35 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.001 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4527> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.001 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.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4529> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle2-lemma-2.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 7.78 seconds
;; VERIFY took 10.80 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.39 seconds
;; Checking the proof took 91.47 seconds
;; VERIFY took 127.71 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.09 seconds
;; Checking the proof took 11.75 seconds
;; VERIFY took 16.71 seconds
4532> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2.proofs
;; Reading the file took 0.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4533> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2.proof
;; Reading the file took 0.001 seconds
;; Checking the proof took 0.001 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.004 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.04 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.26 seconds
;; Checking the proof took 15.08 seconds
;; VERIFY took 20.88 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.35 seconds
;; Checking the proof took 20.35 seconds
;; VERIFY took 28.56 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 0.53 seconds
;; Checking the proof took 80.88 seconds
;; VERIFY took 114.48 seconds
4538> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-OKP
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-okp.proofs
;; Reading the file took 0.002 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.002 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.27 seconds
;; Checking the proof took 4.43 seconds
;; VERIFY took 6.74 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.01 seconds
;; Checking the proof took 0.63 seconds
;; VERIFY took 0.80 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.31 seconds
;; Checking the proof took 32.13 seconds
;; VERIFY took 47.17 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.22 seconds
;; Checking the proof took 17.60 seconds
;; VERIFY took 25.77 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 0.44 seconds
;; Checking the proof took 6.86 seconds
;; VERIFY took 10.39 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.005 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.05 seconds
4546> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4547> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr-under-iff.proof
;; Reading the file took 0.004 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4548> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-default-3-bldr.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 1.85 seconds
;; VERIFY took 2.55 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.29 seconds
;; Checking the proof took 16.71 seconds
;; VERIFY took 23.48 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.19 seconds
;; Checking the proof took 14.46 seconds
;; VERIFY took 20.20 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.03 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.05 seconds
4552> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.005 seconds
;; VERIFY took 0.02 seconds
4553> VERIFY BOOLEANP-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-clause.aux-split-default-3-bldr-okp.proof
;; Reading the file took 0.16 seconds
;; Checking the proof took 2.00 seconds
;; VERIFY took 3.02 seconds
4554> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.41 seconds
;; VERIFY took 0.52 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.24 seconds
;; Checking the proof took 15.84 seconds
;; VERIFY took 23.25 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.18 seconds
;; Checking the proof took 9.09 seconds
;; VERIFY took 13.31 seconds
4557> VERIFY FORCING-SOUNDNESS-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/thm-forcing-soundness-of-clause.aux-split-default-3-bldr-okp.proof
;; Reading the file took 0.36 seconds
;; Checking the proof took 4.14 seconds
;; VERIFY took 6.41 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.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.004 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.002 seconds
;; Checking the proof took 0.001 seconds
;; VERIFY took 0.004 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.01 seconds
;; VERIFY took 0.02 seconds
4561> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-limsplit-cutoff-step-bldr.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 1.27 seconds
;; VERIFY took 1.83 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.19 seconds
;; Checking the proof took 11.46 seconds
;; VERIFY took 15.66 seconds
4563> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-clause.aux-limsplit-cutoff-step-bldr.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 1.74 seconds
;; VERIFY took 2.45 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.003 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.001 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.13 seconds
;; Checking the proof took 2.00 seconds
;; VERIFY took 2.98 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.41 seconds
;; VERIFY took 0.55 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.17 seconds
;; Checking the proof took 15.95 seconds
;; VERIFY took 23.26 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.18 seconds
;; Checking the proof took 9.13 seconds
;; VERIFY took 13.35 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.35 seconds
;; Checking the proof took 4.14 seconds
;; VERIFY took 6.38 seconds
4571> DEFINE LEVEL2.STEP-OKP
;; Reading from Proofs/level2/admit-level2.step-okp.proofs
;; Reading the file took 0.002 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4572> VERIFY LEVEL2.STEP-OKP
;; Reading from Proofs/level2/thm-level2.step-okp.proof
;; Reading the file took 0.01 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.24 seconds
;; Checking the proof took 3.04 seconds
;; VERIFY took 4.88 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 0.71 seconds
;; Checking the proof took 16.91 seconds
;; VERIFY took 26.66 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.22 seconds
;; Checking the proof took 3.39 seconds
;; VERIFY took 4.85 seconds
4576> DEFINE LEVEL2.FLAG-PROOFP
;; Reading from Proofs/level2/admit-level2.flag-proofp.proofs
;; Reading the file took 0.18 seconds
;; Checking the proofs took 1.19 seconds
;; DEFINE took 1.79 seconds
4577> VERIFY LEVEL2.FLAG-PROOFP
;; Reading from Proofs/level2/thm-level2.flag-proofp.proof
;; Reading the file took 0.002 seconds
;; Checking the proof took 0.001 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.003 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.001 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.001 seconds
;; VERIFY took 0.02 seconds
4582> VERIFY DEFINITION-OF-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-definition-of-level2.proofp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.10 seconds
4583> VERIFY DEFINITION-OF-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-definition-of-level2.proof-listp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.30 seconds
4584> VERIFY LEVEL2.PROOFP-WHEN-NOT-CONSP
;; Reading from Proofs/level2/thm-level2.proofp-when-not-consp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.07 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.03 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.09 seconds
4586> VERIFY LEVEL2.PROOF-LISTP-OF-CONS
;; Reading from Proofs/level2/thm-level2.proof-listp-of-cons.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.10 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 0.34 seconds
;; Checking the proof took 2.94 seconds
;; VERIFY took 4.28 seconds
4588> VERIFY BOOLEANP-OF-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-booleanp-of-level2.proofp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.16 seconds
4589> VERIFY BOOLEANP-OF-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-booleanp-of-level2.proof-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.15 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.22 seconds
;; Checking the proof took 1.09 seconds
;; VERIFY took 1.74 seconds
4591> VERIFY LEVEL2.PROOF-LISTP-OF-APP
;; Reading from Proofs/level2/thm-level2.proof-listp-of-app.proof
;; Reading the file took 0.34 seconds
;; Checking the proof took 2.22 seconds
;; VERIFY took 3.59 seconds
4592> VERIFY LEVEL2.PROOF-LISTP-OF-REV
;; Reading from Proofs/level2/thm-level2.proof-listp-of-rev.proof
;; Reading the file took 0.24 seconds
;; Checking the proof took 1.11 seconds
;; VERIFY took 1.80 seconds
4593> VERIFY LEVEL2.PROOFP-OF-CAR-WHEN-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proofp-of-car-when-level2.proof-listp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.25 seconds
4594> VERIFY LEVEL2.PROOF-LISTP-OF-CDR-WHEN-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proof-listp-of-cdr-when-level2.proof-listp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.15 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.14 seconds
;; Checking the proof took 0.85 seconds
;; VERIFY took 1.29 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.02 seconds
;; Checking the proof took 0.09 seconds
;; VERIFY took 0.15 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.12 seconds
;; Checking the proof took 0.75 seconds
;; VERIFY took 1.11 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.22 seconds
;; Checking the proof took 1.23 seconds
;; VERIFY took 1.94 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.15 seconds
;; Checking the proof took 0.73 seconds
;; VERIFY took 1.12 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.13 seconds
;; Checking the proof took 0.95 seconds
;; VERIFY took 1.41 seconds
4601> VERIFY LEVEL2.PROOF-LISTP-OF-SUBSETP-WHEN-LEVEL2.PROOF-LISTP-ALT
;; Reading from Proofs/level2/thm-level2.proof-listp-of-subsetp-when-level2.proof-listp-alt.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 seconds
4602> VERIFY LEVEL2.PROOF-LISTP-OF-REPEAT
;; Reading from Proofs/level2/thm-level2.proof-listp-of-repeat.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.83 seconds
;; VERIFY took 1.23 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 1.29 seconds
;; Checking the proof took 13.61 seconds
;; VERIFY took 20.51 seconds
4604> VERIFY LOGIC.PROVABLEP-WHEN-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-logic.provablep-when-level2.proofp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.40 seconds
;; VERIFY took 0.60 seconds
4605> VERIFY LOGIC.PROVABLE-LISTP-WHEN-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-logic.provable-listp-when-level2.proof-listp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.35 seconds
;; VERIFY took 0.55 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 0.60 seconds
;; Checking the proof took 4.16 seconds
;; VERIFY took 6.37 seconds
4607> VERIFY LEVEL2.PROOFP-WHEN-LOGIC.PROOFP
;; Reading from Proofs/level2/thm-level2.proofp-when-logic.proofp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.24 seconds
4608> VERIFY LEVEL2.PROOF-LISTP-WHEN-LOGIC.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proof-listp-when-logic.proof-listp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.24 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.03 seconds
;; VERIFY took 0.06 seconds
4610> VERIFY INSTALL-NEW-PROOFP-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-install-new-proofp-level2.proofp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.07 seconds
4611 > SWITCH LEVEL2.PROOFP
;; SWITCH took 0.00 seconds
4612 > FINISH level2
[undoing binding stack and other enclosing state... done]
[saving current Lisp image into level2.nemesis-sbcl:
writing 2752 bytes from the read-only space at 0x01000000
writing 1712 bytes from the static space at 0x01100000
writing 29270016 bytes from the dynamic space at 0x09000000
done]

real	86m1.284s
user	85m32.429s
sys	0m3.812s