%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT030+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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.46s 0.75s
% Output : CNFRefutation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT030+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n006.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 12:18:46 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.41 (re.compile("\."), Token.FullStop),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.41 (re.compile("\("), Token.OpenPar),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.41 (re.compile("\)"), Token.ClosePar),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.41 (re.compile("\["), Token.OpenSquare),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("~\|"), Token.Nor),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("\|"), Token.Or),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.41 (re.compile("\?"), Token.Existential),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.41 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.48 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.48 """
% 0.22/0.48 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.48 """
% 0.32/0.57 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.57 """
% 0.46/0.75 % Version: 1.5
% 0.46/0.75 % SZS status Theorem
% 0.46/0.75 % SZS output start CNFRefutation
% 0.46/0.75 fof(prove_l12,conjecture,(![E]:((environment(E)&stable(E))=>(?[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/sandbox/benchmark/theBenchmark.p', prove_l12)).
% 0.46/0.75 fof(c0,negated_conjecture,(~(![E]:((environment(E)&stable(E))=>(?[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(assume_negation,[status(cth)],[prove_l12])).
% 0.46/0.75 fof(c1,negated_conjecture,(~(![E]:((environment(E)&stable(E))=>(?[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)],[c0])).
% 0.46/0.75 fof(c2,negated_conjecture,(?[E]:((environment(E)&stable(E))&(![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)],[c1])).
% 0.46/0.75 fof(c3,negated_conjecture,(?[X2]:((environment(X2)&stable(X2))&(![X3]:((~in_environment(X2,X3)|greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3)))|(?[X4]:((subpopulations(first_movers,efficient_producers,X2,X4)&greater(X4,X3))&~greater(growth_rate(efficient_producers,X4),growth_rate(first_movers,X4)))))))),inference(variable_rename,[status(thm)],[c2])).
% 0.46/0.75 fof(c5,negated_conjecture,(![X3]:((environment(skolem0001)&stable(skolem0001))&((~in_environment(skolem0001,X3)|greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3)))|((subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(X3))&greater(skolem0002(X3),X3))&~greater(growth_rate(efficient_producers,skolem0002(X3)),growth_rate(first_movers,skolem0002(X3))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((environment(skolem0001)&stable(skolem0001))&(![X3]:((~in_environment(skolem0001,X3)|greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3)))|((subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(X3))&greater(skolem0002(X3),X3))&~greater(growth_rate(efficient_producers,skolem0002(X3)),growth_rate(first_movers,skolem0002(X3))))))),inference(skolemize,[status(esa)],[c3])).])).
% 0.46/0.75 fof(c6,negated_conjecture,(![X3]:((environment(skolem0001)&stable(skolem0001))&((((~in_environment(skolem0001,X3)|greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3)))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(X3)))&((~in_environment(skolem0001,X3)|greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3)))|greater(skolem0002(X3),X3)))&((~in_environment(skolem0001,X3)|greater(growth_rate(efficient_producers,X3),growth_rate(first_movers,X3)))|~greater(growth_rate(efficient_producers,skolem0002(X3)),growth_rate(first_movers,skolem0002(X3))))))),inference(distribute,[status(thm)],[c5])).
% 0.46/0.75 cnf(c7,negated_conjecture,environment(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.75 cnf(c8,negated_conjecture,stable(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.75 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/sandbox/benchmark/theBenchmark.p', l1)).
% 0.46/0.75 fof(c12,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])).
% 0.46/0.75 fof(c13,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),growth_rate(first_movers,X7)))))))),inference(variable_rename,[status(thm)],[c12])).
% 0.46/0.75 fof(c15,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),growth_rate(first_movers,X7))))))),inference(shift_quantors,[status(thm)],[fof(c14,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),growth_rate(first_movers,X7))))))),inference(skolemize,[status(esa)],[c13])).])).
% 0.46/0.75 fof(c16,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),growth_rate(first_movers,X7))))))),inference(distribute,[status(thm)],[c15])).
% 0.46/0.75 cnf(c17,plain,~environment(X13)|~stable(X13)|in_environment(X13,skolem0003(X13)),inference(split_conjunct,[status(thm)],[c16])).
% 0.46/0.75 cnf(c34,plain,~environment(skolem0001)|in_environment(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c17, c8])).
% 0.46/0.75 cnf(c35,plain,in_environment(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c34, c7])).
% 0.46/0.75 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/sandbox/benchmark/theBenchmark.p', mp_earliest_time_growth_rate_exceeds)).
% 0.46/0.75 fof(c19,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])).
% 0.46/0.75 fof(c20,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)],[c19])).
% 0.46/0.75 fof(c21,plain,(![X8]:((~environment(X8)|(![X9]:(~in_environment(X8,X9)|(?[X10]:((subpopulations(first_movers,efficient_producers,X8,X10)&greater_or_equal(X10,X9))&~greater(growth_rate(efficient_producers,X10),growth_rate(first_movers,X10)))))))|(?[X11]:((in_environment(X8,X11)&~greater(growth_rate(efficient_producers,X11),growth_rate(first_movers,X11)))&(![X12]:((~subpopulations(first_movers,efficient_producers,X8,X12)|~greater(X12,X11))|greater(growth_rate(efficient_producers,X12),growth_rate(first_movers,X12)))))))),inference(variable_rename,[status(thm)],[c20])).
% 0.46/0.75 fof(c23,plain,(![X8]:(![X9]:(![X12]:((~environment(X8)|(~in_environment(X8,X9)|((subpopulations(first_movers,efficient_producers,X8,skolem0004(X8,X9))&greater_or_equal(skolem0004(X8,X9),X9))&~greater(growth_rate(efficient_producers,skolem0004(X8,X9)),growth_rate(first_movers,skolem0004(X8,X9))))))|((in_environment(X8,skolem0005(X8))&~greater(growth_rate(efficient_producers,skolem0005(X8)),growth_rate(first_movers,skolem0005(X8))))&((~subpopulations(first_movers,efficient_producers,X8,X12)|~greater(X12,skolem0005(X8)))|greater(growth_rate(efficient_producers,X12),growth_rate(first_movers,X12)))))))),inference(shift_quantors,[status(thm)],[fof(c22,plain,(![X8]:((~environment(X8)|(![X9]:(~in_environment(X8,X9)|((subpopulations(first_movers,efficient_producers,X8,skolem0004(X8,X9))&greater_or_equal(skolem0004(X8,X9),X9))&~greater(growth_rate(efficient_producers,skolem0004(X8,X9)),growth_rate(first_movers,skolem0004(X8,X9)))))))|((in_environment(X8,skolem0005(X8))&~greater(growth_rate(efficient_producers,skolem0005(X8)),growth_rate(first_movers,skolem0005(X8))))&(![X12]:((~subpopulations(first_movers,efficient_producers,X8,X12)|~greater(X12,skolem0005(X8)))|greater(growth_rate(efficient_producers,X12),growth_rate(first_movers,X12))))))),inference(skolemize,[status(esa)],[c21])).])).
% 0.46/0.75 fof(c24,plain,(![X8]:(![X9]:(![X12]:((((((~environment(X8)|(~in_environment(X8,X9)|subpopulations(first_movers,efficient_producers,X8,skolem0004(X8,X9))))|in_environment(X8,skolem0005(X8)))&((~environment(X8)|(~in_environment(X8,X9)|subpopulations(first_movers,efficient_producers,X8,skolem0004(X8,X9))))|~greater(growth_rate(efficient_producers,skolem0005(X8)),growth_rate(first_movers,skolem0005(X8)))))&((~environment(X8)|(~in_environment(X8,X9)|subpopulations(first_movers,efficient_producers,X8,skolem0004(X8,X9))))|((~subpopulations(first_movers,efficient_producers,X8,X12)|~greater(X12,skolem0005(X8)))|greater(growth_rate(efficient_producers,X12),growth_rate(first_movers,X12)))))&((((~environment(X8)|(~in_environment(X8,X9)|greater_or_equal(skolem0004(X8,X9),X9)))|in_environment(X8,skolem0005(X8)))&((~environment(X8)|(~in_environment(X8,X9)|greater_or_equal(skolem0004(X8,X9),X9)))|~greater(growth_rate(efficient_producers,skolem0005(X8)),growth_rate(first_movers,skolem0005(X8)))))&((~environment(X8)|(~in_environment(X8,X9)|greater_or_equal(skolem0004(X8,X9),X9)))|((~subpopulations(first_movers,efficient_producers,X8,X12)|~greater(X12,skolem0005(X8)))|greater(growth_rate(efficient_producers,X12),growth_rate(first_movers,X12))))))&((((~environment(X8)|(~in_environment(X8,X9)|~greater(growth_rate(efficient_producers,skolem0004(X8,X9)),growth_rate(first_movers,skolem0004(X8,X9)))))|in_environment(X8,skolem0005(X8)))&((~environment(X8)|(~in_environment(X8,X9)|~greater(growth_rate(efficient_producers,skolem0004(X8,X9)),growth_rate(first_movers,skolem0004(X8,X9)))))|~greater(growth_rate(efficient_producers,skolem0005(X8)),growth_rate(first_movers,skolem0005(X8)))))&((~environment(X8)|(~in_environment(X8,X9)|~greater(growth_rate(efficient_producers,skolem0004(X8,X9)),growth_rate(first_movers,skolem0004(X8,X9)))))|((~subpopulations(first_movers,efficient_producers,X8,X12)|~greater(X12,skolem0005(X8)))|greater(growth_rate(efficient_producers,X12),growth_rate(first_movers,X12))))))))),inference(distribute,[status(thm)],[c23])).
% 0.46/0.75 cnf(c32,plain,~environment(X33)|~in_environment(X33,X32)|~greater(growth_rate(efficient_producers,skolem0004(X33,X32)),growth_rate(first_movers,skolem0004(X33,X32)))|~greater(growth_rate(efficient_producers,skolem0005(X33)),growth_rate(first_movers,skolem0005(X33))),inference(split_conjunct,[status(thm)],[c24])).
% 0.46/0.75 cnf(c29,plain,~environment(X22)|~in_environment(X22,X21)|greater_or_equal(skolem0004(X22,X21),X21)|~greater(growth_rate(efficient_producers,skolem0005(X22)),growth_rate(first_movers,skolem0005(X22))),inference(split_conjunct,[status(thm)],[c24])).
% 0.46/0.75 cnf(c31,plain,~environment(X24)|~in_environment(X24,X23)|~greater(growth_rate(efficient_producers,skolem0004(X24,X23)),growth_rate(first_movers,skolem0004(X24,X23)))|in_environment(X24,skolem0005(X24)),inference(split_conjunct,[status(thm)],[c24])).
% 0.46/0.75 cnf(c28,plain,~environment(X16)|~in_environment(X16,X15)|greater_or_equal(skolem0004(X16,X15),X15)|in_environment(X16,skolem0005(X16)),inference(split_conjunct,[status(thm)],[c24])).
% 0.46/0.75 cnf(c37,plain,~environment(skolem0001)|greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c28, c35])).
% 0.46/0.75 cnf(c40,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c37, c7])).
% 0.46/0.75 cnf(c25,plain,~environment(X19)|~in_environment(X19,X18)|subpopulations(first_movers,efficient_producers,X19,skolem0004(X19,X18))|in_environment(X19,skolem0005(X19)),inference(split_conjunct,[status(thm)],[c24])).
% 0.46/0.75 cnf(c39,plain,~environment(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c25, c35])).
% 0.46/0.75 cnf(c45,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c39, c7])).
% 0.46/0.75 cnf(c18,plain,~environment(X26)|~stable(X26)|~subpopulations(first_movers,efficient_producers,X26,X25)|~greater_or_equal(X25,skolem0003(X26))|greater(growth_rate(efficient_producers,X25),growth_rate(first_movers,X25)),inference(split_conjunct,[status(thm)],[c16])).
% 0.46/0.75 cnf(c50,plain,~environment(skolem0001)|~stable(skolem0001)|~greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001))))|in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c18, c45])).
% 0.46/0.75 cnf(c92,plain,~environment(skolem0001)|~stable(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001))))|in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c50, c40])).
% 0.46/0.75 cnf(c93,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001))))|in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c92, c8])).
% 0.46/0.75 cnf(c94,plain,greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001))))|in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c93, c7])).
% 0.46/0.75 cnf(c97,plain,in_environment(skolem0001,skolem0005(skolem0001))|~environment(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c94, c31])).
% 0.46/0.75 cnf(c103,plain,in_environment(skolem0001,skolem0005(skolem0001))|~environment(skolem0001),inference(resolution,[status(thm)],[c97, c35])).
% 0.46/0.75 cnf(c104,plain,in_environment(skolem0001,skolem0005(skolem0001)),inference(resolution,[status(thm)],[c103, c7])).
% 0.46/0.75 cnf(c11,negated_conjecture,~in_environment(skolem0001,X20)|greater(growth_rate(efficient_producers,X20),growth_rate(first_movers,X20))|~greater(growth_rate(efficient_producers,skolem0002(X20)),growth_rate(first_movers,skolem0002(X20))),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.75 cnf(c10,negated_conjecture,~in_environment(skolem0001,X17)|greater(growth_rate(efficient_producers,X17),growth_rate(first_movers,X17))|greater(skolem0002(X17),X17),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.75 cnf(c108,plain,greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001)),inference(resolution,[status(thm)],[c104, c10])).
% 0.46/0.75 cnf(c43,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001)),inference(resolution,[status(thm)],[c40, c10])).
% 0.46/0.75 cnf(c57,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|~in_environment(skolem0001,X37)|greater_or_equal(skolem0004(skolem0001,X37),X37),inference(resolution,[status(thm)],[c43, c29])).
% 0.46/0.75 cnf(c58,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001),inference(resolution,[status(thm)],[c57, c35])).
% 0.46/0.75 cnf(c61,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001)),inference(resolution,[status(thm)],[c58, c7])).
% 0.46/0.75 cnf(c26,plain,~environment(X28)|~in_environment(X28,X27)|subpopulations(first_movers,efficient_producers,X28,skolem0004(X28,X27))|~greater(growth_rate(efficient_producers,skolem0005(X28)),growth_rate(first_movers,skolem0005(X28))),inference(split_conjunct,[status(thm)],[c24])).
% 0.46/0.75 cnf(c110,plain,greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|~in_environment(skolem0001,X47)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,X47)),inference(resolution,[status(thm)],[c108, c26])).
% 0.46/0.75 cnf(c126,plain,greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001))),inference(resolution,[status(thm)],[c110, c35])).
% 0.46/0.75 cnf(c128,plain,greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001))),inference(resolution,[status(thm)],[c126, c7])).
% 0.46/0.75 cnf(c131,plain,greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|~stable(skolem0001)|~greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c128, c18])).
% 0.46/0.75 cnf(c162,plain,greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|~stable(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c131, c61])).
% 0.46/0.75 cnf(c164,plain,greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c162, c8])).
% 0.46/0.75 cnf(c165,plain,greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c164, c7])).
% 0.46/0.75 cnf(c168,plain,greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001))|~greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c165, c32])).
% 0.46/0.75 cnf(c171,plain,greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c168, c108])).
% 0.46/0.75 cnf(c173,plain,greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|~environment(skolem0001),inference(resolution,[status(thm)],[c171, c35])).
% 0.46/0.75 cnf(c174,plain,greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001)),inference(resolution,[status(thm)],[c173, c7])).
% 0.46/0.75 cnf(c30,plain,~environment(X30)|~in_environment(X30,X29)|greater_or_equal(skolem0004(X30,X29),X29)|~subpopulations(first_movers,efficient_producers,X30,X31)|~greater(X31,skolem0005(X30))|greater(growth_rate(efficient_producers,X31),growth_rate(first_movers,X31)),inference(split_conjunct,[status(thm)],[c24])).
% 0.46/0.75 cnf(c9,negated_conjecture,~in_environment(skolem0001,X14)|greater(growth_rate(efficient_producers,X14),growth_rate(first_movers,X14))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(X14)),inference(split_conjunct,[status(thm)],[c6])).
% 0.46/0.75 cnf(c109,plain,greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001))),inference(resolution,[status(thm)],[c104, c9])).
% 0.46/0.75 cnf(c42,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001)))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001))),inference(resolution,[status(thm)],[c40, c9])).
% 0.46/0.75 cnf(c63,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001)))|~environment(skolem0001)|~in_environment(skolem0001,X41)|greater_or_equal(skolem0004(skolem0001,X41),X41),inference(resolution,[status(thm)],[c42, c29])).
% 0.46/0.75 cnf(c67,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001)))|~environment(skolem0001),inference(resolution,[status(thm)],[c63, c35])).
% 0.46/0.75 cnf(c78,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001))),inference(resolution,[status(thm)],[c67, c7])).
% 0.46/0.75 cnf(c115,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001)))|~environment(skolem0001)|~in_environment(skolem0001,X49)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,X49)),inference(resolution,[status(thm)],[c109, c26])).
% 0.46/0.75 cnf(c136,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001)))|~environment(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001))),inference(resolution,[status(thm)],[c115, c35])).
% 0.46/0.75 cnf(c138,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001)))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001))),inference(resolution,[status(thm)],[c136, c7])).
% 0.46/0.75 cnf(c144,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001)))|~environment(skolem0001)|~stable(skolem0001)|~greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c138, c18])).
% 0.46/0.75 cnf(c177,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001)))|~environment(skolem0001)|~stable(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c144, c78])).
% 0.46/0.75 cnf(c178,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001)))|~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c177, c8])).
% 0.46/0.75 cnf(c179,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001)))|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c178, c7])).
% 0.46/0.75 cnf(c183,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001)))|~environment(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001))|~greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c179, c32])).
% 0.46/0.75 cnf(c186,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001)))|~environment(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c183, c109])).
% 0.46/0.75 cnf(c187,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001)))|~environment(skolem0001),inference(resolution,[status(thm)],[c186, c35])).
% 0.46/0.75 cnf(c188,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0002(skolem0005(skolem0001))),inference(resolution,[status(thm)],[c187, c7])).
% 0.46/0.75 cnf(c189,plain,~environment(skolem0001)|~in_environment(skolem0001,X62)|greater_or_equal(skolem0004(skolem0001,X62),X62)|~greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|greater(growth_rate(efficient_producers,skolem0002(skolem0005(skolem0001))),growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c188, c30])).
% 0.46/0.75 cnf(c192,plain,~environment(skolem0001)|~in_environment(skolem0001,X63)|greater_or_equal(skolem0004(skolem0001,X63),X63)|greater(growth_rate(efficient_producers,skolem0002(skolem0005(skolem0001))),growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c189, c174])).
% 0.46/0.75 cnf(c193,plain,~environment(skolem0001)|greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(growth_rate(efficient_producers,skolem0002(skolem0005(skolem0001))),growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c192, c35])).
% 0.46/0.75 cnf(c195,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(growth_rate(efficient_producers,skolem0002(skolem0005(skolem0001))),growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c193, c7])).
% 0.46/0.75 cnf(c196,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|~in_environment(skolem0001,skolem0005(skolem0001))|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c195, c11])).
% 0.46/0.75 cnf(c199,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c196, c104])).
% 0.46/0.75 cnf(c201,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|~environment(skolem0001)|~in_environment(skolem0001,X66)|greater_or_equal(skolem0004(skolem0001,X66),X66),inference(resolution,[status(thm)],[c199, c29])).
% 0.46/0.75 cnf(c203,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|~environment(skolem0001),inference(resolution,[status(thm)],[c201, c35])).
% 0.46/0.75 cnf(c205,plain,greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001)),inference(resolution,[status(thm)],[c203, c7])).
% 0.46/0.75 cnf(c27,plain,~environment(X35)|~in_environment(X35,X34)|subpopulations(first_movers,efficient_producers,X35,skolem0004(X35,X34))|~subpopulations(first_movers,efficient_producers,X35,X36)|~greater(X36,skolem0005(X35))|greater(growth_rate(efficient_producers,X36),growth_rate(first_movers,X36)),inference(split_conjunct,[status(thm)],[c24])).
% 0.46/0.75 cnf(c190,plain,~environment(skolem0001)|~in_environment(skolem0001,X72)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,X72))|~greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|greater(growth_rate(efficient_producers,skolem0002(skolem0005(skolem0001))),growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c188, c27])).
% 0.46/0.75 cnf(c212,plain,~environment(skolem0001)|~in_environment(skolem0001,X73)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,X73))|greater(growth_rate(efficient_producers,skolem0002(skolem0005(skolem0001))),growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c190, c174])).
% 0.46/0.75 cnf(c213,plain,~environment(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|greater(growth_rate(efficient_producers,skolem0002(skolem0005(skolem0001))),growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c212, c35])).
% 0.46/0.75 cnf(c215,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|greater(growth_rate(efficient_producers,skolem0002(skolem0005(skolem0001))),growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c213, c7])).
% 0.46/0.75 cnf(c219,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|~in_environment(skolem0001,skolem0005(skolem0001))|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c215, c11])).
% 0.46/0.75 cnf(c225,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c219, c104])).
% 0.46/0.75 cnf(c229,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|~environment(skolem0001)|~in_environment(skolem0001,X77)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,X77)),inference(resolution,[status(thm)],[c225, c26])).
% 0.46/0.75 cnf(c233,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001)))|~environment(skolem0001),inference(resolution,[status(thm)],[c229, c35])).
% 0.46/0.75 cnf(c235,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0004(skolem0001,skolem0003(skolem0001))),inference(resolution,[status(thm)],[c233, c7])).
% 0.46/0.75 cnf(c238,plain,~environment(skolem0001)|~stable(skolem0001)|~greater_or_equal(skolem0004(skolem0001,skolem0003(skolem0001)),skolem0003(skolem0001))|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c235, c18])).
% 0.46/0.75 cnf(c253,plain,~environment(skolem0001)|~stable(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c238, c205])).
% 0.46/0.75 cnf(c254,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c253, c8])).
% 0.46/0.75 cnf(c255,plain,greater(growth_rate(efficient_producers,skolem0004(skolem0001,skolem0003(skolem0001))),growth_rate(first_movers,skolem0004(skolem0001,skolem0003(skolem0001)))),inference(resolution,[status(thm)],[c254, c7])).
% 0.46/0.75 cnf(c256,plain,~environment(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001))|~greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c255, c32])).
% 0.46/0.75 cnf(c33,plain,~environment(X39)|~in_environment(X39,X38)|~greater(growth_rate(efficient_producers,skolem0004(X39,X38)),growth_rate(first_movers,skolem0004(X39,X38)))|~subpopulations(first_movers,efficient_producers,X39,X40)|~greater(X40,skolem0005(X39))|greater(growth_rate(efficient_producers,X40),growth_rate(first_movers,X40)),inference(split_conjunct,[status(thm)],[c24])).
% 0.46/0.75 cnf(c257,plain,~environment(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001))|~subpopulations(first_movers,efficient_producers,skolem0001,X82)|~greater(X82,skolem0005(skolem0001))|greater(growth_rate(efficient_producers,X82),growth_rate(first_movers,X82)),inference(resolution,[status(thm)],[c255, c33])).
% 0.46/0.75 cnf(c261,plain,~environment(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001))|~greater(skolem0002(skolem0005(skolem0001)),skolem0005(skolem0001))|greater(growth_rate(efficient_producers,skolem0002(skolem0005(skolem0001))),growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c257, c188])).
% 0.46/0.75 cnf(c263,plain,~environment(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001))|greater(growth_rate(efficient_producers,skolem0002(skolem0005(skolem0001))),growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c261, c174])).
% 0.46/0.75 cnf(c264,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0002(skolem0005(skolem0001))),growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c263, c35])).
% 0.46/0.75 cnf(c265,plain,greater(growth_rate(efficient_producers,skolem0002(skolem0005(skolem0001))),growth_rate(first_movers,skolem0002(skolem0005(skolem0001)))),inference(resolution,[status(thm)],[c264, c7])).
% 0.46/0.75 cnf(c266,plain,~in_environment(skolem0001,skolem0005(skolem0001))|greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c265, c11])).
% 0.46/0.75 cnf(c267,plain,greater(growth_rate(efficient_producers,skolem0005(skolem0001)),growth_rate(first_movers,skolem0005(skolem0001))),inference(resolution,[status(thm)],[c266, c104])).
% 0.46/0.75 cnf(c268,plain,~environment(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c267, c256])).
% 0.46/0.75 cnf(c271,plain,~environment(skolem0001),inference(resolution,[status(thm)],[c268, c35])).
% 0.46/0.75 cnf(c272,plain,$false,inference(resolution,[status(thm)],[c271, c7])).
% 0.46/0.75 % SZS output end CNFRefutation
% 0.46/0.75
% 0.46/0.75 % Initial clauses : 16
% 0.46/0.75 % Processed clauses : 136
% 0.46/0.75 % Factors computed : 0
% 0.46/0.75 % Resolvents computed: 239
% 0.46/0.75 % Tautologies deleted: 0
% 0.46/0.75 % Forward subsumed : 64
% 0.46/0.75 % Backward subsumed : 106
% 0.46/0.75 % -------- CPU Time ---------
% 0.46/0.75 % User time : 0.379 s
% 0.46/0.75 % System time : 0.022 s
% 0.46/0.75 % Total time : 0.401 s
%------------------------------------------------------------------------------