%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM590+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 : n004.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:17 PM UTC 2026
% Result : Theorem 0.02s 15.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM590+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.12/15.40 % Computer : n004.cluster.edu
% 0.12/15.40 % Model : x86_64 x86_64
% 0.12/15.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/15.40 % Memory : 8046.5625MB
% 0.12/15.40 % OS : Linux 6.8.0-71-generic
% 0.02/15.40 % CPULimit : 300
% 0.02/15.40 % WCLimit : 300
% 0.02/15.40 % DateTime : Mon Sep 21 02:42:51 UTC 2026
% 0.02/15.40 % CPUTime :
% 0.02/15.44 % Drodi V4.1.1
% 0.02/15.49 % Refutation found
% 0.02/15.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.02/15.49 % SZS output start CNFRefutation for theBenchmark
% 0.02/15.49 fof(f82,hypothesis,(
% 0.02/15.49 (! [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)) ) ) )),
% 0.02/15.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/15.49 fof(f90,hypothesis,(
% 0.02/15.49 aElementOf0(xi,szNzAzT0) ),
% 0.02/15.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/15.49 fof(f91,hypothesis,(
% 0.02/15.49 ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))& (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) ))& aSet0(xY)& (! [W0] :( aElementOf0(W0,xY)<=> ( aElement0(W0)& aElementOf0(W0,sdtlpdtrp0(xN,xi))& W0 != szmzizndt0(sdtlpdtrp0(xN,xi)) ) ))& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))& xd = sdtlpdtrp0(xC,xi) ) ),
% 0.02/15.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/15.49 fof(f92,conjecture,(
% 0.02/15.49 ( (! [W0] :( aElementOf0(W0,xY)=> aElementOf0(W0,szNzAzT0) ))| aSubsetOf0(xY,szNzAzT0) ) ),
% 0.02/15.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/15.49 fof(f93,negated_conjecture,(
% 0.02/15.49 ~(( (! [W0] :( aElementOf0(W0,xY)=> aElementOf0(W0,szNzAzT0) ))| aSubsetOf0(xY,szNzAzT0) ) )),
% 0.02/15.49 inference(negated_conjecture,[status(cth)],[f92])).
% 0.02/15.49 fof(f409,plain,(
% 0.02/15.49 ![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))))),
% 0.02/15.49 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 0.02/15.49 fof(f411,plain,(
% 0.02/15.49 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,sdtlpdtrp0(xN,X0))|aElementOf0(X1,szNzAzT0))),
% 0.02/15.49 inference(cnf_transformation,[status(thm)],[f409])).
% 0.02/15.49 fof(f499,plain,(
% 0.02/15.49 aElementOf0(xi,szNzAzT0)),
% 0.02/15.49 inference(cnf_transformation,[status(thm)],[f90])).
% 0.02/15.49 fof(f500,plain,(
% 0.02/15.49 ((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(xY))&(![W0]: (aElementOf0(W0,xY)<=>((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))&xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&xd=sdtlpdtrp0(xC,xi)),
% 0.02/15.49 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 0.02/15.49 fof(f501,plain,(
% 0.02/15.49 ((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(xY))&(![W0]: ((~aElementOf0(W0,xY)|((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))&(aElementOf0(W0,xY)|((~aElement0(W0)|~aElementOf0(W0,sdtlpdtrp0(xN,xi)))|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))))&xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&xd=sdtlpdtrp0(xC,xi)),
% 0.02/15.49 inference(NNF_transformation,[status(thm)],[f500])).
% 0.02/15.49 fof(f502,plain,(
% 0.02/15.49 ((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(xY))&((![W0]: (~aElementOf0(W0,xY)|((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))&(![W0]: (aElementOf0(W0,xY)|((~aElement0(W0)|~aElementOf0(W0,sdtlpdtrp0(xN,xi)))|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))))&xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&xd=sdtlpdtrp0(xC,xi)),
% 0.02/15.49 inference(miniscoping,[status(thm)],[f501])).
% 0.02/15.49 fof(f507,plain,(
% 0.02/15.49 ![X0]: (~aElementOf0(X0,xY)|aElementOf0(X0,sdtlpdtrp0(xN,xi)))),
% 0.02/15.49 inference(cnf_transformation,[status(thm)],[f502])).
% 0.02/15.49 fof(f512,plain,(
% 0.02/15.49 ((?[W0]: (aElementOf0(W0,xY)&~aElementOf0(W0,szNzAzT0)))&~aSubsetOf0(xY,szNzAzT0))),
% 0.02/15.49 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 0.02/15.49 fof(f513,plain,(
% 0.02/15.49 (aElementOf0(sK27_skl,xY)&~aElementOf0(sK27_skl,szNzAzT0))&~aSubsetOf0(xY,szNzAzT0)),
% 0.02/15.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(W0,sK27_skl)],[f512])).
% 0.02/15.49 fof(f514,plain,(
% 0.02/15.49 aElementOf0(sK27_skl,xY)),
% 0.02/15.49 inference(cnf_transformation,[status(thm)],[f513])).
% 0.15/15.51 fof(f515,plain,(
% 0.15/15.51 ~aElementOf0(sK27_skl,szNzAzT0)),
% 0.15/15.51 inference(cnf_transformation,[status(thm)],[f513])).
% 0.15/15.51 fof(f760,plain,(
% 0.15/15.51 aElementOf0(sK27_skl,sdtlpdtrp0(xN,xi))),
% 0.15/15.51 inference(resolution,[status(thm)],[f507,f514])).
% 0.15/15.51 fof(f997,plain,(
% 0.15/15.51 ~aElementOf0(xi,szNzAzT0)|aElementOf0(sK27_skl,szNzAzT0)),
% 0.15/15.51 inference(resolution,[status(thm)],[f411,f760])).
% 0.15/15.51 fof(f999,definition,(
% 0.15/15.51 sQ40_spl <=> (aElementOf0(xi,szNzAzT0))),
% 0.15/15.51 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.15/15.51 fof(f1001,plain,(
% 0.15/15.51 ~aElementOf0(xi,szNzAzT0)|sQ40_spl),
% 0.15/15.51 inference(component_clause,[status(thm)],[f999])).
% 0.15/15.51 fof(f1002,definition,(
% 0.15/15.51 sQ41_spl <=> (aElementOf0(sK27_skl,szNzAzT0))),
% 0.15/15.51 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.15/15.51 fof(f1003,plain,(
% 0.15/15.51 aElementOf0(sK27_skl,szNzAzT0)|~sQ41_spl),
% 0.15/15.51 inference(component_clause,[status(thm)],[f1002])).
% 0.15/15.51 fof(f1005,plain,(
% 0.15/15.51 ~sQ40_spl|sQ41_spl),
% 0.15/15.51 inference(split_clause,[status(thm)],[f997,f999,f1002])).
% 0.15/15.51 fof(f1096,plain,(
% 0.15/15.51 $false|~sQ41_spl),
% 0.15/15.51 inference(forward_subsumption_resolution,[status(thm)],[f1003,f515])).
% 0.15/15.51 fof(f1097,plain,(
% 0.15/15.51 ~sQ41_spl),
% 0.15/15.51 inference(contradiction_clause,[status(thm)],[f1096])).
% 0.15/15.51 fof(f1302,plain,(
% 0.15/15.51 $false|sQ40_spl),
% 0.15/15.51 inference(forward_subsumption_resolution,[status(thm)],[f499,f1001])).
% 0.15/15.51 fof(f1303,plain,(
% 0.15/15.51 sQ40_spl),
% 0.15/15.51 inference(contradiction_clause,[status(thm)],[f1302])).
% 0.15/15.51 fof(f1304,plain,(
% 0.15/15.51 $false),
% 0.15/15.51 inference(sat_refutation,[status(thm)],[f1005,f1097,f1303])).
% 0.15/15.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/15.54 % Elapsed time: 0.130172 seconds
% 0.15/15.54 % CPU time: 0.216938 seconds
% 0.15/15.54 % Total memory used: 34.818 MB
% 0.15/15.54 % Net memory used: 34.681 MB
%------------------------------------------------------------------------------