%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT035-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n012.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:46 PM UTC 2026
% Result : Unsatisfiable 27.52s 3.90s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT035-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 01:22:09 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 % Drodi V4.1.1
% 27.52/3.90 % Refutation found
% 27.52/3.90 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 27.52/3.90 % SZS output start CNFRefutation for theBenchmark
% 27.52/3.90 fof(f1,axiom,(
% 27.52/3.90 (![A,B,C]: (( ~ greater(A,B)| ~ greater(B,C)| greater(A,C) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f2,axiom,(
% 27.52/3.90 (![A,B,C]: (( ~ in_environment(A,B)| ~ in_environment(A,C)| greater(C,B)| C = B| greater(B,C) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f3,axiom,(
% 27.52/3.90 (![A,B]: (( ~ greater_or_equal(A,B)| greater(A,B)| A = B ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f4,axiom,(
% 27.52/3.90 (![A,B]: (( ~ greater(A,B)| greater_or_equal(A,B) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f5,axiom,(
% 27.52/3.90 (![A,B]: (( A != B| greater_or_equal(A,B) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f6,hypothesis,(
% 27.52/3.90 (![A,B,C,D]: (( ~ environment(A)| ~ subpopulations(B,C,A,D)| ~ greater_or_equal(growth_rate(C,D),zero)| ~ greater(zero,growth_rate(B,D))| outcompetes(C,B,D) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f7,hypothesis,(
% 27.52/3.90 (![A,B,C,D]: (( ~ environment(A)| ~ subpopulations(B,C,A,D)| ~ outcompetes(C,B,D)| greater_or_equal(growth_rate(C,D),zero) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f8,hypothesis,(
% 27.52/3.90 (![A,B,C,D]: (( ~ environment(A)| ~ subpopulations(B,C,A,D)| ~ outcompetes(C,B,D)| greater(zero,growth_rate(B,D)) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f9,hypothesis,(
% 27.52/3.90 (![A,B]: (( ~ environment(A)| ~ subpopulations(first_movers,efficient_producers,A,B)| ~ greater_or_equal(B,equilibrium(A))| growth_rate(first_movers,B) = zero| greater(growth_rate(first_movers,B),zero)| greater(growth_rate(efficient_producers,B),zero) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f10,hypothesis,(
% 27.52/3.90 (![A,B]: (( ~ environment(A)| ~ subpopulations(first_movers,efficient_producers,A,B)| ~ greater_or_equal(B,equilibrium(A))| growth_rate(first_movers,B) = zero| greater(growth_rate(first_movers,B),zero)| greater(zero,growth_rate(first_movers,B)) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f11,hypothesis,(
% 27.52/3.90 (![A,B]: (( ~ environment(A)| ~ subpopulations(first_movers,efficient_producers,A,B)| ~ greater_or_equal(B,equilibrium(A))| growth_rate(first_movers,B) = zero| greater(zero,growth_rate(efficient_producers,B))| greater(growth_rate(efficient_producers,B),zero) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f12,hypothesis,(
% 27.52/3.90 (![A,B]: (( ~ environment(A)| ~ subpopulations(first_movers,efficient_producers,A,B)| ~ greater_or_equal(B,equilibrium(A))| growth_rate(first_movers,B) = zero| greater(zero,growth_rate(efficient_producers,B))| greater(zero,growth_rate(first_movers,B)) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f13,hypothesis,(
% 27.52/3.90 (![A,B]: (( ~ environment(A)| ~ subpopulations(first_movers,efficient_producers,A,B)| ~ greater_or_equal(B,equilibrium(A))| growth_rate(efficient_producers,B) = zero| greater(growth_rate(first_movers,B),zero)| greater(growth_rate(efficient_producers,B),zero) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f14,hypothesis,(
% 27.52/3.90 (![A,B]: (( ~ environment(A)| ~ subpopulations(first_movers,efficient_producers,A,B)| ~ greater_or_equal(B,equilibrium(A))| growth_rate(efficient_producers,B) = zero| greater(growth_rate(first_movers,B),zero)| greater(zero,growth_rate(first_movers,B)) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f15,hypothesis,(
% 27.52/3.90 (![A,B]: (( ~ environment(A)| ~ subpopulations(first_movers,efficient_producers,A,B)| ~ greater_or_equal(B,equilibrium(A))| growth_rate(efficient_producers,B) = zero| greater(zero,growth_rate(efficient_producers,B))| greater(growth_rate(efficient_producers,B),zero) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f16,hypothesis,(
% 27.52/3.90 (![A,B]: (( ~ environment(A)| ~ subpopulations(first_movers,efficient_producers,A,B)| ~ greater_or_equal(B,equilibrium(A))| growth_rate(efficient_producers,B) = zero| greater(zero,growth_rate(efficient_producers,B))| greater(zero,growth_rate(first_movers,B)) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f17,hypothesis,(
% 27.52/3.90 (![A]: (( ~ environment(A)| ~ stable(A)| in_environment(A,sk1(A)) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f18,hypothesis,(
% 27.52/3.90 (![A,B]: (( ~ environment(A)| ~ stable(A)| ~ subpopulations(first_movers,efficient_producers,A,B)| ~ greater_or_equal(B,sk1(A))| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B)) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f19,hypothesis,(
% 27.52/3.90 (![A]: (( ~ environment(A)| ~ stable(A)| in_environment(A,sk2(A)) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f20,hypothesis,(
% 27.52/3.90 (![A]: (( ~ environment(A)| ~ stable(A)| greater_or_equal(sk2(A),equilibrium(A)) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f21,negated_conjecture,(
% 27.52/3.90 environment(sk3) ),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f22,negated_conjecture,(
% 27.52/3.90 stable(sk3) ),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f23,negated_conjecture,(
% 27.52/3.90 (![A]: (( ~ in_environment(sk3,A)| subpopulations(first_movers,efficient_producers,sk3,sk4(A)) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f24,negated_conjecture,(
% 27.52/3.90 (![A]: (( ~ in_environment(sk3,A)| greater_or_equal(sk4(A),A) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f25,negated_conjecture,(
% 27.52/3.90 (![A]: (( ~ in_environment(sk3,A)| ~ outcompetes(efficient_producers,first_movers,sk4(A)) ) ))),
% 27.52/3.90 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.52/3.90 fof(f26,plain,(
% 27.52/3.90 ![A,C]: ((![B]: (~greater(A,B)|~greater(B,C)))|greater(A,C))),
% 27.52/3.90 inference(miniscoping,[status(thm)],[f1])).
% 27.52/3.90 fof(f27,plain,(
% 27.52/3.90 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 27.52/3.90 inference(cnf_transformation,[status(thm)],[f26])).
% 27.52/3.90 fof(f28,plain,(
% 27.52/3.90 ![B,C]: ((((![A]: (~in_environment(A,B)|~in_environment(A,C)))|greater(C,B))|C=B)|greater(B,C))),
% 27.52/3.90 inference(miniscoping,[status(thm)],[f2])).
% 27.52/3.90 fof(f29,plain,(
% 27.52/3.90 ![X0,X1,X2]: (~in_environment(X0,X1)|~in_environment(X0,X2)|greater(X2,X1)|X2=X1|greater(X1,X2))),
% 27.52/3.90 inference(cnf_transformation,[status(thm)],[f28])).
% 27.52/3.90 fof(f30,plain,(
% 27.52/3.90 ![X0,X1]: (~greater_or_equal(X0,X1)|greater(X0,X1)|X0=X1)),
% 27.52/3.90 inference(cnf_transformation,[status(thm)],[f3])).
% 27.52/3.90 fof(f31,plain,(
% 27.52/3.90 ![X0,X1]: (~greater(X0,X1)|greater_or_equal(X0,X1))),
% 27.52/3.90 inference(cnf_transformation,[status(thm)],[f4])).
% 27.52/3.90 fof(f32,plain,(
% 27.52/3.90 ![X0,X1]: (~X0=X1|greater_or_equal(X0,X1))),
% 27.52/3.90 inference(cnf_transformation,[status(thm)],[f5])).
% 27.52/3.90 fof(f33,plain,(
% 27.52/3.90 ![B,C,D]: ((((![A]: (~environment(A)|~subpopulations(B,C,A,D)))|~greater_or_equal(growth_rate(C,D),zero))|~greater(zero,growth_rate(B,D)))|outcompetes(C,B,D))),
% 27.52/3.90 inference(miniscoping,[status(thm)],[f6])).
% 27.52/3.90 fof(f34,plain,(
% 27.52/3.90 ![X0,X1,X2,X3]: (~environment(X0)|~subpopulations(X1,X2,X0,X3)|~greater_or_equal(growth_rate(X2,X3),zero)|~greater(zero,growth_rate(X1,X3))|outcompetes(X2,X1,X3))),
% 27.52/3.90 inference(cnf_transformation,[status(thm)],[f33])).
% 27.52/3.90 fof(f35,plain,(
% 27.52/3.90 ![C,D]: ((![B]: ((![A]: (~environment(A)|~subpopulations(B,C,A,D)))|~outcompetes(C,B,D)))|greater_or_equal(growth_rate(C,D),zero))),
% 27.52/3.90 inference(miniscoping,[status(thm)],[f7])).
% 27.52/3.90 fof(f36,plain,(
% 27.52/3.90 ![X0,X1,X2,X3]: (~environment(X0)|~subpopulations(X1,X2,X0,X3)|~outcompetes(X2,X1,X3)|greater_or_equal(growth_rate(X2,X3),zero))),
% 27.52/3.90 inference(cnf_transformation,[status(thm)],[f35])).
% 27.52/3.90 fof(f37,plain,(
% 27.52/3.90 ![B,D]: ((![C]: ((![A]: (~environment(A)|~subpopulations(B,C,A,D)))|~outcompetes(C,B,D)))|greater(zero,growth_rate(B,D)))),
% 27.52/3.90 inference(miniscoping,[status(thm)],[f8])).
% 27.52/3.90 fof(f38,plain,(
% 27.52/3.90 ![X0,X1,X2,X3]: (~environment(X0)|~subpopulations(X1,X2,X0,X3)|~outcompetes(X2,X1,X3)|greater(zero,growth_rate(X1,X3)))),
% 27.52/3.90 inference(cnf_transformation,[status(thm)],[f37])).
% 27.52/3.90 fof(f39,plain,(
% 27.52/3.90 ![B]: ((((![A]: ((~environment(A)|~subpopulations(first_movers,efficient_producers,A,B))|~greater_or_equal(B,equilibrium(A))))|growth_rate(first_movers,B)=zero)|greater(growth_rate(first_movers,B),zero))|greater(growth_rate(efficient_producers,B),zero))),
% 21.24/3.91 inference(miniscoping,[status(thm)],[f9])).
% 21.24/3.91 fof(f40,plain,(
% 21.24/3.91 ![X0,X1]: (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,equilibrium(X0))|growth_rate(first_movers,X1)=zero|greater(growth_rate(first_movers,X1),zero)|greater(growth_rate(efficient_producers,X1),zero))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f39])).
% 21.24/3.91 fof(f41,plain,(
% 21.24/3.91 ![B]: ((((![A]: ((~environment(A)|~subpopulations(first_movers,efficient_producers,A,B))|~greater_or_equal(B,equilibrium(A))))|growth_rate(first_movers,B)=zero)|greater(growth_rate(first_movers,B),zero))|greater(zero,growth_rate(first_movers,B)))),
% 21.24/3.91 inference(miniscoping,[status(thm)],[f10])).
% 21.24/3.91 fof(f42,plain,(
% 21.24/3.91 ![X0,X1]: (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,equilibrium(X0))|growth_rate(first_movers,X1)=zero|greater(growth_rate(first_movers,X1),zero)|greater(zero,growth_rate(first_movers,X1)))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f41])).
% 21.24/3.91 fof(f43,plain,(
% 21.24/3.91 ![B]: ((((![A]: ((~environment(A)|~subpopulations(first_movers,efficient_producers,A,B))|~greater_or_equal(B,equilibrium(A))))|growth_rate(first_movers,B)=zero)|greater(zero,growth_rate(efficient_producers,B)))|greater(growth_rate(efficient_producers,B),zero))),
% 21.24/3.91 inference(miniscoping,[status(thm)],[f11])).
% 21.24/3.91 fof(f44,plain,(
% 21.24/3.91 ![X0,X1]: (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,equilibrium(X0))|growth_rate(first_movers,X1)=zero|greater(zero,growth_rate(efficient_producers,X1))|greater(growth_rate(efficient_producers,X1),zero))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f43])).
% 21.24/3.91 fof(f45,plain,(
% 21.24/3.91 ![B]: ((((![A]: ((~environment(A)|~subpopulations(first_movers,efficient_producers,A,B))|~greater_or_equal(B,equilibrium(A))))|growth_rate(first_movers,B)=zero)|greater(zero,growth_rate(efficient_producers,B)))|greater(zero,growth_rate(first_movers,B)))),
% 21.24/3.91 inference(miniscoping,[status(thm)],[f12])).
% 21.24/3.91 fof(f46,plain,(
% 21.24/3.91 ![X0,X1]: (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,equilibrium(X0))|growth_rate(first_movers,X1)=zero|greater(zero,growth_rate(efficient_producers,X1))|greater(zero,growth_rate(first_movers,X1)))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f45])).
% 21.24/3.91 fof(f47,plain,(
% 21.24/3.91 ![B]: ((((![A]: ((~environment(A)|~subpopulations(first_movers,efficient_producers,A,B))|~greater_or_equal(B,equilibrium(A))))|growth_rate(efficient_producers,B)=zero)|greater(growth_rate(first_movers,B),zero))|greater(growth_rate(efficient_producers,B),zero))),
% 21.24/3.91 inference(miniscoping,[status(thm)],[f13])).
% 21.24/3.91 fof(f48,plain,(
% 21.24/3.91 ![X0,X1]: (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,equilibrium(X0))|growth_rate(efficient_producers,X1)=zero|greater(growth_rate(first_movers,X1),zero)|greater(growth_rate(efficient_producers,X1),zero))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f47])).
% 21.24/3.91 fof(f49,plain,(
% 21.24/3.91 ![B]: ((((![A]: ((~environment(A)|~subpopulations(first_movers,efficient_producers,A,B))|~greater_or_equal(B,equilibrium(A))))|growth_rate(efficient_producers,B)=zero)|greater(growth_rate(first_movers,B),zero))|greater(zero,growth_rate(first_movers,B)))),
% 21.24/3.91 inference(miniscoping,[status(thm)],[f14])).
% 21.24/3.91 fof(f50,plain,(
% 21.24/3.91 ![X0,X1]: (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,equilibrium(X0))|growth_rate(efficient_producers,X1)=zero|greater(growth_rate(first_movers,X1),zero)|greater(zero,growth_rate(first_movers,X1)))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f49])).
% 21.24/3.91 fof(f51,plain,(
% 21.24/3.91 ![B]: ((((![A]: ((~environment(A)|~subpopulations(first_movers,efficient_producers,A,B))|~greater_or_equal(B,equilibrium(A))))|growth_rate(efficient_producers,B)=zero)|greater(zero,growth_rate(efficient_producers,B)))|greater(growth_rate(efficient_producers,B),zero))),
% 21.24/3.91 inference(miniscoping,[status(thm)],[f15])).
% 21.24/3.91 fof(f52,plain,(
% 21.24/3.91 ![X0,X1]: (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,equilibrium(X0))|growth_rate(efficient_producers,X1)=zero|greater(zero,growth_rate(efficient_producers,X1))|greater(growth_rate(efficient_producers,X1),zero))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f51])).
% 21.24/3.91 fof(f53,plain,(
% 21.24/3.91 ![B]: ((((![A]: ((~environment(A)|~subpopulations(first_movers,efficient_producers,A,B))|~greater_or_equal(B,equilibrium(A))))|growth_rate(efficient_producers,B)=zero)|greater(zero,growth_rate(efficient_producers,B)))|greater(zero,growth_rate(first_movers,B)))),
% 21.24/3.91 inference(miniscoping,[status(thm)],[f16])).
% 21.24/3.91 fof(f54,plain,(
% 21.24/3.91 ![X0,X1]: (~environment(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,equilibrium(X0))|growth_rate(efficient_producers,X1)=zero|greater(zero,growth_rate(efficient_producers,X1))|greater(zero,growth_rate(first_movers,X1)))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f53])).
% 21.24/3.91 fof(f55,plain,(
% 21.24/3.91 ![X0]: (~environment(X0)|~stable(X0)|in_environment(X0,sk1(X0)))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f17])).
% 21.24/3.91 fof(f56,plain,(
% 21.24/3.91 ![B]: ((![A]: (((~environment(A)|~stable(A))|~subpopulations(first_movers,efficient_producers,A,B))|~greater_or_equal(B,sk1(A))))|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B)))),
% 21.24/3.91 inference(miniscoping,[status(thm)],[f18])).
% 21.24/3.91 fof(f57,plain,(
% 21.24/3.91 ![X0,X1]: (~environment(X0)|~stable(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,sk1(X0))|greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1)))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f56])).
% 21.24/3.91 fof(f58,plain,(
% 21.24/3.91 ![X0]: (~environment(X0)|~stable(X0)|in_environment(X0,sk2(X0)))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f19])).
% 21.24/3.91 fof(f59,plain,(
% 21.24/3.91 ![X0]: (~environment(X0)|~stable(X0)|greater_or_equal(sk2(X0),equilibrium(X0)))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f20])).
% 21.24/3.91 fof(f60,plain,(
% 21.24/3.91 environment(sk3)),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f21])).
% 21.24/3.91 fof(f61,plain,(
% 21.24/3.91 stable(sk3)),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f22])).
% 21.24/3.91 fof(f62,plain,(
% 21.24/3.91 ![X0]: (~in_environment(sk3,X0)|subpopulations(first_movers,efficient_producers,sk3,sk4(X0)))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f23])).
% 21.24/3.91 fof(f63,plain,(
% 21.24/3.91 ![X0]: (~in_environment(sk3,X0)|greater_or_equal(sk4(X0),X0))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f24])).
% 21.24/3.91 fof(f64,plain,(
% 21.24/3.91 ![X0]: (~in_environment(sk3,X0)|~outcompetes(efficient_producers,first_movers,sk4(X0)))),
% 21.24/3.91 inference(cnf_transformation,[status(thm)],[f25])).
% 21.24/3.91 fof(f65,plain,(
% 21.24/3.91 ![X0]: (greater_or_equal(X0,X0))),
% 21.24/3.91 inference(destructive_equality_resolution,[status(thm)],[f32])).
% 21.24/3.91 fof(f66,plain,(
% 21.24/3.91 ~environment(sk3)|in_environment(sk3,sk1(sk3))),
% 21.24/3.91 inference(resolution,[status(thm)],[f55,f61])).
% 21.24/3.91 fof(f67,definition,(
% 21.24/3.91 sQ0_spl <=> (environment(sk3))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f69,plain,(
% 21.24/3.91 ~environment(sk3)|sQ0_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f67])).
% 21.24/3.91 fof(f70,definition,(
% 21.24/3.91 sQ1_spl <=> (in_environment(sk3,sk1(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f71,plain,(
% 21.24/3.91 in_environment(sk3,sk1(sk3))|~sQ1_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f70])).
% 21.24/3.91 fof(f73,plain,(
% 21.24/3.91 ~sQ0_spl|sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f66,f67,f70])).
% 21.24/3.91 fof(f74,plain,(
% 21.24/3.91 $false|sQ0_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f69,f60])).
% 21.24/3.91 fof(f75,plain,(
% 21.24/3.91 sQ0_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f74])).
% 21.24/3.91 fof(f76,plain,(
% 21.24/3.91 greater_or_equal(sk4(sk1(sk3)),sk1(sk3))|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f71,f63])).
% 21.24/3.91 fof(f77,plain,(
% 21.24/3.91 subpopulations(first_movers,efficient_producers,sk3,sk4(sk1(sk3)))|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f71,f62])).
% 21.24/3.91 fof(f78,plain,(
% 21.24/3.91 ~environment(sk3)|in_environment(sk3,sk2(sk3))),
% 21.24/3.91 inference(resolution,[status(thm)],[f58,f61])).
% 21.24/3.91 fof(f79,definition,(
% 21.24/3.91 sQ2_spl <=> (in_environment(sk3,sk2(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f80,plain,(
% 21.24/3.91 in_environment(sk3,sk2(sk3))|~sQ2_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f79])).
% 21.24/3.91 fof(f82,plain,(
% 21.24/3.91 ~sQ0_spl|sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f78,f67,f79])).
% 21.24/3.91 fof(f83,plain,(
% 21.24/3.91 ~environment(sk3)|greater_or_equal(sk2(sk3),equilibrium(sk3))),
% 21.24/3.91 inference(resolution,[status(thm)],[f59,f61])).
% 21.24/3.91 fof(f84,definition,(
% 21.24/3.91 sQ3_spl <=> (greater_or_equal(sk2(sk3),equilibrium(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f85,plain,(
% 21.24/3.91 greater_or_equal(sk2(sk3),equilibrium(sk3))|~sQ3_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f84])).
% 21.24/3.91 fof(f87,plain,(
% 21.24/3.91 ~sQ0_spl|sQ3_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f83,f67,f84])).
% 21.24/3.91 fof(f88,plain,(
% 21.24/3.91 greater_or_equal(sk4(sk2(sk3)),sk2(sk3))|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f80,f63])).
% 21.24/3.91 fof(f89,plain,(
% 21.24/3.91 subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3)))|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f80,f62])).
% 21.24/3.91 fof(f90,plain,(
% 21.24/3.91 greater(sk2(sk3),equilibrium(sk3))|sk2(sk3)=equilibrium(sk3)|~sQ3_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f30,f85])).
% 21.24/3.91 fof(f92,definition,(
% 21.24/3.91 sQ4_spl <=> (greater(sk2(sk3),equilibrium(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f93,plain,(
% 21.24/3.91 greater(sk2(sk3),equilibrium(sk3))|~sQ4_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f92])).
% 21.24/3.91 fof(f95,definition,(
% 21.24/3.91 sQ5_spl <=> (sk2(sk3)=equilibrium(sk3))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f96,plain,(
% 21.24/3.91 sk2(sk3)=equilibrium(sk3)|~sQ5_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f95])).
% 21.24/3.91 fof(f98,plain,(
% 21.24/3.91 sQ4_spl|sQ5_spl|~sQ3_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f90,f92,f95,f84])).
% 21.24/3.91 fof(f99,plain,(
% 21.24/3.91 ![X0]: (~in_environment(sk3,X0)|greater(X0,sk2(sk3))|X0=sk2(sk3)|greater(sk2(sk3),X0)|~sQ2_spl)),
% 21.24/3.91 inference(resolution,[status(thm)],[f29,f80])).
% 21.24/3.91 fof(f100,plain,(
% 21.24/3.91 ![X0]: (~in_environment(sk3,X0)|greater(X0,sk1(sk3))|X0=sk1(sk3)|greater(sk1(sk3),X0)|~sQ1_spl)),
% 21.24/3.91 inference(resolution,[status(thm)],[f29,f71])).
% 21.24/3.91 fof(f101,plain,(
% 21.24/3.91 greater(sk2(sk3),sk2(sk3))|sk2(sk3)=sk2(sk3)|greater(sk2(sk3),sk2(sk3))|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f99,f80])).
% 21.24/3.91 fof(f102,plain,(
% 21.24/3.91 greater(sk1(sk3),sk2(sk3))|sk1(sk3)=sk2(sk3)|greater(sk2(sk3),sk1(sk3))|~sQ2_spl|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f99,f71])).
% 21.24/3.91 fof(f103,definition,(
% 21.24/3.91 sQ6_spl <=> (greater(sk2(sk3),sk2(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f104,plain,(
% 21.24/3.91 greater(sk2(sk3),sk2(sk3))|~sQ6_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f103])).
% 21.24/3.91 fof(f106,definition,(
% 21.24/3.91 sQ7_spl <=> (sk2(sk3)=sk2(sk3))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f109,plain,(
% 21.24/3.91 sQ6_spl|sQ7_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f101,f103,f106,f79])).
% 21.24/3.91 fof(f110,definition,(
% 21.24/3.91 sQ8_spl <=> (greater(sk1(sk3),sk2(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f111,plain,(
% 21.24/3.91 greater(sk1(sk3),sk2(sk3))|~sQ8_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f110])).
% 21.24/3.91 fof(f112,plain,(
% 21.24/3.91 ~greater(sk1(sk3),sk2(sk3))|sQ8_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f110])).
% 21.24/3.91 fof(f113,definition,(
% 21.24/3.91 sQ9_spl <=> (sk1(sk3)=sk2(sk3))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f114,plain,(
% 21.24/3.91 sk1(sk3)=sk2(sk3)|~sQ9_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f113])).
% 21.24/3.91 fof(f116,definition,(
% 21.24/3.91 sQ10_spl <=> (greater(sk2(sk3),sk1(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f117,plain,(
% 21.24/3.91 greater(sk2(sk3),sk1(sk3))|~sQ10_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f116])).
% 21.24/3.91 fof(f118,plain,(
% 21.24/3.91 ~greater(sk2(sk3),sk1(sk3))|sQ10_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f116])).
% 21.24/3.91 fof(f119,plain,(
% 21.24/3.91 sQ8_spl|sQ9_spl|sQ10_spl|~sQ2_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f102,f110,f113,f116,f79,f70])).
% 21.24/3.91 fof(f121,plain,(
% 21.24/3.91 greater(sk1(sk3),sk1(sk3))|sk1(sk3)=sk1(sk3)|greater(sk1(sk3),sk1(sk3))|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f100,f71])).
% 21.24/3.91 fof(f123,definition,(
% 21.24/3.91 sQ11_spl <=> (greater(sk1(sk3),sk1(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f124,plain,(
% 21.24/3.91 greater(sk1(sk3),sk1(sk3))|~sQ11_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f123])).
% 21.24/3.91 fof(f126,definition,(
% 21.24/3.91 sQ12_spl <=> (sk1(sk3)=sk1(sk3))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f129,plain,(
% 21.24/3.91 sQ11_spl|sQ12_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f121,f123,f126,f70])).
% 21.24/3.91 fof(f135,plain,(
% 21.24/3.91 greater_or_equal(sk2(sk3),sk1(sk3))|~sQ10_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f117,f31])).
% 21.24/3.91 fof(f140,plain,(
% 21.24/3.91 greater(sk4(sk1(sk3)),sk1(sk3))|sk4(sk1(sk3))=sk1(sk3)|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f76,f30])).
% 21.24/3.91 fof(f141,definition,(
% 21.24/3.91 sQ13_spl <=> (greater(sk4(sk1(sk3)),sk1(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f142,plain,(
% 21.24/3.91 greater(sk4(sk1(sk3)),sk1(sk3))|~sQ13_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f141])).
% 21.24/3.91 fof(f143,plain,(
% 21.24/3.91 ~greater(sk4(sk1(sk3)),sk1(sk3))|sQ13_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f141])).
% 21.24/3.91 fof(f144,definition,(
% 21.24/3.91 sQ14_spl <=> (sk4(sk1(sk3))=sk1(sk3))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f145,plain,(
% 21.24/3.91 sk4(sk1(sk3))=sk1(sk3)|~sQ14_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f144])).
% 21.24/3.91 fof(f147,plain,(
% 21.24/3.91 sQ13_spl|sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f140,f141,f144,f70])).
% 21.24/3.91 fof(f150,plain,(
% 21.24/3.91 subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))|~sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f145,f77])).
% 21.24/3.91 fof(f151,plain,(
% 21.24/3.91 ~in_environment(sk3,sk1(sk3))|~outcompetes(efficient_producers,first_movers,sk1(sk3))|~sQ14_spl),
% 21.24/3.91 inference(paramodulation,[status(thm)],[f145,f64])).
% 21.24/3.91 fof(f152,definition,(
% 21.24/3.91 sQ15_spl <=> (outcompetes(efficient_producers,first_movers,sk1(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f155,plain,(
% 21.24/3.91 ~sQ1_spl|~sQ15_spl|~sQ14_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f151,f70,f152,f144])).
% 21.24/3.91 fof(f156,plain,(
% 21.24/3.91 greater(sk4(sk2(sk3)),sk2(sk3))|sk4(sk2(sk3))=sk2(sk3)|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f88,f30])).
% 21.24/3.91 fof(f157,definition,(
% 21.24/3.91 sQ16_spl <=> (greater(sk4(sk2(sk3)),sk2(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f158,plain,(
% 21.24/3.91 greater(sk4(sk2(sk3)),sk2(sk3))|~sQ16_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f157])).
% 21.24/3.91 fof(f160,definition,(
% 21.24/3.91 sQ17_spl <=> (sk4(sk2(sk3))=sk2(sk3))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f161,plain,(
% 21.24/3.91 sk4(sk2(sk3))=sk2(sk3)|~sQ17_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f160])).
% 21.24/3.91 fof(f162,plain,(
% 21.24/3.91 ~sk4(sk2(sk3))=sk2(sk3)|sQ17_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f160])).
% 21.24/3.91 fof(f163,plain,(
% 21.24/3.91 sQ16_spl|sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f156,f157,f160,f79])).
% 21.24/3.91 fof(f166,plain,(
% 21.24/3.91 subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f161,f89])).
% 21.24/3.91 fof(f169,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|growth_rate(efficient_producers,sk4(sk1(sk3)))=zero|greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))|greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f77,f54])).
% 21.24/3.91 fof(f172,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|growth_rate(efficient_producers,sk4(sk1(sk3)))=zero|greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)|greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f77,f48])).
% 21.24/3.91 fof(f174,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|growth_rate(first_movers,sk4(sk1(sk3)))=zero|greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))|greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f77,f44])).
% 21.24/3.91 fof(f177,plain,(
% 21.24/3.91 ~environment(sk3)|~stable(sk3)|~greater_or_equal(sk4(sk1(sk3)),sk1(sk3))|greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f77,f57])).
% 21.24/3.91 fof(f180,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))|outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f77,f34])).
% 21.24/3.91 fof(f181,definition,(
% 21.24/3.91 sQ18_spl <=> (greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f182,plain,(
% 21.24/3.91 greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|~sQ18_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f181])).
% 21.24/3.91 fof(f183,plain,(
% 21.24/3.91 ~greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|sQ18_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f181])).
% 21.24/3.91 fof(f184,definition,(
% 21.24/3.91 sQ19_spl <=> (growth_rate(efficient_producers,sk4(sk1(sk3)))=zero)),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f185,plain,(
% 21.24/3.91 growth_rate(efficient_producers,sk4(sk1(sk3)))=zero|~sQ19_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f184])).
% 21.24/3.91 fof(f186,plain,(
% 21.24/3.91 ~growth_rate(efficient_producers,sk4(sk1(sk3)))=zero|sQ19_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f184])).
% 21.24/3.91 fof(f187,definition,(
% 21.24/3.91 sQ20_spl <=> (greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3)))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f188,plain,(
% 21.24/3.91 greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))|~sQ20_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f187])).
% 21.24/3.91 fof(f189,plain,(
% 21.24/3.91 ~greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))|sQ20_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f187])).
% 21.24/3.91 fof(f190,definition,(
% 21.24/3.91 sQ21_spl <=> (greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f193,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ18_spl|sQ19_spl|sQ20_spl|sQ21_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f169,f67,f181,f184,f187,f190,f70])).
% 21.24/3.91 fof(f194,definition,(
% 21.24/3.91 sQ22_spl <=> (greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f195,plain,(
% 21.24/3.91 greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~sQ22_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f194])).
% 21.24/3.91 fof(f198,definition,(
% 21.24/3.91 sQ23_spl <=> (greater(growth_rate(first_movers,sk4(sk1(sk3))),zero))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f199,plain,(
% 21.24/3.91 greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)|~sQ23_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f198])).
% 21.24/3.91 fof(f200,plain,(
% 21.24/3.91 ~greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)|sQ23_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f198])).
% 21.24/3.91 fof(f202,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ18_spl|sQ19_spl|sQ23_spl|sQ22_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f172,f67,f181,f184,f198,f194,f70])).
% 21.24/3.91 fof(f203,definition,(
% 21.24/3.91 sQ24_spl <=> (growth_rate(first_movers,sk4(sk1(sk3)))=zero)),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f204,plain,(
% 21.24/3.91 growth_rate(first_movers,sk4(sk1(sk3)))=zero|~sQ24_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f203])).
% 21.24/3.91 fof(f207,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ18_spl|sQ24_spl|sQ20_spl|sQ22_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f174,f67,f181,f203,f187,f194,f70])).
% 21.24/3.91 fof(f210,definition,(
% 21.24/3.91 sQ25_spl <=> (stable(sk3))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f212,plain,(
% 21.24/3.91 ~stable(sk3)|sQ25_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f210])).
% 21.24/3.91 fof(f213,definition,(
% 21.24/3.91 sQ26_spl <=> (greater_or_equal(sk4(sk1(sk3)),sk1(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f215,plain,(
% 21.24/3.91 ~greater_or_equal(sk4(sk1(sk3)),sk1(sk3))|sQ26_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f213])).
% 21.24/3.91 fof(f216,definition,(
% 21.24/3.91 sQ27_spl <=> (greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f217,plain,(
% 21.24/3.91 greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))|~sQ27_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f216])).
% 21.24/3.91 fof(f219,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ25_spl|~sQ26_spl|sQ27_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f177,f67,f210,f213,f216,f70])).
% 21.24/3.91 fof(f220,definition,(
% 21.24/3.91 sQ28_spl <=> (outcompetes(efficient_producers,first_movers,sk4(sk1(sk3))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f221,plain,(
% 21.24/3.91 outcompetes(efficient_producers,first_movers,sk4(sk1(sk3)))|~sQ28_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f220])).
% 21.24/3.91 fof(f224,definition,(
% 21.24/3.91 sQ29_spl <=> (greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f225,plain,(
% 21.24/3.91 greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~sQ29_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f224])).
% 21.24/3.91 fof(f226,plain,(
% 21.24/3.91 ~greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|sQ29_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f224])).
% 21.24/3.91 fof(f228,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ29_spl|~sQ21_spl|sQ28_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f180,f67,f224,f190,f220,f70])).
% 21.24/3.91 fof(f231,plain,(
% 21.24/3.91 greater(zero,zero)|~sQ19_spl|~sQ22_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f185,f195])).
% 21.24/3.91 fof(f232,plain,(
% 21.24/3.91 greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))|~sQ19_spl|~sQ27_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f185,f217])).
% 21.24/3.91 fof(f234,plain,(
% 21.24/3.91 $false|~sQ1_spl|sQ26_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f215,f76])).
% 21.24/3.91 fof(f235,plain,(
% 21.24/3.91 ~sQ1_spl|sQ26_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f234])).
% 21.24/3.91 fof(f236,plain,(
% 21.24/3.91 $false|sQ25_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f212,f61])).
% 21.24/3.91 fof(f237,plain,(
% 21.24/3.91 sQ25_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f236])).
% 21.24/3.91 fof(f240,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk2(sk3),equilibrium(sk3))|growth_rate(efficient_producers,sk2(sk3))=zero|greater(zero,growth_rate(efficient_producers,sk2(sk3)))|greater(zero,growth_rate(first_movers,sk2(sk3)))|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f166,f54])).
% 21.24/3.91 fof(f241,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk2(sk3),equilibrium(sk3))|growth_rate(efficient_producers,sk2(sk3))=zero|greater(zero,growth_rate(efficient_producers,sk2(sk3)))|greater(growth_rate(efficient_producers,sk2(sk3)),zero)|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f166,f52])).
% 21.24/3.91 fof(f242,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk2(sk3),equilibrium(sk3))|growth_rate(efficient_producers,sk2(sk3))=zero|greater(growth_rate(first_movers,sk2(sk3)),zero)|greater(zero,growth_rate(first_movers,sk2(sk3)))|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f166,f50])).
% 21.24/3.91 fof(f243,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk2(sk3),equilibrium(sk3))|growth_rate(efficient_producers,sk2(sk3))=zero|greater(growth_rate(first_movers,sk2(sk3)),zero)|greater(growth_rate(efficient_producers,sk2(sk3)),zero)|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f166,f48])).
% 21.24/3.91 fof(f244,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk2(sk3),equilibrium(sk3))|growth_rate(first_movers,sk2(sk3))=zero|greater(zero,growth_rate(efficient_producers,sk2(sk3)))|greater(zero,growth_rate(first_movers,sk2(sk3)))|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f166,f46])).
% 21.24/3.91 fof(f245,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk2(sk3),equilibrium(sk3))|growth_rate(first_movers,sk2(sk3))=zero|greater(zero,growth_rate(efficient_producers,sk2(sk3)))|greater(growth_rate(efficient_producers,sk2(sk3)),zero)|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f166,f44])).
% 21.24/3.91 fof(f246,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk2(sk3),equilibrium(sk3))|growth_rate(first_movers,sk2(sk3))=zero|greater(growth_rate(first_movers,sk2(sk3)),zero)|greater(zero,growth_rate(first_movers,sk2(sk3)))|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f166,f42])).
% 21.24/3.91 fof(f247,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk2(sk3),equilibrium(sk3))|growth_rate(first_movers,sk2(sk3))=zero|greater(growth_rate(first_movers,sk2(sk3)),zero)|greater(growth_rate(efficient_producers,sk2(sk3)),zero)|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f166,f40])).
% 21.24/3.91 fof(f248,plain,(
% 21.24/3.91 ~environment(sk3)|~stable(sk3)|~greater_or_equal(sk2(sk3),sk1(sk3))|greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f166,f57])).
% 21.24/3.91 fof(f251,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(growth_rate(efficient_producers,sk2(sk3)),zero)|~greater(zero,growth_rate(first_movers,sk2(sk3)))|outcompetes(efficient_producers,first_movers,sk2(sk3))|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f166,f34])).
% 21.24/3.91 fof(f252,definition,(
% 21.24/3.91 sQ30_spl <=> (growth_rate(efficient_producers,sk2(sk3))=zero)),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f253,plain,(
% 21.24/3.91 growth_rate(efficient_producers,sk2(sk3))=zero|~sQ30_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f252])).
% 21.24/3.91 fof(f255,definition,(
% 21.24/3.91 sQ31_spl <=> (greater(zero,growth_rate(efficient_producers,sk2(sk3))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f256,plain,(
% 21.24/3.91 greater(zero,growth_rate(efficient_producers,sk2(sk3)))|~sQ31_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f255])).
% 21.24/3.91 fof(f258,definition,(
% 21.24/3.91 sQ32_spl <=> (greater(zero,growth_rate(first_movers,sk2(sk3))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f259,plain,(
% 21.24/3.91 greater(zero,growth_rate(first_movers,sk2(sk3)))|~sQ32_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f258])).
% 21.24/3.91 fof(f260,plain,(
% 21.24/3.91 ~greater(zero,growth_rate(first_movers,sk2(sk3)))|sQ32_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f258])).
% 21.24/3.91 fof(f261,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ3_spl|sQ30_spl|sQ31_spl|sQ32_spl|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f240,f67,f84,f252,f255,f258,f160,f79])).
% 21.24/3.91 fof(f262,definition,(
% 21.24/3.91 sQ33_spl <=> (greater(growth_rate(efficient_producers,sk2(sk3)),zero))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f263,plain,(
% 21.24/3.91 greater(growth_rate(efficient_producers,sk2(sk3)),zero)|~sQ33_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f262])).
% 21.24/3.91 fof(f265,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ3_spl|sQ30_spl|sQ31_spl|sQ33_spl|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f241,f67,f84,f252,f255,f262,f160,f79])).
% 21.24/3.91 fof(f266,definition,(
% 21.24/3.91 sQ34_spl <=> (greater(growth_rate(first_movers,sk2(sk3)),zero))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f267,plain,(
% 21.24/3.91 greater(growth_rate(first_movers,sk2(sk3)),zero)|~sQ34_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f266])).
% 21.24/3.91 fof(f269,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ3_spl|sQ30_spl|sQ34_spl|sQ32_spl|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f242,f67,f84,f252,f266,f258,f160,f79])).
% 21.24/3.91 fof(f270,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ3_spl|sQ30_spl|sQ34_spl|sQ33_spl|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f243,f67,f84,f252,f266,f262,f160,f79])).
% 21.24/3.91 fof(f271,definition,(
% 21.24/3.91 sQ35_spl <=> (growth_rate(first_movers,sk2(sk3))=zero)),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f272,plain,(
% 21.24/3.91 growth_rate(first_movers,sk2(sk3))=zero|~sQ35_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f271])).
% 21.24/3.91 fof(f274,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ3_spl|sQ35_spl|sQ31_spl|sQ32_spl|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f244,f67,f84,f271,f255,f258,f160,f79])).
% 21.24/3.91 fof(f275,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ3_spl|sQ35_spl|sQ31_spl|sQ33_spl|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f245,f67,f84,f271,f255,f262,f160,f79])).
% 21.24/3.91 fof(f276,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ3_spl|sQ35_spl|sQ34_spl|sQ32_spl|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f246,f67,f84,f271,f266,f258,f160,f79])).
% 21.24/3.91 fof(f277,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ3_spl|sQ35_spl|sQ34_spl|sQ33_spl|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f247,f67,f84,f271,f266,f262,f160,f79])).
% 21.24/3.91 fof(f278,definition,(
% 21.24/3.91 sQ36_spl <=> (greater_or_equal(sk2(sk3),sk1(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f279,plain,(
% 21.24/3.91 greater_or_equal(sk2(sk3),sk1(sk3))|~sQ36_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f278])).
% 21.24/3.91 fof(f280,plain,(
% 21.24/3.91 ~greater_or_equal(sk2(sk3),sk1(sk3))|sQ36_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f278])).
% 21.24/3.91 fof(f281,definition,(
% 21.24/3.91 sQ37_spl <=> (greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f282,plain,(
% 21.24/3.91 greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))|~sQ37_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f281])).
% 21.24/3.91 fof(f284,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ25_spl|~sQ36_spl|sQ37_spl|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f248,f67,f210,f278,f281,f160,f79])).
% 21.24/3.91 fof(f285,definition,(
% 21.24/3.91 sQ38_spl <=> (outcompetes(efficient_producers,first_movers,sk2(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f287,plain,(
% 21.24/3.91 ~outcompetes(efficient_producers,first_movers,sk2(sk3))|sQ38_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f285])).
% 21.24/3.91 fof(f289,definition,(
% 21.24/3.91 sQ39_spl <=> (greater_or_equal(growth_rate(efficient_producers,sk2(sk3)),zero))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f293,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ39_spl|~sQ32_spl|sQ38_spl|~sQ17_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f251,f67,f289,f258,f285,f160,f79])).
% 21.24/3.91 fof(f294,plain,(
% 21.24/3.91 greater(zero,zero)|~sQ35_spl|~sQ34_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f272,f267])).
% 21.24/3.91 fof(f297,plain,(
% 21.24/3.91 $false|~sQ10_spl|sQ36_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f280,f135])).
% 21.24/3.91 fof(f298,plain,(
% 21.24/3.91 ~sQ10_spl|sQ36_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f297])).
% 21.24/3.91 fof(f299,plain,(
% 21.24/3.91 ![X0]: (~greater(sk1(sk3),X0)|greater(sk4(sk1(sk3)),X0)|~sQ13_spl)),
% 21.24/3.91 inference(resolution,[status(thm)],[f142,f27])).
% 21.24/3.91 fof(f301,plain,(
% 21.24/3.91 ~in_environment(sk3,sk2(sk3))|~outcompetes(efficient_producers,first_movers,sk2(sk3))|~sQ17_spl),
% 21.24/3.91 inference(paramodulation,[status(thm)],[f161,f64])).
% 21.24/3.91 fof(f302,plain,(
% 21.24/3.91 ~sQ2_spl|~sQ38_spl|~sQ17_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f301,f79,f285,f160])).
% 21.24/3.91 fof(f303,plain,(
% 21.24/3.91 greater(zero,growth_rate(first_movers,sk2(sk3)))|~sQ30_spl|~sQ37_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f253,f282])).
% 21.24/3.91 fof(f304,plain,(
% 21.24/3.91 ~greater(zero,zero)|~sQ35_spl|sQ32_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f272,f260])).
% 21.24/3.91 fof(f305,plain,(
% 21.24/3.91 sQ32_spl|~sQ30_spl|~sQ37_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f303,f258,f252,f281])).
% 21.24/3.91 fof(f306,plain,(
% 21.24/3.91 ~in_environment(sk3,sk1(sk3))|~sQ28_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f221,f64])).
% 21.24/3.91 fof(f307,plain,(
% 21.24/3.91 $false|~sQ1_spl|~sQ28_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f306,f71])).
% 21.24/3.91 fof(f308,plain,(
% 21.24/3.91 ~sQ1_spl|~sQ28_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f307])).
% 21.24/3.91 fof(f309,plain,(
% 21.24/3.91 ![X0]: (~greater(growth_rate(first_movers,sk4(sk1(sk3))),X0)|greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)|~sQ27_spl)),
% 21.24/3.91 inference(resolution,[status(thm)],[f217,f27])).
% 21.24/3.91 fof(f310,plain,(
% 21.24/3.91 greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))|~sQ27_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f217,f31])).
% 21.24/3.91 fof(f311,plain,(
% 21.24/3.91 ![X0]: (~greater(sk2(sk3),X0)|greater(sk1(sk3),X0)|~sQ8_spl)),
% 21.24/3.91 inference(resolution,[status(thm)],[f111,f27])).
% 21.24/3.91 fof(f324,plain,(
% 21.24/3.91 greater(sk1(sk3),equilibrium(sk3))|~sQ8_spl|~sQ4_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f311,f93])).
% 21.24/3.91 fof(f326,plain,(
% 21.24/3.91 greater_or_equal(sk1(sk3),equilibrium(sk3))|~sQ8_spl|~sQ4_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f324,f31])).
% 21.24/3.91 fof(f327,plain,(
% 21.24/3.91 greater(sk1(sk3),equilibrium(sk3))|sk1(sk3)=equilibrium(sk3)|~sQ8_spl|~sQ4_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f326,f30])).
% 21.24/3.91 fof(f328,definition,(
% 21.24/3.91 sQ40_spl <=> (greater(sk1(sk3),equilibrium(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f329,plain,(
% 21.24/3.91 greater(sk1(sk3),equilibrium(sk3))|~sQ40_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f328])).
% 21.24/3.91 fof(f330,plain,(
% 21.24/3.91 ~greater(sk1(sk3),equilibrium(sk3))|sQ40_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f328])).
% 21.24/3.91 fof(f331,definition,(
% 21.24/3.91 sQ41_spl <=> (sk1(sk3)=equilibrium(sk3))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f332,plain,(
% 21.24/3.91 sk1(sk3)=equilibrium(sk3)|~sQ41_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f331])).
% 21.24/3.91 fof(f333,plain,(
% 21.24/3.91 ~sk1(sk3)=equilibrium(sk3)|sQ41_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f331])).
% 21.24/3.91 fof(f334,plain,(
% 21.24/3.91 sQ40_spl|sQ41_spl|~sQ8_spl|~sQ4_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f327,f328,f331,f110,f92])).
% 21.24/3.91 fof(f339,plain,(
% 21.24/3.91 $false|sQ32_spl|~sQ35_spl|~sQ34_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f294,f304])).
% 21.24/3.91 fof(f340,plain,(
% 21.24/3.91 sQ32_spl|~sQ35_spl|~sQ34_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f339])).
% 21.24/3.91 fof(f341,plain,(
% 21.24/3.91 $false|~sQ35_spl|sQ32_spl|~sQ19_spl|~sQ22_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f231,f304])).
% 21.24/3.91 fof(f342,plain,(
% 21.24/3.91 ~sQ35_spl|sQ32_spl|~sQ19_spl|~sQ22_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f341])).
% 21.24/3.91 fof(f346,plain,(
% 21.24/3.91 greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~sQ24_spl|~sQ27_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f204,f310])).
% 21.24/3.91 fof(f349,plain,(
% 21.24/3.91 ~greater_or_equal(equilibrium(sk3),sk1(sk3))|~sQ5_spl|sQ36_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f96,f280])).
% 21.24/3.91 fof(f351,plain,(
% 21.24/3.91 ~outcompetes(efficient_producers,first_movers,equilibrium(sk3))|~sQ5_spl|sQ38_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f96,f287])).
% 21.24/3.91 fof(f373,plain,(
% 21.24/3.91 sk1(sk3)=equilibrium(sk3)|~sQ5_spl|~sQ9_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f96,f114])).
% 21.24/3.91 fof(f374,plain,(
% 21.24/3.91 growth_rate(efficient_producers,equilibrium(sk3))=zero|~sQ5_spl|~sQ30_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f96,f253])).
% 21.24/3.91 fof(f386,plain,(
% 21.24/3.91 ~greater_or_equal(equilibrium(sk3),equilibrium(sk3))|~sQ9_spl|~sQ5_spl|sQ36_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f373,f349])).
% 21.24/3.91 fof(f387,plain,(
% 21.24/3.91 $false|~sQ9_spl|~sQ5_spl|sQ36_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f386,f65])).
% 21.24/3.91 fof(f388,plain,(
% 21.24/3.91 ~sQ9_spl|~sQ5_spl|sQ36_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f387])).
% 21.24/3.91 fof(f404,plain,(
% 21.24/3.91 greater_or_equal(sk4(sk2(sk3)),sk2(sk3))|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f80,f63])).
% 21.24/3.91 fof(f405,plain,(
% 21.24/3.91 subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3)))|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f80,f62])).
% 21.24/3.91 fof(f478,plain,(
% 21.24/3.91 greater_or_equal(sk1(sk3),equilibrium(sk3))|~sQ40_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f329,f31])).
% 21.24/3.91 fof(f494,plain,(
% 21.24/3.91 greater(sk4(sk1(sk3)),equilibrium(sk3))|~sQ13_spl|~sQ40_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f299,f329])).
% 21.24/3.91 fof(f496,plain,(
% 21.24/3.91 greater(sk4(sk1(sk3)),sk2(sk3))|~sQ13_spl|~sQ8_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f299,f111])).
% 21.24/3.91 fof(f499,plain,(
% 21.24/3.91 greater_or_equal(sk4(sk1(sk3)),sk2(sk3))|~sQ13_spl|~sQ8_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f496,f31])).
% 21.24/3.91 fof(f502,plain,(
% 21.24/3.91 greater(sk4(sk1(sk3)),sk2(sk3))|sk4(sk1(sk3))=sk2(sk3)|~sQ13_spl|~sQ8_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f499,f30])).
% 21.24/3.91 fof(f503,definition,(
% 21.24/3.91 sQ43_spl <=> (greater(sk4(sk1(sk3)),sk2(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f504,plain,(
% 21.24/3.91 greater(sk4(sk1(sk3)),sk2(sk3))|~sQ43_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f503])).
% 21.24/3.91 fof(f506,definition,(
% 21.24/3.91 sQ44_spl <=> (sk4(sk1(sk3))=sk2(sk3))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f507,plain,(
% 21.24/3.91 sk4(sk1(sk3))=sk2(sk3)|~sQ44_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f506])).
% 21.24/3.91 fof(f508,plain,(
% 21.24/3.91 ~sk4(sk1(sk3))=sk2(sk3)|sQ44_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f506])).
% 21.24/3.91 fof(f509,plain,(
% 21.24/3.91 sQ43_spl|sQ44_spl|~sQ13_spl|~sQ8_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f502,f503,f506,f141,f110])).
% 21.24/3.91 fof(f511,plain,(
% 21.24/3.91 greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|~sQ13_spl|~sQ40_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f494,f31])).
% 21.24/3.91 fof(f512,plain,(
% 21.24/3.91 $false|sQ18_spl|~sQ13_spl|~sQ40_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f511,f183])).
% 21.24/3.91 fof(f513,plain,(
% 21.24/3.91 sQ18_spl|~sQ13_spl|~sQ40_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f512])).
% 21.24/3.91 fof(f521,plain,(
% 21.24/3.91 ~greater(sk2(sk3),equilibrium(sk3))|~sQ41_spl|sQ10_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f332,f118])).
% 21.24/3.91 fof(f531,plain,(
% 21.24/3.91 greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|~sQ41_spl|~sQ1_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f332,f76])).
% 21.24/3.91 fof(f549,plain,(
% 21.24/3.91 $false|~sQ4_spl|~sQ41_spl|sQ10_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f521,f93])).
% 21.24/3.91 fof(f550,plain,(
% 21.24/3.91 ~sQ4_spl|~sQ41_spl|sQ10_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f549])).
% 21.24/3.91 fof(f569,plain,(
% 21.24/3.91 sQ21_spl|~sQ19_spl|~sQ27_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f232,f190,f184,f216])).
% 21.24/3.91 fof(f577,plain,(
% 21.24/3.91 ~greater_or_equal(sk2(sk3),equilibrium(sk3))|~sQ44_spl|sQ18_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f507,f183])).
% 21.24/3.91 fof(f578,plain,(
% 21.24/3.91 $false|~sQ3_spl|~sQ44_spl|sQ18_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f577,f85])).
% 21.24/3.91 fof(f579,plain,(
% 21.24/3.91 ~sQ3_spl|~sQ44_spl|sQ18_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f578])).
% 21.24/3.91 fof(f586,plain,(
% 21.24/3.91 greater(zero,zero)|~sQ30_spl|~sQ33_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f253,f263])).
% 21.24/3.91 fof(f598,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|growth_rate(efficient_producers,sk4(sk2(sk3)))=zero|greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))|greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f405,f54])).
% 21.24/3.91 fof(f599,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|growth_rate(efficient_producers,sk4(sk2(sk3)))=zero|greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))|greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f405,f52])).
% 21.24/3.91 fof(f600,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|growth_rate(efficient_producers,sk4(sk2(sk3)))=zero|greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)|greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f405,f50])).
% 21.24/3.91 fof(f601,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|growth_rate(efficient_producers,sk4(sk2(sk3)))=zero|greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)|greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f405,f48])).
% 21.24/3.91 fof(f602,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|growth_rate(first_movers,sk4(sk2(sk3)))=zero|greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))|greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f405,f46])).
% 21.24/3.91 fof(f603,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|growth_rate(first_movers,sk4(sk2(sk3)))=zero|greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))|greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f405,f44])).
% 21.24/3.91 fof(f604,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|growth_rate(first_movers,sk4(sk2(sk3)))=zero|greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)|greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f405,f42])).
% 21.24/3.91 fof(f606,plain,(
% 21.24/3.91 ~environment(sk3)|~stable(sk3)|~greater_or_equal(sk4(sk2(sk3)),sk1(sk3))|greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f405,f57])).
% 21.24/3.91 fof(f609,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|~greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))|~sQ2_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f405,f34])).
% 21.24/3.91 fof(f610,definition,(
% 21.24/3.91 sQ45_spl <=> (greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f612,plain,(
% 21.24/3.91 ~greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|sQ45_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f610])).
% 21.24/3.91 fof(f613,definition,(
% 21.24/3.91 sQ46_spl <=> (growth_rate(efficient_producers,sk4(sk2(sk3)))=zero)),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f614,plain,(
% 21.24/3.91 growth_rate(efficient_producers,sk4(sk2(sk3)))=zero|~sQ46_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f613])).
% 21.24/3.91 fof(f615,plain,(
% 21.24/3.91 ~growth_rate(efficient_producers,sk4(sk2(sk3)))=zero|sQ46_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f613])).
% 21.24/3.91 fof(f616,definition,(
% 21.24/3.91 sQ47_spl <=> (greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3)))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f617,plain,(
% 21.24/3.91 greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))|~sQ47_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f616])).
% 21.24/3.91 fof(f618,plain,(
% 21.24/3.91 ~greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))|sQ47_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f616])).
% 21.24/3.91 fof(f619,definition,(
% 21.24/3.91 sQ48_spl <=> (greater(zero,growth_rate(first_movers,sk4(sk2(sk3)))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f621,plain,(
% 21.24/3.91 ~greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|sQ48_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f619])).
% 21.24/3.91 fof(f622,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ45_spl|sQ46_spl|sQ47_spl|sQ48_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f598,f67,f610,f613,f616,f619,f79])).
% 21.24/3.91 fof(f623,definition,(
% 21.24/3.91 sQ49_spl <=> (greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f624,plain,(
% 21.24/3.91 greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|~sQ49_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f623])).
% 21.24/3.91 fof(f625,plain,(
% 21.24/3.91 ~greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|sQ49_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f623])).
% 21.24/3.91 fof(f626,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ45_spl|sQ46_spl|sQ47_spl|sQ49_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f599,f67,f610,f613,f616,f623,f79])).
% 21.24/3.91 fof(f627,definition,(
% 21.24/3.91 sQ50_spl <=> (greater(growth_rate(first_movers,sk4(sk2(sk3))),zero))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f628,plain,(
% 21.24/3.91 greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)|~sQ50_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f627])).
% 21.24/3.91 fof(f629,plain,(
% 21.24/3.91 ~greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)|sQ50_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f627])).
% 21.24/3.91 fof(f630,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ45_spl|sQ46_spl|sQ50_spl|sQ48_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f600,f67,f610,f613,f627,f619,f79])).
% 21.24/3.91 fof(f631,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ45_spl|sQ46_spl|sQ50_spl|sQ49_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f601,f67,f610,f613,f627,f623,f79])).
% 21.24/3.91 fof(f632,definition,(
% 21.24/3.91 sQ51_spl <=> (growth_rate(first_movers,sk4(sk2(sk3)))=zero)),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f633,plain,(
% 21.24/3.91 growth_rate(first_movers,sk4(sk2(sk3)))=zero|~sQ51_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f632])).
% 21.24/3.91 fof(f635,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ45_spl|sQ51_spl|sQ47_spl|sQ48_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f602,f67,f610,f632,f616,f619,f79])).
% 21.24/3.91 fof(f636,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ45_spl|sQ51_spl|sQ47_spl|sQ49_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f603,f67,f610,f632,f616,f623,f79])).
% 21.24/3.91 fof(f637,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ45_spl|sQ51_spl|sQ50_spl|sQ48_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f604,f67,f610,f632,f627,f619,f79])).
% 21.24/3.91 fof(f639,definition,(
% 21.24/3.91 sQ52_spl <=> (greater_or_equal(sk4(sk2(sk3)),sk1(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f641,plain,(
% 21.24/3.91 ~greater_or_equal(sk4(sk2(sk3)),sk1(sk3))|sQ52_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f639])).
% 21.24/3.91 fof(f642,definition,(
% 21.24/3.91 sQ53_spl <=> (greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f643,plain,(
% 21.24/3.91 greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))|~sQ53_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f642])).
% 21.24/3.91 fof(f644,plain,(
% 21.24/3.91 ~greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))|sQ53_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f642])).
% 21.24/3.91 fof(f645,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ25_spl|~sQ52_spl|sQ53_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f606,f67,f210,f639,f642,f79])).
% 21.24/3.91 fof(f646,definition,(
% 21.24/3.91 sQ54_spl <=> (outcompetes(efficient_producers,first_movers,sk4(sk2(sk3))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f647,plain,(
% 21.24/3.91 outcompetes(efficient_producers,first_movers,sk4(sk2(sk3)))|~sQ54_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f646])).
% 21.24/3.91 fof(f650,definition,(
% 21.24/3.91 sQ55_spl <=> (greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f651,plain,(
% 21.24/3.91 greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|~sQ55_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f650])).
% 21.24/3.91 fof(f652,plain,(
% 21.24/3.91 ~greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|sQ55_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f650])).
% 21.24/3.91 fof(f654,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ55_spl|~sQ48_spl|sQ54_spl|~sQ2_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f609,f67,f650,f619,f646,f79])).
% 21.24/3.91 fof(f655,plain,(
% 21.24/3.91 greater(zero,zero)|~sQ51_spl|~sQ50_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f633,f628])).
% 21.24/3.91 fof(f656,plain,(
% 21.24/3.91 greater(zero,zero)|~sQ46_spl|~sQ47_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f614,f617])).
% 21.24/3.91 fof(f657,plain,(
% 21.24/3.91 greater(zero,zero)|~sQ46_spl|~sQ49_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f614,f624])).
% 21.24/3.91 fof(f658,plain,(
% 21.24/3.91 greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ46_spl|~sQ53_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f614,f643])).
% 21.24/3.91 fof(f659,plain,(
% 21.24/3.91 greater(zero,zero)|~sQ51_spl|~sQ46_spl|~sQ53_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f633,f658])).
% 21.24/3.91 fof(f690,plain,(
% 21.24/3.91 ![X0]: (~greater(sk2(sk3),X0)|greater(sk4(sk2(sk3)),X0)|~sQ16_spl)),
% 21.24/3.91 inference(resolution,[status(thm)],[f158,f27])).
% 21.24/3.91 fof(f698,plain,(
% 21.24/3.91 greater(sk4(sk1(sk3)),equilibrium(sk3))|sk4(sk1(sk3))=equilibrium(sk3)|~sQ18_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f182,f30])).
% 21.24/3.91 fof(f699,definition,(
% 21.24/3.91 sQ56_spl <=> (greater(sk4(sk1(sk3)),equilibrium(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f700,plain,(
% 21.24/3.91 greater(sk4(sk1(sk3)),equilibrium(sk3))|~sQ56_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f699])).
% 21.24/3.91 fof(f701,plain,(
% 21.24/3.91 ~greater(sk4(sk1(sk3)),equilibrium(sk3))|sQ56_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f699])).
% 21.24/3.91 fof(f702,definition,(
% 21.24/3.91 sQ57_spl <=> (sk4(sk1(sk3))=equilibrium(sk3))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f703,plain,(
% 21.24/3.91 sk4(sk1(sk3))=equilibrium(sk3)|~sQ57_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f702])).
% 21.24/3.91 fof(f705,plain,(
% 21.24/3.91 sQ56_spl|sQ57_spl|~sQ18_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f698,f699,f702,f181])).
% 21.24/3.91 fof(f726,plain,(
% 21.24/3.91 ~in_environment(sk3,sk1(sk3))|~outcompetes(efficient_producers,first_movers,equilibrium(sk3))|~sQ57_spl),
% 21.24/3.91 inference(paramodulation,[status(thm)],[f703,f64])).
% 21.24/3.91 fof(f727,definition,(
% 21.24/3.91 sQ58_spl <=> (outcompetes(efficient_producers,first_movers,equilibrium(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f730,plain,(
% 21.24/3.91 ~sQ1_spl|~sQ58_spl|~sQ57_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f726,f70,f727,f702])).
% 21.24/3.91 fof(f757,plain,(
% 21.24/3.91 ~in_environment(sk3,sk2(sk3))|~sQ54_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f647,f64])).
% 21.24/3.91 fof(f758,plain,(
% 21.24/3.91 $false|~sQ2_spl|~sQ54_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f757,f80])).
% 21.24/3.91 fof(f759,plain,(
% 21.24/3.91 ~sQ2_spl|~sQ54_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f758])).
% 21.24/3.91 fof(f760,plain,(
% 21.24/3.91 ~greater(zero,zero)|~sQ51_spl|sQ48_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f633,f621])).
% 21.24/3.91 fof(f761,plain,(
% 21.24/3.91 $false|~sQ35_spl|~sQ34_spl|~sQ51_spl|sQ48_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f760,f294])).
% 21.24/3.91 fof(f762,plain,(
% 21.24/3.91 ~sQ35_spl|~sQ34_spl|~sQ51_spl|sQ48_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f761])).
% 21.24/3.91 fof(f763,plain,(
% 21.24/3.91 $false|~sQ51_spl|sQ48_spl|~sQ46_spl|~sQ49_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f657,f760])).
% 21.24/3.91 fof(f764,plain,(
% 21.24/3.91 ~sQ51_spl|sQ48_spl|~sQ46_spl|~sQ49_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f763])).
% 21.24/3.91 fof(f765,plain,(
% 21.24/3.91 $false|sQ48_spl|~sQ51_spl|~sQ50_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f655,f760])).
% 21.24/3.91 fof(f766,plain,(
% 21.24/3.91 sQ48_spl|~sQ51_spl|~sQ50_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f765])).
% 21.24/3.91 fof(f767,plain,(
% 21.24/3.91 $false|~sQ51_spl|sQ48_spl|~sQ30_spl|~sQ33_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f586,f760])).
% 21.24/3.91 fof(f768,plain,(
% 21.24/3.91 ~sQ51_spl|sQ48_spl|~sQ30_spl|~sQ33_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f767])).
% 21.24/3.91 fof(f771,plain,(
% 21.24/3.91 ![X0]: (~greater(growth_rate(efficient_producers,sk4(sk1(sk3))),X0)|greater(zero,X0)|~sQ20_spl)),
% 21.24/3.91 inference(resolution,[status(thm)],[f188,f27])).
% 21.24/3.91 fof(f774,plain,(
% 21.24/3.91 greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~sQ22_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f195,f31])).
% 21.24/3.91 fof(f780,plain,(
% 21.24/3.91 greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|~sQ56_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f700,f31])).
% 21.24/3.91 fof(f782,plain,(
% 21.24/3.91 greater_or_equal(sk4(sk1(sk3)),sk2(sk3))|~sQ43_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f504,f31])).
% 21.24/3.91 fof(f797,plain,(
% 21.24/3.91 ![X0]: (~greater(growth_rate(efficient_producers,sk4(sk2(sk3))),X0)|greater(zero,X0)|~sQ47_spl)),
% 21.24/3.91 inference(resolution,[status(thm)],[f617,f27])).
% 21.24/3.91 fof(f800,plain,(
% 21.24/3.91 greater_or_equal(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|~sQ49_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f624,f31])).
% 21.24/3.91 fof(f801,plain,(
% 21.24/3.91 ![X0]: (~greater(growth_rate(first_movers,sk4(sk2(sk3))),X0)|greater(growth_rate(efficient_producers,sk4(sk2(sk3))),X0)|~sQ53_spl)),
% 21.24/3.91 inference(resolution,[status(thm)],[f643,f27])).
% 21.24/3.91 fof(f804,plain,(
% 21.24/3.91 greater(sk4(sk2(sk3)),sk1(sk3))|~sQ16_spl|~sQ10_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f690,f117])).
% 21.24/3.91 fof(f806,plain,(
% 21.24/3.91 greater(sk4(sk2(sk3)),equilibrium(sk3))|~sQ16_spl|~sQ4_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f690,f93])).
% 21.24/3.91 fof(f807,plain,(
% 21.24/3.91 greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~sQ27_spl|~sQ23_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f309,f199])).
% 21.24/3.91 fof(f816,plain,(
% 21.24/3.91 greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))|~sQ20_spl|~sQ27_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f771,f217])).
% 21.24/3.91 fof(f818,plain,(
% 21.24/3.91 sQ21_spl|~sQ20_spl|~sQ27_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f816,f190,f187,f216])).
% 21.24/3.91 fof(f833,plain,(
% 21.24/3.91 sQ29_spl|~sQ24_spl|~sQ27_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f346,f224,f203,f216])).
% 21.24/3.91 fof(f835,plain,(
% 21.24/3.91 ~greater_or_equal(zero,zero)|~sQ19_spl|sQ29_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f185,f226])).
% 21.24/3.91 fof(f836,plain,(
% 21.24/3.91 $false|~sQ19_spl|sQ29_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f835,f65])).
% 21.24/3.91 fof(f837,plain,(
% 21.24/3.91 ~sQ19_spl|sQ29_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f836])).
% 21.24/3.91 fof(f838,plain,(
% 21.24/3.91 sQ29_spl|~sQ22_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f774,f224,f194])).
% 21.24/3.91 fof(f839,plain,(
% 21.24/3.91 sQ22_spl|~sQ27_spl|~sQ23_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f807,f194,f216,f198])).
% 21.24/3.91 fof(f842,plain,(
% 21.24/3.91 sQ18_spl|~sQ56_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f780,f181,f699])).
% 21.24/3.91 fof(f850,plain,(
% 21.24/3.91 sQ48_spl|~sQ46_spl|~sQ53_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f658,f619,f613,f642])).
% 21.24/3.91 fof(f851,plain,(
% 21.24/3.91 ~greater(zero,zero)|~sQ46_spl|sQ49_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f614,f625])).
% 21.24/3.91 fof(f852,plain,(
% 21.24/3.91 $false|~sQ47_spl|~sQ46_spl|sQ49_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f851,f656])).
% 21.24/3.91 fof(f853,plain,(
% 21.24/3.91 ~sQ47_spl|~sQ46_spl|sQ49_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f852])).
% 21.24/3.91 fof(f854,plain,(
% 21.24/3.91 greater(sk1(sk3),sk2(sk3))|~sQ14_spl|~sQ43_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f145,f504])).
% 21.24/3.91 fof(f859,plain,(
% 21.24/3.91 ~greater(sk1(sk3),sk1(sk3))|~sQ14_spl|sQ13_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f145,f143])).
% 21.24/3.91 fof(f860,plain,(
% 21.24/3.91 ~greater(growth_rate(first_movers,sk1(sk3)),zero)|~sQ14_spl|sQ23_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f145,f200])).
% 21.24/3.91 fof(f863,plain,(
% 21.24/3.91 ~greater(zero,growth_rate(efficient_producers,sk1(sk3)))|~sQ14_spl|sQ20_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f145,f189])).
% 21.24/3.91 fof(f864,plain,(
% 21.24/3.91 greater_or_equal(growth_rate(efficient_producers,sk1(sk3)),zero)|~sQ14_spl|~sQ29_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f145,f225])).
% 21.24/3.91 fof(f867,plain,(
% 21.24/3.91 ~growth_rate(efficient_producers,sk1(sk3))=zero|~sQ14_spl|sQ19_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f145,f186])).
% 21.24/3.91 fof(f873,plain,(
% 21.24/3.91 ~greater(sk1(sk3),equilibrium(sk3))|~sQ14_spl|sQ56_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f145,f701])).
% 21.24/3.91 fof(f874,plain,(
% 21.24/3.91 sQ8_spl|~sQ14_spl|~sQ43_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f854,f110,f144,f503])).
% 21.24/3.91 fof(f875,plain,(
% 21.24/3.91 $false|~sQ11_spl|~sQ14_spl|sQ13_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f859,f124])).
% 21.24/3.91 fof(f876,plain,(
% 21.24/3.91 ~sQ11_spl|~sQ14_spl|sQ13_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f875])).
% 21.24/3.91 fof(f883,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk1(sk3),equilibrium(sk3))|growth_rate(efficient_producers,sk1(sk3))=zero|greater(zero,growth_rate(efficient_producers,sk1(sk3)))|greater(zero,growth_rate(first_movers,sk1(sk3)))|~sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f150,f54])).
% 21.24/3.91 fof(f884,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk1(sk3),equilibrium(sk3))|growth_rate(efficient_producers,sk1(sk3))=zero|greater(zero,growth_rate(efficient_producers,sk1(sk3)))|greater(growth_rate(efficient_producers,sk1(sk3)),zero)|~sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f150,f52])).
% 21.24/3.91 fof(f885,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk1(sk3),equilibrium(sk3))|growth_rate(efficient_producers,sk1(sk3))=zero|greater(growth_rate(first_movers,sk1(sk3)),zero)|greater(zero,growth_rate(first_movers,sk1(sk3)))|~sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f150,f50])).
% 21.24/3.91 fof(f886,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(sk1(sk3),equilibrium(sk3))|growth_rate(efficient_producers,sk1(sk3))=zero|greater(growth_rate(first_movers,sk1(sk3)),zero)|greater(growth_rate(efficient_producers,sk1(sk3)),zero)|~sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f150,f48])).
% 21.24/3.91 fof(f891,plain,(
% 21.24/3.91 ~environment(sk3)|~stable(sk3)|~greater_or_equal(sk1(sk3),sk1(sk3))|greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))|~sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f150,f57])).
% 21.24/3.91 fof(f894,plain,(
% 21.24/3.91 ~environment(sk3)|~greater_or_equal(growth_rate(efficient_producers,sk1(sk3)),zero)|~greater(zero,growth_rate(first_movers,sk1(sk3)))|outcompetes(efficient_producers,first_movers,sk1(sk3))|~sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f150,f34])).
% 21.24/3.91 fof(f895,definition,(
% 21.24/3.91 sQ59_spl <=> (greater_or_equal(sk1(sk3),equilibrium(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f897,plain,(
% 21.24/3.91 ~greater_or_equal(sk1(sk3),equilibrium(sk3))|sQ59_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f895])).
% 21.24/3.91 fof(f898,definition,(
% 21.24/3.91 sQ60_spl <=> (growth_rate(efficient_producers,sk1(sk3))=zero)),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f899,plain,(
% 21.24/3.91 growth_rate(efficient_producers,sk1(sk3))=zero|~sQ60_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f898])).
% 21.24/3.91 fof(f901,definition,(
% 21.24/3.91 sQ61_spl <=> (greater(zero,growth_rate(efficient_producers,sk1(sk3))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f902,plain,(
% 21.24/3.91 greater(zero,growth_rate(efficient_producers,sk1(sk3)))|~sQ61_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f901])).
% 21.24/3.91 fof(f904,definition,(
% 21.24/3.91 sQ62_spl <=> (greater(zero,growth_rate(first_movers,sk1(sk3))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f905,plain,(
% 21.24/3.91 greater(zero,growth_rate(first_movers,sk1(sk3)))|~sQ62_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f904])).
% 21.24/3.91 fof(f906,plain,(
% 21.24/3.91 ~greater(zero,growth_rate(first_movers,sk1(sk3)))|sQ62_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f904])).
% 21.24/3.91 fof(f907,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ59_spl|sQ60_spl|sQ61_spl|sQ62_spl|~sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f883,f67,f895,f898,f901,f904,f144,f70])).
% 21.24/3.91 fof(f908,definition,(
% 21.24/3.91 sQ63_spl <=> (greater(growth_rate(efficient_producers,sk1(sk3)),zero))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f909,plain,(
% 21.24/3.91 greater(growth_rate(efficient_producers,sk1(sk3)),zero)|~sQ63_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f908])).
% 21.24/3.91 fof(f911,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ59_spl|sQ60_spl|sQ61_spl|sQ63_spl|~sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f884,f67,f895,f898,f901,f908,f144,f70])).
% 21.24/3.91 fof(f912,definition,(
% 21.24/3.91 sQ64_spl <=> (greater(growth_rate(first_movers,sk1(sk3)),zero))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f913,plain,(
% 21.24/3.91 greater(growth_rate(first_movers,sk1(sk3)),zero)|~sQ64_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f912])).
% 21.24/3.91 fof(f915,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ59_spl|sQ60_spl|sQ64_spl|sQ62_spl|~sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f885,f67,f895,f898,f912,f904,f144,f70])).
% 21.24/3.91 fof(f916,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ59_spl|sQ60_spl|sQ64_spl|sQ63_spl|~sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f886,f67,f895,f898,f912,f908,f144,f70])).
% 21.24/3.91 fof(f917,definition,(
% 21.24/3.91 sQ65_spl <=> (growth_rate(first_movers,sk1(sk3))=zero)),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f918,plain,(
% 21.24/3.91 growth_rate(first_movers,sk1(sk3))=zero|~sQ65_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f917])).
% 21.24/3.91 fof(f924,definition,(
% 21.24/3.91 sQ66_spl <=> (greater_or_equal(sk1(sk3),sk1(sk3)))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f926,plain,(
% 21.24/3.91 ~greater_or_equal(sk1(sk3),sk1(sk3))|sQ66_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f924])).
% 21.24/3.91 fof(f927,definition,(
% 21.24/3.91 sQ67_spl <=> (greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3))))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f928,plain,(
% 21.24/3.91 greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))|~sQ67_spl),
% 21.24/3.91 inference(component_clause,[status(thm)],[f927])).
% 21.24/3.91 fof(f930,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ25_spl|~sQ66_spl|sQ67_spl|~sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f891,f67,f210,f924,f927,f144,f70])).
% 21.24/3.91 fof(f932,definition,(
% 21.24/3.91 sQ68_spl <=> (greater_or_equal(growth_rate(efficient_producers,sk1(sk3)),zero))),
% 21.24/3.91 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 21.24/3.91 fof(f936,plain,(
% 21.24/3.91 ~sQ0_spl|~sQ68_spl|~sQ62_spl|sQ15_spl|~sQ14_spl|~sQ1_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f894,f67,f932,f904,f152,f144,f70])).
% 21.24/3.91 fof(f937,plain,(
% 21.24/3.91 $false|~sQ14_spl|sQ23_spl|~sQ64_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f913,f860])).
% 21.24/3.91 fof(f938,plain,(
% 21.24/3.91 ~sQ14_spl|sQ23_spl|~sQ64_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f937])).
% 21.24/3.91 fof(f943,plain,(
% 21.24/3.91 $false|~sQ14_spl|sQ20_spl|~sQ61_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f902,f863])).
% 21.24/3.91 fof(f944,plain,(
% 21.24/3.91 ~sQ14_spl|sQ20_spl|~sQ61_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f943])).
% 21.24/3.91 fof(f945,plain,(
% 21.24/3.91 $false|~sQ14_spl|sQ19_spl|~sQ60_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f899,f867])).
% 21.24/3.91 fof(f946,plain,(
% 21.24/3.91 ~sQ14_spl|sQ19_spl|~sQ60_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f945])).
% 21.24/3.91 fof(f947,plain,(
% 21.24/3.91 $false|sQ66_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f926,f65])).
% 21.24/3.91 fof(f948,plain,(
% 21.24/3.91 sQ66_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f947])).
% 21.24/3.91 fof(f949,plain,(
% 21.24/3.91 greater(growth_rate(efficient_producers,sk1(sk3)),zero)|~sQ65_spl|~sQ67_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f918,f928])).
% 21.24/3.91 fof(f950,plain,(
% 21.24/3.91 ~greater(zero,zero)|~sQ65_spl|sQ62_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f918,f906])).
% 21.24/3.91 fof(f951,plain,(
% 21.24/3.91 greater(zero,zero)|~sQ65_spl|~sQ64_spl),
% 21.24/3.91 inference(forward_demodulation,[status(thm)],[f918,f913])).
% 21.24/3.91 fof(f952,plain,(
% 21.24/3.91 $false|sQ62_spl|~sQ65_spl|~sQ64_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f951,f950])).
% 21.24/3.91 fof(f953,plain,(
% 21.24/3.91 sQ62_spl|~sQ65_spl|~sQ64_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f952])).
% 21.24/3.91 fof(f967,plain,(
% 21.24/3.91 greater(growth_rate(efficient_producers,sk1(sk3)),zero)|growth_rate(efficient_producers,sk1(sk3))=zero|~sQ14_spl|~sQ29_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f864,f30])).
% 21.24/3.91 fof(f968,plain,(
% 21.24/3.91 sQ63_spl|sQ60_spl|~sQ14_spl|~sQ29_spl),
% 21.24/3.91 inference(split_clause,[status(thm)],[f967,f908,f898,f144,f224])).
% 21.24/3.91 fof(f996,plain,(
% 21.24/3.91 greater_or_equal(sk4(sk2(sk3)),sk1(sk3))|~sQ16_spl|~sQ10_spl),
% 21.24/3.91 inference(resolution,[status(thm)],[f804,f31])).
% 21.24/3.91 fof(f997,plain,(
% 21.24/3.91 $false|sQ52_spl|~sQ16_spl|~sQ10_spl),
% 21.24/3.91 inference(forward_subsumption_resolution,[status(thm)],[f996,f641])).
% 21.24/3.91 fof(f998,plain,(
% 21.24/3.91 sQ52_spl|~sQ16_spl|~sQ10_spl),
% 21.24/3.91 inference(contradiction_clause,[status(thm)],[f997])).
% 21.24/3.91 fof(f1000,plain,(
% 21.24/3.91 greater(zero,zero)|~sQ60_spl|~sQ65_spl|~sQ67_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f899,f949])).
% 21.24/3.91 fof(f1008,plain,(
% 21.24/3.91 greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~sQ9_spl|~sQ49_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f114,f800])).
% 21.24/3.91 fof(f1014,plain,(
% 21.24/3.91 ~greater(sk1(sk3),sk1(sk3))|~sQ9_spl|sQ8_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f114,f112])).
% 21.24/3.91 fof(f1022,plain,(
% 21.24/3.91 greater(zero,growth_rate(first_movers,sk1(sk3)))|~sQ9_spl|~sQ32_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f114,f259])).
% 21.24/3.91 fof(f1028,plain,(
% 21.24/3.91 ~sk4(sk2(sk3))=sk1(sk3)|~sQ9_spl|sQ17_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f114,f162])).
% 21.24/3.91 fof(f1029,plain,(
% 21.24/3.91 greater(sk2(sk3),sk1(sk3))|~sQ9_spl|~sQ6_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f114,f104])).
% 21.24/3.91 fof(f1032,plain,(
% 21.24/3.91 greater(sk1(sk3),equilibrium(sk3))|~sQ9_spl|~sQ4_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f114,f93])).
% 21.24/3.91 fof(f1034,plain,(
% 21.24/3.91 greater_or_equal(sk1(sk3),equilibrium(sk3))|~sQ9_spl|~sQ3_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f114,f85])).
% 21.24/3.91 fof(f1039,plain,(
% 21.24/3.91 ~sk4(sk1(sk3))=sk1(sk3)|~sQ9_spl|sQ44_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f114,f508])).
% 21.24/3.91 fof(f1046,plain,(
% 21.24/3.91 greater(sk4(sk1(sk3)),equilibrium(sk3))|~sQ9_spl|~sQ16_spl|~sQ4_spl),
% 21.24/3.91 inference(backward_demodulation,[status(thm)],[f114,f806])).
% 21.24/3.92 fof(f1054,plain,(
% 21.24/3.92 ~greater_or_equal(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~sQ9_spl|sQ55_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f114,f652])).
% 21.24/3.92 fof(f1055,plain,(
% 21.24/3.92 $false|~sQ29_spl|~sQ9_spl|sQ55_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1054,f225])).
% 21.24/3.92 fof(f1056,plain,(
% 21.24/3.92 ~sQ29_spl|~sQ9_spl|sQ55_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1055])).
% 21.24/3.92 fof(f1058,plain,(
% 21.24/3.92 sQ29_spl|~sQ9_spl|~sQ49_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1008,f224,f113,f623])).
% 21.24/3.92 fof(f1061,plain,(
% 21.24/3.92 sQ62_spl|~sQ9_spl|~sQ32_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1022,f904,f113,f258])).
% 21.24/3.92 fof(f1064,plain,(
% 21.24/3.92 ~sk4(sk1(sk3))=sk1(sk3)|~sQ9_spl|sQ17_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f114,f1028])).
% 21.24/3.92 fof(f1065,plain,(
% 21.24/3.92 greater(sk1(sk3),sk1(sk3))|~sQ9_spl|~sQ6_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f114,f1029])).
% 21.24/3.92 fof(f1066,plain,(
% 21.24/3.92 $false|sQ8_spl|~sQ9_spl|~sQ6_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1065,f1014])).
% 21.24/3.92 fof(f1067,plain,(
% 21.24/3.92 sQ8_spl|~sQ9_spl|~sQ6_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1066])).
% 21.24/3.92 fof(f1068,plain,(
% 21.24/3.92 $false|sQ59_spl|~sQ9_spl|~sQ3_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1034,f897])).
% 21.24/3.92 fof(f1069,plain,(
% 21.24/3.92 sQ59_spl|~sQ9_spl|~sQ3_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1068])).
% 21.24/3.92 fof(f1072,plain,(
% 21.24/3.92 ~sQ14_spl|~sQ9_spl|sQ44_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1039,f144,f113,f506])).
% 21.24/3.92 fof(f1073,plain,(
% 21.24/3.92 sQ56_spl|~sQ9_spl|~sQ16_spl|~sQ4_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1046,f699,f113,f157,f92])).
% 21.24/3.92 fof(f1074,plain,(
% 21.24/3.92 $false|~sQ9_spl|sQ17_spl|~sQ14_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f145,f1064])).
% 21.24/3.92 fof(f1075,plain,(
% 21.24/3.92 ~sQ9_spl|sQ17_spl|~sQ14_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1074])).
% 21.24/3.92 fof(f1076,plain,(
% 21.24/3.92 ~sQ40_spl|~sQ14_spl|sQ56_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f873,f328,f144,f699])).
% 21.24/3.92 fof(f1077,plain,(
% 21.24/3.92 sQ59_spl|~sQ40_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f478,f895,f328])).
% 21.24/3.92 fof(f1091,plain,(
% 21.24/3.92 sQ55_spl|~sQ49_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f800,f650,f623])).
% 21.24/3.92 fof(f1106,plain,(
% 21.24/3.92 ~greater_or_equal(sk2(sk3),equilibrium(sk3))|~sQ17_spl|sQ45_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f161,f612])).
% 21.24/3.92 fof(f1119,plain,(
% 21.24/3.92 sQ40_spl|~sQ9_spl|~sQ4_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1032,f328,f113,f92])).
% 21.24/3.92 fof(f1120,plain,(
% 21.24/3.92 ~greater(zero,growth_rate(first_movers,sk2(sk3)))|~sQ17_spl|sQ48_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f161,f621])).
% 21.24/3.92 fof(f1121,plain,(
% 21.24/3.92 ~greater(zero,growth_rate(first_movers,sk1(sk3)))|~sQ9_spl|~sQ17_spl|sQ48_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f114,f1120])).
% 21.24/3.92 fof(f1123,plain,(
% 21.24/3.92 $false|~sQ9_spl|~sQ17_spl|sQ48_spl|~sQ62_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f905,f1121])).
% 21.24/3.92 fof(f1124,plain,(
% 21.24/3.92 ~sQ9_spl|~sQ17_spl|sQ48_spl|~sQ62_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1123])).
% 21.24/3.92 fof(f1213,plain,(
% 21.24/3.92 greater(sk2(sk3),sk1(sk3))|sk2(sk3)=sk1(sk3)|~sQ36_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f279,f30])).
% 21.24/3.92 fof(f1214,plain,(
% 21.24/3.92 sQ10_spl|sQ9_spl|~sQ36_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1213,f116,f113,f278])).
% 21.24/3.92 fof(f1216,plain,(
% 21.24/3.92 sQ18_spl|~sQ41_spl|~sQ1_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f531,f181,f331,f70])).
% 21.24/3.92 fof(f1218,plain,(
% 21.24/3.92 greater(sk4(sk1(sk3)),equilibrium(sk3))|~sQ41_spl|~sQ13_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f332,f142])).
% 21.24/3.92 fof(f1240,plain,(
% 21.24/3.92 greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|~sQ41_spl|~sQ16_spl|~sQ10_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f332,f996])).
% 21.24/3.92 fof(f1255,plain,(
% 21.24/3.92 sQ56_spl|~sQ41_spl|~sQ13_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1218,f699,f331,f141])).
% 21.24/3.92 fof(f1262,plain,(
% 21.24/3.92 $false|sQ45_spl|~sQ41_spl|~sQ16_spl|~sQ10_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1240,f612])).
% 21.24/3.92 fof(f1263,plain,(
% 21.24/3.92 sQ45_spl|~sQ41_spl|~sQ16_spl|~sQ10_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1262])).
% 21.24/3.92 fof(f1326,plain,(
% 21.24/3.92 greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|~sQ16_spl|~sQ4_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f806,f31])).
% 21.24/3.92 fof(f1327,plain,(
% 21.24/3.92 $false|sQ45_spl|~sQ16_spl|~sQ4_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1326,f612])).
% 21.24/3.92 fof(f1328,plain,(
% 21.24/3.92 sQ45_spl|~sQ16_spl|~sQ4_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1327])).
% 21.24/3.92 fof(f1331,plain,(
% 21.24/3.92 greater(sk4(sk2(sk3)),sk1(sk3))|sk4(sk2(sk3))=sk1(sk3)|~sQ16_spl|~sQ10_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f996,f30])).
% 21.24/3.92 fof(f1332,definition,(
% 21.24/3.92 sQ69_spl <=> (greater(sk4(sk2(sk3)),sk1(sk3)))),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1335,definition,(
% 21.24/3.92 sQ70_spl <=> (sk4(sk2(sk3))=sk1(sk3))),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1336,plain,(
% 21.24/3.92 sk4(sk2(sk3))=sk1(sk3)|~sQ70_spl),
% 21.24/3.92 inference(component_clause,[status(thm)],[f1335])).
% 21.24/3.92 fof(f1338,plain,(
% 21.24/3.92 sQ69_spl|sQ70_spl|~sQ16_spl|~sQ10_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1331,f1332,f1335,f157,f116])).
% 21.24/3.92 fof(f1340,plain,(
% 21.24/3.92 ~growth_rate(efficient_producers,sk1(sk3))=zero|~sQ70_spl|sQ46_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f1336,f615])).
% 21.24/3.92 fof(f1342,plain,(
% 21.24/3.92 greater(sk1(sk3),equilibrium(sk3))|~sQ70_spl|~sQ16_spl|~sQ4_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f1336,f806])).
% 21.24/3.92 fof(f1344,plain,(
% 21.24/3.92 ~greater(growth_rate(efficient_producers,sk1(sk3)),zero)|~sQ70_spl|sQ49_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f1336,f625])).
% 21.24/3.92 fof(f1346,plain,(
% 21.24/3.92 ~greater_or_equal(growth_rate(efficient_producers,sk1(sk3)),zero)|~sQ70_spl|sQ55_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f1336,f652])).
% 21.24/3.92 fof(f1366,plain,(
% 21.24/3.92 ~sQ60_spl|~sQ70_spl|sQ46_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1340,f898,f1335,f613])).
% 21.24/3.92 fof(f1368,plain,(
% 21.24/3.92 sQ40_spl|~sQ70_spl|~sQ16_spl|~sQ4_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1342,f328,f1335,f157,f92])).
% 21.24/3.92 fof(f1372,plain,(
% 21.24/3.92 ~greater(zero,zero)|~sQ60_spl|~sQ70_spl|sQ49_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f899,f1344])).
% 21.24/3.92 fof(f1373,plain,(
% 21.24/3.92 $false|~sQ65_spl|~sQ67_spl|~sQ60_spl|~sQ70_spl|sQ49_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1372,f1000])).
% 21.24/3.92 fof(f1374,plain,(
% 21.24/3.92 ~sQ65_spl|~sQ67_spl|~sQ60_spl|~sQ70_spl|sQ49_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1373])).
% 21.24/3.92 fof(f1415,plain,(
% 21.24/3.92 greater(sk4(sk2(sk3)),equilibrium(sk3))|sk4(sk2(sk3))=equilibrium(sk3)|~sQ16_spl|~sQ4_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f1326,f30])).
% 21.24/3.92 fof(f1416,definition,(
% 21.24/3.92 sQ71_spl <=> (greater(sk4(sk2(sk3)),equilibrium(sk3)))),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1419,definition,(
% 21.24/3.92 sQ72_spl <=> (sk4(sk2(sk3))=equilibrium(sk3))),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1420,plain,(
% 21.24/3.92 sk4(sk2(sk3))=equilibrium(sk3)|~sQ72_spl),
% 21.24/3.92 inference(component_clause,[status(thm)],[f1419])).
% 21.24/3.92 fof(f1421,plain,(
% 21.24/3.92 ~sk4(sk2(sk3))=equilibrium(sk3)|sQ72_spl),
% 21.24/3.92 inference(component_clause,[status(thm)],[f1419])).
% 21.24/3.92 fof(f1422,plain,(
% 21.24/3.92 sQ71_spl|sQ72_spl|~sQ16_spl|~sQ4_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1415,f1416,f1419,f157,f92])).
% 21.24/3.92 fof(f1430,plain,(
% 21.24/3.92 ~greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)|~sQ72_spl|sQ49_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f1420,f625])).
% 21.24/3.92 fof(f1432,plain,(
% 21.24/3.92 greater_or_equal(equilibrium(sk3),sk1(sk3))|~sQ72_spl|~sQ16_spl|~sQ10_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f1420,f996])).
% 21.24/3.92 fof(f1435,plain,(
% 21.24/3.92 ~growth_rate(efficient_producers,equilibrium(sk3))=zero|~sQ72_spl|sQ46_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f1420,f615])).
% 21.24/3.92 fof(f1436,plain,(
% 21.24/3.92 subpopulations(first_movers,efficient_producers,sk3,equilibrium(sk3))|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f1420,f405])).
% 21.24/3.92 fof(f1454,plain,(
% 21.24/3.92 ~environment(sk3)|~greater_or_equal(equilibrium(sk3),equilibrium(sk3))|growth_rate(efficient_producers,equilibrium(sk3))=zero|greater(zero,growth_rate(efficient_producers,equilibrium(sk3)))|greater(zero,growth_rate(first_movers,equilibrium(sk3)))|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f1436,f54])).
% 21.24/3.92 fof(f1455,plain,(
% 21.24/3.92 ~environment(sk3)|~greater_or_equal(equilibrium(sk3),equilibrium(sk3))|growth_rate(efficient_producers,equilibrium(sk3))=zero|greater(zero,growth_rate(efficient_producers,equilibrium(sk3)))|greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f1436,f52])).
% 21.24/3.92 fof(f1456,plain,(
% 21.24/3.92 ~environment(sk3)|~greater_or_equal(equilibrium(sk3),equilibrium(sk3))|growth_rate(efficient_producers,equilibrium(sk3))=zero|greater(growth_rate(first_movers,equilibrium(sk3)),zero)|greater(zero,growth_rate(first_movers,equilibrium(sk3)))|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f1436,f50])).
% 21.24/3.92 fof(f1457,plain,(
% 21.24/3.92 ~environment(sk3)|~greater_or_equal(equilibrium(sk3),equilibrium(sk3))|growth_rate(efficient_producers,equilibrium(sk3))=zero|greater(growth_rate(first_movers,equilibrium(sk3)),zero)|greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f1436,f48])).
% 21.24/3.92 fof(f1458,plain,(
% 21.24/3.92 ~environment(sk3)|~greater_or_equal(equilibrium(sk3),equilibrium(sk3))|growth_rate(first_movers,equilibrium(sk3))=zero|greater(zero,growth_rate(efficient_producers,equilibrium(sk3)))|greater(zero,growth_rate(first_movers,equilibrium(sk3)))|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f1436,f46])).
% 21.24/3.92 fof(f1459,plain,(
% 21.24/3.92 ~environment(sk3)|~greater_or_equal(equilibrium(sk3),equilibrium(sk3))|growth_rate(first_movers,equilibrium(sk3))=zero|greater(zero,growth_rate(efficient_producers,equilibrium(sk3)))|greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f1436,f44])).
% 21.24/3.92 fof(f1460,plain,(
% 21.24/3.92 ~environment(sk3)|~greater_or_equal(equilibrium(sk3),equilibrium(sk3))|growth_rate(first_movers,equilibrium(sk3))=zero|greater(growth_rate(first_movers,equilibrium(sk3)),zero)|greater(zero,growth_rate(first_movers,equilibrium(sk3)))|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f1436,f42])).
% 21.24/3.92 fof(f1461,plain,(
% 21.24/3.92 ~environment(sk3)|~greater_or_equal(equilibrium(sk3),equilibrium(sk3))|growth_rate(first_movers,equilibrium(sk3))=zero|greater(growth_rate(first_movers,equilibrium(sk3)),zero)|greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f1436,f40])).
% 21.24/3.92 fof(f1462,plain,(
% 21.24/3.92 ~environment(sk3)|~stable(sk3)|~greater_or_equal(equilibrium(sk3),sk1(sk3))|greater(growth_rate(efficient_producers,equilibrium(sk3)),growth_rate(first_movers,equilibrium(sk3)))|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f1436,f57])).
% 21.24/3.92 fof(f1463,plain,(
% 21.24/3.92 ~environment(sk3)|~outcompetes(efficient_producers,first_movers,equilibrium(sk3))|greater(zero,growth_rate(first_movers,equilibrium(sk3)))|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f1436,f38])).
% 21.24/3.92 fof(f1464,plain,(
% 21.24/3.92 ~environment(sk3)|~outcompetes(efficient_producers,first_movers,equilibrium(sk3))|greater_or_equal(growth_rate(efficient_producers,equilibrium(sk3)),zero)|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f1436,f36])).
% 21.24/3.92 fof(f1465,plain,(
% 21.24/3.92 ~environment(sk3)|~greater_or_equal(growth_rate(efficient_producers,equilibrium(sk3)),zero)|~greater(zero,growth_rate(first_movers,equilibrium(sk3)))|outcompetes(efficient_producers,first_movers,equilibrium(sk3))|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f1436,f34])).
% 21.24/3.92 fof(f1466,definition,(
% 21.24/3.92 sQ73_spl <=> (greater_or_equal(equilibrium(sk3),equilibrium(sk3)))),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1468,plain,(
% 21.24/3.92 ~greater_or_equal(equilibrium(sk3),equilibrium(sk3))|sQ73_spl),
% 21.24/3.92 inference(component_clause,[status(thm)],[f1466])).
% 21.24/3.92 fof(f1469,definition,(
% 21.24/3.92 sQ74_spl <=> (growth_rate(efficient_producers,equilibrium(sk3))=zero)),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1470,plain,(
% 21.24/3.92 growth_rate(efficient_producers,equilibrium(sk3))=zero|~sQ74_spl),
% 21.24/3.92 inference(component_clause,[status(thm)],[f1469])).
% 21.24/3.92 fof(f1472,definition,(
% 21.24/3.92 sQ75_spl <=> (greater(zero,growth_rate(efficient_producers,equilibrium(sk3))))),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1475,definition,(
% 21.24/3.92 sQ76_spl <=> (greater(zero,growth_rate(first_movers,equilibrium(sk3))))),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1478,plain,(
% 21.24/3.92 ~sQ0_spl|~sQ73_spl|sQ74_spl|sQ75_spl|sQ76_spl|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1454,f67,f1466,f1469,f1472,f1475,f1419,f79])).
% 21.24/3.92 fof(f1479,definition,(
% 21.24/3.92 sQ77_spl <=> (greater(growth_rate(efficient_producers,equilibrium(sk3)),zero))),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1480,plain,(
% 21.24/3.92 greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)|~sQ77_spl),
% 21.24/3.92 inference(component_clause,[status(thm)],[f1479])).
% 21.24/3.92 fof(f1482,plain,(
% 21.24/3.92 ~sQ0_spl|~sQ73_spl|sQ74_spl|sQ75_spl|sQ77_spl|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1455,f67,f1466,f1469,f1472,f1479,f1419,f79])).
% 21.24/3.92 fof(f1483,definition,(
% 21.24/3.92 sQ78_spl <=> (greater(growth_rate(first_movers,equilibrium(sk3)),zero))),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1486,plain,(
% 21.24/3.92 ~sQ0_spl|~sQ73_spl|sQ74_spl|sQ78_spl|sQ76_spl|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1456,f67,f1466,f1469,f1483,f1475,f1419,f79])).
% 21.24/3.92 fof(f1487,plain,(
% 21.24/3.92 ~sQ0_spl|~sQ73_spl|sQ74_spl|sQ78_spl|sQ77_spl|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1457,f67,f1466,f1469,f1483,f1479,f1419,f79])).
% 21.24/3.92 fof(f1488,definition,(
% 21.24/3.92 sQ79_spl <=> (growth_rate(first_movers,equilibrium(sk3))=zero)),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1489,plain,(
% 21.24/3.92 growth_rate(first_movers,equilibrium(sk3))=zero|~sQ79_spl),
% 21.24/3.92 inference(component_clause,[status(thm)],[f1488])).
% 21.24/3.92 fof(f1491,plain,(
% 21.24/3.92 ~sQ0_spl|~sQ73_spl|sQ79_spl|sQ75_spl|sQ76_spl|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1458,f67,f1466,f1488,f1472,f1475,f1419,f79])).
% 21.24/3.92 fof(f1492,plain,(
% 21.24/3.92 ~sQ0_spl|~sQ73_spl|sQ79_spl|sQ75_spl|sQ77_spl|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1459,f67,f1466,f1488,f1472,f1479,f1419,f79])).
% 21.24/3.92 fof(f1493,plain,(
% 21.24/3.92 ~sQ0_spl|~sQ73_spl|sQ79_spl|sQ78_spl|sQ76_spl|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1460,f67,f1466,f1488,f1483,f1475,f1419,f79])).
% 21.24/3.92 fof(f1494,plain,(
% 21.24/3.92 ~sQ0_spl|~sQ73_spl|sQ79_spl|sQ78_spl|sQ77_spl|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1461,f67,f1466,f1488,f1483,f1479,f1419,f79])).
% 21.24/3.92 fof(f1495,definition,(
% 21.24/3.92 sQ80_spl <=> (greater_or_equal(equilibrium(sk3),sk1(sk3)))),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1497,plain,(
% 21.24/3.92 ~greater_or_equal(equilibrium(sk3),sk1(sk3))|sQ80_spl),
% 21.24/3.92 inference(component_clause,[status(thm)],[f1495])).
% 21.24/3.92 fof(f1498,definition,(
% 21.24/3.92 sQ81_spl <=> (greater(growth_rate(efficient_producers,equilibrium(sk3)),growth_rate(first_movers,equilibrium(sk3))))),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1499,plain,(
% 21.24/3.92 greater(growth_rate(efficient_producers,equilibrium(sk3)),growth_rate(first_movers,equilibrium(sk3)))|~sQ81_spl),
% 21.24/3.92 inference(component_clause,[status(thm)],[f1498])).
% 21.24/3.92 fof(f1501,plain,(
% 21.24/3.92 ~sQ0_spl|~sQ25_spl|~sQ80_spl|sQ81_spl|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1462,f67,f210,f1495,f1498,f1419,f79])).
% 21.24/3.92 fof(f1502,plain,(
% 21.24/3.92 ~sQ0_spl|~sQ58_spl|sQ76_spl|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1463,f67,f727,f1475,f1419,f79])).
% 21.24/3.92 fof(f1503,definition,(
% 21.24/3.92 sQ82_spl <=> (greater_or_equal(growth_rate(efficient_producers,equilibrium(sk3)),zero))),
% 21.24/3.92 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 21.24/3.92 fof(f1506,plain,(
% 21.24/3.92 ~sQ0_spl|~sQ58_spl|sQ82_spl|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1464,f67,f727,f1503,f1419,f79])).
% 21.24/3.92 fof(f1507,plain,(
% 21.24/3.92 ~sQ0_spl|~sQ82_spl|~sQ76_spl|sQ58_spl|~sQ72_spl|~sQ2_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1465,f67,f1503,f1475,f727,f1419,f79])).
% 21.24/3.92 fof(f1508,plain,(
% 21.24/3.92 $false|sQ73_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1468,f65])).
% 21.24/3.92 fof(f1509,plain,(
% 21.24/3.92 sQ73_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1508])).
% 21.24/3.92 fof(f1510,plain,(
% 21.24/3.92 $false|~sQ72_spl|sQ49_spl|~sQ77_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1480,f1430])).
% 21.24/3.92 fof(f1511,plain,(
% 21.24/3.92 ~sQ72_spl|sQ49_spl|~sQ77_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1510])).
% 21.24/3.92 fof(f1514,plain,(
% 21.24/3.92 greater(zero,growth_rate(first_movers,equilibrium(sk3)))|~sQ74_spl|~sQ81_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f1470,f1499])).
% 21.24/3.92 fof(f1515,plain,(
% 21.24/3.92 greater(zero,zero)|~sQ79_spl|~sQ74_spl|~sQ81_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f1489,f1514])).
% 21.24/3.92 fof(f1547,plain,(
% 21.24/3.92 greater_or_equal(growth_rate(efficient_producers,sk1(sk3)),zero)|~sQ63_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f909,f31])).
% 21.24/3.92 fof(f1575,plain,(
% 21.24/3.92 greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|~sQ53_spl|~sQ50_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f801,f628])).
% 21.24/3.92 fof(f1576,plain,(
% 21.24/3.92 sQ49_spl|~sQ53_spl|~sQ50_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1575,f623,f642,f627])).
% 21.24/3.92 fof(f1579,plain,(
% 21.24/3.92 ~greater(zero,zero)|~sQ46_spl|sQ49_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f614,f625])).
% 21.24/3.92 fof(f1583,plain,(
% 21.24/3.92 $false|~sQ79_spl|~sQ74_spl|~sQ81_spl|~sQ46_spl|sQ49_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f851,f1515])).
% 21.24/3.92 fof(f1584,plain,(
% 21.24/3.92 ~sQ79_spl|~sQ74_spl|~sQ81_spl|~sQ46_spl|sQ49_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1583])).
% 21.24/3.92 fof(f1591,plain,(
% 21.24/3.92 $false|~sQ51_spl|~sQ53_spl|~sQ46_spl|sQ49_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1579,f659])).
% 21.24/3.92 fof(f1592,plain,(
% 21.24/3.92 ~sQ51_spl|~sQ53_spl|~sQ46_spl|sQ49_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1591])).
% 21.24/3.92 fof(f1607,plain,(
% 21.24/3.92 $false|sQ80_spl|~sQ72_spl|~sQ16_spl|~sQ10_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1432,f1497])).
% 21.24/3.92 fof(f1608,plain,(
% 21.24/3.92 sQ80_spl|~sQ72_spl|~sQ16_spl|~sQ10_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1607])).
% 21.24/3.92 fof(f1610,plain,(
% 21.24/3.92 ~zero=zero|~sQ74_spl|~sQ72_spl|sQ46_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f1470,f1435])).
% 21.24/3.92 fof(f1611,plain,(
% 21.24/3.92 $false|~sQ74_spl|~sQ72_spl|sQ46_spl),
% 21.24/3.92 inference(trivial_equality_resolution,[status(thm)],[f1610])).
% 21.24/3.92 fof(f1612,plain,(
% 21.24/3.92 ~sQ74_spl|~sQ72_spl|sQ46_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1611])).
% 21.24/3.92 fof(f1657,plain,(
% 21.24/3.92 greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|growth_rate(efficient_producers,sk4(sk2(sk3)))=zero|~sQ55_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f651,f30])).
% 21.24/3.92 fof(f1658,plain,(
% 21.24/3.92 sQ49_spl|sQ46_spl|~sQ55_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1657,f623,f613,f650])).
% 21.24/3.92 fof(f1683,plain,(
% 21.24/3.92 greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ47_spl|~sQ53_spl),
% 21.24/3.92 inference(resolution,[status(thm)],[f797,f643])).
% 21.24/3.92 fof(f1685,plain,(
% 21.24/3.92 sQ48_spl|~sQ47_spl|~sQ53_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1683,f619,f616,f642])).
% 21.24/3.92 fof(f1686,plain,(
% 21.24/3.92 $false|~sQ3_spl|~sQ17_spl|sQ45_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1106,f85])).
% 21.24/3.92 fof(f1687,plain,(
% 21.24/3.92 ~sQ3_spl|~sQ17_spl|sQ45_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1686])).
% 21.24/3.92 fof(f1691,plain,(
% 21.24/3.92 ~sk2(sk3)=equilibrium(sk3)|~sQ17_spl|sQ72_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f161,f1421])).
% 21.24/3.92 fof(f1696,plain,(
% 21.24/3.92 ~greater(growth_rate(first_movers,sk2(sk3)),zero)|~sQ17_spl|sQ50_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f161,f629])).
% 21.24/3.92 fof(f1697,plain,(
% 21.24/3.92 $false|~sQ34_spl|~sQ17_spl|sQ50_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1696,f267])).
% 21.24/3.92 fof(f1698,plain,(
% 21.24/3.92 ~sQ34_spl|~sQ17_spl|sQ50_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1697])).
% 21.24/3.92 fof(f1699,plain,(
% 21.24/3.92 ~greater(zero,growth_rate(efficient_producers,sk2(sk3)))|~sQ17_spl|sQ47_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f161,f618])).
% 21.24/3.92 fof(f1700,plain,(
% 21.24/3.92 $false|~sQ31_spl|~sQ17_spl|sQ47_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1699,f256])).
% 21.24/3.92 fof(f1701,plain,(
% 21.24/3.92 ~sQ31_spl|~sQ17_spl|sQ47_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1700])).
% 21.24/3.92 fof(f1703,plain,(
% 21.24/3.92 ~greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk4(sk2(sk3))))|~sQ17_spl|sQ53_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f161,f644])).
% 21.24/3.92 fof(f1704,plain,(
% 21.24/3.92 ~greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))|~sQ17_spl|sQ53_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f161,f1703])).
% 21.24/3.92 fof(f1705,plain,(
% 21.24/3.92 $false|~sQ37_spl|~sQ17_spl|sQ53_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1704,f282])).
% 21.24/3.92 fof(f1706,plain,(
% 21.24/3.92 ~sQ37_spl|~sQ17_spl|sQ53_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1705])).
% 21.24/3.92 fof(f1707,plain,(
% 21.24/3.92 $false|~sQ63_spl|~sQ70_spl|sQ55_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1346,f1547])).
% 21.24/3.92 fof(f1708,plain,(
% 21.24/3.92 ~sQ63_spl|~sQ70_spl|sQ55_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1707])).
% 21.24/3.92 fof(f1737,plain,(
% 21.24/3.92 greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|~sQ5_spl|~sQ2_spl),
% 21.24/3.92 inference(backward_demodulation,[status(thm)],[f96,f404])).
% 21.24/3.92 fof(f1748,plain,(
% 21.24/3.92 greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|~sQ5_spl|~sQ43_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f96,f782])).
% 21.24/3.92 fof(f1749,plain,(
% 21.24/3.92 $false|sQ18_spl|~sQ5_spl|~sQ43_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1748,f183])).
% 21.24/3.92 fof(f1750,plain,(
% 21.24/3.92 sQ18_spl|~sQ5_spl|~sQ43_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1749])).
% 21.24/3.92 fof(f1763,plain,(
% 21.24/3.92 sQ45_spl|~sQ5_spl|~sQ2_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f1737,f610,f95,f79])).
% 21.24/3.92 fof(f1801,plain,(
% 21.24/3.92 ~equilibrium(sk3)=equilibrium(sk3)|~sQ5_spl|~sQ17_spl|sQ72_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f96,f1691])).
% 21.24/3.92 fof(f1802,plain,(
% 21.24/3.92 $false|~sQ5_spl|~sQ17_spl|sQ72_spl),
% 21.24/3.92 inference(trivial_equality_resolution,[status(thm)],[f1801])).
% 21.24/3.92 fof(f1803,plain,(
% 21.24/3.92 ~sQ5_spl|~sQ17_spl|sQ72_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1802])).
% 21.24/3.92 fof(f1816,plain,(
% 21.24/3.92 ~sQ58_spl|~sQ5_spl|sQ38_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f351,f727,f95,f285])).
% 21.24/3.92 fof(f1840,plain,(
% 21.24/3.92 sQ74_spl|~sQ5_spl|~sQ30_spl),
% 21.24/3.92 inference(split_clause,[status(thm)],[f374,f1469,f95,f252])).
% 21.24/3.92 fof(f1853,plain,(
% 21.24/3.92 greater(sk1(sk3),equilibrium(sk3))|~sQ5_spl|~sQ8_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f96,f111])).
% 21.24/3.92 fof(f1854,plain,(
% 21.24/3.92 $false|sQ40_spl|~sQ5_spl|~sQ8_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1853,f330])).
% 21.24/3.92 fof(f1855,plain,(
% 21.24/3.92 sQ40_spl|~sQ5_spl|~sQ8_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1854])).
% 21.24/3.92 fof(f1864,plain,(
% 21.24/3.92 sk1(sk3)=equilibrium(sk3)|~sQ5_spl|~sQ9_spl),
% 21.24/3.92 inference(forward_demodulation,[status(thm)],[f96,f114])).
% 21.24/3.92 fof(f1865,plain,(
% 21.24/3.92 $false|sQ41_spl|~sQ5_spl|~sQ9_spl),
% 21.24/3.92 inference(forward_subsumption_resolution,[status(thm)],[f1864,f333])).
% 21.24/3.92 fof(f1866,plain,(
% 21.24/3.92 sQ41_spl|~sQ5_spl|~sQ9_spl),
% 21.24/3.92 inference(contradiction_clause,[status(thm)],[f1865])).
% 21.24/3.92 fof(f1867,plain,(
% 21.24/3.92 $false),
% 21.24/3.92 inference(sat_refutation,[status(thm)],[f73,f75,f82,f87,f98,f109,f119,f129,f147,f155,f163,f193,f202,f207,f219,f228,f235,f237,f261,f265,f269,f270,f274,f275,f276,f277,f284,f293,f298,f302,f305,f308,f334,f340,f342,f388,f509,f513,f550,f569,f579,f622,f626,f630,f631,f635,f636,f637,f645,f654,f705,f730,f759,f762,f764,f766,f768,f818,f833,f837,f838,f839,f842,f850,f853,f874,f876,f907,f911,f915,f916,f930,f936,f938,f944,f946,f948,f953,f968,f998,f1056,f1058,f1061,f1067,f1069,f1072,f1073,f1075,f1076,f1077,f1091,f1119,f1124,f1214,f1216,f1255,f1263,f1328,f1338,f1366,f1368,f1374,f1422,f1478,f1482,f1486,f1487,f1491,f1492,f1493,f1494,f1501,f1502,f1506,f1507,f1509,f1511,f1576,f1584,f1592,f1608,f1612,f1658,f1685,f1687,f1698,f1701,f1706,f1708,f1750,f1763,f1803,f1816,f1840,f1855,f1866])).
% 21.24/3.92 % SZS output end CNFRefutation for theBenchmark.p
% 21.24/3.92 % Elapsed time: 3.624201 seconds
% 21.24/3.92 % CPU time: 28.628435 seconds
% 21.24/3.92 % Total memory used: 175.978 MB
% 21.24/3.92 % Net memory used: 162.586 MB
%------------------------------------------------------------------------------