%------------------------------------------------------------------------------ % 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 : 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:54 AM UTC 2026 % Result : Theorem 64.96s 65.20s % Output : Refutation 68.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT042+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.08/0.34 % Computer : n018.cluster.edu % 0.08/0.34 % Model : x86_64 x86_64 % 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.34 % Memory : 8046.5625MB % 0.08/0.34 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Mon Sep 7 13:05:22 UTC 2026 % 0.08/0.35 % CPUTime : % 64.96/65.20 % 64.96/65.20 SPASS V 3.9 % 64.96/65.20 SPASS beiseite: Proof found. % 64.96/65.20 % SZS status Theorem % 64.96/65.20 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 64.96/65.20 SPASS derived 26484 clauses, backtracked 2539 clauses, performed 20 splits and kept 8902 clauses. % 64.96/65.20 SPASS allocated 121590 KBytes. % 64.96/65.20 SPASS spent 0:01:04.78 on the problem. % 64.96/65.20 0:00:00.06 for the input. % 64.96/65.20 0:00:00.05 for the FLOTTER CNF translation. % 64.96/65.20 0:00:01.07 for inferences. % 64.96/65.20 0:00:00.59 for the backtracking. % 64.96/65.20 0:01:02.84 for the reduction. % 64.96/65.20 % 64.96/65.20 % 64.96/65.20 Here is a proof with depth 5, length 183 : % 64.96/65.20 % SZS output start Refutation % 64.96/65.20 1[0:Inp] || -> organization(skc3)*. % 64.96/65.20 2[0:Inp] || has_immunity(skc3,skc5)* -> . % 64.96/65.20 3[0:Inp] || has_immunity(skc3,skc4)* -> . % 64.96/65.20 5[0:Inp] || equal(u,v) -> smaller_or_equal(u,v)*. % 64.96/65.20 6[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 64.96/65.20 7[0:Inp] || equal(u,v) -> greater_or_equal(u,v)*. % 64.96/65.20 8[0:Inp] || smaller(u,v)* -> greater(v,u). % 64.96/65.20 11[0:Inp] || -> greater(u,v) equal(u,v) smaller(u,v)*. % 64.96/65.20 12[0:Inp] || smaller_or_equal(u,v)* -> equal(u,v) smaller(u,v). % 64.96/65.20 13[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 64.96/65.20 14[0:Inp] || -> greater(stock_of_knowledge(u,v),stock_of_knowledge(u,w)) SkP0(w,v,u)*. % 64.96/65.20 15[0:Inp] || -> smaller_or_equal(internal_friction(u,v),internal_friction(u,w))* SkP0(w,v,u). % 64.96/65.20 16[0:Inp] || -> greater_or_equal(external_ties(u,v),external_ties(u,w))* SkP0(w,v,u). % 64.96/65.20 18[0:Inp] || SkP0(skc5,skc4,skc3) -> greater_or_equal(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5))*. % 64.96/65.20 19[0:Inp] || SkP0(skc5,skc4,skc3) -> smaller_or_equal(internal_friction(skc3,skc4),internal_friction(skc3,skc5))*. % 64.96/65.20 20[0:Inp] || SkP0(skc5,skc4,skc3)* -> greater(external_ties(skc3,skc4),external_ties(skc3,skc5)). % 64.96/65.20 21[0:Inp] || smaller(hazard_of_mortality(u,v),hazard_of_mortality(u,w))* -> SkP0(w,v,u). % 64.96/65.20 22[0:Inp] || smaller(hazard_of_mortality(skc3,skc4),hazard_of_mortality(skc3,skc5))* SkP0(skc5,skc4,skc3) -> . % 64.96/65.20 23[0:Inp] organization(u) || greater(external_ties(u,v),external_ties(u,w))* -> greater(position(u,v),position(u,w)). % 64.96/65.20 24[0:Inp] organization(u) || equal(external_ties(u,v),external_ties(u,w))* -> equal(position(u,v),position(u,w)). % 64.96/65.20 25[0:Inp] organization(u) || equal(stock_of_knowledge(u,v),stock_of_knowledge(u,w)) equal(internal_friction(u,v),internal_friction(u,w))* -> equal(capability(u,v),capability(u,w)). % 64.96/65.20 26[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)). % 64.96/65.20 27[0:Inp] organization(u) || greater(stock_of_knowledge(u,v),stock_of_knowledge(u,w)) smaller_or_equal(internal_friction(u,v),internal_friction(u,w))* -> greater(capability(u,v),capability(u,w)). % 64.96/65.20 29[0:Inp] organization(u) || greater_or_equal(capability(u,v),capability(u,w)) greater(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))*. % 64.96/65.20 30[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))*. % 64.96/65.20 31[0:MRR:19.0,15.1] || -> smaller_or_equal(internal_friction(skc3,skc4),internal_friction(skc3,skc5))*. % 64.96/65.20 32[0:MRR:22.1,21.1] || smaller(hazard_of_mortality(skc3,skc4),hazard_of_mortality(skc3,skc5))* -> . % 64.96/65.20 35[0:Res:1.0,27.0] || greater(stock_of_knowledge(skc3,u),stock_of_knowledge(skc3,v)) smaller_or_equal(internal_friction(skc3,u),internal_friction(skc3,v))* -> greater(capability(skc3,u),capability(skc3,v)). % 64.96/65.20 38[0:Res:1.0,23.0] || greater(external_ties(skc3,u),external_ties(skc3,v))* -> greater(position(skc3,u),position(skc3,v)). % 64.96/65.20 39[0:Res:1.0,25.0] || equal(stock_of_knowledge(skc3,u),stock_of_knowledge(skc3,v)) equal(internal_friction(skc3,u),internal_friction(skc3,v))* -> equal(capability(skc3,u),capability(skc3,v)). % 64.96/65.20 40[0:Res:1.0,24.0] || equal(external_ties(skc3,u),external_ties(skc3,v))* -> equal(position(skc3,u),position(skc3,v)). % 64.96/65.20 44[0:Res:30.5,3.0] organization(skc3) || greater_or_equal(position(skc3,skc4),position(skc3,u)) greater(capability(skc3,skc4),capability(skc3,u)) -> smaller(hazard_of_mortality(skc3,skc4),hazard_of_mortality(skc3,u))* has_immunity(skc3,u). % 64.96/65.20 53[0:Res:31.0,12.0] || -> equal(internal_friction(skc3,skc5),internal_friction(skc3,skc4)) smaller(internal_friction(skc3,skc4),internal_friction(skc3,skc5))*. % 64.96/65.20 54[0:Res:31.0,27.1] organization(skc3) || greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5))*r -> greater(capability(skc3,skc4),capability(skc3,skc5)). % 64.96/65.20 55[0:Res:11.0,32.0] || -> greater(hazard_of_mortality(skc3,skc4),hazard_of_mortality(skc3,skc5))*r equal(hazard_of_mortality(skc3,skc5),hazard_of_mortality(skc3,skc4)). % 64.96/65.20 57[0:Res:30.3,32.0] organization(skc3) || greater_or_equal(position(skc3,skc4),position(skc3,skc5))* greater(capability(skc3,skc4),capability(skc3,skc5)) -> has_immunity(skc3,skc5) has_immunity(skc3,skc4). % 64.96/65.20 58[0:Res:29.3,32.0] organization(skc3) || greater(position(skc3,skc4),position(skc3,skc5)) greater_or_equal(capability(skc3,skc4),capability(skc3,skc5))* -> has_immunity(skc3,skc5) has_immunity(skc3,skc4). % 64.96/65.20 60[0:MRR:54.0,1.0] || greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5))*r -> greater(capability(skc3,skc4),capability(skc3,skc5)). % 64.96/65.20 63[0:MRR:58.0,58.3,58.4,1.0,2.0,3.0] || greater_or_equal(capability(skc3,skc4),capability(skc3,skc5))* greater(position(skc3,skc4),position(skc3,skc5)) -> . % 64.96/65.20 64[0:MRR:57.0,57.3,57.4,1.0,2.0,3.0] || greater(capability(skc3,skc4),capability(skc3,skc5)) greater_or_equal(position(skc3,skc4),position(skc3,skc5))* -> . % 64.96/65.20 70[0:MRR:44.0,1.0] || greater(capability(skc3,skc4),capability(skc3,u)) greater_or_equal(position(skc3,skc4),position(skc3,u)) -> has_immunity(skc3,u) smaller(hazard_of_mortality(skc3,skc4),hazard_of_mortality(skc3,u))*. % 64.96/65.20 89[1:Spt:55.1] || -> equal(hazard_of_mortality(skc3,skc5),hazard_of_mortality(skc3,skc4))**. % 64.96/65.20 98[1:Rew:89.0,32.0] || smaller(hazard_of_mortality(skc3,skc4),hazard_of_mortality(skc3,skc4))* -> . % 64.96/65.20 124[0:Res:53.1,8.0] || -> equal(internal_friction(skc3,skc5),internal_friction(skc3,skc4)) greater(internal_friction(skc3,skc5),internal_friction(skc3,skc4))*l. % 64.96/65.20 128[0:Res:16.0,13.0] || -> SkP0(u,v,w)* equal(external_ties(w,v),external_ties(w,u)) greater(external_ties(w,v),external_ties(w,u)). % 64.96/65.20 129[0:Res:18.1,13.0] || SkP0(skc5,skc4,skc3)* -> equal(stock_of_knowledge(skc3,skc5),stock_of_knowledge(skc3,skc4)) greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5)). % 64.96/65.20 130[0:MRR:129.0,14.1] || -> equal(stock_of_knowledge(skc3,skc5),stock_of_knowledge(skc3,skc4)) greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5))*r. % 64.96/65.20 131[0:Res:14.1,20.0] || -> greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5)) greater(external_ties(skc3,skc4),external_ties(skc3,skc5))*r. % 64.96/65.20 137[2:Spt:124.0] || -> equal(internal_friction(skc3,skc5),internal_friction(skc3,skc4))**. % 64.96/65.20 138[2:Rew:137.0,31.0] || -> smaller_or_equal(internal_friction(skc3,skc4),internal_friction(skc3,skc4))*. % 64.96/65.20 151[2:SpL:137.0,25.2] organization(skc3) || equal(stock_of_knowledge(skc3,u),stock_of_knowledge(skc3,skc5)) equal(internal_friction(skc3,u),internal_friction(skc3,skc4))* -> equal(capability(skc3,u),capability(skc3,skc5)). % 64.96/65.20 152[2:SSi:151.0,1.0] || equal(stock_of_knowledge(skc3,u),stock_of_knowledge(skc3,skc5)) equal(internal_friction(skc3,u),internal_friction(skc3,skc4))* -> equal(capability(skc3,u),capability(skc3,skc5)). % 64.96/65.20 159[3:Spt:130.0] || -> equal(stock_of_knowledge(skc3,skc5),stock_of_knowledge(skc3,skc4))**. % 64.96/65.20 161[3:Rew:159.0,131.0] || -> greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc4)) greater(external_ties(skc3,skc4),external_ties(skc3,skc5))*r. % 64.96/65.20 163[3:Rew:159.0,152.0] || equal(stock_of_knowledge(skc3,u),stock_of_knowledge(skc3,skc4)) equal(internal_friction(skc3,u),internal_friction(skc3,skc4))* -> equal(capability(skc3,u),capability(skc3,skc5)). % 64.96/65.20 197[0:Res:6.1,64.1] || greater(position(skc3,skc4),position(skc3,skc5))*r greater(capability(skc3,skc4),capability(skc3,skc5)) -> . % 64.96/65.20 198[0:Res:7.1,64.1] || equal(position(skc3,skc5),position(skc3,skc4))** greater(capability(skc3,skc4),capability(skc3,skc5)) -> . % 64.96/65.20 200[0:Res:7.1,63.0] || equal(capability(skc3,skc5),capability(skc3,skc4)) greater(position(skc3,skc4),position(skc3,skc5))*r -> . % 64.96/65.20 230[0:Res:5.1,26.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))*. % 64.96/65.20 312[2:Res:138.0,27.2] organization(skc3) || greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc4))* -> greater(capability(skc3,skc4),capability(skc3,skc4)). % 64.96/65.20 317[2:SSi:312.0,1.0] || greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc4))* -> greater(capability(skc3,skc4),capability(skc3,skc4)). % 64.96/65.20 348[1:Res:30.5,98.0] organization(skc3) || greater(capability(skc3,skc4),capability(skc3,skc4)) greater_or_equal(position(skc3,skc4),position(skc3,skc4))* -> has_immunity(skc3,skc4) has_immunity(skc3,skc4). % 64.96/65.20 352[1:Obv:348.3] organization(skc3) || greater(capability(skc3,skc4),capability(skc3,skc4)) greater_or_equal(position(skc3,skc4),position(skc3,skc4))* -> has_immunity(skc3,skc4). % 64.96/65.20 353[1:SSi:352.0,1.0] || greater(capability(skc3,skc4),capability(skc3,skc4)) greater_or_equal(position(skc3,skc4),position(skc3,skc4))* -> has_immunity(skc3,skc4). % 64.96/65.20 354[1:MRR:353.2,3.0] || greater(capability(skc3,skc4),capability(skc3,skc4)) greater_or_equal(position(skc3,skc4),position(skc3,skc4))* -> . % 64.96/65.20 365[1:Res:7.1,354.1] || equal(position(skc3,skc4),position(skc3,skc4))* greater(capability(skc3,skc4),capability(skc3,skc4)) -> . % 64.96/65.20 366[1:Obv:365.0] || greater(capability(skc3,skc4),capability(skc3,skc4))* -> . % 64.96/65.20 367[2:MRR:317.1,366.0] || greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc4))* -> . % 64.96/65.20 368[3:MRR:161.0,367.0] || -> greater(external_ties(skc3,skc4),external_ties(skc3,skc5))*r. % 64.96/65.20 370[3:Res:368.0,23.1] organization(skc3) || -> greater(position(skc3,skc4),position(skc3,skc5))*r. % 64.96/65.20 377[3:SSi:370.0,1.0] || -> greater(position(skc3,skc4),position(skc3,skc5))*r. % 64.96/65.20 378[3:MRR:63.1,377.0] || greater_or_equal(capability(skc3,skc4),capability(skc3,skc5))* -> . % 64.96/65.20 383[3:Res:7.1,378.0] || equal(capability(skc3,skc5),capability(skc3,skc4))** -> . % 64.96/65.20 694[3:EqR:163.1] || equal(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc4))* -> equal(capability(skc3,skc5),capability(skc3,skc4)). % 64.96/65.20 696[3:Obv:694.0] || -> equal(capability(skc3,skc5),capability(skc3,skc4))**. % 64.96/65.20 697[3:MRR:696.0,383.0] || -> . % 64.96/65.20 698[3:Spt:697.0,130.0,159.0] || equal(stock_of_knowledge(skc3,skc5),stock_of_knowledge(skc3,skc4))** -> . % 64.96/65.20 699[3:Spt:697.0,130.1] || -> greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5))*r. % 64.96/65.20 700[3:MRR:60.0,699.0] || -> greater(capability(skc3,skc4),capability(skc3,skc5))*r. % 64.96/65.20 702[3:MRR:198.1,700.0] || equal(position(skc3,skc5),position(skc3,skc4))** -> . % 64.96/65.20 704[3:MRR:197.1,700.0] || greater(position(skc3,skc4),position(skc3,skc5))*r -> . % 64.96/65.20 712[4:Spt:18.0] || SkP0(skc5,skc4,skc3)* -> . % 64.96/65.20 722[4:Res:128.0,712.0] || -> equal(external_ties(skc3,skc5),external_ties(skc3,skc4)) greater(external_ties(skc3,skc4),external_ties(skc3,skc5))*r. % 64.96/65.20 874[4:Res:722.1,38.0] || -> equal(external_ties(skc3,skc5),external_ties(skc3,skc4))** greater(position(skc3,skc4),position(skc3,skc5)). % 64.96/65.20 887[4:MRR:874.1,704.0] || -> equal(external_ties(skc3,skc5),external_ties(skc3,skc4))**. % 64.96/65.20 895[4:SpL:887.0,40.0] || equal(external_ties(skc3,u),external_ties(skc3,skc4))* -> equal(position(skc3,u),position(skc3,skc5)). % 64.96/65.20 906[4:EqR:895.0] || -> equal(position(skc3,skc5),position(skc3,skc4))**. % 64.96/65.20 908[4:MRR:906.0,702.0] || -> . % 64.96/65.20 909[4:Spt:908.0,18.0,712.0] || -> SkP0(skc5,skc4,skc3)*. % 64.96/65.20 910[4:Spt:908.0,18.1] || -> greater_or_equal(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5))*. % 64.96/65.20 911[4:MRR:20.0,909.0] || -> greater(external_ties(skc3,skc4),external_ties(skc3,skc5))*r. % 64.96/65.20 914[4:Res:911.0,23.1] organization(skc3) || -> greater(position(skc3,skc4),position(skc3,skc5))*r. % 64.96/65.20 929[4:SSi:914.0,1.0] || -> greater(position(skc3,skc4),position(skc3,skc5))*r. % 64.96/65.20 930[4:MRR:929.0,704.0] || -> . % 64.96/65.20 931[2:Spt:930.0,124.0,137.0] || equal(internal_friction(skc3,skc5),internal_friction(skc3,skc4))** -> . % 64.96/65.20 932[2:Spt:930.0,124.1] || -> greater(internal_friction(skc3,skc5),internal_friction(skc3,skc4))*l. % 64.96/65.20 942[3:Spt:18.0] || SkP0(skc5,skc4,skc3)* -> . % 64.96/65.20 947[3:Res:14.1,942.0] || -> greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5))*r. % 64.96/65.20 952[3:Res:128.0,942.0] || -> equal(external_ties(skc3,skc5),external_ties(skc3,skc4)) greater(external_ties(skc3,skc4),external_ties(skc3,skc5))*r. % 64.96/65.20 953[3:MRR:60.0,947.0] || -> greater(capability(skc3,skc4),capability(skc3,skc5))*r. % 64.96/65.20 955[3:MRR:198.1,953.0] || equal(position(skc3,skc5),position(skc3,skc4))** -> . % 64.96/65.20 957[3:MRR:197.1,953.0] || greater(position(skc3,skc4),position(skc3,skc5))*r -> . % 64.96/65.20 1121[0:Res:70.3,21.0] || greater(capability(skc3,skc4),capability(skc3,u)) greater_or_equal(position(skc3,skc4),position(skc3,u))* -> has_immunity(skc3,u) SkP0(u,skc4,skc3). % 64.96/65.20 1134[3:Res:952.1,38.0] || -> equal(external_ties(skc3,skc5),external_ties(skc3,skc4))** greater(position(skc3,skc4),position(skc3,skc5)). % 64.96/65.20 1147[3:MRR:1134.1,957.0] || -> equal(external_ties(skc3,skc5),external_ties(skc3,skc4))**. % 64.96/65.20 1155[3:SpL:1147.0,40.0] || equal(external_ties(skc3,u),external_ties(skc3,skc4))* -> equal(position(skc3,u),position(skc3,skc5)). % 64.96/65.20 1197[3:EqR:1155.0] || -> equal(position(skc3,skc5),position(skc3,skc4))**. % 64.96/65.20 1199[3:MRR:1197.0,955.0] || -> . % 64.96/65.20 1200[3:Spt:1199.0,18.0,942.0] || -> SkP0(skc5,skc4,skc3)*. % 64.96/65.20 1201[3:Spt:1199.0,18.1] || -> greater_or_equal(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5))*. % 64.96/65.20 1202[3:MRR:20.0,1200.0] || -> greater(external_ties(skc3,skc4),external_ties(skc3,skc5))*r. % 64.96/65.20 1206[3:Res:1202.0,38.0] || -> greater(position(skc3,skc4),position(skc3,skc5))*r. % 64.96/65.20 1216[3:MRR:197.0,1206.0] || greater(capability(skc3,skc4),capability(skc3,skc5))*r -> . % 64.96/65.20 1217[3:MRR:60.1,1216.0] || greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5))*r -> . % 64.96/65.20 1218[3:MRR:130.1,1217.0] || -> equal(stock_of_knowledge(skc3,skc5),stock_of_knowledge(skc3,skc4))**. % 64.96/65.20 1937[0:Res:230.3,8.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)). % 64.96/65.20 2117[0:Res:15.0,35.1] || greater(stock_of_knowledge(skc3,u),stock_of_knowledge(skc3,v)) -> SkP0(v,u,skc3)* greater(capability(skc3,u),capability(skc3,v)). % 64.96/65.20 2122[0:MRR:2117.0,14.0] || -> SkP0(u,v,skc3)* greater(capability(skc3,v),capability(skc3,u)). % 64.96/65.20 2124[0:MRR:1121.0,2122.1] || greater_or_equal(position(skc3,skc4),position(skc3,u))* -> has_immunity(skc3,u) SkP0(u,skc4,skc3). % 64.96/65.20 2130[0:Res:7.1,2124.0] || equal(position(skc3,skc4),position(skc3,u)) -> has_immunity(skc3,u) SkP0(u,skc4,skc3)*. % 64.96/65.20 26808[0:Res:31.0,35.1] || greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5))*r -> greater(capability(skc3,skc4),capability(skc3,skc5)). % 64.96/65.20 27034[2:Res:932.0,1937.2] organization(skc3) || equal(stock_of_knowledge(skc3,skc5),stock_of_knowledge(skc3,skc4))** -> greater(capability(skc3,skc4),capability(skc3,skc5)). % 64.96/65.20 27095[3:Rew:1218.0,27034.1] organization(skc3) || equal(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc4))* -> greater(capability(skc3,skc4),capability(skc3,skc5)). % 64.96/65.20 27096[3:Obv:27095.1] organization(skc3) || -> greater(capability(skc3,skc4),capability(skc3,skc5))*r. % 64.96/65.20 27097[3:SSi:27096.0,1.0] || -> greater(capability(skc3,skc4),capability(skc3,skc5))*r. % 64.96/65.20 27098[3:MRR:27097.0,1216.0] || -> . % 64.96/65.20 27113[1:Spt:27098.0,55.1,89.0] || equal(hazard_of_mortality(skc3,skc5),hazard_of_mortality(skc3,skc4))** -> . % 64.96/65.20 27114[1:Spt:27098.0,55.0] || -> greater(hazard_of_mortality(skc3,skc4),hazard_of_mortality(skc3,skc5))*r. % 64.96/65.20 27217[2:Spt:53.0] || -> equal(internal_friction(skc3,skc5),internal_friction(skc3,skc4))**. % 64.96/65.20 27239[2:SpL:27217.0,39.1] || equal(stock_of_knowledge(skc3,u),stock_of_knowledge(skc3,skc5)) equal(internal_friction(skc3,u),internal_friction(skc3,skc4))* -> equal(capability(skc3,u),capability(skc3,skc5)). % 64.96/65.20 27261[3:Spt:20.0] || SkP0(skc5,skc4,skc3)* -> . % 64.96/65.20 27268[3:Res:2122.0,27261.0] || -> greater(capability(skc3,skc4),capability(skc3,skc5))*r. % 64.96/65.20 27272[3:Res:128.0,27261.0] || -> equal(external_ties(skc3,skc5),external_ties(skc3,skc4)) greater(external_ties(skc3,skc4),external_ties(skc3,skc5))*r. % 64.96/65.20 27275[3:MRR:198.1,27268.0] || equal(position(skc3,skc5),position(skc3,skc4))** -> . % 68.26/68.58 27276[3:MRR:197.1,27268.0] || greater(position(skc3,skc4),position(skc3,skc5))*r -> . % 68.26/68.58 27702[4:Spt:27272.0] || -> equal(external_ties(skc3,skc5),external_ties(skc3,skc4))**. % 68.26/68.58 27718[4:SpL:27702.0,40.0] || equal(external_ties(skc3,u),external_ties(skc3,skc4))* -> equal(position(skc3,u),position(skc3,skc5)). % 68.26/68.58 27756[4:EqR:27718.0] || -> equal(position(skc3,skc5),position(skc3,skc4))**. % 68.26/68.58 27758[4:MRR:27756.0,27275.0] || -> . % 68.26/68.58 27759[4:Spt:27758.0,27272.0,27702.0] || equal(external_ties(skc3,skc5),external_ties(skc3,skc4))** -> . % 68.26/68.58 27760[4:Spt:27758.0,27272.1] || -> greater(external_ties(skc3,skc4),external_ties(skc3,skc5))*r. % 68.26/68.58 27766[4:Res:27760.0,23.1] organization(skc3) || -> greater(position(skc3,skc4),position(skc3,skc5))*r. % 68.26/68.58 27805[4:SSi:27766.0,1.0] || -> greater(position(skc3,skc4),position(skc3,skc5))*r. % 68.26/68.58 27806[4:MRR:27805.0,27276.0] || -> . % 68.26/68.58 27807[3:Spt:27806.0,20.0,27261.0] || -> SkP0(skc5,skc4,skc3)*. % 68.26/68.58 27808[3:Spt:27806.0,20.1] || -> greater(external_ties(skc3,skc4),external_ties(skc3,skc5))*r. % 68.26/68.58 27816[3:Res:27808.0,38.0] || -> greater(position(skc3,skc4),position(skc3,skc5))*r. % 68.26/68.58 27850[3:MRR:200.1,27816.0] || equal(capability(skc3,skc5),capability(skc3,skc4))** -> . % 68.26/68.58 27851[3:MRR:197.0,27816.0] || greater(capability(skc3,skc4),capability(skc3,skc5))*r -> . % 68.26/68.58 27852[3:MRR:26808.1,27851.0] || greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5))*r -> . % 68.26/68.58 27853[3:MRR:130.1,27852.0] || -> equal(stock_of_knowledge(skc3,skc5),stock_of_knowledge(skc3,skc4))**. % 68.26/68.58 27855[3:Rew:27853.0,27239.0] || equal(stock_of_knowledge(skc3,u),stock_of_knowledge(skc3,skc4)) equal(internal_friction(skc3,u),internal_friction(skc3,skc4))* -> equal(capability(skc3,u),capability(skc3,skc5)). % 68.26/68.58 29196[3:EqR:27855.1] || equal(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc4))* -> equal(capability(skc3,skc5),capability(skc3,skc4)). % 68.26/68.58 29198[3:Obv:29196.0] || -> equal(capability(skc3,skc5),capability(skc3,skc4))**. % 68.26/68.58 29199[3:MRR:29198.0,27850.0] || -> . % 68.26/68.58 29200[2:Spt:29199.0,53.0,27217.0] || equal(internal_friction(skc3,skc5),internal_friction(skc3,skc4))** -> . % 68.26/68.58 29201[2:Spt:29199.0,53.1] || -> smaller(internal_friction(skc3,skc4),internal_friction(skc3,skc5))*. % 68.26/68.58 29202[2:MRR:124.0,29200.0] || -> greater(internal_friction(skc3,skc5),internal_friction(skc3,skc4))*l. % 68.26/68.58 29215[2:Res:29202.0,1937.2] organization(skc3) || equal(stock_of_knowledge(skc3,skc5),stock_of_knowledge(skc3,skc4))** -> greater(capability(skc3,skc4),capability(skc3,skc5)). % 68.26/68.58 29244[2:SSi:29215.0,1.0] || equal(stock_of_knowledge(skc3,skc5),stock_of_knowledge(skc3,skc4))** -> greater(capability(skc3,skc4),capability(skc3,skc5)). % 68.26/68.58 29260[3:Spt:20.0] || SkP0(skc5,skc4,skc3)* -> . % 68.26/68.58 29267[3:Res:2122.0,29260.0] || -> greater(capability(skc3,skc4),capability(skc3,skc5))*r. % 68.26/68.58 29269[3:Res:2130.2,29260.0] || equal(position(skc3,skc5),position(skc3,skc4))** -> has_immunity(skc3,skc5). % 68.26/68.58 29275[3:Res:128.0,29260.0] || -> equal(external_ties(skc3,skc5),external_ties(skc3,skc4)) greater(external_ties(skc3,skc4),external_ties(skc3,skc5))*r. % 68.26/68.58 29276[3:MRR:29269.1,2.0] || equal(position(skc3,skc5),position(skc3,skc4))** -> . % 68.26/68.58 29279[3:MRR:197.1,29267.0] || greater(position(skc3,skc4),position(skc3,skc5))*r -> . % 68.26/68.58 29410[4:Spt:29275.0] || -> equal(external_ties(skc3,skc5),external_ties(skc3,skc4))**. % 68.26/68.58 29426[4:SpL:29410.0,40.0] || equal(external_ties(skc3,u),external_ties(skc3,skc4))* -> equal(position(skc3,u),position(skc3,skc5)). % 68.26/68.58 29441[4:EqR:29426.0] || -> equal(position(skc3,skc5),position(skc3,skc4))**. % 68.26/68.58 29443[4:MRR:29441.0,29276.0] || -> . % 68.26/68.58 29444[4:Spt:29443.0,29275.0,29410.0] || equal(external_ties(skc3,skc5),external_ties(skc3,skc4))** -> . % 68.26/68.58 29445[4:Spt:29443.0,29275.1] || -> greater(external_ties(skc3,skc4),external_ties(skc3,skc5))*r. % 68.26/68.58 29451[4:Res:29445.0,23.1] organization(skc3) || -> greater(position(skc3,skc4),position(skc3,skc5))*r. % 68.26/68.58 29487[4:SSi:29451.0,1.0] || -> greater(position(skc3,skc4),position(skc3,skc5))*r. % 68.26/68.58 29488[4:MRR:29487.0,29279.0] || -> . % 68.26/68.58 29489[3:Spt:29488.0,20.0,29260.0] || -> SkP0(skc5,skc4,skc3)*. % 68.26/68.58 29490[3:Spt:29488.0,20.1] || -> greater(external_ties(skc3,skc4),external_ties(skc3,skc5))*r. % 68.26/68.58 29498[3:Res:29490.0,38.0] || -> greater(position(skc3,skc4),position(skc3,skc5))*r. % 68.26/68.58 29534[3:MRR:197.0,29498.0] || greater(capability(skc3,skc4),capability(skc3,skc5))*r -> . % 68.26/68.58 29535[3:MRR:29244.1,29534.0] || equal(stock_of_knowledge(skc3,skc5),stock_of_knowledge(skc3,skc4))** -> . % 68.26/68.58 29536[3:MRR:26808.1,29534.0] || greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5))*r -> . % 68.26/68.58 29537[3:MRR:130.0,29535.0] || -> greater(stock_of_knowledge(skc3,skc4),stock_of_knowledge(skc3,skc5))*r. % 68.26/68.58 29538[3:MRR:29536.0,29537.0] || -> . % 68.26/68.58 % SZS output end Refutation % 68.26/68.58 Formulae used in the proof : lemma_1 definition_smaller_or_equal definition_greater_or_equal definition_smaller meaning_postulate_greater_comparable assumption_6 assumption_5 assumption_4 % 68.26/68.58 %------------------------------------------------------------------------------