%------------------------------------------------------------------------------ % 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 : n005.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 : Theorem 0.22s 0.47s % Output : Refutation 0.22s % 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.13/0.37 % Computer : n005.cluster.edu % 0.13/0.37 % Model : x86_64 x86_64 % 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.37 % Memory : 8046.5625MB % 0.13/0.37 % OS : Linux 6.8.0-71-generic % 0.13/0.37 % CPULimit : 300 % 0.13/0.37 % WCLimit : 300 % 0.13/0.37 % DateTime : Mon Sep 7 13:30:05 UTC 2026 % 0.13/0.38 % CPUTime : % 0.22/0.47 % 0.22/0.47 SPASS V 3.9 % 0.22/0.47 SPASS beiseite: Proof found. % 0.22/0.47 % SZS status Theorem % 0.22/0.47 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.22/0.47 SPASS derived 197 clauses, backtracked 0 clauses, performed 1 splits and kept 86 clauses. % 0.22/0.47 SPASS allocated 97798 KBytes. % 0.22/0.47 SPASS spent 0:00:00.08 on the problem. % 0.22/0.47 0:00:00.03 for the input. % 0.22/0.47 0:00:00.02 for the FLOTTER CNF translation. % 0.22/0.47 0:00:00.00 for inferences. % 0.22/0.47 0:00:00.00 for the backtracking. % 0.22/0.47 0:00:00.00 for the reduction. % 0.22/0.47 % 0.22/0.47 % 0.22/0.47 Here is a proof with depth 4, length 30 : % 0.22/0.47 % SZS output start Refutation % 0.22/0.47 1[0:Inp] || -> has_endowment(skc4)*. % 0.22/0.47 2[0:Inp] || -> organization(skc4)*. % 0.22/0.47 3[0:Inp] || -> greater(eta,zero)*r. % 0.22/0.47 4[0:Inp] || -> greater(age(skc4,skc7),eta)*l. % 0.22/0.47 5[0:Inp] || -> smaller_or_equal(age(skc4,skc6),eta)*. % 0.22/0.47 6[0:Inp] || -> equal(age(skc4,skc5),zero)**. % 0.22/0.47 8[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 0.22/0.47 13[0:Inp] || greater(u,v) -> smaller(v,u)*. % 0.22/0.47 19[0:Inp] has_endowment(u) || smaller_or_equal(age(u,v),eta)* -> has_immunity(u,v). % 0.22/0.47 20[0:Inp] has_endowment(u) || has_immunity(u,v) greater(age(u,v),eta)*l -> . % 0.22/0.47 23[0:Inp] || equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5)) greater(hazard_of_mortality(skc4,skc7),hazard_of_mortality(skc4,skc6))*l -> . % 0.22/0.47 26[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.47 27[0:Inp] organization(u) || has_immunity(u,v) has_immunity(u,w) -> equal(hazard_of_mortality(u,v),hazard_of_mortality(u,w))*. % 0.22/0.47 28[0:Res:2.0,26.0] || has_immunity(skc4,u) -> has_immunity(skc4,v) greater(hazard_of_mortality(skc4,v),hazard_of_mortality(skc4,u))*. % 0.22/0.47 31[0:Res:2.0,27.0] || has_immunity(skc4,u) has_immunity(skc4,v) -> equal(hazard_of_mortality(skc4,u),hazard_of_mortality(skc4,v))*. % 0.22/0.47 35[0:Res:1.0,19.0] || smaller_or_equal(age(skc4,u),eta)* -> has_immunity(skc4,u). % 0.22/0.47 41[0:Res:5.0,19.1] has_endowment(skc4) || -> has_immunity(skc4,skc6)*. % 0.22/0.47 45[0:Res:3.0,13.0] || -> smaller(zero,eta)*. % 0.22/0.47 47[0:Res:4.0,20.2] has_endowment(skc4) || has_immunity(skc4,skc7)* -> . % 0.22/0.47 56[0:MRR:41.0,1.0] || -> has_immunity(skc4,skc6)*. % 0.22/0.47 57[0:MRR:47.0,1.0] || has_immunity(skc4,skc7)* -> . % 0.22/0.47 61[0:Res:45.0,8.0] || -> smaller_or_equal(zero,eta)*. % 0.22/0.47 63[0:SpL:6.0,35.0] || smaller_or_equal(zero,eta) -> has_immunity(skc4,skc5)*. % 0.22/0.47 66[0:MRR:63.0,61.0] || -> has_immunity(skc4,skc5)*. % 0.22/0.47 237[0:Res:28.2,23.1] || has_immunity(skc4,skc6) equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5))** -> has_immunity(skc4,skc7). % 0.22/0.47 254[0:MRR:237.0,237.2,56.0,57.0] || equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5))** -> . % 0.22/0.47 263[0:SpL:31.2,254.0] || has_immunity(skc4,u) has_immunity(skc4,skc6) equal(hazard_of_mortality(skc4,u),hazard_of_mortality(skc4,skc5))* -> . % 0.22/0.47 267[0:MRR:263.1,56.0] || has_immunity(skc4,u) equal(hazard_of_mortality(skc4,u),hazard_of_mortality(skc4,skc5))* -> . % 0.22/0.47 268[0:EqR:267.1] || has_immunity(skc4,skc5)* -> . % 0.22/0.47 277[0:MRR:268.0,66.0] || -> . % 0.22/0.47 % SZS output end Refutation % 0.22/0.47 Formulae used in the proof : theorem_6 definition_smaller_or_equal definition_smaller definition_1 assumption_3 assumption_2 % 0.22/0.47 %------------------------------------------------------------------------------