%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT056-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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.22s 0.49s % Output : Refutation 0.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT056-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.09/0.35 % Computer : n028.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Mon Sep 7 13:31:17 UTC 2026 % 0.09/0.36 % CPUTime : % 0.22/0.49 % 0.22/0.49 SPASS V 3.9 % 0.22/0.49 SPASS beiseite: Proof found. % 0.22/0.49 % SZS status Theorem % 0.22/0.49 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.22/0.49 SPASS derived 223 clauses, backtracked 26 clauses, performed 2 splits and kept 116 clauses. % 0.22/0.49 SPASS allocated 75823 KBytes. % 0.22/0.49 SPASS spent 0:00:00.11 on the problem. % 0.22/0.49 0:00:00.06 for the input. % 0.22/0.49 0:00:00.00 for the FLOTTER CNF translation. % 0.22/0.49 0:00:00.00 for inferences. % 0.22/0.49 0:00:00.00 for the backtracking. % 0.22/0.49 0:00:00.01 for the reduction. % 0.22/0.49 % 0.22/0.49 % 0.22/0.49 Here is a proof with depth 4, length 44 : % 0.22/0.49 % SZS output start Refutation % 0.22/0.49 2[0:Inp] has_endowment(u) || smaller_or_equal(age(u,v),eta)* -> has_immunity(u,v). % 0.22/0.49 3[0:Inp] has_endowment(u) || has_immunity(u,v) greater(age(u,v),eta)*l -> . % 0.22/0.49 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.22/0.49 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.22/0.49 10[0:Inp] || -> organization(sk2)*. % 0.22/0.49 11[0:Inp] || -> has_endowment(sk2)*. % 0.22/0.49 12[0:Inp] || -> equal(age(sk2,sk3),zero)**. % 0.22/0.49 13[0:Inp] || -> smaller_or_equal(age(sk2,sk4),eta)*. % 0.22/0.49 14[0:Inp] || -> greater(age(sk2,sk5),eta)*l. % 0.22/0.49 15[0:Inp] || -> greater_or_equal(eta,sigma)*. % 0.22/0.49 16[0:Inp] || -> greater(sigma,zero)*l. % 0.22/0.49 17[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.22/0.49 19[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 0.22/0.49 21[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.22/0.49 25[0:Inp] || greater(u,v) -> smaller(v,u)*. % 0.22/0.49 27[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.22/0.49 30[0:Res:11.0,2.0] || smaller_or_equal(age(sk2,u),eta)* -> has_immunity(sk2,u). % 0.22/0.49 32[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.22/0.49 35[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.22/0.49 37[0:Res:15.0,21.0] || -> equal(sigma,eta) greater(eta,sigma)*r. % 0.22/0.49 38[0:Res:13.0,2.1] has_endowment(sk2) || -> has_immunity(sk2,sk4)*. % 0.22/0.49 46[0:Res:16.0,25.0] || -> smaller(zero,sigma)*. % 0.22/0.49 48[0:Res:14.0,3.1] has_endowment(sk2) || has_immunity(sk2,sk5)* -> . % 0.22/0.49 57[0:MRR:38.0,11.0] || -> has_immunity(sk2,sk4)*. % 0.22/0.49 58[0:MRR:48.0,11.0] || has_immunity(sk2,sk5)* -> . % 0.22/0.49 61[1:Spt:37.0] || -> equal(sigma,eta)**. % 0.22/0.49 62[1:Rew:61.0,46.0] || -> smaller(zero,eta)*. % 0.22/0.49 69[1:Res:62.0,19.0] || -> smaller_or_equal(zero,eta)*. % 0.22/0.49 71[0:SpL:12.0,30.0] || smaller_or_equal(zero,eta) -> has_immunity(sk2,sk3)*. % 0.22/0.49 74[1:MRR:71.0,69.0] || -> has_immunity(sk2,sk3)*. % 0.22/0.49 78[0:Res:25.1,19.0] || greater(u,v) -> smaller_or_equal(v,u)*. % 0.22/0.49 84[0:Res:78.1,30.0] || greater(eta,age(sk2,u))*r -> has_immunity(sk2,u). % 0.22/0.49 96[0:SpL:12.0,84.0] || greater(eta,zero) -> has_immunity(sk2,sk3)*. % 0.22/0.49 247[0:Res:32.2,17.1] || has_immunity(sk2,sk4) equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3))** -> has_immunity(sk2,sk5). % 0.22/0.49 264[0:MRR:247.0,247.2,57.0,58.0] || equal(hazard_of_mortality(sk2,sk4),hazard_of_mortality(sk2,sk3))** -> . % 0.22/0.49 273[0:SpL:35.2,264.0] || has_immunity(sk2,sk4) has_immunity(sk2,u) equal(hazard_of_mortality(sk2,u),hazard_of_mortality(sk2,sk3))* -> . % 0.22/0.49 277[0:MRR:273.0,57.0] || has_immunity(sk2,u) equal(hazard_of_mortality(sk2,u),hazard_of_mortality(sk2,sk3))* -> . % 0.22/0.49 278[0:EqR:277.1] || has_immunity(sk2,sk3)* -> . % 0.22/0.49 287[1:MRR:278.0,74.0] || -> . % 0.22/0.49 297[1:Spt:287.0,37.0,61.0] || equal(sigma,eta)** -> . % 0.22/0.49 298[1:Spt:287.0,37.1] || -> greater(eta,sigma)*r. % 0.22/0.49 302[0:MRR:96.1,278.0] || greater(eta,zero)*r -> . % 0.22/0.49 319[1:OCh:27.1,27.0,16.0,298.0] || -> greater(eta,zero)*r. % 0.22/0.49 322[1:MRR:319.0,302.0] || -> . % 0.22/0.49 % SZS output end Refutation % 0.22/0.49 Formulae used in the proof : definition_1_32 definition_1_33 assumption_2_38 assumption_3_39 lemma_9_40 lemma_9_41 lemma_9_42 lemma_9_43 lemma_9_44 lemma_9_45 lemma_9_46 lemma_9_47 definition_smaller_or_equal_2 definition_greater_or_equal_4 definition_smaller_8 meaning_postulate_greater_transitive_10 % 0.22/0.49 %------------------------------------------------------------------------------