%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT054+1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n009.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:57 AM UTC 2026 % Result : Theorem 0.27s 0.53s % Output : Refutation 0.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT054+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : run_spass %d %s % 0.08/0.35 % Computer : n009.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Mon Sep 7 13:24:37 UTC 2026 % 0.08/0.35 % CPUTime : % 0.27/0.53 % 0.27/0.53 SPASS V 3.9 % 0.27/0.53 SPASS beiseite: Proof found. % 0.27/0.53 % SZS status Theorem % 0.27/0.53 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.27/0.53 SPASS derived 182 clauses, backtracked 8 clauses, performed 2 splits and kept 122 clauses. % 0.27/0.53 SPASS allocated 97767 KBytes. % 0.27/0.53 SPASS spent 0:00:00.17 on the problem. % 0.27/0.53 0:00:00.06 for the input. % 0.27/0.53 0:00:00.05 for the FLOTTER CNF translation. % 0.27/0.53 0:00:00.00 for inferences. % 0.27/0.53 0:00:00.00 for the backtracking. % 0.27/0.53 0:00:00.01 for the reduction. % 0.27/0.53 % 0.27/0.53 % 0.27/0.53 Here is a proof with depth 4, length 56 : % 0.27/0.53 % SZS output start Refutation % 0.27/0.53 1[0:Inp] || -> organization(skc4)*. % 0.27/0.53 2[0:Inp] || has_endowment(skc4)* -> . % 0.27/0.53 4[0:Inp] || -> greater(age(skc4,skc7),sigma)*l. % 0.27/0.53 5[0:Inp] || -> equal(age(skc4,skc5),zero)**. % 0.27/0.53 6[0:Inp] || -> smaller_or_equal(age(skc4,skc6),sigma)*. % 0.27/0.53 7[0:Inp] || dissimilar(u,v,w)* -> organization(u). % 0.27/0.53 12[0:Inp] || smaller(u,v)* -> greater(v,u). % 0.27/0.53 14[0:Inp] || greater(hazard_of_mortality(skc4,skc7),hazard_of_mortality(skc4,skc6))*l -> . % 0.27/0.53 15[0:Inp] || greater(u,v)*+ greater(v,u)* -> . % 0.27/0.53 16[0:Inp] organization(u) || has_immunity(u,v)* -> has_endowment(u). % 0.27/0.53 18[0:Inp] || smaller_or_equal(u,v) -> equal(u,v) smaller(u,v)*. % 0.27/0.53 21[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.27/0.53 22[0:Inp] organization(u) || equal(age(u,v),zero)** -> is_aligned(u,v). % 0.27/0.53 23[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)* -> . % 0.27/0.53 24[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) dissimilar(u,v,w)*. % 0.27/0.53 26[0:Inp] organization(u) || has_immunity(u,v) -> has_immunity(u,w) greater(hazard_of_mortality(u,w),hazard_of_mortality(u,v))*. % 0.27/0.53 27[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) greater(capability(u,v),capability(u,w))*. % 0.27/0.53 28[0:Inp] organization(u) || greater(age(u,v),sigma) equal(age(u,w),zero) -> dissimilar(u,w,v)*. % 0.27/0.53 29[0:Inp] organization(u) || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.27/0.53 30[0:Inp] organization(u) || greater(capability(u,v),capability(u,w))* -> has_immunity(u,w) greater(hazard_of_mortality(u,w),hazard_of_mortality(u,v)) has_immunity(u,v). % 0.27/0.53 31[0:MRR:29.0,7.1] || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.27/0.53 32[0:MRR:30.4,26.1] organization(u) || greater(capability(u,v),capability(u,w))* -> has_immunity(u,w) greater(hazard_of_mortality(u,w),hazard_of_mortality(u,v)). % 0.27/0.53 37[0:Res:1.0,24.0] || is_aligned(skc4,u) -> is_aligned(skc4,v) dissimilar(skc4,u,v)*. % 0.27/0.53 39[0:Res:1.0,22.0] || equal(age(skc4,u),zero)** -> is_aligned(skc4,u). % 0.27/0.53 40[0:Res:1.0,16.0] || has_immunity(skc4,u)* -> has_endowment(skc4). % 0.27/0.53 42[0:Res:6.0,18.0] || -> equal(age(skc4,skc6),sigma) smaller(age(skc4,skc6),sigma)*. % 0.27/0.53 43[0:Res:5.0,31.0] || dissimilar(skc4,skc5,u)* -> greater(age(skc4,u),sigma). % 0.27/0.53 45[0:Res:5.0,22.1] organization(skc4) || -> is_aligned(skc4,skc5)*. % 0.27/0.53 54[0:Res:4.0,28.2] organization(skc4) || equal(age(skc4,u),zero) -> dissimilar(skc4,u,skc7)*. % 0.27/0.53 62[0:Res:32.3,14.0] organization(skc4) || greater(capability(skc4,skc6),capability(skc4,skc7))*r -> has_immunity(skc4,skc7). % 0.27/0.53 68[0:MRR:40.1,2.0] || has_immunity(skc4,u)* -> . % 0.27/0.53 69[0:MRR:45.0,1.0] || -> is_aligned(skc4,skc5)*. % 0.27/0.53 70[0:MRR:54.0,1.0] || equal(age(skc4,u),zero) -> dissimilar(skc4,u,skc7)*. % 0.27/0.53 72[0:MRR:62.0,62.2,1.0,68.0] || greater(capability(skc4,skc6),capability(skc4,skc7))*r -> . % 0.27/0.53 95[0:Res:42.1,12.0] || -> equal(age(skc4,skc6),sigma) greater(sigma,age(skc4,skc6))*r. % 0.27/0.53 101[0:Res:70.1,23.2] || equal(age(skc4,u),zero)** is_aligned(skc4,skc7) is_aligned(skc4,u) -> . % 0.27/0.53 104[0:MRR:101.2,39.1] || equal(age(skc4,u),zero)** is_aligned(skc4,skc7) -> . % 0.27/0.53 109[0:SpL:5.0,104.0] || equal(zero,zero) is_aligned(skc4,skc7)* -> . % 0.27/0.53 110[0:Obv:109.0] || is_aligned(skc4,skc7)* -> . % 0.27/0.53 117[1:Spt:95.0] || -> equal(age(skc4,skc6),sigma)**. % 0.27/0.53 134[0:Res:37.2,43.0] || is_aligned(skc4,skc5) -> is_aligned(skc4,u) greater(age(skc4,u),sigma)*l. % 0.27/0.53 137[0:MRR:134.0,69.0] || -> is_aligned(skc4,u) greater(age(skc4,u),sigma)*l. % 0.27/0.53 139[1:SpR:117.0,137.1] || -> is_aligned(skc4,skc6)* greater(sigma,sigma). % 0.27/0.53 151[0:Res:137.1,15.0] || greater(sigma,age(skc4,u))*r -> is_aligned(skc4,u). % 0.27/0.53 177[1:SpL:117.0,151.0] || greater(sigma,sigma) -> is_aligned(skc4,skc6)*. % 0.27/0.53 178[1:MRR:177.0,139.1] || -> is_aligned(skc4,skc6)*. % 0.27/0.53 219[0:Res:27.3,72.0] organization(skc4) || is_aligned(skc4,skc6) -> is_aligned(skc4,skc7)*. % 0.27/0.53 234[0:SSi:219.0,1.0] || is_aligned(skc4,skc6) -> is_aligned(skc4,skc7)*. % 0.27/0.53 235[1:MRR:234.0,234.1,178.0,110.0] || -> . % 0.27/0.53 240[1:Spt:235.0,95.0,117.0] || equal(age(skc4,skc6),sigma)** -> . % 0.27/0.53 241[1:Spt:235.0,95.1] || -> greater(sigma,age(skc4,skc6))*r. % 0.27/0.53 242[0:MRR:234.1,110.0] || is_aligned(skc4,skc6)* -> . % 0.27/0.53 246[1:OCh:21.1,21.0,241.0,137.1] || -> is_aligned(skc4,skc6)* greater(sigma,sigma). % 0.27/0.53 247[1:NCh:21.2,21.1,241.0,151.0] || greater(sigma,sigma) -> is_aligned(skc4,skc6)*. % 0.27/0.53 254[1:MRR:246.0,242.0] || -> greater(sigma,sigma)*. % 0.27/0.53 255[1:MRR:247.0,247.1,254.0,242.0] || -> . % 0.27/0.53 % SZS output end Refutation % 0.27/0.53 Formulae used in the proof : theorem_5 definition_2 definition_smaller meaning_postulate_greater_strict assumption_1 definition_smaller_or_equal meaning_postulate_greater_transitive assumption_13 assumption_3 assumption_14 assumption_15 assumption_16 % 0.27/0.53 %------------------------------------------------------------------------------