%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM609+1 : 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:20 PM UTC 2026
% Result : Theorem 6.29s 1.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM609+1 : 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.10/0.35 % Computer : n009.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 02:44:27 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 6.29/1.32 % Refutation found
% 6.29/1.32 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.29/1.32 % SZS output start CNFRefutation for theBenchmark
% 6.29/1.32 fof(f3,axiom,(
% 6.29/1.32 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 6.29/1.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.29/1.32 fof(f10,definition,(
% 6.29/1.32 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 6.29/1.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.29/1.32 fof(f15,definition,(
% 6.29/1.32 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtpldt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& ( aElementOf0(W3,W0)| W3 = W1 ) ) ) )) ) )) )),
% 6.29/1.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.29/1.32 fof(f17,axiom,(
% 6.29/1.32 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) )) )),
% 6.29/1.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.29/1.32 fof(f23,axiom,(
% 6.29/1.32 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 6.29/1.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.29/1.32 fof(f101,hypothesis,(
% 6.29/1.32 aSubsetOf0(xQ,szNzAzT0) ),
% 6.29/1.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.29/1.32 fof(f103,hypothesis,(
% 6.29/1.32 xp = szmzizndt0(xQ) ),
% 6.29/1.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.29/1.32 fof(f104,hypothesis,(
% 6.29/1.32 ( aSet0(xP)& xP = sdtmndt0(xQ,szmzizndt0(xQ)) ) ),
% 6.29/1.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.29/1.32 fof(f105,hypothesis,(
% 6.29/1.32 aElementOf0(xp,xQ) ),
% 6.29/1.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.29/1.32 fof(f107,conjecture,(
% 6.29/1.32 aSubsetOf0(xP,xQ) ),
% 6.29/1.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.29/1.32 fof(f108,negated_conjecture,(
% 6.29/1.32 ~(aSubsetOf0(xP,xQ) )),
% 6.29/1.32 inference(negated_conjecture,[status(cth)],[f107])).
% 6.29/1.32 fof(f115,plain,(
% 6.29/1.32 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 6.29/1.32 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 6.29/1.32 fof(f116,plain,(
% 6.29/1.32 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 6.29/1.32 inference(cnf_transformation,[status(thm)],[f115])).
% 6.29/1.32 fof(f133,plain,(
% 6.29/1.32 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 6.29/1.32 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 6.29/1.32 fof(f134,plain,(
% 6.29/1.32 ![W0]: (~aSet0(W0)|(![W1]: ((~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))&(aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 6.29/1.32 inference(NNF_transformation,[status(thm)],[f133])).
% 6.29/1.32 fof(f135,plain,(
% 6.29/1.32 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 6.29/1.32 inference(miniscoping,[status(thm)],[f134])).
% 6.29/1.32 fof(f136,plain,(
% 6.29/1.32 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(aElementOf0(sK1_skl(W1,W0),W1)&~aElementOf0(sK1_skl(W1,W0),W0)))))))),
% 6.29/1.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f135])).
% 6.29/1.32 fof(f137,plain,(
% 6.29/1.32 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 6.29/1.32 inference(cnf_transformation,[status(thm)],[f136])).
% 6.29/1.32 fof(f139,plain,(
% 6.29/1.32 ![X0,X1]: (~aSet0(X0)|aSubsetOf0(X1,X0)|~aSet0(X1)|aElementOf0(sK1_skl(X1,X0),X1))),
% 6.29/1.32 inference(cnf_transformation,[status(thm)],[f136])).
% 6.29/1.32 fof(f140,plain,(
% 6.29/1.32 ![X0,X1]: (~aSet0(X0)|aSubsetOf0(X1,X0)|~aSet0(X1)|~aElementOf0(sK1_skl(X1,X0),X0))),
% 6.29/1.32 inference(cnf_transformation,[status(thm)],[f136])).
% 6.29/1.32 fof(f149,plain,(
% 6.29/1.32 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtpldt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))),
% 6.29/1.32 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 6.29/1.32 fof(f150,plain,(
% 6.29/1.32 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: ((~W2=sdtpldt0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1)))&(aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))))))&(W2=sdtpldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))&(aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))))),
% 6.29/1.32 inference(NNF_transformation,[status(thm)],[f149])).
% 6.29/1.32 fof(f151,plain,(
% 6.29/1.32 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtpldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))&(![W3]: (aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1))))))))&(![W2]: (W2=sdtpldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))&(aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))))),
% 6.29/1.32 inference(miniscoping,[status(thm)],[f150])).
% 6.29/1.32 fof(f152,plain,(
% 6.29/1.32 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtpldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))&(![W3]: (aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1))))))))&(![W2]: (W2=sdtpldt0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK2_skl(W2,W1,W0),W2)|(~aElement0(sK2_skl(W2,W1,W0))|(~aElementOf0(sK2_skl(W2,W1,W0),W0)&~sK2_skl(W2,W1,W0)=W1)))&(aElementOf0(sK2_skl(W2,W1,W0),W2)|(aElement0(sK2_skl(W2,W1,W0))&(aElementOf0(sK2_skl(W2,W1,W0),W0)|sK2_skl(W2,W1,W0)=W1)))))))))),
% 6.29/1.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W3,sK2_skl(W2,W1,W0))],[f151])).
% 6.29/1.32 fof(f156,plain,(
% 6.29/1.32 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtpldt0(X0,X1)|aElementOf0(X3,X2)|~aElement0(X3)|~aElementOf0(X3,X0))),
% 6.29/1.32 inference(cnf_transformation,[status(thm)],[f152])).
% 6.29/1.32 fof(f173,plain,(
% 6.29/1.32 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|sdtpldt0(sdtmndt0(W0,W1),W1)=W0)))),
% 6.29/1.32 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 6.29/1.32 fof(f174,plain,(
% 6.29/1.32 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|sdtpldt0(sdtmndt0(X0,X1),X1)=X0)),
% 6.29/1.32 inference(cnf_transformation,[status(thm)],[f173])).
% 6.29/1.32 fof(f185,plain,(
% 6.29/1.32 aSet0(szNzAzT0)),
% 6.29/1.32 inference(cnf_transformation,[status(thm)],[f23])).
% 6.29/1.32 fof(f442,plain,(
% 6.29/1.32 aSubsetOf0(xQ,szNzAzT0)),
% 6.29/1.32 inference(cnf_transformation,[status(thm)],[f101])).
% 6.29/1.32 fof(f444,plain,(
% 6.29/1.32 xp=szmzizndt0(xQ)),
% 6.29/1.32 inference(cnf_transformation,[status(thm)],[f103])).
% 6.29/1.32 fof(f445,plain,(
% 6.29/1.32 aSet0(xP)),
% 6.29/1.32 inference(cnf_transformation,[status(thm)],[f104])).
% 6.29/1.32 fof(f446,plain,(
% 6.29/1.32 xP=sdtmndt0(xQ,szmzizndt0(xQ))),
% 6.29/1.32 inference(cnf_transformation,[status(thm)],[f104])).
% 6.29/1.32 fof(f447,plain,(
% 6.29/1.32 aElementOf0(xp,xQ)),
% 6.29/1.32 inference(cnf_transformation,[status(thm)],[f105])).
% 6.29/1.32 fof(f449,plain,(
% 6.29/1.32 ~aSubsetOf0(xP,xQ)),
% 6.29/1.32 inference(cnf_transformation,[status(thm)],[f108])).
% 6.29/1.32 fof(f462,plain,(
% 6.29/1.32 ~aSet0(szNzAzT0)|aSet0(xQ)),
% 6.29/1.32 inference(resolution,[status(thm)],[f137,f442])).
% 6.29/1.32 fof(f480,plain,(
% 6.29/1.32 aSet0(xQ)),
% 6.29/1.32 inference(backward_subsumption_resolution,[status(thm)],[f462,f185])).
% 6.29/1.32 fof(f555,plain,(
% 6.29/1.32 xP=sdtmndt0(xQ,xp)),
% 6.29/1.32 inference(backward_demodulation,[status(thm)],[f444,f446])).
% 6.29/1.32 fof(f559,plain,(
% 6.29/1.32 ~aSet0(xQ)|aElement0(xp)),
% 6.29/1.32 inference(resolution,[status(thm)],[f447,f116])).
% 6.29/1.32 fof(f560,plain,(
% 6.29/1.32 aElement0(xp)),
% 6.29/1.32 inference(forward_subsumption_resolution,[status(thm)],[f559,f480])).
% 6.29/1.32 fof(f586,plain,(
% 6.29/1.32 ![X0]: (aSubsetOf0(X0,xQ)|~aSet0(X0)|aElementOf0(sK1_skl(X0,xQ),X0))),
% 6.29/1.32 inference(resolution,[status(thm)],[f139,f480])).
% 6.29/1.32 fof(f788,plain,(
% 6.29/1.32 aSubsetOf0(xP,xQ)|aElementOf0(sK1_skl(xP,xQ),xP)),
% 6.29/1.32 inference(resolution,[status(thm)],[f586,f445])).
% 6.29/1.32 fof(f789,plain,(
% 6.29/1.32 aElementOf0(sK1_skl(xP,xQ),xP)),
% 6.29/1.32 inference(forward_subsumption_resolution,[status(thm)],[f788,f449])).
% 6.29/1.32 fof(f857,plain,(
% 6.29/1.32 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtpldt0(X0,X1)|aElementOf0(X3,X2)|~aElementOf0(X3,X0))),
% 6.29/1.32 inference(forward_subsumption_resolution,[status(thm)],[f156,f116])).
% 6.29/1.32 fof(f872,plain,(
% 6.29/1.32 ![X0,X1,X2]: (~aSet0(X0)|~X1=sdtpldt0(X0,xp)|aElementOf0(X2,X1)|~aElementOf0(X2,X0))),
% 6.29/1.32 inference(resolution,[status(thm)],[f857,f560])).
% 6.29/1.32 fof(f1979,plain,(
% 6.29/1.32 ~aSet0(xQ)|sdtpldt0(sdtmndt0(xQ,xp),xp)=xQ),
% 6.29/1.32 inference(resolution,[status(thm)],[f174,f447])).
% 6.29/1.32 fof(f2000,plain,(
% 6.29/1.32 ~aSet0(xQ)|sdtpldt0(xP,xp)=xQ),
% 6.29/1.32 inference(forward_demodulation,[status(thm)],[f555,f1979])).
% 6.29/1.32 fof(f2001,plain,(
% 6.29/1.32 sdtpldt0(xP,xp)=xQ),
% 6.29/1.32 inference(forward_subsumption_resolution,[status(thm)],[f2000,f480])).
% 6.29/1.33 fof(f7364,plain,(
% 6.29/1.33 ![X0]: (~aSet0(xP)|~X0=sdtpldt0(xP,xp)|aElementOf0(sK1_skl(xP,xQ),X0))),
% 6.29/1.33 inference(resolution,[status(thm)],[f872,f789])).
% 6.29/1.33 fof(f7440,plain,(
% 6.29/1.33 ![X0]: (~aSet0(xP)|~X0=xQ|aElementOf0(sK1_skl(xP,xQ),X0))),
% 6.29/1.33 inference(forward_demodulation,[status(thm)],[f2001,f7364])).
% 6.29/1.33 fof(f7441,plain,(
% 6.29/1.33 ![X0]: (~X0=xQ|aElementOf0(sK1_skl(xP,xQ),X0))),
% 6.29/1.33 inference(forward_subsumption_resolution,[status(thm)],[f7440,f445])).
% 6.29/1.33 fof(f8473,plain,(
% 6.29/1.33 aElementOf0(sK1_skl(xP,xQ),sdtpldt0(xP,xp))),
% 6.29/1.33 inference(resolution,[status(thm)],[f7441,f2001])).
% 6.29/1.33 fof(f8475,plain,(
% 6.29/1.33 aElementOf0(sK1_skl(xP,xQ),xQ)),
% 6.29/1.33 inference(forward_demodulation,[status(thm)],[f2001,f8473])).
% 6.29/1.33 fof(f8476,plain,(
% 6.29/1.33 ~aSet0(xQ)|aSubsetOf0(xP,xQ)|~aSet0(xP)),
% 6.29/1.33 inference(resolution,[status(thm)],[f8475,f140])).
% 6.29/1.33 fof(f8500,plain,(
% 6.29/1.33 aSubsetOf0(xP,xQ)|~aSet0(xP)),
% 6.29/1.33 inference(forward_subsumption_resolution,[status(thm)],[f8476,f480])).
% 6.29/1.33 fof(f8508,plain,(
% 6.29/1.33 ~aSet0(xP)),
% 6.29/1.33 inference(forward_subsumption_resolution,[status(thm)],[f8500,f449])).
% 6.29/1.33 fof(f8509,plain,(
% 6.29/1.33 $false),
% 6.29/1.33 inference(backward_subsumption_resolution,[status(thm)],[f445,f8508])).
% 6.29/1.33 % SZS output end CNFRefutation for theBenchmark.p
% 6.29/1.34 % Elapsed time: 0.970623 seconds
% 6.29/1.34 % CPU time: 7.363194 seconds
% 6.29/1.34 % Total memory used: 196.465 MB
% 6.29/1.34 % Net memory used: 189.406 MB
%------------------------------------------------------------------------------