%------------------------------------------------------------------------------ % 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 : n018.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 : Theorem 0.22s 0.56s % Output : Refutation 0.22s % 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.09/0.36 % Computer : n018.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Mon Sep 7 13:38:52 UTC 2026 % 0.09/0.36 % CPUTime : % 0.22/0.56 % 0.22/0.56 SPASS V 3.9 % 0.22/0.56 SPASS beiseite: Proof found. % 0.22/0.56 % SZS status Theorem % 0.22/0.56 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.22/0.56 SPASS derived 220 clauses, backtracked 11 clauses, performed 1 splits and kept 122 clauses. % 0.22/0.56 SPASS allocated 97833 KBytes. % 0.22/0.56 SPASS spent 0:00:00.17 on the problem. % 0.22/0.56 0:00:00.06 for the input. % 0.22/0.56 0:00:00.05 for the FLOTTER CNF translation. % 0.22/0.56 0:00:00.00 for inferences. % 0.22/0.56 0:00:00.00 for the backtracking. % 0.22/0.56 0:00:00.01 for the reduction. % 0.22/0.56 % 0.22/0.56 % 0.22/0.56 Here is a proof with depth 5, length 67 : % 0.22/0.56 % SZS output start Refutation % 0.22/0.56 1[0:Inp] || -> robust_position(skc4)*. % 0.22/0.56 2[0:Inp] || -> organization(skc4)*. % 0.22/0.56 3[0:Inp] || has_endowment(skc4)* -> . % 0.22/0.56 5[0:Inp] || -> greater(tau,zero)*l. % 0.22/0.56 6[0:Inp] || -> equal(tau,sigma)**. % 0.22/0.56 7[0:Inp] || -> greater(mod2,mod1)*l. % 0.22/0.56 8[0:Inp] || -> greater(age(skc4,skc7),sigma)*l. % 0.22/0.56 9[0:Inp] || -> smaller_or_equal(age(skc4,skc6),sigma)*. % 0.22/0.56 10[0:Inp] || -> equal(age(skc4,skc5),zero)**. % 0.22/0.56 11[0:Inp] || dissimilar(u,v,w)* -> organization(u). % 0.22/0.56 12[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 0.22/0.56 17[0:Inp] || greater(u,v) -> smaller(v,u)*. % 0.22/0.56 19[0:Inp] organization(u) || has_immunity(u,v)* -> has_endowment(u). % 0.22/0.56 26[0:Inp] organization(u) || equal(age(u,v),zero)** -> is_aligned(u,v). % 0.22/0.56 27[0:Inp] robust_position(u) || greater(age(u,v),tau)*l -> positional_advantage(u,v). % 0.22/0.56 30[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)* -> . % 0.22/0.56 31[0:Inp] robust_position(u) || positional_advantage(u,v) smaller_or_equal(age(u,v),tau)* -> . % 0.22/0.56 33[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) dissimilar(u,v,w)*. % 0.22/0.56 36[0:Inp] || equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5)) smaller(hazard_of_mortality(skc4,skc7),hazard_of_mortality(skc4,skc6))* -> . % 0.22/0.56 38[0:Inp] organization(u) || positional_advantage(u,v) -> has_immunity(u,v) is_aligned(u,v) equal(hazard_of_mortality(u,v),mod1)**. % 0.22/0.56 39[0:Inp] organization(u) || is_aligned(u,v) -> has_immunity(u,v) positional_advantage(u,v) equal(hazard_of_mortality(u,v),mod2)**. % 0.22/0.56 40[0:Inp] organization(u) || greater(age(u,v),sigma) equal(age(u,w),zero) -> dissimilar(u,w,v)*. % 0.22/0.56 41[0:Inp] organization(u) || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.22/0.56 43[0:Rew:6.0,5.0] || -> greater(sigma,zero)*l. % 0.22/0.56 45[0:Rew:6.0,31.2] robust_position(u) || positional_advantage(u,v) smaller_or_equal(age(u,v),sigma)* -> . % 0.22/0.56 47[0:Rew:6.0,27.1] robust_position(u) || greater(age(u,v),sigma)*l -> positional_advantage(u,v). % 0.22/0.56 49[0:MRR:41.0,11.1] || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.22/0.56 52[0:Res:2.0,38.0] || positional_advantage(skc4,u) -> is_aligned(skc4,u) equal(hazard_of_mortality(skc4,u),mod1)** has_immunity(skc4,u). % 0.22/0.56 53[0:Res:2.0,39.0] || is_aligned(skc4,u) -> positional_advantage(skc4,u) equal(hazard_of_mortality(skc4,u),mod2)** has_immunity(skc4,u). % 0.22/0.56 55[0:Res:2.0,33.0] || is_aligned(skc4,u) -> is_aligned(skc4,v) dissimilar(skc4,u,v)*. % 0.22/0.56 57[0:Res:2.0,26.0] || equal(age(skc4,u),zero)** -> is_aligned(skc4,u). % 0.22/0.56 59[0:Res:2.0,19.0] || has_immunity(skc4,u)* -> has_endowment(skc4). % 0.22/0.56 60[0:Res:1.0,47.0] || greater(age(skc4,u),sigma)*l -> positional_advantage(skc4,u). % 0.22/0.56 61[0:Res:1.0,45.0] || positional_advantage(skc4,u) smaller_or_equal(age(skc4,u),sigma)* -> . % 0.22/0.56 67[0:Res:10.0,49.0] || dissimilar(skc4,skc5,u)* -> greater(age(skc4,u),sigma). % 0.22/0.56 69[0:Res:10.0,26.1] organization(skc4) || -> is_aligned(skc4,skc5)*. % 0.22/0.56 74[0:Res:9.0,45.2] robust_position(skc4) || positional_advantage(skc4,skc6)* -> . % 0.22/0.56 78[0:Res:43.0,17.0] || -> smaller(zero,sigma)*. % 0.22/0.56 81[0:Res:8.0,40.2] organization(skc4) || equal(age(skc4,u),zero) -> dissimilar(skc4,u,skc7)*. % 0.22/0.56 98[0:MRR:59.1,3.0] || has_immunity(skc4,u)* -> . % 0.22/0.56 99[0:MRR:69.0,2.0] || -> is_aligned(skc4,skc5)*. % 0.22/0.56 101[0:MRR:74.0,1.0] || positional_advantage(skc4,skc6)* -> . % 0.22/0.56 102[0:MRR:81.0,2.0] || equal(age(skc4,u),zero) -> dissimilar(skc4,u,skc7)*. % 0.22/0.56 104[0:MRR:52.3,98.0] || positional_advantage(skc4,u) -> is_aligned(skc4,u) equal(hazard_of_mortality(skc4,u),mod1)**. % 0.22/0.56 105[0:MRR:53.3,98.0] || is_aligned(skc4,u) -> positional_advantage(skc4,u) equal(hazard_of_mortality(skc4,u),mod2)**. % 0.22/0.56 110[0:Res:78.0,12.0] || -> smaller_or_equal(zero,sigma)*. % 0.22/0.56 116[0:SpL:10.0,61.1] || positional_advantage(skc4,skc5)* smaller_or_equal(zero,sigma) -> . % 0.22/0.56 119[0:MRR:116.1,110.0] || positional_advantage(skc4,skc5)* -> . % 0.22/0.56 158[0:Res:102.1,30.2] || equal(age(skc4,u),zero)** is_aligned(skc4,skc7) is_aligned(skc4,u) -> . % 0.22/0.56 161[0:MRR:158.2,57.1] || equal(age(skc4,u),zero)** is_aligned(skc4,skc7) -> . % 0.22/0.56 162[0:SpL:10.0,161.0] || equal(zero,zero) is_aligned(skc4,skc7)* -> . % 0.22/0.56 163[0:Obv:162.0] || is_aligned(skc4,skc7)* -> . % 0.22/0.56 211[0:Res:55.2,67.0] || is_aligned(skc4,skc5) -> is_aligned(skc4,u) greater(age(skc4,u),sigma)*l. % 0.22/0.56 214[0:MRR:211.0,99.0] || -> is_aligned(skc4,u) greater(age(skc4,u),sigma)*l. % 0.22/0.56 235[0:Res:214.1,60.0] || -> is_aligned(skc4,u) positional_advantage(skc4,u)*. % 0.22/0.56 238[0:MRR:105.0,235.0] || -> positional_advantage(skc4,u) equal(hazard_of_mortality(skc4,u),mod2)**. % 0.22/0.56 239[0:MRR:104.0,235.1] || -> is_aligned(skc4,u) equal(hazard_of_mortality(skc4,u),mod1)**. % 0.22/0.56 249[0:SpL:238.1,36.1] || equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5)) smaller(hazard_of_mortality(skc4,skc7),mod2)* -> positional_advantage(skc4,skc6). % 0.22/0.56 251[0:Rew:238.1,249.0] || equal(hazard_of_mortality(skc4,skc5),mod2) smaller(hazard_of_mortality(skc4,skc7),mod2)* -> positional_advantage(skc4,skc6). % 0.22/0.56 283[0:MRR:251.2,101.0] || equal(hazard_of_mortality(skc4,skc5),mod2) smaller(hazard_of_mortality(skc4,skc7),mod2)* -> . % 0.22/0.56 290[0:SpL:239.1,283.1] || equal(hazard_of_mortality(skc4,skc5),mod2)** smaller(mod1,mod2) -> is_aligned(skc4,skc7). % 0.22/0.56 297[0:MRR:290.2,163.0] || equal(hazard_of_mortality(skc4,skc5),mod2)** smaller(mod1,mod2) -> . % 0.22/0.56 314[0:SpL:238.1,297.0] || equal(mod2,mod2) smaller(mod1,mod2)* -> positional_advantage(skc4,skc5). % 0.22/0.56 317[0:Obv:314.0] || smaller(mod1,mod2)* -> positional_advantage(skc4,skc5). % 0.22/0.56 318[0:MRR:317.1,119.0] || smaller(mod1,mod2)* -> . % 0.22/0.56 321[0:Res:17.1,318.0] || greater(mod2,mod1)*l -> . % 0.22/0.56 322[0:MRR:321.0,7.0] || -> . % 0.22/0.56 % SZS output end Refutation % 0.22/0.56 Formulae used in the proof : theorem_8 assumption_19 definition_2 definition_smaller_or_equal definition_smaller assumption_1 assumption_13 definition_4 assumption_17 assumption_15 % 0.22/0.56 %------------------------------------------------------------------------------