%------------------------------------------------------------------------------ % 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 : n016.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 : Unsatisfiable 0.20s 0.48s % Output : Refutation 0.20s % 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.09/0.34 % Computer : n016.cluster.edu % 0.09/0.34 % Model : x86_64 x86_64 % 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.34 % Memory : 8046.5625MB % 0.09/0.34 % OS : Linux 6.8.0-71-generic % 0.09/0.34 % CPULimit : 300 % 0.09/0.34 % WCLimit : 300 % 0.09/0.34 % DateTime : Mon Sep 7 13:29:47 UTC 2026 % 0.09/0.34 % CPUTime : % 0.20/0.48 % 0.20/0.48 SPASS V 3.9 % 0.20/0.48 SPASS beiseite: Proof found. % 0.20/0.48 % SZS status Theorem % 0.20/0.48 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.48 SPASS derived 182 clauses, backtracked 8 clauses, performed 2 splits and kept 122 clauses. % 0.20/0.48 SPASS allocated 75795 KBytes. % 0.20/0.48 SPASS spent 0:00:00.12 on the problem. % 0.20/0.48 0:00:00.06 for the input. % 0.20/0.48 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.48 0:00:00.00 for inferences. % 0.20/0.48 0:00:00.00 for the backtracking. % 0.20/0.48 0:00:00.01 for the reduction. % 0.20/0.48 % 0.20/0.48 % 0.20/0.48 Here is a proof with depth 4, length 56 : % 0.20/0.48 % SZS output start Refutation % 0.20/0.48 1[0:Inp] organization(u) || has_immunity(u,v)* -> has_endowment(u). % 0.20/0.48 2[0:Inp] organization(u) || has_immunity(u,v) -> has_immunity(u,w) greater(hazard_of_mortality(u,w),hazard_of_mortality(u,v))*. % 0.20/0.48 3[0:Inp] || dissimilar(u,v,w)* -> organization(u). % 0.20/0.48 5[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)* -> . % 0.20/0.48 7[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) dissimilar(u,v,w)*. % 0.20/0.48 10[0:Inp] organization(u) || equal(age(u,v),zero)** -> is_aligned(u,v). % 0.20/0.48 11[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) greater(capability(u,v),capability(u,w))*. % 0.20/0.48 12[0:Inp] organization(u) || greater(age(u,v),sigma) equal(age(u,w),zero) -> dissimilar(u,w,v)*. % 0.20/0.48 13[0:Inp] organization(u) || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.20/0.48 14[0:Inp] organization(u) || greater(capability(u,v),capability(u,w))* -> has_immunity(u,w) has_immunity(u,v) greater(hazard_of_mortality(u,w),hazard_of_mortality(u,v)). % 0.20/0.48 15[0:Inp] || -> organization(sk1)*. % 0.20/0.48 16[0:Inp] || has_endowment(sk1)* -> . % 0.20/0.48 17[0:Inp] || -> equal(age(sk1,sk2),zero)**. % 0.20/0.48 18[0:Inp] || -> smaller_or_equal(age(sk1,sk3),sigma)*. % 0.20/0.48 19[0:Inp] || -> greater(age(sk1,sk4),sigma)*l. % 0.20/0.48 21[0:Inp] || greater(hazard_of_mortality(sk1,sk4),hazard_of_mortality(sk1,sk3))*l -> . % 0.20/0.48 22[0:Inp] || smaller_or_equal(u,v) -> equal(u,v) smaller(u,v)*. % 0.20/0.48 28[0:Inp] || smaller(u,v)* -> greater(v,u). % 0.20/0.48 30[0:Inp] || greater(u,v)*+ greater(v,u)* -> . % 0.20/0.48 31[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.20/0.48 33[0:MRR:13.0,3.1] || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.20/0.48 34[0:MRR:14.3,2.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.20/0.48 39[0:Res:15.0,7.0] || is_aligned(sk1,u) -> is_aligned(sk1,v) dissimilar(sk1,u,v)*. % 0.20/0.48 41[0:Res:15.0,10.0] || equal(age(sk1,u),zero)** -> is_aligned(sk1,u). % 0.20/0.48 42[0:Res:15.0,1.0] || has_immunity(sk1,u)* -> has_endowment(sk1). % 0.20/0.48 44[0:Res:18.0,22.0] || -> equal(age(sk1,sk3),sigma) smaller(age(sk1,sk3),sigma)*. % 0.20/0.48 45[0:Res:17.0,33.0] || dissimilar(sk1,sk2,u)* -> greater(age(sk1,u),sigma). % 0.20/0.48 47[0:Res:17.0,10.1] organization(sk1) || -> is_aligned(sk1,sk2)*. % 0.20/0.48 56[0:Res:19.0,12.2] organization(sk1) || equal(age(sk1,u),zero) -> dissimilar(sk1,u,sk4)*. % 0.20/0.48 64[0:Res:34.3,21.0] organization(sk1) || greater(capability(sk1,sk3),capability(sk1,sk4))*r -> has_immunity(sk1,sk4). % 0.20/0.48 70[0:MRR:42.1,16.0] || has_immunity(sk1,u)* -> . % 0.20/0.48 71[0:MRR:47.0,15.0] || -> is_aligned(sk1,sk2)*. % 0.20/0.48 72[0:MRR:56.0,15.0] || equal(age(sk1,u),zero) -> dissimilar(sk1,u,sk4)*. % 0.20/0.48 74[0:MRR:64.0,64.2,15.0,70.0] || greater(capability(sk1,sk3),capability(sk1,sk4))*r -> . % 0.20/0.48 97[0:Res:44.1,28.0] || -> equal(age(sk1,sk3),sigma) greater(sigma,age(sk1,sk3))*r. % 0.20/0.48 103[0:Res:72.1,5.2] || equal(age(sk1,u),zero)** is_aligned(sk1,sk4) is_aligned(sk1,u) -> . % 0.20/0.48 106[0:MRR:103.2,41.1] || equal(age(sk1,u),zero)** is_aligned(sk1,sk4) -> . % 0.20/0.48 111[0:SpL:17.0,106.0] || equal(zero,zero) is_aligned(sk1,sk4)* -> . % 0.20/0.48 112[0:Obv:111.0] || is_aligned(sk1,sk4)* -> . % 0.20/0.48 119[1:Spt:97.0] || -> equal(age(sk1,sk3),sigma)**. % 0.20/0.48 136[0:Res:39.2,45.0] || is_aligned(sk1,sk2) -> is_aligned(sk1,u) greater(age(sk1,u),sigma)*l. % 0.20/0.48 139[0:MRR:136.0,71.0] || -> is_aligned(sk1,u) greater(age(sk1,u),sigma)*l. % 0.20/0.48 141[1:SpR:119.0,139.1] || -> is_aligned(sk1,sk3)* greater(sigma,sigma). % 0.20/0.48 153[0:Res:139.1,30.0] || greater(sigma,age(sk1,u))*r -> is_aligned(sk1,u). % 0.20/0.48 179[1:SpL:119.0,153.0] || greater(sigma,sigma) -> is_aligned(sk1,sk3)*. % 0.20/0.48 180[1:MRR:179.0,141.1] || -> is_aligned(sk1,sk3)*. % 0.20/0.48 221[0:Res:11.3,74.0] organization(sk1) || is_aligned(sk1,sk3) -> is_aligned(sk1,sk4)*. % 0.20/0.48 236[0:SSi:221.0,15.0] || is_aligned(sk1,sk3) -> is_aligned(sk1,sk4)*. % 0.20/0.48 237[1:MRR:236.0,236.1,180.0,112.0] || -> . % 0.20/0.48 242[1:Spt:237.0,97.0,119.0] || equal(age(sk1,sk3),sigma)** -> . % 0.20/0.48 243[1:Spt:237.0,97.1] || -> greater(sigma,age(sk1,sk3))*r. % 0.20/0.48 244[0:MRR:236.1,112.0] || is_aligned(sk1,sk3)* -> . % 0.20/0.48 248[1:OCh:31.1,31.0,243.0,139.1] || -> is_aligned(sk1,sk3)* greater(sigma,sigma). % 0.20/0.48 249[1:NCh:31.2,31.1,243.0,153.0] || greater(sigma,sigma) -> is_aligned(sk1,sk3)*. % 0.20/0.48 256[1:MRR:248.0,244.0] || -> greater(sigma,sigma)*. % 0.20/0.48 257[1:MRR:249.0,249.1,256.0,244.0] || -> . % 0.20/0.48 % SZS output end Refutation % 0.20/0.48 Formulae used in the proof : assumption_1_38 assumption_3_39 definition_2_40 definition_2_42 definition_2_44 assumption_13_47 assumption_14_48 assumption_15_49 assumption_15_50 assumption_16_51 theorem_5_52 theorem_5_53 theorem_5_54 theorem_5_55 theorem_5_56 theorem_5_58 definition_smaller_or_equal_1 definition_smaller_7 meaning_postulate_greater_strict_9 meaning_postulate_greater_transitive_10 % 0.20/0.48 %------------------------------------------------------------------------------