%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT027+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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 2.81s 3.14s
% Output : CNFRefutation 2.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT027+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 7 12:15:22 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.43 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.02/0.43 (re.compile("\."), Token.FullStop),
% 0.02/0.43 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.02/0.43 (re.compile("\("), Token.OpenPar),
% 0.02/0.43 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.02/0.43 (re.compile("\)"), Token.ClosePar),
% 0.02/0.43 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.02/0.43 (re.compile("\["), Token.OpenSquare),
% 0.02/0.43 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.02/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.02/0.43 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.02/0.43 (re.compile("~\|"), Token.Nor),
% 0.02/0.43 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.02/0.43 (re.compile("\|"), Token.Or),
% 0.02/0.43 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.02/0.43 (re.compile("\?"), Token.Existential),
% 0.02/0.43 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.02/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.02/0.43 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.02/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.50 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.22/0.50 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.32/0.60 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.60 """
% 2.81/3.14 % Version: 1.5
% 2.81/3.14 % SZS status Theorem
% 2.81/3.14 % SZS output start CNFRefutation
% 2.81/3.14 fof(prove_l9,conjecture,(![E]:((environment(E)&stable(E))=>(?[To]:(greater(To,appear(efficient_producers,E))&contracts_from(To,first_movers))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l9)).
% 2.81/3.14 fof(c10,negated_conjecture,(~(![E]:((environment(E)&stable(E))=>(?[To]:(greater(To,appear(efficient_producers,E))&contracts_from(To,first_movers)))))),inference(assume_negation,[status(cth)],[prove_l9])).
% 2.81/3.14 fof(c11,negated_conjecture,(?[E]:((environment(E)&stable(E))&(![To]:(~greater(To,appear(efficient_producers,E))|~contracts_from(To,first_movers))))),inference(fof_nnf,[status(thm)],[c10])).
% 2.81/3.14 fof(c12,negated_conjecture,(?[X2]:((environment(X2)&stable(X2))&(![X3]:(~greater(X3,appear(efficient_producers,X2))|~contracts_from(X3,first_movers))))),inference(variable_rename,[status(thm)],[c11])).
% 2.81/3.14 fof(c14,negated_conjecture,(![X3]:((environment(skolem0001)&stable(skolem0001))&(~greater(X3,appear(efficient_producers,skolem0001))|~contracts_from(X3,first_movers)))),inference(shift_quantors,[status(thm)],[fof(c13,negated_conjecture,((environment(skolem0001)&stable(skolem0001))&(![X3]:(~greater(X3,appear(efficient_producers,skolem0001))|~contracts_from(X3,first_movers)))),inference(skolemize,[status(esa)],[c12])).])).
% 2.81/3.14 cnf(c17,negated_conjecture,~greater(X61,appear(efficient_producers,skolem0001))|~contracts_from(X61,first_movers),inference(split_conjunct,[status(thm)],[c14])).
% 2.81/3.14 cnf(c15,negated_conjecture,environment(skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 2.81/3.14 cnf(c16,negated_conjecture,stable(skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 2.81/3.14 fof(l10,plain,(![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', l10)).
% 2.81/3.14 fof(c18,plain,(![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)],[l10])).
% 2.81/3.14 fof(c19,plain,(![X4]:((~environment(X4)|~stable(X4))|(?[X5]:(greater(X5,appear(efficient_producers,X4))&(![X6]:((~subpopulations(first_movers,efficient_producers,X4,X6)|~greater_or_equal(X6,X5))|greater(zero,growth_rate(first_movers,X6)))))))),inference(variable_rename,[status(thm)],[c18])).
% 2.81/3.14 fof(c21,plain,(![X4]:(![X6]:((~environment(X4)|~stable(X4))|(greater(skolem0002(X4),appear(efficient_producers,X4))&((~subpopulations(first_movers,efficient_producers,X4,X6)|~greater_or_equal(X6,skolem0002(X4)))|greater(zero,growth_rate(first_movers,X6))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,(![X4]:((~environment(X4)|~stable(X4))|(greater(skolem0002(X4),appear(efficient_producers,X4))&(![X6]:((~subpopulations(first_movers,efficient_producers,X4,X6)|~greater_or_equal(X6,skolem0002(X4)))|greater(zero,growth_rate(first_movers,X6))))))),inference(skolemize,[status(esa)],[c19])).])).
% 2.81/3.14 fof(c22,plain,(![X4]:(![X6]:(((~environment(X4)|~stable(X4))|greater(skolem0002(X4),appear(efficient_producers,X4)))&((~environment(X4)|~stable(X4))|((~subpopulations(first_movers,efficient_producers,X4,X6)|~greater_or_equal(X6,skolem0002(X4)))|greater(zero,growth_rate(first_movers,X6))))))),inference(distribute,[status(thm)],[c21])).
% 2.81/3.14 cnf(c23,plain,~environment(X115)|~stable(X115)|greater(skolem0002(X115),appear(efficient_producers,X115)),inference(split_conjunct,[status(thm)],[c22])).
% 2.81/3.14 cnf(c82,plain,~environment(skolem0001)|greater(skolem0002(skolem0001),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c23, c16])).
% 2.81/3.14 cnf(c83,plain,greater(skolem0002(skolem0001),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c82, c15])).
% 2.81/3.14 cnf(c86,plain,~contracts_from(skolem0002(skolem0001),first_movers),inference(resolution,[status(thm)],[c83, c17])).
% 2.81/3.14 fof(mp_EP_in_stable_environments,axiom,(![E]:((environment(E)&stable(E))=>in_environment(E,appear(efficient_producers,E)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_EP_in_stable_environments)).
% 2.81/3.14 fof(c39,plain,(![E]:((~environment(E)|~stable(E))|in_environment(E,appear(efficient_producers,E)))),inference(fof_nnf,[status(thm)],[mp_EP_in_stable_environments])).
% 2.81/3.14 fof(c40,plain,(![X16]:((~environment(X16)|~stable(X16))|in_environment(X16,appear(efficient_producers,X16)))),inference(variable_rename,[status(thm)],[c39])).
% 2.81/3.14 cnf(c41,plain,~environment(X62)|~stable(X62)|in_environment(X62,appear(efficient_producers,X62)),inference(split_conjunct,[status(thm)],[c40])).
% 2.81/3.14 cnf(c67,plain,~environment(skolem0001)|in_environment(skolem0001,appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c41, c16])).
% 2.81/3.14 cnf(c74,plain,in_environment(skolem0001,appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c67, c15])).
% 2.81/3.14 fof(mp_long_stable_environments,axiom,(![E]:(![T1]:(![T2]:((((environment(E)&stable(E))&in_environment(E,T1))&greater(T2,T1))=>in_environment(E,T2))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_long_stable_environments)).
% 2.81/3.14 fof(c42,plain,(![E]:(![T1]:(![T2]:((((~environment(E)|~stable(E))|~in_environment(E,T1))|~greater(T2,T1))|in_environment(E,T2))))),inference(fof_nnf,[status(thm)],[mp_long_stable_environments])).
% 2.81/3.14 fof(c43,plain,(![X17]:(![X18]:(![X19]:((((~environment(X17)|~stable(X17))|~in_environment(X17,X18))|~greater(X19,X18))|in_environment(X17,X19))))),inference(variable_rename,[status(thm)],[c42])).
% 2.81/3.14 cnf(c44,plain,~environment(X128)|~stable(X128)|~in_environment(X128,X129)|~greater(X127,X129)|in_environment(X128,X127),inference(split_conjunct,[status(thm)],[c43])).
% 2.81/3.14 cnf(c90,plain,~environment(X145)|~stable(X145)|~in_environment(X145,appear(efficient_producers,skolem0001))|in_environment(X145,skolem0002(skolem0001)),inference(resolution,[status(thm)],[c44, c83])).
% 2.81/3.14 cnf(c100,plain,~environment(skolem0001)|~stable(skolem0001)|in_environment(skolem0001,skolem0002(skolem0001)),inference(resolution,[status(thm)],[c90, c74])).
% 2.81/3.14 cnf(c101,plain,~environment(skolem0001)|in_environment(skolem0001,skolem0002(skolem0001)),inference(resolution,[status(thm)],[c100, c16])).
% 2.81/3.14 cnf(c102,plain,in_environment(skolem0001,skolem0002(skolem0001)),inference(resolution,[status(thm)],[c101, c15])).
% 2.81/3.14 fof(mp_contracts_from,axiom,(![E]:(![To]:((((environment(E)&stable(E))&in_environment(E,To))&(![T]:((greater(cardinality_at_time(first_movers,T),zero)&greater_or_equal(T,To))=>greater(zero,growth_rate(first_movers,T)))))=>contracts_from(To,first_movers)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_contracts_from)).
% 2.81/3.14 fof(c48,plain,(![E]:(![To]:((((~environment(E)|~stable(E))|~in_environment(E,To))|(?[T]:((greater(cardinality_at_time(first_movers,T),zero)&greater_or_equal(T,To))&~greater(zero,growth_rate(first_movers,T)))))|contracts_from(To,first_movers)))),inference(fof_nnf,[status(thm)],[mp_contracts_from])).
% 2.81/3.14 fof(c49,plain,(![X22]:(![X23]:((((~environment(X22)|~stable(X22))|~in_environment(X22,X23))|(?[X24]:((greater(cardinality_at_time(first_movers,X24),zero)&greater_or_equal(X24,X23))&~greater(zero,growth_rate(first_movers,X24)))))|contracts_from(X23,first_movers)))),inference(variable_rename,[status(thm)],[c48])).
% 2.81/3.14 fof(c50,plain,(![X22]:(![X23]:((((~environment(X22)|~stable(X22))|~in_environment(X22,X23))|((greater(cardinality_at_time(first_movers,skolem0003(X22,X23)),zero)&greater_or_equal(skolem0003(X22,X23),X23))&~greater(zero,growth_rate(first_movers,skolem0003(X22,X23)))))|contracts_from(X23,first_movers)))),inference(skolemize,[status(esa)],[c49])).
% 2.81/3.14 fof(c51,plain,(![X22]:(![X23]:((((((~environment(X22)|~stable(X22))|~in_environment(X22,X23))|greater(cardinality_at_time(first_movers,skolem0003(X22,X23)),zero))|contracts_from(X23,first_movers))&((((~environment(X22)|~stable(X22))|~in_environment(X22,X23))|greater_or_equal(skolem0003(X22,X23),X23))|contracts_from(X23,first_movers)))&((((~environment(X22)|~stable(X22))|~in_environment(X22,X23))|~greater(zero,growth_rate(first_movers,skolem0003(X22,X23))))|contracts_from(X23,first_movers))))),inference(distribute,[status(thm)],[c50])).
% 2.81/3.14 cnf(c54,plain,~environment(X153)|~stable(X153)|~in_environment(X153,X152)|~greater(zero,growth_rate(first_movers,skolem0003(X153,X152)))|contracts_from(X152,first_movers),inference(split_conjunct,[status(thm)],[c51])).
% 2.81/3.14 cnf(c53,plain,~environment(X144)|~stable(X144)|~in_environment(X144,X143)|greater_or_equal(skolem0003(X144,X143),X143)|contracts_from(X143,first_movers),inference(split_conjunct,[status(thm)],[c51])).
% 2.81/3.14 cnf(c103,plain,~environment(skolem0001)|~stable(skolem0001)|greater_or_equal(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|contracts_from(skolem0002(skolem0001),first_movers),inference(resolution,[status(thm)],[c102, c53])).
% 2.81/3.14 cnf(c133,plain,~environment(skolem0001)|greater_or_equal(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|contracts_from(skolem0002(skolem0001),first_movers),inference(resolution,[status(thm)],[c103, c16])).
% 2.81/3.14 cnf(c138,plain,greater_or_equal(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|contracts_from(skolem0002(skolem0001),first_movers),inference(resolution,[status(thm)],[c133, c15])).
% 2.81/3.14 cnf(c142,plain,greater_or_equal(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001)),inference(resolution,[status(thm)],[c138, c86])).
% 2.81/3.14 cnf(c24,plain,~environment(X125)|~stable(X125)|~subpopulations(first_movers,efficient_producers,X125,X126)|~greater_or_equal(X126,skolem0002(X125))|greater(zero,growth_rate(first_movers,X126)),inference(split_conjunct,[status(thm)],[c22])).
% 2.81/3.14 cnf(reflexivity,axiom,X25=X25,theory(equality)).
% 2.81/3.14 cnf(c7,axiom,X102!=X99|X101!=X100|~greater(X102,X101)|greater(X99,X100),theory(equality)).
% 2.81/3.14 cnf(c84,plain,skolem0002(skolem0001)!=X133|appear(efficient_producers,skolem0001)!=X134|greater(X133,X134),inference(resolution,[status(thm)],[c83, c7])).
% 2.81/3.14 cnf(c93,plain,skolem0002(skolem0001)!=X137|greater(X137,appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c84, reflexivity])).
% 2.81/3.14 fof(mp_greater_transitivity,axiom,(![X]:(![Y]:(![Z]:((greater(X,Y)&greater(Y,Z))=>greater(X,Z))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_greater_transitivity)).
% 2.81/3.14 fof(c36,plain,(![X]:(![Y]:(![Z]:((~greater(X,Y)|~greater(Y,Z))|greater(X,Z))))),inference(fof_nnf,[status(thm)],[mp_greater_transitivity])).
% 2.81/3.14 fof(c37,plain,(![X13]:(![X14]:(![X15]:((~greater(X13,X14)|~greater(X14,X15))|greater(X13,X15))))),inference(variable_rename,[status(thm)],[c36])).
% 2.81/3.14 cnf(c38,plain,~greater(X59,X58)|~greater(X58,X57)|greater(X59,X57),inference(split_conjunct,[status(thm)],[c37])).
% 2.81/3.14 cnf(c87,plain,~greater(X124,skolem0002(skolem0001))|greater(X124,appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c83, c38])).
% 2.81/3.14 cnf(symmetry,axiom,X27!=X26|X26=X27,theory(equality)).
% 2.81/3.14 fof(mp_greater_or_equal,axiom,(![X]:(![Y]:(greater_or_equal(X,Y)<=>(greater(X,Y)|X=Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_greater_or_equal)).
% 2.81/3.14 fof(c28,plain,(![X]:(![Y]:((~greater_or_equal(X,Y)|(greater(X,Y)|X=Y))&((~greater(X,Y)&X!=Y)|greater_or_equal(X,Y))))),inference(fof_nnf,[status(thm)],[mp_greater_or_equal])).
% 2.81/3.14 fof(c29,plain,((![X]:(![Y]:(~greater_or_equal(X,Y)|(greater(X,Y)|X=Y))))&(![X]:(![Y]:((~greater(X,Y)&X!=Y)|greater_or_equal(X,Y))))),inference(shift_quantors,[status(thm)],[c28])).
% 2.81/3.14 fof(c31,plain,(![X9]:(![X10]:(![X11]:(![X12]:((~greater_or_equal(X9,X10)|(greater(X9,X10)|X9=X10))&((~greater(X11,X12)&X11!=X12)|greater_or_equal(X11,X12))))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X9]:(![X10]:(~greater_or_equal(X9,X10)|(greater(X9,X10)|X9=X10))))&(![X11]:(![X12]:((~greater(X11,X12)&X11!=X12)|greater_or_equal(X11,X12))))),inference(variable_rename,[status(thm)],[c29])).])).
% 2.81/3.14 fof(c32,plain,(![X9]:(![X10]:(![X11]:(![X12]:((~greater_or_equal(X9,X10)|(greater(X9,X10)|X9=X10))&((~greater(X11,X12)|greater_or_equal(X11,X12))&(X11!=X12|greater_or_equal(X11,X12)))))))),inference(distribute,[status(thm)],[c31])).
% 2.81/3.14 cnf(c33,plain,~greater_or_equal(X50,X51)|greater(X50,X51)|X50=X51,inference(split_conjunct,[status(thm)],[c32])).
% 2.81/3.14 cnf(c145,plain,greater(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0003(skolem0001,skolem0002(skolem0001))=skolem0002(skolem0001),inference(resolution,[status(thm)],[c142, c33])).
% 2.81/3.14 cnf(c185,plain,greater(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0002(skolem0001)=skolem0003(skolem0001,skolem0002(skolem0001)),inference(resolution,[status(thm)],[c145, symmetry])).
% 2.81/3.14 cnf(c201,plain,skolem0002(skolem0001)=skolem0003(skolem0001,skolem0002(skolem0001))|greater(skolem0003(skolem0001,skolem0002(skolem0001)),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c185, c87])).
% 2.81/3.14 cnf(c263,plain,greater(skolem0003(skolem0001,skolem0002(skolem0001)),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c201, c93])).
% 2.81/3.14 cnf(c287,plain,~environment(X201)|~stable(X201)|~in_environment(X201,appear(efficient_producers,skolem0001))|in_environment(X201,skolem0003(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c263, c44])).
% 2.81/3.14 cnf(c301,plain,~environment(skolem0001)|~stable(skolem0001)|in_environment(skolem0001,skolem0003(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c287, c74])).
% 2.81/3.14 cnf(c302,plain,~environment(skolem0001)|in_environment(skolem0001,skolem0003(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c301, c16])).
% 2.81/3.14 cnf(c303,plain,in_environment(skolem0001,skolem0003(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c302, c15])).
% 2.81/3.14 cnf(c52,plain,~environment(X147)|~stable(X147)|~in_environment(X147,X146)|greater(cardinality_at_time(first_movers,skolem0003(X147,X146)),zero)|contracts_from(X146,first_movers),inference(split_conjunct,[status(thm)],[c51])).
% 2.81/3.14 cnf(c105,plain,~environment(skolem0001)|~stable(skolem0001)|greater(cardinality_at_time(first_movers,skolem0003(skolem0001,skolem0002(skolem0001))),zero)|contracts_from(skolem0002(skolem0001),first_movers),inference(resolution,[status(thm)],[c52, c102])).
% 2.81/3.14 cnf(c137,plain,~environment(skolem0001)|greater(cardinality_at_time(first_movers,skolem0003(skolem0001,skolem0002(skolem0001))),zero)|contracts_from(skolem0002(skolem0001),first_movers),inference(resolution,[status(thm)],[c105, c16])).
% 2.81/3.14 cnf(c148,plain,greater(cardinality_at_time(first_movers,skolem0003(skolem0001,skolem0002(skolem0001))),zero)|contracts_from(skolem0002(skolem0001),first_movers),inference(resolution,[status(thm)],[c137, c15])).
% 2.81/3.14 cnf(c154,plain,greater(cardinality_at_time(first_movers,skolem0003(skolem0001,skolem0002(skolem0001))),zero),inference(resolution,[status(thm)],[c148, c86])).
% 2.81/3.14 fof(mp_non_empty_fm_and_ep,axiom,(![E]:(![T]:((((environment(E)&in_environment(E,T))&greater(cardinality_at_time(first_movers,T),zero))&greater(cardinality_at_time(efficient_producers,T),zero))=>subpopulations(first_movers,efficient_producers,E,T)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_non_empty_fm_and_ep)).
% 2.81/3.14 fof(c45,plain,(![E]:(![T]:((((~environment(E)|~in_environment(E,T))|~greater(cardinality_at_time(first_movers,T),zero))|~greater(cardinality_at_time(efficient_producers,T),zero))|subpopulations(first_movers,efficient_producers,E,T)))),inference(fof_nnf,[status(thm)],[mp_non_empty_fm_and_ep])).
% 2.81/3.14 fof(c46,plain,(![X20]:(![X21]:((((~environment(X20)|~in_environment(X20,X21))|~greater(cardinality_at_time(first_movers,X21),zero))|~greater(cardinality_at_time(efficient_producers,X21),zero))|subpopulations(first_movers,efficient_producers,X20,X21)))),inference(variable_rename,[status(thm)],[c45])).
% 2.81/3.14 cnf(c47,plain,~environment(X141)|~in_environment(X141,X142)|~greater(cardinality_at_time(first_movers,X142),zero)|~greater(cardinality_at_time(efficient_producers,X142),zero)|subpopulations(first_movers,efficient_producers,X141,X142),inference(split_conjunct,[status(thm)],[c46])).
% 2.81/3.14 fof(t6,plain,(![E]:(![T]:(((environment(E)&in_environment(E,T))&greater_or_equal(T,appear(efficient_producers,E)))=>greater(cardinality_at_time(efficient_producers,T),zero)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t6)).
% 2.81/3.14 fof(c25,plain,(![E]:(![T]:(((~environment(E)|~in_environment(E,T))|~greater_or_equal(T,appear(efficient_producers,E)))|greater(cardinality_at_time(efficient_producers,T),zero)))),inference(fof_nnf,[status(thm)],[t6])).
% 2.81/3.14 fof(c26,plain,(![X7]:(![X8]:(((~environment(X7)|~in_environment(X7,X8))|~greater_or_equal(X8,appear(efficient_producers,X7)))|greater(cardinality_at_time(efficient_producers,X8),zero)))),inference(variable_rename,[status(thm)],[c25])).
% 2.81/3.14 cnf(c27,plain,~environment(X136)|~in_environment(X136,X135)|~greater_or_equal(X135,appear(efficient_producers,X136))|greater(cardinality_at_time(efficient_producers,X135),zero),inference(split_conjunct,[status(thm)],[c26])).
% 2.81/3.14 cnf(c34,plain,~greater(X32,X33)|greater_or_equal(X32,X33),inference(split_conjunct,[status(thm)],[c32])).
% 2.81/3.14 cnf(c288,plain,greater_or_equal(skolem0003(skolem0001,skolem0002(skolem0001)),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c263, c34])).
% 2.81/3.14 cnf(c293,plain,~environment(skolem0001)|~in_environment(skolem0001,skolem0003(skolem0001,skolem0002(skolem0001)))|greater(cardinality_at_time(efficient_producers,skolem0003(skolem0001,skolem0002(skolem0001))),zero),inference(resolution,[status(thm)],[c288, c27])).
% 2.81/3.14 cnf(c398,plain,~environment(skolem0001)|greater(cardinality_at_time(efficient_producers,skolem0003(skolem0001,skolem0002(skolem0001))),zero),inference(resolution,[status(thm)],[c293, c303])).
% 2.81/3.14 cnf(c399,plain,greater(cardinality_at_time(efficient_producers,skolem0003(skolem0001,skolem0002(skolem0001))),zero),inference(resolution,[status(thm)],[c398, c15])).
% 2.81/3.14 cnf(c406,plain,~environment(X939)|~in_environment(X939,skolem0003(skolem0001,skolem0002(skolem0001)))|~greater(cardinality_at_time(first_movers,skolem0003(skolem0001,skolem0002(skolem0001))),zero)|subpopulations(first_movers,efficient_producers,X939,skolem0003(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c399, c47])).
% 2.81/3.14 cnf(c3951,plain,~environment(X940)|~in_environment(X940,skolem0003(skolem0001,skolem0002(skolem0001)))|subpopulations(first_movers,efficient_producers,X940,skolem0003(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c406, c154])).
% 2.81/3.14 cnf(c3952,plain,~environment(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c3951, c303])).
% 2.81/3.14 cnf(c3953,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c3952, c15])).
% 2.81/3.14 cnf(c3955,plain,~environment(skolem0001)|~stable(skolem0001)|~greater_or_equal(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|greater(zero,growth_rate(first_movers,skolem0003(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c3953, c24])).
% 2.81/3.14 cnf(c3962,plain,~environment(skolem0001)|~stable(skolem0001)|greater(zero,growth_rate(first_movers,skolem0003(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c3955, c142])).
% 2.81/3.14 cnf(c3963,plain,~environment(skolem0001)|greater(zero,growth_rate(first_movers,skolem0003(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c3962, c16])).
% 2.81/3.14 cnf(c3964,plain,greater(zero,growth_rate(first_movers,skolem0003(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c3963, c15])).
% 2.81/3.14 cnf(c3965,plain,~environment(skolem0001)|~stable(skolem0001)|~in_environment(skolem0001,skolem0002(skolem0001))|contracts_from(skolem0002(skolem0001),first_movers),inference(resolution,[status(thm)],[c3964, c54])).
% 2.81/3.14 cnf(c3985,plain,~environment(skolem0001)|~stable(skolem0001)|contracts_from(skolem0002(skolem0001),first_movers),inference(resolution,[status(thm)],[c3965, c102])).
% 2.81/3.14 cnf(c3986,plain,~environment(skolem0001)|contracts_from(skolem0002(skolem0001),first_movers),inference(resolution,[status(thm)],[c3985, c16])).
% 2.81/3.14 cnf(c3987,plain,contracts_from(skolem0002(skolem0001),first_movers),inference(resolution,[status(thm)],[c3986, c15])).
% 2.81/3.14 cnf(c3989,plain,$false,inference(resolution,[status(thm)],[c3987, c86])).
% 2.81/3.14 % SZS output end CNFRefutation
% 2.81/3.14
% 2.81/3.14 % Initial clauses : 29
% 2.81/3.14 % Processed clauses : 460
% 2.81/3.14 % Factors computed : 6
% 2.81/3.14 % Resolvents computed: 3931
% 2.81/3.14 % Tautologies deleted: 5
% 2.81/3.14 % Forward subsumed : 381
% 2.81/3.14 % Backward subsumed : 41
% 2.81/3.14 % -------- CPU Time ---------
% 2.81/3.14 % User time : 2.730 s
% 2.81/3.14 % System time : 0.048 s
% 2.81/3.14 % Total time : 2.778 s
%------------------------------------------------------------------------------