%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT063+1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n014.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:58 AM UTC 2026 % Result : Theorem 1.07s 1.30s % Output : Refutation 1.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT063+1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.04 % Command : run_spass %d %s % 0.11/0.36 % Computer : n014.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:40:26 UTC 2026 % 0.11/0.36 % CPUTime : % 1.07/1.30 % 1.07/1.30 SPASS V 3.9 % 1.07/1.30 SPASS beiseite: Proof found. % 1.07/1.30 % SZS status Theorem % 1.07/1.30 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.07/1.30 SPASS derived 3283 clauses, backtracked 608 clauses, performed 6 splits and kept 1793 clauses. % 1.07/1.30 SPASS allocated 100003 KBytes. % 1.07/1.30 SPASS spent 0:00:00.92 on the problem. % 1.07/1.30 0:00:00.06 for the input. % 1.07/1.30 0:00:00.06 for the FLOTTER CNF translation. % 1.07/1.30 0:00:00.05 for inferences. % 1.07/1.30 0:00:00.01 for the backtracking. % 1.07/1.30 0:00:00.69 for the reduction. % 1.07/1.30 % 1.07/1.30 % 1.07/1.30 Here is a proof with depth 5, length 166 : % 1.07/1.30 % SZS output start Refutation % 1.07/1.30 1[0:Inp] || -> organization(skc5)*. % 1.07/1.30 2[0:Inp] || -> robust_position(skc5)*. % 1.07/1.30 3[0:Inp] || has_endowment(skc5)* -> . % 1.07/1.30 4[0:Inp] || -> smaller(sigma,tau)*. % 1.07/1.30 5[0:Inp] || -> greater(tau,zero)*l. % 1.07/1.30 10[0:Inp] || -> greater(high,mod2)*l. % 1.07/1.30 12[0:Inp] || -> greater(mod2,mod1)*l. % 1.07/1.30 13[0:Inp] || -> greater(age(skc5,skc9),tau)*l. % 1.07/1.30 14[0:Inp] || -> smaller_or_equal(age(skc5,skc8),tau)*. % 1.07/1.30 15[0:Inp] || -> greater(age(skc5,skc8),sigma)*l. % 1.07/1.30 16[0:Inp] || -> smaller_or_equal(age(skc5,skc7),sigma)*. % 1.07/1.30 17[0:Inp] || -> equal(age(skc5,skc6),zero)**. % 1.07/1.30 19[0:Inp] || dissimilar(u,v,w)* -> organization(u). % 1.07/1.30 20[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 1.07/1.30 21[0:Inp] || equal(u,v) -> smaller_or_equal(u,v)*. % 1.07/1.30 24[0:Inp] || smaller(u,v)* -> greater(v,u). % 1.07/1.30 25[0:Inp] || greater(u,v) -> smaller(v,u)*. % 1.07/1.30 26[0:Inp] || greater(u,v)*+ greater(v,u)* -> . % 1.07/1.30 27[0:Inp] organization(u) || has_immunity(u,v)* -> has_endowment(u). % 1.07/1.30 28[0:Inp] || -> greater(u,v) equal(u,v) smaller(u,v)*. % 1.07/1.30 29[0:Inp] || smaller_or_equal(u,v) -> equal(u,v) smaller(u,v)*. % 1.07/1.30 33[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 1.07/1.30 35[0:Inp] organization(u) || equal(age(u,v),zero)** -> is_aligned(u,v). % 1.07/1.30 36[0:Inp] robust_position(u) || greater(age(u,v),tau)*l -> positional_advantage(u,v). % 1.07/1.30 40[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)* -> . % 1.07/1.30 41[0:Inp] robust_position(u) || positional_advantage(u,v) smaller_or_equal(age(u,v),tau)* -> . % 1.07/1.30 44[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) dissimilar(u,v,w)*. % 1.07/1.30 50[0:Inp] organization(u) || -> has_immunity(u,v) positional_advantage(u,v) is_aligned(u,v) equal(hazard_of_mortality(u,v),high)**. % 1.07/1.30 51[0:Inp] organization(u) || positional_advantage(u,v) -> has_immunity(u,v) is_aligned(u,v) equal(hazard_of_mortality(u,v),mod1)**. % 1.07/1.30 52[0:Inp] organization(u) || is_aligned(u,v) -> has_immunity(u,v) positional_advantage(u,v) equal(hazard_of_mortality(u,v),mod2)**. % 1.07/1.30 53[0:Inp] organization(u) || greater(age(u,v),sigma) equal(age(u,w),zero) -> dissimilar(u,w,v)*. % 1.07/1.30 54[0:Inp] organization(u) || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 1.07/1.30 56[0:Inp] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc8)) smaller(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7))* -> . % 1.07/1.30 58[0:MRR:54.0,19.1] || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 1.07/1.30 60[0:Res:2.0,41.0] || positional_advantage(skc5,u) smaller_or_equal(age(skc5,u),tau)* -> . % 1.07/1.30 63[0:Res:1.0,51.0] || positional_advantage(skc5,u) -> is_aligned(skc5,u) equal(hazard_of_mortality(skc5,u),mod1)** has_immunity(skc5,u). % 1.07/1.30 64[0:Res:1.0,52.0] || is_aligned(skc5,u) -> positional_advantage(skc5,u) equal(hazard_of_mortality(skc5,u),mod2)** has_immunity(skc5,u). % 1.07/1.30 65[0:Res:1.0,50.0] || -> is_aligned(skc5,u) positional_advantage(skc5,u) equal(hazard_of_mortality(skc5,u),high)** has_immunity(skc5,u). % 1.07/1.30 67[0:Res:1.0,44.0] || is_aligned(skc5,u) -> is_aligned(skc5,v) dissimilar(skc5,u,v)*. % 1.07/1.30 71[0:Res:1.0,27.0] || has_immunity(skc5,u)* -> has_endowment(skc5). % 1.07/1.30 72[0:Res:4.0,24.0] || -> greater(tau,sigma)*l. % 1.07/1.30 73[0:Res:4.0,20.0] || -> smaller_or_equal(sigma,tau)*. % 1.07/1.30 76[0:Res:17.0,58.0] || dissimilar(skc5,skc6,u)* -> greater(age(skc5,u),sigma). % 1.07/1.30 77[0:Res:17.0,53.1] organization(skc5) || greater(age(skc5,u),sigma) -> dissimilar(skc5,skc6,u)*. % 1.07/1.30 78[0:Res:17.0,35.1] organization(skc5) || -> is_aligned(skc5,skc6)*. % 1.07/1.30 83[0:Res:16.0,29.0] || -> equal(age(skc5,skc7),sigma) smaller(age(skc5,skc7),sigma)*. % 1.07/1.30 84[0:Res:14.0,41.2] robust_position(skc5) || positional_advantage(skc5,skc8)* -> . % 1.07/1.30 92[0:Res:5.0,25.0] || -> smaller(zero,tau)*. % 1.07/1.30 94[0:Res:15.0,53.2] organization(skc5) || equal(age(skc5,u),zero) -> dissimilar(skc5,u,skc8)*. % 1.07/1.30 99[0:Res:13.0,36.1] robust_position(skc5) || -> positional_advantage(skc5,skc9)*. % 1.07/1.30 108[0:MRR:71.1,3.0] || has_immunity(skc5,u)* -> . % 1.07/1.30 109[0:MRR:78.0,1.0] || -> is_aligned(skc5,skc6)*. % 1.07/1.30 110[0:MRR:99.0,2.0] || -> positional_advantage(skc5,skc9)*. % 1.07/1.30 111[0:MRR:84.0,2.0] || positional_advantage(skc5,skc8)* -> . % 1.07/1.30 113[0:MRR:94.0,1.0] || equal(age(skc5,u),zero) -> dissimilar(skc5,u,skc8)*. % 1.07/1.30 114[0:MRR:65.3,108.0] || -> positional_advantage(skc5,u) is_aligned(skc5,u) equal(hazard_of_mortality(skc5,u),high)**. % 1.07/1.30 115[0:MRR:63.3,108.0] || positional_advantage(skc5,u) -> is_aligned(skc5,u) equal(hazard_of_mortality(skc5,u),mod1)**. % 1.07/1.30 116[0:MRR:64.3,108.0] || is_aligned(skc5,u) -> positional_advantage(skc5,u) equal(hazard_of_mortality(skc5,u),mod2)**. % 1.07/1.30 118[0:MRR:77.0,1.0] || greater(age(skc5,u),sigma) -> dissimilar(skc5,skc6,u)*. % 1.07/1.30 121[0:Res:17.0,113.0] || -> dissimilar(skc5,skc6,skc8)*. % 1.07/1.30 135[0:Res:92.0,20.0] || -> smaller_or_equal(zero,tau)*. % 1.07/1.30 146[0:SpL:17.0,60.1] || positional_advantage(skc5,skc6)* smaller_or_equal(zero,tau) -> . % 1.07/1.30 148[0:MRR:146.1,135.0] || positional_advantage(skc5,skc6)* -> . % 1.07/1.30 164[0:Res:25.1,20.0] || greater(u,v) -> smaller_or_equal(v,u)*. % 1.07/1.30 168[0:Res:83.1,24.0] || -> equal(age(skc5,skc7),sigma) greater(sigma,age(skc5,skc7))*r. % 1.07/1.30 200[0:Res:121.0,40.2] || is_aligned(skc5,skc8)* is_aligned(skc5,skc6) -> . % 1.07/1.30 204[0:MRR:200.1,109.0] || is_aligned(skc5,skc8)* -> . % 1.07/1.30 217[0:Res:28.2,20.0] || -> greater(u,v) equal(u,v) smaller_or_equal(u,v)*. % 1.07/1.30 218[0:MRR:217.1,21.0] || -> greater(u,v) smaller_or_equal(u,v)*. % 1.07/1.30 219[0:Res:218.1,60.1] || positional_advantage(skc5,u) -> greater(age(skc5,u),tau)*l. % 1.07/1.30 233[1:Spt:168.0] || -> equal(age(skc5,skc7),sigma)**. % 1.07/1.30 238[1:SpL:233.0,60.1] || positional_advantage(skc5,skc7)* smaller_or_equal(sigma,tau) -> . % 1.07/1.30 246[1:MRR:238.1,73.0] || positional_advantage(skc5,skc7)* -> . % 1.07/1.30 256[0:Res:118.1,40.2] || greater(age(skc5,u),sigma)*l is_aligned(skc5,u) is_aligned(skc5,skc6) -> . % 1.07/1.30 257[0:MRR:256.2,109.0] || greater(age(skc5,u),sigma)*l is_aligned(skc5,u) -> . % 1.07/1.30 260[0:Res:67.2,76.0] || is_aligned(skc5,skc6) -> is_aligned(skc5,u) greater(age(skc5,u),sigma)*l. % 1.07/1.30 268[0:MRR:260.0,109.0] || -> is_aligned(skc5,u) greater(age(skc5,u),sigma)*l. % 1.07/1.30 271[1:SpR:233.0,268.1] || -> is_aligned(skc5,skc7)* greater(sigma,sigma). % 1.07/1.30 292[0:NCh:33.2,33.0,257.0,219.1] || greater(tau,sigma) is_aligned(skc5,u) positional_advantage(skc5,u)* -> . % 1.07/1.30 299[0:MRR:292.0,72.0] || is_aligned(skc5,u) positional_advantage(skc5,u)* -> . % 1.07/1.30 300[0:MRR:115.1,299.0] || positional_advantage(skc5,u) -> equal(hazard_of_mortality(skc5,u),mod1)**. % 1.07/1.30 301[0:MRR:116.1,299.1] || is_aligned(skc5,u) -> equal(hazard_of_mortality(skc5,u),mod2)**. % 1.07/1.30 354[0:Res:12.0,26.0] || greater(mod1,mod2)*r -> . % 1.07/1.30 356[0:Res:10.0,26.0] || greater(mod2,high)*r -> . % 1.07/1.30 369[0:NCh:33.2,33.0,26.0,12.0] || equal(mod1,u) greater(u,mod2)* -> . % 1.07/1.30 410[0:Res:10.0,369.1] || equal(high,mod1)** -> . % 1.07/1.30 589[0:SpL:300.1,56.2] || positional_advantage(skc5,skc9) equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc8))* smaller(mod1,hazard_of_mortality(skc5,skc7)) -> . % 1.07/1.30 596[0:Res:28.2,56.2] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc8))* -> greater(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7)) equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7)). % 1.07/1.30 597[0:Res:29.2,56.2] || smaller_or_equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7)) equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc8))* -> equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7)). % 1.07/1.30 599[0:MRR:589.0,110.0] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc8))* smaller(mod1,hazard_of_mortality(skc5,skc7)) -> . % 1.07/1.30 1933[0:SpL:114.2,597.2] || smaller_or_equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7))* equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc7),high) -> positional_advantage(skc5,skc8) is_aligned(skc5,skc8) equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7)). % 1.07/1.32 1953[0:MRR:1933.3,1933.4,111.0,204.0] || smaller_or_equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7))* equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc7),high) -> equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7)). % 1.07/1.32 1960[2:Spt:596.3] || -> equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7))**. % 1.07/1.32 1979[2:SpR:1960.0,300.1] || positional_advantage(skc5,skc9) -> equal(hazard_of_mortality(skc5,skc7),mod1)**. % 1.07/1.32 1987[2:MRR:1979.0,110.0] || -> equal(hazard_of_mortality(skc5,skc7),mod1)**. % 1.07/1.32 2007[2:SpR:1987.0,114.2] || -> positional_advantage(skc5,skc7)* is_aligned(skc5,skc7) equal(high,mod1). % 1.07/1.32 2009[2:SpR:1987.0,301.1] || is_aligned(skc5,skc7)* -> equal(mod2,mod1). % 1.07/1.32 2018[2:MRR:2007.0,2007.2,246.0,410.0] || -> is_aligned(skc5,skc7)*. % 1.07/1.32 2020[2:MRR:2009.0,2018.0] || -> equal(mod2,mod1)**. % 1.07/1.32 2021[2:Rew:2020.0,12.0] || -> greater(mod1,mod1)*. % 1.07/1.32 2025[2:Rew:2020.0,354.0] || greater(mod1,mod1)* -> . % 1.07/1.32 2256[2:MRR:2025.0,2021.0] || -> . % 1.07/1.32 2285[2:Spt:2256.0,596.3,1960.0] || equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7))** -> . % 1.07/1.32 2286[2:Spt:2256.0,596.0,596.1,596.2] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc8))* -> greater(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7)). % 1.07/1.32 2287[2:MRR:1953.3,2285.0] || smaller_or_equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7))* equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc7),high) -> . % 1.07/1.32 2469[3:Spt:56.0] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6))** -> . % 1.07/1.32 2472[3:SpL:52.4,2469.0] organization(skc5) || is_aligned(skc5,skc7) equal(hazard_of_mortality(skc5,skc6),mod2)** -> has_immunity(skc5,skc7) positional_advantage(skc5,skc7). % 1.07/1.32 2478[3:SSi:2472.0,2.0,1.0] || is_aligned(skc5,skc7) equal(hazard_of_mortality(skc5,skc6),mod2)** -> has_immunity(skc5,skc7) positional_advantage(skc5,skc7). % 1.07/1.32 2479[3:MRR:2478.2,2478.3,108.0,246.0] || is_aligned(skc5,skc7) equal(hazard_of_mortality(skc5,skc6),mod2)** -> . % 1.07/1.32 2532[3:SpL:301.1,2479.1] || is_aligned(skc5,skc6) is_aligned(skc5,skc7)* equal(mod2,mod2) -> . % 1.07/1.32 2540[3:Obv:2532.2] || is_aligned(skc5,skc6) is_aligned(skc5,skc7)* -> . % 1.07/1.32 2541[3:MRR:2540.0,109.0] || is_aligned(skc5,skc7)* -> . % 1.07/1.32 2545[3:MRR:271.0,2541.0] || -> greater(sigma,sigma)*. % 1.07/1.32 2605[3:Res:2545.0,26.0] || greater(sigma,sigma)* -> . % 1.07/1.32 2608[3:MRR:2605.0,2545.0] || -> . % 1.07/1.32 2609[3:Spt:2608.0,56.0,2469.0] || -> equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6))**. % 1.07/1.32 2610[3:Spt:2608.0,56.1,56.2] || smaller(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc8)) smaller(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7))* -> . % 1.07/1.32 2614[3:Rew:2609.0,2287.2,2609.0,2287.1,2609.0,2287.0] || smaller_or_equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc6))* equal(hazard_of_mortality(skc5,skc6),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc6),high) -> . % 1.07/1.32 2615[3:Obv:2614.1] || smaller_or_equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc6))* smaller(hazard_of_mortality(skc5,skc6),high) -> . % 1.07/1.32 2657[3:SpR:2609.0,114.2] || -> positional_advantage(skc5,skc7) is_aligned(skc5,skc7) equal(hazard_of_mortality(skc5,skc6),high)**. % 1.07/1.32 2659[3:SpR:2609.0,301.1] || is_aligned(skc5,skc7) -> equal(hazard_of_mortality(skc5,skc6),mod2)**. % 1.07/1.32 2670[3:MRR:2657.0,246.0] || -> is_aligned(skc5,skc7) equal(hazard_of_mortality(skc5,skc6),high)**. % 1.07/1.32 2691[4:Spt:2670.1] || -> equal(hazard_of_mortality(skc5,skc6),high)**. % 1.07/1.32 2733[4:SpR:2691.0,301.1] || is_aligned(skc5,skc6)* -> equal(high,mod2). % 1.07/1.32 2740[4:MRR:2733.0,109.0] || -> equal(high,mod2)**. % 1.07/1.32 2802[4:Rew:2740.0,10.0] || -> greater(mod2,mod2)*. % 1.07/1.33 2803[4:Rew:2740.0,356.0] || greater(mod2,mod2)* -> . % 1.07/1.33 2971[4:MRR:2803.0,2802.0] || -> . % 1.07/1.33 3022[4:Spt:2971.0,2670.1,2691.0] || equal(hazard_of_mortality(skc5,skc6),high)** -> . % 1.07/1.33 3023[4:Spt:2971.0,2670.0] || -> is_aligned(skc5,skc7)*. % 1.07/1.33 3025[4:MRR:2659.0,3023.0] || -> equal(hazard_of_mortality(skc5,skc6),mod2)**. % 1.07/1.33 3030[4:Rew:3025.0,2615.1,3025.0,2615.0] || smaller_or_equal(hazard_of_mortality(skc5,skc9),mod2)* smaller(mod2,high) -> . % 1.07/1.33 3262[4:SpL:300.1,3030.0] || positional_advantage(skc5,skc9) smaller_or_equal(mod1,mod2) smaller(mod2,high)* -> . % 1.07/1.33 3271[4:MRR:3262.0,110.0] || smaller_or_equal(mod1,mod2) smaller(mod2,high)* -> . % 1.07/1.33 3275[4:Res:25.1,3271.1] || greater(high,mod2) smaller_or_equal(mod1,mod2)* -> . % 1.07/1.33 3277[4:MRR:3275.0,10.0] || smaller_or_equal(mod1,mod2)* -> . % 1.07/1.33 3280[4:Res:164.1,3277.0] || greater(mod2,mod1)*l -> . % 1.07/1.33 3282[4:MRR:3280.0,12.0] || -> . % 1.07/1.33 3283[1:Spt:3282.0,168.0,233.0] || equal(age(skc5,skc7),sigma)** -> . % 1.07/1.33 3284[1:Spt:3282.0,168.1] || -> greater(sigma,age(skc5,skc7))*r. % 1.07/1.33 3295[1:Res:3284.0,26.0] || greater(age(skc5,skc7),sigma)*l -> . % 1.07/1.33 3328[1:Res:268.1,3295.0] || -> is_aligned(skc5,skc7)*. % 1.07/1.33 3380[2:Spt:56.0] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6))** -> . % 1.07/1.33 3382[2:SpL:301.1,3380.0] || is_aligned(skc5,skc7) equal(hazard_of_mortality(skc5,skc6),mod2)** -> . % 1.07/1.33 3389[2:MRR:3382.0,3328.0] || equal(hazard_of_mortality(skc5,skc6),mod2)** -> . % 1.07/1.33 3393[2:SpL:52.4,3389.0] organization(skc5) || is_aligned(skc5,skc6) equal(mod2,mod2) -> has_immunity(skc5,skc6) positional_advantage(skc5,skc6)*. % 1.07/1.33 3400[2:Obv:3393.2] organization(skc5) || is_aligned(skc5,skc6) -> has_immunity(skc5,skc6) positional_advantage(skc5,skc6)*. % 1.07/1.33 3401[2:SSi:3400.0,2.0,1.0] || is_aligned(skc5,skc6) -> has_immunity(skc5,skc6) positional_advantage(skc5,skc6)*. % 1.07/1.33 3402[2:MRR:3401.0,3401.1,3401.2,109.0,108.0,148.0] || -> . % 1.07/1.33 3403[2:Spt:3402.0,56.0,3380.0] || -> equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6))**. % 1.07/1.33 3404[2:Spt:3402.0,56.1,56.2] || smaller(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc8)) smaller(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7))* -> . % 1.07/1.33 3406[2:Rew:3403.0,599.2,3403.0,599.1,3403.0,599.0] || equal(hazard_of_mortality(skc5,skc6),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc6),hazard_of_mortality(skc5,skc8))* smaller(mod1,hazard_of_mortality(skc5,skc6)) -> . % 1.07/1.33 3407[2:Obv:3406.0] || smaller(hazard_of_mortality(skc5,skc6),hazard_of_mortality(skc5,skc8))* smaller(mod1,hazard_of_mortality(skc5,skc6)) -> . % 1.07/1.33 3431[2:SpR:3403.0,301.1] || is_aligned(skc5,skc7) -> equal(hazard_of_mortality(skc5,skc6),mod2)**. % 1.07/1.33 3439[2:MRR:3431.0,3328.0] || -> equal(hazard_of_mortality(skc5,skc6),mod2)**. % 1.07/1.33 3444[2:Rew:3439.0,3407.0] || smaller(mod2,hazard_of_mortality(skc5,skc8))* smaller(mod1,hazard_of_mortality(skc5,skc6)) -> . % 1.07/1.33 3457[2:Rew:3439.0,3444.1] || smaller(mod2,hazard_of_mortality(skc5,skc8))* smaller(mod1,mod2) -> . % 1.07/1.33 3502[2:SpL:114.2,3457.0] || smaller(mod2,high)* smaller(mod1,mod2) -> positional_advantage(skc5,skc8) is_aligned(skc5,skc8). % 1.07/1.33 3513[2:MRR:3502.2,3502.3,111.0,204.0] || smaller(mod2,high)* smaller(mod1,mod2) -> . % 1.07/1.33 3516[2:Res:25.1,3513.0] || greater(high,mod2) smaller(mod1,mod2)* -> . % 1.07/1.33 3517[2:MRR:3516.0,10.0] || smaller(mod1,mod2)* -> . % 1.07/1.33 3518[2:Res:28.2,3517.0] || -> greater(mod1,mod2)*r equal(mod2,mod1). % 1.07/1.33 3522[2:MRR:3518.0,354.0] || -> equal(mod2,mod1)**. % 1.07/1.33 3543[2:Rew:3522.0,12.0] || -> greater(mod1,mod1)*. % 1.07/1.33 3551[2:Rew:3522.0,354.0] || greater(mod1,mod1)* -> . % 1.07/1.33 3766[2:MRR:3551.0,3543.0] || -> . % 1.07/1.33 % SZS output end Refutation % 1.07/1.33 Formulae used in the proof : theorem_9 assumption_18d assumption_19 definition_2 definition_smaller_or_equal definition_smaller meaning_postulate_greater_strict assumption_1 meaning_postulate_greater_comparable meaning_postulate_greater_transitive assumption_13 definition_4 assumption_17 assumption_15 % 1.07/1.33 %------------------------------------------------------------------------------