%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM582+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 : n013.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:16 PM UTC 2026
% Result : Theorem 0.22s 10.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM582+3 : 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.18/10.45 % Computer : n013.cluster.edu
% 0.18/10.45 % Model : x86_64 x86_64
% 0.18/10.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/10.45 % Memory : 8046.5625MB
% 0.18/10.45 % OS : Linux 6.8.0-71-generic
% 0.18/10.45 % CPULimit : 300
% 0.18/10.45 % WCLimit : 300
% 0.18/10.45 % DateTime : Mon Sep 21 02:41:46 UTC 2026
% 0.18/10.45 % CPUTime :
% 0.18/10.48 % Drodi V4.1.1
% 0.22/10.97 % Refutation found
% 0.22/10.97 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.22/10.97 % SZS output start CNFRefutation for theBenchmark
% 0.22/10.97 fof(f24,axiom,(
% 0.22/10.97 aElementOf0(sz00,szNzAzT0) ),
% 0.22/10.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/10.97 fof(f30,axiom,(
% 0.22/10.97 (! [W0] :( aElementOf0(W0,szNzAzT0)=> sdtlseqdt0(sz00,W0) ) )),
% 0.22/10.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/10.97 fof(f81,hypothesis,(
% 0.22/10.97 ( aFunction0(xN)& szDzozmdt0(xN) = szNzAzT0& sdtlpdtrp0(xN,sz00) = xS& (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( ( ( ( aSet0(sdtlpdtrp0(xN,W0))& (! [W1] :( aElementOf0(W1,sdtlpdtrp0(xN,W0))=> aElementOf0(W1,szNzAzT0) ) ))| aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0) )& isCountable0(sdtlpdtrp0(xN,W0)) )=> ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))& (! [W1] :( aElementOf0(W1,sdtlpdtrp0(xN,W0))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1) ))& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& (! [W1] :( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=> ( aElement0(W1)& aElementOf0(W1,sdtlpdtrp0(xN,W0))& W1 != szmzizndt0(sdtlpdtrp0(xN,W0)) ) ))& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))& (! [W1] :( aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))=> aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ))& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0))) ) ) ) )) ),
% 0.22/10.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/10.97 fof(f83,hypothesis,(
% 0.22/10.97 (! [W0,W1] :( ( aElementOf0(W0,szNzAzT0)& aElementOf0(W1,szNzAzT0) )=> ( sdtlseqdt0(W1,W0)=> ( (! [W2] :( aElementOf0(W2,sdtlpdtrp0(xN,W0))=> aElementOf0(W2,sdtlpdtrp0(xN,W1)) ))& aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1)) ) ) ) )),
% 0.22/10.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/10.97 fof(f85,hypothesis,(
% 0.22/10.97 aElementOf0(xi,szNzAzT0) ),
% 0.22/10.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/10.97 fof(f88,conjecture,(
% 0.22/10.97 ( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> aElementOf0(W0,xS) ))| aSubsetOf0(sdtlpdtrp0(xN,xi),xS) ) ),
% 0.22/10.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/10.97 fof(f89,negated_conjecture,(
% 0.22/10.97 ~(( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> aElementOf0(W0,xS) ))| aSubsetOf0(sdtlpdtrp0(xN,xi),xS) ) )),
% 0.22/10.97 inference(negated_conjecture,[status(cth)],[f88])).
% 0.22/10.97 fof(f168,plain,(
% 0.22/10.97 aElementOf0(sz00,szNzAzT0)),
% 0.22/10.97 inference(cnf_transformation,[status(thm)],[f24])).
% 0.22/10.97 fof(f182,plain,(
% 0.22/10.97 ![W0]: (~aElementOf0(W0,szNzAzT0)|sdtlseqdt0(sz00,W0))),
% 0.22/10.97 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.22/10.97 fof(f183,plain,(
% 0.22/10.97 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlseqdt0(sz00,X0))),
% 0.22/10.97 inference(cnf_transformation,[status(thm)],[f182])).
% 0.22/10.97 fof(f386,plain,(
% 0.22/10.97 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![W0]: (~aElementOf0(W0,szNzAzT0)|((((~aSet0(sdtlpdtrp0(xN,W0))|(?[W1]: (aElementOf0(W1,sdtlpdtrp0(xN,W0))&~aElementOf0(W1,szNzAzT0))))&~aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0))|~isCountable0(sdtlpdtrp0(xN,W0)))|(((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W1]: (aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=>((aElement0(W1)&aElementOf0(W1,sdtlpdtrp0(xN,W0)))&~W1=szmzizndt0(sdtlpdtrp0(xN,W0))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0))))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))|aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 0.22/10.97 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 0.22/10.97 fof(f387,definition,(
% 0.22/10.97 ![W0]: (sP4_prd(W0)<=>(((~aSet0(sdtlpdtrp0(xN,W0))|(?[W1]: (aElementOf0(W1,sdtlpdtrp0(xN,W0))&~aElementOf0(W1,szNzAzT0))))&~aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0))|~isCountable0(sdtlpdtrp0(xN,W0))))),
% 0.22/10.97 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.22/10.97 fof(f388,plain,(
% 0.22/10.97 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(sP4_prd(W0)|(((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W1]: (aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=>((aElement0(W1)&aElementOf0(W1,sdtlpdtrp0(xN,W0)))&~W1=szmzizndt0(sdtlpdtrp0(xN,W0))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0))))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))|aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 0.22/10.97 inference(formula_renaming,[status(thm)],[f386,f387])).
% 0.22/10.97 fof(f389,plain,(
% 0.22/10.97 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(sP4_prd(W0)|(((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W1]: ((~aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((aElement0(W1)&aElementOf0(W1,sdtlpdtrp0(xN,W0)))&~W1=szmzizndt0(sdtlpdtrp0(xN,W0))))&(aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((~aElement0(W1)|~aElementOf0(W1,sdtlpdtrp0(xN,W0)))|W1=szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0))))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))|aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 0.22/10.97 inference(NNF_transformation,[status(thm)],[f388])).
% 0.22/10.97 fof(f390,plain,(
% 0.22/10.97 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(sP4_prd(W0)|(((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&((![W1]: (~aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((aElement0(W1)&aElementOf0(W1,sdtlpdtrp0(xN,W0)))&~W1=szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W1]: (aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((~aElement0(W1)|~aElementOf0(W1,sdtlpdtrp0(xN,W0)))|W1=szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0))))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))|aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 0.22/10.97 inference(miniscoping,[status(thm)],[f389])).
% 0.22/10.97 fof(f393,plain,(
% 0.22/10.97 sdtlpdtrp0(xN,sz00)=xS),
% 0.22/10.97 inference(cnf_transformation,[status(thm)],[f390])).
% 0.22/10.97 fof(f410,plain,(
% 0.22/10.97 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|(~sdtlseqdt0(W1,W0)|((![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,W0))|aElementOf0(W2,sdtlpdtrp0(xN,W1))))&aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1)))))),
% 0.22/10.97 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 0.22/10.97 fof(f412,plain,(
% 0.22/10.97 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X1,X0)|aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1)))),
% 0.22/10.97 inference(cnf_transformation,[status(thm)],[f410])).
% 0.22/10.97 fof(f420,plain,(
% 0.22/10.97 aElementOf0(xi,szNzAzT0)),
% 0.22/10.97 inference(cnf_transformation,[status(thm)],[f85])).
% 0.22/10.97 fof(f447,plain,(
% 0.22/10.97 ((?[W0]: (aElementOf0(W0,sdtlpdtrp0(xN,xi))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtlpdtrp0(xN,xi),xS))),
% 0.22/10.97 inference(pre_NNF_transformation,[status(thm)],[f89])).
% 0.22/10.97 fof(f448,plain,(
% 0.22/10.97 (aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi))&~aElementOf0(sK24_skl,xS))&~aSubsetOf0(sdtlpdtrp0(xN,xi),xS)),
% 0.22/10.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W0,sK24_skl)],[f447])).
% 0.22/10.98 fof(f451,plain,(
% 0.22/10.98 ~aSubsetOf0(sdtlpdtrp0(xN,xi),xS)),
% 0.22/10.98 inference(cnf_transformation,[status(thm)],[f448])).
% 0.22/10.98 fof(f696,definition,(
% 0.22/10.98 sQ21_spl <=> (aElementOf0(xi,szNzAzT0))),
% 0.22/10.98 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.22/10.98 fof(f698,plain,(
% 0.22/10.98 ~aElementOf0(xi,szNzAzT0)|sQ21_spl),
% 0.22/10.98 inference(component_clause,[status(thm)],[f696])).
% 0.22/10.98 fof(f703,definition,(
% 0.22/10.98 sQ23_spl <=> (aElementOf0(sz00,szNzAzT0))),
% 0.22/10.98 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.22/10.98 fof(f705,plain,(
% 0.22/10.98 ~aElementOf0(sz00,szNzAzT0)|sQ23_spl),
% 0.22/10.98 inference(component_clause,[status(thm)],[f703])).
% 0.22/10.98 fof(f707,plain,(
% 0.22/10.98 $false|sQ21_spl),
% 0.22/10.98 inference(forward_subsumption_resolution,[status(thm)],[f698,f420])).
% 0.22/10.98 fof(f708,plain,(
% 0.22/10.98 sQ21_spl),
% 0.22/10.98 inference(contradiction_clause,[status(thm)],[f707])).
% 0.22/10.98 fof(f1373,plain,(
% 0.22/10.98 sdtlseqdt0(sz00,xi)),
% 0.22/10.98 inference(resolution,[status(thm)],[f420,f183])).
% 0.22/10.98 fof(f3189,plain,(
% 0.22/10.98 $false|sQ23_spl),
% 0.22/10.98 inference(forward_subsumption_resolution,[status(thm)],[f705,f168])).
% 0.22/10.98 fof(f3190,plain,(
% 0.22/10.98 sQ23_spl),
% 0.22/10.98 inference(contradiction_clause,[status(thm)],[f3189])).
% 0.22/10.98 fof(f5498,plain,(
% 0.22/10.98 ~aElementOf0(xi,szNzAzT0)|~aElementOf0(sz00,szNzAzT0)|aSubsetOf0(sdtlpdtrp0(xN,xi),sdtlpdtrp0(xN,sz00))),
% 0.22/10.98 inference(resolution,[status(thm)],[f412,f1373])).
% 0.22/10.98 fof(f5530,definition,(
% 0.22/10.98 sQ636_spl <=> (aSubsetOf0(sdtlpdtrp0(xN,xi),sdtlpdtrp0(xN,sz00)))),
% 0.22/10.98 introduced(definition,[new_symbols(definition,[sQ636_spl])],[split_symbol_definition])).
% 0.22/10.98 fof(f5531,plain,(
% 0.22/10.98 aSubsetOf0(sdtlpdtrp0(xN,xi),sdtlpdtrp0(xN,sz00))|~sQ636_spl),
% 0.22/10.98 inference(component_clause,[status(thm)],[f5530])).
% 0.22/10.98 fof(f5533,plain,(
% 0.22/10.98 ~sQ21_spl|~sQ23_spl|sQ636_spl),
% 0.22/10.98 inference(split_clause,[status(thm)],[f5498,f696,f703,f5530])).
% 0.22/10.98 fof(f5543,plain,(
% 0.22/10.98 aSubsetOf0(sdtlpdtrp0(xN,xi),xS)|~sQ636_spl),
% 0.22/10.98 inference(forward_demodulation,[status(thm)],[f393,f5531])).
% 0.22/10.98 fof(f5544,plain,(
% 0.22/10.98 $false|~sQ636_spl),
% 0.22/10.98 inference(forward_subsumption_resolution,[status(thm)],[f5543,f451])).
% 0.22/10.98 fof(f5545,plain,(
% 0.22/10.98 ~sQ636_spl),
% 0.22/10.98 inference(contradiction_clause,[status(thm)],[f5544])).
% 0.22/10.98 fof(f5546,plain,(
% 0.22/10.98 $false),
% 0.22/10.98 inference(sat_refutation,[status(thm)],[f708,f3190,f5533,f5545])).
% 0.22/10.98 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/11.00 % Elapsed time: 0.533246 seconds
% 0.22/11.00 % CPU time: 3.880790 seconds
% 0.22/11.00 % Total memory used: 153.295 MB
% 0.22/11.00 % Net memory used: 150.345 MB
%------------------------------------------------------------------------------