%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT043+1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.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:55 AM UTC 2026 % Result : Theorem 14.35s 14.69s % Output : Refutation 14.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT043+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.10/0.36 % Computer : n016.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:09:47 UTC 2026 % 0.10/0.37 % CPUTime : % 14.35/14.69 % 14.35/14.69 SPASS V 3.9 % 14.35/14.69 SPASS beiseite: Proof found. % 14.35/14.69 % SZS status Theorem % 14.35/14.69 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 14.35/14.69 SPASS derived 21018 clauses, backtracked 1820 clauses, performed 9 splits and kept 6525 clauses. % 14.35/14.69 SPASS allocated 115171 KBytes. % 14.35/14.69 SPASS spent 0:0:12.87 on the problem. % 14.35/14.69 0:00:00.03 for the input. % 14.35/14.69 0:00:00.02 for the FLOTTER CNF translation. % 14.35/14.69 0:00:00.38 for inferences. % 14.35/14.69 0:00:00.11 for the backtracking. % 14.35/14.69 0:0:12.29 for the reduction. % 14.35/14.69 % 14.35/14.69 % 14.35/14.69 Here is a proof with depth 4, length 30 : % 14.35/14.69 % SZS output start Refutation % 14.35/14.69 1[0:Inp] || -> organization(skc3)*. % 14.35/14.69 2[0:Inp] || has_immunity(skc3,skc5)* -> . % 14.35/14.69 3[0:Inp] || has_immunity(skc3,skc4)* -> . % 14.35/14.69 4[0:Inp] || -> equal(stock_of_knowledge(skc3,skc5),stock_of_knowledge(skc3,skc4))**. % 14.35/14.69 5[0:Inp] || -> greater(internal_friction(skc3,skc4),internal_friction(skc3,skc5))*r. % 14.35/14.69 6[0:Inp] || -> equal(external_ties(skc3,skc5),external_ties(skc3,skc4))**. % 14.35/14.69 8[0:Inp] || equal(u,v) -> smaller_or_equal(u,v)*. % 14.35/14.69 10[0:Inp] || equal(u,v) -> greater_or_equal(u,v)*. % 14.35/14.69 11[0:Inp] || smaller(u,v)* -> greater(v,u). % 14.35/14.69 13[0:Inp] || greater(hazard_of_mortality(skc3,skc4),hazard_of_mortality(skc3,skc5))*r -> . % 14.35/14.69 20[0:Inp] organization(u) || equal(external_ties(u,v),external_ties(u,w))* -> equal(position(u,v),position(u,w)). % 14.35/14.69 22[0:Inp] organization(u) || smaller_or_equal(stock_of_knowledge(u,v),stock_of_knowledge(u,w))* greater(internal_friction(u,v),internal_friction(u,w)) -> smaller(capability(u,v),capability(u,w)). % 14.35/14.69 26[0:Inp] organization(u) || greater(capability(u,v),capability(u,w)) greater_or_equal(position(u,v),position(u,w)) -> has_immunity(u,v) has_immunity(u,w) smaller(hazard_of_mortality(u,v),hazard_of_mortality(u,w))*. % 14.35/14.69 35[0:Res:26.4,3.0] organization(skc3) || greater_or_equal(position(skc3,u),position(skc3,skc4)) greater(capability(skc3,u),capability(skc3,skc4)) -> smaller(hazard_of_mortality(skc3,u),hazard_of_mortality(skc3,skc4))* has_immunity(skc3,u). % 14.35/14.69 49[0:Res:6.0,20.1] organization(skc3) || -> equal(position(skc3,skc5),position(skc3,skc4))**. % 14.35/14.69 57[0:MRR:49.0,1.0] || -> equal(position(skc3,skc5),position(skc3,skc4))**. % 14.35/14.69 73[0:MRR:35.0,1.0] || greater(capability(skc3,u),capability(skc3,skc4)) greater_or_equal(position(skc3,u),position(skc3,skc4)) -> has_immunity(skc3,u) smaller(hazard_of_mortality(skc3,u),hazard_of_mortality(skc3,skc4))*. % 14.35/14.69 250[0:Res:8.1,22.1] organization(u) || equal(stock_of_knowledge(u,v),stock_of_knowledge(u,w)) greater(internal_friction(u,v),internal_friction(u,w)) -> smaller(capability(u,v),capability(u,w))*. % 14.35/14.69 2463[0:Res:73.3,11.0] || greater(capability(skc3,u),capability(skc3,skc4)) greater_or_equal(position(skc3,u),position(skc3,skc4))* -> has_immunity(skc3,u) greater(hazard_of_mortality(skc3,skc4),hazard_of_mortality(skc3,u)). % 14.35/14.69 4249[0:Res:250.3,11.0] organization(u) || equal(stock_of_knowledge(u,v),stock_of_knowledge(u,w)) greater(internal_friction(u,v),internal_friction(u,w))* -> greater(capability(u,w),capability(u,v)). % 14.35/14.69 16434[0:SpL:57.0,2463.1] || greater(capability(skc3,skc5),capability(skc3,skc4)) greater_or_equal(position(skc3,skc4),position(skc3,skc4))* -> has_immunity(skc3,skc5) greater(hazard_of_mortality(skc3,skc4),hazard_of_mortality(skc3,skc5)). % 14.35/14.69 17612[0:MRR:16434.2,2.0] || greater(capability(skc3,skc5),capability(skc3,skc4)) greater_or_equal(position(skc3,skc4),position(skc3,skc4))* -> greater(hazard_of_mortality(skc3,skc4),hazard_of_mortality(skc3,skc5)). % 14.35/14.69 17613[0:MRR:17612.2,13.0] || greater(capability(skc3,skc5),capability(skc3,skc4)) greater_or_equal(position(skc3,skc4),position(skc3,skc4))* -> . % 14.35/14.69 17905[0:Res:10.1,17613.1] || equal(position(skc3,skc4),position(skc3,skc4))* greater(capability(skc3,skc5),capability(skc3,skc4)) -> . % 14.35/14.69 17906[0:Obv:17905.0] || greater(capability(skc3,skc5),capability(skc3,skc4))*l -> . % 14.35/14.69 23946[0:Res:5.0,4249.2] organization(skc3) || equal(stock_of_knowledge(skc3,skc5),stock_of_knowledge(skc3,skc4))** -> greater(capability(skc3,skc5),capability(skc3,skc4)). % 14.35/14.69 23989[0:Rew:4.0,23946.1] organization(skc3) || equal(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc4))* -> greater(capability(skc3,skc5),capability(skc3,skc4)). % 14.35/14.69 23990[0:Obv:23989.1] organization(skc3) || -> greater(capability(skc3,skc5),capability(skc3,skc4))*l. % 14.35/14.69 23991[0:SSi:23990.0,1.0] || -> greater(capability(skc3,skc5),capability(skc3,skc4))*l. % 14.35/14.69 23992[0:MRR:23991.0,17906.0] || -> . % 14.35/14.69 % SZS output end Refutation % 14.35/14.69 Formulae used in the proof : lemma_2 definition_smaller_or_equal definition_greater_or_equal definition_smaller assumption_6 assumption_5 assumption_4 % 14.35/14.69 %------------------------------------------------------------------------------