%------------------------------------------------------------------------------ % 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 : n018.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.57s % 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.07/0.35 % Computer : n018.cluster.edu % 0.07/0.35 % Model : x86_64 x86_64 % 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.35 % Memory : 8046.5625MB % 0.07/0.35 % OS : Linux 6.8.0-71-generic % 0.07/0.36 % CPULimit : 300 % 0.07/0.36 % WCLimit : 300 % 0.07/0.36 % DateTime : Mon Sep 7 13:29:22 UTC 2026 % 0.07/0.36 % CPUTime : % 0.22/0.57 % 0.22/0.57 SPASS V 3.9 % 0.22/0.57 SPASS beiseite: Proof found. % 0.22/0.57 % SZS status Theorem % 0.22/0.57 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.22/0.57 SPASS derived 378 clauses, backtracked 26 clauses, performed 2 splits and kept 174 clauses. % 0.22/0.57 SPASS allocated 97970 KBytes. % 0.22/0.57 SPASS spent 0:00:00.19 on the problem. % 0.22/0.57 0:00:00.06 for the input. % 0.22/0.57 0:00:00.05 for the FLOTTER CNF translation. % 0.22/0.57 0:00:00.01 for inferences. % 0.22/0.57 0:00:00.00 for the backtracking. % 0.22/0.57 0:00:00.03 for the reduction. % 0.22/0.57 % 0.22/0.57 % 0.22/0.57 Here is a proof with depth 4, length 44 : % 0.22/0.57 % SZS output start Refutation % 0.22/0.57 1[0:Inp] || -> has_endowment(skc4)*. % 0.22/0.57 2[0:Inp] || -> organization(skc4)*. % 0.22/0.57 3[0:Inp] || -> greater_or_equal(eta,sigma)*. % 0.22/0.57 4[0:Inp] || -> greater(sigma,zero)*l. % 0.22/0.57 5[0:Inp] || -> greater(age(skc4,skc7),eta)*l. % 0.22/0.57 6[0:Inp] || -> smaller_or_equal(age(skc4,skc6),eta)*. % 0.22/0.57 7[0:Inp] || -> equal(age(skc4,skc5),zero)**. % 0.22/0.57 9[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 0.22/0.57 14[0:Inp] || greater(u,v) -> smaller(v,u)*. % 0.22/0.57 18[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.22/0.57 19[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.22/0.57 20[0:Inp] has_endowment(u) || smaller_or_equal(age(u,v),eta)* -> has_immunity(u,v). % 0.22/0.57 21[0:Inp] has_endowment(u) || has_immunity(u,v) greater(age(u,v),eta)*l -> . % 0.22/0.57 24[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.57 27[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.57 28[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.57 29[0:Res:2.0,27.0] || has_immunity(skc4,u) -> has_immunity(skc4,v) greater(hazard_of_mortality(skc4,v),hazard_of_mortality(skc4,u))*. % 0.22/0.57 32[0:Res:2.0,28.0] || has_immunity(skc4,u) has_immunity(skc4,v) -> equal(hazard_of_mortality(skc4,u),hazard_of_mortality(skc4,v))*. % 0.22/0.57 36[0:Res:1.0,20.0] || smaller_or_equal(age(skc4,u),eta)* -> has_immunity(skc4,u). % 0.22/0.57 38[0:Res:3.0,18.0] || -> equal(sigma,eta) greater(eta,sigma)*r. % 0.22/0.57 43[0:Res:6.0,20.1] has_endowment(skc4) || -> has_immunity(skc4,skc6)*. % 0.22/0.57 47[0:Res:4.0,14.0] || -> smaller(zero,sigma)*. % 0.22/0.57 49[0:Res:5.0,21.2] has_endowment(skc4) || has_immunity(skc4,skc7)* -> . % 0.22/0.57 58[0:MRR:43.0,1.0] || -> has_immunity(skc4,skc6)*. % 0.22/0.57 59[0:MRR:49.0,1.0] || has_immunity(skc4,skc7)* -> . % 0.22/0.57 62[1:Spt:38.0] || -> equal(sigma,eta)**. % 0.22/0.57 63[1:Rew:62.0,47.0] || -> smaller(zero,eta)*. % 0.22/0.57 70[1:Res:63.0,9.0] || -> smaller_or_equal(zero,eta)*. % 0.22/0.57 72[0:SpL:7.0,36.0] || smaller_or_equal(zero,eta) -> has_immunity(skc4,skc5)*. % 0.22/0.57 75[1:MRR:72.0,70.0] || -> has_immunity(skc4,skc5)*. % 0.22/0.57 79[0:Res:14.1,9.0] || greater(u,v) -> smaller_or_equal(v,u)*. % 0.22/0.57 85[0:Res:79.1,36.0] || greater(eta,age(skc4,u))*r -> has_immunity(skc4,u). % 0.22/0.57 91[0:SpL:7.0,85.0] || greater(eta,zero) -> has_immunity(skc4,skc5)*. % 0.22/0.57 423[0:Res:29.2,24.1] || has_immunity(skc4,skc6) equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5))** -> has_immunity(skc4,skc7). % 0.22/0.57 430[0:MRR:423.0,423.2,58.0,59.0] || equal(hazard_of_mortality(skc4,skc6),hazard_of_mortality(skc4,skc5))** -> . % 0.22/0.57 431[0:SpL:32.2,430.0] || has_immunity(skc4,u) has_immunity(skc4,skc6) equal(hazard_of_mortality(skc4,u),hazard_of_mortality(skc4,skc5))* -> . % 0.22/0.57 435[0:MRR:431.1,58.0] || has_immunity(skc4,u) equal(hazard_of_mortality(skc4,u),hazard_of_mortality(skc4,skc5))* -> . % 0.22/0.57 436[0:EqR:435.1] || has_immunity(skc4,skc5)* -> . % 0.22/0.57 445[1:MRR:436.0,75.0] || -> . % 0.22/0.57 455[1:Spt:445.0,38.0,62.0] || equal(sigma,eta)** -> . % 0.22/0.57 456[1:Spt:445.0,38.1] || -> greater(eta,sigma)*r. % 0.22/0.57 460[0:MRR:91.1,436.0] || greater(eta,zero)*r -> . % 0.22/0.57 479[1:OCh:19.1,19.0,4.0,456.0] || -> greater(eta,zero)*r. % 0.22/0.57 484[1:MRR:479.0,460.0] || -> . % 0.22/0.57 % SZS output end Refutation % 0.22/0.57 Formulae used in the proof : lemma_9 definition_smaller_or_equal definition_smaller definition_greater_or_equal meaning_postulate_greater_transitive definition_1 assumption_3 assumption_2 % 0.22/0.57 %------------------------------------------------------------------------------