%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM538+1 : 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 : n020.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:09 PM UTC 2026
% Result : Theorem 27.90s 4.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM538+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n020.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 02:39:33 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 27.90/4.01 % Refutation found
% 27.90/4.01 % SZS status Theorem for theBenchmark: Theorem is valid
% 27.90/4.01 % SZS output start CNFRefutation for theBenchmark
% 27.90/4.01 fof(f3,axiom,(
% 27.90/4.01 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 27.90/4.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.90/4.01 fof(f16,definition,(
% 27.90/4.01 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtmndt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& aElementOf0(W3,W0)& W3 != W1 ) ) )) ) )) )),
% 27.90/4.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.90/4.01 fof(f17,axiom,(
% 27.90/4.01 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> sdtpldt0(sdtmndt0(W0,W1),W1) = W0 ) )) )),
% 27.90/4.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.90/4.01 fof(f22,axiom,(
% 27.90/4.01 (! [W0] :( aElement0(W0)=> (! [W1] :( ( aSet0(W1)& isFinite0(W1) )=> isFinite0(sdtmndt0(W1,W0)) ) )) )),
% 27.90/4.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.90/4.01 fof(f43,axiom,(
% 27.90/4.01 (! [W0] :( ( aSet0(W0)& isFinite0(W0) )=> (! [W1] :( aElement0(W1)=> ( ~ aElementOf0(W1,W0)=> sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) )) )),
% 27.90/4.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.90/4.01 fof(f44,hypothesis,(
% 27.90/4.01 aSet0(xS) ),
% 27.90/4.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.90/4.01 fof(f45,hypothesis,(
% 27.90/4.01 ( isFinite0(xS)& aElementOf0(xx,xS) ) ),
% 27.90/4.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.90/4.01 fof(f46,conjecture,(
% 27.90/4.01 szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))) = sbrdtbr0(xS) ),
% 27.90/4.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.90/4.01 fof(f47,negated_conjecture,(
% 27.90/4.01 ~(szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))) = sbrdtbr0(xS) )),
% 27.90/4.01 inference(negated_conjecture,[status(cth)],[f46])).
% 27.90/4.01 fof(f54,plain,(
% 27.90/4.01 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 27.90/4.01 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 27.90/4.01 fof(f55,plain,(
% 27.90/4.01 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 27.90/4.01 inference(cnf_transformation,[status(thm)],[f54])).
% 27.90/4.01 fof(f101,plain,(
% 27.90/4.01 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1)))))))),
% 27.90/4.01 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 27.90/4.01 fof(f102,definition,(
% 27.90/4.01 ![W0,W1,W3]: (sP0_prd(W3,W1,W0)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1))),
% 27.90/4.01 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 27.90/4.01 fof(f103,plain,(
% 27.90/4.01 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>sP0_prd(W3,W1,W0)))))))),
% 27.90/4.01 inference(formula_renaming,[status(thm)],[f101,f102])).
% 27.90/4.01 fof(f104,plain,(
% 27.90/4.01 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: ((~W2=sdtmndt0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|sP0_prd(W3,W1,W0))&(aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0))))))&(W2=sdtmndt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0))&(aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))))))))),
% 27.90/4.01 inference(NNF_transformation,[status(thm)],[f103])).
% 27.90/4.01 fof(f105,plain,(
% 27.90/4.01 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtmndt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))&(![W3]: (aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0)))))))&(![W2]: (W2=sdtmndt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0))&(aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))))))))),
% 27.90/4.01 inference(miniscoping,[status(thm)],[f104])).
% 27.90/4.01 fof(f106,plain,(
% 27.90/4.01 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtmndt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))&(![W3]: (aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0)))))))&(![W2]: (W2=sdtmndt0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK3_skl(W2,W1,W0),W2)|~sP0_prd(sK3_skl(W2,W1,W0),W1,W0))&(aElementOf0(sK3_skl(W2,W1,W0),W2)|sP0_prd(sK3_skl(W2,W1,W0),W1,W0))))))))),
% 27.90/4.01 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(W3,sK3_skl(W2,W1,W0))],[f105])).
% 27.90/4.01 fof(f107,plain,(
% 27.90/4.01 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtmndt0(X0,X1)|aSet0(X2))),
% 27.90/4.01 inference(cnf_transformation,[status(thm)],[f106])).
% 27.90/4.01 fof(f108,plain,(
% 27.90/4.01 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtmndt0(X0,X1)|~aElementOf0(X3,X2)|sP0_prd(X3,X1,X0))),
% 27.90/4.01 inference(cnf_transformation,[status(thm)],[f106])).
% 27.90/4.01 fof(f112,plain,(
% 27.90/4.01 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|sdtpldt0(sdtmndt0(W0,W1),W1)=W0)))),
% 27.90/4.01 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 27.90/4.01 fof(f113,plain,(
% 27.90/4.01 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|sdtpldt0(sdtmndt0(X0,X1),X1)=X0)),
% 27.90/4.01 inference(cnf_transformation,[status(thm)],[f112])).
% 27.90/4.01 fof(f122,plain,(
% 27.90/4.01 ![W0]: (~aElement0(W0)|(![W1]: ((~aSet0(W1)|~isFinite0(W1))|isFinite0(sdtmndt0(W1,W0)))))),
% 27.90/4.01 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 27.90/4.01 fof(f123,plain,(
% 27.90/4.01 ![X0,X1]: (~aElement0(X0)|~aSet0(X1)|~isFinite0(X1)|isFinite0(sdtmndt0(X1,X0)))),
% 27.90/4.01 inference(cnf_transformation,[status(thm)],[f122])).
% 27.90/4.01 fof(f172,plain,(
% 27.90/4.01 ![W0]: ((~aSet0(W0)|~isFinite0(W0))|(![W1]: (~aElement0(W1)|(aElementOf0(W1,W0)|sbrdtbr0(sdtpldt0(W0,W1))=szszuzczcdt0(sbrdtbr0(W0))))))),
% 27.90/4.01 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 27.90/4.01 fof(f173,plain,(
% 27.90/4.01 ![X0,X1]: (~aSet0(X0)|~isFinite0(X0)|~aElement0(X1)|aElementOf0(X1,X0)|sbrdtbr0(sdtpldt0(X0,X1))=szszuzczcdt0(sbrdtbr0(X0)))),
% 27.90/4.01 inference(cnf_transformation,[status(thm)],[f172])).
% 27.90/4.01 fof(f174,plain,(
% 27.90/4.01 aSet0(xS)),
% 27.90/4.01 inference(cnf_transformation,[status(thm)],[f44])).
% 27.90/4.01 fof(f175,plain,(
% 27.90/4.01 isFinite0(xS)),
% 27.90/4.01 inference(cnf_transformation,[status(thm)],[f45])).
% 27.90/4.01 fof(f176,plain,(
% 27.90/4.01 aElementOf0(xx,xS)),
% 27.90/4.01 inference(cnf_transformation,[status(thm)],[f45])).
% 27.90/4.01 fof(f177,plain,(
% 27.90/4.01 ~szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx)))=sbrdtbr0(xS)),
% 27.90/4.01 inference(cnf_transformation,[status(thm)],[f47])).
% 27.90/4.01 fof(f178,plain,(
% 27.90/4.01 ![W0,W1,W3]: ((~sP0_prd(W3,W1,W0)|((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1))&(sP0_prd(W3,W1,W0)|((~aElement0(W3)|~aElementOf0(W3,W0))|W3=W1)))),
% 27.90/4.01 inference(NNF_transformation,[status(thm)],[f102])).
% 27.90/4.01 fof(f179,plain,(
% 27.90/4.01 (![W0,W1,W3]: (~sP0_prd(W3,W1,W0)|((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1)))&(![W0,W1,W3]: (sP0_prd(W3,W1,W0)|((~aElement0(W3)|~aElementOf0(W3,W0))|W3=W1)))),
% 27.90/4.01 inference(miniscoping,[status(thm)],[f178])).
% 27.90/4.01 fof(f182,plain,(
% 27.90/4.01 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|~X0=X1)),
% 27.90/4.01 inference(cnf_transformation,[status(thm)],[f179])).
% 27.90/4.01 fof(f193,plain,(
% 27.90/4.01 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aSet0(sdtmndt0(X0,X1)))),
% 27.90/4.01 inference(destructive_equality_resolution,[status(thm)],[f107])).
% 27.90/4.01 fof(f194,plain,(
% 27.90/4.01 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~aElementOf0(X2,sdtmndt0(X0,X1))|sP0_prd(X2,X1,X0))),
% 27.90/4.01 inference(destructive_equality_resolution,[status(thm)],[f108])).
% 27.90/4.01 fof(f197,plain,(
% 27.90/4.01 ![X0,X1]: (~sP0_prd(X0,X0,X1))),
% 27.90/4.01 inference(destructive_equality_resolution,[status(thm)],[f182])).
% 27.90/4.01 fof(f199,plain,(
% 27.90/4.01 ![X0]: (~aElement0(X0)|aSet0(sdtmndt0(xS,X0)))),
% 27.90/4.01 inference(resolution,[status(thm)],[f193,f174])).
% 27.90/4.01 fof(f212,plain,(
% 27.90/4.01 ~aSet0(xS)|sdtpldt0(sdtmndt0(xS,xx),xx)=xS),
% 27.90/4.01 inference(resolution,[status(thm)],[f113,f176])).
% 27.90/4.01 fof(f213,plain,(
% 27.90/4.01 sdtpldt0(sdtmndt0(xS,xx),xx)=xS),
% 27.90/4.01 inference(forward_subsumption_resolution,[status(thm)],[f212,f174])).
% 27.90/4.01 fof(f237,plain,(
% 27.90/4.01 ~aSet0(xS)|aElement0(xx)),
% 27.90/4.01 inference(resolution,[status(thm)],[f55,f176])).
% 27.90/4.01 fof(f240,plain,(
% 27.90/4.01 aElement0(xx)),
% 27.90/4.01 inference(forward_subsumption_resolution,[status(thm)],[f237,f174])).
% 27.90/4.01 fof(f252,plain,(
% 27.90/4.01 aSet0(sdtmndt0(xS,xx))),
% 27.90/4.01 inference(resolution,[status(thm)],[f240,f199])).
% 27.90/4.01 fof(f264,plain,(
% 27.90/4.01 ![X0]: (~aSet0(X0)|~isFinite0(X0)|isFinite0(sdtmndt0(X0,xx)))),
% 27.90/4.01 inference(resolution,[status(thm)],[f123,f240])).
% 27.90/4.01 fof(f335,plain,(
% 27.90/4.01 ![X0]: (~isFinite0(sdtmndt0(xS,xx))|~aElement0(X0)|aElementOf0(X0,sdtmndt0(xS,xx))|sbrdtbr0(sdtpldt0(sdtmndt0(xS,xx),X0))=szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))))),
% 27.90/4.01 inference(resolution,[status(thm)],[f173,f252])).
% 27.90/4.01 fof(f1415,plain,(
% 27.90/4.01 ~isFinite0(xS)|isFinite0(sdtmndt0(xS,xx))),
% 27.90/4.01 inference(resolution,[status(thm)],[f264,f174])).
% 27.90/4.01 fof(f1417,plain,(
% 27.90/4.01 isFinite0(sdtmndt0(xS,xx))),
% 27.90/4.01 inference(forward_subsumption_resolution,[status(thm)],[f1415,f175])).
% 27.90/4.01 fof(f43812,plain,(
% 27.90/4.01 ![X0]: (~aElement0(X0)|aElementOf0(X0,sdtmndt0(xS,xx))|sbrdtbr0(sdtpldt0(sdtmndt0(xS,xx),X0))=szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))))),
% 27.90/4.01 inference(forward_subsumption_resolution,[status(thm)],[f335,f1417])).
% 27.90/4.01 fof(f43833,plain,(
% 27.90/4.01 aElementOf0(xx,sdtmndt0(xS,xx))|sbrdtbr0(sdtpldt0(sdtmndt0(xS,xx),xx))=szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx)))),
% 28.63/4.05 inference(resolution,[status(thm)],[f43812,f240])).
% 28.63/4.05 fof(f43915,plain,(
% 28.63/4.05 aElementOf0(xx,sdtmndt0(xS,xx))|sbrdtbr0(xS)=szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx)))),
% 28.63/4.05 inference(forward_demodulation,[status(thm)],[f213,f43833])).
% 28.63/4.05 fof(f43916,plain,(
% 28.63/4.05 aElementOf0(xx,sdtmndt0(xS,xx))),
% 28.63/4.05 inference(forward_subsumption_resolution,[status(thm)],[f43915,f177])).
% 28.63/4.05 fof(f43917,plain,(
% 28.63/4.05 ~aSet0(xS)|~aElement0(xx)|sP0_prd(xx,xx,xS)),
% 28.63/4.05 inference(resolution,[status(thm)],[f43916,f194])).
% 28.63/4.05 fof(f43926,plain,(
% 28.63/4.05 ~aElement0(xx)|sP0_prd(xx,xx,xS)),
% 28.63/4.05 inference(forward_subsumption_resolution,[status(thm)],[f43917,f174])).
% 28.63/4.05 fof(f43933,plain,(
% 28.63/4.05 sP0_prd(xx,xx,xS)),
% 28.63/4.05 inference(forward_subsumption_resolution,[status(thm)],[f43926,f240])).
% 28.63/4.05 fof(f43937,plain,(
% 28.63/4.05 $false),
% 28.63/4.05 inference(resolution,[status(thm)],[f43933,f197])).
% 28.63/4.05 % SZS output end CNFRefutation for theBenchmark.p
% 28.63/4.06 % Elapsed time: 3.700382 seconds
% 28.63/4.06 % CPU time: 29.020526 seconds
% 28.63/4.06 % Total memory used: 335.004 MB
% 28.63/4.06 % Net memory used: 311.325 MB
%------------------------------------------------------------------------------