%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT039+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:18:45 AM UTC 2026
% Result : Theorem 0.66s 0.92s
% Output : CNFRefutation 0.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT039+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.34 % Computer : n009.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 7 12:53:52 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.41 (re.compile("\."), Token.FullStop),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.41 (re.compile("\("), Token.OpenPar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.41 (re.compile("\)"), Token.ClosePar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.41 (re.compile("\["), Token.OpenSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("~\|"), Token.Nor),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("\|"), Token.Or),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.41 (re.compile("\?"), Token.Existential),
% 0.12/0.41 /export/starexec/sandbox2/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/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.12/0.47 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.12/0.47 """
% 0.23/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.48 """
% 0.23/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.57 """
% 0.66/0.92 % Version: 1.5
% 0.66/0.92 % SZS status Theorem
% 0.66/0.92 % SZS output start CNFRefutation
% 0.66/0.92 fof(prove_t8,conjecture,(![P]:((observational_period(P)&slow_change(P))=>selection_favors(efficient_producers,first_movers,P))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_t8)).
% 0.66/0.92 fof(c11,negated_conjecture,(~(![P]:((observational_period(P)&slow_change(P))=>selection_favors(efficient_producers,first_movers,P)))),inference(assume_negation,[status(cth)],[prove_t8])).
% 0.66/0.92 fof(c12,negated_conjecture,(?[P]:((observational_period(P)&slow_change(P))&~selection_favors(efficient_producers,first_movers,P))),inference(fof_nnf,[status(thm)],[c11])).
% 0.66/0.92 fof(c13,negated_conjecture,(?[X2]:((observational_period(X2)&slow_change(X2))&~selection_favors(efficient_producers,first_movers,X2))),inference(variable_rename,[status(thm)],[c12])).
% 0.66/0.92 fof(c14,negated_conjecture,((observational_period(skolem0001)&slow_change(skolem0001))&~selection_favors(efficient_producers,first_movers,skolem0001)),inference(skolemize,[status(esa)],[c13])).
% 0.66/0.92 cnf(c17,negated_conjecture,~selection_favors(efficient_producers,first_movers,skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 0.66/0.92 cnf(c15,negated_conjecture,observational_period(skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 0.66/0.92 fof(mp_organizational_sets1,axiom,propagation_strategy(first_movers),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_organizational_sets1)).
% 0.66/0.92 cnf(c46,plain,propagation_strategy(first_movers),inference(split_conjunct,[status(thm)],[mp_organizational_sets1])).
% 0.66/0.92 fof(mp_organizational_sets2,axiom,propagation_strategy(efficient_producers),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_organizational_sets2)).
% 0.66/0.92 cnf(c45,plain,propagation_strategy(efficient_producers),inference(split_conjunct,[status(thm)],[mp_organizational_sets2])).
% 0.66/0.92 fof(mp3_favoured_trategy,axiom,(![P]:((((observational_period(P)&propagation_strategy(first_movers))&propagation_strategy(efficient_producers))&(![E]:((environment(E)&in_environment(P,E))=>selection_favors(efficient_producers,first_movers,end_time(E)))))=>selection_favors(efficient_producers,first_movers,P))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp3_favoured_trategy)).
% 0.66/0.92 fof(c54,plain,(![P]:((((~observational_period(P)|~propagation_strategy(first_movers))|~propagation_strategy(efficient_producers))|(?[E]:((environment(E)&in_environment(P,E))&~selection_favors(efficient_producers,first_movers,end_time(E)))))|selection_favors(efficient_producers,first_movers,P))),inference(fof_nnf,[status(thm)],[mp3_favoured_trategy])).
% 0.66/0.92 fof(c55,plain,(![X22]:((((~observational_period(X22)|~propagation_strategy(first_movers))|~propagation_strategy(efficient_producers))|(?[X23]:((environment(X23)&in_environment(X22,X23))&~selection_favors(efficient_producers,first_movers,end_time(X23)))))|selection_favors(efficient_producers,first_movers,X22))),inference(variable_rename,[status(thm)],[c54])).
% 0.66/0.92 fof(c56,plain,(![X22]:((((~observational_period(X22)|~propagation_strategy(first_movers))|~propagation_strategy(efficient_producers))|((environment(skolem0003(X22))&in_environment(X22,skolem0003(X22)))&~selection_favors(efficient_producers,first_movers,end_time(skolem0003(X22)))))|selection_favors(efficient_producers,first_movers,X22))),inference(skolemize,[status(esa)],[c55])).
% 0.66/0.92 fof(c57,plain,(![X22]:((((((~observational_period(X22)|~propagation_strategy(first_movers))|~propagation_strategy(efficient_producers))|environment(skolem0003(X22)))|selection_favors(efficient_producers,first_movers,X22))&((((~observational_period(X22)|~propagation_strategy(first_movers))|~propagation_strategy(efficient_producers))|in_environment(X22,skolem0003(X22)))|selection_favors(efficient_producers,first_movers,X22)))&((((~observational_period(X22)|~propagation_strategy(first_movers))|~propagation_strategy(efficient_producers))|~selection_favors(efficient_producers,first_movers,end_time(skolem0003(X22))))|selection_favors(efficient_producers,first_movers,X22)))),inference(distribute,[status(thm)],[c56])).
% 0.66/0.92 cnf(c60,plain,~observational_period(X113)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)|~selection_favors(efficient_producers,first_movers,end_time(skolem0003(X113)))|selection_favors(efficient_producers,first_movers,X113),inference(split_conjunct,[status(thm)],[c57])).
% 0.66/0.92 cnf(c58,plain,~observational_period(X107)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)|environment(skolem0003(X107))|selection_favors(efficient_producers,first_movers,X107),inference(split_conjunct,[status(thm)],[c57])).
% 0.66/0.92 cnf(c79,plain,~observational_period(X108)|~propagation_strategy(first_movers)|environment(skolem0003(X108))|selection_favors(efficient_producers,first_movers,X108),inference(resolution,[status(thm)],[c58, c45])).
% 0.66/0.92 cnf(c80,plain,~observational_period(X109)|environment(skolem0003(X109))|selection_favors(efficient_producers,first_movers,X109),inference(resolution,[status(thm)],[c79, c46])).
% 0.66/0.92 cnf(c81,plain,environment(skolem0003(skolem0001))|selection_favors(efficient_producers,first_movers,skolem0001),inference(resolution,[status(thm)],[c80, c15])).
% 0.66/0.93 cnf(c83,plain,environment(skolem0003(skolem0001)),inference(resolution,[status(thm)],[c81, c17])).
% 0.66/0.93 cnf(reflexivity,axiom,X24=X24,theory(equality)).
% 0.66/0.93 fof(mp_greater_or_equal,axiom,(![X]:(![Y]:(greater_or_equal(X,Y)<=>(greater(X,Y)|X=Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_or_equal)).
% 0.66/0.93 fof(c25,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])).
% 0.66/0.93 fof(c26,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)],[c25])).
% 0.66/0.93 fof(c28,plain,(![X7]:(![X8]:(![X9]:(![X10]:((~greater_or_equal(X7,X8)|(greater(X7,X8)|X7=X8))&((~greater(X9,X10)&X9!=X10)|greater_or_equal(X9,X10))))))),inference(shift_quantors,[status(thm)],[fof(c27,plain,((![X7]:(![X8]:(~greater_or_equal(X7,X8)|(greater(X7,X8)|X7=X8))))&(![X9]:(![X10]:((~greater(X9,X10)&X9!=X10)|greater_or_equal(X9,X10))))),inference(variable_rename,[status(thm)],[c26])).])).
% 0.66/0.93 fof(c29,plain,(![X7]:(![X8]:(![X9]:(![X10]:((~greater_or_equal(X7,X8)|(greater(X7,X8)|X7=X8))&((~greater(X9,X10)|greater_or_equal(X9,X10))&(X9!=X10|greater_or_equal(X9,X10)))))))),inference(distribute,[status(thm)],[c28])).
% 0.66/0.93 cnf(c32,plain,X31!=X30|greater_or_equal(X31,X30),inference(split_conjunct,[status(thm)],[c29])).
% 0.66/0.93 cnf(c62,plain,greater_or_equal(X32,X32),inference(resolution,[status(thm)],[c32, reflexivity])).
% 0.66/0.93 fof(mp_time_in_environment,axiom,(![E]:(![T]:(((environment(E)&greater_or_equal(T,start_time(E)))&greater_or_equal(end_time(E),T))=>in_environment(E,T)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_time_in_environment)).
% 0.66/0.93 fof(c42,plain,(![E]:(![T]:(((~environment(E)|~greater_or_equal(T,start_time(E)))|~greater_or_equal(end_time(E),T))|in_environment(E,T)))),inference(fof_nnf,[status(thm)],[mp_time_in_environment])).
% 0.66/0.93 fof(c43,plain,(![X17]:(![X18]:(((~environment(X17)|~greater_or_equal(X18,start_time(X17)))|~greater_or_equal(end_time(X17),X18))|in_environment(X17,X18)))),inference(variable_rename,[status(thm)],[c42])).
% 0.66/0.93 cnf(c44,plain,~environment(X98)|~greater_or_equal(X99,start_time(X98))|~greater_or_equal(end_time(X98),X99)|in_environment(X98,X99),inference(split_conjunct,[status(thm)],[c43])).
% 0.66/0.93 cnf(c78,plain,~environment(X100)|~greater_or_equal(end_time(X100),start_time(X100))|in_environment(X100,end_time(X100)),inference(resolution,[status(thm)],[c44, c62])).
% 0.66/0.93 cnf(c31,plain,~greater(X29,X28)|greater_or_equal(X29,X28),inference(split_conjunct,[status(thm)],[c29])).
% 0.66/0.93 cnf(c7,axiom,X78!=X76|X77!=X79|~in_environment(X78,X77)|in_environment(X76,X79),theory(equality)).
% 0.66/0.93 cnf(c16,negated_conjecture,slow_change(skolem0001),inference(split_conjunct,[status(thm)],[c14])).
% 0.66/0.93 fof(mp4_critical_point,axiom,(![P]:((observational_period(P)&slow_change(P))=>(![E]:((environment(E)&in_environment(P,E))=>(?[T]:(in_environment(E,T)&greater(T,critical_point(E)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp4_critical_point)).
% 0.66/0.93 fof(c47,plain,(![P]:((~observational_period(P)|~slow_change(P))|(![E]:((~environment(E)|~in_environment(P,E))|(?[T]:(in_environment(E,T)&greater(T,critical_point(E)))))))),inference(fof_nnf,[status(thm)],[mp4_critical_point])).
% 0.66/0.93 fof(c48,plain,(![X19]:((~observational_period(X19)|~slow_change(X19))|(![X20]:((~environment(X20)|~in_environment(X19,X20))|(?[X21]:(in_environment(X20,X21)&greater(X21,critical_point(X20)))))))),inference(variable_rename,[status(thm)],[c47])).
% 0.66/0.93 fof(c50,plain,(![X19]:(![X20]:((~observational_period(X19)|~slow_change(X19))|((~environment(X20)|~in_environment(X19,X20))|(in_environment(X20,skolem0002(X19,X20))&greater(skolem0002(X19,X20),critical_point(X20))))))),inference(shift_quantors,[status(thm)],[fof(c49,plain,(![X19]:((~observational_period(X19)|~slow_change(X19))|(![X20]:((~environment(X20)|~in_environment(X19,X20))|(in_environment(X20,skolem0002(X19,X20))&greater(skolem0002(X19,X20),critical_point(X20))))))),inference(skolemize,[status(esa)],[c48])).])).
% 0.66/0.93 fof(c51,plain,(![X19]:(![X20]:(((~observational_period(X19)|~slow_change(X19))|((~environment(X20)|~in_environment(X19,X20))|in_environment(X20,skolem0002(X19,X20))))&((~observational_period(X19)|~slow_change(X19))|((~environment(X20)|~in_environment(X19,X20))|greater(skolem0002(X19,X20),critical_point(X20))))))),inference(distribute,[status(thm)],[c50])).
% 0.66/0.93 cnf(c52,plain,~observational_period(X102)|~slow_change(X102)|~environment(X101)|~in_environment(X102,X101)|in_environment(X101,skolem0002(X102,X101)),inference(split_conjunct,[status(thm)],[c51])).
% 0.66/0.93 cnf(c59,plain,~observational_period(X110)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)|in_environment(X110,skolem0003(X110))|selection_favors(efficient_producers,first_movers,X110),inference(split_conjunct,[status(thm)],[c57])).
% 0.66/0.93 cnf(c86,plain,~observational_period(X111)|~propagation_strategy(first_movers)|in_environment(X111,skolem0003(X111))|selection_favors(efficient_producers,first_movers,X111),inference(resolution,[status(thm)],[c59, c45])).
% 0.66/0.93 cnf(c89,plain,~observational_period(X112)|in_environment(X112,skolem0003(X112))|selection_favors(efficient_producers,first_movers,X112),inference(resolution,[status(thm)],[c86, c46])).
% 0.66/0.93 cnf(c90,plain,in_environment(skolem0001,skolem0003(skolem0001))|selection_favors(efficient_producers,first_movers,skolem0001),inference(resolution,[status(thm)],[c89, c15])).
% 0.66/0.93 cnf(c95,plain,in_environment(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c90, c17])).
% 0.66/0.93 cnf(c99,plain,~observational_period(skolem0001)|~slow_change(skolem0001)|~environment(skolem0003(skolem0001))|in_environment(skolem0003(skolem0001),skolem0002(skolem0001,skolem0003(skolem0001))),inference(resolution,[status(thm)],[c95, c52])).
% 0.66/0.93 cnf(c122,plain,~observational_period(skolem0001)|~slow_change(skolem0001)|in_environment(skolem0003(skolem0001),skolem0002(skolem0001,skolem0003(skolem0001))),inference(resolution,[status(thm)],[c99, c83])).
% 0.66/0.93 cnf(c123,plain,~observational_period(skolem0001)|in_environment(skolem0003(skolem0001),skolem0002(skolem0001,skolem0003(skolem0001))),inference(resolution,[status(thm)],[c122, c16])).
% 0.66/0.93 cnf(c124,plain,in_environment(skolem0003(skolem0001),skolem0002(skolem0001,skolem0003(skolem0001))),inference(resolution,[status(thm)],[c123, c15])).
% 0.66/0.93 cnf(c126,plain,skolem0003(skolem0001)!=X128|skolem0002(skolem0001,skolem0003(skolem0001))!=X129|in_environment(X128,X129),inference(resolution,[status(thm)],[c124, c7])).
% 0.66/0.93 cnf(symmetry,axiom,X25!=X26|X26=X25,theory(equality)).
% 0.66/0.93 fof(mp_greater_transitivity,axiom,(![X]:(![Y]:(![Z]:((greater(X,Y)&greater(Y,Z))=>greater(X,Z))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_greater_transitivity)).
% 0.66/0.93 fof(c33,plain,(![X]:(![Y]:(![Z]:((~greater(X,Y)|~greater(Y,Z))|greater(X,Z))))),inference(fof_nnf,[status(thm)],[mp_greater_transitivity])).
% 0.66/0.93 fof(c34,plain,(![X11]:(![X12]:(![X13]:((~greater(X11,X12)|~greater(X12,X13))|greater(X11,X13))))),inference(variable_rename,[status(thm)],[c33])).
% 0.66/0.93 cnf(c35,plain,~greater(X72,X70)|~greater(X70,X71)|greater(X72,X71),inference(split_conjunct,[status(thm)],[c34])).
% 0.66/0.93 cnf(c9,axiom,X82!=X80|X81!=X83|~greater(X82,X81)|greater(X80,X83),theory(equality)).
% 0.66/0.93 cnf(c53,plain,~observational_period(X106)|~slow_change(X106)|~environment(X105)|~in_environment(X106,X105)|greater(skolem0002(X106,X105),critical_point(X105)),inference(split_conjunct,[status(thm)],[c51])).
% 0.66/0.93 cnf(c97,plain,~observational_period(skolem0001)|~slow_change(skolem0001)|~environment(skolem0003(skolem0001))|greater(skolem0002(skolem0001,skolem0003(skolem0001)),critical_point(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c95, c53])).
% 0.66/0.93 cnf(c138,plain,~observational_period(skolem0001)|~slow_change(skolem0001)|greater(skolem0002(skolem0001,skolem0003(skolem0001)),critical_point(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c97, c83])).
% 0.66/0.93 cnf(c139,plain,~observational_period(skolem0001)|greater(skolem0002(skolem0001,skolem0003(skolem0001)),critical_point(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c138, c16])).
% 0.66/0.93 cnf(c140,plain,greater(skolem0002(skolem0001,skolem0003(skolem0001)),critical_point(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c139, c15])).
% 0.66/0.93 cnf(c144,plain,skolem0002(skolem0001,skolem0003(skolem0001))!=X136|critical_point(skolem0003(skolem0001))!=X137|greater(X136,X137),inference(resolution,[status(thm)],[c140, c9])).
% 0.66/0.93 cnf(c148,plain,critical_point(skolem0003(skolem0001))!=X138|greater(skolem0002(skolem0001,skolem0003(skolem0001)),X138),inference(resolution,[status(thm)],[c144, reflexivity])).
% 0.66/0.93 cnf(c30,plain,~greater_or_equal(X67,X68)|greater(X67,X68)|X67=X68,inference(split_conjunct,[status(thm)],[c29])).
% 0.66/0.93 fof(mp_time_of_critical_point,axiom,(![E]:(environment(E)=>greater_or_equal(critical_point(E),start_time(E)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_time_of_critical_point)).
% 0.66/0.93 fof(c36,plain,(![E]:(~environment(E)|greater_or_equal(critical_point(E),start_time(E)))),inference(fof_nnf,[status(thm)],[mp_time_of_critical_point])).
% 0.66/0.93 fof(c37,plain,(![X14]:(~environment(X14)|greater_or_equal(critical_point(X14),start_time(X14)))),inference(variable_rename,[status(thm)],[c36])).
% 0.66/0.93 cnf(c38,plain,~environment(X57)|greater_or_equal(critical_point(X57),start_time(X57)),inference(split_conjunct,[status(thm)],[c37])).
% 0.66/0.93 cnf(c85,plain,greater_or_equal(critical_point(skolem0003(skolem0001)),start_time(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c83, c38])).
% 0.66/0.93 cnf(c87,plain,greater(critical_point(skolem0003(skolem0001)),start_time(skolem0003(skolem0001)))|critical_point(skolem0003(skolem0001))=start_time(skolem0003(skolem0001)),inference(resolution,[status(thm)],[c85, c30])).
% 0.66/0.93 cnf(c105,plain,critical_point(skolem0003(skolem0001))=start_time(skolem0003(skolem0001))|~greater(X135,critical_point(skolem0003(skolem0001)))|greater(X135,start_time(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c87, c35])).
% 0.66/0.93 cnf(c147,plain,critical_point(skolem0003(skolem0001))=start_time(skolem0003(skolem0001))|greater(skolem0002(skolem0001,skolem0003(skolem0001)),start_time(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c105, c140])).
% 0.66/0.93 cnf(c183,plain,greater(skolem0002(skolem0001,skolem0003(skolem0001)),start_time(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c147, c148])).
% 0.66/0.93 cnf(c199,plain,~greater(X145,skolem0002(skolem0001,skolem0003(skolem0001)))|greater(X145,start_time(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c183, c35])).
% 0.66/0.93 fof(mp_environment_end_point,axiom,(![E]:(![T]:((environment(E)&in_environment(E,T))=>greater_or_equal(end_time(E),T)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mp_environment_end_point)).
% 0.66/0.93 fof(c39,plain,(![E]:(![T]:((~environment(E)|~in_environment(E,T))|greater_or_equal(end_time(E),T)))),inference(fof_nnf,[status(thm)],[mp_environment_end_point])).
% 0.66/0.93 fof(c40,plain,(![X15]:(![X16]:((~environment(X15)|~in_environment(X15,X16))|greater_or_equal(end_time(X15),X16)))),inference(variable_rename,[status(thm)],[c39])).
% 0.66/0.93 cnf(c41,plain,~environment(X74)|~in_environment(X74,X75)|greater_or_equal(end_time(X74),X75),inference(split_conjunct,[status(thm)],[c40])).
% 0.66/0.93 cnf(c128,plain,~environment(skolem0003(skolem0001))|greater_or_equal(end_time(skolem0003(skolem0001)),skolem0002(skolem0001,skolem0003(skolem0001))),inference(resolution,[status(thm)],[c124, c41])).
% 0.66/0.93 cnf(c132,plain,greater_or_equal(end_time(skolem0003(skolem0001)),skolem0002(skolem0001,skolem0003(skolem0001))),inference(resolution,[status(thm)],[c128, c83])).
% 0.66/0.93 cnf(c134,plain,greater(end_time(skolem0003(skolem0001)),skolem0002(skolem0001,skolem0003(skolem0001)))|end_time(skolem0003(skolem0001))=skolem0002(skolem0001,skolem0003(skolem0001)),inference(resolution,[status(thm)],[c132, c30])).
% 0.66/0.93 cnf(c263,plain,end_time(skolem0003(skolem0001))=skolem0002(skolem0001,skolem0003(skolem0001))|greater(end_time(skolem0003(skolem0001)),start_time(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c134, c199])).
% 0.66/0.93 cnf(c279,plain,greater(end_time(skolem0003(skolem0001)),start_time(skolem0003(skolem0001)))|skolem0002(skolem0001,skolem0003(skolem0001))=end_time(skolem0003(skolem0001)),inference(resolution,[status(thm)],[c263, symmetry])).
% 0.66/0.93 cnf(c321,plain,greater(end_time(skolem0003(skolem0001)),start_time(skolem0003(skolem0001)))|skolem0003(skolem0001)!=X153|in_environment(X153,end_time(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c279, c126])).
% 0.66/0.93 cnf(c427,plain,greater(end_time(skolem0003(skolem0001)),start_time(skolem0003(skolem0001)))|in_environment(skolem0003(skolem0001),end_time(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c321, reflexivity])).
% 0.66/0.93 cnf(c429,plain,in_environment(skolem0003(skolem0001),end_time(skolem0003(skolem0001)))|greater_or_equal(end_time(skolem0003(skolem0001)),start_time(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c427, c31])).
% 0.66/0.93 cnf(c442,plain,in_environment(skolem0003(skolem0001),end_time(skolem0003(skolem0001)))|~environment(skolem0003(skolem0001)),inference(resolution,[status(thm)],[c429, c78])).
% 0.66/0.93 cnf(c444,plain,in_environment(skolem0003(skolem0001),end_time(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c442, c83])).
% 0.66/0.93 fof(l8,plain,(![E]:(![T]:(((environment(E)&in_environment(E,T))&greater(T,critical_point(E)))=>selection_favors(efficient_producers,first_movers,T)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l8)).
% 0.66/0.93 fof(c18,plain,(![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)],[l8])).
% 0.66/0.93 fof(c19,plain,(![X3]:(![X4]:(((~environment(X3)|~in_environment(X3,X4))|~greater(X4,critical_point(X3)))|selection_favors(efficient_producers,first_movers,X4)))),inference(variable_rename,[status(thm)],[c18])).
% 0.66/0.93 cnf(c20,plain,~environment(X95)|~in_environment(X95,X96)|~greater(X96,critical_point(X95))|selection_favors(efficient_producers,first_movers,X96),inference(split_conjunct,[status(thm)],[c19])).
% 0.66/0.93 cnf(c141,plain,~greater(X134,skolem0002(skolem0001,skolem0003(skolem0001)))|greater(X134,critical_point(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c140, c35])).
% 0.66/0.93 cnf(c265,plain,end_time(skolem0003(skolem0001))=skolem0002(skolem0001,skolem0003(skolem0001))|greater(end_time(skolem0003(skolem0001)),critical_point(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c134, c141])).
% 0.66/0.93 cnf(c296,plain,greater(end_time(skolem0003(skolem0001)),critical_point(skolem0003(skolem0001)))|skolem0002(skolem0001,skolem0003(skolem0001))=end_time(skolem0003(skolem0001)),inference(resolution,[status(thm)],[c265, symmetry])).
% 0.66/0.93 cnf(c376,plain,greater(end_time(skolem0003(skolem0001)),critical_point(skolem0003(skolem0001)))|critical_point(skolem0003(skolem0001))!=X210|greater(end_time(skolem0003(skolem0001)),X210),inference(resolution,[status(thm)],[c296, c144])).
% 0.66/0.93 cnf(c863,plain,greater(end_time(skolem0003(skolem0001)),critical_point(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c376, reflexivity])).
% 0.66/0.93 cnf(c868,plain,~environment(skolem0003(skolem0001))|~in_environment(skolem0003(skolem0001),end_time(skolem0003(skolem0001)))|selection_favors(efficient_producers,first_movers,end_time(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c863, c20])).
% 0.66/0.93 cnf(c908,plain,~environment(skolem0003(skolem0001))|selection_favors(efficient_producers,first_movers,end_time(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c868, c444])).
% 0.66/0.93 cnf(c909,plain,selection_favors(efficient_producers,first_movers,end_time(skolem0003(skolem0001))),inference(resolution,[status(thm)],[c908, c83])).
% 0.66/0.93 cnf(c911,plain,~observational_period(skolem0001)|~propagation_strategy(first_movers)|~propagation_strategy(efficient_producers)|selection_favors(efficient_producers,first_movers,skolem0001),inference(resolution,[status(thm)],[c909, c60])).
% 0.66/0.93 cnf(c912,plain,~observational_period(skolem0001)|~propagation_strategy(first_movers)|selection_favors(efficient_producers,first_movers,skolem0001),inference(resolution,[status(thm)],[c911, c45])).
% 0.66/0.93 cnf(c915,plain,~observational_period(skolem0001)|selection_favors(efficient_producers,first_movers,skolem0001),inference(resolution,[status(thm)],[c912, c46])).
% 0.66/0.93 cnf(c916,plain,selection_favors(efficient_producers,first_movers,skolem0001),inference(resolution,[status(thm)],[c915, c15])).
% 0.66/0.93 cnf(c917,plain,$false,inference(resolution,[status(thm)],[c916, c17])).
% 0.66/0.93 % SZS output end CNFRefutation
% 0.66/0.93
% 0.66/0.93 % Initial clauses : 33
% 0.66/0.93 % Processed clauses : 218
% 0.66/0.93 % Factors computed : 3
% 0.66/0.93 % Resolvents computed: 855
% 0.66/0.93 % Tautologies deleted: 7
% 0.66/0.93 % Forward subsumed : 162
% 0.66/0.93 % Backward subsumed : 79
% 0.66/0.93 % -------- CPU Time ---------
% 0.66/0.93 % User time : 0.557 s
% 0.66/0.93 % System time : 0.023 s
% 0.66/0.93 % Total time : 0.580 s
%------------------------------------------------------------------------------