%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT026-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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 29.15s 29.49s
% Output : CNFRefutation 29.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 18
% Syntax : Number of clauses : 54 ( 17 unt; 11 nHn; 53 RR)
% Number of literals : 133 ( 12 equ; 69 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-4 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 45 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_l8_45,negated_conjecture,
~ selection_favors(efficient_producers,first_movers,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l8_45) ).
cnf(prove_l8_42,negated_conjecture,
environment(sk1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l8_42) ).
cnf(prove_l8_43,negated_conjecture,
in_environment(sk1,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l8_43) ).
cnf(mp_non_empty_fm_and_ep_30,axiom,
( ~ environment(X26)
| ~ in_environment(X26,X27)
| ~ greater(cardinality_at_time(first_movers,X27),zero)
| ~ greater(cardinality_at_time(efficient_producers,X27),zero)
| subpopulations(first_movers,efficient_producers,X26,X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_non_empty_fm_and_ep_30) ).
cnf(t6_41,plain,
( ~ environment(X73)
| ~ in_environment(X73,X74)
| ~ greater_or_equal(X74,appear(efficient_producers,X73))
| greater(cardinality_at_time(efficient_producers,X74),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_41) ).
cnf(mp_greater_or_equal_37,axiom,
( ~ greater(X3,X4)
| greater_or_equal(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_37) ).
cnf(prove_l8_44,negated_conjecture,
greater(sk2,critical_point(sk1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l8_44) ).
cnf(mp_greater_transitivity_35,axiom,
( ~ greater(X22,X23)
| ~ greater(X23,X24)
| greater(X22,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_transitivity_35) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c6,axiom,
( X50 != X51
| X53 != X52
| ~ greater(X50,X53)
| greater(X51,X52) ),
theory(equality) ).
cnf(c31,plain,
( sk2 != X79
| critical_point(sk1) != X78
| greater(X79,X78) ),
inference(resolution,[status(thm)],[c6,prove_l8_44]) ).
cnf(mp_greater_or_equal_36,axiom,
( ~ greater_or_equal(X28,X29)
| greater(X28,X29)
| X28 = X29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_36) ).
cnf(mp_critical_point_after_EP_34,axiom,
( ~ environment(X47)
| greater_or_equal(critical_point(X47),appear(efficient_producers,X47)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_critical_point_after_EP_34) ).
cnf(c27,plain,
greater_or_equal(critical_point(sk1),appear(efficient_producers,sk1)),
inference(resolution,[status(thm)],[mp_critical_point_after_EP_34,prove_l8_42]) ).
cnf(c28,plain,
( greater(critical_point(sk1),appear(efficient_producers,sk1))
| critical_point(sk1) = appear(efficient_producers,sk1) ),
inference(resolution,[status(thm)],[c27,mp_greater_or_equal_36]) ).
cnf(c117,plain,
( greater(critical_point(sk1),appear(efficient_producers,sk1))
| sk2 != X182
| greater(X182,appear(efficient_producers,sk1)) ),
inference(resolution,[status(thm)],[c28,c31]) ).
cnf(c444,plain,
( greater(critical_point(sk1),appear(efficient_producers,sk1))
| greater(sk2,appear(efficient_producers,sk1)) ),
inference(resolution,[status(thm)],[c117,reflexivity]) ).
cnf(c447,plain,
( greater(sk2,appear(efficient_producers,sk1))
| ~ greater(X222,critical_point(sk1))
| greater(X222,appear(efficient_producers,sk1)) ),
inference(resolution,[status(thm)],[c444,mp_greater_transitivity_35]) ).
cnf(c692,plain,
greater(sk2,appear(efficient_producers,sk1)),
inference(resolution,[status(thm)],[c447,prove_l8_44]) ).
cnf(c693,plain,
greater_or_equal(sk2,appear(efficient_producers,sk1)),
inference(resolution,[status(thm)],[c692,mp_greater_or_equal_37]) ).
cnf(c698,plain,
( ~ environment(sk1)
| ~ in_environment(sk1,sk2)
| greater(cardinality_at_time(efficient_producers,sk2),zero) ),
inference(resolution,[status(thm)],[c693,t6_41]) ).
cnf(c707,plain,
( ~ environment(sk1)
| greater(cardinality_at_time(efficient_producers,sk2),zero) ),
inference(resolution,[status(thm)],[c698,prove_l8_43]) ).
cnf(c708,plain,
greater(cardinality_at_time(efficient_producers,sk2),zero),
inference(resolution,[status(thm)],[c707,prove_l8_42]) ).
cnf(c715,plain,
( ~ environment(X302)
| ~ in_environment(X302,sk2)
| ~ greater(cardinality_at_time(first_movers,sk2),zero)
| subpopulations(first_movers,efficient_producers,X302,sk2) ),
inference(resolution,[status(thm)],[c708,mp_non_empty_fm_and_ep_30]) ).
cnf(mp_subpopulations_33,axiom,
( ~ environment(X45)
| ~ in_environment(X45,X46)
| subpopulation(efficient_producers,X45,X46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_subpopulations_33) ).
cnf(c25,plain,
( ~ environment(sk1)
| subpopulation(efficient_producers,sk1,sk2) ),
inference(resolution,[status(thm)],[mp_subpopulations_33,prove_l8_43]) ).
cnf(c26,plain,
subpopulation(efficient_producers,sk1,sk2),
inference(resolution,[status(thm)],[c25,prove_l8_42]) ).
cnf(mp_subpopulations_32,axiom,
( ~ environment(X43)
| ~ in_environment(X43,X44)
| subpopulation(first_movers,X43,X44) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_subpopulations_32) ).
cnf(c23,plain,
( ~ environment(sk1)
| subpopulation(first_movers,sk1,sk2) ),
inference(resolution,[status(thm)],[mp_subpopulations_32,prove_l8_43]) ).
cnf(c24,plain,
subpopulation(first_movers,sk1,sk2),
inference(resolution,[status(thm)],[c23,prove_l8_42]) ).
cnf(mp2_favour_members_29,axiom,
( ~ environment(X16)
| ~ subpopulation(X17,X16,X18)
| ~ subpopulation(X15,X16,X18)
| ~ greater(cardinality_at_time(X17,X18),zero)
| cardinality_at_time(X15,X18) != zero
| selection_favors(X17,X15,X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp2_favour_members_29) ).
cnf(mp_first_movers_exist_31,axiom,
( ~ environment(X37)
| ~ in_environment(X37,X38)
| greater_or_equal(cardinality_at_time(first_movers,X38),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_first_movers_exist_31) ).
cnf(c21,plain,
( ~ environment(sk1)
| greater_or_equal(cardinality_at_time(first_movers,sk2),zero) ),
inference(resolution,[status(thm)],[mp_first_movers_exist_31,prove_l8_43]) ).
cnf(c29,plain,
greater_or_equal(cardinality_at_time(first_movers,sk2),zero),
inference(resolution,[status(thm)],[c21,prove_l8_42]) ).
cnf(c30,plain,
( greater(cardinality_at_time(first_movers,sk2),zero)
| cardinality_at_time(first_movers,sk2) = zero ),
inference(resolution,[status(thm)],[c29,mp_greater_or_equal_36]) ).
cnf(c76,plain,
( greater(cardinality_at_time(first_movers,sk2),zero)
| ~ environment(X177)
| ~ subpopulation(X176,X177,sk2)
| ~ subpopulation(first_movers,X177,sk2)
| ~ greater(cardinality_at_time(X176,sk2),zero)
| selection_favors(X176,first_movers,sk2) ),
inference(resolution,[status(thm)],[c30,mp2_favour_members_29]) ).
cnf(c713,plain,
( greater(cardinality_at_time(first_movers,sk2),zero)
| ~ environment(X2648)
| ~ subpopulation(efficient_producers,X2648,sk2)
| ~ subpopulation(first_movers,X2648,sk2)
| selection_favors(efficient_producers,first_movers,sk2) ),
inference(resolution,[status(thm)],[c708,c76]) ).
cnf(c40002,plain,
( greater(cardinality_at_time(first_movers,sk2),zero)
| ~ environment(sk1)
| ~ subpopulation(efficient_producers,sk1,sk2)
| selection_favors(efficient_producers,first_movers,sk2) ),
inference(resolution,[status(thm)],[c713,c24]) ).
cnf(c40003,plain,
( greater(cardinality_at_time(first_movers,sk2),zero)
| ~ environment(sk1)
| selection_favors(efficient_producers,first_movers,sk2) ),
inference(resolution,[status(thm)],[c40002,c26]) ).
cnf(c40004,plain,
( greater(cardinality_at_time(first_movers,sk2),zero)
| selection_favors(efficient_producers,first_movers,sk2) ),
inference(resolution,[status(thm)],[c40003,prove_l8_42]) ).
cnf(c40010,plain,
greater(cardinality_at_time(first_movers,sk2),zero),
inference(resolution,[status(thm)],[c40004,prove_l8_45]) ).
cnf(c40014,plain,
( ~ environment(X2651)
| ~ in_environment(X2651,sk2)
| subpopulations(first_movers,efficient_producers,X2651,sk2) ),
inference(resolution,[status(thm)],[c40010,c715]) ).
cnf(c40017,plain,
( ~ environment(sk1)
| subpopulations(first_movers,efficient_producers,sk1,sk2) ),
inference(resolution,[status(thm)],[c40014,prove_l8_43]) ).
cnf(c40018,plain,
subpopulations(first_movers,efficient_producers,sk1,sk2),
inference(resolution,[status(thm)],[c40017,prove_l8_42]) ).
cnf(mp1_high_growth_rates_28,axiom,
( ~ environment(X8)
| ~ subpopulations(X9,X10,X8,X7)
| ~ greater(growth_rate(X10,X7),growth_rate(X9,X7))
| selection_favors(X10,X9,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp1_high_growth_rates_28) ).
cnf(d1_40,plain,
( ~ environment(X60)
| X61 != critical_point(X60)
| ~ subpopulations(first_movers,efficient_producers,X60,X62)
| ~ greater(X62,X61)
| greater(growth_rate(efficient_producers,X62),growth_rate(first_movers,X62)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_40) ).
cnf(c40020,plain,
( ~ environment(sk1)
| X2678 != critical_point(sk1)
| ~ greater(sk2,X2678)
| greater(growth_rate(efficient_producers,sk2),growth_rate(first_movers,sk2)) ),
inference(resolution,[status(thm)],[c40018,d1_40]) ).
cnf(c40031,plain,
( ~ environment(sk1)
| ~ greater(sk2,critical_point(sk1))
| greater(growth_rate(efficient_producers,sk2),growth_rate(first_movers,sk2)) ),
inference(resolution,[status(thm)],[c40020,reflexivity]) ).
cnf(c40057,plain,
( ~ environment(sk1)
| greater(growth_rate(efficient_producers,sk2),growth_rate(first_movers,sk2)) ),
inference(resolution,[status(thm)],[c40031,prove_l8_44]) ).
cnf(c40058,plain,
greater(growth_rate(efficient_producers,sk2),growth_rate(first_movers,sk2)),
inference(resolution,[status(thm)],[c40057,prove_l8_42]) ).
cnf(c40060,plain,
( ~ environment(X2684)
| ~ subpopulations(first_movers,efficient_producers,X2684,sk2)
| selection_favors(efficient_producers,first_movers,sk2) ),
inference(resolution,[status(thm)],[c40058,mp1_high_growth_rates_28]) ).
cnf(c40066,plain,
( ~ environment(sk1)
| selection_favors(efficient_producers,first_movers,sk2) ),
inference(resolution,[status(thm)],[c40060,c40018]) ).
cnf(c40067,plain,
selection_favors(efficient_producers,first_movers,sk2),
inference(resolution,[status(thm)],[c40066,prove_l8_42]) ).
cnf(c40068,plain,
$false,
inference(resolution,[status(thm)],[c40067,prove_l8_45]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT026-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.35 % Computer : n003.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 12:13:54 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.42 (re.compile("\."), Token.FullStop),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.42 (re.compile("\("), Token.OpenPar),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.42 (re.compile("\)"), Token.ClosePar),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.42 (re.compile("\["), Token.OpenSquare),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.42 (re.compile("~\|"), Token.Nor),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.42 (re.compile("\|"), Token.Or),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.42 (re.compile("\?"), Token.Existential),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.42 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.21/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.49 """
% 0.21/0.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.49 """
% 0.31/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.31/0.58 """
% 29.15/29.49 % Version: 1.5
% 29.15/29.49 % SZS status Unsatisfiable
% 29.15/29.49 % SZS output start CNFRefutation
% See solution above
% 29.15/29.49
% 29.15/29.49 % Initial clauses : 32
% 29.15/29.49 % Processed clauses : 1178
% 29.15/29.49 % Factors computed : 6
% 29.15/29.49 % Resolvents computed: 40053
% 29.15/29.49 % Tautologies deleted: 4
% 29.15/29.49 % Forward subsumed : 1348
% 29.15/29.49 % Backward subsumed : 996
% 29.15/29.49 % -------- CPU Time ---------
% 29.15/29.49 % User time : 28.954 s
% 29.15/29.49 % System time : 0.179 s
% 29.15/29.49 % Total time : 29.133 s
%------------------------------------------------------------------------------