%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT030-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 : n018.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.15s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT030-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.38 % Computer : n018.cluster.edu
% 0.15/0.38 % Model : x86_64 x86_64
% 0.15/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.38 % Memory : 8046.5625MB
% 0.15/0.38 % OS : Linux 6.8.0-71-generic
% 0.15/0.38 % CPULimit : 300
% 0.15/0.38 % WCLimit : 300
% 0.15/0.38 % DateTime : Mon Sep 21 01:24:13 UTC 2026
% 0.15/0.39 % CPUTime :
% 0.15/0.40 % Drodi V4.1.1
% 0.15/0.40 % Refutation found
% 0.15/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.40 fof(f1,axiom,(
% 0.15/0.40 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| subpopulations(first_movers,efficient_producers,A,sk1(B,A))| in_environment(A,sk2(A)) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f2,axiom,(
% 0.15/0.40 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| greater_or_equal(sk1(B,A),B)| in_environment(A,sk2(A)) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f3,axiom,(
% 0.15/0.40 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| subpopulations(first_movers,efficient_producers,A,sk1(B,A))| ~ greater(growth_rate(efficient_producers,sk2(A)),growth_rate(first_movers,sk2(A))) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f4,axiom,(
% 0.15/0.40 (![A,B,C]: (( ~ environment(A)| ~ in_environment(A,B)| subpopulations(first_movers,efficient_producers,A,sk1(B,A))| ~ subpopulations(first_movers,efficient_producers,A,C)| ~ greater(C,sk2(A))| greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C)) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f5,axiom,(
% 0.15/0.40 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| greater_or_equal(sk1(B,A),B)| ~ greater(growth_rate(efficient_producers,sk2(A)),growth_rate(first_movers,sk2(A))) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f6,axiom,(
% 0.15/0.40 (![A,B,C]: (( ~ environment(A)| ~ in_environment(A,B)| greater_or_equal(sk1(B,A),B)| ~ subpopulations(first_movers,efficient_producers,A,C)| ~ greater(C,sk2(A))| greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C)) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f7,axiom,(
% 0.15/0.40 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| ~ greater(growth_rate(efficient_producers,sk1(B,A)),growth_rate(first_movers,sk1(B,A)))| in_environment(A,sk2(A)) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f8,axiom,(
% 0.15/0.40 (![A,B]: (( ~ environment(A)| ~ in_environment(A,B)| ~ greater(growth_rate(efficient_producers,sk1(B,A)),growth_rate(first_movers,sk1(B,A)))| ~ greater(growth_rate(efficient_producers,sk2(A)),growth_rate(first_movers,sk2(A))) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f9,axiom,(
% 0.15/0.40 (![A,B,C]: (( ~ environment(A)| ~ in_environment(A,B)| ~ greater(growth_rate(efficient_producers,sk1(B,A)),growth_rate(first_movers,sk1(B,A)))| ~ subpopulations(first_movers,efficient_producers,A,C)| ~ greater(C,sk2(A))| greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C)) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f10,hypothesis,(
% 0.15/0.40 (![A]: (( ~ environment(A)| ~ stable(A)| in_environment(A,sk3(A)) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f11,hypothesis,(
% 0.15/0.40 (![A,B]: (( ~ environment(A)| ~ stable(A)| ~ subpopulations(first_movers,efficient_producers,A,B)| ~ greater_or_equal(B,sk3(A))| greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B)) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f12,negated_conjecture,(
% 0.15/0.40 environment(sk4) ),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f13,negated_conjecture,(
% 0.15/0.40 stable(sk4) ),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f14,negated_conjecture,(
% 0.15/0.40 (![A]: (( ~ in_environment(sk4,A)| greater(growth_rate(efficient_producers,A),growth_rate(first_movers,A))| subpopulations(first_movers,efficient_producers,sk4,sk5(A)) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f15,negated_conjecture,(
% 0.15/0.40 (![A]: (( ~ in_environment(sk4,A)| greater(growth_rate(efficient_producers,A),growth_rate(first_movers,A))| greater(sk5(A),A) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f16,negated_conjecture,(
% 0.15/0.40 (![A]: (( ~ in_environment(sk4,A)| greater(growth_rate(efficient_producers,A),growth_rate(first_movers,A))| ~ greater(growth_rate(efficient_producers,sk5(A)),growth_rate(first_movers,sk5(A))) ) ))),
% 0.15/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.40 fof(f17,plain,(
% 0.15/0.40 ![A]: ((![B]: ((~environment(A)|~in_environment(A,B))|subpopulations(first_movers,efficient_producers,A,sk1(B,A))))|in_environment(A,sk2(A)))),
% 0.15/0.40 inference(miniscoping,[status(thm)],[f1])).
% 0.15/0.40 fof(f18,plain,(
% 0.15/0.40 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|subpopulations(first_movers,efficient_producers,X0,sk1(X1,X0))|in_environment(X0,sk2(X0)))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f17])).
% 0.15/0.40 fof(f19,plain,(
% 0.15/0.40 ![A]: ((![B]: ((~environment(A)|~in_environment(A,B))|greater_or_equal(sk1(B,A),B)))|in_environment(A,sk2(A)))),
% 0.15/0.40 inference(miniscoping,[status(thm)],[f2])).
% 0.15/0.40 fof(f20,plain,(
% 0.15/0.40 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|greater_or_equal(sk1(X1,X0),X1)|in_environment(X0,sk2(X0)))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f19])).
% 0.15/0.40 fof(f21,plain,(
% 0.15/0.40 ![A]: ((![B]: ((~environment(A)|~in_environment(A,B))|subpopulations(first_movers,efficient_producers,A,sk1(B,A))))|~greater(growth_rate(efficient_producers,sk2(A)),growth_rate(first_movers,sk2(A))))),
% 0.15/0.40 inference(miniscoping,[status(thm)],[f3])).
% 0.15/0.40 fof(f22,plain,(
% 0.15/0.40 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|subpopulations(first_movers,efficient_producers,X0,sk1(X1,X0))|~greater(growth_rate(efficient_producers,sk2(X0)),growth_rate(first_movers,sk2(X0))))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f21])).
% 0.15/0.40 fof(f23,plain,(
% 0.15/0.40 ![C]: ((![A]: (((![B]: ((~environment(A)|~in_environment(A,B))|subpopulations(first_movers,efficient_producers,A,sk1(B,A))))|~subpopulations(first_movers,efficient_producers,A,C))|~greater(C,sk2(A))))|greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C)))),
% 0.15/0.40 inference(miniscoping,[status(thm)],[f4])).
% 0.15/0.40 fof(f24,plain,(
% 0.15/0.40 ![X0,X1,X2]: (~environment(X0)|~in_environment(X0,X1)|subpopulations(first_movers,efficient_producers,X0,sk1(X1,X0))|~subpopulations(first_movers,efficient_producers,X0,X2)|~greater(X2,sk2(X0))|greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f23])).
% 0.15/0.40 fof(f25,plain,(
% 0.15/0.40 ![A]: ((![B]: ((~environment(A)|~in_environment(A,B))|greater_or_equal(sk1(B,A),B)))|~greater(growth_rate(efficient_producers,sk2(A)),growth_rate(first_movers,sk2(A))))),
% 0.15/0.40 inference(miniscoping,[status(thm)],[f5])).
% 0.15/0.40 fof(f26,plain,(
% 0.15/0.40 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|greater_or_equal(sk1(X1,X0),X1)|~greater(growth_rate(efficient_producers,sk2(X0)),growth_rate(first_movers,sk2(X0))))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f25])).
% 0.15/0.40 fof(f27,plain,(
% 0.15/0.40 ![C]: ((![A]: (((![B]: ((~environment(A)|~in_environment(A,B))|greater_or_equal(sk1(B,A),B)))|~subpopulations(first_movers,efficient_producers,A,C))|~greater(C,sk2(A))))|greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C)))),
% 0.15/0.40 inference(miniscoping,[status(thm)],[f6])).
% 0.15/0.40 fof(f28,plain,(
% 0.15/0.40 ![X0,X1,X2]: (~environment(X0)|~in_environment(X0,X1)|greater_or_equal(sk1(X1,X0),X1)|~subpopulations(first_movers,efficient_producers,X0,X2)|~greater(X2,sk2(X0))|greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f27])).
% 0.15/0.40 fof(f29,plain,(
% 0.15/0.40 ![A]: ((![B]: ((~environment(A)|~in_environment(A,B))|~greater(growth_rate(efficient_producers,sk1(B,A)),growth_rate(first_movers,sk1(B,A)))))|in_environment(A,sk2(A)))),
% 0.15/0.40 inference(miniscoping,[status(thm)],[f7])).
% 0.15/0.40 fof(f30,plain,(
% 0.15/0.40 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|~greater(growth_rate(efficient_producers,sk1(X1,X0)),growth_rate(first_movers,sk1(X1,X0)))|in_environment(X0,sk2(X0)))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f29])).
% 0.15/0.40 fof(f31,plain,(
% 0.15/0.40 ![A]: ((![B]: ((~environment(A)|~in_environment(A,B))|~greater(growth_rate(efficient_producers,sk1(B,A)),growth_rate(first_movers,sk1(B,A)))))|~greater(growth_rate(efficient_producers,sk2(A)),growth_rate(first_movers,sk2(A))))),
% 0.15/0.40 inference(miniscoping,[status(thm)],[f8])).
% 0.15/0.40 fof(f32,plain,(
% 0.15/0.40 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|~greater(growth_rate(efficient_producers,sk1(X1,X0)),growth_rate(first_movers,sk1(X1,X0)))|~greater(growth_rate(efficient_producers,sk2(X0)),growth_rate(first_movers,sk2(X0))))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f31])).
% 0.15/0.40 fof(f33,plain,(
% 0.15/0.40 ![C]: ((![A]: (((![B]: ((~environment(A)|~in_environment(A,B))|~greater(growth_rate(efficient_producers,sk1(B,A)),growth_rate(first_movers,sk1(B,A)))))|~subpopulations(first_movers,efficient_producers,A,C))|~greater(C,sk2(A))))|greater(growth_rate(efficient_producers,C),growth_rate(first_movers,C)))),
% 0.15/0.40 inference(miniscoping,[status(thm)],[f9])).
% 0.15/0.40 fof(f34,plain,(
% 0.15/0.40 ![X0,X1,X2]: (~environment(X0)|~in_environment(X0,X1)|~greater(growth_rate(efficient_producers,sk1(X1,X0)),growth_rate(first_movers,sk1(X1,X0)))|~subpopulations(first_movers,efficient_producers,X0,X2)|~greater(X2,sk2(X0))|greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f33])).
% 0.15/0.40 fof(f35,plain,(
% 0.15/0.40 ![X0]: (~environment(X0)|~stable(X0)|in_environment(X0,sk3(X0)))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f10])).
% 0.15/0.40 fof(f36,plain,(
% 0.15/0.40 ![B]: ((![A]: (((~environment(A)|~stable(A))|~subpopulations(first_movers,efficient_producers,A,B))|~greater_or_equal(B,sk3(A))))|greater(growth_rate(efficient_producers,B),growth_rate(first_movers,B)))),
% 0.15/0.40 inference(miniscoping,[status(thm)],[f11])).
% 0.15/0.40 fof(f37,plain,(
% 0.15/0.40 ![X0,X1]: (~environment(X0)|~stable(X0)|~subpopulations(first_movers,efficient_producers,X0,X1)|~greater_or_equal(X1,sk3(X0))|greater(growth_rate(efficient_producers,X1),growth_rate(first_movers,X1)))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f36])).
% 0.15/0.40 fof(f38,plain,(
% 0.15/0.40 environment(sk4)),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.15/0.40 fof(f39,plain,(
% 0.15/0.40 stable(sk4)),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f13])).
% 0.15/0.40 fof(f40,plain,(
% 0.15/0.40 ![X0]: (~in_environment(sk4,X0)|greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))|subpopulations(first_movers,efficient_producers,sk4,sk5(X0)))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f14])).
% 0.15/0.40 fof(f41,plain,(
% 0.15/0.40 ![X0]: (~in_environment(sk4,X0)|greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))|greater(sk5(X0),X0))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f15])).
% 0.15/0.40 fof(f42,plain,(
% 0.15/0.40 ![X0]: (~in_environment(sk4,X0)|greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0))|~greater(growth_rate(efficient_producers,sk5(X0)),growth_rate(first_movers,sk5(X0))))),
% 0.15/0.40 inference(cnf_transformation,[status(thm)],[f16])).
% 0.15/0.40 fof(f43,plain,(
% 0.15/0.40 ~environment(sk4)|in_environment(sk4,sk3(sk4))),
% 0.15/0.40 inference(resolution,[status(thm)],[f35,f39])).
% 0.15/0.40 fof(f44,definition,(
% 0.15/0.40 sQ0_spl <=> (environment(sk4))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f46,plain,(
% 0.15/0.40 ~environment(sk4)|sQ0_spl),
% 0.15/0.40 inference(component_clause,[status(thm)],[f44])).
% 0.15/0.40 fof(f47,definition,(
% 0.15/0.40 sQ1_spl <=> (in_environment(sk4,sk3(sk4)))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f48,plain,(
% 0.15/0.40 in_environment(sk4,sk3(sk4))|~sQ1_spl),
% 0.15/0.40 inference(component_clause,[status(thm)],[f47])).
% 0.15/0.40 fof(f50,plain,(
% 0.15/0.40 ~sQ0_spl|sQ1_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f43,f44,f47])).
% 0.15/0.40 fof(f51,plain,(
% 0.15/0.40 $false|sQ0_spl),
% 0.15/0.40 inference(forward_subsumption_resolution,[status(thm)],[f46,f38])).
% 0.15/0.40 fof(f52,plain,(
% 0.15/0.40 sQ0_spl),
% 0.15/0.40 inference(contradiction_clause,[status(thm)],[f51])).
% 0.15/0.40 fof(f53,plain,(
% 0.15/0.40 greater(growth_rate(efficient_producers,sk3(sk4)),growth_rate(first_movers,sk3(sk4)))|~greater(growth_rate(efficient_producers,sk5(sk3(sk4))),growth_rate(first_movers,sk5(sk3(sk4))))|~sQ1_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f48,f42])).
% 0.15/0.40 fof(f54,plain,(
% 0.15/0.40 ~environment(sk4)|greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))|in_environment(sk4,sk2(sk4))|~sQ1_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f48,f20])).
% 0.15/0.40 fof(f55,plain,(
% 0.15/0.40 ~environment(sk4)|~greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))|~greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|~sQ1_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f48,f32])).
% 0.15/0.40 fof(f56,plain,(
% 0.15/0.40 ~environment(sk4)|~greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))|in_environment(sk4,sk2(sk4))|~sQ1_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f48,f30])).
% 0.15/0.40 fof(f57,definition,(
% 0.15/0.40 sQ2_spl <=> (greater(growth_rate(efficient_producers,sk3(sk4)),growth_rate(first_movers,sk3(sk4))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f60,definition,(
% 0.15/0.40 sQ3_spl <=> (greater(growth_rate(efficient_producers,sk5(sk3(sk4))),growth_rate(first_movers,sk5(sk3(sk4)))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f62,plain,(
% 0.15/0.40 ~greater(growth_rate(efficient_producers,sk5(sk3(sk4))),growth_rate(first_movers,sk5(sk3(sk4))))|sQ3_spl),
% 0.15/0.40 inference(component_clause,[status(thm)],[f60])).
% 0.15/0.40 fof(f63,plain,(
% 0.15/0.40 sQ2_spl|~sQ3_spl|~sQ1_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f53,f57,f60,f47])).
% 0.15/0.40 fof(f64,definition,(
% 0.15/0.40 sQ4_spl <=> (greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4)))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f65,plain,(
% 0.15/0.40 greater_or_equal(sk1(sk3(sk4),sk4),sk3(sk4))|~sQ4_spl),
% 0.15/0.40 inference(component_clause,[status(thm)],[f64])).
% 0.15/0.40 fof(f67,definition,(
% 0.15/0.40 sQ5_spl <=> (in_environment(sk4,sk2(sk4)))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f68,plain,(
% 0.15/0.40 in_environment(sk4,sk2(sk4))|~sQ5_spl),
% 0.15/0.40 inference(component_clause,[status(thm)],[f67])).
% 0.15/0.40 fof(f70,plain,(
% 0.15/0.40 ~sQ0_spl|sQ4_spl|sQ5_spl|~sQ1_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f54,f44,f64,f67,f47])).
% 0.15/0.40 fof(f71,definition,(
% 0.15/0.40 sQ6_spl <=> (greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f73,plain,(
% 0.15/0.40 ~greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))|sQ6_spl),
% 0.15/0.40 inference(component_clause,[status(thm)],[f71])).
% 0.15/0.40 fof(f74,definition,(
% 0.15/0.40 sQ7_spl <=> (greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f76,plain,(
% 0.15/0.40 ~greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|sQ7_spl),
% 0.15/0.40 inference(component_clause,[status(thm)],[f74])).
% 0.15/0.40 fof(f77,plain,(
% 0.15/0.40 ~sQ0_spl|~sQ6_spl|~sQ7_spl|~sQ1_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f55,f44,f71,f74,f47])).
% 0.15/0.40 fof(f78,plain,(
% 0.15/0.40 ~sQ0_spl|~sQ6_spl|sQ5_spl|~sQ1_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f56,f44,f71,f67,f47])).
% 0.15/0.40 fof(f79,plain,(
% 0.15/0.40 greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|~greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))|~sQ5_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f68,f42])).
% 0.15/0.40 fof(f81,plain,(
% 0.15/0.40 ~environment(sk4)|~greater(growth_rate(efficient_producers,sk1(sk2(sk4),sk4)),growth_rate(first_movers,sk1(sk2(sk4),sk4)))|~greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|~sQ5_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f68,f32])).
% 0.15/0.40 fof(f83,definition,(
% 0.15/0.40 sQ8_spl <=> (greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4)))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f85,plain,(
% 0.15/0.40 ~greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))|sQ8_spl),
% 0.15/0.40 inference(component_clause,[status(thm)],[f83])).
% 0.15/0.40 fof(f86,plain,(
% 0.15/0.40 sQ7_spl|~sQ8_spl|~sQ5_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f79,f74,f83,f67])).
% 0.15/0.40 fof(f91,definition,(
% 0.15/0.40 sQ10_spl <=> (greater(growth_rate(efficient_producers,sk1(sk2(sk4),sk4)),growth_rate(first_movers,sk1(sk2(sk4),sk4))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f93,plain,(
% 0.15/0.40 ~greater(growth_rate(efficient_producers,sk1(sk2(sk4),sk4)),growth_rate(first_movers,sk1(sk2(sk4),sk4)))|sQ10_spl),
% 0.15/0.40 inference(component_clause,[status(thm)],[f91])).
% 0.15/0.40 fof(f94,plain,(
% 0.15/0.40 ~sQ0_spl|~sQ10_spl|~sQ7_spl|~sQ5_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f81,f44,f91,f74,f67])).
% 0.15/0.40 fof(f96,plain,(
% 0.15/0.40 ![X0,X1]: (~environment(X0)|~in_environment(X0,X1)|~greater(growth_rate(efficient_producers,sk1(X1,X0)),growth_rate(first_movers,sk1(X1,X0)))|~subpopulations(first_movers,efficient_producers,X0,sk5(sk2(sk4)))|~greater(sk5(sk2(sk4)),sk2(X0))|sQ8_spl)),
% 0.15/0.40 inference(resolution,[status(thm)],[f85,f34])).
% 0.15/0.40 fof(f97,plain,(
% 0.15/0.40 ~in_environment(sk4,sk5(sk2(sk4)))|subpopulations(first_movers,efficient_producers,sk4,sk5(sk5(sk2(sk4))))|sQ8_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f85,f40])).
% 0.15/0.40 fof(f98,plain,(
% 0.15/0.40 ~in_environment(sk4,sk5(sk2(sk4)))|greater(sk5(sk5(sk2(sk4))),sk5(sk2(sk4)))|sQ8_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f85,f41])).
% 0.15/0.40 fof(f99,definition,(
% 0.15/0.40 sQ11_spl <=> (in_environment(sk4,sk5(sk2(sk4))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f102,definition,(
% 0.15/0.40 sQ12_spl <=> (subpopulations(first_movers,efficient_producers,sk4,sk5(sk5(sk2(sk4)))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f105,plain,(
% 0.15/0.40 ~sQ11_spl|sQ12_spl|sQ8_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f97,f99,f102,f83])).
% 0.15/0.40 fof(f106,definition,(
% 0.15/0.40 sQ13_spl <=> (greater(sk5(sk5(sk2(sk4))),sk5(sk2(sk4))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f109,plain,(
% 0.15/0.40 ~sQ11_spl|sQ13_spl|sQ8_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f98,f99,f106,f83])).
% 0.15/0.40 fof(f112,plain,(
% 0.15/0.40 ~in_environment(sk4,sk5(sk3(sk4)))|subpopulations(first_movers,efficient_producers,sk4,sk5(sk5(sk3(sk4))))|sQ3_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f62,f40])).
% 0.15/0.40 fof(f113,plain,(
% 0.15/0.40 ~in_environment(sk4,sk5(sk3(sk4)))|greater(sk5(sk5(sk3(sk4))),sk5(sk3(sk4)))|sQ3_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f62,f41])).
% 0.15/0.40 fof(f114,definition,(
% 0.15/0.40 sQ14_spl <=> (in_environment(sk4,sk5(sk3(sk4))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f117,definition,(
% 0.15/0.40 sQ15_spl <=> (subpopulations(first_movers,efficient_producers,sk4,sk5(sk5(sk3(sk4)))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f120,plain,(
% 0.15/0.40 ~sQ14_spl|sQ15_spl|sQ3_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f112,f114,f117,f60])).
% 0.15/0.40 fof(f121,definition,(
% 0.15/0.40 sQ16_spl <=> (greater(sk5(sk5(sk3(sk4))),sk5(sk3(sk4))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f124,plain,(
% 0.15/0.40 ~sQ14_spl|sQ16_spl|sQ3_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f113,f114,f121,f60])).
% 0.15/0.40 fof(f125,plain,(
% 0.15/0.40 ![X0]: (~environment(X0)|~stable(X0)|~subpopulations(first_movers,efficient_producers,X0,sk1(sk3(sk4),sk4))|~greater_or_equal(sk1(sk3(sk4),sk4),sk3(X0))|sQ6_spl)),
% 0.15/0.40 inference(resolution,[status(thm)],[f73,f37])).
% 0.15/0.40 fof(f127,plain,(
% 0.15/0.40 ~in_environment(sk4,sk1(sk3(sk4),sk4))|subpopulations(first_movers,efficient_producers,sk4,sk5(sk1(sk3(sk4),sk4)))|sQ6_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f73,f40])).
% 0.15/0.40 fof(f128,plain,(
% 0.15/0.40 ~in_environment(sk4,sk1(sk3(sk4),sk4))|greater(sk5(sk1(sk3(sk4),sk4)),sk1(sk3(sk4),sk4))|sQ6_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f73,f41])).
% 0.15/0.40 fof(f129,definition,(
% 0.15/0.40 sQ17_spl <=> (in_environment(sk4,sk1(sk3(sk4),sk4)))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f132,definition,(
% 0.15/0.40 sQ18_spl <=> (subpopulations(first_movers,efficient_producers,sk4,sk5(sk1(sk3(sk4),sk4))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f135,plain,(
% 0.15/0.40 ~sQ17_spl|sQ18_spl|sQ6_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f127,f129,f132,f71])).
% 0.15/0.40 fof(f136,definition,(
% 0.15/0.40 sQ19_spl <=> (greater(sk5(sk1(sk3(sk4),sk4)),sk1(sk3(sk4),sk4)))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f139,plain,(
% 0.15/0.40 ~sQ17_spl|sQ19_spl|sQ6_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f128,f129,f136,f71])).
% 0.15/0.40 fof(f142,plain,(
% 0.15/0.40 ~in_environment(sk4,sk2(sk4))|subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))|sQ7_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f76,f40])).
% 0.15/0.40 fof(f143,plain,(
% 0.15/0.40 ~in_environment(sk4,sk2(sk4))|greater(sk5(sk2(sk4)),sk2(sk4))|sQ7_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f76,f41])).
% 0.15/0.40 fof(f144,definition,(
% 0.15/0.40 sQ20_spl <=> (subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f147,plain,(
% 0.15/0.40 ~sQ5_spl|sQ20_spl|sQ7_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f142,f67,f144,f74])).
% 0.15/0.40 fof(f148,definition,(
% 0.15/0.40 sQ21_spl <=> (greater(sk5(sk2(sk4)),sk2(sk4)))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f149,plain,(
% 0.15/0.40 greater(sk5(sk2(sk4)),sk2(sk4))|~sQ21_spl),
% 0.15/0.40 inference(component_clause,[status(thm)],[f148])).
% 0.15/0.40 fof(f151,plain,(
% 0.15/0.40 ~sQ5_spl|sQ21_spl|sQ7_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f143,f67,f148,f74])).
% 0.15/0.40 fof(f162,plain,(
% 0.15/0.40 ~in_environment(sk4,sk1(sk2(sk4),sk4))|subpopulations(first_movers,efficient_producers,sk4,sk5(sk1(sk2(sk4),sk4)))|sQ10_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f93,f40])).
% 0.15/0.40 fof(f163,plain,(
% 0.15/0.40 ~in_environment(sk4,sk1(sk2(sk4),sk4))|greater(sk5(sk1(sk2(sk4),sk4)),sk1(sk2(sk4),sk4))|sQ10_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f93,f41])).
% 0.15/0.40 fof(f164,definition,(
% 0.15/0.40 sQ22_spl <=> (in_environment(sk4,sk1(sk2(sk4),sk4)))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f167,definition,(
% 0.15/0.40 sQ23_spl <=> (subpopulations(first_movers,efficient_producers,sk4,sk5(sk1(sk2(sk4),sk4))))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f170,plain,(
% 0.15/0.40 ~sQ22_spl|sQ23_spl|sQ10_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f162,f164,f167,f91])).
% 0.15/0.40 fof(f171,definition,(
% 0.15/0.40 sQ24_spl <=> (greater(sk5(sk1(sk2(sk4),sk4)),sk1(sk2(sk4),sk4)))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f174,plain,(
% 0.15/0.40 ~sQ22_spl|sQ24_spl|sQ10_spl),
% 0.15/0.40 inference(split_clause,[status(thm)],[f163,f164,f171,f91])).
% 0.15/0.40 fof(f175,plain,(
% 0.15/0.40 ~environment(sk4)|~stable(sk4)|~subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))|~environment(sk4)|~in_environment(sk4,sk3(sk4))|~greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|sQ6_spl),
% 0.15/0.40 inference(resolution,[status(thm)],[f125,f26])).
% 0.15/0.40 fof(f176,definition,(
% 0.15/0.40 sQ25_spl <=> (stable(sk4))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f178,plain,(
% 0.15/0.40 ~stable(sk4)|sQ25_spl),
% 0.15/0.40 inference(component_clause,[status(thm)],[f176])).
% 0.15/0.40 fof(f179,definition,(
% 0.15/0.40 sQ26_spl <=> (subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4)))),
% 0.15/0.40 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.15/0.40 fof(f181,plain,(
% 0.15/0.40 ~subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))|sQ26_spl),
% 0.15/0.40 inference(component_clause,[status(thm)],[f179])).
% 0.15/0.40 fof(f182,plain,(
% 0.15/0.40 ~sQ0_spl|~sQ25_spl|~sQ26_spl|~sQ1_spl|~sQ7_spl|sQ6_spl),
% 0.15/0.41 inference(split_clause,[status(thm)],[f175,f44,f176,f179,f47,f74,f71])).
% 0.15/0.41 fof(f183,plain,(
% 0.15/0.41 ![X0]: (~environment(sk4)|~in_environment(sk4,X0)|greater_or_equal(sk1(X0,sk4),X0)|~subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))|greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))|~sQ21_spl)),
% 0.15/0.41 inference(resolution,[status(thm)],[f149,f28])).
% 0.15/0.41 fof(f184,plain,(
% 0.15/0.41 ![X0]: (~environment(sk4)|~in_environment(sk4,X0)|subpopulations(first_movers,efficient_producers,sk4,sk1(X0,sk4))|~subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))|greater(growth_rate(efficient_producers,sk5(sk2(sk4))),growth_rate(first_movers,sk5(sk2(sk4))))|~sQ21_spl)),
% 0.15/0.41 inference(resolution,[status(thm)],[f149,f24])).
% 0.15/0.41 fof(f185,definition,(
% 0.15/0.41 ![X0]: (sQ27_spl <=> (~in_environment(sk4,X0)|greater_or_equal(sk1(X0,sk4),X0)))),
% 0.15/0.41 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.15/0.41 fof(f186,plain,(
% 0.17/0.43 ![X0]: (~in_environment(sk4,X0)|greater_or_equal(sk1(X0,sk4),X0)|~sQ27_spl)),
% 0.17/0.43 inference(component_clause,[status(thm)],[f185])).
% 0.17/0.43 fof(f188,plain,(
% 0.17/0.43 ~sQ0_spl|sQ27_spl|~sQ20_spl|sQ8_spl|~sQ21_spl),
% 0.17/0.43 inference(split_clause,[status(thm)],[f183,f44,f185,f144,f83,f148])).
% 0.17/0.43 fof(f189,definition,(
% 0.17/0.43 ![X0]: (sQ28_spl <=> (~in_environment(sk4,X0)|subpopulations(first_movers,efficient_producers,sk4,sk1(X0,sk4))))),
% 0.17/0.43 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.17/0.43 fof(f190,plain,(
% 0.17/0.43 ![X0]: (~in_environment(sk4,X0)|subpopulations(first_movers,efficient_producers,sk4,sk1(X0,sk4))|~sQ28_spl)),
% 0.17/0.43 inference(component_clause,[status(thm)],[f189])).
% 0.17/0.43 fof(f192,plain,(
% 0.17/0.43 ~sQ0_spl|sQ28_spl|~sQ20_spl|sQ8_spl|~sQ21_spl),
% 0.17/0.43 inference(split_clause,[status(thm)],[f184,f44,f189,f144,f83,f148])).
% 0.17/0.43 fof(f193,plain,(
% 0.17/0.43 ~in_environment(sk4,sk3(sk4))|~environment(sk4)|~stable(sk4)|~subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))|~sQ27_spl|sQ6_spl),
% 0.17/0.43 inference(resolution,[status(thm)],[f186,f125])).
% 0.17/0.43 fof(f194,plain,(
% 0.17/0.43 ~sQ1_spl|~sQ0_spl|~sQ25_spl|~sQ26_spl|~sQ27_spl|sQ6_spl),
% 0.17/0.43 inference(split_clause,[status(thm)],[f193,f47,f44,f176,f179,f185,f71])).
% 0.17/0.43 fof(f195,plain,(
% 0.17/0.43 $false|sQ25_spl),
% 0.17/0.43 inference(forward_subsumption_resolution,[status(thm)],[f178,f39])).
% 0.17/0.43 fof(f196,plain,(
% 0.17/0.43 sQ25_spl),
% 0.17/0.43 inference(contradiction_clause,[status(thm)],[f195])).
% 0.17/0.43 fof(f197,plain,(
% 0.17/0.43 ~environment(sk4)|~in_environment(sk4,sk3(sk4))|~greater(growth_rate(efficient_producers,sk2(sk4)),growth_rate(first_movers,sk2(sk4)))|sQ26_spl),
% 0.17/0.43 inference(resolution,[status(thm)],[f181,f22])).
% 0.17/0.43 fof(f198,plain,(
% 0.17/0.43 ~environment(sk4)|~in_environment(sk4,sk3(sk4))|in_environment(sk4,sk2(sk4))|sQ26_spl),
% 0.17/0.43 inference(resolution,[status(thm)],[f181,f18])).
% 0.17/0.43 fof(f199,plain,(
% 0.17/0.43 ~sQ0_spl|~sQ1_spl|~sQ7_spl|sQ26_spl),
% 0.17/0.43 inference(split_clause,[status(thm)],[f197,f44,f47,f74,f179])).
% 0.17/0.43 fof(f200,plain,(
% 0.17/0.43 ~sQ0_spl|~sQ1_spl|sQ5_spl|sQ26_spl),
% 0.17/0.43 inference(split_clause,[status(thm)],[f198,f44,f47,f67,f179])).
% 0.17/0.43 fof(f201,plain,(
% 0.17/0.43 ~environment(sk4)|~stable(sk4)|~subpopulations(first_movers,efficient_producers,sk4,sk1(sk3(sk4),sk4))|~sQ4_spl|sQ6_spl),
% 0.17/0.43 inference(resolution,[status(thm)],[f65,f125])).
% 0.17/0.43 fof(f202,plain,(
% 0.17/0.43 ~sQ0_spl|~sQ25_spl|~sQ26_spl|~sQ4_spl|sQ6_spl),
% 0.17/0.43 inference(split_clause,[status(thm)],[f201,f44,f176,f179,f64,f71])).
% 0.17/0.43 fof(f233,plain,(
% 0.17/0.43 ![X0]: (~environment(sk4)|~in_environment(sk4,X0)|~greater(growth_rate(efficient_producers,sk1(X0,sk4)),growth_rate(first_movers,sk1(X0,sk4)))|~subpopulations(first_movers,efficient_producers,sk4,sk5(sk2(sk4)))|sQ8_spl|~sQ21_spl)),
% 0.17/0.43 inference(resolution,[status(thm)],[f96,f149])).
% 0.17/0.43 fof(f234,definition,(
% 0.17/0.43 ![X0]: (sQ29_spl <=> (~in_environment(sk4,X0)|~greater(growth_rate(efficient_producers,sk1(X0,sk4)),growth_rate(first_movers,sk1(X0,sk4)))))),
% 0.17/0.43 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.17/0.43 fof(f235,plain,(
% 0.17/0.43 ![X0]: (~in_environment(sk4,X0)|~greater(growth_rate(efficient_producers,sk1(X0,sk4)),growth_rate(first_movers,sk1(X0,sk4)))|~sQ29_spl)),
% 0.17/0.43 inference(component_clause,[status(thm)],[f234])).
% 0.17/0.43 fof(f237,plain,(
% 0.17/0.43 ~sQ0_spl|sQ29_spl|~sQ20_spl|sQ8_spl|~sQ21_spl),
% 0.17/0.43 inference(split_clause,[status(thm)],[f233,f44,f234,f144,f83,f148])).
% 0.17/0.43 fof(f239,plain,(
% 0.17/0.43 ~greater(growth_rate(efficient_producers,sk1(sk3(sk4),sk4)),growth_rate(first_movers,sk1(sk3(sk4),sk4)))|~sQ29_spl|~sQ1_spl),
% 0.17/0.43 inference(resolution,[status(thm)],[f235,f48])).
% 0.17/0.43 fof(f240,plain,(
% 0.17/0.43 ~sQ6_spl|~sQ29_spl|~sQ1_spl),
% 0.17/0.43 inference(split_clause,[status(thm)],[f239,f71,f234,f47])).
% 0.17/0.43 fof(f241,plain,(
% 0.17/0.43 ~in_environment(sk4,sk3(sk4))|sQ26_spl|~sQ28_spl),
% 0.17/0.43 inference(resolution,[status(thm)],[f181,f190])).
% 0.17/0.43 fof(f244,plain,(
% 0.17/0.43 $false|~sQ1_spl|sQ26_spl|~sQ28_spl),
% 0.17/0.43 inference(forward_subsumption_resolution,[status(thm)],[f241,f48])).
% 0.17/0.43 fof(f245,plain,(
% 0.17/0.43 ~sQ1_spl|sQ26_spl|~sQ28_spl),
% 0.17/0.43 inference(contradiction_clause,[status(thm)],[f244])).
% 0.17/0.43 fof(f246,plain,(
% 0.17/0.43 $false),
% 0.17/0.43 inference(sat_refutation,[status(thm)],[f50,f52,f63,f70,f77,f78,f86,f94,f105,f109,f120,f124,f135,f139,f147,f151,f170,f174,f182,f188,f192,f194,f196,f199,f200,f202,f237,f240,f245])).
% 0.17/0.44 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.46 % Elapsed time: 0.061009 seconds
% 0.17/0.46 % CPU time: 0.047710 seconds
% 0.17/0.46 % Total memory used: 698.800 KB
% 0.17/0.46 % Net memory used: 692.992 KB
%------------------------------------------------------------------------------