%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT083+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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.18s 0.43s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT083+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.02 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.04/0.29 % Computer : n012.cluster.edu
% 0.04/0.29 % Model : x86_64 x86_64
% 0.04/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.29 % Memory : 8046.5625MB
% 0.04/0.29 % OS : Linux 6.8.0-71-generic
% 0.04/0.29 % CPULimit : 300
% 0.04/0.29 % WCLimit : 300
% 0.04/0.29 % DateTime : Mon Sep 7 14:17:56 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.32 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.04/0.32 (re.compile("\."), Token.FullStop),
% 0.04/0.32 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.04/0.32 (re.compile("\("), Token.OpenPar),
% 0.04/0.32 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.04/0.32 (re.compile("\)"), Token.ClosePar),
% 0.04/0.32 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.04/0.32 (re.compile("\["), Token.OpenSquare),
% 0.04/0.32 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.04/0.33 (re.compile("\]"), Token.CloseSquare),
% 0.04/0.33 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.04/0.33 (re.compile("~\|"), Token.Nor),
% 0.08/0.33 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.08/0.33 (re.compile("\|"), Token.Or),
% 0.08/0.33 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.08/0.33 (re.compile("\?"), Token.Existential),
% 0.08/0.33 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.08/0.33 (re.compile("\s+"), Token.WhiteSpace),
% 0.08/0.33 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.08/0.33 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.08/0.36 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.08/0.36 """
% 0.08/0.36 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.08/0.36 """
% 0.08/0.39 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.08/0.39 """
% 0.18/0.43 % Version: 1.5
% 0.18/0.43 % SZS status Theorem
% 0.18/0.43 % SZS output start CNFRefutation
% 0.18/0.43 fof(irreflexive,axiom,(![X]:(~less(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', irreflexive)).
% 0.18/0.43 fof(c134,plain,(![X]:~less(X,X)),inference(fof_simplification,[status(thm)],[irreflexive])).
% 0.18/0.43 fof(c135,plain,(![X88]:~less(X88,X88)),inference(variable_rename,[status(thm)],[c134])).
% 0.18/0.43 cnf(c136,plain,~less(X92,X92),inference(split_conjunct,[status(thm)],[c135])).
% 0.18/0.43 fof(odrl423,conjecture,(~(?[X]:(in_open(X,v0,v600)&less(v600,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', odrl423)).
% 0.18/0.43 fof(c12,negated_conjecture,(~(~(?[X]:(in_open(X,v0,v600)&less(v600,X))))),inference(assume_negation,[status(cth)],[odrl423])).
% 0.18/0.43 fof(c13,negated_conjecture,(?[X]:(in_open(X,v0,v600)&less(v600,X))),inference(fof_nnf,[status(thm)],[c12])).
% 0.18/0.43 fof(c14,negated_conjecture,(?[X2]:(in_open(X2,v0,v600)&less(v600,X2))),inference(variable_rename,[status(thm)],[c13])).
% 0.18/0.43 fof(c15,negated_conjecture,(in_open(skolem0001,v0,v600)&less(v600,skolem0001)),inference(skolemize,[status(esa)],[c14])).
% 0.18/0.43 cnf(c17,negated_conjecture,less(v600,skolem0001),inference(split_conjunct,[status(thm)],[c15])).
% 0.18/0.43 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.18/0.43 fof(c115,plain,(![X]:(![Y]:(~less(X,Y)|leq(X,Y)))),inference(fof_nnf,[status(thm)],[less_implies_leq])).
% 0.18/0.43 fof(c116,plain,(![X75]:(![X76]:(~less(X75,X76)|leq(X75,X76)))),inference(variable_rename,[status(thm)],[c115])).
% 0.18/0.43 cnf(c117,plain,~less(X101,X102)|leq(X101,X102),inference(split_conjunct,[status(thm)],[c116])).
% 0.18/0.43 cnf(c16,negated_conjecture,in_open(skolem0001,v0,v600),inference(split_conjunct,[status(thm)],[c15])).
% 0.18/0.43 fof(in_open,axiom,(![X]:(![A]:(![B]:(in_open(X,A,B)<=>(less(A,X)&less(X,B)))))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+2.ax', in_open)).
% 0.18/0.43 fof(c74,plain,(![X]:(![A]:(![B]:((~in_open(X,A,B)|(less(A,X)&less(X,B)))&((~less(A,X)|~less(X,B))|in_open(X,A,B)))))),inference(fof_nnf,[status(thm)],[in_open])).
% 0.18/0.43 fof(c75,plain,((![X]:(![A]:(![B]:(~in_open(X,A,B)|(less(A,X)&less(X,B))))))&(![X]:(![A]:(![B]:((~less(A,X)|~less(X,B))|in_open(X,A,B)))))),inference(shift_quantors,[status(thm)],[c74])).
% 0.18/0.43 fof(c77,plain,(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:((~in_open(X42,X43,X44)|(less(X43,X42)&less(X42,X44)))&((~less(X46,X45)|~less(X45,X47))|in_open(X45,X46,X47))))))))),inference(shift_quantors,[status(thm)],[fof(c76,plain,((![X42]:(![X43]:(![X44]:(~in_open(X42,X43,X44)|(less(X43,X42)&less(X42,X44))))))&(![X45]:(![X46]:(![X47]:((~less(X46,X45)|~less(X45,X47))|in_open(X45,X46,X47)))))),inference(variable_rename,[status(thm)],[c75])).])).
% 0.18/0.43 fof(c78,plain,(![X42]:(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(((~in_open(X42,X43,X44)|less(X43,X42))&(~in_open(X42,X43,X44)|less(X42,X44)))&((~less(X46,X45)|~less(X45,X47))|in_open(X45,X46,X47))))))))),inference(distribute,[status(thm)],[c77])).
% 0.18/0.43 cnf(c80,plain,~in_open(X123,X124,X122)|less(X123,X122),inference(split_conjunct,[status(thm)],[c78])).
% 0.18/0.43 cnf(c154,plain,less(skolem0001,v600),inference(resolution,[status(thm)],[c80, c16])).
% 0.18/0.43 cnf(c155,plain,leq(skolem0001,v600),inference(resolution,[status(thm)],[c154, c117])).
% 0.18/0.43 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.18/0.43 fof(c109,plain,(![X]:(![Y]:(![Z]:((~less(X,Y)|~leq(Y,Z))|less(X,Z))))),inference(fof_nnf,[status(thm)],[less_leq_trans])).
% 0.18/0.43 fof(c110,plain,(![X69]:(![X70]:(![X71]:((~less(X69,X70)|~leq(X70,X71))|less(X69,X71))))),inference(variable_rename,[status(thm)],[c109])).
% 0.18/0.43 cnf(c111,plain,~less(X193,X191)|~leq(X191,X192)|less(X193,X192),inference(split_conjunct,[status(thm)],[c110])).
% 0.18/0.43 cnf(c176,plain,~less(X205,skolem0001)|less(X205,v600),inference(resolution,[status(thm)],[c111, c155])).
% 0.18/0.43 cnf(c180,plain,less(v600,v600),inference(resolution,[status(thm)],[c176, c17])).
% 0.18/0.43 cnf(c183,plain,$false,inference(resolution,[status(thm)],[c180, c136])).
% 0.18/0.43 % SZS output end CNFRefutation
% 0.18/0.43
% 0.18/0.43 % Initial clauses : 66
% 0.18/0.43 % Processed clauses : 53
% 0.18/0.43 % Factors computed : 3
% 0.18/0.43 % Resolvents computed: 45
% 0.18/0.43 % Tautologies deleted: 7
% 0.18/0.43 % Forward subsumed : 10
% 0.18/0.43 % Backward subsumed : 0
% 0.18/0.43 % -------- CPU Time ---------
% 0.18/0.43 % User time : 0.119 s
% 0.18/0.43 % System time : 0.011 s
% 0.18/0.43 % Total time : 0.130 s
%------------------------------------------------------------------------------