%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT082+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.56s 0.80s
% Output : CNFRefutation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT082+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.03 % 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:56 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.13/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.38 (re.compile("\."), Token.FullStop),
% 0.13/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.38 (re.compile("\("), Token.OpenPar),
% 0.13/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.38 (re.compile("\)"), Token.ClosePar),
% 0.13/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.38 (re.compile("\["), Token.OpenSquare),
% 0.13/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.38 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.38 (re.compile("~\|"), Token.Nor),
% 0.13/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.38 (re.compile("\|"), Token.Or),
% 0.13/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.38 (re.compile("\?"), Token.Existential),
% 0.13/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.38 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.38 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.38 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.13/0.41 """
% 0.13/0.41 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.13/0.41 """
% 0.13/0.45 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.13/0.45 """
% 0.56/0.80 % Version: 1.5
% 0.56/0.80 % SZS status Theorem
% 0.56/0.80 % SZS output start CNFRefutation
% 0.56/0.80 fof(irreflexive,axiom,(![X]:(~less(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', irreflexive)).
% 0.56/0.80 fof(c183,plain,(![X]:~less(X,X)),inference(fof_simplification,[status(thm)],[irreflexive])).
% 0.56/0.80 fof(c184,plain,(![X90]:~less(X90,X90)),inference(variable_rename,[status(thm)],[c183])).
% 0.56/0.80 cnf(c185,plain,~less(X97,X97),inference(split_conjunct,[status(thm)],[c184])).
% 0.56/0.80 fof(ord_v600_v601,axiom,less(v600,v601),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ord_v600_v601)).
% 0.56/0.80 cnf(c43,plain,less(v600,v601),inference(split_conjunct,[status(thm)],[ord_v600_v601])).
% 0.56/0.80 fof(odrl411,conjecture,(~(?[X]:(?[Y]:(?[Z]:(((((in_closed(X,v600,v600)&in_closed(X,v601,v601))&less(v300,Y))&in_open(Y,v0,v500))&leq(v16,Z))&in_lopen(Z,v0,v32)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', odrl411)).
% 0.56/0.80 fof(c12,negated_conjecture,(~(~(?[X]:(?[Y]:(?[Z]:(((((in_closed(X,v600,v600)&in_closed(X,v601,v601))&less(v300,Y))&in_open(Y,v0,v500))&leq(v16,Z))&in_lopen(Z,v0,v32))))))),inference(assume_negation,[status(cth)],[odrl411])).
% 0.56/0.80 fof(c13,negated_conjecture,(?[X]:(?[Y]:(?[Z]:(((((in_closed(X,v600,v600)&in_closed(X,v601,v601))&less(v300,Y))&in_open(Y,v0,v500))&leq(v16,Z))&in_lopen(Z,v0,v32))))),inference(fof_nnf,[status(thm)],[c12])).
% 0.56/0.80 fof(c14,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(((((in_closed(X2,v600,v600)&in_closed(X2,v601,v601))&less(v300,X3))&in_open(X3,v0,v500))&leq(v16,X4))&in_lopen(X4,v0,v32))))),inference(variable_rename,[status(thm)],[c13])).
% 0.56/0.80 fof(c15,negated_conjecture,(((((in_closed(skolem0001,v600,v600)&in_closed(skolem0001,v601,v601))&less(v300,skolem0002))&in_open(skolem0002,v0,v500))&leq(v16,skolem0003))&in_lopen(skolem0003,v0,v32)),inference(skolemize,[status(esa)],[c14])).
% 0.56/0.80 cnf(c17,negated_conjecture,in_closed(skolem0001,v601,v601),inference(split_conjunct,[status(thm)],[c15])).
% 0.56/0.80 fof(in_closed,axiom,(![X]:(![A]:(![B]:(in_closed(X,A,B)<=>(leq(A,X)&leq(X,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax', in_closed)).
% 0.56/0.80 fof(c147,plain,(![X]:(![A]:(![B]:((~in_closed(X,A,B)|(leq(A,X)&leq(X,B)))&((~leq(A,X)|~leq(X,B))|in_closed(X,A,B)))))),inference(fof_nnf,[status(thm)],[in_closed])).
% 0.56/0.80 fof(c148,plain,((![X]:(![A]:(![B]:(~in_closed(X,A,B)|(leq(A,X)&leq(X,B))))))&(![X]:(![A]:(![B]:((~leq(A,X)|~leq(X,B))|in_closed(X,A,B)))))),inference(shift_quantors,[status(thm)],[c147])).
% 0.56/0.80 fof(c150,plain,(![X62]:(![X63]:(![X64]:(![X65]:(![X66]:(![X67]:((~in_closed(X62,X63,X64)|(leq(X63,X62)&leq(X62,X64)))&((~leq(X66,X65)|~leq(X65,X67))|in_closed(X65,X66,X67))))))))),inference(shift_quantors,[status(thm)],[fof(c149,plain,((![X62]:(![X63]:(![X64]:(~in_closed(X62,X63,X64)|(leq(X63,X62)&leq(X62,X64))))))&(![X65]:(![X66]:(![X67]:((~leq(X66,X65)|~leq(X65,X67))|in_closed(X65,X66,X67)))))),inference(variable_rename,[status(thm)],[c148])).])).
% 0.56/0.80 fof(c151,plain,(![X62]:(![X63]:(![X64]:(![X65]:(![X66]:(![X67]:(((~in_closed(X62,X63,X64)|leq(X63,X62))&(~in_closed(X62,X63,X64)|leq(X62,X64)))&((~leq(X66,X65)|~leq(X65,X67))|in_closed(X65,X66,X67))))))))),inference(distribute,[status(thm)],[c150])).
% 0.56/0.80 cnf(c152,plain,~in_closed(X208,X206,X207)|leq(X206,X208),inference(split_conjunct,[status(thm)],[c151])).
% 0.56/0.80 cnf(c293,plain,leq(v601,skolem0001),inference(resolution,[status(thm)],[c152, c17])).
% 0.56/0.80 cnf(c16,negated_conjecture,in_closed(skolem0001,v600,v600),inference(split_conjunct,[status(thm)],[c15])).
% 0.56/0.80 cnf(c153,plain,~in_closed(X216,X214,X215)|leq(X216,X215),inference(split_conjunct,[status(thm)],[c151])).
% 0.56/0.80 cnf(c298,plain,leq(skolem0001,v600),inference(resolution,[status(thm)],[c153, c16])).
% 0.56/0.80 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.56/0.80 fof(c155,plain,(![X]:(![Y]:(![Z]:((~leq(X,Y)|~leq(Y,Z))|leq(X,Z))))),inference(fof_nnf,[status(thm)],[leq_trans])).
% 0.56/0.80 fof(c156,plain,(![X68]:(![X69]:(![X70]:((~leq(X68,X69)|~leq(X69,X70))|leq(X68,X70))))),inference(variable_rename,[status(thm)],[c155])).
% 0.56/0.80 cnf(c157,plain,~leq(X219,X218)|~leq(X218,X217)|leq(X219,X217),inference(split_conjunct,[status(thm)],[c156])).
% 0.56/0.80 cnf(c304,plain,~leq(X239,skolem0001)|leq(X239,v600),inference(resolution,[status(thm)],[c157, c298])).
% 0.56/0.80 cnf(c368,plain,leq(v601,v600),inference(resolution,[status(thm)],[c304, c293])).
% 0.56/0.80 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.56/0.80 fof(c158,plain,(![X]:(![Y]:(![Z]:((~less(X,Y)|~leq(Y,Z))|less(X,Z))))),inference(fof_nnf,[status(thm)],[less_leq_trans])).
% 0.56/0.80 fof(c159,plain,(![X71]:(![X72]:(![X73]:((~less(X71,X72)|~leq(X72,X73))|less(X71,X73))))),inference(variable_rename,[status(thm)],[c158])).
% 0.56/0.80 cnf(c160,plain,~less(X284,X282)|~leq(X282,X283)|less(X284,X283),inference(split_conjunct,[status(thm)],[c159])).
% 0.56/0.80 cnf(c613,plain,~less(X557,v601)|less(X557,v600),inference(resolution,[status(thm)],[c160, c368])).
% 0.56/0.80 cnf(c1790,plain,less(v600,v600),inference(resolution,[status(thm)],[c613, c43])).
% 0.56/0.80 cnf(c1816,plain,$false,inference(resolution,[status(thm)],[c1790, c185])).
% 0.56/0.80 % SZS output end CNFRefutation
% 0.56/0.80
% 0.56/0.80 % Initial clauses : 115
% 0.56/0.80 % Processed clauses : 401
% 0.56/0.80 % Factors computed : 24
% 0.56/0.80 % Resolvents computed: 1607
% 0.56/0.80 % Tautologies deleted: 9
% 0.56/0.80 % Forward subsumed : 365
% 0.56/0.80 % Backward subsumed : 1
% 0.56/0.80 % -------- CPU Time ---------
% 0.56/0.80 % User time : 0.431 s
% 0.56/0.80 % System time : 0.016 s
% 0.56/0.80 % Total time : 0.447 s
%------------------------------------------------------------------------------