%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT034+2 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n020.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 : Theorem 0.57s 0.80s % 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.0.0. % 0.00/0.04 % Command : run_spass %d %s % 0.10/0.34 % Computer : n020.cluster.edu % 0.10/0.34 % Model : x86_64 x86_64 % 0.10/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.34 % Memory : 8046.5625MB % 0.10/0.34 % OS : Linux 6.8.0-71-generic % 0.10/0.34 % CPULimit : 300 % 0.10/0.34 % WCLimit : 300 % 0.10/0.34 % DateTime : Mon Sep 7 12:32:13 UTC 2026 % 0.10/0.34 % CPUTime : % 0.57/0.80 % 0.57/0.80 SPASS V 3.9 % 0.57/0.80 SPASS beiseite: Proof found. % 0.57/0.80 % SZS status Theorem % 0.57/0.80 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.57/0.80 SPASS derived 1159 clauses, backtracked 86 clauses, performed 5 splits and kept 627 clauses. % 0.57/0.80 SPASS allocated 98818 KBytes. % 0.57/0.80 SPASS spent 0:00:00.45 on the problem. % 0.57/0.80 0:00:00.06 for the input. % 0.57/0.80 0:00:00.05 for the FLOTTER CNF translation. % 0.57/0.80 0:00:00.04 for inferences. % 0.57/0.80 0:00:00.01 for the backtracking. % 0.57/0.80 0:00:00.24 for the reduction. % 0.57/0.80 % 0.57/0.80 % 0.57/0.80 Here is a proof with depth 8, length 126 : % 0.57/0.80 % SZS output start Refutation % 0.57/0.80 1[0:Inp] || -> environment(skc3)*. % 0.57/0.80 2[0:Inp] || -> in_environment(skc3,critical_point(skc3))*. % 0.57/0.80 3[0:Inp] || -> greater(critical_point(skc3),skc2)*. % 0.57/0.80 4[0:Inp] || -> greater_or_equal(skc2,appear(efficient_producers,skc3))*. % 0.57/0.80 5[0:Inp] || selection_favors(first_movers,efficient_producers,skc2)* -> . % 0.57/0.80 7[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 0.57/0.80 8[0:Inp] || equal(u,v) -> greater_or_equal(u,v)*. % 0.57/0.80 10[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 0.57/0.80 11[0:Inp] environment(u) || greater(growth_rate(efficient_producers,critical_point(u)),growth_rate(first_movers,critical_point(u)))* -> . % 0.57/0.80 12[0:Inp] environment(u) || in_environment(u,critical_point(u)) -> subpopulations(first_movers,efficient_producers,u,critical_point(u))*. % 0.57/0.80 13[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v) -> subpopulations(efficient_producers,first_movers,u,v)*. % 0.57/0.80 14[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v) -> greater_or_equal(v,appear(efficient_producers,u))*. % 0.57/0.80 15[0:Inp] environment(u) || in_environment(u,appear(efficient_producers,u)) -> subpopulations(first_movers,efficient_producers,u,appear(efficient_producers,u))*. % 0.57/0.80 16[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.57/0.80 18[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.57/0.80 20[0:Inp] environment(u) || subpopulations(first_movers,efficient_producers,u,v)*+ -> decreases(difference(founding_rate(first_movers,v),founding_rate(efficient_producers,v)))*. % 0.57/0.80 21[0:Inp] environment(u) || decreases(difference(disbanding_rate(first_movers,v),disbanding_rate(efficient_producers,v)))*+ subpopulations(first_movers,efficient_producers,u,v)* -> . % 0.57/0.80 23[0:Inp] environment(u) || greater(growth_rate(v,w),growth_rate(x,w))*+ subpopulations(x,v,u,w)* -> selection_favors(v,x,w). % 0.57/0.80 24[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.57/0.80 27[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.57/0.80 28[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.57/0.80 29[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.57/0.80 30[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.57/0.80 37[0:Res:1.0,23.0] || greater(growth_rate(u,v),growth_rate(w,v))* subpopulations(w,u,skc3,v) -> selection_favors(u,w,v). % 0.57/0.80 41[0:Res:1.0,15.0] || in_environment(skc3,appear(efficient_producers,skc3)) -> subpopulations(first_movers,efficient_producers,skc3,appear(efficient_producers,skc3))*. % 0.57/0.80 44[0:Res:1.0,14.0] || subpopulations(first_movers,efficient_producers,skc3,u) -> greater_or_equal(u,appear(efficient_producers,skc3))*. % 0.57/0.80 45[0:Res:1.0,11.0] || greater(growth_rate(efficient_producers,critical_point(skc3)),growth_rate(first_movers,critical_point(skc3)))* -> . % 0.57/0.80 48[0:Res:3.0,7.0] || -> greater_or_equal(critical_point(skc3),skc2)*. % 0.57/0.80 51[0:Res:2.0,24.2] environment(skc3) || greater(critical_point(skc3),u) greater_or_equal(u,appear(efficient_producers,skc3))* -> in_environment(skc3,u). % 0.57/0.80 52[0:Res:2.0,12.1] environment(skc3) || -> subpopulations(first_movers,efficient_producers,skc3,critical_point(skc3))*. % 0.57/0.80 58[0:Res:4.0,24.3] environment(skc3) || greater(critical_point(skc3),skc2) in_environment(skc3,critical_point(skc3))* -> in_environment(skc3,skc2). % 0.57/0.80 59[0:Res:4.0,30.2] environment(skc3) || in_environment(skc3,u) decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2))) greater(u,skc2) greater_or_equal(difference(growth_rate(first_movers,u),growth_rate(efficient_producers,u)),zero)* -> greater(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)),zero). % 0.57/0.80 60[0:Res:4.0,10.0] || -> greater(skc2,appear(efficient_producers,skc3))* equal(appear(efficient_producers,skc3),skc2). % 0.57/0.80 61[0:Res:4.0,29.3] environment(u) || greater_or_equal(v,skc2) subpopulations(first_movers,efficient_producers,u,v)* subpopulations(first_movers,efficient_producers,u,appear(efficient_producers,skc3))*+ -> subpopulations(first_movers,efficient_producers,u,skc2). % 0.57/0.80 65[0:MRR:52.0,1.0] || -> subpopulations(first_movers,efficient_producers,skc3,critical_point(skc3))*. % 0.57/0.80 66[0:MRR:58.0,58.1,58.2,1.0,3.0,2.0] || -> in_environment(skc3,skc2)*. % 0.57/0.80 67[0:MRR:51.0,1.0] || greater_or_equal(u,appear(efficient_producers,skc3))* greater(critical_point(skc3),u) -> in_environment(skc3,u). % 0.57/0.80 70[0:MRR:59.0,1.0] || decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2))) greater(u,skc2) in_environment(skc3,u) greater_or_equal(difference(growth_rate(first_movers,u),growth_rate(efficient_producers,u)),zero)* -> greater(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)),zero). % 0.57/0.80 71[1:Spt:60.1] || -> equal(appear(efficient_producers,skc3),skc2)**. % 0.57/0.80 80[1:Rew:71.0,41.0] || in_environment(skc3,skc2) -> subpopulations(first_movers,efficient_producers,skc3,appear(efficient_producers,skc3))*. % 0.57/0.80 81[1:Rew:71.0,80.1] || in_environment(skc3,skc2) -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.57/0.80 82[1:MRR:81.0,66.0] || -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.57/0.80 128[1:Res:82.0,20.1] environment(skc3) || -> decreases(difference(founding_rate(first_movers,skc2),founding_rate(efficient_producers,skc2)))*. % 0.57/0.80 132[1:SSi:128.0,1.0] || -> decreases(difference(founding_rate(first_movers,skc2),founding_rate(efficient_producers,skc2)))*. % 0.57/0.80 226[1:Res:132.0,27.0] || -> decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2))) decreases(difference(disbanding_rate(first_movers,skc2),disbanding_rate(efficient_producers,skc2)))*. % 0.57/0.80 234[1:Res:226.1,21.1] environment(u) || subpopulations(first_movers,efficient_producers,u,skc2)*+ -> decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)))*. % 0.57/0.80 235[1:Res:82.0,234.1] environment(skc3) || -> decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)))*. % 0.57/0.80 236[1:SSi:235.0,1.0] || -> decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)))*. % 0.57/0.80 237[1:MRR:70.0,236.0] || greater(u,skc2) in_environment(skc3,u) greater_or_equal(difference(growth_rate(first_movers,u),growth_rate(efficient_producers,u)),zero)* -> greater(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)),zero). % 0.57/0.80 239[0:Res:65.0,28.1] environment(skc3) || -> greater(zero,difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3)))) greater_or_equal(difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3))),zero)*. % 0.57/0.80 243[0:SSi:239.0,1.0] || -> greater(zero,difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3)))) greater_or_equal(difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3))),zero)*. % 0.57/0.80 256[0:Res:65.0,29.3] environment(skc3) || greater_or_equal(critical_point(skc3),u) greater_or_equal(u,v)* subpopulations(first_movers,efficient_producers,skc3,v)* -> subpopulations(first_movers,efficient_producers,skc3,u)*. % 0.57/0.80 260[0:SSi:256.0,1.0] || greater_or_equal(critical_point(skc3),u) greater_or_equal(u,v)* subpopulations(first_movers,efficient_producers,skc3,v)*+ -> subpopulations(first_movers,efficient_producers,skc3,u)*. % 0.57/0.80 350[0:Res:15.2,260.2] environment(skc3) || in_environment(skc3,appear(efficient_producers,skc3)) greater_or_equal(critical_point(skc3),u) greater_or_equal(u,appear(efficient_producers,skc3))* -> subpopulations(first_movers,efficient_producers,skc3,u). % 0.57/0.80 488[1:Res:243.1,237.2] || greater(critical_point(skc3),skc2) in_environment(skc3,critical_point(skc3)) -> greater(zero,difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3))))* greater(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)),zero). % 0.57/0.80 489[1:MRR:488.0,488.1,3.0,2.0] || -> greater(zero,difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3))))* greater(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)),zero). % 0.57/0.80 490[2:Spt:489.0] || -> greater(zero,difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3))))*. % 0.57/0.80 492[2:Res:490.0,16.0] || -> greater(growth_rate(efficient_producers,critical_point(skc3)),growth_rate(first_movers,critical_point(skc3)))*. % 0.57/0.80 494[2:MRR:492.0,45.0] || -> . % 0.57/0.80 495[2:Spt:494.0,489.0,490.0] || greater(zero,difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3))))* -> . % 0.57/0.80 496[2:Spt:494.0,489.1] || -> greater(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)),zero)*. % 0.57/0.80 503[2:Res:496.0,18.0] || -> greater(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2))*. % 0.57/0.80 507[2:Res:503.0,37.0] || subpopulations(efficient_producers,first_movers,skc3,skc2)* -> selection_favors(first_movers,efficient_producers,skc2). % 0.57/0.80 510[2:MRR:507.1,5.0] || subpopulations(efficient_producers,first_movers,skc3,skc2)* -> . % 0.57/0.80 512[2:Res:13.2,510.0] environment(skc3) || subpopulations(first_movers,efficient_producers,skc3,skc2)* -> . % 0.57/0.80 514[2:SSi:512.0,1.0] || subpopulations(first_movers,efficient_producers,skc3,skc2)* -> . % 0.57/0.80 515[2:MRR:514.0,82.0] || -> . % 0.57/0.80 516[1:Spt:515.0,60.1,71.0] || equal(appear(efficient_producers,skc3),skc2)** -> . % 0.57/0.80 517[1:Spt:515.0,60.0] || -> greater(skc2,appear(efficient_producers,skc3))*. % 0.57/0.80 519[0:SSi:350.0,1.0] || in_environment(skc3,appear(efficient_producers,skc3)) greater_or_equal(critical_point(skc3),u) greater_or_equal(u,appear(efficient_producers,skc3))* -> subpopulations(first_movers,efficient_producers,skc3,u). % 0.57/0.80 529[0:Res:44.1,10.0] || subpopulations(first_movers,efficient_producers,skc3,u) -> equal(u,appear(efficient_producers,skc3)) greater(u,appear(efficient_producers,skc3))*. % 0.57/0.80 547[0:Res:8.1,67.0] || equal(u,appear(efficient_producers,skc3)) greater(critical_point(skc3),u)* -> in_environment(skc3,u). % 0.57/0.80 574[0:Res:529.2,547.1] || subpopulations(first_movers,efficient_producers,skc3,critical_point(skc3))* equal(appear(efficient_producers,skc3),appear(efficient_producers,skc3)) -> equal(appear(efficient_producers,skc3),critical_point(skc3)) in_environment(skc3,appear(efficient_producers,skc3)). % 0.57/0.80 581[0:Obv:574.1] || subpopulations(first_movers,efficient_producers,skc3,critical_point(skc3))* -> equal(appear(efficient_producers,skc3),critical_point(skc3)) in_environment(skc3,appear(efficient_producers,skc3)). % 0.57/0.80 582[0:MRR:581.0,65.0] || -> equal(appear(efficient_producers,skc3),critical_point(skc3)) in_environment(skc3,appear(efficient_producers,skc3))*. % 0.57/0.80 588[2:Spt:582.0] || -> equal(appear(efficient_producers,skc3),critical_point(skc3))**. % 0.57/0.80 610[2:Rew:588.0,61.3] environment(u) || greater_or_equal(v,skc2) subpopulations(first_movers,efficient_producers,u,v)* subpopulations(first_movers,efficient_producers,u,critical_point(skc3))*+ -> subpopulations(first_movers,efficient_producers,u,skc2). % 0.57/0.80 693[2:Res:65.0,610.3] environment(skc3) || greater_or_equal(u,skc2) subpopulations(first_movers,efficient_producers,skc3,u)* -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.57/0.80 696[2:SSi:693.0,1.0] || greater_or_equal(u,skc2) subpopulations(first_movers,efficient_producers,skc3,u)*+ -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.57/0.80 699[2:Res:65.0,696.1] || greater_or_equal(critical_point(skc3),skc2) -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.57/0.80 703[2:MRR:699.0,48.0] || -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.57/0.80 714[2:Res:703.0,20.1] environment(skc3) || -> decreases(difference(founding_rate(first_movers,skc2),founding_rate(efficient_producers,skc2)))*. % 0.57/0.80 717[2:SSi:714.0,1.0] || -> decreases(difference(founding_rate(first_movers,skc2),founding_rate(efficient_producers,skc2)))*. % 0.57/0.80 733[2:Res:717.0,27.0] || -> decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2))) decreases(difference(disbanding_rate(first_movers,skc2),disbanding_rate(efficient_producers,skc2)))*. % 0.57/0.80 783[2:Res:733.1,21.1] environment(u) || subpopulations(first_movers,efficient_producers,u,skc2)*+ -> decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)))*. % 0.57/0.80 786[2:Res:703.0,783.1] environment(skc3) || -> decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)))*. % 0.57/0.80 787[2:SSi:786.0,1.0] || -> decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)))*. % 0.57/0.80 788[2:MRR:70.0,787.0] || greater(u,skc2) in_environment(skc3,u) greater_or_equal(difference(growth_rate(first_movers,u),growth_rate(efficient_producers,u)),zero)* -> greater(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)),zero). % 0.57/0.80 1134[3:Spt:243.0] || -> greater(zero,difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3))))*. % 0.57/0.80 1137[3:Res:1134.0,16.0] || -> greater(growth_rate(efficient_producers,critical_point(skc3)),growth_rate(first_movers,critical_point(skc3)))*. % 0.57/0.80 1139[3:MRR:1137.0,45.0] || -> . % 0.57/0.80 1140[3:Spt:1139.0,243.0,1134.0] || greater(zero,difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3))))* -> . % 0.57/0.80 1141[3:Spt:1139.0,243.1] || -> greater_or_equal(difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3))),zero)*. % 0.57/0.80 1154[3:Res:1141.0,788.2] || greater(critical_point(skc3),skc2) in_environment(skc3,critical_point(skc3)) -> greater(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)),zero)*. % 0.57/0.80 1155[3:MRR:1154.0,1154.1,3.0,2.0] || -> greater(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)),zero)*. % 0.57/0.80 1159[3:Res:1155.0,18.0] || -> greater(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2))*. % 0.57/0.80 1165[3:Res:1159.0,37.0] || subpopulations(efficient_producers,first_movers,skc3,skc2)* -> selection_favors(first_movers,efficient_producers,skc2). % 0.57/0.80 1168[3:MRR:1165.1,5.0] || subpopulations(efficient_producers,first_movers,skc3,skc2)* -> . % 0.57/0.80 1170[3:Res:13.2,1168.0] environment(skc3) || subpopulations(first_movers,efficient_producers,skc3,skc2)* -> . % 0.57/0.80 1172[3:SSi:1170.0,1.0] || subpopulations(first_movers,efficient_producers,skc3,skc2)* -> . % 0.57/0.80 1173[3:MRR:1172.0,703.0] || -> . % 0.57/0.80 1174[2:Spt:1173.0,582.0,588.0] || equal(appear(efficient_producers,skc3),critical_point(skc3))** -> . % 0.57/0.80 1175[2:Spt:1173.0,582.1] || -> in_environment(skc3,appear(efficient_producers,skc3))*. % 0.57/0.80 1178[2:MRR:519.0,1175.0] || greater_or_equal(critical_point(skc3),u) greater_or_equal(u,appear(efficient_producers,skc3))* -> subpopulations(first_movers,efficient_producers,skc3,u). % 0.57/0.82 1247[2:Res:4.0,1178.1] || greater_or_equal(critical_point(skc3),skc2) -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.57/0.82 1249[2:MRR:1247.0,48.0] || -> subpopulations(first_movers,efficient_producers,skc3,skc2)*. % 0.57/0.82 1262[2:Res:1249.0,20.1] environment(skc3) || -> decreases(difference(founding_rate(first_movers,skc2),founding_rate(efficient_producers,skc2)))*. % 0.57/0.82 1265[2:SSi:1262.0,1.0] || -> decreases(difference(founding_rate(first_movers,skc2),founding_rate(efficient_producers,skc2)))*. % 0.57/0.82 1268[2:Res:1265.0,27.0] || -> decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2))) decreases(difference(disbanding_rate(first_movers,skc2),disbanding_rate(efficient_producers,skc2)))*. % 0.57/0.82 1297[2:Res:1268.1,21.1] environment(u) || subpopulations(first_movers,efficient_producers,u,skc2)*+ -> decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)))*. % 0.57/0.82 1325[2:Res:1249.0,1297.1] environment(skc3) || -> decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)))*. % 0.57/0.82 1326[2:SSi:1325.0,1.0] || -> decreases(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)))*. % 0.57/0.82 1327[2:MRR:70.0,1326.0] || greater(u,skc2) in_environment(skc3,u) greater_or_equal(difference(growth_rate(first_movers,u),growth_rate(efficient_producers,u)),zero)* -> greater(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)),zero). % 0.57/0.82 1442[3:Spt:243.0] || -> greater(zero,difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3))))*. % 0.57/0.82 1444[3:Res:1442.0,16.0] || -> greater(growth_rate(efficient_producers,critical_point(skc3)),growth_rate(first_movers,critical_point(skc3)))*. % 0.57/0.82 1446[3:MRR:1444.0,45.0] || -> . % 0.57/0.82 1447[3:Spt:1446.0,243.0,1442.0] || greater(zero,difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3))))* -> . % 0.57/0.82 1448[3:Spt:1446.0,243.1] || -> greater_or_equal(difference(growth_rate(first_movers,critical_point(skc3)),growth_rate(efficient_producers,critical_point(skc3))),zero)*. % 0.57/0.82 1458[3:Res:1448.0,1327.2] || greater(critical_point(skc3),skc2) in_environment(skc3,critical_point(skc3)) -> greater(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)),zero)*. % 0.57/0.82 1459[3:MRR:1458.0,1458.1,3.0,2.0] || -> greater(difference(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2)),zero)*. % 0.57/0.82 1462[3:Res:1459.0,18.0] || -> greater(growth_rate(first_movers,skc2),growth_rate(efficient_producers,skc2))*. % 0.57/0.82 1467[3:Res:1462.0,37.0] || subpopulations(efficient_producers,first_movers,skc3,skc2)* -> selection_favors(first_movers,efficient_producers,skc2). % 0.57/0.82 1470[3:MRR:1467.1,5.0] || subpopulations(efficient_producers,first_movers,skc3,skc2)* -> . % 0.57/0.82 1472[3:Res:13.2,1470.0] environment(skc3) || subpopulations(first_movers,efficient_producers,skc3,skc2)* -> . % 0.57/0.82 1474[3:SSi:1472.0,1.0] || subpopulations(first_movers,efficient_producers,skc3,skc2)* -> . % 0.57/0.82 1475[3:MRR:1474.0,1249.0] || -> . % 0.57/0.82 % SZS output end Refutation % 0.57/0.82 Formulae used in the proof : prove_t3 mp_greater_or_equal d1 mp_critical_point_means_FM_and_EP mp_symmetry_of_subpopulations mp_FM_and_EP_members_EP_appeared mp_FM_and_EP_when_EP_appears mp_negative_growth_rate_difference mp_positive_growth_rate_difference a12 l3 mp1_high_growth_rates mp_critical_time_points mp_difference_between_founding_rates mp_relationship_of_growth_rates a10 mp_decreasing_function % 0.57/0.82 %------------------------------------------------------------------------------