%------------------------------------------------------------------------------ % 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 : n006.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 : Unsatisfiable 0.78s 1.03s % Output : Refutation 0.78s % 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.10/0.37 % Computer : n006.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Mon Sep 7 13:41:16 UTC 2026 % 0.10/0.37 % CPUTime : % 0.78/1.03 % 0.78/1.03 SPASS V 3.9 % 0.78/1.03 SPASS beiseite: Proof found. % 0.78/1.03 % SZS status Theorem % 0.78/1.03 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.78/1.03 SPASS derived 2701 clauses, backtracked 312 clauses, performed 5 splits and kept 1353 clauses. % 0.78/1.03 SPASS allocated 77635 KBytes. % 0.78/1.03 SPASS spent 0:00:00.65 on the problem. % 0.78/1.03 0:00:00.06 for the input. % 0.78/1.03 0:00:00.00 for the FLOTTER CNF translation. % 0.78/1.03 0:00:00.04 for inferences. % 0.78/1.03 0:00:00.00 for the backtracking. % 0.78/1.03 0:00:00.48 for the reduction. % 0.78/1.03 % 0.78/1.03 % 0.78/1.03 Here is a proof with depth 5, length 151 : % 0.78/1.03 % SZS output start Refutation % 0.78/1.03 8[0:Inp] organization(u) || has_immunity(u,v)* -> has_endowment(u). % 0.78/1.03 9[0:Inp] || dissimilar(u,v,w)* -> organization(u). % 0.78/1.03 11[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)* -> . % 0.78/1.03 13[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) dissimilar(u,v,w)*. % 0.78/1.03 16[0:Inp] organization(u) || equal(age(u,v),zero)** -> is_aligned(u,v). % 0.78/1.03 17[0:Inp] organization(u) || greater(age(u,v),sigma) equal(age(u,w),zero) -> dissimilar(u,w,v)*. % 0.78/1.03 18[0:Inp] organization(u) || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.78/1.03 19[0:Inp] robust_position(u) || positional_advantage(u,v) smaller_or_equal(age(u,v),tau)* -> . % 0.78/1.03 20[0:Inp] robust_position(u) || greater(age(u,v),tau)*l -> positional_advantage(u,v). % 0.78/1.03 27[0:Inp] organization(u) || positional_advantage(u,v) -> is_aligned(u,v) has_immunity(u,v) equal(hazard_of_mortality(u,v),mod1)**. % 0.78/1.03 28[0:Inp] organization(u) || is_aligned(u,v) -> positional_advantage(u,v) has_immunity(u,v) equal(hazard_of_mortality(u,v),mod2)**. % 0.78/1.03 29[0:Inp] organization(u) || -> positional_advantage(u,v) is_aligned(u,v) has_immunity(u,v) equal(hazard_of_mortality(u,v),high)**. % 0.78/1.03 33[0:Inp] || -> greater(high,mod2)*l. % 0.78/1.03 35[0:Inp] || -> greater(mod2,mod1)*l. % 0.78/1.03 36[0:Inp] || -> organization(sk3)*. % 0.78/1.03 37[0:Inp] || -> robust_position(sk3)*. % 0.78/1.03 38[0:Inp] || has_endowment(sk3)* -> . % 0.78/1.03 39[0:Inp] || -> equal(age(sk3,sk4),zero)**. % 0.78/1.03 41[0:Inp] || -> greater(tau,zero)*l. % 0.78/1.03 42[0:Inp] || -> smaller(sigma,tau)*. % 0.78/1.03 43[0:Inp] || -> smaller_or_equal(age(sk3,sk5),sigma)*. % 0.78/1.03 44[0:Inp] || -> greater(age(sk3,sk6),sigma)*l. % 0.78/1.03 45[0:Inp] || -> smaller_or_equal(age(sk3,sk6),tau)*. % 0.78/1.03 46[0:Inp] || -> greater(age(sk3,sk7),tau)*l. % 0.78/1.03 47[0:Inp] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk6)) smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))* -> . % 0.78/1.03 48[0:Inp] || smaller_or_equal(u,v) -> equal(u,v) smaller(u,v)*. % 0.78/1.03 49[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 0.78/1.03 50[0:Inp] || equal(u,v) -> smaller_or_equal(u,v)*. % 0.78/1.03 54[0:Inp] || smaller(u,v)* -> greater(v,u). % 0.78/1.03 55[0:Inp] || greater(u,v) -> smaller(v,u)*. % 0.78/1.03 56[0:Inp] || greater(u,v)*+ greater(v,u)* -> . % 0.78/1.03 57[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.78/1.03 58[0:Inp] || -> greater(u,v) equal(u,v) smaller(u,v)*. % 0.78/1.03 60[0:MRR:18.0,9.1] || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 0.78/1.03 62[0:Res:37.0,19.0] || positional_advantage(sk3,u) smaller_or_equal(age(sk3,u),tau)* -> . % 0.78/1.03 65[0:Res:36.0,27.0] || positional_advantage(sk3,u) -> has_immunity(sk3,u) is_aligned(sk3,u) equal(hazard_of_mortality(sk3,u),mod1)**. % 0.78/1.03 66[0:Res:36.0,28.0] || is_aligned(sk3,u) -> has_immunity(sk3,u) positional_advantage(sk3,u) equal(hazard_of_mortality(sk3,u),mod2)**. % 0.78/1.03 67[0:Res:36.0,29.0] || -> has_immunity(sk3,u) is_aligned(sk3,u) positional_advantage(sk3,u) equal(hazard_of_mortality(sk3,u),high)**. % 0.78/1.03 69[0:Res:36.0,13.0] || is_aligned(sk3,u) -> is_aligned(sk3,v) dissimilar(sk3,u,v)*. % 0.78/1.03 73[0:Res:36.0,8.0] || has_immunity(sk3,u)* -> has_endowment(sk3). % 0.78/1.03 74[0:Res:42.0,54.0] || -> greater(tau,sigma)*l. % 0.78/1.03 75[0:Res:42.0,49.0] || -> smaller_or_equal(sigma,tau)*. % 0.78/1.03 78[0:Res:45.0,19.1] robust_position(sk3) || positional_advantage(sk3,sk6)* -> . % 0.78/1.03 80[0:Res:43.0,48.0] || -> equal(age(sk3,sk5),sigma) smaller(age(sk3,sk5),sigma)*. % 0.78/1.03 81[0:Res:39.0,60.0] || dissimilar(sk3,sk4,u)* -> greater(age(sk3,u),sigma). % 0.78/1.03 82[0:Res:39.0,17.1] organization(sk3) || greater(age(sk3,u),sigma) -> dissimilar(sk3,sk4,u)*. % 0.78/1.03 83[0:Res:39.0,16.1] organization(sk3) || -> is_aligned(sk3,sk4)*. % 0.78/1.03 90[0:Res:41.0,55.0] || -> smaller(zero,tau)*. % 0.78/1.03 96[0:Res:46.0,20.1] robust_position(sk3) || -> positional_advantage(sk3,sk7)*. % 0.78/1.03 101[0:Res:44.0,17.2] organization(sk3) || equal(age(sk3,u),zero) -> dissimilar(sk3,u,sk6)*. % 0.78/1.03 110[0:MRR:73.1,38.0] || has_immunity(sk3,u)* -> . % 0.78/1.03 111[0:MRR:83.0,36.0] || -> is_aligned(sk3,sk4)*. % 0.78/1.03 112[0:MRR:96.0,37.0] || -> positional_advantage(sk3,sk7)*. % 0.78/1.03 113[0:MRR:78.0,37.0] || positional_advantage(sk3,sk6)* -> . % 0.78/1.03 115[0:MRR:101.0,36.0] || equal(age(sk3,u),zero) -> dissimilar(sk3,u,sk6)*. % 0.78/1.03 116[0:MRR:67.0,110.0] || -> positional_advantage(sk3,u) is_aligned(sk3,u) equal(hazard_of_mortality(sk3,u),high)**. % 0.78/1.03 117[0:MRR:65.1,110.0] || positional_advantage(sk3,u) -> is_aligned(sk3,u) equal(hazard_of_mortality(sk3,u),mod1)**. % 0.78/1.03 118[0:MRR:66.1,110.0] || is_aligned(sk3,u) -> positional_advantage(sk3,u) equal(hazard_of_mortality(sk3,u),mod2)**. % 0.78/1.03 120[0:MRR:82.0,36.0] || greater(age(sk3,u),sigma) -> dissimilar(sk3,sk4,u)*. % 0.78/1.03 122[0:Res:39.0,115.0] || -> dissimilar(sk3,sk4,sk6)*. % 0.78/1.03 137[0:Res:90.0,49.0] || -> smaller_or_equal(zero,tau)*. % 0.78/1.03 147[0:SpL:39.0,62.1] || positional_advantage(sk3,sk4)* smaller_or_equal(zero,tau) -> . % 0.78/1.03 149[0:MRR:147.1,137.0] || positional_advantage(sk3,sk4)* -> . % 0.78/1.03 171[0:Res:80.1,54.0] || -> equal(age(sk3,sk5),sigma) greater(sigma,age(sk3,sk5))*r. % 0.78/1.03 205[0:Res:122.0,11.2] || is_aligned(sk3,sk6)* is_aligned(sk3,sk4) -> . % 0.78/1.03 209[0:MRR:205.1,111.0] || is_aligned(sk3,sk6)* -> . % 0.78/1.03 219[0:Res:58.2,49.0] || -> greater(u,v) equal(u,v) smaller_or_equal(u,v)*. % 0.78/1.03 220[0:MRR:219.1,50.0] || -> greater(u,v) smaller_or_equal(u,v)*. % 0.78/1.03 221[0:Res:220.1,62.1] || positional_advantage(sk3,u) -> greater(age(sk3,u),tau)*l. % 0.78/1.03 242[1:Spt:171.0] || -> equal(age(sk3,sk5),sigma)**. % 0.78/1.03 247[1:SpL:242.0,62.1] || positional_advantage(sk3,sk5)* smaller_or_equal(sigma,tau) -> . % 0.78/1.03 255[1:MRR:247.1,75.0] || positional_advantage(sk3,sk5)* -> . % 0.78/1.03 264[0:Res:120.1,11.2] || greater(age(sk3,u),sigma)*l is_aligned(sk3,u) is_aligned(sk3,sk4) -> . % 0.78/1.03 265[0:MRR:264.2,111.0] || greater(age(sk3,u),sigma)*l is_aligned(sk3,u) -> . % 0.78/1.03 268[0:Res:69.2,81.0] || is_aligned(sk3,sk4) -> is_aligned(sk3,u) greater(age(sk3,u),sigma)*l. % 0.78/1.03 276[0:MRR:268.0,111.0] || -> is_aligned(sk3,u) greater(age(sk3,u),sigma)*l. % 0.78/1.03 279[1:SpR:242.0,276.1] || -> is_aligned(sk3,sk5)* greater(sigma,sigma). % 0.78/1.03 312[0:NCh:57.2,57.0,265.0,221.1] || greater(tau,sigma) is_aligned(sk3,u) positional_advantage(sk3,u)* -> . % 0.78/1.03 317[0:MRR:312.0,74.0] || is_aligned(sk3,u) positional_advantage(sk3,u)* -> . % 0.78/1.03 318[0:MRR:117.1,317.0] || positional_advantage(sk3,u) -> equal(hazard_of_mortality(sk3,u),mod1)**. % 0.78/1.03 319[0:MRR:118.1,317.1] || is_aligned(sk3,u) -> equal(hazard_of_mortality(sk3,u),mod2)**. % 0.78/1.03 335[0:Res:35.0,56.0] || greater(mod1,mod2)*r -> . % 0.78/1.03 342[0:Res:276.1,56.0] || greater(sigma,age(sk3,u))*r -> is_aligned(sk3,u). % 0.78/1.03 487[0:SpL:318.1,47.2] || positional_advantage(sk3,sk7) equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk6))* smaller(mod1,hazard_of_mortality(sk3,sk5)) -> . % 0.78/1.03 494[0:Res:58.2,47.2] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk6))* -> greater(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5)) equal(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5)). % 0.78/1.03 497[0:MRR:487.0,112.0] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk6))* smaller(mod1,hazard_of_mortality(sk3,sk5)) -> . % 0.78/1.03 1235[1:SpL:242.0,342.0] || greater(sigma,sigma) -> is_aligned(sk3,sk5)*. % 0.78/1.03 1240[1:MRR:1235.0,279.1] || -> is_aligned(sk3,sk5)*. % 0.78/1.03 1915[2:Spt:494.3] || -> equal(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))**. % 0.78/1.03 1927[2:SpR:1915.0,318.1] || positional_advantage(sk3,sk7) -> equal(hazard_of_mortality(sk3,sk5),mod1)**. % 0.78/1.03 1935[2:MRR:1927.0,112.0] || -> equal(hazard_of_mortality(sk3,sk5),mod1)**. % 0.78/1.03 1957[2:SpR:1935.0,319.1] || is_aligned(sk3,sk5)* -> equal(mod2,mod1). % 0.78/1.03 1964[2:MRR:1957.0,1240.0] || -> equal(mod2,mod1)**. % 0.78/1.03 1965[2:Rew:1964.0,35.0] || -> greater(mod1,mod1)*. % 0.78/1.03 1969[2:Rew:1964.0,335.0] || greater(mod1,mod1)* -> . % 0.78/1.03 2183[2:MRR:1969.0,1965.0] || -> . % 0.78/1.05 2210[2:Spt:2183.0,494.3,1915.0] || equal(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))** -> . % 0.78/1.05 2211[2:Spt:2183.0,494.0,494.1,494.2] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk6))* -> greater(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5)). % 0.78/1.05 2343[2:SpL:318.1,2210.0] || positional_advantage(sk3,sk7) equal(hazard_of_mortality(sk3,sk5),mod1)** -> . % 0.78/1.05 2349[2:MRR:2343.0,112.0] || equal(hazard_of_mortality(sk3,sk5),mod1)** -> . % 0.78/1.05 2378[2:SpL:28.4,2349.0] organization(sk3) || is_aligned(sk3,sk5) equal(mod2,mod1) -> positional_advantage(sk3,sk5)* has_immunity(sk3,sk5). % 0.78/1.05 2381[2:SSi:2378.0,37.0,36.0] || is_aligned(sk3,sk5) equal(mod2,mod1) -> positional_advantage(sk3,sk5)* has_immunity(sk3,sk5). % 0.78/1.05 2382[2:MRR:2381.0,2381.2,2381.3,1240.0,255.0,110.0] || equal(mod2,mod1)** -> . % 0.78/1.05 2404[3:Spt:47.0] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4))** -> . % 0.78/1.05 2405[3:SpL:319.1,2404.0] || is_aligned(sk3,sk5) equal(hazard_of_mortality(sk3,sk4),mod2)** -> . % 0.78/1.05 2413[3:MRR:2405.0,1240.0] || equal(hazard_of_mortality(sk3,sk4),mod2)** -> . % 0.78/1.05 2417[3:SpL:28.4,2413.0] organization(sk3) || is_aligned(sk3,sk4) equal(mod2,mod2) -> positional_advantage(sk3,sk4)* has_immunity(sk3,sk4). % 0.78/1.05 2424[3:Obv:2417.2] organization(sk3) || is_aligned(sk3,sk4) -> positional_advantage(sk3,sk4)* has_immunity(sk3,sk4). % 0.78/1.05 2425[3:SSi:2424.0,37.0,36.0] || is_aligned(sk3,sk4) -> positional_advantage(sk3,sk4)* has_immunity(sk3,sk4). % 0.78/1.05 2426[3:MRR:2425.0,2425.1,2425.2,111.0,149.0,110.0] || -> . % 0.78/1.05 2427[3:Spt:2426.0,47.0,2404.0] || -> equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4))**. % 0.78/1.05 2428[3:Spt:2426.0,47.1,47.2] || smaller(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk6)) smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))* -> . % 0.78/1.05 2434[3:Rew:2427.0,497.2,2427.0,497.1,2427.0,497.0] || equal(hazard_of_mortality(sk3,sk4),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk4),hazard_of_mortality(sk3,sk6))* smaller(mod1,hazard_of_mortality(sk3,sk4)) -> . % 0.78/1.05 2435[3:Obv:2434.0] || smaller(hazard_of_mortality(sk3,sk4),hazard_of_mortality(sk3,sk6))* smaller(mod1,hazard_of_mortality(sk3,sk4)) -> . % 0.78/1.05 2476[3:SpR:2427.0,319.1] || is_aligned(sk3,sk5) -> equal(hazard_of_mortality(sk3,sk4),mod2)**. % 0.78/1.05 2483[3:MRR:2476.0,1240.0] || -> equal(hazard_of_mortality(sk3,sk4),mod2)**. % 0.78/1.05 2490[3:Rew:2483.0,2435.0] || smaller(mod2,hazard_of_mortality(sk3,sk6))* smaller(mod1,hazard_of_mortality(sk3,sk4)) -> . % 0.78/1.05 2508[3:Rew:2483.0,2490.1] || smaller(mod2,hazard_of_mortality(sk3,sk6))* smaller(mod1,mod2) -> . % 0.78/1.05 2582[3:SpL:116.2,2508.0] || smaller(mod2,high)* smaller(mod1,mod2) -> positional_advantage(sk3,sk6) is_aligned(sk3,sk6). % 0.78/1.05 2591[3:MRR:2582.2,2582.3,113.0,209.0] || smaller(mod2,high)* smaller(mod1,mod2) -> . % 0.78/1.05 2595[3:Res:55.1,2591.0] || greater(high,mod2) smaller(mod1,mod2)* -> . % 0.78/1.05 2596[3:MRR:2595.0,33.0] || smaller(mod1,mod2)* -> . % 0.78/1.05 2597[3:Res:58.2,2596.0] || -> greater(mod1,mod2)*r equal(mod2,mod1). % 0.78/1.05 2602[3:MRR:2597.0,2597.1,335.0,2382.0] || -> . % 0.78/1.05 2603[1:Spt:2602.0,171.0,242.0] || equal(age(sk3,sk5),sigma)** -> . % 0.78/1.05 2604[1:Spt:2602.0,171.1] || -> greater(sigma,age(sk3,sk5))*r. % 0.78/1.05 2619[1:Res:2604.0,342.0] || -> is_aligned(sk3,sk5)*. % 0.78/1.05 2712[2:Spt:47.0] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4))** -> . % 0.78/1.05 2713[2:SpL:319.1,2712.0] || is_aligned(sk3,sk5) equal(hazard_of_mortality(sk3,sk4),mod2)** -> . % 0.78/1.05 2721[2:MRR:2713.0,2619.0] || equal(hazard_of_mortality(sk3,sk4),mod2)** -> . % 0.78/1.05 2725[2:SpL:28.4,2721.0] organization(sk3) || is_aligned(sk3,sk4) equal(mod2,mod2) -> positional_advantage(sk3,sk4)* has_immunity(sk3,sk4). % 0.78/1.05 2732[2:Obv:2725.2] organization(sk3) || is_aligned(sk3,sk4) -> positional_advantage(sk3,sk4)* has_immunity(sk3,sk4). % 0.78/1.05 2733[2:SSi:2732.0,37.0,36.0] || is_aligned(sk3,sk4) -> positional_advantage(sk3,sk4)* has_immunity(sk3,sk4). % 0.78/1.05 2734[2:MRR:2733.0,2733.1,2733.2,111.0,149.0,110.0] || -> . % 0.78/1.05 2735[2:Spt:2734.0,47.0,2712.0] || -> equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4))**. % 0.78/1.05 2736[2:Spt:2734.0,47.1,47.2] || smaller(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk6)) smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))* -> . % 0.78/1.05 2738[2:Rew:2735.0,497.2,2735.0,497.1,2735.0,497.0] || equal(hazard_of_mortality(sk3,sk4),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk4),hazard_of_mortality(sk3,sk6))* smaller(mod1,hazard_of_mortality(sk3,sk4)) -> . % 0.78/1.05 2739[2:Obv:2738.0] || smaller(hazard_of_mortality(sk3,sk4),hazard_of_mortality(sk3,sk6))* smaller(mod1,hazard_of_mortality(sk3,sk4)) -> . % 0.78/1.05 2764[2:SpR:2735.0,319.1] || is_aligned(sk3,sk5) -> equal(hazard_of_mortality(sk3,sk4),mod2)**. % 0.78/1.05 2771[2:MRR:2764.0,2619.0] || -> equal(hazard_of_mortality(sk3,sk4),mod2)**. % 0.78/1.05 2776[2:Rew:2771.0,2739.0] || smaller(mod2,hazard_of_mortality(sk3,sk6))* smaller(mod1,hazard_of_mortality(sk3,sk4)) -> . % 0.78/1.05 2789[2:Rew:2771.0,2776.1] || smaller(mod2,hazard_of_mortality(sk3,sk6))* smaller(mod1,mod2) -> . % 0.78/1.05 2836[2:SpL:116.2,2789.0] || smaller(mod2,high)* smaller(mod1,mod2) -> positional_advantage(sk3,sk6) is_aligned(sk3,sk6). % 0.78/1.05 2845[2:MRR:2836.2,2836.3,113.0,209.0] || smaller(mod2,high)* smaller(mod1,mod2) -> . % 0.78/1.05 2848[2:Res:55.1,2845.0] || greater(high,mod2) smaller(mod1,mod2)* -> . % 0.78/1.05 2849[2:MRR:2848.0,33.0] || smaller(mod1,mod2)* -> . % 0.78/1.05 2850[2:Res:58.2,2849.0] || -> greater(mod1,mod2)*r equal(mod2,mod1). % 0.78/1.05 2854[2:MRR:2850.0,335.0] || -> equal(mod2,mod1)**. % 0.78/1.05 2881[2:Rew:2854.0,35.0] || -> greater(mod1,mod1)*. % 0.78/1.05 2886[2:Rew:2854.0,335.0] || greater(mod1,mod1)* -> . % 0.78/1.05 3082[2:MRR:2886.0,2881.0] || -> . % 0.78/1.05 % SZS output end Refutation % 0.78/1.05 Formulae used in the proof : assumption_1_46 definition_2_47 definition_2_49 definition_2_51 assumption_13_54 assumption_15_55 assumption_15_56 definition_4_57 definition_4_58 assumption_17_65 assumption_17_66 assumption_17_67 assumption_18d_71 assumption_19_73 theorem_9_74 theorem_9_75 theorem_9_76 theorem_9_77 theorem_9_79 theorem_9_80 theorem_9_81 theorem_9_82 theorem_9_83 theorem_9_84 theorem_9_85 definition_smaller_or_equal_1 definition_smaller_or_equal_2 definition_smaller_or_equal_3 definition_smaller_7 definition_smaller_8 meaning_postulate_greater_strict_9 meaning_postulate_greater_transitive_10 meaning_postulate_greater_comparable_11 % 0.78/1.05 %------------------------------------------------------------------------------