%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT034-2 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n010.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:51 AM UTC 2026 % Result : Unsatisfiable 0.47s 0.79s % Output : Refutation 0.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT034-2 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : run_spass %d %s % 0.11/0.36 % Computer : n010.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Mon Sep 7 12:32:40 UTC 2026 % 0.11/0.37 % CPUTime : % 0.47/0.79 % 0.47/0.79 SPASS V 3.9 % 0.47/0.79 SPASS beiseite: Proof found. % 0.47/0.79 % SZS status Theorem % 0.47/0.79 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.47/0.79 SPASS derived 1108 clauses, backtracked 89 clauses, performed 5 splits and kept 659 clauses. % 0.47/0.79 SPASS allocated 76784 KBytes. % 0.47/0.79 SPASS spent 0:00:00.41 on the problem. % 0.47/0.79 0:00:00.06 for the input. % 0.47/0.79 0:00:00.00 for the FLOTTER CNF translation. % 0.47/0.79 0:00:00.04 for inferences. % 0.47/0.79 0:00:00.01 for the backtracking. % 0.47/0.79 0:00:00.25 for the reduction. % 0.47/0.79 % 0.47/0.79 % 0.47/0.79 Here is a proof with depth 8, length 129 : % 0.47/0.79 % SZS output start Refutation % 0.47/0.79 1[0:Inp] environment(u) || greater(growth_rate(v,w),growth_rate(x,w))*+ subpopulations(x,v,u,w)* -> selection_favors(v,x,w). % 0.47/0.79 2[0:Inp] environment(u) || decreases(difference(disbanding_rate(first_movers,v),disbanding_rate(efficient_producers,v)))*+ subpopulations(first_movers,efficient_producers,u,v)* -> . % 0.47/0.79 3[0:Inp] environment(u) || in_environment(u,critical_point(u)) -> subpopulations(first_movers,efficient_producers,u,critical_point(u))*. % 0.47/0.79 4[0:Inp] environment(u) || in_environment(u,appear(efficient_producers,u)) -> subpopulations(first_movers,efficient_producers,u,appear(efficient_producers,u))*. % 0.47/0.79 5[0:Inp] || decreases(difference(founding_rate(first_movers,u),founding_rate(efficient_producers,u)))* -> decreases(difference(growth_rate(first_movers,u),growth_rate(efficient_producers,u))) decreases(difference(disbanding_rate(first_movers,u),disbanding_rate(efficient_producers,u))). % 0.47/0.79 6[0:Inp] environment(u) || decreases(difference(growth_rate(first_movers,v),growth_rate(efficient_producers,v))) greater(w,v)* in_environment(u,w)* greater_or_equal(v,appear(efficient_producers,u))* greater_or_equal(difference(growth_rate(first_movers,w),growth_rate(efficient_producers,w)),zero)*+ -> greater(difference(growth_rate(first_movers,v),growth_rate(efficient_producers,v)),zero)*. % 0.47/0.79 7[0:Inp] || greater(zero,difference(growth_rate(first_movers,u),growth_rate(efficient_producers,u)))* -> greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u)). % 0.47/0.79 9[0:Inp] || greater(difference(growth_rate(first_movers,u),growth_rate(efficient_producers,u)),zero)* -> greater(growth_rate(first_movers,u),growth_rate(efficient_producers,u)). % 0.47/0.79 14[0:Inp] environment(u) || in_environment(u,critical_point(u))* greater_or_equal(v,appear(efficient_producers,u))*+ greater(critical_point(u),v) -> in_environment(u,v). % 0.47/0.79 16[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v) -> subpopulations(efficient_producers,first_movers,u,v)*. % 0.47/0.79 17[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v) -> greater_or_equal(v,appear(efficient_producers,u))*. % 0.47/0.79 18[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.47/0.79 19[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 0.47/0.79 20[0:Inp] || equal(u,v) -> greater_or_equal(u,v)*. % 0.47/0.79 21[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)*+ -> greater(zero,difference(growth_rate(first_movers,v),growth_rate(efficient_producers,v))) greater_or_equal(difference(growth_rate(first_movers,v),growth_rate(efficient_producers,v)),zero)*. % 0.47/0.79 22[0:Inp] environment(u) || equal(v,critical_point(u))* greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v))*+ -> . % 0.47/0.79 24[0:Inp] environment(u) || greater_or_equal(v,w)* greater_or_equal(w,x)* subpopulations(first_movers,efficient_producers,u,v)*+ subpopulations(first_movers,efficient_producers,u,x)* -> subpopulations(first_movers,efficient_producers,u,w)*. % 0.47/0.79 25[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)*+ -> decreases(difference(founding_rate(first_movers,v),founding_rate(efficient_producers,v)))*. % 0.47/0.79 26[0:Inp] || -> environment(sk1)*. % 0.47/0.79 27[0:Inp] || -> in_environment(sk1,critical_point(sk1))*. % 0.47/0.79 28[0:Inp] || -> greater_or_equal(sk2,appear(efficient_producers,sk1))*. % 0.47/0.79 29[0:Inp] || -> greater(critical_point(sk1),sk2)*. % 0.47/0.79 30[0:Inp] || selection_favors(first_movers,efficient_producers,sk2)* -> . % 0.47/0.79 38[0:Res:26.0,1.0] || greater(growth_rate(u,v),growth_rate(w,v))* subpopulations(w,u,sk1,v) -> selection_favors(u,w,v). % 0.47/0.79 41[0:Res:26.0,4.0] || in_environment(sk1,appear(efficient_producers,sk1)) -> subpopulations(first_movers,efficient_producers,sk1,appear(efficient_producers,sk1))*. % 0.47/0.79 42[0:Res:26.0,22.0] || equal(u,critical_point(sk1)) greater(growth_rate(efficient_producers,u),growth_rate(first_movers,u))* -> . % 0.47/0.79 45[0:Res:26.0,17.0] || subpopulations(first_movers,efficient_producers,sk1,u) -> greater_or_equal(u,appear(efficient_producers,sk1))*. % 0.47/0.79 48[0:Res:29.0,19.0] || -> greater_or_equal(critical_point(sk1),sk2)*. % 0.47/0.79 52[0:Res:27.0,14.1] environment(sk1) || greater_or_equal(u,appear(efficient_producers,sk1))* greater(critical_point(sk1),u) -> in_environment(sk1,u). % 0.47/0.79 53[0:Res:27.0,3.1] environment(sk1) || -> subpopulations(first_movers,efficient_producers,sk1,critical_point(sk1))*. % 0.47/0.79 59[0:Res:28.0,14.2] environment(sk1) || in_environment(sk1,critical_point(sk1))* greater(critical_point(sk1),sk2) -> in_environment(sk1,sk2). % 0.47/0.79 60[0:Res:28.0,6.3] environment(sk1) || in_environment(sk1,u) greater_or_equal(difference(growth_rate(first_movers,u),growth_rate(efficient_producers,u)),zero)* greater(u,sk2) decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2))) -> greater(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)),zero). % 0.47/0.79 61[0:Res:28.0,18.0] || -> greater(sk2,appear(efficient_producers,sk1))* equal(appear(efficient_producers,sk1),sk2). % 0.47/0.79 62[0:Res:28.0,24.3] environment(u) || greater_or_equal(v,sk2) subpopulations(first_movers,efficient_producers,u,v)* subpopulations(first_movers,efficient_producers,u,appear(efficient_producers,sk1))*+ -> subpopulations(first_movers,efficient_producers,u,sk2). % 0.47/0.79 66[0:MRR:53.0,26.0] || -> subpopulations(first_movers,efficient_producers,sk1,critical_point(sk1))*. % 0.47/0.79 67[0:MRR:59.0,59.1,59.2,26.0,27.0,29.0] || -> in_environment(sk1,sk2)*. % 0.47/0.79 68[0:MRR:52.0,26.0] || greater_or_equal(u,appear(efficient_producers,sk1))* greater(critical_point(sk1),u) -> in_environment(sk1,u). % 0.47/0.79 71[0:MRR:60.0,26.0] || decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2))) greater(u,sk2) in_environment(sk1,u) greater_or_equal(difference(growth_rate(first_movers,u),growth_rate(efficient_producers,u)),zero)* -> greater(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)),zero). % 0.47/0.79 72[1:Spt:61.1] || -> equal(appear(efficient_producers,sk1),sk2)**. % 0.47/0.79 81[1:Rew:72.0,41.0] || in_environment(sk1,sk2) -> subpopulations(first_movers,efficient_producers,sk1,appear(efficient_producers,sk1))*. % 0.47/0.79 82[1:Rew:72.0,81.1] || in_environment(sk1,sk2) -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.47/0.79 83[1:MRR:82.0,67.0] || -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.47/0.79 129[1:Res:83.0,25.1] environment(sk1) || -> decreases(difference(founding_rate(first_movers,sk2),founding_rate(efficient_producers,sk2)))*. % 0.47/0.79 133[1:SSi:129.0,26.0] || -> decreases(difference(founding_rate(first_movers,sk2),founding_rate(efficient_producers,sk2)))*. % 0.47/0.79 184[1:Res:133.0,5.0] || -> decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2))) decreases(difference(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2)))*. % 0.47/0.79 190[1:Res:184.1,2.1] environment(u) || subpopulations(first_movers,efficient_producers,u,sk2)*+ -> decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)))*. % 0.47/0.79 191[1:Res:83.0,190.1] environment(sk1) || -> decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)))*. % 0.47/0.79 192[1:SSi:191.0,26.0] || -> decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)))*. % 0.47/0.79 193[1:MRR:71.0,192.0] || greater(u,sk2) in_environment(sk1,u) greater_or_equal(difference(growth_rate(first_movers,u),growth_rate(efficient_producers,u)),zero)* -> greater(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)),zero). % 0.47/0.79 210[0:Res:66.0,21.1] environment(sk1) || -> greater(zero,difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1)))) greater_or_equal(difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1))),zero)*. % 0.47/0.79 214[0:SSi:210.0,26.0] || -> greater(zero,difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1)))) greater_or_equal(difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1))),zero)*. % 0.47/0.79 227[0:Res:66.0,24.3] environment(sk1) || greater_or_equal(critical_point(sk1),u) greater_or_equal(u,v)* subpopulations(first_movers,efficient_producers,sk1,v)* -> subpopulations(first_movers,efficient_producers,sk1,u)*. % 0.47/0.79 231[0:SSi:227.0,26.0] || greater_or_equal(critical_point(sk1),u) greater_or_equal(u,v)* subpopulations(first_movers,efficient_producers,sk1,v)*+ -> subpopulations(first_movers,efficient_producers,sk1,u)*. % 0.47/0.79 327[0:Res:4.2,231.2] environment(sk1) || in_environment(sk1,appear(efficient_producers,sk1)) greater_or_equal(critical_point(sk1),u) greater_or_equal(u,appear(efficient_producers,sk1))* -> subpopulations(first_movers,efficient_producers,sk1,u). % 0.47/0.79 461[1:Res:214.1,193.2] || greater(critical_point(sk1),sk2) in_environment(sk1,critical_point(sk1)) -> greater(zero,difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1))))* greater(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)),zero). % 0.47/0.79 463[1:MRR:461.0,461.1,29.0,27.0] || -> greater(zero,difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1))))* greater(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)),zero). % 0.47/0.79 464[2:Spt:463.0] || -> greater(zero,difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1))))*. % 0.47/0.79 466[2:Res:464.0,7.0] || -> greater(growth_rate(efficient_producers,critical_point(sk1)),growth_rate(first_movers,critical_point(sk1)))*. % 0.47/0.79 469[2:Res:466.0,42.1] || equal(critical_point(sk1),critical_point(sk1))* -> . % 0.47/0.79 474[2:Obv:469.0] || -> . % 0.47/0.79 476[2:Spt:474.0,463.0,464.0] || greater(zero,difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1))))* -> . % 0.47/0.79 477[2:Spt:474.0,463.1] || -> greater(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)),zero)*. % 0.47/0.79 484[2:Res:477.0,9.0] || -> greater(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2))*. % 0.47/0.79 489[2:Res:484.0,38.0] || subpopulations(efficient_producers,first_movers,sk1,sk2)* -> selection_favors(first_movers,efficient_producers,sk2). % 0.47/0.79 491[2:MRR:489.1,30.0] || subpopulations(efficient_producers,first_movers,sk1,sk2)* -> . % 0.47/0.79 493[2:Res:16.2,491.0] environment(sk1) || subpopulations(first_movers,efficient_producers,sk1,sk2)* -> . % 0.47/0.79 495[2:SSi:493.0,26.0] || subpopulations(first_movers,efficient_producers,sk1,sk2)* -> . % 0.47/0.79 496[2:MRR:495.0,83.0] || -> . % 0.47/0.79 497[1:Spt:496.0,61.1,72.0] || equal(appear(efficient_producers,sk1),sk2)** -> . % 0.47/0.79 498[1:Spt:496.0,61.0] || -> greater(sk2,appear(efficient_producers,sk1))*. % 0.47/0.79 499[0:SSi:327.0,26.0] || in_environment(sk1,appear(efficient_producers,sk1)) greater_or_equal(critical_point(sk1),u) greater_or_equal(u,appear(efficient_producers,sk1))* -> subpopulations(first_movers,efficient_producers,sk1,u). % 0.47/0.79 508[0:Res:45.1,18.0] || subpopulations(first_movers,efficient_producers,sk1,u) -> equal(u,appear(efficient_producers,sk1)) greater(u,appear(efficient_producers,sk1))*. % 0.47/0.79 522[0:Res:20.1,68.0] || equal(u,appear(efficient_producers,sk1)) greater(critical_point(sk1),u)* -> in_environment(sk1,u). % 0.47/0.79 551[0:Res:508.2,522.1] || subpopulations(first_movers,efficient_producers,sk1,critical_point(sk1))* equal(appear(efficient_producers,sk1),appear(efficient_producers,sk1)) -> equal(appear(efficient_producers,sk1),critical_point(sk1)) in_environment(sk1,appear(efficient_producers,sk1)). % 0.47/0.79 558[0:Obv:551.1] || subpopulations(first_movers,efficient_producers,sk1,critical_point(sk1))* -> equal(appear(efficient_producers,sk1),critical_point(sk1)) in_environment(sk1,appear(efficient_producers,sk1)). % 0.47/0.79 559[0:MRR:558.0,66.0] || -> equal(appear(efficient_producers,sk1),critical_point(sk1)) in_environment(sk1,appear(efficient_producers,sk1))*. % 0.47/0.79 564[2:Spt:559.0] || -> equal(appear(efficient_producers,sk1),critical_point(sk1))**. % 0.47/0.79 587[2:Rew:564.0,62.3] environment(u) || greater_or_equal(v,sk2) subpopulations(first_movers,efficient_producers,u,v)* subpopulations(first_movers,efficient_producers,u,critical_point(sk1))*+ -> subpopulations(first_movers,efficient_producers,u,sk2). % 0.47/0.79 659[2:Res:66.0,587.3] environment(sk1) || greater_or_equal(u,sk2) subpopulations(first_movers,efficient_producers,sk1,u)* -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.47/0.79 662[2:SSi:659.0,26.0] || greater_or_equal(u,sk2) subpopulations(first_movers,efficient_producers,sk1,u)*+ -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.47/0.79 665[2:Res:66.0,662.1] || greater_or_equal(critical_point(sk1),sk2) -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.47/0.79 669[2:MRR:665.0,48.0] || -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.47/0.79 680[2:Res:669.0,25.1] environment(sk1) || -> decreases(difference(founding_rate(first_movers,sk2),founding_rate(efficient_producers,sk2)))*. % 0.47/0.79 681[2:SSi:680.0,26.0] || -> decreases(difference(founding_rate(first_movers,sk2),founding_rate(efficient_producers,sk2)))*. % 0.47/0.79 683[2:Res:681.0,5.0] || -> decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2))) decreases(difference(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2)))*. % 0.47/0.79 729[2:Res:683.1,2.1] environment(u) || subpopulations(first_movers,efficient_producers,u,sk2)*+ -> decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)))*. % 0.47/0.79 753[2:Res:669.0,729.1] environment(sk1) || -> decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)))*. % 0.47/0.79 754[2:SSi:753.0,26.0] || -> decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)))*. % 0.47/0.79 755[2:MRR:71.0,754.0] || greater(u,sk2) in_environment(sk1,u) greater_or_equal(difference(growth_rate(first_movers,u),growth_rate(efficient_producers,u)),zero)* -> greater(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)),zero). % 0.47/0.79 1017[3:Spt:214.0] || -> greater(zero,difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1))))*. % 0.47/0.79 1020[3:Res:1017.0,7.0] || -> greater(growth_rate(efficient_producers,critical_point(sk1)),growth_rate(first_movers,critical_point(sk1)))*. % 0.47/0.79 1024[3:Res:1020.0,42.1] || equal(critical_point(sk1),critical_point(sk1))* -> . % 0.47/0.79 1029[3:Obv:1024.0] || -> . % 0.47/0.79 1031[3:Spt:1029.0,214.0,1017.0] || greater(zero,difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1))))* -> . % 0.47/0.79 1032[3:Spt:1029.0,214.1] || -> greater_or_equal(difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1))),zero)*. % 0.47/0.79 1045[3:Res:1032.0,755.2] || greater(critical_point(sk1),sk2) in_environment(sk1,critical_point(sk1)) -> greater(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)),zero)*. % 0.47/0.79 1046[3:MRR:1045.0,1045.1,29.0,27.0] || -> greater(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)),zero)*. % 0.47/0.79 1050[3:Res:1046.0,9.0] || -> greater(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2))*. % 0.47/0.79 1058[3:Res:1050.0,38.0] || subpopulations(efficient_producers,first_movers,sk1,sk2)* -> selection_favors(first_movers,efficient_producers,sk2). % 0.47/0.79 1060[3:MRR:1058.1,30.0] || subpopulations(efficient_producers,first_movers,sk1,sk2)* -> . % 0.47/0.79 1063[3:Res:16.2,1060.0] environment(sk1) || subpopulations(first_movers,efficient_producers,sk1,sk2)* -> . % 0.47/0.79 1065[3:SSi:1063.0,26.0] || subpopulations(first_movers,efficient_producers,sk1,sk2)* -> . % 0.47/0.79 1066[3:MRR:1065.0,669.0] || -> . % 0.47/0.79 1067[2:Spt:1066.0,559.0,564.0] || equal(appear(efficient_producers,sk1),critical_point(sk1))** -> . % 0.47/0.79 1068[2:Spt:1066.0,559.1] || -> in_environment(sk1,appear(efficient_producers,sk1))*. % 0.47/0.79 1070[2:MRR:499.0,1068.0] || greater_or_equal(critical_point(sk1),u) greater_or_equal(u,appear(efficient_producers,sk1))* -> subpopulations(first_movers,efficient_producers,sk1,u). % 0.57/0.80 1140[2:Res:28.0,1070.1] || greater_or_equal(critical_point(sk1),sk2) -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.57/0.80 1141[2:MRR:1140.0,48.0] || -> subpopulations(first_movers,efficient_producers,sk1,sk2)*. % 0.57/0.80 1156[2:Res:1141.0,25.1] environment(sk1) || -> decreases(difference(founding_rate(first_movers,sk2),founding_rate(efficient_producers,sk2)))*. % 0.57/0.80 1159[2:SSi:1156.0,26.0] || -> decreases(difference(founding_rate(first_movers,sk2),founding_rate(efficient_producers,sk2)))*. % 0.57/0.80 1161[2:Res:1159.0,5.0] || -> decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2))) decreases(difference(disbanding_rate(first_movers,sk2),disbanding_rate(efficient_producers,sk2)))*. % 0.57/0.80 1185[2:Res:1161.1,2.1] environment(u) || subpopulations(first_movers,efficient_producers,u,sk2)*+ -> decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)))*. % 0.57/0.80 1220[2:Res:1141.0,1185.1] environment(sk1) || -> decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)))*. % 0.57/0.80 1221[2:SSi:1220.0,26.0] || -> decreases(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)))*. % 0.57/0.80 1222[2:MRR:71.0,1221.0] || greater(u,sk2) in_environment(sk1,u) greater_or_equal(difference(growth_rate(first_movers,u),growth_rate(efficient_producers,u)),zero)* -> greater(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)),zero). % 0.57/0.80 1365[3:Spt:214.0] || -> greater(zero,difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1))))*. % 0.57/0.80 1368[3:Res:1365.0,7.0] || -> greater(growth_rate(efficient_producers,critical_point(sk1)),growth_rate(first_movers,critical_point(sk1)))*. % 0.57/0.80 1372[3:Res:1368.0,42.1] || equal(critical_point(sk1),critical_point(sk1))* -> . % 0.57/0.80 1377[3:Obv:1372.0] || -> . % 0.57/0.80 1379[3:Spt:1377.0,214.0,1365.0] || greater(zero,difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1))))* -> . % 0.57/0.80 1380[3:Spt:1377.0,214.1] || -> greater_or_equal(difference(growth_rate(first_movers,critical_point(sk1)),growth_rate(efficient_producers,critical_point(sk1))),zero)*. % 0.57/0.80 1391[3:Res:1380.0,1222.2] || greater(critical_point(sk1),sk2) in_environment(sk1,critical_point(sk1)) -> greater(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)),zero)*. % 0.57/0.80 1392[3:MRR:1391.0,1391.1,29.0,27.0] || -> greater(difference(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2)),zero)*. % 0.57/0.80 1396[3:Res:1392.0,9.0] || -> greater(growth_rate(first_movers,sk2),growth_rate(efficient_producers,sk2))*. % 0.57/0.80 1403[3:Res:1396.0,38.0] || subpopulations(efficient_producers,first_movers,sk1,sk2)* -> selection_favors(first_movers,efficient_producers,sk2). % 0.57/0.80 1405[3:MRR:1403.1,30.0] || subpopulations(efficient_producers,first_movers,sk1,sk2)* -> . % 0.57/0.80 1407[3:Res:16.2,1405.0] environment(sk1) || subpopulations(first_movers,efficient_producers,sk1,sk2)* -> . % 0.57/0.80 1409[3:SSi:1407.0,26.0] || subpopulations(first_movers,efficient_producers,sk1,sk2)* -> . % 0.57/0.80 1410[3:MRR:1409.0,1141.0] || -> . % 0.57/0.80 % SZS output end Refutation % 0.57/0.80 Formulae used in the proof : mp1_high_growth_rates_33 l3_34 mp_critical_point_means_FM_and_EP_35 mp_FM_and_EP_when_EP_appears_36 mp_difference_between_founding_rates_37 mp_decreasing_function_38 mp_negative_growth_rate_difference_39 mp_positive_growth_rate_difference_41 mp_critical_time_points_46 mp_symmetry_of_subpopulations_48 mp_FM_and_EP_members_EP_appeared_49 mp_greater_or_equal_50 mp_greater_or_equal_51 mp_greater_or_equal_52 mp_relationship_of_growth_rates_53 d1_54 a10_56 a12_57 prove_t3_58 prove_t3_59 prove_t3_60 prove_t3_61 prove_t3_62 % 0.57/0.80 %------------------------------------------------------------------------------