%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL654+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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:53 PM UTC 2026
% Result : Theorem 6.17s 6.49s
% Output : CNFRefutation 6.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL654+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.34 % Computer : n010.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sat Sep 5 00:38:08 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.13/0.40 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.41 (re.compile("\."), Token.FullStop),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.41 (re.compile("\("), Token.OpenPar),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.41 (re.compile("\)"), Token.ClosePar),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.41 (re.compile("\["), Token.OpenSquare),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("~\|"), Token.Nor),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("\|"), Token.Or),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.41 (re.compile("\?"), Token.Existential),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.48 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.48 """
% 0.23/0.48 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.48 """
% 0.33/0.57 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.57 """
% 6.17/6.49 % Version: 1.5
% 6.17/6.49 % SZS status Theorem
% 6.17/6.49 % SZS output start CNFRefutation
% 6.17/6.49 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))|(~(![X]:((~r1(Y,X))|p1(X)))))))&(~(![Y]:((~r1(X,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))|$false)))))))|(![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))))|(~(![X]:((~r1(Y,X))|p1(X)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 6.17/6.49 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))|(~(![X]:((~r1(Y,X))|p1(X)))))))&(~(![Y]:((~r1(X,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))|$false)))))))|(![Y]:(((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|p1(Y))))))|(~(![X]:((~r1(Y,X))|p1(X))))))))))),inference(assume_negation,[status(cth)],[main])).
% 6.17/6.49 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)|(~(![X]:(~r1(Y,X)|p1(X)))))))&(~(![Y]:(~r1(X,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)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|p1(Y))))))|(~(![X]:(~r1(Y,X)|p1(X))))))))))),inference(fof_simplification,[status(thm)],[c0])).
% 6.17/6.49 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)|(?[X]:(r1(Y,X)&~p1(X)))))|(![Y]:(~r1(X,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)&(?[X]:(r1(Y,X)&(?[Y]:(r1(X,Y)&~p1(Y))))))&(![X]:(~r1(Y,X)|p1(X))))))),inference(fof_nnf,[status(thm)],[c1])).
% 6.17/6.49 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)|(?[X9]:(r1(X8,X9)&~p1(X9)))))|(![X10]:(~r1(X7,X10)|p1(X10)))))))))&(![X11]:(~r1(X2,X11)|((![X12]:(~r1(X11,X12)|(?[X13]:(r1(X12,X13)&(![X14]:(~r1(X13,X14)|p1(X14)))))))|(![X15]:(~r1(X11,X15)|(?[X16]:(r1(X15,X16)&~p1(X16)))))))))&(![X17]:(~r1(X2,X17)|(?[X18]:r1(X17,X18)))))&(?[X19]:((r1(X2,X19)&(?[X20]:(r1(X19,X20)&(?[X21]:(r1(X20,X21)&~p1(X21))))))&(![X22]:(~r1(X19,X22)|p1(X22))))))),inference(variable_rename,[status(thm)],[c2])).
% 6.17/6.49 fof(c5,negated_conjecture,(![X3]:(![X4]:(![X6]:(![X7]:(![X8]:(![X10]:(![X11]:(![X12]:(![X14]:(![X15]:(![X17]:(![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,X8)|(r1(X8,skolem0003(X6,X7,X8))&~p1(skolem0003(X6,X7,X8))))|(~r1(X7,X10)|p1(X10))))))&(~r1(skolem0001,X11)|((~r1(X11,X12)|(r1(X12,skolem0004(X11,X12))&(~r1(skolem0004(X11,X12),X14)|p1(X14))))|(~r1(X11,X15)|(r1(X15,skolem0005(X11,X15))&~p1(skolem0005(X11,X15)))))))&(~r1(skolem0001,X17)|r1(X17,skolem0006(X17))))&((r1(skolem0001,skolem0007)&(r1(skolem0007,skolem0008)&(r1(skolem0008,skolem0009)&~p1(skolem0009))))&(~r1(skolem0007,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)|((![X8]:(~r1(X7,X8)|(r1(X8,skolem0003(X6,X7,X8))&~p1(skolem0003(X6,X7,X8)))))|(![X10]:(~r1(X7,X10)|p1(X10)))))))))&(![X11]:(~r1(skolem0001,X11)|((![X12]:(~r1(X11,X12)|(r1(X12,skolem0004(X11,X12))&(![X14]:(~r1(skolem0004(X11,X12),X14)|p1(X14))))))|(![X15]:(~r1(X11,X15)|(r1(X15,skolem0005(X11,X15))&~p1(skolem0005(X11,X15)))))))))&(![X17]:(~r1(skolem0001,X17)|r1(X17,skolem0006(X17)))))&((r1(skolem0001,skolem0007)&(r1(skolem0007,skolem0008)&(r1(skolem0008,skolem0009)&~p1(skolem0009))))&(![X22]:(~r1(skolem0007,X22)|p1(X22))))),inference(skolemize,[status(esa)],[c3])).])).
% 6.17/6.49 fof(c6,negated_conjecture,(![X3]:(![X4]:(![X6]:(![X7]:(![X8]:(![X10]:(![X11]:(![X12]:(![X14]:(![X15]:(![X17]:(![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,X8)|r1(X8,skolem0003(X6,X7,X8)))|(~r1(X7,X10)|p1(X10)))))&(~r1(skolem0001,X6)|(~r1(X6,X7)|((~r1(X7,X8)|~p1(skolem0003(X6,X7,X8)))|(~r1(X7,X10)|p1(X10)))))))&(((~r1(skolem0001,X11)|((~r1(X11,X12)|r1(X12,skolem0004(X11,X12)))|(~r1(X11,X15)|r1(X15,skolem0005(X11,X15)))))&(~r1(skolem0001,X11)|((~r1(X11,X12)|r1(X12,skolem0004(X11,X12)))|(~r1(X11,X15)|~p1(skolem0005(X11,X15))))))&((~r1(skolem0001,X11)|((~r1(X11,X12)|(~r1(skolem0004(X11,X12),X14)|p1(X14)))|(~r1(X11,X15)|r1(X15,skolem0005(X11,X15)))))&(~r1(skolem0001,X11)|((~r1(X11,X12)|(~r1(skolem0004(X11,X12),X14)|p1(X14)))|(~r1(X11,X15)|~p1(skolem0005(X11,X15))))))))&(~r1(skolem0001,X17)|r1(X17,skolem0006(X17))))&((r1(skolem0001,skolem0007)&(r1(skolem0007,skolem0008)&(r1(skolem0008,skolem0009)&~p1(skolem0009))))&(~r1(skolem0007,X22)|p1(X22)))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 6.17/6.49 cnf(c19,negated_conjecture,~p1(skolem0009),inference(split_conjunct,[status(thm)],[c6])).
% 6.17/6.49 cnf(c16,negated_conjecture,r1(skolem0001,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 6.17/6.49 cnf(c17,negated_conjecture,r1(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 6.17/6.49 cnf(c18,negated_conjecture,r1(skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c6])).
% 6.17/6.49 fof(reflexivity,axiom,(![X]:r1(X,X)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity)).
% 6.17/6.49 fof(c21,plain,(![X23]:r1(X23,X23)),inference(variable_rename,[status(thm)],[reflexivity])).
% 6.17/6.49 cnf(c22,plain,r1(X24,X24),inference(split_conjunct,[status(thm)],[c21])).
% 6.17/6.49 cnf(c12,negated_conjecture,~r1(skolem0001,X45)|~r1(X45,X44)|r1(X44,skolem0004(X45,X44))|~r1(X45,X46)|~p1(skolem0005(X45,X46)),inference(split_conjunct,[status(thm)],[c6])).
% 6.17/6.49 cnf(c20,negated_conjecture,~r1(skolem0007,X27)|p1(X27),inference(split_conjunct,[status(thm)],[c6])).
% 6.17/6.49 cnf(c11,negated_conjecture,~r1(skolem0001,X42)|~r1(X42,X41)|r1(X41,skolem0004(X42,X41))|~r1(X42,X43)|r1(X43,skolem0005(X42,X43)),inference(split_conjunct,[status(thm)],[c6])).
% 6.17/6.49 cnf(c73,plain,~r1(skolem0001,X58)|~r1(X58,X59)|r1(X59,skolem0004(X58,X59))|r1(X58,skolem0005(X58,X58)),inference(resolution,[status(thm)],[c11, c22])).
% 6.17/6.49 cnf(c161,plain,~r1(skolem0001,skolem0007)|r1(skolem0008,skolem0004(skolem0007,skolem0008))|r1(skolem0007,skolem0005(skolem0007,skolem0007)),inference(resolution,[status(thm)],[c73, c17])).
% 6.17/6.49 cnf(c1180,plain,r1(skolem0008,skolem0004(skolem0007,skolem0008))|r1(skolem0007,skolem0005(skolem0007,skolem0007)),inference(resolution,[status(thm)],[c161, c16])).
% 6.17/6.49 cnf(c1200,plain,r1(skolem0008,skolem0004(skolem0007,skolem0008))|p1(skolem0005(skolem0007,skolem0007)),inference(resolution,[status(thm)],[c1180, c20])).
% 6.17/6.49 cnf(c1227,plain,r1(skolem0008,skolem0004(skolem0007,skolem0008))|~r1(skolem0001,skolem0007)|~r1(skolem0007,X261)|r1(X261,skolem0004(skolem0007,X261))|~r1(skolem0007,skolem0007),inference(resolution,[status(thm)],[c1200, c12])).
% 6.17/6.49 cnf(c5074,plain,r1(skolem0008,skolem0004(skolem0007,skolem0008))|~r1(skolem0001,skolem0007)|~r1(skolem0007,X262)|r1(X262,skolem0004(skolem0007,X262)),inference(resolution,[status(thm)],[c1227, c22])).
% 6.17/6.49 cnf(c5092,plain,r1(skolem0008,skolem0004(skolem0007,skolem0008))|~r1(skolem0001,skolem0007),inference(resolution,[status(thm)],[c5074, c17])).
% 6.17/6.49 cnf(c5101,plain,r1(skolem0008,skolem0004(skolem0007,skolem0008)),inference(resolution,[status(thm)],[c5092, c16])).
% 6.17/6.49 cnf(c10,negated_conjecture,~r1(skolem0001,X39)|~r1(X39,X37)|~r1(X37,X38)|~p1(skolem0003(X39,X37,X38))|~r1(X37,X40)|p1(X40),inference(split_conjunct,[status(thm)],[c6])).
% 6.17/6.49 cnf(c14,negated_conjecture,~r1(skolem0001,X53)|~r1(X53,X51)|~r1(skolem0004(X53,X51),X52)|p1(X52)|~r1(X53,X54)|~p1(skolem0005(X53,X54)),inference(split_conjunct,[status(thm)],[c6])).
% 6.17/6.49 cnf(c9,negated_conjecture,~r1(skolem0001,X34)|~r1(X34,X32)|~r1(X32,X33)|r1(X33,skolem0003(X34,X32,X33))|~r1(X32,X35)|p1(X35),inference(split_conjunct,[status(thm)],[c6])).
% 6.17/6.49 cnf(c55,plain,~r1(skolem0001,X89)|~r1(X89,skolem0008)|~r1(skolem0008,X88)|r1(X88,skolem0003(X89,skolem0008,X88))|p1(skolem0009),inference(resolution,[status(thm)],[c9, c18])).
% 6.17/6.49 cnf(c5103,plain,~r1(skolem0001,X267)|~r1(X267,skolem0008)|r1(skolem0004(skolem0007,skolem0008),skolem0003(X267,skolem0008,skolem0004(skolem0007,skolem0008)))|p1(skolem0009),inference(resolution,[status(thm)],[c5101, c55])).
% 6.17/6.49 cnf(c5120,plain,~r1(skolem0001,skolem0007)|r1(skolem0004(skolem0007,skolem0008),skolem0003(skolem0007,skolem0008,skolem0004(skolem0007,skolem0008)))|p1(skolem0009),inference(resolution,[status(thm)],[c5103, c17])).
% 6.17/6.49 cnf(c5121,plain,r1(skolem0004(skolem0007,skolem0008),skolem0003(skolem0007,skolem0008,skolem0004(skolem0007,skolem0008)))|p1(skolem0009),inference(resolution,[status(thm)],[c5120, c16])).
% 6.17/6.49 cnf(c5136,plain,r1(skolem0004(skolem0007,skolem0008),skolem0003(skolem0007,skolem0008,skolem0004(skolem0007,skolem0008))),inference(resolution,[status(thm)],[c5121, c19])).
% 6.17/6.49 cnf(c5141,plain,~r1(skolem0001,skolem0007)|~r1(skolem0007,skolem0008)|p1(skolem0003(skolem0007,skolem0008,skolem0004(skolem0007,skolem0008)))|~r1(skolem0007,X422)|~p1(skolem0005(skolem0007,X422)),inference(resolution,[status(thm)],[c5136, c14])).
% 6.17/6.49 cnf(c13,negated_conjecture,~r1(skolem0001,X49)|~r1(X49,X47)|~r1(skolem0004(X49,X47),X48)|p1(X48)|~r1(X49,X50)|r1(X50,skolem0005(X49,X50)),inference(split_conjunct,[status(thm)],[c6])).
% 6.17/6.49 cnf(c5146,plain,~r1(skolem0001,skolem0007)|~r1(skolem0007,skolem0008)|p1(skolem0003(skolem0007,skolem0008,skolem0004(skolem0007,skolem0008)))|~r1(skolem0007,X446)|r1(X446,skolem0005(skolem0007,X446)),inference(resolution,[status(thm)],[c5136, c13])).
% 6.17/6.49 cnf(c6521,plain,~r1(skolem0001,skolem0007)|~r1(skolem0007,skolem0008)|p1(skolem0003(skolem0007,skolem0008,skolem0004(skolem0007,skolem0008)))|r1(skolem0007,skolem0005(skolem0007,skolem0007)),inference(resolution,[status(thm)],[c5146, c22])).
% 6.17/6.49 cnf(c6552,plain,~r1(skolem0001,skolem0007)|p1(skolem0003(skolem0007,skolem0008,skolem0004(skolem0007,skolem0008)))|r1(skolem0007,skolem0005(skolem0007,skolem0007)),inference(resolution,[status(thm)],[c6521, c17])).
% 6.17/6.49 cnf(c6553,plain,p1(skolem0003(skolem0007,skolem0008,skolem0004(skolem0007,skolem0008)))|r1(skolem0007,skolem0005(skolem0007,skolem0007)),inference(resolution,[status(thm)],[c6552, c16])).
% 6.17/6.49 cnf(c6556,plain,p1(skolem0003(skolem0007,skolem0008,skolem0004(skolem0007,skolem0008)))|p1(skolem0005(skolem0007,skolem0007)),inference(resolution,[status(thm)],[c6553, c20])).
% 6.17/6.49 cnf(c6583,plain,p1(skolem0003(skolem0007,skolem0008,skolem0004(skolem0007,skolem0008)))|~r1(skolem0001,skolem0007)|~r1(skolem0007,skolem0008)|~r1(skolem0007,skolem0007),inference(resolution,[status(thm)],[c6556, c5141])).
% 6.17/6.49 cnf(c6585,plain,p1(skolem0003(skolem0007,skolem0008,skolem0004(skolem0007,skolem0008)))|~r1(skolem0001,skolem0007)|~r1(skolem0007,skolem0008),inference(resolution,[status(thm)],[c6583, c22])).
% 6.17/6.49 cnf(c6586,plain,p1(skolem0003(skolem0007,skolem0008,skolem0004(skolem0007,skolem0008)))|~r1(skolem0001,skolem0007),inference(resolution,[status(thm)],[c6585, c17])).
% 6.17/6.49 cnf(c6587,plain,p1(skolem0003(skolem0007,skolem0008,skolem0004(skolem0007,skolem0008))),inference(resolution,[status(thm)],[c6586, c16])).
% 6.17/6.49 cnf(c6588,plain,~r1(skolem0001,skolem0007)|~r1(skolem0007,skolem0008)|~r1(skolem0008,skolem0004(skolem0007,skolem0008))|~r1(skolem0008,X449)|p1(X449),inference(resolution,[status(thm)],[c6587, c10])).
% 6.17/6.49 cnf(c6590,plain,~r1(skolem0001,skolem0007)|~r1(skolem0007,skolem0008)|~r1(skolem0008,X450)|p1(X450),inference(resolution,[status(thm)],[c6588, c5101])).
% 6.17/6.49 cnf(c6598,plain,~r1(skolem0001,skolem0007)|~r1(skolem0007,skolem0008)|p1(skolem0009),inference(resolution,[status(thm)],[c6590, c18])).
% 6.17/6.49 cnf(c6600,plain,~r1(skolem0001,skolem0007)|p1(skolem0009),inference(resolution,[status(thm)],[c6598, c17])).
% 6.17/6.49 cnf(c6601,plain,p1(skolem0009),inference(resolution,[status(thm)],[c6600, c16])).
% 6.17/6.49 cnf(c6602,plain,$false,inference(resolution,[status(thm)],[c6601, c19])).
% 6.17/6.49 % SZS output end CNFRefutation
% 6.17/6.49
% 6.17/6.49 % Initial clauses : 15
% 6.17/6.49 % Processed clauses : 906
% 6.17/6.49 % Factors computed : 93
% 6.17/6.49 % Resolvents computed: 6487
% 6.17/6.49 % Tautologies deleted: 4
% 6.17/6.49 % Forward subsumed : 945
% 6.17/6.49 % Backward subsumed : 650
% 6.17/6.49 % -------- CPU Time ---------
% 6.17/6.49 % User time : 6.095 s
% 6.17/6.49 % System time : 0.052 s
% 6.17/6.49 % Total time : 6.147 s
%------------------------------------------------------------------------------