%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL682+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:59:03 PM UTC 2026
% Result : Theorem 0.32s 0.63s
% Output : CNFRefutation 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL682+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.02/0.36 % Computer : n016.cluster.edu
% 0.02/0.36 % Model : x86_64 x86_64
% 0.02/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.36 % Memory : 8046.5625MB
% 0.02/0.36 % OS : Linux 6.8.0-71-generic
% 0.02/0.36 % CPULimit : 300
% 0.02/0.36 % WCLimit : 300
% 0.02/0.36 % DateTime : Fri Sep 4 16:10:58 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.02/0.42 (re.compile("\."), Token.FullStop),
% 0.02/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.02/0.42 (re.compile("\("), Token.OpenPar),
% 0.02/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.02/0.42 (re.compile("\)"), Token.ClosePar),
% 0.02/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.02/0.42 (re.compile("\["), Token.OpenSquare),
% 0.02/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.02/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.02/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.02/0.42 (re.compile("~\|"), Token.Nor),
% 0.02/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.02/0.42 (re.compile("\|"), Token.Or),
% 0.02/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.02/0.42 (re.compile("\?"), Token.Existential),
% 0.02/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.02/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.02/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.02/0.42 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.49 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.49 """
% 0.23/0.50 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.50 """
% 0.32/0.59 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.59 """
% 0.32/0.63 % Version: 1.5
% 0.32/0.63 % SZS status Theorem
% 0.32/0.63 % SZS output start CNFRefutation
% 0.32/0.63 fof(main,conjecture,(~(?[X]:(~(((((~(![Y]:((~r1(X,Y))|(~((((~(![X]:((~r1(Y,X))|p16(X))))|(~(![X]:((~r1(Y,X))|p12(X)))))|(~(![X]:((~r1(Y,X))|p14(X)))))|(~(![X]:((~r1(Y,X))|p12(X)))))))))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p15(X))))))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p13(X))))))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p12(X))))))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p11(X))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 0.32/0.63 fof(c0,negated_conjecture,(~(~(?[X]:(~(((((~(![Y]:((~r1(X,Y))|(~((((~(![X]:((~r1(Y,X))|p16(X))))|(~(![X]:((~r1(Y,X))|p12(X)))))|(~(![X]:((~r1(Y,X))|p14(X)))))|(~(![X]:((~r1(Y,X))|p12(X)))))))))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p15(X))))))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p13(X))))))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p12(X))))))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|p11(X)))))))))),inference(assume_negation,[status(cth)],[main])).
% 0.32/0.63 fof(c1,negated_conjecture,(~(~(?[X]:(~(((((~(![Y]:(~r1(X,Y)|(~((((~(![X]:(~r1(Y,X)|p16(X))))|(~(![X]:(~r1(Y,X)|p12(X)))))|(~(![X]:(~r1(Y,X)|p14(X)))))|(~(![X]:(~r1(Y,X)|p12(X)))))))))|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p15(X))))))|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p13(X))))))|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p12(X))))))|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|p11(X)))))))))),inference(fof_simplification,[status(thm)],[c0])).
% 0.32/0.63 fof(c2,negated_conjecture,(?[X]:(((((![Y]:(~r1(X,Y)|((((![X]:(~r1(Y,X)|p16(X)))&(![X]:(~r1(Y,X)|p12(X))))&(![X]:(~r1(Y,X)|p14(X))))&(![X]:(~r1(Y,X)|p12(X))))))&(?[Y]:(r1(X,Y)&(?[X]:(r1(Y,X)&~p15(X))))))&(?[Y]:(r1(X,Y)&(?[X]:(r1(Y,X)&~p13(X))))))&(?[Y]:(r1(X,Y)&(?[X]:(r1(Y,X)&~p12(X))))))&(?[Y]:(r1(X,Y)&(?[X]:(r1(Y,X)&~p11(X))))))),inference(fof_nnf,[status(thm)],[c1])).
% 0.32/0.63 fof(c3,negated_conjecture,(?[X2]:(((((![X3]:(~r1(X2,X3)|((((![X4]:(~r1(X3,X4)|p16(X4)))&(![X5]:(~r1(X3,X5)|p12(X5))))&(![X6]:(~r1(X3,X6)|p14(X6))))&(![X7]:(~r1(X3,X7)|p12(X7))))))&(?[X8]:(r1(X2,X8)&(?[X9]:(r1(X8,X9)&~p15(X9))))))&(?[X10]:(r1(X2,X10)&(?[X11]:(r1(X10,X11)&~p13(X11))))))&(?[X12]:(r1(X2,X12)&(?[X13]:(r1(X12,X13)&~p12(X13))))))&(?[X14]:(r1(X2,X14)&(?[X15]:(r1(X14,X15)&~p11(X15))))))),inference(variable_rename,[status(thm)],[c2])).
% 0.32/0.63 fof(c5,negated_conjecture,(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(((((~r1(skolem0001,X3)|((((~r1(X3,X4)|p16(X4))&(~r1(X3,X5)|p12(X5)))&(~r1(X3,X6)|p14(X6)))&(~r1(X3,X7)|p12(X7))))&(r1(skolem0001,skolem0002)&(r1(skolem0002,skolem0003)&~p15(skolem0003))))&(r1(skolem0001,skolem0004)&(r1(skolem0004,skolem0005)&~p13(skolem0005))))&(r1(skolem0001,skolem0006)&(r1(skolem0006,skolem0007)&~p12(skolem0007))))&(r1(skolem0001,skolem0008)&(r1(skolem0008,skolem0009)&~p11(skolem0009))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,(((((![X3]:(~r1(skolem0001,X3)|((((![X4]:(~r1(X3,X4)|p16(X4)))&(![X5]:(~r1(X3,X5)|p12(X5))))&(![X6]:(~r1(X3,X6)|p14(X6))))&(![X7]:(~r1(X3,X7)|p12(X7))))))&(r1(skolem0001,skolem0002)&(r1(skolem0002,skolem0003)&~p15(skolem0003))))&(r1(skolem0001,skolem0004)&(r1(skolem0004,skolem0005)&~p13(skolem0005))))&(r1(skolem0001,skolem0006)&(r1(skolem0006,skolem0007)&~p12(skolem0007))))&(r1(skolem0001,skolem0008)&(r1(skolem0008,skolem0009)&~p11(skolem0009)))),inference(skolemize,[status(esa)],[c3])).])).
% 0.32/0.63 fof(c6,negated_conjecture,(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:((((((((~r1(skolem0001,X3)|(~r1(X3,X4)|p16(X4)))&(~r1(skolem0001,X3)|(~r1(X3,X5)|p12(X5))))&(~r1(skolem0001,X3)|(~r1(X3,X6)|p14(X6))))&(~r1(skolem0001,X3)|(~r1(X3,X7)|p12(X7))))&(r1(skolem0001,skolem0002)&(r1(skolem0002,skolem0003)&~p15(skolem0003))))&(r1(skolem0001,skolem0004)&(r1(skolem0004,skolem0005)&~p13(skolem0005))))&(r1(skolem0001,skolem0006)&(r1(skolem0006,skolem0007)&~p12(skolem0007))))&(r1(skolem0001,skolem0008)&(r1(skolem0008,skolem0009)&~p11(skolem0009))))))))),inference(distribute,[status(thm)],[c5])).
% 0.32/0.63 cnf(c19,negated_conjecture,~p12(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 0.32/0.63 cnf(c17,negated_conjecture,r1(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 0.32/0.63 cnf(c8,negated_conjecture,~r1(skolem0001,X23)|~r1(X23,X24)|p12(X24),inference(split_conjunct,[status(thm)],[c6])).
% 0.32/0.63 cnf(c18,negated_conjecture,r1(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 0.32/0.63 cnf(c43,plain,~r1(skolem0001,skolem0006)|p12(skolem0007),inference(resolution,[status(thm)],[c18, c8])).
% 0.32/0.63 cnf(c88,plain,p12(skolem0007),inference(resolution,[status(thm)],[c43, c17])).
% 0.32/0.63 cnf(c89,plain,$false,inference(resolution,[status(thm)],[c88, c19])).
% 0.32/0.63 % SZS output end CNFRefutation
% 0.32/0.63
% 0.32/0.63 % Initial clauses : 18
% 0.32/0.63 % Processed clauses : 47
% 0.32/0.63 % Factors computed : 4
% 0.32/0.63 % Resolvents computed: 58
% 0.32/0.63 % Tautologies deleted: 2
% 0.32/0.63 % Forward subsumed : 9
% 0.32/0.63 % Backward subsumed : 6
% 0.32/0.63 % -------- CPU Time ---------
% 0.32/0.63 % User time : 0.243 s
% 0.32/0.63 % System time : 0.022 s
% 0.32/0.63 % Total time : 0.265 s
%------------------------------------------------------------------------------