%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM597+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 : 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 01:43:18 PM UTC 2026
% Result : Theorem 0.14s 10.74s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM597+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/10.55 % Computer : n008.cluster.edu
% 0.08/10.55 % Model : x86_64 x86_64
% 0.08/10.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/10.55 % Memory : 8046.5625MB
% 0.08/10.55 % OS : Linux 6.8.0-71-generic
% 0.08/10.55 % CPULimit : 300
% 0.08/10.55 % WCLimit : 300
% 0.08/10.55 % DateTime : Mon Sep 21 02:44:35 UTC 2026
% 0.08/10.55 % CPUTime :
% 0.08/10.58 % Drodi V4.1.1
% 0.14/10.74 % Refutation found
% 0.14/10.74 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/10.74 % SZS output start CNFRefutation for theBenchmark
% 0.14/10.74 fof(f92,hypothesis,(
% 0.14/10.74 ( 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/10.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.74 fof(f93,hypothesis,(
% 0.14/10.74 ( 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)))=> aElementOf0(W0,xT) ))& aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT) ) ),
% 0.14/10.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.74 fof(f94,hypothesis,(
% 0.14/10.74 ~ ( ( aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))& (! [W0] :( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))<=> ( aElementOf0(W0,szDzozmdt0(xd))& sdtlpdtrp0(xd,W0) = szDzizrdt0(xd) ) ) ))=> ~ (? [W0] : aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))) )) ),
% 0.14/10.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.74 fof(f95,conjecture,(
% 0.14/10.74 aElementOf0(szDzizrdt0(xd),xT) ),
% 0.14/10.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/10.74 fof(f96,negated_conjecture,(
% 0.14/10.74 ~(aElementOf0(szDzizrdt0(xd),xT) )),
% 0.14/10.74 inference(negated_conjecture,[status(cth)],[f95])).
% 0.14/10.74 fof(f534,plain,(
% 0.14/10.74 (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/10.74 inference(pre_NNF_transformation,[status(thm)],[f92])).
% 0.14/10.74 fof(f535,plain,(
% 0.14/10.74 (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/10.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK32_skl]),skolemize(W2,sK32_skl(W1,W0))],[f534])).
% 0.14/10.74 fof(f537,plain,(
% 0.14/10.74 szDzozmdt0(xd)=szNzAzT0),
% 0.14/10.74 inference(cnf_transformation,[status(thm)],[f535])).
% 0.14/10.74 fof(f542,plain,(
% 0.14/10.74 ((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)))|aElementOf0(W0,xT))))&aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)),
% 0.14/10.74 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 0.14/10.74 fof(f543,plain,(
% 0.14/10.74 ((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))))))&(![W0]: (~aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd)))|aElementOf0(W0,xT))))&aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)),
% 0.14/10.74 inference(NNF_transformation,[status(thm)],[f542])).
% 0.14/10.74 fof(f544,plain,(
% 0.14/10.74 ((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))))))&(![W0]: (~aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd)))|aElementOf0(W0,xT))))&aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)),
% 0.14/10.74 inference(miniscoping,[status(thm)],[f543])).
% 0.14/10.74 fof(f545,plain,(
% 0.14/10.74 ((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))))))&(![W0]: (~aElementOf0(W0,sdtlcdtrc0(xd,szDzozmdt0(xd)))|aElementOf0(W0,xT))))&aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)),
% 0.14/10.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK33_skl]),skolemize(W1,sK33_skl(W0))],[f544])).
% 0.14/10.74 fof(f549,plain,(
% 0.14/10.74 ![X0,X1]: (aElementOf0(X0,sdtlcdtrc0(xd,szDzozmdt0(xd)))|~aElementOf0(X1,szDzozmdt0(xd))|~sdtlpdtrp0(xd,X1)=X0)),
% 0.14/10.74 inference(cnf_transformation,[status(thm)],[f545])).
% 0.14/10.74 fof(f550,plain,(
% 0.14/10.74 ![X0]: (~aElementOf0(X0,sdtlcdtrc0(xd,szDzozmdt0(xd)))|aElementOf0(X0,xT))),
% 0.14/10.74 inference(cnf_transformation,[status(thm)],[f545])).
% 0.14/10.74 fof(f552,plain,(
% 0.14/10.74 ((aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))&(![W0]: (aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))<=>(aElementOf0(W0,szDzozmdt0(xd))&sdtlpdtrp0(xd,W0)=szDzizrdt0(xd)))))&(?[W0]: aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))))),
% 0.14/10.74 inference(pre_NNF_transformation,[status(thm)],[f94])).
% 0.14/10.74 fof(f553,plain,(
% 0.14/10.74 (aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))&(![W0]: ((~aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(aElementOf0(W0,szDzozmdt0(xd))&sdtlpdtrp0(xd,W0)=szDzizrdt0(xd)))&(aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(~aElementOf0(W0,szDzozmdt0(xd))|~sdtlpdtrp0(xd,W0)=szDzizrdt0(xd))))))&(?[W0]: aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))))),
% 0.14/10.74 inference(NNF_transformation,[status(thm)],[f552])).
% 0.14/10.74 fof(f554,plain,(
% 0.14/10.74 (aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))&((![W0]: (~aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(aElementOf0(W0,szDzozmdt0(xd))&sdtlpdtrp0(xd,W0)=szDzizrdt0(xd))))&(![W0]: (aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(~aElementOf0(W0,szDzozmdt0(xd))|~sdtlpdtrp0(xd,W0)=szDzizrdt0(xd))))))&(?[W0]: aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd))))),
% 0.14/10.74 inference(miniscoping,[status(thm)],[f553])).
% 0.14/10.74 fof(f555,plain,(
% 0.14/10.74 (aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))&((![W0]: (~aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(aElementOf0(W0,szDzozmdt0(xd))&sdtlpdtrp0(xd,W0)=szDzizrdt0(xd))))&(![W0]: (aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(~aElementOf0(W0,szDzozmdt0(xd))|~sdtlpdtrp0(xd,W0)=szDzizrdt0(xd))))))&aElementOf0(sK34_skl,sdtlbdtrb0(xd,szDzizrdt0(xd)))),
% 0.14/10.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(W0,sK34_skl)],[f554])).
% 0.14/10.74 fof(f557,plain,(
% 0.14/10.74 ![X0]: (~aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|aElementOf0(X0,szDzozmdt0(xd)))),
% 0.14/10.74 inference(cnf_transformation,[status(thm)],[f555])).
% 0.14/10.74 fof(f558,plain,(
% 0.14/10.74 ![X0]: (~aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|sdtlpdtrp0(xd,X0)=szDzizrdt0(xd))),
% 0.14/10.74 inference(cnf_transformation,[status(thm)],[f555])).
% 0.14/10.74 fof(f560,plain,(
% 0.14/10.74 aElementOf0(sK34_skl,sdtlbdtrb0(xd,szDzizrdt0(xd)))),
% 0.14/10.74 inference(cnf_transformation,[status(thm)],[f555])).
% 0.14/10.74 fof(f561,plain,(
% 0.14/10.74 ~aElementOf0(szDzizrdt0(xd),xT)),
% 0.14/10.74 inference(cnf_transformation,[status(thm)],[f96])).
% 0.14/10.74 fof(f785,plain,(
% 0.14/10.74 ![X0]: (aElementOf0(sdtlpdtrp0(xd,X0),sdtlcdtrc0(xd,szDzozmdt0(xd)))|~aElementOf0(X0,szDzozmdt0(xd)))),
% 0.14/10.74 inference(destructive_equality_resolution,[status(thm)],[f549])).
% 0.14/10.74 fof(f815,plain,(
% 0.14/10.74 ![X0]: (~aElementOf0(X0,sdtlcdtrc0(xd,szNzAzT0))|aElementOf0(X0,xT))),
% 0.14/10.74 inference(forward_demodulation,[status(thm)],[f537,f550])).
% 0.14/10.74 fof(f816,plain,(
% 0.14/10.74 ![X0]: (~aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|aElementOf0(X0,szNzAzT0))),
% 0.14/10.74 inference(forward_demodulation,[status(thm)],[f537,f557])).
% 0.14/10.74 fof(f817,plain,(
% 0.14/10.74 ![X0]: (aElementOf0(sdtlpdtrp0(xd,X0),sdtlcdtrc0(xd,szNzAzT0))|~aElementOf0(X0,szDzozmdt0(xd)))),
% 0.14/10.74 inference(forward_demodulation,[status(thm)],[f537,f785])).
% 0.14/10.74 fof(f818,plain,(
% 0.14/10.74 ![X0]: (aElementOf0(sdtlpdtrp0(xd,X0),sdtlcdtrc0(xd,szNzAzT0))|~aElementOf0(X0,szNzAzT0))),
% 0.14/10.74 inference(forward_demodulation,[status(thm)],[f537,f817])).
% 0.14/10.74 fof(f819,plain,(
% 0.14/10.74 sdtlpdtrp0(xd,sK34_skl)=szDzizrdt0(xd)),
% 0.14/10.74 inference(resolution,[status(thm)],[f560,f558])).
% 0.14/10.74 fof(f820,plain,(
% 0.14/10.74 aElementOf0(sK34_skl,szNzAzT0)),
% 0.14/10.74 inference(resolution,[status(thm)],[f560,f816])).
% 0.14/10.74 fof(f916,plain,(
% 0.14/10.74 aElementOf0(sdtlpdtrp0(xd,sK34_skl),sdtlcdtrc0(xd,szNzAzT0))),
% 0.14/10.74 inference(resolution,[status(thm)],[f820,f818])).
% 0.14/10.75 fof(f926,plain,(
% 0.14/10.75 aElementOf0(szDzizrdt0(xd),sdtlcdtrc0(xd,szNzAzT0))),
% 0.14/10.75 inference(forward_demodulation,[status(thm)],[f819,f916])).
% 0.14/10.75 fof(f1087,plain,(
% 0.14/10.75 aElementOf0(szDzizrdt0(xd),xT)),
% 0.14/10.75 inference(resolution,[status(thm)],[f926,f815])).
% 0.14/10.75 fof(f1090,plain,(
% 0.14/10.75 $false),
% 0.14/10.75 inference(forward_subsumption_resolution,[status(thm)],[f1087,f561])).
% 0.14/10.75 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/10.77 % Elapsed time: 0.204790 seconds
% 0.14/10.77 % CPU time: 1.244462 seconds
% 0.14/10.77 % Total memory used: 142.412 MB
% 0.14/10.77 % Net memory used: 140.727 MB
%------------------------------------------------------------------------------