%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWC540_1 : TPTP v9.0.0. Bugfixed v9.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n012.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:07:47 AM UTC 2025 % Result : Theorem 28.77s 4.50s % Output : Proof 36.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWC540_1 : TPTP v9.0.0. Bugfixed v9.1.0. % 0.03/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n012.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Mon Mar 31 13:41:34 EDT 2025 % 0.13/0.34 % CPUTime : % 0.67/0.65 ________ _____ % 0.67/0.65 ___ __ \_________(_)________________________________ % 0.67/0.65 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.67/0.65 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.67/0.65 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.67/0.65 % 0.67/0.65 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.67/0.65 (2023-06-19) % 0.67/0.65 % 0.67/0.65 (c) Philipp Rümmer, 2009-2023 % 0.67/0.65 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.67/0.65 Amanda Stjerna. % 0.67/0.65 Free software under BSD-3-Clause. % 0.67/0.65 % 0.67/0.65 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.67/0.65 % 0.67/0.65 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.67/0.66 Running up to 7 provers in parallel. % 0.67/0.67 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.67/0.67 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.67/0.67 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.67/0.67 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.67/0.67 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.67/0.67 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.67/0.67 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 7.50/1.75 Prover 1: Preprocessing ... % 7.60/1.80 Prover 6: Preprocessing ... % 7.60/1.80 Prover 2: Preprocessing ... % 7.60/1.80 Prover 5: Preprocessing ... % 7.60/1.80 Prover 0: Preprocessing ... % 7.60/1.80 Prover 3: Preprocessing ... % 7.60/1.81 Prover 4: Preprocessing ... % 16.39/2.95 Prover 5: Proving ... % 16.96/2.98 Prover 2: Proving ... % 17.25/3.01 Prover 1: Warning: ignoring some quantifiers % 17.46/3.10 Prover 3: Warning: ignoring some quantifiers % 17.46/3.11 Prover 4: Warning: ignoring some quantifiers % 18.15/3.14 Prover 1: Constructing countermodel ... % 18.15/3.14 Prover 3: Constructing countermodel ... % 18.15/3.17 Prover 6: Proving ... % 18.64/3.22 Prover 0: Proving ... % 18.64/3.26 Prover 4: Constructing countermodel ... % 28.77/4.50 Prover 0: proved (3831ms) % 28.77/4.50 % 28.77/4.50 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 28.77/4.50 % 28.77/4.51 Prover 6: stopped % 28.77/4.51 Prover 5: stopped % 28.77/4.51 Prover 2: stopped % 28.77/4.51 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 28.77/4.51 Prover 3: stopped % 29.05/4.52 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 29.05/4.52 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 29.05/4.53 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 29.05/4.53 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 31.54/4.90 Prover 11: Preprocessing ... % 32.03/4.91 Prover 7: Preprocessing ... % 32.03/4.92 Prover 10: Preprocessing ... % 32.03/4.92 Prover 13: Preprocessing ... % 32.03/4.94 Prover 8: Preprocessing ... % 33.81/5.14 Prover 7: Warning: ignoring some quantifiers % 33.89/5.15 Prover 10: Warning: ignoring some quantifiers % 33.89/5.17 Prover 7: Constructing countermodel ... % 33.89/5.17 Prover 4: Found proof (size 60) % 33.89/5.17 Prover 10: Constructing countermodel ... % 33.89/5.18 Prover 13: Warning: ignoring some quantifiers % 33.89/5.18 Prover 4: proved (4507ms) % 33.89/5.18 Prover 1: stopped % 33.89/5.19 Prover 7: stopped % 33.89/5.19 Prover 10: stopped % 33.89/5.20 Prover 13: Constructing countermodel ... % 34.36/5.22 Prover 13: stopped % 34.64/5.31 Prover 8: Warning: ignoring some quantifiers % 34.64/5.33 Prover 8: Constructing countermodel ... % 34.64/5.35 Prover 8: stopped % 35.14/5.38 Prover 11: Warning: ignoring some quantifiers % 35.30/5.40 Prover 11: Constructing countermodel ... % 35.30/5.42 Prover 11: stopped % 35.30/5.42 % 35.30/5.42 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 35.30/5.42 % 35.30/5.43 % SZS output start Proof for theBenchmark % 35.30/5.44 Assumptions after simplification: % 35.30/5.44 --------------------------------- % 35.30/5.44 % 35.30/5.44 (Define:aprp:3) % 35.51/5.48 set_4(g_s64_75) & set_0(g_s40_40) & set_0(g_s37_37) & ? [v0: set_4] : % 35.51/5.48 (set_4(v0) & ! [v1: int] : ! [v2: set_0] : ! [v3: set_0] : ! [v4: int] : % 35.51/5.48 ! [v5: int] : (v5 = 0 | ~ (mem4(v1, v3, v0) = 0) | ~ (mem4(v1, v2, v0) = % 35.51/5.48 0) | ~ (mem0(v4, v3) = v5) | ~ set_0(v3) | ~ set_0(v2) | ? [v6: int] % 35.51/5.48 : ( ~ (v6 = 0) & mem0(v4, v2) = v6)) & ! [v1: int] : ! [v2: set_0] : ! % 35.51/5.48 [v3: set_0] : ! [v4: int] : ! [v5: int] : (v5 = 0 | ~ (mem4(v1, v3, v0) = % 35.51/5.48 0) | ~ (mem4(v1, v2, v0) = 0) | ~ (mem0(v4, v2) = v5) | ~ set_0(v3) | % 35.51/5.48 ~ set_0(v2) | ? [v6: int] : ( ~ (v6 = 0) & mem0(v4, v3) = v6)) & ! [v1: % 35.51/5.48 set_0] : ! [v2: int] : ! [v3: int] : ! [v4: int] : (v3 = 0 | ~ % 35.51/5.48 (mem4(v4, v1, v0) = 0) | ~ (mem0(v2, g_s37_37) = v3) | ~ set_0(v1) | ? % 35.51/5.48 [v5: int] : ( ~ (v5 = 0) & mem0(v2, v1) = v5)) & ! [v1: int] : ! [v2: % 35.51/5.48 set_0] : ! [v3: set_0] : ! [v4: int] : ( ~ (mem4(v1, v3, v0) = 0) | ~ % 35.51/5.48 (mem4(v1, v2, v0) = 0) | ~ (mem0(v4, v3) = 0) | ~ set_0(v3) | ~ % 35.51/5.48 set_0(v2) | mem0(v4, v2) = 0) & ! [v1: int] : ! [v2: set_0] : ! [v3: % 35.51/5.48 set_0] : ! [v4: int] : ( ~ (mem4(v1, v3, v0) = 0) | ~ (mem4(v1, v2, v0) % 35.51/5.48 = 0) | ~ (mem0(v4, v2) = 0) | ~ set_0(v3) | ~ set_0(v2) | mem0(v4, % 35.51/5.48 v3) = 0) & ! [v1: set_0] : ! [v2: int] : ! [v3: int] : (v3 = 0 | ~ % 35.51/5.48 (mem4(v2, v1, v0) = v3) | ~ set_0(v1) | ? [v4: int] : ( ~ (v4 = 0) & % 35.51/5.48 mem4(v2, v1, g_s64_75) = v4)) & ! [v1: set_0] : ! [v2: int] : ! [v3: % 35.51/5.48 int] : (v3 = 0 | ~ (mem4(v2, v1, g_s64_75) = v3) | ~ set_0(v1) | ? [v4: % 35.51/5.48 int] : ( ~ (v4 = 0) & mem4(v2, v1, v0) = v4)) & ! [v1: int] : ! [v2: % 35.51/5.48 int] : ! [v3: set_0] : (v2 = 0 | ~ (mem4(v1, v3, v0) = 0) | ~ (mem0(v1, % 35.51/5.48 g_s40_40) = v2) | ~ set_0(v3)) & ! [v1: set_0] : ! [v2: int] : ! % 35.51/5.49 [v3: int] : ( ~ (mem4(v3, v1, v0) = 0) | ~ (mem0(v2, v1) = 0) | ~ % 35.51/5.49 set_0(v1) | mem0(v2, g_s37_37) = 0) & ! [v1: set_0] : ! [v2: int] : ( ~ % 35.51/5.49 (mem4(v2, v1, v0) = 0) | ~ set_0(v1) | mem4(v2, v1, g_s64_75) = 0) & ! % 35.51/5.49 [v1: set_0] : ! [v2: int] : ( ~ (mem4(v2, v1, g_s64_75) = 0) | ~ set_0(v1) % 35.51/5.49 | mem4(v2, v1, v0) = 0) & ! [v1: int] : ( ~ (mem0(v1, g_s40_40) = 0) | ? % 35.51/5.49 [v2: set_0] : (mem4(v1, v2, v0) = 0 & set_0(v2)))) % 35.51/5.49 % 35.51/5.49 (Define:ctx:16) % 35.51/5.49 set_0(g_s37_37) & ? [v0: int] : ( ~ (v0 = 0) & mem0(max_int, g_s37_37) = v0) % 35.51/5.49 % 35.51/5.49 (Define:imlprp:2) % 35.51/5.49 set_4(g_s64_75) & set_2(g_s79_65) & set_2(g_s78_64) & set_0(g_s40_40) & ! % 35.51/5.49 [v0: set_0] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: int] : ( ~ % 35.51/5.49 ($lesseq(1, $difference(v2, v4))) | ~ (mem4(v1, v0, g_s64_75) = 0) | ~ % 35.51/5.49 (mem2(v1, v4, g_s79_65) = 0) | ~ (mem2(v1, v3, g_s78_64) = 0) | ~ % 35.51/5.49 (mem0(v2, v0) = 0) | ~ set_0(v0)) & ! [v0: set_0] : ! [v1: int] : ! [v2: % 35.51/5.49 int] : ! [v3: int] : ! [v4: int] : ( ~ ($lesseq(1, $difference(v3, v2))) | % 35.51/5.49 ~ (mem4(v1, v0, g_s64_75) = 0) | ~ (mem2(v1, v4, g_s79_65) = 0) | ~ % 35.51/5.49 (mem2(v1, v3, g_s78_64) = 0) | ~ (mem0(v2, v0) = 0) | ~ set_0(v0)) & ! % 35.51/5.49 [v0: set_0] : ! [v1: int] : ! [v2: int] : ! [v3: int] : (v3 = 0 | ~ % 35.51/5.49 (mem4(v1, v0, g_s64_75) = 0) | ~ (mem0(v2, v0) = v3) | ~ set_0(v0) | ? % 35.51/5.49 [v4: int] : ? [v5: int] : (mem2(v1, v5, g_s79_65) = 0 & mem2(v1, v4, % 35.51/5.49 g_s78_64) = 0 & ( ~ ($lesseq(v2, v5)) | ~ ($lesseq(v4, v2))))) & ! % 35.51/5.49 [v0: set_0] : ! [v1: int] : ! [v2: int] : (v2 = 0 | ~ (mem4(v1, v0, % 35.51/5.49 g_s64_75) = v2) | ~ set_0(v0) | ? [v3: int] : ? [v4: any] : ? [v5: % 35.51/5.49 int] : ? [v6: int] : ? [v7: int] : ? [v8: int] : (( ~ (v3 = 0) & % 35.51/5.49 mem0(v1, g_s40_40) = v3) | (mem0(v3, v0) = v4 & ( ~ (v4 = 0) | (v8 = 0 & % 35.51/5.49 v7 = 0 & mem2(v1, v6, g_s79_65) = 0 & mem2(v1, v5, g_s78_64) = 0 & ( % 35.51/5.49 ~ ($lesseq(v3, v6)) | ~ ($lesseq(v5, v3))))) & (v4 = 0 | ( ! [v9: % 35.51/5.49 int] : ! [v10: int] : ( ~ ($lesseq(1, $difference(v3, v10))) | ~ % 35.51/5.49 (mem2(v1, v10, g_s79_65) = 0) | ~ (mem2(v1, v9, g_s78_64) = 0)) & % 35.51/5.49 ! [v9: int] : ! [v10: int] : ( ~ ($lesseq(1, $difference(v9, v3))) % 35.51/5.49 | ~ (mem2(v1, v10, g_s79_65) = 0) | ~ (mem2(v1, v9, g_s78_64) = % 35.51/5.49 0))))))) & ! [v0: set_0] : ! [v1: int] : ( ~ (mem4(v1, v0, % 35.51/5.49 g_s64_75) = 0) | ~ set_0(v0) | mem0(v1, g_s40_40) = 0) % 35.51/5.49 % 35.51/5.49 (Goal) % 35.51/5.50 set_2(g_s79_65) & set_2(g_s78_64) & ? [v0: int] : ? [v1: int] : ($lesseq(1, % 35.51/5.50 $difference(v0, v1)) & mem2(g_s90_81, v1, g_s79_65) = 0 & mem2(g_s90_81, % 35.51/5.50 v0, g_s78_64) = 0) % 35.51/5.50 % 35.51/5.50 (Local_Hyp:1) % 35.51/5.50 mem0(g_s90_81, g_s40_40) = 0 & set_0(g_s40_40) % 35.51/5.50 % 35.51/5.50 (Local_Hyp:2) % 35.51/5.50 set_4(g_s64_75) & ? [v0: set_0] : ? [v1: int] : ( ~ (v1 = 0) & % 35.51/5.50 mem4(g_s90_81, v0, g_s64_75) = v1 & set_0(v0) & ! [v2: int] : ~ (mem0(v2, % 35.51/5.50 v0) = 0)) % 35.51/5.50 % 35.51/5.50 (max_int_axiom) % 35.75/5.50 max_int = 2147483647 % 35.75/5.50 % 35.75/5.50 (function-axioms) % 35.75/5.50 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: set_3] : ! % 35.75/5.50 [v3: int] : ! [v4: int] : ! [v5: int] : (v1 = v0 | ~ (mem3(v5, v4, v3, v2) % 35.75/5.50 = v1) | ~ (mem3(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 35.75/5.50 [v1: MultipleValueBool] : ! [v2: set_4] : ! [v3: set_0] : ! [v4: int] : (v1 % 35.75/5.50 = v0 | ~ (mem4(v4, v3, v2) = v1) | ~ (mem4(v4, v3, v2) = v0)) & ! [v0: % 35.75/5.50 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: set_2] : ! [v3: % 35.75/5.50 int] : ! [v4: int] : (v1 = v0 | ~ (mem2(v4, v3, v2) = v1) | ~ (mem2(v4, % 35.75/5.50 v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 35.75/5.50 : ! [v2: set_0] : ! [v3: int] : (v1 = v0 | ~ (mem0(v3, v2) = v1) | ~ % 35.75/5.50 (mem0(v3, v2) = v0)) % 35.75/5.50 % 35.75/5.50 Further assumptions not needed in the proof: % 35.75/5.50 -------------------------------------------- % 35.75/5.50 Define:aprp:0, Define:aprp:1, Define:aprp:2, Define:aprp:4, Define:aprp:5, % 35.75/5.50 Define:aprp:6, Define:aprp:7, Define:aprp:8, Define:ctx:0, Define:ctx:1, % 35.75/5.50 Define:ctx:10, Define:ctx:11, Define:ctx:12, Define:ctx:13, Define:ctx:14, % 35.75/5.50 Define:ctx:15, Define:ctx:17, Define:ctx:18, Define:ctx:19, Define:ctx:2, % 35.75/5.50 Define:ctx:20, Define:ctx:21, Define:ctx:22, Define:ctx:23, Define:ctx:24, % 35.75/5.50 Define:ctx:25, Define:ctx:26, Define:ctx:27, Define:ctx:28, Define:ctx:29, % 35.75/5.50 Define:ctx:3, Define:ctx:30, Define:ctx:31, Define:ctx:32, Define:ctx:33, % 35.75/5.50 Define:ctx:34, Define:ctx:35, Define:ctx:36, Define:ctx:37, Define:ctx:38, % 35.75/5.50 Define:ctx:39, Define:ctx:4, Define:ctx:40, Define:ctx:41, Define:ctx:42, % 35.75/5.50 Define:ctx:43, Define:ctx:44, Define:ctx:45, Define:ctx:46, Define:ctx:47, % 35.75/5.50 Define:ctx:48, Define:ctx:49, Define:ctx:5, Define:ctx:50, Define:ctx:51, % 35.75/5.50 Define:ctx:52, Define:ctx:53, Define:ctx:54, Define:ctx:55, Define:ctx:6, % 35.75/5.50 Define:ctx:7, Define:ctx:8, Define:ctx:9, Define:imext:0, Define:imext:1, % 35.75/5.50 Define:imlprp:0, Define:imlprp:1, Define:imlprp:3, Define:imlprp:4, % 35.75/5.50 Define:imprp:0, Define:imprp:1, Define:imprp:10, Define:imprp:2, Define:imprp:3, % 35.75/5.50 Define:imprp:4, Define:imprp:5, Define:imprp:6, Define:imprp:7, Define:imprp:8, % 35.75/5.50 Define:imprp:9, Define:inv:0, Define:inv:1, Define:inv:2, Define:inv:3, % 35.75/5.50 Define:inv:4, Define:inv:5, Define:inv:6, Define:inv:7, Define:seext:0, % 35.75/5.50 Define:seext:1, Define:seext:2, Define:seext:3, Local_Hyp:0, min_int_axiom % 35.75/5.50 % 35.75/5.50 Those formulas are unsatisfiable: % 35.75/5.50 --------------------------------- % 35.75/5.50 % 35.75/5.50 Begin of proof % 35.75/5.50 | % 35.75/5.50 | ALPHA: (Define:aprp:3) implies: % 35.75/5.51 | (1) ? [v0: set_4] : (set_4(v0) & ! [v1: int] : ! [v2: set_0] : ! [v3: % 35.75/5.51 | set_0] : ! [v4: int] : ! [v5: int] : (v5 = 0 | ~ (mem4(v1, v3, % 35.75/5.51 | v0) = 0) | ~ (mem4(v1, v2, v0) = 0) | ~ (mem0(v4, v3) = v5) | % 35.75/5.51 | ~ set_0(v3) | ~ set_0(v2) | ? [v6: int] : ( ~ (v6 = 0) & % 35.75/5.51 | mem0(v4, v2) = v6)) & ! [v1: int] : ! [v2: set_0] : ! [v3: % 35.75/5.51 | set_0] : ! [v4: int] : ! [v5: int] : (v5 = 0 | ~ (mem4(v1, v3, % 35.75/5.51 | v0) = 0) | ~ (mem4(v1, v2, v0) = 0) | ~ (mem0(v4, v2) = v5) | % 35.75/5.51 | ~ set_0(v3) | ~ set_0(v2) | ? [v6: int] : ( ~ (v6 = 0) & % 35.75/5.51 | mem0(v4, v3) = v6)) & ! [v1: set_0] : ! [v2: int] : ! [v3: % 35.75/5.51 | int] : ! [v4: int] : (v3 = 0 | ~ (mem4(v4, v1, v0) = 0) | ~ % 35.75/5.51 | (mem0(v2, g_s37_37) = v3) | ~ set_0(v1) | ? [v5: int] : ( ~ (v5 = % 35.75/5.51 | 0) & mem0(v2, v1) = v5)) & ! [v1: int] : ! [v2: set_0] : ! % 35.75/5.51 | [v3: set_0] : ! [v4: int] : ( ~ (mem4(v1, v3, v0) = 0) | ~ % 35.75/5.51 | (mem4(v1, v2, v0) = 0) | ~ (mem0(v4, v3) = 0) | ~ set_0(v3) | ~ % 35.75/5.51 | set_0(v2) | mem0(v4, v2) = 0) & ! [v1: int] : ! [v2: set_0] : ! % 35.75/5.51 | [v3: set_0] : ! [v4: int] : ( ~ (mem4(v1, v3, v0) = 0) | ~ % 35.75/5.51 | (mem4(v1, v2, v0) = 0) | ~ (mem0(v4, v2) = 0) | ~ set_0(v3) | ~ % 35.75/5.51 | set_0(v2) | mem0(v4, v3) = 0) & ! [v1: set_0] : ! [v2: int] : ! % 35.75/5.51 | [v3: int] : (v3 = 0 | ~ (mem4(v2, v1, v0) = v3) | ~ set_0(v1) | ? % 35.75/5.51 | [v4: int] : ( ~ (v4 = 0) & mem4(v2, v1, g_s64_75) = v4)) & ! [v1: % 35.75/5.51 | set_0] : ! [v2: int] : ! [v3: int] : (v3 = 0 | ~ (mem4(v2, v1, % 35.75/5.51 | g_s64_75) = v3) | ~ set_0(v1) | ? [v4: int] : ( ~ (v4 = 0) & % 35.75/5.51 | mem4(v2, v1, v0) = v4)) & ! [v1: int] : ! [v2: int] : ! [v3: % 35.75/5.51 | set_0] : (v2 = 0 | ~ (mem4(v1, v3, v0) = 0) | ~ (mem0(v1, % 35.75/5.51 | g_s40_40) = v2) | ~ set_0(v3)) & ! [v1: set_0] : ! [v2: int] % 35.75/5.51 | : ! [v3: int] : ( ~ (mem4(v3, v1, v0) = 0) | ~ (mem0(v2, v1) = 0) | % 35.75/5.51 | ~ set_0(v1) | mem0(v2, g_s37_37) = 0) & ! [v1: set_0] : ! [v2: % 35.75/5.51 | int] : ( ~ (mem4(v2, v1, v0) = 0) | ~ set_0(v1) | mem4(v2, v1, % 35.75/5.51 | g_s64_75) = 0) & ! [v1: set_0] : ! [v2: int] : ( ~ (mem4(v2, % 35.75/5.51 | v1, g_s64_75) = 0) | ~ set_0(v1) | mem4(v2, v1, v0) = 0) & ! % 35.75/5.51 | [v1: int] : ( ~ (mem0(v1, g_s40_40) = 0) | ? [v2: set_0] : (mem4(v1, % 35.75/5.51 | v2, v0) = 0 & set_0(v2)))) % 35.75/5.51 | % 35.75/5.51 | ALPHA: (Define:ctx:16) implies: % 35.75/5.51 | (2) ? [v0: int] : ( ~ (v0 = 0) & mem0(max_int, g_s37_37) = v0) % 35.75/5.51 | % 35.75/5.51 | ALPHA: (Define:imlprp:2) implies: % 35.75/5.51 | (3) ! [v0: set_0] : ! [v1: int] : ! [v2: int] : (v2 = 0 | ~ (mem4(v1, % 35.75/5.51 | v0, g_s64_75) = v2) | ~ set_0(v0) | ? [v3: int] : ? [v4: any] % 35.75/5.51 | : ? [v5: int] : ? [v6: int] : ? [v7: int] : ? [v8: int] : (( ~ % 35.75/5.51 | (v3 = 0) & mem0(v1, g_s40_40) = v3) | (mem0(v3, v0) = v4 & ( ~ % 35.75/5.51 | (v4 = 0) | (v8 = 0 & v7 = 0 & mem2(v1, v6, g_s79_65) = 0 & % 35.75/5.51 | mem2(v1, v5, g_s78_64) = 0 & ( ~ ($lesseq(v3, v6)) | ~ % 35.75/5.51 | ($lesseq(v5, v3))))) & (v4 = 0 | ( ! [v9: int] : ! [v10: % 35.75/5.51 | int] : ( ~ ($lesseq(1, $difference(v3, v10))) | ~ % 35.75/5.51 | (mem2(v1, v10, g_s79_65) = 0) | ~ (mem2(v1, v9, g_s78_64) % 35.75/5.51 | = 0)) & ! [v9: int] : ! [v10: int] : ( ~ ($lesseq(1, % 35.75/5.51 | $difference(v9, v3))) | ~ (mem2(v1, v10, g_s79_65) = % 35.75/5.51 | 0) | ~ (mem2(v1, v9, g_s78_64) = 0))))))) % 35.75/5.52 | (4) ! [v0: set_0] : ! [v1: int] : ! [v2: int] : ! [v3: int] : (v3 = 0 | % 35.75/5.52 | ~ (mem4(v1, v0, g_s64_75) = 0) | ~ (mem0(v2, v0) = v3) | ~ % 35.75/5.52 | set_0(v0) | ? [v4: int] : ? [v5: int] : (mem2(v1, v5, g_s79_65) = 0 % 35.75/5.52 | & mem2(v1, v4, g_s78_64) = 0 & ( ~ ($lesseq(v2, v5)) | ~ % 35.75/5.52 | ($lesseq(v4, v2))))) % 35.75/5.52 | % 35.75/5.52 | ALPHA: (Local_Hyp:1) implies: % 35.75/5.52 | (5) mem0(g_s90_81, g_s40_40) = 0 % 35.75/5.52 | % 35.75/5.52 | ALPHA: (Local_Hyp:2) implies: % 35.75/5.52 | (6) ? [v0: set_0] : ? [v1: int] : ( ~ (v1 = 0) & mem4(g_s90_81, v0, % 35.75/5.52 | g_s64_75) = v1 & set_0(v0) & ! [v2: int] : ~ (mem0(v2, v0) = 0)) % 35.75/5.52 | % 35.75/5.52 | ALPHA: (Goal) implies: % 35.75/5.52 | (7) ? [v0: int] : ? [v1: int] : ($lesseq(1, $difference(v0, v1)) & % 35.75/5.52 | mem2(g_s90_81, v1, g_s79_65) = 0 & mem2(g_s90_81, v0, g_s78_64) = 0) % 35.75/5.52 | % 35.75/5.52 | ALPHA: (function-axioms) implies: % 35.75/5.52 | (8) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 35.75/5.52 | set_0] : ! [v3: int] : (v1 = v0 | ~ (mem0(v3, v2) = v1) | ~ % 35.75/5.52 | (mem0(v3, v2) = v0)) % 35.75/5.52 | % 35.75/5.52 | DELTA: instantiating (2) with fresh symbol all_74_0 gives: % 35.75/5.52 | (9) ~ (all_74_0 = 0) & mem0(max_int, g_s37_37) = all_74_0 % 35.75/5.52 | % 35.75/5.52 | ALPHA: (9) implies: % 35.75/5.52 | (10) ~ (all_74_0 = 0) % 35.75/5.52 | (11) mem0(max_int, g_s37_37) = all_74_0 % 35.75/5.52 | % 35.75/5.52 | DELTA: instantiating (7) with fresh symbols all_90_0, all_90_1 gives: % 35.75/5.52 | (12) $lesseq(1, $difference(all_90_1, all_90_0)) & mem2(g_s90_81, all_90_0, % 35.75/5.52 | g_s79_65) = 0 & mem2(g_s90_81, all_90_1, g_s78_64) = 0 % 35.75/5.52 | % 35.75/5.52 | ALPHA: (12) implies: % 35.75/5.52 | (13) $lesseq(1, $difference(all_90_1, all_90_0)) % 35.75/5.52 | (14) mem2(g_s90_81, all_90_1, g_s78_64) = 0 % 35.75/5.52 | (15) mem2(g_s90_81, all_90_0, g_s79_65) = 0 % 35.75/5.52 | % 35.75/5.52 | DELTA: instantiating (6) with fresh symbols all_95_0, all_95_1 gives: % 35.75/5.52 | (16) ~ (all_95_0 = 0) & mem4(g_s90_81, all_95_1, g_s64_75) = all_95_0 & % 35.75/5.52 | set_0(all_95_1) & ! [v0: int] : ~ (mem0(v0, all_95_1) = 0) % 35.75/5.52 | % 35.75/5.52 | ALPHA: (16) implies: % 35.75/5.52 | (17) ~ (all_95_0 = 0) % 35.75/5.52 | (18) set_0(all_95_1) % 35.75/5.52 | (19) mem4(g_s90_81, all_95_1, g_s64_75) = all_95_0 % 35.75/5.52 | (20) ! [v0: int] : ~ (mem0(v0, all_95_1) = 0) % 35.75/5.52 | % 35.75/5.52 | DELTA: instantiating (1) with fresh symbol all_167_0 gives: % 35.75/5.53 | (21) set_4(all_167_0) & ! [v0: int] : ! [v1: set_0] : ! [v2: set_0] : ! % 35.75/5.53 | [v3: int] : ! [v4: int] : (v4 = 0 | ~ (mem4(v0, v2, all_167_0) = 0) % 35.75/5.53 | | ~ (mem4(v0, v1, all_167_0) = 0) | ~ (mem0(v3, v2) = v4) | ~ % 35.75/5.53 | set_0(v2) | ~ set_0(v1) | ? [v5: int] : ( ~ (v5 = 0) & mem0(v3, % 35.75/5.53 | v1) = v5)) & ! [v0: int] : ! [v1: set_0] : ! [v2: set_0] : ! % 35.75/5.53 | [v3: int] : ! [v4: int] : (v4 = 0 | ~ (mem4(v0, v2, all_167_0) = 0) % 35.75/5.53 | | ~ (mem4(v0, v1, all_167_0) = 0) | ~ (mem0(v3, v1) = v4) | ~ % 35.75/5.53 | set_0(v2) | ~ set_0(v1) | ? [v5: int] : ( ~ (v5 = 0) & mem0(v3, % 35.75/5.53 | v2) = v5)) & ! [v0: set_0] : ! [v1: int] : ! [v2: int] : ! % 35.75/5.53 | [v3: int] : (v2 = 0 | ~ (mem4(v3, v0, all_167_0) = 0) | ~ (mem0(v1, % 35.75/5.53 | g_s37_37) = v2) | ~ set_0(v0) | ? [v4: int] : ( ~ (v4 = 0) & % 35.75/5.53 | mem0(v1, v0) = v4)) & ! [v0: int] : ! [v1: set_0] : ! [v2: % 35.75/5.53 | set_0] : ! [v3: int] : ( ~ (mem4(v0, v2, all_167_0) = 0) | ~ % 35.75/5.53 | (mem4(v0, v1, all_167_0) = 0) | ~ (mem0(v3, v2) = 0) | ~ set_0(v2) % 35.75/5.53 | | ~ set_0(v1) | mem0(v3, v1) = 0) & ! [v0: int] : ! [v1: set_0] : % 35.75/5.53 | ! [v2: set_0] : ! [v3: int] : ( ~ (mem4(v0, v2, all_167_0) = 0) | ~ % 35.75/5.53 | (mem4(v0, v1, all_167_0) = 0) | ~ (mem0(v3, v1) = 0) | ~ set_0(v2) % 35.75/5.53 | | ~ set_0(v1) | mem0(v3, v2) = 0) & ! [v0: set_0] : ! [v1: int] : % 35.75/5.53 | ! [v2: int] : (v2 = 0 | ~ (mem4(v1, v0, all_167_0) = v2) | ~ % 35.75/5.53 | set_0(v0) | ? [v3: int] : ( ~ (v3 = 0) & mem4(v1, v0, g_s64_75) = % 35.75/5.53 | v3)) & ! [v0: set_0] : ! [v1: int] : ! [v2: int] : (v2 = 0 | ~ % 35.75/5.53 | (mem4(v1, v0, g_s64_75) = v2) | ~ set_0(v0) | ? [v3: int] : ( ~ % 35.75/5.53 | (v3 = 0) & mem4(v1, v0, all_167_0) = v3)) & ! [v0: int] : ! [v1: % 35.75/5.53 | int] : ! [v2: set_0] : (v1 = 0 | ~ (mem4(v0, v2, all_167_0) = 0) | % 35.75/5.53 | ~ (mem0(v0, g_s40_40) = v1) | ~ set_0(v2)) & ! [v0: set_0] : ! % 35.75/5.53 | [v1: int] : ! [v2: int] : ( ~ (mem4(v2, v0, all_167_0) = 0) | ~ % 35.75/5.53 | (mem0(v1, v0) = 0) | ~ set_0(v0) | mem0(v1, g_s37_37) = 0) & ! % 35.75/5.53 | [v0: set_0] : ! [v1: int] : ( ~ (mem4(v1, v0, all_167_0) = 0) | ~ % 35.75/5.53 | set_0(v0) | mem4(v1, v0, g_s64_75) = 0) & ! [v0: set_0] : ! [v1: % 35.75/5.53 | int] : ( ~ (mem4(v1, v0, g_s64_75) = 0) | ~ set_0(v0) | mem4(v1, % 35.75/5.53 | v0, all_167_0) = 0) & ! [v0: int] : ( ~ (mem0(v0, g_s40_40) = 0) % 35.75/5.53 | | ? [v1: set_0] : (mem4(v0, v1, all_167_0) = 0 & set_0(v1))) % 35.75/5.53 | % 35.75/5.53 | ALPHA: (21) implies: % 35.75/5.53 | (22) ! [v0: int] : ( ~ (mem0(v0, g_s40_40) = 0) | ? [v1: set_0] : % 35.75/5.53 | (mem4(v0, v1, all_167_0) = 0 & set_0(v1))) % 35.75/5.53 | (23) ! [v0: set_0] : ! [v1: int] : ( ~ (mem4(v1, v0, all_167_0) = 0) | ~ % 35.75/5.53 | set_0(v0) | mem4(v1, v0, g_s64_75) = 0) % 35.75/5.53 | (24) ! [v0: set_0] : ! [v1: int] : ! [v2: int] : ! [v3: int] : (v2 = 0 % 35.75/5.53 | | ~ (mem4(v3, v0, all_167_0) = 0) | ~ (mem0(v1, g_s37_37) = v2) | % 35.75/5.53 | ~ set_0(v0) | ? [v4: int] : ( ~ (v4 = 0) & mem0(v1, v0) = v4)) % 35.75/5.53 | % 35.75/5.53 | REDUCE: (11), (max_int_axiom) imply: % 35.75/5.53 | (25) mem0(2147483647, g_s37_37) = all_74_0 % 35.75/5.53 | % 35.75/5.53 | GROUND_INST: instantiating (22) with g_s90_81, simplifying with (5) gives: % 35.75/5.53 | (26) ? [v0: set_0] : (mem4(g_s90_81, v0, all_167_0) = 0 & set_0(v0)) % 35.75/5.53 | % 35.75/5.53 | GROUND_INST: instantiating (3) with all_95_1, g_s90_81, all_95_0, simplifying % 35.75/5.53 | with (18), (19) gives: % 35.75/5.53 | (27) all_95_0 = 0 | ? [v0: int] : ? [v1: any] : ? [v2: int] : ? [v3: % 35.75/5.53 | int] : ? [v4: int] : ? [v5: int] : (( ~ (v0 = 0) & mem0(g_s90_81, % 35.75/5.53 | g_s40_40) = v0) | (mem0(v0, all_95_1) = v1 & ( ~ (v1 = 0) | (v5 % 35.75/5.53 | = 0 & v4 = 0 & mem2(g_s90_81, v3, g_s79_65) = 0 & % 35.75/5.53 | mem2(g_s90_81, v2, g_s78_64) = 0 & ( ~ ($lesseq(v0, v3)) | ~ % 35.75/5.53 | ($lesseq(v2, v0))))) & (v1 = 0 | ( ! [v6: int] : ! [v7: % 35.75/5.53 | int] : ( ~ ($lesseq(1, $difference(v0, v7))) | ~ % 35.75/5.53 | (mem2(g_s90_81, v7, g_s79_65) = 0) | ~ (mem2(g_s90_81, v6, % 35.75/5.53 | g_s78_64) = 0)) & ! [v6: int] : ! [v7: int] : ( ~ % 35.75/5.53 | ($lesseq(1, $difference(v6, v0))) | ~ (mem2(g_s90_81, v7, % 35.75/5.53 | g_s79_65) = 0) | ~ (mem2(g_s90_81, v6, g_s78_64) = % 35.75/5.53 | 0)))))) % 35.75/5.53 | % 35.75/5.53 | DELTA: instantiating (26) with fresh symbol all_238_0 gives: % 35.75/5.53 | (28) mem4(g_s90_81, all_238_0, all_167_0) = 0 & set_0(all_238_0) % 35.75/5.53 | % 35.75/5.53 | ALPHA: (28) implies: % 35.75/5.53 | (29) set_0(all_238_0) % 35.75/5.53 | (30) mem4(g_s90_81, all_238_0, all_167_0) = 0 % 35.75/5.53 | % 35.75/5.53 | BETA: splitting (27) gives: % 35.75/5.53 | % 35.75/5.53 | Case 1: % 35.75/5.53 | | % 35.75/5.53 | | (31) all_95_0 = 0 % 35.75/5.53 | | % 35.75/5.53 | | REDUCE: (17), (31) imply: % 35.75/5.53 | | (32) $false % 35.75/5.54 | | % 35.75/5.54 | | CLOSE: (32) is inconsistent. % 35.75/5.54 | | % 35.75/5.54 | Case 2: % 35.75/5.54 | | % 35.75/5.54 | | (33) ? [v0: int] : ? [v1: any] : ? [v2: int] : ? [v3: int] : ? [v4: % 35.75/5.54 | | int] : ? [v5: int] : (( ~ (v0 = 0) & mem0(g_s90_81, g_s40_40) = % 35.75/5.54 | | v0) | (mem0(v0, all_95_1) = v1 & ( ~ (v1 = 0) | (v5 = 0 & v4 = 0 % 35.75/5.54 | | & mem2(g_s90_81, v3, g_s79_65) = 0 & mem2(g_s90_81, v2, % 35.75/5.54 | | g_s78_64) = 0 & ( ~ ($lesseq(v0, v3)) | ~ ($lesseq(v2, % 35.75/5.54 | | v0))))) & (v1 = 0 | ( ! [v6: int] : ! [v7: int] : ( ~ % 35.75/5.54 | | ($lesseq(1, $difference(v0, v7))) | ~ (mem2(g_s90_81, v7, % 35.75/5.54 | | g_s79_65) = 0) | ~ (mem2(g_s90_81, v6, g_s78_64) = % 35.75/5.54 | | 0)) & ! [v6: int] : ! [v7: int] : ( ~ ($lesseq(1, % 35.75/5.54 | | $difference(v6, v0))) | ~ (mem2(g_s90_81, v7, % 35.75/5.54 | | g_s79_65) = 0) | ~ (mem2(g_s90_81, v6, g_s78_64) = % 35.75/5.54 | | 0)))))) % 35.75/5.54 | | % 35.75/5.54 | | DELTA: instantiating (33) with fresh symbols all_289_0, all_289_1, % 35.75/5.54 | | all_289_2, all_289_3, all_289_4, all_289_5 gives: % 35.75/5.54 | | (34) ( ~ (all_289_5 = 0) & mem0(g_s90_81, g_s40_40) = all_289_5) | % 35.75/5.54 | | (mem0(all_289_5, all_95_1) = all_289_4 & ( ~ (all_289_4 = 0) | % 35.75/5.54 | | (all_289_0 = 0 & all_289_1 = 0 & mem2(g_s90_81, all_289_2, % 35.75/5.54 | | g_s79_65) = 0 & mem2(g_s90_81, all_289_3, g_s78_64) = 0 & ( % 35.75/5.54 | | ~ ($lesseq(all_289_5, all_289_2)) | ~ ($lesseq(all_289_3, % 35.75/5.54 | | all_289_5))))) & (all_289_4 = 0 | ( ! [v0: int] : ! % 35.75/5.54 | | [v1: int] : ( ~ ($lesseq(1, $difference(all_289_5, v1))) | ~ % 35.75/5.54 | | (mem2(g_s90_81, v1, g_s79_65) = 0) | ~ (mem2(g_s90_81, v0, % 35.75/5.54 | | g_s78_64) = 0)) & ! [v0: int] : ! [v1: int] : ( ~ % 35.75/5.54 | | ($lesseq(1, $difference(v0, all_289_5))) | ~ % 35.75/5.54 | | (mem2(g_s90_81, v1, g_s79_65) = 0) | ~ (mem2(g_s90_81, v0, % 35.75/5.54 | | g_s78_64) = 0))))) % 35.75/5.54 | | % 35.75/5.54 | | BETA: splitting (34) gives: % 35.75/5.54 | | % 35.75/5.54 | | Case 1: % 35.75/5.54 | | | % 35.75/5.54 | | | (35) ~ (all_289_5 = 0) & mem0(g_s90_81, g_s40_40) = all_289_5 % 35.75/5.54 | | | % 35.75/5.54 | | | ALPHA: (35) implies: % 35.75/5.54 | | | (36) ~ (all_289_5 = 0) % 35.75/5.54 | | | (37) mem0(g_s90_81, g_s40_40) = all_289_5 % 35.75/5.54 | | | % 35.75/5.54 | | | GROUND_INST: instantiating (8) with 0, all_289_5, g_s40_40, g_s90_81, % 35.75/5.54 | | | simplifying with (5), (37) gives: % 35.75/5.54 | | | (38) all_289_5 = 0 % 35.75/5.54 | | | % 35.75/5.54 | | | REDUCE: (36), (38) imply: % 35.75/5.54 | | | (39) $false % 35.75/5.54 | | | % 35.75/5.54 | | | CLOSE: (39) is inconsistent. % 35.75/5.54 | | | % 35.75/5.54 | | Case 2: % 35.75/5.54 | | | % 35.75/5.54 | | | (40) mem0(all_289_5, all_95_1) = all_289_4 & ( ~ (all_289_4 = 0) | % 35.75/5.54 | | | (all_289_0 = 0 & all_289_1 = 0 & mem2(g_s90_81, all_289_2, % 35.75/5.54 | | | g_s79_65) = 0 & mem2(g_s90_81, all_289_3, g_s78_64) = 0 & ( % 35.75/5.54 | | | ~ ($lesseq(all_289_5, all_289_2)) | ~ ($lesseq(all_289_3, % 35.75/5.54 | | | all_289_5))))) & (all_289_4 = 0 | ( ! [v0: int] : ! % 35.75/5.54 | | | [v1: int] : ( ~ ($lesseq(1, $difference(all_289_5, v1))) | ~ % 35.75/5.54 | | | (mem2(g_s90_81, v1, g_s79_65) = 0) | ~ (mem2(g_s90_81, v0, % 35.75/5.54 | | | g_s78_64) = 0)) & ! [v0: int] : ! [v1: int] : ( ~ % 35.75/5.54 | | | ($lesseq(1, $difference(v0, all_289_5))) | ~ % 35.75/5.54 | | | (mem2(g_s90_81, v1, g_s79_65) = 0) | ~ (mem2(g_s90_81, v0, % 35.75/5.54 | | | g_s78_64) = 0)))) % 35.75/5.54 | | | % 35.75/5.54 | | | ALPHA: (40) implies: % 35.75/5.54 | | | (41) mem0(all_289_5, all_95_1) = all_289_4 % 35.75/5.54 | | | (42) all_289_4 = 0 | ( ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(1, % 35.75/5.54 | | | $difference(all_289_5, v1))) | ~ (mem2(g_s90_81, v1, % 35.75/5.54 | | | g_s79_65) = 0) | ~ (mem2(g_s90_81, v0, g_s78_64) = 0)) & % 35.75/5.54 | | | ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(1, $difference(v0, % 35.75/5.54 | | | all_289_5))) | ~ (mem2(g_s90_81, v1, g_s79_65) = 0) | % 35.75/5.54 | | | ~ (mem2(g_s90_81, v0, g_s78_64) = 0))) % 35.75/5.54 | | | % 35.75/5.54 | | | GROUND_INST: instantiating (24) with all_238_0, 2147483647, all_74_0, % 35.75/5.54 | | | g_s90_81, simplifying with (25), (29), (30) gives: % 35.75/5.55 | | | (43) all_74_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & mem0(2147483647, % 35.75/5.55 | | | all_238_0) = v0) % 35.75/5.55 | | | % 35.75/5.55 | | | GROUND_INST: instantiating (23) with all_238_0, g_s90_81, simplifying with % 35.75/5.55 | | | (29), (30) gives: % 35.75/5.55 | | | (44) mem4(g_s90_81, all_238_0, g_s64_75) = 0 % 35.75/5.55 | | | % 35.75/5.55 | | | BETA: splitting (43) gives: % 35.75/5.55 | | | % 35.75/5.55 | | | Case 1: % 35.75/5.55 | | | | % 35.75/5.55 | | | | (45) all_74_0 = 0 % 35.75/5.55 | | | | % 35.75/5.55 | | | | REDUCE: (10), (45) imply: % 35.75/5.55 | | | | (46) $false % 35.75/5.55 | | | | % 35.75/5.55 | | | | CLOSE: (46) is inconsistent. % 35.75/5.55 | | | | % 35.75/5.55 | | | Case 2: % 35.75/5.55 | | | | % 35.75/5.55 | | | | (47) ? [v0: int] : ( ~ (v0 = 0) & mem0(2147483647, all_238_0) = v0) % 35.75/5.55 | | | | % 35.75/5.55 | | | | DELTA: instantiating (47) with fresh symbol all_344_0 gives: % 35.75/5.55 | | | | (48) ~ (all_344_0 = 0) & mem0(2147483647, all_238_0) = all_344_0 % 35.75/5.55 | | | | % 35.75/5.55 | | | | ALPHA: (48) implies: % 35.75/5.55 | | | | (49) ~ (all_344_0 = 0) % 35.75/5.55 | | | | (50) mem0(2147483647, all_238_0) = all_344_0 % 35.75/5.55 | | | | % 35.75/5.55 | | | | GROUND_INST: instantiating (4) with all_238_0, g_s90_81, 2147483647, % 35.75/5.55 | | | | all_344_0, simplifying with (29), (44), (50) gives: % 35.75/5.55 | | | | (51) all_344_0 = 0 | ? [v0: int] : ? [v1: int] : (mem2(g_s90_81, % 35.75/5.55 | | | | v1, g_s79_65) = 0 & mem2(g_s90_81, v0, g_s78_64) = 0 & ( ~ % 35.75/5.55 | | | | ($lesseq(2147483647, v1)) | ~ ($lesseq(v0, 2147483647)))) % 35.75/5.55 | | | | % 35.75/5.55 | | | | BETA: splitting (51) gives: % 35.75/5.55 | | | | % 35.75/5.55 | | | | Case 1: % 35.75/5.55 | | | | | % 35.75/5.55 | | | | | (52) all_344_0 = 0 % 35.75/5.55 | | | | | % 35.75/5.55 | | | | | REDUCE: (49), (52) imply: % 35.75/5.55 | | | | | (53) $false % 35.75/5.55 | | | | | % 35.75/5.55 | | | | | CLOSE: (53) is inconsistent. % 35.75/5.55 | | | | | % 35.75/5.55 | | | | Case 2: % 35.75/5.55 | | | | | % 36.01/5.55 | | | | | (54) ? [v0: int] : ? [v1: int] : (mem2(g_s90_81, v1, g_s79_65) = % 36.01/5.55 | | | | | 0 & mem2(g_s90_81, v0, g_s78_64) = 0 & ( ~ % 36.01/5.55 | | | | | ($lesseq(2147483647, v1)) | ~ ($lesseq(v0, 2147483647)))) % 36.01/5.55 | | | | | % 36.01/5.55 | | | | | DELTA: instantiating (54) with fresh symbols all_506_0, all_506_1 % 36.01/5.55 | | | | | gives: % 36.01/5.55 | | | | | (55) mem2(g_s90_81, all_506_0, g_s79_65) = 0 & mem2(g_s90_81, % 36.01/5.55 | | | | | all_506_1, g_s78_64) = 0 & ( ~ ($lesseq(2147483647, % 36.01/5.55 | | | | | all_506_0)) | ~ ($lesseq(all_506_1, 2147483647))) % 36.01/5.55 | | | | | % 36.01/5.55 | | | | | ALPHA: (55) implies: % 36.01/5.55 | | | | | (56) mem2(g_s90_81, all_506_1, g_s78_64) = 0 % 36.01/5.55 | | | | | (57) mem2(g_s90_81, all_506_0, g_s79_65) = 0 % 36.01/5.55 | | | | | % 36.01/5.55 | | | | | BETA: splitting (42) gives: % 36.01/5.55 | | | | | % 36.01/5.55 | | | | | Case 1: % 36.01/5.55 | | | | | | % 36.01/5.55 | | | | | | (58) all_289_4 = 0 % 36.01/5.55 | | | | | | % 36.01/5.55 | | | | | | REDUCE: (41), (58) imply: % 36.01/5.55 | | | | | | (59) mem0(all_289_5, all_95_1) = 0 % 36.01/5.55 | | | | | | % 36.01/5.55 | | | | | | GROUND_INST: instantiating (20) with all_289_5, simplifying with % 36.01/5.55 | | | | | | (59) gives: % 36.01/5.55 | | | | | | (60) $false % 36.01/5.55 | | | | | | % 36.01/5.55 | | | | | | CLOSE: (60) is inconsistent. % 36.01/5.55 | | | | | | % 36.01/5.55 | | | | | Case 2: % 36.01/5.55 | | | | | | % 36.01/5.55 | | | | | | (61) ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(1, % 36.01/5.55 | | | | | | $difference(all_289_5, v1))) | ~ (mem2(g_s90_81, v1, % 36.01/5.55 | | | | | | g_s79_65) = 0) | ~ (mem2(g_s90_81, v0, g_s78_64) = % 36.01/5.55 | | | | | | 0)) & ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(1, % 36.01/5.55 | | | | | | $difference(v0, all_289_5))) | ~ (mem2(g_s90_81, v1, % 36.01/5.55 | | | | | | g_s79_65) = 0) | ~ (mem2(g_s90_81, v0, g_s78_64) = % 36.01/5.55 | | | | | | 0)) % 36.01/5.55 | | | | | | % 36.01/5.55 | | | | | | ALPHA: (61) implies: % 36.01/5.55 | | | | | | (62) ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(1, % 36.01/5.55 | | | | | | $difference(v0, all_289_5))) | ~ (mem2(g_s90_81, v1, % 36.01/5.55 | | | | | | g_s79_65) = 0) | ~ (mem2(g_s90_81, v0, g_s78_64) = % 36.01/5.55 | | | | | | 0)) % 36.01/5.55 | | | | | | (63) ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(1, % 36.01/5.55 | | | | | | $difference(all_289_5, v1))) | ~ (mem2(g_s90_81, v1, % 36.01/5.55 | | | | | | g_s79_65) = 0) | ~ (mem2(g_s90_81, v0, g_s78_64) = % 36.01/5.55 | | | | | | 0)) % 36.01/5.55 | | | | | | % 36.01/5.55 | | | | | | GROUND_INST: instantiating (63) with all_506_1, all_90_0, % 36.01/5.55 | | | | | | simplifying with (15), (56) gives: % 36.01/5.55 | | | | | | (64) $lesseq(all_289_5, all_90_0) % 36.01/5.55 | | | | | | % 36.01/5.55 | | | | | | GROUND_INST: instantiating (62) with all_90_1, all_506_0, % 36.01/5.55 | | | | | | simplifying with (14), (57) gives: % 36.01/5.55 | | | | | | (65) $lesseq(all_90_1, all_289_5) % 36.01/5.55 | | | | | | % 36.01/5.55 | | | | | | COMBINE_INEQS: (64), (65) imply: % 36.01/5.55 | | | | | | (66) $lesseq(all_90_1, all_90_0) % 36.01/5.55 | | | | | | % 36.01/5.55 | | | | | | COMBINE_INEQS: (13), (66) imply: % 36.01/5.55 | | | | | | (67) $false % 36.01/5.55 | | | | | | % 36.01/5.55 | | | | | | CLOSE: (67) is inconsistent. % 36.01/5.55 | | | | | | % 36.01/5.55 | | | | | End of split % 36.01/5.55 | | | | | % 36.01/5.55 | | | | End of split % 36.01/5.55 | | | | % 36.01/5.55 | | | End of split % 36.01/5.55 | | | % 36.01/5.55 | | End of split % 36.01/5.55 | | % 36.01/5.56 | End of split % 36.01/5.56 | % 36.01/5.56 End of proof % 36.01/5.56 % SZS output end Proof for theBenchmark % 36.01/5.56 % 36.01/5.56 4908ms %------------------------------------------------------------------------------