%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT023+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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 0.47s 0.71s
% Output : CNFRefutation 0.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT023+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.06 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.42 % Computer : n007.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 7 12:04:11 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.16/0.48 (re.compile("\."), Token.FullStop),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.16/0.48 (re.compile("\("), Token.OpenPar),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.16/0.48 (re.compile("\)"), Token.ClosePar),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.16/0.48 (re.compile("\["), Token.OpenSquare),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.16/0.48 (re.compile("\]"), Token.CloseSquare),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.16/0.48 (re.compile("~\|"), Token.Nor),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.16/0.48 (re.compile("\|"), Token.Or),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.16/0.48 (re.compile("\?"), Token.Existential),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.16/0.48 (re.compile("\s+"), Token.WhiteSpace),
% 0.16/0.48 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.16/0.48 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.27/0.54 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.27/0.54 """
% 0.27/0.54 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.27/0.54 """
% 0.38/0.62 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.38/0.62 """
% 0.47/0.71 % Version: 1.5
% 0.47/0.71 % SZS status Theorem
% 0.47/0.71 % SZS output start CNFRefutation
% 0.47/0.71 fof(prove_l5,conjecture,(![E]:((environment(E)&stable(E))=>in_environment(E,critical_point(E)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l5)).
% 0.47/0.71 fof(c7,negated_conjecture,(~(![E]:((environment(E)&stable(E))=>in_environment(E,critical_point(E))))),inference(assume_negation,[status(cth)],[prove_l5])).
% 0.47/0.71 fof(c8,negated_conjecture,(?[E]:((environment(E)&stable(E))&~in_environment(E,critical_point(E)))),inference(fof_nnf,[status(thm)],[c7])).
% 0.47/0.71 fof(c9,negated_conjecture,(?[X2]:((environment(X2)&stable(X2))&~in_environment(X2,critical_point(X2)))),inference(variable_rename,[status(thm)],[c8])).
% 0.47/0.71 fof(c10,negated_conjecture,((environment(skolem0001)&stable(skolem0001))&~in_environment(skolem0001,critical_point(skolem0001))),inference(skolemize,[status(esa)],[c9])).
% 0.47/0.71 cnf(c13,negated_conjecture,~in_environment(skolem0001,critical_point(skolem0001)),inference(split_conjunct,[status(thm)],[c10])).
% 0.47/0.71 cnf(reflexivity,axiom,X9=X9,theory(equality)).
% 0.47/0.71 cnf(c11,negated_conjecture,environment(skolem0001),inference(split_conjunct,[status(thm)],[c10])).
% 0.47/0.71 cnf(c12,negated_conjecture,stable(skolem0001),inference(split_conjunct,[status(thm)],[c10])).
% 0.47/0.71 fof(l12,plain,(![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', l12)).
% 0.47/0.71 fof(c14,plain,(![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)],[l12])).
% 0.47/0.71 fof(c15,plain,(![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)],[c14])).
% 0.47/0.71 fof(c16,plain,(![X3]:((~environment(X3)|~stable(X3))|(?[X4]:((in_environment(X3,X4)&~greater(growth_rate(efficient_producers,X4),growth_rate(first_movers,X4)))&(![X5]:((~subpopulations(first_movers,efficient_producers,X3,X5)|~greater(X5,X4))|greater(growth_rate(efficient_producers,X5),growth_rate(first_movers,X5)))))))),inference(variable_rename,[status(thm)],[c15])).
% 0.47/0.71 fof(c18,plain,(![X3]:(![X5]:((~environment(X3)|~stable(X3))|((in_environment(X3,skolem0002(X3))&~greater(growth_rate(efficient_producers,skolem0002(X3)),growth_rate(first_movers,skolem0002(X3))))&((~subpopulations(first_movers,efficient_producers,X3,X5)|~greater(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))&~greater(growth_rate(efficient_producers,skolem0002(X3)),growth_rate(first_movers,skolem0002(X3))))&(![X5]:((~subpopulations(first_movers,efficient_producers,X3,X5)|~greater(X5,skolem0002(X3)))|greater(growth_rate(efficient_producers,X5),growth_rate(first_movers,X5))))))),inference(skolemize,[status(esa)],[c16])).])).
% 0.47/0.71 fof(c19,plain,(![X3]:(![X5]:((((~environment(X3)|~stable(X3))|in_environment(X3,skolem0002(X3)))&((~environment(X3)|~stable(X3))|~greater(growth_rate(efficient_producers,skolem0002(X3)),growth_rate(first_movers,skolem0002(X3)))))&((~environment(X3)|~stable(X3))|((~subpopulations(first_movers,efficient_producers,X3,X5)|~greater(X5,skolem0002(X3)))|greater(growth_rate(efficient_producers,X5),growth_rate(first_movers,X5))))))),inference(distribute,[status(thm)],[c18])).
% 0.47/0.71 cnf(c20,plain,~environment(X28)|~stable(X28)|in_environment(X28,skolem0002(X28)),inference(split_conjunct,[status(thm)],[c19])).
% 0.47/0.71 cnf(c37,plain,~environment(skolem0001)|in_environment(skolem0001,skolem0002(skolem0001)),inference(resolution,[status(thm)],[c20, c12])).
% 0.47/0.71 cnf(c38,plain,in_environment(skolem0001,skolem0002(skolem0001)),inference(resolution,[status(thm)],[c37, c11])).
% 0.47/0.71 cnf(c2,axiom,X42!=X44|X41!=X43|~in_environment(X42,X41)|in_environment(X44,X43),theory(equality)).
% 0.47/0.71 cnf(c43,plain,skolem0001!=X50|skolem0002(skolem0001)!=X49|in_environment(X50,X49),inference(resolution,[status(thm)],[c2, c38])).
% 0.47/0.71 cnf(c21,plain,~environment(X52)|~stable(X52)|~greater(growth_rate(efficient_producers,skolem0002(X52)),growth_rate(first_movers,skolem0002(X52))),inference(split_conjunct,[status(thm)],[c19])).
% 0.47/0.71 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/sandbox/benchmark/theBenchmark.p', d1)).
% 0.47/0.71 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_simplification,[status(thm)],[d1])).
% 0.47/0.71 fof(c24,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)],[c23])).
% 0.47/0.71 fof(c25,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)],[c24])).
% 0.47/0.71 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))&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)],[c25])).
% 0.47/0.71 fof(c27,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)],[c26])).
% 0.47/0.71 cnf(c30,plain,~environment(X67)|greater(growth_rate(efficient_producers,X68),growth_rate(first_movers,X68))|~in_environment(X67,X68)|~greater(growth_rate(efficient_producers,skolem0003(X67,X68)),growth_rate(first_movers,skolem0003(X67,X68)))|X68=critical_point(X67),inference(split_conjunct,[status(thm)],[c27])).
% 0.47/0.71 cnf(c29,plain,~environment(X63)|greater(growth_rate(efficient_producers,X64),growth_rate(first_movers,X64))|~in_environment(X63,X64)|greater(skolem0003(X63,X64),X64)|X64=critical_point(X63),inference(split_conjunct,[status(thm)],[c27])).
% 0.47/0.71 cnf(c46,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0002(skolem0001)),growth_rate(first_movers,skolem0002(skolem0001)))|greater(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0002(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c29, c38])).
% 0.47/0.71 cnf(c48,plain,greater(growth_rate(efficient_producers,skolem0002(skolem0001)),growth_rate(first_movers,skolem0002(skolem0001)))|greater(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0002(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c46, c11])).
% 0.47/0.71 cnf(c50,plain,greater(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0002(skolem0001)=critical_point(skolem0001)|~environment(skolem0001)|~stable(skolem0001),inference(resolution,[status(thm)],[c48, c21])).
% 0.47/0.71 cnf(c62,plain,greater(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0002(skolem0001)=critical_point(skolem0001)|~environment(skolem0001),inference(resolution,[status(thm)],[c50, c12])).
% 0.47/0.71 cnf(c63,plain,greater(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0002(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c62, c11])).
% 0.47/0.71 cnf(c67,plain,greater(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|skolem0001!=X69|in_environment(X69,critical_point(skolem0001)),inference(resolution,[status(thm)],[c63, c43])).
% 0.47/0.71 cnf(c96,plain,greater(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|in_environment(skolem0001,critical_point(skolem0001)),inference(resolution,[status(thm)],[c67, reflexivity])).
% 0.47/0.71 cnf(c98,plain,greater(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001)),inference(resolution,[status(thm)],[c96, c13])).
% 0.47/0.71 cnf(c22,plain,~environment(X61)|~stable(X61)|~subpopulations(first_movers,efficient_producers,X61,X62)|~greater(X62,skolem0002(X61))|greater(growth_rate(efficient_producers,X62),growth_rate(first_movers,X62)),inference(split_conjunct,[status(thm)],[c19])).
% 0.47/0.71 cnf(c28,plain,~environment(X65)|greater(growth_rate(efficient_producers,X66),growth_rate(first_movers,X66))|~in_environment(X65,X66)|subpopulations(first_movers,efficient_producers,X65,skolem0003(X65,X66))|X66=critical_point(X65),inference(split_conjunct,[status(thm)],[c27])).
% 0.47/0.71 cnf(c47,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0002(skolem0001)),growth_rate(first_movers,skolem0002(skolem0001)))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0002(skolem0001)))|skolem0002(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c28, c38])).
% 0.47/0.71 cnf(c49,plain,greater(growth_rate(efficient_producers,skolem0002(skolem0001)),growth_rate(first_movers,skolem0002(skolem0001)))|subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0002(skolem0001)))|skolem0002(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c47, c11])).
% 0.47/0.71 cnf(c83,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0002(skolem0001)))|skolem0002(skolem0001)=critical_point(skolem0001)|~environment(skolem0001)|~stable(skolem0001),inference(resolution,[status(thm)],[c49, c21])).
% 0.47/0.71 cnf(c106,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0002(skolem0001)))|skolem0002(skolem0001)=critical_point(skolem0001)|~environment(skolem0001),inference(resolution,[status(thm)],[c83, c12])).
% 0.47/0.71 cnf(c107,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0002(skolem0001)))|skolem0002(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c106, c11])).
% 0.47/0.71 cnf(c112,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0002(skolem0001)))|skolem0001!=X96|in_environment(X96,critical_point(skolem0001)),inference(resolution,[status(thm)],[c107, c43])).
% 0.47/0.71 cnf(c130,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0002(skolem0001)))|in_environment(skolem0001,critical_point(skolem0001)),inference(resolution,[status(thm)],[c112, reflexivity])).
% 0.47/0.71 cnf(c133,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0003(skolem0001,skolem0002(skolem0001))),inference(resolution,[status(thm)],[c130, c13])).
% 0.47/0.71 cnf(c138,plain,~environment(skolem0001)|~stable(skolem0001)|~greater(skolem0003(skolem0001,skolem0002(skolem0001)),skolem0002(skolem0001))|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c133, c22])).
% 0.47/0.71 cnf(c143,plain,~environment(skolem0001)|~stable(skolem0001)|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c138, c98])).
% 0.47/0.71 cnf(c144,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c143, c12])).
% 0.47/0.71 cnf(c145,plain,greater(growth_rate(efficient_producers,skolem0003(skolem0001,skolem0002(skolem0001))),growth_rate(first_movers,skolem0003(skolem0001,skolem0002(skolem0001)))),inference(resolution,[status(thm)],[c144, c11])).
% 0.47/0.71 cnf(c146,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0002(skolem0001)),growth_rate(first_movers,skolem0002(skolem0001)))|~in_environment(skolem0001,skolem0002(skolem0001))|skolem0002(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c145, c30])).
% 0.47/0.71 cnf(c150,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0002(skolem0001)),growth_rate(first_movers,skolem0002(skolem0001)))|skolem0002(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c146, c38])).
% 0.47/0.71 cnf(c151,plain,greater(growth_rate(efficient_producers,skolem0002(skolem0001)),growth_rate(first_movers,skolem0002(skolem0001)))|skolem0002(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c150, c11])).
% 0.47/0.71 cnf(c152,plain,skolem0002(skolem0001)=critical_point(skolem0001)|~environment(skolem0001)|~stable(skolem0001),inference(resolution,[status(thm)],[c151, c21])).
% 0.47/0.71 cnf(c164,plain,skolem0002(skolem0001)=critical_point(skolem0001)|~environment(skolem0001),inference(resolution,[status(thm)],[c152, c12])).
% 0.47/0.71 cnf(c165,plain,skolem0002(skolem0001)=critical_point(skolem0001),inference(resolution,[status(thm)],[c164, c11])).
% 0.47/0.71 cnf(c167,plain,skolem0001!=X144|in_environment(X144,critical_point(skolem0001)),inference(resolution,[status(thm)],[c165, c43])).
% 0.47/0.71 cnf(c184,plain,in_environment(skolem0001,critical_point(skolem0001)),inference(resolution,[status(thm)],[c167, reflexivity])).
% 0.47/0.71 cnf(c185,plain,$false,inference(resolution,[status(thm)],[c184, c13])).
% 0.47/0.71 % SZS output end CNFRefutation
% 0.47/0.71
% 0.47/0.71 % Initial clauses : 19
% 0.47/0.71 % Processed clauses : 64
% 0.47/0.71 % Factors computed : 2
% 0.47/0.71 % Resolvents computed: 156
% 0.47/0.71 % Tautologies deleted: 4
% 0.47/0.71 % Forward subsumed : 71
% 0.47/0.71 % Backward subsumed : 25
% 0.47/0.71 % -------- CPU Time ---------
% 0.47/0.71 % User time : 0.269 s
% 0.47/0.71 % System time : 0.016 s
% 0.47/0.71 % Total time : 0.285 s
%------------------------------------------------------------------------------