%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT081+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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.67s 0.91s
% Output : CNFRefutation 0.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT081+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.35 % Computer : n007.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 14:14:11 UTC 2026
% 0.10/0.35 % 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.41 (re.compile("\?"), Token.Existential),
% 0.13/0.41 /export/starexec/sandbox2/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/sandbox2/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/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.48 """
% 0.22/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.48 """
% 0.33/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.57 """
% 0.67/0.91 % Version: 1.5
% 0.67/0.91 % SZS status Theorem
% 0.67/0.91 % SZS output start CNFRefutation
% 0.67/0.91 fof(irreflexive,axiom,(![X]:(~less(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', irreflexive)).
% 0.67/0.91 fof(c157,plain,(![X]:~less(X,X)),inference(fof_simplification,[status(thm)],[irreflexive])).
% 0.67/0.91 fof(c158,plain,(![X89]:~less(X89,X89)),inference(variable_rename,[status(thm)],[c157])).
% 0.67/0.91 cnf(c159,plain,~less(X93,X93),inference(split_conjunct,[status(thm)],[c158])).
% 0.67/0.91 fof(ord_v600_v800,axiom,less(v600,v800),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ord_v600_v800)).
% 0.67/0.91 cnf(c30,plain,less(v600,v800),inference(split_conjunct,[status(thm)],[ord_v600_v800])).
% 0.67/0.91 fof(ord_v400_v600,axiom,less(v400,v600),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ord_v400_v600)).
% 0.67/0.91 cnf(c32,plain,less(v400,v600),inference(split_conjunct,[status(thm)],[ord_v400_v600])).
% 0.67/0.91 fof(less_implies_leq,axiom,(![X]:(![Y]:(less(X,Y)=>leq(X,Y)))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', less_implies_leq)).
% 0.67/0.91 fof(c138,plain,(![X]:(![Y]:(~less(X,Y)|leq(X,Y)))),inference(fof_nnf,[status(thm)],[less_implies_leq])).
% 0.67/0.91 fof(c139,plain,(![X76]:(![X77]:(~less(X76,X77)|leq(X76,X77)))),inference(variable_rename,[status(thm)],[c138])).
% 0.67/0.91 cnf(c140,plain,~less(X123,X122)|leq(X123,X122),inference(split_conjunct,[status(thm)],[c139])).
% 0.67/0.91 cnf(c187,plain,leq(v400,v600),inference(resolution,[status(thm)],[c140, c32])).
% 0.67/0.91 fof(leq_trans,axiom,(![X]:(![Y]:(![Z]:((leq(X,Y)&leq(Y,Z))=>leq(X,Z))))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', leq_trans)).
% 0.67/0.91 fof(c129,plain,(![X]:(![Y]:(![Z]:((~leq(X,Y)|~leq(Y,Z))|leq(X,Z))))),inference(fof_nnf,[status(thm)],[leq_trans])).
% 0.67/0.91 fof(c130,plain,(![X67]:(![X68]:(![X69]:((~leq(X67,X68)|~leq(X68,X69))|leq(X67,X69))))),inference(variable_rename,[status(thm)],[c129])).
% 0.67/0.91 cnf(c131,plain,~leq(X200,X202)|~leq(X202,X201)|leq(X200,X201),inference(split_conjunct,[status(thm)],[c130])).
% 0.67/0.91 cnf(c223,plain,~leq(X213,v400)|leq(X213,v600),inference(resolution,[status(thm)],[c131, c187])).
% 0.67/0.91 fof(odrl402,conjecture,(~(?[X]:(?[Y]:(((in_lopen(X,v0,v400)&leq(v800,X))&in_lopen(Y,v0,v600))&leq(v200,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', odrl402)).
% 0.67/0.91 fof(c12,negated_conjecture,(~(~(?[X]:(?[Y]:(((in_lopen(X,v0,v400)&leq(v800,X))&in_lopen(Y,v0,v600))&leq(v200,Y)))))),inference(assume_negation,[status(cth)],[odrl402])).
% 0.67/0.91 fof(c13,negated_conjecture,(?[X]:(?[Y]:(((in_lopen(X,v0,v400)&leq(v800,X))&in_lopen(Y,v0,v600))&leq(v200,Y)))),inference(fof_nnf,[status(thm)],[c12])).
% 0.67/0.91 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(((in_lopen(X2,v0,v400)&leq(v800,X2))&in_lopen(X3,v0,v600))&leq(v200,X3)))),inference(variable_rename,[status(thm)],[c13])).
% 0.67/0.91 fof(c15,negated_conjecture,(((in_lopen(skolem0001,v0,v400)&leq(v800,skolem0001))&in_lopen(skolem0002,v0,v600))&leq(v200,skolem0002)),inference(skolemize,[status(esa)],[c14])).
% 0.67/0.91 cnf(c17,negated_conjecture,leq(v800,skolem0001),inference(split_conjunct,[status(thm)],[c15])).
% 0.67/0.91 cnf(c16,negated_conjecture,in_lopen(skolem0001,v0,v400),inference(split_conjunct,[status(thm)],[c15])).
% 0.67/0.91 fof(in_lopen,axiom,(![X]:(![A]:(![B]:(in_lopen(X,A,B)<=>(less(A,X)&leq(X,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax', in_lopen)).
% 0.67/0.91 fof(c113,plain,(![X]:(![A]:(![B]:((~in_lopen(X,A,B)|(less(A,X)&leq(X,B)))&((~less(A,X)|~leq(X,B))|in_lopen(X,A,B)))))),inference(fof_nnf,[status(thm)],[in_lopen])).
% 0.67/0.91 fof(c114,plain,((![X]:(![A]:(![B]:(~in_lopen(X,A,B)|(less(A,X)&leq(X,B))))))&(![X]:(![A]:(![B]:((~less(A,X)|~leq(X,B))|in_lopen(X,A,B)))))),inference(shift_quantors,[status(thm)],[c113])).
% 0.67/0.91 fof(c116,plain,(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:((~in_lopen(X55,X56,X57)|(less(X56,X55)&leq(X55,X57)))&((~less(X59,X58)|~leq(X58,X60))|in_lopen(X58,X59,X60))))))))),inference(shift_quantors,[status(thm)],[fof(c115,plain,((![X55]:(![X56]:(![X57]:(~in_lopen(X55,X56,X57)|(less(X56,X55)&leq(X55,X57))))))&(![X58]:(![X59]:(![X60]:((~less(X59,X58)|~leq(X58,X60))|in_lopen(X58,X59,X60)))))),inference(variable_rename,[status(thm)],[c114])).])).
% 0.67/0.91 fof(c117,plain,(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:(((~in_lopen(X55,X56,X57)|less(X56,X55))&(~in_lopen(X55,X56,X57)|leq(X55,X57)))&((~less(X59,X58)|~leq(X58,X60))|in_lopen(X58,X59,X60))))))))),inference(distribute,[status(thm)],[c116])).
% 0.67/0.91 cnf(c119,plain,~in_lopen(X185,X184,X183)|leq(X185,X183),inference(split_conjunct,[status(thm)],[c117])).
% 0.67/0.91 cnf(c209,plain,leq(skolem0001,v400),inference(resolution,[status(thm)],[c119, c16])).
% 0.67/0.91 cnf(c231,plain,~leq(X232,skolem0001)|leq(X232,v400),inference(resolution,[status(thm)],[c131, c209])).
% 0.67/0.91 cnf(c280,plain,leq(v800,v400),inference(resolution,[status(thm)],[c231, c17])).
% 0.67/0.91 cnf(c291,plain,leq(v800,v600),inference(resolution,[status(thm)],[c280, c223])).
% 0.67/0.91 fof(less_leq_trans,axiom,(![X]:(![Y]:(![Z]:((less(X,Y)&leq(Y,Z))=>less(X,Z))))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', less_leq_trans)).
% 0.67/0.91 fof(c132,plain,(![X]:(![Y]:(![Z]:((~less(X,Y)|~leq(Y,Z))|less(X,Z))))),inference(fof_nnf,[status(thm)],[less_leq_trans])).
% 0.67/0.91 fof(c133,plain,(![X70]:(![X71]:(![X72]:((~less(X70,X71)|~leq(X71,X72))|less(X70,X72))))),inference(variable_rename,[status(thm)],[c132])).
% 0.67/0.91 cnf(c134,plain,~less(X292,X293)|~leq(X293,X291)|less(X292,X291),inference(split_conjunct,[status(thm)],[c133])).
% 0.67/0.91 cnf(c459,plain,~less(X405,v800)|less(X405,v600),inference(resolution,[status(thm)],[c134, c291])).
% 0.67/0.91 cnf(c894,plain,less(v600,v600),inference(resolution,[status(thm)],[c459, c30])).
% 0.67/0.91 cnf(c899,plain,$false,inference(resolution,[status(thm)],[c894, c159])).
% 0.67/0.91 % SZS output end CNFRefutation
% 0.67/0.91
% 0.67/0.91 % Initial clauses : 89
% 0.67/0.91 % Processed clauses : 222
% 0.67/0.91 % Factors computed : 12
% 0.67/0.91 % Resolvents computed: 733
% 0.67/0.91 % Tautologies deleted: 9
% 0.67/0.91 % Forward subsumed : 196
% 0.67/0.91 % Backward subsumed : 1
% 0.67/0.91 % -------- CPU Time ---------
% 0.67/0.91 % User time : 0.536 s
% 0.67/0.91 % System time : 0.023 s
% 0.67/0.91 % Total time : 0.559 s
%------------------------------------------------------------------------------