%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT030-1 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n012.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:50 AM UTC 2026 % Result : Unsatisfiable 0.07s 0.40s % Output : Refutation 0.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : MGT030-1 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.02 % Command : run_spass %d %s % 0.05/0.31 % Computer : n012.cluster.edu % 0.05/0.31 % Model : x86_64 x86_64 % 0.05/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.05/0.31 % Memory : 8046.5625MB % 0.05/0.31 % OS : Linux 6.8.0-71-generic % 0.05/0.31 % CPULimit : 300 % 0.05/0.31 % WCLimit : 300 % 0.05/0.31 % DateTime : Mon Sep 7 12:18:56 UTC 2026 % 0.05/0.31 % CPUTime : % 0.07/0.40 % 0.07/0.40 SPASS V 3.9 % 0.07/0.40 SPASS beiseite: Proof found. % 0.07/0.40 % SZS status Theorem % 0.07/0.40 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.07/0.40 SPASS derived 348 clauses, backtracked 180 clauses, performed 8 splits and kept 325 clauses. % 0.07/0.40 SPASS allocated 76120 KBytes. % 0.07/0.40 SPASS spent 0:00:00.09 on the problem. % 0.07/0.40 0:00:00.03 for the input. % 0.07/0.40 0:00:00.00 for the FLOTTER CNF translation. % 0.07/0.40 0:00:00.01 for inferences. % 0.07/0.40 0:00:00.00 for the backtracking. % 0.07/0.40 0:00:00.03 for the reduction. % 0.07/0.40 % 0.07/0.40 % 0.07/0.40 Here is a proof with depth 8, length 155 : % 0.07/0.40 % SZS output start Refutation % 0.07/0.40 1[0:Inp] environment(u) || in_environment(u,v) -> in_environment(u,sk2(u)) subpopulations(first_movers,efficient_producers,u,sk1(v,u))*. % 0.07/0.40 2[0:Inp] environment(u) || in_environment(u,v)+ -> in_environment(u,sk2(u))* greater_or_equal(sk1(v,u),v)*. % 0.07/0.40 3[0:Inp] environment(u) || in_environment(u,v) greater(growth_rate(efficient_producers,sk2(u)),growth_rate(first_movers,sk2(u)))*+ -> subpopulations(first_movers,efficient_producers,u,sk1(v,u))*. % 0.07/0.40 4[0:Inp] environment(u) || in_environment(u,v) greater(w,sk2(u)) subpopulations(first_movers,efficient_producers,u,w)*+ -> greater(growth_rate(efficient_producers,w),growth_rate(first_movers,w))* subpopulations(first_movers,efficient_producers,u,sk1(v,u))*. % 0.07/0.40 5[0:Inp] environment(u) || in_environment(u,v) greater(growth_rate(efficient_producers,sk2(u)),growth_rate(first_movers,sk2(u)))*+ -> greater_or_equal(sk1(v,u),v)*. % 0.07/0.40 6[0:Inp] environment(u) || in_environment(u,v) greater(w,sk2(u)) subpopulations(first_movers,efficient_producers,u,w)*+ -> greater_or_equal(sk1(v,u),v)* greater(growth_rate(efficient_producers,w),growth_rate(first_movers,w))*. % 0.07/0.40 7[0:Inp] environment(u) || in_environment(u,v) greater(growth_rate(efficient_producers,sk1(v,u)),growth_rate(first_movers,sk1(v,u)))* -> in_environment(u,sk2(u)). % 0.07/0.40 8[0:Inp] environment(u) || in_environment(u,v) greater(growth_rate(efficient_producers,sk2(u)),growth_rate(first_movers,sk2(u))) greater(growth_rate(efficient_producers,sk1(v,u)),growth_rate(first_movers,sk1(v,u)))* -> . % 0.07/0.40 9[0:Inp] environment(u) || in_environment(u,v) greater(w,sk2(u)) greater(growth_rate(efficient_producers,sk1(v,u)),growth_rate(first_movers,sk1(v,u)))*+ subpopulations(first_movers,efficient_producers,u,w)* -> greater(growth_rate(efficient_producers,w),growth_rate(first_movers,w))*. % 0.07/0.40 10[0:Inp] stable(u) environment(u) || -> in_environment(u,sk3(u))*. % 0.07/0.40 11[0:Inp] stable(u) environment(u) || greater_or_equal(v,sk3(u)) subpopulations(first_movers,efficient_producers,u,v)*+ -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v))*. % 0.07/0.40 12[0:Inp] || -> environment(sk4)*. % 0.07/0.40 13[0:Inp] || -> stable(sk4)*. % 0.07/0.40 14[0:Inp] || in_environment(sk4,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))* subpopulations(first_movers,efficient_producers,sk4,sk5(u)). % 0.07/0.40 15[0:Inp] || in_environment(sk4,u) -> greater(sk5(u),u) greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.40 16[0:Inp] || in_environment(sk4,u) greater(growth_rate(efficient_producers,sk5(u)),growth_rate(first_movers,sk5(u)))* -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u)). % 0.07/0.40 18[0:Res:13.0,10.1] environment(sk4) || -> in_environment(sk4,sk3(sk4))*. % 0.07/0.40 20[0:Res:12.0,4.0] || greater(u,sk2(sk4)) in_environment(sk4,v) subpopulations(first_movers,efficient_producers,sk4,u)+ -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))* subpopulations(first_movers,efficient_producers,sk4,sk1(v,sk4))*. % 0.07/0.40 21[0:Res:12.0,6.0] || greater(u,sk2(sk4)) in_environment(sk4,v) subpopulations(first_movers,efficient_producers,sk4,u)+ -> greater_or_equal(sk1(v,sk4),v)* greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.40 22[0:Res:12.0,8.0] || in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))) greater(growth_rate(efficient_producers,sk1(u,sk4)),growth_rate(first_movers,sk1(u,sk4)))* -> . % 0.07/0.40 23[0:Res:12.0,11.0] stable(sk4) || subpopulations(first_movers,efficient_producers,sk4,u) greater_or_equal(u,sk3(sk4)) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.40 24[0:Res:12.0,3.0] || in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))*+ -> subpopulations(first_movers,efficient_producers,sk4,sk1(u,sk4))*. % 0.07/0.40 25[0:Res:12.0,7.0] || in_environment(sk4,u) greater(growth_rate(efficient_producers,sk1(u,sk4)),growth_rate(first_movers,sk1(u,sk4)))* -> in_environment(sk4,sk2(sk4)). % 0.07/0.40 26[0:Res:12.0,5.0] || in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))*+ -> greater_or_equal(sk1(u,sk4),u)*. % 0.07/0.40 27[0:Res:12.0,1.0] || in_environment(sk4,u) -> in_environment(sk4,sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,sk1(u,sk4))*. % 0.07/0.40 28[0:Res:12.0,2.0] || in_environment(sk4,u) -> in_environment(sk4,sk2(sk4)) greater_or_equal(sk1(u,sk4),u)*. % 0.07/0.40 30[0:MRR:18.0,12.0] || -> in_environment(sk4,sk3(sk4))*. % 0.07/0.40 31[0:MRR:23.0,13.0] || greater_or_equal(u,sk3(sk4)) subpopulations(first_movers,efficient_producers,sk4,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.40 37[1:Spt:21.0,21.2,21.4] || greater(u,sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.40 38[2:Spt:28.0,28.2] || in_environment(sk4,u) -> greater_or_equal(sk1(u,sk4),u)*. % 0.07/0.40 39[3:Spt:27.0,27.2] || in_environment(sk4,u) -> subpopulations(first_movers,efficient_producers,sk4,sk1(u,sk4))*. % 0.07/0.40 40[0:Res:30.0,2.1] environment(sk4) || -> in_environment(sk4,sk2(sk4)) greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))*. % 0.07/0.40 41[0:Res:10.2,2.1] stable(u) environment(u) environment(u) || -> in_environment(u,sk2(u)) greater_or_equal(sk1(sk3(u),u),sk3(u))*. % 0.07/0.40 42[0:SSi:40.0,13.0,12.0] || -> in_environment(sk4,sk2(sk4)) greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))*. % 0.07/0.40 43[0:Obv:41.1] stable(u) environment(u) || -> in_environment(u,sk2(u)) greater_or_equal(sk1(sk3(u),u),sk3(u))*. % 0.07/0.40 44[0:Res:31.2,25.1] || greater_or_equal(sk1(u,sk4),sk3(sk4)) subpopulations(first_movers,efficient_producers,sk4,sk1(u,sk4))* in_environment(sk4,u) -> in_environment(sk4,sk2(sk4)). % 0.07/0.40 49[3:MRR:44.1,39.1] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> in_environment(sk4,sk2(sk4)). % 0.07/0.40 51[3:Res:42.1,49.0] || in_environment(sk4,sk3(sk4)) -> in_environment(sk4,sk2(sk4))* in_environment(sk4,sk2(sk4))*. % 0.07/0.40 53[3:Obv:51.1] || in_environment(sk4,sk3(sk4)) -> in_environment(sk4,sk2(sk4))*. % 0.07/0.40 54[3:MRR:53.0,30.0] || -> in_environment(sk4,sk2(sk4))*. % 0.07/0.40 60[1:Res:37.2,16.1] || greater(sk5(u),sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,sk5(u)) in_environment(sk4,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.40 61[1:MRR:60.1,14.2] || greater(sk5(u),sk2(sk4)) in_environment(sk4,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.40 72[0:Res:15.2,5.2] environment(u) || in_environment(sk4,sk2(u))+ in_environment(u,v) -> greater(sk5(sk2(u)),sk2(u))* greater_or_equal(sk1(v,u),v)*. % 0.07/0.40 101[3:Res:39.1,11.3] stable(sk4) environment(sk4) || in_environment(sk4,u) greater_or_equal(sk1(u,sk4),sk3(sk4)) -> greater(growth_rate(efficient_producers,sk1(u,sk4)),growth_rate(first_movers,sk1(u,sk4)))*. % 0.07/0.40 102[0:Res:1.3,11.3] environment(u) stable(u) environment(u) || in_environment(u,v) greater_or_equal(sk1(v,u),sk3(u)) -> in_environment(u,sk2(u)) greater(growth_rate(efficient_producers,sk1(v,u)),growth_rate(first_movers,sk1(v,u)))*. % 0.07/0.40 103[3:SSi:101.1,101.0,13.0,12.0,13.0,12.0] || in_environment(sk4,u) greater_or_equal(sk1(u,sk4),sk3(sk4)) -> greater(growth_rate(efficient_producers,sk1(u,sk4)),growth_rate(first_movers,sk1(u,sk4)))*. % 0.07/0.40 104[0:Obv:102.0] stable(u) environment(u) || in_environment(u,v) greater_or_equal(sk1(v,u),sk3(u)) -> in_environment(u,sk2(u)) greater(growth_rate(efficient_producers,sk1(v,u)),growth_rate(first_movers,sk1(v,u)))*. % 0.07/0.40 105[0:MRR:104.5,7.2] stable(u) environment(u) || in_environment(u,v) greater_or_equal(sk1(v,u),sk3(u))* -> in_environment(u,sk2(u)). % 0.07/0.40 107[0:Res:43.3,105.3] stable(u) environment(u) stable(u) environment(u) || in_environment(u,sk3(u)) -> in_environment(u,sk2(u))* in_environment(u,sk2(u))*. % 0.07/0.40 109[0:Obv:107.5] stable(u) environment(u) || in_environment(u,sk3(u)) -> in_environment(u,sk2(u))*. % 0.07/0.40 110[0:MRR:109.2,10.2] stable(u) environment(u) || -> in_environment(u,sk2(u))*. % 0.07/0.40 111[0:Res:110.2,72.1] stable(sk4) environment(sk4) environment(sk4) || in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4))* greater_or_equal(sk1(u,sk4),u)*. % 0.07/0.40 114[0:Obv:111.1] stable(sk4) environment(sk4) || in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4))* greater_or_equal(sk1(u,sk4),u)*. % 0.07/0.40 125[3:Res:103.2,8.3] environment(sk4) || in_environment(sk4,u) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))* -> . % 0.07/0.40 128[3:Obv:125.1] environment(sk4) || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))* -> . % 0.07/0.40 129[3:SSi:128.0,13.0,12.0] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))*+ -> . % 0.07/0.40 135[3:Res:61.2,129.2] || greater(sk5(sk2(sk4)),sk2(sk4))* in_environment(sk4,sk2(sk4)) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.40 138[3:Res:15.2,129.2] || in_environment(sk4,sk2(sk4)) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.40 140[3:MRR:138.0,54.0] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.40 142[3:MRR:135.1,54.0] || greater(sk5(sk2(sk4)),sk2(sk4))* greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.40 143[3:MRR:142.0,140.2] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.40 144[3:Res:38.1,143.0] || in_environment(sk4,sk3(sk4))* in_environment(sk4,sk3(sk4))* -> . % 0.07/0.40 145[3:Obv:144.0] || in_environment(sk4,sk3(sk4))* -> . % 0.07/0.40 146[3:MRR:145.0,30.0] || -> . % 0.07/0.40 147[3:Spt:146.0,27.1] || -> in_environment(sk4,sk2(sk4))*. % 0.07/0.40 155[1:Res:61.2,24.1] || greater(sk5(sk2(sk4)),sk2(sk4)) in_environment(sk4,sk2(sk4)) in_environment(sk4,u) -> subpopulations(first_movers,efficient_producers,sk4,sk1(u,sk4))*. % 0.07/0.40 158[0:Res:15.2,24.1] || in_environment(sk4,sk2(sk4)) in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,sk1(u,sk4))*. % 0.07/0.40 160[3:MRR:158.0,147.0] || in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,sk1(u,sk4))*. % 0.07/0.40 162[3:MRR:155.1,147.0] || greater(sk5(sk2(sk4)),sk2(sk4)) in_environment(sk4,u) -> subpopulations(first_movers,efficient_producers,sk4,sk1(u,sk4))*. % 0.07/0.40 163[3:MRR:162.0,160.1] || in_environment(sk4,u) -> subpopulations(first_movers,efficient_producers,sk4,sk1(u,sk4))*. % 0.07/0.40 166[3:Res:163.1,11.3] stable(sk4) environment(sk4) || in_environment(sk4,u) greater_or_equal(sk1(u,sk4),sk3(sk4)) -> greater(growth_rate(efficient_producers,sk1(u,sk4)),growth_rate(first_movers,sk1(u,sk4)))*. % 0.07/0.40 168[3:SSi:166.1,166.0,13.0,12.0,13.0,12.0] || in_environment(sk4,u) greater_or_equal(sk1(u,sk4),sk3(sk4)) -> greater(growth_rate(efficient_producers,sk1(u,sk4)),growth_rate(first_movers,sk1(u,sk4)))*. % 0.07/0.40 169[3:Res:168.2,8.3] environment(sk4) || in_environment(sk4,u) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))* -> . % 0.07/0.40 172[3:Obv:169.1] environment(sk4) || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))* -> . % 0.07/0.40 173[3:SSi:172.0,13.0,12.0] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))*+ -> . % 0.07/0.40 179[3:Res:61.2,173.2] || greater(sk5(sk2(sk4)),sk2(sk4))* in_environment(sk4,sk2(sk4)) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.40 182[3:Res:15.2,173.2] || in_environment(sk4,sk2(sk4)) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.40 184[3:MRR:182.0,147.0] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.40 186[3:MRR:179.1,147.0] || greater(sk5(sk2(sk4)),sk2(sk4))* greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.40 187[3:MRR:186.0,184.2] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.40 188[3:Res:38.1,187.0] || in_environment(sk4,sk3(sk4))* in_environment(sk4,sk3(sk4))* -> . % 0.07/0.40 189[3:Obv:188.0] || in_environment(sk4,sk3(sk4))* -> . % 0.07/0.40 190[3:MRR:189.0,30.0] || -> . % 0.07/0.40 191[2:Spt:190.0,28.1] || -> in_environment(sk4,sk2(sk4))*. % 0.07/0.40 192[0:SSi:114.1,114.0,13.0,12.0,13.0,12.0] || in_environment(sk4,u)+ -> greater(sk5(sk2(sk4)),sk2(sk4))* greater_or_equal(sk1(u,sk4),u)*. % 0.07/0.40 193[2:MRR:158.0,191.0] || in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,sk1(u,sk4))*. % 0.07/0.40 195[2:MRR:155.0,155.1,193.1,191.0] || in_environment(sk4,u) -> subpopulations(first_movers,efficient_producers,sk4,sk1(u,sk4))*. % 0.07/0.40 200[2:Res:195.1,11.3] stable(sk4) environment(sk4) || in_environment(sk4,u) greater_or_equal(sk1(u,sk4),sk3(sk4)) -> greater(growth_rate(efficient_producers,sk1(u,sk4)),growth_rate(first_movers,sk1(u,sk4)))*. % 0.07/0.40 203[2:SSi:200.1,200.0,13.0,12.0,13.0,12.0] || in_environment(sk4,u) greater_or_equal(sk1(u,sk4),sk3(sk4)) -> greater(growth_rate(efficient_producers,sk1(u,sk4)),growth_rate(first_movers,sk1(u,sk4)))*. % 0.07/0.40 205[3:Spt:192.0,192.2] || in_environment(sk4,u) -> greater_or_equal(sk1(u,sk4),u)*. % 0.07/0.40 206[2:Res:203.2,8.3] environment(sk4) || in_environment(sk4,u) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))* -> . % 0.07/0.40 209[2:Obv:206.1] environment(sk4) || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))* -> . % 0.07/0.40 210[2:SSi:209.0,13.0,12.0] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))*+ -> . % 0.07/0.40 216[2:Res:61.2,210.2] || greater(sk5(sk2(sk4)),sk2(sk4))* in_environment(sk4,sk2(sk4)) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.40 219[2:Res:15.2,210.2] || in_environment(sk4,sk2(sk4)) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.40 221[2:MRR:219.0,191.0] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.40 223[2:MRR:216.1,191.0] || greater(sk5(sk2(sk4)),sk2(sk4))* greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.40 224[2:MRR:223.0,221.2] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.40 235[3:Res:205.1,224.0] || in_environment(sk4,sk3(sk4))* in_environment(sk4,sk3(sk4))* -> . % 0.07/0.40 236[3:Obv:235.0] || in_environment(sk4,sk3(sk4))* -> . % 0.07/0.40 237[3:MRR:236.0,30.0] || -> . % 0.07/0.40 238[3:Spt:237.0,192.1] || -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.40 244[1:Res:61.2,26.1] || greater(sk5(sk2(sk4)),sk2(sk4))* in_environment(sk4,sk2(sk4)) in_environment(sk4,u) -> greater_or_equal(sk1(u,sk4),u)*. % 0.07/0.40 250[3:MRR:244.0,244.1,238.0,191.0] || in_environment(sk4,u) -> greater_or_equal(sk1(u,sk4),u)*. % 0.07/0.40 251[3:Res:250.1,224.0] || in_environment(sk4,sk3(sk4))* in_environment(sk4,sk3(sk4))* -> . % 0.07/0.40 252[3:Obv:251.0] || in_environment(sk4,sk3(sk4))* -> . % 0.07/0.40 253[3:MRR:252.0,30.0] || -> . % 0.07/0.40 254[1:Spt:253.0,21.1,21.3] || in_environment(sk4,u) -> greater_or_equal(sk1(u,sk4),u)*. % 0.07/0.40 262[2:Spt:20.1,20.4] || in_environment(sk4,u) -> subpopulations(first_movers,efficient_producers,sk4,sk1(u,sk4))*. % 0.07/0.40 263[2:Res:262.1,11.3] stable(sk4) environment(sk4) || in_environment(sk4,u) greater_or_equal(sk1(u,sk4),sk3(sk4)) -> greater(growth_rate(efficient_producers,sk1(u,sk4)),growth_rate(first_movers,sk1(u,sk4)))*. % 0.07/0.40 266[2:SSi:263.1,263.0,13.0,12.0,13.0,12.0] || in_environment(sk4,u) greater_or_equal(sk1(u,sk4),sk3(sk4)) -> greater(growth_rate(efficient_producers,sk1(u,sk4)),growth_rate(first_movers,sk1(u,sk4)))*. % 0.07/0.40 267[3:Spt:42.0] || -> in_environment(sk4,sk2(sk4))*. % 0.07/0.40 273[2:Res:266.2,9.3] environment(sk4) || in_environment(sk4,u) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(v,sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,v) -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v))*. % 0.07/0.41 274[2:Res:266.2,8.3] environment(sk4) || in_environment(sk4,u) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))* -> . % 0.07/0.41 277[2:Obv:274.1] environment(sk4) || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))* -> . % 0.07/0.41 278[2:SSi:277.0,13.0,12.0] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))*+ -> . % 0.07/0.41 279[2:Obv:273.1] environment(sk4) || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(v,sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,v) -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v))*. % 0.07/0.41 280[2:SSi:279.0,13.0,12.0] || greater_or_equal(sk1(u,sk4),sk3(sk4))*+ in_environment(sk4,u) greater(v,sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,v) -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v))*. % 0.07/0.41 287[2:Res:15.2,278.2] || in_environment(sk4,sk2(sk4)) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.41 288[3:MRR:287.0,267.0] || greater_or_equal(sk1(u,sk4),sk3(sk4))*+ in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.41 294[3:Res:254.1,288.0] || in_environment(sk4,sk3(sk4)) in_environment(sk4,sk3(sk4)) -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.41 295[3:Obv:294.0] || in_environment(sk4,sk3(sk4)) -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.41 296[3:MRR:295.0,30.0] || -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.41 328[0:Res:31.2,22.2] || greater_or_equal(sk1(u,sk4),sk3(sk4)) subpopulations(first_movers,efficient_producers,sk4,sk1(u,sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))* -> . % 0.07/0.41 412[2:Res:254.1,280.0] || in_environment(sk4,sk3(sk4)) in_environment(sk4,sk3(sk4)) greater(u,sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.41 413[2:Obv:412.0] || in_environment(sk4,sk3(sk4)) greater(u,sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.41 414[2:MRR:413.0,30.0] || greater(u,sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.41 415[2:Res:414.2,16.1] || greater(sk5(u),sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,sk5(u)) in_environment(sk4,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.41 428[2:MRR:415.1,14.2] || greater(sk5(u),sk2(sk4)) in_environment(sk4,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.41 438[2:Res:428.2,278.2] || greater(sk5(sk2(sk4)),sk2(sk4))* in_environment(sk4,sk2(sk4)) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.41 443[3:MRR:438.0,438.1,296.0,267.0] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.41 447[3:Res:254.1,443.0] || in_environment(sk4,sk3(sk4))* in_environment(sk4,sk3(sk4))* -> . % 0.07/0.41 448[3:Obv:447.0] || in_environment(sk4,sk3(sk4))* -> . % 0.07/0.41 449[3:MRR:448.0,30.0] || -> . % 0.07/0.41 450[3:Spt:449.0,42.0,267.0] || in_environment(sk4,sk2(sk4))* -> . % 0.07/0.41 451[3:Spt:449.0,42.1] || -> greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))*. % 0.07/0.41 456[3:Res:110.2,450.0] stable(sk4) environment(sk4) || -> . % 0.07/0.41 457[3:SSi:456.1,456.0,13.0,12.0,13.0,12.0] || -> . % 0.07/0.41 458[2:Spt:457.0,20.0,20.2,20.3] || greater(u,sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.41 459[0:MRR:328.1,24.2] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))*+ -> . % 0.07/0.41 472[2:Res:458.2,16.1] || greater(sk5(u),sk2(sk4)) subpopulations(first_movers,efficient_producers,sk4,sk5(u)) in_environment(sk4,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.41 480[2:MRR:472.1,14.2] || greater(sk5(u),sk2(sk4)) in_environment(sk4,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.07/0.41 488[3:Spt:42.0] || -> in_environment(sk4,sk2(sk4))*. % 0.07/0.41 517[2:Res:480.2,459.2] || greater(sk5(sk2(sk4)),sk2(sk4))* in_environment(sk4,sk2(sk4)) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.41 525[0:Res:15.2,459.2] || in_environment(sk4,sk2(sk4)) greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.41 526[3:MRR:525.0,488.0] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> greater(sk5(sk2(sk4)),sk2(sk4))*. % 0.07/0.41 529[3:MRR:517.1,488.0] || greater(sk5(sk2(sk4)),sk2(sk4))* greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.41 530[3:MRR:529.0,526.2] || greater_or_equal(sk1(u,sk4),sk3(sk4))* in_environment(sk4,u) -> . % 0.07/0.41 531[3:Res:254.1,530.0] || in_environment(sk4,sk3(sk4))* in_environment(sk4,sk3(sk4))* -> . % 0.07/0.41 532[3:Obv:531.0] || in_environment(sk4,sk3(sk4))* -> . % 0.07/0.41 533[3:MRR:532.0,30.0] || -> . % 0.07/0.41 534[3:Spt:533.0,42.0,488.0] || in_environment(sk4,sk2(sk4))* -> . % 0.07/0.41 535[3:Spt:533.0,42.1] || -> greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))*. % 0.07/0.41 540[3:Res:110.2,534.0] stable(sk4) environment(sk4) || -> . % 0.07/0.41 541[3:SSi:540.1,540.0,13.0,12.0,13.0,12.0] || -> . % 0.07/0.41 % SZS output end Refutation % 0.07/0.41 Formulae used in the proof : mp_earliest_time_growth_rate_exceeds_1 mp_earliest_time_growth_rate_exceeds_2 mp_earliest_time_growth_rate_exceeds_3 mp_earliest_time_growth_rate_exceeds_4 mp_earliest_time_growth_rate_exceeds_5 mp_earliest_time_growth_rate_exceeds_6 mp_earliest_time_growth_rate_exceeds_7 mp_earliest_time_growth_rate_exceeds_8 mp_earliest_time_growth_rate_exceeds_9 l1_10 l1_11 prove_l12_12 prove_l12_13 prove_l12_14 prove_l12_15 prove_l12_16 % 0.07/0.41 %------------------------------------------------------------------------------