%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NUM558+3 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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:36:11 EDT 2024
% Result : Theorem 0.68s 0.88s
% Output : Refutation 0.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : NUM558+3 : TPTP v8.1.2. Released v4.0.0.
% 0.12/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n018.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 17:15:08 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.68/0.88 % Version: 1.5
% 0.68/0.88 % SZS status Theorem
% 0.68/0.88 % SZS output start CNFRefutation
% 0.68/0.88 fof(m__,conjecture,aElementOf0(xx,xT),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__)).
% 0.68/0.88 fof(c16,negated_conjecture,(~aElementOf0(xx,xT)),inference(assume_negation,[status(cth)],[m__])).
% 0.68/0.88 fof(c17,negated_conjecture,~aElementOf0(xx,xT),inference(fof_simplification,[status(thm)],[c16])).
% 0.68/0.88 cnf(c18,negated_conjecture,~aElementOf0(xx,xT),inference(split_conjunct,[status(thm)],[c17])).
% 0.68/0.88 fof(m__2202_02,plain,((aSet0(xS)&aSet0(xT))&xk!=sz00),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2202_02)).
% 0.68/0.88 cnf(c93,plain,aSet0(xS),inference(split_conjunct,[status(thm)],[m__2202_02])).
% 0.68/0.88 fof(m__2256,plain,aElementOf0(xx,xS),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2256)).
% 0.68/0.88 cnf(c59,plain,aElementOf0(xx,xS),inference(split_conjunct,[status(thm)],[m__2256])).
% 0.68/0.88 fof(mEOfElem,axiom,(![W0]:(aSet0(W0)=>(![W1]:(aElementOf0(W1,W0)=>aElement0(W1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mEOfElem)).
% 0.68/0.88 fof(c367,plain,(![W0]:(~aSet0(W0)|(![W1]:(~aElementOf0(W1,W0)|aElement0(W1))))),inference(fof_nnf,[status(thm)],[mEOfElem])).
% 0.68/0.88 fof(c369,plain,(![X138]:(![X139]:(~aSet0(X138)|(~aElementOf0(X139,X138)|aElement0(X139))))),inference(shift_quantors,[status(thm)],[fof(c368,plain,(![X138]:(~aSet0(X138)|(![X139]:(~aElementOf0(X139,X138)|aElement0(X139))))),inference(variable_rename,[status(thm)],[c367])).])).
% 0.68/0.88 cnf(c370,plain,~aSet0(X221)|~aElementOf0(X220,X221)|aElement0(X220),inference(split_conjunct,[status(thm)],[c369])).
% 0.68/0.88 cnf(c549,plain,~aSet0(xS)|aElement0(xx),inference(resolution,[status(thm)],[c370, c59])).
% 0.68/0.88 cnf(c555,plain,aElement0(xx),inference(resolution,[status(thm)],[c549, c93])).
% 0.68/0.88 cnf(reflexivity,axiom,X140=X140,theory(equality)).
% 0.68/0.88 fof(m__2357,plain,((((aSet0(sdtmndt0(xQ,xy))&(![W0]:(aElementOf0(W0,sdtmndt0(xQ,xy))<=>((aElement0(W0)&aElementOf0(W0,xQ))&W0!=xy))))&aSet0(xP))&(![W0]:(aElementOf0(W0,xP)<=>(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xQ,xy))|W0=xx)))))&xP=sdtpldt0(sdtmndt0(xQ,xy),xx)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2357)).
% 0.68/0.88 fof(c26,plain,((((aSet0(sdtmndt0(xQ,xy))&(![W0]:((~aElementOf0(W0,sdtmndt0(xQ,xy))|((aElement0(W0)&aElementOf0(W0,xQ))&W0!=xy))&(((~aElement0(W0)|~aElementOf0(W0,xQ))|W0=xy)|aElementOf0(W0,sdtmndt0(xQ,xy))))))&aSet0(xP))&(![W0]:((~aElementOf0(W0,xP)|(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xQ,xy))|W0=xx)))&((~aElement0(W0)|(~aElementOf0(W0,sdtmndt0(xQ,xy))&W0!=xx))|aElementOf0(W0,xP)))))&xP=sdtpldt0(sdtmndt0(xQ,xy),xx)),inference(fof_nnf,[status(thm)],[m__2357])).
% 0.68/0.88 fof(c27,plain,((((aSet0(sdtmndt0(xQ,xy))&((![W0]:(~aElementOf0(W0,sdtmndt0(xQ,xy))|((aElement0(W0)&aElementOf0(W0,xQ))&W0!=xy)))&(![W0]:(((~aElement0(W0)|~aElementOf0(W0,xQ))|W0=xy)|aElementOf0(W0,sdtmndt0(xQ,xy))))))&aSet0(xP))&((![W0]:(~aElementOf0(W0,xP)|(aElement0(W0)&(aElementOf0(W0,sdtmndt0(xQ,xy))|W0=xx))))&(![W0]:((~aElement0(W0)|(~aElementOf0(W0,sdtmndt0(xQ,xy))&W0!=xx))|aElementOf0(W0,xP)))))&xP=sdtpldt0(sdtmndt0(xQ,xy),xx)),inference(shift_quantors,[status(thm)],[c26])).
% 0.68/0.88 fof(c29,plain,(![X3]:(![X4]:(![X5]:(![X6]:((((aSet0(sdtmndt0(xQ,xy))&((~aElementOf0(X3,sdtmndt0(xQ,xy))|((aElement0(X3)&aElementOf0(X3,xQ))&X3!=xy))&(((~aElement0(X4)|~aElementOf0(X4,xQ))|X4=xy)|aElementOf0(X4,sdtmndt0(xQ,xy)))))&aSet0(xP))&((~aElementOf0(X5,xP)|(aElement0(X5)&(aElementOf0(X5,sdtmndt0(xQ,xy))|X5=xx)))&((~aElement0(X6)|(~aElementOf0(X6,sdtmndt0(xQ,xy))&X6!=xx))|aElementOf0(X6,xP))))&xP=sdtpldt0(sdtmndt0(xQ,xy),xx)))))),inference(shift_quantors,[status(thm)],[fof(c28,plain,((((aSet0(sdtmndt0(xQ,xy))&((![X3]:(~aElementOf0(X3,sdtmndt0(xQ,xy))|((aElement0(X3)&aElementOf0(X3,xQ))&X3!=xy)))&(![X4]:(((~aElement0(X4)|~aElementOf0(X4,xQ))|X4=xy)|aElementOf0(X4,sdtmndt0(xQ,xy))))))&aSet0(xP))&((![X5]:(~aElementOf0(X5,xP)|(aElement0(X5)&(aElementOf0(X5,sdtmndt0(xQ,xy))|X5=xx))))&(![X6]:((~aElement0(X6)|(~aElementOf0(X6,sdtmndt0(xQ,xy))&X6!=xx))|aElementOf0(X6,xP)))))&xP=sdtpldt0(sdtmndt0(xQ,xy),xx)),inference(variable_rename,[status(thm)],[c27])).])).
% 0.68/0.88 fof(c30,plain,(![X3]:(![X4]:(![X5]:(![X6]:((((aSet0(sdtmndt0(xQ,xy))&((((~aElementOf0(X3,sdtmndt0(xQ,xy))|aElement0(X3))&(~aElementOf0(X3,sdtmndt0(xQ,xy))|aElementOf0(X3,xQ)))&(~aElementOf0(X3,sdtmndt0(xQ,xy))|X3!=xy))&(((~aElement0(X4)|~aElementOf0(X4,xQ))|X4=xy)|aElementOf0(X4,sdtmndt0(xQ,xy)))))&aSet0(xP))&(((~aElementOf0(X5,xP)|aElement0(X5))&(~aElementOf0(X5,xP)|(aElementOf0(X5,sdtmndt0(xQ,xy))|X5=xx)))&(((~aElement0(X6)|~aElementOf0(X6,sdtmndt0(xQ,xy)))|aElementOf0(X6,xP))&((~aElement0(X6)|X6!=xx)|aElementOf0(X6,xP)))))&xP=sdtpldt0(sdtmndt0(xQ,xy),xx)))))),inference(distribute,[status(thm)],[c29])).
% 0.68/0.88 cnf(c40,plain,~aElement0(X227)|X227!=xx|aElementOf0(X227,xP),inference(split_conjunct,[status(thm)],[c30])).
% 0.68/0.88 cnf(c559,plain,~aElement0(xx)|aElementOf0(xx,xP),inference(resolution,[status(thm)],[c40, reflexivity])).
% 0.68/0.88 cnf(c590,plain,aElementOf0(xx,xP),inference(resolution,[status(thm)],[c559, c555])).
% 0.68/0.88 fof(m__2227,plain,((((((aSet0(slbdtsldtrb0(xS,xk))&(![W0]:((aElementOf0(W0,slbdtsldtrb0(xS,xk))=>(((aSet0(W0)&(![W1]:(aElementOf0(W1,W0)=>aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xk))&((((aSet0(W0)&(![W1]:(aElementOf0(W1,W0)=>aElementOf0(W1,xS))))|aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xk)=>aElementOf0(W0,slbdtsldtrb0(xS,xk))))))&aSet0(slbdtsldtrb0(xT,xk)))&(![W0]:((aElementOf0(W0,slbdtsldtrb0(xT,xk))=>(((aSet0(W0)&(![W1]:(aElementOf0(W1,W0)=>aElementOf0(W1,xT))))&aSubsetOf0(W0,xT))&sbrdtbr0(W0)=xk))&((((aSet0(W0)&(![W1]:(aElementOf0(W1,W0)=>aElementOf0(W1,xT))))|aSubsetOf0(W0,xT))&sbrdtbr0(W0)=xk)=>aElementOf0(W0,slbdtsldtrb0(xT,xk))))))&(![W0]:(aElementOf0(W0,slbdtsldtrb0(xS,xk))=>aElementOf0(W0,slbdtsldtrb0(xT,xk)))))&aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk)))&(~((![W0]:((aElementOf0(W0,slbdtsldtrb0(xS,xk))=>(((aSet0(W0)&(![W1]:(aElementOf0(W1,W0)=>aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xk))&((((aSet0(W0)&(![W1]:(aElementOf0(W1,W0)=>aElementOf0(W1,xS))))|aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xk)=>aElementOf0(W0,slbdtsldtrb0(xS,xk)))))=>((~(?[W0]:aElementOf0(W0,slbdtsldtrb0(xS,xk))))|slbdtsldtrb0(xS,xk)=slcrc0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2227)).
% 0.68/0.88 fof(c60,plain,((((((aSet0(slbdtsldtrb0(xS,xk))&(![W0]:((~aElementOf0(W0,slbdtsldtrb0(xS,xk))|(((aSet0(W0)&(![W1]:(~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xk))&((((~aSet0(W0)|(?[W1]:(aElementOf0(W1,W0)&~aElementOf0(W1,xS))))&~aSubsetOf0(W0,xS))|sbrdtbr0(W0)!=xk)|aElementOf0(W0,slbdtsldtrb0(xS,xk))))))&aSet0(slbdtsldtrb0(xT,xk)))&(![W0]:((~aElementOf0(W0,slbdtsldtrb0(xT,xk))|(((aSet0(W0)&(![W1]:(~aElementOf0(W1,W0)|aElementOf0(W1,xT))))&aSubsetOf0(W0,xT))&sbrdtbr0(W0)=xk))&((((~aSet0(W0)|(?[W1]:(aElementOf0(W1,W0)&~aElementOf0(W1,xT))))&~aSubsetOf0(W0,xT))|sbrdtbr0(W0)!=xk)|aElementOf0(W0,slbdtsldtrb0(xT,xk))))))&(![W0]:(~aElementOf0(W0,slbdtsldtrb0(xS,xk))|aElementOf0(W0,slbdtsldtrb0(xT,xk)))))&aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk)))&((![W0]:((~aElementOf0(W0,slbdtsldtrb0(xS,xk))|(((aSet0(W0)&(![W1]:(~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xk))&((((~aSet0(W0)|(?[W1]:(aElementOf0(W1,W0)&~aElementOf0(W1,xS))))&~aSubsetOf0(W0,xS))|sbrdtbr0(W0)!=xk)|aElementOf0(W0,slbdtsldtrb0(xS,xk)))))&((?[W0]:aElementOf0(W0,slbdtsldtrb0(xS,xk)))&slbdtsldtrb0(xS,xk)!=slcrc0))),inference(fof_nnf,[status(thm)],[m__2227])).
% 0.68/0.88 fof(c61,plain,((((((aSet0(slbdtsldtrb0(xS,xk))&((![W0]:(~aElementOf0(W0,slbdtsldtrb0(xS,xk))|(((aSet0(W0)&(![W1]:(~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xk)))&(![W0]:((((~aSet0(W0)|(?[W1]:(aElementOf0(W1,W0)&~aElementOf0(W1,xS))))&~aSubsetOf0(W0,xS))|sbrdtbr0(W0)!=xk)|aElementOf0(W0,slbdtsldtrb0(xS,xk))))))&aSet0(slbdtsldtrb0(xT,xk)))&((![W0]:(~aElementOf0(W0,slbdtsldtrb0(xT,xk))|(((aSet0(W0)&(![W1]:(~aElementOf0(W1,W0)|aElementOf0(W1,xT))))&aSubsetOf0(W0,xT))&sbrdtbr0(W0)=xk)))&(![W0]:((((~aSet0(W0)|(?[W1]:(aElementOf0(W1,W0)&~aElementOf0(W1,xT))))&~aSubsetOf0(W0,xT))|sbrdtbr0(W0)!=xk)|aElementOf0(W0,slbdtsldtrb0(xT,xk))))))&(![W0]:(~aElementOf0(W0,slbdtsldtrb0(xS,xk))|aElementOf0(W0,slbdtsldtrb0(xT,xk)))))&aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk)))&(((![W0]:(~aElementOf0(W0,slbdtsldtrb0(xS,xk))|(((aSet0(W0)&(![W1]:(~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=xk)))&(![W0]:((((~aSet0(W0)|(?[W1]:(aElementOf0(W1,W0)&~aElementOf0(W1,xS))))&~aSubsetOf0(W0,xS))|sbrdtbr0(W0)!=xk)|aElementOf0(W0,slbdtsldtrb0(xS,xk)))))&((?[W0]:aElementOf0(W0,slbdtsldtrb0(xS,xk)))&slbdtsldtrb0(xS,xk)!=slcrc0))),inference(shift_quantors,[status(thm)],[c60])).
% 0.68/0.88 fof(c62,plain,((((((aSet0(slbdtsldtrb0(xS,xk))&((![X8]:(~aElementOf0(X8,slbdtsldtrb0(xS,xk))|(((aSet0(X8)&(![X9]:(~aElementOf0(X9,X8)|aElementOf0(X9,xS))))&aSubsetOf0(X8,xS))&sbrdtbr0(X8)=xk)))&(![X10]:((((~aSet0(X10)|(?[X11]:(aElementOf0(X11,X10)&~aElementOf0(X11,xS))))&~aSubsetOf0(X10,xS))|sbrdtbr0(X10)!=xk)|aElementOf0(X10,slbdtsldtrb0(xS,xk))))))&aSet0(slbdtsldtrb0(xT,xk)))&((![X12]:(~aElementOf0(X12,slbdtsldtrb0(xT,xk))|(((aSet0(X12)&(![X13]:(~aElementOf0(X13,X12)|aElementOf0(X13,xT))))&aSubsetOf0(X12,xT))&sbrdtbr0(X12)=xk)))&(![X14]:((((~aSet0(X14)|(?[X15]:(aElementOf0(X15,X14)&~aElementOf0(X15,xT))))&~aSubsetOf0(X14,xT))|sbrdtbr0(X14)!=xk)|aElementOf0(X14,slbdtsldtrb0(xT,xk))))))&(![X16]:(~aElementOf0(X16,slbdtsldtrb0(xS,xk))|aElementOf0(X16,slbdtsldtrb0(xT,xk)))))&aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk)))&(((![X17]:(~aElementOf0(X17,slbdtsldtrb0(xS,xk))|(((aSet0(X17)&(![X18]:(~aElementOf0(X18,X17)|aElementOf0(X18,xS))))&aSubsetOf0(X17,xS))&sbrdtbr0(X17)=xk)))&(![X19]:((((~aSet0(X19)|(?[X20]:(aElementOf0(X20,X19)&~aElementOf0(X20,xS))))&~aSubsetOf0(X19,xS))|sbrdtbr0(X19)!=xk)|aElementOf0(X19,slbdtsldtrb0(xS,xk)))))&((?[X21]:aElementOf0(X21,slbdtsldtrb0(xS,xk)))&slbdtsldtrb0(xS,xk)!=slcrc0))),inference(variable_rename,[status(thm)],[c61])).
% 0.68/0.88 fof(c64,plain,(![X8]:(![X9]:(![X10]:(![X12]:(![X13]:(![X14]:(![X16]:(![X17]:(![X18]:(![X19]:((((((aSet0(slbdtsldtrb0(xS,xk))&((~aElementOf0(X8,slbdtsldtrb0(xS,xk))|(((aSet0(X8)&(~aElementOf0(X9,X8)|aElementOf0(X9,xS)))&aSubsetOf0(X8,xS))&sbrdtbr0(X8)=xk))&((((~aSet0(X10)|(aElementOf0(skolem0001(X10),X10)&~aElementOf0(skolem0001(X10),xS)))&~aSubsetOf0(X10,xS))|sbrdtbr0(X10)!=xk)|aElementOf0(X10,slbdtsldtrb0(xS,xk)))))&aSet0(slbdtsldtrb0(xT,xk)))&((~aElementOf0(X12,slbdtsldtrb0(xT,xk))|(((aSet0(X12)&(~aElementOf0(X13,X12)|aElementOf0(X13,xT)))&aSubsetOf0(X12,xT))&sbrdtbr0(X12)=xk))&((((~aSet0(X14)|(aElementOf0(skolem0002(X14),X14)&~aElementOf0(skolem0002(X14),xT)))&~aSubsetOf0(X14,xT))|sbrdtbr0(X14)!=xk)|aElementOf0(X14,slbdtsldtrb0(xT,xk)))))&(~aElementOf0(X16,slbdtsldtrb0(xS,xk))|aElementOf0(X16,slbdtsldtrb0(xT,xk))))&aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk)))&(((~aElementOf0(X17,slbdtsldtrb0(xS,xk))|(((aSet0(X17)&(~aElementOf0(X18,X17)|aElementOf0(X18,xS)))&aSubsetOf0(X17,xS))&sbrdtbr0(X17)=xk))&((((~aSet0(X19)|(aElementOf0(skolem0003(X19),X19)&~aElementOf0(skolem0003(X19),xS)))&~aSubsetOf0(X19,xS))|sbrdtbr0(X19)!=xk)|aElementOf0(X19,slbdtsldtrb0(xS,xk))))&(aElementOf0(skolem0004,slbdtsldtrb0(xS,xk))&slbdtsldtrb0(xS,xk)!=slcrc0))))))))))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,((((((aSet0(slbdtsldtrb0(xS,xk))&((![X8]:(~aElementOf0(X8,slbdtsldtrb0(xS,xk))|(((aSet0(X8)&(![X9]:(~aElementOf0(X9,X8)|aElementOf0(X9,xS))))&aSubsetOf0(X8,xS))&sbrdtbr0(X8)=xk)))&(![X10]:((((~aSet0(X10)|(aElementOf0(skolem0001(X10),X10)&~aElementOf0(skolem0001(X10),xS)))&~aSubsetOf0(X10,xS))|sbrdtbr0(X10)!=xk)|aElementOf0(X10,slbdtsldtrb0(xS,xk))))))&aSet0(slbdtsldtrb0(xT,xk)))&((![X12]:(~aElementOf0(X12,slbdtsldtrb0(xT,xk))|(((aSet0(X12)&(![X13]:(~aElementOf0(X13,X12)|aElementOf0(X13,xT))))&aSubsetOf0(X12,xT))&sbrdtbr0(X12)=xk)))&(![X14]:((((~aSet0(X14)|(aElementOf0(skolem0002(X14),X14)&~aElementOf0(skolem0002(X14),xT)))&~aSubsetOf0(X14,xT))|sbrdtbr0(X14)!=xk)|aElementOf0(X14,slbdtsldtrb0(xT,xk))))))&(![X16]:(~aElementOf0(X16,slbdtsldtrb0(xS,xk))|aElementOf0(X16,slbdtsldtrb0(xT,xk)))))&aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk)))&(((![X17]:(~aElementOf0(X17,slbdtsldtrb0(xS,xk))|(((aSet0(X17)&(![X18]:(~aElementOf0(X18,X17)|aElementOf0(X18,xS))))&aSubsetOf0(X17,xS))&sbrdtbr0(X17)=xk)))&(![X19]:((((~aSet0(X19)|(aElementOf0(skolem0003(X19),X19)&~aElementOf0(skolem0003(X19),xS)))&~aSubsetOf0(X19,xS))|sbrdtbr0(X19)!=xk)|aElementOf0(X19,slbdtsldtrb0(xS,xk)))))&(aElementOf0(skolem0004,slbdtsldtrb0(xS,xk))&slbdtsldtrb0(xS,xk)!=slcrc0))),inference(skolemize,[status(esa)],[c62])).])).
% 0.68/0.88 fof(c65,plain,(![X8]:(![X9]:(![X10]:(![X12]:(![X13]:(![X14]:(![X16]:(![X17]:(![X18]:(![X19]:((((((aSet0(slbdtsldtrb0(xS,xk))&(((((~aElementOf0(X8,slbdtsldtrb0(xS,xk))|aSet0(X8))&(~aElementOf0(X8,slbdtsldtrb0(xS,xk))|(~aElementOf0(X9,X8)|aElementOf0(X9,xS))))&(~aElementOf0(X8,slbdtsldtrb0(xS,xk))|aSubsetOf0(X8,xS)))&(~aElementOf0(X8,slbdtsldtrb0(xS,xk))|sbrdtbr0(X8)=xk))&(((((~aSet0(X10)|aElementOf0(skolem0001(X10),X10))|sbrdtbr0(X10)!=xk)|aElementOf0(X10,slbdtsldtrb0(xS,xk)))&(((~aSet0(X10)|~aElementOf0(skolem0001(X10),xS))|sbrdtbr0(X10)!=xk)|aElementOf0(X10,slbdtsldtrb0(xS,xk))))&((~aSubsetOf0(X10,xS)|sbrdtbr0(X10)!=xk)|aElementOf0(X10,slbdtsldtrb0(xS,xk))))))&aSet0(slbdtsldtrb0(xT,xk)))&(((((~aElementOf0(X12,slbdtsldtrb0(xT,xk))|aSet0(X12))&(~aElementOf0(X12,slbdtsldtrb0(xT,xk))|(~aElementOf0(X13,X12)|aElementOf0(X13,xT))))&(~aElementOf0(X12,slbdtsldtrb0(xT,xk))|aSubsetOf0(X12,xT)))&(~aElementOf0(X12,slbdtsldtrb0(xT,xk))|sbrdtbr0(X12)=xk))&(((((~aSet0(X14)|aElementOf0(skolem0002(X14),X14))|sbrdtbr0(X14)!=xk)|aElementOf0(X14,slbdtsldtrb0(xT,xk)))&(((~aSet0(X14)|~aElementOf0(skolem0002(X14),xT))|sbrdtbr0(X14)!=xk)|aElementOf0(X14,slbdtsldtrb0(xT,xk))))&((~aSubsetOf0(X14,xT)|sbrdtbr0(X14)!=xk)|aElementOf0(X14,slbdtsldtrb0(xT,xk))))))&(~aElementOf0(X16,slbdtsldtrb0(xS,xk))|aElementOf0(X16,slbdtsldtrb0(xT,xk))))&aSubsetOf0(slbdtsldtrb0(xS,xk),slbdtsldtrb0(xT,xk)))&((((((~aElementOf0(X17,slbdtsldtrb0(xS,xk))|aSet0(X17))&(~aElementOf0(X17,slbdtsldtrb0(xS,xk))|(~aElementOf0(X18,X17)|aElementOf0(X18,xS))))&(~aElementOf0(X17,slbdtsldtrb0(xS,xk))|aSubsetOf0(X17,xS)))&(~aElementOf0(X17,slbdtsldtrb0(xS,xk))|sbrdtbr0(X17)=xk))&(((((~aSet0(X19)|aElementOf0(skolem0003(X19),X19))|sbrdtbr0(X19)!=xk)|aElementOf0(X19,slbdtsldtrb0(xS,xk)))&(((~aSet0(X19)|~aElementOf0(skolem0003(X19),xS))|sbrdtbr0(X19)!=xk)|aElementOf0(X19,slbdtsldtrb0(xS,xk))))&((~aSubsetOf0(X19,xS)|sbrdtbr0(X19)!=xk)|aElementOf0(X19,slbdtsldtrb0(xS,xk)))))&(aElementOf0(skolem0004,slbdtsldtrb0(xS,xk))&slbdtsldtrb0(xS,xk)!=slcrc0))))))))))))),inference(distribute,[status(thm)],[c64])).
% 0.68/0.88 cnf(c76,plain,~aElementOf0(X243,slbdtsldtrb0(xT,xk))|~aElementOf0(X242,X243)|aElementOf0(X242,xT),inference(split_conjunct,[status(thm)],[c65])).
% 0.68/0.88 fof(m__2378,plain,((((![W0]:(aElementOf0(W0,xP)=>aElementOf0(W0,xS)))&aSubsetOf0(xP,xS))&sbrdtbr0(xP)=xk)&aElementOf0(xP,slbdtsldtrb0(xS,xk))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', m__2378)).
% 0.68/0.88 fof(c19,plain,((((![W0]:(~aElementOf0(W0,xP)|aElementOf0(W0,xS)))&aSubsetOf0(xP,xS))&sbrdtbr0(xP)=xk)&aElementOf0(xP,slbdtsldtrb0(xS,xk))),inference(fof_nnf,[status(thm)],[m__2378])).
% 0.68/0.88 fof(c21,plain,(![X2]:((((~aElementOf0(X2,xP)|aElementOf0(X2,xS))&aSubsetOf0(xP,xS))&sbrdtbr0(xP)=xk)&aElementOf0(xP,slbdtsldtrb0(xS,xk)))),inference(shift_quantors,[status(thm)],[fof(c20,plain,((((![X2]:(~aElementOf0(X2,xP)|aElementOf0(X2,xS)))&aSubsetOf0(xP,xS))&sbrdtbr0(xP)=xk)&aElementOf0(xP,slbdtsldtrb0(xS,xk))),inference(variable_rename,[status(thm)],[c19])).])).
% 0.68/0.88 cnf(c25,plain,aElementOf0(xP,slbdtsldtrb0(xS,xk)),inference(split_conjunct,[status(thm)],[c21])).
% 0.68/0.88 cnf(c82,plain,~aElementOf0(X254,slbdtsldtrb0(xS,xk))|aElementOf0(X254,slbdtsldtrb0(xT,xk)),inference(split_conjunct,[status(thm)],[c65])).
% 0.68/0.88 cnf(c708,plain,aElementOf0(xP,slbdtsldtrb0(xT,xk)),inference(resolution,[status(thm)],[c82, c25])).
% 0.68/0.88 cnf(c729,plain,~aElementOf0(X261,xP)|aElementOf0(X261,xT),inference(resolution,[status(thm)],[c708, c76])).
% 0.68/0.88 cnf(c742,plain,aElementOf0(xx,xT),inference(resolution,[status(thm)],[c729, c590])).
% 0.68/0.88 cnf(c743,plain,$false,inference(resolution,[status(thm)],[c742, c18])).
% 0.68/0.88 % SZS output end CNFRefutation
% 0.68/0.88
% 0.68/0.88 % Initial clauses : 189
% 0.68/0.88 % Processed clauses : 196
% 0.68/0.88 % Factors computed : 6
% 0.68/0.88 % Resolvents computed: 366
% 0.68/0.88 % Tautologies deleted: 13
% 0.68/0.88 % Forward subsumed : 71
% 0.68/0.88 % Backward subsumed : 6
% 0.68/0.88 % -------- CPU Time ---------
% 0.68/0.88 % User time : 0.506 s
% 0.68/0.88 % System time : 0.020 s
% 0.68/0.88 % Total time : 0.526 s
%------------------------------------------------------------------------------