%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT029+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n017.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 : Theorem 0.40s 0.66s % Output : Refutation 0.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT029+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : run_spass %d %s % 0.08/0.35 % Computer : n017.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Mon Sep 7 12:11:09 UTC 2026 % 0.08/0.35 % CPUTime : % 0.40/0.66 % 0.40/0.66 SPASS V 3.9 % 0.40/0.66 SPASS beiseite: Proof found. % 0.40/0.66 % SZS status Theorem % 0.40/0.66 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.40/0.66 SPASS derived 1045 clauses, backtracked 321 clauses, performed 19 splits and kept 640 clauses. % 0.40/0.66 SPASS allocated 98500 KBytes. % 0.40/0.66 SPASS spent 0:00:00.30 on the problem. % 0.40/0.66 0:00:00.06 for the input. % 0.40/0.66 0:00:00.05 for the FLOTTER CNF translation. % 0.40/0.66 0:00:00.04 for inferences. % 0.40/0.66 0:00:00.00 for the backtracking. % 0.40/0.66 0:00:00.10 for the reduction. % 0.40/0.66 % 0.40/0.66 % 0.40/0.66 Here is a proof with depth 8, length 362 : % 0.40/0.66 % SZS output start Refutation % 0.40/0.66 1[0:Inp] || -> environment(skc1)*. % 0.40/0.66 2[0:Inp] || -> stable(skc1)*. % 0.40/0.66 3[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 0.40/0.66 4[0:Inp] || equal(u,v) -> greater_or_equal(u,v)*. % 0.40/0.66 5[0:Inp] || in_environment(skc1,u) -> greater_or_equal(skf3(u),u)*. % 0.40/0.66 6[0:Inp] SkP0(u) || -> equal(growth_rate(first_movers,u),zero)**. % 0.40/0.66 7[0:Inp] SkP0(u) || -> equal(growth_rate(efficient_producers,u),zero)**. % 0.40/0.66 8[0:Inp] SkP1(u) || -> greater(growth_rate(first_movers,u),zero)*l. % 0.40/0.66 9[0:Inp] SkP1(u) || -> greater(zero,growth_rate(efficient_producers,u))*r. % 0.40/0.66 10[0:Inp] || in_environment(skc1,u) -> subpopulations(first_movers,efficient_producers,skc1,skf3(u))*. % 0.40/0.66 11[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.40/0.66 12[0:Inp] stable(u) environment(u) || -> in_environment(u,skf5(u))*. % 0.40/0.66 13[0:Inp] stable(u) environment(u) || -> in_environment(u,skf6(u))*. % 0.40/0.66 14[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 0.40/0.66 15[0:Inp] stable(u) environment(u) || -> greater_or_equal(skf6(u),equilibrium(u))*. % 0.40/0.66 16[0:Inp] || greater(zero,growth_rate(first_movers,skf3(u))) greater(growth_rate(efficient_producers,skf3(u)),zero)*l -> . % 0.40/0.66 17[0:Inp] || in_environment(u,v)*+ in_environment(u,w)* -> greater(v,w)* equal(v,w) greater(w,v)*. % 0.40/0.66 18[0:Inp] environment(u) || greater_or_equal(v,equilibrium(u)) subpopulations(first_movers,efficient_producers,u,v)* -> SkP0(v) SkP1(v) greater(zero,growth_rate(first_movers,v)). % 0.40/0.66 19[0:Inp] environment(u) || greater_or_equal(v,equilibrium(u)) subpopulations(first_movers,efficient_producers,u,v)* -> SkP0(v) SkP1(v) greater(growth_rate(efficient_producers,v),zero). % 0.40/0.66 20[0:Inp] stable(u) environment(u) || greater_or_equal(v,skf5(u)) subpopulations(first_movers,efficient_producers,u,v)* -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v)). % 0.40/0.66 22[0:Res:2.0,15.1] environment(skc1) || -> greater_or_equal(skf6(skc1),equilibrium(skc1))*. % 0.40/0.66 23[0:Res:2.0,12.1] environment(skc1) || -> in_environment(skc1,skf5(skc1))*. % 0.40/0.66 24[0:Res:2.0,13.1] environment(skc1) || -> in_environment(skc1,skf6(skc1))*. % 0.40/0.66 25[0:Res:1.0,20.0] stable(skc1) || subpopulations(first_movers,efficient_producers,skc1,u)* greater_or_equal(u,skf5(skc1)) -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u)). % 0.40/0.66 31[0:MRR:23.0,1.0] || -> in_environment(skc1,skf5(skc1))*. % 0.40/0.66 32[0:MRR:24.0,1.0] || -> in_environment(skc1,skf6(skc1))*. % 0.40/0.66 33[0:MRR:22.0,1.0] || -> greater_or_equal(skf6(skc1),equilibrium(skc1))*. % 0.40/0.66 34[0:MRR:25.0,2.0] || greater_or_equal(u,skf5(skc1)) subpopulations(first_movers,efficient_producers,skc1,u)* -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u)). % 0.40/0.66 45[0:Res:33.0,11.0] || -> equal(skf6(skc1),equilibrium(skc1)) greater(skf6(skc1),equilibrium(skc1))*l. % 0.40/0.66 46[0:Res:15.2,11.0] stable(u) environment(u) || -> equal(skf6(u),equilibrium(u)) greater(skf6(u),equilibrium(u))*l. % 0.40/0.66 47[0:Res:5.1,11.0] || in_environment(skc1,u)* -> equal(skf3(u),u) greater(skf3(u),u). % 0.40/0.66 48[1:Spt:45.0] || -> equal(skf6(skc1),equilibrium(skc1))**. % 0.40/0.66 49[1:Rew:48.0,32.0] || -> in_environment(skc1,equilibrium(skc1))*. % 0.40/0.66 54[0:SpL:7.1,16.1] SkP0(skf3(u)) || greater(zero,growth_rate(first_movers,skf3(u)))*r greater(zero,zero) -> . % 0.40/0.66 55[0:Rew:6.1,54.1] SkP0(skf3(u)) || greater(zero,zero)* greater(zero,zero)* -> . % 0.40/0.66 56[0:Obv:55.1] SkP0(skf3(u)) || greater(zero,zero)* -> . % 0.40/0.66 58[0:Res:31.0,47.0] || -> equal(skf3(skf5(skc1)),skf5(skc1)) greater(skf3(skf5(skc1)),skf5(skc1))*l. % 0.40/0.66 59[1:Res:49.0,47.0] || -> equal(skf3(equilibrium(skc1)),equilibrium(skc1)) greater(skf3(equilibrium(skc1)),equilibrium(skc1))*l. % 0.40/0.66 60[0:Res:13.2,47.0] stable(skc1) environment(skc1) || -> equal(skf3(skf6(skc1)),skf6(skc1)) greater(skf3(skf6(skc1)),skf6(skc1))*l. % 0.40/0.66 63[0:Res:31.0,17.0] || in_environment(skc1,u)* -> greater(skf5(skc1),u) equal(skf5(skc1),u) greater(u,skf5(skc1)). % 0.40/0.66 64[1:Res:49.0,17.0] || in_environment(skc1,u)* -> greater(equilibrium(skc1),u) equal(equilibrium(skc1),u) greater(u,equilibrium(skc1)). % 0.40/0.66 68[0:Res:10.1,34.1] || in_environment(skc1,u) greater_or_equal(skf3(u),skf5(skc1))* -> greater(growth_rate(efficient_producers,skf3(u)),growth_rate(first_movers,skf3(u))). % 0.40/0.66 69[0:Res:10.1,19.2] environment(skc1) || in_environment(skc1,u) greater_or_equal(skf3(u),equilibrium(skc1))* -> SkP0(skf3(u)) SkP1(skf3(u)) greater(growth_rate(efficient_producers,skf3(u)),zero). % 0.40/0.66 70[0:SSi:69.0,2.0,1.0] || in_environment(skc1,u) greater_or_equal(skf3(u),equilibrium(skc1))* -> SkP0(skf3(u)) SkP1(skf3(u)) greater(growth_rate(efficient_producers,skf3(u)),zero). % 0.40/0.66 71[0:Res:3.1,68.1] || greater(skf3(u),skf5(skc1)) in_environment(skc1,u) -> greater(growth_rate(efficient_producers,skf3(u)),growth_rate(first_movers,skf3(u)))*l. % 0.40/0.66 72[0:Res:4.1,68.1] || equal(skf3(u),skf5(skc1)) in_environment(skc1,u) -> greater(growth_rate(efficient_producers,skf3(u)),growth_rate(first_movers,skf3(u)))*l. % 0.40/0.66 73[0:Res:5.1,68.1] || in_environment(skc1,skf5(skc1)) in_environment(skc1,skf5(skc1)) -> greater(growth_rate(efficient_producers,skf3(skf5(skc1))),growth_rate(first_movers,skf3(skf5(skc1))))*l. % 0.40/0.66 74[0:Obv:73.0] || in_environment(skc1,skf5(skc1)) -> greater(growth_rate(efficient_producers,skf3(skf5(skc1))),growth_rate(first_movers,skf3(skf5(skc1))))*l. % 0.40/0.66 75[0:MRR:74.0,31.0] || -> greater(growth_rate(efficient_producers,skf3(skf5(skc1))),growth_rate(first_movers,skf3(skf5(skc1))))*l. % 0.40/0.66 76[0:SpR:7.1,75.0] SkP0(skf3(skf5(skc1))) || -> greater(zero,growth_rate(first_movers,skf3(skf5(skc1))))*r. % 0.40/0.66 77[0:OCh:14.1,14.0,75.0,9.1] SkP1(skf3(skf5(skc1))) || -> greater(zero,growth_rate(first_movers,skf3(skf5(skc1))))*r. % 0.40/0.66 78[0:NCh:14.2,14.0,75.0,16.1] || greater(zero,growth_rate(first_movers,skf3(skf5(skc1)))) greater(growth_rate(first_movers,skf3(skf5(skc1))),zero)*l -> . % 0.40/0.66 79[0:NCh:14.2,14.0,75.0,16.1] || greater(zero,growth_rate(first_movers,skf3(skf5(skc1))))*r equal(growth_rate(first_movers,skf3(skf5(skc1))),zero) -> . % 0.40/0.66 80[0:Rew:6.1,76.1] SkP0(skf3(skf5(skc1))) || -> greater(zero,zero)*. % 0.40/0.66 81[0:MRR:80.1,56.1] SkP0(skf3(skf5(skc1))) || -> . % 0.40/0.66 82[0:Res:10.1,18.2] environment(skc1) || in_environment(skc1,u) greater_or_equal(skf3(u),equilibrium(skc1))* -> SkP0(skf3(u)) SkP1(skf3(u)) greater(zero,growth_rate(first_movers,skf3(u))). % 0.40/0.66 83[0:SSi:82.0,2.0,1.0] || in_environment(skc1,u) greater_or_equal(skf3(u),equilibrium(skc1))* -> SkP0(skf3(u)) SkP1(skf3(u)) greater(zero,growth_rate(first_movers,skf3(u))). % 0.40/0.66 85[0:SpR:7.1,72.2] SkP0(skf3(u)) || equal(skf3(u),skf5(skc1)) in_environment(skc1,u) -> greater(zero,growth_rate(first_movers,skf3(u)))*r. % 0.40/0.66 86[0:OCh:14.1,14.0,72.2,9.1] SkP1(skf3(u)) || equal(skf3(u),skf5(skc1)) in_environment(skc1,u) -> greater(zero,growth_rate(first_movers,skf3(u)))*r. % 0.40/0.66 87[0:NCh:14.2,14.0,72.2,16.1] || equal(skf3(u),skf5(skc1)) in_environment(skc1,u) greater(zero,growth_rate(first_movers,skf3(u))) greater(growth_rate(first_movers,skf3(u)),zero)*l -> . % 0.40/0.66 89[0:Rew:6.1,85.3] SkP0(skf3(u)) || equal(skf3(u),skf5(skc1)) in_environment(skc1,u)* -> greater(zero,zero). % 0.40/0.66 90[0:MRR:89.3,56.1] SkP0(skf3(u)) || equal(skf3(u),skf5(skc1)) in_environment(skc1,u)* -> . % 0.40/0.66 95[0:Res:8.1,78.1] SkP1(skf3(skf5(skc1))) || greater(zero,growth_rate(first_movers,skf3(skf5(skc1))))*r -> . % 0.40/0.66 98[0:MRR:95.1,77.1] SkP1(skf3(skf5(skc1))) || -> . % 0.40/0.66 100[0:Res:3.1,70.1] || greater(skf3(u),equilibrium(skc1)) in_environment(skc1,u) -> SkP0(skf3(u)) SkP1(skf3(u)) greater(growth_rate(efficient_producers,skf3(u)),zero)*l. % 0.40/0.66 101[0:Res:4.1,70.1] || equal(skf3(u),equilibrium(skc1)) in_environment(skc1,u) -> SkP0(skf3(u)) SkP1(skf3(u)) greater(growth_rate(efficient_producers,skf3(u)),zero)*l. % 0.40/0.66 102[0:Res:5.1,70.1] || in_environment(skc1,equilibrium(skc1)) in_environment(skc1,equilibrium(skc1)) -> SkP0(skf3(equilibrium(skc1))) SkP1(skf3(equilibrium(skc1))) greater(growth_rate(efficient_producers,skf3(equilibrium(skc1))),zero)*l. % 0.40/0.66 103[0:Obv:102.0] || in_environment(skc1,equilibrium(skc1)) -> SkP0(skf3(equilibrium(skc1))) SkP1(skf3(equilibrium(skc1))) greater(growth_rate(efficient_producers,skf3(equilibrium(skc1))),zero)*l. % 0.40/0.66 104[1:MRR:103.0,49.0] || -> SkP0(skf3(equilibrium(skc1))) SkP1(skf3(equilibrium(skc1))) greater(growth_rate(efficient_producers,skf3(equilibrium(skc1))),zero)*l. % 0.40/0.66 106[1:Res:104.2,16.1] || greater(zero,growth_rate(first_movers,skf3(equilibrium(skc1))))*r -> SkP0(skf3(equilibrium(skc1))) SkP1(skf3(equilibrium(skc1))). % 0.40/0.66 111[2:Spt:106.1] || -> SkP0(skf3(equilibrium(skc1)))*. % 0.40/0.66 113[2:SoR:56.0,111.0] || greater(zero,zero)* -> . % 0.40/0.66 116[0:Res:3.1,83.1] || greater(skf3(u),equilibrium(skc1)) in_environment(skc1,u) -> SkP0(skf3(u)) SkP1(skf3(u)) greater(zero,growth_rate(first_movers,skf3(u)))*r. % 0.40/0.66 117[0:Res:4.1,83.1] || equal(skf3(u),equilibrium(skc1)) in_environment(skc1,u) -> SkP0(skf3(u)) SkP1(skf3(u)) greater(zero,growth_rate(first_movers,skf3(u)))*r. % 0.40/0.66 118[0:Res:5.1,83.1] || in_environment(skc1,equilibrium(skc1)) in_environment(skc1,equilibrium(skc1)) -> SkP0(skf3(equilibrium(skc1))) SkP1(skf3(equilibrium(skc1))) greater(zero,growth_rate(first_movers,skf3(equilibrium(skc1))))*r. % 0.40/0.66 119[0:Obv:118.0] || in_environment(skc1,equilibrium(skc1)) -> SkP0(skf3(equilibrium(skc1))) SkP1(skf3(equilibrium(skc1))) greater(zero,growth_rate(first_movers,skf3(equilibrium(skc1))))*r. % 0.40/0.66 120[1:Res:31.0,64.0] || -> greater(equilibrium(skc1),skf5(skc1)) equal(skf5(skc1),equilibrium(skc1)) greater(skf5(skc1),equilibrium(skc1))*l. % 0.40/0.66 124[3:Spt:120.1] || -> equal(skf5(skc1),equilibrium(skc1))**. % 0.40/0.66 128[3:Rew:124.0,75.0] || -> greater(growth_rate(efficient_producers,skf3(equilibrium(skc1))),growth_rate(first_movers,skf3(equilibrium(skc1))))*l. % 0.40/0.66 154[3:SpR:7.1,128.0] SkP0(skf3(equilibrium(skc1))) || -> greater(zero,growth_rate(first_movers,skf3(equilibrium(skc1))))*r. % 0.40/0.66 158[3:Rew:6.1,154.1] SkP0(skf3(equilibrium(skc1))) || -> greater(zero,zero)*. % 0.40/0.66 159[3:SSi:158.0,111.0] || -> greater(zero,zero)*. % 0.40/0.66 160[3:MRR:159.0,113.0] || -> . % 0.40/0.66 161[3:Spt:160.0,120.1,124.0] || equal(skf5(skc1),equilibrium(skc1))** -> . % 0.40/0.66 162[3:Spt:160.0,120.0,120.2] || -> greater(equilibrium(skc1),skf5(skc1)) greater(skf5(skc1),equilibrium(skc1))*l. % 0.40/0.66 171[4:Spt:58.0] || -> equal(skf3(skf5(skc1)),skf5(skc1))**. % 0.40/0.66 172[4:Rew:171.0,75.0] || -> greater(growth_rate(efficient_producers,skf5(skc1)),growth_rate(first_movers,skf5(skc1)))*l. % 0.40/0.66 173[4:Rew:171.0,78.0] || greater(zero,growth_rate(first_movers,skf5(skc1))) greater(growth_rate(first_movers,skf3(skf5(skc1))),zero)*l -> . % 0.40/0.66 176[4:Rew:171.0,173.1] || greater(zero,growth_rate(first_movers,skf5(skc1))) greater(growth_rate(first_movers,skf5(skc1)),zero)*l -> . % 0.40/0.66 180[4:SpL:171.0,16.1] || greater(zero,growth_rate(first_movers,skf3(skf5(skc1))))*r greater(growth_rate(efficient_producers,skf5(skc1)),zero) -> . % 0.40/0.66 181[4:SpL:171.0,83.1] || in_environment(skc1,skf5(skc1)) greater_or_equal(skf5(skc1),equilibrium(skc1)) -> SkP0(skf3(skf5(skc1))) SkP1(skf3(skf5(skc1))) greater(zero,growth_rate(first_movers,skf3(skf5(skc1))))*r. % 0.40/0.66 182[4:SpL:171.0,70.1] || in_environment(skc1,skf5(skc1)) greater_or_equal(skf5(skc1),equilibrium(skc1)) -> SkP0(skf3(skf5(skc1))) SkP1(skf3(skf5(skc1))) greater(growth_rate(efficient_producers,skf3(skf5(skc1))),zero)*l. % 0.40/0.66 185[4:Rew:171.0,180.0] || greater(zero,growth_rate(first_movers,skf5(skc1))) greater(growth_rate(efficient_producers,skf5(skc1)),zero)*l -> . % 0.40/0.66 186[4:Rew:171.0,182.4,171.0,182.3,171.0,182.2] || in_environment(skc1,skf5(skc1)) greater_or_equal(skf5(skc1),equilibrium(skc1))* -> SkP0(skf5(skc1)) SkP1(skf5(skc1)) greater(growth_rate(efficient_producers,skf5(skc1)),zero). % 0.40/0.66 187[4:MRR:186.0,31.0] || greater_or_equal(skf5(skc1),equilibrium(skc1))* -> SkP0(skf5(skc1)) SkP1(skf5(skc1)) greater(growth_rate(efficient_producers,skf5(skc1)),zero). % 0.40/0.66 188[4:Rew:171.0,181.4,171.0,181.3,171.0,181.2] || in_environment(skc1,skf5(skc1)) greater_or_equal(skf5(skc1),equilibrium(skc1))* -> SkP0(skf5(skc1)) SkP1(skf5(skc1)) greater(zero,growth_rate(first_movers,skf5(skc1))). % 0.40/0.66 189[4:MRR:188.0,31.0] || greater_or_equal(skf5(skc1),equilibrium(skc1))* -> SkP0(skf5(skc1)) SkP1(skf5(skc1)) greater(zero,growth_rate(first_movers,skf5(skc1))). % 0.40/0.66 198[4:SpR:7.1,172.0] SkP0(skf5(skc1)) || -> greater(zero,growth_rate(first_movers,skf5(skc1)))*r. % 0.40/0.66 199[4:OCh:14.1,14.0,172.0,9.1] SkP1(skf5(skc1)) || -> greater(zero,growth_rate(first_movers,skf5(skc1)))*r. % 0.40/0.66 200[4:Rew:6.1,198.1] SkP0(skf5(skc1)) || -> greater(zero,zero)*. % 0.40/0.66 201[4:MRR:200.1,113.0] SkP0(skf5(skc1)) || -> . % 0.40/0.66 202[4:MRR:187.1,201.0] || greater_or_equal(skf5(skc1),equilibrium(skc1))* -> SkP1(skf5(skc1)) greater(growth_rate(efficient_producers,skf5(skc1)),zero). % 0.40/0.66 203[4:MRR:189.1,201.0] || greater_or_equal(skf5(skc1),equilibrium(skc1))* -> SkP1(skf5(skc1)) greater(zero,growth_rate(first_movers,skf5(skc1))). % 0.40/0.66 204[4:MRR:203.1,199.0] || greater_or_equal(skf5(skc1),equilibrium(skc1))* -> greater(zero,growth_rate(first_movers,skf5(skc1))). % 0.40/0.66 210[5:Spt:59.0] || -> equal(skf3(equilibrium(skc1)),equilibrium(skc1))**. % 0.40/0.66 211[5:Rew:210.0,111.0] || -> SkP0(equilibrium(skc1))*. % 0.40/0.66 214[5:SpR:210.0,10.1] || in_environment(skc1,equilibrium(skc1)) -> subpopulations(first_movers,efficient_producers,skc1,equilibrium(skc1))*. % 0.40/0.66 219[5:MRR:214.0,49.0] || -> subpopulations(first_movers,efficient_producers,skc1,equilibrium(skc1))*. % 0.40/0.66 223[5:Res:219.0,34.1] || greater_or_equal(equilibrium(skc1),skf5(skc1))* -> greater(growth_rate(efficient_producers,equilibrium(skc1)),growth_rate(first_movers,equilibrium(skc1))). % 0.40/0.66 234[4:Res:3.1,204.0] || greater(skf5(skc1),equilibrium(skc1)) -> greater(zero,growth_rate(first_movers,skf5(skc1)))*r. % 0.40/0.66 237[6:Spt:202.1] || -> SkP1(skf5(skc1))*. % 0.40/0.66 238[6:MRR:199.0,237.0] || -> greater(zero,growth_rate(first_movers,skf5(skc1)))*r. % 0.40/0.66 254[6:OCh:14.1,14.0,238.0,8.1] SkP1(skf5(skc1)) || -> greater(zero,zero)*. % 0.40/0.66 255[6:SSi:254.0,237.0] || -> greater(zero,zero)*. % 0.40/0.66 256[6:MRR:255.0,113.0] || -> . % 0.40/0.66 257[6:Spt:256.0,202.1,237.0] || SkP1(skf5(skc1))* -> . % 0.40/0.66 258[6:Spt:256.0,202.0,202.2] || greater_or_equal(skf5(skc1),equilibrium(skc1))* -> greater(growth_rate(efficient_producers,skf5(skc1)),zero). % 0.40/0.66 259[6:Res:3.1,258.0] || greater(skf5(skc1),equilibrium(skc1)) -> greater(growth_rate(efficient_producers,skf5(skc1)),zero)*l. % 0.40/0.66 268[5:Res:3.1,223.0] || greater(equilibrium(skc1),skf5(skc1)) -> greater(growth_rate(efficient_producers,equilibrium(skc1)),growth_rate(first_movers,equilibrium(skc1)))*l. % 0.40/0.66 280[0:Res:101.4,16.1] || equal(skf3(u),equilibrium(skc1)) in_environment(skc1,u) greater(zero,growth_rate(first_movers,skf3(u)))*r -> SkP0(skf3(u)) SkP1(skf3(u)). % 0.40/0.66 284[0:MRR:280.2,117.4] || equal(skf3(u),equilibrium(skc1)) in_environment(skc1,u) -> SkP0(skf3(u))* SkP1(skf3(u)). % 0.40/0.66 287[0:SoR:81.0,284.2] || in_environment(skc1,skf5(skc1)) equal(skf3(skf5(skc1)),equilibrium(skc1)) -> SkP1(skf3(skf5(skc1)))*. % 0.40/0.66 312[4:Res:8.1,176.1] SkP1(skf5(skc1)) || greater(zero,growth_rate(first_movers,skf5(skc1)))*r -> . % 0.40/0.66 315[4:MRR:312.1,199.1] SkP1(skf5(skc1)) || -> . % 0.40/0.66 318[6:Res:259.1,185.1] || greater(skf5(skc1),equilibrium(skc1)) greater(zero,growth_rate(first_movers,skf5(skc1)))*r -> . % 0.40/0.66 323[6:MRR:318.1,234.1] || greater(skf5(skc1),equilibrium(skc1))*l -> . % 0.40/0.66 324[6:MRR:162.1,323.0] || -> greater(equilibrium(skc1),skf5(skc1))*r. % 0.40/0.66 325[6:MRR:268.0,324.0] || -> greater(growth_rate(efficient_producers,equilibrium(skc1)),growth_rate(first_movers,equilibrium(skc1)))*l. % 0.40/0.66 330[0:Res:100.4,16.1] || greater(skf3(u),equilibrium(skc1)) in_environment(skc1,u) greater(zero,growth_rate(first_movers,skf3(u)))*r -> SkP0(skf3(u)) SkP1(skf3(u)). % 0.40/0.66 334[0:MRR:330.2,116.4] || greater(skf3(u),equilibrium(skc1)) in_environment(skc1,u) -> SkP0(skf3(u))* SkP1(skf3(u)). % 0.40/0.66 336[6:SpR:7.1,325.0] SkP0(equilibrium(skc1)) || -> greater(zero,growth_rate(first_movers,equilibrium(skc1)))*r. % 0.40/0.66 340[6:Rew:6.1,336.1] SkP0(equilibrium(skc1)) || -> greater(zero,zero)*. % 0.40/0.66 341[6:SSi:340.0,211.0] || -> greater(zero,zero)*. % 0.40/0.66 342[6:MRR:341.0,113.0] || -> . % 0.40/0.66 343[5:Spt:342.0,59.0,210.0] || equal(skf3(equilibrium(skc1)),equilibrium(skc1))** -> . % 0.40/0.66 344[5:Spt:342.0,59.1] || -> greater(skf3(equilibrium(skc1)),equilibrium(skc1))*l. % 0.40/0.66 345[4:MRR:202.1,315.0] || greater_or_equal(skf5(skc1),equilibrium(skc1))* -> greater(growth_rate(efficient_producers,skf5(skc1)),zero). % 0.40/0.66 348[4:Res:3.1,345.0] || greater(skf5(skc1),equilibrium(skc1)) -> greater(growth_rate(efficient_producers,skf5(skc1)),zero)*l. % 0.40/0.66 352[6:Spt:162.1] || -> greater(skf5(skc1),equilibrium(skc1))*l. % 0.40/0.66 354[6:MRR:234.0,352.0] || -> greater(zero,growth_rate(first_movers,skf5(skc1)))*r. % 0.40/0.66 355[6:MRR:348.0,352.0] || -> greater(growth_rate(efficient_producers,skf5(skc1)),zero)*l. % 0.40/0.66 357[6:MRR:185.0,354.0] || greater(growth_rate(efficient_producers,skf5(skc1)),zero)*l -> . % 0.40/0.66 358[6:MRR:357.0,355.0] || -> . % 0.40/0.66 359[6:Spt:358.0,162.1,352.0] || greater(skf5(skc1),equilibrium(skc1))*l -> . % 0.40/0.66 360[6:Spt:358.0,162.0] || -> greater(equilibrium(skc1),skf5(skc1))*r. % 0.40/0.66 367[0:SoR:90.0,334.2] || equal(skf3(u),skf5(skc1)) in_environment(skc1,u) in_environment(skc1,u) greater(skf3(u),equilibrium(skc1)) -> SkP1(skf3(u))*. % 0.40/0.66 368[0:SoR:81.0,334.2] || in_environment(skc1,skf5(skc1)) greater(skf3(skf5(skc1)),equilibrium(skc1)) -> SkP1(skf3(skf5(skc1)))*. % 0.40/0.66 372[0:Obv:367.1] || equal(skf3(u),skf5(skc1)) in_environment(skc1,u) greater(skf3(u),equilibrium(skc1)) -> SkP1(skf3(u))*. % 0.40/0.66 403[0:SpR:7.1,71.2] SkP0(skf3(u)) || greater(skf3(u),skf5(skc1)) in_environment(skc1,u) -> greater(zero,growth_rate(first_movers,skf3(u)))*r. % 0.40/0.66 404[0:OCh:14.1,14.0,71.2,9.1] SkP1(skf3(u)) || greater(skf3(u),skf5(skc1)) in_environment(skc1,u) -> greater(zero,growth_rate(first_movers,skf3(u)))*r. % 0.40/0.66 405[0:NCh:14.2,14.0,71.2,16.1] || greater(skf3(u),skf5(skc1)) in_environment(skc1,u) greater(zero,growth_rate(first_movers,skf3(u))) greater(growth_rate(first_movers,skf3(u)),zero)*l -> . % 0.40/0.66 407[0:Rew:6.1,403.3] SkP0(skf3(u)) || greater(skf3(u),skf5(skc1)) in_environment(skc1,u)* -> greater(zero,zero). % 0.40/0.66 408[2:MRR:407.3,113.0] SkP0(skf3(u)) || greater(skf3(u),skf5(skc1)) in_environment(skc1,u)* -> . % 0.40/0.66 409[2:SoR:408.0,111.0] || greater(skf3(equilibrium(skc1)),skf5(skc1)) in_environment(skc1,equilibrium(skc1))* -> . % 0.40/0.66 412[2:MRR:409.1,49.0] || greater(skf3(equilibrium(skc1)),skf5(skc1))*l -> . % 0.40/0.66 415[5:NCh:14.2,14.0,412.0,344.0] || greater(equilibrium(skc1),skf5(skc1))*r -> . % 0.40/0.66 417[6:MRR:415.0,360.0] || -> . % 0.40/0.66 418[4:Spt:417.0,58.0,171.0] || equal(skf3(skf5(skc1)),skf5(skc1))** -> . % 0.40/0.66 419[4:Spt:417.0,58.1] || -> greater(skf3(skf5(skc1)),skf5(skc1))*l. % 0.40/0.66 420[0:MRR:287.0,287.2,31.0,98.0] || equal(skf3(skf5(skc1)),equilibrium(skc1))** -> . % 0.40/0.66 421[0:MRR:368.0,368.2,31.0,98.0] || greater(skf3(skf5(skc1)),equilibrium(skc1))*l -> . % 0.40/0.66 423[5:Spt:59.0] || -> equal(skf3(equilibrium(skc1)),equilibrium(skc1))**. % 0.40/0.66 426[5:Rew:423.0,412.0] || greater(equilibrium(skc1),skf5(skc1))*r -> . % 0.40/0.66 427[5:MRR:162.0,426.0] || -> greater(skf5(skc1),equilibrium(skc1))*l. % 0.40/0.66 462[4:NCh:14.2,14.0,421.0,419.0] || greater(skf5(skc1),equilibrium(skc1))*l -> . % 0.40/0.66 464[5:MRR:462.0,427.0] || -> . % 0.40/0.66 465[5:Spt:464.0,59.0,423.0] || equal(skf3(equilibrium(skc1)),equilibrium(skc1))** -> . % 0.40/0.66 466[5:Spt:464.0,59.1] || -> greater(skf3(equilibrium(skc1)),equilibrium(skc1))*l. % 0.40/0.66 467[4:MRR:162.1,462.0] || -> greater(equilibrium(skc1),skf5(skc1))*r. % 0.40/0.66 472[5:NCh:14.2,14.0,412.0,466.0] || greater(equilibrium(skc1),skf5(skc1))*r -> . % 0.40/0.66 474[5:MRR:472.0,467.0] || -> . % 0.40/0.66 475[2:Spt:474.0,106.1,111.0] || SkP0(skf3(equilibrium(skc1)))* -> . % 0.40/0.66 476[2:Spt:474.0,106.0,106.2] || greater(zero,growth_rate(first_movers,skf3(equilibrium(skc1))))*r -> SkP1(skf3(equilibrium(skc1))). % 0.40/0.66 478[1:MRR:119.0,49.0] || -> SkP0(skf3(equilibrium(skc1))) SkP1(skf3(equilibrium(skc1))) greater(zero,growth_rate(first_movers,skf3(equilibrium(skc1))))*r. % 0.40/0.66 479[2:MRR:478.0,478.2,475.0,476.0] || -> SkP1(skf3(equilibrium(skc1)))*. % 0.40/0.66 480[0:MRR:407.3,56.1] SkP0(skf3(u)) || greater(skf3(u),skf5(skc1)) in_environment(skc1,u)* -> . % 0.40/0.66 497[3:Spt:59.0] || -> equal(skf3(equilibrium(skc1)),equilibrium(skc1))**. % 0.40/0.66 498[3:Rew:497.0,479.0] || -> SkP1(equilibrium(skc1))*. % 0.40/0.66 504[3:SpR:497.0,71.2] || greater(skf3(equilibrium(skc1)),skf5(skc1)) in_environment(skc1,equilibrium(skc1)) -> greater(growth_rate(efficient_producers,equilibrium(skc1)),growth_rate(first_movers,equilibrium(skc1)))*l. % 0.40/0.66 511[3:SpL:497.0,16.1] || greater(zero,growth_rate(first_movers,skf3(equilibrium(skc1))))*r greater(growth_rate(efficient_producers,equilibrium(skc1)),zero) -> . % 0.40/0.66 519[3:Rew:497.0,511.0] || greater(zero,growth_rate(first_movers,equilibrium(skc1))) greater(growth_rate(efficient_producers,equilibrium(skc1)),zero)*l -> . % 0.40/0.66 526[3:Rew:497.0,504.0] || greater(equilibrium(skc1),skf5(skc1)) in_environment(skc1,equilibrium(skc1)) -> greater(growth_rate(efficient_producers,equilibrium(skc1)),growth_rate(first_movers,equilibrium(skc1)))*l. % 0.40/0.66 527[3:MRR:526.1,49.0] || greater(equilibrium(skc1),skf5(skc1)) -> greater(growth_rate(efficient_producers,equilibrium(skc1)),growth_rate(first_movers,equilibrium(skc1)))*l. % 0.40/0.66 528[4:Spt:58.0] || -> equal(skf3(skf5(skc1)),skf5(skc1))**. % 0.40/0.66 529[4:Rew:528.0,420.0] || equal(skf5(skc1),equilibrium(skc1))** -> . % 0.40/0.66 531[4:Rew:528.0,421.0] || greater(skf5(skc1),equilibrium(skc1))*l -> . % 0.40/0.66 534[4:MRR:120.1,529.0] || -> greater(equilibrium(skc1),skf5(skc1)) greater(skf5(skc1),equilibrium(skc1))*l. % 0.40/0.66 536[4:MRR:534.1,531.0] || -> greater(equilibrium(skc1),skf5(skc1))*r. % 0.40/0.66 537[4:MRR:527.0,536.0] || -> greater(growth_rate(efficient_producers,equilibrium(skc1)),growth_rate(first_movers,equilibrium(skc1)))*l. % 0.40/0.66 584[4:OCh:14.1,14.0,537.0,9.1] SkP1(equilibrium(skc1)) || -> greater(zero,growth_rate(first_movers,equilibrium(skc1)))*r. % 0.40/0.66 586[4:SSi:584.0,498.0] || -> greater(zero,growth_rate(first_movers,equilibrium(skc1)))*r. % 0.40/0.66 587[4:MRR:519.0,586.0] || greater(growth_rate(efficient_producers,equilibrium(skc1)),zero)*l -> . % 0.40/0.66 589[4:NCh:14.2,14.0,587.0,537.0] || greater(growth_rate(first_movers,equilibrium(skc1)),zero)*l -> . % 0.40/0.66 595[4:OCh:14.1,14.0,586.0,8.1] SkP1(equilibrium(skc1)) || -> greater(zero,zero)*. % 0.40/0.66 596[4:SSi:595.0,498.0] || -> greater(zero,zero)*. % 0.40/0.66 616[4:NCh:14.2,14.0,589.0,8.1] SkP1(equilibrium(skc1)) || greater(zero,zero)* -> . % 0.40/0.66 621[4:SSi:616.0,498.0] || greater(zero,zero)* -> . % 0.40/0.66 622[4:MRR:621.0,596.0] || -> . % 0.40/0.66 623[4:Spt:622.0,58.0,528.0] || equal(skf3(skf5(skc1)),skf5(skc1))** -> . % 0.40/0.66 624[4:Spt:622.0,58.1] || -> greater(skf3(skf5(skc1)),skf5(skc1))*l. % 0.40/0.66 625[4:NCh:14.2,14.0,421.0,624.0] || greater(skf5(skc1),equilibrium(skc1))*l -> . % 0.40/0.66 626[4:NCh:14.2,14.0,421.0,624.0] || equal(skf5(skc1),equilibrium(skc1))** -> . % 0.40/0.66 627[4:MRR:120.1,626.0] || -> greater(equilibrium(skc1),skf5(skc1)) greater(skf5(skc1),equilibrium(skc1))*l. % 0.40/0.66 628[4:MRR:627.1,625.0] || -> greater(equilibrium(skc1),skf5(skc1))*r. % 0.40/0.66 629[4:MRR:527.0,628.0] || -> greater(growth_rate(efficient_producers,equilibrium(skc1)),growth_rate(first_movers,equilibrium(skc1)))*l. % 0.40/0.66 631[4:OCh:14.1,14.0,629.0,9.1] SkP1(equilibrium(skc1)) || -> greater(zero,growth_rate(first_movers,equilibrium(skc1)))*r. % 0.40/0.66 633[4:SSi:631.0,498.0] || -> greater(zero,growth_rate(first_movers,equilibrium(skc1)))*r. % 0.40/0.66 634[4:MRR:519.0,633.0] || greater(growth_rate(efficient_producers,equilibrium(skc1)),zero)*l -> . % 0.40/0.66 636[4:OCh:14.1,14.0,633.0,8.1] SkP1(equilibrium(skc1)) || -> greater(zero,zero)*. % 0.40/0.66 637[4:SSi:636.0,498.0] || -> greater(zero,zero)*. % 0.40/0.66 653[4:NCh:14.2,14.0,634.0,629.0] || greater(growth_rate(first_movers,equilibrium(skc1)),zero)*l -> . % 0.40/0.66 660[4:NCh:14.2,14.0,653.0,8.1] SkP1(equilibrium(skc1)) || greater(zero,zero)* -> . % 0.40/0.66 665[4:SSi:660.0,498.0] || greater(zero,zero)* -> . % 0.40/0.66 666[4:MRR:665.0,637.0] || -> . % 0.40/0.66 667[3:Spt:666.0,59.0,497.0] || equal(skf3(equilibrium(skc1)),equilibrium(skc1))** -> . % 0.40/0.67 668[3:Spt:666.0,59.1] || -> greater(skf3(equilibrium(skc1)),equilibrium(skc1))*l. % 0.40/0.67 680[4:Spt:58.0] || -> equal(skf3(skf5(skc1)),skf5(skc1))**. % 0.40/0.67 681[4:Rew:680.0,420.0] || equal(skf5(skc1),equilibrium(skc1))** -> . % 0.40/0.67 682[4:Rew:680.0,421.0] || greater(skf5(skc1),equilibrium(skc1))*l -> . % 0.40/0.67 686[4:MRR:120.1,681.0] || -> greater(equilibrium(skc1),skf5(skc1)) greater(skf5(skc1),equilibrium(skc1))*l. % 0.40/0.67 688[4:MRR:686.1,682.0] || -> greater(equilibrium(skc1),skf5(skc1))*r. % 0.40/0.67 746[0:SoR:480.0,334.2] || greater(skf3(u),skf5(skc1)) in_environment(skc1,u) in_environment(skc1,u) greater(skf3(u),equilibrium(skc1)) -> SkP1(skf3(u))*. % 0.40/0.67 748[0:Obv:746.1] || greater(skf3(u),skf5(skc1)) in_environment(skc1,u) greater(skf3(u),equilibrium(skc1)) -> SkP1(skf3(u))*. % 0.40/0.67 1016[0:Res:8.1,87.3] SkP1(skf3(u)) || equal(skf3(u),skf5(skc1)) in_environment(skc1,u) greater(zero,growth_rate(first_movers,skf3(u)))*r -> . % 0.40/0.67 1019[0:MRR:1016.3,86.3] SkP1(skf3(u)) || equal(skf3(u),skf5(skc1)) in_environment(skc1,u)* -> . % 0.40/0.67 1074[0:Res:8.1,405.3] SkP1(skf3(u)) || greater(skf3(u),skf5(skc1)) in_environment(skc1,u) greater(zero,growth_rate(first_movers,skf3(u)))*r -> . % 0.40/0.67 1077[0:MRR:1074.3,404.3] SkP1(skf3(u)) || greater(skf3(u),skf5(skc1)) in_environment(skc1,u)* -> . % 0.40/0.67 1080[2:SoR:1077.0,479.0] || greater(skf3(equilibrium(skc1)),skf5(skc1)) in_environment(skc1,equilibrium(skc1))* -> . % 0.40/0.67 1083[2:MRR:1080.1,49.0] || greater(skf3(equilibrium(skc1)),skf5(skc1))*l -> . % 0.40/0.67 1086[3:NCh:14.2,14.0,1083.0,668.0] || greater(equilibrium(skc1),skf5(skc1))*r -> . % 0.40/0.67 1087[3:NCh:14.2,14.0,1083.0,668.0] || equal(skf5(skc1),equilibrium(skc1))** -> . % 0.40/0.67 1088[4:MRR:1086.0,688.0] || -> . % 0.40/0.67 1089[4:Spt:1088.0,58.0,680.0] || equal(skf3(skf5(skc1)),skf5(skc1))** -> . % 0.40/0.67 1090[4:Spt:1088.0,58.1] || -> greater(skf3(skf5(skc1)),skf5(skc1))*l. % 0.40/0.67 1092[0:MRR:372.3,1019.0] || equal(skf3(u),skf5(skc1)) in_environment(skc1,u)* greater(skf3(u),equilibrium(skc1)) -> . % 0.40/0.67 1094[3:MRR:120.0,120.1,1086.0,1087.0] || -> greater(skf5(skc1),equilibrium(skc1))*l. % 0.40/0.67 1095[0:MRR:748.3,1077.0] || greater(skf3(u),skf5(skc1)) in_environment(skc1,u)* greater(skf3(u),equilibrium(skc1)) -> . % 0.40/0.67 1096[4:NCh:14.2,14.0,421.0,1090.0] || greater(skf5(skc1),equilibrium(skc1))*l -> . % 0.40/0.67 1098[4:MRR:1096.0,1094.0] || -> . % 0.40/0.67 1099[1:Spt:1098.0,45.0,48.0] || equal(skf6(skc1),equilibrium(skc1))** -> . % 0.40/0.67 1100[1:Spt:1098.0,45.1] || -> greater(skf6(skc1),equilibrium(skc1))*l. % 0.40/0.67 1101[0:SSi:60.1,60.0,2.0,1.0,2.0,1.0] || -> equal(skf3(skf6(skc1)),skf6(skc1)) greater(skf3(skf6(skc1)),skf6(skc1))*l. % 0.40/0.67 1104[0:Res:32.0,63.0] || -> greater(skf5(skc1),skf6(skc1)) equal(skf6(skc1),skf5(skc1)) greater(skf6(skc1),skf5(skc1))*l. % 0.40/0.67 1130[2:Spt:58.0] || -> equal(skf3(skf5(skc1)),skf5(skc1))**. % 0.40/0.67 1132[2:Rew:1130.0,421.0] || greater(skf5(skc1),equilibrium(skc1))*l -> . % 0.40/0.67 1133[2:Rew:1130.0,75.0] || -> greater(growth_rate(efficient_producers,skf5(skc1)),growth_rate(first_movers,skf5(skc1)))*l. % 0.40/0.67 1134[2:Rew:1130.0,78.0] || greater(zero,growth_rate(first_movers,skf5(skc1))) greater(growth_rate(first_movers,skf3(skf5(skc1))),zero)*l -> . % 0.40/0.67 1135[2:Rew:1130.0,79.0] || greater(zero,growth_rate(first_movers,skf5(skc1))) equal(growth_rate(first_movers,skf3(skf5(skc1))),zero)** -> . % 0.40/0.67 1136[2:Rew:1130.0,1135.1] || greater(zero,growth_rate(first_movers,skf5(skc1)))*r equal(growth_rate(first_movers,skf5(skc1)),zero) -> . % 0.40/0.67 1137[2:Rew:1130.0,1134.1] || greater(zero,growth_rate(first_movers,skf5(skc1))) greater(growth_rate(first_movers,skf5(skc1)),zero)*l -> . % 0.40/0.67 1148[2:SpL:1130.0,16.1] || greater(zero,growth_rate(first_movers,skf3(skf5(skc1))))*r greater(growth_rate(efficient_producers,skf5(skc1)),zero) -> . % 0.40/0.67 1150[2:SpL:1130.0,83.1] || in_environment(skc1,skf5(skc1)) greater_or_equal(skf5(skc1),equilibrium(skc1)) -> SkP0(skf3(skf5(skc1))) SkP1(skf3(skf5(skc1))) greater(zero,growth_rate(first_movers,skf3(skf5(skc1))))*r. % 0.40/0.67 1151[2:SpL:1130.0,70.1] || in_environment(skc1,skf5(skc1)) greater_or_equal(skf5(skc1),equilibrium(skc1)) -> SkP0(skf3(skf5(skc1))) SkP1(skf3(skf5(skc1))) greater(growth_rate(efficient_producers,skf3(skf5(skc1))),zero)*l. % 0.40/0.67 1155[2:Rew:1130.0,1148.0] || greater(zero,growth_rate(first_movers,skf5(skc1))) greater(growth_rate(efficient_producers,skf5(skc1)),zero)*l -> . % 0.40/0.67 1157[2:Rew:1130.0,1151.4,1130.0,1151.3,1130.0,1151.2] || in_environment(skc1,skf5(skc1)) greater_or_equal(skf5(skc1),equilibrium(skc1))* -> SkP0(skf5(skc1)) SkP1(skf5(skc1)) greater(growth_rate(efficient_producers,skf5(skc1)),zero). % 0.40/0.67 1158[2:MRR:1157.0,31.0] || greater_or_equal(skf5(skc1),equilibrium(skc1))* -> SkP0(skf5(skc1)) SkP1(skf5(skc1)) greater(growth_rate(efficient_producers,skf5(skc1)),zero). % 0.40/0.67 1159[2:Rew:1130.0,1150.4,1130.0,1150.3,1130.0,1150.2] || in_environment(skc1,skf5(skc1)) greater_or_equal(skf5(skc1),equilibrium(skc1))* -> SkP0(skf5(skc1)) SkP1(skf5(skc1)) greater(zero,growth_rate(first_movers,skf5(skc1))). % 0.40/0.67 1160[2:MRR:1159.0,31.0] || greater_or_equal(skf5(skc1),equilibrium(skc1))* -> SkP0(skf5(skc1)) SkP1(skf5(skc1)) greater(zero,growth_rate(first_movers,skf5(skc1))). % 0.40/0.67 1174[2:SpR:7.1,1133.0] SkP0(skf5(skc1)) || -> greater(zero,growth_rate(first_movers,skf5(skc1)))*r. % 0.40/0.67 1175[2:OCh:14.1,14.0,1133.0,9.1] SkP1(skf5(skc1)) || -> greater(zero,growth_rate(first_movers,skf5(skc1)))*r. % 0.40/0.67 1176[2:Rew:6.1,1174.1] SkP0(skf5(skc1)) || -> greater(zero,zero)*. % 0.40/0.67 1177[2:MRR:1160.2,1175.0] || greater_or_equal(skf5(skc1),equilibrium(skc1))* -> SkP0(skf5(skc1)) greater(zero,growth_rate(first_movers,skf5(skc1))). % 0.40/0.67 1199[2:SpL:6.1,1136.0] SkP0(skf5(skc1)) || greater(zero,zero) equal(growth_rate(first_movers,skf5(skc1)),zero)** -> . % 0.40/0.67 1200[2:Rew:6.1,1199.2] SkP0(skf5(skc1)) || greater(zero,zero)* equal(zero,zero) -> . % 0.40/0.67 1201[2:Obv:1200.2] SkP0(skf5(skc1)) || greater(zero,zero)* -> . % 0.40/0.67 1202[2:MRR:1201.1,1176.1] SkP0(skf5(skc1)) || -> . % 0.40/0.67 1203[2:MRR:1158.1,1202.0] || greater_or_equal(skf5(skc1),equilibrium(skc1))* -> SkP1(skf5(skc1)) greater(growth_rate(efficient_producers,skf5(skc1)),zero). % 0.40/0.67 1204[2:MRR:1177.1,1202.0] || greater_or_equal(skf5(skc1),equilibrium(skc1))* -> greater(zero,growth_rate(first_movers,skf5(skc1))). % 0.40/0.67 1222[3:Spt:1203.1] || -> SkP1(skf5(skc1))*. % 0.40/0.67 1223[3:MRR:1175.0,1222.0] || -> greater(zero,growth_rate(first_movers,skf5(skc1)))*r. % 0.40/0.67 1225[3:MRR:1137.0,1223.0] || greater(growth_rate(first_movers,skf5(skc1)),zero)*l -> . % 0.40/0.67 1230[3:OCh:14.1,14.0,1223.0,8.1] SkP1(skf5(skc1)) || -> greater(zero,zero)*. % 0.40/0.67 1231[3:SSi:1230.0,1222.0] || -> greater(zero,zero)*. % 0.40/0.67 1247[3:NCh:14.2,14.0,1225.0,8.1] SkP1(skf5(skc1)) || greater(zero,zero)* -> . % 0.40/0.67 1252[3:SSi:1247.0,1222.0] || greater(zero,zero)* -> . % 0.40/0.67 1253[3:MRR:1252.0,1231.0] || -> . % 0.40/0.67 1254[3:Spt:1253.0,1203.1,1222.0] || SkP1(skf5(skc1))* -> . % 0.40/0.67 1255[3:Spt:1253.0,1203.0,1203.2] || greater_or_equal(skf5(skc1),equilibrium(skc1))* -> greater(growth_rate(efficient_producers,skf5(skc1)),zero). % 0.40/0.67 1294[0:Res:32.0,1092.1] || equal(skf3(skf6(skc1)),skf5(skc1)) greater(skf3(skf6(skc1)),equilibrium(skc1))*l -> . % 0.40/0.67 1301[0:NCh:14.2,14.0,1294.1,1101.1] || equal(skf3(skf6(skc1)),skf5(skc1))** greater(skf6(skc1),equilibrium(skc1)) -> equal(skf3(skf6(skc1)),skf6(skc1)). % 0.40/0.67 1303[1:MRR:1301.1,1100.0] || equal(skf3(skf6(skc1)),skf5(skc1))** -> equal(skf3(skf6(skc1)),skf6(skc1)). % 0.40/0.67 1305[1:Rew:1303.1,1294.1] || equal(skf3(skf6(skc1)),skf5(skc1))** greater(skf6(skc1),equilibrium(skc1)) -> . % 0.40/0.67 1306[1:MRR:1305.1,1100.0] || equal(skf3(skf6(skc1)),skf5(skc1))** -> . % 0.40/0.67 1325[4:Spt:1104.1] || -> equal(skf6(skc1),skf5(skc1))**. % 0.40/0.67 1329[4:Rew:1325.0,33.0] || -> greater_or_equal(skf5(skc1),equilibrium(skc1))*. % 0.40/0.67 1336[4:MRR:1255.0,1329.0] || -> greater(growth_rate(efficient_producers,skf5(skc1)),zero)*l. % 0.40/0.67 1337[4:MRR:1204.0,1329.0] || -> greater(zero,growth_rate(first_movers,skf5(skc1)))*r. % 0.40/0.67 1341[4:MRR:1155.1,1336.0] || greater(zero,growth_rate(first_movers,skf5(skc1)))*r -> . % 0.40/0.67 1344[4:MRR:1341.0,1337.0] || -> . % 0.40/0.67 1351[4:Spt:1344.0,1104.1,1325.0] || equal(skf6(skc1),skf5(skc1))** -> . % 0.40/0.67 1352[4:Spt:1344.0,1104.0,1104.2] || -> greater(skf5(skc1),skf6(skc1)) greater(skf6(skc1),skf5(skc1))*l. % 0.40/0.67 1362[5:Spt:1101.0] || -> equal(skf3(skf6(skc1)),skf6(skc1))**. % 0.40/0.67 1368[5:SpR:1362.0,71.2] || greater(skf3(skf6(skc1)),skf5(skc1)) in_environment(skc1,skf6(skc1)) -> greater(growth_rate(efficient_producers,skf6(skc1)),growth_rate(first_movers,skf6(skc1)))*l. % 0.40/0.67 1370[5:SpR:1362.0,334.2] || greater(skf3(skf6(skc1)),equilibrium(skc1)) in_environment(skc1,skf6(skc1)) -> SkP0(skf6(skc1)) SkP1(skf3(skf6(skc1)))*. % 0.40/0.67 1375[5:SpL:1362.0,405.3] || greater(skf3(skf6(skc1)),skf5(skc1)) in_environment(skc1,skf6(skc1)) greater(zero,growth_rate(first_movers,skf3(skf6(skc1))))*r greater(growth_rate(first_movers,skf6(skc1)),zero) -> . % 0.40/0.67 1377[5:SpL:1362.0,16.1] || greater(zero,growth_rate(first_movers,skf3(skf6(skc1))))*r greater(growth_rate(efficient_producers,skf6(skc1)),zero) -> . % 0.40/0.67 1384[5:Rew:1362.0,1370.3,1362.0,1370.0] || greater(skf6(skc1),equilibrium(skc1)) in_environment(skc1,skf6(skc1))* -> SkP0(skf6(skc1)) SkP1(skf6(skc1)). % 0.40/0.67 1385[5:MRR:1384.1,32.0] || greater(skf6(skc1),equilibrium(skc1)) -> SkP0(skf6(skc1))* SkP1(skf6(skc1)). % 0.40/0.67 1386[5:MRR:1385.0,1100.0] || -> SkP0(skf6(skc1))* SkP1(skf6(skc1)). % 0.40/0.67 1387[5:Rew:1362.0,1377.0] || greater(zero,growth_rate(first_movers,skf6(skc1))) greater(growth_rate(efficient_producers,skf6(skc1)),zero)*l -> . % 0.40/0.67 1393[5:Rew:1362.0,1368.0] || greater(skf6(skc1),skf5(skc1)) in_environment(skc1,skf6(skc1)) -> greater(growth_rate(efficient_producers,skf6(skc1)),growth_rate(first_movers,skf6(skc1)))*l. % 0.40/0.68 1394[5:MRR:1393.1,32.0] || greater(skf6(skc1),skf5(skc1)) -> greater(growth_rate(efficient_producers,skf6(skc1)),growth_rate(first_movers,skf6(skc1)))*l. % 0.40/0.68 1399[5:Rew:1362.0,1375.2,1362.0,1375.0] || greater(skf6(skc1),skf5(skc1)) in_environment(skc1,skf6(skc1)) greater(zero,growth_rate(first_movers,skf6(skc1))) greater(growth_rate(first_movers,skf6(skc1)),zero)*l -> . % 0.40/0.68 1400[5:MRR:1399.1,32.0] || greater(skf6(skc1),skf5(skc1)) greater(zero,growth_rate(first_movers,skf6(skc1))) greater(growth_rate(first_movers,skf6(skc1)),zero)*l -> . % 0.40/0.68 1441[5:SpL:7.1,1387.1] SkP0(skf6(skc1)) || greater(zero,growth_rate(first_movers,skf6(skc1)))*r greater(zero,zero) -> . % 0.40/0.68 1442[5:Rew:6.1,1441.1] SkP0(skf6(skc1)) || greater(zero,zero)* greater(zero,zero)* -> . % 0.40/0.68 1443[5:Obv:1442.1] SkP0(skf6(skc1)) || greater(zero,zero)* -> . % 0.40/0.68 1446[5:SpR:7.1,1394.1] SkP0(skf6(skc1)) || greater(skf6(skc1),skf5(skc1)) -> greater(zero,growth_rate(first_movers,skf6(skc1)))*r. % 0.40/0.68 1447[5:OCh:14.1,14.0,1394.1,9.1] SkP1(skf6(skc1)) || greater(skf6(skc1),skf5(skc1)) -> greater(zero,growth_rate(first_movers,skf6(skc1)))*r. % 0.40/0.68 1450[5:Rew:6.1,1446.2] SkP0(skf6(skc1)) || greater(skf6(skc1),skf5(skc1))*l -> greater(zero,zero). % 0.40/0.68 1451[5:MRR:1450.2,1443.1] SkP0(skf6(skc1)) || greater(skf6(skc1),skf5(skc1))*l -> . % 0.40/0.68 1452[5:SoR:1451.0,1386.0] || greater(skf6(skc1),skf5(skc1)) -> SkP1(skf6(skc1))*. % 0.40/0.68 1453[5:MRR:1447.0,1452.1] || greater(skf6(skc1),skf5(skc1)) -> greater(zero,growth_rate(first_movers,skf6(skc1)))*r. % 0.40/0.68 1455[5:MRR:1400.1,1453.1] || greater(skf6(skc1),skf5(skc1)) greater(growth_rate(first_movers,skf6(skc1)),zero)*l -> . % 0.40/0.68 1487[5:Res:8.1,1455.1] SkP1(skf6(skc1)) || greater(skf6(skc1),skf5(skc1))*l -> . % 0.40/0.68 1490[5:MRR:1487.0,1452.1] || greater(skf6(skc1),skf5(skc1))*l -> . % 0.40/0.68 1491[5:MRR:1352.1,1490.0] || -> greater(skf5(skc1),skf6(skc1))*r. % 0.40/0.68 1493[5:OCh:14.1,14.0,1491.0,46.3] stable(skc1) environment(skc1) || -> equal(skf6(skc1),equilibrium(skc1))** greater(skf5(skc1),equilibrium(skc1)). % 0.40/0.68 1497[5:SSi:1493.1,1493.0,2.0,1.0,2.0,1.0] || -> equal(skf6(skc1),equilibrium(skc1))** greater(skf5(skc1),equilibrium(skc1)). % 0.40/0.68 1498[5:MRR:1497.0,1497.1,1099.0,1132.0] || -> . % 0.40/0.68 1499[5:Spt:1498.0,1101.0,1362.0] || equal(skf3(skf6(skc1)),skf6(skc1))** -> . % 0.40/0.68 1500[5:Spt:1498.0,1101.1] || -> greater(skf3(skf6(skc1)),skf6(skc1))*l. % 0.40/0.68 1505[0:Res:32.0,1095.1] || greater(skf3(skf6(skc1)),skf5(skc1))*l greater(skf3(skf6(skc1)),equilibrium(skc1)) -> . % 0.40/0.68 1510[5:NCh:14.2,14.0,1505.0,1500.0] || greater(skf6(skc1),skf5(skc1)) greater(skf3(skf6(skc1)),equilibrium(skc1))*l -> . % 0.40/0.68 1512[5:NCh:14.2,14.0,1510.1,1500.0] || greater(skf6(skc1),skf5(skc1))*l greater(skf6(skc1),equilibrium(skc1)) -> . % 0.40/0.68 1514[5:MRR:1512.1,1100.0] || greater(skf6(skc1),skf5(skc1))*l -> . % 0.40/0.68 1515[5:MRR:1352.1,1514.0] || -> greater(skf5(skc1),skf6(skc1))*r. % 0.40/0.68 1516[5:OCh:14.1,14.0,1515.0,46.3] stable(skc1) environment(skc1) || -> equal(skf6(skc1),equilibrium(skc1))** greater(skf5(skc1),equilibrium(skc1)). % 0.40/0.68 1520[5:SSi:1516.1,1516.0,2.0,1.0,2.0,1.0] || -> equal(skf6(skc1),equilibrium(skc1))** greater(skf5(skc1),equilibrium(skc1)). % 0.40/0.68 1521[5:MRR:1520.0,1520.1,1099.0,1132.0] || -> . % 0.40/0.68 1522[2:Spt:1521.0,58.0,1130.0] || equal(skf3(skf5(skc1)),skf5(skc1))** -> . % 0.40/0.68 1523[2:Spt:1521.0,58.1] || -> greater(skf3(skf5(skc1)),skf5(skc1))*l. % 0.40/0.68 1524[2:NCh:14.2,14.0,421.0,1523.0] || greater(skf5(skc1),equilibrium(skc1))*l -> . % 0.40/0.68 1526[3:Spt:1101.0] || -> equal(skf3(skf6(skc1)),skf6(skc1))**. % 0.40/0.68 1527[3:Rew:1526.0,1306.0] || equal(skf6(skc1),skf5(skc1))** -> . % 0.40/0.68 1529[3:Rew:1526.0,1505.0] || greater(skf6(skc1),skf5(skc1)) greater(skf3(skf6(skc1)),equilibrium(skc1))*l -> . % 0.40/0.68 1530[3:MRR:1104.1,1527.0] || -> greater(skf5(skc1),skf6(skc1)) greater(skf6(skc1),skf5(skc1))*l. % 0.40/0.68 1531[3:Rew:1526.0,1529.1] || greater(skf6(skc1),skf5(skc1))*l greater(skf6(skc1),equilibrium(skc1)) -> . % 0.40/0.68 1532[3:MRR:1531.1,1100.0] || greater(skf6(skc1),skf5(skc1))*l -> . % 0.40/0.68 1533[3:MRR:1530.1,1532.0] || -> greater(skf5(skc1),skf6(skc1))*r. % 0.40/0.68 1577[3:OCh:14.1,14.0,1533.0,46.3] stable(skc1) environment(skc1) || -> equal(skf6(skc1),equilibrium(skc1))** greater(skf5(skc1),equilibrium(skc1)). % 0.40/0.68 1581[3:SSi:1577.1,1577.0,2.0,1.0,2.0,1.0] || -> equal(skf6(skc1),equilibrium(skc1))** greater(skf5(skc1),equilibrium(skc1)). % 0.40/0.68 1582[3:MRR:1581.0,1099.0] || -> greater(skf5(skc1),equilibrium(skc1))*l. % 0.40/0.68 1583[3:MRR:1582.0,1524.0] || -> . % 0.40/0.68 1584[3:Spt:1583.0,1101.0,1526.0] || equal(skf3(skf6(skc1)),skf6(skc1))** -> . % 0.40/0.68 1585[3:Spt:1583.0,1101.1] || -> greater(skf3(skf6(skc1)),skf6(skc1))*l. % 0.40/0.68 1595[3:NCh:14.2,14.0,1505.0,1585.0] || greater(skf6(skc1),skf5(skc1)) greater(skf3(skf6(skc1)),equilibrium(skc1))*l -> . % 0.40/0.68 1597[4:Spt:1104.1] || -> equal(skf6(skc1),skf5(skc1))**. % 0.40/0.68 1601[4:Rew:1597.0,1100.0] || -> greater(skf5(skc1),equilibrium(skc1))*l. % 0.40/0.68 1612[4:MRR:1601.0,1524.0] || -> . % 0.40/0.68 1618[4:Spt:1612.0,1104.1,1597.0] || equal(skf6(skc1),skf5(skc1))** -> . % 0.40/0.68 1619[4:Spt:1612.0,1104.0,1104.2] || -> greater(skf5(skc1),skf6(skc1)) greater(skf6(skc1),skf5(skc1))*l. % 0.40/0.68 1620[5:Spt:1619.0] || -> greater(skf5(skc1),skf6(skc1))*r. % 0.40/0.68 1621[5:OCh:14.1,14.0,1620.0,46.3] stable(skc1) environment(skc1) || -> equal(skf6(skc1),equilibrium(skc1))** greater(skf5(skc1),equilibrium(skc1)). % 0.40/0.68 1623[5:SSi:1621.1,1621.0,2.0,1.0,2.0,1.0] || -> equal(skf6(skc1),equilibrium(skc1))** greater(skf5(skc1),equilibrium(skc1)). % 0.40/0.68 1624[5:MRR:1623.1,1524.0] || -> equal(skf6(skc1),equilibrium(skc1))**. % 0.40/0.68 1625[5:MRR:1624.0,1099.0] || -> . % 0.40/0.68 1626[5:Spt:1625.0,1619.0,1620.0] || greater(skf5(skc1),skf6(skc1))*r -> . % 0.40/0.68 1627[5:Spt:1625.0,1619.1] || -> greater(skf6(skc1),skf5(skc1))*l. % 0.40/0.68 1629[5:MRR:1595.0,1627.0] || greater(skf3(skf6(skc1)),equilibrium(skc1))*l -> . % 0.40/0.68 1640[5:NCh:14.2,14.0,1629.0,1585.0] || greater(skf6(skc1),equilibrium(skc1))*l -> . % 0.40/0.68 1642[5:MRR:1640.0,1100.0] || -> . % 0.40/0.68 % SZS output end Refutation % 0.40/0.68 Formulae used in the proof : prove_l11 a4 mp_greater_or_equal l6 l1 mp_greater_transitivity mp_times_in_environment % 0.40/0.68 %------------------------------------------------------------------------------