%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM584+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 : n003.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 22.98s 3.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM584+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.09/0.35 % Computer : n003.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 02:43:31 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 22.98/3.39 % Refutation found
% 22.98/3.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 22.98/3.39 % SZS output start CNFRefutation for theBenchmark
% 22.98/3.39 fof(f10,definition,(
% 22.98/3.39 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 22.98/3.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.39 fof(f23,axiom,(
% 22.98/3.39 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 22.98/3.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.39 fof(f57,definition,(
% 22.98/3.39 (! [W0,W1] :( ( aSet0(W0)& aElementOf0(W1,szNzAzT0) )=> (! [W2] :( W2 = slbdtsldtrb0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aSubsetOf0(W3,W0)& sbrdtbr0(W3) = W1 ) ) )) ) )) )),
% 22.98/3.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.39 fof(f74,hypothesis,(
% 22.98/3.39 aElementOf0(xK,szNzAzT0) ),
% 22.98/3.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.39 fof(f75,hypothesis,(
% 22.98/3.39 ( aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 22.98/3.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.39 fof(f76,hypothesis,(
% 22.98/3.39 ( aFunction0(xc)& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ),
% 22.98/3.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.39 fof(f87,hypothesis,(
% 22.98/3.39 sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = xK ),
% 22.98/3.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.39 fof(f88,hypothesis,(
% 22.98/3.39 aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS) ),
% 22.98/3.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.39 fof(f89,conjecture,(
% 22.98/3.39 aElementOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),slbdtsldtrb0(xS,xK)) ),
% 22.98/3.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.98/3.39 fof(f90,negated_conjecture,(
% 22.98/3.39 ~(aElementOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),slbdtsldtrb0(xS,xK)) )),
% 22.98/3.39 inference(negated_conjecture,[status(cth)],[f89])).
% 22.98/3.39 fof(f115,plain,(
% 22.98/3.39 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 22.98/3.39 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 22.98/3.39 fof(f116,plain,(
% 22.98/3.39 ![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))))))))),
% 22.98/3.39 inference(NNF_transformation,[status(thm)],[f115])).
% 22.98/3.39 fof(f117,plain,(
% 22.98/3.39 ![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))))))))),
% 22.98/3.39 inference(miniscoping,[status(thm)],[f116])).
% 22.98/3.39 fof(f118,plain,(
% 22.98/3.39 ![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)))))))),
% 22.98/3.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f117])).
% 22.98/3.39 fof(f119,plain,(
% 22.98/3.39 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 22.98/3.39 inference(cnf_transformation,[status(thm)],[f118])).
% 22.98/3.39 fof(f167,plain,(
% 22.98/3.39 aSet0(szNzAzT0)),
% 22.98/3.39 inference(cnf_transformation,[status(thm)],[f23])).
% 22.98/3.39 fof(f272,plain,(
% 22.98/3.39 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|(![W2]: (W2=slbdtsldtrb0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))))))),
% 22.98/3.39 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 22.98/3.39 fof(f273,plain,(
% 22.98/3.39 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|(![W2]: ((~W2=slbdtsldtrb0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1))&(aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1))))))&(W2=slbdtsldtrb0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1))&(aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))))))))),
% 22.98/3.39 inference(NNF_transformation,[status(thm)],[f272])).
% 22.98/3.39 fof(f274,plain,(
% 22.98/3.39 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|((![W2]: (~W2=slbdtsldtrb0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))&(![W3]: (aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1)))))))&(![W2]: (W2=slbdtsldtrb0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1))&(aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))))))))),
% 22.98/3.39 inference(miniscoping,[status(thm)],[f273])).
% 22.98/3.39 fof(f275,plain,(
% 22.98/3.39 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|((![W2]: (~W2=slbdtsldtrb0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))&(![W3]: (aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1)))))))&(![W2]: (W2=slbdtsldtrb0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK10_skl(W2,W1,W0),W2)|(~aSubsetOf0(sK10_skl(W2,W1,W0),W0)|~sbrdtbr0(sK10_skl(W2,W1,W0))=W1))&(aElementOf0(sK10_skl(W2,W1,W0),W2)|(aSubsetOf0(sK10_skl(W2,W1,W0),W0)&sbrdtbr0(sK10_skl(W2,W1,W0))=W1))))))))),
% 22.98/3.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W3,sK10_skl(W2,W1,W0))],[f274])).
% 22.98/3.39 fof(f279,plain,(
% 22.98/3.39 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~X2=slbdtsldtrb0(X0,X1)|aElementOf0(X3,X2)|~aSubsetOf0(X3,X0)|~sbrdtbr0(X3)=X1)),
% 22.98/3.39 inference(cnf_transformation,[status(thm)],[f275])).
% 22.98/3.39 fof(f349,plain,(
% 22.98/3.39 aElementOf0(xK,szNzAzT0)),
% 22.98/3.39 inference(cnf_transformation,[status(thm)],[f74])).
% 22.98/3.39 fof(f350,plain,(
% 22.98/3.39 aSubsetOf0(xS,szNzAzT0)),
% 22.98/3.39 inference(cnf_transformation,[status(thm)],[f75])).
% 22.98/3.39 fof(f353,plain,(
% 22.98/3.39 szDzozmdt0(xc)=slbdtsldtrb0(xS,xK)),
% 22.98/3.39 inference(cnf_transformation,[status(thm)],[f76])).
% 22.98/3.39 fof(f380,plain,(
% 22.98/3.39 sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))=xK),
% 22.98/3.39 inference(cnf_transformation,[status(thm)],[f87])).
% 22.98/3.39 fof(f381,plain,(
% 22.98/3.39 aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS)),
% 22.98/3.39 inference(cnf_transformation,[status(thm)],[f88])).
% 22.98/3.39 fof(f382,plain,(
% 22.98/3.39 ~aElementOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),slbdtsldtrb0(xS,xK))),
% 22.98/3.39 inference(cnf_transformation,[status(thm)],[f90])).
% 22.98/3.39 fof(f424,plain,(
% 22.98/3.39 ![X0,X1]: (~aSet0(X0)|~aElementOf0(sbrdtbr0(X1),szNzAzT0)|aElementOf0(X1,slbdtsldtrb0(X0,sbrdtbr0(X1)))|~aSubsetOf0(X1,X0))),
% 22.98/3.39 inference(destructive_equality_resolution,[status(thm)],[f279])).
% 22.98/3.39 fof(f441,plain,(
% 22.98/3.39 ~aElementOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),szDzozmdt0(xc))),
% 22.98/3.39 inference(forward_demodulation,[status(thm)],[f353,f382])).
% 22.98/3.39 fof(f456,definition,(
% 22.98/3.39 sQ2_spl <=> (aSet0(szNzAzT0))),
% 22.98/3.39 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 22.98/3.39 fof(f458,plain,(
% 22.98/3.39 ~aSet0(szNzAzT0)|sQ2_spl),
% 22.98/3.39 inference(component_clause,[status(thm)],[f456])).
% 22.98/3.39 fof(f467,plain,(
% 22.98/3.39 $false|sQ2_spl),
% 22.98/3.39 inference(forward_subsumption_resolution,[status(thm)],[f458,f167])).
% 22.98/3.39 fof(f468,plain,(
% 22.98/3.39 sQ2_spl),
% 22.98/3.39 inference(contradiction_clause,[status(thm)],[f467])).
% 22.98/3.39 fof(f478,definition,(
% 22.98/3.39 sQ6_spl <=> (aSet0(xS))),
% 22.98/3.39 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 22.98/3.39 fof(f693,plain,(
% 22.98/3.39 ~aSet0(szNzAzT0)|aSet0(xS)),
% 22.98/3.39 inference(resolution,[status(thm)],[f350,f119])).
% 22.98/3.39 fof(f699,plain,(
% 22.98/3.39 ~sQ2_spl|sQ6_spl),
% 22.98/3.39 inference(split_clause,[status(thm)],[f693,f456,f478])).
% 22.98/3.39 fof(f6564,plain,(
% 22.98/3.39 ~aSet0(xS)|~aElementOf0(sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),szNzAzT0)|aElementOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),slbdtsldtrb0(xS,sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))))),
% 22.98/3.39 inference(resolution,[status(thm)],[f424,f381])).
% 22.98/3.39 fof(f6571,definition,(
% 22.98/3.39 sQ315_spl <=> (aElementOf0(sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),szNzAzT0))),
% 22.98/3.39 introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition])).
% 22.98/3.39 fof(f6573,plain,(
% 22.98/3.39 ~aElementOf0(sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))),szNzAzT0)|sQ315_spl),
% 22.98/3.39 inference(component_clause,[status(thm)],[f6571])).
% 22.98/3.39 fof(f6574,definition,(
% 22.98/3.39 sQ316_spl <=> (aElementOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),slbdtsldtrb0(xS,sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))))),
% 22.98/3.39 introduced(definition,[new_symbols(definition,[sQ316_spl])],[split_symbol_definition])).
% 22.98/3.39 fof(f6575,plain,(
% 22.98/3.39 aElementOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),slbdtsldtrb0(xS,sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))))|~sQ316_spl),
% 22.98/3.39 inference(component_clause,[status(thm)],[f6574])).
% 22.98/3.39 fof(f6577,plain,(
% 22.98/3.39 ~sQ6_spl|~sQ315_spl|sQ316_spl),
% 14.86/3.41 inference(split_clause,[status(thm)],[f6564,f478,f6571,f6574])).
% 14.86/3.41 fof(f6614,plain,(
% 14.86/3.41 ~aElementOf0(xK,szNzAzT0)|sQ315_spl),
% 14.86/3.41 inference(forward_demodulation,[status(thm)],[f380,f6573])).
% 14.86/3.41 fof(f6615,plain,(
% 14.86/3.41 $false|sQ315_spl),
% 14.86/3.41 inference(forward_subsumption_resolution,[status(thm)],[f6614,f349])).
% 14.86/3.41 fof(f6616,plain,(
% 14.86/3.41 sQ315_spl),
% 14.86/3.41 inference(contradiction_clause,[status(thm)],[f6615])).
% 14.86/3.41 fof(f6621,plain,(
% 14.86/3.41 aElementOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),slbdtsldtrb0(xS,xK))|~sQ316_spl),
% 14.86/3.41 inference(forward_demodulation,[status(thm)],[f380,f6575])).
% 14.86/3.41 fof(f6622,plain,(
% 14.86/3.41 aElementOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),szDzozmdt0(xc))|~sQ316_spl),
% 14.86/3.41 inference(forward_demodulation,[status(thm)],[f353,f6621])).
% 14.86/3.41 fof(f6623,plain,(
% 14.86/3.41 $false|~sQ316_spl),
% 14.86/3.41 inference(forward_subsumption_resolution,[status(thm)],[f6622,f441])).
% 14.86/3.41 fof(f6624,plain,(
% 14.86/3.41 ~sQ316_spl),
% 14.86/3.41 inference(contradiction_clause,[status(thm)],[f6623])).
% 14.86/3.41 fof(f6625,plain,(
% 14.86/3.41 $false),
% 14.86/3.41 inference(sat_refutation,[status(thm)],[f468,f699,f6577,f6616,f6624])).
% 14.86/3.41 % SZS output end CNFRefutation for theBenchmark.p
% 14.86/3.43 % Elapsed time: 3.058223 seconds
% 14.86/3.43 % CPU time: 23.908617 seconds
% 14.86/3.43 % Total memory used: 292.312 MB
% 14.86/3.43 % Net memory used: 275.937 MB
%------------------------------------------------------------------------------