%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL668+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:58 PM UTC 2026
% Result : Theorem 33.55s 33.81s
% Output : CNFRefutation 33.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL668+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 : n014.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 07:02:42 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.10/0.42 (re.compile("\."), Token.FullStop),
% 0.10/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.10/0.42 (re.compile("\("), Token.OpenPar),
% 0.10/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.10/0.42 (re.compile("\)"), Token.ClosePar),
% 0.10/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.10/0.42 (re.compile("\["), Token.OpenSquare),
% 0.10/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.10/0.42 (re.compile("\]"), Token.CloseSquare),
% 0.10/0.42 /export/starexec/sandbox2/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.10/0.42 (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.22/0.50 /export/starexec/sandbox2/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.22/0.50 /export/starexec/sandbox2/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.50 """
% 0.32/0.59 /export/starexec/sandbox2/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.59 """
% 33.55/33.81 % Version: 1.5
% 33.55/33.81 % SZS status Theorem
% 33.55/33.81 % SZS output start CNFRefutation
% 33.55/33.81 fof(reflexivity,axiom,(![X]:r1(X,X)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity)).
% 33.55/33.81 fof(c41,plain,(![X50]:r1(X50,X50)),inference(variable_rename,[status(thm)],[reflexivity])).
% 33.55/33.81 cnf(c42,plain,r1(X51,X51),inference(split_conjunct,[status(thm)],[c41])).
% 33.55/33.81 fof(main,conjecture,(~(?[X]:(~((((![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|((((((~p12(X))&(~p10(X)))&(~p8(X)))&(~p6(X)))&(~p4(X)))&(~p2(X)))))))))))))))|(![Y]:((~r1(X,Y))|p7(Y))))|(~(![Y]:((~r1(X,Y))|(~(((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(~(((~p5(X))&(~p1(X)))|(p1(X)&p5(X)))))))))))))))))))|(![X]:((~r1(Y,X))|p6(X))))|(~(![X]:((~r1(Y,X))|(~(((~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(~(((~p4(X))&(~p5(X)))|(p5(X)&p4(X)))))))))))))))))|(![Y]:((~r1(X,Y))|p5(Y))))|(~(![Y]:((~r1(X,Y))|(~(((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(~(((~p3(X))&(~p4(X)))|(p4(X)&p3(X)))))))))))))))|(![X]:((~r1(Y,X))|p4(X))))|(~(![X]:((~r1(Y,X))|(~(((~(![Y]:((~r1(X,Y))|(![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))|(![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))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(((((p6(X)&p5(X))&p4(X))&p3(X))&p2(X))&p1(X)))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 33.55/33.81 fof(c0,negated_conjecture,(~(~(?[X]:(~((((![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|((((((~p12(X))&(~p10(X)))&(~p8(X)))&(~p6(X)))&(~p4(X)))&(~p2(X)))))))))))))))|(![Y]:((~r1(X,Y))|p7(Y))))|(~(![Y]:((~r1(X,Y))|(~(((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(~(((~p5(X))&(~p1(X)))|(p1(X)&p5(X)))))))))))))))))))|(![X]:((~r1(Y,X))|p6(X))))|(~(![X]:((~r1(Y,X))|(~(((~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(~(((~p4(X))&(~p5(X)))|(p5(X)&p4(X)))))))))))))))))|(![Y]:((~r1(X,Y))|p5(Y))))|(~(![Y]:((~r1(X,Y))|(~(((~(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(~(((~p3(X))&(~p4(X)))|(p4(X)&p3(X)))))))))))))))|(![X]:((~r1(Y,X))|p4(X))))|(~(![X]:((~r1(Y,X))|(~(((~(![Y]:((~r1(X,Y))|(![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))|(![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))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(((((p6(X)&p5(X))&p4(X))&p3(X))&p2(X))&p1(X))))))))))))))))))),inference(assume_negation,[status(cth)],[main])).
% 33.55/33.81 fof(c1,negated_conjecture,(~(~(?[X]:(~((((![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(((((~p12(X)&~p10(X))&~p8(X))&~p6(X))&~p4(X))&~p2(X))))))))))))))|(![Y]:(~r1(X,Y)|p7(Y))))|(~(![Y]:(~r1(X,Y)|(~(((~(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(~((~p5(X)&~p1(X))|(p1(X)&p5(X)))))))))))))))))))|(![X]:(~r1(Y,X)|p6(X))))|(~(![X]:(~r1(Y,X)|(~(((~(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(~((~p4(X)&~p5(X))|(p5(X)&p4(X)))))))))))))))))|(![Y]:(~r1(X,Y)|p5(Y))))|(~(![Y]:(~r1(X,Y)|(~(((~(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(~((~p3(X)&~p4(X))|(p4(X)&p3(X)))))))))))))))|(![X]:(~r1(Y,X)|p4(X))))|(~(![X]:(~r1(Y,X)|(~(((~(![Y]:(~r1(X,Y)|(![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)|(![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)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(((((p6(X)&p5(X))&p4(X))&p3(X))&p2(X))&p1(X))))))))))))))))))),inference(fof_simplification,[status(thm)],[c0])).
% 33.55/33.81 fof(c2,negated_conjecture,(?[X]:((((?[Y]:(r1(X,Y)&(?[X]:(r1(Y,X)&(?[Y]:(r1(X,Y)&(?[X]:(r1(Y,X)&(?[Y]:(r1(X,Y)&(?[X]:(r1(Y,X)&(((((p12(X)|p10(X))|p8(X))|p6(X))|p4(X))|p2(X))))))))))))))&(?[Y]:(r1(X,Y)&~p7(Y))))&(![Y]:(~r1(X,Y)|(((![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|((p5(X)|p1(X))&(~p1(X)|~p5(X)))))))))))))))))&(?[X]:(r1(Y,X)&~p6(X))))&(![X]:(~r1(Y,X)|(((![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|((p4(X)|p5(X))&(~p5(X)|~p4(X)))))))))))))))&(?[Y]:(r1(X,Y)&~p5(Y))))&(![Y]:(~r1(X,Y)|(((![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|(![Y]:(~r1(X,Y)|(![X]:(~r1(Y,X)|((p3(X)|p4(X))&(~p4(X)|~p3(X)))))))))))))&(?[X]:(r1(Y,X)&~p4(X))))&(![X]:(~r1(Y,X)|(((![Y]:(~r1(X,Y)|(![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)|(![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)&(?[Y]:(r1(X,Y)&(?[X]:(r1(Y,X)&(((((~p6(X)|~p5(X))|~p4(X))|~p3(X))|~p2(X))|~p1(X)))))))))))))))),inference(fof_nnf,[status(thm)],[c1])).
% 33.55/33.81 fof(c3,negated_conjecture,(?[X2]:((((?[X3]:(r1(X2,X3)&(?[X4]:(r1(X3,X4)&(?[X5]:(r1(X4,X5)&(?[X6]:(r1(X5,X6)&(?[X7]:(r1(X6,X7)&(?[X8]:(r1(X7,X8)&(((((p12(X8)|p10(X8))|p8(X8))|p6(X8))|p4(X8))|p2(X8))))))))))))))&(?[X9]:(r1(X2,X9)&~p7(X9))))&(![X10]:(~r1(X2,X10)|(((![X11]:(~r1(X10,X11)|(![X12]:(~r1(X11,X12)|(![X13]:(~r1(X12,X13)|(![X14]:(~r1(X13,X14)|(![X15]:(~r1(X14,X15)|(![X16]:(~r1(X15,X16)|(![X17]:(~r1(X16,X17)|((p5(X17)|p1(X17))&(~p1(X17)|~p5(X17)))))))))))))))))&(?[X18]:(r1(X10,X18)&~p6(X18))))&(![X19]:(~r1(X10,X19)|(((![X20]:(~r1(X19,X20)|(![X21]:(~r1(X20,X21)|(![X22]:(~r1(X21,X22)|(![X23]:(~r1(X22,X23)|(![X24]:(~r1(X23,X24)|(![X25]:(~r1(X24,X25)|((p4(X25)|p5(X25))&(~p5(X25)|~p4(X25)))))))))))))))&(?[X26]:(r1(X19,X26)&~p5(X26))))&(![X27]:(~r1(X19,X27)|(((![X28]:(~r1(X27,X28)|(![X29]:(~r1(X28,X29)|(![X30]:(~r1(X29,X30)|(![X31]:(~r1(X30,X31)|(![X32]:(~r1(X31,X32)|((p3(X32)|p4(X32))&(~p4(X32)|~p3(X32)))))))))))))&(?[X33]:(r1(X27,X33)&~p4(X33))))&(![X34]:(~r1(X27,X34)|(((![X35]:(~r1(X34,X35)|(![X36]:(~r1(X35,X36)|(![X37]:(~r1(X36,X37)|(![X38]:(~r1(X37,X38)|((p2(X38)|p3(X38))&(~p3(X38)|~p2(X38)))))))))))&(?[X39]:(r1(X34,X39)&~p3(X39))))&(![X40]:(~r1(X34,X40)|(![X41]:(~r1(X40,X41)|(![X42]:(~r1(X41,X42)|(![X43]:(~r1(X42,X43)|((p1(X43)|p2(X43))&(~p2(X43)|~p1(X43))))))))))))))))))))))))&(?[X44]:(r1(X2,X44)&(?[X45]:(r1(X44,X45)&(?[X46]:(r1(X45,X46)&(?[X47]:(r1(X46,X47)&(?[X48]:(r1(X47,X48)&(?[X49]:(r1(X48,X49)&(((((~p6(X49)|~p5(X49))|~p4(X49))|~p3(X49))|~p2(X49))|~p1(X49)))))))))))))))),inference(variable_rename,[status(thm)],[c2])).
% 33.55/33.81 fof(c5,negated_conjecture,(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X40]:(![X41]:(![X42]:(![X43]:((((r1(skolem0001,skolem0002)&(r1(skolem0002,skolem0003)&(r1(skolem0003,skolem0004)&(r1(skolem0004,skolem0005)&(r1(skolem0005,skolem0006)&(r1(skolem0006,skolem0007)&(((((p12(skolem0007)|p10(skolem0007))|p8(skolem0007))|p6(skolem0007))|p4(skolem0007))|p2(skolem0007))))))))&(r1(skolem0001,skolem0008)&~p7(skolem0008)))&(~r1(skolem0001,X10)|(((~r1(X10,X11)|(~r1(X11,X12)|(~r1(X12,X13)|(~r1(X13,X14)|(~r1(X14,X15)|(~r1(X15,X16)|(~r1(X16,X17)|((p5(X17)|p1(X17))&(~p1(X17)|~p5(X17))))))))))&(r1(X10,skolem0009(X10))&~p6(skolem0009(X10))))&(~r1(X10,X19)|(((~r1(X19,X20)|(~r1(X20,X21)|(~r1(X21,X22)|(~r1(X22,X23)|(~r1(X23,X24)|(~r1(X24,X25)|((p4(X25)|p5(X25))&(~p5(X25)|~p4(X25)))))))))&(r1(X19,skolem0010(X10,X19))&~p5(skolem0010(X10,X19))))&(~r1(X19,X27)|(((~r1(X27,X28)|(~r1(X28,X29)|(~r1(X29,X30)|(~r1(X30,X31)|(~r1(X31,X32)|((p3(X32)|p4(X32))&(~p4(X32)|~p3(X32))))))))&(r1(X27,skolem0011(X10,X19,X27))&~p4(skolem0011(X10,X19,X27))))&(~r1(X27,X34)|(((~r1(X34,X35)|(~r1(X35,X36)|(~r1(X36,X37)|(~r1(X37,X38)|((p2(X38)|p3(X38))&(~p3(X38)|~p2(X38)))))))&(r1(X34,skolem0012(X10,X19,X27,X34))&~p3(skolem0012(X10,X19,X27,X34))))&(~r1(X34,X40)|(~r1(X40,X41)|(~r1(X41,X42)|(~r1(X42,X43)|((p1(X43)|p2(X43))&(~p2(X43)|~p1(X43))))))))))))))))&(r1(skolem0001,skolem0013)&(r1(skolem0013,skolem0014)&(r1(skolem0014,skolem0015)&(r1(skolem0015,skolem0016)&(r1(skolem0016,skolem0017)&(r1(skolem0017,skolem0018)&(((((~p6(skolem0018)|~p5(skolem0018))|~p4(skolem0018))|~p3(skolem0018))|~p2(skolem0018))|~p1(skolem0018))))))))))))))))))))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((((r1(skolem0001,skolem0002)&(r1(skolem0002,skolem0003)&(r1(skolem0003,skolem0004)&(r1(skolem0004,skolem0005)&(r1(skolem0005,skolem0006)&(r1(skolem0006,skolem0007)&(((((p12(skolem0007)|p10(skolem0007))|p8(skolem0007))|p6(skolem0007))|p4(skolem0007))|p2(skolem0007))))))))&(r1(skolem0001,skolem0008)&~p7(skolem0008)))&(![X10]:(~r1(skolem0001,X10)|(((![X11]:(~r1(X10,X11)|(![X12]:(~r1(X11,X12)|(![X13]:(~r1(X12,X13)|(![X14]:(~r1(X13,X14)|(![X15]:(~r1(X14,X15)|(![X16]:(~r1(X15,X16)|(![X17]:(~r1(X16,X17)|((p5(X17)|p1(X17))&(~p1(X17)|~p5(X17)))))))))))))))))&(r1(X10,skolem0009(X10))&~p6(skolem0009(X10))))&(![X19]:(~r1(X10,X19)|(((![X20]:(~r1(X19,X20)|(![X21]:(~r1(X20,X21)|(![X22]:(~r1(X21,X22)|(![X23]:(~r1(X22,X23)|(![X24]:(~r1(X23,X24)|(![X25]:(~r1(X24,X25)|((p4(X25)|p5(X25))&(~p5(X25)|~p4(X25)))))))))))))))&(r1(X19,skolem0010(X10,X19))&~p5(skolem0010(X10,X19))))&(![X27]:(~r1(X19,X27)|(((![X28]:(~r1(X27,X28)|(![X29]:(~r1(X28,X29)|(![X30]:(~r1(X29,X30)|(![X31]:(~r1(X30,X31)|(![X32]:(~r1(X31,X32)|((p3(X32)|p4(X32))&(~p4(X32)|~p3(X32)))))))))))))&(r1(X27,skolem0011(X10,X19,X27))&~p4(skolem0011(X10,X19,X27))))&(![X34]:(~r1(X27,X34)|(((![X35]:(~r1(X34,X35)|(![X36]:(~r1(X35,X36)|(![X37]:(~r1(X36,X37)|(![X38]:(~r1(X37,X38)|((p2(X38)|p3(X38))&(~p3(X38)|~p2(X38)))))))))))&(r1(X34,skolem0012(X10,X19,X27,X34))&~p3(skolem0012(X10,X19,X27,X34))))&(![X40]:(~r1(X34,X40)|(![X41]:(~r1(X40,X41)|(![X42]:(~r1(X41,X42)|(![X43]:(~r1(X42,X43)|((p1(X43)|p2(X43))&(~p2(X43)|~p1(X43))))))))))))))))))))))))&(r1(skolem0001,skolem0013)&(r1(skolem0013,skolem0014)&(r1(skolem0014,skolem0015)&(r1(skolem0015,skolem0016)&(r1(skolem0016,skolem0017)&(r1(skolem0017,skolem0018)&(((((~p6(skolem0018)|~p5(skolem0018))|~p4(skolem0018))|~p3(skolem0018))|~p2(skolem0018))|~p1(skolem0018))))))))),inference(skolemize,[status(esa)],[c3])).])).
% 33.55/33.81 fof(c6,negated_conjecture,(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X40]:(![X41]:(![X42]:(![X43]:((((r1(skolem0001,skolem0002)&(r1(skolem0002,skolem0003)&(r1(skolem0003,skolem0004)&(r1(skolem0004,skolem0005)&(r1(skolem0005,skolem0006)&(r1(skolem0006,skolem0007)&(((((p12(skolem0007)|p10(skolem0007))|p8(skolem0007))|p6(skolem0007))|p4(skolem0007))|p2(skolem0007))))))))&(r1(skolem0001,skolem0008)&~p7(skolem0008)))&((((~r1(skolem0001,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~r1(X12,X13)|(~r1(X13,X14)|(~r1(X14,X15)|(~r1(X15,X16)|(~r1(X16,X17)|(p5(X17)|p1(X17))))))))))&(~r1(skolem0001,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~r1(X12,X13)|(~r1(X13,X14)|(~r1(X14,X15)|(~r1(X15,X16)|(~r1(X16,X17)|(~p1(X17)|~p5(X17)))))))))))&((~r1(skolem0001,X10)|r1(X10,skolem0009(X10)))&(~r1(skolem0001,X10)|~p6(skolem0009(X10)))))&((((~r1(skolem0001,X10)|(~r1(X10,X19)|(~r1(X19,X20)|(~r1(X20,X21)|(~r1(X21,X22)|(~r1(X22,X23)|(~r1(X23,X24)|(~r1(X24,X25)|(p4(X25)|p5(X25))))))))))&(~r1(skolem0001,X10)|(~r1(X10,X19)|(~r1(X19,X20)|(~r1(X20,X21)|(~r1(X21,X22)|(~r1(X22,X23)|(~r1(X23,X24)|(~r1(X24,X25)|(~p5(X25)|~p4(X25)))))))))))&((~r1(skolem0001,X10)|(~r1(X10,X19)|r1(X19,skolem0010(X10,X19))))&(~r1(skolem0001,X10)|(~r1(X10,X19)|~p5(skolem0010(X10,X19))))))&((((~r1(skolem0001,X10)|(~r1(X10,X19)|(~r1(X19,X27)|(~r1(X27,X28)|(~r1(X28,X29)|(~r1(X29,X30)|(~r1(X30,X31)|(~r1(X31,X32)|(p3(X32)|p4(X32))))))))))&(~r1(skolem0001,X10)|(~r1(X10,X19)|(~r1(X19,X27)|(~r1(X27,X28)|(~r1(X28,X29)|(~r1(X29,X30)|(~r1(X30,X31)|(~r1(X31,X32)|(~p4(X32)|~p3(X32)))))))))))&((~r1(skolem0001,X10)|(~r1(X10,X19)|(~r1(X19,X27)|r1(X27,skolem0011(X10,X19,X27)))))&(~r1(skolem0001,X10)|(~r1(X10,X19)|(~r1(X19,X27)|~p4(skolem0011(X10,X19,X27)))))))&((((~r1(skolem0001,X10)|(~r1(X10,X19)|(~r1(X19,X27)|(~r1(X27,X34)|(~r1(X34,X35)|(~r1(X35,X36)|(~r1(X36,X37)|(~r1(X37,X38)|(p2(X38)|p3(X38))))))))))&(~r1(skolem0001,X10)|(~r1(X10,X19)|(~r1(X19,X27)|(~r1(X27,X34)|(~r1(X34,X35)|(~r1(X35,X36)|(~r1(X36,X37)|(~r1(X37,X38)|(~p3(X38)|~p2(X38)))))))))))&((~r1(skolem0001,X10)|(~r1(X10,X19)|(~r1(X19,X27)|(~r1(X27,X34)|r1(X34,skolem0012(X10,X19,X27,X34))))))&(~r1(skolem0001,X10)|(~r1(X10,X19)|(~r1(X19,X27)|(~r1(X27,X34)|~p3(skolem0012(X10,X19,X27,X34))))))))&((~r1(skolem0001,X10)|(~r1(X10,X19)|(~r1(X19,X27)|(~r1(X27,X34)|(~r1(X34,X40)|(~r1(X40,X41)|(~r1(X41,X42)|(~r1(X42,X43)|(p1(X43)|p2(X43))))))))))&(~r1(skolem0001,X10)|(~r1(X10,X19)|(~r1(X19,X27)|(~r1(X27,X34)|(~r1(X34,X40)|(~r1(X40,X41)|(~r1(X41,X42)|(~r1(X42,X43)|(~p2(X43)|~p1(X43))))))))))))))))&(r1(skolem0001,skolem0013)&(r1(skolem0013,skolem0014)&(r1(skolem0014,skolem0015)&(r1(skolem0015,skolem0016)&(r1(skolem0016,skolem0017)&(r1(skolem0017,skolem0018)&(((((~p6(skolem0018)|~p5(skolem0018))|~p4(skolem0018))|~p3(skolem0018))|~p2(skolem0018))|~p1(skolem0018))))))))))))))))))))))))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 33.55/33.81 cnf(c27,negated_conjecture,~r1(skolem0001,X112)|~r1(X112,X111)|~r1(X111,X113)|~p4(skolem0011(X112,X111,X113)),inference(split_conjunct,[status(thm)],[c6])).
% 33.55/33.81 cnf(c26,negated_conjecture,~r1(skolem0001,X108)|~r1(X108,X107)|~r1(X107,X109)|r1(X109,skolem0011(X108,X107,X109)),inference(split_conjunct,[status(thm)],[c6])).
% 33.55/33.81 cnf(c293,plain,~r1(skolem0001,X110)|~r1(X110,X110)|r1(X110,skolem0011(X110,X110,X110)),inference(factor,[status(thm)],[c26])).
% 33.55/33.81 cnf(c346,plain,~r1(skolem0001,X114)|r1(X114,skolem0011(X114,X114,X114)),inference(resolution,[status(thm)],[c293, c42])).
% 33.55/33.81 cnf(c349,plain,r1(skolem0001,skolem0011(skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c346, c42])).
% 33.55/33.81 cnf(c24,negated_conjecture,~r1(skolem0001,X94)|~r1(X94,X91)|~r1(X91,X97)|~r1(X97,X93)|~r1(X93,X92)|~r1(X92,X96)|~r1(X96,X95)|~r1(X95,X98)|p3(X98)|p4(X98),inference(split_conjunct,[status(thm)],[c6])).
% 33.55/33.81 cnf(c214,plain,~r1(skolem0001,X1239)|~r1(X1239,X1241)|~r1(X1241,X1240)|~r1(X1240,X1244)|~r1(X1244,X1242)|~r1(X1242,X1243)|~r1(X1243,X1240)|p3(X1244)|p4(X1244),inference(factor,[status(thm)],[c24])).
% 33.55/33.81 cnf(c7456,plain,~r1(skolem0001,X2716)|~r1(X2716,X2714)|~r1(X2714,X2713)|~r1(X2713,X2715)|~r1(X2715,X2713)|p3(X2715)|p4(X2715),inference(factor,[status(thm)],[c214])).
% 33.55/33.81 cnf(c14089,plain,~r1(skolem0001,X2718)|~r1(X2718,X2717)|~r1(X2717,X2717)|~r1(X2717,X2718)|p3(X2718)|p4(X2718),inference(factor,[status(thm)],[c7456])).
% 33.55/33.81 cnf(c14230,plain,~r1(skolem0001,X2719)|~r1(X2719,X2719)|p3(X2719)|p4(X2719),inference(factor,[status(thm)],[c14089])).
% 33.55/33.81 cnf(c14371,plain,~r1(skolem0001,X2720)|p3(X2720)|p4(X2720),inference(resolution,[status(thm)],[c14230, c42])).
% 33.55/33.81 cnf(c14372,plain,p3(skolem0011(skolem0001,skolem0001,skolem0001))|p4(skolem0011(skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c14371, c349])).
% 33.55/33.81 cnf(c14410,plain,p3(skolem0011(skolem0001,skolem0001,skolem0001))|~r1(skolem0001,skolem0001),inference(resolution,[status(thm)],[c14372, c27])).
% 33.55/33.81 cnf(c14411,plain,p3(skolem0011(skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c14410, c42])).
% 33.55/33.81 cnf(c29,negated_conjecture,~r1(skolem0001,X129)|~r1(X129,X127)|~r1(X127,X132)|~r1(X132,X130)|~r1(X130,X128)|~r1(X128,X126)|~r1(X126,X131)|~r1(X131,X133)|~p3(X133)|~p2(X133),inference(split_conjunct,[status(thm)],[c6])).
% 33.55/33.81 cnf(c468,plain,~r1(skolem0001,X2760)|~r1(X2760,X2759)|~r1(X2759,X2757)|~r1(X2757,X2758)|~r1(X2758,X2756)|~r1(X2756,X2761)|~r1(X2761,X2757)|~p3(X2758)|~p2(X2758),inference(factor,[status(thm)],[c29])).
% 33.55/33.81 cnf(c15131,plain,~r1(skolem0001,X4549)|~r1(X4549,X4550)|~r1(X4550,X4551)|~r1(X4551,X4548)|~r1(X4548,X4551)|~p3(X4548)|~p2(X4548),inference(factor,[status(thm)],[c468])).
% 33.55/33.81 cnf(c22093,plain,~r1(skolem0001,X4553)|~r1(X4553,X4552)|~r1(X4552,X4552)|~r1(X4552,X4553)|~p3(X4553)|~p2(X4553),inference(factor,[status(thm)],[c15131])).
% 33.55/33.81 cnf(c22244,plain,~r1(skolem0001,X4554)|~r1(X4554,X4554)|~p3(X4554)|~p2(X4554),inference(factor,[status(thm)],[c22093])).
% 33.55/33.81 cnf(c22394,plain,~r1(skolem0001,X4555)|~p3(X4555)|~p2(X4555),inference(resolution,[status(thm)],[c22244, c42])).
% 33.55/33.81 cnf(c22395,plain,~p3(skolem0011(skolem0001,skolem0001,skolem0001))|~p2(skolem0011(skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c22394, c349])).
% 33.55/33.81 cnf(c17,negated_conjecture,~r1(skolem0001,X63)|~r1(X63,X67)|~r1(X67,X64)|~r1(X64,X66)|~r1(X66,X69)|~r1(X69,X62)|~r1(X62,X65)|~r1(X65,X68)|~p1(X68)|~p5(X68),inference(split_conjunct,[status(thm)],[c6])).
% 33.55/33.81 cnf(c76,plain,~r1(skolem0001,X373)|~r1(X373,X375)|~r1(X375,X374)|~r1(X374,X376)|~r1(X376,X377)|~r1(X377,X378)|~r1(X378,X374)|~p1(X376)|~p5(X376),inference(factor,[status(thm)],[c17])).
% 33.55/33.81 cnf(c2290,plain,~r1(skolem0001,X1168)|~r1(X1168,X1169)|~r1(X1169,X1167)|~r1(X1167,X1166)|~r1(X1166,X1167)|~p1(X1166)|~p5(X1166),inference(factor,[status(thm)],[c76])).
% 33.55/33.81 cnf(c6616,plain,~r1(skolem0001,X1177)|~r1(X1177,X1176)|~r1(X1176,X1176)|~r1(X1176,X1177)|~p1(X1177)|~p5(X1177),inference(factor,[status(thm)],[c2290])).
% 33.55/33.81 cnf(c6731,plain,~r1(skolem0001,X1178)|~r1(X1178,X1178)|~p1(X1178)|~p5(X1178),inference(factor,[status(thm)],[c6616])).
% 33.55/33.81 cnf(c6845,plain,~r1(skolem0001,X1179)|~p1(X1179)|~p5(X1179),inference(resolution,[status(thm)],[c6731, c42])).
% 33.55/33.81 cnf(c6846,plain,~p1(skolem0011(skolem0001,skolem0001,skolem0001))|~p5(skolem0011(skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c6845, c349])).
% 33.55/33.81 cnf(c20,negated_conjecture,~r1(skolem0001,X77)|~r1(X77,X75)|~r1(X75,X81)|~r1(X81,X79)|~r1(X79,X80)|~r1(X80,X82)|~r1(X82,X76)|~r1(X76,X78)|p4(X78)|p5(X78),inference(split_conjunct,[status(thm)],[c6])).
% 33.55/33.81 cnf(c131,plain,~r1(skolem0001,X606)|~r1(X606,X607)|~r1(X607,X608)|~r1(X608,X605)|~r1(X605,X604)|~r1(X604,X603)|~r1(X603,X608)|p4(X605)|p5(X605),inference(factor,[status(thm)],[c20])).
% 33.55/33.81 cnf(c4182,plain,~r1(skolem0001,X1670)|~r1(X1670,X1671)|~r1(X1671,X1673)|~r1(X1673,X1672)|~r1(X1672,X1673)|p4(X1672)|p5(X1672),inference(factor,[status(thm)],[c131])).
% 33.55/33.81 cnf(c9081,plain,~r1(skolem0001,X1675)|~r1(X1675,X1674)|~r1(X1674,X1674)|~r1(X1674,X1675)|p4(X1675)|p5(X1675),inference(factor,[status(thm)],[c4182])).
% 33.55/33.81 cnf(c9196,plain,~r1(skolem0001,X1676)|~r1(X1676,X1676)|p4(X1676)|p5(X1676),inference(factor,[status(thm)],[c9081])).
% 33.55/33.81 cnf(c9310,plain,~r1(skolem0001,X1677)|p4(X1677)|p5(X1677),inference(resolution,[status(thm)],[c9196, c42])).
% 33.55/33.81 cnf(c9311,plain,p4(skolem0011(skolem0001,skolem0001,skolem0001))|p5(skolem0011(skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c9310, c349])).
% 33.55/33.81 cnf(c9351,plain,p5(skolem0011(skolem0001,skolem0001,skolem0001))|~r1(skolem0001,skolem0001),inference(resolution,[status(thm)],[c9311, c27])).
% 33.55/33.81 cnf(c9353,plain,p5(skolem0011(skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c9351, c42])).
% 33.55/33.81 cnf(c9354,plain,~p1(skolem0011(skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c9353, c6846])).
% 33.55/33.81 cnf(c32,negated_conjecture,~r1(skolem0001,X143)|~r1(X143,X142)|~r1(X142,X149)|~r1(X149,X144)|~r1(X144,X147)|~r1(X147,X146)|~r1(X146,X148)|~r1(X148,X145)|p1(X145)|p2(X145),inference(split_conjunct,[status(thm)],[c6])).
% 33.55/33.81 cnf(c598,plain,~r1(skolem0001,X3511)|~r1(X3511,X3515)|~r1(X3515,X3512)|~r1(X3512,X3516)|~r1(X3516,X3513)|~r1(X3513,X3514)|~r1(X3514,X3512)|p1(X3516)|p2(X3516),inference(factor,[status(thm)],[c32])).
% 33.55/33.81 cnf(c18320,plain,~r1(skolem0001,X5135)|~r1(X5135,X5136)|~r1(X5136,X5134)|~r1(X5134,X5137)|~r1(X5137,X5134)|p1(X5137)|p2(X5137),inference(factor,[status(thm)],[c598])).
% 33.55/33.81 cnf(c24324,plain,~r1(skolem0001,X5139)|~r1(X5139,X5138)|~r1(X5138,X5138)|~r1(X5138,X5139)|p1(X5139)|p2(X5139),inference(factor,[status(thm)],[c18320])).
% 33.55/33.81 cnf(c24484,plain,~r1(skolem0001,X5140)|~r1(X5140,X5140)|p1(X5140)|p2(X5140),inference(factor,[status(thm)],[c24324])).
% 33.55/33.81 cnf(c24643,plain,~r1(skolem0001,X5147)|p1(X5147)|p2(X5147),inference(resolution,[status(thm)],[c24484, c42])).
% 33.55/33.81 cnf(c24644,plain,p1(skolem0011(skolem0001,skolem0001,skolem0001))|p2(skolem0011(skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c24643, c349])).
% 33.55/33.81 cnf(c24732,plain,p2(skolem0011(skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c24644, c9354])).
% 33.55/33.81 cnf(c24734,plain,~p3(skolem0011(skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c24732, c22395])).
% 33.55/33.81 cnf(c24735,plain,$false,inference(resolution,[status(thm)],[c24734, c14411])).
% 33.55/33.81 % SZS output end CNFRefutation
% 33.55/33.81
% 33.55/33.81 % Initial clauses : 35
% 33.55/33.81 % Processed clauses : 2392
% 33.55/33.81 % Factors computed : 2546
% 33.55/33.81 % Resolvents computed: 22147
% 33.55/33.81 % Tautologies deleted: 105
% 33.55/33.81 % Forward subsumed : 1550
% 33.55/33.81 % Backward subsumed : 944
% 33.55/33.81 % -------- CPU Time ---------
% 33.55/33.81 % User time : 33.334 s
% 33.55/33.81 % System time : 0.114 s
% 33.55/33.81 % Total time : 33.448 s
%------------------------------------------------------------------------------