%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : GEO514+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 : n015.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 48.69s 7.48s % Output : Proof 50.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : GEO514+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.15/0.35 % Computer : n015.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Tue Aug 29 20:28:56 EDT 2023 % 0.15/0.35 % CPUTime : % 0.22/0.61 ________ _____ % 0.22/0.61 ___ __ \_________(_)________________________________ % 0.22/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.22/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.22/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.22/0.61 % 0.22/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.22/0.61 (2023-06-19) % 0.22/0.61 % 0.22/0.61 (c) Philipp Rümmer, 2009-2023 % 0.22/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.22/0.61 Amanda Stjerna. % 0.22/0.61 Free software under BSD-3-Clause. % 0.22/0.61 % 0.22/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.22/0.61 % 0.22/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.22/0.62 Running up to 7 provers in parallel. % 0.22/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.22/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.22/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.22/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.22/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.22/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.22/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 5.56/1.66 Prover 4: Preprocessing ... % 5.56/1.68 Prover 1: Preprocessing ... % 5.56/1.70 Prover 3: Preprocessing ... % 5.56/1.70 Prover 5: Preprocessing ... % 5.56/1.70 Prover 0: Preprocessing ... % 5.56/1.70 Prover 6: Preprocessing ... % 5.56/1.70 Prover 2: Preprocessing ... % 16.43/3.05 Prover 5: Proving ... % 16.43/3.07 Prover 2: Proving ... % 17.39/3.16 Prover 1: Warning: ignoring some quantifiers % 18.64/3.29 Prover 6: Proving ... % 18.64/3.32 Prover 3: Warning: ignoring some quantifiers % 18.64/3.34 Prover 1: Constructing countermodel ... % 19.22/3.37 Prover 3: Constructing countermodel ... % 22.74/3.85 Prover 4: Constructing countermodel ... % 23.64/3.96 Prover 0: Proving ... % 27.76/4.52 Prover 3: gave up % 27.76/4.52 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 30.15/4.82 Prover 7: Preprocessing ... % 31.44/5.14 Prover 7: Warning: ignoring some quantifiers % 32.74/5.18 Prover 7: Constructing countermodel ... % 41.17/6.34 Prover 1: gave up % 41.17/6.34 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 42.80/6.51 Prover 7: gave up % 42.80/6.52 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 43.41/6.57 Prover 8: Preprocessing ... % 44.07/6.71 Prover 9: Preprocessing ... % 45.76/6.90 Prover 4: Found proof (size 228) % 45.76/6.90 Prover 4: proved (6265ms) % 45.76/6.91 Prover 0: stopped % 45.76/6.91 Prover 6: stopped % 46.13/6.91 Prover 2: stopped % 46.13/7.00 Prover 8: Warning: ignoring some quantifiers % 46.13/7.04 Prover 8: Constructing countermodel ... % 46.13/7.06 Prover 8: stopped % 46.76/7.09 Prover 5: stopped % 48.44/7.44 Prover 9: Warning: ignoring some quantifiers % 48.69/7.47 Prover 9: Constructing countermodel ... % 48.69/7.47 Prover 9: stopped % 48.69/7.47 % 48.69/7.48 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 48.69/7.48 % 49.08/7.55 % SZS output start Proof for theBenchmark % 49.08/7.59 Assumptions after simplification: % 49.08/7.59 --------------------------------- % 49.08/7.59 % 49.08/7.59 (aA8) % 49.08/7.63 $i(gamma) & $i(beta) & $i(alpha) & ? [v0: int] : ? [v1: int] : ? [v2: int] % 49.08/7.63 : ( ~ (v2 = 0) & ~ (v1 = 0) & ~ (v0 = 0) & s_t(gamma, alpha, beta) = v2 & % 49.08/7.63 s_t(beta, gamma, alpha) = v1 & s_t(alpha, beta, gamma) = v0) % 49.08/7.63 % 49.08/7.63 (aExtSameSide2) % 49.08/7.63 ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: int] : ( ~ (v4 % 49.08/7.63 = 0) & ~ (v1 = v0) & samesideline(v2, v3, v1, v0) = v4 & samesideline(v2, % 49.08/7.63 v3, v0, v1) = 0 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 49.08/7.63 % 49.08/7.63 (aSatz3_13a) % 49.08/7.63 ~ (beta = alpha) & $i(beta) & $i(alpha) % 49.08/7.63 % 49.08/7.63 (aSatz3_13b) % 49.08/7.63 ~ (gamma = beta) & $i(gamma) & $i(beta) % 49.08/7.63 % 49.08/7.63 (aSatz3_2) % 49.08/7.64 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_t(v2, % 49.08/7.64 v1, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ % 49.08/7.64 (v4 = 0) & s_t(v0, v1, v2) = v4)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 49.08/7.64 $i] : ( ~ (s_t(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 49.08/7.64 s_t(v2, v1, v0) = 0) % 49.08/7.64 % 49.08/7.64 (aSatz4_11d) % 49.08/7.64 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 49.08/7.64 (s_col(v1, v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] % 49.08/7.64 : ( ~ (v4 = 0) & s_col(v0, v1, v2) = v4)) & ! [v0: $i] : ! [v1: $i] : ! % 49.08/7.64 [v2: $i] : ( ~ (s_col(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 49.08/7.64 s_col(v1, v0, v2) = 0) % 49.08/7.64 % 49.08/7.64 (aSatz5_12b) % 49.48/7.65 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_t(v0, % 49.48/7.65 v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? % 49.48/7.65 [v5: any] : ? [v6: any] : (le(v1, v2, v0, v2) = v6 & le(v0, v1, v0, v2) = % 49.48/7.65 v5 & s_col(v0, v1, v2) = v4 & ( ~ (v6 = 0) | ~ (v5 = 0) | ~ (v4 = 0)))) % 49.48/7.65 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (le(v1, v2, v0, v2) = 0) | ~ % 49.48/7.65 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: any] : ? [v5: any] % 49.48/7.65 : (le(v0, v1, v0, v2) = v5 & s_col(v0, v1, v2) = v3 & s_t(v0, v1, v2) = v4 & % 49.48/7.65 ( ~ (v5 = 0) | ~ (v3 = 0) | v4 = 0))) & ! [v0: $i] : ! [v1: $i] : ! % 49.48/7.65 [v2: $i] : ( ~ (le(v0, v1, v0, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 49.48/7.65 ? [v3: any] : ? [v4: any] : ? [v5: any] : (le(v1, v2, v0, v2) = v5 & % 49.48/7.65 s_col(v0, v1, v2) = v3 & s_t(v0, v1, v2) = v4 & ( ~ (v5 = 0) | ~ (v3 = 0) % 49.48/7.65 | v4 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_col(v0, % 49.48/7.65 v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? % 49.48/7.65 [v4: any] : ? [v5: any] : (le(v1, v2, v0, v2) = v5 & le(v0, v1, v0, v2) = % 49.48/7.65 v4 & s_t(v0, v1, v2) = v3 & ( ~ (v5 = 0) | ~ (v4 = 0) | v3 = 0))) % 49.48/7.65 % 49.48/7.65 (aSatz6_13a) % 49.48/7.66 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_t(v1, % 49.48/7.66 v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? % 49.48/7.66 [v5: any] : (sameside(v0, v1, v2) = v4 & le(v1, v0, v1, v2) = v5 & ( ~ (v5 = % 49.48/7.66 0) | ~ (v4 = 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 49.48/7.66 (sameside(v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: % 49.48/7.66 any] : ? [v4: any] : (le(v1, v0, v1, v2) = v3 & s_t(v1, v0, v2) = v4 & ( % 49.48/7.66 ~ (v3 = 0) | v4 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 49.48/7.66 (le(v1, v0, v1, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] % 49.48/7.66 : ? [v4: any] : (sameside(v0, v1, v2) = v3 & s_t(v1, v0, v2) = v4 & ( ~ (v3 % 49.48/7.66 = 0) | v4 = 0))) % 49.48/7.66 % 49.48/7.66 (aSatz6_15a) % 49.48/7.67 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : ! [v5: % 49.48/7.67 int] : (v5 = 0 | v4 = 0 | v3 = v0 | v2 = v0 | v1 = v0 | ~ (sameside(v3, v0, % 49.48/7.67 v2) = v5) | ~ (sameside(v3, v0, v1) = v4) | ~ $i(v3) | ~ $i(v2) | ~ % 49.48/7.67 $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: any] : (s_col(v3, v0, v1) = v7 & % 49.48/7.67 s_t(v1, v0, v2) = v6 & ( ~ (v7 = 0) | ~ (v6 = 0)))) & ! [v0: $i] : ! % 49.48/7.67 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | v3 = v0 | v2 = % 49.48/7.67 v0 | v1 = v0 | ~ (sameside(v3, v0, v2) = v4) | ~ (s_col(v3, v0, v1) = 0) | % 49.48/7.67 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] % 49.48/7.67 : (sameside(v3, v0, v1) = v6 & s_t(v1, v0, v2) = v5 & ( ~ (v5 = 0) | v6 = % 49.48/7.67 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 49.48/7.67 int] : (v4 = 0 | v3 = v0 | v2 = v0 | v1 = v0 | ~ (sameside(v3, v0, v2) = % 49.48/7.67 v4) | ~ (s_t(v1, v0, v2) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 49.48/7.67 $i(v0) | ? [v5: any] : ? [v6: any] : (sameside(v3, v0, v1) = v6 & % 49.48/7.67 s_col(v3, v0, v1) = v5 & ( ~ (v5 = 0) | v6 = 0))) & ! [v0: $i] : ! [v1: % 49.48/7.67 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 | v3 = v0 | v2 = v0 % 49.48/7.67 | v1 = v0 | ~ (sameside(v3, v0, v1) = v4) | ~ (s_t(v1, v0, v2) = 0) | ~ % 49.48/7.67 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: any] : ? [v6: any] : % 49.48/7.67 (sameside(v3, v0, v2) = v6 & s_col(v3, v0, v1) = v5 & ( ~ (v5 = 0) | v6 = % 49.48/7.67 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v3 = v0 % 49.48/7.67 | v2 = v0 | v1 = v0 | ~ (s_col(v3, v0, v1) = 0) | ~ (s_t(v1, v0, v2) = 0) % 49.48/7.67 | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: % 49.48/7.67 any] : (sameside(v3, v0, v2) = v5 & sameside(v3, v0, v1) = v4 & (v5 = 0 | % 49.48/7.67 v4 = 0))) % 49.48/7.67 % 49.48/7.67 (d_Defn6_1) % 49.48/7.67 $i(xb) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | v2 % 49.48/7.67 = v1 | v1 = v0 | ~ (sameside(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 49.48/7.67 $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_t(v1, v2, v0) = v4)) & ! [v0: $i] % 49.48/7.67 : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | v1 = v0 | v1 = xb | ~ % 49.48/7.67 (sameside(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 49.48/7.67 int] : ( ~ (v4 = 0) & s_t(v1, v0, v2) = v4)) & ! [v0: $i] : ! [v1: $i] : % 49.48/7.67 ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_t(v1, v2, v0) = v3) | ~ $i(v2) | % 49.48/7.67 ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : (sameside(v0, v1, v2) % 49.48/7.67 = v4 & s_t(v1, v0, v2) = v5 & ( ~ (v4 = 0) | v5 = 0))) & ! [v0: $i] : ! % 49.48/7.67 [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (s_t(v1, v0, v2) = v3) | % 49.48/7.67 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : % 49.48/7.67 (sameside(v0, v1, v2) = v4 & s_t(v1, v2, v0) = v5 & ( ~ (v4 = 0) | v5 = 0))) % 49.48/7.67 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = v1 | v1 = v0 | ~ (s_t(v1, % 49.48/7.67 v2, v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | sameside(v0, v1, v2) % 49.48/7.67 = 0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | v1 = xb | ~ % 49.48/7.67 (s_t(v1, v0, v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | sameside(v0, v1, % 49.48/7.67 v2) = 0) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (sameside(v0, v1, % 49.48/7.67 v2) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: any] : ? [v4: % 49.48/7.67 any] : (s_t(v1, v2, v0) = v4 & s_t(v1, v0, v2) = v3 & (v4 = 0 | v3 = 0))) % 49.48/7.67 & ! [v0: $i] : ! [v1: $i] : ( ~ (sameside(v0, v1, v1) = 0) | ~ $i(v1) | ~ % 49.48/7.68 $i(v0)) & ! [v0: $i] : ! [v1: $i] : ( ~ (sameside(v0, v0, v1) = 0) | ~ % 49.48/7.68 $i(v1) | ~ $i(v0)) % 49.48/7.68 % 49.48/7.68 (d_Defn9_7) % 49.48/7.73 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 49.48/7.73 $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 | v6 = v5 | v6 = v1 | v5 = v4 | % 49.48/7.73 v4 = v0 | v3 = v2 | ~ (samesideline(v0, v1, v2, v3) = v7) | ~ (s_col(v2, % 49.48/7.73 v3, v6) = 0) | ~ (s_t(v0, v4, v5) = 0) | ~ $i(v6) | ~ $i(v5) | ~ % 49.48/7.73 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v8: any] : ? % 49.48/7.73 [v9: any] : ? [v10: any] : ? [v11: any] : (s_col(v2, v3, v4) = v9 & % 49.48/7.73 s_col(v2, v3, v1) = v11 & s_col(v2, v3, v0) = v10 & s_t(v1, v6, v5) = v8 & % 49.48/7.73 ( ~ (v9 = 0) | ~ (v8 = 0) | v11 = 0 | v10 = 0))) & ! [v0: $i] : ! [v1: % 49.48/7.73 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : % 49.48/7.73 ! [v7: int] : (v7 = 0 | v6 = v5 | v6 = v1 | v5 = v4 | v4 = v0 | v3 = v2 | ~ % 49.48/7.73 (samesideline(v0, v1, v2, v3) = v7) | ~ (s_col(v2, v3, v4) = 0) | ~ % 49.48/7.73 (s_t(v1, v6, v5) = 0) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 49.48/7.73 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v8: any] : ? [v9: any] : ? [v10: any] % 49.48/7.73 : ? [v11: any] : (s_col(v2, v3, v6) = v9 & s_col(v2, v3, v1) = v11 & % 49.48/7.73 s_col(v2, v3, v0) = v10 & s_t(v0, v4, v5) = v8 & ( ~ (v9 = 0) | ~ (v8 = % 49.48/7.73 0) | v11 = 0 | v10 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 49.48/7.73 ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 % 49.48/7.73 | v6 = v5 | v6 = v1 | v5 = v4 | v4 = v0 | v3 = v2 | ~ (samesideline(v0, v1, % 49.48/7.73 v2, v3) = v7) | ~ (s_t(v1, v6, v5) = 0) | ~ (s_t(v0, v4, v5) = 0) | ~ % 49.48/7.73 $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 49.48/7.73 $i(v0) | ? [v8: any] : ? [v9: any] : ? [v10: any] : ? [v11: any] : % 49.48/7.73 (s_col(v2, v3, v6) = v9 & s_col(v2, v3, v4) = v8 & s_col(v2, v3, v1) = v11 & % 49.48/7.73 s_col(v2, v3, v0) = v10 & ( ~ (v9 = 0) | ~ (v8 = 0) | v11 = 0 | v10 = % 49.48/7.73 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 49.48/7.73 $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 | v6 = v5 | v6 = v1 % 49.48/7.73 | v5 = v4 | v4 = v0 | v3 = v2 | ~ (s_col(v2, v3, v6) = 0) | ~ (s_col(v2, % 49.48/7.73 v3, v1) = v7) | ~ (s_t(v0, v4, v5) = 0) | ~ $i(v6) | ~ $i(v5) | ~ % 49.48/7.73 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v8: any] : ? % 49.48/7.73 [v9: any] : ? [v10: any] : ? [v11: any] : (samesideline(v0, v1, v2, v3) = % 49.48/7.73 v11 & s_col(v2, v3, v4) = v9 & s_col(v2, v3, v0) = v10 & s_t(v1, v6, v5) = % 49.48/7.73 v8 & ( ~ (v9 = 0) | ~ (v8 = 0) | v11 = 0 | v10 = 0))) & ! [v0: $i] : ! % 49.48/7.74 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] % 49.48/7.74 : ! [v7: int] : (v7 = 0 | v6 = v5 | v6 = v1 | v5 = v4 | v4 = v0 | v3 = v2 | % 49.48/7.74 ~ (s_col(v2, v3, v4) = 0) | ~ (s_col(v2, v3, v0) = v7) | ~ (s_t(v1, v6, % 49.48/7.74 v5) = 0) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 49.48/7.74 ~ $i(v1) | ~ $i(v0) | ? [v8: any] : ? [v9: any] : ? [v10: any] : ? % 49.48/7.74 [v11: any] : (samesideline(v0, v1, v2, v3) = v11 & s_col(v2, v3, v6) = v9 & % 49.48/7.74 s_col(v2, v3, v1) = v10 & s_t(v0, v4, v5) = v8 & ( ~ (v9 = 0) | ~ (v8 = % 49.48/7.74 0) | v11 = 0 | v10 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 49.48/7.74 ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 % 49.48/7.74 | v6 = v5 | v6 = v1 | v5 = v4 | v4 = v0 | v3 = v2 | ~ (s_col(v2, v3, v1) = % 49.48/7.74 v7) | ~ (s_t(v1, v6, v5) = 0) | ~ (s_t(v0, v4, v5) = 0) | ~ $i(v6) | ~ % 49.48/7.74 $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v8: % 49.48/7.74 any] : ? [v9: any] : ? [v10: any] : ? [v11: any] : (samesideline(v0, % 49.48/7.74 v1, v2, v3) = v11 & s_col(v2, v3, v6) = v9 & s_col(v2, v3, v4) = v8 & % 49.48/7.74 s_col(v2, v3, v0) = v10 & ( ~ (v9 = 0) | ~ (v8 = 0) | v11 = 0 | v10 = % 49.48/7.74 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 49.48/7.74 $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 | v6 = v5 | v6 = v1 % 49.48/7.74 | v5 = v4 | v4 = v0 | v3 = v2 | ~ (s_col(v2, v3, v0) = v7) | ~ (s_t(v1, % 49.48/7.74 v6, v5) = 0) | ~ (s_t(v0, v4, v5) = 0) | ~ $i(v6) | ~ $i(v5) | ~ % 49.48/7.74 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v8: any] : ? % 49.48/7.74 [v9: any] : ? [v10: any] : ? [v11: any] : (samesideline(v0, v1, v2, v3) = % 49.48/7.74 v11 & s_col(v2, v3, v6) = v9 & s_col(v2, v3, v4) = v8 & s_col(v2, v3, v1) % 49.48/7.74 = v10 & ( ~ (v9 = 0) | ~ (v8 = 0) | v11 = 0 | v10 = 0))) & ! [v0: $i] : % 49.48/7.74 ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: % 49.48/7.74 $i] : (v6 = v5 | v6 = v1 | v5 = v4 | v4 = v0 | v3 = v2 | ~ (s_col(v2, v3, % 49.48/7.74 v6) = 0) | ~ (s_t(v1, v6, v5) = 0) | ~ (s_t(v0, v4, v5) = 0) | ~ % 49.48/7.74 $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 49.48/7.74 $i(v0) | ? [v7: any] : ? [v8: any] : ? [v9: any] : ? [v10: any] : % 49.48/7.74 (samesideline(v0, v1, v2, v3) = v10 & s_col(v2, v3, v4) = v7 & s_col(v2, v3, % 49.48/7.74 v1) = v9 & s_col(v2, v3, v0) = v8 & ( ~ (v7 = 0) | v10 = 0 | v9 = 0 | v8 % 49.48/7.74 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 49.48/7.74 $i] : ! [v5: $i] : ! [v6: $i] : (v6 = v5 | v6 = v1 | v5 = v4 | v4 = v0 | % 49.48/7.74 v3 = v2 | ~ (s_col(v2, v3, v4) = 0) | ~ (s_t(v1, v6, v5) = 0) | ~ % 49.48/7.74 (s_t(v0, v4, v5) = 0) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 49.48/7.74 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v7: any] : ? [v8: any] : ? [v9: any] % 49.48/7.74 : ? [v10: any] : (samesideline(v0, v1, v2, v3) = v10 & s_col(v2, v3, v6) = % 49.48/7.74 v7 & s_col(v2, v3, v1) = v9 & s_col(v2, v3, v0) = v8 & ( ~ (v7 = 0) | v10 % 49.48/7.74 = 0 | v9 = 0 | v8 = 0))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 49.48/7.74 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: int] : (v6 = 0 | ~ (ss3(v0, % 49.48/7.74 v1, v2, v3) = v5) | ~ (ss2(v0, v1, v2, v3) = v4) | ~ (s_t(v1, v4, v5) % 49.48/7.74 = v6) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v7: int] : ( ~ % 49.48/7.74 (v7 = 0) & samesideline(v0, v1, v2, v3) = v7)) & ! [v0: $i] : ! [v1: $i] % 49.48/7.74 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: int] : (v6 = % 49.48/7.74 0 | ~ (ss3(v0, v1, v2, v3) = v5) | ~ (ss1(v0, v1, v2, v3) = v4) | ~ % 49.48/7.74 (s_t(v0, v4, v5) = v6) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 49.48/7.74 [v7: int] : ( ~ (v7 = 0) & samesideline(v0, v1, v2, v3) = v7)) & ! [v0: $i] % 49.48/7.74 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: int] : (v5 = % 49.48/7.74 0 | ~ (ss2(v0, v1, v2, v3) = v4) | ~ (s_col(v2, v3, v4) = v5) | ~ $i(v3) % 49.48/7.74 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: int] : ( ~ (v6 = 0) & % 49.48/7.74 samesideline(v0, v1, v2, v3) = v6)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 49.48/7.74 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: int] : (v5 = 0 | ~ (ss1(v0, v1, % 49.48/7.74 v2, v3) = v4) | ~ (s_col(v2, v3, v4) = v5) | ~ $i(v3) | ~ $i(v2) | ~ % 49.48/7.74 $i(v1) | ~ $i(v0) | ? [v6: int] : ( ~ (v6 = 0) & samesideline(v0, v1, v2, % 49.48/7.74 v3) = v6)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 49.48/7.74 [v4: $i] : ( ~ (ss3(v0, v1, v2, v3) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 49.48/7.74 | ~ $i(v0) | ? [v5: any] : ? [v6: $i] : (ss2(v0, v1, v2, v3) = v6 & % 49.48/7.74 samesideline(v0, v1, v2, v3) = v5 & $i(v6) & ( ~ (v6 = v4) | ~ (v5 = % 49.48/7.74 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 49.48/7.74 [v4: $i] : ( ~ (ss3(v0, v1, v2, v3) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 49.48/7.74 | ~ $i(v0) | ? [v5: any] : ? [v6: $i] : (ss1(v0, v1, v2, v3) = v6 & % 49.48/7.74 samesideline(v0, v1, v2, v3) = v5 & $i(v6) & ( ~ (v6 = v4) | ~ (v5 = % 49.48/7.74 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 49.48/7.74 [v4: $i] : ( ~ (ss2(v0, v1, v2, v3) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 49.48/7.74 | ~ $i(v0) | ? [v5: any] : ? [v6: $i] : (ss3(v0, v1, v2, v3) = v6 & % 49.48/7.74 samesideline(v0, v1, v2, v3) = v5 & $i(v6) & ( ~ (v6 = v4) | ~ (v5 = % 49.48/7.74 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 49.48/7.74 [v4: $i] : ( ~ (ss1(v0, v1, v2, v3) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) % 49.48/7.74 | ~ $i(v0) | ? [v5: any] : ? [v6: $i] : (ss3(v0, v1, v2, v3) = v6 & % 49.48/7.74 samesideline(v0, v1, v2, v3) = v5 & $i(v6) & ( ~ (v6 = v4) | ~ (v5 = % 49.48/7.74 0)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 49.48/7.74 (ss2(v0, v1, v2, v3) = v1) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 49.48/7.74 ? [v4: int] : ( ~ (v4 = 0) & samesideline(v0, v1, v2, v3) = v4)) & ! [v0: % 49.48/7.74 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (ss1(v0, v1, v2, v3) = % 49.48/7.74 v0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ % 49.48/7.74 (v4 = 0) & samesideline(v0, v1, v2, v3) = v4)) & ! [v0: $i] : ! [v1: $i] % 49.48/7.74 : ! [v2: $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, v2, v3) = 0) | ~ % 49.48/7.74 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : ( ~ % 49.48/7.74 (v5 = v4) & ss3(v0, v1, v2, v3) = v4 & ss2(v0, v1, v2, v3) = v5 & $i(v5) & % 49.48/7.74 $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 49.48/7.74 (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 49.48/7.74 $i(v0) | ? [v4: $i] : ? [v5: $i] : ( ~ (v5 = v4) & ss3(v0, v1, v2, v3) = % 49.48/7.74 v4 & ss1(v0, v1, v2, v3) = v5 & $i(v5) & $i(v4))) & ! [v0: $i] : ! [v1: % 49.48/7.74 $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, v2, v3) = 0) | % 49.48/7.74 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : % 49.48/7.74 (ss3(v0, v1, v2, v3) = v5 & ss2(v0, v1, v2, v3) = v4 & s_t(v1, v4, v5) = 0 & % 49.48/7.74 $i(v5) & $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 49.48/7.74 : ( ~ (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 49.48/7.74 ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : (ss3(v0, v1, v2, v3) = v5 & ss1(v0, % 49.48/7.74 v1, v2, v3) = v4 & s_t(v0, v4, v5) = 0 & $i(v5) & $i(v4))) & ! [v0: $i] % 49.48/7.74 : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, v2, v3) % 49.48/7.74 = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ( ~ % 49.48/7.74 (v4 = v1) & ss2(v0, v1, v2, v3) = v4 & $i(v4))) & ! [v0: $i] : ! [v1: % 49.48/7.74 $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, v2, v3) = 0) | % 49.48/7.74 ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: $i] : ( ~ (v4 = v0) & % 49.48/7.74 ss1(v0, v1, v2, v3) = v4 & $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 49.48/7.74 $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ % 49.48/7.74 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_col(v2, v3, % 49.48/7.74 v1) = v4)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 49.48/7.74 (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 49.48/7.74 $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_col(v2, v3, v0) = v4)) & ! [v0: % 49.48/7.74 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, % 49.48/7.74 v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 49.48/7.74 $i] : (ss2(v0, v1, v2, v3) = v4 & s_col(v2, v3, v4) = 0 & $i(v4))) & ! % 49.48/7.74 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (samesideline(v0, v1, % 49.48/7.74 v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 49.48/7.74 $i] : (ss1(v0, v1, v2, v3) = v4 & s_col(v2, v3, v4) = 0 & $i(v4))) & ! % 49.48/7.74 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (samesideline(v0, v1, v2, v2) = 0) % 49.48/7.74 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0)) % 49.48/7.74 % 49.48/7.74 (d_insert) % 49.48/7.74 $i(gamma) & $i(alpha) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 49.48/7.74 : ! [v4: $i] : ! [v5: $i] : ( ~ (ext(v4, v2, v0, v1) = v5) | ~ (ext(v3, v2, % 49.48/7.74 alpha, gamma) = v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 49.48/7.74 (insert(v0, v1, v2, v3) = v5 & $i(v5))) & ! [v0: $i] : ! [v1: $i] : ! % 49.48/7.74 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ (insert(v0, v1, v2, v3) = v4) | ~ % 49.48/7.74 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (ext(v5, v2, v0, % 49.48/7.74 v1) = v4 & ext(v3, v2, alpha, gamma) = v5 & $i(v5) & $i(v4))) % 49.48/7.74 % 49.48/7.74 (function-axioms) % 49.48/7.77 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 49.48/7.77 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] % 49.48/7.77 : ! [v9: $i] : (v1 = v0 | ~ (s_afs(v9, v8, v7, v6, v5, v4, v3, v2) = v1) | % 49.48/7.77 ~ (s_afs(v9, v8, v7, v6, v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] % 49.48/7.77 : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 49.48/7.77 [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : (v1 = v0 | % 49.48/7.77 ~ (s_fs(v9, v8, v7, v6, v5, v4, v3, v2) = v1) | ~ (s_fs(v9, v8, v7, v6, v5, % 49.48/7.77 v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 49.48/7.77 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 49.48/7.77 ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : (v1 = v0 | ~ % 49.48/7.77 (s_ifs(v9, v8, v7, v6, v5, v4, v3, v2) = v1) | ~ (s_ifs(v9, v8, v7, v6, v5, % 49.48/7.77 v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 49.48/7.77 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 49.48/7.77 ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : (v1 = v0 | ~ (s_kf(v8, v7, v6, v5, % 49.48/7.77 v4, v3, v2) = v1) | ~ (s_kf(v8, v7, v6, v5, v4, v3, v2) = v0)) & ! % 49.48/7.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 49.48/7.77 $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : (v1 = v0 | ~ % 49.48/7.77 (s_e3(v7, v6, v5, v4, v3, v2) = v1) | ~ (s_e3(v7, v6, v5, v4, v3, v2) = % 49.48/7.77 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 49.48/7.77 : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : (v1 = v0 | ~ (crossbar(v7, v6, % 49.48/7.77 v5, v4, v3, v2) = v1) | ~ (crossbar(v7, v6, v5, v4, v3, v2) = v0)) & ! % 49.48/7.77 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 49.48/7.77 : ! [v6: $i] : (v1 = v0 | ~ (g811(v6, v5, v4, v3, v2) = v1) | ~ (g811(v6, % 49.48/7.77 v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 49.48/7.77 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (f811(v6, % 49.48/7.77 v5, v4, v3, v2) = v1) | ~ (f811(v6, v5, v4, v3, v2) = v0)) & ! [v0: % 49.48/7.77 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 49.48/7.77 ! [v6: $i] : (v1 = v0 | ~ (midpointAux(v6, v5, v4, v3, v2) = v1) | ~ % 49.48/7.77 (midpointAux(v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 49.48/7.77 [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | % 49.48/7.77 ~ (g813(v6, v5, v4, v3, v2) = v1) | ~ (g813(v6, v5, v4, v3, v2) = v0)) & ! % 49.48/7.77 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 49.48/7.77 : ! [v6: $i] : (v1 = v0 | ~ (f813(v6, v5, v4, v3, v2) = v1) | ~ (f813(v6, % 49.48/7.77 v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 49.48/7.77 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 49.48/7.77 ! [v6: $i] : (v1 = v0 | ~ (perpAt(v6, v5, v4, v3, v2) = v1) | ~ (perpAt(v6, % 49.48/7.77 v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 49.48/7.77 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ % 49.48/7.77 (insert5(v6, v5, v4, v3, v2) = v1) | ~ (insert5(v6, v5, v4, v3, v2) = v0)) % 49.48/7.77 & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! % 49.48/7.77 [v5: $i] : ! [v6: $i] : (v1 = v0 | ~ (ip(v6, v5, v4, v3, v2) = v1) | ~ % 49.48/7.77 (ip(v6, v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 49.48/7.77 ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (ss3(v5, v4, v3, v2) = % 49.48/7.77 v1) | ~ (ss3(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 49.48/7.77 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (ss2(v5, v4, % 49.48/7.77 v3, v2) = v1) | ~ (ss2(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 49.48/7.77 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 49.48/7.77 (ss1(v5, v4, v3, v2) = v1) | ~ (ss1(v5, v4, v3, v2) = v0)) & ! [v0: % 49.48/7.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 49.48/7.77 : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (opposite(v5, v4, v3, v2) = v1) | % 49.48/7.77 ~ (opposite(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 49.48/7.77 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 49.48/7.77 (v1 = v0 | ~ (samesideline(v5, v4, v3, v2) = v1) | ~ (samesideline(v5, v4, % 49.48/7.77 v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 49.48/7.77 ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (il(v5, v4, v3, v2) = v1) | ~ % 49.48/7.77 (il(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 49.48/7.77 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 49.48/7.77 (v1 = v0 | ~ (perp(v5, v4, v3, v2) = v1) | ~ (perp(v5, v4, v3, v2) = v0)) & % 49.48/7.77 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 49.48/7.77 $i] : (v1 = v0 | ~ (ins(v5, v4, v3, v2) = v1) | ~ (ins(v5, v4, v3, v2) = % 49.48/7.77 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 49.48/7.77 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (le(v5, v4, % 49.48/7.77 v3, v2) = v1) | ~ (le(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 49.48/7.77 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 49.48/7.77 (insert(v5, v4, v3, v2) = v1) | ~ (insert(v5, v4, v3, v2) = v0)) & ! [v0: % 49.48/7.77 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 49.48/7.77 (v1 = v0 | ~ (ext(v5, v4, v3, v2) = v1) | ~ (ext(v5, v4, v3, v2) = v0)) & ! % 49.48/7.77 [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: % 49.48/7.77 $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ (s_e(v5, v4, v3, v2) = v1) | % 49.48/7.77 ~ (s_e(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 49.48/7.77 ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (erectAux(v4, v3, v2) = v1) | ~ % 49.48/7.77 (erectAux(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 49.48/7.77 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (erect(v4, v3, v2) = v1) | ~ % 49.48/7.77 (erect(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 49.48/7.77 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (erectAux21a(v4, v3, v2) = v1) | ~ % 49.48/7.77 (erectAux21a(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 49.48/7.77 ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (erect21a(v4, v3, v2) = v1) | ~ % 49.48/7.77 (erect21a(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 49.48/7.77 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (foot(v4, v3, v2) = v1) | ~ (foot(v4, % 49.48/7.77 v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 49.48/7.77 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (s_r(v4, v3, v2) = % 49.48/7.77 v1) | ~ (s_r(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 49.48/7.77 : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (isomidpoint(v4, v3, v2) = v1) | % 49.48/7.77 ~ (isomidpoint(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 49.48/7.77 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 49.48/7.77 (s_m(v4, v3, v2) = v1) | ~ (s_m(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 49.48/7.77 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (c63(v4, v3, % 49.48/7.77 v2) = v1) | ~ (c63(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 49.48/7.77 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | % 49.48/7.77 ~ (sameside(v4, v3, v2) = v1) | ~ (sameside(v4, v3, v2) = v0)) & ! [v0: % 49.48/7.77 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 49.48/7.77 : ! [v4: $i] : (v1 = v0 | ~ (s_col(v4, v3, v2) = v1) | ~ (s_col(v4, v3, v2) % 49.48/7.77 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 49.48/7.77 $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (s_t(v4, v3, v2) = v1) | ~ % 49.48/7.77 (s_t(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 49.48/7.77 $i] : (v1 = v0 | ~ (midpoint(v3, v2) = v1) | ~ (midpoint(v3, v2) = v0)) & % 49.48/7.77 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (s(v3, % 49.48/7.77 v2) = v1) | ~ (s(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 49.48/7.77 $i] : ! [v3: $i] : (v1 = v0 | ~ (pointOffLine(v3, v2) = v1) | ~ % 49.48/7.77 (pointOffLine(v3, v2) = v0)) % 49.48/7.77 % 49.48/7.77 Further assumptions not needed in the proof: % 49.48/7.77 -------------------------------------------- % 49.48/7.77 aA1, aA2, aA3, aA4, aA5, aA6, aA7, aA9, aExtCol2, aExtPerp, aExtPerp2, % 49.48/7.77 aExtPerp3, aExtPerp4, aExtPerp5, aExtPerp6, aExtSameSide1, aNarbouxLemma1, % 49.48/7.77 aSatz2_1, aSatz2_11, aSatz2_12, aSatz2_13, aSatz2_14, aSatz2_15, aSatz2_2, % 49.48/7.77 aSatz2_3, aSatz2_4, aSatz2_5, aSatz2_8, aSatz3_1, aSatz3_13c, aSatz3_14a, % 49.48/7.77 aSatz3_14b, aSatz3_17, aSatz3_3, aSatz3_4, aSatz3_5a, aSatz3_5b, aSatz3_6a, % 49.48/7.77 aSatz3_6b, aSatz3_7a, aSatz3_7b, aSatz4_11a, aSatz4_11b, aSatz4_11c, aSatz4_11e, % 49.48/7.77 aSatz4_12, aSatz4_12b, aSatz4_13, aSatz4_14, aSatz4_16, aSatz4_17, aSatz4_18, % 49.48/7.77 aSatz4_19, aSatz4_2, aSatz4_3, aSatz4_5, aSatz4_6, aSatz5_1, aSatz5_10, % 49.48/7.77 aSatz5_11, aSatz5_12a1, aSatz5_12a2, aSatz5_2, aSatz5_3, aSatz5_5a, aSatz5_5b, % 49.48/7.77 aSatz5_6, aSatz5_7, aSatz5_8, aSatz5_9, aSatz6_11a, aSatz6_11b, aSatz6_13b, % 49.48/7.77 aSatz6_15b, aSatz6_15c, aSatz6_15d, aSatz6_16a, aSatz6_16b, aSatz6_17a, % 49.48/7.77 aSatz6_17b, aSatz6_18, aSatz6_21, aSatz6_25, aSatz6_28, aSatz6_2a, aSatz6_2b, % 49.48/7.77 aSatz6_3a, aSatz6_3b, aSatz6_4a, aSatz6_4b, aSatz6_5, aSatz6_6, aSatz6_7, % 49.48/7.77 aSatz7_10a, aSatz7_10b, aSatz7_13, aSatz7_15a, aSatz7_15b, aSatz7_16a, % 49.48/7.77 aSatz7_16b, aSatz7_17, aSatz7_18, aSatz7_19, aSatz7_2, aSatz7_20, aSatz7_21, % 49.48/7.77 aSatz7_22, aSatz7_22a, aSatz7_22b, aSatz7_25, aSatz7_3a, aSatz7_3b, aSatz7_4a, % 49.48/7.77 aSatz7_4b, aSatz7_6, aSatz7_7, aSatz7_8, aSatz7_9, aSatz8_10, aSatz8_12a, % 49.48/7.77 aSatz8_12b, aSatz8_13a, aSatz8_13b, aSatz8_14a, aSatz8_14b, aSatz8_14c, % 49.48/7.77 aSatz8_15, aSatz8_16a, aSatz8_16b, aSatz8_18, aSatz8_18a, aSatz8_2, aSatz8_20a, % 49.48/7.77 aSatz8_20b, aSatz8_21, aSatz8_21a, aSatz8_22, aSatz8_22b, aSatz8_24, aSatz8_24a, % 49.48/7.77 aSatz8_24b, aSatz8_3, aSatz8_4, aSatz8_5, aSatz8_6, aSatz8_7, aSatz8_8, % 49.48/7.77 aSatz8_9, aext1, aperp1, d_Defn2_10, d_Defn4_1, d_Defn4_10, d_Defn4_15, % 49.48/7.77 d_Defn4_4, d_Defn5_4, d_Defn7_1, d_Defn7_23, d_Defn8_1, d_Defn8_11a, % 49.48/7.77 d_Defn8_11b, d_Defn9_1 % 49.48/7.77 % 49.48/7.77 Those formulas are unsatisfiable: % 49.48/7.77 --------------------------------- % 49.48/7.77 % 49.48/7.77 Begin of proof % 49.48/7.77 | % 49.48/7.77 | ALPHA: (aA8) implies: % 49.48/7.77 | (1) ? [v0: int] : ? [v1: int] : ? [v2: int] : ( ~ (v2 = 0) & ~ (v1 = 0) % 49.48/7.77 | & ~ (v0 = 0) & s_t(gamma, alpha, beta) = v2 & s_t(beta, gamma, % 49.48/7.77 | alpha) = v1 & s_t(alpha, beta, gamma) = v0) % 49.48/7.77 | % 49.48/7.78 | ALPHA: (aSatz3_2) implies: % 49.48/7.78 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 49.48/7.78 | (s_t(v2, v1, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 49.48/7.78 | int] : ( ~ (v4 = 0) & s_t(v0, v1, v2) = v4)) % 49.48/7.78 | % 49.48/7.78 | ALPHA: (aSatz3_13a) implies: % 49.48/7.78 | (3) ~ (beta = alpha) % 49.48/7.78 | % 49.48/7.78 | ALPHA: (aSatz3_13b) implies: % 49.48/7.78 | (4) ~ (gamma = beta) % 49.48/7.78 | (5) $i(beta) % 49.48/7.78 | % 49.48/7.78 | ALPHA: (aSatz4_11d) implies: % 49.48/7.78 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (s_col(v0, v1, v2) = 0) | % 49.48/7.78 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | s_col(v1, v0, v2) = 0) % 49.48/7.78 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 49.48/7.78 | (s_col(v1, v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 49.48/7.78 | [v4: int] : ( ~ (v4 = 0) & s_col(v0, v1, v2) = v4)) % 49.48/7.78 | % 49.48/7.78 | ALPHA: (aSatz5_12b) implies: % 49.48/7.78 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 49.48/7.78 | (s_t(v0, v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 49.48/7.78 | any] : ? [v5: any] : ? [v6: any] : (le(v1, v2, v0, v2) = v6 & % 49.48/7.78 | le(v0, v1, v0, v2) = v5 & s_col(v0, v1, v2) = v4 & ( ~ (v6 = 0) | % 49.48/7.78 | ~ (v5 = 0) | ~ (v4 = 0)))) % 49.48/7.78 | % 49.48/7.78 | ALPHA: (aSatz6_13a) implies: % 49.48/7.78 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 49.48/7.78 | (s_t(v1, v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 49.48/7.78 | any] : ? [v5: any] : (sameside(v0, v1, v2) = v4 & le(v1, v0, v1, % 49.48/7.78 | v2) = v5 & ( ~ (v5 = 0) | ~ (v4 = 0)))) % 49.48/7.78 | % 49.48/7.78 | ALPHA: (aSatz6_15a) implies: % 49.48/7.78 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : % 49.48/7.78 | ! [v5: int] : (v5 = 0 | v4 = 0 | v3 = v0 | v2 = v0 | v1 = v0 | ~ % 49.48/7.78 | (sameside(v3, v0, v2) = v5) | ~ (sameside(v3, v0, v1) = v4) | ~ % 49.48/7.78 | $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v6: any] : ? [v7: % 49.48/7.78 | any] : (s_col(v3, v0, v1) = v7 & s_t(v1, v0, v2) = v6 & ( ~ (v7 = % 49.48/7.78 | 0) | ~ (v6 = 0)))) % 49.48/7.78 | % 49.48/7.78 | ALPHA: (d_insert) implies: % 49.48/7.78 | (11) $i(alpha) % 49.48/7.78 | (12) $i(gamma) % 49.48/7.78 | % 49.48/7.78 | ALPHA: (d_Defn6_1) implies: % 49.48/7.78 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 49.48/7.78 | (s_t(v1, v0, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 49.48/7.78 | any] : ? [v5: any] : (sameside(v0, v1, v2) = v4 & s_t(v1, v2, v0) % 49.48/7.78 | = v5 & ( ~ (v4 = 0) | v5 = 0))) % 49.48/7.79 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 49.48/7.79 | (s_t(v1, v2, v0) = v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v4: % 49.48/7.79 | any] : ? [v5: any] : (sameside(v0, v1, v2) = v4 & s_t(v1, v0, v2) % 49.48/7.79 | = v5 & ( ~ (v4 = 0) | v5 = 0))) % 49.48/7.79 | % 49.48/7.79 | ALPHA: (d_Defn9_7) implies: % 49.48/7.79 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 49.48/7.79 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 49.48/7.79 | $i(v1) | ~ $i(v0) | ? [v4: $i] : (ss1(v0, v1, v2, v3) = v4 & % 49.48/7.79 | s_col(v2, v3, v4) = 0 & $i(v4))) % 49.48/7.79 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 49.48/7.79 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 49.48/7.79 | $i(v1) | ~ $i(v0) | ? [v4: $i] : (ss2(v0, v1, v2, v3) = v4 & % 49.48/7.79 | s_col(v2, v3, v4) = 0 & $i(v4))) % 49.48/7.79 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 49.48/7.79 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 49.48/7.79 | $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_col(v2, v3, v0) % 49.48/7.79 | = v4)) % 49.48/7.79 | (18) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 49.48/7.79 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 49.48/7.79 | $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & s_col(v2, v3, v1) % 49.48/7.79 | = v4)) % 49.48/7.79 | (19) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 49.48/7.79 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 49.48/7.79 | $i(v1) | ~ $i(v0) | ? [v4: $i] : ( ~ (v4 = v0) & ss1(v0, v1, v2, % 49.48/7.79 | v3) = v4 & $i(v4))) % 49.48/7.79 | (20) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 49.48/7.79 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 49.48/7.79 | $i(v1) | ~ $i(v0) | ? [v4: $i] : ( ~ (v4 = v1) & ss2(v0, v1, v2, % 49.48/7.79 | v3) = v4 & $i(v4))) % 49.48/7.79 | (21) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 49.48/7.79 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 49.48/7.79 | $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : (ss3(v0, v1, v2, % 49.48/7.79 | v3) = v5 & ss1(v0, v1, v2, v3) = v4 & s_t(v0, v4, v5) = 0 & % 49.48/7.79 | $i(v5) & $i(v4))) % 49.48/7.79 | (22) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 49.48/7.79 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 49.48/7.79 | $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : (ss3(v0, v1, v2, % 49.48/7.79 | v3) = v5 & ss2(v0, v1, v2, v3) = v4 & s_t(v1, v4, v5) = 0 & % 49.48/7.79 | $i(v5) & $i(v4))) % 49.48/7.79 | (23) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 49.48/7.79 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 49.48/7.79 | $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : ( ~ (v5 = v4) & % 49.48/7.79 | ss3(v0, v1, v2, v3) = v4 & ss1(v0, v1, v2, v3) = v5 & $i(v5) & % 49.48/7.79 | $i(v4))) % 49.48/7.79 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 49.48/7.79 | (samesideline(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 49.48/7.79 | $i(v1) | ~ $i(v0) | ? [v4: $i] : ? [v5: $i] : ( ~ (v5 = v4) & % 49.48/7.79 | ss3(v0, v1, v2, v3) = v4 & ss2(v0, v1, v2, v3) = v5 & $i(v5) & % 49.48/7.79 | $i(v4))) % 49.48/7.79 | (25) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 49.48/7.79 | ! [v5: $i] : ! [v6: $i] : ! [v7: int] : (v7 = 0 | v6 = v5 | v6 = v1 % 49.48/7.79 | | v5 = v4 | v4 = v0 | v3 = v2 | ~ (samesideline(v0, v1, v2, v3) = % 49.48/7.79 | v7) | ~ (s_t(v1, v6, v5) = 0) | ~ (s_t(v0, v4, v5) = 0) | ~ % 49.48/7.79 | $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 49.48/7.79 | ~ $i(v0) | ? [v8: any] : ? [v9: any] : ? [v10: any] : ? [v11: % 49.48/7.79 | any] : (s_col(v2, v3, v6) = v9 & s_col(v2, v3, v4) = v8 & % 49.48/7.79 | s_col(v2, v3, v1) = v11 & s_col(v2, v3, v0) = v10 & ( ~ (v9 = 0) | % 49.48/7.79 | ~ (v8 = 0) | v11 = 0 | v10 = 0))) % 49.48/7.79 | % 49.48/7.79 | ALPHA: (function-axioms) implies: % 49.48/7.79 | (26) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 49.48/7.79 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (s_t(v4, v3, v2) = v1) | % 49.48/7.79 | ~ (s_t(v4, v3, v2) = v0)) % 49.48/7.79 | (27) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 49.48/7.79 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (s_col(v4, v3, v2) = v1) | % 49.48/7.79 | ~ (s_col(v4, v3, v2) = v0)) % 49.48/7.80 | (28) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 49.48/7.80 | : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (sameside(v4, v3, v2) = % 49.48/7.80 | v1) | ~ (sameside(v4, v3, v2) = v0)) % 49.48/7.80 | (29) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 49.48/7.80 | ! [v5: $i] : (v1 = v0 | ~ (ss1(v5, v4, v3, v2) = v1) | ~ (ss1(v5, % 49.48/7.80 | v4, v3, v2) = v0)) % 49.48/7.80 | (30) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 49.48/7.80 | ! [v5: $i] : (v1 = v0 | ~ (ss2(v5, v4, v3, v2) = v1) | ~ (ss2(v5, % 49.48/7.80 | v4, v3, v2) = v0)) % 49.48/7.80 | (31) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 49.48/7.80 | ! [v5: $i] : (v1 = v0 | ~ (ss3(v5, v4, v3, v2) = v1) | ~ (ss3(v5, % 49.48/7.80 | v4, v3, v2) = v0)) % 49.48/7.80 | % 49.48/7.80 | DELTA: instantiating (1) with fresh symbols all_172_0, all_172_1, all_172_2 % 49.48/7.80 | gives: % 49.48/7.80 | (32) ~ (all_172_0 = 0) & ~ (all_172_1 = 0) & ~ (all_172_2 = 0) & % 49.48/7.80 | s_t(gamma, alpha, beta) = all_172_0 & s_t(beta, gamma, alpha) = % 49.48/7.80 | all_172_1 & s_t(alpha, beta, gamma) = all_172_2 % 49.48/7.80 | % 49.48/7.80 | ALPHA: (32) implies: % 49.48/7.80 | (33) ~ (all_172_2 = 0) % 49.48/7.80 | (34) ~ (all_172_1 = 0) % 49.48/7.80 | (35) ~ (all_172_0 = 0) % 49.48/7.80 | (36) s_t(alpha, beta, gamma) = all_172_2 % 49.48/7.80 | (37) s_t(beta, gamma, alpha) = all_172_1 % 49.48/7.80 | (38) s_t(gamma, alpha, beta) = all_172_0 % 49.48/7.80 | % 49.48/7.80 | DELTA: instantiating (aExtSameSide2) with fresh symbols all_174_0, all_174_1, % 49.48/7.80 | all_174_2, all_174_3, all_174_4 gives: % 49.48/7.80 | (39) ~ (all_174_0 = 0) & ~ (all_174_3 = all_174_4) & % 49.48/7.80 | samesideline(all_174_2, all_174_1, all_174_3, all_174_4) = all_174_0 & % 49.48/7.80 | samesideline(all_174_2, all_174_1, all_174_4, all_174_3) = 0 & % 49.48/7.80 | $i(all_174_1) & $i(all_174_2) & $i(all_174_3) & $i(all_174_4) % 49.48/7.80 | % 49.48/7.80 | ALPHA: (39) implies: % 49.48/7.80 | (40) ~ (all_174_3 = all_174_4) % 49.48/7.80 | (41) ~ (all_174_0 = 0) % 49.48/7.80 | (42) $i(all_174_4) % 49.48/7.80 | (43) $i(all_174_3) % 49.48/7.80 | (44) $i(all_174_2) % 49.48/7.80 | (45) $i(all_174_1) % 49.48/7.80 | (46) samesideline(all_174_2, all_174_1, all_174_4, all_174_3) = 0 % 49.48/7.80 | (47) samesideline(all_174_2, all_174_1, all_174_3, all_174_4) = all_174_0 % 49.48/7.80 | % 49.48/7.80 | GROUND_INST: instantiating (2) with gamma, beta, alpha, all_172_2, simplifying % 49.48/7.80 | with (5), (11), (12), (36) gives: % 49.48/7.80 | (48) all_172_2 = 0 | ? [v0: int] : ( ~ (v0 = 0) & s_t(gamma, beta, alpha) % 49.48/7.80 | = v0) % 49.48/7.80 | % 49.48/7.80 | GROUND_INST: instantiating (14) with alpha, beta, gamma, all_172_1, % 49.48/7.80 | simplifying with (5), (11), (12), (37) gives: % 49.48/7.80 | (49) all_172_1 = 0 | ? [v0: any] : ? [v1: any] : (sameside(alpha, beta, % 49.48/7.80 | gamma) = v0 & s_t(beta, alpha, gamma) = v1 & ( ~ (v0 = 0) | v1 = % 49.48/7.80 | 0)) % 49.48/7.80 | % 49.48/7.80 | GROUND_INST: instantiating (9) with gamma, beta, alpha, all_172_1, simplifying % 49.48/7.80 | with (5), (11), (12), (37) gives: % 49.48/7.80 | (50) all_172_1 = 0 | ? [v0: any] : ? [v1: any] : (sameside(gamma, beta, % 49.48/7.80 | alpha) = v0 & le(beta, gamma, beta, alpha) = v1 & ( ~ (v1 = 0) | % 49.48/7.80 | ~ (v0 = 0))) % 49.48/7.80 | % 49.48/7.80 | GROUND_INST: instantiating (13) with gamma, beta, alpha, all_172_1, % 49.48/7.80 | simplifying with (5), (11), (12), (37) gives: % 49.48/7.80 | (51) all_172_1 = 0 | ? [v0: any] : ? [v1: any] : (sameside(gamma, beta, % 49.48/7.80 | alpha) = v0 & s_t(beta, alpha, gamma) = v1 & ( ~ (v0 = 0) | v1 = % 49.48/7.80 | 0)) % 49.48/7.80 | % 49.48/7.80 | GROUND_INST: instantiating (2) with beta, alpha, gamma, all_172_0, simplifying % 49.48/7.80 | with (5), (11), (12), (38) gives: % 49.48/7.80 | (52) all_172_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & s_t(beta, alpha, gamma) % 49.48/7.80 | = v0) % 49.48/7.80 | % 49.48/7.80 | GROUND_INST: instantiating (14) with beta, gamma, alpha, all_172_0, % 49.48/7.80 | simplifying with (5), (11), (12), (38) gives: % 49.48/7.80 | (53) all_172_0 = 0 | ? [v0: any] : ? [v1: any] : (sameside(beta, gamma, % 49.48/7.80 | alpha) = v0 & s_t(gamma, beta, alpha) = v1 & ( ~ (v0 = 0) | v1 = % 49.48/7.80 | 0)) % 49.48/7.80 | % 49.48/7.81 | GROUND_INST: instantiating (13) with alpha, gamma, beta, all_172_0, % 49.48/7.81 | simplifying with (5), (11), (12), (38) gives: % 49.48/7.81 | (54) all_172_0 = 0 | ? [v0: any] : ? [v1: any] : (sameside(alpha, gamma, % 49.48/7.81 | beta) = v0 & s_t(gamma, beta, alpha) = v1 & ( ~ (v0 = 0) | v1 = % 49.48/7.81 | 0)) % 49.48/7.81 | % 49.48/7.81 | GROUND_INST: instantiating (8) with gamma, alpha, beta, all_172_0, simplifying % 49.48/7.81 | with (5), (11), (12), (38) gives: % 49.48/7.81 | (55) all_172_0 = 0 | ? [v0: any] : ? [v1: any] : ? [v2: any] : % 49.48/7.81 | (le(gamma, alpha, gamma, beta) = v1 & le(alpha, beta, gamma, beta) = % 49.48/7.81 | v2 & s_col(gamma, alpha, beta) = v0 & ( ~ (v2 = 0) | ~ (v1 = 0) | % 49.48/7.81 | ~ (v0 = 0))) % 49.48/7.81 | % 49.48/7.81 | GROUND_INST: instantiating (24) with all_174_2, all_174_1, all_174_4, % 49.48/7.81 | all_174_3, simplifying with (42), (43), (44), (45), (46) gives: % 50.01/7.81 | (56) ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = v0) & ss3(all_174_2, all_174_1, % 50.01/7.81 | all_174_4, all_174_3) = v0 & ss2(all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3) = v1 & $i(v1) & $i(v0)) % 50.01/7.81 | % 50.01/7.81 | GROUND_INST: instantiating (23) with all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3, simplifying with (42), (43), (44), (45), (46) gives: % 50.01/7.81 | (57) ? [v0: $i] : ? [v1: $i] : ( ~ (v1 = v0) & ss3(all_174_2, all_174_1, % 50.01/7.81 | all_174_4, all_174_3) = v0 & ss1(all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3) = v1 & $i(v1) & $i(v0)) % 50.01/7.81 | % 50.01/7.81 | GROUND_INST: instantiating (22) with all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3, simplifying with (42), (43), (44), (45), (46) gives: % 50.01/7.81 | (58) ? [v0: $i] : ? [v1: $i] : (ss3(all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3) = v1 & ss2(all_174_2, all_174_1, all_174_4, all_174_3) % 50.01/7.81 | = v0 & s_t(all_174_1, v0, v1) = 0 & $i(v1) & $i(v0)) % 50.01/7.81 | % 50.01/7.81 | GROUND_INST: instantiating (21) with all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3, simplifying with (42), (43), (44), (45), (46) gives: % 50.01/7.81 | (59) ? [v0: $i] : ? [v1: $i] : (ss3(all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3) = v1 & ss1(all_174_2, all_174_1, all_174_4, all_174_3) % 50.01/7.81 | = v0 & s_t(all_174_2, v0, v1) = 0 & $i(v1) & $i(v0)) % 50.01/7.81 | % 50.01/7.81 | GROUND_INST: instantiating (20) with all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3, simplifying with (42), (43), (44), (45), (46) gives: % 50.01/7.81 | (60) ? [v0: any] : ( ~ (v0 = all_174_1) & ss2(all_174_2, all_174_1, % 50.01/7.81 | all_174_4, all_174_3) = v0 & $i(v0)) % 50.01/7.81 | % 50.01/7.81 | GROUND_INST: instantiating (19) with all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3, simplifying with (42), (43), (44), (45), (46) gives: % 50.01/7.81 | (61) ? [v0: any] : ( ~ (v0 = all_174_2) & ss1(all_174_2, all_174_1, % 50.01/7.81 | all_174_4, all_174_3) = v0 & $i(v0)) % 50.01/7.81 | % 50.01/7.81 | GROUND_INST: instantiating (18) with all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3, simplifying with (42), (43), (44), (45), (46) gives: % 50.01/7.81 | (62) ? [v0: int] : ( ~ (v0 = 0) & s_col(all_174_4, all_174_3, all_174_1) = % 50.01/7.81 | v0) % 50.01/7.81 | % 50.01/7.81 | GROUND_INST: instantiating (17) with all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3, simplifying with (42), (43), (44), (45), (46) gives: % 50.01/7.81 | (63) ? [v0: int] : ( ~ (v0 = 0) & s_col(all_174_4, all_174_3, all_174_2) = % 50.01/7.81 | v0) % 50.01/7.81 | % 50.01/7.81 | GROUND_INST: instantiating (16) with all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3, simplifying with (42), (43), (44), (45), (46) gives: % 50.01/7.81 | (64) ? [v0: $i] : (ss2(all_174_2, all_174_1, all_174_4, all_174_3) = v0 & % 50.01/7.81 | s_col(all_174_4, all_174_3, v0) = 0 & $i(v0)) % 50.01/7.81 | % 50.01/7.81 | GROUND_INST: instantiating (15) with all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3, simplifying with (42), (43), (44), (45), (46) gives: % 50.01/7.81 | (65) ? [v0: $i] : (ss1(all_174_2, all_174_1, all_174_4, all_174_3) = v0 & % 50.01/7.81 | s_col(all_174_4, all_174_3, v0) = 0 & $i(v0)) % 50.01/7.81 | % 50.01/7.81 | DELTA: instantiating (63) with fresh symbol all_183_0 gives: % 50.01/7.81 | (66) ~ (all_183_0 = 0) & s_col(all_174_4, all_174_3, all_174_2) = % 50.01/7.81 | all_183_0 % 50.01/7.81 | % 50.01/7.81 | ALPHA: (66) implies: % 50.01/7.81 | (67) ~ (all_183_0 = 0) % 50.01/7.81 | (68) s_col(all_174_4, all_174_3, all_174_2) = all_183_0 % 50.01/7.81 | % 50.01/7.81 | DELTA: instantiating (62) with fresh symbol all_185_0 gives: % 50.01/7.81 | (69) ~ (all_185_0 = 0) & s_col(all_174_4, all_174_3, all_174_1) = % 50.01/7.81 | all_185_0 % 50.01/7.81 | % 50.01/7.81 | ALPHA: (69) implies: % 50.01/7.81 | (70) ~ (all_185_0 = 0) % 50.01/7.81 | (71) s_col(all_174_4, all_174_3, all_174_1) = all_185_0 % 50.01/7.81 | % 50.01/7.81 | DELTA: instantiating (60) with fresh symbol all_187_0 gives: % 50.01/7.81 | (72) ~ (all_187_0 = all_174_1) & ss2(all_174_2, all_174_1, all_174_4, % 50.01/7.81 | all_174_3) = all_187_0 & $i(all_187_0) % 50.01/7.81 | % 50.01/7.81 | ALPHA: (72) implies: % 50.01/7.81 | (73) ~ (all_187_0 = all_174_1) % 50.01/7.81 | (74) ss2(all_174_2, all_174_1, all_174_4, all_174_3) = all_187_0 % 50.01/7.81 | % 50.01/7.81 | DELTA: instantiating (65) with fresh symbol all_189_0 gives: % 50.01/7.81 | (75) ss1(all_174_2, all_174_1, all_174_4, all_174_3) = all_189_0 & % 50.01/7.81 | s_col(all_174_4, all_174_3, all_189_0) = 0 & $i(all_189_0) % 50.01/7.81 | % 50.01/7.81 | ALPHA: (75) implies: % 50.01/7.81 | (76) s_col(all_174_4, all_174_3, all_189_0) = 0 % 50.01/7.81 | (77) ss1(all_174_2, all_174_1, all_174_4, all_174_3) = all_189_0 % 50.01/7.81 | % 50.01/7.81 | DELTA: instantiating (64) with fresh symbol all_191_0 gives: % 50.01/7.81 | (78) ss2(all_174_2, all_174_1, all_174_4, all_174_3) = all_191_0 & % 50.01/7.81 | s_col(all_174_4, all_174_3, all_191_0) = 0 & $i(all_191_0) % 50.01/7.81 | % 50.01/7.82 | ALPHA: (78) implies: % 50.01/7.82 | (79) $i(all_191_0) % 50.01/7.82 | (80) s_col(all_174_4, all_174_3, all_191_0) = 0 % 50.01/7.82 | (81) ss2(all_174_2, all_174_1, all_174_4, all_174_3) = all_191_0 % 50.01/7.82 | % 50.01/7.82 | DELTA: instantiating (61) with fresh symbol all_193_0 gives: % 50.01/7.82 | (82) ~ (all_193_0 = all_174_2) & ss1(all_174_2, all_174_1, all_174_4, % 50.01/7.82 | all_174_3) = all_193_0 & $i(all_193_0) % 50.01/7.82 | % 50.01/7.82 | ALPHA: (82) implies: % 50.01/7.82 | (83) ~ (all_193_0 = all_174_2) % 50.01/7.82 | (84) $i(all_193_0) % 50.01/7.82 | (85) ss1(all_174_2, all_174_1, all_174_4, all_174_3) = all_193_0 % 50.01/7.82 | % 50.01/7.82 | DELTA: instantiating (59) with fresh symbols all_195_0, all_195_1 gives: % 50.01/7.82 | (86) ss3(all_174_2, all_174_1, all_174_4, all_174_3) = all_195_0 & % 50.01/7.82 | ss1(all_174_2, all_174_1, all_174_4, all_174_3) = all_195_1 & % 50.01/7.82 | s_t(all_174_2, all_195_1, all_195_0) = 0 & $i(all_195_0) & % 50.01/7.82 | $i(all_195_1) % 50.01/7.82 | % 50.01/7.82 | ALPHA: (86) implies: % 50.01/7.82 | (87) s_t(all_174_2, all_195_1, all_195_0) = 0 % 50.01/7.82 | (88) ss1(all_174_2, all_174_1, all_174_4, all_174_3) = all_195_1 % 50.01/7.82 | (89) ss3(all_174_2, all_174_1, all_174_4, all_174_3) = all_195_0 % 50.01/7.82 | % 50.01/7.82 | DELTA: instantiating (56) with fresh symbols all_197_0, all_197_1 gives: % 50.01/7.82 | (90) ~ (all_197_0 = all_197_1) & ss3(all_174_2, all_174_1, all_174_4, % 50.01/7.82 | all_174_3) = all_197_1 & ss2(all_174_2, all_174_1, all_174_4, % 50.01/7.82 | all_174_3) = all_197_0 & $i(all_197_0) & $i(all_197_1) % 50.01/7.82 | % 50.01/7.82 | ALPHA: (90) implies: % 50.01/7.82 | (91) ~ (all_197_0 = all_197_1) % 50.01/7.82 | (92) $i(all_197_1) % 50.01/7.82 | (93) ss2(all_174_2, all_174_1, all_174_4, all_174_3) = all_197_0 % 50.01/7.82 | (94) ss3(all_174_2, all_174_1, all_174_4, all_174_3) = all_197_1 % 50.01/7.82 | % 50.01/7.82 | DELTA: instantiating (58) with fresh symbols all_199_0, all_199_1 gives: % 50.01/7.82 | (95) ss3(all_174_2, all_174_1, all_174_4, all_174_3) = all_199_0 & % 50.01/7.82 | ss2(all_174_2, all_174_1, all_174_4, all_174_3) = all_199_1 & % 50.01/7.82 | s_t(all_174_1, all_199_1, all_199_0) = 0 & $i(all_199_0) & % 50.01/7.82 | $i(all_199_1) % 50.01/7.82 | % 50.01/7.82 | ALPHA: (95) implies: % 50.01/7.82 | (96) s_t(all_174_1, all_199_1, all_199_0) = 0 % 50.01/7.82 | (97) ss2(all_174_2, all_174_1, all_174_4, all_174_3) = all_199_1 % 50.01/7.82 | (98) ss3(all_174_2, all_174_1, all_174_4, all_174_3) = all_199_0 % 50.01/7.82 | % 50.01/7.82 | DELTA: instantiating (57) with fresh symbols all_201_0, all_201_1 gives: % 50.01/7.82 | (99) ~ (all_201_0 = all_201_1) & ss3(all_174_2, all_174_1, all_174_4, % 50.01/7.82 | all_174_3) = all_201_1 & ss1(all_174_2, all_174_1, all_174_4, % 50.01/7.82 | all_174_3) = all_201_0 & $i(all_201_0) & $i(all_201_1) % 50.01/7.82 | % 50.01/7.82 | ALPHA: (99) implies: % 50.01/7.82 | (100) ~ (all_201_0 = all_201_1) % 50.01/7.82 | (101) ss1(all_174_2, all_174_1, all_174_4, all_174_3) = all_201_0 % 50.01/7.82 | (102) ss3(all_174_2, all_174_1, all_174_4, all_174_3) = all_201_1 % 50.01/7.82 | % 50.01/7.82 | BETA: splitting (52) gives: % 50.01/7.82 | % 50.01/7.82 | Case 1: % 50.01/7.82 | | % 50.01/7.82 | | (103) all_172_0 = 0 % 50.01/7.82 | | % 50.01/7.82 | | REDUCE: (35), (103) imply: % 50.01/7.82 | | (104) $false % 50.01/7.82 | | % 50.01/7.82 | | CLOSE: (104) is inconsistent. % 50.01/7.82 | | % 50.01/7.82 | Case 2: % 50.01/7.82 | | % 50.01/7.82 | | (105) ? [v0: int] : ( ~ (v0 = 0) & s_t(beta, alpha, gamma) = v0) % 50.01/7.82 | | % 50.01/7.82 | | DELTA: instantiating (105) with fresh symbol all_227_0 gives: % 50.01/7.82 | | (106) ~ (all_227_0 = 0) & s_t(beta, alpha, gamma) = all_227_0 % 50.01/7.82 | | % 50.01/7.82 | | ALPHA: (106) implies: % 50.01/7.82 | | (107) ~ (all_227_0 = 0) % 50.01/7.82 | | (108) s_t(beta, alpha, gamma) = all_227_0 % 50.01/7.82 | | % 50.01/7.82 | | BETA: splitting (48) gives: % 50.01/7.82 | | % 50.01/7.82 | | Case 1: % 50.01/7.82 | | | % 50.01/7.82 | | | (109) all_172_2 = 0 % 50.01/7.82 | | | % 50.01/7.82 | | | REDUCE: (33), (109) imply: % 50.01/7.82 | | | (110) $false % 50.01/7.82 | | | % 50.01/7.82 | | | CLOSE: (110) is inconsistent. % 50.01/7.82 | | | % 50.01/7.82 | | Case 2: % 50.01/7.82 | | | % 50.01/7.82 | | | (111) ? [v0: int] : ( ~ (v0 = 0) & s_t(gamma, beta, alpha) = v0) % 50.01/7.82 | | | % 50.01/7.82 | | | DELTA: instantiating (111) with fresh symbol all_257_0 gives: % 50.01/7.82 | | | (112) ~ (all_257_0 = 0) & s_t(gamma, beta, alpha) = all_257_0 % 50.01/7.82 | | | % 50.01/7.82 | | | ALPHA: (112) implies: % 50.01/7.82 | | | (113) ~ (all_257_0 = 0) % 50.01/7.82 | | | (114) s_t(gamma, beta, alpha) = all_257_0 % 50.01/7.82 | | | % 50.01/7.82 | | | BETA: splitting (54) gives: % 50.01/7.82 | | | % 50.01/7.82 | | | Case 1: % 50.01/7.82 | | | | % 50.01/7.82 | | | | (115) all_172_0 = 0 % 50.01/7.82 | | | | % 50.01/7.82 | | | | REDUCE: (35), (115) imply: % 50.01/7.82 | | | | (116) $false % 50.01/7.82 | | | | % 50.01/7.82 | | | | CLOSE: (116) is inconsistent. % 50.01/7.82 | | | | % 50.01/7.82 | | | Case 2: % 50.01/7.82 | | | | % 50.01/7.82 | | | | (117) ? [v0: any] : ? [v1: any] : (sameside(alpha, gamma, beta) = % 50.01/7.82 | | | | v0 & s_t(gamma, beta, alpha) = v1 & ( ~ (v0 = 0) | v1 = 0)) % 50.01/7.82 | | | | % 50.01/7.82 | | | | DELTA: instantiating (117) with fresh symbols all_297_0, all_297_1 % 50.01/7.82 | | | | gives: % 50.01/7.82 | | | | (118) sameside(alpha, gamma, beta) = all_297_1 & s_t(gamma, beta, % 50.01/7.82 | | | | alpha) = all_297_0 & ( ~ (all_297_1 = 0) | all_297_0 = 0) % 50.01/7.82 | | | | % 50.01/7.82 | | | | ALPHA: (118) implies: % 50.01/7.82 | | | | (119) s_t(gamma, beta, alpha) = all_297_0 % 50.01/7.82 | | | | % 50.01/7.82 | | | | BETA: splitting (50) gives: % 50.01/7.82 | | | | % 50.01/7.82 | | | | Case 1: % 50.01/7.82 | | | | | % 50.01/7.82 | | | | | (120) all_172_1 = 0 % 50.01/7.82 | | | | | % 50.01/7.82 | | | | | REDUCE: (34), (120) imply: % 50.01/7.82 | | | | | (121) $false % 50.01/7.82 | | | | | % 50.01/7.82 | | | | | CLOSE: (121) is inconsistent. % 50.01/7.82 | | | | | % 50.01/7.82 | | | | Case 2: % 50.01/7.82 | | | | | % 50.01/7.82 | | | | | (122) ? [v0: any] : ? [v1: any] : (sameside(gamma, beta, alpha) = % 50.01/7.82 | | | | | v0 & le(beta, gamma, beta, alpha) = v1 & ( ~ (v1 = 0) | ~ % 50.01/7.82 | | | | | (v0 = 0))) % 50.01/7.82 | | | | | % 50.01/7.82 | | | | | DELTA: instantiating (122) with fresh symbols all_302_0, all_302_1 % 50.01/7.82 | | | | | gives: % 50.01/7.83 | | | | | (123) sameside(gamma, beta, alpha) = all_302_1 & le(beta, gamma, % 50.01/7.83 | | | | | beta, alpha) = all_302_0 & ( ~ (all_302_0 = 0) | ~ % 50.01/7.83 | | | | | (all_302_1 = 0)) % 50.01/7.83 | | | | | % 50.01/7.83 | | | | | ALPHA: (123) implies: % 50.01/7.83 | | | | | (124) sameside(gamma, beta, alpha) = all_302_1 % 50.01/7.83 | | | | | % 50.01/7.83 | | | | | BETA: splitting (49) gives: % 50.01/7.83 | | | | | % 50.01/7.83 | | | | | Case 1: % 50.01/7.83 | | | | | | % 50.01/7.83 | | | | | | (125) all_172_1 = 0 % 50.01/7.83 | | | | | | % 50.01/7.83 | | | | | | REDUCE: (34), (125) imply: % 50.01/7.83 | | | | | | (126) $false % 50.01/7.83 | | | | | | % 50.01/7.83 | | | | | | CLOSE: (126) is inconsistent. % 50.01/7.83 | | | | | | % 50.01/7.83 | | | | | Case 2: % 50.01/7.83 | | | | | | % 50.01/7.83 | | | | | | (127) ? [v0: any] : ? [v1: any] : (sameside(alpha, beta, gamma) % 50.01/7.83 | | | | | | = v0 & s_t(beta, alpha, gamma) = v1 & ( ~ (v0 = 0) | v1 = % 50.01/7.83 | | | | | | 0)) % 50.01/7.83 | | | | | | % 50.01/7.83 | | | | | | DELTA: instantiating (127) with fresh symbols all_307_0, all_307_1 % 50.01/7.83 | | | | | | gives: % 50.01/7.83 | | | | | | (128) sameside(alpha, beta, gamma) = all_307_1 & s_t(beta, alpha, % 50.01/7.83 | | | | | | gamma) = all_307_0 & ( ~ (all_307_1 = 0) | all_307_0 = 0) % 50.01/7.83 | | | | | | % 50.01/7.83 | | | | | | ALPHA: (128) implies: % 50.01/7.83 | | | | | | (129) s_t(beta, alpha, gamma) = all_307_0 % 50.01/7.83 | | | | | | % 50.01/7.83 | | | | | | BETA: splitting (53) gives: % 50.01/7.83 | | | | | | % 50.01/7.83 | | | | | | Case 1: % 50.01/7.83 | | | | | | | % 50.01/7.83 | | | | | | | (130) all_172_0 = 0 % 50.01/7.83 | | | | | | | % 50.01/7.83 | | | | | | | REDUCE: (35), (130) imply: % 50.01/7.83 | | | | | | | (131) $false % 50.01/7.83 | | | | | | | % 50.01/7.83 | | | | | | | CLOSE: (131) is inconsistent. % 50.01/7.83 | | | | | | | % 50.01/7.83 | | | | | | Case 2: % 50.01/7.83 | | | | | | | % 50.01/7.83 | | | | | | | (132) ? [v0: any] : ? [v1: any] : (sameside(beta, gamma, % 50.01/7.83 | | | | | | | alpha) = v0 & s_t(gamma, beta, alpha) = v1 & ( ~ (v0 % 50.01/7.83 | | | | | | | = 0) | v1 = 0)) % 50.01/7.83 | | | | | | | % 50.01/7.83 | | | | | | | DELTA: instantiating (132) with fresh symbols all_322_0, all_322_1 % 50.01/7.83 | | | | | | | gives: % 50.01/7.83 | | | | | | | (133) sameside(beta, gamma, alpha) = all_322_1 & s_t(gamma, % 50.01/7.83 | | | | | | | beta, alpha) = all_322_0 & ( ~ (all_322_1 = 0) | % 50.01/7.83 | | | | | | | all_322_0 = 0) % 50.01/7.83 | | | | | | | % 50.01/7.83 | | | | | | | ALPHA: (133) implies: % 50.01/7.83 | | | | | | | (134) s_t(gamma, beta, alpha) = all_322_0 % 50.01/7.83 | | | | | | | (135) ~ (all_322_1 = 0) | all_322_0 = 0 % 50.01/7.83 | | | | | | | % 50.01/7.83 | | | | | | | BETA: splitting (51) gives: % 50.01/7.83 | | | | | | | % 50.01/7.83 | | | | | | | Case 1: % 50.01/7.83 | | | | | | | | % 50.01/7.83 | | | | | | | | (136) all_172_1 = 0 % 50.01/7.83 | | | | | | | | % 50.01/7.83 | | | | | | | | REDUCE: (34), (136) imply: % 50.01/7.83 | | | | | | | | (137) $false % 50.01/7.83 | | | | | | | | % 50.01/7.83 | | | | | | | | CLOSE: (137) is inconsistent. % 50.01/7.83 | | | | | | | | % 50.01/7.83 | | | | | | | Case 2: % 50.01/7.83 | | | | | | | | % 50.01/7.83 | | | | | | | | (138) ? [v0: any] : ? [v1: any] : (sameside(gamma, beta, % 50.01/7.83 | | | | | | | | alpha) = v0 & s_t(beta, alpha, gamma) = v1 & ( ~ % 50.01/7.83 | | | | | | | | (v0 = 0) | v1 = 0)) % 50.01/7.83 | | | | | | | | % 50.01/7.83 | | | | | | | | DELTA: instantiating (138) with fresh symbols all_337_0, % 50.01/7.83 | | | | | | | | all_337_1 gives: % 50.01/7.83 | | | | | | | | (139) sameside(gamma, beta, alpha) = all_337_1 & s_t(beta, % 50.01/7.83 | | | | | | | | alpha, gamma) = all_337_0 & ( ~ (all_337_1 = 0) | % 50.01/7.83 | | | | | | | | all_337_0 = 0) % 50.01/7.83 | | | | | | | | % 50.01/7.83 | | | | | | | | ALPHA: (139) implies: % 50.01/7.83 | | | | | | | | (140) s_t(beta, alpha, gamma) = all_337_0 % 50.01/7.83 | | | | | | | | (141) sameside(gamma, beta, alpha) = all_337_1 % 50.01/7.83 | | | | | | | | (142) ~ (all_337_1 = 0) | all_337_0 = 0 % 50.01/7.83 | | | | | | | | % 50.01/7.83 | | | | | | | | BETA: splitting (55) gives: % 50.01/7.83 | | | | | | | | % 50.01/7.83 | | | | | | | | Case 1: % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | (143) all_172_0 = 0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | REDUCE: (35), (143) imply: % 50.01/7.83 | | | | | | | | | (144) $false % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | CLOSE: (144) is inconsistent. % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | Case 2: % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (26) with all_307_0, all_337_0, % 50.01/7.83 | | | | | | | | | gamma, alpha, beta, simplifying with (129), (140) % 50.01/7.83 | | | | | | | | | gives: % 50.01/7.83 | | | | | | | | | (145) all_337_0 = all_307_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (26) with all_227_0, all_337_0, % 50.01/7.83 | | | | | | | | | gamma, alpha, beta, simplifying with (108), (140) % 50.01/7.83 | | | | | | | | | gives: % 50.01/7.83 | | | | | | | | | (146) all_337_0 = all_227_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (26) with all_297_0, all_322_0, % 50.01/7.83 | | | | | | | | | alpha, beta, gamma, simplifying with (119), (134) % 50.01/7.83 | | | | | | | | | gives: % 50.01/7.83 | | | | | | | | | (147) all_322_0 = all_297_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (26) with all_257_0, all_322_0, % 50.01/7.83 | | | | | | | | | alpha, beta, gamma, simplifying with (114), (134) % 50.01/7.83 | | | | | | | | | gives: % 50.01/7.83 | | | | | | | | | (148) all_322_0 = all_257_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (28) with all_302_1, all_337_1, % 50.01/7.83 | | | | | | | | | alpha, beta, gamma, simplifying with (124), (141) % 50.01/7.83 | | | | | | | | | gives: % 50.01/7.83 | | | | | | | | | (149) all_337_1 = all_302_1 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (29) with all_189_0, all_195_1, % 50.01/7.83 | | | | | | | | | all_174_3, all_174_4, all_174_1, all_174_2, % 50.01/7.83 | | | | | | | | | simplifying with (77), (88) gives: % 50.01/7.83 | | | | | | | | | (150) all_195_1 = all_189_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (29) with all_195_1, all_201_0, % 50.01/7.83 | | | | | | | | | all_174_3, all_174_4, all_174_1, all_174_2, % 50.01/7.83 | | | | | | | | | simplifying with (88), (101) gives: % 50.01/7.83 | | | | | | | | | (151) all_201_0 = all_195_1 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (29) with all_193_0, all_201_0, % 50.01/7.83 | | | | | | | | | all_174_3, all_174_4, all_174_1, all_174_2, % 50.01/7.83 | | | | | | | | | simplifying with (85), (101) gives: % 50.01/7.83 | | | | | | | | | (152) all_201_0 = all_193_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (30) with all_191_0, all_197_0, % 50.01/7.83 | | | | | | | | | all_174_3, all_174_4, all_174_1, all_174_2, % 50.01/7.83 | | | | | | | | | simplifying with (81), (93) gives: % 50.01/7.83 | | | | | | | | | (153) all_197_0 = all_191_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (30) with all_197_0, all_199_1, % 50.01/7.83 | | | | | | | | | all_174_3, all_174_4, all_174_1, all_174_2, % 50.01/7.83 | | | | | | | | | simplifying with (93), (97) gives: % 50.01/7.83 | | | | | | | | | (154) all_199_1 = all_197_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (30) with all_187_0, all_199_1, % 50.01/7.83 | | | | | | | | | all_174_3, all_174_4, all_174_1, all_174_2, % 50.01/7.83 | | | | | | | | | simplifying with (74), (97) gives: % 50.01/7.83 | | | | | | | | | (155) all_199_1 = all_187_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (31) with all_197_1, all_199_0, % 50.01/7.83 | | | | | | | | | all_174_3, all_174_4, all_174_1, all_174_2, % 50.01/7.83 | | | | | | | | | simplifying with (94), (98) gives: % 50.01/7.83 | | | | | | | | | (156) all_199_0 = all_197_1 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (31) with all_199_0, all_201_1, % 50.01/7.83 | | | | | | | | | all_174_3, all_174_4, all_174_1, all_174_2, % 50.01/7.83 | | | | | | | | | simplifying with (98), (102) gives: % 50.01/7.83 | | | | | | | | | (157) all_201_1 = all_199_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | GROUND_INST: instantiating (31) with all_195_0, all_201_1, % 50.01/7.83 | | | | | | | | | all_174_3, all_174_4, all_174_1, all_174_2, % 50.01/7.83 | | | | | | | | | simplifying with (89), (102) gives: % 50.01/7.83 | | | | | | | | | (158) all_201_1 = all_195_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | COMBINE_EQS: (145), (146) imply: % 50.01/7.83 | | | | | | | | | (159) all_307_0 = all_227_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | COMBINE_EQS: (147), (148) imply: % 50.01/7.83 | | | | | | | | | (160) all_297_0 = all_257_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | COMBINE_EQS: (151), (152) imply: % 50.01/7.83 | | | | | | | | | (161) all_195_1 = all_193_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | SIMP: (161) implies: % 50.01/7.83 | | | | | | | | | (162) all_195_1 = all_193_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | COMBINE_EQS: (157), (158) imply: % 50.01/7.83 | | | | | | | | | (163) all_199_0 = all_195_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | SIMP: (163) implies: % 50.01/7.83 | | | | | | | | | (164) all_199_0 = all_195_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | COMBINE_EQS: (156), (164) imply: % 50.01/7.83 | | | | | | | | | (165) all_197_1 = all_195_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | SIMP: (165) implies: % 50.01/7.83 | | | | | | | | | (166) all_197_1 = all_195_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | COMBINE_EQS: (154), (155) imply: % 50.01/7.83 | | | | | | | | | (167) all_197_0 = all_187_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | SIMP: (167) implies: % 50.01/7.83 | | | | | | | | | (168) all_197_0 = all_187_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | COMBINE_EQS: (153), (168) imply: % 50.01/7.83 | | | | | | | | | (169) all_191_0 = all_187_0 % 50.01/7.83 | | | | | | | | | % 50.01/7.83 | | | | | | | | | SIMP: (169) implies: % 50.01/7.83 | | | | | | | | | (170) all_191_0 = all_187_0 % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | COMBINE_EQS: (150), (162) imply: % 50.01/7.84 | | | | | | | | | (171) all_193_0 = all_189_0 % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | SIMP: (171) implies: % 50.01/7.84 | | | | | | | | | (172) all_193_0 = all_189_0 % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | COMBINE_EQS: (152), (172) imply: % 50.01/7.84 | | | | | | | | | (173) all_201_0 = all_189_0 % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | REDUCE: (100), (158), (173) imply: % 50.01/7.84 | | | | | | | | | (174) ~ (all_195_0 = all_189_0) % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | SIMP: (174) implies: % 50.01/7.84 | | | | | | | | | (175) ~ (all_195_0 = all_189_0) % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | REDUCE: (91), (166), (168) imply: % 50.01/7.84 | | | | | | | | | (176) ~ (all_195_0 = all_187_0) % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | SIMP: (176) implies: % 50.01/7.84 | | | | | | | | | (177) ~ (all_195_0 = all_187_0) % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | REDUCE: (83), (172) imply: % 50.01/7.84 | | | | | | | | | (178) ~ (all_189_0 = all_174_2) % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | REDUCE: (80), (170) imply: % 50.01/7.84 | | | | | | | | | (179) s_col(all_174_4, all_174_3, all_187_0) = 0 % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | REDUCE: (96), (155), (164) imply: % 50.01/7.84 | | | | | | | | | (180) s_t(all_174_1, all_187_0, all_195_0) = 0 % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | REDUCE: (87), (150) imply: % 50.01/7.84 | | | | | | | | | (181) s_t(all_174_2, all_189_0, all_195_0) = 0 % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | REDUCE: (92), (166) imply: % 50.01/7.84 | | | | | | | | | (182) $i(all_195_0) % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | REDUCE: (84), (172) imply: % 50.01/7.84 | | | | | | | | | (183) $i(all_189_0) % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | REDUCE: (79), (170) imply: % 50.01/7.84 | | | | | | | | | (184) $i(all_187_0) % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | BETA: splitting (142) gives: % 50.01/7.84 | | | | | | | | | % 50.01/7.84 | | | | | | | | | Case 1: % 50.01/7.84 | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | (185) ~ (all_337_1 = 0) % 50.01/7.84 | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | REDUCE: (149), (185) imply: % 50.01/7.84 | | | | | | | | | | (186) ~ (all_302_1 = 0) % 50.01/7.84 | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | BETA: splitting (135) gives: % 50.01/7.84 | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | Case 1: % 50.01/7.84 | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | GROUND_INST: instantiating (25) with all_174_2, all_174_1, % 50.01/7.84 | | | | | | | | | | | all_174_3, all_174_4, all_189_0, all_195_0, % 50.01/7.84 | | | | | | | | | | | all_187_0, all_174_0, simplifying with (42), (43), % 50.01/7.84 | | | | | | | | | | | (44), (45), (47), (180), (181), (182), (183), % 50.01/7.84 | | | | | | | | | | | (184) gives: % 50.01/7.84 | | | | | | | | | | | (187) all_195_0 = all_189_0 | all_195_0 = all_187_0 | % 50.01/7.84 | | | | | | | | | | | all_189_0 = all_174_2 | all_187_0 = all_174_1 | % 50.01/7.84 | | | | | | | | | | | all_174_0 = 0 | all_174_3 = all_174_4 | ? [v0: % 50.01/7.84 | | | | | | | | | | | any] : ? [v1: any] : ? [v2: any] : ? [v3: % 50.01/7.84 | | | | | | | | | | | any] : (s_col(all_174_3, all_174_4, all_189_0) = % 50.01/7.84 | | | | | | | | | | | v0 & s_col(all_174_3, all_174_4, all_187_0) = v1 % 50.01/7.84 | | | | | | | | | | | & s_col(all_174_3, all_174_4, all_174_1) = v3 & % 50.01/7.84 | | | | | | | | | | | s_col(all_174_3, all_174_4, all_174_2) = v2 & ( % 50.01/7.84 | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 50.01/7.84 | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | GROUND_INST: instantiating (7) with all_174_3, all_174_4, % 50.01/7.84 | | | | | | | | | | | all_174_2, all_183_0, simplifying with (42), (43), % 50.01/7.84 | | | | | | | | | | | (44), (68) gives: % 50.01/7.84 | | | | | | | | | | | (188) all_183_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & % 50.01/7.84 | | | | | | | | | | | s_col(all_174_3, all_174_4, all_174_2) = v0) % 50.01/7.84 | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | GROUND_INST: instantiating (7) with all_174_3, all_174_4, % 50.01/7.84 | | | | | | | | | | | all_174_1, all_185_0, simplifying with (42), (43), % 50.01/7.84 | | | | | | | | | | | (45), (71) gives: % 50.01/7.84 | | | | | | | | | | | (189) all_185_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & % 50.01/7.84 | | | | | | | | | | | s_col(all_174_3, all_174_4, all_174_1) = v0) % 50.01/7.84 | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | GROUND_INST: instantiating (6) with all_174_4, all_174_3, % 50.01/7.84 | | | | | | | | | | | all_187_0, simplifying with (42), (43), (179), % 50.01/7.84 | | | | | | | | | | | (184) gives: % 50.01/7.84 | | | | | | | | | | | (190) s_col(all_174_3, all_174_4, all_187_0) = 0 % 50.01/7.84 | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | GROUND_INST: instantiating (6) with all_174_4, all_174_3, % 50.01/7.84 | | | | | | | | | | | all_189_0, simplifying with (42), (43), (76), % 50.01/7.84 | | | | | | | | | | | (183) gives: % 50.01/7.84 | | | | | | | | | | | (191) s_col(all_174_3, all_174_4, all_189_0) = 0 % 50.01/7.84 | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | GROUND_INST: instantiating (10) with beta, alpha, alpha, gamma, % 50.01/7.84 | | | | | | | | | | | all_302_1, all_302_1, simplifying with (5), (11), % 50.01/7.84 | | | | | | | | | | | (12), (124) gives: % 50.01/7.84 | | | | | | | | | | | (192) all_302_1 = 0 | gamma = beta | beta = alpha | ? % 50.01/7.84 | | | | | | | | | | | [v0: any] : ? [v1: any] : (s_col(gamma, beta, % 50.01/7.84 | | | | | | | | | | | alpha) = v1 & s_t(alpha, beta, alpha) = v0 & ( % 50.01/7.84 | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0))) % 50.01/7.84 | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | BETA: splitting (189) gives: % 50.01/7.84 | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | Case 1: % 50.01/7.84 | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | (193) all_185_0 = 0 % 50.01/7.84 | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | REDUCE: (70), (193) imply: % 50.01/7.84 | | | | | | | | | | | | (194) $false % 50.01/7.84 | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | CLOSE: (194) is inconsistent. % 50.01/7.84 | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | Case 2: % 50.01/7.84 | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | (195) ? [v0: int] : ( ~ (v0 = 0) & s_col(all_174_3, % 50.01/7.84 | | | | | | | | | | | | all_174_4, all_174_1) = v0) % 50.01/7.84 | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | DELTA: instantiating (195) with fresh symbol all_609_0 % 50.01/7.84 | | | | | | | | | | | | gives: % 50.01/7.84 | | | | | | | | | | | | (196) ~ (all_609_0 = 0) & s_col(all_174_3, all_174_4, % 50.01/7.84 | | | | | | | | | | | | all_174_1) = all_609_0 % 50.01/7.84 | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | ALPHA: (196) implies: % 50.01/7.84 | | | | | | | | | | | | (197) ~ (all_609_0 = 0) % 50.01/7.84 | | | | | | | | | | | | (198) s_col(all_174_3, all_174_4, all_174_1) = all_609_0 % 50.01/7.84 | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | BETA: splitting (188) gives: % 50.01/7.84 | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | Case 1: % 50.01/7.84 | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | (199) all_183_0 = 0 % 50.01/7.84 | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | REDUCE: (67), (199) imply: % 50.01/7.84 | | | | | | | | | | | | | (200) $false % 50.01/7.84 | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | CLOSE: (200) is inconsistent. % 50.01/7.84 | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | Case 2: % 50.01/7.84 | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | (201) ? [v0: int] : ( ~ (v0 = 0) & s_col(all_174_3, % 50.01/7.84 | | | | | | | | | | | | | all_174_4, all_174_2) = v0) % 50.01/7.84 | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | DELTA: instantiating (201) with fresh symbol all_782_0 % 50.01/7.84 | | | | | | | | | | | | | gives: % 50.01/7.84 | | | | | | | | | | | | | (202) ~ (all_782_0 = 0) & s_col(all_174_3, all_174_4, % 50.01/7.84 | | | | | | | | | | | | | all_174_2) = all_782_0 % 50.01/7.84 | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | ALPHA: (202) implies: % 50.01/7.84 | | | | | | | | | | | | | (203) ~ (all_782_0 = 0) % 50.01/7.84 | | | | | | | | | | | | | (204) s_col(all_174_3, all_174_4, all_174_2) = all_782_0 % 50.01/7.84 | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | BETA: splitting (187) gives: % 50.01/7.84 | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | Case 1: % 50.01/7.84 | | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | | (205) all_174_0 = 0 % 50.01/7.84 | | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | | REDUCE: (41), (205) imply: % 50.01/7.84 | | | | | | | | | | | | | | (206) $false % 50.01/7.84 | | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | | CLOSE: (206) is inconsistent. % 50.01/7.84 | | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | Case 2: % 50.01/7.84 | | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | | (207) all_195_0 = all_189_0 | all_195_0 = all_187_0 | % 50.01/7.84 | | | | | | | | | | | | | | all_189_0 = all_174_2 | all_187_0 = all_174_1 | % 50.01/7.84 | | | | | | | | | | | | | | all_174_3 = all_174_4 | ? [v0: any] : ? [v1: % 50.01/7.84 | | | | | | | | | | | | | | any] : ? [v2: any] : ? [v3: any] : % 50.01/7.84 | | | | | | | | | | | | | | (s_col(all_174_3, all_174_4, all_189_0) = v0 & % 50.01/7.84 | | | | | | | | | | | | | | s_col(all_174_3, all_174_4, all_187_0) = v1 & % 50.01/7.84 | | | | | | | | | | | | | | s_col(all_174_3, all_174_4, all_174_1) = v3 & % 50.01/7.84 | | | | | | | | | | | | | | s_col(all_174_3, all_174_4, all_174_2) = v2 & ( % 50.01/7.84 | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 50.01/7.84 | | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | | BETA: splitting (207) gives: % 50.01/7.84 | | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | | Case 1: % 50.01/7.84 | | | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | | | (208) all_195_0 = all_189_0 % 50.01/7.84 | | | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | | | REDUCE: (175), (208) imply: % 50.01/7.84 | | | | | | | | | | | | | | | (209) $false % 50.01/7.84 | | | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | | | CLOSE: (209) is inconsistent. % 50.01/7.84 | | | | | | | | | | | | | | | % 50.01/7.84 | | | | | | | | | | | | | | Case 2: % 50.01/7.84 | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | (210) all_195_0 = all_187_0 | all_189_0 = all_174_2 | % 50.01/7.85 | | | | | | | | | | | | | | | all_187_0 = all_174_1 | all_174_3 = all_174_4 | ? % 50.01/7.85 | | | | | | | | | | | | | | | [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 50.01/7.85 | | | | | | | | | | | | | | | any] : (s_col(all_174_3, all_174_4, all_189_0) = % 50.01/7.85 | | | | | | | | | | | | | | | v0 & s_col(all_174_3, all_174_4, all_187_0) = v1 % 50.01/7.85 | | | | | | | | | | | | | | | & s_col(all_174_3, all_174_4, all_174_1) = v3 & % 50.01/7.85 | | | | | | | | | | | | | | | s_col(all_174_3, all_174_4, all_174_2) = v2 & ( % 50.01/7.85 | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 50.01/7.85 | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | BETA: splitting (210) gives: % 50.01/7.85 | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | Case 1: % 50.01/7.85 | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | (211) all_195_0 = all_187_0 % 50.01/7.85 | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | REDUCE: (177), (211) imply: % 50.01/7.85 | | | | | | | | | | | | | | | | (212) $false % 50.01/7.85 | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | CLOSE: (212) is inconsistent. % 50.01/7.85 | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | Case 2: % 50.01/7.85 | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | (213) all_189_0 = all_174_2 | all_187_0 = all_174_1 | % 50.01/7.85 | | | | | | | | | | | | | | | | all_174_3 = all_174_4 | ? [v0: any] : ? [v1: % 50.01/7.85 | | | | | | | | | | | | | | | | any] : ? [v2: any] : ? [v3: any] : % 50.01/7.85 | | | | | | | | | | | | | | | | (s_col(all_174_3, all_174_4, all_189_0) = v0 & % 50.01/7.85 | | | | | | | | | | | | | | | | s_col(all_174_3, all_174_4, all_187_0) = v1 & % 50.01/7.85 | | | | | | | | | | | | | | | | s_col(all_174_3, all_174_4, all_174_1) = v3 & % 50.01/7.85 | | | | | | | | | | | | | | | | s_col(all_174_3, all_174_4, all_174_2) = v2 & ( % 50.01/7.85 | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 50.01/7.85 | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | BETA: splitting (213) gives: % 50.01/7.85 | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | Case 1: % 50.01/7.85 | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | (214) all_189_0 = all_174_2 % 50.01/7.85 | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | REDUCE: (178), (214) imply: % 50.01/7.85 | | | | | | | | | | | | | | | | | (215) $false % 50.01/7.85 | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | CLOSE: (215) is inconsistent. % 50.01/7.85 | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | Case 2: % 50.01/7.85 | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | (216) all_187_0 = all_174_1 | all_174_3 = all_174_4 | ? % 50.01/7.85 | | | | | | | | | | | | | | | | | [v0: any] : ? [v1: any] : ? [v2: any] : ? [v3: % 50.01/7.85 | | | | | | | | | | | | | | | | | any] : (s_col(all_174_3, all_174_4, all_189_0) = % 50.01/7.85 | | | | | | | | | | | | | | | | | v0 & s_col(all_174_3, all_174_4, all_187_0) = v1 % 50.01/7.85 | | | | | | | | | | | | | | | | | & s_col(all_174_3, all_174_4, all_174_1) = v3 & % 50.01/7.85 | | | | | | | | | | | | | | | | | s_col(all_174_3, all_174_4, all_174_2) = v2 & ( % 50.01/7.85 | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 50.01/7.85 | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | BETA: splitting (192) gives: % 50.01/7.85 | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | Case 1: % 50.01/7.85 | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | (217) gamma = beta % 50.01/7.85 | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | REDUCE: (4), (217) imply: % 50.01/7.85 | | | | | | | | | | | | | | | | | | (218) $false % 50.01/7.85 | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | CLOSE: (218) is inconsistent. % 50.01/7.85 | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | Case 2: % 50.01/7.85 | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | (219) all_302_1 = 0 | beta = alpha | ? [v0: any] : ? % 50.01/7.85 | | | | | | | | | | | | | | | | | | [v1: any] : (s_col(gamma, beta, alpha) = v1 & % 50.01/7.85 | | | | | | | | | | | | | | | | | | s_t(alpha, beta, alpha) = v0 & ( ~ (v1 = 0) | ~ % 50.01/7.85 | | | | | | | | | | | | | | | | | | (v0 = 0))) % 50.01/7.85 | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | BETA: splitting (216) gives: % 50.01/7.85 | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | Case 1: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | (220) all_187_0 = all_174_1 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | REDUCE: (73), (220) imply: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | (221) $false % 50.01/7.85 | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | CLOSE: (221) is inconsistent. % 50.01/7.85 | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | Case 2: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | (222) all_174_3 = all_174_4 | ? [v0: any] : ? [v1: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | any] : ? [v2: any] : ? [v3: any] : % 50.01/7.85 | | | | | | | | | | | | | | | | | | | (s_col(all_174_3, all_174_4, all_189_0) = v0 & % 50.01/7.85 | | | | | | | | | | | | | | | | | | | s_col(all_174_3, all_174_4, all_187_0) = v1 & % 50.01/7.85 | | | | | | | | | | | | | | | | | | | s_col(all_174_3, all_174_4, all_174_1) = v3 & % 50.01/7.85 | | | | | | | | | | | | | | | | | | | s_col(all_174_3, all_174_4, all_174_2) = v2 & ( % 50.01/7.85 | | | | | | | | | | | | | | | | | | | ~ (v1 = 0) | ~ (v0 = 0) | v3 = 0 | v2 = 0)) % 50.01/7.85 | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | BETA: splitting (219) gives: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | Case 1: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | (223) beta = alpha % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | REDUCE: (3), (223) imply: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | (224) $false % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | CLOSE: (224) is inconsistent. % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | Case 2: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | (225) all_302_1 = 0 | ? [v0: any] : ? [v1: any] : % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | (s_col(gamma, beta, alpha) = v1 & s_t(alpha, beta, % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | alpha) = v0 & ( ~ (v1 = 0) | ~ (v0 = 0))) % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | BETA: splitting (222) gives: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | Case 1: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | (226) all_174_3 = all_174_4 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | REDUCE: (40), (226) imply: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | (227) $false % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | CLOSE: (227) is inconsistent. % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | Case 2: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | (228) ? [v0: any] : ? [v1: any] : ? [v2: any] : ? % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | [v3: any] : (s_col(all_174_3, all_174_4, % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_189_0) = v0 & s_col(all_174_3, all_174_4, % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_187_0) = v1 & s_col(all_174_3, all_174_4, % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_174_1) = v3 & s_col(all_174_3, all_174_4, % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_174_2) = v2 & ( ~ (v1 = 0) | ~ (v0 = 0) | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | v3 = 0 | v2 = 0)) % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | DELTA: instantiating (228) with fresh symbols all_1137_0, % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_1137_1, all_1137_2, all_1137_3 gives: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | (229) s_col(all_174_3, all_174_4, all_189_0) = % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_1137_3 & s_col(all_174_3, all_174_4, % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_187_0) = all_1137_2 & s_col(all_174_3, % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_174_4, all_174_1) = all_1137_0 & % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | s_col(all_174_3, all_174_4, all_174_2) = % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_1137_1 & ( ~ (all_1137_2 = 0) | ~ (all_1137_3 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | = 0) | all_1137_0 = 0 | all_1137_1 = 0) % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | ALPHA: (229) implies: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | (230) s_col(all_174_3, all_174_4, all_174_2) = % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_1137_1 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | (231) s_col(all_174_3, all_174_4, all_174_1) = % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_1137_0 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | (232) s_col(all_174_3, all_174_4, all_187_0) = % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_1137_2 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | (233) s_col(all_174_3, all_174_4, all_189_0) = % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_1137_3 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | (234) ~ (all_1137_2 = 0) | ~ (all_1137_3 = 0) | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | all_1137_0 = 0 | all_1137_1 = 0 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | BETA: splitting (225) gives: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | Case 1: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | (235) all_302_1 = 0 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | REDUCE: (186), (235) imply: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | (236) $false % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | CLOSE: (236) is inconsistent. % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | Case 2: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (27) with all_782_0, all_1137_1, % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | all_174_2, all_174_4, all_174_3, simplifying with % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | (204), (230) gives: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | (237) all_1137_1 = all_782_0 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (27) with all_609_0, all_1137_0, % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | all_174_1, all_174_4, all_174_3, simplifying with % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | (198), (231) gives: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | (238) all_1137_0 = all_609_0 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (27) with 0, all_1137_2, all_187_0, % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | all_174_4, all_174_3, simplifying with (190), % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | (232) gives: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | (239) all_1137_2 = 0 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (27) with 0, all_1137_3, all_189_0, % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | all_174_4, all_174_3, simplifying with (191), % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | (233) gives: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | (240) all_1137_3 = 0 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (234) gives: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | Case 1: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | (241) ~ (all_1137_2 = 0) % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (239), (241) imply: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | (242) $false % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (242) is inconsistent. % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | Case 2: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | (243) ~ (all_1137_3 = 0) | all_1137_0 = 0 | all_1137_1 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | = 0 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (243) gives: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | (244) ~ (all_1137_3 = 0) % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (240), (244) imply: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | (245) $false % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (245) is inconsistent. % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | (246) all_1137_0 = 0 | all_1137_1 = 0 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (246) gives: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | (247) all_1137_0 = 0 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (238), (247) imply: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | (248) all_609_0 = 0 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (197), (248) imply: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | (249) $false % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (249) is inconsistent. % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | (250) all_1137_1 = 0 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_EQS: (237), (250) imply: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | (251) all_782_0 = 0 % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | REDUCE: (203), (251) imply: % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | (252) $false % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (252) is inconsistent. % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | End of split % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | End of split % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | End of split % 50.01/7.85 | | | | | | | | | | | | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | | | | | | | | | | | End of split % 50.01/7.86 | | | | | | | | | | | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | | | | | | | | | | End of split % 50.01/7.86 | | | | | | | | | | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | | | | | | | | | End of split % 50.01/7.86 | | | | | | | | | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | | | | | | | | End of split % 50.01/7.86 | | | | | | | | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | | | | | | | End of split % 50.01/7.86 | | | | | | | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | | | | | | End of split % 50.01/7.86 | | | | | | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | | | | | End of split % 50.01/7.86 | | | | | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | | | | End of split % 50.01/7.86 | | | | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | | | End of split % 50.01/7.86 | | | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | | End of split % 50.01/7.86 | | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | End of split % 50.01/7.86 | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | Case 2: % 50.01/7.86 | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | (253) all_322_0 = 0 % 50.01/7.86 | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | COMBINE_EQS: (148), (253) imply: % 50.01/7.86 | | | | | | | | | | | (254) all_257_0 = 0 % 50.01/7.86 | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | REDUCE: (113), (254) imply: % 50.01/7.86 | | | | | | | | | | | (255) $false % 50.01/7.86 | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | | CLOSE: (255) is inconsistent. % 50.01/7.86 | | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | End of split % 50.01/7.86 | | | | | | | | | | % 50.01/7.86 | | | | | | | | | Case 2: % 50.01/7.86 | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | (256) all_337_0 = 0 % 50.01/7.86 | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | COMBINE_EQS: (146), (256) imply: % 50.01/7.86 | | | | | | | | | | (257) all_227_0 = 0 % 50.01/7.86 | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | REDUCE: (107), (257) imply: % 50.01/7.86 | | | | | | | | | | (258) $false % 50.01/7.86 | | | | | | | | | | % 50.01/7.86 | | | | | | | | | | CLOSE: (258) is inconsistent. % 50.01/7.86 | | | | | | | | | | % 50.01/7.86 | | | | | | | | | End of split % 50.01/7.86 | | | | | | | | | % 50.01/7.86 | | | | | | | | End of split % 50.01/7.86 | | | | | | | | % 50.01/7.86 | | | | | | | End of split % 50.01/7.86 | | | | | | | % 50.01/7.86 | | | | | | End of split % 50.01/7.86 | | | | | | % 50.01/7.86 | | | | | End of split % 50.01/7.86 | | | | | % 50.01/7.86 | | | | End of split % 50.01/7.86 | | | | % 50.01/7.86 | | | End of split % 50.01/7.86 | | | % 50.01/7.86 | | End of split % 50.01/7.86 | | % 50.01/7.86 | End of split % 50.01/7.86 | % 50.01/7.86 End of proof % 50.01/7.86 % SZS output end Proof for theBenchmark % 50.01/7.86 % 50.01/7.86 7244ms %------------------------------------------------------------------------------