i i i i i i i ooooo o ooooooo ooooo ooooo I I I I I I I 8 8 8 8 8 o 8 8 I \ `+' / I 8 8 8 8 8 8 \ `-+-' / 8 8 8 ooooo 8oooo `-__|__-' 8 8 8 8 8 | 8 o 8 8 o 8 8 ------+------ ooooo 8oooooo ooo8ooo ooooo 8 Welcome to GNU CLISP 2.47 (2008-10-23) Copyright (c) Bruno Haible, Michael Stoll 1992, 1993 Copyright (c) Bruno Haible, Marcus Daniels 1994-1997 Copyright (c) Bruno Haible, Pierpaolo Bernardi, Sam Steingold 1998 Copyright (c) Bruno Haible, Sam Steingold 1999-2000 Copyright (c) Sam Steingold, Bruno Haible 2001-2008 Type :h and hit Enter for context help. Milawa Proof Checker. 4010> DEFINE BUILD.AXIOM ;; Reading from Proofs/level2/admit-build.axiom.proofs ;; Reading the file took 0.05 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.05 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.02 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.02 seconds ;; VERIFY took 0.05 seconds 4013> VERIFY LOGIC.METHOD-OF-BUILD.AXIOM ;; Reading from Proofs/level2/thm-logic.method-of-build.axiom.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.04 seconds 4014> VERIFY LOGIC.CONCLUSION-OF-BUILD.AXIOM ;; Reading from Proofs/level2/thm-logic.conclusion-of-build.axiom.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.08 seconds 4015> VERIFY LOGIC.SUBPROOFS-OF-BUILD.AXIOM ;; Reading from Proofs/level2/thm-logic.subproofs-of-build.axiom.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.06 seconds 4016> VERIFY LOGIC.EXTRAS-OF-BUILD.AXIOM ;; Reading from Proofs/level2/thm-logic.extras-of-build.axiom.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.06 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.15 seconds ;; VERIFY took 0.22 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.13 seconds ;; Checking the proof took 0.95 seconds ;; VERIFY took 1.46 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.02 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4021> VERIFY BUILD.THEOREM-UNDER-IFF ;; Reading from Proofs/level2/thm-build.theorem-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.04 seconds 4022> VERIFY LOGIC.METHOD-OF-BUILD.THEOREM ;; Reading from Proofs/level2/thm-logic.method-of-build.theorem.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.04 seconds 4023> VERIFY LOGIC.CONCLUSION-OF-BUILD.THEOREM ;; Reading from Proofs/level2/thm-logic.conclusion-of-build.theorem.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.04 seconds 4024> VERIFY LOGIC.SUBPROOFS-OF-BUILD.THEOREM ;; Reading from Proofs/level2/thm-logic.subproofs-of-build.theorem.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.06 seconds 4025> VERIFY LOGIC.EXTRAS-OF-BUILD.THEOREM ;; Reading from Proofs/level2/thm-logic.extras-of-build.theorem.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.07 seconds 4026> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.THEOREM ;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.theorem.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.15 seconds ;; VERIFY took 0.24 seconds 4027> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.THEOREM ;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.theorem.proof ;; Reading the file took 0.05 seconds ;; Checking the proof took 0.97 seconds ;; VERIFY took 1.41 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.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4030> VERIFY BUILD.PROPOSITIONAL-SCHEMA-UNDER-IFF ;; Reading from Proofs/level2/thm-build.propositional-schema-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.05 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.03 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.06 seconds 4032> VERIFY LOGIC.CONCLUSION-OF-BUILD.PROPOSITIONAL-SCHEMA ;; Reading from Proofs/level2/thm-logic.conclusion-of-build.propositional-schema.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.06 seconds ;; VERIFY took 0.09 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.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.06 seconds 4034> VERIFY LOGIC.EXTRAS-OF-BUILD.PROPOSITIONAL-SCHEMA ;; Reading from Proofs/level2/thm-logic.extras-of-build.propositional-schema.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.05 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.04 seconds ;; Checking the proof took 0.23 seconds ;; VERIFY took 0.34 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 1.13 seconds ;; VERIFY took 1.59 seconds 4037> DEFINE BUILD.CUT ;; Reading from Proofs/level2/admit-build.cut.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4038> VERIFY BUILD.CUT ;; Reading from Proofs/level2/thm-build.cut.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4039> VERIFY BUILD.CUT-UNDER-IFF ;; Reading from Proofs/level2/thm-build.cut-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.06 seconds 4040> VERIFY LOGIC.METHOD-OF-BUILD.CUT ;; Reading from Proofs/level2/thm-logic.method-of-build.cut.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.05 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.08 seconds ;; VERIFY took 0.12 seconds 4042> VERIFY LOGIC.SUBPROOFS-OF-BUILD.CUT ;; Reading from Proofs/level2/thm-logic.subproofs-of-build.cut.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 0.19 seconds ;; VERIFY took 0.26 seconds 4043> VERIFY LOGIC.EXTRAS-OF-BUILD.CUT ;; Reading from Proofs/level2/thm-logic.extras-of-build.cut.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.06 seconds 4044> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.CUT ;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.cut.proof ;; Reading the file took 0.08 seconds ;; Checking the proof took 1.48 seconds ;; VERIFY took 2.26 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.25 seconds ;; Checking the proof took 6.39 seconds ;; VERIFY took 9.89 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.03 seconds ;; VERIFY took 0.04 seconds 4049> VERIFY LOGIC.METHOD-OF-BUILD.CONTRACTION ;; Reading from Proofs/level2/thm-logic.method-of-build.contraction.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.05 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.03 seconds ;; VERIFY took 0.05 seconds 4051> VERIFY LOGIC.SUBPROOFS-OF-BUILD.CONTRACTION ;; Reading from Proofs/level2/thm-logic.subproofs-of-build.contraction.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.10 seconds ;; VERIFY took 0.12 seconds 4052> VERIFY LOGIC.EXTRAS-OF-BUILD.CONTRACTION ;; Reading from Proofs/level2/thm-logic.extras-of-build.contraction.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.05 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.55 seconds ;; VERIFY took 0.83 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 1.90 seconds ;; VERIFY took 2.80 seconds 4055> DEFINE BUILD.EXPANSION ;; Reading from Proofs/level2/admit-build.expansion.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4056> VERIFY BUILD.EXPANSION ;; Reading from Proofs/level2/thm-build.expansion.proof ;; Reading the file took 0.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.01 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.05 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.02 seconds ;; VERIFY took 0.04 seconds 4059> VERIFY LOGIC.CONCLUSION-OF-BUILD.EXPANSION ;; Reading from Proofs/level2/thm-logic.conclusion-of-build.expansion.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.06 seconds ;; VERIFY took 0.09 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.10 seconds ;; VERIFY took 0.14 seconds 4061> VERIFY LOGIC.EXTRAS-OF-BUILD.EXPANSION ;; Reading from Proofs/level2/thm-logic.extras-of-build.expansion.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.06 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.03 seconds ;; Checking the proof took 0.34 seconds ;; VERIFY took 0.50 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.08 seconds ;; Checking the proof took 1.29 seconds ;; VERIFY took 1.87 seconds 4064> DEFINE BUILD.ASSOCIATIVITY ;; Reading from Proofs/level2/admit-build.associativity.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4065> VERIFY BUILD.ASSOCIATIVITY ;; Reading from Proofs/level2/thm-build.associativity.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4066> VERIFY BUILD.ASSOCIATIVITY-UNDER-IFF ;; Reading from Proofs/level2/thm-build.associativity-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.07 seconds 4067> VERIFY LOGIC.METHOD-OF-BUILD.ASSOCIATIVITY ;; Reading from Proofs/level2/thm-logic.method-of-build.associativity.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.06 seconds 4068> VERIFY LOGIC.CONCLUSION-OF-BUILD.ASSOCIATIVITY ;; Reading from Proofs/level2/thm-logic.conclusion-of-build.associativity.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.13 seconds ;; VERIFY took 0.21 seconds 4069> VERIFY LOGIC.SUBPROOFS-OF-BUILD.ASSOCIATIVITY ;; Reading from Proofs/level2/thm-logic.subproofs-of-build.associativity.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 0.11 seconds ;; VERIFY took 0.16 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.04 seconds ;; VERIFY took 0.07 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 1.16 seconds ;; VERIFY took 1.72 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.13 seconds ;; Checking the proof took 3.79 seconds ;; VERIFY took 5.45 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.02 seconds 4075> VERIFY BUILD.INSTANTIATION-UNDER-IFF ;; Reading from Proofs/level2/thm-build.instantiation-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.06 seconds ;; VERIFY took 0.10 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.45 seconds ;; VERIFY took 0.66 seconds 4077> VERIFY LOGIC.CONCLUSION-OF-BUILD.INSTANTIATION ;; Reading from Proofs/level2/thm-logic.conclusion-of-build.instantiation.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.23 seconds ;; VERIFY took 0.34 seconds 4078> VERIFY LOGIC.SUBPROOFS-OF-BUILD.INSTANTIATION ;; Reading from Proofs/level2/thm-logic.subproofs-of-build.instantiation.proof ;; Reading the file took 0.09 seconds ;; Checking the proof took 1.87 seconds ;; VERIFY took 2.88 seconds 4079> VERIFY LOGIC.EXTRAS-OF-BUILD.INSTANTIATION ;; Reading from Proofs/level2/thm-logic.extras-of-build.instantiation.proof ;; Reading the file took 0.06 seconds ;; Checking the proof took 0.44 seconds ;; VERIFY took 0.68 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.13 seconds ;; Checking the proof took 0.74 seconds ;; VERIFY took 1.19 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.17 seconds ;; Checking the proof took 3.05 seconds ;; VERIFY took 4.66 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.01 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.04 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.02 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.05 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.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.05 seconds 4087> VERIFY LOGIC.SUBPROOFS-OF-BUILD.FUNCTIONAL-EQUALITY ;; Reading from Proofs/level2/thm-logic.subproofs-of-build.functional-equality.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.07 seconds 4088> VERIFY LOGIC.EXTRAS-OF-BUILD.FUNCTIONAL-EQUALITY ;; Reading from Proofs/level2/thm-logic.extras-of-build.functional-equality.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.06 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.08 seconds ;; Checking the proof took 0.57 seconds ;; VERIFY took 0.87 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.19 seconds ;; Checking the proof took 3.28 seconds ;; VERIFY took 4.96 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.03 seconds ;; VERIFY took 0.05 seconds 4094> VERIFY LOGIC.METHOD-OF-BUILD.BETA-REDUCTION ;; Reading from Proofs/level2/thm-logic.method-of-build.beta-reduction.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.05 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.11 seconds ;; VERIFY took 0.16 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.06 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.10 seconds 4097> VERIFY LOGIC.EXTRAS-OF-BUILD.BETA-REDUCTION ;; Reading from Proofs/level2/thm-logic.extras-of-build.beta-reduction.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.08 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.11 seconds ;; Checking the proof took 1.71 seconds ;; VERIFY took 2.54 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.20 seconds ;; Checking the proof took 5.54 seconds ;; VERIFY took 8.45 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.02 seconds 4102> VERIFY BUILD.BASE-EVAL-UNDER-IFF ;; Reading from Proofs/level2/thm-build.base-eval-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.05 seconds 4103> VERIFY LOGIC.METHOD-OF-BUILD.BASE-EVAL ;; Reading from Proofs/level2/thm-logic.method-of-build.base-eval.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.05 seconds 4104> VERIFY LOGIC.CONCLUSION-OF-BUILD.BASE-EVAL ;; Reading from Proofs/level2/thm-logic.conclusion-of-build.base-eval.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.06 seconds ;; VERIFY took 0.09 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.03 seconds ;; VERIFY took 0.06 seconds 4106> VERIFY LOGIC.EXTRAS-OF-BUILD.BASE-EVAL ;; Reading from Proofs/level2/thm-logic.extras-of-build.base-eval.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.05 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.05 seconds ;; Checking the proof took 0.28 seconds ;; VERIFY took 0.44 seconds 4108> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.BASE-EVAL ;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.base-eval.proof ;; Reading the file took 0.07 seconds ;; Checking the proof took 1.34 seconds ;; VERIFY took 1.93 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.31 seconds ;; DEFINE took 0.43 seconds 4110> VERIFY BUILD.INSTANTIATION-LIST ;; Reading from Proofs/level2/thm-build.instantiation-list.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 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.06 seconds ;; Checking the proof took 0.09 seconds ;; VERIFY took 0.17 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.15 seconds ;; VERIFY took 0.20 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.25 seconds ;; Checking the proof took 3.99 seconds ;; VERIFY took 5.92 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.24 seconds ;; Checking the proof took 3.87 seconds ;; VERIFY took 5.70 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.46 seconds ;; Checking the proof took 5.51 seconds ;; VERIFY took 8.49 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.02 seconds 4118> VERIFY BUILD.INDUCTION-UNDER-IFF ;; Reading from Proofs/level2/thm-build.induction-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.06 seconds 4119> VERIFY LOGIC.METHOD-OF-BUILD.INDUCTION ;; Reading from Proofs/level2/thm-logic.method-of-build.induction.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.05 seconds 4120> VERIFY LOGIC.CONCLUSION-OF-BUILD.INDUCTION ;; Reading from Proofs/level2/thm-logic.conclusion-of-build.induction.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.06 seconds 4121> VERIFY LOGIC.SUBPROOFS-OF-BUILD.INDUCTION ;; Reading from Proofs/level2/thm-logic.subproofs-of-build.induction.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.08 seconds 4122> VERIFY LOGIC.EXTRAS-OF-BUILD.INDUCTION ;; Reading from Proofs/level2/thm-logic.extras-of-build.induction.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.30 seconds ;; VERIFY took 0.40 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.03 seconds ;; Checking the proof took 0.29 seconds ;; VERIFY took 0.43 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.39 seconds ;; Checking the proof took 13.76 seconds ;; VERIFY took 21.79 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.02 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4127> VERIFY BUILD.COMMUTE-OR-UNDER-IFF ;; Reading from Proofs/level2/thm-build.commute-or-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.06 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.06 seconds ;; Checking the proof took 0.65 seconds ;; VERIFY took 1.00 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.16 seconds ;; VERIFY took 0.24 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.10 seconds ;; Checking the proof took 0.74 seconds ;; VERIFY took 1.19 seconds 4131> DEFINE BUILD.COMMUTE-OR-OKP ;; Reading from Proofs/level2/admit-build.commute-or-okp.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.02 seconds 4132> VERIFY BUILD.COMMUTE-OR-OKP ;; Reading from Proofs/level2/thm-build.commute-or-okp.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.01 seconds ;; VERIFY took 0.04 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.22 seconds ;; Checking the proof took 3.17 seconds ;; VERIFY took 4.76 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.04 seconds ;; Checking the proof took 0.94 seconds ;; VERIFY took 1.24 seconds 4135> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.COMMUTE-OR-OKP ;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.commute-or-okp.proof ;; Reading the file took 0.22 seconds ;; Checking the proof took 27.58 seconds ;; VERIFY took 41.74 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.30 seconds ;; Checking the proof took 17.41 seconds ;; VERIFY took 26.41 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.52 seconds ;; Checking the proof took 9.47 seconds ;; VERIFY took 15.13 seconds 4138> DEFINE BUILD.RIGHT-EXPANSION ;; Reading from Proofs/level2/admit-build.right-expansion.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4139> VERIFY BUILD.RIGHT-EXPANSION ;; Reading from Proofs/level2/thm-build.right-expansion.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.03 seconds 4140> VERIFY BUILD.RIGHT-EXPANSION-UNDER-IFF ;; Reading from Proofs/level2/thm-build.right-expansion-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.07 seconds 4141> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.RIGHT-EXPANSION ;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.right-expansion.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.23 seconds ;; VERIFY took 0.37 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.12 seconds ;; Checking the proof took 1.40 seconds ;; VERIFY took 2.09 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.05 seconds ;; Checking the proof took 0.43 seconds ;; VERIFY took 0.68 seconds 4144> DEFINE BUILD.RIGHT-EXPANSION-OKP ;; Reading from Proofs/level2/admit-build.right-expansion-okp.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4145> VERIFY BUILD.RIGHT-EXPANSION-OKP ;; Reading from Proofs/level2/thm-build.right-expansion-okp.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.01 seconds ;; VERIFY took 0.04 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.13 seconds ;; Checking the proof took 2.06 seconds ;; VERIFY took 3.07 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.03 seconds ;; Checking the proof took 0.65 seconds ;; VERIFY took 0.84 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.44 seconds ;; Checking the proof took 41.93 seconds ;; VERIFY took 63.73 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.26 seconds ;; Checking the proof took 9.42 seconds ;; VERIFY took 14.34 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.41 seconds ;; Checking the proof took 6.80 seconds ;; VERIFY took 10.89 seconds 4151> DEFINE BUILD.MODUS-PONENS ;; Reading from Proofs/level2/admit-build.modus-ponens.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.02 seconds 4152> VERIFY BUILD.MODUS-PONENS ;; Reading from Proofs/level2/thm-build.modus-ponens.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.04 seconds 4153> VERIFY BUILD.MODUS-PONENS-UNDER-IFF ;; Reading from Proofs/level2/thm-build.modus-ponens-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.05 seconds ;; VERIFY took 0.08 seconds 4154> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.MODUS-PONENS ;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.modus-ponens.proof ;; Reading the file took 0.07 seconds ;; Checking the proof took 2.84 seconds ;; VERIFY took 4.25 seconds 4155> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.MODUS-PONENS ;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.modus-ponens.proof ;; Reading the file took 0.19 seconds ;; Checking the proof took 3.89 seconds ;; VERIFY took 5.85 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.33 seconds ;; Checking the proof took 36.54 seconds ;; VERIFY took 54.78 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.02 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.02 seconds ;; VERIFY took 0.04 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.14 seconds ;; Checking the proof took 3.97 seconds ;; VERIFY took 5.70 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.06 seconds ;; Checking the proof took 1.23 seconds ;; VERIFY took 1.60 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.39 seconds ;; Checking the proof took 52.72 seconds ;; VERIFY took 78.04 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.26 seconds ;; Checking the proof took 24.54 seconds ;; VERIFY took 36.17 seconds 4163> VERIFY FORCING-SOUNDNESS-OF-BUILD.MODUS-PONENS-OKP ;; Reading from Proofs/level2/thm-forcing-soundness-of-build.modus-ponens-okp.proof ;; Reading the file took 1.01 seconds ;; Checking the proof took 30.22 seconds ;; VERIFY took 46.76 seconds 4164> DEFINE BUILD.MODUS-PONENS-2 ;; Reading from Proofs/level2/admit-build.modus-ponens-2.proofs ;; Reading the file took 0.03 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.03 seconds 4165> VERIFY BUILD.MODUS-PONENS-2 ;; Reading from Proofs/level2/thm-build.modus-ponens-2.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.05 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.05 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.11 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.13 seconds ;; Checking the proof took 3.07 seconds ;; VERIFY took 4.63 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.04 seconds ;; Checking the proof took 0.28 seconds ;; VERIFY took 0.45 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.29 seconds ;; Checking the proof took 41.03 seconds ;; VERIFY took 61.18 seconds 4170> DEFINE BUILD.MODUS-PONENS-2-OKP ;; Reading from Proofs/level2/admit-build.modus-ponens-2-okp.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.02 seconds 4171> VERIFY BUILD.MODUS-PONENS-2-OKP ;; Reading from Proofs/level2/thm-build.modus-ponens-2-okp.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.03 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.13 seconds ;; Checking the proof took 3.75 seconds ;; VERIFY took 5.41 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.05 seconds ;; Checking the proof took 1.15 seconds ;; VERIFY took 1.50 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.36 seconds ;; Checking the proof took 51.23 seconds ;; VERIFY took 75.95 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.26 seconds ;; Checking the proof took 29.46 seconds ;; VERIFY took 43.39 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.96 seconds ;; Checking the proof took 29.78 seconds ;; VERIFY took 46.04 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.02 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.04 seconds ;; VERIFY took 0.10 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.11 seconds ;; Checking the proof took 11.30 seconds ;; VERIFY took 16.56 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.51 seconds ;; Checking the proof took 104.16 seconds ;; VERIFY took 148.20 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.14 seconds ;; Checking the proof took 18.05 seconds ;; VERIFY took 26.73 seconds 4183> DEFINE BUILD.RIGHT-ASSOCIATIVITY-OKP ;; Reading from Proofs/level2/admit-build.right-associativity-okp.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.03 seconds 4184> VERIFY BUILD.RIGHT-ASSOCIATIVITY-OKP ;; Reading from Proofs/level2/thm-build.right-associativity-okp.proof ;; Reading the file took 0.07 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.10 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.36 seconds ;; Checking the proof took 9.10 seconds ;; VERIFY took 13.80 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.05 seconds ;; Checking the proof took 1.80 seconds ;; VERIFY took 2.34 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.32 seconds ;; Checking the proof took 73.47 seconds ;; VERIFY took 110.22 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.33 seconds ;; Checking the proof took 42.18 seconds ;; VERIFY took 63.28 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.66 seconds ;; Checking the proof took 18.28 seconds ;; VERIFY took 28.38 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.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.01 seconds 4192> VERIFY BUILD.DISJOINED-LEFT-EXPANSION-UNDER-IFF ;; Reading from Proofs/level2/thm-build.disjoined-left-expansion-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.07 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.08 seconds ;; Checking the proof took 1.32 seconds ;; VERIFY took 2.02 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.30 seconds ;; Checking the proof took 14.79 seconds ;; VERIFY took 21.22 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 2.32 seconds ;; VERIFY took 3.55 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.04 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.02 seconds ;; VERIFY took 0.04 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.33 seconds ;; Checking the proof took 7.38 seconds ;; VERIFY took 11.25 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.05 seconds ;; Checking the proof took 1.36 seconds ;; VERIFY took 1.78 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.57 seconds ;; Checking the proof took 103.11 seconds ;; VERIFY took 155.13 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.38 seconds ;; Checking the proof took 26.20 seconds ;; VERIFY took 39.42 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.67 seconds ;; Checking the proof took 16.69 seconds ;; VERIFY took 26.08 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.05 seconds ;; VERIFY took 0.08 seconds 4206> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-RIGHT-EXPANSION ;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-right-expansion.proof ;; Reading the file took 0.08 seconds ;; Checking the proof took 5.49 seconds ;; VERIFY took 8.23 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.51 seconds ;; Checking the proof took 27.18 seconds ;; VERIFY took 39.84 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.08 seconds ;; Checking the proof took 9.87 seconds ;; VERIFY took 14.92 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.02 seconds 4210> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION-OKP ;; Reading from Proofs/level2/thm-build.disjoined-right-expansion-okp.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.06 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.30 seconds ;; Checking the proof took 7.44 seconds ;; VERIFY took 11.26 seconds 4212> VERIFY BUILD.DISJOINED-RIGHT-EXPANSION-OKP-OF-LOGIC.APPEAL-IDENTITY ;; Reading from Proofs/level2/thm-build.disjoined-right-expansion-okp-of-logic.appeal-identity.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 1.38 seconds ;; VERIFY took 1.77 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.57 seconds ;; Checking the proof took 104.17 seconds ;; VERIFY took 156.26 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.33 seconds ;; Checking the proof took 26.58 seconds ;; VERIFY took 39.76 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.69 seconds ;; Checking the proof took 17.08 seconds ;; VERIFY took 26.57 seconds 4216> DEFINE BUILD.DISJOINED-CONTRACTION ;; Reading from Proofs/level2/admit-build.disjoined-contraction.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.02 seconds 4217> VERIFY BUILD.DISJOINED-CONTRACTION ;; Reading from Proofs/level2/thm-build.disjoined-contraction.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.05 seconds 4218> VERIFY BUILD.DISJOINED-CONTRACTION-UNDER-IFF ;; Reading from Proofs/level2/thm-build.disjoined-contraction-under-iff.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 0.06 seconds ;; VERIFY took 0.11 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.21 seconds ;; Checking the proof took 15.67 seconds ;; VERIFY took 23.05 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.16 seconds ;; Checking the proof took 3.83 seconds ;; VERIFY took 5.63 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.36 seconds ;; Checking the proof took 63.17 seconds ;; VERIFY took 92.13 seconds 4222> DEFINE BUILD.DISJOINED-CONTRACTION-OKP ;; Reading from Proofs/level2/admit-build.disjoined-contraction-okp.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.03 seconds 4223> VERIFY BUILD.DISJOINED-CONTRACTION-OKP ;; Reading from Proofs/level2/thm-build.disjoined-contraction-okp.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.04 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.25 seconds ;; Checking the proof took 7.26 seconds ;; VERIFY took 10.75 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 1.66 seconds ;; VERIFY took 2.17 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.34 seconds ;; Checking the proof took 75.63 seconds ;; VERIFY took 112.38 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.32 seconds ;; Checking the proof took 56.60 seconds ;; VERIFY took 83.90 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.76 seconds ;; Checking the proof took 30.86 seconds ;; VERIFY took 47.23 seconds 4229> DEFINE BUILD.CANCEL-NEG-NEG ;; Reading from Proofs/level2/admit-build.cancel-neg-neg.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4230> VERIFY BUILD.CANCEL-NEG-NEG ;; Reading from Proofs/level2/thm-build.cancel-neg-neg.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4231> VERIFY BUILD.CANCEL-NEG-NEG-UNDER-IFF ;; Reading from Proofs/level2/thm-build.cancel-neg-neg-under-iff.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.09 seconds 4232> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.CANCEL-NEG-NEG ;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.cancel-neg-neg.proof ;; Reading the file took 0.08 seconds ;; Checking the proof took 1.87 seconds ;; VERIFY took 2.71 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 10.61 seconds ;; VERIFY took 14.98 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.08 seconds ;; Checking the proof took 2.39 seconds ;; VERIFY took 3.50 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.02 seconds 4236> VERIFY BUILD.CANCEL-NEG-NEG-OKP ;; Reading from Proofs/level2/thm-build.cancel-neg-neg-okp.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.01 seconds ;; VERIFY took 0.03 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 2.39 seconds ;; VERIFY took 3.39 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.86 seconds ;; VERIFY took 1.10 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.21 seconds ;; Checking the proof took 24.19 seconds ;; VERIFY took 35.83 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.24 seconds ;; Checking the proof took 20.50 seconds ;; VERIFY took 30.24 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.59 seconds ;; Checking the proof took 15.21 seconds ;; VERIFY took 23.58 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.01 seconds 4243> VERIFY BUILD.INSERT-NEG-NEG ;; Reading from Proofs/level2/thm-build.insert-neg-neg.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4244> VERIFY BUILD.INSERT-NEG-NEG-UNDER-IFF ;; Reading from Proofs/level2/thm-build.insert-neg-neg-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.07 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 1.17 seconds ;; VERIFY took 1.73 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.12 seconds ;; Checking the proof took 4.14 seconds ;; VERIFY took 5.79 seconds 4247> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.INSERT-NEG-NEG ;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.insert-neg-neg.proof ;; Reading the file took 0.09 seconds ;; Checking the proof took 1.61 seconds ;; VERIFY took 2.42 seconds 4248> DEFINE BUILD.INSERT-NEG-NEG-OKP ;; Reading from Proofs/level2/admit-build.insert-neg-neg-okp.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4249> VERIFY BUILD.INSERT-NEG-NEG-OKP ;; Reading from Proofs/level2/thm-build.insert-neg-neg-okp.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.01 seconds ;; VERIFY took 0.03 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.11 seconds ;; Checking the proof took 2.15 seconds ;; VERIFY took 3.08 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.02 seconds ;; Checking the proof took 0.77 seconds ;; VERIFY took 0.98 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.65 seconds ;; Checking the proof took 39.60 seconds ;; VERIFY took 58.97 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.25 seconds ;; Checking the proof took 9.86 seconds ;; VERIFY took 14.69 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.37 seconds ;; Checking the proof took 4.67 seconds ;; VERIFY took 7.47 seconds 4255> DEFINE BUILD.LHS-INSERT-NEG-NEG ;; Reading from Proofs/level2/admit-build.lhs-insert-neg-neg.proofs ;; Reading the file took 0.02 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.02 seconds 4256> VERIFY BUILD.LHS-INSERT-NEG-NEG ;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.03 seconds 4257> VERIFY BUILD.LHS-INSERT-NEG-NEG-UNDER-IFF ;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.06 seconds ;; VERIFY took 0.09 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.10 seconds ;; Checking the proof took 2.59 seconds ;; VERIFY took 3.79 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.37 seconds ;; Checking the proof took 14.90 seconds ;; VERIFY took 21.01 seconds 4260> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.LHS-INSERT-NEG-NEG ;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.lhs-insert-neg-neg.proof ;; Reading the file took 0.12 seconds ;; Checking the proof took 5.09 seconds ;; VERIFY took 7.44 seconds 4261> DEFINE BUILD.LHS-INSERT-NEG-NEG-OKP ;; Reading from Proofs/level2/admit-build.lhs-insert-neg-neg-okp.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.02 seconds 4262> VERIFY BUILD.LHS-INSERT-NEG-NEG-OKP ;; Reading from Proofs/level2/thm-build.lhs-insert-neg-neg-okp.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.04 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.23 seconds ;; Checking the proof took 6.78 seconds ;; VERIFY took 10.00 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.08 seconds ;; Checking the proof took 1.58 seconds ;; VERIFY took 2.06 seconds 4265> VERIFY LEMMA-1-FOR-SOUNDNESS-OF-BUILD.LHS-INSERT-NEG-NEG-OKP ;; Reading from Proofs/level2/thm-lemma-1-for-soundness-of-build.lhs-insert-neg-neg-okp.proof ;; Reading the file took 1.16 seconds ;; Checking the proof took 138.83 seconds ;; VERIFY took 206.32 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.23 seconds ;; Checking the proof took 27.35 seconds ;; VERIFY took 40.40 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.60 seconds ;; Checking the proof took 11.58 seconds ;; VERIFY took 17.98 seconds 4268> DEFINE BUILD.MERGE-NEGATIVES ;; Reading from Proofs/level2/admit-build.merge-negatives.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4269> VERIFY BUILD.MERGE-NEGATIVES ;; Reading from Proofs/level2/thm-build.merge-negatives.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4270> VERIFY BUILD.MERGE-NEGATIVES-UNDER-IFF ;; Reading from Proofs/level2/thm-build.merge-negatives-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.09 seconds ;; VERIFY took 0.16 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.14 seconds ;; Checking the proof took 73.27 seconds ;; VERIFY took 107.44 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.64 seconds ;; Checking the proof took 181.91 seconds ;; VERIFY took 264.79 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.19 seconds ;; Checking the proof took 106.02 seconds ;; VERIFY took 157.08 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.04 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.02 seconds ;; VERIFY took 0.04 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.20 seconds ;; Checking the proof took 7.07 seconds ;; VERIFY took 10.31 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.06 seconds ;; Checking the proof took 1.62 seconds ;; VERIFY took 2.08 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.49 seconds ;; Checking the proof took 65.26 seconds ;; VERIFY took 95.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.35 seconds ;; Checking the proof took 31.34 seconds ;; VERIFY took 45.92 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.74 seconds ;; Checking the proof took 23.15 seconds ;; VERIFY took 35.18 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.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4283> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-1-UNDER-IFF ;; Reading from Proofs/level2/thm-build.merge-implications-lemma-1-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.09 seconds ;; VERIFY took 0.15 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 70.68 seconds ;; VERIFY took 102.53 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.99 seconds ;; Checking the proof took 219.32 seconds ;; VERIFY took 317.49 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.21 seconds ;; Checking the proof took 122.50 seconds ;; VERIFY took 179.78 seconds 4287> DEFINE BUILD.MERGE-IMPLICATIONS-LEMMA-2 ;; Reading from Proofs/level2/admit-build.merge-implications-lemma-2.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4288> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-2 ;; Reading from Proofs/level2/thm-build.merge-implications-lemma-2.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.03 seconds 4289> VERIFY BUILD.MERGE-IMPLICATIONS-LEMMA-2-UNDER-IFF ;; Reading from Proofs/level2/thm-build.merge-implications-lemma-2-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.05 seconds ;; VERIFY took 0.09 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.16 seconds ;; Checking the proof took 59.10 seconds ;; VERIFY took 86.03 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.54 seconds ;; Checking the proof took 274.23 seconds ;; VERIFY took 400.83 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.14 seconds ;; Checking the proof took 74.91 seconds ;; VERIFY took 109.96 seconds 4293> DEFINE BUILD.MERGE-IMPLICATIONS ;; Reading from Proofs/level2/admit-build.merge-implications.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4294> VERIFY BUILD.MERGE-IMPLICATIONS ;; Reading from Proofs/level2/thm-build.merge-implications.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.01 seconds 4295> VERIFY BUILD.MERGE-IMPLICATIONS-UNDER-IFF ;; Reading from Proofs/level2/thm-build.merge-implications-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.05 seconds ;; VERIFY took 0.08 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.10 seconds ;; Checking the proof took 6.10 seconds ;; VERIFY took 8.87 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.66 seconds ;; Checking the proof took 109.71 seconds ;; VERIFY took 159.20 seconds 4298> VERIFY FORCING-LOGIC.PROOFP-OF-BUILD.MERGE-IMPLICATIONS ;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-build.merge-implications.proof ;; Reading the file took 0.14 seconds ;; Checking the proof took 8.20 seconds ;; VERIFY took 12.08 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.05 seconds 4300> VERIFY BUILD.MERGE-IMPLICATIONS-OKP ;; Reading from Proofs/level2/thm-build.merge-implications-okp.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.07 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.57 seconds ;; Checking the proof took 29.52 seconds ;; VERIFY took 43.96 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 3.69 seconds ;; VERIFY took 4.68 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.68 seconds ;; Checking the proof took 251.41 seconds ;; VERIFY took 366.18 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.45 seconds ;; Checking the proof took 112.30 seconds ;; VERIFY took 163.30 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 1.44 seconds ;; Checking the proof took 71.76 seconds ;; VERIFY took 106.69 seconds 4306> DEFINE BUILD.DISJOINED-COMMUTE-OR-LEMMA-1 ;; Reading from Proofs/level2/admit-build.disjoined-commute-or-lemma-1.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4307> VERIFY BUILD.DISJOINED-COMMUTE-OR-LEMMA-1 ;; Reading from Proofs/level2/thm-build.disjoined-commute-or-lemma-1.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4308> VERIFY BUILD.DISJOINED-COMMUTE-OR-LEMMA-1-UNDER-IFF ;; Reading from Proofs/level2/thm-build.disjoined-commute-or-lemma-1-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.08 seconds ;; VERIFY took 0.14 seconds 4309> VERIFY FORCING-LOGIC.APPEALP-OF-BUILD.DISJOINED-COMMUTE-OR-LEMMA-1 ;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-build.disjoined-commute-or-lemma-1.proof ;; Reading the file took 0.21 seconds ;; Checking the proof took 52.56 seconds ;; VERIFY took 76.41 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.57 seconds ;; Checking the proof took 130.33 seconds ;; VERIFY took 187.99 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.14 seconds ;; Checking the proof took 83.34 seconds ;; VERIFY took 121.74 seconds 4312> DEFINE BUILD.DISJOINED-COMMUTE-OR ;; Reading from Proofs/level2/admit-build.disjoined-commute-or.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4313> VERIFY BUILD.DISJOINED-COMMUTE-OR ;; Reading from Proofs/level2/thm-build.disjoined-commute-or.proof ;; Reading the file took 0.06 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.07 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.07 seconds ;; VERIFY took 0.12 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.22 seconds ;; Checking the proof took 69.50 seconds ;; VERIFY took 99.60 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.37 seconds ;; Checking the proof took 277.79 seconds ;; VERIFY took 386.79 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.24 seconds ;; Checking the proof took 85.31 seconds ;; VERIFY took 123.55 seconds 4318> DEFINE BUILD.DISJOINED-COMMUTE-OR-OKP ;; Reading from Proofs/level2/admit-build.disjoined-commute-or-okp.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.03 seconds 4319> VERIFY BUILD.DISJOINED-COMMUTE-OR-OKP ;; Reading from Proofs/level2/thm-build.disjoined-commute-or-okp.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.05 seconds 4320> VERIFY BOOLEANP-OF-BUILD.DISJOINED-COMMUTE-OR-OKP ;; Reading from Proofs/level2/thm-booleanp-of-build.disjoined-commute-or-okp.proof ;; Reading the file took 0.23 seconds ;; Checking the proof took 9.82 seconds ;; VERIFY took 14.37 seconds 4321> VERIFY BUILD.DISJOINED-COMMUTE-OR-OKP-OF-LOGIC.APPEAL-IDENTITY ;; Reading from Proofs/level2/thm-build.disjoined-commute-or-okp-of-logic.appeal-identity.proof ;; Reading the file took 0.07 seconds ;; Checking the proof took 1.96 seconds ;; VERIFY took 2.52 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.35 seconds ;; Checking the proof took 79.84 seconds ;; VERIFY took 117.02 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.34 seconds ;; Checking the proof took 45.97 seconds ;; VERIFY took 67.16 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.63 seconds ;; Checking the proof took 19.99 seconds ;; VERIFY took 30.17 seconds 4325> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-1A ;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-1a.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; 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.02 seconds 4327> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-1A-UNDER-IFF ;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-1a-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.07 seconds ;; VERIFY took 0.13 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.19 seconds ;; Checking the proof took 37.93 seconds ;; VERIFY took 54.94 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.69 seconds ;; Checking the proof took 211.67 seconds ;; VERIFY took 303.70 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.22 seconds ;; Checking the proof took 67.78 seconds ;; VERIFY took 99.10 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.02 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.03 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.04 seconds ;; Checking the proof took 0.05 seconds ;; VERIFY took 0.11 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.12 seconds ;; Checking the proof took 13.85 seconds ;; VERIFY took 19.72 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.52 seconds ;; Checking the proof took 62.32 seconds ;; VERIFY took 88.41 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.18 seconds ;; Checking the proof took 27.38 seconds ;; VERIFY took 39.87 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.01 seconds 4338> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2A ;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2a.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4339> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2A-UNDER-IFF ;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2a-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.07 seconds ;; VERIFY took 0.14 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.17 seconds ;; Checking the proof took 48.08 seconds ;; VERIFY took 70.09 seconds 4341> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-ASSOC-LEMMA-2A ;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-assoc-lemma-2a.proof ;; Reading the file took 0.69 seconds ;; Checking the proof took 144.19 seconds ;; VERIFY took 209.09 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 85.22 seconds ;; VERIFY took 125.05 seconds 4343> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-2 ;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-2.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4344> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2 ;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4345> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-2-UNDER-IFF ;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-2-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.05 seconds ;; VERIFY took 0.09 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.10 seconds ;; Checking the proof took 13.71 seconds ;; VERIFY took 19.59 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.51 seconds ;; Checking the proof took 64.27 seconds ;; VERIFY took 90.51 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.16 seconds ;; Checking the proof took 27.03 seconds ;; VERIFY took 39.51 seconds 4349> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-3A ;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-3a.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4350> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-3A ;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-3a.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.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.01 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.06 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.19 seconds ;; Checking the proof took 10.56 seconds ;; VERIFY took 14.87 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.34 seconds ;; Checking the proof took 19.99 seconds ;; VERIFY took 28.14 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.40 seconds ;; Checking the proof took 26.21 seconds ;; VERIFY took 37.92 seconds 4355> DEFINE BUILD.DISJOINED-ASSOC-LEMMA-3 ;; Reading from Proofs/level2/admit-build.disjoined-assoc-lemma-3.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.02 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.01 seconds ;; VERIFY took 0.02 seconds 4357> VERIFY BUILD.DISJOINED-ASSOC-LEMMA-3-UNDER-IFF ;; Reading from Proofs/level2/thm-build.disjoined-assoc-lemma-3-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.08 seconds ;; VERIFY took 0.12 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 10.35 seconds ;; VERIFY took 14.54 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.63 seconds ;; Checking the proof took 101.76 seconds ;; VERIFY took 143.63 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.11 seconds ;; Checking the proof took 13.71 seconds ;; VERIFY took 19.46 seconds 4361> DEFINE BUILD.DISJOINED-RIGHT-ASSOCIATIVITY ;; Reading from Proofs/level2/admit-build.disjoined-right-associativity.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.00 seconds 4362> VERIFY BUILD.DISJOINED-RIGHT-ASSOCIATIVITY ;; Reading from Proofs/level2/thm-build.disjoined-right-associativity.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.05 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.02 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.08 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 20.40 seconds ;; VERIFY took 28.99 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.51 seconds ;; Checking the proof took 263.96 seconds ;; VERIFY took 370.08 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.17 seconds ;; Checking the proof took 26.73 seconds ;; VERIFY took 38.37 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.06 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.03 seconds ;; VERIFY took 0.06 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.45 seconds ;; Checking the proof took 23.26 seconds ;; VERIFY took 34.46 seconds 4370> VERIFY BUILD.DISJOINED-RIGHT-ASSOCIATIVITY-OKP-OF-LOGIC.APPEAL-IDENTITY ;; Reading from Proofs/level2/thm-build.disjoined-right-associativity-okp-of-logic.appeal-identity.proof ;; Reading the file took 0.05 seconds ;; Checking the proof took 3.22 seconds ;; VERIFY took 4.10 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.49 seconds ;; Checking the proof took 170.09 seconds ;; VERIFY took 247.64 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.37 seconds ;; Checking the proof took 92.66 seconds ;; VERIFY took 134.81 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.73 seconds ;; Checking the proof took 34.23 seconds ;; VERIFY took 50.70 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.02 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.03 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.07 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.23 seconds ;; Checking the proof took 6.47 seconds ;; VERIFY took 9.35 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.49 seconds ;; Checking the proof took 111.80 seconds ;; VERIFY took 157.10 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 8.48 seconds ;; VERIFY took 12.13 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.02 seconds 4382> VERIFY BUILD.DISJOINED-ASSOCIATIVITY-UNDER-IFF ;; Reading from Proofs/level2/thm-build.disjoined-associativity-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.07 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.08 seconds ;; Checking the proof took 18.14 seconds ;; VERIFY took 25.90 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.63 seconds ;; Checking the proof took 154.29 seconds ;; VERIFY took 217.76 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.12 seconds ;; Checking the proof took 23.69 seconds ;; VERIFY took 34.06 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.09 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.03 seconds ;; VERIFY took 0.06 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.45 seconds ;; Checking the proof took 23.51 seconds ;; VERIFY took 34.70 seconds 4389> VERIFY BUILD.DISJOINED-ASSOCIATIVITY-OKP-OF-LOGIC.APPEAL-IDENTITY ;; Reading from Proofs/level2/thm-build.disjoined-associativity-okp-of-logic.appeal-identity.proof ;; Reading the file took 0.06 seconds ;; Checking the proof took 3.26 seconds ;; VERIFY took 4.14 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.48 seconds ;; Checking the proof took 171.71 seconds ;; VERIFY took 249.26 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.32 seconds ;; Checking the proof took 93.63 seconds ;; VERIFY took 135.78 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.71 seconds ;; Checking the proof took 34.57 seconds ;; VERIFY took 51.04 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.02 seconds ;; Checking the proof took 0.05 seconds ;; VERIFY took 0.10 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.12 seconds ;; Checking the proof took 17.19 seconds ;; VERIFY took 24.75 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.69 seconds ;; Checking the proof took 129.35 seconds ;; VERIFY took 187.67 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.43 seconds ;; Checking the proof took 270.55 seconds ;; VERIFY took 391.68 seconds 4399> DEFINE BUILD.DISJOINED-CUT-LEMMA-2 ;; Reading from Proofs/level2/admit-build.disjoined-cut-lemma-2.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.00 seconds 4400> VERIFY BUILD.DISJOINED-CUT-LEMMA-2 ;; Reading from Proofs/level2/thm-build.disjoined-cut-lemma-2.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.03 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.03 seconds ;; VERIFY took 0.06 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.12 seconds ;; Checking the proof took 6.02 seconds ;; VERIFY took 8.70 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.78 seconds ;; Checking the proof took 268.52 seconds ;; VERIFY took 386.09 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.13 seconds ;; Checking the proof took 7.87 seconds ;; VERIFY took 11.46 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.03 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.04 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.04 seconds ;; VERIFY took 0.06 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.27 seconds ;; Checking the proof took 20.99 seconds ;; VERIFY took 30.27 seconds 4409> VERIFY FORCING-LOGIC.CONCLUSION-OF-BUILD.DISJOINED-CUT ;; Reading from Proofs/level2/thm-forcing-logic.conclusion-of-build.disjoined-cut.proof ;; Reading the file took 1.07 seconds ;; Checking the proof took 312.25 seconds ;; VERIFY took 449.33 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.31 seconds ;; Checking the proof took 31.36 seconds ;; VERIFY took 45.46 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.07 seconds 4412> VERIFY BUILD.DISJOINED-CUT-OKP ;; Reading from Proofs/level2/thm-build.disjoined-cut-okp.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.10 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.63 seconds ;; Checking the proof took 40.79 seconds ;; VERIFY took 59.67 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.03 seconds ;; Checking the proof took 4.62 seconds ;; VERIFY took 5.77 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.65 seconds ;; Checking the proof took 385.54 seconds ;; VERIFY took 551.68 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.46 seconds ;; Checking the proof took 167.57 seconds ;; VERIFY took 239.22 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.50 seconds ;; Checking the proof took 111.33 seconds ;; VERIFY took 161.49 seconds 4418> DEFINE BUILD.DISJOINED-MODUS-PONENS ;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4419> VERIFY BUILD.DISJOINED-MODUS-PONENS ;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4420> VERIFY BUILD.DISJOINED-MODUS-PONENS-UNDER-IFF ;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.13 seconds ;; VERIFY took 0.23 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.31 seconds ;; Checking the proof took 169.00 seconds ;; VERIFY took 241.24 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.70 seconds ;; Checking the proof took 398.04 seconds ;; VERIFY took 571.87 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.48 seconds ;; Checking the proof took 348.98 seconds ;; VERIFY took 502.05 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.07 seconds 4425> VERIFY BUILD.DISJOINED-MODUS-PONENS-OKP ;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-okp.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.08 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.36 seconds ;; Checking the proof took 20.82 seconds ;; VERIFY took 29.91 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.06 seconds ;; Checking the proof took 3.27 seconds ;; VERIFY took 4.10 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.57 seconds ;; Checking the proof took 232.34 seconds ;; VERIFY took 330.88 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.34 seconds ;; Checking the proof took 101.32 seconds ;; VERIFY took 143.70 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 1.39 seconds ;; Checking the proof took 83.57 seconds ;; VERIFY took 121.62 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.03 seconds 4432> VERIFY BUILD.DISJOINED-MODUS-PONENS-2 ;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4433> VERIFY BUILD.DISJOINED-MODUS-PONENS-2-UNDER-IFF ;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.14 seconds ;; VERIFY took 0.23 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.36 seconds ;; Checking the proof took 153.10 seconds ;; VERIFY took 218.22 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.62 seconds ;; Checking the proof took 380.25 seconds ;; VERIFY took 545.13 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.42 seconds ;; Checking the proof took 315.15 seconds ;; VERIFY took 452.55 seconds 4437> DEFINE BUILD.DISJOINED-MODUS-PONENS-2-OKP ;; Reading from Proofs/level2/admit-build.disjoined-modus-ponens-2-okp.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.04 seconds 4438> VERIFY BUILD.DISJOINED-MODUS-PONENS-2-OKP ;; Reading from Proofs/level2/thm-build.disjoined-modus-ponens-2-okp.proof ;; Reading the file took 0.05 seconds ;; Checking the proof took 0.03 seconds ;; VERIFY took 0.10 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.34 seconds ;; Checking the proof took 20.42 seconds ;; VERIFY took 29.30 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.06 seconds ;; Checking the proof took 3.20 seconds ;; VERIFY took 4.02 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.60 seconds ;; Checking the proof took 230.17 seconds ;; VERIFY took 327.57 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.33 seconds ;; Checking the proof took 115.68 seconds ;; VERIFY took 164.04 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 1.38 seconds ;; Checking the proof took 83.91 seconds ;; VERIFY took 121.87 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.05 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.05 seconds 4445> VERIFY BUILD.LHS-COMMUTE-OR-THEN-RASSOC ;; Reading from Proofs/level2/thm-build.lhs-commute-or-then-rassoc.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.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.01 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.07 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 6.01 seconds ;; VERIFY took 8.45 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.26 seconds ;; Checking the proof took 54.95 seconds ;; VERIFY took 75.55 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.11 seconds ;; Checking the proof took 8.33 seconds ;; VERIFY took 11.85 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.03 seconds 4451> VERIFY BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP ;; Reading from Proofs/level2/thm-build.lhs-commute-or-then-rassoc-okp.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.04 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.24 seconds ;; Checking the proof took 10.44 seconds ;; VERIFY took 15.00 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.07 seconds ;; Checking the proof took 2.06 seconds ;; VERIFY took 2.62 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.34 seconds ;; Checking the proof took 84.36 seconds ;; VERIFY took 121.12 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.28 seconds ;; Checking the proof took 48.42 seconds ;; VERIFY took 69.42 seconds 4456> VERIFY FORCING-SOUNDNESS-OF-BUILD.LHS-COMMUTE-OR-THEN-RASSOC-OKP ;; Reading from Proofs/level2/thm-forcing-soundness-of-build.lhs-commute-or-then-rassoc-okp.proof ;; Reading the file took 0.64 seconds ;; Checking the proof took 20.96 seconds ;; VERIFY took 31.02 seconds 4457> DEFINE RW.CREWRITE-TWIDDLE-BLDR ;; Reading from Proofs/level2/admit-rw.crewrite-twiddle-bldr.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; 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.02 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.08 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.09 seconds ;; Checking the proof took 6.05 seconds ;; VERIFY took 8.52 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.35 seconds ;; Checking the proof took 55.26 seconds ;; VERIFY took 75.95 seconds 4462> VERIFY FORCING-LOGIC.PROOFP-OF-RW.CREWRITE-TWIDDLE-BLDR ;; Reading from Proofs/level2/thm-forcing-logic.proofp-of-rw.crewrite-twiddle-bldr.proof ;; Reading the file took 0.10 seconds ;; Checking the proof took 8.38 seconds ;; VERIFY took 11.90 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.04 seconds 4464> VERIFY RW.CREWRITE-TWIDDLE-BLDR-OKP ;; Reading from Proofs/level2/thm-rw.crewrite-twiddle-bldr-okp.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.07 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.25 seconds ;; Checking the proof took 10.51 seconds ;; VERIFY took 15.08 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.07 seconds ;; Checking the proof took 2.07 seconds ;; VERIFY took 2.64 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.34 seconds ;; Checking the proof took 84.94 seconds ;; VERIFY took 121.71 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.27 seconds ;; Checking the proof took 48.72 seconds ;; VERIFY took 69.73 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.64 seconds ;; Checking the proof took 21.09 seconds ;; VERIFY took 31.15 seconds 4470> DEFINE RW.CREWRITE-TWIDDLE2-LEMMA ;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-lemma.proofs ;; Reading the file took 0.01 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.01 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.06 seconds ;; VERIFY took 0.10 seconds 4473> VERIFY FORCING-LOGIC.APPEALP-OF-RW.CREWRITE-TWIDDLE2-LEMMA ;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-rw.crewrite-twiddle2-lemma.proof ;; Reading the file took 0.15 seconds ;; Checking the proof took 50.69 seconds ;; VERIFY took 70.99 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.78 seconds ;; Checking the proof took 432.15 seconds ;; VERIFY took 598.18 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.20 seconds ;; Checking the proof took 80.58 seconds ;; VERIFY took 113.66 seconds 4476> DEFINE RW.CREWRITE-TWIDDLE2-BLDR ;; Reading from Proofs/level2/admit-rw.crewrite-twiddle2-bldr.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4477> VERIFY RW.CREWRITE-TWIDDLE2-BLDR ;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-bldr.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4478> VERIFY RW.CREWRITE-TWIDDLE2-BLDR-UNDER-IFF ;; Reading from Proofs/level2/thm-rw.crewrite-twiddle2-bldr-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.07 seconds 4479> VERIFY FORCING-LOGIC.APPEALP-OF-RW.CREWRITE-TWIDDLE2-BLDR ;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-rw.crewrite-twiddle2-bldr.proof ;; Reading the file took 0.10 seconds ;; Checking the proof took 31.70 seconds ;; VERIFY took 44.11 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.71 seconds ;; Checking the proof took 469.28 seconds ;; VERIFY took 648.54 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 43.44 seconds ;; VERIFY took 60.86 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.05 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.03 seconds ;; VERIFY took 0.06 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.46 seconds ;; Checking the proof took 24.37 seconds ;; VERIFY took 35.43 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 3.34 seconds ;; VERIFY took 4.18 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.46 seconds ;; Checking the proof took 176.35 seconds ;; VERIFY took 252.15 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.32 seconds ;; Checking the proof took 96.86 seconds ;; VERIFY took 138.33 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.72 seconds ;; Checking the proof took 35.93 seconds ;; VERIFY took 52.26 seconds 4489> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1 ;; Reading from Proofs/level2/admit-clause.aux-split-twiddle-lemma-1.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4490> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1 ;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-lemma-1.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4491> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-LEMMA-1-UNDER-IFF ;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-lemma-1-under-iff.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 0.14 seconds ;; VERIFY took 0.23 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.15 seconds ;; Checking the proof took 134.35 seconds ;; VERIFY took 189.29 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.72 seconds ;; Checking the proof took 305.12 seconds ;; VERIFY took 432.25 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.46 seconds ;; Checking the proof took 763.26 seconds ;; VERIFY took 1063.97 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.01 seconds ;; VERIFY took 0.02 seconds 4497> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-UNDER-IFF ;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-under-iff.proof ;; Reading the file took 0.03 seconds ;; Checking the proof took 0.05 seconds ;; VERIFY took 0.10 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.31 seconds ;; Checking the proof took 48.62 seconds ;; VERIFY took 67.44 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.54 seconds ;; Checking the proof took 73.87 seconds ;; VERIFY took 104.19 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.46 seconds ;; Checking the proof took 419.05 seconds ;; VERIFY took 582.86 seconds 4501> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE-OKP ;; Reading from Proofs/level2/admit-clause.aux-split-twiddle-okp.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.07 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.03 seconds ;; VERIFY took 0.06 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.33 seconds ;; Checking the proof took 20.24 seconds ;; VERIFY took 29.58 seconds 4504> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE-OKP-OF-LOGIC.APPEAL-IDENTITY ;; Reading from Proofs/level2/thm-clause.aux-split-twiddle-okp-of-logic.appeal-identity.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 3.10 seconds ;; VERIFY took 3.87 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.39 seconds ;; Checking the proof took 180.66 seconds ;; VERIFY took 256.77 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.57 seconds ;; Checking the proof took 124.69 seconds ;; VERIFY took 176.76 seconds 4507> VERIFY FORCING-SOUNDNESS-OF-CLAUSE.AUX-SPLIT-TWIDDLE-OKP ;; Reading from Proofs/level2/thm-forcing-soundness-of-clause.aux-split-twiddle-okp.proof ;; Reading the file took 1.02 seconds ;; Checking the proof took 56.12 seconds ;; VERIFY took 81.52 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.03 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.05 seconds ;; VERIFY took 0.10 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.08 seconds ;; Checking the proof took 12.91 seconds ;; VERIFY took 18.28 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.82 seconds ;; Checking the proof took 123.77 seconds ;; VERIFY took 171.70 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.17 seconds ;; Checking the proof took 23.59 seconds ;; VERIFY took 33.71 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.02 seconds 4516> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-1-UNDER-IFF ;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-1-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.05 seconds ;; VERIFY took 0.10 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.16 seconds ;; Checking the proof took 40.56 seconds ;; VERIFY took 56.61 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.75 seconds ;; Checking the proof took 421.99 seconds ;; VERIFY took 588.11 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.51 seconds ;; Checking the proof took 504.35 seconds ;; VERIFY took 711.12 seconds 4520> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A ;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-lemma-2a.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4521> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A ;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2a.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4522> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2A-UNDER-IFF ;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2a-under-iff.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.08 seconds ;; VERIFY took 0.15 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.17 seconds ;; Checking the proof took 54.52 seconds ;; VERIFY took 76.61 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.66 seconds ;; Checking the proof took 159.22 seconds ;; VERIFY took 224.04 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.17 seconds ;; Checking the proof took 93.55 seconds ;; VERIFY took 133.32 seconds 4526> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2 ;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-lemma-2.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4527> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2-LEMMA-2 ;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2-lemma-2.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.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.05 seconds ;; VERIFY took 0.09 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.13 seconds ;; Checking the proof took 39.58 seconds ;; VERIFY took 54.97 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.64 seconds ;; Checking the proof took 479.81 seconds ;; VERIFY took 660.40 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.12 seconds ;; Checking the proof took 60.65 seconds ;; VERIFY took 85.24 seconds 4532> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2 ;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4533> VERIFY CLAUSE.AUX-SPLIT-TWIDDLE2 ;; Reading from Proofs/level2/thm-clause.aux-split-twiddle2.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.01 seconds ;; VERIFY took 0.02 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.13 seconds ;; VERIFY took 0.19 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.36 seconds ;; Checking the proof took 77.67 seconds ;; VERIFY took 106.78 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.65 seconds ;; Checking the proof took 107.29 seconds ;; VERIFY took 148.10 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.68 seconds ;; Checking the proof took 431.65 seconds ;; VERIFY took 601.20 seconds 4538> DEFINE CLAUSE.AUX-SPLIT-TWIDDLE2-OKP ;; Reading from Proofs/level2/admit-clause.aux-split-twiddle2-okp.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.05 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.03 seconds ;; VERIFY took 0.05 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.46 seconds ;; Checking the proof took 25.11 seconds ;; VERIFY took 36.20 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 3.46 seconds ;; VERIFY took 4.30 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.45 seconds ;; Checking the proof took 182.96 seconds ;; VERIFY took 259.07 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.32 seconds ;; Checking the proof took 99.92 seconds ;; VERIFY took 141.45 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.73 seconds ;; Checking the proof took 37.13 seconds ;; VERIFY took 53.48 seconds 4545> DEFINE CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR ;; Reading from Proofs/level2/admit-clause.aux-split-default-3-bldr.proofs ;; Reading the file took 0.01 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.01 seconds 4546> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR ;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.01 seconds 4547> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-UNDER-IFF ;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.07 seconds 4548> VERIFY FORCING-LOGIC.APPEALP-OF-CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR ;; Reading from Proofs/level2/thm-forcing-logic.appealp-of-clause.aux-split-default-3-bldr.proof ;; Reading the file took 0.09 seconds ;; Checking the proof took 9.13 seconds ;; VERIFY took 12.61 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.47 seconds ;; Checking the proof took 88.49 seconds ;; VERIFY took 121.65 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.35 seconds ;; Checking the proof took 75.49 seconds ;; VERIFY took 103.78 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.03 seconds 4552> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP ;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr-okp.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.08 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.22 seconds ;; Checking the proof took 11.09 seconds ;; VERIFY took 15.68 seconds 4554> VERIFY CLAUSE.AUX-SPLIT-DEFAULT-3-BLDR-OKP-OF-LOGIC.APPEAL-IDENTITY ;; Reading from Proofs/level2/thm-clause.aux-split-default-3-bldr-okp-of-logic.appeal-identity.proof ;; Reading the file took 0.06 seconds ;; Checking the proof took 2.19 seconds ;; VERIFY took 2.74 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.31 seconds ;; Checking the proof took 89.72 seconds ;; VERIFY took 126.74 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.27 seconds ;; Checking the proof took 51.50 seconds ;; VERIFY took 72.68 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.64 seconds ;; Checking the proof took 22.36 seconds ;; VERIFY took 32.52 seconds 4558> DEFINE CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR ;; Reading from Proofs/level2/admit-clause.aux-limsplit-cutoff-step-bldr.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.00 seconds 4559> VERIFY CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR ;; Reading from Proofs/level2/thm-clause.aux-limsplit-cutoff-step-bldr.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 seconds 4560> VERIFY CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-UNDER-IFF ;; Reading from Proofs/level2/thm-clause.aux-limsplit-cutoff-step-bldr-under-iff.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.05 seconds ;; VERIFY took 0.08 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.09 seconds ;; Checking the proof took 6.51 seconds ;; VERIFY took 9.02 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.34 seconds ;; Checking the proof took 58.65 seconds ;; VERIFY took 79.49 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.10 seconds ;; Checking the proof took 9.00 seconds ;; VERIFY took 12.53 seconds 4564> DEFINE CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-OKP ;; Reading from Proofs/level2/admit-clause.aux-limsplit-cutoff-step-bldr-okp.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.03 seconds 4565> VERIFY CLAUSE.AUX-LIMSPLIT-CUTOFF-STEP-BLDR-OKP ;; Reading from Proofs/level2/thm-clause.aux-limsplit-cutoff-step-bldr-okp.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.02 seconds ;; VERIFY took 0.05 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.24 seconds ;; Checking the proof took 11.14 seconds ;; VERIFY took 15.73 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.07 seconds ;; Checking the proof took 2.20 seconds ;; VERIFY took 2.77 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.33 seconds ;; Checking the proof took 90.13 seconds ;; VERIFY took 127.14 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.29 seconds ;; Checking the proof took 51.73 seconds ;; VERIFY took 72.83 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.70 seconds ;; Checking the proof took 22.36 seconds ;; VERIFY took 32.54 seconds 4571> DEFINE LEVEL2.STEP-OKP ;; Reading from Proofs/level2/admit-level2.step-okp.proofs ;; Reading the file took 0.00 seconds ;; Checking the proofs took 0.00 seconds ;; DEFINE took 0.02 seconds 4572> VERIFY LEVEL2.STEP-OKP ;; Reading from Proofs/level2/thm-level2.step-okp.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.04 seconds ;; VERIFY took 0.07 seconds 4573> VERIFY SOUNDNESS-OF-LEVEL2.STEP-OKP ;; Reading from Proofs/level2/thm-soundness-of-level2.step-okp.proof ;; Reading the file took 0.34 seconds ;; Checking the proof took 16.39 seconds ;; VERIFY took 24.72 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 1.08 seconds ;; Checking the proof took 94.71 seconds ;; VERIFY took 141.11 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.35 seconds ;; Checking the proof took 18.28 seconds ;; VERIFY took 24.73 seconds 4576> DEFINE LEVEL2.FLAG-PROOFP ;; Reading from Proofs/level2/admit-level2.flag-proofp.proofs ;; Reading the file took 0.32 seconds ;; Checking the proofs took 6.24 seconds ;; DEFINE took 8.56 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.01 seconds ;; VERIFY took 0.03 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.02 seconds ;; Checking the proof took 0.00 seconds ;; VERIFY took 0.02 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.02 seconds 4582> VERIFY DEFINITION-OF-LEVEL2.PROOFP ;; Reading from Proofs/level2/thm-definition-of-level2.proofp.proof ;; Reading the file took 0.06 seconds ;; Checking the proof took 0.25 seconds ;; VERIFY took 0.41 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.94 seconds ;; VERIFY took 1.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.03 seconds ;; Checking the proof took 0.19 seconds ;; VERIFY took 0.27 seconds 4585> VERIFY LEVEL2.PROOF-LISTP-WHEN-NOT-CONSP ;; Reading from Proofs/level2/thm-level2.proof-listp-when-not-consp.proof ;; Reading the file took 0.02 seconds ;; Checking the proof took 0.20 seconds ;; VERIFY took 0.28 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.29 seconds ;; VERIFY took 0.41 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.62 seconds ;; Checking the proof took 15.10 seconds ;; VERIFY took 20.64 seconds 4588> VERIFY BOOLEANP-OF-LEVEL2.PROOFP ;; Reading from Proofs/level2/thm-booleanp-of-level2.proofp.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.53 seconds ;; VERIFY took 0.70 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.50 seconds ;; VERIFY took 0.67 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.32 seconds ;; Checking the proof took 5.44 seconds ;; VERIFY took 7.87 seconds 4591> VERIFY LEVEL2.PROOF-LISTP-OF-APP ;; Reading from Proofs/level2/thm-level2.proof-listp-of-app.proof ;; Reading the file took 0.63 seconds ;; Checking the proof took 11.30 seconds ;; VERIFY took 17.00 seconds 4592> VERIFY LEVEL2.PROOF-LISTP-OF-REV ;; Reading from Proofs/level2/thm-level2.proof-listp-of-rev.proof ;; Reading the file took 0.31 seconds ;; Checking the proof took 5.74 seconds ;; VERIFY took 8.34 seconds 4593> VERIFY LEVEL2.PROOFP-OF-CAR-WHEN-LEVEL2.PROOF-LISTP ;; Reading from Proofs/level2/thm-level2.proofp-of-car-when-level2.proof-listp.proof ;; Reading the file took 0.10 seconds ;; Checking the proof took 0.74 seconds ;; VERIFY took 1.10 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.04 seconds ;; Checking the proof took 0.44 seconds ;; VERIFY took 0.63 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.21 seconds ;; Checking the proof took 4.21 seconds ;; VERIFY took 5.92 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.06 seconds ;; Checking the proof took 0.47 seconds ;; VERIFY took 0.71 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.20 seconds ;; Checking the proof took 3.64 seconds ;; VERIFY took 5.03 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.38 seconds ;; Checking the proof took 6.16 seconds ;; VERIFY took 8.96 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.20 seconds ;; Checking the proof took 3.51 seconds ;; VERIFY took 4.89 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.28 seconds ;; Checking the proof took 4.69 seconds ;; VERIFY took 6.60 seconds 4601> VERIFY LEVEL2.PROOF-LISTP-OF-SUBSETP-WHEN-LEVEL2.PROOF-LISTP-ALT ;; Reading from Proofs/level2/thm-level2.proof-listp-of-subsetp-when-level2.proof-listp-alt.proof ;; Reading the file took 0.05 seconds ;; Checking the proof took 0.16 seconds ;; VERIFY took 0.27 seconds 4602> VERIFY LEVEL2.PROOF-LISTP-OF-REPEAT ;; Reading from Proofs/level2/thm-level2.proof-listp-of-repeat.proof ;; Reading the file took 0.19 seconds ;; Checking the proof took 3.99 seconds ;; VERIFY took 5.57 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 2.09 seconds ;; Checking the proof took 70.12 seconds ;; VERIFY took 100.06 seconds 4604> VERIFY LOGIC.PROVABLEP-WHEN-LEVEL2.PROOFP ;; Reading from Proofs/level2/thm-logic.provablep-when-level2.proofp.proof ;; Reading the file took 0.09 seconds ;; Checking the proof took 1.83 seconds ;; VERIFY took 2.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.08 seconds ;; Checking the proof took 1.84 seconds ;; VERIFY took 2.67 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.94 seconds ;; Checking the proof took 21.68 seconds ;; VERIFY took 30.62 seconds 4607> VERIFY LEVEL2.PROOFP-WHEN-LOGIC.PROOFP ;; Reading from Proofs/level2/thm-level2.proofp-when-logic.proofp.proof ;; Reading the file took 0.04 seconds ;; Checking the proof took 0.80 seconds ;; VERIFY took 1.11 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.04 seconds ;; Checking the proof took 0.79 seconds ;; VERIFY took 1.10 seconds 4609> VERIFY FORCING-LEVEL2.PROOFP-OF-LOGIC.PROVABLE-WITNESS ;; Reading from Proofs/level2/thm-forcing-level2.proofp-of-logic.provable-witness.proof ;; Reading the file took 0.01 seconds ;; Checking the proof took 0.12 seconds ;; VERIFY took 0.18 seconds 4610> VERIFY INSTALL-NEW-PROOFP-LEVEL2.PROOFP ;; Reading from Proofs/level2/thm-install-new-proofp-level2.proofp.proof ;; Reading the file took 0.05 seconds ;; Checking the proof took 0.16 seconds ;; VERIFY took 0.27 seconds 4611 > SWITCH LEVEL2.PROOFP ;; SWITCH took 0.00 seconds 4612 > FINISH level2 ;; Wrote the memory image into level2.nemesis-clisp (4,372,188 bytes) Bytes permanently allocated: 89,856 Bytes currently in use: 4,279,128 Bytes available until next GC: 1,067,672 Bye. real 456m29.015s user 454m2.543s sys 0m11.857s