%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT046-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n017.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 : Unsatisfiable 1.36s 1.65s % Output : Refutation 1.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT046-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.11/0.36 % Computer : n017.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Mon Sep 7 13:05:54 UTC 2026 % 0.11/0.37 % CPUTime : % 1.36/1.65 % 1.36/1.65 SPASS V 3.9 % 1.36/1.65 SPASS beiseite: Proof found. % 1.36/1.65 % SZS status Theorem % 1.36/1.65 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.36/1.65 SPASS derived 2051 clauses, backtracked 0 clauses, performed 3 splits and kept 1082 clauses. % 1.36/1.65 SPASS allocated 77576 KBytes. % 1.36/1.65 SPASS spent 0:00:01.25 on the problem. % 1.36/1.65 0:00:00.06 for the input. % 1.36/1.65 0:00:00.00 for the FLOTTER CNF translation. % 1.36/1.65 0:00:00.07 for inferences. % 1.36/1.65 0:00:00.01 for the backtracking. % 1.36/1.65 0:00:01.06 for the reduction. % 1.36/1.65 % 1.36/1.65 % 1.36/1.65 Here is a proof with depth 3, length 32 : % 1.36/1.65 % SZS output start Refutation % 1.36/1.65 1[0:Inp] organization(u) || has_immunity(u,v)* -> has_endowment(u). % 1.36/1.65 3[0:Inp] organization(u) || greater(position(u,v),position(u,w)) greater_or_equal(capability(u,v),capability(u,w)) -> has_immunity(u,v) has_immunity(u,w) smaller(hazard_of_mortality(u,v),hazard_of_mortality(u,w))*. % 1.36/1.65 5[0:Inp] organization(u) || smaller_or_equal(internal_friction(u,v),internal_friction(u,w))* greater(stock_of_knowledge(u,v),stock_of_knowledge(u,w)) -> greater(capability(u,v),capability(u,w)). % 1.36/1.65 8[0:Inp] organization(u) || greater(external_ties(u,v),external_ties(u,w))* -> greater(position(u,v),position(u,w)). % 1.36/1.65 10[0:Inp] organization(u) || greater(age(u,v),age(u,w))* -> greater(stock_of_knowledge(u,v),stock_of_knowledge(u,w)). % 1.36/1.65 11[0:Inp] organization(u) || greater(age(u,v),age(u,w))* -> greater(external_ties(u,v),external_ties(u,w)). % 1.36/1.65 12[0:Inp] organization(u) || -> equal(internal_friction(u,v),internal_friction(u,w))*. % 1.36/1.65 13[0:Inp] || -> organization(sk1)*. % 1.36/1.65 14[0:Inp] || has_endowment(sk1)* -> . % 1.36/1.65 15[0:Inp] || -> greater(age(sk1,sk3),age(sk1,sk2))*r. % 1.36/1.65 16[0:Inp] || smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))* -> . % 1.36/1.65 19[0:Inp] || equal(u,v) -> smaller_or_equal(u,v)*. % 1.36/1.65 21[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 1.36/1.65 39[0:Res:13.0,1.0] || has_immunity(sk1,u)* -> has_endowment(sk1). % 1.36/1.65 43[0:Res:3.5,16.0] organization(sk1) || greater_or_equal(capability(sk1,sk3),capability(sk1,sk2))* greater(position(sk1,sk3),position(sk1,sk2)) -> has_immunity(sk1,sk2) has_immunity(sk1,sk3). % 1.36/1.65 50[0:Res:15.0,11.1] organization(sk1) || -> greater(external_ties(sk1,sk3),external_ties(sk1,sk2))*r. % 1.36/1.65 51[0:Res:15.0,10.1] organization(sk1) || -> greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))*r. % 1.36/1.65 52[0:MRR:39.1,14.0] || has_immunity(sk1,u)* -> . % 1.36/1.65 53[0:MRR:50.0,13.0] || -> greater(external_ties(sk1,sk3),external_ties(sk1,sk2))*r. % 1.36/1.65 54[0:MRR:51.0,13.0] || -> greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))*r. % 1.36/1.65 57[0:MRR:43.0,43.3,43.4,13.0,52.0,52.0] || greater(position(sk1,sk3),position(sk1,sk2)) greater_or_equal(capability(sk1,sk3),capability(sk1,sk2))* -> . % 1.36/1.65 258[0:Res:21.1,57.1] || greater(capability(sk1,sk3),capability(sk1,sk2)) greater(position(sk1,sk3),position(sk1,sk2))*r -> . % 1.36/1.65 263[0:Res:53.0,8.1] organization(sk1) || -> greater(position(sk1,sk3),position(sk1,sk2))*r. % 1.36/1.65 275[0:SSi:263.0,13.0] || -> greater(position(sk1,sk3),position(sk1,sk2))*r. % 1.36/1.65 278[0:MRR:258.1,275.0] || greater(capability(sk1,sk3),capability(sk1,sk2))*r -> . % 1.36/1.65 347[0:SpL:12.1,5.1] organization(u) organization(u) || smaller_or_equal(internal_friction(u,v),internal_friction(u,w))* greater(stock_of_knowledge(u,x),stock_of_knowledge(u,w))* -> greater(capability(u,x),capability(u,w)). % 1.36/1.65 352[0:Obv:347.0] organization(u) || smaller_or_equal(internal_friction(u,v),internal_friction(u,w))* greater(stock_of_knowledge(u,x),stock_of_knowledge(u,w))*+ -> greater(capability(u,x),capability(u,w)). % 1.36/1.65 2329[0:Res:54.0,352.2] organization(sk1) || smaller_or_equal(internal_friction(sk1,u),internal_friction(sk1,sk2))* -> greater(capability(sk1,sk3),capability(sk1,sk2)). % 1.36/1.65 2363[0:SSi:2329.0,13.0] || smaller_or_equal(internal_friction(sk1,u),internal_friction(sk1,sk2))* -> greater(capability(sk1,sk3),capability(sk1,sk2)). % 1.36/1.65 2364[0:MRR:2363.1,278.0] || smaller_or_equal(internal_friction(sk1,u),internal_friction(sk1,sk2))* -> . % 1.36/1.65 2374[0:Res:19.1,2364.0] || equal(internal_friction(sk1,u),internal_friction(sk1,sk2))* -> . % 1.36/1.65 2375[0:Obv:2374.0] || -> . % 1.36/1.65 % SZS output end Refutation % 1.36/1.65 Formulae used in the proof : assumption_1_41 assumption_4_43 assumption_5_45 assumption_6_48 assumption_7_50 assumption_8_51 assumption_9_52 theorem_1_53 theorem_1_54 theorem_1_55 theorem_1_56 definition_smaller_or_equal_3 definition_greater_or_equal_5 % 1.36/1.65 %------------------------------------------------------------------------------