%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWC537_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 : 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:07:47 AM UTC 2025 % Result : Theorem 54.99s 7.90s % Output : Proof 55.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWC537_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.14/0.34 % Computer : n003.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Mon Mar 31 13:40:33 EDT 2025 % 0.14/0.34 % CPUTime : % 0.56/0.62 ________ _____ % 0.56/0.62 ___ __ \_________(_)________________________________ % 0.56/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.56/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.56/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.56/0.62 % 0.56/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.56/0.62 (2023-06-19) % 0.56/0.62 % 0.56/0.62 (c) Philipp Rümmer, 2009-2023 % 0.56/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.56/0.62 Amanda Stjerna. % 0.56/0.62 Free software under BSD-3-Clause. % 0.56/0.62 % 0.56/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.56/0.62 % 0.56/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.56/0.63 Running up to 7 provers in parallel. % 0.72/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.72/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.72/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.72/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.72/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.72/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.72/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 9.41/2.03 Prover 3: Preprocessing ... % 9.41/2.03 Prover 6: Preprocessing ... % 9.41/2.03 Prover 5: Preprocessing ... % 9.41/2.03 Prover 2: Preprocessing ... % 9.41/2.03 Prover 1: Preprocessing ... % 9.41/2.04 Prover 0: Preprocessing ... % 9.84/2.06 Prover 4: Preprocessing ... % 20.67/3.48 Prover 5: Proving ... % 20.67/3.49 Prover 2: Proving ... % 22.33/3.72 Prover 1: Warning: ignoring some quantifiers % 23.34/3.85 Prover 3: Warning: ignoring some quantifiers % 23.62/3.87 Prover 4: Warning: ignoring some quantifiers % 23.62/3.87 Prover 6: Proving ... % 23.62/3.90 Prover 3: Constructing countermodel ... % 23.62/3.92 Prover 1: Constructing countermodel ... % 24.31/3.96 Prover 4: Constructing countermodel ... % 24.31/3.98 Prover 0: Proving ... % 54.99/7.90 Prover 1: Found proof (size 78) % 54.99/7.90 Prover 1: proved (7260ms) % 54.99/7.90 Prover 3: stopped % 54.99/7.90 Prover 6: stopped % 54.99/7.90 Prover 5: stopped % 54.99/7.90 Prover 0: stopped % 54.99/7.90 Prover 4: stopped % 54.99/7.90 Prover 2: stopped % 54.99/7.90 % 54.99/7.90 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.99/7.90 % 54.99/7.91 % SZS output start Proof for theBenchmark % 54.99/7.92 Assumptions after simplification: % 54.99/7.92 --------------------------------- % 54.99/7.92 % 54.99/7.92 (Define:inv:5) % 55.60/7.94 set_2(g_s149_1_144) & set_0(g_s56_52) & set_0(g_s12_10) & ! [v0: int] : ! % 55.60/7.94 [v1: int] : ! [v2: any] : ! [v3: any] : ( ~ (mem0(v1, g_s56_52) = v2) | ~ % 55.60/7.94 (mem0(v0, g_s12_10) = v3) | ? [v4: int] : ( ~ (v4 = 0) & mem2(v1, v0, % 55.60/7.94 g_s149_1_144) = v4) | (v3 = 0 & v2 = 0)) & ! [v0: int] : ! [v1: int] : % 55.60/7.94 ! [v2: int] : (v2 = v1 | ~ (mem2(v0, v2, g_s149_1_144) = 0) | ~ (mem2(v0, % 55.60/7.94 v1, g_s149_1_144) = 0)) % 55.60/7.94 % 55.60/7.94 (Define:seext:36) % 55.60/7.94 set_2(g_s143_135) & set_0(g_s56_52) & set_0(g_s12_10) & ! [v0: int] : ! [v1: % 55.60/7.94 int] : ! [v2: any] : ! [v3: any] : ( ~ (mem0(v1, g_s56_52) = v2) | ~ % 55.60/7.94 (mem0(v0, g_s12_10) = v3) | ? [v4: int] : ( ~ (v4 = 0) & mem2(v1, v0, % 55.60/7.94 g_s143_135) = v4) | (v3 = 0 & v2 = 0)) & ! [v0: int] : ! [v1: int] : % 55.60/7.94 ! [v2: int] : (v2 = v1 | ~ (mem2(v0, v2, g_s143_135) = 0) | ~ (mem2(v0, v1, % 55.60/7.94 g_s143_135) = 0)) % 55.60/7.94 % 55.60/7.94 (Goal) % 55.60/7.94 set_2(g_s149_1_144) & set_2(g_s143_135) & set_0(g_s56_52) & set_0(g_s12_10) & % 55.60/7.94 ( ? [v0: int] : ? [v1: int] : ? [v2: int] : ? [v3: any] : ? [v4: any] : ? % 55.60/7.94 [v5: any] : ? [v6: any] : ( ~ (v2 = v1) & mem2(v0, v2, g_s149_1_144) = v6 & % 55.60/7.94 mem2(v0, v1, g_s149_1_144) = v4 & mem2(g_s157_148, v2, g_s143_135) = v5 & % 55.60/7.94 mem2(g_s157_148, v1, g_s143_135) = v3 & ((v6 = 0 & ! [v7: int] : ( ~ (v0 % 55.60/7.94 = g_s157_148) | ~ (mem2(g_s157_148, v7, g_s143_135) = 0))) | (v5 % 55.60/7.94 = 0 & v0 = g_s157_148)) & ((v4 = 0 & ! [v7: int] : ( ~ (v0 = % 55.60/7.94 g_s157_148) | ~ (mem2(g_s157_148, v7, g_s143_135) = 0))) | (v3 = % 55.60/7.94 0 & v0 = g_s157_148))) | ? [v0: int] : ? [v1: int] : ? [v2: any] : % 55.60/7.94 ? [v3: any] : ? [v4: any] : ? [v5: any] : (mem0(v1, g_s56_52) = v4 & % 55.60/7.94 mem0(v0, g_s12_10) = v5 & mem2(v1, v0, g_s149_1_144) = v3 & % 55.60/7.94 mem2(g_s157_148, v0, g_s143_135) = v2 & ( ~ (v5 = 0) | ~ (v4 = 0)) & ((v3 % 55.60/7.94 = 0 & ! [v6: int] : ( ~ (v1 = g_s157_148) | ~ (mem2(g_s157_148, v6, % 55.60/7.94 g_s143_135) = 0))) | (v2 = 0 & v1 = g_s157_148)))) % 55.60/7.94 % 55.60/7.94 (Local_Hyp:0) % 55.60/7.95 mem0(g_s157_148, g_s146_138) = 0 & set_2(g_s143_135) & set_0(g_s146_138) & ? % 55.60/7.95 [v0: int] : (mem2(g_s157_148, v0, g_s143_135) = 0) % 55.60/7.95 % 55.60/7.95 (gh_1_def) % 55.60/7.95 mem0(g_s157_148, g_s56_52) = 0 & set_0(g_s56_52) % 55.60/7.95 % 55.60/7.95 (gh_4_def) % 55.60/7.95 mem0(g_s157_148, g_s56_52) = 0 & set_0(g_s56_52) % 55.60/7.95 % 55.60/7.95 (function-axioms) % 55.60/7.95 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: set_4] : ! % 55.60/7.95 [v3: set_0] : ! [v4: int] : ! [v5: int] : (v1 = v0 | ~ (mem4(v5, v4, v3, % 55.60/7.95 v2) = v1) | ~ (mem4(v5, v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] % 55.60/7.95 : ! [v1: MultipleValueBool] : ! [v2: set_3] : ! [v3: int] : ! [v4: int] : % 55.60/7.95 ! [v5: int] : (v1 = v0 | ~ (mem3(v5, v4, v3, v2) = v1) | ~ (mem3(v5, v4, v3, % 55.60/7.95 v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : % 55.60/7.95 ! [v2: set_5] : ! [v3: set_2] : ! [v4: int] : (v1 = v0 | ~ (mem5(v4, v3, % 55.60/7.95 v2) = v1) | ~ (mem5(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 55.60/7.95 ! [v1: MultipleValueBool] : ! [v2: set_2] : ! [v3: int] : ! [v4: int] : (v1 % 55.60/7.95 = v0 | ~ (mem2(v4, v3, v2) = v1) | ~ (mem2(v4, v3, v2) = v0)) & ! [v0: % 55.60/7.95 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: set_0] : ! [v3: % 55.60/7.95 int] : (v1 = v0 | ~ (mem0(v3, v2) = v1) | ~ (mem0(v3, v2) = v0)) % 55.60/7.95 % 55.60/7.95 Further assumptions not needed in the proof: % 55.60/7.95 -------------------------------------------- % 55.60/7.95 Define:abs:0, Define:abs:1, Define:abs:2, Define:ctx:0, Define:ctx:1, % 55.60/7.95 Define:ctx:10, Define:ctx:100, Define:ctx:101, Define:ctx:102, Define:ctx:103, % 55.60/7.95 Define:ctx:104, Define:ctx:105, Define:ctx:106, Define:ctx:107, Define:ctx:108, % 55.60/7.95 Define:ctx:109, Define:ctx:11, Define:ctx:110, Define:ctx:111, Define:ctx:112, % 55.60/7.95 Define:ctx:113, Define:ctx:114, Define:ctx:115, Define:ctx:116, Define:ctx:12, % 55.60/7.95 Define:ctx:13, Define:ctx:14, Define:ctx:15, Define:ctx:16, Define:ctx:17, % 55.60/7.95 Define:ctx:18, Define:ctx:19, Define:ctx:2, Define:ctx:20, Define:ctx:21, % 55.60/7.95 Define:ctx:22, Define:ctx:23, Define:ctx:24, Define:ctx:25, Define:ctx:26, % 55.60/7.95 Define:ctx:27, Define:ctx:28, Define:ctx:29, Define:ctx:3, Define:ctx:30, % 55.60/7.95 Define:ctx:31, Define:ctx:32, Define:ctx:33, Define:ctx:34, Define:ctx:35, % 55.60/7.95 Define:ctx:36, Define:ctx:37, Define:ctx:38, Define:ctx:39, Define:ctx:4, % 55.60/7.95 Define:ctx:40, Define:ctx:41, Define:ctx:42, Define:ctx:43, Define:ctx:44, % 55.60/7.95 Define:ctx:45, Define:ctx:46, Define:ctx:47, Define:ctx:48, Define:ctx:49, % 55.60/7.95 Define:ctx:5, Define:ctx:50, Define:ctx:51, Define:ctx:52, Define:ctx:53, % 55.60/7.95 Define:ctx:54, Define:ctx:55, Define:ctx:56, Define:ctx:57, Define:ctx:58, % 55.60/7.95 Define:ctx:59, Define:ctx:6, Define:ctx:60, Define:ctx:61, Define:ctx:62, % 55.60/7.95 Define:ctx:63, Define:ctx:64, Define:ctx:65, Define:ctx:66, Define:ctx:67, % 55.60/7.95 Define:ctx:68, Define:ctx:69, Define:ctx:7, Define:ctx:70, Define:ctx:71, % 55.60/7.95 Define:ctx:72, Define:ctx:73, Define:ctx:74, Define:ctx:75, Define:ctx:76, % 55.60/7.95 Define:ctx:77, Define:ctx:78, Define:ctx:79, Define:ctx:8, Define:ctx:80, % 55.60/7.95 Define:ctx:81, Define:ctx:82, Define:ctx:83, Define:ctx:84, Define:ctx:85, % 55.60/7.95 Define:ctx:86, Define:ctx:87, Define:ctx:88, Define:ctx:89, Define:ctx:9, % 55.60/7.95 Define:ctx:90, Define:ctx:91, Define:ctx:92, Define:ctx:93, Define:ctx:94, % 55.60/7.95 Define:ctx:95, Define:ctx:96, Define:ctx:97, Define:ctx:98, Define:ctx:99, % 55.60/7.95 Define:inv:0, Define:inv:1, Define:inv:2, Define:inv:3, Define:inv:4, % 55.60/7.95 Define:seext:0, Define:seext:1, Define:seext:10, Define:seext:11, % 55.60/7.95 Define:seext:12, Define:seext:13, Define:seext:14, Define:seext:15, % 55.60/7.95 Define:seext:16, Define:seext:17, Define:seext:18, Define:seext:19, % 55.60/7.95 Define:seext:2, Define:seext:20, Define:seext:21, Define:seext:22, % 55.60/7.95 Define:seext:23, Define:seext:24, Define:seext:25, Define:seext:26, % 55.60/7.95 Define:seext:27, Define:seext:28, Define:seext:29, Define:seext:3, % 55.60/7.95 Define:seext:30, Define:seext:31, Define:seext:32, Define:seext:33, % 55.60/7.95 Define:seext:34, Define:seext:35, Define:seext:37, Define:seext:38, % 55.60/7.95 Define:seext:39, Define:seext:4, Define:seext:5, Define:seext:6, Define:seext:7, % 55.60/7.95 Define:seext:8, Define:seext:9, Local_Hyp:1, gh_0_def, gh_2_def, gh_3_def, % 55.60/7.95 gh_5_def, max_int_axiom, min_int_axiom % 55.60/7.95 % 55.60/7.95 Those formulas are unsatisfiable: % 55.60/7.95 --------------------------------- % 55.60/7.95 % 55.60/7.95 Begin of proof % 55.60/7.95 | % 55.60/7.95 | ALPHA: (Define:inv:5) implies: % 55.60/7.95 | (1) ! [v0: int] : ! [v1: int] : ! [v2: int] : (v2 = v1 | ~ (mem2(v0, % 55.60/7.95 | v2, g_s149_1_144) = 0) | ~ (mem2(v0, v1, g_s149_1_144) = 0)) % 55.60/7.96 | (2) ! [v0: int] : ! [v1: int] : ! [v2: any] : ! [v3: any] : ( ~ % 55.60/7.96 | (mem0(v1, g_s56_52) = v2) | ~ (mem0(v0, g_s12_10) = v3) | ? [v4: % 55.60/7.96 | int] : ( ~ (v4 = 0) & mem2(v1, v0, g_s149_1_144) = v4) | (v3 = 0 & % 55.60/7.96 | v2 = 0)) % 55.60/7.96 | % 55.60/7.96 | ALPHA: (Define:seext:36) implies: % 55.60/7.96 | (3) ! [v0: int] : ! [v1: int] : ! [v2: int] : (v2 = v1 | ~ (mem2(v0, % 55.60/7.96 | v2, g_s143_135) = 0) | ~ (mem2(v0, v1, g_s143_135) = 0)) % 55.60/7.96 | (4) ! [v0: int] : ! [v1: int] : ! [v2: any] : ! [v3: any] : ( ~ % 55.60/7.96 | (mem0(v1, g_s56_52) = v2) | ~ (mem0(v0, g_s12_10) = v3) | ? [v4: % 55.60/7.96 | int] : ( ~ (v4 = 0) & mem2(v1, v0, g_s143_135) = v4) | (v3 = 0 & v2 % 55.60/7.96 | = 0)) % 55.60/7.96 | % 55.60/7.96 | ALPHA: (gh_4_def) implies: % 55.60/7.96 | (5) mem0(g_s157_148, g_s56_52) = 0 % 55.60/7.96 | % 55.60/7.96 | ALPHA: (Local_Hyp:0) implies: % 55.60/7.96 | (6) ? [v0: int] : (mem2(g_s157_148, v0, g_s143_135) = 0) % 55.60/7.96 | % 55.60/7.96 | ALPHA: (Goal) implies: % 55.60/7.96 | (7) ? [v0: int] : ? [v1: int] : ? [v2: int] : ? [v3: any] : ? [v4: % 55.60/7.96 | any] : ? [v5: any] : ? [v6: any] : ( ~ (v2 = v1) & mem2(v0, v2, % 55.60/7.96 | g_s149_1_144) = v6 & mem2(v0, v1, g_s149_1_144) = v4 & % 55.60/7.96 | mem2(g_s157_148, v2, g_s143_135) = v5 & mem2(g_s157_148, v1, % 55.60/7.96 | g_s143_135) = v3 & ((v6 = 0 & ! [v7: int] : ( ~ (v0 = g_s157_148) % 55.60/7.96 | | ~ (mem2(g_s157_148, v7, g_s143_135) = 0))) | (v5 = 0 & v0 = % 55.60/7.96 | g_s157_148)) & ((v4 = 0 & ! [v7: int] : ( ~ (v0 = g_s157_148) | % 55.60/7.96 | ~ (mem2(g_s157_148, v7, g_s143_135) = 0))) | (v3 = 0 & v0 = % 55.60/7.96 | g_s157_148))) | ? [v0: int] : ? [v1: int] : ? [v2: any] : ? % 55.60/7.96 | [v3: any] : ? [v4: any] : ? [v5: any] : (mem0(v1, g_s56_52) = v4 & % 55.60/7.96 | mem0(v0, g_s12_10) = v5 & mem2(v1, v0, g_s149_1_144) = v3 & % 55.60/7.96 | mem2(g_s157_148, v0, g_s143_135) = v2 & ( ~ (v5 = 0) | ~ (v4 = 0)) & % 55.60/7.96 | ((v3 = 0 & ! [v6: int] : ( ~ (v1 = g_s157_148) | ~ % 55.60/7.96 | (mem2(g_s157_148, v6, g_s143_135) = 0))) | (v2 = 0 & v1 = % 55.60/7.96 | g_s157_148))) % 55.60/7.96 | % 55.60/7.96 | ALPHA: (function-axioms) implies: % 55.60/7.96 | (8) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 55.60/7.96 | set_0] : ! [v3: int] : (v1 = v0 | ~ (mem0(v3, v2) = v1) | ~ % 55.60/7.96 | (mem0(v3, v2) = v0)) % 55.60/7.96 | (9) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 55.60/7.96 | set_2] : ! [v3: int] : ! [v4: int] : (v1 = v0 | ~ (mem2(v4, v3, % 55.60/7.96 | v2) = v1) | ~ (mem2(v4, v3, v2) = v0)) % 55.60/7.96 | % 55.60/7.96 | DELTA: instantiating (6) with fresh symbol all_103_0 gives: % 55.60/7.96 | (10) mem2(g_s157_148, all_103_0, g_s143_135) = 0 % 55.60/7.96 | % 55.60/7.96 | BETA: splitting (7) gives: % 55.60/7.96 | % 55.60/7.96 | Case 1: % 55.60/7.96 | | % 55.60/7.97 | | (11) ? [v0: int] : ? [v1: int] : ? [v2: int] : ? [v3: any] : ? [v4: % 55.60/7.97 | | any] : ? [v5: any] : ? [v6: any] : ( ~ (v2 = v1) & mem2(v0, v2, % 55.60/7.97 | | g_s149_1_144) = v6 & mem2(v0, v1, g_s149_1_144) = v4 & % 55.60/7.97 | | mem2(g_s157_148, v2, g_s143_135) = v5 & mem2(g_s157_148, v1, % 55.60/7.97 | | g_s143_135) = v3 & ((v6 = 0 & ! [v7: int] : ( ~ (v0 = % 55.60/7.97 | | g_s157_148) | ~ (mem2(g_s157_148, v7, g_s143_135) = 0))) % 55.60/7.97 | | | (v5 = 0 & v0 = g_s157_148)) & ((v4 = 0 & ! [v7: int] : ( ~ % 55.60/7.97 | | (v0 = g_s157_148) | ~ (mem2(g_s157_148, v7, g_s143_135) = % 55.60/7.97 | | 0))) | (v3 = 0 & v0 = g_s157_148))) % 55.60/7.97 | | % 55.60/7.97 | | DELTA: instantiating (11) with fresh symbols all_843_0, all_843_1, % 55.60/7.97 | | all_843_2, all_843_3, all_843_4, all_843_5, all_843_6 gives: % 55.60/7.97 | | (12) ~ (all_843_4 = all_843_5) & mem2(all_843_6, all_843_4, % 55.60/7.97 | | g_s149_1_144) = all_843_0 & mem2(all_843_6, all_843_5, % 55.60/7.97 | | g_s149_1_144) = all_843_2 & mem2(g_s157_148, all_843_4, % 55.60/7.97 | | g_s143_135) = all_843_1 & mem2(g_s157_148, all_843_5, g_s143_135) % 55.60/7.97 | | = all_843_3 & ((all_843_0 = 0 & ! [v0: int] : ( ~ (all_843_6 = % 55.60/7.97 | | g_s157_148) | ~ (mem2(g_s157_148, v0, g_s143_135) = 0))) | % 55.60/7.97 | | (all_843_1 = 0 & all_843_6 = g_s157_148)) & ((all_843_2 = 0 & ! % 55.60/7.97 | | [v0: int] : ( ~ (all_843_6 = g_s157_148) | ~ (mem2(g_s157_148, % 55.60/7.97 | | v0, g_s143_135) = 0))) | (all_843_3 = 0 & all_843_6 = % 55.60/7.97 | | g_s157_148)) % 55.60/7.97 | | % 55.60/7.97 | | ALPHA: (12) implies: % 55.60/7.97 | | (13) ~ (all_843_4 = all_843_5) % 55.60/7.97 | | (14) mem2(g_s157_148, all_843_5, g_s143_135) = all_843_3 % 55.60/7.97 | | (15) mem2(g_s157_148, all_843_4, g_s143_135) = all_843_1 % 55.60/7.97 | | (16) mem2(all_843_6, all_843_5, g_s149_1_144) = all_843_2 % 55.60/7.97 | | (17) mem2(all_843_6, all_843_4, g_s149_1_144) = all_843_0 % 55.60/7.97 | | (18) (all_843_2 = 0 & ! [v0: int] : ( ~ (all_843_6 = g_s157_148) | ~ % 55.60/7.97 | | (mem2(g_s157_148, v0, g_s143_135) = 0))) | (all_843_3 = 0 & % 55.60/7.97 | | all_843_6 = g_s157_148) % 55.60/7.97 | | (19) (all_843_0 = 0 & ! [v0: int] : ( ~ (all_843_6 = g_s157_148) | ~ % 55.60/7.97 | | (mem2(g_s157_148, v0, g_s143_135) = 0))) | (all_843_1 = 0 & % 55.60/7.97 | | all_843_6 = g_s157_148) % 55.60/7.97 | | % 55.60/7.97 | | BETA: splitting (18) gives: % 55.60/7.97 | | % 55.60/7.97 | | Case 1: % 55.60/7.97 | | | % 55.60/7.97 | | | (20) all_843_2 = 0 & ! [v0: int] : ( ~ (all_843_6 = g_s157_148) | ~ % 55.60/7.97 | | | (mem2(g_s157_148, v0, g_s143_135) = 0)) % 55.60/7.97 | | | % 55.60/7.97 | | | ALPHA: (20) implies: % 55.60/7.97 | | | (21) all_843_2 = 0 % 55.60/7.97 | | | (22) ! [v0: int] : ( ~ (all_843_6 = g_s157_148) | ~ (mem2(g_s157_148, % 55.60/7.97 | | | v0, g_s143_135) = 0)) % 55.60/7.97 | | | % 55.60/7.97 | | | REDUCE: (16), (21) imply: % 55.60/7.97 | | | (23) mem2(all_843_6, all_843_5, g_s149_1_144) = 0 % 55.60/7.97 | | | % 55.60/7.97 | | | BETA: splitting (19) gives: % 55.60/7.97 | | | % 55.60/7.97 | | | Case 1: % 55.60/7.97 | | | | % 55.60/7.97 | | | | (24) all_843_0 = 0 & ! [v0: int] : ( ~ (all_843_6 = g_s157_148) | ~ % 55.60/7.97 | | | | (mem2(g_s157_148, v0, g_s143_135) = 0)) % 55.60/7.97 | | | | % 55.60/7.97 | | | | ALPHA: (24) implies: % 55.60/7.97 | | | | (25) all_843_0 = 0 % 55.60/7.97 | | | | % 55.60/7.97 | | | | REDUCE: (17), (25) imply: % 55.60/7.97 | | | | (26) mem2(all_843_6, all_843_4, g_s149_1_144) = 0 % 55.60/7.97 | | | | % 55.60/7.97 | | | | GROUND_INST: instantiating (1) with all_843_6, all_843_5, all_843_4, % 55.60/7.97 | | | | simplifying with (23), (26) gives: % 55.60/7.97 | | | | (27) all_843_4 = all_843_5 % 55.60/7.97 | | | | % 55.60/7.97 | | | | REDUCE: (13), (27) imply: % 55.60/7.97 | | | | (28) $false % 55.60/7.97 | | | | % 55.60/7.97 | | | | CLOSE: (28) is inconsistent. % 55.60/7.97 | | | | % 55.60/7.97 | | | Case 2: % 55.60/7.97 | | | | % 55.60/7.97 | | | | (29) all_843_1 = 0 & all_843_6 = g_s157_148 % 55.60/7.98 | | | | % 55.60/7.98 | | | | ALPHA: (29) implies: % 55.60/7.98 | | | | (30) all_843_6 = g_s157_148 % 55.60/7.98 | | | | % 55.60/7.98 | | | | GROUND_INST: instantiating (22) with all_103_0, simplifying with (10) % 55.60/7.98 | | | | gives: % 55.60/7.98 | | | | (31) ~ (all_843_6 = g_s157_148) % 55.60/7.98 | | | | % 55.60/7.98 | | | | REDUCE: (30), (31) imply: % 55.60/7.98 | | | | (32) $false % 55.60/7.98 | | | | % 55.60/7.98 | | | | CLOSE: (32) is inconsistent. % 55.60/7.98 | | | | % 55.60/7.98 | | | End of split % 55.60/7.98 | | | % 55.60/7.98 | | Case 2: % 55.60/7.98 | | | % 55.60/7.98 | | | (33) all_843_3 = 0 & all_843_6 = g_s157_148 % 55.60/7.98 | | | % 55.60/7.98 | | | ALPHA: (33) implies: % 55.60/7.98 | | | (34) all_843_6 = g_s157_148 % 55.60/7.98 | | | (35) all_843_3 = 0 % 55.60/7.98 | | | % 55.60/7.98 | | | REDUCE: (14), (35) imply: % 55.60/7.98 | | | (36) mem2(g_s157_148, all_843_5, g_s143_135) = 0 % 55.60/7.98 | | | % 55.60/7.98 | | | GROUND_INST: instantiating (3) with g_s157_148, all_103_0, all_843_5, % 55.60/7.98 | | | simplifying with (10), (36) gives: % 55.60/7.98 | | | (37) all_843_5 = all_103_0 % 55.60/7.98 | | | % 55.60/7.98 | | | REDUCE: (13), (37) imply: % 55.60/7.98 | | | (38) ~ (all_843_4 = all_103_0) % 55.60/7.98 | | | % 55.60/7.98 | | | BETA: splitting (19) gives: % 55.60/7.98 | | | % 55.60/7.98 | | | Case 1: % 55.60/7.98 | | | | % 55.60/7.98 | | | | (39) all_843_0 = 0 & ! [v0: int] : ( ~ (all_843_6 = g_s157_148) | ~ % 55.60/7.98 | | | | (mem2(g_s157_148, v0, g_s143_135) = 0)) % 55.60/7.98 | | | | % 55.60/7.98 | | | | ALPHA: (39) implies: % 55.60/7.98 | | | | (40) ! [v0: int] : ( ~ (all_843_6 = g_s157_148) | ~ % 55.60/7.98 | | | | (mem2(g_s157_148, v0, g_s143_135) = 0)) % 55.60/7.98 | | | | % 55.60/7.98 | | | | GROUND_INST: instantiating (40) with all_103_0, simplifying with (10) % 55.60/7.98 | | | | gives: % 55.60/7.98 | | | | (41) ~ (all_843_6 = g_s157_148) % 55.60/7.98 | | | | % 55.60/7.98 | | | | REDUCE: (34), (41) imply: % 55.60/7.98 | | | | (42) $false % 55.60/7.98 | | | | % 55.60/7.98 | | | | CLOSE: (42) is inconsistent. % 55.60/7.98 | | | | % 55.60/7.98 | | | Case 2: % 55.60/7.98 | | | | % 55.60/7.98 | | | | (43) all_843_1 = 0 & all_843_6 = g_s157_148 % 55.60/7.98 | | | | % 55.60/7.98 | | | | ALPHA: (43) implies: % 55.60/7.98 | | | | (44) all_843_1 = 0 % 55.60/7.98 | | | | % 55.60/7.98 | | | | REDUCE: (15), (44) imply: % 55.60/7.98 | | | | (45) mem2(g_s157_148, all_843_4, g_s143_135) = 0 % 55.60/7.98 | | | | % 55.60/7.98 | | | | GROUND_INST: instantiating (3) with g_s157_148, all_103_0, all_843_4, % 55.60/7.98 | | | | simplifying with (10), (45) gives: % 55.60/7.98 | | | | (46) all_843_4 = all_103_0 % 55.60/7.98 | | | | % 55.60/7.98 | | | | REDUCE: (38), (46) imply: % 55.60/7.98 | | | | (47) $false % 55.60/7.98 | | | | % 55.60/7.98 | | | | CLOSE: (47) is inconsistent. % 55.60/7.98 | | | | % 55.60/7.98 | | | End of split % 55.60/7.98 | | | % 55.60/7.98 | | End of split % 55.60/7.98 | | % 55.60/7.98 | Case 2: % 55.60/7.98 | | % 55.60/7.98 | | (48) ? [v0: int] : ? [v1: int] : ? [v2: any] : ? [v3: any] : ? [v4: % 55.60/7.98 | | any] : ? [v5: any] : (mem0(v1, g_s56_52) = v4 & mem0(v0, % 55.60/7.98 | | g_s12_10) = v5 & mem2(v1, v0, g_s149_1_144) = v3 & % 55.60/7.98 | | mem2(g_s157_148, v0, g_s143_135) = v2 & ( ~ (v5 = 0) | ~ (v4 = % 55.60/7.98 | | 0)) & ((v3 = 0 & ! [v6: int] : ( ~ (v1 = g_s157_148) | ~ % 55.60/7.98 | | (mem2(g_s157_148, v6, g_s143_135) = 0))) | (v2 = 0 & v1 = % 55.60/7.98 | | g_s157_148))) % 55.60/7.98 | | % 55.60/7.98 | | DELTA: instantiating (48) with fresh symbols all_843_0, all_843_1, % 55.60/7.98 | | all_843_2, all_843_3, all_843_4, all_843_5 gives: % 55.60/7.98 | | (49) mem0(all_843_4, g_s56_52) = all_843_1 & mem0(all_843_5, g_s12_10) = % 55.60/7.98 | | all_843_0 & mem2(all_843_4, all_843_5, g_s149_1_144) = all_843_2 & % 55.60/7.98 | | mem2(g_s157_148, all_843_5, g_s143_135) = all_843_3 & ( ~ (all_843_0 % 55.60/7.98 | | = 0) | ~ (all_843_1 = 0)) & ((all_843_2 = 0 & ! [v0: int] : ( % 55.60/7.98 | | ~ (all_843_4 = g_s157_148) | ~ (mem2(g_s157_148, v0, % 55.60/7.98 | | g_s143_135) = 0))) | (all_843_3 = 0 & all_843_4 = % 55.60/7.98 | | g_s157_148)) % 55.60/7.98 | | % 55.60/7.98 | | ALPHA: (49) implies: % 55.60/7.98 | | (50) mem2(g_s157_148, all_843_5, g_s143_135) = all_843_3 % 55.60/7.98 | | (51) mem2(all_843_4, all_843_5, g_s149_1_144) = all_843_2 % 55.60/7.98 | | (52) mem0(all_843_5, g_s12_10) = all_843_0 % 55.60/7.98 | | (53) mem0(all_843_4, g_s56_52) = all_843_1 % 55.60/7.98 | | (54) (all_843_2 = 0 & ! [v0: int] : ( ~ (all_843_4 = g_s157_148) | ~ % 55.60/7.98 | | (mem2(g_s157_148, v0, g_s143_135) = 0))) | (all_843_3 = 0 & % 55.60/7.98 | | all_843_4 = g_s157_148) % 55.60/7.98 | | (55) ~ (all_843_0 = 0) | ~ (all_843_1 = 0) % 55.60/7.98 | | % 55.60/7.98 | | GROUND_INST: instantiating (4) with all_843_5, g_s157_148, 0, all_843_0, % 55.60/7.98 | | simplifying with (5), (52) gives: % 55.60/7.99 | | (56) all_843_0 = 0 | ? [v0: int] : ( ~ (v0 = 0) & mem2(g_s157_148, % 55.60/7.99 | | all_843_5, g_s143_135) = v0) % 55.60/7.99 | | % 55.60/7.99 | | GROUND_INST: instantiating (2) with all_843_5, all_843_4, all_843_1, % 55.60/7.99 | | all_843_0, simplifying with (52), (53) gives: % 55.60/7.99 | | (57) ? [v0: int] : ( ~ (v0 = 0) & mem2(all_843_4, all_843_5, % 55.60/7.99 | | g_s149_1_144) = v0) | (all_843_0 = 0 & all_843_1 = 0) % 55.60/7.99 | | % 55.60/7.99 | | BETA: splitting (54) gives: % 55.60/7.99 | | % 55.60/7.99 | | Case 1: % 55.60/7.99 | | | % 55.60/7.99 | | | (58) all_843_2 = 0 & ! [v0: int] : ( ~ (all_843_4 = g_s157_148) | ~ % 55.60/7.99 | | | (mem2(g_s157_148, v0, g_s143_135) = 0)) % 55.60/7.99 | | | % 55.60/7.99 | | | ALPHA: (58) implies: % 55.60/7.99 | | | (59) all_843_2 = 0 % 55.60/7.99 | | | % 55.60/7.99 | | | REDUCE: (51), (59) imply: % 55.60/7.99 | | | (60) mem2(all_843_4, all_843_5, g_s149_1_144) = 0 % 55.60/7.99 | | | % 55.60/7.99 | | | BETA: splitting (57) gives: % 55.60/7.99 | | | % 55.60/7.99 | | | Case 1: % 55.60/7.99 | | | | % 55.60/7.99 | | | | (61) ? [v0: int] : ( ~ (v0 = 0) & mem2(all_843_4, all_843_5, % 55.60/7.99 | | | | g_s149_1_144) = v0) % 55.60/7.99 | | | | % 55.60/7.99 | | | | DELTA: instantiating (61) with fresh symbol all_1369_0 gives: % 55.60/7.99 | | | | (62) ~ (all_1369_0 = 0) & mem2(all_843_4, all_843_5, g_s149_1_144) = % 55.60/7.99 | | | | all_1369_0 % 55.60/7.99 | | | | % 55.60/7.99 | | | | ALPHA: (62) implies: % 55.60/7.99 | | | | (63) ~ (all_1369_0 = 0) % 55.60/7.99 | | | | (64) mem2(all_843_4, all_843_5, g_s149_1_144) = all_1369_0 % 55.60/7.99 | | | | % 55.60/7.99 | | | | GROUND_INST: instantiating (9) with 0, all_1369_0, g_s149_1_144, % 55.60/7.99 | | | | all_843_5, all_843_4, simplifying with (60), (64) gives: % 55.60/7.99 | | | | (65) all_1369_0 = 0 % 55.60/7.99 | | | | % 55.60/7.99 | | | | REDUCE: (63), (65) imply: % 55.60/7.99 | | | | (66) $false % 55.60/7.99 | | | | % 55.60/7.99 | | | | CLOSE: (66) is inconsistent. % 55.60/7.99 | | | | % 55.60/7.99 | | | Case 2: % 55.60/7.99 | | | | % 55.60/7.99 | | | | (67) all_843_0 = 0 & all_843_1 = 0 % 55.60/7.99 | | | | % 55.60/7.99 | | | | ALPHA: (67) implies: % 55.60/7.99 | | | | (68) all_843_1 = 0 % 55.60/7.99 | | | | (69) all_843_0 = 0 % 55.60/7.99 | | | | % 55.60/7.99 | | | | BETA: splitting (55) gives: % 55.60/7.99 | | | | % 55.60/7.99 | | | | Case 1: % 55.60/7.99 | | | | | % 55.60/7.99 | | | | | (70) ~ (all_843_0 = 0) % 55.60/7.99 | | | | | % 55.60/7.99 | | | | | REDUCE: (69), (70) imply: % 55.60/7.99 | | | | | (71) $false % 55.60/7.99 | | | | | % 55.60/7.99 | | | | | CLOSE: (71) is inconsistent. % 55.60/7.99 | | | | | % 55.60/7.99 | | | | Case 2: % 55.60/7.99 | | | | | % 55.60/7.99 | | | | | (72) ~ (all_843_1 = 0) % 55.60/7.99 | | | | | % 55.60/7.99 | | | | | REDUCE: (68), (72) imply: % 55.60/7.99 | | | | | (73) $false % 55.60/7.99 | | | | | % 55.60/7.99 | | | | | CLOSE: (73) is inconsistent. % 55.60/7.99 | | | | | % 55.60/7.99 | | | | End of split % 55.60/7.99 | | | | % 55.60/7.99 | | | End of split % 55.60/7.99 | | | % 55.60/7.99 | | Case 2: % 55.60/7.99 | | | % 55.60/7.99 | | | (74) all_843_3 = 0 & all_843_4 = g_s157_148 % 55.60/7.99 | | | % 55.60/7.99 | | | ALPHA: (74) implies: % 55.60/7.99 | | | (75) all_843_4 = g_s157_148 % 55.60/7.99 | | | (76) all_843_3 = 0 % 55.60/7.99 | | | % 55.60/7.99 | | | REDUCE: (53), (75) imply: % 55.60/7.99 | | | (77) mem0(g_s157_148, g_s56_52) = all_843_1 % 55.60/7.99 | | | % 55.60/7.99 | | | REDUCE: (50), (76) imply: % 55.60/7.99 | | | (78) mem2(g_s157_148, all_843_5, g_s143_135) = 0 % 55.60/7.99 | | | % 55.60/7.99 | | | BETA: splitting (56) gives: % 55.60/7.99 | | | % 55.60/7.99 | | | Case 1: % 55.60/7.99 | | | | % 55.60/7.99 | | | | (79) all_843_0 = 0 % 55.60/7.99 | | | | % 55.60/7.99 | | | | BETA: splitting (55) gives: % 55.60/7.99 | | | | % 55.60/7.99 | | | | Case 1: % 55.60/7.99 | | | | | % 55.60/7.99 | | | | | (80) ~ (all_843_0 = 0) % 55.60/7.99 | | | | | % 55.60/7.99 | | | | | REDUCE: (79), (80) imply: % 55.60/7.99 | | | | | (81) $false % 55.60/7.99 | | | | | % 55.60/7.99 | | | | | CLOSE: (81) is inconsistent. % 55.60/7.99 | | | | | % 55.60/7.99 | | | | Case 2: % 55.60/7.99 | | | | | % 55.60/7.99 | | | | | (82) ~ (all_843_1 = 0) % 55.60/7.99 | | | | | % 55.60/7.99 | | | | | GROUND_INST: instantiating (8) with 0, all_843_1, g_s56_52, % 55.60/7.99 | | | | | g_s157_148, simplifying with (5), (77) gives: % 55.60/7.99 | | | | | (83) all_843_1 = 0 % 55.60/7.99 | | | | | % 55.60/7.99 | | | | | REDUCE: (82), (83) imply: % 55.60/7.99 | | | | | (84) $false % 55.60/7.99 | | | | | % 55.60/7.99 | | | | | CLOSE: (84) is inconsistent. % 55.60/7.99 | | | | | % 55.60/7.99 | | | | End of split % 55.60/7.99 | | | | % 55.60/7.99 | | | Case 2: % 55.60/7.99 | | | | % 55.60/7.99 | | | | (85) ? [v0: int] : ( ~ (v0 = 0) & mem2(g_s157_148, all_843_5, % 55.60/7.99 | | | | g_s143_135) = v0) % 55.60/7.99 | | | | % 55.60/7.99 | | | | DELTA: instantiating (85) with fresh symbol all_1368_0 gives: % 55.60/7.99 | | | | (86) ~ (all_1368_0 = 0) & mem2(g_s157_148, all_843_5, g_s143_135) = % 55.60/7.99 | | | | all_1368_0 % 55.60/7.99 | | | | % 55.60/7.99 | | | | ALPHA: (86) implies: % 55.60/7.99 | | | | (87) ~ (all_1368_0 = 0) % 55.60/7.99 | | | | (88) mem2(g_s157_148, all_843_5, g_s143_135) = all_1368_0 % 55.60/7.99 | | | | % 55.60/7.99 | | | | GROUND_INST: instantiating (9) with 0, all_1368_0, g_s143_135, % 55.60/7.99 | | | | all_843_5, g_s157_148, simplifying with (78), (88) gives: % 55.60/7.99 | | | | (89) all_1368_0 = 0 % 55.60/7.99 | | | | % 55.60/7.99 | | | | REDUCE: (87), (89) imply: % 55.60/7.99 | | | | (90) $false % 55.60/7.99 | | | | % 55.60/7.99 | | | | CLOSE: (90) is inconsistent. % 55.60/7.99 | | | | % 55.60/7.99 | | | End of split % 55.60/7.99 | | | % 55.60/7.99 | | End of split % 55.60/7.99 | | % 55.60/7.99 | End of split % 55.60/7.99 | % 55.60/7.99 End of proof % 55.60/8.00 % SZS output end Proof for theBenchmark % 55.60/8.00 % 55.60/8.00 7376ms %------------------------------------------------------------------------------