%------------------------------------------------------------------------------ % 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 : n008.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.05s 1.39s % Output : Refutation 1.15s % 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.04 % Command : run_spass %d %s % 0.09/0.36 % Computer : n008.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Mon Sep 7 13:43:23 UTC 2026 % 0.09/0.36 % CPUTime : % 1.05/1.39 % 1.05/1.39 SPASS V 3.9 % 1.05/1.39 SPASS beiseite: Proof found. % 1.05/1.39 % SZS status Theorem % 1.05/1.39 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.05/1.39 SPASS derived 3413 clauses, backtracked 660 clauses, performed 8 splits and kept 1870 clauses. % 1.05/1.39 SPASS allocated 99973 KBytes. % 1.05/1.39 SPASS spent 0:00:01.01 on the problem. % 1.05/1.39 0:00:00.06 for the input. % 1.05/1.39 0:00:00.06 for the FLOTTER CNF translation. % 1.05/1.39 0:00:00.05 for inferences. % 1.05/1.39 0:00:00.00 for the backtracking. % 1.05/1.39 0:00:00.78 for the reduction. % 1.05/1.39 % 1.05/1.39 % 1.05/1.39 Here is a proof with depth 5, length 142 : % 1.05/1.39 % SZS output start Refutation % 1.05/1.39 1[0:Inp] || -> organization(skc5)*. % 1.05/1.39 2[0:Inp] || -> robust_position(skc5)*. % 1.05/1.39 3[0:Inp] || has_endowment(skc5)* -> . % 1.05/1.39 4[0:Inp] || -> greater(sigma,tau)*r. % 1.05/1.39 5[0:Inp] || -> greater(tau,zero)*l. % 1.05/1.39 8[0:Inp] || -> greater(mod1,low)*l. % 1.05/1.39 12[0:Inp] || -> greater(mod2,mod1)*l. % 1.05/1.39 13[0:Inp] || -> greater(age(skc5,skc9),sigma)*l. % 1.05/1.39 14[0:Inp] || -> smaller_or_equal(age(skc5,skc8),sigma)*. % 1.05/1.39 15[0:Inp] || -> greater(age(skc5,skc8),tau)*l. % 1.05/1.39 16[0:Inp] || -> smaller_or_equal(age(skc5,skc7),tau)*. % 1.05/1.39 17[0:Inp] || -> equal(age(skc5,skc6),zero)**. % 1.05/1.39 19[0:Inp] || dissimilar(u,v,w)* -> organization(u). % 1.05/1.39 20[0:Inp] || smaller(u,v)* -> smaller_or_equal(u,v). % 1.05/1.39 24[0:Inp] || smaller(u,v)* -> greater(v,u). % 1.05/1.39 25[0:Inp] || greater(u,v) -> smaller(v,u)*. % 1.05/1.39 26[0:Inp] || greater(u,v)*+ greater(v,u)* -> . % 1.05/1.39 27[0:Inp] organization(u) || has_immunity(u,v)* -> has_endowment(u). % 1.05/1.39 28[0:Inp] || -> greater(u,v) equal(u,v) smaller(u,v)*. % 1.05/1.39 29[0:Inp] || smaller_or_equal(u,v) -> equal(u,v) smaller(u,v)*. % 1.05/1.39 33[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 1.05/1.39 35[0:Inp] organization(u) || equal(age(u,v),zero)** -> is_aligned(u,v). % 1.05/1.39 36[0:Inp] robust_position(u) || greater(age(u,v),tau)*l -> positional_advantage(u,v). % 1.05/1.39 40[0:Inp] || is_aligned(u,v) is_aligned(u,w) dissimilar(u,w,v)* -> . % 1.05/1.39 41[0:Inp] robust_position(u) || positional_advantage(u,v) smaller_or_equal(age(u,v),tau)* -> . % 1.05/1.39 44[0:Inp] organization(u) || is_aligned(u,v) -> is_aligned(u,w) dissimilar(u,v,w)*. % 1.05/1.39 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.05/1.39 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.05/1.39 53[0:Inp] organization(u) || greater(age(u,v),sigma) equal(age(u,w),zero) -> dissimilar(u,w,v)*. % 1.05/1.39 54[0:Inp] organization(u) || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 1.05/1.39 55[0:Inp] organization(u) || is_aligned(u,v) positional_advantage(u,v) -> has_immunity(u,v) equal(hazard_of_mortality(u,v),low)**. % 1.05/1.39 56[0:Inp] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7))* smaller(hazard_of_mortality(skc5,skc8),hazard_of_mortality(skc5,skc9)) -> . % 1.05/1.39 58[0:MRR:54.0,19.1] || equal(age(u,v),zero) dissimilar(u,v,w)* -> greater(age(u,w),sigma). % 1.05/1.39 59[0:Res:2.0,36.0] || greater(age(skc5,u),tau)*l -> positional_advantage(skc5,u). % 1.05/1.39 60[0:Res:2.0,41.0] || positional_advantage(skc5,u) smaller_or_equal(age(skc5,u),tau)* -> . % 1.05/1.39 62[0:Res:1.0,55.0] || positional_advantage(skc5,u) is_aligned(skc5,u) -> equal(hazard_of_mortality(skc5,u),low)** has_immunity(skc5,u). % 1.05/1.39 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.05/1.39 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.05/1.39 67[0:Res:1.0,44.0] || is_aligned(skc5,u) -> is_aligned(skc5,v) dissimilar(skc5,u,v)*. % 1.05/1.39 71[0:Res:1.0,27.0] || has_immunity(skc5,u)* -> has_endowment(skc5). % 1.05/1.39 74[0:Res:17.0,58.0] || dissimilar(skc5,skc6,u)* -> greater(age(skc5,u),sigma). % 1.05/1.39 76[0:Res:17.0,35.1] organization(skc5) || -> is_aligned(skc5,skc6)*. % 1.05/1.39 81[0:Res:16.0,41.2] robust_position(skc5) || positional_advantage(skc5,skc7)* -> . % 1.05/1.39 83[0:Res:14.0,29.0] || -> equal(age(skc5,skc8),sigma) smaller(age(skc5,skc8),sigma)*. % 1.05/1.39 90[0:Res:5.0,25.0] || -> smaller(zero,tau)*. % 1.05/1.39 96[0:Res:15.0,36.1] robust_position(skc5) || -> positional_advantage(skc5,skc8)*. % 1.05/1.39 101[0:Res:13.0,53.2] organization(skc5) || equal(age(skc5,u),zero) -> dissimilar(skc5,u,skc9)*. % 1.05/1.39 110[0:MRR:71.1,3.0] || has_immunity(skc5,u)* -> . % 1.05/1.39 111[0:MRR:76.0,1.0] || -> is_aligned(skc5,skc6)*. % 1.05/1.39 112[0:MRR:96.0,2.0] || -> positional_advantage(skc5,skc8)*. % 1.05/1.39 113[0:MRR:81.0,2.0] || positional_advantage(skc5,skc7)* -> . % 1.05/1.39 115[0:MRR:101.0,1.0] || equal(age(skc5,u),zero) -> dissimilar(skc5,u,skc9)*. % 1.05/1.39 117[0:MRR:63.3,110.0] || positional_advantage(skc5,u) -> is_aligned(skc5,u) equal(hazard_of_mortality(skc5,u),mod1)**. % 1.05/1.39 118[0:MRR:64.3,110.0] || is_aligned(skc5,u) -> positional_advantage(skc5,u) equal(hazard_of_mortality(skc5,u),mod2)**. % 1.05/1.39 119[0:MRR:62.3,110.0] || is_aligned(skc5,u) positional_advantage(skc5,u) -> equal(hazard_of_mortality(skc5,u),low)**. % 1.05/1.39 123[0:Res:17.0,115.0] || -> dissimilar(skc5,skc6,skc9)*. % 1.05/1.39 127[1:Spt:83.0] || -> equal(age(skc5,skc8),sigma)**. % 1.05/1.39 136[0:Res:90.0,20.0] || -> smaller_or_equal(zero,tau)*. % 1.05/1.39 152[0:SpL:17.0,60.1] || positional_advantage(skc5,skc6)* smaller_or_equal(zero,tau) -> . % 1.05/1.39 156[0:MRR:152.1,136.0] || positional_advantage(skc5,skc6)* -> . % 1.05/1.39 212[0:Res:123.0,40.2] || is_aligned(skc5,skc9)* is_aligned(skc5,skc6) -> . % 1.05/1.39 216[0:MRR:212.1,111.0] || is_aligned(skc5,skc9)* -> . % 1.05/1.39 271[0:Res:67.2,74.0] || is_aligned(skc5,skc6) -> is_aligned(skc5,u) greater(age(skc5,u),sigma)*l. % 1.05/1.39 276[0:MRR:271.0,111.0] || -> is_aligned(skc5,u) greater(age(skc5,u),sigma)*l. % 1.05/1.39 277[1:SpR:127.0,276.1] || -> is_aligned(skc5,skc8)* greater(sigma,sigma). % 1.05/1.39 280[0:NCh:33.2,33.0,276.1,59.0] || greater(sigma,tau) -> is_aligned(skc5,u) positional_advantage(skc5,u)*. % 1.05/1.39 283[0:MRR:280.0,4.0] || -> is_aligned(skc5,u) positional_advantage(skc5,u)*. % 1.05/1.39 284[0:MRR:118.0,283.0] || -> positional_advantage(skc5,u) equal(hazard_of_mortality(skc5,u),mod2)**. % 1.05/1.39 285[0:MRR:117.0,283.1] || -> is_aligned(skc5,u) equal(hazard_of_mortality(skc5,u),mod1)**. % 1.05/1.39 368[0:Res:12.0,26.0] || greater(mod1,mod2)*r -> . % 1.05/1.39 373[0:Res:8.0,26.0] || greater(low,mod1)*r -> . % 1.05/1.39 380[0:Res:276.1,26.0] || greater(sigma,age(skc5,u))*r -> is_aligned(skc5,u). % 1.05/1.39 603[0:Res:28.2,56.1] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc8),hazard_of_mortality(skc5,skc9))* -> greater(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7)) equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7)). % 1.05/1.39 605[0:Res:25.1,56.1] || greater(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc9)) equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc8),hazard_of_mortality(skc5,skc9))* -> . % 1.05/1.39 795[1:SpL:127.0,380.0] || greater(sigma,sigma) -> is_aligned(skc5,skc8)*. % 1.05/1.39 800[1:MRR:795.0,277.1] || -> is_aligned(skc5,skc8)*. % 1.05/1.39 2368[0:SpL:285.1,605.2] || greater(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc9)) equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc8),mod1)* -> is_aligned(skc5,skc9). % 1.05/1.39 2387[0:Rew:285.1,2368.0] || greater(hazard_of_mortality(skc5,skc7),mod1) equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc8),mod1)* -> is_aligned(skc5,skc9). % 1.05/1.39 2388[0:MRR:2387.3,216.0] || greater(hazard_of_mortality(skc5,skc7),mod1) equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc8),mod1)* -> . % 1.05/1.39 2462[2:Spt:603.3] || -> equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7))**. % 1.05/1.39 2479[2:SpR:2462.0,285.1] || -> is_aligned(skc5,skc9) equal(hazard_of_mortality(skc5,skc7),mod1)**. % 1.05/1.39 2486[2:MRR:2479.0,216.0] || -> equal(hazard_of_mortality(skc5,skc7),mod1)**. % 1.05/1.39 2507[2:SpR:2486.0,284.1] || -> positional_advantage(skc5,skc7)* equal(mod2,mod1). % 1.05/1.39 2515[2:MRR:2507.0,113.0] || -> equal(mod2,mod1)**. % 1.05/1.39 2516[2:Rew:2515.0,12.0] || -> greater(mod1,mod1)*. % 1.05/1.39 2520[2:Rew:2515.0,368.0] || greater(mod1,mod1)* -> . % 1.05/1.39 2776[2:MRR:2520.0,2516.0] || -> . % 1.05/1.39 2808[2:Spt:2776.0,603.3,2462.0] || equal(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7))** -> . % 1.05/1.39 2809[2:Spt:2776.0,603.0,603.1,603.2] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc8),hazard_of_mortality(skc5,skc9))* -> greater(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7)). % 1.15/1.41 2815[2:SpL:285.1,2809.1] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc8),mod1)* -> is_aligned(skc5,skc9) greater(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7)). % 1.15/1.41 2830[2:Rew:285.1,2815.3] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc8),mod1)* -> is_aligned(skc5,skc9) greater(mod1,hazard_of_mortality(skc5,skc7)). % 1.15/1.41 2831[2:MRR:2830.2,216.0] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc8),mod1)* -> greater(mod1,hazard_of_mortality(skc5,skc7)). % 1.15/1.41 2999[3:Spt:56.0] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6))** -> . % 1.15/1.41 3000[3:SpL:284.1,2999.0] || equal(hazard_of_mortality(skc5,skc6),mod2)** -> positional_advantage(skc5,skc7). % 1.15/1.41 3008[3:MRR:3000.1,113.0] || equal(hazard_of_mortality(skc5,skc6),mod2)** -> . % 1.15/1.41 3012[3:SpL:52.4,3008.0] organization(skc5) || is_aligned(skc5,skc6) equal(mod2,mod2) -> has_immunity(skc5,skc6) positional_advantage(skc5,skc6)*. % 1.15/1.41 3019[3:Obv:3012.2] organization(skc5) || is_aligned(skc5,skc6) -> has_immunity(skc5,skc6) positional_advantage(skc5,skc6)*. % 1.15/1.41 3020[3:SSi:3019.0,2.0,1.0] || is_aligned(skc5,skc6) -> has_immunity(skc5,skc6) positional_advantage(skc5,skc6)*. % 1.15/1.41 3021[3:MRR:3020.0,3020.1,3020.2,283.0,110.0,156.0] || -> . % 1.15/1.41 3022[3:Spt:3021.0,56.0,2999.0] || -> equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6))**. % 1.15/1.41 3023[3:Spt:3021.0,56.1,56.2] || smaller(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7))* smaller(hazard_of_mortality(skc5,skc8),hazard_of_mortality(skc5,skc9)) -> . % 1.15/1.41 3033[3:Rew:3022.0,2831.2,3022.0,2831.0] || equal(hazard_of_mortality(skc5,skc6),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc8),mod1)* -> greater(mod1,hazard_of_mortality(skc5,skc6)). % 1.15/1.41 3034[3:Obv:3033.0] || smaller(hazard_of_mortality(skc5,skc8),mod1)* -> greater(mod1,hazard_of_mortality(skc5,skc6)). % 1.15/1.41 3077[3:SpR:3022.0,284.1] || -> positional_advantage(skc5,skc7) equal(hazard_of_mortality(skc5,skc6),mod2)**. % 1.15/1.41 3084[3:MRR:3077.0,113.0] || -> equal(hazard_of_mortality(skc5,skc6),mod2)**. % 1.15/1.41 3097[3:Rew:3084.0,3034.1] || smaller(hazard_of_mortality(skc5,skc8),mod1)* -> greater(mod1,mod2). % 1.15/1.41 3109[3:MRR:3097.1,368.0] || smaller(hazard_of_mortality(skc5,skc8),mod1)* -> . % 1.15/1.41 3141[3:SpL:119.2,3109.0] || is_aligned(skc5,skc8) positional_advantage(skc5,skc8) smaller(low,mod1)* -> . % 1.15/1.41 3150[3:MRR:3141.0,3141.1,800.0,112.0] || smaller(low,mod1)* -> . % 1.15/1.41 3151[3:Res:28.2,3150.0] || -> greater(low,mod1)*r equal(mod1,low). % 1.15/1.41 3155[3:MRR:3151.0,373.0] || -> equal(mod1,low)**. % 1.15/1.41 3156[3:Rew:3155.0,8.0] || -> greater(low,low)*. % 1.15/1.41 3160[3:Rew:3155.0,373.0] || greater(low,low)* -> . % 1.15/1.41 3399[3:MRR:3160.0,3156.0] || -> . % 1.15/1.41 3423[1:Spt:3399.0,83.0,127.0] || equal(age(skc5,skc8),sigma)** -> . % 1.15/1.41 3424[1:Spt:3399.0,83.1] || -> smaller(age(skc5,skc8),sigma)*. % 1.15/1.41 3428[1:Res:3424.0,24.0] || -> greater(sigma,age(skc5,skc8))*r. % 1.15/1.41 3606[2:Spt:56.0] || equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6))** -> . % 1.15/1.41 3608[2:SpL:284.1,3606.0] || equal(hazard_of_mortality(skc5,skc6),mod2)** -> positional_advantage(skc5,skc7). % 1.15/1.41 3614[2:MRR:3608.1,113.0] || equal(hazard_of_mortality(skc5,skc6),mod2)** -> . % 1.15/1.41 3619[2:SpL:52.4,3614.0] organization(skc5) || is_aligned(skc5,skc6) equal(mod2,mod2) -> has_immunity(skc5,skc6) positional_advantage(skc5,skc6)*. % 1.15/1.41 3624[2:Obv:3619.2] organization(skc5) || is_aligned(skc5,skc6) -> has_immunity(skc5,skc6) positional_advantage(skc5,skc6)*. % 1.15/1.41 3625[2:SSi:3624.0,2.0,1.0] || is_aligned(skc5,skc6) -> has_immunity(skc5,skc6) positional_advantage(skc5,skc6)*. % 1.15/1.41 3626[2:MRR:3625.0,3625.1,3625.2,283.0,110.0,156.0] || -> . % 1.15/1.41 3627[2:Spt:3626.0,56.0,3606.0] || -> equal(hazard_of_mortality(skc5,skc7),hazard_of_mortality(skc5,skc6))**. % 1.15/1.41 3628[2:Spt:3626.0,56.1,56.2] || smaller(hazard_of_mortality(skc5,skc9),hazard_of_mortality(skc5,skc7))* smaller(hazard_of_mortality(skc5,skc8),hazard_of_mortality(skc5,skc9)) -> . % 1.15/1.41 3632[2:Rew:3627.0,2388.1,3627.0,2388.0] || greater(hazard_of_mortality(skc5,skc6),mod1) equal(hazard_of_mortality(skc5,skc6),hazard_of_mortality(skc5,skc6)) smaller(hazard_of_mortality(skc5,skc8),mod1)* -> . % 1.15/1.41 3633[2:Obv:3632.1] || greater(hazard_of_mortality(skc5,skc6),mod1) smaller(hazard_of_mortality(skc5,skc8),mod1)* -> . % 1.15/1.41 3662[2:SpR:3627.0,284.1] || -> positional_advantage(skc5,skc7) equal(hazard_of_mortality(skc5,skc6),mod2)**. % 1.15/1.41 3670[2:MRR:3662.0,113.0] || -> equal(hazard_of_mortality(skc5,skc6),mod2)**. % 1.15/1.41 3675[2:Rew:3670.0,3633.0] || greater(mod2,mod1) smaller(hazard_of_mortality(skc5,skc8),mod1)* -> . % 1.15/1.41 3690[2:MRR:3675.0,12.0] || smaller(hazard_of_mortality(skc5,skc8),mod1)* -> . % 1.15/1.41 3745[2:SpL:55.4,3690.0] organization(skc5) || is_aligned(skc5,skc8) positional_advantage(skc5,skc8) smaller(low,mod1)* -> has_immunity(skc5,skc8). % 1.15/1.41 3753[2:SSi:3745.0,2.0,1.0] || is_aligned(skc5,skc8) positional_advantage(skc5,skc8) smaller(low,mod1)* -> has_immunity(skc5,skc8). % 1.15/1.41 3754[2:MRR:3753.1,3753.3,112.0,110.0] || is_aligned(skc5,skc8) smaller(low,mod1)* -> . % 1.15/1.41 3760[2:Res:25.1,3754.1] || greater(mod1,low) is_aligned(skc5,skc8)* -> . % 1.15/1.41 3761[2:MRR:3760.0,8.0] || is_aligned(skc5,skc8)* -> . % 1.15/1.41 3791[1:OCh:33.1,33.0,3428.0,276.1] || -> is_aligned(skc5,skc8)* greater(sigma,sigma). % 1.15/1.41 3797[1:NCh:33.2,33.1,3428.0,380.0] || greater(sigma,sigma) -> is_aligned(skc5,skc8)*. % 1.15/1.41 3820[2:MRR:3791.0,3761.0] || -> greater(sigma,sigma)*. % 1.15/1.41 3821[2:MRR:3797.1,3761.0] || greater(sigma,sigma)* -> . % 1.15/1.41 3822[2:MRR:3821.0,3820.0] || -> . % 1.15/1.41 % SZS output end Refutation % 1.15/1.41 Formulae used in the proof : theorem_10 assumption_18b 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.15/1.41 %------------------------------------------------------------------------------