%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : COM022+4 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:17:45 EDT 2024
% Result : Theorem 5.11s 5.30s
% Output : Refutation 5.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : COM022+4 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n017.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 07:12:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 5.11/5.30 % Version: 1.5
% 5.11/5.30 % SZS status Theorem
% 5.11/5.30 % SZS output start CNFRefutation
% 5.11/5.30 fof(m__731,plain,((aElement0(xa)&aElement0(xb))&aElement0(xc)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__731)).
% 5.11/5.30 cnf(c719,plain,aElement0(xb),inference(split_conjunct,[status(thm)],[m__731])).
% 5.11/5.30 cnf(reflexivity,axiom,X89=X89,theory(equality)).
% 5.11/5.30 fof(m__,conjecture,(((((aReductOfIn0(xb,xa,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xb))))|sdtmndtplgtdt0(xa,xR,xb))&((aReductOfIn0(xc,xa,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xc))))|sdtmndtplgtdt0(xa,xR,xc)))=>(?[W0]:((((aElement0(W0)&aReductOfIn0(W0,xa,xR))&(W0=xb|((aReductOfIn0(xb,W0,xR)|(?[W1]:((aElement0(W1)&aReductOfIn0(W1,W0,xR))&sdtmndtplgtdt0(W1,xR,xb))))&sdtmndtplgtdt0(W0,xR,xb))))&sdtmndtasgtdt0(W0,xR,xb))&(?[W1]:((((aElement0(W1)&aReductOfIn0(W1,xa,xR))&(W1=xc|((aReductOfIn0(xc,W1,xR)|(?[W2]:((aElement0(W2)&aReductOfIn0(W2,W1,xR))&sdtmndtplgtdt0(W2,xR,xc))))&sdtmndtplgtdt0(W1,xR,xc))))&sdtmndtasgtdt0(W1,xR,xc))&(?[W2]:(((((aElement0(W2)&(W0=W2|((aReductOfIn0(W2,W0,xR)|(?[W3]:((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W2))))&sdtmndtplgtdt0(W0,xR,W2))))&sdtmndtasgtdt0(W0,xR,W2))&(W1=W2|((aReductOfIn0(W2,W1,xR)|(?[W3]:((aElement0(W3)&aReductOfIn0(W3,W1,xR))&sdtmndtplgtdt0(W3,xR,W2))))&sdtmndtplgtdt0(W1,xR,W2))))&sdtmndtasgtdt0(W1,xR,W2))&(?[W3]:((((((((aElement0(W3)&(W2=W3|((aReductOfIn0(W3,W2,xR)|(?[W4]:((aElement0(W4)&aReductOfIn0(W4,W2,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W2,xR,W3))))&sdtmndtasgtdt0(W2,xR,W3))&(~(?[W4]:aReductOfIn0(W4,W3,xR))))&aNormalFormOfIn0(W3,W2,xR))&(xb=W3|((aReductOfIn0(W3,xb,xR)|(?[W4]:((aElement0(W4)&aReductOfIn0(W4,xb,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(xb,xR,W3))))&sdtmndtasgtdt0(xb,xR,W3))&(xc=W3|((aReductOfIn0(W3,xc,xR)|(?[W4]:((aElement0(W4)&aReductOfIn0(W4,xc,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(xc,xR,W3))))&sdtmndtasgtdt0(xc,xR,W3))))))))))=>(((((xa=xb|((aReductOfIn0(xb,xa,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xb))))&sdtmndtplgtdt0(xa,xR,xb)))&sdtmndtasgtdt0(xa,xR,xb))&(xa=xc|((aReductOfIn0(xc,xa,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xc))))&sdtmndtplgtdt0(xa,xR,xc))))&sdtmndtasgtdt0(xa,xR,xc))=>(?[W0]:((aElement0(W0)&((((xb=W0|aReductOfIn0(W0,xb,xR))|(?[W1]:((aElement0(W1)&aReductOfIn0(W1,xb,xR))&sdtmndtplgtdt0(W1,xR,W0))))|sdtmndtplgtdt0(xb,xR,W0))|sdtmndtasgtdt0(xb,xR,W0)))&((((xc=W0|aReductOfIn0(W0,xc,xR))|(?[W1]:((aElement0(W1)&aReductOfIn0(W1,xc,xR))&sdtmndtplgtdt0(W1,xR,W0))))|sdtmndtplgtdt0(xc,xR,W0))|sdtmndtasgtdt0(xc,xR,W0)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__)).
% 5.11/5.30 fof(c10,negated_conjecture,(~(((((aReductOfIn0(xb,xa,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xb))))|sdtmndtplgtdt0(xa,xR,xb))&((aReductOfIn0(xc,xa,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xc))))|sdtmndtplgtdt0(xa,xR,xc)))=>(?[W0]:((((aElement0(W0)&aReductOfIn0(W0,xa,xR))&(W0=xb|((aReductOfIn0(xb,W0,xR)|(?[W1]:((aElement0(W1)&aReductOfIn0(W1,W0,xR))&sdtmndtplgtdt0(W1,xR,xb))))&sdtmndtplgtdt0(W0,xR,xb))))&sdtmndtasgtdt0(W0,xR,xb))&(?[W1]:((((aElement0(W1)&aReductOfIn0(W1,xa,xR))&(W1=xc|((aReductOfIn0(xc,W1,xR)|(?[W2]:((aElement0(W2)&aReductOfIn0(W2,W1,xR))&sdtmndtplgtdt0(W2,xR,xc))))&sdtmndtplgtdt0(W1,xR,xc))))&sdtmndtasgtdt0(W1,xR,xc))&(?[W2]:(((((aElement0(W2)&(W0=W2|((aReductOfIn0(W2,W0,xR)|(?[W3]:((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W2))))&sdtmndtplgtdt0(W0,xR,W2))))&sdtmndtasgtdt0(W0,xR,W2))&(W1=W2|((aReductOfIn0(W2,W1,xR)|(?[W3]:((aElement0(W3)&aReductOfIn0(W3,W1,xR))&sdtmndtplgtdt0(W3,xR,W2))))&sdtmndtplgtdt0(W1,xR,W2))))&sdtmndtasgtdt0(W1,xR,W2))&(?[W3]:((((((((aElement0(W3)&(W2=W3|((aReductOfIn0(W3,W2,xR)|(?[W4]:((aElement0(W4)&aReductOfIn0(W4,W2,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W2,xR,W3))))&sdtmndtasgtdt0(W2,xR,W3))&(~(?[W4]:aReductOfIn0(W4,W3,xR))))&aNormalFormOfIn0(W3,W2,xR))&(xb=W3|((aReductOfIn0(W3,xb,xR)|(?[W4]:((aElement0(W4)&aReductOfIn0(W4,xb,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(xb,xR,W3))))&sdtmndtasgtdt0(xb,xR,W3))&(xc=W3|((aReductOfIn0(W3,xc,xR)|(?[W4]:((aElement0(W4)&aReductOfIn0(W4,xc,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(xc,xR,W3))))&sdtmndtasgtdt0(xc,xR,W3))))))))))=>(((((xa=xb|((aReductOfIn0(xb,xa,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xb))))&sdtmndtplgtdt0(xa,xR,xb)))&sdtmndtasgtdt0(xa,xR,xb))&(xa=xc|((aReductOfIn0(xc,xa,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xc))))&sdtmndtplgtdt0(xa,xR,xc))))&sdtmndtasgtdt0(xa,xR,xc))=>(?[W0]:((aElement0(W0)&((((xb=W0|aReductOfIn0(W0,xb,xR))|(?[W1]:((aElement0(W1)&aReductOfIn0(W1,xb,xR))&sdtmndtplgtdt0(W1,xR,W0))))|sdtmndtplgtdt0(xb,xR,W0))|sdtmndtasgtdt0(xb,xR,W0)))&((((xc=W0|aReductOfIn0(W0,xc,xR))|(?[W1]:((aElement0(W1)&aReductOfIn0(W1,xc,xR))&sdtmndtplgtdt0(W1,xR,W0))))|sdtmndtplgtdt0(xc,xR,W0))|sdtmndtasgtdt0(xc,xR,W0))))))),inference(assume_negation,[status(cth)],[m__])).
% 5.11/5.30 fof(c11,negated_conjecture,(((((~aReductOfIn0(xb,xa,xR)&(![W0]:((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|~sdtmndtplgtdt0(W0,xR,xb))))&~sdtmndtplgtdt0(xa,xR,xb))|((~aReductOfIn0(xc,xa,xR)&(![W0]:((~aElement0(W0)|~aReductOfIn0(W0,xa,xR))|~sdtmndtplgtdt0(W0,xR,xc))))&~sdtmndtplgtdt0(xa,xR,xc)))|(?[W0]:((((aElement0(W0)&aReductOfIn0(W0,xa,xR))&(W0=xb|((aReductOfIn0(xb,W0,xR)|(?[W1]:((aElement0(W1)&aReductOfIn0(W1,W0,xR))&sdtmndtplgtdt0(W1,xR,xb))))&sdtmndtplgtdt0(W0,xR,xb))))&sdtmndtasgtdt0(W0,xR,xb))&(?[W1]:((((aElement0(W1)&aReductOfIn0(W1,xa,xR))&(W1=xc|((aReductOfIn0(xc,W1,xR)|(?[W2]:((aElement0(W2)&aReductOfIn0(W2,W1,xR))&sdtmndtplgtdt0(W2,xR,xc))))&sdtmndtplgtdt0(W1,xR,xc))))&sdtmndtasgtdt0(W1,xR,xc))&(?[W2]:(((((aElement0(W2)&(W0=W2|((aReductOfIn0(W2,W0,xR)|(?[W3]:((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W2))))&sdtmndtplgtdt0(W0,xR,W2))))&sdtmndtasgtdt0(W0,xR,W2))&(W1=W2|((aReductOfIn0(W2,W1,xR)|(?[W3]:((aElement0(W3)&aReductOfIn0(W3,W1,xR))&sdtmndtplgtdt0(W3,xR,W2))))&sdtmndtplgtdt0(W1,xR,W2))))&sdtmndtasgtdt0(W1,xR,W2))&(?[W3]:((((((((aElement0(W3)&(W2=W3|((aReductOfIn0(W3,W2,xR)|(?[W4]:((aElement0(W4)&aReductOfIn0(W4,W2,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W2,xR,W3))))&sdtmndtasgtdt0(W2,xR,W3))&(![W4]:~aReductOfIn0(W4,W3,xR)))&aNormalFormOfIn0(W3,W2,xR))&(xb=W3|((aReductOfIn0(W3,xb,xR)|(?[W4]:((aElement0(W4)&aReductOfIn0(W4,xb,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(xb,xR,W3))))&sdtmndtasgtdt0(xb,xR,W3))&(xc=W3|((aReductOfIn0(W3,xc,xR)|(?[W4]:((aElement0(W4)&aReductOfIn0(W4,xc,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(xc,xR,W3))))&sdtmndtasgtdt0(xc,xR,W3))))))))))&(((((xa=xb|((aReductOfIn0(xb,xa,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xb))))&sdtmndtplgtdt0(xa,xR,xb)))&sdtmndtasgtdt0(xa,xR,xb))&(xa=xc|((aReductOfIn0(xc,xa,xR)|(?[W0]:((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtplgtdt0(W0,xR,xc))))&sdtmndtplgtdt0(xa,xR,xc))))&sdtmndtasgtdt0(xa,xR,xc))&(![W0]:((~aElement0(W0)|((((xb!=W0&~aReductOfIn0(W0,xb,xR))&(![W1]:((~aElement0(W1)|~aReductOfIn0(W1,xb,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xb,xR,W0))&~sdtmndtasgtdt0(xb,xR,W0)))|((((xc!=W0&~aReductOfIn0(W0,xc,xR))&(![W1]:((~aElement0(W1)|~aReductOfIn0(W1,xc,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xc,xR,W0))&~sdtmndtasgtdt0(xc,xR,W0)))))),inference(fof_nnf,[status(thm)],[c10])).
% 5.11/5.30 fof(c12,negated_conjecture,(((((~aReductOfIn0(xb,xa,xR)&(![X2]:((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))))&~sdtmndtplgtdt0(xa,xR,xb))|((~aReductOfIn0(xc,xa,xR)&(![X3]:((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc))))&~sdtmndtplgtdt0(xa,xR,xc)))|(?[X4]:((((aElement0(X4)&aReductOfIn0(X4,xa,xR))&(X4=xb|((aReductOfIn0(xb,X4,xR)|(?[X5]:((aElement0(X5)&aReductOfIn0(X5,X4,xR))&sdtmndtplgtdt0(X5,xR,xb))))&sdtmndtplgtdt0(X4,xR,xb))))&sdtmndtasgtdt0(X4,xR,xb))&(?[X6]:((((aElement0(X6)&aReductOfIn0(X6,xa,xR))&(X6=xc|((aReductOfIn0(xc,X6,xR)|(?[X7]:((aElement0(X7)&aReductOfIn0(X7,X6,xR))&sdtmndtplgtdt0(X7,xR,xc))))&sdtmndtplgtdt0(X6,xR,xc))))&sdtmndtasgtdt0(X6,xR,xc))&(?[X8]:(((((aElement0(X8)&(X4=X8|((aReductOfIn0(X8,X4,xR)|(?[X9]:((aElement0(X9)&aReductOfIn0(X9,X4,xR))&sdtmndtplgtdt0(X9,xR,X8))))&sdtmndtplgtdt0(X4,xR,X8))))&sdtmndtasgtdt0(X4,xR,X8))&(X6=X8|((aReductOfIn0(X8,X6,xR)|(?[X10]:((aElement0(X10)&aReductOfIn0(X10,X6,xR))&sdtmndtplgtdt0(X10,xR,X8))))&sdtmndtplgtdt0(X6,xR,X8))))&sdtmndtasgtdt0(X6,xR,X8))&(?[X11]:((((((((aElement0(X11)&(X8=X11|((aReductOfIn0(X11,X8,xR)|(?[X12]:((aElement0(X12)&aReductOfIn0(X12,X8,xR))&sdtmndtplgtdt0(X12,xR,X11))))&sdtmndtplgtdt0(X8,xR,X11))))&sdtmndtasgtdt0(X8,xR,X11))&(![X13]:~aReductOfIn0(X13,X11,xR)))&aNormalFormOfIn0(X11,X8,xR))&(xb=X11|((aReductOfIn0(X11,xb,xR)|(?[X14]:((aElement0(X14)&aReductOfIn0(X14,xb,xR))&sdtmndtplgtdt0(X14,xR,X11))))&sdtmndtplgtdt0(xb,xR,X11))))&sdtmndtasgtdt0(xb,xR,X11))&(xc=X11|((aReductOfIn0(X11,xc,xR)|(?[X15]:((aElement0(X15)&aReductOfIn0(X15,xc,xR))&sdtmndtplgtdt0(X15,xR,X11))))&sdtmndtplgtdt0(xc,xR,X11))))&sdtmndtasgtdt0(xc,xR,X11))))))))))&(((((xa=xb|((aReductOfIn0(xb,xa,xR)|(?[X16]:((aElement0(X16)&aReductOfIn0(X16,xa,xR))&sdtmndtplgtdt0(X16,xR,xb))))&sdtmndtplgtdt0(xa,xR,xb)))&sdtmndtasgtdt0(xa,xR,xb))&(xa=xc|((aReductOfIn0(xc,xa,xR)|(?[X17]:((aElement0(X17)&aReductOfIn0(X17,xa,xR))&sdtmndtplgtdt0(X17,xR,xc))))&sdtmndtplgtdt0(xa,xR,xc))))&sdtmndtasgtdt0(xa,xR,xc))&(![X18]:((~aElement0(X18)|((((xb!=X18&~aReductOfIn0(X18,xb,xR))&(![X19]:((~aElement0(X19)|~aReductOfIn0(X19,xb,xR))|~sdtmndtplgtdt0(X19,xR,X18))))&~sdtmndtplgtdt0(xb,xR,X18))&~sdtmndtasgtdt0(xb,xR,X18)))|((((xc!=X18&~aReductOfIn0(X18,xc,xR))&(![X20]:((~aElement0(X20)|~aReductOfIn0(X20,xc,xR))|~sdtmndtplgtdt0(X20,xR,X18))))&~sdtmndtplgtdt0(xc,xR,X18))&~sdtmndtasgtdt0(xc,xR,X18)))))),inference(variable_rename,[status(thm)],[c11])).
% 5.11/5.32 fof(c14,negated_conjecture,(![X2]:(![X3]:(![X13]:(![X18]:(![X19]:(![X20]:(((((~aReductOfIn0(xb,xa,xR)&((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb)))&~sdtmndtplgtdt0(xa,xR,xb))|((~aReductOfIn0(xc,xa,xR)&((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))&~sdtmndtplgtdt0(xa,xR,xc)))|((((aElement0(skolem0001)&aReductOfIn0(skolem0001,xa,xR))&(skolem0001=xb|((aReductOfIn0(xb,skolem0001,xR)|((aElement0(skolem0002)&aReductOfIn0(skolem0002,skolem0001,xR))&sdtmndtplgtdt0(skolem0002,xR,xb)))&sdtmndtplgtdt0(skolem0001,xR,xb))))&sdtmndtasgtdt0(skolem0001,xR,xb))&((((aElement0(skolem0003)&aReductOfIn0(skolem0003,xa,xR))&(skolem0003=xc|((aReductOfIn0(xc,skolem0003,xR)|((aElement0(skolem0004)&aReductOfIn0(skolem0004,skolem0003,xR))&sdtmndtplgtdt0(skolem0004,xR,xc)))&sdtmndtplgtdt0(skolem0003,xR,xc))))&sdtmndtasgtdt0(skolem0003,xR,xc))&(((((aElement0(skolem0005)&(skolem0001=skolem0005|((aReductOfIn0(skolem0005,skolem0001,xR)|((aElement0(skolem0006)&aReductOfIn0(skolem0006,skolem0001,xR))&sdtmndtplgtdt0(skolem0006,xR,skolem0005)))&sdtmndtplgtdt0(skolem0001,xR,skolem0005))))&sdtmndtasgtdt0(skolem0001,xR,skolem0005))&(skolem0003=skolem0005|((aReductOfIn0(skolem0005,skolem0003,xR)|((aElement0(skolem0007)&aReductOfIn0(skolem0007,skolem0003,xR))&sdtmndtplgtdt0(skolem0007,xR,skolem0005)))&sdtmndtplgtdt0(skolem0003,xR,skolem0005))))&sdtmndtasgtdt0(skolem0003,xR,skolem0005))&((((((((aElement0(skolem0008)&(skolem0005=skolem0008|((aReductOfIn0(skolem0008,skolem0005,xR)|((aElement0(skolem0009)&aReductOfIn0(skolem0009,skolem0005,xR))&sdtmndtplgtdt0(skolem0009,xR,skolem0008)))&sdtmndtplgtdt0(skolem0005,xR,skolem0008))))&sdtmndtasgtdt0(skolem0005,xR,skolem0008))&~aReductOfIn0(X13,skolem0008,xR))&aNormalFormOfIn0(skolem0008,skolem0005,xR))&(xb=skolem0008|((aReductOfIn0(skolem0008,xb,xR)|((aElement0(skolem0010)&aReductOfIn0(skolem0010,xb,xR))&sdtmndtplgtdt0(skolem0010,xR,skolem0008)))&sdtmndtplgtdt0(xb,xR,skolem0008))))&sdtmndtasgtdt0(xb,xR,skolem0008))&(xc=skolem0008|((aReductOfIn0(skolem0008,xc,xR)|((aElement0(skolem0011)&aReductOfIn0(skolem0011,xc,xR))&sdtmndtplgtdt0(skolem0011,xR,skolem0008)))&sdtmndtplgtdt0(xc,xR,skolem0008))))&sdtmndtasgtdt0(xc,xR,skolem0008))))))&(((((xa=xb|((aReductOfIn0(xb,xa,xR)|((aElement0(skolem0012)&aReductOfIn0(skolem0012,xa,xR))&sdtmndtplgtdt0(skolem0012,xR,xb)))&sdtmndtplgtdt0(xa,xR,xb)))&sdtmndtasgtdt0(xa,xR,xb))&(xa=xc|((aReductOfIn0(xc,xa,xR)|((aElement0(skolem0013)&aReductOfIn0(skolem0013,xa,xR))&sdtmndtplgtdt0(skolem0013,xR,xc)))&sdtmndtplgtdt0(xa,xR,xc))))&sdtmndtasgtdt0(xa,xR,xc))&((~aElement0(X18)|((((xb!=X18&~aReductOfIn0(X18,xb,xR))&((~aElement0(X19)|~aReductOfIn0(X19,xb,xR))|~sdtmndtplgtdt0(X19,xR,X18)))&~sdtmndtplgtdt0(xb,xR,X18))&~sdtmndtasgtdt0(xb,xR,X18)))|((((xc!=X18&~aReductOfIn0(X18,xc,xR))&((~aElement0(X20)|~aReductOfIn0(X20,xc,xR))|~sdtmndtplgtdt0(X20,xR,X18)))&~sdtmndtplgtdt0(xc,xR,X18))&~sdtmndtasgtdt0(xc,xR,X18))))))))))),inference(shift_quantors,[status(thm)],[fof(c13,negated_conjecture,(((((~aReductOfIn0(xb,xa,xR)&(![X2]:((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))))&~sdtmndtplgtdt0(xa,xR,xb))|((~aReductOfIn0(xc,xa,xR)&(![X3]:((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc))))&~sdtmndtplgtdt0(xa,xR,xc)))|((((aElement0(skolem0001)&aReductOfIn0(skolem0001,xa,xR))&(skolem0001=xb|((aReductOfIn0(xb,skolem0001,xR)|((aElement0(skolem0002)&aReductOfIn0(skolem0002,skolem0001,xR))&sdtmndtplgtdt0(skolem0002,xR,xb)))&sdtmndtplgtdt0(skolem0001,xR,xb))))&sdtmndtasgtdt0(skolem0001,xR,xb))&((((aElement0(skolem0003)&aReductOfIn0(skolem0003,xa,xR))&(skolem0003=xc|((aReductOfIn0(xc,skolem0003,xR)|((aElement0(skolem0004)&aReductOfIn0(skolem0004,skolem0003,xR))&sdtmndtplgtdt0(skolem0004,xR,xc)))&sdtmndtplgtdt0(skolem0003,xR,xc))))&sdtmndtasgtdt0(skolem0003,xR,xc))&(((((aElement0(skolem0005)&(skolem0001=skolem0005|((aReductOfIn0(skolem0005,skolem0001,xR)|((aElement0(skolem0006)&aReductOfIn0(skolem0006,skolem0001,xR))&sdtmndtplgtdt0(skolem0006,xR,skolem0005)))&sdtmndtplgtdt0(skolem0001,xR,skolem0005))))&sdtmndtasgtdt0(skolem0001,xR,skolem0005))&(skolem0003=skolem0005|((aReductOfIn0(skolem0005,skolem0003,xR)|((aElement0(skolem0007)&aReductOfIn0(skolem0007,skolem0003,xR))&sdtmndtplgtdt0(skolem0007,xR,skolem0005)))&sdtmndtplgtdt0(skolem0003,xR,skolem0005))))&sdtmndtasgtdt0(skolem0003,xR,skolem0005))&((((((((aElement0(skolem0008)&(skolem0005=skolem0008|((aReductOfIn0(skolem0008,skolem0005,xR)|((aElement0(skolem0009)&aReductOfIn0(skolem0009,skolem0005,xR))&sdtmndtplgtdt0(skolem0009,xR,skolem0008)))&sdtmndtplgtdt0(skolem0005,xR,skolem0008))))&sdtmndtasgtdt0(skolem0005,xR,skolem0008))&(![X13]:~aReductOfIn0(X13,skolem0008,xR)))&aNormalFormOfIn0(skolem0008,skolem0005,xR))&(xb=skolem0008|((aReductOfIn0(skolem0008,xb,xR)|((aElement0(skolem0010)&aReductOfIn0(skolem0010,xb,xR))&sdtmndtplgtdt0(skolem0010,xR,skolem0008)))&sdtmndtplgtdt0(xb,xR,skolem0008))))&sdtmndtasgtdt0(xb,xR,skolem0008))&(xc=skolem0008|((aReductOfIn0(skolem0008,xc,xR)|((aElement0(skolem0011)&aReductOfIn0(skolem0011,xc,xR))&sdtmndtplgtdt0(skolem0011,xR,skolem0008)))&sdtmndtplgtdt0(xc,xR,skolem0008))))&sdtmndtasgtdt0(xc,xR,skolem0008))))))&(((((xa=xb|((aReductOfIn0(xb,xa,xR)|((aElement0(skolem0012)&aReductOfIn0(skolem0012,xa,xR))&sdtmndtplgtdt0(skolem0012,xR,xb)))&sdtmndtplgtdt0(xa,xR,xb)))&sdtmndtasgtdt0(xa,xR,xb))&(xa=xc|((aReductOfIn0(xc,xa,xR)|((aElement0(skolem0013)&aReductOfIn0(skolem0013,xa,xR))&sdtmndtplgtdt0(skolem0013,xR,xc)))&sdtmndtplgtdt0(xa,xR,xc))))&sdtmndtasgtdt0(xa,xR,xc))&(![X18]:((~aElement0(X18)|((((xb!=X18&~aReductOfIn0(X18,xb,xR))&(![X19]:((~aElement0(X19)|~aReductOfIn0(X19,xb,xR))|~sdtmndtplgtdt0(X19,xR,X18))))&~sdtmndtplgtdt0(xb,xR,X18))&~sdtmndtasgtdt0(xb,xR,X18)))|((((xc!=X18&~aReductOfIn0(X18,xc,xR))&(![X20]:((~aElement0(X20)|~aReductOfIn0(X20,xc,xR))|~sdtmndtplgtdt0(X20,xR,X18))))&~sdtmndtplgtdt0(xc,xR,X18))&~sdtmndtasgtdt0(xc,xR,X18)))))),inference(skolemize,[status(esa)],[c12])).])).
% 5.11/5.32 fof(c15,negated_conjecture,(![X2]:(![X3]:(![X13]:(![X18]:(![X19]:(![X20]:(((((((((((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|aElement0(skolem0001))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|aReductOfIn0(skolem0001,xa,xR)))&(((((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aElement0(skolem0002))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aReductOfIn0(skolem0002,skolem0001,xR)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|sdtmndtplgtdt0(skolem0002,xR,xb)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0001=xb|sdtmndtplgtdt0(skolem0001,xR,xb)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0001,xR,xb)))&((((((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|aElement0(skolem0003))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|aReductOfIn0(skolem0003,xa,xR)))&(((((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aElement0(skolem0004))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aReductOfIn0(skolem0004,skolem0003,xR)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|sdtmndtplgtdt0(skolem0004,xR,xc)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0003=xc|sdtmndtplgtdt0(skolem0003,xR,xc)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0003,xR,xc)))&(((((((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|aElement0(skolem0005))&(((((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aElement0(skolem0006))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aReductOfIn0(skolem0006,skolem0001,xR)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|sdtmndtplgtdt0(skolem0006,xR,skolem0005)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0001=skolem0005|sdtmndtplgtdt0(skolem0001,xR,skolem0005)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0001,xR,skolem0005)))&(((((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aElement0(skolem0007))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aReductOfIn0(skolem0007,skolem0003,xR)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|sdtmndtplgtdt0(skolem0007,xR,skolem0005)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0003=skolem0005|sdtmndtplgtdt0(skolem0003,xR,skolem0005)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0003,xR,skolem0005)))&((((((((((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|aElement0(skolem0008))&(((((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aElement0(skolem0009))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aReductOfIn0(skolem0009,skolem0005,xR)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|sdtmndtplgtdt0(skolem0009,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(skolem0005=skolem0008|sdtmndtplgtdt0(skolem0005,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0005,xR,skolem0008)))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|~aReductOfIn0(X13,skolem0008,xR)))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|aNormalFormOfIn0(skolem0008,skolem0005,xR)))&(((((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aElement0(skolem0010))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aReductOfIn0(skolem0010,xb,xR)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|sdtmndtplgtdt0(skolem0010,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(xb=skolem0008|sdtmndtplgtdt0(xb,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(xb,xR,skolem0008)))&(((((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aElement0(skolem0011))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aReductOfIn0(skolem0011,xc,xR)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|sdtmndtplgtdt0(skolem0011,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|(xc=skolem0008|sdtmndtplgtdt0(xc,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(xc,xR,skolem0008))))))&((((((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aElement0(skolem0001))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aReductOfIn0(skolem0001,xa,xR)))&(((((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aElement0(skolem0002))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aReductOfIn0(skolem0002,skolem0001,xR)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|sdtmndtplgtdt0(skolem0002,xR,xb)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=xb|sdtmndtplgtdt0(skolem0001,xR,xb)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0001,xR,xb)))&((((((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aElement0(skolem0003))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aReductOfIn0(skolem0003,xa,xR)))&(((((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aElement0(skolem0004))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aReductOfIn0(skolem0004,skolem0003,xR)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|sdtmndtplgtdt0(skolem0004,xR,xc)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=xc|sdtmndtplgtdt0(skolem0003,xR,xc)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0003,xR,xc)))&(((((((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aElement0(skolem0005))&(((((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aElement0(skolem0006))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aReductOfIn0(skolem0006,skolem0001,xR)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|sdtmndtplgtdt0(skolem0006,xR,skolem0005)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=skolem0005|sdtmndtplgtdt0(skolem0001,xR,skolem0005)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0001,xR,skolem0005)))&(((((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aElement0(skolem0007))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aReductOfIn0(skolem0007,skolem0003,xR)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|sdtmndtplgtdt0(skolem0007,xR,skolem0005)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=skolem0005|sdtmndtplgtdt0(skolem0003,xR,skolem0005)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0003,xR,skolem0005)))&((((((((((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aElement0(skolem0008))&(((((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aElement0(skolem0009))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aReductOfIn0(skolem0009,skolem0005,xR)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|sdtmndtplgtdt0(skolem0009,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0005=skolem0008|sdtmndtplgtdt0(skolem0005,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0005,xR,skolem0008)))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|~aReductOfIn0(X13,skolem0008,xR)))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aNormalFormOfIn0(skolem0008,skolem0005,xR)))&(((((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aElement0(skolem0010))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aReductOfIn0(skolem0010,xb,xR)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|sdtmndtplgtdt0(skolem0010,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xb=skolem0008|sdtmndtplgtdt0(xb,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(xb,xR,skolem0008)))&(((((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aElement0(skolem0011))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aReductOfIn0(skolem0011,xc,xR)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|sdtmndtplgtdt0(skolem0011,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xc=skolem0008|sdtmndtplgtdt0(xc,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(xc,xR,skolem0008)))))))&((((((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0001))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|aReductOfIn0(skolem0001,xa,xR)))&(((((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aElement0(skolem0002))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aReductOfIn0(skolem0002,skolem0001,xR)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|sdtmndtplgtdt0(skolem0002,xR,xb)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=xb|sdtmndtplgtdt0(skolem0001,xR,xb)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0001,xR,xb)))&((((((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0003))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|aReductOfIn0(skolem0003,xa,xR)))&(((((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aElement0(skolem0004))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aReductOfIn0(skolem0004,skolem0003,xR)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|sdtmndtplgtdt0(skolem0004,xR,xc)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=xc|sdtmndtplgtdt0(skolem0003,xR,xc)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0003,xR,xc)))&(((((((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0005))&(((((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aElement0(skolem0006))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aReductOfIn0(skolem0006,skolem0001,xR)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|sdtmndtplgtdt0(skolem0006,xR,skolem0005)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=skolem0005|sdtmndtplgtdt0(skolem0001,xR,skolem0005)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0001,xR,skolem0005)))&(((((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aElement0(skolem0007))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aReductOfIn0(skolem0007,skolem0003,xR)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|sdtmndtplgtdt0(skolem0007,xR,skolem0005)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=skolem0005|sdtmndtplgtdt0(skolem0003,xR,skolem0005)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0003,xR,skolem0005)))&((((((((((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0008))&(((((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aElement0(skolem0009))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aReductOfIn0(skolem0009,skolem0005,xR)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|sdtmndtplgtdt0(skolem0009,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0005=skolem0008|sdtmndtplgtdt0(skolem0005,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0005,xR,skolem0008)))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|~aReductOfIn0(X13,skolem0008,xR)))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|aNormalFormOfIn0(skolem0008,skolem0005,xR)))&(((((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aElement0(skolem0010))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aReductOfIn0(skolem0010,xb,xR)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|sdtmndtplgtdt0(skolem0010,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(xb=skolem0008|sdtmndtplgtdt0(xb,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(xb,xR,skolem0008)))&(((((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aElement0(skolem0011))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aReductOfIn0(skolem0011,xc,xR)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|sdtmndtplgtdt0(skolem0011,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|(xc=skolem0008|sdtmndtplgtdt0(xc,xR,skolem0008)))))&((~aReductOfIn0(xb,xa,xR)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(xc,xR,skolem0008)))))))&((((((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|aElement0(skolem0001))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|aReductOfIn0(skolem0001,xa,xR)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aElement0(skolem0002))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aReductOfIn0(skolem0002,skolem0001,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|sdtmndtplgtdt0(skolem0002,xR,xb)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0001=xb|sdtmndtplgtdt0(skolem0001,xR,xb)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0001,xR,xb)))&((((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|aElement0(skolem0003))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|aReductOfIn0(skolem0003,xa,xR)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aElement0(skolem0004))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aReductOfIn0(skolem0004,skolem0003,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|sdtmndtplgtdt0(skolem0004,xR,xc)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0003=xc|sdtmndtplgtdt0(skolem0003,xR,xc)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0003,xR,xc)))&(((((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|aElement0(skolem0005))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aElement0(skolem0006))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aReductOfIn0(skolem0006,skolem0001,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|sdtmndtplgtdt0(skolem0006,xR,skolem0005)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0001=skolem0005|sdtmndtplgtdt0(skolem0001,xR,skolem0005)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0001,xR,skolem0005)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aElement0(skolem0007))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aReductOfIn0(skolem0007,skolem0003,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|sdtmndtplgtdt0(skolem0007,xR,skolem0005)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0003=skolem0005|sdtmndtplgtdt0(skolem0003,xR,skolem0005)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0003,xR,skolem0005)))&((((((((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|aElement0(skolem0008))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aElement0(skolem0009))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aReductOfIn0(skolem0009,skolem0005,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|sdtmndtplgtdt0(skolem0009,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(skolem0005=skolem0008|sdtmndtplgtdt0(skolem0005,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0005,xR,skolem0008)))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|~aReductOfIn0(X13,skolem0008,xR)))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|aNormalFormOfIn0(skolem0008,skolem0005,xR)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aElement0(skolem0010))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aReductOfIn0(skolem0010,xb,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|sdtmndtplgtdt0(skolem0010,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(xb=skolem0008|sdtmndtplgtdt0(xb,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(xb,xR,skolem0008)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aElement0(skolem0011))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aReductOfIn0(skolem0011,xc,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|sdtmndtplgtdt0(skolem0011,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|(xc=skolem0008|sdtmndtplgtdt0(xc,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(xc,xR,skolem0008))))))&((((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aElement0(skolem0001))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aReductOfIn0(skolem0001,xa,xR)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aElement0(skolem0002))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aReductOfIn0(skolem0002,skolem0001,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|sdtmndtplgtdt0(skolem0002,xR,xb)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=xb|sdtmndtplgtdt0(skolem0001,xR,xb)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0001,xR,xb)))&((((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aElement0(skolem0003))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aReductOfIn0(skolem0003,xa,xR)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aElement0(skolem0004))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aReductOfIn0(skolem0004,skolem0003,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|sdtmndtplgtdt0(skolem0004,xR,xc)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=xc|sdtmndtplgtdt0(skolem0003,xR,xc)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0003,xR,xc)))&(((((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aElement0(skolem0005))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aElement0(skolem0006))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aReductOfIn0(skolem0006,skolem0001,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|sdtmndtplgtdt0(skolem0006,xR,skolem0005)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=skolem0005|sdtmndtplgtdt0(skolem0001,xR,skolem0005)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0001,xR,skolem0005)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aElement0(skolem0007))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aReductOfIn0(skolem0007,skolem0003,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|sdtmndtplgtdt0(skolem0007,xR,skolem0005)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=skolem0005|sdtmndtplgtdt0(skolem0003,xR,skolem0005)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0003,xR,skolem0005)))&((((((((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aElement0(skolem0008))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aElement0(skolem0009))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aReductOfIn0(skolem0009,skolem0005,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|sdtmndtplgtdt0(skolem0009,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0005=skolem0008|sdtmndtplgtdt0(skolem0005,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0005,xR,skolem0008)))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|~aReductOfIn0(X13,skolem0008,xR)))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aNormalFormOfIn0(skolem0008,skolem0005,xR)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aElement0(skolem0010))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aReductOfIn0(skolem0010,xb,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|sdtmndtplgtdt0(skolem0010,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xb=skolem0008|sdtmndtplgtdt0(xb,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(xb,xR,skolem0008)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aElement0(skolem0011))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aReductOfIn0(skolem0011,xc,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|sdtmndtplgtdt0(skolem0011,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xc=skolem0008|sdtmndtplgtdt0(xc,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(xc,xR,skolem0008)))))))&((((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0001))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|aReductOfIn0(skolem0001,xa,xR)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aElement0(skolem0002))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aReductOfIn0(skolem0002,skolem0001,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|sdtmndtplgtdt0(skolem0002,xR,xb)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=xb|sdtmndtplgtdt0(skolem0001,xR,xb)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0001,xR,xb)))&((((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0003))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|aReductOfIn0(skolem0003,xa,xR)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aElement0(skolem0004))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aReductOfIn0(skolem0004,skolem0003,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|sdtmndtplgtdt0(skolem0004,xR,xc)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=xc|sdtmndtplgtdt0(skolem0003,xR,xc)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0003,xR,xc)))&(((((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0005))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aElement0(skolem0006))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aReductOfIn0(skolem0006,skolem0001,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|sdtmndtplgtdt0(skolem0006,xR,skolem0005)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=skolem0005|sdtmndtplgtdt0(skolem0001,xR,skolem0005)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0001,xR,skolem0005)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aElement0(skolem0007))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aReductOfIn0(skolem0007,skolem0003,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|sdtmndtplgtdt0(skolem0007,xR,skolem0005)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=skolem0005|sdtmndtplgtdt0(skolem0003,xR,skolem0005)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0003,xR,skolem0005)))&((((((((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0008))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aElement0(skolem0009))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aReductOfIn0(skolem0009,skolem0005,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|sdtmndtplgtdt0(skolem0009,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0005=skolem0008|sdtmndtplgtdt0(skolem0005,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0005,xR,skolem0008)))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|~aReductOfIn0(X13,skolem0008,xR)))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|aNormalFormOfIn0(skolem0008,skolem0005,xR)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aElement0(skolem0010))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aReductOfIn0(skolem0010,xb,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|sdtmndtplgtdt0(skolem0010,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(xb=skolem0008|sdtmndtplgtdt0(xb,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(xb,xR,skolem0008)))&(((((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aElement0(skolem0011))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aReductOfIn0(skolem0011,xc,xR)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|sdtmndtplgtdt0(skolem0011,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|(xc=skolem0008|sdtmndtplgtdt0(xc,xR,skolem0008)))))&((((~aElement0(X2)|~aReductOfIn0(X2,xa,xR))|~sdtmndtplgtdt0(X2,xR,xb))|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(xc,xR,skolem0008))))))))&((((((((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|aElement0(skolem0001))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|aReductOfIn0(skolem0001,xa,xR)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aElement0(skolem0002))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aReductOfIn0(skolem0002,skolem0001,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|sdtmndtplgtdt0(skolem0002,xR,xb)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0001=xb|sdtmndtplgtdt0(skolem0001,xR,xb)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0001,xR,xb)))&((((((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|aElement0(skolem0003))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|aReductOfIn0(skolem0003,xa,xR)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aElement0(skolem0004))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aReductOfIn0(skolem0004,skolem0003,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|sdtmndtplgtdt0(skolem0004,xR,xc)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0003=xc|sdtmndtplgtdt0(skolem0003,xR,xc)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0003,xR,xc)))&(((((((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|aElement0(skolem0005))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aElement0(skolem0006))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aReductOfIn0(skolem0006,skolem0001,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|sdtmndtplgtdt0(skolem0006,xR,skolem0005)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0001=skolem0005|sdtmndtplgtdt0(skolem0001,xR,skolem0005)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0001,xR,skolem0005)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aElement0(skolem0007))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aReductOfIn0(skolem0007,skolem0003,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|sdtmndtplgtdt0(skolem0007,xR,skolem0005)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0003=skolem0005|sdtmndtplgtdt0(skolem0003,xR,skolem0005)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0003,xR,skolem0005)))&((((((((((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|aElement0(skolem0008))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aElement0(skolem0009))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aReductOfIn0(skolem0009,skolem0005,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|sdtmndtplgtdt0(skolem0009,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(skolem0005=skolem0008|sdtmndtplgtdt0(skolem0005,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(skolem0005,xR,skolem0008)))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|~aReductOfIn0(X13,skolem0008,xR)))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|aNormalFormOfIn0(skolem0008,skolem0005,xR)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aElement0(skolem0010))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aReductOfIn0(skolem0010,xb,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|sdtmndtplgtdt0(skolem0010,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(xb=skolem0008|sdtmndtplgtdt0(xb,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(xb,xR,skolem0008)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aElement0(skolem0011))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aReductOfIn0(skolem0011,xc,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|sdtmndtplgtdt0(skolem0011,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|(xc=skolem0008|sdtmndtplgtdt0(xc,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~aReductOfIn0(xc,xa,xR))|sdtmndtasgtdt0(xc,xR,skolem0008))))))&((((((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aElement0(skolem0001))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aReductOfIn0(skolem0001,xa,xR)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aElement0(skolem0002))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aReductOfIn0(skolem0002,skolem0001,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|sdtmndtplgtdt0(skolem0002,xR,xb)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=xb|sdtmndtplgtdt0(skolem0001,xR,xb)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0001,xR,xb)))&((((((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aElement0(skolem0003))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aReductOfIn0(skolem0003,xa,xR)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aElement0(skolem0004))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aReductOfIn0(skolem0004,skolem0003,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|sdtmndtplgtdt0(skolem0004,xR,xc)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=xc|sdtmndtplgtdt0(skolem0003,xR,xc)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0003,xR,xc)))&(((((((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aElement0(skolem0005))&(((((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aElement0(skolem0006))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aReductOfIn0(skolem0006,skolem0001,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|sdtmndtplgtdt0(skolem0006,xR,skolem0005)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0001=skolem0005|sdtmndtplgtdt0(skolem0001,xR,skolem0005)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0001,xR,skolem0005)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aElement0(skolem0007))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aReductOfIn0(skolem0007,skolem0003,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|sdtmndtplgtdt0(skolem0007,xR,skolem0005)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0003=skolem0005|sdtmndtplgtdt0(skolem0003,xR,skolem0005)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0003,xR,skolem0005)))&((((((((((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aElement0(skolem0008))&(((((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aElement0(skolem0009))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aReductOfIn0(skolem0009,skolem0005,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|sdtmndtplgtdt0(skolem0009,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(skolem0005=skolem0008|sdtmndtplgtdt0(skolem0005,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(skolem0005,xR,skolem0008)))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|~aReductOfIn0(X13,skolem0008,xR)))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|aNormalFormOfIn0(skolem0008,skolem0005,xR)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aElement0(skolem0010))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aReductOfIn0(skolem0010,xb,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|sdtmndtplgtdt0(skolem0010,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xb=skolem0008|sdtmndtplgtdt0(xb,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(xb,xR,skolem0008)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aElement0(skolem0011))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aReductOfIn0(skolem0011,xc,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|sdtmndtplgtdt0(skolem0011,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|(xc=skolem0008|sdtmndtplgtdt0(xc,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|((~aElement0(X3)|~aReductOfIn0(X3,xa,xR))|~sdtmndtplgtdt0(X3,xR,xc)))|sdtmndtasgtdt0(xc,xR,skolem0008)))))))&((((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0001))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|aReductOfIn0(skolem0001,xa,xR)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aElement0(skolem0002))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|aReductOfIn0(skolem0002,skolem0001,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=xb|(aReductOfIn0(xb,skolem0001,xR)|sdtmndtplgtdt0(skolem0002,xR,xb)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=xb|sdtmndtplgtdt0(skolem0001,xR,xb)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0001,xR,xb)))&((((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0003))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|aReductOfIn0(skolem0003,xa,xR)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aElement0(skolem0004))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|aReductOfIn0(skolem0004,skolem0003,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=xc|(aReductOfIn0(xc,skolem0003,xR)|sdtmndtplgtdt0(skolem0004,xR,xc)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=xc|sdtmndtplgtdt0(skolem0003,xR,xc)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0003,xR,xc)))&(((((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0005))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aElement0(skolem0006))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|aReductOfIn0(skolem0006,skolem0001,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=skolem0005|(aReductOfIn0(skolem0005,skolem0001,xR)|sdtmndtplgtdt0(skolem0006,xR,skolem0005)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0001=skolem0005|sdtmndtplgtdt0(skolem0001,xR,skolem0005)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0001,xR,skolem0005)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aElement0(skolem0007))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|aReductOfIn0(skolem0007,skolem0003,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=skolem0005|(aReductOfIn0(skolem0005,skolem0003,xR)|sdtmndtplgtdt0(skolem0007,xR,skolem0005)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0003=skolem0005|sdtmndtplgtdt0(skolem0003,xR,skolem0005)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0003,xR,skolem0005)))&((((((((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|aElement0(skolem0008))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aElement0(skolem0009))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|aReductOfIn0(skolem0009,skolem0005,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0005=skolem0008|(aReductOfIn0(skolem0008,skolem0005,xR)|sdtmndtplgtdt0(skolem0009,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(skolem0005=skolem0008|sdtmndtplgtdt0(skolem0005,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(skolem0005,xR,skolem0008)))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|~aReductOfIn0(X13,skolem0008,xR)))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|aNormalFormOfIn0(skolem0008,skolem0005,xR)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aElement0(skolem0010))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|aReductOfIn0(skolem0010,xb,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(xb=skolem0008|(aReductOfIn0(skolem0008,xb,xR)|sdtmndtplgtdt0(skolem0010,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(xb=skolem0008|sdtmndtplgtdt0(xb,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(xb,xR,skolem0008)))&(((((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aElement0(skolem0011))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|aReductOfIn0(skolem0011,xc,xR)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(xc=skolem0008|(aReductOfIn0(skolem0008,xc,xR)|sdtmndtplgtdt0(skolem0011,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(xc=skolem0008|sdtmndtplgtdt0(xc,xR,skolem0008)))))&((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|sdtmndtasgtdt0(xc,xR,skolem0008))))))))&((((((((xa=xb|(aReductOfIn0(xb,xa,xR)|aElement0(skolem0012)))&(xa=xb|(aReductOfIn0(xb,xa,xR)|aReductOfIn0(skolem0012,xa,xR))))&(xa=xb|(aReductOfIn0(xb,xa,xR)|sdtmndtplgtdt0(skolem0012,xR,xb))))&(xa=xb|sdtmndtplgtdt0(xa,xR,xb)))&sdtmndtasgtdt0(xa,xR,xb))&((((xa=xc|(aReductOfIn0(xc,xa,xR)|aElement0(skolem0013)))&(xa=xc|(aReductOfIn0(xc,xa,xR)|aReductOfIn0(skolem0013,xa,xR))))&(xa=xc|(aReductOfIn0(xc,xa,xR)|sdtmndtplgtdt0(skolem0013,xR,xc))))&(xa=xc|sdtmndtplgtdt0(xa,xR,xc))))&sdtmndtasgtdt0(xa,xR,xc))&((((((((((~aElement0(X18)|xb!=X18)|xc!=X18)&((~aElement0(X18)|xb!=X18)|~aReductOfIn0(X18,xc,xR)))&((~aElement0(X18)|xb!=X18)|((~aElement0(X20)|~aReductOfIn0(X20,xc,xR))|~sdtmndtplgtdt0(X20,xR,X18))))&((~aElement0(X18)|xb!=X18)|~sdtmndtplgtdt0(xc,xR,X18)))&((~aElement0(X18)|xb!=X18)|~sdtmndtasgtdt0(xc,xR,X18)))&((((((~aElement0(X18)|~aReductOfIn0(X18,xb,xR))|xc!=X18)&((~aElement0(X18)|~aReductOfIn0(X18,xb,xR))|~aReductOfIn0(X18,xc,xR)))&((~aElement0(X18)|~aReductOfIn0(X18,xb,xR))|((~aElement0(X20)|~aReductOfIn0(X20,xc,xR))|~sdtmndtplgtdt0(X20,xR,X18))))&((~aElement0(X18)|~aReductOfIn0(X18,xb,xR))|~sdtmndtplgtdt0(xc,xR,X18)))&((~aElement0(X18)|~aReductOfIn0(X18,xb,xR))|~sdtmndtasgtdt0(xc,xR,X18))))&((((((~aElement0(X18)|((~aElement0(X19)|~aReductOfIn0(X19,xb,xR))|~sdtmndtplgtdt0(X19,xR,X18)))|xc!=X18)&((~aElement0(X18)|((~aElement0(X19)|~aReductOfIn0(X19,xb,xR))|~sdtmndtplgtdt0(X19,xR,X18)))|~aReductOfIn0(X18,xc,xR)))&((~aElement0(X18)|((~aElement0(X19)|~aReductOfIn0(X19,xb,xR))|~sdtmndtplgtdt0(X19,xR,X18)))|((~aElement0(X20)|~aReductOfIn0(X20,xc,xR))|~sdtmndtplgtdt0(X20,xR,X18))))&((~aElement0(X18)|((~aElement0(X19)|~aReductOfIn0(X19,xb,xR))|~sdtmndtplgtdt0(X19,xR,X18)))|~sdtmndtplgtdt0(xc,xR,X18)))&((~aElement0(X18)|((~aElement0(X19)|~aReductOfIn0(X19,xb,xR))|~sdtmndtplgtdt0(X19,xR,X18)))|~sdtmndtasgtdt0(xc,xR,X18))))&((((((~aElement0(X18)|~sdtmndtplgtdt0(xb,xR,X18))|xc!=X18)&((~aElement0(X18)|~sdtmndtplgtdt0(xb,xR,X18))|~aReductOfIn0(X18,xc,xR)))&((~aElement0(X18)|~sdtmndtplgtdt0(xb,xR,X18))|((~aElement0(X20)|~aReductOfIn0(X20,xc,xR))|~sdtmndtplgtdt0(X20,xR,X18))))&((~aElement0(X18)|~sdtmndtplgtdt0(xb,xR,X18))|~sdtmndtplgtdt0(xc,xR,X18)))&((~aElement0(X18)|~sdtmndtplgtdt0(xb,xR,X18))|~sdtmndtasgtdt0(xc,xR,X18))))&((((((~aElement0(X18)|~sdtmndtasgtdt0(xb,xR,X18))|xc!=X18)&((~aElement0(X18)|~sdtmndtasgtdt0(xb,xR,X18))|~aReductOfIn0(X18,xc,xR)))&((~aElement0(X18)|~sdtmndtasgtdt0(xb,xR,X18))|((~aElement0(X20)|~aReductOfIn0(X20,xc,xR))|~sdtmndtplgtdt0(X20,xR,X18))))&((~aElement0(X18)|~sdtmndtasgtdt0(xb,xR,X18))|~sdtmndtplgtdt0(xc,xR,X18)))&((~aElement0(X18)|~sdtmndtasgtdt0(xb,xR,X18))|~sdtmndtasgtdt0(xc,xR,X18)))))))))))),inference(distribute,[status(thm)],[c14])).
% 5.11/5.32 cnf(c417,negated_conjecture,~aElement0(X160)|xb!=X160|~sdtmndtasgtdt0(xc,xR,X160),inference(split_conjunct,[status(thm)],[c15])).
% 5.11/5.32 cnf(c411,negated_conjecture,xa=xc|sdtmndtplgtdt0(xa,xR,xc),inference(split_conjunct,[status(thm)],[c15])).
% 5.11/5.32 cnf(c385,negated_conjecture,~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc)|aElement0(skolem0008),inference(split_conjunct,[status(thm)],[c15])).
% 5.11/5.32 cnf(c1470,plain,~sdtmndtplgtdt0(xa,xR,xb)|aElement0(skolem0008)|xa=xc,inference(resolution,[status(thm)],[c385, c411])).
% 5.11/5.32 cnf(c720,plain,aElement0(xc),inference(split_conjunct,[status(thm)],[m__731])).
% 5.11/5.32 cnf(c437,negated_conjecture,~aElement0(X188)|~sdtmndtasgtdt0(xb,xR,X188)|~sdtmndtasgtdt0(xc,xR,X188),inference(split_conjunct,[status(thm)],[c15])).
% 5.11/5.32 fof(m__656,plain,aRewritingSystem0(xR),file('/export/starexec/sandbox/benchmark/theBenchmark.p', m__656)).
% 5.11/5.32 cnf(c742,plain,aRewritingSystem0(xR),inference(split_conjunct,[status(thm)],[m__656])).
% 5.11/5.32 fof(mTCRDef,plain,(![W0]:(![W1]:(![W2]:(((aElement0(W0)&aRewritingSystem0(W1))&aElement0(W2))=>(sdtmndtasgtdt0(W0,W1,W2)<=>(W0=W2|sdtmndtplgtdt0(W0,W1,W2))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mTCRDef)).
% 5.11/5.32 fof(c799,plain,(![W0]:(![W1]:(![W2]:(((~aElement0(W0)|~aRewritingSystem0(W1))|~aElement0(W2))|((~sdtmndtasgtdt0(W0,W1,W2)|(W0=W2|sdtmndtplgtdt0(W0,W1,W2)))&((W0!=W2&~sdtmndtplgtdt0(W0,W1,W2))|sdtmndtasgtdt0(W0,W1,W2))))))),inference(fof_nnf,[status(thm)],[mTCRDef])).
% 5.11/5.32 fof(c800,plain,(![X74]:(![X75]:(![X76]:(((~aElement0(X74)|~aRewritingSystem0(X75))|~aElement0(X76))|((~sdtmndtasgtdt0(X74,X75,X76)|(X74=X76|sdtmndtplgtdt0(X74,X75,X76)))&((X74!=X76&~sdtmndtplgtdt0(X74,X75,X76))|sdtmndtasgtdt0(X74,X75,X76))))))),inference(variable_rename,[status(thm)],[c799])).
% 5.11/5.32 fof(c801,plain,(![X74]:(![X75]:(![X76]:((((~aElement0(X74)|~aRewritingSystem0(X75))|~aElement0(X76))|(~sdtmndtasgtdt0(X74,X75,X76)|(X74=X76|sdtmndtplgtdt0(X74,X75,X76))))&((((~aElement0(X74)|~aRewritingSystem0(X75))|~aElement0(X76))|(X74!=X76|sdtmndtasgtdt0(X74,X75,X76)))&(((~aElement0(X74)|~aRewritingSystem0(X75))|~aElement0(X76))|(~sdtmndtplgtdt0(X74,X75,X76)|sdtmndtasgtdt0(X74,X75,X76)))))))),inference(distribute,[status(thm)],[c800])).
% 5.11/5.32 cnf(c803,plain,~aElement0(X196)|~aRewritingSystem0(X195)|~aElement0(X194)|X196!=X194|sdtmndtasgtdt0(X196,X195,X194),inference(split_conjunct,[status(thm)],[c801])).
% 5.11/5.32 cnf(c964,plain,~aElement0(X198)|~aRewritingSystem0(X197)|sdtmndtasgtdt0(X198,X197,X198),inference(resolution,[status(thm)],[c803, reflexivity])).
% 5.11/5.32 cnf(c970,plain,~aElement0(X199)|sdtmndtasgtdt0(X199,xR,X199),inference(resolution,[status(thm)],[c964, c742])).
% 5.11/5.32 cnf(c977,plain,sdtmndtasgtdt0(xc,xR,xc),inference(resolution,[status(thm)],[c970, c720])).
% 5.11/5.32 cnf(c988,plain,~aElement0(xc)|~sdtmndtasgtdt0(xb,xR,xc),inference(resolution,[status(thm)],[c977, c437])).
% 5.11/5.32 cnf(c406,negated_conjecture,xa=xb|sdtmndtplgtdt0(xa,xR,xb),inference(split_conjunct,[status(thm)],[c15])).
% 5.11/5.32 cnf(c412,negated_conjecture,sdtmndtasgtdt0(xa,xR,xc),inference(split_conjunct,[status(thm)],[c15])).
% 5.11/5.32 cnf(c5,axiom,X139!=X135|X136!=X140|X137!=X138|~sdtmndtasgtdt0(X139,X136,X137)|sdtmndtasgtdt0(X135,X140,X138),theory(equality)).
% 5.11/5.32 cnf(c843,plain,xa!=X242|xR!=X240|xc!=X241|sdtmndtasgtdt0(X242,X240,X241),inference(resolution,[status(thm)],[c5, c412])).
% 5.11/5.32 cnf(c1594,plain,xa!=X243|xR!=X244|sdtmndtasgtdt0(X243,X244,xc),inference(resolution,[status(thm)],[c843, reflexivity])).
% 5.11/5.32 cnf(c1596,plain,xa!=X245|sdtmndtasgtdt0(X245,xR,xc),inference(resolution,[status(thm)],[c1594, reflexivity])).
% 5.11/5.32 cnf(c1598,plain,sdtmndtasgtdt0(xb,xR,xc)|sdtmndtplgtdt0(xa,xR,xb),inference(resolution,[status(thm)],[c1596, c406])).
% 5.11/5.32 cnf(c1620,plain,sdtmndtplgtdt0(xa,xR,xb)|~aElement0(xc),inference(resolution,[status(thm)],[c1598, c988])).
% 5.11/5.32 cnf(c1634,plain,sdtmndtplgtdt0(xa,xR,xb),inference(resolution,[status(thm)],[c1620, c720])).
% 5.11/5.32 cnf(c1643,plain,aElement0(skolem0008)|xa=xc,inference(resolution,[status(thm)],[c1634, c1470])).
% 5.11/5.32 cnf(c407,negated_conjecture,sdtmndtasgtdt0(xa,xR,xb),inference(split_conjunct,[status(thm)],[c15])).
% 5.11/5.32 cnf(c844,plain,xa!=X341|xR!=X339|xb!=X340|sdtmndtasgtdt0(X341,X339,X340),inference(resolution,[status(thm)],[c5, c407])).
% 5.11/5.32 cnf(c2392,plain,xa!=X344|xR!=X343|sdtmndtasgtdt0(X344,X343,xb),inference(resolution,[status(thm)],[c844, reflexivity])).
% 5.11/5.32 cnf(c2397,plain,xa!=X345|sdtmndtasgtdt0(X345,xR,xb),inference(resolution,[status(thm)],[c2392, reflexivity])).
% 5.11/5.32 cnf(c2408,plain,sdtmndtasgtdt0(xc,xR,xb)|aElement0(skolem0008),inference(resolution,[status(thm)],[c2397, c1643])).
% 5.11/5.32 cnf(c2434,plain,aElement0(skolem0008)|~aElement0(xb)|xb!=xb,inference(resolution,[status(thm)],[c2408, c417])).
% 5.11/5.32 cnf(c2462,plain,aElement0(skolem0008)|~aElement0(xb),inference(resolution,[status(thm)],[c2434, reflexivity])).
% 5.11/5.32 cnf(c2466,plain,aElement0(skolem0008),inference(resolution,[status(thm)],[c2462, c719])).
% 5.11/5.32 cnf(c2409,plain,sdtmndtasgtdt0(xc,xR,xb)|sdtmndtplgtdt0(xa,xR,xc),inference(resolution,[status(thm)],[c2397, c411])).
% 5.11/5.32 cnf(c2473,plain,sdtmndtplgtdt0(xa,xR,xc)|~aElement0(xb)|xb!=xb,inference(resolution,[status(thm)],[c2409, c417])).
% 5.11/5.32 cnf(c2621,plain,sdtmndtplgtdt0(xa,xR,xc)|~aElement0(xb),inference(resolution,[status(thm)],[c2473, reflexivity])).
% 5.11/5.32 cnf(c2622,plain,sdtmndtplgtdt0(xa,xR,xc),inference(resolution,[status(thm)],[c2621, c719])).
% 5.11/5.32 cnf(c397,negated_conjecture,~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc)|sdtmndtasgtdt0(xb,xR,skolem0008),inference(split_conjunct,[status(thm)],[c15])).
% 5.11/5.32 cnf(c6488,plain,~sdtmndtplgtdt0(xa,xR,xb)|sdtmndtasgtdt0(xb,xR,skolem0008),inference(resolution,[status(thm)],[c397, c2622])).
% 5.11/5.32 cnf(c6489,plain,sdtmndtasgtdt0(xb,xR,skolem0008),inference(resolution,[status(thm)],[c6488, c1634])).
% 5.11/5.32 cnf(c402,negated_conjecture,~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc)|sdtmndtasgtdt0(xc,xR,skolem0008),inference(split_conjunct,[status(thm)],[c15])).
% 5.11/5.32 cnf(c6549,plain,~sdtmndtplgtdt0(xa,xR,xb)|sdtmndtasgtdt0(xc,xR,skolem0008),inference(resolution,[status(thm)],[c402, c2622])).
% 5.11/5.32 cnf(c6622,plain,sdtmndtasgtdt0(xc,xR,skolem0008),inference(resolution,[status(thm)],[c6549, c1634])).
% 5.11/5.32 cnf(c6626,plain,~aElement0(skolem0008)|~sdtmndtasgtdt0(xb,xR,skolem0008),inference(resolution,[status(thm)],[c6622, c437])).
% 5.11/5.32 cnf(c6628,plain,~aElement0(skolem0008),inference(resolution,[status(thm)],[c6626, c6489])).
% 5.11/5.32 cnf(c6629,plain,$false,inference(resolution,[status(thm)],[c6628, c2466])).
% 5.11/5.32 % SZS output end CNFRefutation
% 5.11/5.32
% 5.11/5.32 % Initial clauses : 773
% 5.11/5.32 % Processed clauses : 1233
% 5.11/5.32 % Factors computed : 52
% 5.11/5.32 % Resolvents computed: 5748
% 5.11/5.32 % Tautologies deleted: 11
% 5.11/5.32 % Forward subsumed : 1073
% 5.11/5.32 % Backward subsumed : 698
% 5.11/5.32 % -------- CPU Time ---------
% 5.11/5.32 % User time : 4.931 s
% 5.11/5.32 % System time : 0.036 s
% 5.11/5.32 % Total time : 4.967 s
%------------------------------------------------------------------------------