%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL686+1.001 : TPTP v9.3.1. Released v4.0.0.
% 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 : Mon Sep 7 12:59:04 PM UTC 2026
% Result : Theorem 0.33s 0.63s
% Output : CNFRefutation 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL686+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 09:50:36 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.12/0.41 (re.compile("\."), Token.FullStop),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.12/0.41 (re.compile("\("), Token.OpenPar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.12/0.41 (re.compile("\)"), Token.ClosePar),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.12/0.41 (re.compile("\["), Token.OpenSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.12/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("~\|"), Token.Nor),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.12/0.41 (re.compile("\|"), Token.Or),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.12/0.41 (re.compile("\?"), Token.Existential),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.12/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.12/0.41 /export/starexec/sandbox2/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.12/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.21/0.48 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.21/0.48 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.48 """
% 0.21/0.57 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.21/0.57 """
% 0.33/0.63 % Version: 1.5
% 0.33/0.63 % SZS status Theorem
% 0.33/0.63 % SZS output start CNFRefutation
% 0.33/0.63 fof(reflexivity,axiom,(![X]:r1(X,X)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity)).
% 0.33/0.63 fof(c23,plain,(![X14]:r1(X14,X14)),inference(variable_rename,[status(thm)],[reflexivity])).
% 0.33/0.63 cnf(c24,plain,r1(X15,X15),inference(split_conjunct,[status(thm)],[c23])).
% 0.33/0.63 fof(main,conjecture,(~(?[X]:(~((![Y]:(((~r1(X,Y))|(~p3(Y)))|(![X]:((~r1(Y,X))|(~p1(X))))))|(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|(~((((![Y]:((~r1(X,Y))|$false))|(~(![Y]:((~r1(X,Y))|(~((p2(Y)&(~p1(Y)))|((~p2(Y))&p1(Y))))))))|(![Y]:((~r1(X,Y))|p3(Y))))|(![Y]:(((~r1(X,Y))|((~p1(Y))&(~p2(Y))))|(p2(Y)&p1(Y))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 0.33/0.63 fof(c0,negated_conjecture,(~(~(?[X]:(~((![Y]:(((~r1(X,Y))|(~p3(Y)))|(![X]:((~r1(Y,X))|(~p1(X))))))|(![Y]:((~r1(X,Y))|(~(![X]:((~r1(Y,X))|(~((((![Y]:((~r1(X,Y))|$false))|(~(![Y]:((~r1(X,Y))|(~((p2(Y)&(~p1(Y)))|((~p2(Y))&p1(Y))))))))|(![Y]:((~r1(X,Y))|p3(Y))))|(![Y]:(((~r1(X,Y))|((~p1(Y))&(~p2(Y))))|(p2(Y)&p1(Y)))))))))))))))),inference(assume_negation,[status(cth)],[main])).
% 0.33/0.63 fof(c1,negated_conjecture,(~(~(?[X]:(~((![Y]:((~r1(X,Y)|~p3(Y))|(![X]:(~r1(Y,X)|~p1(X)))))|(![Y]:(~r1(X,Y)|(~(![X]:(~r1(Y,X)|(~((((![Y]:~r1(X,Y))|(~(![Y]:(~r1(X,Y)|(~((p2(Y)&~p1(Y))|(~p2(Y)&p1(Y))))))))|(![Y]:(~r1(X,Y)|p3(Y))))|(![Y]:((~r1(X,Y)|(~p1(Y)&~p2(Y)))|(p2(Y)&p1(Y)))))))))))))))),inference(fof_simplification,[status(thm)],[c0])).
% 0.33/0.63 fof(c2,negated_conjecture,(?[X]:((?[Y]:((r1(X,Y)&p3(Y))&(?[X]:(r1(Y,X)&p1(X)))))&(?[Y]:(r1(X,Y)&(![X]:(~r1(Y,X)|((((?[Y]:r1(X,Y))&(![Y]:(~r1(X,Y)|((~p2(Y)|p1(Y))&(p2(Y)|~p1(Y))))))&(?[Y]:(r1(X,Y)&~p3(Y))))&(?[Y]:((r1(X,Y)&(p1(Y)|p2(Y)))&(~p2(Y)|~p1(Y))))))))))),inference(fof_nnf,[status(thm)],[c1])).
% 0.33/0.63 fof(c3,negated_conjecture,(?[X2]:((?[X3]:((r1(X2,X3)&p3(X3))&(?[X4]:(r1(X3,X4)&p1(X4)))))&(?[X5]:(r1(X2,X5)&(![X6]:(~r1(X5,X6)|((((?[X7]:r1(X6,X7))&(![X8]:(~r1(X6,X8)|((~p2(X8)|p1(X8))&(p2(X8)|~p1(X8))))))&(?[X9]:(r1(X6,X9)&~p3(X9))))&(?[X10]:((r1(X6,X10)&(p1(X10)|p2(X10)))&(~p2(X10)|~p1(X10))))))))))),inference(variable_rename,[status(thm)],[c2])).
% 0.33/0.63 fof(c5,negated_conjecture,(![X6]:(![X8]:(((r1(skolem0001,skolem0002)&p3(skolem0002))&(r1(skolem0002,skolem0003)&p1(skolem0003)))&(r1(skolem0001,skolem0004)&(~r1(skolem0004,X6)|(((r1(X6,skolem0005(X6))&(~r1(X6,X8)|((~p2(X8)|p1(X8))&(p2(X8)|~p1(X8)))))&(r1(X6,skolem0006(X6))&~p3(skolem0006(X6))))&((r1(X6,skolem0007(X6))&(p1(skolem0007(X6))|p2(skolem0007(X6))))&(~p2(skolem0007(X6))|~p1(skolem0007(X6)))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,(((r1(skolem0001,skolem0002)&p3(skolem0002))&(r1(skolem0002,skolem0003)&p1(skolem0003)))&(r1(skolem0001,skolem0004)&(![X6]:(~r1(skolem0004,X6)|(((r1(X6,skolem0005(X6))&(![X8]:(~r1(X6,X8)|((~p2(X8)|p1(X8))&(p2(X8)|~p1(X8))))))&(r1(X6,skolem0006(X6))&~p3(skolem0006(X6))))&((r1(X6,skolem0007(X6))&(p1(skolem0007(X6))|p2(skolem0007(X6))))&(~p2(skolem0007(X6))|~p1(skolem0007(X6))))))))),inference(skolemize,[status(esa)],[c3])).])).
% 0.33/0.63 fof(c6,negated_conjecture,(![X6]:(![X8]:(((r1(skolem0001,skolem0002)&p3(skolem0002))&(r1(skolem0002,skolem0003)&p1(skolem0003)))&(r1(skolem0001,skolem0004)&((((~r1(skolem0004,X6)|r1(X6,skolem0005(X6)))&((~r1(skolem0004,X6)|(~r1(X6,X8)|(~p2(X8)|p1(X8))))&(~r1(skolem0004,X6)|(~r1(X6,X8)|(p2(X8)|~p1(X8))))))&((~r1(skolem0004,X6)|r1(X6,skolem0006(X6)))&(~r1(skolem0004,X6)|~p3(skolem0006(X6)))))&(((~r1(skolem0004,X6)|r1(X6,skolem0007(X6)))&(~r1(skolem0004,X6)|(p1(skolem0007(X6))|p2(skolem0007(X6)))))&(~r1(skolem0004,X6)|(~p2(skolem0007(X6))|~p1(skolem0007(X6)))))))))),inference(distribute,[status(thm)],[c5])).
% 0.33/0.63 cnf(c17,negated_conjecture,~r1(skolem0004,X21)|r1(X21,skolem0007(X21)),inference(split_conjunct,[status(thm)],[c6])).
% 0.33/0.63 cnf(c39,plain,r1(skolem0004,skolem0007(skolem0004)),inference(resolution,[status(thm)],[c17, c24])).
% 0.33/0.63 cnf(c13,negated_conjecture,~r1(skolem0004,X20)|~r1(X20,X19)|~p2(X19)|p1(X19),inference(split_conjunct,[status(thm)],[c6])).
% 0.33/0.63 cnf(c36,plain,~r1(skolem0004,X22)|~p2(X22)|p1(X22),inference(resolution,[status(thm)],[c13, c24])).
% 0.33/0.63 cnf(c48,plain,~p2(skolem0007(skolem0004))|p1(skolem0007(skolem0004)),inference(resolution,[status(thm)],[c36, c39])).
% 0.33/0.63 cnf(c18,negated_conjecture,~r1(skolem0004,X33)|p1(skolem0007(X33))|p2(skolem0007(X33)),inference(split_conjunct,[status(thm)],[c6])).
% 0.33/0.63 cnf(c69,plain,p1(skolem0007(skolem0004))|p2(skolem0007(skolem0004)),inference(resolution,[status(thm)],[c18, c24])).
% 0.33/0.63 cnf(c124,plain,p1(skolem0007(skolem0004)),inference(resolution,[status(thm)],[c69, c48])).
% 0.33/0.63 cnf(c14,negated_conjecture,~r1(skolem0004,X27)|~r1(X27,X26)|p2(X26)|~p1(X26),inference(split_conjunct,[status(thm)],[c6])).
% 0.33/0.63 cnf(c62,plain,~r1(skolem0004,X37)|p2(X37)|~p1(X37),inference(resolution,[status(thm)],[c14, c24])).
% 0.33/0.63 cnf(c80,plain,p2(skolem0007(skolem0004))|~p1(skolem0007(skolem0004)),inference(resolution,[status(thm)],[c62, c39])).
% 0.33/0.63 cnf(c126,plain,p2(skolem0007(skolem0004)),inference(resolution,[status(thm)],[c80, c124])).
% 0.33/0.63 cnf(c19,negated_conjecture,~r1(skolem0004,X36)|~p2(skolem0007(X36))|~p1(skolem0007(X36)),inference(split_conjunct,[status(thm)],[c6])).
% 0.33/0.63 cnf(c125,plain,~r1(skolem0004,skolem0004)|~p2(skolem0007(skolem0004)),inference(resolution,[status(thm)],[c124, c19])).
% 0.33/0.63 cnf(c130,plain,~r1(skolem0004,skolem0004),inference(resolution,[status(thm)],[c125, c126])).
% 0.33/0.63 cnf(c131,plain,$false,inference(resolution,[status(thm)],[c130, c24])).
% 0.33/0.63 % SZS output end CNFRefutation
% 0.33/0.63
% 0.33/0.63 % Initial clauses : 15
% 0.33/0.63 % Processed clauses : 57
% 0.33/0.63 % Factors computed : 3
% 0.33/0.63 % Resolvents computed: 104
% 0.33/0.63 % Tautologies deleted: 2
% 0.33/0.63 % Forward subsumed : 15
% 0.33/0.63 % Backward subsumed : 4
% 0.33/0.63 % -------- CPU Time ---------
% 0.33/0.63 % User time : 0.257 s
% 0.33/0.63 % System time : 0.023 s
% 0.33/0.63 % Total time : 0.280 s
%------------------------------------------------------------------------------