%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT057-1 : TPTP v9.3.0. Released v2.4.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:48 AM UTC 2026
% Result : Unsatisfiable 54.90s 55.17s
% Output : CNFRefutation 54.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 16
% Syntax : Number of clauses : 37 ( 19 unt; 3 nHn; 33 RR)
% Number of literals : 66 ( 16 equ; 31 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-2 aty)
% Number of variables : 27 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(theorem_6_41,negated_conjecture,
has_endowment(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_6_41) ).
cnf(theorem_6_44,negated_conjecture,
greater(age(sk2,sk5),eta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_6_44) ).
cnf(definition_1_33,axiom,
( ~ has_endowment(X46)
| ~ greater(age(X46,X47),eta)
| ~ has_immunity(X46,X47) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_1_33) ).
cnf(c59,plain,
( ~ has_endowment(sk2)
| ~ has_immunity(sk2,sk5) ),
inference(resolution,[status(thm)],[definition_1_33,theorem_6_44]) ).
cnf(theorem_6_40,negated_conjecture,
organization(sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_6_40) ).
cnf(theorem_6_43,negated_conjecture,
smaller_or_equal(age(sk2,sk4),eta),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_6_43) ).
cnf(definition_1_32,axiom,
( ~ has_endowment(X39)
| ~ smaller_or_equal(age(X39,X40),eta)
| has_immunity(X39,X40) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_1_32) ).
cnf(c48,plain,
( ~ has_endowment(sk2)
| has_immunity(sk2,sk4) ),
inference(resolution,[status(thm)],[definition_1_32,theorem_6_43]) ).
cnf(c68,plain,
has_immunity(sk2,sk4),
inference(resolution,[status(thm)],[c48,theorem_6_41]) ).
cnf(assumption_3_39,axiom,
( ~ organization(X69)
| ~ has_immunity(X69,X70)
| has_immunity(X69,X71)
| greater(hazard_of_mortality(X69,X71),hazard_of_mortality(X69,X70)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_3_39) ).
cnf(c124,plain,
( ~ organization(sk2)
| has_immunity(sk2,X520)
| greater(hazard_of_mortality(sk2,X520),hazard_of_mortality(sk2,sk4)) ),
inference(resolution,[status(thm)],[assumption_3_39,c68]) ).
cnf(c1042,plain,
( has_immunity(sk2,X4404)
| greater(hazard_of_mortality(sk2,X4404),hazard_of_mortality(sk2,sk4)) ),
inference(resolution,[status(thm)],[c124,theorem_6_40]) ).
cnf(theorem_6_46,negated_conjecture,
( ~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4))
| hazard_of_mortality(sk2,sk4) != hazard_of_mortality(sk2,sk3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_6_46) ).
cnf(symmetry,axiom,
( X28 != X29
| X29 = X28 ),
theory(equality) ).
cnf(assumption_2_38,axiom,
( ~ organization(X61)
| ~ has_immunity(X61,X62)
| ~ has_immunity(X61,X63)
| hazard_of_mortality(X61,X62) = hazard_of_mortality(X61,X63) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',assumption_2_38) ).
cnf(c92,plain,
( ~ organization(sk2)
| ~ has_immunity(sk2,X383)
| hazard_of_mortality(sk2,X383) = hazard_of_mortality(sk2,sk4) ),
inference(resolution,[status(thm)],[assumption_2_38,c68]) ).
cnf(theorem_6_42,negated_conjecture,
age(sk2,sk3) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_6_42) ).
cnf(c37,plain,
zero = age(sk2,sk3),
inference(resolution,[status(thm)],[theorem_6_42,symmetry]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(definition_smaller_or_equal_2,axiom,
( ~ smaller(X6,X7)
| smaller_or_equal(X6,X7) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT001-0.ax',definition_smaller_or_equal_2) ).
cnf(theorem_6_45,negated_conjecture,
greater(eta,zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',theorem_6_45) ).
cnf(definition_smaller_8,axiom,
( ~ greater(X20,X21)
| smaller(X21,X20) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MGT001-0.ax',definition_smaller_8) ).
cnf(c17,plain,
smaller(zero,eta),
inference(resolution,[status(thm)],[definition_smaller_8,theorem_6_45]) ).
cnf(c20,plain,
smaller_or_equal(zero,eta),
inference(resolution,[status(thm)],[c17,definition_smaller_or_equal_2]) ).
cnf(c3,axiom,
( X100 != X102
| X101 != X99
| ~ smaller_or_equal(X100,X101)
| smaller_or_equal(X102,X99) ),
theory(equality) ).
cnf(c178,plain,
( zero != X594
| eta != X595
| smaller_or_equal(X594,X595) ),
inference(resolution,[status(thm)],[c3,c20]) ).
cnf(c1240,plain,
( zero != X596
| smaller_or_equal(X596,eta) ),
inference(resolution,[status(thm)],[c178,reflexivity]) ).
cnf(c1242,plain,
smaller_or_equal(age(sk2,sk3),eta),
inference(resolution,[status(thm)],[c1240,c37]) ).
cnf(c1262,plain,
( ~ has_endowment(sk2)
| has_immunity(sk2,sk3) ),
inference(resolution,[status(thm)],[c1242,definition_1_32]) ).
cnf(c1263,plain,
has_immunity(sk2,sk3),
inference(resolution,[status(thm)],[c1262,theorem_6_41]) ).
cnf(c1268,plain,
( ~ organization(sk2)
| hazard_of_mortality(sk2,sk3) = hazard_of_mortality(sk2,sk4) ),
inference(resolution,[status(thm)],[c1263,c92]) ).
cnf(c90263,plain,
hazard_of_mortality(sk2,sk3) = hazard_of_mortality(sk2,sk4),
inference(resolution,[status(thm)],[c1268,theorem_6_40]) ).
cnf(c90417,plain,
hazard_of_mortality(sk2,sk4) = hazard_of_mortality(sk2,sk3),
inference(resolution,[status(thm)],[c90263,symmetry]) ).
cnf(c90480,plain,
~ greater(hazard_of_mortality(sk2,sk5),hazard_of_mortality(sk2,sk4)),
inference(resolution,[status(thm)],[c90417,theorem_6_46]) ).
cnf(c90680,plain,
has_immunity(sk2,sk5),
inference(resolution,[status(thm)],[c90480,c1042]) ).
cnf(c90841,plain,
~ has_endowment(sk2),
inference(resolution,[status(thm)],[c90680,c59]) ).
cnf(c90845,plain,
$false,
inference(resolution,[status(thm)],[c90841,theorem_6_41]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT057-1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.36 % Computer : n009.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 7 13:30:52 UTC 2026
% 0.03/0.37 % CPUTime :
% 0.03/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.03/0.43 (re.compile("\."), Token.FullStop),
% 0.03/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.03/0.43 (re.compile("\("), Token.OpenPar),
% 0.03/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.03/0.43 (re.compile("\)"), Token.ClosePar),
% 0.03/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.03/0.43 (re.compile("\["), Token.OpenSquare),
% 0.03/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.03/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.03/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.03/0.43 (re.compile("~\|"), Token.Nor),
% 0.03/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.03/0.43 (re.compile("\|"), Token.Or),
% 0.03/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.03/0.43 (re.compile("\?"), Token.Existential),
% 0.03/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.03/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.03/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.03/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.50 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.50 """
% 0.23/0.50 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.50 """
% 0.33/0.60 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.60 """
% 54.90/55.17 % Version: 1.5
% 54.90/55.17 % SZS status Unsatisfiable
% 54.90/55.17 % SZS output start CNFRefutation
% See solution above
% 54.90/55.17
% 54.90/55.17 % Initial clauses : 40
% 54.90/55.17 % Processed clauses : 1024
% 54.90/55.17 % Factors computed : 383
% 54.90/55.17 % Resolvents computed: 90473
% 54.90/55.17 % Tautologies deleted: 19
% 54.90/55.17 % Forward subsumed : 3237
% 54.90/55.17 % Backward subsumed : 36
% 54.90/55.17 % -------- CPU Time ---------
% 54.90/55.17 % User time : 54.506 s
% 54.90/55.17 % System time : 0.295 s
% 54.90/55.17 % Total time : 54.801 s
%------------------------------------------------------------------------------