%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM606+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 : n014.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.14s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM606+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.11/0.36 % Computer : n014.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 02:44:04 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 0.14/0.42 % Refutation found
% 0.14/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.42 fof(f5,definition,(
% 0.14/0.42 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f6,axiom,(
% 0.14/0.42 isFinite0(slcrc0) ),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f9,axiom,(
% 0.14/0.42 (! [W0] :( ( aSet0(W0)& isCountable0(W0) )=> W0 != slcrc0 ) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f10,definition,(
% 0.14/0.42 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f12,axiom,(
% 0.14/0.42 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f23,axiom,(
% 0.14/0.42 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f73,hypothesis,(
% 0.14/0.42 ( aSet0(xT)& isFinite0(xT) ) ),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f75,hypothesis,(
% 0.14/0.42 ( aSet0(xS)& (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,szNzAzT0) ))& aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f95,hypothesis,(
% 0.14/0.42 ( 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.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f96,hypothesis,(
% 0.14/0.42 ( aSet0(xO)& isCountable0(xO) ) ),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f98,hypothesis,(
% 0.14/0.42 ( (! [W0] :( aElementOf0(W0,xO)=> aElementOf0(W0,xS) ))& aSubsetOf0(xO,xS) ) ),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f99,hypothesis,(
% 0.14/0.42 ( aSet0(xQ)& (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,xO) ))& aSubsetOf0(xQ,xO)& sbrdtbr0(xQ) = xK& aElementOf0(xQ,slbdtsldtrb0(xO,xK)) ) ),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f101,conjecture,(
% 0.14/0.42 ( (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,szNzAzT0) ))| aSubsetOf0(xQ,szNzAzT0) ) ),
% 0.14/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f102,negated_conjecture,(
% 0.14/0.42 ~(( (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,szNzAzT0) ))| aSubsetOf0(xQ,szNzAzT0) ) )),
% 0.14/0.42 inference(negated_conjecture,[status(cth)],[f101])).
% 0.14/0.42 fof(f113,plain,(
% 0.14/0.42 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.14/0.42 fof(f114,plain,(
% 0.14/0.42 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.14/0.42 inference(NNF_transformation,[status(thm)],[f113])).
% 0.14/0.42 fof(f115,plain,(
% 0.14/0.42 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.14/0.42 inference(miniscoping,[status(thm)],[f114])).
% 0.14/0.42 fof(f116,plain,(
% 0.14/0.42 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 0.14/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f115])).
% 0.14/0.42 fof(f117,plain,(
% 0.14/0.42 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f116])).
% 0.14/0.42 fof(f118,plain,(
% 0.14/0.42 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f116])).
% 0.14/0.42 fof(f120,plain,(
% 0.14/0.42 isFinite0(slcrc0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f6])).
% 0.14/0.42 fof(f125,plain,(
% 0.14/0.42 ![W0]: ((~aSet0(W0)|~isCountable0(W0))|~W0=slcrc0)),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.14/0.42 fof(f126,plain,(
% 0.14/0.42 ![X0]: (~aSet0(X0)|~isCountable0(X0)|~X0=slcrc0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.42 fof(f127,plain,(
% 0.14/0.42 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.14/0.42 fof(f128,plain,(
% 0.14/0.42 ![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.14/0.42 inference(NNF_transformation,[status(thm)],[f127])).
% 0.14/0.42 fof(f129,plain,(
% 0.14/0.42 ![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.14/0.42 inference(miniscoping,[status(thm)],[f128])).
% 0.14/0.42 fof(f130,plain,(
% 0.14/0.42 ![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.14/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f129])).
% 0.14/0.42 fof(f132,plain,(
% 0.14/0.42 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f130])).
% 0.14/0.42 fof(f137,plain,(
% 0.14/0.42 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.14/0.42 fof(f138,plain,(
% 0.14/0.42 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f137])).
% 0.14/0.42 fof(f179,plain,(
% 0.14/0.42 aSet0(szNzAzT0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f23])).
% 0.14/0.42 fof(f180,plain,(
% 0.14/0.42 isCountable0(szNzAzT0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f23])).
% 0.14/0.42 fof(f359,plain,(
% 0.14/0.42 aSet0(xT)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f73])).
% 0.14/0.42 fof(f360,plain,(
% 0.14/0.42 isFinite0(xT)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f73])).
% 0.14/0.42 fof(f362,plain,(
% 0.14/0.42 ((aSet0(xS)&(![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,szNzAzT0))))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 0.14/0.42 fof(f363,plain,(
% 0.14/0.42 aSet0(xS)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f362])).
% 0.14/0.42 fof(f365,plain,(
% 0.14/0.42 aSubsetOf0(xS,szNzAzT0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f362])).
% 0.14/0.42 fof(f366,plain,(
% 0.14/0.42 isCountable0(xS)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f362])).
% 0.14/0.42 fof(f565,plain,(
% 0.14/0.42 (((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.14/0.42 inference(NNF_transformation,[status(thm)],[f95])).
% 0.14/0.42 fof(f566,plain,(
% 0.14/0.42 (((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.14/0.42 inference(miniscoping,[status(thm)],[f565])).
% 0.14/0.42 fof(f567,plain,(
% 0.14/0.42 (((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.14/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(W1,sK34_skl(W0))],[f566])).
% 0.14/0.42 fof(f568,plain,(
% 0.14/0.42 aSet0(xO)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f567])).
% 0.14/0.42 fof(f577,plain,(
% 0.14/0.42 aSet0(xO)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f96])).
% 0.14/0.42 fof(f578,plain,(
% 0.14/0.42 isCountable0(xO)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f96])).
% 0.14/0.42 fof(f587,plain,(
% 0.14/0.42 (![W0]: (~aElementOf0(W0,xO)|aElementOf0(W0,xS)))&aSubsetOf0(xO,xS)),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f98])).
% 0.14/0.42 fof(f589,plain,(
% 0.14/0.42 aSubsetOf0(xO,xS)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f587])).
% 0.14/0.42 fof(f590,plain,(
% 0.14/0.42 (((aSet0(xQ)&(![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,xO))))&aSubsetOf0(xQ,xO))&sbrdtbr0(xQ)=xK)&aElementOf0(xQ,slbdtsldtrb0(xO,xK))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f99])).
% 0.14/0.42 fof(f592,plain,(
% 0.14/0.42 ![X0]: (~aElementOf0(X0,xQ)|aElementOf0(X0,xO))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f590])).
% 0.14/0.42 fof(f601,plain,(
% 0.14/0.42 ((?[W0]: (aElementOf0(W0,xQ)&~aElementOf0(W0,szNzAzT0)))&~aSubsetOf0(xQ,szNzAzT0))),
% 0.14/0.42 inference(pre_NNF_transformation,[status(thm)],[f102])).
% 0.14/0.42 fof(f602,plain,(
% 0.14/0.42 (aElementOf0(sK37_skl,xQ)&~aElementOf0(sK37_skl,szNzAzT0))&~aSubsetOf0(xQ,szNzAzT0)),
% 0.14/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK37_skl]),skolemize(W0,sK37_skl)],[f601])).
% 0.14/0.42 fof(f603,plain,(
% 0.14/0.42 aElementOf0(sK37_skl,xQ)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f602])).
% 0.14/0.42 fof(f604,plain,(
% 0.14/0.42 ~aElementOf0(sK37_skl,szNzAzT0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f602])).
% 0.14/0.42 fof(f788,plain,(
% 0.14/0.42 aSet0(slcrc0)),
% 0.14/0.42 inference(destructive_equality_resolution,[status(thm)],[f117])).
% 0.14/0.42 fof(f789,plain,(
% 0.14/0.42 ![X0]: (~aElementOf0(X0,slcrc0))),
% 0.14/0.42 inference(destructive_equality_resolution,[status(thm)],[f118])).
% 0.14/0.42 fof(f790,plain,(
% 0.14/0.42 ~aSet0(slcrc0)|~isCountable0(slcrc0)),
% 0.14/0.42 inference(destructive_equality_resolution,[status(thm)],[f126])).
% 0.14/0.42 fof(f853,definition,(
% 0.14/0.42 sQ0_spl <=> (aSet0(xO))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f855,plain,(
% 0.14/0.42 ~aSet0(xO)|sQ0_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f853])).
% 0.14/0.42 fof(f863,plain,(
% 0.14/0.42 aElementOf0(sK37_skl,xO)),
% 0.14/0.42 inference(resolution,[status(thm)],[f592,f603])).
% 0.14/0.42 fof(f865,plain,(
% 0.14/0.42 ![X0]: (~aSet0(X0)|~aSubsetOf0(xO,X0)|aElementOf0(sK37_skl,X0))),
% 0.14/0.42 inference(resolution,[status(thm)],[f132,f863])).
% 0.14/0.42 fof(f868,plain,(
% 0.14/0.42 ![X0]: (~aSet0(szNzAzT0)|~aSubsetOf0(X0,szNzAzT0)|~aElementOf0(sK37_skl,X0))),
% 0.14/0.42 inference(resolution,[status(thm)],[f132,f604])).
% 0.14/0.42 fof(f873,definition,(
% 0.14/0.42 sQ2_spl <=> (aSet0(szNzAzT0))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f875,plain,(
% 0.14/0.42 ~aSet0(szNzAzT0)|sQ2_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f873])).
% 0.14/0.42 fof(f876,definition,(
% 0.14/0.42 ![X0]: (sQ3_spl <=> (~aSubsetOf0(X0,szNzAzT0)|~aElementOf0(sK37_skl,X0)))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f877,plain,(
% 0.14/0.42 ![X0]: (~aSubsetOf0(X0,szNzAzT0)|~aElementOf0(sK37_skl,X0)|~sQ3_spl)),
% 0.14/0.42 inference(component_clause,[status(thm)],[f876])).
% 0.14/0.42 fof(f879,plain,(
% 0.14/0.42 ~sQ2_spl|sQ3_spl),
% 0.14/0.42 inference(split_clause,[status(thm)],[f868,f873,f876])).
% 0.14/0.42 fof(f910,plain,(
% 0.14/0.42 aSubsetOf0(slcrc0,slcrc0)),
% 0.14/0.42 inference(resolution,[status(thm)],[f788,f138])).
% 0.14/0.42 fof(f912,plain,(
% 0.14/0.42 aSubsetOf0(xT,xT)),
% 0.14/0.42 inference(resolution,[status(thm)],[f359,f138])).
% 0.14/0.42 fof(f970,definition,(
% 0.14/0.42 sQ22_spl <=> (aElementOf0(sK0_skl(slcrc0),slcrc0))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f971,plain,(
% 0.14/0.42 aElementOf0(sK0_skl(slcrc0),slcrc0)|~sQ22_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f970])).
% 0.14/0.42 fof(f983,plain,(
% 0.14/0.42 $false|sQ2_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f875,f179])).
% 0.14/0.42 fof(f984,plain,(
% 0.14/0.42 sQ2_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f983])).
% 0.14/0.42 fof(f1000,definition,(
% 0.14/0.42 sQ27_spl <=> (aSubsetOf0(slcrc0,slcrc0))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f1002,plain,(
% 0.14/0.42 ~aSubsetOf0(slcrc0,slcrc0)|sQ27_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f1000])).
% 0.14/0.42 fof(f1019,definition,(
% 0.14/0.42 sQ30_spl <=> (aSet0(xT))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f1021,plain,(
% 0.14/0.42 ~aSet0(xT)|sQ30_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f1019])).
% 0.14/0.42 fof(f1022,definition,(
% 0.14/0.42 sQ31_spl <=> (aSubsetOf0(xT,xT))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f1024,plain,(
% 0.14/0.42 ~aSubsetOf0(xT,xT)|sQ31_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f1022])).
% 0.14/0.42 fof(f1032,definition,(
% 0.14/0.42 sQ33_spl <=> (aSet0(xS))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f1034,plain,(
% 0.14/0.42 ~aSet0(xS)|sQ33_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f1032])).
% 0.14/0.42 fof(f1045,plain,(
% 0.14/0.42 $false|sQ33_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1034,f363])).
% 0.14/0.42 fof(f1046,plain,(
% 0.14/0.42 sQ33_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1045])).
% 0.14/0.42 fof(f1094,plain,(
% 0.14/0.42 $false|sQ30_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1021,f359])).
% 0.14/0.42 fof(f1095,plain,(
% 0.14/0.42 sQ30_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1094])).
% 0.14/0.42 fof(f1096,plain,(
% 0.14/0.42 $false|sQ31_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1024,f912])).
% 0.14/0.42 fof(f1097,plain,(
% 0.14/0.42 sQ31_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1096])).
% 0.14/0.42 fof(f1099,plain,(
% 0.14/0.42 $false|sQ0_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f568,f855])).
% 0.14/0.42 fof(f1100,plain,(
% 0.14/0.42 sQ0_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1099])).
% 0.14/0.42 fof(f1102,plain,(
% 0.14/0.42 aSubsetOf0(xO,xO)),
% 0.14/0.42 inference(resolution,[status(thm)],[f577,f138])).
% 0.14/0.42 fof(f1103,definition,(
% 0.14/0.42 sQ43_spl <=> (xO=slcrc0)),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f1104,plain,(
% 0.14/0.42 xO=slcrc0|~sQ43_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f1103])).
% 0.14/0.42 fof(f1148,definition,(
% 0.14/0.42 sQ45_spl <=> (isCountable0(xO))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f1150,plain,(
% 0.14/0.42 ~isCountable0(xO)|sQ45_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f1148])).
% 0.14/0.42 fof(f1162,plain,(
% 0.14/0.42 $false|sQ45_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1150,f578])).
% 0.14/0.42 fof(f1163,plain,(
% 0.14/0.42 sQ45_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1162])).
% 0.14/0.42 fof(f1164,plain,(
% 0.14/0.42 ~aSet0(xO)|~isCountable0(slcrc0)|~sQ43_spl),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f1104,f790])).
% 0.14/0.42 fof(f1165,plain,(
% 0.14/0.42 ~aSet0(xO)|~isCountable0(xO)|~sQ43_spl),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f1104,f1164])).
% 0.14/0.42 fof(f1166,plain,(
% 0.14/0.42 $false|~sQ43_spl),
% 0.14/0.42 inference(backward_subsumption_resolution,[status(thm)],[f578,f1167])).
% 0.14/0.42 fof(f1167,plain,(
% 0.14/0.42 ~isCountable0(xO)|~sQ43_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1165,f577])).
% 0.14/0.42 fof(f1168,plain,(
% 0.14/0.42 ~sQ43_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1166])).
% 0.14/0.42 fof(f1189,definition,(
% 0.14/0.42 sQ52_spl <=> (aSubsetOf0(xO,xO))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f1191,plain,(
% 0.14/0.42 ~aSubsetOf0(xO,xO)|sQ52_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f1189])).
% 0.14/0.42 fof(f1197,plain,(
% 0.14/0.42 $false|sQ52_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1191,f1102])).
% 0.14/0.42 fof(f1198,plain,(
% 0.14/0.42 sQ52_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1197])).
% 0.14/0.42 fof(f1225,definition,(
% 0.14/0.42 sQ54_spl <=> (isCountable0(xS))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f1227,plain,(
% 0.14/0.42 ~isCountable0(xS)|sQ54_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f1225])).
% 0.14/0.42 fof(f1232,plain,(
% 0.14/0.42 $false|sQ54_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1227,f366])).
% 0.14/0.42 fof(f1233,plain,(
% 0.14/0.42 sQ54_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1232])).
% 0.14/0.42 fof(f1246,definition,(
% 0.14/0.42 sQ56_spl <=> (isCountable0(szNzAzT0))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f1248,plain,(
% 0.14/0.42 ~isCountable0(szNzAzT0)|sQ56_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f1246])).
% 0.14/0.42 fof(f1253,plain,(
% 0.14/0.42 $false|sQ56_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1248,f180])).
% 0.14/0.42 fof(f1254,plain,(
% 0.14/0.42 sQ56_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1253])).
% 0.14/0.42 fof(f1258,definition,(
% 0.14/0.42 sQ58_spl <=> (isFinite0(slcrc0))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f1260,plain,(
% 0.14/0.42 ~isFinite0(slcrc0)|sQ58_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f1258])).
% 0.14/0.42 fof(f1262,plain,(
% 0.14/0.42 $false|sQ58_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1260,f120])).
% 0.14/0.42 fof(f1263,plain,(
% 0.14/0.42 sQ58_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1262])).
% 0.14/0.42 fof(f1270,definition,(
% 0.14/0.42 sQ60_spl <=> (isFinite0(xT))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f1272,plain,(
% 0.14/0.42 ~isFinite0(xT)|sQ60_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f1270])).
% 0.14/0.42 fof(f1274,plain,(
% 0.14/0.42 $false|sQ60_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1272,f360])).
% 0.14/0.42 fof(f1275,plain,(
% 0.14/0.42 sQ60_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1274])).
% 0.14/0.42 fof(f1483,plain,(
% 0.14/0.42 ~aSet0(xS)|aElementOf0(sK37_skl,xS)),
% 0.14/0.42 inference(resolution,[status(thm)],[f589,f865])).
% 0.14/0.42 fof(f1489,definition,(
% 0.14/0.42 sQ75_spl <=> (aElementOf0(sK37_skl,xS))),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.14/0.42 fof(f1490,plain,(
% 0.14/0.42 aElementOf0(sK37_skl,xS)|~sQ75_spl),
% 0.14/0.42 inference(component_clause,[status(thm)],[f1489])).
% 0.14/0.42 fof(f1492,plain,(
% 0.14/0.42 ~sQ33_spl|sQ75_spl),
% 0.14/0.42 inference(split_clause,[status(thm)],[f1483,f1032,f1489])).
% 0.14/0.42 fof(f1550,plain,(
% 0.14/0.42 ~aSubsetOf0(xS,szNzAzT0)|~sQ75_spl|~sQ3_spl),
% 0.14/0.42 inference(resolution,[status(thm)],[f1490,f877])).
% 0.14/0.42 fof(f1687,plain,(
% 0.14/0.42 $false|sQ27_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1002,f910])).
% 0.14/0.42 fof(f1688,plain,(
% 0.14/0.42 sQ27_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1687])).
% 0.14/0.42 fof(f1689,plain,(
% 0.14/0.42 $false|~sQ22_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f971,f789])).
% 0.14/0.42 fof(f1690,plain,(
% 0.14/0.42 ~sQ22_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1689])).
% 0.14/0.42 fof(f1828,plain,(
% 0.14/0.42 $false|~sQ75_spl|~sQ3_spl),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f365,f1550])).
% 0.14/0.42 fof(f1829,plain,(
% 0.14/0.42 ~sQ75_spl|~sQ3_spl),
% 0.14/0.42 inference(contradiction_clause,[status(thm)],[f1828])).
% 0.14/0.42 fof(f1830,plain,(
% 0.14/0.42 $false),
% 0.14/0.42 inference(sat_refutation,[status(thm)],[f879,f984,f1046,f1095,f1097,f1100,f1163,f1168,f1198,f1233,f1254,f1263,f1275,f1492,f1688,f1690,f1829])).
% 0.14/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.46 % Elapsed time: 0.081513 seconds
% 0.14/0.46 % CPU time: 0.322231 seconds
% 0.14/0.46 % Total memory used: 127.212 MB
% 0.14/0.46 % Net memory used: 126.667 MB
%------------------------------------------------------------------------------