%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT077+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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:50 AM UTC 2026
% Result : Theorem 60.96s 61.22s
% Output : CNFRefutation 60.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT077+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 : n009.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.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 7 14:13:09 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.42 (re.compile("\."), Token.FullStop),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.42 (re.compile("\("), Token.OpenPar),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.42 (re.compile("\)"), Token.ClosePar),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.42 (re.compile("\["), Token.OpenSquare),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.42 (re.compile("~\|"), Token.Nor),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.42 (re.compile("\|"), Token.Or),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.42 (re.compile("\?"), Token.Existential),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.49 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.22/0.49 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.32/0.58 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.58 """
% 60.96/61.22 % Version: 1.5
% 60.96/61.22 % SZS status Theorem
% 60.96/61.22 % SZS output start CNFRefutation
% 60.96/61.22 fof(ord_v200_v500,axiom,less(v200,v500),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ord_v200_v500)).
% 60.96/61.22 cnf(c28,plain,less(v200,v500),inference(split_conjunct,[status(thm)],[ord_v200_v500])).
% 60.96/61.22 fof(ord_v100_v200,axiom,less(v100,v200),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ord_v100_v200)).
% 60.96/61.22 cnf(c31,plain,less(v100,v200),inference(split_conjunct,[status(thm)],[ord_v100_v200])).
% 60.96/61.22 fof(ord_v0_v500,axiom,less(v0,v500),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ord_v0_v500)).
% 60.96/61.22 cnf(c33,plain,less(v0,v500),inference(split_conjunct,[status(thm)],[ord_v0_v500])).
% 60.96/61.22 fof(ord_v500_v800,axiom,less(v500,v800),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ord_v500_v800)).
% 60.96/61.22 cnf(c26,plain,less(v500,v800),inference(split_conjunct,[status(thm)],[ord_v500_v800])).
% 60.96/61.22 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)).
% 60.96/61.22 fof(c93,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])).
% 60.96/61.22 fof(c94,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)],[c93])).
% 60.96/61.22 fof(c96,plain,(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(![X48]:((~in_open(X43,X44,X45)|(less(X44,X43)&less(X43,X45)))&((~less(X47,X46)|~less(X46,X48))|in_open(X46,X47,X48))))))))),inference(shift_quantors,[status(thm)],[fof(c95,plain,((![X43]:(![X44]:(![X45]:(~in_open(X43,X44,X45)|(less(X44,X43)&less(X43,X45))))))&(![X46]:(![X47]:(![X48]:((~less(X47,X46)|~less(X46,X48))|in_open(X46,X47,X48)))))),inference(variable_rename,[status(thm)],[c94])).])).
% 60.96/61.22 fof(c97,plain,(![X43]:(![X44]:(![X45]:(![X46]:(![X47]:(![X48]:(((~in_open(X43,X44,X45)|less(X44,X43))&(~in_open(X43,X44,X45)|less(X43,X45)))&((~less(X47,X46)|~less(X46,X48))|in_open(X46,X47,X48))))))))),inference(distribute,[status(thm)],[c96])).
% 60.96/61.22 cnf(c100,plain,~less(X281,X280)|~less(X280,X282)|in_open(X280,X281,X282),inference(split_conjunct,[status(thm)],[c97])).
% 60.96/61.22 cnf(c467,plain,~less(X482,v500)|in_open(v500,X482,v800),inference(resolution,[status(thm)],[c100, c26])).
% 60.96/61.22 cnf(c1539,plain,in_open(v500,v0,v800),inference(resolution,[status(thm)],[c467, c33])).
% 60.96/61.22 fof(odrl327,conjecture,(?[X]:(?[Y]:(((less(v200,X)&in_open(X,v0,v800))&less(v100,Y))&in_open(Y,v0,v500)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', odrl327)).
% 60.96/61.22 fof(c12,negated_conjecture,(~(?[X]:(?[Y]:(((less(v200,X)&in_open(X,v0,v800))&less(v100,Y))&in_open(Y,v0,v500))))),inference(assume_negation,[status(cth)],[odrl327])).
% 60.96/61.22 fof(c13,negated_conjecture,(![X]:(![Y]:(((~less(v200,X)|~in_open(X,v0,v800))|~less(v100,Y))|~in_open(Y,v0,v500)))),inference(fof_nnf,[status(thm)],[c12])).
% 60.96/61.22 fof(c14,negated_conjecture,(![X2]:(![X3]:(((~less(v200,X2)|~in_open(X2,v0,v800))|~less(v100,X3))|~in_open(X3,v0,v500)))),inference(variable_rename,[status(thm)],[c13])).
% 60.96/61.22 cnf(c15,negated_conjecture,~less(v200,X204)|~in_open(X204,v0,v800)|~less(v100,X203)|~in_open(X203,v0,v500),inference(split_conjunct,[status(thm)],[c14])).
% 60.96/61.22 fof(ord_v0_v200,axiom,less(v0,v200),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ord_v0_v200)).
% 60.96/61.22 cnf(c34,plain,less(v0,v200),inference(split_conjunct,[status(thm)],[ord_v0_v200])).
% 60.96/61.22 cnf(c461,plain,~less(X476,v200)|in_open(v200,X476,v500),inference(resolution,[status(thm)],[c100, c28])).
% 60.96/61.22 cnf(c1513,plain,in_open(v200,v0,v500),inference(resolution,[status(thm)],[c461, c34])).
% 60.96/61.22 cnf(c1521,plain,~less(v200,X3179)|~in_open(X3179,v0,v800)|~less(v100,v200),inference(resolution,[status(thm)],[c1513, c15])).
% 60.96/61.22 cnf(c71400,plain,~less(v200,v500)|~less(v100,v200),inference(resolution,[status(thm)],[c1521, c1539])).
% 60.96/61.22 cnf(c75340,plain,~less(v200,v500),inference(resolution,[status(thm)],[c71400, c31])).
% 60.96/61.22 cnf(c75438,plain,$false,inference(resolution,[status(thm)],[c75340, c28])).
% 60.96/61.22 % SZS output end CNFRefutation
% 60.96/61.22
% 60.96/61.22 % Initial clauses : 88
% 60.96/61.22 % Processed clauses : 1979
% 60.96/61.22 % Factors computed : 103
% 60.96/61.22 % Resolvents computed: 75181
% 60.96/61.22 % Tautologies deleted: 11
% 60.96/61.22 % Forward subsumed : 3580
% 60.96/61.22 % Backward subsumed : 10
% 60.96/61.22 % -------- CPU Time ---------
% 60.96/61.22 % User time : 60.642 s
% 60.96/61.22 % System time : 0.215 s
% 60.96/61.22 % Total time : 60.857 s
%------------------------------------------------------------------------------