%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM539+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 : n013.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 0.19s 15.75s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM539+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/15.63 % Computer : n013.cluster.edu
% 0.16/15.63 % Model : x86_64 x86_64
% 0.16/15.63 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/15.63 % Memory : 8046.5625MB
% 0.16/15.63 % OS : Linux 6.8.0-71-generic
% 0.16/15.63 % CPULimit : 300
% 0.16/15.63 % WCLimit : 300
% 0.16/15.63 % DateTime : Mon Sep 21 02:38:23 UTC 2026
% 0.16/15.64 % CPUTime :
% 0.16/15.65 % Drodi V4.1.1
% 0.19/15.75 % Refutation found
% 0.19/15.75 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/15.75 % SZS output start CNFRefutation for theBenchmark
% 0.19/15.75 fof(f5,definition,(
% 0.19/15.75 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 0.19/15.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/15.75 fof(f10,definition,(
% 0.19/15.75 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 0.19/15.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/15.75 fof(f23,axiom,(
% 0.19/15.75 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 0.19/15.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/15.75 fof(f35,axiom,(
% 0.19/15.75 (! [W0,W1] :( ( aElementOf0(W0,szNzAzT0)& aElementOf0(W1,szNzAzT0) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W1,W0) )=> W0 = W1 ) ) )),
% 0.19/15.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/15.75 fof(f47,definition,(
% 0.19/15.75 (! [W0] :( ( aSubsetOf0(W0,szNzAzT0)& W0 != slcrc0 )=> (! [W1] :( W1 = szmzizndt0(W0)<=> ( aElementOf0(W1,W0)& (! [W2] :( aElementOf0(W2,W0)=> sdtlseqdt0(W1,W2) ) )) ) )) )),
% 0.19/15.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/15.75 fof(f49,hypothesis,(
% 0.19/15.75 ( aSubsetOf0(xS,szNzAzT0)& aSubsetOf0(xT,szNzAzT0)& xS != slcrc0& xT != slcrc0 ) ),
% 0.19/15.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/15.75 fof(f50,hypothesis,(
% 0.19/15.75 ( aElementOf0(szmzizndt0(xS),xT)& aElementOf0(szmzizndt0(xT),xS) ) ),
% 0.19/15.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/15.75 fof(f51,conjecture,(
% 0.19/15.75 szmzizndt0(xS) = szmzizndt0(xT) ),
% 0.19/15.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/15.75 fof(f52,negated_conjecture,(
% 0.19/15.75 ~(szmzizndt0(xS) = szmzizndt0(xT) )),
% 0.19/15.75 inference(negated_conjecture,[status(cth)],[f51])).
% 0.19/15.75 fof(f63,plain,(
% 0.19/15.75 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 0.19/15.75 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.19/15.75 fof(f64,plain,(
% 0.19/15.75 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.19/15.75 inference(NNF_transformation,[status(thm)],[f63])).
% 0.19/15.75 fof(f65,plain,(
% 0.19/15.75 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 0.19/15.75 inference(miniscoping,[status(thm)],[f64])).
% 0.19/15.75 fof(f66,plain,(
% 0.19/15.75 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 0.19/15.75 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f65])).
% 0.19/15.75 fof(f68,plain,(
% 0.19/15.75 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 0.19/15.75 inference(cnf_transformation,[status(thm)],[f66])).
% 0.19/15.75 fof(f77,plain,(
% 0.19/15.75 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 0.19/15.75 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.19/15.75 fof(f78,plain,(
% 0.19/15.75 ![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.19/15.75 inference(NNF_transformation,[status(thm)],[f77])).
% 0.19/15.75 fof(f79,plain,(
% 0.19/15.75 ![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.19/15.75 inference(miniscoping,[status(thm)],[f78])).
% 0.19/15.75 fof(f80,plain,(
% 0.19/15.75 ![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.19/15.75 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f79])).
% 0.19/15.75 fof(f82,plain,(
% 0.19/15.75 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 0.19/15.75 inference(cnf_transformation,[status(thm)],[f80])).
% 0.19/15.75 fof(f129,plain,(
% 0.19/15.75 aSet0(szNzAzT0)),
% 0.19/15.75 inference(cnf_transformation,[status(thm)],[f23])).
% 0.19/15.75 fof(f157,plain,(
% 0.19/15.75 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W0))|W0=W1))),
% 0.19/15.75 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.19/15.75 fof(f158,plain,(
% 0.19/15.75 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X1,X0)|X0=X1)),
% 0.19/15.75 inference(cnf_transformation,[status(thm)],[f157])).
% 0.19/15.75 fof(f187,plain,(
% 0.19/15.75 ![W0]: ((~aSubsetOf0(W0,szNzAzT0)|W0=slcrc0)|(![W1]: (W1=szmzizndt0(W0)<=>(aElementOf0(W1,W0)&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2)))))))),
% 0.19/15.75 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.19/15.75 fof(f188,plain,(
% 0.19/15.75 ![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))))))))),
% 0.19/15.75 inference(NNF_transformation,[status(thm)],[f187])).
% 0.19/15.75 fof(f189,plain,(
% 0.19/15.75 ![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))))))))),
% 0.19/15.75 inference(miniscoping,[status(thm)],[f188])).
% 0.19/15.75 fof(f190,plain,(
% 0.19/15.75 ![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))))))))),
% 0.19/15.75 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W2,sK6_skl(W1,W0))],[f189])).
% 0.19/15.75 fof(f191,plain,(
% 0.19/15.75 ![X0,X1]: (~aSubsetOf0(X0,szNzAzT0)|X0=slcrc0|~X1=szmzizndt0(X0)|aElementOf0(X1,X0))),
% 0.19/15.75 inference(cnf_transformation,[status(thm)],[f190])).
% 0.19/15.75 fof(f192,plain,(
% 0.19/15.75 ![X0,X1,X2]: (~aSubsetOf0(X0,szNzAzT0)|X0=slcrc0|~X1=szmzizndt0(X0)|~aElementOf0(X2,X0)|sdtlseqdt0(X1,X2))),
% 0.19/15.75 inference(cnf_transformation,[status(thm)],[f190])).
% 0.19/15.75 fof(f203,plain,(
% 0.19/15.75 aSubsetOf0(xS,szNzAzT0)),
% 0.19/15.75 inference(cnf_transformation,[status(thm)],[f49])).
% 0.19/15.75 fof(f204,plain,(
% 0.19/15.75 aSubsetOf0(xT,szNzAzT0)),
% 0.19/15.75 inference(cnf_transformation,[status(thm)],[f49])).
% 0.19/15.75 fof(f206,plain,(
% 0.19/15.75 ~xT=slcrc0),
% 0.19/15.75 inference(cnf_transformation,[status(thm)],[f49])).
% 0.19/15.75 fof(f207,plain,(
% 0.19/15.75 aElementOf0(szmzizndt0(xS),xT)),
% 0.19/15.75 inference(cnf_transformation,[status(thm)],[f50])).
% 0.19/15.75 fof(f208,plain,(
% 0.19/15.75 aElementOf0(szmzizndt0(xT),xS)),
% 0.19/15.75 inference(cnf_transformation,[status(thm)],[f50])).
% 0.19/15.75 fof(f209,plain,(
% 0.19/15.75 ~szmzizndt0(xS)=szmzizndt0(xT)),
% 0.19/15.75 inference(cnf_transformation,[status(thm)],[f52])).
% 0.19/15.75 fof(f226,plain,(
% 0.19/15.75 ![X0,X1,X2]: (~aSubsetOf0(X0,szNzAzT0)|~X1=szmzizndt0(X0)|~aElementOf0(X2,X0)|sdtlseqdt0(X1,X2))),
% 0.19/15.75 inference(forward_subsumption_resolution,[status(thm)],[f192,f68])).
% 0.19/15.75 fof(f233,plain,(
% 0.19/15.75 ![X0]: (~aSubsetOf0(X0,szNzAzT0)|X0=slcrc0|aElementOf0(szmzizndt0(X0),X0))),
% 0.19/15.75 inference(equality_resolution,[status(thm)],[f191])).
% 0.19/15.75 fof(f234,plain,(
% 0.19/15.75 xT=slcrc0|aElementOf0(szmzizndt0(xT),xT)),
% 0.19/15.75 inference(resolution,[status(thm)],[f233,f204])).
% 0.19/15.75 fof(f236,plain,(
% 0.19/15.75 aElementOf0(szmzizndt0(xT),xT)),
% 0.19/15.75 inference(forward_subsumption_resolution,[status(thm)],[f234,f206])).
% 0.19/15.75 fof(f238,plain,(
% 0.19/15.75 ![X0,X1]: (~aSubsetOf0(X0,szNzAzT0)|~aElementOf0(X1,X0)|sdtlseqdt0(szmzizndt0(X0),X1))),
% 0.19/15.75 inference(equality_resolution,[status(thm)],[f226])).
% 0.19/15.75 fof(f239,plain,(
% 0.19/15.75 ![X0]: (~aElementOf0(X0,xT)|sdtlseqdt0(szmzizndt0(xT),X0))),
% 0.19/15.75 inference(resolution,[status(thm)],[f238,f204])).
% 0.19/15.75 fof(f240,plain,(
% 0.19/15.75 ![X0]: (~aElementOf0(X0,xS)|sdtlseqdt0(szmzizndt0(xS),X0))),
% 0.19/15.75 inference(resolution,[status(thm)],[f238,f203])).
% 0.19/15.75 fof(f242,plain,(
% 0.19/15.75 sdtlseqdt0(szmzizndt0(xT),szmzizndt0(xS))),
% 0.19/15.75 inference(resolution,[status(thm)],[f239,f207])).
% 0.19/15.75 fof(f243,plain,(
% 0.19/15.75 sdtlseqdt0(szmzizndt0(xS),szmzizndt0(xT))),
% 0.19/15.75 inference(resolution,[status(thm)],[f240,f208])).
% 0.19/15.75 fof(f245,plain,(
% 0.19/15.75 ![X0]: (~aSet0(szNzAzT0)|~aElementOf0(X0,xT)|aElementOf0(X0,szNzAzT0))),
% 0.19/15.75 inference(resolution,[status(thm)],[f82,f204])).
% 0.19/15.75 fof(f247,plain,(
% 0.19/15.75 ![X0]: (~aElementOf0(X0,xT)|aElementOf0(X0,szNzAzT0))),
% 0.19/15.75 inference(forward_subsumption_resolution,[status(thm)],[f245,f129])).
% 0.19/15.75 fof(f249,plain,(
% 0.19/15.75 aElementOf0(szmzizndt0(xT),szNzAzT0)),
% 0.19/15.75 inference(resolution,[status(thm)],[f247,f236])).
% 0.19/15.75 fof(f250,plain,(
% 0.19/15.75 aElementOf0(szmzizndt0(xS),szNzAzT0)),
% 0.19/15.75 inference(resolution,[status(thm)],[f247,f207])).
% 0.19/15.76 fof(f269,plain,(
% 0.19/15.76 ~aElementOf0(szmzizndt0(xS),szNzAzT0)|~aElementOf0(szmzizndt0(xT),szNzAzT0)|~sdtlseqdt0(szmzizndt0(xT),szmzizndt0(xS))|szmzizndt0(xS)=szmzizndt0(xT)),
% 0.19/15.76 inference(resolution,[status(thm)],[f158,f243])).
% 0.19/15.76 fof(f278,plain,(
% 0.19/15.76 ~aElementOf0(szmzizndt0(xT),szNzAzT0)|~sdtlseqdt0(szmzizndt0(xT),szmzizndt0(xS))|szmzizndt0(xS)=szmzizndt0(xT)),
% 0.19/15.76 inference(forward_subsumption_resolution,[status(thm)],[f269,f250])).
% 0.19/15.76 fof(f284,plain,(
% 0.19/15.76 ~aElementOf0(szmzizndt0(xT),szNzAzT0)|szmzizndt0(xS)=szmzizndt0(xT)),
% 0.19/15.76 inference(resolution,[status(thm)],[f278,f242])).
% 0.19/15.76 fof(f295,plain,(
% 0.19/15.76 ~szmzizndt0(xS)=szmzizndt0(xS)),
% 0.19/15.76 inference(backward_demodulation,[status(thm)],[f297,f209])).
% 0.19/15.76 fof(f297,plain,(
% 0.19/15.76 szmzizndt0(xS)=szmzizndt0(xT)),
% 0.19/15.76 inference(forward_subsumption_resolution,[status(thm)],[f284,f249])).
% 0.19/15.76 fof(f301,plain,(
% 0.19/15.76 $false),
% 0.19/15.76 inference(trivial_equality_resolution,[status(thm)],[f295])).
% 0.19/15.76 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/15.76 % Elapsed time: 0.121083 seconds
% 0.19/15.76 % CPU time: 0.718628 seconds
% 0.19/15.76 % Total memory used: 96.340 MB
% 0.19/15.76 % Net memory used: 95.316 MB
%------------------------------------------------------------------------------