%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT039-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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 : Unsatisfiable 0.66s 1.01s
% Output : CNFRefutation 0.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 22
% Syntax : Number of clauses : 72 ( 19 unt; 21 nHn; 70 RR)
% Number of literals : 173 ( 24 equ; 81 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 50 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_t8_38,negated_conjecture,
~ selection_favors(efficient_producers,first_movers,sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t8_38) ).
cnf(prove_t8_36,negated_conjecture,
observational_period(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t8_36) ).
cnf(mp_organizational_sets1_25,axiom,
propagation_strategy(first_movers),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_organizational_sets1_25) ).
cnf(mp_organizational_sets2_26,axiom,
propagation_strategy(efficient_producers),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_organizational_sets2_26) ).
cnf(mp3_favoured_trategy_22,axiom,
( ~ observational_period(X19)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| ~ selection_favors(efficient_producers,first_movers,end_time(sk1(X19)))
| selection_favors(efficient_producers,first_movers,X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp3_favoured_trategy_22) ).
cnf(mp3_favoured_trategy_20,axiom,
( ~ observational_period(X3)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| environment(sk1(X3))
| selection_favors(efficient_producers,first_movers,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp3_favoured_trategy_20) ).
cnf(c13,plain,
( ~ observational_period(X97)
| ~ propagation_strategy(first_movers)
| environment(sk1(X97))
| selection_favors(efficient_producers,first_movers,X97) ),
inference(resolution,[status(thm)],[mp3_favoured_trategy_20,mp_organizational_sets2_26]) ).
cnf(c38,plain,
( ~ observational_period(X98)
| environment(sk1(X98))
| selection_favors(efficient_producers,first_movers,X98) ),
inference(resolution,[status(thm)],[c13,mp_organizational_sets1_25]) ).
cnf(c39,plain,
( environment(sk1(sk3))
| selection_favors(efficient_producers,first_movers,sk3) ),
inference(resolution,[status(thm)],[c38,prove_t8_36]) ).
cnf(c41,plain,
environment(sk1(sk3)),
inference(resolution,[status(thm)],[c39,prove_t8_38]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(mp_greater_or_equal_33,axiom,
( X7 != X6
| greater_or_equal(X7,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_33) ).
cnf(c14,plain,
greater_or_equal(X8,X8),
inference(resolution,[status(thm)],[mp_greater_or_equal_33,reflexivity]) ).
cnf(mp_time_in_environment_27,axiom,
( ~ environment(X50)
| ~ greater_or_equal(X49,start_time(X50))
| ~ greater_or_equal(end_time(X50),X49)
| in_environment(X50,X49) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_time_in_environment_27) ).
cnf(c27,plain,
( ~ environment(X82)
| ~ greater_or_equal(end_time(X82),start_time(X82))
| in_environment(X82,end_time(X82)) ),
inference(resolution,[status(thm)],[mp_time_in_environment_27,c14]) ).
cnf(mp_greater_or_equal_32,axiom,
( ~ greater(X5,X4)
| greater_or_equal(X5,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_32) ).
cnf(c9,axiom,
( X62 != X61
| X63 != X60
| ~ in_environment(X62,X63)
| in_environment(X61,X60) ),
theory(equality) ).
cnf(prove_t8_37,negated_conjecture,
slow_change(sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_t8_37) ).
cnf(mp4_critical_point_23,axiom,
( ~ observational_period(X28)
| ~ slow_change(X28)
| ~ environment(X27)
| ~ in_environment(X28,X27)
| in_environment(X27,sk2(X27,X28)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp4_critical_point_23) ).
cnf(mp3_favoured_trategy_21,axiom,
( ~ observational_period(X11)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| in_environment(X11,sk1(X11))
| selection_favors(efficient_producers,first_movers,X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp3_favoured_trategy_21) ).
cnf(c16,plain,
( ~ observational_period(X105)
| ~ propagation_strategy(first_movers)
| in_environment(X105,sk1(X105))
| selection_favors(efficient_producers,first_movers,X105) ),
inference(resolution,[status(thm)],[mp3_favoured_trategy_21,mp_organizational_sets2_26]) ).
cnf(c46,plain,
( ~ observational_period(X106)
| in_environment(X106,sk1(X106))
| selection_favors(efficient_producers,first_movers,X106) ),
inference(resolution,[status(thm)],[c16,mp_organizational_sets1_25]) ).
cnf(c47,plain,
( in_environment(sk3,sk1(sk3))
| selection_favors(efficient_producers,first_movers,sk3) ),
inference(resolution,[status(thm)],[c46,prove_t8_36]) ).
cnf(c52,plain,
in_environment(sk3,sk1(sk3)),
inference(resolution,[status(thm)],[c47,prove_t8_38]) ).
cnf(c56,plain,
( ~ observational_period(sk3)
| ~ slow_change(sk3)
| ~ environment(sk1(sk3))
| in_environment(sk1(sk3),sk2(sk1(sk3),sk3)) ),
inference(resolution,[status(thm)],[c52,mp4_critical_point_23]) ).
cnf(c83,plain,
( ~ observational_period(sk3)
| ~ slow_change(sk3)
| in_environment(sk1(sk3),sk2(sk1(sk3),sk3)) ),
inference(resolution,[status(thm)],[c56,c41]) ).
cnf(c84,plain,
( ~ observational_period(sk3)
| in_environment(sk1(sk3),sk2(sk1(sk3),sk3)) ),
inference(resolution,[status(thm)],[c83,prove_t8_37]) ).
cnf(c85,plain,
in_environment(sk1(sk3),sk2(sk1(sk3),sk3)),
inference(resolution,[status(thm)],[c84,prove_t8_36]) ).
cnf(c87,plain,
( sk1(sk3) != X121
| sk2(sk1(sk3),sk3) != X122
| in_environment(X121,X122) ),
inference(resolution,[status(thm)],[c85,c9]) ).
cnf(symmetry,axiom,
( X10 != X9
| X9 = X10 ),
theory(equality) ).
cnf(mp_greater_transitivity_30,axiom,
( ~ greater(X30,X29)
| ~ greater(X29,X31)
| greater(X30,X31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_transitivity_30) ).
cnf(c11,axiom,
( X66 != X65
| X67 != X64
| ~ greater(X66,X67)
| greater(X65,X64) ),
theory(equality) ).
cnf(mp4_critical_point_24,axiom,
( ~ observational_period(X40)
| ~ slow_change(X40)
| ~ environment(X39)
| ~ in_environment(X40,X39)
| greater(sk2(X39,X40),critical_point(X39)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp4_critical_point_24) ).
cnf(c55,plain,
( ~ observational_period(sk3)
| ~ slow_change(sk3)
| ~ environment(sk1(sk3))
| greater(sk2(sk1(sk3),sk3),critical_point(sk1(sk3))) ),
inference(resolution,[status(thm)],[c52,mp4_critical_point_24]) ).
cnf(c99,plain,
( ~ observational_period(sk3)
| ~ slow_change(sk3)
| greater(sk2(sk1(sk3),sk3),critical_point(sk1(sk3))) ),
inference(resolution,[status(thm)],[c55,c41]) ).
cnf(c100,plain,
( ~ observational_period(sk3)
| greater(sk2(sk1(sk3),sk3),critical_point(sk1(sk3))) ),
inference(resolution,[status(thm)],[c99,prove_t8_37]) ).
cnf(c101,plain,
greater(sk2(sk1(sk3),sk3),critical_point(sk1(sk3))),
inference(resolution,[status(thm)],[c100,prove_t8_36]) ).
cnf(c103,plain,
( sk2(sk1(sk3),sk3) != X129
| critical_point(sk1(sk3)) != X130
| greater(X129,X130) ),
inference(resolution,[status(thm)],[c101,c11]) ).
cnf(c109,plain,
( critical_point(sk1(sk3)) != X131
| greater(sk2(sk1(sk3),sk3),X131) ),
inference(resolution,[status(thm)],[c103,reflexivity]) ).
cnf(mp_greater_or_equal_31,axiom,
( ~ greater_or_equal(X34,X33)
| greater(X34,X33)
| X34 = X33 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_greater_or_equal_31) ).
cnf(mp_time_of_critical_point_29,axiom,
( ~ environment(X26)
| greater_or_equal(critical_point(X26),start_time(X26)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_time_of_critical_point_29) ).
cnf(c43,plain,
greater_or_equal(critical_point(sk1(sk3)),start_time(sk1(sk3))),
inference(resolution,[status(thm)],[c41,mp_time_of_critical_point_29]) ).
cnf(c44,plain,
( greater(critical_point(sk1(sk3)),start_time(sk1(sk3)))
| critical_point(sk1(sk3)) = start_time(sk1(sk3)) ),
inference(resolution,[status(thm)],[c43,mp_greater_or_equal_31]) ).
cnf(c62,plain,
( critical_point(sk1(sk3)) = start_time(sk1(sk3))
| ~ greater(X128,critical_point(sk1(sk3)))
| greater(X128,start_time(sk1(sk3))) ),
inference(resolution,[status(thm)],[c44,mp_greater_transitivity_30]) ).
cnf(c108,plain,
( critical_point(sk1(sk3)) = start_time(sk1(sk3))
| greater(sk2(sk1(sk3),sk3),start_time(sk1(sk3))) ),
inference(resolution,[status(thm)],[c62,c101]) ).
cnf(c175,plain,
greater(sk2(sk1(sk3),sk3),start_time(sk1(sk3))),
inference(resolution,[status(thm)],[c108,c109]) ).
cnf(c208,plain,
( ~ greater(X137,sk2(sk1(sk3),sk3))
| greater(X137,start_time(sk1(sk3))) ),
inference(resolution,[status(thm)],[c175,mp_greater_transitivity_30]) ).
cnf(mp_environment_end_point_28,axiom,
( ~ environment(X59)
| ~ in_environment(X59,X58)
| greater_or_equal(end_time(X59),X58) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp_environment_end_point_28) ).
cnf(c90,plain,
( ~ environment(sk1(sk3))
| greater_or_equal(end_time(sk1(sk3)),sk2(sk1(sk3),sk3)) ),
inference(resolution,[status(thm)],[c85,mp_environment_end_point_28]) ).
cnf(c93,plain,
greater_or_equal(end_time(sk1(sk3)),sk2(sk1(sk3),sk3)),
inference(resolution,[status(thm)],[c90,c41]) ).
cnf(c95,plain,
( greater(end_time(sk1(sk3)),sk2(sk1(sk3),sk3))
| end_time(sk1(sk3)) = sk2(sk1(sk3),sk3) ),
inference(resolution,[status(thm)],[c93,mp_greater_or_equal_31]) ).
cnf(c312,plain,
( end_time(sk1(sk3)) = sk2(sk1(sk3),sk3)
| greater(end_time(sk1(sk3)),start_time(sk1(sk3))) ),
inference(resolution,[status(thm)],[c95,c208]) ).
cnf(c336,plain,
( greater(end_time(sk1(sk3)),start_time(sk1(sk3)))
| sk2(sk1(sk3),sk3) = end_time(sk1(sk3)) ),
inference(resolution,[status(thm)],[c312,symmetry]) ).
cnf(c385,plain,
( greater(end_time(sk1(sk3)),start_time(sk1(sk3)))
| sk1(sk3) != X149
| in_environment(X149,end_time(sk1(sk3))) ),
inference(resolution,[status(thm)],[c336,c87]) ).
cnf(c517,plain,
( greater(end_time(sk1(sk3)),start_time(sk1(sk3)))
| in_environment(sk1(sk3),end_time(sk1(sk3))) ),
inference(resolution,[status(thm)],[c385,reflexivity]) ).
cnf(c521,plain,
( in_environment(sk1(sk3),end_time(sk1(sk3)))
| greater_or_equal(end_time(sk1(sk3)),start_time(sk1(sk3))) ),
inference(resolution,[status(thm)],[c517,mp_greater_or_equal_32]) ).
cnf(c531,plain,
( in_environment(sk1(sk3),end_time(sk1(sk3)))
| ~ environment(sk1(sk3)) ),
inference(resolution,[status(thm)],[c521,c27]) ).
cnf(c534,plain,
in_environment(sk1(sk3),end_time(sk1(sk3))),
inference(resolution,[status(thm)],[c531,c41]) ).
cnf(l8_35,plain,
( ~ environment(X90)
| ~ in_environment(X90,X89)
| ~ greater(X89,critical_point(X90))
| selection_favors(efficient_producers,first_movers,X89) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l8_35) ).
cnf(c102,plain,
( ~ greater(X127,sk2(sk1(sk3),sk3))
| greater(X127,critical_point(sk1(sk3))) ),
inference(resolution,[status(thm)],[c101,mp_greater_transitivity_30]) ).
cnf(c314,plain,
( end_time(sk1(sk3)) = sk2(sk1(sk3),sk3)
| greater(end_time(sk1(sk3)),critical_point(sk1(sk3))) ),
inference(resolution,[status(thm)],[c95,c102]) ).
cnf(c358,plain,
( greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))
| sk2(sk1(sk3),sk3) = end_time(sk1(sk3)) ),
inference(resolution,[status(thm)],[c314,symmetry]) ).
cnf(c446,plain,
( greater(end_time(sk1(sk3)),critical_point(sk1(sk3)))
| critical_point(sk1(sk3)) != X199
| greater(end_time(sk1(sk3)),X199) ),
inference(resolution,[status(thm)],[c358,c103]) ).
cnf(c1169,plain,
greater(end_time(sk1(sk3)),critical_point(sk1(sk3))),
inference(resolution,[status(thm)],[c446,reflexivity]) ).
cnf(c1177,plain,
( ~ environment(sk1(sk3))
| ~ in_environment(sk1(sk3),end_time(sk1(sk3)))
| selection_favors(efficient_producers,first_movers,end_time(sk1(sk3))) ),
inference(resolution,[status(thm)],[c1169,l8_35]) ).
cnf(c1191,plain,
( ~ environment(sk1(sk3))
| selection_favors(efficient_producers,first_movers,end_time(sk1(sk3))) ),
inference(resolution,[status(thm)],[c1177,c534]) ).
cnf(c1192,plain,
selection_favors(efficient_producers,first_movers,end_time(sk1(sk3))),
inference(resolution,[status(thm)],[c1191,c41]) ).
cnf(c1193,plain,
( ~ observational_period(sk3)
| ~ propagation_strategy(first_movers)
| ~ propagation_strategy(efficient_producers)
| selection_favors(efficient_producers,first_movers,sk3) ),
inference(resolution,[status(thm)],[c1192,mp3_favoured_trategy_22]) ).
cnf(c1195,plain,
( ~ observational_period(sk3)
| ~ propagation_strategy(first_movers)
| selection_favors(efficient_producers,first_movers,sk3) ),
inference(resolution,[status(thm)],[c1193,mp_organizational_sets2_26]) ).
cnf(c1196,plain,
( ~ observational_period(sk3)
| selection_favors(efficient_producers,first_movers,sk3) ),
inference(resolution,[status(thm)],[c1195,mp_organizational_sets1_25]) ).
cnf(c1197,plain,
selection_favors(efficient_producers,first_movers,sk3),
inference(resolution,[status(thm)],[c1196,prove_t8_36]) ).
cnf(c1198,plain,
$false,
inference(resolution,[status(thm)],[c1197,prove_t8_38]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT039-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.35 % Computer : n010.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 7 12:54:41 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.41 (re.compile("\."), Token.FullStop),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.41 (re.compile("\("), Token.OpenPar),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.41 (re.compile("\)"), Token.ClosePar),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.41 (re.compile("\["), Token.OpenSquare),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("~\|"), Token.Nor),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("\|"), Token.Or),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.42 (re.compile("\?"), Token.Existential),
% 0.13/0.42 /export/starexec/sandbox2/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/sandbox2/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.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.21/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.32/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.57 """
% 0.66/1.01 % Version: 1.5
% 0.66/1.01 % SZS status Unsatisfiable
% 0.66/1.01 % SZS output start CNFRefutation
% See solution above
% 0.66/1.01
% 0.66/1.01 % Initial clauses : 35
% 0.66/1.01 % Processed clauses : 214
% 0.66/1.01 % Factors computed : 4
% 0.66/1.01 % Resolvents computed: 1183
% 0.66/1.01 % Tautologies deleted: 7
% 0.66/1.01 % Forward subsumed : 161
% 0.66/1.01 % Backward subsumed : 58
% 0.66/1.01 % -------- CPU Time ---------
% 0.66/1.01 % User time : 0.625 s
% 0.66/1.01 % System time : 0.027 s
% 0.66/1.01 % Total time : 0.652 s
%------------------------------------------------------------------------------