%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT064-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:59 AM UTC 2026 % Result : Unsatisfiable 1.05s 1.30s % Output : Refutation 1.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT064-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : run_spass %d %s % 0.10/0.35 % Computer : n011.cluster.edu % 0.10/0.35 % Model : x86_64 x86_64 % 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.35 % Memory : 8046.5625MB % 0.10/0.35 % OS : Linux 6.8.0-71-generic % 0.10/0.35 % CPULimit : 300 % 0.10/0.35 % WCLimit : 300 % 0.10/0.35 % DateTime : Mon Sep 7 13:43:45 UTC 2026 % 0.10/0.35 % CPUTime : % 1.05/1.30 % 1.05/1.30 SPASS V 3.9 % 1.05/1.30 SPASS beiseite: Proof found. % 1.05/1.30 % SZS status Theorem % 1.05/1.30 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.05/1.30 SPASS derived 3452 clauses, backtracked 677 clauses, performed 8 splits and kept 1889 clauses. % 1.05/1.30 SPASS allocated 78030 KBytes. % 1.05/1.30 SPASS spent 0:00:00.93 on the problem. % 1.05/1.30 0:00:00.06 for the input. % 1.05/1.30 0:00:00.00 for the FLOTTER CNF translation. % 1.05/1.30 0:00:00.06 for inferences. % 1.05/1.30 0:00:00.00 for the backtracking. % 1.05/1.30 0:00:00.75 for the reduction. % 1.05/1.30 % 1.05/1.30 % 1.05/1.30 Here is a proof with depth 5, length 142 : % 1.05/1.30 % SZS output start Refutation % 1.05/1.30 8[0:Inp] organization(u) || has_immunity(u,v)* -> has_endowment(u). % 1.05/1.30 9[0:Inp] || dissimilar(u,v,w)* -> organization(u). % 1.05/1.30 11[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)* -> . % 1.05/1.30 13[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) dissimilar(u,v,w)*. % 1.05/1.30 16[0:Inp] organization(u) || equal(age(u,v),zero)** -> is_aligned(u,v). % 1.05/1.30 17[0:Inp] organization(u) || greater(age(u,v),sigma) equal(age(u,w),zero) -> dissimilar(u,w,v)*. % 1.05/1.30 18[0:Inp] organization(u) || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 1.05/1.30 19[0:Inp] robust_position(u) || positional_advantage(u,v) smaller_or_equal(age(u,v),tau)* -> . % 1.05/1.30 20[0:Inp] robust_position(u) || greater(age(u,v),tau)*l -> positional_advantage(u,v). % 1.05/1.30 26[0:Inp] organization(u) || positional_advantage(u,v) is_aligned(u,v) -> has_immunity(u,v) equal(hazard_of_mortality(u,v),low)**. % 1.05/1.30 27[0:Inp] organization(u) || positional_advantage(u,v) -> is_aligned(u,v) has_immunity(u,v) equal(hazard_of_mortality(u,v),mod1)**. % 1.05/1.30 28[0:Inp] organization(u) || is_aligned(u,v) -> positional_advantage(u,v) has_immunity(u,v) equal(hazard_of_mortality(u,v),mod2)**. % 1.05/1.30 31[0:Inp] || -> greater(mod1,low)*l. % 1.05/1.30 35[0:Inp] || -> greater(mod2,mod1)*l. % 1.05/1.30 36[0:Inp] || -> organization(sk3)*. % 1.05/1.30 37[0:Inp] || -> robust_position(sk3)*. % 1.05/1.30 38[0:Inp] || has_endowment(sk3)* -> . % 1.05/1.30 39[0:Inp] || -> equal(age(sk3,sk4),zero)**. % 1.05/1.30 41[0:Inp] || -> greater(tau,zero)*l. % 1.05/1.30 42[0:Inp] || -> greater(sigma,tau)*r. % 1.05/1.30 43[0:Inp] || -> smaller_or_equal(age(sk3,sk5),tau)*. % 1.05/1.30 44[0:Inp] || -> greater(age(sk3,sk6),tau)*l. % 1.05/1.30 45[0:Inp] || -> smaller_or_equal(age(sk3,sk6),sigma)*. % 1.05/1.30 46[0:Inp] || -> greater(age(sk3,sk7),sigma)*l. % 1.05/1.30 47[0:Inp] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))* smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7)) -> . % 1.05/1.30 48[0:Inp] || smaller_or_equal(u,v) -> equal(u,v) smaller(u,v)*. % 1.05/1.30 49[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 1.05/1.30 54[0:Inp] || smaller(u,v)* -> greater(v,u). % 1.05/1.30 55[0:Inp] || greater(u,v) -> smaller(v,u)*. % 1.05/1.30 56[0:Inp] || greater(u,v)*+ greater(v,u)* -> . % 1.05/1.30 57[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 1.05/1.30 58[0:Inp] || -> greater(u,v) equal(u,v) smaller(u,v)*. % 1.05/1.30 60[0:MRR:18.0,9.1] || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 1.05/1.30 61[0:Res:37.0,20.0] || greater(age(sk3,u),tau)*l -> positional_advantage(sk3,u). % 1.05/1.30 62[0:Res:37.0,19.0] || positional_advantage(sk3,u) smaller_or_equal(age(sk3,u),tau)* -> . % 1.05/1.30 64[0:Res:36.0,26.0] || is_aligned(sk3,u) positional_advantage(sk3,u) -> has_immunity(sk3,u) equal(hazard_of_mortality(sk3,u),low)**. % 1.05/1.30 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)**. % 1.05/1.30 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)**. % 1.05/1.30 69[0:Res:36.0,13.0] || is_aligned(sk3,u) -> is_aligned(sk3,v) dissimilar(sk3,u,v)*. % 1.05/1.30 73[0:Res:36.0,8.0] || has_immunity(sk3,u)* -> has_endowment(sk3). % 1.05/1.30 76[0:Res:45.0,48.0] || -> equal(age(sk3,sk6),sigma) smaller(age(sk3,sk6),sigma)*. % 1.05/1.30 77[0:Res:43.0,19.1] robust_position(sk3) || positional_advantage(sk3,sk5)* -> . % 1.05/1.30 79[0:Res:39.0,60.0] || dissimilar(sk3,sk4,u)* -> greater(age(sk3,u),sigma). % 1.05/1.30 81[0:Res:39.0,16.1] organization(sk3) || -> is_aligned(sk3,sk4)*. % 1.05/1.30 92[0:Res:41.0,55.0] || -> smaller(zero,tau)*. % 1.05/1.30 98[0:Res:46.0,17.2] organization(sk3) || equal(age(sk3,u),zero) -> dissimilar(sk3,u,sk7)*. % 1.05/1.30 103[0:Res:44.0,20.1] robust_position(sk3) || -> positional_advantage(sk3,sk6)*. % 1.05/1.30 112[0:MRR:73.1,38.0] || has_immunity(sk3,u)* -> . % 1.05/1.30 113[0:MRR:81.0,36.0] || -> is_aligned(sk3,sk4)*. % 1.05/1.30 114[0:MRR:103.0,37.0] || -> positional_advantage(sk3,sk6)*. % 1.05/1.30 115[0:MRR:77.0,37.0] || positional_advantage(sk3,sk5)* -> . % 1.05/1.30 117[0:MRR:98.0,36.0] || equal(age(sk3,u),zero) -> dissimilar(sk3,u,sk7)*. % 1.05/1.30 119[0:MRR:65.1,112.0] || positional_advantage(sk3,u) -> is_aligned(sk3,u) equal(hazard_of_mortality(sk3,u),mod1)**. % 1.05/1.30 120[0:MRR:66.1,112.0] || is_aligned(sk3,u) -> positional_advantage(sk3,u) equal(hazard_of_mortality(sk3,u),mod2)**. % 1.05/1.30 121[0:MRR:64.2,112.0] || positional_advantage(sk3,u) is_aligned(sk3,u) -> equal(hazard_of_mortality(sk3,u),low)**. % 1.05/1.30 124[0:Res:39.0,117.0] || -> dissimilar(sk3,sk4,sk7)*. % 1.05/1.30 127[1:Spt:76.0] || -> equal(age(sk3,sk6),sigma)**. % 1.05/1.30 136[0:Res:92.0,49.0] || -> smaller_or_equal(zero,tau)*. % 1.05/1.30 152[0:SpL:39.0,62.1] || positional_advantage(sk3,sk4)* smaller_or_equal(zero,tau) -> . % 1.05/1.30 156[0:MRR:152.1,136.0] || positional_advantage(sk3,sk4)* -> . % 1.05/1.30 213[0:Res:124.0,11.2] || is_aligned(sk3,sk7)* is_aligned(sk3,sk4) -> . % 1.05/1.30 217[0:MRR:213.1,113.0] || is_aligned(sk3,sk7)* -> . % 1.05/1.30 272[0:Res:69.2,79.0] || is_aligned(sk3,sk4) -> is_aligned(sk3,u) greater(age(sk3,u),sigma)*l. % 1.05/1.30 277[0:MRR:272.0,113.0] || -> is_aligned(sk3,u) greater(age(sk3,u),sigma)*l. % 1.05/1.30 278[1:SpR:127.0,277.1] || -> is_aligned(sk3,sk6)* greater(sigma,sigma). % 1.05/1.30 281[0:NCh:57.2,57.0,277.1,61.0] || greater(sigma,tau) -> is_aligned(sk3,u) positional_advantage(sk3,u)*. % 1.05/1.30 284[0:MRR:281.0,42.0] || -> is_aligned(sk3,u) positional_advantage(sk3,u)*. % 1.05/1.30 285[0:MRR:120.0,284.0] || -> positional_advantage(sk3,u) equal(hazard_of_mortality(sk3,u),mod2)**. % 1.05/1.30 286[0:MRR:119.0,284.1] || -> is_aligned(sk3,u) equal(hazard_of_mortality(sk3,u),mod1)**. % 1.05/1.30 400[0:Res:35.0,56.0] || greater(mod1,mod2)*r -> . % 1.05/1.30 405[0:Res:31.0,56.0] || greater(low,mod1)*r -> . % 1.05/1.30 407[0:Res:277.1,56.0] || greater(sigma,age(sk3,u))*r -> is_aligned(sk3,u). % 1.05/1.30 540[0:Res:58.2,47.1] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7))* -> greater(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5)) equal(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5)). % 1.05/1.30 542[0:Res:55.1,47.1] || greater(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk7)) equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7))* -> . % 1.05/1.30 837[1:SpL:127.0,407.0] || greater(sigma,sigma) -> is_aligned(sk3,sk6)*. % 1.05/1.30 842[1:MRR:837.0,278.1] || -> is_aligned(sk3,sk6)*. % 1.05/1.30 2418[0:SpL:286.1,542.2] || greater(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk7)) equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk6),mod1)* -> is_aligned(sk3,sk7). % 1.05/1.30 2437[0:Rew:286.1,2418.0] || greater(hazard_of_mortality(sk3,sk5),mod1) equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk6),mod1)* -> is_aligned(sk3,sk7). % 1.05/1.30 2438[0:MRR:2437.3,217.0] || greater(hazard_of_mortality(sk3,sk5),mod1) equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk6),mod1)* -> . % 1.05/1.30 2512[2:Spt:540.3] || -> equal(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))**. % 1.05/1.30 2529[2:SpR:2512.0,286.1] || -> is_aligned(sk3,sk7) equal(hazard_of_mortality(sk3,sk5),mod1)**. % 1.05/1.30 2536[2:MRR:2529.0,217.0] || -> equal(hazard_of_mortality(sk3,sk5),mod1)**. % 1.05/1.30 2557[2:SpR:2536.0,285.1] || -> positional_advantage(sk3,sk5)* equal(mod2,mod1). % 1.05/1.30 2565[2:MRR:2557.0,115.0] || -> equal(mod2,mod1)**. % 1.05/1.30 2566[2:Rew:2565.0,35.0] || -> greater(mod1,mod1)*. % 1.05/1.30 2570[2:Rew:2565.0,400.0] || greater(mod1,mod1)* -> . % 1.05/1.30 2835[2:MRR:2570.0,2566.0] || -> . % 1.05/1.30 2867[2:Spt:2835.0,540.3,2512.0] || equal(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))** -> . % 1.05/1.30 2868[2:Spt:2835.0,540.0,540.1,540.2] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7))* -> greater(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5)). % 1.05/1.30 2874[2:SpL:286.1,2868.1] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk6),mod1)* -> is_aligned(sk3,sk7) greater(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5)). % 1.05/1.32 2889[2:Rew:286.1,2874.3] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk6),mod1)* -> is_aligned(sk3,sk7) greater(mod1,hazard_of_mortality(sk3,sk5)). % 1.05/1.32 2890[2:MRR:2889.2,217.0] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk6),mod1)* -> greater(mod1,hazard_of_mortality(sk3,sk5)). % 1.05/1.32 3047[3:Spt:47.0] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4))** -> . % 1.05/1.32 3048[3:SpL:285.1,3047.0] || equal(hazard_of_mortality(sk3,sk4),mod2)** -> positional_advantage(sk3,sk5). % 1.05/1.32 3056[3:MRR:3048.1,115.0] || equal(hazard_of_mortality(sk3,sk4),mod2)** -> . % 1.05/1.32 3060[3:SpL:28.4,3056.0] organization(sk3) || is_aligned(sk3,sk4) equal(mod2,mod2) -> positional_advantage(sk3,sk4)* has_immunity(sk3,sk4). % 1.05/1.32 3067[3:Obv:3060.2] organization(sk3) || is_aligned(sk3,sk4) -> positional_advantage(sk3,sk4)* has_immunity(sk3,sk4). % 1.05/1.32 3068[3:SSi:3067.0,37.0,36.0] || is_aligned(sk3,sk4) -> positional_advantage(sk3,sk4)* has_immunity(sk3,sk4). % 1.05/1.32 3069[3:MRR:3068.0,3068.1,3068.2,284.0,156.0,112.0] || -> . % 1.05/1.32 3070[3:Spt:3069.0,47.0,3047.0] || -> equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4))**. % 1.05/1.32 3071[3:Spt:3069.0,47.1,47.2] || smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))* smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7)) -> . % 1.05/1.32 3081[3:Rew:3070.0,2890.2,3070.0,2890.0] || equal(hazard_of_mortality(sk3,sk4),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk6),mod1)* -> greater(mod1,hazard_of_mortality(sk3,sk4)). % 1.05/1.32 3082[3:Obv:3081.0] || smaller(hazard_of_mortality(sk3,sk6),mod1)* -> greater(mod1,hazard_of_mortality(sk3,sk4)). % 1.05/1.32 3125[3:SpR:3070.0,285.1] || -> positional_advantage(sk3,sk5) equal(hazard_of_mortality(sk3,sk4),mod2)**. % 1.05/1.32 3132[3:MRR:3125.0,115.0] || -> equal(hazard_of_mortality(sk3,sk4),mod2)**. % 1.05/1.32 3145[3:Rew:3132.0,3082.1] || smaller(hazard_of_mortality(sk3,sk6),mod1)* -> greater(mod1,mod2). % 1.05/1.32 3157[3:MRR:3145.1,400.0] || smaller(hazard_of_mortality(sk3,sk6),mod1)* -> . % 1.05/1.32 3189[3:SpL:121.2,3157.0] || positional_advantage(sk3,sk6) is_aligned(sk3,sk6) smaller(low,mod1)* -> . % 1.05/1.32 3198[3:MRR:3189.0,3189.1,114.0,842.0] || smaller(low,mod1)* -> . % 1.05/1.32 3199[3:Res:58.2,3198.0] || -> greater(low,mod1)*r equal(mod1,low). % 1.05/1.32 3203[3:MRR:3199.0,405.0] || -> equal(mod1,low)**. % 1.05/1.32 3204[3:Rew:3203.0,31.0] || -> greater(low,low)*. % 1.05/1.32 3208[3:Rew:3203.0,405.0] || greater(low,low)* -> . % 1.05/1.32 3450[3:MRR:3208.0,3204.0] || -> . % 1.05/1.32 3474[1:Spt:3450.0,76.0,127.0] || equal(age(sk3,sk6),sigma)** -> . % 1.05/1.32 3475[1:Spt:3450.0,76.1] || -> smaller(age(sk3,sk6),sigma)*. % 1.05/1.32 3479[1:Res:3475.0,54.0] || -> greater(sigma,age(sk3,sk6))*r. % 1.05/1.32 3665[2:Spt:47.0] || equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4))** -> . % 1.05/1.32 3667[2:SpL:285.1,3665.0] || equal(hazard_of_mortality(sk3,sk4),mod2)** -> positional_advantage(sk3,sk5). % 1.05/1.32 3673[2:MRR:3667.1,115.0] || equal(hazard_of_mortality(sk3,sk4),mod2)** -> . % 1.05/1.32 3678[2:SpL:28.4,3673.0] organization(sk3) || is_aligned(sk3,sk4) equal(mod2,mod2) -> positional_advantage(sk3,sk4)* has_immunity(sk3,sk4). % 1.05/1.32 3683[2:Obv:3678.2] organization(sk3) || is_aligned(sk3,sk4) -> positional_advantage(sk3,sk4)* has_immunity(sk3,sk4). % 1.05/1.32 3684[2:SSi:3683.0,37.0,36.0] || is_aligned(sk3,sk4) -> positional_advantage(sk3,sk4)* has_immunity(sk3,sk4). % 1.05/1.32 3685[2:MRR:3684.0,3684.1,3684.2,284.0,156.0,112.0] || -> . % 1.05/1.32 3686[2:Spt:3685.0,47.0,3665.0] || -> equal(hazard_of_mortality(sk3,sk5),hazard_of_mortality(sk3,sk4))**. % 1.05/1.32 3687[2:Spt:3685.0,47.1,47.2] || smaller(hazard_of_mortality(sk3,sk7),hazard_of_mortality(sk3,sk5))* smaller(hazard_of_mortality(sk3,sk6),hazard_of_mortality(sk3,sk7)) -> . % 1.05/1.32 3691[2:Rew:3686.0,2438.1,3686.0,2438.0] || greater(hazard_of_mortality(sk3,sk4),mod1) equal(hazard_of_mortality(sk3,sk4),hazard_of_mortality(sk3,sk4)) smaller(hazard_of_mortality(sk3,sk6),mod1)* -> . % 1.05/1.32 3692[2:Obv:3691.1] || greater(hazard_of_mortality(sk3,sk4),mod1) smaller(hazard_of_mortality(sk3,sk6),mod1)* -> . % 1.05/1.32 3721[2:SpR:3686.0,285.1] || -> positional_advantage(sk3,sk5) equal(hazard_of_mortality(sk3,sk4),mod2)**. % 1.05/1.32 3729[2:MRR:3721.0,115.0] || -> equal(hazard_of_mortality(sk3,sk4),mod2)**. % 1.05/1.32 3734[2:Rew:3729.0,3692.0] || greater(mod2,mod1) smaller(hazard_of_mortality(sk3,sk6),mod1)* -> . % 1.05/1.32 3749[2:MRR:3734.0,35.0] || smaller(hazard_of_mortality(sk3,sk6),mod1)* -> . % 1.05/1.32 3804[2:SpL:26.4,3749.0] organization(sk3) || positional_advantage(sk3,sk6) is_aligned(sk3,sk6) smaller(low,mod1)* -> has_immunity(sk3,sk6). % 1.05/1.32 3812[2:SSi:3804.0,37.0,36.0] || positional_advantage(sk3,sk6) is_aligned(sk3,sk6) smaller(low,mod1)* -> has_immunity(sk3,sk6). % 1.05/1.32 3813[2:MRR:3812.0,3812.3,114.0,112.0] || is_aligned(sk3,sk6) smaller(low,mod1)* -> . % 1.05/1.32 3819[2:Res:55.1,3813.1] || greater(mod1,low) is_aligned(sk3,sk6)* -> . % 1.05/1.32 3820[2:MRR:3819.0,31.0] || is_aligned(sk3,sk6)* -> . % 1.05/1.32 3849[1:OCh:57.1,57.0,3479.0,277.1] || -> is_aligned(sk3,sk6)* greater(sigma,sigma). % 1.05/1.32 3873[1:NCh:57.2,57.1,3479.0,407.0] || greater(sigma,sigma) -> is_aligned(sk3,sk6)*. % 1.05/1.32 3880[2:MRR:3849.0,3820.0] || -> greater(sigma,sigma)*. % 1.05/1.32 3881[2:MRR:3873.1,3820.0] || greater(sigma,sigma)* -> . % 1.05/1.32 3882[2:MRR:3881.0,3880.0] || -> . % 1.05/1.32 % SZS output end Refutation % 1.05/1.32 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_64 assumption_17_65 assumption_17_66 assumption_18b_69 assumption_19_73 theorem_10_74 theorem_10_75 theorem_10_76 theorem_10_77 theorem_10_79 theorem_10_80 theorem_10_81 theorem_10_82 theorem_10_83 theorem_10_84 theorem_10_85 definition_smaller_or_equal_1 definition_smaller_or_equal_2 definition_smaller_7 definition_smaller_8 meaning_postulate_greater_strict_9 meaning_postulate_greater_transitive_10 meaning_postulate_greater_comparable_11 % 1.05/1.32 %------------------------------------------------------------------------------