%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM560+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 : n003.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:12 PM UTC 2026
% Result : Theorem 1.21s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM560+1 : 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.06/0.34 % Computer : n003.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Mon Sep 21 02:42:02 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.06/0.36 % Drodi V4.1.1
% 1.21/0.62 % Refutation found
% 1.21/0.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.21/0.62 % SZS output start CNFRefutation for theBenchmark
% 1.21/0.62 fof(f10,definition,(
% 1.21/0.62 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 1.21/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.21/0.62 fof(f64,axiom,(
% 1.21/0.62 (! [W0] :( aFunction0(W0)=> aSet0(szDzozmdt0(W0)) ) )),
% 1.21/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.21/0.62 fof(f66,definition,(
% 1.21/0.62 (! [W0,W1] :( ( aFunction0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtlbdtrb0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElementOf0(W3,szDzozmdt0(W0))& sdtlpdtrp0(W0,W3) = W1 ) ) )) ) )) )),
% 1.21/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.21/0.62 fof(f67,hypothesis,(
% 1.21/0.62 ( aFunction0(xF)& aElement0(xy) ) ),
% 1.21/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.21/0.62 fof(f68,conjecture,(
% 1.21/0.62 aSubsetOf0(sdtlbdtrb0(xF,xy),szDzozmdt0(xF)) ),
% 1.21/0.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.21/0.62 fof(f69,negated_conjecture,(
% 1.21/0.62 ~(aSubsetOf0(sdtlbdtrb0(xF,xy),szDzozmdt0(xF)) )),
% 1.21/0.62 inference(negated_conjecture,[status(cth)],[f68])).
% 1.21/0.62 fof(f94,plain,(
% 1.21/0.62 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 1.21/0.62 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 1.21/0.62 fof(f95,plain,(
% 1.21/0.62 ![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))))))))),
% 1.21/0.62 inference(NNF_transformation,[status(thm)],[f94])).
% 1.21/0.62 fof(f96,plain,(
% 1.21/0.62 ![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))))))))),
% 1.21/0.62 inference(miniscoping,[status(thm)],[f95])).
% 1.21/0.62 fof(f97,plain,(
% 1.21/0.62 ![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)))))))),
% 1.21/0.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f96])).
% 1.21/0.62 fof(f100,plain,(
% 1.21/0.62 ![X0,X1]: (~aSet0(X0)|aSubsetOf0(X1,X0)|~aSet0(X1)|aElementOf0(sK1_skl(X1,X0),X1))),
% 1.21/0.62 inference(cnf_transformation,[status(thm)],[f97])).
% 1.21/0.62 fof(f101,plain,(
% 1.21/0.62 ![X0,X1]: (~aSet0(X0)|aSubsetOf0(X1,X0)|~aSet0(X1)|~aElementOf0(sK1_skl(X1,X0),X0))),
% 1.21/0.62 inference(cnf_transformation,[status(thm)],[f97])).
% 1.21/0.62 fof(f278,plain,(
% 1.21/0.62 ![W0]: (~aFunction0(W0)|aSet0(szDzozmdt0(W0)))),
% 1.21/0.62 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 1.21/0.62 fof(f279,plain,(
% 1.21/0.62 ![X0]: (~aFunction0(X0)|aSet0(szDzozmdt0(X0)))),
% 1.21/0.62 inference(cnf_transformation,[status(thm)],[f278])).
% 1.21/0.62 fof(f282,plain,(
% 1.21/0.62 ![W0,W1]: ((~aFunction0(W0)|~aElement0(W1))|(![W2]: (W2=sdtlbdtrb0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aElementOf0(W3,szDzozmdt0(W0))&sdtlpdtrp0(W0,W3)=W1)))))))),
% 1.21/0.62 inference(pre_NNF_transformation,[status(thm)],[f66])).
% 1.21/0.62 fof(f283,plain,(
% 1.21/0.62 ![W0,W1]: ((~aFunction0(W0)|~aElement0(W1))|(![W2]: ((~W2=sdtlbdtrb0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aElementOf0(W3,szDzozmdt0(W0))&sdtlpdtrp0(W0,W3)=W1))&(aElementOf0(W3,W2)|(~aElementOf0(W3,szDzozmdt0(W0))|~sdtlpdtrp0(W0,W3)=W1))))))&(W2=sdtlbdtrb0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElementOf0(W3,szDzozmdt0(W0))|~sdtlpdtrp0(W0,W3)=W1))&(aElementOf0(W3,W2)|(aElementOf0(W3,szDzozmdt0(W0))&sdtlpdtrp0(W0,W3)=W1)))))))))),
% 1.21/0.62 inference(NNF_transformation,[status(thm)],[f282])).
% 1.21/0.62 fof(f284,plain,(
% 1.21/0.62 ![W0,W1]: ((~aFunction0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtlbdtrb0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElementOf0(W3,szDzozmdt0(W0))&sdtlpdtrp0(W0,W3)=W1)))&(![W3]: (aElementOf0(W3,W2)|(~aElementOf0(W3,szDzozmdt0(W0))|~sdtlpdtrp0(W0,W3)=W1)))))))&(![W2]: (W2=sdtlbdtrb0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElementOf0(W3,szDzozmdt0(W0))|~sdtlpdtrp0(W0,W3)=W1))&(aElementOf0(W3,W2)|(aElementOf0(W3,szDzozmdt0(W0))&sdtlpdtrp0(W0,W3)=W1)))))))))),
% 1.21/0.62 inference(miniscoping,[status(thm)],[f283])).
% 1.21/0.63 fof(f285,plain,(
% 1.21/0.63 ![W0,W1]: ((~aFunction0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtlbdtrb0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElementOf0(W3,szDzozmdt0(W0))&sdtlpdtrp0(W0,W3)=W1)))&(![W3]: (aElementOf0(W3,W2)|(~aElementOf0(W3,szDzozmdt0(W0))|~sdtlpdtrp0(W0,W3)=W1)))))))&(![W2]: (W2=sdtlbdtrb0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK12_skl(W2,W1,W0),W2)|(~aElementOf0(sK12_skl(W2,W1,W0),szDzozmdt0(W0))|~sdtlpdtrp0(W0,sK12_skl(W2,W1,W0))=W1))&(aElementOf0(sK12_skl(W2,W1,W0),W2)|(aElementOf0(sK12_skl(W2,W1,W0),szDzozmdt0(W0))&sdtlpdtrp0(W0,sK12_skl(W2,W1,W0))=W1))))))))),
% 1.21/0.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(W3,sK12_skl(W2,W1,W0))],[f284])).
% 1.21/0.63 fof(f286,plain,(
% 1.21/0.63 ![X0,X1,X2]: (~aFunction0(X0)|~aElement0(X1)|~X2=sdtlbdtrb0(X0,X1)|aSet0(X2))),
% 1.21/0.63 inference(cnf_transformation,[status(thm)],[f285])).
% 1.21/0.63 fof(f287,plain,(
% 1.21/0.63 ![X0,X1,X2,X3]: (~aFunction0(X0)|~aElement0(X1)|~X2=sdtlbdtrb0(X0,X1)|~aElementOf0(X3,X2)|aElementOf0(X3,szDzozmdt0(X0)))),
% 1.21/0.63 inference(cnf_transformation,[status(thm)],[f285])).
% 1.21/0.63 fof(f293,plain,(
% 1.21/0.63 aFunction0(xF)),
% 1.21/0.63 inference(cnf_transformation,[status(thm)],[f67])).
% 1.21/0.63 fof(f294,plain,(
% 1.21/0.63 aElement0(xy)),
% 1.21/0.63 inference(cnf_transformation,[status(thm)],[f67])).
% 1.21/0.63 fof(f295,plain,(
% 1.21/0.63 ~aSubsetOf0(sdtlbdtrb0(xF,xy),szDzozmdt0(xF))),
% 1.21/0.63 inference(cnf_transformation,[status(thm)],[f69])).
% 1.21/0.63 fof(f307,plain,(
% 1.21/0.63 aSet0(szDzozmdt0(xF))),
% 1.21/0.63 inference(resolution,[status(thm)],[f279,f293])).
% 1.21/0.63 fof(f310,plain,(
% 1.21/0.63 ![X0,X1]: (~aElement0(X0)|~X1=sdtlbdtrb0(xF,X0)|aSet0(X1))),
% 1.21/0.63 inference(resolution,[status(thm)],[f286,f293])).
% 1.21/0.63 fof(f311,plain,(
% 1.21/0.63 ![X0]: (~X0=sdtlbdtrb0(xF,xy)|aSet0(X0))),
% 1.21/0.63 inference(resolution,[status(thm)],[f310,f294])).
% 1.21/0.63 fof(f312,plain,(
% 1.21/0.63 aSet0(sdtlbdtrb0(xF,xy))),
% 1.21/0.63 inference(equality_resolution,[status(thm)],[f311])).
% 1.21/0.63 fof(f323,plain,(
% 1.21/0.63 ![X0,X1,X2]: (~aElement0(X0)|~X1=sdtlbdtrb0(xF,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,szDzozmdt0(xF)))),
% 1.21/0.63 inference(resolution,[status(thm)],[f287,f293])).
% 1.21/0.63 fof(f324,plain,(
% 1.21/0.63 ![X0,X1]: (~X0=sdtlbdtrb0(xF,xy)|~aElementOf0(X1,X0)|aElementOf0(X1,szDzozmdt0(xF)))),
% 1.21/0.63 inference(resolution,[status(thm)],[f323,f294])).
% 1.21/0.63 fof(f468,plain,(
% 1.21/0.63 ![X0]: (aSubsetOf0(X0,szDzozmdt0(xF))|~aSet0(X0)|aElementOf0(sK1_skl(X0,szDzozmdt0(xF)),X0))),
% 1.21/0.63 inference(resolution,[status(thm)],[f100,f307])).
% 1.21/0.63 fof(f551,plain,(
% 1.21/0.63 aSubsetOf0(sdtlbdtrb0(xF,xy),szDzozmdt0(xF))|aElementOf0(sK1_skl(sdtlbdtrb0(xF,xy),szDzozmdt0(xF)),sdtlbdtrb0(xF,xy))),
% 1.21/0.63 inference(resolution,[status(thm)],[f468,f312])).
% 1.21/0.63 fof(f553,plain,(
% 1.21/0.63 aElementOf0(sK1_skl(sdtlbdtrb0(xF,xy),szDzozmdt0(xF)),sdtlbdtrb0(xF,xy))),
% 1.21/0.63 inference(forward_subsumption_resolution,[status(thm)],[f551,f295])).
% 1.21/0.63 fof(f679,plain,(
% 1.21/0.63 ~sdtlbdtrb0(xF,xy)=sdtlbdtrb0(xF,xy)|aElementOf0(sK1_skl(sdtlbdtrb0(xF,xy),szDzozmdt0(xF)),szDzozmdt0(xF))),
% 1.21/0.63 inference(resolution,[status(thm)],[f553,f324])).
% 1.21/0.63 fof(f681,plain,(
% 1.21/0.63 aElementOf0(sK1_skl(sdtlbdtrb0(xF,xy),szDzozmdt0(xF)),szDzozmdt0(xF))),
% 1.21/0.63 inference(trivial_equality_resolution,[status(thm)],[f679])).
% 1.21/0.63 fof(f685,plain,(
% 1.21/0.63 ~aSet0(szDzozmdt0(xF))|aSubsetOf0(sdtlbdtrb0(xF,xy),szDzozmdt0(xF))|~aSet0(sdtlbdtrb0(xF,xy))),
% 1.21/0.63 inference(resolution,[status(thm)],[f681,f101])).
% 1.21/0.63 fof(f691,plain,(
% 1.21/0.63 aSubsetOf0(sdtlbdtrb0(xF,xy),szDzozmdt0(xF))|~aSet0(sdtlbdtrb0(xF,xy))),
% 1.21/0.63 inference(forward_subsumption_resolution,[status(thm)],[f685,f307])).
% 1.21/0.63 fof(f1713,plain,(
% 1.21/0.63 ~aSet0(sdtlbdtrb0(xF,xy))),
% 1.21/0.63 inference(forward_subsumption_resolution,[status(thm)],[f691,f295])).
% 1.21/0.63 fof(f1714,plain,(
% 1.21/0.63 $false),
% 1.21/0.63 inference(backward_subsumption_resolution,[status(thm)],[f312,f1713])).
% 1.21/0.63 % SZS output end CNFRefutation for theBenchmark.p
% 1.21/0.63 % Elapsed time: 0.276764 seconds
% 1.21/0.63 % CPU time: 1.825296 seconds
% 1.21/0.63 % Total memory used: 138.755 MB
% 1.21/0.63 % Net memory used: 136.430 MB
%------------------------------------------------------------------------------