%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM545+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 : n018.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:10 PM UTC 2026
% Result : Theorem 0.17s 5.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM545+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.12/5.39 % Computer : n018.cluster.edu
% 0.12/5.39 % Model : x86_64 x86_64
% 0.12/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.39 % Memory : 8046.5625MB
% 0.12/5.39 % OS : Linux 6.8.0-71-generic
% 0.12/5.39 % CPULimit : 300
% 0.12/5.39 % WCLimit : 300
% 0.12/5.39 % DateTime : Mon Sep 21 02:41:04 UTC 2026
% 0.12/5.40 % CPUTime :
% 0.17/5.42 % Drodi V4.1.1
% 0.17/5.71 % Refutation found
% 0.17/5.71 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/5.71 % SZS output start CNFRefutation for theBenchmark
% 0.17/5.71 fof(f5,definition,(
% 0.17/5.71 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 0.17/5.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.71 fof(f10,definition,(
% 0.17/5.71 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 0.17/5.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.71 fof(f12,axiom,(
% 0.17/5.71 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 0.17/5.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.71 fof(f23,axiom,(
% 0.17/5.71 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 0.17/5.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.71 fof(f24,axiom,(
% 0.17/5.71 aElementOf0(sz00,szNzAzT0) ),
% 0.17/5.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.71 fof(f25,axiom,(
% 0.17/5.71 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aElementOf0(szszuzczcdt0(W0),szNzAzT0)& szszuzczcdt0(W0) != sz00 ) ) )),
% 0.17/5.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.71 fof(f48,definition,(
% 0.17/5.71 (! [W0] :( ( aSubsetOf0(W0,szNzAzT0)& isFinite0(W0)& W0 != slcrc0 )=> (! [W1] :( W1 = szmzazxdt0(W0)<=> ( aElementOf0(W1,W0)& (! [W2] :( aElementOf0(W2,W0)=> sdtlseqdt0(W2,W1) ) )) ) )) )),
% 0.17/5.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.71 fof(f52,axiom,(
% 0.17/5.71 slbdtrb0(sz00) = slcrc0 ),
% 0.17/5.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.71 fof(f53,axiom,(
% 0.17/5.71 (! [W0,W1] :( ( aElementOf0(W0,szNzAzT0)& aElementOf0(W1,szNzAzT0) )=> ( aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1)))<=> ( aElementOf0(W0,slbdtrb0(W1))| W0 = W1 ) ) ) )),
% 0.17/5.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.71 fof(f55,hypothesis,(
% 0.17/5.71 ( aSubsetOf0(xS,szNzAzT0)& isFinite0(xS) ) ),
% 0.17/5.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.71 fof(f56,hypothesis,(
% 0.17/5.71 ( xS != slcrc0=> aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ) ),
% 0.17/5.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.71 fof(f57,conjecture,(
% 0.17/5.71 (? [W0] :( aElementOf0(W0,szNzAzT0)& aSubsetOf0(xS,slbdtrb0(W0)) ) )),
% 0.17/5.71 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/5.71 fof(f58,negated_conjecture,(
% 0.17/5.71 ~((? [W0] :( aElementOf0(W0,szNzAzT0)& aSubsetOf0(xS,slbdtrb0(W0)) ) ))),
% 0.17/5.71 inference(negated_conjecture,[status(cth)],[f57])).
% 0.17/5.71 fof(f69,plain,(
% 0.17/5.71 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 0.17/5.71 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.17/5.71 fof(f70,plain,(
% 0.17/5.71 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.17/5.71 inference(NNF_transformation,[status(thm)],[f69])).
% 0.17/5.71 fof(f71,plain,(
% 0.17/5.71 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.17/5.71 inference(miniscoping,[status(thm)],[f70])).
% 0.17/5.71 fof(f72,plain,(
% 0.17/5.71 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 0.17/5.71 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f71])).
% 0.17/5.71 fof(f73,plain,(
% 0.17/5.71 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f72])).
% 0.17/5.71 fof(f74,plain,(
% 0.17/5.71 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f72])).
% 0.17/5.71 fof(f83,plain,(
% 0.17/5.71 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 0.17/5.71 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.17/5.71 fof(f84,plain,(
% 0.17/5.71 ![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.17/5.71 inference(NNF_transformation,[status(thm)],[f83])).
% 0.17/5.71 fof(f85,plain,(
% 0.17/5.71 ![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.17/5.71 inference(miniscoping,[status(thm)],[f84])).
% 0.17/5.71 fof(f86,plain,(
% 0.17/5.71 ![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.17/5.71 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f85])).
% 0.17/5.71 fof(f88,plain,(
% 0.17/5.71 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f86])).
% 0.17/5.71 fof(f93,plain,(
% 0.17/5.71 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 0.17/5.71 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.17/5.71 fof(f94,plain,(
% 0.17/5.71 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f93])).
% 0.17/5.71 fof(f135,plain,(
% 0.17/5.71 aSet0(szNzAzT0)),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f23])).
% 0.17/5.71 fof(f137,plain,(
% 0.17/5.71 aElementOf0(sz00,szNzAzT0)),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f24])).
% 0.17/5.71 fof(f138,plain,(
% 0.17/5.71 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aElementOf0(szszuzczcdt0(W0),szNzAzT0)&~szszuzczcdt0(W0)=sz00))),
% 0.17/5.71 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.17/5.71 fof(f139,plain,(
% 0.17/5.71 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(szszuzczcdt0(X0),szNzAzT0))),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f138])).
% 0.17/5.71 fof(f140,plain,(
% 0.17/5.71 ![X0]: (~aElementOf0(X0,szNzAzT0)|~szszuzczcdt0(X0)=sz00)),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f138])).
% 0.17/5.71 fof(f201,plain,(
% 0.17/5.71 ![W0]: (((~aSubsetOf0(W0,szNzAzT0)|~isFinite0(W0))|W0=slcrc0)|(![W1]: (W1=szmzazxdt0(W0)<=>(aElementOf0(W1,W0)&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W2,W1)))))))),
% 0.17/5.71 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 0.17/5.71 fof(f202,plain,(
% 0.17/5.71 ![W0]: (((~aSubsetOf0(W0,szNzAzT0)|~isFinite0(W0))|W0=slcrc0)|(![W1]: ((~W1=szmzazxdt0(W0)|(aElementOf0(W1,W0)&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W2,W1)))))&(W1=szmzazxdt0(W0)|(~aElementOf0(W1,W0)|(?[W2]: (aElementOf0(W2,W0)&~sdtlseqdt0(W2,W1))))))))),
% 0.17/5.71 inference(NNF_transformation,[status(thm)],[f201])).
% 0.17/5.71 fof(f203,plain,(
% 0.17/5.71 ![W0]: (((~aSubsetOf0(W0,szNzAzT0)|~isFinite0(W0))|W0=slcrc0)|((![W1]: (~W1=szmzazxdt0(W0)|(aElementOf0(W1,W0)&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W2,W1))))))&(![W1]: (W1=szmzazxdt0(W0)|(~aElementOf0(W1,W0)|(?[W2]: (aElementOf0(W2,W0)&~sdtlseqdt0(W2,W1))))))))),
% 0.17/5.71 inference(miniscoping,[status(thm)],[f202])).
% 0.17/5.71 fof(f204,plain,(
% 0.17/5.71 ![W0]: (((~aSubsetOf0(W0,szNzAzT0)|~isFinite0(W0))|W0=slcrc0)|((![W1]: (~W1=szmzazxdt0(W0)|(aElementOf0(W1,W0)&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W2,W1))))))&(![W1]: (W1=szmzazxdt0(W0)|(~aElementOf0(W1,W0)|(aElementOf0(sK7_skl(W1,W0),W0)&~sdtlseqdt0(sK7_skl(W1,W0),W1)))))))),
% 0.17/5.71 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(W2,sK7_skl(W1,W0))],[f203])).
% 0.17/5.71 fof(f205,plain,(
% 0.17/5.71 ![X0,X1]: (~aSubsetOf0(X0,szNzAzT0)|~isFinite0(X0)|X0=slcrc0|~X1=szmzazxdt0(X0)|aElementOf0(X1,X0))),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f204])).
% 0.17/5.71 fof(f224,plain,(
% 0.17/5.71 slbdtrb0(sz00)=slcrc0),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f52])).
% 0.17/5.71 fof(f225,plain,(
% 0.17/5.71 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|(aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1)))<=>(aElementOf0(W0,slbdtrb0(W1))|W0=W1)))),
% 0.17/5.71 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.17/5.71 fof(f226,plain,(
% 0.17/5.71 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|((~aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1)))|(aElementOf0(W0,slbdtrb0(W1))|W0=W1))&(aElementOf0(W0,slbdtrb0(szszuzczcdt0(W1)))|(~aElementOf0(W0,slbdtrb0(W1))&~W0=W1))))),
% 0.17/5.71 inference(NNF_transformation,[status(thm)],[f225])).
% 0.17/5.71 fof(f229,plain,(
% 0.17/5.71 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|aElementOf0(X0,slbdtrb0(szszuzczcdt0(X1)))|~X0=X1)),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f226])).
% 0.17/5.71 fof(f234,plain,(
% 0.17/5.71 aSubsetOf0(xS,szNzAzT0)),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f55])).
% 0.17/5.71 fof(f235,plain,(
% 0.17/5.71 isFinite0(xS)),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f55])).
% 0.17/5.71 fof(f236,plain,(
% 0.17/5.71 xS=slcrc0|aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))),
% 0.17/5.71 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 0.17/5.71 fof(f237,plain,(
% 0.17/5.71 xS=slcrc0|aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f236])).
% 0.17/5.71 fof(f238,plain,(
% 0.17/5.71 (![W0]: (~aElementOf0(W0,szNzAzT0)|~aSubsetOf0(xS,slbdtrb0(W0))))),
% 0.17/5.71 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 0.17/5.71 fof(f239,plain,(
% 0.17/5.71 ![X0]: (~aElementOf0(X0,szNzAzT0)|~aSubsetOf0(xS,slbdtrb0(X0)))),
% 0.17/5.71 inference(cnf_transformation,[status(thm)],[f238])).
% 0.17/5.71 fof(f246,definition,(
% 0.17/5.71 sQ0_spl <=> (xS=slcrc0)),
% 0.17/5.71 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.17/5.71 fof(f247,plain,(
% 0.17/5.71 xS=slcrc0|~sQ0_spl),
% 0.17/5.71 inference(component_clause,[status(thm)],[f246])).
% 0.17/5.71 fof(f249,definition,(
% 0.17/5.71 sQ1_spl <=> (aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),
% 0.17/5.71 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.17/5.71 fof(f250,plain,(
% 0.17/5.71 aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|~sQ1_spl),
% 0.17/5.71 inference(component_clause,[status(thm)],[f249])).
% 0.17/5.71 fof(f252,plain,(
% 0.17/5.71 sQ0_spl|sQ1_spl),
% 0.17/5.71 inference(split_clause,[status(thm)],[f237,f246,f249])).
% 0.17/5.71 fof(f253,plain,(
% 0.17/5.71 aSet0(slcrc0)),
% 0.17/5.71 inference(destructive_equality_resolution,[status(thm)],[f73])).
% 0.17/5.71 fof(f254,plain,(
% 0.17/5.71 ![X0]: (~aElementOf0(X0,slcrc0))),
% 0.17/5.71 inference(destructive_equality_resolution,[status(thm)],[f74])).
% 0.17/5.71 fof(f268,plain,(
% 0.17/5.71 ![X0]: (~aSubsetOf0(X0,szNzAzT0)|~isFinite0(X0)|X0=slcrc0|aElementOf0(szmzazxdt0(X0),X0))),
% 0.17/5.71 inference(destructive_equality_resolution,[status(thm)],[f205])).
% 0.17/5.71 fof(f274,plain,(
% 0.17/5.71 ![X1]: (~aElementOf0(X1,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|aElementOf0(X1,slbdtrb0(szszuzczcdt0(X1))))),
% 0.17/5.71 inference(destructive_equality_resolution,[status(thm)],[f229])).
% 0.17/5.71 fof(f275,plain,(
% 0.17/5.71 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(X0,slbdtrb0(szszuzczcdt0(X0))))),
% 0.17/5.71 inference(duplicate_literals_removal,[status(thm)],[f274])).
% 0.17/5.71 fof(f278,definition,(
% 0.17/5.71 sQ2_spl <=> (aSet0(szNzAzT0))),
% 0.17/5.71 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.17/5.71 fof(f280,plain,(
% 0.17/5.71 ~aSet0(szNzAzT0)|sQ2_spl),
% 0.17/5.71 inference(component_clause,[status(thm)],[f278])).
% 0.17/5.71 fof(f285,plain,(
% 0.17/5.71 ![X0]: (~aSet0(szNzAzT0)|~aElementOf0(X0,xS)|aElementOf0(X0,szNzAzT0))),
% 0.17/5.71 inference(resolution,[status(thm)],[f88,f234])).
% 0.17/5.71 fof(f286,definition,(
% 0.17/5.71 ![X0]: (sQ4_spl <=> (~aElementOf0(X0,xS)|aElementOf0(X0,szNzAzT0)))),
% 0.17/5.71 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.17/5.71 fof(f287,plain,(
% 0.17/5.71 ![X0]: (~aElementOf0(X0,xS)|aElementOf0(X0,szNzAzT0)|~sQ4_spl)),
% 0.17/5.71 inference(component_clause,[status(thm)],[f286])).
% 0.17/5.71 fof(f289,plain,(
% 0.17/5.71 ~sQ2_spl|sQ4_spl),
% 0.17/5.71 inference(split_clause,[status(thm)],[f285,f278,f286])).
% 0.17/5.71 fof(f290,plain,(
% 0.17/5.71 aSubsetOf0(slcrc0,slcrc0)),
% 0.17/5.71 inference(resolution,[status(thm)],[f253,f94])).
% 0.17/5.71 fof(f308,plain,(
% 0.17/5.71 $false|sQ2_spl),
% 0.17/5.71 inference(forward_subsumption_resolution,[status(thm)],[f280,f135])).
% 0.17/5.71 fof(f309,plain,(
% 0.17/5.71 sQ2_spl),
% 0.17/5.71 inference(contradiction_clause,[status(thm)],[f308])).
% 0.17/5.71 fof(f405,definition,(
% 0.17/5.71 sQ19_spl <=> (isFinite0(xS))),
% 0.17/5.71 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.17/5.71 fof(f407,plain,(
% 0.17/5.71 ~isFinite0(xS)|sQ19_spl),
% 0.17/5.71 inference(component_clause,[status(thm)],[f405])).
% 0.17/5.71 fof(f451,plain,(
% 0.17/5.71 aElementOf0(sz00,slbdtrb0(szszuzczcdt0(sz00)))),
% 0.17/5.71 inference(resolution,[status(thm)],[f137,f275])).
% 0.17/5.71 fof(f479,plain,(
% 0.17/5.71 ~aElementOf0(sz00,szNzAzT0)|~aSubsetOf0(xS,slcrc0)),
% 0.17/5.71 inference(paramodulation,[status(thm)],[f224,f239])).
% 0.17/5.71 fof(f480,definition,(
% 0.17/5.71 sQ29_spl <=> (aElementOf0(sz00,szNzAzT0))),
% 0.17/5.71 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.17/5.71 fof(f482,plain,(
% 0.17/5.71 ~aElementOf0(sz00,szNzAzT0)|sQ29_spl),
% 0.17/5.71 inference(component_clause,[status(thm)],[f480])).
% 0.17/5.71 fof(f495,definition,(
% 0.17/5.71 sQ33_spl <=> (aSubsetOf0(xS,slcrc0))),
% 0.17/5.71 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.17/5.71 fof(f497,plain,(
% 0.17/5.71 ~aSubsetOf0(xS,slcrc0)|sQ33_spl),
% 0.17/5.71 inference(component_clause,[status(thm)],[f495])).
% 0.17/5.71 fof(f498,plain,(
% 0.17/5.71 ~sQ29_spl|~sQ33_spl),
% 0.17/5.71 inference(split_clause,[status(thm)],[f479,f480,f495])).
% 0.17/5.71 fof(f499,plain,(
% 0.17/5.71 $false|sQ29_spl),
% 0.17/5.71 inference(forward_subsumption_resolution,[status(thm)],[f482,f137])).
% 0.17/5.71 fof(f500,plain,(
% 0.17/5.71 sQ29_spl),
% 0.17/5.71 inference(contradiction_clause,[status(thm)],[f499])).
% 0.17/5.71 fof(f546,plain,(
% 0.17/5.71 ~aSubsetOf0(slcrc0,slcrc0)|~sQ0_spl|sQ33_spl),
% 0.17/5.71 inference(backward_demodulation,[status(thm)],[f247,f497])).
% 0.17/5.71 fof(f553,plain,(
% 0.17/5.71 $false|~sQ0_spl|sQ33_spl),
% 0.17/5.71 inference(forward_subsumption_resolution,[status(thm)],[f546,f290])).
% 0.17/5.71 fof(f554,plain,(
% 0.17/5.71 ~sQ0_spl|sQ33_spl),
% 0.17/5.71 inference(contradiction_clause,[status(thm)],[f553])).
% 0.17/5.71 fof(f617,definition,(
% 0.17/5.71 sQ43_spl <=> (aElementOf0(szszuzczcdt0(sz00),szNzAzT0))),
% 0.17/5.71 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.17/5.71 fof(f619,plain,(
% 0.17/5.71 ~aElementOf0(szszuzczcdt0(sz00),szNzAzT0)|sQ43_spl),
% 0.17/5.71 inference(component_clause,[status(thm)],[f617])).
% 0.17/5.71 fof(f706,definition,(
% 0.17/5.71 sQ55_spl <=> (aElementOf0(sK1_skl(slcrc0,xS),slcrc0))),
% 0.17/5.71 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.17/5.71 fof(f707,plain,(
% 0.17/5.71 aElementOf0(sK1_skl(slcrc0,xS),slcrc0)|~sQ55_spl),
% 0.17/5.71 inference(component_clause,[status(thm)],[f706])).
% 0.17/5.71 fof(f756,plain,(
% 0.17/5.71 $false|sQ19_spl),
% 0.17/5.71 inference(forward_subsumption_resolution,[status(thm)],[f407,f235])).
% 0.17/5.71 fof(f757,plain,(
% 0.17/5.71 sQ19_spl),
% 0.17/5.71 inference(contradiction_clause,[status(thm)],[f756])).
% 0.17/5.71 fof(f764,plain,(
% 0.17/5.71 aElementOf0(szszuzczcdt0(sz00),szNzAzT0)),
% 0.17/5.71 inference(resolution,[status(thm)],[f139,f137])).
% 0.17/5.71 fof(f765,plain,(
% 0.17/5.71 $false|sQ43_spl),
% 0.17/5.71 inference(forward_subsumption_resolution,[status(thm)],[f764,f619])).
% 0.17/5.71 fof(f766,plain,(
% 0.17/5.71 sQ43_spl),
% 0.17/5.71 inference(contradiction_clause,[status(thm)],[f765])).
% 0.17/5.71 fof(f768,plain,(
% 0.17/5.71 ~szszuzczcdt0(sz00)=sz00),
% 0.17/5.71 inference(resolution,[status(thm)],[f140,f137])).
% 0.17/5.71 fof(f943,definition,(
% 0.17/5.71 sQ79_spl <=> (szszuzczcdt0(sz00)=sz00)),
% 0.17/5.71 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.17/5.71 fof(f944,plain,(
% 0.17/5.71 szszuzczcdt0(sz00)=sz00|~sQ79_spl),
% 0.17/5.71 inference(component_clause,[status(thm)],[f943])).
% 0.17/5.71 fof(f964,plain,(
% 0.17/5.71 $false|~sQ79_spl),
% 0.17/5.71 inference(forward_subsumption_resolution,[status(thm)],[f944,f768])).
% 0.17/5.71 fof(f965,plain,(
% 0.17/5.71 ~sQ79_spl),
% 0.17/5.71 inference(contradiction_clause,[status(thm)],[f964])).
% 0.17/5.71 fof(f1201,definition,(
% 0.17/5.71 sQ115_spl <=> (slbdtrb0(szszuzczcdt0(sz00))=slcrc0)),
% 0.17/5.71 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.17/5.71 fof(f1202,plain,(
% 0.17/5.71 slbdtrb0(szszuzczcdt0(sz00))=slcrc0|~sQ115_spl),
% 0.17/5.71 inference(component_clause,[status(thm)],[f1201])).
% 0.17/5.71 fof(f1283,definition,(
% 0.17/5.71 sQ130_spl <=> (aElementOf0(sbrdtbr0(xS),slcrc0))),
% 0.17/5.71 introduced(definition,[new_symbols(definition,[sQ130_spl])],[split_symbol_definition])).
% 0.17/5.71 fof(f1284,plain,(
% 0.17/5.71 aElementOf0(sbrdtbr0(xS),slcrc0)|~sQ130_spl),
% 0.17/5.71 inference(component_clause,[status(thm)],[f1283])).
% 0.17/5.71 fof(f1290,plain,(
% 0.17/5.71 $false|~sQ130_spl),
% 0.17/5.71 inference(forward_subsumption_resolution,[status(thm)],[f1284,f254])).
% 0.17/5.71 fof(f1291,plain,(
% 0.17/5.71 ~sQ130_spl),
% 0.17/5.71 inference(contradiction_clause,[status(thm)],[f1290])).
% 0.17/5.71 fof(f1375,plain,(
% 0.17/5.71 aElementOf0(sz00,slcrc0)|~sQ115_spl),
% 0.17/5.71 inference(backward_demodulation,[status(thm)],[f1202,f451])).
% 0.17/5.71 fof(f1385,plain,(
% 0.17/5.71 $false|~sQ115_spl),
% 0.17/5.71 inference(forward_subsumption_resolution,[status(thm)],[f1375,f254])).
% 0.17/5.71 fof(f1386,plain,(
% 0.17/5.71 ~sQ115_spl),
% 0.17/5.71 inference(contradiction_clause,[status(thm)],[f1385])).
% 0.17/5.71 fof(f1952,plain,(
% 0.17/5.71 ~isFinite0(xS)|xS=slcrc0|aElementOf0(szmzazxdt0(xS),xS)),
% 0.17/5.71 inference(resolution,[status(thm)],[f268,f234])).
% 0.17/5.71 fof(f1954,definition,(
% 0.17/5.71 sQ226_spl <=> (aElementOf0(szmzazxdt0(xS),xS))),
% 0.17/5.71 introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition])).
% 0.17/5.71 fof(f1955,plain,(
% 0.17/5.71 aElementOf0(szmzazxdt0(xS),xS)|~sQ226_spl),
% 0.17/5.71 inference(component_clause,[status(thm)],[f1954])).
% 0.17/5.71 fof(f1957,plain,(
% 0.17/5.71 ~sQ19_spl|sQ0_spl|sQ226_spl),
% 0.17/5.71 inference(split_clause,[status(thm)],[f1952,f405,f246,f1954])).
% 0.17/5.71 fof(f2020,plain,(
% 0.17/5.71 aElementOf0(szmzazxdt0(xS),szNzAzT0)|~sQ226_spl|~sQ4_spl),
% 0.17/5.71 inference(resolution,[status(thm)],[f1955,f287])).
% 0.17/5.71 fof(f2159,plain,(
% 0.17/5.71 $false|~sQ55_spl),
% 0.17/5.71 inference(forward_subsumption_resolution,[status(thm)],[f707,f254])).
% 0.17/5.71 fof(f2160,plain,(
% 0.17/5.71 ~sQ55_spl),
% 0.17/5.71 inference(contradiction_clause,[status(thm)],[f2159])).
% 0.17/5.71 fof(f2279,plain,(
% 0.17/5.71 ~aElementOf0(szszuzczcdt0(szmzazxdt0(xS)),szNzAzT0)|~sQ1_spl),
% 0.17/5.71 inference(resolution,[status(thm)],[f250,f239])).
% 0.17/5.73 fof(f2481,definition,(
% 0.17/5.73 sQ289_spl <=> (aElementOf0(sK1_skl(slcrc0,szNzAzT0),slcrc0))),
% 0.17/5.73 introduced(definition,[new_symbols(definition,[sQ289_spl])],[split_symbol_definition])).
% 0.17/5.73 fof(f2482,plain,(
% 0.17/5.73 aElementOf0(sK1_skl(slcrc0,szNzAzT0),slcrc0)|~sQ289_spl),
% 0.17/5.73 inference(component_clause,[status(thm)],[f2481])).
% 0.17/5.73 fof(f2576,plain,(
% 0.17/5.73 $false|~sQ289_spl),
% 0.17/5.73 inference(forward_subsumption_resolution,[status(thm)],[f2482,f254])).
% 0.17/5.73 fof(f2577,plain,(
% 0.17/5.73 ~sQ289_spl),
% 0.17/5.73 inference(contradiction_clause,[status(thm)],[f2576])).
% 0.17/5.73 fof(f2918,plain,(
% 0.17/5.73 aElementOf0(szszuzczcdt0(szmzazxdt0(xS)),szNzAzT0)|~sQ226_spl|~sQ4_spl),
% 0.17/5.73 inference(resolution,[status(thm)],[f2020,f139])).
% 0.17/5.73 fof(f2938,plain,(
% 0.17/5.73 $false|~sQ1_spl|~sQ226_spl|~sQ4_spl),
% 0.17/5.73 inference(forward_subsumption_resolution,[status(thm)],[f2918,f2279])).
% 0.17/5.73 fof(f2939,plain,(
% 0.17/5.73 ~sQ1_spl|~sQ226_spl|~sQ4_spl),
% 0.17/5.73 inference(contradiction_clause,[status(thm)],[f2938])).
% 0.17/5.73 fof(f2940,plain,(
% 0.17/5.73 $false),
% 0.17/5.73 inference(sat_refutation,[status(thm)],[f252,f289,f309,f498,f500,f554,f757,f766,f965,f1291,f1386,f1957,f2160,f2577,f2939])).
% 0.17/5.73 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/5.74 % Elapsed time: 0.325782 seconds
% 0.17/5.74 % CPU time: 2.298064 seconds
% 0.17/5.74 % Total memory used: 132.038 MB
% 0.17/5.74 % Net memory used: 130.151 MB
%------------------------------------------------------------------------------