%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL638+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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 : Mon Sep 7 12:58:46 PM UTC 2026
% Result : Theorem 0.39s 0.67s
% Output : CNFRefutation 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL638+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.36 % Computer : n004.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 4 19:37:44 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.10/0.43 (re.compile("\."), Token.FullStop),
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.10/0.43 (re.compile("\("), Token.OpenPar),
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.10/0.43 (re.compile("\)"), Token.ClosePar),
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.10/0.43 (re.compile("\["), Token.OpenSquare),
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.10/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.10/0.43 (re.compile("~\|"), Token.Nor),
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.10/0.43 (re.compile("\|"), Token.Or),
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.10/0.43 (re.compile("\?"), Token.Existential),
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.10/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.10/0.43 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.10/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.50 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.50 """
% 0.23/0.50 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.50 """
% 0.33/0.59 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.59 """
% 0.39/0.67 % Version: 1.5
% 0.39/0.67 % SZS status Theorem
% 0.39/0.67 % SZS output start CNFRefutation
% 0.39/0.67 fof(main,conjecture,(~(?[X]:(~((((((~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(~(![Y]:((~r1(X,Y))|p1(Y)))))))&(~p1(Y)))))))|(~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(~(![Y]:((~r1(X,Y))|(~p1(Y))))))))&p1(Y)))))))|(~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|(~p1(X))))))))))&(![X]:((~r1(Y,X))|(~(![Y]:((~r1(X,Y))|(~p1(Y)))))))))))))|(~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))))&(![X]:((~r1(Y,X))|p1(X)))))))))|(~(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|$false)))))))|(![Y]:(((~r1(X,Y))|p1(Y))|(~(![X]:((~r1(Y,X))|p1(X)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 0.39/0.67 fof(c0,negated_conjecture,(~(~(?[X]:(~((((((~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(~(![Y]:((~r1(X,Y))|p1(Y)))))))&(~p1(Y)))))))|(~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(~(![Y]:((~r1(X,Y))|(~p1(Y))))))))&p1(Y)))))))|(~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|(~p1(X))))))))))&(![X]:((~r1(Y,X))|(~(![Y]:((~r1(X,Y))|(~p1(Y)))))))))))))|(~(![Y]:((~r1(X,Y))|(~((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))))&(![X]:((~r1(Y,X))|p1(X)))))))))|(~(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|$false)))))))|(![Y]:(((~r1(X,Y))|p1(Y))|(~(![X]:((~r1(Y,X))|p1(X))))))))))),inference(assume_negation,[status(cth)],[main])).
% 0.39/0.67 fof(c1,negated_conjecture,(~(~(?[X]:(~((((((~(![Y]:(~r1(X,Y)|(~((~(![X]:(~r1(Y,X)|(~(![Y]:(~r1(X,Y)|p1(Y)))))))&~p1(Y))))))|(~(![Y]:(~r1(X,Y)|(~((~(![X]:(~r1(Y,X)|(~(![Y]:(~r1(X,Y)|~p1(Y)))))))&p1(Y)))))))|(~(![Y]:(~r1(X,Y)|(~((~(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(~(![X]:(~r1(Y,X)|~p1(X)))))))))&(![X]:(~r1(Y,X)|(~(![Y]:(~r1(X,Y)|~p1(Y))))))))))))|(~(![Y]:(~r1(X,Y)|(~((~(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|p1(Y))))))&(![X]:(~r1(Y,X)|p1(X)))))))))|(~(![Y]:(~r1(X,Y)|(~(![X]:~r1(Y,X)))))))|(![Y]:((~r1(X,Y)|p1(Y))|(~(![X]:(~r1(Y,X)|p1(X))))))))))),inference(fof_simplification,[status(thm)],[c0])).
% 0.39/0.67 fof(c2,negated_conjecture,(?[X]:((((((![Y]:(~r1(X,Y)|((![X]:(~r1(Y,X)|(?[Y]:(r1(X,Y)&~p1(Y)))))|p1(Y))))&(![Y]:(~r1(X,Y)|((![X]:(~r1(Y,X)|(?[Y]:(r1(X,Y)&p1(Y)))))|~p1(Y)))))&(![Y]:(~r1(X,Y)|((![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(?[X]:(r1(Y,X)&p1(X)))))))|(?[X]:(r1(Y,X)&(![Y]:(~r1(X,Y)|~p1(Y)))))))))&(![Y]:(~r1(X,Y)|((![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|p1(Y)))))|(?[X]:(r1(Y,X)&~p1(X)))))))&(![Y]:(~r1(X,Y)|(?[X]:r1(Y,X)))))&(?[Y]:((r1(X,Y)&~p1(Y))&(![X]:(~r1(Y,X)|p1(X))))))),inference(fof_nnf,[status(thm)],[c1])).
% 0.39/0.67 fof(c3,negated_conjecture,(?[X2]:((((((![X3]:(~r1(X2,X3)|((![X4]:(~r1(X3,X4)|(?[X5]:(r1(X4,X5)&~p1(X5)))))|p1(X3))))&(![X6]:(~r1(X2,X6)|((![X7]:(~r1(X6,X7)|(?[X8]:(r1(X7,X8)&p1(X8)))))|~p1(X6)))))&(![X9]:(~r1(X2,X9)|((![X10]:(~r1(X9,X10)|(![X11]:(~r1(X10,X11)|(?[X12]:(r1(X11,X12)&p1(X12)))))))|(?[X13]:(r1(X9,X13)&(![X14]:(~r1(X13,X14)|~p1(X14)))))))))&(![X15]:(~r1(X2,X15)|((![X16]:(~r1(X15,X16)|(![X17]:(~r1(X16,X17)|p1(X17)))))|(?[X18]:(r1(X15,X18)&~p1(X18)))))))&(![X19]:(~r1(X2,X19)|(?[X20]:r1(X19,X20)))))&(?[X21]:((r1(X2,X21)&~p1(X21))&(![X22]:(~r1(X21,X22)|p1(X22))))))),inference(variable_rename,[status(thm)],[c2])).
% 0.39/0.67 fof(c5,negated_conjecture,(![X3]:(![X4]:(![X6]:(![X7]:(![X9]:(![X10]:(![X11]:(![X14]:(![X15]:(![X16]:(![X17]:(![X19]:(![X22]:((((((~r1(skolem0001,X3)|((~r1(X3,X4)|(r1(X4,skolem0002(X3,X4))&~p1(skolem0002(X3,X4))))|p1(X3)))&(~r1(skolem0001,X6)|((~r1(X6,X7)|(r1(X7,skolem0003(X6,X7))&p1(skolem0003(X6,X7))))|~p1(X6))))&(~r1(skolem0001,X9)|((~r1(X9,X10)|(~r1(X10,X11)|(r1(X11,skolem0004(X9,X10,X11))&p1(skolem0004(X9,X10,X11)))))|(r1(X9,skolem0005(X9))&(~r1(skolem0005(X9),X14)|~p1(X14))))))&(~r1(skolem0001,X15)|((~r1(X15,X16)|(~r1(X16,X17)|p1(X17)))|(r1(X15,skolem0006(X15))&~p1(skolem0006(X15))))))&(~r1(skolem0001,X19)|r1(X19,skolem0007(X19))))&((r1(skolem0001,skolem0008)&~p1(skolem0008))&(~r1(skolem0008,X22)|p1(X22))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((((((![X3]:(~r1(skolem0001,X3)|((![X4]:(~r1(X3,X4)|(r1(X4,skolem0002(X3,X4))&~p1(skolem0002(X3,X4)))))|p1(X3))))&(![X6]:(~r1(skolem0001,X6)|((![X7]:(~r1(X6,X7)|(r1(X7,skolem0003(X6,X7))&p1(skolem0003(X6,X7)))))|~p1(X6)))))&(![X9]:(~r1(skolem0001,X9)|((![X10]:(~r1(X9,X10)|(![X11]:(~r1(X10,X11)|(r1(X11,skolem0004(X9,X10,X11))&p1(skolem0004(X9,X10,X11)))))))|(r1(X9,skolem0005(X9))&(![X14]:(~r1(skolem0005(X9),X14)|~p1(X14))))))))&(![X15]:(~r1(skolem0001,X15)|((![X16]:(~r1(X15,X16)|(![X17]:(~r1(X16,X17)|p1(X17)))))|(r1(X15,skolem0006(X15))&~p1(skolem0006(X15)))))))&(![X19]:(~r1(skolem0001,X19)|r1(X19,skolem0007(X19)))))&((r1(skolem0001,skolem0008)&~p1(skolem0008))&(![X22]:(~r1(skolem0008,X22)|p1(X22))))),inference(skolemize,[status(esa)],[c3])).])).
% 0.39/0.67 fof(c6,negated_conjecture,(![X3]:(![X4]:(![X6]:(![X7]:(![X9]:(![X10]:(![X11]:(![X14]:(![X15]:(![X16]:(![X17]:(![X19]:(![X22]:(((((((~r1(skolem0001,X3)|((~r1(X3,X4)|r1(X4,skolem0002(X3,X4)))|p1(X3)))&(~r1(skolem0001,X3)|((~r1(X3,X4)|~p1(skolem0002(X3,X4)))|p1(X3))))&((~r1(skolem0001,X6)|((~r1(X6,X7)|r1(X7,skolem0003(X6,X7)))|~p1(X6)))&(~r1(skolem0001,X6)|((~r1(X6,X7)|p1(skolem0003(X6,X7)))|~p1(X6)))))&(((~r1(skolem0001,X9)|((~r1(X9,X10)|(~r1(X10,X11)|r1(X11,skolem0004(X9,X10,X11))))|r1(X9,skolem0005(X9))))&(~r1(skolem0001,X9)|((~r1(X9,X10)|(~r1(X10,X11)|r1(X11,skolem0004(X9,X10,X11))))|(~r1(skolem0005(X9),X14)|~p1(X14)))))&((~r1(skolem0001,X9)|((~r1(X9,X10)|(~r1(X10,X11)|p1(skolem0004(X9,X10,X11))))|r1(X9,skolem0005(X9))))&(~r1(skolem0001,X9)|((~r1(X9,X10)|(~r1(X10,X11)|p1(skolem0004(X9,X10,X11))))|(~r1(skolem0005(X9),X14)|~p1(X14)))))))&((~r1(skolem0001,X15)|((~r1(X15,X16)|(~r1(X16,X17)|p1(X17)))|r1(X15,skolem0006(X15))))&(~r1(skolem0001,X15)|((~r1(X15,X16)|(~r1(X16,X17)|p1(X17)))|~p1(skolem0006(X15))))))&(~r1(skolem0001,X19)|r1(X19,skolem0007(X19))))&((r1(skolem0001,skolem0008)&~p1(skolem0008))&(~r1(skolem0008,X22)|p1(X22))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 0.39/0.67 cnf(c19,negated_conjecture,~p1(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.67 cnf(c18,negated_conjecture,r1(skolem0001,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.67 cnf(c17,negated_conjecture,~r1(skolem0001,X24)|r1(X24,skolem0007(X24)),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.67 cnf(c21,plain,r1(skolem0008,skolem0007(skolem0008)),inference(resolution,[status(thm)],[c17, c18])).
% 0.39/0.67 cnf(c8,negated_conjecture,~r1(skolem0001,X28)|~r1(X28,X27)|~p1(skolem0002(X28,X27))|p1(X28),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.67 cnf(c7,negated_conjecture,~r1(skolem0001,X26)|~r1(X26,X25)|r1(X25,skolem0002(X26,X25))|p1(X26),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.67 cnf(c24,plain,~r1(skolem0001,skolem0008)|r1(skolem0007(skolem0008),skolem0002(skolem0008,skolem0007(skolem0008)))|p1(skolem0008),inference(resolution,[status(thm)],[c7, c21])).
% 0.39/0.67 cnf(c50,plain,r1(skolem0007(skolem0008),skolem0002(skolem0008,skolem0007(skolem0008)))|p1(skolem0008),inference(resolution,[status(thm)],[c24, c18])).
% 0.39/0.67 cnf(c57,plain,r1(skolem0007(skolem0008),skolem0002(skolem0008,skolem0007(skolem0008))),inference(resolution,[status(thm)],[c50, c19])).
% 0.39/0.67 cnf(c16,negated_conjecture,~r1(skolem0001,X36)|~r1(X36,X37)|~r1(X37,X38)|p1(X38)|~p1(skolem0006(X36)),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.67 cnf(c20,negated_conjecture,~r1(skolem0008,X23)|p1(X23),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.67 cnf(c15,negated_conjecture,~r1(skolem0001,X39)|~r1(X39,X40)|~r1(X40,X41)|p1(X41)|r1(X39,skolem0006(X39)),inference(split_conjunct,[status(thm)],[c6])).
% 0.39/0.67 cnf(c58,plain,~r1(skolem0001,X67)|~r1(X67,skolem0007(skolem0008))|p1(skolem0002(skolem0008,skolem0007(skolem0008)))|r1(X67,skolem0006(X67)),inference(resolution,[status(thm)],[c57, c15])).
% 0.39/0.67 cnf(c71,plain,~r1(skolem0001,skolem0008)|p1(skolem0002(skolem0008,skolem0007(skolem0008)))|r1(skolem0008,skolem0006(skolem0008)),inference(resolution,[status(thm)],[c58, c21])).
% 0.39/0.67 cnf(c72,plain,p1(skolem0002(skolem0008,skolem0007(skolem0008)))|r1(skolem0008,skolem0006(skolem0008)),inference(resolution,[status(thm)],[c71, c18])).
% 0.39/0.67 cnf(c74,plain,p1(skolem0002(skolem0008,skolem0007(skolem0008)))|p1(skolem0006(skolem0008)),inference(resolution,[status(thm)],[c72, c20])).
% 0.39/0.67 cnf(c81,plain,p1(skolem0006(skolem0008))|~r1(skolem0001,skolem0008)|~r1(skolem0008,skolem0007(skolem0008))|p1(skolem0008),inference(resolution,[status(thm)],[c74, c8])).
% 0.39/0.67 cnf(c83,plain,p1(skolem0006(skolem0008))|~r1(skolem0001,skolem0008)|p1(skolem0008),inference(resolution,[status(thm)],[c81, c21])).
% 0.39/0.67 cnf(c84,plain,p1(skolem0006(skolem0008))|p1(skolem0008),inference(resolution,[status(thm)],[c83, c18])).
% 0.39/0.67 cnf(c86,plain,p1(skolem0006(skolem0008)),inference(resolution,[status(thm)],[c84, c19])).
% 0.39/0.67 cnf(c87,plain,~r1(skolem0001,skolem0008)|~r1(skolem0008,X70)|~r1(X70,X71)|p1(X71),inference(resolution,[status(thm)],[c86, c16])).
% 0.39/0.67 cnf(c94,plain,~r1(skolem0001,skolem0008)|~r1(skolem0008,skolem0007(skolem0008))|p1(skolem0002(skolem0008,skolem0007(skolem0008))),inference(resolution,[status(thm)],[c87, c57])).
% 0.39/0.67 cnf(c95,plain,~r1(skolem0001,skolem0008)|p1(skolem0002(skolem0008,skolem0007(skolem0008))),inference(resolution,[status(thm)],[c94, c21])).
% 0.39/0.67 cnf(c96,plain,p1(skolem0002(skolem0008,skolem0007(skolem0008))),inference(resolution,[status(thm)],[c95, c18])).
% 0.39/0.67 cnf(c97,plain,~r1(skolem0001,skolem0008)|~r1(skolem0008,skolem0007(skolem0008))|p1(skolem0008),inference(resolution,[status(thm)],[c96, c8])).
% 0.39/0.67 cnf(c98,plain,~r1(skolem0001,skolem0008)|p1(skolem0008),inference(resolution,[status(thm)],[c97, c21])).
% 0.39/0.67 cnf(c99,plain,p1(skolem0008),inference(resolution,[status(thm)],[c98, c18])).
% 0.39/0.67 cnf(c100,plain,$false,inference(resolution,[status(thm)],[c99, c19])).
% 0.39/0.67 % SZS output end CNFRefutation
% 0.39/0.67
% 0.39/0.67 % Initial clauses : 14
% 0.39/0.67 % Processed clauses : 62
% 0.39/0.67 % Factors computed : 22
% 0.39/0.67 % Resolvents computed: 58
% 0.39/0.67 % Tautologies deleted: 0
% 0.39/0.67 % Forward subsumed : 12
% 0.39/0.67 % Backward subsumed : 18
% 0.39/0.67 % -------- CPU Time ---------
% 0.39/0.67 % User time : 0.277 s
% 0.39/0.67 % System time : 0.029 s
% 0.39/0.67 % Total time : 0.306 s
%------------------------------------------------------------------------------