%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT042-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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:54 AM UTC 2026 % Result : Unsatisfiable 9.16s 9.45s % Output : Refutation 9.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT042-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.11/0.36 % Computer : n011.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.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Mon Sep 7 13:04:30 UTC 2026 % 0.11/0.36 % CPUTime : % 9.16/9.45 % 9.16/9.45 SPASS V 3.9 % 9.16/9.45 SPASS beiseite: Proof found. % 9.16/9.45 % SZS status Theorem % 9.16/9.45 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.16/9.45 SPASS derived 13404 clauses, backtracked 193 clauses, performed 12 splits and kept 4580 clauses. % 9.16/9.45 SPASS allocated 87387 KBytes. % 9.16/9.45 SPASS spent 0:00:09.06 on the problem. % 9.16/9.45 0:00:00.03 for the input. % 9.16/9.45 0:00:00.00 for the FLOTTER CNF translation. % 9.16/9.45 0:00:00.21 for inferences. % 9.16/9.45 0:00:00.10 for the backtracking. % 9.16/9.45 0:00:08.68 for the reduction. % 9.16/9.45 % 9.16/9.45 % 9.16/9.45 Here is a proof with depth 4, length 91 : % 9.16/9.45 % SZS output start Refutation % 9.16/9.45 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))*. % 9.16/9.45 2[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))*. % 9.16/9.45 4[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)). % 9.16/9.45 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)). % 9.16/9.45 6[0:Inp] organization(u) || equal(internal_friction(u,v),internal_friction(u,w))* equal(stock_of_knowledge(u,v),stock_of_knowledge(u,w)) -> equal(capability(u,v),capability(u,w)). % 9.16/9.45 7[0:Inp] organization(u) || greater(external_ties(u,v),external_ties(u,w))* -> greater(position(u,v),position(u,w)). % 9.16/9.45 8[0:Inp] organization(u) || equal(external_ties(u,v),external_ties(u,w))* -> equal(position(u,v),position(u,w)). % 9.16/9.45 9[0:Inp] || -> organization(sk1)*. % 9.16/9.45 10[0:Inp] || has_immunity(sk1,sk2)* -> . % 9.16/9.45 11[0:Inp] || has_immunity(sk1,sk3)* -> . % 9.16/9.45 12[0:Inp] || -> greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) greater_or_equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))*. % 9.16/9.45 14[0:Inp] || -> greater(external_ties(sk1,sk3),external_ties(sk1,sk2))*l greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)). % 9.16/9.45 17[0:Inp] || -> smaller_or_equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2))* smaller_or_equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2))*. % 9.16/9.45 20[0:Inp] || -> greater_or_equal(external_ties(sk1,sk3),external_ties(sk1,sk2))* greater(external_ties(sk1,sk3),external_ties(sk1,sk2)). % 9.16/9.45 27[0:Inp] || smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))* smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))* -> . % 9.16/9.45 28[0:Inp] || smaller_or_equal(u,v)* -> equal(u,v) smaller(u,v). % 9.16/9.45 30[0:Inp] || equal(u,v) -> smaller_or_equal(u,v)*. % 9.16/9.45 31[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 9.16/9.45 32[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 9.16/9.45 33[0:Inp] || equal(u,v) -> greater_or_equal(u,v)*. % 9.16/9.45 34[0:Inp] || smaller(u,v)* -> greater(v,u). % 9.16/9.45 36[0:Inp] || greater(u,v)*+ greater(v,u)* -> . % 9.16/9.45 39[0:Obv:17.0] || -> smaller_or_equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2))*. % 9.16/9.45 40[0:Obv:27.0] || smaller(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2))* -> . % 9.16/9.45 41[0:MRR:20.1,32.0] || -> greater_or_equal(external_ties(sk1,sk3),external_ties(sk1,sk2))*. % 9.16/9.45 42[0:MRR:12.0,32.0] || -> greater_or_equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))*. % 9.16/9.45 45[0:Res:9.0,4.0] || smaller_or_equal(internal_friction(sk1,u),internal_friction(sk1,v))* greater(stock_of_knowledge(sk1,u),stock_of_knowledge(sk1,v)) -> greater(capability(sk1,u),capability(sk1,v)). % 9.16/9.45 48[0:Res:9.0,7.0] || greater(external_ties(sk1,u),external_ties(sk1,v))* -> greater(position(sk1,u),position(sk1,v)). % 9.16/9.45 50[0:Res:9.0,8.0] || equal(external_ties(sk1,u),external_ties(sk1,v))* -> equal(position(sk1,u),position(sk1,v)). % 9.16/9.45 63[0:Res:39.0,28.0] || -> equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2)) smaller(internal_friction(sk1,sk3),internal_friction(sk1,sk2))*. % 9.16/9.45 64[0:Res:39.0,4.2] organization(sk1) || greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))*l -> greater(capability(sk1,sk3),capability(sk1,sk2)). % 9.16/9.45 65[0:Res:41.0,31.0] || -> equal(external_ties(sk1,sk3),external_ties(sk1,sk2)) greater(external_ties(sk1,sk3),external_ties(sk1,sk2))*l. % 9.16/9.45 66[0:Res:42.0,31.0] || -> equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2)) greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))*l. % 9.16/9.45 70[0:Res:2.5,40.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). % 9.16/9.45 71[0:Res:1.5,40.0] organization(sk1) || greater(capability(sk1,sk3),capability(sk1,sk2)) greater_or_equal(position(sk1,sk3),position(sk1,sk2))* -> has_immunity(sk1,sk2) has_immunity(sk1,sk3). % 9.16/9.45 72[0:MRR:64.0,9.0] || greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))*l -> greater(capability(sk1,sk3),capability(sk1,sk2)). % 9.16/9.45 75[0:MRR:71.0,71.3,71.4,9.0,10.0,11.0] || greater_or_equal(position(sk1,sk3),position(sk1,sk2))* greater(capability(sk1,sk3),capability(sk1,sk2)) -> . % 9.16/9.45 76[0:MRR:70.0,70.3,70.4,9.0,10.0,11.0] || greater(position(sk1,sk3),position(sk1,sk2)) greater_or_equal(capability(sk1,sk3),capability(sk1,sk2))* -> . % 9.16/9.45 94[1:Spt:66.0] || -> equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))**. % 9.16/9.45 95[1:Rew:94.0,72.0] || greater(stock_of_knowledge(sk1,sk2),stock_of_knowledge(sk1,sk2))* -> greater(capability(sk1,sk3),capability(sk1,sk2)). % 9.16/9.45 96[1:Rew:94.0,14.1] || -> greater(external_ties(sk1,sk3),external_ties(sk1,sk2))*l greater(stock_of_knowledge(sk1,sk2),stock_of_knowledge(sk1,sk2)). % 9.16/9.45 99[2:Spt:65.0] || -> equal(external_ties(sk1,sk3),external_ties(sk1,sk2))**. % 9.16/9.45 100[2:Rew:99.0,96.0] || -> greater(external_ties(sk1,sk2),external_ties(sk1,sk2))* greater(stock_of_knowledge(sk1,sk2),stock_of_knowledge(sk1,sk2)). % 9.16/9.45 110[0:Res:63.1,34.0] || -> equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2)) greater(internal_friction(sk1,sk2),internal_friction(sk1,sk3))*r. % 9.16/9.45 112[2:SpL:99.0,50.0] || equal(external_ties(sk1,sk2),external_ties(sk1,u))* -> equal(position(sk1,sk3),position(sk1,u)). % 9.16/9.45 114[2:EqR:112.0] || -> equal(position(sk1,sk3),position(sk1,sk2))**. % 9.16/9.45 118[2:Rew:114.0,75.0] || greater_or_equal(position(sk1,sk2),position(sk1,sk2))* greater(capability(sk1,sk3),capability(sk1,sk2)) -> . % 9.16/9.45 172[2:Res:33.1,118.0] || equal(position(sk1,sk2),position(sk1,sk2))* greater(capability(sk1,sk3),capability(sk1,sk2)) -> . % 9.16/9.45 173[2:Obv:172.0] || greater(capability(sk1,sk3),capability(sk1,sk2))*l -> . % 9.16/9.45 174[2:MRR:95.1,173.0] || greater(stock_of_knowledge(sk1,sk2),stock_of_knowledge(sk1,sk2))* -> . % 9.16/9.45 175[2:MRR:100.1,174.0] || -> greater(external_ties(sk1,sk2),external_ties(sk1,sk2))*. % 9.16/9.45 176[2:Res:175.0,36.0] || greater(external_ties(sk1,sk2),external_ties(sk1,sk2))* -> . % 9.16/9.45 177[2:MRR:176.0,175.0] || -> . % 9.16/9.45 178[2:Spt:177.0,65.0,99.0] || equal(external_ties(sk1,sk3),external_ties(sk1,sk2))** -> . % 9.16/9.45 179[2:Spt:177.0,65.1] || -> greater(external_ties(sk1,sk3),external_ties(sk1,sk2))*l. % 9.16/9.45 186[0:Res:41.0,31.0] || -> equal(external_ties(sk1,sk3),external_ties(sk1,sk2)) greater(external_ties(sk1,sk3),external_ties(sk1,sk2))*l. % 9.16/9.45 191[3:Spt:63.0] || -> equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2))**. % 9.16/9.45 205[0:Res:32.1,76.1] || greater(capability(sk1,sk3),capability(sk1,sk2)) greater(position(sk1,sk3),position(sk1,sk2))*l -> . % 9.16/9.45 206[0:Res:33.1,76.1] || equal(capability(sk1,sk3),capability(sk1,sk2)) greater(position(sk1,sk3),position(sk1,sk2))*l -> . % 9.16/9.45 208[0:Res:33.1,75.0] || equal(position(sk1,sk3),position(sk1,sk2))** greater(capability(sk1,sk3),capability(sk1,sk2)) -> . % 9.16/9.45 217[3:SpL:191.0,6.1] organization(sk1) || equal(internal_friction(sk1,u),internal_friction(sk1,sk2))* equal(stock_of_knowledge(sk1,u),stock_of_knowledge(sk1,sk3)) -> equal(capability(sk1,u),capability(sk1,sk3)). % 9.16/9.45 218[3:Rew:94.0,217.2] organization(sk1) || equal(internal_friction(sk1,u),internal_friction(sk1,sk2))* equal(stock_of_knowledge(sk1,u),stock_of_knowledge(sk1,sk2)) -> equal(capability(sk1,u),capability(sk1,sk3)). % 9.16/9.45 219[3:SSi:218.0,9.0] || equal(internal_friction(sk1,u),internal_friction(sk1,sk2))* equal(stock_of_knowledge(sk1,u),stock_of_knowledge(sk1,sk2)) -> equal(capability(sk1,u),capability(sk1,sk3)). % 9.36/9.69 248[2:Res:179.0,7.1] organization(sk1) || -> greater(position(sk1,sk3),position(sk1,sk2))*l. % 9.36/9.69 263[2:SSi:248.0,9.0] || -> greater(position(sk1,sk3),position(sk1,sk2))*l. % 9.36/9.69 265[2:MRR:206.1,263.0] || equal(capability(sk1,sk3),capability(sk1,sk2))** -> . % 9.36/9.69 266[2:MRR:205.1,263.0] || greater(capability(sk1,sk3),capability(sk1,sk2))*l -> . % 9.36/9.69 289[0:Res:30.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))*. % 9.36/9.69 533[3:EqR:219.0] || equal(stock_of_knowledge(sk1,sk2),stock_of_knowledge(sk1,sk2))* -> equal(capability(sk1,sk3),capability(sk1,sk2)). % 9.36/9.69 535[3:Obv:533.0] || -> equal(capability(sk1,sk3),capability(sk1,sk2))**. % 9.36/9.69 536[3:MRR:535.0,265.0] || -> . % 9.36/9.69 537[3:Spt:536.0,63.0,191.0] || equal(internal_friction(sk1,sk3),internal_friction(sk1,sk2))** -> . % 9.36/9.69 538[3:Spt:536.0,63.1] || -> smaller(internal_friction(sk1,sk3),internal_friction(sk1,sk2))*. % 9.36/9.69 539[3:MRR:110.0,537.0] || -> greater(internal_friction(sk1,sk2),internal_friction(sk1,sk3))*r. % 9.36/9.69 1794[0:Res:289.3,34.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)). % 9.36/9.69 1827[0:Res:39.0,45.0] || greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))*l -> greater(capability(sk1,sk3),capability(sk1,sk2)). % 9.36/9.69 14369[3:Res:539.0,1794.2] organization(sk1) || equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))** -> greater(capability(sk1,sk3),capability(sk1,sk2)). % 9.36/9.69 14442[3:Rew:94.0,14369.1] organization(sk1) || equal(stock_of_knowledge(sk1,sk2),stock_of_knowledge(sk1,sk2))* -> greater(capability(sk1,sk3),capability(sk1,sk2)). % 9.36/9.69 14443[3:Obv:14442.1] organization(sk1) || -> greater(capability(sk1,sk3),capability(sk1,sk2))*l. % 9.36/9.69 14444[3:SSi:14443.0,9.0] || -> greater(capability(sk1,sk3),capability(sk1,sk2))*l. % 9.36/9.69 14445[3:MRR:14444.0,266.0] || -> . % 9.36/9.69 14510[1:Spt:14445.0,66.0,94.0] || equal(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))** -> . % 9.36/9.69 14511[1:Spt:14445.0,66.1] || -> greater(stock_of_knowledge(sk1,sk3),stock_of_knowledge(sk1,sk2))*l. % 9.36/9.69 14514[1:MRR:1827.0,14511.0] || -> greater(capability(sk1,sk3),capability(sk1,sk2))*l. % 9.36/9.69 14515[1:MRR:208.1,14514.0] || equal(position(sk1,sk3),position(sk1,sk2))** -> . % 9.36/9.69 14517[1:MRR:205.0,14514.0] || greater(position(sk1,sk3),position(sk1,sk2))*l -> . % 9.36/9.69 14736[0:Res:186.1,48.0] || -> equal(external_ties(sk1,sk3),external_ties(sk1,sk2))** greater(position(sk1,sk3),position(sk1,sk2)). % 9.36/9.69 14768[1:MRR:14736.1,14517.0] || -> equal(external_ties(sk1,sk3),external_ties(sk1,sk2))**. % 9.36/9.69 14775[1:SpL:14768.0,50.0] || equal(external_ties(sk1,u),external_ties(sk1,sk2))* -> equal(position(sk1,u),position(sk1,sk3)). % 9.36/9.69 14790[1:EqR:14775.0] || -> equal(position(sk1,sk3),position(sk1,sk2))**. % 9.36/9.69 14792[1:MRR:14790.0,14515.0] || -> . % 9.36/9.69 % SZS output end Refutation % 9.36/9.69 Formulae used in the proof : assumption_4_38 assumption_4_39 assumption_5_41 assumption_5_42 assumption_5_43 assumption_6_44 assumption_6_45 lemma_1_46 lemma_1_47 lemma_1_48 lemma_1_49 lemma_1_51 lemma_1_54 lemma_1_57 lemma_1_64 definition_smaller_or_equal_1 definition_smaller_or_equal_3 definition_greater_or_equal_4 definition_greater_or_equal_5 definition_greater_or_equal_6 definition_smaller_7 meaning_postulate_greater_strict_9 % 9.36/9.69 %------------------------------------------------------------------------------