%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT029-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:25:44 PM UTC 2026
% Result : Unsatisfiable 0.11s 0.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT029-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n003.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 01:23:46 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 0.11/0.70 % Refutation found
% 0.11/0.70 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.11/0.70 % SZS output start CNFRefutation for theBenchmark
% 0.11/0.70 fof(f1,axiom,(
% 0.11/0.70 (![A,B,C]: (( ~ greater(A,B)| ~ greater(B,C)| greater(A,C) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f2,axiom,(
% 0.11/0.70 (![A,B,C]: (( ~ in_environment(A,B)| ~ in_environment(A,C)| greater(C,B)| C = B| greater(B,C) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f3,axiom,(
% 0.11/0.70 (![A,B]: (( ~ greater_or_equal(A,B)| greater(A,B)| A = B ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f4,axiom,(
% 0.11/0.70 (![A,B]: (( ~ greater(A,B)| greater_or_equal(A,B) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f5,axiom,(
% 0.11/0.70 (![A,B]: (( A != B| greater_or_equal(A,B) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f6,hypothesis,(
% 0.11/0.70 (![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) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f7,hypothesis,(
% 0.11/0.70 (![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)) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f8,hypothesis,(
% 0.11/0.70 (![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) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f9,hypothesis,(
% 0.11/0.70 (![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)) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f10,hypothesis,(
% 0.11/0.70 (![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) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f11,hypothesis,(
% 0.11/0.70 (![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)) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f12,hypothesis,(
% 0.11/0.70 (![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) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f13,hypothesis,(
% 0.11/0.70 (![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)) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f14,hypothesis,(
% 0.11/0.70 (![A]: (( ~ environment(A)| ~ stable(A)| in_environment(A,sk1(A)) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f15,hypothesis,(
% 0.11/0.70 (![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)) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f16,hypothesis,(
% 0.11/0.70 (![A]: (( ~ environment(A)| ~ stable(A)| in_environment(A,sk2(A)) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f17,hypothesis,(
% 0.11/0.70 (![A]: (( ~ environment(A)| ~ stable(A)| greater_or_equal(sk2(A),equilibrium(A)) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f18,negated_conjecture,(
% 0.11/0.70 environment(sk3) ),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f19,negated_conjecture,(
% 0.11/0.70 stable(sk3) ),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f20,negated_conjecture,(
% 0.11/0.70 (![A]: (( ~ in_environment(sk3,A)| subpopulations(first_movers,efficient_producers,sk3,sk4(A)) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f21,negated_conjecture,(
% 0.11/0.70 (![A]: (( ~ in_environment(sk3,A)| greater_or_equal(sk4(A),A) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f22,negated_conjecture,(
% 0.11/0.70 (![A]: (( ~ in_environment(sk3,A)| ~ greater(growth_rate(efficient_producers,sk4(A)),zero)| ~ greater(zero,growth_rate(first_movers,sk4(A))) ) ))),
% 0.11/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.11/0.70 fof(f23,plain,(
% 0.11/0.70 ![A,C]: ((![B]: (~greater(A,B)|~greater(B,C)))|greater(A,C))),
% 0.11/0.70 inference(miniscoping,[status(thm)],[f1])).
% 0.11/0.70 fof(f24,plain,(
% 0.11/0.70 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f23])).
% 0.11/0.70 fof(f25,plain,(
% 0.11/0.70 ![B,C]: ((((![A]: (~in_environment(A,B)|~in_environment(A,C)))|greater(C,B))|C=B)|greater(B,C))),
% 0.11/0.70 inference(miniscoping,[status(thm)],[f2])).
% 0.11/0.70 fof(f26,plain,(
% 0.11/0.70 ![X0,X1,X2]: (~in_environment(X0,X1)|~in_environment(X0,X2)|greater(X2,X1)|X2=X1|greater(X1,X2))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f25])).
% 0.11/0.70 fof(f27,plain,(
% 0.11/0.70 ![X0,X1]: (~greater_or_equal(X0,X1)|greater(X0,X1)|X0=X1)),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f3])).
% 0.11/0.70 fof(f28,plain,(
% 0.11/0.70 ![X0,X1]: (~greater(X0,X1)|greater_or_equal(X0,X1))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f4])).
% 0.11/0.70 fof(f29,plain,(
% 0.11/0.70 ![X0,X1]: (~X0=X1|greater_or_equal(X0,X1))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f5])).
% 0.11/0.70 fof(f30,plain,(
% 0.11/0.70 ![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))),
% 0.11/0.70 inference(miniscoping,[status(thm)],[f6])).
% 0.11/0.70 fof(f31,plain,(
% 0.11/0.70 ![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))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f30])).
% 0.11/0.70 fof(f32,plain,(
% 0.11/0.70 ![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)))),
% 0.11/0.70 inference(miniscoping,[status(thm)],[f7])).
% 0.11/0.70 fof(f33,plain,(
% 0.11/0.70 ![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)))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f32])).
% 0.11/0.70 fof(f34,plain,(
% 0.11/0.70 ![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))),
% 0.11/0.70 inference(miniscoping,[status(thm)],[f8])).
% 0.11/0.70 fof(f35,plain,(
% 0.11/0.70 ![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))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f34])).
% 0.11/0.70 fof(f36,plain,(
% 0.11/0.70 ![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)))),
% 0.11/0.70 inference(miniscoping,[status(thm)],[f9])).
% 0.11/0.70 fof(f37,plain,(
% 0.11/0.70 ![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)))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f36])).
% 0.11/0.70 fof(f38,plain,(
% 0.11/0.70 ![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))),
% 0.11/0.70 inference(miniscoping,[status(thm)],[f10])).
% 0.11/0.70 fof(f39,plain,(
% 0.11/0.70 ![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))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f38])).
% 0.11/0.70 fof(f40,plain,(
% 0.11/0.70 ![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)))),
% 0.11/0.70 inference(miniscoping,[status(thm)],[f11])).
% 0.11/0.70 fof(f41,plain,(
% 0.11/0.70 ![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)))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f40])).
% 0.11/0.70 fof(f42,plain,(
% 0.11/0.70 ![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))),
% 0.11/0.70 inference(miniscoping,[status(thm)],[f12])).
% 0.11/0.70 fof(f43,plain,(
% 0.11/0.70 ![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))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f42])).
% 0.11/0.70 fof(f44,plain,(
% 0.11/0.70 ![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)))),
% 0.11/0.70 inference(miniscoping,[status(thm)],[f13])).
% 0.11/0.70 fof(f45,plain,(
% 0.11/0.70 ![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)))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f44])).
% 0.11/0.70 fof(f46,plain,(
% 0.11/0.70 ![X0]: (~environment(X0)|~stable(X0)|in_environment(X0,sk1(X0)))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f14])).
% 0.11/0.70 fof(f47,plain,(
% 0.11/0.70 ![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)))),
% 0.11/0.70 inference(miniscoping,[status(thm)],[f15])).
% 0.11/0.70 fof(f48,plain,(
% 0.11/0.70 ![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)))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f47])).
% 0.11/0.70 fof(f49,plain,(
% 0.11/0.70 ![X0]: (~environment(X0)|~stable(X0)|in_environment(X0,sk2(X0)))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f16])).
% 0.11/0.70 fof(f50,plain,(
% 0.11/0.70 ![X0]: (~environment(X0)|~stable(X0)|greater_or_equal(sk2(X0),equilibrium(X0)))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f17])).
% 0.11/0.70 fof(f51,plain,(
% 0.11/0.70 environment(sk3)),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f18])).
% 0.11/0.70 fof(f52,plain,(
% 0.11/0.70 stable(sk3)),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f19])).
% 0.11/0.70 fof(f53,plain,(
% 0.11/0.70 ![X0]: (~in_environment(sk3,X0)|subpopulations(first_movers,efficient_producers,sk3,sk4(X0)))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f20])).
% 0.11/0.70 fof(f54,plain,(
% 0.11/0.70 ![X0]: (~in_environment(sk3,X0)|greater_or_equal(sk4(X0),X0))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f21])).
% 0.11/0.70 fof(f55,plain,(
% 0.11/0.70 ![X0]: (~in_environment(sk3,X0)|~greater(growth_rate(efficient_producers,sk4(X0)),zero)|~greater(zero,growth_rate(first_movers,sk4(X0))))),
% 0.11/0.70 inference(cnf_transformation,[status(thm)],[f22])).
% 0.11/0.70 fof(f56,plain,(
% 0.11/0.70 ![X0]: (greater_or_equal(X0,X0))),
% 0.11/0.70 inference(destructive_equality_resolution,[status(thm)],[f29])).
% 0.11/0.70 fof(f58,plain,(
% 0.11/0.70 ~stable(sk3)|in_environment(sk3,sk1(sk3))),
% 0.11/0.70 inference(resolution,[status(thm)],[f46,f51])).
% 0.11/0.70 fof(f59,definition,(
% 0.11/0.70 sQ0_spl <=> (stable(sk3))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f61,plain,(
% 0.11/0.70 ~stable(sk3)|sQ0_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f59])).
% 0.11/0.70 fof(f62,definition,(
% 0.11/0.70 sQ1_spl <=> (in_environment(sk3,sk1(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f63,plain,(
% 0.11/0.70 in_environment(sk3,sk1(sk3))|~sQ1_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f62])).
% 0.11/0.70 fof(f65,plain,(
% 0.11/0.70 ~sQ0_spl|sQ1_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f58,f59,f62])).
% 0.11/0.70 fof(f66,plain,(
% 0.11/0.70 $false|sQ0_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f61,f52])).
% 0.11/0.70 fof(f67,plain,(
% 0.11/0.70 sQ0_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f66])).
% 0.11/0.70 fof(f68,plain,(
% 0.11/0.70 subpopulations(first_movers,efficient_producers,sk3,sk4(sk1(sk3)))|~sQ1_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f63,f53])).
% 0.11/0.70 fof(f69,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk1(sk3)),sk1(sk3))|~sQ1_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f63,f54])).
% 0.11/0.70 fof(f70,plain,(
% 0.11/0.70 ![X0]: (~in_environment(sk3,X0)|greater(sk1(sk3),X0)|sk1(sk3)=X0|greater(X0,sk1(sk3))|~sQ1_spl)),
% 0.11/0.70 inference(resolution,[status(thm)],[f63,f26])).
% 0.11/0.70 fof(f71,plain,(
% 0.11/0.70 greater(sk4(sk1(sk3)),sk1(sk3))|sk4(sk1(sk3))=sk1(sk3)|~sQ1_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f69,f27])).
% 0.11/0.70 fof(f72,definition,(
% 0.11/0.70 sQ2_spl <=> (greater(sk4(sk1(sk3)),sk1(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f73,plain,(
% 0.11/0.70 greater(sk4(sk1(sk3)),sk1(sk3))|~sQ2_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f72])).
% 0.11/0.70 fof(f75,definition,(
% 0.11/0.70 sQ3_spl <=> (sk4(sk1(sk3))=sk1(sk3))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f76,plain,(
% 0.11/0.70 sk4(sk1(sk3))=sk1(sk3)|~sQ3_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f75])).
% 0.11/0.70 fof(f78,plain,(
% 0.11/0.70 sQ2_spl|sQ3_spl|~sQ1_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f71,f72,f75,f62])).
% 0.11/0.70 fof(f81,plain,(
% 0.11/0.70 greater(sk1(sk3),sk1(sk3))|sk1(sk3)=sk1(sk3)|greater(sk1(sk3),sk1(sk3))|~sQ1_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f70,f63])).
% 0.11/0.70 fof(f82,definition,(
% 0.11/0.70 sQ4_spl <=> (greater(sk1(sk3),sk1(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f83,plain,(
% 0.11/0.70 greater(sk1(sk3),sk1(sk3))|~sQ4_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f82])).
% 0.11/0.70 fof(f85,definition,(
% 0.11/0.70 sQ5_spl <=> (sk1(sk3)=sk1(sk3))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f88,plain,(
% 0.11/0.70 sQ4_spl|sQ5_spl|~sQ1_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f81,f82,f85,f62])).
% 0.11/0.70 fof(f91,plain,(
% 0.11/0.70 ~stable(sk3)|in_environment(sk3,sk2(sk3))),
% 0.11/0.70 inference(resolution,[status(thm)],[f49,f51])).
% 0.11/0.70 fof(f92,definition,(
% 0.11/0.70 sQ6_spl <=> (in_environment(sk3,sk2(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f93,plain,(
% 0.11/0.70 in_environment(sk3,sk2(sk3))|~sQ6_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f92])).
% 0.11/0.70 fof(f95,plain,(
% 0.11/0.70 ~sQ0_spl|sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f91,f59,f92])).
% 0.11/0.70 fof(f96,plain,(
% 0.11/0.70 ~stable(sk3)|greater_or_equal(sk2(sk3),equilibrium(sk3))),
% 0.11/0.70 inference(resolution,[status(thm)],[f50,f51])).
% 0.11/0.70 fof(f97,definition,(
% 0.11/0.70 sQ7_spl <=> (greater_or_equal(sk2(sk3),equilibrium(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f98,plain,(
% 0.11/0.70 greater_or_equal(sk2(sk3),equilibrium(sk3))|~sQ7_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f97])).
% 0.11/0.70 fof(f100,plain,(
% 0.11/0.70 ~sQ0_spl|sQ7_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f96,f59,f97])).
% 0.11/0.70 fof(f101,plain,(
% 0.11/0.70 greater(sk1(sk3),sk2(sk3))|sk1(sk3)=sk2(sk3)|greater(sk2(sk3),sk1(sk3))|~sQ6_spl|~sQ1_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f93,f70])).
% 0.11/0.70 fof(f102,plain,(
% 0.11/0.70 subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3)))|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f93,f53])).
% 0.11/0.70 fof(f103,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk2(sk3)),sk2(sk3))|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f93,f54])).
% 0.11/0.70 fof(f105,definition,(
% 0.11/0.70 sQ8_spl <=> (greater(sk1(sk3),sk2(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f106,plain,(
% 0.11/0.70 greater(sk1(sk3),sk2(sk3))|~sQ8_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f105])).
% 0.11/0.70 fof(f108,definition,(
% 0.11/0.70 sQ9_spl <=> (sk1(sk3)=sk2(sk3))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f109,plain,(
% 0.11/0.70 sk1(sk3)=sk2(sk3)|~sQ9_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f108])).
% 0.11/0.70 fof(f111,definition,(
% 0.11/0.70 sQ10_spl <=> (greater(sk2(sk3),sk1(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f112,plain,(
% 0.11/0.70 greater(sk2(sk3),sk1(sk3))|~sQ10_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f111])).
% 0.11/0.70 fof(f114,plain,(
% 0.11/0.70 sQ8_spl|sQ9_spl|sQ10_spl|~sQ6_spl|~sQ1_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f101,f105,f108,f111,f92,f62])).
% 0.11/0.70 fof(f115,plain,(
% 0.11/0.70 greater(sk2(sk3),equilibrium(sk3))|sk2(sk3)=equilibrium(sk3)|~sQ7_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f98,f27])).
% 0.11/0.70 fof(f116,definition,(
% 0.11/0.70 sQ11_spl <=> (greater(sk2(sk3),equilibrium(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f117,plain,(
% 0.11/0.70 greater(sk2(sk3),equilibrium(sk3))|~sQ11_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f116])).
% 0.11/0.70 fof(f119,definition,(
% 0.11/0.70 sQ12_spl <=> (sk2(sk3)=equilibrium(sk3))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f120,plain,(
% 0.11/0.70 sk2(sk3)=equilibrium(sk3)|~sQ12_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f119])).
% 0.11/0.70 fof(f122,plain,(
% 0.11/0.70 sQ11_spl|sQ12_spl|~sQ7_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f115,f116,f119,f97])).
% 0.11/0.70 fof(f125,plain,(
% 0.11/0.70 greater_or_equal(sk2(sk3),sk1(sk3))|~sQ10_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f112,f28])).
% 0.11/0.70 fof(f126,plain,(
% 0.11/0.70 ![X0]: (~greater(X0,sk2(sk3))|greater(X0,sk1(sk3))|~sQ10_spl)),
% 0.11/0.70 inference(resolution,[status(thm)],[f112,f24])).
% 0.11/0.70 fof(f131,plain,(
% 0.11/0.70 greater(sk4(sk2(sk3)),sk2(sk3))|sk4(sk2(sk3))=sk2(sk3)|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f103,f27])).
% 0.11/0.70 fof(f132,definition,(
% 0.11/0.70 sQ13_spl <=> (greater(sk4(sk2(sk3)),sk2(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f133,plain,(
% 0.11/0.70 greater(sk4(sk2(sk3)),sk2(sk3))|~sQ13_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f132])).
% 0.11/0.70 fof(f135,definition,(
% 0.11/0.70 sQ14_spl <=> (sk4(sk2(sk3))=sk2(sk3))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f136,plain,(
% 0.11/0.70 sk4(sk2(sk3))=sk2(sk3)|~sQ14_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f135])).
% 0.11/0.70 fof(f138,plain,(
% 0.11/0.70 sQ13_spl|sQ14_spl|~sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f131,f132,f135,f92])).
% 0.11/0.70 fof(f142,plain,(
% 0.11/0.70 ~in_environment(sk3,sk2(sk3))|~greater(growth_rate(efficient_producers,sk2(sk3)),zero)|~greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ14_spl),
% 0.11/0.70 inference(paramodulation,[status(thm)],[f136,f55])).
% 0.11/0.70 fof(f143,definition,(
% 0.11/0.70 sQ15_spl <=> (greater(growth_rate(efficient_producers,sk2(sk3)),zero))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f145,plain,(
% 0.11/0.70 ~greater(growth_rate(efficient_producers,sk2(sk3)),zero)|sQ15_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f143])).
% 0.11/0.70 fof(f146,definition,(
% 0.11/0.70 sQ16_spl <=> (greater(zero,growth_rate(first_movers,sk4(sk2(sk3)))))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f148,plain,(
% 0.11/0.70 ~greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|sQ16_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f146])).
% 0.11/0.70 fof(f149,plain,(
% 0.11/0.70 ~sQ6_spl|~sQ15_spl|~sQ16_spl|~sQ14_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f142,f92,f143,f146,f135])).
% 0.11/0.70 fof(f154,plain,(
% 0.11/0.70 ~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),
% 0.11/0.70 inference(resolution,[status(thm)],[f48,f68])).
% 0.11/0.70 fof(f155,definition,(
% 0.11/0.70 sQ17_spl <=> (environment(sk3))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f157,plain,(
% 0.11/0.70 ~environment(sk3)|sQ17_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f155])).
% 0.11/0.70 fof(f158,definition,(
% 0.11/0.70 sQ18_spl <=> (greater_or_equal(sk4(sk1(sk3)),sk1(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f160,plain,(
% 0.11/0.70 ~greater_or_equal(sk4(sk1(sk3)),sk1(sk3))|sQ18_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f158])).
% 0.11/0.70 fof(f161,definition,(
% 0.11/0.70 sQ19_spl <=> (greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3)))))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f162,plain,(
% 0.11/0.70 greater(growth_rate(efficient_producers,sk4(sk1(sk3))),growth_rate(first_movers,sk4(sk1(sk3))))|~sQ19_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f161])).
% 0.11/0.70 fof(f164,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ0_spl|~sQ18_spl|sQ19_spl|~sQ1_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f154,f155,f59,f158,f161,f62])).
% 0.11/0.70 fof(f165,plain,(
% 0.11/0.70 $false|~sQ1_spl|sQ18_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f160,f69])).
% 0.11/0.70 fof(f166,plain,(
% 0.11/0.70 ~sQ1_spl|sQ18_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f165])).
% 0.11/0.70 fof(f167,plain,(
% 0.11/0.70 $false|sQ17_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f157,f51])).
% 0.11/0.70 fof(f168,plain,(
% 0.11/0.70 sQ17_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f167])).
% 0.11/0.70 fof(f170,plain,(
% 0.11/0.70 greater(sk4(sk2(sk3)),sk1(sk3))|~sQ10_spl|~sQ13_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f126,f133])).
% 0.11/0.70 fof(f171,plain,(
% 0.11/0.70 ~environment(sk3)|~greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|growth_rate(first_movers,sk4(sk1(sk3)))=zero|greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)|greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~sQ1_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f31,f68])).
% 0.11/0.70 fof(f172,definition,(
% 0.11/0.70 sQ20_spl <=> (greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f173,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|~sQ20_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f172])).
% 0.11/0.70 fof(f174,plain,(
% 0.11/0.70 ~greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|sQ20_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f172])).
% 0.11/0.70 fof(f175,definition,(
% 0.11/0.70 sQ21_spl <=> (growth_rate(first_movers,sk4(sk1(sk3)))=zero)),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f176,plain,(
% 0.11/0.70 growth_rate(first_movers,sk4(sk1(sk3)))=zero|~sQ21_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f175])).
% 0.11/0.70 fof(f178,definition,(
% 0.11/0.70 sQ22_spl <=> (greater(growth_rate(first_movers,sk4(sk1(sk3))),zero))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f179,plain,(
% 0.11/0.70 greater(growth_rate(first_movers,sk4(sk1(sk3))),zero)|~sQ22_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f178])).
% 0.11/0.70 fof(f181,definition,(
% 0.11/0.70 sQ23_spl <=> (greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f182,plain,(
% 0.11/0.70 greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~sQ23_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f181])).
% 0.11/0.70 fof(f184,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ20_spl|sQ21_spl|sQ22_spl|sQ23_spl|~sQ1_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f171,f155,f172,f175,f178,f181,f62])).
% 0.11/0.70 fof(f185,plain,(
% 0.11/0.70 greater(zero,zero)|~sQ21_spl|~sQ22_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f176,f179])).
% 0.11/0.70 fof(f186,plain,(
% 0.11/0.70 greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~sQ21_spl|~sQ19_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f176,f162])).
% 0.11/0.70 fof(f187,plain,(
% 0.11/0.70 ~greater_or_equal(sk4(sk1(sk3)),sk2(sk3))|~sQ12_spl|sQ20_spl),
% 0.11/0.70 inference(forward_demodulation,[status(thm)],[f120,f174])).
% 0.11/0.70 fof(f189,definition,(
% 0.11/0.70 sQ24_spl <=> (greater(zero,growth_rate(first_movers,sk4(sk1(sk3)))))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f191,plain,(
% 0.11/0.70 ~greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))|sQ24_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f189])).
% 0.11/0.70 fof(f195,definition,(
% 0.11/0.70 sQ25_spl <=> (greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3)))))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f196,plain,(
% 0.11/0.70 greater(zero,growth_rate(efficient_producers,sk4(sk1(sk3))))|~sQ25_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f195])).
% 0.11/0.70 fof(f201,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk2(sk3)),sk1(sk3))|~sQ10_spl|~sQ13_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f170,f28])).
% 0.11/0.70 fof(f203,plain,(
% 0.11/0.70 greater(sk4(sk2(sk3)),sk1(sk3))|sk4(sk2(sk3))=sk1(sk3)|~sQ10_spl|~sQ13_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f201,f27])).
% 0.11/0.70 fof(f204,definition,(
% 0.11/0.70 sQ26_spl <=> (greater(sk4(sk2(sk3)),sk1(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f205,plain,(
% 0.11/0.70 greater(sk4(sk2(sk3)),sk1(sk3))|~sQ26_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f204])).
% 0.11/0.70 fof(f206,plain,(
% 0.11/0.70 ~greater(sk4(sk2(sk3)),sk1(sk3))|sQ26_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f204])).
% 0.11/0.70 fof(f207,definition,(
% 0.11/0.70 sQ27_spl <=> (sk4(sk2(sk3))=sk1(sk3))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f208,plain,(
% 0.11/0.70 sk4(sk2(sk3))=sk1(sk3)|~sQ27_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f207])).
% 0.11/0.70 fof(f210,plain,(
% 0.11/0.70 sQ26_spl|sQ27_spl|~sQ10_spl|~sQ13_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f203,f204,f207,f111,f132])).
% 0.11/0.70 fof(f214,plain,(
% 0.11/0.70 subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))|~sQ27_spl|~sQ6_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f208,f102])).
% 0.11/0.70 fof(f217,plain,(
% 0.11/0.70 ~greater_or_equal(sk4(sk1(sk3)),sk1(sk3))|~sQ9_spl|~sQ12_spl|sQ20_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f109,f187])).
% 0.11/0.70 fof(f226,plain,(
% 0.11/0.70 ~sQ18_spl|~sQ9_spl|~sQ12_spl|sQ20_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f217,f158,f108,f119,f172])).
% 0.11/0.70 fof(f241,plain,(
% 0.11/0.70 subpopulations(first_movers,efficient_producers,sk3,sk1(sk3))|~sQ3_spl|~sQ1_spl),
% 0.11/0.70 inference(forward_demodulation,[status(thm)],[f76,f68])).
% 0.11/0.70 fof(f246,plain,(
% 0.11/0.70 ~greater_or_equal(sk1(sk3),equilibrium(sk3))|~sQ3_spl|sQ20_spl),
% 0.11/0.70 inference(forward_demodulation,[status(thm)],[f76,f174])).
% 0.11/0.70 fof(f253,plain,(
% 0.11/0.70 ![X0]: (~greater(X0,sk1(sk3))|greater(X0,sk2(sk3))|~sQ8_spl)),
% 0.11/0.70 inference(resolution,[status(thm)],[f106,f24])).
% 0.11/0.70 fof(f254,plain,(
% 0.11/0.70 ~in_environment(sk3,sk1(sk3))|~greater(growth_rate(efficient_producers,sk1(sk3)),zero)|~greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))|~sQ3_spl),
% 0.11/0.70 inference(paramodulation,[status(thm)],[f76,f55])).
% 0.11/0.70 fof(f255,definition,(
% 0.11/0.70 sQ28_spl <=> (greater(growth_rate(efficient_producers,sk1(sk3)),zero))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f256,plain,(
% 0.11/0.70 greater(growth_rate(efficient_producers,sk1(sk3)),zero)|~sQ28_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f255])).
% 0.11/0.70 fof(f257,plain,(
% 0.11/0.70 ~greater(growth_rate(efficient_producers,sk1(sk3)),zero)|sQ28_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f255])).
% 0.11/0.70 fof(f258,plain,(
% 0.11/0.70 ~sQ1_spl|~sQ28_spl|~sQ24_spl|~sQ3_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f254,f62,f255,f189,f75])).
% 0.11/0.70 fof(f262,plain,(
% 0.11/0.70 ![X0]: (~greater(X0,sk2(sk3))|greater(X0,equilibrium(sk3))|~sQ11_spl)),
% 0.11/0.70 inference(resolution,[status(thm)],[f117,f24])).
% 0.11/0.70 fof(f269,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk2(sk3)),sk1(sk3))|~sQ26_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f205,f28])).
% 0.11/0.70 fof(f281,plain,(
% 0.11/0.70 ~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)|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f102,f35])).
% 0.11/0.70 fof(f282,plain,(
% 0.11/0.70 ~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))))|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f102,f33])).
% 0.11/0.70 fof(f283,plain,(
% 0.11/0.70 ~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(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f102,f31])).
% 0.11/0.70 fof(f284,plain,(
% 0.11/0.70 ~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))))|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f102,f48])).
% 0.11/0.70 fof(f285,definition,(
% 0.11/0.70 sQ31_spl <=> (greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f286,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|~sQ31_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f285])).
% 0.11/0.70 fof(f287,plain,(
% 0.11/0.70 ~greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|sQ31_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f285])).
% 0.11/0.70 fof(f288,definition,(
% 0.11/0.70 sQ32_spl <=> (growth_rate(first_movers,sk4(sk2(sk3)))=zero)),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f289,plain,(
% 0.11/0.70 growth_rate(first_movers,sk4(sk2(sk3)))=zero|~sQ32_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f288])).
% 0.11/0.70 fof(f291,definition,(
% 0.11/0.70 sQ33_spl <=> (greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3)))))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f292,plain,(
% 0.11/0.70 greater(zero,growth_rate(efficient_producers,sk4(sk2(sk3))))|~sQ33_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f291])).
% 0.11/0.70 fof(f294,definition,(
% 0.11/0.70 sQ34_spl <=> (greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f295,plain,(
% 0.11/0.70 greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|~sQ34_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f294])).
% 0.11/0.70 fof(f296,plain,(
% 0.11/0.70 ~greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|sQ34_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f294])).
% 0.11/0.70 fof(f297,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ31_spl|sQ32_spl|sQ33_spl|sQ34_spl|~sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f281,f155,f285,f288,f291,f294,f92])).
% 0.11/0.70 fof(f298,definition,(
% 0.11/0.70 sQ35_spl <=> (greater(growth_rate(first_movers,sk4(sk2(sk3))),zero))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f299,plain,(
% 0.11/0.70 greater(growth_rate(first_movers,sk4(sk2(sk3))),zero)|~sQ35_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f298])).
% 0.11/0.70 fof(f301,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ31_spl|sQ32_spl|sQ35_spl|sQ16_spl|~sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f282,f155,f285,f288,f298,f146,f92])).
% 0.11/0.70 fof(f302,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ31_spl|sQ32_spl|sQ35_spl|sQ34_spl|~sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f283,f155,f285,f288,f298,f294,f92])).
% 0.11/0.70 fof(f303,definition,(
% 0.11/0.70 sQ36_spl <=> (greater_or_equal(sk4(sk2(sk3)),sk1(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f304,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk2(sk3)),sk1(sk3))|~sQ36_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f303])).
% 0.11/0.70 fof(f305,plain,(
% 0.11/0.70 ~greater_or_equal(sk4(sk2(sk3)),sk1(sk3))|sQ36_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f303])).
% 0.11/0.70 fof(f306,definition,(
% 0.11/0.70 sQ37_spl <=> (greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3)))))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f307,plain,(
% 0.11/0.70 greater(growth_rate(efficient_producers,sk4(sk2(sk3))),growth_rate(first_movers,sk4(sk2(sk3))))|~sQ37_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f306])).
% 0.11/0.70 fof(f309,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ0_spl|~sQ36_spl|sQ37_spl|~sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f284,f155,f59,f303,f306,f92])).
% 0.11/0.70 fof(f311,plain,(
% 0.11/0.70 $false|~sQ26_spl|sQ36_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f305,f269])).
% 0.11/0.70 fof(f312,plain,(
% 0.11/0.70 ~sQ26_spl|sQ36_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f311])).
% 0.11/0.70 fof(f313,plain,(
% 0.11/0.70 greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|~sQ32_spl|~sQ37_spl),
% 0.11/0.70 inference(forward_demodulation,[status(thm)],[f289,f307])).
% 0.11/0.70 fof(f316,plain,(
% 0.11/0.70 greater_or_equal(sk1(sk3),sk2(sk3))|~sQ27_spl|~sQ6_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f208,f103])).
% 0.11/0.70 fof(f317,plain,(
% 0.11/0.70 greater(sk1(sk3),sk2(sk3))|~sQ27_spl|~sQ13_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f208,f133])).
% 0.11/0.70 fof(f318,plain,(
% 0.11/0.70 ~greater(sk1(sk3),sk1(sk3))|~sQ27_spl|sQ26_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f208,f206])).
% 0.11/0.70 fof(f320,plain,(
% 0.11/0.70 greater(growth_rate(efficient_producers,sk1(sk3)),zero)|~sQ27_spl|~sQ34_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f208,f295])).
% 0.11/0.70 fof(f325,plain,(
% 0.11/0.70 $false|~sQ4_spl|~sQ27_spl|sQ26_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f318,f83])).
% 0.11/0.70 fof(f326,plain,(
% 0.11/0.70 ~sQ4_spl|~sQ27_spl|sQ26_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f325])).
% 0.11/0.70 fof(f327,plain,(
% 0.11/0.70 $false|sQ28_spl|~sQ27_spl|~sQ34_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f320,f257])).
% 0.11/0.70 fof(f328,plain,(
% 0.11/0.70 sQ28_spl|~sQ27_spl|~sQ34_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f327])).
% 0.11/0.70 fof(f329,plain,(
% 0.11/0.70 sQ34_spl|~sQ32_spl|~sQ37_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f313,f294,f288,f306])).
% 0.11/0.70 fof(f330,plain,(
% 0.11/0.70 ~greater(growth_rate(efficient_producers,sk1(sk3)),zero)|~sQ27_spl|sQ34_spl),
% 0.11/0.70 inference(forward_demodulation,[status(thm)],[f208,f296])).
% 0.11/0.70 fof(f331,plain,(
% 0.11/0.70 $false|~sQ27_spl|sQ34_spl|~sQ28_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f256,f330])).
% 0.11/0.70 fof(f332,plain,(
% 0.11/0.70 ~sQ27_spl|sQ34_spl|~sQ28_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f331])).
% 0.11/0.70 fof(f338,plain,(
% 0.11/0.70 ~greater_or_equal(sk1(sk3),sk1(sk3))|~sQ27_spl|sQ36_spl),
% 0.11/0.70 inference(forward_demodulation,[status(thm)],[f208,f305])).
% 0.11/0.70 fof(f339,plain,(
% 0.11/0.70 $false|~sQ27_spl|sQ36_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f338,f56])).
% 0.11/0.70 fof(f340,plain,(
% 0.11/0.70 ~sQ27_spl|sQ36_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f339])).
% 0.11/0.70 fof(f356,plain,(
% 0.11/0.70 greater(sk4(sk1(sk3)),sk2(sk3))|~sQ8_spl|~sQ2_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f253,f73])).
% 0.11/0.70 fof(f358,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk1(sk3)),sk2(sk3))|~sQ8_spl|~sQ2_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f356,f28])).
% 0.11/0.70 fof(f360,plain,(
% 0.11/0.70 greater(sk4(sk1(sk3)),sk2(sk3))|sk4(sk1(sk3))=sk2(sk3)|~sQ8_spl|~sQ2_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f358,f27])).
% 0.11/0.70 fof(f361,definition,(
% 0.11/0.70 sQ38_spl <=> (greater(sk4(sk1(sk3)),sk2(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f362,plain,(
% 0.11/0.70 greater(sk4(sk1(sk3)),sk2(sk3))|~sQ38_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f361])).
% 0.11/0.70 fof(f363,plain,(
% 0.11/0.70 ~greater(sk4(sk1(sk3)),sk2(sk3))|sQ38_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f361])).
% 0.11/0.70 fof(f364,definition,(
% 0.11/0.70 sQ39_spl <=> (sk4(sk1(sk3))=sk2(sk3))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f365,plain,(
% 0.11/0.70 sk4(sk1(sk3))=sk2(sk3)|~sQ39_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f364])).
% 0.11/0.70 fof(f367,plain,(
% 0.11/0.70 sQ38_spl|sQ39_spl|~sQ8_spl|~sQ2_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f360,f361,f364,f105,f72])).
% 0.11/0.70 fof(f371,plain,(
% 0.11/0.70 greater(sk2(sk3),sk1(sk3))|~sQ39_spl|~sQ2_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f365,f73])).
% 0.11/0.70 fof(f382,plain,(
% 0.11/0.70 ~greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|~sQ9_spl|sQ31_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f109,f287])).
% 0.11/0.70 fof(f384,plain,(
% 0.11/0.70 greater(sk4(sk2(sk3)),sk1(sk3))|~sQ9_spl|~sQ13_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f109,f133])).
% 0.11/0.70 fof(f385,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk2(sk3)),sk1(sk3))|~sQ9_spl|~sQ6_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f109,f103])).
% 0.11/0.70 fof(f387,plain,(
% 0.11/0.70 ~greater(growth_rate(efficient_producers,sk1(sk3)),zero)|~sQ9_spl|sQ15_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f109,f145])).
% 0.11/0.70 fof(f408,plain,(
% 0.11/0.70 sQ10_spl|~sQ39_spl|~sQ2_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f371,f111,f364,f72])).
% 0.11/0.70 fof(f415,plain,(
% 0.11/0.70 ~sQ20_spl|~sQ9_spl|sQ31_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f382,f172,f108,f285])).
% 0.11/0.70 fof(f416,plain,(
% 0.11/0.70 sQ26_spl|~sQ9_spl|~sQ13_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f384,f204,f108,f132])).
% 0.11/0.70 fof(f417,plain,(
% 0.11/0.70 sQ36_spl|~sQ9_spl|~sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f385,f303,f108,f92])).
% 0.11/0.70 fof(f419,plain,(
% 0.11/0.70 ~sQ28_spl|~sQ9_spl|sQ15_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f387,f255,f108,f143])).
% 0.11/0.70 fof(f429,plain,(
% 0.11/0.70 ~greater(zero,zero)|~sQ21_spl|sQ24_spl),
% 0.11/0.70 inference(forward_demodulation,[status(thm)],[f176,f191])).
% 0.11/0.70 fof(f430,plain,(
% 0.11/0.70 $false|~sQ22_spl|~sQ21_spl|sQ24_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f429,f185])).
% 0.11/0.70 fof(f431,plain,(
% 0.11/0.70 ~sQ22_spl|~sQ21_spl|sQ24_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f430])).
% 0.11/0.70 fof(f437,plain,(
% 0.11/0.70 greater(sk1(sk3),sk2(sk3))|~sQ27_spl|~sQ13_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f208,f133])).
% 0.11/0.70 fof(f448,plain,(
% 0.11/0.70 sQ8_spl|~sQ27_spl|~sQ13_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f317,f105,f207,f132])).
% 0.11/0.70 fof(f458,plain,(
% 0.11/0.70 subpopulations(first_movers,efficient_producers,sk3,sk4(sk2(sk3)))|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f93,f53])).
% 0.11/0.70 fof(f459,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk2(sk3)),sk2(sk3))|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f93,f54])).
% 0.11/0.70 fof(f468,plain,(
% 0.11/0.70 ~in_environment(sk3,sk2(sk3))|~greater(growth_rate(efficient_producers,sk1(sk3)),zero)|~greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ27_spl),
% 0.11/0.70 inference(paramodulation,[status(thm)],[f208,f55])).
% 0.11/0.70 fof(f469,plain,(
% 0.11/0.70 ~sQ6_spl|~sQ28_spl|~sQ16_spl|~sQ27_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f468,f92,f255,f146,f207])).
% 0.11/0.70 fof(f476,plain,(
% 0.11/0.70 greater(sk1(sk3),sk2(sk3))|sk1(sk3)=sk2(sk3)|~sQ27_spl|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f316,f27])).
% 0.11/0.70 fof(f477,plain,(
% 0.11/0.70 sQ8_spl|sQ9_spl|~sQ27_spl|~sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f476,f105,f108,f207,f92])).
% 0.11/0.70 fof(f484,plain,(
% 0.11/0.70 ~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(zero,growth_rate(first_movers,sk4(sk1(sk3))))|~sQ1_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f68,f41])).
% 0.11/0.70 fof(f485,plain,(
% 0.11/0.70 ~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),
% 0.11/0.70 inference(resolution,[status(thm)],[f68,f39])).
% 0.11/0.70 fof(f486,plain,(
% 0.11/0.70 ~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(zero,growth_rate(first_movers,sk4(sk1(sk3))))|~sQ1_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f68,f37])).
% 0.11/0.70 fof(f491,definition,(
% 0.11/0.70 sQ40_spl <=> (growth_rate(efficient_producers,sk4(sk1(sk3)))=zero)),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f492,plain,(
% 0.11/0.70 growth_rate(efficient_producers,sk4(sk1(sk3)))=zero|~sQ40_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f491])).
% 0.11/0.70 fof(f494,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ20_spl|sQ40_spl|sQ22_spl|sQ24_spl|~sQ1_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f484,f155,f172,f491,f178,f189,f62])).
% 0.11/0.70 fof(f495,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ20_spl|sQ40_spl|sQ22_spl|sQ23_spl|~sQ1_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f485,f155,f172,f491,f178,f181,f62])).
% 0.11/0.70 fof(f496,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ20_spl|sQ21_spl|sQ25_spl|sQ24_spl|~sQ1_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f486,f155,f172,f175,f195,f189,f62])).
% 0.11/0.70 fof(f501,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk1(sk3)),sk2(sk3))|~sQ38_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f362,f28])).
% 0.11/0.70 fof(f511,plain,(
% 0.11/0.70 ~environment(sk3)|~stable(sk3)|~greater_or_equal(sk1(sk3),sk1(sk3))|greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))|~sQ27_spl|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f214,f48])).
% 0.11/0.70 fof(f512,definition,(
% 0.11/0.70 sQ41_spl <=> (greater_or_equal(sk1(sk3),equilibrium(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f513,plain,(
% 0.11/0.70 greater_or_equal(sk1(sk3),equilibrium(sk3))|~sQ41_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f512])).
% 0.11/0.70 fof(f514,plain,(
% 0.11/0.70 ~greater_or_equal(sk1(sk3),equilibrium(sk3))|sQ41_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f512])).
% 0.11/0.70 fof(f536,definition,(
% 0.11/0.70 sQ47_spl <=> (greater_or_equal(sk1(sk3),sk1(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f538,plain,(
% 0.11/0.70 ~greater_or_equal(sk1(sk3),sk1(sk3))|sQ47_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f536])).
% 0.11/0.70 fof(f539,definition,(
% 0.11/0.70 sQ48_spl <=> (greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3))))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f542,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ0_spl|~sQ47_spl|sQ48_spl|~sQ27_spl|~sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f511,f155,f59,f536,f539,f207,f92])).
% 0.11/0.70 fof(f543,plain,(
% 0.11/0.70 $false|sQ47_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f538,f56])).
% 0.11/0.70 fof(f544,plain,(
% 0.11/0.70 sQ47_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f543])).
% 0.11/0.70 fof(f549,plain,(
% 0.11/0.70 greater(sk4(sk1(sk3)),equilibrium(sk3))|~sQ11_spl|~sQ38_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f262,f362])).
% 0.11/0.70 fof(f550,plain,(
% 0.11/0.70 greater(sk1(sk3),equilibrium(sk3))|~sQ11_spl|~sQ27_spl|~sQ13_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f262,f437])).
% 0.11/0.70 fof(f551,plain,(
% 0.11/0.70 greater_or_equal(sk1(sk3),equilibrium(sk3))|~sQ11_spl|~sQ27_spl|~sQ13_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f550,f28])).
% 0.11/0.70 fof(f555,plain,(
% 0.11/0.70 $false|~sQ11_spl|~sQ27_spl|~sQ13_spl|sQ41_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f514,f551])).
% 0.11/0.70 fof(f556,plain,(
% 0.11/0.70 ~sQ11_spl|~sQ27_spl|~sQ13_spl|sQ41_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f555])).
% 0.11/0.70 fof(f570,plain,(
% 0.11/0.70 greater(sk1(sk3),equilibrium(sk3))|sk1(sk3)=equilibrium(sk3)|~sQ11_spl|~sQ27_spl|~sQ13_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f551,f27])).
% 0.11/0.70 fof(f571,definition,(
% 0.11/0.70 sQ49_spl <=> (greater(sk1(sk3),equilibrium(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f572,plain,(
% 0.11/0.70 greater(sk1(sk3),equilibrium(sk3))|~sQ49_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f571])).
% 0.11/0.70 fof(f574,definition,(
% 0.11/0.70 sQ50_spl <=> (sk1(sk3)=equilibrium(sk3))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f575,plain,(
% 0.11/0.70 sk1(sk3)=equilibrium(sk3)|~sQ50_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f574])).
% 0.11/0.70 fof(f577,plain,(
% 0.11/0.70 sQ49_spl|sQ50_spl|~sQ11_spl|~sQ27_spl|~sQ13_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f570,f571,f574,f116,f207,f132])).
% 0.11/0.70 fof(f578,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|~sQ11_spl|~sQ38_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f549,f28])).
% 0.11/0.70 fof(f580,plain,(
% 0.11/0.70 sQ20_spl|~sQ11_spl|~sQ38_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f578,f172,f116,f361])).
% 0.11/0.70 fof(f583,plain,(
% 0.11/0.70 greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))|~sQ40_spl|~sQ19_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f492,f162])).
% 0.11/0.70 fof(f588,plain,(
% 0.11/0.70 ~greater_or_equal(sk1(sk3),sk1(sk3))|~sQ50_spl|sQ41_spl),
% 0.11/0.70 inference(forward_demodulation,[status(thm)],[f575,f514])).
% 0.11/0.70 fof(f589,plain,(
% 0.11/0.70 $false|~sQ50_spl|sQ41_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f588,f56])).
% 0.11/0.70 fof(f590,plain,(
% 0.11/0.70 ~sQ50_spl|sQ41_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f589])).
% 0.11/0.70 fof(f611,plain,(
% 0.11/0.70 ~greater(sk2(sk3),sk1(sk3))|~sQ14_spl|sQ26_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f136,f206])).
% 0.11/0.70 fof(f612,plain,(
% 0.11/0.70 ~greater_or_equal(sk2(sk3),sk1(sk3))|~sQ14_spl|sQ36_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f136,f305])).
% 0.11/0.70 fof(f615,plain,(
% 0.11/0.70 ~greater_or_equal(sk2(sk3),equilibrium(sk3))|~sQ14_spl|sQ31_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f136,f287])).
% 0.11/0.70 fof(f618,plain,(
% 0.11/0.70 subpopulations(first_movers,efficient_producers,sk3,sk2(sk3))|~sQ14_spl|~sQ6_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f136,f458])).
% 0.11/0.70 fof(f620,plain,(
% 0.11/0.70 ~greater(zero,growth_rate(first_movers,sk2(sk3)))|~sQ14_spl|sQ16_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f136,f148])).
% 0.11/0.70 fof(f626,plain,(
% 0.11/0.70 ~sQ10_spl|~sQ14_spl|sQ26_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f611,f111,f135,f204])).
% 0.11/0.70 fof(f627,plain,(
% 0.11/0.70 $false|~sQ10_spl|~sQ14_spl|sQ36_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f612,f125])).
% 0.11/0.70 fof(f628,plain,(
% 0.11/0.70 ~sQ10_spl|~sQ14_spl|sQ36_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f627])).
% 0.11/0.70 fof(f630,plain,(
% 0.11/0.70 sQ24_spl|~sQ40_spl|~sQ19_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f583,f189,f491,f161])).
% 0.11/0.70 fof(f648,plain,(
% 0.11/0.70 ~in_environment(sk3,sk1(sk3))|~greater(growth_rate(efficient_producers,sk2(sk3)),zero)|~greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))|~sQ39_spl),
% 0.11/0.70 inference(paramodulation,[status(thm)],[f365,f55])).
% 0.11/0.70 fof(f649,plain,(
% 0.11/0.70 ~sQ1_spl|~sQ15_spl|~sQ24_spl|~sQ39_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f648,f62,f143,f189,f364])).
% 0.11/0.70 fof(f670,plain,(
% 0.11/0.70 greater(growth_rate(efficient_producers,sk2(sk3)),zero)|~sQ39_spl|~sQ23_spl),
% 0.11/0.70 inference(forward_demodulation,[status(thm)],[f365,f182])).
% 0.11/0.70 fof(f675,plain,(
% 0.11/0.70 $false|~sQ39_spl|~sQ23_spl|sQ15_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f145,f670])).
% 0.11/0.70 fof(f676,plain,(
% 0.11/0.70 ~sQ39_spl|~sQ23_spl|sQ15_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f675])).
% 0.11/0.70 fof(f679,plain,(
% 0.11/0.70 sQ23_spl|~sQ21_spl|~sQ19_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f186,f181,f175,f161])).
% 0.11/0.70 fof(f690,plain,(
% 0.11/0.70 greater(sk1(sk3),equilibrium(sk3))|sk1(sk3)=equilibrium(sk3)|~sQ41_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f513,f27])).
% 0.11/0.70 fof(f691,plain,(
% 0.11/0.70 sQ49_spl|sQ50_spl|~sQ41_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f690,f571,f574,f512])).
% 0.11/0.70 fof(f694,plain,(
% 0.11/0.70 greater_or_equal(sk1(sk3),equilibrium(sk3))|~sQ49_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f572,f28])).
% 0.11/0.70 fof(f721,plain,(
% 0.11/0.70 sQ41_spl|~sQ49_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f694,f512,f571])).
% 0.11/0.70 fof(f730,plain,(
% 0.11/0.70 ~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))))|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f458,f45])).
% 0.11/0.70 fof(f731,plain,(
% 0.11/0.70 ~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)|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f458,f43])).
% 0.11/0.70 fof(f732,plain,(
% 0.11/0.70 ~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))))|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f458,f41])).
% 0.11/0.70 fof(f733,plain,(
% 0.11/0.70 ~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)|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f458,f39])).
% 0.11/0.70 fof(f734,plain,(
% 0.11/0.70 ~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))))|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f458,f37])).
% 0.11/0.70 fof(f739,definition,(
% 0.11/0.70 sQ51_spl <=> (growth_rate(efficient_producers,sk4(sk2(sk3)))=zero)),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f740,plain,(
% 0.11/0.70 growth_rate(efficient_producers,sk4(sk2(sk3)))=zero|~sQ51_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f739])).
% 0.11/0.70 fof(f742,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ31_spl|sQ51_spl|sQ33_spl|sQ16_spl|~sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f730,f155,f285,f739,f291,f146,f92])).
% 0.11/0.70 fof(f743,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ31_spl|sQ51_spl|sQ33_spl|sQ34_spl|~sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f731,f155,f285,f739,f291,f294,f92])).
% 0.11/0.70 fof(f744,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ31_spl|sQ51_spl|sQ35_spl|sQ16_spl|~sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f732,f155,f285,f739,f298,f146,f92])).
% 0.11/0.70 fof(f745,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ31_spl|sQ51_spl|sQ35_spl|sQ34_spl|~sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f733,f155,f285,f739,f298,f294,f92])).
% 0.11/0.70 fof(f746,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ31_spl|sQ32_spl|sQ33_spl|sQ16_spl|~sQ6_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f734,f155,f285,f288,f291,f146,f92])).
% 0.11/0.70 fof(f751,plain,(
% 0.11/0.70 greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ51_spl|~sQ37_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f740,f307])).
% 0.11/0.70 fof(f770,plain,(
% 0.11/0.70 greater(sk4(sk2(sk3)),sk1(sk3))|sk4(sk2(sk3))=sk1(sk3)|~sQ36_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f304,f27])).
% 0.11/0.70 fof(f771,plain,(
% 0.11/0.70 sQ26_spl|sQ27_spl|~sQ36_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f770,f204,f207,f303])).
% 0.11/0.70 fof(f776,plain,(
% 0.11/0.70 ~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),
% 0.11/0.70 inference(resolution,[status(thm)],[f68,f45])).
% 0.11/0.70 fof(f785,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ20_spl|sQ40_spl|sQ25_spl|sQ24_spl|~sQ1_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f776,f155,f172,f491,f195,f189,f62])).
% 0.11/0.70 fof(f819,plain,(
% 0.11/0.70 greater(growth_rate(efficient_producers,sk1(sk3)),zero)|~sQ3_spl|~sQ23_spl),
% 0.11/0.70 inference(forward_demodulation,[status(thm)],[f76,f182])).
% 0.11/0.70 fof(f820,plain,(
% 0.11/0.70 $false|sQ28_spl|~sQ3_spl|~sQ23_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f819,f257])).
% 0.11/0.70 fof(f821,plain,(
% 0.11/0.70 sQ28_spl|~sQ3_spl|~sQ23_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f820])).
% 0.11/0.70 fof(f848,plain,(
% 0.11/0.70 greater(sk4(sk2(sk3)),equilibrium(sk3))|~sQ11_spl|~sQ13_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f262,f133])).
% 0.11/0.70 fof(f849,plain,(
% 0.11/0.70 greater(sk4(sk2(sk3)),equilibrium(sk3))|sk4(sk2(sk3))=equilibrium(sk3)|~sQ31_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f286,f27])).
% 0.11/0.70 fof(f850,definition,(
% 0.11/0.70 sQ52_spl <=> (greater(sk4(sk2(sk3)),equilibrium(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f853,definition,(
% 0.11/0.70 sQ53_spl <=> (sk4(sk2(sk3))=equilibrium(sk3))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f854,plain,(
% 0.11/0.70 sk4(sk2(sk3))=equilibrium(sk3)|~sQ53_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f853])).
% 0.11/0.70 fof(f856,plain,(
% 0.11/0.70 sQ52_spl|sQ53_spl|~sQ31_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f849,f850,f853,f285])).
% 0.11/0.70 fof(f871,plain,(
% 0.11/0.70 ~in_environment(sk3,sk2(sk3))|~greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)|~greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ53_spl),
% 0.11/0.70 inference(paramodulation,[status(thm)],[f854,f55])).
% 0.11/0.70 fof(f872,definition,(
% 0.11/0.70 sQ54_spl <=> (greater(growth_rate(efficient_producers,equilibrium(sk3)),zero))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f874,plain,(
% 0.11/0.70 ~greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)|sQ54_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f872])).
% 0.11/0.70 fof(f875,plain,(
% 0.11/0.70 ~sQ6_spl|~sQ54_spl|~sQ16_spl|~sQ53_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f871,f92,f872,f146,f853])).
% 0.11/0.70 fof(f878,plain,(
% 0.11/0.70 greater(sk4(sk1(sk3)),equilibrium(sk3))|sk4(sk1(sk3))=equilibrium(sk3)|~sQ20_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f173,f27])).
% 0.11/0.70 fof(f879,definition,(
% 0.11/0.70 sQ55_spl <=> (greater(sk4(sk1(sk3)),equilibrium(sk3)))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f880,plain,(
% 0.11/0.70 greater(sk4(sk1(sk3)),equilibrium(sk3))|~sQ55_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f879])).
% 0.11/0.70 fof(f882,definition,(
% 0.11/0.70 sQ56_spl <=> (sk4(sk1(sk3))=equilibrium(sk3))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f883,plain,(
% 0.11/0.70 sk4(sk1(sk3))=equilibrium(sk3)|~sQ56_spl),
% 0.11/0.70 inference(component_clause,[status(thm)],[f882])).
% 0.11/0.70 fof(f885,plain,(
% 0.11/0.70 sQ55_spl|sQ56_spl|~sQ20_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f878,f879,f882,f172])).
% 0.11/0.70 fof(f897,plain,(
% 0.11/0.70 greater(growth_rate(efficient_producers,equilibrium(sk3)),zero)|~sQ56_spl|~sQ23_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f883,f182])).
% 0.11/0.70 fof(f898,plain,(
% 0.11/0.70 $false|sQ54_spl|~sQ56_spl|~sQ23_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f897,f874])).
% 0.11/0.70 fof(f899,plain,(
% 0.11/0.70 sQ54_spl|~sQ56_spl|~sQ23_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f898])).
% 0.11/0.70 fof(f900,plain,(
% 0.11/0.70 sQ16_spl|~sQ51_spl|~sQ37_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f751,f146,f739,f306])).
% 0.11/0.70 fof(f935,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk2(sk3)),equilibrium(sk3))|~sQ11_spl|~sQ13_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f848,f28])).
% 0.11/0.70 fof(f963,plain,(
% 0.11/0.70 ~in_environment(sk3,sk1(sk3))|~greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))|~sQ23_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f182,f55])).
% 0.11/0.70 fof(f966,plain,(
% 0.11/0.70 ~sQ1_spl|~sQ24_spl|~sQ23_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f963,f62,f189,f181])).
% 0.11/0.70 fof(f972,plain,(
% 0.11/0.70 ~in_environment(sk3,sk2(sk3))|~greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ34_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f295,f55])).
% 0.11/0.70 fof(f975,plain,(
% 0.11/0.70 ~sQ6_spl|~sQ16_spl|~sQ34_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f972,f92,f146,f294])).
% 0.11/0.70 fof(f976,plain,(
% 0.11/0.70 sQ31_spl|~sQ11_spl|~sQ13_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f935,f285,f116,f132])).
% 0.11/0.70 fof(f977,plain,(
% 0.11/0.70 $false|~sQ7_spl|~sQ14_spl|sQ31_spl),
% 0.11/0.70 inference(forward_subsumption_resolution,[status(thm)],[f615,f98])).
% 0.11/0.70 fof(f978,plain,(
% 0.11/0.70 ~sQ7_spl|~sQ14_spl|sQ31_spl),
% 0.11/0.70 inference(contradiction_clause,[status(thm)],[f977])).
% 0.11/0.70 fof(f994,plain,(
% 0.11/0.70 ![X0]: (~greater(X0,growth_rate(first_movers,sk4(sk1(sk3))))|greater(X0,zero)|~sQ22_spl)),
% 0.11/0.70 inference(resolution,[status(thm)],[f179,f24])).
% 0.11/0.70 fof(f998,plain,(
% 0.11/0.70 ![X0]: (~greater(X0,growth_rate(efficient_producers,sk4(sk2(sk3))))|greater(X0,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ37_spl)),
% 0.11/0.70 inference(resolution,[status(thm)],[f307,f24])).
% 0.11/0.70 fof(f1006,plain,(
% 0.11/0.70 ![X0]: (~greater(X0,growth_rate(first_movers,sk4(sk2(sk3))))|greater(X0,zero)|~sQ35_spl)),
% 0.11/0.70 inference(resolution,[status(thm)],[f299,f24])).
% 0.11/0.70 fof(f1022,plain,(
% 0.11/0.70 ![X0]: (~greater(X0,growth_rate(efficient_producers,sk4(sk1(sk3))))|greater(X0,growth_rate(first_movers,sk4(sk1(sk3))))|~sQ19_spl)),
% 0.11/0.70 inference(resolution,[status(thm)],[f162,f24])).
% 0.11/0.70 fof(f1032,plain,(
% 0.11/0.70 greater(growth_rate(efficient_producers,sk4(sk1(sk3))),zero)|~sQ22_spl|~sQ19_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f994,f162])).
% 0.11/0.70 fof(f1033,plain,(
% 0.11/0.70 sQ23_spl|~sQ22_spl|~sQ19_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f1032,f181,f178,f161])).
% 0.11/0.70 fof(f1056,plain,(
% 0.11/0.70 greater(growth_rate(efficient_producers,sk4(sk2(sk3))),zero)|~sQ35_spl|~sQ37_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f1006,f307])).
% 0.11/0.70 fof(f1072,plain,(
% 0.11/0.70 greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ37_spl|~sQ33_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f998,f292])).
% 0.11/0.70 fof(f1074,plain,(
% 0.11/0.70 sQ16_spl|~sQ37_spl|~sQ33_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f1072,f146,f306,f291])).
% 0.11/0.70 fof(f1075,plain,(
% 0.11/0.70 sQ34_spl|~sQ35_spl|~sQ37_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f1056,f294,f298,f306])).
% 0.11/0.70 fof(f1142,plain,(
% 0.11/0.70 ~environment(sk3)|~stable(sk3)|~greater_or_equal(sk1(sk3),sk1(sk3))|greater(growth_rate(efficient_producers,sk1(sk3)),growth_rate(first_movers,sk1(sk3)))|~sQ3_spl|~sQ1_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f241,f48])).
% 0.11/0.70 fof(f1151,plain,(
% 0.11/0.70 ~sQ17_spl|~sQ0_spl|~sQ47_spl|sQ48_spl|~sQ3_spl|~sQ1_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f1142,f155,f59,f536,f539,f75,f62])).
% 0.11/0.70 fof(f1157,plain,(
% 0.11/0.70 ~in_environment(sk3,sk2(sk3))|~greater(zero,zero)|~greater(zero,growth_rate(first_movers,sk4(sk2(sk3))))|~sQ51_spl),
% 0.11/0.70 inference(paramodulation,[status(thm)],[f740,f55])).
% 0.11/0.70 fof(f1158,definition,(
% 0.11/0.70 sQ59_spl <=> (greater(zero,zero))),
% 0.11/0.70 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.11/0.70 fof(f1161,plain,(
% 0.11/0.70 ~sQ6_spl|~sQ59_spl|~sQ16_spl|~sQ51_spl),
% 0.11/0.70 inference(split_clause,[status(thm)],[f1157,f92,f1158,f146,f739])).
% 0.11/0.70 fof(f1253,plain,(
% 0.11/0.70 ~greater(growth_rate(efficient_producers,sk2(sk3)),zero)|~sQ14_spl|sQ34_spl),
% 0.11/0.70 inference(backward_demodulation,[status(thm)],[f136,f296])).
% 0.11/0.70 fof(f1290,plain,(
% 0.11/0.70 greater_or_equal(sk4(sk1(sk3)),equilibrium(sk3))|~sQ55_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f880,f28])).
% 0.11/0.70 fof(f1296,plain,(
% 0.11/0.70 ~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)))|~sQ14_spl|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f618,f45])).
% 0.11/0.70 fof(f1297,plain,(
% 0.11/0.70 ~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)|~sQ14_spl|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f618,f43])).
% 0.11/0.70 fof(f1298,plain,(
% 0.11/0.70 ~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)))|~sQ14_spl|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f618,f41])).
% 0.11/0.70 fof(f1299,plain,(
% 0.11/0.70 ~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)|~sQ14_spl|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f618,f39])).
% 0.11/0.70 fof(f1300,plain,(
% 0.11/0.70 ~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)))|~sQ14_spl|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f618,f37])).
% 0.11/0.70 fof(f1301,plain,(
% 0.11/0.70 ~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)|~sQ14_spl|~sQ6_spl),
% 0.11/0.70 inference(resolution,[status(thm)],[f618,f35])).
% 0.11/0.70 fof(f1302,plain,(
% 1.53/0.70 ~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)))|~sQ14_spl|~sQ6_spl),
% 1.53/0.70 inference(resolution,[status(thm)],[f618,f33])).
% 1.53/0.70 fof(f1303,plain,(
% 1.53/0.70 ~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)|~sQ14_spl|~sQ6_spl),
% 1.53/0.70 inference(resolution,[status(thm)],[f618,f31])).
% 1.53/0.70 fof(f1304,plain,(
% 1.53/0.70 ~environment(sk3)|~stable(sk3)|~greater_or_equal(sk2(sk3),sk1(sk3))|greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))|~sQ14_spl|~sQ6_spl),
% 1.53/0.70 inference(resolution,[status(thm)],[f618,f48])).
% 1.53/0.70 fof(f1305,definition,(
% 1.53/0.70 sQ63_spl <=> (growth_rate(efficient_producers,sk2(sk3))=zero)),
% 1.53/0.70 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 1.53/0.70 fof(f1308,definition,(
% 1.53/0.70 sQ64_spl <=> (greater(zero,growth_rate(efficient_producers,sk2(sk3))))),
% 1.53/0.70 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 1.53/0.70 fof(f1311,definition,(
% 1.53/0.70 sQ65_spl <=> (greater(zero,growth_rate(first_movers,sk2(sk3))))),
% 1.53/0.70 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 1.53/0.70 fof(f1312,plain,(
% 1.53/0.70 greater(zero,growth_rate(first_movers,sk2(sk3)))|~sQ65_spl),
% 1.53/0.70 inference(component_clause,[status(thm)],[f1311])).
% 1.53/0.70 fof(f1314,plain,(
% 1.53/0.70 ~sQ17_spl|~sQ7_spl|sQ63_spl|sQ64_spl|sQ65_spl|~sQ14_spl|~sQ6_spl),
% 1.53/0.70 inference(split_clause,[status(thm)],[f1296,f155,f97,f1305,f1308,f1311,f135,f92])).
% 1.53/0.70 fof(f1315,plain,(
% 1.53/0.70 ~sQ17_spl|~sQ7_spl|sQ63_spl|sQ64_spl|sQ15_spl|~sQ14_spl|~sQ6_spl),
% 1.53/0.70 inference(split_clause,[status(thm)],[f1297,f155,f97,f1305,f1308,f143,f135,f92])).
% 1.53/0.70 fof(f1316,definition,(
% 1.53/0.70 sQ66_spl <=> (greater(growth_rate(first_movers,sk2(sk3)),zero))),
% 1.53/0.70 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 1.53/0.70 fof(f1319,plain,(
% 1.53/0.70 ~sQ17_spl|~sQ7_spl|sQ63_spl|sQ66_spl|sQ65_spl|~sQ14_spl|~sQ6_spl),
% 1.53/0.70 inference(split_clause,[status(thm)],[f1298,f155,f97,f1305,f1316,f1311,f135,f92])).
% 1.53/0.70 fof(f1320,plain,(
% 1.53/0.70 ~sQ17_spl|~sQ7_spl|sQ63_spl|sQ66_spl|sQ15_spl|~sQ14_spl|~sQ6_spl),
% 1.53/0.70 inference(split_clause,[status(thm)],[f1299,f155,f97,f1305,f1316,f143,f135,f92])).
% 1.53/0.70 fof(f1321,definition,(
% 1.53/0.70 sQ67_spl <=> (growth_rate(first_movers,sk2(sk3))=zero)),
% 1.53/0.70 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 1.53/0.70 fof(f1322,plain,(
% 1.53/0.70 growth_rate(first_movers,sk2(sk3))=zero|~sQ67_spl),
% 1.53/0.70 inference(component_clause,[status(thm)],[f1321])).
% 1.53/0.70 fof(f1324,plain,(
% 1.53/0.70 ~sQ17_spl|~sQ7_spl|sQ67_spl|sQ64_spl|sQ65_spl|~sQ14_spl|~sQ6_spl),
% 1.53/0.70 inference(split_clause,[status(thm)],[f1300,f155,f97,f1321,f1308,f1311,f135,f92])).
% 1.53/0.70 fof(f1325,plain,(
% 1.53/0.70 ~sQ17_spl|~sQ7_spl|sQ67_spl|sQ64_spl|sQ15_spl|~sQ14_spl|~sQ6_spl),
% 1.53/0.70 inference(split_clause,[status(thm)],[f1301,f155,f97,f1321,f1308,f143,f135,f92])).
% 1.53/0.70 fof(f1326,plain,(
% 1.53/0.70 ~sQ17_spl|~sQ7_spl|sQ67_spl|sQ66_spl|sQ65_spl|~sQ14_spl|~sQ6_spl),
% 1.53/0.70 inference(split_clause,[status(thm)],[f1302,f155,f97,f1321,f1316,f1311,f135,f92])).
% 1.53/0.70 fof(f1327,plain,(
% 1.53/0.70 ~sQ17_spl|~sQ7_spl|sQ67_spl|sQ66_spl|sQ15_spl|~sQ14_spl|~sQ6_spl),
% 1.53/0.70 inference(split_clause,[status(thm)],[f1303,f155,f97,f1321,f1316,f143,f135,f92])).
% 1.53/0.70 fof(f1328,definition,(
% 1.53/0.70 sQ68_spl <=> (greater_or_equal(sk2(sk3),sk1(sk3)))),
% 1.53/0.70 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 1.53/0.70 fof(f1330,plain,(
% 1.53/0.70 ~greater_or_equal(sk2(sk3),sk1(sk3))|sQ68_spl),
% 1.53/0.70 inference(component_clause,[status(thm)],[f1328])).
% 1.53/0.70 fof(f1331,definition,(
% 1.53/0.70 sQ69_spl <=> (greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3))))),
% 1.53/0.70 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 1.53/0.70 fof(f1332,plain,(
% 1.53/0.70 greater(growth_rate(efficient_producers,sk2(sk3)),growth_rate(first_movers,sk2(sk3)))|~sQ69_spl),
% 1.53/0.70 inference(component_clause,[status(thm)],[f1331])).
% 1.53/0.70 fof(f1334,plain,(
% 1.53/0.70 ~sQ17_spl|~sQ0_spl|~sQ68_spl|sQ69_spl|~sQ14_spl|~sQ6_spl),
% 1.53/0.70 inference(split_clause,[status(thm)],[f1304,f155,f59,f1328,f1331,f135,f92])).
% 1.53/0.70 fof(f1350,plain,(
% 1.53/0.70 ~greater(zero,zero)|~sQ67_spl|~sQ14_spl|sQ16_spl),
% 1.53/0.70 inference(backward_demodulation,[status(thm)],[f1322,f620])).
% 1.53/0.70 fof(f1359,plain,(
% 1.53/0.70 ~sQ59_spl|~sQ67_spl|~sQ14_spl|sQ16_spl),
% 1.53/0.70 inference(split_clause,[status(thm)],[f1350,f1158,f1321,f135,f146])).
% 1.53/0.70 fof(f1362,plain,(
% 1.53/0.70 greater(growth_rate(efficient_producers,sk2(sk3)),zero)|~sQ67_spl|~sQ69_spl),
% 1.53/0.70 inference(forward_demodulation,[status(thm)],[f1322,f1332])).
% 1.53/0.70 fof(f1363,plain,(
% 1.53/0.70 $false|~sQ14_spl|sQ34_spl|~sQ67_spl|~sQ69_spl),
% 1.53/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1362,f1253])).
% 1.53/0.70 fof(f1364,plain,(
% 1.53/0.70 ~sQ14_spl|sQ34_spl|~sQ67_spl|~sQ69_spl),
% 1.53/0.70 inference(contradiction_clause,[status(thm)],[f1363])).
% 1.53/0.70 fof(f1365,plain,(
% 1.53/0.70 $false|~sQ14_spl|sQ16_spl|~sQ65_spl),
% 1.53/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1312,f620])).
% 1.53/0.70 fof(f1366,plain,(
% 1.53/0.70 ~sQ14_spl|sQ16_spl|~sQ65_spl),
% 1.53/0.70 inference(contradiction_clause,[status(thm)],[f1365])).
% 1.53/0.70 fof(f1497,plain,(
% 1.53/0.70 greater(zero,growth_rate(first_movers,sk4(sk1(sk3))))|~sQ19_spl|~sQ25_spl),
% 1.53/0.70 inference(resolution,[status(thm)],[f1022,f196])).
% 1.53/0.70 fof(f1498,plain,(
% 1.53/0.70 sQ24_spl|~sQ19_spl|~sQ25_spl),
% 1.53/0.70 inference(split_clause,[status(thm)],[f1497,f189,f161,f195])).
% 1.53/0.70 fof(f1510,plain,(
% 1.53/0.70 ~sQ41_spl|~sQ3_spl|sQ20_spl),
% 1.53/0.70 inference(split_clause,[status(thm)],[f246,f512,f75,f172])).
% 1.53/0.70 fof(f1511,plain,(
% 1.53/0.70 sQ20_spl|~sQ55_spl),
% 1.53/0.70 inference(split_clause,[status(thm)],[f1290,f172,f879])).
% 1.53/0.70 fof(f1522,plain,(
% 1.53/0.70 ~greater(sk1(sk3),sk2(sk3))|~sQ3_spl|sQ38_spl),
% 1.53/0.70 inference(forward_demodulation,[status(thm)],[f76,f363])).
% 1.53/0.70 fof(f1523,plain,(
% 1.53/0.70 $false|~sQ8_spl|~sQ3_spl|sQ38_spl),
% 1.53/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1522,f106])).
% 1.53/0.70 fof(f1524,plain,(
% 1.53/0.70 ~sQ8_spl|~sQ3_spl|sQ38_spl),
% 1.53/0.70 inference(contradiction_clause,[status(thm)],[f1523])).
% 1.53/0.70 fof(f1581,plain,(
% 1.53/0.70 ~greater_or_equal(sk2(sk3),sk2(sk3))|~sQ39_spl|~sQ12_spl|sQ20_spl),
% 1.53/0.70 inference(forward_demodulation,[status(thm)],[f365,f187])).
% 1.53/0.70 fof(f1582,plain,(
% 1.53/0.70 $false|~sQ39_spl|~sQ12_spl|sQ20_spl),
% 1.53/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1581,f56])).
% 1.53/0.70 fof(f1583,plain,(
% 1.53/0.70 ~sQ39_spl|~sQ12_spl|sQ20_spl),
% 1.53/0.70 inference(contradiction_clause,[status(thm)],[f1582])).
% 1.53/0.70 fof(f1590,plain,(
% 1.53/0.70 ~greater_or_equal(sk4(sk1(sk3)),sk2(sk3))|~sQ12_spl|sQ20_spl),
% 1.53/0.70 inference(forward_demodulation,[status(thm)],[f120,f174])).
% 1.53/0.70 fof(f1592,plain,(
% 1.53/0.70 $false|~sQ12_spl|sQ20_spl|~sQ8_spl|~sQ2_spl),
% 1.53/0.70 inference(forward_subsumption_resolution,[status(thm)],[f358,f1590])).
% 1.53/0.70 fof(f1593,plain,(
% 1.53/0.70 ~sQ12_spl|sQ20_spl|~sQ8_spl|~sQ2_spl),
% 1.53/0.70 inference(contradiction_clause,[status(thm)],[f1592])).
% 1.53/0.70 fof(f1594,plain,(
% 1.53/0.70 $false|~sQ12_spl|sQ20_spl|~sQ38_spl),
% 1.53/0.70 inference(forward_subsumption_resolution,[status(thm)],[f501,f1590])).
% 1.53/0.70 fof(f1595,plain,(
% 1.53/0.70 ~sQ12_spl|sQ20_spl|~sQ38_spl),
% 1.53/0.70 inference(contradiction_clause,[status(thm)],[f1594])).
% 1.53/0.70 fof(f1600,plain,(
% 1.53/0.70 $false|~sQ10_spl|sQ68_spl),
% 1.53/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1330,f125])).
% 1.53/0.70 fof(f1601,plain,(
% 1.53/0.70 ~sQ10_spl|sQ68_spl),
% 1.53/0.70 inference(contradiction_clause,[status(thm)],[f1600])).
% 1.53/0.70 fof(f1602,plain,(
% 1.53/0.70 ~greater_or_equal(sk4(sk2(sk3)),sk2(sk3))|~sQ12_spl|sQ31_spl),
% 1.53/0.70 inference(forward_demodulation,[status(thm)],[f120,f287])).
% 1.53/0.70 fof(f1603,plain,(
% 1.53/0.70 $false|~sQ6_spl|~sQ12_spl|sQ31_spl),
% 1.53/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1602,f459])).
% 1.53/0.70 fof(f1604,plain,(
% 1.53/0.70 ~sQ6_spl|~sQ12_spl|sQ31_spl),
% 1.53/0.70 inference(contradiction_clause,[status(thm)],[f1603])).
% 1.53/0.70 fof(f1605,plain,(
% 1.53/0.70 $false),
% 1.53/0.70 inference(sat_refutation,[status(thm)],[f65,f67,f78,f88,f95,f100,f114,f122,f138,f149,f164,f166,f168,f184,f210,f226,f258,f297,f301,f302,f309,f312,f326,f328,f329,f332,f340,f367,f408,f415,f416,f417,f419,f431,f448,f469,f477,f494,f495,f496,f542,f544,f556,f577,f580,f590,f626,f628,f630,f649,f676,f679,f691,f721,f742,f743,f744,f745,f746,f771,f785,f821,f856,f875,f885,f899,f900,f966,f975,f976,f978,f1033,f1074,f1075,f1151,f1161,f1314,f1315,f1319,f1320,f1324,f1325,f1326,f1327,f1334,f1359,f1364,f1366,f1498,f1510,f1511,f1524,f1583,f1593,f1595,f1601,f1604])).
% 1.53/0.70 % SZS output end CNFRefutation for theBenchmark.p
% 1.53/0.71 % Elapsed time: 0.353629 seconds
% 1.53/0.71 % CPU time: 2.521995 seconds
% 1.53/0.71 % Total memory used: 99.833 MB
% 1.53/0.71 % Net memory used: 97.709 MB
%------------------------------------------------------------------------------