%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM594+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 : n016.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:18 PM UTC 2026
% Result : Theorem 0.14s 5.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM594+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.09/5.37 % Computer : n016.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Mon Sep 21 02:47:43 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.14/5.40 % Drodi V4.1.1
% 0.14/5.44 % Refutation found
% 0.14/5.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/5.44 % SZS output start CNFRefutation for theBenchmark
% 0.14/5.44 fof(f92,hypothesis,(
% 0.14/5.44 ( 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) ) )) )) ),
% 0.14/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.44 fof(f93,hypothesis,(
% 0.14/5.44 ( aSet0(sdtlcdtrc0(xd,szDzozmdt0(xd)))& (! [W0] :( aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd)))<=> (? [W1] :( aElementOf0(W1,szDzozmdt0(xd))& sdtlpdtrp0(xd,W1) = W0 ) )) )) ),
% 0.14/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.44 fof(f94,hypothesis,(
% 0.14/5.44 ( (? [W0] :( aElementOf0(W0,szDzozmdt0(xd))& sdtlpdtrp0(xd,W0) = xx ))& aElementOf0(xx,sdtlcdtrc0(xd,szDzozmdt0(xd))) ) ),
% 0.14/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.44 fof(f95,conjecture,(
% 0.14/5.44 (? [W0] :( aElementOf0(W0,szNzAzT0)& sdtlpdtrp0(xd,W0) = xx ) )),
% 0.14/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/5.44 fof(f96,negated_conjecture,(
% 0.14/5.44 ~((? [W0] :( aElementOf0(W0,szNzAzT0)& sdtlpdtrp0(xd,W0) = xx ) ))),
% 0.14/5.44 inference(negated_conjecture,[status(cth)],[f95])).
% 0.14/5.44 fof(f534,plain,(
% 0.14/5.44 (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)))))),
% 0.14/5.44 inference(pre_NNF_transformation,[status(thm)],[f92])).
% 0.14/5.44 fof(f535,plain,(
% 0.14/5.44 (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)))))),
% 0.14/5.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK32_skl]),skolemize(W2,sK32_skl(W1,W0))],[f534])).
% 0.14/5.44 fof(f537,plain,(
% 0.14/5.44 szDzozmdt0(xd)=szNzAzT0),
% 0.14/5.44 inference(cnf_transformation,[status(thm)],[f535])).
% 0.14/5.44 fof(f542,plain,(
% 0.14/5.44 aSet0(sdtlcdtrc0(xd,szDzozmdt0(xd)))&(![W0]: ((~aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd)))|(?[W1]: (aElementOf0(W1,szDzozmdt0(xd))&sdtlpdtrp0(xd,W1)=W0)))&(aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd)))|(![W1]: (~aElementOf0(W1,szDzozmdt0(xd))|~sdtlpdtrp0(xd,W1)=W0)))))),
% 0.14/5.44 inference(NNF_transformation,[status(thm)],[f93])).
% 0.14/5.44 fof(f543,plain,(
% 0.14/5.44 aSet0(sdtlcdtrc0(xd,szDzozmdt0(xd)))&((![W0]: (~aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd)))|(?[W1]: (aElementOf0(W1,szDzozmdt0(xd))&sdtlpdtrp0(xd,W1)=W0))))&(![W0]: (aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd)))|(![W1]: (~aElementOf0(W1,szDzozmdt0(xd))|~sdtlpdtrp0(xd,W1)=W0)))))),
% 0.14/5.44 inference(miniscoping,[status(thm)],[f542])).
% 0.14/5.44 fof(f544,plain,(
% 0.14/5.44 aSet0(sdtlcdtrc0(xd,szDzozmdt0(xd)))&((![W0]: (~aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd)))|(aElementOf0(sK33_skl(W0),szDzozmdt0(xd))&sdtlpdtrp0(xd,sK33_skl(W0))=W0)))&(![W0]: (aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd)))|(![W1]: (~aElementOf0(W1,szDzozmdt0(xd))|~sdtlpdtrp0(xd,W1)=W0)))))),
% 0.14/5.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK33_skl]),skolemize(W1,sK33_skl(W0))],[f543])).
% 0.14/5.44 fof(f546,plain,(
% 0.14/5.44 ![X0]: (~aElementOf0(X0,sdtlcdtrc0(xd,szDzozmdt0(xd)))|aElementOf0(sK33_skl(X0),szDzozmdt0(xd)))),
% 0.14/5.44 inference(cnf_transformation,[status(thm)],[f544])).
% 0.14/5.44 fof(f547,plain,(
% 0.14/5.44 ![X0]: (~aElementOf0(X0,sdtlcdtrc0(xd,szDzozmdt0(xd)))|sdtlpdtrp0(xd,sK33_skl(X0))=X0)),
% 0.14/5.44 inference(cnf_transformation,[status(thm)],[f544])).
% 0.14/5.44 fof(f549,plain,(
% 0.14/5.44 (aElementOf0(sK34_skl,szDzozmdt0(xd))&sdtlpdtrp0(xd,sK34_skl)=xx)&aElementOf0(xx,sdtlcdtrc0(xd,szDzozmdt0(xd)))),
% 0.14/5.44 inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(W0,sK34_skl)],[f94])).
% 0.14/5.45 fof(f552,plain,(
% 0.14/5.45 aElementOf0(xx,sdtlcdtrc0(xd,szDzozmdt0(xd)))),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f549])).
% 0.14/5.45 fof(f553,plain,(
% 0.14/5.45 (![W0]: (~aElementOf0(W0,szNzAzT0)|~sdtlpdtrp0(xd,W0)=xx))),
% 0.14/5.45 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 0.14/5.45 fof(f554,plain,(
% 0.14/5.45 ![X0]: (~aElementOf0(X0,szNzAzT0)|~sdtlpdtrp0(xd,X0)=xx)),
% 0.14/5.45 inference(cnf_transformation,[status(thm)],[f553])).
% 0.14/5.45 fof(f792,plain,(
% 0.14/5.45 ![X0]: (~aElementOf0(X0,sdtlcdtrc0(xd,szNzAzT0))|aElementOf0(sK33_skl(X0),szDzozmdt0(xd)))),
% 0.14/5.45 inference(forward_demodulation,[status(thm)],[f537,f546])).
% 0.14/5.45 fof(f793,plain,(
% 0.14/5.45 ![X0]: (~aElementOf0(X0,sdtlcdtrc0(xd,szNzAzT0))|aElementOf0(sK33_skl(X0),szNzAzT0))),
% 0.14/5.45 inference(forward_demodulation,[status(thm)],[f537,f792])).
% 0.14/5.45 fof(f794,plain,(
% 0.14/5.45 ![X0]: (~aElementOf0(X0,sdtlcdtrc0(xd,szNzAzT0))|sdtlpdtrp0(xd,sK33_skl(X0))=X0)),
% 0.14/5.45 inference(forward_demodulation,[status(thm)],[f537,f547])).
% 0.14/5.45 fof(f799,plain,(
% 0.14/5.45 aElementOf0(xx,sdtlcdtrc0(xd,szNzAzT0))),
% 0.14/5.45 inference(forward_demodulation,[status(thm)],[f537,f552])).
% 0.14/5.45 fof(f831,plain,(
% 0.14/5.45 aElementOf0(sK33_skl(xx),szNzAzT0)),
% 0.14/5.45 inference(resolution,[status(thm)],[f793,f799])).
% 0.14/5.45 fof(f839,plain,(
% 0.14/5.45 sdtlpdtrp0(xd,sK33_skl(xx))=xx),
% 0.14/5.45 inference(resolution,[status(thm)],[f794,f799])).
% 0.14/5.45 fof(f849,plain,(
% 0.14/5.45 ~aElementOf0(sK33_skl(xx),szNzAzT0)),
% 0.14/5.45 inference(resolution,[status(thm)],[f839,f554])).
% 0.14/5.45 fof(f852,plain,(
% 0.14/5.45 $false),
% 0.14/5.45 inference(forward_subsumption_resolution,[status(thm)],[f849,f831])).
% 0.14/5.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/5.46 % Elapsed time: 0.078997 seconds
% 0.14/5.46 % CPU time: 0.272483 seconds
% 0.14/5.46 % Total memory used: 90.423 MB
% 0.14/5.46 % Net memory used: 90.116 MB
%------------------------------------------------------------------------------