%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM592+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 : n002.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:18 PM UTC 2026
% Result : Theorem 0.28s 0.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM592+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.44 % Computer : n002.cluster.edu
% 0.20/0.44 % Model : x86_64 x86_64
% 0.20/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.44 % Memory : 8046.5625MB
% 0.20/0.44 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Mon Sep 21 02:45:32 UTC 2026
% 0.20/0.45 % CPUTime :
% 0.20/0.48 % Drodi V4.1.1
% 0.28/0.95 % Refutation found
% 0.28/0.95 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.28/0.95 % SZS output start CNFRefutation for theBenchmark
% 0.28/0.95 fof(f5,definition,(
% 0.28/0.95 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 0.28/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.95 fof(f25,axiom,(
% 0.28/0.95 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aElementOf0(szszuzczcdt0(W0),szNzAzT0)& szszuzczcdt0(W0) != sz00 ) ) )),
% 0.28/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.95 fof(f64,axiom,(
% 0.28/0.95 (! [W0] :( aFunction0(W0)=> aSet0(szDzozmdt0(W0)) ) )),
% 0.28/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.95 fof(f74,hypothesis,(
% 0.28/0.95 aElementOf0(xK,szNzAzT0) ),
% 0.28/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.95 fof(f76,hypothesis,(
% 0.28/0.95 ( aFunction0(xc)& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ),
% 0.28/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.95 fof(f80,hypothesis,(
% 0.28/0.95 ( aElementOf0(xk,szNzAzT0)& szszuzczcdt0(xk) = xK ) ),
% 0.28/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.95 fof(f91,hypothesis,(
% 0.28/0.95 ( xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))& xd = sdtlpdtrp0(xC,xi) ) ),
% 0.28/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.95 fof(f92,hypothesis,(
% 0.28/0.95 ( aSubsetOf0(xY,szNzAzT0)& isCountable0(xY)& aFunction0(xd)& szDzozmdt0(xd) = slbdtsldtrb0(xY,xk)& aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT) ) ),
% 0.28/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.95 fof(f93,hypothesis,(
% 0.28/0.95 ( aElementOf0(xu,xT)& aSubsetOf0(xX,xY)& isCountable0(xX)& (! [W0] :( ( aSet0(W0)& aElementOf0(W0,slbdtsldtrb0(xX,xk)) )=> sdtlpdtrp0(xd,W0) = xu ) )) ),
% 0.28/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.95 fof(f94,conjecture,(
% 0.28/0.95 (? [W0] :( aElementOf0(W0,xT)& (? [W1] :( aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))& isCountable0(W1)& (! [W2] :( ( aSet0(W2)& aElementOf0(W2,slbdtsldtrb0(W1,xk)) )=> sdtlpdtrp0(sdtlpdtrp0(xC,xi),W2) = W0 ) )) )) )),
% 0.28/0.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.95 fof(f95,negated_conjecture,(
% 0.28/0.95 ~((? [W0] :( aElementOf0(W0,xT)& (? [W1] :( aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))& isCountable0(W1)& (! [W2] :( ( aSet0(W2)& aElementOf0(W2,slbdtsldtrb0(W1,xk)) )=> sdtlpdtrp0(sdtlpdtrp0(xC,xi),W2) = W0 ) )) )) ))),
% 0.28/0.95 inference(negated_conjecture,[status(cth)],[f94])).
% 0.28/0.95 fof(f106,plain,(
% 0.28/0.95 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 0.28/0.95 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.28/0.95 fof(f107,plain,(
% 0.28/0.95 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.28/0.95 inference(NNF_transformation,[status(thm)],[f106])).
% 0.28/0.95 fof(f108,plain,(
% 0.28/0.95 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.28/0.95 inference(miniscoping,[status(thm)],[f107])).
% 0.28/0.95 fof(f109,plain,(
% 0.28/0.95 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 0.28/0.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f108])).
% 0.28/0.95 fof(f111,plain,(
% 0.28/0.95 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f109])).
% 0.28/0.95 fof(f175,plain,(
% 0.28/0.95 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aElementOf0(szszuzczcdt0(W0),szNzAzT0)&~szszuzczcdt0(W0)=sz00))),
% 0.28/0.95 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.28/0.95 fof(f177,plain,(
% 0.28/0.95 ![X0]: (~aElementOf0(X0,szNzAzT0)|~szszuzczcdt0(X0)=sz00)),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f175])).
% 0.28/0.95 fof(f304,plain,(
% 0.28/0.95 ![W0]: (~aFunction0(W0)|aSet0(szDzozmdt0(W0)))),
% 0.28/0.95 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.28/0.95 fof(f305,plain,(
% 0.28/0.95 ![X0]: (~aFunction0(X0)|aSet0(szDzozmdt0(X0)))),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f304])).
% 0.28/0.95 fof(f354,plain,(
% 0.28/0.95 aElementOf0(xK,szNzAzT0)),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f74])).
% 0.28/0.95 fof(f357,plain,(
% 0.28/0.95 aFunction0(xc)),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f76])).
% 0.28/0.95 fof(f369,plain,(
% 0.28/0.95 szszuzczcdt0(xk)=xK),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f80])).
% 0.28/0.95 fof(f397,plain,(
% 0.28/0.95 xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f91])).
% 0.28/0.95 fof(f398,plain,(
% 0.28/0.95 xd=sdtlpdtrp0(xC,xi)),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f91])).
% 0.28/0.95 fof(f401,plain,(
% 0.28/0.95 aFunction0(xd)),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f92])).
% 0.28/0.95 fof(f404,plain,(
% 0.28/0.95 ((aElementOf0(xu,xT)&aSubsetOf0(xX,xY))&isCountable0(xX))&(![W0]: ((~aSet0(W0)|~aElementOf0(W0,slbdtsldtrb0(xX,xk)))|sdtlpdtrp0(xd,W0)=xu))),
% 0.28/0.95 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 0.28/0.95 fof(f405,plain,(
% 0.28/0.95 aElementOf0(xu,xT)),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f404])).
% 0.28/0.95 fof(f406,plain,(
% 0.28/0.95 aSubsetOf0(xX,xY)),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f404])).
% 0.28/0.95 fof(f407,plain,(
% 0.28/0.95 isCountable0(xX)),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f404])).
% 0.28/0.95 fof(f408,plain,(
% 0.28/0.95 ![X0]: (~aSet0(X0)|~aElementOf0(X0,slbdtsldtrb0(xX,xk))|sdtlpdtrp0(xd,X0)=xu)),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f404])).
% 0.28/0.95 fof(f409,plain,(
% 0.28/0.95 (![W0]: (~aElementOf0(W0,xT)|(![W1]: ((~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~isCountable0(W1))|(?[W2]: ((aSet0(W2)&aElementOf0(W2,slbdtsldtrb0(W1,xk)))&~sdtlpdtrp0(sdtlpdtrp0(xC,xi),W2)=W0))))))),
% 0.28/0.95 inference(pre_NNF_transformation,[status(thm)],[f95])).
% 0.28/0.95 fof(f410,plain,(
% 0.28/0.95 ![W0]: (~aElementOf0(W0,xT)|(![W1]: ((~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~isCountable0(W1))|((aSet0(sK21_skl(W1,W0))&aElementOf0(sK21_skl(W1,W0),slbdtsldtrb0(W1,xk)))&~sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK21_skl(W1,W0))=W0))))),
% 0.28/0.95 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(W2,sK21_skl(W1,W0))],[f409])).
% 0.28/0.95 fof(f411,plain,(
% 0.28/0.95 ![X0,X1]: (~aElementOf0(X0,xT)|~aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~isCountable0(X1)|aSet0(sK21_skl(X1,X0)))),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f410])).
% 0.28/0.95 fof(f412,plain,(
% 0.28/0.95 ![X0,X1]: (~aElementOf0(X0,xT)|~aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~isCountable0(X1)|aElementOf0(sK21_skl(X1,X0),slbdtsldtrb0(X1,xk)))),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f410])).
% 0.28/0.95 fof(f413,plain,(
% 0.28/0.95 ![X0,X1]: (~aElementOf0(X0,xT)|~aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~isCountable0(X1)|~sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK21_skl(X1,X0))=X0)),
% 0.28/0.95 inference(cnf_transformation,[status(thm)],[f410])).
% 0.28/0.95 fof(f421,plain,(
% 0.28/0.95 ![X0]: (~aElementOf0(X0,slcrc0))),
% 0.28/0.95 inference(destructive_equality_resolution,[status(thm)],[f111])).
% 0.28/0.95 fof(f789,definition,(
% 0.28/0.95 sQ40_spl <=> (aElementOf0(sK1_skl(slcrc0,slcrc0),slcrc0))),
% 0.28/0.95 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.28/0.95 fof(f790,plain,(
% 0.28/0.95 aElementOf0(sK1_skl(slcrc0,slcrc0),slcrc0)|~sQ40_spl),
% 0.28/0.95 inference(component_clause,[status(thm)],[f789])).
% 0.28/0.95 fof(f869,plain,(
% 0.28/0.95 ~szszuzczcdt0(xK)=sz00),
% 0.28/0.95 inference(resolution,[status(thm)],[f177,f354])).
% 0.28/0.95 fof(f1698,plain,(
% 0.28/0.95 ![X0]: (~aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~isCountable0(X0)|aElementOf0(sK21_skl(X0,xu),slbdtsldtrb0(X0,xk)))),
% 0.28/0.95 inference(resolution,[status(thm)],[f412,f405])).
% 0.28/0.95 fof(f1699,plain,(
% 0.28/0.95 ![X0]: (~aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~isCountable0(X0)|~sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK21_skl(X0,xu))=xu)),
% 0.28/0.95 inference(resolution,[status(thm)],[f413,f405])).
% 0.28/0.95 fof(f1760,plain,(
% 0.28/0.95 ![X0]: (~aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~isCountable0(X0)|aSet0(sK21_skl(X0,xu)))),
% 0.28/0.95 inference(resolution,[status(thm)],[f411,f405])).
% 0.28/0.95 fof(f2783,plain,(
% 0.28/0.95 aSet0(szDzozmdt0(xd))),
% 0.28/0.95 inference(resolution,[status(thm)],[f305,f401])).
% 0.28/0.95 fof(f2785,plain,(
% 0.28/0.95 aSet0(szDzozmdt0(xc))),
% 0.28/0.95 inference(resolution,[status(thm)],[f305,f357])).
% 0.28/0.95 fof(f4344,definition,(
% 0.28/0.95 sQ525_spl <=> (aSet0(szDzozmdt0(xd)))),
% 0.28/0.95 introduced(definition,[new_symbols(definition,[sQ525_spl])],[split_symbol_definition])).
% 0.28/0.95 fof(f4346,plain,(
% 0.28/0.95 ~aSet0(szDzozmdt0(xd))|sQ525_spl),
% 0.28/0.95 inference(component_clause,[status(thm)],[f4344])).
% 0.28/0.95 fof(f4697,definition,(
% 0.28/0.95 sQ599_spl <=> (aSet0(szDzozmdt0(xc)))),
% 0.28/0.95 introduced(definition,[new_symbols(definition,[sQ599_spl])],[split_symbol_definition])).
% 0.28/0.95 fof(f4699,plain,(
% 0.28/0.95 ~aSet0(szDzozmdt0(xc))|sQ599_spl),
% 0.28/0.95 inference(component_clause,[status(thm)],[f4697])).
% 0.28/0.95 fof(f5016,plain,(
% 0.28/0.95 ![X0]: (~aSubsetOf0(X0,xY)|~isCountable0(X0)|~sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK21_skl(X0,xu))=xu)),
% 0.28/0.95 inference(backward_demodulation,[status(thm)],[f397,f1699])).
% 0.28/0.95 fof(f5017,plain,(
% 0.28/0.95 ![X0]: (~aSubsetOf0(X0,xY)|~isCountable0(X0)|aElementOf0(sK21_skl(X0,xu),slbdtsldtrb0(X0,xk)))),
% 0.28/0.95 inference(backward_demodulation,[status(thm)],[f397,f1698])).
% 0.28/0.95 fof(f5019,plain,(
% 0.28/0.95 ![X0]: (~aSubsetOf0(X0,xY)|~isCountable0(X0)|aSet0(sK21_skl(X0,xu)))),
% 0.28/0.95 inference(backward_demodulation,[status(thm)],[f397,f1760])).
% 0.28/0.95 fof(f5061,plain,(
% 0.28/0.95 ~isCountable0(xX)|aSet0(sK21_skl(xX,xu))),
% 0.28/0.95 inference(resolution,[status(thm)],[f5019,f406])).
% 0.28/0.95 fof(f5063,definition,(
% 0.28/0.95 sQ661_spl <=> (isCountable0(xX))),
% 0.28/0.95 introduced(definition,[new_symbols(definition,[sQ661_spl])],[split_symbol_definition])).
% 0.28/0.95 fof(f5065,plain,(
% 0.28/0.95 ~isCountable0(xX)|sQ661_spl),
% 0.28/0.95 inference(component_clause,[status(thm)],[f5063])).
% 0.28/0.95 fof(f5066,definition,(
% 0.28/0.95 sQ662_spl <=> (aSet0(sK21_skl(xX,xu)))),
% 0.28/0.95 introduced(definition,[new_symbols(definition,[sQ662_spl])],[split_symbol_definition])).
% 0.28/0.95 fof(f5069,plain,(
% 0.28/0.95 ~sQ661_spl|sQ662_spl),
% 0.28/0.95 inference(split_clause,[status(thm)],[f5061,f5063,f5066])).
% 0.28/0.95 fof(f5074,plain,(
% 0.28/0.95 $false|sQ661_spl),
% 0.28/0.95 inference(forward_subsumption_resolution,[status(thm)],[f5065,f407])).
% 0.28/0.95 fof(f5075,plain,(
% 0.28/0.95 sQ661_spl),
% 0.28/0.95 inference(contradiction_clause,[status(thm)],[f5074])).
% 0.28/0.95 fof(f5327,plain,(
% 0.28/0.95 $false|sQ525_spl),
% 0.28/0.95 inference(forward_subsumption_resolution,[status(thm)],[f4346,f2783])).
% 0.28/0.95 fof(f5328,plain,(
% 0.28/0.95 sQ525_spl),
% 0.28/0.95 inference(contradiction_clause,[status(thm)],[f5327])).
% 0.28/0.95 fof(f5410,plain,(
% 0.28/0.95 ![X0]: (~aSubsetOf0(X0,xY)|~isCountable0(X0)|~sdtlpdtrp0(xd,sK21_skl(X0,xu))=xu)),
% 0.28/0.95 inference(forward_demodulation,[status(thm)],[f398,f5016])).
% 0.28/0.95 fof(f5411,plain,(
% 0.28/0.95 ~isCountable0(xX)|~sdtlpdtrp0(xd,sK21_skl(xX,xu))=xu),
% 0.28/0.95 inference(resolution,[status(thm)],[f5410,f406])).
% 0.28/0.95 fof(f5413,definition,(
% 0.28/0.95 sQ702_spl <=> (sdtlpdtrp0(xd,sK21_skl(xX,xu))=xu)),
% 0.28/0.95 introduced(definition,[new_symbols(definition,[sQ702_spl])],[split_symbol_definition])).
% 0.28/0.95 fof(f5416,plain,(
% 0.28/0.95 ~sQ661_spl|~sQ702_spl),
% 0.28/0.95 inference(split_clause,[status(thm)],[f5411,f5063,f5413])).
% 0.28/0.95 fof(f5516,plain,(
% 0.28/0.95 $false|sQ599_spl),
% 0.28/0.95 inference(forward_subsumption_resolution,[status(thm)],[f4699,f2785])).
% 0.28/0.95 fof(f5517,plain,(
% 0.28/0.95 sQ599_spl),
% 0.28/0.95 inference(contradiction_clause,[status(thm)],[f5516])).
% 0.28/0.95 fof(f5556,plain,(
% 0.28/0.95 ~isCountable0(xX)|aElementOf0(sK21_skl(xX,xu),slbdtsldtrb0(xX,xk))),
% 0.28/0.95 inference(resolution,[status(thm)],[f5017,f406])).
% 0.28/0.95 fof(f5558,definition,(
% 0.28/0.95 sQ709_spl <=> (aElementOf0(sK21_skl(xX,xu),slbdtsldtrb0(xX,xk)))),
% 0.28/0.95 introduced(definition,[new_symbols(definition,[sQ709_spl])],[split_symbol_definition])).
% 0.28/0.95 fof(f5559,plain,(
% 0.28/0.95 aElementOf0(sK21_skl(xX,xu),slbdtsldtrb0(xX,xk))|~sQ709_spl),
% 0.28/0.95 inference(component_clause,[status(thm)],[f5558])).
% 0.28/0.95 fof(f5561,plain,(
% 0.28/0.95 ~sQ661_spl|sQ709_spl),
% 0.28/0.95 inference(split_clause,[status(thm)],[f5556,f5063,f5558])).
% 0.28/0.95 fof(f5752,plain,(
% 0.28/0.95 $false|~sQ40_spl),
% 0.28/0.95 inference(forward_subsumption_resolution,[status(thm)],[f790,f421])).
% 0.28/0.95 fof(f5753,plain,(
% 0.28/0.95 ~sQ40_spl),
% 0.28/0.95 inference(contradiction_clause,[status(thm)],[f5752])).
% 0.28/0.95 fof(f5819,definition,(
% 0.28/0.95 sQ738_spl <=> (szszuzczcdt0(xi)=szszuzczcdt0(xi))),
% 0.28/0.95 introduced(definition,[new_symbols(definition,[sQ738_spl])],[split_symbol_definition])).
% 0.28/0.95 fof(f5821,plain,(
% 0.28/0.95 ~szszuzczcdt0(xi)=szszuzczcdt0(xi)|sQ738_spl),
% 0.28/0.95 inference(component_clause,[status(thm)],[f5819])).
% 0.28/0.95 fof(f5832,plain,(
% 0.28/0.95 $false|sQ738_spl),
% 0.28/0.95 inference(trivial_equality_resolution,[status(thm)],[f5821])).
% 0.28/0.95 fof(f5833,plain,(
% 0.28/0.95 sQ738_spl),
% 0.28/0.95 inference(contradiction_clause,[status(thm)],[f5832])).
% 0.28/0.95 fof(f6079,definition,(
% 0.28/0.95 sQ754_spl <=> (xK=szszuzczcdt0(xk))),
% 0.28/0.95 introduced(definition,[new_symbols(definition,[sQ754_spl])],[split_symbol_definition])).
% 0.28/0.95 fof(f6081,plain,(
% 0.28/0.95 ~xK=szszuzczcdt0(xk)|sQ754_spl),
% 0.28/0.95 inference(component_clause,[status(thm)],[f6079])).
% 0.28/0.95 fof(f6088,plain,(
% 0.28/0.95 ~xK=xK|sQ754_spl),
% 0.28/0.96 inference(forward_demodulation,[status(thm)],[f369,f6081])).
% 0.28/0.96 fof(f6089,plain,(
% 0.28/0.96 $false|sQ754_spl),
% 0.28/0.96 inference(trivial_equality_resolution,[status(thm)],[f6088])).
% 0.28/0.96 fof(f6090,plain,(
% 0.28/0.96 sQ754_spl),
% 0.28/0.96 inference(contradiction_clause,[status(thm)],[f6089])).
% 0.28/0.96 fof(f6277,definition,(
% 0.28/0.96 sQ775_spl <=> (szszuzczcdt0(xK)=sz00)),
% 0.28/0.96 introduced(definition,[new_symbols(definition,[sQ775_spl])],[split_symbol_definition])).
% 0.28/0.96 fof(f6278,plain,(
% 0.28/0.96 szszuzczcdt0(xK)=sz00|~sQ775_spl),
% 0.28/0.96 inference(component_clause,[status(thm)],[f6277])).
% 0.28/0.96 fof(f6304,plain,(
% 0.28/0.96 $false|~sQ775_spl),
% 0.28/0.96 inference(forward_subsumption_resolution,[status(thm)],[f6278,f869])).
% 0.28/0.96 fof(f6305,plain,(
% 0.28/0.96 ~sQ775_spl),
% 0.28/0.96 inference(contradiction_clause,[status(thm)],[f6304])).
% 0.28/0.96 fof(f6505,definition,(
% 0.28/0.96 sQ797_spl <=> (szszuzczcdt0(xK)=szszuzczcdt0(xK))),
% 0.28/0.96 introduced(definition,[new_symbols(definition,[sQ797_spl])],[split_symbol_definition])).
% 0.28/0.96 fof(f6507,plain,(
% 0.28/0.96 ~szszuzczcdt0(xK)=szszuzczcdt0(xK)|sQ797_spl),
% 0.28/0.96 inference(component_clause,[status(thm)],[f6505])).
% 0.28/0.96 fof(f6514,plain,(
% 0.28/0.96 $false|sQ797_spl),
% 0.28/0.96 inference(trivial_equality_resolution,[status(thm)],[f6507])).
% 0.28/0.96 fof(f6515,plain,(
% 0.28/0.96 sQ797_spl),
% 0.28/0.96 inference(contradiction_clause,[status(thm)],[f6514])).
% 0.28/0.96 fof(f6534,definition,(
% 0.28/0.96 sQ802_spl <=> (szszuzczcdt0(sz00)=szszuzczcdt0(sz00))),
% 0.28/0.96 introduced(definition,[new_symbols(definition,[sQ802_spl])],[split_symbol_definition])).
% 0.28/0.96 fof(f6536,plain,(
% 0.28/0.96 ~szszuzczcdt0(sz00)=szszuzczcdt0(sz00)|sQ802_spl),
% 0.28/0.96 inference(component_clause,[status(thm)],[f6534])).
% 0.28/0.96 fof(f6538,plain,(
% 0.28/0.96 $false|sQ802_spl),
% 0.28/0.96 inference(trivial_equality_resolution,[status(thm)],[f6536])).
% 0.28/0.96 fof(f6539,plain,(
% 0.28/0.96 sQ802_spl),
% 0.28/0.96 inference(contradiction_clause,[status(thm)],[f6538])).
% 0.28/0.96 fof(f8073,plain,(
% 0.28/0.96 ~aSet0(sK21_skl(xX,xu))|sdtlpdtrp0(xd,sK21_skl(xX,xu))=xu|~sQ709_spl),
% 0.28/0.96 inference(resolution,[status(thm)],[f5559,f408])).
% 0.28/0.96 fof(f8080,plain,(
% 0.28/0.96 ~sQ662_spl|sQ702_spl|~sQ709_spl),
% 0.28/0.96 inference(split_clause,[status(thm)],[f8073,f5066,f5413,f5558])).
% 0.28/0.96 fof(f8105,plain,(
% 0.28/0.96 $false),
% 0.28/0.96 inference(sat_refutation,[status(thm)],[f5069,f5075,f5328,f5416,f5517,f5561,f5753,f5833,f6090,f6305,f6515,f6539,f8080])).
% 0.28/0.96 % SZS output end CNFRefutation for theBenchmark.p
% 0.99/1.01 % Elapsed time: 0.538015 seconds
% 0.99/1.01 % CPU time: 3.620931 seconds
% 0.99/1.01 % Total memory used: 149.908 MB
% 0.99/1.01 % Net memory used: 147.507 MB
%------------------------------------------------------------------------------