%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM494+3 : 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 : n010.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:02 PM UTC 2026
% Result : Theorem 14.34s 2.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM494+3 : 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.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 02:35:25 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 14.34/2.45 % Refutation found
% 14.34/2.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 14.34/2.45 % SZS output start CNFRefutation for theBenchmark
% 14.34/2.45 fof(f4,axiom,(
% 14.34/2.45 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtpldt0(W0,W1)) ) )),
% 14.34/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.34/2.45 fof(f14,axiom,(
% 14.34/2.45 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2)| sdtpldt0(W1,W0) = sdtpldt0(W2,W0) )=> W1 = W2 ) ) )),
% 14.34/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.34/2.45 fof(f24,axiom,(
% 14.34/2.45 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( ( W0 != W1& sdtlseqdt0(W0,W1) )=> (! [W2] :( aNaturalNumber0(W2)=> ( sdtpldt0(W2,W0) != sdtpldt0(W2,W1)& sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1))& sdtpldt0(W0,W2) != sdtpldt0(W1,W2)& sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2)) ) ) )) ) )),
% 14.34/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.34/2.45 fof(f39,hypothesis,(
% 14.34/2.45 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp) ) ),
% 14.34/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.34/2.45 fof(f43,hypothesis,(
% 14.34/2.45 ( aNaturalNumber0(xr)& sdtpldt0(xp,xr) = xn& xr = sdtmndt0(xn,xp) ) ),
% 14.34/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.34/2.45 fof(f44,hypothesis,(
% 14.34/2.45 ( xr != xn& (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xr,W0) = xn ))& sdtlseqdt0(xr,xn) ) ),
% 14.34/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.34/2.45 fof(f46,conjecture,(
% 14.34/2.45 ( sdtpldt0(sdtpldt0(xr,xm),xp) != sdtpldt0(sdtpldt0(xn,xm),xp)& ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(sdtpldt0(sdtpldt0(xr,xm),xp),W0) = sdtpldt0(sdtpldt0(xn,xm),xp) ))| sdtlseqdt0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp)) ) ) ),
% 14.34/2.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.34/2.45 fof(f47,negated_conjecture,(
% 14.34/2.45 ~(( sdtpldt0(sdtpldt0(xr,xm),xp) != sdtpldt0(sdtpldt0(xn,xm),xp)& ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(sdtpldt0(sdtpldt0(xr,xm),xp),W0) = sdtpldt0(sdtpldt0(xn,xm),xp) ))| sdtlseqdt0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp)) ) ) )),
% 14.34/2.45 inference(negated_conjecture,[status(cth)],[f46])).
% 14.34/2.45 fof(f54,plain,(
% 14.34/2.45 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtpldt0(W0,W1)))),
% 14.34/2.45 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 14.34/2.45 fof(f55,plain,(
% 14.34/2.45 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtpldt0(X0,X1)))),
% 14.34/2.45 inference(cnf_transformation,[status(thm)],[f54])).
% 14.34/2.45 fof(f78,plain,(
% 14.34/2.45 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|((~sdtpldt0(W0,W1)=sdtpldt0(W0,W2)&~sdtpldt0(W1,W0)=sdtpldt0(W2,W0))|W1=W2))),
% 14.34/2.45 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 14.34/2.45 fof(f80,plain,(
% 14.34/2.45 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtpldt0(X1,X0)=sdtpldt0(X2,X0)|X1=X2)),
% 14.34/2.45 inference(cnf_transformation,[status(thm)],[f78])).
% 14.34/2.45 fof(f110,plain,(
% 14.34/2.45 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((W0=W1|~sdtlseqdt0(W0,W1))|(![W2]: (~aNaturalNumber0(W2)|(((~sdtpldt0(W2,W0)=sdtpldt0(W2,W1)&sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1)))&~sdtpldt0(W0,W2)=sdtpldt0(W1,W2))&sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2)))))))),
% 14.34/2.45 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 14.34/2.45 fof(f114,plain,(
% 14.34/2.45 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=X1|~sdtlseqdt0(X0,X1)|~aNaturalNumber0(X2)|sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2)))),
% 14.34/2.45 inference(cnf_transformation,[status(thm)],[f110])).
% 14.34/2.45 fof(f166,plain,(
% 14.34/2.45 aNaturalNumber0(xn)),
% 14.34/2.45 inference(cnf_transformation,[status(thm)],[f39])).
% 14.34/2.45 fof(f167,plain,(
% 14.34/2.45 aNaturalNumber0(xm)),
% 14.34/2.45 inference(cnf_transformation,[status(thm)],[f39])).
% 14.34/2.45 fof(f168,plain,(
% 14.34/2.45 aNaturalNumber0(xp)),
% 14.34/2.45 inference(cnf_transformation,[status(thm)],[f39])).
% 14.34/2.45 fof(f194,plain,(
% 14.34/2.45 aNaturalNumber0(xr)),
% 14.34/2.45 inference(cnf_transformation,[status(thm)],[f43])).
% 14.34/2.45 fof(f197,plain,(
% 14.34/2.45 (~xr=xn&(aNaturalNumber0(sK7_skl)&sdtpldt0(xr,sK7_skl)=xn))&sdtlseqdt0(xr,xn)),
% 14.34/2.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(W0,sK7_skl)],[f44])).
% 14.34/2.45 fof(f198,plain,(
% 14.34/2.45 ~xr=xn),
% 14.34/2.45 inference(cnf_transformation,[status(thm)],[f197])).
% 14.80/2.47 fof(f201,plain,(
% 14.80/2.47 sdtlseqdt0(xr,xn)),
% 14.80/2.47 inference(cnf_transformation,[status(thm)],[f197])).
% 14.80/2.47 fof(f206,plain,(
% 14.80/2.47 (sdtpldt0(sdtpldt0(xr,xm),xp)=sdtpldt0(sdtpldt0(xn,xm),xp)|((![W0]: (~aNaturalNumber0(W0)|~sdtpldt0(sdtpldt0(sdtpldt0(xr,xm),xp),W0)=sdtpldt0(sdtpldt0(xn,xm),xp)))&~sdtlseqdt0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))))),
% 14.80/2.47 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 14.80/2.47 fof(f208,plain,(
% 14.80/2.47 sdtpldt0(sdtpldt0(xr,xm),xp)=sdtpldt0(sdtpldt0(xn,xm),xp)|~sdtlseqdt0(sdtpldt0(sdtpldt0(xr,xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp))),
% 14.80/2.47 inference(cnf_transformation,[status(thm)],[f206])).
% 14.80/2.47 fof(f813,plain,(
% 14.80/2.47 ~aNaturalNumber0(sdtpldt0(xr,xm))|~aNaturalNumber0(sdtpldt0(xn,xm))|sdtpldt0(xr,xm)=sdtpldt0(xn,xm)|~sdtlseqdt0(sdtpldt0(xr,xm),sdtpldt0(xn,xm))|~aNaturalNumber0(xp)|sdtpldt0(sdtpldt0(xr,xm),xp)=sdtpldt0(sdtpldt0(xn,xm),xp)),
% 14.80/2.47 inference(resolution,[status(thm)],[f114,f208])).
% 14.80/2.47 fof(f819,plain,(
% 14.80/2.47 ~aNaturalNumber0(sdtpldt0(xr,xm))|~aNaturalNumber0(sdtpldt0(xn,xm))|sdtpldt0(xr,xm)=sdtpldt0(xn,xm)|~sdtlseqdt0(sdtpldt0(xr,xm),sdtpldt0(xn,xm))|~aNaturalNumber0(xp)),
% 14.80/2.48 inference(forward_subsumption_resolution,[status(thm)],[f813,f80])).
% 14.80/2.48 fof(f1016,plain,(
% 14.80/2.48 ~aNaturalNumber0(sdtpldt0(xr,xm))|~aNaturalNumber0(sdtpldt0(xn,xm))|sdtpldt0(xr,xm)=sdtpldt0(xn,xm)|~sdtlseqdt0(sdtpldt0(xr,xm),sdtpldt0(xn,xm))),
% 14.80/2.48 inference(resolution,[status(thm)],[f819,f168])).
% 14.80/2.48 fof(f1017,plain,(
% 14.80/2.48 ~aNaturalNumber0(sdtpldt0(xn,xm))|sdtpldt0(xr,xm)=sdtpldt0(xn,xm)|~sdtlseqdt0(sdtpldt0(xr,xm),sdtpldt0(xn,xm))|~aNaturalNumber0(xr)|~aNaturalNumber0(xm)),
% 14.80/2.48 inference(resolution,[status(thm)],[f1016,f55])).
% 14.80/2.48 fof(f1018,plain,(
% 14.80/2.48 ~aNaturalNumber0(sdtpldt0(xn,xm))|sdtpldt0(xr,xm)=sdtpldt0(xn,xm)|~sdtlseqdt0(sdtpldt0(xr,xm),sdtpldt0(xn,xm))|~aNaturalNumber0(xm)),
% 14.80/2.48 inference(forward_subsumption_resolution,[status(thm)],[f1017,f194])).
% 14.80/2.48 fof(f1019,plain,(
% 14.80/2.48 ~aNaturalNumber0(sdtpldt0(xn,xm))|sdtpldt0(xr,xm)=sdtpldt0(xn,xm)|~sdtlseqdt0(sdtpldt0(xr,xm),sdtpldt0(xn,xm))),
% 14.80/2.48 inference(resolution,[status(thm)],[f1018,f167])).
% 14.80/2.48 fof(f1020,plain,(
% 14.80/2.48 sdtpldt0(xr,xm)=sdtpldt0(xn,xm)|~sdtlseqdt0(sdtpldt0(xr,xm),sdtpldt0(xn,xm))|~aNaturalNumber0(xn)|~aNaturalNumber0(xm)),
% 14.80/2.48 inference(resolution,[status(thm)],[f1019,f55])).
% 14.80/2.48 fof(f1021,plain,(
% 14.80/2.48 sdtpldt0(xr,xm)=sdtpldt0(xn,xm)|~sdtlseqdt0(sdtpldt0(xr,xm),sdtpldt0(xn,xm))|~aNaturalNumber0(xm)),
% 14.80/2.48 inference(forward_subsumption_resolution,[status(thm)],[f1020,f166])).
% 14.80/2.48 fof(f1022,plain,(
% 14.80/2.48 sdtpldt0(xr,xm)=sdtpldt0(xn,xm)|~sdtlseqdt0(sdtpldt0(xr,xm),sdtpldt0(xn,xm))),
% 14.80/2.48 inference(resolution,[status(thm)],[f1021,f167])).
% 14.80/2.48 fof(f1023,plain,(
% 14.80/2.48 sdtpldt0(xr,xm)=sdtpldt0(xn,xm)|~aNaturalNumber0(xr)|~aNaturalNumber0(xn)|xr=xn|~sdtlseqdt0(xr,xn)|~aNaturalNumber0(xm)),
% 14.80/2.48 inference(resolution,[status(thm)],[f1022,f114])).
% 14.80/2.48 fof(f1025,plain,(
% 14.80/2.48 ~aNaturalNumber0(xr)|~aNaturalNumber0(xn)|xr=xn|~sdtlseqdt0(xr,xn)|~aNaturalNumber0(xm)),
% 14.80/2.48 inference(forward_subsumption_resolution,[status(thm)],[f1023,f80])).
% 14.80/2.48 fof(f1026,plain,(
% 14.80/2.48 ~aNaturalNumber0(xn)|xr=xn|~sdtlseqdt0(xr,xn)|~aNaturalNumber0(xm)),
% 14.80/2.48 inference(resolution,[status(thm)],[f1025,f194])).
% 14.80/2.48 fof(f1027,plain,(
% 14.80/2.48 xr=xn|~sdtlseqdt0(xr,xn)|~aNaturalNumber0(xm)),
% 14.80/2.48 inference(forward_subsumption_resolution,[status(thm)],[f1026,f166])).
% 14.80/2.48 fof(f1324,plain,(
% 14.80/2.48 xr=xn|~sdtlseqdt0(xr,xn)),
% 14.80/2.48 inference(resolution,[status(thm)],[f1027,f167])).
% 14.80/2.48 fof(f1326,plain,(
% 14.80/2.48 ~sdtlseqdt0(xr,xn)),
% 14.80/2.48 inference(forward_subsumption_resolution,[status(thm)],[f1324,f198])).
% 14.80/2.48 fof(f1327,plain,(
% 14.80/2.48 $false),
% 14.80/2.48 inference(backward_subsumption_resolution,[status(thm)],[f201,f1326])).
% 14.80/2.48 % SZS output end CNFRefutation for theBenchmark.p
% 14.80/2.49 % Elapsed time: 2.126832 seconds
% 14.80/2.49 % CPU time: 16.546168 seconds
% 14.80/2.49 % Total memory used: 229.724 MB
% 14.80/2.49 % Net memory used: 219.162 MB
%------------------------------------------------------------------------------