%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT061-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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.97s 1.21s % Output : Refutation 0.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT061-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.10/0.35 % Computer : n011.cluster.edu % 0.10/0.35 % Model : x86_64 x86_64 % 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.35 % Memory : 8046.5625MB % 0.10/0.35 % OS : Linux 6.8.0-71-generic % 0.10/0.35 % CPULimit : 300 % 0.10/0.35 % WCLimit : 300 % 0.10/0.35 % DateTime : Mon Sep 7 13:36:15 UTC 2026 % 0.10/0.36 % CPUTime : % 0.97/1.21 % 0.97/1.21 SPASS V 3.9 % 0.97/1.21 SPASS beiseite: Proof found. % 0.97/1.21 % SZS status Theorem % 0.97/1.21 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.97/1.21 SPASS derived 3894 clauses, backtracked 0 clauses, performed 4 splits and kept 1257 clauses. % 0.97/1.21 SPASS allocated 78210 KBytes. % 0.97/1.21 SPASS spent 0:00:00.82 on the problem. % 0.97/1.21 0:00:00.06 for the input. % 0.97/1.21 0:00:00.00 for the FLOTTER CNF translation. % 0.97/1.21 0:00:00.08 for inferences. % 0.97/1.21 0:00:00.01 for the backtracking. % 0.97/1.21 0:00:00.61 for the reduction. % 0.97/1.21 % 0.97/1.21 % 0.97/1.21 Here is a proof with depth 4, length 64 : % 0.97/1.21 % SZS output start Refutation % 0.97/1.21 1[0:Inp] organization(u) || has_immunity(u,v)* -> has_endowment(u). % 0.97/1.21 2[0:Inp] || dissimilar(u,v,w)* -> organization(u). % 0.97/1.21 4[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)* -> . % 0.97/1.21 6[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) dissimilar(u,v,w)*. % 0.97/1.21 9[0:Inp] organization(u) || equal(age(u,v),zero)** -> is_aligned(u,v). % 0.97/1.21 10[0:Inp] organization(u) || greater(age(u,v),sigma) equal(age(u,w),zero) -> dissimilar(u,w,v)*. % 0.97/1.21 11[0:Inp] organization(u) || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.97/1.21 12[0:Inp] fragile_position(u) || smaller_or_equal(age(u,v),sigma)* -> positional_advantage(u,v). % 0.97/1.21 13[0:Inp] fragile_position(u) || positional_advantage(u,v) greater(age(u,v),sigma)*l -> . % 0.97/1.21 19[0:Inp] organization(u) || positional_advantage(u,v) is_aligned(u,v) -> has_immunity(u,v) equal(hazard_of_mortality(u,v),low)**. % 0.97/1.21 22[0:Inp] organization(u) || -> positional_advantage(u,v) is_aligned(u,v) has_immunity(u,v) equal(hazard_of_mortality(u,v),high)**. % 0.97/1.21 26[0:Inp] || -> greater(high,mod2)*l. % 0.97/1.21 27[0:Inp] || -> greater(mod2,low)*l. % 0.97/1.21 28[0:Inp] || -> organization(sk2)*. % 0.97/1.21 29[0:Inp] || -> fragile_position(sk2)*. % 0.97/1.21 30[0:Inp] || has_endowment(sk2)* -> . % 0.97/1.21 31[0:Inp] || -> equal(age(sk2,sk3),zero)**. % 0.97/1.21 32[0:Inp] || -> greater(sigma,zero)*l. % 0.97/1.21 33[0:Inp] || -> smaller_or_equal(age(sk2,sk4),sigma)*. % 0.97/1.21 34[0:Inp] || -> greater(age(sk2,sk5),sigma)*l. % 0.97/1.21 35[0:Inp] || equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3)) greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))*l -> . % 0.97/1.21 37[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 0.97/1.21 43[0:Inp] || greater(u,v) -> smaller(v,u)*. % 0.97/1.21 45[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.97/1.21 47[0:MRR:11.0,2.1] || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.97/1.21 48[0:Res:29.0,13.0] || positional_advantage(sk2,u) greater(age(sk2,u),sigma)*l -> . % 0.97/1.21 49[0:Res:29.0,12.0] || smaller_or_equal(age(sk2,u),sigma)* -> positional_advantage(sk2,u). % 0.97/1.21 51[0:Res:28.0,19.0] || is_aligned(sk2,u) positional_advantage(sk2,u) -> has_immunity(sk2,u) equal(hazard_of_mortality(sk2,u),low)**. % 0.97/1.21 54[0:Res:28.0,22.0] || -> has_immunity(sk2,u) is_aligned(sk2,u) positional_advantage(sk2,u) equal(hazard_of_mortality(sk2,u),high)**. % 0.97/1.21 55[0:Res:28.0,6.0] || is_aligned(sk2,u) -> is_aligned(sk2,v) dissimilar(sk2,u,v)*. % 0.97/1.21 59[0:Res:28.0,1.0] || has_immunity(sk2,u)* -> has_endowment(sk2). % 0.97/1.21 61[0:Res:33.0,12.1] fragile_position(sk2) || -> positional_advantage(sk2,sk4)*. % 0.97/1.21 63[0:Res:31.0,47.0] || dissimilar(sk2,sk3,u)* -> greater(age(sk2,u),sigma). % 0.97/1.21 65[0:Res:31.0,9.1] organization(sk2) || -> is_aligned(sk2,sk3)*. % 0.97/1.21 72[0:Res:32.0,43.0] || -> smaller(zero,sigma)*. % 0.97/1.21 75[0:Res:34.0,10.2] organization(sk2) || equal(age(sk2,u),zero) -> dissimilar(sk2,u,sk5)*. % 0.97/1.21 84[0:MRR:59.1,30.0] || has_immunity(sk2,u)* -> . % 0.97/1.21 85[0:MRR:61.0,29.0] || -> positional_advantage(sk2,sk4)*. % 0.97/1.21 86[0:MRR:65.0,28.0] || -> is_aligned(sk2,sk3)*. % 0.97/1.21 88[0:MRR:75.0,28.0] || equal(age(sk2,u),zero) -> dissimilar(sk2,u,sk5)*. % 0.97/1.21 89[0:MRR:54.0,84.0] || -> positional_advantage(sk2,u) is_aligned(sk2,u) equal(hazard_of_mortality(sk2,u),high)**. % 0.97/1.21 92[0:MRR:51.2,84.0] || positional_advantage(sk2,u) is_aligned(sk2,u) -> equal(hazard_of_mortality(sk2,u),low)**. % 0.97/1.21 95[0:Res:31.0,88.0] || -> dissimilar(sk2,sk3,sk5)*. % 0.97/1.21 102[0:Res:72.0,37.0] || -> smaller_or_equal(zero,sigma)*. % 0.97/1.21 105[0:SpL:31.0,49.0] || smaller_or_equal(zero,sigma) -> positional_advantage(sk2,sk3)*. % 0.97/1.21 108[0:MRR:105.0,102.0] || -> positional_advantage(sk2,sk3)*. % 0.97/1.21 148[0:Res:95.0,4.2] || is_aligned(sk2,sk5)* is_aligned(sk2,sk3) -> . % 0.97/1.21 152[0:MRR:148.1,86.0] || is_aligned(sk2,sk5)* -> . % 0.97/1.21 190[0:Res:55.2,63.0] || is_aligned(sk2,sk3) -> is_aligned(sk2,u) greater(age(sk2,u),sigma)*l. % 0.97/1.21 195[0:MRR:190.0,86.0] || -> is_aligned(sk2,u) greater(age(sk2,u),sigma)*l. % 0.97/1.21 206[0:Res:195.1,48.1] || positional_advantage(sk2,u)* -> is_aligned(sk2,u). % 0.97/1.21 214[0:MRR:89.0,206.0] || -> is_aligned(sk2,u) equal(hazard_of_mortality(sk2,u),high)**. % 0.97/1.21 215[0:MRR:92.1,206.1] || positional_advantage(sk2,u) -> equal(hazard_of_mortality(sk2,u),low)**. % 0.97/1.21 385[0:SpL:214.1,35.1] || equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3)) greater(high,hazard_of_mortality(sk2,sk4))*r -> is_aligned(sk2,sk5). % 0.97/1.21 391[0:MRR:385.2,152.0] || equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3)) greater(high,hazard_of_mortality(sk2,sk4))*r -> . % 0.97/1.21 953[0:CRe:45.0,26.0] || greater(mod2,u)*+ -> greater(high,u)*. % 0.97/1.21 1233[0:Res:27.0,953.0] || -> greater(high,low)*l. % 0.97/1.21 4095[0:SpL:215.1,391.1] || positional_advantage(sk2,sk4) equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3))** greater(high,low) -> . % 0.97/1.21 4106[0:Rew:215.1,4095.1] || positional_advantage(sk2,sk4) equal(hazard_of_mortality(sk2,sk3),low)** greater(high,low) -> . % 0.97/1.21 4107[0:MRR:4106.0,4106.2,85.0,1233.0] || equal(hazard_of_mortality(sk2,sk3),low)** -> . % 0.97/1.21 4111[0:SpL:19.4,4107.0] organization(sk2) || positional_advantage(sk2,sk3) is_aligned(sk2,sk3) equal(low,low) -> has_immunity(sk2,sk3)*. % 0.97/1.21 4118[0:Obv:4111.3] organization(sk2) || positional_advantage(sk2,sk3) is_aligned(sk2,sk3) -> has_immunity(sk2,sk3)*. % 0.97/1.21 4119[0:SSi:4118.0,29.0,28.0] || positional_advantage(sk2,sk3) is_aligned(sk2,sk3) -> has_immunity(sk2,sk3)*. % 0.97/1.21 4120[0:MRR:4119.0,4119.1,4119.2,108.0,86.0,84.0] || -> . % 0.97/1.21 % SZS output end Refutation % 0.97/1.21 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_3_50 definition_3_51 assumption_17_57 assumption_17_60 assumption_18d_64 assumption_18e_65 theorem_7_66 theorem_7_67 theorem_7_68 theorem_7_69 theorem_7_70 theorem_7_71 theorem_7_72 theorem_7_73 definition_smaller_or_equal_2 definition_smaller_8 meaning_postulate_greater_transitive_10 % 0.97/1.21 %------------------------------------------------------------------------------