FindProof---0.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : FindProof---0.1
% Problem  : MGT029+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300

% Computer : n020.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 : Fri Sep 25 02:11:23 PM UTC 2026

% Result   : Theorem 78.59s 11.07s
% Output   : Proof 78.59s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : MGT029+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04  % Command  : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.35  % Computer : n020.cluster.edu
% 0.09/0.35  % Model    : x86_64 x86_64
% 0.09/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35  % Memory   : 8046.5625MB
% 0.09/0.35  % OS       : Linux 6.8.0-71-generic
% 0.09/0.36  % CPULimit : 300
% 0.09/0.36  % WCLimit  : 300
% 0.09/0.36  % DateTime : Thu Sep 24 01:05:47 UTC 2026
% 0.09/0.36  % CPUTime  : 
% 0.09/0.36  Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 78.59/11.07  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 78.59/11.07  % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 78.59/11.07  fof(sdef0, definition, (spl0 <=> (~stable(sk2))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 78.59/11.07  cnf(p24, plain, (~stable(sk2) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 78.59/11.07  fof(f6, conjecture, ! [E] : ( ( environment(E) & stable(E) ) => ? [To] : ( in_environment(E,To) & ! [T] : ( ( subpopulations(first_movers,efficient_producers,E,T) & greater_or_equal(T,To) ) => ( greater(growth_rate(efficient_producers,T),zero) & greater(zero,growth_rate(first_movers,T)) ) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_l11)).
% 78.59/11.07  fof(f6_neg, negated_conjecture, ~(! [E] : ( ( environment(E) & stable(E) ) => ? [To] : ( in_environment(E,To) & ! [T] : ( ( subpopulations(first_movers,efficient_producers,E,T) & greater_or_equal(T,To) ) => ( greater(growth_rate(efficient_producers,T),zero) & greater(zero,growth_rate(first_movers,T)) ) ) ) )), inference(negated_conjecture, [status(cth)], [f6])).
% 78.59/11.07  fof(f6_nnf, plain, ? [E] : (((environment(E) & stable(E)) & ! [To] : ((~(in_environment(E,To)) | ? [T] : (((subpopulations(first_movers,efficient_producers,E,T) & greater_or_equal(T,To)) & (~(greater(growth_rate(efficient_producers,T),zero)) | ~(greater(zero,growth_rate(first_movers,T)))))))))), inference(nnf_transformation, [status(thm)], [f6_neg])).
% 78.59/11.07  fof(f6_sk, plain, ! [To] : (((environment(sk2) & stable(sk2)) & (~(in_environment(sk2,To)) | ((subpopulations(first_movers,efficient_producers,sk2,sk3(To)) & greater_or_equal(sk3(To),To)) & (~(greater(growth_rate(efficient_producers,sk3(To)),zero)) | ~(greater(zero,growth_rate(first_movers,sk3(To))))))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk2,sk3])], [f6_nnf])).
% 78.59/11.07  cnf(c18, plain, stable(sk2), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 78.59/11.07  cnf(p26, plain, ($false | ~spl0), inference(resolution, [status(thm)], [p24, c18])).
% 78.59/11.07  cnf(sct0, plain, (~spl0), inference(avatar_contradiction_clause, [status(thm)], [p26])).
% 78.59/11.07  fof(sdef11, definition, (spl11 <=> (growth_rate(first_movers,sk0(sk2)) = zero)), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 78.59/11.07  cnf(p52, plain, (growth_rate(first_movers,sk0(sk2)) = zero | ~spl11), inference(avatar_component_clause, [status(thm)], [sdef11])).
% 78.59/11.07  fof(sdef12, definition, (spl12 <=> (greater(growth_rate(first_movers,sk0(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 78.59/11.07  cnf(p53, plain, (greater(growth_rate(first_movers,sk0(sk2)),zero) | ~spl12), inference(avatar_component_clause, [status(thm)], [sdef12])).
% 78.59/11.07  cnf(p60, plain, (greater(zero,zero) | ~spl11 | ~spl12), inference(superposition, [status(thm)], [p52, p53])).
% 78.59/11.07  fof(sdef5, definition, (spl5 <=> (sk3(sk0(sk2)) = sk0(sk2))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 78.59/11.07  cnf(p35, plain, (sk3(sk0(sk2)) = sk0(sk2) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 78.59/11.07  fof(sdef3, definition, (spl3 <=> (~greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 78.59/11.07  cnf(p31, plain, (~greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 78.59/11.07  cnf(p43, plain, (~greater(zero,growth_rate(first_movers,sk0(sk2))) | ~spl3 | ~spl5), inference(superposition, [status(thm)], [p35, p31])).
% 78.59/11.07  cnf(p57, plain, (~greater(zero,zero) | ~spl3 | ~spl5 | ~spl11), inference(superposition, [status(thm)], [p52, p43])).
% 78.59/11.07  cnf(p61, plain, ($false | ~spl3 | ~spl5 | ~spl11 | ~spl12), inference(resolution, [status(thm)], [p60, p57])).
% 78.59/11.07  cnf(sct1, plain, (~spl3 | ~spl5 | ~spl11 | ~spl12), inference(avatar_contradiction_clause, [status(thm)], [p61])).
% 78.59/11.07  fof(sdef9, definition, (spl9 <=> (greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 78.59/11.07  cnf(p49, plain, (greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 78.59/11.07  fof(sdef2, definition, (spl2 <=> (~greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 78.59/11.07  cnf(p30, plain, (~greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 78.59/11.07  cnf(p71, plain, ($false | ~spl2 | ~spl9), inference(resolution, [status(thm)], [p49, p30])).
% 78.59/11.07  cnf(sct2, plain, (~spl2 | ~spl9), inference(avatar_contradiction_clause, [status(thm)], [p71])).
% 78.59/11.07  fof(sdef20, definition, (spl20 <=> (sk1(sk2) = sk0(sk2))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 78.59/11.07  cnf(p99, plain, (sk1(sk2) = sk0(sk2) | ~spl20), inference(avatar_component_clause, [status(thm)], [sdef20])).
% 78.59/11.07  fof(sdef22, definition, (spl22 <=> (greater_or_equal(sk1(sk2),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 78.59/11.07  cnf(p106, plain, (greater_or_equal(sk1(sk2),equilibrium(sk2)) | ~spl22), inference(avatar_component_clause, [status(thm)], [sdef22])).
% 78.59/11.07  cnf(p120, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl20 | ~spl22), inference(superposition, [status(thm)], [p99, p106])).
% 78.59/11.07  fof(sdef10, definition, (spl10 <=> (~greater_or_equal(sk0(sk2),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 78.59/11.07  cnf(p51, plain, (~greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 78.59/11.07  cnf(p145, plain, ($false | ~spl10 | ~spl20 | ~spl22), inference(resolution, [status(thm)], [p120, p51])).
% 78.59/11.07  cnf(sct3, plain, (~spl10 | ~spl20 | ~spl22), inference(avatar_contradiction_clause, [status(thm)], [p145])).
% 78.59/11.07  fof(sdef29, definition, (spl29 <=> (equilibrium(sk2) = sk0(sk2))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 78.59/11.07  cnf(p141, plain, (equilibrium(sk2) = sk0(sk2) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 78.59/11.07  fof(sdef1, definition, (spl1 <=> (in_environment(sk2,sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 78.59/11.07  cnf(p25, plain, (in_environment(sk2,sk0(sk2)) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 78.59/11.07  cnf(c20, plain, ~in_environment(sk2,X1) | greater_or_equal(sk3(X1),X1), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 78.59/11.07  cnf(p27, plain, (greater_or_equal(sk3(sk0(sk2)),sk0(sk2)) | ~spl1), inference(resolution, [status(thm)], [p25, c20])).
% 78.59/11.07  cnf(p153, plain, (greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl1 | ~spl29), inference(superposition, [status(thm)], [p141, p27])).
% 78.59/11.07  fof(sdef6, definition, (spl6 <=> (~greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 78.59/11.07  cnf(p46, plain, (~greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 78.59/11.07  cnf(p254, plain, ($false | ~spl1 | ~spl6 | ~spl29), inference(resolution, [status(thm)], [p153, p46])).
% 78.59/11.07  cnf(sct4, plain, (~spl1 | ~spl6 | ~spl29), inference(avatar_contradiction_clause, [status(thm)], [p254])).
% 78.59/11.07  fof(sdef14, definition, (spl14 <=> (greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 78.59/11.07  cnf(p74, plain, (greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl14), inference(avatar_component_clause, [status(thm)], [sdef14])).
% 78.59/11.07  cnf(p414, plain, ($false | ~spl3 | ~spl14), inference(resolution, [status(thm)], [p31, p74])).
% 78.59/11.07  cnf(sct5, plain, (~spl3 | ~spl14), inference(avatar_contradiction_clause, [status(thm)], [p414])).
% 78.59/11.07  fof(sdef32, definition, (spl32 <=> (growth_rate(efficient_producers,sk3(sk0(sk2))) = zero)), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 78.59/11.07  cnf(p147, plain, (growth_rate(efficient_producers,sk3(sk0(sk2))) = zero | ~spl32), inference(avatar_component_clause, [status(thm)], [sdef32])).
% 78.59/11.07  cnf(p456, plain, (~greater(zero,zero) | ~spl2 | ~spl32), inference(superposition, [status(thm)], [p147, p30])).
% 78.59/11.07  cnf(p459, plain, ($false | ~spl2 | ~spl11 | ~spl12 | ~spl32), inference(resolution, [status(thm)], [p456, p60])).
% 78.59/11.07  cnf(sct6, plain, (~spl2 | ~spl11 | ~spl12 | ~spl32), inference(avatar_contradiction_clause, [status(thm)], [p459])).
% 78.59/11.07  fof(sdef7, definition, (spl7 <=> (growth_rate(first_movers,sk3(sk0(sk2))) = zero)), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 78.59/11.07  cnf(p47, plain, (growth_rate(first_movers,sk3(sk0(sk2))) = zero | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 78.59/11.07  fof(sdef8, definition, (spl8 <=> (greater(growth_rate(first_movers,sk3(sk0(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 78.59/11.07  cnf(p48, plain, (greater(growth_rate(first_movers,sk3(sk0(sk2))),zero) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 78.59/11.07  cnf(p68, plain, (greater(zero,zero) | ~spl7 | ~spl8), inference(superposition, [status(thm)], [p47, p48])).
% 78.59/11.07  cnf(p460, plain, ($false | ~spl2 | ~spl7 | ~spl8 | ~spl32), inference(resolution, [status(thm)], [p456, p68])).
% 78.59/11.07  cnf(sct7, plain, (~spl2 | ~spl7 | ~spl8 | ~spl32), inference(avatar_contradiction_clause, [status(thm)], [p460])).
% 78.59/11.07  fof(sdef37, definition, (spl37 <=> (~greater_or_equal(sk3(sk0(sk2)),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 78.59/11.07  cnf(p249, plain, (~greater_or_equal(sk3(sk0(sk2)),sk0(sk2)) | ~spl37), inference(avatar_component_clause, [status(thm)], [sdef37])).
% 78.59/11.07  cnf(p489, plain, ($false | ~spl1 | ~spl37), inference(resolution, [status(thm)], [p249, p27])).
% 78.59/11.07  cnf(sct8, plain, (~spl1 | ~spl37), inference(avatar_contradiction_clause, [status(thm)], [p489])).
% 78.59/11.07  fof(sdef44, definition, (spl44 <=> (growth_rate(first_movers,sk3(sk1(sk2))) = zero)), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 78.59/11.07  cnf(p265, plain, (growth_rate(first_movers,sk3(sk1(sk2))) = zero | ~spl44), inference(avatar_component_clause, [status(thm)], [sdef44])).
% 78.59/11.07  fof(sdef18, definition, (spl18 <=> (~greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 78.59/11.07  cnf(p95, plain, (~greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl18), inference(avatar_component_clause, [status(thm)], [sdef18])).
% 78.59/11.07  cnf(p554, plain, (~greater(zero,zero) | ~spl18 | ~spl44), inference(superposition, [status(thm)], [p265, p95])).
% 78.59/11.07  cnf(p557, plain, ($false | ~spl11 | ~spl12 | ~spl18 | ~spl44), inference(resolution, [status(thm)], [p554, p60])).
% 78.59/11.07  cnf(sct9, plain, (~spl11 | ~spl12 | ~spl18 | ~spl44), inference(avatar_contradiction_clause, [status(thm)], [p557])).
% 78.59/11.07  cnf(p558, plain, ($false | ~spl7 | ~spl8 | ~spl18 | ~spl44), inference(resolution, [status(thm)], [p554, p68])).
% 78.59/11.07  cnf(sct10, plain, (~spl7 | ~spl8 | ~spl18 | ~spl44), inference(avatar_contradiction_clause, [status(thm)], [p558])).
% 78.59/11.07  fof(sdef46, definition, (spl46 <=> (greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 78.59/11.07  cnf(p267, plain, (greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl46), inference(avatar_component_clause, [status(thm)], [sdef46])).
% 78.59/11.07  fof(sdef17, definition, (spl17 <=> (~greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 78.59/11.07  cnf(p94, plain, (~greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 78.59/11.07  cnf(p568, plain, ($false | ~spl17 | ~spl46), inference(resolution, [status(thm)], [p267, p94])).
% 78.59/11.07  cnf(sct11, plain, (~spl17 | ~spl46), inference(avatar_contradiction_clause, [status(thm)], [p568])).
% 78.59/11.07  fof(sdef34, definition, (spl34 <=> (sk3(sk1(sk2)) = sk1(sk2))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 78.59/11.07  cnf(p240, plain, (sk3(sk1(sk2)) = sk1(sk2) | ~spl34), inference(avatar_component_clause, [status(thm)], [sdef34])).
% 78.59/11.07  fof(sdef43, definition, (spl43 <=> (~greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 78.59/11.07  cnf(p264, plain, (~greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | ~spl43), inference(avatar_component_clause, [status(thm)], [sdef43])).
% 78.59/11.07  cnf(p543, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | ~spl34 | ~spl43), inference(superposition, [status(thm)], [p240, p264])).
% 78.59/11.07  cnf(p640, plain, ($false | ~spl22 | ~spl34 | ~spl43), inference(resolution, [status(thm)], [p543, p106])).
% 78.59/11.07  cnf(sct12, plain, (~spl22 | ~spl34 | ~spl43), inference(avatar_contradiction_clause, [status(thm)], [p640])).
% 78.59/11.07  fof(sdef49, definition, (spl49 <=> (growth_rate(efficient_producers,sk3(sk1(sk2))) = zero)), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 78.59/11.07  cnf(p274, plain, (growth_rate(efficient_producers,sk3(sk1(sk2))) = zero | ~spl49), inference(avatar_component_clause, [status(thm)], [sdef49])).
% 78.59/11.07  cnf(p652, plain, (~greater(zero,zero) | ~spl17 | ~spl49), inference(superposition, [status(thm)], [p274, p94])).
% 78.59/11.07  cnf(p656, plain, ($false | ~spl11 | ~spl12 | ~spl17 | ~spl49), inference(resolution, [status(thm)], [p652, p60])).
% 78.59/11.07  cnf(sct13, plain, (~spl11 | ~spl12 | ~spl17 | ~spl49), inference(avatar_contradiction_clause, [status(thm)], [p656])).
% 78.59/11.07  cnf(p657, plain, ($false | ~spl7 | ~spl8 | ~spl17 | ~spl49), inference(resolution, [status(thm)], [p652, p68])).
% 78.59/11.07  cnf(sct14, plain, (~spl7 | ~spl8 | ~spl17 | ~spl49), inference(avatar_contradiction_clause, [status(thm)], [p657])).
% 78.59/11.07  fof(sdef52, definition, (spl52 <=> (sk0(sk2) = sk1(sk2))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 78.59/11.07  cnf(p296, plain, (sk0(sk2) = sk1(sk2) | ~spl52), inference(avatar_component_clause, [status(thm)], [sdef52])).
% 78.59/11.07  fof(sdef16, definition, (spl16 <=> (in_environment(sk2,sk1(sk2)))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 78.59/11.07  cnf(p90, plain, (in_environment(sk2,sk1(sk2)) | ~spl16), inference(avatar_component_clause, [status(thm)], [sdef16])).
% 78.59/11.07  cnf(p91, plain, (greater_or_equal(sk3(sk1(sk2)),sk1(sk2)) | ~spl16), inference(resolution, [status(thm)], [p90, c20])).
% 78.59/11.07  cnf(p311, plain, (greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | ~spl16 | ~spl52), inference(superposition, [status(thm)], [p296, p91])).
% 78.59/11.07  fof(sdef50, definition, (spl50 <=> (~greater_or_equal(sk3(sk1(sk2)),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 78.59/11.07  cnf(p279, plain, (~greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | ~spl50), inference(avatar_component_clause, [status(thm)], [sdef50])).
% 78.59/11.07  cnf(p703, plain, ($false | ~spl16 | ~spl50 | ~spl52), inference(resolution, [status(thm)], [p311, p279])).
% 78.59/11.07  cnf(sct15, plain, (~spl16 | ~spl50 | ~spl52), inference(avatar_contradiction_clause, [status(thm)], [p703])).
% 78.59/11.07  fof(sdef54, definition, (spl54 <=> (equilibrium(sk2) = sk1(sk2))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 78.59/11.07  cnf(p299, plain, (equilibrium(sk2) = sk1(sk2) | ~spl54), inference(avatar_component_clause, [status(thm)], [sdef54])).
% 78.59/11.07  cnf(p345, plain, (greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | ~spl16 | ~spl54), inference(superposition, [status(thm)], [p299, p91])).
% 78.59/11.07  cnf(p710, plain, ($false | ~spl16 | ~spl43 | ~spl54), inference(resolution, [status(thm)], [p345, p264])).
% 78.59/11.07  cnf(sct16, plain, (~spl16 | ~spl43 | ~spl54), inference(avatar_contradiction_clause, [status(thm)], [p710])).
% 78.59/11.07  fof(sdef65, definition, (spl65 <=> (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 78.59/11.07  cnf(p724, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | ~spl65), inference(avatar_component_clause, [status(thm)], [sdef65])).
% 78.59/11.07  fof(f2, axiom, ! [X,Y] : ( greater_or_equal(X,Y) <=> ( greater(X,Y) | X = Y ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_or_equal)).
% 78.59/11.07  fof(f2_nnf, plain, ! [X,Y] : (((~(greater_or_equal(X,Y)) | (greater(X,Y) | X = Y)) & (greater_or_equal(X,Y) | (~(greater(X,Y)) & X != Y)))), inference(nnf_transformation, [status(thm)], [f2])).
% 78.59/11.07  fof(f2_sk, plain, ! [X,Y] : (((~(greater_or_equal(X,Y)) | (greater(X,Y) | X = Y)) & (greater_or_equal(X,Y) | (~(greater(X,Y)) & X != Y)))), inference(skolemisation, [status(esa)], [f2_nnf])).
% 78.59/11.07  cnf(c4, plain, greater_or_equal(X0,X1) | X0 != X1, inference(cnf_transformation, [status(esa)], [f2_sk])).
% 78.59/11.07  cnf(p22, plain, greater_or_equal(X0,X0), inference(equality_resolution, [status(thm)], [c4])).
% 78.59/11.07  cnf(p741, plain, ($false | ~spl65), inference(resolution, [status(thm)], [p724, p22])).
% 78.59/11.07  cnf(sct17, plain, (~spl65), inference(avatar_contradiction_clause, [status(thm)], [p741])).
% 78.59/11.07  fof(sdef72, definition, (spl72 <=> (~greater_or_equal(equilibrium(sk2),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 78.59/11.07  cnf(p739, plain, (~greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl72), inference(avatar_component_clause, [status(thm)], [sdef72])).
% 78.59/11.07  fof(sdef28, definition, (spl28 <=> (greater(equilibrium(sk2),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 78.59/11.07  cnf(p140, plain, (greater(equilibrium(sk2),sk0(sk2)) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 78.59/11.07  cnf(c3, plain, greater_or_equal(X0,X1) | ~greater(X0,X1), inference(cnf_transformation, [status(esa)], [f2_sk])).
% 78.59/11.07  cnf(p149, plain, (greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl28), inference(resolution, [status(thm)], [p140, c3])).
% 78.59/11.07  cnf(p742, plain, ($false | ~spl28 | ~spl72), inference(resolution, [status(thm)], [p739, p149])).
% 78.59/11.07  cnf(sct18, plain, (~spl28 | ~spl72), inference(avatar_contradiction_clause, [status(thm)], [p742])).
% 78.59/11.07  cnf(p150, plain, (greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl29), inference(resolution, [status(thm)], [p141, c4])).
% 78.59/11.07  cnf(p743, plain, ($false | ~spl29 | ~spl72), inference(resolution, [status(thm)], [p739, p150])).
% 78.59/11.07  cnf(sct19, plain, (~spl29 | ~spl72), inference(avatar_contradiction_clause, [status(thm)], [p743])).
% 78.59/11.07  fof(sdef38, definition, (spl38 <=> (greater(growth_rate(efficient_producers,sk3(sk0(sk2))),growth_rate(first_movers,sk3(sk0(sk2)))))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 78.59/11.07  cnf(p250, plain, (greater(growth_rate(efficient_producers,sk3(sk0(sk2))),growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl38), inference(avatar_component_clause, [status(thm)], [sdef38])).
% 78.59/11.07  cnf(p492, plain, (greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl7 | ~spl38), inference(superposition, [status(thm)], [p47, p250])).
% 78.59/11.07  cnf(p814, plain, ($false | ~spl2 | ~spl7 | ~spl38), inference(resolution, [status(thm)], [p492, p30])).
% 78.59/11.07  cnf(sct20, plain, (~spl2 | ~spl7 | ~spl38), inference(avatar_contradiction_clause, [status(thm)], [p814])).
% 78.59/11.07  fof(f0, axiom, ! [X,Y,Z] : ( ( greater(X,Y) & greater(Y,Z) ) => greater(X,Z) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_transitivity)).
% 78.59/11.07  fof(f0_nnf, plain, ! [X,Y,Z] : (((~(greater(X,Y)) | ~(greater(Y,Z))) | greater(X,Z))), inference(nnf_transformation, [status(thm)], [f0])).
% 78.59/11.07  fof(f0_sk, plain, ! [X,Y,Z] : (((~(greater(X,Y)) | ~(greater(Y,Z))) | greater(X,Z))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 78.59/11.07  cnf(c0, plain, ~greater(X0,X1) | ~greater(X1,X2) | greater(X0,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 78.59/11.07  cnf(p76, plain, (~greater(growth_rate(first_movers,sk3(sk0(sk2))),X0) | greater(zero,X0) | ~spl14), inference(resolution, [status(thm)], [p74, c0])).
% 78.59/11.07  cnf(p88, plain, (greater(zero,zero) | ~spl8 | ~spl14), inference(resolution, [status(thm)], [p76, p48])).
% 78.59/11.07  cnf(p815, plain, ($false | ~spl2 | ~spl8 | ~spl14 | ~spl32), inference(resolution, [status(thm)], [p456, p88])).
% 78.59/11.07  cnf(sct21, plain, (~spl2 | ~spl8 | ~spl14 | ~spl32), inference(avatar_contradiction_clause, [status(thm)], [p815])).
% 78.59/11.07  fof(sdef45, definition, (spl45 <=> (greater(growth_rate(first_movers,sk3(sk1(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 78.59/11.07  cnf(p266, plain, (greater(growth_rate(first_movers,sk3(sk1(sk2))),zero) | ~spl45), inference(avatar_component_clause, [status(thm)], [sdef45])).
% 78.59/11.07  cnf(p564, plain, (greater(zero,zero) | ~spl44 | ~spl45), inference(superposition, [status(thm)], [p265, p266])).
% 78.59/11.07  cnf(p816, plain, ($false | ~spl2 | ~spl32 | ~spl44 | ~spl45), inference(resolution, [status(thm)], [p456, p564])).
% 78.59/11.07  cnf(sct22, plain, (~spl2 | ~spl32 | ~spl44 | ~spl45), inference(avatar_contradiction_clause, [status(thm)], [p816])).
% 78.59/11.07  cnf(p817, plain, ($false | ~spl8 | ~spl14 | ~spl18 | ~spl44), inference(resolution, [status(thm)], [p554, p88])).
% 78.59/11.07  cnf(sct23, plain, (~spl8 | ~spl14 | ~spl18 | ~spl44), inference(avatar_contradiction_clause, [status(thm)], [p817])).
% 78.59/11.07  cnf(p818, plain, ($false | ~spl18 | ~spl44 | ~spl45), inference(resolution, [status(thm)], [p554, p564])).
% 78.59/11.07  cnf(sct24, plain, (~spl18 | ~spl44 | ~spl45), inference(avatar_contradiction_clause, [status(thm)], [p818])).
% 78.59/11.07  cnf(p819, plain, ($false | ~spl8 | ~spl14 | ~spl17 | ~spl49), inference(resolution, [status(thm)], [p652, p88])).
% 78.59/11.07  cnf(sct25, plain, (~spl8 | ~spl14 | ~spl17 | ~spl49), inference(avatar_contradiction_clause, [status(thm)], [p819])).
% 78.59/11.07  cnf(p820, plain, ($false | ~spl17 | ~spl44 | ~spl45 | ~spl49), inference(resolution, [status(thm)], [p652, p564])).
% 78.59/11.07  cnf(sct26, plain, (~spl17 | ~spl44 | ~spl45 | ~spl49), inference(avatar_contradiction_clause, [status(thm)], [p820])).
% 78.59/11.07  fof(sdef30, definition, (spl30 <=> (greater(sk0(sk2),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 78.59/11.07  cnf(p142, plain, (greater(sk0(sk2),equilibrium(sk2)) | ~spl30), inference(avatar_component_clause, [status(thm)], [sdef30])).
% 78.59/11.07  fof(sdef4, definition, (spl4 <=> (greater(sk3(sk0(sk2)),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 78.59/11.07  cnf(p34, plain, (greater(sk3(sk0(sk2)),sk0(sk2)) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 78.59/11.07  cnf(p36, plain, (~greater(sk0(sk2),X0) | greater(sk3(sk0(sk2)),X0) | ~spl4), inference(resolution, [status(thm)], [p34, c0])).
% 78.59/11.07  cnf(p192, plain, (greater(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl4 | ~spl30), inference(resolution, [status(thm)], [p142, p36])).
% 78.59/11.07  cnf(p256, plain, (greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl4 | ~spl30), inference(resolution, [status(thm)], [p192, c3])).
% 78.59/11.07  cnf(p826, plain, ($false | ~spl4 | ~spl6 | ~spl30), inference(resolution, [status(thm)], [p46, p256])).
% 78.59/11.07  cnf(sct27, plain, (~spl4 | ~spl6 | ~spl30), inference(avatar_contradiction_clause, [status(thm)], [p826])).
% 78.59/11.07  fof(sdef39, definition, (spl39 <=> (greater(sk3(sk0(sk2)),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 78.59/11.07  cnf(p252, plain, (greater(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl39), inference(avatar_component_clause, [status(thm)], [sdef39])).
% 78.59/11.07  cnf(p497, plain, (greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl39), inference(resolution, [status(thm)], [p252, c3])).
% 78.59/11.07  cnf(p827, plain, ($false | ~spl6 | ~spl39), inference(resolution, [status(thm)], [p46, p497])).
% 78.59/11.07  cnf(sct28, plain, (~spl6 | ~spl39), inference(avatar_contradiction_clause, [status(thm)], [p827])).
% 78.59/11.07  fof(sdef21, definition, (spl21 <=> (greater(sk0(sk2),sk1(sk2)))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 78.59/11.07  cnf(p100, plain, (greater(sk0(sk2),sk1(sk2)) | ~spl21), inference(avatar_component_clause, [status(thm)], [sdef21])).
% 78.59/11.07  cnf(p111, plain, (~greater(sk1(sk2),X0) | greater(sk0(sk2),X0) | ~spl21), inference(resolution, [status(thm)], [p100, c0])).
% 78.59/11.07  fof(sdef24, definition, (spl24 <=> (greater(sk1(sk2),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 78.59/11.07  cnf(p118, plain, (greater(sk1(sk2),equilibrium(sk2)) | ~spl24), inference(avatar_component_clause, [status(thm)], [sdef24])).
% 78.59/11.07  cnf(p368, plain, (greater(sk0(sk2),equilibrium(sk2)) | ~spl21 | ~spl24), inference(resolution, [status(thm)], [p111, p118])).
% 78.59/11.07  cnf(p468, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl21 | ~spl24), inference(resolution, [status(thm)], [p368, c3])).
% 78.59/11.07  cnf(p828, plain, ($false | ~spl10 | ~spl21 | ~spl24), inference(resolution, [status(thm)], [p51, p468])).
% 78.59/11.07  cnf(sct29, plain, (~spl10 | ~spl21 | ~spl24), inference(avatar_contradiction_clause, [status(thm)], [p828])).
% 78.59/11.07  fof(sdef58, definition, (spl58 <=> (sk3(sk0(sk2)) = sk1(sk2))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 78.59/11.07  cnf(p687, plain, (sk3(sk0(sk2)) = sk1(sk2) | ~spl58), inference(avatar_component_clause, [status(thm)], [sdef58])).
% 78.59/11.07  cnf(p852, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | ~spl6 | ~spl58), inference(superposition, [status(thm)], [p687, p46])).
% 78.59/11.07  cnf(p883, plain, ($false | ~spl6 | ~spl22 | ~spl58), inference(resolution, [status(thm)], [p852, p106])).
% 78.59/11.07  cnf(sct30, plain, (~spl6 | ~spl22 | ~spl58), inference(avatar_contradiction_clause, [status(thm)], [p883])).
% 78.59/11.07  fof(sdef60, definition, (spl60 <=> (sk3(sk1(sk2)) = sk0(sk2))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 78.59/11.07  cnf(p702, plain, (sk3(sk1(sk2)) = sk0(sk2) | ~spl60), inference(avatar_component_clause, [status(thm)], [sdef60])).
% 78.59/11.07  cnf(p904, plain, (~greater_or_equal(sk0(sk2),sk0(sk2)) | ~spl50 | ~spl60), inference(superposition, [status(thm)], [p702, p279])).
% 78.59/11.07  cnf(p923, plain, ($false | ~spl50 | ~spl60), inference(resolution, [status(thm)], [p904, p22])).
% 78.59/11.07  cnf(sct31, plain, (~spl50 | ~spl60), inference(avatar_contradiction_clause, [status(thm)], [p923])).
% 78.59/11.07  fof(sdef62, definition, (spl62 <=> (sk3(equilibrium(sk2)) = sk1(sk2))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 78.59/11.07  cnf(p706, plain, (sk3(equilibrium(sk2)) = sk1(sk2) | ~spl62), inference(avatar_component_clause, [status(thm)], [sdef62])).
% 78.59/11.07  fof(sdef42, definition, (spl42 <=> (sk3(equilibrium(sk2)) = equilibrium(sk2))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 78.59/11.07  cnf(p259, plain, (sk3(equilibrium(sk2)) = equilibrium(sk2) | ~spl42), inference(avatar_component_clause, [status(thm)], [sdef42])).
% 78.59/11.07  cnf(p939, plain, (sk1(sk2) = equilibrium(sk2) | ~spl42 | ~spl62), inference(superposition, [status(thm)], [p706, p259])).
% 78.59/11.07  cnf(p975, plain, (~greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl42 | ~spl50 | ~spl62), inference(superposition, [status(thm)], [p939, p279])).
% 78.59/11.07  cnf(p1008, plain, ($false | ~spl28 | ~spl42 | ~spl50 | ~spl62), inference(resolution, [status(thm)], [p975, p149])).
% 78.59/11.07  cnf(sct32, plain, (~spl28 | ~spl42 | ~spl50 | ~spl62), inference(avatar_contradiction_clause, [status(thm)], [p1008])).
% 78.59/11.07  fof(sdef51, definition, (spl51 <=> (greater(growth_rate(efficient_producers,sk3(sk1(sk2))),growth_rate(first_movers,sk3(sk1(sk2)))))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 78.59/11.07  cnf(p280, plain, (greater(growth_rate(efficient_producers,sk3(sk1(sk2))),growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl51), inference(avatar_component_clause, [status(thm)], [sdef51])).
% 78.59/11.07  cnf(p671, plain, (greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl44 | ~spl51), inference(superposition, [status(thm)], [p265, p280])).
% 78.59/11.07  cnf(p1024, plain, ($false | ~spl17 | ~spl44 | ~spl51), inference(resolution, [status(thm)], [p671, p94])).
% 78.59/11.07  cnf(sct33, plain, (~spl17 | ~spl44 | ~spl51), inference(avatar_contradiction_clause, [status(thm)], [p1024])).
% 78.59/11.07  fof(sdef64, definition, (spl64 <=> (sk3(sk1(sk2)) = equilibrium(sk2))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 78.59/11.07  cnf(p709, plain, (sk3(sk1(sk2)) = equilibrium(sk2) | ~spl64), inference(avatar_component_clause, [status(thm)], [sdef64])).
% 78.59/11.07  cnf(p1079, plain, (~greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl50 | ~spl64), inference(superposition, [status(thm)], [p709, p279])).
% 78.59/11.07  cnf(p1100, plain, ($false | ~spl28 | ~spl50 | ~spl64), inference(resolution, [status(thm)], [p1079, p149])).
% 78.59/11.07  cnf(sct34, plain, (~spl28 | ~spl50 | ~spl64), inference(avatar_contradiction_clause, [status(thm)], [p1100])).
% 78.59/11.07  fof(sdef47, definition, (spl47 <=> (greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 78.59/11.07  cnf(p269, plain, (greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl47), inference(avatar_component_clause, [status(thm)], [sdef47])).
% 78.59/11.07  cnf(p628, plain, (~greater(growth_rate(first_movers,sk3(sk1(sk2))),X0) | greater(zero,X0) | ~spl47), inference(resolution, [status(thm)], [p269, c0])).
% 78.59/11.07  cnf(p884, plain, (greater(zero,zero) | ~spl45 | ~spl47), inference(resolution, [status(thm)], [p628, p266])).
% 78.59/11.07  cnf(p1101, plain, ($false | ~spl2 | ~spl32 | ~spl45 | ~spl47), inference(resolution, [status(thm)], [p456, p884])).
% 78.59/11.07  cnf(sct35, plain, (~spl2 | ~spl32 | ~spl45 | ~spl47), inference(avatar_contradiction_clause, [status(thm)], [p1101])).
% 78.59/11.07  cnf(p1102, plain, ($false | ~spl17 | ~spl45 | ~spl47 | ~spl49), inference(resolution, [status(thm)], [p652, p884])).
% 78.59/11.07  cnf(sct36, plain, (~spl17 | ~spl45 | ~spl47 | ~spl49), inference(avatar_contradiction_clause, [status(thm)], [p1102])).
% 78.59/11.07  fof(sdef48, definition, (spl48 <=> (greater(zero,growth_rate(efficient_producers,sk3(sk1(sk2)))))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 78.59/11.07  cnf(p271, plain, (greater(zero,growth_rate(efficient_producers,sk3(sk1(sk2)))) | ~spl48), inference(avatar_component_clause, [status(thm)], [sdef48])).
% 78.59/11.07  cnf(p655, plain, (greater(zero,zero) | ~spl48 | ~spl49), inference(superposition, [status(thm)], [p274, p271])).
% 78.59/11.07  cnf(p1103, plain, ($false | ~spl17 | ~spl48 | ~spl49), inference(resolution, [status(thm)], [p655, p652])).
% 78.59/11.07  cnf(sct37, plain, (~spl17 | ~spl48 | ~spl49), inference(avatar_contradiction_clause, [status(thm)], [p1103])).
% 78.59/11.07  cnf(p469, plain, (greater(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl4 | ~spl21 | ~spl24), inference(resolution, [status(thm)], [p368, p36])).
% 78.59/11.07  cnf(p720, plain, (greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl4 | ~spl21 | ~spl24), inference(resolution, [status(thm)], [p469, c3])).
% 78.59/11.07  cnf(p1104, plain, ($false | ~spl4 | ~spl6 | ~spl21 | ~spl24), inference(resolution, [status(thm)], [p720, p46])).
% 78.59/11.07  cnf(sct38, plain, (~spl4 | ~spl6 | ~spl21 | ~spl24), inference(avatar_contradiction_clause, [status(thm)], [p1104])).
% 78.59/11.07  fof(sdef68, definition, (spl68 <=> (greater(growth_rate(efficient_producers,equilibrium(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 78.59/11.07  cnf(p727, plain, (greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl68), inference(avatar_component_clause, [status(thm)], [sdef68])).
% 78.59/11.07  fof(sdef55, definition, (spl55 <=> (~greater(growth_rate(efficient_producers,equilibrium(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 78.59/11.07  cnf(p624, plain, (~greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl55), inference(avatar_component_clause, [status(thm)], [sdef55])).
% 78.59/11.07  cnf(p1115, plain, ($false | ~spl55 | ~spl68), inference(resolution, [status(thm)], [p727, p624])).
% 78.59/11.07  cnf(sct39, plain, (~spl55 | ~spl68), inference(avatar_contradiction_clause, [status(thm)], [p1115])).
% 78.59/11.07  fof(sdef66, definition, (spl66 <=> (growth_rate(first_movers,equilibrium(sk2)) = zero)), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 78.59/11.07  cnf(p725, plain, (growth_rate(first_movers,equilibrium(sk2)) = zero | ~spl66), inference(avatar_component_clause, [status(thm)], [sdef66])).
% 78.59/11.07  fof(sdef67, definition, (spl67 <=> (greater(growth_rate(first_movers,equilibrium(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 78.59/11.07  cnf(p726, plain, (greater(growth_rate(first_movers,equilibrium(sk2)),zero) | ~spl67), inference(avatar_component_clause, [status(thm)], [sdef67])).
% 78.59/11.07  cnf(p1112, plain, (greater(zero,zero) | ~spl66 | ~spl67), inference(superposition, [status(thm)], [p725, p726])).
% 78.59/11.07  cnf(p1116, plain, ($false | ~spl17 | ~spl49 | ~spl66 | ~spl67), inference(resolution, [status(thm)], [p1112, p652])).
% 78.59/11.07  cnf(sct40, plain, (~spl17 | ~spl49 | ~spl66 | ~spl67), inference(avatar_contradiction_clause, [status(thm)], [p1116])).
% 78.59/11.07  fof(sdef56, definition, (spl56 <=> (~greater(zero,growth_rate(first_movers,equilibrium(sk2))))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 78.59/11.07  cnf(p625, plain, (~greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl56), inference(avatar_component_clause, [status(thm)], [sdef56])).
% 78.59/11.07  cnf(p1109, plain, (~greater(zero,zero) | ~spl56 | ~spl66), inference(superposition, [status(thm)], [p725, p625])).
% 78.59/11.07  cnf(p1117, plain, ($false | ~spl56 | ~spl66 | ~spl67), inference(resolution, [status(thm)], [p1112, p1109])).
% 78.59/11.07  cnf(sct41, plain, (~spl56 | ~spl66 | ~spl67), inference(avatar_contradiction_clause, [status(thm)], [p1117])).
% 78.59/11.07  fof(sdef33, definition, (spl33 <=> (greater(sk3(sk1(sk2)),sk1(sk2)))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 78.59/11.07  cnf(p239, plain, (greater(sk3(sk1(sk2)),sk1(sk2)) | ~spl33), inference(avatar_component_clause, [status(thm)], [sdef33])).
% 78.59/11.07  cnf(p281, plain, (~greater(sk1(sk2),X0) | greater(sk3(sk1(sk2)),X0) | ~spl33), inference(resolution, [status(thm)], [p239, c0])).
% 78.59/11.07  fof(sdef19, definition, (spl19 <=> (greater(sk1(sk2),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 78.59/11.07  cnf(p98, plain, (greater(sk1(sk2),sk0(sk2)) | ~spl19), inference(avatar_component_clause, [status(thm)], [sdef19])).
% 78.59/11.07  cnf(p672, plain, (greater(sk3(sk1(sk2)),sk0(sk2)) | ~spl19 | ~spl33), inference(resolution, [status(thm)], [p281, p98])).
% 78.59/11.07  cnf(p838, plain, (greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | ~spl19 | ~spl33), inference(resolution, [status(thm)], [p672, c3])).
% 78.59/11.07  cnf(p1144, plain, ($false | ~spl19 | ~spl33 | ~spl50), inference(resolution, [status(thm)], [p838, p279])).
% 78.59/11.07  cnf(sct42, plain, (~spl19 | ~spl33 | ~spl50), inference(avatar_contradiction_clause, [status(thm)], [p1144])).
% 78.59/11.07  fof(sdef31, definition, (spl31 <=> (sk0(sk2) = equilibrium(sk2))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 78.59/11.07  cnf(p144, plain, (sk0(sk2) = equilibrium(sk2) | ~spl31), inference(avatar_component_clause, [status(thm)], [sdef31])).
% 78.59/11.07  cnf(p1146, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | ~spl10 | ~spl31), inference(superposition, [status(thm)], [p144, p51])).
% 78.59/11.07  cnf(p1179, plain, ($false | ~spl10 | ~spl31), inference(resolution, [status(thm)], [p1146, p22])).
% 78.59/11.07  cnf(sct43, plain, (~spl10 | ~spl31), inference(avatar_contradiction_clause, [status(thm)], [p1179])).
% 78.59/11.07  cnf(p1180, plain, ($false | ~spl18 | ~spl47), inference(resolution, [status(thm)], [p95, p269])).
% 78.59/11.07  cnf(sct44, plain, (~spl18 | ~spl47), inference(avatar_contradiction_clause, [status(thm)], [p1180])).
% 78.59/11.07  cnf(p203, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl6 | ~spl31), inference(superposition, [status(thm)], [p144, p46])).
% 78.59/11.07  cnf(p196, plain, (greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl1 | ~spl31), inference(superposition, [status(thm)], [p144, p27])).
% 78.59/11.07  cnf(p1193, plain, ($false | ~spl1 | ~spl6 | ~spl31), inference(resolution, [status(thm)], [p203, p196])).
% 78.59/11.07  cnf(sct45, plain, (~spl1 | ~spl6 | ~spl31), inference(avatar_contradiction_clause, [status(thm)], [p1193])).
% 78.59/11.07  cnf(p1194, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | ~spl43 | ~spl64), inference(superposition, [status(thm)], [p709, p264])).
% 78.59/11.07  cnf(p1198, plain, ($false | ~spl43 | ~spl64), inference(resolution, [status(thm)], [p1194, p22])).
% 78.59/11.07  cnf(sct46, plain, (~spl43 | ~spl64), inference(avatar_contradiction_clause, [status(thm)], [p1198])).
% 78.59/11.07  cnf(p673, plain, (greater(sk3(sk1(sk2)),equilibrium(sk2)) | ~spl24 | ~spl33), inference(resolution, [status(thm)], [p281, p118])).
% 78.59/11.07  cnf(p840, plain, (greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | ~spl24 | ~spl33), inference(resolution, [status(thm)], [p673, c3])).
% 78.59/11.07  cnf(p1199, plain, ($false | ~spl24 | ~spl33 | ~spl43), inference(resolution, [status(thm)], [p840, p264])).
% 78.59/11.07  cnf(sct47, plain, (~spl24 | ~spl33 | ~spl43), inference(avatar_contradiction_clause, [status(thm)], [p1199])).
% 78.59/11.07  fof(sdef74, definition, (spl74 <=> (~greater_or_equal(sk1(sk2),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl74])], [avatar_definition])).
% 78.59/11.07  cnf(p1294, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | ~spl74), inference(avatar_component_clause, [status(thm)], [sdef74])).
% 78.59/11.07  cnf(p1311, plain, ($false | ~spl22 | ~spl74), inference(resolution, [status(thm)], [p1294, p106])).
% 78.59/11.07  cnf(sct48, plain, (~spl22 | ~spl74), inference(avatar_contradiction_clause, [status(thm)], [p1311])).
% 78.59/11.07  fof(sdef81, definition, (spl81 <=> (~greater_or_equal(sk1(sk2),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl81])], [avatar_definition])).
% 78.59/11.07  cnf(p1309, plain, (~greater_or_equal(sk1(sk2),sk0(sk2)) | ~spl81), inference(avatar_component_clause, [status(thm)], [sdef81])).
% 78.59/11.07  cnf(p102, plain, (greater_or_equal(sk1(sk2),sk0(sk2)) | ~spl19), inference(resolution, [status(thm)], [p98, c3])).
% 78.59/11.07  cnf(p1312, plain, ($false | ~spl19 | ~spl81), inference(resolution, [status(thm)], [p1309, p102])).
% 78.59/11.07  cnf(sct49, plain, (~spl19 | ~spl81), inference(avatar_contradiction_clause, [status(thm)], [p1312])).
% 78.59/11.07  cnf(p1074, plain, (~greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl17 | ~spl64), inference(superposition, [status(thm)], [p709, p94])).
% 78.59/11.07  cnf(p1333, plain, ($false | ~spl17 | ~spl64 | ~spl68), inference(resolution, [status(thm)], [p1074, p727])).
% 78.59/11.07  cnf(sct50, plain, (~spl17 | ~spl64 | ~spl68), inference(avatar_contradiction_clause, [status(thm)], [p1333])).
% 78.59/11.07  fof(sdef75, definition, (spl75 <=> (growth_rate(first_movers,sk1(sk2)) = zero)), introduced(definition, [new_symbols(naming, [spl75])], [avatar_definition])).
% 78.59/11.08  cnf(p1295, plain, (growth_rate(first_movers,sk1(sk2)) = zero | ~spl75), inference(avatar_component_clause, [status(thm)], [sdef75])).
% 78.59/11.08  fof(sdef27, definition, (spl27 <=> (~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 78.59/11.08  cnf(p137, plain, (~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl27), inference(avatar_component_clause, [status(thm)], [sdef27])).
% 78.59/11.08  cnf(p937, plain, (~greater(zero,growth_rate(first_movers,sk1(sk2))) | ~spl27 | ~spl62), inference(superposition, [status(thm)], [p706, p137])).
% 78.59/11.08  cnf(p1362, plain, (~greater(zero,zero) | ~spl27 | ~spl62 | ~spl75), inference(superposition, [status(thm)], [p1295, p937])).
% 78.59/11.08  cnf(p1363, plain, ($false | ~spl11 | ~spl12 | ~spl27 | ~spl62 | ~spl75), inference(resolution, [status(thm)], [p1362, p60])).
% 78.59/11.08  cnf(sct51, plain, (~spl11 | ~spl12 | ~spl27 | ~spl62 | ~spl75), inference(avatar_contradiction_clause, [status(thm)], [p1363])).
% 78.59/11.08  cnf(p1364, plain, ($false | ~spl8 | ~spl14 | ~spl27 | ~spl62 | ~spl75), inference(resolution, [status(thm)], [p1362, p88])).
% 78.59/11.08  cnf(sct52, plain, (~spl8 | ~spl14 | ~spl27 | ~spl62 | ~spl75), inference(avatar_contradiction_clause, [status(thm)], [p1364])).
% 78.59/11.08  cnf(p1365, plain, ($false | ~spl27 | ~spl45 | ~spl47 | ~spl62 | ~spl75), inference(resolution, [status(thm)], [p1362, p884])).
% 78.59/11.08  cnf(sct53, plain, (~spl27 | ~spl45 | ~spl47 | ~spl62 | ~spl75), inference(avatar_contradiction_clause, [status(thm)], [p1365])).
% 78.59/11.08  fof(sdef77, definition, (spl77 <=> (greater(growth_rate(efficient_producers,sk1(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl77])], [avatar_definition])).
% 78.59/11.08  cnf(p1297, plain, (greater(growth_rate(efficient_producers,sk1(sk2)),zero) | ~spl77), inference(avatar_component_clause, [status(thm)], [sdef77])).
% 78.59/11.08  fof(sdef26, definition, (spl26 <=> (~greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 78.59/11.08  cnf(p136, plain, (~greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~spl26), inference(avatar_component_clause, [status(thm)], [sdef26])).
% 78.59/11.08  cnf(p936, plain, (~greater(growth_rate(efficient_producers,sk1(sk2)),zero) | ~spl26 | ~spl62), inference(superposition, [status(thm)], [p706, p136])).
% 78.59/11.08  cnf(p1371, plain, ($false | ~spl26 | ~spl62 | ~spl77), inference(resolution, [status(thm)], [p1297, p936])).
% 78.59/11.08  cnf(sct54, plain, (~spl26 | ~spl62 | ~spl77), inference(avatar_contradiction_clause, [status(thm)], [p1371])).
% 78.59/11.08  fof(sdef57, definition, (spl57 <=> (greater(sk3(sk0(sk2)),sk1(sk2)))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 78.59/11.08  cnf(p686, plain, (greater(sk3(sk0(sk2)),sk1(sk2)) | ~spl57), inference(avatar_component_clause, [status(thm)], [sdef57])).
% 78.59/11.08  cnf(p845, plain, (~greater(sk1(sk2),X0) | greater(sk3(sk0(sk2)),X0) | ~spl57), inference(resolution, [status(thm)], [p686, c0])).
% 78.59/11.08  cnf(p1276, plain, (greater(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl24 | ~spl57), inference(resolution, [status(thm)], [p845, p118])).
% 78.59/11.08  cnf(p1351, plain, (greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl24 | ~spl57), inference(resolution, [status(thm)], [p1276, c3])).
% 78.59/11.08  cnf(p1399, plain, ($false | ~spl6 | ~spl24 | ~spl57), inference(resolution, [status(thm)], [p1351, p46])).
% 78.59/11.08  cnf(sct55, plain, (~spl6 | ~spl24 | ~spl57), inference(avatar_contradiction_clause, [status(thm)], [p1399])).
% 78.59/11.08  cnf(p490, plain, (~greater(growth_rate(first_movers,sk3(sk0(sk2))),X0) | greater(growth_rate(efficient_producers,sk3(sk0(sk2))),X0) | ~spl38), inference(resolution, [status(thm)], [p250, c0])).
% 78.59/11.08  cnf(p804, plain, (greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl8 | ~spl38), inference(resolution, [status(thm)], [p490, p48])).
% 78.59/11.08  cnf(p1402, plain, ($false | ~spl2 | ~spl8 | ~spl38), inference(resolution, [status(thm)], [p804, p30])).
% 78.59/11.08  cnf(sct56, plain, (~spl2 | ~spl8 | ~spl38), inference(avatar_contradiction_clause, [status(thm)], [p1402])).
% 78.59/11.08  cnf(p665, plain, (~greater(growth_rate(first_movers,sk3(sk1(sk2))),X0) | greater(growth_rate(efficient_producers,sk3(sk1(sk2))),X0) | ~spl51), inference(resolution, [status(thm)], [p280, c0])).
% 78.59/11.08  cnf(p1010, plain, (greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl45 | ~spl51), inference(resolution, [status(thm)], [p665, p266])).
% 78.59/11.08  cnf(p1405, plain, ($false | ~spl17 | ~spl45 | ~spl51), inference(resolution, [status(thm)], [p1010, p94])).
% 78.59/11.08  cnf(sct57, plain, (~spl17 | ~spl45 | ~spl51), inference(avatar_contradiction_clause, [status(thm)], [p1405])).
% 78.59/11.08  cnf(p1412, plain, (~greater_or_equal(sk1(sk2),sk0(sk2)) | ~spl34 | ~spl50), inference(superposition, [status(thm)], [p240, p279])).
% 78.59/11.08  cnf(p1421, plain, ($false | ~spl19 | ~spl34 | ~spl50), inference(resolution, [status(thm)], [p1412, p102])).
% 78.59/11.08  cnf(sct58, plain, (~spl19 | ~spl34 | ~spl50), inference(avatar_contradiction_clause, [status(thm)], [p1421])).
% 78.59/11.08  cnf(p1422, plain, ($false | ~spl2 | ~spl32 | ~spl66 | ~spl67), inference(resolution, [status(thm)], [p456, p1112])).
% 78.59/11.08  cnf(sct59, plain, (~spl2 | ~spl32 | ~spl66 | ~spl67), inference(avatar_contradiction_clause, [status(thm)], [p1422])).
% 78.59/11.08  fof(sdef25, definition, (spl25 <=> (sk1(sk2) = equilibrium(sk2))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 78.59/11.08  cnf(p119, plain, (sk1(sk2) = equilibrium(sk2) | ~spl25), inference(avatar_component_clause, [status(thm)], [sdef25])).
% 78.59/11.08  cnf(p112, plain, (greater_or_equal(sk0(sk2),sk1(sk2)) | ~spl21), inference(resolution, [status(thm)], [p100, c3])).
% 78.59/11.08  cnf(p131, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl21 | ~spl25), inference(superposition, [status(thm)], [p119, p112])).
% 78.59/11.08  cnf(p1469, plain, ($false | ~spl10 | ~spl21 | ~spl25), inference(resolution, [status(thm)], [p131, p51])).
% 78.59/11.08  cnf(sct60, plain, (~spl10 | ~spl21 | ~spl25), inference(avatar_contradiction_clause, [status(thm)], [p1469])).
% 78.59/11.08  fof(sdef63, definition, (spl63 <=> (greater(sk3(sk1(sk2)),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 78.59/11.08  cnf(p708, plain, (greater(sk3(sk1(sk2)),equilibrium(sk2)) | ~spl63), inference(avatar_component_clause, [status(thm)], [sdef63])).
% 78.59/11.08  cnf(p1065, plain, (greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | ~spl63), inference(resolution, [status(thm)], [p708, c3])).
% 78.59/11.08  cnf(p1518, plain, ($false | ~spl43 | ~spl63), inference(resolution, [status(thm)], [p264, p1065])).
% 78.59/11.08  cnf(sct61, plain, (~spl43 | ~spl63), inference(avatar_contradiction_clause, [status(thm)], [p1518])).
% 78.59/11.08  cnf(p539, plain, (~greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl26 | ~spl42), inference(superposition, [status(thm)], [p259, p136])).
% 78.59/11.08  cnf(p1519, plain, ($false | ~spl26 | ~spl42 | ~spl68), inference(resolution, [status(thm)], [p539, p727])).
% 78.59/11.08  cnf(sct62, plain, (~spl26 | ~spl42 | ~spl68), inference(avatar_contradiction_clause, [status(thm)], [p1519])).
% 78.59/11.08  cnf(p113, plain, (greater(sk3(sk0(sk2)),sk1(sk2)) | ~spl4 | ~spl21), inference(resolution, [status(thm)], [p100, p36])).
% 78.59/11.08  cnf(p242, plain, (greater_or_equal(sk3(sk0(sk2)),sk1(sk2)) | ~spl4 | ~spl21), inference(resolution, [status(thm)], [p113, c3])).
% 78.59/11.08  cnf(p754, plain, (greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl4 | ~spl21 | ~spl25), inference(superposition, [status(thm)], [p119, p242])).
% 78.59/11.08  cnf(p1521, plain, ($false | ~spl4 | ~spl6 | ~spl21 | ~spl25), inference(resolution, [status(thm)], [p754, p46])).
% 78.59/11.08  cnf(sct63, plain, (~spl4 | ~spl6 | ~spl21 | ~spl25), inference(avatar_contradiction_clause, [status(thm)], [p1521])).
% 78.59/11.08  cnf(p760, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl25 | ~spl43), inference(superposition, [status(thm)], [p119, p264])).
% 78.59/11.08  fof(sdef41, definition, (spl41 <=> (greater(sk3(equilibrium(sk2)),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 78.59/11.08  cnf(p258, plain, (greater(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl41), inference(avatar_component_clause, [status(thm)], [sdef41])).
% 78.59/11.08  cnf(p532, plain, (greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl41), inference(resolution, [status(thm)], [p258, c3])).
% 78.59/11.08  cnf(p1522, plain, ($false | ~spl25 | ~spl41 | ~spl43), inference(resolution, [status(thm)], [p760, p532])).
% 78.59/11.08  cnf(sct64, plain, (~spl25 | ~spl41 | ~spl43), inference(avatar_contradiction_clause, [status(thm)], [p1522])).
% 78.59/11.08  cnf(p125, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl16 | ~spl25), inference(superposition, [status(thm)], [p119, p90])).
% 78.59/11.08  cnf(p133, plain, (greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl16 | ~spl25), inference(resolution, [status(thm)], [p125, c20])).
% 78.59/11.08  cnf(p1523, plain, ($false | ~spl16 | ~spl25 | ~spl43), inference(resolution, [status(thm)], [p760, p133])).
% 78.59/11.08  cnf(sct65, plain, (~spl16 | ~spl25 | ~spl43), inference(avatar_contradiction_clause, [status(thm)], [p1523])).
% 78.59/11.08  cnf(p1524, plain, ($false | ~spl18 | ~spl44 | ~spl48 | ~spl49), inference(resolution, [status(thm)], [p554, p655])).
% 78.59/11.08  cnf(sct66, plain, (~spl18 | ~spl44 | ~spl48 | ~spl49), inference(avatar_contradiction_clause, [status(thm)], [p1524])).
% 78.59/11.08  cnf(p1525, plain, ($false | ~spl18 | ~spl44 | ~spl66 | ~spl67), inference(resolution, [status(thm)], [p554, p1112])).
% 78.59/11.08  cnf(sct67, plain, (~spl18 | ~spl44 | ~spl66 | ~spl67), inference(avatar_contradiction_clause, [status(thm)], [p1525])).
% 78.59/11.08  fof(sdef71, definition, (spl71 <=> (growth_rate(efficient_producers,equilibrium(sk2)) = zero)), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 78.59/11.08  cnf(p734, plain, (growth_rate(efficient_producers,equilibrium(sk2)) = zero | ~spl71), inference(avatar_component_clause, [status(thm)], [sdef71])).
% 78.59/11.08  cnf(p1127, plain, (greater(zero,zero) | ~spl68 | ~spl71), inference(superposition, [status(thm)], [p734, p727])).
% 78.59/11.08  cnf(p1526, plain, ($false | ~spl18 | ~spl44 | ~spl68 | ~spl71), inference(resolution, [status(thm)], [p554, p1127])).
% 78.59/11.08  cnf(sct68, plain, (~spl18 | ~spl44 | ~spl68 | ~spl71), inference(avatar_contradiction_clause, [status(thm)], [p1526])).
% 78.59/11.08  fof(sdef70, definition, (spl70 <=> (greater(zero,growth_rate(efficient_producers,equilibrium(sk2))))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 78.59/11.08  cnf(p731, plain, (greater(zero,growth_rate(efficient_producers,equilibrium(sk2))) | ~spl70), inference(avatar_component_clause, [status(thm)], [sdef70])).
% 78.59/11.08  cnf(p1128, plain, (greater(zero,zero) | ~spl70 | ~spl71), inference(superposition, [status(thm)], [p734, p731])).
% 78.59/11.08  cnf(p1527, plain, ($false | ~spl18 | ~spl44 | ~spl70 | ~spl71), inference(resolution, [status(thm)], [p554, p1128])).
% 78.59/11.08  cnf(sct69, plain, (~spl18 | ~spl44 | ~spl70 | ~spl71), inference(avatar_contradiction_clause, [status(thm)], [p1527])).
% 78.59/11.08  fof(sdef76, definition, (spl76 <=> (greater(growth_rate(first_movers,sk1(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl76])], [avatar_definition])).
% 78.59/11.08  cnf(p1296, plain, (greater(growth_rate(first_movers,sk1(sk2)),zero) | ~spl76), inference(avatar_component_clause, [status(thm)], [sdef76])).
% 78.59/11.08  cnf(p1368, plain, (greater(zero,zero) | ~spl75 | ~spl76), inference(superposition, [status(thm)], [p1295, p1296])).
% 78.59/11.08  cnf(p1528, plain, ($false | ~spl18 | ~spl44 | ~spl75 | ~spl76), inference(resolution, [status(thm)], [p554, p1368])).
% 78.59/11.08  cnf(sct70, plain, (~spl18 | ~spl44 | ~spl75 | ~spl76), inference(avatar_contradiction_clause, [status(thm)], [p1528])).
% 78.59/11.08  fof(sdef80, definition, (spl80 <=> (growth_rate(efficient_producers,sk1(sk2)) = zero)), introduced(definition, [new_symbols(naming, [spl80])], [avatar_definition])).
% 78.59/11.08  cnf(p1304, plain, (growth_rate(efficient_producers,sk1(sk2)) = zero | ~spl80), inference(avatar_component_clause, [status(thm)], [sdef80])).
% 78.59/11.08  cnf(p1385, plain, (greater(zero,zero) | ~spl77 | ~spl80), inference(superposition, [status(thm)], [p1304, p1297])).
% 78.59/11.08  cnf(p1529, plain, ($false | ~spl18 | ~spl44 | ~spl77 | ~spl80), inference(resolution, [status(thm)], [p554, p1385])).
% 78.59/11.08  cnf(sct71, plain, (~spl18 | ~spl44 | ~spl77 | ~spl80), inference(avatar_contradiction_clause, [status(thm)], [p1529])).
% 78.59/11.08  fof(sdef79, definition, (spl79 <=> (greater(zero,growth_rate(efficient_producers,sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl79])], [avatar_definition])).
% 78.59/11.08  cnf(p1301, plain, (greater(zero,growth_rate(efficient_producers,sk1(sk2))) | ~spl79), inference(avatar_component_clause, [status(thm)], [sdef79])).
% 78.59/11.08  cnf(p1386, plain, (greater(zero,zero) | ~spl79 | ~spl80), inference(superposition, [status(thm)], [p1304, p1301])).
% 78.59/11.08  cnf(p1530, plain, ($false | ~spl18 | ~spl44 | ~spl79 | ~spl80), inference(resolution, [status(thm)], [p554, p1386])).
% 78.59/11.08  cnf(sct72, plain, (~spl18 | ~spl44 | ~spl79 | ~spl80), inference(avatar_contradiction_clause, [status(thm)], [p1530])).
% 78.59/11.08  fof(sdef69, definition, (spl69 <=> (greater(zero,growth_rate(first_movers,equilibrium(sk2))))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 78.59/11.08  cnf(p729, plain, (greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl69), inference(avatar_component_clause, [status(thm)], [sdef69])).
% 78.59/11.08  cnf(p1118, plain, (~greater(growth_rate(first_movers,equilibrium(sk2)),X0) | greater(zero,X0) | ~spl69), inference(resolution, [status(thm)], [p729, c0])).
% 78.59/11.08  cnf(p1490, plain, (greater(zero,zero) | ~spl67 | ~spl69), inference(resolution, [status(thm)], [p1118, p726])).
% 78.59/11.08  cnf(p1531, plain, ($false | ~spl18 | ~spl44 | ~spl67 | ~spl69), inference(resolution, [status(thm)], [p554, p1490])).
% 78.59/11.08  cnf(sct73, plain, (~spl18 | ~spl44 | ~spl67 | ~spl69), inference(avatar_contradiction_clause, [status(thm)], [p1531])).
% 78.59/11.08  fof(sdef23, definition, (spl23 <=> (greater(zero,growth_rate(efficient_producers,sk3(sk0(sk2)))))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 78.59/11.08  cnf(p116, plain, (greater(zero,growth_rate(efficient_producers,sk3(sk0(sk2)))) | ~spl23), inference(avatar_component_clause, [status(thm)], [sdef23])).
% 78.59/11.08  cnf(p457, plain, (greater(zero,zero) | ~spl23 | ~spl32), inference(superposition, [status(thm)], [p147, p116])).
% 78.59/11.08  cnf(p1532, plain, ($false | ~spl2 | ~spl23 | ~spl32), inference(resolution, [status(thm)], [p457, p456])).
% 78.59/11.08  cnf(sct74, plain, (~spl2 | ~spl23 | ~spl32), inference(avatar_contradiction_clause, [status(thm)], [p1532])).
% 78.59/11.08  cnf(p1533, plain, ($false | ~spl56 | ~spl69), inference(resolution, [status(thm)], [p625, p729])).
% 78.59/11.08  cnf(sct75, plain, (~spl56 | ~spl69), inference(avatar_contradiction_clause, [status(thm)], [p1533])).
% 78.59/11.08  fof(sdef78, definition, (spl78 <=> (greater(zero,growth_rate(first_movers,sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl78])], [avatar_definition])).
% 78.59/11.08  cnf(p1299, plain, (greater(zero,growth_rate(first_movers,sk1(sk2))) | ~spl78), inference(avatar_component_clause, [status(thm)], [sdef78])).
% 78.59/11.08  cnf(p1538, plain, ($false | ~spl27 | ~spl62 | ~spl78), inference(resolution, [status(thm)], [p937, p1299])).
% 78.59/11.08  cnf(sct76, plain, (~spl27 | ~spl62 | ~spl78), inference(avatar_contradiction_clause, [status(thm)], [p1538])).
% 78.59/11.08  cnf(p1557, plain, (greater(zero,zero) | ~spl46 | ~spl49), inference(superposition, [status(thm)], [p274, p267])).
% 78.59/11.08  cnf(p1558, plain, ($false | ~spl2 | ~spl32 | ~spl46 | ~spl49), inference(resolution, [status(thm)], [p1557, p456])).
% 78.59/11.08  cnf(sct77, plain, (~spl2 | ~spl32 | ~spl46 | ~spl49), inference(avatar_contradiction_clause, [status(thm)], [p1558])).
% 78.59/11.08  cnf(p1559, plain, ($false | ~spl18 | ~spl44 | ~spl46 | ~spl49), inference(resolution, [status(thm)], [p1557, p554])).
% 78.59/11.08  cnf(sct78, plain, (~spl18 | ~spl44 | ~spl46 | ~spl49), inference(avatar_contradiction_clause, [status(thm)], [p1559])).
% 78.59/11.08  cnf(p1567, plain, (greater(zero,zero) | ~spl44 | ~spl49 | ~spl51), inference(superposition, [status(thm)], [p274, p671])).
% 78.59/11.08  cnf(p1568, plain, ($false | ~spl2 | ~spl32 | ~spl44 | ~spl49 | ~spl51), inference(resolution, [status(thm)], [p1567, p456])).
% 78.59/11.08  cnf(sct79, plain, (~spl2 | ~spl32 | ~spl44 | ~spl49 | ~spl51), inference(avatar_contradiction_clause, [status(thm)], [p1568])).
% 78.59/11.08  cnf(p1569, plain, ($false | ~spl18 | ~spl44 | ~spl49 | ~spl51), inference(resolution, [status(thm)], [p1567, p554])).
% 78.59/11.08  cnf(sct80, plain, (~spl18 | ~spl44 | ~spl49 | ~spl51), inference(avatar_contradiction_clause, [status(thm)], [p1569])).
% 78.59/11.08  cnf(p641, plain, (~greater(growth_rate(efficient_producers,sk3(sk1(sk2))),X0) | greater(zero,X0) | ~spl48), inference(resolution, [status(thm)], [p271, c0])).
% 78.59/11.08  cnf(p987, plain, (greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl48 | ~spl51), inference(resolution, [status(thm)], [p641, p280])).
% 78.59/11.08  cnf(p1628, plain, ($false | ~spl18 | ~spl48 | ~spl51), inference(resolution, [status(thm)], [p987, p95])).
% 78.59/11.08  cnf(sct81, plain, (~spl18 | ~spl48 | ~spl51), inference(avatar_contradiction_clause, [status(thm)], [p1628])).
% 78.59/11.08  cnf(p55, plain, (~greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl5 | ~spl6), inference(superposition, [status(thm)], [p35, p46])).
% 78.59/11.08  cnf(p191, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl30), inference(resolution, [status(thm)], [p142, c3])).
% 78.59/11.08  cnf(p1629, plain, ($false | ~spl5 | ~spl6 | ~spl30), inference(resolution, [status(thm)], [p55, p191])).
% 78.59/11.08  cnf(sct82, plain, (~spl5 | ~spl6 | ~spl30), inference(avatar_contradiction_clause, [status(thm)], [p1629])).
% 78.59/11.08  cnf(p1630, plain, ($false | ~spl5 | ~spl6 | ~spl21 | ~spl24), inference(resolution, [status(thm)], [p55, p468])).
% 78.59/11.08  cnf(sct83, plain, (~spl5 | ~spl6 | ~spl21 | ~spl24), inference(avatar_contradiction_clause, [status(thm)], [p1630])).
% 78.59/11.08  cnf(p1631, plain, ($false | ~spl5 | ~spl6 | ~spl21 | ~spl25), inference(resolution, [status(thm)], [p55, p131])).
% 78.59/11.08  cnf(sct84, plain, (~spl5 | ~spl6 | ~spl21 | ~spl25), inference(avatar_contradiction_clause, [status(thm)], [p1631])).
% 78.59/11.08  cnf(p413, plain, (~greater(zero,zero) | ~spl3 | ~spl7), inference(superposition, [status(thm)], [p47, p31])).
% 78.59/11.08  cnf(p1632, plain, ($false | ~spl3 | ~spl7 | ~spl11 | ~spl12), inference(resolution, [status(thm)], [p413, p60])).
% 78.59/11.08  cnf(sct85, plain, (~spl3 | ~spl7 | ~spl11 | ~spl12), inference(avatar_contradiction_clause, [status(thm)], [p1632])).
% 78.59/11.08  cnf(p1633, plain, ($false | ~spl3 | ~spl7 | ~spl8), inference(resolution, [status(thm)], [p413, p68])).
% 78.59/11.08  cnf(sct86, plain, (~spl3 | ~spl7 | ~spl8), inference(avatar_contradiction_clause, [status(thm)], [p1633])).
% 78.59/11.08  cnf(p1634, plain, ($false | ~spl3 | ~spl7 | ~spl44 | ~spl45), inference(resolution, [status(thm)], [p413, p564])).
% 78.59/11.08  cnf(sct87, plain, (~spl3 | ~spl7 | ~spl44 | ~spl45), inference(avatar_contradiction_clause, [status(thm)], [p1634])).
% 78.59/11.08  cnf(p636, plain, (greater(zero,zero) | ~spl44 | ~spl47), inference(superposition, [status(thm)], [p265, p269])).
% 78.59/11.08  cnf(p1635, plain, ($false | ~spl3 | ~spl7 | ~spl44 | ~spl47), inference(resolution, [status(thm)], [p413, p636])).
% 78.59/11.08  cnf(sct88, plain, (~spl3 | ~spl7 | ~spl44 | ~spl47), inference(avatar_contradiction_clause, [status(thm)], [p1635])).
% 78.59/11.08  cnf(p1636, plain, ($false | ~spl3 | ~spl7 | ~spl68 | ~spl71), inference(resolution, [status(thm)], [p413, p1127])).
% 78.59/11.08  cnf(sct89, plain, (~spl3 | ~spl7 | ~spl68 | ~spl71), inference(avatar_contradiction_clause, [status(thm)], [p1636])).
% 78.59/11.08  cnf(p1637, plain, ($false | ~spl3 | ~spl7 | ~spl70 | ~spl71), inference(resolution, [status(thm)], [p413, p1128])).
% 78.59/11.08  cnf(sct90, plain, (~spl3 | ~spl7 | ~spl70 | ~spl71), inference(avatar_contradiction_clause, [status(thm)], [p1637])).
% 78.59/11.08  cnf(p1638, plain, ($false | ~spl3 | ~spl7 | ~spl75 | ~spl76), inference(resolution, [status(thm)], [p413, p1368])).
% 78.59/11.08  cnf(sct91, plain, (~spl3 | ~spl7 | ~spl75 | ~spl76), inference(avatar_contradiction_clause, [status(thm)], [p1638])).
% 78.59/11.08  cnf(p1639, plain, ($false | ~spl3 | ~spl7 | ~spl77 | ~spl80), inference(resolution, [status(thm)], [p413, p1385])).
% 78.59/11.08  cnf(sct92, plain, (~spl3 | ~spl7 | ~spl77 | ~spl80), inference(avatar_contradiction_clause, [status(thm)], [p1639])).
% 78.59/11.08  cnf(p1640, plain, ($false | ~spl3 | ~spl7 | ~spl79 | ~spl80), inference(resolution, [status(thm)], [p413, p1386])).
% 78.59/11.08  cnf(sct93, plain, (~spl3 | ~spl7 | ~spl79 | ~spl80), inference(avatar_contradiction_clause, [status(thm)], [p1640])).
% 78.59/11.08  cnf(p1641, plain, ($false | ~spl3 | ~spl7 | ~spl67 | ~spl69), inference(resolution, [status(thm)], [p413, p1490])).
% 78.59/11.08  cnf(sct94, plain, (~spl3 | ~spl7 | ~spl67 | ~spl69), inference(avatar_contradiction_clause, [status(thm)], [p1641])).
% 78.59/11.08  cnf(p1642, plain, ($false | ~spl3 | ~spl7 | ~spl23 | ~spl32), inference(resolution, [status(thm)], [p413, p457])).
% 78.59/11.08  cnf(sct95, plain, (~spl3 | ~spl7 | ~spl23 | ~spl32), inference(avatar_contradiction_clause, [status(thm)], [p1642])).
% 78.59/11.08  cnf(p1372, plain, (~greater(growth_rate(first_movers,sk1(sk2)),X0) | greater(zero,X0) | ~spl78), inference(resolution, [status(thm)], [p1299, c0])).
% 78.59/11.08  cnf(p1578, plain, (greater(zero,zero) | ~spl76 | ~spl78), inference(resolution, [status(thm)], [p1372, p1296])).
% 78.59/11.08  cnf(p1643, plain, ($false | ~spl3 | ~spl7 | ~spl76 | ~spl78), inference(resolution, [status(thm)], [p413, p1578])).
% 78.59/11.08  cnf(sct96, plain, (~spl3 | ~spl7 | ~spl76 | ~spl78), inference(avatar_contradiction_clause, [status(thm)], [p1643])).
% 78.59/11.08  fof(sdef59, definition, (spl59 <=> (greater(sk3(sk1(sk2)),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 78.59/11.08  cnf(p701, plain, (greater(sk3(sk1(sk2)),sk0(sk2)) | ~spl59), inference(avatar_component_clause, [status(thm)], [sdef59])).
% 78.59/11.08  cnf(p893, plain, (greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | ~spl59), inference(resolution, [status(thm)], [p701, c3])).
% 78.59/11.08  cnf(p1651, plain, ($false | ~spl50 | ~spl59), inference(resolution, [status(thm)], [p279, p893])).
% 78.59/11.08  cnf(sct97, plain, (~spl50 | ~spl59), inference(avatar_contradiction_clause, [status(thm)], [p1651])).
% 78.59/11.08  cnf(p1694, plain, (greater(zero,zero) | ~spl9 | ~spl32), inference(superposition, [status(thm)], [p147, p49])).
% 78.59/11.08  cnf(p1698, plain, ($false | ~spl9 | ~spl18 | ~spl32 | ~spl44), inference(resolution, [status(thm)], [p1694, p554])).
% 78.59/11.08  cnf(sct98, plain, (~spl9 | ~spl18 | ~spl32 | ~spl44), inference(avatar_contradiction_clause, [status(thm)], [p1698])).
% 78.59/11.08  cnf(p1696, plain, (greater(zero,zero) | ~spl7 | ~spl32 | ~spl38), inference(superposition, [status(thm)], [p147, p492])).
% 78.59/11.08  cnf(p1699, plain, ($false | ~spl7 | ~spl18 | ~spl32 | ~spl38 | ~spl44), inference(resolution, [status(thm)], [p1696, p554])).
% 78.59/11.08  cnf(sct99, plain, (~spl7 | ~spl18 | ~spl32 | ~spl38 | ~spl44), inference(avatar_contradiction_clause, [status(thm)], [p1699])).
% 78.59/11.08  cnf(p1700, plain, ($false | ~spl7 | ~spl17 | ~spl32 | ~spl38 | ~spl49), inference(resolution, [status(thm)], [p1696, p652])).
% 78.59/11.08  cnf(sct100, plain, (~spl7 | ~spl17 | ~spl32 | ~spl38 | ~spl49), inference(avatar_contradiction_clause, [status(thm)], [p1700])).
% 78.59/11.08  cnf(p847, plain, (greater_or_equal(sk1(sk2),sk0(sk2)) | ~spl1 | ~spl58), inference(superposition, [status(thm)], [p687, p27])).
% 78.59/11.08  cnf(p1760, plain, ($false | ~spl1 | ~spl58 | ~spl81), inference(resolution, [status(thm)], [p847, p1309])).
% 78.59/11.08  cnf(sct101, plain, (~spl1 | ~spl58 | ~spl81), inference(avatar_contradiction_clause, [status(thm)], [p1760])).
% 78.59/11.08  cnf(p1676, plain, (~greater_or_equal(sk0(sk2),sk0(sk2)) | ~spl20 | ~spl81), inference(superposition, [status(thm)], [p99, p1309])).
% 78.59/11.08  cnf(p1803, plain, ($false | ~spl20 | ~spl81), inference(resolution, [status(thm)], [p1676, p22])).
% 78.59/11.08  cnf(sct102, plain, (~spl20 | ~spl81), inference(avatar_contradiction_clause, [status(thm)], [p1803])).
% 78.59/11.08  cnf(p789, plain, (~greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | ~spl29 | ~spl50), inference(superposition, [status(thm)], [p141, p279])).
% 78.59/11.08  cnf(p2025, plain, ($false | ~spl24 | ~spl29 | ~spl33 | ~spl50), inference(resolution, [status(thm)], [p789, p840])).
% 78.59/11.08  cnf(sct103, plain, (~spl24 | ~spl29 | ~spl33 | ~spl50), inference(avatar_contradiction_clause, [status(thm)], [p2025])).
% 78.59/11.08  cnf(p121, plain, (~greater(equilibrium(sk2),X0) | greater(sk1(sk2),X0) | ~spl24), inference(resolution, [status(thm)], [p118, c0])).
% 78.59/11.08  cnf(p395, plain, (greater(sk1(sk2),sk0(sk2)) | ~spl24 | ~spl28), inference(resolution, [status(thm)], [p121, p140])).
% 78.59/11.08  cnf(p677, plain, (greater(sk3(sk1(sk2)),sk0(sk2)) | ~spl24 | ~spl28 | ~spl33), inference(resolution, [status(thm)], [p281, p395])).
% 78.59/11.08  cnf(p842, plain, (greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | ~spl24 | ~spl28 | ~spl33), inference(resolution, [status(thm)], [p677, c3])).
% 78.59/11.08  cnf(p2100, plain, ($false | ~spl24 | ~spl28 | ~spl33 | ~spl50), inference(resolution, [status(thm)], [p842, p279])).
% 78.59/11.08  cnf(sct104, plain, (~spl24 | ~spl28 | ~spl33 | ~spl50), inference(avatar_contradiction_clause, [status(thm)], [p2100])).
% 78.59/11.08  fof(sdef35, definition, (spl35 <=> (greater(sk3(equilibrium(sk2)),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 78.59/11.08  cnf(p246, plain, (greater(sk3(equilibrium(sk2)),sk0(sk2)) | ~spl35), inference(avatar_component_clause, [status(thm)], [sdef35])).
% 78.59/11.08  cnf(p935, plain, (greater(sk1(sk2),sk0(sk2)) | ~spl35 | ~spl62), inference(superposition, [status(thm)], [p706, p246])).
% 78.59/11.08  fof(sdef53, definition, (spl53 <=> (greater(equilibrium(sk2),sk1(sk2)))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 78.59/11.08  cnf(p298, plain, (greater(equilibrium(sk2),sk1(sk2)) | ~spl53), inference(avatar_component_clause, [status(thm)], [sdef53])).
% 78.59/11.08  cnf(p330, plain, (~greater(sk1(sk2),X0) | greater(equilibrium(sk2),X0) | ~spl53), inference(resolution, [status(thm)], [p298, c0])).
% 78.59/11.08  cnf(p948, plain, (greater(equilibrium(sk2),sk0(sk2)) | ~spl35 | ~spl53 | ~spl62), inference(resolution, [status(thm)], [p935, p330])).
% 78.59/11.08  cnf(p994, plain, (greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl35 | ~spl53 | ~spl62), inference(resolution, [status(thm)], [p948, c3])).
% 78.59/11.08  cnf(p2101, plain, ($false | ~spl35 | ~spl53 | ~spl62 | ~spl72), inference(resolution, [status(thm)], [p739, p994])).
% 78.59/11.08  cnf(sct105, plain, (~spl35 | ~spl53 | ~spl62 | ~spl72), inference(avatar_contradiction_clause, [status(thm)], [p2101])).
% 78.59/11.08  cnf(p331, plain, (greater_or_equal(equilibrium(sk2),sk1(sk2)) | ~spl53), inference(resolution, [status(thm)], [p298, c3])).
% 78.59/11.08  cnf(p1659, plain, (greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl20 | ~spl53), inference(superposition, [status(thm)], [p99, p331])).
% 78.59/11.08  cnf(p2102, plain, ($false | ~spl20 | ~spl53 | ~spl72), inference(resolution, [status(thm)], [p739, p1659])).
% 78.59/11.08  cnf(sct106, plain, (~spl20 | ~spl53 | ~spl72), inference(avatar_contradiction_clause, [status(thm)], [p2102])).
% 78.59/11.08  cnf(p947, plain, (greater(sk3(sk1(sk2)),sk0(sk2)) | ~spl33 | ~spl35 | ~spl62), inference(resolution, [status(thm)], [p935, p281])).
% 78.59/11.08  cnf(p1315, plain, (greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | ~spl33 | ~spl35 | ~spl62), inference(resolution, [status(thm)], [p947, c3])).
% 78.59/11.08  cnf(p2105, plain, ($false | ~spl33 | ~spl35 | ~spl50 | ~spl62), inference(resolution, [status(thm)], [p1315, p279])).
% 78.59/11.08  cnf(sct107, plain, (~spl33 | ~spl35 | ~spl50 | ~spl62), inference(avatar_contradiction_clause, [status(thm)], [p2105])).
% 78.59/11.08  cnf(p1650, plain, (~greater_or_equal(sk3(sk0(sk2)),sk0(sk2)) | ~spl20 | ~spl50), inference(superposition, [status(thm)], [p99, p279])).
% 78.59/11.08  cnf(p2149, plain, ($false | ~spl1 | ~spl20 | ~spl50), inference(resolution, [status(thm)], [p1650, p27])).
% 78.59/11.08  cnf(sct108, plain, (~spl1 | ~spl20 | ~spl50), inference(avatar_contradiction_clause, [status(thm)], [p2149])).
% 78.59/11.08  cnf(p375, plain, (~greater(growth_rate(efficient_producers,sk3(sk0(sk2))),X0) | greater(zero,X0) | ~spl23), inference(resolution, [status(thm)], [p116, c0])).
% 78.59/11.08  cnf(p717, plain, (greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl23 | ~spl38), inference(resolution, [status(thm)], [p375, p250])).
% 78.59/11.08  cnf(p2152, plain, ($false | ~spl3 | ~spl23 | ~spl38), inference(resolution, [status(thm)], [p31, p717])).
% 78.59/11.08  cnf(sct109, plain, (~spl3 | ~spl23 | ~spl38), inference(avatar_contradiction_clause, [status(thm)], [p2152])).
% 78.59/11.08  cnf(p2153, plain, ($false | ~spl3 | ~spl7 | ~spl45 | ~spl47), inference(resolution, [status(thm)], [p413, p884])).
% 78.59/11.08  cnf(sct110, plain, (~spl3 | ~spl7 | ~spl45 | ~spl47), inference(avatar_contradiction_clause, [status(thm)], [p2153])).
% 78.59/11.08  cnf(p1122, plain, (greater(zero,zero) | ~spl66 | ~spl69), inference(superposition, [status(thm)], [p725, p729])).
% 78.59/11.08  cnf(p2154, plain, ($false | ~spl3 | ~spl7 | ~spl66 | ~spl69), inference(resolution, [status(thm)], [p413, p1122])).
% 78.59/11.08  cnf(sct111, plain, (~spl3 | ~spl7 | ~spl66 | ~spl69), inference(avatar_contradiction_clause, [status(thm)], [p2154])).
% 78.59/11.08  cnf(p2155, plain, ($false | ~spl3 | ~spl7 | ~spl9 | ~spl32), inference(resolution, [status(thm)], [p413, p1694])).
% 78.59/11.08  cnf(sct112, plain, (~spl3 | ~spl7 | ~spl9 | ~spl32), inference(avatar_contradiction_clause, [status(thm)], [p2155])).
% 78.59/11.08  cnf(p2156, plain, ($false | ~spl3 | ~spl7 | ~spl32 | ~spl38), inference(resolution, [status(thm)], [p413, p1696])).
% 78.59/11.08  cnf(sct113, plain, (~spl3 | ~spl7 | ~spl32 | ~spl38), inference(avatar_contradiction_clause, [status(thm)], [p2156])).
% 78.59/11.08  fof(f4, hypothesis, ! [E] : ( ( environment(E) & stable(E) ) => ? [To] : ( in_environment(E,To) & ! [T] : ( ( subpopulations(first_movers,efficient_producers,E,T) & greater_or_equal(T,To) ) => greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l1)).
% 78.59/11.08  fof(f4_nnf, plain, ! [E] : (((~(environment(E)) | ~(stable(E))) | ? [To] : ((in_environment(E,To) & ! [T] : (((~(subpopulations(first_movers,efficient_producers,E,T)) | ~(greater_or_equal(T,To))) | greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)))))))), inference(nnf_transformation, [status(thm)], [f4])).
% 78.59/11.08  fof(f4_sk, plain, ! [E,T] : (((~(environment(E)) | ~(stable(E))) | (in_environment(E,sk0(E)) & ((~(subpopulations(first_movers,efficient_producers,E,T)) | ~(greater_or_equal(T,sk0(E)))) | greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0])], [f4_nnf])).
% 78.59/11.08  cnf(c13, plain, ~environment(X0) | ~stable(X0) | in_environment(X0,sk0(X0)), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 78.59/11.08  cnf(c17, plain, environment(sk2), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 78.59/11.08  cnf(p23, plain, ~stable(sk2) | in_environment(sk2,sk0(sk2)), inference(resolution, [status(thm)], [c13, c17])).
% 78.59/11.08  cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [p23, sdef0, sdef1])).
% 78.59/11.08  cnf(c21, plain, ~in_environment(sk2,X1) | ~greater(growth_rate(efficient_producers,sk3(X1)),zero) | ~greater(zero,growth_rate(first_movers,sk3(X1))), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 78.59/11.08  cnf(p29, plain, (~greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl1), inference(resolution, [status(thm)], [p25, c21])).
% 78.59/11.08  cnf(ssp1, plain, (~spl1 | spl2 | spl3), inference(avatar_split_clause, [status(thm)], [p29, sdef2, sdef3])).
% 78.59/11.08  cnf(c2, plain, ~greater_or_equal(X0,X1) | greater(X0,X1) | X0 = X1, inference(cnf_transformation, [status(esa)], [f2_sk])).
% 78.59/11.08  cnf(p33, plain, (greater(sk3(sk0(sk2)),sk0(sk2)) | sk3(sk0(sk2)) = sk0(sk2) | ~spl1), inference(resolution, [status(thm)], [c2, p27])).
% 78.59/11.08  cnf(ssp2, plain, (~spl1 | spl4 | spl5), inference(avatar_split_clause, [status(thm)], [p33, sdef4, sdef5])).
% 78.59/11.08  fof(f3, hypothesis, ! [E,T] : ( ( environment(E) & subpopulations(first_movers,efficient_producers,E,T) & greater_or_equal(T,equilibrium(E)) ) => ( ( growth_rate(first_movers,T) = zero & growth_rate(efficient_producers,T) = zero ) | ( greater(growth_rate(first_movers,T),zero) & greater(zero,growth_rate(efficient_producers,T)) ) | ( greater(growth_rate(efficient_producers,T),zero) & greater(zero,growth_rate(first_movers,T)) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l6)).
% 78.59/11.08  fof(f3_nnf, plain, ! [E,T] : ((((~(environment(E)) | ~(subpopulations(first_movers,efficient_producers,E,T))) | ~(greater_or_equal(T,equilibrium(E)))) | (((growth_rate(first_movers,T) = zero & growth_rate(efficient_producers,T) = zero) | (greater(growth_rate(first_movers,T),zero) & greater(zero,growth_rate(efficient_producers,T)))) | (greater(growth_rate(efficient_producers,T),zero) & greater(zero,growth_rate(first_movers,T)))))), inference(nnf_transformation, [status(thm)], [f3])).
% 78.59/11.08  fof(f3_sk, plain, ! [E,T] : ((((~(environment(E)) | ~(subpopulations(first_movers,efficient_producers,E,T))) | ~(greater_or_equal(T,equilibrium(E)))) | (((growth_rate(first_movers,T) = zero & growth_rate(efficient_producers,T) = zero) | (greater(growth_rate(first_movers,T),zero) & greater(zero,growth_rate(efficient_producers,T)))) | (greater(growth_rate(efficient_producers,T),zero) & greater(zero,growth_rate(first_movers,T)))))), inference(skolemisation, [status(esa)], [f3_nnf])).
% 78.59/11.08  cnf(c5, plain, ~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), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 78.59/11.08  cnf(p39, plain, ~subpopulations(first_movers,efficient_producers,sk2,X0) | ~greater_or_equal(X0,equilibrium(sk2)) | growth_rate(first_movers,X0) = zero | greater(growth_rate(first_movers,X0),zero) | greater(growth_rate(efficient_producers,X0),zero), inference(resolution, [status(thm)], [c5, c17])).
% 78.59/11.08  cnf(c19, plain, ~in_environment(sk2,X1) | subpopulations(first_movers,efficient_producers,sk2,sk3(X1)), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 78.59/11.08  cnf(p28, plain, (subpopulations(first_movers,efficient_producers,sk2,sk3(sk0(sk2))) | ~spl1), inference(resolution, [status(thm)], [p25, c19])).
% 78.59/11.08  cnf(p45, plain, (~greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(sk0(sk2))) = zero | greater(growth_rate(first_movers,sk3(sk0(sk2))),zero) | greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl1), inference(resolution, [status(thm)], [p39, p28])).
% 78.59/11.08  cnf(ssp3, plain, (~spl1 | spl6 | spl7 | spl8 | spl9), inference(avatar_split_clause, [status(thm)], [p45, sdef6, sdef7, sdef8, sdef9])).
% 78.59/11.08  cnf(p40, plain, (subpopulations(first_movers,efficient_producers,sk2,sk0(sk2)) | ~spl1 | ~spl5), inference(superposition, [status(thm)], [p35, p28])).
% 78.59/11.08  cnf(p50, plain, (~greater_or_equal(sk0(sk2),equilibrium(sk2)) | growth_rate(first_movers,sk0(sk2)) = zero | greater(growth_rate(first_movers,sk0(sk2)),zero) | greater(growth_rate(efficient_producers,sk0(sk2)),zero) | ~spl1 | ~spl5), inference(resolution, [status(thm)], [p39, p40])).
% 78.59/11.08  fof(sdef13, definition, (spl13 <=> (greater(growth_rate(efficient_producers,sk0(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 78.59/11.08  cnf(ssp4, plain, (~spl1 | ~spl5 | spl10 | spl11 | spl12 | spl13), inference(avatar_split_clause, [status(thm)], [p50, sdef10, sdef11, sdef12, sdef13])).
% 78.59/11.08  cnf(c6, plain, ~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)), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 78.59/11.08  cnf(p42, plain, ~subpopulations(first_movers,efficient_producers,sk2,X0) | ~greater_or_equal(X0,equilibrium(sk2)) | growth_rate(first_movers,X0) = zero | greater(growth_rate(first_movers,X0),zero) | greater(zero,growth_rate(first_movers,X0)), inference(resolution, [status(thm)], [c6, c17])).
% 78.59/11.08  cnf(p73, plain, (~greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(sk0(sk2))) = zero | greater(growth_rate(first_movers,sk3(sk0(sk2))),zero) | greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl1), inference(resolution, [status(thm)], [p42, p28])).
% 78.59/11.08  cnf(ssp5, plain, (~spl1 | spl6 | spl7 | spl8 | spl14), inference(avatar_split_clause, [status(thm)], [p73, sdef6, sdef7, sdef8, sdef14])).
% 78.59/11.08  cnf(c14, plain, ~environment(X0) | ~stable(X0) | ~subpopulations(first_movers,efficient_producers,X0,X2) | ~greater_or_equal(X2,sk0(X0)) | greater(growth_rate(efficient_producers,X2),growth_rate(first_movers,X2)), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 78.59/11.08  cnf(p84, plain, ~stable(sk2) | ~subpopulations(first_movers,efficient_producers,sk2,X0) | ~greater_or_equal(X0,sk0(sk2)) | greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)), inference(resolution, [status(thm)], [c14, c17])).
% 78.59/11.08  fof(sdef15, definition, (spl15 <=> (~subpopulations(first_movers,efficient_producers,sk2,X0) | ~greater_or_equal(X0,sk0(sk2)) | greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 78.59/11.08  cnf(ssp6, plain, (spl0 | spl15), inference(avatar_split_clause, [status(thm)], [p84, sdef0, sdef15])).
% 78.59/11.08  fof(f5, hypothesis, ! [E] : ( ( environment(E) & stable(E) ) => ? [T] : ( in_environment(E,T) & greater_or_equal(T,equilibrium(E)) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', a4)).
% 78.59/11.08  fof(f5_nnf, plain, ! [E] : (((~(environment(E)) | ~(stable(E))) | ? [T] : ((in_environment(E,T) & greater_or_equal(T,equilibrium(E)))))), inference(nnf_transformation, [status(thm)], [f5])).
% 78.59/11.08  fof(f5_sk, plain, ! [E] : (((~(environment(E)) | ~(stable(E))) | (in_environment(E,sk1(E)) & greater_or_equal(sk1(E),equilibrium(E))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk1])], [f5_nnf])).
% 78.59/11.08  cnf(c15, plain, ~environment(X0) | ~stable(X0) | in_environment(X0,sk1(X0)), inference(cnf_transformation, [status(esa)], [f5_sk])).
% 78.59/11.08  cnf(p89, plain, ~stable(sk2) | in_environment(sk2,sk1(sk2)), inference(resolution, [status(thm)], [c15, c17])).
% 78.59/11.08  cnf(ssp7, plain, (spl0 | spl16), inference(avatar_split_clause, [status(thm)], [p89, sdef0, sdef16])).
% 78.59/11.08  cnf(p93, plain, (~greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl16), inference(resolution, [status(thm)], [p90, c21])).
% 78.59/11.08  cnf(ssp8, plain, (~spl16 | spl17 | spl18), inference(avatar_split_clause, [status(thm)], [p93, sdef17, sdef18])).
% 78.59/11.08  fof(f1, axiom, ! [E,T1,T2] : ( ( in_environment(E,T1) & in_environment(E,T2) ) => ( greater(T2,T1) | T2 = T1 | greater(T1,T2) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_times_in_environment)).
% 78.59/11.08  fof(f1_nnf, plain, ! [E,T1,T2] : (((~(in_environment(E,T1)) | ~(in_environment(E,T2))) | ((greater(T2,T1) | T2 = T1) | greater(T1,T2)))), inference(nnf_transformation, [status(thm)], [f1])).
% 78.59/11.08  fof(f1_sk, plain, ! [E,T1,T2] : (((~(in_environment(E,T1)) | ~(in_environment(E,T2))) | ((greater(T2,T1) | T2 = T1) | greater(T1,T2)))), inference(skolemisation, [status(esa)], [f1_nnf])).
% 78.59/11.08  cnf(c1, plain, ~in_environment(X0,X1) | ~in_environment(X0,X2) | greater(X2,X1) | X2 = X1 | greater(X1,X2), inference(cnf_transformation, [status(esa)], [f1_sk])).
% 78.59/11.08  cnf(p32, plain, (~in_environment(sk2,X0) | greater(X0,sk0(sk2)) | X0 = sk0(sk2) | greater(sk0(sk2),X0) | ~spl1), inference(resolution, [status(thm)], [p25, c1])).
% 78.59/11.08  cnf(p97, plain, (greater(sk1(sk2),sk0(sk2)) | sk1(sk2) = sk0(sk2) | greater(sk0(sk2),sk1(sk2)) | ~spl1 | ~spl16), inference(resolution, [status(thm)], [p90, p32])).
% 78.59/11.08  cnf(ssp9, plain, (~spl1 | ~spl16 | spl19 | spl20 | spl21), inference(avatar_split_clause, [status(thm)], [p97, sdef19, sdef20, sdef21])).
% 78.59/11.08  cnf(c16, plain, ~environment(X0) | ~stable(X0) | greater_or_equal(sk1(X0),equilibrium(X0)), inference(cnf_transformation, [status(esa)], [f5_sk])).
% 78.59/11.08  cnf(p105, plain, ~stable(sk2) | greater_or_equal(sk1(sk2),equilibrium(sk2)), inference(resolution, [status(thm)], [c16, c17])).
% 78.59/11.08  cnf(ssp10, plain, (spl0 | spl22), inference(avatar_split_clause, [status(thm)], [p105, sdef0, sdef22])).
% 78.59/11.08  cnf(p103, plain, (in_environment(sk2,sk0(sk2)) | ~spl16 | ~spl20), inference(superposition, [status(thm)], [p99, p90])).
% 78.59/11.08  cnf(p109, plain, (~greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl16 | ~spl20), inference(resolution, [status(thm)], [p103, c21])).
% 78.59/11.08  cnf(ssp11, plain, (~spl16 | ~spl20 | spl2 | spl3), inference(avatar_split_clause, [status(thm)], [p109, sdef2, sdef3])).
% 78.59/11.08  cnf(c7, plain, ~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), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 78.59/11.08  cnf(p44, plain, ~subpopulations(first_movers,efficient_producers,sk2,X0) | ~greater_or_equal(X0,equilibrium(sk2)) | growth_rate(first_movers,X0) = zero | greater(zero,growth_rate(efficient_producers,X0)) | greater(growth_rate(efficient_producers,X0),zero), inference(resolution, [status(thm)], [c7, c17])).
% 78.59/11.08  cnf(p115, plain, (~greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(sk0(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(sk0(sk2)))) | greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl1), inference(resolution, [status(thm)], [p44, p28])).
% 78.59/11.08  cnf(ssp12, plain, (~spl1 | spl6 | spl7 | spl9 | spl23), inference(avatar_split_clause, [status(thm)], [p115, sdef6, sdef7, sdef9, sdef23])).
% 78.59/11.08  cnf(p117, plain, (greater(sk1(sk2),equilibrium(sk2)) | sk1(sk2) = equilibrium(sk2) | ~spl22), inference(resolution, [status(thm)], [p106, c2])).
% 78.59/11.08  cnf(ssp13, plain, (~spl22 | spl24 | spl25), inference(avatar_split_clause, [status(thm)], [p117, sdef24, sdef25])).
% 78.59/11.08  cnf(c8, plain, ~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)), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 78.59/11.08  cnf(p56, plain, ~subpopulations(first_movers,efficient_producers,sk2,X0) | ~greater_or_equal(X0,equilibrium(sk2)) | growth_rate(first_movers,X0) = zero | greater(zero,growth_rate(efficient_producers,X0)) | greater(zero,growth_rate(first_movers,X0)), inference(resolution, [status(thm)], [c8, c17])).
% 78.59/11.08  cnf(p124, plain, (~greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(sk0(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(sk0(sk2)))) | greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl1), inference(resolution, [status(thm)], [p56, p28])).
% 78.59/11.08  cnf(ssp14, plain, (~spl1 | spl6 | spl7 | spl14 | spl23), inference(avatar_split_clause, [status(thm)], [p124, sdef6, sdef7, sdef14, sdef23])).
% 78.59/11.08  cnf(p135, plain, (~greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl16 | ~spl25), inference(resolution, [status(thm)], [p125, c21])).
% 78.59/11.08  cnf(ssp15, plain, (~spl16 | ~spl25 | spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p135, sdef26, sdef27])).
% 78.59/11.08  cnf(p139, plain, (greater(equilibrium(sk2),sk0(sk2)) | equilibrium(sk2) = sk0(sk2) | greater(sk0(sk2),equilibrium(sk2)) | ~spl1 | ~spl16 | ~spl25), inference(resolution, [status(thm)], [p125, p32])).
% 78.59/11.08  cnf(ssp16, plain, (~spl1 | ~spl16 | ~spl25 | spl28 | spl29 | spl30), inference(avatar_split_clause, [status(thm)], [p139, sdef28, sdef29, sdef30])).
% 78.59/11.08  cnf(p143, plain, (greater(sk0(sk2),equilibrium(sk2)) | sk0(sk2) = equilibrium(sk2) | ~spl20 | ~spl22), inference(resolution, [status(thm)], [p120, c2])).
% 78.59/11.08  cnf(ssp17, plain, (~spl20 | ~spl22 | spl30 | spl31), inference(avatar_split_clause, [status(thm)], [p143, sdef30, sdef31])).
% 78.59/11.08  cnf(c9, plain, ~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), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 78.59/11.08  cnf(p62, plain, ~subpopulations(first_movers,efficient_producers,sk2,X0) | ~greater_or_equal(X0,equilibrium(sk2)) | growth_rate(efficient_producers,X0) = zero | greater(growth_rate(first_movers,X0),zero) | greater(growth_rate(efficient_producers,X0),zero), inference(resolution, [status(thm)], [c9, c17])).
% 78.59/11.08  cnf(p146, plain, (~greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(sk0(sk2))) = zero | greater(growth_rate(first_movers,sk3(sk0(sk2))),zero) | greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl1), inference(resolution, [status(thm)], [p62, p28])).
% 78.59/11.08  cnf(ssp18, plain, (~spl1 | spl6 | spl8 | spl9 | spl32), inference(avatar_split_clause, [status(thm)], [p146, sdef6, sdef8, sdef9, sdef32])).
% 78.59/11.08  cnf(p151, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl1 | ~spl29), inference(superposition, [status(thm)], [p141, p25])).
% 78.59/11.08  cnf(p188, plain, (~greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl1 | ~spl29), inference(resolution, [status(thm)], [p151, c21])).
% 78.59/11.08  cnf(ssp19, plain, (~spl1 | ~spl29 | spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p188, sdef26, sdef27])).
% 78.59/11.08  cnf(c10, plain, ~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)), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 78.59/11.08  cnf(p65, plain, ~subpopulations(first_movers,efficient_producers,sk2,X0) | ~greater_or_equal(X0,equilibrium(sk2)) | growth_rate(efficient_producers,X0) = zero | greater(growth_rate(first_movers,X0),zero) | greater(zero,growth_rate(first_movers,X0)), inference(resolution, [status(thm)], [c10, c17])).
% 78.59/11.08  cnf(p194, plain, (~greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(sk0(sk2))) = zero | greater(growth_rate(first_movers,sk3(sk0(sk2))),zero) | greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl1), inference(resolution, [status(thm)], [p65, p28])).
% 78.59/11.08  cnf(ssp20, plain, (~spl1 | spl6 | spl8 | spl14 | spl32), inference(avatar_split_clause, [status(thm)], [p194, sdef6, sdef8, sdef14, sdef32])).
% 78.59/11.08  cnf(p195, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl1 | ~spl31), inference(superposition, [status(thm)], [p144, p25])).
% 78.59/11.08  cnf(p225, plain, (~greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl1 | ~spl31), inference(resolution, [status(thm)], [p195, c21])).
% 78.59/11.08  cnf(ssp21, plain, (~spl1 | ~spl31 | spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p225, sdef26, sdef27])).
% 78.59/11.08  cnf(c11, plain, ~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), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 78.59/11.08  cnf(p72, plain, ~subpopulations(first_movers,efficient_producers,sk2,X0) | ~greater_or_equal(X0,equilibrium(sk2)) | growth_rate(efficient_producers,X0) = zero | greater(zero,growth_rate(efficient_producers,X0)) | greater(growth_rate(efficient_producers,X0),zero), inference(resolution, [status(thm)], [c11, c17])).
% 78.59/11.08  cnf(p227, plain, (~greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(sk0(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(sk0(sk2)))) | greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl1), inference(resolution, [status(thm)], [p72, p28])).
% 78.59/11.08  cnf(ssp22, plain, (~spl1 | spl6 | spl9 | spl23 | spl32), inference(avatar_split_clause, [status(thm)], [p227, sdef6, sdef9, sdef23, sdef32])).
% 78.59/11.08  cnf(c12, plain, ~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)), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 78.59/11.08  cnf(p75, plain, ~subpopulations(first_movers,efficient_producers,sk2,X0) | ~greater_or_equal(X0,equilibrium(sk2)) | growth_rate(efficient_producers,X0) = zero | greater(zero,growth_rate(efficient_producers,X0)) | greater(zero,growth_rate(first_movers,X0)), inference(resolution, [status(thm)], [c12, c17])).
% 78.59/11.08  cnf(p230, plain, (~greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(sk0(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(sk0(sk2)))) | greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl1), inference(resolution, [status(thm)], [p75, p28])).
% 78.59/11.08  cnf(ssp23, plain, (~spl1 | spl6 | spl14 | spl23 | spl32), inference(avatar_split_clause, [status(thm)], [p230, sdef6, sdef14, sdef23, sdef32])).
% 78.59/11.08  cnf(p238, plain, (greater(sk3(sk1(sk2)),sk1(sk2)) | sk3(sk1(sk2)) = sk1(sk2) | ~spl16), inference(resolution, [status(thm)], [p91, c2])).
% 78.59/11.08  cnf(ssp24, plain, (~spl16 | spl33 | spl34), inference(avatar_split_clause, [status(thm)], [p238, sdef33, sdef34])).
% 78.59/11.08  cnf(p152, plain, (greater_or_equal(sk3(equilibrium(sk2)),sk0(sk2)) | ~spl1 | ~spl29), inference(superposition, [status(thm)], [p141, p27])).
% 78.59/11.08  cnf(p245, plain, (greater(sk3(equilibrium(sk2)),sk0(sk2)) | sk3(equilibrium(sk2)) = sk0(sk2) | ~spl1 | ~spl29), inference(resolution, [status(thm)], [p152, c2])).
% 78.59/11.08  fof(sdef36, definition, (spl36 <=> (sk3(equilibrium(sk2)) = sk0(sk2))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 78.59/11.08  cnf(ssp25, plain, (~spl1 | ~spl29 | spl35 | spl36), inference(avatar_split_clause, [status(thm)], [p245, sdef35, sdef36])).
% 78.59/11.08  cnf(p85, plain, (~subpopulations(first_movers,efficient_producers,sk2,X0) | ~greater_or_equal(X0,sk0(sk2)) | greater(growth_rate(efficient_producers,X0),growth_rate(first_movers,X0)) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 78.59/11.08  cnf(p248, plain, (~greater_or_equal(sk3(sk0(sk2)),sk0(sk2)) | greater(growth_rate(efficient_producers,sk3(sk0(sk2))),growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl1 | ~spl15), inference(resolution, [status(thm)], [p85, p28])).
% 78.59/11.08  cnf(ssp26, plain, (~spl1 | ~spl15 | spl37 | spl38), inference(avatar_split_clause, [status(thm)], [p248, sdef37, sdef38])).
% 78.59/11.08  cnf(p251, plain, (greater(sk3(sk0(sk2)),equilibrium(sk2)) | sk3(sk0(sk2)) = equilibrium(sk2) | ~spl1 | ~spl29), inference(resolution, [status(thm)], [p153, c2])).
% 78.59/11.08  fof(sdef40, definition, (spl40 <=> (sk3(sk0(sk2)) = equilibrium(sk2))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 78.59/11.08  cnf(ssp27, plain, (~spl1 | ~spl29 | spl39 | spl40), inference(avatar_split_clause, [status(thm)], [p251, sdef39, sdef40])).
% 78.59/11.08  cnf(p257, plain, (greater(sk3(equilibrium(sk2)),equilibrium(sk2)) | sk3(equilibrium(sk2)) = equilibrium(sk2) | ~spl1 | ~spl31), inference(resolution, [status(thm)], [p196, c2])).
% 78.59/11.08  cnf(ssp28, plain, (~spl1 | ~spl31 | spl41 | spl42), inference(avatar_split_clause, [status(thm)], [p257, sdef41, sdef42])).
% 78.59/11.08  cnf(p92, plain, (subpopulations(first_movers,efficient_producers,sk2,sk3(sk1(sk2))) | ~spl16), inference(resolution, [status(thm)], [p90, c19])).
% 78.59/11.08  cnf(p263, plain, (~greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(sk1(sk2))) = zero | greater(growth_rate(first_movers,sk3(sk1(sk2))),zero) | greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl16), inference(resolution, [status(thm)], [p92, p39])).
% 78.59/11.08  cnf(ssp29, plain, (~spl16 | spl43 | spl44 | spl45 | spl46), inference(avatar_split_clause, [status(thm)], [p263, sdef43, sdef44, sdef45, sdef46])).
% 78.59/11.08  cnf(p268, plain, (~greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(sk1(sk2))) = zero | greater(growth_rate(first_movers,sk3(sk1(sk2))),zero) | greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl16), inference(resolution, [status(thm)], [p92, p42])).
% 78.59/11.08  cnf(ssp30, plain, (~spl16 | spl43 | spl44 | spl45 | spl47), inference(avatar_split_clause, [status(thm)], [p268, sdef43, sdef44, sdef45, sdef47])).
% 78.59/11.08  cnf(p270, plain, (~greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(sk1(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(sk1(sk2)))) | greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl16), inference(resolution, [status(thm)], [p92, p44])).
% 78.59/11.08  cnf(ssp31, plain, (~spl16 | spl43 | spl44 | spl46 | spl48), inference(avatar_split_clause, [status(thm)], [p270, sdef43, sdef44, sdef46, sdef48])).
% 78.59/11.08  cnf(p272, plain, (~greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(sk1(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(sk1(sk2)))) | greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl16), inference(resolution, [status(thm)], [p92, p56])).
% 78.59/11.08  cnf(ssp32, plain, (~spl16 | spl43 | spl44 | spl47 | spl48), inference(avatar_split_clause, [status(thm)], [p272, sdef43, sdef44, sdef47, sdef48])).
% 78.59/11.08  cnf(p273, plain, (~greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(sk1(sk2))) = zero | greater(growth_rate(first_movers,sk3(sk1(sk2))),zero) | greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl16), inference(resolution, [status(thm)], [p92, p62])).
% 78.59/11.08  cnf(ssp33, plain, (~spl16 | spl43 | spl45 | spl46 | spl49), inference(avatar_split_clause, [status(thm)], [p273, sdef43, sdef45, sdef46, sdef49])).
% 78.59/11.08  cnf(p275, plain, (~greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(sk1(sk2))) = zero | greater(growth_rate(first_movers,sk3(sk1(sk2))),zero) | greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl16), inference(resolution, [status(thm)], [p92, p65])).
% 78.59/11.08  cnf(ssp34, plain, (~spl16 | spl43 | spl45 | spl47 | spl49), inference(avatar_split_clause, [status(thm)], [p275, sdef43, sdef45, sdef47, sdef49])).
% 78.59/11.08  cnf(p276, plain, (~greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(sk1(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(sk1(sk2)))) | greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl16), inference(resolution, [status(thm)], [p92, p72])).
% 78.59/11.08  cnf(ssp35, plain, (~spl16 | spl43 | spl46 | spl48 | spl49), inference(avatar_split_clause, [status(thm)], [p276, sdef43, sdef46, sdef48, sdef49])).
% 78.59/11.08  cnf(p277, plain, (~greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(sk1(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(sk1(sk2)))) | greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl16), inference(resolution, [status(thm)], [p92, p75])).
% 78.59/11.08  cnf(ssp36, plain, (~spl16 | spl43 | spl47 | spl48 | spl49), inference(avatar_split_clause, [status(thm)], [p277, sdef43, sdef47, sdef48, sdef49])).
% 78.59/11.08  cnf(p278, plain, (~greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | greater(growth_rate(efficient_producers,sk3(sk1(sk2))),growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl15 | ~spl16), inference(resolution, [status(thm)], [p92, p85])).
% 78.59/11.08  cnf(ssp37, plain, (~spl15 | ~spl16 | spl50 | spl51), inference(avatar_split_clause, [status(thm)], [p278, sdef50, sdef51])).
% 78.59/11.08  cnf(p96, plain, (~in_environment(sk2,X0) | greater(X0,sk1(sk2)) | X0 = sk1(sk2) | greater(sk1(sk2),X0) | ~spl16), inference(resolution, [status(thm)], [p90, c1])).
% 78.59/11.08  cnf(p295, plain, (greater(sk0(sk2),sk1(sk2)) | sk0(sk2) = sk1(sk2) | greater(sk1(sk2),sk0(sk2)) | ~spl1 | ~spl16), inference(resolution, [status(thm)], [p96, p25])).
% 78.59/11.08  cnf(ssp38, plain, (~spl1 | ~spl16 | spl19 | spl21 | spl52), inference(avatar_split_clause, [status(thm)], [p295, sdef19, sdef21, sdef52])).
% 78.59/11.08  cnf(p297, plain, (greater(equilibrium(sk2),sk1(sk2)) | equilibrium(sk2) = sk1(sk2) | greater(sk1(sk2),equilibrium(sk2)) | ~spl1 | ~spl16 | ~spl31), inference(resolution, [status(thm)], [p96, p195])).
% 78.59/11.08  cnf(ssp39, plain, (~spl1 | ~spl16 | ~spl31 | spl24 | spl53 | spl54), inference(avatar_split_clause, [status(thm)], [p297, sdef24, sdef53, sdef54])).
% 78.59/11.08  cnf(p301, plain, (in_environment(sk2,sk0(sk2)) | ~spl16 | ~spl52), inference(superposition, [status(thm)], [p296, p90])).
% 78.59/11.08  cnf(p323, plain, (~greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl16 | ~spl52), inference(resolution, [status(thm)], [p301, c21])).
% 78.59/11.08  cnf(ssp40, plain, (~spl16 | ~spl52 | spl2 | spl3), inference(avatar_split_clause, [status(thm)], [p323, sdef2, sdef3])).
% 78.59/11.08  cnf(p325, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl16 | ~spl31 | ~spl52), inference(superposition, [status(thm)], [p144, p301])).
% 78.59/11.08  cnf(p328, plain, (~greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl16 | ~spl31 | ~spl52), inference(resolution, [status(thm)], [p325, c21])).
% 78.59/11.08  cnf(ssp41, plain, (~spl16 | ~spl31 | ~spl52 | spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p328, sdef26, sdef27])).
% 78.59/11.08  cnf(p336, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl16 | ~spl54), inference(superposition, [status(thm)], [p299, p90])).
% 78.59/11.08  cnf(p362, plain, (~greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl16 | ~spl54), inference(resolution, [status(thm)], [p336, c21])).
% 78.59/11.08  cnf(ssp42, plain, (~spl16 | ~spl54 | spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p362, sdef26, sdef27])).
% 78.59/11.08  cnf(p364, plain, (greater(equilibrium(sk2),sk0(sk2)) | equilibrium(sk2) = sk0(sk2) | greater(sk0(sk2),equilibrium(sk2)) | ~spl1 | ~spl16 | ~spl54), inference(resolution, [status(thm)], [p336, p32])).
% 78.59/11.08  cnf(ssp43, plain, (~spl1 | ~spl16 | ~spl54 | spl28 | spl29 | spl30), inference(avatar_split_clause, [status(thm)], [p364, sdef28, sdef29, sdef30])).
% 78.59/11.08  cnf(p304, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl22 | ~spl52), inference(superposition, [status(thm)], [p296, p106])).
% 78.59/11.08  cnf(p371, plain, (greater(sk0(sk2),equilibrium(sk2)) | sk0(sk2) = equilibrium(sk2) | ~spl22 | ~spl52), inference(resolution, [status(thm)], [p304, c2])).
% 78.59/11.08  cnf(ssp44, plain, (~spl22 | ~spl52 | spl30 | spl31), inference(avatar_split_clause, [status(thm)], [p371, sdef30, sdef31])).
% 78.59/11.08  cnf(p358, plain, (sk0(sk2) = equilibrium(sk2) | ~spl52 | ~spl54), inference(superposition, [status(thm)], [p299, p296])).
% 78.59/11.08  cnf(p418, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl1 | ~spl52 | ~spl54), inference(superposition, [status(thm)], [p358, p25])).
% 78.59/11.08  cnf(p461, plain, (~greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl1 | ~spl52 | ~spl54), inference(resolution, [status(thm)], [p418, c21])).
% 78.59/11.08  cnf(ssp45, plain, (~spl1 | ~spl52 | ~spl54 | spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p461, sdef26, sdef27])).
% 78.59/11.08  cnf(p253, plain, (sk3(sk0(sk2)) = equilibrium(sk2) | ~spl40), inference(avatar_component_clause, [status(thm)], [sdef40])).
% 78.59/11.08  cnf(p499, plain, (greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl1 | ~spl40), inference(superposition, [status(thm)], [p253, p27])).
% 78.59/11.08  cnf(p542, plain, (greater(equilibrium(sk2),sk0(sk2)) | equilibrium(sk2) = sk0(sk2) | ~spl1 | ~spl40), inference(resolution, [status(thm)], [p499, c2])).
% 78.59/11.08  cnf(ssp46, plain, (~spl1 | ~spl40 | spl28 | spl29), inference(avatar_split_clause, [status(thm)], [p542, sdef28, sdef29])).
% 78.59/11.08  cnf(p247, plain, (sk3(equilibrium(sk2)) = sk0(sk2) | ~spl36), inference(avatar_component_clause, [status(thm)], [sdef36])).
% 78.59/11.08  cnf(p538, plain, (sk0(sk2) = equilibrium(sk2) | ~spl36 | ~spl42), inference(superposition, [status(thm)], [p247, p259])).
% 78.59/11.08  cnf(p580, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl1 | ~spl36 | ~spl42), inference(superposition, [status(thm)], [p538, p25])).
% 78.59/11.08  cnf(p623, plain, (~greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl1 | ~spl36 | ~spl42), inference(resolution, [status(thm)], [p580, c21])).
% 78.59/11.08  cnf(ssp47, plain, (~spl1 | ~spl36 | ~spl42 | spl55 | spl56), inference(avatar_split_clause, [status(thm)], [p623, sdef55, sdef56])).
% 78.59/11.08  cnf(p627, plain, (greater(equilibrium(sk2),sk1(sk2)) | equilibrium(sk2) = sk1(sk2) | greater(sk1(sk2),equilibrium(sk2)) | ~spl1 | ~spl16 | ~spl36 | ~spl42), inference(resolution, [status(thm)], [p580, p96])).
% 78.59/11.08  cnf(ssp48, plain, (~spl1 | ~spl16 | ~spl36 | ~spl42 | spl24 | spl53 | spl54), inference(avatar_split_clause, [status(thm)], [p627, sdef24, sdef53, sdef54])).
% 78.59/11.08  cnf(p608, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl16 | ~spl36 | ~spl42 | ~spl52), inference(superposition, [status(thm)], [p538, p301])).
% 78.59/11.08  cnf(p638, plain, (~greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl16 | ~spl36 | ~spl42 | ~spl52), inference(resolution, [status(thm)], [p608, c21])).
% 78.59/11.08  cnf(ssp49, plain, (~spl16 | ~spl36 | ~spl42 | ~spl52 | spl55 | spl56), inference(avatar_split_clause, [status(thm)], [p638, sdef55, sdef56])).
% 78.59/11.08  cnf(p310, plain, (greater_or_equal(sk3(sk0(sk2)),sk1(sk2)) | ~spl16 | ~spl52), inference(superposition, [status(thm)], [p296, p91])).
% 78.59/11.08  cnf(p685, plain, (greater(sk3(sk0(sk2)),sk1(sk2)) | sk3(sk0(sk2)) = sk1(sk2) | ~spl16 | ~spl52), inference(resolution, [status(thm)], [p310, c2])).
% 78.59/11.08  cnf(ssp50, plain, (~spl16 | ~spl52 | spl57 | spl58), inference(avatar_split_clause, [status(thm)], [p685, sdef57, sdef58])).
% 78.59/11.08  cnf(p688, plain, (greater_or_equal(equilibrium(sk2),sk1(sk2)) | ~spl16 | ~spl40 | ~spl52), inference(superposition, [status(thm)], [p253, p310])).
% 78.59/11.08  cnf(p689, plain, (greater(equilibrium(sk2),sk1(sk2)) | equilibrium(sk2) = sk1(sk2) | ~spl16 | ~spl40 | ~spl52), inference(resolution, [status(thm)], [p688, c2])).
% 78.59/11.08  cnf(ssp51, plain, (~spl16 | ~spl40 | ~spl52 | spl53 | spl54), inference(avatar_split_clause, [status(thm)], [p689, sdef53, sdef54])).
% 78.59/11.08  cnf(p690, plain, (greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl16 | ~spl40 | ~spl52), inference(superposition, [status(thm)], [p296, p688])).
% 78.59/11.08  cnf(p699, plain, (greater(equilibrium(sk2),sk0(sk2)) | equilibrium(sk2) = sk0(sk2) | ~spl16 | ~spl40 | ~spl52), inference(resolution, [status(thm)], [p690, c2])).
% 78.59/11.08  cnf(ssp52, plain, (~spl16 | ~spl40 | ~spl52 | spl28 | spl29), inference(avatar_split_clause, [status(thm)], [p699, sdef28, sdef29])).
% 78.59/11.08  cnf(p700, plain, (greater(sk3(sk1(sk2)),sk0(sk2)) | sk3(sk1(sk2)) = sk0(sk2) | ~spl16 | ~spl52), inference(resolution, [status(thm)], [p311, c2])).
% 78.59/11.08  cnf(ssp53, plain, (~spl16 | ~spl52 | spl59 | spl60), inference(avatar_split_clause, [status(thm)], [p700, sdef59, sdef60])).
% 78.59/11.08  cnf(p344, plain, (greater_or_equal(sk3(equilibrium(sk2)),sk1(sk2)) | ~spl16 | ~spl54), inference(superposition, [status(thm)], [p299, p91])).
% 78.59/11.08  cnf(p704, plain, (greater(sk3(equilibrium(sk2)),sk1(sk2)) | sk3(equilibrium(sk2)) = sk1(sk2) | ~spl16 | ~spl54), inference(resolution, [status(thm)], [p344, c2])).
% 78.59/11.08  fof(sdef61, definition, (spl61 <=> (greater(sk3(equilibrium(sk2)),sk1(sk2)))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 78.59/11.08  cnf(ssp54, plain, (~spl16 | ~spl54 | spl61 | spl62), inference(avatar_split_clause, [status(thm)], [p704, sdef61, sdef62])).
% 78.59/11.08  cnf(p707, plain, (greater(sk3(sk1(sk2)),equilibrium(sk2)) | sk3(sk1(sk2)) = equilibrium(sk2) | ~spl16 | ~spl54), inference(resolution, [status(thm)], [p345, c2])).
% 78.59/11.08  cnf(ssp55, plain, (~spl16 | ~spl54 | spl63 | spl64), inference(avatar_split_clause, [status(thm)], [p707, sdef63, sdef64])).
% 78.59/11.08  cnf(p502, plain, (subpopulations(first_movers,efficient_producers,sk2,equilibrium(sk2)) | ~spl1 | ~spl40), inference(superposition, [status(thm)], [p253, p28])).
% 78.59/11.08  cnf(p723, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(first_movers,equilibrium(sk2)) = zero | greater(growth_rate(first_movers,equilibrium(sk2)),zero) | greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl1 | ~spl40), inference(resolution, [status(thm)], [p502, p39])).
% 78.59/11.08  cnf(ssp56, plain, (~spl1 | ~spl40 | spl65 | spl66 | spl67 | spl68), inference(avatar_split_clause, [status(thm)], [p723, sdef65, sdef66, sdef67, sdef68])).
% 78.59/11.08  cnf(p728, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(first_movers,equilibrium(sk2)) = zero | greater(growth_rate(first_movers,equilibrium(sk2)),zero) | greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl1 | ~spl40), inference(resolution, [status(thm)], [p502, p42])).
% 78.59/11.08  cnf(ssp57, plain, (~spl1 | ~spl40 | spl65 | spl66 | spl67 | spl69), inference(avatar_split_clause, [status(thm)], [p728, sdef65, sdef66, sdef67, sdef69])).
% 78.59/11.08  cnf(p730, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(first_movers,equilibrium(sk2)) = zero | greater(zero,growth_rate(efficient_producers,equilibrium(sk2))) | greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl1 | ~spl40), inference(resolution, [status(thm)], [p502, p44])).
% 78.59/11.08  cnf(ssp58, plain, (~spl1 | ~spl40 | spl65 | spl66 | spl68 | spl70), inference(avatar_split_clause, [status(thm)], [p730, sdef65, sdef66, sdef68, sdef70])).
% 78.59/11.08  cnf(p732, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(first_movers,equilibrium(sk2)) = zero | greater(zero,growth_rate(efficient_producers,equilibrium(sk2))) | greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl1 | ~spl40), inference(resolution, [status(thm)], [p502, p56])).
% 78.59/11.08  cnf(ssp59, plain, (~spl1 | ~spl40 | spl65 | spl66 | spl69 | spl70), inference(avatar_split_clause, [status(thm)], [p732, sdef65, sdef66, sdef69, sdef70])).
% 78.59/11.08  cnf(p733, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,equilibrium(sk2)) = zero | greater(growth_rate(first_movers,equilibrium(sk2)),zero) | greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl1 | ~spl40), inference(resolution, [status(thm)], [p502, p62])).
% 78.59/11.08  cnf(ssp60, plain, (~spl1 | ~spl40 | spl65 | spl67 | spl68 | spl71), inference(avatar_split_clause, [status(thm)], [p733, sdef65, sdef67, sdef68, sdef71])).
% 78.59/11.08  cnf(p735, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,equilibrium(sk2)) = zero | greater(growth_rate(first_movers,equilibrium(sk2)),zero) | greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl1 | ~spl40), inference(resolution, [status(thm)], [p502, p65])).
% 78.59/11.08  cnf(ssp61, plain, (~spl1 | ~spl40 | spl65 | spl67 | spl69 | spl71), inference(avatar_split_clause, [status(thm)], [p735, sdef65, sdef67, sdef69, sdef71])).
% 78.59/11.08  cnf(p736, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,equilibrium(sk2)) = zero | greater(zero,growth_rate(efficient_producers,equilibrium(sk2))) | greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl1 | ~spl40), inference(resolution, [status(thm)], [p502, p72])).
% 78.59/11.08  cnf(ssp62, plain, (~spl1 | ~spl40 | spl65 | spl68 | spl70 | spl71), inference(avatar_split_clause, [status(thm)], [p736, sdef65, sdef68, sdef70, sdef71])).
% 78.59/11.08  cnf(p737, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,equilibrium(sk2)) = zero | greater(zero,growth_rate(efficient_producers,equilibrium(sk2))) | greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl1 | ~spl40), inference(resolution, [status(thm)], [p502, p75])).
% 78.59/11.08  cnf(ssp63, plain, (~spl1 | ~spl40 | spl65 | spl69 | spl70 | spl71), inference(avatar_split_clause, [status(thm)], [p737, sdef65, sdef69, sdef70, sdef71])).
% 78.59/11.08  cnf(p738, plain, (~greater_or_equal(equilibrium(sk2),sk0(sk2)) | greater(growth_rate(efficient_producers,equilibrium(sk2)),growth_rate(first_movers,equilibrium(sk2))) | ~spl1 | ~spl15 | ~spl40), inference(resolution, [status(thm)], [p502, p85])).
% 78.59/11.08  fof(sdef73, definition, (spl73 <=> (greater(growth_rate(efficient_producers,equilibrium(sk2)),growth_rate(first_movers,equilibrium(sk2))))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 78.59/11.08  cnf(ssp64, plain, (~spl1 | ~spl15 | ~spl40 | spl72 | spl73), inference(avatar_split_clause, [status(thm)], [p738, sdef72, sdef73])).
% 78.59/11.08  cnf(p748, plain, (greater(equilibrium(sk2),sk1(sk2)) | equilibrium(sk2) = sk1(sk2) | greater(sk1(sk2),equilibrium(sk2)) | ~spl1 | ~spl16 | ~spl29), inference(resolution, [status(thm)], [p151, p96])).
% 78.59/11.08  cnf(ssp65, plain, (~spl1 | ~spl16 | ~spl29 | spl24 | spl53 | spl54), inference(avatar_split_clause, [status(thm)], [p748, sdef24, sdef53, sdef54])).
% 78.59/11.08  cnf(p878, plain, (greater(sk1(sk2),sk0(sk2)) | sk1(sk2) = sk0(sk2) | ~spl1 | ~spl58), inference(resolution, [status(thm)], [p847, c2])).
% 78.59/11.08  cnf(ssp66, plain, (~spl1 | ~spl58 | spl19 | spl20), inference(avatar_split_clause, [status(thm)], [p878, sdef19, sdef20])).
% 78.59/11.08  cnf(p896, plain, (greater_or_equal(sk0(sk2),sk1(sk2)) | ~spl16 | ~spl60), inference(superposition, [status(thm)], [p702, p91])).
% 78.59/11.08  cnf(p916, plain, (greater(sk0(sk2),sk1(sk2)) | sk0(sk2) = sk1(sk2) | ~spl16 | ~spl60), inference(resolution, [status(thm)], [p896, c2])).
% 78.59/11.08  cnf(ssp67, plain, (~spl16 | ~spl60 | spl21 | spl52), inference(avatar_split_clause, [status(thm)], [p916, sdef21, sdef52])).
% 78.59/11.08  cnf(p955, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl16 | ~spl42 | ~spl62), inference(superposition, [status(thm)], [p939, p90])).
% 78.59/11.08  cnf(p989, plain, (~greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl16 | ~spl42 | ~spl62), inference(resolution, [status(thm)], [p955, c21])).
% 78.59/11.08  cnf(ssp68, plain, (~spl16 | ~spl42 | ~spl62 | spl55 | spl56), inference(avatar_split_clause, [status(thm)], [p989, sdef55, sdef56])).
% 78.59/11.08  cnf(p991, plain, (greater(equilibrium(sk2),sk0(sk2)) | equilibrium(sk2) = sk0(sk2) | greater(sk0(sk2),equilibrium(sk2)) | ~spl1 | ~spl16 | ~spl42 | ~spl62), inference(resolution, [status(thm)], [p955, p32])).
% 78.59/11.08  cnf(ssp69, plain, (~spl1 | ~spl16 | ~spl42 | ~spl62 | spl28 | spl29 | spl30), inference(avatar_split_clause, [status(thm)], [p991, sdef28, sdef29, sdef30])).
% 78.59/11.08  cnf(p1018, plain, (sk1(sk2) = sk0(sk2) | ~spl36 | ~spl62), inference(superposition, [status(thm)], [p706, p247])).
% 78.59/11.08  cnf(p1025, plain, (in_environment(sk2,sk0(sk2)) | ~spl16 | ~spl36 | ~spl62), inference(superposition, [status(thm)], [p1018, p90])).
% 78.59/11.08  cnf(p1062, plain, (~greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl16 | ~spl36 | ~spl62), inference(resolution, [status(thm)], [p1025, c21])).
% 78.59/11.08  cnf(ssp70, plain, (~spl16 | ~spl36 | ~spl62 | spl2 | spl3), inference(avatar_split_clause, [status(thm)], [p1062, sdef2, sdef3])).
% 78.59/11.08  cnf(p1028, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl22 | ~spl36 | ~spl62), inference(superposition, [status(thm)], [p1018, p106])).
% 78.59/11.08  cnf(p1070, plain, (greater(sk0(sk2),equilibrium(sk2)) | sk0(sk2) = equilibrium(sk2) | ~spl22 | ~spl36 | ~spl62), inference(resolution, [status(thm)], [p1028, c2])).
% 78.59/11.08  cnf(ssp71, plain, (~spl22 | ~spl36 | ~spl62 | spl30 | spl31), inference(avatar_split_clause, [status(thm)], [p1070, sdef30, sdef31])).
% 78.59/11.08  cnf(p1071, plain, (greater_or_equal(equilibrium(sk2),sk1(sk2)) | ~spl16 | ~spl64), inference(superposition, [status(thm)], [p709, p91])).
% 78.59/11.08  cnf(p1096, plain, (greater(equilibrium(sk2),sk1(sk2)) | equilibrium(sk2) = sk1(sk2) | ~spl16 | ~spl64), inference(resolution, [status(thm)], [p1071, c2])).
% 78.59/11.08  cnf(ssp72, plain, (~spl16 | ~spl64 | spl53 | spl54), inference(avatar_split_clause, [status(thm)], [p1096, sdef53, sdef54])).
% 78.59/11.08  cnf(p1185, plain, (greater_or_equal(sk1(sk2),equilibrium(sk2)) | ~spl1 | ~spl31 | ~spl62), inference(superposition, [status(thm)], [p706, p196])).
% 78.59/11.08  cnf(p1186, plain, (greater(sk1(sk2),equilibrium(sk2)) | sk1(sk2) = equilibrium(sk2) | ~spl1 | ~spl31 | ~spl62), inference(resolution, [status(thm)], [p1185, c2])).
% 78.59/11.08  cnf(ssp73, plain, (~spl1 | ~spl31 | ~spl62 | spl24 | spl25), inference(avatar_split_clause, [status(thm)], [p1186, sdef24, sdef25])).
% 78.59/11.08  cnf(p1217, plain, (sk1(sk2) = equilibrium(sk2) | ~spl34 | ~spl64), inference(superposition, [status(thm)], [p240, p709])).
% 78.59/11.08  cnf(p1225, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl16 | ~spl34 | ~spl64), inference(superposition, [status(thm)], [p1217, p90])).
% 78.59/11.08  cnf(p1271, plain, (~greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl16 | ~spl34 | ~spl64), inference(resolution, [status(thm)], [p1225, c21])).
% 78.59/11.08  cnf(ssp74, plain, (~spl16 | ~spl34 | ~spl64 | spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p1271, sdef26, sdef27])).
% 78.59/11.08  cnf(p1273, plain, (greater(equilibrium(sk2),sk0(sk2)) | equilibrium(sk2) = sk0(sk2) | greater(sk0(sk2),equilibrium(sk2)) | ~spl1 | ~spl16 | ~spl34 | ~spl64), inference(resolution, [status(thm)], [p1225, p32])).
% 78.59/11.08  cnf(ssp75, plain, (~spl1 | ~spl16 | ~spl34 | ~spl64 | spl28 | spl29 | spl30), inference(avatar_split_clause, [status(thm)], [p1273, sdef28, sdef29, sdef30])).
% 78.59/11.08  cnf(p283, plain, (subpopulations(first_movers,efficient_producers,sk2,sk1(sk2)) | ~spl16 | ~spl34), inference(superposition, [status(thm)], [p240, p92])).
% 78.59/11.08  cnf(p1293, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(first_movers,sk1(sk2)) = zero | greater(growth_rate(first_movers,sk1(sk2)),zero) | greater(growth_rate(efficient_producers,sk1(sk2)),zero) | ~spl16 | ~spl34), inference(resolution, [status(thm)], [p283, p39])).
% 78.59/11.08  cnf(ssp76, plain, (~spl16 | ~spl34 | spl74 | spl75 | spl76 | spl77), inference(avatar_split_clause, [status(thm)], [p1293, sdef74, sdef75, sdef76, sdef77])).
% 78.59/11.08  cnf(p1298, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(first_movers,sk1(sk2)) = zero | greater(growth_rate(first_movers,sk1(sk2)),zero) | greater(zero,growth_rate(first_movers,sk1(sk2))) | ~spl16 | ~spl34), inference(resolution, [status(thm)], [p283, p42])).
% 78.59/11.08  cnf(ssp77, plain, (~spl16 | ~spl34 | spl74 | spl75 | spl76 | spl78), inference(avatar_split_clause, [status(thm)], [p1298, sdef74, sdef75, sdef76, sdef78])).
% 78.59/11.08  cnf(p1300, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(first_movers,sk1(sk2)) = zero | greater(zero,growth_rate(efficient_producers,sk1(sk2))) | greater(growth_rate(efficient_producers,sk1(sk2)),zero) | ~spl16 | ~spl34), inference(resolution, [status(thm)], [p283, p44])).
% 78.59/11.08  cnf(ssp78, plain, (~spl16 | ~spl34 | spl74 | spl75 | spl77 | spl79), inference(avatar_split_clause, [status(thm)], [p1300, sdef74, sdef75, sdef77, sdef79])).
% 78.59/11.08  cnf(p1302, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(first_movers,sk1(sk2)) = zero | greater(zero,growth_rate(efficient_producers,sk1(sk2))) | greater(zero,growth_rate(first_movers,sk1(sk2))) | ~spl16 | ~spl34), inference(resolution, [status(thm)], [p283, p56])).
% 78.59/11.08  cnf(ssp79, plain, (~spl16 | ~spl34 | spl74 | spl75 | spl78 | spl79), inference(avatar_split_clause, [status(thm)], [p1302, sdef74, sdef75, sdef78, sdef79])).
% 78.59/11.08  cnf(p1303, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,sk1(sk2)) = zero | greater(growth_rate(first_movers,sk1(sk2)),zero) | greater(growth_rate(efficient_producers,sk1(sk2)),zero) | ~spl16 | ~spl34), inference(resolution, [status(thm)], [p283, p62])).
% 78.59/11.08  cnf(ssp80, plain, (~spl16 | ~spl34 | spl74 | spl76 | spl77 | spl80), inference(avatar_split_clause, [status(thm)], [p1303, sdef74, sdef76, sdef77, sdef80])).
% 78.59/11.08  cnf(p1305, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,sk1(sk2)) = zero | greater(growth_rate(first_movers,sk1(sk2)),zero) | greater(zero,growth_rate(first_movers,sk1(sk2))) | ~spl16 | ~spl34), inference(resolution, [status(thm)], [p283, p65])).
% 78.59/11.08  cnf(ssp81, plain, (~spl16 | ~spl34 | spl74 | spl76 | spl78 | spl80), inference(avatar_split_clause, [status(thm)], [p1305, sdef74, sdef76, sdef78, sdef80])).
% 78.59/11.08  cnf(p1306, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,sk1(sk2)) = zero | greater(zero,growth_rate(efficient_producers,sk1(sk2))) | greater(growth_rate(efficient_producers,sk1(sk2)),zero) | ~spl16 | ~spl34), inference(resolution, [status(thm)], [p283, p72])).
% 78.59/11.08  cnf(ssp82, plain, (~spl16 | ~spl34 | spl74 | spl77 | spl79 | spl80), inference(avatar_split_clause, [status(thm)], [p1306, sdef74, sdef77, sdef79, sdef80])).
% 78.59/11.08  cnf(p1307, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,sk1(sk2)) = zero | greater(zero,growth_rate(efficient_producers,sk1(sk2))) | greater(zero,growth_rate(first_movers,sk1(sk2))) | ~spl16 | ~spl34), inference(resolution, [status(thm)], [p283, p75])).
% 78.59/11.08  cnf(ssp83, plain, (~spl16 | ~spl34 | spl74 | spl78 | spl79 | spl80), inference(avatar_split_clause, [status(thm)], [p1307, sdef74, sdef78, sdef79, sdef80])).
% 78.59/11.08  cnf(p1308, plain, (~greater_or_equal(sk1(sk2),sk0(sk2)) | greater(growth_rate(efficient_producers,sk1(sk2)),growth_rate(first_movers,sk1(sk2))) | ~spl15 | ~spl16 | ~spl34), inference(resolution, [status(thm)], [p283, p85])).
% 78.59/11.08  fof(sdef82, definition, (spl82 <=> (greater(growth_rate(efficient_producers,sk1(sk2)),growth_rate(first_movers,sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl82])], [avatar_definition])).
% 78.59/11.08  cnf(ssp84, plain, (~spl15 | ~spl16 | ~spl34 | spl81 | spl82), inference(avatar_split_clause, [status(thm)], [p1308, sdef81, sdef82])).
% 78.59/11.08  cnf(p1072, plain, (subpopulations(first_movers,efficient_producers,sk2,equilibrium(sk2)) | ~spl16 | ~spl64), inference(superposition, [status(thm)], [p709, p92])).
% 78.59/11.08  cnf(p1324, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(first_movers,equilibrium(sk2)) = zero | greater(growth_rate(first_movers,equilibrium(sk2)),zero) | greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl16 | ~spl64), inference(resolution, [status(thm)], [p1072, p39])).
% 78.59/11.08  cnf(ssp85, plain, (~spl16 | ~spl64 | spl65 | spl66 | spl67 | spl68), inference(avatar_split_clause, [status(thm)], [p1324, sdef65, sdef66, sdef67, sdef68])).
% 78.59/11.08  cnf(p1325, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(first_movers,equilibrium(sk2)) = zero | greater(growth_rate(first_movers,equilibrium(sk2)),zero) | greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl16 | ~spl64), inference(resolution, [status(thm)], [p1072, p42])).
% 78.59/11.08  cnf(ssp86, plain, (~spl16 | ~spl64 | spl65 | spl66 | spl67 | spl69), inference(avatar_split_clause, [status(thm)], [p1325, sdef65, sdef66, sdef67, sdef69])).
% 78.59/11.08  cnf(p1326, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(first_movers,equilibrium(sk2)) = zero | greater(zero,growth_rate(efficient_producers,equilibrium(sk2))) | greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl16 | ~spl64), inference(resolution, [status(thm)], [p1072, p44])).
% 78.59/11.08  cnf(ssp87, plain, (~spl16 | ~spl64 | spl65 | spl66 | spl68 | spl70), inference(avatar_split_clause, [status(thm)], [p1326, sdef65, sdef66, sdef68, sdef70])).
% 78.59/11.08  cnf(p1327, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(first_movers,equilibrium(sk2)) = zero | greater(zero,growth_rate(efficient_producers,equilibrium(sk2))) | greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl16 | ~spl64), inference(resolution, [status(thm)], [p1072, p56])).
% 78.59/11.08  cnf(ssp88, plain, (~spl16 | ~spl64 | spl65 | spl66 | spl69 | spl70), inference(avatar_split_clause, [status(thm)], [p1327, sdef65, sdef66, sdef69, sdef70])).
% 78.59/11.08  cnf(p1328, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,equilibrium(sk2)) = zero | greater(growth_rate(first_movers,equilibrium(sk2)),zero) | greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl16 | ~spl64), inference(resolution, [status(thm)], [p1072, p62])).
% 78.59/11.08  cnf(ssp89, plain, (~spl16 | ~spl64 | spl65 | spl67 | spl68 | spl71), inference(avatar_split_clause, [status(thm)], [p1328, sdef65, sdef67, sdef68, sdef71])).
% 78.59/11.08  cnf(p1329, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,equilibrium(sk2)) = zero | greater(growth_rate(first_movers,equilibrium(sk2)),zero) | greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl16 | ~spl64), inference(resolution, [status(thm)], [p1072, p65])).
% 78.59/11.08  cnf(ssp90, plain, (~spl16 | ~spl64 | spl65 | spl67 | spl69 | spl71), inference(avatar_split_clause, [status(thm)], [p1329, sdef65, sdef67, sdef69, sdef71])).
% 78.59/11.08  cnf(p1330, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,equilibrium(sk2)) = zero | greater(zero,growth_rate(efficient_producers,equilibrium(sk2))) | greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl16 | ~spl64), inference(resolution, [status(thm)], [p1072, p72])).
% 78.59/11.08  cnf(ssp91, plain, (~spl16 | ~spl64 | spl65 | spl68 | spl70 | spl71), inference(avatar_split_clause, [status(thm)], [p1330, sdef65, sdef68, sdef70, sdef71])).
% 78.59/11.08  cnf(p1331, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,equilibrium(sk2)) = zero | greater(zero,growth_rate(efficient_producers,equilibrium(sk2))) | greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl16 | ~spl64), inference(resolution, [status(thm)], [p1072, p75])).
% 78.59/11.08  cnf(ssp92, plain, (~spl16 | ~spl64 | spl65 | spl69 | spl70 | spl71), inference(avatar_split_clause, [status(thm)], [p1331, sdef65, sdef69, sdef70, sdef71])).
% 78.59/11.08  cnf(p1332, plain, (~greater_or_equal(equilibrium(sk2),sk0(sk2)) | greater(growth_rate(efficient_producers,equilibrium(sk2)),growth_rate(first_movers,equilibrium(sk2))) | ~spl15 | ~spl16 | ~spl64), inference(resolution, [status(thm)], [p1072, p85])).
% 78.59/11.08  cnf(ssp93, plain, (~spl15 | ~spl16 | ~spl64 | spl72 | spl73), inference(avatar_split_clause, [status(thm)], [p1332, sdef72, sdef73])).
% 78.59/11.08  cnf(p1435, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl16 | ~spl25 | ~spl60), inference(superposition, [status(thm)], [p119, p896])).
% 78.59/11.08  cnf(p1510, plain, (greater(sk0(sk2),equilibrium(sk2)) | sk0(sk2) = equilibrium(sk2) | ~spl16 | ~spl25 | ~spl60), inference(resolution, [status(thm)], [p1435, c2])).
% 78.59/11.08  cnf(ssp94, plain, (~spl16 | ~spl25 | ~spl60 | spl30 | spl31), inference(avatar_split_clause, [status(thm)], [p1510, sdef30, sdef31])).
% 78.59/11.08  cnf(p1511, plain, (greater(sk3(equilibrium(sk2)),equilibrium(sk2)) | sk3(equilibrium(sk2)) = equilibrium(sk2) | ~spl16 | ~spl25), inference(resolution, [status(thm)], [p133, c2])).
% 78.59/11.08  cnf(ssp95, plain, (~spl16 | ~spl25 | spl41 | spl42), inference(avatar_split_clause, [status(thm)], [p1511, sdef41, sdef42])).
% 78.59/11.08  cnf(p1645, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl16 | ~spl20 | ~spl29), inference(superposition, [status(thm)], [p141, p103])).
% 78.59/11.08  cnf(p1648, plain, (~greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl16 | ~spl20 | ~spl29), inference(resolution, [status(thm)], [p1645, c21])).
% 78.59/11.08  cnf(ssp96, plain, (~spl16 | ~spl20 | ~spl29 | spl26 | spl27), inference(avatar_split_clause, [status(thm)], [p1648, sdef26, sdef27])).
% 78.59/11.08  cnf(p1712, plain, (greater_or_equal(sk1(sk2),equilibrium(sk2)) | ~spl1 | ~spl29 | ~spl58), inference(superposition, [status(thm)], [p141, p847])).
% 78.59/11.08  cnf(p1861, plain, (greater(sk1(sk2),equilibrium(sk2)) | sk1(sk2) = equilibrium(sk2) | ~spl1 | ~spl29 | ~spl58), inference(resolution, [status(thm)], [p1712, c2])).
% 78.59/11.08  cnf(ssp97, plain, (~spl1 | ~spl29 | ~spl58 | spl24 | spl25), inference(avatar_split_clause, [status(thm)], [p1861, sdef24, sdef25])).
% 78.59/11.08  cnf(p1706, plain, (sk0(sk2) = equilibrium(sk2) | ~spl29 | ~spl36), inference(superposition, [status(thm)], [p141, p247])).
% 78.59/11.08  cnf(p1843, plain, (equilibrium(sk2) = sk1(sk2) | ~spl29 | ~spl36 | ~spl58), inference(superposition, [status(thm)], [p1706, p687])).
% 78.59/11.08  cnf(p1899, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl16 | ~spl29 | ~spl36 | ~spl58), inference(superposition, [status(thm)], [p1843, p90])).
% 78.59/11.08  cnf(p1924, plain, (~greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl16 | ~spl29 | ~spl36 | ~spl58), inference(resolution, [status(thm)], [p1899, c21])).
% 78.59/11.08  cnf(ssp98, plain, (~spl16 | ~spl29 | ~spl36 | ~spl58 | spl55 | spl56), inference(avatar_split_clause, [status(thm)], [p1924, sdef55, sdef56])).
% 78.59/11.08  cnf(p107, plain, (greater_or_equal(sk3(sk0(sk2)),sk0(sk2)) | ~spl16 | ~spl20), inference(resolution, [status(thm)], [p103, c20])).
% 78.59/11.08  cnf(p1929, plain, (greater(sk3(sk0(sk2)),sk0(sk2)) | sk3(sk0(sk2)) = sk0(sk2) | ~spl16 | ~spl20), inference(resolution, [status(thm)], [p107, c2])).
% 78.59/11.08  cnf(ssp99, plain, (~spl16 | ~spl20 | spl4 | spl5), inference(avatar_split_clause, [status(thm)], [p1929, sdef4, sdef5])).
% 78.59/11.08  cnf(p187, plain, (greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl1 | ~spl29), inference(resolution, [status(thm)], [p151, c20])).
% 78.59/11.08  cnf(p1965, plain, (greater(sk3(equilibrium(sk2)),equilibrium(sk2)) | sk3(equilibrium(sk2)) = equilibrium(sk2) | ~spl1 | ~spl29), inference(resolution, [status(thm)], [p187, c2])).
% 78.59/11.08  cnf(ssp100, plain, (~spl1 | ~spl29 | spl41 | spl42), inference(avatar_split_clause, [status(thm)], [p1965, sdef41, sdef42])).
% 78.59/11.08  cnf(p850, plain, (subpopulations(first_movers,efficient_producers,sk2,sk1(sk2)) | ~spl1 | ~spl58), inference(superposition, [status(thm)], [p687, p28])).
% 78.59/11.08  cnf(p2106, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(first_movers,sk1(sk2)) = zero | greater(growth_rate(first_movers,sk1(sk2)),zero) | greater(growth_rate(efficient_producers,sk1(sk2)),zero) | ~spl1 | ~spl58), inference(resolution, [status(thm)], [p850, p39])).
% 78.59/11.08  cnf(ssp101, plain, (~spl1 | ~spl58 | spl74 | spl75 | spl76 | spl77), inference(avatar_split_clause, [status(thm)], [p2106, sdef74, sdef75, sdef76, sdef77])).
% 78.59/11.08  cnf(p2107, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(first_movers,sk1(sk2)) = zero | greater(growth_rate(first_movers,sk1(sk2)),zero) | greater(zero,growth_rate(first_movers,sk1(sk2))) | ~spl1 | ~spl58), inference(resolution, [status(thm)], [p850, p42])).
% 78.59/11.08  cnf(ssp102, plain, (~spl1 | ~spl58 | spl74 | spl75 | spl76 | spl78), inference(avatar_split_clause, [status(thm)], [p2107, sdef74, sdef75, sdef76, sdef78])).
% 78.59/11.08  cnf(p2109, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(first_movers,sk1(sk2)) = zero | greater(zero,growth_rate(efficient_producers,sk1(sk2))) | greater(growth_rate(efficient_producers,sk1(sk2)),zero) | ~spl1 | ~spl58), inference(resolution, [status(thm)], [p850, p44])).
% 78.59/11.08  cnf(ssp103, plain, (~spl1 | ~spl58 | spl74 | spl75 | spl77 | spl79), inference(avatar_split_clause, [status(thm)], [p2109, sdef74, sdef75, sdef77, sdef79])).
% 78.59/11.08  cnf(p2110, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(first_movers,sk1(sk2)) = zero | greater(zero,growth_rate(efficient_producers,sk1(sk2))) | greater(zero,growth_rate(first_movers,sk1(sk2))) | ~spl1 | ~spl58), inference(resolution, [status(thm)], [p850, p56])).
% 78.59/11.08  cnf(ssp104, plain, (~spl1 | ~spl58 | spl74 | spl75 | spl78 | spl79), inference(avatar_split_clause, [status(thm)], [p2110, sdef74, sdef75, sdef78, sdef79])).
% 78.59/11.08  cnf(p2111, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,sk1(sk2)) = zero | greater(growth_rate(first_movers,sk1(sk2)),zero) | greater(growth_rate(efficient_producers,sk1(sk2)),zero) | ~spl1 | ~spl58), inference(resolution, [status(thm)], [p850, p62])).
% 78.59/11.08  cnf(ssp105, plain, (~spl1 | ~spl58 | spl74 | spl76 | spl77 | spl80), inference(avatar_split_clause, [status(thm)], [p2111, sdef74, sdef76, sdef77, sdef80])).
% 78.59/11.08  cnf(p2112, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,sk1(sk2)) = zero | greater(growth_rate(first_movers,sk1(sk2)),zero) | greater(zero,growth_rate(first_movers,sk1(sk2))) | ~spl1 | ~spl58), inference(resolution, [status(thm)], [p850, p65])).
% 78.59/11.08  cnf(ssp106, plain, (~spl1 | ~spl58 | spl74 | spl76 | spl78 | spl80), inference(avatar_split_clause, [status(thm)], [p2112, sdef74, sdef76, sdef78, sdef80])).
% 78.59/11.08  cnf(p2113, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,sk1(sk2)) = zero | greater(zero,growth_rate(efficient_producers,sk1(sk2))) | greater(growth_rate(efficient_producers,sk1(sk2)),zero) | ~spl1 | ~spl58), inference(resolution, [status(thm)], [p850, p72])).
% 78.59/11.08  cnf(ssp107, plain, (~spl1 | ~spl58 | spl74 | spl77 | spl79 | spl80), inference(avatar_split_clause, [status(thm)], [p2113, sdef74, sdef77, sdef79, sdef80])).
% 78.59/11.08  cnf(p2114, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | growth_rate(efficient_producers,sk1(sk2)) = zero | greater(zero,growth_rate(efficient_producers,sk1(sk2))) | greater(zero,growth_rate(first_movers,sk1(sk2))) | ~spl1 | ~spl58), inference(resolution, [status(thm)], [p850, p75])).
% 78.59/11.08  cnf(ssp108, plain, (~spl1 | ~spl58 | spl74 | spl78 | spl79 | spl80), inference(avatar_split_clause, [status(thm)], [p2114, sdef74, sdef78, sdef79, sdef80])).
% 78.59/11.08  cnf(p2115, plain, (~greater_or_equal(sk1(sk2),sk0(sk2)) | greater(growth_rate(efficient_producers,sk1(sk2)),growth_rate(first_movers,sk1(sk2))) | ~spl1 | ~spl15 | ~spl58), inference(resolution, [status(thm)], [p850, p85])).
% 78.59/11.08  cnf(ssp109, plain, (~spl1 | ~spl15 | ~spl58 | spl81 | spl82), inference(avatar_split_clause, [status(thm)], [p2115, sdef81, sdef82])).
% 78.59/11.08  cnf(sat_ref, plain, $false, inference(avatar_sat_refutation, [status(thm)], [ssp0, ssp1, ssp2, ssp3, ssp4, ssp5, ssp6, ssp7, ssp8, ssp9, ssp10, ssp11, ssp12, ssp13, ssp14, ssp15, ssp16, ssp17, ssp18, ssp19, ssp20, ssp21, ssp22, ssp23, ssp24, ssp25, ssp26, ssp27, ssp28, ssp29, ssp30, ssp31, ssp32, ssp33, ssp34, ssp35, ssp36, ssp37, ssp38, ssp39, ssp40, ssp41, ssp42, ssp43, ssp44, ssp45, ssp46, ssp47, ssp48, ssp49, ssp50, ssp51, ssp52, ssp53, ssp54, ssp55, ssp56, ssp57, ssp58, ssp59, ssp60, ssp61, ssp62, ssp63, ssp64, ssp65, ssp66, ssp67, ssp68, ssp69, ssp70, ssp71, ssp72, ssp73, ssp74, ssp75, ssp76, ssp77, ssp78, ssp79, ssp80, ssp81, ssp82, ssp83, ssp84, ssp85, ssp86, ssp87, ssp88, ssp89, ssp90, ssp91, ssp92, ssp93, ssp94, ssp95, ssp96, ssp97, ssp98, ssp99, ssp100, ssp101, ssp102, ssp103, ssp104, ssp105, ssp106, ssp107, ssp108, ssp109, sct0, sct1, sct2, sct3, sct4, sct5, sct6, sct7, sct8, sct9, sct10, sct11, sct12, sct13, sct14, sct15, sct16, sct17, sct18, sct19, sct20, sct21, sct22, sct23, sct24, sct25, sct26, sct27, sct28, sct29, sct30, sct31, sct32, sct33, sct34, sct35, sct36, sct37, sct38, sct39, sct40, sct41, sct42, sct43, sct44, sct45, sct46, sct47, sct48, sct49, sct50, sct51, sct52, sct53, sct54, sct55, sct56, sct57, sct58, sct59, sct60, sct61, sct62, sct63, sct64, sct65, sct66, sct67, sct68, sct69, sct70, sct71, sct72, sct73, sct74, sct75, sct76, sct77, sct78, sct79, sct80, sct81, sct82, sct83, sct84, sct85, sct86, sct87, sct88, sct89, sct90, sct91, sct92, sct93, sct94, sct95, sct96, sct97, sct98, sct99, sct100, sct101, sct102, sct103, sct104, sct105, sct106, sct107, sct108, sct109, sct110, sct111, sct112, sct113])).
% 78.59/11.08  % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------