%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT029+1 : 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 : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:25:44 PM UTC 2026
% Result : Theorem 0.27s 0.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT029+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n010.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 01:22:26 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.48 % Drodi V4.1.1
% 0.27/0.87 % Refutation found
% 0.27/0.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.27/0.87 % SZS output start CNFRefutation for theBenchmark
% 0.27/0.87 fof(f1,axiom,(
% 0.27/0.87 (! [X,Y,Z] :( ( greater(X,Y)& greater(Y,Z) )=> greater(X,Z) ) )),
% 0.27/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.87 fof(f2,axiom,(
% 0.27/0.87 (! [E,T1,T2] :( ( in_environment(E,T1)& in_environment(E,T2) )=> ( greater(T2,T1)| T2 = T1| greater(T1,T2) ) ) )),
% 0.27/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.87 fof(f3,axiom,(
% 0.27/0.87 (! [X,Y] :( greater_or_equal(X,Y)<=> ( greater(X,Y)| X = Y ) ) )),
% 0.27/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.87 fof(f4,hypothesis,(
% 0.27/0.87 (! [E,T] :( ( environment(E)& subpopulations(first_movers,efficient_producers,E,T)& greater_or_equal(T,equilibrium(E)) )=> ( ( growth_rate(first_movers,T) = zero& growth_rate(efficient_producers,T) = zero )| ( greater(growth_rate(first_movers,T),zero)& greater(zero,growth_rate(efficient_producers,T)) )| ( greater(growth_rate(efficient_producers,T),zero)& greater(zero,growth_rate(first_movers,T)) ) ) ) )),
% 0.27/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.87 fof(f5,hypothesis,(
% 0.27/0.87 (! [E] :( ( environment(E)& stable(E) )=> (? [To] :( in_environment(E,To)& (! [T] :( ( subpopulations(first_movers,efficient_producers,E,T)& greater_or_equal(T,To) )=> greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) )) )) )),
% 0.27/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.87 fof(f6,hypothesis,(
% 0.27/0.87 (! [E] :( ( environment(E)& stable(E) )=> (? [T] :( in_environment(E,T)& greater_or_equal(T,equilibrium(E)) ) )) )),
% 0.27/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.87 fof(f7,conjecture,(
% 0.27/0.87 (! [E] :( ( environment(E)& stable(E) )=> (? [To] :( in_environment(E,To)& (! [T] :( ( subpopulations(first_movers,efficient_producers,E,T)& greater_or_equal(T,To) )=> ( greater(growth_rate(efficient_producers,T),zero)& greater(zero,growth_rate(first_movers,T)) ) ) )) )) )),
% 0.27/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.27/0.87 fof(f8,negated_conjecture,(
% 0.27/0.87 ~((! [E] :( ( environment(E)& stable(E) )=> (? [To] :( in_environment(E,To)& (! [T] :( ( subpopulations(first_movers,efficient_producers,E,T)& greater_or_equal(T,To) )=> ( greater(growth_rate(efficient_producers,T),zero)& greater(zero,growth_rate(first_movers,T)) ) ) )) )) ))),
% 0.27/0.87 inference(negated_conjecture,[status(cth)],[f7])).
% 0.27/0.87 fof(f9,plain,(
% 0.27/0.87 ![X,Y,Z]: ((~greater(X,Y)|~greater(Y,Z))|greater(X,Z))),
% 0.27/0.87 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.27/0.87 fof(f10,plain,(
% 0.27/0.87 ![X,Z]: ((![Y]: (~greater(X,Y)|~greater(Y,Z)))|greater(X,Z))),
% 0.27/0.87 inference(miniscoping,[status(thm)],[f9])).
% 0.27/0.87 fof(f11,plain,(
% 0.27/0.87 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f10])).
% 0.27/0.87 fof(f12,plain,(
% 0.27/0.87 ![E,T1,T2]: ((~in_environment(E,T1)|~in_environment(E,T2))|((greater(T2,T1)|T2=T1)|greater(T1,T2)))),
% 0.27/0.87 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.27/0.87 fof(f13,plain,(
% 0.27/0.87 ![T1,T2]: ((![E]: (~in_environment(E,T1)|~in_environment(E,T2)))|((greater(T2,T1)|T2=T1)|greater(T1,T2)))),
% 0.27/0.87 inference(miniscoping,[status(thm)],[f12])).
% 0.27/0.87 fof(f14,plain,(
% 0.27/0.87 ![X0,X1,X2]: (~in_environment(X0,X1)|~in_environment(X0,X2)|greater(X2,X1)|X2=X1|greater(X1,X2))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f13])).
% 0.27/0.87 fof(f15,plain,(
% 0.27/0.87 ![X,Y]: ((~greater_or_equal(X,Y)|(greater(X,Y)|X=Y))&(greater_or_equal(X,Y)|(~greater(X,Y)&~X=Y)))),
% 0.27/0.87 inference(NNF_transformation,[status(thm)],[f3])).
% 0.27/0.87 fof(f16,plain,(
% 0.27/0.87 (![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.27/0.87 inference(miniscoping,[status(thm)],[f15])).
% 0.27/0.87 fof(f17,plain,(
% 0.27/0.87 ![X0,X1]: (~greater_or_equal(X0,X1)|greater(X0,X1)|X0=X1)),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f16])).
% 0.27/0.87 fof(f18,plain,(
% 0.27/0.87 ![X0,X1]: (greater_or_equal(X0,X1)|~greater(X0,X1))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f16])).
% 0.27/0.87 fof(f19,plain,(
% 0.27/0.87 ![X0,X1]: (greater_or_equal(X0,X1)|~X0=X1)),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f16])).
% 0.27/0.87 fof(f20,plain,(
% 0.27/0.87 ![E,T]: (((~environment(E)|~subpopulations(first_movers,efficient_producers,E,T))|~greater_or_equal(T,equilibrium(E)))|(((growth_rate(first_movers,T)=zero&growth_rate(efficient_producers,T)=zero)|(greater(growth_rate(first_movers,T),zero)&greater(zero,growth_rate(efficient_producers,T))))|(greater(growth_rate(efficient_producers,T),zero)&greater(zero,growth_rate(first_movers,T)))))),
% 0.27/0.87 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.27/0.87 fof(f21,definition,(
% 0.27/0.87 ![T]: (sP0_prd(T)<=>((growth_rate(first_movers,T)=zero&growth_rate(efficient_producers,T)=zero)|(greater(growth_rate(first_movers,T),zero)&greater(zero,growth_rate(efficient_producers,T)))))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.27/0.87 fof(f22,plain,(
% 0.27/0.87 ![E,T]: (((~environment(E)|~subpopulations(first_movers,efficient_producers,E,T))|~greater_or_equal(T,equilibrium(E)))|(sP0_prd(T)|(greater(growth_rate(efficient_producers,T),zero)&greater(zero,growth_rate(first_movers,T)))))),
% 0.27/0.87 inference(formula_renaming,[status(thm)],[f20,f21])).
% 0.27/0.87 fof(f23,plain,(
% 0.27/0.87 ![T]: ((![E]: ((~environment(E)|~subpopulations(first_movers,efficient_producers,E,T))|~greater_or_equal(T,equilibrium(E))))|(sP0_prd(T)|(greater(growth_rate(efficient_producers,T),zero)&greater(zero,growth_rate(first_movers,T)))))),
% 0.27/0.87 inference(miniscoping,[status(thm)],[f22])).
% 0.27/0.87 fof(f24,plain,(
% 0.27/0.87 ![X0,X1]: (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,equilibrium(X0))|sP0_prd(X1)|greater(growth_rate(efficient_producers,X1),zero))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f23])).
% 0.27/0.87 fof(f25,plain,(
% 0.27/0.87 ![X0,X1]: (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,equilibrium(X0))|sP0_prd(X1)|greater(zero,growth_rate(first_movers,X1)))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f23])).
% 0.27/0.87 fof(f26,plain,(
% 0.27/0.87 ![E]: ((~environment(E)|~stable(E))|(?[To]: (in_environment(E,To)&(![T]: ((~subpopulations(first_movers,efficient_producers,E,T)|~greater_or_equal(T,To))|greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)))))))),
% 0.27/0.87 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.27/0.87 fof(f27,plain,(
% 0.27/0.87 ![E]: ((~environment(E)|~stable(E))|(in_environment(E,sK0_skl(E))&(![T]: ((~subpopulations(first_movers,efficient_producers,E,T)|~greater_or_equal(T,sK0_skl(E)))|greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T))))))),
% 0.27/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(To,sK0_skl(E))],[f26])).
% 0.27/0.87 fof(f28,plain,(
% 0.27/0.87 ![X0]: (~environment(X0)|~stable(X0)|in_environment(X0,sK0_skl(X0)))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f27])).
% 0.27/0.87 fof(f29,plain,(
% 0.27/0.87 ![X0,X1]: (~environment(X0)|~stable(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,sK0_skl(X0))|greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1)))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f27])).
% 0.27/0.87 fof(f30,plain,(
% 0.27/0.87 ![E]: ((~environment(E)|~stable(E))|(?[T]: (in_environment(E,T)&greater_or_equal(T,equilibrium(E)))))),
% 0.27/0.87 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 0.27/0.87 fof(f31,plain,(
% 0.27/0.87 ![E]: ((~environment(E)|~stable(E))|(in_environment(E,sK1_skl(E))&greater_or_equal(sK1_skl(E),equilibrium(E))))),
% 0.27/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(T,sK1_skl(E))],[f30])).
% 0.27/0.87 fof(f32,plain,(
% 0.27/0.87 ![X0]: (~environment(X0)|~stable(X0)|in_environment(X0,sK1_skl(X0)))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f31])).
% 0.27/0.87 fof(f33,plain,(
% 0.27/0.87 ![X0]: (~environment(X0)|~stable(X0)|greater_or_equal(sK1_skl(X0),equilibrium(X0)))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f31])).
% 0.27/0.87 fof(f34,plain,(
% 0.27/0.87 (?[E]: ((environment(E)&stable(E))&(![To]: (~in_environment(E,To)|(?[T]: ((subpopulations(first_movers,efficient_producers,E,T)&greater_or_equal(T,To))&(~greater(growth_rate(efficient_producers,T),zero)|~greater(zero,growth_rate(first_movers,T)))))))))),
% 0.27/0.87 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.27/0.87 fof(f35,plain,(
% 0.27/0.87 ((environment(sK2_skl)&stable(sK2_skl))&(![To]: (~in_environment(sK2_skl,To)|((subpopulations(first_movers,efficient_producers,sK2_skl,sK3_skl(To))&greater_or_equal(sK3_skl(To),To))&(~greater(growth_rate(efficient_producers,sK3_skl(To)),zero)|~greater(zero,growth_rate(first_movers,sK3_skl(To))))))))),
% 0.27/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(E,sK2_skl),skolemize(T,sK3_skl(To))],[f34])).
% 0.27/0.87 fof(f36,plain,(
% 0.27/0.87 environment(sK2_skl)),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f35])).
% 0.27/0.87 fof(f37,plain,(
% 0.27/0.87 stable(sK2_skl)),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f35])).
% 0.27/0.87 fof(f38,plain,(
% 0.27/0.87 ![X0]: (~in_environment(sK2_skl,X0)|subpopulations(first_movers,efficient_producers,sK2_skl,sK3_skl(X0)))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f35])).
% 0.27/0.87 fof(f39,plain,(
% 0.27/0.87 ![X0]: (~in_environment(sK2_skl,X0)|greater_or_equal(sK3_skl(X0),X0))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f35])).
% 0.27/0.87 fof(f40,plain,(
% 0.27/0.87 ![X0]: (~in_environment(sK2_skl,X0)|~greater(growth_rate(efficient_producers,sK3_skl(X0)),zero)|~greater(zero,growth_rate(first_movers,sK3_skl(X0))))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f35])).
% 0.27/0.87 fof(f41,plain,(
% 0.27/0.87 ![T]: ((~sP0_prd(T)|((growth_rate(first_movers,T)=zero&growth_rate(efficient_producers,T)=zero)|(greater(growth_rate(first_movers,T),zero)&greater(zero,growth_rate(efficient_producers,T)))))&(sP0_prd(T)|((~growth_rate(first_movers,T)=zero|~growth_rate(efficient_producers,T)=zero)&(~greater(growth_rate(first_movers,T),zero)|~greater(zero,growth_rate(efficient_producers,T))))))),
% 0.27/0.87 inference(NNF_transformation,[status(thm)],[f21])).
% 0.27/0.87 fof(f42,plain,(
% 0.27/0.87 (![T]: (~sP0_prd(T)|((growth_rate(first_movers,T)=zero&growth_rate(efficient_producers,T)=zero)|(greater(growth_rate(first_movers,T),zero)&greater(zero,growth_rate(efficient_producers,T))))))&(![T]: (sP0_prd(T)|((~growth_rate(first_movers,T)=zero|~growth_rate(efficient_producers,T)=zero)&(~greater(growth_rate(first_movers,T),zero)|~greater(zero,growth_rate(efficient_producers,T))))))),
% 0.27/0.87 inference(miniscoping,[status(thm)],[f41])).
% 0.27/0.87 fof(f43,plain,(
% 0.27/0.87 ![X0]: (~sP0_prd(X0)|growth_rate(first_movers,X0)=zero|greater(growth_rate(first_movers,X0),zero))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f42])).
% 0.27/0.87 fof(f44,plain,(
% 0.27/0.87 ![X0]: (~sP0_prd(X0)|growth_rate(first_movers,X0)=zero|greater(zero,growth_rate(efficient_producers,X0)))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f42])).
% 0.27/0.87 fof(f45,plain,(
% 0.27/0.87 ![X0]: (~sP0_prd(X0)|growth_rate(efficient_producers,X0)=zero|greater(growth_rate(first_movers,X0),zero))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f42])).
% 0.27/0.87 fof(f46,plain,(
% 0.27/0.87 ![X0]: (~sP0_prd(X0)|growth_rate(efficient_producers,X0)=zero|greater(zero,growth_rate(efficient_producers,X0)))),
% 0.27/0.87 inference(cnf_transformation,[status(thm)],[f42])).
% 0.27/0.87 fof(f49,plain,(
% 0.27/0.87 ![X0]: (greater_or_equal(X0,X0))),
% 0.27/0.87 inference(destructive_equality_resolution,[status(thm)],[f19])).
% 0.27/0.87 fof(f51,plain,(
% 0.27/0.87 ~environment(sK2_skl)|in_environment(sK2_skl,sK0_skl(sK2_skl))),
% 0.27/0.87 inference(resolution,[status(thm)],[f28,f37])).
% 0.27/0.87 fof(f52,definition,(
% 0.27/0.87 sQ0_spl <=> (environment(sK2_skl))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f54,plain,(
% 0.27/0.87 ~environment(sK2_skl)|sQ0_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f52])).
% 0.27/0.87 fof(f55,definition,(
% 0.27/0.87 sQ1_spl <=> (in_environment(sK2_skl,sK0_skl(sK2_skl)))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f56,plain,(
% 0.27/0.87 in_environment(sK2_skl,sK0_skl(sK2_skl))|~sQ1_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f55])).
% 0.27/0.87 fof(f58,plain,(
% 0.27/0.87 ~sQ0_spl|sQ1_spl),
% 0.27/0.87 inference(split_clause,[status(thm)],[f51,f52,f55])).
% 0.27/0.87 fof(f59,plain,(
% 0.27/0.87 $false|sQ0_spl),
% 0.27/0.87 inference(forward_subsumption_resolution,[status(thm)],[f54,f36])).
% 0.27/0.87 fof(f60,plain,(
% 0.27/0.87 sQ0_spl),
% 0.27/0.87 inference(contradiction_clause,[status(thm)],[f59])).
% 0.27/0.87 fof(f61,plain,(
% 0.27/0.87 greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),sK0_skl(sK2_skl))|~sQ1_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f56,f39])).
% 0.27/0.87 fof(f62,plain,(
% 0.27/0.87 subpopulations(first_movers,efficient_producers,sK2_skl,sK3_skl(sK0_skl(sK2_skl)))|~sQ1_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f56,f38])).
% 0.27/0.87 fof(f63,plain,(
% 0.27/0.87 ![X0]: (~in_environment(sK2_skl,X0)|greater(X0,sK0_skl(sK2_skl))|X0=sK0_skl(sK2_skl)|greater(sK0_skl(sK2_skl),X0)|~sQ1_spl)),
% 0.27/0.87 inference(resolution,[status(thm)],[f56,f14])).
% 0.27/0.87 fof(f64,plain,(
% 0.27/0.87 ~environment(sK2_skl)|in_environment(sK2_skl,sK1_skl(sK2_skl))),
% 0.27/0.87 inference(resolution,[status(thm)],[f32,f37])).
% 0.27/0.87 fof(f65,definition,(
% 0.27/0.87 sQ2_spl <=> (in_environment(sK2_skl,sK1_skl(sK2_skl)))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f66,plain,(
% 0.27/0.87 in_environment(sK2_skl,sK1_skl(sK2_skl))|~sQ2_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f65])).
% 0.27/0.87 fof(f68,plain,(
% 0.27/0.87 ~sQ0_spl|sQ2_spl),
% 0.27/0.87 inference(split_clause,[status(thm)],[f64,f52,f65])).
% 0.27/0.87 fof(f69,plain,(
% 0.27/0.87 ~environment(sK2_skl)|greater_or_equal(sK1_skl(sK2_skl),equilibrium(sK2_skl))),
% 0.27/0.87 inference(resolution,[status(thm)],[f33,f37])).
% 0.27/0.87 fof(f70,definition,(
% 0.27/0.87 sQ3_spl <=> (greater_or_equal(sK1_skl(sK2_skl),equilibrium(sK2_skl)))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f71,plain,(
% 0.27/0.87 greater_or_equal(sK1_skl(sK2_skl),equilibrium(sK2_skl))|~sQ3_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f70])).
% 0.27/0.87 fof(f73,plain,(
% 0.27/0.87 ~sQ0_spl|sQ3_spl),
% 0.27/0.87 inference(split_clause,[status(thm)],[f69,f52,f70])).
% 0.27/0.87 fof(f74,plain,(
% 0.27/0.87 greater_or_equal(sK3_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl))|~sQ2_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f66,f39])).
% 0.27/0.87 fof(f75,plain,(
% 0.27/0.87 subpopulations(first_movers,efficient_producers,sK2_skl,sK3_skl(sK1_skl(sK2_skl)))|~sQ2_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f66,f38])).
% 0.27/0.87 fof(f77,plain,(
% 0.27/0.87 greater(sK1_skl(sK2_skl),equilibrium(sK2_skl))|sK1_skl(sK2_skl)=equilibrium(sK2_skl)|~sQ3_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f71,f17])).
% 0.27/0.87 fof(f78,definition,(
% 0.27/0.87 sQ4_spl <=> (greater(sK1_skl(sK2_skl),equilibrium(sK2_skl)))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f79,plain,(
% 0.27/0.87 greater(sK1_skl(sK2_skl),equilibrium(sK2_skl))|~sQ4_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f78])).
% 0.27/0.87 fof(f81,definition,(
% 0.27/0.87 sQ5_spl <=> (sK1_skl(sK2_skl)=equilibrium(sK2_skl))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f82,plain,(
% 0.27/0.87 sK1_skl(sK2_skl)=equilibrium(sK2_skl)|~sQ5_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f81])).
% 0.27/0.87 fof(f84,plain,(
% 0.27/0.87 sQ4_spl|sQ5_spl|~sQ3_spl),
% 0.27/0.87 inference(split_clause,[status(thm)],[f77,f78,f81,f70])).
% 0.27/0.87 fof(f85,plain,(
% 0.27/0.87 greater(sK3_skl(sK0_skl(sK2_skl)),sK0_skl(sK2_skl))|sK3_skl(sK0_skl(sK2_skl))=sK0_skl(sK2_skl)|~sQ1_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f61,f17])).
% 0.27/0.87 fof(f86,definition,(
% 0.27/0.87 sQ6_spl <=> (greater(sK3_skl(sK0_skl(sK2_skl)),sK0_skl(sK2_skl)))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f87,plain,(
% 0.27/0.87 greater(sK3_skl(sK0_skl(sK2_skl)),sK0_skl(sK2_skl))|~sQ6_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f86])).
% 0.27/0.87 fof(f89,definition,(
% 0.27/0.87 sQ7_spl <=> (sK3_skl(sK0_skl(sK2_skl))=sK0_skl(sK2_skl))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f90,plain,(
% 0.27/0.87 sK3_skl(sK0_skl(sK2_skl))=sK0_skl(sK2_skl)|~sQ7_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f89])).
% 0.27/0.87 fof(f92,plain,(
% 0.27/0.87 sQ6_spl|sQ7_spl|~sQ1_spl),
% 0.27/0.87 inference(split_clause,[status(thm)],[f85,f86,f89,f55])).
% 0.27/0.87 fof(f95,plain,(
% 0.27/0.87 greater(sK3_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl))|sK3_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|~sQ2_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f74,f17])).
% 0.27/0.87 fof(f96,definition,(
% 0.27/0.87 sQ8_spl <=> (greater(sK3_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl)))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f97,plain,(
% 0.27/0.87 greater(sK3_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl))|~sQ8_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f96])).
% 0.27/0.87 fof(f99,definition,(
% 0.27/0.87 sQ9_spl <=> (sK3_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f100,plain,(
% 0.27/0.87 sK3_skl(sK1_skl(sK2_skl))=sK1_skl(sK2_skl)|~sQ9_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f99])).
% 0.27/0.87 fof(f102,plain,(
% 0.27/0.87 sQ8_spl|sQ9_spl|~sQ2_spl),
% 0.27/0.87 inference(split_clause,[status(thm)],[f95,f96,f99,f65])).
% 0.27/0.87 fof(f103,plain,(
% 0.27/0.87 ~environment(sK2_skl)|~stable(sK2_skl)|~greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),sK0_skl(sK2_skl))|greater(growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))),growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))))|~sQ1_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f62,f29])).
% 0.27/0.87 fof(f104,plain,(
% 0.27/0.87 ~environment(sK2_skl)|~greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),equilibrium(sK2_skl))|sP0_prd(sK3_skl(sK0_skl(sK2_skl)))|greater(zero,growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))))|~sQ1_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f62,f25])).
% 0.27/0.87 fof(f105,plain,(
% 0.27/0.87 ~environment(sK2_skl)|~greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),equilibrium(sK2_skl))|sP0_prd(sK3_skl(sK0_skl(sK2_skl)))|greater(growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))),zero)|~sQ1_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f62,f24])).
% 0.27/0.87 fof(f106,definition,(
% 0.27/0.87 sQ10_spl <=> (stable(sK2_skl))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f108,plain,(
% 0.27/0.87 ~stable(sK2_skl)|sQ10_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f106])).
% 0.27/0.87 fof(f109,definition,(
% 0.27/0.87 sQ11_spl <=> (greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),sK0_skl(sK2_skl)))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f111,plain,(
% 0.27/0.87 ~greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),sK0_skl(sK2_skl))|sQ11_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f109])).
% 0.27/0.87 fof(f112,definition,(
% 0.27/0.87 sQ12_spl <=> (greater(growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))),growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl)))))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f113,plain,(
% 0.27/0.87 greater(growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))),growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))))|~sQ12_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f112])).
% 0.27/0.87 fof(f115,plain,(
% 0.27/0.87 ~sQ0_spl|~sQ10_spl|~sQ11_spl|sQ12_spl|~sQ1_spl),
% 0.27/0.87 inference(split_clause,[status(thm)],[f103,f52,f106,f109,f112,f55])).
% 0.27/0.87 fof(f116,definition,(
% 0.27/0.87 sQ13_spl <=> (greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),equilibrium(sK2_skl)))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f118,plain,(
% 0.27/0.87 ~greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),equilibrium(sK2_skl))|sQ13_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f116])).
% 0.27/0.87 fof(f119,definition,(
% 0.27/0.87 sQ14_spl <=> (sP0_prd(sK3_skl(sK0_skl(sK2_skl))))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f120,plain,(
% 0.27/0.87 sP0_prd(sK3_skl(sK0_skl(sK2_skl)))|~sQ14_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f119])).
% 0.27/0.87 fof(f121,plain,(
% 0.27/0.87 ~sP0_prd(sK3_skl(sK0_skl(sK2_skl)))|sQ14_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f119])).
% 0.27/0.87 fof(f122,definition,(
% 0.27/0.87 sQ15_spl <=> (greater(zero,growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl)))))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f124,plain,(
% 0.27/0.87 ~greater(zero,growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))))|sQ15_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f122])).
% 0.27/0.87 fof(f125,plain,(
% 0.27/0.87 ~sQ0_spl|~sQ13_spl|sQ14_spl|sQ15_spl|~sQ1_spl),
% 0.27/0.87 inference(split_clause,[status(thm)],[f104,f52,f116,f119,f122,f55])).
% 0.27/0.87 fof(f126,definition,(
% 0.27/0.87 sQ16_spl <=> (greater(growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))),zero))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f127,plain,(
% 0.27/0.87 greater(growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))),zero)|~sQ16_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f126])).
% 0.27/0.87 fof(f129,plain,(
% 0.27/0.87 ~sQ0_spl|~sQ13_spl|sQ14_spl|sQ16_spl|~sQ1_spl),
% 0.27/0.87 inference(split_clause,[status(thm)],[f105,f52,f116,f119,f126,f55])).
% 0.27/0.87 fof(f130,plain,(
% 0.27/0.87 greater(sK1_skl(sK2_skl),sK0_skl(sK2_skl))|sK1_skl(sK2_skl)=sK0_skl(sK2_skl)|greater(sK0_skl(sK2_skl),sK1_skl(sK2_skl))|~sQ1_spl|~sQ2_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f63,f66])).
% 0.27/0.87 fof(f132,definition,(
% 0.27/0.87 sQ17_spl <=> (greater(sK1_skl(sK2_skl),sK0_skl(sK2_skl)))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f133,plain,(
% 0.27/0.87 greater(sK1_skl(sK2_skl),sK0_skl(sK2_skl))|~sQ17_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f132])).
% 0.27/0.87 fof(f135,definition,(
% 0.27/0.87 sQ18_spl <=> (sK1_skl(sK2_skl)=sK0_skl(sK2_skl))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f136,plain,(
% 0.27/0.87 sK1_skl(sK2_skl)=sK0_skl(sK2_skl)|~sQ18_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f135])).
% 0.27/0.87 fof(f138,definition,(
% 0.27/0.87 sQ19_spl <=> (greater(sK0_skl(sK2_skl),sK1_skl(sK2_skl)))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f139,plain,(
% 0.27/0.87 greater(sK0_skl(sK2_skl),sK1_skl(sK2_skl))|~sQ19_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f138])).
% 0.27/0.87 fof(f141,plain,(
% 0.27/0.87 sQ17_spl|sQ18_spl|sQ19_spl|~sQ1_spl|~sQ2_spl),
% 0.27/0.87 inference(split_clause,[status(thm)],[f130,f132,f135,f138,f55,f65])).
% 0.27/0.87 fof(f149,plain,(
% 0.27/0.87 ~environment(sK2_skl)|~stable(sK2_skl)|~greater_or_equal(sK3_skl(sK1_skl(sK2_skl)),sK0_skl(sK2_skl))|greater(growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl))),growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))))|~sQ2_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f75,f29])).
% 0.27/0.87 fof(f150,plain,(
% 0.27/0.87 ~environment(sK2_skl)|~greater_or_equal(sK3_skl(sK1_skl(sK2_skl)),equilibrium(sK2_skl))|sP0_prd(sK3_skl(sK1_skl(sK2_skl)))|greater(zero,growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))))|~sQ2_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f75,f25])).
% 0.27/0.87 fof(f151,plain,(
% 0.27/0.87 ~environment(sK2_skl)|~greater_or_equal(sK3_skl(sK1_skl(sK2_skl)),equilibrium(sK2_skl))|sP0_prd(sK3_skl(sK1_skl(sK2_skl)))|greater(growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl))),zero)|~sQ2_spl),
% 0.27/0.87 inference(resolution,[status(thm)],[f75,f24])).
% 0.27/0.87 fof(f152,definition,(
% 0.27/0.87 sQ22_spl <=> (greater_or_equal(sK3_skl(sK1_skl(sK2_skl)),sK0_skl(sK2_skl)))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f154,plain,(
% 0.27/0.87 ~greater_or_equal(sK3_skl(sK1_skl(sK2_skl)),sK0_skl(sK2_skl))|sQ22_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f152])).
% 0.27/0.87 fof(f155,definition,(
% 0.27/0.87 sQ23_spl <=> (greater(growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl))),growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl)))))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f156,plain,(
% 0.27/0.87 greater(growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl))),growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))))|~sQ23_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f155])).
% 0.27/0.87 fof(f158,plain,(
% 0.27/0.87 ~sQ0_spl|~sQ10_spl|~sQ22_spl|sQ23_spl|~sQ2_spl),
% 0.27/0.87 inference(split_clause,[status(thm)],[f149,f52,f106,f152,f155,f65])).
% 0.27/0.87 fof(f159,definition,(
% 0.27/0.87 sQ24_spl <=> (greater_or_equal(sK3_skl(sK1_skl(sK2_skl)),equilibrium(sK2_skl)))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f161,plain,(
% 0.27/0.87 ~greater_or_equal(sK3_skl(sK1_skl(sK2_skl)),equilibrium(sK2_skl))|sQ24_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f159])).
% 0.27/0.87 fof(f162,definition,(
% 0.27/0.87 sQ25_spl <=> (sP0_prd(sK3_skl(sK1_skl(sK2_skl))))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f163,plain,(
% 0.27/0.87 sP0_prd(sK3_skl(sK1_skl(sK2_skl)))|~sQ25_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f162])).
% 0.27/0.87 fof(f165,definition,(
% 0.27/0.87 sQ26_spl <=> (greater(zero,growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl)))))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.27/0.87 fof(f166,plain,(
% 0.27/0.87 greater(zero,growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))))|~sQ26_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f165])).
% 0.27/0.87 fof(f167,plain,(
% 0.27/0.87 ~greater(zero,growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))))|sQ26_spl),
% 0.27/0.87 inference(component_clause,[status(thm)],[f165])).
% 0.27/0.87 fof(f168,plain,(
% 0.27/0.87 ~sQ0_spl|~sQ24_spl|sQ25_spl|sQ26_spl|~sQ2_spl),
% 0.27/0.87 inference(split_clause,[status(thm)],[f150,f52,f159,f162,f165,f65])).
% 0.27/0.87 fof(f169,definition,(
% 0.27/0.87 sQ27_spl <=> (greater(growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl))),zero))),
% 0.27/0.87 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f170,plain,(
% 0.27/0.89 greater(growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl))),zero)|~sQ27_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f169])).
% 0.27/0.89 fof(f172,plain,(
% 0.27/0.89 ~sQ0_spl|~sQ24_spl|sQ25_spl|sQ27_spl|~sQ2_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f151,f52,f159,f162,f169,f65])).
% 0.27/0.89 fof(f173,plain,(
% 0.27/0.89 $false|sQ10_spl),
% 0.27/0.89 inference(forward_subsumption_resolution,[status(thm)],[f108,f37])).
% 0.27/0.89 fof(f174,plain,(
% 0.27/0.89 sQ10_spl),
% 0.27/0.89 inference(contradiction_clause,[status(thm)],[f173])).
% 0.27/0.89 fof(f175,plain,(
% 0.27/0.89 $false|~sQ1_spl|sQ11_spl),
% 0.27/0.89 inference(forward_subsumption_resolution,[status(thm)],[f111,f61])).
% 0.27/0.89 fof(f176,plain,(
% 0.27/0.89 ~sQ1_spl|sQ11_spl),
% 0.27/0.89 inference(contradiction_clause,[status(thm)],[f175])).
% 0.27/0.89 fof(f187,plain,(
% 0.27/0.89 growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl)))=zero|greater(growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))),zero)|~sQ14_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f120,f43])).
% 0.27/0.89 fof(f188,definition,(
% 0.27/0.89 sQ30_spl <=> (growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl)))=zero)),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f189,plain,(
% 0.27/0.89 growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl)))=zero|~sQ30_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f188])).
% 0.27/0.89 fof(f191,definition,(
% 0.27/0.89 sQ31_spl <=> (greater(growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))),zero))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f192,plain,(
% 0.27/0.89 greater(growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))),zero)|~sQ31_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f191])).
% 0.27/0.89 fof(f194,plain,(
% 0.27/0.89 sQ30_spl|sQ31_spl|~sQ14_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f187,f188,f191,f119])).
% 0.27/0.89 fof(f195,plain,(
% 0.27/0.89 growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl)))=zero|greater(growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))),zero)|~sQ25_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f163,f43])).
% 0.27/0.89 fof(f196,definition,(
% 0.27/0.89 sQ32_spl <=> (growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl)))=zero)),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f197,plain,(
% 0.27/0.89 growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl)))=zero|~sQ32_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f196])).
% 0.27/0.89 fof(f199,definition,(
% 0.27/0.89 sQ33_spl <=> (greater(growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))),zero))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f200,plain,(
% 0.27/0.89 greater(growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))),zero)|~sQ33_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f199])).
% 0.27/0.89 fof(f202,plain,(
% 0.27/0.89 sQ32_spl|sQ33_spl|~sQ25_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f195,f196,f199,f162])).
% 0.27/0.89 fof(f205,plain,(
% 0.27/0.89 ![X0]: (~greater(sK0_skl(sK2_skl),X0)|greater(sK3_skl(sK0_skl(sK2_skl)),X0)|~sQ6_spl)),
% 0.27/0.89 inference(resolution,[status(thm)],[f87,f11])).
% 0.27/0.89 fof(f207,plain,(
% 0.27/0.89 ![X0]: (~greater(sK1_skl(sK2_skl),X0)|greater(sK0_skl(sK2_skl),X0)|~sQ19_spl)),
% 0.27/0.89 inference(resolution,[status(thm)],[f139,f11])).
% 0.27/0.89 fof(f208,plain,(
% 0.27/0.89 greater_or_equal(sK0_skl(sK2_skl),sK1_skl(sK2_skl))|~sQ19_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f139,f18])).
% 0.27/0.89 fof(f209,plain,(
% 0.27/0.89 ![X0]: (~greater(sK1_skl(sK2_skl),X0)|greater(sK3_skl(sK1_skl(sK2_skl)),X0)|~sQ8_spl)),
% 0.27/0.89 inference(resolution,[status(thm)],[f97,f11])).
% 0.27/0.89 fof(f215,plain,(
% 0.27/0.89 ~in_environment(sK2_skl,sK1_skl(sK2_skl))|~greater(zero,growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))))|~sQ27_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f170,f40])).
% 0.27/0.89 fof(f218,plain,(
% 0.27/0.89 ~sQ2_spl|~sQ26_spl|~sQ27_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f215,f65,f165,f169])).
% 0.27/0.89 fof(f222,definition,(
% 0.27/0.89 sQ34_spl <=> (greater(zero,zero))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f224,plain,(
% 0.27/0.89 ~greater(zero,zero)|sQ34_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f222])).
% 0.27/0.89 fof(f225,definition,(
% 0.27/0.89 sQ35_spl <=> (greater(zero,growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl)))))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f226,plain,(
% 0.27/0.89 greater(zero,growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))))|~sQ35_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f225])).
% 0.27/0.89 fof(f235,plain,(
% 0.27/0.89 ~greater_or_equal(sK3_skl(sK1_skl(sK2_skl)),sK1_skl(sK2_skl))|~sQ5_spl|sQ24_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f82,f161])).
% 0.27/0.89 fof(f240,plain,(
% 0.27/0.89 $false|~sQ2_spl|~sQ5_spl|sQ24_spl),
% 0.27/0.89 inference(forward_subsumption_resolution,[status(thm)],[f235,f74])).
% 0.27/0.89 fof(f241,plain,(
% 0.27/0.89 ~sQ2_spl|~sQ5_spl|sQ24_spl),
% 0.27/0.89 inference(contradiction_clause,[status(thm)],[f240])).
% 0.27/0.89 fof(f249,plain,(
% 0.27/0.89 ~greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),sK0_skl(sK2_skl))|~sQ18_spl|sQ22_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f136,f154])).
% 0.27/0.89 fof(f259,plain,(
% 0.27/0.89 ~sQ11_spl|~sQ18_spl|sQ22_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f249,f109,f135,f152])).
% 0.27/0.89 fof(f273,plain,(
% 0.27/0.89 growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl)))=zero|greater(zero,growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))))|~sQ14_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f120,f46])).
% 0.27/0.89 fof(f274,plain,(
% 0.27/0.89 growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl)))=zero|greater(growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))),zero)|~sQ14_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f120,f45])).
% 0.27/0.89 fof(f275,plain,(
% 0.27/0.89 growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl)))=zero|greater(zero,growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))))|~sQ14_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f120,f44])).
% 0.27/0.89 fof(f277,definition,(
% 0.27/0.89 sQ36_spl <=> (growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl)))=zero)),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f278,plain,(
% 0.27/0.89 growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl)))=zero|~sQ36_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f277])).
% 0.27/0.89 fof(f280,plain,(
% 0.27/0.89 sQ36_spl|sQ35_spl|~sQ14_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f273,f277,f225,f119])).
% 0.27/0.89 fof(f281,plain,(
% 0.27/0.89 sQ36_spl|sQ31_spl|~sQ14_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f274,f277,f191,f119])).
% 0.27/0.89 fof(f282,plain,(
% 0.27/0.89 sQ30_spl|sQ35_spl|~sQ14_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f275,f188,f225,f119])).
% 0.27/0.89 fof(f299,plain,(
% 0.27/0.89 greater_or_equal(sK1_skl(sK2_skl),sK0_skl(sK2_skl))|~sQ17_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f133,f18])).
% 0.27/0.89 fof(f315,plain,(
% 0.27/0.89 ~in_environment(sK2_skl,sK0_skl(sK2_skl))|~greater(zero,growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))))|~sQ16_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f127,f40])).
% 0.27/0.89 fof(f318,plain,(
% 0.27/0.89 ~sQ1_spl|~sQ15_spl|~sQ16_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f315,f55,f122,f126])).
% 0.27/0.89 fof(f320,plain,(
% 0.27/0.89 greater(growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))),growth_rate(first_movers,sK0_skl(sK2_skl)))|~sQ7_spl|~sQ12_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f90,f113])).
% 0.27/0.89 fof(f322,plain,(
% 0.27/0.89 subpopulations(first_movers,efficient_producers,sK2_skl,sK0_skl(sK2_skl))|~sQ7_spl|~sQ1_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f90,f62])).
% 0.27/0.89 fof(f324,plain,(
% 0.27/0.89 ~in_environment(sK2_skl,sK0_skl(sK2_skl))|~greater(growth_rate(efficient_producers,sK0_skl(sK2_skl)),zero)|~greater(zero,growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))))|~sQ7_spl),
% 0.27/0.89 inference(paramodulation,[status(thm)],[f90,f40])).
% 0.27/0.89 fof(f325,plain,(
% 0.27/0.89 greater(growth_rate(efficient_producers,sK0_skl(sK2_skl)),growth_rate(first_movers,sK0_skl(sK2_skl)))|~sQ7_spl|~sQ12_spl),
% 0.27/0.89 inference(forward_demodulation,[status(thm)],[f90,f320])).
% 0.27/0.89 fof(f326,definition,(
% 0.27/0.89 sQ38_spl <=> (greater(growth_rate(efficient_producers,sK0_skl(sK2_skl)),zero))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f329,plain,(
% 0.27/0.89 ~sQ1_spl|~sQ38_spl|~sQ15_spl|~sQ7_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f324,f55,f326,f122,f89])).
% 0.27/0.89 fof(f358,plain,(
% 0.27/0.89 ![X0]: (~greater(growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))),X0)|greater(growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))),X0)|~sQ12_spl)),
% 0.27/0.89 inference(resolution,[status(thm)],[f113,f11])).
% 0.27/0.89 fof(f360,plain,(
% 0.27/0.89 greater(growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl))),zero)|~sQ32_spl|~sQ23_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f197,f156])).
% 0.27/0.89 fof(f361,plain,(
% 0.27/0.89 ~greater(zero,zero)|~sQ32_spl|sQ26_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f197,f167])).
% 0.27/0.89 fof(f363,definition,(
% 0.27/0.89 sQ39_spl <=> (greater(zero,growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl)))))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f364,plain,(
% 0.27/0.89 greater(zero,growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl))))|~sQ39_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f363])).
% 0.27/0.89 fof(f369,plain,(
% 0.27/0.89 growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl)))=zero|greater(zero,growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl))))|~sQ25_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f163,f46])).
% 0.27/0.89 fof(f370,plain,(
% 0.27/0.89 growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl)))=zero|greater(growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))),zero)|~sQ25_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f163,f45])).
% 0.27/0.89 fof(f371,plain,(
% 0.27/0.89 growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl)))=zero|greater(zero,growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl))))|~sQ25_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f163,f44])).
% 0.27/0.89 fof(f373,definition,(
% 0.27/0.89 sQ40_spl <=> (growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl)))=zero)),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f374,plain,(
% 0.27/0.89 growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl)))=zero|~sQ40_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f373])).
% 0.27/0.89 fof(f376,plain,(
% 0.27/0.89 sQ40_spl|sQ39_spl|~sQ25_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f369,f373,f363,f162])).
% 0.27/0.89 fof(f377,plain,(
% 0.27/0.89 sQ40_spl|sQ33_spl|~sQ25_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f370,f373,f199,f162])).
% 0.27/0.89 fof(f378,plain,(
% 0.27/0.89 sQ32_spl|sQ39_spl|~sQ25_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f371,f196,f363,f162])).
% 0.27/0.89 fof(f382,plain,(
% 0.27/0.89 ~in_environment(sK2_skl,sK1_skl(sK2_skl))|~greater(zero,growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))))|~sQ32_spl|~sQ23_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f360,f40])).
% 0.27/0.89 fof(f385,plain,(
% 0.27/0.89 ~sQ2_spl|~sQ26_spl|~sQ32_spl|~sQ23_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f382,f65,f165,f196,f155])).
% 0.27/0.89 fof(f386,plain,(
% 0.27/0.89 greater(growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))),zero)|~sQ30_spl|~sQ12_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f189,f113])).
% 0.27/0.89 fof(f387,plain,(
% 0.27/0.89 ~greater(zero,zero)|~sQ30_spl|sQ15_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f189,f124])).
% 0.27/0.89 fof(f391,plain,(
% 0.27/0.89 ~in_environment(sK2_skl,sK0_skl(sK2_skl))|~greater(zero,zero)|~greater(zero,growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))))|~sQ36_spl),
% 0.27/0.89 inference(paramodulation,[status(thm)],[f278,f40])).
% 0.27/0.89 fof(f394,plain,(
% 0.27/0.89 ~sQ1_spl|~sQ34_spl|~sQ15_spl|~sQ36_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f391,f55,f222,f122,f277])).
% 0.27/0.89 fof(f399,plain,(
% 0.27/0.89 greater(zero,zero)|~sQ36_spl|~sQ30_spl|~sQ12_spl),
% 0.27/0.89 inference(forward_demodulation,[status(thm)],[f278,f386])).
% 0.27/0.89 fof(f400,plain,(
% 0.27/0.89 $false|sQ34_spl|~sQ36_spl|~sQ30_spl|~sQ12_spl),
% 0.27/0.89 inference(forward_subsumption_resolution,[status(thm)],[f399,f224])).
% 0.27/0.89 fof(f401,plain,(
% 0.27/0.89 sQ34_spl|~sQ36_spl|~sQ30_spl|~sQ12_spl),
% 0.27/0.89 inference(contradiction_clause,[status(thm)],[f400])).
% 0.27/0.89 fof(f416,plain,(
% 0.27/0.89 greater(sK3_skl(sK0_skl(sK2_skl)),sK1_skl(sK2_skl))|~sQ6_spl|~sQ19_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f205,f139])).
% 0.27/0.89 fof(f420,plain,(
% 0.27/0.89 greater(sK0_skl(sK2_skl),equilibrium(sK2_skl))|~sQ19_spl|~sQ4_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f207,f79])).
% 0.27/0.89 fof(f423,plain,(
% 0.27/0.89 greater_or_equal(sK0_skl(sK2_skl),equilibrium(sK2_skl))|~sQ19_spl|~sQ4_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f420,f18])).
% 0.27/0.89 fof(f424,plain,(
% 0.27/0.89 greater(sK0_skl(sK2_skl),equilibrium(sK2_skl))|sK0_skl(sK2_skl)=equilibrium(sK2_skl)|~sQ19_spl|~sQ4_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f423,f17])).
% 0.27/0.89 fof(f425,definition,(
% 0.27/0.89 sQ42_spl <=> (greater(sK0_skl(sK2_skl),equilibrium(sK2_skl)))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f426,plain,(
% 0.27/0.89 greater(sK0_skl(sK2_skl),equilibrium(sK2_skl))|~sQ42_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f425])).
% 0.27/0.89 fof(f428,definition,(
% 0.27/0.89 sQ43_spl <=> (sK0_skl(sK2_skl)=equilibrium(sK2_skl))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f429,plain,(
% 0.27/0.89 sK0_skl(sK2_skl)=equilibrium(sK2_skl)|~sQ43_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f428])).
% 0.27/0.89 fof(f431,plain,(
% 0.27/0.89 sQ42_spl|sQ43_spl|~sQ19_spl|~sQ4_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f424,f425,f428,f138,f78])).
% 0.27/0.89 fof(f433,plain,(
% 0.27/0.89 greater(sK3_skl(sK1_skl(sK2_skl)),sK0_skl(sK2_skl))|~sQ8_spl|~sQ17_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f209,f133])).
% 0.27/0.89 fof(f434,plain,(
% 0.27/0.89 greater(sK3_skl(sK1_skl(sK2_skl)),equilibrium(sK2_skl))|~sQ8_spl|~sQ4_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f209,f79])).
% 0.27/0.89 fof(f444,plain,(
% 0.27/0.89 ~greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),sK0_skl(sK2_skl))|~sQ43_spl|sQ13_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f429,f118])).
% 0.27/0.89 fof(f446,plain,(
% 0.27/0.89 greater_or_equal(sK1_skl(sK2_skl),sK0_skl(sK2_skl))|~sQ43_spl|~sQ3_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f429,f71])).
% 0.27/0.89 fof(f447,plain,(
% 0.27/0.89 ~sQ11_spl|~sQ43_spl|sQ13_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f444,f109,f428,f116])).
% 0.27/0.89 fof(f448,plain,(
% 0.27/0.89 ~sQ34_spl|~sQ32_spl|sQ26_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f361,f222,f196,f165])).
% 0.27/0.89 fof(f449,plain,(
% 0.27/0.89 sQ16_spl|~sQ30_spl|~sQ12_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f386,f126,f188,f112])).
% 0.27/0.89 fof(f464,definition,(
% 0.27/0.89 sQ45_spl <=> (greater(sK3_skl(sK0_skl(sK2_skl)),equilibrium(sK2_skl)))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f465,plain,(
% 0.27/0.89 greater(sK3_skl(sK0_skl(sK2_skl)),equilibrium(sK2_skl))|~sQ45_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f464])).
% 0.27/0.89 fof(f472,plain,(
% 0.27/0.89 greater(sK3_skl(sK0_skl(sK2_skl)),equilibrium(sK2_skl))|~sQ42_spl|~sQ6_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f426,f205])).
% 0.27/0.89 fof(f474,plain,(
% 0.27/0.89 greater_or_equal(sK0_skl(sK2_skl),equilibrium(sK2_skl))|~sQ42_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f426,f18])).
% 0.27/0.89 fof(f521,plain,(
% 0.27/0.89 ~in_environment(sK2_skl,sK1_skl(sK2_skl))|~greater(zero,zero)|~greater(zero,growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))))|~sQ40_spl),
% 0.27/0.89 inference(paramodulation,[status(thm)],[f374,f40])).
% 0.27/0.89 fof(f524,plain,(
% 0.27/0.89 ~sQ2_spl|~sQ34_spl|~sQ26_spl|~sQ40_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f521,f65,f222,f165,f373])).
% 0.27/0.89 fof(f533,plain,(
% 0.27/0.89 greater_or_equal(sK3_skl(sK1_skl(sK2_skl)),sK0_skl(sK2_skl))|~sQ8_spl|~sQ17_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f433,f18])).
% 0.27/0.89 fof(f534,plain,(
% 0.27/0.89 $false|sQ22_spl|~sQ8_spl|~sQ17_spl),
% 0.27/0.89 inference(forward_subsumption_resolution,[status(thm)],[f533,f154])).
% 0.27/0.89 fof(f535,plain,(
% 0.27/0.89 sQ22_spl|~sQ8_spl|~sQ17_spl),
% 0.27/0.89 inference(contradiction_clause,[status(thm)],[f534])).
% 0.27/0.89 fof(f537,definition,(
% 0.27/0.89 sQ48_spl <=> (greater(sK3_skl(sK1_skl(sK2_skl)),sK0_skl(sK2_skl)))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f538,plain,(
% 0.27/0.89 greater(sK3_skl(sK1_skl(sK2_skl)),sK0_skl(sK2_skl))|~sQ48_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f537])).
% 0.27/0.89 fof(f540,definition,(
% 0.27/0.89 sQ49_spl <=> (sK3_skl(sK1_skl(sK2_skl))=sK0_skl(sK2_skl))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f541,plain,(
% 0.27/0.89 sK3_skl(sK1_skl(sK2_skl))=sK0_skl(sK2_skl)|~sQ49_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f540])).
% 0.27/0.89 fof(f552,plain,(
% 0.27/0.89 sP0_prd(sK0_skl(sK2_skl))|~sQ49_spl|~sQ25_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f541,f163])).
% 0.27/0.89 fof(f553,plain,(
% 0.27/0.89 greater(growth_rate(first_movers,sK0_skl(sK2_skl)),zero)|~sQ49_spl|~sQ33_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f541,f200])).
% 0.27/0.89 fof(f558,plain,(
% 0.27/0.89 ~in_environment(sK2_skl,sK1_skl(sK2_skl))|~greater(growth_rate(efficient_producers,sK0_skl(sK2_skl)),zero)|~greater(zero,growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))))|~sQ49_spl),
% 0.27/0.89 inference(paramodulation,[status(thm)],[f541,f40])).
% 0.27/0.89 fof(f561,plain,(
% 0.27/0.89 ~sQ2_spl|~sQ38_spl|~sQ26_spl|~sQ49_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f558,f65,f326,f165,f540])).
% 0.27/0.89 fof(f582,plain,(
% 0.27/0.89 ![X0]: (~greater(growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))),X0)|greater(growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl))),X0)|~sQ23_spl)),
% 0.27/0.89 inference(resolution,[status(thm)],[f156,f11])).
% 0.27/0.89 fof(f647,definition,(
% 0.27/0.89 sQ57_spl <=> (greater_or_equal(sK1_skl(sK2_skl),sK0_skl(sK2_skl)))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f648,plain,(
% 0.27/0.89 greater_or_equal(sK1_skl(sK2_skl),sK0_skl(sK2_skl))|~sQ57_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f647])).
% 0.27/0.89 fof(f721,definition,(
% 0.27/0.89 sQ65_spl <=> (greater(sK3_skl(sK0_skl(sK2_skl)),sK1_skl(sK2_skl)))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f722,plain,(
% 0.27/0.89 greater(sK3_skl(sK0_skl(sK2_skl)),sK1_skl(sK2_skl))|~sQ65_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f721])).
% 0.27/0.89 fof(f724,definition,(
% 0.27/0.89 sQ66_spl <=> (sK3_skl(sK0_skl(sK2_skl))=sK1_skl(sK2_skl))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f725,plain,(
% 0.27/0.89 sK3_skl(sK0_skl(sK2_skl))=sK1_skl(sK2_skl)|~sQ66_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f724])).
% 0.27/0.89 fof(f747,plain,(
% 0.27/0.89 ~greater_or_equal(sK1_skl(sK2_skl),sK0_skl(sK2_skl))|~sQ9_spl|sQ22_spl),
% 0.27/0.89 inference(forward_demodulation,[status(thm)],[f100,f154])).
% 0.27/0.89 fof(f748,plain,(
% 0.27/0.89 $false|~sQ17_spl|~sQ9_spl|sQ22_spl),
% 0.27/0.89 inference(forward_subsumption_resolution,[status(thm)],[f747,f299])).
% 0.27/0.89 fof(f749,plain,(
% 0.27/0.89 ~sQ17_spl|~sQ9_spl|sQ22_spl),
% 0.27/0.89 inference(contradiction_clause,[status(thm)],[f748])).
% 0.27/0.89 fof(f750,plain,(
% 0.27/0.89 greater(sK1_skl(sK2_skl),sK0_skl(sK2_skl))|sK1_skl(sK2_skl)=sK0_skl(sK2_skl)|~sQ43_spl|~sQ3_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f446,f17])).
% 0.27/0.89 fof(f751,plain,(
% 0.27/0.89 sQ17_spl|sQ18_spl|~sQ43_spl|~sQ3_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f750,f132,f135,f428,f70])).
% 0.27/0.89 fof(f770,plain,(
% 0.27/0.89 ~greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),sK1_skl(sK2_skl))|~sQ5_spl|sQ13_spl),
% 0.27/0.89 inference(forward_demodulation,[status(thm)],[f82,f118])).
% 0.27/0.89 fof(f786,plain,(
% 0.27/0.89 greater(growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))),zero)|~sQ31_spl|~sQ12_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f192,f358])).
% 0.27/0.89 fof(f804,plain,(
% 0.27/0.89 greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),sK1_skl(sK2_skl))|~sQ6_spl|~sQ19_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f416,f18])).
% 0.27/0.89 fof(f805,plain,(
% 0.27/0.89 $false|~sQ5_spl|sQ13_spl|~sQ6_spl|~sQ19_spl),
% 0.27/0.89 inference(forward_subsumption_resolution,[status(thm)],[f804,f770])).
% 0.27/0.89 fof(f806,plain,(
% 0.27/0.89 ~sQ5_spl|sQ13_spl|~sQ6_spl|~sQ19_spl),
% 0.27/0.89 inference(contradiction_clause,[status(thm)],[f805])).
% 0.27/0.89 fof(f808,plain,(
% 0.27/0.89 greater(sK3_skl(sK0_skl(sK2_skl)),sK1_skl(sK2_skl))|~sQ5_spl|~sQ45_spl),
% 0.27/0.89 inference(forward_demodulation,[status(thm)],[f82,f465])).
% 0.27/0.89 fof(f835,plain,(
% 0.27/0.89 greater(sK1_skl(sK2_skl),sK0_skl(sK2_skl))|~sQ66_spl|~sQ6_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f725,f87])).
% 0.27/0.89 fof(f843,plain,(
% 0.27/0.89 sQ17_spl|~sQ66_spl|~sQ6_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f835,f132,f724,f86])).
% 0.27/0.89 fof(f876,plain,(
% 0.27/0.89 greater_or_equal(sK3_skl(sK1_skl(sK2_skl)),sK0_skl(sK2_skl))|~sQ48_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f538,f18])).
% 0.27/0.89 fof(f877,plain,(
% 0.27/0.89 sQ22_spl|~sQ48_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f876,f152,f537])).
% 0.27/0.89 fof(f878,plain,(
% 0.27/0.89 greater(zero,zero)|~sQ32_spl|~sQ26_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f197,f166])).
% 0.27/0.89 fof(f881,plain,(
% 0.27/0.89 sQ34_spl|~sQ32_spl|~sQ26_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f878,f222,f196,f165])).
% 0.27/0.89 fof(f891,plain,(
% 0.27/0.89 ~environment(sK2_skl)|~stable(sK2_skl)|~greater_or_equal(sK0_skl(sK2_skl),sK0_skl(sK2_skl))|greater(growth_rate(efficient_producers,sK0_skl(sK2_skl)),growth_rate(first_movers,sK0_skl(sK2_skl)))|~sQ7_spl|~sQ1_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f322,f29])).
% 0.27/0.89 fof(f892,plain,(
% 0.27/0.89 ~environment(sK2_skl)|~greater_or_equal(sK0_skl(sK2_skl),equilibrium(sK2_skl))|sP0_prd(sK0_skl(sK2_skl))|greater(zero,growth_rate(first_movers,sK0_skl(sK2_skl)))|~sQ7_spl|~sQ1_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f322,f25])).
% 0.27/0.89 fof(f893,plain,(
% 0.27/0.89 ~environment(sK2_skl)|~greater_or_equal(sK0_skl(sK2_skl),equilibrium(sK2_skl))|sP0_prd(sK0_skl(sK2_skl))|greater(growth_rate(efficient_producers,sK0_skl(sK2_skl)),zero)|~sQ7_spl|~sQ1_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f322,f24])).
% 0.27/0.89 fof(f894,definition,(
% 0.27/0.89 sQ67_spl <=> (greater_or_equal(sK0_skl(sK2_skl),sK0_skl(sK2_skl)))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f896,plain,(
% 0.27/0.89 ~greater_or_equal(sK0_skl(sK2_skl),sK0_skl(sK2_skl))|sQ67_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f894])).
% 0.27/0.89 fof(f897,definition,(
% 0.27/0.89 sQ68_spl <=> (greater(growth_rate(efficient_producers,sK0_skl(sK2_skl)),growth_rate(first_movers,sK0_skl(sK2_skl))))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f900,plain,(
% 0.27/0.89 ~sQ0_spl|~sQ10_spl|~sQ67_spl|sQ68_spl|~sQ7_spl|~sQ1_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f891,f52,f106,f894,f897,f89,f55])).
% 0.27/0.89 fof(f901,definition,(
% 0.27/0.89 sQ69_spl <=> (greater_or_equal(sK0_skl(sK2_skl),equilibrium(sK2_skl)))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f903,plain,(
% 0.27/0.89 ~greater_or_equal(sK0_skl(sK2_skl),equilibrium(sK2_skl))|sQ69_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f901])).
% 0.27/0.89 fof(f904,definition,(
% 0.27/0.89 sQ70_spl <=> (sP0_prd(sK0_skl(sK2_skl)))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f905,plain,(
% 0.27/0.89 sP0_prd(sK0_skl(sK2_skl))|~sQ70_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f904])).
% 0.27/0.89 fof(f907,definition,(
% 0.27/0.89 sQ71_spl <=> (greater(zero,growth_rate(first_movers,sK0_skl(sK2_skl))))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f910,plain,(
% 0.27/0.89 ~sQ0_spl|~sQ69_spl|sQ70_spl|sQ71_spl|~sQ7_spl|~sQ1_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f892,f52,f901,f904,f907,f89,f55])).
% 0.27/0.89 fof(f911,plain,(
% 0.27/0.89 ~sQ0_spl|~sQ69_spl|sQ70_spl|sQ38_spl|~sQ7_spl|~sQ1_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f893,f52,f901,f904,f326,f89,f55])).
% 0.27/0.89 fof(f912,plain,(
% 0.27/0.89 $false|sQ67_spl),
% 0.27/0.89 inference(forward_subsumption_resolution,[status(thm)],[f896,f49])).
% 0.27/0.89 fof(f913,plain,(
% 0.27/0.89 sQ67_spl),
% 0.27/0.89 inference(contradiction_clause,[status(thm)],[f912])).
% 0.27/0.89 fof(f931,definition,(
% 0.27/0.89 sQ72_spl <=> (growth_rate(efficient_producers,sK0_skl(sK2_skl))=zero)),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f932,plain,(
% 0.27/0.89 growth_rate(efficient_producers,sK0_skl(sK2_skl))=zero|~sQ72_spl),
% 0.27/0.89 inference(component_clause,[status(thm)],[f931])).
% 0.27/0.89 fof(f934,definition,(
% 0.27/0.89 sQ73_spl <=> (greater(zero,growth_rate(efficient_producers,sK0_skl(sK2_skl))))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f938,definition,(
% 0.27/0.89 sQ74_spl <=> (greater(growth_rate(first_movers,sK0_skl(sK2_skl)),zero))),
% 0.27/0.89 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.27/0.89 fof(f947,plain,(
% 0.27/0.89 ~sQ34_spl|~sQ30_spl|sQ15_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f387,f222,f188,f122])).
% 0.27/0.89 fof(f948,plain,(
% 0.27/0.89 ~greater(zero,growth_rate(first_movers,sK0_skl(sK2_skl)))|~sQ7_spl|sQ15_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f90,f124])).
% 0.27/0.89 fof(f957,plain,(
% 0.27/0.89 growth_rate(efficient_producers,sK0_skl(sK2_skl))=zero|greater(zero,growth_rate(efficient_producers,sK0_skl(sK2_skl)))|~sQ70_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f905,f46])).
% 0.27/0.89 fof(f961,plain,(
% 0.27/0.89 sQ72_spl|sQ73_spl|~sQ70_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f957,f931,f934,f904])).
% 0.27/0.89 fof(f965,plain,(
% 0.27/0.89 ~greater_or_equal(sK0_skl(sK2_skl),sK1_skl(sK2_skl))|~sQ5_spl|sQ69_spl),
% 0.27/0.89 inference(forward_demodulation,[status(thm)],[f82,f903])).
% 0.27/0.89 fof(f966,plain,(
% 0.27/0.89 $false|~sQ19_spl|~sQ5_spl|sQ69_spl),
% 0.27/0.89 inference(forward_subsumption_resolution,[status(thm)],[f965,f208])).
% 0.27/0.89 fof(f967,plain,(
% 0.27/0.89 ~sQ19_spl|~sQ5_spl|sQ69_spl),
% 0.27/0.89 inference(contradiction_clause,[status(thm)],[f966])).
% 0.27/0.89 fof(f980,plain,(
% 0.27/0.89 ~sP0_prd(sK0_skl(sK2_skl))|~sQ7_spl|sQ14_spl),
% 0.27/0.89 inference(forward_demodulation,[status(thm)],[f90,f121])).
% 0.27/0.89 fof(f981,plain,(
% 0.27/0.89 $false|~sQ70_spl|~sQ7_spl|sQ14_spl),
% 0.27/0.89 inference(forward_subsumption_resolution,[status(thm)],[f980,f905])).
% 0.27/0.89 fof(f982,plain,(
% 0.27/0.89 ~sQ70_spl|~sQ7_spl|sQ14_spl),
% 0.27/0.89 inference(contradiction_clause,[status(thm)],[f981])).
% 0.27/0.89 fof(f983,plain,(
% 0.27/0.89 ~greater_or_equal(sK0_skl(sK2_skl),sK1_skl(sK2_skl))|~sQ7_spl|~sQ5_spl|sQ13_spl),
% 0.27/0.89 inference(forward_demodulation,[status(thm)],[f90,f770])).
% 0.27/0.89 fof(f984,plain,(
% 0.27/0.89 $false|~sQ19_spl|~sQ7_spl|~sQ5_spl|sQ13_spl),
% 0.27/0.89 inference(forward_subsumption_resolution,[status(thm)],[f983,f208])).
% 0.27/0.89 fof(f985,plain,(
% 0.27/0.89 ~sQ19_spl|~sQ7_spl|~sQ5_spl|sQ13_spl),
% 0.27/0.89 inference(contradiction_clause,[status(thm)],[f984])).
% 0.27/0.89 fof(f991,plain,(
% 0.27/0.89 greater(growth_rate(efficient_producers,sK0_skl(sK2_skl)),zero)|~sQ7_spl|~sQ31_spl|~sQ12_spl),
% 0.27/0.89 inference(forward_demodulation,[status(thm)],[f90,f786])).
% 0.27/0.89 fof(f1043,plain,(
% 0.27/0.89 greater(zero,growth_rate(first_movers,sK0_skl(sK2_skl)))|~sQ72_spl|~sQ7_spl|~sQ12_spl),
% 0.27/0.89 inference(backward_demodulation,[status(thm)],[f932,f325])).
% 0.27/0.89 fof(f1046,plain,(
% 0.27/0.89 $false|sQ15_spl|~sQ72_spl|~sQ7_spl|~sQ12_spl),
% 0.27/0.89 inference(forward_subsumption_resolution,[status(thm)],[f1043,f948])).
% 0.27/0.89 fof(f1047,plain,(
% 0.27/0.89 sQ15_spl|~sQ72_spl|~sQ7_spl|~sQ12_spl),
% 0.27/0.89 inference(contradiction_clause,[status(thm)],[f1046])).
% 0.27/0.89 fof(f1065,plain,(
% 0.27/0.89 greater_or_equal(growth_rate(efficient_producers,sK0_skl(sK2_skl)),zero)|~sQ7_spl|~sQ31_spl|~sQ12_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f991,f18])).
% 0.27/0.89 fof(f1073,plain,(
% 0.27/0.89 greater(growth_rate(efficient_producers,sK0_skl(sK2_skl)),zero)|growth_rate(efficient_producers,sK0_skl(sK2_skl))=zero|~sQ7_spl|~sQ31_spl|~sQ12_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f1065,f17])).
% 0.27/0.89 fof(f1074,plain,(
% 0.27/0.89 sQ38_spl|sQ72_spl|~sQ7_spl|~sQ31_spl|~sQ12_spl),
% 0.27/0.89 inference(split_clause,[status(thm)],[f1073,f326,f931,f89,f191,f112])).
% 0.27/0.89 fof(f1172,plain,(
% 0.27/0.89 ![X0]: (~greater(growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))),X0)|greater(zero,X0)|~sQ35_spl)),
% 0.27/0.89 inference(resolution,[status(thm)],[f226,f11])).
% 0.27/0.89 fof(f1182,plain,(
% 0.27/0.89 ~in_environment(sK2_skl,sK0_skl(sK2_skl))|~greater(zero,growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))))|~sQ31_spl|~sQ12_spl),
% 0.27/0.89 inference(resolution,[status(thm)],[f786,f40])).
% 0.27/0.89 fof(f1184,plain,(
% 0.27/0.89 greater_or_equal(growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))),zero)|~sQ31_spl|~sQ12_spl),
% 0.27/0.90 inference(resolution,[status(thm)],[f786,f18])).
% 0.27/0.90 fof(f1185,plain,(
% 0.27/0.90 ~sQ1_spl|~sQ15_spl|~sQ31_spl|~sQ12_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f1182,f55,f122,f191,f112])).
% 0.27/0.90 fof(f1188,plain,(
% 0.27/0.90 greater(growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl))),zero)|growth_rate(efficient_producers,sK3_skl(sK0_skl(sK2_skl)))=zero|~sQ31_spl|~sQ12_spl),
% 0.27/0.90 inference(resolution,[status(thm)],[f1184,f17])).
% 0.27/0.90 fof(f1189,plain,(
% 0.27/0.90 sQ16_spl|sQ36_spl|~sQ31_spl|~sQ12_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f1188,f126,f277,f191,f112])).
% 0.27/0.90 fof(f1205,plain,(
% 0.27/0.90 greater(zero,growth_rate(first_movers,sK3_skl(sK0_skl(sK2_skl))))|~sQ35_spl|~sQ12_spl),
% 0.27/0.90 inference(resolution,[status(thm)],[f1172,f113])).
% 0.27/0.90 fof(f1206,plain,(
% 0.27/0.90 sQ15_spl|~sQ35_spl|~sQ12_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f1205,f122,f225,f112])).
% 0.27/0.90 fof(f1214,plain,(
% 0.27/0.90 sQ70_spl|~sQ49_spl|~sQ25_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f552,f904,f540,f162])).
% 0.27/0.90 fof(f1215,plain,(
% 0.27/0.90 sQ74_spl|~sQ49_spl|~sQ33_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f553,f938,f540,f199])).
% 0.27/0.90 fof(f1282,plain,(
% 0.27/0.90 greater(sK1_skl(sK2_skl),sK0_skl(sK2_skl))|sK1_skl(sK2_skl)=sK0_skl(sK2_skl)|~sQ57_spl),
% 0.27/0.90 inference(resolution,[status(thm)],[f648,f17])).
% 0.27/0.90 fof(f1283,plain,(
% 0.27/0.90 sQ17_spl|sQ18_spl|~sQ57_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f1282,f132,f135,f647])).
% 0.27/0.90 fof(f1295,plain,(
% 0.27/0.90 greater(growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl))),zero)|~sQ33_spl|~sQ23_spl),
% 0.27/0.90 inference(resolution,[status(thm)],[f200,f582])).
% 0.27/0.90 fof(f1299,plain,(
% 0.27/0.90 sQ27_spl|~sQ33_spl|~sQ23_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f1295,f169,f199,f155])).
% 0.27/0.90 fof(f1327,plain,(
% 0.27/0.90 greater(growth_rate(efficient_producers,sK0_skl(sK2_skl)),zero)|~sQ7_spl|~sQ16_spl),
% 0.27/0.90 inference(forward_demodulation,[status(thm)],[f90,f127])).
% 0.27/0.90 fof(f1356,plain,(
% 0.27/0.90 greater(zero,zero)|~sQ40_spl|~sQ32_spl|~sQ23_spl),
% 0.27/0.90 inference(backward_demodulation,[status(thm)],[f374,f360])).
% 0.27/0.90 fof(f1360,plain,(
% 0.27/0.90 sQ34_spl|~sQ40_spl|~sQ32_spl|~sQ23_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f1356,f222,f373,f196,f155])).
% 0.27/0.90 fof(f1365,plain,(
% 0.27/0.90 greater(zero,zero)|~sQ32_spl|~sQ33_spl),
% 0.27/0.90 inference(forward_demodulation,[status(thm)],[f197,f200])).
% 0.27/0.90 fof(f1366,plain,(
% 0.27/0.90 $false|sQ34_spl|~sQ32_spl|~sQ33_spl),
% 0.27/0.90 inference(forward_subsumption_resolution,[status(thm)],[f1365,f224])).
% 0.27/0.90 fof(f1367,plain,(
% 0.27/0.90 sQ34_spl|~sQ32_spl|~sQ33_spl),
% 0.27/0.90 inference(contradiction_clause,[status(thm)],[f1366])).
% 0.27/0.90 fof(f1413,plain,(
% 0.27/0.90 greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),sK1_skl(sK2_skl))|~sQ65_spl),
% 0.27/0.90 inference(resolution,[status(thm)],[f722,f18])).
% 0.27/0.90 fof(f1414,plain,(
% 0.27/0.90 $false|~sQ5_spl|sQ13_spl|~sQ65_spl),
% 0.27/0.90 inference(forward_subsumption_resolution,[status(thm)],[f1413,f770])).
% 0.27/0.90 fof(f1415,plain,(
% 0.27/0.90 ~sQ5_spl|sQ13_spl|~sQ65_spl),
% 0.27/0.90 inference(contradiction_clause,[status(thm)],[f1414])).
% 0.27/0.90 fof(f1416,plain,(
% 0.27/0.90 sQ38_spl|~sQ7_spl|~sQ16_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f1327,f326,f89,f126])).
% 0.27/0.90 fof(f1460,plain,(
% 0.27/0.90 sQ65_spl|~sQ5_spl|~sQ45_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f808,f721,f81,f464])).
% 0.27/0.90 fof(f1559,plain,(
% 0.27/0.90 ![X0]: (~greater(growth_rate(efficient_producers,sK3_skl(sK1_skl(sK2_skl))),X0)|greater(zero,X0)|~sQ39_spl)),
% 0.27/0.90 inference(resolution,[status(thm)],[f364,f11])).
% 0.27/0.90 fof(f1589,plain,(
% 0.27/0.90 greater(zero,growth_rate(first_movers,sK3_skl(sK1_skl(sK2_skl))))|~sQ39_spl|~sQ23_spl),
% 0.27/0.90 inference(resolution,[status(thm)],[f1559,f156])).
% 0.27/0.90 fof(f1590,plain,(
% 0.27/0.90 sQ26_spl|~sQ39_spl|~sQ23_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f1589,f165,f363,f155])).
% 0.27/0.90 fof(f1638,plain,(
% 0.27/0.90 ~greater_or_equal(sK1_skl(sK2_skl),equilibrium(sK2_skl))|~sQ9_spl|sQ24_spl),
% 0.27/0.90 inference(forward_demodulation,[status(thm)],[f100,f161])).
% 0.27/0.90 fof(f1639,plain,(
% 0.27/0.90 $false|~sQ3_spl|~sQ9_spl|sQ24_spl),
% 0.27/0.90 inference(forward_subsumption_resolution,[status(thm)],[f1638,f71])).
% 0.27/0.90 fof(f1640,plain,(
% 0.27/0.90 ~sQ3_spl|~sQ9_spl|sQ24_spl),
% 0.27/0.90 inference(contradiction_clause,[status(thm)],[f1639])).
% 0.27/0.90 fof(f1709,plain,(
% 0.27/0.90 greater_or_equal(sK3_skl(sK1_skl(sK2_skl)),equilibrium(sK2_skl))|~sQ8_spl|~sQ4_spl),
% 0.27/0.90 inference(resolution,[status(thm)],[f434,f18])).
% 0.27/0.90 fof(f1710,plain,(
% 0.27/0.90 sQ24_spl|~sQ8_spl|~sQ4_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f1709,f159,f96,f78])).
% 0.27/0.90 fof(f1778,plain,(
% 0.27/0.90 greater_or_equal(sK3_skl(sK0_skl(sK2_skl)),equilibrium(sK2_skl))|~sQ42_spl|~sQ6_spl),
% 0.27/0.90 inference(resolution,[status(thm)],[f472,f18])).
% 0.27/0.90 fof(f1779,plain,(
% 0.27/0.90 sQ13_spl|~sQ42_spl|~sQ6_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f1778,f116,f425,f86])).
% 0.27/0.90 fof(f1780,plain,(
% 0.27/0.90 $false|~sQ42_spl|sQ69_spl),
% 0.27/0.90 inference(forward_subsumption_resolution,[status(thm)],[f903,f474])).
% 0.27/0.90 fof(f1781,plain,(
% 0.27/0.90 ~sQ42_spl|sQ69_spl),
% 0.27/0.90 inference(contradiction_clause,[status(thm)],[f1780])).
% 0.27/0.90 fof(f1792,plain,(
% 0.27/0.90 ~greater(zero,growth_rate(first_movers,sK0_skl(sK2_skl)))|~sQ7_spl|sQ15_spl),
% 0.27/0.90 inference(backward_demodulation,[status(thm)],[f90,f124])).
% 0.27/0.90 fof(f1795,plain,(
% 0.27/0.90 ~greater_or_equal(sK0_skl(sK2_skl),equilibrium(sK2_skl))|~sQ7_spl|sQ13_spl),
% 0.27/0.90 inference(backward_demodulation,[status(thm)],[f90,f118])).
% 0.27/0.90 fof(f1801,plain,(
% 0.27/0.90 ~sQ71_spl|~sQ7_spl|sQ15_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f1792,f907,f89,f122])).
% 0.27/0.90 fof(f1803,plain,(
% 0.27/0.90 ~sQ69_spl|~sQ7_spl|sQ13_spl),
% 0.27/0.90 inference(split_clause,[status(thm)],[f1795,f901,f89,f116])).
% 0.27/0.90 fof(f1805,plain,(
% 0.27/0.90 $false),
% 0.27/0.90 inference(sat_refutation,[status(thm)],[f58,f60,f68,f73,f84,f92,f102,f115,f125,f129,f141,f158,f168,f172,f174,f176,f194,f202,f218,f241,f259,f280,f281,f282,f318,f329,f376,f377,f378,f385,f394,f401,f431,f447,f448,f449,f524,f535,f561,f749,f751,f806,f843,f877,f881,f900,f910,f911,f913,f947,f961,f967,f982,f985,f1047,f1074,f1185,f1189,f1206,f1214,f1215,f1283,f1299,f1360,f1367,f1415,f1416,f1460,f1590,f1640,f1710,f1779,f1781,f1801,f1803])).
% 0.27/0.90 % SZS output end CNFRefutation for theBenchmark.p
% 0.27/0.91 % Elapsed time: 0.440003 seconds
% 0.27/0.91 % CPU time: 3.042892 seconds
% 0.27/0.91 % Total memory used: 100.097 MB
% 0.27/0.91 % Net memory used: 97.845 MB
%------------------------------------------------------------------------------