%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT065-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n007.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:59 AM UTC 2026 % Result : Unsatisfiable 1.14s 1.49s % Output : Refutation 1.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT065-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.10/0.36 % Computer : n007.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Mon Sep 7 13:44:26 UTC 2026 % 0.10/0.36 % CPUTime : % 1.14/1.49 % 1.14/1.49 SPASS V 3.9 % 1.14/1.49 SPASS beiseite: Proof found. % 1.14/1.49 % SZS status Theorem % 1.14/1.49 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.14/1.49 SPASS derived 9795 clauses, backtracked 654 clauses, performed 6 splits and kept 2788 clauses. % 1.14/1.49 SPASS allocated 81454 KBytes. % 1.14/1.49 SPASS spent 0:00:01.06 on the problem. % 1.14/1.49 0:00:00.03 for the input. % 1.14/1.49 0:00:00.00 for the FLOTTER CNF translation. % 1.14/1.49 0:00:00.09 for inferences. % 1.14/1.49 0:00:00.01 for the backtracking. % 1.14/1.49 0:00:00.90 for the reduction. % 1.14/1.49 % 1.14/1.49 % 1.14/1.49 Here is a proof with depth 3, length 66 : % 1.14/1.49 % SZS output start Refutation % 1.14/1.49 2[0:Inp] has_endowment(u) || smaller_or_equal(age(u,v),eta)* -> has_immunity(u,v). % 1.14/1.49 3[0:Inp] has_endowment(u) || has_immunity(u,v) greater(age(u,v),eta)*l -> . % 1.14/1.49 10[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)* -> . % 1.14/1.49 15[0:Inp] organization(u) || equal(age(u,v),zero)** -> is_aligned(u,v). % 1.14/1.49 16[0:Inp] organization(u) || greater(age(u,v),sigma) equal(age(u,w),zero) -> dissimilar(u,w,v)*. % 1.14/1.49 18[0:Inp] organization(u) || has_immunity(u,v) -> equal(hazard_of_mortality(u,v),very_low)**. % 1.14/1.49 20[0:Inp] organization(u) || positional_advantage(u,v) -> is_aligned(u,v) has_immunity(u,v) equal(hazard_of_mortality(u,v),mod1)**. % 1.14/1.49 22[0:Inp] organization(u) || -> positional_advantage(u,v) is_aligned(u,v) has_immunity(u,v) equal(hazard_of_mortality(u,v),high)**. % 1.14/1.49 24[0:Inp] || -> greater(mod1,low)*l. % 1.14/1.49 25[0:Inp] || -> greater(low,very_low)*l. % 1.14/1.49 26[0:Inp] || -> greater(high,mod2)*l. % 1.14/1.49 27[0:Inp] || -> greater(mod2,low)*l. % 1.14/1.49 28[0:Inp] || -> organization(sk2)*. % 1.14/1.49 30[0:Inp] || -> has_endowment(sk2)*. % 1.14/1.49 31[0:Inp] || -> equal(age(sk2,sk3),zero)**. % 1.14/1.49 34[0:Inp] || -> greater(eta,zero)*r. % 1.14/1.49 37[0:Inp] || -> smaller_or_equal(age(sk2,sk4),eta)*. % 1.14/1.49 38[0:Inp] || -> greater(age(sk2,sk5),sigma)*l. % 1.14/1.49 40[0:Inp] || -> greater(age(sk2,sk5),eta)*l. % 1.14/1.49 41[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 -> . % 1.14/1.49 43[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 1.14/1.49 49[0:Inp] || greater(u,v) -> smaller(v,u)*. % 1.14/1.49 51[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 1.14/1.49 55[0:Res:30.0,2.0] || smaller_or_equal(age(sk2,u),eta)* -> has_immunity(sk2,u). % 1.14/1.49 67[0:Res:28.0,15.0] || equal(age(sk2,u),zero)** -> is_aligned(sk2,u). % 1.14/1.49 68[0:Res:28.0,18.0] || has_immunity(sk2,u) -> equal(hazard_of_mortality(sk2,u),very_low)**. % 1.14/1.49 69[0:Res:37.0,2.1] has_endowment(sk2) || -> has_immunity(sk2,sk4)*. % 1.14/1.49 82[0:Res:34.0,49.0] || -> smaller(zero,eta)*. % 1.14/1.49 92[0:Res:40.0,3.1] has_endowment(sk2) || has_immunity(sk2,sk5)* -> . % 1.14/1.49 101[0:Res:38.0,16.2] organization(sk2) || equal(age(sk2,u),zero) -> dissimilar(sk2,u,sk5)*. % 1.14/1.49 110[0:MRR:69.0,30.0] || -> has_immunity(sk2,sk4)*. % 1.14/1.49 112[0:MRR:92.0,30.0] || has_immunity(sk2,sk5)* -> . % 1.14/1.49 113[0:MRR:101.0,28.0] || equal(age(sk2,u),zero) -> dissimilar(sk2,u,sk5)*. % 1.14/1.49 157[0:Res:82.0,43.0] || -> smaller_or_equal(zero,eta)*. % 1.14/1.49 160[0:SpL:31.0,55.0] || smaller_or_equal(zero,eta) -> has_immunity(sk2,sk3)*. % 1.14/1.49 163[0:MRR:160.0,157.0] || -> has_immunity(sk2,sk3)*. % 1.14/1.49 195[0:Res:113.1,10.2] || equal(age(sk2,u),zero)** is_aligned(sk2,sk5) is_aligned(sk2,u) -> . % 1.14/1.49 198[0:MRR:195.2,67.1] || equal(age(sk2,u),zero)** is_aligned(sk2,sk5) -> . % 1.14/1.49 199[0:SpL:31.0,198.0] || equal(zero,zero) is_aligned(sk2,sk5)* -> . % 1.14/1.49 201[0:Obv:199.0] || is_aligned(sk2,sk5)* -> . % 1.14/1.49 417[0:SpL:20.4,41.1] organization(sk2) || positional_advantage(sk2,sk5) equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3)) greater(mod1,hazard_of_mortality(sk2,sk4))*r -> is_aligned(sk2,sk5) has_immunity(sk2,sk5). % 1.14/1.49 419[0:SpL:22.4,41.1] organization(sk2) || equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3)) greater(high,hazard_of_mortality(sk2,sk4))*r -> positional_advantage(sk2,sk5) is_aligned(sk2,sk5) has_immunity(sk2,sk5). % 1.14/1.49 946[0:CRe:51.0,27.0] || greater(low,u)*+ -> greater(mod2,u)*. % 1.14/1.49 948[0:CRe:51.0,24.0] || greater(low,u)*+ -> greater(mod1,u)*. % 1.14/1.49 950[0:CRe:51.0,26.0] || greater(mod2,u)*+ -> greater(high,u)*. % 1.14/1.49 1077[0:Res:25.0,946.0] || -> greater(mod2,very_low)*l. % 1.14/1.49 1142[0:Res:25.0,948.0] || -> greater(mod1,very_low)*l. % 1.14/1.49 1177[0:Res:1077.0,950.0] || -> greater(high,very_low)*l. % 1.14/1.49 9281[0:SSi:419.0,30.0,28.0] || equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3)) greater(high,hazard_of_mortality(sk2,sk4))*r -> positional_advantage(sk2,sk5) is_aligned(sk2,sk5) has_immunity(sk2,sk5). % 1.14/1.49 9282[0:MRR:9281.3,9281.4,201.0,112.0] || equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3)) greater(high,hazard_of_mortality(sk2,sk4))*r -> positional_advantage(sk2,sk5). % 1.14/1.49 9283[0:SSi:417.0,30.0,28.0] || positional_advantage(sk2,sk5) equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3)) greater(mod1,hazard_of_mortality(sk2,sk4))*r -> is_aligned(sk2,sk5) has_immunity(sk2,sk5). % 1.14/1.49 9284[0:MRR:9283.3,9283.4,201.0,112.0] || positional_advantage(sk2,sk5) equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3)) greater(mod1,hazard_of_mortality(sk2,sk4))*r -> . % 1.14/1.49 10173[0:SpL:68.1,9282.1] || has_immunity(sk2,sk4) equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3))** greater(high,very_low) -> positional_advantage(sk2,sk5). % 1.14/1.49 10183[0:Rew:68.1,10173.1] || has_immunity(sk2,sk4) equal(hazard_of_mortality(sk2,sk3),very_low)** greater(high,very_low) -> positional_advantage(sk2,sk5). % 1.14/1.49 10184[0:MRR:10183.0,10183.2,110.0,1177.0] || equal(hazard_of_mortality(sk2,sk3),very_low)** -> positional_advantage(sk2,sk5). % 1.14/1.49 10190[0:SpL:68.1,10184.0] || has_immunity(sk2,sk3) equal(very_low,very_low) -> positional_advantage(sk2,sk5)*. % 1.14/1.49 10196[0:Obv:10190.1] || has_immunity(sk2,sk3) -> positional_advantage(sk2,sk5)*. % 1.14/1.49 10197[0:MRR:10196.0,163.0] || -> positional_advantage(sk2,sk5)*. % 1.14/1.49 10198[0:MRR:9284.0,10197.0] || equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3)) greater(mod1,hazard_of_mortality(sk2,sk4))*r -> . % 1.14/1.49 10207[0:SpL:68.1,10198.1] || has_immunity(sk2,sk4) equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3))** greater(mod1,very_low) -> . % 1.14/1.49 10217[0:Rew:68.1,10207.1] || has_immunity(sk2,sk4) equal(hazard_of_mortality(sk2,sk3),very_low)** greater(mod1,very_low) -> . % 1.14/1.49 10218[0:MRR:10217.0,10217.2,110.0,1142.0] || equal(hazard_of_mortality(sk2,sk3),very_low)** -> . % 1.14/1.49 10229[0:SpL:18.2,10218.0] organization(sk2) || has_immunity(sk2,sk3)* equal(very_low,very_low) -> . % 1.14/1.49 10232[0:Obv:10229.2] organization(sk2) || has_immunity(sk2,sk3)* -> . % 1.14/1.49 10233[0:SSi:10232.0,30.0,28.0] || has_immunity(sk2,sk3)* -> . % 1.14/1.49 10234[0:MRR:10233.0,163.0] || -> . % 1.14/1.49 % SZS output end Refutation % 1.14/1.49 Formulae used in the proof : definition_1_41 definition_1_42 definition_2_49 assumption_13_54 assumption_15_55 assumption_17_57 assumption_17_59 assumption_17_61 assumption_18b_63 assumption_18c_64 assumption_18d_65 assumption_18e_66 theorem_11_67 theorem_11_69 theorem_11_70 theorem_11_73 theorem_11_76 theorem_11_77 theorem_11_79 theorem_11_80 definition_smaller_or_equal_2 definition_smaller_8 meaning_postulate_greater_transitive_10 % 1.14/1.49 %------------------------------------------------------------------------------