%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT027-1 : TPTP v9.3.0. Released v2.4.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 : Unsatisfiable 12.36s 12.62s
% Output : CNFRefutation 12.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 18
% Syntax : Number of clauses : 63 ( 17 unt; 12 nHn; 62 RR)
% Number of literals : 158 ( 12 equ; 85 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 40 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_l9_39,negated_conjecture,
( ~ greater(X42,appear(efficient_producers,sk3))
| ~ contracts_from(X42,first_movers) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l9_39) ).
cnf(prove_l9_37,negated_conjecture,
environment(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l9_37) ).
cnf(prove_l9_38,negated_conjecture,
stable(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_l9_38) ).
cnf(l10_35,plain,
( ~ environment(X46)
| ~ stable(X46)
| greater(sk2(X46),appear(efficient_producers,X46)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l10_35) ).
cnf(c25,plain,
( ~ environment(sk3)
| greater(sk2(sk3),appear(efficient_producers,sk3)) ),
inference(resolution,[status(thm)],[l10_35,prove_l9_38]) ).
cnf(c32,plain,
greater(sk2(sk3),appear(efficient_producers,sk3)),
inference(resolution,[status(thm)],[c25,prove_l9_37]) ).
cnf(c35,plain,
~ contracts_from(sk2(sk3),first_movers),
inference(resolution,[status(thm)],[c32,prove_l9_39]) ).
cnf(mp_EP_in_stable_environments_29,axiom,
( ~ environment(X41)
| ~ stable(X41)
| in_environment(X41,appear(efficient_producers,X41)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_EP_in_stable_environments_29) ).
cnf(c21,plain,
( ~ environment(sk3)
| in_environment(sk3,appear(efficient_producers,sk3)) ),
inference(resolution,[status(thm)],[mp_EP_in_stable_environments_29,prove_l9_38]) ).
cnf(c22,plain,
in_environment(sk3,appear(efficient_producers,sk3)),
inference(resolution,[status(thm)],[c21,prove_l9_37]) ).
cnf(mp_long_stable_environments_28,axiom,
( ~ environment(X43)
| ~ stable(X43)
| ~ in_environment(X43,X44)
| ~ greater(X45,X44)
| in_environment(X43,X45) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_long_stable_environments_28) ).
cnf(c36,plain,
( ~ environment(X141)
| ~ stable(X141)
| ~ in_environment(X141,appear(efficient_producers,sk3))
| in_environment(X141,sk2(sk3)) ),
inference(resolution,[status(thm)],[c32,mp_long_stable_environments_28]) ).
cnf(c65,plain,
( ~ environment(sk3)
| ~ stable(sk3)
| in_environment(sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[c36,c22]) ).
cnf(c66,plain,
( ~ environment(sk3)
| in_environment(sk3,sk2(sk3)) ),
inference(resolution,[status(thm)],[c65,prove_l9_38]) ).
cnf(c67,plain,
in_environment(sk3,sk2(sk3)),
inference(resolution,[status(thm)],[c66,prove_l9_37]) ).
cnf(mp_contracts_from_26,axiom,
( ~ environment(X27)
| ~ stable(X27)
| ~ in_environment(X27,X28)
| ~ greater(zero,growth_rate(first_movers,sk1(X28,X27)))
| contracts_from(X28,first_movers) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_contracts_from_26) ).
cnf(mp_contracts_from_25,axiom,
( ~ environment(X16)
| ~ stable(X16)
| ~ in_environment(X16,X17)
| greater_or_equal(sk1(X17,X16),X17)
| contracts_from(X17,first_movers) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_contracts_from_25) ).
cnf(c68,plain,
( ~ environment(sk3)
| ~ stable(sk3)
| greater_or_equal(sk1(sk2(sk3),sk3),sk2(sk3))
| contracts_from(sk2(sk3),first_movers) ),
inference(resolution,[status(thm)],[c67,mp_contracts_from_25]) ).
cnf(c101,plain,
( ~ environment(sk3)
| greater_or_equal(sk1(sk2(sk3),sk3),sk2(sk3))
| contracts_from(sk2(sk3),first_movers) ),
inference(resolution,[status(thm)],[c68,prove_l9_38]) ).
cnf(c102,plain,
( greater_or_equal(sk1(sk2(sk3),sk3),sk2(sk3))
| contracts_from(sk2(sk3),first_movers) ),
inference(resolution,[status(thm)],[c101,prove_l9_37]) ).
cnf(c105,plain,
greater_or_equal(sk1(sk2(sk3),sk3),sk2(sk3)),
inference(resolution,[status(thm)],[c102,c35]) ).
cnf(l10_36,plain,
( ~ environment(X73)
| ~ stable(X73)
| ~ subpopulations(first_movers,efficient_producers,X73,X74)
| ~ greater_or_equal(X74,sk2(X73))
| greater(zero,growth_rate(first_movers,X74)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l10_36) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c8,axiom,
( X54 != X52
| X51 != X53
| ~ greater(X54,X51)
| greater(X52,X53) ),
theory(equality) ).
cnf(c34,plain,
( sk2(sk3) != X135
| appear(efficient_producers,sk3) != X136
| greater(X135,X136) ),
inference(resolution,[status(thm)],[c32,c8]) ).
cnf(c59,plain,
( sk2(sk3) != X137
| greater(X137,appear(efficient_producers,sk3)) ),
inference(resolution,[status(thm)],[c34,reflexivity]) ).
cnf(mp_greater_transitivity_30,axiom,
( ~ greater(X21,X22)
| ~ greater(X22,X23)
| greater(X21,X23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_transitivity_30) ).
cnf(c33,plain,
( ~ greater(X75,sk2(sk3))
| greater(X75,appear(efficient_producers,sk3)) ),
inference(resolution,[status(thm)],[c32,mp_greater_transitivity_30]) ).
cnf(symmetry,axiom,
( X10 != X11
| X11 = X10 ),
theory(equality) ).
cnf(mp_greater_or_equal_31,axiom,
( ~ greater_or_equal(X25,X26)
| greater(X25,X26)
| X25 = X26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_31) ).
cnf(c108,plain,
( greater(sk1(sk2(sk3),sk3),sk2(sk3))
| sk1(sk2(sk3),sk3) = sk2(sk3) ),
inference(resolution,[status(thm)],[c105,mp_greater_or_equal_31]) ).
cnf(c127,plain,
( greater(sk1(sk2(sk3),sk3),sk2(sk3))
| sk2(sk3) = sk1(sk2(sk3),sk3) ),
inference(resolution,[status(thm)],[c108,symmetry]) ).
cnf(c168,plain,
( sk2(sk3) = sk1(sk2(sk3),sk3)
| greater(sk1(sk2(sk3),sk3),appear(efficient_producers,sk3)) ),
inference(resolution,[status(thm)],[c127,c33]) ).
cnf(c249,plain,
greater(sk1(sk2(sk3),sk3),appear(efficient_producers,sk3)),
inference(resolution,[status(thm)],[c168,c59]) ).
cnf(c289,plain,
( ~ environment(X192)
| ~ stable(X192)
| ~ in_environment(X192,appear(efficient_producers,sk3))
| in_environment(X192,sk1(sk2(sk3),sk3)) ),
inference(resolution,[status(thm)],[c249,mp_long_stable_environments_28]) ).
cnf(c301,plain,
( ~ environment(sk3)
| ~ stable(sk3)
| in_environment(sk3,sk1(sk2(sk3),sk3)) ),
inference(resolution,[status(thm)],[c289,c22]) ).
cnf(c302,plain,
( ~ environment(sk3)
| in_environment(sk3,sk1(sk2(sk3),sk3)) ),
inference(resolution,[status(thm)],[c301,prove_l9_38]) ).
cnf(c303,plain,
in_environment(sk3,sk1(sk2(sk3),sk3)),
inference(resolution,[status(thm)],[c302,prove_l9_37]) ).
cnf(mp_contracts_from_24,axiom,
( ~ environment(X7)
| ~ stable(X7)
| ~ in_environment(X7,X8)
| greater(cardinality_at_time(first_movers,sk1(X8,X7)),zero)
| contracts_from(X8,first_movers) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_contracts_from_24) ).
cnf(c69,plain,
( ~ environment(sk3)
| ~ stable(sk3)
| greater(cardinality_at_time(first_movers,sk1(sk2(sk3),sk3)),zero)
| contracts_from(sk2(sk3),first_movers) ),
inference(resolution,[status(thm)],[c67,mp_contracts_from_24]) ).
cnf(c111,plain,
( ~ environment(sk3)
| greater(cardinality_at_time(first_movers,sk1(sk2(sk3),sk3)),zero)
| contracts_from(sk2(sk3),first_movers) ),
inference(resolution,[status(thm)],[c69,prove_l9_38]) ).
cnf(c147,plain,
( greater(cardinality_at_time(first_movers,sk1(sk2(sk3),sk3)),zero)
| contracts_from(sk2(sk3),first_movers) ),
inference(resolution,[status(thm)],[c111,prove_l9_37]) ).
cnf(c152,plain,
greater(cardinality_at_time(first_movers,sk1(sk2(sk3),sk3)),zero),
inference(resolution,[status(thm)],[c147,c35]) ).
cnf(mp_non_empty_fm_and_ep_27,axiom,
( ~ environment(X38)
| ~ in_environment(X38,X39)
| ~ greater(cardinality_at_time(first_movers,X39),zero)
| ~ greater(cardinality_at_time(efficient_producers,X39),zero)
| subpopulations(first_movers,efficient_producers,X38,X39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_non_empty_fm_and_ep_27) ).
cnf(t6_34,plain,
( ~ environment(X63)
| ~ in_environment(X63,X64)
| ~ greater_or_equal(X64,appear(efficient_producers,X63))
| greater(cardinality_at_time(efficient_producers,X64),zero) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_34) ).
cnf(mp_greater_or_equal_32,axiom,
( ~ greater(X3,X4)
| greater_or_equal(X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_32) ).
cnf(c290,plain,
greater_or_equal(sk1(sk2(sk3),sk3),appear(efficient_producers,sk3)),
inference(resolution,[status(thm)],[c249,mp_greater_or_equal_32]) ).
cnf(c293,plain,
( ~ environment(sk3)
| ~ in_environment(sk3,sk1(sk2(sk3),sk3))
| greater(cardinality_at_time(efficient_producers,sk1(sk2(sk3),sk3)),zero) ),
inference(resolution,[status(thm)],[c290,t6_34]) ).
cnf(c461,plain,
( ~ environment(sk3)
| greater(cardinality_at_time(efficient_producers,sk1(sk2(sk3),sk3)),zero) ),
inference(resolution,[status(thm)],[c293,c303]) ).
cnf(c462,plain,
greater(cardinality_at_time(efficient_producers,sk1(sk2(sk3),sk3)),zero),
inference(resolution,[status(thm)],[c461,prove_l9_37]) ).
cnf(c463,plain,
( ~ environment(X1115)
| ~ in_environment(X1115,sk1(sk2(sk3),sk3))
| ~ greater(cardinality_at_time(first_movers,sk1(sk2(sk3),sk3)),zero)
| subpopulations(first_movers,efficient_producers,X1115,sk1(sk2(sk3),sk3)) ),
inference(resolution,[status(thm)],[c462,mp_non_empty_fm_and_ep_27]) ).
cnf(c9068,plain,
( ~ environment(X1116)
| ~ in_environment(X1116,sk1(sk2(sk3),sk3))
| subpopulations(first_movers,efficient_producers,X1116,sk1(sk2(sk3),sk3)) ),
inference(resolution,[status(thm)],[c463,c152]) ).
cnf(c9069,plain,
( ~ environment(sk3)
| subpopulations(first_movers,efficient_producers,sk3,sk1(sk2(sk3),sk3)) ),
inference(resolution,[status(thm)],[c9068,c303]) ).
cnf(c9070,plain,
subpopulations(first_movers,efficient_producers,sk3,sk1(sk2(sk3),sk3)),
inference(resolution,[status(thm)],[c9069,prove_l9_37]) ).
cnf(c9072,plain,
( ~ environment(sk3)
| ~ stable(sk3)
| ~ greater_or_equal(sk1(sk2(sk3),sk3),sk2(sk3))
| greater(zero,growth_rate(first_movers,sk1(sk2(sk3),sk3))) ),
inference(resolution,[status(thm)],[c9070,l10_36]) ).
cnf(c9080,plain,
( ~ environment(sk3)
| ~ stable(sk3)
| greater(zero,growth_rate(first_movers,sk1(sk2(sk3),sk3))) ),
inference(resolution,[status(thm)],[c9072,c105]) ).
cnf(c9081,plain,
( ~ environment(sk3)
| greater(zero,growth_rate(first_movers,sk1(sk2(sk3),sk3))) ),
inference(resolution,[status(thm)],[c9080,prove_l9_38]) ).
cnf(c9082,plain,
greater(zero,growth_rate(first_movers,sk1(sk2(sk3),sk3))),
inference(resolution,[status(thm)],[c9081,prove_l9_37]) ).
cnf(c9087,plain,
( ~ environment(sk3)
| ~ stable(sk3)
| ~ in_environment(sk3,sk2(sk3))
| contracts_from(sk2(sk3),first_movers) ),
inference(resolution,[status(thm)],[c9082,mp_contracts_from_26]) ).
cnf(c9106,plain,
( ~ environment(sk3)
| ~ stable(sk3)
| contracts_from(sk2(sk3),first_movers) ),
inference(resolution,[status(thm)],[c9087,c67]) ).
cnf(c9111,plain,
( ~ environment(sk3)
| contracts_from(sk2(sk3),first_movers) ),
inference(resolution,[status(thm)],[c9106,prove_l9_38]) ).
cnf(c9112,plain,
contracts_from(sk2(sk3),first_movers),
inference(resolution,[status(thm)],[c9111,prove_l9_37]) ).
cnf(c9114,plain,
$false,
inference(resolution,[status(thm)],[c9112,c35]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : MGT027-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.06 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.43 % Computer : n018.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Mon Sep 7 12:15:52 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.27/0.53 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.27/0.53 (re.compile("\."), Token.FullStop),
% 0.27/0.53 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.27/0.53 (re.compile("\("), Token.OpenPar),
% 0.27/0.53 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.27/0.53 (re.compile("\)"), Token.ClosePar),
% 0.27/0.53 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.27/0.53 (re.compile("\["), Token.OpenSquare),
% 0.27/0.53 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.27/0.53 (re.compile("\]"), Token.CloseSquare),
% 0.27/0.53 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.27/0.53 (re.compile("~\|"), Token.Nor),
% 0.27/0.53 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.27/0.53 (re.compile("\|"), Token.Or),
% 0.27/0.53 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.27/0.53 (re.compile("\?"), Token.Existential),
% 0.27/0.53 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.27/0.53 (re.compile("\s+"), Token.WhiteSpace),
% 0.27/0.53 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.27/0.53 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.37/0.64 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.37/0.64 """
% 0.37/0.64 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.37/0.64 """
% 0.56/0.80 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.56/0.80 """
% 12.36/12.62 % Version: 1.5
% 12.36/12.62 % SZS status Unsatisfiable
% 12.36/12.62 % SZS output start CNFRefutation
% See solution above
% 12.36/12.62
% 12.36/12.62 % Initial clauses : 31
% 12.36/12.62 % Processed clauses : 662
% 12.36/12.62 % Factors computed : 7
% 12.36/12.62 % Resolvents computed: 9096
% 12.36/12.62 % Tautologies deleted: 5
% 12.36/12.62 % Forward subsumed : 632
% 12.36/12.62 % Backward subsumed : 39
% 12.36/12.62 % -------- CPU Time ---------
% 12.36/12.62 % User time : 12.092 s
% 12.36/12.62 % System time : 0.088 s
% 12.36/12.62 % Total time : 12.180 s
%------------------------------------------------------------------------------