%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT028+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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:42 AM UTC 2026
% Result : Theorem 0.38s 0.67s
% Output : CNFRefutation 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT028+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 7 12:14:52 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.43 (re.compile("\."), Token.FullStop),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.43 (re.compile("\("), Token.OpenPar),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.43 (re.compile("\)"), Token.ClosePar),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.43 (re.compile("\["), Token.OpenSquare),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("~\|"), Token.Nor),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("\|"), Token.Or),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.43 (re.compile("\?"), Token.Existential),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.09/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.09/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.21/0.50 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.50 """
% 0.21/0.50 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.50 """
% 0.31/0.59 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.31/0.59 """
% 0.38/0.67 % Version: 1.5
% 0.38/0.67 % SZS status Theorem
% 0.38/0.67 % SZS output start CNFRefutation
% 0.38/0.67 fof(prove_l10,conjecture,(![E]:((environment(E)&stable(E))=>(?[To]:(greater(To,appear(efficient_producers,E))&(![T]:((subpopulations(first_movers,efficient_producers,E,T)&greater_or_equal(T,To))=>greater(zero,growth_rate(first_movers,T)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l10)).
% 0.38/0.67 fof(c0,negated_conjecture,(~(![E]:((environment(E)&stable(E))=>(?[To]:(greater(To,appear(efficient_producers,E))&(![T]:((subpopulations(first_movers,efficient_producers,E,T)&greater_or_equal(T,To))=>greater(zero,growth_rate(first_movers,T))))))))),inference(assume_negation,[status(cth)],[prove_l10])).
% 0.38/0.67 fof(c1,negated_conjecture,(?[E]:((environment(E)&stable(E))&(![To]:(~greater(To,appear(efficient_producers,E))|(?[T]:((subpopulations(first_movers,efficient_producers,E,T)&greater_or_equal(T,To))&~greater(zero,growth_rate(first_movers,T)))))))),inference(fof_nnf,[status(thm)],[c0])).
% 0.38/0.67 fof(c2,negated_conjecture,(?[X2]:((environment(X2)&stable(X2))&(![X3]:(~greater(X3,appear(efficient_producers,X2))|(?[X4]:((subpopulations(first_movers,efficient_producers,X2,X4)&greater_or_equal(X4,X3))&~greater(zero,growth_rate(first_movers,X4)))))))),inference(variable_rename,[status(thm)],[c1])).
% 0.38/0.67 fof(c4,negated_conjecture,(![X3]:((environment(skolem0001)&stable(skolem0001))&(~greater(X3,appear(efficient_producers,skolem0001))|((subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(X3))&greater_or_equal(skolem0002(X3),X3))&~greater(zero,growth_rate(first_movers,skolem0002(X3))))))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,((environment(skolem0001)&stable(skolem0001))&(![X3]:(~greater(X3,appear(efficient_producers,skolem0001))|((subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(X3))&greater_or_equal(skolem0002(X3),X3))&~greater(zero,growth_rate(first_movers,skolem0002(X3))))))),inference(skolemize,[status(esa)],[c2])).])).
% 0.38/0.67 fof(c5,negated_conjecture,(![X3]:((environment(skolem0001)&stable(skolem0001))&(((~greater(X3,appear(efficient_producers,skolem0001))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(X3)))&(~greater(X3,appear(efficient_producers,skolem0001))|greater_or_equal(skolem0002(X3),X3)))&(~greater(X3,appear(efficient_producers,skolem0001))|~greater(zero,growth_rate(first_movers,skolem0002(X3))))))),inference(distribute,[status(thm)],[c4])).
% 0.38/0.67 cnf(c6,negated_conjecture,environment(skolem0001),inference(split_conjunct,[status(thm)],[c5])).
% 0.38/0.67 cnf(c7,negated_conjecture,stable(skolem0001),inference(split_conjunct,[status(thm)],[c5])).
% 0.38/0.67 fof(l11,plain,(![E]:((environment(E)&stable(E))=>(?[To]:(in_environment(E,To)&(![T]:((subpopulations(first_movers,efficient_producers,E,T)&greater_or_equal(T,To))=>(greater(growth_rate(efficient_producers,T),zero)&greater(zero,growth_rate(first_movers,T))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', l11)).
% 0.38/0.67 fof(c11,plain,(![E]:((~environment(E)|~stable(E))|(?[To]:(in_environment(E,To)&(![T]:((~subpopulations(first_movers,efficient_producers,E,T)|~greater_or_equal(T,To))|(greater(growth_rate(efficient_producers,T),zero)&greater(zero,growth_rate(first_movers,T))))))))),inference(fof_nnf,[status(thm)],[l11])).
% 0.38/0.67 fof(c12,plain,(![X5]:((~environment(X5)|~stable(X5))|(?[X6]:(in_environment(X5,X6)&(![X7]:((~subpopulations(first_movers,efficient_producers,X5,X7)|~greater_or_equal(X7,X6))|(greater(growth_rate(efficient_producers,X7),zero)&greater(zero,growth_rate(first_movers,X7))))))))),inference(variable_rename,[status(thm)],[c11])).
% 0.38/0.67 fof(c14,plain,(![X5]:(![X7]:((~environment(X5)|~stable(X5))|(in_environment(X5,skolem0003(X5))&((~subpopulations(first_movers,efficient_producers,X5,X7)|~greater_or_equal(X7,skolem0003(X5)))|(greater(growth_rate(efficient_producers,X7),zero)&greater(zero,growth_rate(first_movers,X7)))))))),inference(shift_quantors,[status(thm)],[fof(c13,plain,(![X5]:((~environment(X5)|~stable(X5))|(in_environment(X5,skolem0003(X5))&(![X7]:((~subpopulations(first_movers,efficient_producers,X5,X7)|~greater_or_equal(X7,skolem0003(X5)))|(greater(growth_rate(efficient_producers,X7),zero)&greater(zero,growth_rate(first_movers,X7)))))))),inference(skolemize,[status(esa)],[c12])).])).
% 0.38/0.67 fof(c15,plain,(![X5]:(![X7]:(((~environment(X5)|~stable(X5))|in_environment(X5,skolem0003(X5)))&(((~environment(X5)|~stable(X5))|((~subpopulations(first_movers,efficient_producers,X5,X7)|~greater_or_equal(X7,skolem0003(X5)))|greater(growth_rate(efficient_producers,X7),zero)))&((~environment(X5)|~stable(X5))|((~subpopulations(first_movers,efficient_producers,X5,X7)|~greater_or_equal(X7,skolem0003(X5)))|greater(zero,growth_rate(first_movers,X7)))))))),inference(distribute,[status(thm)],[c14])).
% 0.38/0.67 cnf(c16,plain,~environment(X13)|~stable(X13)|in_environment(X13,skolem0003(X13)),inference(split_conjunct,[status(thm)],[c15])).
% 0.38/0.67 cnf(c30,plain,~environment(skolem0001)|in_environment(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c16, c7])).
% 0.38/0.67 cnf(c31,plain,in_environment(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c30, c6])).
% 0.38/0.67 fof(mp_first_movers_negative_growth,axiom,(![E]:(((environment(E)&stable(E))&(?[T1]:(in_environment(E,T1)&(![T]:((subpopulations(first_movers,efficient_producers,E,T)&greater_or_equal(T,T1))=>greater(zero,growth_rate(first_movers,T)))))))=>(?[T2]:(greater(T2,appear(efficient_producers,E))&(![T]:((subpopulations(first_movers,efficient_producers,E,T)&greater_or_equal(T,T2))=>greater(zero,growth_rate(first_movers,T)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_first_movers_negative_growth)).
% 0.38/0.67 fof(c19,plain,(![E]:(((~environment(E)|~stable(E))|(![T1]:(~in_environment(E,T1)|(?[T]:((subpopulations(first_movers,efficient_producers,E,T)&greater_or_equal(T,T1))&~greater(zero,growth_rate(first_movers,T)))))))|(?[T2]:(greater(T2,appear(efficient_producers,E))&(![T]:((~subpopulations(first_movers,efficient_producers,E,T)|~greater_or_equal(T,T2))|greater(zero,growth_rate(first_movers,T)))))))),inference(fof_nnf,[status(thm)],[mp_first_movers_negative_growth])).
% 0.38/0.67 fof(c20,plain,(![X8]:(((~environment(X8)|~stable(X8))|(![X9]:(~in_environment(X8,X9)|(?[X10]:((subpopulations(first_movers,efficient_producers,X8,X10)&greater_or_equal(X10,X9))&~greater(zero,growth_rate(first_movers,X10)))))))|(?[X11]:(greater(X11,appear(efficient_producers,X8))&(![X12]:((~subpopulations(first_movers,efficient_producers,X8,X12)|~greater_or_equal(X12,X11))|greater(zero,growth_rate(first_movers,X12)))))))),inference(variable_rename,[status(thm)],[c19])).
% 0.38/0.67 fof(c22,plain,(![X8]:(![X9]:(![X12]:(((~environment(X8)|~stable(X8))|(~in_environment(X8,X9)|((subpopulations(first_movers,efficient_producers,X8,skolem0004(X8,X9))&greater_or_equal(skolem0004(X8,X9),X9))&~greater(zero,growth_rate(first_movers,skolem0004(X8,X9))))))|(greater(skolem0005(X8),appear(efficient_producers,X8))&((~subpopulations(first_movers,efficient_producers,X8,X12)|~greater_or_equal(X12,skolem0005(X8)))|greater(zero,growth_rate(first_movers,X12)))))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,(![X8]:(((~environment(X8)|~stable(X8))|(![X9]:(~in_environment(X8,X9)|((subpopulations(first_movers,efficient_producers,X8,skolem0004(X8,X9))&greater_or_equal(skolem0004(X8,X9),X9))&~greater(zero,growth_rate(first_movers,skolem0004(X8,X9)))))))|(greater(skolem0005(X8),appear(efficient_producers,X8))&(![X12]:((~subpopulations(first_movers,efficient_producers,X8,X12)|~greater_or_equal(X12,skolem0005(X8)))|greater(zero,growth_rate(first_movers,X12))))))),inference(skolemize,[status(esa)],[c20])).])).
% 0.38/0.67 fof(c23,plain,(![X8]:(![X9]:(![X12]:((((((~environment(X8)|~stable(X8))|(~in_environment(X8,X9)|subpopulations(first_movers,efficient_producers,X8,skolem0004(X8,X9))))|greater(skolem0005(X8),appear(efficient_producers,X8)))&(((~environment(X8)|~stable(X8))|(~in_environment(X8,X9)|subpopulations(first_movers,efficient_producers,X8,skolem0004(X8,X9))))|((~subpopulations(first_movers,efficient_producers,X8,X12)|~greater_or_equal(X12,skolem0005(X8)))|greater(zero,growth_rate(first_movers,X12)))))&((((~environment(X8)|~stable(X8))|(~in_environment(X8,X9)|greater_or_equal(skolem0004(X8,X9),X9)))|greater(skolem0005(X8),appear(efficient_producers,X8)))&(((~environment(X8)|~stable(X8))|(~in_environment(X8,X9)|greater_or_equal(skolem0004(X8,X9),X9)))|((~subpopulations(first_movers,efficient_producers,X8,X12)|~greater_or_equal(X12,skolem0005(X8)))|greater(zero,growth_rate(first_movers,X12))))))&((((~environment(X8)|~stable(X8))|(~in_environment(X8,X9)|~greater(zero,growth_rate(first_movers,skolem0004(X8,X9)))))|greater(skolem0005(X8),appear(efficient_producers,X8)))&(((~environment(X8)|~stable(X8))|(~in_environment(X8,X9)|~greater(zero,growth_rate(first_movers,skolem0004(X8,X9)))))|((~subpopulations(first_movers,efficient_producers,X8,X12)|~greater_or_equal(X12,skolem0005(X8)))|greater(zero,growth_rate(first_movers,X12))))))))),inference(distribute,[status(thm)],[c22])).
% 0.38/0.67 cnf(c28,plain,~environment(X25)|~stable(X25)|~in_environment(X25,X26)|~greater(zero,growth_rate(first_movers,skolem0004(X25,X26)))|greater(skolem0005(X25),appear(efficient_producers,X25)),inference(split_conjunct,[status(thm)],[c23])).
% 0.38/0.67 cnf(c26,plain,~environment(X17)|~stable(X17)|~in_environment(X17,X18)|greater_or_equal(skolem0004(X17,X18),X18)|greater(skolem0005(X17),appear(efficient_producers,X17)),inference(split_conjunct,[status(thm)],[c23])).
% 0.38/0.67 cnf(c32,plain,~environment(skolem0001)|~stable(skolem0001)|greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c26, c31])).
% 0.38/0.67 cnf(c34,plain,~environment(skolem0001)|greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c32, c7])).
% 0.38/0.67 cnf(c35,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c34, c6])).
% 0.38/0.67 cnf(c18,plain,~environment(X22)|~stable(X22)|~subpopulations(first_movers,efficient_producers,X22,X21)|~greater_or_equal(X21,skolem0003(X22))|greater(zero,growth_rate(first_movers,X21)),inference(split_conjunct,[status(thm)],[c15])).
% 0.38/0.67 cnf(c24,plain,~environment(X23)|~stable(X23)|~in_environment(X23,X24)|subpopulations(first_movers,efficient_producers,X23,skolem0004(X23,X24))|greater(skolem0005(X23),appear(efficient_producers,X23)),inference(split_conjunct,[status(thm)],[c23])).
% 0.38/0.67 cnf(c33,plain,~environment(skolem0001)|~stable(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c24, c31])).
% 0.38/0.67 cnf(c41,plain,~environment(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c33, c7])).
% 0.38/0.67 cnf(c42,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c41, c6])).
% 0.38/0.67 cnf(c43,plain,greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001))|~environment(skolem0001)|~stable(skolem0001)|~greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(zero,growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c42, c18])).
% 0.38/0.67 cnf(c63,plain,greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001))|~environment(skolem0001)|~stable(skolem0001)|greater(zero,growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c43, c35])).
% 0.38/0.67 cnf(c67,plain,greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001))|~environment(skolem0001)|greater(zero,growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c63, c7])).
% 0.38/0.67 cnf(c68,plain,greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001))|greater(zero,growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c67, c6])).
% 0.38/0.67 cnf(c72,plain,greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001))|~environment(skolem0001)|~stable(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c68, c28])).
% 0.38/0.67 cnf(c76,plain,greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001))|~environment(skolem0001)|~stable(skolem0001),inference(resolution,[status(thm)],[c72, c31])).
% 0.38/0.67 cnf(c80,plain,greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001))|~environment(skolem0001),inference(resolution,[status(thm)],[c76, c7])).
% 0.38/0.67 cnf(c81,plain,greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c80, c6])).
% 0.38/0.67 cnf(c10,negated_conjecture,~greater(X16,appear(efficient_producers,skolem0001))|~greater(zero,growth_rate(first_movers,skolem0002(X16))),inference(split_conjunct,[status(thm)],[c5])).
% 0.38/0.67 cnf(c9,negated_conjecture,~greater(X15,appear(efficient_producers,skolem0001))|greater_or_equal(skolem0002(X15),X15),inference(split_conjunct,[status(thm)],[c5])).
% 0.38/0.67 cnf(c83,plain,greater_or_equal(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001)),inference(resolution,[status(thm)],[c81, c9])).
% 0.38/0.67 cnf(c8,negated_conjecture,~greater(X14,appear(efficient_producers,skolem0001))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(X14)),inference(split_conjunct,[status(thm)],[c5])).
% 0.38/0.67 cnf(c82,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001))),inference(resolution,[status(thm)],[c81, c8])).
% 0.38/0.67 cnf(c29,plain,~environment(X34)|~stable(X34)|~in_environment(X34,X35)|~greater(zero,growth_rate(first_movers,skolem0004(X34,X35)))|~subpopulations(first_movers,efficient_producers,X34,X33)|~greater_or_equal(X33,skolem0005(X34))|greater(zero,growth_rate(first_movers,X33)),inference(split_conjunct,[status(thm)],[c23])).
% 0.38/0.67 cnf(c27,plain,~environment(X31)|~stable(X31)|~in_environment(X31,X32)|greater_or_equal(skolem0004(X31,X32),X32)|~subpopulations(first_movers,efficient_producers,X31,X30)|~greater_or_equal(X30,skolem0005(X31))|greater(zero,growth_rate(first_movers,X30)),inference(split_conjunct,[status(thm)],[c23])).
% 0.38/0.67 cnf(c88,plain,~environment(skolem0001)|~stable(skolem0001)|~in_environment(skolem0001,X38)|greater_or_equal(skolem0004(skolem0001,X38),X38)|~greater_or_equal(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c82, c27])).
% 0.38/0.67 cnf(c89,plain,~environment(skolem0001)|~stable(skolem0001)|~in_environment(skolem0001,X39)|greater_or_equal(skolem0004(skolem0001,X39),X39)|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c88, c83])).
% 0.38/0.67 cnf(c90,plain,~environment(skolem0001)|~stable(skolem0001)|greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c89, c31])).
% 0.38/0.67 cnf(c91,plain,~environment(skolem0001)|greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c90, c7])).
% 0.38/0.67 cnf(c92,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c91, c6])).
% 0.38/0.67 cnf(c93,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|~greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c92, c10])).
% 0.38/0.67 cnf(c94,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001)),inference(resolution,[status(thm)],[c93, c81])).
% 0.38/0.67 cnf(c25,plain,~environment(X28)|~stable(X28)|~in_environment(X28,X29)|subpopulations(first_movers,efficient_producers,X28,skolem0004(X28,X29))|~subpopulations(first_movers,efficient_producers,X28,X27)|~greater_or_equal(X27,skolem0005(X28))|greater(zero,growth_rate(first_movers,X27)),inference(split_conjunct,[status(thm)],[c23])).
% 0.38/0.67 cnf(c87,plain,~environment(skolem0001)|~stable(skolem0001)|~in_environment(skolem0001,X42)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,X42))|~greater_or_equal(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c82, c25])).
% 0.38/0.67 cnf(c95,plain,~environment(skolem0001)|~stable(skolem0001)|~in_environment(skolem0001,X43)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,X43))|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c87, c83])).
% 0.38/0.67 cnf(c96,plain,~environment(skolem0001)|~stable(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c95, c31])).
% 0.38/0.67 cnf(c97,plain,~environment(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c96, c7])).
% 0.38/0.67 cnf(c98,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c97, c6])).
% 0.38/0.67 cnf(c103,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|~greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c98, c10])).
% 0.38/0.67 cnf(c104,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001))),inference(resolution,[status(thm)],[c103, c81])).
% 0.38/0.67 cnf(c105,plain,~environment(skolem0001)|~stable(skolem0001)|~greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(zero,growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c104, c18])).
% 0.38/0.67 cnf(c109,plain,~environment(skolem0001)|~stable(skolem0001)|greater(zero,growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c105, c94])).
% 0.38/0.67 cnf(c110,plain,~environment(skolem0001)|greater(zero,growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c109, c7])).
% 0.38/0.67 cnf(c111,plain,greater(zero,growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c110, c6])).
% 0.38/0.67 cnf(c112,plain,~environment(skolem0001)|~stable(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001))|~subpopulations(first_movers,efficient_producers,skolem0001,X47)|~greater_or_equal(X47,skolem0005(skolem0001))|greater(zero,growth_rate(first_movers,X47)),inference(resolution,[status(thm)],[c111, c29])).
% 0.38/0.67 cnf(c117,plain,~environment(skolem0001)|~stable(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001))|~greater_or_equal(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c112, c82])).
% 0.38/0.67 cnf(c119,plain,~environment(skolem0001)|~stable(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001))|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c117, c83])).
% 0.38/0.67 cnf(c120,plain,~environment(skolem0001)|~stable(skolem0001)|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c119, c31])).
% 0.38/0.67 cnf(c121,plain,~environment(skolem0001)|greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c120, c7])).
% 0.38/0.67 cnf(c122,plain,greater(zero,growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c121, c6])).
% 0.38/0.67 cnf(c123,plain,~greater(skolem0005(skolem0001),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c122, c10])).
% 0.38/0.67 cnf(c124,plain,$false,inference(resolution,[status(thm)],[c123, c81])).
% 0.38/0.67 % SZS output end CNFRefutation
% 0.38/0.67
% 0.38/0.67 % Initial clauses : 14
% 0.38/0.67 % Processed clauses : 72
% 0.38/0.67 % Factors computed : 0
% 0.38/0.67 % Resolvents computed: 95
% 0.38/0.67 % Tautologies deleted: 0
% 0.38/0.67 % Forward subsumed : 21
% 0.38/0.67 % Backward subsumed : 46
% 0.38/0.67 % -------- CPU Time ---------
% 0.38/0.67 % User time : 0.276 s
% 0.38/0.67 % System time : 0.026 s
% 0.38/0.67 % Total time : 0.302 s
%------------------------------------------------------------------------------