%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT089+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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:51 AM UTC 2026
% Result : Theorem 0.39s 0.68s
% Output : CNFRefutation 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT089+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.38 % Computer : n006.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Mon Sep 7 14:00:16 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.44 (re.compile("\."), Token.FullStop),
% 0.09/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.44 (re.compile("\("), Token.OpenPar),
% 0.09/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.44 (re.compile("\)"), Token.ClosePar),
% 0.09/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.44 (re.compile("\["), Token.OpenSquare),
% 0.09/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.44 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.44 (re.compile("~\|"), Token.Nor),
% 0.09/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.44 (re.compile("\|"), Token.Or),
% 0.09/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.44 (re.compile("\?"), Token.Existential),
% 0.09/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.09/0.44 (re.compile("\s+"), Token.WhiteSpace),
% 0.09/0.44 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.09/0.44 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.51 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.51 """
% 0.23/0.51 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.51 """
% 0.33/0.60 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.60 """
% 0.39/0.68 % Version: 1.5
% 0.39/0.68 % SZS status Theorem
% 0.39/0.68 % SZS output start CNFRefutation
% 0.39/0.68 fof(odrl604,conjecture,prec(v5,v5,o,o),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', odrl604)).
% 0.39/0.68 fof(c17,negated_conjecture,(~prec(v5,v5,o,o)),inference(assume_negation,[status(cth)],[odrl604])).
% 0.39/0.68 fof(c18,negated_conjecture,~prec(v5,v5,o,o),inference(fof_simplification,[status(thm)],[c17])).
% 0.39/0.68 cnf(c19,negated_conjecture,~prec(v5,v5,o,o),inference(split_conjunct,[status(thm)],[c18])).
% 0.39/0.68 cnf(reflexivity,axiom,X121=X121,theory(equality)).
% 0.39/0.68 fof(leq_def,axiom,(![X]:(![Y]:(leq(X,Y)<=>(less(X,Y)|X=Y)))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', leq_def)).
% 0.39/0.68 fof(c168,plain,(![X]:(![Y]:((~leq(X,Y)|(less(X,Y)|X=Y))&((~less(X,Y)&X!=Y)|leq(X,Y))))),inference(fof_nnf,[status(thm)],[leq_def])).
% 0.39/0.68 fof(c169,plain,((![X]:(![Y]:(~leq(X,Y)|(less(X,Y)|X=Y))))&(![X]:(![Y]:((~less(X,Y)&X!=Y)|leq(X,Y))))),inference(shift_quantors,[status(thm)],[c168])).
% 0.39/0.68 fof(c171,plain,(![X111]:(![X112]:(![X113]:(![X114]:((~leq(X111,X112)|(less(X111,X112)|X111=X112))&((~less(X113,X114)&X113!=X114)|leq(X113,X114))))))),inference(shift_quantors,[status(thm)],[fof(c170,plain,((![X111]:(![X112]:(~leq(X111,X112)|(less(X111,X112)|X111=X112))))&(![X113]:(![X114]:((~less(X113,X114)&X113!=X114)|leq(X113,X114))))),inference(variable_rename,[status(thm)],[c169])).])).
% 0.39/0.68 fof(c172,plain,(![X111]:(![X112]:(![X113]:(![X114]:((~leq(X111,X112)|(less(X111,X112)|X111=X112))&((~less(X113,X114)|leq(X113,X114))&(X113!=X114|leq(X113,X114)))))))),inference(distribute,[status(thm)],[c171])).
% 0.39/0.68 cnf(c175,plain,X146!=X145|leq(X146,X145),inference(split_conjunct,[status(thm)],[c172])).
% 0.39/0.68 cnf(c189,plain,leq(X147,X147),inference(resolution,[status(thm)],[c175, reflexivity])).
% 0.39/0.68 fof(prec_oo,axiom,(![U]:(![L]:(prec(U,L,o,o)<=>leq(U,L)))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+5.ax', prec_oo)).
% 0.39/0.68 fof(c39,plain,(![U]:(![L]:((~prec(U,L,o,o)|leq(U,L))&(~leq(U,L)|prec(U,L,o,o))))),inference(fof_nnf,[status(thm)],[prec_oo])).
% 0.39/0.68 fof(c40,plain,((![U]:(![L]:(~prec(U,L,o,o)|leq(U,L))))&(![U]:(![L]:(~leq(U,L)|prec(U,L,o,o))))),inference(shift_quantors,[status(thm)],[c39])).
% 0.39/0.68 fof(c42,plain,(![X18]:(![X19]:(![X20]:(![X21]:((~prec(X18,X19,o,o)|leq(X18,X19))&(~leq(X20,X21)|prec(X20,X21,o,o))))))),inference(shift_quantors,[status(thm)],[fof(c41,plain,((![X18]:(![X19]:(~prec(X18,X19,o,o)|leq(X18,X19))))&(![X20]:(![X21]:(~leq(X20,X21)|prec(X20,X21,o,o))))),inference(variable_rename,[status(thm)],[c40])).])).
% 0.39/0.68 cnf(c44,plain,~leq(X211,X210)|prec(X211,X210,o,o),inference(split_conjunct,[status(thm)],[c42])).
% 0.39/0.68 cnf(c194,plain,prec(X212,X212,o,o),inference(resolution,[status(thm)],[c44, c189])).
% 0.39/0.68 cnf(c196,plain,$false,inference(resolution,[status(thm)],[c194, c19])).
% 0.39/0.68 % SZS output end CNFRefutation
% 0.39/0.68
% 0.39/0.68 % Initial clauses : 92
% 0.39/0.68 % Processed clauses : 49
% 0.39/0.68 % Factors computed : 2
% 0.39/0.68 % Resolvents computed: 11
% 0.39/0.68 % Tautologies deleted: 5
% 0.39/0.68 % Forward subsumed : 2
% 0.39/0.68 % Backward subsumed : 0
% 0.39/0.68 % -------- CPU Time ---------
% 0.39/0.68 % User time : 0.283 s
% 0.39/0.68 % System time : 0.020 s
% 0.39/0.68 % Total time : 0.303 s
%------------------------------------------------------------------------------