%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : MGT039-2 : TPTP v9.3.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n009.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:54 AM UTC 2026 % Result : Unsatisfiable 4.35s 4.68s % Output : Refutation 4.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT039-2 : TPTP v9.3.0. Released v2.4.0. % 0.00/0.03 % Command : run_spass %d %s % 0.07/0.34 % Computer : n009.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Mon Sep 7 12:56:22 UTC 2026 % 0.07/0.34 % CPUTime : % 4.35/4.68 % 4.35/4.68 SPASS V 3.9 % 4.35/4.68 SPASS beiseite: Proof found. % 4.35/4.68 % SZS status Theorem % 4.35/4.68 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 4.35/4.68 SPASS derived 2186 clauses, backtracked 212 clauses, performed 21 splits and kept 1718 clauses. % 4.35/4.68 SPASS allocated 78860 KBytes. % 4.35/4.68 SPASS spent 0:00:04.33 on the problem. % 4.35/4.68 0:00:00.06 for the input. % 4.35/4.68 0:00:00.00 for the FLOTTER CNF translation. % 4.35/4.68 0:00:00.12 for inferences. % 4.35/4.68 0:00:00.04 for the backtracking. % 4.35/4.68 0:00:04.04 for the reduction. % 4.35/4.68 % 4.35/4.68 % 4.35/4.68 Here is a proof with depth 15, length 183 : % 4.35/4.68 % SZS output start Refutation % 4.35/4.68 1[0:Inp] environment(u) || greater(growth_rate(v,w),growth_rate(x,w)) subpopulations(x,v,u,w)* -> selection_favors(v,x,w). % 4.35/4.68 2[0:Inp] environment(u) || equal(cardinality_at_time(v,w),zero) greater(cardinality_at_time(x,w),zero)+ subpopulation(v,u,w)* subpopulation(x,u,w)* -> selection_favors(x,v,w)*. % 4.35/4.68 3[0:Inp] observational_period(u) || propagation_strategy(first_movers) propagation_strategy(efficient_producers) -> environment(sk1(u)) selection_favors(efficient_producers,first_movers,u)*. % 4.35/4.68 4[0:Inp] observational_period(u) || propagation_strategy(first_movers) propagation_strategy(efficient_producers) -> in_environment(u,sk1(u))* selection_favors(efficient_producers,first_movers,u)*. % 4.35/4.68 5[0:Inp] observational_period(u) || propagation_strategy(first_movers) propagation_strategy(efficient_producers) selection_favors(efficient_producers,first_movers,end_time(sk1(u)))* -> selection_favors(efficient_producers,first_movers,u). % 4.35/4.68 6[0:Inp] environment(u) slow_change(v) observational_period(v) || in_environment(v,u) -> in_environment(u,sk2(u,v))*. % 4.35/4.68 7[0:Inp] environment(u) slow_change(v) observational_period(v) || in_environment(v,u) -> greater(sk2(u,v),critical_point(u))*l. % 4.35/4.68 8[0:Inp] || -> propagation_strategy(first_movers)*. % 4.35/4.68 9[0:Inp] || -> propagation_strategy(efficient_producers)*. % 4.35/4.68 10[0:Inp] environment(u) || greater_or_equal(v,start_time(u))*+ greater_or_equal(end_time(u),v)* -> in_environment(u,v). % 4.35/4.68 11[0:Inp] environment(u) || in_environment(u,v) -> greater_or_equal(end_time(u),v)*. % 4.35/4.68 12[0:Inp] environment(u) || in_environment(u,v) greater(cardinality_at_time(efficient_producers,v),zero) greater(cardinality_at_time(first_movers,v),zero) -> subpopulations(first_movers,efficient_producers,u,v)*. % 4.35/4.68 13[0:Inp] environment(u) || in_environment(u,v)*+ -> greater_or_equal(cardinality_at_time(first_movers,v),zero)*. % 4.35/4.68 14[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(first_movers,u,v)*. % 4.35/4.68 15[0:Inp] environment(u) || in_environment(u,v) -> subpopulation(efficient_producers,u,v)*. % 4.35/4.68 16[0:Inp] environment(u) || -> greater_or_equal(critical_point(u),appear(efficient_producers,u))*. % 4.35/4.68 17[0:Inp] environment(u) || -> greater_or_equal(critical_point(u),start_time(u))*. % 4.35/4.68 18[0:Inp] || greater(u,v)* greater(v,w)* -> greater(u,w)*. % 4.35/4.68 20[0:Inp] || greater_or_equal(u,v)* -> equal(u,v) greater(u,v). % 4.35/4.68 21[0:Inp] || greater(u,v) -> greater_or_equal(u,v)*. % 4.35/4.68 22[0:Inp] || equal(u,v) -> greater_or_equal(u,v)*. % 4.35/4.68 24[0:Inp] environment(u) || greater(v,w)*+ equal(w,critical_point(u))* subpopulations(first_movers,efficient_producers,u,v)* -> greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v)). % 4.35/4.68 25[0:Inp] environment(u) || in_environment(u,v) greater_or_equal(v,appear(efficient_producers,u))* -> greater(cardinality_at_time(efficient_producers,v),zero). % 4.35/4.68 26[0:Inp] || -> observational_period(sk3)*. % 4.35/4.68 27[0:Inp] || -> slow_change(sk3)*. % 4.35/4.68 28[0:Inp] || selection_favors(efficient_producers,first_movers,sk3)* -> . % 4.35/4.68 29[0:MRR:3.1,3.2,8.0,9.0] observational_period(u) || -> environment(sk1(u)) selection_favors(efficient_producers,first_movers,u)*. % 4.35/4.68 30[0:MRR:4.1,4.2,8.0,9.0] observational_period(u) || -> in_environment(u,sk1(u))* selection_favors(efficient_producers,first_movers,u)*. % 4.35/4.68 31[0:MRR:5.1,5.2,8.0,9.0] observational_period(u) || selection_favors(efficient_producers,first_movers,end_time(sk1(u)))* -> selection_favors(efficient_producers,first_movers,u). % 4.35/4.68 33[0:Res:27.0,6.1] observational_period(sk3) environment(u) || in_environment(sk3,u) -> in_environment(u,sk2(u,sk3))*. % 4.35/4.68 34[0:Res:26.0,7.0] slow_change(sk3) environment(u) || in_environment(sk3,u) -> greater(sk2(u,sk3),critical_point(u))*l. % 4.35/4.68 39[0:Res:31.2,28.0] observational_period(sk3) || selection_favors(efficient_producers,first_movers,end_time(sk1(sk3)))* -> . % 4.35/4.68 40[0:Res:30.2,28.0] observational_period(sk3) || -> in_environment(sk3,sk1(sk3))*. % 4.35/4.68 41[0:Res:29.2,28.0] observational_period(sk3) || -> environment(sk1(sk3))*. % 4.35/4.68 44[0:MRR:41.0,26.0] || -> environment(sk1(sk3))*. % 4.35/4.68 45[0:MRR:40.0,26.0] || -> in_environment(sk3,sk1(sk3))*. % 4.35/4.68 46[0:MRR:39.0,26.0] || selection_favors(efficient_producers,first_movers,end_time(sk1(sk3)))* -> . % 4.35/4.68 47[0:MRR:33.0,26.0] environment(u) || in_environment(sk3,u) -> in_environment(u,sk2(u,sk3))*. % 4.35/4.68 48[0:MRR:34.0,27.0] environment(u) || in_environment(sk3,u) -> greater(sk2(u,sk3),critical_point(u))*l. % 4.35/4.68 59[0:Res:11.2,20.0] environment(u) || in_environment(u,v)* -> equal(end_time(u),v) greater(end_time(u),v). % 4.35/4.68 60[0:Res:17.1,20.0] environment(u) || -> equal(start_time(u),critical_point(u)) greater(critical_point(u),start_time(u))*r. % 4.35/4.68 61[0:Res:16.1,20.0] environment(u) || -> equal(appear(efficient_producers,u),critical_point(u)) greater(critical_point(u),appear(efficient_producers,u))*r. % 4.35/4.69 63[0:Res:21.1,10.1] environment(u) || greater(v,start_time(u)) greater_or_equal(end_time(u),v)* -> in_environment(u,v). % 4.35/4.69 64[0:Res:22.1,10.1] environment(u) || equal(v,start_time(u)) greater_or_equal(end_time(u),v)* -> in_environment(u,v). % 4.35/4.69 65[0:Res:11.2,10.1] environment(u) environment(v) || in_environment(u,start_time(v)) greater_or_equal(end_time(v),end_time(u))* -> in_environment(v,end_time(u)). % 4.35/4.69 66[0:Res:17.1,10.1] environment(u) environment(u) || greater_or_equal(end_time(u),critical_point(u))* -> in_environment(u,critical_point(u)). % 4.35/4.69 67[0:Obv:66.0] environment(u) || greater_or_equal(end_time(u),critical_point(u))* -> in_environment(u,critical_point(u)). % 4.35/4.69 68[0:Res:21.1,67.1] environment(u) || greater(end_time(u),critical_point(u)) -> in_environment(u,critical_point(u))*. % 4.35/4.69 77[0:Res:21.1,64.2] environment(u) || greater(end_time(u),v) equal(v,start_time(u)) -> in_environment(u,v)*. % 4.35/4.69 86[0:Res:21.1,25.2] environment(u) || greater(v,appear(efficient_producers,u))*+ in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l. % 4.35/4.69 101[0:Res:47.2,59.1] environment(u) environment(u) || in_environment(sk3,u) -> equal(sk2(u,sk3),end_time(u)) greater(end_time(u),sk2(u,sk3))*r. % 4.35/4.69 105[0:Obv:101.0] environment(u) || in_environment(sk3,u) -> equal(sk2(u,sk3),end_time(u)) greater(end_time(u),sk2(u,sk3))*r. % 4.35/4.69 109[0:Res:22.1,63.2] environment(u) || equal(end_time(u),v) greater(v,start_time(u)) -> in_environment(u,v)*. % 4.35/4.69 121[0:Res:77.3,13.1] environment(u) environment(u) || greater(end_time(u),v)* equal(v,start_time(u))* -> greater_or_equal(cardinality_at_time(first_movers,v),zero)*. % 4.35/4.69 123[0:Obv:121.0] environment(u) || greater(end_time(u),v)*+ equal(v,start_time(u))* -> greater_or_equal(cardinality_at_time(first_movers,v),zero)*. % 4.35/4.69 126[0:Res:109.3,13.1] environment(u) environment(u) || equal(end_time(u),v) greater(v,start_time(u))* -> greater_or_equal(cardinality_at_time(first_movers,v),zero)*. % 4.35/4.69 128[0:Obv:126.0] environment(u) || equal(end_time(u),v) greater(v,start_time(u))*+ -> greater_or_equal(cardinality_at_time(first_movers,v),zero)*. % 4.35/4.69 131[0:Res:22.1,65.3] environment(u) environment(v) || equal(end_time(v),end_time(u))+ in_environment(u,start_time(v))* -> in_environment(v,end_time(u))*. % 4.35/4.69 135[0:EqR:131.2] environment(u) environment(u) || in_environment(u,start_time(u))* -> in_environment(u,end_time(u)). % 4.35/4.69 136[0:Obv:135.0] environment(u) || in_environment(u,start_time(u))* -> in_environment(u,end_time(u)). % 4.35/4.69 138[0:Res:77.3,136.1] environment(u) environment(u) || greater(end_time(u),start_time(u)) equal(start_time(u),start_time(u)) -> in_environment(u,end_time(u))*. % 4.35/4.69 141[0:Obv:138.3] environment(u) || greater(end_time(u),start_time(u)) -> in_environment(u,end_time(u))*. % 4.35/4.69 150[0:Res:12.4,1.2] environment(u) environment(u) || in_environment(u,v)* greater(cardinality_at_time(efficient_producers,v),zero) greater(cardinality_at_time(first_movers,v),zero) greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v)) -> selection_favors(efficient_producers,first_movers,v)*. % 4.35/4.69 151[0:Obv:150.0] environment(u) || in_environment(u,v)* greater(cardinality_at_time(efficient_producers,v),zero) greater(cardinality_at_time(first_movers,v),zero) greater(growth_rate(efficient_producers,v),growth_rate(first_movers,v))+ -> selection_favors(efficient_producers,first_movers,v)*. % 4.35/4.69 161[0:NCh:18.2,18.1,123.1,60.2] environment(u) environment(v) || greater(end_time(u),critical_point(v))+ equal(start_time(v),start_time(u))* -> greater_or_equal(cardinality_at_time(first_movers,start_time(v)),zero)* equal(start_time(v),critical_point(v)). % 4.35/4.69 176[0:NCh:18.2,18.1,128.2,60.2] environment(u) environment(u) || equal(end_time(u),v) greater(v,critical_point(u))* -> greater_or_equal(cardinality_at_time(first_movers,v),zero)* equal(start_time(u),critical_point(u))**. % 4.35/4.69 180[0:Obv:176.0] environment(u) || equal(end_time(u),v) greater(v,critical_point(u))*+ -> greater_or_equal(cardinality_at_time(first_movers,v),zero)* equal(start_time(u),critical_point(u))**. % 4.35/4.69 184[0:OCh:18.1,18.0,105.3,48.2] environment(u) environment(u) || in_environment(sk3,u) in_environment(sk3,u) -> equal(sk2(u,sk3),end_time(u))** greater(end_time(u),critical_point(u)). % 4.35/4.69 188[0:Obv:184.2] environment(u) || in_environment(sk3,u) -> equal(sk2(u,sk3),end_time(u))** greater(end_time(u),critical_point(u)). % 4.35/4.69 213[0:SpR:188.2,48.2] environment(u) environment(u) || in_environment(sk3,u)* in_environment(sk3,u)* -> greater(end_time(u),critical_point(u)) greater(end_time(u),critical_point(u)). % 4.35/4.69 222[0:Obv:213.4] environment(u) || in_environment(sk3,u)* -> greater(end_time(u),critical_point(u)). % 4.35/4.69 226[0:Res:45.0,222.1] environment(sk1(sk3)) || -> greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))*r. % 4.35/4.69 236[0:SSi:226.0,44.0] || -> greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))*r. % 4.35/4.69 238[0:Res:236.0,24.1] environment(u) || equal(critical_point(sk1(sk3)),critical_point(u)) subpopulations(first_movers,efficient_producers,u,end_time(sk1(sk3)))* -> greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3)))). % 4.35/4.69 252[0:NCh:18.2,18.1,86.1,61.2] environment(u) environment(u) || greater(v,critical_point(u)) in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l equal(appear(efficient_producers,u),critical_point(u))**. % 4.35/4.69 256[0:Obv:252.0] environment(u) || greater(v,critical_point(u))+ in_environment(u,v)* -> greater(cardinality_at_time(efficient_producers,v),zero)*l equal(appear(efficient_producers,u),critical_point(u))**. % 4.35/4.69 439[0:Res:236.0,180.2] environment(sk1(sk3)) || equal(end_time(sk1(sk3)),end_time(sk1(sk3))) -> greater_or_equal(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)* equal(start_time(sk1(sk3)),critical_point(sk1(sk3))). % 4.35/4.69 458[0:Obv:439.1] environment(sk1(sk3)) || -> greater_or_equal(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)* equal(start_time(sk1(sk3)),critical_point(sk1(sk3))). % 4.35/4.69 459[0:SSi:458.0,44.0] || -> greater_or_equal(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)* equal(start_time(sk1(sk3)),critical_point(sk1(sk3))). % 4.35/4.69 464[0:Res:459.0,20.0] || -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3))) equal(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero) greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)*l. % 4.35/4.69 651[0:Res:236.0,256.1] environment(sk1(sk3)) || in_environment(sk1(sk3),end_time(sk1(sk3)))* -> greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero) equal(appear(efficient_producers,sk1(sk3)),critical_point(sk1(sk3))). % 4.35/4.69 681[0:NCh:18.2,18.1,256.1,236.0] environment(sk1(sk3)) || equal(u,end_time(sk1(sk3))) in_environment(sk1(sk3),u)* -> greater(cardinality_at_time(efficient_producers,u),zero) equal(appear(efficient_producers,sk1(sk3)),critical_point(sk1(sk3)))**. % 4.35/4.69 682[0:SSi:651.0,44.0] || in_environment(sk1(sk3),end_time(sk1(sk3)))* -> greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero) equal(appear(efficient_producers,sk1(sk3)),critical_point(sk1(sk3))). % 4.35/4.69 683[0:SSi:681.0,44.0] || equal(u,end_time(sk1(sk3)))+ in_environment(sk1(sk3),u)* -> greater(cardinality_at_time(efficient_producers,u),zero) equal(appear(efficient_producers,sk1(sk3)),critical_point(sk1(sk3)))**. % 4.35/4.69 708[1:Spt:682.1] || -> greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)*l. % 4.35/4.69 709[1:Res:708.0,2.2] environment(u) || equal(cardinality_at_time(v,end_time(sk1(sk3))),zero)+ subpopulation(v,u,end_time(sk1(sk3)))* subpopulation(efficient_producers,u,end_time(sk1(sk3)))* -> selection_favors(efficient_producers,v,end_time(sk1(sk3)))*. % 4.35/4.69 995[0:Res:12.4,238.2] environment(u) environment(u) || in_environment(u,end_time(sk1(sk3)))* greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)*l greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero) equal(critical_point(sk1(sk3)),critical_point(u)) -> greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3)))). % 4.35/4.69 996[0:Obv:995.0] environment(u) || in_environment(u,end_time(sk1(sk3)))* greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)*l greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero) equal(critical_point(sk1(sk3)),critical_point(u)) -> greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3)))). % 4.35/4.69 997[1:MRR:996.2,708.0] environment(u) || in_environment(u,end_time(sk1(sk3)))* greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)*l equal(critical_point(sk1(sk3)),critical_point(u)) -> greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3)))). % 4.35/4.69 1144[0:Res:236.0,161.2] environment(sk1(sk3)) environment(sk1(sk3)) || equal(start_time(sk1(sk3)),start_time(sk1(sk3))) -> greater_or_equal(cardinality_at_time(first_movers,start_time(sk1(sk3))),zero)* equal(start_time(sk1(sk3)),critical_point(sk1(sk3))). % 4.35/4.69 1147[0:Obv:1144.2] environment(sk1(sk3)) || -> greater_or_equal(cardinality_at_time(first_movers,start_time(sk1(sk3))),zero)* equal(start_time(sk1(sk3)),critical_point(sk1(sk3))). % 4.35/4.69 1148[0:SSi:1147.0,44.0] || -> greater_or_equal(cardinality_at_time(first_movers,start_time(sk1(sk3))),zero)* equal(start_time(sk1(sk3)),critical_point(sk1(sk3))). % 4.35/4.69 1149[2:Spt:1148.1] || -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 4.35/4.69 1202[2:SpL:1149.0,10.1] environment(sk1(sk3)) || greater_or_equal(u,critical_point(sk1(sk3)))* greater_or_equal(end_time(sk1(sk3)),u)* -> in_environment(sk1(sk3),u). % 4.35/4.69 1206[2:SpL:1149.0,136.1] environment(sk1(sk3)) || in_environment(sk1(sk3),critical_point(sk1(sk3)))* -> in_environment(sk1(sk3),end_time(sk1(sk3))). % 4.35/4.69 1211[2:SSi:1206.0,44.0] || in_environment(sk1(sk3),critical_point(sk1(sk3)))* -> in_environment(sk1(sk3),end_time(sk1(sk3))). % 4.35/4.69 1212[2:SSi:1202.0,44.0] || greater_or_equal(u,critical_point(sk1(sk3)))*+ greater_or_equal(end_time(sk1(sk3)),u)* -> in_environment(sk1(sk3),u). % 4.35/4.69 1222[2:Res:68.2,1211.0] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> in_environment(sk1(sk3),end_time(sk1(sk3)))*. % 4.35/4.69 1225[2:SSi:1222.0,44.0] || greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> in_environment(sk1(sk3),end_time(sk1(sk3)))*. % 4.35/4.69 1226[2:MRR:1225.0,236.0] || -> in_environment(sk1(sk3),end_time(sk1(sk3)))*. % 4.35/4.69 1228[2:Res:1226.0,13.1] environment(sk1(sk3)) || -> greater_or_equal(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)*. % 4.35/4.69 1232[2:SSi:1228.0,44.0] || -> greater_or_equal(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)*. % 4.35/4.69 1234[2:Res:1232.0,20.0] || -> equal(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero) greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)*l. % 4.35/4.69 1235[2:Res:21.1,1212.0] || greater(u,critical_point(sk1(sk3))) greater_or_equal(end_time(sk1(sk3)),u)* -> in_environment(sk1(sk3),u). % 4.35/4.69 1303[3:Spt:1234.0] || -> equal(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)**. % 4.35/4.69 1318[3:SpL:1303.0,709.1] environment(u) || equal(zero,zero) subpopulation(first_movers,u,end_time(sk1(sk3))) subpopulation(efficient_producers,u,end_time(sk1(sk3)))* -> selection_favors(efficient_producers,first_movers,end_time(sk1(sk3)))*. % 4.35/4.69 1321[3:Obv:1318.1] environment(u) || subpopulation(first_movers,u,end_time(sk1(sk3))) subpopulation(efficient_producers,u,end_time(sk1(sk3)))* -> selection_favors(efficient_producers,first_movers,end_time(sk1(sk3)))*. % 4.35/4.69 1322[3:MRR:1321.3,46.0] environment(u) || subpopulation(first_movers,u,end_time(sk1(sk3))) subpopulation(efficient_producers,u,end_time(sk1(sk3)))* -> . % 4.35/4.69 1326[3:Res:15.2,1322.2] environment(u) environment(u) || in_environment(u,end_time(sk1(sk3))) subpopulation(first_movers,u,end_time(sk1(sk3)))* -> . % 4.35/4.69 1327[3:Obv:1326.0] environment(u) || in_environment(u,end_time(sk1(sk3))) subpopulation(first_movers,u,end_time(sk1(sk3)))* -> . % 4.35/4.69 1328[3:MRR:1327.2,14.2] environment(u) || in_environment(u,end_time(sk1(sk3)))* -> . % 4.35/4.69 1335[3:Res:141.2,1328.1] environment(sk1(sk3)) environment(sk1(sk3)) || greater(end_time(sk1(sk3)),start_time(sk1(sk3)))*r -> . % 4.35/4.69 1347[3:Obv:1335.0] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),start_time(sk1(sk3)))*r -> . % 4.35/4.69 1348[3:Rew:1149.0,1347.1] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))*r -> . % 4.35/4.69 1349[3:SSi:1348.0,44.0] || greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))*r -> . % 4.35/4.69 1350[3:MRR:1349.0,236.0] || -> . % 4.35/4.69 1364[3:Spt:1350.0,1234.0,1303.0] || equal(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)** -> . % 4.35/4.69 1365[3:Spt:1350.0,1234.1] || -> greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)*l. % 4.35/4.69 1366[3:MRR:997.2,1365.0] environment(u) || in_environment(u,end_time(sk1(sk3)))* equal(critical_point(sk1(sk3)),critical_point(u))+ -> greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3))))*l. % 4.35/4.69 1417[2:Res:22.1,1235.1] || equal(end_time(sk1(sk3)),u) greater(u,critical_point(sk1(sk3))) -> in_environment(sk1(sk3),u)*. % 4.35/4.69 1821[3:EqR:1366.2] environment(sk1(sk3)) || in_environment(sk1(sk3),end_time(sk1(sk3)))* -> greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3)))). % 4.35/4.69 1822[3:SSi:1821.0,44.0] || in_environment(sk1(sk3),end_time(sk1(sk3)))* -> greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3)))). % 4.35/4.69 1823[3:MRR:1822.0,1226.0] || -> greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3))))*l. % 4.35/4.69 1826[3:Res:1823.0,151.4] environment(u) || in_environment(u,end_time(sk1(sk3)))* greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero) greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero) -> selection_favors(efficient_producers,first_movers,end_time(sk1(sk3)))*. % 4.35/4.69 1856[3:MRR:1826.2,1826.3,1826.4,708.0,1365.0,46.0] environment(u) || in_environment(u,end_time(sk1(sk3)))* -> . % 4.35/4.69 1867[3:Res:1417.2,1856.1] environment(sk1(sk3)) || equal(end_time(sk1(sk3)),end_time(sk1(sk3))) greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))*r -> . % 4.35/4.69 1882[3:Obv:1867.1] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))*r -> . % 4.35/4.69 1883[3:SSi:1882.0,44.0] || greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))*r -> . % 4.35/4.69 1884[3:MRR:1883.0,236.0] || -> . % 4.35/4.69 1900[2:Spt:1884.0,1148.1,1149.0] || equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))** -> . % 4.35/4.69 1901[2:Spt:1884.0,1148.0] || -> greater_or_equal(cardinality_at_time(first_movers,start_time(sk1(sk3))),zero)*. % 4.35/4.69 1903[2:MRR:464.0,1900.0] || -> equal(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero) greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)*l. % 4.35/4.69 1942[3:Spt:1903.0] || -> equal(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)**. % 4.35/4.69 1957[3:SpL:1942.0,709.1] environment(u) || equal(zero,zero) subpopulation(first_movers,u,end_time(sk1(sk3))) subpopulation(efficient_producers,u,end_time(sk1(sk3)))* -> selection_favors(efficient_producers,first_movers,end_time(sk1(sk3)))*. % 4.35/4.69 1960[3:Obv:1957.1] environment(u) || subpopulation(first_movers,u,end_time(sk1(sk3))) subpopulation(efficient_producers,u,end_time(sk1(sk3)))* -> selection_favors(efficient_producers,first_movers,end_time(sk1(sk3)))*. % 4.35/4.69 1961[3:MRR:1960.3,46.0] environment(u) || subpopulation(first_movers,u,end_time(sk1(sk3))) subpopulation(efficient_producers,u,end_time(sk1(sk3)))* -> . % 4.35/4.69 1963[3:Res:15.2,1961.2] environment(u) environment(u) || in_environment(u,end_time(sk1(sk3))) subpopulation(first_movers,u,end_time(sk1(sk3)))* -> . % 4.35/4.69 1964[3:Obv:1963.0] environment(u) || in_environment(u,end_time(sk1(sk3))) subpopulation(first_movers,u,end_time(sk1(sk3)))* -> . % 4.35/4.69 1965[3:MRR:1964.2,14.2] environment(u) || in_environment(u,end_time(sk1(sk3)))* -> . % 4.35/4.69 1972[3:Res:141.2,1965.1] environment(sk1(sk3)) environment(sk1(sk3)) || greater(end_time(sk1(sk3)),start_time(sk1(sk3)))*r -> . % 4.35/4.69 1979[3:Obv:1972.0] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),start_time(sk1(sk3)))*r -> . % 4.35/4.69 1980[3:SSi:1979.0,44.0] || greater(end_time(sk1(sk3)),start_time(sk1(sk3)))*r -> . % 4.35/4.69 2001[3:NCh:18.2,18.1,1980.0,60.2] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 4.35/4.69 2005[3:SSi:2001.0,44.0] || greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 4.35/4.69 2006[3:MRR:2005.0,2005.1,236.0,1900.0] || -> . % 4.35/4.69 2007[3:Spt:2006.0,1903.0,1942.0] || equal(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)** -> . % 4.35/4.69 2008[3:Spt:2006.0,1903.1] || -> greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero)*l. % 4.35/4.69 2020[3:MRR:997.2,2008.0] environment(u) || in_environment(u,end_time(sk1(sk3)))* equal(critical_point(sk1(sk3)),critical_point(u))+ -> greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3))))*l. % 4.35/4.69 2190[3:EqR:2020.2] environment(sk1(sk3)) || in_environment(sk1(sk3),end_time(sk1(sk3)))* -> greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3)))). % 4.35/4.69 2191[3:SSi:2190.0,44.0] || in_environment(sk1(sk3),end_time(sk1(sk3)))* -> greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3)))). % 4.35/4.69 2198[3:Res:141.2,2191.0] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),start_time(sk1(sk3))) -> greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3))))*l. % 4.35/4.69 2203[3:SSi:2198.0,44.0] || greater(end_time(sk1(sk3)),start_time(sk1(sk3))) -> greater(growth_rate(efficient_producers,end_time(sk1(sk3))),growth_rate(first_movers,end_time(sk1(sk3))))*l. % 4.35/4.69 2303[3:Res:2203.1,151.4] environment(u) || greater(end_time(sk1(sk3)),start_time(sk1(sk3))) in_environment(u,end_time(sk1(sk3)))* greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero) greater(cardinality_at_time(first_movers,end_time(sk1(sk3))),zero) -> selection_favors(efficient_producers,first_movers,end_time(sk1(sk3)))*. % 4.35/4.69 2333[3:MRR:2303.3,2303.4,2303.5,708.0,2008.0,46.0] environment(u) || greater(end_time(sk1(sk3)),start_time(sk1(sk3))) in_environment(u,end_time(sk1(sk3)))* -> . % 4.35/4.69 2381[3:Res:141.2,2333.2] environment(sk1(sk3)) environment(sk1(sk3)) || greater(end_time(sk1(sk3)),start_time(sk1(sk3)))*r greater(end_time(sk1(sk3)),start_time(sk1(sk3)))*r -> . % 4.35/4.69 2387[3:Obv:2381.2] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),start_time(sk1(sk3)))*r -> . % 4.35/4.69 2388[3:SSi:2387.0,44.0] || greater(end_time(sk1(sk3)),start_time(sk1(sk3)))*r -> . % 4.35/4.69 2397[3:NCh:18.2,18.1,2388.0,60.2] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 4.35/4.69 2401[3:SSi:2397.0,44.0] || greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 4.35/4.69 2402[3:MRR:2401.0,2401.1,236.0,1900.0] || -> . % 4.35/4.69 2403[1:Spt:2402.0,682.1,708.0] || greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)*l -> . % 4.35/4.69 2404[1:Spt:2402.0,682.0,682.2] || in_environment(sk1(sk3),end_time(sk1(sk3)))* -> equal(appear(efficient_producers,sk1(sk3)),critical_point(sk1(sk3))). % 4.35/4.69 2612[2:Spt:683.0,683.1,683.2] || equal(u,end_time(sk1(sk3))) in_environment(sk1(sk3),u)* -> greater(cardinality_at_time(efficient_producers,u),zero). % 4.35/4.69 2624[2:Res:141.2,2612.1] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),start_time(sk1(sk3))) equal(end_time(sk1(sk3)),end_time(sk1(sk3))) -> greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)*l. % 4.45/4.75 2636[2:Obv:2624.2] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),start_time(sk1(sk3))) -> greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)*l. % 4.45/4.75 2637[2:SSi:2636.0,44.0] || greater(end_time(sk1(sk3)),start_time(sk1(sk3))) -> greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)*l. % 4.45/4.75 2638[2:MRR:2637.1,2403.0] || greater(end_time(sk1(sk3)),start_time(sk1(sk3)))*r -> . % 4.45/4.75 2676[2:NCh:18.2,18.1,2638.0,60.2] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 4.45/4.75 2679[2:SSi:2676.0,44.0] || greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 4.45/4.75 2680[2:MRR:2679.0,236.0] || -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 4.45/4.75 2684[2:Rew:2680.0,2638.0] || greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))*r -> . % 4.45/4.75 2714[2:MRR:2684.0,236.0] || -> . % 4.45/4.75 2733[2:Spt:2714.0,683.3] || -> equal(appear(efficient_producers,sk1(sk3)),critical_point(sk1(sk3)))**. % 4.45/4.75 2745[2:SpL:2733.0,86.1] environment(sk1(sk3)) || greater(u,critical_point(sk1(sk3))) in_environment(sk1(sk3),u)* -> greater(cardinality_at_time(efficient_producers,u),zero). % 4.45/4.75 2761[2:SSi:2745.0,44.0] || greater(u,critical_point(sk1(sk3))) in_environment(sk1(sk3),u)* -> greater(cardinality_at_time(efficient_producers,u),zero). % 4.45/4.75 2905[2:Res:141.2,2761.1] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),start_time(sk1(sk3))) greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)*l. % 4.45/4.75 2914[2:SSi:2905.0,44.0] || greater(end_time(sk1(sk3)),start_time(sk1(sk3))) greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> greater(cardinality_at_time(efficient_producers,end_time(sk1(sk3))),zero)*l. % 4.45/4.75 2915[2:MRR:2914.1,2914.2,236.0,2403.0] || greater(end_time(sk1(sk3)),start_time(sk1(sk3)))*r -> . % 4.45/4.75 2927[2:NCh:18.2,18.1,2915.0,60.2] environment(sk1(sk3)) || greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 4.45/4.75 2929[2:SSi:2927.0,44.0] || greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 4.45/4.75 2930[2:MRR:2929.0,236.0] || -> equal(start_time(sk1(sk3)),critical_point(sk1(sk3)))**. % 4.45/4.75 2933[2:Rew:2930.0,2915.0] || greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))*r -> . % 4.45/4.75 2950[2:MRR:2933.0,236.0] || -> . % 4.45/4.75 % SZS output end Refutation % 4.45/4.75 Formulae used in the proof : mp1_high_growth_rates_33 mp2_favour_members_34 mp3_favoured_trategy_35 mp3_favoured_trategy_36 mp3_favoured_trategy_37 mp4_critical_point_38 mp4_critical_point_39 mp_organizational_sets1_40 mp_organizational_sets2_41 mp_time_in_environment_42 mp_environment_end_point_43 mp_contains_FM_and_EP_44 mp_first_movers_exist_45 mp_subpopulations_46 mp_subpopulations_47 mp_critical_point_after_EP_48 mp_time_of_critical_point_49 mp_greater_transitivity_50 mp_greater_or_equal_52 mp_greater_or_equal_53 mp_greater_or_equal_54 d1_56 t6_57 prove_t8_58 prove_t8_59 prove_t8_60 % 4.45/4.75 %------------------------------------------------------------------------------