%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SEV549+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n003.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 : Tue Apr 1 02:02:55 AM UTC 2025 % Result : Theorem 22.44s 3.72s % Output : Proof 23.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SEV549+1 : TPTP v9.1.0. Released v9.1.0. % 0.06/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n003.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Mon Mar 31 11:48:03 EDT 2025 % 0.12/0.34 % CPUTime : % 0.50/0.60 ________ _____ % 0.50/0.60 ___ __ \_________(_)________________________________ % 0.50/0.60 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.50/0.60 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.50/0.60 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.50/0.60 % 0.50/0.60 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.50/0.60 (2023-06-19) % 0.50/0.60 % 0.50/0.60 (c) Philipp Rümmer, 2009-2023 % 0.50/0.60 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.50/0.60 Amanda Stjerna. % 0.50/0.60 Free software under BSD-3-Clause. % 0.50/0.60 % 0.50/0.60 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.50/0.60 % 0.50/0.60 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.50/0.61 Running up to 7 provers in parallel. % 0.50/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.50/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.50/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.50/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.50/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.50/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.50/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.69/1.11 Prover 4: Preprocessing ... % 2.69/1.11 Prover 1: Preprocessing ... % 3.03/1.14 Prover 0: Preprocessing ... % 3.03/1.14 Prover 3: Preprocessing ... % 3.03/1.14 Prover 6: Preprocessing ... % 3.03/1.14 Prover 5: Preprocessing ... % 3.03/1.14 Prover 2: Preprocessing ... % 6.44/1.60 Prover 2: Proving ... % 6.44/1.62 Prover 5: Proving ... % 7.04/1.67 Prover 6: Proving ... % 7.04/1.68 Prover 3: Constructing countermodel ... % 7.04/1.72 Prover 1: Constructing countermodel ... % 7.70/1.77 Prover 0: Proving ... % 8.17/1.83 Prover 4: Constructing countermodel ... % 9.63/2.06 Prover 3: gave up % 9.88/2.07 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 9.88/2.11 Prover 7: Preprocessing ... % 10.43/2.13 Prover 1: gave up % 10.43/2.13 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 10.78/2.18 Prover 7: Warning: ignoring some quantifiers % 10.78/2.19 Prover 8: Preprocessing ... % 10.78/2.19 Prover 7: Constructing countermodel ... % 12.12/2.37 Prover 8: Warning: ignoring some quantifiers % 12.12/2.39 Prover 8: Constructing countermodel ... % 14.40/2.69 Prover 8: gave up % 14.40/2.69 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 14.40/2.72 Prover 9: Preprocessing ... % 16.11/2.89 Prover 9: Constructing countermodel ... % 22.44/3.71 Prover 4: Found proof (size 451) % 22.44/3.71 Prover 4: proved (3085ms) % 22.44/3.71 Prover 9: stopped % 22.44/3.71 Prover 6: stopped % 22.44/3.71 Prover 5: stopped % 22.44/3.71 Prover 2: stopped % 22.44/3.71 Prover 7: stopped % 22.44/3.72 Prover 0: stopped % 22.44/3.72 % 22.44/3.72 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 22.44/3.72 % 22.44/3.74 % SZS output start Proof for theBenchmark % 22.44/3.75 Assumptions after simplification: % 22.44/3.75 --------------------------------- % 22.44/3.75 % 22.44/3.75 (a_def) % 22.81/3.77 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (u(v0, v2) = v3) | % 22.81/3.77 ~ (s(v1) = v2) | ~ $i(v1) | ~ $i(v0) | (a(v0, v1) = v3 & $i(v3))) & ! % 22.81/3.77 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (a(v0, v1) = v2) | ~ $i(v1) | ~ % 22.81/3.77 $i(v0) | ? [v3: $i] : (u(v0, v3) = v2 & s(v1) = v3 & $i(v3) & $i(v2))) % 22.81/3.77 % 22.81/3.77 (atleast2p_def) % 22.81/3.78 ! [v0: $i] : ! [v1: int] : ! [v2: $i] : ! [v3: $i] : (v1 = 0 | ~ % 22.81/3.78 (atleast2p(v0) = v1) | ~ (p(v2) = v3) | ~ $i(v2) | ~ $i(v0) | ? [v4: % 22.81/3.78 any] : ? [v5: any] : (subq(v0, v3) = v5 & mem(v2, v0) = v4 & ( ~ (v4 = 0) % 22.81/3.78 | v5 = 0))) & ! [v0: $i] : ! [v1: int] : ! [v2: $i] : (v1 = 0 | ~ % 22.81/3.78 (atleast2p(v0) = v1) | ~ (mem(v2, v0) = 0) | ~ $i(v2) | ~ $i(v0) | ? % 22.81/3.78 [v3: $i] : (p(v2) = v3 & subq(v0, v3) = 0 & $i(v3))) & ! [v0: $i] : ( ~ % 22.81/3.78 (atleast2p(v0) = 0) | ~ $i(v0) | ? [v1: $i] : ? [v2: $i] : ? [v3: int] : % 22.81/3.78 ( ~ (v3 = 0) & p(v1) = v2 & subq(v0, v2) = v3 & mem(v1, v0) = 0 & $i(v2) & % 22.81/3.78 $i(v1))) % 22.81/3.78 % 22.81/3.78 (atleast3p_def) % 22.81/3.78 ! [v0: $i] : ! [v1: int] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | v1 = 0 | % 22.81/3.78 ~ (atleast3p(v0) = v1) | ~ (subq(v0, v2) = v3) | ~ $i(v2) | ~ $i(v0) | ? % 22.81/3.78 [v4: any] : ? [v5: any] : (atleast2p(v2) = v5 & subq(v2, v0) = v4 & ( ~ (v5 % 22.81/3.78 = 0) | ~ (v4 = 0)))) & ! [v0: $i] : ! [v1: int] : ! [v2: $i] : (v1 % 22.81/3.78 = 0 | ~ (atleast3p(v0) = v1) | ~ (atleast2p(v2) = 0) | ~ $i(v2) | ~ % 22.81/3.78 $i(v0) | ? [v3: any] : ? [v4: any] : (subq(v2, v0) = v3 & subq(v0, v2) = % 22.81/3.78 v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0: $i] : ! [v1: int] : ! [v2: $i] : % 22.81/3.78 (v1 = 0 | ~ (atleast3p(v0) = v1) | ~ (subq(v2, v0) = 0) | ~ $i(v2) | ~ % 22.81/3.78 $i(v0) | ? [v3: any] : ? [v4: any] : (atleast2p(v2) = v3 & subq(v0, v2) = % 22.81/3.78 v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0: $i] : ( ~ (atleast3p(v0) = 0) | ~ % 22.81/3.78 $i(v0) | ? [v1: $i] : ? [v2: int] : ( ~ (v2 = 0) & atleast2p(v1) = 0 & % 22.81/3.78 subq(v1, v0) = 0 & subq(v0, v1) = v2 & $i(v1))) % 22.81/3.78 % 22.81/3.78 (atleast4p_def) % 22.81/3.79 ! [v0: $i] : ! [v1: int] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | v1 = 0 | % 22.81/3.79 ~ (atleast4p(v0) = v1) | ~ (subq(v0, v2) = v3) | ~ $i(v2) | ~ $i(v0) | ? % 22.81/3.79 [v4: any] : ? [v5: any] : (atleast3p(v2) = v5 & subq(v2, v0) = v4 & ( ~ (v5 % 22.81/3.79 = 0) | ~ (v4 = 0)))) & ! [v0: $i] : ! [v1: int] : ! [v2: $i] : (v1 % 22.81/3.79 = 0 | ~ (atleast4p(v0) = v1) | ~ (atleast3p(v2) = 0) | ~ $i(v2) | ~ % 22.81/3.79 $i(v0) | ? [v3: any] : ? [v4: any] : (subq(v2, v0) = v3 & subq(v0, v2) = % 22.81/3.79 v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0: $i] : ! [v1: int] : ! [v2: $i] : % 22.81/3.79 (v1 = 0 | ~ (atleast4p(v0) = v1) | ~ (subq(v2, v0) = 0) | ~ $i(v2) | ~ % 22.81/3.79 $i(v0) | ? [v3: any] : ? [v4: any] : (atleast3p(v2) = v3 & subq(v0, v2) = % 22.81/3.79 v4 & ( ~ (v3 = 0) | v4 = 0))) & ! [v0: $i] : ( ~ (atleast4p(v0) = 0) | ~ % 22.81/3.79 $i(v0) | ? [v1: $i] : ? [v2: int] : ( ~ (v2 = 0) & atleast3p(v1) = 0 & % 22.81/3.79 subq(v1, v0) = 0 & subq(v0, v1) = v2 & $i(v1))) % 22.81/3.79 % 22.81/3.79 (atmost3_28) % 22.81/3.79 $i(e) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 22.81/3.79 ? [v5: $i] : ? [v6: $i] : (atleast4p(v6) = 0 & n(v4) = v5 & n(v0) = v1 & n(e) % 22.81/3.79 = v0 & u(v2, v5) = v6 & s(v3) = v4 & s(v1) = v2 & s(v0) = v3 & $i(v6) & % 22.81/3.79 $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 22.81/3.79 % 22.81/3.79 (n_def) % 22.81/3.79 ! [v0: $i] : ! [v1: $i] : ( ~ (n(v0) = v1) | ~ $i(v0) | (a(v0, v0) = v1 & % 22.81/3.79 $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (a(v0, v0) = v1) | ~ $i(v0) | % 22.81/3.79 (n(v0) = v1 & $i(v1))) % 22.81/3.79 % 22.81/3.79 (p_ax) % 22.81/3.79 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (p(v1) = % 22.81/3.79 v2) | ~ (mem(v0, v2) = v3) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ % 22.81/3.79 (v4 = 0) & subq(v0, v1) = v4)) & ! [v0: $i] : ! [v1: $i] : ! [v2: int] % 22.81/3.79 : (v2 = 0 | ~ (subq(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? % 22.81/3.79 [v4: int] : ( ~ (v4 = 0) & p(v1) = v3 & mem(v0, v3) = v4 & $i(v3))) & ! % 22.81/3.79 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (p(v1) = v2) | ~ (mem(v0, v2) = 0) % 22.81/3.79 | ~ $i(v1) | ~ $i(v0) | subq(v0, v1) = 0) & ! [v0: $i] : ! [v1: $i] : ( % 22.81/3.79 ~ (subq(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: $i] : (p(v1) = v2 & % 22.81/3.79 mem(v0, v2) = 0 & $i(v2))) % 22.81/3.79 % 22.81/3.79 (s_ax) % 22.81/3.80 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (s(v0) = v1) | ~ % 22.81/3.80 (mem(v0, v1) = v2) | ~ $i(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 22.81/3.80 (v1 = v0 | ~ (s(v1) = v2) | ~ (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 22.81/3.80 % 22.81/3.80 (subq_def) % 22.81/3.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 22.81/3.80 (subq(v0, v1) = 0) | ~ (mem(v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 22.81/3.80 $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & mem(v2, v0) = v4)) & ! [v0: $i] : ! % 22.81/3.80 [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ~ $i(v1) | ~ % 22.81/3.80 $i(v0) | ? [v3: $i] : ? [v4: int] : ( ~ (v4 = 0) & mem(v3, v1) = v4 & % 22.81/3.80 mem(v3, v0) = 0 & $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 22.81/3.80 (subq(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ % 22.81/3.80 $i(v0) | mem(v2, v1) = 0) % 22.81/3.80 % 22.81/3.80 (u_ax) % 22.81/3.80 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 22.81/3.80 | ~ (u(v1, v2) = v3) | ~ (mem(v0, v3) = v4) | ~ $i(v2) | ~ $i(v1) | ~ % 22.81/3.80 $i(v0) | ? [v5: int] : ? [v6: int] : ( ~ (v6 = 0) & ~ (v5 = 0) & mem(v0, % 22.81/3.80 v2) = v6 & mem(v0, v1) = v5)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 22.81/3.80 : ! [v3: $i] : ( ~ (u(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ~ $i(v2) | ~ % 22.81/3.80 $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : (mem(v0, v2) = v5 & % 22.81/3.80 mem(v0, v1) = v4 & (v5 = 0 | v4 = 0))) % 22.81/3.80 % 22.81/3.80 (function-axioms) % 22.81/3.81 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (a(v3, % 22.81/3.81 v2) = v1) | ~ (a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 22.81/3.81 $i] : ! [v3: $i] : (v1 = v0 | ~ (m(v3, v2) = v1) | ~ (m(v3, v2) = v0)) & % 22.81/3.81 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (u(v3, % 22.81/3.81 v2) = v1) | ~ (u(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (disj(v3, v2) % 22.81/3.81 = v1) | ~ (disj(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (subq(v3, v2) % 22.81/3.81 = v1) | ~ (subq(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) % 22.81/3.81 = v1) | ~ (mem(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast16p(v2) = v1) | ~ % 22.81/3.81 (atleast16p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast15p(v2) = v1) | ~ % 22.81/3.81 (atleast15p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast14p(v2) = v1) | ~ % 22.81/3.81 (atleast14p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast13p(v2) = v1) | ~ % 22.81/3.81 (atleast13p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast12p(v2) = v1) | ~ % 22.81/3.81 (atleast12p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast11p(v2) = v1) | ~ % 22.81/3.81 (atleast11p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast10p(v2) = v1) | ~ % 22.81/3.81 (atleast10p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast9p(v2) = v1) | ~ % 22.81/3.81 (atleast9p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast8p(v2) = v1) | ~ % 22.81/3.81 (atleast8p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast7p(v2) = v1) | ~ % 22.81/3.81 (atleast7p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast6p(v2) = v1) | ~ % 22.81/3.81 (atleast6p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast5p(v2) = v1) | ~ % 22.81/3.81 (atleast5p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast4p(v2) = v1) | ~ % 22.81/3.81 (atleast4p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast3p(v2) = v1) | ~ % 22.81/3.81 (atleast3p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 22.81/3.81 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast2p(v2) = v1) | ~ % 22.81/3.81 (atleast2p(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | % 22.81/3.81 ~ (p(v2) = v1) | ~ (p(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 22.81/3.81 : (v1 = v0 | ~ (n(v2) = v1) | ~ (n(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 22.81/3.81 ! [v2: $i] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 22.81/3.81 % 22.81/3.81 Further assumptions not needed in the proof: % 22.81/3.81 -------------------------------------------- % 22.81/3.81 atleast10p_def, atleast11p_def, atleast12p_def, atleast13p_def, atleast14p_def, % 22.81/3.81 atleast15p_def, atleast16p_def, atleast5p_def, atleast6p_def, atleast7p_def, % 22.81/3.81 atleast8p_def, atleast9p_def, disj_def, e_ax, m_ax, setext % 22.81/3.81 % 22.81/3.81 Those formulas are unsatisfiable: % 22.81/3.81 --------------------------------- % 22.81/3.81 % 22.81/3.81 Begin of proof % 22.81/3.81 | % 22.81/3.81 | ALPHA: (subq_def) implies: % 22.81/3.81 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (subq(v0, v1) = 0) | ~ % 22.81/3.81 | (mem(v2, v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | mem(v2, v1) = % 22.81/3.81 | 0) % 22.81/3.81 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (subq(v0, v1) = % 22.81/3.81 | v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: int] : ( ~ (v4 % 22.81/3.81 | = 0) & mem(v3, v1) = v4 & mem(v3, v0) = 0 & $i(v3))) % 22.81/3.81 | % 22.81/3.81 | ALPHA: (s_ax) implies: % 22.81/3.81 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | % 22.81/3.81 | ~ (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 22.81/3.81 | % 22.81/3.81 | ALPHA: (u_ax) implies: % 22.81/3.82 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (u(v1, v2) % 22.81/3.82 | = v3) | ~ (mem(v0, v3) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 22.81/3.82 | ? [v4: any] : ? [v5: any] : (mem(v0, v2) = v5 & mem(v0, v1) = v4 & % 22.81/3.82 | (v5 = 0 | v4 = 0))) % 23.08/3.82 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : % 23.08/3.82 | (v4 = 0 | ~ (u(v1, v2) = v3) | ~ (mem(v0, v3) = v4) | ~ $i(v2) | ~ % 23.08/3.82 | $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ( ~ (v6 = 0) & ~ % 23.08/3.82 | (v5 = 0) & mem(v0, v2) = v6 & mem(v0, v1) = v5)) % 23.08/3.82 | % 23.08/3.82 | ALPHA: (a_def) implies: % 23.08/3.82 | (6) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (a(v0, v1) = v2) | ~ % 23.08/3.82 | $i(v1) | ~ $i(v0) | ? [v3: $i] : (u(v0, v3) = v2 & s(v1) = v3 & % 23.08/3.82 | $i(v3) & $i(v2))) % 23.08/3.82 | % 23.08/3.82 | ALPHA: (n_def) implies: % 23.08/3.82 | (7) ! [v0: $i] : ! [v1: $i] : ( ~ (n(v0) = v1) | ~ $i(v0) | (a(v0, v0) = % 23.08/3.82 | v1 & $i(v1))) % 23.08/3.82 | % 23.08/3.82 | ALPHA: (p_ax) implies: % 23.08/3.82 | (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 23.08/3.82 | (p(v1) = v2) | ~ (mem(v0, v2) = v3) | ~ $i(v1) | ~ $i(v0) | ? % 23.08/3.82 | [v4: int] : ( ~ (v4 = 0) & subq(v0, v1) = v4)) % 23.08/3.82 | % 23.08/3.82 | ALPHA: (atleast2p_def) implies: % 23.08/3.82 | (9) ! [v0: $i] : ( ~ (atleast2p(v0) = 0) | ~ $i(v0) | ? [v1: $i] : ? % 23.08/3.82 | [v2: $i] : ? [v3: int] : ( ~ (v3 = 0) & p(v1) = v2 & subq(v0, v2) = % 23.08/3.82 | v3 & mem(v1, v0) = 0 & $i(v2) & $i(v1))) % 23.08/3.82 | % 23.08/3.82 | ALPHA: (atleast3p_def) implies: % 23.08/3.82 | (10) ! [v0: $i] : ( ~ (atleast3p(v0) = 0) | ~ $i(v0) | ? [v1: $i] : ? % 23.08/3.82 | [v2: int] : ( ~ (v2 = 0) & atleast2p(v1) = 0 & subq(v1, v0) = 0 & % 23.08/3.82 | subq(v0, v1) = v2 & $i(v1))) % 23.08/3.82 | % 23.08/3.82 | ALPHA: (atleast4p_def) implies: % 23.08/3.82 | (11) ! [v0: $i] : ( ~ (atleast4p(v0) = 0) | ~ $i(v0) | ? [v1: $i] : ? % 23.08/3.82 | [v2: int] : ( ~ (v2 = 0) & atleast3p(v1) = 0 & subq(v1, v0) = 0 & % 23.08/3.82 | subq(v0, v1) = v2 & $i(v1))) % 23.08/3.82 | % 23.08/3.82 | ALPHA: (atmost3_28) implies: % 23.08/3.82 | (12) $i(e) % 23.08/3.82 | (13) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 23.08/3.82 | ? [v5: $i] : ? [v6: $i] : (atleast4p(v6) = 0 & n(v4) = v5 & n(v0) = % 23.08/3.82 | v1 & n(e) = v0 & u(v2, v5) = v6 & s(v3) = v4 & s(v1) = v2 & s(v0) = % 23.08/3.82 | v3 & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 23.08/3.82 | % 23.08/3.82 | ALPHA: (function-axioms) implies: % 23.08/3.82 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v2) = v1) | % 23.08/3.82 | ~ (s(v2) = v0)) % 23.08/3.83 | (15) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 23.08/3.83 | : ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = % 23.08/3.83 | v0)) % 23.08/3.83 | % 23.08/3.83 | DELTA: instantiating (13) with fresh symbols all_29_0, all_29_1, all_29_2, % 23.08/3.83 | all_29_3, all_29_4, all_29_5, all_29_6 gives: % 23.08/3.83 | (16) atleast4p(all_29_0) = 0 & n(all_29_2) = all_29_1 & n(all_29_6) = % 23.08/3.83 | all_29_5 & n(e) = all_29_6 & u(all_29_4, all_29_1) = all_29_0 & % 23.08/3.83 | s(all_29_3) = all_29_2 & s(all_29_5) = all_29_4 & s(all_29_6) = % 23.08/3.83 | all_29_3 & $i(all_29_0) & $i(all_29_1) & $i(all_29_2) & $i(all_29_3) & % 23.08/3.83 | $i(all_29_4) & $i(all_29_5) & $i(all_29_6) % 23.08/3.83 | % 23.08/3.83 | ALPHA: (16) implies: % 23.08/3.83 | (17) $i(all_29_4) % 23.08/3.83 | (18) $i(all_29_2) % 23.08/3.83 | (19) $i(all_29_0) % 23.08/3.83 | (20) s(all_29_6) = all_29_3 % 23.08/3.83 | (21) s(all_29_5) = all_29_4 % 23.08/3.83 | (22) s(all_29_3) = all_29_2 % 23.08/3.83 | (23) u(all_29_4, all_29_1) = all_29_0 % 23.08/3.83 | (24) n(e) = all_29_6 % 23.08/3.83 | (25) n(all_29_6) = all_29_5 % 23.08/3.83 | (26) n(all_29_2) = all_29_1 % 23.08/3.83 | (27) atleast4p(all_29_0) = 0 % 23.08/3.83 | % 23.08/3.83 | GROUND_INST: instantiating (7) with e, all_29_6, simplifying with (12), (24) % 23.08/3.83 | gives: % 23.08/3.83 | (28) a(e, e) = all_29_6 & $i(all_29_6) % 23.08/3.83 | % 23.08/3.83 | ALPHA: (28) implies: % 23.08/3.83 | (29) $i(all_29_6) % 23.08/3.83 | (30) a(e, e) = all_29_6 % 23.08/3.83 | % 23.08/3.83 | GROUND_INST: instantiating (7) with all_29_6, all_29_5, simplifying with (25), % 23.08/3.83 | (29) gives: % 23.08/3.83 | (31) a(all_29_6, all_29_6) = all_29_5 & $i(all_29_5) % 23.08/3.83 | % 23.08/3.83 | ALPHA: (31) implies: % 23.08/3.83 | (32) a(all_29_6, all_29_6) = all_29_5 % 23.08/3.83 | % 23.08/3.83 | GROUND_INST: instantiating (7) with all_29_2, all_29_1, simplifying with (18), % 23.08/3.83 | (26) gives: % 23.08/3.83 | (33) a(all_29_2, all_29_2) = all_29_1 & $i(all_29_1) % 23.08/3.83 | % 23.08/3.83 | ALPHA: (33) implies: % 23.08/3.83 | (34) a(all_29_2, all_29_2) = all_29_1 % 23.08/3.83 | % 23.08/3.83 | GROUND_INST: instantiating (11) with all_29_0, simplifying with (19), (27) % 23.08/3.83 | gives: % 23.08/3.83 | (35) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & atleast3p(v0) = 0 & % 23.08/3.83 | subq(v0, all_29_0) = 0 & subq(all_29_0, v0) = v1 & $i(v0)) % 23.08/3.83 | % 23.08/3.83 | DELTA: instantiating (35) with fresh symbols all_37_0, all_37_1 gives: % 23.08/3.83 | (36) ~ (all_37_0 = 0) & atleast3p(all_37_1) = 0 & subq(all_37_1, all_29_0) % 23.08/3.83 | = 0 & subq(all_29_0, all_37_1) = all_37_0 & $i(all_37_1) % 23.08/3.83 | % 23.08/3.83 | ALPHA: (36) implies: % 23.08/3.83 | (37) ~ (all_37_0 = 0) % 23.08/3.83 | (38) $i(all_37_1) % 23.08/3.83 | (39) subq(all_29_0, all_37_1) = all_37_0 % 23.08/3.83 | (40) subq(all_37_1, all_29_0) = 0 % 23.08/3.83 | (41) atleast3p(all_37_1) = 0 % 23.08/3.83 | % 23.08/3.83 | GROUND_INST: instantiating (2) with all_29_0, all_37_1, all_37_0, simplifying % 23.08/3.83 | with (19), (38), (39) gives: % 23.08/3.84 | (42) all_37_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & mem(v0, % 23.08/3.84 | all_37_1) = v1 & mem(v0, all_29_0) = 0 & $i(v0)) % 23.08/3.84 | % 23.08/3.84 | GROUND_INST: instantiating (6) with e, e, all_29_6, simplifying with (12), % 23.08/3.84 | (30) gives: % 23.08/3.84 | (43) ? [v0: $i] : (u(e, v0) = all_29_6 & s(e) = v0 & $i(v0) & % 23.08/3.84 | $i(all_29_6)) % 23.08/3.84 | % 23.08/3.84 | GROUND_INST: instantiating (6) with all_29_6, all_29_6, all_29_5, simplifying % 23.08/3.84 | with (29), (32) gives: % 23.08/3.84 | (44) ? [v0: $i] : (u(all_29_6, v0) = all_29_5 & s(all_29_6) = v0 & $i(v0) % 23.08/3.84 | & $i(all_29_5)) % 23.08/3.84 | % 23.08/3.84 | GROUND_INST: instantiating (6) with all_29_2, all_29_2, all_29_1, simplifying % 23.08/3.84 | with (18), (34) gives: % 23.08/3.84 | (45) ? [v0: $i] : (u(all_29_2, v0) = all_29_1 & s(all_29_2) = v0 & $i(v0) % 23.08/3.84 | & $i(all_29_1)) % 23.08/3.84 | % 23.08/3.84 | GROUND_INST: instantiating (10) with all_37_1, simplifying with (38), (41) % 23.08/3.84 | gives: % 23.08/3.84 | (46) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & atleast2p(v0) = 0 & % 23.08/3.84 | subq(v0, all_37_1) = 0 & subq(all_37_1, v0) = v1 & $i(v0)) % 23.08/3.84 | % 23.08/3.84 | DELTA: instantiating (45) with fresh symbol all_46_0 gives: % 23.08/3.84 | (47) u(all_29_2, all_46_0) = all_29_1 & s(all_29_2) = all_46_0 & % 23.08/3.84 | $i(all_46_0) & $i(all_29_1) % 23.08/3.84 | % 23.08/3.84 | ALPHA: (47) implies: % 23.08/3.84 | (48) $i(all_29_1) % 23.08/3.84 | (49) $i(all_46_0) % 23.08/3.84 | (50) s(all_29_2) = all_46_0 % 23.08/3.84 | (51) u(all_29_2, all_46_0) = all_29_1 % 23.08/3.84 | % 23.08/3.84 | DELTA: instantiating (44) with fresh symbol all_48_0 gives: % 23.08/3.84 | (52) u(all_29_6, all_48_0) = all_29_5 & s(all_29_6) = all_48_0 & % 23.08/3.84 | $i(all_48_0) & $i(all_29_5) % 23.08/3.84 | % 23.08/3.84 | ALPHA: (52) implies: % 23.08/3.84 | (53) $i(all_29_5) % 23.08/3.84 | (54) $i(all_48_0) % 23.08/3.84 | (55) s(all_29_6) = all_48_0 % 23.08/3.84 | (56) u(all_29_6, all_48_0) = all_29_5 % 23.08/3.84 | % 23.08/3.84 | DELTA: instantiating (43) with fresh symbol all_50_0 gives: % 23.08/3.84 | (57) u(e, all_50_0) = all_29_6 & s(e) = all_50_0 & $i(all_50_0) & % 23.08/3.84 | $i(all_29_6) % 23.08/3.84 | % 23.08/3.84 | DELTA: instantiating (46) with fresh symbols all_52_0, all_52_1 gives: % 23.08/3.84 | (58) ~ (all_52_0 = 0) & atleast2p(all_52_1) = 0 & subq(all_52_1, all_37_1) % 23.08/3.84 | = 0 & subq(all_37_1, all_52_1) = all_52_0 & $i(all_52_1) % 23.08/3.84 | % 23.08/3.84 | ALPHA: (58) implies: % 23.08/3.84 | (59) ~ (all_52_0 = 0) % 23.08/3.84 | (60) $i(all_52_1) % 23.08/3.84 | (61) subq(all_37_1, all_52_1) = all_52_0 % 23.08/3.84 | (62) subq(all_52_1, all_37_1) = 0 % 23.08/3.84 | (63) atleast2p(all_52_1) = 0 % 23.08/3.84 | % 23.08/3.84 | BETA: splitting (42) gives: % 23.08/3.84 | % 23.08/3.84 | Case 1: % 23.08/3.84 | | % 23.08/3.84 | | (64) all_37_0 = 0 % 23.08/3.84 | | % 23.08/3.84 | | REDUCE: (37), (64) imply: % 23.08/3.84 | | (65) $false % 23.08/3.84 | | % 23.08/3.84 | | CLOSE: (65) is inconsistent. % 23.08/3.84 | | % 23.08/3.84 | Case 2: % 23.08/3.84 | | % 23.08/3.84 | | (66) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & mem(v0, all_37_1) = v1 & % 23.08/3.84 | | mem(v0, all_29_0) = 0 & $i(v0)) % 23.08/3.84 | | % 23.08/3.84 | | DELTA: instantiating (66) with fresh symbols all_58_0, all_58_1 gives: % 23.08/3.85 | | (67) ~ (all_58_0 = 0) & mem(all_58_1, all_37_1) = all_58_0 & % 23.08/3.85 | | mem(all_58_1, all_29_0) = 0 & $i(all_58_1) % 23.08/3.85 | | % 23.08/3.85 | | ALPHA: (67) implies: % 23.08/3.85 | | (68) ~ (all_58_0 = 0) % 23.08/3.85 | | (69) $i(all_58_1) % 23.08/3.85 | | (70) mem(all_58_1, all_29_0) = 0 % 23.08/3.85 | | (71) mem(all_58_1, all_37_1) = all_58_0 % 23.08/3.85 | | % 23.08/3.85 | | GROUND_INST: instantiating (14) with all_29_3, all_48_0, all_29_6, % 23.08/3.85 | | simplifying with (20), (55) gives: % 23.08/3.85 | | (72) all_48_0 = all_29_3 % 23.08/3.85 | | % 23.08/3.85 | | REDUCE: (56), (72) imply: % 23.08/3.85 | | (73) u(all_29_6, all_29_3) = all_29_5 % 23.08/3.85 | | % 23.08/3.85 | | REDUCE: (54), (72) imply: % 23.08/3.85 | | (74) $i(all_29_3) % 23.08/3.85 | | % 23.08/3.85 | | GROUND_INST: instantiating (4) with all_58_1, all_29_4, all_29_1, all_29_0, % 23.08/3.85 | | simplifying with (17), (23), (48), (69), (70) gives: % 23.08/3.85 | | (75) ? [v0: any] : ? [v1: any] : (mem(all_58_1, all_29_1) = v1 & % 23.08/3.85 | | mem(all_58_1, all_29_4) = v0 & (v1 = 0 | v0 = 0)) % 23.08/3.85 | | % 23.08/3.85 | | GROUND_INST: instantiating (2) with all_37_1, all_52_1, all_52_0, % 23.08/3.85 | | simplifying with (38), (60), (61) gives: % 23.08/3.85 | | (76) all_52_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & mem(v0, % 23.08/3.85 | | all_52_1) = v1 & mem(v0, all_37_1) = 0 & $i(v0)) % 23.08/3.85 | | % 23.08/3.85 | | GROUND_INST: instantiating (9) with all_52_1, simplifying with (60), (63) % 23.08/3.85 | | gives: % 23.08/3.85 | | (77) ? [v0: $i] : ? [v1: $i] : ? [v2: int] : ( ~ (v2 = 0) & p(v0) = v1 % 23.08/3.85 | | & subq(all_52_1, v1) = v2 & mem(v0, all_52_1) = 0 & $i(v1) & % 23.08/3.85 | | $i(v0)) % 23.08/3.85 | | % 23.08/3.85 | | DELTA: instantiating (75) with fresh symbols all_76_0, all_76_1 gives: % 23.08/3.85 | | (78) mem(all_58_1, all_29_1) = all_76_0 & mem(all_58_1, all_29_4) = % 23.08/3.85 | | all_76_1 & (all_76_0 = 0 | all_76_1 = 0) % 23.08/3.85 | | % 23.08/3.85 | | ALPHA: (78) implies: % 23.08/3.85 | | (79) mem(all_58_1, all_29_4) = all_76_1 % 23.08/3.85 | | (80) mem(all_58_1, all_29_1) = all_76_0 % 23.08/3.85 | | (81) all_76_0 = 0 | all_76_1 = 0 % 23.08/3.85 | | % 23.08/3.85 | | DELTA: instantiating (77) with fresh symbols all_78_0, all_78_1, all_78_2 % 23.08/3.85 | | gives: % 23.08/3.85 | | (82) ~ (all_78_0 = 0) & p(all_78_2) = all_78_1 & subq(all_52_1, % 23.08/3.85 | | all_78_1) = all_78_0 & mem(all_78_2, all_52_1) = 0 & $i(all_78_1) % 23.08/3.85 | | & $i(all_78_2) % 23.08/3.85 | | % 23.08/3.85 | | ALPHA: (82) implies: % 23.08/3.85 | | (83) ~ (all_78_0 = 0) % 23.08/3.85 | | (84) $i(all_78_2) % 23.08/3.85 | | (85) $i(all_78_1) % 23.08/3.85 | | (86) mem(all_78_2, all_52_1) = 0 % 23.08/3.85 | | (87) subq(all_52_1, all_78_1) = all_78_0 % 23.08/3.85 | | (88) p(all_78_2) = all_78_1 % 23.08/3.85 | | % 23.08/3.85 | | BETA: splitting (76) gives: % 23.08/3.85 | | % 23.08/3.85 | | Case 1: % 23.08/3.85 | | | % 23.08/3.85 | | | (89) all_52_0 = 0 % 23.08/3.85 | | | % 23.08/3.85 | | | REDUCE: (59), (89) imply: % 23.08/3.85 | | | (90) $false % 23.08/3.85 | | | % 23.08/3.85 | | | CLOSE: (90) is inconsistent. % 23.08/3.85 | | | % 23.08/3.85 | | Case 2: % 23.08/3.85 | | | % 23.08/3.85 | | | (91) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & mem(v0, all_52_1) = v1 % 23.08/3.85 | | | & mem(v0, all_37_1) = 0 & $i(v0)) % 23.08/3.85 | | | % 23.08/3.85 | | | DELTA: instantiating (91) with fresh symbols all_89_0, all_89_1 gives: % 23.08/3.85 | | | (92) ~ (all_89_0 = 0) & mem(all_89_1, all_52_1) = all_89_0 & % 23.08/3.85 | | | mem(all_89_1, all_37_1) = 0 & $i(all_89_1) % 23.08/3.85 | | | % 23.08/3.85 | | | ALPHA: (92) implies: % 23.08/3.85 | | | (93) ~ (all_89_0 = 0) % 23.08/3.85 | | | (94) $i(all_89_1) % 23.08/3.85 | | | (95) mem(all_89_1, all_37_1) = 0 % 23.08/3.85 | | | (96) mem(all_89_1, all_52_1) = all_89_0 % 23.08/3.85 | | | % 23.27/3.85 | | | GROUND_INST: instantiating (1) with all_52_1, all_37_1, all_78_2, % 23.27/3.85 | | | simplifying with (38), (60), (62), (84), (86) gives: % 23.27/3.85 | | | (97) mem(all_78_2, all_37_1) = 0 % 23.27/3.85 | | | % 23.27/3.86 | | | GROUND_INST: instantiating (1) with all_37_1, all_29_0, all_89_1, % 23.27/3.86 | | | simplifying with (19), (38), (40), (94), (95) gives: % 23.27/3.86 | | | (98) mem(all_89_1, all_29_0) = 0 % 23.27/3.86 | | | % 23.27/3.86 | | | GROUND_INST: instantiating (2) with all_52_1, all_78_1, all_78_0, % 23.27/3.86 | | | simplifying with (60), (85), (87) gives: % 23.27/3.86 | | | (99) all_78_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & mem(v0, % 23.27/3.86 | | | all_78_1) = v1 & mem(v0, all_52_1) = 0 & $i(v0)) % 23.27/3.86 | | | % 23.27/3.86 | | | BETA: splitting (99) gives: % 23.27/3.86 | | | % 23.27/3.86 | | | Case 1: % 23.27/3.86 | | | | % 23.27/3.86 | | | | (100) all_78_0 = 0 % 23.27/3.86 | | | | % 23.27/3.86 | | | | REDUCE: (83), (100) imply: % 23.27/3.86 | | | | (101) $false % 23.27/3.86 | | | | % 23.27/3.86 | | | | CLOSE: (101) is inconsistent. % 23.27/3.86 | | | | % 23.27/3.86 | | | Case 2: % 23.27/3.86 | | | | % 23.27/3.86 | | | | (102) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & mem(v0, all_78_1) = % 23.27/3.86 | | | | v1 & mem(v0, all_52_1) = 0 & $i(v0)) % 23.27/3.86 | | | | % 23.27/3.86 | | | | DELTA: instantiating (102) with fresh symbols all_110_0, all_110_1 % 23.27/3.86 | | | | gives: % 23.27/3.86 | | | | (103) ~ (all_110_0 = 0) & mem(all_110_1, all_78_1) = all_110_0 & % 23.27/3.86 | | | | mem(all_110_1, all_52_1) = 0 & $i(all_110_1) % 23.27/3.86 | | | | % 23.27/3.86 | | | | ALPHA: (103) implies: % 23.27/3.86 | | | | (104) ~ (all_110_0 = 0) % 23.27/3.86 | | | | (105) $i(all_110_1) % 23.27/3.86 | | | | (106) mem(all_110_1, all_52_1) = 0 % 23.27/3.86 | | | | (107) mem(all_110_1, all_78_1) = all_110_0 % 23.27/3.86 | | | | % 23.27/3.86 | | | | GROUND_INST: instantiating (1) with all_37_1, all_29_0, all_78_2, % 23.27/3.86 | | | | simplifying with (19), (38), (40), (84), (97) gives: % 23.27/3.86 | | | | (108) mem(all_78_2, all_29_0) = 0 % 23.27/3.86 | | | | % 23.27/3.86 | | | | GROUND_INST: instantiating (4) with all_89_1, all_29_4, all_29_1, % 23.27/3.86 | | | | all_29_0, simplifying with (17), (23), (48), (94), (98) % 23.27/3.86 | | | | gives: % 23.27/3.86 | | | | (109) ? [v0: any] : ? [v1: any] : (mem(all_89_1, all_29_1) = v1 & % 23.27/3.86 | | | | mem(all_89_1, all_29_4) = v0 & (v1 = 0 | v0 = 0)) % 23.27/3.86 | | | | % 23.27/3.86 | | | | GROUND_INST: instantiating (1) with all_52_1, all_37_1, all_110_1, % 23.27/3.86 | | | | simplifying with (38), (60), (62), (105), (106) gives: % 23.27/3.86 | | | | (110) mem(all_110_1, all_37_1) = 0 % 23.27/3.86 | | | | % 23.27/3.86 | | | | GROUND_INST: instantiating (8) with all_110_1, all_78_2, all_78_1, % 23.27/3.86 | | | | all_110_0, simplifying with (84), (88), (105), (107) gives: % 23.27/3.86 | | | | (111) all_110_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & subq(all_110_1, % 23.27/3.86 | | | | all_78_2) = v0) % 23.27/3.86 | | | | % 23.27/3.86 | | | | DELTA: instantiating (109) with fresh symbols all_123_0, all_123_1 % 23.27/3.86 | | | | gives: % 23.27/3.86 | | | | (112) mem(all_89_1, all_29_1) = all_123_0 & mem(all_89_1, all_29_4) = % 23.27/3.86 | | | | all_123_1 & (all_123_0 = 0 | all_123_1 = 0) % 23.27/3.86 | | | | % 23.27/3.86 | | | | ALPHA: (112) implies: % 23.27/3.86 | | | | (113) mem(all_89_1, all_29_4) = all_123_1 % 23.27/3.86 | | | | (114) mem(all_89_1, all_29_1) = all_123_0 % 23.27/3.86 | | | | (115) all_123_0 = 0 | all_123_1 = 0 % 23.27/3.86 | | | | % 23.27/3.86 | | | | BETA: splitting (111) gives: % 23.27/3.86 | | | | % 23.27/3.86 | | | | Case 1: % 23.27/3.86 | | | | | % 23.27/3.86 | | | | | (116) all_110_0 = 0 % 23.27/3.86 | | | | | % 23.27/3.86 | | | | | REDUCE: (104), (116) imply: % 23.27/3.86 | | | | | (117) $false % 23.27/3.86 | | | | | % 23.27/3.86 | | | | | CLOSE: (117) is inconsistent. % 23.27/3.86 | | | | | % 23.27/3.86 | | | | Case 2: % 23.27/3.86 | | | | | % 23.27/3.86 | | | | | (118) ? [v0: int] : ( ~ (v0 = 0) & subq(all_110_1, all_78_2) = v0) % 23.27/3.86 | | | | | % 23.27/3.86 | | | | | DELTA: instantiating (118) with fresh symbol all_129_0 gives: % 23.27/3.86 | | | | | (119) ~ (all_129_0 = 0) & subq(all_110_1, all_78_2) = all_129_0 % 23.27/3.86 | | | | | % 23.27/3.86 | | | | | ALPHA: (119) implies: % 23.27/3.86 | | | | | (120) ~ (all_129_0 = 0) % 23.27/3.86 | | | | | (121) subq(all_110_1, all_78_2) = all_129_0 % 23.27/3.86 | | | | | % 23.27/3.86 | | | | | GROUND_INST: instantiating (4) with all_78_2, all_29_4, all_29_1, % 23.27/3.86 | | | | | all_29_0, simplifying with (17), (23), (48), (84), (108) % 23.27/3.86 | | | | | gives: % 23.27/3.86 | | | | | (122) ? [v0: any] : ? [v1: any] : (mem(all_78_2, all_29_1) = v1 & % 23.27/3.86 | | | | | mem(all_78_2, all_29_4) = v0 & (v1 = 0 | v0 = 0)) % 23.27/3.86 | | | | | % 23.27/3.86 | | | | | GROUND_INST: instantiating (1) with all_37_1, all_29_0, all_110_1, % 23.27/3.86 | | | | | simplifying with (19), (38), (40), (105), (110) gives: % 23.27/3.86 | | | | | (123) mem(all_110_1, all_29_0) = 0 % 23.27/3.86 | | | | | % 23.27/3.86 | | | | | GROUND_INST: instantiating (2) with all_110_1, all_78_2, all_129_0, % 23.27/3.86 | | | | | simplifying with (84), (105), (121) gives: % 23.27/3.86 | | | | | (124) all_129_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & % 23.27/3.86 | | | | | mem(v0, all_110_1) = 0 & mem(v0, all_78_2) = v1 & $i(v0)) % 23.27/3.86 | | | | | % 23.27/3.86 | | | | | DELTA: instantiating (122) with fresh symbols all_137_0, all_137_1 % 23.27/3.86 | | | | | gives: % 23.27/3.86 | | | | | (125) mem(all_78_2, all_29_1) = all_137_0 & mem(all_78_2, all_29_4) % 23.27/3.86 | | | | | = all_137_1 & (all_137_0 = 0 | all_137_1 = 0) % 23.27/3.86 | | | | | % 23.27/3.87 | | | | | ALPHA: (125) implies: % 23.27/3.87 | | | | | (126) mem(all_78_2, all_29_4) = all_137_1 % 23.27/3.87 | | | | | (127) mem(all_78_2, all_29_1) = all_137_0 % 23.27/3.87 | | | | | (128) all_137_0 = 0 | all_137_1 = 0 % 23.27/3.87 | | | | | % 23.27/3.87 | | | | | BETA: splitting (124) gives: % 23.27/3.87 | | | | | % 23.27/3.87 | | | | | Case 1: % 23.27/3.87 | | | | | | % 23.27/3.87 | | | | | | (129) all_129_0 = 0 % 23.27/3.87 | | | | | | % 23.27/3.87 | | | | | | REDUCE: (120), (129) imply: % 23.27/3.87 | | | | | | (130) $false % 23.27/3.87 | | | | | | % 23.27/3.87 | | | | | | CLOSE: (130) is inconsistent. % 23.27/3.87 | | | | | | % 23.27/3.87 | | | | | Case 2: % 23.27/3.87 | | | | | | % 23.27/3.87 | | | | | | (131) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & mem(v0, % 23.27/3.87 | | | | | | all_110_1) = 0 & mem(v0, all_78_2) = v1 & $i(v0)) % 23.27/3.87 | | | | | | % 23.27/3.87 | | | | | | DELTA: instantiating (131) with fresh symbols all_143_0, all_143_1 % 23.27/3.87 | | | | | | gives: % 23.27/3.87 | | | | | | (132) ~ (all_143_0 = 0) & mem(all_143_1, all_110_1) = 0 & % 23.27/3.87 | | | | | | mem(all_143_1, all_78_2) = all_143_0 & $i(all_143_1) % 23.27/3.87 | | | | | | % 23.27/3.87 | | | | | | ALPHA: (132) implies: % 23.27/3.87 | | | | | | (133) ~ (all_143_0 = 0) % 23.27/3.87 | | | | | | (134) $i(all_143_1) % 23.27/3.87 | | | | | | (135) mem(all_143_1, all_78_2) = all_143_0 % 23.27/3.87 | | | | | | (136) mem(all_143_1, all_110_1) = 0 % 23.27/3.87 | | | | | | % 23.27/3.87 | | | | | | GROUND_INST: instantiating (4) with all_110_1, all_29_4, all_29_1, % 23.27/3.87 | | | | | | all_29_0, simplifying with (17), (23), (48), (105), % 23.27/3.87 | | | | | | (123) gives: % 23.27/3.87 | | | | | | (137) ? [v0: any] : ? [v1: any] : (mem(all_110_1, all_29_1) = % 23.27/3.87 | | | | | | v1 & mem(all_110_1, all_29_4) = v0 & (v1 = 0 | v0 = 0)) % 23.27/3.87 | | | | | | % 23.27/3.87 | | | | | | DELTA: instantiating (137) with fresh symbols all_150_0, all_150_1 % 23.27/3.87 | | | | | | gives: % 23.27/3.87 | | | | | | (138) mem(all_110_1, all_29_1) = all_150_0 & mem(all_110_1, % 23.27/3.87 | | | | | | all_29_4) = all_150_1 & (all_150_0 = 0 | all_150_1 = 0) % 23.27/3.87 | | | | | | % 23.27/3.87 | | | | | | ALPHA: (138) implies: % 23.27/3.87 | | | | | | (139) mem(all_110_1, all_29_4) = all_150_1 % 23.27/3.87 | | | | | | (140) mem(all_110_1, all_29_1) = all_150_0 % 23.27/3.87 | | | | | | (141) all_150_0 = 0 | all_150_1 = 0 % 23.27/3.87 | | | | | | % 23.27/3.87 | | | | | | BETA: splitting (81) gives: % 23.27/3.87 | | | | | | % 23.27/3.87 | | | | | | Case 1: % 23.27/3.87 | | | | | | | % 23.27/3.87 | | | | | | | (142) all_76_0 = 0 % 23.27/3.87 | | | | | | | % 23.27/3.87 | | | | | | | REDUCE: (80), (142) imply: % 23.27/3.87 | | | | | | | (143) mem(all_58_1, all_29_1) = 0 % 23.27/3.87 | | | | | | | % 23.27/3.87 | | | | | | | GROUND_INST: instantiating (4) with all_58_1, all_29_2, all_46_0, % 23.27/3.87 | | | | | | | all_29_1, simplifying with (18), (49), (51), (69), % 23.27/3.87 | | | | | | | (143) gives: % 23.27/3.87 | | | | | | | (144) ? [v0: any] : ? [v1: any] : (mem(all_58_1, all_46_0) = % 23.27/3.87 | | | | | | | v1 & mem(all_58_1, all_29_2) = v0 & (v1 = 0 | v0 = 0)) % 23.27/3.87 | | | | | | | % 23.27/3.87 | | | | | | | DELTA: instantiating (144) with fresh symbols all_164_0, all_164_1 % 23.27/3.87 | | | | | | | gives: % 23.27/3.87 | | | | | | | (145) mem(all_58_1, all_46_0) = all_164_0 & mem(all_58_1, % 23.27/3.87 | | | | | | | all_29_2) = all_164_1 & (all_164_0 = 0 | all_164_1 = 0) % 23.27/3.87 | | | | | | | % 23.27/3.87 | | | | | | | ALPHA: (145) implies: % 23.27/3.87 | | | | | | | (146) mem(all_58_1, all_29_2) = all_164_1 % 23.27/3.87 | | | | | | | (147) mem(all_58_1, all_46_0) = all_164_0 % 23.27/3.87 | | | | | | | (148) all_164_0 = 0 | all_164_1 = 0 % 23.27/3.87 | | | | | | | % 23.27/3.87 | | | | | | | BETA: splitting (115) gives: % 23.27/3.87 | | | | | | | % 23.27/3.87 | | | | | | | Case 1: % 23.27/3.87 | | | | | | | | % 23.27/3.87 | | | | | | | | (149) all_123_0 = 0 % 23.27/3.87 | | | | | | | | % 23.27/3.87 | | | | | | | | REDUCE: (114), (149) imply: % 23.27/3.87 | | | | | | | | (150) mem(all_89_1, all_29_1) = 0 % 23.27/3.87 | | | | | | | | % 23.27/3.87 | | | | | | | | GROUND_INST: instantiating (4) with all_89_1, all_29_2, % 23.27/3.87 | | | | | | | | all_46_0, all_29_1, simplifying with (18), (49), % 23.27/3.87 | | | | | | | | (51), (94), (150) gives: % 23.27/3.87 | | | | | | | | (151) ? [v0: any] : ? [v1: any] : (mem(all_89_1, all_46_0) % 23.27/3.87 | | | | | | | | = v1 & mem(all_89_1, all_29_2) = v0 & (v1 = 0 | v0 = % 23.27/3.87 | | | | | | | | 0)) % 23.27/3.87 | | | | | | | | % 23.27/3.87 | | | | | | | | DELTA: instantiating (151) with fresh symbols all_178_0, % 23.27/3.87 | | | | | | | | all_178_1 gives: % 23.27/3.87 | | | | | | | | (152) mem(all_89_1, all_46_0) = all_178_0 & mem(all_89_1, % 23.27/3.87 | | | | | | | | all_29_2) = all_178_1 & (all_178_0 = 0 | all_178_1 = % 23.27/3.87 | | | | | | | | 0) % 23.27/3.87 | | | | | | | | % 23.27/3.87 | | | | | | | | ALPHA: (152) implies: % 23.27/3.87 | | | | | | | | (153) mem(all_89_1, all_29_2) = all_178_1 % 23.27/3.87 | | | | | | | | (154) mem(all_89_1, all_46_0) = all_178_0 % 23.27/3.87 | | | | | | | | (155) all_178_0 = 0 | all_178_1 = 0 % 23.27/3.87 | | | | | | | | % 23.27/3.87 | | | | | | | | BETA: splitting (128) gives: % 23.27/3.87 | | | | | | | | % 23.27/3.87 | | | | | | | | Case 1: % 23.27/3.87 | | | | | | | | | % 23.27/3.87 | | | | | | | | | (156) all_137_0 = 0 % 23.27/3.87 | | | | | | | | | % 23.27/3.87 | | | | | | | | | REDUCE: (127), (156) imply: % 23.27/3.87 | | | | | | | | | (157) mem(all_78_2, all_29_1) = 0 % 23.27/3.87 | | | | | | | | | % 23.27/3.87 | | | | | | | | | GROUND_INST: instantiating (4) with all_78_2, all_29_2, % 23.27/3.87 | | | | | | | | | all_46_0, all_29_1, simplifying with (18), (49), % 23.27/3.87 | | | | | | | | | (51), (84), (157) gives: % 23.27/3.87 | | | | | | | | | (158) ? [v0: any] : ? [v1: any] : (mem(all_78_2, % 23.27/3.87 | | | | | | | | | all_46_0) = v1 & mem(all_78_2, all_29_2) = v0 & % 23.27/3.87 | | | | | | | | | (v1 = 0 | v0 = 0)) % 23.27/3.87 | | | | | | | | | % 23.27/3.87 | | | | | | | | | DELTA: instantiating (158) with fresh symbols all_192_0, % 23.27/3.87 | | | | | | | | | all_192_1 gives: % 23.27/3.87 | | | | | | | | | (159) mem(all_78_2, all_46_0) = all_192_0 & mem(all_78_2, % 23.27/3.87 | | | | | | | | | all_29_2) = all_192_1 & (all_192_0 = 0 | all_192_1 % 23.27/3.87 | | | | | | | | | = 0) % 23.27/3.87 | | | | | | | | | % 23.27/3.87 | | | | | | | | | ALPHA: (159) implies: % 23.27/3.87 | | | | | | | | | (160) mem(all_78_2, all_29_2) = all_192_1 % 23.27/3.87 | | | | | | | | | (161) mem(all_78_2, all_46_0) = all_192_0 % 23.27/3.87 | | | | | | | | | (162) all_192_0 = 0 | all_192_1 = 0 % 23.27/3.87 | | | | | | | | | % 23.27/3.87 | | | | | | | | | BETA: splitting (148) gives: % 23.27/3.87 | | | | | | | | | % 23.27/3.87 | | | | | | | | | Case 1: % 23.27/3.87 | | | | | | | | | | % 23.27/3.87 | | | | | | | | | | (163) all_164_0 = 0 % 23.27/3.87 | | | | | | | | | | % 23.27/3.87 | | | | | | | | | | REDUCE: (147), (163) imply: % 23.27/3.87 | | | | | | | | | | (164) mem(all_58_1, all_46_0) = 0 % 23.27/3.87 | | | | | | | | | | % 23.27/3.87 | | | | | | | | | | GROUND_INST: instantiating (3) with all_58_1, all_29_2, % 23.27/3.87 | | | | | | | | | | all_46_0, simplifying with (18), (50), (69), (164) % 23.27/3.87 | | | | | | | | | | gives: % 23.27/3.87 | | | | | | | | | | (165) all_58_1 = all_29_2 % 23.27/3.87 | | | | | | | | | | % 23.27/3.87 | | | | | | | | | | REDUCE: (71), (165) imply: % 23.27/3.87 | | | | | | | | | | (166) mem(all_29_2, all_37_1) = all_58_0 % 23.27/3.87 | | | | | | | | | | % 23.27/3.87 | | | | | | | | | | BETA: splitting (155) gives: % 23.27/3.87 | | | | | | | | | | % 23.27/3.87 | | | | | | | | | | Case 1: % 23.27/3.87 | | | | | | | | | | | % 23.27/3.87 | | | | | | | | | | | (167) all_178_0 = 0 % 23.27/3.87 | | | | | | | | | | | % 23.27/3.87 | | | | | | | | | | | REDUCE: (154), (167) imply: % 23.27/3.87 | | | | | | | | | | | (168) mem(all_89_1, all_46_0) = 0 % 23.27/3.87 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | REF_CLOSE: (3), (15), (18), (50), (68), (94), (95), (166), % 23.27/3.88 | | | | | | | | | | | (168) are inconsistent by sub-proof #12. % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | Case 2: % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | (169) all_178_1 = 0 % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | REDUCE: (153), (169) imply: % 23.27/3.88 | | | | | | | | | | | (170) mem(all_89_1, all_29_2) = 0 % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | GROUND_INST: instantiating (3) with all_89_1, all_29_3, % 23.27/3.88 | | | | | | | | | | | all_29_2, simplifying with (22), (74), (94), (170) % 23.27/3.88 | | | | | | | | | | | gives: % 23.27/3.88 | | | | | | | | | | | (171) all_89_1 = all_29_3 % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | REDUCE: (96), (171) imply: % 23.27/3.88 | | | | | | | | | | | (172) mem(all_29_3, all_52_1) = all_89_0 % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | BETA: splitting (162) gives: % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | Case 1: % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | | (173) all_192_0 = 0 % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | | REDUCE: (161), (173) imply: % 23.27/3.88 | | | | | | | | | | | | (174) mem(all_78_2, all_46_0) = 0 % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | | REF_CLOSE: (3), (15), (18), (50), (68), (84), (97), (166), % 23.27/3.88 | | | | | | | | | | | | (174) are inconsistent by sub-proof #11. % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | Case 2: % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | | (175) all_192_1 = 0 % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | | REDUCE: (160), (175) imply: % 23.27/3.88 | | | | | | | | | | | | (176) mem(all_78_2, all_29_2) = 0 % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | | REF_CLOSE: (3), (15), (22), (74), (84), (86), (93), (172), % 23.27/3.88 | | | | | | | | | | | | (176) are inconsistent by sub-proof #10. % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | End of split % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | End of split % 23.27/3.88 | | | | | | | | | | % 23.27/3.88 | | | | | | | | | Case 2: % 23.27/3.88 | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | (177) all_164_1 = 0 % 23.27/3.88 | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | REDUCE: (146), (177) imply: % 23.27/3.88 | | | | | | | | | | (178) mem(all_58_1, all_29_2) = 0 % 23.27/3.88 | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | GROUND_INST: instantiating (3) with all_58_1, all_29_3, % 23.27/3.88 | | | | | | | | | | all_29_2, simplifying with (22), (69), (74), (178) % 23.27/3.88 | | | | | | | | | | gives: % 23.27/3.88 | | | | | | | | | | (179) all_58_1 = all_29_3 % 23.27/3.88 | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | REDUCE: (71), (179) imply: % 23.27/3.88 | | | | | | | | | | (180) mem(all_29_3, all_37_1) = all_58_0 % 23.27/3.88 | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | BETA: splitting (155) gives: % 23.27/3.88 | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | Case 1: % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | (181) all_178_0 = 0 % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | REDUCE: (154), (181) imply: % 23.27/3.88 | | | | | | | | | | | (182) mem(all_89_1, all_46_0) = 0 % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | GROUND_INST: instantiating (3) with all_89_1, all_29_2, % 23.27/3.88 | | | | | | | | | | | all_46_0, simplifying with (18), (50), (94), (182) % 23.27/3.88 | | | | | | | | | | | gives: % 23.27/3.88 | | | | | | | | | | | (183) all_89_1 = all_29_2 % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | REDUCE: (96), (183) imply: % 23.27/3.88 | | | | | | | | | | | (184) mem(all_29_2, all_52_1) = all_89_0 % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | BETA: splitting (162) gives: % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | Case 1: % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | | (185) all_192_0 = 0 % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | | REDUCE: (161), (185) imply: % 23.27/3.88 | | | | | | | | | | | | (186) mem(all_78_2, all_46_0) = 0 % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | | REF_CLOSE: (3), (15), (18), (50), (84), (86), (93), (184), % 23.27/3.88 | | | | | | | | | | | | (186) are inconsistent by sub-proof #9. % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | Case 2: % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | | (187) all_192_1 = 0 % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | | REDUCE: (160), (187) imply: % 23.27/3.88 | | | | | | | | | | | | (188) mem(all_78_2, all_29_2) = 0 % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | | REF_CLOSE: (3), (15), (22), (68), (74), (84), (97), (180), % 23.27/3.88 | | | | | | | | | | | | (188) are inconsistent by sub-proof #8. % 23.27/3.88 | | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | End of split % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | Case 2: % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | (189) all_178_1 = 0 % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | REDUCE: (153), (189) imply: % 23.27/3.88 | | | | | | | | | | | (190) mem(all_89_1, all_29_2) = 0 % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | REF_CLOSE: (3), (15), (22), (68), (74), (94), (95), (180), % 23.27/3.88 | | | | | | | | | | | (190) are inconsistent by sub-proof #7. % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | End of split % 23.27/3.88 | | | | | | | | | | % 23.27/3.88 | | | | | | | | | End of split % 23.27/3.88 | | | | | | | | | % 23.27/3.88 | | | | | | | | Case 2: % 23.27/3.88 | | | | | | | | | % 23.27/3.88 | | | | | | | | | (191) all_137_1 = 0 % 23.27/3.88 | | | | | | | | | % 23.27/3.88 | | | | | | | | | REDUCE: (126), (191) imply: % 23.27/3.88 | | | | | | | | | (192) mem(all_78_2, all_29_4) = 0 % 23.27/3.88 | | | | | | | | | % 23.27/3.88 | | | | | | | | | GROUND_INST: instantiating (3) with all_78_2, all_29_5, % 23.27/3.88 | | | | | | | | | all_29_4, simplifying with (21), (53), (84), (192) % 23.27/3.88 | | | | | | | | | gives: % 23.27/3.88 | | | | | | | | | (193) all_78_2 = all_29_5 % 23.27/3.88 | | | | | | | | | % 23.27/3.88 | | | | | | | | | REDUCE: (121), (193) imply: % 23.27/3.88 | | | | | | | | | (194) subq(all_110_1, all_29_5) = all_129_0 % 23.27/3.88 | | | | | | | | | % 23.27/3.88 | | | | | | | | | REDUCE: (135), (193) imply: % 23.27/3.88 | | | | | | | | | (195) mem(all_143_1, all_29_5) = all_143_0 % 23.27/3.88 | | | | | | | | | % 23.27/3.88 | | | | | | | | | GROUND_INST: instantiating (5) with all_143_1, all_29_6, % 23.27/3.88 | | | | | | | | | all_29_3, all_29_5, all_143_0, simplifying with % 23.27/3.88 | | | | | | | | | (29), (73), (74), (134), (195) gives: % 23.27/3.88 | | | | | | | | | (196) all_143_0 = 0 | ? [v0: int] : ? [v1: int] : ( ~ (v1 % 23.27/3.88 | | | | | | | | | = 0) & ~ (v0 = 0) & mem(all_143_1, all_29_3) = % 23.27/3.88 | | | | | | | | | v1 & mem(all_143_1, all_29_6) = v0) % 23.27/3.88 | | | | | | | | | % 23.27/3.88 | | | | | | | | | GROUND_INST: instantiating (2) with all_110_1, all_29_5, % 23.27/3.88 | | | | | | | | | all_129_0, simplifying with (53), (105), (194) % 23.27/3.88 | | | | | | | | | gives: % 23.27/3.88 | | | | | | | | | (197) all_129_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 % 23.27/3.88 | | | | | | | | | = 0) & mem(v0, all_110_1) = 0 & mem(v0, all_29_5) % 23.27/3.88 | | | | | | | | | = v1 & $i(v0)) % 23.27/3.88 | | | | | | | | | % 23.27/3.88 | | | | | | | | | BETA: splitting (141) gives: % 23.27/3.88 | | | | | | | | | % 23.27/3.88 | | | | | | | | | Case 1: % 23.27/3.88 | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | (198) all_150_0 = 0 % 23.27/3.88 | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | REDUCE: (140), (198) imply: % 23.27/3.88 | | | | | | | | | | (199) mem(all_110_1, all_29_1) = 0 % 23.27/3.88 | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | BETA: splitting (196) gives: % 23.27/3.88 | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | Case 1: % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | (200) all_143_0 = 0 % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | REDUCE: (133), (200) imply: % 23.27/3.88 | | | | | | | | | | | (201) $false % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | CLOSE: (201) is inconsistent. % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | Case 2: % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | GROUND_INST: instantiating (4) with all_110_1, all_29_2, % 23.27/3.88 | | | | | | | | | | | all_46_0, all_29_1, simplifying with (18), (49), % 23.27/3.88 | | | | | | | | | | | (51), (105), (199) gives: % 23.27/3.88 | | | | | | | | | | | (202) ? [v0: any] : ? [v1: any] : (mem(all_110_1, % 23.27/3.88 | | | | | | | | | | | all_46_0) = v1 & mem(all_110_1, all_29_2) = v0 % 23.27/3.88 | | | | | | | | | | | & (v1 = 0 | v0 = 0)) % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | DELTA: instantiating (202) with fresh symbols all_222_0, % 23.27/3.88 | | | | | | | | | | | all_222_1 gives: % 23.27/3.88 | | | | | | | | | | | (203) mem(all_110_1, all_46_0) = all_222_0 & % 23.27/3.88 | | | | | | | | | | | mem(all_110_1, all_29_2) = all_222_1 & (all_222_0 % 23.27/3.88 | | | | | | | | | | | = 0 | all_222_1 = 0) % 23.27/3.88 | | | | | | | | | | | % 23.27/3.88 | | | | | | | | | | | ALPHA: (203) implies: % 23.27/3.89 | | | | | | | | | | | (204) mem(all_110_1, all_29_2) = all_222_1 % 23.27/3.89 | | | | | | | | | | | (205) mem(all_110_1, all_46_0) = all_222_0 % 23.27/3.89 | | | | | | | | | | | (206) all_222_0 = 0 | all_222_1 = 0 % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | BETA: splitting (148) gives: % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | Case 1: % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | (207) all_164_0 = 0 % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | REDUCE: (147), (207) imply: % 23.27/3.89 | | | | | | | | | | | | (208) mem(all_58_1, all_46_0) = 0 % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | GROUND_INST: instantiating (3) with all_58_1, all_29_2, % 23.27/3.89 | | | | | | | | | | | | all_46_0, simplifying with (18), (50), (69), (208) % 23.27/3.89 | | | | | | | | | | | | gives: % 23.27/3.89 | | | | | | | | | | | | (209) all_58_1 = all_29_2 % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | REDUCE: (71), (209) imply: % 23.27/3.89 | | | | | | | | | | | | (210) mem(all_29_2, all_37_1) = all_58_0 % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | BETA: splitting (155) gives: % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | Case 1: % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | (211) all_178_0 = 0 % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | REDUCE: (154), (211) imply: % 23.27/3.89 | | | | | | | | | | | | | (212) mem(all_89_1, all_46_0) = 0 % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | REF_CLOSE: (3), (15), (18), (50), (68), (94), (95), (210), % 23.27/3.89 | | | | | | | | | | | | | (212) are inconsistent by sub-proof #12. % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | Case 2: % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | (213) all_178_1 = 0 % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | REDUCE: (153), (213) imply: % 23.27/3.89 | | | | | | | | | | | | | (214) mem(all_89_1, all_29_2) = 0 % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | GROUND_INST: instantiating (3) with all_89_1, all_29_3, % 23.27/3.89 | | | | | | | | | | | | | all_29_2, simplifying with (22), (74), (94), (214) % 23.27/3.89 | | | | | | | | | | | | | gives: % 23.27/3.89 | | | | | | | | | | | | | (215) all_89_1 = all_29_3 % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | REDUCE: (96), (215) imply: % 23.27/3.89 | | | | | | | | | | | | | (216) mem(all_29_3, all_52_1) = all_89_0 % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | BETA: splitting (206) gives: % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | Case 1: % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | | (217) all_222_0 = 0 % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | | REDUCE: (205), (217) imply: % 23.27/3.89 | | | | | | | | | | | | | | (218) mem(all_110_1, all_46_0) = 0 % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | | REF_CLOSE: (3), (15), (18), (50), (68), (105), (110), (210), % 23.27/3.89 | | | | | | | | | | | | | | (218) are inconsistent by sub-proof #6. % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | Case 2: % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | | (219) all_222_1 = 0 % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | | REDUCE: (204), (219) imply: % 23.27/3.89 | | | | | | | | | | | | | | (220) mem(all_110_1, all_29_2) = 0 % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | | REF_CLOSE: (3), (15), (22), (74), (93), (105), (106), (216), % 23.27/3.89 | | | | | | | | | | | | | | (220) are inconsistent by sub-proof #5. % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | End of split % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | End of split % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | Case 2: % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | (221) all_164_1 = 0 % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | REDUCE: (146), (221) imply: % 23.27/3.89 | | | | | | | | | | | | (222) mem(all_58_1, all_29_2) = 0 % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | GROUND_INST: instantiating (3) with all_58_1, all_29_3, % 23.27/3.89 | | | | | | | | | | | | all_29_2, simplifying with (22), (69), (74), (222) % 23.27/3.89 | | | | | | | | | | | | gives: % 23.27/3.89 | | | | | | | | | | | | (223) all_58_1 = all_29_3 % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | REDUCE: (71), (223) imply: % 23.27/3.89 | | | | | | | | | | | | (224) mem(all_29_3, all_37_1) = all_58_0 % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | BETA: splitting (155) gives: % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | Case 1: % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | (225) all_178_0 = 0 % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | REDUCE: (154), (225) imply: % 23.27/3.89 | | | | | | | | | | | | | (226) mem(all_89_1, all_46_0) = 0 % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | GROUND_INST: instantiating (3) with all_89_1, all_29_2, % 23.27/3.89 | | | | | | | | | | | | | all_46_0, simplifying with (18), (50), (94), (226) % 23.27/3.89 | | | | | | | | | | | | | gives: % 23.27/3.89 | | | | | | | | | | | | | (227) all_89_1 = all_29_2 % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | REDUCE: (96), (227) imply: % 23.27/3.89 | | | | | | | | | | | | | (228) mem(all_29_2, all_52_1) = all_89_0 % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | BETA: splitting (206) gives: % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | Case 1: % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | | (229) all_222_0 = 0 % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | | REDUCE: (205), (229) imply: % 23.27/3.89 | | | | | | | | | | | | | | (230) mem(all_110_1, all_46_0) = 0 % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | | REF_CLOSE: (3), (15), (18), (50), (93), (105), (106), (228), % 23.27/3.89 | | | | | | | | | | | | | | (230) are inconsistent by sub-proof #4. % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | Case 2: % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | | (231) all_222_1 = 0 % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | | REDUCE: (204), (231) imply: % 23.27/3.89 | | | | | | | | | | | | | | (232) mem(all_110_1, all_29_2) = 0 % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | | REF_CLOSE: (3), (15), (22), (68), (74), (105), (110), (224), % 23.27/3.89 | | | | | | | | | | | | | | (232) are inconsistent by sub-proof #3. % 23.27/3.89 | | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | End of split % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | Case 2: % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | (233) all_178_1 = 0 % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | REDUCE: (153), (233) imply: % 23.27/3.89 | | | | | | | | | | | | | (234) mem(all_89_1, all_29_2) = 0 % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | | REF_CLOSE: (3), (15), (22), (68), (74), (94), (95), (224), % 23.27/3.89 | | | | | | | | | | | | | (234) are inconsistent by sub-proof #7. % 23.27/3.89 | | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | | End of split % 23.27/3.89 | | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | End of split % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | End of split % 23.27/3.89 | | | | | | | | | | % 23.27/3.89 | | | | | | | | | Case 2: % 23.27/3.89 | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | (235) all_150_1 = 0 % 23.27/3.89 | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | REDUCE: (139), (235) imply: % 23.27/3.89 | | | | | | | | | | (236) mem(all_110_1, all_29_4) = 0 % 23.27/3.89 | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | BETA: splitting (197) gives: % 23.27/3.89 | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | Case 1: % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | (237) all_129_0 = 0 % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | REDUCE: (120), (237) imply: % 23.27/3.89 | | | | | | | | | | | (238) $false % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | CLOSE: (238) is inconsistent. % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | Case 2: % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | GROUND_INST: instantiating (3) with all_110_1, all_29_5, % 23.27/3.89 | | | | | | | | | | | all_29_4, simplifying with (21), (53), (105), % 23.27/3.89 | | | | | | | | | | | (236) gives: % 23.27/3.89 | | | | | | | | | | | (239) all_110_1 = all_29_5 % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | REDUCE: (136), (239) imply: % 23.27/3.89 | | | | | | | | | | | (240) mem(all_143_1, all_29_5) = 0 % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | GROUND_INST: instantiating (15) with all_143_0, 0, all_29_5, % 23.27/3.89 | | | | | | | | | | | all_143_1, simplifying with (195), (240) gives: % 23.27/3.89 | | | | | | | | | | | (241) all_143_0 = 0 % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | REDUCE: (133), (241) imply: % 23.27/3.89 | | | | | | | | | | | (242) $false % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | | CLOSE: (242) is inconsistent. % 23.27/3.89 | | | | | | | | | | | % 23.27/3.89 | | | | | | | | | | End of split % 23.27/3.89 | | | | | | | | | | % 23.27/3.89 | | | | | | | | | End of split % 23.27/3.89 | | | | | | | | | % 23.27/3.89 | | | | | | | | End of split % 23.27/3.89 | | | | | | | | % 23.27/3.89 | | | | | | | Case 2: % 23.27/3.89 | | | | | | | | % 23.27/3.89 | | | | | | | | (243) all_123_1 = 0 % 23.27/3.89 | | | | | | | | % 23.27/3.89 | | | | | | | | REDUCE: (113), (243) imply: % 23.27/3.89 | | | | | | | | (244) mem(all_89_1, all_29_4) = 0 % 23.27/3.89 | | | | | | | | % 23.27/3.89 | | | | | | | | GROUND_INST: instantiating (3) with all_89_1, all_29_5, % 23.27/3.89 | | | | | | | | all_29_4, simplifying with (21), (53), (94), (244) % 23.27/3.89 | | | | | | | | gives: % 23.27/3.89 | | | | | | | | (245) all_89_1 = all_29_5 % 23.27/3.89 | | | | | | | | % 23.27/3.89 | | | | | | | | REDUCE: (96), (245) imply: % 23.27/3.89 | | | | | | | | (246) mem(all_29_5, all_52_1) = all_89_0 % 23.27/3.89 | | | | | | | | % 23.27/3.89 | | | | | | | | BETA: splitting (128) gives: % 23.27/3.89 | | | | | | | | % 23.27/3.89 | | | | | | | | Case 1: % 23.27/3.89 | | | | | | | | | % 23.27/3.89 | | | | | | | | | (247) all_137_0 = 0 % 23.27/3.89 | | | | | | | | | % 23.27/3.89 | | | | | | | | | REDUCE: (127), (247) imply: % 23.27/3.89 | | | | | | | | | (248) mem(all_78_2, all_29_1) = 0 % 23.27/3.89 | | | | | | | | | % 23.27/3.89 | | | | | | | | | GROUND_INST: instantiating (4) with all_78_2, all_29_2, % 23.27/3.89 | | | | | | | | | all_46_0, all_29_1, simplifying with (18), (49), % 23.27/3.89 | | | | | | | | | (51), (84), (248) gives: % 23.27/3.89 | | | | | | | | | (249) ? [v0: any] : ? [v1: any] : (mem(all_78_2, % 23.27/3.89 | | | | | | | | | all_46_0) = v1 & mem(all_78_2, all_29_2) = v0 & % 23.27/3.89 | | | | | | | | | (v1 = 0 | v0 = 0)) % 23.27/3.89 | | | | | | | | | % 23.27/3.89 | | | | | | | | | DELTA: instantiating (249) with fresh symbols all_197_0, % 23.27/3.89 | | | | | | | | | all_197_1 gives: % 23.27/3.89 | | | | | | | | | (250) mem(all_78_2, all_46_0) = all_197_0 & mem(all_78_2, % 23.27/3.89 | | | | | | | | | all_29_2) = all_197_1 & (all_197_0 = 0 | all_197_1 % 23.27/3.89 | | | | | | | | | = 0) % 23.27/3.89 | | | | | | | | | % 23.27/3.89 | | | | | | | | | ALPHA: (250) implies: % 23.27/3.89 | | | | | | | | | (251) mem(all_78_2, all_29_2) = all_197_1 % 23.27/3.89 | | | | | | | | | (252) mem(all_78_2, all_46_0) = all_197_0 % 23.27/3.90 | | | | | | | | | (253) all_197_0 = 0 | all_197_1 = 0 % 23.27/3.90 | | | | | | | | | % 23.27/3.90 | | | | | | | | | BETA: splitting (141) gives: % 23.27/3.90 | | | | | | | | | % 23.27/3.90 | | | | | | | | | Case 1: % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | (254) all_150_0 = 0 % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | REDUCE: (140), (254) imply: % 23.27/3.90 | | | | | | | | | | (255) mem(all_110_1, all_29_1) = 0 % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | GROUND_INST: instantiating (4) with all_110_1, all_29_2, % 23.27/3.90 | | | | | | | | | | all_46_0, all_29_1, simplifying with (18), (49), % 23.27/3.90 | | | | | | | | | | (51), (105), (255) gives: % 23.27/3.90 | | | | | | | | | | (256) ? [v0: any] : ? [v1: any] : (mem(all_110_1, % 23.27/3.90 | | | | | | | | | | all_46_0) = v1 & mem(all_110_1, all_29_2) = v0 % 23.27/3.90 | | | | | | | | | | & (v1 = 0 | v0 = 0)) % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | DELTA: instantiating (256) with fresh symbols all_211_0, % 23.27/3.90 | | | | | | | | | | all_211_1 gives: % 23.27/3.90 | | | | | | | | | | (257) mem(all_110_1, all_46_0) = all_211_0 & % 23.27/3.90 | | | | | | | | | | mem(all_110_1, all_29_2) = all_211_1 & (all_211_0 = % 23.27/3.90 | | | | | | | | | | 0 | all_211_1 = 0) % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | ALPHA: (257) implies: % 23.27/3.90 | | | | | | | | | | (258) mem(all_110_1, all_29_2) = all_211_1 % 23.27/3.90 | | | | | | | | | | (259) mem(all_110_1, all_46_0) = all_211_0 % 23.27/3.90 | | | | | | | | | | (260) all_211_0 = 0 | all_211_1 = 0 % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | BETA: splitting (148) gives: % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | Case 1: % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | (261) all_164_0 = 0 % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | REDUCE: (147), (261) imply: % 23.27/3.90 | | | | | | | | | | | (262) mem(all_58_1, all_46_0) = 0 % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | GROUND_INST: instantiating (3) with all_58_1, all_29_2, % 23.27/3.90 | | | | | | | | | | | all_46_0, simplifying with (18), (50), (69), (262) % 23.27/3.90 | | | | | | | | | | | gives: % 23.27/3.90 | | | | | | | | | | | (263) all_58_1 = all_29_2 % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | REDUCE: (71), (263) imply: % 23.27/3.90 | | | | | | | | | | | (264) mem(all_29_2, all_37_1) = all_58_0 % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | BETA: splitting (253) gives: % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | Case 1: % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | (265) all_197_0 = 0 % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | REDUCE: (252), (265) imply: % 23.27/3.90 | | | | | | | | | | | | (266) mem(all_78_2, all_46_0) = 0 % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | REF_CLOSE: (3), (15), (18), (50), (68), (84), (97), (264), % 23.27/3.90 | | | | | | | | | | | | (266) are inconsistent by sub-proof #11. % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | Case 2: % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | (267) all_197_1 = 0 % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | REDUCE: (251), (267) imply: % 23.27/3.90 | | | | | | | | | | | | (268) mem(all_78_2, all_29_2) = 0 % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | GROUND_INST: instantiating (3) with all_78_2, all_29_3, % 23.27/3.90 | | | | | | | | | | | | all_29_2, simplifying with (22), (74), (84), (268) % 23.27/3.90 | | | | | | | | | | | | gives: % 23.27/3.90 | | | | | | | | | | | | (269) all_78_2 = all_29_3 % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | REDUCE: (135), (269) imply: % 23.27/3.90 | | | | | | | | | | | | (270) mem(all_143_1, all_29_3) = all_143_0 % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | BETA: splitting (260) gives: % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | Case 1: % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | | (271) all_211_0 = 0 % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | | REDUCE: (259), (271) imply: % 23.27/3.90 | | | | | | | | | | | | | (272) mem(all_110_1, all_46_0) = 0 % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | | REF_CLOSE: (3), (15), (18), (50), (68), (105), (110), (264), % 23.27/3.90 | | | | | | | | | | | | | (272) are inconsistent by sub-proof #6. % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | Case 2: % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | | (273) all_211_1 = 0 % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | | REDUCE: (258), (273) imply: % 23.27/3.90 | | | | | | | | | | | | | (274) mem(all_110_1, all_29_2) = 0 % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | | REF_CLOSE: (3), (15), (22), (74), (105), (133), (136), (270), % 23.27/3.90 | | | | | | | | | | | | | (274) are inconsistent by sub-proof #2. % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | End of split % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | End of split % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | Case 2: % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | (275) all_164_1 = 0 % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | REDUCE: (146), (275) imply: % 23.27/3.90 | | | | | | | | | | | (276) mem(all_58_1, all_29_2) = 0 % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | GROUND_INST: instantiating (3) with all_58_1, all_29_3, % 23.27/3.90 | | | | | | | | | | | all_29_2, simplifying with (22), (69), (74), (276) % 23.27/3.90 | | | | | | | | | | | gives: % 23.27/3.90 | | | | | | | | | | | (277) all_58_1 = all_29_3 % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | REDUCE: (71), (277) imply: % 23.27/3.90 | | | | | | | | | | | (278) mem(all_29_3, all_37_1) = all_58_0 % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | BETA: splitting (253) gives: % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | Case 1: % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | (279) all_197_0 = 0 % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | REDUCE: (252), (279) imply: % 23.27/3.90 | | | | | | | | | | | | (280) mem(all_78_2, all_46_0) = 0 % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | GROUND_INST: instantiating (3) with all_78_2, all_29_2, % 23.27/3.90 | | | | | | | | | | | | all_46_0, simplifying with (18), (50), (84), (280) % 23.27/3.90 | | | | | | | | | | | | gives: % 23.27/3.90 | | | | | | | | | | | | (281) all_78_2 = all_29_2 % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | REDUCE: (135), (281) imply: % 23.27/3.90 | | | | | | | | | | | | (282) mem(all_143_1, all_29_2) = all_143_0 % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | BETA: splitting (260) gives: % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | Case 1: % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | | (283) all_211_0 = 0 % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | | REDUCE: (259), (283) imply: % 23.27/3.90 | | | | | | | | | | | | | (284) mem(all_110_1, all_46_0) = 0 % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | | REF_CLOSE: (3), (15), (18), (50), (105), (133), (136), (282), % 23.27/3.90 | | | | | | | | | | | | | (284) are inconsistent by sub-proof #1. % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | Case 2: % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | | (285) all_211_1 = 0 % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | | REDUCE: (258), (285) imply: % 23.27/3.90 | | | | | | | | | | | | | (286) mem(all_110_1, all_29_2) = 0 % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | | REF_CLOSE: (3), (15), (22), (68), (74), (105), (110), (278), % 23.27/3.90 | | | | | | | | | | | | | (286) are inconsistent by sub-proof #3. % 23.27/3.90 | | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | End of split % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | Case 2: % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | (287) all_197_1 = 0 % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | REDUCE: (251), (287) imply: % 23.27/3.90 | | | | | | | | | | | | (288) mem(all_78_2, all_29_2) = 0 % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | | REF_CLOSE: (3), (15), (22), (68), (74), (84), (97), (278), % 23.27/3.90 | | | | | | | | | | | | (288) are inconsistent by sub-proof #8. % 23.27/3.90 | | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | | End of split % 23.27/3.90 | | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | End of split % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | Case 2: % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | (289) all_150_1 = 0 % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | REDUCE: (139), (289) imply: % 23.27/3.90 | | | | | | | | | | (290) mem(all_110_1, all_29_4) = 0 % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | GROUND_INST: instantiating (3) with all_110_1, all_29_5, % 23.27/3.90 | | | | | | | | | | all_29_4, simplifying with (21), (53), (105), % 23.27/3.90 | | | | | | | | | | (290) gives: % 23.27/3.90 | | | | | | | | | | (291) all_110_1 = all_29_5 % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | REDUCE: (106), (291) imply: % 23.27/3.90 | | | | | | | | | | (292) mem(all_29_5, all_52_1) = 0 % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | GROUND_INST: instantiating (15) with all_89_0, 0, all_52_1, % 23.27/3.90 | | | | | | | | | | all_29_5, simplifying with (246), (292) gives: % 23.27/3.90 | | | | | | | | | | (293) all_89_0 = 0 % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | REDUCE: (93), (293) imply: % 23.27/3.90 | | | | | | | | | | (294) $false % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | | CLOSE: (294) is inconsistent. % 23.27/3.90 | | | | | | | | | | % 23.27/3.90 | | | | | | | | | End of split % 23.27/3.90 | | | | | | | | | % 23.27/3.90 | | | | | | | | Case 2: % 23.27/3.90 | | | | | | | | | % 23.27/3.90 | | | | | | | | | (295) all_137_1 = 0 % 23.27/3.90 | | | | | | | | | % 23.27/3.90 | | | | | | | | | REDUCE: (126), (295) imply: % 23.27/3.90 | | | | | | | | | (296) mem(all_78_2, all_29_4) = 0 % 23.27/3.90 | | | | | | | | | % 23.27/3.90 | | | | | | | | | GROUND_INST: instantiating (3) with all_78_2, all_29_5, % 23.27/3.90 | | | | | | | | | all_29_4, simplifying with (21), (53), (84), (296) % 23.27/3.90 | | | | | | | | | gives: % 23.27/3.90 | | | | | | | | | (297) all_78_2 = all_29_5 % 23.27/3.90 | | | | | | | | | % 23.27/3.90 | | | | | | | | | REDUCE: (86), (297) imply: % 23.27/3.90 | | | | | | | | | (298) mem(all_29_5, all_52_1) = 0 % 23.27/3.90 | | | | | | | | | % 23.27/3.90 | | | | | | | | | GROUND_INST: instantiating (15) with all_89_0, 0, all_52_1, % 23.27/3.90 | | | | | | | | | all_29_5, simplifying with (246), (298) gives: % 23.27/3.90 | | | | | | | | | (299) all_89_0 = 0 % 23.27/3.90 | | | | | | | | | % 23.27/3.90 | | | | | | | | | REDUCE: (93), (299) imply: % 23.27/3.90 | | | | | | | | | (300) $false % 23.27/3.90 | | | | | | | | | % 23.27/3.90 | | | | | | | | | CLOSE: (300) is inconsistent. % 23.27/3.90 | | | | | | | | | % 23.27/3.90 | | | | | | | | End of split % 23.27/3.90 | | | | | | | | % 23.27/3.90 | | | | | | | End of split % 23.27/3.90 | | | | | | | % 23.27/3.90 | | | | | | Case 2: % 23.27/3.90 | | | | | | | % 23.27/3.90 | | | | | | | (301) all_76_1 = 0 % 23.27/3.90 | | | | | | | % 23.27/3.90 | | | | | | | REDUCE: (79), (301) imply: % 23.27/3.90 | | | | | | | (302) mem(all_58_1, all_29_4) = 0 % 23.27/3.90 | | | | | | | % 23.27/3.90 | | | | | | | GROUND_INST: instantiating (3) with all_58_1, all_29_5, all_29_4, % 23.27/3.90 | | | | | | | simplifying with (21), (53), (69), (302) gives: % 23.27/3.90 | | | | | | | (303) all_58_1 = all_29_5 % 23.27/3.90 | | | | | | | % 23.27/3.90 | | | | | | | REDUCE: (71), (303) imply: % 23.27/3.90 | | | | | | | (304) mem(all_29_5, all_37_1) = all_58_0 % 23.27/3.90 | | | | | | | % 23.27/3.90 | | | | | | | BETA: splitting (115) gives: % 23.27/3.90 | | | | | | | % 23.27/3.90 | | | | | | | Case 1: % 23.27/3.90 | | | | | | | | % 23.27/3.90 | | | | | | | | (305) all_123_0 = 0 % 23.27/3.90 | | | | | | | | % 23.27/3.90 | | | | | | | | REDUCE: (114), (305) imply: % 23.27/3.90 | | | | | | | | (306) mem(all_89_1, all_29_1) = 0 % 23.27/3.90 | | | | | | | | % 23.27/3.91 | | | | | | | | GROUND_INST: instantiating (4) with all_89_1, all_29_2, % 23.27/3.91 | | | | | | | | all_46_0, all_29_1, simplifying with (18), (49), % 23.27/3.91 | | | | | | | | (51), (94), (306) gives: % 23.27/3.91 | | | | | | | | (307) ? [v0: any] : ? [v1: any] : (mem(all_89_1, all_46_0) % 23.27/3.91 | | | | | | | | = v1 & mem(all_89_1, all_29_2) = v0 & (v1 = 0 | v0 = % 23.27/3.91 | | | | | | | | 0)) % 23.27/3.91 | | | | | | | | % 23.27/3.91 | | | | | | | | DELTA: instantiating (307) with fresh symbols all_183_0, % 23.27/3.91 | | | | | | | | all_183_1 gives: % 23.27/3.91 | | | | | | | | (308) mem(all_89_1, all_46_0) = all_183_0 & mem(all_89_1, % 23.27/3.91 | | | | | | | | all_29_2) = all_183_1 & (all_183_0 = 0 | all_183_1 = % 23.27/3.91 | | | | | | | | 0) % 23.27/3.91 | | | | | | | | % 23.27/3.91 | | | | | | | | ALPHA: (308) implies: % 23.27/3.91 | | | | | | | | (309) mem(all_89_1, all_29_2) = all_183_1 % 23.27/3.91 | | | | | | | | (310) mem(all_89_1, all_46_0) = all_183_0 % 23.27/3.91 | | | | | | | | (311) all_183_0 = 0 | all_183_1 = 0 % 23.27/3.91 | | | | | | | | % 23.27/3.91 | | | | | | | | BETA: splitting (128) gives: % 23.27/3.91 | | | | | | | | % 23.27/3.91 | | | | | | | | Case 1: % 23.27/3.91 | | | | | | | | | % 23.27/3.91 | | | | | | | | | (312) all_137_0 = 0 % 23.27/3.91 | | | | | | | | | % 23.27/3.91 | | | | | | | | | REDUCE: (127), (312) imply: % 23.27/3.91 | | | | | | | | | (313) mem(all_78_2, all_29_1) = 0 % 23.27/3.91 | | | | | | | | | % 23.27/3.91 | | | | | | | | | GROUND_INST: instantiating (4) with all_78_2, all_29_2, % 23.27/3.91 | | | | | | | | | all_46_0, all_29_1, simplifying with (18), (49), % 23.27/3.91 | | | | | | | | | (51), (84), (313) gives: % 23.27/3.91 | | | | | | | | | (314) ? [v0: any] : ? [v1: any] : (mem(all_78_2, % 23.27/3.91 | | | | | | | | | all_46_0) = v1 & mem(all_78_2, all_29_2) = v0 & % 23.27/3.91 | | | | | | | | | (v1 = 0 | v0 = 0)) % 23.27/3.91 | | | | | | | | | % 23.27/3.91 | | | | | | | | | DELTA: instantiating (314) with fresh symbols all_197_0, % 23.27/3.91 | | | | | | | | | all_197_1 gives: % 23.27/3.91 | | | | | | | | | (315) mem(all_78_2, all_46_0) = all_197_0 & mem(all_78_2, % 23.27/3.91 | | | | | | | | | all_29_2) = all_197_1 & (all_197_0 = 0 | all_197_1 % 23.27/3.91 | | | | | | | | | = 0) % 23.27/3.91 | | | | | | | | | % 23.27/3.91 | | | | | | | | | ALPHA: (315) implies: % 23.27/3.91 | | | | | | | | | (316) mem(all_78_2, all_29_2) = all_197_1 % 23.27/3.91 | | | | | | | | | (317) mem(all_78_2, all_46_0) = all_197_0 % 23.27/3.91 | | | | | | | | | (318) all_197_0 = 0 | all_197_1 = 0 % 23.27/3.91 | | | | | | | | | % 23.27/3.91 | | | | | | | | | BETA: splitting (141) gives: % 23.27/3.91 | | | | | | | | | % 23.27/3.91 | | | | | | | | | Case 1: % 23.27/3.91 | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | (319) all_150_0 = 0 % 23.27/3.91 | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | REDUCE: (140), (319) imply: % 23.27/3.91 | | | | | | | | | | (320) mem(all_110_1, all_29_1) = 0 % 23.27/3.91 | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | GROUND_INST: instantiating (4) with all_110_1, all_29_2, % 23.27/3.91 | | | | | | | | | | all_46_0, all_29_1, simplifying with (18), (49), % 23.27/3.91 | | | | | | | | | | (51), (105), (320) gives: % 23.27/3.91 | | | | | | | | | | (321) ? [v0: any] : ? [v1: any] : (mem(all_110_1, % 23.27/3.91 | | | | | | | | | | all_46_0) = v1 & mem(all_110_1, all_29_2) = v0 % 23.27/3.91 | | | | | | | | | | & (v1 = 0 | v0 = 0)) % 23.27/3.91 | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | DELTA: instantiating (321) with fresh symbols all_211_0, % 23.27/3.91 | | | | | | | | | | all_211_1 gives: % 23.27/3.91 | | | | | | | | | | (322) mem(all_110_1, all_46_0) = all_211_0 & % 23.27/3.91 | | | | | | | | | | mem(all_110_1, all_29_2) = all_211_1 & (all_211_0 = % 23.27/3.91 | | | | | | | | | | 0 | all_211_1 = 0) % 23.27/3.91 | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | ALPHA: (322) implies: % 23.27/3.91 | | | | | | | | | | (323) mem(all_110_1, all_29_2) = all_211_1 % 23.27/3.91 | | | | | | | | | | (324) mem(all_110_1, all_46_0) = all_211_0 % 23.27/3.91 | | | | | | | | | | (325) all_211_0 = 0 | all_211_1 = 0 % 23.27/3.91 | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | BETA: splitting (311) gives: % 23.27/3.91 | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | Case 1: % 23.27/3.91 | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | (326) all_183_0 = 0 % 23.27/3.91 | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | REDUCE: (310), (326) imply: % 23.27/3.91 | | | | | | | | | | | (327) mem(all_89_1, all_46_0) = 0 % 23.27/3.91 | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | GROUND_INST: instantiating (3) with all_89_1, all_29_2, % 23.27/3.91 | | | | | | | | | | | all_46_0, simplifying with (18), (50), (94), (327) % 23.27/3.91 | | | | | | | | | | | gives: % 23.27/3.91 | | | | | | | | | | | (328) all_89_1 = all_29_2 % 23.27/3.91 | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | REDUCE: (96), (328) imply: % 23.27/3.91 | | | | | | | | | | | (329) mem(all_29_2, all_52_1) = all_89_0 % 23.27/3.91 | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | BETA: splitting (318) gives: % 23.27/3.91 | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | Case 1: % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | (330) all_197_0 = 0 % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | REDUCE: (317), (330) imply: % 23.27/3.91 | | | | | | | | | | | | (331) mem(all_78_2, all_46_0) = 0 % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | REF_CLOSE: (3), (15), (18), (50), (84), (86), (93), (329), % 23.27/3.91 | | | | | | | | | | | | (331) are inconsistent by sub-proof #9. % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | Case 2: % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | (332) all_197_1 = 0 % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | REDUCE: (316), (332) imply: % 23.27/3.91 | | | | | | | | | | | | (333) mem(all_78_2, all_29_2) = 0 % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | GROUND_INST: instantiating (3) with all_78_2, all_29_3, % 23.27/3.91 | | | | | | | | | | | | all_29_2, simplifying with (22), (74), (84), (333) % 23.27/3.91 | | | | | | | | | | | | gives: % 23.27/3.91 | | | | | | | | | | | | (334) all_78_2 = all_29_3 % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | REDUCE: (135), (334) imply: % 23.27/3.91 | | | | | | | | | | | | (335) mem(all_143_1, all_29_3) = all_143_0 % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | BETA: splitting (325) gives: % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | Case 1: % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | | (336) all_211_0 = 0 % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | | REDUCE: (324), (336) imply: % 23.27/3.91 | | | | | | | | | | | | | (337) mem(all_110_1, all_46_0) = 0 % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | | REF_CLOSE: (3), (15), (18), (50), (93), (105), (106), (329), % 23.27/3.91 | | | | | | | | | | | | | (337) are inconsistent by sub-proof #4. % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | Case 2: % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | | (338) all_211_1 = 0 % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | | REDUCE: (323), (338) imply: % 23.27/3.91 | | | | | | | | | | | | | (339) mem(all_110_1, all_29_2) = 0 % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | | REF_CLOSE: (3), (15), (22), (74), (105), (133), (136), (335), % 23.27/3.91 | | | | | | | | | | | | | (339) are inconsistent by sub-proof #2. % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | End of split % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | End of split % 23.27/3.91 | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | Case 2: % 23.27/3.91 | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | (340) all_183_1 = 0 % 23.27/3.91 | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | REDUCE: (309), (340) imply: % 23.27/3.91 | | | | | | | | | | | (341) mem(all_89_1, all_29_2) = 0 % 23.27/3.91 | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | GROUND_INST: instantiating (3) with all_89_1, all_29_3, % 23.27/3.91 | | | | | | | | | | | all_29_2, simplifying with (22), (74), (94), (341) % 23.27/3.91 | | | | | | | | | | | gives: % 23.27/3.91 | | | | | | | | | | | (342) all_89_1 = all_29_3 % 23.27/3.91 | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | REDUCE: (96), (342) imply: % 23.27/3.91 | | | | | | | | | | | (343) mem(all_29_3, all_52_1) = all_89_0 % 23.27/3.91 | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | BETA: splitting (318) gives: % 23.27/3.91 | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | Case 1: % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | (344) all_197_0 = 0 % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | REDUCE: (317), (344) imply: % 23.27/3.91 | | | | | | | | | | | | (345) mem(all_78_2, all_46_0) = 0 % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | GROUND_INST: instantiating (3) with all_78_2, all_29_2, % 23.27/3.91 | | | | | | | | | | | | all_46_0, simplifying with (18), (50), (84), (345) % 23.27/3.91 | | | | | | | | | | | | gives: % 23.27/3.91 | | | | | | | | | | | | (346) all_78_2 = all_29_2 % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | REDUCE: (135), (346) imply: % 23.27/3.91 | | | | | | | | | | | | (347) mem(all_143_1, all_29_2) = all_143_0 % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | BETA: splitting (325) gives: % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | Case 1: % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | | (348) all_211_0 = 0 % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | | REDUCE: (324), (348) imply: % 23.27/3.91 | | | | | | | | | | | | | (349) mem(all_110_1, all_46_0) = 0 % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | | REF_CLOSE: (3), (15), (18), (50), (105), (133), (136), (347), % 23.27/3.91 | | | | | | | | | | | | | (349) are inconsistent by sub-proof #1. % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | Case 2: % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | | (350) all_211_1 = 0 % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | | REDUCE: (323), (350) imply: % 23.27/3.91 | | | | | | | | | | | | | (351) mem(all_110_1, all_29_2) = 0 % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | | REF_CLOSE: (3), (15), (22), (74), (93), (105), (106), (343), % 23.27/3.91 | | | | | | | | | | | | | (351) are inconsistent by sub-proof #5. % 23.27/3.91 | | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | End of split % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | Case 2: % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | (352) all_197_1 = 0 % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.91 | | | | | | | | | | | | REDUCE: (316), (352) imply: % 23.27/3.91 | | | | | | | | | | | | (353) mem(all_78_2, all_29_2) = 0 % 23.27/3.91 | | | | | | | | | | | | % 23.27/3.92 | | | | | | | | | | | | REF_CLOSE: (3), (15), (22), (74), (84), (86), (93), (343), % 23.27/3.92 | | | | | | | | | | | | (353) are inconsistent by sub-proof #10. % 23.27/3.92 | | | | | | | | | | | | % 23.27/3.92 | | | | | | | | | | | End of split % 23.27/3.92 | | | | | | | | | | | % 23.27/3.92 | | | | | | | | | | End of split % 23.27/3.92 | | | | | | | | | | % 23.27/3.92 | | | | | | | | | Case 2: % 23.27/3.92 | | | | | | | | | | % 23.27/3.92 | | | | | | | | | | (354) all_150_1 = 0 % 23.27/3.92 | | | | | | | | | | % 23.27/3.92 | | | | | | | | | | REDUCE: (139), (354) imply: % 23.27/3.92 | | | | | | | | | | (355) mem(all_110_1, all_29_4) = 0 % 23.27/3.92 | | | | | | | | | | % 23.27/3.92 | | | | | | | | | | GROUND_INST: instantiating (3) with all_110_1, all_29_5, % 23.27/3.92 | | | | | | | | | | all_29_4, simplifying with (21), (53), (105), % 23.27/3.92 | | | | | | | | | | (355) gives: % 23.27/3.92 | | | | | | | | | | (356) all_110_1 = all_29_5 % 23.27/3.92 | | | | | | | | | | % 23.27/3.92 | | | | | | | | | | REDUCE: (110), (356) imply: % 23.27/3.92 | | | | | | | | | | (357) mem(all_29_5, all_37_1) = 0 % 23.27/3.92 | | | | | | | | | | % 23.27/3.92 | | | | | | | | | | GROUND_INST: instantiating (15) with all_58_0, 0, all_37_1, % 23.27/3.92 | | | | | | | | | | all_29_5, simplifying with (304), (357) gives: % 23.27/3.92 | | | | | | | | | | (358) all_58_0 = 0 % 23.27/3.92 | | | | | | | | | | % 23.27/3.92 | | | | | | | | | | REDUCE: (68), (358) imply: % 23.27/3.92 | | | | | | | | | | (359) $false % 23.27/3.92 | | | | | | | | | | % 23.27/3.92 | | | | | | | | | | CLOSE: (359) is inconsistent. % 23.27/3.92 | | | | | | | | | | % 23.27/3.92 | | | | | | | | | End of split % 23.27/3.92 | | | | | | | | | % 23.27/3.92 | | | | | | | | Case 2: % 23.27/3.92 | | | | | | | | | % 23.27/3.92 | | | | | | | | | (360) all_137_1 = 0 % 23.27/3.92 | | | | | | | | | % 23.27/3.92 | | | | | | | | | REDUCE: (126), (360) imply: % 23.27/3.92 | | | | | | | | | (361) mem(all_78_2, all_29_4) = 0 % 23.27/3.92 | | | | | | | | | % 23.27/3.92 | | | | | | | | | GROUND_INST: instantiating (3) with all_78_2, all_29_5, % 23.27/3.92 | | | | | | | | | all_29_4, simplifying with (21), (53), (84), (361) % 23.27/3.92 | | | | | | | | | gives: % 23.27/3.92 | | | | | | | | | (362) all_78_2 = all_29_5 % 23.27/3.92 | | | | | | | | | % 23.27/3.92 | | | | | | | | | REDUCE: (97), (362) imply: % 23.27/3.92 | | | | | | | | | (363) mem(all_29_5, all_37_1) = 0 % 23.27/3.92 | | | | | | | | | % 23.27/3.92 | | | | | | | | | GROUND_INST: instantiating (15) with all_58_0, 0, all_37_1, % 23.27/3.92 | | | | | | | | | all_29_5, simplifying with (304), (363) gives: % 23.27/3.92 | | | | | | | | | (364) all_58_0 = 0 % 23.27/3.92 | | | | | | | | | % 23.27/3.92 | | | | | | | | | REDUCE: (68), (364) imply: % 23.27/3.92 | | | | | | | | | (365) $false % 23.27/3.92 | | | | | | | | | % 23.27/3.92 | | | | | | | | | CLOSE: (365) is inconsistent. % 23.27/3.92 | | | | | | | | | % 23.27/3.92 | | | | | | | | End of split % 23.27/3.92 | | | | | | | | % 23.27/3.92 | | | | | | | Case 2: % 23.27/3.92 | | | | | | | | % 23.27/3.92 | | | | | | | | (366) all_123_1 = 0 % 23.27/3.92 | | | | | | | | % 23.27/3.92 | | | | | | | | REDUCE: (113), (366) imply: % 23.27/3.92 | | | | | | | | (367) mem(all_89_1, all_29_4) = 0 % 23.27/3.92 | | | | | | | | % 23.27/3.92 | | | | | | | | GROUND_INST: instantiating (3) with all_89_1, all_29_5, % 23.27/3.92 | | | | | | | | all_29_4, simplifying with (21), (53), (94), (367) % 23.27/3.92 | | | | | | | | gives: % 23.27/3.92 | | | | | | | | (368) all_89_1 = all_29_5 % 23.27/3.92 | | | | | | | | % 23.27/3.92 | | | | | | | | REDUCE: (95), (368) imply: % 23.27/3.92 | | | | | | | | (369) mem(all_29_5, all_37_1) = 0 % 23.27/3.92 | | | | | | | | % 23.27/3.92 | | | | | | | | GROUND_INST: instantiating (15) with all_58_0, 0, all_37_1, % 23.27/3.92 | | | | | | | | all_29_5, simplifying with (304), (369) gives: % 23.27/3.92 | | | | | | | | (370) all_58_0 = 0 % 23.27/3.92 | | | | | | | | % 23.27/3.92 | | | | | | | | REDUCE: (68), (370) imply: % 23.27/3.92 | | | | | | | | (371) $false % 23.27/3.92 | | | | | | | | % 23.27/3.92 | | | | | | | | CLOSE: (371) is inconsistent. % 23.27/3.92 | | | | | | | | % 23.27/3.92 | | | | | | | End of split % 23.27/3.92 | | | | | | | % 23.27/3.92 | | | | | | End of split % 23.27/3.92 | | | | | | % 23.27/3.92 | | | | | End of split % 23.27/3.92 | | | | | % 23.27/3.92 | | | | End of split % 23.27/3.92 | | | | % 23.27/3.92 | | | End of split % 23.27/3.92 | | | % 23.27/3.92 | | End of split % 23.27/3.92 | | % 23.27/3.92 | End of split % 23.27/3.92 | % 23.27/3.92 End of proof % 23.27/3.92 % 23.27/3.92 Sub-proof #1 shows that the following formulas are inconsistent: % 23.27/3.92 ---------------------------------------------------------------- % 23.27/3.92 (1) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.27/3.92 ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 23.27/3.92 (2) ~ (all_143_0 = 0) % 23.27/3.92 (3) mem(all_143_1, all_110_1) = 0 % 23.27/3.92 (4) s(all_29_2) = all_46_0 % 23.27/3.92 (5) $i(all_29_2) % 23.27/3.92 (6) $i(all_110_1) % 23.27/3.92 (7) mem(all_143_1, all_29_2) = all_143_0 % 23.27/3.92 (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | ~ % 23.27/3.92 (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 23.27/3.92 (9) mem(all_110_1, all_46_0) = 0 % 23.27/3.92 % 23.27/3.92 Begin of proof % 23.27/3.92 | % 23.27/3.92 | GROUND_INST: instantiating (8) with all_110_1, all_29_2, all_46_0, simplifying % 23.27/3.92 | with (4), (5), (6), (9) gives: % 23.27/3.92 | (10) all_110_1 = all_29_2 % 23.27/3.92 | % 23.27/3.92 | REDUCE: (3), (10) imply: % 23.27/3.92 | (11) mem(all_143_1, all_29_2) = 0 % 23.27/3.92 | % 23.27/3.92 | GROUND_INST: instantiating (1) with all_143_0, 0, all_29_2, all_143_1, % 23.27/3.92 | simplifying with (7), (11) gives: % 23.27/3.92 | (12) all_143_0 = 0 % 23.27/3.92 | % 23.27/3.92 | REDUCE: (2), (12) imply: % 23.27/3.92 | (13) $false % 23.27/3.92 | % 23.27/3.92 | CLOSE: (13) is inconsistent. % 23.27/3.92 | % 23.27/3.92 End of proof % 23.27/3.92 % 23.27/3.92 Sub-proof #2 shows that the following formulas are inconsistent: % 23.27/3.92 ---------------------------------------------------------------- % 23.27/3.92 (1) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.27/3.92 ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 23.27/3.92 (2) ~ (all_143_0 = 0) % 23.27/3.92 (3) mem(all_110_1, all_29_2) = 0 % 23.27/3.92 (4) mem(all_143_1, all_110_1) = 0 % 23.27/3.92 (5) s(all_29_3) = all_29_2 % 23.27/3.92 (6) $i(all_110_1) % 23.27/3.92 (7) mem(all_143_1, all_29_3) = all_143_0 % 23.27/3.92 (8) $i(all_29_3) % 23.27/3.92 (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | ~ % 23.27/3.92 (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 23.27/3.92 % 23.27/3.92 Begin of proof % 23.27/3.92 | % 23.27/3.92 | GROUND_INST: instantiating (9) with all_110_1, all_29_3, all_29_2, simplifying % 23.27/3.92 | with (3), (5), (6), (8) gives: % 23.27/3.92 | (10) all_110_1 = all_29_3 % 23.27/3.92 | % 23.27/3.92 | REDUCE: (4), (10) imply: % 23.27/3.92 | (11) mem(all_143_1, all_29_3) = 0 % 23.27/3.92 | % 23.27/3.92 | GROUND_INST: instantiating (1) with all_143_0, 0, all_29_3, all_143_1, % 23.27/3.92 | simplifying with (7), (11) gives: % 23.27/3.92 | (12) all_143_0 = 0 % 23.27/3.92 | % 23.27/3.92 | REDUCE: (2), (12) imply: % 23.27/3.92 | (13) $false % 23.27/3.92 | % 23.27/3.92 | CLOSE: (13) is inconsistent. % 23.27/3.92 | % 23.27/3.92 End of proof % 23.27/3.92 % 23.27/3.92 Sub-proof #3 shows that the following formulas are inconsistent: % 23.27/3.92 ---------------------------------------------------------------- % 23.27/3.92 (1) mem(all_110_1, all_37_1) = 0 % 23.27/3.92 (2) mem(all_29_3, all_37_1) = all_58_0 % 23.27/3.92 (3) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.27/3.92 ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 23.27/3.92 (4) mem(all_110_1, all_29_2) = 0 % 23.27/3.92 (5) ~ (all_58_0 = 0) % 23.27/3.92 (6) s(all_29_3) = all_29_2 % 23.27/3.92 (7) $i(all_110_1) % 23.27/3.92 (8) $i(all_29_3) % 23.27/3.92 (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | ~ % 23.27/3.92 (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 23.27/3.92 % 23.27/3.92 Begin of proof % 23.27/3.92 | % 23.27/3.93 | GROUND_INST: instantiating (9) with all_110_1, all_29_3, all_29_2, simplifying % 23.27/3.93 | with (4), (6), (7), (8) gives: % 23.27/3.93 | (10) all_110_1 = all_29_3 % 23.27/3.93 | % 23.27/3.93 | REDUCE: (1), (10) imply: % 23.27/3.93 | (11) mem(all_29_3, all_37_1) = 0 % 23.27/3.93 | % 23.27/3.93 | GROUND_INST: instantiating (3) with all_58_0, 0, all_37_1, all_29_3, % 23.27/3.93 | simplifying with (2), (11) gives: % 23.27/3.93 | (12) all_58_0 = 0 % 23.27/3.93 | % 23.27/3.93 | REDUCE: (5), (12) imply: % 23.27/3.93 | (13) $false % 23.27/3.93 | % 23.27/3.93 | CLOSE: (13) is inconsistent. % 23.27/3.93 | % 23.27/3.93 End of proof % 23.27/3.93 % 23.27/3.93 Sub-proof #4 shows that the following formulas are inconsistent: % 23.27/3.93 ---------------------------------------------------------------- % 23.27/3.93 (1) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.27/3.93 ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 23.27/3.93 (2) mem(all_29_2, all_52_1) = all_89_0 % 23.27/3.93 (3) s(all_29_2) = all_46_0 % 23.27/3.93 (4) ~ (all_89_0 = 0) % 23.27/3.93 (5) $i(all_29_2) % 23.27/3.93 (6) mem(all_110_1, all_52_1) = 0 % 23.27/3.93 (7) $i(all_110_1) % 23.27/3.93 (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | ~ % 23.27/3.93 (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 23.27/3.93 (9) mem(all_110_1, all_46_0) = 0 % 23.27/3.93 % 23.27/3.93 Begin of proof % 23.27/3.93 | % 23.27/3.93 | GROUND_INST: instantiating (8) with all_110_1, all_29_2, all_46_0, simplifying % 23.27/3.93 | with (3), (5), (7), (9) gives: % 23.27/3.93 | (10) all_110_1 = all_29_2 % 23.27/3.93 | % 23.27/3.93 | REDUCE: (6), (10) imply: % 23.27/3.93 | (11) mem(all_29_2, all_52_1) = 0 % 23.27/3.93 | % 23.27/3.93 | GROUND_INST: instantiating (1) with all_89_0, 0, all_52_1, all_29_2, % 23.27/3.93 | simplifying with (2), (11) gives: % 23.27/3.93 | (12) all_89_0 = 0 % 23.27/3.93 | % 23.27/3.93 | REDUCE: (4), (12) imply: % 23.27/3.93 | (13) $false % 23.27/3.93 | % 23.27/3.93 | CLOSE: (13) is inconsistent. % 23.27/3.93 | % 23.27/3.93 End of proof % 23.27/3.93 % 23.27/3.93 Sub-proof #5 shows that the following formulas are inconsistent: % 23.27/3.93 ---------------------------------------------------------------- % 23.27/3.93 (1) mem(all_29_3, all_52_1) = all_89_0 % 23.27/3.93 (2) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.27/3.93 ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 23.27/3.93 (3) mem(all_110_1, all_29_2) = 0 % 23.27/3.93 (4) ~ (all_89_0 = 0) % 23.27/3.93 (5) s(all_29_3) = all_29_2 % 23.27/3.93 (6) mem(all_110_1, all_52_1) = 0 % 23.27/3.93 (7) $i(all_110_1) % 23.27/3.93 (8) $i(all_29_3) % 23.27/3.93 (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | ~ % 23.27/3.93 (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 23.27/3.93 % 23.27/3.93 Begin of proof % 23.27/3.93 | % 23.27/3.93 | GROUND_INST: instantiating (9) with all_110_1, all_29_3, all_29_2, simplifying % 23.27/3.93 | with (3), (5), (7), (8) gives: % 23.27/3.93 | (10) all_110_1 = all_29_3 % 23.27/3.93 | % 23.27/3.93 | REDUCE: (6), (10) imply: % 23.27/3.93 | (11) mem(all_29_3, all_52_1) = 0 % 23.27/3.93 | % 23.27/3.93 | GROUND_INST: instantiating (2) with all_89_0, 0, all_52_1, all_29_3, % 23.27/3.93 | simplifying with (1), (11) gives: % 23.27/3.93 | (12) all_89_0 = 0 % 23.27/3.93 | % 23.27/3.93 | REDUCE: (4), (12) imply: % 23.27/3.93 | (13) $false % 23.27/3.93 | % 23.27/3.93 | CLOSE: (13) is inconsistent. % 23.27/3.93 | % 23.27/3.93 End of proof % 23.27/3.93 % 23.27/3.93 Sub-proof #6 shows that the following formulas are inconsistent: % 23.27/3.93 ---------------------------------------------------------------- % 23.27/3.93 (1) mem(all_110_1, all_37_1) = 0 % 23.27/3.93 (2) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.27/3.93 ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 23.27/3.93 (3) mem(all_29_2, all_37_1) = all_58_0 % 23.27/3.93 (4) s(all_29_2) = all_46_0 % 23.27/3.93 (5) ~ (all_58_0 = 0) % 23.27/3.93 (6) $i(all_29_2) % 23.27/3.93 (7) $i(all_110_1) % 23.27/3.93 (8) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | ~ % 23.27/3.93 (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 23.27/3.93 (9) mem(all_110_1, all_46_0) = 0 % 23.27/3.93 % 23.27/3.93 Begin of proof % 23.27/3.93 | % 23.27/3.93 | GROUND_INST: instantiating (8) with all_110_1, all_29_2, all_46_0, simplifying % 23.27/3.93 | with (4), (6), (7), (9) gives: % 23.27/3.93 | (10) all_110_1 = all_29_2 % 23.27/3.93 | % 23.27/3.93 | REDUCE: (1), (10) imply: % 23.27/3.93 | (11) mem(all_29_2, all_37_1) = 0 % 23.27/3.93 | % 23.27/3.93 | GROUND_INST: instantiating (2) with all_58_0, 0, all_37_1, all_29_2, % 23.27/3.93 | simplifying with (3), (11) gives: % 23.27/3.93 | (12) all_58_0 = 0 % 23.27/3.93 | % 23.27/3.93 | REDUCE: (5), (12) imply: % 23.27/3.93 | (13) $false % 23.27/3.93 | % 23.27/3.93 | CLOSE: (13) is inconsistent. % 23.27/3.93 | % 23.27/3.93 End of proof % 23.27/3.93 % 23.27/3.93 Sub-proof #7 shows that the following formulas are inconsistent: % 23.27/3.93 ---------------------------------------------------------------- % 23.27/3.93 (1) mem(all_89_1, all_29_2) = 0 % 23.27/3.93 (2) mem(all_29_3, all_37_1) = all_58_0 % 23.27/3.93 (3) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.27/3.93 ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 23.27/3.93 (4) mem(all_89_1, all_37_1) = 0 % 23.27/3.93 (5) $i(all_89_1) % 23.27/3.93 (6) ~ (all_58_0 = 0) % 23.27/3.93 (7) s(all_29_3) = all_29_2 % 23.27/3.93 (8) $i(all_29_3) % 23.27/3.93 (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | ~ % 23.27/3.93 (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 23.27/3.93 % 23.27/3.93 Begin of proof % 23.27/3.93 | % 23.27/3.93 | GROUND_INST: instantiating (9) with all_89_1, all_29_3, all_29_2, simplifying % 23.27/3.93 | with (1), (5), (7), (8) gives: % 23.27/3.93 | (10) all_89_1 = all_29_3 % 23.27/3.93 | % 23.27/3.93 | REDUCE: (4), (10) imply: % 23.27/3.93 | (11) mem(all_29_3, all_37_1) = 0 % 23.27/3.93 | % 23.27/3.93 | GROUND_INST: instantiating (3) with all_58_0, 0, all_37_1, all_29_3, % 23.27/3.93 | simplifying with (2), (11) gives: % 23.27/3.93 | (12) all_58_0 = 0 % 23.27/3.93 | % 23.27/3.93 | REDUCE: (6), (12) imply: % 23.27/3.93 | (13) $false % 23.27/3.93 | % 23.27/3.93 | CLOSE: (13) is inconsistent. % 23.27/3.93 | % 23.27/3.93 End of proof % 23.27/3.93 % 23.27/3.93 Sub-proof #8 shows that the following formulas are inconsistent: % 23.27/3.93 ---------------------------------------------------------------- % 23.27/3.93 (1) $i(all_78_2) % 23.27/3.93 (2) mem(all_29_3, all_37_1) = all_58_0 % 23.27/3.93 (3) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.27/3.93 ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 23.27/3.93 (4) mem(all_78_2, all_29_2) = 0 % 23.27/3.93 (5) ~ (all_58_0 = 0) % 23.27/3.93 (6) s(all_29_3) = all_29_2 % 23.27/3.93 (7) mem(all_78_2, all_37_1) = 0 % 23.27/3.93 (8) $i(all_29_3) % 23.27/3.93 (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | ~ % 23.27/3.93 (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 23.27/3.93 % 23.27/3.93 Begin of proof % 23.27/3.93 | % 23.27/3.93 | GROUND_INST: instantiating (9) with all_78_2, all_29_3, all_29_2, simplifying % 23.27/3.93 | with (1), (4), (6), (8) gives: % 23.27/3.93 | (10) all_78_2 = all_29_3 % 23.27/3.93 | % 23.27/3.93 | REDUCE: (7), (10) imply: % 23.27/3.93 | (11) mem(all_29_3, all_37_1) = 0 % 23.27/3.93 | % 23.27/3.93 | GROUND_INST: instantiating (3) with all_58_0, 0, all_37_1, all_29_3, % 23.27/3.93 | simplifying with (2), (11) gives: % 23.27/3.93 | (12) all_58_0 = 0 % 23.27/3.93 | % 23.27/3.93 | REDUCE: (5), (12) imply: % 23.27/3.93 | (13) $false % 23.27/3.93 | % 23.27/3.93 | CLOSE: (13) is inconsistent. % 23.27/3.93 | % 23.27/3.93 End of proof % 23.27/3.93 % 23.27/3.93 Sub-proof #9 shows that the following formulas are inconsistent: % 23.27/3.93 ---------------------------------------------------------------- % 23.27/3.93 (1) $i(all_78_2) % 23.27/3.93 (2) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.27/3.93 ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 23.27/3.93 (3) mem(all_29_2, all_52_1) = all_89_0 % 23.27/3.93 (4) mem(all_78_2, all_46_0) = 0 % 23.27/3.93 (5) s(all_29_2) = all_46_0 % 23.27/3.93 (6) mem(all_78_2, all_52_1) = 0 % 23.27/3.93 (7) ~ (all_89_0 = 0) % 23.27/3.93 (8) $i(all_29_2) % 23.27/3.94 (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | ~ % 23.27/3.94 (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 23.27/3.94 % 23.27/3.94 Begin of proof % 23.27/3.94 | % 23.27/3.94 | GROUND_INST: instantiating (9) with all_78_2, all_29_2, all_46_0, simplifying % 23.27/3.94 | with (1), (4), (5), (8) gives: % 23.27/3.94 | (10) all_78_2 = all_29_2 % 23.27/3.94 | % 23.27/3.94 | REDUCE: (6), (10) imply: % 23.27/3.94 | (11) mem(all_29_2, all_52_1) = 0 % 23.27/3.94 | % 23.27/3.94 | GROUND_INST: instantiating (2) with all_89_0, 0, all_52_1, all_29_2, % 23.27/3.94 | simplifying with (3), (11) gives: % 23.27/3.94 | (12) all_89_0 = 0 % 23.27/3.94 | % 23.27/3.94 | REDUCE: (7), (12) imply: % 23.27/3.94 | (13) $false % 23.27/3.94 | % 23.27/3.94 | CLOSE: (13) is inconsistent. % 23.27/3.94 | % 23.27/3.94 End of proof % 23.27/3.94 % 23.27/3.94 Sub-proof #10 shows that the following formulas are inconsistent: % 23.27/3.94 ---------------------------------------------------------------- % 23.27/3.94 (1) $i(all_78_2) % 23.27/3.94 (2) mem(all_29_3, all_52_1) = all_89_0 % 23.27/3.94 (3) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.27/3.94 ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 23.27/3.94 (4) mem(all_78_2, all_29_2) = 0 % 23.27/3.94 (5) mem(all_78_2, all_52_1) = 0 % 23.27/3.94 (6) ~ (all_89_0 = 0) % 23.27/3.94 (7) s(all_29_3) = all_29_2 % 23.27/3.94 (8) $i(all_29_3) % 23.27/3.94 (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | ~ % 23.27/3.94 (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 23.27/3.94 % 23.27/3.94 Begin of proof % 23.27/3.94 | % 23.27/3.94 | GROUND_INST: instantiating (9) with all_78_2, all_29_3, all_29_2, simplifying % 23.27/3.94 | with (1), (4), (7), (8) gives: % 23.27/3.94 | (10) all_78_2 = all_29_3 % 23.27/3.94 | % 23.27/3.94 | REDUCE: (5), (10) imply: % 23.27/3.94 | (11) mem(all_29_3, all_52_1) = 0 % 23.27/3.94 | % 23.27/3.94 | GROUND_INST: instantiating (3) with all_89_0, 0, all_52_1, all_29_3, % 23.27/3.94 | simplifying with (2), (11) gives: % 23.27/3.94 | (12) all_89_0 = 0 % 23.27/3.94 | % 23.27/3.94 | REDUCE: (6), (12) imply: % 23.27/3.94 | (13) $false % 23.27/3.94 | % 23.27/3.94 | CLOSE: (13) is inconsistent. % 23.27/3.94 | % 23.27/3.94 End of proof % 23.27/3.94 % 23.27/3.94 Sub-proof #11 shows that the following formulas are inconsistent: % 23.27/3.94 ---------------------------------------------------------------- % 23.27/3.94 (1) $i(all_78_2) % 23.27/3.94 (2) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.27/3.94 ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 23.27/3.94 (3) mem(all_29_2, all_37_1) = all_58_0 % 23.27/3.94 (4) mem(all_78_2, all_46_0) = 0 % 23.27/3.94 (5) s(all_29_2) = all_46_0 % 23.27/3.94 (6) ~ (all_58_0 = 0) % 23.27/3.94 (7) $i(all_29_2) % 23.27/3.94 (8) mem(all_78_2, all_37_1) = 0 % 23.27/3.94 (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | ~ % 23.27/3.94 (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 23.27/3.94 % 23.27/3.94 Begin of proof % 23.27/3.94 | % 23.27/3.94 | GROUND_INST: instantiating (9) with all_78_2, all_29_2, all_46_0, simplifying % 23.27/3.94 | with (1), (4), (5), (7) gives: % 23.27/3.94 | (10) all_78_2 = all_29_2 % 23.27/3.94 | % 23.27/3.94 | REDUCE: (8), (10) imply: % 23.27/3.94 | (11) mem(all_29_2, all_37_1) = 0 % 23.27/3.94 | % 23.27/3.94 | GROUND_INST: instantiating (2) with all_58_0, 0, all_37_1, all_29_2, % 23.27/3.94 | simplifying with (3), (11) gives: % 23.27/3.94 | (12) all_58_0 = 0 % 23.27/3.94 | % 23.27/3.94 | REDUCE: (6), (12) imply: % 23.27/3.94 | (13) $false % 23.27/3.94 | % 23.27/3.94 | CLOSE: (13) is inconsistent. % 23.27/3.94 | % 23.27/3.94 End of proof % 23.27/3.94 % 23.27/3.94 Sub-proof #12 shows that the following formulas are inconsistent: % 23.27/3.94 ---------------------------------------------------------------- % 23.27/3.94 (1) mem(all_89_1, all_46_0) = 0 % 23.27/3.94 (2) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 23.27/3.94 ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = v0)) % 23.27/3.94 (3) mem(all_29_2, all_37_1) = all_58_0 % 23.27/3.94 (4) mem(all_89_1, all_37_1) = 0 % 23.27/3.94 (5) s(all_29_2) = all_46_0 % 23.27/3.94 (6) $i(all_89_1) % 23.27/3.94 (7) ~ (all_58_0 = 0) % 23.27/3.94 (8) $i(all_29_2) % 23.27/3.94 (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | ~ % 23.27/3.94 (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 23.27/3.94 % 23.27/3.94 Begin of proof % 23.27/3.94 | % 23.27/3.94 | GROUND_INST: instantiating (9) with all_89_1, all_29_2, all_46_0, simplifying % 23.27/3.94 | with (1), (5), (6), (8) gives: % 23.27/3.94 | (10) all_89_1 = all_29_2 % 23.27/3.94 | % 23.27/3.94 | REDUCE: (4), (10) imply: % 23.27/3.94 | (11) mem(all_29_2, all_37_1) = 0 % 23.27/3.94 | % 23.27/3.94 | GROUND_INST: instantiating (2) with all_58_0, 0, all_37_1, all_29_2, % 23.27/3.94 | simplifying with (3), (11) gives: % 23.27/3.94 | (12) all_58_0 = 0 % 23.27/3.94 | % 23.27/3.94 | REDUCE: (7), (12) imply: % 23.27/3.94 | (13) $false % 23.27/3.94 | % 23.27/3.94 | CLOSE: (13) is inconsistent. % 23.27/3.94 | % 23.27/3.94 End of proof % 23.27/3.94 % SZS output end Proof for theBenchmark % 23.27/3.94 % 23.27/3.94 3337ms %------------------------------------------------------------------------------