%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM545+2 : 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 : n026.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.10s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM545+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 02:41:51 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.49 % Refutation found
% 0.10/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.49 fof(f5,definition,(
% 0.10/0.49 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f24,axiom,(
% 0.10/0.49 aElementOf0(sz00,szNzAzT0) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f25,axiom,(
% 0.10/0.49 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aElementOf0(szszuzczcdt0(W0),szNzAzT0)& szszuzczcdt0(W0) != sz00 ) ) )),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f55,hypothesis,(
% 0.10/0.49 ( aSet0(xS)& (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,szNzAzT0) ))& aSubsetOf0(xS,szNzAzT0)& isFinite0(xS) ) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f56,hypothesis,(
% 0.10/0.49 ( ~ ( ~ (? [W0] : aElementOf0(W0,xS))& xS = slcrc0 )=> ( aElementOf0(szmzazxdt0(xS),xS)& (! [W0] :( aElementOf0(W0,xS)=> sdtlseqdt0(W0,szmzazxdt0(xS)) ))& aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))& (! [W0] :( aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))<=> ( aElementOf0(W0,szNzAzT0)& sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))) ) ))& (! [W0] :( aElementOf0(W0,xS)=> aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ))& aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))) ) ) ),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f57,conjecture,(
% 0.10/0.49 (? [W0] :( aElementOf0(W0,szNzAzT0)& ( ( aSet0(slbdtrb0(W0))& (! [W1] :( aElementOf0(W1,slbdtrb0(W0))<=> ( aElementOf0(W1,szNzAzT0)& sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ))=> ( (! [W1] :( aElementOf0(W1,xS)=> aElementOf0(W1,slbdtrb0(W0)) ))| aSubsetOf0(xS,slbdtrb0(W0)) ) ) ) )),
% 0.10/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.49 fof(f58,negated_conjecture,(
% 0.10/0.49 ~((? [W0] :( aElementOf0(W0,szNzAzT0)& ( ( aSet0(slbdtrb0(W0))& (! [W1] :( aElementOf0(W1,slbdtrb0(W0))<=> ( aElementOf0(W1,szNzAzT0)& sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) ))=> ( (! [W1] :( aElementOf0(W1,xS)=> aElementOf0(W1,slbdtrb0(W0)) ))| aSubsetOf0(xS,slbdtrb0(W0)) ) ) ) ))),
% 0.10/0.49 inference(negated_conjecture,[status(cth)],[f57])).
% 0.10/0.49 fof(f69,plain,(
% 0.10/0.49 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 0.10/0.49 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.10/0.49 fof(f70,plain,(
% 0.10/0.49 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f69])).
% 0.10/0.49 fof(f71,plain,(
% 0.10/0.49 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.10/0.49 inference(miniscoping,[status(thm)],[f70])).
% 0.10/0.49 fof(f72,plain,(
% 0.10/0.49 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 0.10/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f71])).
% 0.10/0.49 fof(f73,plain,(
% 0.10/0.49 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f72])).
% 0.10/0.49 fof(f74,plain,(
% 0.10/0.49 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f72])).
% 0.10/0.49 fof(f137,plain,(
% 0.10/0.49 aElementOf0(sz00,szNzAzT0)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f24])).
% 0.10/0.49 fof(f138,plain,(
% 0.10/0.49 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aElementOf0(szszuzczcdt0(W0),szNzAzT0)&~szszuzczcdt0(W0)=sz00))),
% 0.10/0.49 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.10/0.49 fof(f139,plain,(
% 0.10/0.49 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(szszuzczcdt0(X0),szNzAzT0))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f138])).
% 0.10/0.49 fof(f234,plain,(
% 0.10/0.49 ((aSet0(xS)&(![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,szNzAzT0))))&aSubsetOf0(xS,szNzAzT0))&isFinite0(xS)),
% 0.10/0.49 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.10/0.49 fof(f236,plain,(
% 0.10/0.49 ![X0]: (~aElementOf0(X0,xS)|aElementOf0(X0,szNzAzT0))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f234])).
% 0.10/0.49 fof(f239,plain,(
% 0.10/0.49 ((![W0]: ~aElementOf0(W0,xS))&xS=slcrc0)|(((((aElementOf0(szmzazxdt0(xS),xS)&(![W0]: (~aElementOf0(W0,xS)|sdtlseqdt0(W0,szmzazxdt0(xS)))))&aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))&(![W0]: (aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))<=>(aElementOf0(W0,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))))))&(![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))&aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),
% 0.10/0.49 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 0.10/0.49 fof(f240,definition,(
% 0.10/0.49 sP1_prd<=>((![W0]: ~aElementOf0(W0,xS))&xS=slcrc0)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.10/0.49 fof(f241,plain,(
% 0.10/0.49 sP1_prd|(((((aElementOf0(szmzazxdt0(xS),xS)&(![W0]: (~aElementOf0(W0,xS)|sdtlseqdt0(W0,szmzazxdt0(xS)))))&aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))&(![W0]: (aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))<=>(aElementOf0(W0,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))))))&(![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))&aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),
% 0.10/0.49 inference(formula_renaming,[status(thm)],[f239,f240])).
% 0.10/0.49 fof(f242,plain,(
% 0.10/0.49 sP1_prd|(((((aElementOf0(szmzazxdt0(xS),xS)&(![W0]: (~aElementOf0(W0,xS)|sdtlseqdt0(W0,szmzazxdt0(xS)))))&aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))&(![W0]: ((~aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(aElementOf0(W0,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS)))))&(aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(~aElementOf0(W0,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))))))))&(![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))&aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f241])).
% 0.10/0.49 fof(f243,plain,(
% 0.10/0.49 sP1_prd|(((((aElementOf0(szmzazxdt0(xS),xS)&(![W0]: (~aElementOf0(W0,xS)|sdtlseqdt0(W0,szmzazxdt0(xS)))))&aSet0(slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))&((![W0]: (~aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(aElementOf0(W0,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))))))&(![W0]: (aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|(~aElementOf0(W0,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W0),szszuzczcdt0(szmzazxdt0(xS))))))))&(![W0]: (~aElementOf0(W0,xS)|aElementOf0(W0,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))))&aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),
% 0.10/0.49 inference(miniscoping,[status(thm)],[f242])).
% 0.10/0.49 fof(f244,plain,(
% 0.10/0.49 sP1_prd|aElementOf0(szmzazxdt0(xS),xS)),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f243])).
% 0.10/0.49 fof(f251,plain,(
% 0.10/0.49 sP1_prd|aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f243])).
% 0.10/0.49 fof(f252,plain,(
% 0.10/0.49 (![W0]: (~aElementOf0(W0,szNzAzT0)|((aSet0(slbdtrb0(W0))&(![W1]: (aElementOf0(W1,slbdtrb0(W0))<=>(aElementOf0(W1,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W1),W0)))))&((?[W1]: (aElementOf0(W1,xS)&~aElementOf0(W1,slbdtrb0(W0))))&~aSubsetOf0(xS,slbdtrb0(W0))))))),
% 0.10/0.49 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 0.10/0.49 fof(f253,plain,(
% 0.10/0.49 ![W0]: (~aElementOf0(W0,szNzAzT0)|((aSet0(slbdtrb0(W0))&(![W1]: ((~aElementOf0(W1,slbdtrb0(W0))|(aElementOf0(W1,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W1),W0)))&(aElementOf0(W1,slbdtrb0(W0))|(~aElementOf0(W1,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W1),W0))))))&((?[W1]: (aElementOf0(W1,xS)&~aElementOf0(W1,slbdtrb0(W0))))&~aSubsetOf0(xS,slbdtrb0(W0)))))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f252])).
% 0.10/0.49 fof(f254,plain,(
% 0.10/0.49 ![W0]: (~aElementOf0(W0,szNzAzT0)|((aSet0(slbdtrb0(W0))&((![W1]: (~aElementOf0(W1,slbdtrb0(W0))|(aElementOf0(W1,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W1),W0))))&(![W1]: (aElementOf0(W1,slbdtrb0(W0))|(~aElementOf0(W1,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W1),W0))))))&((?[W1]: (aElementOf0(W1,xS)&~aElementOf0(W1,slbdtrb0(W0))))&~aSubsetOf0(xS,slbdtrb0(W0)))))),
% 0.10/0.49 inference(miniscoping,[status(thm)],[f253])).
% 0.10/0.49 fof(f255,plain,(
% 0.10/0.49 ![W0]: (~aElementOf0(W0,szNzAzT0)|((aSet0(slbdtrb0(W0))&((![W1]: (~aElementOf0(W1,slbdtrb0(W0))|(aElementOf0(W1,szNzAzT0)&sdtlseqdt0(szszuzczcdt0(W1),W0))))&(![W1]: (aElementOf0(W1,slbdtrb0(W0))|(~aElementOf0(W1,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(W1),W0))))))&((aElementOf0(sK9_skl(W0),xS)&~aElementOf0(sK9_skl(W0),slbdtrb0(W0)))&~aSubsetOf0(xS,slbdtrb0(W0)))))),
% 0.10/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(W1,sK9_skl(W0))],[f254])).
% 0.10/0.49 fof(f260,plain,(
% 0.10/0.49 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(sK9_skl(X0),xS))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f255])).
% 0.10/0.49 fof(f262,plain,(
% 0.10/0.49 ![X0]: (~aElementOf0(X0,szNzAzT0)|~aSubsetOf0(xS,slbdtrb0(X0)))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f255])).
% 0.10/0.49 fof(f269,plain,(
% 0.10/0.49 (~sP1_prd|((![W0]: ~aElementOf0(W0,xS))&xS=slcrc0))&(sP1_prd|((?[W0]: aElementOf0(W0,xS))|~xS=slcrc0))),
% 0.10/0.49 inference(NNF_transformation,[status(thm)],[f240])).
% 0.10/0.49 fof(f270,plain,(
% 0.10/0.49 (~sP1_prd|((![W0]: ~aElementOf0(W0,xS))&xS=slcrc0))&(sP1_prd|(aElementOf0(sK10_skl,xS)|~xS=slcrc0))),
% 0.10/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W0,sK10_skl)],[f269])).
% 0.10/0.49 fof(f271,plain,(
% 0.10/0.49 ![X0]: (~sP1_prd|~aElementOf0(X0,xS))),
% 0.10/0.49 inference(cnf_transformation,[status(thm)],[f270])).
% 0.10/0.49 fof(f274,definition,(
% 0.10/0.49 sQ0_spl <=> (sP1_prd)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f277,definition,(
% 0.10/0.49 sQ1_spl <=> (aElementOf0(szmzazxdt0(xS),xS))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f278,plain,(
% 0.10/0.49 aElementOf0(szmzazxdt0(xS),xS)|~sQ1_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f277])).
% 0.10/0.49 fof(f280,plain,(
% 0.10/0.49 sQ0_spl|sQ1_spl),
% 0.10/0.49 inference(split_clause,[status(thm)],[f244,f274,f277])).
% 0.10/0.49 fof(f305,definition,(
% 0.10/0.49 sQ8_spl <=> (aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f306,plain,(
% 0.10/0.49 aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|~sQ8_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f305])).
% 0.10/0.49 fof(f308,plain,(
% 0.10/0.49 sQ0_spl|sQ8_spl),
% 0.10/0.49 inference(split_clause,[status(thm)],[f251,f274,f305])).
% 0.10/0.49 fof(f309,definition,(
% 0.10/0.49 ![X0]: (sQ9_spl <=> (~aElementOf0(X0,xS)))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f310,plain,(
% 0.10/0.49 ![X0]: (~aElementOf0(X0,xS)|~sQ9_spl)),
% 0.10/0.49 inference(component_clause,[status(thm)],[f309])).
% 0.10/0.49 fof(f312,plain,(
% 0.10/0.49 ~sQ0_spl|sQ9_spl),
% 0.10/0.49 inference(split_clause,[status(thm)],[f271,f274,f309])).
% 0.10/0.49 fof(f321,plain,(
% 0.10/0.49 aSet0(slcrc0)),
% 0.10/0.49 inference(destructive_equality_resolution,[status(thm)],[f73])).
% 0.10/0.49 fof(f322,plain,(
% 0.10/0.49 ![X0]: (~aElementOf0(X0,slcrc0))),
% 0.10/0.49 inference(destructive_equality_resolution,[status(thm)],[f74])).
% 0.10/0.49 fof(f364,plain,(
% 0.10/0.49 ![X0]: (~aElementOf0(X0,szNzAzT0)|~sQ9_spl)),
% 0.10/0.49 inference(backward_subsumption_resolution,[status(thm)],[f260,f310])).
% 0.10/0.49 fof(f372,plain,(
% 0.10/0.49 $false|~sQ9_spl),
% 0.10/0.49 inference(backward_subsumption_resolution,[status(thm)],[f137,f364])).
% 0.10/0.49 fof(f373,plain,(
% 0.10/0.49 ~sQ9_spl),
% 0.10/0.49 inference(contradiction_clause,[status(thm)],[f372])).
% 0.10/0.49 fof(f409,definition,(
% 0.10/0.49 sQ19_spl <=> (szNzAzT0=slcrc0)),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f410,plain,(
% 0.10/0.49 szNzAzT0=slcrc0|~sQ19_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f409])).
% 0.10/0.49 fof(f416,plain,(
% 0.10/0.49 aElementOf0(sz00,slcrc0)|~sQ19_spl),
% 0.10/0.49 inference(backward_demodulation,[status(thm)],[f410,f137])).
% 0.10/0.49 fof(f470,plain,(
% 0.10/0.49 $false|~sQ19_spl),
% 0.10/0.49 inference(forward_subsumption_resolution,[status(thm)],[f416,f322])).
% 0.10/0.49 fof(f471,plain,(
% 0.10/0.49 ~sQ19_spl),
% 0.10/0.49 inference(contradiction_clause,[status(thm)],[f470])).
% 0.10/0.49 fof(f513,definition,(
% 0.10/0.49 sQ24_spl <=> (aSet0(slcrc0))),
% 0.10/0.49 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.10/0.49 fof(f515,plain,(
% 0.10/0.49 ~aSet0(slcrc0)|sQ24_spl),
% 0.10/0.49 inference(component_clause,[status(thm)],[f513])).
% 0.10/0.49 fof(f519,plain,(
% 0.10/0.49 $false|sQ24_spl),
% 0.10/0.49 inference(forward_subsumption_resolution,[status(thm)],[f515,f321])).
% 0.10/0.49 fof(f520,plain,(
% 0.10/0.49 sQ24_spl),
% 0.10/0.49 inference(contradiction_clause,[status(thm)],[f519])).
% 0.10/0.49 fof(f521,plain,(
% 0.10/0.49 aElementOf0(szmzazxdt0(xS),szNzAzT0)|~sQ1_spl),
% 0.10/0.49 inference(resolution,[status(thm)],[f278,f236])).
% 0.10/0.49 fof(f654,plain,(
% 0.10/0.49 aElementOf0(szszuzczcdt0(szmzazxdt0(xS)),szNzAzT0)|~sQ1_spl),
% 0.10/0.49 inference(resolution,[status(thm)],[f139,f521])).
% 0.10/0.49 fof(f834,plain,(
% 0.10/0.49 ~aSubsetOf0(xS,slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))|~sQ1_spl),
% 0.10/0.50 inference(resolution,[status(thm)],[f654,f262])).
% 0.10/0.50 fof(f837,plain,(
% 0.10/0.50 $false|~sQ8_spl|~sQ1_spl),
% 0.10/0.50 inference(forward_subsumption_resolution,[status(thm)],[f834,f306])).
% 0.10/0.50 fof(f838,plain,(
% 0.10/0.50 ~sQ8_spl|~sQ1_spl),
% 0.10/0.50 inference(contradiction_clause,[status(thm)],[f837])).
% 0.10/0.50 fof(f839,plain,(
% 0.10/0.50 $false),
% 0.10/0.50 inference(sat_refutation,[status(thm)],[f280,f308,f312,f373,f471,f520,f838])).
% 0.10/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.51 % Elapsed time: 0.141484 seconds
% 0.10/0.51 % CPU time: 0.855770 seconds
% 0.10/0.51 % Total memory used: 120.481 MB
% 0.10/0.51 % Net memory used: 119.379 MB
%------------------------------------------------------------------------------