%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT084+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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.92s
% Output : CNFRefutation 0.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT084+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.36 % Computer : n016.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 7 14:23:17 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.15/0.43 (re.compile("\."), Token.FullStop),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.15/0.43 (re.compile("\("), Token.OpenPar),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.15/0.43 (re.compile("\)"), Token.ClosePar),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.15/0.43 (re.compile("\["), Token.OpenSquare),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.15/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.15/0.43 (re.compile("~\|"), Token.Nor),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.15/0.43 (re.compile("\|"), Token.Or),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.15/0.43 (re.compile("\?"), Token.Existential),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.15/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.15/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.15/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.25/0.50 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.25/0.50 """
% 0.25/0.50 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.25/0.50 """
% 0.34/0.59 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.34/0.59 """
% 0.67/0.92 % Version: 1.5
% 0.67/0.92 % SZS status Theorem
% 0.67/0.92 % SZS output start CNFRefutation
% 0.67/0.92 fof(irreflexive,axiom,(![X]:(~less(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', irreflexive)).
% 0.67/0.92 fof(c150,plain,(![X]:~less(X,X)),inference(fof_simplification,[status(thm)],[irreflexive])).
% 0.67/0.92 fof(c151,plain,(![X90]:~less(X90,X90)),inference(variable_rename,[status(thm)],[c150])).
% 0.67/0.92 cnf(c152,plain,~less(X94,X94),inference(split_conjunct,[status(thm)],[c151])).
% 0.67/0.92 fof(odrl432,conjecture,(~(?[X]:(?[Y]:(?[Z]:(((((in_lopen(X,v0,v600)&leq(v600,X))&in_lopen(Y,v0,v400))&less(v400,Y))&in_lopen(Z,v0,v200))&leq(v200,Z)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', odrl432)).
% 0.67/0.92 fof(c12,negated_conjecture,(~(~(?[X]:(?[Y]:(?[Z]:(((((in_lopen(X,v0,v600)&leq(v600,X))&in_lopen(Y,v0,v400))&less(v400,Y))&in_lopen(Z,v0,v200))&leq(v200,Z))))))),inference(assume_negation,[status(cth)],[odrl432])).
% 0.67/0.92 fof(c13,negated_conjecture,(?[X]:(?[Y]:(?[Z]:(((((in_lopen(X,v0,v600)&leq(v600,X))&in_lopen(Y,v0,v400))&less(v400,Y))&in_lopen(Z,v0,v200))&leq(v200,Z))))),inference(fof_nnf,[status(thm)],[c12])).
% 0.67/0.92 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(((((in_lopen(X2,v0,v600)&leq(v600,X2))&in_lopen(X3,v0,v400))&less(v400,X3))&in_lopen(X4,v0,v200))&leq(v200,X4))))),inference(variable_rename,[status(thm)],[c13])).
% 0.67/0.92 fof(c15,negated_conjecture,(((((in_lopen(skolem0001,v0,v600)&leq(v600,skolem0001))&in_lopen(skolem0002,v0,v400))&less(v400,skolem0002))&in_lopen(skolem0003,v0,v200))&leq(v200,skolem0003)),inference(skolemize,[status(esa)],[c14])).
% 0.67/0.92 cnf(c19,negated_conjecture,less(v400,skolem0002),inference(split_conjunct,[status(thm)],[c15])).
% 0.67/0.92 cnf(c18,negated_conjecture,in_lopen(skolem0002,v0,v400),inference(split_conjunct,[status(thm)],[c15])).
% 0.67/0.92 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.92 fof(c106,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.92 fof(c107,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)],[c106])).
% 0.67/0.92 fof(c109,plain,(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:((~in_lopen(X56,X57,X58)|(less(X57,X56)&leq(X56,X58)))&((~less(X60,X59)|~leq(X59,X61))|in_lopen(X59,X60,X61))))))))),inference(shift_quantors,[status(thm)],[fof(c108,plain,((![X56]:(![X57]:(![X58]:(~in_lopen(X56,X57,X58)|(less(X57,X56)&leq(X56,X58))))))&(![X59]:(![X60]:(![X61]:((~less(X60,X59)|~leq(X59,X61))|in_lopen(X59,X60,X61)))))),inference(variable_rename,[status(thm)],[c107])).])).
% 0.67/0.92 fof(c110,plain,(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:(((~in_lopen(X56,X57,X58)|less(X57,X56))&(~in_lopen(X56,X57,X58)|leq(X56,X58)))&((~less(X60,X59)|~leq(X59,X61))|in_lopen(X59,X60,X61))))))))),inference(distribute,[status(thm)],[c109])).
% 0.67/0.92 cnf(c112,plain,~in_lopen(X177,X178,X176)|leq(X177,X176),inference(split_conjunct,[status(thm)],[c110])).
% 0.67/0.92 cnf(c199,plain,leq(skolem0002,v400),inference(resolution,[status(thm)],[c112, c18])).
% 0.67/0.92 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.92 fof(c125,plain,(![X]:(![Y]:(![Z]:((~less(X,Y)|~leq(Y,Z))|less(X,Z))))),inference(fof_nnf,[status(thm)],[less_leq_trans])).
% 0.67/0.92 fof(c126,plain,(![X71]:(![X72]:(![X73]:((~less(X71,X72)|~leq(X72,X73))|less(X71,X73))))),inference(variable_rename,[status(thm)],[c125])).
% 0.67/0.92 cnf(c127,plain,~less(X298,X299)|~leq(X299,X297)|less(X298,X297),inference(split_conjunct,[status(thm)],[c126])).
% 0.67/0.92 cnf(c452,plain,~less(X424,skolem0002)|less(X424,v400),inference(resolution,[status(thm)],[c127, c199])).
% 0.67/0.92 cnf(c888,plain,less(v400,v400),inference(resolution,[status(thm)],[c452, c19])).
% 0.67/0.92 cnf(c899,plain,$false,inference(resolution,[status(thm)],[c888, c152])).
% 0.67/0.92 % SZS output end CNFRefutation
% 0.67/0.92
% 0.67/0.92 % Initial clauses : 82
% 0.67/0.92 % Processed clauses : 231
% 0.67/0.92 % Factors computed : 12
% 0.67/0.92 % Resolvents computed: 739
% 0.67/0.92 % Tautologies deleted: 9
% 0.67/0.92 % Forward subsumed : 183
% 0.67/0.92 % Backward subsumed : 1
% 0.67/0.92 % -------- CPU Time ---------
% 0.67/0.92 % User time : 0.525 s
% 0.67/0.92 % System time : 0.029 s
% 0.67/0.92 % Total time : 0.554 s
%------------------------------------------------------------------------------