%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL650+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:51 PM UTC 2026
% Result : Theorem 0.96s 1.24s
% Output : CNFRefutation 0.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL650+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 : n003.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 : Sat Sep 5 20:01:06 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.10/0.42 (re.compile("\."), Token.FullStop),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.10/0.42 (re.compile("\("), Token.OpenPar),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.10/0.42 (re.compile("\)"), Token.ClosePar),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.10/0.42 (re.compile("\["), Token.OpenSquare),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.10/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.10/0.42 (re.compile("~\|"), Token.Nor),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.10/0.42 (re.compile("\|"), Token.Or),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.10/0.42 (re.compile("\?"), Token.Existential),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.10/0.42 (re.compile("\s+"), Token.WhiteSpace),
% 0.10/0.42 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.10/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.24/0.49 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.49 """
% 0.24/0.50 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.50 """
% 0.24/0.59 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.24/0.59 """
% 0.96/1.24 % Version: 1.5
% 0.96/1.24 % SZS status Theorem
% 0.96/1.24 % SZS output start CNFRefutation
% 0.96/1.24 fof(main,conjecture,(~(?[X]:(~((((![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|((((~p8(X))&(~p6(X)))&(~p4(X)))&(~p2(X)))))))))))|(![Y]:((~r1(X,Y))|p5(Y))))|(~(![Y]:((~r1(X,Y))|(~(((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(~(((~p3(X))&(~p1(X)))|(p1(X)&p3(X)))))))))))|(![X]:((~r1(Y,X))|p4(X))))|(~(![X]:((~r1(Y,X))|(~(((~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(~(((~p2(X))&(~p3(X)))|(p3(X)&p2(X)))))))))|(![Y]:((~r1(X,Y))|p3(Y))))|(~(![Y]:((~r1(X,Y))|(~(~(![X]:((~r1(Y,X))|(~(((~p1(X))&(~p2(X)))|(p2(X)&p1(X))))))))))))))))))))))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(((p4(X)&p3(X))&p2(X))&p1(X)))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 0.96/1.24 fof(c0,negated_conjecture,(~(~(?[X]:(~((((![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|((((~p8(X))&(~p6(X)))&(~p4(X)))&(~p2(X)))))))))))|(![Y]:((~r1(X,Y))|p5(Y))))|(~(![Y]:((~r1(X,Y))|(~(((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(~(((~p3(X))&(~p1(X)))|(p1(X)&p3(X)))))))))))|(![X]:((~r1(Y,X))|p4(X))))|(~(![X]:((~r1(Y,X))|(~(((~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(~(((~p2(X))&(~p3(X)))|(p3(X)&p2(X)))))))))|(![Y]:((~r1(X,Y))|p3(Y))))|(~(![Y]:((~r1(X,Y))|(~(~(![X]:((~r1(Y,X))|(~(((~p1(X))&(~p2(X)))|(p2(X)&p1(X))))))))))))))))))))))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(((p4(X)&p3(X))&p2(X))&p1(X))))))))))))))),inference(assume_negation,[status(cth)],[main])).
% 0.96/1.24 fof(c1,negated_conjecture,(~(~(?[X]:(~((((![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(((~p8(X)&~p6(X))&~p4(X))&~p2(X))))))))))|(![Y]:(~r1(X,Y)|p5(Y))))|(~(![Y]:(~r1(X,Y)|(~(((~(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(~((~p3(X)&~p1(X))|(p1(X)&p3(X)))))))))))|(![X]:(~r1(Y,X)|p4(X))))|(~(![X]:(~r1(Y,X)|(~(((~(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(~((~p2(X)&~p3(X))|(p3(X)&p2(X)))))))))|(![Y]:(~r1(X,Y)|p3(Y))))|(~(![Y]:(~r1(X,Y)|(~(~(![X]:(~r1(Y,X)|(~((~p1(X)&~p2(X))|(p2(X)&p1(X))))))))))))))))))))))|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(((p4(X)&p3(X))&p2(X))&p1(X))))))))))))))),inference(fof_simplification,[status(thm)],[c0])).
% 0.96/1.24 fof(c2,negated_conjecture,(?[X]:((((?[Y]:(r1(X,Y)&(?[X]:(r1(Y,X)&(?[Y]:(r1(X,Y)&(?[X]:(r1(Y,X)&(((p8(X)|p6(X))|p4(X))|p2(X))))))))))&(?[Y]:(r1(X,Y)&~p5(Y))))&(![Y]:(~r1(X,Y)|(((![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|((p3(X)|p1(X))&(~p1(X)|~p3(X)))))))))&(?[X]:(r1(Y,X)&~p4(X))))&(![X]:(~r1(Y,X)|(((![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|((p2(X)|p3(X))&(~p3(X)|~p2(X)))))))&(?[Y]:(r1(X,Y)&~p3(Y))))&(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|((p1(X)|p2(X))&(~p2(X)|~p1(X))))))))))))))&(?[Y]:(r1(X,Y)&(?[X]:(r1(Y,X)&(?[Y]:(r1(X,Y)&(?[X]:(r1(Y,X)&(((~p4(X)|~p3(X))|~p2(X))|~p1(X)))))))))))),inference(fof_nnf,[status(thm)],[c1])).
% 0.96/1.24 fof(c3,negated_conjecture,(?[X2]:((((?[X3]:(r1(X2,X3)&(?[X4]:(r1(X3,X4)&(?[X5]:(r1(X4,X5)&(?[X6]:(r1(X5,X6)&(((p8(X6)|p6(X6))|p4(X6))|p2(X6))))))))))&(?[X7]:(r1(X2,X7)&~p5(X7))))&(![X8]:(~r1(X2,X8)|(((![X9]:(~r1(X8,X9)|(![X10]:(~r1(X9,X10)|(![X11]:(~r1(X10,X11)|((p3(X11)|p1(X11))&(~p1(X11)|~p3(X11)))))))))&(?[X12]:(r1(X8,X12)&~p4(X12))))&(![X13]:(~r1(X8,X13)|(((![X14]:(~r1(X13,X14)|(![X15]:(~r1(X14,X15)|((p2(X15)|p3(X15))&(~p3(X15)|~p2(X15)))))))&(?[X16]:(r1(X13,X16)&~p3(X16))))&(![X17]:(~r1(X13,X17)|(![X18]:(~r1(X17,X18)|((p1(X18)|p2(X18))&(~p2(X18)|~p1(X18))))))))))))))&(?[X19]:(r1(X2,X19)&(?[X20]:(r1(X19,X20)&(?[X21]:(r1(X20,X21)&(?[X22]:(r1(X21,X22)&(((~p4(X22)|~p3(X22))|~p2(X22))|~p1(X22)))))))))))),inference(variable_rename,[status(thm)],[c2])).
% 0.96/1.24 fof(c5,negated_conjecture,(![X8]:(![X9]:(![X10]:(![X11]:(![X13]:(![X14]:(![X15]:(![X17]:(![X18]:((((r1(skolem0001,skolem0002)&(r1(skolem0002,skolem0003)&(r1(skolem0003,skolem0004)&(r1(skolem0004,skolem0005)&(((p8(skolem0005)|p6(skolem0005))|p4(skolem0005))|p2(skolem0005))))))&(r1(skolem0001,skolem0006)&~p5(skolem0006)))&(~r1(skolem0001,X8)|(((~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|((p3(X11)|p1(X11))&(~p1(X11)|~p3(X11))))))&(r1(X8,skolem0007(X8))&~p4(skolem0007(X8))))&(~r1(X8,X13)|(((~r1(X13,X14)|(~r1(X14,X15)|((p2(X15)|p3(X15))&(~p3(X15)|~p2(X15)))))&(r1(X13,skolem0008(X8,X13))&~p3(skolem0008(X8,X13))))&(~r1(X13,X17)|(~r1(X17,X18)|((p1(X18)|p2(X18))&(~p2(X18)|~p1(X18))))))))))&(r1(skolem0001,skolem0009)&(r1(skolem0009,skolem0010)&(r1(skolem0010,skolem0011)&(r1(skolem0011,skolem0012)&(((~p4(skolem0012)|~p3(skolem0012))|~p2(skolem0012))|~p1(skolem0012)))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((((r1(skolem0001,skolem0002)&(r1(skolem0002,skolem0003)&(r1(skolem0003,skolem0004)&(r1(skolem0004,skolem0005)&(((p8(skolem0005)|p6(skolem0005))|p4(skolem0005))|p2(skolem0005))))))&(r1(skolem0001,skolem0006)&~p5(skolem0006)))&(![X8]:(~r1(skolem0001,X8)|(((![X9]:(~r1(X8,X9)|(![X10]:(~r1(X9,X10)|(![X11]:(~r1(X10,X11)|((p3(X11)|p1(X11))&(~p1(X11)|~p3(X11)))))))))&(r1(X8,skolem0007(X8))&~p4(skolem0007(X8))))&(![X13]:(~r1(X8,X13)|(((![X14]:(~r1(X13,X14)|(![X15]:(~r1(X14,X15)|((p2(X15)|p3(X15))&(~p3(X15)|~p2(X15)))))))&(r1(X13,skolem0008(X8,X13))&~p3(skolem0008(X8,X13))))&(![X17]:(~r1(X13,X17)|(![X18]:(~r1(X17,X18)|((p1(X18)|p2(X18))&(~p2(X18)|~p1(X18))))))))))))))&(r1(skolem0001,skolem0009)&(r1(skolem0009,skolem0010)&(r1(skolem0010,skolem0011)&(r1(skolem0011,skolem0012)&(((~p4(skolem0012)|~p3(skolem0012))|~p2(skolem0012))|~p1(skolem0012))))))),inference(skolemize,[status(esa)],[c3])).])).
% 0.96/1.24 fof(c6,negated_conjecture,(![X8]:(![X9]:(![X10]:(![X11]:(![X13]:(![X14]:(![X15]:(![X17]:(![X18]:((((r1(skolem0001,skolem0002)&(r1(skolem0002,skolem0003)&(r1(skolem0003,skolem0004)&(r1(skolem0004,skolem0005)&(((p8(skolem0005)|p6(skolem0005))|p4(skolem0005))|p2(skolem0005))))))&(r1(skolem0001,skolem0006)&~p5(skolem0006)))&((((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(p3(X11)|p1(X11))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~p1(X11)|~p3(X11)))))))&((~r1(skolem0001,X8)|r1(X8,skolem0007(X8)))&(~r1(skolem0001,X8)|~p4(skolem0007(X8)))))&((((~r1(skolem0001,X8)|(~r1(X8,X13)|(~r1(X13,X14)|(~r1(X14,X15)|(p2(X15)|p3(X15))))))&(~r1(skolem0001,X8)|(~r1(X8,X13)|(~r1(X13,X14)|(~r1(X14,X15)|(~p3(X15)|~p2(X15)))))))&((~r1(skolem0001,X8)|(~r1(X8,X13)|r1(X13,skolem0008(X8,X13))))&(~r1(skolem0001,X8)|(~r1(X8,X13)|~p3(skolem0008(X8,X13))))))&((~r1(skolem0001,X8)|(~r1(X8,X13)|(~r1(X13,X17)|(~r1(X17,X18)|(p1(X18)|p2(X18))))))&(~r1(skolem0001,X8)|(~r1(X8,X13)|(~r1(X13,X17)|(~r1(X17,X18)|(~p2(X18)|~p1(X18))))))))))&(r1(skolem0001,skolem0009)&(r1(skolem0009,skolem0010)&(r1(skolem0010,skolem0011)&(r1(skolem0011,skolem0012)&(((~p4(skolem0012)|~p3(skolem0012))|~p2(skolem0012))|~p1(skolem0012)))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 0.96/1.24 cnf(c7,negated_conjecture,r1(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c6])).
% 0.96/1.24 cnf(c8,negated_conjecture,r1(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c6])).
% 0.96/1.24 cnf(c9,negated_conjecture,r1(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.96/1.24 cnf(c10,negated_conjecture,r1(skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 0.96/1.24 cnf(c15,negated_conjecture,~r1(skolem0001,X29)|~r1(X29,X30)|~r1(X30,X32)|~r1(X32,X31)|~p1(X31)|~p3(X31),inference(split_conjunct,[status(thm)],[c6])).
% 0.96/1.24 cnf(c55,plain,~r1(skolem0001,X148)|~r1(X148,X147)|~r1(X147,skolem0004)|~p1(skolem0005)|~p3(skolem0005),inference(resolution,[status(thm)],[c15, c10])).
% 0.96/1.24 cnf(c377,plain,~r1(skolem0001,X149)|~r1(X149,skolem0003)|~p1(skolem0005)|~p3(skolem0005),inference(resolution,[status(thm)],[c55, c9])).
% 0.96/1.24 cnf(c378,plain,~r1(skolem0001,skolem0002)|~p1(skolem0005)|~p3(skolem0005),inference(resolution,[status(thm)],[c377, c8])).
% 0.96/1.24 cnf(c379,plain,~p1(skolem0005)|~p3(skolem0005),inference(resolution,[status(thm)],[c378, c7])).
% 0.96/1.24 cnf(c18,negated_conjecture,~r1(skolem0001,X37)|~r1(X37,X40)|~r1(X40,X38)|~r1(X38,X39)|p2(X39)|p3(X39),inference(split_conjunct,[status(thm)],[c6])).
% 0.96/1.24 cnf(c83,plain,~r1(skolem0001,X180)|~r1(X180,X179)|~r1(X179,skolem0004)|p2(skolem0005)|p3(skolem0005),inference(resolution,[status(thm)],[c18, c10])).
% 0.96/1.24 cnf(c419,plain,~r1(skolem0001,X181)|~r1(X181,skolem0003)|p2(skolem0005)|p3(skolem0005),inference(resolution,[status(thm)],[c83, c9])).
% 0.96/1.24 cnf(c420,plain,~r1(skolem0001,skolem0002)|p2(skolem0005)|p3(skolem0005),inference(resolution,[status(thm)],[c419, c8])).
% 0.96/1.24 cnf(c421,plain,p2(skolem0005)|p3(skolem0005),inference(resolution,[status(thm)],[c420, c7])).
% 0.96/1.24 cnf(c422,plain,p2(skolem0005)|~p1(skolem0005),inference(resolution,[status(thm)],[c421, c379])).
% 0.96/1.24 cnf(c22,negated_conjecture,~r1(skolem0001,X45)|~r1(X45,X46)|~r1(X46,X47)|~r1(X47,X48)|p1(X48)|p2(X48),inference(split_conjunct,[status(thm)],[c6])).
% 0.96/1.24 cnf(c125,plain,~r1(skolem0001,X249)|~r1(X249,X250)|~r1(X250,skolem0004)|p1(skolem0005)|p2(skolem0005),inference(resolution,[status(thm)],[c22, c10])).
% 0.96/1.24 cnf(c505,plain,~r1(skolem0001,X251)|~r1(X251,skolem0003)|p1(skolem0005)|p2(skolem0005),inference(resolution,[status(thm)],[c125, c9])).
% 0.96/1.24 cnf(c506,plain,~r1(skolem0001,skolem0002)|p1(skolem0005)|p2(skolem0005),inference(resolution,[status(thm)],[c505, c8])).
% 0.96/1.24 cnf(c507,plain,p1(skolem0005)|p2(skolem0005),inference(resolution,[status(thm)],[c506, c7])).
% 0.96/1.24 cnf(c511,plain,p2(skolem0005),inference(resolution,[status(thm)],[c507, c422])).
% 0.96/1.24 cnf(c14,negated_conjecture,~r1(skolem0001,X23)|~r1(X23,X24)|~r1(X24,X26)|~r1(X26,X25)|p3(X25)|p1(X25),inference(split_conjunct,[status(thm)],[c6])).
% 0.96/1.24 cnf(c35,plain,~r1(skolem0001,X83)|~r1(X83,X84)|~r1(X84,skolem0004)|p3(skolem0005)|p1(skolem0005),inference(resolution,[status(thm)],[c14, c10])).
% 0.96/1.24 cnf(c225,plain,~r1(skolem0001,X86)|~r1(X86,skolem0003)|p3(skolem0005)|p1(skolem0005),inference(resolution,[status(thm)],[c35, c9])).
% 0.96/1.24 cnf(c226,plain,~r1(skolem0001,skolem0002)|p3(skolem0005)|p1(skolem0005),inference(resolution,[status(thm)],[c225, c8])).
% 0.96/1.24 cnf(c227,plain,p3(skolem0005)|p1(skolem0005),inference(resolution,[status(thm)],[c226, c7])).
% 0.96/1.24 cnf(c19,negated_conjecture,~r1(skolem0001,X41)|~r1(X41,X44)|~r1(X44,X42)|~r1(X42,X43)|~p3(X43)|~p2(X43),inference(split_conjunct,[status(thm)],[c6])).
% 0.96/1.24 cnf(c103,plain,~r1(skolem0001,X214)|~r1(X214,X215)|~r1(X215,skolem0004)|~p3(skolem0005)|~p2(skolem0005),inference(resolution,[status(thm)],[c19, c10])).
% 0.96/1.24 cnf(c463,plain,~r1(skolem0001,X217)|~r1(X217,skolem0003)|~p3(skolem0005)|~p2(skolem0005),inference(resolution,[status(thm)],[c103, c9])).
% 0.96/1.24 cnf(c465,plain,~r1(skolem0001,skolem0002)|~p3(skolem0005)|~p2(skolem0005),inference(resolution,[status(thm)],[c463, c8])).
% 0.96/1.24 cnf(c466,plain,~p3(skolem0005)|~p2(skolem0005),inference(resolution,[status(thm)],[c465, c7])).
% 0.96/1.24 cnf(c513,plain,~p3(skolem0005),inference(resolution,[status(thm)],[c511, c466])).
% 0.96/1.24 cnf(c514,plain,p1(skolem0005),inference(resolution,[status(thm)],[c513, c227])).
% 0.96/1.24 cnf(c23,negated_conjecture,~r1(skolem0001,X53)|~r1(X53,X54)|~r1(X54,X55)|~r1(X55,X56)|~p2(X56)|~p1(X56),inference(split_conjunct,[status(thm)],[c6])).
% 0.96/1.24 cnf(c160,plain,~r1(skolem0001,X286)|~r1(X286,X285)|~r1(X285,skolem0004)|~p2(skolem0005)|~p1(skolem0005),inference(resolution,[status(thm)],[c23, c10])).
% 0.96/1.24 cnf(c563,plain,~r1(skolem0001,X287)|~r1(X287,skolem0003)|~p2(skolem0005)|~p1(skolem0005),inference(resolution,[status(thm)],[c160, c9])).
% 0.96/1.24 cnf(c564,plain,~r1(skolem0001,skolem0002)|~p2(skolem0005)|~p1(skolem0005),inference(resolution,[status(thm)],[c563, c8])).
% 0.96/1.24 cnf(c565,plain,~p2(skolem0005)|~p1(skolem0005),inference(resolution,[status(thm)],[c564, c7])).
% 0.96/1.24 cnf(c566,plain,~p2(skolem0005),inference(resolution,[status(thm)],[c565, c514])).
% 0.96/1.24 cnf(c567,plain,$false,inference(resolution,[status(thm)],[c566, c511])).
% 0.96/1.24 % SZS output end CNFRefutation
% 0.96/1.24
% 0.96/1.24 % Initial clauses : 22
% 0.96/1.24 % Processed clauses : 333
% 0.96/1.24 % Factors computed : 206
% 0.96/1.24 % Resolvents computed: 333
% 0.96/1.24 % Tautologies deleted: 5
% 0.96/1.24 % Forward subsumed : 101
% 0.96/1.24 % Backward subsumed : 55
% 0.96/1.24 % -------- CPU Time ---------
% 0.96/1.24 % User time : 0.854 s
% 0.96/1.24 % System time : 0.020 s
% 0.96/1.24 % Total time : 0.874 s
%------------------------------------------------------------------------------