%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM566+1 : 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 : n019.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:14 PM UTC 2026
% Result : Theorem 64.87s 8.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM566+1 : 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.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 02:40:21 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 64.87/8.69 % Refutation found
% 64.87/8.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 64.87/8.69 % SZS output start CNFRefutation for theBenchmark
% 64.87/8.69 fof(f10,definition,(
% 64.87/8.69 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 64.87/8.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.87/8.69 fof(f12,axiom,(
% 64.87/8.69 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 64.87/8.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.87/8.69 fof(f23,axiom,(
% 64.87/8.69 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 64.87/8.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.87/8.69 fof(f64,axiom,(
% 64.87/8.69 (! [W0] :( aFunction0(W0)=> aSet0(szDzozmdt0(W0)) ) )),
% 64.87/8.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.87/8.69 fof(f68,definition,(
% 64.87/8.69 (! [W0] :( aFunction0(W0)=> (! [W1] :( aSubsetOf0(W1,szDzozmdt0(W0))=> (! [W2] :( W2 = sdtlcdtrc0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> (? [W4] :( aElementOf0(W4,W1)& sdtlpdtrp0(W0,W4) = W3 ) )) )) ) )) )) )),
% 64.87/8.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.87/8.69 fof(f73,hypothesis,(
% 64.87/8.69 ( aSet0(xT)& isFinite0(xT) ) ),
% 64.87/8.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.87/8.69 fof(f75,hypothesis,(
% 64.87/8.69 ( aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 64.87/8.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.87/8.69 fof(f76,hypothesis,(
% 64.87/8.69 ( aFunction0(xc)& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ),
% 64.87/8.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.87/8.69 fof(f78,hypothesis,(
% 64.87/8.69 xK = sz00 ),
% 64.87/8.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.87/8.69 fof(f79,hypothesis,(
% 64.87/8.69 aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00)) ),
% 64.87/8.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.87/8.69 fof(f80,hypothesis,(
% 64.87/8.69 (! [W0] :( aElementOf0(W0,slbdtsldtrb0(xS,sz00))=> sdtlpdtrp0(xc,W0) = sdtlpdtrp0(xc,slcrc0) ) )),
% 64.87/8.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.87/8.69 fof(f81,conjecture,(
% 64.87/8.69 (? [W0] :( aElementOf0(W0,xT)& (? [W1] :( aSubsetOf0(W1,xS)& isCountable0(W1)& (! [W2] :( aElementOf0(W2,slbdtsldtrb0(W1,xK))=> sdtlpdtrp0(xc,W2) = W0 ) )) )) )),
% 64.87/8.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.87/8.69 fof(f82,negated_conjecture,(
% 64.87/8.69 ~((? [W0] :( aElementOf0(W0,xT)& (? [W1] :( aSubsetOf0(W1,xS)& isCountable0(W1)& (! [W2] :( aElementOf0(W2,slbdtsldtrb0(W1,xK))=> sdtlpdtrp0(xc,W2) = W0 ) )) )) ))),
% 64.87/8.69 inference(negated_conjecture,[status(cth)],[f81])).
% 64.87/8.69 fof(f107,plain,(
% 64.87/8.69 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 64.87/8.69 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 64.87/8.69 fof(f108,plain,(
% 64.87/8.69 ![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))))))))),
% 64.87/8.69 inference(NNF_transformation,[status(thm)],[f107])).
% 64.87/8.69 fof(f109,plain,(
% 64.87/8.69 ![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))))))))),
% 64.87/8.69 inference(miniscoping,[status(thm)],[f108])).
% 64.87/8.69 fof(f110,plain,(
% 64.87/8.69 ![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)))))))),
% 64.87/8.69 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f109])).
% 64.87/8.69 fof(f111,plain,(
% 64.87/8.69 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f110])).
% 64.87/8.69 fof(f112,plain,(
% 64.87/8.69 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f110])).
% 64.87/8.69 fof(f117,plain,(
% 64.87/8.69 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 64.87/8.69 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 64.87/8.69 fof(f118,plain,(
% 64.87/8.69 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f117])).
% 64.87/8.69 fof(f159,plain,(
% 64.87/8.69 aSet0(szNzAzT0)),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f23])).
% 64.87/8.69 fof(f291,plain,(
% 64.87/8.69 ![W0]: (~aFunction0(W0)|aSet0(szDzozmdt0(W0)))),
% 64.87/8.69 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 64.87/8.69 fof(f292,plain,(
% 64.87/8.69 ![X0]: (~aFunction0(X0)|aSet0(szDzozmdt0(X0)))),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f291])).
% 64.87/8.69 fof(f308,plain,(
% 64.87/8.69 ![W0]: (~aFunction0(W0)|(![W1]: (~aSubsetOf0(W1,szDzozmdt0(W0))|(![W2]: (W2=sdtlcdtrc0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(?[W4]: (aElementOf0(W4,W1)&sdtlpdtrp0(W0,W4)=W3))))))))))),
% 64.87/8.69 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 64.87/8.69 fof(f309,plain,(
% 64.87/8.69 ![W0]: (~aFunction0(W0)|(![W1]: (~aSubsetOf0(W1,szDzozmdt0(W0))|(![W2]: ((~W2=sdtlcdtrc0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(?[W4]: (aElementOf0(W4,W1)&sdtlpdtrp0(W0,W4)=W3)))&(aElementOf0(W3,W2)|(![W4]: (~aElementOf0(W4,W1)|~sdtlpdtrp0(W0,W4)=W3)))))))&(W2=sdtlcdtrc0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(![W4]: (~aElementOf0(W4,W1)|~sdtlpdtrp0(W0,W4)=W3)))&(aElementOf0(W3,W2)|(?[W4]: (aElementOf0(W4,W1)&sdtlpdtrp0(W0,W4)=W3))))))))))))),
% 64.87/8.69 inference(NNF_transformation,[status(thm)],[f308])).
% 64.87/8.69 fof(f310,plain,(
% 64.87/8.69 ![W0]: (~aFunction0(W0)|(![W1]: (~aSubsetOf0(W1,szDzozmdt0(W0))|((![W2]: (~W2=sdtlcdtrc0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(?[W4]: (aElementOf0(W4,W1)&sdtlpdtrp0(W0,W4)=W3))))&(![W3]: (aElementOf0(W3,W2)|(![W4]: (~aElementOf0(W4,W1)|~sdtlpdtrp0(W0,W4)=W3))))))))&(![W2]: (W2=sdtlcdtrc0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(![W4]: (~aElementOf0(W4,W1)|~sdtlpdtrp0(W0,W4)=W3)))&(aElementOf0(W3,W2)|(?[W4]: (aElementOf0(W4,W1)&sdtlpdtrp0(W0,W4)=W3))))))))))))),
% 64.87/8.69 inference(miniscoping,[status(thm)],[f309])).
% 64.87/8.69 fof(f311,plain,(
% 64.87/8.69 ![W0]: (~aFunction0(W0)|(![W1]: (~aSubsetOf0(W1,szDzozmdt0(W0))|((![W2]: (~W2=sdtlcdtrc0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElementOf0(sK13_skl(W3,W2,W1,W0),W1)&sdtlpdtrp0(W0,sK13_skl(W3,W2,W1,W0))=W3)))&(![W3]: (aElementOf0(W3,W2)|(![W4]: (~aElementOf0(W4,W1)|~sdtlpdtrp0(W0,W4)=W3))))))))&(![W2]: (W2=sdtlcdtrc0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK14_skl(W2,W1,W0),W2)|(![W4]: (~aElementOf0(W4,W1)|~sdtlpdtrp0(W0,W4)=sK14_skl(W2,W1,W0))))&(aElementOf0(sK14_skl(W2,W1,W0),W2)|(aElementOf0(sK15_skl(W2,W1,W0),W1)&sdtlpdtrp0(W0,sK15_skl(W2,W1,W0))=sK14_skl(W2,W1,W0)))))))))))),
% 64.87/8.69 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(W4,sK13_skl(W3,W2,W1,W0)),skolemize(W3,sK14_skl(W2,W1,W0)),skolemize(W4,sK15_skl(W2,W1,W0))],[f310])).
% 64.87/8.69 fof(f315,plain,(
% 64.87/8.69 ![X0,X1,X2,X3,X4]: (~aFunction0(X0)|~aSubsetOf0(X1,szDzozmdt0(X0))|~X2=sdtlcdtrc0(X0,X1)|aElementOf0(X3,X2)|~aElementOf0(X4,X1)|~sdtlpdtrp0(X0,X4)=X3)),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f311])).
% 64.87/8.69 fof(f339,plain,(
% 64.87/8.69 aSet0(xT)),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f73])).
% 64.87/8.69 fof(f342,plain,(
% 64.87/8.69 aSubsetOf0(xS,szNzAzT0)),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f75])).
% 64.87/8.69 fof(f343,plain,(
% 64.87/8.69 isCountable0(xS)),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f75])).
% 64.87/8.69 fof(f344,plain,(
% 64.87/8.69 aFunction0(xc)),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f76])).
% 64.87/8.69 fof(f345,plain,(
% 64.87/8.69 szDzozmdt0(xc)=slbdtsldtrb0(xS,xK)),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f76])).
% 64.87/8.69 fof(f346,plain,(
% 64.87/8.69 aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f76])).
% 64.87/8.69 fof(f353,plain,(
% 64.87/8.69 xK=sz00),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f78])).
% 64.87/8.69 fof(f354,plain,(
% 64.87/8.69 aElementOf0(slcrc0,slbdtsldtrb0(xS,sz00))),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f79])).
% 64.87/8.69 fof(f355,plain,(
% 64.87/8.69 ![W0]: (~aElementOf0(W0,slbdtsldtrb0(xS,sz00))|sdtlpdtrp0(xc,W0)=sdtlpdtrp0(xc,slcrc0))),
% 64.87/8.69 inference(pre_NNF_transformation,[status(thm)],[f80])).
% 64.87/8.69 fof(f356,plain,(
% 64.87/8.69 ![X0]: (~aElementOf0(X0,slbdtsldtrb0(xS,sz00))|sdtlpdtrp0(xc,X0)=sdtlpdtrp0(xc,slcrc0))),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f355])).
% 64.87/8.69 fof(f357,plain,(
% 64.87/8.69 (![W0]: (~aElementOf0(W0,xT)|(![W1]: ((~aSubsetOf0(W1,xS)|~isCountable0(W1))|(?[W2]: (aElementOf0(W2,slbdtsldtrb0(W1,xK))&~sdtlpdtrp0(xc,W2)=W0))))))),
% 64.87/8.69 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 64.87/8.69 fof(f358,plain,(
% 64.87/8.69 ![W0]: (~aElementOf0(W0,xT)|(![W1]: ((~aSubsetOf0(W1,xS)|~isCountable0(W1))|(aElementOf0(sK21_skl(W1,W0),slbdtsldtrb0(W1,xK))&~sdtlpdtrp0(xc,sK21_skl(W1,W0))=W0))))),
% 64.87/8.69 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(W2,sK21_skl(W1,W0))],[f357])).
% 64.87/8.69 fof(f359,plain,(
% 64.87/8.69 ![X0,X1]: (~aElementOf0(X0,xT)|~aSubsetOf0(X1,xS)|~isCountable0(X1)|aElementOf0(sK21_skl(X1,X0),slbdtsldtrb0(X1,xK)))),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f358])).
% 64.87/8.69 fof(f360,plain,(
% 64.87/8.69 ![X0,X1]: (~aElementOf0(X0,xT)|~aSubsetOf0(X1,xS)|~isCountable0(X1)|~sdtlpdtrp0(xc,sK21_skl(X1,X0))=X0)),
% 64.87/8.69 inference(cnf_transformation,[status(thm)],[f358])).
% 64.87/8.69 fof(f411,plain,(
% 64.87/8.69 ![X0,X1,X2]: (~aFunction0(X0)|~aSubsetOf0(X1,szDzozmdt0(X0))|aElementOf0(sdtlpdtrp0(X0,X2),sdtlcdtrc0(X0,X1))|~aElementOf0(X2,X1))),
% 64.87/8.69 inference(destructive_equality_resolution,[status(thm)],[f315])).
% 64.87/8.69 fof(f421,plain,(
% 64.87/8.69 szDzozmdt0(xc)=slbdtsldtrb0(xS,sz00)),
% 64.87/8.69 inference(backward_demodulation,[status(thm)],[f353,f345])).
% 64.87/8.69 fof(f423,plain,(
% 64.87/8.69 ![X0,X1]: (~aElementOf0(X0,xT)|~aSubsetOf0(X1,xS)|~isCountable0(X1)|aElementOf0(sK21_skl(X1,X0),slbdtsldtrb0(X1,sz00)))),
% 64.87/8.69 inference(forward_demodulation,[status(thm)],[f353,f359])).
% 64.87/8.69 fof(f425,plain,(
% 64.87/8.69 ![X0]: (~aElementOf0(X0,szDzozmdt0(xc))|sdtlpdtrp0(xc,X0)=sdtlpdtrp0(xc,slcrc0))),
% 64.87/8.69 inference(backward_demodulation,[status(thm)],[f421,f356])).
% 64.87/8.69 fof(f426,plain,(
% 64.87/8.69 aElementOf0(slcrc0,szDzozmdt0(xc))),
% 64.87/8.69 inference(backward_demodulation,[status(thm)],[f421,f354])).
% 64.87/8.69 fof(f432,plain,(
% 64.87/8.69 ~aSet0(szNzAzT0)|aSet0(xS)),
% 64.87/8.69 inference(resolution,[status(thm)],[f342,f111])).
% 64.87/8.69 fof(f434,plain,(
% 64.87/8.69 aSet0(xS)),
% 64.87/8.69 inference(forward_subsumption_resolution,[status(thm)],[f432,f159])).
% 64.87/8.69 fof(f436,plain,(
% 64.87/8.69 aSubsetOf0(xS,xS)),
% 64.87/8.69 inference(resolution,[status(thm)],[f118,f434])).
% 64.87/8.69 fof(f439,plain,(
% 64.87/8.69 ![X0]: (~aElementOf0(X0,xT)|~isCountable0(xS)|~sdtlpdtrp0(xc,sK21_skl(xS,X0))=X0)),
% 64.87/8.69 inference(resolution,[status(thm)],[f436,f360])).
% 64.87/8.69 fof(f442,plain,(
% 64.87/8.69 ![X0]: (~aElementOf0(X0,xT)|~sdtlpdtrp0(xc,sK21_skl(xS,X0))=X0)),
% 64.87/8.69 inference(forward_subsumption_resolution,[status(thm)],[f439,f343])).
% 64.87/8.69 fof(f453,plain,(
% 64.87/8.69 ![X0]: (~aElementOf0(X0,xT)|~aSubsetOf0(xS,xS)|~isCountable0(xS)|aElementOf0(sK21_skl(xS,X0),szDzozmdt0(xc)))),
% 64.87/8.69 inference(paramodulation,[status(thm)],[f421,f423])).
% 64.87/8.69 fof(f454,plain,(
% 64.87/8.69 ![X0]: (~aElementOf0(X0,xT)|~isCountable0(xS)|aElementOf0(sK21_skl(xS,X0),szDzozmdt0(xc)))),
% 64.87/8.69 inference(forward_subsumption_resolution,[status(thm)],[f453,f436])).
% 64.87/8.69 fof(f495,plain,(
% 64.87/8.69 ![X0]: (~aElementOf0(X0,xT)|aElementOf0(sK21_skl(xS,X0),szDzozmdt0(xc)))),
% 64.87/8.69 inference(resolution,[status(thm)],[f343,f454])).
% 64.87/8.69 fof(f498,plain,(
% 64.87/8.69 ![X0]: (~aElementOf0(X0,xT)|sdtlpdtrp0(xc,sK21_skl(xS,X0))=sdtlpdtrp0(xc,slcrc0))),
% 64.87/8.69 inference(resolution,[status(thm)],[f495,f425])).
% 64.87/8.69 fof(f616,plain,(
% 64.87/8.69 ![X0]: (~aSet0(xT)|~aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(X0,xT))),
% 64.87/8.69 inference(resolution,[status(thm)],[f346,f112])).
% 64.87/8.69 fof(f618,plain,(
% 64.87/8.69 ![X0]: (~aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc)))|aElementOf0(X0,xT))),
% 64.87/8.69 inference(forward_subsumption_resolution,[status(thm)],[f616,f339])).
% 64.87/8.69 fof(f628,plain,(
% 64.87/8.69 aSet0(szDzozmdt0(xc))),
% 64.87/8.69 inference(resolution,[status(thm)],[f292,f344])).
% 64.87/8.69 fof(f638,plain,(
% 64.87/8.69 aSubsetOf0(szDzozmdt0(xc),szDzozmdt0(xc))),
% 64.87/8.69 inference(resolution,[status(thm)],[f628,f118])).
% 64.87/8.69 fof(f4430,plain,(
% 64.87/8.69 ![X0,X1]: (~aSubsetOf0(X0,szDzozmdt0(xc))|aElementOf0(sdtlpdtrp0(xc,X1),sdtlcdtrc0(xc,X0))|~aElementOf0(X1,X0))),
% 64.87/8.69 inference(resolution,[status(thm)],[f411,f344])).
% 64.87/8.69 fof(f4469,plain,(
% 64.87/8.69 ![X0]: (~aSubsetOf0(szDzozmdt0(xc),szDzozmdt0(xc))|~aElementOf0(X0,szDzozmdt0(xc))|aElementOf0(sdtlpdtrp0(xc,X0),xT))),
% 64.87/8.69 inference(resolution,[status(thm)],[f4430,f618])).
% 64.87/8.69 fof(f4473,plain,(
% 64.87/8.69 ![X0]: (~aElementOf0(X0,szDzozmdt0(xc))|aElementOf0(sdtlpdtrp0(xc,X0),xT))),
% 64.87/8.69 inference(forward_subsumption_resolution,[status(thm)],[f4469,f638])).
% 64.87/8.69 fof(f4477,plain,(
% 64.87/8.69 aElementOf0(sdtlpdtrp0(xc,slcrc0),xT)),
% 64.87/8.69 inference(resolution,[status(thm)],[f4473,f426])).
% 64.87/8.69 fof(f4487,plain,(
% 64.87/8.69 sdtlpdtrp0(xc,sK21_skl(xS,sdtlpdtrp0(xc,slcrc0)))=sdtlpdtrp0(xc,slcrc0)),
% 64.87/8.69 inference(resolution,[status(thm)],[f4477,f498])).
% 64.87/8.69 fof(f4489,plain,(
% 64.87/8.69 ~sdtlpdtrp0(xc,sK21_skl(xS,sdtlpdtrp0(xc,slcrc0)))=sdtlpdtrp0(xc,slcrc0)),
% 61.61/8.75 inference(resolution,[status(thm)],[f4477,f442])).
% 61.61/8.75 fof(f4491,plain,(
% 61.61/8.75 ~sdtlpdtrp0(xc,slcrc0)=sdtlpdtrp0(xc,slcrc0)),
% 61.61/8.75 inference(forward_demodulation,[status(thm)],[f4487,f4489])).
% 61.61/8.75 fof(f4492,plain,(
% 61.61/8.75 $false),
% 61.61/8.75 inference(trivial_equality_resolution,[status(thm)],[f4491])).
% 61.61/8.75 % SZS output end CNFRefutation for theBenchmark.p
% 61.61/8.76 % Elapsed time: 8.384544 seconds
% 61.61/8.76 % CPU time: 66.010891 seconds
% 61.61/8.76 % Total memory used: 524.836 MB
% 61.61/8.76 % Net memory used: 497.765 MB
%------------------------------------------------------------------------------