%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : MGT073+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:17:29 AM UTC 2026 % Result : Theorem 21.75s 4.09s % Output : Proof 24.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : MGT073+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.06 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.18/0.43 % Computer : n015.cluster.edu % 0.18/0.43 % Model : x86_64 x86_64 % 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.43 % Memory : 8046.5625MB % 0.18/0.43 % OS : Linux 6.8.0-71-generic % 0.18/0.43 % CPULimit : 300 % 0.18/0.43 % WCLimit : 300 % 0.18/0.43 % DateTime : Mon Sep 7 14:00:15 UTC 2026 % 0.18/0.43 % CPUTime : % 0.18/0.46 OpenJDK 64-Bit Server VM warning: Options -Xverify:none and -noverify were deprecated in JDK 13 and will likely be removed in a future release. % 0.91/0.96 ________ _____ % 0.91/0.96 ___ __ \_________(_)________________________________ % 0.91/0.96 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.91/0.96 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.91/0.96 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.91/0.96 % 0.91/0.96 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.91/0.96 (2023-06-19) % 0.91/0.96 % 0.91/0.96 (c) Philipp Rümmer, 2009-2023 % 0.91/0.96 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.91/0.96 Amanda Stjerna. % 0.91/0.96 Free software under BSD-3-Clause. % 0.91/0.96 % 0.91/0.96 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.91/0.96 % 0.91/0.97 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.91/0.99 Running up to 7 provers in parallel. % 0.91/1.02 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.91/1.02 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.91/1.02 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.91/1.02 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.91/1.02 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.91/1.02 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.91/1.02 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 7.83/2.25 Prover 1: Preprocessing ... % 7.83/2.25 Prover 4: Preprocessing ... % 8.39/2.32 Prover 0: Preprocessing ... % 8.39/2.32 Prover 2: Preprocessing ... % 8.39/2.32 Prover 6: Preprocessing ... % 8.39/2.32 Prover 5: Preprocessing ... % 8.39/2.32 Prover 3: Preprocessing ... % 18.59/3.61 Prover 1: Constructing countermodel ... % 18.59/3.61 Prover 5: Proving ... % 19.39/3.72 Prover 2: Proving ... % 20.20/3.82 Prover 3: Constructing countermodel ... % 20.20/3.87 Prover 6: Proving ... % 21.75/4.04 Prover 4: Constructing countermodel ... % 21.75/4.06 Prover 0: Proving ... % 21.75/4.07 Prover 3: proved (3053ms) % 21.75/4.08 % 21.75/4.09 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 21.75/4.09 % 21.75/4.09 Prover 1: Found proof (size 13) % 21.75/4.09 Prover 1: proved (3064ms) % 21.75/4.09 Prover 2: stopped % 21.75/4.09 Prover 6: stopped % 21.75/4.09 Prover 5: stopped % 21.75/4.09 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 21.75/4.11 Prover 0: stopped % 21.75/4.11 Prover 4: stopped % 22.84/4.25 Prover 7: Preprocessing ... % 23.49/4.33 Prover 7: stopped % 23.49/4.33 % 23.49/4.33 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 23.49/4.33 % 23.49/4.34 % SZS output start Proof for theBenchmark % 23.49/4.36 Assumptions after simplification: % 23.49/4.36 --------------------------------- % 23.49/4.36 % 23.49/4.36 (axis_compatible_def) % 23.98/4.45 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: int] : (v4 = 0 % 23.98/4.45 | ~ (axis_compatible(v0, v1, v2, v3) = v4) | ~ $i(v3) | ~ $i(v2) | ~ % 23.98/4.45 $i(v1) | ~ $i(v0) | ! [v5: $i] : ( ~ (in_closed(v5, v0, v1) = 0) | ~ % 23.98/4.45 $i(v5) | ? [v6: int] : ( ~ (v6 = 0) & in_closed(v5, v2, v3) = v6))) & ! % 23.98/4.45 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ (axis_compatible(v0, % 23.98/4.46 v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ? % 23.98/4.46 [v4: $i] : (in_closed(v4, v2, v3) = 0 & in_closed(v4, v0, v1) = 0 & $i(v4))) % 23.98/4.46 % 23.98/4.46 (compatible_hyp) % 23.98/4.46 axis_compatible(n0, n10, n5, n10) = 0 & $i(n10) & $i(n5) & $i(n0) % 23.98/4.46 % 23.98/4.46 (no_false_compatible) % 23.98/4.46 $i(n10) & $i(n5) & $i(n0) & ! [v0: $i] : ( ~ (in_closed(v0, n0, n10) = 0) | % 23.98/4.46 ~ $i(v0) | ? [v1: int] : ( ~ (v1 = 0) & in_closed(v0, n5, n10) = v1)) % 23.98/4.46 % 23.98/4.47 (function-axioms) % 24.47/4.52 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 24.47/4.52 [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] % 24.47/4.52 : ! [v9: $i] : ! [v10: $i] : (v1 = v0 | ~ (in_box3(v10, v9, v8, v7, v6, v5, % 24.47/4.52 v4, v3, v2) = v1) | ~ (in_box3(v10, v9, v8, v7, v6, v5, v4, v3, v2) = % 24.47/4.52 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 24.47/4.52 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : % 24.47/4.52 ! [v8: $i] : ! [v9: $i] : (v1 = v0 | ~ (box2_conflict(v9, v8, v7, v6, v5, % 24.47/4.52 v4, v3, v2) = v1) | ~ (box2_conflict(v9, v8, v7, v6, v5, v4, v3, v2) = % 24.47/4.52 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 24.47/4.52 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : % 24.47/4.52 ! [v8: $i] : ! [v9: $i] : (v1 = v0 | ~ (box2_compatible(v9, v8, v7, v6, v5, % 24.47/4.52 v4, v3, v2) = v1) | ~ (box2_compatible(v9, v8, v7, v6, v5, v4, v3, v2) % 24.47/4.52 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 24.47/4.52 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : % 24.47/4.52 (v1 = v0 | ~ (in_box2(v7, v6, v5, v4, v3, v2) = v1) | ~ (in_box2(v7, v6, v5, % 24.47/4.52 v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 24.47/4.52 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : % 24.47/4.52 (v1 = v0 | ~ (axis_subsumes(v5, v4, v3, v2) = v1) | ~ (axis_subsumes(v5, v4, % 24.47/4.52 v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 24.47/4.52 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 24.47/4.52 (axis_compatible(v5, v4, v3, v2) = v1) | ~ (axis_compatible(v5, v4, v3, v2) % 24.47/4.52 = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 24.47/4.52 $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : (v1 = v0 | ~ % 24.47/4.52 (axis_conflict(v5, v4, v3, v2) = v1) | ~ (axis_conflict(v5, v4, v3, v2) = % 24.47/4.52 v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: % 24.47/4.52 $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (in_open(v4, v3, v2) = v1) | % 24.47/4.52 ~ (in_open(v4, v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 24.47/4.52 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ % 24.47/4.52 (in_ropen(v4, v3, v2) = v1) | ~ (in_ropen(v4, v3, v2) = v0)) & ! [v0: % 24.47/4.52 MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] % 24.47/4.52 : ! [v4: $i] : (v1 = v0 | ~ (in_lopen(v4, v3, v2) = v1) | ~ (in_lopen(v4, % 24.47/4.52 v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] % 24.47/4.52 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (in_closed(v4, v3, % 24.47/4.52 v2) = v1) | ~ (in_closed(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 24.47/4.52 : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (box_verdict(v3, v2) = v1) | ~ % 24.47/4.52 (box_verdict(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 24.47/4.52 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (leq(v3, v2) % 24.47/4.52 = v1) | ~ (leq(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 24.47/4.52 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (less(v3, v2) % 24.47/4.52 = v1) | ~ (less(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 24.47/4.52 MultipleValueBool] : ! [v2: $i] : (v1 = v0 | ~ (is_verdict(v2) = v1) | ~ % 24.47/4.52 (is_verdict(v2) = v0)) % 24.47/4.52 % 24.47/4.52 Further assumptions not needed in the proof: % 24.47/4.52 -------------------------------------------- % 24.47/4.53 axis_conflict_def, axis_subsumes_def, box2_conflict, box2_overlap, % 24.47/4.53 box_compatible, box_conflict, box_unknown, box_verdict_total, % 24.47/4.53 compatible_is_verdict, conflict_is_verdict, in_box2, in_box3, in_closed, % 24.47/4.53 in_lopen, in_open, in_ropen, irreflexive, leq_antisym, leq_def, leq_less_trans, % 24.47/4.53 leq_trans, less_implies_leq, less_leq_trans, order_0_5, order_5_10, % 24.47/4.53 shape_closed, shape_lopen, shape_open, shape_point, shape_ropen, transitive, % 24.47/4.53 trichotomy, unknown_is_verdict, verdict_enum, verdicts_distinct_cf_cp, % 24.47/4.53 verdicts_distinct_cf_un, verdicts_distinct_cp_un % 24.47/4.53 % 24.47/4.53 Those formulas are unsatisfiable: % 24.47/4.53 --------------------------------- % 24.47/4.53 % 24.47/4.53 Begin of proof % 24.47/4.53 | % 24.47/4.53 | ALPHA: (axis_compatible_def) implies: % 24.47/4.54 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 24.47/4.54 | (axis_compatible(v0, v1, v2, v3) = 0) | ~ $i(v3) | ~ $i(v2) | ~ % 24.47/4.54 | $i(v1) | ~ $i(v0) | ? [v4: $i] : (in_closed(v4, v2, v3) = 0 & % 24.47/4.54 | in_closed(v4, v0, v1) = 0 & $i(v4))) % 24.47/4.54 | % 24.47/4.54 | ALPHA: (compatible_hyp) implies: % 24.47/4.54 | (2) axis_compatible(n0, n10, n5, n10) = 0 % 24.47/4.54 | % 24.47/4.54 | ALPHA: (no_false_compatible) implies: % 24.47/4.54 | (3) $i(n0) % 24.47/4.54 | (4) $i(n5) % 24.47/4.55 | (5) $i(n10) % 24.47/4.55 | (6) ! [v0: $i] : ( ~ (in_closed(v0, n0, n10) = 0) | ~ $i(v0) | ? [v1: % 24.47/4.55 | int] : ( ~ (v1 = 0) & in_closed(v0, n5, n10) = v1)) % 24.47/4.55 | % 24.47/4.55 | ALPHA: (function-axioms) implies: % 24.47/4.55 | (7) ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : % 24.47/4.55 | ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (in_closed(v4, v3, v2) = v1) % 24.47/4.55 | | ~ (in_closed(v4, v3, v2) = v0)) % 24.47/4.55 | % 24.47/4.56 | GROUND_INST: instantiating (1) with n0, n10, n5, n10, simplifying with (2), % 24.47/4.56 | (3), (4), (5) gives: % 24.47/4.56 | (8) ? [v0: $i] : (in_closed(v0, n5, n10) = 0 & in_closed(v0, n0, n10) = 0 % 24.47/4.56 | & $i(v0)) % 24.47/4.56 | % 24.47/4.56 | DELTA: instantiating (8) with fresh symbol all_40_0 gives: % 24.47/4.57 | (9) in_closed(all_40_0, n5, n10) = 0 & in_closed(all_40_0, n0, n10) = 0 & % 24.47/4.57 | $i(all_40_0) % 24.47/4.57 | % 24.47/4.57 | ALPHA: (9) implies: % 24.47/4.57 | (10) $i(all_40_0) % 24.47/4.57 | (11) in_closed(all_40_0, n0, n10) = 0 % 24.47/4.57 | (12) in_closed(all_40_0, n5, n10) = 0 % 24.47/4.57 | % 24.47/4.57 | GROUND_INST: instantiating (6) with all_40_0, simplifying with (10), (11) % 24.47/4.57 | gives: % 24.47/4.57 | (13) ? [v0: int] : ( ~ (v0 = 0) & in_closed(all_40_0, n5, n10) = v0) % 24.47/4.57 | % 24.47/4.57 | DELTA: instantiating (13) with fresh symbol all_47_0 gives: % 24.47/4.57 | (14) ~ (all_47_0 = 0) & in_closed(all_40_0, n5, n10) = all_47_0 % 24.47/4.57 | % 24.47/4.57 | ALPHA: (14) implies: % 24.47/4.57 | (15) ~ (all_47_0 = 0) % 24.47/4.57 | (16) in_closed(all_40_0, n5, n10) = all_47_0 % 24.47/4.57 | % 24.47/4.58 | GROUND_INST: instantiating (7) with 0, all_47_0, n10, n5, all_40_0, % 24.47/4.58 | simplifying with (12), (16) gives: % 24.47/4.58 | (17) all_47_0 = 0 % 24.47/4.58 | % 24.47/4.58 | REDUCE: (15), (17) imply: % 24.47/4.58 | (18) $false % 24.47/4.58 | % 24.47/4.58 | CLOSE: (18) is inconsistent. % 24.47/4.58 | % 24.47/4.58 End of proof % 24.47/4.58 % SZS output end Proof for theBenchmark % 24.47/4.58 % 24.47/4.58 3613ms %------------------------------------------------------------------------------