%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT057-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n001.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.14s 0.50s % Output : Refutation 0.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT057-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.08/0.35 % Computer : n001.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:35:52 UTC 2026 % 0.08/0.36 % CPUTime : % 0.14/0.50 % 0.14/0.50 SPASS V 3.9 % 0.14/0.50 SPASS beiseite: Proof found. % 0.14/0.50 % SZS status Theorem % 0.14/0.50 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.14/0.50 SPASS derived 196 clauses, backtracked 0 clauses, performed 1 splits and kept 85 clauses. % 0.14/0.50 SPASS allocated 75804 KBytes. % 0.14/0.50 SPASS spent 0:00:00.12 on the problem. % 0.14/0.50 0:00:00.06 for the input. % 0.14/0.50 0:00:00.00 for the FLOTTER CNF translation. % 0.14/0.50 0:00:00.00 for inferences. % 0.14/0.50 0:00:00.00 for the backtracking. % 0.14/0.50 0:00:00.01 for the reduction. % 0.14/0.50 % 0.14/0.50 % 0.14/0.50 Here is a proof with depth 4, length 30 : % 0.14/0.50 % SZS output start Refutation % 0.14/0.50 2[0:Inp] has_endowment(u) || smaller_or_equal(age(u,v),eta)* -> has_immunity(u,v). % 0.14/0.50 3[0:Inp] has_endowment(u) || has_immunity(u,v) greater(age(u,v),eta)*l -> . % 0.14/0.50 8[0:Inp] organization(u) || has_immunity(u,v) has_immunity(u,w) -> equal(hazard_of_mortality(u,w),hazard_of_mortality(u,v))*. % 0.14/0.50 9[0:Inp] organization(u) || has_immunity(u,v) -> has_immunity(u,w) greater(hazard_of_mortality(u,w),hazard_of_mortality(u,v))*. % 0.14/0.50 10[0:Inp] || -> organization(sk2)*. % 0.14/0.50 11[0:Inp] || -> has_endowment(sk2)*. % 0.14/0.50 12[0:Inp] || -> equal(age(sk2,sk3),zero)**. % 0.14/0.50 13[0:Inp] || -> smaller_or_equal(age(sk2,sk4),eta)*. % 0.14/0.50 14[0:Inp] || -> greater(age(sk2,sk5),eta)*l. % 0.14/0.50 15[0:Inp] || -> greater(eta,zero)*r. % 0.14/0.50 16[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.14/0.50 18[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 0.14/0.50 24[0:Inp] || greater(u,v) -> smaller(v,u)*. % 0.14/0.50 29[0:Res:11.0,2.0] || smaller_or_equal(age(sk2,u),eta)* -> has_immunity(sk2,u). % 0.14/0.50 31[0:Res:10.0,9.0] || has_immunity(sk2,u) -> has_immunity(sk2,v) greater(hazard_of_mortality(sk2,v),hazard_of_mortality(sk2,u))*. % 0.14/0.50 34[0:Res:10.0,8.0] || has_immunity(sk2,u) has_immunity(sk2,v) -> equal(hazard_of_mortality(sk2,v),hazard_of_mortality(sk2,u))*. % 0.14/0.50 36[0:Res:13.0,2.1] has_endowment(sk2) || -> has_immunity(sk2,sk4)*. % 0.14/0.50 44[0:Res:15.0,24.0] || -> smaller(zero,eta)*. % 0.14/0.50 46[0:Res:14.0,3.1] has_endowment(sk2) || has_immunity(sk2,sk5)* -> . % 0.14/0.50 55[0:MRR:36.0,11.0] || -> has_immunity(sk2,sk4)*. % 0.14/0.50 56[0:MRR:46.0,11.0] || has_immunity(sk2,sk5)* -> . % 0.14/0.50 60[0:Res:44.0,18.0] || -> smaller_or_equal(zero,eta)*. % 0.14/0.50 62[0:SpL:12.0,29.0] || smaller_or_equal(zero,eta) -> has_immunity(sk2,sk3)*. % 0.14/0.50 65[0:MRR:62.0,60.0] || -> has_immunity(sk2,sk3)*. % 0.14/0.50 259[0:Res:31.2,16.1] || has_immunity(sk2,sk4) equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3))** -> has_immunity(sk2,sk5). % 0.14/0.50 262[0:MRR:259.0,259.2,55.0,56.0] || equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3))** -> . % 0.14/0.50 263[0:SpL:34.2,262.0] || has_immunity(sk2,sk4) has_immunity(sk2,u) equal(hazard_of_mortality(sk2,u),hazard_of_mortality(sk2,sk3))* -> . % 0.14/0.50 267[0:MRR:263.0,55.0] || has_immunity(sk2,u) equal(hazard_of_mortality(sk2,u),hazard_of_mortality(sk2,sk3))* -> . % 0.14/0.50 268[0:EqR:267.1] || has_immunity(sk2,sk3)* -> . % 0.14/0.50 277[0:MRR:268.0,65.0] || -> . % 0.14/0.50 % SZS output end Refutation % 0.14/0.50 Formulae used in the proof : definition_1_32 definition_1_33 assumption_2_38 assumption_3_39 theorem_6_40 theorem_6_41 theorem_6_42 theorem_6_43 theorem_6_44 theorem_6_45 theorem_6_46 definition_smaller_or_equal_2 definition_smaller_8 % 0.14/0.50 %------------------------------------------------------------------------------