%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG108+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:22 PM UTC 2026
% Result : Theorem 0.17s 0.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG108+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n008.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:20:53 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 0.17/0.61 % Refutation found
% 0.17/0.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.61 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.61 fof(f2,axiom,(
% 0.17/0.61 aElement0(sz00) ),
% 0.17/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.61 fof(f3,axiom,(
% 0.17/0.61 aElement0(sz10) ),
% 0.17/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.61 fof(f13,axiom,(
% 0.17/0.61 (! [W0] :( aElement0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 0.17/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.61 fof(f16,axiom,(
% 0.17/0.61 (! [W0] :( aElement0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 0.17/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.61 fof(f39,hypothesis,(
% 0.17/0.61 ( aElement0(xa)& aElement0(xb) ) ),
% 0.17/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.61 fof(f41,hypothesis,(
% 0.17/0.61 ( aElement0(xc)& (? [W0] :( aElement0(W0)& sdtasdt0(xc,W0) = xa ))& doDivides0(xc,xa)& aDivisorOf0(xc,xa)& aElement0(xc)& (? [W0] :( aElement0(W0)& sdtasdt0(xc,W0) = xb ))& doDivides0(xc,xb)& aDivisorOf0(xc,xb)& (! [W0] :( ( ( ( aElement0(W0)& ( (? [W1] :( aElement0(W1)& sdtasdt0(W0,W1) = xa ))| doDivides0(W0,xa) ) )| aDivisorOf0(W0,xa) )& ( (? [W1] :( aElement0(W1)& sdtasdt0(W0,W1) = xb ))| doDivides0(W0,xb)| aDivisorOf0(W0,xb) ) )=> ( (? [W1] :( aElement0(W1)& sdtasdt0(W0,W1) = xc ))& doDivides0(W0,xc) ) ))& aGcdOfAnd0(xc,xa,xb) ) ),
% 0.17/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.61 fof(f42,hypothesis,(
% 0.17/0.61 ( 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)) ) ),
% 0.17/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.61 fof(f43,conjecture,(
% 0.17/0.61 ( ( (? [W0] :( aElement0(W0)& sdtasdt0(xa,W0) = sz00 ))| aElementOf0(sz00,slsdtgt0(xa)) )& ( (? [W0] :( aElement0(W0)& sdtasdt0(xa,W0) = xa ))| aElementOf0(xa,slsdtgt0(xa)) )& ( (? [W0] :( aElement0(W0)& sdtasdt0(xb,W0) = sz00 ))| aElementOf0(sz00,slsdtgt0(xb)) )& ( (? [W0] :( aElement0(W0)& sdtasdt0(xb,W0) = xb ))| aElementOf0(xb,slsdtgt0(xb)) ) ) ),
% 0.17/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/0.61 fof(f44,negated_conjecture,(
% 0.17/0.61 ~(( ( (? [W0] :( aElement0(W0)& sdtasdt0(xa,W0) = sz00 ))| aElementOf0(sz00,slsdtgt0(xa)) )& ( (? [W0] :( aElement0(W0)& sdtasdt0(xa,W0) = xa ))| aElementOf0(xa,slsdtgt0(xa)) )& ( (? [W0] :( aElement0(W0)& sdtasdt0(xb,W0) = sz00 ))| aElementOf0(sz00,slsdtgt0(xb)) )& ( (? [W0] :( aElement0(W0)& sdtasdt0(xb,W0) = xb ))| aElementOf0(xb,slsdtgt0(xb)) ) ) )),
% 0.17/0.61 inference(negated_conjecture,[status(cth)],[f43])).
% 0.17/0.61 fof(f48,plain,(
% 0.17/0.61 aElement0(sz00)),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f2])).
% 0.17/0.61 fof(f49,plain,(
% 0.17/0.61 aElement0(sz10)),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f3])).
% 0.17/0.61 fof(f70,plain,(
% 0.17/0.61 ![W0]: (~aElement0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 0.17/0.61 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.17/0.61 fof(f71,plain,(
% 0.17/0.61 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sz10)=X0)),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f70])).
% 0.17/0.61 fof(f79,plain,(
% 0.17/0.61 ![W0]: (~aElement0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 0.17/0.61 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.17/0.61 fof(f80,plain,(
% 0.17/0.61 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f79])).
% 0.17/0.61 fof(f197,plain,(
% 0.17/0.61 aElement0(xa)),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f39])).
% 0.17/0.61 fof(f198,plain,(
% 0.17/0.61 aElement0(xb)),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f39])).
% 0.17/0.61 fof(f200,plain,(
% 0.17/0.61 ((((((((aElement0(xc)&(?[W0]: (aElement0(W0)&sdtasdt0(xc,W0)=xa)))&doDivides0(xc,xa))&aDivisorOf0(xc,xa))&aElement0(xc))&(?[W0]: (aElement0(W0)&sdtasdt0(xc,W0)=xb)))&doDivides0(xc,xb))&aDivisorOf0(xc,xb))&(![W0]: ((((~aElement0(W0)|((![W1]: (~aElement0(W1)|~sdtasdt0(W0,W1)=xa))&~doDivides0(W0,xa)))&~aDivisorOf0(W0,xa))|(((![W1]: (~aElement0(W1)|~sdtasdt0(W0,W1)=xb))&~doDivides0(W0,xb))&~aDivisorOf0(W0,xb)))|((?[W1]: (aElement0(W1)&sdtasdt0(W0,W1)=xc))&doDivides0(W0,xc)))))&aGcdOfAnd0(xc,xa,xb)),
% 0.17/0.61 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.17/0.61 fof(f201,definition,(
% 0.17/0.61 ![W0]: (sP3_prd(W0)<=>(((~aElement0(W0)|((![W1]: (~aElement0(W1)|~sdtasdt0(W0,W1)=xa))&~doDivides0(W0,xa)))&~aDivisorOf0(W0,xa))|(((![W1]: (~aElement0(W1)|~sdtasdt0(W0,W1)=xb))&~doDivides0(W0,xb))&~aDivisorOf0(W0,xb))))),
% 0.17/0.61 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.17/0.61 fof(f202,plain,(
% 0.17/0.61 ((((((((aElement0(xc)&(?[W0]: (aElement0(W0)&sdtasdt0(xc,W0)=xa)))&doDivides0(xc,xa))&aDivisorOf0(xc,xa))&aElement0(xc))&(?[W0]: (aElement0(W0)&sdtasdt0(xc,W0)=xb)))&doDivides0(xc,xb))&aDivisorOf0(xc,xb))&(![W0]: (sP3_prd(W0)|((?[W1]: (aElement0(W1)&sdtasdt0(W0,W1)=xc))&doDivides0(W0,xc)))))&aGcdOfAnd0(xc,xa,xb)),
% 0.17/0.61 inference(formula_renaming,[status(thm)],[f200,f201])).
% 0.17/0.61 fof(f203,plain,(
% 0.17/0.61 ((((((((aElement0(xc)&(aElement0(sK20_skl)&sdtasdt0(xc,sK20_skl)=xa))&doDivides0(xc,xa))&aDivisorOf0(xc,xa))&aElement0(xc))&(aElement0(sK21_skl)&sdtasdt0(xc,sK21_skl)=xb))&doDivides0(xc,xb))&aDivisorOf0(xc,xb))&(![W0]: (sP3_prd(W0)|((aElement0(sK22_skl(W0))&sdtasdt0(W0,sK22_skl(W0))=xc)&doDivides0(W0,xc)))))&aGcdOfAnd0(xc,xa,xb)),
% 0.17/0.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl,sK22_skl]),skolemize(W0,sK20_skl),skolemize(W0,sK21_skl),skolemize(W1,sK22_skl(W0))],[f202])).
% 0.17/0.61 fof(f205,plain,(
% 0.17/0.61 aElement0(sK20_skl)),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f203])).
% 0.17/0.61 fof(f210,plain,(
% 0.17/0.61 aElement0(sK21_skl)),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f203])).
% 0.17/0.61 fof(f218,plain,(
% 0.17/0.61 (((((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))),
% 0.17/0.61 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.17/0.61 fof(f219,plain,(
% 0.17/0.61 (((((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))),
% 0.17/0.61 inference(NNF_transformation,[status(thm)],[f218])).
% 0.17/0.61 fof(f220,plain,(
% 0.17/0.61 (((((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))),
% 0.17/0.61 inference(miniscoping,[status(thm)],[f219])).
% 0.17/0.61 fof(f221,plain,(
% 0.17/0.61 (((((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))),
% 0.17/0.61 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))],[f220])).
% 0.17/0.61 fof(f231,plain,(
% 0.17/0.61 ![X0,X1]: (aElementOf0(X0,slsdtgt0(xb))|~aElement0(X1)|~sdtasdt0(xb,X1)=X0)),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f221])).
% 0.17/0.61 fof(f237,plain,(
% 0.17/0.61 (((((![W0]: (~aElement0(W0)|~sdtasdt0(xa,W0)=sz00))&~aElementOf0(sz00,slsdtgt0(xa)))|((![W0]: (~aElement0(W0)|~sdtasdt0(xa,W0)=xa))&~aElementOf0(xa,slsdtgt0(xa))))|((![W0]: (~aElement0(W0)|~sdtasdt0(xb,W0)=sz00))&~aElementOf0(sz00,slsdtgt0(xb))))|((![W0]: (~aElement0(W0)|~sdtasdt0(xb,W0)=xb))&~aElementOf0(xb,slsdtgt0(xb))))),
% 0.17/0.61 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 0.17/0.61 fof(f238,definition,(
% 0.17/0.61 sP4_prd<=>((((![W0]: (~aElement0(W0)|~sdtasdt0(xa,W0)=sz00))&~aElementOf0(sz00,slsdtgt0(xa)))|((![W0]: (~aElement0(W0)|~sdtasdt0(xa,W0)=xa))&~aElementOf0(xa,slsdtgt0(xa))))|((![W0]: (~aElement0(W0)|~sdtasdt0(xb,W0)=sz00))&~aElementOf0(sz00,slsdtgt0(xb))))),
% 0.17/0.61 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.17/0.61 fof(f239,plain,(
% 0.17/0.61 sP4_prd|((![W0]: (~aElement0(W0)|~sdtasdt0(xb,W0)=xb))&~aElementOf0(xb,slsdtgt0(xb)))),
% 0.17/0.61 inference(formula_renaming,[status(thm)],[f237,f238])).
% 0.17/0.61 fof(f240,plain,(
% 0.17/0.61 ![X0]: (sP4_prd|~aElement0(X0)|~sdtasdt0(xb,X0)=xb)),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f239])).
% 0.17/0.61 fof(f270,definition,(
% 0.17/0.61 sP6_prd<=>(((![W0]: (~aElement0(W0)|~sdtasdt0(xa,W0)=sz00))&~aElementOf0(sz00,slsdtgt0(xa)))|((![W0]: (~aElement0(W0)|~sdtasdt0(xa,W0)=xa))&~aElementOf0(xa,slsdtgt0(xa))))),
% 0.17/0.61 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.17/0.61 fof(f271,plain,(
% 0.17/0.61 sP4_prd<=>(sP6_prd|((![W0]: (~aElement0(W0)|~sdtasdt0(xb,W0)=sz00))&~aElementOf0(sz00,slsdtgt0(xb))))),
% 0.17/0.61 inference(formula_renaming,[status(thm)],[f238,f270])).
% 0.17/0.61 fof(f272,plain,(
% 0.17/0.61 (~sP4_prd|(sP6_prd|((![W0]: (~aElement0(W0)|~sdtasdt0(xb,W0)=sz00))&~aElementOf0(sz00,slsdtgt0(xb)))))&(sP4_prd|(~sP6_prd&((?[W0]: (aElement0(W0)&sdtasdt0(xb,W0)=sz00))|aElementOf0(sz00,slsdtgt0(xb)))))),
% 0.17/0.61 inference(NNF_transformation,[status(thm)],[f271])).
% 0.17/0.61 fof(f273,plain,(
% 0.17/0.61 (~sP4_prd|(sP6_prd|((![W0]: (~aElement0(W0)|~sdtasdt0(xb,W0)=sz00))&~aElementOf0(sz00,slsdtgt0(xb)))))&(sP4_prd|(~sP6_prd&((aElement0(sK28_skl)&sdtasdt0(xb,sK28_skl)=sz00)|aElementOf0(sz00,slsdtgt0(xb)))))),
% 0.17/0.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl]),skolemize(W0,sK28_skl)],[f272])).
% 0.17/0.61 fof(f275,plain,(
% 0.17/0.61 ~sP4_prd|sP6_prd|~aElementOf0(sz00,slsdtgt0(xb))),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f273])).
% 0.17/0.61 fof(f288,plain,(
% 0.17/0.61 (~sP6_prd|(((![W0]: (~aElement0(W0)|~sdtasdt0(xa,W0)=sz00))&~aElementOf0(sz00,slsdtgt0(xa)))|((![W0]: (~aElement0(W0)|~sdtasdt0(xa,W0)=xa))&~aElementOf0(xa,slsdtgt0(xa)))))&(sP6_prd|(((?[W0]: (aElement0(W0)&sdtasdt0(xa,W0)=sz00))|aElementOf0(sz00,slsdtgt0(xa)))&((?[W0]: (aElement0(W0)&sdtasdt0(xa,W0)=xa))|aElementOf0(xa,slsdtgt0(xa)))))),
% 0.17/0.61 inference(NNF_transformation,[status(thm)],[f270])).
% 0.17/0.61 fof(f289,plain,(
% 0.17/0.61 (~sP6_prd|(((![W0]: (~aElement0(W0)|~sdtasdt0(xa,W0)=sz00))&~aElementOf0(sz00,slsdtgt0(xa)))|((![W0]: (~aElement0(W0)|~sdtasdt0(xa,W0)=xa))&~aElementOf0(xa,slsdtgt0(xa)))))&(sP6_prd|(((aElement0(sK30_skl)&sdtasdt0(xa,sK30_skl)=sz00)|aElementOf0(sz00,slsdtgt0(xa)))&((aElement0(sK31_skl)&sdtasdt0(xa,sK31_skl)=xa)|aElementOf0(xa,slsdtgt0(xa)))))),
% 0.17/0.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK30_skl,sK31_skl]),skolemize(W0,sK30_skl),skolemize(W0,sK31_skl)],[f288])).
% 0.17/0.61 fof(f290,plain,(
% 0.17/0.61 ![X0,X1]: (~sP6_prd|~aElement0(X0)|~sdtasdt0(xa,X0)=sz00|~aElement0(X1)|~sdtasdt0(xa,X1)=xa)),
% 0.17/0.61 inference(cnf_transformation,[status(thm)],[f289])).
% 0.17/0.61 fof(f305,definition,(
% 0.17/0.61 sQ2_spl <=> (sP4_prd)),
% 0.17/0.61 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.17/0.61 fof(f308,definition,(
% 0.17/0.61 ![X0]: (sQ3_spl <=> (~aElement0(X0)|~sdtasdt0(xb,X0)=xb))),
% 0.17/0.61 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.17/0.61 fof(f309,plain,(
% 0.17/0.61 ![X0]: (~aElement0(X0)|~sdtasdt0(xb,X0)=xb|~sQ3_spl)),
% 0.17/0.61 inference(component_clause,[status(thm)],[f308])).
% 0.17/0.61 fof(f311,plain,(
% 0.17/0.61 sQ2_spl|sQ3_spl),
% 0.17/0.61 inference(split_clause,[status(thm)],[f240,f305,f308])).
% 0.17/0.61 fof(f316,definition,(
% 0.17/0.61 sQ5_spl <=> (sP6_prd)),
% 0.17/0.61 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.17/0.61 fof(f323,definition,(
% 0.17/0.61 sQ7_spl <=> (aElementOf0(sz00,slsdtgt0(xb)))),
% 0.17/0.61 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.17/0.61 fof(f326,plain,(
% 0.17/0.61 ~sQ2_spl|sQ5_spl|~sQ7_spl),
% 0.17/0.61 inference(split_clause,[status(thm)],[f275,f305,f316,f323])).
% 0.17/0.61 fof(f336,definition,(
% 0.17/0.61 ![X0]: (sQ10_spl <=> (~aElement0(X0)|~sdtasdt0(xa,X0)=sz00))),
% 0.17/0.61 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.17/0.61 fof(f337,plain,(
% 0.17/0.61 ![X0]: (~aElement0(X0)|~sdtasdt0(xa,X0)=sz00|~sQ10_spl)),
% 0.17/0.61 inference(component_clause,[status(thm)],[f336])).
% 0.17/0.61 fof(f339,definition,(
% 0.17/0.61 ![X1]: (sQ11_spl <=> (~aElement0(X1)|~sdtasdt0(xa,X1)=xa))),
% 0.17/0.61 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.17/0.61 fof(f340,plain,(
% 0.17/0.61 ![X0]: (~aElement0(X0)|~sdtasdt0(xa,X0)=xa|~sQ11_spl)),
% 0.17/0.61 inference(component_clause,[status(thm)],[f339])).
% 0.17/0.61 fof(f342,plain,(
% 0.17/0.61 ~sQ5_spl|sQ10_spl|sQ11_spl),
% 0.17/0.61 inference(split_clause,[status(thm)],[f290,f316,f336,f339])).
% 0.17/0.61 fof(f381,plain,(
% 0.17/0.61 ![X0]: (aElementOf0(sdtasdt0(xb,X0),slsdtgt0(xb))|~aElement0(X0))),
% 0.17/0.61 inference(destructive_equality_resolution,[status(thm)],[f231])).
% 0.17/0.61 fof(f384,plain,(
% 0.17/0.61 ~sdtasdt0(xa,sz00)=sz00|~sQ10_spl),
% 0.17/0.61 inference(resolution,[status(thm)],[f48,f337])).
% 0.17/0.61 fof(f419,plain,(
% 0.17/0.61 ~sdtasdt0(xa,sz10)=xa|~sQ11_spl),
% 0.17/0.61 inference(resolution,[status(thm)],[f340,f49])).
% 0.17/0.61 fof(f461,plain,(
% 0.17/0.61 sdtasdt0(xb,sz00)=sz00),
% 0.17/0.61 inference(resolution,[status(thm)],[f80,f198])).
% 0.17/0.61 fof(f462,plain,(
% 0.17/0.61 sdtasdt0(xa,sz00)=sz00),
% 0.17/0.61 inference(resolution,[status(thm)],[f80,f197])).
% 0.17/0.61 fof(f464,plain,(
% 0.17/0.61 $false|~sQ10_spl),
% 0.17/0.61 inference(forward_subsumption_resolution,[status(thm)],[f462,f384])).
% 0.17/0.61 fof(f465,plain,(
% 0.17/0.61 ~sQ10_spl),
% 0.17/0.61 inference(contradiction_clause,[status(thm)],[f464])).
% 0.17/0.61 fof(f556,definition,(
% 0.17/0.61 sQ18_spl <=> (aElement0(sK21_skl))),
% 0.17/0.61 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.17/0.61 fof(f558,plain,(
% 0.17/0.61 ~aElement0(sK21_skl)|sQ18_spl),
% 0.17/0.61 inference(component_clause,[status(thm)],[f556])).
% 0.17/0.61 fof(f559,definition,(
% 0.17/0.61 sQ19_spl <=> (aElement0(sz00))),
% 0.17/0.61 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.17/0.61 fof(f561,plain,(
% 0.17/0.61 ~aElement0(sz00)|sQ19_spl),
% 0.17/0.61 inference(component_clause,[status(thm)],[f559])).
% 0.17/0.61 fof(f564,definition,(
% 0.17/0.61 sQ20_spl <=> (aElement0(sK20_skl))),
% 0.17/0.61 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.17/0.61 fof(f566,plain,(
% 0.17/0.61 ~aElement0(sK20_skl)|sQ20_spl),
% 0.17/0.61 inference(component_clause,[status(thm)],[f564])).
% 0.17/0.61 fof(f574,definition,(
% 0.17/0.61 sQ22_spl <=> (aElement0(sz10))),
% 0.17/0.61 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.17/0.61 fof(f576,plain,(
% 0.17/0.61 ~aElement0(sz10)|sQ22_spl),
% 0.17/0.61 inference(component_clause,[status(thm)],[f574])).
% 0.17/0.61 fof(f675,plain,(
% 0.17/0.61 $false|sQ19_spl),
% 0.17/0.61 inference(forward_subsumption_resolution,[status(thm)],[f561,f48])).
% 0.17/0.61 fof(f676,plain,(
% 0.17/0.61 sQ19_spl),
% 0.17/0.61 inference(contradiction_clause,[status(thm)],[f675])).
% 0.17/0.61 fof(f747,plain,(
% 0.17/0.62 sdtasdt0(xb,sz10)=xb),
% 0.17/0.62 inference(resolution,[status(thm)],[f71,f198])).
% 0.17/0.62 fof(f748,plain,(
% 0.17/0.62 sdtasdt0(xa,sz10)=xa),
% 0.17/0.62 inference(resolution,[status(thm)],[f71,f197])).
% 0.17/0.62 fof(f749,plain,(
% 0.17/0.62 $false|~sQ11_spl),
% 0.17/0.62 inference(forward_subsumption_resolution,[status(thm)],[f748,f419])).
% 0.17/0.62 fof(f750,plain,(
% 0.17/0.62 ~sQ11_spl),
% 0.17/0.62 inference(contradiction_clause,[status(thm)],[f749])).
% 0.17/0.62 fof(f1034,plain,(
% 0.17/0.62 $false|sQ22_spl),
% 0.17/0.62 inference(forward_subsumption_resolution,[status(thm)],[f576,f49])).
% 0.17/0.62 fof(f1035,plain,(
% 0.17/0.62 sQ22_spl),
% 0.17/0.62 inference(contradiction_clause,[status(thm)],[f1034])).
% 0.17/0.62 fof(f1092,plain,(
% 0.17/0.62 aElementOf0(sz00,slsdtgt0(xb))|~aElement0(sz00)),
% 0.17/0.62 inference(paramodulation,[status(thm)],[f461,f381])).
% 0.17/0.62 fof(f1096,plain,(
% 0.17/0.62 sQ7_spl|~sQ19_spl),
% 0.17/0.62 inference(split_clause,[status(thm)],[f1092,f323,f559])).
% 0.17/0.62 fof(f1144,plain,(
% 0.17/0.62 $false|sQ20_spl),
% 0.17/0.62 inference(forward_subsumption_resolution,[status(thm)],[f566,f205])).
% 0.17/0.62 fof(f1145,plain,(
% 0.17/0.62 sQ20_spl),
% 0.17/0.62 inference(contradiction_clause,[status(thm)],[f1144])).
% 0.17/0.62 fof(f1153,plain,(
% 0.17/0.62 $false|sQ18_spl),
% 0.17/0.62 inference(forward_subsumption_resolution,[status(thm)],[f558,f210])).
% 0.17/0.62 fof(f1154,plain,(
% 0.17/0.62 sQ18_spl),
% 0.17/0.62 inference(contradiction_clause,[status(thm)],[f1153])).
% 0.17/0.62 fof(f1155,plain,(
% 0.17/0.62 ~aElement0(sz10)|~sQ3_spl),
% 0.17/0.62 inference(resolution,[status(thm)],[f747,f309])).
% 0.17/0.62 fof(f1160,plain,(
% 0.17/0.62 ~sQ22_spl|~sQ3_spl),
% 0.17/0.62 inference(split_clause,[status(thm)],[f1155,f574,f308])).
% 0.17/0.62 fof(f1168,plain,(
% 0.17/0.62 $false),
% 0.17/0.62 inference(sat_refutation,[status(thm)],[f311,f326,f342,f465,f676,f750,f1035,f1096,f1145,f1154,f1160])).
% 0.17/0.62 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/0.64 % Elapsed time: 0.190221 seconds
% 0.17/0.64 % CPU time: 0.850627 seconds
% 0.17/0.64 % Total memory used: 117.051 MB
% 0.17/0.64 % Net memory used: 116.162 MB
%------------------------------------------------------------------------------