%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SEV581+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 : n014.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:57 AM UTC 2025 % Result : Theorem 14.59s 2.73s % Output : Proof 17.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.11 % Problem : SEV581+1 : TPTP v9.1.0. Released v9.1.0. % 0.09/0.11 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.09/0.31 % Computer : n014.cluster.edu % 0.09/0.31 % Model : x86_64 x86_64 % 0.09/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.31 % Memory : 8042.1875MB % 0.09/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.31 % CPULimit : 300 % 0.09/0.31 % WCLimit : 300 % 0.09/0.31 % DateTime : Mon Mar 31 13:14:49 EDT 2025 % 0.09/0.31 % CPUTime : % 0.59/0.62 ________ _____ % 0.59/0.62 ___ __ \_________(_)________________________________ % 0.59/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.59/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.59/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.59/0.62 % 0.59/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.59/0.62 (2023-06-19) % 0.59/0.62 % 0.59/0.62 (c) Philipp Rümmer, 2009-2023 % 0.59/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.59/0.62 Amanda Stjerna. % 0.59/0.62 Free software under BSD-3-Clause. % 0.59/0.62 % 0.59/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.59/0.62 % 0.59/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.64/0.63 Running up to 7 provers in parallel. % 0.64/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.64/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.64/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.64/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.64/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.64/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.64/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.72/1.14 Prover 4: Preprocessing ... % 2.72/1.14 Prover 1: Preprocessing ... % 3.40/1.19 Prover 6: Preprocessing ... % 3.40/1.19 Prover 2: Preprocessing ... % 3.40/1.19 Prover 5: Preprocessing ... % 3.40/1.19 Prover 0: Preprocessing ... % 3.40/1.21 Prover 3: Preprocessing ... % 7.19/1.74 Prover 5: Proving ... % 7.19/1.76 Prover 2: Proving ... % 8.67/1.95 Prover 6: Proving ... % 9.16/2.02 Prover 1: Constructing countermodel ... % 9.16/2.03 Prover 3: Constructing countermodel ... % 10.03/2.11 Prover 4: Constructing countermodel ... % 10.19/2.16 Prover 0: Proving ... % 11.45/2.30 Prover 3: gave up % 11.45/2.34 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 11.45/2.35 Prover 1: gave up % 11.45/2.35 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 12.24/2.41 Prover 7: Preprocessing ... % 12.31/2.46 Prover 8: Preprocessing ... % 13.00/2.55 Prover 6: gave up % 13.00/2.56 Prover 7: Warning: ignoring some quantifiers % 13.00/2.56 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 13.00/2.57 Prover 7: Constructing countermodel ... % 13.63/2.61 Prover 9: Preprocessing ... % 14.59/2.72 Prover 0: proved (2084ms) % 14.59/2.72 % 14.59/2.73 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 14.59/2.73 % 14.59/2.74 Prover 2: stopped % 14.59/2.75 Prover 5: stopped % 14.59/2.76 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 14.59/2.76 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 14.59/2.76 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 14.59/2.80 Prover 10: Preprocessing ... % 15.26/2.82 Prover 8: Warning: ignoring some quantifiers % 15.26/2.82 Prover 13: Preprocessing ... % 15.26/2.85 Prover 8: Constructing countermodel ... % 15.26/2.87 Prover 11: Preprocessing ... % 15.26/2.89 Prover 10: Warning: ignoring some quantifiers % 15.98/2.91 Prover 10: Constructing countermodel ... % 15.98/2.96 Prover 9: Constructing countermodel ... % 15.98/2.97 Prover 13: Warning: ignoring some quantifiers % 15.98/2.99 Prover 4: Found proof (size 155) % 15.98/2.99 Prover 4: proved (2342ms) % 15.98/2.99 Prover 13: Constructing countermodel ... % 15.98/2.99 Prover 11: stopped % 15.98/2.99 Prover 10: stopped % 15.98/2.99 Prover 8: stopped % 15.98/2.99 Prover 9: stopped % 15.98/3.00 Prover 7: stopped % 16.73/3.00 Prover 13: stopped % 16.73/3.00 % 16.73/3.00 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.73/3.00 % 16.78/3.04 % SZS output start Proof for theBenchmark % 16.78/3.04 Assumptions after simplification: % 16.78/3.04 --------------------------------- % 16.78/3.04 % 16.78/3.04 (a_def) % 16.78/3.08 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (u(v0, v2) = v3) | % 16.78/3.08 ~ (s(v1) = v2) | ~ $i(v1) | ~ $i(v0) | (a(v0, v1) = v3 & $i(v3))) & ! % 16.78/3.08 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (a(v0, v1) = v2) | ~ $i(v1) | ~ % 16.78/3.08 $i(v0) | ? [v3: $i] : (u(v0, v3) = v2 & s(v1) = v3 & $i(v3) & $i(v2))) % 16.78/3.08 % 16.78/3.09 (n_def) % 16.78/3.09 ! [v0: $i] : ! [v1: $i] : ( ~ (n(v0) = v1) | ~ $i(v0) | (a(v0, v0) = v1 & % 16.78/3.09 $i(v1))) & ! [v0: $i] : ! [v1: $i] : ( ~ (a(v0, v0) = v1) | ~ $i(v0) | % 16.78/3.09 (n(v0) = v1 & $i(v1))) % 16.78/3.09 % 16.78/3.09 (p_ax) % 16.78/3.10 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ (p(v1) = % 16.78/3.10 v2) | ~ (mem(v0, v2) = v3) | ~ $i(v1) | ~ $i(v0) | ? [v4: int] : ( ~ % 16.78/3.10 (v4 = 0) & subq(v0, v1) = v4)) & ! [v0: $i] : ! [v1: $i] : ! [v2: int] % 16.78/3.10 : (v2 = 0 | ~ (subq(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? % 16.78/3.10 [v4: int] : ( ~ (v4 = 0) & p(v1) = v3 & mem(v0, v3) = v4 & $i(v3))) & ! % 16.78/3.10 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (p(v1) = v2) | ~ (mem(v0, v2) = 0) % 16.78/3.10 | ~ $i(v1) | ~ $i(v0) | subq(v0, v1) = 0) & ! [v0: $i] : ! [v1: $i] : ( % 16.78/3.10 ~ (subq(v0, v1) = 0) | ~ $i(v1) | ~ $i(v0) | ? [v2: $i] : (p(v1) = v2 & % 16.78/3.10 mem(v0, v2) = 0 & $i(v2))) % 16.78/3.10 % 16.78/3.10 (s_ax) % 16.78/3.10 ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (s(v0) = v1) | ~ % 16.78/3.10 (mem(v0, v1) = v2) | ~ $i(v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 16.78/3.10 (v1 = v0 | ~ (s(v1) = v2) | ~ (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 16.78/3.10 % 16.78/3.10 (subq_342_343) % 17.25/3.11 $i(e) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 17.25/3.11 ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? [v10: % 17.25/3.11 $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: int] : ( ~ (v13 = 0) & p(v4) = % 17.25/3.11 v10 & n(v4) = v5 & n(v1) = v4 & n(v0) = v6 & n(e) = v0 & a(v10, v7) = v11 & % 17.25/3.11 a(v5, v7) = v8 & u(v3, v8) = v9 & u(v1, v11) = v12 & s(v6) = v7 & s(v2) = v3 % 17.25/3.11 & s(v1) = v2 & s(v0) = v1 & subq(v9, v12) = v13 & $i(v12) & $i(v11) & % 17.25/3.11 $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & % 17.25/3.11 $i(v2) & $i(v1) & $i(v0)) % 17.25/3.11 % 17.25/3.11 (subq_def) % 17.25/3.11 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 17.25/3.11 (subq(v0, v1) = 0) | ~ (mem(v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 17.25/3.11 $i(v0) | ? [v4: int] : ( ~ (v4 = 0) & mem(v2, v0) = v4)) & ! [v0: $i] : ! % 17.25/3.11 [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (subq(v0, v1) = v2) | ~ $i(v1) | ~ % 17.25/3.11 $i(v0) | ? [v3: $i] : ? [v4: int] : ( ~ (v4 = 0) & mem(v3, v1) = v4 & % 17.25/3.11 mem(v3, v0) = 0 & $i(v3))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 17.25/3.11 (subq(v0, v1) = 0) | ~ (mem(v2, v0) = 0) | ~ $i(v2) | ~ $i(v1) | ~ % 17.25/3.11 $i(v0) | mem(v2, v1) = 0) % 17.25/3.11 % 17.25/3.11 (u_ax) % 17.25/3.12 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 17.25/3.12 | ~ (u(v1, v2) = v3) | ~ (mem(v0, v3) = v4) | ~ $i(v2) | ~ $i(v1) | ~ % 17.25/3.12 $i(v0) | ? [v5: int] : ? [v6: int] : ( ~ (v6 = 0) & ~ (v5 = 0) & mem(v0, % 17.25/3.12 v2) = v6 & mem(v0, v1) = v5)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 17.25/3.12 : ! [v3: $i] : ( ~ (u(v1, v2) = v3) | ~ (mem(v0, v3) = 0) | ~ $i(v2) | ~ % 17.25/3.12 $i(v1) | ~ $i(v0) | ? [v4: any] : ? [v5: any] : (mem(v0, v2) = v5 & % 17.25/3.12 mem(v0, v1) = v4 & (v5 = 0 | v4 = 0))) % 17.25/3.12 % 17.25/3.12 (function-axioms) % 17.25/3.13 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (a(v3, % 17.25/3.13 v2) = v1) | ~ (a(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 17.25/3.13 $i] : ! [v3: $i] : (v1 = v0 | ~ (m(v3, v2) = v1) | ~ (m(v3, v2) = v0)) & % 17.25/3.13 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (u(v3, % 17.25/3.13 v2) = v1) | ~ (u(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (disj(v3, v2) % 17.25/3.13 = v1) | ~ (disj(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (subq(v3, v2) % 17.25/3.13 = v1) | ~ (subq(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) % 17.25/3.13 = v1) | ~ (mem(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast16p(v2) = v1) | ~ % 17.25/3.13 (atleast16p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast15p(v2) = v1) | ~ % 17.25/3.13 (atleast15p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast14p(v2) = v1) | ~ % 17.25/3.13 (atleast14p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast13p(v2) = v1) | ~ % 17.25/3.13 (atleast13p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast12p(v2) = v1) | ~ % 17.25/3.13 (atleast12p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast11p(v2) = v1) | ~ % 17.25/3.13 (atleast11p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast10p(v2) = v1) | ~ % 17.25/3.13 (atleast10p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast9p(v2) = v1) | ~ % 17.25/3.13 (atleast9p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast8p(v2) = v1) | ~ % 17.25/3.13 (atleast8p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast7p(v2) = v1) | ~ % 17.25/3.13 (atleast7p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast6p(v2) = v1) | ~ % 17.25/3.13 (atleast6p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast5p(v2) = v1) | ~ % 17.25/3.13 (atleast5p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast4p(v2) = v1) | ~ % 17.25/3.13 (atleast4p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast3p(v2) = v1) | ~ % 17.25/3.13 (atleast3p(v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 17.25/3.13 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (atleast2p(v2) = v1) | ~ % 17.25/3.13 (atleast2p(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | % 17.25/3.13 ~ (p(v2) = v1) | ~ (p(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] % 17.25/3.13 : (v1 = v0 | ~ (n(v2) = v1) | ~ (n(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : % 17.25/3.13 ! [v2: $i] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 17.25/3.13 % 17.25/3.13 Further assumptions not needed in the proof: % 17.25/3.13 -------------------------------------------- % 17.25/3.13 atleast10p_def, atleast11p_def, atleast12p_def, atleast13p_def, atleast14p_def, % 17.25/3.13 atleast15p_def, atleast16p_def, atleast2p_def, atleast3p_def, atleast4p_def, % 17.25/3.13 atleast5p_def, atleast6p_def, atleast7p_def, atleast8p_def, atleast9p_def, % 17.25/3.13 disj_def, e_ax, m_ax, setext % 17.25/3.13 % 17.25/3.13 Those formulas are unsatisfiable: % 17.25/3.13 --------------------------------- % 17.25/3.13 % 17.25/3.13 Begin of proof % 17.25/3.13 | % 17.25/3.13 | ALPHA: (subq_def) implies: % 17.25/3.13 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: int] : (v2 = 0 | ~ (subq(v0, v1) = % 17.25/3.13 | v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: int] : ( ~ (v4 % 17.25/3.13 | = 0) & mem(v3, v1) = v4 & mem(v3, v0) = 0 & $i(v3))) % 17.25/3.13 | % 17.25/3.13 | ALPHA: (s_ax) implies: % 17.25/3.14 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v1) = v2) | % 17.25/3.14 | ~ (mem(v0, v2) = 0) | ~ $i(v1) | ~ $i(v0)) % 17.25/3.14 | % 17.25/3.14 | ALPHA: (u_ax) implies: % 17.25/3.14 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (u(v1, v2) % 17.25/3.14 | = v3) | ~ (mem(v0, v3) = 0) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 17.25/3.14 | ? [v4: any] : ? [v5: any] : (mem(v0, v2) = v5 & mem(v0, v1) = v4 & % 17.25/3.14 | (v5 = 0 | v4 = 0))) % 17.25/3.14 | (4) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : % 17.25/3.14 | (v4 = 0 | ~ (u(v1, v2) = v3) | ~ (mem(v0, v3) = v4) | ~ $i(v2) | ~ % 17.25/3.14 | $i(v1) | ~ $i(v0) | ? [v5: int] : ? [v6: int] : ( ~ (v6 = 0) & ~ % 17.25/3.14 | (v5 = 0) & mem(v0, v2) = v6 & mem(v0, v1) = v5)) % 17.25/3.14 | % 17.25/3.14 | ALPHA: (a_def) implies: % 17.25/3.14 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (a(v0, v1) = v2) | ~ % 17.25/3.14 | $i(v1) | ~ $i(v0) | ? [v3: $i] : (u(v0, v3) = v2 & s(v1) = v3 & % 17.25/3.14 | $i(v3) & $i(v2))) % 17.25/3.14 | % 17.25/3.14 | ALPHA: (n_def) implies: % 17.25/3.14 | (6) ! [v0: $i] : ! [v1: $i] : ( ~ (n(v0) = v1) | ~ $i(v0) | (a(v0, v0) = % 17.25/3.14 | v1 & $i(v1))) % 17.25/3.14 | % 17.25/3.14 | ALPHA: (p_ax) implies: % 17.25/3.14 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: int] : (v3 = 0 | ~ % 17.25/3.14 | (p(v1) = v2) | ~ (mem(v0, v2) = v3) | ~ $i(v1) | ~ $i(v0) | ? % 17.25/3.14 | [v4: int] : ( ~ (v4 = 0) & subq(v0, v1) = v4)) % 17.25/3.14 | % 17.25/3.14 | ALPHA: (subq_342_343) implies: % 17.25/3.14 | (8) $i(e) % 17.25/3.15 | (9) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 17.25/3.15 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 17.25/3.15 | [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: int] : ( ~ (v13 = 0) % 17.25/3.15 | & p(v4) = v10 & n(v4) = v5 & n(v1) = v4 & n(v0) = v6 & n(e) = v0 & % 17.25/3.15 | a(v10, v7) = v11 & a(v5, v7) = v8 & u(v3, v8) = v9 & u(v1, v11) = v12 % 17.25/3.15 | & s(v6) = v7 & s(v2) = v3 & s(v1) = v2 & s(v0) = v1 & subq(v9, v12) = % 17.25/3.15 | v13 & $i(v12) & $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) % 17.25/3.15 | & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 17.25/3.15 | % 17.25/3.15 | ALPHA: (function-axioms) implies: % 17.25/3.15 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (s(v2) = v1) | % 17.25/3.15 | ~ (s(v2) = v0)) % 17.25/3.15 | (11) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] % 17.25/3.15 | : ! [v3: $i] : (v1 = v0 | ~ (mem(v3, v2) = v1) | ~ (mem(v3, v2) = % 17.25/3.15 | v0)) % 17.25/3.15 | % 17.25/3.15 | DELTA: instantiating (9) with fresh symbols all_29_0, all_29_1, all_29_2, % 17.25/3.15 | all_29_3, all_29_4, all_29_5, all_29_6, all_29_7, all_29_8, all_29_9, % 17.25/3.15 | all_29_10, all_29_11, all_29_12, all_29_13 gives: % 17.25/3.15 | (12) ~ (all_29_0 = 0) & p(all_29_9) = all_29_3 & n(all_29_9) = all_29_8 & % 17.25/3.15 | n(all_29_12) = all_29_9 & n(all_29_13) = all_29_7 & n(e) = all_29_13 & % 17.25/3.15 | a(all_29_3, all_29_6) = all_29_2 & a(all_29_8, all_29_6) = all_29_5 & % 17.25/3.15 | u(all_29_10, all_29_5) = all_29_4 & u(all_29_12, all_29_2) = all_29_1 % 17.25/3.15 | & s(all_29_7) = all_29_6 & s(all_29_11) = all_29_10 & s(all_29_12) = % 17.25/3.15 | all_29_11 & s(all_29_13) = all_29_12 & subq(all_29_4, all_29_1) = % 17.25/3.15 | all_29_0 & $i(all_29_1) & $i(all_29_2) & $i(all_29_3) & $i(all_29_4) & % 17.25/3.15 | $i(all_29_5) & $i(all_29_6) & $i(all_29_7) & $i(all_29_8) & % 17.25/3.15 | $i(all_29_9) & $i(all_29_10) & $i(all_29_11) & $i(all_29_12) & % 17.25/3.15 | $i(all_29_13) % 17.25/3.15 | % 17.25/3.15 | ALPHA: (12) implies: % 17.25/3.15 | (13) ~ (all_29_0 = 0) % 17.25/3.15 | (14) $i(all_29_12) % 17.25/3.15 | (15) $i(all_29_10) % 17.25/3.15 | (16) $i(all_29_8) % 17.25/3.16 | (17) $i(all_29_6) % 17.25/3.16 | (18) $i(all_29_4) % 17.25/3.16 | (19) $i(all_29_3) % 17.25/3.16 | (20) $i(all_29_1) % 17.25/3.16 | (21) subq(all_29_4, all_29_1) = all_29_0 % 17.25/3.16 | (22) s(all_29_13) = all_29_12 % 17.25/3.16 | (23) s(all_29_12) = all_29_11 % 17.25/3.16 | (24) s(all_29_11) = all_29_10 % 17.25/3.16 | (25) u(all_29_12, all_29_2) = all_29_1 % 17.25/3.16 | (26) u(all_29_10, all_29_5) = all_29_4 % 17.25/3.16 | (27) a(all_29_8, all_29_6) = all_29_5 % 17.25/3.16 | (28) a(all_29_3, all_29_6) = all_29_2 % 17.25/3.16 | (29) n(e) = all_29_13 % 17.25/3.16 | (30) n(all_29_13) = all_29_7 % 17.25/3.16 | (31) n(all_29_12) = all_29_9 % 17.25/3.16 | (32) n(all_29_9) = all_29_8 % 17.25/3.16 | (33) p(all_29_9) = all_29_3 % 17.25/3.16 | % 17.25/3.16 | GROUND_INST: instantiating (1) with all_29_4, all_29_1, all_29_0, simplifying % 17.25/3.16 | with (18), (20), (21) gives: % 17.25/3.16 | (34) all_29_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & mem(v0, % 17.25/3.16 | all_29_1) = v1 & mem(v0, all_29_4) = 0 & $i(v0)) % 17.25/3.16 | % 17.25/3.16 | GROUND_INST: instantiating (5) with all_29_8, all_29_6, all_29_5, simplifying % 17.25/3.16 | with (16), (17), (27) gives: % 17.25/3.16 | (35) ? [v0: $i] : (u(all_29_8, v0) = all_29_5 & s(all_29_6) = v0 & $i(v0) % 17.25/3.16 | & $i(all_29_5)) % 17.25/3.16 | % 17.25/3.16 | GROUND_INST: instantiating (5) with all_29_3, all_29_6, all_29_2, simplifying % 17.25/3.16 | with (17), (19), (28) gives: % 17.25/3.16 | (36) ? [v0: $i] : (u(all_29_3, v0) = all_29_2 & s(all_29_6) = v0 & $i(v0) % 17.25/3.16 | & $i(all_29_2)) % 17.25/3.16 | % 17.25/3.16 | GROUND_INST: instantiating (6) with e, all_29_13, simplifying with (8), (29) % 17.25/3.16 | gives: % 17.25/3.16 | (37) a(e, e) = all_29_13 & $i(all_29_13) % 17.25/3.16 | % 17.25/3.16 | ALPHA: (37) implies: % 17.25/3.16 | (38) $i(all_29_13) % 17.25/3.16 | % 17.25/3.16 | GROUND_INST: instantiating (6) with all_29_13, all_29_7, simplifying with % 17.25/3.16 | (30), (38) gives: % 17.25/3.17 | (39) a(all_29_13, all_29_13) = all_29_7 & $i(all_29_7) % 17.25/3.17 | % 17.25/3.17 | ALPHA: (39) implies: % 17.25/3.17 | (40) a(all_29_13, all_29_13) = all_29_7 % 17.25/3.17 | % 17.25/3.17 | GROUND_INST: instantiating (6) with all_29_12, all_29_9, simplifying with % 17.25/3.17 | (14), (31) gives: % 17.25/3.17 | (41) a(all_29_12, all_29_12) = all_29_9 & $i(all_29_9) % 17.25/3.17 | % 17.25/3.17 | ALPHA: (41) implies: % 17.25/3.17 | (42) $i(all_29_9) % 17.25/3.17 | (43) a(all_29_12, all_29_12) = all_29_9 % 17.25/3.17 | % 17.25/3.17 | GROUND_INST: instantiating (6) with all_29_9, all_29_8, simplifying with (32), % 17.25/3.17 | (42) gives: % 17.25/3.17 | (44) a(all_29_9, all_29_9) = all_29_8 & $i(all_29_8) % 17.25/3.17 | % 17.25/3.17 | ALPHA: (44) implies: % 17.25/3.17 | (45) a(all_29_9, all_29_9) = all_29_8 % 17.25/3.17 | % 17.25/3.17 | DELTA: instantiating (36) with fresh symbol all_37_0 gives: % 17.25/3.17 | (46) u(all_29_3, all_37_0) = all_29_2 & s(all_29_6) = all_37_0 & % 17.25/3.17 | $i(all_37_0) & $i(all_29_2) % 17.25/3.17 | % 17.25/3.17 | ALPHA: (46) implies: % 17.25/3.17 | (47) $i(all_29_2) % 17.25/3.17 | (48) s(all_29_6) = all_37_0 % 17.25/3.17 | (49) u(all_29_3, all_37_0) = all_29_2 % 17.25/3.17 | % 17.25/3.17 | DELTA: instantiating (35) with fresh symbol all_39_0 gives: % 17.25/3.17 | (50) u(all_29_8, all_39_0) = all_29_5 & s(all_29_6) = all_39_0 & % 17.25/3.17 | $i(all_39_0) & $i(all_29_5) % 17.25/3.17 | % 17.25/3.17 | ALPHA: (50) implies: % 17.25/3.17 | (51) $i(all_29_5) % 17.25/3.17 | (52) $i(all_39_0) % 17.25/3.17 | (53) s(all_29_6) = all_39_0 % 17.25/3.17 | (54) u(all_29_8, all_39_0) = all_29_5 % 17.25/3.17 | % 17.25/3.17 | BETA: splitting (34) gives: % 17.25/3.17 | % 17.25/3.17 | Case 1: % 17.25/3.17 | | % 17.25/3.17 | | (55) all_29_0 = 0 % 17.25/3.17 | | % 17.25/3.17 | | REDUCE: (13), (55) imply: % 17.25/3.17 | | (56) $false % 17.25/3.17 | | % 17.25/3.17 | | CLOSE: (56) is inconsistent. % 17.25/3.17 | | % 17.25/3.17 | Case 2: % 17.25/3.17 | | % 17.25/3.17 | | (57) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & mem(v0, all_29_1) = v1 & % 17.25/3.17 | | mem(v0, all_29_4) = 0 & $i(v0)) % 17.25/3.18 | | % 17.25/3.18 | | DELTA: instantiating (57) with fresh symbols all_45_0, all_45_1 gives: % 17.25/3.18 | | (58) ~ (all_45_0 = 0) & mem(all_45_1, all_29_1) = all_45_0 & % 17.25/3.18 | | mem(all_45_1, all_29_4) = 0 & $i(all_45_1) % 17.25/3.18 | | % 17.25/3.18 | | ALPHA: (58) implies: % 17.25/3.18 | | (59) ~ (all_45_0 = 0) % 17.25/3.18 | | (60) $i(all_45_1) % 17.25/3.18 | | (61) mem(all_45_1, all_29_4) = 0 % 17.25/3.18 | | (62) mem(all_45_1, all_29_1) = all_45_0 % 17.25/3.18 | | % 17.25/3.18 | | GROUND_INST: instantiating (10) with all_37_0, all_39_0, all_29_6, % 17.25/3.18 | | simplifying with (48), (53) gives: % 17.25/3.18 | | (63) all_39_0 = all_37_0 % 17.25/3.18 | | % 17.25/3.18 | | REDUCE: (54), (63) imply: % 17.25/3.18 | | (64) u(all_29_8, all_37_0) = all_29_5 % 17.25/3.18 | | % 17.25/3.18 | | REDUCE: (52), (63) imply: % 17.25/3.18 | | (65) $i(all_37_0) % 17.25/3.18 | | % 17.25/3.18 | | GROUND_INST: instantiating (3) with all_45_1, all_29_10, all_29_5, all_29_4, % 17.25/3.18 | | simplifying with (15), (26), (51), (60), (61) gives: % 17.25/3.18 | | (66) ? [v0: any] : ? [v1: any] : (mem(all_45_1, all_29_5) = v1 & % 17.25/3.18 | | mem(all_45_1, all_29_10) = v0 & (v1 = 0 | v0 = 0)) % 17.25/3.18 | | % 17.25/3.18 | | GROUND_INST: instantiating (4) with all_45_1, all_29_12, all_29_2, all_29_1, % 17.25/3.18 | | all_45_0, simplifying with (14), (25), (47), (60), (62) gives: % 17.25/3.18 | | (67) all_45_0 = 0 | ? [v0: int] : ? [v1: int] : ( ~ (v1 = 0) & ~ (v0 = % 17.25/3.18 | | 0) & mem(all_45_1, all_29_2) = v1 & mem(all_45_1, all_29_12) = % 17.25/3.18 | | v0) % 17.25/3.18 | | % 17.25/3.18 | | GROUND_INST: instantiating (5) with all_29_13, all_29_13, all_29_7, % 17.25/3.18 | | simplifying with (38), (40) gives: % 17.25/3.18 | | (68) ? [v0: $i] : (u(all_29_13, v0) = all_29_7 & s(all_29_13) = v0 & % 17.25/3.18 | | $i(v0) & $i(all_29_7)) % 17.25/3.18 | | % 17.25/3.19 | | GROUND_INST: instantiating (5) with all_29_12, all_29_12, all_29_9, % 17.25/3.19 | | simplifying with (14), (43) gives: % 17.25/3.19 | | (69) ? [v0: $i] : (u(all_29_12, v0) = all_29_9 & s(all_29_12) = v0 & % 17.25/3.19 | | $i(v0) & $i(all_29_9)) % 17.25/3.19 | | % 17.25/3.19 | | GROUND_INST: instantiating (5) with all_29_9, all_29_9, all_29_8, % 17.25/3.19 | | simplifying with (42), (45) gives: % 17.25/3.19 | | (70) ? [v0: $i] : (u(all_29_9, v0) = all_29_8 & s(all_29_9) = v0 & % 17.25/3.19 | | $i(v0) & $i(all_29_8)) % 17.25/3.19 | | % 17.25/3.19 | | DELTA: instantiating (70) with fresh symbol all_61_0 gives: % 17.25/3.19 | | (71) u(all_29_9, all_61_0) = all_29_8 & s(all_29_9) = all_61_0 & % 17.25/3.19 | | $i(all_61_0) & $i(all_29_8) % 17.25/3.19 | | % 17.25/3.19 | | ALPHA: (71) implies: % 17.25/3.19 | | (72) $i(all_61_0) % 17.25/3.19 | | (73) s(all_29_9) = all_61_0 % 17.25/3.19 | | (74) u(all_29_9, all_61_0) = all_29_8 % 17.25/3.19 | | % 17.25/3.19 | | DELTA: instantiating (68) with fresh symbol all_63_0 gives: % 17.25/3.19 | | (75) u(all_29_13, all_63_0) = all_29_7 & s(all_29_13) = all_63_0 & % 17.25/3.19 | | $i(all_63_0) & $i(all_29_7) % 17.25/3.19 | | % 17.25/3.19 | | ALPHA: (75) implies: % 17.25/3.19 | | (76) $i(all_63_0) % 17.25/3.19 | | (77) s(all_29_13) = all_63_0 % 17.25/3.19 | | % 17.25/3.19 | | DELTA: instantiating (66) with fresh symbols all_65_0, all_65_1 gives: % 17.25/3.19 | | (78) mem(all_45_1, all_29_5) = all_65_0 & mem(all_45_1, all_29_10) = % 17.25/3.19 | | all_65_1 & (all_65_0 = 0 | all_65_1 = 0) % 17.25/3.19 | | % 17.25/3.19 | | ALPHA: (78) implies: % 17.25/3.19 | | (79) mem(all_45_1, all_29_10) = all_65_1 % 17.25/3.19 | | (80) mem(all_45_1, all_29_5) = all_65_0 % 17.25/3.19 | | (81) all_65_0 = 0 | all_65_1 = 0 % 17.25/3.19 | | % 17.25/3.19 | | DELTA: instantiating (69) with fresh symbol all_69_0 gives: % 17.25/3.19 | | (82) u(all_29_12, all_69_0) = all_29_9 & s(all_29_12) = all_69_0 & % 17.25/3.19 | | $i(all_69_0) & $i(all_29_9) % 17.25/3.19 | | % 17.25/3.19 | | ALPHA: (82) implies: % 17.25/3.19 | | (83) $i(all_69_0) % 17.25/3.19 | | (84) s(all_29_12) = all_69_0 % 17.25/3.19 | | (85) u(all_29_12, all_69_0) = all_29_9 % 17.25/3.19 | | % 17.25/3.19 | | BETA: splitting (67) gives: % 17.25/3.19 | | % 17.25/3.19 | | Case 1: % 17.25/3.19 | | | % 17.25/3.19 | | | (86) all_45_0 = 0 % 17.25/3.19 | | | % 17.25/3.19 | | | REDUCE: (59), (86) imply: % 17.25/3.19 | | | (87) $false % 17.25/3.19 | | | % 17.25/3.19 | | | CLOSE: (87) is inconsistent. % 17.25/3.19 | | | % 17.25/3.19 | | Case 2: % 17.25/3.19 | | | % 17.25/3.19 | | | (88) ? [v0: int] : ? [v1: int] : ( ~ (v1 = 0) & ~ (v0 = 0) & % 17.25/3.19 | | | mem(all_45_1, all_29_2) = v1 & mem(all_45_1, all_29_12) = v0) % 17.70/3.20 | | | % 17.70/3.20 | | | DELTA: instantiating (88) with fresh symbols all_75_0, all_75_1 gives: % 17.70/3.20 | | | (89) ~ (all_75_0 = 0) & ~ (all_75_1 = 0) & mem(all_45_1, all_29_2) = % 17.70/3.20 | | | all_75_0 & mem(all_45_1, all_29_12) = all_75_1 % 17.70/3.20 | | | % 17.70/3.20 | | | ALPHA: (89) implies: % 17.70/3.20 | | | (90) ~ (all_75_1 = 0) % 17.70/3.20 | | | (91) ~ (all_75_0 = 0) % 17.70/3.20 | | | (92) mem(all_45_1, all_29_12) = all_75_1 % 17.70/3.20 | | | (93) mem(all_45_1, all_29_2) = all_75_0 % 17.70/3.20 | | | % 17.70/3.20 | | | GROUND_INST: instantiating (10) with all_29_12, all_63_0, all_29_13, % 17.70/3.20 | | | simplifying with (22), (77) gives: % 17.70/3.20 | | | (94) all_63_0 = all_29_12 % 17.70/3.20 | | | % 17.70/3.20 | | | GROUND_INST: instantiating (10) with all_29_11, all_69_0, all_29_12, % 17.70/3.20 | | | simplifying with (23), (84) gives: % 17.70/3.20 | | | (95) all_69_0 = all_29_11 % 17.70/3.20 | | | % 17.70/3.20 | | | REDUCE: (85), (95) imply: % 17.70/3.20 | | | (96) u(all_29_12, all_29_11) = all_29_9 % 17.70/3.20 | | | % 17.70/3.20 | | | REDUCE: (83), (95) imply: % 17.70/3.20 | | | (97) $i(all_29_11) % 17.70/3.20 | | | % 17.70/3.20 | | | GROUND_INST: instantiating (4) with all_45_1, all_29_3, all_37_0, % 17.70/3.20 | | | all_29_2, all_75_0, simplifying with (19), (49), (60), (65), % 17.70/3.20 | | | (93) gives: % 17.70/3.20 | | | (98) all_75_0 = 0 | ? [v0: int] : ? [v1: int] : ( ~ (v1 = 0) & ~ (v0 % 17.70/3.20 | | | = 0) & mem(all_45_1, all_37_0) = v1 & mem(all_45_1, all_29_3) % 17.70/3.20 | | | = v0) % 17.70/3.20 | | | % 17.70/3.20 | | | BETA: splitting (81) gives: % 17.70/3.20 | | | % 17.70/3.20 | | | Case 1: % 17.70/3.20 | | | | % 17.70/3.20 | | | | (99) all_65_0 = 0 % 17.70/3.20 | | | | % 17.70/3.20 | | | | REDUCE: (80), (99) imply: % 17.70/3.20 | | | | (100) mem(all_45_1, all_29_5) = 0 % 17.70/3.20 | | | | % 17.70/3.20 | | | | BETA: splitting (98) gives: % 17.70/3.20 | | | | % 17.70/3.20 | | | | Case 1: % 17.70/3.20 | | | | | % 17.70/3.20 | | | | | (101) all_75_0 = 0 % 17.70/3.20 | | | | | % 17.70/3.20 | | | | | REDUCE: (91), (101) imply: % 17.70/3.20 | | | | | (102) $false % 17.70/3.20 | | | | | % 17.70/3.20 | | | | | CLOSE: (102) is inconsistent. % 17.70/3.20 | | | | | % 17.70/3.20 | | | | Case 2: % 17.70/3.20 | | | | | % 17.70/3.20 | | | | | (103) ? [v0: int] : ? [v1: int] : ( ~ (v1 = 0) & ~ (v0 = 0) & % 17.70/3.20 | | | | | mem(all_45_1, all_37_0) = v1 & mem(all_45_1, all_29_3) = % 17.70/3.20 | | | | | v0) % 17.70/3.20 | | | | | % 17.70/3.20 | | | | | DELTA: instantiating (103) with fresh symbols all_92_0, all_92_1 % 17.70/3.20 | | | | | gives: % 17.70/3.20 | | | | | (104) ~ (all_92_0 = 0) & ~ (all_92_1 = 0) & mem(all_45_1, % 17.70/3.20 | | | | | all_37_0) = all_92_0 & mem(all_45_1, all_29_3) = all_92_1 % 17.70/3.20 | | | | | % 17.70/3.20 | | | | | ALPHA: (104) implies: % 17.70/3.20 | | | | | (105) ~ (all_92_1 = 0) % 17.70/3.20 | | | | | (106) ~ (all_92_0 = 0) % 17.70/3.20 | | | | | (107) mem(all_45_1, all_29_3) = all_92_1 % 17.70/3.20 | | | | | (108) mem(all_45_1, all_37_0) = all_92_0 % 17.70/3.20 | | | | | % 17.70/3.20 | | | | | GROUND_INST: instantiating (3) with all_45_1, all_29_8, all_37_0, % 17.70/3.20 | | | | | all_29_5, simplifying with (16), (60), (64), (65), (100) % 17.70/3.21 | | | | | gives: % 17.70/3.21 | | | | | (109) ? [v0: any] : ? [v1: any] : (mem(all_45_1, all_37_0) = v1 & % 17.70/3.21 | | | | | mem(all_45_1, all_29_8) = v0 & (v1 = 0 | v0 = 0)) % 17.70/3.21 | | | | | % 17.70/3.21 | | | | | GROUND_INST: instantiating (7) with all_45_1, all_29_9, all_29_3, % 17.70/3.21 | | | | | all_92_1, simplifying with (33), (42), (60), (107) gives: % 17.70/3.21 | | | | | (110) all_92_1 = 0 | ? [v0: int] : ( ~ (v0 = 0) & subq(all_45_1, % 17.70/3.21 | | | | | all_29_9) = v0) % 17.70/3.21 | | | | | % 17.70/3.21 | | | | | DELTA: instantiating (109) with fresh symbols all_99_0, all_99_1 % 17.70/3.21 | | | | | gives: % 17.70/3.21 | | | | | (111) mem(all_45_1, all_37_0) = all_99_0 & mem(all_45_1, all_29_8) % 17.70/3.21 | | | | | = all_99_1 & (all_99_0 = 0 | all_99_1 = 0) % 17.70/3.21 | | | | | % 17.70/3.21 | | | | | ALPHA: (111) implies: % 17.70/3.21 | | | | | (112) mem(all_45_1, all_29_8) = all_99_1 % 17.70/3.21 | | | | | (113) mem(all_45_1, all_37_0) = all_99_0 % 17.70/3.21 | | | | | (114) all_99_0 = 0 | all_99_1 = 0 % 17.70/3.21 | | | | | % 17.70/3.21 | | | | | BETA: splitting (110) gives: % 17.70/3.21 | | | | | % 17.70/3.21 | | | | | Case 1: % 17.70/3.21 | | | | | | % 17.70/3.21 | | | | | | (115) all_92_1 = 0 % 17.70/3.21 | | | | | | % 17.70/3.21 | | | | | | REDUCE: (105), (115) imply: % 17.70/3.21 | | | | | | (116) $false % 17.70/3.21 | | | | | | % 17.70/3.21 | | | | | | CLOSE: (116) is inconsistent. % 17.70/3.21 | | | | | | % 17.70/3.21 | | | | | Case 2: % 17.70/3.21 | | | | | | % 17.70/3.21 | | | | | | (117) ? [v0: int] : ( ~ (v0 = 0) & subq(all_45_1, all_29_9) = % 17.70/3.21 | | | | | | v0) % 17.70/3.21 | | | | | | % 17.70/3.21 | | | | | | DELTA: instantiating (117) with fresh symbol all_105_0 gives: % 17.70/3.21 | | | | | | (118) ~ (all_105_0 = 0) & subq(all_45_1, all_29_9) = all_105_0 % 17.70/3.21 | | | | | | % 17.70/3.21 | | | | | | ALPHA: (118) implies: % 17.70/3.21 | | | | | | (119) ~ (all_105_0 = 0) % 17.70/3.21 | | | | | | (120) subq(all_45_1, all_29_9) = all_105_0 % 17.70/3.21 | | | | | | % 17.70/3.21 | | | | | | GROUND_INST: instantiating (11) with all_92_0, all_99_0, all_37_0, % 17.70/3.21 | | | | | | all_45_1, simplifying with (108), (113) gives: % 17.70/3.21 | | | | | | (121) all_99_0 = all_92_0 % 17.70/3.21 | | | | | | % 17.70/3.21 | | | | | | BETA: splitting (114) gives: % 17.70/3.21 | | | | | | % 17.70/3.21 | | | | | | Case 1: % 17.70/3.21 | | | | | | | % 17.70/3.21 | | | | | | | (122) all_99_0 = 0 % 17.70/3.21 | | | | | | | % 17.70/3.21 | | | | | | | COMBINE_EQS: (121), (122) imply: % 17.70/3.21 | | | | | | | (123) all_92_0 = 0 % 17.70/3.21 | | | | | | | % 17.70/3.21 | | | | | | | REDUCE: (106), (123) imply: % 17.70/3.21 | | | | | | | (124) $false % 17.70/3.21 | | | | | | | % 17.70/3.21 | | | | | | | CLOSE: (124) is inconsistent. % 17.70/3.21 | | | | | | | % 17.70/3.21 | | | | | | Case 2: % 17.70/3.21 | | | | | | | % 17.70/3.21 | | | | | | | (125) all_99_1 = 0 % 17.70/3.21 | | | | | | | % 17.70/3.21 | | | | | | | REDUCE: (112), (125) imply: % 17.70/3.21 | | | | | | | (126) mem(all_45_1, all_29_8) = 0 % 17.70/3.21 | | | | | | | % 17.70/3.21 | | | | | | | GROUND_INST: instantiating (3) with all_45_1, all_29_9, all_61_0, % 17.70/3.21 | | | | | | | all_29_8, simplifying with (42), (60), (72), (74), % 17.70/3.21 | | | | | | | (126) gives: % 17.70/3.21 | | | | | | | (127) ? [v0: any] : ? [v1: any] : (mem(all_45_1, all_61_0) = % 17.70/3.21 | | | | | | | v1 & mem(all_45_1, all_29_9) = v0 & (v1 = 0 | v0 = 0)) % 17.70/3.21 | | | | | | | % 17.70/3.21 | | | | | | | GROUND_INST: instantiating (1) with all_45_1, all_29_9, all_105_0, % 17.70/3.21 | | | | | | | simplifying with (42), (60), (120) gives: % 17.70/3.22 | | | | | | | (128) all_105_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) % 17.70/3.22 | | | | | | | & mem(v0, all_45_1) = 0 & mem(v0, all_29_9) = v1 & % 17.70/3.22 | | | | | | | $i(v0)) % 17.70/3.22 | | | | | | | % 17.70/3.22 | | | | | | | DELTA: instantiating (127) with fresh symbols all_120_0, all_120_1 % 17.70/3.22 | | | | | | | gives: % 17.70/3.22 | | | | | | | (129) mem(all_45_1, all_61_0) = all_120_0 & mem(all_45_1, % 17.70/3.22 | | | | | | | all_29_9) = all_120_1 & (all_120_0 = 0 | all_120_1 = 0) % 17.70/3.22 | | | | | | | % 17.70/3.22 | | | | | | | ALPHA: (129) implies: % 17.70/3.22 | | | | | | | (130) mem(all_45_1, all_29_9) = all_120_1 % 17.70/3.22 | | | | | | | (131) mem(all_45_1, all_61_0) = all_120_0 % 17.70/3.22 | | | | | | | (132) all_120_0 = 0 | all_120_1 = 0 % 17.70/3.22 | | | | | | | % 17.70/3.22 | | | | | | | BETA: splitting (128) gives: % 17.70/3.22 | | | | | | | % 17.70/3.22 | | | | | | | Case 1: % 17.70/3.22 | | | | | | | | % 17.70/3.22 | | | | | | | | (133) all_105_0 = 0 % 17.70/3.22 | | | | | | | | % 17.70/3.22 | | | | | | | | REDUCE: (119), (133) imply: % 17.70/3.22 | | | | | | | | (134) $false % 17.70/3.22 | | | | | | | | % 17.70/3.22 | | | | | | | | CLOSE: (134) is inconsistent. % 17.70/3.22 | | | | | | | | % 17.70/3.22 | | | | | | | Case 2: % 17.70/3.22 | | | | | | | | % 17.70/3.22 | | | | | | | | (135) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & mem(v0, % 17.70/3.22 | | | | | | | | all_45_1) = 0 & mem(v0, all_29_9) = v1 & $i(v0)) % 17.70/3.22 | | | | | | | | % 17.70/3.22 | | | | | | | | DELTA: instantiating (135) with fresh symbols all_126_0, % 17.70/3.22 | | | | | | | | all_126_1 gives: % 17.70/3.22 | | | | | | | | (136) ~ (all_126_0 = 0) & mem(all_126_1, all_45_1) = 0 & % 17.70/3.22 | | | | | | | | mem(all_126_1, all_29_9) = all_126_0 & $i(all_126_1) % 17.70/3.22 | | | | | | | | % 17.70/3.22 | | | | | | | | ALPHA: (136) implies: % 17.70/3.22 | | | | | | | | (137) ~ (all_126_0 = 0) % 17.70/3.22 | | | | | | | | (138) $i(all_126_1) % 17.70/3.22 | | | | | | | | (139) mem(all_126_1, all_29_9) = all_126_0 % 17.70/3.22 | | | | | | | | (140) mem(all_126_1, all_45_1) = 0 % 17.70/3.22 | | | | | | | | % 17.70/3.22 | | | | | | | | GROUND_INST: instantiating (4) with all_126_1, all_29_12, % 17.70/3.22 | | | | | | | | all_29_11, all_29_9, all_126_0, simplifying with % 17.70/3.22 | | | | | | | | (14), (96), (97), (138), (139) gives: % 17.70/3.22 | | | | | | | | (141) all_126_0 = 0 | ? [v0: int] : ? [v1: int] : ( ~ (v1 = % 17.70/3.22 | | | | | | | | 0) & ~ (v0 = 0) & mem(all_126_1, all_29_11) = v1 & % 17.70/3.22 | | | | | | | | mem(all_126_1, all_29_12) = v0) % 17.70/3.22 | | | | | | | | % 17.70/3.22 | | | | | | | | BETA: splitting (132) gives: % 17.70/3.22 | | | | | | | | % 17.70/3.22 | | | | | | | | Case 1: % 17.70/3.22 | | | | | | | | | % 17.70/3.22 | | | | | | | | | (142) all_120_0 = 0 % 17.70/3.22 | | | | | | | | | % 17.70/3.22 | | | | | | | | | REDUCE: (131), (142) imply: % 17.70/3.22 | | | | | | | | | (143) mem(all_45_1, all_61_0) = 0 % 17.70/3.22 | | | | | | | | | % 17.70/3.22 | | | | | | | | | GROUND_INST: instantiating (2) with all_45_1, all_29_9, % 17.70/3.22 | | | | | | | | | all_61_0, simplifying with (42), (60), (73), (143) % 17.70/3.22 | | | | | | | | | gives: % 17.70/3.22 | | | | | | | | | (144) all_45_1 = all_29_9 % 17.70/3.22 | | | | | | | | | % 17.70/3.22 | | | | | | | | | REDUCE: (140), (144) imply: % 17.70/3.22 | | | | | | | | | (145) mem(all_126_1, all_29_9) = 0 % 17.70/3.22 | | | | | | | | | % 17.70/3.22 | | | | | | | | | GROUND_INST: instantiating (11) with all_126_0, 0, all_29_9, % 17.70/3.22 | | | | | | | | | all_126_1, simplifying with (139), (145) gives: % 17.70/3.22 | | | | | | | | | (146) all_126_0 = 0 % 17.70/3.22 | | | | | | | | | % 17.70/3.22 | | | | | | | | | REDUCE: (137), (146) imply: % 17.70/3.22 | | | | | | | | | (147) $false % 17.70/3.22 | | | | | | | | | % 17.70/3.22 | | | | | | | | | CLOSE: (147) is inconsistent. % 17.70/3.22 | | | | | | | | | % 17.70/3.22 | | | | | | | | Case 2: % 17.70/3.22 | | | | | | | | | % 17.70/3.22 | | | | | | | | | (148) all_120_1 = 0 % 17.70/3.22 | | | | | | | | | % 17.70/3.22 | | | | | | | | | REDUCE: (130), (148) imply: % 17.70/3.22 | | | | | | | | | (149) mem(all_45_1, all_29_9) = 0 % 17.70/3.22 | | | | | | | | | % 17.70/3.22 | | | | | | | | | BETA: splitting (141) gives: % 17.70/3.22 | | | | | | | | | % 17.70/3.22 | | | | | | | | | Case 1: % 17.70/3.22 | | | | | | | | | | % 17.70/3.22 | | | | | | | | | | (150) all_126_0 = 0 % 17.70/3.22 | | | | | | | | | | % 17.70/3.22 | | | | | | | | | | REDUCE: (137), (150) imply: % 17.70/3.22 | | | | | | | | | | (151) $false % 17.70/3.22 | | | | | | | | | | % 17.70/3.22 | | | | | | | | | | CLOSE: (151) is inconsistent. % 17.70/3.22 | | | | | | | | | | % 17.70/3.22 | | | | | | | | | Case 2: % 17.70/3.22 | | | | | | | | | | % 17.70/3.22 | | | | | | | | | | (152) ? [v0: int] : ? [v1: int] : ( ~ (v1 = 0) & ~ (v0 % 17.70/3.23 | | | | | | | | | | = 0) & mem(all_126_1, all_29_11) = v1 & % 17.70/3.23 | | | | | | | | | | mem(all_126_1, all_29_12) = v0) % 17.70/3.23 | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | DELTA: instantiating (152) with fresh symbols all_139_0, % 17.70/3.23 | | | | | | | | | | all_139_1 gives: % 17.70/3.23 | | | | | | | | | | (153) ~ (all_139_0 = 0) & ~ (all_139_1 = 0) & % 17.70/3.23 | | | | | | | | | | mem(all_126_1, all_29_11) = all_139_0 & % 17.70/3.23 | | | | | | | | | | mem(all_126_1, all_29_12) = all_139_1 % 17.70/3.23 | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | ALPHA: (153) implies: % 17.70/3.23 | | | | | | | | | | (154) ~ (all_139_1 = 0) % 17.70/3.23 | | | | | | | | | | (155) mem(all_126_1, all_29_12) = all_139_1 % 17.70/3.23 | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | GROUND_INST: instantiating (3) with all_45_1, all_29_12, % 17.70/3.23 | | | | | | | | | | all_29_11, all_29_9, simplifying with (14), (60), % 17.70/3.23 | | | | | | | | | | (96), (97), (149) gives: % 17.70/3.23 | | | | | | | | | | (156) ? [v0: any] : ? [v1: any] : (mem(all_45_1, % 17.70/3.23 | | | | | | | | | | all_29_11) = v1 & mem(all_45_1, all_29_12) = v0 % 17.70/3.23 | | | | | | | | | | & (v1 = 0 | v0 = 0)) % 17.70/3.23 | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | DELTA: instantiating (156) with fresh symbols all_146_0, % 17.70/3.23 | | | | | | | | | | all_146_1 gives: % 17.70/3.23 | | | | | | | | | | (157) mem(all_45_1, all_29_11) = all_146_0 & % 17.70/3.23 | | | | | | | | | | mem(all_45_1, all_29_12) = all_146_1 & (all_146_0 = % 17.70/3.23 | | | | | | | | | | 0 | all_146_1 = 0) % 17.70/3.23 | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | ALPHA: (157) implies: % 17.70/3.23 | | | | | | | | | | (158) mem(all_45_1, all_29_12) = all_146_1 % 17.70/3.23 | | | | | | | | | | (159) mem(all_45_1, all_29_11) = all_146_0 % 17.70/3.23 | | | | | | | | | | (160) all_146_0 = 0 | all_146_1 = 0 % 17.70/3.23 | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | GROUND_INST: instantiating (11) with all_75_1, all_146_1, % 17.70/3.23 | | | | | | | | | | all_29_12, all_45_1, simplifying with (92), (158) % 17.70/3.23 | | | | | | | | | | gives: % 17.70/3.23 | | | | | | | | | | (161) all_146_1 = all_75_1 % 17.70/3.23 | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | BETA: splitting (160) gives: % 17.70/3.23 | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | Case 1: % 17.70/3.23 | | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | | (162) all_146_0 = 0 % 17.70/3.23 | | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | | REDUCE: (159), (162) imply: % 17.70/3.23 | | | | | | | | | | | (163) mem(all_45_1, all_29_11) = 0 % 17.70/3.23 | | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | | GROUND_INST: instantiating (2) with all_45_1, all_29_12, % 17.70/3.23 | | | | | | | | | | | all_29_11, simplifying with (14), (23), (60), % 17.70/3.23 | | | | | | | | | | | (163) gives: % 17.70/3.23 | | | | | | | | | | | (164) all_45_1 = all_29_12 % 17.70/3.23 | | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | | REDUCE: (140), (164) imply: % 17.70/3.23 | | | | | | | | | | | (165) mem(all_126_1, all_29_12) = 0 % 17.70/3.23 | | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | | GROUND_INST: instantiating (11) with all_139_1, 0, all_29_12, % 17.70/3.23 | | | | | | | | | | | all_126_1, simplifying with (155), (165) gives: % 17.70/3.23 | | | | | | | | | | | (166) all_139_1 = 0 % 17.70/3.23 | | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | | REDUCE: (154), (166) imply: % 17.70/3.23 | | | | | | | | | | | (167) $false % 17.70/3.23 | | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | | CLOSE: (167) is inconsistent. % 17.70/3.23 | | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | Case 2: % 17.70/3.23 | | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | | (168) all_146_1 = 0 % 17.70/3.23 | | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | | COMBINE_EQS: (161), (168) imply: % 17.70/3.23 | | | | | | | | | | | (169) all_75_1 = 0 % 17.70/3.23 | | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | | REDUCE: (90), (169) imply: % 17.70/3.23 | | | | | | | | | | | (170) $false % 17.70/3.23 | | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | | CLOSE: (170) is inconsistent. % 17.70/3.23 | | | | | | | | | | | % 17.70/3.23 | | | | | | | | | | End of split % 17.70/3.23 | | | | | | | | | | % 17.70/3.23 | | | | | | | | | End of split % 17.70/3.23 | | | | | | | | | % 17.70/3.23 | | | | | | | | End of split % 17.70/3.23 | | | | | | | | % 17.70/3.23 | | | | | | | End of split % 17.70/3.23 | | | | | | | % 17.70/3.23 | | | | | | End of split % 17.70/3.23 | | | | | | % 17.70/3.23 | | | | | End of split % 17.70/3.23 | | | | | % 17.70/3.23 | | | | End of split % 17.70/3.23 | | | | % 17.70/3.23 | | | Case 2: % 17.70/3.23 | | | | % 17.70/3.23 | | | | (171) all_65_1 = 0 % 17.70/3.23 | | | | % 17.70/3.23 | | | | REDUCE: (79), (171) imply: % 17.70/3.23 | | | | (172) mem(all_45_1, all_29_10) = 0 % 17.70/3.23 | | | | % 17.70/3.23 | | | | BETA: splitting (98) gives: % 17.70/3.23 | | | | % 17.70/3.23 | | | | Case 1: % 17.70/3.23 | | | | | % 17.70/3.23 | | | | | (173) all_75_0 = 0 % 17.70/3.23 | | | | | % 17.70/3.23 | | | | | REDUCE: (91), (173) imply: % 17.70/3.23 | | | | | (174) $false % 17.70/3.23 | | | | | % 17.70/3.23 | | | | | CLOSE: (174) is inconsistent. % 17.70/3.23 | | | | | % 17.70/3.23 | | | | Case 2: % 17.70/3.23 | | | | | % 17.70/3.23 | | | | | (175) ? [v0: int] : ? [v1: int] : ( ~ (v1 = 0) & ~ (v0 = 0) & % 17.70/3.23 | | | | | mem(all_45_1, all_37_0) = v1 & mem(all_45_1, all_29_3) = % 17.70/3.23 | | | | | v0) % 17.70/3.23 | | | | | % 17.70/3.23 | | | | | DELTA: instantiating (175) with fresh symbols all_92_0, all_92_1 % 17.70/3.23 | | | | | gives: % 17.70/3.23 | | | | | (176) ~ (all_92_0 = 0) & ~ (all_92_1 = 0) & mem(all_45_1, % 17.70/3.23 | | | | | all_37_0) = all_92_0 & mem(all_45_1, all_29_3) = all_92_1 % 17.70/3.23 | | | | | % 17.70/3.23 | | | | | ALPHA: (176) implies: % 17.70/3.23 | | | | | (177) ~ (all_92_1 = 0) % 17.70/3.23 | | | | | (178) mem(all_45_1, all_29_3) = all_92_1 % 17.70/3.23 | | | | | % 17.70/3.24 | | | | | GROUND_INST: instantiating (2) with all_45_1, all_29_11, all_29_10, % 17.70/3.24 | | | | | simplifying with (24), (60), (97), (172) gives: % 17.70/3.24 | | | | | (179) all_45_1 = all_29_11 % 17.70/3.24 | | | | | % 17.70/3.24 | | | | | GROUND_INST: instantiating (7) with all_45_1, all_29_9, all_29_3, % 17.70/3.24 | | | | | all_92_1, simplifying with (33), (42), (60), (178) gives: % 17.70/3.24 | | | | | (180) all_92_1 = 0 | ? [v0: int] : ( ~ (v0 = 0) & subq(all_45_1, % 17.70/3.24 | | | | | all_29_9) = v0) % 17.70/3.24 | | | | | % 17.70/3.24 | | | | | BETA: splitting (180) gives: % 17.70/3.24 | | | | | % 17.70/3.24 | | | | | Case 1: % 17.70/3.24 | | | | | | % 17.70/3.24 | | | | | | (181) all_92_1 = 0 % 17.70/3.24 | | | | | | % 17.70/3.24 | | | | | | REDUCE: (177), (181) imply: % 17.70/3.24 | | | | | | (182) $false % 17.70/3.24 | | | | | | % 17.70/3.24 | | | | | | CLOSE: (182) is inconsistent. % 17.70/3.24 | | | | | | % 17.70/3.24 | | | | | Case 2: % 17.70/3.24 | | | | | | % 17.70/3.24 | | | | | | (183) ? [v0: int] : ( ~ (v0 = 0) & subq(all_45_1, all_29_9) = % 17.70/3.24 | | | | | | v0) % 17.70/3.24 | | | | | | % 17.70/3.24 | | | | | | DELTA: instantiating (183) with fresh symbol all_113_0 gives: % 17.70/3.24 | | | | | | (184) ~ (all_113_0 = 0) & subq(all_45_1, all_29_9) = all_113_0 % 17.70/3.24 | | | | | | % 17.70/3.24 | | | | | | ALPHA: (184) implies: % 17.70/3.24 | | | | | | (185) ~ (all_113_0 = 0) % 17.70/3.24 | | | | | | (186) subq(all_45_1, all_29_9) = all_113_0 % 17.70/3.24 | | | | | | % 17.70/3.24 | | | | | | REDUCE: (179), (186) imply: % 17.70/3.24 | | | | | | (187) subq(all_29_11, all_29_9) = all_113_0 % 17.70/3.24 | | | | | | % 17.70/3.24 | | | | | | GROUND_INST: instantiating (1) with all_29_11, all_29_9, all_113_0, % 17.70/3.24 | | | | | | simplifying with (42), (97), (187) gives: % 17.70/3.24 | | | | | | (188) all_113_0 = 0 | ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & % 17.70/3.24 | | | | | | mem(v0, all_29_9) = v1 & mem(v0, all_29_11) = 0 & $i(v0)) % 17.70/3.24 | | | | | | % 17.70/3.24 | | | | | | BETA: splitting (188) gives: % 17.70/3.24 | | | | | | % 17.70/3.24 | | | | | | Case 1: % 17.70/3.24 | | | | | | | % 17.70/3.24 | | | | | | | (189) all_113_0 = 0 % 17.70/3.24 | | | | | | | % 17.70/3.24 | | | | | | | REDUCE: (185), (189) imply: % 17.70/3.24 | | | | | | | (190) $false % 17.70/3.24 | | | | | | | % 17.70/3.24 | | | | | | | CLOSE: (190) is inconsistent. % 17.70/3.24 | | | | | | | % 17.70/3.24 | | | | | | Case 2: % 17.70/3.24 | | | | | | | % 17.70/3.24 | | | | | | | (191) ? [v0: $i] : ? [v1: int] : ( ~ (v1 = 0) & mem(v0, % 17.70/3.24 | | | | | | | all_29_9) = v1 & mem(v0, all_29_11) = 0 & $i(v0)) % 17.70/3.24 | | | | | | | % 17.70/3.24 | | | | | | | DELTA: instantiating (191) with fresh symbols all_127_0, all_127_1 % 17.70/3.24 | | | | | | | gives: % 17.70/3.24 | | | | | | | (192) ~ (all_127_0 = 0) & mem(all_127_1, all_29_9) = all_127_0 % 17.70/3.24 | | | | | | | & mem(all_127_1, all_29_11) = 0 & $i(all_127_1) % 17.70/3.24 | | | | | | | % 17.70/3.24 | | | | | | | ALPHA: (192) implies: % 17.70/3.24 | | | | | | | (193) ~ (all_127_0 = 0) % 17.70/3.24 | | | | | | | (194) $i(all_127_1) % 17.70/3.24 | | | | | | | (195) mem(all_127_1, all_29_11) = 0 % 17.70/3.24 | | | | | | | (196) mem(all_127_1, all_29_9) = all_127_0 % 17.70/3.24 | | | | | | | % 17.70/3.24 | | | | | | | GROUND_INST: instantiating (2) with all_127_1, all_29_12, % 17.70/3.24 | | | | | | | all_29_11, simplifying with (14), (23), (194), (195) % 17.70/3.24 | | | | | | | gives: % 17.70/3.24 | | | | | | | (197) all_127_1 = all_29_12 % 17.70/3.24 | | | | | | | % 17.70/3.24 | | | | | | | GROUND_INST: instantiating (4) with all_127_1, all_29_12, % 17.70/3.24 | | | | | | | all_29_11, all_29_9, all_127_0, simplifying with % 17.70/3.24 | | | | | | | (14), (96), (97), (194), (196) gives: % 17.70/3.24 | | | | | | | (198) all_127_0 = 0 | ? [v0: int] : ? [v1: int] : ( ~ (v1 = % 17.70/3.24 | | | | | | | 0) & ~ (v0 = 0) & mem(all_127_1, all_29_11) = v1 & % 17.70/3.24 | | | | | | | mem(all_127_1, all_29_12) = v0) % 17.70/3.24 | | | | | | | % 17.70/3.24 | | | | | | | REDUCE: (195), (197) imply: % 17.70/3.24 | | | | | | | (199) mem(all_29_12, all_29_11) = 0 % 17.70/3.24 | | | | | | | % 17.70/3.24 | | | | | | | BETA: splitting (198) gives: % 17.70/3.24 | | | | | | | % 17.70/3.24 | | | | | | | Case 1: % 17.70/3.24 | | | | | | | | % 17.70/3.24 | | | | | | | | (200) all_127_0 = 0 % 17.70/3.24 | | | | | | | | % 17.70/3.24 | | | | | | | | REDUCE: (193), (200) imply: % 17.70/3.24 | | | | | | | | (201) $false % 17.70/3.24 | | | | | | | | % 17.70/3.24 | | | | | | | | CLOSE: (201) is inconsistent. % 17.70/3.24 | | | | | | | | % 17.70/3.24 | | | | | | | Case 2: % 17.70/3.24 | | | | | | | | % 17.70/3.24 | | | | | | | | (202) ? [v0: int] : ? [v1: int] : ( ~ (v1 = 0) & ~ (v0 = % 17.70/3.24 | | | | | | | | 0) & mem(all_127_1, all_29_11) = v1 & % 17.70/3.24 | | | | | | | | mem(all_127_1, all_29_12) = v0) % 17.70/3.24 | | | | | | | | % 17.70/3.24 | | | | | | | | DELTA: instantiating (202) with fresh symbols all_149_0, % 17.70/3.24 | | | | | | | | all_149_1 gives: % 17.70/3.24 | | | | | | | | (203) ~ (all_149_0 = 0) & ~ (all_149_1 = 0) & % 17.70/3.24 | | | | | | | | mem(all_127_1, all_29_11) = all_149_0 & mem(all_127_1, % 17.70/3.24 | | | | | | | | all_29_12) = all_149_1 % 17.70/3.24 | | | | | | | | % 17.70/3.24 | | | | | | | | ALPHA: (203) implies: % 17.70/3.24 | | | | | | | | (204) ~ (all_149_0 = 0) % 17.70/3.24 | | | | | | | | (205) mem(all_127_1, all_29_11) = all_149_0 % 17.70/3.24 | | | | | | | | % 17.70/3.24 | | | | | | | | REDUCE: (197), (205) imply: % 17.70/3.25 | | | | | | | | (206) mem(all_29_12, all_29_11) = all_149_0 % 17.70/3.25 | | | | | | | | % 17.70/3.25 | | | | | | | | GROUND_INST: instantiating (11) with 0, all_149_0, all_29_11, % 17.70/3.25 | | | | | | | | all_29_12, simplifying with (199), (206) gives: % 17.70/3.25 | | | | | | | | (207) all_149_0 = 0 % 17.70/3.25 | | | | | | | | % 17.70/3.25 | | | | | | | | REDUCE: (204), (207) imply: % 17.70/3.25 | | | | | | | | (208) $false % 17.70/3.25 | | | | | | | | % 17.70/3.25 | | | | | | | | CLOSE: (208) is inconsistent. % 17.70/3.25 | | | | | | | | % 17.70/3.25 | | | | | | | End of split % 17.70/3.25 | | | | | | | % 17.70/3.25 | | | | | | End of split % 17.70/3.25 | | | | | | % 17.70/3.25 | | | | | End of split % 17.70/3.25 | | | | | % 17.70/3.25 | | | | End of split % 17.70/3.25 | | | | % 17.70/3.25 | | | End of split % 17.70/3.25 | | | % 17.70/3.25 | | End of split % 17.70/3.25 | | % 17.70/3.25 | End of split % 17.70/3.25 | % 17.70/3.25 End of proof % 17.70/3.25 % SZS output end Proof for theBenchmark % 17.70/3.25 % 17.70/3.25 2629ms %------------------------------------------------------------------------------