%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT026+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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 28.95s 29.29s
% Output : CNFRefutation 28.95s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT026+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n004.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:11:45 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 """
% 28.95/29.29 % Version: 1.5
% 28.95/29.29 % SZS status Theorem
% 28.95/29.29 % SZS output start CNFRefutation
% 28.95/29.29 fof(prove_l8,conjecture,(![E]:(![T]:(((environment(E)&in_environment(E,T))&greater(T,critical_point(E)))=>selection_favors(efficient_producers,first_movers,T)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_l8)).
% 28.95/29.29 fof(c11,negated_conjecture,(~(![E]:(![T]:(((environment(E)&in_environment(E,T))&greater(T,critical_point(E)))=>selection_favors(efficient_producers,first_movers,T))))),inference(assume_negation,[status(cth)],[prove_l8])).
% 28.95/29.29 fof(c12,negated_conjecture,(?[E]:(?[T]:(((environment(E)&in_environment(E,T))&greater(T,critical_point(E)))&~selection_favors(efficient_producers,first_movers,T)))),inference(fof_nnf,[status(thm)],[c11])).
% 28.95/29.29 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(((environment(X2)&in_environment(X2,X3))&greater(X3,critical_point(X2)))&~selection_favors(efficient_producers,first_movers,X3)))),inference(variable_rename,[status(thm)],[c12])).
% 28.95/29.29 fof(c14,negated_conjecture,(((environment(skolem0001)&in_environment(skolem0001,skolem0002))&greater(skolem0002,critical_point(skolem0001)))&~selection_favors(efficient_producers,first_movers,skolem0002)),inference(skolemize,[status(esa)],[c13])).
% 28.95/29.29 cnf(c18,negated_conjecture,~selection_favors(efficient_producers,first_movers,skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 28.95/29.29 cnf(c15,negated_conjecture,environment(skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 28.95/29.29 cnf(c16,negated_conjecture,in_environment(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c14])).
% 28.95/29.29 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)).
% 28.95/29.29 fof(c51,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])).
% 28.95/29.29 fof(c52,plain,(![X21]:(![X22]:((((~environment(X21)|~in_environment(X21,X22))|~greater(cardinality_at_time(first_movers,X22),zero))|~greater(cardinality_at_time(efficient_producers,X22),zero))|subpopulations(first_movers,efficient_producers,X21,X22)))),inference(variable_rename,[status(thm)],[c51])).
% 28.95/29.29 cnf(c53,plain,~environment(X168)|~in_environment(X168,X167)|~greater(cardinality_at_time(first_movers,X167),zero)|~greater(cardinality_at_time(efficient_producers,X167),zero)|subpopulations(first_movers,efficient_producers,X168,X167),inference(split_conjunct,[status(thm)],[c52])).
% 28.95/29.29 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)).
% 28.95/29.29 fof(c19,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])).
% 28.95/29.29 fof(c20,plain,(![X4]:(![X5]:(((~environment(X4)|~in_environment(X4,X5))|~greater_or_equal(X5,appear(efficient_producers,X4)))|greater(cardinality_at_time(efficient_producers,X5),zero)))),inference(variable_rename,[status(thm)],[c19])).
% 28.95/29.29 cnf(c21,plain,~environment(X145)|~in_environment(X145,X144)|~greater_or_equal(X144,appear(efficient_producers,X145))|greater(cardinality_at_time(efficient_producers,X144),zero),inference(split_conjunct,[status(thm)],[c20])).
% 28.95/29.29 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)).
% 28.95/29.29 fof(c29,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])).
% 28.95/29.29 fof(c30,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)],[c29])).
% 28.95/29.29 fof(c32,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(c31,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)],[c30])).])).
% 28.95/29.29 fof(c33,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)],[c32])).
% 28.95/29.29 cnf(c35,plain,~greater(X39,X38)|greater_or_equal(X39,X38),inference(split_conjunct,[status(thm)],[c33])).
% 28.95/29.29 cnf(c17,negated_conjecture,greater(skolem0002,critical_point(skolem0001)),inference(split_conjunct,[status(thm)],[c14])).
% 28.95/29.29 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)).
% 28.95/29.29 fof(c37,plain,(![X]:(![Y]:(![Z]:((~greater(X,Y)|~greater(Y,Z))|greater(X,Z))))),inference(fof_nnf,[status(thm)],[mp_greater_transitivity])).
% 28.95/29.29 fof(c38,plain,(![X13]:(![X14]:(![X15]:((~greater(X13,X14)|~greater(X14,X15))|greater(X13,X15))))),inference(variable_rename,[status(thm)],[c37])).
% 28.95/29.29 cnf(c39,plain,~greater(X64,X65)|~greater(X65,X63)|greater(X64,X63),inference(split_conjunct,[status(thm)],[c38])).
% 28.95/29.29 cnf(reflexivity,axiom,X31=X31,theory(equality)).
% 28.95/29.29 cnf(c5,axiom,X85!=X84|X83!=X86|~greater(X85,X83)|greater(X84,X86),theory(equality)).
% 28.95/29.29 cnf(c83,plain,skolem0002!=X148|critical_point(skolem0001)!=X149|greater(X148,X149),inference(resolution,[status(thm)],[c5, c17])).
% 28.95/29.29 cnf(c34,plain,~greater_or_equal(X61,X60)|greater(X61,X60)|X61=X60,inference(split_conjunct,[status(thm)],[c33])).
% 28.95/29.29 fof(mp_critical_point_after_EP,axiom,(![E]:(environment(E)=>greater_or_equal(critical_point(E),appear(efficient_producers,E)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_critical_point_after_EP)).
% 28.95/29.29 fof(c40,plain,(![E]:(~environment(E)|greater_or_equal(critical_point(E),appear(efficient_producers,E)))),inference(fof_nnf,[status(thm)],[mp_critical_point_after_EP])).
% 28.95/29.29 fof(c41,plain,(![X16]:(~environment(X16)|greater_or_equal(critical_point(X16),appear(efficient_producers,X16)))),inference(variable_rename,[status(thm)],[c40])).
% 28.95/29.29 cnf(c42,plain,~environment(X72)|greater_or_equal(critical_point(X72),appear(efficient_producers,X72)),inference(split_conjunct,[status(thm)],[c41])).
% 28.95/29.29 cnf(c77,plain,greater_or_equal(critical_point(skolem0001),appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c42, c15])).
% 28.95/29.29 cnf(c78,plain,greater(critical_point(skolem0001),appear(efficient_producers,skolem0001))|critical_point(skolem0001)=appear(efficient_producers,skolem0001),inference(resolution,[status(thm)],[c77, c34])).
% 28.95/29.29 cnf(c176,plain,greater(critical_point(skolem0001),appear(efficient_producers,skolem0001))|skolem0002!=X209|greater(X209,appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c78, c83])).
% 28.95/29.29 cnf(c477,plain,greater(critical_point(skolem0001),appear(efficient_producers,skolem0001))|greater(skolem0002,appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c176, reflexivity])).
% 28.95/29.29 cnf(c479,plain,greater(skolem0002,appear(efficient_producers,skolem0001))|~greater(X249,critical_point(skolem0001))|greater(X249,appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c477, c39])).
% 28.95/29.29 cnf(c720,plain,greater(skolem0002,appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c479, c17])).
% 28.95/29.29 cnf(c721,plain,greater_or_equal(skolem0002,appear(efficient_producers,skolem0001)),inference(resolution,[status(thm)],[c720, c35])).
% 28.95/29.29 cnf(c726,plain,~environment(skolem0001)|~in_environment(skolem0001,skolem0002)|greater(cardinality_at_time(efficient_producers,skolem0002),zero),inference(resolution,[status(thm)],[c721, c21])).
% 28.95/29.29 cnf(c756,plain,~environment(skolem0001)|greater(cardinality_at_time(efficient_producers,skolem0002),zero),inference(resolution,[status(thm)],[c726, c16])).
% 28.95/29.29 cnf(c757,plain,greater(cardinality_at_time(efficient_producers,skolem0002),zero),inference(resolution,[status(thm)],[c756, c15])).
% 28.95/29.29 cnf(c759,plain,~environment(X329)|~in_environment(X329,skolem0002)|~greater(cardinality_at_time(first_movers,skolem0002),zero)|subpopulations(first_movers,efficient_producers,X329,skolem0002),inference(resolution,[status(thm)],[c757, c53])).
% 28.95/29.29 fof(mp_subpopulations,axiom,(![E]:(![T]:((environment(E)&in_environment(E,T))=>(subpopulation(first_movers,E,T)&subpopulation(efficient_producers,E,T))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_subpopulations)).
% 28.95/29.29 fof(c43,plain,(![E]:(![T]:((~environment(E)|~in_environment(E,T))|(subpopulation(first_movers,E,T)&subpopulation(efficient_producers,E,T))))),inference(fof_nnf,[status(thm)],[mp_subpopulations])).
% 28.95/29.29 fof(c44,plain,(![X17]:(![X18]:((~environment(X17)|~in_environment(X17,X18))|(subpopulation(first_movers,X17,X18)&subpopulation(efficient_producers,X17,X18))))),inference(variable_rename,[status(thm)],[c43])).
% 28.95/29.29 fof(c45,plain,(![X17]:(![X18]:(((~environment(X17)|~in_environment(X17,X18))|subpopulation(first_movers,X17,X18))&((~environment(X17)|~in_environment(X17,X18))|subpopulation(efficient_producers,X17,X18))))),inference(distribute,[status(thm)],[c44])).
% 28.95/29.29 cnf(c47,plain,~environment(X81)|~in_environment(X81,X82)|subpopulation(efficient_producers,X81,X82),inference(split_conjunct,[status(thm)],[c45])).
% 28.95/29.29 cnf(c81,plain,~environment(skolem0001)|subpopulation(efficient_producers,skolem0001,skolem0002),inference(resolution,[status(thm)],[c47, c16])).
% 28.95/29.29 cnf(c82,plain,subpopulation(efficient_producers,skolem0001,skolem0002),inference(resolution,[status(thm)],[c81, c15])).
% 28.95/29.29 cnf(c46,plain,~environment(X73)|~in_environment(X73,X74)|subpopulation(first_movers,X73,X74),inference(split_conjunct,[status(thm)],[c45])).
% 28.95/29.29 cnf(c79,plain,~environment(skolem0001)|subpopulation(first_movers,skolem0001,skolem0002),inference(resolution,[status(thm)],[c46, c16])).
% 28.95/29.29 cnf(c80,plain,subpopulation(first_movers,skolem0001,skolem0002),inference(resolution,[status(thm)],[c79, c15])).
% 28.95/29.29 fof(mp2_favour_members,axiom,(![E]:(![S1]:(![S2]:(![T]:(((((environment(E)&subpopulation(S1,E,T))&subpopulation(S2,E,T))&greater(cardinality_at_time(S1,T),zero))&cardinality_at_time(S2,T)=zero)=>selection_favors(S1,S2,T)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp2_favour_members)).
% 28.95/29.29 fof(c54,plain,(![E]:(![S1]:(![S2]:(![T]:(((((~environment(E)|~subpopulation(S1,E,T))|~subpopulation(S2,E,T))|~greater(cardinality_at_time(S1,T),zero))|cardinality_at_time(S2,T)!=zero)|selection_favors(S1,S2,T)))))),inference(fof_nnf,[status(thm)],[mp2_favour_members])).
% 28.95/29.29 fof(c55,plain,(![X23]:(![X24]:(![X25]:(![X26]:(((((~environment(X23)|~subpopulation(X24,X23,X26))|~subpopulation(X25,X23,X26))|~greater(cardinality_at_time(X24,X26),zero))|cardinality_at_time(X25,X26)!=zero)|selection_favors(X24,X25,X26)))))),inference(variable_rename,[status(thm)],[c54])).
% 28.95/29.29 cnf(c56,plain,~environment(X178)|~subpopulation(X177,X178,X176)|~subpopulation(X179,X178,X176)|~greater(cardinality_at_time(X177,X176),zero)|cardinality_at_time(X179,X176)!=zero|selection_favors(X177,X179,X176),inference(split_conjunct,[status(thm)],[c55])).
% 28.95/29.29 fof(mp_first_movers_exist,axiom,(![E]:(![T]:((environment(E)&in_environment(E,T))=>greater_or_equal(cardinality_at_time(first_movers,T),zero)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp_first_movers_exist)).
% 28.95/29.29 fof(c48,plain,(![E]:(![T]:((~environment(E)|~in_environment(E,T))|greater_or_equal(cardinality_at_time(first_movers,T),zero)))),inference(fof_nnf,[status(thm)],[mp_first_movers_exist])).
% 28.95/29.29 fof(c49,plain,(![X19]:(![X20]:((~environment(X19)|~in_environment(X19,X20))|greater_or_equal(cardinality_at_time(first_movers,X20),zero)))),inference(variable_rename,[status(thm)],[c48])).
% 28.95/29.29 cnf(c50,plain,~environment(X147)|~in_environment(X147,X146)|greater_or_equal(cardinality_at_time(first_movers,X146),zero),inference(split_conjunct,[status(thm)],[c49])).
% 28.95/29.29 cnf(c103,plain,~environment(skolem0001)|greater_or_equal(cardinality_at_time(first_movers,skolem0002),zero),inference(resolution,[status(thm)],[c50, c16])).
% 28.95/29.29 cnf(c104,plain,greater_or_equal(cardinality_at_time(first_movers,skolem0002),zero),inference(resolution,[status(thm)],[c103, c15])).
% 28.95/29.29 cnf(c105,plain,greater(cardinality_at_time(first_movers,skolem0002),zero)|cardinality_at_time(first_movers,skolem0002)=zero,inference(resolution,[status(thm)],[c104, c34])).
% 28.95/29.29 cnf(c137,plain,greater(cardinality_at_time(first_movers,skolem0002),zero)|~environment(X210)|~subpopulation(X211,X210,skolem0002)|~subpopulation(first_movers,X210,skolem0002)|~greater(cardinality_at_time(X211,skolem0002),zero)|selection_favors(X211,first_movers,skolem0002),inference(resolution,[status(thm)],[c105, c56])).
% 28.95/29.29 cnf(c760,plain,greater(cardinality_at_time(first_movers,skolem0002),zero)|~environment(X2677)|~subpopulation(efficient_producers,X2677,skolem0002)|~subpopulation(first_movers,X2677,skolem0002)|selection_favors(efficient_producers,first_movers,skolem0002),inference(resolution,[status(thm)],[c757, c137])).
% 28.95/29.29 cnf(c40051,plain,greater(cardinality_at_time(first_movers,skolem0002),zero)|~environment(skolem0001)|~subpopulation(efficient_producers,skolem0001,skolem0002)|selection_favors(efficient_producers,first_movers,skolem0002),inference(resolution,[status(thm)],[c760, c80])).
% 28.95/29.29 cnf(c40052,plain,greater(cardinality_at_time(first_movers,skolem0002),zero)|~environment(skolem0001)|selection_favors(efficient_producers,first_movers,skolem0002),inference(resolution,[status(thm)],[c40051, c82])).
% 28.95/29.29 cnf(c40053,plain,greater(cardinality_at_time(first_movers,skolem0002),zero)|selection_favors(efficient_producers,first_movers,skolem0002),inference(resolution,[status(thm)],[c40052, c15])).
% 28.95/29.29 cnf(c40059,plain,greater(cardinality_at_time(first_movers,skolem0002),zero),inference(resolution,[status(thm)],[c40053, c18])).
% 28.95/29.29 cnf(c40061,plain,~environment(X2679)|~in_environment(X2679,skolem0002)|subpopulations(first_movers,efficient_producers,X2679,skolem0002),inference(resolution,[status(thm)],[c40059, c759])).
% 28.95/29.29 cnf(c40066,plain,~environment(skolem0001)|subpopulations(first_movers,efficient_producers,skolem0001,skolem0002),inference(resolution,[status(thm)],[c40061, c16])).
% 28.95/29.29 cnf(c40067,plain,subpopulations(first_movers,efficient_producers,skolem0001,skolem0002),inference(resolution,[status(thm)],[c40066, c15])).
% 28.95/29.29 fof(mp1_high_growth_rates,axiom,(![E]:(![S1]:(![S2]:(![T]:(((environment(E)&subpopulations(S1,S2,E,T))&greater(growth_rate(S2,T),growth_rate(S1,T)))=>selection_favors(S2,S1,T)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp1_high_growth_rates)).
% 28.95/29.29 fof(c57,plain,(![E]:(![S1]:(![S2]:(![T]:(((~environment(E)|~subpopulations(S1,S2,E,T))|~greater(growth_rate(S2,T),growth_rate(S1,T)))|selection_favors(S2,S1,T)))))),inference(fof_nnf,[status(thm)],[mp1_high_growth_rates])).
% 28.95/29.29 fof(c58,plain,(![X27]:(![X28]:(![X29]:(![X30]:(((~environment(X27)|~subpopulations(X28,X29,X27,X30))|~greater(growth_rate(X29,X30),growth_rate(X28,X30)))|selection_favors(X29,X28,X30)))))),inference(variable_rename,[status(thm)],[c57])).
% 28.95/29.29 cnf(c59,plain,~environment(X183)|~subpopulations(X184,X186,X183,X185)|~greater(growth_rate(X186,X185),growth_rate(X184,X185))|selection_favors(X186,X184,X185),inference(split_conjunct,[status(thm)],[c58])).
% 28.95/29.29 fof(d1,plain,(![E]:(![Tc]:((environment(E)&Tc=critical_point(E))=>((~greater(growth_rate(efficient_producers,Tc),growth_rate(first_movers,Tc)))&(![T]:((subpopulations(first_movers,efficient_producers,E,T)&greater(T,Tc))=>greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1)).
% 28.95/29.29 fof(c22,plain,(![E]:(![Tc]:((environment(E)&Tc=critical_point(E))=>(~greater(growth_rate(efficient_producers,Tc),growth_rate(first_movers,Tc))&(![T]:((subpopulations(first_movers,efficient_producers,E,T)&greater(T,Tc))=>greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)))))))),inference(fof_simplification,[status(thm)],[d1])).
% 28.95/29.29 fof(c23,plain,(![E]:(![Tc]:((~environment(E)|Tc!=critical_point(E))|(~greater(growth_rate(efficient_producers,Tc),growth_rate(first_movers,Tc))&(![T]:((~subpopulations(first_movers,efficient_producers,E,T)|~greater(T,Tc))|greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)))))))),inference(fof_nnf,[status(thm)],[c22])).
% 28.95/29.29 fof(c25,plain,(![X6]:(![X7]:(![X8]:((~environment(X6)|X7!=critical_point(X6))|(~greater(growth_rate(efficient_producers,X7),growth_rate(first_movers,X7))&((~subpopulations(first_movers,efficient_producers,X6,X8)|~greater(X8,X7))|greater(growth_rate(efficient_producers,X8),growth_rate(first_movers,X8)))))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,(![X6]:(![X7]:((~environment(X6)|X7!=critical_point(X6))|(~greater(growth_rate(efficient_producers,X7),growth_rate(first_movers,X7))&(![X8]:((~subpopulations(first_movers,efficient_producers,X6,X8)|~greater(X8,X7))|greater(growth_rate(efficient_producers,X8),growth_rate(first_movers,X8)))))))),inference(variable_rename,[status(thm)],[c23])).])).
% 28.95/29.29 fof(c26,plain,(![X6]:(![X7]:(![X8]:(((~environment(X6)|X7!=critical_point(X6))|~greater(growth_rate(efficient_producers,X7),growth_rate(first_movers,X7)))&((~environment(X6)|X7!=critical_point(X6))|((~subpopulations(first_movers,efficient_producers,X6,X8)|~greater(X8,X7))|greater(growth_rate(efficient_producers,X8),growth_rate(first_movers,X8)))))))),inference(distribute,[status(thm)],[c25])).
% 28.95/29.29 cnf(c28,plain,~environment(X157)|X156!=critical_point(X157)|~subpopulations(first_movers,efficient_producers,X157,X158)|~greater(X158,X156)|greater(growth_rate(efficient_producers,X158),growth_rate(first_movers,X158)),inference(split_conjunct,[status(thm)],[c26])).
% 28.95/29.29 cnf(c40069,plain,~environment(skolem0001)|X2702!=critical_point(skolem0001)|~greater(skolem0002,X2702)|greater(growth_rate(efficient_producers,skolem0002),growth_rate(first_movers,skolem0002)),inference(resolution,[status(thm)],[c40067, c28])).
% 28.95/29.29 cnf(c40077,plain,~environment(skolem0001)|~greater(skolem0002,critical_point(skolem0001))|greater(growth_rate(efficient_producers,skolem0002),growth_rate(first_movers,skolem0002)),inference(resolution,[status(thm)],[c40069, reflexivity])).
% 28.95/29.29 cnf(c40078,plain,~environment(skolem0001)|greater(growth_rate(efficient_producers,skolem0002),growth_rate(first_movers,skolem0002)),inference(resolution,[status(thm)],[c40077, c17])).
% 28.95/29.29 cnf(c40079,plain,greater(growth_rate(efficient_producers,skolem0002),growth_rate(first_movers,skolem0002)),inference(resolution,[status(thm)],[c40078, c15])).
% 28.95/29.29 cnf(c40082,plain,~environment(X2706)|~subpopulations(first_movers,efficient_producers,X2706,skolem0002)|selection_favors(efficient_producers,first_movers,skolem0002),inference(resolution,[status(thm)],[c40079, c59])).
% 28.95/29.29 cnf(c40087,plain,~environment(skolem0001)|selection_favors(efficient_producers,first_movers,skolem0002),inference(resolution,[status(thm)],[c40082, c40067])).
% 28.95/29.29 cnf(c40088,plain,selection_favors(efficient_producers,first_movers,skolem0002),inference(resolution,[status(thm)],[c40087, c15])).
% 28.95/29.29 cnf(c40089,plain,$false,inference(resolution,[status(thm)],[c40088, c18])).
% 28.95/29.29 % SZS output end CNFRefutation
% 28.95/29.29
% 28.95/29.29 % Initial clauses : 32
% 28.95/29.29 % Processed clauses : 1175
% 28.95/29.29 % Factors computed : 6
% 28.95/29.29 % Resolvents computed: 40025
% 28.95/29.29 % Tautologies deleted: 4
% 28.95/29.29 % Forward subsumed : 1350
% 28.95/29.29 % Backward subsumed : 996
% 28.95/29.29 % -------- CPU Time ---------
% 28.95/29.29 % User time : 28.736 s
% 28.95/29.29 % System time : 0.203 s
% 28.95/29.29 % Total time : 28.939 s
%------------------------------------------------------------------------------