%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM527+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 : n002.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:07 PM UTC 2026
% Result : Theorem 17.45s 2.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM527+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.10/0.35 % Computer : n002.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 02:40:46 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 17.45/2.62 % Refutation found
% 17.45/2.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 17.45/2.62 % SZS output start CNFRefutation for theBenchmark
% 17.45/2.62 fof(f5,axiom,(
% 17.45/2.62 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtasdt0(W0,W1)) ) )),
% 17.45/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.45/2.62 fof(f9,axiom,(
% 17.45/2.62 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 17.45/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.45/2.62 fof(f20,axiom,(
% 17.45/2.62 (! [W0] :( aNaturalNumber0(W0)=> sdtlseqdt0(W0,W0) ) )),
% 17.45/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.45/2.62 fof(f22,axiom,(
% 17.45/2.62 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W1,W2) )=> sdtlseqdt0(W0,W2) ) ) )),
% 17.45/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.45/2.62 fof(f25,axiom,(
% 17.45/2.62 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> ( ( W0 != sz00& W1 != W2& sdtlseqdt0(W1,W2) )=> ( sdtasdt0(W0,W1) != sdtasdt0(W0,W2)& sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))& sdtasdt0(W1,W0) != sdtasdt0(W2,W0)& sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) ) )),
% 17.45/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.45/2.62 fof(f40,hypothesis,(
% 17.45/2.62 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp)& xn != sz00& xm != sz00& xp != sz00 ) ),
% 17.45/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.45/2.62 fof(f47,conjecture,(
% 17.45/2.62 ( sdtlseqdt0(xn,xm)=> sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)) ) ),
% 17.45/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 17.45/2.62 fof(f48,negated_conjecture,(
% 17.45/2.62 ~(( sdtlseqdt0(xn,xm)=> sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)) ) )),
% 17.45/2.62 inference(negated_conjecture,[status(cth)],[f47])).
% 17.45/2.62 fof(f57,plain,(
% 17.45/2.62 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtasdt0(W0,W1)))),
% 17.45/2.62 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 17.45/2.62 fof(f58,plain,(
% 17.45/2.62 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtasdt0(X0,X1)))),
% 17.45/2.62 inference(cnf_transformation,[status(thm)],[f57])).
% 17.45/2.62 fof(f66,plain,(
% 17.45/2.62 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 17.45/2.62 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 17.45/2.62 fof(f67,plain,(
% 17.45/2.62 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 17.45/2.62 inference(cnf_transformation,[status(thm)],[f66])).
% 17.45/2.62 fof(f102,plain,(
% 17.45/2.62 ![W0]: (~aNaturalNumber0(W0)|sdtlseqdt0(W0,W0))),
% 17.45/2.62 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 17.45/2.62 fof(f103,plain,(
% 17.45/2.62 ![X0]: (~aNaturalNumber0(X0)|sdtlseqdt0(X0,X0))),
% 17.45/2.62 inference(cnf_transformation,[status(thm)],[f102])).
% 17.45/2.62 fof(f106,plain,(
% 17.45/2.62 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W2))|sdtlseqdt0(W0,W2)))),
% 17.45/2.62 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 17.45/2.62 fof(f107,plain,(
% 17.45/2.62 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X1,X2)|sdtlseqdt0(X0,X2))),
% 17.45/2.62 inference(cnf_transformation,[status(thm)],[f106])).
% 17.45/2.62 fof(f116,plain,(
% 17.45/2.62 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|(((W0=sz00|W1=W2)|~sdtlseqdt0(W1,W2))|(((~sdtasdt0(W0,W1)=sdtasdt0(W0,W2)&sdtlseqdt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2)))&~sdtasdt0(W1,W0)=sdtasdt0(W2,W0))&sdtlseqdt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)))))),
% 17.45/2.62 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 17.45/2.62 fof(f118,plain,(
% 17.45/2.62 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|X0=sz00|X1=X2|~sdtlseqdt0(X1,X2)|sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 17.45/2.62 inference(cnf_transformation,[status(thm)],[f116])).
% 17.45/2.62 fof(f169,plain,(
% 17.45/2.62 aNaturalNumber0(xn)),
% 17.45/2.62 inference(cnf_transformation,[status(thm)],[f40])).
% 17.45/2.62 fof(f170,plain,(
% 17.45/2.62 aNaturalNumber0(xm)),
% 17.45/2.62 inference(cnf_transformation,[status(thm)],[f40])).
% 17.45/2.62 fof(f172,plain,(
% 17.45/2.62 ~xn=sz00),
% 17.45/2.62 inference(cnf_transformation,[status(thm)],[f40])).
% 17.45/2.62 fof(f173,plain,(
% 17.45/2.62 ~xm=sz00),
% 17.45/2.62 inference(cnf_transformation,[status(thm)],[f40])).
% 17.45/2.62 fof(f183,plain,(
% 17.45/2.62 (sdtlseqdt0(xn,xm)&~sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)))),
% 17.45/2.62 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 17.45/2.62 fof(f184,plain,(
% 17.45/2.62 sdtlseqdt0(xn,xm)),
% 17.45/2.62 inference(cnf_transformation,[status(thm)],[f183])).
% 17.45/2.62 fof(f185,plain,(
% 17.45/2.62 ~sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))),
% 17.45/2.62 inference(cnf_transformation,[status(thm)],[f183])).
% 17.45/2.62 fof(f204,plain,(
% 17.45/2.62 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,xm)=sdtasdt0(xm,X0))),
% 17.45/2.62 inference(resolution,[status(thm)],[f67,f170])).
% 17.45/2.62 fof(f277,plain,(
% 17.45/2.62 sdtasdt0(xn,xm)=sdtasdt0(xm,xn)),
% 17.45/2.62 inference(resolution,[status(thm)],[f204,f169])).
% 17.45/2.62 fof(f285,plain,(
% 17.45/2.62 ![X0]: (~aNaturalNumber0(sdtasdt0(xn,xn))|~aNaturalNumber0(X0)|~aNaturalNumber0(sdtasdt0(xm,xm))|~sdtlseqdt0(sdtasdt0(xn,xn),X0)|~sdtlseqdt0(X0,sdtasdt0(xm,xm)))),
% 17.45/2.62 inference(resolution,[status(thm)],[f107,f185])).
% 17.45/2.62 fof(f334,plain,(
% 17.45/2.62 ![X0]: (~aNaturalNumber0(sdtasdt0(xn,xn))|~aNaturalNumber0(X0)|~sdtlseqdt0(sdtasdt0(xn,xn),X0)|~sdtlseqdt0(X0,sdtasdt0(xm,xm))|~aNaturalNumber0(xm)|~aNaturalNumber0(xm))),
% 17.45/2.62 inference(resolution,[status(thm)],[f285,f58])).
% 17.45/2.62 fof(f335,plain,(
% 17.45/2.62 ![X0]: (~aNaturalNumber0(sdtasdt0(xn,xn))|~aNaturalNumber0(X0)|~sdtlseqdt0(sdtasdt0(xn,xn),X0)|~sdtlseqdt0(X0,sdtasdt0(xm,xm))|~aNaturalNumber0(xm))),
% 17.45/2.62 inference(duplicate_literals_removal,[status(thm)],[f334])).
% 17.45/2.62 fof(f336,plain,(
% 17.45/2.62 ![X0]: (~aNaturalNumber0(sdtasdt0(xn,xn))|~aNaturalNumber0(X0)|~sdtlseqdt0(sdtasdt0(xn,xn),X0)|~sdtlseqdt0(X0,sdtasdt0(xm,xm)))),
% 17.45/2.62 inference(forward_subsumption_resolution,[status(thm)],[f335,f170])).
% 17.45/2.62 fof(f434,plain,(
% 17.45/2.62 ![X0]: (~aNaturalNumber0(X0)|~aNaturalNumber0(xn)|~aNaturalNumber0(xm)|X0=sz00|xn=xm|sdtlseqdt0(sdtasdt0(X0,xn),sdtasdt0(X0,xm)))),
% 17.45/2.62 inference(resolution,[status(thm)],[f118,f184])).
% 17.45/2.62 fof(f438,plain,(
% 17.45/2.62 ![X0]: (~aNaturalNumber0(X0)|~aNaturalNumber0(xm)|X0=sz00|xn=xm|sdtlseqdt0(sdtasdt0(X0,xn),sdtasdt0(X0,xm)))),
% 17.45/2.62 inference(forward_subsumption_resolution,[status(thm)],[f434,f169])).
% 17.45/2.62 fof(f551,plain,(
% 17.45/2.62 ![X0]: (~aNaturalNumber0(X0)|X0=sz00|xn=xm|sdtlseqdt0(sdtasdt0(X0,xn),sdtasdt0(X0,xm)))),
% 17.45/2.62 inference(resolution,[status(thm)],[f438,f170])).
% 17.45/2.62 fof(f650,plain,(
% 17.45/2.62 xm=sz00|xn=xm|sdtlseqdt0(sdtasdt0(xm,xn),sdtasdt0(xm,xm))),
% 17.45/2.62 inference(resolution,[status(thm)],[f551,f170])).
% 17.45/2.62 fof(f651,plain,(
% 17.45/2.62 xn=sz00|xn=xm|sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xn,xm))),
% 17.45/2.62 inference(resolution,[status(thm)],[f551,f169])).
% 17.45/2.62 fof(f657,plain,(
% 17.45/2.62 xm=sz00|xn=xm|sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xm,xm))),
% 17.45/2.62 inference(forward_demodulation,[status(thm)],[f277,f650])).
% 17.45/2.62 fof(f658,plain,(
% 17.45/2.62 xn=xm|sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xm,xm))),
% 17.45/2.62 inference(forward_subsumption_resolution,[status(thm)],[f657,f173])).
% 17.45/2.62 fof(f659,plain,(
% 17.45/2.62 xn=xm|sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xn,xm))),
% 17.45/2.62 inference(forward_subsumption_resolution,[status(thm)],[f651,f172])).
% 17.45/2.62 fof(f788,plain,(
% 17.45/2.62 ![X0]: (~aNaturalNumber0(X0)|~sdtlseqdt0(sdtasdt0(xn,xn),X0)|~sdtlseqdt0(X0,sdtasdt0(xm,xm))|~aNaturalNumber0(xn)|~aNaturalNumber0(xn))),
% 17.45/2.62 inference(resolution,[status(thm)],[f336,f58])).
% 17.45/2.62 fof(f789,plain,(
% 17.45/2.62 ![X0]: (~aNaturalNumber0(X0)|~sdtlseqdt0(sdtasdt0(xn,xn),X0)|~sdtlseqdt0(X0,sdtasdt0(xm,xm))|~aNaturalNumber0(xn))),
% 17.45/2.62 inference(duplicate_literals_removal,[status(thm)],[f788])).
% 17.45/2.62 fof(f790,plain,(
% 17.45/2.62 ![X0]: (~aNaturalNumber0(X0)|~sdtlseqdt0(sdtasdt0(xn,xn),X0)|~sdtlseqdt0(X0,sdtasdt0(xm,xm)))),
% 17.45/2.62 inference(forward_subsumption_resolution,[status(thm)],[f789,f169])).
% 17.45/2.62 fof(f1685,plain,(
% 17.45/2.62 ~aNaturalNumber0(sdtasdt0(xn,xm))|~sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xm,xm))|xn=xm),
% 17.45/2.62 inference(resolution,[status(thm)],[f790,f659])).
% 17.45/2.62 fof(f1689,plain,(
% 17.45/2.62 ~aNaturalNumber0(sdtasdt0(xn,xm))|xn=xm),
% 17.45/2.62 inference(forward_subsumption_resolution,[status(thm)],[f1685,f658])).
% 17.45/2.62 fof(f1693,plain,(
% 17.45/2.62 xn=xm|~aNaturalNumber0(xn)|~aNaturalNumber0(xm)),
% 17.45/2.62 inference(resolution,[status(thm)],[f1689,f58])).
% 17.45/2.62 fof(f1694,plain,(
% 17.45/2.62 xn=xm|~aNaturalNumber0(xm)),
% 17.45/2.62 inference(forward_subsumption_resolution,[status(thm)],[f1693,f169])).
% 17.45/2.62 fof(f1711,plain,(
% 17.45/2.62 xn=xm),
% 17.45/2.62 inference(resolution,[status(thm)],[f1694,f170])).
% 17.45/2.62 fof(f1775,plain,(
% 17.45/2.62 ~sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xn))),
% 17.45/2.62 inference(backward_demodulation,[status(thm)],[f1711,f185])).
% 17.45/2.62 fof(f1938,plain,(
% 17.45/2.62 ~sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xn,xm))),
% 17.45/2.64 inference(forward_demodulation,[status(thm)],[f277,f1775])).
% 17.45/2.64 fof(f1939,plain,(
% 17.45/2.64 ~sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xn,xn))),
% 17.45/2.64 inference(forward_demodulation,[status(thm)],[f1711,f1938])).
% 17.45/2.64 fof(f2127,plain,(
% 17.45/2.64 ~aNaturalNumber0(sdtasdt0(xn,xn))),
% 17.45/2.64 inference(resolution,[status(thm)],[f1939,f103])).
% 17.45/2.64 fof(f2142,plain,(
% 17.45/2.64 ~aNaturalNumber0(xn)|~aNaturalNumber0(xn)),
% 17.45/2.64 inference(resolution,[status(thm)],[f2127,f58])).
% 17.45/2.64 fof(f2143,plain,(
% 17.45/2.64 ~aNaturalNumber0(xn)),
% 17.45/2.64 inference(duplicate_literals_removal,[status(thm)],[f2142])).
% 17.45/2.64 fof(f2144,plain,(
% 17.45/2.64 $false),
% 17.45/2.64 inference(forward_subsumption_resolution,[status(thm)],[f2143,f169])).
% 17.45/2.64 % SZS output end CNFRefutation for theBenchmark.p
% 17.45/2.65 % Elapsed time: 2.282071 seconds
% 17.45/2.65 % CPU time: 17.806869 seconds
% 17.45/2.65 % Total memory used: 254.964 MB
% 17.45/2.65 % Net memory used: 241.992 MB
%------------------------------------------------------------------------------