%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT106+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:52 AM UTC 2026
% Result : Unsatisfiable 0.41s 0.67s
% Output : CNFRefutation 0.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT106+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 14:41:56 UTC 2026
% 0.09/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.23/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.48 """
% 0.23/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.48 """
% 0.34/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.34/0.57 """
% 0.41/0.67 % Version: 1.5
% 0.41/0.67 % SZS status Unsatisfiable
% 0.41/0.67 % SZS output start CNFRefutation
% 0.41/0.67 fof(irreflexive,axiom,(![X]:(~less(X,X))),file('/export/starexec/sandbox2/benchmark/Axioms/MGT002+0.ax', irreflexive)).
% 0.41/0.67 fof(c135,plain,(![X]:~less(X,X)),inference(fof_simplification,[status(thm)],[irreflexive])).
% 0.41/0.67 fof(c136,plain,(![X87]:~less(X87,X87)),inference(variable_rename,[status(thm)],[c135])).
% 0.41/0.67 cnf(c137,plain,~less(X91,X91),inference(split_conjunct,[status(thm)],[c136])).
% 0.41/0.67 fof(ord_v600_v800,axiom,less(v600,v800),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ord_v600_v800)).
% 0.41/0.67 cnf(c18,plain,less(v600,v800),inference(split_conjunct,[status(thm)],[ord_v600_v800])).
% 0.41/0.67 fof(wit_leq,axiom,leq(v800,w),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', wit_leq)).
% 0.41/0.67 cnf(c12,plain,leq(v800,w),inference(split_conjunct,[status(thm)],[wit_leq])).
% 0.41/0.67 fof(wit_in_lopen,axiom,in_lopen(w,v0,v600),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', wit_in_lopen)).
% 0.41/0.67 cnf(c13,plain,in_lopen(w,v0,v600),inference(split_conjunct,[status(thm)],[wit_in_lopen])).
% 0.41/0.67 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.41/0.67 fof(c91,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.41/0.67 fof(c92,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)],[c91])).
% 0.41/0.67 fof(c94,plain,(![X53]:(![X54]:(![X55]:(![X56]:(![X57]:(![X58]:((~in_lopen(X53,X54,X55)|(less(X54,X53)&leq(X53,X55)))&((~less(X57,X56)|~leq(X56,X58))|in_lopen(X56,X57,X58))))))))),inference(shift_quantors,[status(thm)],[fof(c93,plain,((![X53]:(![X54]:(![X55]:(~in_lopen(X53,X54,X55)|(less(X54,X53)&leq(X53,X55))))))&(![X56]:(![X57]:(![X58]:((~less(X57,X56)|~leq(X56,X58))|in_lopen(X56,X57,X58)))))),inference(variable_rename,[status(thm)],[c92])).])).
% 0.41/0.67 fof(c95,plain,(![X53]:(![X54]:(![X55]:(![X56]:(![X57]:(![X58]:(((~in_lopen(X53,X54,X55)|less(X54,X53))&(~in_lopen(X53,X54,X55)|leq(X53,X55)))&((~less(X57,X56)|~leq(X56,X58))|in_lopen(X56,X57,X58))))))))),inference(distribute,[status(thm)],[c94])).
% 0.41/0.67 cnf(c97,plain,~in_lopen(X145,X146,X147)|leq(X145,X147),inference(split_conjunct,[status(thm)],[c95])).
% 0.41/0.67 cnf(c157,plain,leq(w,v600),inference(resolution,[status(thm)],[c97, c13])).
% 0.41/0.67 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.41/0.67 fof(c107,plain,(![X]:(![Y]:(![Z]:((~leq(X,Y)|~leq(Y,Z))|leq(X,Z))))),inference(fof_nnf,[status(thm)],[leq_trans])).
% 0.41/0.67 fof(c108,plain,(![X65]:(![X66]:(![X67]:((~leq(X65,X66)|~leq(X66,X67))|leq(X65,X67))))),inference(variable_rename,[status(thm)],[c107])).
% 0.41/0.67 cnf(c109,plain,~leq(X167,X168)|~leq(X168,X166)|leq(X167,X166),inference(split_conjunct,[status(thm)],[c108])).
% 0.41/0.67 cnf(c164,plain,~leq(X187,w)|leq(X187,v600),inference(resolution,[status(thm)],[c109, c157])).
% 0.41/0.67 cnf(c177,plain,leq(v800,v600),inference(resolution,[status(thm)],[c164, c12])).
% 0.41/0.67 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.41/0.67 fof(c110,plain,(![X]:(![Y]:(![Z]:((~less(X,Y)|~leq(Y,Z))|less(X,Z))))),inference(fof_nnf,[status(thm)],[less_leq_trans])).
% 0.41/0.67 fof(c111,plain,(![X68]:(![X69]:(![X70]:((~less(X68,X69)|~leq(X69,X70))|less(X68,X70))))),inference(variable_rename,[status(thm)],[c110])).
% 0.41/0.67 cnf(c112,plain,~less(X221,X219)|~leq(X219,X220)|less(X221,X220),inference(split_conjunct,[status(thm)],[c111])).
% 0.41/0.67 cnf(c215,plain,~less(X232,v800)|less(X232,v600),inference(resolution,[status(thm)],[c112, c177])).
% 0.41/0.67 cnf(c228,plain,less(v600,v600),inference(resolution,[status(thm)],[c215, c18])).
% 0.41/0.67 cnf(c231,plain,$false,inference(resolution,[status(thm)],[c228, c137])).
% 0.41/0.67 % SZS output end CNFRefutation
% 0.41/0.67
% 0.41/0.67 % Initial clauses : 71
% 0.41/0.67 % Processed clauses : 77
% 0.41/0.67 % Factors computed : 5
% 0.41/0.67 % Resolvents computed: 92
% 0.41/0.67 % Tautologies deleted: 7
% 0.41/0.67 % Forward subsumed : 28
% 0.41/0.67 % Backward subsumed : 0
% 0.41/0.67 % -------- CPU Time ---------
% 0.41/0.67 % User time : 0.294 s
% 0.41/0.67 % System time : 0.029 s
% 0.41/0.67 % Total time : 0.323 s
%------------------------------------------------------------------------------