%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : GEO513+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 : n001.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:33 EDT 2023 % Result : Theorem 67.32s 9.58s % Output : Proof 68.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : GEO513+1 : TPTP v8.1.2. Released v7.0.0. % 0.00/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n001.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Tue Aug 29 22:04:08 EDT 2023 % 0.13/0.35 % CPUTime : % 0.21/0.57 ________ _____ % 0.21/0.57 ___ __ \_________(_)________________________________ % 0.21/0.57 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.57 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.57 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.57 % 0.21/0.57 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.57 (2023-06-19) % 0.21/0.57 % 0.21/0.57 (c) Philipp Rümmer, 2009-2023 % 0.21/0.57 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.57 Amanda Stjerna. % 0.21/0.57 Free software under BSD-3-Clause. % 0.21/0.57 % 0.21/0.57 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.57 % 0.21/0.57 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.21/0.58 Running up to 7 provers in parallel. % 0.21/0.60 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.60 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.60 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.60 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.60 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.60 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.60 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 8.11/1.81 Prover 4: Preprocessing ... % 8.11/1.84 Prover 5: Preprocessing ... % 8.11/1.84 Prover 6: Preprocessing ... % 8.11/1.84 Prover 2: Preprocessing ... % 8.11/1.84 Prover 0: Preprocessing ... % 8.11/1.84 Prover 3: Preprocessing ... % 8.11/1.84 Prover 1: Preprocessing ... % 18.58/3.24 Prover 1: Warning: ignoring some quantifiers % 19.10/3.25 Prover 5: Proving ... % 19.10/3.25 Prover 2: Proving ... % 19.26/3.31 Prover 6: Proving ... % 19.66/3.33 Prover 3: Warning: ignoring some quantifiers % 19.88/3.35 Prover 1: Constructing countermodel ... % 19.88/3.38 Prover 3: Constructing countermodel ... % 23.62/3.93 Prover 4: Constructing countermodel ... % 24.33/3.97 Prover 0: Proving ... % 47.19/6.95 Prover 3: gave up % 47.45/6.96 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 49.66/7.27 Prover 7: Preprocessing ... % 51.28/7.48 Prover 7: Warning: ignoring some quantifiers % 51.28/7.55 Prover 7: Constructing countermodel ... % 67.32/9.56 Prover 4: Found proof (size 311) % 67.32/9.56 Prover 4: proved (8970ms) % 67.32/9.57 Prover 2: stopped % 67.32/9.57 Prover 5: stopped % 67.32/9.57 Prover 6: stopped % 67.32/9.57 Prover 1: stopped % 67.32/9.57 Prover 0: stopped % 67.32/9.58 Prover 7: stopped % 67.32/9.58 % 67.32/9.58 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 67.32/9.58 % 67.32/9.61 % SZS output start Proof for theBenchmark % 67.32/9.62 Assumptions after simplification: % 67.32/9.62 --------------------------------- % 67.32/9.62 % 67.32/9.62 (aA8) % 67.70/9.65 $i(gamma) & $i(beta) & $i(alpha) & ? [v0: int] : ? [v1: int] : ? [v2: int] % 67.70/9.65 : ( ~ (v2 = 0) & ~ (v1 = 0) & ~ (v0 = 0) & s_t(gamma, alpha, beta) = v2 & % 67.70/9.65 s_t(beta, gamma, alpha) = v1 & s_t(alpha, beta, gamma) = v0) % 67.70/9.65 % 67.70/9.65 (aExtCol2) % 67.70/9.66 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 67.70/9.66 int] : (v5 = 0 | v3 = v2 | v1 = v0 | ~ (s_col(v2, v3, v4) = 0) | ~ % 67.70/9.66 (s_col(v0, v1, v4) = v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 67.70/9.66 ~ $i(v0) | ? [v6: any] : ? [v7: any] : (s_col(v0, v1, v3) = v7 & s_col(v0, % 67.70/9.66 v1, v2) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0)))) & ! [v0: $i] : ! [v1: $i] % 67.70/9.66 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: int] : (v5 = 0 | v3 = v2 | % 67.70/9.66 v1 = v0 | ~ (s_col(v0, v1, v4) = v5) | ~ (s_col(v0, v1, v3) = 0) | ~ % 67.70/9.66 (s_col(v0, v1, v2) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 67.70/9.66 $i(v0) | ? [v6: int] : ( ~ (v6 = 0) & s_col(v2, v3, v4) = v6)) & ! [v0: % 67.70/9.66 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v3 = v2 | v1 % 67.70/9.66 = v0 | ~ (s_col(v2, v3, v4) = 0) | ~ (s_col(v0, v1, v3) = 0) | ~ $i(v4) | % 67.70/9.66 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] % 67.70/9.66 : (s_col(v0, v1, v4) = v6 & s_col(v0, v1, v2) = v5 & ( ~ (v5 = 0) | v6 = % 67.70/9.66 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 67.70/9.66 $i] : (v3 = v2 | v1 = v0 | ~ (s_col(v2, v3, v4) = 0) | ~ (s_col(v0, v1, % 67.70/9.66 v2) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 67.70/9.66 ? [v5: any] : ? [v6: any] : (s_col(v0, v1, v4) = v6 & s_col(v0, v1, v3) = % 67.70/9.66 v5 & ( ~ (v5 = 0) | v6 = 0))) % 67.70/9.66 % 67.70/9.66 (aExtSameSide1) % 67.70/9.66 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: % 67.70/9.66 int] : ( ~ (v5 = 0) & ~ (v2 = v0) & ~ (v1 = v0) & samesideline(v3, v4, v0, % 67.70/9.66 v2) = v5 & samesideline(v3, v4, v0, v1) = 0 & s_col(v0, v1, v2) = 0 & % 67.70/9.66 $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 67.70/9.66 % 67.70/9.66 (aSatz3_13b) % 67.70/9.66 ~ (gamma = beta) & $i(gamma) & $i(beta) % 67.70/9.66 % 67.70/9.66 (aSatz3_2) % 67.70/9.67 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_t(v2, % 67.70/9.67 v1, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ % 67.70/9.67 (v4 = 0) & s_t(v0, v1, v2) = v4)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 67.70/9.67 $i] : ( ~ (s_t(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 67.70/9.67 s_t(v2, v1, v0) = 0) % 67.70/9.67 % 67.70/9.67 (aSatz4_11a) % 67.70/9.67 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 67.70/9.67 (s_col(v1, v2, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] % 67.70/9.67 : ( ~ (v4 = 0) & s_col(v0, v1, v2) = v4)) & ! [v0: $i] : ! [v1: $i] : ! % 67.70/9.67 [v2: $i] : ( ~ (s_col(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 67.70/9.67 s_col(v1, v2, v0) = 0) % 67.70/9.67 % 67.70/9.67 (aSatz4_11b) % 67.70/9.67 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 67.70/9.67 (s_col(v2, v0, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] % 67.70/9.67 : ( ~ (v4 = 0) & s_col(v0, v1, v2) = v4)) & ! [v0: $i] : ! [v1: $i] : ! % 67.70/9.67 [v2: $i] : ( ~ (s_col(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 67.70/9.67 s_col(v2, v0, v1) = 0) % 67.70/9.67 % 67.70/9.67 (aSatz4_11c) % 67.70/9.67 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 67.70/9.67 (s_col(v2, v1, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] % 67.70/9.67 : ( ~ (v4 = 0) & s_col(v0, v1, v2) = v4)) & ! [v0: $i] : ! [v1: $i] : ! % 67.70/9.67 [v2: $i] : ( ~ (s_col(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 67.70/9.67 s_col(v2, v1, v0) = 0) % 67.70/9.67 % 67.70/9.67 (aSatz4_11e) % 67.92/9.67 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 67.92/9.67 (s_col(v0, v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] % 67.92/9.67 : ( ~ (v4 = 0) & s_col(v0, v1, v2) = v4)) & ! [v0: $i] : ! [v1: $i] : ! % 67.92/9.67 [v2: $i] : ( ~ (s_col(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 67.92/9.67 s_col(v0, v2, v1) = 0) % 67.92/9.67 % 67.92/9.67 (aSatz6_16b) % 67.92/9.68 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 67.92/9.68 | v2 = v0 | v1 = v0 | ~ (s_col(v0, v2, v3) = v4) | ~ (s_col(v0, v1, v3) = % 67.92/9.68 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ( ~ % 67.92/9.68 (v5 = 0) & s_col(v0, v1, v2) = v5)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 67.92/9.68 $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | v2 = v0 | v1 = v0 | ~ % 67.92/9.68 (s_col(v0, v2, v3) = v4) | ~ (s_col(v0, v1, v2) = 0) | ~ $i(v3) | ~ % 67.92/9.68 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ( ~ (v5 = 0) & s_col(v0, v1, % 67.92/9.68 v3) = v5)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v2 % 67.92/9.68 = v0 | v1 = v0 | ~ (s_col(v0, v1, v3) = 0) | ~ (s_col(v0, v1, v2) = 0) | % 67.92/9.68 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | s_col(v0, v2, v3) = 0) % 67.92/9.68 % 67.92/9.68 (aSatz6_18) % 67.92/9.68 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 67.92/9.68 int] : (v5 = 0 | v3 = v2 | v1 = v0 | ~ (s_col(v2, v3, v4) = 0) | ~ % 67.92/9.68 (s_col(v0, v1, v4) = v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 67.92/9.68 ~ $i(v0) | ? [v6: any] : ? [v7: any] : (s_col(v2, v3, v1) = v7 & s_col(v2, % 67.92/9.68 v3, v0) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0)))) & ! [v0: $i] : ! [v1: $i] % 67.92/9.68 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: int] : (v5 = 0 | v3 = v2 | % 67.92/9.68 v1 = v0 | ~ (s_col(v2, v3, v1) = 0) | ~ (s_col(v0, v1, v4) = v5) | ~ % 67.92/9.68 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? % 67.92/9.68 [v7: any] : (s_col(v2, v3, v4) = v7 & s_col(v2, v3, v0) = v6 & ( ~ (v7 = 0) % 67.92/9.68 | ~ (v6 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 67.92/9.68 : ! [v4: $i] : ! [v5: int] : (v5 = 0 | v3 = v2 | v1 = v0 | ~ (s_col(v2, v3, % 67.92/9.68 v0) = 0) | ~ (s_col(v0, v1, v4) = v5) | ~ $i(v4) | ~ $i(v3) | ~ % 67.92/9.68 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : (s_col(v2, % 67.92/9.68 v3, v4) = v7 & s_col(v2, v3, v1) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0)))) & % 67.92/9.68 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v3 = v2 % 67.92/9.68 | v1 = v0 | ~ (s_col(v2, v3, v4) = 0) | ~ (s_col(v2, v3, v1) = 0) | ~ % 67.92/9.68 (s_col(v2, v3, v0) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 67.92/9.68 $i(v0) | s_col(v0, v1, v4) = 0) % 67.92/9.68 % 67.92/9.68 (aSatz7_21) % 67.92/9.69 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 67.92/9.69 int] : (v5 = 0 | v3 = v1 | ~ (s_m(v0, v4, v2) = v5) | ~ (s_col(v1, v4, v3) % 67.92/9.69 = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: % 67.92/9.69 any] : ? [v7: any] : ? [v8: any] : ? [v9: any] : (s_col(v0, v4, v2) = % 67.92/9.69 v9 & s_col(v0, v1, v2) = v6 & s_e(v1, v2, v3, v0) = v8 & s_e(v0, v1, v2, % 67.92/9.69 v3) = v7 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0) | v6 = 0))) & ! % 67.92/9.70 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 67.92/9.70 int] : (v5 = 0 | v3 = v1 | ~ (s_m(v0, v4, v2) = v5) | ~ (s_e(v1, v2, v3, % 67.92/9.70 v0) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 67.92/9.70 ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: any] : (s_col(v1, v4, % 67.92/9.70 v3) = v9 & s_col(v0, v4, v2) = v8 & s_col(v0, v1, v2) = v6 & s_e(v0, v1, % 67.92/9.70 v2, v3) = v7 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0) | v6 = 0))) & ! % 67.92/9.70 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 67.92/9.70 int] : (v5 = 0 | v3 = v1 | ~ (s_m(v0, v4, v2) = v5) | ~ (s_e(v0, v1, v2, % 67.92/9.70 v3) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 67.92/9.70 ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: any] : (s_col(v1, v4, % 67.92/9.70 v3) = v9 & s_col(v0, v4, v2) = v8 & s_col(v0, v1, v2) = v6 & s_e(v1, v2, % 67.92/9.70 v3, v0) = v7 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v7 = 0) | v6 = 0))) & ! % 67.92/9.70 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 67.92/9.70 int] : (v5 = 0 | v3 = v1 | ~ (s_col(v1, v4, v3) = 0) | ~ (s_col(v0, v1, % 67.92/9.70 v2) = v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 67.92/9.70 ? [v6: any] : ? [v7: any] : ? [v8: any] : ? [v9: any] : (s_m(v0, v4, v2) % 67.92/9.70 = v9 & s_col(v0, v4, v2) = v8 & s_e(v1, v2, v3, v0) = v7 & s_e(v0, v1, v2, % 67.92/9.70 v3) = v6 & ( ~ (v8 = 0) | ~ (v7 = 0) | ~ (v6 = 0) | v9 = 0))) & ! % 67.92/9.70 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v3 = v1 | % 67.92/9.70 ~ (s_col(v1, v4, v3) = 0) | ~ (s_col(v0, v4, v2) = 0) | ~ $i(v4) | ~ % 67.92/9.70 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : % 67.92/9.70 ? [v7: any] : ? [v8: any] : (s_m(v0, v4, v2) = v8 & s_col(v0, v1, v2) = v5 % 67.92/9.70 & s_e(v1, v2, v3, v0) = v7 & s_e(v0, v1, v2, v3) = v6 & ( ~ (v7 = 0) | ~ % 67.92/9.70 (v6 = 0) | v8 = 0 | v5 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 67.92/9.70 : ! [v3: $i] : ! [v4: $i] : (v3 = v1 | ~ (s_col(v1, v4, v3) = 0) | ~ % 67.92/9.70 (s_e(v1, v2, v3, v0) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 67.92/9.70 ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : % 67.92/9.70 (s_m(v0, v4, v2) = v8 & s_col(v0, v4, v2) = v7 & s_col(v0, v1, v2) = v5 & % 67.92/9.70 s_e(v0, v1, v2, v3) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0) | v8 = 0 | v5 = 0))) % 67.92/9.70 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v3 = % 67.92/9.70 v1 | ~ (s_col(v1, v4, v3) = 0) | ~ (s_e(v0, v1, v2, v3) = 0) | ~ $i(v4) | % 67.92/9.70 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] % 67.92/9.70 : ? [v7: any] : ? [v8: any] : (s_m(v0, v4, v2) = v8 & s_col(v0, v4, v2) = % 67.92/9.70 v7 & s_col(v0, v1, v2) = v5 & s_e(v1, v2, v3, v0) = v6 & ( ~ (v7 = 0) | ~ % 67.92/9.70 (v6 = 0) | v8 = 0 | v5 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 67.92/9.70 : ! [v3: $i] : ! [v4: $i] : (v3 = v1 | ~ (s_col(v0, v4, v2) = 0) | ~ % 67.92/9.70 (s_e(v1, v2, v3, v0) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 67.92/9.70 ~ $i(v0) | ? [v5: any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : % 67.92/9.70 (s_m(v0, v4, v2) = v8 & s_col(v1, v4, v3) = v7 & s_col(v0, v1, v2) = v5 & % 67.92/9.70 s_e(v0, v1, v2, v3) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0) | v8 = 0 | v5 = 0))) % 67.92/9.70 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v3 = % 67.92/9.70 v1 | ~ (s_col(v0, v4, v2) = 0) | ~ (s_e(v0, v1, v2, v3) = 0) | ~ $i(v4) | % 67.92/9.70 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] % 67.92/9.70 : ? [v7: any] : ? [v8: any] : (s_m(v0, v4, v2) = v8 & s_col(v1, v4, v3) = % 67.92/9.70 v7 & s_col(v0, v1, v2) = v5 & s_e(v1, v2, v3, v0) = v6 & ( ~ (v7 = 0) | ~ % 67.92/9.70 (v6 = 0) | v8 = 0 | v5 = 0))) % 67.92/9.70 % 67.92/9.70 (aext1) % 67.92/9.70 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 67.92/9.70 | v1 = v0 | ~ (s_col(v0, v2, v3) = v4) | ~ (s_col(v0, v1, v3) = 0) | ~ % 67.92/9.70 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: int] : ( ~ (v5 = 0) & % 67.92/9.70 s_col(v0, v1, v2) = v5)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 67.92/9.70 [v3: $i] : ! [v4: int] : (v4 = 0 | v1 = v0 | ~ (s_col(v0, v2, v3) = v4) | ~ % 67.92/9.70 (s_col(v0, v1, v2) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 67.92/9.70 [v5: int] : ( ~ (v5 = 0) & s_col(v0, v1, v3) = v5)) & ! [v0: $i] : ! [v1: % 67.92/9.70 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (s_col(v0, v1, v3) = 0) | ~ % 67.92/9.70 (s_col(v0, v1, v2) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 67.92/9.70 s_col(v0, v2, v3) = 0) % 67.92/9.70 % 67.92/9.70 (d_Defn6_1) % 67.92/9.71 $i(xb) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | v2 % 67.92/9.71 = v1 | v1 = v0 | ~ (sameside(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 67.92/9.71 $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_t(v1, v2, v0) = v4)) & ! [v0: $i] % 67.92/9.71 : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | v1 = v0 | v1 = xb | ~ % 67.92/9.71 (sameside(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 67.92/9.71 int] : ( ~ (v4 = 0) & s_t(v1, v0, v2) = v4)) & ! [v0: $i] : ! [v1: $i] : % 67.92/9.71 ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_t(v1, v2, v0) = v3) | ~ $i(v2) | % 67.92/9.71 ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : (sameside(v0, v1, v2) % 67.92/9.71 = v4 & s_t(v1, v0, v2) = v5 & ( ~ (v4 = 0) | v5 = 0))) & ! [v0: $i] : ! % 67.92/9.71 [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_t(v1, v0, v2) = v3) | % 67.92/9.71 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : % 67.92/9.71 (sameside(v0, v1, v2) = v4 & s_t(v1, v2, v0) = v5 & ( ~ (v4 = 0) | v5 = 0))) % 67.92/9.71 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | v1 = v0 | ~ (s_t(v1, % 67.92/9.71 v2, v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | sameside(v0, v1, v2) % 67.92/9.71 = 0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | v1 = xb | ~ % 67.92/9.71 (s_t(v1, v0, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | sameside(v0, v1, % 67.92/9.71 v2) = 0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sameside(v0, v1, % 67.92/9.71 v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 67.92/9.71 any] : (s_t(v1, v2, v0) = v4 & s_t(v1, v0, v2) = v3 & (v4 = 0 | v3 = 0))) % 67.92/9.71 & ! [v0: $i] : ! [v1: $i] : ( ~ (sameside(v0, v1, v1) = 0) | ~ $i(v1) | ~ % 67.92/9.71 $i(v0)) & ! [v0: $i] : ! [v1: $i] : ( ~ (sameside(v0, v0, v1) = 0) | ~ % 67.92/9.71 $i(v1) | ~ $i(v0)) % 67.92/9.71 % 67.92/9.71 (d_Defn9_7) % 67.92/9.74 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 67.92/9.74 $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 | v6 = v5 | v6 = v1 | v5 = v4 | % 67.92/9.74 v4 = v0 | v3 = v2 | ~ (samesideline(v0, v1, v2, v3) = v7) | ~ (s_col(v2, % 67.92/9.74 v3, v6) = 0) | ~ (s_t(v0, v4, v5) = 0) | ~ $i(v6) | ~ $i(v5) | ~ % 67.92/9.74 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v8: any] : ? % 67.92/9.74 [v9: any] : ? [v10: any] : ? [v11: any] : (s_col(v2, v3, v4) = v9 & % 67.92/9.74 s_col(v2, v3, v1) = v11 & s_col(v2, v3, v0) = v10 & s_t(v1, v6, v5) = v8 & % 67.92/9.74 ( ~ (v9 = 0) | ~ (v8 = 0) | v11 = 0 | v10 = 0))) & ! [v0: $i] : ! [v1: % 67.92/9.74 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : % 67.92/9.74 ! [v7: int] : (v7 = 0 | v6 = v5 | v6 = v1 | v5 = v4 | v4 = v0 | v3 = v2 | ~ % 67.92/9.74 (samesideline(v0, v1, v2, v3) = v7) | ~ (s_col(v2, v3, v4) = 0) | ~ % 67.92/9.74 (s_t(v1, v6, v5) = 0) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 67.92/9.74 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v8: any] : ? [v9: any] : ? [v10: any] % 67.92/9.74 : ? [v11: any] : (s_col(v2, v3, v6) = v9 & s_col(v2, v3, v1) = v11 & % 67.92/9.74 s_col(v2, v3, v0) = v10 & s_t(v0, v4, v5) = v8 & ( ~ (v9 = 0) | ~ (v8 = % 67.92/9.74 0) | v11 = 0 | v10 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 67.92/9.74 ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 % 67.92/9.74 | v6 = v5 | v6 = v1 | v5 = v4 | v4 = v0 | v3 = v2 | ~ (samesideline(v0, v1, % 67.92/9.74 v2, v3) = v7) | ~ (s_t(v1, v6, v5) = 0) | ~ (s_t(v0, v4, v5) = 0) | ~ % 67.92/9.74 $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 67.92/9.74 $i(v0) | ? [v8: any] : ? [v9: any] : ? [v10: any] : ? [v11: any] : % 67.92/9.74 (s_col(v2, v3, v6) = v9 & s_col(v2, v3, v4) = v8 & s_col(v2, v3, v1) = v11 & % 67.92/9.74 s_col(v2, v3, v0) = v10 & ( ~ (v9 = 0) | ~ (v8 = 0) | v11 = 0 | v10 = % 67.92/9.74 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 67.92/9.74 $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 | v6 = v5 | v6 = v1 % 67.92/9.74 | v5 = v4 | v4 = v0 | v3 = v2 | ~ (s_col(v2, v3, v6) = 0) | ~ (s_col(v2, % 67.92/9.74 v3, v1) = v7) | ~ (s_t(v0, v4, v5) = 0) | ~ $i(v6) | ~ $i(v5) | ~ % 67.92/9.74 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v8: any] : ? % 67.92/9.74 [v9: any] : ? [v10: any] : ? [v11: any] : (samesideline(v0, v1, v2, v3) = % 67.92/9.74 v11 & s_col(v2, v3, v4) = v9 & s_col(v2, v3, v0) = v10 & s_t(v1, v6, v5) = % 67.92/9.74 v8 & ( ~ (v9 = 0) | ~ (v8 = 0) | v11 = 0 | v10 = 0))) & ! [v0: $i] : ! % 67.92/9.74 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] % 67.92/9.74 : ! [v7: int] : (v7 = 0 | v6 = v5 | v6 = v1 | v5 = v4 | v4 = v0 | v3 = v2 | % 67.92/9.74 ~ (s_col(v2, v3, v4) = 0) | ~ (s_col(v2, v3, v0) = v7) | ~ (s_t(v1, v6, % 67.92/9.74 v5) = 0) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 67.92/9.74 ~ $i(v1) | ~ $i(v0) | ? [v8: any] : ? [v9: any] : ? [v10: any] : ? % 67.92/9.74 [v11: any] : (samesideline(v0, v1, v2, v3) = v11 & s_col(v2, v3, v6) = v9 & % 67.92/9.74 s_col(v2, v3, v1) = v10 & s_t(v0, v4, v5) = v8 & ( ~ (v9 = 0) | ~ (v8 = % 67.92/9.74 0) | v11 = 0 | v10 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 67.92/9.74 ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 % 67.92/9.74 | v6 = v5 | v6 = v1 | v5 = v4 | v4 = v0 | v3 = v2 | ~ (s_col(v2, v3, v1) = % 67.92/9.74 v7) | ~ (s_t(v1, v6, v5) = 0) | ~ (s_t(v0, v4, v5) = 0) | ~ $i(v6) | ~ % 67.92/9.74 $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v8: % 67.92/9.74 any] : ? [v9: any] : ? [v10: any] : ? [v11: any] : (samesideline(v0, % 67.92/9.74 v1, v2, v3) = v11 & s_col(v2, v3, v6) = v9 & s_col(v2, v3, v4) = v8 & % 67.92/9.74 s_col(v2, v3, v0) = v10 & ( ~ (v9 = 0) | ~ (v8 = 0) | v11 = 0 | v10 = % 67.92/9.74 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 67.92/9.74 $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 | v6 = v5 | v6 = v1 % 67.92/9.74 | v5 = v4 | v4 = v0 | v3 = v2 | ~ (s_col(v2, v3, v0) = v7) | ~ (s_t(v1, % 67.92/9.74 v6, v5) = 0) | ~ (s_t(v0, v4, v5) = 0) | ~ $i(v6) | ~ $i(v5) | ~ % 67.92/9.74 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v8: any] : ? % 67.92/9.74 [v9: any] : ? [v10: any] : ? [v11: any] : (samesideline(v0, v1, v2, v3) = % 67.92/9.74 v11 & s_col(v2, v3, v6) = v9 & s_col(v2, v3, v4) = v8 & s_col(v2, v3, v1) % 67.92/9.74 = v10 & ( ~ (v9 = 0) | ~ (v8 = 0) | v11 = 0 | v10 = 0))) & ! [v0: $i] : % 67.92/9.74 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: % 67.92/9.74 $i] : (v6 = v5 | v6 = v1 | v5 = v4 | v4 = v0 | v3 = v2 | ~ (s_col(v2, v3, % 67.92/9.74 v6) = 0) | ~ (s_t(v1, v6, v5) = 0) | ~ (s_t(v0, v4, v5) = 0) | ~ % 67.92/9.74 $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 67.92/9.74 $i(v0) | ? [v7: any] : ? [v8: any] : ? [v9: any] : ? [v10: any] : % 67.92/9.74 (samesideline(v0, v1, v2, v3) = v10 & s_col(v2, v3, v4) = v7 & s_col(v2, v3, % 67.92/9.74 v1) = v9 & s_col(v2, v3, v0) = v8 & ( ~ (v7 = 0) | v10 = 0 | v9 = 0 | v8 % 67.92/9.74 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 67.92/9.74 $i] : ! [v5: $i] : ! [v6: $i] : (v6 = v5 | v6 = v1 | v5 = v4 | v4 = v0 | % 67.92/9.74 v3 = v2 | ~ (s_col(v2, v3, v4) = 0) | ~ (s_t(v1, v6, v5) = 0) | ~ % 67.92/9.74 (s_t(v0, v4, v5) = 0) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 67.92/9.74 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v7: any] : ? [v8: any] : ? [v9: any] % 67.92/9.74 : ? [v10: any] : (samesideline(v0, v1, v2, v3) = v10 & s_col(v2, v3, v6) = % 67.92/9.74 v7 & s_col(v2, v3, v1) = v9 & s_col(v2, v3, v0) = v8 & ( ~ (v7 = 0) | v10 % 67.92/9.74 = 0 | v9 = 0 | v8 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 67.92/9.74 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: int] : (v6 = 0 | ~ (ss3(v0, % 67.92/9.74 v1, v2, v3) = v5) | ~ (ss2(v0, v1, v2, v3) = v4) | ~ (s_t(v1, v4, v5) % 67.92/9.74 = v6) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v7: int] : ( ~ % 67.92/9.74 (v7 = 0) & samesideline(v0, v1, v2, v3) = v7)) & ! [v0: $i] : ! [v1: $i] % 67.92/9.74 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: int] : (v6 = % 67.92/9.74 0 | ~ (ss3(v0, v1, v2, v3) = v5) | ~ (ss1(v0, v1, v2, v3) = v4) | ~ % 67.92/9.74 (s_t(v0, v4, v5) = v6) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 67.92/9.74 [v7: int] : ( ~ (v7 = 0) & samesideline(v0, v1, v2, v3) = v7)) & ! [v0: $i] % 67.92/9.74 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: int] : (v5 = % 67.92/9.74 0 | ~ (ss2(v0, v1, v2, v3) = v4) | ~ (s_col(v2, v3, v4) = v5) | ~ $i(v3) % 67.92/9.74 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: int] : ( ~ (v6 = 0) & % 67.92/9.74 samesideline(v0, v1, v2, v3) = v6)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 67.92/9.74 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: int] : (v5 = 0 | ~ (ss1(v0, v1, % 67.92/9.74 v2, v3) = v4) | ~ (s_col(v2, v3, v4) = v5) | ~ $i(v3) | ~ $i(v2) | ~ % 67.92/9.74 $i(v1) | ~ $i(v0) | ? [v6: int] : ( ~ (v6 = 0) & samesideline(v0, v1, v2, % 67.92/9.74 v3) = v6)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 67.92/9.74 [v4: $i] : ( ~ (ss3(v0, v1, v2, v3) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 67.92/9.74 | ~ $i(v0) | ? [v5: any] : ? [v6: $i] : (ss2(v0, v1, v2, v3) = v6 & % 67.92/9.74 samesideline(v0, v1, v2, v3) = v5 & $i(v6) & ( ~ (v6 = v4) | ~ (v5 = % 67.92/9.74 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 67.92/9.74 [v4: $i] : ( ~ (ss3(v0, v1, v2, v3) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 67.92/9.74 | ~ $i(v0) | ? [v5: any] : ? [v6: $i] : (ss1(v0, v1, v2, v3) = v6 & % 67.92/9.74 samesideline(v0, v1, v2, v3) = v5 & $i(v6) & ( ~ (v6 = v4) | ~ (v5 = % 68.26/9.74 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 68.26/9.74 [v4: $i] : ( ~ (ss2(v0, v1, v2, v3) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 68.26/9.74 | ~ $i(v0) | ? [v5: any] : ? [v6: $i] : (ss3(v0, v1, v2, v3) = v6 & % 68.26/9.74 samesideline(v0, v1, v2, v3) = v5 & $i(v6) & ( ~ (v6 = v4) | ~ (v5 = % 68.26/9.74 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 68.26/9.74 [v4: $i] : ( ~ (ss1(v0, v1, v2, v3) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 68.26/9.74 | ~ $i(v0) | ? [v5: any] : ? [v6: $i] : (ss3(v0, v1, v2, v3) = v6 & % 68.26/9.74 samesideline(v0, v1, v2, v3) = v5 & $i(v6) & ( ~ (v6 = v4) | ~ (v5 = % 68.26/9.74 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 68.26/9.74 (ss2(v0, v1, v2, v3) = v1) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 68.26/9.74 ? [v4: int] : ( ~ (v4 = 0) & samesideline(v0, v1, v2, v3) = v4)) & ! [v0: % 68.26/9.74 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (ss1(v0, v1, v2, v3) = % 68.26/9.74 v0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ % 68.26/9.74 (v4 = 0) & samesideline(v0, v1, v2, v3) = v4)) & ! [v0: $i] : ! [v1: $i] % 68.26/9.74 : ! [v2: $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, v2, v3) = 0) | ~ % 68.26/9.74 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : ( ~ % 68.26/9.74 (v5 = v4) & ss3(v0, v1, v2, v3) = v4 & ss2(v0, v1, v2, v3) = v5 & $i(v5) & % 68.26/9.74 $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 68.26/9.74 (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 68.26/9.74 $i(v0) | ? [v4: $i] : ? [v5: $i] : ( ~ (v5 = v4) & ss3(v0, v1, v2, v3) = % 68.26/9.74 v4 & ss1(v0, v1, v2, v3) = v5 & $i(v5) & $i(v4))) & ! [v0: $i] : ! [v1: % 68.26/9.74 $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, v2, v3) = 0) | % 68.26/9.74 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : % 68.26/9.74 (ss3(v0, v1, v2, v3) = v5 & ss2(v0, v1, v2, v3) = v4 & s_t(v1, v4, v5) = 0 & % 68.26/9.74 $i(v5) & $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 68.26/9.74 : ( ~ (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 68.26/9.74 ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : (ss3(v0, v1, v2, v3) = v5 & ss1(v0, % 68.26/9.74 v1, v2, v3) = v4 & s_t(v0, v4, v5) = 0 & $i(v5) & $i(v4))) & ! [v0: $i] % 68.26/9.74 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, v2, v3) % 68.26/9.74 = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ( ~ % 68.26/9.74 (v4 = v1) & ss2(v0, v1, v2, v3) = v4 & $i(v4))) & ! [v0: $i] : ! [v1: % 68.26/9.74 $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, v2, v3) = 0) | % 68.26/9.74 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ( ~ (v4 = v0) & % 68.26/9.74 ss1(v0, v1, v2, v3) = v4 & $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 68.26/9.74 $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ % 68.26/9.74 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_col(v2, v3, % 68.26/9.74 v1) = v4)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 68.26/9.74 (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 68.26/9.74 $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_col(v2, v3, v0) = v4)) & ! [v0: % 68.26/9.74 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, % 68.26/9.74 v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 68.26/9.74 $i] : (ss2(v0, v1, v2, v3) = v4 & s_col(v2, v3, v4) = 0 & $i(v4))) & ! % 68.26/9.74 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, % 68.26/9.74 v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 68.26/9.74 $i] : (ss1(v0, v1, v2, v3) = v4 & s_col(v2, v3, v4) = 0 & $i(v4))) & ! % 68.26/9.74 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (samesideline(v0, v1, v2, v2) = 0) % 68.26/9.74 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0)) % 68.26/9.74 % 68.26/9.74 (d_insert) % 68.26/9.74 $i(gamma) & $i(alpha) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 68.26/9.74 : ! [v4: $i] : ! [v5: $i] : ( ~ (ext(v4, v2, v0, v1) = v5) | ~ (ext(v3, v2, % 68.26/9.74 alpha, gamma) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 68.26/9.74 (insert(v0, v1, v2, v3) = v5 & $i(v5))) & ! [v0: $i] : ! [v1: $i] : ! % 68.26/9.74 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (insert(v0, v1, v2, v3) = v4) | ~ % 68.26/9.74 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (ext(v5, v2, v0, % 68.26/9.74 v1) = v4 & ext(v3, v2, alpha, gamma) = v5 & $i(v5) & $i(v4))) % 68.26/9.74 % 68.26/9.74 (function-axioms) % 68.26/9.76 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 68.26/9.76 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] % 68.26/9.76 : ! [v9: $i] : (v1 = v0 | ~ (s_afs(v9, v8, v7, v6, v5, v4, v3, v2) = v1) | % 68.26/9.76 ~ (s_afs(v9, v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] % 68.26/9.76 : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 68.26/9.76 [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : (v1 = v0 | % 68.26/9.76 ~ (s_fs(v9, v8, v7, v6, v5, v4, v3, v2) = v1) | ~ (s_fs(v9, v8, v7, v6, v5, % 68.26/9.76 v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 68.26/9.76 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 68.26/9.76 ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : (v1 = v0 | ~ % 68.26/9.76 (s_ifs(v9, v8, v7, v6, v5, v4, v3, v2) = v1) | ~ (s_ifs(v9, v8, v7, v6, v5, % 68.26/9.76 v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 68.26/9.76 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 68.26/9.76 ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : (v1 = v0 | ~ (s_kf(v8, v7, v6, v5, % 68.26/9.76 v4, v3, v2) = v1) | ~ (s_kf(v8, v7, v6, v5, v4, v3, v2) = v0)) & ! % 68.26/9.76 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 68.26/9.76 $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : (v1 = v0 | ~ % 68.26/9.76 (s_e3(v7, v6, v5, v4, v3, v2) = v1) | ~ (s_e3(v7, v6, v5, v4, v3, v2) = % 68.26/9.76 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 68.26/9.76 : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : (v1 = v0 | ~ (crossbar(v7, v6, % 68.26/9.76 v5, v4, v3, v2) = v1) | ~ (crossbar(v7, v6, v5, v4, v3, v2) = v0)) & ! % 68.26/9.76 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 68.26/9.76 : ! [v6: $i] : (v1 = v0 | ~ (g811(v6, v5, v4, v3, v2) = v1) | ~ (g811(v6, % 68.26/9.76 v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 68.26/9.76 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (f811(v6, % 68.26/9.76 v5, v4, v3, v2) = v1) | ~ (f811(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 68.26/9.76 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 68.26/9.76 ! [v6: $i] : (v1 = v0 | ~ (midpointAux(v6, v5, v4, v3, v2) = v1) | ~ % 68.26/9.76 (midpointAux(v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 68.26/9.76 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | % 68.26/9.76 ~ (g813(v6, v5, v4, v3, v2) = v1) | ~ (g813(v6, v5, v4, v3, v2) = v0)) & ! % 68.26/9.76 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 68.26/9.76 : ! [v6: $i] : (v1 = v0 | ~ (f813(v6, v5, v4, v3, v2) = v1) | ~ (f813(v6, % 68.26/9.76 v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 68.26/9.76 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 68.26/9.76 ! [v6: $i] : (v1 = v0 | ~ (perpAt(v6, v5, v4, v3, v2) = v1) | ~ (perpAt(v6, % 68.26/9.76 v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 68.26/9.76 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ % 68.26/9.76 (insert5(v6, v5, v4, v3, v2) = v1) | ~ (insert5(v6, v5, v4, v3, v2) = v0)) % 68.26/9.76 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 68.26/9.76 [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (ip(v6, v5, v4, v3, v2) = v1) | ~ % 68.26/9.76 (ip(v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 68.26/9.76 ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (ss3(v5, v4, v3, v2) = % 68.26/9.76 v1) | ~ (ss3(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 68.26/9.76 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (ss2(v5, v4, % 68.26/9.76 v3, v2) = v1) | ~ (ss2(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 68.26/9.76 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 68.26/9.76 (ss1(v5, v4, v3, v2) = v1) | ~ (ss1(v5, v4, v3, v2) = v0)) & ! [v0: % 68.26/9.76 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 68.26/9.76 : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (samesideline(v5, v4, v3, v2) = % 68.26/9.76 v1) | ~ (samesideline(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] % 68.26/9.76 : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 68.26/9.76 [v5: $i] : (v1 = v0 | ~ (opposite(v5, v4, v3, v2) = v1) | ~ (opposite(v5, % 68.26/9.76 v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 68.26/9.76 $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (il(v5, v4, v3, v2) = v1) | % 68.26/9.76 ~ (il(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 68.26/9.76 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 68.26/9.76 (v1 = v0 | ~ (perp(v5, v4, v3, v2) = v1) | ~ (perp(v5, v4, v3, v2) = v0)) & % 68.26/9.76 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 68.26/9.76 $i] : (v1 = v0 | ~ (ins(v5, v4, v3, v2) = v1) | ~ (ins(v5, v4, v3, v2) = % 68.26/9.76 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 68.26/9.76 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (le(v5, v4, % 68.26/9.76 v3, v2) = v1) | ~ (le(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 68.26/9.76 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 68.26/9.76 (insert(v5, v4, v3, v2) = v1) | ~ (insert(v5, v4, v3, v2) = v0)) & ! [v0: % 68.26/9.76 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 68.26/9.76 (v1 = v0 | ~ (ext(v5, v4, v3, v2) = v1) | ~ (ext(v5, v4, v3, v2) = v0)) & ! % 68.26/9.76 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 68.26/9.76 $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (s_e(v5, v4, v3, v2) = v1) | % 68.26/9.76 ~ (s_e(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 68.26/9.76 ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (erectAux(v4, v3, v2) = v1) | ~ % 68.26/9.76 (erectAux(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 68.26/9.76 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (erect(v4, v3, v2) = v1) | ~ % 68.26/9.76 (erect(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 68.26/9.76 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (erectAux21a(v4, v3, v2) = v1) | ~ % 68.26/9.76 (erectAux21a(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 68.26/9.76 ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (erect21a(v4, v3, v2) = v1) | ~ % 68.26/9.76 (erect21a(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 68.26/9.76 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (foot(v4, v3, v2) = v1) | ~ (foot(v4, % 68.26/9.76 v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 68.26/9.76 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (s_r(v4, v3, v2) = % 68.26/9.76 v1) | ~ (s_r(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 68.26/9.76 : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (isomidpoint(v4, v3, v2) = v1) | % 68.26/9.76 ~ (isomidpoint(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 68.26/9.76 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 68.26/9.76 (s_m(v4, v3, v2) = v1) | ~ (s_m(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 68.26/9.76 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (c63(v4, v3, % 68.26/9.76 v2) = v1) | ~ (c63(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 68.26/9.76 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 68.26/9.76 ~ (sameside(v4, v3, v2) = v1) | ~ (sameside(v4, v3, v2) = v0)) & ! [v0: % 68.26/9.76 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 68.26/9.76 : ! [v4: $i] : (v1 = v0 | ~ (s_col(v4, v3, v2) = v1) | ~ (s_col(v4, v3, v2) % 68.26/9.76 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 68.26/9.76 $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (s_t(v4, v3, v2) = v1) | ~ % 68.26/9.76 (s_t(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 68.26/9.76 $i] : (v1 = v0 | ~ (midpoint(v3, v2) = v1) | ~ (midpoint(v3, v2) = v0)) & % 68.26/9.76 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (s(v3, % 68.26/9.76 v2) = v1) | ~ (s(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 68.26/9.76 $i] : ! [v3: $i] : (v1 = v0 | ~ (pointOffLine(v3, v2) = v1) | ~ % 68.26/9.76 (pointOffLine(v3, v2) = v0)) % 68.26/9.76 % 68.26/9.76 Further assumptions not needed in the proof: % 68.26/9.76 -------------------------------------------- % 68.26/9.76 aA1, aA2, aA3, aA4, aA5, aA6, aA7, aA9, aExtPerp, aExtPerp2, aExtPerp3, % 68.26/9.76 aExtPerp4, aExtPerp5, aExtPerp6, aNarbouxLemma1, aSatz2_1, aSatz2_11, aSatz2_12, % 68.26/9.76 aSatz2_13, aSatz2_14, aSatz2_15, aSatz2_2, aSatz2_3, aSatz2_4, aSatz2_5, % 68.26/9.76 aSatz2_8, aSatz3_1, aSatz3_13a, aSatz3_13c, aSatz3_14a, aSatz3_14b, aSatz3_17, % 68.26/9.76 aSatz3_3, aSatz3_4, aSatz3_5a, aSatz3_5b, aSatz3_6a, aSatz3_6b, aSatz3_7a, % 68.26/9.76 aSatz3_7b, aSatz4_11d, aSatz4_12, aSatz4_12b, aSatz4_13, aSatz4_14, aSatz4_16, % 68.26/9.76 aSatz4_17, aSatz4_18, aSatz4_19, aSatz4_2, aSatz4_3, aSatz4_5, aSatz4_6, % 68.26/9.76 aSatz5_1, aSatz5_10, aSatz5_11, aSatz5_12a1, aSatz5_12a2, aSatz5_12b, aSatz5_2, % 68.26/9.76 aSatz5_3, aSatz5_5a, aSatz5_5b, aSatz5_6, aSatz5_7, aSatz5_8, aSatz5_9, % 68.26/9.76 aSatz6_11a, aSatz6_11b, aSatz6_13a, aSatz6_13b, aSatz6_15a, aSatz6_15b, % 68.26/9.76 aSatz6_15c, aSatz6_15d, aSatz6_16a, aSatz6_17a, aSatz6_17b, aSatz6_21, % 68.26/9.76 aSatz6_25, aSatz6_28, aSatz6_2a, aSatz6_2b, aSatz6_3a, aSatz6_3b, aSatz6_4a, % 68.26/9.76 aSatz6_4b, aSatz6_5, aSatz6_6, aSatz6_7, aSatz7_10a, aSatz7_10b, aSatz7_13, % 68.26/9.76 aSatz7_15a, aSatz7_15b, aSatz7_16a, aSatz7_16b, aSatz7_17, aSatz7_18, aSatz7_19, % 68.26/9.76 aSatz7_2, aSatz7_20, aSatz7_22, aSatz7_22a, aSatz7_22b, aSatz7_25, aSatz7_3a, % 68.26/9.76 aSatz7_3b, aSatz7_4a, aSatz7_4b, aSatz7_6, aSatz7_7, aSatz7_8, aSatz7_9, % 68.26/9.76 aSatz8_10, aSatz8_12a, aSatz8_12b, aSatz8_13a, aSatz8_13b, aSatz8_14a, % 68.26/9.76 aSatz8_14b, aSatz8_14c, aSatz8_15, aSatz8_16a, aSatz8_16b, aSatz8_18, % 68.26/9.76 aSatz8_18a, aSatz8_2, aSatz8_20a, aSatz8_20b, aSatz8_21, aSatz8_21a, aSatz8_22, % 68.26/9.76 aSatz8_22b, aSatz8_24, aSatz8_24a, aSatz8_24b, aSatz8_3, aSatz8_4, aSatz8_5, % 68.26/9.76 aSatz8_6, aSatz8_7, aSatz8_8, aSatz8_9, aperp1, d_Defn2_10, d_Defn4_1, % 68.26/9.76 d_Defn4_10, d_Defn4_15, d_Defn4_4, d_Defn5_4, d_Defn7_1, d_Defn7_23, d_Defn8_1, % 68.26/9.76 d_Defn8_11a, d_Defn8_11b, d_Defn9_1 % 68.26/9.76 % 68.26/9.76 Those formulas are unsatisfiable: % 68.26/9.76 --------------------------------- % 68.26/9.76 % 68.26/9.76 Begin of proof % 68.26/9.76 | % 68.26/9.76 | ALPHA: (aA8) implies: % 68.26/9.76 | (1) ? [v0: int] : ? [v1: int] : ? [v2: int] : ( ~ (v2 = 0) & ~ (v1 = 0) % 68.26/9.76 | & ~ (v0 = 0) & s_t(gamma, alpha, beta) = v2 & s_t(beta, gamma, % 68.26/9.76 | alpha) = v1 & s_t(alpha, beta, gamma) = v0) % 68.26/9.76 | % 68.26/9.76 | ALPHA: (aSatz3_2) implies: % 68.26/9.76 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 68.26/9.76 | (s_t(v2, v1, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 68.26/9.76 | int] : ( ~ (v4 = 0) & s_t(v0, v1, v2) = v4)) % 68.26/9.76 | % 68.26/9.76 | ALPHA: (aSatz3_13b) implies: % 68.26/9.76 | (3) $i(beta) % 68.26/9.76 | % 68.26/9.76 | ALPHA: (aSatz4_11a) implies: % 68.26/9.76 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_col(v0, v1, v2) = 0) | % 68.26/9.76 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | s_col(v1, v2, v0) = 0) % 68.26/9.76 | % 68.26/9.76 | ALPHA: (aSatz4_11b) implies: % 68.37/9.76 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_col(v0, v1, v2) = 0) | % 68.37/9.76 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | s_col(v2, v0, v1) = 0) % 68.37/9.76 | % 68.37/9.76 | ALPHA: (aSatz4_11c) implies: % 68.37/9.76 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_col(v0, v1, v2) = 0) | % 68.37/9.76 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | s_col(v2, v1, v0) = 0) % 68.37/9.76 | % 68.37/9.76 | ALPHA: (aSatz4_11e) implies: % 68.37/9.77 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_col(v0, v1, v2) = 0) | % 68.37/9.77 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | s_col(v0, v2, v1) = 0) % 68.37/9.77 | % 68.37/9.77 | ALPHA: (aSatz6_16b) implies: % 68.37/9.77 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : % 68.37/9.77 | (v4 = 0 | v2 = v0 | v1 = v0 | ~ (s_col(v0, v2, v3) = v4) | ~ % 68.37/9.77 | (s_col(v0, v1, v2) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 68.37/9.77 | $i(v0) | ? [v5: int] : ( ~ (v5 = 0) & s_col(v0, v1, v3) = v5)) % 68.37/9.77 | % 68.37/9.77 | ALPHA: (aSatz6_18) implies: % 68.37/9.77 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 68.37/9.77 | ! [v5: int] : (v5 = 0 | v3 = v2 | v1 = v0 | ~ (s_col(v2, v3, v1) = 0) % 68.37/9.77 | | ~ (s_col(v0, v1, v4) = v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 68.37/9.77 | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : (s_col(v2, v3, % 68.37/9.77 | v4) = v7 & s_col(v2, v3, v0) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0)))) % 68.37/9.77 | % 68.37/9.77 | ALPHA: (aSatz7_21) implies: % 68.37/9.77 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 68.37/9.77 | (v3 = v1 | ~ (s_col(v1, v4, v3) = 0) | ~ (s_col(v0, v4, v2) = 0) | % 68.37/9.77 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: % 68.37/9.77 | any] : ? [v6: any] : ? [v7: any] : ? [v8: any] : (s_m(v0, v4, % 68.37/9.77 | v2) = v8 & s_col(v0, v1, v2) = v5 & s_e(v1, v2, v3, v0) = v7 & % 68.37/9.77 | s_e(v0, v1, v2, v3) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0) | v8 = 0 | % 68.37/9.77 | v5 = 0))) % 68.37/9.77 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 68.37/9.77 | ! [v5: int] : (v5 = 0 | v3 = v1 | ~ (s_col(v1, v4, v3) = 0) | ~ % 68.37/9.77 | (s_col(v0, v1, v2) = v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 68.37/9.77 | $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : ? [v8: any] : ? % 68.37/9.77 | [v9: any] : (s_m(v0, v4, v2) = v9 & s_col(v0, v4, v2) = v8 & s_e(v1, % 68.37/9.77 | v2, v3, v0) = v7 & s_e(v0, v1, v2, v3) = v6 & ( ~ (v8 = 0) | ~ % 68.37/9.77 | (v7 = 0) | ~ (v6 = 0) | v9 = 0))) % 68.37/9.77 | % 68.37/9.77 | ALPHA: (aExtCol2) implies: % 68.37/9.77 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 68.37/9.77 | (v3 = v2 | v1 = v0 | ~ (s_col(v2, v3, v4) = 0) | ~ (s_col(v0, v1, % 68.37/9.77 | v3) = 0) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 68.37/9.77 | $i(v0) | ? [v5: any] : ? [v6: any] : (s_col(v0, v1, v4) = v6 & % 68.37/9.77 | s_col(v0, v1, v2) = v5 & ( ~ (v5 = 0) | v6 = 0))) % 68.37/9.77 | % 68.37/9.77 | ALPHA: (aext1) implies: % 68.37/9.77 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 68.37/9.77 | (s_col(v0, v1, v3) = 0) | ~ (s_col(v0, v1, v2) = 0) | ~ $i(v3) | % 68.37/9.77 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | s_col(v0, v2, v3) = 0) % 68.37/9.77 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : % 68.37/9.77 | (v4 = 0 | v1 = v0 | ~ (s_col(v0, v2, v3) = v4) | ~ (s_col(v0, v1, % 68.37/9.77 | v2) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 68.37/9.77 | [v5: int] : ( ~ (v5 = 0) & s_col(v0, v1, v3) = v5)) % 68.37/9.77 | % 68.37/9.77 | ALPHA: (d_insert) implies: % 68.37/9.77 | (15) $i(alpha) % 68.37/9.77 | (16) $i(gamma) % 68.37/9.77 | % 68.37/9.77 | ALPHA: (d_Defn6_1) implies: % 68.37/9.77 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 68.37/9.77 | (s_t(v1, v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 68.37/9.77 | any] : ? [v5: any] : (sameside(v0, v1, v2) = v4 & s_t(v1, v2, v0) % 68.37/9.77 | = v5 & ( ~ (v4 = 0) | v5 = 0))) % 68.37/9.77 | (18) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 68.37/9.77 | (s_t(v1, v2, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 68.37/9.77 | any] : ? [v5: any] : (sameside(v0, v1, v2) = v4 & s_t(v1, v0, v2) % 68.37/9.77 | = v5 & ( ~ (v4 = 0) | v5 = 0))) % 68.37/9.77 | % 68.37/9.77 | ALPHA: (d_Defn9_7) implies: % 68.37/9.78 | (19) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 68.37/9.78 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 68.37/9.78 | $i(v1) | ~ $i(v0) | ? [v4: $i] : (ss1(v0, v1, v2, v3) = v4 & % 68.37/9.78 | s_col(v2, v3, v4) = 0 & $i(v4))) % 68.37/9.78 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 68.37/9.78 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 68.37/9.78 | $i(v1) | ~ $i(v0) | ? [v4: $i] : (ss2(v0, v1, v2, v3) = v4 & % 68.37/9.78 | s_col(v2, v3, v4) = 0 & $i(v4))) % 68.37/9.78 | (21) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 68.37/9.78 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 68.37/9.78 | $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_col(v2, v3, v0) % 68.37/9.78 | = v4)) % 68.37/9.78 | (22) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 68.37/9.78 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 68.37/9.78 | $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_col(v2, v3, v1) % 68.37/9.78 | = v4)) % 68.37/9.78 | (23) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 68.37/9.78 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 68.37/9.78 | $i(v1) | ~ $i(v0) | ? [v4: $i] : ( ~ (v4 = v0) & ss1(v0, v1, v2, % 68.37/9.78 | v3) = v4 & $i(v4))) % 68.37/9.78 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 68.37/9.78 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 68.37/9.78 | $i(v1) | ~ $i(v0) | ? [v4: $i] : ( ~ (v4 = v1) & ss2(v0, v1, v2, % 68.37/9.78 | v3) = v4 & $i(v4))) % 68.37/9.78 | (25) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 68.37/9.78 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 68.37/9.78 | $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : (ss3(v0, v1, v2, % 68.37/9.78 | v3) = v5 & ss1(v0, v1, v2, v3) = v4 & s_t(v0, v4, v5) = 0 & % 68.37/9.78 | $i(v5) & $i(v4))) % 68.37/9.78 | (26) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 68.37/9.78 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 68.37/9.78 | $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : (ss3(v0, v1, v2, % 68.37/9.78 | v3) = v5 & ss2(v0, v1, v2, v3) = v4 & s_t(v1, v4, v5) = 0 & % 68.37/9.78 | $i(v5) & $i(v4))) % 68.37/9.78 | (27) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 68.37/9.78 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 68.37/9.78 | $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : ( ~ (v5 = v4) & % 68.37/9.78 | ss3(v0, v1, v2, v3) = v4 & ss1(v0, v1, v2, v3) = v5 & $i(v5) & % 68.37/9.78 | $i(v4))) % 68.37/9.78 | (28) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 68.37/9.78 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 68.37/9.78 | $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : ( ~ (v5 = v4) & % 68.37/9.78 | ss3(v0, v1, v2, v3) = v4 & ss2(v0, v1, v2, v3) = v5 & $i(v5) & % 68.37/9.78 | $i(v4))) % 68.37/9.78 | (29) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 68.37/9.78 | ! [v5: $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 | v6 = v5 | v6 = v1 % 68.37/9.78 | | v5 = v4 | v4 = v0 | v3 = v2 | ~ (s_col(v2, v3, v1) = v7) | ~ % 68.37/9.78 | (s_t(v1, v6, v5) = 0) | ~ (s_t(v0, v4, v5) = 0) | ~ $i(v6) | ~ % 68.37/9.78 | $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 68.37/9.78 | ? [v8: any] : ? [v9: any] : ? [v10: any] : ? [v11: any] : % 68.37/9.78 | (samesideline(v0, v1, v2, v3) = v11 & s_col(v2, v3, v6) = v9 & % 68.37/9.78 | s_col(v2, v3, v4) = v8 & s_col(v2, v3, v0) = v10 & ( ~ (v9 = 0) | % 68.37/9.78 | ~ (v8 = 0) | v11 = 0 | v10 = 0))) % 68.37/9.78 | (30) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 68.37/9.78 | ! [v5: $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 | v6 = v5 | v6 = v1 % 68.37/9.78 | | v5 = v4 | v4 = v0 | v3 = v2 | ~ (samesideline(v0, v1, v2, v3) = % 68.37/9.78 | v7) | ~ (s_t(v1, v6, v5) = 0) | ~ (s_t(v0, v4, v5) = 0) | ~ % 68.37/9.78 | $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 68.37/9.78 | ~ $i(v0) | ? [v8: any] : ? [v9: any] : ? [v10: any] : ? [v11: % 68.37/9.78 | any] : (s_col(v2, v3, v6) = v9 & s_col(v2, v3, v4) = v8 & % 68.37/9.78 | s_col(v2, v3, v1) = v11 & s_col(v2, v3, v0) = v10 & ( ~ (v9 = 0) | % 68.37/9.78 | ~ (v8 = 0) | v11 = 0 | v10 = 0))) % 68.37/9.78 | % 68.37/9.78 | ALPHA: (function-axioms) implies: % 68.37/9.79 | (31) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 68.37/9.79 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (s_t(v4, v3, v2) = v1) | % 68.37/9.79 | ~ (s_t(v4, v3, v2) = v0)) % 68.37/9.79 | (32) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 68.37/9.79 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (s_col(v4, v3, v2) = v1) | % 68.37/9.79 | ~ (s_col(v4, v3, v2) = v0)) % 68.37/9.79 | (33) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 68.37/9.79 | ! [v5: $i] : (v1 = v0 | ~ (ss1(v5, v4, v3, v2) = v1) | ~ (ss1(v5, % 68.37/9.79 | v4, v3, v2) = v0)) % 68.37/9.79 | (34) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 68.37/9.79 | ! [v5: $i] : (v1 = v0 | ~ (ss2(v5, v4, v3, v2) = v1) | ~ (ss2(v5, % 68.37/9.79 | v4, v3, v2) = v0)) % 68.37/9.79 | (35) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 68.37/9.79 | ! [v5: $i] : (v1 = v0 | ~ (ss3(v5, v4, v3, v2) = v1) | ~ (ss3(v5, % 68.37/9.79 | v4, v3, v2) = v0)) % 68.37/9.79 | % 68.37/9.79 | DELTA: instantiating (1) with fresh symbols all_171_0, all_171_1, all_171_2 % 68.37/9.79 | gives: % 68.37/9.79 | (36) ~ (all_171_0 = 0) & ~ (all_171_1 = 0) & ~ (all_171_2 = 0) & % 68.37/9.79 | s_t(gamma, alpha, beta) = all_171_0 & s_t(beta, gamma, alpha) = % 68.37/9.79 | all_171_1 & s_t(alpha, beta, gamma) = all_171_2 % 68.37/9.79 | % 68.37/9.79 | ALPHA: (36) implies: % 68.37/9.79 | (37) ~ (all_171_1 = 0) % 68.37/9.79 | (38) ~ (all_171_0 = 0) % 68.37/9.79 | (39) s_t(beta, gamma, alpha) = all_171_1 % 68.37/9.79 | (40) s_t(gamma, alpha, beta) = all_171_0 % 68.37/9.79 | % 68.37/9.79 | DELTA: instantiating (aExtSameSide1) with fresh symbols all_175_0, all_175_1, % 68.37/9.79 | all_175_2, all_175_3, all_175_4, all_175_5 gives: % 68.37/9.79 | (41) ~ (all_175_0 = 0) & ~ (all_175_3 = all_175_5) & ~ (all_175_4 = % 68.37/9.79 | all_175_5) & samesideline(all_175_2, all_175_1, all_175_5, % 68.37/9.79 | all_175_3) = all_175_0 & samesideline(all_175_2, all_175_1, % 68.37/9.79 | all_175_5, all_175_4) = 0 & s_col(all_175_5, all_175_4, all_175_3) = % 68.37/9.79 | 0 & $i(all_175_1) & $i(all_175_2) & $i(all_175_3) & $i(all_175_4) & % 68.37/9.79 | $i(all_175_5) % 68.37/9.79 | % 68.37/9.79 | ALPHA: (41) implies: % 68.37/9.79 | (42) ~ (all_175_4 = all_175_5) % 68.37/9.79 | (43) ~ (all_175_3 = all_175_5) % 68.37/9.79 | (44) ~ (all_175_0 = 0) % 68.37/9.79 | (45) $i(all_175_5) % 68.37/9.79 | (46) $i(all_175_4) % 68.37/9.79 | (47) $i(all_175_3) % 68.37/9.79 | (48) $i(all_175_2) % 68.37/9.79 | (49) $i(all_175_1) % 68.37/9.79 | (50) s_col(all_175_5, all_175_4, all_175_3) = 0 % 68.37/9.79 | (51) samesideline(all_175_2, all_175_1, all_175_5, all_175_4) = 0 % 68.37/9.79 | (52) samesideline(all_175_2, all_175_1, all_175_5, all_175_3) = all_175_0 % 68.37/9.79 | % 68.37/9.79 | GROUND_INST: instantiating (18) with alpha, beta, gamma, all_171_1, % 68.37/9.79 | simplifying with (3), (15), (16), (39) gives: % 68.37/9.79 | (53) all_171_1 = 0 | ? [v0: any] : ? [v1: any] : (sameside(alpha, beta, % 68.37/9.79 | gamma) = v0 & s_t(beta, alpha, gamma) = v1 & ( ~ (v0 = 0) | v1 = % 68.37/9.79 | 0)) % 68.37/9.79 | % 68.37/9.79 | GROUND_INST: instantiating (17) with gamma, beta, alpha, all_171_1, % 68.37/9.79 | simplifying with (3), (15), (16), (39) gives: % 68.37/9.79 | (54) all_171_1 = 0 | ? [v0: any] : ? [v1: any] : (sameside(gamma, beta, % 68.37/9.79 | alpha) = v0 & s_t(beta, alpha, gamma) = v1 & ( ~ (v0 = 0) | v1 = % 68.37/9.79 | 0)) % 68.37/9.79 | % 68.37/9.79 | GROUND_INST: instantiating (2) with beta, alpha, gamma, all_171_0, simplifying % 68.37/9.79 | with (3), (15), (16), (40) gives: % 68.37/9.79 | (55) all_171_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & s_t(beta, alpha, gamma) % 68.37/9.79 | = v0) % 68.37/9.79 | % 68.37/9.79 | GROUND_INST: instantiating (10) with all_175_5, all_175_5, all_175_3, % 68.37/9.79 | all_175_3, all_175_4, simplifying with (45), (46), (47), (50) % 68.37/9.79 | gives: % 68.37/9.79 | (56) all_175_3 = all_175_5 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 68.37/9.79 | ? [v3: any] : (s_m(all_175_5, all_175_4, all_175_3) = v3 & % 68.37/9.79 | s_col(all_175_5, all_175_5, all_175_3) = v0 & s_e(all_175_5, % 68.37/9.79 | all_175_3, all_175_3, all_175_5) = v2 & s_e(all_175_5, all_175_5, % 68.37/9.79 | all_175_3, all_175_3) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0) | v3 = 0 | % 68.37/9.79 | v0 = 0)) % 68.37/9.79 | % 68.37/9.79 | GROUND_INST: instantiating (6) with all_175_5, all_175_4, all_175_3, % 68.37/9.79 | simplifying with (45), (46), (47), (50) gives: % 68.37/9.79 | (57) s_col(all_175_3, all_175_4, all_175_5) = 0 % 68.37/9.79 | % 68.37/9.79 | GROUND_INST: instantiating (5) with all_175_5, all_175_4, all_175_3, % 68.37/9.79 | simplifying with (45), (46), (47), (50) gives: % 68.37/9.79 | (58) s_col(all_175_3, all_175_5, all_175_4) = 0 % 68.37/9.79 | % 68.37/9.79 | GROUND_INST: instantiating (4) with all_175_5, all_175_4, all_175_3, % 68.37/9.79 | simplifying with (45), (46), (47), (50) gives: % 68.37/9.79 | (59) s_col(all_175_4, all_175_3, all_175_5) = 0 % 68.37/9.79 | % 68.37/9.79 | GROUND_INST: instantiating (7) with all_175_5, all_175_4, all_175_3, % 68.37/9.79 | simplifying with (45), (46), (47), (50) gives: % 68.37/9.79 | (60) s_col(all_175_5, all_175_3, all_175_4) = 0 % 68.37/9.79 | % 68.37/9.80 | GROUND_INST: instantiating (28) with all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4, simplifying with (45), (46), (48), (49), (51) gives: % 68.37/9.80 | (61) ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = v0) & ss3(all_175_2, all_175_1, % 68.37/9.80 | all_175_5, all_175_4) = v0 & ss2(all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4) = v1 & $i(v1) & $i(v0)) % 68.37/9.80 | % 68.37/9.80 | GROUND_INST: instantiating (27) with all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4, simplifying with (45), (46), (48), (49), (51) gives: % 68.37/9.80 | (62) ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = v0) & ss3(all_175_2, all_175_1, % 68.37/9.80 | all_175_5, all_175_4) = v0 & ss1(all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4) = v1 & $i(v1) & $i(v0)) % 68.37/9.80 | % 68.37/9.80 | GROUND_INST: instantiating (26) with all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4, simplifying with (45), (46), (48), (49), (51) gives: % 68.37/9.80 | (63) ? [v0: $i] : ? [v1: $i] : (ss3(all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4) = v1 & ss2(all_175_2, all_175_1, all_175_5, all_175_4) % 68.37/9.80 | = v0 & s_t(all_175_1, v0, v1) = 0 & $i(v1) & $i(v0)) % 68.37/9.80 | % 68.37/9.80 | GROUND_INST: instantiating (25) with all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4, simplifying with (45), (46), (48), (49), (51) gives: % 68.37/9.80 | (64) ? [v0: $i] : ? [v1: $i] : (ss3(all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4) = v1 & ss1(all_175_2, all_175_1, all_175_5, all_175_4) % 68.37/9.80 | = v0 & s_t(all_175_2, v0, v1) = 0 & $i(v1) & $i(v0)) % 68.37/9.80 | % 68.37/9.80 | GROUND_INST: instantiating (24) with all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4, simplifying with (45), (46), (48), (49), (51) gives: % 68.37/9.80 | (65) ? [v0: any] : ( ~ (v0 = all_175_1) & ss2(all_175_2, all_175_1, % 68.37/9.80 | all_175_5, all_175_4) = v0 & $i(v0)) % 68.37/9.80 | % 68.37/9.80 | GROUND_INST: instantiating (23) with all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4, simplifying with (45), (46), (48), (49), (51) gives: % 68.37/9.80 | (66) ? [v0: any] : ( ~ (v0 = all_175_2) & ss1(all_175_2, all_175_1, % 68.37/9.80 | all_175_5, all_175_4) = v0 & $i(v0)) % 68.37/9.80 | % 68.37/9.80 | GROUND_INST: instantiating (22) with all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4, simplifying with (45), (46), (48), (49), (51) gives: % 68.37/9.80 | (67) ? [v0: int] : ( ~ (v0 = 0) & s_col(all_175_5, all_175_4, all_175_1) = % 68.37/9.80 | v0) % 68.37/9.80 | % 68.37/9.80 | GROUND_INST: instantiating (21) with all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4, simplifying with (45), (46), (48), (49), (51) gives: % 68.37/9.80 | (68) ? [v0: int] : ( ~ (v0 = 0) & s_col(all_175_5, all_175_4, all_175_2) = % 68.37/9.80 | v0) % 68.37/9.80 | % 68.37/9.80 | GROUND_INST: instantiating (20) with all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4, simplifying with (45), (46), (48), (49), (51) gives: % 68.37/9.80 | (69) ? [v0: $i] : (ss2(all_175_2, all_175_1, all_175_5, all_175_4) = v0 & % 68.37/9.80 | s_col(all_175_5, all_175_4, v0) = 0 & $i(v0)) % 68.37/9.80 | % 68.37/9.80 | GROUND_INST: instantiating (19) with all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4, simplifying with (45), (46), (48), (49), (51) gives: % 68.37/9.80 | (70) ? [v0: $i] : (ss1(all_175_2, all_175_1, all_175_5, all_175_4) = v0 & % 68.37/9.80 | s_col(all_175_5, all_175_4, v0) = 0 & $i(v0)) % 68.37/9.80 | % 68.37/9.80 | DELTA: instantiating (68) with fresh symbol all_183_0 gives: % 68.37/9.80 | (71) ~ (all_183_0 = 0) & s_col(all_175_5, all_175_4, all_175_2) = % 68.37/9.80 | all_183_0 % 68.37/9.80 | % 68.37/9.80 | ALPHA: (71) implies: % 68.37/9.80 | (72) ~ (all_183_0 = 0) % 68.37/9.80 | (73) s_col(all_175_5, all_175_4, all_175_2) = all_183_0 % 68.37/9.80 | % 68.37/9.80 | DELTA: instantiating (67) with fresh symbol all_185_0 gives: % 68.37/9.80 | (74) ~ (all_185_0 = 0) & s_col(all_175_5, all_175_4, all_175_1) = % 68.37/9.80 | all_185_0 % 68.37/9.80 | % 68.37/9.80 | ALPHA: (74) implies: % 68.37/9.80 | (75) ~ (all_185_0 = 0) % 68.37/9.80 | (76) s_col(all_175_5, all_175_4, all_175_1) = all_185_0 % 68.37/9.80 | % 68.37/9.80 | DELTA: instantiating (66) with fresh symbol all_187_0 gives: % 68.37/9.80 | (77) ~ (all_187_0 = all_175_2) & ss1(all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4) = all_187_0 & $i(all_187_0) % 68.37/9.80 | % 68.37/9.80 | ALPHA: (77) implies: % 68.37/9.80 | (78) ~ (all_187_0 = all_175_2) % 68.37/9.80 | (79) ss1(all_175_2, all_175_1, all_175_5, all_175_4) = all_187_0 % 68.37/9.80 | % 68.37/9.80 | DELTA: instantiating (65) with fresh symbol all_189_0 gives: % 68.37/9.80 | (80) ~ (all_189_0 = all_175_1) & ss2(all_175_2, all_175_1, all_175_5, % 68.37/9.80 | all_175_4) = all_189_0 & $i(all_189_0) % 68.37/9.80 | % 68.37/9.80 | ALPHA: (80) implies: % 68.37/9.80 | (81) ~ (all_189_0 = all_175_1) % 68.37/9.80 | (82) ss2(all_175_2, all_175_1, all_175_5, all_175_4) = all_189_0 % 68.37/9.80 | % 68.37/9.80 | DELTA: instantiating (70) with fresh symbol all_191_0 gives: % 68.37/9.80 | (83) ss1(all_175_2, all_175_1, all_175_5, all_175_4) = all_191_0 & % 68.37/9.80 | s_col(all_175_5, all_175_4, all_191_0) = 0 & $i(all_191_0) % 68.37/9.80 | % 68.37/9.80 | ALPHA: (83) implies: % 68.37/9.80 | (84) $i(all_191_0) % 68.37/9.80 | (85) s_col(all_175_5, all_175_4, all_191_0) = 0 % 68.37/9.80 | (86) ss1(all_175_2, all_175_1, all_175_5, all_175_4) = all_191_0 % 68.37/9.80 | % 68.37/9.80 | DELTA: instantiating (69) with fresh symbol all_193_0 gives: % 68.37/9.80 | (87) ss2(all_175_2, all_175_1, all_175_5, all_175_4) = all_193_0 & % 68.37/9.80 | s_col(all_175_5, all_175_4, all_193_0) = 0 & $i(all_193_0) % 68.37/9.80 | % 68.37/9.80 | ALPHA: (87) implies: % 68.37/9.80 | (88) $i(all_193_0) % 68.37/9.80 | (89) s_col(all_175_5, all_175_4, all_193_0) = 0 % 68.37/9.80 | (90) ss2(all_175_2, all_175_1, all_175_5, all_175_4) = all_193_0 % 68.37/9.80 | % 68.37/9.80 | DELTA: instantiating (64) with fresh symbols all_201_0, all_201_1 gives: % 68.37/9.80 | (91) ss3(all_175_2, all_175_1, all_175_5, all_175_4) = all_201_0 & % 68.37/9.80 | ss1(all_175_2, all_175_1, all_175_5, all_175_4) = all_201_1 & % 68.37/9.80 | s_t(all_175_2, all_201_1, all_201_0) = 0 & $i(all_201_0) & % 68.37/9.80 | $i(all_201_1) % 68.37/9.80 | % 68.37/9.80 | ALPHA: (91) implies: % 68.37/9.80 | (92) s_t(all_175_2, all_201_1, all_201_0) = 0 % 68.37/9.80 | (93) ss1(all_175_2, all_175_1, all_175_5, all_175_4) = all_201_1 % 68.37/9.80 | (94) ss3(all_175_2, all_175_1, all_175_5, all_175_4) = all_201_0 % 68.37/9.80 | % 68.37/9.80 | DELTA: instantiating (63) with fresh symbols all_203_0, all_203_1 gives: % 68.37/9.80 | (95) ss3(all_175_2, all_175_1, all_175_5, all_175_4) = all_203_0 & % 68.37/9.80 | ss2(all_175_2, all_175_1, all_175_5, all_175_4) = all_203_1 & % 68.37/9.80 | s_t(all_175_1, all_203_1, all_203_0) = 0 & $i(all_203_0) & % 68.37/9.80 | $i(all_203_1) % 68.37/9.80 | % 68.37/9.80 | ALPHA: (95) implies: % 68.37/9.81 | (96) $i(all_203_0) % 68.37/9.81 | (97) s_t(all_175_1, all_203_1, all_203_0) = 0 % 68.37/9.81 | (98) ss2(all_175_2, all_175_1, all_175_5, all_175_4) = all_203_1 % 68.37/9.81 | (99) ss3(all_175_2, all_175_1, all_175_5, all_175_4) = all_203_0 % 68.37/9.81 | % 68.37/9.81 | DELTA: instantiating (61) with fresh symbols all_205_0, all_205_1 gives: % 68.37/9.81 | (100) ~ (all_205_0 = all_205_1) & ss3(all_175_2, all_175_1, all_175_5, % 68.37/9.81 | all_175_4) = all_205_1 & ss2(all_175_2, all_175_1, all_175_5, % 68.37/9.81 | all_175_4) = all_205_0 & $i(all_205_0) & $i(all_205_1) % 68.37/9.81 | % 68.37/9.81 | ALPHA: (100) implies: % 68.37/9.81 | (101) ~ (all_205_0 = all_205_1) % 68.37/9.81 | (102) ss2(all_175_2, all_175_1, all_175_5, all_175_4) = all_205_0 % 68.37/9.81 | (103) ss3(all_175_2, all_175_1, all_175_5, all_175_4) = all_205_1 % 68.37/9.81 | % 68.37/9.81 | DELTA: instantiating (62) with fresh symbols all_207_0, all_207_1 gives: % 68.37/9.81 | (104) ~ (all_207_0 = all_207_1) & ss3(all_175_2, all_175_1, all_175_5, % 68.37/9.81 | all_175_4) = all_207_1 & ss1(all_175_2, all_175_1, all_175_5, % 68.37/9.81 | all_175_4) = all_207_0 & $i(all_207_0) & $i(all_207_1) % 68.37/9.81 | % 68.37/9.81 | ALPHA: (104) implies: % 68.37/9.81 | (105) ~ (all_207_0 = all_207_1) % 68.37/9.81 | (106) ss1(all_175_2, all_175_1, all_175_5, all_175_4) = all_207_0 % 68.37/9.81 | (107) ss3(all_175_2, all_175_1, all_175_5, all_175_4) = all_207_1 % 68.37/9.81 | % 68.37/9.81 | BETA: splitting (55) gives: % 68.37/9.81 | % 68.37/9.81 | Case 1: % 68.37/9.81 | | % 68.37/9.81 | | (108) all_171_0 = 0 % 68.37/9.81 | | % 68.37/9.81 | | REDUCE: (38), (108) imply: % 68.37/9.81 | | (109) $false % 68.37/9.81 | | % 68.37/9.81 | | CLOSE: (109) is inconsistent. % 68.37/9.81 | | % 68.37/9.81 | Case 2: % 68.37/9.81 | | % 68.37/9.81 | | (110) ? [v0: int] : ( ~ (v0 = 0) & s_t(beta, alpha, gamma) = v0) % 68.37/9.81 | | % 68.37/9.81 | | DELTA: instantiating (110) with fresh symbol all_246_0 gives: % 68.37/9.81 | | (111) ~ (all_246_0 = 0) & s_t(beta, alpha, gamma) = all_246_0 % 68.37/9.81 | | % 68.37/9.81 | | ALPHA: (111) implies: % 68.37/9.81 | | (112) ~ (all_246_0 = 0) % 68.37/9.81 | | (113) s_t(beta, alpha, gamma) = all_246_0 % 68.37/9.81 | | % 68.37/9.81 | | BETA: splitting (53) gives: % 68.37/9.81 | | % 68.37/9.81 | | Case 1: % 68.37/9.81 | | | % 68.37/9.81 | | | (114) all_171_1 = 0 % 68.37/9.81 | | | % 68.37/9.81 | | | REDUCE: (37), (114) imply: % 68.37/9.81 | | | (115) $false % 68.37/9.81 | | | % 68.37/9.81 | | | CLOSE: (115) is inconsistent. % 68.37/9.81 | | | % 68.37/9.81 | | Case 2: % 68.37/9.81 | | | % 68.37/9.81 | | | (116) ? [v0: any] : ? [v1: any] : (sameside(alpha, beta, gamma) = v0 % 68.37/9.81 | | | & s_t(beta, alpha, gamma) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 68.37/9.81 | | | % 68.37/9.81 | | | DELTA: instantiating (116) with fresh symbols all_321_0, all_321_1 gives: % 68.37/9.81 | | | (117) sameside(alpha, beta, gamma) = all_321_1 & s_t(beta, alpha, % 68.37/9.81 | | | gamma) = all_321_0 & ( ~ (all_321_1 = 0) | all_321_0 = 0) % 68.37/9.81 | | | % 68.37/9.81 | | | ALPHA: (117) implies: % 68.37/9.81 | | | (118) s_t(beta, alpha, gamma) = all_321_0 % 68.37/9.81 | | | (119) ~ (all_321_1 = 0) | all_321_0 = 0 % 68.37/9.81 | | | % 68.37/9.81 | | | BETA: splitting (54) gives: % 68.37/9.81 | | | % 68.37/9.81 | | | Case 1: % 68.37/9.81 | | | | % 68.37/9.81 | | | | (120) all_171_1 = 0 % 68.37/9.81 | | | | % 68.37/9.81 | | | | REDUCE: (37), (120) imply: % 68.37/9.81 | | | | (121) $false % 68.37/9.81 | | | | % 68.37/9.81 | | | | CLOSE: (121) is inconsistent. % 68.37/9.81 | | | | % 68.37/9.81 | | | Case 2: % 68.37/9.81 | | | | % 68.37/9.81 | | | | (122) ? [v0: any] : ? [v1: any] : (sameside(gamma, beta, alpha) = % 68.37/9.81 | | | | v0 & s_t(beta, alpha, gamma) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 68.37/9.81 | | | | % 68.37/9.81 | | | | DELTA: instantiating (122) with fresh symbols all_351_0, all_351_1 % 68.37/9.81 | | | | gives: % 68.37/9.81 | | | | (123) sameside(gamma, beta, alpha) = all_351_1 & s_t(beta, alpha, % 68.37/9.81 | | | | gamma) = all_351_0 & ( ~ (all_351_1 = 0) | all_351_0 = 0) % 68.37/9.81 | | | | % 68.37/9.81 | | | | ALPHA: (123) implies: % 68.37/9.81 | | | | (124) s_t(beta, alpha, gamma) = all_351_0 % 68.37/9.81 | | | | % 68.37/9.81 | | | | BETA: splitting (56) gives: % 68.37/9.81 | | | | % 68.37/9.81 | | | | Case 1: % 68.37/9.81 | | | | | % 68.37/9.81 | | | | | (125) all_175_3 = all_175_5 % 68.37/9.81 | | | | | % 68.37/9.81 | | | | | REDUCE: (43), (125) imply: % 68.37/9.81 | | | | | (126) $false % 68.37/9.81 | | | | | % 68.37/9.81 | | | | | CLOSE: (126) is inconsistent. % 68.37/9.81 | | | | | % 68.37/9.81 | | | | Case 2: % 68.37/9.81 | | | | | % 68.37/9.81 | | | | | % 68.37/9.81 | | | | | GROUND_INST: instantiating (31) with all_321_0, all_351_0, gamma, % 68.37/9.81 | | | | | alpha, beta, simplifying with (118), (124) gives: % 68.37/9.81 | | | | | (127) all_351_0 = all_321_0 % 68.37/9.81 | | | | | % 68.37/9.81 | | | | | GROUND_INST: instantiating (31) with all_246_0, all_351_0, gamma, % 68.37/9.81 | | | | | alpha, beta, simplifying with (113), (124) gives: % 68.37/9.81 | | | | | (128) all_351_0 = all_246_0 % 68.37/9.81 | | | | | % 68.37/9.81 | | | | | GROUND_INST: instantiating (33) with all_187_0, all_201_1, all_175_4, % 68.37/9.81 | | | | | all_175_5, all_175_1, all_175_2, simplifying with (79), % 68.37/9.81 | | | | | (93) gives: % 68.37/9.81 | | | | | (129) all_201_1 = all_187_0 % 68.37/9.81 | | | | | % 68.37/9.81 | | | | | GROUND_INST: instantiating (33) with all_201_1, all_207_0, all_175_4, % 68.37/9.81 | | | | | all_175_5, all_175_1, all_175_2, simplifying with (93), % 68.37/9.81 | | | | | (106) gives: % 68.37/9.81 | | | | | (130) all_207_0 = all_201_1 % 68.37/9.81 | | | | | % 68.37/9.81 | | | | | GROUND_INST: instantiating (33) with all_191_0, all_207_0, all_175_4, % 68.37/9.81 | | | | | all_175_5, all_175_1, all_175_2, simplifying with (86), % 68.37/9.81 | | | | | (106) gives: % 68.37/9.81 | | | | | (131) all_207_0 = all_191_0 % 68.37/9.81 | | | | | % 68.37/9.81 | | | | | GROUND_INST: instantiating (34) with all_193_0, all_203_1, all_175_4, % 68.37/9.81 | | | | | all_175_5, all_175_1, all_175_2, simplifying with (90), % 68.37/9.81 | | | | | (98) gives: % 68.37/9.81 | | | | | (132) all_203_1 = all_193_0 % 68.37/9.81 | | | | | % 68.37/9.81 | | | | | GROUND_INST: instantiating (34) with all_203_1, all_205_0, all_175_4, % 68.37/9.81 | | | | | all_175_5, all_175_1, all_175_2, simplifying with (98), % 68.37/9.81 | | | | | (102) gives: % 68.37/9.81 | | | | | (133) all_205_0 = all_203_1 % 68.37/9.81 | | | | | % 68.37/9.81 | | | | | GROUND_INST: instantiating (34) with all_189_0, all_205_0, all_175_4, % 68.37/9.81 | | | | | all_175_5, all_175_1, all_175_2, simplifying with (82), % 68.37/9.81 | | | | | (102) gives: % 68.37/9.81 | | | | | (134) all_205_0 = all_189_0 % 68.37/9.81 | | | | | % 68.37/9.81 | | | | | GROUND_INST: instantiating (35) with all_203_0, all_205_1, all_175_4, % 68.37/9.81 | | | | | all_175_5, all_175_1, all_175_2, simplifying with (99), % 68.37/9.81 | | | | | (103) gives: % 68.37/9.82 | | | | | (135) all_205_1 = all_203_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | GROUND_INST: instantiating (35) with all_205_1, all_207_1, all_175_4, % 68.37/9.82 | | | | | all_175_5, all_175_1, all_175_2, simplifying with (103), % 68.37/9.82 | | | | | (107) gives: % 68.37/9.82 | | | | | (136) all_207_1 = all_205_1 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | GROUND_INST: instantiating (35) with all_201_0, all_207_1, all_175_4, % 68.37/9.82 | | | | | all_175_5, all_175_1, all_175_2, simplifying with (94), % 68.37/9.82 | | | | | (107) gives: % 68.37/9.82 | | | | | (137) all_207_1 = all_201_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | COMBINE_EQS: (127), (128) imply: % 68.37/9.82 | | | | | (138) all_321_0 = all_246_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | COMBINE_EQS: (130), (131) imply: % 68.37/9.82 | | | | | (139) all_201_1 = all_191_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | SIMP: (139) implies: % 68.37/9.82 | | | | | (140) all_201_1 = all_191_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | COMBINE_EQS: (136), (137) imply: % 68.37/9.82 | | | | | (141) all_205_1 = all_201_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | SIMP: (141) implies: % 68.37/9.82 | | | | | (142) all_205_1 = all_201_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | COMBINE_EQS: (133), (134) imply: % 68.37/9.82 | | | | | (143) all_203_1 = all_189_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | SIMP: (143) implies: % 68.37/9.82 | | | | | (144) all_203_1 = all_189_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | COMBINE_EQS: (135), (142) imply: % 68.37/9.82 | | | | | (145) all_203_0 = all_201_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | COMBINE_EQS: (132), (144) imply: % 68.37/9.82 | | | | | (146) all_193_0 = all_189_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | SIMP: (146) implies: % 68.37/9.82 | | | | | (147) all_193_0 = all_189_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | COMBINE_EQS: (129), (140) imply: % 68.37/9.82 | | | | | (148) all_191_0 = all_187_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | COMBINE_EQS: (131), (148) imply: % 68.37/9.82 | | | | | (149) all_207_0 = all_187_0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | REDUCE: (105), (137), (149) imply: % 68.37/9.82 | | | | | (150) ~ (all_201_0 = all_187_0) % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | SIMP: (150) implies: % 68.37/9.82 | | | | | (151) ~ (all_201_0 = all_187_0) % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | REDUCE: (101), (134), (142) imply: % 68.37/9.82 | | | | | (152) ~ (all_201_0 = all_189_0) % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | SIMP: (152) implies: % 68.37/9.82 | | | | | (153) ~ (all_201_0 = all_189_0) % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | REDUCE: (89), (147) imply: % 68.37/9.82 | | | | | (154) s_col(all_175_5, all_175_4, all_189_0) = 0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | REDUCE: (85), (148) imply: % 68.37/9.82 | | | | | (155) s_col(all_175_5, all_175_4, all_187_0) = 0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | REDUCE: (97), (144), (145) imply: % 68.37/9.82 | | | | | (156) s_t(all_175_1, all_189_0, all_201_0) = 0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | REDUCE: (92), (129) imply: % 68.37/9.82 | | | | | (157) s_t(all_175_2, all_187_0, all_201_0) = 0 % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | REDUCE: (96), (145) imply: % 68.37/9.82 | | | | | (158) $i(all_201_0) % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | REDUCE: (88), (147) imply: % 68.37/9.82 | | | | | (159) $i(all_189_0) % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | REDUCE: (84), (148) imply: % 68.37/9.82 | | | | | (160) $i(all_187_0) % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | BETA: splitting (119) gives: % 68.37/9.82 | | | | | % 68.37/9.82 | | | | | Case 1: % 68.37/9.82 | | | | | | % 68.37/9.82 | | | | | | % 68.37/9.82 | | | | | | GROUND_INST: instantiating (30) with all_175_2, all_175_1, % 68.37/9.82 | | | | | | all_175_5, all_175_3, all_187_0, all_201_0, all_189_0, % 68.37/9.82 | | | | | | all_175_0, simplifying with (45), (47), (48), (49), % 68.37/9.82 | | | | | | (52), (156), (157), (158), (159), (160) gives: % 68.37/9.82 | | | | | | (161) all_201_0 = all_189_0 | all_201_0 = all_187_0 | all_189_0 = % 68.37/9.82 | | | | | | all_175_1 | all_187_0 = all_175_2 | all_175_0 = 0 | % 68.37/9.82 | | | | | | all_175_3 = all_175_5 | ? [v0: any] : ? [v1: any] : ? % 68.37/9.82 | | | | | | [v2: any] : ? [v3: any] : (s_col(all_175_5, all_175_3, % 68.37/9.82 | | | | | | all_189_0) = v1 & s_col(all_175_5, all_175_3, % 68.37/9.82 | | | | | | all_187_0) = v0 & s_col(all_175_5, all_175_3, % 68.37/9.82 | | | | | | all_175_1) = v3 & s_col(all_175_5, all_175_3, % 68.37/9.82 | | | | | | all_175_2) = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | % 68.37/9.82 | | | | | | v2 = 0)) % 68.37/9.82 | | | | | | % 68.37/9.82 | | | | | | GROUND_INST: instantiating (29) with all_175_1, all_175_2, % 68.37/9.82 | | | | | | all_175_5, all_175_4, all_189_0, all_201_0, all_187_0, % 68.37/9.82 | | | | | | all_183_0, simplifying with (45), (46), (48), (49), % 68.37/9.82 | | | | | | (73), (156), (157), (158), (159), (160) gives: % 68.37/9.82 | | | | | | (162) all_201_0 = all_189_0 | all_201_0 = all_187_0 | all_189_0 = % 68.37/9.82 | | | | | | all_175_1 | all_187_0 = all_175_2 | all_183_0 = 0 | % 68.37/9.82 | | | | | | all_175_4 = all_175_5 | ? [v0: any] : ? [v1: any] : ? % 68.37/9.82 | | | | | | [v2: any] : ? [v3: any] : (samesideline(all_175_1, % 68.37/9.82 | | | | | | all_175_2, all_175_5, all_175_4) = v3 & % 68.37/9.82 | | | | | | s_col(all_175_5, all_175_4, all_189_0) = v0 & % 68.37/9.82 | | | | | | s_col(all_175_5, all_175_4, all_187_0) = v1 & % 68.37/9.82 | | | | | | s_col(all_175_5, all_175_4, all_175_1) = v2 & ( ~ (v1 = % 68.37/9.82 | | | | | | 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 68.37/9.82 | | | | | | % 68.37/9.82 | | | | | | GROUND_INST: instantiating (13) with all_175_5, all_175_4, % 68.37/9.82 | | | | | | all_175_3, all_187_0, simplifying with (45), (46), % 68.37/9.82 | | | | | | (47), (50), (155), (160) gives: % 68.37/9.82 | | | | | | (163) all_175_4 = all_175_5 | s_col(all_175_5, all_175_3, % 68.37/9.82 | | | | | | all_187_0) = 0 % 68.37/9.82 | | | | | | % 68.37/9.82 | | | | | | GROUND_INST: instantiating (13) with all_175_5, all_175_4, % 68.37/9.82 | | | | | | all_175_3, all_189_0, simplifying with (45), (46), % 68.37/9.82 | | | | | | (47), (50), (154), (159) gives: % 68.37/9.82 | | | | | | (164) all_175_4 = all_175_5 | s_col(all_175_5, all_175_3, % 68.37/9.82 | | | | | | all_189_0) = 0 % 68.37/9.82 | | | | | | % 68.37/9.82 | | | | | | GROUND_INST: instantiating (12) with all_175_5, all_175_3, % 68.37/9.82 | | | | | | all_175_5, all_175_4, all_189_0, simplifying with (45), % 68.37/9.82 | | | | | | (46), (47), (60), (154), (159) gives: % 68.37/9.82 | | | | | | (165) all_175_3 = all_175_5 | all_175_4 = all_175_5 | ? [v0: % 68.37/9.82 | | | | | | any] : ? [v1: any] : (s_col(all_175_5, all_175_3, % 68.37/9.82 | | | | | | all_189_0) = v1 & s_col(all_175_5, all_175_3, % 68.37/9.82 | | | | | | all_175_5) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 68.37/9.82 | | | | | | % 68.37/9.82 | | | | | | GROUND_INST: instantiating (12) with all_175_5, all_175_3, % 68.37/9.82 | | | | | | all_175_5, all_175_4, all_187_0, simplifying with (45), % 68.37/9.82 | | | | | | (46), (47), (60), (155), (160) gives: % 68.37/9.82 | | | | | | (166) all_175_3 = all_175_5 | all_175_4 = all_175_5 | ? [v0: % 68.37/9.82 | | | | | | any] : ? [v1: any] : (s_col(all_175_5, all_175_3, % 68.37/9.82 | | | | | | all_187_0) = v1 & s_col(all_175_5, all_175_3, % 68.37/9.82 | | | | | | all_175_5) = v0 & ( ~ (v0 = 0) | v1 = 0)) % 68.37/9.82 | | | | | | % 68.37/9.82 | | | | | | GROUND_INST: instantiating (8) with all_175_5, all_175_3, all_175_4, % 68.37/9.82 | | | | | | all_175_1, all_185_0, simplifying with (45), (46), % 68.37/9.82 | | | | | | (47), (49), (60), (76) gives: % 68.37/9.82 | | | | | | (167) all_185_0 = 0 | all_175_3 = all_175_5 | all_175_4 = % 68.37/9.82 | | | | | | all_175_5 | ? [v0: int] : ( ~ (v0 = 0) & s_col(all_175_5, % 68.37/9.82 | | | | | | all_175_3, all_175_1) = v0) % 68.37/9.82 | | | | | | % 68.37/9.82 | | | | | | GROUND_INST: instantiating (9) with all_175_5, all_175_4, all_175_5, % 68.37/9.82 | | | | | | all_175_3, all_175_1, all_185_0, simplifying with (45), % 68.37/9.82 | | | | | | (46), (47), (49), (60), (76) gives: % 68.37/9.83 | | | | | | (168) all_185_0 = 0 | all_175_3 = all_175_5 | all_175_4 = % 68.37/9.83 | | | | | | all_175_5 | ? [v0: any] : ? [v1: any] : (s_col(all_175_5, % 68.37/9.83 | | | | | | all_175_3, all_175_1) = v1 & s_col(all_175_5, % 68.37/9.83 | | | | | | all_175_3, all_175_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = % 68.37/9.83 | | | | | | 0))) % 68.37/9.83 | | | | | | % 68.37/9.83 | | | | | | GROUND_INST: instantiating (14) with all_175_5, all_175_3, % 68.37/9.83 | | | | | | all_175_4, all_175_2, all_183_0, simplifying with (45), % 68.37/9.83 | | | | | | (46), (47), (48), (60), (73) gives: % 68.37/9.83 | | | | | | (169) all_183_0 = 0 | all_175_3 = all_175_5 | ? [v0: int] : ( ~ % 68.37/9.83 | | | | | | (v0 = 0) & s_col(all_175_5, all_175_3, all_175_2) = v0) % 68.37/9.83 | | | | | | % 68.37/9.83 | | | | | | GROUND_INST: instantiating (11) with all_175_5, all_175_4, % 68.37/9.83 | | | | | | all_175_1, all_175_5, all_175_3, all_185_0, simplifying % 68.37/9.83 | | | | | | with (45), (46), (47), (49), (59), (76) gives: % 68.37/9.83 | | | | | | (170) all_185_0 = 0 | all_175_4 = all_175_5 | ? [v0: any] : ? % 68.37/9.83 | | | | | | [v1: any] : ? [v2: any] : ? [v3: any] : (s_m(all_175_5, % 68.37/9.83 | | | | | | all_175_3, all_175_1) = v3 & s_col(all_175_5, % 68.37/9.83 | | | | | | all_175_3, all_175_1) = v2 & s_e(all_175_4, all_175_1, % 68.37/9.83 | | | | | | all_175_5, all_175_5) = v1 & s_e(all_175_5, all_175_4, % 68.37/9.83 | | | | | | all_175_1, all_175_5) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) % 68.37/9.83 | | | | | | | ~ (v0 = 0) | v3 = 0)) % 68.37/9.83 | | | | | | % 68.37/9.83 | | | | | | GROUND_INST: instantiating (11) with all_175_5, all_175_4, % 68.37/9.83 | | | | | | all_175_2, all_175_5, all_175_3, all_183_0, simplifying % 68.37/9.83 | | | | | | with (45), (46), (47), (48), (59), (73) gives: % 68.37/9.83 | | | | | | (171) all_183_0 = 0 | all_175_4 = all_175_5 | ? [v0: any] : ? % 68.37/9.83 | | | | | | [v1: any] : ? [v2: any] : ? [v3: any] : (s_m(all_175_5, % 68.37/9.83 | | | | | | all_175_3, all_175_2) = v3 & s_col(all_175_5, % 68.37/9.83 | | | | | | all_175_3, all_175_2) = v2 & s_e(all_175_4, all_175_2, % 68.37/9.83 | | | | | | all_175_5, all_175_5) = v1 & s_e(all_175_5, all_175_4, % 68.37/9.83 | | | | | | all_175_2, all_175_5) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) % 68.37/9.83 | | | | | | | ~ (v0 = 0) | v3 = 0)) % 68.37/9.83 | | | | | | % 68.37/9.83 | | | | | | GROUND_INST: instantiating (9) with all_175_5, all_175_4, all_175_3, % 68.37/9.83 | | | | | | all_175_5, all_175_1, all_185_0, simplifying with (45), % 68.37/9.83 | | | | | | (46), (47), (49), (58), (76) gives: % 68.37/9.83 | | | | | | (172) all_185_0 = 0 | all_175_3 = all_175_5 | all_175_4 = % 68.37/9.83 | | | | | | all_175_5 | ? [v0: any] : ? [v1: any] : (s_col(all_175_3, % 68.37/9.83 | | | | | | all_175_5, all_175_1) = v1 & s_col(all_175_3, % 68.37/9.83 | | | | | | all_175_5, all_175_5) = v0 & ( ~ (v1 = 0) | ~ (v0 = % 68.37/9.83 | | | | | | 0))) % 68.37/9.83 | | | | | | % 68.37/9.83 | | | | | | GROUND_INST: instantiating (10) with all_175_5, all_175_3, % 68.37/9.83 | | | | | | all_189_0, all_175_5, all_175_4, simplifying with (45), % 68.37/9.83 | | | | | | (46), (47), (57), (154), (159) gives: % 68.37/9.83 | | | | | | (173) all_175_3 = all_175_5 | ? [v0: any] : ? [v1: any] : ? % 68.37/9.83 | | | | | | [v2: any] : ? [v3: any] : (s_m(all_175_5, all_175_4, % 68.37/9.83 | | | | | | all_189_0) = v3 & s_col(all_175_5, all_175_3, % 68.37/9.83 | | | | | | all_189_0) = v0 & s_e(all_175_3, all_189_0, all_175_5, % 68.37/9.83 | | | | | | all_175_5) = v2 & s_e(all_175_5, all_175_3, all_189_0, % 68.37/9.83 | | | | | | all_175_5) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0) | v3 = 0 | % 68.37/9.83 | | | | | | v0 = 0)) % 68.37/9.83 | | | | | | % 68.37/9.83 | | | | | | GROUND_INST: instantiating (10) with all_175_5, all_175_3, % 68.37/9.83 | | | | | | all_187_0, all_175_5, all_175_4, simplifying with (45), % 68.37/9.83 | | | | | | (46), (47), (57), (155), (160) gives: % 68.37/9.83 | | | | | | (174) all_175_3 = all_175_5 | ? [v0: any] : ? [v1: any] : ? % 68.37/9.83 | | | | | | [v2: any] : ? [v3: any] : (s_m(all_175_5, all_175_4, % 68.37/9.83 | | | | | | all_187_0) = v3 & s_col(all_175_5, all_175_3, % 68.37/9.83 | | | | | | all_187_0) = v0 & s_e(all_175_3, all_187_0, all_175_5, % 68.37/9.83 | | | | | | all_175_5) = v2 & s_e(all_175_5, all_175_3, all_187_0, % 68.37/9.83 | | | | | | all_175_5) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0) | v3 = 0 | % 68.37/9.83 | | | | | | v0 = 0)) % 68.37/9.83 | | | | | | % 68.37/9.83 | | | | | | BETA: splitting (174) gives: % 68.37/9.83 | | | | | | % 68.37/9.83 | | | | | | Case 1: % 68.37/9.83 | | | | | | | % 68.37/9.83 | | | | | | | (175) all_175_3 = all_175_5 % 68.37/9.83 | | | | | | | % 68.37/9.83 | | | | | | | REDUCE: (43), (175) imply: % 68.37/9.83 | | | | | | | (176) $false % 68.37/9.83 | | | | | | | % 68.37/9.83 | | | | | | | CLOSE: (176) is inconsistent. % 68.37/9.83 | | | | | | | % 68.37/9.83 | | | | | | Case 2: % 68.37/9.83 | | | | | | | % 68.37/9.83 | | | | | | | (177) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: any] % 68.37/9.83 | | | | | | | : (s_m(all_175_5, all_175_4, all_187_0) = v3 & % 68.37/9.83 | | | | | | | s_col(all_175_5, all_175_3, all_187_0) = v0 & % 68.37/9.83 | | | | | | | s_e(all_175_3, all_187_0, all_175_5, all_175_5) = v2 & % 68.37/9.83 | | | | | | | s_e(all_175_5, all_175_3, all_187_0, all_175_5) = v1 & % 68.37/9.83 | | | | | | | ( ~ (v2 = 0) | ~ (v1 = 0) | v3 = 0 | v0 = 0)) % 68.37/9.83 | | | | | | | % 68.37/9.83 | | | | | | | DELTA: instantiating (177) with fresh symbols all_726_0, % 68.37/9.83 | | | | | | | all_726_1, all_726_2, all_726_3 gives: % 68.37/9.83 | | | | | | | (178) s_m(all_175_5, all_175_4, all_187_0) = all_726_0 & % 68.37/9.83 | | | | | | | s_col(all_175_5, all_175_3, all_187_0) = all_726_3 & % 68.37/9.83 | | | | | | | s_e(all_175_3, all_187_0, all_175_5, all_175_5) = % 68.37/9.83 | | | | | | | all_726_1 & s_e(all_175_5, all_175_3, all_187_0, % 68.37/9.83 | | | | | | | all_175_5) = all_726_2 & ( ~ (all_726_1 = 0) | ~ % 68.37/9.83 | | | | | | | (all_726_2 = 0) | all_726_0 = 0 | all_726_3 = 0) % 68.37/9.83 | | | | | | | % 68.37/9.83 | | | | | | | ALPHA: (178) implies: % 68.37/9.83 | | | | | | | (179) s_col(all_175_5, all_175_3, all_187_0) = all_726_3 % 68.37/9.83 | | | | | | | % 68.37/9.83 | | | | | | | BETA: splitting (173) gives: % 68.37/9.83 | | | | | | | % 68.37/9.83 | | | | | | | Case 1: % 68.37/9.83 | | | | | | | | % 68.37/9.83 | | | | | | | | (180) all_175_3 = all_175_5 % 68.37/9.83 | | | | | | | | % 68.37/9.83 | | | | | | | | REDUCE: (43), (180) imply: % 68.37/9.83 | | | | | | | | (181) $false % 68.37/9.83 | | | | | | | | % 68.37/9.83 | | | | | | | | CLOSE: (181) is inconsistent. % 68.37/9.83 | | | | | | | | % 68.37/9.83 | | | | | | | Case 2: % 68.37/9.83 | | | | | | | | % 68.37/9.83 | | | | | | | | (182) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 68.37/9.83 | | | | | | | | any] : (s_m(all_175_5, all_175_4, all_189_0) = v3 & % 68.37/9.83 | | | | | | | | s_col(all_175_5, all_175_3, all_189_0) = v0 & % 68.37/9.83 | | | | | | | | s_e(all_175_3, all_189_0, all_175_5, all_175_5) = v2 % 68.37/9.83 | | | | | | | | & s_e(all_175_5, all_175_3, all_189_0, all_175_5) = % 68.37/9.83 | | | | | | | | v1 & ( ~ (v2 = 0) | ~ (v1 = 0) | v3 = 0 | v0 = 0)) % 68.37/9.83 | | | | | | | | % 68.37/9.83 | | | | | | | | DELTA: instantiating (182) with fresh symbols all_820_0, % 68.37/9.83 | | | | | | | | all_820_1, all_820_2, all_820_3 gives: % 68.37/9.83 | | | | | | | | (183) s_m(all_175_5, all_175_4, all_189_0) = all_820_0 & % 68.37/9.83 | | | | | | | | s_col(all_175_5, all_175_3, all_189_0) = all_820_3 & % 68.37/9.83 | | | | | | | | s_e(all_175_3, all_189_0, all_175_5, all_175_5) = % 68.37/9.83 | | | | | | | | all_820_1 & s_e(all_175_5, all_175_3, all_189_0, % 68.37/9.83 | | | | | | | | all_175_5) = all_820_2 & ( ~ (all_820_1 = 0) | ~ % 68.37/9.83 | | | | | | | | (all_820_2 = 0) | all_820_0 = 0 | all_820_3 = 0) % 68.37/9.83 | | | | | | | | % 68.37/9.83 | | | | | | | | ALPHA: (183) implies: % 68.37/9.83 | | | | | | | | (184) s_col(all_175_5, all_175_3, all_189_0) = all_820_3 % 68.37/9.83 | | | | | | | | % 68.37/9.83 | | | | | | | | BETA: splitting (169) gives: % 68.37/9.83 | | | | | | | | % 68.37/9.83 | | | | | | | | Case 1: % 68.37/9.83 | | | | | | | | | % 68.37/9.83 | | | | | | | | | (185) all_183_0 = 0 % 68.37/9.83 | | | | | | | | | % 68.37/9.83 | | | | | | | | | REDUCE: (72), (185) imply: % 68.37/9.83 | | | | | | | | | (186) $false % 68.37/9.83 | | | | | | | | | % 68.37/9.83 | | | | | | | | | CLOSE: (186) is inconsistent. % 68.37/9.83 | | | | | | | | | % 68.37/9.83 | | | | | | | | Case 2: % 68.37/9.83 | | | | | | | | | % 68.37/9.83 | | | | | | | | | (187) all_175_3 = all_175_5 | ? [v0: int] : ( ~ (v0 = 0) & % 68.37/9.83 | | | | | | | | | s_col(all_175_5, all_175_3, all_175_2) = v0) % 68.37/9.83 | | | | | | | | | % 68.37/9.83 | | | | | | | | | BETA: splitting (163) gives: % 68.37/9.83 | | | | | | | | | % 68.37/9.83 | | | | | | | | | Case 1: % 68.37/9.83 | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | (188) s_col(all_175_5, all_175_3, all_187_0) = 0 % 68.37/9.83 | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | BETA: splitting (164) gives: % 68.37/9.83 | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | Case 1: % 68.37/9.83 | | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | | (189) s_col(all_175_5, all_175_3, all_189_0) = 0 % 68.37/9.83 | | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | | BETA: splitting (187) gives: % 68.37/9.83 | | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | | Case 1: % 68.37/9.83 | | | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | | | (190) all_175_3 = all_175_5 % 68.37/9.83 | | | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | | | REDUCE: (43), (190) imply: % 68.37/9.83 | | | | | | | | | | | | (191) $false % 68.37/9.83 | | | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | | | CLOSE: (191) is inconsistent. % 68.37/9.83 | | | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | | Case 2: % 68.37/9.83 | | | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | | | (192) ? [v0: int] : ( ~ (v0 = 0) & s_col(all_175_5, % 68.37/9.83 | | | | | | | | | | | | all_175_3, all_175_2) = v0) % 68.37/9.83 | | | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | | | DELTA: instantiating (192) with fresh symbol all_1060_0 % 68.37/9.83 | | | | | | | | | | | | gives: % 68.37/9.83 | | | | | | | | | | | | (193) ~ (all_1060_0 = 0) & s_col(all_175_5, all_175_3, % 68.37/9.83 | | | | | | | | | | | | all_175_2) = all_1060_0 % 68.37/9.83 | | | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | | | ALPHA: (193) implies: % 68.37/9.83 | | | | | | | | | | | | (194) s_col(all_175_5, all_175_3, all_175_2) = % 68.37/9.83 | | | | | | | | | | | | all_1060_0 % 68.37/9.83 | | | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | | | BETA: splitting (165) gives: % 68.37/9.83 | | | | | | | | | | | | % 68.37/9.83 | | | | | | | | | | | | Case 1: % 68.37/9.84 | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | (195) all_175_3 = all_175_5 % 68.37/9.84 | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | REDUCE: (43), (195) imply: % 68.37/9.84 | | | | | | | | | | | | | (196) $false % 68.37/9.84 | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | CLOSE: (196) is inconsistent. % 68.37/9.84 | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | Case 2: % 68.37/9.84 | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | (197) all_175_4 = all_175_5 | ? [v0: any] : ? [v1: % 68.37/9.84 | | | | | | | | | | | | | any] : (s_col(all_175_5, all_175_3, all_189_0) = % 68.37/9.84 | | | | | | | | | | | | | v1 & s_col(all_175_5, all_175_3, all_175_5) = v0 % 68.37/9.84 | | | | | | | | | | | | | & ( ~ (v0 = 0) | v1 = 0)) % 68.37/9.84 | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | BETA: splitting (166) gives: % 68.37/9.84 | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | Case 1: % 68.37/9.84 | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | (198) all_175_3 = all_175_5 % 68.37/9.84 | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | REDUCE: (43), (198) imply: % 68.37/9.84 | | | | | | | | | | | | | | (199) $false % 68.37/9.84 | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | CLOSE: (199) is inconsistent. % 68.37/9.84 | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | Case 2: % 68.37/9.84 | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | (200) all_175_4 = all_175_5 | ? [v0: any] : ? [v1: % 68.37/9.84 | | | | | | | | | | | | | | any] : (s_col(all_175_5, all_175_3, all_187_0) = % 68.37/9.84 | | | | | | | | | | | | | | v1 & s_col(all_175_5, all_175_3, all_175_5) = v0 % 68.37/9.84 | | | | | | | | | | | | | | & ( ~ (v0 = 0) | v1 = 0)) % 68.37/9.84 | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | BETA: splitting (167) gives: % 68.37/9.84 | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | Case 1: % 68.37/9.84 | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | (201) all_185_0 = 0 % 68.37/9.84 | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | REDUCE: (75), (201) imply: % 68.37/9.84 | | | | | | | | | | | | | | | (202) $false % 68.37/9.84 | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | CLOSE: (202) is inconsistent. % 68.37/9.84 | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | Case 2: % 68.37/9.84 | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | (203) all_175_3 = all_175_5 | all_175_4 = all_175_5 | ? % 68.37/9.84 | | | | | | | | | | | | | | | [v0: int] : ( ~ (v0 = 0) & s_col(all_175_5, % 68.37/9.84 | | | | | | | | | | | | | | | all_175_3, all_175_1) = v0) % 68.37/9.84 | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | BETA: splitting (168) gives: % 68.37/9.84 | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | Case 1: % 68.37/9.84 | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | (204) all_185_0 = 0 % 68.37/9.84 | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | REDUCE: (75), (204) imply: % 68.37/9.84 | | | | | | | | | | | | | | | | (205) $false % 68.37/9.84 | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | CLOSE: (205) is inconsistent. % 68.37/9.84 | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | Case 2: % 68.37/9.84 | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | (206) all_175_3 = all_175_5 | all_175_4 = all_175_5 | ? % 68.37/9.84 | | | | | | | | | | | | | | | | [v0: any] : ? [v1: any] : (s_col(all_175_5, % 68.37/9.84 | | | | | | | | | | | | | | | | all_175_3, all_175_1) = v1 & s_col(all_175_5, % 68.37/9.84 | | | | | | | | | | | | | | | | all_175_3, all_175_5) = v0 & ( ~ (v1 = 0) | ~ % 68.37/9.84 | | | | | | | | | | | | | | | | (v0 = 0))) % 68.37/9.84 | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | BETA: splitting (171) gives: % 68.37/9.84 | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | Case 1: % 68.37/9.84 | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | (207) all_183_0 = 0 % 68.37/9.84 | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | REDUCE: (72), (207) imply: % 68.37/9.84 | | | | | | | | | | | | | | | | | (208) $false % 68.37/9.84 | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | CLOSE: (208) is inconsistent. % 68.37/9.84 | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | Case 2: % 68.37/9.84 | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | (209) all_175_4 = all_175_5 | ? [v0: any] : ? [v1: % 68.37/9.84 | | | | | | | | | | | | | | | | | any] : ? [v2: any] : ? [v3: any] : % 68.37/9.84 | | | | | | | | | | | | | | | | | (s_m(all_175_5, all_175_3, all_175_2) = v3 & % 68.37/9.84 | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_175_2) = v2 & % 68.37/9.84 | | | | | | | | | | | | | | | | | s_e(all_175_4, all_175_2, all_175_5, all_175_5) % 68.37/9.84 | | | | | | | | | | | | | | | | | = v1 & s_e(all_175_5, all_175_4, all_175_2, % 68.37/9.84 | | | | | | | | | | | | | | | | | all_175_5) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | % 68.37/9.84 | | | | | | | | | | | | | | | | | ~ (v0 = 0) | v3 = 0)) % 68.37/9.84 | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | BETA: splitting (197) gives: % 68.37/9.84 | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.84 | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | (210) all_175_4 = all_175_5 % 68.37/9.84 | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | REDUCE: (42), (210) imply: % 68.37/9.84 | | | | | | | | | | | | | | | | | | (211) $false % 68.37/9.84 | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | CLOSE: (211) is inconsistent. % 68.37/9.84 | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.84 | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | (212) ? [v0: any] : ? [v1: any] : (s_col(all_175_5, % 68.37/9.84 | | | | | | | | | | | | | | | | | | all_175_3, all_189_0) = v1 & s_col(all_175_5, % 68.37/9.84 | | | | | | | | | | | | | | | | | | all_175_3, all_175_5) = v0 & ( ~ (v0 = 0) | v1 % 68.37/9.84 | | | | | | | | | | | | | | | | | | = 0)) % 68.37/9.84 | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | DELTA: instantiating (212) with fresh symbols all_1134_0, % 68.37/9.84 | | | | | | | | | | | | | | | | | | all_1134_1 gives: % 68.37/9.84 | | | | | | | | | | | | | | | | | | (213) s_col(all_175_5, all_175_3, all_189_0) = % 68.37/9.84 | | | | | | | | | | | | | | | | | | all_1134_0 & s_col(all_175_5, all_175_3, % 68.37/9.84 | | | | | | | | | | | | | | | | | | all_175_5) = all_1134_1 & ( ~ (all_1134_1 = 0) | % 68.37/9.84 | | | | | | | | | | | | | | | | | | all_1134_0 = 0) % 68.37/9.84 | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | ALPHA: (213) implies: % 68.37/9.84 | | | | | | | | | | | | | | | | | | (214) s_col(all_175_5, all_175_3, all_189_0) = % 68.37/9.84 | | | | | | | | | | | | | | | | | | all_1134_0 % 68.37/9.84 | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | BETA: splitting (200) gives: % 68.37/9.84 | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | (215) all_175_4 = all_175_5 % 68.37/9.84 | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | REDUCE: (42), (215) imply: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | (216) $false % 68.37/9.84 | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | CLOSE: (216) is inconsistent. % 68.37/9.84 | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | (217) ? [v0: any] : ? [v1: any] : (s_col(all_175_5, % 68.37/9.84 | | | | | | | | | | | | | | | | | | | all_175_3, all_187_0) = v1 & s_col(all_175_5, % 68.37/9.84 | | | | | | | | | | | | | | | | | | | all_175_3, all_175_5) = v0 & ( ~ (v0 = 0) | v1 % 68.37/9.84 | | | | | | | | | | | | | | | | | | | = 0)) % 68.37/9.84 | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | DELTA: instantiating (217) with fresh symbols all_1139_0, % 68.37/9.84 | | | | | | | | | | | | | | | | | | | all_1139_1 gives: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | (218) s_col(all_175_5, all_175_3, all_187_0) = % 68.37/9.84 | | | | | | | | | | | | | | | | | | | all_1139_0 & s_col(all_175_5, all_175_3, % 68.37/9.84 | | | | | | | | | | | | | | | | | | | all_175_5) = all_1139_1 & ( ~ (all_1139_1 = 0) | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | all_1139_0 = 0) % 68.37/9.84 | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | ALPHA: (218) implies: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | (219) s_col(all_175_5, all_175_3, all_187_0) = % 68.37/9.84 | | | | | | | | | | | | | | | | | | | all_1139_0 % 68.37/9.84 | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | BETA: splitting (203) gives: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | (220) all_175_3 = all_175_5 % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | REDUCE: (43), (220) imply: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | (221) $false % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | CLOSE: (221) is inconsistent. % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | (222) all_175_4 = all_175_5 | ? [v0: int] : ( ~ (v0 = % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | 0) & s_col(all_175_5, all_175_3, all_175_1) = % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | v0) % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | BETA: splitting (206) gives: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | (223) all_175_3 = all_175_5 % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | REDUCE: (43), (223) imply: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | (224) $false % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | CLOSE: (224) is inconsistent. % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | (225) all_175_4 = all_175_5 | ? [v0: any] : ? [v1: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | any] : (s_col(all_175_5, all_175_3, all_175_1) = % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | v1 & s_col(all_175_5, all_175_3, all_175_5) = v0 % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | & ( ~ (v1 = 0) | ~ (v0 = 0))) % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | BETA: splitting (170) gives: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | (226) all_185_0 = 0 % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (75), (226) imply: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | (227) $false % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | CLOSE: (227) is inconsistent. % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | (228) all_175_4 = all_175_5 | ? [v0: any] : ? [v1: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | any] : ? [v2: any] : ? [v3: any] : % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | (s_m(all_175_5, all_175_3, all_175_1) = v3 & % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_175_1) = v2 & % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | s_e(all_175_4, all_175_1, all_175_5, all_175_5) % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | = v1 & s_e(all_175_5, all_175_4, all_175_1, % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | all_175_5) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | ~ (v0 = 0) | v3 = 0)) % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (161) gives: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | (229) all_175_0 = 0 % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (44), (229) imply: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | (230) $false % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (230) is inconsistent. % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | (231) all_201_0 = all_189_0 | all_201_0 = all_187_0 | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | all_189_0 = all_175_1 | all_187_0 = all_175_2 | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | all_175_3 = all_175_5 | ? [v0: any] : ? [v1: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | any] : ? [v2: any] : ? [v3: any] : % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | (s_col(all_175_5, all_175_3, all_189_0) = v1 & % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_187_0) = v0 & % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_175_1) = v3 & % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_175_2) = v2 & ( % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (225) gives: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | (232) all_175_4 = all_175_5 % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (42), (232) imply: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | (233) $false % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (233) is inconsistent. % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | (234) ? [v0: any] : ? [v1: any] : (s_col(all_175_5, % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | all_175_3, all_175_1) = v1 & s_col(all_175_5, % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | all_175_3, all_175_5) = v0 & ( ~ (v1 = 0) | ~ % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | (v0 = 0))) % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (234) with fresh symbols all_1254_0, % 68.37/9.84 | | | | | | | | | | | | | | | | | | | | | | | | all_1254_1 gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | (235) s_col(all_175_5, all_175_3, all_175_1) = % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | all_1254_0 & s_col(all_175_5, all_175_3, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | all_175_5) = all_1254_1 & ( ~ (all_1254_0 = 0) | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | ~ (all_1254_1 = 0)) % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (235) implies: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | (236) s_col(all_175_5, all_175_3, all_175_1) = % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | all_1254_0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (209) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | (237) all_175_4 = all_175_5 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (42), (237) imply: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | (238) $false % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (238) is inconsistent. % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | (239) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | [v3: any] : (s_m(all_175_5, all_175_3, all_175_2) % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | = v3 & s_col(all_175_5, all_175_3, all_175_2) = % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | v2 & s_e(all_175_4, all_175_2, all_175_5, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | all_175_5) = v1 & s_e(all_175_5, all_175_4, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | all_175_2, all_175_5) = v0 & ( ~ (v2 = 0) | ~ % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (239) with fresh symbols all_1340_0, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | all_1340_1, all_1340_2, all_1340_3 gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | (240) s_m(all_175_5, all_175_3, all_175_2) = all_1340_0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | & s_col(all_175_5, all_175_3, all_175_2) = % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | all_1340_1 & s_e(all_175_4, all_175_2, all_175_5, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | all_175_5) = all_1340_2 & s_e(all_175_5, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | all_175_4, all_175_2, all_175_5) = all_1340_3 & % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | ( ~ (all_1340_1 = 0) | ~ (all_1340_2 = 0) | ~ % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | (all_1340_3 = 0) | all_1340_0 = 0) % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (240) implies: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | (241) s_col(all_175_5, all_175_3, all_175_2) = % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | all_1340_1 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (228) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | (242) all_175_4 = all_175_5 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (42), (242) imply: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | (243) $false % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (243) is inconsistent. % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | (244) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | [v3: any] : (s_m(all_175_5, all_175_3, all_175_1) % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | = v3 & s_col(all_175_5, all_175_3, all_175_1) = % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | v2 & s_e(all_175_4, all_175_1, all_175_5, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_5) = v1 & s_e(all_175_5, all_175_4, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_1, all_175_5) = v0 & ( ~ (v2 = 0) | ~ % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | (v1 = 0) | ~ (v0 = 0) | v3 = 0)) % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (244) with fresh symbols all_1348_0, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | all_1348_1, all_1348_2, all_1348_3 gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | (245) s_m(all_175_5, all_175_3, all_175_1) = all_1348_0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | & s_col(all_175_5, all_175_3, all_175_1) = % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | all_1348_1 & s_e(all_175_4, all_175_1, all_175_5, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_5) = all_1348_2 & s_e(all_175_5, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_4, all_175_1, all_175_5) = all_1348_3 & % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | ( ~ (all_1348_1 = 0) | ~ (all_1348_2 = 0) | ~ % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | (all_1348_3 = 0) | all_1348_0 = 0) % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (245) implies: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | (246) s_col(all_175_5, all_175_3, all_175_1) = % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | all_1348_1 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (172) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | (247) all_185_0 = 0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (75), (247) imply: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | (248) $false % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (248) is inconsistent. % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | (249) all_175_3 = all_175_5 | all_175_4 = all_175_5 | ? % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | [v0: any] : ? [v1: any] : (s_col(all_175_3, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_5, all_175_1) = v1 & s_col(all_175_3, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_5, all_175_5) = v0 & ( ~ (v1 = 0) | ~ % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | (v0 = 0))) % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (162) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (250) all_183_0 = 0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (72), (250) imply: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (251) $false % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (251) is inconsistent. % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (252) all_201_0 = all_189_0 | all_201_0 = all_187_0 | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_189_0 = all_175_1 | all_187_0 = all_175_2 | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_4 = all_175_5 | ? [v0: any] : ? [v1: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | any] : ? [v2: any] : ? [v3: any] : % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (samesideline(all_175_1, all_175_2, all_175_5, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_4) = v3 & s_col(all_175_5, all_175_4, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_189_0) = v0 & s_col(all_175_5, all_175_4, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_187_0) = v1 & s_col(all_175_5, all_175_4, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_1) = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | v3 = 0 | v2 = 0)) % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (249) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (253) all_175_3 = all_175_5 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (43), (253) imply: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (254) $false % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (254) is inconsistent. % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (255) all_175_4 = all_175_5 | ? [v0: any] : ? [v1: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | any] : (s_col(all_175_3, all_175_5, all_175_1) = % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | v1 & s_col(all_175_3, all_175_5, all_175_5) = v0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | & ( ~ (v1 = 0) | ~ (v0 = 0))) % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (252) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (256) all_201_0 = all_189_0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (153), (256) imply: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (257) $false % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (257) is inconsistent. % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (192) with fresh symbol all_1531_0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (258) ~ (all_1531_0 = 0) & s_col(all_175_5, all_175_3, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_2) = all_1531_0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (258) implies: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (259) ~ (all_1531_0 = 0) % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (260) s_col(all_175_5, all_175_3, all_175_2) = % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_1531_0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (222) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (261) all_175_4 = all_175_5 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (42), (261) imply: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (262) $false % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (262) is inconsistent. % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (263) ? [v0: int] : ( ~ (v0 = 0) & s_col(all_175_5, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_3, all_175_1) = v0) % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (263) with fresh symbol all_1556_0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (264) ~ (all_1556_0 = 0) & s_col(all_175_5, all_175_3, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_1) = all_1556_0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (264) implies: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (265) ~ (all_1556_0 = 0) % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (266) s_col(all_175_5, all_175_3, all_175_1) = % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_1556_0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (255) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (267) all_175_4 = all_175_5 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (42), (267) imply: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (268) $false % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (268) is inconsistent. % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_1340_1, all_1531_0, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_2, all_175_3, all_175_5, simplifying with % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (241), (260) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (269) all_1531_0 = all_1340_1 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_1060_0, all_1531_0, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_2, all_175_3, all_175_5, simplifying with % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (194), (260) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (270) all_1531_0 = all_1060_0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_1348_1, all_1556_0, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_1, all_175_3, all_175_5, simplifying with % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (246), (266) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (271) all_1556_0 = all_1348_1 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_1254_0, all_1556_0, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_1, all_175_3, all_175_5, simplifying with % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (236), (266) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (272) all_1556_0 = all_1254_0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_726_3, all_1139_0, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_187_0, all_175_3, all_175_5, simplifying with % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (179), (219) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (273) all_1139_0 = all_726_3 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with 0, all_1139_0, all_187_0, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_3, all_175_5, simplifying with (188), % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (219) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (274) all_1139_0 = 0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_820_3, all_1134_0, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_189_0, all_175_3, all_175_5, simplifying with % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (184), (214) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (275) all_1134_0 = all_820_3 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with 0, all_1134_0, all_189_0, % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_3, all_175_5, simplifying with (189), % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (214) gives: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (276) all_1134_0 = 0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (271), (272) imply: % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (277) all_1348_1 = all_1254_0 % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.85 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (277) implies: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (278) all_1348_1 = all_1254_0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (269), (270) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (279) all_1340_1 = all_1060_0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (273), (274) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (280) all_726_3 = 0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (275), (276) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (281) all_820_3 = 0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (281) implies: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (282) all_820_3 = 0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (265), (272) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (283) ~ (all_1254_0 = 0) % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (259), (270) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (284) ~ (all_1060_0 = 0) % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (231) gives: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (285) all_201_0 = all_189_0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (153), (285) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (286) $false % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (286) is inconsistent. % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (287) all_201_0 = all_187_0 | all_189_0 = all_175_1 | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_187_0 = all_175_2 | all_175_3 = all_175_5 | ? % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | any] : (s_col(all_175_5, all_175_3, all_189_0) = % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | v1 & s_col(all_175_5, all_175_3, all_187_0) = v0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | & s_col(all_175_5, all_175_3, all_175_1) = v3 & % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_175_2) = v2 & ( % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (287) gives: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (288) all_201_0 = all_187_0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (151), (288) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (289) $false % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (289) is inconsistent. % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (290) all_189_0 = all_175_1 | all_187_0 = all_175_2 | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_3 = all_175_5 | ? [v0: any] : ? [v1: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | any] : ? [v2: any] : ? [v3: any] : % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (s_col(all_175_5, all_175_3, all_189_0) = v1 & % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_187_0) = v0 & % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_175_1) = v3 & % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_175_2) = v2 & ( % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (290) gives: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (291) all_189_0 = all_175_1 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (81), (291) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (292) $false % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (292) is inconsistent. % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (293) all_187_0 = all_175_2 | all_175_3 = all_175_5 | ? % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | any] : (s_col(all_175_5, all_175_3, all_189_0) = % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | v1 & s_col(all_175_5, all_175_3, all_187_0) = v0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | & s_col(all_175_5, all_175_3, all_175_1) = v3 & % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_175_2) = v2 & ( % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (293) gives: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (294) all_187_0 = all_175_2 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (78), (294) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (295) $false % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (295) is inconsistent. % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (296) all_175_3 = all_175_5 | ? [v0: any] : ? [v1: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | any] : ? [v2: any] : ? [v3: any] : % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (s_col(all_175_5, all_175_3, all_189_0) = v1 & % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_187_0) = v0 & % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_175_1) = v3 & % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_175_2) = v2 & ( % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (296) gives: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (297) all_175_3 = all_175_5 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (43), (297) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (298) $false % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (298) is inconsistent. % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (299) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | [v3: any] : (s_col(all_175_5, all_175_3, % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_189_0) = v1 & s_col(all_175_5, all_175_3, % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_187_0) = v0 & s_col(all_175_5, all_175_3, % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_1) = v3 & s_col(all_175_5, all_175_3, % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_2) = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | v3 = 0 | v2 = 0)) % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (299) with fresh symbols all_1751_0, % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_1751_1, all_1751_2, all_1751_3 gives: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (300) s_col(all_175_5, all_175_3, all_189_0) = % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_1751_2 & s_col(all_175_5, all_175_3, % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_187_0) = all_1751_3 & s_col(all_175_5, % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_3, all_175_1) = all_1751_0 & % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | s_col(all_175_5, all_175_3, all_175_2) = % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_1751_1 & ( ~ (all_1751_2 = 0) | ~ (all_1751_3 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0) | all_1751_0 = 0 | all_1751_1 = 0) % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ALPHA: (300) implies: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (301) s_col(all_175_5, all_175_3, all_175_2) = % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_1751_1 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (302) s_col(all_175_5, all_175_3, all_175_1) = % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_1751_0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (303) s_col(all_175_5, all_175_3, all_187_0) = % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_1751_3 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (304) s_col(all_175_5, all_175_3, all_189_0) = % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_1751_2 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (305) ~ (all_1751_2 = 0) | ~ (all_1751_3 = 0) | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_1751_0 = 0 | all_1751_1 = 0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_1060_0, all_1751_1, % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_2, all_175_3, all_175_5, simplifying with % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (194), (301) gives: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (306) all_1751_1 = all_1060_0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with all_1254_0, all_1751_0, % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_1, all_175_3, all_175_5, simplifying with % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (236), (302) gives: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (307) all_1751_0 = all_1254_0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with 0, all_1751_3, all_187_0, % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_3, all_175_5, simplifying with (188), % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (303) gives: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (308) all_1751_3 = 0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (32) with 0, all_1751_2, all_189_0, % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_175_3, all_175_5, simplifying with (189), % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (304) gives: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (309) all_1751_2 = 0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (305) gives: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (310) ~ (all_1751_2 = 0) % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (309), (310) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (311) $false % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (311) is inconsistent. % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (312) ~ (all_1751_3 = 0) | all_1751_0 = 0 | all_1751_1 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | = 0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (312) gives: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (313) ~ (all_1751_3 = 0) % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (308), (313) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (314) $false % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (314) is inconsistent. % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (315) all_1751_0 = 0 | all_1751_1 = 0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (315) gives: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (316) all_1751_0 = 0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (307), (316) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (317) all_1254_0 = 0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (283), (317) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (318) $false % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (318) is inconsistent. % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (319) all_1751_1 = 0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (306), (319) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (320) all_1060_0 = 0 % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (284), (320) imply: % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (321) $false % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (321) is inconsistent. % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | End of split % 68.37/9.86 | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | Case 2: % 68.37/9.86 | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | (322) all_175_4 = all_175_5 % 68.37/9.86 | | | | | | | | | | | % 68.37/9.86 | | | | | | | | | | | REDUCE: (42), (322) imply: % 68.37/9.87 | | | | | | | | | | | (323) $false % 68.37/9.87 | | | | | | | | | | | % 68.37/9.87 | | | | | | | | | | | CLOSE: (323) is inconsistent. % 68.37/9.87 | | | | | | | | | | | % 68.37/9.87 | | | | | | | | | | End of split % 68.37/9.87 | | | | | | | | | | % 68.37/9.87 | | | | | | | | | Case 2: % 68.37/9.87 | | | | | | | | | | % 68.37/9.87 | | | | | | | | | | (324) all_175_4 = all_175_5 % 68.37/9.87 | | | | | | | | | | % 68.37/9.87 | | | | | | | | | | REDUCE: (42), (324) imply: % 68.37/9.87 | | | | | | | | | | (325) $false % 68.37/9.87 | | | | | | | | | | % 68.37/9.87 | | | | | | | | | | CLOSE: (325) is inconsistent. % 68.37/9.87 | | | | | | | | | | % 68.37/9.87 | | | | | | | | | End of split % 68.37/9.87 | | | | | | | | | % 68.37/9.87 | | | | | | | | End of split % 68.37/9.87 | | | | | | | | % 68.37/9.87 | | | | | | | End of split % 68.37/9.87 | | | | | | | % 68.37/9.87 | | | | | | End of split % 68.37/9.87 | | | | | | % 68.37/9.87 | | | | | Case 2: % 68.37/9.87 | | | | | | % 68.37/9.87 | | | | | | (326) all_321_0 = 0 % 68.37/9.87 | | | | | | % 68.37/9.87 | | | | | | COMBINE_EQS: (138), (326) imply: % 68.37/9.87 | | | | | | (327) all_246_0 = 0 % 68.37/9.87 | | | | | | % 68.37/9.87 | | | | | | REDUCE: (112), (327) imply: % 68.37/9.87 | | | | | | (328) $false % 68.37/9.87 | | | | | | % 68.37/9.87 | | | | | | CLOSE: (328) is inconsistent. % 68.37/9.87 | | | | | | % 68.37/9.87 | | | | | End of split % 68.37/9.87 | | | | | % 68.37/9.87 | | | | End of split % 68.37/9.87 | | | | % 68.37/9.87 | | | End of split % 68.37/9.87 | | | % 68.37/9.87 | | End of split % 68.37/9.87 | | % 68.37/9.87 | End of split % 68.37/9.87 | % 68.37/9.87 End of proof % 68.37/9.87 % SZS output end Proof for theBenchmark % 68.37/9.87 % 68.37/9.87 9293ms %------------------------------------------------------------------------------