%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : LCL456+1 : TPTP v9.3.1. Bugfixed v9.2.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n008.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 12:54:11 PM UTC 2026 % Result : Theorem 24.66s 3.96s % Output : Proof 50.87s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL456+1 : TPTP v9.3.1. Bugfixed v9.2.0. % 0.00/0.04 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.08/0.35 % Computer : n008.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Fri Sep 4 18:43:38 UTC 2026 % 0.08/0.35 % CPUTime : % 0.13/0.37 OpenJDK 64-Bit Server VM warning: Options -Xverify:none and -noverify were deprecated in JDK 13 and will likely be removed in a future release. % 0.69/0.70 ________ _____ % 0.69/0.70 ___ __ \_________(_)________________________________ % 0.69/0.70 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.69/0.70 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.69/0.70 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.69/0.70 % 0.69/0.70 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.69/0.70 (2023-06-19) % 0.69/0.70 % 0.69/0.70 (c) Philipp Rümmer, 2009-2023 % 0.69/0.70 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.69/0.70 Amanda Stjerna. % 0.69/0.70 Free software under BSD-3-Clause. % 0.69/0.70 % 0.69/0.70 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.69/0.70 % 0.69/0.70 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.69/0.72 Running up to 7 provers in parallel. % 0.69/0.74 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.69/0.74 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.69/0.74 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.69/0.74 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.69/0.74 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.69/0.74 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.69/0.74 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.21/1.30 Prover 4: Preprocessing ... % 4.21/1.31 Prover 1: Preprocessing ... % 4.21/1.36 Prover 0: Preprocessing ... % 4.21/1.36 Prover 3: Preprocessing ... % 4.21/1.36 Prover 2: Preprocessing ... % 4.21/1.36 Prover 6: Preprocessing ... % 4.21/1.37 Prover 5: Preprocessing ... % 11.24/2.25 Prover 6: Constructing countermodel ... % 11.24/2.26 Prover 1: Constructing countermodel ... % 12.03/2.35 Prover 5: Proving ... % 12.03/2.40 Prover 4: Constructing countermodel ... % 12.81/2.41 Prover 3: Constructing countermodel ... % 13.64/2.59 Prover 0: Proving ... % 14.41/2.64 Prover 2: Proving ... % 20.69/3.40 Prover 1: gave up % 20.69/3.40 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 20.69/3.48 Prover 7: Preprocessing ... % 23.10/3.72 Prover 7: Constructing countermodel ... % 24.66/3.96 Prover 0: proved (3224ms) % 24.66/3.96 % 24.66/3.96 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 24.66/3.96 % 24.66/3.97 Prover 5: stopped % 24.66/3.97 Prover 2: stopped % 24.66/3.97 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 24.66/3.97 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 24.66/3.97 Prover 6: stopped % 24.66/3.97 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 24.66/3.98 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 24.66/3.98 Prover 3: stopped % 24.66/3.98 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 24.66/4.08 Prover 8: Preprocessing ... % 24.66/4.08 Prover 10: Preprocessing ... % 26.10/4.14 Prover 11: Preprocessing ... % 26.10/4.17 Prover 13: Preprocessing ... % 26.10/4.17 Prover 16: Preprocessing ... % 27.78/4.37 Prover 8: Warning: ignoring some quantifiers % 28.61/4.42 Prover 13: Constructing countermodel ... % 28.61/4.42 Prover 8: Constructing countermodel ... % 28.61/4.46 Prover 16: Warning: ignoring some quantifiers % 28.61/4.48 Prover 16: Constructing countermodel ... % 29.37/4.51 Prover 11: Constructing countermodel ... % 29.37/4.52 Prover 10: Constructing countermodel ... % 30.96/4.75 Prover 8: gave up % 30.96/4.76 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 31.75/4.82 Prover 13: gave up % 32.53/4.94 Prover 19: Preprocessing ... % 32.53/4.94 Prover 10: gave up % 34.53/5.17 Prover 19: Constructing countermodel ... % 37.06/5.58 Prover 19: gave up % 44.90/6.68 Prover 16: gave up % 49.29/7.37 Prover 4: Found proof (size 125) % 49.29/7.37 Prover 4: proved (6636ms) % 49.29/7.37 Prover 7: stopped % 49.29/7.37 Prover 11: stopped % 49.29/7.37 % 49.29/7.38 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 49.29/7.38 % 49.92/7.41 % SZS output start Proof for theBenchmark % 49.92/7.41 Assumptions after simplification: % 49.92/7.41 --------------------------------- % 49.92/7.41 % 49.92/7.41 (hilbert_implies_3) % 49.92/7.42 implies_3 % 49.92/7.42 % 49.92/7.42 (hilbert_modus_ponens) % 49.92/7.42 modus_ponens % 49.92/7.42 % 49.92/7.42 (hilbert_op_implies_and) % 49.92/7.42 op_implies_and % 49.92/7.42 % 49.92/7.42 (hilbert_op_or) % 49.92/7.42 op_or % 49.92/7.42 % 49.92/7.42 (hilbert_or_1) % 49.92/7.42 or_1 % 49.92/7.42 % 49.92/7.42 (hilbert_or_2) % 49.92/7.42 or_2 % 49.92/7.42 % 49.92/7.42 (hilbert_or_3) % 49.92/7.42 or_3 % 49.92/7.42 % 49.92/7.42 (implies_3) % 49.92/7.48 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 49.92/7.48 $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: int] : ($i(v2) & $i(v1) & $i(v0) & % 49.92/7.48 (( ~ (v8 = 0) & implies(v4, v5) = v6 & implies(v3, v6) = v7 & implies(v1, % 49.92/7.48 v2) = v4 & implies(v0, v2) = v5 & implies(v0, v1) = v3 & % 49.92/7.48 is_a_theorem(v7) = v8 & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & ~ % 49.92/7.48 implies_3) | (implies_3 & ! [v9: $i] : ! [v10: $i] : ! [v11: $i] : ! % 49.92/7.48 [v12: $i] : ! [v13: $i] : ! [v14: $i] : ( ~ (implies(v12, v13) = v14) % 49.92/7.48 | ~ (implies(v10, v11) = v12) | ~ (implies(v9, v11) = v13) | ~ % 49.92/7.48 $i(v11) | ~ $i(v10) | ~ $i(v9) | ? [v15: $i] : ? [v16: $i] : % 49.92/7.48 (implies(v15, v14) = v16 & implies(v9, v10) = v15 & is_a_theorem(v16) % 49.92/7.48 = 0 & $i(v16) & $i(v15)))))) % 49.92/7.48 % 49.92/7.48 (modus_ponens) % 49.92/7.49 ? [v0: $i] : ? [v1: $i] : ? [v2: int] : ? [v3: $i] : ? [v4: int] : ? % 49.92/7.49 [v5: int] : ($i(v1) & $i(v0) & ((v4 = 0 & v2 = 0 & ~ (v5 = 0) & implies(v0, % 49.92/7.49 v1) = v3 & is_a_theorem(v3) = 0 & is_a_theorem(v1) = v5 & % 49.92/7.49 is_a_theorem(v0) = 0 & $i(v3) & ~ modus_ponens) | (modus_ponens & ! % 49.92/7.49 [v6: $i] : ! [v7: $i] : ! [v8: $i] : ( ~ (implies(v6, v7) = v8) | ~ % 49.92/7.49 $i(v7) | ~ $i(v6) | ? [v9: any] : ? [v10: any] : ? [v11: any] : % 49.92/7.49 (is_a_theorem(v8) = v10 & is_a_theorem(v7) = v11 & is_a_theorem(v6) = % 49.92/7.49 v9 & ( ~ (v10 = 0) | ~ (v9 = 0) | v11 = 0)))))) % 49.92/7.49 % 49.92/7.49 (op_implies_and) % 49.92/7.49 ~ op_implies_and | ( ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( % 49.92/7.49 ~ (and(v0, v2) = v3) | ~ (not(v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 49.92/7.49 $i] : (not(v3) = v4 & implies(v0, v1) = v4 & $i(v4))) & ! [v0: $i] : ! % 49.92/7.49 [v1: $i] : ! [v2: $i] : ( ~ (implies(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) % 49.92/7.49 | ? [v3: $i] : ? [v4: $i] : (and(v0, v3) = v4 & not(v4) = v2 & not(v1) = % 49.92/7.49 v3 & $i(v4) & $i(v3) & $i(v2)))) % 49.92/7.49 % 49.92/7.49 (op_or) % 49.92/7.49 ~ op_or | ( ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 49.92/7.49 $i] : ( ~ (and(v2, v3) = v4) | ~ (not(v1) = v3) | ~ (not(v0) = v2) | ~ % 49.92/7.49 $i(v1) | ~ $i(v0) | ? [v5: $i] : (or(v0, v1) = v5 & not(v4) = v5 & % 49.92/7.49 $i(v5))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (or(v0, v1) = % 49.92/7.50 v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 49.92/7.50 (and(v3, v4) = v5 & not(v5) = v2 & not(v1) = v4 & not(v0) = v3 & $i(v5) & % 49.92/7.50 $i(v4) & $i(v3) & $i(v2)))) % 49.92/7.50 % 49.92/7.50 (or_1) % 50.38/7.50 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: int] : ($i(v1) % 50.38/7.50 & $i(v0) & (( ~ (v4 = 0) & or(v0, v1) = v2 & implies(v0, v2) = v3 & % 50.38/7.50 is_a_theorem(v3) = v4 & $i(v3) & $i(v2) & ~ or_1) | (or_1 & ! [v5: $i] % 50.38/7.50 : ! [v6: $i] : ! [v7: $i] : ( ~ (or(v5, v6) = v7) | ~ $i(v6) | ~ % 50.38/7.50 $i(v5) | ? [v8: $i] : (implies(v5, v7) = v8 & is_a_theorem(v8) = 0 & % 50.38/7.50 $i(v8)))))) % 50.38/7.50 % 50.38/7.50 (or_2) % 50.38/7.50 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: int] : ($i(v1) % 50.38/7.50 & $i(v0) & (( ~ (v4 = 0) & or(v0, v1) = v2 & implies(v1, v2) = v3 & % 50.38/7.50 is_a_theorem(v3) = v4 & $i(v3) & $i(v2) & ~ or_2) | (or_2 & ! [v5: $i] % 50.38/7.50 : ! [v6: $i] : ! [v7: $i] : ( ~ (or(v5, v6) = v7) | ~ $i(v6) | ~ % 50.38/7.50 $i(v5) | ? [v8: $i] : (implies(v6, v7) = v8 & is_a_theorem(v8) = 0 & % 50.38/7.50 $i(v8)))))) % 50.38/7.50 % 50.38/7.50 (or_3) % 50.38/7.50 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 50.38/7.50 $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: int] : ($i(v2) & % 50.38/7.50 $i(v1) & $i(v0) & (( ~ (v9 = 0) & or(v0, v1) = v5 & implies(v5, v2) = v6 & % 50.38/7.50 implies(v4, v6) = v7 & implies(v3, v7) = v8 & implies(v1, v2) = v4 & % 50.38/7.50 implies(v0, v2) = v3 & is_a_theorem(v8) = v9 & $i(v8) & $i(v7) & $i(v6) % 50.38/7.50 & $i(v5) & $i(v4) & $i(v3) & ~ or_3) | (or_3 & ! [v10: $i] : ! [v11: % 50.38/7.50 $i] : ! [v12: $i] : ! [v13: $i] : ! [v14: $i] : ( ~ (or(v10, v11) = % 50.38/7.51 v13) | ~ (implies(v13, v12) = v14) | ~ $i(v12) | ~ $i(v11) | ~ % 50.38/7.51 $i(v10) | ? [v15: $i] : ? [v16: $i] : ? [v17: $i] : ? [v18: $i] : % 50.38/7.51 (implies(v16, v14) = v17 & implies(v15, v17) = v18 & implies(v11, v12) % 50.38/7.51 = v16 & implies(v10, v12) = v15 & is_a_theorem(v18) = 0 & $i(v18) & % 50.38/7.51 $i(v17) & $i(v16) & $i(v15)))))) % 50.38/7.51 % 50.38/7.51 (principia_r3) % 50.38/7.51 ~ r3 % 50.38/7.51 % 50.38/7.51 (r3) % 50.38/7.51 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 50.38/7.51 int] : ($i(v1) & $i(v0) & (( ~ (v5 = 0) & or(v1, v0) = v3 & or(v0, v1) = v2 % 50.38/7.51 & implies(v2, v3) = v4 & is_a_theorem(v4) = v5 & $i(v4) & $i(v3) & % 50.38/7.51 $i(v2) & ~ r3) | (r3 & ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ( ~ % 50.38/7.51 (or(v7, v6) = v8) | ~ $i(v7) | ~ $i(v6) | ? [v9: $i] : ? [v10: $i] % 50.38/7.51 : (or(v6, v7) = v9 & implies(v9, v8) = v10 & is_a_theorem(v10) = 0 & % 50.38/7.51 $i(v10) & $i(v9))) & ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ( ~ % 50.38/7.51 (or(v6, v7) = v8) | ~ $i(v7) | ~ $i(v6) | ? [v9: $i] : ? [v10: $i] % 50.38/7.51 : (or(v7, v6) = v9 & implies(v8, v9) = v10 & is_a_theorem(v10) = 0 & % 50.38/7.51 $i(v10) & $i(v9)))))) % 50.38/7.51 % 50.38/7.51 (function-axioms) % 50.38/7.51 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (or(v3, % 50.38/7.51 v2) = v1) | ~ (or(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 50.38/7.51 $i] : ! [v3: $i] : (v1 = v0 | ~ (and(v3, v2) = v1) | ~ (and(v3, v2) = % 50.38/7.51 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 50.38/7.51 ~ (equiv(v3, v2) = v1) | ~ (equiv(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 50.38/7.51 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (implies(v3, v2) = v1) | ~ % 50.38/7.51 (implies(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 % 50.38/7.51 | ~ (not(v2) = v1) | ~ (not(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 50.38/7.51 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (is_a_theorem(v2) = v1) % 50.38/7.51 | ~ (is_a_theorem(v2) = v0)) % 50.38/7.51 % 50.38/7.51 Further assumptions not needed in the proof: % 50.38/7.51 -------------------------------------------- % 50.38/7.51 and_1, and_2, and_3, cn1, cn2, cn3, equivalence_1, equivalence_2, equivalence_3, % 50.38/7.51 hilbert_and_1, hilbert_and_2, hilbert_and_3, hilbert_equivalence_1, % 50.38/7.51 hilbert_equivalence_2, hilbert_equivalence_3, hilbert_implies_1, % 50.38/7.51 hilbert_implies_2, hilbert_modus_tollens, hilbert_op_equiv, implies_1, % 50.38/7.51 implies_2, kn1, kn2, kn3, modus_tollens, op_and, op_equiv, op_implies_or, % 50.38/7.51 principia_op_and, principia_op_equiv, principia_op_implies_or, r1, r2, r4, r5, % 50.38/7.51 substitution_of_equivalents, use_substitution_of_equivalents % 50.38/7.51 % 50.38/7.51 Those formulas are unsatisfiable: % 50.38/7.51 --------------------------------- % 50.38/7.51 % 50.38/7.51 Begin of proof % 50.38/7.52 | % 50.38/7.52 | ALPHA: (function-axioms) implies: % 50.38/7.52 | (1) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 50.38/7.52 | (v1 = v0 | ~ (is_a_theorem(v2) = v1) | ~ (is_a_theorem(v2) = v0)) % 50.38/7.52 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 50.38/7.52 | (implies(v3, v2) = v1) | ~ (implies(v3, v2) = v0)) % 50.38/7.52 | % 50.38/7.52 | DELTA: instantiating (or_1) with fresh symbols all_20_0, all_20_1, all_20_2, % 50.38/7.52 | all_20_3, all_20_4 gives: % 50.38/7.52 | (3) $i(all_20_3) & $i(all_20_4) & (( ~ (all_20_0 = 0) & or(all_20_4, % 50.38/7.52 | all_20_3) = all_20_2 & implies(all_20_4, all_20_2) = all_20_1 & % 50.38/7.52 | is_a_theorem(all_20_1) = all_20_0 & $i(all_20_1) & $i(all_20_2) & % 50.38/7.52 | ~ or_1) | (or_1 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 50.38/7.52 | (or(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : % 50.38/7.52 | (implies(v0, v2) = v3 & is_a_theorem(v3) = 0 & $i(v3))))) % 50.38/7.52 | % 50.38/7.52 | ALPHA: (3) implies: % 50.38/7.53 | (4) ( ~ (all_20_0 = 0) & or(all_20_4, all_20_3) = all_20_2 & % 50.38/7.53 | implies(all_20_4, all_20_2) = all_20_1 & is_a_theorem(all_20_1) = % 50.38/7.53 | all_20_0 & $i(all_20_1) & $i(all_20_2) & ~ or_1) | (or_1 & ! [v0: % 50.38/7.53 | $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (or(v0, v1) = v2) | ~ $i(v1) % 50.38/7.53 | | ~ $i(v0) | ? [v3: $i] : (implies(v0, v2) = v3 & % 50.38/7.53 | is_a_theorem(v3) = 0 & $i(v3)))) % 50.38/7.53 | % 50.38/7.53 | DELTA: instantiating (or_2) with fresh symbols all_22_0, all_22_1, all_22_2, % 50.38/7.53 | all_22_3, all_22_4 gives: % 50.38/7.53 | (5) $i(all_22_3) & $i(all_22_4) & (( ~ (all_22_0 = 0) & or(all_22_4, % 50.38/7.53 | all_22_3) = all_22_2 & implies(all_22_3, all_22_2) = all_22_1 & % 50.38/7.53 | is_a_theorem(all_22_1) = all_22_0 & $i(all_22_1) & $i(all_22_2) & % 50.38/7.53 | ~ or_2) | (or_2 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 50.38/7.53 | (or(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : % 50.38/7.53 | (implies(v1, v2) = v3 & is_a_theorem(v3) = 0 & $i(v3))))) % 50.38/7.53 | % 50.38/7.53 | ALPHA: (5) implies: % 50.38/7.53 | (6) ( ~ (all_22_0 = 0) & or(all_22_4, all_22_3) = all_22_2 & % 50.38/7.53 | implies(all_22_3, all_22_2) = all_22_1 & is_a_theorem(all_22_1) = % 50.38/7.53 | all_22_0 & $i(all_22_1) & $i(all_22_2) & ~ or_2) | (or_2 & ! [v0: % 50.38/7.53 | $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (or(v0, v1) = v2) | ~ $i(v1) % 50.38/7.53 | | ~ $i(v0) | ? [v3: $i] : (implies(v1, v2) = v3 & % 50.38/7.53 | is_a_theorem(v3) = 0 & $i(v3)))) % 50.38/7.53 | % 50.38/7.53 | DELTA: instantiating (modus_ponens) with fresh symbols all_32_0, all_32_1, % 50.38/7.53 | all_32_2, all_32_3, all_32_4, all_32_5 gives: % 50.38/7.53 | (7) $i(all_32_4) & $i(all_32_5) & ((all_32_1 = 0 & all_32_3 = 0 & ~ % 50.38/7.53 | (all_32_0 = 0) & implies(all_32_5, all_32_4) = all_32_2 & % 50.38/7.53 | is_a_theorem(all_32_2) = 0 & is_a_theorem(all_32_4) = all_32_0 & % 50.38/7.53 | is_a_theorem(all_32_5) = 0 & $i(all_32_2) & ~ modus_ponens) | % 50.38/7.53 | (modus_ponens & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 50.38/7.53 | (implies(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : % 50.38/7.53 | ? [v4: any] : ? [v5: any] : (is_a_theorem(v2) = v4 & % 50.38/7.53 | is_a_theorem(v1) = v5 & is_a_theorem(v0) = v3 & ( ~ (v4 = 0) | % 50.38/7.53 | ~ (v3 = 0) | v5 = 0))))) % 50.38/7.53 | % 50.38/7.53 | ALPHA: (7) implies: % 50.38/7.54 | (8) (all_32_1 = 0 & all_32_3 = 0 & ~ (all_32_0 = 0) & implies(all_32_5, % 50.38/7.54 | all_32_4) = all_32_2 & is_a_theorem(all_32_2) = 0 & % 50.38/7.54 | is_a_theorem(all_32_4) = all_32_0 & is_a_theorem(all_32_5) = 0 & % 50.38/7.54 | $i(all_32_2) & ~ modus_ponens) | (modus_ponens & ! [v0: $i] : ! % 50.38/7.54 | [v1: $i] : ! [v2: $i] : ( ~ (implies(v0, v1) = v2) | ~ $i(v1) | ~ % 50.38/7.54 | $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 50.38/7.54 | (is_a_theorem(v2) = v4 & is_a_theorem(v1) = v5 & is_a_theorem(v0) = % 50.38/7.54 | v3 & ( ~ (v4 = 0) | ~ (v3 = 0) | v5 = 0)))) % 50.38/7.54 | % 50.38/7.54 | DELTA: instantiating (r3) with fresh symbols all_38_0, all_38_1, all_38_2, % 50.38/7.54 | all_38_3, all_38_4, all_38_5 gives: % 50.38/7.54 | (9) $i(all_38_4) & $i(all_38_5) & (( ~ (all_38_0 = 0) & or(all_38_4, % 50.38/7.54 | all_38_5) = all_38_2 & or(all_38_5, all_38_4) = all_38_3 & % 50.38/7.54 | implies(all_38_3, all_38_2) = all_38_1 & is_a_theorem(all_38_1) = % 50.38/7.54 | all_38_0 & $i(all_38_1) & $i(all_38_2) & $i(all_38_3) & ~ r3) | % 50.38/7.54 | (r3 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (or(v1, v0) = v2) % 50.38/7.54 | | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : (or(v0, v1) % 50.38/7.54 | = v3 & implies(v3, v2) = v4 & is_a_theorem(v4) = 0 & $i(v4) & % 50.38/7.54 | $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 50.38/7.54 | (or(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: % 50.38/7.54 | $i] : (or(v1, v0) = v3 & implies(v2, v3) = v4 & % 50.38/7.54 | is_a_theorem(v4) = 0 & $i(v4) & $i(v3))))) % 50.38/7.54 | % 50.38/7.54 | ALPHA: (9) implies: % 50.38/7.54 | (10) $i(all_38_5) % 50.38/7.54 | (11) $i(all_38_4) % 50.38/7.55 | (12) ( ~ (all_38_0 = 0) & or(all_38_4, all_38_5) = all_38_2 & or(all_38_5, % 50.38/7.55 | all_38_4) = all_38_3 & implies(all_38_3, all_38_2) = all_38_1 & % 50.38/7.55 | is_a_theorem(all_38_1) = all_38_0 & $i(all_38_1) & $i(all_38_2) & % 50.38/7.55 | $i(all_38_3) & ~ r3) | (r3 & ! [v0: $i] : ! [v1: $i] : ! [v2: % 50.38/7.55 | $i] : ( ~ (or(v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] % 50.38/7.55 | : ? [v4: $i] : (or(v0, v1) = v3 & implies(v3, v2) = v4 & % 50.38/7.55 | is_a_theorem(v4) = 0 & $i(v4) & $i(v3))) & ! [v0: $i] : ! [v1: % 50.38/7.55 | $i] : ! [v2: $i] : ( ~ (or(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) % 50.38/7.55 | | ? [v3: $i] : ? [v4: $i] : (or(v1, v0) = v3 & implies(v2, v3) = % 50.38/7.55 | v4 & is_a_theorem(v4) = 0 & $i(v4) & $i(v3)))) % 50.38/7.55 | % 50.38/7.55 | DELTA: instantiating (implies_3) with fresh symbols all_42_0, all_42_1, % 50.38/7.55 | all_42_2, all_42_3, all_42_4, all_42_5, all_42_6, all_42_7, all_42_8 % 50.38/7.55 | gives: % 50.38/7.55 | (13) $i(all_42_6) & $i(all_42_7) & $i(all_42_8) & (( ~ (all_42_0 = 0) & % 50.38/7.55 | implies(all_42_4, all_42_3) = all_42_2 & implies(all_42_5, % 50.38/7.55 | all_42_2) = all_42_1 & implies(all_42_7, all_42_6) = all_42_4 & % 50.38/7.55 | implies(all_42_8, all_42_6) = all_42_3 & implies(all_42_8, % 50.38/7.55 | all_42_7) = all_42_5 & is_a_theorem(all_42_1) = all_42_0 & % 50.38/7.55 | $i(all_42_1) & $i(all_42_2) & $i(all_42_3) & $i(all_42_4) & % 50.38/7.55 | $i(all_42_5) & ~ implies_3) | (implies_3 & ! [v0: $i] : ! [v1: % 50.38/7.55 | $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( % 50.38/7.55 | ~ (implies(v3, v4) = v5) | ~ (implies(v1, v2) = v3) | ~ % 50.38/7.55 | (implies(v0, v2) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 50.38/7.55 | [v6: $i] : ? [v7: $i] : (implies(v6, v5) = v7 & implies(v0, v1) % 50.38/7.55 | = v6 & is_a_theorem(v7) = 0 & $i(v7) & $i(v6))))) % 50.38/7.55 | % 50.38/7.55 | ALPHA: (13) implies: % 50.38/7.56 | (14) ( ~ (all_42_0 = 0) & implies(all_42_4, all_42_3) = all_42_2 & % 50.38/7.56 | implies(all_42_5, all_42_2) = all_42_1 & implies(all_42_7, all_42_6) % 50.38/7.56 | = all_42_4 & implies(all_42_8, all_42_6) = all_42_3 & % 50.38/7.56 | implies(all_42_8, all_42_7) = all_42_5 & is_a_theorem(all_42_1) = % 50.38/7.56 | all_42_0 & $i(all_42_1) & $i(all_42_2) & $i(all_42_3) & $i(all_42_4) % 50.38/7.56 | & $i(all_42_5) & ~ implies_3) | (implies_3 & ! [v0: $i] : ! [v1: % 50.38/7.56 | $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ % 50.38/7.56 | (implies(v3, v4) = v5) | ~ (implies(v1, v2) = v3) | ~ % 50.38/7.56 | (implies(v0, v2) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 50.38/7.56 | [v6: $i] : ? [v7: $i] : (implies(v6, v5) = v7 & implies(v0, v1) = % 50.38/7.56 | v6 & is_a_theorem(v7) = 0 & $i(v7) & $i(v6)))) % 50.38/7.56 | % 50.38/7.56 | DELTA: instantiating (or_3) with fresh symbols all_46_0, all_46_1, all_46_2, % 50.38/7.56 | all_46_3, all_46_4, all_46_5, all_46_6, all_46_7, all_46_8, all_46_9 % 50.38/7.56 | gives: % 50.38/7.56 | (15) $i(all_46_7) & $i(all_46_8) & $i(all_46_9) & (( ~ (all_46_0 = 0) & % 50.38/7.56 | or(all_46_9, all_46_8) = all_46_4 & implies(all_46_4, all_46_7) = % 50.38/7.56 | all_46_3 & implies(all_46_5, all_46_3) = all_46_2 & % 50.38/7.56 | implies(all_46_6, all_46_2) = all_46_1 & implies(all_46_8, % 50.38/7.56 | all_46_7) = all_46_5 & implies(all_46_9, all_46_7) = all_46_6 & % 50.38/7.56 | is_a_theorem(all_46_1) = all_46_0 & $i(all_46_1) & $i(all_46_2) & % 50.38/7.56 | $i(all_46_3) & $i(all_46_4) & $i(all_46_5) & $i(all_46_6) & ~ % 50.38/7.56 | or_3) | (or_3 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 50.38/7.56 | $i] : ! [v4: $i] : ( ~ (or(v0, v1) = v3) | ~ (implies(v3, v2) % 50.38/7.56 | = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : ? % 50.38/7.56 | [v6: $i] : ? [v7: $i] : ? [v8: $i] : (implies(v6, v4) = v7 & % 50.38/7.56 | implies(v5, v7) = v8 & implies(v1, v2) = v6 & implies(v0, v2) % 50.38/7.56 | = v5 & is_a_theorem(v8) = 0 & $i(v8) & $i(v7) & $i(v6) & % 50.38/7.56 | $i(v5))))) % 50.38/7.56 | % 50.38/7.56 | ALPHA: (15) implies: % 50.38/7.56 | (16) ( ~ (all_46_0 = 0) & or(all_46_9, all_46_8) = all_46_4 & % 50.38/7.57 | implies(all_46_4, all_46_7) = all_46_3 & implies(all_46_5, all_46_3) % 50.38/7.57 | = all_46_2 & implies(all_46_6, all_46_2) = all_46_1 & % 50.38/7.57 | implies(all_46_8, all_46_7) = all_46_5 & implies(all_46_9, all_46_7) % 50.38/7.57 | = all_46_6 & is_a_theorem(all_46_1) = all_46_0 & $i(all_46_1) & % 50.38/7.57 | $i(all_46_2) & $i(all_46_3) & $i(all_46_4) & $i(all_46_5) & % 50.38/7.57 | $i(all_46_6) & ~ or_3) | (or_3 & ! [v0: $i] : ! [v1: $i] : ! % 50.38/7.57 | [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (or(v0, v1) = v3) | ~ % 50.38/7.57 | (implies(v3, v2) = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 50.38/7.57 | [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : (implies(v6, % 50.38/7.57 | v4) = v7 & implies(v5, v7) = v8 & implies(v1, v2) = v6 & % 50.38/7.57 | implies(v0, v2) = v5 & is_a_theorem(v8) = 0 & $i(v8) & $i(v7) & % 50.38/7.57 | $i(v6) & $i(v5)))) % 50.38/7.57 | % 50.38/7.57 | BETA: splitting (12) gives: % 50.38/7.57 | % 50.38/7.57 | Case 1: % 50.38/7.57 | | % 50.38/7.57 | | (17) ~ (all_38_0 = 0) & or(all_38_4, all_38_5) = all_38_2 & or(all_38_5, % 50.38/7.57 | | all_38_4) = all_38_3 & implies(all_38_3, all_38_2) = all_38_1 & % 50.38/7.57 | | is_a_theorem(all_38_1) = all_38_0 & $i(all_38_1) & $i(all_38_2) & % 50.38/7.57 | | $i(all_38_3) & ~ r3 % 50.38/7.57 | | % 50.38/7.57 | | ALPHA: (17) implies: % 50.38/7.57 | | (18) ~ (all_38_0 = 0) % 50.38/7.57 | | (19) $i(all_38_3) % 50.38/7.57 | | (20) $i(all_38_2) % 50.38/7.57 | | (21) is_a_theorem(all_38_1) = all_38_0 % 50.38/7.57 | | (22) implies(all_38_3, all_38_2) = all_38_1 % 50.38/7.57 | | (23) or(all_38_5, all_38_4) = all_38_3 % 50.38/7.57 | | (24) or(all_38_4, all_38_5) = all_38_2 % 50.38/7.57 | | % 50.38/7.57 | | BETA: splitting (op_or) gives: % 50.38/7.57 | | % 50.38/7.57 | | Case 1: % 50.38/7.57 | | | % 50.38/7.57 | | | (25) ~ op_or % 50.38/7.57 | | | % 50.38/7.57 | | | PRED_UNIFY: (25), (hilbert_op_or) imply: % 50.38/7.57 | | | (26) $false % 50.38/7.57 | | | % 50.38/7.57 | | | CLOSE: (26) is inconsistent. % 50.38/7.57 | | | % 50.38/7.57 | | Case 2: % 50.38/7.57 | | | % 50.38/7.57 | | | (27) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 50.38/7.57 | | | $i] : ( ~ (and(v2, v3) = v4) | ~ (not(v1) = v3) | ~ (not(v0) = % 50.38/7.57 | | | v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (or(v0, v1) = v5 & % 50.38/7.57 | | | not(v4) = v5 & $i(v5))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 50.38/7.57 | | | $i] : ( ~ (or(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 50.38/7.57 | | | $i] : ? [v4: $i] : ? [v5: $i] : (and(v3, v4) = v5 & not(v5) % 50.38/7.57 | | | = v2 & not(v1) = v4 & not(v0) = v3 & $i(v5) & $i(v4) & $i(v3) % 50.38/7.57 | | | & $i(v2))) % 50.38/7.57 | | | % 50.38/7.57 | | | ALPHA: (27) implies: % 50.38/7.58 | | | (28) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (or(v0, v1) = v2) | % 50.38/7.58 | | | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 50.38/7.58 | | | (and(v3, v4) = v5 & not(v5) = v2 & not(v1) = v4 & not(v0) = v3 & % 50.38/7.58 | | | $i(v5) & $i(v4) & $i(v3) & $i(v2))) % 50.38/7.58 | | | % 50.38/7.58 | | | BETA: splitting (op_implies_and) gives: % 50.38/7.58 | | | % 50.38/7.58 | | | Case 1: % 50.38/7.58 | | | | % 50.38/7.58 | | | | (29) ~ op_implies_and % 50.38/7.58 | | | | % 50.38/7.58 | | | | PRED_UNIFY: (29), (hilbert_op_implies_and) imply: % 50.38/7.58 | | | | (30) $false % 50.38/7.58 | | | | % 50.38/7.58 | | | | CLOSE: (30) is inconsistent. % 50.38/7.58 | | | | % 50.38/7.58 | | | Case 2: % 50.38/7.58 | | | | % 50.38/7.58 | | | | (31) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 50.38/7.58 | | | | (and(v0, v2) = v3) | ~ (not(v1) = v2) | ~ $i(v1) | ~ $i(v0) % 50.38/7.58 | | | | | ? [v4: $i] : (not(v3) = v4 & implies(v0, v1) = v4 & % 50.38/7.58 | | | | $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 50.38/7.58 | | | | (implies(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : % 50.38/7.58 | | | | ? [v4: $i] : (and(v0, v3) = v4 & not(v4) = v2 & not(v1) = v3 % 50.38/7.58 | | | | & $i(v4) & $i(v3) & $i(v2))) % 50.38/7.58 | | | | % 50.38/7.58 | | | | ALPHA: (31) implies: % 50.38/7.58 | | | | (32) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (implies(v0, v1) = % 50.38/7.58 | | | | v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : % 50.38/7.58 | | | | (and(v0, v3) = v4 & not(v4) = v2 & not(v1) = v3 & $i(v4) & % 50.38/7.58 | | | | $i(v3) & $i(v2))) % 50.38/7.58 | | | | % 50.38/7.58 | | | | BETA: splitting (8) gives: % 50.38/7.58 | | | | % 50.38/7.58 | | | | Case 1: % 50.38/7.58 | | | | | % 50.38/7.58 | | | | | (33) all_32_1 = 0 & all_32_3 = 0 & ~ (all_32_0 = 0) & % 50.38/7.58 | | | | | implies(all_32_5, all_32_4) = all_32_2 & % 50.38/7.58 | | | | | is_a_theorem(all_32_2) = 0 & is_a_theorem(all_32_4) = all_32_0 % 50.38/7.58 | | | | | & is_a_theorem(all_32_5) = 0 & $i(all_32_2) & ~ modus_ponens % 50.38/7.58 | | | | | % 50.38/7.58 | | | | | ALPHA: (33) implies: % 50.38/7.58 | | | | | (34) ~ modus_ponens % 50.38/7.58 | | | | | % 50.38/7.58 | | | | | PRED_UNIFY: (34), (hilbert_modus_ponens) imply: % 50.38/7.58 | | | | | (35) $false % 50.38/7.58 | | | | | % 50.38/7.58 | | | | | CLOSE: (35) is inconsistent. % 50.38/7.58 | | | | | % 50.38/7.58 | | | | Case 2: % 50.38/7.58 | | | | | % 50.38/7.58 | | | | | (36) modus_ponens & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 50.38/7.58 | | | | | (implies(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 50.38/7.58 | | | | | any] : ? [v4: any] : ? [v5: any] : (is_a_theorem(v2) = % 50.38/7.58 | | | | | v4 & is_a_theorem(v1) = v5 & is_a_theorem(v0) = v3 & ( ~ % 50.38/7.58 | | | | | (v4 = 0) | ~ (v3 = 0) | v5 = 0))) % 50.38/7.58 | | | | | % 50.38/7.58 | | | | | ALPHA: (36) implies: % 50.38/7.59 | | | | | (37) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (implies(v0, v1) % 50.38/7.59 | | | | | = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 50.38/7.59 | | | | | any] : ? [v5: any] : (is_a_theorem(v2) = v4 & % 50.38/7.59 | | | | | is_a_theorem(v1) = v5 & is_a_theorem(v0) = v3 & ( ~ (v4 = % 50.38/7.59 | | | | | 0) | ~ (v3 = 0) | v5 = 0))) % 50.38/7.59 | | | | | % 50.38/7.59 | | | | | BETA: splitting (16) gives: % 50.38/7.59 | | | | | % 50.38/7.59 | | | | | Case 1: % 50.38/7.59 | | | | | | % 50.38/7.59 | | | | | | (38) ~ (all_46_0 = 0) & or(all_46_9, all_46_8) = all_46_4 & % 50.38/7.59 | | | | | | implies(all_46_4, all_46_7) = all_46_3 & implies(all_46_5, % 50.38/7.59 | | | | | | all_46_3) = all_46_2 & implies(all_46_6, all_46_2) = % 50.38/7.59 | | | | | | all_46_1 & implies(all_46_8, all_46_7) = all_46_5 & % 50.38/7.59 | | | | | | implies(all_46_9, all_46_7) = all_46_6 & % 50.38/7.59 | | | | | | is_a_theorem(all_46_1) = all_46_0 & $i(all_46_1) & % 50.38/7.59 | | | | | | $i(all_46_2) & $i(all_46_3) & $i(all_46_4) & $i(all_46_5) & % 50.38/7.59 | | | | | | $i(all_46_6) & ~ or_3 % 50.38/7.59 | | | | | | % 50.38/7.59 | | | | | | ALPHA: (38) implies: % 50.38/7.59 | | | | | | (39) ~ or_3 % 50.38/7.59 | | | | | | % 50.38/7.59 | | | | | | PRED_UNIFY: (39), (hilbert_or_3) imply: % 50.38/7.59 | | | | | | (40) $false % 50.38/7.59 | | | | | | % 50.38/7.59 | | | | | | CLOSE: (40) is inconsistent. % 50.38/7.59 | | | | | | % 50.38/7.59 | | | | | Case 2: % 50.38/7.59 | | | | | | % 50.38/7.59 | | | | | | (41) or_3 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 50.38/7.59 | | | | | | : ! [v4: $i] : ( ~ (or(v0, v1) = v3) | ~ (implies(v3, v2) % 50.38/7.59 | | | | | | = v4) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] % 50.38/7.59 | | | | | | : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : (implies(v6, % 50.38/7.59 | | | | | | v4) = v7 & implies(v5, v7) = v8 & implies(v1, v2) = v6 % 50.38/7.59 | | | | | | & implies(v0, v2) = v5 & is_a_theorem(v8) = 0 & $i(v8) & % 50.38/7.59 | | | | | | $i(v7) & $i(v6) & $i(v5))) % 50.38/7.59 | | | | | | % 50.38/7.59 | | | | | | ALPHA: (41) implies: % 50.38/7.59 | | | | | | (42) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 50.38/7.59 | | | | | | [v4: $i] : ( ~ (or(v0, v1) = v3) | ~ (implies(v3, v2) = v4) % 50.38/7.59 | | | | | | | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : ? % 50.38/7.59 | | | | | | [v6: $i] : ? [v7: $i] : ? [v8: $i] : (implies(v6, v4) = % 50.38/7.59 | | | | | | v7 & implies(v5, v7) = v8 & implies(v1, v2) = v6 & % 50.38/7.59 | | | | | | implies(v0, v2) = v5 & is_a_theorem(v8) = 0 & $i(v8) & % 50.38/7.59 | | | | | | $i(v7) & $i(v6) & $i(v5))) % 50.38/7.59 | | | | | | % 50.38/7.59 | | | | | | BETA: splitting (4) gives: % 50.38/7.59 | | | | | | % 50.38/7.59 | | | | | | Case 1: % 50.38/7.59 | | | | | | | % 50.38/7.59 | | | | | | | (43) ~ (all_20_0 = 0) & or(all_20_4, all_20_3) = all_20_2 & % 50.38/7.59 | | | | | | | implies(all_20_4, all_20_2) = all_20_1 & % 50.38/7.59 | | | | | | | is_a_theorem(all_20_1) = all_20_0 & $i(all_20_1) & % 50.38/7.59 | | | | | | | $i(all_20_2) & ~ or_1 % 50.38/7.59 | | | | | | | % 50.38/7.59 | | | | | | | ALPHA: (43) implies: % 50.38/7.59 | | | | | | | (44) ~ or_1 % 50.38/7.59 | | | | | | | % 50.38/7.59 | | | | | | | PRED_UNIFY: (44), (hilbert_or_1) imply: % 50.38/7.59 | | | | | | | (45) $false % 50.38/7.59 | | | | | | | % 50.38/7.59 | | | | | | | CLOSE: (45) is inconsistent. % 50.38/7.59 | | | | | | | % 50.38/7.59 | | | | | | Case 2: % 50.38/7.59 | | | | | | | % 50.38/7.59 | | | | | | | (46) or_1 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 50.38/7.59 | | | | | | | (or(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] % 50.38/7.59 | | | | | | | : (implies(v0, v2) = v3 & is_a_theorem(v3) = 0 & % 50.38/7.59 | | | | | | | $i(v3))) % 50.38/7.59 | | | | | | | % 50.38/7.59 | | | | | | | ALPHA: (46) implies: % 50.38/7.59 | | | | | | | (47) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (or(v0, v1) % 50.38/7.59 | | | | | | | = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : % 50.38/7.59 | | | | | | | (implies(v0, v2) = v3 & is_a_theorem(v3) = 0 & $i(v3))) % 50.38/7.59 | | | | | | | % 50.38/7.59 | | | | | | | BETA: splitting (6) gives: % 50.38/7.59 | | | | | | | % 50.38/7.59 | | | | | | | Case 1: % 50.38/7.59 | | | | | | | | % 50.38/7.60 | | | | | | | | (48) ~ (all_22_0 = 0) & or(all_22_4, all_22_3) = all_22_2 & % 50.38/7.60 | | | | | | | | implies(all_22_3, all_22_2) = all_22_1 & % 50.38/7.60 | | | | | | | | is_a_theorem(all_22_1) = all_22_0 & $i(all_22_1) & % 50.38/7.60 | | | | | | | | $i(all_22_2) & ~ or_2 % 50.38/7.60 | | | | | | | | % 50.38/7.60 | | | | | | | | ALPHA: (48) implies: % 50.38/7.60 | | | | | | | | (49) ~ or_2 % 50.38/7.60 | | | | | | | | % 50.38/7.60 | | | | | | | | PRED_UNIFY: (49), (hilbert_or_2) imply: % 50.38/7.60 | | | | | | | | (50) $false % 50.38/7.60 | | | | | | | | % 50.38/7.60 | | | | | | | | CLOSE: (50) is inconsistent. % 50.38/7.60 | | | | | | | | % 50.38/7.60 | | | | | | | Case 2: % 50.38/7.60 | | | | | | | | % 50.87/7.60 | | | | | | | | (51) or_2 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 50.87/7.60 | | | | | | | | (or(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 50.87/7.60 | | | | | | | | $i] : (implies(v1, v2) = v3 & is_a_theorem(v3) = 0 & % 50.87/7.60 | | | | | | | | $i(v3))) % 50.87/7.60 | | | | | | | | % 50.87/7.60 | | | | | | | | ALPHA: (51) implies: % 50.87/7.60 | | | | | | | | (52) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (or(v0, % 50.87/7.60 | | | | | | | | v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : % 50.87/7.60 | | | | | | | | (implies(v1, v2) = v3 & is_a_theorem(v3) = 0 & % 50.87/7.60 | | | | | | | | $i(v3))) % 50.87/7.60 | | | | | | | | % 50.87/7.60 | | | | | | | | BETA: splitting (14) gives: % 50.87/7.60 | | | | | | | | % 50.87/7.60 | | | | | | | | Case 1: % 50.87/7.60 | | | | | | | | | % 50.87/7.60 | | | | | | | | | (53) ~ (all_42_0 = 0) & implies(all_42_4, all_42_3) = % 50.87/7.60 | | | | | | | | | all_42_2 & implies(all_42_5, all_42_2) = all_42_1 & % 50.87/7.60 | | | | | | | | | implies(all_42_7, all_42_6) = all_42_4 & % 50.87/7.60 | | | | | | | | | implies(all_42_8, all_42_6) = all_42_3 & % 50.87/7.60 | | | | | | | | | implies(all_42_8, all_42_7) = all_42_5 & % 50.87/7.60 | | | | | | | | | is_a_theorem(all_42_1) = all_42_0 & $i(all_42_1) & % 50.87/7.60 | | | | | | | | | $i(all_42_2) & $i(all_42_3) & $i(all_42_4) & % 50.87/7.60 | | | | | | | | | $i(all_42_5) & ~ implies_3 % 50.87/7.60 | | | | | | | | | % 50.87/7.60 | | | | | | | | | ALPHA: (53) implies: % 50.87/7.60 | | | | | | | | | (54) ~ implies_3 % 50.87/7.60 | | | | | | | | | % 50.87/7.60 | | | | | | | | | PRED_UNIFY: (54), (hilbert_implies_3) imply: % 50.87/7.60 | | | | | | | | | (55) $false % 50.87/7.60 | | | | | | | | | % 50.87/7.60 | | | | | | | | | CLOSE: (55) is inconsistent. % 50.87/7.60 | | | | | | | | | % 50.87/7.60 | | | | | | | | Case 2: % 50.87/7.60 | | | | | | | | | % 50.87/7.60 | | | | | | | | | % 50.87/7.60 | | | | | | | | | GROUND_INST: instantiating (37) with all_38_3, all_38_2, % 50.87/7.60 | | | | | | | | | all_38_1, simplifying with (19), (20), (22) gives: % 50.87/7.60 | | | | | | | | | (56) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 50.87/7.60 | | | | | | | | | (is_a_theorem(all_38_1) = v1 & is_a_theorem(all_38_2) % 50.87/7.60 | | | | | | | | | = v2 & is_a_theorem(all_38_3) = v0 & ( ~ (v1 = 0) | % 50.87/7.60 | | | | | | | | | ~ (v0 = 0) | v2 = 0)) % 50.87/7.60 | | | | | | | | | % 50.87/7.60 | | | | | | | | | GROUND_INST: instantiating (32) with all_38_3, all_38_2, % 50.87/7.60 | | | | | | | | | all_38_1, simplifying with (19), (20), (22) gives: % 50.87/7.60 | | | | | | | | | (57) ? [v0: $i] : ? [v1: $i] : (and(all_38_3, v0) = v1 & % 50.87/7.60 | | | | | | | | | not(v1) = all_38_1 & not(all_38_2) = v0 & $i(v1) & % 50.87/7.60 | | | | | | | | | $i(v0) & $i(all_38_1)) % 50.87/7.60 | | | | | | | | | % 50.87/7.61 | | | | | | | | | GROUND_INST: instantiating (42) with all_38_5, all_38_4, % 50.87/7.61 | | | | | | | | | all_38_2, all_38_3, all_38_1, simplifying with % 50.87/7.61 | | | | | | | | | (10), (11), (20), (22), (23) gives: % 50.87/7.61 | | | | | | | | | (58) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] % 50.87/7.61 | | | | | | | | | : (implies(v1, all_38_1) = v2 & implies(v0, v2) = v3 & % 50.87/7.61 | | | | | | | | | implies(all_38_4, all_38_2) = v1 & implies(all_38_5, % 50.87/7.61 | | | | | | | | | all_38_2) = v0 & is_a_theorem(v3) = 0 & $i(v3) & % 50.87/7.61 | | | | | | | | | $i(v2) & $i(v1) & $i(v0)) % 50.87/7.61 | | | | | | | | | % 50.87/7.61 | | | | | | | | | GROUND_INST: instantiating (28) with all_38_4, all_38_5, % 50.87/7.61 | | | | | | | | | all_38_2, simplifying with (10), (11), (24) gives: % 50.87/7.61 | | | | | | | | | (59) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (and(v0, v1) % 50.87/7.61 | | | | | | | | | = v2 & not(v2) = all_38_2 & not(all_38_4) = v0 & % 50.87/7.61 | | | | | | | | | not(all_38_5) = v1 & $i(v2) & $i(v1) & $i(v0) & % 50.87/7.61 | | | | | | | | | $i(all_38_2)) % 50.87/7.61 | | | | | | | | | % 50.87/7.61 | | | | | | | | | GROUND_INST: instantiating (52) with all_38_4, all_38_5, % 50.87/7.61 | | | | | | | | | all_38_2, simplifying with (10), (11), (24) gives: % 50.87/7.61 | | | | | | | | | (60) ? [v0: $i] : (implies(all_38_5, all_38_2) = v0 & % 50.87/7.61 | | | | | | | | | is_a_theorem(v0) = 0 & $i(v0)) % 50.87/7.61 | | | | | | | | | % 50.87/7.61 | | | | | | | | | GROUND_INST: instantiating (47) with all_38_4, all_38_5, % 50.87/7.61 | | | | | | | | | all_38_2, simplifying with (10), (11), (24) gives: % 50.87/7.61 | | | | | | | | | (61) ? [v0: $i] : (implies(all_38_4, all_38_2) = v0 & % 50.87/7.61 | | | | | | | | | is_a_theorem(v0) = 0 & $i(v0)) % 50.87/7.61 | | | | | | | | | % 50.87/7.61 | | | | | | | | | DELTA: instantiating (61) with fresh symbol all_146_0 gives: % 50.87/7.61 | | | | | | | | | (62) implies(all_38_4, all_38_2) = all_146_0 & % 50.87/7.61 | | | | | | | | | is_a_theorem(all_146_0) = 0 & $i(all_146_0) % 50.87/7.61 | | | | | | | | | % 50.87/7.61 | | | | | | | | | ALPHA: (62) implies: % 50.87/7.61 | | | | | | | | | (63) is_a_theorem(all_146_0) = 0 % 50.87/7.62 | | | | | | | | | (64) implies(all_38_4, all_38_2) = all_146_0 % 50.87/7.62 | | | | | | | | | % 50.87/7.62 | | | | | | | | | DELTA: instantiating (60) with fresh symbol all_154_0 gives: % 50.87/7.62 | | | | | | | | | (65) implies(all_38_5, all_38_2) = all_154_0 & % 50.87/7.62 | | | | | | | | | is_a_theorem(all_154_0) = 0 & $i(all_154_0) % 50.87/7.62 | | | | | | | | | % 50.87/7.62 | | | | | | | | | ALPHA: (65) implies: % 50.87/7.62 | | | | | | | | | (66) is_a_theorem(all_154_0) = 0 % 50.87/7.62 | | | | | | | | | (67) implies(all_38_5, all_38_2) = all_154_0 % 50.87/7.62 | | | | | | | | | % 50.87/7.62 | | | | | | | | | DELTA: instantiating (57) with fresh symbols all_168_0, % 50.87/7.62 | | | | | | | | | all_168_1 gives: % 50.87/7.63 | | | | | | | | | (68) and(all_38_3, all_168_1) = all_168_0 & not(all_168_0) % 50.87/7.63 | | | | | | | | | = all_38_1 & not(all_38_2) = all_168_1 & $i(all_168_0) % 50.87/7.63 | | | | | | | | | & $i(all_168_1) & $i(all_38_1) % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | ALPHA: (68) implies: % 50.87/7.63 | | | | | | | | | (69) $i(all_38_1) % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | DELTA: instantiating (56) with fresh symbols all_170_0, % 50.87/7.63 | | | | | | | | | all_170_1, all_170_2 gives: % 50.87/7.63 | | | | | | | | | (70) is_a_theorem(all_38_1) = all_170_1 & % 50.87/7.63 | | | | | | | | | is_a_theorem(all_38_2) = all_170_0 & % 50.87/7.63 | | | | | | | | | is_a_theorem(all_38_3) = all_170_2 & ( ~ (all_170_1 = % 50.87/7.63 | | | | | | | | | 0) | ~ (all_170_2 = 0) | all_170_0 = 0) % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | ALPHA: (70) implies: % 50.87/7.63 | | | | | | | | | (71) is_a_theorem(all_38_1) = all_170_1 % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | DELTA: instantiating (59) with fresh symbols all_174_0, % 50.87/7.63 | | | | | | | | | all_174_1, all_174_2 gives: % 50.87/7.63 | | | | | | | | | (72) and(all_174_2, all_174_1) = all_174_0 & not(all_174_0) % 50.87/7.63 | | | | | | | | | = all_38_2 & not(all_38_4) = all_174_2 & not(all_38_5) % 50.87/7.63 | | | | | | | | | = all_174_1 & $i(all_174_0) & $i(all_174_1) & % 50.87/7.63 | | | | | | | | | $i(all_174_2) & $i(all_38_2) % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | DELTA: instantiating (58) with fresh symbols all_178_0, % 50.87/7.63 | | | | | | | | | all_178_1, all_178_2, all_178_3 gives: % 50.87/7.63 | | | | | | | | | (73) implies(all_178_2, all_38_1) = all_178_1 & % 50.87/7.63 | | | | | | | | | implies(all_178_3, all_178_1) = all_178_0 & % 50.87/7.63 | | | | | | | | | implies(all_38_4, all_38_2) = all_178_2 & % 50.87/7.63 | | | | | | | | | implies(all_38_5, all_38_2) = all_178_3 & % 50.87/7.63 | | | | | | | | | is_a_theorem(all_178_0) = 0 & $i(all_178_0) & % 50.87/7.63 | | | | | | | | | $i(all_178_1) & $i(all_178_2) & $i(all_178_3) % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | ALPHA: (73) implies: % 50.87/7.63 | | | | | | | | | (74) $i(all_178_3) % 50.87/7.63 | | | | | | | | | (75) $i(all_178_2) % 50.87/7.63 | | | | | | | | | (76) $i(all_178_1) % 50.87/7.63 | | | | | | | | | (77) is_a_theorem(all_178_0) = 0 % 50.87/7.63 | | | | | | | | | (78) implies(all_38_5, all_38_2) = all_178_3 % 50.87/7.63 | | | | | | | | | (79) implies(all_38_4, all_38_2) = all_178_2 % 50.87/7.63 | | | | | | | | | (80) implies(all_178_3, all_178_1) = all_178_0 % 50.87/7.63 | | | | | | | | | (81) implies(all_178_2, all_38_1) = all_178_1 % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | GROUND_INST: instantiating (1) with all_38_0, all_170_1, % 50.87/7.63 | | | | | | | | | all_38_1, simplifying with (21), (71) gives: % 50.87/7.63 | | | | | | | | | (82) all_170_1 = all_38_0 % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | GROUND_INST: instantiating (2) with all_154_0, all_178_3, % 50.87/7.63 | | | | | | | | | all_38_2, all_38_5, simplifying with (67), (78) % 50.87/7.63 | | | | | | | | | gives: % 50.87/7.63 | | | | | | | | | (83) all_178_3 = all_154_0 % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | GROUND_INST: instantiating (2) with all_146_0, all_178_2, % 50.87/7.63 | | | | | | | | | all_38_2, all_38_4, simplifying with (64), (79) % 50.87/7.63 | | | | | | | | | gives: % 50.87/7.63 | | | | | | | | | (84) all_178_2 = all_146_0 % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | REDUCE: (81), (84) imply: % 50.87/7.63 | | | | | | | | | (85) implies(all_146_0, all_38_1) = all_178_1 % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | REDUCE: (80), (83) imply: % 50.87/7.63 | | | | | | | | | (86) implies(all_154_0, all_178_1) = all_178_0 % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | REDUCE: (75), (84) imply: % 50.87/7.63 | | | | | | | | | (87) $i(all_146_0) % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | REDUCE: (74), (83) imply: % 50.87/7.63 | | | | | | | | | (88) $i(all_154_0) % 50.87/7.63 | | | | | | | | | % 50.87/7.63 | | | | | | | | | GROUND_INST: instantiating (37) with all_38_5, all_38_2, % 50.87/7.63 | | | | | | | | | all_154_0, simplifying with (10), (20), (67) % 50.87/7.63 | | | | | | | | | gives: % 50.87/7.64 | | | | | | | | | (89) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 50.87/7.64 | | | | | | | | | (is_a_theorem(all_154_0) = v1 & is_a_theorem(all_38_2) % 50.87/7.64 | | | | | | | | | = v2 & is_a_theorem(all_38_5) = v0 & ( ~ (v1 = 0) | % 50.87/7.64 | | | | | | | | | ~ (v0 = 0) | v2 = 0)) % 50.87/7.64 | | | | | | | | | % 50.87/7.64 | | | | | | | | | GROUND_INST: instantiating (37) with all_38_4, all_38_2, % 50.87/7.64 | | | | | | | | | all_146_0, simplifying with (11), (20), (64) % 50.87/7.64 | | | | | | | | | gives: % 50.87/7.64 | | | | | | | | | (90) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 50.87/7.64 | | | | | | | | | (is_a_theorem(all_146_0) = v1 & is_a_theorem(all_38_2) % 50.87/7.64 | | | | | | | | | = v2 & is_a_theorem(all_38_4) = v0 & ( ~ (v1 = 0) | % 50.87/7.64 | | | | | | | | | ~ (v0 = 0) | v2 = 0)) % 50.87/7.64 | | | | | | | | | % 50.87/7.64 | | | | | | | | | GROUND_INST: instantiating (37) with all_146_0, all_38_1, % 50.87/7.64 | | | | | | | | | all_178_1, simplifying with (69), (85), (87) % 50.87/7.64 | | | | | | | | | gives: % 50.87/7.64 | | | | | | | | | (91) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 50.87/7.64 | | | | | | | | | (is_a_theorem(all_178_1) = v1 & % 50.87/7.64 | | | | | | | | | is_a_theorem(all_146_0) = v0 & % 50.87/7.64 | | | | | | | | | is_a_theorem(all_38_1) = v2 & ( ~ (v1 = 0) | ~ (v0 % 50.87/7.64 | | | | | | | | | = 0) | v2 = 0)) % 50.87/7.64 | | | | | | | | | % 50.87/7.64 | | | | | | | | | GROUND_INST: instantiating (37) with all_154_0, all_178_1, % 50.87/7.64 | | | | | | | | | all_178_0, simplifying with (76), (86), (88) % 50.87/7.64 | | | | | | | | | gives: % 50.87/7.64 | | | | | | | | | (92) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 50.87/7.64 | | | | | | | | | (is_a_theorem(all_178_0) = v1 & % 50.87/7.64 | | | | | | | | | is_a_theorem(all_178_1) = v2 & % 50.87/7.64 | | | | | | | | | is_a_theorem(all_154_0) = v0 & ( ~ (v1 = 0) | ~ (v0 % 50.87/7.64 | | | | | | | | | = 0) | v2 = 0)) % 50.87/7.64 | | | | | | | | | % 50.87/7.64 | | | | | | | | | DELTA: instantiating (90) with fresh symbols all_630_0, % 50.87/7.64 | | | | | | | | | all_630_1, all_630_2 gives: % 50.87/7.64 | | | | | | | | | (93) is_a_theorem(all_146_0) = all_630_1 & % 50.87/7.64 | | | | | | | | | is_a_theorem(all_38_2) = all_630_0 & % 50.87/7.64 | | | | | | | | | is_a_theorem(all_38_4) = all_630_2 & ( ~ (all_630_1 = % 50.87/7.64 | | | | | | | | | 0) | ~ (all_630_2 = 0) | all_630_0 = 0) % 50.87/7.64 | | | | | | | | | % 50.87/7.64 | | | | | | | | | ALPHA: (93) implies: % 50.87/7.64 | | | | | | | | | (94) is_a_theorem(all_146_0) = all_630_1 % 50.87/7.64 | | | | | | | | | % 50.87/7.64 | | | | | | | | | DELTA: instantiating (89) with fresh symbols all_638_0, % 50.87/7.64 | | | | | | | | | all_638_1, all_638_2 gives: % 50.87/7.64 | | | | | | | | | (95) is_a_theorem(all_154_0) = all_638_1 & % 50.87/7.64 | | | | | | | | | is_a_theorem(all_38_2) = all_638_0 & % 50.87/7.64 | | | | | | | | | is_a_theorem(all_38_5) = all_638_2 & ( ~ (all_638_1 = % 50.87/7.64 | | | | | | | | | 0) | ~ (all_638_2 = 0) | all_638_0 = 0) % 50.87/7.64 | | | | | | | | | % 50.87/7.64 | | | | | | | | | ALPHA: (95) implies: % 50.87/7.64 | | | | | | | | | (96) is_a_theorem(all_154_0) = all_638_1 % 50.87/7.64 | | | | | | | | | % 50.87/7.64 | | | | | | | | | DELTA: instantiating (92) with fresh symbols all_666_0, % 50.87/7.64 | | | | | | | | | all_666_1, all_666_2 gives: % 50.87/7.65 | | | | | | | | | (97) is_a_theorem(all_178_0) = all_666_1 & % 50.87/7.65 | | | | | | | | | is_a_theorem(all_178_1) = all_666_0 & % 50.87/7.65 | | | | | | | | | is_a_theorem(all_154_0) = all_666_2 & ( ~ (all_666_1 = % 50.87/7.65 | | | | | | | | | 0) | ~ (all_666_2 = 0) | all_666_0 = 0) % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | ALPHA: (97) implies: % 50.87/7.65 | | | | | | | | | (98) is_a_theorem(all_154_0) = all_666_2 % 50.87/7.65 | | | | | | | | | (99) is_a_theorem(all_178_1) = all_666_0 % 50.87/7.65 | | | | | | | | | (100) is_a_theorem(all_178_0) = all_666_1 % 50.87/7.65 | | | | | | | | | (101) ~ (all_666_1 = 0) | ~ (all_666_2 = 0) | all_666_0 = % 50.87/7.65 | | | | | | | | | 0 % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | DELTA: instantiating (91) with fresh symbols all_680_0, % 50.87/7.65 | | | | | | | | | all_680_1, all_680_2 gives: % 50.87/7.65 | | | | | | | | | (102) is_a_theorem(all_178_1) = all_680_1 & % 50.87/7.65 | | | | | | | | | is_a_theorem(all_146_0) = all_680_2 & % 50.87/7.65 | | | | | | | | | is_a_theorem(all_38_1) = all_680_0 & ( ~ (all_680_1 = % 50.87/7.65 | | | | | | | | | 0) | ~ (all_680_2 = 0) | all_680_0 = 0) % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | ALPHA: (102) implies: % 50.87/7.65 | | | | | | | | | (103) is_a_theorem(all_38_1) = all_680_0 % 50.87/7.65 | | | | | | | | | (104) is_a_theorem(all_146_0) = all_680_2 % 50.87/7.65 | | | | | | | | | (105) is_a_theorem(all_178_1) = all_680_1 % 50.87/7.65 | | | | | | | | | (106) ~ (all_680_1 = 0) | ~ (all_680_2 = 0) | all_680_0 = % 50.87/7.65 | | | | | | | | | 0 % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | GROUND_INST: instantiating (1) with all_38_0, all_680_0, % 50.87/7.65 | | | | | | | | | all_38_1, simplifying with (21), (103) gives: % 50.87/7.65 | | | | | | | | | (107) all_680_0 = all_38_0 % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | GROUND_INST: instantiating (1) with 0, all_680_2, all_146_0, % 50.87/7.65 | | | | | | | | | simplifying with (63), (104) gives: % 50.87/7.65 | | | | | | | | | (108) all_680_2 = 0 % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | GROUND_INST: instantiating (1) with all_630_1, all_680_2, % 50.87/7.65 | | | | | | | | | all_146_0, simplifying with (94), (104) gives: % 50.87/7.65 | | | | | | | | | (109) all_680_2 = all_630_1 % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | GROUND_INST: instantiating (1) with 0, all_666_2, all_154_0, % 50.87/7.65 | | | | | | | | | simplifying with (66), (98) gives: % 50.87/7.65 | | | | | | | | | (110) all_666_2 = 0 % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | GROUND_INST: instantiating (1) with all_638_1, all_666_2, % 50.87/7.65 | | | | | | | | | all_154_0, simplifying with (96), (98) gives: % 50.87/7.65 | | | | | | | | | (111) all_666_2 = all_638_1 % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | GROUND_INST: instantiating (1) with all_666_0, all_680_1, % 50.87/7.65 | | | | | | | | | all_178_1, simplifying with (99), (105) gives: % 50.87/7.65 | | | | | | | | | (112) all_680_1 = all_666_0 % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | GROUND_INST: instantiating (1) with 0, all_666_1, all_178_0, % 50.87/7.65 | | | | | | | | | simplifying with (77), (100) gives: % 50.87/7.65 | | | | | | | | | (113) all_666_1 = 0 % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | COMBINE_EQS: (108), (109) imply: % 50.87/7.65 | | | | | | | | | (114) all_630_1 = 0 % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | COMBINE_EQS: (110), (111) imply: % 50.87/7.65 | | | | | | | | | (115) all_638_1 = 0 % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | BETA: splitting (106) gives: % 50.87/7.65 | | | | | | | | | % 50.87/7.65 | | | | | | | | | Case 1: % 50.87/7.65 | | | | | | | | | | % 50.87/7.65 | | | | | | | | | | (116) ~ (all_680_1 = 0) % 50.87/7.65 | | | | | | | | | | % 50.87/7.65 | | | | | | | | | | REDUCE: (112), (116) imply: % 50.87/7.65 | | | | | | | | | | (117) ~ (all_666_0 = 0) % 50.87/7.65 | | | | | | | | | | % 50.87/7.65 | | | | | | | | | | BETA: splitting (101) gives: % 50.87/7.65 | | | | | | | | | | % 50.87/7.65 | | | | | | | | | | Case 1: % 50.87/7.65 | | | | | | | | | | | % 50.87/7.65 | | | | | | | | | | | (118) ~ (all_666_1 = 0) % 50.87/7.65 | | | | | | | | | | | % 50.87/7.65 | | | | | | | | | | | REDUCE: (113), (118) imply: % 50.87/7.65 | | | | | | | | | | | (119) $false % 50.87/7.65 | | | | | | | | | | | % 50.87/7.65 | | | | | | | | | | | CLOSE: (119) is inconsistent. % 50.87/7.65 | | | | | | | | | | | % 50.87/7.65 | | | | | | | | | | Case 2: % 50.87/7.65 | | | | | | | | | | | % 50.87/7.65 | | | | | | | | | | | (120) ~ (all_666_2 = 0) | all_666_0 = 0 % 50.87/7.66 | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | BETA: splitting (120) gives: % 50.87/7.66 | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | Case 1: % 50.87/7.66 | | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | | (121) ~ (all_666_2 = 0) % 50.87/7.66 | | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | | REDUCE: (110), (121) imply: % 50.87/7.66 | | | | | | | | | | | | (122) $false % 50.87/7.66 | | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | | CLOSE: (122) is inconsistent. % 50.87/7.66 | | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | Case 2: % 50.87/7.66 | | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | | (123) all_666_0 = 0 % 50.87/7.66 | | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | | REDUCE: (117), (123) imply: % 50.87/7.66 | | | | | | | | | | | | (124) $false % 50.87/7.66 | | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | | CLOSE: (124) is inconsistent. % 50.87/7.66 | | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | End of split % 50.87/7.66 | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | End of split % 50.87/7.66 | | | | | | | | | | % 50.87/7.66 | | | | | | | | | Case 2: % 50.87/7.66 | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | (125) ~ (all_680_2 = 0) | all_680_0 = 0 % 50.87/7.66 | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | BETA: splitting (125) gives: % 50.87/7.66 | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | Case 1: % 50.87/7.66 | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | (126) ~ (all_680_2 = 0) % 50.87/7.66 | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | REDUCE: (108), (126) imply: % 50.87/7.66 | | | | | | | | | | | (127) $false % 50.87/7.66 | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | CLOSE: (127) is inconsistent. % 50.87/7.66 | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | Case 2: % 50.87/7.66 | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | (128) all_680_0 = 0 % 50.87/7.66 | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | COMBINE_EQS: (107), (128) imply: % 50.87/7.66 | | | | | | | | | | | (129) all_38_0 = 0 % 50.87/7.66 | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | SIMP: (129) implies: % 50.87/7.66 | | | | | | | | | | | (130) all_38_0 = 0 % 50.87/7.66 | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | REDUCE: (18), (130) imply: % 50.87/7.66 | | | | | | | | | | | (131) $false % 50.87/7.66 | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | | CLOSE: (131) is inconsistent. % 50.87/7.66 | | | | | | | | | | | % 50.87/7.66 | | | | | | | | | | End of split % 50.87/7.66 | | | | | | | | | | % 50.87/7.66 | | | | | | | | | End of split % 50.87/7.66 | | | | | | | | | % 50.87/7.66 | | | | | | | | End of split % 50.87/7.66 | | | | | | | | % 50.87/7.66 | | | | | | | End of split % 50.87/7.66 | | | | | | | % 50.87/7.66 | | | | | | End of split % 50.87/7.66 | | | | | | % 50.87/7.66 | | | | | End of split % 50.87/7.66 | | | | | % 50.87/7.66 | | | | End of split % 50.87/7.66 | | | | % 50.87/7.66 | | | End of split % 50.87/7.66 | | | % 50.87/7.66 | | End of split % 50.87/7.66 | | % 50.87/7.66 | Case 2: % 50.87/7.66 | | % 50.87/7.66 | | (132) r3 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (or(v1, v0) = % 50.87/7.66 | | v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : % 50.87/7.66 | | (or(v0, v1) = v3 & implies(v3, v2) = v4 & is_a_theorem(v4) = 0 & % 50.87/7.66 | | $i(v4) & $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( % 50.87/7.66 | | ~ (or(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? % 50.87/7.66 | | [v4: $i] : (or(v1, v0) = v3 & implies(v2, v3) = v4 & % 50.87/7.66 | | is_a_theorem(v4) = 0 & $i(v4) & $i(v3))) % 50.87/7.66 | | % 50.87/7.66 | | ALPHA: (132) implies: % 50.87/7.66 | | (133) r3 % 50.87/7.66 | | % 50.87/7.66 | | PRED_UNIFY: (133), (principia_r3) imply: % 50.87/7.66 | | (134) $false % 50.87/7.66 | | % 50.87/7.66 | | CLOSE: (134) is inconsistent. % 50.87/7.66 | | % 50.87/7.66 | End of split % 50.87/7.66 | % 50.87/7.66 End of proof % 50.87/7.66 % SZS output end Proof for theBenchmark % 50.87/7.66 % 50.87/7.66 6960ms %------------------------------------------------------------------------------