%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWC539_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 : n026.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 27.33s 4.28s % Output : Proof 35.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWC539_1 : TPTP v9.0.0. Bugfixed v9.1.0. % 0.11/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.32 % Computer : n026.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Mon Mar 31 13:41:37 EDT 2025 % 0.12/0.32 % CPUTime : % 0.60/0.58 ________ _____ % 0.60/0.58 ___ __ \_________(_)________________________________ % 0.60/0.58 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.60/0.58 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.60/0.58 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.60/0.58 % 0.60/0.58 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.60/0.58 (2023-06-19) % 0.60/0.58 % 0.60/0.58 (c) Philipp Rümmer, 2009-2023 % 0.60/0.58 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.60/0.58 Amanda Stjerna. % 0.60/0.58 Free software under BSD-3-Clause. % 0.60/0.58 % 0.60/0.58 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.60/0.58 % 0.60/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.60/0.59 Running up to 7 provers in parallel. % 0.66/0.61 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.66/0.61 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.66/0.61 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.66/0.61 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.66/0.61 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.66/0.61 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.66/0.61 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 7.94/1.81 Prover 4: Preprocessing ... % 8.75/1.91 Prover 1: Preprocessing ... % 9.32/1.96 Prover 3: Preprocessing ... % 9.32/1.96 Prover 5: Preprocessing ... % 9.32/1.96 Prover 6: Preprocessing ... % 9.32/1.96 Prover 2: Preprocessing ... % 9.32/1.96 Prover 0: Preprocessing ... % 18.60/3.12 Prover 5: Proving ... % 19.10/3.25 Prover 2: Proving ... % 20.23/3.41 Prover 6: Proving ... % 20.90/3.44 Prover 1: Warning: ignoring some quantifiers % 20.90/3.45 Prover 3: Warning: ignoring some quantifiers % 21.40/3.51 Prover 3: Constructing countermodel ... % 21.40/3.53 Prover 4: Warning: ignoring some quantifiers % 22.00/3.57 Prover 1: Constructing countermodel ... % 22.66/3.70 Prover 0: Proving ... % 23.25/3.74 Prover 4: Constructing countermodel ... % 27.33/4.28 Prover 0: proved (3674ms) % 27.33/4.28 % 27.33/4.28 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 27.33/4.28 % 27.33/4.28 Prover 2: stopped % 27.33/4.28 Prover 5: stopped % 27.33/4.28 Prover 3: stopped % 27.33/4.30 Prover 6: stopped % 27.81/4.32 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 27.81/4.32 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 27.81/4.32 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 27.81/4.32 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 27.81/4.32 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 31.61/4.80 Prover 4: Found proof (size 11) % 31.61/4.81 Prover 4: proved (4203ms) % 31.61/4.81 Prover 1: stopped % 31.61/4.81 Prover 7: Preprocessing ... % 31.86/4.87 Prover 8: Preprocessing ... % 31.86/4.87 Prover 10: Preprocessing ... % 31.86/4.88 Prover 13: Preprocessing ... % 31.86/4.89 Prover 11: Preprocessing ... % 32.93/4.97 Prover 7: stopped % 32.93/4.99 Prover 10: stopped % 32.93/5.04 Prover 13: stopped % 33.70/5.09 Prover 11: stopped % 34.49/5.35 Prover 8: Warning: ignoring some quantifiers % 34.94/5.39 Prover 8: Constructing countermodel ... % 35.03/5.41 Prover 8: stopped % 35.03/5.41 % 35.03/5.41 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 35.03/5.41 % 35.03/5.41 % SZS output start Proof for theBenchmark % 35.12/5.42 Assumptions after simplification: % 35.12/5.42 --------------------------------- % 35.12/5.43 % 35.12/5.43 (Define:imprp:14) % 35.12/5.46 set_2(g_s104_89) & set_0(g_s65_65) & set_0(g_s6_6) & ? [v0: set_2] : % 35.12/5.46 (set_2(v0) & ! [v1: int] : ! [v2: int] : ! [v3: int] : (v3 = v2 | ~ % 35.12/5.46 (mem2(v1, v3, v0) = 0) | ~ (mem2(v1, v2, v0) = 0)) & ! [v1: int] : ! % 35.12/5.46 [v2: int] : ! [v3: int] : (v3 = 0 | ~ (mem2(v2, v1, v0) = v3) | ? [v4: % 35.12/5.46 int] : ( ~ (v4 = 0) & mem2(v2, v1, g_s104_89) = v4)) & ! [v1: int] : ! % 35.12/5.46 [v2: int] : ! [v3: int] : (v3 = 0 | ~ (mem2(v2, v1, g_s104_89) = v3) | ? % 35.12/5.46 [v4: int] : ( ~ (v4 = 0) & mem2(v2, v1, v0) = v4)) & ! [v1: int] : ! % 35.12/5.46 [v2: int] : ! [v3: int] : (v2 = 0 | ~ (mem2(v3, v1, v0) = 0) | ~ % 35.12/5.46 (mem0(v1, g_s6_6) = v2)) & ! [v1: int] : ! [v2: int] : ! [v3: int] : % 35.12/5.46 (v2 = 0 | ~ (mem2(v1, v3, v0) = 0) | ~ (mem0(v1, g_s65_65) = v2)) & ! % 35.12/5.46 [v1: int] : ! [v2: int] : ( ~ (mem2(v2, v1, v0) = 0) | mem2(v2, v1, % 35.12/5.46 g_s104_89) = 0) & ! [v1: int] : ! [v2: int] : ( ~ (mem2(v2, v1, % 35.12/5.46 g_s104_89) = 0) | mem2(v2, v1, v0) = 0) & ! [v1: int] : ( ~ (mem0(v1, % 35.12/5.46 g_s65_65) = 0) | ? [v2: int] : (mem2(v1, v2, v0) = 0))) % 35.12/5.46 % 35.12/5.46 (Goal) % 35.12/5.47 set_2(g_s104_89) & set_0(g_s66_66) & set_0(g_s37_37) & ? [v0: int] : ? [v1: % 35.12/5.47 int] : ? [v2: int] : ( ~ (v2 = v1) & mem2(v0, v2, g_s104_89) = 0 & mem2(v0, % 35.12/5.47 v1, g_s104_89) = 0 & mem0(v2, g_s37_37) = 0 & mem0(v1, g_s37_37) = 0 & % 35.12/5.47 mem0(v0, g_s66_66) = 0) % 35.12/5.47 % 35.12/5.47 Further assumptions not needed in the proof: % 35.12/5.47 -------------------------------------------- % 35.12/5.47 Define:ctx:0, Define:ctx:1, Define:ctx:10, Define:ctx:100, Define:ctx:101, % 35.12/5.47 Define:ctx:102, Define:ctx:103, Define:ctx:104, Define:ctx:105, Define:ctx:106, % 35.12/5.47 Define:ctx:107, Define:ctx:108, Define:ctx:109, Define:ctx:11, Define:ctx:110, % 35.12/5.47 Define:ctx:111, Define:ctx:112, Define:ctx:113, Define:ctx:114, Define:ctx:115, % 35.12/5.47 Define:ctx:116, Define:ctx:117, Define:ctx:12, Define:ctx:13, Define:ctx:14, % 35.12/5.47 Define:ctx:15, Define:ctx:16, Define:ctx:17, Define:ctx:18, Define:ctx:19, % 35.12/5.47 Define:ctx:2, Define:ctx:20, Define:ctx:21, Define:ctx:22, Define:ctx:23, % 35.12/5.47 Define:ctx:24, Define:ctx:25, Define:ctx:26, Define:ctx:27, Define:ctx:28, % 35.12/5.47 Define:ctx:29, Define:ctx:3, Define:ctx:30, Define:ctx:31, Define:ctx:32, % 35.12/5.47 Define:ctx:33, Define:ctx:34, Define:ctx:35, Define:ctx:36, Define:ctx:37, % 35.12/5.47 Define:ctx:38, Define:ctx:39, Define:ctx:4, Define:ctx:40, Define:ctx:41, % 35.12/5.47 Define:ctx:42, Define:ctx:43, Define:ctx:44, Define:ctx:45, Define:ctx:46, % 35.12/5.47 Define:ctx:47, Define:ctx:48, Define:ctx:49, Define:ctx:5, Define:ctx:50, % 35.12/5.47 Define:ctx:51, Define:ctx:52, Define:ctx:53, Define:ctx:54, Define:ctx:55, % 35.12/5.47 Define:ctx:56, Define:ctx:57, Define:ctx:58, Define:ctx:59, Define:ctx:6, % 35.12/5.47 Define:ctx:60, Define:ctx:61, Define:ctx:62, Define:ctx:63, Define:ctx:64, % 35.12/5.47 Define:ctx:65, Define:ctx:66, Define:ctx:67, Define:ctx:68, Define:ctx:69, % 35.12/5.47 Define:ctx:7, Define:ctx:70, Define:ctx:71, Define:ctx:72, Define:ctx:73, % 35.12/5.47 Define:ctx:74, Define:ctx:75, Define:ctx:76, Define:ctx:77, Define:ctx:78, % 35.12/5.47 Define:ctx:79, Define:ctx:8, Define:ctx:80, Define:ctx:81, Define:ctx:82, % 35.12/5.47 Define:ctx:83, Define:ctx:84, Define:ctx:85, Define:ctx:86, Define:ctx:87, % 35.12/5.47 Define:ctx:88, Define:ctx:89, Define:ctx:9, Define:ctx:90, Define:ctx:91, % 35.12/5.47 Define:ctx:92, Define:ctx:93, Define:ctx:94, Define:ctx:95, Define:ctx:96, % 35.12/5.47 Define:ctx:97, Define:ctx:98, Define:ctx:99, Define:imprp:0, Define:imprp:1, % 35.12/5.47 Define:imprp:10, Define:imprp:11, Define:imprp:12, Define:imprp:13, % 35.12/5.47 Define:imprp:15, Define:imprp:16, Define:imprp:17, Define:imprp:18, % 35.12/5.47 Define:imprp:2, Define:imprp:3, Define:imprp:4, Define:imprp:5, Define:imprp:6, % 35.12/5.47 Define:imprp:7, Define:imprp:8, Define:imprp:9, max_int_axiom, min_int_axiom % 35.12/5.47 % 35.12/5.47 Those formulas are unsatisfiable: % 35.12/5.47 --------------------------------- % 35.12/5.47 % 35.12/5.47 Begin of proof % 35.12/5.47 | % 35.12/5.47 | ALPHA: (Define:imprp:14) implies: % 35.12/5.48 | (1) ? [v0: set_2] : (set_2(v0) & ! [v1: int] : ! [v2: int] : ! [v3: % 35.12/5.48 | int] : (v3 = v2 | ~ (mem2(v1, v3, v0) = 0) | ~ (mem2(v1, v2, v0) % 35.12/5.48 | = 0)) & ! [v1: int] : ! [v2: int] : ! [v3: int] : (v3 = 0 | ~ % 35.12/5.48 | (mem2(v2, v1, v0) = v3) | ? [v4: int] : ( ~ (v4 = 0) & mem2(v2, % 35.12/5.48 | v1, g_s104_89) = v4)) & ! [v1: int] : ! [v2: int] : ! [v3: % 35.12/5.48 | int] : (v3 = 0 | ~ (mem2(v2, v1, g_s104_89) = v3) | ? [v4: int] : % 35.12/5.48 | ( ~ (v4 = 0) & mem2(v2, v1, v0) = v4)) & ! [v1: int] : ! [v2: % 35.12/5.48 | int] : ! [v3: int] : (v2 = 0 | ~ (mem2(v3, v1, v0) = 0) | ~ % 35.12/5.48 | (mem0(v1, g_s6_6) = v2)) & ! [v1: int] : ! [v2: int] : ! [v3: % 35.12/5.48 | int] : (v2 = 0 | ~ (mem2(v1, v3, v0) = 0) | ~ (mem0(v1, g_s65_65) % 35.12/5.48 | = v2)) & ! [v1: int] : ! [v2: int] : ( ~ (mem2(v2, v1, v0) = 0) % 35.12/5.48 | | mem2(v2, v1, g_s104_89) = 0) & ! [v1: int] : ! [v2: int] : ( ~ % 35.12/5.48 | (mem2(v2, v1, g_s104_89) = 0) | mem2(v2, v1, v0) = 0) & ! [v1: % 35.12/5.48 | int] : ( ~ (mem0(v1, g_s65_65) = 0) | ? [v2: int] : (mem2(v1, v2, % 35.12/5.48 | v0) = 0))) % 35.12/5.48 | % 35.12/5.48 | ALPHA: (Goal) implies: % 35.12/5.48 | (2) ? [v0: int] : ? [v1: int] : ? [v2: int] : ( ~ (v2 = v1) & mem2(v0, % 35.12/5.48 | v2, g_s104_89) = 0 & mem2(v0, v1, g_s104_89) = 0 & mem0(v2, % 35.12/5.48 | g_s37_37) = 0 & mem0(v1, g_s37_37) = 0 & mem0(v0, g_s66_66) = 0) % 35.12/5.48 | % 35.12/5.48 | DELTA: instantiating (2) with fresh symbols all_91_0, all_91_1, all_91_2 % 35.12/5.48 | gives: % 35.12/5.49 | (3) ~ (all_91_0 = all_91_1) & mem2(all_91_2, all_91_0, g_s104_89) = 0 & % 35.12/5.49 | mem2(all_91_2, all_91_1, g_s104_89) = 0 & mem0(all_91_0, g_s37_37) = 0 % 35.12/5.49 | & mem0(all_91_1, g_s37_37) = 0 & mem0(all_91_2, g_s66_66) = 0 % 35.12/5.49 | % 35.12/5.49 | ALPHA: (3) implies: % 35.12/5.49 | (4) ~ (all_91_0 = all_91_1) % 35.12/5.49 | (5) mem2(all_91_2, all_91_1, g_s104_89) = 0 % 35.12/5.49 | (6) mem2(all_91_2, all_91_0, g_s104_89) = 0 % 35.12/5.49 | % 35.12/5.49 | DELTA: instantiating (1) with fresh symbol all_135_0 gives: % 35.12/5.49 | (7) set_2(all_135_0) & ! [v0: int] : ! [v1: int] : ! [v2: int] : (v2 = % 35.12/5.49 | v1 | ~ (mem2(v0, v2, all_135_0) = 0) | ~ (mem2(v0, v1, all_135_0) = % 35.12/5.49 | 0)) & ! [v0: int] : ! [v1: int] : ! [v2: int] : (v2 = 0 | ~ % 35.12/5.50 | (mem2(v1, v0, all_135_0) = v2) | ? [v3: int] : ( ~ (v3 = 0) & % 35.12/5.50 | mem2(v1, v0, g_s104_89) = v3)) & ! [v0: int] : ! [v1: int] : ! % 35.12/5.50 | [v2: int] : (v2 = 0 | ~ (mem2(v1, v0, g_s104_89) = v2) | ? [v3: int] % 35.12/5.50 | : ( ~ (v3 = 0) & mem2(v1, v0, all_135_0) = v3)) & ! [v0: int] : ! % 35.12/5.50 | [v1: int] : ! [v2: int] : (v1 = 0 | ~ (mem2(v2, v0, all_135_0) = 0) | % 35.12/5.50 | ~ (mem0(v0, g_s6_6) = v1)) & ! [v0: int] : ! [v1: int] : ! [v2: % 35.12/5.50 | int] : (v1 = 0 | ~ (mem2(v0, v2, all_135_0) = 0) | ~ (mem0(v0, % 35.12/5.50 | g_s65_65) = v1)) & ! [v0: int] : ! [v1: int] : ( ~ (mem2(v1, % 35.12/5.50 | v0, all_135_0) = 0) | mem2(v1, v0, g_s104_89) = 0) & ! [v0: int] % 35.12/5.50 | : ! [v1: int] : ( ~ (mem2(v1, v0, g_s104_89) = 0) | mem2(v1, v0, % 35.12/5.50 | all_135_0) = 0) & ! [v0: int] : ( ~ (mem0(v0, g_s65_65) = 0) | ? % 35.12/5.50 | [v1: int] : (mem2(v0, v1, all_135_0) = 0)) % 35.12/5.50 | % 35.12/5.50 | ALPHA: (7) implies: % 35.12/5.50 | (8) ! [v0: int] : ! [v1: int] : ( ~ (mem2(v1, v0, g_s104_89) = 0) | % 35.12/5.50 | mem2(v1, v0, all_135_0) = 0) % 35.49/5.50 | (9) ! [v0: int] : ! [v1: int] : ! [v2: int] : (v2 = v1 | ~ (mem2(v0, % 35.49/5.50 | v2, all_135_0) = 0) | ~ (mem2(v0, v1, all_135_0) = 0)) % 35.49/5.50 | % 35.49/5.50 | GROUND_INST: instantiating (8) with all_91_1, all_91_2, simplifying with (5) % 35.49/5.50 | gives: % 35.49/5.50 | (10) mem2(all_91_2, all_91_1, all_135_0) = 0 % 35.49/5.50 | % 35.49/5.50 | GROUND_INST: instantiating (8) with all_91_0, all_91_2, simplifying with (6) % 35.49/5.50 | gives: % 35.49/5.50 | (11) mem2(all_91_2, all_91_0, all_135_0) = 0 % 35.49/5.50 | % 35.49/5.50 | GROUND_INST: instantiating (9) with all_91_2, all_91_1, all_91_0, simplifying % 35.49/5.50 | with (10), (11) gives: % 35.49/5.50 | (12) all_91_0 = all_91_1 % 35.49/5.50 | % 35.49/5.50 | REDUCE: (4), (12) imply: % 35.49/5.50 | (13) $false % 35.49/5.50 | % 35.49/5.50 | CLOSE: (13) is inconsistent. % 35.49/5.50 | % 35.49/5.50 End of proof % 35.49/5.50 % SZS output end Proof for theBenchmark % 35.49/5.50 % 35.49/5.50 4924ms %------------------------------------------------------------------------------