%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT023-2 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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:49 AM UTC 2026 % Result : Unsatisfiable 0.45s 0.75s % Output : Refutation 0.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT023-2 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : run_spass %d %s % 0.07/0.33 % Computer : n028.cluster.edu % 0.07/0.33 % Model : x86_64 x86_64 % 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.33 % Memory : 8046.5625MB % 0.07/0.33 % OS : Linux 6.8.0-71-generic % 0.07/0.33 % CPULimit : 300 % 0.07/0.33 % WCLimit : 300 % 0.07/0.33 % DateTime : Mon Sep 7 12:10:02 UTC 2026 % 0.07/0.34 % CPUTime : % 0.45/0.75 % 0.45/0.75 SPASS V 3.9 % 0.45/0.75 SPASS beiseite: Proof found. % 0.45/0.75 % SZS status Theorem % 0.45/0.75 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.45/0.75 SPASS derived 730 clauses, backtracked 499 clauses, performed 27 splits and kept 899 clauses. % 0.45/0.75 SPASS allocated 76465 KBytes. % 0.45/0.75 SPASS spent 0:00:00.40 on the problem. % 0.45/0.75 0:00:00.06 for the input. % 0.45/0.75 0:00:00.00 for the FLOTTER CNF translation. % 0.45/0.75 0:00:00.02 for inferences. % 0.45/0.75 0:00:00.01 for the backtracking. % 0.45/0.75 0:00:00.27 for the reduction. % 0.45/0.75 % 0.45/0.75 % 0.45/0.75 Here is a proof with depth 9, length 259 : % 0.45/0.75 % SZS output start Refutation % 0.45/0.75 1[0:Inp] environment(u) || in_environment(u,v) -> in_environment(u,sk2(u)) subpopulations(first_movers,efficient_producers,u,sk1(v,u))*. % 0.45/0.75 2[0:Inp] environment(u) || in_environment(u,v)+ -> in_environment(u,sk2(u))* greater_or_equal(sk1(v,u),v)*. % 0.45/0.75 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.45/0.75 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.45/0.75 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.45/0.75 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.45/0.75 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.45/0.75 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.45/0.75 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.45/0.75 10[0:Inp] environment(u) || in_environment(u,v)+ -> equal(v,critical_point(u)) greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v))* subpopulations(first_movers,efficient_producers,u,sk3(v,u))*. % 0.45/0.75 11[0:Inp] environment(u) || in_environment(u,v)+ -> equal(v,critical_point(u)) greater(sk3(v,u),v)* greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v))*. % 0.45/0.75 12[0:Inp] environment(u) || in_environment(u,v) greater(growth_rate(efficient_producers,sk3(v,u)),growth_rate(first_movers,sk3(v,u)))* -> equal(v,critical_point(u)) greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v)). % 0.45/0.75 13[0:Inp] stable(u) environment(u) || -> in_environment(u,sk4(u))*. % 0.45/0.75 14[0:Inp] stable(u) environment(u) || greater_or_equal(v,sk4(u)) subpopulations(first_movers,efficient_producers,u,v)*+ -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v))*. % 0.45/0.75 15[0:Inp] || -> environment(sk5)*. % 0.45/0.75 16[0:Inp] || -> stable(sk5)*. % 0.45/0.75 17[0:Inp] || in_environment(sk5,critical_point(sk5))* -> . % 0.45/0.75 19[0:Res:16.0,13.1] environment(sk5) || -> in_environment(sk5,sk4(sk5))*. % 0.45/0.75 21[0:Res:15.0,4.0] || greater(u,sk2(sk5)) in_environment(sk5,v) subpopulations(first_movers,efficient_producers,sk5,u)+ -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))* subpopulations(first_movers,efficient_producers,sk5,sk1(v,sk5))*. % 0.45/0.75 22[0:Res:15.0,12.0] || in_environment(sk5,u) greater(growth_rate(efficient_producers,sk3(u,sk5)),growth_rate(first_movers,sk3(u,sk5)))* -> equal(u,critical_point(sk5)) greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u)). % 0.45/0.75 23[0:Res:15.0,6.0] || greater(u,sk2(sk5)) in_environment(sk5,v) subpopulations(first_movers,efficient_producers,sk5,u)+ -> greater_or_equal(sk1(v,sk5),v)* greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 24[0:Res:15.0,8.0] || in_environment(sk5,u) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5))) greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))* -> . % 0.45/0.75 25[0:Res:15.0,10.0] || in_environment(sk5,u) -> equal(u,critical_point(sk5)) greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))* subpopulations(first_movers,efficient_producers,sk5,sk3(u,sk5)). % 0.45/0.75 26[0:Res:15.0,14.0] stable(sk5) || subpopulations(first_movers,efficient_producers,sk5,u) greater_or_equal(u,sk4(sk5)) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 27[0:Res:15.0,3.0] || in_environment(sk5,u) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*+ -> subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))*. % 0.45/0.75 28[0:Res:15.0,11.0] || in_environment(sk5,u) -> equal(u,critical_point(sk5)) greater(sk3(u,sk5),u) greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 29[0:Res:15.0,7.0] || in_environment(sk5,u) greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))* -> in_environment(sk5,sk2(sk5)). % 0.45/0.75 30[0:Res:15.0,5.0] || in_environment(sk5,u) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*+ -> greater_or_equal(sk1(u,sk5),u)*. % 0.45/0.75 31[0:Res:15.0,1.0] || in_environment(sk5,u) -> in_environment(sk5,sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))*. % 0.45/0.75 32[0:Res:15.0,2.0] || in_environment(sk5,u) -> in_environment(sk5,sk2(sk5)) greater_or_equal(sk1(u,sk5),u)*. % 0.45/0.75 34[0:MRR:19.0,15.0] || -> in_environment(sk5,sk4(sk5))*. % 0.45/0.75 35[0:MRR:26.0,16.0] || greater_or_equal(u,sk4(sk5)) subpopulations(first_movers,efficient_producers,sk5,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 36[1:Spt:23.0,23.2,23.4] || greater(u,sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 37[2:Spt:32.0,32.2] || in_environment(sk5,u) -> greater_or_equal(sk1(u,sk5),u)*. % 0.45/0.75 38[3:Spt:31.0,31.2] || in_environment(sk5,u) -> subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))*. % 0.45/0.75 39[0:Res:34.0,2.1] environment(sk5) || -> in_environment(sk5,sk2(sk5)) greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))*. % 0.45/0.75 40[0:Res:13.2,2.1] stable(u) environment(u) environment(u) || -> in_environment(u,sk2(u)) greater_or_equal(sk1(sk4(u),u),sk4(u))*. % 0.45/0.75 41[0:SSi:39.0,16.0,15.0] || -> in_environment(sk5,sk2(sk5)) greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))*. % 0.45/0.75 42[0:Obv:40.1] stable(u) environment(u) || -> in_environment(u,sk2(u)) greater_or_equal(sk1(sk4(u),u),sk4(u))*. % 0.45/0.75 43[0:Res:35.2,29.1] || greater_or_equal(sk1(u,sk5),sk4(sk5)) subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))* in_environment(sk5,u) -> in_environment(sk5,sk2(sk5)). % 0.45/0.75 46[3:MRR:43.1,38.1] || greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) -> in_environment(sk5,sk2(sk5)). % 0.45/0.75 48[3:Res:41.1,46.0] || in_environment(sk5,sk4(sk5))* -> in_environment(sk5,sk2(sk5)) in_environment(sk5,sk2(sk5)). % 0.45/0.75 50[3:Obv:48.1] || in_environment(sk5,sk4(sk5))* -> in_environment(sk5,sk2(sk5)). % 0.45/0.75 51[3:MRR:50.0,34.0] || -> in_environment(sk5,sk2(sk5))*. % 0.45/0.75 63[0:Res:34.0,11.1] environment(sk5) || -> equal(sk4(sk5),critical_point(sk5)) greater(sk3(sk4(sk5),sk5),sk4(sk5)) greater(growth_rate(efficient_producers,sk4(sk5)),growth_rate(first_movers,sk4(sk5)))*. % 0.45/0.75 64[3:Res:51.0,11.1] environment(sk5) || -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 66[3:SSi:64.0,16.0,15.0] || -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 67[0:SSi:63.0,16.0,15.0] || -> equal(sk4(sk5),critical_point(sk5)) greater(sk3(sk4(sk5),sk5),sk4(sk5)) greater(growth_rate(efficient_producers,sk4(sk5)),growth_rate(first_movers,sk4(sk5)))*. % 0.45/0.75 73[4:Spt:66.0] || -> equal(critical_point(sk5),sk2(sk5))**. % 0.45/0.75 74[4:Rew:73.0,17.0] || in_environment(sk5,sk2(sk5))* -> . % 0.45/0.75 85[4:MRR:74.0,51.0] || -> . % 0.45/0.75 86[4:Spt:85.0,66.0,73.0] || equal(critical_point(sk5),sk2(sk5))** -> . % 0.45/0.75 87[4:Spt:85.0,66.1,66.2] || -> greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 93[3:Res:38.1,14.3] stable(sk5) environment(sk5) || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5)) -> greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))*. % 0.45/0.75 94[0:Res:1.3,14.3] environment(u) stable(u) environment(u) || in_environment(u,v) greater_or_equal(sk1(v,u),sk4(u)) -> in_environment(u,sk2(u)) greater(growth_rate(efficient_producers,sk1(v,u)),growth_rate(first_movers,sk1(v,u)))*. % 0.45/0.75 95[3:SSi:93.1,93.0,16.0,15.0,16.0,15.0] || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5)) -> greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))*. % 0.45/0.75 96[0:Obv:94.0] stable(u) environment(u) || in_environment(u,v) greater_or_equal(sk1(v,u),sk4(u)) -> in_environment(u,sk2(u)) greater(growth_rate(efficient_producers,sk1(v,u)),growth_rate(first_movers,sk1(v,u)))*. % 0.45/0.75 97[0:MRR:96.5,7.2] stable(u) environment(u) || in_environment(u,v) greater_or_equal(sk1(v,u),sk4(u))* -> in_environment(u,sk2(u)). % 0.45/0.75 98[5:Spt:67.0] || -> equal(sk4(sk5),critical_point(sk5))**. % 0.45/0.75 99[5:Rew:98.0,34.0] || -> in_environment(sk5,critical_point(sk5))*. % 0.45/0.75 105[5:MRR:99.0,17.0] || -> . % 0.45/0.75 106[5:Spt:105.0,67.0,98.0] || equal(sk4(sk5),critical_point(sk5))** -> . % 0.45/0.75 107[5:Spt:105.0,67.1,67.2] || -> greater(sk3(sk4(sk5),sk5),sk4(sk5)) greater(growth_rate(efficient_producers,sk4(sk5)),growth_rate(first_movers,sk4(sk5)))*. % 0.45/0.75 113[3:Res:51.0,10.1] environment(sk5) || -> equal(critical_point(sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)). % 0.45/0.75 118[3:SSi:113.0,16.0,15.0] || -> equal(critical_point(sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)). % 0.45/0.75 119[4:MRR:118.0,86.0] || -> greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)). % 0.45/0.75 121[6:Spt:119.0] || -> greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 122[6:MRR:24.1,121.0] || in_environment(sk5,u) greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))* -> . % 0.45/0.75 123[6:MRR:95.2,122.1] || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5))* -> . % 0.45/0.75 126[6:Res:37.1,123.1] || in_environment(sk5,sk4(sk5))* in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 128[6:Obv:126.0] || in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 129[6:MRR:128.0,34.0] || -> . % 0.45/0.75 130[6:Spt:129.0,119.0,121.0] || greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* -> . % 0.45/0.75 131[6:Spt:129.0,119.1] || -> subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))*. % 0.45/0.75 132[6:MRR:87.1,130.0] || -> greater(sk3(sk2(sk5),sk5),sk2(sk5))*. % 0.45/0.75 139[0:Res:42.3,97.3] stable(u) environment(u) stable(u) environment(u) || in_environment(u,sk4(u))* -> in_environment(u,sk2(u)) in_environment(u,sk2(u)). % 0.45/0.75 141[0:Obv:139.5] stable(u) environment(u) || in_environment(u,sk4(u))* -> in_environment(u,sk2(u)). % 0.45/0.75 142[0:MRR:141.2,13.2] stable(u) environment(u) || -> in_environment(u,sk2(u))*. % 0.45/0.75 183[1:Res:36.2,22.1] || greater(sk3(u,sk5),sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,sk3(u,sk5)) in_environment(sk5,u) -> equal(u,critical_point(sk5)) greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 184[1:MRR:183.1,25.3] || greater(sk3(u,sk5),sk2(sk5)) in_environment(sk5,u) -> equal(u,critical_point(sk5)) greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 188[6:Res:184.3,130.0] || greater(sk3(sk2(sk5),sk5),sk2(sk5))* in_environment(sk5,sk2(sk5)) -> equal(critical_point(sk5),sk2(sk5)). % 0.45/0.75 193[6:MRR:188.0,188.1,188.2,132.0,51.0,86.0] || -> . % 0.45/0.75 194[3:Spt:193.0,31.1] || -> in_environment(sk5,sk2(sk5))*. % 0.45/0.75 195[3:Res:194.0,10.1] environment(sk5) || -> equal(critical_point(sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)). % 0.45/0.75 196[3:Res:194.0,11.1] environment(sk5) || -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 198[3:SSi:196.0,16.0,15.0] || -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 199[3:SSi:195.0,16.0,15.0] || -> equal(critical_point(sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)). % 0.45/0.75 200[4:Spt:67.0] || -> equal(sk4(sk5),critical_point(sk5))**. % 0.45/0.75 201[4:Rew:200.0,34.0] || -> in_environment(sk5,critical_point(sk5))*. % 0.45/0.75 209[4:MRR:201.0,17.0] || -> . % 0.45/0.75 210[4:Spt:209.0,67.0,200.0] || equal(sk4(sk5),critical_point(sk5))** -> . % 0.45/0.75 211[4:Spt:209.0,67.1,67.2] || -> greater(sk3(sk4(sk5),sk5),sk4(sk5)) greater(growth_rate(efficient_producers,sk4(sk5)),growth_rate(first_movers,sk4(sk5)))*. % 0.45/0.75 222[5:Spt:198.0] || -> equal(critical_point(sk5),sk2(sk5))**. % 0.45/0.75 223[5:Rew:222.0,17.0] || in_environment(sk5,sk2(sk5))* -> . % 0.45/0.75 248[5:MRR:223.0,194.0] || -> . % 0.45/0.75 252[5:Spt:248.0,198.0,222.0] || equal(critical_point(sk5),sk2(sk5))** -> . % 0.45/0.75 253[5:Spt:248.0,198.1,198.2] || -> greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 254[5:MRR:199.0,252.0] || -> greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)). % 0.45/0.75 255[6:Spt:253.0] || -> greater(sk3(sk2(sk5),sk5),sk2(sk5))*. % 0.45/0.75 256[7:Spt:254.0] || -> greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 257[7:MRR:27.1,256.0] || in_environment(sk5,u) -> subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))*. % 0.45/0.75 258[7:MRR:24.1,256.0] || in_environment(sk5,u) greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))* -> . % 0.45/0.75 262[7:Res:257.1,14.3] stable(sk5) environment(sk5) || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5)) -> greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))*. % 0.45/0.75 265[7:SSi:262.1,262.0,16.0,15.0,16.0,15.0] || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5)) -> greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))*. % 0.45/0.75 266[7:MRR:265.2,258.1] || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5))* -> . % 0.45/0.75 267[7:Res:37.1,266.1] || in_environment(sk5,sk4(sk5))* in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 268[7:Obv:267.0] || in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 269[7:MRR:268.0,34.0] || -> . % 0.45/0.75 270[7:Spt:269.0,254.0,256.0] || greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* -> . % 0.45/0.75 271[7:Spt:269.0,254.1] || -> subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))*. % 0.45/0.75 298[7:Res:184.3,270.0] || greater(sk3(sk2(sk5),sk5),sk2(sk5))* in_environment(sk5,sk2(sk5)) -> equal(critical_point(sk5),sk2(sk5)). % 0.45/0.75 302[7:MRR:298.0,298.1,298.2,255.0,194.0,252.0] || -> . % 0.45/0.75 303[6:Spt:302.0,253.0,255.0] || greater(sk3(sk2(sk5),sk5),sk2(sk5))* -> . % 0.45/0.75 304[6:Spt:302.0,253.1] || -> greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 305[6:MRR:27.1,304.0] || in_environment(sk5,u) -> subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))*. % 0.45/0.75 306[6:MRR:24.1,304.0] || in_environment(sk5,u) greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))* -> . % 0.45/0.75 315[6:Res:305.1,14.3] stable(sk5) environment(sk5) || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5)) -> greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))*. % 0.45/0.75 319[6:SSi:315.1,315.0,16.0,15.0,16.0,15.0] || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5)) -> greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))*. % 0.45/0.75 320[6:MRR:319.2,306.1] || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5))* -> . % 0.45/0.75 321[6:Res:37.1,320.1] || in_environment(sk5,sk4(sk5))* in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 322[6:Obv:321.0] || in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 323[6:MRR:322.0,34.0] || -> . % 0.45/0.75 324[2:Spt:323.0,32.1] || -> in_environment(sk5,sk2(sk5))*. % 0.45/0.75 326[2:Res:324.0,11.1] environment(sk5) || -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 328[2:SSi:326.0,16.0,15.0] || -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 330[1:Res:184.3,30.1] || greater(sk3(sk2(sk5),sk5),sk2(sk5))* in_environment(sk5,sk2(sk5)) in_environment(sk5,u) -> equal(critical_point(sk5),sk2(sk5)) greater_or_equal(sk1(u,sk5),u)*. % 0.45/0.75 332[0:Res:28.3,30.1] || in_environment(sk5,sk2(sk5)) in_environment(sk5,u) -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5))* greater_or_equal(sk1(u,sk5),u)*. % 0.45/0.75 335[2:MRR:332.0,324.0] || in_environment(sk5,u) -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5))* greater_or_equal(sk1(u,sk5),u)*. % 0.45/0.75 337[2:MRR:330.1,324.0] || greater(sk3(sk2(sk5),sk5),sk2(sk5))* in_environment(sk5,u) -> equal(critical_point(sk5),sk2(sk5)) greater_or_equal(sk1(u,sk5),u)*. % 0.45/0.75 338[2:MRR:337.0,335.2] || in_environment(sk5,u) -> equal(critical_point(sk5),sk2(sk5)) greater_or_equal(sk1(u,sk5),u)*. % 0.45/0.75 339[3:Spt:338.0,338.2] || in_environment(sk5,u) -> greater_or_equal(sk1(u,sk5),u)*. % 0.45/0.75 340[1:Res:184.3,27.1] || greater(sk3(sk2(sk5),sk5),sk2(sk5))* in_environment(sk5,sk2(sk5)) in_environment(sk5,u) -> equal(critical_point(sk5),sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))*. % 0.45/0.75 342[0:Res:28.3,27.1] || in_environment(sk5,sk2(sk5)) in_environment(sk5,u) -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5))* subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))*. % 0.45/0.75 345[2:MRR:342.0,324.0] || in_environment(sk5,u) -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5))* subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))*. % 0.45/0.75 347[2:MRR:340.1,324.0] || greater(sk3(sk2(sk5),sk5),sk2(sk5))* in_environment(sk5,u) -> equal(critical_point(sk5),sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))*. % 0.45/0.75 348[2:MRR:347.0,345.2] || in_environment(sk5,u) -> equal(critical_point(sk5),sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))*. % 0.45/0.75 349[4:Spt:348.0,348.2] || in_environment(sk5,u) -> subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))*. % 0.45/0.75 351[4:Res:349.1,14.3] stable(sk5) environment(sk5) || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5)) -> greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))*. % 0.45/0.75 355[4:SSi:351.1,351.0,16.0,15.0,16.0,15.0] || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5)) -> greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))*. % 0.45/0.75 356[5:Spt:67.0] || -> equal(sk4(sk5),critical_point(sk5))**. % 0.45/0.75 357[5:Rew:356.0,34.0] || -> in_environment(sk5,critical_point(sk5))*. % 0.45/0.75 373[5:MRR:357.0,17.0] || -> . % 0.45/0.75 374[5:Spt:373.0,67.0,356.0] || equal(sk4(sk5),critical_point(sk5))** -> . % 0.45/0.75 375[5:Spt:373.0,67.1,67.2] || -> greater(sk3(sk4(sk5),sk5),sk4(sk5)) greater(growth_rate(efficient_producers,sk4(sk5)),growth_rate(first_movers,sk4(sk5)))*. % 0.45/0.75 386[6:Spt:328.0] || -> equal(critical_point(sk5),sk2(sk5))**. % 0.45/0.75 387[6:Rew:386.0,17.0] || in_environment(sk5,sk2(sk5))* -> . % 0.45/0.75 420[6:MRR:387.0,324.0] || -> . % 0.45/0.75 424[6:Spt:420.0,328.0,386.0] || equal(critical_point(sk5),sk2(sk5))** -> . % 0.45/0.75 425[6:Spt:420.0,328.1,328.2] || -> greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 427[7:Spt:425.0] || -> greater(sk3(sk2(sk5),sk5),sk2(sk5))*. % 0.45/0.75 437[4:Res:355.2,8.3] environment(sk5) || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* -> . % 0.45/0.75 440[4:Obv:437.1] environment(sk5) || greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* -> . % 0.45/0.75 441[4:SSi:440.0,16.0,15.0] || greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*+ -> . % 0.45/0.75 473[0:Res:35.2,24.2] || greater_or_equal(sk1(u,sk5),sk4(sk5)) subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))* in_environment(sk5,u) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* -> . % 0.45/0.75 487[4:Res:184.3,441.2] || greater(sk3(sk2(sk5),sk5),sk2(sk5))* in_environment(sk5,sk2(sk5)) greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) -> equal(critical_point(sk5),sk2(sk5)). % 0.45/0.75 493[7:MRR:487.0,487.1,487.4,427.0,324.0,424.0] || greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) -> . % 0.45/0.75 502[7:Res:339.1,493.0] || in_environment(sk5,sk4(sk5))* in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 503[7:Obv:502.0] || in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 504[7:MRR:503.0,34.0] || -> . % 0.45/0.75 505[7:Spt:504.0,425.0,427.0] || greater(sk3(sk2(sk5),sk5),sk2(sk5))* -> . % 0.45/0.75 506[7:Spt:504.0,425.1] || -> greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 513[7:MRR:441.2,506.0] || greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) -> . % 0.45/0.75 516[7:Res:339.1,513.0] || in_environment(sk5,sk4(sk5))* in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 517[7:Obv:516.0] || in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 518[7:MRR:517.0,34.0] || -> . % 0.45/0.75 519[4:Spt:518.0,348.1] || -> equal(critical_point(sk5),sk2(sk5))**. % 0.45/0.75 520[4:Rew:519.0,17.0] || in_environment(sk5,sk2(sk5))* -> . % 0.45/0.75 554[4:MRR:520.0,324.0] || -> . % 0.45/0.75 559[0:MRR:473.1,27.2] || greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* -> . % 0.45/0.75 569[3:Spt:554.0,338.1] || -> equal(critical_point(sk5),sk2(sk5))**. % 0.45/0.75 570[3:Rew:569.0,17.0] || in_environment(sk5,sk2(sk5))* -> . % 0.45/0.75 571[3:MRR:570.0,324.0] || -> . % 0.45/0.75 613[1:Spt:571.0,23.1,23.3] || in_environment(sk5,u) -> greater_or_equal(sk1(u,sk5),u)*. % 0.45/0.75 617[2:Spt:21.1,21.4] || in_environment(sk5,u) -> subpopulations(first_movers,efficient_producers,sk5,sk1(u,sk5))*. % 0.45/0.75 618[2:Res:617.1,14.3] stable(sk5) environment(sk5) || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5)) -> greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))*. % 0.45/0.75 621[2:SSi:618.1,618.0,16.0,15.0,16.0,15.0] || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5)) -> greater(growth_rate(efficient_producers,sk1(u,sk5)),growth_rate(first_movers,sk1(u,sk5)))*. % 0.45/0.75 622[3:Spt:41.0] || -> in_environment(sk5,sk2(sk5))*. % 0.45/0.75 623[3:Res:622.0,10.1] environment(sk5) || -> equal(critical_point(sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)). % 0.45/0.75 624[3:Res:622.0,11.1] environment(sk5) || -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 626[3:SSi:624.0,16.0,15.0] || -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 627[3:SSi:623.0,16.0,15.0] || -> equal(critical_point(sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)). % 0.45/0.75 634[4:Spt:67.0] || -> equal(sk4(sk5),critical_point(sk5))**. % 0.45/0.75 635[4:Rew:634.0,34.0] || -> in_environment(sk5,critical_point(sk5))*. % 0.45/0.75 654[4:MRR:635.0,17.0] || -> . % 0.45/0.75 655[4:Spt:654.0,67.0,634.0] || equal(sk4(sk5),critical_point(sk5))** -> . % 0.45/0.75 656[4:Spt:654.0,67.1,67.2] || -> greater(sk3(sk4(sk5),sk5),sk4(sk5)) greater(growth_rate(efficient_producers,sk4(sk5)),growth_rate(first_movers,sk4(sk5)))*. % 0.45/0.75 667[5:Spt:626.0] || -> equal(critical_point(sk5),sk2(sk5))**. % 0.45/0.75 668[5:Rew:667.0,17.0] || in_environment(sk5,sk2(sk5))* -> . % 0.45/0.75 698[5:MRR:668.0,622.0] || -> . % 0.45/0.75 702[5:Spt:698.0,626.0,667.0] || equal(critical_point(sk5),sk2(sk5))** -> . % 0.45/0.75 703[5:Spt:698.0,626.1,626.2] || -> greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 704[5:MRR:627.0,702.0] || -> greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)). % 0.45/0.75 705[6:Spt:703.0] || -> greater(sk3(sk2(sk5),sk5),sk2(sk5))*. % 0.45/0.75 706[7:Spt:704.0] || -> greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 708[7:MRR:559.2,706.0] || greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) -> . % 0.45/0.75 714[7:Res:613.1,708.0] || in_environment(sk5,sk4(sk5))* in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 715[7:Obv:714.0] || in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 716[7:MRR:715.0,34.0] || -> . % 0.45/0.75 717[7:Spt:716.0,704.0,706.0] || greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* -> . % 0.45/0.75 718[7:Spt:716.0,704.1] || -> subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))*. % 0.45/0.75 732[2:Res:621.2,9.3] environment(sk5) || in_environment(sk5,u) greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) greater(v,sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,v) -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v))*. % 0.45/0.75 737[2:Obv:732.1] environment(sk5) || greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) greater(v,sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,v) -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v))*. % 0.45/0.75 738[2:SSi:737.0,16.0,15.0] || greater_or_equal(sk1(u,sk5),sk4(sk5))*+ in_environment(sk5,u) greater(v,sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,v) -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v))*. % 0.45/0.75 824[2:Res:613.1,738.0] || in_environment(sk5,sk4(sk5)) in_environment(sk5,sk4(sk5)) greater(u,sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 825[2:Obv:824.0] || in_environment(sk5,sk4(sk5)) greater(u,sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 826[2:MRR:825.0,34.0] || greater(u,sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 834[2:Res:826.2,22.1] || greater(sk3(u,sk5),sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,sk3(u,sk5)) in_environment(sk5,u) -> equal(u,critical_point(sk5)) greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 835[2:MRR:834.1,25.3] || greater(sk3(u,sk5),sk2(sk5)) in_environment(sk5,u) -> equal(u,critical_point(sk5)) greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 841[7:Res:835.3,717.0] || greater(sk3(sk2(sk5),sk5),sk2(sk5))* in_environment(sk5,sk2(sk5)) -> equal(critical_point(sk5),sk2(sk5)). % 0.45/0.75 847[7:MRR:841.0,841.1,841.2,705.0,622.0,702.0] || -> . % 0.45/0.75 848[6:Spt:847.0,703.0,705.0] || greater(sk3(sk2(sk5),sk5),sk2(sk5))* -> . % 0.45/0.75 849[6:Spt:847.0,703.1] || -> greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 850[6:MRR:559.2,849.0] || greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) -> . % 0.45/0.75 870[6:Res:613.1,850.0] || in_environment(sk5,sk4(sk5))* in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 873[6:Obv:870.0] || in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 874[6:MRR:873.0,34.0] || -> . % 0.45/0.75 875[3:Spt:874.0,41.0,622.0] || in_environment(sk5,sk2(sk5))* -> . % 0.45/0.75 876[3:Spt:874.0,41.1] || -> greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))*. % 0.45/0.75 879[3:Res:142.2,875.0] stable(sk5) environment(sk5) || -> . % 0.45/0.75 880[3:SSi:879.1,879.0,16.0,15.0,16.0,15.0] || -> . % 0.45/0.75 881[2:Spt:880.0,21.0,21.2,21.3] || greater(u,sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,u) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 888[2:Res:881.2,22.1] || greater(sk3(u,sk5),sk2(sk5)) subpopulations(first_movers,efficient_producers,sk5,sk3(u,sk5)) in_environment(sk5,u) -> equal(u,critical_point(sk5)) greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 889[2:MRR:888.1,25.3] || greater(sk3(u,sk5),sk2(sk5)) in_environment(sk5,u) -> equal(u,critical_point(sk5)) greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))*. % 0.45/0.75 897[3:Spt:41.0] || -> in_environment(sk5,sk2(sk5))*. % 0.45/0.75 901[3:Res:897.0,10.1] environment(sk5) || -> equal(critical_point(sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)). % 0.45/0.75 902[3:Res:897.0,11.1] environment(sk5) || -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 904[3:SSi:902.0,16.0,15.0] || -> equal(critical_point(sk5),sk2(sk5)) greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 905[3:SSi:901.0,16.0,15.0] || -> equal(critical_point(sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)). % 0.45/0.75 906[4:Spt:67.0] || -> equal(sk4(sk5),critical_point(sk5))**. % 0.45/0.75 907[4:Rew:906.0,34.0] || -> in_environment(sk5,critical_point(sk5))*. % 0.45/0.75 927[4:MRR:907.0,17.0] || -> . % 0.45/0.75 928[4:Spt:927.0,67.0,906.0] || equal(sk4(sk5),critical_point(sk5))** -> . % 0.45/0.75 929[4:Spt:927.0,67.1,67.2] || -> greater(sk3(sk4(sk5),sk5),sk4(sk5)) greater(growth_rate(efficient_producers,sk4(sk5)),growth_rate(first_movers,sk4(sk5)))*. % 0.45/0.75 943[5:Spt:904.0] || -> equal(critical_point(sk5),sk2(sk5))**. % 0.45/0.75 944[5:Rew:943.0,17.0] || in_environment(sk5,sk2(sk5))* -> . % 0.45/0.75 975[5:MRR:944.0,897.0] || -> . % 0.45/0.75 979[5:Spt:975.0,904.0,943.0] || equal(critical_point(sk5),sk2(sk5))** -> . % 0.45/0.75 980[5:Spt:975.0,904.1,904.2] || -> greater(sk3(sk2(sk5),sk5),sk2(sk5)) greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 981[5:MRR:905.0,979.0] || -> greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5)). % 0.45/0.75 982[6:Spt:980.0] || -> greater(sk3(sk2(sk5),sk5),sk2(sk5))*. % 0.45/0.75 983[7:Spt:981.0] || -> greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 985[7:MRR:559.2,983.0] || greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) -> . % 0.45/0.75 991[7:Res:613.1,985.0] || in_environment(sk5,sk4(sk5))* in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 992[7:Obv:991.0] || in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 993[7:MRR:992.0,34.0] || -> . % 0.45/0.75 994[7:Spt:993.0,981.0,983.0] || greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))* -> . % 0.45/0.75 995[7:Spt:993.0,981.1] || -> subpopulations(first_movers,efficient_producers,sk5,sk3(sk2(sk5),sk5))*. % 0.45/0.75 1035[7:Res:889.3,994.0] || greater(sk3(sk2(sk5),sk5),sk2(sk5))* in_environment(sk5,sk2(sk5)) -> equal(critical_point(sk5),sk2(sk5)). % 0.45/0.75 1040[7:MRR:1035.0,1035.1,1035.2,982.0,897.0,979.0] || -> . % 0.45/0.75 1041[6:Spt:1040.0,980.0,982.0] || greater(sk3(sk2(sk5),sk5),sk2(sk5))* -> . % 0.45/0.75 1042[6:Spt:1040.0,980.1] || -> greater(growth_rate(efficient_producers,sk2(sk5)),growth_rate(first_movers,sk2(sk5)))*. % 0.45/0.75 1043[6:MRR:559.2,1042.0] || greater_or_equal(sk1(u,sk5),sk4(sk5))* in_environment(sk5,u) -> . % 0.45/0.75 1056[6:Res:613.1,1043.0] || in_environment(sk5,sk4(sk5))* in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 1059[6:Obv:1056.0] || in_environment(sk5,sk4(sk5))* -> . % 0.45/0.75 1060[6:MRR:1059.0,34.0] || -> . % 0.45/0.75 1061[3:Spt:1060.0,41.0,897.0] || in_environment(sk5,sk2(sk5))* -> . % 0.45/0.75 1062[3:Spt:1060.0,41.1] || -> greater_or_equal(sk1(sk4(sk5),sk5),sk4(sk5))*. % 0.45/0.75 1065[3:Res:142.2,1061.0] stable(sk5) environment(sk5) || -> . % 0.45/0.76 1066[3:SSi:1065.1,1065.0,16.0,15.0,16.0,15.0] || -> . % 0.45/0.76 % SZS output end Refutation % 0.45/0.76 Formulae used in the proof : mp_earliest_time_growth_rate_exceeds_19 mp_earliest_time_growth_rate_exceeds_20 mp_earliest_time_growth_rate_exceeds_21 mp_earliest_time_growth_rate_exceeds_22 mp_earliest_time_growth_rate_exceeds_23 mp_earliest_time_growth_rate_exceeds_24 mp_earliest_time_growth_rate_exceeds_25 mp_earliest_time_growth_rate_exceeds_26 mp_earliest_time_growth_rate_exceeds_27 d1_28 d1_29 d1_30 l1_31 l1_32 prove_l5_33 prove_l5_34 prove_l5_35 % 0.45/0.76 %------------------------------------------------------------------------------