%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT088+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.19s 0.48s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT088+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.02 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 7 14:21:41 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.09/0.33 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.33 (re.compile("\."), Token.FullStop),
% 0.09/0.33 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.33 (re.compile("\("), Token.OpenPar),
% 0.09/0.33 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.33 (re.compile("\)"), Token.ClosePar),
% 0.09/0.33 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.33 (re.compile("\["), Token.OpenSquare),
% 0.09/0.33 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.33 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.33 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.33 (re.compile("~\|"), Token.Nor),
% 0.09/0.33 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.33 (re.compile("\|"), Token.Or),
% 0.09/0.33 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.33 (re.compile("\?"), Token.Existential),
% 0.09/0.33 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.09/0.33 (re.compile("\s+"), Token.WhiteSpace),
% 0.09/0.33 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.09/0.33 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.09/0.36 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.09/0.36 """
% 0.09/0.36 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.09/0.36 """
% 0.09/0.40 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.09/0.40 """
% 0.19/0.48 % Version: 1.5
% 0.19/0.48 % SZS status Theorem
% 0.19/0.48 % SZS output start CNFRefutation
% 0.19/0.48 fof(ord_v200_v400,axiom,less(v200,v400),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ord_v200_v400)).
% 0.19/0.48 cnf(c24,plain,less(v200,v400),inference(split_conjunct,[status(thm)],[ord_v200_v400])).
% 0.19/0.48 fof(odrl509,conjecture,(?[X]:(less(v200,X)&in_lopen(X,v0,v400))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', odrl509)).
% 0.19/0.48 fof(c12,negated_conjecture,(~(?[X]:(less(v200,X)&in_lopen(X,v0,v400)))),inference(assume_negation,[status(cth)],[odrl509])).
% 0.19/0.48 fof(c13,negated_conjecture,(![X]:(~less(v200,X)|~in_lopen(X,v0,v400))),inference(fof_nnf,[status(thm)],[c12])).
% 0.19/0.48 fof(c14,negated_conjecture,(![X2]:(~less(v200,X2)|~in_lopen(X2,v0,v400))),inference(variable_rename,[status(thm)],[c13])).
% 0.19/0.48 cnf(c15,negated_conjecture,~less(v200,X204)|~in_lopen(X204,v0,v400),inference(split_conjunct,[status(thm)],[c14])).
% 0.19/0.48 fof(ord_v0_v400,axiom,less(v0,v400),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ord_v0_v400)).
% 0.19/0.48 cnf(c26,plain,less(v0,v400),inference(split_conjunct,[status(thm)],[ord_v0_v400])).
% 0.19/0.48 cnf(reflexivity,axiom,X92=X92,theory(equality)).
% 0.19/0.48 fof(leq_def,axiom,(![X]:(![Y]:(leq(X,Y)<=>(less(X,Y)|X=Y)))),file('/export/starexec/sandbox/benchmark/Axioms/MGT002+0.ax', leq_def)).
% 0.19/0.48 fof(c137,plain,(![X]:(![Y]:((~leq(X,Y)|(less(X,Y)|X=Y))&((~less(X,Y)&X!=Y)|leq(X,Y))))),inference(fof_nnf,[status(thm)],[leq_def])).
% 0.19/0.48 fof(c138,plain,((![X]:(![Y]:(~leq(X,Y)|(less(X,Y)|X=Y))))&(![X]:(![Y]:((~less(X,Y)&X!=Y)|leq(X,Y))))),inference(shift_quantors,[status(thm)],[c137])).
% 0.19/0.48 fof(c140,plain,(![X82]:(![X83]:(![X84]:(![X85]:((~leq(X82,X83)|(less(X82,X83)|X82=X83))&((~less(X84,X85)&X84!=X85)|leq(X84,X85))))))),inference(shift_quantors,[status(thm)],[fof(c139,plain,((![X82]:(![X83]:(~leq(X82,X83)|(less(X82,X83)|X82=X83))))&(![X84]:(![X85]:((~less(X84,X85)&X84!=X85)|leq(X84,X85))))),inference(variable_rename,[status(thm)],[c138])).])).
% 0.19/0.48 fof(c141,plain,(![X82]:(![X83]:(![X84]:(![X85]:((~leq(X82,X83)|(less(X82,X83)|X82=X83))&((~less(X84,X85)|leq(X84,X85))&(X84!=X85|leq(X84,X85)))))))),inference(distribute,[status(thm)],[c140])).
% 0.19/0.48 cnf(c144,plain,X122!=X123|leq(X122,X123),inference(split_conjunct,[status(thm)],[c141])).
% 0.19/0.48 cnf(c176,plain,leq(X124,X124),inference(resolution,[status(thm)],[c144, reflexivity])).
% 0.19/0.48 fof(in_lopen,axiom,(![X]:(![A]:(![B]:(in_lopen(X,A,B)<=>(less(A,X)&leq(X,B)))))),file('/export/starexec/sandbox/benchmark/Axioms/MGT002+2.ax', in_lopen)).
% 0.19/0.48 fof(c100,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.19/0.48 fof(c101,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)],[c100])).
% 0.19/0.48 fof(c103,plain,(![X54]:(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:((~in_lopen(X54,X55,X56)|(less(X55,X54)&leq(X54,X56)))&((~less(X58,X57)|~leq(X57,X59))|in_lopen(X57,X58,X59))))))))),inference(shift_quantors,[status(thm)],[fof(c102,plain,((![X54]:(![X55]:(![X56]:(~in_lopen(X54,X55,X56)|(less(X55,X54)&leq(X54,X56))))))&(![X57]:(![X58]:(![X59]:((~less(X58,X57)|~leq(X57,X59))|in_lopen(X57,X58,X59)))))),inference(variable_rename,[status(thm)],[c101])).])).
% 0.19/0.48 fof(c104,plain,(![X54]:(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:(((~in_lopen(X54,X55,X56)|less(X55,X54))&(~in_lopen(X54,X55,X56)|leq(X54,X56)))&((~less(X58,X57)|~leq(X57,X59))|in_lopen(X57,X58,X59))))))))),inference(distribute,[status(thm)],[c103])).
% 0.19/0.48 cnf(c107,plain,~less(X323,X324)|~leq(X324,X325)|in_lopen(X324,X323,X325),inference(split_conjunct,[status(thm)],[c104])).
% 0.19/0.48 cnf(c603,plain,~less(X327,X326)|in_lopen(X326,X327,X326),inference(resolution,[status(thm)],[c107, c176])).
% 0.19/0.48 cnf(c623,plain,in_lopen(v400,v0,v400),inference(resolution,[status(thm)],[c603, c26])).
% 0.19/0.48 cnf(c672,plain,~less(v200,v400),inference(resolution,[status(thm)],[c623, c15])).
% 0.19/0.48 cnf(c675,plain,$false,inference(resolution,[status(thm)],[c672, c24])).
% 0.19/0.48 % SZS output end CNFRefutation
% 0.19/0.48
% 0.19/0.48 % Initial clauses : 79
% 0.19/0.48 % Processed clauses : 146
% 0.19/0.48 % Factors computed : 11
% 0.19/0.48 % Resolvents computed: 514
% 0.19/0.48 % Tautologies deleted: 9
% 0.19/0.48 % Forward subsumed : 57
% 0.19/0.48 % Backward subsumed : 0
% 0.19/0.48 % -------- CPU Time ---------
% 0.19/0.48 % User time : 0.169 s
% 0.19/0.48 % System time : 0.014 s
% 0.19/0.48 % Total time : 0.183 s
%------------------------------------------------------------------------------