%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM565+3 : 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 : n014.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:13 PM UTC 2026
% Result : Theorem 0.16s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM565+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.41 % Computer : n014.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Mon Sep 21 02:40:05 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 0.16/0.49 % Refutation found
% 0.16/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.49 fof(f42,axiom,(
% 0.16/0.49 (! [W0] :( aSet0(W0)=> ( sbrdtbr0(W0) = sz00<=> W0 = slcrc0 ) ) )),
% 0.16/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f80,conjecture,(
% 0.16/0.49 (! [W0] :( ( aSet0(W0)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xS) ))& aSubsetOf0(W0,xS)& sbrdtbr0(W0) = sz00& aElementOf0(W0,slbdtsldtrb0(xS,sz00)) )=> ( ( aSet0(slcrc0)& ~ (? [W1] : aElementOf0(W1,slcrc0) ))=> sdtlpdtrp0(xc,W0) = sdtlpdtrp0(xc,slcrc0) ) ) )),
% 0.16/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f81,negated_conjecture,(
% 0.16/0.49 ~((! [W0] :( ( aSet0(W0)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xS) ))& aSubsetOf0(W0,xS)& sbrdtbr0(W0) = sz00& aElementOf0(W0,slbdtsldtrb0(xS,sz00)) )=> ( ( aSet0(slcrc0)& ~ (? [W1] : aElementOf0(W1,slcrc0) ))=> sdtlpdtrp0(xc,W0) = sdtlpdtrp0(xc,slcrc0) ) ) ))),
% 0.16/0.49 inference(negated_conjecture,[status(cth)],[f80])).
% 0.16/0.49 fof(f202,plain,(
% 0.16/0.49 ![W0]: (~aSet0(W0)|(sbrdtbr0(W0)=sz00<=>W0=slcrc0))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.16/0.49 fof(f203,plain,(
% 0.16/0.49 ![W0]: (~aSet0(W0)|((~sbrdtbr0(W0)=sz00|W0=slcrc0)&(sbrdtbr0(W0)=sz00|~W0=slcrc0)))),
% 0.16/0.49 inference(NNF_transformation,[status(thm)],[f202])).
% 0.16/0.49 fof(f204,plain,(
% 0.16/0.49 ![X0]: (~aSet0(X0)|~sbrdtbr0(X0)=sz00|X0=slcrc0)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f203])).
% 0.16/0.49 fof(f381,plain,(
% 0.16/0.49 (?[W0]: (((((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&sbrdtbr0(W0)=sz00)&aElementOf0(W0,slbdtsldtrb0(xS,sz00)))&((aSet0(slcrc0)&(![W1]: ~aElementOf0(W1,slcrc0)))&~sdtlpdtrp0(xc,W0)=sdtlpdtrp0(xc,slcrc0))))),
% 0.16/0.49 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 0.16/0.49 fof(f382,plain,(
% 0.16/0.49 (((((aSet0(sK23_skl)&(![W1]: (~aElementOf0(W1,sK23_skl)|aElementOf0(W1,xS))))&aSubsetOf0(sK23_skl,xS))&sbrdtbr0(sK23_skl)=sz00)&aElementOf0(sK23_skl,slbdtsldtrb0(xS,sz00)))&((aSet0(slcrc0)&(![W1]: ~aElementOf0(W1,slcrc0)))&~sdtlpdtrp0(xc,sK23_skl)=sdtlpdtrp0(xc,slcrc0)))),
% 0.16/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(W0,sK23_skl)],[f381])).
% 0.16/0.49 fof(f383,plain,(
% 0.16/0.49 aSet0(sK23_skl)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f382])).
% 0.16/0.49 fof(f386,plain,(
% 0.16/0.49 sbrdtbr0(sK23_skl)=sz00),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f382])).
% 0.16/0.49 fof(f390,plain,(
% 0.16/0.49 ~sdtlpdtrp0(xc,sK23_skl)=sdtlpdtrp0(xc,slcrc0)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f382])).
% 0.16/0.49 fof(f581,plain,(
% 0.16/0.49 ~sbrdtbr0(sK23_skl)=sz00|sK23_skl=slcrc0),
% 0.16/0.49 inference(resolution,[status(thm)],[f204,f383])).
% 0.16/0.49 fof(f582,plain,(
% 0.16/0.49 ~sz00=sz00|sK23_skl=slcrc0),
% 0.16/0.49 inference(forward_demodulation,[status(thm)],[f386,f581])).
% 0.16/0.49 fof(f583,plain,(
% 0.16/0.49 sK23_skl=slcrc0),
% 0.16/0.49 inference(trivial_equality_resolution,[status(thm)],[f582])).
% 0.16/0.49 fof(f597,plain,(
% 0.16/0.49 ~sdtlpdtrp0(xc,sK23_skl)=sdtlpdtrp0(xc,sK23_skl)),
% 0.16/0.49 inference(backward_demodulation,[status(thm)],[f583,f390])).
% 0.16/0.49 fof(f603,plain,(
% 0.16/0.49 $false),
% 0.16/0.49 inference(trivial_equality_resolution,[status(thm)],[f597])).
% 0.16/0.49 % SZS output end CNFRefutation for theBenchmark.p
% 0.26/0.53 % Elapsed time: 0.095524 seconds
% 0.26/0.53 % CPU time: 0.253142 seconds
% 0.26/0.53 % Total memory used: 112.810 MB
% 0.26/0.53 % Net memory used: 112.609 MB
%------------------------------------------------------------------------------