%------------------------------------------------------------------------------ % 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 : n010.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 37.95s 38.22s % Output : Refutation 37.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT043-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : run_spass %d %s % 0.10/0.36 % Computer : n010.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:06:40 UTC 2026 % 0.10/0.36 % CPUTime : % 37.95/38.22 % 37.95/38.22 SPASS V 3.9 % 37.95/38.22 SPASS beiseite: Proof found. % 37.95/38.22 % SZS status Theorem % 37.95/38.22 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 37.95/38.22 SPASS derived 20825 clauses, backtracked 972 clauses, performed 10 splits and kept 6128 clauses. % 37.95/38.22 SPASS allocated 92851 KBytes. % 37.95/38.22 SPASS spent 0:0:34.78 on the problem. % 37.95/38.22 0:00:00.06 for the input. % 37.95/38.22 0:00:00.00 for the FLOTTER CNF translation. % 37.95/38.22 0:00:00.93 for inferences. % 37.95/38.22 0:00:00.26 for the backtracking. % 37.95/38.22 0:0:33.44 for the reduction. % 37.95/38.22 % 37.95/38.22 % 37.95/38.22 Here is a proof with depth 4, length 30 : % 37.95/38.22 % SZS output start Refutation % 37.95/38.22 1[0:Inp] organization(u) || greater_or_equal(position(u,v),position(u,w)) greater(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))*. % 37.95/38.22 5[0:Inp] organization(u) || greater(internal_friction(u,v),internal_friction(u,w)) smaller_or_equal(stock_of_knowledge(u,v),stock_of_knowledge(u,w))* -> smaller(capability(u,v),capability(u,w)). % 37.95/38.22 8[0:Inp] organization(u) || equal(external_ties(u,v),external_ties(u,w))* -> equal(position(u,v),position(u,w)). % 37.95/38.22 9[0:Inp] || -> organization(sk1)*. % 37.95/38.22 10[0:Inp] || has_immunity(sk1,sk2)* -> . % 37.95/38.22 11[0:Inp] || has_immunity(sk1,sk3)* -> . % 37.95/38.22 12[0:Inp] || -> equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))**. % 37.95/38.22 13[0:Inp] || -> greater(internal_friction(sk1,sk3),internal_friction(sk1,sk2))*l. % 37.95/38.22 14[0:Inp] || -> equal(external_ties(sk1,sk3),external_ties(sk1,sk2))**. % 37.95/38.22 15[0:Inp] || greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))*l -> . % 37.95/38.22 18[0:Inp] || equal(u,v) -> smaller_or_equal(u,v)*. % 37.95/38.22 21[0:Inp] || equal(u,v) -> greater_or_equal(u,v)*. % 37.95/38.22 22[0:Inp] || smaller(u,v)* -> greater(v,u). % 37.95/38.22 45[0:Res:1.4,10.0] organization(sk1) || greater(capability(sk1,sk2),capability(sk1,u)) greater_or_equal(position(sk1,sk2),position(sk1,u)) -> has_immunity(sk1,u) smaller(hazard_of_mortality(sk1,sk2),hazard_of_mortality(sk1,u))*. % 37.95/38.22 49[0:Res:14.0,8.1] organization(sk1) || -> equal(position(sk1,sk3),position(sk1,sk2))**. % 37.95/38.22 57[0:MRR:49.0,9.0] || -> equal(position(sk1,sk3),position(sk1,sk2))**. % 37.95/38.22 62[0:MRR:45.0,9.0] || greater_or_equal(position(sk1,sk2),position(sk1,u)) greater(capability(sk1,sk2),capability(sk1,u)) -> has_immunity(sk1,u) smaller(hazard_of_mortality(sk1,sk2),hazard_of_mortality(sk1,u))*. % 37.95/38.22 205[0:Res:18.1,5.2] 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))*. % 37.95/38.22 804[0:Res:62.3,22.0] || greater_or_equal(position(sk1,sk2),position(sk1,u))* greater(capability(sk1,sk2),capability(sk1,u)) -> has_immunity(sk1,u) greater(hazard_of_mortality(sk1,u),hazard_of_mortality(sk1,sk2)). % 37.95/38.22 2372[0:Res:205.3,22.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)). % 37.95/38.22 12852[0:SpL:57.0,804.0] || greater_or_equal(position(sk1,sk2),position(sk1,sk2))* greater(capability(sk1,sk2),capability(sk1,sk3)) -> has_immunity(sk1,sk3) greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)). % 37.95/38.22 13143[0:MRR:12852.2,11.0] || greater_or_equal(position(sk1,sk2),position(sk1,sk2))* greater(capability(sk1,sk2),capability(sk1,sk3)) -> greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)). % 37.95/38.22 13144[0:MRR:13143.2,15.0] || greater_or_equal(position(sk1,sk2),position(sk1,sk2))* greater(capability(sk1,sk2),capability(sk1,sk3)) -> . % 37.95/38.22 13464[0:Res:21.1,13144.0] || equal(position(sk1,sk2),position(sk1,sk2))* greater(capability(sk1,sk2),capability(sk1,sk3)) -> . % 37.95/38.22 13465[0:Obv:13464.0] || greater(capability(sk1,sk2),capability(sk1,sk3))*r -> . % 37.95/38.22 23000[0:Res:13.0,2372.2] organization(sk1) || equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))** -> greater(capability(sk1,sk2),capability(sk1,sk3)). % 37.95/38.22 23093[0:Rew:12.0,23000.1] organization(sk1) || equal(stock_of_knowledge(sk1,sk2),stock_of_knowledge(sk1,sk2))* -> greater(capability(sk1,sk2),capability(sk1,sk3)). % 37.95/38.22 23094[0:Obv:23093.1] organization(sk1) || -> greater(capability(sk1,sk2),capability(sk1,sk3))*r. % 37.95/38.22 23095[0:SSi:23094.0,9.0] || -> greater(capability(sk1,sk2),capability(sk1,sk3))*r. % 37.95/38.22 23096[0:MRR:23095.0,13465.0] || -> . % 37.95/38.22 % SZS output end Refutation % 37.95/38.22 Formulae used in the proof : assumption_4_38 assumption_5_42 assumption_6_45 lemma_2_46 lemma_2_47 lemma_2_48 lemma_2_49 lemma_2_50 lemma_2_51 lemma_2_52 definition_smaller_or_equal_3 definition_greater_or_equal_6 definition_smaller_7 % 37.95/38.22 %------------------------------------------------------------------------------