%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM610+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 : n020.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:20 PM UTC 2026
% Result : Theorem 0.13s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM610+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.07/0.35 % Computer : n020.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 02:45:17 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.38 % Drodi V4.1.1
% 0.13/0.40 % Refutation found
% 0.13/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.40 fof(f5,definition,(
% 0.13/0.40 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f10,definition,(
% 0.13/0.40 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f95,hypothesis,(
% 0.13/0.40 ( aSet0(xO)& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))& (! [W0] :( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))<=> ( aElementOf0(W0,szDzozmdt0(xd))& sdtlpdtrp0(xd,W0) = szDzizrdt0(xd) ) ))& (! [W0] :( aElementOf0(W0,xO)<=> (? [W1] :( aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))& sdtlpdtrp0(xe,W1) = W0 ) )))& xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f99,hypothesis,(
% 0.13/0.40 ( aSet0(xQ)& (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,xO) ))& aSubsetOf0(xQ,xO)& sbrdtbr0(xQ) = xK& aElementOf0(xQ,slbdtsldtrb0(xO,xK)) ) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f107,hypothesis,(
% 0.13/0.40 ( (! [W0] :( aElementOf0(W0,xP)=> aElementOf0(W0,xQ) ))& aSubsetOf0(xP,xQ) ) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f108,conjecture,(
% 0.13/0.40 ( (! [W0] :( aElementOf0(W0,xP)=> aElementOf0(W0,xO) ))| aSubsetOf0(xP,xO) ) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f109,negated_conjecture,(
% 0.13/0.40 ~(( (! [W0] :( aElementOf0(W0,xP)=> aElementOf0(W0,xO) ))| aSubsetOf0(xP,xO) ) )),
% 0.13/0.40 inference(negated_conjecture,[status(cth)],[f108])).
% 0.13/0.40 fof(f120,plain,(
% 0.13/0.40 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.13/0.40 fof(f121,plain,(
% 0.13/0.40 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f120])).
% 0.13/0.40 fof(f122,plain,(
% 0.13/0.40 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f121])).
% 0.13/0.40 fof(f123,plain,(
% 0.13/0.40 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f122])).
% 0.13/0.40 fof(f124,plain,(
% 0.13/0.40 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f123])).
% 0.13/0.40 fof(f134,plain,(
% 0.13/0.40 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.13/0.40 fof(f135,plain,(
% 0.13/0.40 ![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))))))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f134])).
% 0.13/0.40 fof(f136,plain,(
% 0.13/0.40 ![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))))))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f135])).
% 0.13/0.40 fof(f137,plain,(
% 0.13/0.40 ![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)))))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f136])).
% 0.13/0.40 fof(f138,plain,(
% 0.13/0.40 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f137])).
% 0.13/0.40 fof(f139,plain,(
% 0.13/0.40 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f137])).
% 0.13/0.40 fof(f572,plain,(
% 0.13/0.40 (((aSet0(xO)&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,xO)|(?[W1]: (aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))&sdtlpdtrp0(xe,W1)=W0)))&(aElementOf0(W0,xO)|(![W1]: (~aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))|~sdtlpdtrp0(xe,W1)=W0))))))&xO=sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f95])).
% 0.13/0.40 fof(f573,plain,(
% 0.13/0.40 (((aSet0(xO)&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,xO)|(?[W1]: (aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))&sdtlpdtrp0(xe,W1)=W0))))&(![W0]: (aElementOf0(W0,xO)|(![W1]: (~aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))|~sdtlpdtrp0(xe,W1)=W0))))))&xO=sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f572])).
% 0.13/0.40 fof(f574,plain,(
% 0.13/0.40 (((aSet0(xO)&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,xO)|(aElementOf0(sK34_skl(W0),sdtlbdtrb0(xd,szDzizrdt0(xd)))&sdtlpdtrp0(xe,sK34_skl(W0))=W0)))&(![W0]: (aElementOf0(W0,xO)|(![W1]: (~aElementOf0(W1,sdtlbdtrb0(xd,szDzizrdt0(xd)))|~sdtlpdtrp0(xe,W1)=W0))))))&xO=sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(W1,sK34_skl(W0))],[f573])).
% 0.13/0.40 fof(f575,plain,(
% 0.13/0.40 aSet0(xO)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f574])).
% 0.13/0.40 fof(f597,plain,(
% 0.13/0.40 (((aSet0(xQ)&(![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,xO))))&aSubsetOf0(xQ,xO))&sbrdtbr0(xQ)=xK)&aElementOf0(xQ,slbdtsldtrb0(xO,xK))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f99])).
% 0.13/0.40 fof(f600,plain,(
% 0.13/0.40 aSubsetOf0(xQ,xO)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f597])).
% 0.13/0.40 fof(f635,plain,(
% 0.13/0.40 (![W0]: (~aElementOf0(W0,xP)|aElementOf0(W0,xQ)))&aSubsetOf0(xP,xQ)),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f107])).
% 0.13/0.40 fof(f637,plain,(
% 0.13/0.40 aSubsetOf0(xP,xQ)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f635])).
% 0.13/0.40 fof(f638,plain,(
% 0.13/0.40 ((?[W0]: (aElementOf0(W0,xP)&~aElementOf0(W0,xO)))&~aSubsetOf0(xP,xO))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f109])).
% 0.13/0.40 fof(f639,plain,(
% 0.13/0.40 (aElementOf0(sK38_skl,xP)&~aElementOf0(sK38_skl,xO))&~aSubsetOf0(xP,xO)),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl]),skolemize(W0,sK38_skl)],[f638])).
% 0.13/0.40 fof(f640,plain,(
% 0.13/0.40 aElementOf0(sK38_skl,xP)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f639])).
% 0.13/0.40 fof(f641,plain,(
% 0.13/0.40 ~aElementOf0(sK38_skl,xO)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f639])).
% 0.13/0.40 fof(f825,plain,(
% 0.13/0.40 aSet0(slcrc0)),
% 0.13/0.40 inference(destructive_equality_resolution,[status(thm)],[f124])).
% 0.13/0.40 fof(f894,definition,(
% 0.13/0.40 sQ1_spl <=> (aSet0(xO))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f896,plain,(
% 0.13/0.40 ~aSet0(xO)|sQ1_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f894])).
% 0.13/0.40 fof(f898,plain,(
% 0.13/0.40 ~aSet0(xO)|aSet0(xQ)),
% 0.13/0.40 inference(resolution,[status(thm)],[f600,f138])).
% 0.13/0.40 fof(f899,definition,(
% 0.13/0.40 sQ2_spl <=> (aSet0(xQ))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f902,plain,(
% 0.13/0.40 ~sQ1_spl|sQ2_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f898,f894,f899])).
% 0.13/0.40 fof(f908,plain,(
% 0.13/0.40 $false|sQ1_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f896,f575])).
% 0.13/0.40 fof(f909,plain,(
% 0.13/0.40 sQ1_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f908])).
% 0.13/0.40 fof(f915,plain,(
% 0.13/0.40 ![X0]: (~aSet0(X0)|~aSubsetOf0(xP,X0)|aElementOf0(sK38_skl,X0))),
% 0.13/0.40 inference(resolution,[status(thm)],[f139,f640])).
% 0.13/0.40 fof(f917,plain,(
% 0.13/0.40 ![X0]: (~aSet0(xO)|~aSubsetOf0(X0,xO)|~aElementOf0(sK38_skl,X0))),
% 0.13/0.40 inference(resolution,[status(thm)],[f139,f641])).
% 0.13/0.41 fof(f920,definition,(
% 0.13/0.41 ![X0]: (sQ4_spl <=> (~aSubsetOf0(X0,xO)|~aElementOf0(sK38_skl,X0)))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f921,plain,(
% 0.13/0.41 ![X0]: (~aSubsetOf0(X0,xO)|~aElementOf0(sK38_skl,X0)|~sQ4_spl)),
% 0.13/0.41 inference(component_clause,[status(thm)],[f920])).
% 0.13/0.41 fof(f923,plain,(
% 0.13/0.41 ~sQ1_spl|sQ4_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f917,f894,f920])).
% 0.13/0.41 fof(f972,definition,(
% 0.13/0.41 sQ14_spl <=> (aSet0(slcrc0))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f974,plain,(
% 0.13/0.41 ~aSet0(slcrc0)|sQ14_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f972])).
% 0.13/0.41 fof(f979,plain,(
% 0.13/0.41 $false|sQ14_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f974,f825])).
% 0.13/0.41 fof(f980,plain,(
% 0.13/0.41 sQ14_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f979])).
% 0.13/0.41 fof(f1039,plain,(
% 0.13/0.41 ~aSet0(xQ)|aElementOf0(sK38_skl,xQ)),
% 0.13/0.41 inference(resolution,[status(thm)],[f915,f637])).
% 0.13/0.41 fof(f1040,definition,(
% 0.13/0.41 sQ30_spl <=> (aElementOf0(sK38_skl,xQ))),
% 0.13/0.41 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.13/0.41 fof(f1041,plain,(
% 0.13/0.41 aElementOf0(sK38_skl,xQ)|~sQ30_spl),
% 0.13/0.41 inference(component_clause,[status(thm)],[f1040])).
% 0.13/0.41 fof(f1043,plain,(
% 0.13/0.41 ~sQ2_spl|sQ30_spl),
% 0.13/0.41 inference(split_clause,[status(thm)],[f1039,f899,f1040])).
% 0.13/0.41 fof(f1044,plain,(
% 0.13/0.41 ~aSubsetOf0(xQ,xO)|~sQ30_spl|~sQ4_spl),
% 0.13/0.41 inference(resolution,[status(thm)],[f1041,f921])).
% 0.13/0.41 fof(f1047,plain,(
% 0.13/0.41 $false|~sQ30_spl|~sQ4_spl),
% 0.13/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1044,f600])).
% 0.13/0.41 fof(f1048,plain,(
% 0.13/0.41 ~sQ30_spl|~sQ4_spl),
% 0.13/0.41 inference(contradiction_clause,[status(thm)],[f1047])).
% 0.13/0.41 fof(f1049,plain,(
% 0.13/0.41 $false),
% 0.13/0.41 inference(sat_refutation,[status(thm)],[f902,f909,f923,f980,f1043,f1048])).
% 0.13/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.43 % Elapsed time: 0.073824 seconds
% 0.13/0.43 % CPU time: 0.192437 seconds
% 0.13/0.43 % Total memory used: 94.732 MB
% 0.13/0.43 % Net memory used: 94.430 MB
%------------------------------------------------------------------------------