%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT035+1 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.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:34 PM UTC 2026
% Result : Theorem 78.39s 10.59s
% Output : Proof 78.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT035+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.56 % Computer : n017.cluster.edu
% 0.10/0.56 % Model : x86_64 x86_64
% 0.10/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.56 % Memory : 8046.5625MB
% 0.10/0.56 % OS : Linux 6.8.0-71-generic
% 0.10/0.56 % CPULimit : 300
% 0.10/0.56 % WCLimit : 300
% 0.10/0.56 % DateTime : Thu Sep 24 01:03:02 UTC 2026
% 0.10/0.57 % CPUTime :
% 0.10/0.57 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 78.39/10.59 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 78.39/10.59 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 78.39/10.59 fof(sdef0, definition, (spl0 <=> (~stable(sk2))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 78.39/10.59 cnf(p27, plain, (~stable(sk2) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 78.39/10.59 fof(f7, conjecture, ! [E] : ( ( environment(E) & stable(E) ) => ? [To] : ( in_environment(E,To) & ! [T] : ( ( subpopulations(first_movers,efficient_producers,E,T) & greater_or_equal(T,To) ) => outcompetes(efficient_producers,first_movers,T) ) ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_t4)).
% 78.39/10.59 fof(f7_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) ) => outcompetes(efficient_producers,first_movers,T) ) ) )), inference(negated_conjecture, [status(cth)], [f7])).
% 78.39/10.59 fof(f7_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)) & ~(outcompetes(efficient_producers,first_movers,T)))))))), inference(nnf_transformation, [status(thm)], [f7_neg])).
% 78.39/10.59 fof(f7_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)) & ~(outcompetes(efficient_producers,first_movers,sk3(To))))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk2,sk3])], [f7_nnf])).
% 78.39/10.59 cnf(c21, plain, stable(sk2), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 78.39/10.59 cnf(p29, plain, ($false | ~spl0), inference(resolution, [status(thm)], [p27, c21])).
% 78.39/10.59 cnf(sct0, plain, (~spl0), inference(avatar_contradiction_clause, [status(thm)], [p29])).
% 78.39/10.59 fof(sdef9, definition, (spl9 <=> (outcompetes(efficient_producers,first_movers,sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 78.39/10.59 cnf(p51, plain, (outcompetes(efficient_producers,first_movers,sk0(sk2)) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 78.39/10.59 fof(sdef3, definition, (spl3 <=> (sk3(sk0(sk2)) = sk0(sk2))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 78.39/10.59 cnf(p36, plain, (sk3(sk0(sk2)) = sk0(sk2) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 78.39/10.59 fof(sdef1, definition, (spl1 <=> (in_environment(sk2,sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 78.39/10.59 cnf(p28, plain, (in_environment(sk2,sk0(sk2)) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 78.39/10.59 cnf(c24, plain, ~in_environment(sk2,X1) | ~outcompetes(efficient_producers,first_movers,sk3(X1)), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 78.39/10.59 cnf(p31, plain, (~outcompetes(efficient_producers,first_movers,sk3(sk0(sk2))) | ~spl1), inference(resolution, [status(thm)], [p28, c24])).
% 78.39/10.59 cnf(p39, plain, (~outcompetes(efficient_producers,first_movers,sk0(sk2)) | ~spl1 | ~spl3), inference(superposition, [status(thm)], [p36, p31])).
% 78.39/10.59 cnf(p53, plain, ($false | ~spl1 | ~spl3 | ~spl9), inference(resolution, [status(thm)], [p51, p39])).
% 78.39/10.59 cnf(sct1, plain, (~spl1 | ~spl3 | ~spl9), inference(avatar_contradiction_clause, [status(thm)], [p53])).
% 78.39/10.59 fof(sdef6, definition, (spl6 <=> (outcompetes(efficient_producers,first_movers,sk3(sk0(sk2))))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 78.39/10.59 cnf(p47, plain, (outcompetes(efficient_producers,first_movers,sk3(sk0(sk2))) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 78.39/10.59 cnf(p54, plain, ($false | ~spl1 | ~spl6), inference(resolution, [status(thm)], [p47, p31])).
% 78.39/10.59 cnf(sct2, plain, (~spl1 | ~spl6), inference(avatar_contradiction_clause, [status(thm)], [p54])).
% 78.39/10.59 fof(sdef11, definition, (spl11 <=> (growth_rate(first_movers,sk3(sk0(sk2))) = zero)), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 78.39/10.59 cnf(p58, plain, (growth_rate(first_movers,sk3(sk0(sk2))) = zero | ~spl11), inference(avatar_component_clause, [status(thm)], [sdef11])).
% 78.39/10.59 fof(sdef12, definition, (spl12 <=> (greater(growth_rate(first_movers,sk3(sk0(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 78.39/10.59 cnf(p59, plain, (greater(growth_rate(first_movers,sk3(sk0(sk2))),zero) | ~spl12), inference(avatar_component_clause, [status(thm)], [sdef12])).
% 78.39/10.59 cnf(p65, plain, (greater(zero,zero) | ~spl11 | ~spl12), inference(superposition, [status(thm)], [p58, p59])).
% 78.39/10.59 fof(sdef5, definition, (spl5 <=> (~greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 78.39/10.59 cnf(p46, plain, (~greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 78.39/10.59 cnf(p62, plain, (~greater(zero,zero) | ~spl5 | ~spl11), inference(superposition, [status(thm)], [p58, p46])).
% 78.39/10.59 cnf(p67, plain, ($false | ~spl5 | ~spl11 | ~spl12), inference(resolution, [status(thm)], [p65, p62])).
% 78.39/10.59 cnf(sct3, plain, (~spl5 | ~spl11 | ~spl12), inference(avatar_contradiction_clause, [status(thm)], [p67])).
% 78.39/10.59 fof(sdef13, definition, (spl13 <=> (greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 78.39/10.59 cnf(p60, plain, (greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl13), inference(avatar_component_clause, [status(thm)], [sdef13])).
% 78.39/10.59 fof(f2, axiom, ! [X,Y] : ( greater_or_equal(X,Y) <=> ( greater(X,Y) | X = Y ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_greater_or_equal)).
% 78.39/10.59 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.39/10.59 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.39/10.59 cnf(c3, plain, greater_or_equal(X0,X1) | ~greater(X0,X1), inference(cnf_transformation, [status(esa)], [f2_sk])).
% 78.39/10.59 cnf(p69, plain, (greater_or_equal(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl13), inference(resolution, [status(thm)], [p60, c3])).
% 78.39/10.59 fof(sdef4, definition, (spl4 <=> (~greater_or_equal(growth_rate(efficient_producers,sk3(sk0(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 78.39/10.59 cnf(p45, plain, (~greater_or_equal(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 78.39/10.59 cnf(p70, plain, ($false | ~spl4 | ~spl13), inference(resolution, [status(thm)], [p69, p45])).
% 78.39/10.59 cnf(sct4, plain, (~spl4 | ~spl13), inference(avatar_contradiction_clause, [status(thm)], [p70])).
% 78.39/10.59 fof(sdef16, definition, (spl16 <=> (growth_rate(efficient_producers,sk3(sk0(sk2))) = zero)), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 78.39/10.59 cnf(p92, plain, (growth_rate(efficient_producers,sk3(sk0(sk2))) = zero | ~spl16), inference(avatar_component_clause, [status(thm)], [sdef16])).
% 78.39/10.59 cnf(p93, plain, (~greater_or_equal(zero,zero) | ~spl4 | ~spl16), inference(superposition, [status(thm)], [p92, p45])).
% 78.39/10.59 cnf(c4, plain, greater_or_equal(X0,X1) | X0 != X1, inference(cnf_transformation, [status(esa)], [f2_sk])).
% 78.39/10.59 cnf(p25, plain, greater_or_equal(X0,X0), inference(equality_resolution, [status(thm)], [c4])).
% 78.39/10.59 cnf(p95, plain, ($false | ~spl4 | ~spl16), inference(resolution, [status(thm)], [p93, p25])).
% 78.39/10.59 cnf(sct5, plain, (~spl4 | ~spl16), inference(avatar_contradiction_clause, [status(thm)], [p95])).
% 78.39/10.59 fof(sdef18, definition, (spl18 <=> (~greater_or_equal(sk3(sk0(sk2)),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 78.39/10.59 cnf(p100, plain, (~greater_or_equal(sk3(sk0(sk2)),sk0(sk2)) | ~spl18), inference(avatar_component_clause, [status(thm)], [sdef18])).
% 78.39/10.59 cnf(c23, plain, ~in_environment(sk2,X1) | greater_or_equal(sk3(X1),X1), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 78.39/10.59 cnf(p30, plain, (greater_or_equal(sk3(sk0(sk2)),sk0(sk2)) | ~spl1), inference(resolution, [status(thm)], [p28, c23])).
% 78.39/10.59 cnf(p102, plain, ($false | ~spl1 | ~spl18), inference(resolution, [status(thm)], [p100, p30])).
% 78.39/10.59 cnf(sct6, plain, (~spl1 | ~spl18), inference(avatar_contradiction_clause, [status(thm)], [p102])).
% 78.39/10.59 fof(sdef19, definition, (spl19 <=> (greater(growth_rate(efficient_producers,sk3(sk0(sk2))),growth_rate(first_movers,sk3(sk0(sk2)))))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 78.39/10.59 cnf(p101, plain, (greater(growth_rate(efficient_producers,sk3(sk0(sk2))),growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl19), inference(avatar_component_clause, [status(thm)], [sdef19])).
% 78.39/10.59 cnf(p105, plain, (greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl11 | ~spl19), inference(superposition, [status(thm)], [p58, p101])).
% 78.39/10.59 cnf(p109, plain, (greater_or_equal(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl11 | ~spl19), inference(resolution, [status(thm)], [p105, c3])).
% 78.39/10.59 cnf(p324, plain, ($false | ~spl4 | ~spl11 | ~spl19), inference(resolution, [status(thm)], [p109, p45])).
% 78.39/10.59 cnf(sct7, plain, (~spl4 | ~spl11 | ~spl19), inference(avatar_contradiction_clause, [status(thm)], [p324])).
% 78.39/10.59 fof(sdef28, definition, (spl28 <=> (equilibrium(sk2) = sk0(sk2))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 78.39/10.59 cnf(p158, plain, (equilibrium(sk2) = sk0(sk2) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 78.39/10.59 cnf(p211, plain, (greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl1 | ~spl28), inference(superposition, [status(thm)], [p158, p30])).
% 78.39/10.59 fof(sdef10, definition, (spl10 <=> (~greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 78.39/10.59 cnf(p57, plain, (~greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 78.39/10.59 cnf(p538, plain, ($false | ~spl1 | ~spl10 | ~spl28), inference(resolution, [status(thm)], [p211, p57])).
% 78.39/10.59 cnf(sct8, plain, (~spl1 | ~spl10 | ~spl28), inference(avatar_contradiction_clause, [status(thm)], [p538])).
% 78.39/10.59 fof(sdef30, definition, (spl30 <=> (sk0(sk2) = equilibrium(sk2))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 78.39/10.59 cnf(p161, plain, (sk0(sk2) = equilibrium(sk2) | ~spl30), inference(avatar_component_clause, [status(thm)], [sdef30])).
% 78.39/10.59 cnf(p286, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl10 | ~spl30), inference(superposition, [status(thm)], [p161, p57])).
% 78.39/10.59 cnf(p276, plain, (greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl1 | ~spl30), inference(superposition, [status(thm)], [p161, p30])).
% 78.39/10.59 cnf(p593, plain, ($false | ~spl1 | ~spl10 | ~spl30), inference(resolution, [status(thm)], [p286, p276])).
% 78.39/10.59 cnf(sct9, plain, (~spl1 | ~spl10 | ~spl30), inference(avatar_contradiction_clause, [status(thm)], [p593])).
% 78.39/10.59 fof(sdef14, definition, (spl14 <=> (greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 78.39/10.59 cnf(p73, plain, (greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl14), inference(avatar_component_clause, [status(thm)], [sdef14])).
% 78.39/10.59 cnf(p601, plain, ($false | ~spl5 | ~spl14), inference(resolution, [status(thm)], [p46, p73])).
% 78.39/10.59 cnf(sct10, plain, (~spl5 | ~spl14), inference(avatar_contradiction_clause, [status(thm)], [p601])).
% 78.39/10.59 fof(sdef35, definition, (spl35 <=> (outcompetes(efficient_producers,first_movers,sk3(sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 78.39/10.59 cnf(p334, plain, (outcompetes(efficient_producers,first_movers,sk3(sk1(sk2))) | ~spl35), inference(avatar_component_clause, [status(thm)], [sdef35])).
% 78.39/10.59 fof(sdef20, definition, (spl20 <=> (in_environment(sk2,sk1(sk2)))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 78.39/10.59 cnf(p112, plain, (in_environment(sk2,sk1(sk2)) | ~spl20), inference(avatar_component_clause, [status(thm)], [sdef20])).
% 78.39/10.59 cnf(p114, plain, (~outcompetes(efficient_producers,first_movers,sk3(sk1(sk2))) | ~spl20), inference(resolution, [status(thm)], [p112, c24])).
% 78.39/10.59 cnf(p673, plain, ($false | ~spl20 | ~spl35), inference(resolution, [status(thm)], [p334, p114])).
% 78.39/10.59 cnf(sct11, plain, (~spl20 | ~spl35), inference(avatar_contradiction_clause, [status(thm)], [p673])).
% 78.39/10.59 fof(sdef26, definition, (spl26 <=> (sk1(sk2) = equilibrium(sk2))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 78.39/10.59 cnf(p138, plain, (sk1(sk2) = equilibrium(sk2) | ~spl26), inference(avatar_component_clause, [status(thm)], [sdef26])).
% 78.39/10.59 fof(sdef32, definition, (spl32 <=> (sk3(sk1(sk2)) = sk1(sk2))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 78.39/10.59 cnf(p328, plain, (sk3(sk1(sk2)) = sk1(sk2) | ~spl32), inference(avatar_component_clause, [status(thm)], [sdef32])).
% 78.39/10.59 cnf(p648, plain, (~outcompetes(efficient_producers,first_movers,sk1(sk2)) | ~spl20 | ~spl32), inference(superposition, [status(thm)], [p328, p114])).
% 78.39/10.59 cnf(p665, plain, (~outcompetes(efficient_producers,first_movers,equilibrium(sk2)) | ~spl20 | ~spl26 | ~spl32), inference(superposition, [status(thm)], [p138, p648])).
% 78.39/10.59 fof(sdef47, definition, (spl47 <=> (equilibrium(sk2) = sk1(sk2))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 78.39/10.59 cnf(p358, plain, (equilibrium(sk2) = sk1(sk2) | ~spl47), inference(avatar_component_clause, [status(thm)], [sdef47])).
% 78.39/10.59 fof(sdef45, definition, (spl45 <=> (sk0(sk2) = sk1(sk2))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 78.39/10.59 cnf(p355, plain, (sk0(sk2) = sk1(sk2) | ~spl45), inference(avatar_component_clause, [status(thm)], [sdef45])).
% 78.39/10.59 cnf(p410, plain, (sk0(sk2) = equilibrium(sk2) | ~spl45 | ~spl47), inference(superposition, [status(thm)], [p358, p355])).
% 78.39/10.59 cnf(p481, plain, (outcompetes(efficient_producers,first_movers,equilibrium(sk2)) | ~spl9 | ~spl45 | ~spl47), inference(superposition, [status(thm)], [p410, p51])).
% 78.39/10.59 cnf(p675, plain, ($false | ~spl9 | ~spl20 | ~spl26 | ~spl32 | ~spl45 | ~spl47), inference(resolution, [status(thm)], [p665, p481])).
% 78.39/10.59 cnf(sct12, plain, (~spl9 | ~spl20 | ~spl26 | ~spl32 | ~spl45 | ~spl47), inference(avatar_contradiction_clause, [status(thm)], [p675])).
% 78.39/10.59 fof(sdef36, definition, (spl36 <=> (~greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 78.39/10.59 cnf(p336, plain, (~greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | ~spl36), inference(avatar_component_clause, [status(thm)], [sdef36])).
% 78.39/10.59 cnf(p679, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | ~spl32 | ~spl36), inference(superposition, [status(thm)], [p328, p336])).
% 78.39/10.59 fof(sdef24, definition, (spl24 <=> (greater_or_equal(sk1(sk2),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 78.39/10.59 cnf(p126, plain, (greater_or_equal(sk1(sk2),equilibrium(sk2)) | ~spl24), inference(avatar_component_clause, [status(thm)], [sdef24])).
% 78.39/10.59 cnf(p680, plain, ($false | ~spl24 | ~spl32 | ~spl36), inference(resolution, [status(thm)], [p679, p126])).
% 78.39/10.59 cnf(sct13, plain, (~spl24 | ~spl32 | ~spl36), inference(avatar_contradiction_clause, [status(thm)], [p680])).
% 78.39/10.59 fof(sdef37, definition, (spl37 <=> (growth_rate(first_movers,sk3(sk1(sk2))) = zero)), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 78.39/10.59 cnf(p337, plain, (growth_rate(first_movers,sk3(sk1(sk2))) = zero | ~spl37), inference(avatar_component_clause, [status(thm)], [sdef37])).
% 78.39/10.59 fof(sdef34, definition, (spl34 <=> (~greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 78.39/10.59 cnf(p333, plain, (~greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl34), inference(avatar_component_clause, [status(thm)], [sdef34])).
% 78.39/10.59 cnf(p684, plain, (~greater(zero,zero) | ~spl34 | ~spl37), inference(superposition, [status(thm)], [p337, p333])).
% 78.39/10.59 fof(f0, axiom, ! [X,Y,Z] : ( ( greater(X,Y) & greater(Y,Z) ) => greater(X,Z) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_greater_transitivity)).
% 78.39/10.59 fof(f0_nnf, plain, ! [X,Y,Z] : (((~(greater(X,Y)) | ~(greater(Y,Z))) | greater(X,Z))), inference(nnf_transformation, [status(thm)], [f0])).
% 78.39/10.59 fof(f0_sk, plain, ! [X,Y,Z] : (((~(greater(X,Y)) | ~(greater(Y,Z))) | greater(X,Z))), inference(skolemisation, [status(esa)], [f0_nnf])).
% 78.39/10.59 cnf(c0, plain, ~greater(X0,X1) | ~greater(X1,X2) | greater(X0,X2), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 78.39/10.59 cnf(p74, plain, (~greater(growth_rate(first_movers,sk3(sk0(sk2))),X0) | greater(zero,X0) | ~spl14), inference(resolution, [status(thm)], [p73, c0])).
% 78.39/10.59 cnf(p79, plain, (greater(zero,zero) | ~spl12 | ~spl14), inference(resolution, [status(thm)], [p74, p59])).
% 78.39/10.59 cnf(p685, plain, ($false | ~spl12 | ~spl14 | ~spl34 | ~spl37), inference(resolution, [status(thm)], [p684, p79])).
% 78.39/10.59 cnf(sct14, plain, (~spl12 | ~spl14 | ~spl34 | ~spl37), inference(avatar_contradiction_clause, [status(thm)], [p685])).
% 78.39/10.59 fof(sdef38, definition, (spl38 <=> (greater(growth_rate(first_movers,sk3(sk1(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 78.39/10.59 cnf(p338, plain, (greater(growth_rate(first_movers,sk3(sk1(sk2))),zero) | ~spl38), inference(avatar_component_clause, [status(thm)], [sdef38])).
% 78.39/10.59 cnf(p691, plain, (greater(zero,zero) | ~spl37 | ~spl38), inference(superposition, [status(thm)], [p337, p338])).
% 78.39/10.59 cnf(p692, plain, ($false | ~spl34 | ~spl37 | ~spl38), inference(resolution, [status(thm)], [p691, p684])).
% 78.39/10.59 cnf(sct15, plain, (~spl34 | ~spl37 | ~spl38), inference(avatar_contradiction_clause, [status(thm)], [p692])).
% 78.39/10.59 cnf(p113, plain, (greater_or_equal(sk3(sk1(sk2)),sk1(sk2)) | ~spl20), inference(resolution, [status(thm)], [p112, c23])).
% 78.39/10.59 cnf(p371, plain, (greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | ~spl20 | ~spl45), inference(superposition, [status(thm)], [p355, p113])).
% 78.39/10.59 fof(sdef43, definition, (spl43 <=> (~greater_or_equal(sk3(sk1(sk2)),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 78.39/10.59 cnf(p349, plain, (~greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | ~spl43), inference(avatar_component_clause, [status(thm)], [sdef43])).
% 78.39/10.59 cnf(p712, plain, ($false | ~spl20 | ~spl43 | ~spl45), inference(resolution, [status(thm)], [p371, p349])).
% 78.39/10.59 cnf(sct16, plain, (~spl20 | ~spl43 | ~spl45), inference(avatar_contradiction_clause, [status(thm)], [p712])).
% 78.39/10.59 cnf(p404, plain, (greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | ~spl20 | ~spl47), inference(superposition, [status(thm)], [p358, p113])).
% 78.39/10.59 cnf(p724, plain, ($false | ~spl20 | ~spl36 | ~spl47), inference(resolution, [status(thm)], [p404, p336])).
% 78.39/10.59 cnf(sct17, plain, (~spl20 | ~spl36 | ~spl47), inference(avatar_contradiction_clause, [status(thm)], [p724])).
% 78.39/10.59 fof(sdef42, definition, (spl42 <=> (growth_rate(efficient_producers,sk3(sk1(sk2))) = zero)), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 78.39/10.59 cnf(p346, plain, (growth_rate(efficient_producers,sk3(sk1(sk2))) = zero | ~spl42), inference(avatar_component_clause, [status(thm)], [sdef42])).
% 78.39/10.59 fof(sdef33, definition, (spl33 <=> (~greater_or_equal(growth_rate(efficient_producers,sk3(sk1(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 78.39/10.59 cnf(p332, plain, (~greater_or_equal(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl33), inference(avatar_component_clause, [status(thm)], [sdef33])).
% 78.39/10.59 cnf(p733, plain, (~greater_or_equal(zero,zero) | ~spl33 | ~spl42), inference(superposition, [status(thm)], [p346, p332])).
% 78.39/10.59 cnf(p736, plain, ($false | ~spl33 | ~spl42), inference(resolution, [status(thm)], [p733, p25])).
% 78.39/10.59 cnf(sct18, plain, (~spl33 | ~spl42), inference(avatar_contradiction_clause, [status(thm)], [p736])).
% 78.39/10.59 fof(sdef51, definition, (spl51 <=> (sk3(sk0(sk2)) = equilibrium(sk2))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 78.39/10.59 cnf(p537, plain, (sk3(sk0(sk2)) = equilibrium(sk2) | ~spl51), inference(avatar_component_clause, [status(thm)], [sdef51])).
% 78.39/10.59 cnf(p745, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | ~spl10 | ~spl51), inference(superposition, [status(thm)], [p537, p57])).
% 78.39/10.59 cnf(p779, plain, ($false | ~spl10 | ~spl51), inference(resolution, [status(thm)], [p745, p25])).
% 78.39/10.59 cnf(sct19, plain, (~spl10 | ~spl51), inference(avatar_contradiction_clause, [status(thm)], [p779])).
% 78.39/10.59 fof(sdef29, definition, (spl29 <=> (greater(sk0(sk2),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 78.39/10.59 cnf(p159, plain, (greater(sk0(sk2),equilibrium(sk2)) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 78.39/10.59 fof(sdef2, definition, (spl2 <=> (greater(sk3(sk0(sk2)),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 78.39/10.59 cnf(p35, plain, (greater(sk3(sk0(sk2)),sk0(sk2)) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 78.39/10.59 cnf(p37, plain, (~greater(sk0(sk2),X0) | greater(sk3(sk0(sk2)),X0) | ~spl2), inference(resolution, [status(thm)], [p35, c0])).
% 78.39/10.59 cnf(p272, plain, (greater(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl2 | ~spl29), inference(resolution, [status(thm)], [p159, p37])).
% 78.39/10.59 cnf(p553, plain, (greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl2 | ~spl29), inference(resolution, [status(thm)], [p272, c3])).
% 78.39/10.59 cnf(p786, plain, ($false | ~spl2 | ~spl10 | ~spl29), inference(resolution, [status(thm)], [p553, p57])).
% 78.39/10.59 cnf(sct20, plain, (~spl2 | ~spl10 | ~spl29), inference(avatar_contradiction_clause, [status(thm)], [p786])).
% 78.39/10.59 cnf(p103, plain, (~greater(growth_rate(first_movers,sk3(sk0(sk2))),X0) | greater(growth_rate(efficient_producers,sk3(sk0(sk2))),X0) | ~spl19), inference(resolution, [status(thm)], [p101, c0])).
% 78.39/10.59 cnf(p163, plain, (greater(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl12 | ~spl19), inference(resolution, [status(thm)], [p103, p59])).
% 78.39/10.59 cnf(p458, plain, (greater_or_equal(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~spl12 | ~spl19), inference(resolution, [status(thm)], [p163, c3])).
% 78.39/10.59 cnf(p800, plain, ($false | ~spl4 | ~spl12 | ~spl19), inference(resolution, [status(thm)], [p458, p45])).
% 78.39/10.59 cnf(sct21, plain, (~spl4 | ~spl12 | ~spl19), inference(avatar_contradiction_clause, [status(thm)], [p800])).
% 78.39/10.59 fof(sdef49, definition, (spl49 <=> (sk3(equilibrium(sk2)) = sk0(sk2))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 78.39/10.59 cnf(p534, plain, (sk3(equilibrium(sk2)) = sk0(sk2) | ~spl49), inference(avatar_component_clause, [status(thm)], [sdef49])).
% 78.39/10.59 fof(sdef53, definition, (spl53 <=> (sk3(equilibrium(sk2)) = equilibrium(sk2))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 78.39/10.59 cnf(p559, plain, (sk3(equilibrium(sk2)) = equilibrium(sk2) | ~spl53), inference(avatar_component_clause, [status(thm)], [sdef53])).
% 78.39/10.59 cnf(p803, plain, (sk0(sk2) = equilibrium(sk2) | ~spl49 | ~spl53), inference(superposition, [status(thm)], [p534, p559])).
% 78.39/10.59 cnf(p812, plain, (outcompetes(efficient_producers,first_movers,equilibrium(sk2)) | ~spl9 | ~spl49 | ~spl53), inference(superposition, [status(thm)], [p803, p51])).
% 78.39/10.59 cnf(p809, plain, (~outcompetes(efficient_producers,first_movers,equilibrium(sk2)) | ~spl1 | ~spl49 | ~spl53), inference(superposition, [status(thm)], [p803, p31])).
% 78.39/10.59 cnf(p846, plain, ($false | ~spl1 | ~spl9 | ~spl49 | ~spl53), inference(resolution, [status(thm)], [p812, p809])).
% 78.39/10.59 cnf(sct22, plain, (~spl1 | ~spl9 | ~spl49 | ~spl53), inference(avatar_contradiction_clause, [status(thm)], [p846])).
% 78.39/10.59 cnf(p816, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | ~spl10 | ~spl49 | ~spl53), inference(superposition, [status(thm)], [p803, p57])).
% 78.39/10.59 cnf(p847, plain, ($false | ~spl10 | ~spl49 | ~spl53), inference(resolution, [status(thm)], [p816, p25])).
% 78.39/10.59 cnf(sct23, plain, (~spl10 | ~spl49 | ~spl53), inference(avatar_contradiction_clause, [status(thm)], [p847])).
% 78.39/10.59 fof(sdef57, definition, (spl57 <=> (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 78.39/10.59 cnf(p570, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl57), inference(avatar_component_clause, [status(thm)], [sdef57])).
% 78.39/10.59 cnf(p850, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | ~spl53 | ~spl57), inference(superposition, [status(thm)], [p559, p570])).
% 78.39/10.59 cnf(p851, plain, ($false | ~spl53 | ~spl57), inference(resolution, [status(thm)], [p850, p25])).
% 78.39/10.59 cnf(sct24, plain, (~spl53 | ~spl57), inference(avatar_contradiction_clause, [status(thm)], [p851])).
% 78.39/10.59 fof(sdef58, definition, (spl58 <=> (growth_rate(first_movers,sk3(equilibrium(sk2))) = zero)), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 78.39/10.59 cnf(p571, plain, (growth_rate(first_movers,sk3(equilibrium(sk2))) = zero | ~spl58), inference(avatar_component_clause, [status(thm)], [sdef58])).
% 78.39/10.59 fof(sdef55, definition, (spl55 <=> (~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 78.39/10.59 cnf(p567, plain, (~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl55), inference(avatar_component_clause, [status(thm)], [sdef55])).
% 78.39/10.59 cnf(p880, plain, (~greater(zero,zero) | ~spl55 | ~spl58), inference(superposition, [status(thm)], [p571, p567])).
% 78.39/10.59 cnf(p881, plain, ($false | ~spl37 | ~spl38 | ~spl55 | ~spl58), inference(resolution, [status(thm)], [p880, p691])).
% 78.39/10.59 cnf(sct25, plain, (~spl37 | ~spl38 | ~spl55 | ~spl58), inference(avatar_contradiction_clause, [status(thm)], [p881])).
% 78.39/10.59 fof(sdef66, definition, (spl66 <=> (sk3(sk0(sk2)) = sk1(sk2))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 78.39/10.59 cnf(p708, plain, (sk3(sk0(sk2)) = sk1(sk2) | ~spl66), inference(avatar_component_clause, [status(thm)], [sdef66])).
% 78.39/10.59 cnf(p860, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | ~spl10 | ~spl66), inference(superposition, [status(thm)], [p708, p57])).
% 78.39/10.59 cnf(p882, plain, ($false | ~spl10 | ~spl24 | ~spl66), inference(resolution, [status(thm)], [p860, p126])).
% 78.39/10.59 cnf(sct26, plain, (~spl10 | ~spl24 | ~spl66), inference(avatar_contradiction_clause, [status(thm)], [p882])).
% 78.39/10.59 fof(sdef59, definition, (spl59 <=> (greater(growth_rate(first_movers,sk3(equilibrium(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 78.39/10.59 cnf(p572, plain, (greater(growth_rate(first_movers,sk3(equilibrium(sk2))),zero) | ~spl59), inference(avatar_component_clause, [status(thm)], [sdef59])).
% 78.39/10.59 cnf(p887, plain, (greater(zero,zero) | ~spl58 | ~spl59), inference(superposition, [status(thm)], [p571, p572])).
% 78.39/10.59 cnf(p888, plain, ($false | ~spl55 | ~spl58 | ~spl59), inference(resolution, [status(thm)], [p887, p880])).
% 78.39/10.59 cnf(sct27, plain, (~spl55 | ~spl58 | ~spl59), inference(avatar_contradiction_clause, [status(thm)], [p888])).
% 78.39/10.59 fof(sdef68, definition, (spl68 <=> (sk3(sk1(sk2)) = sk0(sk2))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 78.39/10.59 cnf(p711, plain, (sk3(sk1(sk2)) = sk0(sk2) | ~spl68), inference(avatar_component_clause, [status(thm)], [sdef68])).
% 78.39/10.59 cnf(p890, plain, (~outcompetes(efficient_producers,first_movers,sk0(sk2)) | ~spl20 | ~spl68), inference(superposition, [status(thm)], [p711, p114])).
% 78.39/10.59 cnf(p903, plain, ($false | ~spl9 | ~spl20 | ~spl68), inference(resolution, [status(thm)], [p890, p51])).
% 78.39/10.59 cnf(sct28, plain, (~spl9 | ~spl20 | ~spl68), inference(avatar_contradiction_clause, [status(thm)], [p903])).
% 78.39/10.59 cnf(p896, plain, (~greater_or_equal(sk0(sk2),sk0(sk2)) | ~spl43 | ~spl68), inference(superposition, [status(thm)], [p711, p349])).
% 78.39/10.59 cnf(p911, plain, ($false | ~spl43 | ~spl68), inference(resolution, [status(thm)], [p896, p25])).
% 78.39/10.59 cnf(sct29, plain, (~spl43 | ~spl68), inference(avatar_contradiction_clause, [status(thm)], [p911])).
% 78.39/10.59 fof(sdef70, definition, (spl70 <=> (sk3(equilibrium(sk2)) = sk1(sk2))), introduced(definition, [new_symbols(naming, [spl70])], [avatar_definition])).
% 78.39/10.59 cnf(p720, plain, (sk3(equilibrium(sk2)) = sk1(sk2) | ~spl70), inference(avatar_component_clause, [status(thm)], [sdef70])).
% 78.39/10.59 cnf(p921, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | ~spl57 | ~spl70), inference(superposition, [status(thm)], [p720, p570])).
% 78.39/10.59 cnf(p940, plain, ($false | ~spl24 | ~spl57 | ~spl70), inference(resolution, [status(thm)], [p921, p126])).
% 78.39/10.59 cnf(sct30, plain, (~spl24 | ~spl57 | ~spl70), inference(avatar_contradiction_clause, [status(thm)], [p940])).
% 78.39/10.59 fof(sdef63, definition, (spl63 <=> (growth_rate(efficient_producers,sk3(equilibrium(sk2))) = zero)), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 78.39/10.59 cnf(p580, plain, (growth_rate(efficient_producers,sk3(equilibrium(sk2))) = zero | ~spl63), inference(avatar_component_clause, [status(thm)], [sdef63])).
% 78.39/10.59 fof(sdef54, definition, (spl54 <=> (~greater_or_equal(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 78.39/10.59 cnf(p566, plain, (~greater_or_equal(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~spl54), inference(avatar_component_clause, [status(thm)], [sdef54])).
% 78.39/10.59 cnf(p941, plain, (~greater_or_equal(zero,zero) | ~spl54 | ~spl63), inference(superposition, [status(thm)], [p580, p566])).
% 78.39/10.59 cnf(p945, plain, ($false | ~spl54 | ~spl63), inference(resolution, [status(thm)], [p941, p25])).
% 78.39/10.59 cnf(sct31, plain, (~spl54 | ~spl63), inference(avatar_contradiction_clause, [status(thm)], [p945])).
% 78.39/10.59 fof(sdef72, definition, (spl72 <=> (sk3(sk1(sk2)) = equilibrium(sk2))), introduced(definition, [new_symbols(naming, [spl72])], [avatar_definition])).
% 78.39/10.59 cnf(p723, plain, (sk3(sk1(sk2)) = equilibrium(sk2) | ~spl72), inference(avatar_component_clause, [status(thm)], [sdef72])).
% 78.39/10.59 cnf(p976, plain, (~greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl43 | ~spl72), inference(superposition, [status(thm)], [p723, p349])).
% 78.39/10.59 fof(sdef27, definition, (spl27 <=> (greater(equilibrium(sk2),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 78.39/10.59 cnf(p157, plain, (greater(equilibrium(sk2),sk0(sk2)) | ~spl27), inference(avatar_component_clause, [status(thm)], [sdef27])).
% 78.39/10.59 cnf(p206, plain, (greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl27), inference(resolution, [status(thm)], [p157, c3])).
% 78.39/10.59 cnf(p987, plain, ($false | ~spl27 | ~spl43 | ~spl72), inference(resolution, [status(thm)], [p976, p206])).
% 78.39/10.59 cnf(sct32, plain, (~spl27 | ~spl43 | ~spl72), inference(avatar_contradiction_clause, [status(thm)], [p987])).
% 78.39/10.59 fof(sdef23, definition, (spl23 <=> (greater(sk0(sk2),sk1(sk2)))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 78.39/10.59 cnf(p120, plain, (greater(sk0(sk2),sk1(sk2)) | ~spl23), inference(avatar_component_clause, [status(thm)], [sdef23])).
% 78.39/10.59 cnf(p131, plain, (~greater(sk1(sk2),X0) | greater(sk0(sk2),X0) | ~spl23), inference(resolution, [status(thm)], [p120, c0])).
% 78.39/10.59 fof(sdef25, definition, (spl25 <=> (greater(sk1(sk2),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 78.39/10.59 cnf(p137, plain, (greater(sk1(sk2),equilibrium(sk2)) | ~spl25), inference(avatar_component_clause, [status(thm)], [sdef25])).
% 78.39/10.59 cnf(p417, plain, (greater(sk0(sk2),equilibrium(sk2)) | ~spl23 | ~spl25), inference(resolution, [status(thm)], [p131, p137])).
% 78.39/10.59 cnf(p525, plain, (greater(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl2 | ~spl23 | ~spl25), inference(resolution, [status(thm)], [p417, p37])).
% 78.39/10.59 cnf(p729, plain, (greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl2 | ~spl23 | ~spl25), inference(resolution, [status(thm)], [p525, c3])).
% 78.39/10.59 cnf(p995, plain, ($false | ~spl2 | ~spl10 | ~spl23 | ~spl25), inference(resolution, [status(thm)], [p729, p57])).
% 78.39/10.59 cnf(sct33, plain, (~spl2 | ~spl10 | ~spl23 | ~spl25), inference(avatar_contradiction_clause, [status(thm)], [p995])).
% 78.39/10.59 fof(sdef50, definition, (spl50 <=> (greater(sk3(sk0(sk2)),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 78.39/10.59 cnf(p536, plain, (greater(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl50), inference(avatar_component_clause, [status(thm)], [sdef50])).
% 78.39/10.59 cnf(p738, plain, (greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl50), inference(resolution, [status(thm)], [p536, c3])).
% 78.39/10.59 cnf(p996, plain, ($false | ~spl10 | ~spl50), inference(resolution, [status(thm)], [p738, p57])).
% 78.39/10.59 cnf(sct34, plain, (~spl10 | ~spl50), inference(avatar_contradiction_clause, [status(thm)], [p996])).
% 78.39/10.59 fof(sdef39, definition, (spl39 <=> (greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 78.39/10.59 cnf(p339, plain, (greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl39), inference(avatar_component_clause, [status(thm)], [sdef39])).
% 78.39/10.59 cnf(p695, plain, (greater_or_equal(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl39), inference(resolution, [status(thm)], [p339, c3])).
% 78.39/10.59 cnf(p997, plain, ($false | ~spl33 | ~spl39), inference(resolution, [status(thm)], [p695, p332])).
% 78.39/10.59 cnf(sct35, plain, (~spl33 | ~spl39), inference(avatar_contradiction_clause, [status(thm)], [p997])).
% 78.39/10.59 fof(sdef46, definition, (spl46 <=> (greater(equilibrium(sk2),sk1(sk2)))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 78.39/10.59 cnf(p357, plain, (greater(equilibrium(sk2),sk1(sk2)) | ~spl46), inference(avatar_component_clause, [status(thm)], [sdef46])).
% 78.39/10.59 cnf(p392, plain, (~greater(sk1(sk2),X0) | greater(equilibrium(sk2),X0) | ~spl46), inference(resolution, [status(thm)], [p357, c0])).
% 78.39/10.59 fof(sdef21, definition, (spl21 <=> (greater(sk1(sk2),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 78.39/10.59 cnf(p118, plain, (greater(sk1(sk2),sk0(sk2)) | ~spl21), inference(avatar_component_clause, [status(thm)], [sdef21])).
% 78.39/10.59 cnf(p780, plain, (greater(equilibrium(sk2),sk0(sk2)) | ~spl21 | ~spl46), inference(resolution, [status(thm)], [p392, p118])).
% 78.39/10.59 cnf(p784, plain, (greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl21 | ~spl46), inference(resolution, [status(thm)], [p780, c3])).
% 78.39/10.59 cnf(p998, plain, ($false | ~spl21 | ~spl43 | ~spl46 | ~spl72), inference(resolution, [status(thm)], [p976, p784])).
% 78.39/10.59 cnf(sct36, plain, (~spl21 | ~spl43 | ~spl46 | ~spl72), inference(avatar_contradiction_clause, [status(thm)], [p998])).
% 78.39/10.59 fof(sdef67, definition, (spl67 <=> (greater(sk3(sk1(sk2)),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 78.39/10.59 cnf(p710, plain, (greater(sk3(sk1(sk2)),sk0(sk2)) | ~spl67), inference(avatar_component_clause, [status(thm)], [sdef67])).
% 78.39/10.59 cnf(p884, plain, (greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | ~spl67), inference(resolution, [status(thm)], [p710, c3])).
% 78.39/10.59 cnf(p1000, plain, ($false | ~spl43 | ~spl67), inference(resolution, [status(thm)], [p884, p349])).
% 78.39/10.59 cnf(sct37, plain, (~spl43 | ~spl67), inference(avatar_contradiction_clause, [status(thm)], [p1000])).
% 78.39/10.59 fof(sdef71, definition, (spl71 <=> (greater(sk3(sk1(sk2)),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl71])], [avatar_definition])).
% 78.39/10.59 cnf(p722, plain, (greater(sk3(sk1(sk2)),equilibrium(sk2)) | ~spl71), inference(avatar_component_clause, [status(thm)], [sdef71])).
% 78.39/10.59 cnf(p961, plain, (greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | ~spl71), inference(resolution, [status(thm)], [p722, c3])).
% 78.39/10.59 cnf(p1022, plain, ($false | ~spl36 | ~spl71), inference(resolution, [status(thm)], [p961, p336])).
% 78.39/10.59 cnf(sct38, plain, (~spl36 | ~spl71), inference(avatar_contradiction_clause, [status(thm)], [p1022])).
% 78.39/10.59 fof(sdef31, definition, (spl31 <=> (greater(sk3(sk1(sk2)),sk1(sk2)))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 78.39/10.59 cnf(p327, plain, (greater(sk3(sk1(sk2)),sk1(sk2)) | ~spl31), inference(avatar_component_clause, [status(thm)], [sdef31])).
% 78.39/10.59 cnf(p602, plain, (~greater(sk1(sk2),X0) | greater(sk3(sk1(sk2)),X0) | ~spl31), inference(resolution, [status(thm)], [p327, c0])).
% 78.39/10.59 cnf(p955, plain, (greater(sk3(sk1(sk2)),sk0(sk2)) | ~spl21 | ~spl31), inference(resolution, [status(thm)], [p602, p118])).
% 78.39/10.59 cnf(p1013, plain, (greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | ~spl21 | ~spl31), inference(resolution, [status(thm)], [p955, c3])).
% 78.39/10.59 cnf(p1025, plain, ($false | ~spl21 | ~spl31 | ~spl43), inference(resolution, [status(thm)], [p1013, p349])).
% 78.39/10.59 cnf(sct39, plain, (~spl21 | ~spl31 | ~spl43), inference(avatar_contradiction_clause, [status(thm)], [p1025])).
% 78.39/10.59 cnf(p1037, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | ~spl36 | ~spl72), inference(superposition, [status(thm)], [p723, p336])).
% 78.39/10.59 cnf(p1048, plain, ($false | ~spl36 | ~spl72), inference(resolution, [status(thm)], [p1037, p25])).
% 78.39/10.59 cnf(sct40, plain, (~spl36 | ~spl72), inference(avatar_contradiction_clause, [status(thm)], [p1048])).
% 78.39/10.59 cnf(p956, plain, (greater(sk3(sk1(sk2)),equilibrium(sk2)) | ~spl25 | ~spl31), inference(resolution, [status(thm)], [p602, p137])).
% 78.39/10.59 cnf(p1015, plain, (greater_or_equal(sk3(sk1(sk2)),equilibrium(sk2)) | ~spl25 | ~spl31), inference(resolution, [status(thm)], [p956, c3])).
% 78.39/10.59 cnf(p1052, plain, ($false | ~spl25 | ~spl31 | ~spl36), inference(resolution, [status(thm)], [p1015, p336])).
% 78.39/10.59 cnf(sct41, plain, (~spl25 | ~spl31 | ~spl36), inference(avatar_contradiction_clause, [status(thm)], [p1052])).
% 78.39/10.59 fof(sdef56, definition, (spl56 <=> (outcompetes(efficient_producers,first_movers,sk3(equilibrium(sk2))))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 78.39/10.59 cnf(p568, plain, (outcompetes(efficient_producers,first_movers,sk3(equilibrium(sk2))) | ~spl56), inference(avatar_component_clause, [status(thm)], [sdef56])).
% 78.39/10.59 cnf(p919, plain, (outcompetes(efficient_producers,first_movers,sk1(sk2)) | ~spl56 | ~spl70), inference(superposition, [status(thm)], [p720, p568])).
% 78.39/10.59 cnf(p1053, plain, ($false | ~spl20 | ~spl32 | ~spl56 | ~spl70), inference(resolution, [status(thm)], [p648, p919])).
% 78.39/10.59 cnf(sct42, plain, (~spl20 | ~spl32 | ~spl56 | ~spl70), inference(avatar_contradiction_clause, [status(thm)], [p1053])).
% 78.39/10.59 fof(sdef75, definition, (spl75 <=> (outcompetes(efficient_producers,first_movers,equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl75])], [avatar_definition])).
% 78.39/10.59 cnf(p1078, plain, (outcompetes(efficient_producers,first_movers,equilibrium(sk2)) | ~spl75), inference(avatar_component_clause, [status(thm)], [sdef75])).
% 78.39/10.59 cnf(p970, plain, (~outcompetes(efficient_producers,first_movers,equilibrium(sk2)) | ~spl20 | ~spl72), inference(superposition, [status(thm)], [p723, p114])).
% 78.39/10.59 cnf(p1097, plain, ($false | ~spl20 | ~spl72 | ~spl75), inference(resolution, [status(thm)], [p1078, p970])).
% 78.39/10.59 cnf(sct43, plain, (~spl20 | ~spl72 | ~spl75), inference(avatar_contradiction_clause, [status(thm)], [p1097])).
% 78.39/10.59 fof(sdef76, definition, (spl76 <=> (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl76])], [avatar_definition])).
% 78.39/10.59 cnf(p1080, plain, (~greater_or_equal(equilibrium(sk2),equilibrium(sk2)) | ~spl76), inference(avatar_component_clause, [status(thm)], [sdef76])).
% 78.39/10.59 cnf(p1098, plain, ($false | ~spl76), inference(resolution, [status(thm)], [p1080, p25])).
% 78.39/10.59 cnf(sct44, plain, (~spl76), inference(avatar_contradiction_clause, [status(thm)], [p1098])).
% 78.39/10.59 fof(sdef83, definition, (spl83 <=> (~greater_or_equal(equilibrium(sk2),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl83])], [avatar_definition])).
% 78.39/10.59 cnf(p1093, plain, (~greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl83), inference(avatar_component_clause, [status(thm)], [sdef83])).
% 78.39/10.59 cnf(p1099, plain, ($false | ~spl27 | ~spl83), inference(resolution, [status(thm)], [p1093, p206])).
% 78.39/10.59 cnf(sct45, plain, (~spl27 | ~spl83), inference(avatar_contradiction_clause, [status(thm)], [p1099])).
% 78.39/10.59 fof(sdef77, definition, (spl77 <=> (growth_rate(first_movers,equilibrium(sk2)) = zero)), introduced(definition, [new_symbols(naming, [spl77])], [avatar_definition])).
% 78.39/10.59 cnf(p1081, plain, (growth_rate(first_movers,equilibrium(sk2)) = zero | ~spl77), inference(avatar_component_clause, [status(thm)], [sdef77])).
% 78.39/10.59 fof(sdef74, definition, (spl74 <=> (~greater(zero,growth_rate(first_movers,equilibrium(sk2))))), introduced(definition, [new_symbols(naming, [spl74])], [avatar_definition])).
% 78.39/10.59 cnf(p1077, plain, (~greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl74), inference(avatar_component_clause, [status(thm)], [sdef74])).
% 78.39/10.59 cnf(p1135, plain, (~greater(zero,zero) | ~spl74 | ~spl77), inference(superposition, [status(thm)], [p1081, p1077])).
% 78.39/10.59 cnf(p1136, plain, ($false | ~spl58 | ~spl59 | ~spl74 | ~spl77), inference(resolution, [status(thm)], [p1135, p887])).
% 78.39/10.59 cnf(sct46, plain, (~spl58 | ~spl59 | ~spl74 | ~spl77), inference(avatar_contradiction_clause, [status(thm)], [p1136])).
% 78.39/10.59 fof(sdef60, definition, (spl60 <=> (greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 78.39/10.59 cnf(p573, plain, (greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~spl60), inference(avatar_component_clause, [status(thm)], [sdef60])).
% 78.39/10.59 cnf(p942, plain, (greater(zero,zero) | ~spl60 | ~spl63), inference(superposition, [status(thm)], [p580, p573])).
% 78.39/10.59 cnf(p1137, plain, ($false | ~spl60 | ~spl63 | ~spl74 | ~spl77), inference(resolution, [status(thm)], [p1135, p942])).
% 78.39/10.59 cnf(sct47, plain, (~spl60 | ~spl63 | ~spl74 | ~spl77), inference(avatar_contradiction_clause, [status(thm)], [p1137])).
% 78.39/10.59 fof(sdef62, definition, (spl62 <=> (greater(zero,growth_rate(efficient_producers,sk3(equilibrium(sk2)))))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 78.39/10.59 cnf(p577, plain, (greater(zero,growth_rate(efficient_producers,sk3(equilibrium(sk2)))) | ~spl62), inference(avatar_component_clause, [status(thm)], [sdef62])).
% 78.39/10.59 cnf(p944, plain, (greater(zero,zero) | ~spl62 | ~spl63), inference(superposition, [status(thm)], [p580, p577])).
% 78.39/10.59 cnf(p1138, plain, ($false | ~spl62 | ~spl63 | ~spl74 | ~spl77), inference(resolution, [status(thm)], [p1135, p944])).
% 78.39/10.59 cnf(sct48, plain, (~spl62 | ~spl63 | ~spl74 | ~spl77), inference(avatar_contradiction_clause, [status(thm)], [p1138])).
% 78.39/10.59 fof(sdef40, definition, (spl40 <=> (greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 78.39/10.59 cnf(p341, plain, (greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl40), inference(avatar_component_clause, [status(thm)], [sdef40])).
% 78.39/10.59 cnf(p713, plain, (~greater(growth_rate(first_movers,sk3(sk1(sk2))),X0) | greater(zero,X0) | ~spl40), inference(resolution, [status(thm)], [p341, c0])).
% 78.39/10.59 cnf(p999, plain, (greater(zero,zero) | ~spl38 | ~spl40), inference(resolution, [status(thm)], [p713, p338])).
% 78.39/10.59 cnf(p1139, plain, ($false | ~spl38 | ~spl40 | ~spl74 | ~spl77), inference(resolution, [status(thm)], [p1135, p999])).
% 78.39/10.59 cnf(sct49, plain, (~spl38 | ~spl40 | ~spl74 | ~spl77), inference(avatar_contradiction_clause, [status(thm)], [p1139])).
% 78.39/10.59 fof(sdef61, definition, (spl61 <=> (greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 78.39/10.59 cnf(p575, plain, (greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl61), inference(avatar_component_clause, [status(thm)], [sdef61])).
% 78.39/10.59 cnf(p914, plain, (~greater(growth_rate(first_movers,sk3(equilibrium(sk2))),X0) | greater(zero,X0) | ~spl61), inference(resolution, [status(thm)], [p575, c0])).
% 78.39/10.59 cnf(p1130, plain, (greater(zero,zero) | ~spl59 | ~spl61), inference(resolution, [status(thm)], [p914, p572])).
% 78.39/10.59 cnf(p1140, plain, ($false | ~spl59 | ~spl61 | ~spl74 | ~spl77), inference(resolution, [status(thm)], [p1135, p1130])).
% 78.39/10.59 cnf(sct50, plain, (~spl59 | ~spl61 | ~spl74 | ~spl77), inference(avatar_contradiction_clause, [status(thm)], [p1140])).
% 78.39/10.59 fof(sdef78, definition, (spl78 <=> (greater(growth_rate(first_movers,equilibrium(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl78])], [avatar_definition])).
% 78.39/10.59 cnf(p1082, plain, (greater(growth_rate(first_movers,equilibrium(sk2)),zero) | ~spl78), inference(avatar_component_clause, [status(thm)], [sdef78])).
% 78.39/10.59 cnf(p1143, plain, (greater(zero,zero) | ~spl77 | ~spl78), inference(superposition, [status(thm)], [p1081, p1082])).
% 78.39/10.59 cnf(p1144, plain, ($false | ~spl74 | ~spl77 | ~spl78), inference(resolution, [status(thm)], [p1143, p1135])).
% 78.39/10.59 cnf(sct51, plain, (~spl74 | ~spl77 | ~spl78), inference(avatar_contradiction_clause, [status(thm)], [p1144])).
% 78.39/10.59 fof(sdef82, definition, (spl82 <=> (growth_rate(efficient_producers,equilibrium(sk2)) = zero)), introduced(definition, [new_symbols(naming, [spl82])], [avatar_definition])).
% 78.39/10.59 cnf(p1090, plain, (growth_rate(efficient_producers,equilibrium(sk2)) = zero | ~spl82), inference(avatar_component_clause, [status(thm)], [sdef82])).
% 78.39/10.59 fof(sdef73, definition, (spl73 <=> (~greater_or_equal(growth_rate(efficient_producers,equilibrium(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl73])], [avatar_definition])).
% 78.39/10.59 cnf(p1076, plain, (~greater_or_equal(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl73), inference(avatar_component_clause, [status(thm)], [sdef73])).
% 78.39/10.59 cnf(p1160, plain, (~greater_or_equal(zero,zero) | ~spl73 | ~spl82), inference(superposition, [status(thm)], [p1090, p1076])).
% 78.39/10.59 cnf(p1166, plain, ($false | ~spl73 | ~spl82), inference(resolution, [status(thm)], [p1160, p25])).
% 78.39/10.59 cnf(sct52, plain, (~spl73 | ~spl82), inference(avatar_contradiction_clause, [status(thm)], [p1166])).
% 78.39/10.59 fof(sdef65, definition, (spl65 <=> (greater(sk3(sk0(sk2)),sk1(sk2)))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 78.39/10.59 cnf(p707, plain, (greater(sk3(sk0(sk2)),sk1(sk2)) | ~spl65), inference(avatar_component_clause, [status(thm)], [sdef65])).
% 78.39/10.59 cnf(p852, plain, (~greater(sk1(sk2),X0) | greater(sk3(sk0(sk2)),X0) | ~spl65), inference(resolution, [status(thm)], [p707, c0])).
% 78.39/10.59 cnf(p1056, plain, (greater(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl25 | ~spl65), inference(resolution, [status(thm)], [p852, p137])).
% 78.39/10.59 cnf(p1127, plain, (greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl25 | ~spl65), inference(resolution, [status(thm)], [p1056, c3])).
% 78.39/10.59 cnf(p1184, plain, ($false | ~spl10 | ~spl25 | ~spl65), inference(resolution, [status(thm)], [p1127, p57])).
% 78.39/10.59 cnf(sct53, plain, (~spl10 | ~spl25 | ~spl65), inference(avatar_contradiction_clause, [status(thm)], [p1184])).
% 78.39/10.59 fof(sdef44, definition, (spl44 <=> (greater(growth_rate(efficient_producers,sk3(sk1(sk2))),growth_rate(first_movers,sk3(sk1(sk2)))))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 78.39/10.59 cnf(p350, plain, (greater(growth_rate(efficient_producers,sk3(sk1(sk2))),growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl44), inference(avatar_component_clause, [status(thm)], [sdef44])).
% 78.39/10.59 cnf(p773, plain, (~greater(growth_rate(first_movers,sk3(sk1(sk2))),X0) | greater(growth_rate(efficient_producers,sk3(sk1(sk2))),X0) | ~spl44), inference(resolution, [status(thm)], [p350, c0])).
% 78.39/10.59 cnf(p1024, plain, (greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl38 | ~spl44), inference(resolution, [status(thm)], [p773, p338])).
% 78.39/10.59 cnf(p1224, plain, (greater_or_equal(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl38 | ~spl44), inference(resolution, [status(thm)], [p1024, c3])).
% 78.39/10.59 cnf(p1248, plain, ($false | ~spl33 | ~spl38 | ~spl44), inference(resolution, [status(thm)], [p1224, p332])).
% 78.39/10.59 cnf(sct54, plain, (~spl33 | ~spl38 | ~spl44), inference(avatar_contradiction_clause, [status(thm)], [p1248])).
% 78.39/10.59 cnf(p1249, plain, ($false | ~spl34 | ~spl40), inference(resolution, [status(thm)], [p333, p341])).
% 78.39/10.59 cnf(sct55, plain, (~spl34 | ~spl40), inference(avatar_contradiction_clause, [status(thm)], [p1249])).
% 78.39/10.59 fof(sdef41, definition, (spl41 <=> (greater(zero,growth_rate(efficient_producers,sk3(sk1(sk2)))))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 78.39/10.59 cnf(p343, plain, (greater(zero,growth_rate(efficient_producers,sk3(sk1(sk2)))) | ~spl41), inference(avatar_component_clause, [status(thm)], [sdef41])).
% 78.39/10.59 cnf(p725, plain, (~greater(growth_rate(efficient_producers,sk3(sk1(sk2))),X0) | greater(zero,X0) | ~spl41), inference(resolution, [status(thm)], [p343, c0])).
% 78.39/10.59 cnf(p1005, plain, (greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl41 | ~spl44), inference(resolution, [status(thm)], [p725, p350])).
% 78.39/10.59 cnf(p1250, plain, ($false | ~spl34 | ~spl41 | ~spl44), inference(resolution, [status(thm)], [p333, p1005])).
% 78.39/10.59 cnf(sct56, plain, (~spl34 | ~spl41 | ~spl44), inference(avatar_contradiction_clause, [status(thm)], [p1250])).
% 78.39/10.59 cnf(p1251, plain, ($false | ~spl34 | ~spl37 | ~spl58 | ~spl59), inference(resolution, [status(thm)], [p684, p887])).
% 78.39/10.59 cnf(sct57, plain, (~spl34 | ~spl37 | ~spl58 | ~spl59), inference(avatar_contradiction_clause, [status(thm)], [p1251])).
% 78.39/10.59 cnf(p1252, plain, ($false | ~spl34 | ~spl37 | ~spl60 | ~spl63), inference(resolution, [status(thm)], [p684, p942])).
% 78.39/10.59 cnf(sct58, plain, (~spl34 | ~spl37 | ~spl60 | ~spl63), inference(avatar_contradiction_clause, [status(thm)], [p1252])).
% 78.39/10.59 cnf(p1253, plain, ($false | ~spl34 | ~spl37 | ~spl62 | ~spl63), inference(resolution, [status(thm)], [p684, p944])).
% 78.39/10.59 cnf(sct59, plain, (~spl34 | ~spl37 | ~spl62 | ~spl63), inference(avatar_contradiction_clause, [status(thm)], [p1253])).
% 78.39/10.59 cnf(p1254, plain, ($false | ~spl34 | ~spl37 | ~spl59 | ~spl61), inference(resolution, [status(thm)], [p684, p1130])).
% 78.39/10.59 cnf(sct60, plain, (~spl34 | ~spl37 | ~spl59 | ~spl61), inference(avatar_contradiction_clause, [status(thm)], [p1254])).
% 78.39/10.59 cnf(p1255, plain, ($false | ~spl34 | ~spl37 | ~spl77 | ~spl78), inference(resolution, [status(thm)], [p684, p1143])).
% 78.39/10.59 cnf(sct61, plain, (~spl34 | ~spl37 | ~spl77 | ~spl78), inference(avatar_contradiction_clause, [status(thm)], [p1255])).
% 78.39/10.59 fof(sdef79, definition, (spl79 <=> (greater(growth_rate(efficient_producers,equilibrium(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl79])], [avatar_definition])).
% 78.39/10.59 cnf(p1083, plain, (greater(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl79), inference(avatar_component_clause, [status(thm)], [sdef79])).
% 78.39/10.59 cnf(p1161, plain, (greater(zero,zero) | ~spl79 | ~spl82), inference(superposition, [status(thm)], [p1090, p1083])).
% 78.39/10.59 cnf(p1256, plain, ($false | ~spl34 | ~spl37 | ~spl79 | ~spl82), inference(resolution, [status(thm)], [p684, p1161])).
% 78.39/10.59 cnf(sct62, plain, (~spl34 | ~spl37 | ~spl79 | ~spl82), inference(avatar_contradiction_clause, [status(thm)], [p1256])).
% 78.39/10.59 fof(sdef81, definition, (spl81 <=> (greater(zero,growth_rate(efficient_producers,equilibrium(sk2))))), introduced(definition, [new_symbols(naming, [spl81])], [avatar_definition])).
% 78.39/10.59 cnf(p1087, plain, (greater(zero,growth_rate(efficient_producers,equilibrium(sk2))) | ~spl81), inference(avatar_component_clause, [status(thm)], [sdef81])).
% 78.39/10.59 cnf(p1162, plain, (greater(zero,zero) | ~spl81 | ~spl82), inference(superposition, [status(thm)], [p1090, p1087])).
% 78.39/10.59 cnf(p1257, plain, ($false | ~spl34 | ~spl37 | ~spl81 | ~spl82), inference(resolution, [status(thm)], [p684, p1162])).
% 78.39/10.59 cnf(sct63, plain, (~spl34 | ~spl37 | ~spl81 | ~spl82), inference(avatar_contradiction_clause, [status(thm)], [p1257])).
% 78.39/10.59 cnf(p734, plain, (greater(zero,zero) | ~spl39 | ~spl42), inference(superposition, [status(thm)], [p346, p339])).
% 78.39/10.59 cnf(p1258, plain, ($false | ~spl34 | ~spl37 | ~spl39 | ~spl42), inference(resolution, [status(thm)], [p684, p734])).
% 78.39/10.59 cnf(sct64, plain, (~spl34 | ~spl37 | ~spl39 | ~spl42), inference(avatar_contradiction_clause, [status(thm)], [p1258])).
% 78.39/10.59 fof(sdef80, definition, (spl80 <=> (greater(zero,growth_rate(first_movers,equilibrium(sk2))))), introduced(definition, [new_symbols(naming, [spl80])], [avatar_definition])).
% 78.39/10.59 cnf(p1085, plain, (greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl80), inference(avatar_component_clause, [status(thm)], [sdef80])).
% 78.39/10.59 cnf(p1259, plain, ($false | ~spl74 | ~spl80), inference(resolution, [status(thm)], [p1077, p1085])).
% 78.39/10.59 cnf(sct65, plain, (~spl74 | ~spl80), inference(avatar_contradiction_clause, [status(thm)], [p1259])).
% 78.39/10.59 cnf(p775, plain, (greater(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~spl37 | ~spl44), inference(superposition, [status(thm)], [p337, p350])).
% 78.39/10.59 cnf(p1262, plain, (greater(zero,zero) | ~spl37 | ~spl42 | ~spl44), inference(superposition, [status(thm)], [p346, p775])).
% 78.39/10.59 cnf(p1263, plain, ($false | ~spl34 | ~spl37 | ~spl42 | ~spl44), inference(resolution, [status(thm)], [p1262, p684])).
% 78.39/10.59 cnf(sct66, plain, (~spl34 | ~spl37 | ~spl42 | ~spl44), inference(avatar_contradiction_clause, [status(thm)], [p1263])).
% 78.39/10.59 cnf(p1271, plain, (~greater_or_equal(sk1(sk2),sk0(sk2)) | ~spl32 | ~spl43), inference(superposition, [status(thm)], [p328, p349])).
% 78.39/10.59 cnf(p122, plain, (greater_or_equal(sk1(sk2),sk0(sk2)) | ~spl21), inference(resolution, [status(thm)], [p118, c3])).
% 78.39/10.59 cnf(p1312, plain, ($false | ~spl21 | ~spl32 | ~spl43), inference(resolution, [status(thm)], [p1271, p122])).
% 78.39/10.59 cnf(sct67, plain, (~spl21 | ~spl32 | ~spl43), inference(avatar_contradiction_clause, [status(thm)], [p1312])).
% 78.39/10.59 fof(sdef88, definition, (spl88 <=> (~greater_or_equal(sk1(sk2),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl88])], [avatar_definition])).
% 78.39/10.59 cnf(p1295, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | ~spl88), inference(avatar_component_clause, [status(thm)], [sdef88])).
% 78.39/10.59 cnf(p1404, plain, ($false | ~spl24 | ~spl88), inference(resolution, [status(thm)], [p1295, p126])).
% 78.39/10.59 cnf(sct68, plain, (~spl24 | ~spl88), inference(avatar_contradiction_clause, [status(thm)], [p1404])).
% 78.39/10.59 fof(sdef95, definition, (spl95 <=> (~greater_or_equal(sk1(sk2),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl95])], [avatar_definition])).
% 78.39/10.59 cnf(p1308, plain, (~greater_or_equal(sk1(sk2),sk0(sk2)) | ~spl95), inference(avatar_component_clause, [status(thm)], [sdef95])).
% 78.39/10.59 cnf(p1411, plain, ($false | ~spl21 | ~spl95), inference(resolution, [status(thm)], [p1308, p122])).
% 78.39/10.59 cnf(sct69, plain, (~spl21 | ~spl95), inference(avatar_contradiction_clause, [status(thm)], [p1411])).
% 78.39/10.59 cnf(p144, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl20 | ~spl26), inference(superposition, [status(thm)], [p138, p112])).
% 78.39/10.59 cnf(p153, plain, (~outcompetes(efficient_producers,first_movers,sk3(equilibrium(sk2))) | ~spl20 | ~spl26), inference(resolution, [status(thm)], [p144, c24])).
% 78.39/10.59 cnf(p1418, plain, ($false | ~spl20 | ~spl26 | ~spl56), inference(resolution, [status(thm)], [p153, p568])).
% 78.39/10.59 cnf(sct70, plain, (~spl20 | ~spl26 | ~spl56), inference(avatar_contradiction_clause, [status(thm)], [p1418])).
% 78.39/10.59 cnf(p1419, plain, (~outcompetes(efficient_producers,first_movers,equilibrium(sk2)) | ~spl20 | ~spl26 | ~spl70), inference(superposition, [status(thm)], [p720, p153])).
% 78.39/10.59 cnf(p1420, plain, ($false | ~spl20 | ~spl26 | ~spl70 | ~spl75), inference(resolution, [status(thm)], [p1419, p1078])).
% 78.39/10.59 cnf(sct71, plain, (~spl20 | ~spl26 | ~spl70 | ~spl75), inference(avatar_contradiction_clause, [status(thm)], [p1420])).
% 78.39/10.59 cnf(p676, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl26 | ~spl36), inference(superposition, [status(thm)], [p138, p336])).
% 78.39/10.59 cnf(p152, plain, (greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl20 | ~spl26), inference(resolution, [status(thm)], [p144, c23])).
% 78.39/10.59 cnf(p1421, plain, ($false | ~spl20 | ~spl26 | ~spl36), inference(resolution, [status(thm)], [p676, p152])).
% 78.39/10.59 cnf(sct72, plain, (~spl20 | ~spl26 | ~spl36), inference(avatar_contradiction_clause, [status(thm)], [p1421])).
% 78.39/10.59 cnf(p1422, plain, (~greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl26 | ~spl95), inference(superposition, [status(thm)], [p138, p1308])).
% 78.39/10.59 cnf(p1423, plain, ($false | ~spl26 | ~spl27 | ~spl95), inference(resolution, [status(thm)], [p1422, p206])).
% 78.39/10.59 cnf(sct73, plain, (~spl26 | ~spl27 | ~spl95), inference(avatar_contradiction_clause, [status(thm)], [p1423])).
% 78.39/10.59 cnf(p960, plain, (~greater(equilibrium(sk2),X0) | greater(sk3(sk1(sk2)),X0) | ~spl71), inference(resolution, [status(thm)], [p722, c0])).
% 78.39/10.59 cnf(p1190, plain, (greater(sk3(sk1(sk2)),sk0(sk2)) | ~spl27 | ~spl71), inference(resolution, [status(thm)], [p960, p157])).
% 78.39/10.59 cnf(p1199, plain, (greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | ~spl27 | ~spl71), inference(resolution, [status(thm)], [p1190, c3])).
% 78.39/10.59 cnf(p1424, plain, ($false | ~spl27 | ~spl43 | ~spl71), inference(resolution, [status(thm)], [p349, p1199])).
% 78.39/10.59 cnf(sct74, plain, (~spl27 | ~spl43 | ~spl71), inference(avatar_contradiction_clause, [status(thm)], [p1424])).
% 78.39/10.59 cnf(p148, plain, (greater(sk0(sk2),equilibrium(sk2)) | ~spl23 | ~spl26), inference(superposition, [status(thm)], [p138, p120])).
% 78.39/10.59 cnf(p201, plain, (greater(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl2 | ~spl23 | ~spl26), inference(resolution, [status(thm)], [p148, p37])).
% 78.39/10.59 cnf(p700, plain, (greater_or_equal(sk3(sk0(sk2)),equilibrium(sk2)) | ~spl2 | ~spl23 | ~spl26), inference(resolution, [status(thm)], [p201, c3])).
% 78.39/10.59 cnf(p1425, plain, ($false | ~spl2 | ~spl10 | ~spl23 | ~spl26), inference(resolution, [status(thm)], [p700, p57])).
% 78.39/10.59 cnf(sct75, plain, (~spl2 | ~spl10 | ~spl23 | ~spl26), inference(avatar_contradiction_clause, [status(thm)], [p1425])).
% 78.39/10.59 cnf(p208, plain, (greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl28), inference(resolution, [status(thm)], [p158, c4])).
% 78.39/10.59 cnf(p1427, plain, ($false | ~spl28 | ~spl83), inference(resolution, [status(thm)], [p1093, p208])).
% 78.39/10.59 cnf(sct76, plain, (~spl28 | ~spl83), inference(avatar_contradiction_clause, [status(thm)], [p1427])).
% 78.39/10.59 cnf(p1429, plain, ($false | ~spl5 | ~spl11 | ~spl58 | ~spl59), inference(resolution, [status(thm)], [p62, p887])).
% 78.39/10.59 cnf(sct77, plain, (~spl5 | ~spl11 | ~spl58 | ~spl59), inference(avatar_contradiction_clause, [status(thm)], [p1429])).
% 78.39/10.59 cnf(p1430, plain, ($false | ~spl5 | ~spl11 | ~spl60 | ~spl63), inference(resolution, [status(thm)], [p62, p942])).
% 78.39/10.59 cnf(sct78, plain, (~spl5 | ~spl11 | ~spl60 | ~spl63), inference(avatar_contradiction_clause, [status(thm)], [p1430])).
% 78.39/10.59 cnf(p1431, plain, ($false | ~spl5 | ~spl11 | ~spl62 | ~spl63), inference(resolution, [status(thm)], [p62, p944])).
% 78.39/10.59 cnf(sct79, plain, (~spl5 | ~spl11 | ~spl62 | ~spl63), inference(avatar_contradiction_clause, [status(thm)], [p1431])).
% 78.39/10.59 cnf(p1432, plain, ($false | ~spl5 | ~spl11 | ~spl37 | ~spl38), inference(resolution, [status(thm)], [p62, p691])).
% 78.39/10.59 cnf(sct80, plain, (~spl5 | ~spl11 | ~spl37 | ~spl38), inference(avatar_contradiction_clause, [status(thm)], [p1432])).
% 78.39/10.59 cnf(p1433, plain, ($false | ~spl5 | ~spl11 | ~spl38 | ~spl40), inference(resolution, [status(thm)], [p62, p999])).
% 78.39/10.59 cnf(sct81, plain, (~spl5 | ~spl11 | ~spl38 | ~spl40), inference(avatar_contradiction_clause, [status(thm)], [p1433])).
% 78.39/10.59 cnf(p1434, plain, ($false | ~spl5 | ~spl11 | ~spl59 | ~spl61), inference(resolution, [status(thm)], [p62, p1130])).
% 78.39/10.59 cnf(sct82, plain, (~spl5 | ~spl11 | ~spl59 | ~spl61), inference(avatar_contradiction_clause, [status(thm)], [p1434])).
% 78.39/10.59 cnf(p1435, plain, ($false | ~spl5 | ~spl11 | ~spl77 | ~spl78), inference(resolution, [status(thm)], [p62, p1143])).
% 78.39/10.59 cnf(sct83, plain, (~spl5 | ~spl11 | ~spl77 | ~spl78), inference(avatar_contradiction_clause, [status(thm)], [p1435])).
% 78.39/10.59 cnf(p1436, plain, ($false | ~spl5 | ~spl11 | ~spl79 | ~spl82), inference(resolution, [status(thm)], [p62, p1161])).
% 78.39/10.59 cnf(sct84, plain, (~spl5 | ~spl11 | ~spl79 | ~spl82), inference(avatar_contradiction_clause, [status(thm)], [p1436])).
% 78.39/10.59 cnf(p1437, plain, ($false | ~spl5 | ~spl11 | ~spl81 | ~spl82), inference(resolution, [status(thm)], [p62, p1162])).
% 78.39/10.59 cnf(sct85, plain, (~spl5 | ~spl11 | ~spl81 | ~spl82), inference(avatar_contradiction_clause, [status(thm)], [p1437])).
% 78.39/10.59 cnf(p219, plain, (outcompetes(efficient_producers,first_movers,equilibrium(sk2)) | ~spl9 | ~spl28), inference(superposition, [status(thm)], [p158, p51])).
% 78.39/10.59 cnf(p740, plain, (~outcompetes(efficient_producers,first_movers,equilibrium(sk2)) | ~spl1 | ~spl51), inference(superposition, [status(thm)], [p537, p31])).
% 78.39/10.59 cnf(p1540, plain, ($false | ~spl1 | ~spl9 | ~spl28 | ~spl51), inference(resolution, [status(thm)], [p219, p740])).
% 78.39/10.59 cnf(sct86, plain, (~spl1 | ~spl9 | ~spl28 | ~spl51), inference(avatar_contradiction_clause, [status(thm)], [p1540])).
% 78.39/10.59 cnf(p1570, plain, ($false | ~spl1 | ~spl51 | ~spl75), inference(resolution, [status(thm)], [p740, p1078])).
% 78.39/10.59 cnf(sct87, plain, (~spl1 | ~spl51 | ~spl75), inference(avatar_contradiction_clause, [status(thm)], [p1570])).
% 78.39/10.59 cnf(p854, plain, (greater_or_equal(sk1(sk2),sk0(sk2)) | ~spl1 | ~spl66), inference(superposition, [status(thm)], [p708, p30])).
% 78.39/10.59 cnf(p1571, plain, ($false | ~spl1 | ~spl66 | ~spl95), inference(resolution, [status(thm)], [p854, p1308])).
% 78.39/10.59 cnf(sct88, plain, (~spl1 | ~spl66 | ~spl95), inference(avatar_contradiction_clause, [status(thm)], [p1571])).
% 78.39/10.59 fof(sdef48, definition, (spl48 <=> (greater(sk3(equilibrium(sk2)),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 78.39/10.59 cnf(p533, plain, (greater(sk3(equilibrium(sk2)),sk0(sk2)) | ~spl48), inference(avatar_component_clause, [status(thm)], [sdef48])).
% 78.39/10.59 cnf(p917, plain, (greater(sk1(sk2),sk0(sk2)) | ~spl48 | ~spl70), inference(superposition, [status(thm)], [p720, p533])).
% 78.39/10.59 cnf(p928, plain, (greater_or_equal(sk1(sk2),sk0(sk2)) | ~spl48 | ~spl70), inference(resolution, [status(thm)], [p917, c3])).
% 78.39/10.59 cnf(p1572, plain, ($false | ~spl48 | ~spl70 | ~spl95), inference(resolution, [status(thm)], [p928, p1308])).
% 78.39/10.59 cnf(sct89, plain, (~spl48 | ~spl70 | ~spl95), inference(avatar_contradiction_clause, [status(thm)], [p1572])).
% 78.39/10.59 fof(sdef22, definition, (spl22 <=> (sk1(sk2) = sk0(sk2))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 78.39/10.59 cnf(p119, plain, (sk1(sk2) = sk0(sk2) | ~spl22), inference(avatar_component_clause, [status(thm)], [sdef22])).
% 78.39/10.59 cnf(p1492, plain, (~greater_or_equal(sk0(sk2),sk0(sk2)) | ~spl22 | ~spl95), inference(superposition, [status(thm)], [p119, p1308])).
% 78.39/10.59 cnf(p1579, plain, ($false | ~spl22 | ~spl95), inference(resolution, [status(thm)], [p1492, p25])).
% 78.39/10.59 cnf(sct90, plain, (~spl22 | ~spl95), inference(avatar_contradiction_clause, [status(thm)], [p1579])).
% 78.39/10.59 cnf(p1149, plain, (~greater(growth_rate(first_movers,equilibrium(sk2)),X0) | greater(zero,X0) | ~spl80), inference(resolution, [status(thm)], [p1085, c0])).
% 78.39/10.59 cnf(p1580, plain, (greater(zero,zero) | ~spl78 | ~spl80), inference(resolution, [status(thm)], [p1149, p1082])).
% 78.39/10.59 cnf(p1581, plain, ($false | ~spl5 | ~spl11 | ~spl78 | ~spl80), inference(resolution, [status(thm)], [p1580, p62])).
% 78.39/10.59 cnf(sct91, plain, (~spl5 | ~spl11 | ~spl78 | ~spl80), inference(avatar_contradiction_clause, [status(thm)], [p1581])).
% 78.39/10.59 cnf(p855, plain, (~outcompetes(efficient_producers,first_movers,sk1(sk2)) | ~spl1 | ~spl66), inference(superposition, [status(thm)], [p708, p31])).
% 78.39/10.59 cnf(p1582, plain, ($false | ~spl1 | ~spl56 | ~spl66 | ~spl70), inference(resolution, [status(thm)], [p855, p919])).
% 78.39/10.59 cnf(sct92, plain, (~spl1 | ~spl56 | ~spl66 | ~spl70), inference(avatar_contradiction_clause, [status(thm)], [p1582])).
% 78.39/10.59 fof(sdef87, definition, (spl87 <=> (outcompetes(efficient_producers,first_movers,sk1(sk2)))), introduced(definition, [new_symbols(naming, [spl87])], [avatar_definition])).
% 78.39/10.59 cnf(p1293, plain, (outcompetes(efficient_producers,first_movers,sk1(sk2)) | ~spl87), inference(avatar_component_clause, [status(thm)], [sdef87])).
% 78.39/10.59 cnf(p1583, plain, ($false | ~spl1 | ~spl66 | ~spl87), inference(resolution, [status(thm)], [p855, p1293])).
% 78.39/10.59 cnf(sct93, plain, (~spl1 | ~spl66 | ~spl87), inference(avatar_contradiction_clause, [status(thm)], [p1583])).
% 78.39/10.59 cnf(p1506, plain, (sk0(sk2) = equilibrium(sk2) | ~spl28 | ~spl49), inference(superposition, [status(thm)], [p158, p534])).
% 78.39/10.59 cnf(p1596, plain, (~outcompetes(efficient_producers,first_movers,equilibrium(sk2)) | ~spl1 | ~spl28 | ~spl49), inference(superposition, [status(thm)], [p1506, p31])).
% 78.39/10.59 cnf(p1633, plain, ($false | ~spl1 | ~spl28 | ~spl49 | ~spl75), inference(resolution, [status(thm)], [p1596, p1078])).
% 78.39/10.59 cnf(sct94, plain, (~spl1 | ~spl28 | ~spl49 | ~spl75), inference(avatar_contradiction_clause, [status(thm)], [p1633])).
% 78.39/10.59 cnf(p212, plain, (~outcompetes(efficient_producers,first_movers,sk3(equilibrium(sk2))) | ~spl1 | ~spl28), inference(superposition, [status(thm)], [p158, p31])).
% 78.39/10.59 cnf(p1645, plain, ($false | ~spl1 | ~spl28 | ~spl56), inference(resolution, [status(thm)], [p212, p568])).
% 78.39/10.59 cnf(sct95, plain, (~spl1 | ~spl28 | ~spl56), inference(avatar_contradiction_clause, [status(thm)], [p1645])).
% 78.39/10.59 cnf(p1646, plain, (~outcompetes(efficient_producers,first_movers,sk1(sk2)) | ~spl1 | ~spl28 | ~spl70), inference(superposition, [status(thm)], [p720, p212])).
% 78.39/10.59 cnf(p1648, plain, ($false | ~spl1 | ~spl28 | ~spl70 | ~spl87), inference(resolution, [status(thm)], [p1646, p1293])).
% 78.39/10.59 cnf(sct96, plain, (~spl1 | ~spl28 | ~spl70 | ~spl87), inference(avatar_contradiction_clause, [status(thm)], [p1648])).
% 78.39/10.59 fof(sdef7, definition, (spl7 <=> (~greater_or_equal(growth_rate(efficient_producers,sk0(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 78.39/10.59 cnf(p49, plain, (~greater_or_equal(growth_rate(efficient_producers,sk0(sk2)),zero) | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 78.39/10.59 cnf(p220, plain, (~greater_or_equal(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~spl7 | ~spl28), inference(superposition, [status(thm)], [p158, p49])).
% 78.39/10.59 cnf(p1653, plain, (~greater_or_equal(zero,zero) | ~spl7 | ~spl28 | ~spl82), inference(superposition, [status(thm)], [p1090, p220])).
% 78.39/10.59 cnf(p1654, plain, ($false | ~spl7 | ~spl28 | ~spl82), inference(resolution, [status(thm)], [p1653, p25])).
% 78.39/10.59 cnf(sct97, plain, (~spl7 | ~spl28 | ~spl82), inference(avatar_contradiction_clause, [status(thm)], [p1654])).
% 78.39/10.59 fof(sdef8, definition, (spl8 <=> (~greater(zero,growth_rate(first_movers,sk0(sk2))))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 78.39/10.59 cnf(p50, plain, (~greater(zero,growth_rate(first_movers,sk0(sk2))) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 78.39/10.59 cnf(p221, plain, (~greater(zero,growth_rate(first_movers,equilibrium(sk2))) | ~spl8 | ~spl28), inference(superposition, [status(thm)], [p158, p50])).
% 78.39/10.59 cnf(p1655, plain, ($false | ~spl8 | ~spl28 | ~spl80), inference(resolution, [status(thm)], [p221, p1085])).
% 78.39/10.59 cnf(sct98, plain, (~spl8 | ~spl28 | ~spl80), inference(avatar_contradiction_clause, [status(thm)], [p1655])).
% 78.39/10.59 cnf(p1664, plain, ($false | ~spl55 | ~spl61), inference(resolution, [status(thm)], [p567, p575])).
% 78.39/10.59 cnf(sct99, plain, (~spl55 | ~spl61), inference(avatar_contradiction_clause, [status(thm)], [p1664])).
% 78.39/10.59 cnf(p943, plain, (growth_rate(efficient_producers,sk1(sk2)) = zero | ~spl63 | ~spl70), inference(superposition, [status(thm)], [p720, p580])).
% 78.39/10.59 fof(sdef85, definition, (spl85 <=> (~greater_or_equal(growth_rate(efficient_producers,sk1(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl85])], [avatar_definition])).
% 78.39/10.59 cnf(p1291, plain, (~greater_or_equal(growth_rate(efficient_producers,sk1(sk2)),zero) | ~spl85), inference(avatar_component_clause, [status(thm)], [sdef85])).
% 78.39/10.59 cnf(p1675, plain, (~greater_or_equal(zero,zero) | ~spl63 | ~spl70 | ~spl85), inference(superposition, [status(thm)], [p943, p1291])).
% 78.39/10.59 cnf(p1676, plain, ($false | ~spl63 | ~spl70 | ~spl85), inference(resolution, [status(thm)], [p1675, p25])).
% 78.39/10.59 cnf(sct100, plain, (~spl63 | ~spl70 | ~spl85), inference(avatar_contradiction_clause, [status(thm)], [p1676])).
% 78.39/10.59 fof(sdef86, definition, (spl86 <=> (~greater(zero,growth_rate(first_movers,sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl86])], [avatar_definition])).
% 78.39/10.59 cnf(p1292, plain, (~greater(zero,growth_rate(first_movers,sk1(sk2))) | ~spl86), inference(avatar_component_clause, [status(thm)], [sdef86])).
% 78.39/10.59 cnf(p926, plain, (greater(zero,growth_rate(first_movers,sk1(sk2))) | ~spl61 | ~spl70), inference(superposition, [status(thm)], [p720, p575])).
% 78.39/10.59 cnf(p1678, plain, ($false | ~spl61 | ~spl70 | ~spl86), inference(resolution, [status(thm)], [p1292, p926])).
% 78.39/10.59 cnf(sct101, plain, (~spl61 | ~spl70 | ~spl86), inference(avatar_contradiction_clause, [status(thm)], [p1678])).
% 78.39/10.59 fof(sdef89, definition, (spl89 <=> (growth_rate(first_movers,sk1(sk2)) = zero)), introduced(definition, [new_symbols(naming, [spl89])], [avatar_definition])).
% 78.39/10.59 cnf(p1296, plain, (growth_rate(first_movers,sk1(sk2)) = zero | ~spl89), inference(avatar_component_clause, [status(thm)], [sdef89])).
% 78.39/10.59 fof(sdef90, definition, (spl90 <=> (greater(growth_rate(first_movers,sk1(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl90])], [avatar_definition])).
% 78.39/10.59 cnf(p1297, plain, (greater(growth_rate(first_movers,sk1(sk2)),zero) | ~spl90), inference(avatar_component_clause, [status(thm)], [sdef90])).
% 78.39/10.59 cnf(p1747, plain, (greater(zero,zero) | ~spl89 | ~spl90), inference(superposition, [status(thm)], [p1296, p1297])).
% 78.39/10.59 cnf(p1749, plain, ($false | ~spl5 | ~spl11 | ~spl89 | ~spl90), inference(resolution, [status(thm)], [p1747, p62])).
% 78.39/10.59 cnf(sct102, plain, (~spl5 | ~spl11 | ~spl89 | ~spl90), inference(avatar_contradiction_clause, [status(thm)], [p1749])).
% 78.39/10.59 fof(sdef92, definition, (spl92 <=> (greater(zero,growth_rate(first_movers,sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl92])], [avatar_definition])).
% 78.39/10.59 cnf(p1300, plain, (greater(zero,growth_rate(first_movers,sk1(sk2))) | ~spl92), inference(avatar_component_clause, [status(thm)], [sdef92])).
% 78.39/10.59 cnf(p1763, plain, ($false | ~spl86 | ~spl92), inference(resolution, [status(thm)], [p1300, p1292])).
% 78.39/10.59 cnf(sct103, plain, (~spl86 | ~spl92), inference(avatar_contradiction_clause, [status(thm)], [p1763])).
% 78.39/10.59 fof(sdef94, definition, (spl94 <=> (growth_rate(efficient_producers,sk1(sk2)) = zero)), introduced(definition, [new_symbols(naming, [spl94])], [avatar_definition])).
% 78.39/10.59 cnf(p1305, plain, (growth_rate(efficient_producers,sk1(sk2)) = zero | ~spl94), inference(avatar_component_clause, [status(thm)], [sdef94])).
% 78.39/10.59 cnf(p1780, plain, (~greater_or_equal(zero,zero) | ~spl85 | ~spl94), inference(superposition, [status(thm)], [p1305, p1291])).
% 78.39/10.59 cnf(p1784, plain, ($false | ~spl85 | ~spl94), inference(resolution, [status(thm)], [p1780, p25])).
% 78.39/10.59 cnf(sct104, plain, (~spl85 | ~spl94), inference(avatar_contradiction_clause, [status(thm)], [p1784])).
% 78.39/10.59 fof(sdef91, definition, (spl91 <=> (greater(growth_rate(efficient_producers,sk1(sk2)),zero))), introduced(definition, [new_symbols(naming, [spl91])], [avatar_definition])).
% 78.39/10.59 cnf(p1298, plain, (greater(growth_rate(efficient_producers,sk1(sk2)),zero) | ~spl91), inference(avatar_component_clause, [status(thm)], [sdef91])).
% 78.39/10.59 cnf(p1782, plain, (greater(zero,zero) | ~spl91 | ~spl94), inference(superposition, [status(thm)], [p1305, p1298])).
% 78.39/10.59 cnf(p1785, plain, ($false | ~spl5 | ~spl11 | ~spl91 | ~spl94), inference(resolution, [status(thm)], [p1782, p62])).
% 78.39/10.59 cnf(sct105, plain, (~spl5 | ~spl11 | ~spl91 | ~spl94), inference(avatar_contradiction_clause, [status(thm)], [p1785])).
% 78.39/10.59 fof(sdef93, definition, (spl93 <=> (greater(zero,growth_rate(efficient_producers,sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl93])], [avatar_definition])).
% 78.39/10.59 cnf(p1302, plain, (greater(zero,growth_rate(efficient_producers,sk1(sk2))) | ~spl93), inference(avatar_component_clause, [status(thm)], [sdef93])).
% 78.39/10.59 cnf(p1783, plain, (greater(zero,zero) | ~spl93 | ~spl94), inference(superposition, [status(thm)], [p1305, p1302])).
% 78.39/10.59 cnf(p1786, plain, ($false | ~spl5 | ~spl11 | ~spl93 | ~spl94), inference(resolution, [status(thm)], [p1783, p62])).
% 78.39/10.59 cnf(sct106, plain, (~spl5 | ~spl11 | ~spl93 | ~spl94), inference(avatar_contradiction_clause, [status(thm)], [p1786])).
% 78.39/10.59 cnf(p140, plain, (~greater(equilibrium(sk2),X0) | greater(sk1(sk2),X0) | ~spl25), inference(resolution, [status(thm)], [p137, c0])).
% 78.39/10.59 cnf(p448, plain, (greater(sk1(sk2),sk0(sk2)) | ~spl25 | ~spl27), inference(resolution, [status(thm)], [p140, p157])).
% 78.39/10.59 cnf(p957, plain, (greater(sk3(sk1(sk2)),sk0(sk2)) | ~spl25 | ~spl27 | ~spl31), inference(resolution, [status(thm)], [p602, p448])).
% 78.39/10.59 cnf(p1017, plain, (greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | ~spl25 | ~spl27 | ~spl31), inference(resolution, [status(thm)], [p957, c3])).
% 78.39/10.59 cnf(p1801, plain, ($false | ~spl25 | ~spl27 | ~spl31 | ~spl43), inference(resolution, [status(thm)], [p1017, p349])).
% 78.39/10.59 cnf(sct107, plain, (~spl25 | ~spl27 | ~spl31 | ~spl43), inference(avatar_contradiction_clause, [status(thm)], [p1801])).
% 78.39/10.59 cnf(p1317, plain, (greater(zero,growth_rate(efficient_producers,sk3(equilibrium(sk2)))) | ~spl26 | ~spl41), inference(superposition, [status(thm)], [p138, p343])).
% 78.39/10.59 cnf(p1832, plain, (greater(zero,zero) | ~spl26 | ~spl41 | ~spl63), inference(superposition, [status(thm)], [p580, p1317])).
% 78.39/10.59 cnf(p1833, plain, ($false | ~spl5 | ~spl11 | ~spl26 | ~spl41 | ~spl63), inference(resolution, [status(thm)], [p1832, p62])).
% 78.39/10.59 cnf(sct108, plain, (~spl5 | ~spl11 | ~spl26 | ~spl41 | ~spl63), inference(avatar_contradiction_clause, [status(thm)], [p1833])).
% 78.39/10.59 cnf(p1449, plain, (~greater_or_equal(sk3(sk0(sk2)),sk0(sk2)) | ~spl22 | ~spl43), inference(superposition, [status(thm)], [p119, p349])).
% 78.39/10.59 cnf(p1839, plain, ($false | ~spl1 | ~spl22 | ~spl43), inference(resolution, [status(thm)], [p1449, p30])).
% 78.39/10.59 cnf(sct109, plain, (~spl1 | ~spl22 | ~spl43), inference(avatar_contradiction_clause, [status(thm)], [p1839])).
% 78.39/10.59 cnf(p1536, plain, (~greater_or_equal(sk1(sk2),equilibrium(sk2)) | ~spl28 | ~spl95), inference(superposition, [status(thm)], [p158, p1308])).
% 78.39/10.59 cnf(p1840, plain, ($false | ~spl24 | ~spl28 | ~spl95), inference(resolution, [status(thm)], [p1536, p126])).
% 78.39/10.59 cnf(sct110, plain, (~spl24 | ~spl28 | ~spl95), inference(avatar_contradiction_clause, [status(thm)], [p1840])).
% 78.39/10.59 fof(sdef52, definition, (spl52 <=> (greater(sk3(equilibrium(sk2)),equilibrium(sk2)))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 78.39/10.59 cnf(p558, plain, (greater(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl52), inference(avatar_component_clause, [status(thm)], [sdef52])).
% 78.39/10.59 cnf(p788, plain, (greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl52), inference(resolution, [status(thm)], [p558, c3])).
% 78.39/10.59 cnf(p1841, plain, ($false | ~spl52 | ~spl57), inference(resolution, [status(thm)], [p570, p788])).
% 78.39/10.59 cnf(sct111, plain, (~spl52 | ~spl57), inference(avatar_contradiction_clause, [status(thm)], [p1841])).
% 78.39/10.59 cnf(p1846, plain, (greater(zero,zero) | ~spl13 | ~spl16), inference(superposition, [status(thm)], [p92, p60])).
% 78.39/10.59 cnf(p1847, plain, ($false | ~spl5 | ~spl11 | ~spl13 | ~spl16), inference(resolution, [status(thm)], [p1846, p62])).
% 78.39/10.59 cnf(sct112, plain, (~spl5 | ~spl11 | ~spl13 | ~spl16), inference(avatar_contradiction_clause, [status(thm)], [p1847])).
% 78.39/10.59 cnf(p1850, plain, (greater(zero,zero) | ~spl11 | ~spl16 | ~spl19), inference(superposition, [status(thm)], [p92, p105])).
% 78.39/10.59 cnf(p1852, plain, ($false | ~spl5 | ~spl11 | ~spl16 | ~spl19), inference(resolution, [status(thm)], [p1850, p62])).
% 78.39/10.59 cnf(sct113, plain, (~spl5 | ~spl11 | ~spl16 | ~spl19), inference(avatar_contradiction_clause, [status(thm)], [p1852])).
% 78.39/10.59 cnf(p1899, plain, (~outcompetes(efficient_producers,first_movers,equilibrium(sk2)) | ~spl20 | ~spl26 | ~spl53), inference(superposition, [status(thm)], [p559, p153])).
% 78.39/10.59 cnf(p1900, plain, ($false | ~spl20 | ~spl26 | ~spl53 | ~spl75), inference(resolution, [status(thm)], [p1899, p1078])).
% 78.39/10.59 cnf(sct114, plain, (~spl20 | ~spl26 | ~spl53 | ~spl75), inference(avatar_contradiction_clause, [status(thm)], [p1900])).
% 78.39/10.59 cnf(p1930, plain, (~outcompetes(efficient_producers,first_movers,equilibrium(sk2)) | ~spl1 | ~spl28 | ~spl53), inference(superposition, [status(thm)], [p559, p212])).
% 78.39/10.59 cnf(p1943, plain, ($false | ~spl1 | ~spl28 | ~spl53 | ~spl75), inference(resolution, [status(thm)], [p1930, p1078])).
% 78.39/10.59 cnf(sct115, plain, (~spl1 | ~spl28 | ~spl53 | ~spl75), inference(avatar_contradiction_clause, [status(thm)], [p1943])).
% 78.39/10.59 fof(sdef15, definition, (spl15 <=> (greater(zero,growth_rate(efficient_producers,sk3(sk0(sk2)))))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 78.39/10.59 cnf(p82, plain, (greater(zero,growth_rate(efficient_producers,sk3(sk0(sk2)))) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 78.39/10.59 cnf(p83, plain, (~greater(growth_rate(efficient_producers,sk3(sk0(sk2))),X0) | greater(zero,X0) | ~spl15), inference(resolution, [status(thm)], [p82, c0])).
% 78.39/10.59 cnf(p106, plain, (greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | ~spl15 | ~spl19), inference(resolution, [status(thm)], [p101, p83])).
% 78.39/10.59 cnf(p1950, plain, ($false | ~spl5 | ~spl15 | ~spl19), inference(resolution, [status(thm)], [p46, p106])).
% 78.39/10.59 cnf(sct116, plain, (~spl5 | ~spl15 | ~spl19), inference(avatar_contradiction_clause, [status(thm)], [p1950])).
% 78.39/10.59 cnf(p1952, plain, (~greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl3 | ~spl10), inference(superposition, [status(thm)], [p36, p57])).
% 78.39/10.59 cnf(p271, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl29), inference(resolution, [status(thm)], [p159, c3])).
% 78.39/10.59 cnf(p1971, plain, ($false | ~spl3 | ~spl10 | ~spl29), inference(resolution, [status(thm)], [p1952, p271])).
% 78.39/10.59 cnf(sct117, plain, (~spl3 | ~spl10 | ~spl29), inference(avatar_contradiction_clause, [status(thm)], [p1971])).
% 78.39/10.60 cnf(p524, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl23 | ~spl25), inference(resolution, [status(thm)], [p417, c3])).
% 78.39/10.60 cnf(p1972, plain, ($false | ~spl3 | ~spl10 | ~spl23 | ~spl25), inference(resolution, [status(thm)], [p1952, p524])).
% 78.39/10.60 cnf(sct118, plain, (~spl3 | ~spl10 | ~spl23 | ~spl25), inference(avatar_contradiction_clause, [status(thm)], [p1972])).
% 78.39/10.60 cnf(p132, plain, (greater_or_equal(sk0(sk2),sk1(sk2)) | ~spl23), inference(resolution, [status(thm)], [p120, c3])).
% 78.39/10.60 cnf(p150, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl23 | ~spl26), inference(superposition, [status(thm)], [p138, p132])).
% 78.39/10.60 cnf(p1973, plain, ($false | ~spl3 | ~spl10 | ~spl23 | ~spl26), inference(resolution, [status(thm)], [p1952, p150])).
% 78.39/10.60 cnf(sct119, plain, (~spl3 | ~spl10 | ~spl23 | ~spl26), inference(avatar_contradiction_clause, [status(thm)], [p1973])).
% 78.39/10.60 fof(f5, 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/sandbox/benchmark/theBenchmark.p', l1)).
% 78.39/10.60 fof(f5_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)], [f5])).
% 78.39/10.60 fof(f5_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])], [f5_nnf])).
% 78.39/10.60 cnf(c16, plain, ~environment(X0) | ~stable(X0) | in_environment(X0,sk0(X0)), inference(cnf_transformation, [status(esa)], [f5_sk])).
% 78.39/10.60 cnf(c20, plain, environment(sk2), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 78.39/10.60 cnf(p26, plain, ~stable(sk2) | in_environment(sk2,sk0(sk2)), inference(resolution, [status(thm)], [c16, c20])).
% 78.39/10.60 cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [p26, sdef0, sdef1])).
% 78.39/10.60 cnf(c2, plain, ~greater_or_equal(X0,X1) | greater(X0,X1) | X0 = X1, inference(cnf_transformation, [status(esa)], [f2_sk])).
% 78.39/10.60 cnf(p34, plain, (greater(sk3(sk0(sk2)),sk0(sk2)) | sk3(sk0(sk2)) = sk0(sk2) | ~spl1), inference(resolution, [status(thm)], [c2, p30])).
% 78.39/10.60 cnf(ssp1, plain, (~spl1 | spl2 | spl3), inference(avatar_split_clause, [status(thm)], [p34, sdef2, sdef3])).
% 78.39/10.60 fof(f3, hypothesis, ! [E,S1,S2,T] : ( ( environment(E) & subpopulations(S1,S2,E,T) ) => ( ( greater_or_equal(growth_rate(S2,T),zero) & greater(zero,growth_rate(S1,T)) ) <=> outcompetes(S2,S1,T) ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d2)).
% 78.39/10.60 fof(f3_nnf, plain, ! [E,S1,S2,T] : (((~(environment(E)) | ~(subpopulations(S1,S2,E,T))) | (((~(greater_or_equal(growth_rate(S2,T),zero)) | ~(greater(zero,growth_rate(S1,T)))) | outcompetes(S2,S1,T)) & ((greater_or_equal(growth_rate(S2,T),zero) & greater(zero,growth_rate(S1,T))) | ~(outcompetes(S2,S1,T)))))), inference(nnf_transformation, [status(thm)], [f3])).
% 78.39/10.60 fof(f3_sk, plain, ! [E,S1,S2,T] : (((~(environment(E)) | ~(subpopulations(S1,S2,E,T))) | (((~(greater_or_equal(growth_rate(S2,T),zero)) | ~(greater(zero,growth_rate(S1,T)))) | outcompetes(S2,S1,T)) & ((greater_or_equal(growth_rate(S2,T),zero) & greater(zero,growth_rate(S1,T))) | ~(outcompetes(S2,S1,T)))))), inference(skolemisation, [status(esa)], [f3_nnf])).
% 78.39/10.60 cnf(c5, plain, ~environment(X0) | ~subpopulations(X1,X2,X0,X3) | ~greater_or_equal(growth_rate(X2,X3),zero) | ~greater(zero,growth_rate(X1,X3)) | outcompetes(X2,X1,X3), inference(cnf_transformation, [status(esa)], [f3_sk])).
% 78.39/10.60 cnf(p41, plain, ~subpopulations(X0,X1,sk2,X2) | ~greater_or_equal(growth_rate(X1,X2),zero) | ~greater(zero,growth_rate(X0,X2)) | outcompetes(X1,X0,X2), inference(resolution, [status(thm)], [c5, c20])).
% 78.39/10.60 cnf(c22, plain, ~in_environment(sk2,X1) | subpopulations(first_movers,efficient_producers,sk2,sk3(X1)), inference(cnf_transformation, [status(esa)], [f7_sk])).
% 78.39/10.60 cnf(p32, plain, (subpopulations(first_movers,efficient_producers,sk2,sk3(sk0(sk2))) | ~spl1), inference(resolution, [status(thm)], [p28, c22])).
% 78.39/10.60 cnf(p44, plain, (~greater_or_equal(growth_rate(efficient_producers,sk3(sk0(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(sk0(sk2)))) | outcompetes(efficient_producers,first_movers,sk3(sk0(sk2))) | ~spl1), inference(resolution, [status(thm)], [p41, p32])).
% 78.39/10.60 cnf(ssp2, plain, (~spl1 | spl4 | spl5 | spl6), inference(avatar_split_clause, [status(thm)], [p44, sdef4, sdef5, sdef6])).
% 78.39/10.60 cnf(p42, plain, (subpopulations(first_movers,efficient_producers,sk2,sk0(sk2)) | ~spl1 | ~spl3), inference(superposition, [status(thm)], [p36, p32])).
% 78.39/10.60 cnf(p48, plain, (~greater_or_equal(growth_rate(efficient_producers,sk0(sk2)),zero) | ~greater(zero,growth_rate(first_movers,sk0(sk2))) | outcompetes(efficient_producers,first_movers,sk0(sk2)) | ~spl1 | ~spl3), inference(resolution, [status(thm)], [p41, p42])).
% 78.39/10.60 cnf(ssp3, plain, (~spl1 | ~spl3 | spl7 | spl8 | spl9), inference(avatar_split_clause, [status(thm)], [p48, sdef7, sdef8, sdef9])).
% 78.39/10.60 fof(f4, 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/sandbox/benchmark/theBenchmark.p', l6)).
% 78.39/10.60 fof(f4_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)], [f4])).
% 78.39/10.60 fof(f4_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)], [f4_nnf])).
% 78.39/10.60 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(growth_rate(first_movers,X1),zero) | greater(growth_rate(efficient_producers,X1),zero), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 78.39/10.60 cnf(p55, 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)], [c8, c20])).
% 78.39/10.60 cnf(p56, 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)], [p55, p32])).
% 78.39/10.60 cnf(ssp4, plain, (~spl1 | spl10 | spl11 | spl12 | spl13), inference(avatar_split_clause, [status(thm)], [p56, sdef10, sdef11, sdef12, sdef13])).
% 78.39/10.60 cnf(c9, 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)], [f4_sk])).
% 78.39/10.60 cnf(p61, 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)], [c9, c20])).
% 78.39/10.60 cnf(p72, 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)], [p61, p32])).
% 78.39/10.60 cnf(ssp5, plain, (~spl1 | spl10 | spl11 | spl12 | spl14), inference(avatar_split_clause, [status(thm)], [p72, sdef10, sdef11, sdef12, sdef14])).
% 78.39/10.60 cnf(c10, 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)], [f4_sk])).
% 78.39/10.60 cnf(p66, 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)], [c10, c20])).
% 78.39/10.60 cnf(p81, 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)], [p66, p32])).
% 78.39/10.60 cnf(ssp6, plain, (~spl1 | spl10 | spl11 | spl13 | spl15), inference(avatar_split_clause, [status(thm)], [p81, sdef10, sdef11, sdef13, sdef15])).
% 78.39/10.60 cnf(c11, 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)], [f4_sk])).
% 78.39/10.60 cnf(p71, 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)], [c11, c20])).
% 78.39/10.60 cnf(p89, 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)], [p71, p32])).
% 78.39/10.60 cnf(ssp7, plain, (~spl1 | spl10 | spl11 | spl14 | spl15), inference(avatar_split_clause, [status(thm)], [p89, sdef10, sdef11, sdef14, sdef15])).
% 78.39/10.60 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(growth_rate(first_movers,X1),zero) | greater(growth_rate(efficient_producers,X1),zero), inference(cnf_transformation, [status(esa)], [f4_sk])).
% 78.39/10.60 cnf(p78, 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)], [c12, c20])).
% 78.39/10.60 cnf(p91, 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)], [p78, p32])).
% 78.39/10.60 cnf(ssp8, plain, (~spl1 | spl10 | spl12 | spl13 | spl16), inference(avatar_split_clause, [status(thm)], [p91, sdef10, sdef12, sdef13, sdef16])).
% 78.39/10.60 cnf(c13, 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)], [f4_sk])).
% 78.39/10.60 cnf(p80, 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)], [c13, c20])).
% 78.39/10.60 cnf(p96, 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)], [p80, p32])).
% 78.39/10.60 cnf(ssp9, plain, (~spl1 | spl10 | spl12 | spl14 | spl16), inference(avatar_split_clause, [status(thm)], [p96, sdef10, sdef12, sdef14, sdef16])).
% 78.39/10.60 cnf(c17, 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)], [f5_sk])).
% 78.39/10.60 cnf(p97, 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)], [c17, c20])).
% 78.39/10.60 fof(sdef17, definition, (spl17 <=> (~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, [spl17])], [avatar_definition])).
% 78.39/10.60 cnf(ssp10, plain, (spl0 | spl17), inference(avatar_split_clause, [status(thm)], [p97, sdef0, sdef17])).
% 78.39/10.60 cnf(p98, 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)) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 78.39/10.60 cnf(p99, 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 | ~spl17), inference(resolution, [status(thm)], [p98, p32])).
% 78.39/10.60 cnf(ssp11, plain, (~spl1 | ~spl17 | spl18 | spl19), inference(avatar_split_clause, [status(thm)], [p99, sdef18, sdef19])).
% 78.39/10.60 fof(f6, hypothesis, ! [E] : ( ( environment(E) & stable(E) ) => ? [T] : ( in_environment(E,T) & greater_or_equal(T,equilibrium(E)) ) ), file('/export/starexec/sandbox/benchmark/theBenchmark.p', a4)).
% 78.39/10.60 fof(f6_nnf, plain, ! [E] : (((~(environment(E)) | ~(stable(E))) | ? [T] : ((in_environment(E,T) & greater_or_equal(T,equilibrium(E)))))), inference(nnf_transformation, [status(thm)], [f6])).
% 78.39/10.60 fof(f6_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])], [f6_nnf])).
% 78.39/10.60 cnf(c18, plain, ~environment(X0) | ~stable(X0) | in_environment(X0,sk1(X0)), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 78.39/10.60 cnf(p111, plain, ~stable(sk2) | in_environment(sk2,sk1(sk2)), inference(resolution, [status(thm)], [c18, c20])).
% 78.39/10.60 cnf(ssp12, plain, (spl0 | spl20), inference(avatar_split_clause, [status(thm)], [p111, sdef0, sdef20])).
% 78.39/10.60 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/sandbox/benchmark/theBenchmark.p', mp_times_in_environment)).
% 78.39/10.60 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.39/10.60 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.39/10.60 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.39/10.60 cnf(p33, plain, (~in_environment(sk2,X0) | greater(X0,sk0(sk2)) | X0 = sk0(sk2) | greater(sk0(sk2),X0) | ~spl1), inference(resolution, [status(thm)], [p28, c1])).
% 78.39/10.60 cnf(p117, plain, (greater(sk1(sk2),sk0(sk2)) | sk1(sk2) = sk0(sk2) | greater(sk0(sk2),sk1(sk2)) | ~spl1 | ~spl20), inference(resolution, [status(thm)], [p112, p33])).
% 78.39/10.60 cnf(ssp13, plain, (~spl1 | ~spl20 | spl21 | spl22 | spl23), inference(avatar_split_clause, [status(thm)], [p117, sdef21, sdef22, sdef23])).
% 78.39/10.60 cnf(c19, plain, ~environment(X0) | ~stable(X0) | greater_or_equal(sk1(X0),equilibrium(X0)), inference(cnf_transformation, [status(esa)], [f6_sk])).
% 78.39/10.60 cnf(p125, plain, ~stable(sk2) | greater_or_equal(sk1(sk2),equilibrium(sk2)), inference(resolution, [status(thm)], [c19, c20])).
% 78.39/10.60 cnf(ssp14, plain, (spl0 | spl24), inference(avatar_split_clause, [status(thm)], [p125, sdef0, sdef24])).
% 78.39/10.60 cnf(c14, 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)], [f4_sk])).
% 78.39/10.60 cnf(p86, 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)], [c14, c20])).
% 78.39/10.60 cnf(p135, 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)], [p86, p32])).
% 78.39/10.60 cnf(ssp15, plain, (~spl1 | spl10 | spl13 | spl15 | spl16), inference(avatar_split_clause, [status(thm)], [p135, sdef10, sdef13, sdef15, sdef16])).
% 78.39/10.60 cnf(p136, plain, (greater(sk1(sk2),equilibrium(sk2)) | sk1(sk2) = equilibrium(sk2) | ~spl24), inference(resolution, [status(thm)], [p126, c2])).
% 78.39/10.60 cnf(ssp16, plain, (~spl24 | spl25 | spl26), inference(avatar_split_clause, [status(thm)], [p136, sdef25, sdef26])).
% 78.39/10.60 cnf(c15, 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)], [f4_sk])).
% 78.39/10.60 cnf(p90, 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)], [c15, c20])).
% 78.39/10.60 cnf(p143, 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)], [p90, p32])).
% 78.39/10.60 cnf(ssp17, plain, (~spl1 | spl10 | spl14 | spl15 | spl16), inference(avatar_split_clause, [status(thm)], [p143, sdef10, sdef14, sdef15, sdef16])).
% 78.39/10.60 cnf(p156, plain, (greater(equilibrium(sk2),sk0(sk2)) | equilibrium(sk2) = sk0(sk2) | greater(sk0(sk2),equilibrium(sk2)) | ~spl1 | ~spl20 | ~spl26), inference(resolution, [status(thm)], [p144, p33])).
% 78.39/10.60 cnf(ssp18, plain, (~spl1 | ~spl20 | ~spl26 | spl27 | spl28 | spl29), inference(avatar_split_clause, [status(thm)], [p156, sdef27, sdef28, sdef29])).
% 78.39/10.60 cnf(p139, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl22 | ~spl24), inference(superposition, [status(thm)], [p119, p126])).
% 78.39/10.60 cnf(p160, plain, (greater(sk0(sk2),equilibrium(sk2)) | sk0(sk2) = equilibrium(sk2) | ~spl22 | ~spl24), inference(resolution, [status(thm)], [p139, c2])).
% 78.39/10.60 cnf(ssp19, plain, (~spl22 | ~spl24 | spl29 | spl30), inference(avatar_split_clause, [status(thm)], [p160, sdef29, sdef30])).
% 78.39/10.60 cnf(p326, plain, (greater(sk3(sk1(sk2)),sk1(sk2)) | sk3(sk1(sk2)) = sk1(sk2) | ~spl20), inference(resolution, [status(thm)], [p113, c2])).
% 78.39/10.60 cnf(ssp20, plain, (~spl20 | spl31 | spl32), inference(avatar_split_clause, [status(thm)], [p326, sdef31, sdef32])).
% 78.39/10.60 cnf(p115, plain, (subpopulations(first_movers,efficient_producers,sk2,sk3(sk1(sk2))) | ~spl20), inference(resolution, [status(thm)], [p112, c22])).
% 78.39/10.60 cnf(p331, plain, (~greater_or_equal(growth_rate(efficient_producers,sk3(sk1(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(sk1(sk2)))) | outcompetes(efficient_producers,first_movers,sk3(sk1(sk2))) | ~spl20), inference(resolution, [status(thm)], [p115, p41])).
% 78.39/10.60 cnf(ssp21, plain, (~spl20 | spl33 | spl34 | spl35), inference(avatar_split_clause, [status(thm)], [p331, sdef33, sdef34, sdef35])).
% 78.39/10.60 cnf(p335, 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) | ~spl20), inference(resolution, [status(thm)], [p115, p55])).
% 78.39/10.60 cnf(ssp22, plain, (~spl20 | spl36 | spl37 | spl38 | spl39), inference(avatar_split_clause, [status(thm)], [p335, sdef36, sdef37, sdef38, sdef39])).
% 78.39/10.60 cnf(p340, 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)))) | ~spl20), inference(resolution, [status(thm)], [p115, p61])).
% 78.39/10.60 cnf(ssp23, plain, (~spl20 | spl36 | spl37 | spl38 | spl40), inference(avatar_split_clause, [status(thm)], [p340, sdef36, sdef37, sdef38, sdef40])).
% 78.39/10.60 cnf(p342, 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) | ~spl20), inference(resolution, [status(thm)], [p115, p66])).
% 78.39/10.60 cnf(ssp24, plain, (~spl20 | spl36 | spl37 | spl39 | spl41), inference(avatar_split_clause, [status(thm)], [p342, sdef36, sdef37, sdef39, sdef41])).
% 78.39/10.60 cnf(p344, 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)))) | ~spl20), inference(resolution, [status(thm)], [p115, p71])).
% 78.39/10.60 cnf(ssp25, plain, (~spl20 | spl36 | spl37 | spl40 | spl41), inference(avatar_split_clause, [status(thm)], [p344, sdef36, sdef37, sdef40, sdef41])).
% 78.39/10.60 cnf(p345, 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) | ~spl20), inference(resolution, [status(thm)], [p115, p78])).
% 78.39/10.60 cnf(ssp26, plain, (~spl20 | spl36 | spl38 | spl39 | spl42), inference(avatar_split_clause, [status(thm)], [p345, sdef36, sdef38, sdef39, sdef42])).
% 78.39/10.60 cnf(p347, 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)))) | ~spl20), inference(resolution, [status(thm)], [p115, p80])).
% 78.39/10.60 cnf(ssp27, plain, (~spl20 | spl36 | spl38 | spl40 | spl42), inference(avatar_split_clause, [status(thm)], [p347, sdef36, sdef38, sdef40, sdef42])).
% 78.39/10.60 cnf(p348, plain, (~greater_or_equal(sk3(sk1(sk2)),sk0(sk2)) | greater(growth_rate(efficient_producers,sk3(sk1(sk2))),growth_rate(first_movers,sk3(sk1(sk2)))) | ~spl17 | ~spl20), inference(resolution, [status(thm)], [p115, p98])).
% 78.39/10.60 cnf(ssp28, plain, (~spl17 | ~spl20 | spl43 | spl44), inference(avatar_split_clause, [status(thm)], [p348, sdef43, sdef44])).
% 78.39/10.60 cnf(p351, 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) | ~spl20), inference(resolution, [status(thm)], [p115, p86])).
% 78.39/10.60 cnf(ssp29, plain, (~spl20 | spl36 | spl39 | spl41 | spl42), inference(avatar_split_clause, [status(thm)], [p351, sdef36, sdef39, sdef41, sdef42])).
% 78.39/10.60 cnf(p352, 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)))) | ~spl20), inference(resolution, [status(thm)], [p115, p90])).
% 78.39/10.60 cnf(ssp30, plain, (~spl20 | spl36 | spl40 | spl41 | spl42), inference(avatar_split_clause, [status(thm)], [p352, sdef36, sdef40, sdef41, sdef42])).
% 78.39/10.60 cnf(p116, plain, (~in_environment(sk2,X0) | greater(X0,sk1(sk2)) | X0 = sk1(sk2) | greater(sk1(sk2),X0) | ~spl20), inference(resolution, [status(thm)], [p112, c1])).
% 78.39/10.60 cnf(p354, plain, (greater(sk0(sk2),sk1(sk2)) | sk0(sk2) = sk1(sk2) | greater(sk1(sk2),sk0(sk2)) | ~spl1 | ~spl20), inference(resolution, [status(thm)], [p116, p28])).
% 78.39/10.60 cnf(ssp31, plain, (~spl1 | ~spl20 | spl21 | spl23 | spl45), inference(avatar_split_clause, [status(thm)], [p354, sdef21, sdef23, sdef45])).
% 78.39/10.60 cnf(p209, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl1 | ~spl28), inference(superposition, [status(thm)], [p158, p28])).
% 78.39/10.60 cnf(p356, plain, (greater(equilibrium(sk2),sk1(sk2)) | equilibrium(sk2) = sk1(sk2) | greater(sk1(sk2),equilibrium(sk2)) | ~spl1 | ~spl20 | ~spl28), inference(resolution, [status(thm)], [p116, p209])).
% 78.39/10.60 cnf(ssp32, plain, (~spl1 | ~spl20 | ~spl28 | spl25 | spl46 | spl47), inference(avatar_split_clause, [status(thm)], [p356, sdef25, sdef46, sdef47])).
% 78.39/10.60 cnf(p275, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl1 | ~spl30), inference(superposition, [status(thm)], [p161, p28])).
% 78.39/10.60 cnf(p359, plain, (greater(equilibrium(sk2),sk1(sk2)) | equilibrium(sk2) = sk1(sk2) | greater(sk1(sk2),equilibrium(sk2)) | ~spl1 | ~spl20 | ~spl30), inference(resolution, [status(thm)], [p116, p275])).
% 78.39/10.60 cnf(ssp33, plain, (~spl1 | ~spl20 | ~spl30 | spl25 | spl46 | spl47), inference(avatar_split_clause, [status(thm)], [p359, sdef25, sdef46, sdef47])).
% 78.39/10.60 cnf(p396, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl20 | ~spl47), inference(superposition, [status(thm)], [p358, p112])).
% 78.39/10.60 cnf(p415, plain, (greater(equilibrium(sk2),sk0(sk2)) | equilibrium(sk2) = sk0(sk2) | greater(sk0(sk2),equilibrium(sk2)) | ~spl1 | ~spl20 | ~spl47), inference(resolution, [status(thm)], [p396, p33])).
% 78.39/10.60 cnf(ssp34, plain, (~spl1 | ~spl20 | ~spl47 | spl27 | spl28 | spl29), inference(avatar_split_clause, [status(thm)], [p415, sdef27, sdef28, sdef29])).
% 78.39/10.60 cnf(p364, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl24 | ~spl45), inference(superposition, [status(thm)], [p355, p126])).
% 78.39/10.60 cnf(p426, plain, (greater(sk0(sk2),equilibrium(sk2)) | sk0(sk2) = equilibrium(sk2) | ~spl24 | ~spl45), inference(resolution, [status(thm)], [p364, c2])).
% 78.39/10.60 cnf(ssp35, plain, (~spl24 | ~spl45 | spl29 | spl30), inference(avatar_split_clause, [status(thm)], [p426, sdef29, sdef30])).
% 78.39/10.60 cnf(p210, plain, (greater_or_equal(sk3(equilibrium(sk2)),sk0(sk2)) | ~spl1 | ~spl28), inference(superposition, [status(thm)], [p158, p30])).
% 78.39/10.60 cnf(p532, plain, (greater(sk3(equilibrium(sk2)),sk0(sk2)) | sk3(equilibrium(sk2)) = sk0(sk2) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p210, c2])).
% 78.39/10.60 cnf(ssp36, plain, (~spl1 | ~spl28 | spl48 | spl49), inference(avatar_split_clause, [status(thm)], [p532, sdef48, sdef49])).
% 78.39/10.60 cnf(p535, plain, (greater(sk3(sk0(sk2)),equilibrium(sk2)) | sk3(sk0(sk2)) = equilibrium(sk2) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p211, c2])).
% 78.39/10.60 cnf(ssp37, plain, (~spl1 | ~spl28 | spl50 | spl51), inference(avatar_split_clause, [status(thm)], [p535, sdef50, sdef51])).
% 78.39/10.60 cnf(p557, plain, (greater(sk3(equilibrium(sk2)),equilibrium(sk2)) | sk3(equilibrium(sk2)) = equilibrium(sk2) | ~spl1 | ~spl30), inference(resolution, [status(thm)], [p276, c2])).
% 78.39/10.60 cnf(ssp38, plain, (~spl1 | ~spl30 | spl52 | spl53), inference(avatar_split_clause, [status(thm)], [p557, sdef52, sdef53])).
% 78.39/10.60 cnf(p280, plain, (subpopulations(first_movers,efficient_producers,sk2,sk3(equilibrium(sk2))) | ~spl1 | ~spl30), inference(superposition, [status(thm)], [p161, p32])).
% 78.39/10.60 cnf(p565, plain, (~greater_or_equal(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | outcompetes(efficient_producers,first_movers,sk3(equilibrium(sk2))) | ~spl1 | ~spl30), inference(resolution, [status(thm)], [p280, p41])).
% 78.39/10.60 cnf(ssp39, plain, (~spl1 | ~spl30 | spl54 | spl55 | spl56), inference(avatar_split_clause, [status(thm)], [p565, sdef54, sdef55, sdef56])).
% 78.39/10.60 cnf(p569, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(equilibrium(sk2))) = zero | greater(growth_rate(first_movers,sk3(equilibrium(sk2))),zero) | greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~spl1 | ~spl30), inference(resolution, [status(thm)], [p280, p55])).
% 78.39/10.60 cnf(ssp40, plain, (~spl1 | ~spl30 | spl57 | spl58 | spl59 | spl60), inference(avatar_split_clause, [status(thm)], [p569, sdef57, sdef58, sdef59, sdef60])).
% 78.39/10.60 cnf(p574, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(equilibrium(sk2))) = zero | greater(growth_rate(first_movers,sk3(equilibrium(sk2))),zero) | greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl1 | ~spl30), inference(resolution, [status(thm)], [p280, p61])).
% 78.39/10.60 cnf(ssp41, plain, (~spl1 | ~spl30 | spl57 | spl58 | spl59 | spl61), inference(avatar_split_clause, [status(thm)], [p574, sdef57, sdef58, sdef59, sdef61])).
% 78.39/10.60 cnf(p576, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(equilibrium(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(equilibrium(sk2)))) | greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~spl1 | ~spl30), inference(resolution, [status(thm)], [p280, p66])).
% 78.39/10.60 cnf(ssp42, plain, (~spl1 | ~spl30 | spl57 | spl58 | spl60 | spl62), inference(avatar_split_clause, [status(thm)], [p576, sdef57, sdef58, sdef60, sdef62])).
% 78.39/10.60 cnf(p578, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(equilibrium(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(equilibrium(sk2)))) | greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl1 | ~spl30), inference(resolution, [status(thm)], [p280, p71])).
% 78.39/10.60 cnf(ssp43, plain, (~spl1 | ~spl30 | spl57 | spl58 | spl61 | spl62), inference(avatar_split_clause, [status(thm)], [p578, sdef57, sdef58, sdef61, sdef62])).
% 78.39/10.60 cnf(p579, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(equilibrium(sk2))) = zero | greater(growth_rate(first_movers,sk3(equilibrium(sk2))),zero) | greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~spl1 | ~spl30), inference(resolution, [status(thm)], [p280, p78])).
% 78.39/10.60 cnf(ssp44, plain, (~spl1 | ~spl30 | spl57 | spl59 | spl60 | spl63), inference(avatar_split_clause, [status(thm)], [p579, sdef57, sdef59, sdef60, sdef63])).
% 78.39/10.60 cnf(p581, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(equilibrium(sk2))) = zero | greater(growth_rate(first_movers,sk3(equilibrium(sk2))),zero) | greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl1 | ~spl30), inference(resolution, [status(thm)], [p280, p80])).
% 78.39/10.60 cnf(ssp45, plain, (~spl1 | ~spl30 | spl57 | spl59 | spl61 | spl63), inference(avatar_split_clause, [status(thm)], [p581, sdef57, sdef59, sdef61, sdef63])).
% 78.39/10.60 cnf(p582, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl1 | ~spl17 | ~spl30), inference(resolution, [status(thm)], [p280, p98])).
% 78.39/10.60 fof(sdef64, definition, (spl64 <=> (greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),growth_rate(first_movers,sk3(equilibrium(sk2)))))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 78.39/10.60 cnf(ssp46, plain, (~spl1 | ~spl17 | ~spl30 | spl57 | spl64), inference(avatar_split_clause, [status(thm)], [p582, sdef57, sdef64])).
% 78.39/10.60 cnf(p584, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(equilibrium(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(equilibrium(sk2)))) | greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~spl1 | ~spl30), inference(resolution, [status(thm)], [p280, p86])).
% 78.39/10.60 cnf(ssp47, plain, (~spl1 | ~spl30 | spl57 | spl60 | spl62 | spl63), inference(avatar_split_clause, [status(thm)], [p584, sdef57, sdef60, sdef62, sdef63])).
% 78.39/10.60 cnf(p585, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(equilibrium(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(equilibrium(sk2)))) | greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl1 | ~spl30), inference(resolution, [status(thm)], [p280, p90])).
% 78.39/10.60 cnf(ssp48, plain, (~spl1 | ~spl30 | spl57 | spl61 | spl62 | spl63), inference(avatar_split_clause, [status(thm)], [p585, sdef57, sdef61, sdef62, sdef63])).
% 78.39/10.60 cnf(p693, plain, (greater(sk3(equilibrium(sk2)),equilibrium(sk2)) | sk3(equilibrium(sk2)) = equilibrium(sk2) | ~spl20 | ~spl26), inference(resolution, [status(thm)], [p152, c2])).
% 78.39/10.60 cnf(ssp49, plain, (~spl20 | ~spl26 | spl52 | spl53), inference(avatar_split_clause, [status(thm)], [p693, sdef52, sdef53])).
% 78.39/10.60 cnf(p370, plain, (greater_or_equal(sk3(sk0(sk2)),sk1(sk2)) | ~spl20 | ~spl45), inference(superposition, [status(thm)], [p355, p113])).
% 78.39/10.60 cnf(p706, plain, (greater(sk3(sk0(sk2)),sk1(sk2)) | sk3(sk0(sk2)) = sk1(sk2) | ~spl20 | ~spl45), inference(resolution, [status(thm)], [p370, c2])).
% 78.39/10.60 cnf(ssp50, plain, (~spl20 | ~spl45 | spl65 | spl66), inference(avatar_split_clause, [status(thm)], [p706, sdef65, sdef66])).
% 78.39/10.60 cnf(p709, plain, (greater(sk3(sk1(sk2)),sk0(sk2)) | sk3(sk1(sk2)) = sk0(sk2) | ~spl20 | ~spl45), inference(resolution, [status(thm)], [p371, c2])).
% 78.39/10.60 cnf(ssp51, plain, (~spl20 | ~spl45 | spl67 | spl68), inference(avatar_split_clause, [status(thm)], [p709, sdef67, sdef68])).
% 78.39/10.60 cnf(p403, plain, (greater_or_equal(sk3(equilibrium(sk2)),sk1(sk2)) | ~spl20 | ~spl47), inference(superposition, [status(thm)], [p358, p113])).
% 78.39/10.60 cnf(p718, plain, (greater(sk3(equilibrium(sk2)),sk1(sk2)) | sk3(equilibrium(sk2)) = sk1(sk2) | ~spl20 | ~spl47), inference(resolution, [status(thm)], [p403, c2])).
% 78.39/10.60 fof(sdef69, definition, (spl69 <=> (greater(sk3(equilibrium(sk2)),sk1(sk2)))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 78.39/10.60 cnf(ssp52, plain, (~spl20 | ~spl47 | spl69 | spl70), inference(avatar_split_clause, [status(thm)], [p718, sdef69, sdef70])).
% 78.39/10.60 cnf(p721, plain, (greater(sk3(sk1(sk2)),equilibrium(sk2)) | sk3(sk1(sk2)) = equilibrium(sk2) | ~spl20 | ~spl47), inference(resolution, [status(thm)], [p404, c2])).
% 78.39/10.60 cnf(ssp53, plain, (~spl20 | ~spl47 | spl71 | spl72), inference(avatar_split_clause, [status(thm)], [p721, sdef71, sdef72])).
% 78.39/10.60 cnf(p739, plain, (greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl1 | ~spl51), inference(superposition, [status(thm)], [p537, p30])).
% 78.39/10.60 cnf(p772, plain, (greater(equilibrium(sk2),sk0(sk2)) | equilibrium(sk2) = sk0(sk2) | ~spl1 | ~spl51), inference(resolution, [status(thm)], [p739, c2])).
% 78.39/10.60 cnf(ssp54, plain, (~spl1 | ~spl51 | spl27 | spl28), inference(avatar_split_clause, [status(thm)], [p772, sdef27, sdef28])).
% 78.39/10.60 cnf(p808, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl1 | ~spl49 | ~spl53), inference(superposition, [status(thm)], [p803, p28])).
% 78.39/10.60 cnf(p843, plain, (greater(equilibrium(sk2),sk1(sk2)) | equilibrium(sk2) = sk1(sk2) | greater(sk1(sk2),equilibrium(sk2)) | ~spl1 | ~spl20 | ~spl49 | ~spl53), inference(resolution, [status(thm)], [p808, p116])).
% 78.39/10.60 cnf(ssp55, plain, (~spl1 | ~spl20 | ~spl49 | ~spl53 | spl25 | spl46 | spl47), inference(avatar_split_clause, [status(thm)], [p843, sdef25, sdef46, sdef47])).
% 78.39/10.60 cnf(p876, plain, (greater(sk1(sk2),sk0(sk2)) | sk1(sk2) = sk0(sk2) | ~spl1 | ~spl66), inference(resolution, [status(thm)], [p854, c2])).
% 78.39/10.60 cnf(ssp56, plain, (~spl1 | ~spl66 | spl21 | spl22), inference(avatar_split_clause, [status(thm)], [p876, sdef21, sdef22])).
% 78.39/10.60 cnf(p889, plain, (greater_or_equal(sk0(sk2),sk1(sk2)) | ~spl20 | ~spl68), inference(superposition, [status(thm)], [p711, p113])).
% 78.39/10.60 cnf(p902, plain, (greater(sk0(sk2),sk1(sk2)) | sk0(sk2) = sk1(sk2) | ~spl20 | ~spl68), inference(resolution, [status(thm)], [p889, c2])).
% 78.39/10.60 cnf(ssp57, plain, (~spl20 | ~spl68 | spl23 | spl45), inference(avatar_split_clause, [status(thm)], [p902, sdef23, sdef45])).
% 78.39/10.60 cnf(p969, plain, (greater_or_equal(equilibrium(sk2),sk1(sk2)) | ~spl20 | ~spl72), inference(superposition, [status(thm)], [p723, p113])).
% 78.39/10.60 cnf(p983, plain, (greater(equilibrium(sk2),sk1(sk2)) | equilibrium(sk2) = sk1(sk2) | ~spl20 | ~spl72), inference(resolution, [status(thm)], [p969, c2])).
% 78.39/10.60 cnf(ssp58, plain, (~spl20 | ~spl72 | spl46 | spl47), inference(avatar_split_clause, [status(thm)], [p983, sdef46, sdef47])).
% 78.39/10.60 cnf(p1026, plain, (greater_or_equal(equilibrium(sk2),sk0(sk2)) | ~spl21 | ~spl31 | ~spl72), inference(superposition, [status(thm)], [p723, p1013])).
% 78.39/10.60 cnf(p1034, plain, (greater(equilibrium(sk2),sk0(sk2)) | equilibrium(sk2) = sk0(sk2) | ~spl21 | ~spl31 | ~spl72), inference(resolution, [status(thm)], [p1026, c2])).
% 78.39/10.60 cnf(ssp59, plain, (~spl21 | ~spl31 | ~spl72 | spl27 | spl28), inference(avatar_split_clause, [status(thm)], [p1034, sdef27, sdef28])).
% 78.39/10.60 cnf(p971, plain, (subpopulations(first_movers,efficient_producers,sk2,equilibrium(sk2)) | ~spl20 | ~spl72), inference(superposition, [status(thm)], [p723, p115])).
% 78.39/10.60 cnf(p1075, plain, (~greater_or_equal(growth_rate(efficient_producers,equilibrium(sk2)),zero) | ~greater(zero,growth_rate(first_movers,equilibrium(sk2))) | outcompetes(efficient_producers,first_movers,equilibrium(sk2)) | ~spl20 | ~spl72), inference(resolution, [status(thm)], [p971, p41])).
% 78.39/10.60 cnf(ssp60, plain, (~spl20 | ~spl72 | spl73 | spl74 | spl75), inference(avatar_split_clause, [status(thm)], [p1075, sdef73, sdef74, sdef75])).
% 78.39/10.60 cnf(p1079, 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) | ~spl20 | ~spl72), inference(resolution, [status(thm)], [p971, p55])).
% 78.39/10.60 cnf(ssp61, plain, (~spl20 | ~spl72 | spl76 | spl77 | spl78 | spl79), inference(avatar_split_clause, [status(thm)], [p1079, sdef76, sdef77, sdef78, sdef79])).
% 78.39/10.60 cnf(p1084, 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))) | ~spl20 | ~spl72), inference(resolution, [status(thm)], [p971, p61])).
% 78.39/10.60 cnf(ssp62, plain, (~spl20 | ~spl72 | spl76 | spl77 | spl78 | spl80), inference(avatar_split_clause, [status(thm)], [p1084, sdef76, sdef77, sdef78, sdef80])).
% 78.39/10.60 cnf(p1086, 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) | ~spl20 | ~spl72), inference(resolution, [status(thm)], [p971, p66])).
% 78.39/10.60 cnf(ssp63, plain, (~spl20 | ~spl72 | spl76 | spl77 | spl79 | spl81), inference(avatar_split_clause, [status(thm)], [p1086, sdef76, sdef77, sdef79, sdef81])).
% 78.39/10.60 cnf(p1088, 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))) | ~spl20 | ~spl72), inference(resolution, [status(thm)], [p971, p71])).
% 78.39/10.60 cnf(ssp64, plain, (~spl20 | ~spl72 | spl76 | spl77 | spl80 | spl81), inference(avatar_split_clause, [status(thm)], [p1088, sdef76, sdef77, sdef80, sdef81])).
% 78.39/10.60 cnf(p1089, 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) | ~spl20 | ~spl72), inference(resolution, [status(thm)], [p971, p78])).
% 78.39/10.60 cnf(ssp65, plain, (~spl20 | ~spl72 | spl76 | spl78 | spl79 | spl82), inference(avatar_split_clause, [status(thm)], [p1089, sdef76, sdef78, sdef79, sdef82])).
% 78.39/10.60 cnf(p1091, 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))) | ~spl20 | ~spl72), inference(resolution, [status(thm)], [p971, p80])).
% 78.39/10.60 cnf(ssp66, plain, (~spl20 | ~spl72 | spl76 | spl78 | spl80 | spl82), inference(avatar_split_clause, [status(thm)], [p1091, sdef76, sdef78, sdef80, sdef82])).
% 78.39/10.60 cnf(p1092, plain, (~greater_or_equal(equilibrium(sk2),sk0(sk2)) | greater(growth_rate(efficient_producers,equilibrium(sk2)),growth_rate(first_movers,equilibrium(sk2))) | ~spl17 | ~spl20 | ~spl72), inference(resolution, [status(thm)], [p971, p98])).
% 78.39/10.60 fof(sdef84, definition, (spl84 <=> (greater(growth_rate(efficient_producers,equilibrium(sk2)),growth_rate(first_movers,equilibrium(sk2))))), introduced(definition, [new_symbols(naming, [spl84])], [avatar_definition])).
% 78.39/10.60 cnf(ssp67, plain, (~spl17 | ~spl20 | ~spl72 | spl83 | spl84), inference(avatar_split_clause, [status(thm)], [p1092, sdef83, sdef84])).
% 78.39/10.60 cnf(p1095, 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) | ~spl20 | ~spl72), inference(resolution, [status(thm)], [p971, p86])).
% 78.39/10.60 cnf(ssp68, plain, (~spl20 | ~spl72 | spl76 | spl79 | spl81 | spl82), inference(avatar_split_clause, [status(thm)], [p1095, sdef76, sdef79, sdef81, sdef82])).
% 78.39/10.60 cnf(p1096, 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))) | ~spl20 | ~spl72), inference(resolution, [status(thm)], [p971, p90])).
% 78.39/10.60 cnf(ssp69, plain, (~spl20 | ~spl72 | spl76 | spl80 | spl81 | spl82), inference(avatar_split_clause, [status(thm)], [p1096, sdef76, sdef80, sdef81, sdef82])).
% 78.39/10.60 cnf(p649, plain, (subpopulations(first_movers,efficient_producers,sk2,sk1(sk2)) | ~spl20 | ~spl32), inference(superposition, [status(thm)], [p328, p115])).
% 78.39/10.60 cnf(p1290, plain, (~greater_or_equal(growth_rate(efficient_producers,sk1(sk2)),zero) | ~greater(zero,growth_rate(first_movers,sk1(sk2))) | outcompetes(efficient_producers,first_movers,sk1(sk2)) | ~spl20 | ~spl32), inference(resolution, [status(thm)], [p649, p41])).
% 78.39/10.60 cnf(ssp70, plain, (~spl20 | ~spl32 | spl85 | spl86 | spl87), inference(avatar_split_clause, [status(thm)], [p1290, sdef85, sdef86, sdef87])).
% 78.39/10.60 cnf(p1294, 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) | ~spl20 | ~spl32), inference(resolution, [status(thm)], [p649, p55])).
% 78.39/10.60 cnf(ssp71, plain, (~spl20 | ~spl32 | spl88 | spl89 | spl90 | spl91), inference(avatar_split_clause, [status(thm)], [p1294, sdef88, sdef89, sdef90, sdef91])).
% 78.39/10.60 cnf(p1299, 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))) | ~spl20 | ~spl32), inference(resolution, [status(thm)], [p649, p61])).
% 78.39/10.60 cnf(ssp72, plain, (~spl20 | ~spl32 | spl88 | spl89 | spl90 | spl92), inference(avatar_split_clause, [status(thm)], [p1299, sdef88, sdef89, sdef90, sdef92])).
% 78.39/10.60 cnf(p1301, 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) | ~spl20 | ~spl32), inference(resolution, [status(thm)], [p649, p66])).
% 78.39/10.60 cnf(ssp73, plain, (~spl20 | ~spl32 | spl88 | spl89 | spl91 | spl93), inference(avatar_split_clause, [status(thm)], [p1301, sdef88, sdef89, sdef91, sdef93])).
% 78.39/10.60 cnf(p1303, 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))) | ~spl20 | ~spl32), inference(resolution, [status(thm)], [p649, p71])).
% 78.39/10.60 cnf(ssp74, plain, (~spl20 | ~spl32 | spl88 | spl89 | spl92 | spl93), inference(avatar_split_clause, [status(thm)], [p1303, sdef88, sdef89, sdef92, sdef93])).
% 78.39/10.60 cnf(p1304, 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) | ~spl20 | ~spl32), inference(resolution, [status(thm)], [p649, p78])).
% 78.39/10.60 cnf(ssp75, plain, (~spl20 | ~spl32 | spl88 | spl90 | spl91 | spl94), inference(avatar_split_clause, [status(thm)], [p1304, sdef88, sdef90, sdef91, sdef94])).
% 78.39/10.60 cnf(p1306, 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))) | ~spl20 | ~spl32), inference(resolution, [status(thm)], [p649, p80])).
% 78.39/10.60 cnf(ssp76, plain, (~spl20 | ~spl32 | spl88 | spl90 | spl92 | spl94), inference(avatar_split_clause, [status(thm)], [p1306, sdef88, sdef90, sdef92, sdef94])).
% 78.39/10.60 cnf(p1307, plain, (~greater_or_equal(sk1(sk2),sk0(sk2)) | greater(growth_rate(efficient_producers,sk1(sk2)),growth_rate(first_movers,sk1(sk2))) | ~spl17 | ~spl20 | ~spl32), inference(resolution, [status(thm)], [p649, p98])).
% 78.39/10.60 fof(sdef96, definition, (spl96 <=> (greater(growth_rate(efficient_producers,sk1(sk2)),growth_rate(first_movers,sk1(sk2))))), introduced(definition, [new_symbols(naming, [spl96])], [avatar_definition])).
% 78.39/10.60 cnf(ssp77, plain, (~spl17 | ~spl20 | ~spl32 | spl95 | spl96), inference(avatar_split_clause, [status(thm)], [p1307, sdef95, sdef96])).
% 78.39/10.60 cnf(p1310, 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) | ~spl20 | ~spl32), inference(resolution, [status(thm)], [p649, p86])).
% 78.39/10.60 cnf(ssp78, plain, (~spl20 | ~spl32 | spl88 | spl91 | spl93 | spl94), inference(avatar_split_clause, [status(thm)], [p1310, sdef88, sdef91, sdef93, sdef94])).
% 78.39/10.60 cnf(p1311, 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))) | ~spl20 | ~spl32), inference(resolution, [status(thm)], [p649, p90])).
% 78.39/10.60 cnf(ssp79, plain, (~spl20 | ~spl32 | spl88 | spl92 | spl93 | spl94), inference(avatar_split_clause, [status(thm)], [p1311, sdef88, sdef92, sdef93, sdef94])).
% 78.39/10.60 cnf(p1323, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl20 | ~spl26 | ~spl68), inference(superposition, [status(thm)], [p138, p889])).
% 78.39/10.60 cnf(p1412, plain, (greater(sk0(sk2),equilibrium(sk2)) | sk0(sk2) = equilibrium(sk2) | ~spl20 | ~spl26 | ~spl68), inference(resolution, [status(thm)], [p1323, c2])).
% 78.39/10.60 cnf(ssp80, plain, (~spl20 | ~spl26 | ~spl68 | spl29 | spl30), inference(avatar_split_clause, [status(thm)], [p1412, sdef29, sdef30])).
% 78.39/10.60 cnf(p123, plain, (in_environment(sk2,sk0(sk2)) | ~spl20 | ~spl22), inference(superposition, [status(thm)], [p119, p112])).
% 78.39/10.60 cnf(p127, plain, (greater_or_equal(sk3(sk0(sk2)),sk0(sk2)) | ~spl20 | ~spl22), inference(resolution, [status(thm)], [p123, c23])).
% 78.39/10.60 cnf(p1634, plain, (greater(sk3(sk0(sk2)),sk0(sk2)) | sk3(sk0(sk2)) = sk0(sk2) | ~spl20 | ~spl22), inference(resolution, [status(thm)], [p127, c2])).
% 78.39/10.60 cnf(ssp81, plain, (~spl20 | ~spl22 | spl2 | spl3), inference(avatar_split_clause, [status(thm)], [p1634, sdef2, sdef3])).
% 78.39/10.60 cnf(p1640, plain, (greater_or_equal(sk1(sk2),sk0(sk2)) | ~spl1 | ~spl28 | ~spl70), inference(superposition, [status(thm)], [p720, p210])).
% 78.39/10.60 cnf(p1641, plain, (greater(sk1(sk2),sk0(sk2)) | sk1(sk2) = sk0(sk2) | ~spl1 | ~spl28 | ~spl70), inference(resolution, [status(thm)], [p1640, c2])).
% 78.39/10.60 cnf(ssp82, plain, (~spl1 | ~spl28 | ~spl70 | spl21 | spl22), inference(avatar_split_clause, [status(thm)], [p1641, sdef21, sdef22])).
% 78.39/10.60 cnf(p1642, plain, (greater_or_equal(sk1(sk2),equilibrium(sk2)) | ~spl1 | ~spl28 | ~spl70), inference(superposition, [status(thm)], [p158, p1640])).
% 78.39/10.60 cnf(p1644, plain, (greater(sk1(sk2),equilibrium(sk2)) | sk1(sk2) = equilibrium(sk2) | ~spl1 | ~spl28 | ~spl70), inference(resolution, [status(thm)], [p1642, c2])).
% 78.39/10.60 cnf(ssp83, plain, (~spl1 | ~spl28 | ~spl70 | spl25 | spl26), inference(avatar_split_clause, [status(thm)], [p1644, sdef25, sdef26])).
% 78.39/10.60 cnf(p261, plain, (greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p209, c23])).
% 78.39/10.60 cnf(p1656, plain, (greater(sk3(equilibrium(sk2)),equilibrium(sk2)) | sk3(equilibrium(sk2)) = equilibrium(sk2) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p261, c2])).
% 78.39/10.60 cnf(ssp84, plain, (~spl1 | ~spl28 | spl52 | spl53), inference(avatar_split_clause, [status(thm)], [p1656, sdef52, sdef53])).
% 78.39/10.60 cnf(p245, plain, (in_environment(sk2,equilibrium(sk2)) | ~spl20 | ~spl22 | ~spl28), inference(superposition, [status(thm)], [p158, p123])).
% 78.39/10.60 cnf(p263, plain, (greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | ~spl20 | ~spl22 | ~spl28), inference(resolution, [status(thm)], [p245, c23])).
% 78.39/10.60 cnf(p1658, plain, (greater(sk3(equilibrium(sk2)),equilibrium(sk2)) | sk3(equilibrium(sk2)) = equilibrium(sk2) | ~spl20 | ~spl22 | ~spl28), inference(resolution, [status(thm)], [p263, c2])).
% 78.39/10.60 cnf(ssp85, plain, (~spl20 | ~spl22 | ~spl28 | spl52 | spl53), inference(avatar_split_clause, [status(thm)], [p1658, sdef52, sdef53])).
% 78.39/10.60 cnf(p1682, plain, (sk1(sk2) = sk0(sk2) | ~spl49 | ~spl70), inference(superposition, [status(thm)], [p720, p534])).
% 78.39/10.60 cnf(p1703, plain, (greater_or_equal(sk0(sk2),equilibrium(sk2)) | ~spl24 | ~spl49 | ~spl70), inference(superposition, [status(thm)], [p1682, p126])).
% 78.39/10.60 cnf(p1767, plain, (greater(sk0(sk2),equilibrium(sk2)) | sk0(sk2) = equilibrium(sk2) | ~spl24 | ~spl49 | ~spl70), inference(resolution, [status(thm)], [p1703, c2])).
% 78.39/10.60 cnf(ssp86, plain, (~spl24 | ~spl49 | ~spl70 | spl29 | spl30), inference(avatar_split_clause, [status(thm)], [p1767, sdef29, sdef30])).
% 78.39/10.60 cnf(p217, plain, (subpopulations(first_movers,efficient_producers,sk2,sk3(equilibrium(sk2))) | ~spl1 | ~spl28), inference(superposition, [status(thm)], [p158, p32])).
% 78.39/10.60 cnf(p1853, plain, (~greater_or_equal(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | outcompetes(efficient_producers,first_movers,sk3(equilibrium(sk2))) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p217, p41])).
% 78.39/10.60 cnf(ssp87, plain, (~spl1 | ~spl28 | spl54 | spl55 | spl56), inference(avatar_split_clause, [status(thm)], [p1853, sdef54, sdef55, sdef56])).
% 78.39/10.60 cnf(p1854, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(equilibrium(sk2))) = zero | greater(growth_rate(first_movers,sk3(equilibrium(sk2))),zero) | greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p217, p55])).
% 78.39/10.60 cnf(ssp88, plain, (~spl1 | ~spl28 | spl57 | spl58 | spl59 | spl60), inference(avatar_split_clause, [status(thm)], [p1854, sdef57, sdef58, sdef59, sdef60])).
% 78.39/10.60 cnf(p1855, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(equilibrium(sk2))) = zero | greater(growth_rate(first_movers,sk3(equilibrium(sk2))),zero) | greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p217, p61])).
% 78.39/10.60 cnf(ssp89, plain, (~spl1 | ~spl28 | spl57 | spl58 | spl59 | spl61), inference(avatar_split_clause, [status(thm)], [p1855, sdef57, sdef58, sdef59, sdef61])).
% 78.39/10.60 cnf(p1856, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(equilibrium(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(equilibrium(sk2)))) | greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p217, p66])).
% 78.39/10.60 cnf(ssp90, plain, (~spl1 | ~spl28 | spl57 | spl58 | spl60 | spl62), inference(avatar_split_clause, [status(thm)], [p1856, sdef57, sdef58, sdef60, sdef62])).
% 78.39/10.60 cnf(p1857, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(first_movers,sk3(equilibrium(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(equilibrium(sk2)))) | greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p217, p71])).
% 78.39/10.60 cnf(ssp91, plain, (~spl1 | ~spl28 | spl57 | spl58 | spl61 | spl62), inference(avatar_split_clause, [status(thm)], [p1857, sdef57, sdef58, sdef61, sdef62])).
% 78.39/10.60 cnf(p1858, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(equilibrium(sk2))) = zero | greater(growth_rate(first_movers,sk3(equilibrium(sk2))),zero) | greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p217, p78])).
% 78.39/10.60 cnf(ssp92, plain, (~spl1 | ~spl28 | spl57 | spl59 | spl60 | spl63), inference(avatar_split_clause, [status(thm)], [p1858, sdef57, sdef59, sdef60, sdef63])).
% 78.39/10.60 cnf(p1859, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(equilibrium(sk2))) = zero | greater(growth_rate(first_movers,sk3(equilibrium(sk2))),zero) | greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p217, p80])).
% 78.39/10.60 cnf(ssp93, plain, (~spl1 | ~spl28 | spl57 | spl59 | spl61 | spl63), inference(avatar_split_clause, [status(thm)], [p1859, sdef57, sdef59, sdef61, sdef63])).
% 78.39/10.60 cnf(p1860, plain, (~greater_or_equal(sk3(equilibrium(sk2)),sk0(sk2)) | greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl1 | ~spl17 | ~spl28), inference(resolution, [status(thm)], [p217, p98])).
% 78.39/10.60 fof(sdef97, definition, (spl97 <=> (~greater_or_equal(sk3(equilibrium(sk2)),sk0(sk2)))), introduced(definition, [new_symbols(naming, [spl97])], [avatar_definition])).
% 78.39/10.60 cnf(ssp94, plain, (~spl1 | ~spl17 | ~spl28 | spl64 | spl97), inference(avatar_split_clause, [status(thm)], [p1860, sdef64, sdef97])).
% 78.39/10.60 cnf(p1862, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(equilibrium(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(equilibrium(sk2)))) | greater(growth_rate(efficient_producers,sk3(equilibrium(sk2))),zero) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p217, p86])).
% 78.39/10.60 cnf(ssp95, plain, (~spl1 | ~spl28 | spl57 | spl60 | spl62 | spl63), inference(avatar_split_clause, [status(thm)], [p1862, sdef57, sdef60, sdef62, sdef63])).
% 78.39/10.60 cnf(p1863, plain, (~greater_or_equal(sk3(equilibrium(sk2)),equilibrium(sk2)) | growth_rate(efficient_producers,sk3(equilibrium(sk2))) = zero | greater(zero,growth_rate(efficient_producers,sk3(equilibrium(sk2)))) | greater(zero,growth_rate(first_movers,sk3(equilibrium(sk2)))) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p217, p90])).
% 78.39/10.60 cnf(ssp96, plain, (~spl1 | ~spl28 | spl57 | spl61 | spl62 | spl63), inference(avatar_split_clause, [status(thm)], [p1863, sdef57, sdef61, sdef62, sdef63])).
% 78.39/10.60 cnf(p262, plain, (~in_environment(sk2,X0) | greater(X0,equilibrium(sk2)) | X0 = equilibrium(sk2) | greater(equilibrium(sk2),X0) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p209, c1])).
% 78.39/10.60 cnf(p1948, plain, (greater(sk0(sk2),equilibrium(sk2)) | sk0(sk2) = equilibrium(sk2) | greater(equilibrium(sk2),sk0(sk2)) | ~spl1 | ~spl28), inference(resolution, [status(thm)], [p262, p28])).
% 78.39/10.60 cnf(ssp97, plain, (~spl1 | ~spl28 | spl27 | spl29 | spl30), inference(avatar_split_clause, [status(thm)], [p1948, sdef27, sdef29, sdef30])).
% 78.39/10.60 cnf(p1949, plain, (greater(sk1(sk2),equilibrium(sk2)) | sk1(sk2) = equilibrium(sk2) | greater(equilibrium(sk2),sk1(sk2)) | ~spl1 | ~spl20 | ~spl28), inference(resolution, [status(thm)], [p262, p112])).
% 78.39/10.60 cnf(ssp98, plain, (~spl1 | ~spl20 | ~spl28 | spl25 | spl26 | spl46), inference(avatar_split_clause, [status(thm)], [p1949, sdef25, sdef26, sdef46])).
% 78.39/10.60 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, 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, sct114, sct115, sct116, sct117, sct118, sct119])).
% 78.39/10.60 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------