%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LCL656+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:54 PM UTC 2026
% Result : Theorem 6.37s 6.69s
% Output : CNFRefutation 6.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL656+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.36 % Computer : n027.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 17:28:13 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.09/0.43 (re.compile("\."), Token.FullStop),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.09/0.43 (re.compile("\("), Token.OpenPar),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.09/0.43 (re.compile("\)"), Token.ClosePar),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.09/0.43 (re.compile("\["), Token.OpenSquare),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.09/0.43 (re.compile("\]"), Token.CloseSquare),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("~\|"), Token.Nor),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.09/0.43 (re.compile("\|"), Token.Or),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.09/0.43 (re.compile("\?"), Token.Existential),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.09/0.43 (re.compile("\s+"), Token.WhiteSpace),
% 0.09/0.43 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.09/0.43 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.50 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.50 """
% 0.23/0.50 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.50 """
% 0.35/0.59 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.35/0.59 """
% 6.37/6.69 % Version: 1.5
% 6.37/6.69 % SZS status Theorem
% 6.37/6.69 % SZS output start CNFRefutation
% 6.37/6.69 fof(main,conjecture,(~(?[X]:(~((~(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|(![X]:((~r1(Y,X))|(![Y]:((~r1(X,Y))|p3(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))|(~(((~p6(X))&(~p106(X)))&p105(X))))))&(~(![X]:((~r1(Y,X))|(~((p6(X)&(~p106(X)))&p105(X)))))))|(~((~p105(Y))&p104(Y))))&(((~(![X]:((~r1(Y,X))|(~(((~p5(X))&(~p105(X)))&p104(X))))))&(~(![X]:((~r1(Y,X))|(~((p5(X)&(~p105(X)))&p104(X)))))))|(~((~p104(Y))&p103(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p4(X))&(~p104(X)))&p103(X))))))&(~(![X]:((~r1(Y,X))|(~((p4(X)&(~p104(X)))&p103(X)))))))|(~((~p103(Y))&p102(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p3(X))&(~p103(X)))&p102(X))))))&(~(![X]:((~r1(Y,X))|(~((p3(X)&(~p103(X)))&p102(X)))))))|(~((~p102(Y))&p101(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p2(X))&(~p102(X)))&p101(X))))))&(~(![X]:((~r1(Y,X))|(~((p2(X)&(~p102(X)))&p101(X)))))))|(~((~p101(Y))&p100(Y)))))&((((![X]:(((~r1(Y,X))|(~p6(X)))|(~p105(X))))|p6(Y))&((![X]:(((~r1(Y,X))|p6(X))|(~p105(X))))|(~p6(Y))))|(~p105(Y))))&((((![X]:(((~r1(Y,X))|(~p5(X)))|(~p104(X))))|p5(Y))&((![X]:(((~r1(Y,X))|p5(X))|(~p104(X))))|(~p5(Y))))|(~p104(Y))))&((((![X]:(((~r1(Y,X))|(~p4(X)))|(~p103(X))))|p4(Y))&((![X]:(((~r1(Y,X))|p4(X))|(~p103(X))))|(~p4(Y))))|(~p103(Y))))&((((![X]:(((~r1(Y,X))|(~p3(X)))|(~p102(X))))|p3(Y))&((![X]:(((~r1(Y,X))|p3(X))|(~p102(X))))|(~p3(Y))))|(~p102(Y))))&((((![X]:(((~r1(Y,X))|(~p2(X)))|(~p101(X))))|p2(Y))&((![X]:(((~r1(Y,X))|p2(X))|(~p101(X))))|(~p2(Y))))|(~p101(Y))))&((((![X]:(((~r1(Y,X))|(~p1(X)))|(~p100(X))))|p1(Y))&((![X]:(((~r1(Y,X))|p1(X))|(~p100(X))))|(~p1(Y))))|(~p100(Y))))&(p105(Y)|(~p106(Y))))&(p104(Y)|(~p105(Y))))&(p103(Y)|(~p104(Y))))&(p102(Y)|(~p103(Y))))&(p101(Y)|(~p102(Y))))&(p100(Y)|(~p101(Y))))))))))))))&(~p101(X)))&p100(X))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 6.37/6.69 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))|p3(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))|(~(((~p6(X))&(~p106(X)))&p105(X))))))&(~(![X]:((~r1(Y,X))|(~((p6(X)&(~p106(X)))&p105(X)))))))|(~((~p105(Y))&p104(Y))))&(((~(![X]:((~r1(Y,X))|(~(((~p5(X))&(~p105(X)))&p104(X))))))&(~(![X]:((~r1(Y,X))|(~((p5(X)&(~p105(X)))&p104(X)))))))|(~((~p104(Y))&p103(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p4(X))&(~p104(X)))&p103(X))))))&(~(![X]:((~r1(Y,X))|(~((p4(X)&(~p104(X)))&p103(X)))))))|(~((~p103(Y))&p102(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p3(X))&(~p103(X)))&p102(X))))))&(~(![X]:((~r1(Y,X))|(~((p3(X)&(~p103(X)))&p102(X)))))))|(~((~p102(Y))&p101(Y)))))&(((~(![X]:((~r1(Y,X))|(~(((~p2(X))&(~p102(X)))&p101(X))))))&(~(![X]:((~r1(Y,X))|(~((p2(X)&(~p102(X)))&p101(X)))))))|(~((~p101(Y))&p100(Y)))))&((((![X]:(((~r1(Y,X))|(~p6(X)))|(~p105(X))))|p6(Y))&((![X]:(((~r1(Y,X))|p6(X))|(~p105(X))))|(~p6(Y))))|(~p105(Y))))&((((![X]:(((~r1(Y,X))|(~p5(X)))|(~p104(X))))|p5(Y))&((![X]:(((~r1(Y,X))|p5(X))|(~p104(X))))|(~p5(Y))))|(~p104(Y))))&((((![X]:(((~r1(Y,X))|(~p4(X)))|(~p103(X))))|p4(Y))&((![X]:(((~r1(Y,X))|p4(X))|(~p103(X))))|(~p4(Y))))|(~p103(Y))))&((((![X]:(((~r1(Y,X))|(~p3(X)))|(~p102(X))))|p3(Y))&((![X]:(((~r1(Y,X))|p3(X))|(~p102(X))))|(~p3(Y))))|(~p102(Y))))&((((![X]:(((~r1(Y,X))|(~p2(X)))|(~p101(X))))|p2(Y))&((![X]:(((~r1(Y,X))|p2(X))|(~p101(X))))|(~p2(Y))))|(~p101(Y))))&((((![X]:(((~r1(Y,X))|(~p1(X)))|(~p100(X))))|p1(Y))&((![X]:(((~r1(Y,X))|p1(X))|(~p100(X))))|(~p1(Y))))|(~p100(Y))))&(p105(Y)|(~p106(Y))))&(p104(Y)|(~p105(Y))))&(p103(Y)|(~p104(Y))))&(p102(Y)|(~p103(Y))))&(p101(Y)|(~p102(Y))))&(p100(Y)|(~p101(Y))))))))))))))&(~p101(X)))&p100(X)))))))),inference(assume_negation,[status(cth)],[main])).
% 6.37/6.69 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)|p3(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)|(~((~p6(X)&~p106(X))&p105(X))))))&(~(![X]:(~r1(Y,X)|(~((p6(X)&~p106(X))&p105(X)))))))|(~(~p105(Y)&p104(Y))))&(((~(![X]:(~r1(Y,X)|(~((~p5(X)&~p105(X))&p104(X))))))&(~(![X]:(~r1(Y,X)|(~((p5(X)&~p105(X))&p104(X)))))))|(~(~p104(Y)&p103(Y)))))&(((~(![X]:(~r1(Y,X)|(~((~p4(X)&~p104(X))&p103(X))))))&(~(![X]:(~r1(Y,X)|(~((p4(X)&~p104(X))&p103(X)))))))|(~(~p103(Y)&p102(Y)))))&(((~(![X]:(~r1(Y,X)|(~((~p3(X)&~p103(X))&p102(X))))))&(~(![X]:(~r1(Y,X)|(~((p3(X)&~p103(X))&p102(X)))))))|(~(~p102(Y)&p101(Y)))))&(((~(![X]:(~r1(Y,X)|(~((~p2(X)&~p102(X))&p101(X))))))&(~(![X]:(~r1(Y,X)|(~((p2(X)&~p102(X))&p101(X)))))))|(~(~p101(Y)&p100(Y)))))&((((![X]:((~r1(Y,X)|~p6(X))|~p105(X)))|p6(Y))&((![X]:((~r1(Y,X)|p6(X))|~p105(X)))|~p6(Y)))|~p105(Y)))&((((![X]:((~r1(Y,X)|~p5(X))|~p104(X)))|p5(Y))&((![X]:((~r1(Y,X)|p5(X))|~p104(X)))|~p5(Y)))|~p104(Y)))&((((![X]:((~r1(Y,X)|~p4(X))|~p103(X)))|p4(Y))&((![X]:((~r1(Y,X)|p4(X))|~p103(X)))|~p4(Y)))|~p103(Y)))&((((![X]:((~r1(Y,X)|~p3(X))|~p102(X)))|p3(Y))&((![X]:((~r1(Y,X)|p3(X))|~p102(X)))|~p3(Y)))|~p102(Y)))&((((![X]:((~r1(Y,X)|~p2(X))|~p101(X)))|p2(Y))&((![X]:((~r1(Y,X)|p2(X))|~p101(X)))|~p2(Y)))|~p101(Y)))&((((![X]:((~r1(Y,X)|~p1(X))|~p100(X)))|p1(Y))&((![X]:((~r1(Y,X)|p1(X))|~p100(X)))|~p1(Y)))|~p100(Y)))&(p105(Y)|~p106(Y)))&(p104(Y)|~p105(Y)))&(p103(Y)|~p104(Y)))&(p102(Y)|~p103(Y)))&(p101(Y)|~p102(Y)))&(p100(Y)|~p101(Y)))))))))))))&~p101(X))&p100(X)))))))),inference(fof_simplification,[status(thm)],[c0])).
% 6.37/6.69 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)|p3(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)&((~p6(X)&~p106(X))&p105(X))))&(?[X]:(r1(Y,X)&((p6(X)&~p106(X))&p105(X)))))|(p105(Y)|~p104(Y)))&(((?[X]:(r1(Y,X)&((~p5(X)&~p105(X))&p104(X))))&(?[X]:(r1(Y,X)&((p5(X)&~p105(X))&p104(X)))))|(p104(Y)|~p103(Y))))&(((?[X]:(r1(Y,X)&((~p4(X)&~p104(X))&p103(X))))&(?[X]:(r1(Y,X)&((p4(X)&~p104(X))&p103(X)))))|(p103(Y)|~p102(Y))))&(((?[X]:(r1(Y,X)&((~p3(X)&~p103(X))&p102(X))))&(?[X]:(r1(Y,X)&((p3(X)&~p103(X))&p102(X)))))|(p102(Y)|~p101(Y))))&(((?[X]:(r1(Y,X)&((~p2(X)&~p102(X))&p101(X))))&(?[X]:(r1(Y,X)&((p2(X)&~p102(X))&p101(X)))))|(p101(Y)|~p100(Y))))&((((![X]:((~r1(Y,X)|~p6(X))|~p105(X)))|p6(Y))&((![X]:((~r1(Y,X)|p6(X))|~p105(X)))|~p6(Y)))|~p105(Y)))&((((![X]:((~r1(Y,X)|~p5(X))|~p104(X)))|p5(Y))&((![X]:((~r1(Y,X)|p5(X))|~p104(X)))|~p5(Y)))|~p104(Y)))&((((![X]:((~r1(Y,X)|~p4(X))|~p103(X)))|p4(Y))&((![X]:((~r1(Y,X)|p4(X))|~p103(X)))|~p4(Y)))|~p103(Y)))&((((![X]:((~r1(Y,X)|~p3(X))|~p102(X)))|p3(Y))&((![X]:((~r1(Y,X)|p3(X))|~p102(X)))|~p3(Y)))|~p102(Y)))&((((![X]:((~r1(Y,X)|~p2(X))|~p101(X)))|p2(Y))&((![X]:((~r1(Y,X)|p2(X))|~p101(X)))|~p2(Y)))|~p101(Y)))&((((![X]:((~r1(Y,X)|~p1(X))|~p100(X)))|p1(Y))&((![X]:((~r1(Y,X)|p1(X))|~p100(X)))|~p1(Y)))|~p100(Y)))&(p105(Y)|~p106(Y)))&(p104(Y)|~p105(Y)))&(p103(Y)|~p104(Y)))&(p102(Y)|~p103(Y)))&(p101(Y)|~p102(Y)))&(p100(Y)|~p101(Y)))))))))))))&~p101(X))&p100(X)))),inference(fof_nnf,[status(thm)],[c1])).
% 6.37/6.70 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)|p3(X7)))))))))))&(((![X8]:(~r1(X2,X8)|(![X9]:(~r1(X8,X9)|(![X10]:(~r1(X9,X10)|(![X11]:(~r1(X10,X11)|(![X12]:(~r1(X11,X12)|(((((((((((((((((((?[X13]:(r1(X12,X13)&((~p6(X13)&~p106(X13))&p105(X13))))&(?[X14]:(r1(X12,X14)&((p6(X14)&~p106(X14))&p105(X14)))))|(p105(X12)|~p104(X12)))&(((?[X15]:(r1(X12,X15)&((~p5(X15)&~p105(X15))&p104(X15))))&(?[X16]:(r1(X12,X16)&((p5(X16)&~p105(X16))&p104(X16)))))|(p104(X12)|~p103(X12))))&(((?[X17]:(r1(X12,X17)&((~p4(X17)&~p104(X17))&p103(X17))))&(?[X18]:(r1(X12,X18)&((p4(X18)&~p104(X18))&p103(X18)))))|(p103(X12)|~p102(X12))))&(((?[X19]:(r1(X12,X19)&((~p3(X19)&~p103(X19))&p102(X19))))&(?[X20]:(r1(X12,X20)&((p3(X20)&~p103(X20))&p102(X20)))))|(p102(X12)|~p101(X12))))&(((?[X21]:(r1(X12,X21)&((~p2(X21)&~p102(X21))&p101(X21))))&(?[X22]:(r1(X12,X22)&((p2(X22)&~p102(X22))&p101(X22)))))|(p101(X12)|~p100(X12))))&((((![X23]:((~r1(X12,X23)|~p6(X23))|~p105(X23)))|p6(X12))&((![X24]:((~r1(X12,X24)|p6(X24))|~p105(X24)))|~p6(X12)))|~p105(X12)))&((((![X25]:((~r1(X12,X25)|~p5(X25))|~p104(X25)))|p5(X12))&((![X26]:((~r1(X12,X26)|p5(X26))|~p104(X26)))|~p5(X12)))|~p104(X12)))&((((![X27]:((~r1(X12,X27)|~p4(X27))|~p103(X27)))|p4(X12))&((![X28]:((~r1(X12,X28)|p4(X28))|~p103(X28)))|~p4(X12)))|~p103(X12)))&((((![X29]:((~r1(X12,X29)|~p3(X29))|~p102(X29)))|p3(X12))&((![X30]:((~r1(X12,X30)|p3(X30))|~p102(X30)))|~p3(X12)))|~p102(X12)))&((((![X31]:((~r1(X12,X31)|~p2(X31))|~p101(X31)))|p2(X12))&((![X32]:((~r1(X12,X32)|p2(X32))|~p101(X32)))|~p2(X12)))|~p101(X12)))&((((![X33]:((~r1(X12,X33)|~p1(X33))|~p100(X33)))|p1(X12))&((![X34]:((~r1(X12,X34)|p1(X34))|~p100(X34)))|~p1(X12)))|~p100(X12)))&(p105(X12)|~p106(X12)))&(p104(X12)|~p105(X12)))&(p103(X12)|~p104(X12)))&(p102(X12)|~p103(X12)))&(p101(X12)|~p102(X12)))&(p100(X12)|~p101(X12)))))))))))))&~p101(X2))&p100(X2)))),inference(variable_rename,[status(thm)],[c2])).
% 6.37/6.70 fof(c5,negated_conjecture,(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:((~r1(skolem0001,X3)|(~r1(X3,X4)|(~r1(X4,X5)|(~r1(X5,X6)|(~r1(X6,X7)|p3(X7))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(((((((((((((((((((r1(X12,skolem0002(X8,X9,X10,X11,X12))&((~p6(skolem0002(X8,X9,X10,X11,X12))&~p106(skolem0002(X8,X9,X10,X11,X12)))&p105(skolem0002(X8,X9,X10,X11,X12))))&(r1(X12,skolem0003(X8,X9,X10,X11,X12))&((p6(skolem0003(X8,X9,X10,X11,X12))&~p106(skolem0003(X8,X9,X10,X11,X12)))&p105(skolem0003(X8,X9,X10,X11,X12)))))|(p105(X12)|~p104(X12)))&(((r1(X12,skolem0004(X8,X9,X10,X11,X12))&((~p5(skolem0004(X8,X9,X10,X11,X12))&~p105(skolem0004(X8,X9,X10,X11,X12)))&p104(skolem0004(X8,X9,X10,X11,X12))))&(r1(X12,skolem0005(X8,X9,X10,X11,X12))&((p5(skolem0005(X8,X9,X10,X11,X12))&~p105(skolem0005(X8,X9,X10,X11,X12)))&p104(skolem0005(X8,X9,X10,X11,X12)))))|(p104(X12)|~p103(X12))))&(((r1(X12,skolem0006(X8,X9,X10,X11,X12))&((~p4(skolem0006(X8,X9,X10,X11,X12))&~p104(skolem0006(X8,X9,X10,X11,X12)))&p103(skolem0006(X8,X9,X10,X11,X12))))&(r1(X12,skolem0007(X8,X9,X10,X11,X12))&((p4(skolem0007(X8,X9,X10,X11,X12))&~p104(skolem0007(X8,X9,X10,X11,X12)))&p103(skolem0007(X8,X9,X10,X11,X12)))))|(p103(X12)|~p102(X12))))&(((r1(X12,skolem0008(X8,X9,X10,X11,X12))&((~p3(skolem0008(X8,X9,X10,X11,X12))&~p103(skolem0008(X8,X9,X10,X11,X12)))&p102(skolem0008(X8,X9,X10,X11,X12))))&(r1(X12,skolem0009(X8,X9,X10,X11,X12))&((p3(skolem0009(X8,X9,X10,X11,X12))&~p103(skolem0009(X8,X9,X10,X11,X12)))&p102(skolem0009(X8,X9,X10,X11,X12)))))|(p102(X12)|~p101(X12))))&(((r1(X12,skolem0010(X8,X9,X10,X11,X12))&((~p2(skolem0010(X8,X9,X10,X11,X12))&~p102(skolem0010(X8,X9,X10,X11,X12)))&p101(skolem0010(X8,X9,X10,X11,X12))))&(r1(X12,skolem0011(X8,X9,X10,X11,X12))&((p2(skolem0011(X8,X9,X10,X11,X12))&~p102(skolem0011(X8,X9,X10,X11,X12)))&p101(skolem0011(X8,X9,X10,X11,X12)))))|(p101(X12)|~p100(X12))))&(((((~r1(X12,X23)|~p6(X23))|~p105(X23))|p6(X12))&(((~r1(X12,X24)|p6(X24))|~p105(X24))|~p6(X12)))|~p105(X12)))&(((((~r1(X12,X25)|~p5(X25))|~p104(X25))|p5(X12))&(((~r1(X12,X26)|p5(X26))|~p104(X26))|~p5(X12)))|~p104(X12)))&(((((~r1(X12,X27)|~p4(X27))|~p103(X27))|p4(X12))&(((~r1(X12,X28)|p4(X28))|~p103(X28))|~p4(X12)))|~p103(X12)))&(((((~r1(X12,X29)|~p3(X29))|~p102(X29))|p3(X12))&(((~r1(X12,X30)|p3(X30))|~p102(X30))|~p3(X12)))|~p102(X12)))&(((((~r1(X12,X31)|~p2(X31))|~p101(X31))|p2(X12))&(((~r1(X12,X32)|p2(X32))|~p101(X32))|~p2(X12)))|~p101(X12)))&(((((~r1(X12,X33)|~p1(X33))|~p100(X33))|p1(X12))&(((~r1(X12,X34)|p1(X34))|~p100(X34))|~p1(X12)))|~p100(X12)))&(p105(X12)|~p106(X12)))&(p104(X12)|~p105(X12)))&(p103(X12)|~p104(X12)))&(p102(X12)|~p103(X12)))&(p101(X12)|~p102(X12)))&(p100(X12)|~p101(X12))))))))&~p101(skolem0001))&p100(skolem0001))))))))))))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,((![X3]:(~r1(skolem0001,X3)|(![X4]:(~r1(X3,X4)|(![X5]:(~r1(X4,X5)|(![X6]:(~r1(X5,X6)|(![X7]:(~r1(X6,X7)|p3(X7)))))))))))&(((![X8]:(~r1(skolem0001,X8)|(![X9]:(~r1(X8,X9)|(![X10]:(~r1(X9,X10)|(![X11]:(~r1(X10,X11)|(![X12]:(~r1(X11,X12)|(((((((((((((((((((r1(X12,skolem0002(X8,X9,X10,X11,X12))&((~p6(skolem0002(X8,X9,X10,X11,X12))&~p106(skolem0002(X8,X9,X10,X11,X12)))&p105(skolem0002(X8,X9,X10,X11,X12))))&(r1(X12,skolem0003(X8,X9,X10,X11,X12))&((p6(skolem0003(X8,X9,X10,X11,X12))&~p106(skolem0003(X8,X9,X10,X11,X12)))&p105(skolem0003(X8,X9,X10,X11,X12)))))|(p105(X12)|~p104(X12)))&(((r1(X12,skolem0004(X8,X9,X10,X11,X12))&((~p5(skolem0004(X8,X9,X10,X11,X12))&~p105(skolem0004(X8,X9,X10,X11,X12)))&p104(skolem0004(X8,X9,X10,X11,X12))))&(r1(X12,skolem0005(X8,X9,X10,X11,X12))&((p5(skolem0005(X8,X9,X10,X11,X12))&~p105(skolem0005(X8,X9,X10,X11,X12)))&p104(skolem0005(X8,X9,X10,X11,X12)))))|(p104(X12)|~p103(X12))))&(((r1(X12,skolem0006(X8,X9,X10,X11,X12))&((~p4(skolem0006(X8,X9,X10,X11,X12))&~p104(skolem0006(X8,X9,X10,X11,X12)))&p103(skolem0006(X8,X9,X10,X11,X12))))&(r1(X12,skolem0007(X8,X9,X10,X11,X12))&((p4(skolem0007(X8,X9,X10,X11,X12))&~p104(skolem0007(X8,X9,X10,X11,X12)))&p103(skolem0007(X8,X9,X10,X11,X12)))))|(p103(X12)|~p102(X12))))&(((r1(X12,skolem0008(X8,X9,X10,X11,X12))&((~p3(skolem0008(X8,X9,X10,X11,X12))&~p103(skolem0008(X8,X9,X10,X11,X12)))&p102(skolem0008(X8,X9,X10,X11,X12))))&(r1(X12,skolem0009(X8,X9,X10,X11,X12))&((p3(skolem0009(X8,X9,X10,X11,X12))&~p103(skolem0009(X8,X9,X10,X11,X12)))&p102(skolem0009(X8,X9,X10,X11,X12)))))|(p102(X12)|~p101(X12))))&(((r1(X12,skolem0010(X8,X9,X10,X11,X12))&((~p2(skolem0010(X8,X9,X10,X11,X12))&~p102(skolem0010(X8,X9,X10,X11,X12)))&p101(skolem0010(X8,X9,X10,X11,X12))))&(r1(X12,skolem0011(X8,X9,X10,X11,X12))&((p2(skolem0011(X8,X9,X10,X11,X12))&~p102(skolem0011(X8,X9,X10,X11,X12)))&p101(skolem0011(X8,X9,X10,X11,X12)))))|(p101(X12)|~p100(X12))))&((((![X23]:((~r1(X12,X23)|~p6(X23))|~p105(X23)))|p6(X12))&((![X24]:((~r1(X12,X24)|p6(X24))|~p105(X24)))|~p6(X12)))|~p105(X12)))&((((![X25]:((~r1(X12,X25)|~p5(X25))|~p104(X25)))|p5(X12))&((![X26]:((~r1(X12,X26)|p5(X26))|~p104(X26)))|~p5(X12)))|~p104(X12)))&((((![X27]:((~r1(X12,X27)|~p4(X27))|~p103(X27)))|p4(X12))&((![X28]:((~r1(X12,X28)|p4(X28))|~p103(X28)))|~p4(X12)))|~p103(X12)))&((((![X29]:((~r1(X12,X29)|~p3(X29))|~p102(X29)))|p3(X12))&((![X30]:((~r1(X12,X30)|p3(X30))|~p102(X30)))|~p3(X12)))|~p102(X12)))&((((![X31]:((~r1(X12,X31)|~p2(X31))|~p101(X31)))|p2(X12))&((![X32]:((~r1(X12,X32)|p2(X32))|~p101(X32)))|~p2(X12)))|~p101(X12)))&((((![X33]:((~r1(X12,X33)|~p1(X33))|~p100(X33)))|p1(X12))&((![X34]:((~r1(X12,X34)|p1(X34))|~p100(X34)))|~p1(X12)))|~p100(X12)))&(p105(X12)|~p106(X12)))&(p104(X12)|~p105(X12)))&(p103(X12)|~p104(X12)))&(p102(X12)|~p103(X12)))&(p101(X12)|~p102(X12)))&(p100(X12)|~p101(X12)))))))))))))&~p101(skolem0001))&p100(skolem0001))),inference(skolemize,[status(esa)],[c3])).])).
% 6.37/6.70 fof(c6,negated_conjecture,(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:((~r1(skolem0001,X3)|(~r1(X3,X4)|(~r1(X4,X5)|(~r1(X5,X6)|(~r1(X6,X7)|p3(X7))))))&(((((((((((((((((((((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(r1(X12,skolem0002(X8,X9,X10,X11,X12))|(p105(X12)|~p104(X12))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p6(skolem0002(X8,X9,X10,X11,X12))|(p105(X12)|~p104(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p106(skolem0002(X8,X9,X10,X11,X12))|(p105(X12)|~p104(X12)))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p105(skolem0002(X8,X9,X10,X11,X12))|(p105(X12)|~p104(X12))))))))))&((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(r1(X12,skolem0003(X8,X9,X10,X11,X12))|(p105(X12)|~p104(X12))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p6(skolem0003(X8,X9,X10,X11,X12))|(p105(X12)|~p104(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p106(skolem0003(X8,X9,X10,X11,X12))|(p105(X12)|~p104(X12)))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p105(skolem0003(X8,X9,X10,X11,X12))|(p105(X12)|~p104(X12)))))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(r1(X12,skolem0004(X8,X9,X10,X11,X12))|(p104(X12)|~p103(X12))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p5(skolem0004(X8,X9,X10,X11,X12))|(p104(X12)|~p103(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p105(skolem0004(X8,X9,X10,X11,X12))|(p104(X12)|~p103(X12)))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p104(skolem0004(X8,X9,X10,X11,X12))|(p104(X12)|~p103(X12))))))))))&((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(r1(X12,skolem0005(X8,X9,X10,X11,X12))|(p104(X12)|~p103(X12))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p5(skolem0005(X8,X9,X10,X11,X12))|(p104(X12)|~p103(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p105(skolem0005(X8,X9,X10,X11,X12))|(p104(X12)|~p103(X12)))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p104(skolem0005(X8,X9,X10,X11,X12))|(p104(X12)|~p103(X12))))))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(r1(X12,skolem0006(X8,X9,X10,X11,X12))|(p103(X12)|~p102(X12))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p4(skolem0006(X8,X9,X10,X11,X12))|(p103(X12)|~p102(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p104(skolem0006(X8,X9,X10,X11,X12))|(p103(X12)|~p102(X12)))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p103(skolem0006(X8,X9,X10,X11,X12))|(p103(X12)|~p102(X12))))))))))&((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(r1(X12,skolem0007(X8,X9,X10,X11,X12))|(p103(X12)|~p102(X12))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p4(skolem0007(X8,X9,X10,X11,X12))|(p103(X12)|~p102(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p104(skolem0007(X8,X9,X10,X11,X12))|(p103(X12)|~p102(X12)))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p103(skolem0007(X8,X9,X10,X11,X12))|(p103(X12)|~p102(X12))))))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(r1(X12,skolem0008(X8,X9,X10,X11,X12))|(p102(X12)|~p101(X12))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p3(skolem0008(X8,X9,X10,X11,X12))|(p102(X12)|~p101(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p103(skolem0008(X8,X9,X10,X11,X12))|(p102(X12)|~p101(X12)))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p102(skolem0008(X8,X9,X10,X11,X12))|(p102(X12)|~p101(X12))))))))))&((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(r1(X12,skolem0009(X8,X9,X10,X11,X12))|(p102(X12)|~p101(X12))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p3(skolem0009(X8,X9,X10,X11,X12))|(p102(X12)|~p101(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p103(skolem0009(X8,X9,X10,X11,X12))|(p102(X12)|~p101(X12)))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p102(skolem0009(X8,X9,X10,X11,X12))|(p102(X12)|~p101(X12))))))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(r1(X12,skolem0010(X8,X9,X10,X11,X12))|(p101(X12)|~p100(X12))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p2(skolem0010(X8,X9,X10,X11,X12))|(p101(X12)|~p100(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p102(skolem0010(X8,X9,X10,X11,X12))|(p101(X12)|~p100(X12)))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p101(skolem0010(X8,X9,X10,X11,X12))|(p101(X12)|~p100(X12))))))))))&((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(r1(X12,skolem0011(X8,X9,X10,X11,X12))|(p101(X12)|~p100(X12))))))))&(((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p2(skolem0011(X8,X9,X10,X11,X12))|(p101(X12)|~p100(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~p102(skolem0011(X8,X9,X10,X11,X12))|(p101(X12)|~p100(X12)))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p101(skolem0011(X8,X9,X10,X11,X12))|(p101(X12)|~p100(X12))))))))))))&((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|((((~r1(X12,X23)|~p6(X23))|~p105(X23))|p6(X12))|~p105(X12)))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|((((~r1(X12,X24)|p6(X24))|~p105(X24))|~p6(X12))|~p105(X12)))))))))&((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|((((~r1(X12,X25)|~p5(X25))|~p104(X25))|p5(X12))|~p104(X12)))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|((((~r1(X12,X26)|p5(X26))|~p104(X26))|~p5(X12))|~p104(X12)))))))))&((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|((((~r1(X12,X27)|~p4(X27))|~p103(X27))|p4(X12))|~p103(X12)))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|((((~r1(X12,X28)|p4(X28))|~p103(X28))|~p4(X12))|~p103(X12)))))))))&((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|((((~r1(X12,X29)|~p3(X29))|~p102(X29))|p3(X12))|~p102(X12)))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|((((~r1(X12,X30)|p3(X30))|~p102(X30))|~p3(X12))|~p102(X12)))))))))&((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|((((~r1(X12,X31)|~p2(X31))|~p101(X31))|p2(X12))|~p101(X12)))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|((((~r1(X12,X32)|p2(X32))|~p101(X32))|~p2(X12))|~p101(X12)))))))))&((~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|((((~r1(X12,X33)|~p1(X33))|~p100(X33))|p1(X12))|~p100(X12)))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|((((~r1(X12,X34)|p1(X34))|~p100(X34))|~p1(X12))|~p100(X12)))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p105(X12)|~p106(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p104(X12)|~p105(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p103(X12)|~p104(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p102(X12)|~p103(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p101(X12)|~p102(X12))))))))&(~r1(skolem0001,X8)|(~r1(X8,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(p100(X12)|~p101(X12))))))))&~p101(skolem0001))&p100(skolem0001))))))))))))))))))))))))),inference(distribute,[status(thm)],[c5])).
% 6.47/6.70 cnf(c66,negated_conjecture,~p101(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 6.47/6.70 cnf(c67,negated_conjecture,p100(skolem0001),inference(split_conjunct,[status(thm)],[c6])).
% 6.47/6.70 fof(reflexivity,axiom,(![X]:r1(X,X)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity)).
% 6.47/6.70 fof(c68,plain,(![X35]:r1(X35,X35)),inference(variable_rename,[status(thm)],[reflexivity])).
% 6.47/6.70 cnf(c69,plain,r1(X36,X36),inference(split_conjunct,[status(thm)],[c68])).
% 6.47/6.70 cnf(c42,negated_conjecture,~r1(skolem0001,X482)|~r1(X482,X481)|~r1(X481,X483)|~r1(X483,X485)|~r1(X485,X484)|~p102(skolem0010(X482,X481,X483,X485,X484))|p101(X484)|~p100(X484),inference(split_conjunct,[status(thm)],[c6])).
% 6.47/6.70 cnf(c43,negated_conjecture,~r1(skolem0001,X494)|~r1(X494,X493)|~r1(X493,X495)|~r1(X495,X497)|~r1(X497,X496)|p101(skolem0010(X494,X493,X495,X497,X496))|p101(X496)|~p100(X496),inference(split_conjunct,[status(thm)],[c6])).
% 6.47/6.70 cnf(c355,plain,~r1(skolem0001,X1669)|~r1(X1669,X1668)|~r1(X1668,X1667)|~r1(X1667,X1669)|p101(skolem0010(X1669,X1668,X1667,X1669,X1668))|p101(X1668)|~p100(X1668),inference(factor,[status(thm)],[c43])).
% 6.47/6.70 cnf(c1767,plain,~r1(skolem0001,X1670)|~r1(X1670,X1670)|p101(skolem0010(X1670,X1670,X1670,X1670,X1670))|p101(X1670)|~p100(X1670),inference(factor,[status(thm)],[c355])).
% 6.47/6.70 cnf(c1772,plain,~r1(skolem0001,X1671)|p101(skolem0010(X1671,X1671,X1671,X1671,X1671))|p101(X1671)|~p100(X1671),inference(resolution,[status(thm)],[c1767, c69])).
% 6.47/6.70 cnf(c1774,plain,p101(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001))|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c1772, c69])).
% 6.47/6.70 cnf(c1775,plain,p101(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001))|p101(skolem0001),inference(resolution,[status(thm)],[c1774, c67])).
% 6.47/6.70 cnf(c1776,plain,p101(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c1775, c66])).
% 6.47/6.70 cnf(c40,negated_conjecture,~r1(skolem0001,X460)|~r1(X460,X459)|~r1(X459,X461)|~r1(X461,X463)|~r1(X463,X462)|r1(X462,skolem0010(X460,X459,X461,X463,X462))|p101(X462)|~p100(X462),inference(split_conjunct,[status(thm)],[c6])).
% 6.47/6.70 cnf(c335,plain,~r1(skolem0001,X1625)|~r1(X1625,X1626)|~r1(X1626,X1627)|~r1(X1627,X1625)|r1(X1626,skolem0010(X1625,X1626,X1627,X1625,X1626))|p101(X1626)|~p100(X1626),inference(factor,[status(thm)],[c40])).
% 6.47/6.70 cnf(c1287,plain,~r1(skolem0001,X1631)|~r1(X1631,X1631)|r1(X1631,skolem0010(X1631,X1631,X1631,X1631,X1631))|p101(X1631)|~p100(X1631),inference(factor,[status(thm)],[c335])).
% 6.47/6.70 cnf(c1293,plain,~r1(skolem0001,X1632)|r1(X1632,skolem0010(X1632,X1632,X1632,X1632,X1632))|p101(X1632)|~p100(X1632),inference(resolution,[status(thm)],[c1287, c69])).
% 6.47/6.70 cnf(c1294,plain,r1(skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001))|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c1293, c69])).
% 6.47/6.70 cnf(c1295,plain,r1(skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001))|p101(skolem0001),inference(resolution,[status(thm)],[c1294, c67])).
% 6.47/6.70 cnf(c1520,plain,r1(skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c1295, c66])).
% 6.47/6.70 cnf(c33,negated_conjecture,~r1(skolem0001,X367)|~r1(X367,X366)|~r1(X366,X368)|~r1(X368,X370)|~r1(X370,X369)|~p3(skolem0008(X367,X366,X368,X370,X369))|p102(X369)|~p101(X369),inference(split_conjunct,[status(thm)],[c6])).
% 6.47/6.70 cnf(c7,negated_conjecture,~r1(skolem0001,X40)|~r1(X40,X39)|~r1(X39,X37)|~r1(X37,X38)|~r1(X38,X41)|p3(X41),inference(split_conjunct,[status(thm)],[c6])).
% 6.47/6.70 cnf(c72,plain,~r1(skolem0001,X72)|~r1(X72,X73)|~r1(X73,X71)|~r1(X71,X73)|p3(X71),inference(factor,[status(thm)],[c7])).
% 6.47/6.70 cnf(c95,plain,~r1(skolem0001,X81)|~r1(X81,X82)|~r1(X82,X82)|p3(X82),inference(factor,[status(thm)],[c72])).
% 6.47/6.70 cnf(c104,plain,~r1(skolem0001,X84)|~r1(X84,X85)|p3(X85),inference(resolution,[status(thm)],[c95, c69])).
% 6.47/6.70 cnf(c32,negated_conjecture,~r1(skolem0001,X357)|~r1(X357,X356)|~r1(X356,X358)|~r1(X358,X360)|~r1(X360,X359)|r1(X359,skolem0008(X357,X356,X358,X360,X359))|p102(X359)|~p101(X359),inference(split_conjunct,[status(thm)],[c6])).
% 6.47/6.70 cnf(c1342,plain,p101(skolem0001)|~r1(skolem0001,X3502)|~r1(X3502,X3503)|~r1(X3503,X3504)|~r1(X3504,skolem0001)|r1(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001),skolem0008(X3502,X3503,X3504,skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)))|p102(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001))|~p101(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c1295, c32])).
% 6.47/6.70 cnf(c3817,plain,p101(skolem0001)|~r1(skolem0001,X4349)|~r1(X4349,X4348)|~r1(X4348,X4347)|~r1(X4347,skolem0001)|r1(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001),skolem0008(X4349,X4348,X4347,skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)))|p102(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c1342, c1776])).
% 6.47/6.70 cnf(c4285,plain,p101(skolem0001)|~r1(skolem0001,X4350)|~r1(X4350,skolem0001)|r1(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001),skolem0008(X4350,skolem0001,X4350,skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)))|p102(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)),inference(factor,[status(thm)],[c3817])).
% 6.47/6.70 cnf(c4288,plain,p101(skolem0001)|~r1(skolem0001,skolem0001)|r1(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001),skolem0008(skolem0001,skolem0001,skolem0001,skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)))|p102(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)),inference(factor,[status(thm)],[c4285])).
% 6.47/6.70 cnf(c4290,plain,p101(skolem0001)|r1(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001),skolem0008(skolem0001,skolem0001,skolem0001,skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)))|p102(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c4288, c69])).
% 6.47/6.70 cnf(c4637,plain,p101(skolem0001)|r1(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001),skolem0008(skolem0001,skolem0001,skolem0001,skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)))|~r1(skolem0001,skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c4290, c42])).
% 6.47/6.70 cnf(c4998,plain,p101(skolem0001)|r1(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001),skolem0008(skolem0001,skolem0001,skolem0001,skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)))|~p100(skolem0001),inference(resolution,[status(thm)],[c4637, c69])).
% 6.47/6.70 cnf(c4999,plain,p101(skolem0001)|r1(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001),skolem0008(skolem0001,skolem0001,skolem0001,skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001))),inference(resolution,[status(thm)],[c4998, c67])).
% 6.47/6.70 cnf(c5000,plain,r1(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001),skolem0008(skolem0001,skolem0001,skolem0001,skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001))),inference(resolution,[status(thm)],[c4999, c66])).
% 6.47/6.70 cnf(c5504,plain,~r1(skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001))|p3(skolem0008(skolem0001,skolem0001,skolem0001,skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001))),inference(resolution,[status(thm)],[c5000, c104])).
% 6.47/6.70 cnf(c5669,plain,p3(skolem0008(skolem0001,skolem0001,skolem0001,skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001))),inference(resolution,[status(thm)],[c5504, c1520])).
% 6.47/6.70 cnf(c5670,plain,~r1(skolem0001,skolem0001)|~r1(skolem0001,skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001))|p102(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001))|~p101(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c5669, c33])).
% 6.47/6.70 cnf(c5671,plain,~r1(skolem0001,skolem0001)|p102(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001))|~p101(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c5670, c1520])).
% 6.47/6.70 cnf(c5672,plain,~r1(skolem0001,skolem0001)|p102(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c5671, c1776])).
% 6.47/6.70 cnf(c5673,plain,p102(skolem0010(skolem0001,skolem0001,skolem0001,skolem0001,skolem0001)),inference(resolution,[status(thm)],[c5672, c69])).
% 6.47/6.70 cnf(c5685,plain,~r1(skolem0001,skolem0001)|p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c5673, c42])).
% 6.47/6.70 cnf(c5693,plain,p101(skolem0001)|~p100(skolem0001),inference(resolution,[status(thm)],[c5685, c69])).
% 6.47/6.70 cnf(c5694,plain,p101(skolem0001),inference(resolution,[status(thm)],[c5693, c67])).
% 6.47/6.70 cnf(c5695,plain,$false,inference(resolution,[status(thm)],[c5694, c66])).
% 6.47/6.70 % SZS output end CNFRefutation
% 6.47/6.70
% 6.47/6.70 % Initial clauses : 62
% 6.47/6.70 % Processed clauses : 1177
% 6.47/6.70 % Factors computed : 1866
% 6.47/6.70 % Resolvents computed: 3760
% 6.47/6.70 % Tautologies deleted: 254
% 6.47/6.70 % Forward subsumed : 1896
% 6.47/6.70 % Backward subsumed : 378
% 6.47/6.70 % -------- CPU Time ---------
% 6.47/6.70 % User time : 6.290 s
% 6.47/6.70 % System time : 0.041 s
% 6.47/6.70 % Total time : 6.331 s
%------------------------------------------------------------------------------