%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM620+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 : n015.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:22 PM UTC 2026
% Result : Theorem 6.22s 1.33s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM620+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.09/0.37 % Computer : n015.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 02:47:51 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 6.22/1.33 % Refutation found
% 6.22/1.33 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.22/1.33 % SZS output start CNFRefutation for theBenchmark
% 6.22/1.33 fof(f5,definition,(
% 6.22/1.33 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 6.22/1.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.22/1.33 fof(f9,axiom,(
% 6.22/1.33 (! [W0] :( ( aSet0(W0)& isCountable0(W0) )=> W0 != slcrc0 ) )),
% 6.22/1.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.22/1.33 fof(f10,definition,(
% 6.22/1.33 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 6.22/1.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.22/1.33 fof(f23,axiom,(
% 6.22/1.33 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 6.22/1.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.22/1.33 fof(f25,axiom,(
% 6.22/1.33 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aElementOf0(szszuzczcdt0(W0),szNzAzT0)& szszuzczcdt0(W0) != sz00 ) ) )),
% 6.22/1.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.22/1.33 fof(f47,definition,(
% 6.22/1.33 (! [W0] :( ( aSubsetOf0(W0,szNzAzT0)& W0 != slcrc0 )=> (! [W1] :( W1 = szmzizndt0(W0)<=> ( aElementOf0(W1,W0)& (! [W2] :( aElementOf0(W2,W0)=> sdtlseqdt0(W1,W2) ) )) ) )) )),
% 6.22/1.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.22/1.33 fof(f82,hypothesis,(
% 6.22/1.33 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)& isCountable0(sdtlpdtrp0(xN,W0)) ) ) )),
% 6.22/1.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.22/1.33 fof(f111,hypothesis,(
% 6.22/1.33 ( aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))& aElementOf0(xn,szNzAzT0)& sdtlpdtrp0(xe,xn) = xp ) ),
% 6.22/1.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.22/1.33 fof(f115,hypothesis,(
% 6.22/1.33 ( aElementOf0(xm,szNzAzT0)& xx = sdtlpdtrp0(xe,xm) ) ),
% 6.22/1.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.22/1.33 fof(f116,hypothesis,(
% 6.22/1.33 xx = szmzizndt0(sdtlpdtrp0(xN,xm)) ),
% 6.22/1.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.22/1.33 fof(f117,conjecture,(
% 6.22/1.33 ( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))=> aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ) ),
% 6.22/1.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.22/1.33 fof(f118,negated_conjecture,(
% 6.22/1.33 ~(( aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))=> aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ) )),
% 6.22/1.33 inference(negated_conjecture,[status(cth)],[f117])).
% 6.22/1.33 fof(f129,plain,(
% 6.22/1.33 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 6.22/1.33 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 6.22/1.33 fof(f130,plain,(
% 6.22/1.33 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 6.22/1.33 inference(NNF_transformation,[status(thm)],[f129])).
% 6.22/1.33 fof(f131,plain,(
% 6.22/1.33 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 6.22/1.33 inference(miniscoping,[status(thm)],[f130])).
% 6.22/1.33 fof(f132,plain,(
% 6.22/1.33 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 6.22/1.33 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f131])).
% 6.22/1.33 fof(f133,plain,(
% 6.22/1.33 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f132])).
% 6.22/1.33 fof(f141,plain,(
% 6.22/1.33 ![W0]: ((~aSet0(W0)|~isCountable0(W0))|~W0=slcrc0)),
% 6.22/1.33 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 6.22/1.33 fof(f142,plain,(
% 6.22/1.33 ![X0]: (~aSet0(X0)|~isCountable0(X0)|~X0=slcrc0)),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f141])).
% 6.22/1.33 fof(f143,plain,(
% 6.22/1.33 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 6.22/1.33 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 6.22/1.33 fof(f144,plain,(
% 6.22/1.33 ![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))))))))),
% 6.22/1.33 inference(NNF_transformation,[status(thm)],[f143])).
% 6.22/1.33 fof(f145,plain,(
% 6.22/1.33 ![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))))))))),
% 6.22/1.33 inference(miniscoping,[status(thm)],[f144])).
% 6.22/1.33 fof(f146,plain,(
% 6.22/1.33 ![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)))))))),
% 6.22/1.33 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f145])).
% 6.22/1.33 fof(f147,plain,(
% 6.22/1.33 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f146])).
% 6.22/1.33 fof(f148,plain,(
% 6.22/1.33 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f146])).
% 6.22/1.33 fof(f195,plain,(
% 6.22/1.33 aSet0(szNzAzT0)),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f23])).
% 6.22/1.33 fof(f198,plain,(
% 6.22/1.33 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aElementOf0(szszuzczcdt0(W0),szNzAzT0)&~szszuzczcdt0(W0)=sz00))),
% 6.22/1.33 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 6.22/1.33 fof(f199,plain,(
% 6.22/1.33 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(szszuzczcdt0(X0),szNzAzT0))),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f198])).
% 6.22/1.33 fof(f253,plain,(
% 6.22/1.33 ![W0]: ((~aSubsetOf0(W0,szNzAzT0)|W0=slcrc0)|(![W1]: (W1=szmzizndt0(W0)<=>(aElementOf0(W1,W0)&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2)))))))),
% 6.22/1.33 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 6.22/1.33 fof(f254,plain,(
% 6.22/1.33 ![W0]: ((~aSubsetOf0(W0,szNzAzT0)|W0=slcrc0)|(![W1]: ((~W1=szmzizndt0(W0)|(aElementOf0(W1,W0)&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2)))))&(W1=szmzizndt0(W0)|(~aElementOf0(W1,W0)|(?[W2]: (aElementOf0(W2,W0)&~sdtlseqdt0(W1,W2))))))))),
% 6.22/1.33 inference(NNF_transformation,[status(thm)],[f253])).
% 6.22/1.33 fof(f255,plain,(
% 6.22/1.33 ![W0]: ((~aSubsetOf0(W0,szNzAzT0)|W0=slcrc0)|((![W1]: (~W1=szmzizndt0(W0)|(aElementOf0(W1,W0)&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2))))))&(![W1]: (W1=szmzizndt0(W0)|(~aElementOf0(W1,W0)|(?[W2]: (aElementOf0(W2,W0)&~sdtlseqdt0(W1,W2))))))))),
% 6.22/1.33 inference(miniscoping,[status(thm)],[f254])).
% 6.22/1.33 fof(f256,plain,(
% 6.22/1.33 ![W0]: ((~aSubsetOf0(W0,szNzAzT0)|W0=slcrc0)|((![W1]: (~W1=szmzizndt0(W0)|(aElementOf0(W1,W0)&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2))))))&(![W1]: (W1=szmzizndt0(W0)|(~aElementOf0(W1,W0)|(aElementOf0(sK6_skl(W1,W0),W0)&~sdtlseqdt0(W1,sK6_skl(W1,W0))))))))),
% 6.22/1.33 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W2,sK6_skl(W1,W0))],[f255])).
% 6.22/1.33 fof(f257,plain,(
% 6.22/1.33 ![X0,X1]: (~aSubsetOf0(X0,szNzAzT0)|X0=slcrc0|~X1=szmzizndt0(X0)|aElementOf0(X1,X0))),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f256])).
% 6.22/1.33 fof(f399,plain,(
% 6.22/1.33 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)&isCountable0(sdtlpdtrp0(xN,W0))))),
% 6.22/1.33 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 6.22/1.33 fof(f400,plain,(
% 6.22/1.33 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0))),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f399])).
% 6.22/1.33 fof(f401,plain,(
% 6.22/1.33 ![X0]: (~aElementOf0(X0,szNzAzT0)|isCountable0(sdtlpdtrp0(xN,X0)))),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f399])).
% 6.22/1.33 fof(f464,plain,(
% 6.22/1.33 aElementOf0(xn,szNzAzT0)),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f111])).
% 6.22/1.33 fof(f470,plain,(
% 6.22/1.33 aElementOf0(xm,szNzAzT0)),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f115])).
% 6.22/1.33 fof(f472,plain,(
% 6.22/1.33 xx=szmzizndt0(sdtlpdtrp0(xN,xm))),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f116])).
% 6.22/1.33 fof(f473,plain,(
% 6.22/1.33 (aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))&~aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))))),
% 6.22/1.33 inference(pre_NNF_transformation,[status(thm)],[f118])).
% 6.22/1.33 fof(f474,plain,(
% 6.22/1.33 aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f473])).
% 6.22/1.33 fof(f475,plain,(
% 6.22/1.33 ~aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 6.22/1.33 inference(cnf_transformation,[status(thm)],[f473])).
% 6.22/1.33 fof(f482,plain,(
% 6.22/1.33 aSet0(slcrc0)),
% 6.22/1.33 inference(destructive_equality_resolution,[status(thm)],[f133])).
% 6.22/1.33 fof(f484,plain,(
% 6.22/1.33 ~aSet0(slcrc0)|~isCountable0(slcrc0)),
% 6.22/1.33 inference(destructive_equality_resolution,[status(thm)],[f142])).
% 6.22/1.33 fof(f495,plain,(
% 6.22/1.33 ![X0]: (~aSubsetOf0(X0,szNzAzT0)|X0=slcrc0|aElementOf0(szmzizndt0(X0),X0))),
% 7.02/1.35 inference(destructive_equality_resolution,[status(thm)],[f257])).
% 7.02/1.35 fof(f524,definition,(
% 7.02/1.35 sQ0_spl <=> (aSet0(sdtlpdtrp0(xN,szszuzczcdt0(xn))))),
% 7.02/1.35 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 7.02/1.35 fof(f531,plain,(
% 7.02/1.35 ![X0]: (~aSet0(sdtlpdtrp0(xN,szszuzczcdt0(xn)))|~aElementOf0(X0,sdtlpdtrp0(xN,xm))|aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn))))),
% 7.02/1.35 inference(resolution,[status(thm)],[f148,f474])).
% 7.02/1.35 fof(f532,definition,(
% 7.02/1.35 ![X0]: (sQ2_spl <=> (~aElementOf0(X0,sdtlpdtrp0(xN,xm))|aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn)))))),
% 7.02/1.35 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 7.02/1.35 fof(f533,plain,(
% 7.02/1.35 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xm))|aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn)))|~sQ2_spl)),
% 7.02/1.35 inference(component_clause,[status(thm)],[f532])).
% 7.02/1.35 fof(f535,plain,(
% 7.02/1.35 ~sQ0_spl|sQ2_spl),
% 7.02/1.35 inference(split_clause,[status(thm)],[f531,f524,f532])).
% 7.02/1.35 fof(f582,plain,(
% 7.02/1.35 aElementOf0(szszuzczcdt0(xn),szNzAzT0)),
% 7.02/1.35 inference(resolution,[status(thm)],[f464,f199])).
% 7.02/1.35 fof(f584,definition,(
% 7.02/1.35 sQ12_spl <=> (aSet0(szNzAzT0))),
% 7.02/1.35 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 7.02/1.35 fof(f586,plain,(
% 7.02/1.35 ~aSet0(szNzAzT0)|sQ12_spl),
% 7.02/1.35 inference(component_clause,[status(thm)],[f584])).
% 7.02/1.35 fof(f605,plain,(
% 7.02/1.35 aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0)),
% 7.02/1.35 inference(resolution,[status(thm)],[f470,f400])).
% 7.02/1.35 fof(f670,plain,(
% 7.02/1.35 aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),szNzAzT0)),
% 7.02/1.35 inference(resolution,[status(thm)],[f582,f400])).
% 7.02/1.35 fof(f815,plain,(
% 7.02/1.35 ~isCountable0(slcrc0)),
% 7.02/1.35 inference(forward_subsumption_resolution,[status(thm)],[f484,f482])).
% 7.02/1.35 fof(f1015,definition,(
% 7.02/1.35 sQ92_spl <=> (sdtlpdtrp0(xN,xm)=slcrc0)),
% 7.02/1.35 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 7.02/1.35 fof(f1016,plain,(
% 7.02/1.35 sdtlpdtrp0(xN,xm)=slcrc0|~sQ92_spl),
% 7.02/1.35 inference(component_clause,[status(thm)],[f1015])).
% 7.02/1.35 fof(f1106,plain,(
% 7.02/1.35 ~aSet0(szNzAzT0)|aSet0(sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 7.02/1.35 inference(resolution,[status(thm)],[f670,f147])).
% 7.02/1.35 fof(f1123,plain,(
% 7.02/1.35 ~sQ12_spl|sQ0_spl),
% 7.02/1.35 inference(split_clause,[status(thm)],[f1106,f584,f524])).
% 7.02/1.35 fof(f1218,plain,(
% 7.02/1.35 $false|sQ12_spl),
% 7.02/1.35 inference(forward_subsumption_resolution,[status(thm)],[f195,f586])).
% 7.02/1.35 fof(f1219,plain,(
% 7.02/1.35 sQ12_spl),
% 7.02/1.35 inference(contradiction_clause,[status(thm)],[f1218])).
% 7.02/1.35 fof(f2851,plain,(
% 7.02/1.35 sdtlpdtrp0(xN,xm)=slcrc0|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm))),
% 7.02/1.35 inference(resolution,[status(thm)],[f605,f495])).
% 7.02/1.35 fof(f2888,definition,(
% 7.02/1.35 sQ375_spl <=> (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm)))),
% 7.02/1.35 introduced(definition,[new_symbols(definition,[sQ375_spl])],[split_symbol_definition])).
% 7.02/1.35 fof(f2889,plain,(
% 7.02/1.35 aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),sdtlpdtrp0(xN,xm))|~sQ375_spl),
% 7.02/1.35 inference(component_clause,[status(thm)],[f2888])).
% 7.02/1.35 fof(f2891,plain,(
% 7.02/1.35 sQ92_spl|sQ375_spl),
% 7.02/1.35 inference(split_clause,[status(thm)],[f2851,f1015,f2888])).
% 7.02/1.35 fof(f2927,plain,(
% 7.02/1.35 aElementOf0(xx,sdtlpdtrp0(xN,xm))|~sQ375_spl),
% 7.02/1.35 inference(forward_demodulation,[status(thm)],[f472,f2889])).
% 7.02/1.35 fof(f3819,plain,(
% 7.02/1.35 aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn)))|~sQ2_spl|~sQ375_spl),
% 7.02/1.35 inference(resolution,[status(thm)],[f533,f2927])).
% 7.02/1.35 fof(f3820,plain,(
% 7.02/1.35 $false|~sQ2_spl|~sQ375_spl),
% 7.02/1.35 inference(forward_subsumption_resolution,[status(thm)],[f3819,f475])).
% 7.02/1.35 fof(f3821,plain,(
% 7.02/1.35 ~sQ2_spl|~sQ375_spl),
% 7.02/1.35 inference(contradiction_clause,[status(thm)],[f3820])).
% 7.02/1.35 fof(f4144,plain,(
% 7.02/1.35 isCountable0(sdtlpdtrp0(xN,xm))),
% 7.02/1.35 inference(resolution,[status(thm)],[f401,f470])).
% 7.02/1.35 fof(f4148,plain,(
% 7.02/1.35 isCountable0(slcrc0)|~sQ92_spl),
% 7.02/1.35 inference(forward_demodulation,[status(thm)],[f1016,f4144])).
% 7.02/1.35 fof(f4149,plain,(
% 7.02/1.35 $false|~sQ92_spl),
% 7.02/1.35 inference(forward_subsumption_resolution,[status(thm)],[f4148,f815])).
% 7.02/1.35 fof(f4150,plain,(
% 7.02/1.35 ~sQ92_spl),
% 7.02/1.35 inference(contradiction_clause,[status(thm)],[f4149])).
% 7.02/1.35 fof(f4151,plain,(
% 7.02/1.35 $false),
% 7.02/1.35 inference(sat_refutation,[status(thm)],[f535,f1123,f1219,f2891,f3821,f4150])).
% 7.02/1.35 % SZS output end CNFRefutation for theBenchmark.p
% 7.02/1.37 % Elapsed time: 0.980537 seconds
% 7.02/1.37 % CPU time: 7.307929 seconds
% 7.02/1.37 % Total memory used: 178.590 MB
% 7.02/1.37 % Net memory used: 173.875 MB
%------------------------------------------------------------------------------