%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SEU195+1 : TPTP v8.1.2. Released v3.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 17:43:11 EDT 2023 % Result : Theorem 22.89s 3.87s % Output : Proof 23.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.14 % Problem : SEU195+1 : TPTP v8.1.2. Released v3.3.0. % 0.09/0.15 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.16/0.37 % Computer : n024.cluster.edu % 0.16/0.37 % Model : x86_64 x86_64 % 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.37 % Memory : 8042.1875MB % 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.37 % CPULimit : 300 % 0.16/0.37 % WCLimit : 300 % 0.16/0.37 % DateTime : Wed Aug 23 13:23:09 EDT 2023 % 0.16/0.37 % CPUTime : % 0.23/0.65 ________ _____ % 0.23/0.65 ___ __ \_________(_)________________________________ % 0.23/0.65 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.23/0.65 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.23/0.65 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.23/0.65 % 0.23/0.65 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.23/0.65 (2023-06-19) % 0.23/0.65 % 0.23/0.65 (c) Philipp Rümmer, 2009-2023 % 0.23/0.65 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.23/0.65 Amanda Stjerna. % 0.23/0.65 Free software under BSD-3-Clause. % 0.23/0.65 % 0.23/0.65 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.23/0.65 % 0.23/0.65 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.23/0.66 Running up to 7 provers in parallel. % 0.23/0.68 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.23/0.68 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.23/0.68 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.23/0.68 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.23/0.68 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.23/0.68 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.23/0.68 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.68/1.09 Prover 1: Preprocessing ... % 2.68/1.09 Prover 4: Preprocessing ... % 2.98/1.12 Prover 0: Preprocessing ... % 2.98/1.12 Prover 3: Preprocessing ... % 2.98/1.12 Prover 6: Preprocessing ... % 2.98/1.12 Prover 5: Preprocessing ... % 2.98/1.12 Prover 2: Preprocessing ... % 5.95/1.58 Prover 1: Warning: ignoring some quantifiers % 5.95/1.60 Prover 4: Warning: ignoring some quantifiers % 5.95/1.61 Prover 3: Warning: ignoring some quantifiers % 6.36/1.62 Prover 3: Constructing countermodel ... % 6.36/1.62 Prover 1: Constructing countermodel ... % 6.36/1.63 Prover 5: Proving ... % 6.36/1.63 Prover 4: Constructing countermodel ... % 6.36/1.65 Prover 6: Proving ... % 6.64/1.65 Prover 0: Proving ... % 6.64/1.66 Prover 2: Proving ... % 22.89/3.86 Prover 1: Found proof (size 117) % 22.89/3.87 Prover 1: proved (3195ms) % 22.89/3.87 Prover 3: stopped % 22.89/3.87 Prover 6: stopped % 22.89/3.87 Prover 0: stopped % 22.89/3.87 Prover 4: stopped % 22.89/3.87 Prover 2: stopped % 22.89/3.87 Prover 5: stopped % 22.89/3.87 % 22.89/3.87 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 22.89/3.87 % 23.46/3.89 % SZS output start Proof for theBenchmark % 23.46/3.89 Assumptions after simplification: % 23.46/3.89 --------------------------------- % 23.46/3.89 % 23.46/3.89 (d11_relat_1) % 23.65/3.92 ! [v0: $i] : ( ~ (relation(v0) = 0) | ~ $i(v0) | ! [v1: $i] : ! [v2: $i] : % 23.65/3.92 ! [v3: $i] : ( ~ (relation_dom_restriction(v0, v1) = v3) | ~ (relation(v2) % 23.65/3.92 = 0) | ~ $i(v2) | ~ $i(v1) | (( ~ (v3 = v2) | ( ! [v4: $i] : ! [v5: % 23.65/3.92 $i] : ! [v6: $i] : ! [v7: any] : ( ~ (ordered_pair(v4, v5) = v6) % 23.65/3.92 | ~ (in(v6, v0) = v7) | ~ $i(v5) | ~ $i(v4) | ? [v8: any] : ? % 23.65/3.92 [v9: any] : (in(v6, v2) = v8 & in(v4, v1) = v9 & ( ~ (v8 = 0) | % 23.65/3.92 (v9 = 0 & v7 = 0)))) & ! [v4: $i] : ! [v5: $i] : ! [v6: $i] % 23.65/3.92 : ( ~ (ordered_pair(v4, v5) = v6) | ~ (in(v6, v0) = 0) | ~ $i(v5) % 23.65/3.92 | ~ $i(v4) | ? [v7: any] : ? [v8: any] : (in(v6, v2) = v8 & % 23.65/3.92 in(v4, v1) = v7 & ( ~ (v7 = 0) | v8 = 0))))) & (v3 = v2 | ? % 23.65/3.92 [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: any] : ? [v8: any] : % 23.65/3.92 ? [v9: any] : (ordered_pair(v4, v5) = v6 & in(v6, v2) = v7 & in(v6, % 23.65/3.92 v0) = v9 & in(v4, v1) = v8 & $i(v6) & $i(v5) & $i(v4) & ( ~ (v9 = % 23.65/3.92 0) | ~ (v8 = 0) | ~ (v7 = 0)) & (v7 = 0 | (v9 = 0 & v8 = % 23.65/3.92 0))))))) % 23.65/3.92 % 23.65/3.92 (dt_k5_relat_1) % 23.65/3.92 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (relation_composition(v0, v1) = % 23.65/3.92 v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 23.65/3.92 (relation(v2) = v5 & relation(v1) = v4 & relation(v0) = v3 & ( ~ (v4 = 0) | % 23.65/3.92 ~ (v3 = 0) | v5 = 0))) % 23.65/3.92 % 23.65/3.92 (dt_k6_relat_1) % 23.65/3.93 ! [v0: $i] : ! [v1: $i] : ( ~ (identity_relation(v0) = v1) | ~ $i(v0) | % 23.65/3.93 relation(v1) = 0) % 23.65/3.93 % 23.65/3.93 (dt_k7_relat_1) % 23.65/3.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (relation_dom_restriction(v0, % 23.65/3.93 v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : % 23.65/3.93 (relation(v2) = v4 & relation(v0) = v3 & ( ~ (v3 = 0) | v4 = 0))) % 23.65/3.93 % 23.65/3.93 (fc10_relat_1) % 23.65/3.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (relation_composition(v1, v0) = % 23.65/3.93 v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 23.65/3.93 ? [v6: any] : (empty(v2) = v5 & empty(v0) = v3 & relation(v2) = v6 & % 23.65/3.93 relation(v1) = v4 & ( ~ (v4 = 0) | ~ (v3 = 0) | (v6 = 0 & v5 = 0)))) % 23.65/3.93 % 23.65/3.93 (fc9_relat_1) % 23.65/3.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (relation_composition(v0, v1) = % 23.65/3.93 v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] : % 23.65/3.93 ? [v6: any] : (empty(v2) = v5 & empty(v0) = v3 & relation(v2) = v6 & % 23.65/3.93 relation(v1) = v4 & ( ~ (v4 = 0) | ~ (v3 = 0) | (v6 = 0 & v5 = 0)))) % 23.65/3.93 % 23.65/3.93 (t74_relat_1) % 23.65/3.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 23.65/3.93 $i] : ! [v6: $i] : ! [v7: any] : ( ~ (identity_relation(v2) = v5) | ~ % 23.65/3.93 (relation_composition(v5, v3) = v6) | ~ (ordered_pair(v0, v1) = v4) | ~ % 23.65/3.93 (in(v4, v6) = v7) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v8: % 23.65/3.93 any] : ? [v9: any] : ? [v10: any] : (relation(v3) = v8 & in(v4, v3) = % 23.65/3.93 v10 & in(v0, v2) = v9 & ( ~ (v8 = 0) | (( ~ (v10 = 0) | ~ (v9 = 0) | v7 = % 23.65/3.93 0) & ( ~ (v7 = 0) | (v10 = 0 & v9 = 0)))))) % 23.65/3.93 % 23.65/3.93 (t94_relat_1) % 23.65/3.93 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ( ~ (v4 % 23.65/3.93 = v2) & identity_relation(v0) = v3 & relation_composition(v3, v1) = v4 & % 23.65/3.93 relation_dom_restriction(v1, v0) = v2 & relation(v1) = 0 & $i(v4) & $i(v3) & % 23.65/3.93 $i(v2) & $i(v1) & $i(v0)) % 23.65/3.93 % 23.65/3.93 (function-axioms) % 23.74/3.94 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 23.74/3.94 [v3: $i] : (v1 = v0 | ~ (element(v3, v2) = v1) | ~ (element(v3, v2) = v0)) & % 23.74/3.94 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 23.74/3.94 (relation_composition(v3, v2) = v1) | ~ (relation_composition(v3, v2) = % 23.74/3.94 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 23.74/3.94 ~ (relation_dom_restriction(v3, v2) = v1) | ~ (relation_dom_restriction(v3, % 23.74/3.94 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 23.74/3.94 = v0 | ~ (ordered_pair(v3, v2) = v1) | ~ (ordered_pair(v3, v2) = v0)) & ! % 23.74/3.94 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 23.74/3.94 (unordered_pair(v3, v2) = v1) | ~ (unordered_pair(v3, v2) = v0)) & ! [v0: % 23.74/3.94 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 23.74/3.94 : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) & ! [v0: $i] : ! % 23.74/3.94 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (identity_relation(v2) = v1) | ~ % 23.74/3.94 (identity_relation(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 23.74/3.94 (v1 = v0 | ~ (singleton(v2) = v1) | ~ (singleton(v2) = v0)) & ! [v0: % 23.74/3.94 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | % 23.74/3.94 ~ (empty(v2) = v1) | ~ (empty(v2) = v0)) & ! [v0: MultipleValueBool] : ! % 23.74/3.94 [v1: MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (relation(v2) = v1) | ~ % 23.74/3.94 (relation(v2) = v0)) % 23.74/3.94 % 23.74/3.94 Further assumptions not needed in the proof: % 23.74/3.94 -------------------------------------------- % 23.74/3.94 antisymmetry_r2_hidden, cc1_relat_1, commutativity_k2_tarski, d2_relat_1, % 23.74/3.94 d5_tarski, dt_k1_tarski, dt_k1_xboole_0, dt_k2_tarski, dt_k4_tarski, % 23.74/3.94 dt_m1_subset_1, existence_m1_subset_1, fc1_xboole_0, fc1_zfmisc_1, fc2_subset_1, % 23.74/3.94 fc3_subset_1, fc4_relat_1, rc1_relat_1, rc1_xboole_0, rc2_relat_1, rc2_xboole_0, % 23.74/3.94 t1_subset, t2_subset, t6_boole, t7_boole, t8_boole % 23.74/3.94 % 23.74/3.94 Those formulas are unsatisfiable: % 23.74/3.94 --------------------------------- % 23.74/3.94 % 23.74/3.94 Begin of proof % 23.74/3.94 | % 23.74/3.94 | ALPHA: (function-axioms) implies: % 23.74/3.94 | (1) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.74/3.94 | (v1 = v0 | ~ (relation(v2) = v1) | ~ (relation(v2) = v0)) % 23.74/3.94 | (2) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.74/3.94 | ! [v3: $i] : (v1 = v0 | ~ (in(v3, v2) = v1) | ~ (in(v3, v2) = v0)) % 23.74/3.94 | % 23.74/3.94 | DELTA: instantiating (t94_relat_1) with fresh symbols all_33_0, all_33_1, % 23.74/3.94 | all_33_2, all_33_3, all_33_4 gives: % 23.74/3.94 | (3) ~ (all_33_0 = all_33_2) & identity_relation(all_33_4) = all_33_1 & % 23.74/3.94 | relation_composition(all_33_1, all_33_3) = all_33_0 & % 23.74/3.94 | relation_dom_restriction(all_33_3, all_33_4) = all_33_2 & % 23.74/3.94 | relation(all_33_3) = 0 & $i(all_33_0) & $i(all_33_1) & $i(all_33_2) & % 23.74/3.94 | $i(all_33_3) & $i(all_33_4) % 23.74/3.94 | % 23.74/3.94 | ALPHA: (3) implies: % 23.74/3.94 | (4) ~ (all_33_0 = all_33_2) % 23.74/3.94 | (5) $i(all_33_4) % 23.74/3.94 | (6) $i(all_33_3) % 23.74/3.94 | (7) $i(all_33_2) % 23.74/3.94 | (8) $i(all_33_1) % 23.74/3.94 | (9) $i(all_33_0) % 23.74/3.94 | (10) relation(all_33_3) = 0 % 23.74/3.94 | (11) relation_dom_restriction(all_33_3, all_33_4) = all_33_2 % 23.74/3.94 | (12) relation_composition(all_33_1, all_33_3) = all_33_0 % 23.74/3.94 | (13) identity_relation(all_33_4) = all_33_1 % 23.74/3.94 | % 23.74/3.94 | GROUND_INST: instantiating (d11_relat_1) with all_33_3, simplifying with (6), % 23.74/3.94 | (10) gives: % 23.74/3.95 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 23.74/3.95 | (relation_dom_restriction(all_33_3, v0) = v2) | ~ (relation(v1) = % 23.74/3.95 | 0) | ~ $i(v1) | ~ $i(v0) | (( ~ (v2 = v1) | ( ! [v3: $i] : ! % 23.74/3.95 | [v4: $i] : ! [v5: $i] : ! [v6: any] : ( ~ (ordered_pair(v3, % 23.74/3.95 | v4) = v5) | ~ (in(v5, all_33_3) = v6) | ~ $i(v4) | ~ % 23.74/3.95 | $i(v3) | ? [v7: any] : ? [v8: any] : (in(v5, v1) = v7 & % 23.74/3.95 | in(v3, v0) = v8 & ( ~ (v7 = 0) | (v8 = 0 & v6 = 0)))) & ! % 23.74/3.95 | [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (ordered_pair(v3, % 23.74/3.95 | v4) = v5) | ~ (in(v5, all_33_3) = 0) | ~ $i(v4) | ~ % 23.74/3.95 | $i(v3) | ? [v6: any] : ? [v7: any] : (in(v5, v1) = v7 & % 23.74/3.95 | in(v3, v0) = v6 & ( ~ (v6 = 0) | v7 = 0))))) & (v2 = v1 | % 23.74/3.95 | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: any] : ? [v7: % 23.74/3.95 | any] : ? [v8: any] : (ordered_pair(v3, v4) = v5 & in(v5, v1) % 23.74/3.95 | = v6 & in(v5, all_33_3) = v8 & in(v3, v0) = v7 & $i(v5) & % 23.74/3.95 | $i(v4) & $i(v3) & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0)) & % 23.74/3.95 | (v6 = 0 | (v8 = 0 & v7 = 0)))))) % 23.74/3.95 | % 23.74/3.95 | GROUND_INST: instantiating (dt_k7_relat_1) with all_33_3, all_33_4, all_33_2, % 23.74/3.95 | simplifying with (5), (6), (11) gives: % 23.74/3.95 | (15) ? [v0: any] : ? [v1: any] : (relation(all_33_2) = v1 & % 23.74/3.95 | relation(all_33_3) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 23.74/3.95 | % 23.74/3.95 | GROUND_INST: instantiating (fc10_relat_1) with all_33_3, all_33_1, all_33_0, % 23.74/3.95 | simplifying with (6), (8), (12) gives: % 23.74/3.95 | (16) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 23.74/3.95 | (empty(all_33_0) = v2 & empty(all_33_3) = v0 & relation(all_33_0) = v3 % 23.74/3.95 | & relation(all_33_1) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v3 = 0 & % 23.74/3.95 | v2 = 0))) % 23.74/3.95 | % 23.74/3.95 | GROUND_INST: instantiating (fc9_relat_1) with all_33_1, all_33_3, all_33_0, % 23.74/3.95 | simplifying with (6), (8), (12) gives: % 23.74/3.95 | (17) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] : % 23.74/3.95 | (empty(all_33_0) = v2 & empty(all_33_1) = v0 & relation(all_33_0) = v3 % 23.74/3.95 | & relation(all_33_3) = v1 & ( ~ (v1 = 0) | ~ (v0 = 0) | (v3 = 0 & % 23.74/3.95 | v2 = 0))) % 23.74/3.95 | % 23.74/3.95 | GROUND_INST: instantiating (dt_k5_relat_1) with all_33_1, all_33_3, all_33_0, % 23.74/3.95 | simplifying with (6), (8), (12) gives: % 23.74/3.95 | (18) ? [v0: any] : ? [v1: any] : ? [v2: any] : (relation(all_33_0) = v2 % 23.74/3.95 | & relation(all_33_1) = v0 & relation(all_33_3) = v1 & ( ~ (v1 = 0) | % 23.74/3.95 | ~ (v0 = 0) | v2 = 0)) % 23.74/3.95 | % 23.74/3.95 | GROUND_INST: instantiating (dt_k6_relat_1) with all_33_4, all_33_1, % 23.74/3.95 | simplifying with (5), (13) gives: % 23.74/3.95 | (19) relation(all_33_1) = 0 % 23.74/3.95 | % 23.74/3.95 | DELTA: instantiating (15) with fresh symbols all_49_0, all_49_1 gives: % 23.74/3.95 | (20) relation(all_33_2) = all_49_0 & relation(all_33_3) = all_49_1 & ( ~ % 23.74/3.95 | (all_49_1 = 0) | all_49_0 = 0) % 23.74/3.95 | % 23.74/3.95 | ALPHA: (20) implies: % 23.74/3.95 | (21) relation(all_33_3) = all_49_1 % 23.74/3.95 | (22) relation(all_33_2) = all_49_0 % 23.74/3.95 | (23) ~ (all_49_1 = 0) | all_49_0 = 0 % 23.74/3.95 | % 23.74/3.95 | DELTA: instantiating (18) with fresh symbols all_51_0, all_51_1, all_51_2 % 23.74/3.95 | gives: % 23.74/3.95 | (24) relation(all_33_0) = all_51_0 & relation(all_33_1) = all_51_2 & % 23.74/3.95 | relation(all_33_3) = all_51_1 & ( ~ (all_51_1 = 0) | ~ (all_51_2 = 0) % 23.74/3.95 | | all_51_0 = 0) % 23.74/3.95 | % 23.74/3.95 | ALPHA: (24) implies: % 23.74/3.95 | (25) relation(all_33_3) = all_51_1 % 23.74/3.95 | (26) relation(all_33_1) = all_51_2 % 23.74/3.95 | (27) relation(all_33_0) = all_51_0 % 23.74/3.95 | (28) ~ (all_51_1 = 0) | ~ (all_51_2 = 0) | all_51_0 = 0 % 23.74/3.95 | % 23.74/3.95 | DELTA: instantiating (17) with fresh symbols all_53_0, all_53_1, all_53_2, % 23.74/3.95 | all_53_3 gives: % 23.74/3.95 | (29) empty(all_33_0) = all_53_1 & empty(all_33_1) = all_53_3 & % 23.74/3.95 | relation(all_33_0) = all_53_0 & relation(all_33_3) = all_53_2 & ( ~ % 23.74/3.95 | (all_53_2 = 0) | ~ (all_53_3 = 0) | (all_53_0 = 0 & all_53_1 = 0)) % 23.74/3.95 | % 23.74/3.95 | ALPHA: (29) implies: % 23.74/3.95 | (30) relation(all_33_3) = all_53_2 % 23.74/3.95 | (31) relation(all_33_0) = all_53_0 % 23.74/3.95 | % 23.74/3.95 | DELTA: instantiating (16) with fresh symbols all_55_0, all_55_1, all_55_2, % 23.74/3.95 | all_55_3 gives: % 23.74/3.95 | (32) empty(all_33_0) = all_55_1 & empty(all_33_3) = all_55_3 & % 23.74/3.95 | relation(all_33_0) = all_55_0 & relation(all_33_1) = all_55_2 & ( ~ % 23.74/3.95 | (all_55_2 = 0) | ~ (all_55_3 = 0) | (all_55_0 = 0 & all_55_1 = 0)) % 23.74/3.96 | % 23.74/3.96 | ALPHA: (32) implies: % 23.74/3.96 | (33) relation(all_33_1) = all_55_2 % 23.74/3.96 | (34) relation(all_33_0) = all_55_0 % 23.74/3.96 | % 23.74/3.96 | GROUND_INST: instantiating (1) with all_49_1, all_51_1, all_33_3, simplifying % 23.74/3.96 | with (21), (25) gives: % 23.74/3.96 | (35) all_51_1 = all_49_1 % 23.74/3.96 | % 23.74/3.96 | GROUND_INST: instantiating (1) with 0, all_53_2, all_33_3, simplifying with % 23.74/3.96 | (10), (30) gives: % 23.74/3.96 | (36) all_53_2 = 0 % 23.74/3.96 | % 23.74/3.96 | GROUND_INST: instantiating (1) with all_51_1, all_53_2, all_33_3, simplifying % 23.74/3.96 | with (25), (30) gives: % 23.74/3.96 | (37) all_53_2 = all_51_1 % 23.74/3.96 | % 23.74/3.96 | GROUND_INST: instantiating (1) with all_51_2, all_55_2, all_33_1, simplifying % 23.74/3.96 | with (26), (33) gives: % 23.74/3.96 | (38) all_55_2 = all_51_2 % 23.74/3.96 | % 23.74/3.96 | GROUND_INST: instantiating (1) with 0, all_55_2, all_33_1, simplifying with % 23.74/3.96 | (19), (33) gives: % 23.74/3.96 | (39) all_55_2 = 0 % 23.74/3.96 | % 23.74/3.96 | GROUND_INST: instantiating (1) with all_53_0, all_55_0, all_33_0, simplifying % 23.74/3.96 | with (31), (34) gives: % 23.74/3.96 | (40) all_55_0 = all_53_0 % 23.74/3.96 | % 23.74/3.96 | GROUND_INST: instantiating (1) with all_51_0, all_55_0, all_33_0, simplifying % 23.74/3.96 | with (27), (34) gives: % 23.74/3.96 | (41) all_55_0 = all_51_0 % 23.74/3.96 | % 23.74/3.96 | COMBINE_EQS: (40), (41) imply: % 23.74/3.96 | (42) all_53_0 = all_51_0 % 23.74/3.96 | % 23.74/3.96 | SIMP: (42) implies: % 23.74/3.96 | (43) all_53_0 = all_51_0 % 23.74/3.96 | % 23.74/3.96 | COMBINE_EQS: (38), (39) imply: % 23.74/3.96 | (44) all_51_2 = 0 % 23.74/3.96 | % 23.74/3.96 | SIMP: (44) implies: % 23.74/3.96 | (45) all_51_2 = 0 % 23.74/3.96 | % 23.74/3.96 | COMBINE_EQS: (36), (37) imply: % 23.74/3.96 | (46) all_51_1 = 0 % 23.74/3.96 | % 23.74/3.96 | SIMP: (46) implies: % 23.74/3.96 | (47) all_51_1 = 0 % 23.74/3.96 | % 23.74/3.96 | COMBINE_EQS: (35), (47) imply: % 23.74/3.96 | (48) all_49_1 = 0 % 23.74/3.96 | % 23.74/3.96 | BETA: splitting (28) gives: % 23.74/3.96 | % 23.74/3.96 | Case 1: % 23.74/3.96 | | % 23.74/3.96 | | (49) ~ (all_51_1 = 0) % 23.74/3.96 | | % 23.74/3.96 | | REDUCE: (47), (49) imply: % 23.74/3.96 | | (50) $false % 23.74/3.96 | | % 23.74/3.96 | | CLOSE: (50) is inconsistent. % 23.74/3.96 | | % 23.74/3.96 | Case 2: % 23.74/3.96 | | % 23.74/3.96 | | (51) ~ (all_51_2 = 0) | all_51_0 = 0 % 23.74/3.96 | | % 23.74/3.96 | | BETA: splitting (23) gives: % 23.74/3.96 | | % 23.74/3.96 | | Case 1: % 23.74/3.96 | | | % 23.74/3.96 | | | (52) ~ (all_49_1 = 0) % 23.74/3.96 | | | % 23.74/3.96 | | | REDUCE: (48), (52) imply: % 23.74/3.96 | | | (53) $false % 23.74/3.96 | | | % 23.74/3.96 | | | CLOSE: (53) is inconsistent. % 23.74/3.96 | | | % 23.74/3.96 | | Case 2: % 23.74/3.96 | | | % 23.74/3.96 | | | (54) all_49_0 = 0 % 23.74/3.96 | | | % 23.74/3.96 | | | REDUCE: (22), (54) imply: % 23.74/3.96 | | | (55) relation(all_33_2) = 0 % 23.74/3.96 | | | % 23.74/3.96 | | | BETA: splitting (51) gives: % 23.74/3.96 | | | % 23.74/3.96 | | | Case 1: % 23.74/3.96 | | | | % 23.74/3.96 | | | | (56) ~ (all_51_2 = 0) % 23.74/3.96 | | | | % 23.74/3.96 | | | | REDUCE: (45), (56) imply: % 23.74/3.96 | | | | (57) $false % 23.74/3.96 | | | | % 23.74/3.96 | | | | CLOSE: (57) is inconsistent. % 23.74/3.96 | | | | % 23.74/3.96 | | | Case 2: % 23.74/3.96 | | | | % 23.74/3.96 | | | | (58) all_51_0 = 0 % 23.74/3.96 | | | | % 23.74/3.96 | | | | REDUCE: (27), (58) imply: % 23.74/3.96 | | | | (59) relation(all_33_0) = 0 % 23.74/3.96 | | | | % 23.74/3.96 | | | | GROUND_INST: instantiating (14) with all_33_4, all_33_2, all_33_2, % 23.74/3.96 | | | | simplifying with (5), (7), (11), (55) gives: % 23.74/3.96 | | | | (60) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: any] : ( ~ % 23.74/3.96 | | | | (ordered_pair(v0, v1) = v2) | ~ (in(v2, all_33_3) = v3) | ~ % 23.74/3.96 | | | | $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : (in(v2, % 23.74/3.96 | | | | all_33_2) = v4 & in(v0, all_33_4) = v5 & ( ~ (v4 = 0) | % 23.74/3.96 | | | | (v5 = 0 & v3 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 23.74/3.96 | | | | $i] : ( ~ (ordered_pair(v0, v1) = v2) | ~ (in(v2, all_33_3) = % 23.74/3.96 | | | | 0) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : % 23.74/3.96 | | | | (in(v2, all_33_2) = v4 & in(v0, all_33_4) = v3 & ( ~ (v3 = 0) % 23.74/3.96 | | | | | v4 = 0))) % 23.74/3.96 | | | | % 23.74/3.96 | | | | ALPHA: (60) implies: % 23.74/3.97 | | | | (61) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: any] : ( ~ % 23.74/3.97 | | | | (ordered_pair(v0, v1) = v2) | ~ (in(v2, all_33_3) = v3) | ~ % 23.74/3.97 | | | | $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : (in(v2, % 23.74/3.97 | | | | all_33_2) = v4 & in(v0, all_33_4) = v5 & ( ~ (v4 = 0) | % 23.74/3.97 | | | | (v5 = 0 & v3 = 0)))) % 23.74/3.97 | | | | % 23.74/3.97 | | | | GROUND_INST: instantiating (14) with all_33_4, all_33_0, all_33_2, % 23.74/3.97 | | | | simplifying with (5), (9), (11), (59) gives: % 23.74/3.97 | | | | (62) ( ~ (all_33_0 = all_33_2) | ( ! [v0: $i] : ! [v1: $i] : ! [v2: % 23.74/3.97 | | | | $i] : ! [v3: any] : ( ~ (ordered_pair(v0, v1) = v2) | ~ % 23.74/3.97 | | | | (in(v2, all_33_3) = v3) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 23.74/3.97 | | | | any] : ? [v5: any] : (in(v2, all_33_2) = v4 & in(v0, % 23.74/3.97 | | | | all_33_4) = v5 & ( ~ (v4 = 0) | (v5 = 0 & v3 = 0)))) & % 23.74/3.97 | | | | ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 23.74/3.97 | | | | (ordered_pair(v0, v1) = v2) | ~ (in(v2, all_33_3) = 0) | % 23.74/3.97 | | | | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : % 23.74/3.97 | | | | (in(v2, all_33_2) = v4 & in(v0, all_33_4) = v3 & ( ~ (v3 = % 23.74/3.97 | | | | 0) | v4 = 0))))) & (all_33_0 = all_33_2 | ? [v0: % 23.74/3.97 | | | | $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: any] : ? [v4: % 23.74/3.97 | | | | any] : ? [v5: any] : (ordered_pair(v0, v1) = v2 & in(v2, % 23.74/3.97 | | | | all_33_0) = v3 & in(v2, all_33_3) = v5 & in(v0, all_33_4) % 23.74/3.97 | | | | = v4 & $i(v2) & $i(v1) & $i(v0) & ( ~ (v5 = 0) | ~ (v4 = 0) % 23.74/3.97 | | | | | ~ (v3 = 0)) & (v3 = 0 | (v5 = 0 & v4 = 0)))) % 23.74/3.97 | | | | % 23.74/3.97 | | | | ALPHA: (62) implies: % 23.74/3.97 | | | | (63) all_33_0 = all_33_2 | ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 23.74/3.97 | | | | ? [v3: any] : ? [v4: any] : ? [v5: any] : (ordered_pair(v0, % 23.74/3.97 | | | | v1) = v2 & in(v2, all_33_0) = v3 & in(v2, all_33_3) = v5 & % 23.74/3.97 | | | | in(v0, all_33_4) = v4 & $i(v2) & $i(v1) & $i(v0) & ( ~ (v5 = % 23.74/3.97 | | | | 0) | ~ (v4 = 0) | ~ (v3 = 0)) & (v3 = 0 | (v5 = 0 & v4 = % 23.74/3.97 | | | | 0))) % 23.74/3.97 | | | | % 23.74/3.97 | | | | BETA: splitting (63) gives: % 23.74/3.97 | | | | % 23.74/3.97 | | | | Case 1: % 23.74/3.97 | | | | | % 23.74/3.97 | | | | | (64) all_33_0 = all_33_2 % 23.74/3.97 | | | | | % 23.74/3.97 | | | | | REDUCE: (4), (64) imply: % 23.74/3.97 | | | | | (65) $false % 23.74/3.97 | | | | | % 23.74/3.97 | | | | | CLOSE: (65) is inconsistent. % 23.74/3.97 | | | | | % 23.74/3.97 | | | | Case 2: % 23.74/3.97 | | | | | % 23.74/3.97 | | | | | (66) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: any] : ? % 23.74/3.97 | | | | | [v4: any] : ? [v5: any] : (ordered_pair(v0, v1) = v2 & in(v2, % 23.74/3.97 | | | | | all_33_0) = v3 & in(v2, all_33_3) = v5 & in(v0, all_33_4) % 23.74/3.97 | | | | | = v4 & $i(v2) & $i(v1) & $i(v0) & ( ~ (v5 = 0) | ~ (v4 = 0) % 23.74/3.97 | | | | | | ~ (v3 = 0)) & (v3 = 0 | (v5 = 0 & v4 = 0))) % 23.74/3.97 | | | | | % 23.74/3.97 | | | | | DELTA: instantiating (66) with fresh symbols all_93_0, all_93_1, % 23.74/3.97 | | | | | all_93_2, all_93_3, all_93_4, all_93_5 gives: % 23.74/3.97 | | | | | (67) ordered_pair(all_93_5, all_93_4) = all_93_3 & in(all_93_3, % 23.74/3.97 | | | | | all_33_0) = all_93_2 & in(all_93_3, all_33_3) = all_93_0 & % 23.74/3.97 | | | | | in(all_93_5, all_33_4) = all_93_1 & $i(all_93_3) & % 23.74/3.97 | | | | | $i(all_93_4) & $i(all_93_5) & ( ~ (all_93_0 = 0) | ~ % 23.74/3.97 | | | | | (all_93_1 = 0) | ~ (all_93_2 = 0)) & (all_93_2 = 0 | % 23.74/3.97 | | | | | (all_93_0 = 0 & all_93_1 = 0)) % 23.74/3.97 | | | | | % 23.74/3.97 | | | | | ALPHA: (67) implies: % 23.74/3.97 | | | | | (68) $i(all_93_5) % 23.74/3.97 | | | | | (69) $i(all_93_4) % 23.74/3.98 | | | | | (70) in(all_93_5, all_33_4) = all_93_1 % 23.74/3.98 | | | | | (71) in(all_93_3, all_33_3) = all_93_0 % 23.74/3.98 | | | | | (72) in(all_93_3, all_33_0) = all_93_2 % 23.74/3.98 | | | | | (73) ordered_pair(all_93_5, all_93_4) = all_93_3 % 23.74/3.98 | | | | | (74) all_93_2 = 0 | (all_93_0 = 0 & all_93_1 = 0) % 23.74/3.98 | | | | | (75) ~ (all_93_0 = 0) | ~ (all_93_1 = 0) | ~ (all_93_2 = 0) % 23.74/3.98 | | | | | % 23.74/3.98 | | | | | GROUND_INST: instantiating (t74_relat_1) with all_93_5, all_93_4, % 23.74/3.98 | | | | | all_33_4, all_33_3, all_93_3, all_33_1, all_33_0, % 23.74/3.98 | | | | | all_93_2, simplifying with (5), (6), (12), (13), (68), % 23.74/3.98 | | | | | (69), (72), (73) gives: % 23.74/3.98 | | | | | (76) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 23.74/3.98 | | | | | (relation(all_33_3) = v0 & in(all_93_3, all_33_3) = v2 & % 23.74/3.98 | | | | | in(all_93_5, all_33_4) = v1 & ( ~ (v0 = 0) | (( ~ (v2 = 0) | % 23.74/3.98 | | | | | ~ (v1 = 0) | all_93_2 = 0) & ( ~ (all_93_2 = 0) | (v2 % 23.74/3.98 | | | | | = 0 & v1 = 0))))) % 23.74/3.98 | | | | | % 23.74/3.98 | | | | | GROUND_INST: instantiating (61) with all_93_5, all_93_4, all_93_3, % 23.74/3.98 | | | | | all_93_0, simplifying with (68), (69), (71), (73) gives: % 23.74/3.98 | | | | | (77) ? [v0: any] : ? [v1: any] : (in(all_93_3, all_33_2) = v0 & % 23.74/3.98 | | | | | in(all_93_5, all_33_4) = v1 & ( ~ (v0 = 0) | (v1 = 0 & % 23.74/3.98 | | | | | all_93_0 = 0))) % 23.74/3.98 | | | | | % 23.74/3.98 | | | | | DELTA: instantiating (77) with fresh symbols all_111_0, all_111_1 % 23.74/3.98 | | | | | gives: % 23.74/3.98 | | | | | (78) in(all_93_3, all_33_2) = all_111_1 & in(all_93_5, all_33_4) = % 23.74/3.98 | | | | | all_111_0 & ( ~ (all_111_1 = 0) | (all_111_0 = 0 & all_93_0 = % 23.74/3.98 | | | | | 0)) % 23.74/3.98 | | | | | % 23.74/3.98 | | | | | ALPHA: (78) implies: % 23.74/3.98 | | | | | (79) in(all_93_5, all_33_4) = all_111_0 % 23.74/3.98 | | | | | % 23.74/3.98 | | | | | DELTA: instantiating (76) with fresh symbols all_117_0, all_117_1, % 23.74/3.98 | | | | | all_117_2 gives: % 23.74/3.98 | | | | | (80) relation(all_33_3) = all_117_2 & in(all_93_3, all_33_3) = % 23.74/3.98 | | | | | all_117_0 & in(all_93_5, all_33_4) = all_117_1 & ( ~ % 23.74/3.98 | | | | | (all_117_2 = 0) | (( ~ (all_117_0 = 0) | ~ (all_117_1 = 0) % 23.74/3.98 | | | | | | all_93_2 = 0) & ( ~ (all_93_2 = 0) | (all_117_0 = 0 & % 23.74/3.98 | | | | | all_117_1 = 0)))) % 23.74/3.98 | | | | | % 23.74/3.98 | | | | | ALPHA: (80) implies: % 23.74/3.98 | | | | | (81) in(all_93_5, all_33_4) = all_117_1 % 23.74/3.98 | | | | | (82) in(all_93_3, all_33_3) = all_117_0 % 23.74/3.98 | | | | | (83) relation(all_33_3) = all_117_2 % 23.74/3.98 | | | | | (84) ~ (all_117_2 = 0) | (( ~ (all_117_0 = 0) | ~ (all_117_1 = 0) % 23.74/3.98 | | | | | | all_93_2 = 0) & ( ~ (all_93_2 = 0) | (all_117_0 = 0 & % 23.74/3.98 | | | | | all_117_1 = 0))) % 23.74/3.98 | | | | | % 23.74/3.98 | | | | | GROUND_INST: instantiating (2) with all_93_1, all_117_1, all_33_4, % 23.74/3.98 | | | | | all_93_5, simplifying with (70), (81) gives: % 23.74/3.98 | | | | | (85) all_117_1 = all_93_1 % 23.74/3.98 | | | | | % 23.74/3.98 | | | | | GROUND_INST: instantiating (2) with all_111_0, all_117_1, all_33_4, % 23.74/3.98 | | | | | all_93_5, simplifying with (79), (81) gives: % 23.74/3.98 | | | | | (86) all_117_1 = all_111_0 % 23.74/3.98 | | | | | % 23.74/3.98 | | | | | GROUND_INST: instantiating (2) with all_93_0, all_117_0, all_33_3, % 23.74/3.98 | | | | | all_93_3, simplifying with (71), (82) gives: % 23.74/3.98 | | | | | (87) all_117_0 = all_93_0 % 23.74/3.98 | | | | | % 23.74/3.98 | | | | | GROUND_INST: instantiating (1) with 0, all_117_2, all_33_3, % 23.74/3.98 | | | | | simplifying with (10), (83) gives: % 23.74/3.98 | | | | | (88) all_117_2 = 0 % 23.74/3.98 | | | | | % 23.74/3.98 | | | | | COMBINE_EQS: (85), (86) imply: % 23.74/3.98 | | | | | (89) all_111_0 = all_93_1 % 23.74/3.98 | | | | | % 23.74/3.98 | | | | | BETA: splitting (74) gives: % 23.74/3.98 | | | | | % 23.74/3.98 | | | | | Case 1: % 23.74/3.98 | | | | | | % 23.74/3.98 | | | | | | (90) all_93_2 = 0 % 23.74/3.98 | | | | | | % 23.74/3.98 | | | | | | BETA: splitting (84) gives: % 23.74/3.98 | | | | | | % 23.74/3.98 | | | | | | Case 1: % 23.74/3.98 | | | | | | | % 23.74/3.99 | | | | | | | (91) ~ (all_117_2 = 0) % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | | REDUCE: (88), (91) imply: % 23.74/3.99 | | | | | | | (92) $false % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | | CLOSE: (92) is inconsistent. % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | Case 2: % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | | (93) ( ~ (all_117_0 = 0) | ~ (all_117_1 = 0) | all_93_2 = 0) & % 23.74/3.99 | | | | | | | ( ~ (all_93_2 = 0) | (all_117_0 = 0 & all_117_1 = 0)) % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | | ALPHA: (93) implies: % 23.74/3.99 | | | | | | | (94) ~ (all_93_2 = 0) | (all_117_0 = 0 & all_117_1 = 0) % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | | REF_CLOSE: (75), (85), (87), (90), (94) are inconsistent by % 23.74/3.99 | | | | | | | sub-proof #1. % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | End of split % 23.74/3.99 | | | | | | % 23.74/3.99 | | | | | Case 2: % 23.74/3.99 | | | | | | % 23.74/3.99 | | | | | | (95) all_93_0 = 0 & all_93_1 = 0 % 23.74/3.99 | | | | | | % 23.74/3.99 | | | | | | ALPHA: (95) implies: % 23.74/3.99 | | | | | | (96) all_93_1 = 0 % 23.74/3.99 | | | | | | (97) all_93_0 = 0 % 23.74/3.99 | | | | | | % 23.74/3.99 | | | | | | COMBINE_EQS: (85), (96) imply: % 23.74/3.99 | | | | | | (98) all_117_1 = 0 % 23.74/3.99 | | | | | | % 23.74/3.99 | | | | | | COMBINE_EQS: (87), (97) imply: % 23.74/3.99 | | | | | | (99) all_117_0 = 0 % 23.74/3.99 | | | | | | % 23.74/3.99 | | | | | | BETA: splitting (84) gives: % 23.74/3.99 | | | | | | % 23.74/3.99 | | | | | | Case 1: % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | | (100) ~ (all_117_2 = 0) % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | | REDUCE: (88), (100) imply: % 23.74/3.99 | | | | | | | (101) $false % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | | CLOSE: (101) is inconsistent. % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | Case 2: % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | | (102) ( ~ (all_117_0 = 0) | ~ (all_117_1 = 0) | all_93_2 = 0) % 23.74/3.99 | | | | | | | & ( ~ (all_93_2 = 0) | (all_117_0 = 0 & all_117_1 = 0)) % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | | ALPHA: (102) implies: % 23.74/3.99 | | | | | | | (103) ~ (all_93_2 = 0) | (all_117_0 = 0 & all_117_1 = 0) % 23.74/3.99 | | | | | | | (104) ~ (all_117_0 = 0) | ~ (all_117_1 = 0) | all_93_2 = 0 % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | | BETA: splitting (104) gives: % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | | Case 1: % 23.74/3.99 | | | | | | | | % 23.74/3.99 | | | | | | | | (105) ~ (all_117_0 = 0) % 23.74/3.99 | | | | | | | | % 23.74/3.99 | | | | | | | | REDUCE: (99), (105) imply: % 23.74/3.99 | | | | | | | | (106) $false % 23.74/3.99 | | | | | | | | % 23.74/3.99 | | | | | | | | CLOSE: (106) is inconsistent. % 23.74/3.99 | | | | | | | | % 23.74/3.99 | | | | | | | Case 2: % 23.74/3.99 | | | | | | | | % 23.74/3.99 | | | | | | | | (107) ~ (all_117_1 = 0) | all_93_2 = 0 % 23.74/3.99 | | | | | | | | % 23.74/3.99 | | | | | | | | BETA: splitting (107) gives: % 23.74/3.99 | | | | | | | | % 23.74/3.99 | | | | | | | | Case 1: % 23.74/3.99 | | | | | | | | | % 23.74/3.99 | | | | | | | | | (108) ~ (all_117_1 = 0) % 23.74/3.99 | | | | | | | | | % 23.74/3.99 | | | | | | | | | REDUCE: (98), (108) imply: % 23.74/3.99 | | | | | | | | | (109) $false % 23.74/3.99 | | | | | | | | | % 23.74/3.99 | | | | | | | | | CLOSE: (109) is inconsistent. % 23.74/3.99 | | | | | | | | | % 23.74/3.99 | | | | | | | | Case 2: % 23.74/3.99 | | | | | | | | | % 23.74/3.99 | | | | | | | | | (110) all_93_2 = 0 % 23.74/3.99 | | | | | | | | | % 23.74/3.99 | | | | | | | | | REF_CLOSE: (75), (85), (87), (103), (110) are inconsistent by % 23.74/3.99 | | | | | | | | | sub-proof #1. % 23.74/3.99 | | | | | | | | | % 23.74/3.99 | | | | | | | | End of split % 23.74/3.99 | | | | | | | | % 23.74/3.99 | | | | | | | End of split % 23.74/3.99 | | | | | | | % 23.74/3.99 | | | | | | End of split % 23.74/3.99 | | | | | | % 23.74/3.99 | | | | | End of split % 23.74/3.99 | | | | | % 23.74/3.99 | | | | End of split % 23.74/3.99 | | | | % 23.74/3.99 | | | End of split % 23.74/3.99 | | | % 23.74/3.99 | | End of split % 23.74/3.99 | | % 23.74/3.99 | End of split % 23.74/3.99 | % 23.74/3.99 End of proof % 23.74/3.99 % 23.74/3.99 Sub-proof #1 shows that the following formulas are inconsistent: % 23.74/3.99 ---------------------------------------------------------------- % 23.74/3.99 (1) all_117_1 = all_93_1 % 23.74/3.99 (2) ~ (all_93_0 = 0) | ~ (all_93_1 = 0) | ~ (all_93_2 = 0) % 23.74/3.99 (3) all_93_2 = 0 % 23.74/3.99 (4) ~ (all_93_2 = 0) | (all_117_0 = 0 & all_117_1 = 0) % 23.74/3.99 (5) all_117_0 = all_93_0 % 23.74/3.99 % 23.74/3.99 Begin of proof % 23.74/3.99 | % 23.74/3.99 | BETA: splitting (4) gives: % 23.74/3.99 | % 23.74/3.99 | Case 1: % 23.74/3.99 | | % 23.74/3.99 | | (6) ~ (all_93_2 = 0) % 23.74/3.99 | | % 23.74/3.99 | | REDUCE: (3), (6) imply: % 23.74/3.99 | | (7) $false % 23.74/3.99 | | % 23.74/3.99 | | CLOSE: (7) is inconsistent. % 23.74/3.99 | | % 23.74/3.99 | Case 2: % 23.74/3.99 | | % 23.74/3.99 | | (8) all_117_0 = 0 & all_117_1 = 0 % 23.74/3.99 | | % 23.74/3.99 | | ALPHA: (8) implies: % 23.74/3.99 | | (9) all_117_1 = 0 % 23.74/3.99 | | (10) all_117_0 = 0 % 23.74/3.99 | | % 23.74/3.99 | | COMBINE_EQS: (5), (10) imply: % 23.74/3.99 | | (11) all_93_0 = 0 % 23.74/3.99 | | % 23.74/3.99 | | COMBINE_EQS: (1), (9) imply: % 23.74/3.99 | | (12) all_93_1 = 0 % 23.74/3.99 | | % 23.74/3.99 | | SIMP: (12) implies: % 23.74/3.99 | | (13) all_93_1 = 0 % 23.74/3.99 | | % 23.74/3.99 | | BETA: splitting (2) gives: % 23.74/3.99 | | % 23.74/3.99 | | Case 1: % 23.74/3.99 | | | % 23.74/3.99 | | | (14) ~ (all_93_0 = 0) % 23.74/3.99 | | | % 23.74/3.99 | | | REDUCE: (11), (14) imply: % 23.74/3.99 | | | (15) $false % 23.74/3.99 | | | % 23.74/3.99 | | | CLOSE: (15) is inconsistent. % 23.74/3.99 | | | % 23.74/3.99 | | Case 2: % 23.74/3.99 | | | % 23.74/3.99 | | | (16) ~ (all_93_1 = 0) | ~ (all_93_2 = 0) % 23.74/3.99 | | | % 23.74/3.99 | | | BETA: splitting (16) gives: % 23.74/3.99 | | | % 23.74/3.99 | | | Case 1: % 23.74/3.99 | | | | % 23.74/3.99 | | | | (17) ~ (all_93_1 = 0) % 23.74/3.99 | | | | % 23.74/3.99 | | | | REDUCE: (13), (17) imply: % 23.74/3.99 | | | | (18) $false % 23.74/3.99 | | | | % 23.74/3.99 | | | | CLOSE: (18) is inconsistent. % 23.74/3.99 | | | | % 23.74/3.99 | | | Case 2: % 23.74/3.99 | | | | % 23.74/3.99 | | | | (19) ~ (all_93_2 = 0) % 23.74/3.99 | | | | % 23.74/3.99 | | | | REDUCE: (3), (19) imply: % 23.74/3.99 | | | | (20) $false % 23.74/3.99 | | | | % 23.74/3.99 | | | | CLOSE: (20) is inconsistent. % 23.74/3.99 | | | | % 23.74/3.99 | | | End of split % 23.74/3.99 | | | % 23.74/3.99 | | End of split % 23.74/3.99 | | % 23.74/3.99 | End of split % 23.74/3.99 | % 23.74/3.99 End of proof % 23.74/3.99 % SZS output end Proof for theBenchmark % 23.74/3.99 % 23.74/3.99 3345ms %------------------------------------------------------------------------------