%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT039+2 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 : Thu Sep 24 01:25:47 PM UTC 2026
% Result : Theorem 0.18s 0.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT039+2 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n015.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 01:26:07 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.49 % Drodi V4.1.1
% 0.18/0.67 % Refutation found
% 0.18/0.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/0.67 % SZS output start CNFRefutation for theBenchmark
% 0.18/0.67 fof(f1,axiom,(
% 0.18/0.67 (! [E,S1,S2,T] :( ( environment(E)& subpopulations(S1,S2,E,T)& greater(growth_rate(S2,T),growth_rate(S1,T)) )=> selection_favors(S2,S1,T) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f2,axiom,(
% 0.18/0.67 (! [E,S1,S2,T] :( ( environment(E)& subpopulation(S1,E,T)& subpopulation(S2,E,T)& greater(cardinality_at_time(S1,T),zero)& cardinality_at_time(S2,T) = zero )=> selection_favors(S1,S2,T) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f3,axiom,(
% 0.18/0.67 (! [P] :( ( observational_period(P)& propagation_strategy(first_movers)& propagation_strategy(efficient_producers)& (! [E] :( ( environment(E)& in_environment(P,E) )=> selection_favors(efficient_producers,first_movers,end_time(E)) ) ))=> selection_favors(efficient_producers,first_movers,P) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f4,axiom,(
% 0.18/0.67 (! [P] :( ( observational_period(P)& slow_change(P) )=> (! [E] :( ( environment(E)& in_environment(P,E) )=> (? [T] :( in_environment(E,T)& greater(T,critical_point(E)) ) )) )) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f5,axiom,(
% 0.18/0.67 propagation_strategy(first_movers) ),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f6,axiom,(
% 0.18/0.67 propagation_strategy(efficient_producers) ),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f7,axiom,(
% 0.18/0.67 (! [E,T] :( ( environment(E)& greater_or_equal(T,start_time(E))& greater_or_equal(end_time(E),T) )=> in_environment(E,T) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f8,axiom,(
% 0.18/0.67 (! [E,T] :( ( environment(E)& in_environment(E,T) )=> greater_or_equal(end_time(E),T) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f9,axiom,(
% 0.18/0.67 (! [E,T] :( ( environment(E)& in_environment(E,T)& greater(cardinality_at_time(first_movers,T),zero)& greater(cardinality_at_time(efficient_producers,T),zero) )=> subpopulations(first_movers,efficient_producers,E,T) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f10,axiom,(
% 0.18/0.67 (! [E,T] :( ( environment(E)& in_environment(E,T) )=> greater_or_equal(cardinality_at_time(first_movers,T),zero) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f11,axiom,(
% 0.18/0.67 (! [E,T] :( ( environment(E)& in_environment(E,T) )=> ( subpopulation(first_movers,E,T)& subpopulation(efficient_producers,E,T) ) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f12,axiom,(
% 0.18/0.67 (! [E] :( environment(E)=> greater_or_equal(critical_point(E),appear(efficient_producers,E)) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f13,axiom,(
% 0.18/0.67 (! [E] :( environment(E)=> greater_or_equal(critical_point(E),start_time(E)) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f14,axiom,(
% 0.18/0.67 (! [X,Y,Z] :( ( greater(X,Y)& greater(Y,Z) )=> greater(X,Z) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f16,axiom,(
% 0.18/0.67 (! [X,Y] :( greater_or_equal(X,Y)<=> ( greater(X,Y)| X = Y ) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f17,hypothesis,(
% 0.18/0.67 (! [E,Tc] :( ( environment(E)& Tc = critical_point(E) )=> ( ~ greater(growth_rate(efficient_producers,Tc),growth_rate(first_movers,Tc))& (! [T] :( ( subpopulations(first_movers,efficient_producers,E,T)& greater(T,Tc) )=> greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) )) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f18,hypothesis,(
% 0.18/0.67 (! [E,T] :( ( environment(E)& in_environment(E,T)& greater_or_equal(T,appear(efficient_producers,E)) )=> greater(cardinality_at_time(efficient_producers,T),zero) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f19,conjecture,(
% 0.18/0.67 (! [P] :( ( observational_period(P)& slow_change(P) )=> selection_favors(efficient_producers,first_movers,P) ) )),
% 0.18/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.18/0.67 fof(f20,negated_conjecture,(
% 0.18/0.67 ~((! [P] :( ( observational_period(P)& slow_change(P) )=> selection_favors(efficient_producers,first_movers,P) ) ))),
% 0.18/0.67 inference(negated_conjecture,[status(cth)],[f19])).
% 0.18/0.67 fof(f21,plain,(
% 0.18/0.67 ![E,S1,S2,T]: (((~environment(E)|~subpopulations(S1,S2,E,T))|~greater(growth_rate(S2,T),growth_rate(S1,T)))|selection_favors(S2,S1,T))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.18/0.67 fof(f22,plain,(
% 0.18/0.67 ![S1,S2,T]: (((![E]: (~environment(E)|~subpopulations(S1,S2,E,T)))|~greater(growth_rate(S2,T),growth_rate(S1,T)))|selection_favors(S2,S1,T))),
% 0.18/0.67 inference(miniscoping,[status(thm)],[f21])).
% 0.18/0.67 fof(f23,plain,(
% 0.18/0.67 ![X0,X1,X2,X3]: (~environment(X0)|~subpopulations(X1,X2,X0,X3)|~greater(growth_rate(X2,X3),growth_rate(X1,X3))|selection_favors(X2,X1,X3))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f22])).
% 0.18/0.67 fof(f24,plain,(
% 0.18/0.67 ![E,S1,S2,T]: (((((~environment(E)|~subpopulation(S1,E,T))|~subpopulation(S2,E,T))|~greater(cardinality_at_time(S1,T),zero))|~cardinality_at_time(S2,T)=zero)|selection_favors(S1,S2,T))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.18/0.67 fof(f25,plain,(
% 0.18/0.67 ![S1,S2,T]: ((((![E]: ((~environment(E)|~subpopulation(S1,E,T))|~subpopulation(S2,E,T)))|~greater(cardinality_at_time(S1,T),zero))|~cardinality_at_time(S2,T)=zero)|selection_favors(S1,S2,T))),
% 0.18/0.67 inference(miniscoping,[status(thm)],[f24])).
% 0.18/0.67 fof(f26,plain,(
% 0.18/0.67 ![X0,X1,X2,X3]: (~environment(X0)|~subpopulation(X1,X0,X2)|~subpopulation(X3,X0,X2)|~greater(cardinality_at_time(X1,X2),zero)|~cardinality_at_time(X3,X2)=zero|selection_favors(X1,X3,X2))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f25])).
% 0.18/0.67 fof(f27,plain,(
% 0.18/0.67 ![P]: ((((~observational_period(P)|~propagation_strategy(first_movers))|~propagation_strategy(efficient_producers))|(?[E]: ((environment(E)&in_environment(P,E))&~selection_favors(efficient_producers,first_movers,end_time(E)))))|selection_favors(efficient_producers,first_movers,P))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.18/0.67 fof(f28,plain,(
% 0.18/0.67 ![P]: ((((~observational_period(P)|~propagation_strategy(first_movers))|~propagation_strategy(efficient_producers))|((environment(sK0_skl(P))&in_environment(P,sK0_skl(P)))&~selection_favors(efficient_producers,first_movers,end_time(sK0_skl(P)))))|selection_favors(efficient_producers,first_movers,P))),
% 0.18/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(E,sK0_skl(P))],[f27])).
% 0.18/0.67 fof(f29,plain,(
% 0.18/0.67 ![X0]: (~observational_period(X0)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)|environment(sK0_skl(X0))|selection_favors(efficient_producers,first_movers,X0))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f28])).
% 0.18/0.67 fof(f30,plain,(
% 0.18/0.67 ![X0]: (~observational_period(X0)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)|in_environment(X0,sK0_skl(X0))|selection_favors(efficient_producers,first_movers,X0))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f28])).
% 0.18/0.67 fof(f31,plain,(
% 0.18/0.67 ![X0]: (~observational_period(X0)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)|~selection_favors(efficient_producers,first_movers,end_time(sK0_skl(X0)))|selection_favors(efficient_producers,first_movers,X0))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f28])).
% 0.18/0.67 fof(f32,plain,(
% 0.18/0.67 ![P]: ((~observational_period(P)|~slow_change(P))|(![E]: ((~environment(E)|~in_environment(P,E))|(?[T]: (in_environment(E,T)&greater(T,critical_point(E)))))))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.18/0.67 fof(f33,plain,(
% 0.18/0.67 ![P]: ((~observational_period(P)|~slow_change(P))|(![E]: ((~environment(E)|~in_environment(P,E))|(in_environment(E,sK1_skl(E,P))&greater(sK1_skl(E,P),critical_point(E))))))),
% 0.18/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(T,sK1_skl(E,P))],[f32])).
% 0.18/0.67 fof(f34,plain,(
% 0.18/0.67 ![X0,X1]: (~observational_period(X0)|~slow_change(X0)|~environment(X1)|~in_environment(X0,X1)|in_environment(X1,sK1_skl(X1,X0)))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f33])).
% 0.18/0.67 fof(f35,plain,(
% 0.18/0.67 ![X0,X1]: (~observational_period(X0)|~slow_change(X0)|~environment(X1)|~in_environment(X0,X1)|greater(sK1_skl(X1,X0),critical_point(X1)))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f33])).
% 0.18/0.67 fof(f36,plain,(
% 0.18/0.67 propagation_strategy(first_movers)),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 0.18/0.67 fof(f37,plain,(
% 0.18/0.67 propagation_strategy(efficient_producers)),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 0.18/0.67 fof(f38,plain,(
% 0.18/0.67 ![E,T]: (((~environment(E)|~greater_or_equal(T,start_time(E)))|~greater_or_equal(end_time(E),T))|in_environment(E,T))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.18/0.67 fof(f39,plain,(
% 0.18/0.67 ![X0,X1]: (~environment(X0)|~greater_or_equal(X1,start_time(X0))|~greater_or_equal(end_time(X0),X1)|in_environment(X0,X1))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f38])).
% 0.18/0.67 fof(f40,plain,(
% 0.18/0.67 ![E,T]: ((~environment(E)|~in_environment(E,T))|greater_or_equal(end_time(E),T))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.18/0.67 fof(f41,plain,(
% 0.18/0.67 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|greater_or_equal(end_time(X0),X1))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f40])).
% 0.18/0.67 fof(f42,plain,(
% 0.18/0.67 ![E,T]: ((((~environment(E)|~in_environment(E,T))|~greater(cardinality_at_time(first_movers,T),zero))|~greater(cardinality_at_time(efficient_producers,T),zero))|subpopulations(first_movers,efficient_producers,E,T))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.18/0.67 fof(f43,plain,(
% 0.18/0.67 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|~greater(cardinality_at_time(first_movers,X1),zero)|~greater(cardinality_at_time(efficient_producers,X1),zero)|subpopulations(first_movers,efficient_producers,X0,X1))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f42])).
% 0.18/0.67 fof(f44,plain,(
% 0.18/0.67 ![E,T]: ((~environment(E)|~in_environment(E,T))|greater_or_equal(cardinality_at_time(first_movers,T),zero))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.18/0.67 fof(f45,plain,(
% 0.18/0.67 ![T]: ((![E]: (~environment(E)|~in_environment(E,T)))|greater_or_equal(cardinality_at_time(first_movers,T),zero))),
% 0.18/0.67 inference(miniscoping,[status(thm)],[f44])).
% 0.18/0.67 fof(f46,plain,(
% 0.18/0.67 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|greater_or_equal(cardinality_at_time(first_movers,X1),zero))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f45])).
% 0.18/0.67 fof(f47,plain,(
% 0.18/0.67 ![E,T]: ((~environment(E)|~in_environment(E,T))|(subpopulation(first_movers,E,T)&subpopulation(efficient_producers,E,T)))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.18/0.67 fof(f48,plain,(
% 0.18/0.67 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|subpopulation(first_movers,X0,X1))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f47])).
% 0.18/0.67 fof(f49,plain,(
% 0.18/0.67 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|subpopulation(efficient_producers,X0,X1))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f47])).
% 0.18/0.67 fof(f50,plain,(
% 0.18/0.67 ![E]: (~environment(E)|greater_or_equal(critical_point(E),appear(efficient_producers,E)))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.18/0.67 fof(f51,plain,(
% 0.18/0.67 ![X0]: (~environment(X0)|greater_or_equal(critical_point(X0),appear(efficient_producers,X0)))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f50])).
% 0.18/0.67 fof(f52,plain,(
% 0.18/0.67 ![E]: (~environment(E)|greater_or_equal(critical_point(E),start_time(E)))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.18/0.67 fof(f53,plain,(
% 0.18/0.67 ![X0]: (~environment(X0)|greater_or_equal(critical_point(X0),start_time(X0)))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f52])).
% 0.18/0.67 fof(f54,plain,(
% 0.18/0.67 ![X,Y,Z]: ((~greater(X,Y)|~greater(Y,Z))|greater(X,Z))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.18/0.67 fof(f55,plain,(
% 0.18/0.67 ![X,Z]: ((![Y]: (~greater(X,Y)|~greater(Y,Z)))|greater(X,Z))),
% 0.18/0.67 inference(miniscoping,[status(thm)],[f54])).
% 0.18/0.67 fof(f56,plain,(
% 0.18/0.67 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f55])).
% 0.18/0.67 fof(f59,plain,(
% 0.18/0.67 ![X,Y]: ((~greater_or_equal(X,Y)|(greater(X,Y)|X=Y))&(greater_or_equal(X,Y)|(~greater(X,Y)&~X=Y)))),
% 0.18/0.67 inference(NNF_transformation,[status(thm)],[f16])).
% 0.18/0.67 fof(f60,plain,(
% 0.18/0.67 (![X,Y]: (~greater_or_equal(X,Y)|(greater(X,Y)|X=Y)))&(![X,Y]: (greater_or_equal(X,Y)|(~greater(X,Y)&~X=Y)))),
% 0.18/0.67 inference(miniscoping,[status(thm)],[f59])).
% 0.18/0.67 fof(f61,plain,(
% 0.18/0.67 ![X0,X1]: (~greater_or_equal(X0,X1)|greater(X0,X1)|X0=X1)),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f60])).
% 0.18/0.67 fof(f62,plain,(
% 0.18/0.67 ![X0,X1]: (greater_or_equal(X0,X1)|~greater(X0,X1))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f60])).
% 0.18/0.67 fof(f63,plain,(
% 0.18/0.67 ![X0,X1]: (greater_or_equal(X0,X1)|~X0=X1)),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f60])).
% 0.18/0.67 fof(f64,plain,(
% 0.18/0.67 ![E,Tc]: ((~environment(E)|~Tc=critical_point(E))|(~greater(growth_rate(efficient_producers,Tc),growth_rate(first_movers,Tc))&(![T]: ((~subpopulations(first_movers,efficient_producers,E,T)|~greater(T,Tc))|greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T))))))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.18/0.67 fof(f65,plain,(
% 0.18/0.67 ![X0,X1]: (~environment(X0)|~X1=critical_point(X0)|~greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1)))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f64])).
% 0.18/0.67 fof(f66,plain,(
% 0.18/0.67 ![X0,X1,X2]: (~environment(X0)|~X1=critical_point(X0)|~subpopulations(first_movers,efficient_producers,X0,X2)|~greater(X2,X1)|greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f64])).
% 0.18/0.67 fof(f67,plain,(
% 0.18/0.67 ![E,T]: (((~environment(E)|~in_environment(E,T))|~greater_or_equal(T,appear(efficient_producers,E)))|greater(cardinality_at_time(efficient_producers,T),zero))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.18/0.67 fof(f68,plain,(
% 0.18/0.67 ![T]: ((![E]: ((~environment(E)|~in_environment(E,T))|~greater_or_equal(T,appear(efficient_producers,E))))|greater(cardinality_at_time(efficient_producers,T),zero))),
% 0.18/0.67 inference(miniscoping,[status(thm)],[f67])).
% 0.18/0.67 fof(f69,plain,(
% 0.18/0.67 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|~greater_or_equal(X1,appear(efficient_producers,X0))|greater(cardinality_at_time(efficient_producers,X1),zero))),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f68])).
% 0.18/0.67 fof(f70,plain,(
% 0.18/0.67 (?[P]: ((observational_period(P)&slow_change(P))&~selection_favors(efficient_producers,first_movers,P)))),
% 0.18/0.67 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.18/0.67 fof(f71,plain,(
% 0.18/0.67 ((observational_period(sK2_skl)&slow_change(sK2_skl))&~selection_favors(efficient_producers,first_movers,sK2_skl))),
% 0.18/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(P,sK2_skl)],[f70])).
% 0.18/0.67 fof(f72,plain,(
% 0.18/0.67 observational_period(sK2_skl)),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f71])).
% 0.18/0.67 fof(f73,plain,(
% 0.18/0.67 slow_change(sK2_skl)),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f71])).
% 0.18/0.67 fof(f74,plain,(
% 0.18/0.67 ~selection_favors(efficient_producers,first_movers,sK2_skl)),
% 0.18/0.67 inference(cnf_transformation,[status(thm)],[f71])).
% 0.18/0.67 fof(f75,definition,(
% 0.18/0.67 ![X0]: (sQ0_spl <=> (~observational_period(X0)|environment(sK0_skl(X0))|selection_favors(efficient_producers,first_movers,X0)))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f76,plain,(
% 0.18/0.67 ![X0]: (~observational_period(X0)|environment(sK0_skl(X0))|selection_favors(efficient_producers,first_movers,X0)|~sQ0_spl)),
% 0.18/0.67 inference(component_clause,[status(thm)],[f75])).
% 0.18/0.67 fof(f78,definition,(
% 0.18/0.67 sQ1_spl <=> (propagation_strategy(first_movers))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f80,plain,(
% 0.18/0.67 ~propagation_strategy(first_movers)|sQ1_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f78])).
% 0.18/0.67 fof(f81,definition,(
% 0.18/0.67 sQ2_spl <=> (propagation_strategy(efficient_producers))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f83,plain,(
% 0.18/0.67 ~propagation_strategy(efficient_producers)|sQ2_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f81])).
% 0.18/0.67 fof(f84,plain,(
% 0.18/0.67 sQ0_spl|~sQ1_spl|~sQ2_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f29,f75,f78,f81])).
% 0.18/0.67 fof(f85,definition,(
% 0.18/0.67 ![X0]: (sQ3_spl <=> (~observational_period(X0)|in_environment(X0,sK0_skl(X0))|selection_favors(efficient_producers,first_movers,X0)))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f86,plain,(
% 0.18/0.67 ![X0]: (~observational_period(X0)|in_environment(X0,sK0_skl(X0))|selection_favors(efficient_producers,first_movers,X0)|~sQ3_spl)),
% 0.18/0.67 inference(component_clause,[status(thm)],[f85])).
% 0.18/0.67 fof(f88,plain,(
% 0.18/0.67 sQ3_spl|~sQ1_spl|~sQ2_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f30,f85,f78,f81])).
% 0.18/0.67 fof(f89,definition,(
% 0.18/0.67 ![X0]: (sQ4_spl <=> (~observational_period(X0)|~selection_favors(efficient_producers,first_movers,end_time(sK0_skl(X0)))|selection_favors(efficient_producers,first_movers,X0)))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f90,plain,(
% 0.18/0.67 ![X0]: (~observational_period(X0)|~selection_favors(efficient_producers,first_movers,end_time(sK0_skl(X0)))|selection_favors(efficient_producers,first_movers,X0)|~sQ4_spl)),
% 0.18/0.67 inference(component_clause,[status(thm)],[f89])).
% 0.18/0.67 fof(f92,plain,(
% 0.18/0.67 sQ4_spl|~sQ1_spl|~sQ2_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f31,f89,f78,f81])).
% 0.18/0.67 fof(f93,plain,(
% 0.18/0.67 ![X0]: (greater_or_equal(X0,X0))),
% 0.18/0.67 inference(destructive_equality_resolution,[status(thm)],[f63])).
% 0.18/0.67 fof(f94,plain,(
% 0.18/0.67 ![X0]: (~environment(X0)|~greater(growth_rate(efficient_producers,critical_point(X0)),growth_rate(first_movers,critical_point(X0))))),
% 0.18/0.67 inference(destructive_equality_resolution,[status(thm)],[f65])).
% 0.18/0.67 fof(f95,plain,(
% 0.18/0.67 ![X0,X1]: (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater(X1,critical_point(X0))|greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1)))),
% 0.18/0.67 inference(destructive_equality_resolution,[status(thm)],[f66])).
% 0.18/0.67 fof(f96,plain,(
% 0.18/0.67 $false|sQ2_spl),
% 0.18/0.67 inference(forward_subsumption_resolution,[status(thm)],[f83,f37])).
% 0.18/0.67 fof(f97,plain,(
% 0.18/0.67 sQ2_spl),
% 0.18/0.67 inference(contradiction_clause,[status(thm)],[f96])).
% 0.18/0.67 fof(f98,plain,(
% 0.18/0.67 $false|sQ1_spl),
% 0.18/0.67 inference(forward_subsumption_resolution,[status(thm)],[f80,f36])).
% 0.18/0.67 fof(f99,plain,(
% 0.18/0.67 sQ1_spl),
% 0.18/0.67 inference(contradiction_clause,[status(thm)],[f98])).
% 0.18/0.67 fof(f102,plain,(
% 0.18/0.67 ![X0,X1,X2]: (~greater(X0,sK1_skl(X1,X2))|greater(X0,critical_point(X1))|~observational_period(X2)|~slow_change(X2)|~environment(X1)|~in_environment(X2,X1))),
% 0.18/0.67 inference(resolution,[status(thm)],[f56,f35])).
% 0.18/0.67 fof(f103,plain,(
% 0.18/0.67 environment(sK0_skl(sK2_skl))|selection_favors(efficient_producers,first_movers,sK2_skl)|~sQ0_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f76,f72])).
% 0.18/0.67 fof(f104,definition,(
% 0.18/0.67 sQ5_spl <=> (environment(sK0_skl(sK2_skl)))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f105,plain,(
% 0.18/0.67 environment(sK0_skl(sK2_skl))|~sQ5_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f104])).
% 0.18/0.67 fof(f107,definition,(
% 0.18/0.67 sQ6_spl <=> (selection_favors(efficient_producers,first_movers,sK2_skl))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f108,plain,(
% 0.18/0.67 selection_favors(efficient_producers,first_movers,sK2_skl)|~sQ6_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f107])).
% 0.18/0.67 fof(f110,plain,(
% 0.18/0.67 sQ5_spl|sQ6_spl|~sQ0_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f103,f104,f107,f75])).
% 0.18/0.67 fof(f111,plain,(
% 0.18/0.67 greater_or_equal(critical_point(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl)))|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f105,f53])).
% 0.18/0.67 fof(f112,plain,(
% 0.18/0.67 greater_or_equal(critical_point(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl)))|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f105,f51])).
% 0.18/0.67 fof(f113,plain,(
% 0.18/0.67 ![X0]: (~in_environment(sK0_skl(sK2_skl),X0)|subpopulation(efficient_producers,sK0_skl(sK2_skl),X0)|~sQ5_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f105,f49])).
% 0.18/0.67 fof(f114,plain,(
% 0.18/0.67 ![X0]: (~in_environment(sK0_skl(sK2_skl),X0)|greater_or_equal(cardinality_at_time(first_movers,X0),zero)|~sQ5_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f105,f46])).
% 0.18/0.67 fof(f115,plain,(
% 0.18/0.67 ![X0]: (~in_environment(sK0_skl(sK2_skl),X0)|greater_or_equal(end_time(sK0_skl(sK2_skl)),X0)|~sQ5_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f105,f41])).
% 0.18/0.67 fof(f116,plain,(
% 0.18/0.67 ![X0]: (~greater_or_equal(X0,start_time(sK0_skl(sK2_skl)))|~greater_or_equal(end_time(sK0_skl(sK2_skl)),X0)|in_environment(sK0_skl(sK2_skl),X0)|~sQ5_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f105,f39])).
% 0.18/0.67 fof(f117,plain,(
% 0.18/0.67 ![X0]: (~in_environment(sK0_skl(sK2_skl),X0)|subpopulation(first_movers,sK0_skl(sK2_skl),X0)|~sQ5_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f105,f48])).
% 0.18/0.67 fof(f118,plain,(
% 0.18/0.67 ![X0]: (~observational_period(X0)|~slow_change(X0)|~in_environment(X0,sK0_skl(sK2_skl))|in_environment(sK0_skl(sK2_skl),sK1_skl(sK0_skl(sK2_skl),X0))|~sQ5_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f105,f34])).
% 0.18/0.67 fof(f119,plain,(
% 0.18/0.67 greater(critical_point(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl)))|critical_point(sK0_skl(sK2_skl))=start_time(sK0_skl(sK2_skl))|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f111,f61])).
% 0.18/0.67 fof(f120,definition,(
% 0.18/0.67 sQ7_spl <=> (greater(critical_point(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f121,plain,(
% 0.18/0.67 greater(critical_point(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl)))|~sQ7_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f120])).
% 0.18/0.67 fof(f123,definition,(
% 0.18/0.67 sQ8_spl <=> (critical_point(sK0_skl(sK2_skl))=start_time(sK0_skl(sK2_skl)))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f124,plain,(
% 0.18/0.67 critical_point(sK0_skl(sK2_skl))=start_time(sK0_skl(sK2_skl))|~sQ8_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f123])).
% 0.18/0.67 fof(f126,plain,(
% 0.18/0.67 sQ7_spl|sQ8_spl|~sQ5_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f119,f120,f123,f104])).
% 0.18/0.67 fof(f127,plain,(
% 0.18/0.67 $false|~sQ6_spl),
% 0.18/0.67 inference(forward_subsumption_resolution,[status(thm)],[f108,f74])).
% 0.18/0.67 fof(f128,plain,(
% 0.18/0.67 ~sQ6_spl),
% 0.18/0.67 inference(contradiction_clause,[status(thm)],[f127])).
% 0.18/0.67 fof(f137,plain,(
% 0.18/0.67 greater(critical_point(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl)))|critical_point(sK0_skl(sK2_skl))=appear(efficient_producers,sK0_skl(sK2_skl))|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f112,f61])).
% 0.18/0.67 fof(f138,definition,(
% 0.18/0.67 sQ9_spl <=> (greater(critical_point(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f139,plain,(
% 0.18/0.67 greater(critical_point(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl)))|~sQ9_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f138])).
% 0.18/0.67 fof(f141,definition,(
% 0.18/0.67 sQ10_spl <=> (critical_point(sK0_skl(sK2_skl))=appear(efficient_producers,sK0_skl(sK2_skl)))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f142,plain,(
% 0.18/0.67 critical_point(sK0_skl(sK2_skl))=appear(efficient_producers,sK0_skl(sK2_skl))|~sQ10_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f141])).
% 0.18/0.67 fof(f144,plain,(
% 0.18/0.67 sQ9_spl|sQ10_spl|~sQ5_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f137,f138,f141,f104])).
% 0.18/0.67 fof(f145,plain,(
% 0.18/0.67 in_environment(sK2_skl,sK0_skl(sK2_skl))|selection_favors(efficient_producers,first_movers,sK2_skl)|~sQ3_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f86,f72])).
% 0.18/0.67 fof(f146,definition,(
% 0.18/0.67 sQ11_spl <=> (in_environment(sK2_skl,sK0_skl(sK2_skl)))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f149,plain,(
% 0.18/0.67 sQ11_spl|sQ6_spl|~sQ3_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f145,f146,f107,f85])).
% 0.18/0.67 fof(f150,plain,(
% 0.18/0.67 ![X0]: (~in_environment(sK0_skl(sK2_skl),X0)|~greater_or_equal(X0,appear(efficient_producers,sK0_skl(sK2_skl)))|greater(cardinality_at_time(efficient_producers,X0),zero)|~sQ5_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f69,f105])).
% 0.18/0.67 fof(f152,plain,(
% 0.18/0.67 ~greater_or_equal(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl)))|in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f116,f93])).
% 0.18/0.67 fof(f153,definition,(
% 0.18/0.67 sQ12_spl <=> (greater_or_equal(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f155,plain,(
% 0.18/0.67 ~greater_or_equal(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl)))|sQ12_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f153])).
% 0.18/0.67 fof(f156,definition,(
% 0.18/0.67 sQ13_spl <=> (in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f157,plain,(
% 0.18/0.67 in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))|~sQ13_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f156])).
% 0.18/0.67 fof(f159,plain,(
% 0.18/0.67 ~sQ12_spl|sQ13_spl|~sQ5_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f152,f153,f156,f104])).
% 0.18/0.67 fof(f160,plain,(
% 0.18/0.67 ![X0]: (~greater(X0,critical_point(sK0_skl(sK2_skl)))|greater(X0,appear(efficient_producers,sK0_skl(sK2_skl)))|~sQ9_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f139,f56])).
% 0.18/0.67 fof(f162,plain,(
% 0.18/0.67 ~observational_period(sK2_skl)|~in_environment(sK2_skl,sK0_skl(sK2_skl))|in_environment(sK0_skl(sK2_skl),sK1_skl(sK0_skl(sK2_skl),sK2_skl))|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f118,f73])).
% 0.18/0.67 fof(f163,definition,(
% 0.18/0.67 sQ14_spl <=> (observational_period(sK2_skl))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f165,plain,(
% 0.18/0.67 ~observational_period(sK2_skl)|sQ14_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f163])).
% 0.18/0.67 fof(f166,definition,(
% 0.18/0.67 sQ15_spl <=> (in_environment(sK0_skl(sK2_skl),sK1_skl(sK0_skl(sK2_skl),sK2_skl)))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f167,plain,(
% 0.18/0.67 in_environment(sK0_skl(sK2_skl),sK1_skl(sK0_skl(sK2_skl),sK2_skl))|~sQ15_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f166])).
% 0.18/0.67 fof(f169,plain,(
% 0.18/0.67 ~sQ14_spl|~sQ11_spl|sQ15_spl|~sQ5_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f162,f163,f146,f166,f104])).
% 0.18/0.67 fof(f170,plain,(
% 0.18/0.67 $false|sQ14_spl),
% 0.18/0.67 inference(forward_subsumption_resolution,[status(thm)],[f165,f72])).
% 0.18/0.67 fof(f171,plain,(
% 0.18/0.67 sQ14_spl),
% 0.18/0.67 inference(contradiction_clause,[status(thm)],[f170])).
% 0.18/0.67 fof(f175,plain,(
% 0.18/0.67 ![X0]: (~greater(X0,critical_point(sK0_skl(sK2_skl)))|greater(X0,start_time(sK0_skl(sK2_skl)))|~sQ7_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f121,f56])).
% 0.18/0.67 fof(f179,definition,(
% 0.18/0.67 sQ17_spl <=> (greater_or_equal(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f180,plain,(
% 0.18/0.67 greater_or_equal(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl)))|~sQ17_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f179])).
% 0.18/0.67 fof(f181,plain,(
% 0.18/0.67 ~greater_or_equal(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl)))|sQ17_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f179])).
% 0.18/0.67 fof(f185,plain,(
% 0.18/0.67 ~greater_or_equal(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl)))|~sQ8_spl|sQ12_spl),
% 0.18/0.67 inference(backward_demodulation,[status(thm)],[f124,f155])).
% 0.18/0.67 fof(f187,plain,(
% 0.18/0.67 $false|~sQ17_spl|~sQ8_spl|sQ12_spl),
% 0.18/0.67 inference(forward_subsumption_resolution,[status(thm)],[f185,f180])).
% 0.18/0.67 fof(f188,plain,(
% 0.18/0.67 ~sQ17_spl|~sQ8_spl|sQ12_spl),
% 0.18/0.67 inference(contradiction_clause,[status(thm)],[f187])).
% 0.18/0.67 fof(f189,plain,(
% 0.18/0.67 ![X0]: (~in_environment(sK0_skl(sK2_skl),X0)|~greater_or_equal(X0,critical_point(sK0_skl(sK2_skl)))|greater(cardinality_at_time(efficient_producers,X0),zero)|~sQ10_spl|~sQ5_spl)),
% 0.18/0.67 inference(backward_demodulation,[status(thm)],[f142,f150])).
% 0.18/0.67 fof(f194,plain,(
% 0.18/0.67 greater_or_equal(cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl))),zero)|~sQ13_spl|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f157,f114])).
% 0.18/0.67 fof(f197,plain,(
% 0.18/0.67 greater_or_equal(end_time(sK0_skl(sK2_skl)),sK1_skl(sK0_skl(sK2_skl),sK2_skl))|~sQ15_spl|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f167,f115])).
% 0.18/0.67 fof(f205,definition,(
% 0.18/0.67 sQ18_spl <=> (in_environment(sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f208,definition,(
% 0.18/0.67 sQ19_spl <=> (greater(cardinality_at_time(efficient_producers,critical_point(sK0_skl(sK2_skl))),zero))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f209,plain,(
% 0.18/0.67 greater(cardinality_at_time(efficient_producers,critical_point(sK0_skl(sK2_skl))),zero)|~sQ19_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f208])).
% 0.18/0.67 fof(f217,definition,(
% 0.18/0.67 sQ20_spl <=> (greater_or_equal(start_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f219,plain,(
% 0.18/0.67 ~greater_or_equal(start_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl)))|sQ20_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f217])).
% 0.18/0.67 fof(f242,plain,(
% 0.18/0.67 ![X0]: (~in_environment(sK0_skl(sK2_skl),X0)|greater(cardinality_at_time(efficient_producers,X0),zero)|~greater(X0,appear(efficient_producers,sK0_skl(sK2_skl)))|~sQ5_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f150,f62])).
% 0.18/0.67 fof(f244,definition,(
% 0.18/0.67 sQ24_spl <=> (in_environment(sK0_skl(sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f245,plain,(
% 0.18/0.67 in_environment(sK0_skl(sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl)))|~sQ24_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f244])).
% 0.18/0.67 fof(f246,plain,(
% 0.18/0.67 ~in_environment(sK0_skl(sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl)))|sQ24_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f244])).
% 0.18/0.67 fof(f252,plain,(
% 0.18/0.67 ~in_environment(sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl)))|greater(cardinality_at_time(efficient_producers,critical_point(sK0_skl(sK2_skl))),zero)|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f112,f150])).
% 0.18/0.67 fof(f254,plain,(
% 0.18/0.67 ~sQ18_spl|sQ19_spl|~sQ5_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f252,f205,f208,f104])).
% 0.18/0.67 fof(f263,plain,(
% 0.18/0.67 ~greater(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl)))|sQ12_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f155,f62])).
% 0.18/0.67 fof(f276,definition,(
% 0.18/0.67 sQ28_spl <=> (greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f277,plain,(
% 0.18/0.67 greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl)))|~sQ28_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f276])).
% 0.18/0.67 fof(f281,plain,(
% 0.18/0.67 greater(cardinality_at_time(efficient_producers,sK1_skl(sK0_skl(sK2_skl),sK2_skl)),zero)|~greater(sK1_skl(sK0_skl(sK2_skl),sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl)))|~sQ5_spl|~sQ15_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f242,f167])).
% 0.18/0.67 fof(f282,definition,(
% 0.18/0.67 sQ29_spl <=> (greater(cardinality_at_time(efficient_producers,sK1_skl(sK0_skl(sK2_skl),sK2_skl)),zero))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f283,plain,(
% 0.18/0.67 greater(cardinality_at_time(efficient_producers,sK1_skl(sK0_skl(sK2_skl),sK2_skl)),zero)|~sQ29_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f282])).
% 0.18/0.67 fof(f285,definition,(
% 0.18/0.67 sQ30_spl <=> (greater(sK1_skl(sK0_skl(sK2_skl),sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f286,plain,(
% 0.18/0.67 greater(sK1_skl(sK0_skl(sK2_skl),sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl)))|~sQ30_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f285])).
% 0.18/0.67 fof(f287,plain,(
% 0.18/0.67 ~greater(sK1_skl(sK0_skl(sK2_skl),sK2_skl),appear(efficient_producers,sK0_skl(sK2_skl)))|sQ30_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f285])).
% 0.18/0.67 fof(f288,plain,(
% 0.18/0.67 sQ29_spl|~sQ30_spl|~sQ5_spl|~sQ15_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f281,f282,f285,f104,f166])).
% 0.18/0.67 fof(f298,plain,(
% 0.18/0.67 greater(end_time(sK0_skl(sK2_skl)),sK1_skl(sK0_skl(sK2_skl),sK2_skl))|end_time(sK0_skl(sK2_skl))=sK1_skl(sK0_skl(sK2_skl),sK2_skl)|~sQ15_spl|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f197,f61])).
% 0.18/0.67 fof(f303,definition,(
% 0.18/0.67 sQ34_spl <=> (greater(end_time(sK0_skl(sK2_skl)),sK1_skl(sK0_skl(sK2_skl),sK2_skl)))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f304,plain,(
% 0.18/0.67 greater(end_time(sK0_skl(sK2_skl)),sK1_skl(sK0_skl(sK2_skl),sK2_skl))|~sQ34_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f303])).
% 0.18/0.67 fof(f306,definition,(
% 0.18/0.67 sQ35_spl <=> (end_time(sK0_skl(sK2_skl))=sK1_skl(sK0_skl(sK2_skl),sK2_skl))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f307,plain,(
% 0.18/0.67 end_time(sK0_skl(sK2_skl))=sK1_skl(sK0_skl(sK2_skl),sK2_skl)|~sQ35_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f306])).
% 0.18/0.67 fof(f309,plain,(
% 0.18/0.67 sQ34_spl|sQ35_spl|~sQ15_spl|~sQ5_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f298,f303,f306,f166,f104])).
% 0.18/0.67 fof(f310,plain,(
% 0.18/0.67 ~greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl)))|sQ17_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f181,f62])).
% 0.18/0.67 fof(f332,plain,(
% 0.18/0.67 ![X0,X1]: (~environment(X0)|~subpopulation(efficient_producers,X0,critical_point(sK0_skl(sK2_skl)))|~subpopulation(X1,X0,critical_point(sK0_skl(sK2_skl)))|~cardinality_at_time(X1,critical_point(sK0_skl(sK2_skl)))=zero|selection_favors(efficient_producers,X1,critical_point(sK0_skl(sK2_skl)))|~sQ19_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f209,f26])).
% 0.18/0.67 fof(f336,plain,(
% 0.18/0.67 ![X0]: (~environment(sK0_skl(sK2_skl))|~subpopulation(X0,sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl)))|~cardinality_at_time(X0,critical_point(sK0_skl(sK2_skl)))=zero|selection_favors(efficient_producers,X0,critical_point(sK0_skl(sK2_skl)))|~in_environment(sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl)))|~sQ19_spl|~sQ5_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f332,f113])).
% 0.18/0.67 fof(f337,definition,(
% 0.18/0.67 ![X0]: (sQ39_spl <=> (~subpopulation(X0,sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl)))|~cardinality_at_time(X0,critical_point(sK0_skl(sK2_skl)))=zero|selection_favors(efficient_producers,X0,critical_point(sK0_skl(sK2_skl)))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f340,plain,(
% 0.18/0.67 ~sQ5_spl|sQ39_spl|~sQ18_spl|~sQ19_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f336,f104,f337,f205,f208])).
% 0.18/0.67 fof(f352,plain,(
% 0.18/0.67 greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl)))|~observational_period(sK2_skl)|~slow_change(sK2_skl)|~environment(sK0_skl(sK2_skl))|~in_environment(sK2_skl,sK0_skl(sK2_skl))|~sQ34_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f304,f102])).
% 0.18/0.67 fof(f355,definition,(
% 0.18/0.67 sQ42_spl <=> (slow_change(sK2_skl))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f357,plain,(
% 0.18/0.67 ~slow_change(sK2_skl)|sQ42_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f355])).
% 0.18/0.67 fof(f358,plain,(
% 0.18/0.67 sQ28_spl|~sQ14_spl|~sQ42_spl|~sQ5_spl|~sQ11_spl|~sQ34_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f352,f276,f163,f355,f104,f146,f303])).
% 0.18/0.67 fof(f359,plain,(
% 0.18/0.67 $false|sQ42_spl),
% 0.18/0.67 inference(forward_subsumption_resolution,[status(thm)],[f357,f73])).
% 0.18/0.67 fof(f360,plain,(
% 0.18/0.67 sQ42_spl),
% 0.18/0.67 inference(contradiction_clause,[status(thm)],[f359])).
% 0.18/0.67 fof(f361,plain,(
% 0.18/0.67 $false|sQ17_spl|~sQ28_spl),
% 0.18/0.67 inference(forward_subsumption_resolution,[status(thm)],[f277,f310])).
% 0.18/0.67 fof(f362,plain,(
% 0.18/0.67 sQ17_spl|~sQ28_spl),
% 0.18/0.67 inference(contradiction_clause,[status(thm)],[f361])).
% 0.18/0.67 fof(f363,plain,(
% 0.18/0.67 greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero)|~greater(end_time(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl)))|~sQ13_spl|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f157,f242])).
% 0.18/0.67 fof(f366,definition,(
% 0.18/0.67 sQ43_spl <=> (greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f367,plain,(
% 0.18/0.67 greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero)|~sQ43_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f366])).
% 0.18/0.67 fof(f369,definition,(
% 0.18/0.67 sQ44_spl <=> (greater(end_time(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f372,plain,(
% 0.18/0.67 sQ43_spl|~sQ44_spl|~sQ13_spl|~sQ5_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f363,f366,f369,f156,f104])).
% 0.18/0.67 fof(f379,plain,(
% 0.18/0.67 greater(cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl))),zero)|cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl)))=zero|~sQ13_spl|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f194,f61])).
% 0.18/0.67 fof(f380,definition,(
% 0.18/0.67 sQ45_spl <=> (greater(cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl))),zero))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f381,plain,(
% 0.18/0.67 greater(cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl))),zero)|~sQ45_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f380])).
% 0.18/0.67 fof(f383,definition,(
% 0.18/0.67 sQ46_spl <=> (cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl)))=zero)),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f386,plain,(
% 0.18/0.67 sQ45_spl|sQ46_spl|~sQ13_spl|~sQ5_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f379,f380,f383,f156,f104])).
% 0.18/0.67 fof(f397,plain,(
% 0.18/0.67 $false|sQ20_spl),
% 0.18/0.67 inference(forward_subsumption_resolution,[status(thm)],[f219,f93])).
% 0.18/0.67 fof(f398,plain,(
% 0.18/0.67 sQ20_spl),
% 0.18/0.67 inference(contradiction_clause,[status(thm)],[f397])).
% 0.18/0.67 fof(f414,plain,(
% 0.18/0.67 ~greater_or_equal(critical_point(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl)))|in_environment(sK0_skl(sK2_skl),critical_point(sK0_skl(sK2_skl)))|~sQ17_spl|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f180,f116])).
% 0.18/0.67 fof(f416,definition,(
% 0.18/0.67 sQ51_spl <=> (greater_or_equal(critical_point(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f418,plain,(
% 0.18/0.67 ~greater_or_equal(critical_point(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl)))|sQ51_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f416])).
% 0.18/0.67 fof(f419,plain,(
% 0.18/0.67 ~sQ51_spl|sQ18_spl|~sQ17_spl|~sQ5_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f414,f416,f205,f179,f104])).
% 0.18/0.67 fof(f420,definition,(
% 0.18/0.67 sQ52_spl <=> (end_time(sK0_skl(sK2_skl))=critical_point(sK0_skl(sK2_skl)))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f421,plain,(
% 0.18/0.67 end_time(sK0_skl(sK2_skl))=critical_point(sK0_skl(sK2_skl))|~sQ52_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f420])).
% 0.18/0.67 fof(f429,plain,(
% 0.18/0.67 greater(end_time(sK0_skl(sK2_skl)),start_time(sK0_skl(sK2_skl)))|~sQ28_spl|~sQ7_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f277,f175])).
% 0.18/0.67 fof(f432,plain,(
% 0.18/0.67 $false|~sQ5_spl|sQ51_spl),
% 0.18/0.67 inference(forward_subsumption_resolution,[status(thm)],[f418,f111])).
% 0.18/0.67 fof(f433,plain,(
% 0.18/0.67 ~sQ5_spl|sQ51_spl),
% 0.18/0.67 inference(contradiction_clause,[status(thm)],[f432])).
% 0.18/0.67 fof(f440,plain,(
% 0.18/0.67 ![X0,X1]: (~environment(X0)|~subpopulation(efficient_producers,X0,end_time(sK0_skl(sK2_skl)))|~subpopulation(X1,X0,end_time(sK0_skl(sK2_skl)))|~cardinality_at_time(X1,end_time(sK0_skl(sK2_skl)))=zero|selection_favors(efficient_producers,X1,end_time(sK0_skl(sK2_skl)))|~sQ43_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f367,f26])).
% 0.18/0.67 fof(f450,plain,(
% 0.18/0.67 ![X0]: (~environment(X0)|~in_environment(X0,end_time(sK0_skl(sK2_skl)))|~greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero)|subpopulations(first_movers,efficient_producers,X0,end_time(sK0_skl(sK2_skl)))|~sQ45_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f381,f43])).
% 0.18/0.67 fof(f453,definition,(
% 0.18/0.67 ![X0]: (sQ55_spl <=> (~environment(X0)|~in_environment(X0,end_time(sK0_skl(sK2_skl)))|subpopulations(first_movers,efficient_producers,X0,end_time(sK0_skl(sK2_skl)))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f454,plain,(
% 0.18/0.67 ![X0]: (~environment(X0)|~in_environment(X0,end_time(sK0_skl(sK2_skl)))|subpopulations(first_movers,efficient_producers,X0,end_time(sK0_skl(sK2_skl)))|~sQ55_spl)),
% 0.18/0.67 inference(component_clause,[status(thm)],[f453])).
% 0.18/0.67 fof(f456,plain,(
% 0.18/0.67 sQ55_spl|~sQ43_spl|~sQ45_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f450,f453,f366,f380])).
% 0.18/0.67 fof(f513,plain,(
% 0.18/0.67 ![X0]: (~environment(sK0_skl(sK2_skl))|~subpopulation(X0,sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))|~cardinality_at_time(X0,end_time(sK0_skl(sK2_skl)))=zero|selection_favors(efficient_producers,X0,end_time(sK0_skl(sK2_skl)))|~in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))|~sQ43_spl|~sQ5_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f440,f113])).
% 0.18/0.67 fof(f514,definition,(
% 0.18/0.67 ![X0]: (sQ65_spl <=> (~subpopulation(X0,sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))|~cardinality_at_time(X0,end_time(sK0_skl(sK2_skl)))=zero|selection_favors(efficient_producers,X0,end_time(sK0_skl(sK2_skl)))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f515,plain,(
% 0.18/0.67 ![X0]: (~subpopulation(X0,sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))|~cardinality_at_time(X0,end_time(sK0_skl(sK2_skl)))=zero|selection_favors(efficient_producers,X0,end_time(sK0_skl(sK2_skl)))|~sQ65_spl)),
% 0.18/0.67 inference(component_clause,[status(thm)],[f514])).
% 0.18/0.67 fof(f517,plain,(
% 0.18/0.67 ~sQ5_spl|sQ65_spl|~sQ13_spl|~sQ43_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f513,f104,f514,f156,f366])).
% 0.18/0.67 fof(f562,plain,(
% 0.18/0.67 ~environment(sK0_skl(sK2_skl))|subpopulations(first_movers,efficient_producers,sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))|~sQ55_spl|~sQ13_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f454,f157])).
% 0.18/0.67 fof(f563,plain,(
% 0.18/0.67 ![X0]: (~environment(X0)|~in_environment(X0,end_time(sK0_skl(sK2_skl)))|~environment(X0)|~greater(end_time(sK0_skl(sK2_skl)),critical_point(X0))|greater(growth_rate(efficient_producers,end_time(sK0_skl(sK2_skl))),growth_rate(first_movers,end_time(sK0_skl(sK2_skl))))|~sQ55_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f454,f95])).
% 0.18/0.67 fof(f564,definition,(
% 0.18/0.67 sQ73_spl <=> (subpopulations(first_movers,efficient_producers,sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f565,plain,(
% 0.18/0.67 subpopulations(first_movers,efficient_producers,sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))|~sQ73_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f564])).
% 0.18/0.67 fof(f567,plain,(
% 0.18/0.67 ~sQ5_spl|sQ73_spl|~sQ55_spl|~sQ13_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f562,f104,f564,f453,f156])).
% 0.18/0.67 fof(f568,definition,(
% 0.18/0.67 ![X0]: (sQ74_spl <=> (~environment(X0)|~in_environment(X0,end_time(sK0_skl(sK2_skl)))|~environment(X0)|~greater(end_time(sK0_skl(sK2_skl)),critical_point(X0))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f571,definition,(
% 0.18/0.67 sQ75_spl <=> (greater(growth_rate(efficient_producers,end_time(sK0_skl(sK2_skl))),growth_rate(first_movers,end_time(sK0_skl(sK2_skl)))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f572,plain,(
% 0.18/0.67 greater(growth_rate(efficient_producers,end_time(sK0_skl(sK2_skl))),growth_rate(first_movers,end_time(sK0_skl(sK2_skl))))|~sQ75_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f571])).
% 0.18/0.67 fof(f574,plain,(
% 0.18/0.67 sQ74_spl|sQ75_spl|~sQ55_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f563,f568,f571,f453])).
% 0.18/0.67 fof(f615,definition,(
% 0.18/0.67 sQ83_spl <=> (greater(growth_rate(efficient_producers,critical_point(sK0_skl(sK2_skl))),growth_rate(first_movers,critical_point(sK0_skl(sK2_skl)))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f616,plain,(
% 0.18/0.67 greater(growth_rate(efficient_producers,critical_point(sK0_skl(sK2_skl))),growth_rate(first_movers,critical_point(sK0_skl(sK2_skl))))|~sQ83_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f615])).
% 0.18/0.67 fof(f624,plain,(
% 0.18/0.67 ~environment(sK0_skl(sK2_skl))|~greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl)))|greater(growth_rate(efficient_producers,end_time(sK0_skl(sK2_skl))),growth_rate(first_movers,end_time(sK0_skl(sK2_skl))))|~sQ73_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f565,f95])).
% 0.18/0.67 fof(f625,plain,(
% 0.18/0.67 ~sQ5_spl|~sQ28_spl|sQ75_spl|~sQ73_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f624,f104,f276,f571,f564])).
% 0.18/0.67 fof(f631,plain,(
% 0.18/0.67 ~cardinality_at_time(first_movers,end_time(sK0_skl(sK2_skl)))=zero|selection_favors(efficient_producers,first_movers,end_time(sK0_skl(sK2_skl)))|~in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))|~sQ65_spl|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f515,f117])).
% 0.18/0.67 fof(f633,definition,(
% 0.18/0.67 sQ85_spl <=> (selection_favors(efficient_producers,first_movers,end_time(sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f634,plain,(
% 0.18/0.67 selection_favors(efficient_producers,first_movers,end_time(sK0_skl(sK2_skl)))|~sQ85_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f633])).
% 0.18/0.67 fof(f636,plain,(
% 0.18/0.67 ~sQ46_spl|sQ85_spl|~sQ13_spl|~sQ65_spl|~sQ5_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f631,f383,f633,f156,f514,f104])).
% 0.18/0.67 fof(f711,plain,(
% 0.18/0.67 ![X0]: (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,end_time(sK0_skl(sK2_skl)))|selection_favors(efficient_producers,first_movers,end_time(sK0_skl(sK2_skl)))|~sQ75_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f572,f23])).
% 0.18/0.67 fof(f713,definition,(
% 0.18/0.67 ![X0]: (sQ99_spl <=> (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,end_time(sK0_skl(sK2_skl)))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f714,plain,(
% 0.18/0.67 ![X0]: (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,end_time(sK0_skl(sK2_skl)))|~sQ99_spl)),
% 0.18/0.67 inference(component_clause,[status(thm)],[f713])).
% 0.18/0.67 fof(f716,plain,(
% 0.18/0.67 sQ99_spl|sQ85_spl|~sQ75_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f711,f713,f633,f571])).
% 0.18/0.67 fof(f717,plain,(
% 0.18/0.67 ~environment(sK0_skl(sK2_skl))|~sQ83_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f616,f94])).
% 0.18/0.67 fof(f720,plain,(
% 0.18/0.67 $false|~sQ5_spl|~sQ83_spl),
% 0.18/0.67 inference(forward_subsumption_resolution,[status(thm)],[f717,f105])).
% 0.18/0.67 fof(f721,plain,(
% 0.18/0.67 ~sQ5_spl|~sQ83_spl),
% 0.18/0.67 inference(contradiction_clause,[status(thm)],[f720])).
% 0.18/0.67 fof(f735,plain,(
% 0.18/0.67 ~observational_period(sK2_skl)|selection_favors(efficient_producers,first_movers,sK2_skl)|~sQ85_spl|~sQ4_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f634,f90])).
% 0.18/0.67 fof(f736,plain,(
% 0.18/0.67 ~sQ14_spl|sQ6_spl|~sQ85_spl|~sQ4_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f735,f163,f107,f633,f89])).
% 0.18/0.67 fof(f737,plain,(
% 0.18/0.67 ![X0]: (~environment(X0)|~in_environment(X0,end_time(sK0_skl(sK2_skl)))|~sQ99_spl|~sQ55_spl)),
% 0.18/0.67 inference(backward_subsumption_resolution,[status(thm)],[f454,f714])).
% 0.18/0.67 fof(f744,plain,(
% 0.18/0.67 ~environment(sK0_skl(sK2_skl))|~sQ99_spl|~sQ55_spl|~sQ13_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f737,f157])).
% 0.18/0.67 fof(f745,plain,(
% 0.18/0.67 $false|~sQ5_spl|~sQ99_spl|~sQ55_spl|~sQ13_spl),
% 0.18/0.67 inference(forward_subsumption_resolution,[status(thm)],[f744,f105])).
% 0.18/0.67 fof(f746,plain,(
% 0.18/0.67 ~sQ5_spl|~sQ99_spl|~sQ55_spl|~sQ13_spl),
% 0.18/0.67 inference(contradiction_clause,[status(thm)],[f745])).
% 0.18/0.67 fof(f760,plain,(
% 0.18/0.67 greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero)|~sQ35_spl|~sQ29_spl),
% 0.18/0.67 inference(backward_demodulation,[status(thm)],[f307,f283])).
% 0.18/0.67 fof(f762,plain,(
% 0.18/0.67 in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))|~sQ35_spl|~sQ15_spl),
% 0.18/0.67 inference(backward_demodulation,[status(thm)],[f307,f167])).
% 0.18/0.67 fof(f787,plain,(
% 0.18/0.67 greater_or_equal(end_time(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl)))|~sQ52_spl|~sQ5_spl),
% 0.18/0.67 inference(backward_demodulation,[status(thm)],[f421,f112])).
% 0.18/0.67 fof(f879,plain,(
% 0.18/0.67 ~in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))|greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero)|~sQ52_spl|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f787,f150])).
% 0.18/0.67 fof(f882,plain,(
% 0.18/0.67 ~sQ13_spl|sQ43_spl|~sQ52_spl|~sQ5_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f879,f156,f366,f420,f104])).
% 0.18/0.67 fof(f883,definition,(
% 0.18/0.67 sQ103_spl <=> (end_time(sK0_skl(sK2_skl))=appear(efficient_producers,sK0_skl(sK2_skl)))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f884,plain,(
% 0.18/0.67 end_time(sK0_skl(sK2_skl))=appear(efficient_producers,sK0_skl(sK2_skl))|~sQ103_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f883])).
% 0.18/0.67 fof(f890,plain,(
% 0.18/0.67 ~in_environment(sK0_skl(sK2_skl),end_time(sK0_skl(sK2_skl)))|~sQ103_spl|sQ24_spl),
% 0.18/0.67 inference(backward_demodulation,[status(thm)],[f884,f246])).
% 0.18/0.67 fof(f930,plain,(
% 0.18/0.67 sQ13_spl|~sQ35_spl|~sQ15_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f762,f156,f306,f166])).
% 0.18/0.67 fof(f935,plain,(
% 0.18/0.67 ~sQ13_spl|~sQ103_spl|sQ24_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f890,f156,f883,f244])).
% 0.18/0.67 fof(f1221,plain,(
% 0.18/0.67 ~greater_or_equal(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl)))|greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero)|~sQ10_spl|~sQ5_spl|~sQ13_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f189,f157])).
% 0.18/0.67 fof(f1222,plain,(
% 0.18/0.67 ~sQ17_spl|sQ43_spl|~sQ10_spl|~sQ5_spl|~sQ13_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f1221,f179,f366,f141,f104,f156])).
% 0.18/0.67 fof(f1232,plain,(
% 0.18/0.67 ~greater_or_equal(end_time(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl)))|greater(cardinality_at_time(efficient_producers,end_time(sK0_skl(sK2_skl))),zero)|~sQ5_spl|~sQ13_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f150,f157])).
% 0.18/0.67 fof(f1233,definition,(
% 0.18/0.67 sQ107_spl <=> (greater_or_equal(end_time(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f1235,plain,(
% 0.18/0.67 ~greater_or_equal(end_time(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl)))|sQ107_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f1233])).
% 0.18/0.67 fof(f1236,plain,(
% 0.18/0.67 ~sQ107_spl|sQ43_spl|~sQ5_spl|~sQ13_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f1232,f1233,f366,f104,f156])).
% 0.18/0.67 fof(f1244,plain,(
% 0.18/0.67 ![X0]: (greater(sK1_skl(sK0_skl(sK2_skl),X0),appear(efficient_producers,sK0_skl(sK2_skl)))|~observational_period(X0)|~slow_change(X0)|~environment(sK0_skl(sK2_skl))|~in_environment(X0,sK0_skl(sK2_skl))|~sQ9_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f160,f35])).
% 0.18/0.67 fof(f1245,definition,(
% 0.18/0.67 ![X0]: (sQ109_spl <=> (greater(sK1_skl(sK0_skl(sK2_skl),X0),appear(efficient_producers,sK0_skl(sK2_skl)))|~observational_period(X0)|~slow_change(X0)|~in_environment(X0,sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f1246,plain,(
% 0.18/0.67 ![X0]: (greater(sK1_skl(sK0_skl(sK2_skl),X0),appear(efficient_producers,sK0_skl(sK2_skl)))|~observational_period(X0)|~slow_change(X0)|~in_environment(X0,sK0_skl(sK2_skl))|~sQ109_spl)),
% 0.18/0.67 inference(component_clause,[status(thm)],[f1245])).
% 0.18/0.67 fof(f1248,plain,(
% 0.18/0.67 sQ109_spl|~sQ5_spl|~sQ9_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f1244,f1245,f104,f138])).
% 0.18/0.67 fof(f1262,plain,(
% 0.18/0.67 ~observational_period(sK2_skl)|~slow_change(sK2_skl)|~environment(sK0_skl(sK2_skl))|~in_environment(sK2_skl,sK0_skl(sK2_skl))|greater(end_time(sK0_skl(sK2_skl)),critical_point(sK0_skl(sK2_skl)))|~sQ35_spl),
% 0.18/0.67 inference(paramodulation,[status(thm)],[f307,f35])).
% 0.18/0.67 fof(f1267,plain,(
% 0.18/0.67 ~sQ14_spl|~sQ42_spl|~sQ5_spl|~sQ11_spl|sQ28_spl|~sQ35_spl),
% 0.18/0.67 inference(split_clause,[status(thm)],[f1262,f163,f355,f104,f146,f276,f306])).
% 0.18/0.67 fof(f1270,plain,(
% 0.18/0.67 $false|sQ12_spl|~sQ28_spl|~sQ7_spl),
% 0.18/0.67 inference(forward_subsumption_resolution,[status(thm)],[f429,f263])).
% 0.18/0.67 fof(f1271,plain,(
% 0.18/0.67 sQ12_spl|~sQ28_spl|~sQ7_spl),
% 0.18/0.67 inference(contradiction_clause,[status(thm)],[f1270])).
% 0.18/0.67 fof(f1347,definition,(
% 0.18/0.67 sQ112_spl <=> (greater_or_equal(critical_point(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f1349,plain,(
% 0.18/0.67 ~greater_or_equal(critical_point(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl)))|sQ112_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f1347])).
% 0.18/0.67 fof(f1363,plain,(
% 0.18/0.67 greater_or_equal(end_time(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl)))|~sQ24_spl|~sQ5_spl),
% 0.18/0.67 inference(resolution,[status(thm)],[f245,f115])).
% 0.18/0.67 fof(f1368,definition,(
% 0.18/0.67 sQ115_spl <=> (greater_or_equal(appear(efficient_producers,sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl))))),
% 0.18/0.67 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.18/0.67 fof(f1370,plain,(
% 0.18/0.67 ~greater_or_equal(appear(efficient_producers,sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl)))|sQ115_spl),
% 0.18/0.67 inference(component_clause,[status(thm)],[f1368])).
% 0.18/0.67 fof(f1372,plain,(
% 0.18/0.67 $false|sQ107_spl|~sQ24_spl|~sQ5_spl),
% 0.18/0.67 inference(forward_subsumption_resolution,[status(thm)],[f1363,f1235])).
% 0.18/0.67 fof(f1373,plain,(
% 0.18/0.67 sQ107_spl|~sQ24_spl|~sQ5_spl),
% 0.18/0.67 inference(contradiction_clause,[status(thm)],[f1372])).
% 0.18/0.67 fof(f1413,plain,(
% 0.18/0.67 ![X0]: (~greater(X0,sK1_skl(sK0_skl(sK2_skl),sK2_skl))|greater(X0,appear(efficient_producers,sK0_skl(sK2_skl)))|~sQ30_spl)),
% 0.18/0.67 inference(resolution,[status(thm)],[f286,f56])).
% 0.18/0.67 fof(f1431,plain,(
% 0.18/0.67 greater(end_time(sK0_skl(sK2_skl)),appear(efficient_producers,sK0_skl(sK2_skl)))|~sQ34_spl|~sQ30_spl),
% 0.18/0.68 inference(resolution,[status(thm)],[f304,f1413])).
% 0.18/0.68 fof(f1435,plain,(
% 0.18/0.68 sQ44_spl|~sQ34_spl|~sQ30_spl),
% 0.18/0.68 inference(split_clause,[status(thm)],[f1431,f369,f303,f285])).
% 0.18/0.68 fof(f1437,plain,(
% 0.18/0.68 $false|sQ115_spl),
% 0.18/0.68 inference(forward_subsumption_resolution,[status(thm)],[f1370,f93])).
% 0.18/0.68 fof(f1438,plain,(
% 0.18/0.68 sQ115_spl),
% 0.18/0.68 inference(contradiction_clause,[status(thm)],[f1437])).
% 0.18/0.68 fof(f1439,plain,(
% 0.18/0.68 $false|~sQ5_spl|sQ112_spl),
% 0.18/0.68 inference(forward_subsumption_resolution,[status(thm)],[f1349,f112])).
% 0.18/0.68 fof(f1440,plain,(
% 0.18/0.68 ~sQ5_spl|sQ112_spl),
% 0.18/0.68 inference(contradiction_clause,[status(thm)],[f1439])).
% 0.18/0.68 fof(f1443,plain,(
% 0.18/0.68 ~observational_period(sK2_skl)|~slow_change(sK2_skl)|~in_environment(sK2_skl,sK0_skl(sK2_skl))|sQ30_spl|~sQ109_spl),
% 0.18/0.68 inference(resolution,[status(thm)],[f287,f1246])).
% 0.18/0.68 fof(f1444,plain,(
% 0.18/0.68 ~sQ14_spl|~sQ42_spl|~sQ11_spl|sQ30_spl|~sQ109_spl),
% 0.18/0.68 inference(split_clause,[status(thm)],[f1443,f163,f355,f146,f285,f1245])).
% 0.18/0.68 fof(f1482,plain,(
% 0.18/0.68 sQ43_spl|~sQ35_spl|~sQ29_spl),
% 0.18/0.68 inference(split_clause,[status(thm)],[f760,f366,f306,f282])).
% 0.18/0.68 fof(f1487,plain,(
% 0.18/0.68 $false),
% 0.18/0.68 inference(sat_refutation,[status(thm)],[f84,f88,f92,f97,f99,f110,f126,f128,f144,f149,f159,f169,f171,f188,f254,f288,f309,f340,f358,f360,f362,f372,f386,f398,f419,f433,f456,f517,f567,f574,f625,f636,f716,f721,f736,f746,f882,f930,f935,f1222,f1236,f1248,f1267,f1271,f1373,f1435,f1438,f1440,f1444,f1482])).
% 0.18/0.68 % SZS output end CNFRefutation for theBenchmark.p
% 0.18/0.72 % Elapsed time: 0.237424 seconds
% 0.18/0.72 % CPU time: 1.370641 seconds
% 0.18/0.72 % Total memory used: 95.906 MB
% 0.18/0.72 % Net memory used: 94.880 MB
%------------------------------------------------------------------------------