%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM631+3 : 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 : n009.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 01:43:24 PM UTC 2026
% Result : Theorem 29.24s 4.13s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM631+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 02:45:27 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 29.24/4.13 % Refutation found
% 29.24/4.13 % SZS status Theorem for theBenchmark: Theorem is valid
% 29.24/4.13 % SZS output start CNFRefutation for theBenchmark
% 29.24/4.13 fof(f17,axiom,(
% 29.24/4.13 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) )) )),
% 29.24/4.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.24/4.13 fof(f91,hypothesis,(
% 29.24/4.13 ( aFunction0(xe)& szDzozmdt0(xe) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aElementOf0(sdtlpdtrp0(xe,W0),sdtlpdtrp0(xN,W0))& (! [W1] :( aElementOf0(W1,sdtlpdtrp0(xN,W0))=> sdtlseqdt0(sdtlpdtrp0(xe,W0),W1) ))& sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0)) ) ) )) ),
% 29.24/4.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.24/4.13 fof(f92,hypothesis,(
% 29.24/4.13 ( aFunction0(xd)& szDzozmdt0(xd) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> (! [W1] :( ( aSet0(W1)& ( ( ( (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,sdtlpdtrp0(xN,szszuzczcdt0(W0))) ))| aSubsetOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))) )& sbrdtbr0(W1) = xk )| aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk)) ) )=> sdtlpdtrp0(xd,W0) = sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) ) )) )) ),
% 29.24/4.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.24/4.14 fof(f99,hypothesis,(
% 29.24/4.14 ( aSet0(xQ)& (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,xO) ))& aSubsetOf0(xQ,xO)& sbrdtbr0(xQ) = xK& aElementOf0(xQ,slbdtsldtrb0(xO,xK)) ) ),
% 29.24/4.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.24/4.14 fof(f103,hypothesis,(
% 29.24/4.14 ( aElementOf0(xp,xQ)& (! [W0] :( aElementOf0(W0,xQ)=> sdtlseqdt0(xp,W0) ))& xp = szmzizndt0(xQ) ) ),
% 29.24/4.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.24/4.14 fof(f104,hypothesis,(
% 29.24/4.14 ( aSet0(xP)& (! [W0] :( aElementOf0(W0,xQ)=> sdtlseqdt0(szmzizndt0(xQ),W0) ))& (! [W0] :( aElementOf0(W0,xP)<=> ( aElement0(W0)& aElementOf0(W0,xQ)& W0 != szmzizndt0(xQ) ) ))& xP = sdtmndt0(xQ,szmzizndt0(xQ)) ) ),
% 29.24/4.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.24/4.14 fof(f109,hypothesis,(
% 29.24/4.14 sbrdtbr0(xP) = xk ),
% 29.24/4.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.24/4.14 fof(f111,hypothesis,(
% 29.24/4.14 ( aElementOf0(xn,szDzozmdt0(xd))& sdtlpdtrp0(xd,xn) = szDzizrdt0(xd)& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))& aElementOf0(xn,szNzAzT0)& sdtlpdtrp0(xe,xn) = xp ) ),
% 29.24/4.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.24/4.14 fof(f113,hypothesis,(
% 29.24/4.14 ( (! [W0] :( aElementOf0(W0,xP)=> aElementOf0(W0,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ))& aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ) ),
% 29.24/4.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.24/4.14 fof(f116,hypothesis,(
% 29.24/4.14 ( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xn))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0) ))& aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))& (! [W0] :( aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))<=> ( aElement0(W0)& ( aElementOf0(W0,xP)| W0 = szmzizndt0(sdtlpdtrp0(xN,xn)) ) ) ))& sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) ) ),
% 29.24/4.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.24/4.14 fof(f117,conjecture,(
% 29.24/4.14 sdtlpdtrp0(xc,xQ) = sdtlpdtrp0(xd,xn) ),
% 29.24/4.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 29.24/4.14 fof(f118,negated_conjecture,(
% 29.24/4.14 ~(sdtlpdtrp0(xc,xQ) = sdtlpdtrp0(xd,xn) )),
% 29.24/4.14 inference(negated_conjecture,[status(cth)],[f117])).
% 29.24/4.14 fof(f183,plain,(
% 29.24/4.14 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|sdtpldt0(sdtmndt0(W0,W1),W1)=W0)))),
% 29.24/4.14 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 29.24/4.14 fof(f184,plain,(
% 29.24/4.14 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|sdtpldt0(sdtmndt0(X0,X1),X1)=X0)),
% 29.24/4.14 inference(cnf_transformation,[status(thm)],[f183])).
% 29.24/4.14 fof(f550,plain,(
% 29.24/4.14 (aFunction0(xe)&szDzozmdt0(xe)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|((aElementOf0(sdtlpdtrp0(xe,W0),sdtlpdtrp0(xN,W0))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(sdtlpdtrp0(xe,W0),W1))))&sdtlpdtrp0(xe,W0)=szmzizndt0(sdtlpdtrp0(xN,W0)))))),
% 29.24/4.14 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 29.24/4.14 fof(f555,plain,(
% 29.24/4.14 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlpdtrp0(xe,X0)=szmzizndt0(sdtlpdtrp0(xN,X0)))),
% 29.24/4.14 inference(cnf_transformation,[status(thm)],[f550])).
% 29.24/4.14 fof(f556,plain,(
% 29.24/4.14 (aFunction0(xd)&szDzozmdt0(xd)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(![W1]: ((~aSet0(W1)|((((?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,sdtlpdtrp0(xN,szszuzczcdt0(W0)))))&~aSubsetOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))))|~sbrdtbr0(W1)=xk)&~aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))))|sdtlpdtrp0(xd,W0)=sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)))))),
% 29.24/4.14 inference(pre_NNF_transformation,[status(thm)],[f92])).
% 29.24/4.14 fof(f557,plain,(
% 29.24/4.14 (aFunction0(xd)&szDzozmdt0(xd)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(![W1]: ((~aSet0(W1)|((((aElementOf0(sK32_skl(W1,W0),W1)&~aElementOf0(sK32_skl(W1,W0),sdtlpdtrp0(xN,szszuzczcdt0(W0))))&~aSubsetOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0))))|~sbrdtbr0(W1)=xk)&~aElementOf0(W1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),xk))))|sdtlpdtrp0(xd,W0)=sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)))))),
% 29.24/4.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK32_skl]),skolemize(W2,sK32_skl(W1,W0))],[f556])).
% 29.24/4.14 fof(f562,plain,(
% 29.24/4.14 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aSet0(X1)|~aSubsetOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(X0)))|~sbrdtbr0(X1)=xk|sdtlpdtrp0(xd,X0)=sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1))),
% 29.24/4.14 inference(cnf_transformation,[status(thm)],[f557])).
% 29.24/4.14 fof(f606,plain,(
% 29.24/4.14 (((aSet0(xQ)&(![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,xO))))&aSubsetOf0(xQ,xO))&sbrdtbr0(xQ)=xK)&aElementOf0(xQ,slbdtsldtrb0(xO,xK))),
% 29.24/4.14 inference(pre_NNF_transformation,[status(thm)],[f99])).
% 29.24/4.14 fof(f607,plain,(
% 29.24/4.14 aSet0(xQ)),
% 29.24/4.14 inference(cnf_transformation,[status(thm)],[f606])).
% 29.24/4.14 fof(f626,plain,(
% 29.24/4.14 (aElementOf0(xp,xQ)&(![W0]: (~aElementOf0(W0,xQ)|sdtlseqdt0(xp,W0))))&xp=szmzizndt0(xQ)),
% 29.24/4.14 inference(pre_NNF_transformation,[status(thm)],[f103])).
% 29.24/4.14 fof(f627,plain,(
% 29.24/4.14 aElementOf0(xp,xQ)),
% 29.24/4.14 inference(cnf_transformation,[status(thm)],[f626])).
% 29.24/4.14 fof(f629,plain,(
% 29.24/4.14 xp=szmzizndt0(xQ)),
% 29.24/4.14 inference(cnf_transformation,[status(thm)],[f626])).
% 29.24/4.14 fof(f630,plain,(
% 29.24/4.14 ((aSet0(xP)&(![W0]: (~aElementOf0(W0,xQ)|sdtlseqdt0(szmzizndt0(xQ),W0))))&(![W0]: (aElementOf0(W0,xP)<=>((aElement0(W0)&aElementOf0(W0,xQ))&~W0=szmzizndt0(xQ)))))&xP=sdtmndt0(xQ,szmzizndt0(xQ))),
% 29.24/4.14 inference(pre_NNF_transformation,[status(thm)],[f104])).
% 29.24/4.14 fof(f631,plain,(
% 29.24/4.14 ((aSet0(xP)&(![W0]: (~aElementOf0(W0,xQ)|sdtlseqdt0(szmzizndt0(xQ),W0))))&(![W0]: ((~aElementOf0(W0,xP)|((aElement0(W0)&aElementOf0(W0,xQ))&~W0=szmzizndt0(xQ)))&(aElementOf0(W0,xP)|((~aElement0(W0)|~aElementOf0(W0,xQ))|W0=szmzizndt0(xQ))))))&xP=sdtmndt0(xQ,szmzizndt0(xQ))),
% 29.24/4.14 inference(NNF_transformation,[status(thm)],[f630])).
% 29.24/4.14 fof(f632,plain,(
% 29.24/4.14 ((aSet0(xP)&(![W0]: (~aElementOf0(W0,xQ)|sdtlseqdt0(szmzizndt0(xQ),W0))))&((![W0]: (~aElementOf0(W0,xP)|((aElement0(W0)&aElementOf0(W0,xQ))&~W0=szmzizndt0(xQ))))&(![W0]: (aElementOf0(W0,xP)|((~aElement0(W0)|~aElementOf0(W0,xQ))|W0=szmzizndt0(xQ))))))&xP=sdtmndt0(xQ,szmzizndt0(xQ))),
% 29.24/4.14 inference(miniscoping,[status(thm)],[f631])).
% 29.24/4.14 fof(f633,plain,(
% 29.24/4.14 aSet0(xP)),
% 29.24/4.14 inference(cnf_transformation,[status(thm)],[f632])).
% 29.24/4.14 fof(f639,plain,(
% 29.24/4.14 xP=sdtmndt0(xQ,szmzizndt0(xQ))),
% 29.24/4.14 inference(cnf_transformation,[status(thm)],[f632])).
% 29.24/4.14 fof(f650,plain,(
% 29.24/4.14 sbrdtbr0(xP)=xk),
% 29.24/4.14 inference(cnf_transformation,[status(thm)],[f109])).
% 29.24/4.14 fof(f653,plain,(
% 29.24/4.14 sdtlpdtrp0(xd,xn)=szDzizrdt0(xd)),
% 29.24/4.14 inference(cnf_transformation,[status(thm)],[f111])).
% 29.24/4.14 fof(f655,plain,(
% 29.24/4.14 aElementOf0(xn,szNzAzT0)),
% 29.24/4.14 inference(cnf_transformation,[status(thm)],[f111])).
% 29.24/4.14 fof(f656,plain,(
% 29.24/4.14 sdtlpdtrp0(xe,xn)=xp),
% 29.24/4.14 inference(cnf_transformation,[status(thm)],[f111])).
% 29.24/4.14 fof(f658,plain,(
% 29.24/4.14 (![W0]: (~aElementOf0(W0,xP)|aElementOf0(W0,sdtlpdtrp0(xN,szszuzczcdt0(xn)))))&aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 29.24/4.14 inference(pre_NNF_transformation,[status(thm)],[f113])).
% 29.24/4.14 fof(f660,plain,(
% 29.24/4.14 aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 29.24/4.14 inference(cnf_transformation,[status(thm)],[f658])).
% 29.24/4.14 fof(f675,plain,(
% 29.24/4.14 (((![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xn))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)))&aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))))&(![W0]: (aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))<=>(aElement0(W0)&(aElementOf0(W0,xP)|W0=szmzizndt0(sdtlpdtrp0(xN,xn)))))))&sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))=sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)),
% 29.24/4.14 inference(pre_NNF_transformation,[status(thm)],[f116])).
% 29.24/4.15 fof(f676,plain,(
% 29.24/4.15 (((![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xn))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)))&aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))))&(![W0]: ((~aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))|(aElement0(W0)&(aElementOf0(W0,xP)|W0=szmzizndt0(sdtlpdtrp0(xN,xn)))))&(aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))|(~aElement0(W0)|(~aElementOf0(W0,xP)&~W0=szmzizndt0(sdtlpdtrp0(xN,xn))))))))&sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))=sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)),
% 29.24/4.15 inference(NNF_transformation,[status(thm)],[f675])).
% 29.24/4.15 fof(f677,plain,(
% 29.24/4.15 (((![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xn))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)))&aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))))&((![W0]: (~aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))|(aElement0(W0)&(aElementOf0(W0,xP)|W0=szmzizndt0(sdtlpdtrp0(xN,xn))))))&(![W0]: (aElementOf0(W0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))|(~aElement0(W0)|(~aElementOf0(W0,xP)&~W0=szmzizndt0(sdtlpdtrp0(xN,xn))))))))&sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))=sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)),
% 29.24/4.15 inference(miniscoping,[status(thm)],[f676])).
% 29.24/4.15 fof(f684,plain,(
% 29.24/4.15 sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))))=sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)),
% 29.24/4.15 inference(cnf_transformation,[status(thm)],[f677])).
% 29.24/4.15 fof(f685,plain,(
% 29.24/4.15 ~sdtlpdtrp0(xc,xQ)=sdtlpdtrp0(xd,xn)),
% 29.24/4.15 inference(cnf_transformation,[status(thm)],[f118])).
% 29.24/4.15 fof(f1114,plain,(
% 29.24/4.15 ![X0]: (~aElementOf0(X0,xQ)|sdtpldt0(sdtmndt0(xQ,X0),X0)=xQ)),
% 29.24/4.15 inference(resolution,[status(thm)],[f184,f607])).
% 29.24/4.15 fof(f1897,plain,(
% 29.24/4.15 sdtpldt0(sdtmndt0(xQ,xp),xp)=xQ),
% 29.24/4.15 inference(resolution,[status(thm)],[f627,f1114])).
% 29.24/4.15 fof(f6603,plain,(
% 29.24/4.15 sdtlpdtrp0(xe,xn)=szmzizndt0(sdtlpdtrp0(xN,xn))),
% 29.24/4.15 inference(resolution,[status(thm)],[f555,f655])).
% 29.24/4.15 fof(f6606,plain,(
% 29.24/4.15 xp=szmzizndt0(sdtlpdtrp0(xN,xn))),
% 29.24/4.15 inference(forward_demodulation,[status(thm)],[f656,f6603])).
% 29.24/4.15 fof(f6809,plain,(
% 29.24/4.15 sdtpldt0(xP,xp)=xQ),
% 29.24/4.15 inference(backward_demodulation,[status(thm)],[f6810,f1897])).
% 29.24/4.15 fof(f6810,plain,(
% 29.24/4.15 xP=sdtmndt0(xQ,xp)),
% 29.24/4.15 inference(forward_demodulation,[status(thm)],[f629,f639])).
% 29.24/4.15 fof(f6949,plain,(
% 29.24/4.15 ~sdtlpdtrp0(xc,xQ)=szDzizrdt0(xd)),
% 29.24/4.15 inference(backward_demodulation,[status(thm)],[f653,f685])).
% 29.24/4.15 fof(f7317,plain,(
% 29.24/4.15 ~aElementOf0(xn,szNzAzT0)|~aSet0(xP)|~sbrdtbr0(xP)=xk|sdtlpdtrp0(xd,xn)=sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)),
% 29.24/4.15 inference(resolution,[status(thm)],[f660,f562])).
% 29.24/4.15 fof(f7324,plain,(
% 29.24/4.15 ~aElementOf0(xn,szNzAzT0)|~aSet0(xP)|~xk=xk|sdtlpdtrp0(xd,xn)=sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)),
% 29.24/4.15 inference(forward_demodulation,[status(thm)],[f650,f7317])).
% 29.24/4.15 fof(f7325,plain,(
% 29.24/4.15 ~aElementOf0(xn,szNzAzT0)|~aSet0(xP)|~xk=xk|szDzizrdt0(xd)=sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)),
% 29.24/4.15 inference(forward_demodulation,[status(thm)],[f653,f7324])).
% 29.24/4.15 fof(f7326,plain,(
% 29.24/4.15 ~aElementOf0(xn,szNzAzT0)|~aSet0(xP)|szDzizrdt0(xd)=sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)),
% 29.24/4.15 inference(trivial_equality_resolution,[status(thm)],[f7325])).
% 29.24/4.15 fof(f7327,plain,(
% 29.24/4.15 ~aSet0(xP)|szDzizrdt0(xd)=sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)),
% 29.24/4.15 inference(forward_subsumption_resolution,[status(thm)],[f7326,f655])).
% 29.24/4.15 fof(f7709,plain,(
% 29.24/4.15 sdtlpdtrp0(xc,sdtpldt0(xP,xp))=sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)),
% 29.24/4.15 inference(forward_demodulation,[status(thm)],[f6606,f684])).
% 29.24/4.15 fof(f7710,plain,(
% 29.24/4.15 sdtlpdtrp0(xc,xQ)=sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)),
% 29.24/4.15 inference(forward_demodulation,[status(thm)],[f6809,f7709])).
% 29.24/4.15 fof(f7748,plain,(
% 29.24/4.15 ~aSet0(xP)|szDzizrdt0(xd)=sdtlpdtrp0(xc,xQ)),
% 29.24/4.15 inference(forward_demodulation,[status(thm)],[f7710,f7327])).
% 29.24/4.15 fof(f7750,plain,(
% 29.24/4.15 ~szDzizrdt0(xd)=szDzizrdt0(xd)),
% 29.24/4.15 inference(backward_demodulation,[status(thm)],[f7752,f6949])).
% 29.24/4.15 fof(f7752,plain,(
% 29.24/4.15 szDzizrdt0(xd)=sdtlpdtrp0(xc,xQ)),
% 29.24/4.15 inference(forward_subsumption_resolution,[status(thm)],[f7748,f633])).
% 29.24/4.15 fof(f7758,plain,(
% 29.24/4.15 $false),
% 29.24/4.15 inference(trivial_equality_resolution,[status(thm)],[f7750])).
% 29.24/4.15 % SZS output end CNFRefutation for theBenchmark.p
% 29.24/4.17 % Elapsed time: 3.801995 seconds
% 29.24/4.17 % CPU time: 29.606862 seconds
% 29.24/4.17 % Total memory used: 329.759 MB
% 29.24/4.17 % Net memory used: 314.399 MB
%------------------------------------------------------------------------------