International Allegro CL Enterprise Edition
8.0 [Linux (x86)] (Oct 29, 2009 22:47)
Copyright (C) 1985-2005, Franz Inc., Oakland, CA, USA.  All Rights Reserved.

This development copy of Allegro CL is licensed to:
   [TC8015] University of Texas

;; Optimization settings: safety 0, space 0, speed 3, debug 0.
;; For a complete description of all compiler switches given the
;; current optimization settings evaluate (EXPLAIN-COMPILER-SETTINGS).
Milawa Proof Checker.
4010> DEFINE BUILD.AXIOM
;; Reading from Proofs/level2/admit-build.axiom.proofs
;; Reading the file took 0.06 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.06 seconds
4011> VERIFY BUILD.AXIOM
;; Reading from Proofs/level2/thm-build.axiom.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4012> VERIFY BUILD.AXIOM-UNDER-IFF
;; Reading from Proofs/level2/thm-build.axiom-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4013> VERIFY LOGIC.METHOD-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.method-of-build.axiom.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4015> VERIFY LOGIC.SUBPROOFS-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.axiom.proof
;; Reading the file took 0.00 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4017> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.axiom.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.08 seconds
4018> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.AXIOM
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.axiom.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.35 seconds
4019> DEFINE BUILD.THEOREM
;; Reading from Proofs/level2/admit-build.theorem.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4020> VERIFY BUILD.THEOREM
;; Reading from Proofs/level2/thm-build.theorem.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4021> VERIFY BUILD.THEOREM-UNDER-IFF
;; Reading from Proofs/level2/thm-build.theorem-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4023> VERIFY LOGIC.CONCLUSION-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.theorem.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4024> VERIFY LOGIC.SUBPROOFS-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.theorem.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4025> VERIFY LOGIC.EXTRAS-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-logic.extras-of-build.theorem.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4026> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.THEOREM
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.theorem.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.06 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.08 seconds
;; Checking the proof took 0.23 seconds
;; VERIFY took 0.38 seconds
4028> DEFINE BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/admit-build.propositional-schema.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4029> VERIFY BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-build.propositional-schema.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.00 seconds
4030> VERIFY BUILD.PROPOSITIONAL-SCHEMA-UNDER-IFF
;; Reading from Proofs/level2/thm-build.propositional-schema-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4031> VERIFY LOGIC.METHOD-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-logic.method-of-build.propositional-schema.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
4032> VERIFY LOGIC.CONCLUSION-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.propositional-schema.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.03 seconds
4033> VERIFY LOGIC.SUBPROOFS-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.propositional-schema.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4034> VERIFY LOGIC.EXTRAS-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-logic.extras-of-build.propositional-schema.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.08 seconds
4036> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.PROPOSITIONAL-SCHEMA
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.propositional-schema.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.28 seconds
;; VERIFY took 0.39 seconds
4037> DEFINE BUILD.CUT
;; Reading from Proofs/level2/admit-build.cut.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4038> VERIFY BUILD.CUT
;; Reading from Proofs/level2/thm-build.cut.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4039> VERIFY BUILD.CUT-UNDER-IFF
;; Reading from Proofs/level2/thm-build.cut-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4040> VERIFY LOGIC.METHOD-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-logic.method-of-build.cut.proof
;; Reading the file took 0.00 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.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 seconds
4042> VERIFY LOGIC.SUBPROOFS-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.cut.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.05 seconds
;; VERIFY took 0.07 seconds
4043> VERIFY LOGIC.EXTRAS-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-logic.extras-of-build.cut.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4044> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.CUT
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.cut.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.36 seconds
;; VERIFY took 0.52 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.18 seconds
;; Checking the proof took 1.53 seconds
;; VERIFY took 2.27 seconds
4046> DEFINE BUILD.CONTRACTION
;; Reading from Proofs/level2/admit-build.contraction.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4047> VERIFY BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-build.contraction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4048> VERIFY BUILD.CONTRACTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.contraction-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4049> VERIFY LOGIC.METHOD-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.method-of-build.contraction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4050> VERIFY LOGIC.CONCLUSION-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.contraction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4051> VERIFY LOGIC.SUBPROOFS-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.contraction.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 seconds
4052> VERIFY LOGIC.EXTRAS-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-logic.extras-of-build.contraction.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.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.04 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.21 seconds
4054> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.CONTRACTION
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.contraction.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.45 seconds
;; VERIFY took 0.67 seconds
4055> DEFINE BUILD.EXPANSION
;; Reading from Proofs/level2/admit-build.expansion.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4056> VERIFY BUILD.EXPANSION
;; Reading from Proofs/level2/thm-build.expansion.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
4057> VERIFY BUILD.EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.expansion-under-iff.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.06 seconds
4058> VERIFY LOGIC.METHOD-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.method-of-build.expansion.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4059> VERIFY LOGIC.CONCLUSION-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.expansion.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.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.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 seconds
4061> VERIFY LOGIC.EXTRAS-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-logic.extras-of-build.expansion.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4062> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.expansion.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.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.05 seconds
;; Checking the proof took 0.32 seconds
;; VERIFY took 0.46 seconds
4064> DEFINE BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.associativity.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4065> VERIFY BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4066> VERIFY BUILD.ASSOCIATIVITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.associativity-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4067> VERIFY LOGIC.METHOD-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.method-of-build.associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4068> VERIFY LOGIC.CONCLUSION-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4069> VERIFY LOGIC.SUBPROOFS-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 seconds
4070> VERIFY LOGIC.EXTRAS-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-logic.extras-of-build.associativity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4071> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.associativity.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.27 seconds
;; VERIFY took 0.40 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.08 seconds
;; Checking the proof took 0.88 seconds
;; VERIFY took 1.24 seconds
4073> DEFINE BUILD.INSTANTIATION
;; Reading from Proofs/level2/admit-build.instantiation.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4074> VERIFY BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-build.instantiation.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4075> VERIFY BUILD.INSTANTIATION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.instantiation-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 seconds
4076> VERIFY LOGIC.METHOD-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.method-of-build.instantiation.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.17 seconds
4077> VERIFY LOGIC.CONCLUSION-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.instantiation.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.10 seconds
4078> VERIFY LOGIC.SUBPROOFS-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.instantiation.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.48 seconds
;; VERIFY took 0.69 seconds
4079> VERIFY LOGIC.EXTRAS-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-logic.extras-of-build.instantiation.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.11 seconds
;; VERIFY took 0.18 seconds
4080> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.INSTANTIATION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.instantiation.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.29 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.11 seconds
;; Checking the proof took 0.73 seconds
;; VERIFY took 1.11 seconds
4082> DEFINE BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/admit-build.functional-equality.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4083> VERIFY BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-build.functional-equality.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4084> VERIFY BUILD.FUNCTIONAL-EQUALITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.functional-equality-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 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.00 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4087> VERIFY LOGIC.SUBPROOFS-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.functional-equality.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4088> VERIFY LOGIC.EXTRAS-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-logic.extras-of-build.functional-equality.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4089> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.FUNCTIONAL-EQUALITY
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.functional-equality.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.13 seconds
;; VERIFY took 0.21 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.14 seconds
;; Checking the proof took 0.83 seconds
;; VERIFY took 1.23 seconds
4091> DEFINE BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/admit-build.beta-reduction.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4092> VERIFY BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-build.beta-reduction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4093> VERIFY BUILD.BETA-REDUCTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.beta-reduction-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4094> VERIFY LOGIC.METHOD-OF-BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-logic.method-of-build.beta-reduction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4095> VERIFY LOGIC.CONCLUSION-OF-BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.beta-reduction.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4096> VERIFY LOGIC.SUBPROOFS-OF-BUILD.BETA-REDUCTION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.beta-reduction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.04 seconds
;; Checking the proof took 0.41 seconds
;; VERIFY took 0.57 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.19 seconds
;; Checking the proof took 1.36 seconds
;; VERIFY took 2.01 seconds
4100> DEFINE BUILD.BASE-EVAL
;; Reading from Proofs/level2/admit-build.base-eval.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4101> VERIFY BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-build.base-eval.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4102> VERIFY BUILD.BASE-EVAL-UNDER-IFF
;; Reading from Proofs/level2/thm-build.base-eval-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4103> VERIFY LOGIC.METHOD-OF-BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-logic.method-of-build.base-eval.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4104> VERIFY LOGIC.CONCLUSION-OF-BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.base-eval.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.07 seconds
4105> VERIFY LOGIC.SUBPROOFS-OF-BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.base-eval.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4106> VERIFY LOGIC.EXTRAS-OF-BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-logic.extras-of-build.base-eval.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.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.03 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.12 seconds
4108> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.BASE-EVAL
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.base-eval.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.32 seconds
;; VERIFY took 0.46 seconds
4109> DEFINE BUILD.INSTANTIATION-LIST
;; Reading from Proofs/level2/admit-build.instantiation-list.proofs
;; Reading the file took 0.04 seconds
;; Checking the proofs took 0.07 seconds
;; DEFINE took 0.12 seconds
4110> VERIFY BUILD.INSTANTIATION-LIST
;; Reading from Proofs/level2/thm-build.instantiation-list.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 seconds
4111> VERIFY BUILD.INSTANTIATION-LIST-WHEN-NOT-CONSP
;; Reading from Proofs/level2/thm-build.instantiation-list-when-not-consp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.06 seconds
4112> VERIFY BUILD.INSTANTIATION-LIST-OF-CONS
;; Reading from Proofs/level2/thm-build.instantiation-list-of-cons.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.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.17 seconds
;; Checking the proof took 0.94 seconds
;; VERIFY took 1.39 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.16 seconds
;; Checking the proof took 0.94 seconds
;; VERIFY took 1.36 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.27 seconds
;; Checking the proof took 1.33 seconds
;; VERIFY took 2.04 seconds
4116> DEFINE BUILD.INDUCTION
;; Reading from Proofs/level2/admit-build.induction.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4117> VERIFY BUILD.INDUCTION
;; Reading from Proofs/level2/thm-build.induction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4118> VERIFY BUILD.INDUCTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.induction-under-iff.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
4119> VERIFY LOGIC.METHOD-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-logic.method-of-build.induction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4120> VERIFY LOGIC.CONCLUSION-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-logic.conclusion-of-build.induction.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4121> VERIFY LOGIC.SUBPROOFS-OF-BUILD.INDUCTION
;; Reading from Proofs/level2/thm-logic.subproofs-of-build.induction.proof
;; Reading the file took 0.00 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.02 seconds
;; Checking the proof took 0.08 seconds
;; VERIFY took 0.11 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.10 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.19 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.37 seconds
;; Checking the proof took 3.44 seconds
;; VERIFY took 5.11 seconds
4125> DEFINE BUILD.COMMUTE-OR
;; Reading from Proofs/level2/admit-build.commute-or.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4126> VERIFY BUILD.COMMUTE-OR
;; Reading from Proofs/level2/thm-build.commute-or.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4127> VERIFY BUILD.COMMUTE-OR-UNDER-IFF
;; Reading from Proofs/level2/thm-build.commute-or-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4128> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.COMMUTE-OR
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.commute-or.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.16 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.03 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.08 seconds
4130> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.COMMUTE-OR
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.commute-or.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.19 seconds
;; VERIFY took 0.30 seconds
4131> DEFINE BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/admit-build.commute-or-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4132> VERIFY BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-build.commute-or-okp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 seconds
4133> VERIFY BOOLEANP-OF-BUILD.COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.commute-or-okp.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.76 seconds
;; VERIFY took 1.09 seconds
4134> VERIFY BUILD.COMMUTE-OR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.commute-or-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.22 seconds
;; VERIFY took 0.29 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.20 seconds
;; Checking the proof took 6.66 seconds
;; VERIFY took 9.19 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.17 seconds
;; Checking the proof took 4.22 seconds
;; VERIFY took 5.83 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.33 seconds
;; Checking the proof took 2.35 seconds
;; VERIFY took 3.57 seconds
4138> DEFINE BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/admit-build.right-expansion.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4139> VERIFY BUILD.RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-build.right-expansion.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4140> VERIFY BUILD.RIGHT-EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.right-expansion-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.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.03 seconds
;; Checking the proof took 0.06 seconds
;; VERIFY took 0.10 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.06 seconds
;; Checking the proof took 0.34 seconds
;; VERIFY took 0.50 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.03 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.17 seconds
4144> DEFINE BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/admit-build.right-expansion-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4145> VERIFY BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-build.right-expansion-okp.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4146> VERIFY BOOLEANP-OF-BUILD.RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.right-expansion-okp.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 0.50 seconds
;; VERIFY took 0.75 seconds
4147> VERIFY BUILD.RIGHT-EXPANSION-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.right-expansion-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.15 seconds
;; VERIFY took 0.20 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.26 seconds
;; Checking the proof took 10.37 seconds
;; VERIFY took 14.21 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.16 seconds
;; Checking the proof took 2.30 seconds
;; VERIFY took 3.24 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.30 seconds
;; Checking the proof took 1.66 seconds
;; VERIFY took 2.59 seconds
4151> DEFINE BUILD.MODUS-PONENS
;; Reading from Proofs/level2/admit-build.modus-ponens.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4152> VERIFY BUILD.MODUS-PONENS
;; Reading from Proofs/level2/thm-build.modus-ponens.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4153> VERIFY BUILD.MODUS-PONENS-UNDER-IFF
;; Reading from Proofs/level2/thm-build.modus-ponens-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
4154> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MODUS-PONENS
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.modus-ponens.proof
;; Reading the file took 0.24 seconds
;; Checking the proof took 0.66 seconds
;; VERIFY took 1.12 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.12 seconds
;; Checking the proof took 0.93 seconds
;; VERIFY took 1.34 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.20 seconds
;; Checking the proof took 8.92 seconds
;; VERIFY took 12.13 seconds
4157> DEFINE BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/admit-build.modus-ponens-okp.proofs
;; Reading the file took 0.01 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4159> VERIFY BOOLEANP-OF-BUILD.MODUS-PONENS-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.modus-ponens-okp.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 0.93 seconds
;; VERIFY took 1.30 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.03 seconds
;; Checking the proof took 0.28 seconds
;; VERIFY took 0.36 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.26 seconds
;; Checking the proof took 12.17 seconds
;; VERIFY took 16.48 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.51 seconds
;; Checking the proof took 5.76 seconds
;; VERIFY took 8.11 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.74 seconds
;; Checking the proof took 7.26 seconds
;; VERIFY took 10.66 seconds
4164> DEFINE BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/admit-build.modus-ponens-2.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4165> VERIFY BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/thm-build.modus-ponens-2.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 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.06 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.08 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.55 seconds
;; Checking the proof took 0.74 seconds
;; VERIFY took 1.52 seconds
4168> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.modus-ponens-2.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.12 seconds
4169> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.MODUS-PONENS-2
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.modus-ponens-2.proof
;; Reading the file took 0.30 seconds
;; Checking the proof took 9.93 seconds
;; VERIFY took 13.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.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4171> VERIFY BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-build.modus-ponens-2-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4172> VERIFY BOOLEANP-OF-BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.modus-ponens-2-okp.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.85 seconds
;; VERIFY took 1.19 seconds
4173> VERIFY BUILD.MODUS-PONENS-2-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.modus-ponens-2-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.26 seconds
;; VERIFY took 0.33 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.27 seconds
;; Checking the proof took 11.91 seconds
;; VERIFY took 16.17 seconds
4175> VERIFY LEMMA-2-FOR-SOUNDNESS-OF-BUILD.MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/thm-lemma-2-for-soundness-of-build.modus-ponens-2-okp.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 6.80 seconds
;; VERIFY took 9.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.58 seconds
;; Checking the proof took 7.08 seconds
;; VERIFY took 10.28 seconds
4177> DEFINE BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.right-associativity.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4178> VERIFY BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.right-associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4179> VERIFY BUILD.RIGHT-ASSOCIATIVITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.right-associativity-under-iff.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.05 seconds
4180> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.right-associativity.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 2.74 seconds
;; VERIFY took 3.67 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.37 seconds
;; Checking the proof took 24.48 seconds
;; VERIFY took 32.21 seconds
4182> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.right-associativity.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 4.33 seconds
;; VERIFY took 5.83 seconds
4183> DEFINE BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/admit-build.right-associativity-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4184> VERIFY BUILD.RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-build.right-associativity-okp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 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.18 seconds
;; Checking the proof took 2.19 seconds
;; VERIFY took 3.07 seconds
4186> VERIFY BUILD.RIGHT-ASSOCIATIVITY-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.right-associativity-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.43 seconds
;; VERIFY took 0.54 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.21 seconds
;; Checking the proof took 17.83 seconds
;; VERIFY took 24.02 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.19 seconds
;; Checking the proof took 10.10 seconds
;; VERIFY took 13.67 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.47 seconds
;; Checking the proof took 4.51 seconds
;; VERIFY took 6.58 seconds
4190> DEFINE BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/admit-build.disjoined-left-expansion.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4191> VERIFY BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/thm-build.disjoined-left-expansion.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4192> VERIFY BUILD.DISJOINED-LEFT-EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-left-expansion-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4193> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-left-expansion.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.32 seconds
;; VERIFY took 0.48 seconds
4194> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-LEFT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-left-expansion.proof
;; Reading the file took 0.26 seconds
;; Checking the proof took 3.58 seconds
;; VERIFY took 4.89 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.09 seconds
;; Checking the proof took 0.58 seconds
;; VERIFY took 0.86 seconds
4196> DEFINE BUILD.DISJOINED-LEFT-EXPANSION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-left-expansion-okp.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 seconds
4197> VERIFY BUILD.DISJOINED-LEFT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-build.disjoined-left-expansion-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4198> VERIFY BOOLEANP-OF-BUILD.DISJOINED-LEFT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-left-expansion-okp.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 1.77 seconds
;; VERIFY took 2.53 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.04 seconds
;; Checking the proof took 0.32 seconds
;; VERIFY took 0.42 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.37 seconds
;; Checking the proof took 24.99 seconds
;; VERIFY took 33.89 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.19 seconds
;; Checking the proof took 6.31 seconds
;; VERIFY took 8.62 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.47 seconds
;; Checking the proof took 4.08 seconds
;; VERIFY took 6.05 seconds
4203> DEFINE BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/admit-build.disjoined-right-expansion.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4204> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-build.disjoined-right-expansion.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4205> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-right-expansion-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4206> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-RIGHT-EXPANSION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-right-expansion.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 1.35 seconds
;; VERIFY took 1.86 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.32 seconds
;; Checking the proof took 6.69 seconds
;; VERIFY took 9.05 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.09 seconds
;; Checking the proof took 2.52 seconds
;; VERIFY took 3.42 seconds
4209> DEFINE BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-right-expansion-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4210> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION-OKP
;; Reading from Proofs/level2/thm-build.disjoined-right-expansion-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.20 seconds
;; Checking the proof took 1.81 seconds
;; VERIFY took 2.58 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.08 seconds
;; Checking the proof took 0.33 seconds
;; VERIFY took 0.47 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.41 seconds
;; Checking the proof took 25.83 seconds
;; VERIFY took 34.72 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.18 seconds
;; Checking the proof took 6.36 seconds
;; VERIFY took 8.69 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.50 seconds
;; Checking the proof took 4.09 seconds
;; VERIFY took 6.08 seconds
4216> DEFINE BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/admit-build.disjoined-contraction.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4217> VERIFY BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/thm-build.disjoined-contraction.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4218> VERIFY BUILD.DISJOINED-CONTRACTION-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-contraction-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 seconds
4219> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-CONTRACTION
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-contraction.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 3.73 seconds
;; VERIFY took 5.00 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.12 seconds
;; Checking the proof took 0.93 seconds
;; VERIFY took 1.32 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.24 seconds
;; Checking the proof took 15.12 seconds
;; VERIFY took 20.10 seconds
4222> DEFINE BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/admit-build.disjoined-contraction-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4223> VERIFY BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/thm-build.disjoined-contraction-okp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4224> VERIFY BOOLEANP-OF-BUILD.DISJOINED-CONTRACTION-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-contraction-okp.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 1.72 seconds
;; VERIFY took 2.47 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.07 seconds
;; Checking the proof took 0.38 seconds
;; VERIFY took 0.52 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.25 seconds
;; Checking the proof took 18.16 seconds
;; VERIFY took 24.33 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.18 seconds
;; Checking the proof took 13.61 seconds
;; VERIFY took 18.15 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.50 seconds
;; Checking the proof took 7.60 seconds
;; VERIFY took 10.72 seconds
4229> DEFINE BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/admit-build.cancel-neg-neg.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4230> VERIFY BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/thm-build.cancel-neg-neg.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4231> VERIFY BUILD.CANCEL-NEG-NEG-UNDER-IFF
;; Reading from Proofs/level2/thm-build.cancel-neg-neg-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4232> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.cancel-neg-neg.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.44 seconds
;; VERIFY took 0.61 seconds
4233> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.CANCEL-NEG-NEG
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.cancel-neg-neg.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 2.51 seconds
;; VERIFY took 3.36 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.06 seconds
;; Checking the proof took 0.61 seconds
;; VERIFY took 0.84 seconds
4235> DEFINE BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/admit-build.cancel-neg-neg-okp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4236> VERIFY BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-build.cancel-neg-neg-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4237> VERIFY BOOLEANP-OF-BUILD.CANCEL-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.cancel-neg-neg-okp.proof
;; Reading the file took 0.09 seconds
;; Checking the proof took 0.56 seconds
;; VERIFY took 0.79 seconds
4238> VERIFY BUILD.CANCEL-NEG-NEG-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.cancel-neg-neg-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.20 seconds
;; VERIFY took 0.25 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.22 seconds
;; Checking the proof took 5.74 seconds
;; VERIFY took 7.84 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.20 seconds
;; Checking the proof took 4.86 seconds
;; VERIFY took 6.61 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.37 seconds
;; Checking the proof took 3.68 seconds
;; VERIFY took 5.37 seconds
4242> DEFINE BUILD.INSERT-NEG-NEG
;; Reading from Proofs/level2/admit-build.insert-neg-neg.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4243> VERIFY BUILD.INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-build.insert-neg-neg.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 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.07 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.09 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.06 seconds
;; Checking the proof took 0.28 seconds
;; VERIFY took 0.41 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.08 seconds
;; Checking the proof took 0.97 seconds
;; VERIFY took 1.30 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.06 seconds
;; Checking the proof took 0.39 seconds
;; VERIFY took 0.56 seconds
4248> DEFINE BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/admit-build.insert-neg-neg-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4249> VERIFY BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-build.insert-neg-neg-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4250> VERIFY BOOLEANP-OF-BUILD.INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.insert-neg-neg-okp.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 0.53 seconds
;; VERIFY took 0.74 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.08 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.29 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.43 seconds
;; Checking the proof took 9.62 seconds
;; VERIFY took 13.17 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.16 seconds
;; Checking the proof took 2.39 seconds
;; VERIFY took 3.32 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.19 seconds
;; Checking the proof took 1.15 seconds
;; VERIFY took 1.76 seconds
4255> DEFINE BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/admit-build.lhs-insert-neg-neg.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4256> VERIFY BUILD.LHS-INSERT-NEG-NEG
;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4257> VERIFY BUILD.LHS-INSERT-NEG-NEG-UNDER-IFF
;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg-under-iff.proof
;; Reading the file took 0.02 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.06 seconds
;; Checking the proof took 0.60 seconds
;; VERIFY took 0.84 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.25 seconds
;; Checking the proof took 3.48 seconds
;; VERIFY took 4.67 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.08 seconds
;; Checking the proof took 1.20 seconds
;; VERIFY took 1.64 seconds
4261> DEFINE BUILD.LHS-INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/admit-build.lhs-insert-neg-neg-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4262> VERIFY BUILD.LHS-INSERT-NEG-NEG-OKP
;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.25 seconds
;; Checking the proof took 1.57 seconds
;; VERIFY took 2.30 seconds
4264> VERIFY BUILD.LHS-INSERT-NEG-NEG-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.36 seconds
;; VERIFY took 0.45 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.75 seconds
;; Checking the proof took 32.58 seconds
;; VERIFY took 44.16 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.19 seconds
;; Checking the proof took 6.35 seconds
;; VERIFY took 8.65 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.79 seconds
;; VERIFY took 4.11 seconds
4268> DEFINE BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/admit-build.merge-negatives.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4269> VERIFY BUILD.MERGE-NEGATIVES
;; Reading from Proofs/level2/thm-build.merge-negatives.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4270> VERIFY BUILD.MERGE-NEGATIVES-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-negatives-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.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.11 seconds
;; Checking the proof took 17.50 seconds
;; VERIFY took 23.10 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.48 seconds
;; Checking the proof took 45.38 seconds
;; VERIFY took 59.17 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.18 seconds
;; Checking the proof took 26.40 seconds
;; VERIFY took 34.88 seconds
4274> DEFINE BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/admit-build.merge-negatives-okp.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4276> VERIFY BOOLEANP-OF-BUILD.MERGE-NEGATIVES-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.merge-negatives-okp.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 1.69 seconds
;; VERIFY took 2.32 seconds
4277> VERIFY BUILD.MERGE-NEGATIVES-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.merge-negatives-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.38 seconds
;; VERIFY took 0.47 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.29 seconds
;; Checking the proof took 15.62 seconds
;; VERIFY took 20.81 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.19 seconds
;; Checking the proof took 7.45 seconds
;; VERIFY took 9.98 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.52 seconds
;; Checking the proof took 5.61 seconds
;; VERIFY took 8.07 seconds
4281> DEFINE BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/admit-build.merge-implications-lemma-1.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4282> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-1.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4283> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-1-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 seconds
4284> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MERGE-IMPLICATIONS-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.merge-implications-lemma-1.proof
;; Reading the file took 0.14 seconds
;; Checking the proof took 17.02 seconds
;; VERIFY took 22.19 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.62 seconds
;; Checking the proof took 52.80 seconds
;; VERIFY took 69.04 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.15 seconds
;; Checking the proof took 30.28 seconds
;; VERIFY took 39.62 seconds
4287> DEFINE BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/admit-build.merge-implications-lemma-2.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4288> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-2.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4289> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-2-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-implications-lemma-2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4290> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MERGE-IMPLICATIONS-LEMMA-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.merge-implications-lemma-2.proof
;; Reading the file took 0.12 seconds
;; Checking the proof took 14.26 seconds
;; VERIFY took 18.71 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.38 seconds
;; Checking the proof took 64.49 seconds
;; VERIFY took 85.45 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.12 seconds
;; Checking the proof took 17.99 seconds
;; VERIFY took 23.79 seconds
4293> DEFINE BUILD.MERGE-IMPLICATIONS
;; Reading from Proofs/level2/admit-build.merge-implications.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4294> VERIFY BUILD.MERGE-IMPLICATIONS
;; Reading from Proofs/level2/thm-build.merge-implications.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4295> VERIFY BUILD.MERGE-IMPLICATIONS-UNDER-IFF
;; Reading from Proofs/level2/thm-build.merge-implications-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.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.08 seconds
;; Checking the proof took 1.43 seconds
;; VERIFY took 1.95 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.46 seconds
;; Checking the proof took 25.61 seconds
;; VERIFY took 34.14 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.08 seconds
;; Checking the proof took 1.93 seconds
;; VERIFY took 2.62 seconds
4299> DEFINE BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/admit-build.merge-implications-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4300> VERIFY BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/thm-build.merge-implications-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4301> VERIFY BOOLEANP-OF-BUILD.MERGE-IMPLICATIONS-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.merge-implications-okp.proof
;; Reading the file took 0.35 seconds
;; Checking the proof took 6.76 seconds
;; VERIFY took 9.33 seconds
4302> VERIFY BUILD.MERGE-IMPLICATIONS-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.merge-implications-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.85 seconds
;; VERIFY took 1.03 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.40 seconds
;; Checking the proof took 58.76 seconds
;; VERIFY took 77.60 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 25.57 seconds
;; VERIFY took 33.86 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 16.89 seconds
;; VERIFY took 23.22 seconds
4306> DEFINE BUILD.DISJOINED-COMMUTE-OR-LEMMA-1
;; Reading from Proofs/level2/admit-build.disjoined-commute-or-lemma-1.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4307> VERIFY BUILD.DISJOINED-COMMUTE-OR-LEMMA-1
;; Reading from Proofs/level2/thm-build.disjoined-commute-or-lemma-1.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4308> VERIFY BUILD.DISJOINED-COMMUTE-OR-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-commute-or-lemma-1-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.05 seconds
4309> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-COMMUTE-OR-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-commute-or-lemma-1.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 12.54 seconds
;; VERIFY took 16.42 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.40 seconds
;; Checking the proof took 31.05 seconds
;; VERIFY took 40.67 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.12 seconds
;; Checking the proof took 19.86 seconds
;; VERIFY took 26.13 seconds
4312> DEFINE BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/admit-build.disjoined-commute-or.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4313> VERIFY BUILD.DISJOINED-COMMUTE-OR
;; Reading from Proofs/level2/thm-build.disjoined-commute-or.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4314> VERIFY BUILD.DISJOINED-COMMUTE-OR-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-commute-or-under-iff.proof
;; Reading the file took 0.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.14 seconds
;; Checking the proof took 16.22 seconds
;; VERIFY took 21.20 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.25 seconds
;; Checking the proof took 65.47 seconds
;; VERIFY took 83.73 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.20 seconds
;; Checking the proof took 20.46 seconds
;; VERIFY took 26.83 seconds
4318> DEFINE BUILD.DISJOINED-COMMUTE-OR-OKP
;; Reading from Proofs/level2/admit-build.disjoined-commute-or-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4319> VERIFY BUILD.DISJOINED-COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-build.disjoined-commute-or-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4320> VERIFY BOOLEANP-OF-BUILD.DISJOINED-COMMUTE-OR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-commute-or-okp.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 2.33 seconds
;; VERIFY took 3.22 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.47 seconds
;; VERIFY took 0.59 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.21 seconds
;; Checking the proof took 18.97 seconds
;; VERIFY took 25.09 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.19 seconds
;; Checking the proof took 11.01 seconds
;; VERIFY took 14.56 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.40 seconds
;; Checking the proof took 4.86 seconds
;; VERIFY took 6.87 seconds
4325> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-1A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-1a.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4326> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1A
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1a.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4327> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1A-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1a-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 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.12 seconds
;; Checking the proof took 9.07 seconds
;; VERIFY took 11.89 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.44 seconds
;; Checking the proof took 51.01 seconds
;; VERIFY took 66.30 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.20 seconds
;; Checking the proof took 16.80 seconds
;; VERIFY took 22.12 seconds
4331> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-1.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4332> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4333> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1-under-iff.proof
;; Reading the file took 0.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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 3.28 seconds
;; VERIFY took 4.28 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.43 seconds
;; Checking the proof took 15.34 seconds
;; VERIFY took 20.02 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.16 seconds
;; Checking the proof took 6.80 seconds
;; VERIFY took 9.01 seconds
4337> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-2a.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4338> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2A
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2a.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4339> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2A-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2a-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 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.11 seconds
;; Checking the proof took 11.62 seconds
;; VERIFY took 15.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.43 seconds
;; Checking the proof took 34.94 seconds
;; VERIFY took 45.63 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.18 seconds
;; Checking the proof took 21.13 seconds
;; VERIFY took 27.71 seconds
4343> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-2
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-2.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4344> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4345> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2-under-iff.proof
;; Reading the file took 0.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.13 seconds
;; Checking the proof took 3.25 seconds
;; VERIFY took 4.30 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.46 seconds
;; Checking the proof took 15.21 seconds
;; VERIFY took 19.89 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.12 seconds
;; Checking the proof took 6.76 seconds
;; VERIFY took 8.89 seconds
4349> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-3A
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-3a.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4350> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-3A
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-3a.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 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.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4352> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-3A
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-3a.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 2.58 seconds
;; VERIFY took 3.40 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.23 seconds
;; Checking the proof took 4.91 seconds
;; VERIFY took 6.45 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.26 seconds
;; Checking the proof took 6.52 seconds
;; VERIFY took 8.68 seconds
4355> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-3
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-3.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4356> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-3
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-3.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4357> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-3-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-3-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 seconds
4358> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-3
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-3.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 2.45 seconds
;; VERIFY took 3.20 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.42 seconds
;; Checking the proof took 24.53 seconds
;; VERIFY took 31.71 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.13 seconds
;; Checking the proof took 3.29 seconds
;; VERIFY took 4.35 seconds
4361> DEFINE BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.disjoined-right-associativity.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4362> VERIFY BUILD.DISJOINED-RIGHT-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.disjoined-right-associativity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 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.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 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.08 seconds
;; Checking the proof took 4.87 seconds
;; VERIFY took 6.33 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.34 seconds
;; Checking the proof took 63.06 seconds
;; VERIFY took 80.76 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.10 seconds
;; Checking the proof took 6.48 seconds
;; VERIFY took 8.44 seconds
4367> DEFINE BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/admit-build.disjoined-right-associativity-okp.proofs
;; Reading the file took 0.01 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4368> VERIFY BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-build.disjoined-right-associativity-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 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.31 seconds
;; Checking the proof took 5.46 seconds
;; VERIFY took 7.48 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.03 seconds
;; Checking the proof took 0.76 seconds
;; VERIFY took 0.93 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.26 seconds
;; Checking the proof took 40.40 seconds
;; VERIFY took 52.95 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.29 seconds
;; Checking the proof took 21.79 seconds
;; VERIFY took 28.75 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.52 seconds
;; Checking the proof took 8.27 seconds
;; VERIFY took 11.41 seconds
4374> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-4
;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-4.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4375> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-4
;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-4.proof
;; Reading the file took 0.01 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4377> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOC-LEMMA-4
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-assoc-lemma-4.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 1.55 seconds
;; VERIFY took 2.05 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.32 seconds
;; Checking the proof took 26.50 seconds
;; VERIFY took 34.20 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.09 seconds
;; Checking the proof took 2.02 seconds
;; VERIFY took 2.69 seconds
4380> DEFINE BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/admit-build.disjoined-associativity.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4381> VERIFY BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-build.disjoined-associativity.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4382> VERIFY BUILD.DISJOINED-ASSOCIATIVITY-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-associativity-under-iff.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
4383> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-ASSOCIATIVITY
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-associativity.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 4.17 seconds
;; VERIFY took 5.47 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.40 seconds
;; Checking the proof took 35.00 seconds
;; VERIFY took 45.61 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.09 seconds
;; Checking the proof took 5.55 seconds
;; VERIFY took 7.29 seconds
4386> DEFINE BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/admit-build.disjoined-associativity-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4387> VERIFY BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-build.disjoined-associativity-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4388> VERIFY BOOLEANP-OF-BUILD.DISJOINED-ASSOCIATIVITY-OKP
;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-associativity-okp.proof
;; Reading the file took 0.34 seconds
;; Checking the proof took 5.37 seconds
;; VERIFY took 7.42 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.03 seconds
;; Checking the proof took 0.75 seconds
;; VERIFY took 0.91 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.29 seconds
;; Checking the proof took 39.40 seconds
;; VERIFY took 51.98 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.21 seconds
;; Checking the proof took 21.36 seconds
;; VERIFY took 28.24 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.49 seconds
;; Checking the proof took 8.16 seconds
;; VERIFY took 11.27 seconds
4393> DEFINE BUILD.DISJOINED-CUT-LEMMA-1
;; Reading from Proofs/level2/admit-build.disjoined-cut-lemma-1.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4394> VERIFY BUILD.DISJOINED-CUT-LEMMA-1
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-1.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4395> VERIFY BUILD.DISJOINED-CUT-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-1-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 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.10 seconds
;; Checking the proof took 3.91 seconds
;; VERIFY took 5.20 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.47 seconds
;; Checking the proof took 29.07 seconds
;; VERIFY took 38.84 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.29 seconds
;; Checking the proof took 65.91 seconds
;; VERIFY took 85.97 seconds
4399> DEFINE BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/admit-build.disjoined-cut-lemma-2.proofs
;; Reading the file took 0.03 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 seconds
4400> VERIFY BUILD.DISJOINED-CUT-LEMMA-2
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-2.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4401> VERIFY BUILD.DISJOINED-CUT-LEMMA-2-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.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.11 seconds
;; Checking the proof took 1.46 seconds
;; VERIFY took 1.98 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.50 seconds
;; Checking the proof took 65.05 seconds
;; VERIFY took 84.44 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.12 seconds
;; Checking the proof took 1.91 seconds
;; VERIFY took 2.59 seconds
4405> DEFINE BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/admit-build.disjoined-cut.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4406> VERIFY BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/thm-build.disjoined-cut.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 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.00 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4408> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-CUT
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-cut.proof
;; Reading the file took 0.18 seconds
;; Checking the proof took 5.08 seconds
;; VERIFY took 6.71 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.74 seconds
;; Checking the proof took 75.77 seconds
;; VERIFY took 98.54 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.21 seconds
;; Checking the proof took 7.65 seconds
;; VERIFY took 10.10 seconds
4411> DEFINE BUILD.DISJOINED-CUT-OKP
;; Reading from Proofs/level2/admit-build.disjoined-cut-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 seconds
4412> VERIFY BUILD.DISJOINED-CUT-OKP
;; Reading from Proofs/level2/thm-build.disjoined-cut-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 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.36 seconds
;; Checking the proof took 9.57 seconds
;; VERIFY took 12.81 seconds
4414> VERIFY BUILD.DISJOINED-CUT-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.disjoined-cut-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 1.07 seconds
;; VERIFY took 1.28 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.40 seconds
;; Checking the proof took 90.65 seconds
;; VERIFY took 117.27 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.29 seconds
;; Checking the proof took 39.52 seconds
;; VERIFY took 51.05 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 1.05 seconds
;; Checking the proof took 26.58 seconds
;; VERIFY took 35.65 seconds
4418> DEFINE BUILD.DISJOINED-MODUS-PONENS
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens.proofs
;; Reading the file took 0.05 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.05 seconds
4419> VERIFY BUILD.DISJOINED-MODUS-PONENS
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.03 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.04 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.09 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.25 seconds
;; Checking the proof took 41.46 seconds
;; VERIFY took 53.10 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.21 seconds
;; Checking the proof took 96.91 seconds
;; VERIFY took 125.73 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.31 seconds
;; Checking the proof took 85.68 seconds
;; VERIFY took 110.41 seconds
4424> DEFINE BUILD.DISJOINED-MODUS-PONENS-OKP
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-okp.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 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.26 seconds
;; Checking the proof took 4.84 seconds
;; VERIFY took 6.49 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.07 seconds
;; Checking the proof took 0.76 seconds
;; VERIFY took 0.95 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.38 seconds
;; Checking the proof took 53.84 seconds
;; VERIFY took 69.82 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.23 seconds
;; Checking the proof took 23.60 seconds
;; VERIFY took 30.51 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.88 seconds
;; Checking the proof took 19.95 seconds
;; VERIFY took 26.90 seconds
4431> DEFINE BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-2.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4432> VERIFY BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4433> VERIFY BUILD.DISJOINED-MODUS-PONENS-2-UNDER-IFF
;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.06 seconds
4434> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-MODUS-PONENS-2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-modus-ponens-2.proof
;; Reading the file took 0.27 seconds
;; Checking the proof took 37.38 seconds
;; VERIFY took 47.95 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.13 seconds
;; Checking the proof took 93.30 seconds
;; VERIFY took 120.69 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.28 seconds
;; Checking the proof took 78.02 seconds
;; VERIFY took 100.28 seconds
4437> DEFINE BUILD.DISJOINED-MODUS-PONENS-2-OKP
;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-2-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.01 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.24 seconds
;; Checking the proof took 4.72 seconds
;; VERIFY took 6.32 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.03 seconds
;; Checking the proof took 0.73 seconds
;; VERIFY took 0.88 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.36 seconds
;; Checking the proof took 53.26 seconds
;; VERIFY took 69.06 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.25 seconds
;; Checking the proof took 26.41 seconds
;; VERIFY took 34.31 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.88 seconds
;; Checking the proof took 20.04 seconds
;; VERIFY took 26.99 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.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 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.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4446> VERIFY BUILD.LHS-COMMUTE-OR-THEN-RASSOC-UNDER-IFF
;; Reading from Proofs/level2/thm-build.lhs-commute-or-then-rassoc-under-iff.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 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.06 seconds
;; Checking the proof took 1.43 seconds
;; VERIFY took 1.88 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.19 seconds
;; Checking the proof took 13.19 seconds
;; VERIFY took 16.74 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.08 seconds
;; Checking the proof took 2.03 seconds
;; VERIFY took 2.66 seconds
4450> DEFINE BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP
;; Reading from Proofs/level2/admit-build.lhs-commute-or-then-rassoc-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 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.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 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.18 seconds
;; Checking the proof took 2.37 seconds
;; VERIFY took 3.25 seconds
4453> VERIFY BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-build.lhs-commute-or-then-rassoc-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.47 seconds
;; VERIFY took 0.58 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 19.27 seconds
;; VERIFY took 25.38 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.18 seconds
;; Checking the proof took 11.05 seconds
;; VERIFY took 14.57 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.39 seconds
;; Checking the proof took 4.99 seconds
;; VERIFY took 6.97 seconds
4457> DEFINE RW.CREWRITE-TWIDDLE-BLDR
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle-bldr.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4458> VERIFY RW.CREWRITE-TWIDDLE-BLDR
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4459> VERIFY RW.CREWRITE-TWIDDLE-BLDR-UNDER-IFF
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr-under-iff.proof
;; Reading the file took 0.01 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.06 seconds
;; Checking the proof took 1.41 seconds
;; VERIFY took 1.86 seconds
4461> VERIFY FORCING-LOGIC.CONCLUSION-OF-RW.CREWRITE-TWIDDLE-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-rw.crewrite-twiddle-bldr.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 13.36 seconds
;; VERIFY took 16.92 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.22 seconds
;; Checking the proof took 1.98 seconds
;; VERIFY took 2.76 seconds
4463> DEFINE RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle-bldr-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4464> VERIFY RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4465> VERIFY BOOLEANP-OF-RW.CREWRITE-TWIDDLE-BLDR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-rw.crewrite-twiddle-bldr-okp.proof
;; Reading the file took 0.17 seconds
;; Checking the proof took 2.49 seconds
;; VERIFY took 3.35 seconds
4466> VERIFY RW.CREWRITE-TWIDDLE-BLDR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.49 seconds
;; VERIFY took 0.62 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.21 seconds
;; Checking the proof took 20.22 seconds
;; VERIFY took 26.31 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.20 seconds
;; Checking the proof took 11.58 seconds
;; VERIFY took 15.12 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.37 seconds
;; Checking the proof took 5.12 seconds
;; VERIFY took 7.07 seconds
4470> DEFINE RW.CREWRITE-TWIDDLE2-LEMMA
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-lemma.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4471> VERIFY RW.CREWRITE-TWIDDLE2-LEMMA
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-lemma.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4472> VERIFY RW.CREWRITE-TWIDDLE2-LEMMA-UNDER-IFF
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-lemma-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.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.18 seconds
;; Checking the proof took 12.15 seconds
;; VERIFY took 15.59 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.51 seconds
;; Checking the proof took 102.71 seconds
;; VERIFY took 130.38 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.13 seconds
;; Checking the proof took 19.43 seconds
;; VERIFY took 24.88 seconds
4476> DEFINE RW.CREWRITE-TWIDDLE2-BLDR
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-bldr.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 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.01 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.09 seconds
;; Checking the proof took 7.37 seconds
;; VERIFY took 9.44 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.51 seconds
;; Checking the proof took 110.77 seconds
;; VERIFY took 140.60 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.11 seconds
;; Checking the proof took 10.30 seconds
;; VERIFY took 13.22 seconds
4482> DEFINE RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-bldr-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4483> VERIFY RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-bldr-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4484> VERIFY BOOLEANP-OF-RW.CREWRITE-TWIDDLE2-BLDR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-rw.crewrite-twiddle2-bldr-okp.proof
;; Reading the file took 0.33 seconds
;; Checking the proof took 5.80 seconds
;; VERIFY took 7.82 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.03 seconds
;; Checking the proof took 0.80 seconds
;; VERIFY took 0.96 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.28 seconds
;; Checking the proof took 42.12 seconds
;; VERIFY took 54.46 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.23 seconds
;; Checking the proof took 23.17 seconds
;; VERIFY took 29.99 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.49 seconds
;; Checking the proof took 8.83 seconds
;; VERIFY took 11.92 seconds
4489> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle-lemma-1.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4490> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-lemma-1.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.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.04 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.08 seconds
4492> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle-lemma-1.proof
;; Reading the file took 0.13 seconds
;; Checking the proof took 32.64 seconds
;; VERIFY took 41.50 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.51 seconds
;; Checking the proof took 73.25 seconds
;; VERIFY took 94.14 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.27 seconds
;; Checking the proof took 178.78 seconds
;; VERIFY took 228.41 seconds
4495> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4496> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 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.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 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.18 seconds
;; Checking the proof took 11.07 seconds
;; VERIFY took 14.16 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.32 seconds
;; Checking the proof took 17.24 seconds
;; VERIFY took 22.27 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.31 seconds
;; Checking the proof took 94.16 seconds
;; VERIFY took 120.75 seconds
4501> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE-OKP
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4502> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-OKP
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.02 seconds
4503> VERIFY BOOLEANP-OF-CLAUSE.AUX-SPLIT-TWIDDLE-OKP
;; Reading from Proofs/level2/thm-booleanp-of-clause.aux-split-twiddle-okp.proof
;; Reading the file took 0.24 seconds
;; Checking the proof took 4.55 seconds
;; VERIFY took 6.10 seconds
4504> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.71 seconds
;; VERIFY took 0.85 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.24 seconds
;; Checking the proof took 41.22 seconds
;; VERIFY took 53.26 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.21 seconds
;; Checking the proof took 28.09 seconds
;; VERIFY took 36.35 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.58 seconds
;; Checking the proof took 12.93 seconds
;; VERIFY took 17.40 seconds
4508> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1A
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-lemma-1a.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4509> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1A
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-1a.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4510> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1A-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-1a-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 seconds
4511> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1A
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle2-lemma-1a.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 3.05 seconds
;; VERIFY took 3.97 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.51 seconds
;; Checking the proof took 28.09 seconds
;; VERIFY took 36.28 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.09 seconds
;; Checking the proof took 5.43 seconds
;; VERIFY took 7.05 seconds
4514> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-lemma-1.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4515> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-1.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4516> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-1-under-iff.proof
;; Reading the file took 0.01 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.08 seconds
;; Checking the proof took 9.24 seconds
;; VERIFY took 11.74 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.52 seconds
;; Checking the proof took 98.27 seconds
;; VERIFY took 125.57 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.32 seconds
;; Checking the proof took 120.32 seconds
;; VERIFY took 154.46 seconds
4520> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-lemma-2a.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4521> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2a.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4522> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2a-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.02 seconds
;; VERIFY took 0.04 seconds
4523> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle2-lemma-2a.proof
;; Reading the file took 0.10 seconds
;; Checking the proof took 12.52 seconds
;; VERIFY took 16.08 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.39 seconds
;; Checking the proof took 37.23 seconds
;; VERIFY took 47.88 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.11 seconds
;; Checking the proof took 22.92 seconds
;; VERIFY took 29.42 seconds
4526> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-lemma-2.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4527> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4528> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.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.09 seconds
;; Checking the proof took 9.14 seconds
;; VERIFY took 11.68 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.36 seconds
;; Checking the proof took 111.35 seconds
;; VERIFY took 141.41 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.13 seconds
;; Checking the proof took 14.84 seconds
;; VERIFY took 18.97 seconds
4532> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4533> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4534> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-UNDER-IFF
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-under-iff.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.05 seconds
4535> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-TWIDDLE2
;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-twiddle2.proof
;; Reading the file took 0.20 seconds
;; Checking the proof took 17.94 seconds
;; VERIFY took 22.74 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.37 seconds
;; Checking the proof took 25.01 seconds
;; VERIFY took 31.91 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.49 seconds
;; Checking the proof took 100.89 seconds
;; VERIFY took 129.00 seconds
4538> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-OKP
;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-okp.proofs
;; Reading the file took 0.11 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.11 seconds
4539> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-OKP
;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.03 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.28 seconds
;; Checking the proof took 5.71 seconds
;; VERIFY took 7.68 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.03 seconds
;; Checking the proof took 0.80 seconds
;; VERIFY took 0.95 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.27 seconds
;; Checking the proof took 41.94 seconds
;; VERIFY took 54.26 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.21 seconds
;; Checking the proof took 22.87 seconds
;; VERIFY took 29.66 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.47 seconds
;; Checking the proof took 8.75 seconds
;; VERIFY took 11.82 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.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.02 seconds
4546> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr.proof
;; Reading the file took 0.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.03 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 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.06 seconds
;; Checking the proof took 2.11 seconds
;; VERIFY took 2.71 seconds
4549> VERIFY FORCING-LOGIC.CONCLUSION-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-clause.aux-split-default-3-bldr.proof
;; Reading the file took 0.32 seconds
;; Checking the proof took 20.16 seconds
;; VERIFY took 25.82 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.20 seconds
;; Checking the proof took 17.48 seconds
;; VERIFY took 22.36 seconds
4551> DEFINE CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/admit-clause.aux-split-default-3-bldr-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4552> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.01 seconds
4553> VERIFY BOOLEANP-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP
;; Reading from Proofs/level2/thm-booleanp-of-clause.aux-split-default-3-bldr-okp.proof
;; Reading the file took 0.19 seconds
;; Checking the proof took 2.60 seconds
;; VERIFY took 3.50 seconds
4554> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP-OF-LOGIC.APPEAL-IDENTITY
;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr-okp-of-logic.appeal-identity.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.52 seconds
;; VERIFY took 0.62 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.20 seconds
;; Checking the proof took 21.22 seconds
;; VERIFY took 27.30 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 12.08 seconds
;; VERIFY took 15.61 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 5.35 seconds
;; VERIFY took 7.30 seconds
4558> DEFINE CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR
;; Reading from Proofs/level2/admit-clause.aux-limsplit-cutoff-step-bldr.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4559> VERIFY CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR
;; Reading from Proofs/level2/thm-clause.aux-limsplit-cutoff-step-bldr.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.04 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.03 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.06 seconds
;; Checking the proof took 1.51 seconds
;; VERIFY took 1.96 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.23 seconds
;; Checking the proof took 13.58 seconds
;; VERIFY took 17.18 seconds
4563> VERIFY FORCING-LOGIC.PROOFP-OF-CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR
;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-clause.aux-limsplit-cutoff-step-bldr.proof
;; Reading the file took 0.07 seconds
;; Checking the proof took 2.13 seconds
;; VERIFY took 2.75 seconds
4564> DEFINE CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-OKP
;; Reading from Proofs/level2/admit-clause.aux-limsplit-cutoff-step-bldr-okp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4565> VERIFY CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-OKP
;; Reading from Proofs/level2/thm-clause.aux-limsplit-cutoff-step-bldr-okp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 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.16 seconds
;; Checking the proof took 2.59 seconds
;; VERIFY took 3.44 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.51 seconds
;; VERIFY took 0.62 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.20 seconds
;; Checking the proof took 20.92 seconds
;; VERIFY took 27.01 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.19 seconds
;; Checking the proof took 12.05 seconds
;; VERIFY took 15.59 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.37 seconds
;; Checking the proof took 5.31 seconds
;; VERIFY took 7.27 seconds
4571> DEFINE LEVEL2.STEP-OKP
;; Reading from Proofs/level2/admit-level2.step-okp.proofs
;; Reading the file took 0.02 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.03 seconds
4572> VERIFY LEVEL2.STEP-OKP
;; Reading from Proofs/level2/thm-level2.step-okp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.01 seconds
;; VERIFY took 0.04 seconds
4573> VERIFY SOUNDNESS-OF-LEVEL2.STEP-OKP
;; Reading from Proofs/level2/thm-soundness-of-level2.step-okp.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 3.86 seconds
;; VERIFY took 5.45 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.77 seconds
;; Checking the proof took 22.17 seconds
;; VERIFY took 30.50 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.24 seconds
;; Checking the proof took 3.85 seconds
;; VERIFY took 5.10 seconds
4576> DEFINE LEVEL2.FLAG-PROOFP
;; Reading from Proofs/level2/admit-level2.flag-proofp.proofs
;; Reading the file took 0.21 seconds
;; Checking the proofs took 1.42 seconds
;; DEFINE took 1.97 seconds
4577> VERIFY LEVEL2.FLAG-PROOFP
;; Reading from Proofs/level2/thm-level2.flag-proofp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.02 seconds
4578> DEFINE LEVEL2.PROOFP
;; Reading from Proofs/level2/admit-level2.proofp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4579> VERIFY LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-level2.proofp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4580> DEFINE LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/admit-level2.proof-listp.proofs
;; Reading the file took 0.00 seconds
;; Checking the proofs took 0.00 seconds
;; DEFINE took 0.00 seconds
4581> VERIFY LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proof-listp.proof
;; Reading the file took 0.01 seconds
;; Checking the proof took 0.00 seconds
;; VERIFY took 0.01 seconds
4582> VERIFY DEFINITION-OF-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-definition-of-level2.proofp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.06 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.05 seconds
;; Checking the proof took 0.21 seconds
;; VERIFY took 0.32 seconds
4584> VERIFY LEVEL2.PROOFP-WHEN-NOT-CONSP
;; Reading from Proofs/level2/thm-level2.proofp-when-not-consp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.08 seconds
4585> VERIFY LEVEL2.PROOF-LISTP-WHEN-NOT-CONSP
;; Reading from Proofs/level2/thm-level2.proof-listp-when-not-consp.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.05 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.03 seconds
;; Checking the proof took 0.07 seconds
;; VERIFY took 0.11 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.41 seconds
;; Checking the proof took 3.54 seconds
;; VERIFY took 4.80 seconds
4588> VERIFY BOOLEANP-OF-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-booleanp-of-level2.proofp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.17 seconds
4589> VERIFY BOOLEANP-OF-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-booleanp-of-level2.proof-listp.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.12 seconds
;; VERIFY took 0.17 seconds
4590> VERIFY LEVEL2.PROOF-LISTP-OF-LIST-FIX
;; Reading from Proofs/level2/thm-level2.proof-listp-of-list-fix.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 1.28 seconds
;; VERIFY took 1.86 seconds
4591> VERIFY LEVEL2.PROOF-LISTP-OF-APP
;; Reading from Proofs/level2/thm-level2.proof-listp-of-app.proof
;; Reading the file took 0.39 seconds
;; Checking the proof took 2.66 seconds
;; VERIFY took 3.92 seconds
4592> VERIFY LEVEL2.PROOF-LISTP-OF-REV
;; Reading from Proofs/level2/thm-level2.proof-listp-of-rev.proof
;; Reading the file took 0.21 seconds
;; Checking the proof took 1.35 seconds
;; VERIFY took 1.95 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.06 seconds
;; Checking the proof took 0.17 seconds
;; VERIFY took 0.28 seconds
4594> VERIFY LEVEL2.PROOF-LISTP-OF-CDR-WHEN-LEVEL2.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proof-listp-of-cdr-when-level2.proof-listp.proof
;; Reading the file took 0.06 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.19 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.16 seconds
;; Checking the proof took 0.98 seconds
;; VERIFY took 1.39 seconds
4596> VERIFY LEVEL2.PROOFP-WHEN-MEMBERP-OF-LEVEL2.PROOF-LISTP-ALT
;; Reading from Proofs/level2/thm-level2.proofp-when-memberp-of-level2.proof-listp-alt.proof
;; Reading the file took 0.04 seconds
;; Checking the proof took 0.10 seconds
;; VERIFY took 0.17 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.17 seconds
;; Checking the proof took 0.85 seconds
;; VERIFY took 1.22 seconds
4598> VERIFY LEVEL2.PROOF-LISTP-OF-REMOVE-DUPLICATES
;; Reading from Proofs/level2/thm-level2.proof-listp-of-remove-duplicates.proof
;; Reading the file took 0.25 seconds
;; Checking the proof took 1.45 seconds
;; VERIFY took 2.12 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.16 seconds
;; Checking the proof took 0.82 seconds
;; VERIFY took 1.18 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.17 seconds
;; Checking the proof took 1.11 seconds
;; VERIFY took 1.55 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.04 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.09 seconds
4602> VERIFY LEVEL2.PROOF-LISTP-OF-REPEAT
;; Reading from Proofs/level2/thm-level2.proof-listp-of-repeat.proof
;; Reading the file took 0.22 seconds
;; Checking the proof took 0.93 seconds
;; VERIFY took 1.39 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.30 seconds
;; Checking the proof took 16.81 seconds
;; VERIFY took 22.86 seconds
4604> VERIFY LOGIC.PROVABLEP-WHEN-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-logic.provablep-when-level2.proofp.proof
;; Reading the file took 0.08 seconds
;; Checking the proof took 0.43 seconds
;; VERIFY took 0.64 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.07 seconds
;; Checking the proof took 0.43 seconds
;; VERIFY took 0.63 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.57 seconds
;; Checking the proof took 5.18 seconds
;; VERIFY took 7.12 seconds
4607> VERIFY LEVEL2.PROOFP-WHEN-LOGIC.PROOFP
;; Reading from Proofs/level2/thm-level2.proofp-when-logic.proofp.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.28 seconds
4608> VERIFY LEVEL2.PROOF-LISTP-WHEN-LOGIC.PROOF-LISTP
;; Reading from Proofs/level2/thm-level2.proof-listp-when-logic.proof-listp.proof
;; Reading the file took 0.05 seconds
;; Checking the proof took 0.18 seconds
;; VERIFY took 0.28 seconds
4609> VERIFY FORCING-LEVEL2.PROOFP-OF-LOGIC.PROVABLE-WITNESS
;; Reading from Proofs/level2/thm-forcing-level2.proofp-of-logic.provable-witness.proof
;; Reading the file took 0.03 seconds
;; Checking the proof took 0.03 seconds
;; VERIFY took 0.07 seconds
4610> VERIFY INSTALL-NEW-PROOFP-LEVEL2.PROOFP
;; Reading from Proofs/level2/thm-install-new-proofp-level2.proofp.proof
;; Reading the file took 0.02 seconds
;; Checking the proof took 0.04 seconds
;; VERIFY took 0.07 seconds
4611 > SWITCH LEVEL2.PROOFP
;; SWITCH took 0.00 seconds
4612 > FINISH level2
; Exiting

real	98m56.906s
user	98m29.713s
sys	0m2.748s