%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT059+1 : TPTP v9.3.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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 : Theorem 0.89s 1.15s
% Output : CNFRefutation 0.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT059+1 : TPTP v9.3.0. Released v2.4.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.34 % Computer : n015.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Mon Sep 7 13:36:00 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.41 (re.compile("\."), Token.FullStop),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.41 (re.compile("\("), Token.OpenPar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.41 (re.compile("\)"), Token.ClosePar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.41 (re.compile("\["), Token.OpenSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("~\|"), Token.Nor),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("\|"), Token.Or),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.41 (re.compile("\?"), Token.Existential),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.24/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.48 """
% 0.24/0.49 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.49 """
% 0.24/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.58 """
% 0.89/1.15 % Version: 1.5
% 0.89/1.15 % SZS status Theorem
% 0.89/1.15 % SZS output start CNFRefutation
% 0.89/1.15 fof(assumption_2,conjecture,(![X]:(![T0]:(![T]:(((organization(X)&has_immunity(X,T0))&has_immunity(X,T))=>hazard_of_mortality(X,T0)=hazard_of_mortality(X,T))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_2)).
% 0.89/1.15 fof(c9,negated_conjecture,(~(![X]:(![T0]:(![T]:(((organization(X)&has_immunity(X,T0))&has_immunity(X,T))=>hazard_of_mortality(X,T0)=hazard_of_mortality(X,T)))))),inference(assume_negation,[status(cth)],[assumption_2])).
% 0.89/1.15 fof(c10,negated_conjecture,(?[X]:(?[T0]:(?[T]:(((organization(X)&has_immunity(X,T0))&has_immunity(X,T))&hazard_of_mortality(X,T0)!=hazard_of_mortality(X,T))))),inference(fof_nnf,[status(thm)],[c9])).
% 0.89/1.15 fof(c11,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(((organization(X2)&has_immunity(X2,X3))&has_immunity(X2,X4))&hazard_of_mortality(X2,X3)!=hazard_of_mortality(X2,X4))))),inference(variable_rename,[status(thm)],[c10])).
% 0.89/1.15 fof(c12,negated_conjecture,(((organization(skolem0001)&has_immunity(skolem0001,skolem0002))&has_immunity(skolem0001,skolem0003))&hazard_of_mortality(skolem0001,skolem0002)!=hazard_of_mortality(skolem0001,skolem0003)),inference(skolemize,[status(esa)],[c11])).
% 0.89/1.15 cnf(c16,negated_conjecture,hazard_of_mortality(skolem0001,skolem0002)!=hazard_of_mortality(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c12])).
% 0.89/1.15 cnf(c13,negated_conjecture,organization(skolem0001),inference(split_conjunct,[status(thm)],[c12])).
% 0.89/1.15 cnf(c14,negated_conjecture,has_immunity(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c12])).
% 0.89/1.15 fof(assumption_17,axiom,(![X]:(![T]:(organization(X)=>((has_immunity(X,T)=>hazard_of_mortality(X,T)=very_low)&((~has_immunity(X,T))=>(((((is_aligned(X,T)&positional_advantage(X,T))=>hazard_of_mortality(X,T)=low)&(((~is_aligned(X,T))&positional_advantage(X,T))=>hazard_of_mortality(X,T)=mod1))&((is_aligned(X,T)&(~positional_advantage(X,T)))=>hazard_of_mortality(X,T)=mod2))&(((~is_aligned(X,T))&(~positional_advantage(X,T)))=>hazard_of_mortality(X,T)=high))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', assumption_17)).
% 0.89/1.15 fof(c17,plain,(![X]:(![T]:(organization(X)=>((has_immunity(X,T)=>hazard_of_mortality(X,T)=very_low)&(~has_immunity(X,T)=>(((((is_aligned(X,T)&positional_advantage(X,T))=>hazard_of_mortality(X,T)=low)&((~is_aligned(X,T)&positional_advantage(X,T))=>hazard_of_mortality(X,T)=mod1))&((is_aligned(X,T)&~positional_advantage(X,T))=>hazard_of_mortality(X,T)=mod2))&((~is_aligned(X,T)&~positional_advantage(X,T))=>hazard_of_mortality(X,T)=high))))))),inference(fof_simplification,[status(thm)],[assumption_17])).
% 0.89/1.15 fof(c18,plain,(![X]:(![T]:(~organization(X)|((~has_immunity(X,T)|hazard_of_mortality(X,T)=very_low)&(has_immunity(X,T)|(((((~is_aligned(X,T)|~positional_advantage(X,T))|hazard_of_mortality(X,T)=low)&((is_aligned(X,T)|~positional_advantage(X,T))|hazard_of_mortality(X,T)=mod1))&((~is_aligned(X,T)|positional_advantage(X,T))|hazard_of_mortality(X,T)=mod2))&((is_aligned(X,T)|positional_advantage(X,T))|hazard_of_mortality(X,T)=high))))))),inference(fof_nnf,[status(thm)],[c17])).
% 0.89/1.15 fof(c19,plain,(![X]:(~organization(X)|((![T]:(~has_immunity(X,T)|hazard_of_mortality(X,T)=very_low))&(![T]:(has_immunity(X,T)|(((((~is_aligned(X,T)|~positional_advantage(X,T))|hazard_of_mortality(X,T)=low)&((is_aligned(X,T)|~positional_advantage(X,T))|hazard_of_mortality(X,T)=mod1))&((~is_aligned(X,T)|positional_advantage(X,T))|hazard_of_mortality(X,T)=mod2))&((is_aligned(X,T)|positional_advantage(X,T))|hazard_of_mortality(X,T)=high))))))),inference(shift_quantors,[status(thm)],[c18])).
% 0.89/1.15 fof(c21,plain,(![X5]:(![X6]:(![X7]:(~organization(X5)|((~has_immunity(X5,X6)|hazard_of_mortality(X5,X6)=very_low)&(has_immunity(X5,X7)|(((((~is_aligned(X5,X7)|~positional_advantage(X5,X7))|hazard_of_mortality(X5,X7)=low)&((is_aligned(X5,X7)|~positional_advantage(X5,X7))|hazard_of_mortality(X5,X7)=mod1))&((~is_aligned(X5,X7)|positional_advantage(X5,X7))|hazard_of_mortality(X5,X7)=mod2))&((is_aligned(X5,X7)|positional_advantage(X5,X7))|hazard_of_mortality(X5,X7)=high)))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,(![X5]:(~organization(X5)|((![X6]:(~has_immunity(X5,X6)|hazard_of_mortality(X5,X6)=very_low))&(![X7]:(has_immunity(X5,X7)|(((((~is_aligned(X5,X7)|~positional_advantage(X5,X7))|hazard_of_mortality(X5,X7)=low)&((is_aligned(X5,X7)|~positional_advantage(X5,X7))|hazard_of_mortality(X5,X7)=mod1))&((~is_aligned(X5,X7)|positional_advantage(X5,X7))|hazard_of_mortality(X5,X7)=mod2))&((is_aligned(X5,X7)|positional_advantage(X5,X7))|hazard_of_mortality(X5,X7)=high))))))),inference(variable_rename,[status(thm)],[c19])).])).
% 0.89/1.15 fof(c22,plain,(![X5]:(![X6]:(![X7]:((~organization(X5)|(~has_immunity(X5,X6)|hazard_of_mortality(X5,X6)=very_low))&((((~organization(X5)|(has_immunity(X5,X7)|((~is_aligned(X5,X7)|~positional_advantage(X5,X7))|hazard_of_mortality(X5,X7)=low)))&(~organization(X5)|(has_immunity(X5,X7)|((is_aligned(X5,X7)|~positional_advantage(X5,X7))|hazard_of_mortality(X5,X7)=mod1))))&(~organization(X5)|(has_immunity(X5,X7)|((~is_aligned(X5,X7)|positional_advantage(X5,X7))|hazard_of_mortality(X5,X7)=mod2))))&(~organization(X5)|(has_immunity(X5,X7)|((is_aligned(X5,X7)|positional_advantage(X5,X7))|hazard_of_mortality(X5,X7)=high)))))))),inference(distribute,[status(thm)],[c21])).
% 0.89/1.15 cnf(c23,plain,~organization(X147)|~has_immunity(X147,X148)|hazard_of_mortality(X147,X148)=very_low,inference(split_conjunct,[status(thm)],[c22])).
% 0.89/1.15 cnf(c204,plain,~organization(skolem0001)|hazard_of_mortality(skolem0001,skolem0002)=very_low,inference(resolution,[status(thm)],[c23, c14])).
% 0.89/1.15 cnf(c707,plain,hazard_of_mortality(skolem0001,skolem0002)=very_low,inference(resolution,[status(thm)],[c204, c13])).
% 0.89/1.15 cnf(transitivity,axiom,X30!=X31|X31!=X32|X30=X32,theory(equality)).
% 0.89/1.15 cnf(symmetry,axiom,X28!=X29|X29=X28,theory(equality)).
% 0.89/1.15 cnf(c15,negated_conjecture,has_immunity(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c12])).
% 0.89/1.15 cnf(c205,plain,~organization(skolem0001)|hazard_of_mortality(skolem0001,skolem0003)=very_low,inference(resolution,[status(thm)],[c23, c15])).
% 0.89/1.15 cnf(c826,plain,hazard_of_mortality(skolem0001,skolem0003)=very_low,inference(resolution,[status(thm)],[c205, c13])).
% 0.89/1.15 cnf(c833,plain,very_low=hazard_of_mortality(skolem0001,skolem0003),inference(resolution,[status(thm)],[c826, symmetry])).
% 0.89/1.15 cnf(c873,plain,X775!=very_low|X775=hazard_of_mortality(skolem0001,skolem0003),inference(resolution,[status(thm)],[c833, transitivity])).
% 0.89/1.15 cnf(c1344,plain,hazard_of_mortality(skolem0001,skolem0002)=hazard_of_mortality(skolem0001,skolem0003),inference(resolution,[status(thm)],[c873, c707])).
% 0.89/1.15 cnf(c2531,plain,$false,inference(resolution,[status(thm)],[c1344, c16])).
% 0.89/1.15 % SZS output end CNFRefutation
% 0.89/1.15
% 0.89/1.15 % Initial clauses : 32
% 0.89/1.15 % Processed clauses : 226
% 0.89/1.15 % Factors computed : 52
% 0.89/1.15 % Resolvents computed: 2463
% 0.89/1.15 % Tautologies deleted: 8
% 0.89/1.15 % Forward subsumed : 291
% 0.89/1.15 % Backward subsumed : 10
% 0.89/1.15 % -------- CPU Time ---------
% 0.89/1.15 % User time : 0.776 s
% 0.89/1.15 % System time : 0.026 s
% 0.89/1.15 % Total time : 0.802 s
%------------------------------------------------------------------------------