%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : GEO526+1 : TPTP v8.1.2. Released v7.0.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 : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Aug 30 23:23:36 EDT 2023 % Result : Theorem 89.58s 12.66s % Output : Proof 91.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : GEO526+1 : TPTP v8.1.2. Released v7.0.0. % 0.00/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.11/0.33 % Computer : n008.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Tue Aug 29 22:29:32 EDT 2023 % 0.11/0.33 % CPUTime : % 0.19/0.59 ________ _____ % 0.19/0.59 ___ __ \_________(_)________________________________ % 0.19/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.59 % 0.19/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.59 (2023-06-19) % 0.19/0.59 % 0.19/0.59 (c) Philipp Rümmer, 2009-2023 % 0.19/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.59 Amanda Stjerna. % 0.19/0.59 Free software under BSD-3-Clause. % 0.19/0.59 % 0.19/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.59 % 0.19/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.60 Running up to 7 provers in parallel. % 0.19/0.61 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.61 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.61 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.61 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.61 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.61 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.61 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 8.93/1.94 Prover 4: Preprocessing ... % 9.46/1.95 Prover 1: Preprocessing ... % 9.46/1.95 Prover 3: Preprocessing ... % 9.46/1.95 Prover 0: Preprocessing ... % 9.46/1.95 Prover 2: Preprocessing ... % 9.46/1.95 Prover 5: Preprocessing ... % 9.46/1.95 Prover 6: Preprocessing ... % 20.53/3.48 Prover 1: Warning: ignoring some quantifiers % 20.53/3.49 Prover 5: Proving ... % 20.53/3.59 Prover 2: Proving ... % 20.53/3.67 Prover 6: Proving ... % 21.37/3.68 Prover 3: Warning: ignoring some quantifiers % 21.37/3.71 Prover 1: Constructing countermodel ... % 22.38/3.76 Prover 3: Constructing countermodel ... % 29.29/4.68 Prover 4: Constructing countermodel ... % 29.29/4.68 Prover 0: Proving ... % 73.71/10.52 Prover 2: stopped % 73.71/10.54 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 76.13/10.84 Prover 7: Preprocessing ... % 78.10/11.05 Prover 7: Warning: ignoring some quantifiers % 78.10/11.08 Prover 7: Constructing countermodel ... % 89.58/12.63 Prover 4: Found proof (size 351) % 89.58/12.64 Prover 4: proved (12033ms) % 89.58/12.64 Prover 3: stopped % 89.58/12.64 Prover 0: stopped % 89.58/12.64 Prover 5: stopped % 89.58/12.64 Prover 1: stopped % 89.58/12.65 Prover 6: stopped % 89.58/12.65 Prover 7: stopped % 89.58/12.65 % 89.58/12.66 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 89.58/12.66 % 89.58/12.70 % SZS output start Proof for theBenchmark % 89.58/12.71 Assumptions after simplification: % 89.58/12.71 --------------------------------- % 89.58/12.71 % 89.58/12.71 (aA2) % 90.29/12.74 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 90.29/12.74 $i] : ! [v6: int] : (v6 = 0 | ~ (s_e(v2, v3, v4, v5) = v6) | ~ (s_e(v0, % 90.29/12.74 v1, v4, v5) = 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 90.29/12.74 $i(v1) | ~ $i(v0) | ? [v7: int] : ( ~ (v7 = 0) & s_e(v0, v1, v2, v3) = % 90.29/12.74 v7)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 90.29/12.74 : ! [v5: $i] : ! [v6: int] : (v6 = 0 | ~ (s_e(v2, v3, v4, v5) = v6) | ~ % 90.29/12.74 (s_e(v0, v1, v2, v3) = 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 90.29/12.74 ~ $i(v1) | ~ $i(v0) | ? [v7: int] : ( ~ (v7 = 0) & s_e(v0, v1, v4, v5) = % 90.29/12.74 v7)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 90.29/12.74 : ! [v5: $i] : ( ~ (s_e(v0, v1, v4, v5) = 0) | ~ (s_e(v0, v1, v2, v3) = 0) | % 90.29/12.74 ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 90.29/12.74 s_e(v2, v3, v4, v5) = 0) % 90.29/12.74 % 90.29/12.74 (aA8) % 90.29/12.74 $i(gamma) & $i(beta) & $i(alpha) & ? [v0: int] : ? [v1: int] : ? [v2: int] % 90.29/12.74 : ( ~ (v2 = 0) & ~ (v1 = 0) & ~ (v0 = 0) & s_t(gamma, alpha, beta) = v2 & % 90.29/12.74 s_t(beta, gamma, alpha) = v1 & s_t(alpha, beta, gamma) = v0) % 90.29/12.74 % 90.29/12.74 (aSatz10_12b) % 90.29/12.75 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 90.29/12.75 | ~ (s_r(v3, v1, v2) = 0) | ~ (s_e(v0, v2, v3, v2) = v4) | ~ $i(v3) | ~ % 90.29/12.75 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : (s_r(v0, v1, % 90.29/12.75 v2) = v5 & s_e(v0, v1, v3, v1) = v6 & ( ~ (v6 = 0) | ~ (v5 = 0)))) & ! % 90.29/12.75 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | % 90.29/12.75 ~ (s_r(v0, v1, v2) = 0) | ~ (s_e(v0, v2, v3, v2) = v4) | ~ $i(v3) | ~ % 90.29/12.75 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : (s_r(v3, v1, % 90.29/12.75 v2) = v5 & s_e(v0, v1, v3, v1) = v6 & ( ~ (v6 = 0) | ~ (v5 = 0)))) & ! % 90.29/12.75 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | % 90.29/12.75 ~ (s_e(v0, v2, v3, v2) = v4) | ~ (s_e(v0, v1, v3, v1) = 0) | ~ $i(v3) | ~ % 90.29/12.75 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : (s_r(v3, v1, % 90.29/12.75 v2) = v6 & s_r(v0, v1, v2) = v5 & ( ~ (v6 = 0) | ~ (v5 = 0)))) & ! % 90.29/12.75 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (s_r(v3, v1, v2) = 0) % 90.29/12.75 | ~ (s_r(v0, v1, v2) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 90.29/12.75 ? [v4: any] : ? [v5: any] : (s_e(v0, v2, v3, v2) = v5 & s_e(v0, v1, v3, % 90.29/12.75 v1) = v4 & ( ~ (v4 = 0) | v5 = 0))) & ! [v0: $i] : ! [v1: $i] : ! % 90.29/12.75 [v2: $i] : ! [v3: $i] : ( ~ (s_r(v3, v1, v2) = 0) | ~ (s_e(v0, v1, v3, v1) = % 90.29/12.75 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? % 90.29/12.75 [v5: any] : (s_r(v0, v1, v2) = v4 & s_e(v0, v2, v3, v2) = v5 & ( ~ (v4 = 0) % 90.29/12.75 | v5 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( % 90.29/12.75 ~ (s_r(v0, v1, v2) = 0) | ~ (s_e(v0, v1, v3, v1) = 0) | ~ $i(v3) | ~ % 90.29/12.75 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : (s_r(v3, v1, % 90.29/12.75 v2) = v4 & s_e(v0, v2, v3, v2) = v5 & ( ~ (v4 = 0) | v5 = 0))) % 90.29/12.75 % 90.29/12.75 (aSatz10_12c) % 90.29/12.75 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 90.29/12.75 int] : ( ~ (v5 = 0) & ~ (v4 = v2) & midpoint(v2, v4) = v1 & s_r(v3, v1, v4) % 90.29/12.75 = 0 & s_r(v0, v1, v2) = 0 & s_e(v1, v2, v1, v4) = 0 & s_e(v0, v2, v3, v4) = % 90.29/12.75 v5 & s_e(v0, v1, v3, v1) = 0 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 90.29/12.75 % 90.29/12.75 (aSatz2_11) % 90.29/12.76 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 90.29/12.76 $i] : ! [v6: int] : (v6 = 0 | ~ (s_e(v1, v2, v4, v5) = 0) | ~ (s_e(v0, % 90.29/12.76 v2, v3, v5) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 90.29/12.76 $i(v1) | ~ $i(v0) | ? [v7: any] : ? [v8: any] : ? [v9: any] : (s_t(v3, % 90.29/12.76 v4, v5) = v8 & s_t(v0, v1, v2) = v7 & s_e(v0, v1, v3, v4) = v9 & ( ~ (v9 % 90.29/12.76 = 0) | ~ (v8 = 0) | ~ (v7 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 90.29/12.76 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: int] : (v6 = 0 | % 90.29/12.76 ~ (s_e(v0, v2, v3, v5) = v6) | ~ (s_e(v0, v1, v3, v4) = 0) | ~ $i(v5) | ~ % 90.29/12.76 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v7: any] : ? % 90.29/12.76 [v8: any] : ? [v9: any] : (s_t(v3, v4, v5) = v8 & s_t(v0, v1, v2) = v7 & % 90.29/12.76 s_e(v1, v2, v4, v5) = v9 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0)))) & % 90.29/12.76 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 90.29/12.76 $i] : ( ~ (s_t(v3, v4, v5) = 0) | ~ (s_t(v0, v1, v2) = 0) | ~ $i(v5) | ~ % 90.29/12.76 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? % 90.29/12.76 [v7: any] : ? [v8: any] : (s_e(v1, v2, v4, v5) = v7 & s_e(v0, v2, v3, v5) = % 90.29/12.76 v8 & s_e(v0, v1, v3, v4) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0) | v8 = 0))) & % 90.29/12.76 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 90.29/12.76 $i] : ( ~ (s_e(v1, v2, v4, v5) = 0) | ~ (s_e(v0, v1, v3, v4) = 0) | ~ % 90.29/12.76 $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: % 90.29/12.76 any] : ? [v7: any] : ? [v8: any] : (s_t(v3, v4, v5) = v7 & s_t(v0, v1, % 90.29/12.76 v2) = v6 & s_e(v0, v2, v3, v5) = v8 & ( ~ (v7 = 0) | ~ (v6 = 0) | v8 = % 90.29/12.76 0))) % 90.29/12.76 % 90.29/12.76 (aSatz2_14) % 90.29/12.76 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 90.29/12.76 | ~ (s_e(v1, v0, v3, v2) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 90.29/12.76 $i(v0) | ? [v5: int] : ( ~ (v5 = 0) & s_e(v0, v1, v2, v3) = v5)) & ! [v0: % 90.29/12.76 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (s_e(v0, v1, v2, v3) = % 90.29/12.76 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | s_e(v1, v0, v3, v2) = % 90.29/12.76 0) % 90.29/12.76 % 90.29/12.76 (aSatz2_2) % 90.29/12.76 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 90.29/12.76 | ~ (s_e(v2, v3, v0, v1) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 90.29/12.76 $i(v0) | ? [v5: int] : ( ~ (v5 = 0) & s_e(v0, v1, v2, v3) = v5)) & ! [v0: % 90.29/12.76 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (s_e(v0, v1, v2, v3) = % 90.29/12.76 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | s_e(v2, v3, v0, v1) = % 90.29/12.76 0) % 90.29/12.76 % 90.29/12.76 (aSatz2_3) % 90.29/12.76 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 90.29/12.76 $i] : ! [v6: int] : (v6 = 0 | ~ (s_e(v2, v3, v4, v5) = 0) | ~ (s_e(v0, % 90.29/12.76 v1, v4, v5) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 90.29/12.76 $i(v1) | ~ $i(v0) | ? [v7: int] : ( ~ (v7 = 0) & s_e(v0, v1, v2, v3) = % 90.29/12.76 v7)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 90.29/12.76 : ! [v5: $i] : ! [v6: int] : (v6 = 0 | ~ (s_e(v0, v1, v4, v5) = v6) | ~ % 90.29/12.76 (s_e(v0, v1, v2, v3) = 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 90.29/12.76 ~ $i(v1) | ~ $i(v0) | ? [v7: int] : ( ~ (v7 = 0) & s_e(v2, v3, v4, v5) = % 90.29/12.76 v7)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 90.29/12.76 : ! [v5: $i] : ( ~ (s_e(v2, v3, v4, v5) = 0) | ~ (s_e(v0, v1, v2, v3) = 0) | % 90.29/12.76 ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 90.29/12.76 s_e(v0, v1, v4, v5) = 0) % 90.29/12.76 % 90.29/12.76 (aSatz3_13b) % 90.29/12.76 ~ (gamma = beta) & $i(gamma) & $i(beta) % 90.29/12.76 % 90.29/12.76 (aSatz3_2) % 90.29/12.77 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_t(v2, % 90.29/12.77 v1, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ % 90.29/12.77 (v4 = 0) & s_t(v0, v1, v2) = v4)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 90.29/12.77 $i] : ( ~ (s_t(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 90.29/12.77 s_t(v2, v1, v0) = 0) % 90.29/12.77 % 90.29/12.77 (aSatz3_3) % 90.29/12.77 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (s_t(v0, v0, v1) = v2) % 90.29/12.77 | ~ $i(v1) | ~ $i(v0)) % 90.29/12.77 % 90.29/12.77 (aSatz4_3) % 90.29/12.77 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 90.29/12.77 $i] : ! [v6: int] : (v6 = 0 | ~ (s_e(v1, v2, v4, v5) = 0) | ~ (s_e(v0, % 90.29/12.77 v1, v3, v4) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 90.29/12.77 $i(v1) | ~ $i(v0) | ? [v7: any] : ? [v8: any] : ? [v9: any] : (s_t(v3, % 90.29/12.77 v4, v5) = v8 & s_t(v0, v1, v2) = v7 & s_e(v0, v2, v3, v5) = v9 & ( ~ (v9 % 90.29/12.77 = 0) | ~ (v8 = 0) | ~ (v7 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! % 90.29/12.77 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: int] : (v6 = 0 | % 90.29/12.77 ~ (s_e(v0, v2, v3, v5) = 0) | ~ (s_e(v0, v1, v3, v4) = v6) | ~ $i(v5) | ~ % 90.29/12.77 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v7: any] : ? % 90.29/12.77 [v8: any] : ? [v9: any] : (s_t(v3, v4, v5) = v8 & s_t(v0, v1, v2) = v7 & % 90.29/12.77 s_e(v1, v2, v4, v5) = v9 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0)))) & % 90.29/12.77 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 90.29/12.77 $i] : ( ~ (s_t(v3, v4, v5) = 0) | ~ (s_t(v0, v1, v2) = 0) | ~ $i(v5) | ~ % 90.29/12.77 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? % 90.29/12.77 [v7: any] : ? [v8: any] : (s_e(v1, v2, v4, v5) = v7 & s_e(v0, v2, v3, v5) = % 90.29/12.77 v6 & s_e(v0, v1, v3, v4) = v8 & ( ~ (v7 = 0) | ~ (v6 = 0) | v8 = 0))) & % 90.29/12.77 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 90.29/12.77 $i] : ( ~ (s_e(v1, v2, v4, v5) = 0) | ~ (s_e(v0, v2, v3, v5) = 0) | ~ % 90.29/12.77 $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: % 90.29/12.77 any] : ? [v7: any] : ? [v8: any] : (s_t(v3, v4, v5) = v7 & s_t(v0, v1, % 90.29/12.77 v2) = v6 & s_e(v0, v1, v3, v4) = v8 & ( ~ (v7 = 0) | ~ (v6 = 0) | v8 = % 90.29/12.77 0))) % 90.29/12.77 % 90.29/12.77 (aSatz5_12b) % 90.29/12.77 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_t(v0, % 90.29/12.77 v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? % 90.29/12.77 [v5: any] : ? [v6: any] : (le(v1, v2, v0, v2) = v6 & le(v0, v1, v0, v2) = % 90.29/12.77 v5 & s_col(v0, v1, v2) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) % 90.29/12.77 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (le(v1, v2, v0, v2) = 0) | ~ % 90.29/12.77 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] % 90.29/12.77 : (le(v0, v1, v0, v2) = v5 & s_col(v0, v1, v2) = v3 & s_t(v0, v1, v2) = v4 & % 90.29/12.77 ( ~ (v5 = 0) | ~ (v3 = 0) | v4 = 0))) & ! [v0: $i] : ! [v1: $i] : ! % 90.29/12.77 [v2: $i] : ( ~ (le(v0, v1, v0, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 90.29/12.77 ? [v3: any] : ? [v4: any] : ? [v5: any] : (le(v1, v2, v0, v2) = v5 & % 90.29/12.77 s_col(v0, v1, v2) = v3 & s_t(v0, v1, v2) = v4 & ( ~ (v5 = 0) | ~ (v3 = 0) % 90.29/12.77 | v4 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_col(v0, % 90.29/12.77 v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? % 90.29/12.77 [v4: any] : ? [v5: any] : (le(v1, v2, v0, v2) = v5 & le(v0, v1, v0, v2) = % 90.29/12.77 v4 & s_t(v0, v1, v2) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | v3 = 0))) % 90.29/12.77 % 90.29/12.77 (aSatz6_28) % 90.95/12.78 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 90.95/12.78 $i] : ! [v6: int] : (v6 = 0 | ~ (s_e(v1, v2, v4, v5) = 0) | ~ (s_e(v0, % 90.95/12.78 v2, v3, v5) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 90.95/12.78 $i(v1) | ~ $i(v0) | ? [v7: any] : ? [v8: any] : ? [v9: any] : % 90.95/12.78 (sameside(v3, v4, v5) = v8 & sameside(v0, v1, v2) = v7 & s_e(v1, v0, v4, v3) % 90.95/12.78 = v9 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0)))) & ! [v0: $i] : ! [v1: % 90.95/12.78 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: int] : % 90.95/12.78 (v6 = 0 | ~ (s_e(v1, v0, v4, v3) = 0) | ~ (s_e(v0, v2, v3, v5) = v6) | ~ % 90.95/12.78 $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v7: % 90.95/12.78 any] : ? [v8: any] : ? [v9: any] : (sameside(v3, v4, v5) = v8 & % 90.95/12.78 sameside(v0, v1, v2) = v7 & s_e(v1, v2, v4, v5) = v9 & ( ~ (v9 = 0) | ~ % 90.95/12.78 (v8 = 0) | ~ (v7 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 90.95/12.78 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (sameside(v3, v4, v5) = 0) | ~ % 90.95/12.78 (sameside(v0, v1, v2) = 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 90.95/12.78 ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : % 90.95/12.78 (s_e(v1, v2, v4, v5) = v7 & s_e(v1, v0, v4, v3) = v6 & s_e(v0, v2, v3, v5) = % 90.95/12.78 v8 & ( ~ (v7 = 0) | ~ (v6 = 0) | v8 = 0))) & ! [v0: $i] : ! [v1: $i] : % 90.95/12.78 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ (s_e(v1, v2, v4, % 90.95/12.78 v5) = 0) | ~ (s_e(v1, v0, v4, v3) = 0) | ~ $i(v5) | ~ $i(v4) | ~ % 90.95/12.78 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : % 90.95/12.78 ? [v8: any] : (sameside(v3, v4, v5) = v7 & sameside(v0, v1, v2) = v6 & % 90.95/12.78 s_e(v0, v2, v3, v5) = v8 & ( ~ (v7 = 0) | ~ (v6 = 0) | v8 = 0))) % 90.95/12.78 % 90.95/12.78 (aSatz6_4b) % 90.95/12.78 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 90.95/12.78 (sameside(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 90.95/12.78 any] : ? [v5: any] : (s_col(v0, v1, v2) = v4 & s_t(v0, v1, v2) = v5 & ( ~ % 90.95/12.78 (v4 = 0) | v5 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 90.95/12.78 int] : (v3 = 0 | ~ (s_t(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 90.95/12.78 $i(v0) | ? [v4: any] : ? [v5: any] : (sameside(v0, v1, v2) = v4 & % 90.95/12.78 s_col(v0, v1, v2) = v5 & ( ~ (v5 = 0) | v4 = 0))) & ! [v0: $i] : ! [v1: % 90.95/12.78 $i] : ! [v2: $i] : ( ~ (s_col(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ % 90.95/12.78 $i(v0) | ? [v3: any] : ? [v4: any] : (sameside(v0, v1, v2) = v3 & s_t(v0, % 90.95/12.78 v1, v2) = v4 & (v4 = 0 | v3 = 0))) % 90.95/12.78 % 90.95/12.78 (aSatz7_17) % 90.95/12.78 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v1 | ~ (s_m(v0, % 90.95/12.78 v3, v2) = 0) | ~ (s_m(v0, v1, v2) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 90.95/12.78 $i(v1) | ~ $i(v0)) % 90.95/12.78 % 90.95/12.78 (aSatz7_20) % 90.95/12.79 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | v2 = v0 | % 90.95/12.79 ~ (s_m(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] % 90.95/12.79 : ? [v5: any] : (s_col(v0, v1, v2) = v4 & s_e(v1, v0, v1, v2) = v5 & ( ~ % 90.95/12.79 (v5 = 0) | ~ (v4 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 90.95/12.79 (v2 = v0 | ~ (s_col(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 90.95/12.79 [v3: any] : ? [v4: any] : (s_m(v0, v1, v2) = v4 & s_e(v1, v0, v1, v2) = v3 % 90.95/12.79 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 % 90.95/12.79 = v0 | ~ (s_e(v1, v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 90.95/12.79 [v3: any] : ? [v4: any] : (s_m(v0, v1, v2) = v4 & s_col(v0, v1, v2) = v3 & % 90.95/12.79 ( ~ (v3 = 0) | v4 = 0))) % 90.95/12.79 % 90.95/12.79 (aSatz7_25) % 90.95/12.79 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (isomidpoint(v1, % 90.95/12.79 v2, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? % 90.95/12.79 [v5: any] : (s_m(v1, v3, v2) = v5 & s_e(v0, v1, v0, v2) = v4 & ( ~ (v4 = 0) % 90.95/12.79 | v5 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_e(v0, v1, % 90.95/12.79 v0, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : % 90.95/12.79 (isomidpoint(v1, v2, v0) = v3 & s_m(v1, v3, v2) = 0 & $i(v3))) % 90.95/12.79 % 90.95/12.79 (aSatz7_6) % 90.95/12.79 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_m(v0, v1, v2) = 0) | ~ % 90.95/12.79 $i(v2) | ~ $i(v1) | ~ $i(v0) | s(v1, v0) = v2) % 90.95/12.79 % 90.95/12.79 (aSatz7_7) % 90.95/12.79 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s(v0, v1) = v2) | ~ $i(v1) | % 90.95/12.79 ~ $i(v0) | s(v0, v2) = v1) % 90.95/12.79 % 90.95/12.79 (aSatz8_21a) % 90.95/12.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | v1 = v0 | % 90.95/12.80 ~ (s_col(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] % 90.95/12.80 : ? [v5: $i] : (erectAux21a(v0, v1, v2) = v4 & erect21a(v0, v1, v2) = v5 & % 90.95/12.80 s_t(v2, v4, v5) = 0 & $i(v5) & $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! % 90.95/12.80 [v2: $i] : ! [v3: int] : (v3 = 0 | v1 = v0 | ~ (s_col(v0, v1, v2) = v3) | ~ % 90.95/12.80 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : (erectAux21a(v0, v1, v2) = v4 % 90.95/12.80 & s_col(v0, v1, v4) = 0 & $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 90.95/12.80 $i] : ! [v3: int] : (v3 = 0 | v1 = v0 | ~ (s_col(v0, v1, v2) = v3) | ~ % 90.95/12.80 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : (erect21a(v0, v1, v2) = v4 & % 90.95/12.80 perp(v0, v1, v4, v0) = 0 & $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 90.95/12.80 $i] : ! [v3: $i] : (v1 = v0 | ~ (erectAux21a(v0, v1, v2) = v3) | ~ $i(v2) % 90.95/12.80 | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: any] : ? [v6: any] : % 90.95/12.80 (erect21a(v0, v1, v2) = v4 & s_col(v0, v1, v2) = v6 & s_t(v2, v3, v4) = v5 & % 90.95/12.80 $i(v4) & (v6 = 0 | v5 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 90.95/12.80 ! [v3: $i] : (v1 = v0 | ~ (erectAux21a(v0, v1, v2) = v3) | ~ $i(v2) | ~ % 90.95/12.80 $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : (s_col(v0, v1, v3) = v4 & % 90.95/12.80 s_col(v0, v1, v2) = v5 & (v5 = 0 | v4 = 0))) & ! [v0: $i] : ! [v1: $i] : % 90.95/12.80 ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (erect21a(v0, v1, v2) = v3) | ~ % 90.95/12.80 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: any] : ? [v6: any] : % 90.95/12.80 (erectAux21a(v0, v1, v2) = v4 & s_col(v0, v1, v2) = v6 & s_t(v2, v4, v3) = % 90.95/12.80 v5 & $i(v4) & (v6 = 0 | v5 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 90.95/12.80 $i] : ! [v3: $i] : (v1 = v0 | ~ (erect21a(v0, v1, v2) = v3) | ~ $i(v2) | % 90.95/12.80 ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : (perp(v0, v1, v3, v0) = % 90.95/12.80 v4 & s_col(v0, v1, v2) = v5 & (v5 = 0 | v4 = 0))) % 90.95/12.80 % 90.95/12.80 (aSatz8_22) % 90.95/12.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (midpoint(v0, v1) = v2) | ~ % 90.95/12.80 $i(v1) | ~ $i(v0) | s_m(v0, v2, v1) = 0) % 90.95/12.80 % 90.95/12.80 (aSatz8_4) % 90.95/12.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 90.95/12.80 | ~ (s_r(v0, v1, v3) = v4) | ~ (s(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | % 90.95/12.80 ~ $i(v0) | ? [v5: int] : ( ~ (v5 = 0) & s_r(v0, v1, v2) = v5)) & ! [v0: % 90.95/12.80 $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_r(v0, v1, v2) = 0) | ~ $i(v2) | ~ % 90.95/12.80 $i(v1) | ~ $i(v0) | ? [v3: $i] : (s_r(v0, v1, v3) = 0 & s(v1, v2) = v3 & % 90.95/12.80 $i(v3))) % 90.95/12.80 % 90.95/12.80 (d_Defn4_10) % 90.95/12.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 90.95/12.80 (s_col(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] % 90.95/12.80 : ( ~ (v4 = 0) & s_t(v2, v0, v1) = v4)) & ! [v0: $i] : ! [v1: $i] : ! % 90.95/12.80 [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_col(v0, v1, v2) = v3) | ~ $i(v2) | % 90.95/12.80 ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_t(v1, v2, v0) = v4)) % 90.95/12.80 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 90.95/12.80 (s_col(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] % 90.95/12.80 : ( ~ (v4 = 0) & s_t(v0, v1, v2) = v4)) & ! [v0: $i] : ! [v1: $i] : ! % 90.95/12.80 [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_t(v2, v0, v1) = v3) | ~ $i(v2) | ~ % 90.95/12.80 $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: any] : (s_col(v0, % 90.95/12.80 v1, v2) = v4 & s_t(v1, v2, v0) = v6 & s_t(v0, v1, v2) = v5 & ( ~ (v4 = % 90.95/12.80 0) | v6 = 0 | v5 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 90.95/12.80 [v3: int] : (v3 = 0 | ~ (s_t(v1, v2, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 90.95/12.80 $i(v0) | ? [v4: any] : ? [v5: any] : ? [v6: any] : (s_col(v0, v1, v2) = % 90.95/12.80 v4 & s_t(v2, v0, v1) = v6 & s_t(v0, v1, v2) = v5 & ( ~ (v4 = 0) | v6 = 0 | % 90.95/12.80 v5 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 % 90.95/12.80 = 0 | ~ (s_t(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 90.95/12.80 [v4: any] : ? [v5: any] : ? [v6: any] : (s_col(v0, v1, v2) = v4 & s_t(v2, % 90.95/12.80 v0, v1) = v6 & s_t(v1, v2, v0) = v5 & ( ~ (v4 = 0) | v6 = 0 | v5 = 0))) % 90.95/12.80 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_col(v0, v1, v2) = 0) | ~ % 90.95/12.80 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] % 90.95/12.80 : (s_t(v2, v0, v1) = v5 & s_t(v1, v2, v0) = v4 & s_t(v0, v1, v2) = v3 & (v5 % 90.95/12.80 = 0 | v4 = 0 | v3 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 90.95/12.80 (s_t(v2, v0, v1) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | s_col(v0, v1, % 90.95/12.80 v2) = 0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_t(v1, v2, v0) % 90.95/12.80 = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | s_col(v0, v1, v2) = 0) & ! % 90.95/12.80 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_t(v0, v1, v2) = 0) | ~ $i(v2) | % 90.95/12.80 ~ $i(v1) | ~ $i(v0) | s_col(v0, v1, v2) = 0) % 90.95/12.80 % 90.95/12.80 (d_Defn6_1) % 90.95/12.81 $i(xb) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | v2 % 90.95/12.81 = v1 | v1 = v0 | ~ (sameside(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 90.95/12.81 $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_t(v1, v2, v0) = v4)) & ! [v0: $i] % 90.95/12.81 : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | v1 = v0 | v1 = xb | ~ % 90.95/12.81 (sameside(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 90.95/12.81 int] : ( ~ (v4 = 0) & s_t(v1, v0, v2) = v4)) & ! [v0: $i] : ! [v1: $i] : % 90.95/12.81 ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_t(v1, v2, v0) = v3) | ~ $i(v2) | % 90.95/12.81 ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : (sameside(v0, v1, v2) % 90.95/12.81 = v4 & s_t(v1, v0, v2) = v5 & ( ~ (v4 = 0) | v5 = 0))) & ! [v0: $i] : ! % 90.95/12.81 [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_t(v1, v0, v2) = v3) | % 90.95/12.81 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : % 90.95/12.81 (sameside(v0, v1, v2) = v4 & s_t(v1, v2, v0) = v5 & ( ~ (v4 = 0) | v5 = 0))) % 90.95/12.81 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | v1 = v0 | ~ (s_t(v1, % 90.95/12.81 v2, v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | sameside(v0, v1, v2) % 90.95/12.81 = 0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | v1 = xb | ~ % 90.95/12.81 (s_t(v1, v0, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | sameside(v0, v1, % 90.95/12.81 v2) = 0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sameside(v0, v1, % 90.95/12.81 v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 90.95/12.81 any] : (s_t(v1, v2, v0) = v4 & s_t(v1, v0, v2) = v3 & (v4 = 0 | v3 = 0))) % 91.10/12.81 & ! [v0: $i] : ! [v1: $i] : ( ~ (sameside(v0, v1, v1) = 0) | ~ $i(v1) | ~ % 91.10/12.81 $i(v0)) & ! [v0: $i] : ! [v1: $i] : ( ~ (sameside(v0, v0, v1) = 0) | ~ % 91.10/12.81 $i(v1) | ~ $i(v0)) % 91.10/12.81 % 91.10/12.81 (d_Defn7_1) % 91.10/12.81 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_m(v0, % 91.10/12.81 v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? % 91.10/12.81 [v5: any] : (s_t(v0, v1, v2) = v4 & s_e(v1, v0, v1, v2) = v5 & ( ~ (v5 = 0) % 91.10/12.81 | ~ (v4 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 91.10/12.81 int] : (v3 = 0 | ~ (s_t(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 91.10/12.81 $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_m(v0, v1, v2) = v4)) & ! [v0: $i] % 91.10/12.81 : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_e(v1, v0, v1, v2) % 91.10/12.81 = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & % 91.10/12.81 s_m(v0, v1, v2) = v4)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 91.10/12.81 (s_m(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | s_t(v0, v1, v2) % 91.10/12.81 = 0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_m(v0, v1, v2) = 0) | % 91.10/12.81 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | s_e(v1, v0, v1, v2) = 0) & ! [v0: $i] : % 91.10/12.81 ! [v1: $i] : ! [v2: $i] : ( ~ (s_t(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) % 91.10/12.81 | ~ $i(v0) | ? [v3: any] : ? [v4: any] : (s_m(v0, v1, v2) = v4 & s_e(v1, % 91.10/12.81 v0, v1, v2) = v3 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0: $i] : ! [v1: $i] % 91.10/12.81 : ! [v2: $i] : ( ~ (s_e(v1, v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ % 91.10/12.81 $i(v0) | ? [v3: any] : ? [v4: any] : (s_m(v0, v1, v2) = v4 & s_t(v0, v1, % 91.10/12.81 v2) = v3 & ( ~ (v3 = 0) | v4 = 0))) % 91.10/12.81 % 91.10/12.81 (d_Defn8_1) % 91.10/12.81 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 91.10/12.81 | ~ (s(v1, v2) = v3) | ~ (s_e(v0, v2, v0, v3) = v4) | ~ $i(v2) | ~ % 91.10/12.81 $i(v1) | ~ $i(v0) | ? [v5: int] : ( ~ (v5 = 0) & s_r(v0, v1, v2) = v5)) & % 91.10/12.81 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_r(v0, % 91.10/12.81 v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ? % 91.10/12.81 [v5: int] : ( ~ (v5 = 0) & s(v1, v2) = v4 & s_e(v0, v2, v0, v4) = v5 & % 91.10/12.81 $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 91.10/12.81 (s(v1, v2) = v3) | ~ (s_e(v0, v2, v0, v3) = 0) | ~ $i(v2) | ~ $i(v1) | ~ % 91.10/12.81 $i(v0) | s_r(v0, v1, v2) = 0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( % 91.10/12.81 ~ (s_r(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : % 91.10/12.81 (s(v1, v2) = v3 & s_e(v0, v2, v0, v3) = 0 & $i(v3))) % 91.10/12.81 % 91.10/12.81 (d_insert) % 91.10/12.82 $i(gamma) & $i(alpha) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 91.10/12.82 : ! [v4: $i] : ! [v5: $i] : ( ~ (ext(v4, v2, v0, v1) = v5) | ~ (ext(v3, v2, % 91.10/12.82 alpha, gamma) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 91.10/12.82 (insert(v0, v1, v2, v3) = v5 & $i(v5))) & ! [v0: $i] : ! [v1: $i] : ! % 91.10/12.82 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (insert(v0, v1, v2, v3) = v4) | ~ % 91.10/12.82 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (ext(v5, v2, v0, % 91.10/12.82 v1) = v4 & ext(v3, v2, alpha, gamma) = v5 & $i(v5) & $i(v4))) % 91.10/12.82 % 91.10/12.82 (function-axioms) % 91.10/12.83 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 91.10/12.83 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] % 91.10/12.83 : ! [v9: $i] : (v1 = v0 | ~ (s_afs(v9, v8, v7, v6, v5, v4, v3, v2) = v1) | % 91.10/12.83 ~ (s_afs(v9, v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] % 91.10/12.83 : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 91.18/12.83 [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : (v1 = v0 | % 91.18/12.83 ~ (s_fs(v9, v8, v7, v6, v5, v4, v3, v2) = v1) | ~ (s_fs(v9, v8, v7, v6, v5, % 91.18/12.83 v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 91.18/12.83 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 91.18/12.83 ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : (v1 = v0 | ~ % 91.18/12.83 (s_ifs(v9, v8, v7, v6, v5, v4, v3, v2) = v1) | ~ (s_ifs(v9, v8, v7, v6, v5, % 91.18/12.83 v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 91.18/12.83 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 91.18/12.83 ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : (v1 = v0 | ~ (s_kf(v8, v7, v6, v5, % 91.18/12.83 v4, v3, v2) = v1) | ~ (s_kf(v8, v7, v6, v5, v4, v3, v2) = v0)) & ! % 91.18/12.83 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 91.18/12.83 $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : (v1 = v0 | ~ % 91.18/12.83 (s_e3(v7, v6, v5, v4, v3, v2) = v1) | ~ (s_e3(v7, v6, v5, v4, v3, v2) = % 91.18/12.83 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 91.18/12.83 : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : (v1 = v0 | ~ (crossbar(v7, v6, % 91.18/12.83 v5, v4, v3, v2) = v1) | ~ (crossbar(v7, v6, v5, v4, v3, v2) = v0)) & ! % 91.18/12.83 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 91.18/12.83 : ! [v6: $i] : (v1 = v0 | ~ (g811(v6, v5, v4, v3, v2) = v1) | ~ (g811(v6, % 91.18/12.83 v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 91.18/12.83 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (f811(v6, % 91.18/12.83 v5, v4, v3, v2) = v1) | ~ (f811(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 91.18/12.83 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 91.18/12.83 ! [v6: $i] : (v1 = v0 | ~ (op(v6, v5, v4, v3, v2) = v1) | ~ (op(v6, v5, v4, % 91.18/12.83 v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 91.18/12.83 ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (midpointAux(v6, v5, % 91.18/12.83 v4, v3, v2) = v1) | ~ (midpointAux(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 91.18/12.83 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 91.18/12.83 ! [v6: $i] : (v1 = v0 | ~ (g813(v6, v5, v4, v3, v2) = v1) | ~ (g813(v6, v5, % 91.18/12.83 v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 91.18/12.83 $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (f813(v6, v5, % 91.18/12.83 v4, v3, v2) = v1) | ~ (f813(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 91.18/12.83 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 91.18/12.83 : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (perpAt(v6, v5, v4, % 91.18/12.83 v3, v2) = v1) | ~ (perpAt(v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! % 91.18/12.83 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] % 91.18/12.83 : (v1 = v0 | ~ (insert5(v6, v5, v4, v3, v2) = v1) | ~ (insert5(v6, v5, v4, % 91.18/12.83 v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 91.18/12.83 ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (ip(v6, v5, v4, v3, % 91.18/12.83 v2) = v1) | ~ (ip(v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 91.18/12.83 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 91.18/12.83 (ss3(v5, v4, v3, v2) = v1) | ~ (ss3(v5, v4, v3, v2) = v0)) & ! [v0: $i] : % 91.18/12.83 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 % 91.18/12.83 | ~ (ss2(v5, v4, v3, v2) = v1) | ~ (ss2(v5, v4, v3, v2) = v0)) & ! [v0: % 91.18/12.83 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 91.18/12.83 (v1 = v0 | ~ (ss1(v5, v4, v3, v2) = v1) | ~ (ss1(v5, v4, v3, v2) = v0)) & ! % 91.18/12.83 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 91.18/12.83 $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (opposite(v5, v4, v3, v2) = % 91.18/12.83 v1) | ~ (opposite(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 91.18/12.83 ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 91.18/12.83 $i] : (v1 = v0 | ~ (samesideline(v5, v4, v3, v2) = v1) | ~ % 91.18/12.83 (samesideline(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 91.18/12.83 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (il(v5, v4, % 91.18/12.83 v3, v2) = v1) | ~ (il(v5, v4, v3, v2) = v0)) & ! [v0: % 91.18/12.83 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 91.18/12.83 : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (perp(v5, v4, v3, v2) = v1) | ~ % 91.18/12.83 (perp(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 91.18/12.83 [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (ins(v5, v4, v3, v2) = % 91.18/12.83 v1) | ~ (ins(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 91.18/12.83 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 91.18/12.83 $i] : (v1 = v0 | ~ (le(v5, v4, v3, v2) = v1) | ~ (le(v5, v4, v3, v2) = % 91.18/12.83 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 91.18/12.83 : ! [v5: $i] : (v1 = v0 | ~ (insert(v5, v4, v3, v2) = v1) | ~ (insert(v5, % 91.18/12.83 v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 91.18/12.83 $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (ext(v5, v4, v3, v2) = v1) | % 91.18/12.83 ~ (ext(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 91.18/12.83 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 91.18/12.83 (v1 = v0 | ~ (s_e(v5, v4, v3, v2) = v1) | ~ (s_e(v5, v4, v3, v2) = v0)) & ! % 91.18/12.83 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 91.18/12.83 ~ (reflect(v4, v3, v2) = v1) | ~ (reflect(v4, v3, v2) = v0)) & ! [v0: $i] % 91.18/12.83 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 91.18/12.83 (erectAux(v4, v3, v2) = v1) | ~ (erectAux(v4, v3, v2) = v0)) & ! [v0: $i] % 91.18/12.83 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 91.18/12.83 (erect(v4, v3, v2) = v1) | ~ (erect(v4, v3, v2) = v0)) & ! [v0: $i] : ! % 91.18/12.83 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 91.18/12.83 (erectAux21a(v4, v3, v2) = v1) | ~ (erectAux21a(v4, v3, v2) = v0)) & ! % 91.18/12.83 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 91.18/12.83 ~ (erect21a(v4, v3, v2) = v1) | ~ (erect21a(v4, v3, v2) = v0)) & ! [v0: % 91.18/12.83 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 91.18/12.83 (foot(v4, v3, v2) = v1) | ~ (foot(v4, v3, v2) = v0)) & ! [v0: % 91.18/12.83 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 91.18/12.83 : ! [v4: $i] : (v1 = v0 | ~ (s_r(v4, v3, v2) = v1) | ~ (s_r(v4, v3, v2) = % 91.18/12.83 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 91.18/12.83 : (v1 = v0 | ~ (isomidpoint(v4, v3, v2) = v1) | ~ (isomidpoint(v4, v3, v2) = % 91.18/12.83 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 91.18/12.83 $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (s_m(v4, v3, v2) = v1) | ~ % 91.18/12.83 (s_m(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 91.18/12.83 $i] : ! [v4: $i] : (v1 = v0 | ~ (c63(v4, v3, v2) = v1) | ~ (c63(v4, v3, % 91.18/12.83 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 91.18/12.83 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (sameside(v4, v3, v2) = % 91.18/12.83 v1) | ~ (sameside(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 91.18/12.83 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 91.18/12.83 ~ (s_col(v4, v3, v2) = v1) | ~ (s_col(v4, v3, v2) = v0)) & ! [v0: % 91.18/12.83 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 91.18/12.83 : ! [v4: $i] : (v1 = v0 | ~ (s_t(v4, v3, v2) = v1) | ~ (s_t(v4, v3, v2) = % 91.18/12.83 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 91.18/12.83 ~ (midpoint(v3, v2) = v1) | ~ (midpoint(v3, v2) = v0)) & ! [v0: $i] : ! % 91.18/12.83 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (s(v3, v2) = v1) | ~ % 91.18/12.83 (s(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 91.18/12.83 (v1 = v0 | ~ (pointOffLine(v3, v2) = v1) | ~ (pointOffLine(v3, v2) = v0)) % 91.18/12.83 % 91.18/12.83 Further assumptions not needed in the proof: % 91.18/12.83 -------------------------------------------- % 91.18/12.83 aA1, aA3, aA4, aA5, aA6, aA7, aExtCol2, aExtPerp, aExtPerp2, aExtPerp3, % 91.18/12.83 aExtPerp4, aExtPerp5, aExtPerp6, aExtSameSide1, aExtSameSide2, aLemma9_13a, % 91.18/12.83 aLemma9_13b, aLemma9_13c, aLemma9_13d, aLemma9_13e, aLemma9_13f, % 91.18/12.83 aLemma9_13f_case1, aLemma9_13f_case2, aLemma9_13g, aNarbouxLemma1, aSatz10_10, % 91.18/12.83 aSatz10_10a, aSatz10_2a, aSatz10_2b, aSatz10_4, aSatz10_5, aSatz10_6, aSatz10_7, % 91.18/12.83 aSatz10_8a, aSatz10_8b, aSatz2_1, aSatz2_12, aSatz2_13, aSatz2_15, aSatz2_4, % 91.18/12.83 aSatz2_5, aSatz2_8, aSatz3_1, aSatz3_13a, aSatz3_13c, aSatz3_14a, aSatz3_14b, % 91.18/12.83 aSatz3_17, aSatz3_4, aSatz3_5a, aSatz3_5b, aSatz3_6a, aSatz3_6b, aSatz3_7a, % 91.18/12.83 aSatz3_7b, aSatz4_11a, aSatz4_11b, aSatz4_11c, aSatz4_11d, aSatz4_11e, % 91.18/12.83 aSatz4_12, aSatz4_12b, aSatz4_13, aSatz4_14, aSatz4_16, aSatz4_17, aSatz4_18, % 91.18/12.83 aSatz4_19, aSatz4_2, aSatz4_5, aSatz4_6, aSatz5_1, aSatz5_10, aSatz5_11, % 91.18/12.83 aSatz5_12a1, aSatz5_12a2, aSatz5_2, aSatz5_3, aSatz5_5a, aSatz5_5b, aSatz5_6, % 91.18/12.83 aSatz5_7, aSatz5_8, aSatz5_9, aSatz6_11a, aSatz6_11b, aSatz6_13a, aSatz6_13b, % 91.18/12.83 aSatz6_15a, aSatz6_15b, aSatz6_15c, aSatz6_15d, aSatz6_16a, aSatz6_16b, % 91.18/12.83 aSatz6_17a, aSatz6_17b, aSatz6_18, aSatz6_21, aSatz6_25, aSatz6_2a, aSatz6_2b, % 91.18/12.83 aSatz6_3a, aSatz6_3b, aSatz6_4a, aSatz6_5, aSatz6_6, aSatz6_7, aSatz7_10a, % 91.18/12.83 aSatz7_10b, aSatz7_13, aSatz7_15a, aSatz7_15b, aSatz7_16a, aSatz7_16b, % 91.18/12.83 aSatz7_18, aSatz7_19, aSatz7_2, aSatz7_21, aSatz7_22, aSatz7_22a, aSatz7_22b, % 91.18/12.83 aSatz7_3a, aSatz7_3b, aSatz7_4a, aSatz7_4b, aSatz7_8, aSatz7_9, aSatz8_10, % 91.18/12.83 aSatz8_12a, aSatz8_12b, aSatz8_13a, aSatz8_13b, aSatz8_14a, aSatz8_14b, % 91.18/12.83 aSatz8_14c, aSatz8_15, aSatz8_16a, aSatz8_16b, aSatz8_18, aSatz8_18a, aSatz8_2, % 91.18/12.83 aSatz8_20a, aSatz8_20b, aSatz8_21, aSatz8_22b, aSatz8_24, aSatz8_24a, % 91.18/12.83 aSatz8_24b, aSatz8_3, aSatz8_5, aSatz8_6, aSatz8_7, aSatz8_8, aSatz8_9, % 91.18/12.83 aSatz9_13, aSatz9_16, aSatz9_19b, aSatz9_2, aSatz9_3, aSatz9_3a, aSatz9_4, % 91.18/12.83 aSatz9_4a, aSatz9_4a2, aSatz9_4b, aSatz9_4c, aSatz9_5, aSatz9_6, aSatz9_8, % 91.18/12.83 aSatz9_9, aSideReflect, aext1, aperp1, d_Defn2_10, d_Defn4_1, d_Defn4_15, % 91.18/12.83 d_Defn4_4, d_Defn5_4, d_Defn7_23, d_Defn8_11a, d_Defn8_11b, d_Defn9_1, d_Defn9_7 % 91.18/12.83 % 91.18/12.83 Those formulas are unsatisfiable: % 91.18/12.83 --------------------------------- % 91.18/12.83 % 91.18/12.83 Begin of proof % 91.18/12.83 | % 91.18/12.83 | ALPHA: (aA2) implies: % 91.18/12.83 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 91.18/12.83 | ! [v5: $i] : ( ~ (s_e(v0, v1, v4, v5) = 0) | ~ (s_e(v0, v1, v2, v3) = % 91.18/12.83 | 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 91.18/12.83 | $i(v0) | s_e(v2, v3, v4, v5) = 0) % 91.18/12.83 | % 91.18/12.83 | ALPHA: (aA8) implies: % 91.18/12.83 | (2) ? [v0: int] : ? [v1: int] : ? [v2: int] : ( ~ (v2 = 0) & ~ (v1 = 0) % 91.18/12.83 | & ~ (v0 = 0) & s_t(gamma, alpha, beta) = v2 & s_t(beta, gamma, % 91.18/12.83 | alpha) = v1 & s_t(alpha, beta, gamma) = v0) % 91.18/12.83 | % 91.18/12.83 | ALPHA: (aSatz2_2) implies: % 91.18/12.83 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (s_e(v0, % 91.18/12.83 | v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) % 91.18/12.83 | | s_e(v2, v3, v0, v1) = 0) % 91.18/12.83 | % 91.18/12.83 | ALPHA: (aSatz2_3) implies: % 91.18/12.83 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 91.18/12.83 | ! [v5: $i] : ! [v6: int] : (v6 = 0 | ~ (s_e(v0, v1, v4, v5) = v6) | % 91.18/12.83 | ~ (s_e(v0, v1, v2, v3) = 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 91.18/12.83 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v7: int] : ( ~ (v7 = 0) & % 91.18/12.83 | s_e(v2, v3, v4, v5) = v7)) % 91.18/12.83 | % 91.18/12.83 | ALPHA: (aSatz2_11) implies: % 91.18/12.83 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 91.18/12.83 | ! [v5: $i] : ( ~ (s_e(v1, v2, v4, v5) = 0) | ~ (s_e(v0, v1, v3, v4) = % 91.18/12.83 | 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 91.18/12.83 | $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : (s_t(v3, v4, % 91.18/12.83 | v5) = v7 & s_t(v0, v1, v2) = v6 & s_e(v0, v2, v3, v5) = v8 & ( ~ % 91.18/12.83 | (v7 = 0) | ~ (v6 = 0) | v8 = 0))) % 91.18/12.83 | % 91.18/12.83 | ALPHA: (aSatz2_14) implies: % 91.18/12.84 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (s_e(v0, % 91.18/12.84 | v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) % 91.18/12.84 | | s_e(v1, v0, v3, v2) = 0) % 91.18/12.84 | % 91.18/12.84 | ALPHA: (aSatz3_2) implies: % 91.18/12.84 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 91.18/12.84 | (s_t(v2, v1, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 91.18/12.84 | int] : ( ~ (v4 = 0) & s_t(v0, v1, v2) = v4)) % 91.18/12.84 | % 91.18/12.84 | ALPHA: (aSatz3_13b) implies: % 91.18/12.84 | (8) ~ (gamma = beta) % 91.18/12.84 | (9) $i(beta) % 91.18/12.84 | % 91.18/12.84 | ALPHA: (aSatz4_3) implies: % 91.18/12.84 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 91.18/12.84 | ! [v5: $i] : ( ~ (s_e(v1, v2, v4, v5) = 0) | ~ (s_e(v0, v2, v3, v5) = % 91.18/12.84 | 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 91.18/12.84 | ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : (s_t(v3, v4, % 91.18/12.84 | v5) = v7 & s_t(v0, v1, v2) = v6 & s_e(v0, v1, v3, v4) = v8 & ( ~ % 91.18/12.84 | (v7 = 0) | ~ (v6 = 0) | v8 = 0))) % 91.18/12.84 | % 91.18/12.84 | ALPHA: (aSatz5_12b) implies: % 91.18/12.84 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 91.18/12.84 | (s_t(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 91.18/12.84 | any] : ? [v5: any] : ? [v6: any] : (le(v1, v2, v0, v2) = v6 & % 91.18/12.84 | le(v0, v1, v0, v2) = v5 & s_col(v0, v1, v2) = v4 & ( ~ (v6 = 0) | % 91.18/12.84 | ~ (v5 = 0) | ~ (v4 = 0)))) % 91.18/12.84 | % 91.18/12.84 | ALPHA: (aSatz6_4b) implies: % 91.18/12.84 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 91.18/12.84 | (s_t(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 91.18/12.84 | any] : ? [v5: any] : (sameside(v0, v1, v2) = v4 & s_col(v0, v1, % 91.18/12.84 | v2) = v5 & ( ~ (v5 = 0) | v4 = 0))) % 91.18/12.84 | % 91.18/12.84 | ALPHA: (aSatz6_28) implies: % 91.18/12.84 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 91.18/12.84 | ! [v5: $i] : ( ~ (s_e(v1, v2, v4, v5) = 0) | ~ (s_e(v1, v0, v4, v3) = % 91.18/12.84 | 0) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 91.18/12.84 | ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : % 91.18/12.84 | (sameside(v3, v4, v5) = v7 & sameside(v0, v1, v2) = v6 & s_e(v0, v2, % 91.18/12.84 | v3, v5) = v8 & ( ~ (v7 = 0) | ~ (v6 = 0) | v8 = 0))) % 91.18/12.84 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 91.18/12.84 | ! [v5: $i] : ! [v6: int] : (v6 = 0 | ~ (s_e(v1, v2, v4, v5) = 0) | % 91.18/12.84 | ~ (s_e(v0, v2, v3, v5) = v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | % 91.18/12.84 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v7: any] : ? [v8: any] : ? % 91.18/12.84 | [v9: any] : (sameside(v3, v4, v5) = v8 & sameside(v0, v1, v2) = v7 & % 91.18/12.84 | s_e(v1, v0, v4, v3) = v9 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = % 91.18/12.84 | 0)))) % 91.18/12.84 | % 91.18/12.84 | ALPHA: (aSatz7_20) implies: % 91.18/12.84 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v0 | ~ (s_e(v1, v0, % 91.18/12.84 | v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] % 91.18/12.84 | : ? [v4: any] : (s_m(v0, v1, v2) = v4 & s_col(v0, v1, v2) = v3 & ( % 91.18/12.84 | ~ (v3 = 0) | v4 = 0))) % 91.18/12.84 | % 91.18/12.84 | ALPHA: (aSatz7_25) implies: % 91.18/12.84 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_e(v0, v1, v0, v2) = % 91.18/12.84 | 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : % 91.18/12.84 | (isomidpoint(v1, v2, v0) = v3 & s_m(v1, v3, v2) = 0 & $i(v3))) % 91.18/12.84 | % 91.18/12.84 | ALPHA: (aSatz8_4) implies: % 91.18/12.84 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_r(v0, v1, v2) = 0) | % 91.18/12.84 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : (s_r(v0, v1, v3) = % 91.18/12.84 | 0 & s(v1, v2) = v3 & $i(v3))) % 91.18/12.84 | % 91.18/12.84 | ALPHA: (aSatz8_21a) implies: % 91.18/12.84 | (18) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | v1 % 91.18/12.84 | = v0 | ~ (s_col(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 91.18/12.84 | $i(v0) | ? [v4: $i] : ? [v5: $i] : (erectAux21a(v0, v1, v2) = v4 & % 91.18/12.84 | erect21a(v0, v1, v2) = v5 & s_t(v2, v4, v5) = 0 & $i(v5) & % 91.18/12.84 | $i(v4))) % 91.18/12.84 | % 91.18/12.84 | ALPHA: (aSatz10_12b) implies: % 91.18/12.84 | (19) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (s_r(v0, % 91.18/12.84 | v1, v2) = 0) | ~ (s_e(v0, v1, v3, v1) = 0) | ~ $i(v3) | ~ % 91.18/12.84 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : % 91.18/12.84 | (s_r(v3, v1, v2) = v4 & s_e(v0, v2, v3, v2) = v5 & ( ~ (v4 = 0) | v5 % 91.18/12.84 | = 0))) % 91.18/12.85 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (s_r(v3, % 91.18/12.85 | v1, v2) = 0) | ~ (s_e(v0, v1, v3, v1) = 0) | ~ $i(v3) | ~ % 91.18/12.85 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : % 91.18/12.85 | (s_r(v0, v1, v2) = v4 & s_e(v0, v2, v3, v2) = v5 & ( ~ (v4 = 0) | v5 % 91.18/12.85 | = 0))) % 91.18/12.85 | (21) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (s_r(v3, % 91.18/12.85 | v1, v2) = 0) | ~ (s_r(v0, v1, v2) = 0) | ~ $i(v3) | ~ $i(v2) % 91.18/12.85 | | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : (s_e(v0, v2, % 91.18/12.85 | v3, v2) = v5 & s_e(v0, v1, v3, v1) = v4 & ( ~ (v4 = 0) | v5 = % 91.18/12.85 | 0))) % 91.18/12.85 | % 91.18/12.85 | ALPHA: (d_insert) implies: % 91.18/12.85 | (22) $i(alpha) % 91.18/12.85 | (23) $i(gamma) % 91.18/12.85 | % 91.18/12.85 | ALPHA: (d_Defn4_10) implies: % 91.18/12.85 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 91.18/12.85 | (s_t(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 91.18/12.85 | any] : ? [v5: any] : ? [v6: any] : (s_col(v0, v1, v2) = v4 & % 91.18/12.85 | s_t(v2, v0, v1) = v6 & s_t(v1, v2, v0) = v5 & ( ~ (v4 = 0) | v6 = % 91.18/12.85 | 0 | v5 = 0))) % 91.18/12.85 | (25) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 91.18/12.85 | (s_t(v1, v2, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 91.18/12.85 | any] : ? [v5: any] : ? [v6: any] : (s_col(v0, v1, v2) = v4 & % 91.18/12.85 | s_t(v2, v0, v1) = v6 & s_t(v0, v1, v2) = v5 & ( ~ (v4 = 0) | v6 = % 91.18/12.85 | 0 | v5 = 0))) % 91.18/12.85 | (26) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 91.18/12.85 | (s_t(v2, v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 91.18/12.85 | any] : ? [v5: any] : ? [v6: any] : (s_col(v0, v1, v2) = v4 & % 91.18/12.85 | s_t(v1, v2, v0) = v6 & s_t(v0, v1, v2) = v5 & ( ~ (v4 = 0) | v6 = % 91.18/12.85 | 0 | v5 = 0))) % 91.18/12.85 | % 91.18/12.85 | ALPHA: (d_Defn6_1) implies: % 91.18/12.85 | (27) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 91.18/12.85 | (s_t(v1, v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 91.18/12.85 | any] : ? [v5: any] : (sameside(v0, v1, v2) = v4 & s_t(v1, v2, v0) % 91.18/12.85 | = v5 & ( ~ (v4 = 0) | v5 = 0))) % 91.18/12.85 | (28) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 91.18/12.85 | (s_t(v1, v2, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 91.18/12.85 | any] : ? [v5: any] : (sameside(v0, v1, v2) = v4 & s_t(v1, v0, v2) % 91.18/12.85 | = v5 & ( ~ (v4 = 0) | v5 = 0))) % 91.18/12.85 | % 91.18/12.85 | ALPHA: (d_Defn7_1) implies: % 91.18/12.85 | (29) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_e(v1, v0, v1, v2) = % 91.18/12.85 | 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 91.18/12.85 | any] : (s_m(v0, v1, v2) = v4 & s_t(v0, v1, v2) = v3 & ( ~ (v3 = 0) % 91.18/12.85 | | v4 = 0))) % 91.18/12.85 | % 91.18/12.85 | ALPHA: (d_Defn8_1) implies: % 91.18/12.85 | (30) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_r(v0, v1, v2) = 0) | % 91.18/12.85 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : (s(v1, v2) = v3 & % 91.18/12.85 | s_e(v0, v2, v0, v3) = 0 & $i(v3))) % 91.18/12.85 | % 91.18/12.85 | ALPHA: (function-axioms) implies: % 91.18/12.85 | (31) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 91.18/12.85 | (s(v3, v2) = v1) | ~ (s(v3, v2) = v0)) % 91.18/12.85 | (32) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 91.18/12.85 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (s_t(v4, v3, v2) = v1) | % 91.18/12.85 | ~ (s_t(v4, v3, v2) = v0)) % 91.18/12.85 | (33) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 91.18/12.85 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (s_col(v4, v3, v2) = v1) | % 91.18/12.85 | ~ (s_col(v4, v3, v2) = v0)) % 91.18/12.85 | (34) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 91.18/12.85 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (s_m(v4, v3, v2) = v1) | % 91.18/12.85 | ~ (s_m(v4, v3, v2) = v0)) % 91.18/12.85 | (35) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 91.18/12.85 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (s_r(v4, v3, v2) = v1) | % 91.18/12.85 | ~ (s_r(v4, v3, v2) = v0)) % 91.18/12.85 | (36) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 91.18/12.85 | : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (s_e(v5, v4, % 91.18/12.85 | v3, v2) = v1) | ~ (s_e(v5, v4, v3, v2) = v0)) % 91.18/12.85 | % 91.18/12.85 | DELTA: instantiating (2) with fresh symbols all_208_0, all_208_1, all_208_2 % 91.18/12.85 | gives: % 91.18/12.85 | (37) ~ (all_208_0 = 0) & ~ (all_208_1 = 0) & ~ (all_208_2 = 0) & % 91.18/12.85 | s_t(gamma, alpha, beta) = all_208_0 & s_t(beta, gamma, alpha) = % 91.18/12.85 | all_208_1 & s_t(alpha, beta, gamma) = all_208_2 % 91.18/12.85 | % 91.18/12.85 | ALPHA: (37) implies: % 91.18/12.85 | (38) ~ (all_208_2 = 0) % 91.18/12.86 | (39) ~ (all_208_1 = 0) % 91.18/12.86 | (40) ~ (all_208_0 = 0) % 91.18/12.86 | (41) s_t(alpha, beta, gamma) = all_208_2 % 91.18/12.86 | (42) s_t(beta, gamma, alpha) = all_208_1 % 91.18/12.86 | (43) s_t(gamma, alpha, beta) = all_208_0 % 91.18/12.86 | % 91.18/12.86 | DELTA: instantiating (aSatz10_12c) with fresh symbols all_212_0, all_212_1, % 91.18/12.86 | all_212_2, all_212_3, all_212_4, all_212_5 gives: % 91.18/12.86 | (44) ~ (all_212_0 = 0) & ~ (all_212_1 = all_212_3) & midpoint(all_212_3, % 91.18/12.86 | all_212_1) = all_212_4 & s_r(all_212_2, all_212_4, all_212_1) = 0 & % 91.18/12.86 | s_r(all_212_5, all_212_4, all_212_3) = 0 & s_e(all_212_4, all_212_3, % 91.18/12.86 | all_212_4, all_212_1) = 0 & s_e(all_212_5, all_212_3, all_212_2, % 91.18/12.86 | all_212_1) = all_212_0 & s_e(all_212_5, all_212_4, all_212_2, % 91.18/12.86 | all_212_4) = 0 & $i(all_212_1) & $i(all_212_2) & $i(all_212_3) & % 91.18/12.86 | $i(all_212_4) & $i(all_212_5) % 91.18/12.86 | % 91.18/12.86 | ALPHA: (44) implies: % 91.18/12.86 | (45) ~ (all_212_1 = all_212_3) % 91.18/12.86 | (46) ~ (all_212_0 = 0) % 91.18/12.86 | (47) $i(all_212_5) % 91.18/12.86 | (48) $i(all_212_4) % 91.18/12.86 | (49) $i(all_212_3) % 91.18/12.86 | (50) $i(all_212_2) % 91.18/12.86 | (51) $i(all_212_1) % 91.18/12.86 | (52) s_e(all_212_5, all_212_4, all_212_2, all_212_4) = 0 % 91.18/12.86 | (53) s_e(all_212_5, all_212_3, all_212_2, all_212_1) = all_212_0 % 91.18/12.86 | (54) s_e(all_212_4, all_212_3, all_212_4, all_212_1) = 0 % 91.18/12.86 | (55) s_r(all_212_5, all_212_4, all_212_3) = 0 % 91.18/12.86 | (56) s_r(all_212_2, all_212_4, all_212_1) = 0 % 91.18/12.86 | (57) midpoint(all_212_3, all_212_1) = all_212_4 % 91.18/12.86 | % 91.18/12.86 | GROUND_INST: instantiating (1) with all_212_5, all_212_4, all_212_2, % 91.18/12.86 | all_212_4, all_212_2, all_212_4, simplifying with (47), (48), % 91.18/12.86 | (50), (52) gives: % 91.18/12.86 | (58) s_e(all_212_2, all_212_4, all_212_2, all_212_4) = 0 % 91.18/12.86 | % 91.18/12.86 | GROUND_INST: instantiating (10) with all_212_5, all_212_5, all_212_4, % 91.18/12.86 | all_212_2, all_212_2, all_212_4, simplifying with (47), (48), % 91.18/12.86 | (50), (52) gives: % 91.18/12.86 | (59) ? [v0: any] : ? [v1: any] : ? [v2: any] : (s_t(all_212_2, % 91.18/12.86 | all_212_2, all_212_4) = v1 & s_t(all_212_5, all_212_5, all_212_4) % 91.18/12.86 | = v0 & s_e(all_212_5, all_212_5, all_212_2, all_212_2) = v2 & ( ~ % 91.18/12.86 | (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 91.18/12.86 | % 91.18/12.86 | GROUND_INST: instantiating (3) with all_212_5, all_212_4, all_212_2, % 91.18/12.86 | all_212_4, simplifying with (47), (48), (50), (52) gives: % 91.18/12.86 | (60) s_e(all_212_2, all_212_4, all_212_5, all_212_4) = 0 % 91.18/12.86 | % 91.18/12.86 | GROUND_INST: instantiating (6) with all_212_5, all_212_4, all_212_2, % 91.18/12.86 | all_212_4, simplifying with (47), (48), (50), (52) gives: % 91.18/12.86 | (61) s_e(all_212_4, all_212_5, all_212_4, all_212_2) = 0 % 91.18/12.86 | % 91.18/12.86 | GROUND_INST: instantiating (1) with all_212_4, all_212_3, all_212_4, % 91.18/12.86 | all_212_1, all_212_4, all_212_1, simplifying with (48), (49), % 91.18/12.86 | (51), (54) gives: % 91.18/12.86 | (62) s_e(all_212_4, all_212_1, all_212_4, all_212_1) = 0 % 91.18/12.86 | % 91.18/12.86 | GROUND_INST: instantiating (14) with all_212_5, all_212_4, all_212_3, % 91.18/12.86 | all_212_2, all_212_4, all_212_1, all_212_0, simplifying with % 91.18/12.86 | (47), (48), (49), (50), (51), (53), (54) gives: % 91.18/12.86 | (63) all_212_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.86 | (sameside(all_212_2, all_212_4, all_212_1) = v1 & sameside(all_212_5, % 91.18/12.86 | all_212_4, all_212_3) = v0 & s_e(all_212_4, all_212_5, all_212_4, % 91.18/12.86 | all_212_2) = v2 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = 0))) % 91.18/12.86 | % 91.18/12.86 | GROUND_INST: instantiating (5) with all_212_5, all_212_4, all_212_3, % 91.18/12.86 | all_212_2, all_212_4, all_212_1, simplifying with (47), (48), % 91.18/12.86 | (49), (50), (51), (52), (54) gives: % 91.18/12.86 | (64) ? [v0: any] : ? [v1: any] : ? [v2: any] : (s_t(all_212_2, % 91.18/12.86 | all_212_4, all_212_1) = v1 & s_t(all_212_5, all_212_4, all_212_3) % 91.18/12.86 | = v0 & s_e(all_212_5, all_212_3, all_212_2, all_212_1) = v2 & ( ~ % 91.18/12.86 | (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 91.18/12.86 | % 91.18/12.86 | GROUND_INST: instantiating (15) with all_212_3, all_212_4, all_212_1, % 91.18/12.86 | simplifying with (48), (49), (51), (54) gives: % 91.18/12.86 | (65) all_212_1 = all_212_3 | ? [v0: any] : ? [v1: any] : (s_m(all_212_3, % 91.18/12.86 | all_212_4, all_212_1) = v1 & s_col(all_212_3, all_212_4, % 91.18/12.86 | all_212_1) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 91.18/12.86 | % 91.18/12.86 | GROUND_INST: instantiating (29) with all_212_3, all_212_4, all_212_1, % 91.18/12.86 | simplifying with (48), (49), (51), (54) gives: % 91.18/12.86 | (66) ? [v0: any] : ? [v1: any] : (s_m(all_212_3, all_212_4, all_212_1) = % 91.18/12.86 | v1 & s_t(all_212_3, all_212_4, all_212_1) = v0 & ( ~ (v0 = 0) | v1 = % 91.18/12.86 | 0)) % 91.18/12.86 | % 91.18/12.86 | GROUND_INST: instantiating (16) with all_212_4, all_212_3, all_212_1, % 91.18/12.86 | simplifying with (48), (49), (51), (54) gives: % 91.18/12.86 | (67) ? [v0: $i] : (isomidpoint(all_212_3, all_212_1, all_212_4) = v0 & % 91.18/12.86 | s_m(all_212_3, v0, all_212_1) = 0 & $i(v0)) % 91.18/12.86 | % 91.18/12.86 | GROUND_INST: instantiating (26) with beta, gamma, alpha, all_208_2, % 91.18/12.86 | simplifying with (9), (22), (23), (41) gives: % 91.18/12.87 | (68) all_208_2 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.87 | (s_col(beta, gamma, alpha) = v0 & s_t(gamma, alpha, beta) = v2 & % 91.18/12.87 | s_t(beta, gamma, alpha) = v1 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.87 | % 91.18/12.87 | GROUND_INST: instantiating (25) with gamma, alpha, beta, all_208_2, % 91.18/12.87 | simplifying with (9), (22), (23), (41) gives: % 91.18/12.87 | (69) all_208_2 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.87 | (s_col(gamma, alpha, beta) = v0 & s_t(gamma, alpha, beta) = v1 & % 91.18/12.87 | s_t(beta, gamma, alpha) = v2 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.87 | % 91.18/12.87 | GROUND_INST: instantiating (28) with gamma, alpha, beta, all_208_2, % 91.18/12.87 | simplifying with (9), (22), (23), (41) gives: % 91.18/12.87 | (70) all_208_2 = 0 | ? [v0: any] : ? [v1: any] : (sameside(gamma, alpha, % 91.18/12.87 | beta) = v0 & s_t(alpha, gamma, beta) = v1 & ( ~ (v0 = 0) | v1 = % 91.18/12.87 | 0)) % 91.18/12.87 | % 91.18/12.87 | GROUND_INST: instantiating (27) with beta, alpha, gamma, all_208_2, % 91.18/12.87 | simplifying with (9), (22), (23), (41) gives: % 91.18/12.87 | (71) all_208_2 = 0 | ? [v0: any] : ? [v1: any] : (sameside(beta, alpha, % 91.18/12.87 | gamma) = v0 & s_t(alpha, gamma, beta) = v1 & ( ~ (v0 = 0) | v1 = % 91.18/12.87 | 0)) % 91.18/12.87 | % 91.18/12.87 | GROUND_INST: instantiating (24) with alpha, beta, gamma, all_208_2, % 91.18/12.87 | simplifying with (9), (22), (23), (41) gives: % 91.18/12.87 | (72) all_208_2 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.87 | (s_col(alpha, beta, gamma) = v0 & s_t(gamma, alpha, beta) = v2 & % 91.18/12.87 | s_t(beta, gamma, alpha) = v1 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.87 | % 91.18/12.87 | GROUND_INST: instantiating (7) with alpha, gamma, beta, all_208_1, simplifying % 91.18/12.87 | with (9), (22), (23), (42) gives: % 91.18/12.87 | (73) all_208_1 = 0 | ? [v0: int] : ( ~ (v0 = 0) & s_t(alpha, gamma, beta) % 91.18/12.87 | = v0) % 91.18/12.87 | % 91.18/12.87 | GROUND_INST: instantiating (26) with gamma, alpha, beta, all_208_1, % 91.18/12.87 | simplifying with (9), (22), (23), (42) gives: % 91.18/12.87 | (74) all_208_1 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.87 | (s_col(gamma, alpha, beta) = v0 & s_t(gamma, alpha, beta) = v1 & % 91.18/12.87 | s_t(alpha, beta, gamma) = v2 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.87 | % 91.18/12.87 | GROUND_INST: instantiating (25) with alpha, beta, gamma, all_208_1, % 91.18/12.87 | simplifying with (9), (22), (23), (42) gives: % 91.18/12.87 | (75) all_208_1 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.87 | (s_col(alpha, beta, gamma) = v0 & s_t(gamma, alpha, beta) = v2 & % 91.18/12.87 | s_t(alpha, beta, gamma) = v1 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.87 | % 91.18/12.87 | GROUND_INST: instantiating (11) with beta, gamma, alpha, all_208_1, % 91.18/12.87 | simplifying with (9), (22), (23), (42) gives: % 91.18/12.87 | (76) all_208_1 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.87 | (le(gamma, alpha, beta, alpha) = v2 & le(beta, gamma, beta, alpha) = % 91.18/12.87 | v1 & s_col(beta, gamma, alpha) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | % 91.18/12.87 | ~ (v0 = 0))) % 91.18/12.87 | % 91.18/12.87 | GROUND_INST: instantiating (24) with beta, gamma, alpha, all_208_1, % 91.18/12.87 | simplifying with (9), (22), (23), (42) gives: % 91.18/12.87 | (77) all_208_1 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.87 | (s_col(beta, gamma, alpha) = v0 & s_t(gamma, alpha, beta) = v1 & % 91.18/12.87 | s_t(alpha, beta, gamma) = v2 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.87 | % 91.18/12.87 | GROUND_INST: instantiating (12) with beta, gamma, alpha, all_208_1, % 91.18/12.87 | simplifying with (9), (22), (23), (42) gives: % 91.18/12.87 | (78) all_208_1 = 0 | ? [v0: any] : ? [v1: any] : (sameside(beta, gamma, % 91.18/12.87 | alpha) = v0 & s_col(beta, gamma, alpha) = v1 & ( ~ (v1 = 0) | v0 = % 91.18/12.87 | 0)) % 91.18/12.87 | % 91.18/12.87 | GROUND_INST: instantiating (26) with alpha, beta, gamma, all_208_0, % 91.18/12.87 | simplifying with (9), (22), (23), (43) gives: % 91.18/12.87 | (79) all_208_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.87 | (s_col(alpha, beta, gamma) = v0 & s_t(beta, gamma, alpha) = v2 & % 91.18/12.87 | s_t(alpha, beta, gamma) = v1 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.87 | % 91.18/12.87 | GROUND_INST: instantiating (25) with beta, gamma, alpha, all_208_0, % 91.18/12.87 | simplifying with (9), (22), (23), (43) gives: % 91.18/12.87 | (80) all_208_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.87 | (s_col(beta, gamma, alpha) = v0 & s_t(beta, gamma, alpha) = v1 & % 91.18/12.87 | s_t(alpha, beta, gamma) = v2 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.87 | % 91.18/12.87 | GROUND_INST: instantiating (24) with gamma, alpha, beta, all_208_0, % 91.18/12.87 | simplifying with (9), (22), (23), (43) gives: % 91.18/12.87 | (81) all_208_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.87 | (s_col(gamma, alpha, beta) = v0 & s_t(beta, gamma, alpha) = v2 & % 91.18/12.87 | s_t(alpha, beta, gamma) = v1 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.87 | % 91.18/12.88 | GROUND_INST: instantiating (17) with all_212_5, all_212_4, all_212_3, % 91.18/12.88 | simplifying with (47), (48), (49), (55) gives: % 91.18/12.88 | (82) ? [v0: $i] : (s_r(all_212_5, all_212_4, v0) = 0 & s(all_212_4, % 91.18/12.88 | all_212_3) = v0 & $i(v0)) % 91.18/12.88 | % 91.18/12.88 | GROUND_INST: instantiating (30) with all_212_5, all_212_4, all_212_3, % 91.18/12.88 | simplifying with (47), (48), (49), (55) gives: % 91.18/12.88 | (83) ? [v0: $i] : (s(all_212_4, all_212_3) = v0 & s_e(all_212_5, % 91.18/12.88 | all_212_3, all_212_5, v0) = 0 & $i(v0)) % 91.18/12.88 | % 91.18/12.88 | GROUND_INST: instantiating (21) with all_212_2, all_212_4, all_212_1, % 91.18/12.88 | all_212_2, simplifying with (48), (50), (51), (56) gives: % 91.18/12.88 | (84) ? [v0: any] : ? [v1: any] : (s_e(all_212_2, all_212_1, all_212_2, % 91.18/12.88 | all_212_1) = v1 & s_e(all_212_2, all_212_4, all_212_2, all_212_4) % 91.18/12.88 | = v0 & ( ~ (v0 = 0) | v1 = 0)) % 91.18/12.88 | % 91.18/12.88 | GROUND_INST: instantiating (20) with all_212_5, all_212_4, all_212_1, % 91.18/12.88 | all_212_2, simplifying with (47), (48), (50), (51), (52), (56) % 91.18/12.88 | gives: % 91.18/12.88 | (85) ? [v0: any] : ? [v1: any] : (s_r(all_212_5, all_212_4, all_212_1) = % 91.18/12.88 | v0 & s_e(all_212_5, all_212_1, all_212_2, all_212_1) = v1 & ( ~ (v0 % 91.18/12.88 | = 0) | v1 = 0)) % 91.18/12.88 | % 91.18/12.88 | GROUND_INST: instantiating (17) with all_212_2, all_212_4, all_212_1, % 91.18/12.88 | simplifying with (48), (50), (51), (56) gives: % 91.18/12.88 | (86) ? [v0: $i] : (s_r(all_212_2, all_212_4, v0) = 0 & s(all_212_4, % 91.18/12.88 | all_212_1) = v0 & $i(v0)) % 91.18/12.88 | % 91.18/12.88 | GROUND_INST: instantiating (30) with all_212_2, all_212_4, all_212_1, % 91.18/12.88 | simplifying with (48), (50), (51), (56) gives: % 91.18/12.88 | (87) ? [v0: $i] : (s(all_212_4, all_212_1) = v0 & s_e(all_212_2, % 91.18/12.88 | all_212_1, all_212_2, v0) = 0 & $i(v0)) % 91.18/12.88 | % 91.18/12.88 | GROUND_INST: instantiating (aSatz8_22) with all_212_3, all_212_1, all_212_4, % 91.18/12.88 | simplifying with (49), (51), (57) gives: % 91.18/12.88 | (88) s_m(all_212_3, all_212_4, all_212_1) = 0 % 91.18/12.88 | % 91.18/12.88 | DELTA: instantiating (67) with fresh symbol all_220_0 gives: % 91.18/12.88 | (89) isomidpoint(all_212_3, all_212_1, all_212_4) = all_220_0 & % 91.18/12.88 | s_m(all_212_3, all_220_0, all_212_1) = 0 & $i(all_220_0) % 91.18/12.88 | % 91.18/12.88 | ALPHA: (89) implies: % 91.18/12.88 | (90) $i(all_220_0) % 91.18/12.88 | (91) s_m(all_212_3, all_220_0, all_212_1) = 0 % 91.18/12.88 | % 91.18/12.88 | DELTA: instantiating (83) with fresh symbol all_222_0 gives: % 91.18/12.88 | (92) s(all_212_4, all_212_3) = all_222_0 & s_e(all_212_5, all_212_3, % 91.18/12.88 | all_212_5, all_222_0) = 0 & $i(all_222_0) % 91.18/12.88 | % 91.18/12.88 | ALPHA: (92) implies: % 91.18/12.88 | (93) s_e(all_212_5, all_212_3, all_212_5, all_222_0) = 0 % 91.18/12.88 | (94) s(all_212_4, all_212_3) = all_222_0 % 91.18/12.88 | % 91.18/12.88 | DELTA: instantiating (82) with fresh symbol all_224_0 gives: % 91.18/12.88 | (95) s_r(all_212_5, all_212_4, all_224_0) = 0 & s(all_212_4, all_212_3) = % 91.18/12.88 | all_224_0 & $i(all_224_0) % 91.18/12.88 | % 91.18/12.88 | ALPHA: (95) implies: % 91.18/12.88 | (96) $i(all_224_0) % 91.18/12.88 | (97) s(all_212_4, all_212_3) = all_224_0 % 91.18/12.88 | (98) s_r(all_212_5, all_212_4, all_224_0) = 0 % 91.18/12.88 | % 91.18/12.88 | DELTA: instantiating (87) with fresh symbol all_226_0 gives: % 91.18/12.88 | (99) s(all_212_4, all_212_1) = all_226_0 & s_e(all_212_2, all_212_1, % 91.18/12.88 | all_212_2, all_226_0) = 0 & $i(all_226_0) % 91.18/12.88 | % 91.18/12.88 | ALPHA: (99) implies: % 91.18/12.88 | (100) s(all_212_4, all_212_1) = all_226_0 % 91.18/12.88 | % 91.18/12.88 | DELTA: instantiating (86) with fresh symbol all_228_0 gives: % 91.18/12.88 | (101) s_r(all_212_2, all_212_4, all_228_0) = 0 & s(all_212_4, all_212_1) = % 91.18/12.88 | all_228_0 & $i(all_228_0) % 91.18/12.88 | % 91.18/12.88 | ALPHA: (101) implies: % 91.18/12.88 | (102) $i(all_228_0) % 91.18/12.88 | (103) s(all_212_4, all_212_1) = all_228_0 % 91.18/12.88 | (104) s_r(all_212_2, all_212_4, all_228_0) = 0 % 91.18/12.88 | % 91.18/12.88 | DELTA: instantiating (66) with fresh symbols all_238_0, all_238_1 gives: % 91.18/12.88 | (105) s_m(all_212_3, all_212_4, all_212_1) = all_238_0 & s_t(all_212_3, % 91.18/12.88 | all_212_4, all_212_1) = all_238_1 & ( ~ (all_238_1 = 0) | all_238_0 % 91.18/12.88 | = 0) % 91.18/12.88 | % 91.18/12.88 | ALPHA: (105) implies: % 91.18/12.88 | (106) s_m(all_212_3, all_212_4, all_212_1) = all_238_0 % 91.18/12.88 | % 91.18/12.88 | DELTA: instantiating (85) with fresh symbols all_242_0, all_242_1 gives: % 91.18/12.88 | (107) s_r(all_212_5, all_212_4, all_212_1) = all_242_1 & s_e(all_212_5, % 91.18/12.88 | all_212_1, all_212_2, all_212_1) = all_242_0 & ( ~ (all_242_1 = 0) % 91.18/12.88 | | all_242_0 = 0) % 91.18/12.88 | % 91.18/12.88 | ALPHA: (107) implies: % 91.18/12.88 | (108) s_e(all_212_5, all_212_1, all_212_2, all_212_1) = all_242_0 % 91.18/12.88 | % 91.18/12.88 | DELTA: instantiating (84) with fresh symbols all_244_0, all_244_1 gives: % 91.18/12.88 | (109) s_e(all_212_2, all_212_1, all_212_2, all_212_1) = all_244_0 & % 91.18/12.88 | s_e(all_212_2, all_212_4, all_212_2, all_212_4) = all_244_1 & ( ~ % 91.18/12.88 | (all_244_1 = 0) | all_244_0 = 0) % 91.18/12.88 | % 91.18/12.88 | ALPHA: (109) implies: % 91.18/12.88 | (110) s_e(all_212_2, all_212_4, all_212_2, all_212_4) = all_244_1 % 91.18/12.88 | % 91.18/12.88 | DELTA: instantiating (59) with fresh symbols all_254_0, all_254_1, all_254_2 % 91.18/12.88 | gives: % 91.18/12.88 | (111) s_t(all_212_2, all_212_2, all_212_4) = all_254_1 & s_t(all_212_5, % 91.18/12.88 | all_212_5, all_212_4) = all_254_2 & s_e(all_212_5, all_212_5, % 91.18/12.88 | all_212_2, all_212_2) = all_254_0 & ( ~ (all_254_1 = 0) | ~ % 91.18/12.88 | (all_254_2 = 0) | all_254_0 = 0) % 91.18/12.88 | % 91.18/12.88 | ALPHA: (111) implies: % 91.18/12.88 | (112) s_t(all_212_2, all_212_2, all_212_4) = all_254_1 % 91.18/12.88 | % 91.18/12.88 | DELTA: instantiating (64) with fresh symbols all_256_0, all_256_1, all_256_2 % 91.18/12.88 | gives: % 91.18/12.88 | (113) s_t(all_212_2, all_212_4, all_212_1) = all_256_1 & s_t(all_212_5, % 91.18/12.88 | all_212_4, all_212_3) = all_256_2 & s_e(all_212_5, all_212_3, % 91.18/12.88 | all_212_2, all_212_1) = all_256_0 & ( ~ (all_256_1 = 0) | ~ % 91.18/12.88 | (all_256_2 = 0) | all_256_0 = 0) % 91.18/12.88 | % 91.18/12.88 | ALPHA: (113) implies: % 91.18/12.88 | (114) s_e(all_212_5, all_212_3, all_212_2, all_212_1) = all_256_0 % 91.18/12.88 | % 91.18/12.88 | BETA: splitting (80) gives: % 91.18/12.88 | % 91.18/12.88 | Case 1: % 91.18/12.88 | | % 91.18/12.88 | | (115) all_208_0 = 0 % 91.18/12.88 | | % 91.18/12.88 | | REDUCE: (40), (115) imply: % 91.18/12.88 | | (116) $false % 91.18/12.88 | | % 91.18/12.88 | | CLOSE: (116) is inconsistent. % 91.18/12.88 | | % 91.18/12.88 | Case 2: % 91.18/12.88 | | % 91.18/12.89 | | (117) ? [v0: any] : ? [v1: any] : ? [v2: any] : (s_col(beta, gamma, % 91.18/12.89 | | alpha) = v0 & s_t(beta, gamma, alpha) = v1 & s_t(alpha, beta, % 91.18/12.89 | | gamma) = v2 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.89 | | % 91.18/12.89 | | DELTA: instantiating (117) with fresh symbols all_267_0, all_267_1, % 91.18/12.89 | | all_267_2 gives: % 91.18/12.89 | | (118) s_col(beta, gamma, alpha) = all_267_2 & s_t(beta, gamma, alpha) = % 91.18/12.89 | | all_267_1 & s_t(alpha, beta, gamma) = all_267_0 & ( ~ (all_267_2 = % 91.18/12.89 | | 0) | all_267_0 = 0 | all_267_1 = 0) % 91.18/12.89 | | % 91.18/12.89 | | ALPHA: (118) implies: % 91.18/12.89 | | (119) s_t(alpha, beta, gamma) = all_267_0 % 91.18/12.89 | | (120) s_col(beta, gamma, alpha) = all_267_2 % 91.18/12.89 | | (121) ~ (all_267_2 = 0) | all_267_0 = 0 | all_267_1 = 0 % 91.18/12.89 | | % 91.18/12.89 | | BETA: splitting (75) gives: % 91.18/12.89 | | % 91.18/12.89 | | Case 1: % 91.18/12.89 | | | % 91.18/12.89 | | | (122) all_208_1 = 0 % 91.18/12.89 | | | % 91.18/12.89 | | | REDUCE: (39), (122) imply: % 91.18/12.89 | | | (123) $false % 91.18/12.89 | | | % 91.18/12.89 | | | CLOSE: (123) is inconsistent. % 91.18/12.89 | | | % 91.18/12.89 | | Case 2: % 91.18/12.89 | | | % 91.18/12.89 | | | (124) ? [v0: any] : ? [v1: any] : ? [v2: any] : (s_col(alpha, beta, % 91.18/12.89 | | | gamma) = v0 & s_t(gamma, alpha, beta) = v2 & s_t(alpha, beta, % 91.18/12.89 | | | gamma) = v1 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.89 | | | % 91.18/12.89 | | | DELTA: instantiating (124) with fresh symbols all_272_0, all_272_1, % 91.18/12.89 | | | all_272_2 gives: % 91.18/12.89 | | | (125) s_col(alpha, beta, gamma) = all_272_2 & s_t(gamma, alpha, beta) = % 91.18/12.89 | | | all_272_0 & s_t(alpha, beta, gamma) = all_272_1 & ( ~ (all_272_2 % 91.18/12.89 | | | = 0) | all_272_0 = 0 | all_272_1 = 0) % 91.18/12.89 | | | % 91.18/12.89 | | | ALPHA: (125) implies: % 91.18/12.89 | | | (126) s_t(alpha, beta, gamma) = all_272_1 % 91.18/12.89 | | | % 91.18/12.89 | | | BETA: splitting (77) gives: % 91.18/12.89 | | | % 91.18/12.89 | | | Case 1: % 91.18/12.89 | | | | % 91.18/12.89 | | | | (127) all_208_1 = 0 % 91.18/12.89 | | | | % 91.18/12.89 | | | | REDUCE: (39), (127) imply: % 91.18/12.89 | | | | (128) $false % 91.18/12.89 | | | | % 91.18/12.89 | | | | CLOSE: (128) is inconsistent. % 91.18/12.89 | | | | % 91.18/12.89 | | | Case 2: % 91.18/12.89 | | | | % 91.18/12.89 | | | | (129) ? [v0: any] : ? [v1: any] : ? [v2: any] : (s_col(beta, % 91.18/12.89 | | | | gamma, alpha) = v0 & s_t(gamma, alpha, beta) = v1 & % 91.18/12.89 | | | | s_t(alpha, beta, gamma) = v2 & ( ~ (v0 = 0) | v2 = 0 | v1 = % 91.18/12.89 | | | | 0)) % 91.18/12.89 | | | | % 91.18/12.89 | | | | DELTA: instantiating (129) with fresh symbols all_277_0, all_277_1, % 91.18/12.89 | | | | all_277_2 gives: % 91.18/12.89 | | | | (130) s_col(beta, gamma, alpha) = all_277_2 & s_t(gamma, alpha, beta) % 91.18/12.89 | | | | = all_277_1 & s_t(alpha, beta, gamma) = all_277_0 & ( ~ % 91.18/12.89 | | | | (all_277_2 = 0) | all_277_0 = 0 | all_277_1 = 0) % 91.18/12.89 | | | | % 91.18/12.89 | | | | ALPHA: (130) implies: % 91.18/12.89 | | | | (131) s_t(alpha, beta, gamma) = all_277_0 % 91.18/12.89 | | | | (132) s_t(gamma, alpha, beta) = all_277_1 % 91.18/12.89 | | | | (133) s_col(beta, gamma, alpha) = all_277_2 % 91.18/12.89 | | | | (134) ~ (all_277_2 = 0) | all_277_0 = 0 | all_277_1 = 0 % 91.18/12.89 | | | | % 91.18/12.89 | | | | BETA: splitting (73) gives: % 91.18/12.89 | | | | % 91.18/12.89 | | | | Case 1: % 91.18/12.89 | | | | | % 91.18/12.89 | | | | | (135) all_208_1 = 0 % 91.18/12.89 | | | | | % 91.18/12.89 | | | | | REDUCE: (39), (135) imply: % 91.18/12.89 | | | | | (136) $false % 91.18/12.89 | | | | | % 91.18/12.89 | | | | | CLOSE: (136) is inconsistent. % 91.18/12.89 | | | | | % 91.18/12.89 | | | | Case 2: % 91.18/12.89 | | | | | % 91.18/12.89 | | | | | (137) ? [v0: int] : ( ~ (v0 = 0) & s_t(alpha, gamma, beta) = v0) % 91.18/12.89 | | | | | % 91.18/12.89 | | | | | DELTA: instantiating (137) with fresh symbol all_287_0 gives: % 91.18/12.89 | | | | | (138) ~ (all_287_0 = 0) & s_t(alpha, gamma, beta) = all_287_0 % 91.18/12.89 | | | | | % 91.18/12.89 | | | | | ALPHA: (138) implies: % 91.18/12.89 | | | | | (139) ~ (all_287_0 = 0) % 91.18/12.89 | | | | | (140) s_t(alpha, gamma, beta) = all_287_0 % 91.18/12.89 | | | | | % 91.18/12.89 | | | | | BETA: splitting (74) gives: % 91.18/12.89 | | | | | % 91.18/12.89 | | | | | Case 1: % 91.18/12.89 | | | | | | % 91.18/12.89 | | | | | | (141) all_208_1 = 0 % 91.18/12.89 | | | | | | % 91.18/12.89 | | | | | | REDUCE: (39), (141) imply: % 91.18/12.89 | | | | | | (142) $false % 91.18/12.89 | | | | | | % 91.18/12.89 | | | | | | CLOSE: (142) is inconsistent. % 91.18/12.89 | | | | | | % 91.18/12.89 | | | | | Case 2: % 91.18/12.89 | | | | | | % 91.18/12.89 | | | | | | (143) ? [v0: any] : ? [v1: any] : ? [v2: any] : (s_col(gamma, % 91.18/12.89 | | | | | | alpha, beta) = v0 & s_t(gamma, alpha, beta) = v1 & % 91.18/12.89 | | | | | | s_t(alpha, beta, gamma) = v2 & ( ~ (v0 = 0) | v2 = 0 | v1 % 91.18/12.89 | | | | | | = 0)) % 91.18/12.89 | | | | | | % 91.18/12.89 | | | | | | DELTA: instantiating (143) with fresh symbols all_292_0, all_292_1, % 91.18/12.89 | | | | | | all_292_2 gives: % 91.18/12.89 | | | | | | (144) s_col(gamma, alpha, beta) = all_292_2 & s_t(gamma, alpha, % 91.18/12.89 | | | | | | beta) = all_292_1 & s_t(alpha, beta, gamma) = all_292_0 & % 91.18/12.89 | | | | | | ( ~ (all_292_2 = 0) | all_292_0 = 0 | all_292_1 = 0) % 91.18/12.89 | | | | | | % 91.18/12.89 | | | | | | ALPHA: (144) implies: % 91.18/12.89 | | | | | | (145) s_t(alpha, beta, gamma) = all_292_0 % 91.18/12.89 | | | | | | (146) s_t(gamma, alpha, beta) = all_292_1 % 91.18/12.89 | | | | | | % 91.18/12.89 | | | | | | BETA: splitting (81) gives: % 91.18/12.89 | | | | | | % 91.18/12.89 | | | | | | Case 1: % 91.18/12.89 | | | | | | | % 91.18/12.89 | | | | | | | (147) all_208_0 = 0 % 91.18/12.89 | | | | | | | % 91.18/12.89 | | | | | | | REDUCE: (40), (147) imply: % 91.18/12.89 | | | | | | | (148) $false % 91.18/12.89 | | | | | | | % 91.18/12.89 | | | | | | | CLOSE: (148) is inconsistent. % 91.18/12.89 | | | | | | | % 91.18/12.89 | | | | | | Case 2: % 91.18/12.89 | | | | | | | % 91.18/12.89 | | | | | | | (149) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.89 | | | | | | | (s_col(gamma, alpha, beta) = v0 & s_t(beta, gamma, alpha) % 91.18/12.89 | | | | | | | = v2 & s_t(alpha, beta, gamma) = v1 & ( ~ (v0 = 0) | v2 % 91.18/12.89 | | | | | | | = 0 | v1 = 0)) % 91.18/12.89 | | | | | | | % 91.18/12.89 | | | | | | | DELTA: instantiating (149) with fresh symbols all_302_0, % 91.18/12.89 | | | | | | | all_302_1, all_302_2 gives: % 91.18/12.89 | | | | | | | (150) s_col(gamma, alpha, beta) = all_302_2 & s_t(beta, gamma, % 91.18/12.89 | | | | | | | alpha) = all_302_0 & s_t(alpha, beta, gamma) = % 91.18/12.89 | | | | | | | all_302_1 & ( ~ (all_302_2 = 0) | all_302_0 = 0 | % 91.18/12.89 | | | | | | | all_302_1 = 0) % 91.18/12.89 | | | | | | | % 91.18/12.89 | | | | | | | ALPHA: (150) implies: % 91.18/12.89 | | | | | | | (151) s_t(alpha, beta, gamma) = all_302_1 % 91.18/12.89 | | | | | | | % 91.18/12.89 | | | | | | | BETA: splitting (72) gives: % 91.18/12.89 | | | | | | | % 91.18/12.89 | | | | | | | Case 1: % 91.18/12.89 | | | | | | | | % 91.18/12.89 | | | | | | | | (152) all_208_2 = 0 % 91.18/12.89 | | | | | | | | % 91.18/12.89 | | | | | | | | REDUCE: (38), (152) imply: % 91.18/12.89 | | | | | | | | (153) $false % 91.18/12.89 | | | | | | | | % 91.18/12.89 | | | | | | | | CLOSE: (153) is inconsistent. % 91.18/12.89 | | | | | | | | % 91.18/12.89 | | | | | | | Case 2: % 91.18/12.89 | | | | | | | | % 91.18/12.89 | | | | | | | | (154) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.89 | | | | | | | | (s_col(alpha, beta, gamma) = v0 & s_t(gamma, alpha, % 91.18/12.89 | | | | | | | | beta) = v2 & s_t(beta, gamma, alpha) = v1 & ( ~ (v0 % 91.18/12.89 | | | | | | | | = 0) | v2 = 0 | v1 = 0)) % 91.18/12.89 | | | | | | | | % 91.18/12.89 | | | | | | | | DELTA: instantiating (154) with fresh symbols all_317_0, % 91.18/12.89 | | | | | | | | all_317_1, all_317_2 gives: % 91.18/12.89 | | | | | | | | (155) s_col(alpha, beta, gamma) = all_317_2 & s_t(gamma, % 91.18/12.89 | | | | | | | | alpha, beta) = all_317_0 & s_t(beta, gamma, alpha) = % 91.18/12.89 | | | | | | | | all_317_1 & ( ~ (all_317_2 = 0) | all_317_0 = 0 | % 91.18/12.89 | | | | | | | | all_317_1 = 0) % 91.18/12.89 | | | | | | | | % 91.18/12.89 | | | | | | | | ALPHA: (155) implies: % 91.18/12.89 | | | | | | | | (156) s_t(gamma, alpha, beta) = all_317_0 % 91.18/12.89 | | | | | | | | % 91.18/12.89 | | | | | | | | BETA: splitting (79) gives: % 91.18/12.89 | | | | | | | | % 91.18/12.89 | | | | | | | | Case 1: % 91.18/12.89 | | | | | | | | | % 91.18/12.89 | | | | | | | | | (157) all_208_0 = 0 % 91.18/12.89 | | | | | | | | | % 91.18/12.89 | | | | | | | | | REDUCE: (40), (157) imply: % 91.18/12.89 | | | | | | | | | (158) $false % 91.18/12.89 | | | | | | | | | % 91.18/12.89 | | | | | | | | | CLOSE: (158) is inconsistent. % 91.18/12.89 | | | | | | | | | % 91.18/12.89 | | | | | | | | Case 2: % 91.18/12.89 | | | | | | | | | % 91.18/12.90 | | | | | | | | | (159) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.90 | | | | | | | | | (s_col(alpha, beta, gamma) = v0 & s_t(beta, gamma, % 91.18/12.90 | | | | | | | | | alpha) = v2 & s_t(alpha, beta, gamma) = v1 & ( ~ % 91.18/12.90 | | | | | | | | | (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.90 | | | | | | | | | % 91.18/12.90 | | | | | | | | | DELTA: instantiating (159) with fresh symbols all_322_0, % 91.18/12.90 | | | | | | | | | all_322_1, all_322_2 gives: % 91.18/12.90 | | | | | | | | | (160) s_col(alpha, beta, gamma) = all_322_2 & s_t(beta, % 91.18/12.90 | | | | | | | | | gamma, alpha) = all_322_0 & s_t(alpha, beta, gamma) % 91.18/12.90 | | | | | | | | | = all_322_1 & ( ~ (all_322_2 = 0) | all_322_0 = 0 | % 91.18/12.90 | | | | | | | | | all_322_1 = 0) % 91.18/12.90 | | | | | | | | | % 91.18/12.90 | | | | | | | | | ALPHA: (160) implies: % 91.18/12.90 | | | | | | | | | (161) s_t(alpha, beta, gamma) = all_322_1 % 91.18/12.90 | | | | | | | | | % 91.18/12.90 | | | | | | | | | BETA: splitting (69) gives: % 91.18/12.90 | | | | | | | | | % 91.18/12.90 | | | | | | | | | Case 1: % 91.18/12.90 | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | (162) all_208_2 = 0 % 91.18/12.90 | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | REDUCE: (38), (162) imply: % 91.18/12.90 | | | | | | | | | | (163) $false % 91.18/12.90 | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | CLOSE: (163) is inconsistent. % 91.18/12.90 | | | | | | | | | | % 91.18/12.90 | | | | | | | | | Case 2: % 91.18/12.90 | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | (164) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.90 | | | | | | | | | | (s_col(gamma, alpha, beta) = v0 & s_t(gamma, alpha, % 91.18/12.90 | | | | | | | | | | beta) = v1 & s_t(beta, gamma, alpha) = v2 & ( ~ % 91.18/12.90 | | | | | | | | | | (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.90 | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | DELTA: instantiating (164) with fresh symbols all_327_0, % 91.18/12.90 | | | | | | | | | | all_327_1, all_327_2 gives: % 91.18/12.90 | | | | | | | | | | (165) s_col(gamma, alpha, beta) = all_327_2 & s_t(gamma, % 91.18/12.90 | | | | | | | | | | alpha, beta) = all_327_1 & s_t(beta, gamma, % 91.18/12.90 | | | | | | | | | | alpha) = all_327_0 & ( ~ (all_327_2 = 0) | % 91.18/12.90 | | | | | | | | | | all_327_0 = 0 | all_327_1 = 0) % 91.18/12.90 | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | ALPHA: (165) implies: % 91.18/12.90 | | | | | | | | | | (166) s_t(gamma, alpha, beta) = all_327_1 % 91.18/12.90 | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | BETA: splitting (68) gives: % 91.18/12.90 | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | Case 1: % 91.18/12.90 | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | (167) all_208_2 = 0 % 91.18/12.90 | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | REDUCE: (38), (167) imply: % 91.18/12.90 | | | | | | | | | | | (168) $false % 91.18/12.90 | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | CLOSE: (168) is inconsistent. % 91.18/12.90 | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | Case 2: % 91.18/12.90 | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | (169) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.90 | | | | | | | | | | | (s_col(beta, gamma, alpha) = v0 & s_t(gamma, % 91.18/12.90 | | | | | | | | | | | alpha, beta) = v2 & s_t(beta, gamma, alpha) = % 91.18/12.90 | | | | | | | | | | | v1 & ( ~ (v0 = 0) | v2 = 0 | v1 = 0)) % 91.18/12.90 | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | DELTA: instantiating (169) with fresh symbols all_332_0, % 91.18/12.90 | | | | | | | | | | | all_332_1, all_332_2 gives: % 91.18/12.90 | | | | | | | | | | | (170) s_col(beta, gamma, alpha) = all_332_2 & s_t(gamma, % 91.18/12.90 | | | | | | | | | | | alpha, beta) = all_332_0 & s_t(beta, gamma, % 91.18/12.90 | | | | | | | | | | | alpha) = all_332_1 & ( ~ (all_332_2 = 0) | % 91.18/12.90 | | | | | | | | | | | all_332_0 = 0 | all_332_1 = 0) % 91.18/12.90 | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | ALPHA: (170) implies: % 91.18/12.90 | | | | | | | | | | | (171) s_t(gamma, alpha, beta) = all_332_0 % 91.18/12.90 | | | | | | | | | | | (172) s_col(beta, gamma, alpha) = all_332_2 % 91.18/12.90 | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | BETA: splitting (70) gives: % 91.18/12.90 | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | Case 1: % 91.18/12.90 | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | (173) all_208_2 = 0 % 91.18/12.90 | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | REDUCE: (38), (173) imply: % 91.18/12.90 | | | | | | | | | | | | (174) $false % 91.18/12.90 | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | CLOSE: (174) is inconsistent. % 91.18/12.90 | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | Case 2: % 91.18/12.90 | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | (175) ? [v0: any] : ? [v1: any] : (sameside(gamma, % 91.18/12.90 | | | | | | | | | | | | alpha, beta) = v0 & s_t(alpha, gamma, beta) = % 91.18/12.90 | | | | | | | | | | | | v1 & ( ~ (v0 = 0) | v1 = 0)) % 91.18/12.90 | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | DELTA: instantiating (175) with fresh symbols all_337_0, % 91.18/12.90 | | | | | | | | | | | | all_337_1 gives: % 91.18/12.90 | | | | | | | | | | | | (176) sameside(gamma, alpha, beta) = all_337_1 & % 91.18/12.90 | | | | | | | | | | | | s_t(alpha, gamma, beta) = all_337_0 & ( ~ % 91.18/12.90 | | | | | | | | | | | | (all_337_1 = 0) | all_337_0 = 0) % 91.18/12.90 | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | ALPHA: (176) implies: % 91.18/12.90 | | | | | | | | | | | | (177) s_t(alpha, gamma, beta) = all_337_0 % 91.18/12.90 | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | BETA: splitting (71) gives: % 91.18/12.90 | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | Case 1: % 91.18/12.90 | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | (178) all_208_2 = 0 % 91.18/12.90 | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | REDUCE: (38), (178) imply: % 91.18/12.90 | | | | | | | | | | | | | (179) $false % 91.18/12.90 | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | CLOSE: (179) is inconsistent. % 91.18/12.90 | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | Case 2: % 91.18/12.90 | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | (180) ? [v0: any] : ? [v1: any] : (sameside(beta, % 91.18/12.90 | | | | | | | | | | | | | alpha, gamma) = v0 & s_t(alpha, gamma, beta) = % 91.18/12.90 | | | | | | | | | | | | | v1 & ( ~ (v0 = 0) | v1 = 0)) % 91.18/12.90 | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | DELTA: instantiating (180) with fresh symbols all_362_0, % 91.18/12.90 | | | | | | | | | | | | | all_362_1 gives: % 91.18/12.90 | | | | | | | | | | | | | (181) sameside(beta, alpha, gamma) = all_362_1 & % 91.18/12.90 | | | | | | | | | | | | | s_t(alpha, gamma, beta) = all_362_0 & ( ~ % 91.18/12.90 | | | | | | | | | | | | | (all_362_1 = 0) | all_362_0 = 0) % 91.18/12.90 | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | ALPHA: (181) implies: % 91.18/12.90 | | | | | | | | | | | | | (182) s_t(alpha, gamma, beta) = all_362_0 % 91.18/12.90 | | | | | | | | | | | | | (183) ~ (all_362_1 = 0) | all_362_0 = 0 % 91.18/12.90 | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | BETA: splitting (78) gives: % 91.18/12.90 | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | Case 1: % 91.18/12.90 | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | (184) all_208_1 = 0 % 91.18/12.90 | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | REDUCE: (39), (184) imply: % 91.18/12.90 | | | | | | | | | | | | | | (185) $false % 91.18/12.90 | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | CLOSE: (185) is inconsistent. % 91.18/12.90 | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | Case 2: % 91.18/12.90 | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | (186) ? [v0: any] : ? [v1: any] : (sameside(beta, % 91.18/12.90 | | | | | | | | | | | | | | gamma, alpha) = v0 & s_col(beta, gamma, alpha) % 91.18/12.90 | | | | | | | | | | | | | | = v1 & ( ~ (v1 = 0) | v0 = 0)) % 91.18/12.90 | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | DELTA: instantiating (186) with fresh symbols all_387_0, % 91.18/12.90 | | | | | | | | | | | | | | all_387_1 gives: % 91.18/12.90 | | | | | | | | | | | | | | (187) sameside(beta, gamma, alpha) = all_387_1 & % 91.18/12.90 | | | | | | | | | | | | | | s_col(beta, gamma, alpha) = all_387_0 & ( ~ % 91.18/12.90 | | | | | | | | | | | | | | (all_387_0 = 0) | all_387_1 = 0) % 91.18/12.90 | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | ALPHA: (187) implies: % 91.18/12.90 | | | | | | | | | | | | | | (188) s_col(beta, gamma, alpha) = all_387_0 % 91.18/12.90 | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | BETA: splitting (76) gives: % 91.18/12.90 | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | Case 1: % 91.18/12.90 | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | (189) all_208_1 = 0 % 91.18/12.90 | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | REDUCE: (39), (189) imply: % 91.18/12.90 | | | | | | | | | | | | | | | (190) $false % 91.18/12.90 | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | CLOSE: (190) is inconsistent. % 91.18/12.90 | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | Case 2: % 91.18/12.90 | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | (191) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.90 | | | | | | | | | | | | | | | (le(gamma, alpha, beta, alpha) = v2 & le(beta, % 91.18/12.90 | | | | | | | | | | | | | | | gamma, beta, alpha) = v1 & s_col(beta, gamma, % 91.18/12.90 | | | | | | | | | | | | | | | alpha) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ % 91.18/12.90 | | | | | | | | | | | | | | | (v0 = 0))) % 91.18/12.90 | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | DELTA: instantiating (191) with fresh symbols all_437_0, % 91.18/12.90 | | | | | | | | | | | | | | | all_437_1, all_437_2 gives: % 91.18/12.90 | | | | | | | | | | | | | | | (192) le(gamma, alpha, beta, alpha) = all_437_0 & % 91.18/12.90 | | | | | | | | | | | | | | | le(beta, gamma, beta, alpha) = all_437_1 & % 91.18/12.90 | | | | | | | | | | | | | | | s_col(beta, gamma, alpha) = all_437_2 & ( ~ % 91.18/12.90 | | | | | | | | | | | | | | | (all_437_0 = 0) | ~ (all_437_1 = 0) | ~ % 91.18/12.90 | | | | | | | | | | | | | | | (all_437_2 = 0)) % 91.18/12.90 | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | ALPHA: (192) implies: % 91.18/12.90 | | | | | | | | | | | | | | | (193) s_col(beta, gamma, alpha) = all_437_2 % 91.18/12.90 | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | BETA: splitting (63) gives: % 91.18/12.90 | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | Case 1: % 91.18/12.90 | | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | | (194) all_212_0 = 0 % 91.18/12.90 | | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | | REDUCE: (46), (194) imply: % 91.18/12.90 | | | | | | | | | | | | | | | | (195) $false % 91.18/12.90 | | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | | CLOSE: (195) is inconsistent. % 91.18/12.90 | | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | Case 2: % 91.18/12.90 | | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | | (196) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.18/12.90 | | | | | | | | | | | | | | | | (sameside(all_212_2, all_212_4, all_212_1) = v1 & % 91.18/12.90 | | | | | | | | | | | | | | | | sameside(all_212_5, all_212_4, all_212_3) = v0 & % 91.18/12.90 | | | | | | | | | | | | | | | | s_e(all_212_4, all_212_5, all_212_4, all_212_2) % 91.18/12.90 | | | | | | | | | | | | | | | | = v2 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (v0 = % 91.18/12.90 | | | | | | | | | | | | | | | | 0))) % 91.18/12.90 | | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | | DELTA: instantiating (196) with fresh symbols all_452_0, % 91.18/12.90 | | | | | | | | | | | | | | | | all_452_1, all_452_2 gives: % 91.18/12.90 | | | | | | | | | | | | | | | | (197) sameside(all_212_2, all_212_4, all_212_1) = % 91.18/12.90 | | | | | | | | | | | | | | | | all_452_1 & sameside(all_212_5, all_212_4, % 91.18/12.90 | | | | | | | | | | | | | | | | all_212_3) = all_452_2 & s_e(all_212_4, % 91.18/12.90 | | | | | | | | | | | | | | | | all_212_5, all_212_4, all_212_2) = all_452_0 & ( % 91.18/12.90 | | | | | | | | | | | | | | | | ~ (all_452_0 = 0) | ~ (all_452_1 = 0) | ~ % 91.18/12.90 | | | | | | | | | | | | | | | | (all_452_2 = 0)) % 91.18/12.90 | | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | | ALPHA: (197) implies: % 91.18/12.90 | | | | | | | | | | | | | | | | (198) s_e(all_212_4, all_212_5, all_212_4, all_212_2) = % 91.18/12.90 | | | | | | | | | | | | | | | | all_452_0 % 91.18/12.90 | | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | | BETA: splitting (65) gives: % 91.18/12.90 | | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | | Case 1: % 91.18/12.90 | | | | | | | | | | | | | | | | | % 91.18/12.90 | | | | | | | | | | | | | | | | | (199) all_212_1 = all_212_3 % 91.18/12.90 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | REDUCE: (45), (199) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (200) $false % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | CLOSE: (200) is inconsistent. % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | Case 2: % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | (201) ? [v0: any] : ? [v1: any] : (s_m(all_212_3, % 91.18/12.91 | | | | | | | | | | | | | | | | | all_212_4, all_212_1) = v1 & s_col(all_212_3, % 91.18/12.91 | | | | | | | | | | | | | | | | | all_212_4, all_212_1) = v0 & ( ~ (v0 = 0) | v1 % 91.18/12.91 | | | | | | | | | | | | | | | | | = 0)) % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | DELTA: instantiating (201) with fresh symbols all_457_0, % 91.18/12.91 | | | | | | | | | | | | | | | | | all_457_1 gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (202) s_m(all_212_3, all_212_4, all_212_1) = all_457_0 & % 91.18/12.91 | | | | | | | | | | | | | | | | | s_col(all_212_3, all_212_4, all_212_1) = all_457_1 % 91.18/12.91 | | | | | | | | | | | | | | | | | & ( ~ (all_457_1 = 0) | all_457_0 = 0) % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | ALPHA: (202) implies: % 91.18/12.91 | | | | | | | | | | | | | | | | | (203) s_m(all_212_3, all_212_4, all_212_1) = all_457_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (36) with all_212_0, all_256_0, % 91.18/12.91 | | | | | | | | | | | | | | | | | all_212_1, all_212_2, all_212_3, all_212_5, % 91.18/12.91 | | | | | | | | | | | | | | | | | simplifying with (53), (114) gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (204) all_256_0 = all_212_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (36) with 0, all_452_0, all_212_2, % 91.18/12.91 | | | | | | | | | | | | | | | | | all_212_4, all_212_5, all_212_4, simplifying with % 91.18/12.91 | | | | | | | | | | | | | | | | | (61), (198) gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (205) all_452_0 = 0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (36) with 0, all_244_1, all_212_4, % 91.18/12.91 | | | | | | | | | | | | | | | | | all_212_2, all_212_4, all_212_2, simplifying with % 91.18/12.91 | | | | | | | | | | | | | | | | | (58), (110) gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (206) all_244_1 = 0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_277_0, all_292_0, % 91.18/12.91 | | | | | | | | | | | | | | | | | gamma, beta, alpha, simplifying with (131), (145) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (207) all_292_0 = all_277_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_208_2, all_302_1, % 91.18/12.91 | | | | | | | | | | | | | | | | | gamma, beta, alpha, simplifying with (41), (151) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (208) all_302_1 = all_208_2 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_277_0, all_302_1, % 91.18/12.91 | | | | | | | | | | | | | | | | | gamma, beta, alpha, simplifying with (131), (151) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (209) all_302_1 = all_277_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_272_1, all_302_1, % 91.18/12.91 | | | | | | | | | | | | | | | | | gamma, beta, alpha, simplifying with (126), (151) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (210) all_302_1 = all_272_1 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_292_0, all_322_1, % 91.18/12.91 | | | | | | | | | | | | | | | | | gamma, beta, alpha, simplifying with (145), (161) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (211) all_322_1 = all_292_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_267_0, all_322_1, % 91.18/12.91 | | | | | | | | | | | | | | | | | gamma, beta, alpha, simplifying with (119), (161) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (212) all_322_1 = all_267_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_337_0, all_362_0, % 91.18/12.91 | | | | | | | | | | | | | | | | | beta, gamma, alpha, simplifying with (177), (182) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (213) all_362_0 = all_337_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_287_0, all_362_0, % 91.18/12.91 | | | | | | | | | | | | | | | | | beta, gamma, alpha, simplifying with (140), (182) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (214) all_362_0 = all_287_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_208_0, all_292_1, % 91.18/12.91 | | | | | | | | | | | | | | | | | beta, alpha, gamma, simplifying with (43), (146) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (215) all_292_1 = all_208_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_292_1, all_317_0, % 91.18/12.91 | | | | | | | | | | | | | | | | | beta, alpha, gamma, simplifying with (146), (156) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (216) all_317_0 = all_292_1 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_327_1, all_332_0, % 91.18/12.91 | | | | | | | | | | | | | | | | | beta, alpha, gamma, simplifying with (166), (171) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (217) all_332_0 = all_327_1 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_317_0, all_332_0, % 91.18/12.91 | | | | | | | | | | | | | | | | | beta, alpha, gamma, simplifying with (156), (171) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (218) all_332_0 = all_317_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_277_1, all_332_0, % 91.18/12.91 | | | | | | | | | | | | | | | | | beta, alpha, gamma, simplifying with (132), (171) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (219) all_332_0 = all_277_1 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (33) with all_277_2, all_387_0, % 91.18/12.91 | | | | | | | | | | | | | | | | | alpha, gamma, beta, simplifying with (133), (188) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (220) all_387_0 = all_277_2 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (33) with all_387_0, all_437_2, % 91.18/12.91 | | | | | | | | | | | | | | | | | alpha, gamma, beta, simplifying with (188), (193) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (221) all_437_2 = all_387_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (33) with all_332_2, all_437_2, % 91.18/12.91 | | | | | | | | | | | | | | | | | alpha, gamma, beta, simplifying with (172), (193) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (222) all_437_2 = all_332_2 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (33) with all_267_2, all_437_2, % 91.18/12.91 | | | | | | | | | | | | | | | | | alpha, gamma, beta, simplifying with (120), (193) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (223) all_437_2 = all_267_2 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (34) with all_238_0, all_457_0, % 91.18/12.91 | | | | | | | | | | | | | | | | | all_212_1, all_212_4, all_212_3, simplifying with % 91.18/12.91 | | | | | | | | | | | | | | | | | (106), (203) gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (224) all_457_0 = all_238_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (34) with 0, all_457_0, all_212_1, % 91.18/12.91 | | | | | | | | | | | | | | | | | all_212_4, all_212_3, simplifying with (88), (203) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (225) all_457_0 = 0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (31) with all_222_0, all_224_0, % 91.18/12.91 | | | | | | | | | | | | | | | | | all_212_3, all_212_4, simplifying with (94), (97) % 91.18/12.91 | | | | | | | | | | | | | | | | | gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (226) all_224_0 = all_222_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (31) with all_226_0, all_228_0, % 91.18/12.91 | | | | | | | | | | | | | | | | | all_212_1, all_212_4, simplifying with (100), % 91.18/12.91 | | | | | | | | | | | | | | | | | (103) gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | (227) all_228_0 = all_226_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (224), (225) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (228) all_238_0 = 0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (222), (223) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (229) all_332_2 = all_267_2 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (221), (222) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (230) all_387_0 = all_332_2 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | SIMP: (230) implies: % 91.18/12.91 | | | | | | | | | | | | | | | | | (231) all_387_0 = all_332_2 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (220), (231) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (232) all_332_2 = all_277_2 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | SIMP: (232) implies: % 91.18/12.91 | | | | | | | | | | | | | | | | | (233) all_332_2 = all_277_2 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (213), (214) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (234) all_337_0 = all_287_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (217), (219) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (235) all_327_1 = all_277_1 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (217), (218) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (236) all_327_1 = all_317_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (229), (233) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (237) all_277_2 = all_267_2 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (235), (236) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (238) all_317_0 = all_277_1 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | SIMP: (238) implies: % 91.18/12.91 | | | | | | | | | | | | | | | | | (239) all_317_0 = all_277_1 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (211), (212) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (240) all_292_0 = all_267_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | SIMP: (240) implies: % 91.18/12.91 | | | | | | | | | | | | | | | | | (241) all_292_0 = all_267_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (216), (239) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (242) all_292_1 = all_277_1 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | SIMP: (242) implies: % 91.18/12.91 | | | | | | | | | | | | | | | | | (243) all_292_1 = all_277_1 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (209), (210) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (244) all_277_0 = all_272_1 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | SIMP: (244) implies: % 91.18/12.91 | | | | | | | | | | | | | | | | | (245) all_277_0 = all_272_1 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (208), (210) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (246) all_272_1 = all_208_2 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (207), (241) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (247) all_277_0 = all_267_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | SIMP: (247) implies: % 91.18/12.91 | | | | | | | | | | | | | | | | | (248) all_277_0 = all_267_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (215), (243) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (249) all_277_1 = all_208_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (245), (248) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (250) all_272_1 = all_267_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | SIMP: (250) implies: % 91.18/12.91 | | | | | | | | | | | | | | | | | (251) all_272_1 = all_267_0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (246), (251) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (252) all_267_0 = all_208_2 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | COMBINE_EQS: (248), (252) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (253) all_277_0 = all_208_2 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | REDUCE: (104), (227) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (254) s_r(all_212_2, all_212_4, all_226_0) = 0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | REDUCE: (98), (226) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (255) s_r(all_212_5, all_212_4, all_222_0) = 0 % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | REDUCE: (102), (227) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (256) $i(all_226_0) % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | REDUCE: (96), (226) imply: % 91.18/12.91 | | | | | | | | | | | | | | | | | (257) $i(all_222_0) % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | BETA: splitting (121) gives: % 91.18/12.91 | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | Case 1: % 91.18/12.91 | | | | | | | | | | | | | | | | | | % 91.18/12.91 | | | | | | | | | | | | | | | | | | (258) ~ (all_267_2 = 0) % 91.18/12.92 | | | | | | | | | | | | | | | | | | % 91.18/12.92 | | | | | | | | | | | | | | | | | | BETA: splitting (183) gives: % 91.18/12.92 | | | | | | | | | | | | | | | | | | % 91.18/12.92 | | | | | | | | | | | | | | | | | | Case 1: % 91.18/12.92 | | | | | | | | | | | | | | | | | | | % 91.18/12.92 | | | | | | | | | | | | | | | | | | | % 91.18/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (4) with all_212_5, all_212_3, % 91.18/12.92 | | | | | | | | | | | | | | | | | | | all_212_5, all_222_0, all_212_2, all_212_1, % 91.18/12.92 | | | | | | | | | | | | | | | | | | | all_212_0, simplifying with (47), (49), (50), % 91.18/12.92 | | | | | | | | | | | | | | | | | | | (51), (53), (93), (257) gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (259) all_212_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_e(all_212_5, all_222_0, all_212_2, all_212_1) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | = v0) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (5) with all_212_5, all_212_4, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_212_1, all_212_2, all_212_4, all_212_1, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | simplifying with (47), (48), (50), (51), (52), % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (62) gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (260) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (s_t(all_212_2, all_212_4, all_212_1) = v1 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_t(all_212_5, all_212_4, all_212_1) = v0 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_e(all_212_5, all_212_1, all_212_2, all_212_1) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (13) with all_212_5, all_212_4, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_212_1, all_212_2, all_212_4, all_212_1, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | simplifying with (47), (48), (50), (51), (61), % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (62) gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (261) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (sameside(all_212_2, all_212_4, all_212_1) = v1 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | sameside(all_212_5, all_212_4, all_212_1) = v0 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_e(all_212_5, all_212_1, all_212_2, all_212_1) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_212_2, all_212_2, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_212_4, all_212_5, all_212_5, all_212_4, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | simplifying with (47), (48), (50), (60) gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (262) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (s_t(all_212_2, all_212_2, all_212_4) = v0 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_t(all_212_5, all_212_5, all_212_4) = v1 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_e(all_212_2, all_212_2, all_212_5, all_212_5) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_212_5, all_212_2, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_212_4, all_212_2, all_212_2, all_212_4, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | simplifying with (47), (48), (50), (52), (58) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (263) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (s_t(all_212_2, all_212_2, all_212_4) = v1 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_t(all_212_5, all_212_2, all_212_4) = v0 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_e(all_212_5, all_212_2, all_212_2, all_212_2) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_212_2, all_212_5, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_212_4, all_212_2, all_212_2, all_212_4, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | simplifying with (47), (48), (50), (52), (58) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (264) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (s_t(all_212_2, all_212_2, all_212_4) = v1 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_t(all_212_2, all_212_5, all_212_4) = v0 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_e(all_212_2, all_212_5, all_212_2, all_212_2) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_212_2, all_212_2, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_212_4, all_212_2, all_212_2, all_212_4, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | simplifying with (48), (50), (58) gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (265) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (s_t(all_212_2, all_212_2, all_212_4) = v1 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_t(all_212_2, all_212_2, all_212_4) = v0 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_e(all_212_2, all_212_2, all_212_2, all_212_2) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_212_2, all_212_2, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_212_4, all_212_5, all_212_2, all_212_4, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | simplifying with (47), (48), (50), (58), (60) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (266) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (s_t(all_212_2, all_212_2, all_212_4) = v0 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_t(all_212_5, all_212_2, all_212_4) = v1 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_e(all_212_2, all_212_2, all_212_5, all_212_2) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (10) with all_212_2, all_212_2, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_212_4, all_212_2, all_212_5, all_212_4, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | simplifying with (47), (48), (50), (58), (60) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (267) ? [v0: any] : ? [v1: any] : ? [v2: any] : % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (s_t(all_212_2, all_212_2, all_212_4) = v0 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_t(all_212_2, all_212_5, all_212_4) = v1 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_e(all_212_2, all_212_2, all_212_2, all_212_5) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v2 = 0)) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (aSatz3_3) with all_212_2, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_212_4, all_254_1, simplifying with (48), (50), % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (112) gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (268) all_254_1 = 0 % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (18) with beta, gamma, alpha, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_267_2, simplifying with (9), (22), (23), (120) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (269) all_267_2 = 0 | gamma = beta | ? [v0: $i] : ? % 91.57/12.92 | | | | | | | | | | | | | | | | | | | [v1: $i] : (erectAux21a(beta, gamma, alpha) = v0 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | erect21a(beta, gamma, alpha) = v1 & s_t(alpha, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | v0, v1) = 0 & $i(v1) & $i(v0)) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (aSatz7_17) with all_212_3, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_212_4, all_212_1, all_220_0, simplifying with % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (48), (49), (51), (88), (90), (91) gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (270) all_220_0 = all_212_4 % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (aSatz7_6) with all_212_3, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_220_0, all_212_1, simplifying with (49), (51), % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (90), (91) gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (271) s(all_220_0, all_212_3) = all_212_1 % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (aSatz7_7) with all_212_4, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_212_1, all_226_0, simplifying with (48), (51), % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (100) gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (272) s(all_212_4, all_226_0) = all_212_1 % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (19) with all_212_5, all_212_4, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_222_0, all_212_2, simplifying with (47), (48), % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (50), (52), (255), (257) gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (273) ? [v0: any] : ? [v1: any] : (s_r(all_212_2, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_212_4, all_222_0) = v0 & s_e(all_212_5, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_222_0, all_212_2, all_222_0) = v1 & ( ~ % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (v0 = 0) | v1 = 0)) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (17) with all_212_2, all_212_4, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_226_0, simplifying with (48), (50), (254), % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (256) gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (274) ? [v0: $i] : (s_r(all_212_2, all_212_4, v0) = 0 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s(all_212_4, all_226_0) = v0 & $i(v0)) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (274) with fresh symbol all_525_0 % 91.57/12.92 | | | | | | | | | | | | | | | | | | | gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (275) s_r(all_212_2, all_212_4, all_525_0) = 0 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s(all_212_4, all_226_0) = all_525_0 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | $i(all_525_0) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | ALPHA: (275) implies: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (276) s(all_212_4, all_226_0) = all_525_0 % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (277) s_r(all_212_2, all_212_4, all_525_0) = 0 % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (273) with fresh symbols all_603_0, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_603_1 gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (278) s_r(all_212_2, all_212_4, all_222_0) = all_603_1 & % 91.57/12.92 | | | | | | | | | | | | | | | | | | | s_e(all_212_5, all_222_0, all_212_2, all_222_0) = % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_603_0 & ( ~ (all_603_1 = 0) | all_603_0 = 0) % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | ALPHA: (278) implies: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (279) s_e(all_212_5, all_222_0, all_212_2, all_222_0) = % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_603_0 % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (280) s_r(all_212_2, all_212_4, all_222_0) = all_603_1 % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (281) ~ (all_603_1 = 0) | all_603_0 = 0 % 91.57/12.92 | | | | | | | | | | | | | | | | | | | % 91.57/12.92 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (264) with fresh symbols all_1053_0, % 91.57/12.92 | | | | | | | | | | | | | | | | | | | all_1053_1, all_1053_2 gives: % 91.57/12.92 | | | | | | | | | | | | | | | | | | | (282) s_t(all_212_2, all_212_2, all_212_4) = all_1053_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | & s_t(all_212_2, all_212_5, all_212_4) = % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1053_2 & s_e(all_212_2, all_212_5, all_212_2, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_212_2) = all_1053_0 & ( ~ (all_1053_1 = 0) | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ~ (all_1053_2 = 0) | all_1053_0 = 0) % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ALPHA: (282) implies: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (283) s_t(all_212_2, all_212_2, all_212_4) = all_1053_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (263) with fresh symbols all_1055_0, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1055_1, all_1055_2 gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (284) s_t(all_212_2, all_212_2, all_212_4) = all_1055_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | & s_t(all_212_5, all_212_2, all_212_4) = % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1055_2 & s_e(all_212_5, all_212_2, all_212_2, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_212_2) = all_1055_0 & ( ~ (all_1055_1 = 0) | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ~ (all_1055_2 = 0) | all_1055_0 = 0) % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ALPHA: (284) implies: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (285) s_t(all_212_2, all_212_2, all_212_4) = all_1055_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (265) with fresh symbols all_1085_0, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1085_1, all_1085_2 gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (286) s_t(all_212_2, all_212_2, all_212_4) = all_1085_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | & s_t(all_212_2, all_212_2, all_212_4) = % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1085_2 & s_e(all_212_2, all_212_2, all_212_2, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_212_2) = all_1085_0 & ( ~ (all_1085_1 = 0) | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ~ (all_1085_2 = 0) | all_1085_0 = 0) % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ALPHA: (286) implies: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (287) s_t(all_212_2, all_212_2, all_212_4) = all_1085_2 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (288) s_t(all_212_2, all_212_2, all_212_4) = all_1085_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (289) ~ (all_1085_1 = 0) | ~ (all_1085_2 = 0) | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1085_0 = 0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (267) with fresh symbols all_1107_0, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1107_1, all_1107_2 gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (290) s_t(all_212_2, all_212_2, all_212_4) = all_1107_2 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | & s_t(all_212_2, all_212_5, all_212_4) = % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1107_1 & s_e(all_212_2, all_212_2, all_212_2, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_212_5) = all_1107_0 & ( ~ (all_1107_1 = 0) | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ~ (all_1107_2 = 0) | all_1107_0 = 0) % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ALPHA: (290) implies: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (291) s_t(all_212_2, all_212_2, all_212_4) = all_1107_2 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (266) with fresh symbols all_1109_0, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1109_1, all_1109_2 gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (292) s_t(all_212_2, all_212_2, all_212_4) = all_1109_2 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | & s_t(all_212_5, all_212_2, all_212_4) = % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1109_1 & s_e(all_212_2, all_212_2, all_212_5, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_212_2) = all_1109_0 & ( ~ (all_1109_1 = 0) | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ~ (all_1109_2 = 0) | all_1109_0 = 0) % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ALPHA: (292) implies: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (293) s_t(all_212_2, all_212_2, all_212_4) = all_1109_2 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (260) with fresh symbols all_1119_0, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1119_1, all_1119_2 gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (294) s_t(all_212_2, all_212_4, all_212_1) = all_1119_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | & s_t(all_212_5, all_212_4, all_212_1) = % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1119_2 & s_e(all_212_5, all_212_1, all_212_2, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_212_1) = all_1119_0 & ( ~ (all_1119_1 = 0) | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ~ (all_1119_2 = 0) | all_1119_0 = 0) % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ALPHA: (294) implies: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (295) s_e(all_212_5, all_212_1, all_212_2, all_212_1) = % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1119_0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (261) with fresh symbols all_1151_0, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1151_1, all_1151_2 gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (296) sameside(all_212_2, all_212_4, all_212_1) = % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1151_1 & sameside(all_212_5, all_212_4, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_212_1) = all_1151_2 & s_e(all_212_5, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_212_1, all_212_2, all_212_1) = all_1151_0 & % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ( ~ (all_1151_1 = 0) | ~ (all_1151_2 = 0) | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1151_0 = 0) % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ALPHA: (296) implies: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (297) s_e(all_212_5, all_212_1, all_212_2, all_212_1) = % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1151_0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (262) with fresh symbols all_1167_0, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1167_1, all_1167_2 gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (298) s_t(all_212_2, all_212_2, all_212_4) = all_1167_2 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | & s_t(all_212_5, all_212_5, all_212_4) = % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_1167_1 & s_e(all_212_2, all_212_2, all_212_5, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | all_212_5) = all_1167_0 & ( ~ (all_1167_1 = 0) | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ~ (all_1167_2 = 0) | all_1167_0 = 0) % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | ALPHA: (298) implies: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (299) s_t(all_212_2, all_212_2, all_212_4) = all_1167_2 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | REDUCE: (270), (271) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (300) s(all_212_4, all_212_3) = all_212_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | REDUCE: (112), (268) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | (301) s_t(all_212_2, all_212_2, all_212_4) = 0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | BETA: splitting (259) gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | Case 1: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | (302) all_212_0 = 0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | REDUCE: (46), (302) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | (303) $false % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | CLOSE: (303) is inconsistent. % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | Case 2: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | (304) ? [v0: int] : ( ~ (v0 = 0) & s_e(all_212_5, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | all_222_0, all_212_2, all_212_1) = v0) % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (304) with fresh symbol all_1243_0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | (305) ~ (all_1243_0 = 0) & s_e(all_212_5, all_222_0, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | all_212_2, all_212_1) = all_1243_0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | ALPHA: (305) implies: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | (306) ~ (all_1243_0 = 0) % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | (307) s_e(all_212_5, all_222_0, all_212_2, all_212_1) = % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | all_1243_0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | BETA: splitting (269) gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | Case 1: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | (308) gamma = beta % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | REDUCE: (8), (308) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | (309) $false % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | CLOSE: (309) is inconsistent. % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | Case 2: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | (310) all_267_2 = 0 | ? [v0: $i] : ? [v1: $i] : % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | (erectAux21a(beta, gamma, alpha) = v0 & % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | erect21a(beta, gamma, alpha) = v1 & s_t(alpha, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | v0, v1) = 0 & $i(v1) & $i(v0)) % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | BETA: splitting (310) gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | Case 1: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (311) all_267_2 = 0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (258), (311) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (312) $false % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | CLOSE: (312) is inconsistent. % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | Case 2: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (36) with all_242_0, all_1151_0, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | all_212_1, all_212_2, all_212_1, all_212_5, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | simplifying with (108), (297) gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (313) all_1151_0 = all_242_0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (36) with all_1119_0, all_1151_0, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | all_212_1, all_212_2, all_212_1, all_212_5, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | simplifying with (295), (297) gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (314) all_1151_0 = all_1119_0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_1085_2, all_1085_1, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | all_212_4, all_212_2, all_212_2, simplifying with % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (287), (288) gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (315) all_1085_1 = all_1085_2 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_1053_1, all_1085_1, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | all_212_4, all_212_2, all_212_2, simplifying with % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (283), (288) gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (316) all_1085_1 = all_1053_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with 0, all_1085_1, all_212_4, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | all_212_2, all_212_2, simplifying with (288), % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (301) gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (317) all_1085_1 = 0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_1085_1, all_1107_2, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | all_212_4, all_212_2, all_212_2, simplifying with % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (288), (291) gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (318) all_1107_2 = all_1085_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_1109_2, all_1167_2, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | all_212_4, all_212_2, all_212_2, simplifying with % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (293), (299) gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (319) all_1167_2 = all_1109_2 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_1107_2, all_1167_2, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | all_212_4, all_212_2, all_212_2, simplifying with % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (291), (299) gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (320) all_1167_2 = all_1107_2 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_1055_1, all_1167_2, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | all_212_4, all_212_2, all_212_2, simplifying with % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (285), (299) gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (321) all_1167_2 = all_1055_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (31) with all_222_0, all_212_1, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | all_212_3, all_212_4, simplifying with (94), (300) % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (322) all_222_0 = all_212_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (31) with all_212_1, all_525_0, % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | all_226_0, all_212_4, simplifying with (272), % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (276) gives: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (323) all_525_0 = all_212_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (319), (321) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (324) all_1109_2 = all_1055_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (319), (320) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (325) all_1109_2 = all_1107_2 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (313), (314) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (326) all_1119_0 = all_242_0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (324), (325) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (327) all_1107_2 = all_1055_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | SIMP: (327) implies: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (328) all_1107_2 = all_1055_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (318), (328) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (329) all_1085_1 = all_1055_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | SIMP: (329) implies: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (330) all_1085_1 = all_1055_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (315), (330) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (331) all_1085_2 = all_1055_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (315), (317) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (332) all_1085_2 = 0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (315), (316) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (333) all_1085_2 = all_1053_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (331), (332) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (334) all_1055_1 = 0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (331), (333) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (335) all_1055_1 = all_1053_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (334), (335) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (336) all_1053_1 = 0 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (280), (322) imply: % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | (337) s_r(all_212_2, all_212_4, all_212_1) = all_603_1 % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.93 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (279), (322) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | (338) s_e(all_212_5, all_212_1, all_212_2, all_212_1) = % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | all_603_0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (307), (322) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | (339) s_e(all_212_5, all_212_1, all_212_2, all_212_1) = % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | all_1243_0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (289) gives: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | Case 1: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | (340) ~ (all_1085_1 = 0) % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (317), (340) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | (341) $false % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (341) is inconsistent. % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | Case 2: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | (342) ~ (all_1085_2 = 0) | all_1085_0 = 0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (342) gives: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | (343) ~ (all_1085_2 = 0) % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (332), (343) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | (344) $false % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (344) is inconsistent. % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (36) with all_242_0, all_1243_0, % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | all_212_1, all_212_2, all_212_1, all_212_5, % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (108), (339) gives: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | (345) all_1243_0 = all_242_0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (36) with all_603_0, all_1243_0, % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | all_212_1, all_212_2, all_212_1, all_212_5, % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (338), (339) gives: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | (346) all_1243_0 = all_603_0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (35) with 0, all_603_1, all_212_1, % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | all_212_4, all_212_2, simplifying with (56), (337) % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | gives: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | (347) all_603_1 = 0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (345), (346) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | (348) all_603_0 = all_242_0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (348) implies: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | (349) all_603_0 = all_242_0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (306), (345) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | (350) ~ (all_242_0 = 0) % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (281) gives: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | (351) ~ (all_603_1 = 0) % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (347), (351) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | (352) $false % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (352) is inconsistent. % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | (353) all_603_0 = 0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (349), (353) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | (354) all_242_0 = 0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (350), (354) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | (355) $false % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (355) is inconsistent. % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | Case 2: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | (356) all_362_0 = 0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (214), (356) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | (357) all_287_0 = 0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | REDUCE: (139), (357) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | (358) $false % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | CLOSE: (358) is inconsistent. % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | Case 2: % 91.57/12.94 | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | (359) all_267_2 = 0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | COMBINE_EQS: (237), (359) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | (360) all_277_2 = 0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | BETA: splitting (134) gives: % 91.57/12.94 | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | Case 1: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | (361) ~ (all_277_2 = 0) % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | REDUCE: (360), (361) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | (362) $false % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | CLOSE: (362) is inconsistent. % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | Case 2: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | (363) all_277_0 = 0 | all_277_1 = 0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | BETA: splitting (363) gives: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | Case 1: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | (364) all_277_0 = 0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (253), (364) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | (365) all_208_2 = 0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | REDUCE: (38), (365) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | (366) $false % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | CLOSE: (366) is inconsistent. % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | Case 2: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | (367) all_277_1 = 0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (249), (367) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | (368) all_208_0 = 0 % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | REDUCE: (40), (368) imply: % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | (369) $false % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | CLOSE: (369) is inconsistent. % 91.57/12.94 | | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | | % 91.57/12.94 | | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | | % 91.57/12.94 | | | | | | | | | End of split % 91.57/12.94 | | | | | | | | | % 91.57/12.94 | | | | | | | | End of split % 91.57/12.94 | | | | | | | | % 91.57/12.94 | | | | | | | End of split % 91.57/12.94 | | | | | | | % 91.57/12.94 | | | | | | End of split % 91.57/12.94 | | | | | | % 91.57/12.94 | | | | | End of split % 91.57/12.94 | | | | | % 91.57/12.94 | | | | End of split % 91.57/12.94 | | | | % 91.57/12.94 | | | End of split % 91.57/12.94 | | | % 91.57/12.94 | | End of split % 91.57/12.94 | | % 91.57/12.94 | End of split % 91.57/12.94 | % 91.57/12.94 End of proof % 91.57/12.94 % SZS output end Proof for theBenchmark % 91.57/12.94 % 91.57/12.94 12355ms %------------------------------------------------------------------------------