%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT062-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n003.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:19:58 AM UTC 2026 % Result : Unsatisfiable 0.23s 0.50s % Output : Refutation 0.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT062-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.11/0.37 % Computer : n003.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Mon Sep 7 13:39:54 UTC 2026 % 0.11/0.37 % CPUTime : % 0.23/0.50 % 0.23/0.50 SPASS V 3.9 % 0.23/0.50 SPASS beiseite: Proof found. % 0.23/0.50 % SZS status Theorem % 0.23/0.50 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.23/0.50 SPASS derived 179 clauses, backtracked 0 clauses, performed 1 splits and kept 105 clauses. % 0.23/0.50 SPASS allocated 75786 KBytes. % 0.23/0.50 SPASS spent 0:00:00.12 on the problem. % 0.23/0.50 0:00:00.06 for the input. % 0.23/0.50 0:00:00.00 for the FLOTTER CNF translation. % 0.23/0.50 0:00:00.00 for inferences. % 0.23/0.50 0:00:00.00 for the backtracking. % 0.23/0.50 0:00:00.01 for the reduction. % 0.23/0.50 % 0.23/0.50 % 0.23/0.50 Here is a proof with depth 5, length 67 : % 0.23/0.50 % SZS output start Refutation % 0.23/0.50 1[0:Inp] organization(u) || has_immunity(u,v)* -> has_endowment(u). % 0.23/0.50 2[0:Inp] || dissimilar(u,v,w)* -> organization(u). % 0.23/0.50 4[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)* -> . % 0.23/0.50 6[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) dissimilar(u,v,w)*. % 0.23/0.50 9[0:Inp] organization(u) || equal(age(u,v),zero)** -> is_aligned(u,v). % 0.23/0.50 10[0:Inp] organization(u) || greater(age(u,v),sigma) equal(age(u,w),zero) -> dissimilar(u,w,v)*. % 0.23/0.50 11[0:Inp] organization(u) || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.23/0.51 12[0:Inp] robust_position(u) || smaller_or_equal(age(u,v),tau)* positional_advantage(u,v) -> . % 0.23/0.51 13[0:Inp] robust_position(u) || greater(age(u,v),tau)*l -> positional_advantage(u,v). % 0.23/0.51 20[0:Inp] organization(u) || positional_advantage(u,v) -> is_aligned(u,v) has_immunity(u,v) equal(hazard_of_mortality(u,v),mod1)**. % 0.23/0.51 21[0:Inp] organization(u) || is_aligned(u,v) -> positional_advantage(u,v) has_immunity(u,v) equal(hazard_of_mortality(u,v),mod2)**. % 0.23/0.51 23[0:Inp] || -> greater(mod2,mod1)*l. % 0.23/0.51 24[0:Inp] || -> organization(sk2)*. % 0.23/0.51 25[0:Inp] || -> robust_position(sk2)*. % 0.23/0.51 26[0:Inp] || has_endowment(sk2)* -> . % 0.23/0.51 27[0:Inp] || -> equal(age(sk2,sk3),zero)**. % 0.23/0.51 29[0:Inp] || -> greater(tau,zero)*l. % 0.23/0.51 30[0:Inp] || -> equal(tau,sigma)**. % 0.23/0.51 31[0:Inp] || -> smaller_or_equal(age(sk2,sk4),sigma)*. % 0.23/0.51 32[0:Inp] || -> greater(age(sk2,sk5),sigma)*l. % 0.23/0.51 33[0:Inp] || equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3)) smaller(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))* -> . % 0.23/0.51 35[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 0.23/0.51 41[0:Inp] || greater(u,v) -> smaller(v,u)*. % 0.23/0.51 45[0:Rew:30.0,29.0] || -> greater(sigma,zero)*l. % 0.23/0.51 47[0:Rew:30.0,12.1] robust_position(u) || positional_advantage(u,v) smaller_or_equal(age(u,v),sigma)* -> . % 0.23/0.51 49[0:Rew:30.0,13.1] robust_position(u) || greater(age(u,v),sigma)*l -> positional_advantage(u,v). % 0.23/0.51 51[0:MRR:11.0,2.1] || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.23/0.51 52[0:Res:25.0,49.0] || greater(age(sk2,u),sigma)*l -> positional_advantage(sk2,u). % 0.23/0.51 53[0:Res:25.0,47.0] || positional_advantage(sk2,u) smaller_or_equal(age(sk2,u),sigma)* -> . % 0.23/0.51 56[0:Res:24.0,20.0] || positional_advantage(sk2,u) -> has_immunity(sk2,u) is_aligned(sk2,u) equal(hazard_of_mortality(sk2,u),mod1)**. % 0.23/0.51 57[0:Res:24.0,21.0] || is_aligned(sk2,u) -> has_immunity(sk2,u) positional_advantage(sk2,u) equal(hazard_of_mortality(sk2,u),mod2)**. % 0.23/0.51 59[0:Res:24.0,6.0] || is_aligned(sk2,u) -> is_aligned(sk2,v) dissimilar(sk2,u,v)*. % 0.23/0.51 61[0:Res:24.0,9.0] || equal(age(sk2,u),zero)** -> is_aligned(sk2,u). % 0.23/0.51 63[0:Res:24.0,1.0] || has_immunity(sk2,u)* -> has_endowment(sk2). % 0.23/0.51 69[0:Res:31.0,47.1] robust_position(sk2) || positional_advantage(sk2,sk4)* -> . % 0.23/0.51 71[0:Res:27.0,51.0] || dissimilar(sk2,sk3,u)* -> greater(age(sk2,u),sigma). % 0.23/0.51 73[0:Res:27.0,9.1] organization(sk2) || -> is_aligned(sk2,sk3)*. % 0.23/0.51 80[0:Res:45.0,41.0] || -> smaller(zero,sigma)*. % 0.23/0.51 83[0:Res:32.0,10.2] organization(sk2) || equal(age(sk2,u),zero) -> dissimilar(sk2,u,sk5)*. % 0.23/0.51 100[0:MRR:63.1,26.0] || has_immunity(sk2,u)* -> . % 0.23/0.51 101[0:MRR:73.0,24.0] || -> is_aligned(sk2,sk3)*. % 0.23/0.51 103[0:MRR:69.0,25.0] || positional_advantage(sk2,sk4)* -> . % 0.23/0.51 104[0:MRR:83.0,24.0] || equal(age(sk2,u),zero) -> dissimilar(sk2,u,sk5)*. % 0.23/0.51 106[0:MRR:56.1,100.0] || positional_advantage(sk2,u) -> is_aligned(sk2,u) equal(hazard_of_mortality(sk2,u),mod1)**. % 0.23/0.51 107[0:MRR:57.1,100.0] || is_aligned(sk2,u) -> positional_advantage(sk2,u) equal(hazard_of_mortality(sk2,u),mod2)**. % 0.23/0.51 112[0:Res:80.0,35.0] || -> smaller_or_equal(zero,sigma)*. % 0.23/0.51 118[0:SpL:27.0,53.1] || positional_advantage(sk2,sk3)* smaller_or_equal(zero,sigma) -> . % 0.23/0.51 121[0:MRR:118.1,112.0] || positional_advantage(sk2,sk3)* -> . % 0.23/0.51 161[0:Res:104.1,4.2] || equal(age(sk2,u),zero)** is_aligned(sk2,sk5) is_aligned(sk2,u) -> . % 0.23/0.51 164[0:MRR:161.2,61.1] || equal(age(sk2,u),zero)** is_aligned(sk2,sk5) -> . % 0.23/0.51 168[0:SpL:27.0,164.0] || equal(zero,zero) is_aligned(sk2,sk5)* -> . % 0.23/0.51 169[0:Obv:168.0] || is_aligned(sk2,sk5)* -> . % 0.23/0.51 214[0:Res:59.2,71.0] || is_aligned(sk2,sk3) -> is_aligned(sk2,u) greater(age(sk2,u),sigma)*l. % 0.23/0.51 217[0:MRR:214.0,101.0] || -> is_aligned(sk2,u) greater(age(sk2,u),sigma)*l. % 0.23/0.51 220[0:Res:217.1,52.0] || -> is_aligned(sk2,u) positional_advantage(sk2,u)*. % 0.23/0.51 223[0:MRR:107.0,220.0] || -> positional_advantage(sk2,u) equal(hazard_of_mortality(sk2,u),mod2)**. % 0.23/0.51 224[0:MRR:106.0,220.1] || -> is_aligned(sk2,u) equal(hazard_of_mortality(sk2,u),mod1)**. % 0.23/0.51 239[0:SpL:223.1,33.1] || equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3)) smaller(hazard_of_mortality(sk2,sk5),mod2)* -> positional_advantage(sk2,sk4). % 0.23/0.51 241[0:Rew:223.1,239.0] || equal(hazard_of_mortality(sk2,sk3),mod2) smaller(hazard_of_mortality(sk2,sk5),mod2)* -> positional_advantage(sk2,sk4). % 0.23/0.51 242[0:MRR:241.2,103.0] || equal(hazard_of_mortality(sk2,sk3),mod2) smaller(hazard_of_mortality(sk2,sk5),mod2)* -> . % 0.23/0.51 256[0:SpL:224.1,242.1] || equal(hazard_of_mortality(sk2,sk3),mod2)** smaller(mod1,mod2) -> is_aligned(sk2,sk5). % 0.23/0.51 263[0:MRR:256.2,169.0] || equal(hazard_of_mortality(sk2,sk3),mod2)** smaller(mod1,mod2) -> . % 0.23/0.51 265[0:SpL:223.1,263.0] || equal(mod2,mod2) smaller(mod1,mod2)* -> positional_advantage(sk2,sk3). % 0.23/0.51 268[0:Obv:265.0] || smaller(mod1,mod2)* -> positional_advantage(sk2,sk3). % 0.23/0.51 269[0:MRR:268.1,121.0] || smaller(mod1,mod2)* -> . % 0.23/0.51 272[0:Res:41.1,269.0] || greater(mod2,mod1)*l -> . % 0.23/0.51 273[0:MRR:272.0,23.0] || -> . % 0.23/0.51 % SZS output end Refutation % 0.23/0.51 Formulae used in the proof : assumption_1_39 definition_2_40 definition_2_42 definition_2_44 assumption_13_47 assumption_15_48 assumption_15_49 definition_4_50 definition_4_51 assumption_17_58 assumption_17_59 assumption_19_61 theorem_8_62 theorem_8_63 theorem_8_64 theorem_8_65 theorem_8_67 theorem_8_68 theorem_8_69 theorem_8_70 theorem_8_71 definition_smaller_or_equal_2 definition_smaller_8 % 0.23/0.51 %------------------------------------------------------------------------------