%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM607+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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.10s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM607+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n006.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 02:44:29 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.41 % Refutation found
% 0.10/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.41 fof(f5,definition,(
% 0.10/0.41 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f10,definition,(
% 0.10/0.41 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f12,axiom,(
% 0.10/0.41 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f23,axiom,(
% 0.10/0.41 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f73,hypothesis,(
% 0.10/0.41 ( aSet0(xT)& isFinite0(xT) ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f75,hypothesis,(
% 0.10/0.41 ( aSet0(xS)& (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,szNzAzT0) ))& aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f95,hypothesis,(
% 0.10/0.41 ( 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.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f96,hypothesis,(
% 0.10/0.41 ( aSet0(xO)& isCountable0(xO) ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f98,hypothesis,(
% 0.10/0.41 ( (! [W0] :( aElementOf0(W0,xO)=> aElementOf0(W0,xS) ))& aSubsetOf0(xO,xS) ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f99,hypothesis,(
% 0.10/0.41 ( aSet0(xQ)& (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,xO) ))& aSubsetOf0(xQ,xO)& sbrdtbr0(xQ) = xK& aElementOf0(xQ,slbdtsldtrb0(xO,xK)) ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f100,hypothesis,(
% 0.10/0.41 ( (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,xO) ))& ~ ( ~ (? [W0] : aElementOf0(W0,xQ))| xQ = slcrc0 ) ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f102,conjecture,(
% 0.10/0.41 ( (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,xS) ))| aSubsetOf0(xQ,xS)| (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,xS) ))| aSubsetOf0(xQ,xS)| aElementOf0(xQ,szDzozmdt0(xc)) ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f103,negated_conjecture,(
% 0.10/0.41 ~(( (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,xS) ))| aSubsetOf0(xQ,xS)| (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,xS) ))| aSubsetOf0(xQ,xS)| aElementOf0(xQ,szDzozmdt0(xc)) ) )),
% 0.10/0.41 inference(negated_conjecture,[status(cth)],[f102])).
% 0.10/0.41 fof(f114,plain,(
% 0.10/0.41 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.10/0.41 fof(f115,plain,(
% 0.10/0.41 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.10/0.41 inference(NNF_transformation,[status(thm)],[f114])).
% 0.10/0.41 fof(f116,plain,(
% 0.10/0.41 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.10/0.41 inference(miniscoping,[status(thm)],[f115])).
% 0.10/0.41 fof(f117,plain,(
% 0.10/0.41 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 0.10/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f116])).
% 0.10/0.41 fof(f118,plain,(
% 0.10/0.41 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f117])).
% 0.10/0.41 fof(f128,plain,(
% 0.10/0.41 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.10/0.41 fof(f129,plain,(
% 0.10/0.41 ![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.10/0.41 inference(NNF_transformation,[status(thm)],[f128])).
% 0.10/0.41 fof(f130,plain,(
% 0.10/0.41 ![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.10/0.41 inference(miniscoping,[status(thm)],[f129])).
% 0.10/0.41 fof(f131,plain,(
% 0.10/0.41 ![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.10/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f130])).
% 0.10/0.41 fof(f133,plain,(
% 0.10/0.41 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f131])).
% 0.10/0.41 fof(f138,plain,(
% 0.10/0.41 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.10/0.41 fof(f139,plain,(
% 0.10/0.41 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f138])).
% 0.10/0.41 fof(f180,plain,(
% 0.10/0.41 aSet0(szNzAzT0)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f23])).
% 0.10/0.41 fof(f181,plain,(
% 0.10/0.41 isCountable0(szNzAzT0)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f23])).
% 0.10/0.41 fof(f360,plain,(
% 0.10/0.41 aSet0(xT)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f73])).
% 0.10/0.41 fof(f363,plain,(
% 0.10/0.41 ((aSet0(xS)&(![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,szNzAzT0))))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 0.10/0.41 fof(f364,plain,(
% 0.10/0.41 aSet0(xS)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f363])).
% 0.10/0.41 fof(f367,plain,(
% 0.10/0.41 isCountable0(xS)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f363])).
% 0.10/0.41 fof(f566,plain,(
% 0.10/0.41 (((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.10/0.41 inference(NNF_transformation,[status(thm)],[f95])).
% 0.10/0.41 fof(f567,plain,(
% 0.10/0.41 (((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.10/0.41 inference(miniscoping,[status(thm)],[f566])).
% 0.10/0.41 fof(f568,plain,(
% 0.10/0.41 (((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.10/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK34_skl]),skolemize(W1,sK34_skl(W0))],[f567])).
% 0.10/0.41 fof(f569,plain,(
% 0.10/0.41 aSet0(xO)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f568])).
% 0.10/0.41 fof(f579,plain,(
% 0.10/0.41 isCountable0(xO)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f96])).
% 0.10/0.41 fof(f588,plain,(
% 0.10/0.41 (![W0]: (~aElementOf0(W0,xO)|aElementOf0(W0,xS)))&aSubsetOf0(xO,xS)),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f98])).
% 0.10/0.41 fof(f590,plain,(
% 0.10/0.41 aSubsetOf0(xO,xS)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f588])).
% 0.10/0.41 fof(f591,plain,(
% 0.10/0.41 (((aSet0(xQ)&(![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,xO))))&aSubsetOf0(xQ,xO))&sbrdtbr0(xQ)=xK)&aElementOf0(xQ,slbdtsldtrb0(xO,xK))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f99])).
% 0.10/0.41 fof(f592,plain,(
% 0.10/0.41 aSet0(xQ)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f591])).
% 0.10/0.41 fof(f594,plain,(
% 0.10/0.41 aSubsetOf0(xQ,xO)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f591])).
% 0.10/0.41 fof(f597,plain,(
% 0.10/0.41 (![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,xO)))&((?[W0]: aElementOf0(W0,xQ))&~xQ=slcrc0)),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f100])).
% 0.10/0.41 fof(f598,plain,(
% 0.10/0.41 (![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,xO)))&(aElementOf0(sK36_skl,xQ)&~xQ=slcrc0)),
% 0.10/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl]),skolemize(W0,sK36_skl)],[f597])).
% 0.10/0.41 fof(f601,plain,(
% 0.10/0.41 ~xQ=slcrc0),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f598])).
% 0.10/0.41 fof(f605,plain,(
% 0.10/0.41 (((((?[W0]: (aElementOf0(W0,xQ)&~aElementOf0(W0,xS)))&~aSubsetOf0(xQ,xS))&(?[W0]: (aElementOf0(W0,xQ)&~aElementOf0(W0,xS))))&~aSubsetOf0(xQ,xS))&~aElementOf0(xQ,szDzozmdt0(xc)))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f103])).
% 0.10/0.41 fof(f606,plain,(
% 0.10/0.41 ((((aElementOf0(sK37_skl,xQ)&~aElementOf0(sK37_skl,xS))&~aSubsetOf0(xQ,xS))&(aElementOf0(sK38_skl,xQ)&~aElementOf0(sK38_skl,xS)))&~aSubsetOf0(xQ,xS))&~aElementOf0(xQ,szDzozmdt0(xc))),
% 0.10/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK37_skl,sK38_skl]),skolemize(W0,sK37_skl),skolemize(W0,sK38_skl)],[f605])).
% 0.10/0.41 fof(f610,plain,(
% 0.10/0.41 aElementOf0(sK38_skl,xQ)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f606])).
% 0.10/0.41 fof(f611,plain,(
% 0.10/0.41 ~aElementOf0(sK38_skl,xS)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f606])).
% 0.10/0.41 fof(f796,plain,(
% 0.10/0.41 aSet0(slcrc0)),
% 0.10/0.41 inference(destructive_equality_resolution,[status(thm)],[f118])).
% 0.10/0.41 fof(f863,definition,(
% 0.10/0.41 sQ0_spl <=> (aSet0(szNzAzT0))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f865,plain,(
% 0.10/0.41 ~aSet0(szNzAzT0)|sQ0_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f863])).
% 0.10/0.41 fof(f870,definition,(
% 0.10/0.41 sQ2_spl <=> (aSet0(xO))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f872,plain,(
% 0.10/0.41 ~aSet0(xO)|sQ2_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f870])).
% 0.10/0.41 fof(f874,definition,(
% 0.10/0.41 sQ3_spl <=> (aSet0(xS))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f876,plain,(
% 0.10/0.41 ~aSet0(xS)|sQ3_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f874])).
% 0.10/0.41 fof(f878,plain,(
% 0.10/0.41 ![X0]: (~aSet0(X0)|~aSubsetOf0(xQ,X0)|aElementOf0(sK38_skl,X0))),
% 0.10/0.41 inference(resolution,[status(thm)],[f133,f610])).
% 0.10/0.41 fof(f881,plain,(
% 0.10/0.41 ![X0]: (~aSet0(xS)|~aSubsetOf0(X0,xS)|~aElementOf0(sK38_skl,X0))),
% 0.10/0.41 inference(resolution,[status(thm)],[f133,f611])).
% 0.10/0.41 fof(f885,definition,(
% 0.10/0.41 ![X0]: (sQ4_spl <=> (~aSubsetOf0(X0,xS)|~aElementOf0(sK38_skl,X0)))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f886,plain,(
% 0.10/0.41 ![X0]: (~aSubsetOf0(X0,xS)|~aElementOf0(sK38_skl,X0)|~sQ4_spl)),
% 0.10/0.41 inference(component_clause,[status(thm)],[f885])).
% 0.10/0.41 fof(f888,plain,(
% 0.10/0.41 ~sQ3_spl|sQ4_spl),
% 0.10/0.41 inference(split_clause,[status(thm)],[f881,f874,f885])).
% 0.10/0.41 fof(f894,plain,(
% 0.10/0.41 $false|sQ3_spl),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f876,f364])).
% 0.10/0.41 fof(f895,plain,(
% 0.10/0.41 sQ3_spl),
% 0.10/0.41 inference(contradiction_clause,[status(thm)],[f894])).
% 0.10/0.41 fof(f908,plain,(
% 0.10/0.41 $false|sQ2_spl),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f872,f569])).
% 0.10/0.41 fof(f909,plain,(
% 0.10/0.41 sQ2_spl),
% 0.10/0.41 inference(contradiction_clause,[status(thm)],[f908])).
% 0.10/0.41 fof(f911,definition,(
% 0.10/0.41 sQ8_spl <=> (aSet0(slcrc0))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f913,plain,(
% 0.10/0.41 ~aSet0(slcrc0)|sQ8_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f911])).
% 0.10/0.41 fof(f918,plain,(
% 0.10/0.41 $false|sQ8_spl),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f913,f796])).
% 0.10/0.41 fof(f919,plain,(
% 0.10/0.41 sQ8_spl),
% 0.10/0.41 inference(contradiction_clause,[status(thm)],[f918])).
% 0.10/0.41 fof(f954,definition,(
% 0.10/0.41 sQ18_spl <=> (xQ=slcrc0)),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f955,plain,(
% 0.10/0.41 xQ=slcrc0|~sQ18_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f954])).
% 0.10/0.41 fof(f968,plain,(
% 0.10/0.41 $false|~sQ18_spl),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f955,f601])).
% 0.10/0.41 fof(f969,plain,(
% 0.10/0.41 ~sQ18_spl),
% 0.10/0.41 inference(contradiction_clause,[status(thm)],[f968])).
% 0.10/0.41 fof(f981,plain,(
% 0.10/0.41 ~aSet0(xO)|aElementOf0(sK38_skl,xO)),
% 0.10/0.41 inference(resolution,[status(thm)],[f878,f594])).
% 0.10/0.41 fof(f986,definition,(
% 0.10/0.41 sQ25_spl <=> (aElementOf0(sK38_skl,xO))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f987,plain,(
% 0.10/0.41 aElementOf0(sK38_skl,xO)|~sQ25_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f986])).
% 0.10/0.41 fof(f989,plain,(
% 0.10/0.41 ~sQ2_spl|sQ25_spl),
% 0.10/0.41 inference(split_clause,[status(thm)],[f981,f870,f986])).
% 0.10/0.41 fof(f990,plain,(
% 0.10/0.41 $false|sQ0_spl),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f865,f180])).
% 0.10/0.41 fof(f991,plain,(
% 0.10/0.41 sQ0_spl),
% 0.10/0.41 inference(contradiction_clause,[status(thm)],[f990])).
% 0.10/0.41 fof(f1002,plain,(
% 0.10/0.41 ~aSubsetOf0(xO,xS)|~sQ25_spl|~sQ4_spl),
% 0.10/0.41 inference(resolution,[status(thm)],[f987,f886])).
% 0.10/0.41 fof(f1014,plain,(
% 0.10/0.41 aSubsetOf0(xO,xO)),
% 0.10/0.41 inference(resolution,[status(thm)],[f139,f569])).
% 0.10/0.41 fof(f1015,plain,(
% 0.10/0.41 aSubsetOf0(xT,xT)),
% 0.10/0.41 inference(resolution,[status(thm)],[f139,f360])).
% 0.10/0.41 fof(f1016,plain,(
% 0.10/0.41 aSubsetOf0(szNzAzT0,szNzAzT0)),
% 0.10/0.41 inference(resolution,[status(thm)],[f139,f180])).
% 0.10/0.41 fof(f1017,plain,(
% 0.10/0.41 aSubsetOf0(xQ,xQ)),
% 0.10/0.41 inference(resolution,[status(thm)],[f139,f592])).
% 0.10/0.41 fof(f1018,plain,(
% 0.10/0.41 aSubsetOf0(xS,xS)),
% 0.10/0.41 inference(resolution,[status(thm)],[f139,f364])).
% 0.10/0.41 fof(f1068,definition,(
% 0.10/0.41 sQ33_spl <=> (isCountable0(xO))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f1070,plain,(
% 0.10/0.41 ~isCountable0(xO)|sQ33_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f1068])).
% 0.10/0.41 fof(f1082,definition,(
% 0.10/0.41 sQ37_spl <=> (isCountable0(xS))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f1084,plain,(
% 0.10/0.41 ~isCountable0(xS)|sQ37_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f1082])).
% 0.10/0.41 fof(f1089,plain,(
% 0.10/0.41 $false|sQ37_spl),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1084,f367])).
% 0.10/0.41 fof(f1090,plain,(
% 0.10/0.41 sQ37_spl),
% 0.10/0.41 inference(contradiction_clause,[status(thm)],[f1089])).
% 0.10/0.41 fof(f1091,plain,(
% 0.10/0.41 $false|sQ33_spl),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1070,f579])).
% 0.10/0.41 fof(f1092,plain,(
% 0.10/0.41 sQ33_spl),
% 0.10/0.41 inference(contradiction_clause,[status(thm)],[f1091])).
% 0.10/0.41 fof(f1099,definition,(
% 0.10/0.41 sQ39_spl <=> (aSet0(xT))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f1101,plain,(
% 0.10/0.41 ~aSet0(xT)|sQ39_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f1099])).
% 0.10/0.41 fof(f1120,definition,(
% 0.10/0.41 sQ41_spl <=> (aSubsetOf0(xO,xO))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f1122,plain,(
% 0.10/0.41 ~aSubsetOf0(xO,xO)|sQ41_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f1120])).
% 0.10/0.41 fof(f1128,plain,(
% 0.10/0.41 $false|sQ41_spl),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1122,f1014])).
% 0.10/0.41 fof(f1129,plain,(
% 0.10/0.41 sQ41_spl),
% 0.10/0.41 inference(contradiction_clause,[status(thm)],[f1128])).
% 0.10/0.41 fof(f1132,definition,(
% 0.10/0.41 sQ43_spl <=> (aSubsetOf0(xT,xT))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f1134,plain,(
% 0.10/0.41 ~aSubsetOf0(xT,xT)|sQ43_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f1132])).
% 0.10/0.41 fof(f1142,definition,(
% 0.10/0.41 sQ45_spl <=> (aSubsetOf0(szNzAzT0,szNzAzT0))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f1144,plain,(
% 0.10/0.41 ~aSubsetOf0(szNzAzT0,szNzAzT0)|sQ45_spl),
% 0.10/0.41 inference(component_clause,[status(thm)],[f1142])).
% 0.10/0.41 fof(f1150,plain,(
% 0.10/0.41 $false|sQ45_spl),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1144,f1016])).
% 0.10/0.41 fof(f1151,plain,(
% 0.10/0.41 sQ45_spl),
% 0.10/0.41 inference(contradiction_clause,[status(thm)],[f1150])).
% 0.10/0.41 fof(f1164,definition,(
% 0.10/0.41 sQ49_spl <=> (aSubsetOf0(xQ,xQ))),
% 0.10/0.41 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.10/0.41 fof(f1166,plain,(
% 0.10/0.41 ~aSubsetOf0(xQ,xQ)|sQ49_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f1164])).
% 0.10/0.42 fof(f1172,plain,(
% 0.10/0.42 $false|sQ49_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1166,f1017])).
% 0.10/0.42 fof(f1173,plain,(
% 0.10/0.42 sQ49_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1172])).
% 0.10/0.42 fof(f1176,definition,(
% 0.10/0.42 sQ51_spl <=> (aSubsetOf0(xS,xS))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f1178,plain,(
% 0.10/0.42 ~aSubsetOf0(xS,xS)|sQ51_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f1176])).
% 0.10/0.42 fof(f1184,plain,(
% 0.10/0.42 $false|sQ51_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1178,f1018])).
% 0.10/0.42 fof(f1185,plain,(
% 0.10/0.42 sQ51_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1184])).
% 0.10/0.42 fof(f1222,plain,(
% 0.10/0.42 $false|sQ39_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f360,f1101])).
% 0.10/0.42 fof(f1223,plain,(
% 0.10/0.42 sQ39_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1222])).
% 0.10/0.42 fof(f1224,plain,(
% 0.10/0.42 $false|sQ43_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1134,f1015])).
% 0.10/0.42 fof(f1225,plain,(
% 0.10/0.42 sQ43_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1224])).
% 0.10/0.42 fof(f1240,definition,(
% 0.10/0.42 sQ62_spl <=> (isCountable0(szNzAzT0))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f1242,plain,(
% 0.10/0.42 ~isCountable0(szNzAzT0)|sQ62_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f1240])).
% 0.10/0.42 fof(f1247,plain,(
% 0.10/0.42 $false|sQ62_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1242,f181])).
% 0.10/0.42 fof(f1248,plain,(
% 0.10/0.42 sQ62_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1247])).
% 0.10/0.42 fof(f1384,plain,(
% 0.10/0.42 $false|~sQ25_spl|~sQ4_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f590,f1002])).
% 0.10/0.42 fof(f1385,plain,(
% 0.10/0.42 ~sQ25_spl|~sQ4_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1384])).
% 0.10/0.42 fof(f1386,plain,(
% 0.10/0.42 $false),
% 0.10/0.42 inference(sat_refutation,[status(thm)],[f888,f895,f909,f919,f969,f989,f991,f1090,f1092,f1129,f1151,f1173,f1185,f1223,f1225,f1248,f1385])).
% 0.10/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.44 % Elapsed time: 0.067961 seconds
% 0.10/0.44 % CPU time: 0.236642 seconds
% 0.10/0.44 % Total memory used: 56.380 MB
% 0.10/0.44 % Net memory used: 56.108 MB
%------------------------------------------------------------------------------