%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT031-1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:43 AM UTC 2026
% Result : Satisfiable 0.39s 0.66s
% Output : Saturation 0.39s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c8,axiom,
( X46 != X48
| X47 != X49
| ~ greater_or_equal(X46,X47)
| greater_or_equal(X48,X49) ),
theory(equality) ).
cnf(mp_greater_or_equal_28,axiom,
( ~ greater(X3,X4)
| greater_or_equal(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_28) ).
cnf(prove_l13_32,negated_conjecture,
environment(sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l13_32) ).
cnf(a13_31,plain,
( ~ environment(X35)
| greater(appear(efficient_producers,e),appear(first_movers,X35)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a13_31) ).
cnf(c24,plain,
greater(appear(efficient_producers,e),appear(first_movers,sk2)),
inference(resolution,[status(thm)],[a13_31,prove_l13_32]) ).
cnf(mp_greater_transitivity_26,axiom,
( ~ greater(X17,X18)
| ~ greater(X18,X19)
| greater(X17,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_transitivity_26) ).
cnf(prove_l13_34,negated_conjecture,
appear(an_organisation,sk2) != appear(first_movers,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l13_34) ).
cnf(symmetry,axiom,
( X10 != X9
| X9 = X10 ),
theory(equality) ).
cnf(mp_greater_or_equal_27,axiom,
( ~ greater_or_equal(X21,X22)
| greater(X21,X22)
| X21 = X22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_27) ).
cnf(mp_FM_not_precede_first_25,axiom,
( ~ environment(X34)
| greater_or_equal(appear(first_movers,X34),appear(an_organisation,X34)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_FM_not_precede_first_25) ).
cnf(c22,plain,
greater_or_equal(appear(first_movers,sk2),appear(an_organisation,sk2)),
inference(resolution,[status(thm)],[mp_FM_not_precede_first_25,prove_l13_32]) ).
cnf(c23,plain,
( greater(appear(first_movers,sk2),appear(an_organisation,sk2))
| appear(first_movers,sk2) = appear(an_organisation,sk2) ),
inference(resolution,[status(thm)],[c22,mp_greater_or_equal_27]) ).
cnf(c83,plain,
( greater(appear(first_movers,sk2),appear(an_organisation,sk2))
| appear(an_organisation,sk2) = appear(first_movers,sk2) ),
inference(resolution,[status(thm)],[c23,symmetry]) ).
cnf(c108,plain,
greater(appear(first_movers,sk2),appear(an_organisation,sk2)),
inference(resolution,[status(thm)],[c83,prove_l13_34]) ).
cnf(c121,plain,
( ~ greater(X136,appear(first_movers,sk2))
| greater(X136,appear(an_organisation,sk2)) ),
inference(resolution,[status(thm)],[c108,mp_greater_transitivity_26]) ).
cnf(c123,plain,
greater(appear(efficient_producers,e),appear(an_organisation,sk2)),
inference(resolution,[status(thm)],[c121,c24]) ).
cnf(c124,plain,
greater_or_equal(appear(efficient_producers,e),appear(an_organisation,sk2)),
inference(resolution,[status(thm)],[c123,mp_greater_or_equal_28]) ).
cnf(c128,plain,
( appear(efficient_producers,e) != X147
| appear(an_organisation,sk2) != X146
| greater_or_equal(X147,X146) ),
inference(resolution,[status(thm)],[c124,c8]) ).
cnf(c134,plain,
( appear(efficient_producers,e) != X148
| greater_or_equal(X148,appear(an_organisation,sk2)) ),
inference(resolution,[status(thm)],[c128,reflexivity]) ).
cnf(c5,axiom,
( X38 != X40
| X39 != X41
| ~ greater(X38,X39)
| greater(X40,X41) ),
theory(equality) ).
cnf(c126,plain,
( appear(efficient_producers,e) != X144
| appear(an_organisation,sk2) != X143
| greater(X144,X143) ),
inference(resolution,[status(thm)],[c123,c5]) ).
cnf(c132,plain,
( appear(efficient_producers,e) != X145
| greater(X145,appear(an_organisation,sk2)) ),
inference(resolution,[status(thm)],[c126,reflexivity]) ).
cnf(c122,plain,
( appear(first_movers,sk2) != X141
| appear(an_organisation,sk2) != X140
| greater(X141,X140) ),
inference(resolution,[status(thm)],[c108,c5]) ).
cnf(c130,plain,
( appear(first_movers,sk2) != X142
| greater(X142,appear(an_organisation,sk2)) ),
inference(resolution,[status(thm)],[c122,reflexivity]) ).
cnf(c125,plain,
( ~ greater(X139,appear(efficient_producers,e))
| greater(X139,appear(an_organisation,sk2)) ),
inference(resolution,[status(thm)],[c123,mp_greater_transitivity_26]) ).
cnf(c34,plain,
( appear(first_movers,sk2) != X133
| appear(an_organisation,sk2) != X132
| greater_or_equal(X133,X132) ),
inference(resolution,[status(thm)],[c8,c22]) ).
cnf(c64,plain,
( appear(first_movers,sk2) != X134
| greater_or_equal(X134,appear(an_organisation,sk2)) ),
inference(resolution,[status(thm)],[c34,reflexivity]) ).
cnf(c25,plain,
greater_or_equal(appear(efficient_producers,e),appear(first_movers,sk2)),
inference(resolution,[status(thm)],[c24,mp_greater_or_equal_28]) ).
cnf(c32,plain,
( appear(efficient_producers,e) != X130
| appear(first_movers,sk2) != X129
| greater_or_equal(X130,X129) ),
inference(resolution,[status(thm)],[c8,c25]) ).
cnf(c62,plain,
( appear(efficient_producers,e) != X131
| greater_or_equal(X131,appear(first_movers,sk2)) ),
inference(resolution,[status(thm)],[c32,reflexivity]) ).
cnf(mp_positive_number_when_appear_20,axiom,
( ~ environment(X8)
| greater(number_of_organizations(e,appear(an_organisation,X8)),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_positive_number_when_appear_20) ).
cnf(c10,plain,
greater(number_of_organizations(e,appear(an_organisation,sk2)),zero),
inference(resolution,[status(thm)],[mp_positive_number_when_appear_20,prove_l13_32]) ).
cnf(c19,plain,
greater_or_equal(number_of_organizations(e,appear(an_organisation,sk2)),zero),
inference(resolution,[status(thm)],[c10,mp_greater_or_equal_28]) ).
cnf(c31,plain,
( number_of_organizations(e,appear(an_organisation,sk2)) != X127
| zero != X126
| greater_or_equal(X127,X126) ),
inference(resolution,[status(thm)],[c8,c19]) ).
cnf(c60,plain,
( zero != X128
| greater_or_equal(number_of_organizations(e,appear(an_organisation,sk2)),X128) ),
inference(resolution,[status(thm)],[c31,reflexivity]) ).
cnf(mp_number_mean_non_empty_21,axiom,
( ~ environment(X15)
| ~ greater(number_of_organizations(X15,X16),zero)
| subpopulation(sk1(X16,X15),X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_number_mean_non_empty_21) ).
cnf(c20,plain,
( ~ environment(e)
| subpopulation(sk1(appear(an_organisation,sk2),e),e,appear(an_organisation,sk2)) ),
inference(resolution,[status(thm)],[c10,mp_number_mean_non_empty_21]) ).
cnf(c29,plain,
( number_of_organizations(e,appear(an_organisation,sk2)) != X124
| zero != X123
| greater(X124,X123) ),
inference(resolution,[status(thm)],[c5,c10]) ).
cnf(c58,plain,
( zero != X125
| greater(number_of_organizations(e,appear(an_organisation,sk2)),X125) ),
inference(resolution,[status(thm)],[c29,reflexivity]) ).
cnf(c28,plain,
( appear(efficient_producers,e) != X121
| appear(first_movers,sk2) != X120
| greater(X121,X120) ),
inference(resolution,[status(thm)],[c5,c24]) ).
cnf(c56,plain,
( appear(efficient_producers,e) != X122
| greater(X122,appear(first_movers,sk2)) ),
inference(resolution,[status(thm)],[c28,reflexivity]) ).
cnf(mp_number_mean_non_empty_22,axiom,
( ~ environment(X27)
| ~ greater(number_of_organizations(X27,X28),zero)
| greater(cardinality_at_time(sk1(X28,X27),X28),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_number_mean_non_empty_22) ).
cnf(c18,plain,
( ~ environment(e)
| greater(cardinality_at_time(sk1(appear(an_organisation,sk2),e),appear(an_organisation,sk2)),zero) ),
inference(resolution,[status(thm)],[c10,mp_number_mean_non_empty_22]) ).
cnf(prove_l13_33,negated_conjecture,
in_environment(sk2,appear(an_organisation,sk2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_l13_33) ).
cnf(c7,axiom,
( X42 != X44
| X43 != X45
| ~ in_environment(X42,X43)
| in_environment(X44,X45) ),
theory(equality) ).
cnf(c30,plain,
( sk2 != X117
| appear(an_organisation,sk2) != X118
| in_environment(X117,X118) ),
inference(resolution,[status(thm)],[c7,prove_l13_33]) ).
cnf(c54,plain,
( sk2 != X119
| in_environment(X119,appear(an_organisation,sk2)) ),
inference(resolution,[status(thm)],[c30,reflexivity]) ).
cnf(c26,plain,
( ~ greater(X116,appear(efficient_producers,e))
| greater(X116,appear(first_movers,sk2)) ),
inference(resolution,[status(thm)],[c24,mp_greater_transitivity_26]) ).
cnf(c6,axiom,
( X114 != X111
| X110 != X113
| X115 != X112
| ~ subpopulation(X114,X110,X115)
| subpopulation(X111,X113,X112) ),
theory(equality) ).
cnf(c17,plain,
( ~ greater(X109,number_of_organizations(e,appear(an_organisation,sk2)))
| greater(X109,zero) ),
inference(resolution,[status(thm)],[c10,mp_greater_transitivity_26]) ).
cnf(c3,axiom,
( X97 != X99
| X98 != X100
| cardinality_at_time(X97,X98) = cardinality_at_time(X99,X100) ),
theory(equality) ).
cnf(c51,plain,
( X106 != X104
| cardinality_at_time(X106,X105) = cardinality_at_time(X104,X105) ),
inference(resolution,[status(thm)],[c3,reflexivity]) ).
cnf(c50,plain,
( X101 != X102
| cardinality_at_time(X101,X101) = cardinality_at_time(X102,X102) ),
inference(factor,[status(thm)],[c3]) ).
cnf(c2,axiom,
( X83 != X85
| X84 != X86
| sk1(X83,X84) = sk1(X85,X86) ),
theory(equality) ).
cnf(c47,plain,
( X92 != X94
| sk1(X92,X93) = sk1(X94,X93) ),
inference(resolution,[status(thm)],[c2,reflexivity]) ).
cnf(c46,plain,
( X90 != X89
| sk1(X90,X90) = sk1(X89,X89) ),
inference(factor,[status(thm)],[c2]) ).
cnf(c1,axiom,
( X68 != X70
| X69 != X71
| appear(X68,X69) = appear(X70,X71) ),
theory(equality) ).
cnf(c42,plain,
( X82 != X80
| appear(X82,X81) = appear(X80,X81) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(c41,plain,
( X78 != X77
| appear(X78,X78) = appear(X77,X77) ),
inference(factor,[status(thm)],[c1]) ).
cnf(c0,axiom,
( X61 != X63
| X62 != X64
| number_of_organizations(X61,X62) = number_of_organizations(X63,X64) ),
theory(equality) ).
cnf(c39,plain,
( X74 != X73
| number_of_organizations(X74,X72) = number_of_organizations(X73,X72) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c38,plain,
( X66 != X65
| number_of_organizations(X66,X66) = number_of_organizations(X65,X65) ),
inference(factor,[status(thm)],[c0]) ).
cnf(mp_greater_or_equal_29,axiom,
( X5 != X6
| greater_or_equal(X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_greater_or_equal_29) ).
cnf(c9,plain,
greater_or_equal(X7,X7),
inference(resolution,[status(thm)],[mp_greater_or_equal_29,reflexivity]) ).
cnf(c33,plain,
( X52 != X51
| X52 != X50
| greater_or_equal(X51,X50) ),
inference(resolution,[status(thm)],[c8,c9]) ).
cnf(c36,plain,
( X58 != X59
| greater_or_equal(X59,X58) ),
inference(resolution,[status(thm)],[c33,reflexivity]) ).
cnf(a9_30,plain,
( ~ environment(X55)
| ~ subpopulation(X56,X55,X57)
| ~ greater(cardinality_at_time(X56,X57),zero)
| X56 = efficient_producers
| X56 = first_movers ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a9_30) ).
cnf(mp_no_FM_before_appearance_24,axiom,
( ~ environment(X36)
| ~ in_environment(X36,X37)
| ~ greater(appear(first_movers,X36),X37)
| ~ greater(cardinality_at_time(first_movers,X37),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_no_FM_before_appearance_24) ).
cnf(mp_no_EP_before_appearance_23,axiom,
( ~ environment(X32)
| ~ in_environment(X32,X33)
| ~ greater(appear(efficient_producers,X32),X33)
| ~ greater(cardinality_at_time(efficient_producers,X33),zero) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp_no_EP_before_appearance_23) ).
cnf(transitivity,axiom,
( X25 != X24
| X24 != X26
| X25 = X26 ),
theory(equality) ).
cnf(c4,axiom,
( X12 != X13
| ~ environment(X12)
| environment(X13) ),
theory(equality) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT031-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 : n005.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:21:20 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.41 (re.compile("\."), Token.FullStop),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.41 (re.compile("\("), Token.OpenPar),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.41 (re.compile("\)"), Token.ClosePar),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.41 (re.compile("\["), Token.OpenSquare),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("~\|"), Token.Nor),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("\|"), Token.Or),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.41 (re.compile("\?"), Token.Existential),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/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.33/0.57 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.57 """
% 0.39/0.66 % Version: 1.5
% 0.39/0.66 % SZS status Satisfiable
% 0.39/0.66 % SZS output start Saturation
% See solution above
% 0.39/0.66
% 0.39/0.66 % Initial clauses : 27
% 0.39/0.66 % Processed clauses : 75
% 0.39/0.66 % Factors computed : 7
% 0.39/0.66 % Resolvents computed: 120
% 0.39/0.66 % Tautologies deleted: 4
% 0.39/0.66 % Forward subsumed : 75
% 0.39/0.66 % Backward subsumed : 5
% 0.39/0.66 % -------- CPU Time ---------
% 0.39/0.66 % User time : 0.280 s
% 0.39/0.66 % System time : 0.023 s
% 0.39/0.66 % Total time : 0.303 s
%------------------------------------------------------------------------------