%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG112+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:05:23 PM UTC 2026
% Result : Theorem 4.30s 1.13s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG112+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n002.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 04:23:18 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.45 % Drodi V4.1.1
% 4.30/1.13 % Refutation found
% 4.30/1.13 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.30/1.13 % SZS output start CNFRefutation for theBenchmark
% 4.30/1.13 fof(f42,hypothesis,(
% 4.30/1.13 ( aSet0(xI)& (! [W0] :( aElementOf0(W0,xI)=> ( (! [W1] :( aElementOf0(W1,xI)=> aElementOf0(sdtpldt0(W0,W1),xI) ))& (! [W1] :( aElement0(W1)=> aElementOf0(sdtasdt0(W1,W0),xI) ) )) ))& aIdeal0(xI)& (! [W0] :( aElementOf0(W0,slsdtgt0(xa))<=> (? [W1] :( aElement0(W1)& sdtasdt0(xa,W1) = W0 ) )))& (! [W0] :( aElementOf0(W0,slsdtgt0(xb))<=> (? [W1] :( aElement0(W1)& sdtasdt0(xb,W1) = W0 ) )))& (! [W0] :( aElementOf0(W0,xI)<=> (? [W1,W2] :( aElementOf0(W1,slsdtgt0(xa))& aElementOf0(W2,slsdtgt0(xb))& sdtpldt0(W1,W2) = W0 ) )))& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ) ),
% 4.30/1.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.30/1.13 fof(f44,hypothesis,(
% 4.30/1.13 (? [W0] :( (! [W1] :( aElementOf0(W1,slsdtgt0(xa))<=> (? [W2] :( aElement0(W2)& sdtasdt0(xa,W2) = W1 ) )))& (! [W1] :( aElementOf0(W1,slsdtgt0(xb))<=> (? [W2] :( aElement0(W2)& sdtasdt0(xb,W2) = W1 ) )))& (? [W1,W2] :( aElementOf0(W1,slsdtgt0(xa))& aElementOf0(W2,slsdtgt0(xb))& sdtpldt0(W1,W2) = W0 ))& aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))& W0 != sz00 ) )),
% 4.30/1.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.30/1.13 fof(f45,hypothesis,(
% 4.30/1.13 (! [W0] :( ( ( (? [W1,W2] :( aElementOf0(W1,slsdtgt0(xa))& aElementOf0(W2,slsdtgt0(xb))& sdtpldt0(W1,W2) = W0 ))| aElementOf0(W0,xI) )& W0 != sz00 )=> (? [W1] :( (? [W2,W3] :( aElementOf0(W2,slsdtgt0(xa))& aElementOf0(W3,slsdtgt0(xb))& sdtpldt0(W2,W3) = W1 ))& aElementOf0(W1,xI)& W1 != sz00& (! [W2] :( ( ( (? [W3,W4] :( aElementOf0(W3,slsdtgt0(xa))& aElementOf0(W4,slsdtgt0(xb))& sdtpldt0(W3,W4) = W2 ))| aElementOf0(W2,xI) )& W2 != sz00 )=> ~ iLess0(sbrdtbr0(W2),sbrdtbr0(W1)) ) )) )) )),
% 4.30/1.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.30/1.13 fof(f46,conjecture,(
% 4.30/1.13 (? [W0] :( ( (? [W1,W2] :( aElementOf0(W1,slsdtgt0(xa))& aElementOf0(W2,slsdtgt0(xb))& sdtpldt0(W1,W2) = W0 ))| aElementOf0(W0,xI) )& W0 != sz00& (! [W1] :( ( (? [W2,W3] :( aElementOf0(W2,slsdtgt0(xa))& aElementOf0(W3,slsdtgt0(xb))& sdtpldt0(W2,W3) = W1 ))& aElementOf0(W1,xI)& W1 != sz00 )=> ~ iLess0(sbrdtbr0(W1),sbrdtbr0(W0)) ) )) )),
% 4.30/1.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.30/1.13 fof(f47,negated_conjecture,(
% 4.30/1.13 ~((? [W0] :( ( (? [W1,W2] :( aElementOf0(W1,slsdtgt0(xa))& aElementOf0(W2,slsdtgt0(xb))& sdtpldt0(W1,W2) = W0 ))| aElementOf0(W0,xI) )& W0 != sz00& (! [W1] :( ( (? [W2,W3] :( aElementOf0(W2,slsdtgt0(xa))& aElementOf0(W3,slsdtgt0(xb))& sdtpldt0(W2,W3) = W1 ))& aElementOf0(W1,xI)& W1 != sz00 )=> ~ iLess0(sbrdtbr0(W1),sbrdtbr0(W0)) ) )) ))),
% 4.30/1.13 inference(negated_conjecture,[status(cth)],[f46])).
% 4.30/1.13 fof(f221,plain,(
% 4.30/1.13 (((((aSet0(xI)&(![W0]: (~aElementOf0(W0,xI)|((![W1]: (~aElementOf0(W1,xI)|aElementOf0(sdtpldt0(W0,W1),xI)))&(![W1]: (~aElement0(W1)|aElementOf0(sdtasdt0(W1,W0),xI)))))))&aIdeal0(xI))&(![W0]: (aElementOf0(W0,slsdtgt0(xa))<=>(?[W1]: (aElement0(W1)&sdtasdt0(xa,W1)=W0)))))&(![W0]: (aElementOf0(W0,slsdtgt0(xb))<=>(?[W1]: (aElement0(W1)&sdtasdt0(xb,W1)=W0)))))&(![W0]: (aElementOf0(W0,xI)<=>(?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0)))))&xI=sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
% 4.30/1.13 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 4.30/1.13 fof(f222,plain,(
% 4.30/1.13 (((((aSet0(xI)&(![W0]: (~aElementOf0(W0,xI)|((![W1]: (~aElementOf0(W1,xI)|aElementOf0(sdtpldt0(W0,W1),xI)))&(![W1]: (~aElement0(W1)|aElementOf0(sdtasdt0(W1,W0),xI)))))))&aIdeal0(xI))&(![W0]: ((~aElementOf0(W0,slsdtgt0(xa))|(?[W1]: (aElement0(W1)&sdtasdt0(xa,W1)=W0)))&(aElementOf0(W0,slsdtgt0(xa))|(![W1]: (~aElement0(W1)|~sdtasdt0(xa,W1)=W0))))))&(![W0]: ((~aElementOf0(W0,slsdtgt0(xb))|(?[W1]: (aElement0(W1)&sdtasdt0(xb,W1)=W0)))&(aElementOf0(W0,slsdtgt0(xb))|(![W1]: (~aElement0(W1)|~sdtasdt0(xb,W1)=W0))))))&(![W0]: ((~aElementOf0(W0,xI)|(?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0)))&(aElementOf0(W0,xI)|(![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))))))&xI=sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
% 4.30/1.13 inference(NNF_transformation,[status(thm)],[f221])).
% 4.30/1.13 fof(f223,plain,(
% 4.30/1.13 (((((aSet0(xI)&(![W0]: (~aElementOf0(W0,xI)|((![W1]: (~aElementOf0(W1,xI)|aElementOf0(sdtpldt0(W0,W1),xI)))&(![W1]: (~aElement0(W1)|aElementOf0(sdtasdt0(W1,W0),xI)))))))&aIdeal0(xI))&((![W0]: (~aElementOf0(W0,slsdtgt0(xa))|(?[W1]: (aElement0(W1)&sdtasdt0(xa,W1)=W0))))&(![W0]: (aElementOf0(W0,slsdtgt0(xa))|(![W1]: (~aElement0(W1)|~sdtasdt0(xa,W1)=W0))))))&((![W0]: (~aElementOf0(W0,slsdtgt0(xb))|(?[W1]: (aElement0(W1)&sdtasdt0(xb,W1)=W0))))&(![W0]: (aElementOf0(W0,slsdtgt0(xb))|(![W1]: (~aElement0(W1)|~sdtasdt0(xb,W1)=W0))))))&((![W0]: (~aElementOf0(W0,xI)|(?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0))))&(![W0]: (aElementOf0(W0,xI)|(![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))))))&xI=sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
% 4.30/1.13 inference(miniscoping,[status(thm)],[f222])).
% 4.30/1.13 fof(f224,plain,(
% 4.30/1.13 (((((aSet0(xI)&(![W0]: (~aElementOf0(W0,xI)|((![W1]: (~aElementOf0(W1,xI)|aElementOf0(sdtpldt0(W0,W1),xI)))&(![W1]: (~aElement0(W1)|aElementOf0(sdtasdt0(W1,W0),xI)))))))&aIdeal0(xI))&((![W0]: (~aElementOf0(W0,slsdtgt0(xa))|(aElement0(sK23_skl(W0))&sdtasdt0(xa,sK23_skl(W0))=W0)))&(![W0]: (aElementOf0(W0,slsdtgt0(xa))|(![W1]: (~aElement0(W1)|~sdtasdt0(xa,W1)=W0))))))&((![W0]: (~aElementOf0(W0,slsdtgt0(xb))|(aElement0(sK24_skl(W0))&sdtasdt0(xb,sK24_skl(W0))=W0)))&(![W0]: (aElementOf0(W0,slsdtgt0(xb))|(![W1]: (~aElement0(W1)|~sdtasdt0(xb,W1)=W0))))))&((![W0]: (~aElementOf0(W0,xI)|((aElementOf0(sK25_skl(W0),slsdtgt0(xa))&aElementOf0(sK26_skl(W0),slsdtgt0(xb)))&sdtpldt0(sK25_skl(W0),sK26_skl(W0))=W0)))&(![W0]: (aElementOf0(W0,xI)|(![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))))))&xI=sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
% 4.30/1.13 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl,sK25_skl,sK26_skl]),skolemize(W1,sK23_skl(W0)),skolemize(W1,sK24_skl(W0)),skolemize(W1,sK25_skl(W0)),skolemize(W2,sK26_skl(W0))],[f223])).
% 4.30/1.13 fof(f239,plain,(
% 4.30/1.13 xI=sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
% 4.30/1.13 inference(cnf_transformation,[status(thm)],[f224])).
% 4.30/1.13 fof(f253,plain,(
% 4.30/1.13 ?[W0]: (((((![W1]: ((~aElementOf0(W1,slsdtgt0(xa))|(?[W2]: (aElement0(W2)&sdtasdt0(xa,W2)=W1)))&(aElementOf0(W1,slsdtgt0(xa))|(![W2]: (~aElement0(W2)|~sdtasdt0(xa,W2)=W1)))))&(![W1]: ((~aElementOf0(W1,slsdtgt0(xb))|(?[W2]: (aElement0(W2)&sdtasdt0(xb,W2)=W1)))&(aElementOf0(W1,slsdtgt0(xb))|(![W2]: (~aElement0(W2)|~sdtasdt0(xb,W2)=W1))))))&(?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0)))&aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))))&~W0=sz00)),
% 4.30/1.13 inference(NNF_transformation,[status(thm)],[f44])).
% 4.30/1.13 fof(f254,plain,(
% 4.30/1.13 ?[W0]: ((((((![W1]: (~aElementOf0(W1,slsdtgt0(xa))|(?[W2]: (aElement0(W2)&sdtasdt0(xa,W2)=W1))))&(![W1]: (aElementOf0(W1,slsdtgt0(xa))|(![W2]: (~aElement0(W2)|~sdtasdt0(xa,W2)=W1)))))&((![W1]: (~aElementOf0(W1,slsdtgt0(xb))|(?[W2]: (aElement0(W2)&sdtasdt0(xb,W2)=W1))))&(![W1]: (aElementOf0(W1,slsdtgt0(xb))|(![W2]: (~aElement0(W2)|~sdtasdt0(xb,W2)=W1))))))&(?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0)))&aElementOf0(W0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))))&~W0=sz00)),
% 4.30/1.13 inference(miniscoping,[status(thm)],[f253])).
% 4.30/1.13 fof(f255,plain,(
% 4.30/1.13 ((((((![W1]: (~aElementOf0(W1,slsdtgt0(xa))|(aElement0(sK32_skl(W1))&sdtasdt0(xa,sK32_skl(W1))=W1)))&(![W1]: (aElementOf0(W1,slsdtgt0(xa))|(![W2]: (~aElement0(W2)|~sdtasdt0(xa,W2)=W1)))))&((![W1]: (~aElementOf0(W1,slsdtgt0(xb))|(aElement0(sK33_skl(W1))&sdtasdt0(xb,sK33_skl(W1))=W1)))&(![W1]: (aElementOf0(W1,slsdtgt0(xb))|(![W2]: (~aElement0(W2)|~sdtasdt0(xb,W2)=W1))))))&((aElementOf0(sK34_skl,slsdtgt0(xa))&aElementOf0(sK35_skl,slsdtgt0(xb)))&sdtpldt0(sK34_skl,sK35_skl)=sK31_skl))&aElementOf0(sK31_skl,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))))&~sK31_skl=sz00)),
% 4.30/1.13 inference(skolemize,[status(esa),new_symbols(skolem,[sK31_skl,sK32_skl,sK33_skl,sK34_skl,sK35_skl]),skolemize(W0,sK31_skl),skolemize(W2,sK32_skl(W1)),skolemize(W2,sK33_skl(W1)),skolemize(W1,sK34_skl),skolemize(W2,sK35_skl)],[f254])).
% 4.30/1.13 fof(f265,plain,(
% 4.30/1.13 aElementOf0(sK31_skl,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))),
% 4.30/1.13 inference(cnf_transformation,[status(thm)],[f255])).
% 4.30/1.13 fof(f266,plain,(
% 4.30/1.13 ~sK31_skl=sz00),
% 4.30/1.13 inference(cnf_transformation,[status(thm)],[f255])).
% 4.30/1.13 fof(f267,plain,(
% 4.30/1.13 ![W0]: ((((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,xI))|W0=sz00)|(?[W1]: ((((?[W2,W3]: ((aElementOf0(W2,slsdtgt0(xa))&aElementOf0(W3,slsdtgt0(xb)))&sdtpldt0(W2,W3)=W1))&aElementOf0(W1,xI))&~W1=sz00)&(![W2]: ((((![W3,W4]: ((~aElementOf0(W3,slsdtgt0(xa))|~aElementOf0(W4,slsdtgt0(xb)))|~sdtpldt0(W3,W4)=W2))&~aElementOf0(W2,xI))|W2=sz00)|~iLess0(sbrdtbr0(W2),sbrdtbr0(W1)))))))),
% 4.30/1.13 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 4.30/1.13 fof(f268,definition,(
% 4.30/1.13 ![W0]: (sP4_prd(W0)<=>(((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,xI))|W0=sz00))),
% 4.30/1.13 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 4.30/1.13 fof(f269,plain,(
% 4.30/1.13 ![W0]: (sP4_prd(W0)|(?[W1]: ((((?[W2,W3]: ((aElementOf0(W2,slsdtgt0(xa))&aElementOf0(W3,slsdtgt0(xb)))&sdtpldt0(W2,W3)=W1))&aElementOf0(W1,xI))&~W1=sz00)&(![W2]: ((((![W3,W4]: ((~aElementOf0(W3,slsdtgt0(xa))|~aElementOf0(W4,slsdtgt0(xb)))|~sdtpldt0(W3,W4)=W2))&~aElementOf0(W2,xI))|W2=sz00)|~iLess0(sbrdtbr0(W2),sbrdtbr0(W1)))))))),
% 4.30/1.13 inference(formula_renaming,[status(thm)],[f267,f268])).
% 4.30/1.13 fof(f270,plain,(
% 4.30/1.13 (![W0]: sP4_prd(W0))|(?[W1]: ((((?[W2,W3]: ((aElementOf0(W2,slsdtgt0(xa))&aElementOf0(W3,slsdtgt0(xb)))&sdtpldt0(W2,W3)=W1))&aElementOf0(W1,xI))&~W1=sz00)&(![W2]: ((((![W3,W4]: ((~aElementOf0(W3,slsdtgt0(xa))|~aElementOf0(W4,slsdtgt0(xb)))|~sdtpldt0(W3,W4)=W2))&~aElementOf0(W2,xI))|W2=sz00)|~iLess0(sbrdtbr0(W2),sbrdtbr0(W1))))))),
% 4.30/1.13 inference(miniscoping,[status(thm)],[f269])).
% 4.30/1.13 fof(f271,plain,(
% 4.30/1.13 (![W0]: sP4_prd(W0))|(((((aElementOf0(sK37_skl,slsdtgt0(xa))&aElementOf0(sK38_skl,slsdtgt0(xb)))&sdtpldt0(sK37_skl,sK38_skl)=sK36_skl)&aElementOf0(sK36_skl,xI))&~sK36_skl=sz00)&(![W2]: ((((![W3,W4]: ((~aElementOf0(W3,slsdtgt0(xa))|~aElementOf0(W4,slsdtgt0(xb)))|~sdtpldt0(W3,W4)=W2))&~aElementOf0(W2,xI))|W2=sz00)|~iLess0(sbrdtbr0(W2),sbrdtbr0(sK36_skl)))))),
% 4.30/1.13 inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl,sK37_skl,sK38_skl]),skolemize(W1,sK36_skl),skolemize(W2,sK37_skl),skolemize(W3,sK38_skl)],[f270])).
% 4.30/1.13 fof(f275,plain,(
% 4.30/1.13 ![X0]: (sP4_prd(X0)|aElementOf0(sK36_skl,xI))),
% 4.30/1.13 inference(cnf_transformation,[status(thm)],[f271])).
% 4.30/1.13 fof(f276,plain,(
% 4.30/1.13 ![X0]: (sP4_prd(X0)|~sK36_skl=sz00)),
% 4.30/1.13 inference(cnf_transformation,[status(thm)],[f271])).
% 4.30/1.13 fof(f278,plain,(
% 4.30/1.13 ![X0,X1]: (sP4_prd(X0)|~aElementOf0(X1,xI)|X1=sz00|~iLess0(sbrdtbr0(X1),sbrdtbr0(sK36_skl)))),
% 4.30/1.13 inference(cnf_transformation,[status(thm)],[f271])).
% 4.30/1.13 fof(f279,plain,(
% 4.30/1.13 (![W0]: ((((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,xI))|W0=sz00)|(?[W1]: ((((?[W2,W3]: ((aElementOf0(W2,slsdtgt0(xa))&aElementOf0(W3,slsdtgt0(xb)))&sdtpldt0(W2,W3)=W1))&aElementOf0(W1,xI))&~W1=sz00)&iLess0(sbrdtbr0(W1),sbrdtbr0(W0))))))),
% 4.30/1.13 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 4.30/1.13 fof(f280,definition,(
% 4.30/1.13 ![W0]: (sP5_prd(W0)<=>(((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,xI))|W0=sz00))),
% 4.30/1.13 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 4.30/1.13 fof(f281,plain,(
% 4.30/1.13 ![W0]: (sP5_prd(W0)|(?[W1]: ((((?[W2,W3]: ((aElementOf0(W2,slsdtgt0(xa))&aElementOf0(W3,slsdtgt0(xb)))&sdtpldt0(W2,W3)=W1))&aElementOf0(W1,xI))&~W1=sz00)&iLess0(sbrdtbr0(W1),sbrdtbr0(W0)))))),
% 4.30/1.13 inference(formula_renaming,[status(thm)],[f279,f280])).
% 4.30/1.13 fof(f282,plain,(
% 4.30/1.13 ![W0]: (sP5_prd(W0)|(((((aElementOf0(sK40_skl(W0),slsdtgt0(xa))&aElementOf0(sK41_skl(W0),slsdtgt0(xb)))&sdtpldt0(sK40_skl(W0),sK41_skl(W0))=sK39_skl(W0))&aElementOf0(sK39_skl(W0),xI))&~sK39_skl(W0)=sz00)&iLess0(sbrdtbr0(sK39_skl(W0)),sbrdtbr0(W0))))),
% 4.30/1.13 inference(skolemize,[status(esa),new_symbols(skolem,[sK39_skl,sK40_skl,sK41_skl]),skolemize(W1,sK39_skl(W0)),skolemize(W2,sK40_skl(W0)),skolemize(W3,sK41_skl(W0))],[f281])).
% 4.30/1.13 fof(f286,plain,(
% 4.30/1.13 ![X0]: (sP5_prd(X0)|aElementOf0(sK39_skl(X0),xI))),
% 4.30/1.13 inference(cnf_transformation,[status(thm)],[f282])).
% 4.30/1.13 fof(f287,plain,(
% 4.30/1.13 ![X0]: (sP5_prd(X0)|~sK39_skl(X0)=sz00)),
% 4.30/1.13 inference(cnf_transformation,[status(thm)],[f282])).
% 4.30/1.13 fof(f288,plain,(
% 4.30/1.13 ![X0]: (sP5_prd(X0)|iLess0(sbrdtbr0(sK39_skl(X0)),sbrdtbr0(X0)))),
% 4.30/1.13 inference(cnf_transformation,[status(thm)],[f282])).
% 4.30/1.13 fof(f317,plain,(
% 4.30/1.13 ![W0]: ((~sP4_prd(W0)|(((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,xI))|W0=sz00))&(sP4_prd(W0)|(((?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0))|aElementOf0(W0,xI))&~W0=sz00)))),
% 4.30/1.13 inference(NNF_transformation,[status(thm)],[f268])).
% 4.30/1.13 fof(f318,plain,(
% 4.30/1.13 (![W0]: (~sP4_prd(W0)|(((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,xI))|W0=sz00)))&(![W0]: (sP4_prd(W0)|(((?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0))|aElementOf0(W0,xI))&~W0=sz00)))),
% 4.30/1.13 inference(miniscoping,[status(thm)],[f317])).
% 4.30/1.13 fof(f319,plain,(
% 4.30/1.13 (![W0]: (~sP4_prd(W0)|(((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,xI))|W0=sz00)))&(![W0]: (sP4_prd(W0)|((((aElementOf0(sK43_skl(W0),slsdtgt0(xa))&aElementOf0(sK44_skl(W0),slsdtgt0(xb)))&sdtpldt0(sK43_skl(W0),sK44_skl(W0))=W0)|aElementOf0(W0,xI))&~W0=sz00)))),
% 4.30/1.13 inference(skolemize,[status(esa),new_symbols(skolem,[sK43_skl,sK44_skl]),skolemize(W1,sK43_skl(W0)),skolemize(W2,sK44_skl(W0))],[f318])).
% 4.30/1.13 fof(f321,plain,(
% 4.30/1.13 ![X0]: (~sP4_prd(X0)|~aElementOf0(X0,xI)|X0=sz00)),
% 4.30/1.13 inference(cnf_transformation,[status(thm)],[f319])).
% 4.30/1.13 fof(f326,plain,(
% 4.30/1.13 ![W0]: ((~sP5_prd(W0)|(((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,xI))|W0=sz00))&(sP5_prd(W0)|(((?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0))|aElementOf0(W0,xI))&~W0=sz00)))),
% 4.30/1.13 inference(NNF_transformation,[status(thm)],[f280])).
% 4.30/1.13 fof(f327,plain,(
% 4.30/1.13 (![W0]: (~sP5_prd(W0)|(((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,xI))|W0=sz00)))&(![W0]: (sP5_prd(W0)|(((?[W1,W2]: ((aElementOf0(W1,slsdtgt0(xa))&aElementOf0(W2,slsdtgt0(xb)))&sdtpldt0(W1,W2)=W0))|aElementOf0(W0,xI))&~W0=sz00)))),
% 4.30/1.13 inference(miniscoping,[status(thm)],[f326])).
% 4.30/1.13 fof(f328,plain,(
% 4.30/1.13 (![W0]: (~sP5_prd(W0)|(((![W1,W2]: ((~aElementOf0(W1,slsdtgt0(xa))|~aElementOf0(W2,slsdtgt0(xb)))|~sdtpldt0(W1,W2)=W0))&~aElementOf0(W0,xI))|W0=sz00)))&(![W0]: (sP5_prd(W0)|((((aElementOf0(sK45_skl(W0),slsdtgt0(xa))&aElementOf0(sK46_skl(W0),slsdtgt0(xb)))&sdtpldt0(sK45_skl(W0),sK46_skl(W0))=W0)|aElementOf0(W0,xI))&~W0=sz00)))),
% 4.30/1.13 inference(skolemize,[status(esa),new_symbols(skolem,[sK45_skl,sK46_skl]),skolemize(W1,sK45_skl(W0)),skolemize(W2,sK46_skl(W0))],[f327])).
% 4.30/1.13 fof(f330,plain,(
% 4.30/1.13 ![X0]: (~sP5_prd(X0)|~aElementOf0(X0,xI)|X0=sz00)),
% 4.30/1.13 inference(cnf_transformation,[status(thm)],[f328])).
% 4.30/1.13 fof(f334,plain,(
% 4.30/1.13 ![X0]: (sP5_prd(X0)|~X0=sz00)),
% 4.30/1.13 inference(cnf_transformation,[status(thm)],[f328])).
% 4.30/1.13 fof(f351,definition,(
% 4.30/1.13 ![X0]: (sQ2_spl <=> (sP4_prd(X0)))),
% 4.30/1.13 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 4.30/1.13 fof(f352,plain,(
% 4.30/1.13 ![X0]: (sP4_prd(X0)|~sQ2_spl)),
% 4.30/1.13 inference(component_clause,[status(thm)],[f351])).
% 4.30/1.13 fof(f366,definition,(
% 4.30/1.13 sQ6_spl <=> (aElementOf0(sK36_skl,xI))),
% 4.30/1.13 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 4.30/1.13 fof(f369,plain,(
% 4.30/1.13 sQ2_spl|sQ6_spl),
% 4.30/1.13 inference(split_clause,[status(thm)],[f275,f351,f366])).
% 4.30/1.13 fof(f370,definition,(
% 4.30/1.13 sQ7_spl <=> (sK36_skl=sz00)),
% 4.30/1.13 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 4.30/1.13 fof(f373,plain,(
% 4.30/1.13 sQ2_spl|~sQ7_spl),
% 4.30/1.13 inference(split_clause,[status(thm)],[f276,f351,f370])).
% 4.30/1.13 fof(f378,definition,(
% 4.30/1.13 ![X1]: (sQ9_spl <=> (~aElementOf0(X1,xI)|X1=sz00|~iLess0(sbrdtbr0(X1),sbrdtbr0(sK36_skl))))),
% 4.30/1.13 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 5.12/1.15 fof(f379,plain,(
% 5.12/1.15 ![X0]: (~aElementOf0(X0,xI)|X0=sz00|~iLess0(sbrdtbr0(X0),sbrdtbr0(sK36_skl))|~sQ9_spl)),
% 5.12/1.15 inference(component_clause,[status(thm)],[f378])).
% 5.12/1.15 fof(f381,plain,(
% 5.12/1.15 sQ2_spl|sQ9_spl),
% 5.12/1.15 inference(split_clause,[status(thm)],[f278,f351,f378])).
% 5.12/1.15 fof(f403,plain,(
% 5.12/1.15 sP5_prd(sz00)),
% 5.12/1.15 inference(destructive_equality_resolution,[status(thm)],[f334])).
% 5.12/1.15 fof(f448,plain,(
% 5.12/1.15 ![X0]: (~sP5_prd(sK39_skl(X0))|sK39_skl(X0)=sz00|sP5_prd(X0))),
% 5.12/1.15 inference(resolution,[status(thm)],[f330,f286])).
% 5.12/1.15 fof(f449,plain,(
% 5.12/1.15 ![X0]: (~sP5_prd(sK39_skl(X0))|sP5_prd(X0))),
% 5.12/1.15 inference(forward_subsumption_resolution,[status(thm)],[f448,f287])).
% 5.12/1.15 fof(f5083,plain,(
% 5.12/1.15 aElementOf0(sK31_skl,xI)),
% 5.12/1.15 inference(forward_demodulation,[status(thm)],[f239,f265])).
% 5.12/1.15 fof(f5092,definition,(
% 5.12/1.15 sQ354_spl <=> (sK31_skl=sz00)),
% 5.12/1.15 introduced(definition,[new_symbols(definition,[sQ354_spl])],[split_symbol_definition])).
% 5.12/1.15 fof(f5093,plain,(
% 5.12/1.15 sK31_skl=sz00|~sQ354_spl),
% 5.12/1.15 inference(component_clause,[status(thm)],[f5092])).
% 5.12/1.15 fof(f5096,plain,(
% 5.12/1.15 $false|~sQ354_spl),
% 5.12/1.15 inference(forward_subsumption_resolution,[status(thm)],[f5093,f266])).
% 5.12/1.15 fof(f5097,plain,(
% 5.12/1.15 ~sQ354_spl),
% 5.12/1.15 inference(contradiction_clause,[status(thm)],[f5096])).
% 5.12/1.15 fof(f5102,definition,(
% 5.12/1.15 sQ355_spl <=> (sP5_prd(sz00))),
% 5.12/1.15 introduced(definition,[new_symbols(definition,[sQ355_spl])],[split_symbol_definition])).
% 5.12/1.15 fof(f5104,plain,(
% 5.12/1.15 ~sP5_prd(sz00)|sQ355_spl),
% 5.12/1.15 inference(component_clause,[status(thm)],[f5102])).
% 5.12/1.15 fof(f6326,plain,(
% 5.12/1.15 ![X0]: (~aElementOf0(X0,xI)|X0=sz00|~sQ2_spl)),
% 5.12/1.15 inference(forward_subsumption_resolution,[status(thm)],[f321,f352])).
% 5.12/1.15 fof(f6327,plain,(
% 5.12/1.15 sK31_skl=sz00|~sQ2_spl),
% 5.12/1.15 inference(resolution,[status(thm)],[f6326,f5083])).
% 5.12/1.15 fof(f6328,plain,(
% 5.12/1.15 sQ354_spl|~sQ2_spl),
% 5.12/1.15 inference(split_clause,[status(thm)],[f6327,f5092,f351])).
% 5.12/1.15 fof(f7438,plain,(
% 5.12/1.15 ~aElementOf0(sK39_skl(sK36_skl),xI)|sK39_skl(sK36_skl)=sz00|sP5_prd(sK36_skl)|~sQ9_spl),
% 5.12/1.15 inference(resolution,[status(thm)],[f379,f288])).
% 5.12/1.15 fof(f7446,definition,(
% 5.12/1.15 sQ507_spl <=> (aElementOf0(sK39_skl(sK36_skl),xI))),
% 5.12/1.15 introduced(definition,[new_symbols(definition,[sQ507_spl])],[split_symbol_definition])).
% 5.12/1.15 fof(f7448,plain,(
% 5.12/1.15 ~aElementOf0(sK39_skl(sK36_skl),xI)|sQ507_spl),
% 5.12/1.15 inference(component_clause,[status(thm)],[f7446])).
% 5.12/1.15 fof(f7449,definition,(
% 5.12/1.15 sQ508_spl <=> (sK39_skl(sK36_skl)=sz00)),
% 5.12/1.15 introduced(definition,[new_symbols(definition,[sQ508_spl])],[split_symbol_definition])).
% 5.12/1.15 fof(f7450,plain,(
% 5.12/1.15 sK39_skl(sK36_skl)=sz00|~sQ508_spl),
% 5.12/1.15 inference(component_clause,[status(thm)],[f7449])).
% 5.12/1.15 fof(f7452,definition,(
% 5.12/1.15 sQ509_spl <=> (sP5_prd(sK36_skl))),
% 5.12/1.15 introduced(definition,[new_symbols(definition,[sQ509_spl])],[split_symbol_definition])).
% 5.12/1.15 fof(f7453,plain,(
% 5.12/1.15 sP5_prd(sK36_skl)|~sQ509_spl),
% 5.12/1.15 inference(component_clause,[status(thm)],[f7452])).
% 5.12/1.15 fof(f7455,plain,(
% 5.12/1.15 ~sQ507_spl|sQ508_spl|sQ509_spl|~sQ9_spl),
% 5.12/1.15 inference(split_clause,[status(thm)],[f7438,f7446,f7449,f7452,f378])).
% 5.12/1.15 fof(f7457,plain,(
% 5.12/1.15 ~aElementOf0(sK36_skl,xI)|sK36_skl=sz00|~sQ509_spl),
% 5.12/1.15 inference(resolution,[status(thm)],[f7453,f330])).
% 5.12/1.15 fof(f7458,plain,(
% 5.12/1.15 ~sQ6_spl|sQ7_spl|~sQ509_spl),
% 5.12/1.15 inference(split_clause,[status(thm)],[f7457,f366,f370,f7452])).
% 5.12/1.15 fof(f7465,plain,(
% 5.12/1.15 ~sP5_prd(sz00)|sP5_prd(sK36_skl)|~sQ508_spl),
% 5.12/1.15 inference(paramodulation,[status(thm)],[f7450,f449])).
% 5.12/1.15 fof(f7472,plain,(
% 5.12/1.15 ~sQ355_spl|sQ509_spl|~sQ508_spl),
% 5.12/1.15 inference(split_clause,[status(thm)],[f7465,f5102,f7452,f7449])).
% 5.12/1.15 fof(f7473,plain,(
% 5.12/1.15 $false|sQ355_spl),
% 5.12/1.15 inference(forward_subsumption_resolution,[status(thm)],[f5104,f403])).
% 5.12/1.15 fof(f7474,plain,(
% 5.12/1.15 sQ355_spl),
% 5.12/1.15 inference(contradiction_clause,[status(thm)],[f7473])).
% 5.12/1.15 fof(f7563,plain,(
% 5.12/1.15 sP5_prd(sK36_skl)|sQ507_spl),
% 5.12/1.15 inference(resolution,[status(thm)],[f7448,f286])).
% 5.12/1.15 fof(f7566,plain,(
% 5.12/1.15 sQ509_spl|sQ507_spl),
% 5.12/1.15 inference(split_clause,[status(thm)],[f7563,f7452,f7446])).
% 5.12/1.15 fof(f7581,plain,(
% 5.12/1.15 $false),
% 5.12/1.15 inference(sat_refutation,[status(thm)],[f369,f373,f381,f5097,f6328,f7455,f7458,f7472,f7474,f7566])).
% 5.12/1.15 % SZS output end CNFRefutation for theBenchmark.p
% 5.12/1.17 % Elapsed time: 0.724806 seconds
% 5.12/1.17 % CPU time: 5.385682 seconds
% 5.12/1.17 % Total memory used: 166.243 MB
% 5.12/1.17 % Net memory used: 161.133 MB
%------------------------------------------------------------------------------