%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT023+2 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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 : Tue Sep 8 06:18:41 AM UTC 2026
% Result : Theorem 1.07s 1.34s
% Output : CNFRefutation 1.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT023+2 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.35 % Computer : n028.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 12:09:32 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.41 (re.compile("\."), Token.FullStop),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.41 (re.compile("\("), Token.OpenPar),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.41 (re.compile("\)"), Token.ClosePar),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.41 (re.compile("\["), Token.OpenSquare),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("~\|"), Token.Nor),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("\|"), Token.Or),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.41 (re.compile("\?"), Token.Existential),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.48 """
% 0.22/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.48 """
% 0.32/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.57 """
% 1.07/1.34 % Version: 1.5
% 1.07/1.34 % SZS status Theorem
% 1.07/1.34 % SZS output start CNFRefutation
% 1.07/1.34 fof(prove_l5,conjecture,(![E]:((environment(E)&stable(E))=>in_environment(E,critical_point(E)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_l5)).
% 1.07/1.34 fof(c8,negated_conjecture,(~(![E]:((environment(E)&stable(E))=>in_environment(E,critical_point(E))))),inference(assume_negation,[status(cth)],[prove_l5])).
% 1.07/1.34 fof(c9,negated_conjecture,(?[E]:((environment(E)&stable(E))&~in_environment(E,critical_point(E)))),inference(fof_nnf,[status(thm)],[c8])).
% 1.07/1.34 fof(c10,negated_conjecture,(?[X2]:((environment(X2)&stable(X2))&~in_environment(X2,critical_point(X2)))),inference(variable_rename,[status(thm)],[c9])).
% 1.07/1.34 fof(c11,negated_conjecture,((environment(skolem0001)&stable(skolem0001))&~in_environment(skolem0001,critical_point(skolem0001))),inference(skolemize,[status(esa)],[c10])).
% 1.07/1.34 cnf(c14,negated_conjecture,~in_environment(skolem0001,critical_point(skolem0001)),inference(split_conjunct,[status(thm)],[c11])).
% 1.07/1.34 cnf(reflexivity,axiom,X14=X14,theory(equality)).
% 1.07/1.34 cnf(c3,axiom,X41!=X38|X39!=X40|~in_environment(X41,X39)|in_environment(X38,X40),theory(equality)).
% 1.07/1.34 cnf(c12,negated_conjecture,environment(skolem0001),inference(split_conjunct,[status(thm)],[c11])).
% 1.07/1.34 cnf(c13,negated_conjecture,stable(skolem0001),inference(split_conjunct,[status(thm)],[c11])).
% 1.07/1.34 fof(l1,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)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l1)).
% 1.07/1.34 fof(c15,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(fof_nnf,[status(thm)],[l1])).
% 1.07/1.34 fof(c16,plain,(![X3]:((~environment(X3)|~stable(X3))|(?[X4]:(in_environment(X3,X4)&(![X5]:((~subpopulations(first_movers,efficient_producers,X3,X5)|~greater_or_equal(X5,X4))|greater(growth_rate(efficient_producers,X5),growth_rate(first_movers,X5)))))))),inference(variable_rename,[status(thm)],[c15])).
% 1.07/1.34 fof(c18,plain,(![X3]:(![X5]:((~environment(X3)|~stable(X3))|(in_environment(X3,skolem0002(X3))&((~subpopulations(first_movers,efficient_producers,X3,X5)|~greater_or_equal(X5,skolem0002(X3)))|greater(growth_rate(efficient_producers,X5),growth_rate(first_movers,X5))))))),inference(shift_quantors,[status(thm)],[fof(c17,plain,(![X3]:((~environment(X3)|~stable(X3))|(in_environment(X3,skolem0002(X3))&(![X5]:((~subpopulations(first_movers,efficient_producers,X3,X5)|~greater_or_equal(X5,skolem0002(X3)))|greater(growth_rate(efficient_producers,X5),growth_rate(first_movers,X5))))))),inference(skolemize,[status(esa)],[c16])).])).
% 1.07/1.34 fof(c19,plain,(![X3]:(![X5]:(((~environment(X3)|~stable(X3))|in_environment(X3,skolem0002(X3)))&((~environment(X3)|~stable(X3))|((~subpopulations(first_movers,efficient_producers,X3,X5)|~greater_or_equal(X5,skolem0002(X3)))|greater(growth_rate(efficient_producers,X5),growth_rate(first_movers,X5))))))),inference(distribute,[status(thm)],[c18])).
% 1.07/1.34 cnf(c20,plain,~environment(X37)|~stable(X37)|in_environment(X37,skolem0002(X37)),inference(split_conjunct,[status(thm)],[c19])).
% 1.07/1.34 cnf(c53,plain,~environment(skolem0001)|in_environment(skolem0001,skolem0002(skolem0001)),inference(resolution,[status(thm)],[c20, c13])).
% 1.07/1.34 cnf(c54,plain,in_environment(skolem0001,skolem0002(skolem0001)),inference(resolution,[status(thm)],[c53, c12])).
% 1.07/1.34 fof(mp_earliest_time_growth_rate_exceeds,axiom,(![E]:((environment(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)))))))=>(?[To]:((in_environment(E,To)&(~greater(growth_rate(efficient_producers,To),growth_rate(first_movers,To))))&(![T]:((subpopulations(first_movers,efficient_producers,E,T)&greater(T,To))=>greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds)).
% 1.07/1.34 fof(c30,plain,(![E]:((environment(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)))))))=>(?[To]:((in_environment(E,To)&~greater(growth_rate(efficient_producers,To),growth_rate(first_movers,To)))&(![T]:((subpopulations(first_movers,efficient_producers,E,T)&greater(T,To))=>greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)))))))),inference(fof_simplification,[status(thm)],[mp_earliest_time_growth_rate_exceeds])).
% 1.07/1.34 fof(c31,plain,(![E]:((~environment(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)))))))|(?[To]:((in_environment(E,To)&~greater(growth_rate(efficient_producers,To),growth_rate(first_movers,To)))&(![T]:((~subpopulations(first_movers,efficient_producers,E,T)|~greater(T,To))|greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)))))))),inference(fof_nnf,[status(thm)],[c30])).
% 1.07/1.34 fof(c32,plain,(![X9]:((~environment(X9)|(![X10]:(~in_environment(X9,X10)|(?[X11]:((subpopulations(first_movers,efficient_producers,X9,X11)&greater_or_equal(X11,X10))&~greater(growth_rate(efficient_producers,X11),growth_rate(first_movers,X11)))))))|(?[X12]:((in_environment(X9,X12)&~greater(growth_rate(efficient_producers,X12),growth_rate(first_movers,X12)))&(![X13]:((~subpopulations(first_movers,efficient_producers,X9,X13)|~greater(X13,X12))|greater(growth_rate(efficient_producers,X13),growth_rate(first_movers,X13)))))))),inference(variable_rename,[status(thm)],[c31])).
% 1.07/1.34 fof(c34,plain,(![X9]:(![X10]:(![X13]:((~environment(X9)|(~in_environment(X9,X10)|((subpopulations(first_movers,efficient_producers,X9,skolem0004(X9,X10))&greater_or_equal(skolem0004(X9,X10),X10))&~greater(growth_rate(efficient_producers,skolem0004(X9,X10)),growth_rate(first_movers,skolem0004(X9,X10))))))|((in_environment(X9,skolem0005(X9))&~greater(growth_rate(efficient_producers,skolem0005(X9)),growth_rate(first_movers,skolem0005(X9))))&((~subpopulations(first_movers,efficient_producers,X9,X13)|~greater(X13,skolem0005(X9)))|greater(growth_rate(efficient_producers,X13),growth_rate(first_movers,X13)))))))),inference(shift_quantors,[status(thm)],[fof(c33,plain,(![X9]:((~environment(X9)|(![X10]:(~in_environment(X9,X10)|((subpopulations(first_movers,efficient_producers,X9,skolem0004(X9,X10))&greater_or_equal(skolem0004(X9,X10),X10))&~greater(growth_rate(efficient_producers,skolem0004(X9,X10)),growth_rate(first_movers,skolem0004(X9,X10)))))))|((in_environment(X9,skolem0005(X9))&~greater(growth_rate(efficient_producers,skolem0005(X9)),growth_rate(first_movers,skolem0005(X9))))&(![X13]:((~subpopulations(first_movers,efficient_producers,X9,X13)|~greater(X13,skolem0005(X9)))|greater(growth_rate(efficient_producers,X13),growth_rate(first_movers,X13))))))),inference(skolemize,[status(esa)],[c32])).])).
% 1.07/1.35 fof(c35,plain,(![X9]:(![X10]:(![X13]:((((((~environment(X9)|(~in_environment(X9,X10)|subpopulations(first_movers,efficient_producers,X9,skolem0004(X9,X10))))|in_environment(X9,skolem0005(X9)))&((~environment(X9)|(~in_environment(X9,X10)|subpopulations(first_movers,efficient_producers,X9,skolem0004(X9,X10))))|~greater(growth_rate(efficient_producers,skolem0005(X9)),growth_rate(first_movers,skolem0005(X9)))))&((~environment(X9)|(~in_environment(X9,X10)|subpopulations(first_movers,efficient_producers,X9,skolem0004(X9,X10))))|((~subpopulations(first_movers,efficient_producers,X9,X13)|~greater(X13,skolem0005(X9)))|greater(growth_rate(efficient_producers,X13),growth_rate(first_movers,X13)))))&((((~environment(X9)|(~in_environment(X9,X10)|greater_or_equal(skolem0004(X9,X10),X10)))|in_environment(X9,skolem0005(X9)))&((~environment(X9)|(~in_environment(X9,X10)|greater_or_equal(skolem0004(X9,X10),X10)))|~greater(growth_rate(efficient_producers,skolem0005(X9)),growth_rate(first_movers,skolem0005(X9)))))&((~environment(X9)|(~in_environment(X9,X10)|greater_or_equal(skolem0004(X9,X10),X10)))|((~subpopulations(first_movers,efficient_producers,X9,X13)|~greater(X13,skolem0005(X9)))|greater(growth_rate(efficient_producers,X13),growth_rate(first_movers,X13))))))&((((~environment(X9)|(~in_environment(X9,X10)|~greater(growth_rate(efficient_producers,skolem0004(X9,X10)),growth_rate(first_movers,skolem0004(X9,X10)))))|in_environment(X9,skolem0005(X9)))&((~environment(X9)|(~in_environment(X9,X10)|~greater(growth_rate(efficient_producers,skolem0004(X9,X10)),growth_rate(first_movers,skolem0004(X9,X10)))))|~greater(growth_rate(efficient_producers,skolem0005(X9)),growth_rate(first_movers,skolem0005(X9)))))&((~environment(X9)|(~in_environment(X9,X10)|~greater(growth_rate(efficient_producers,skolem0004(X9,X10)),growth_rate(first_movers,skolem0004(X9,X10)))))|((~subpopulations(first_movers,efficient_producers,X9,X13)|~greater(X13,skolem0005(X9)))|greater(growth_rate(efficient_producers,X13),growth_rate(first_movers,X13))))))))),inference(distribute,[status(thm)],[c34])).
% 1.07/1.35 cnf(c42,plain,~environment(X85)|~in_environment(X85,X86)|~greater(growth_rate(efficient_producers,skolem0004(X85,X86)),growth_rate(first_movers,skolem0004(X85,X86)))|in_environment(X85,skolem0005(X85)),inference(split_conjunct,[status(thm)],[c35])).
% 1.07/1.35 cnf(c39,plain,~environment(X69)|~in_environment(X69,X70)|greater_or_equal(skolem0004(X69,X70),X70)|in_environment(X69,skolem0005(X69)),inference(split_conjunct,[status(thm)],[c35])).
% 1.07/1.35 cnf(c60,plain,~environment(skolem0001)|greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c39, c54])).
% 1.07/1.35 cnf(c62,plain,greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c60, c12])).
% 1.07/1.35 cnf(c21,plain,~environment(X73)|~stable(X73)|~subpopulations(first_movers,efficient_producers,X73,X74)|~greater_or_equal(X74,skolem0002(X73))|greater(growth_rate(efficient_producers,X74),growth_rate(first_movers,X74)),inference(split_conjunct,[status(thm)],[c19])).
% 1.07/1.35 cnf(c36,plain,~environment(X71)|~in_environment(X71,X72)|subpopulations(first_movers,efficient_producers,X71,skolem0004(X71,X72))|in_environment(X71,skolem0005(X71)),inference(split_conjunct,[status(thm)],[c35])).
% 1.07/1.35 cnf(c61,plain,~environment(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001)))|in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c36, c54])).
% 1.07/1.35 cnf(c67,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001)))|in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c61, c12])).
% 1.07/1.35 cnf(c69,plain,in_environment(skolem0001,skolem0005(skolem0001))|~environment(skolem0001)|~stable(skolem0001)|~greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c67, c21])).
% 1.07/1.35 cnf(c123,plain,in_environment(skolem0001,skolem0005(skolem0001))|~environment(skolem0001)|~stable(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c69, c62])).
% 1.07/1.35 cnf(c131,plain,in_environment(skolem0001,skolem0005(skolem0001))|~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c123, c13])).
% 1.07/1.35 cnf(c132,plain,in_environment(skolem0001,skolem0005(skolem0001))|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c131, c12])).
% 1.07/1.35 cnf(c138,plain,in_environment(skolem0001,skolem0005(skolem0001))|~environment(skolem0001)|~in_environment(skolem0001,skolem0002(skolem0001)),inference(resolution,[status(thm)],[c132, c42])).
% 1.07/1.35 cnf(c143,plain,in_environment(skolem0001,skolem0005(skolem0001))|~environment(skolem0001),inference(resolution,[status(thm)],[c138, c54])).
% 1.07/1.35 cnf(c144,plain,in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c143, c12])).
% 1.07/1.35 cnf(c148,plain,skolem0001!=X124|skolem0005(skolem0001)!=X125|in_environment(X124,X125),inference(resolution,[status(thm)],[c144, c3])).
% 1.07/1.35 cnf(c43,plain,~environment(X112)|~in_environment(X112,X113)|~greater(growth_rate(efficient_producers,skolem0004(X112,X113)),growth_rate(first_movers,skolem0004(X112,X113)))|~greater(growth_rate(efficient_producers,skolem0005(X112)),growth_rate(first_movers,skolem0005(X112))),inference(split_conjunct,[status(thm)],[c35])).
% 1.07/1.35 cnf(c40,plain,~environment(X75)|~in_environment(X75,X76)|greater_or_equal(skolem0004(X75,X76),X76)|~greater(growth_rate(efficient_producers,skolem0005(X75)),growth_rate(first_movers,skolem0005(X75))),inference(split_conjunct,[status(thm)],[c35])).
% 1.07/1.35 fof(d1,plain,(![E]:(![To]:((((environment(E)&(~greater(growth_rate(efficient_producers,To),growth_rate(first_movers,To))))&in_environment(E,To))&(![T]:((subpopulations(first_movers,efficient_producers,E,T)&greater(T,To))=>greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)))))=>To=critical_point(E)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1)).
% 1.07/1.35 fof(c22,plain,(![E]:(![To]:((((environment(E)&~greater(growth_rate(efficient_producers,To),growth_rate(first_movers,To)))&in_environment(E,To))&(![T]:((subpopulations(first_movers,efficient_producers,E,T)&greater(T,To))=>greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)))))=>To=critical_point(E)))),inference(fof_simplification,[status(thm)],[d1])).
% 1.07/1.35 fof(c23,plain,(![E]:(![To]:((((~environment(E)|greater(growth_rate(efficient_producers,To),growth_rate(first_movers,To)))|~in_environment(E,To))|(?[T]:((subpopulations(first_movers,efficient_producers,E,T)&greater(T,To))&~greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)))))|To=critical_point(E)))),inference(fof_nnf,[status(thm)],[c22])).
% 1.07/1.35 fof(c24,plain,(![X6]:(![X7]:((((~environment(X6)|greater(growth_rate(efficient_producers,X7),growth_rate(first_movers,X7)))|~in_environment(X6,X7))|(?[X8]:((subpopulations(first_movers,efficient_producers,X6,X8)&greater(X8,X7))&~greater(growth_rate(efficient_producers,X8),growth_rate(first_movers,X8)))))|X7=critical_point(X6)))),inference(variable_rename,[status(thm)],[c23])).
% 1.07/1.35 fof(c25,plain,(![X6]:(![X7]:((((~environment(X6)|greater(growth_rate(efficient_producers,X7),growth_rate(first_movers,X7)))|~in_environment(X6,X7))|((subpopulations(first_movers,efficient_producers,X6,skolem0003(X6,X7))&greater(skolem0003(X6,X7),X7))&~greater(growth_rate(efficient_producers,skolem0003(X6,X7)),growth_rate(first_movers,skolem0003(X6,X7)))))|X7=critical_point(X6)))),inference(skolemize,[status(esa)],[c24])).
% 1.07/1.35 fof(c26,plain,(![X6]:(![X7]:((((((~environment(X6)|greater(growth_rate(efficient_producers,X7),growth_rate(first_movers,X7)))|~in_environment(X6,X7))|subpopulations(first_movers,efficient_producers,X6,skolem0003(X6,X7)))|X7=critical_point(X6))&((((~environment(X6)|greater(growth_rate(efficient_producers,X7),growth_rate(first_movers,X7)))|~in_environment(X6,X7))|greater(skolem0003(X6,X7),X7))|X7=critical_point(X6)))&((((~environment(X6)|greater(growth_rate(efficient_producers,X7),growth_rate(first_movers,X7)))|~in_environment(X6,X7))|~greater(growth_rate(efficient_producers,skolem0003(X6,X7)),growth_rate(first_movers,skolem0003(X6,X7))))|X7=critical_point(X6))))),inference(distribute,[status(thm)],[c25])).
% 1.07/1.35 cnf(c29,plain,~environment(X89)|greater(growth_rate(efficient_producers,X90),growth_rate(first_movers,X90))|~in_environment(X89,X90)|~greater(growth_rate(efficient_producers,skolem0003(X89,X90)),growth_rate(first_movers,skolem0003(X89,X90)))|X90=critical_point(X89),inference(split_conjunct,[status(thm)],[c26])).
% 1.07/1.35 cnf(c28,plain,~environment(X87)|greater(growth_rate(efficient_producers,X88),growth_rate(first_movers,X88))|~in_environment(X87,X88)|greater(skolem0003(X87,X88),X88)|X88=critical_point(X87),inference(split_conjunct,[status(thm)],[c26])).
% 1.07/1.35 cnf(c149,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c144, c28])).
% 1.07/1.35 cnf(c183,plain,greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c149, c12])).
% 1.07/1.35 cnf(c192,plain,greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|skolem0001!=X168|in_environment(X168,critical_point(skolem0001)),inference(resolution,[status(thm)],[c183, c148])).
% 1.07/1.35 cnf(c297,plain,greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|in_environment(skolem0001,critical_point(skolem0001)),inference(resolution,[status(thm)],[c192, reflexivity])).
% 1.07/1.35 cnf(c303,plain,greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001)),inference(resolution,[status(thm)],[c297, c14])).
% 1.07/1.35 cnf(c184,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|skolem0005(skolem0001)=critical_point(skolem0001)|~environment(skolem0001)|~in_environment(skolem0001,X134)|greater_or_equal(skolem0004(skolem0001,X134),X134),inference(resolution,[status(thm)],[c183, c40])).
% 1.07/1.35 cnf(c198,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|skolem0005(skolem0001)=critical_point(skolem0001)|~environment(skolem0001)|greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001)),inference(resolution,[status(thm)],[c184, c54])).
% 1.07/1.35 cnf(c254,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|skolem0005(skolem0001)=critical_point(skolem0001)|greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001)),inference(resolution,[status(thm)],[c198, c12])).
% 1.07/1.35 cnf(c260,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0001!=X150|in_environment(X150,critical_point(skolem0001)),inference(resolution,[status(thm)],[c254, c148])).
% 1.07/1.35 cnf(c278,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|in_environment(skolem0001,critical_point(skolem0001)),inference(resolution,[status(thm)],[c260, reflexivity])).
% 1.07/1.35 cnf(c282,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001)),inference(resolution,[status(thm)],[c278, c14])).
% 1.07/1.35 cnf(c37,plain,~environment(X94)|~in_environment(X94,X95)|subpopulations(first_movers,efficient_producers,X94,skolem0004(X94,X95))|~greater(growth_rate(efficient_producers,skolem0005(X94)),growth_rate(first_movers,skolem0005(X94))),inference(split_conjunct,[status(thm)],[c35])).
% 1.07/1.35 cnf(c311,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|~in_environment(skolem0001,X171)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,X171)),inference(resolution,[status(thm)],[c303, c37])).
% 1.07/1.35 cnf(c317,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c311, c54])).
% 1.07/1.35 cnf(c324,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c317, c12])).
% 1.07/1.35 cnf(c327,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|~stable(skolem0001)|~greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c324, c21])).
% 1.07/1.35 cnf(c633,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|~stable(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c327, c282])).
% 1.07/1.35 cnf(c634,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c633, c13])).
% 1.07/1.35 cnf(c635,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c634, c12])).
% 1.07/1.35 cnf(c638,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|~in_environment(skolem0001,skolem0002(skolem0001))|~greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c635, c43])).
% 1.07/1.35 cnf(c642,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|~in_environment(skolem0001,skolem0002(skolem0001)),inference(resolution,[status(thm)],[c638, c303])).
% 1.07/1.35 cnf(c643,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001),inference(resolution,[status(thm)],[c642, c54])).
% 1.07/1.35 cnf(c644,plain,greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001)),inference(resolution,[status(thm)],[c643, c12])).
% 1.07/1.35 cnf(c41,plain,~environment(X97)|~in_environment(X97,X98)|greater_or_equal(skolem0004(X97,X98),X98)|~subpopulations(first_movers,efficient_producers,X97,X96)|~greater(X96,skolem0005(X97))|greater(growth_rate(efficient_producers,X96),growth_rate(first_movers,X96)),inference(split_conjunct,[status(thm)],[c35])).
% 1.07/1.35 cnf(c27,plain,~environment(X80)|greater(growth_rate(efficient_producers,X81),growth_rate(first_movers,X81))|~in_environment(X80,X81)|subpopulations(first_movers,efficient_producers,X80,skolem0003(X80,X81))|X81=critical_point(X80),inference(split_conjunct,[status(thm)],[c26])).
% 1.07/1.35 cnf(c145,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c144, c27])).
% 1.07/1.35 cnf(c391,plain,greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c145, c12])).
% 1.07/1.35 cnf(c406,plain,greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|skolem0001!=X275|in_environment(X275,critical_point(skolem0001)),inference(resolution,[status(thm)],[c391, c148])).
% 1.07/1.35 cnf(c550,plain,greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|in_environment(skolem0001,critical_point(skolem0001)),inference(resolution,[status(thm)],[c406, reflexivity])).
% 1.07/1.35 cnf(c560,plain,greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c550, c14])).
% 1.07/1.35 cnf(c392,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|skolem0005(skolem0001)=critical_point(skolem0001)|~environment(skolem0001)|~in_environment(skolem0001,X253)|greater_or_equal(skolem0004(skolem0001,X253),X253),inference(resolution,[status(thm)],[c391, c40])).
% 1.07/1.35 cnf(c415,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|skolem0005(skolem0001)=critical_point(skolem0001)|~environment(skolem0001)|greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001)),inference(resolution,[status(thm)],[c392, c54])).
% 1.07/1.35 cnf(c491,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|skolem0005(skolem0001)=critical_point(skolem0001)|greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001)),inference(resolution,[status(thm)],[c415, c12])).
% 1.07/1.35 cnf(c504,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0001!=X265|in_environment(X265,critical_point(skolem0001)),inference(resolution,[status(thm)],[c491, c148])).
% 1.07/1.35 cnf(c527,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|in_environment(skolem0001,critical_point(skolem0001)),inference(resolution,[status(thm)],[c504, reflexivity])).
% 1.07/1.35 cnf(c535,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001)),inference(resolution,[status(thm)],[c527, c14])).
% 1.07/1.35 cnf(c569,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|~environment(skolem0001)|~in_environment(skolem0001,X279)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,X279)),inference(resolution,[status(thm)],[c560, c37])).
% 1.07/1.35 cnf(c578,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|~environment(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c569, c54])).
% 1.07/1.35 cnf(c588,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c578, c12])).
% 1.07/1.35 cnf(c594,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|~environment(skolem0001)|~stable(skolem0001)|~greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c588, c21])).
% 1.07/1.35 cnf(c648,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|~environment(skolem0001)|~stable(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c594, c535])).
% 1.07/1.35 cnf(c649,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c648, c13])).
% 1.07/1.35 cnf(c650,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c649, c12])).
% 1.07/1.35 cnf(c656,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|~environment(skolem0001)|~in_environment(skolem0001,skolem0002(skolem0001))|~greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c650, c43])).
% 1.07/1.35 cnf(c659,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|~environment(skolem0001)|~in_environment(skolem0001,skolem0002(skolem0001)),inference(resolution,[status(thm)],[c656, c560])).
% 1.07/1.35 cnf(c660,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001)))|~environment(skolem0001),inference(resolution,[status(thm)],[c659, c54])).
% 1.07/1.35 cnf(c661,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c660, c12])).
% 1.07/1.35 cnf(c665,plain,~environment(skolem0001)|~in_environment(skolem0001,X535)|greater_or_equal(skolem0004(skolem0001,X535),X535)|~greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0005(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c661, c41])).
% 1.07/1.35 cnf(c670,plain,~environment(skolem0001)|~in_environment(skolem0001,X536)|greater_or_equal(skolem0004(skolem0001,X536),X536)|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0005(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c665, c644])).
% 1.07/1.35 cnf(c672,plain,~environment(skolem0001)|greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0005(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c670, c54])).
% 1.07/1.35 cnf(c677,plain,greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0005(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c672, c12])).
% 1.07/1.35 cnf(c679,plain,greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|~in_environment(skolem0001,skolem0005(skolem0001))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c677, c29])).
% 1.07/1.35 cnf(c742,plain,greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c679, c144])).
% 1.07/1.35 cnf(c743,plain,greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c742, c12])).
% 1.07/1.35 cnf(c745,plain,greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0005(skolem0001)=critical_point(skolem0001)|~environment(skolem0001)|~in_environment(skolem0001,X592)|greater_or_equal(skolem0004(skolem0001,X592),X592),inference(resolution,[status(thm)],[c743, c40])).
% 1.07/1.35 cnf(c760,plain,greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0005(skolem0001)=critical_point(skolem0001)|~environment(skolem0001),inference(resolution,[status(thm)],[c745, c54])).
% 1.07/1.35 cnf(c761,plain,greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c760, c12])).
% 1.07/1.35 cnf(c773,plain,greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0001!=X595|in_environment(X595,critical_point(skolem0001)),inference(resolution,[status(thm)],[c761, c148])).
% 1.07/1.35 cnf(c783,plain,greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|in_environment(skolem0001,critical_point(skolem0001)),inference(resolution,[status(thm)],[c773, reflexivity])).
% 1.07/1.35 cnf(c786,plain,greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001)),inference(resolution,[status(thm)],[c783, c14])).
% 1.07/1.35 cnf(c38,plain,~environment(X100)|~in_environment(X100,X101)|subpopulations(first_movers,efficient_producers,X100,skolem0004(X100,X101))|~subpopulations(first_movers,efficient_producers,X100,X99)|~greater(X99,skolem0005(X100))|greater(growth_rate(efficient_producers,X99),growth_rate(first_movers,X99)),inference(split_conjunct,[status(thm)],[c35])).
% 1.07/1.35 cnf(c664,plain,~environment(skolem0001)|~in_environment(skolem0001,X635)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,X635))|~greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0005(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c661, c38])).
% 1.07/1.35 cnf(c797,plain,~environment(skolem0001)|~in_environment(skolem0001,X636)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,X636))|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0005(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c664, c644])).
% 1.07/1.35 cnf(c799,plain,~environment(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001)))|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0005(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c797, c54])).
% 1.07/1.35 cnf(c807,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001)))|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0005(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c799, c12])).
% 1.07/1.35 cnf(c812,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001)))|~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|~in_environment(skolem0001,skolem0005(skolem0001))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c807, c29])).
% 1.07/1.35 cnf(c895,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001)))|~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c812, c144])).
% 1.07/1.35 cnf(c896,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001)))|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c895, c12])).
% 1.07/1.35 cnf(c914,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001)))|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|skolem0001!=X695|in_environment(X695,critical_point(skolem0001)),inference(resolution,[status(thm)],[c896, c148])).
% 1.07/1.35 cnf(c934,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001)))|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|in_environment(skolem0001,critical_point(skolem0001)),inference(resolution,[status(thm)],[c914, reflexivity])).
% 1.07/1.35 cnf(c942,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001)))|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c934, c14])).
% 1.07/1.35 cnf(c957,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001)))|~environment(skolem0001)|~in_environment(skolem0001,X698)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,X698)),inference(resolution,[status(thm)],[c942, c37])).
% 1.07/1.35 cnf(c962,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001)))|~environment(skolem0001),inference(resolution,[status(thm)],[c957, c54])).
% 1.07/1.35 cnf(c963,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c962, c12])).
% 1.07/1.35 cnf(c965,plain,~environment(skolem0001)|~stable(skolem0001)|~greater_or_equal(skolem0004(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c963, c21])).
% 1.07/1.35 cnf(c972,plain,~environment(skolem0001)|~stable(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c965, c786])).
% 1.07/1.35 cnf(c973,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c972, c13])).
% 1.07/1.35 cnf(c974,plain,greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c973, c12])).
% 1.07/1.35 cnf(c976,plain,~environment(skolem0001)|~in_environment(skolem0001,skolem0002(skolem0001))|~greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c974, c43])).
% 1.07/1.35 cnf(c44,plain,~environment(X115)|~in_environment(X115,X116)|~greater(growth_rate(efficient_producers,skolem0004(X115,X116)),growth_rate(first_movers,skolem0004(X115,X116)))|~subpopulations(first_movers,efficient_producers,X115,X114)|~greater(X114,skolem0005(X115))|greater(growth_rate(efficient_producers,X114),growth_rate(first_movers,X114)),inference(split_conjunct,[status(thm)],[c35])).
% 1.07/1.35 cnf(c978,plain,~environment(skolem0001)|~in_environment(skolem0001,skolem0002(skolem0001))|~subpopulations(first_movers,efficient_producers,skolem0001,X724)|~greater(X724,skolem0005(skolem0001))|greater(growth_rate(efficient_producers,X724),growth_rate(first_movers,X724)),inference(resolution,[status(thm)],[c974, c44])).
% 1.07/1.35 cnf(c984,plain,~environment(skolem0001)|~in_environment(skolem0001,skolem0002(skolem0001))|~greater(skolem0003(skolem0001,skolem0005(skolem0001)),skolem0005(skolem0001))|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0005(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c978, c661])).
% 1.07/1.35 cnf(c985,plain,~environment(skolem0001)|~in_environment(skolem0001,skolem0002(skolem0001))|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0005(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c984, c644])).
% 1.07/1.35 cnf(c986,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0005(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c985, c54])).
% 1.07/1.35 cnf(c987,plain,greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0005(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c986, c12])).
% 1.07/1.35 cnf(c988,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|~in_environment(skolem0001,skolem0005(skolem0001))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c987, c29])).
% 1.07/1.35 cnf(c992,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c988, c144])).
% 1.07/1.35 cnf(c993,plain,greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c992, c12])).
% 1.07/1.35 cnf(c994,plain,skolem0005(skolem0001)=critical_point(skolem0001)|~environment(skolem0001)|~in_environment(skolem0001,skolem0002(skolem0001)),inference(resolution,[status(thm)],[c993, c976])).
% 1.07/1.35 cnf(c1009,plain,skolem0005(skolem0001)=critical_point(skolem0001)|~environment(skolem0001),inference(resolution,[status(thm)],[c994, c54])).
% 1.07/1.35 cnf(c1010,plain,skolem0005(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c1009, c12])).
% 1.07/1.35 cnf(c1021,plain,skolem0001!=X744|in_environment(X744,critical_point(skolem0001)),inference(resolution,[status(thm)],[c1010, c148])).
% 1.07/1.35 cnf(c1030,plain,in_environment(skolem0001,critical_point(skolem0001)),inference(resolution,[status(thm)],[c1021, reflexivity])).
% 1.07/1.35 cnf(c1031,plain,$false,inference(resolution,[status(thm)],[c1030, c14])).
% 1.07/1.35 % SZS output end CNFRefutation
% 1.07/1.35
% 1.07/1.35 % Initial clauses : 28
% 1.07/1.35 % Processed clauses : 369
% 1.07/1.35 % Factors computed : 2
% 1.07/1.35 % Resolvents computed: 990
% 1.07/1.35 % Tautologies deleted: 4
% 1.07/1.35 % Forward subsumed : 527
% 1.07/1.35 % Backward subsumed : 278
% 1.07/1.35 % -------- CPU Time ---------
% 1.07/1.35 % User time : 0.969 s
% 1.07/1.35 % System time : 0.031 s
% 1.07/1.35 % Total time : 1.000 s
%------------------------------------------------------------------------------