%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM504+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 : n005.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:04 PM UTC 2026
% Result : Theorem 155.49s 20.04s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM504+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n005.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 02:35:48 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.38 % Drodi V4.1.1
% 155.49/20.04 % Refutation found
% 155.49/20.04 % SZS status Theorem for theBenchmark: Theorem is valid
% 155.49/20.04 % SZS output start CNFRefutation for theBenchmark
% 155.49/20.04 fof(f2,axiom,(
% 155.49/20.04 aNaturalNumber0(sz00) ),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f3,axiom,(
% 155.49/20.04 ( aNaturalNumber0(sz10)& sz10 != sz00 ) ),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f5,axiom,(
% 155.49/20.04 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtasdt0(W0,W1)) ) )),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f11,axiom,(
% 155.49/20.04 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f12,axiom,(
% 155.49/20.04 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f21,axiom,(
% 155.49/20.04 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W1,W0) )=> W0 = W1 ) ) )),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f30,definition,(
% 155.49/20.04 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( doDivides0(W0,W1)<=> (? [W2] :( aNaturalNumber0(W2)& W1 = sdtasdt0(W0,W2) ) )) ) )),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f31,definition,(
% 155.49/20.04 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( ( W0 != sz00& doDivides0(W0,W1) )=> (! [W2] :( W2 = sdtsldt0(W1,W0)<=> ( aNaturalNumber0(W2)& W1 = sdtasdt0(W0,W2) ) ) )) ) )),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f37,definition,(
% 155.49/20.04 (! [W0] :( aNaturalNumber0(W0)=> ( isPrime0(W0)<=> ( W0 != sz00& W0 != sz10& (! [W1] :( ( aNaturalNumber0(W1)& doDivides0(W1,W0) )=> ( W1 = sz10| W1 = W0 ) ) )) ) ) )),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f39,hypothesis,(
% 155.49/20.04 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp) ) ),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f41,hypothesis,(
% 155.49/20.04 ( isPrime0(xp)& doDivides0(xp,sdtasdt0(xn,xm)) ) ),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f43,hypothesis,(
% 155.49/20.04 ~ sdtlseqdt0(xp,xm) ),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f45,hypothesis,(
% 155.49/20.04 xk = sdtsldt0(sdtasdt0(xn,xm),xp) ),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f48,hypothesis,(
% 155.49/20.04 ( aNaturalNumber0(xr)& doDivides0(xr,xk)& isPrime0(xr) ) ),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f49,hypothesis,(
% 155.49/20.04 ( sdtlseqdt0(xr,xk)& doDivides0(xr,sdtasdt0(xn,xm)) ) ),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f51,hypothesis,(
% 155.49/20.04 ( sdtasdt0(xn,xm) != sdtasdt0(xp,xm)& sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))& sdtasdt0(xp,xm) != sdtasdt0(xp,xk)& sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk)) ) ),
% 155.49/20.04 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 155.49/20.04 fof(f57,plain,(
% 155.49/20.04 aNaturalNumber0(sz00)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f2])).
% 155.49/20.04 fof(f58,plain,(
% 155.49/20.04 aNaturalNumber0(sz10)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f3])).
% 155.49/20.04 fof(f59,plain,(
% 155.49/20.04 ~sz10=sz00),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f3])).
% 155.49/20.04 fof(f62,plain,(
% 155.49/20.04 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtasdt0(W0,W1)))),
% 155.49/20.04 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 155.49/20.04 fof(f63,plain,(
% 155.49/20.04 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtasdt0(X0,X1)))),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f62])).
% 155.49/20.04 fof(f75,plain,(
% 155.49/20.04 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 155.49/20.04 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 155.49/20.04 fof(f76,plain,(
% 155.49/20.04 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz10)=X0)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f75])).
% 155.49/20.04 fof(f77,plain,(
% 155.49/20.04 ![X0]: (~aNaturalNumber0(X0)|X0=sdtasdt0(sz10,X0))),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f75])).
% 155.49/20.04 fof(f78,plain,(
% 155.49/20.04 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 155.49/20.04 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 155.49/20.04 fof(f79,plain,(
% 155.49/20.04 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f78])).
% 155.49/20.04 fof(f109,plain,(
% 155.49/20.04 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W0))|W0=W1))),
% 155.49/20.04 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 155.49/20.04 fof(f110,plain,(
% 155.49/20.04 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X1,X0)|X0=X1)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f109])).
% 155.49/20.04 fof(f135,plain,(
% 155.49/20.04 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(doDivides0(W0,W1)<=>(?[W2]: (aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2)))))),
% 155.49/20.04 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 155.49/20.04 fof(f136,plain,(
% 155.49/20.04 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~doDivides0(W0,W1)|(?[W2]: (aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2))))&(doDivides0(W0,W1)|(![W2]: (~aNaturalNumber0(W2)|~W1=sdtasdt0(W0,W2))))))),
% 155.49/20.04 inference(NNF_transformation,[status(thm)],[f135])).
% 155.49/20.04 fof(f137,plain,(
% 155.49/20.04 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~doDivides0(W0,W1)|(aNaturalNumber0(sK1_skl(W1,W0))&W1=sdtasdt0(W0,sK1_skl(W1,W0))))&(doDivides0(W0,W1)|(![W2]: (~aNaturalNumber0(W2)|~W1=sdtasdt0(W0,W2))))))),
% 155.49/20.04 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f136])).
% 155.49/20.04 fof(f140,plain,(
% 155.49/20.04 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|doDivides0(X0,X1)|~aNaturalNumber0(X2)|~X1=sdtasdt0(X0,X2))),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f137])).
% 155.49/20.04 fof(f141,plain,(
% 155.49/20.04 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((W0=sz00|~doDivides0(W0,W1))|(![W2]: (W2=sdtsldt0(W1,W0)<=>(aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2))))))),
% 155.49/20.04 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 155.49/20.04 fof(f142,plain,(
% 155.49/20.04 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((W0=sz00|~doDivides0(W0,W1))|(![W2]: ((~W2=sdtsldt0(W1,W0)|(aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2)))&(W2=sdtsldt0(W1,W0)|(~aNaturalNumber0(W2)|~W1=sdtasdt0(W0,W2)))))))),
% 155.49/20.04 inference(NNF_transformation,[status(thm)],[f141])).
% 155.49/20.04 fof(f143,plain,(
% 155.49/20.04 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((W0=sz00|~doDivides0(W0,W1))|((![W2]: (~W2=sdtsldt0(W1,W0)|(aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2))))&(![W2]: (W2=sdtsldt0(W1,W0)|(~aNaturalNumber0(W2)|~W1=sdtasdt0(W0,W2)))))))),
% 155.49/20.04 inference(miniscoping,[status(thm)],[f142])).
% 155.49/20.04 fof(f144,plain,(
% 155.49/20.04 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=sz00|~doDivides0(X0,X1)|~X2=sdtsldt0(X1,X0)|aNaturalNumber0(X2))),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f143])).
% 155.49/20.04 fof(f145,plain,(
% 155.49/20.04 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=sz00|~doDivides0(X0,X1)|~X2=sdtsldt0(X1,X0)|X1=sdtasdt0(X0,X2))),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f143])).
% 155.49/20.04 fof(f157,plain,(
% 155.49/20.04 ![W0]: (~aNaturalNumber0(W0)|(isPrime0(W0)<=>((~W0=sz00&~W0=sz10)&(![W1]: ((~aNaturalNumber0(W1)|~doDivides0(W1,W0))|(W1=sz10|W1=W0))))))),
% 155.49/20.04 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 155.49/20.04 fof(f158,plain,(
% 155.49/20.04 ![W0]: (~aNaturalNumber0(W0)|((~isPrime0(W0)|((~W0=sz00&~W0=sz10)&(![W1]: ((~aNaturalNumber0(W1)|~doDivides0(W1,W0))|(W1=sz10|W1=W0)))))&(isPrime0(W0)|((W0=sz00|W0=sz10)|(?[W1]: ((aNaturalNumber0(W1)&doDivides0(W1,W0))&(~W1=sz10&~W1=W0)))))))),
% 155.49/20.04 inference(NNF_transformation,[status(thm)],[f157])).
% 155.49/20.04 fof(f159,plain,(
% 155.49/20.04 ![W0]: (~aNaturalNumber0(W0)|((~isPrime0(W0)|((~W0=sz00&~W0=sz10)&(![W1]: ((~aNaturalNumber0(W1)|~doDivides0(W1,W0))|(W1=sz10|W1=W0)))))&(isPrime0(W0)|((W0=sz00|W0=sz10)|((aNaturalNumber0(sK2_skl(W0))&doDivides0(sK2_skl(W0),W0))&(~sK2_skl(W0)=sz10&~sK2_skl(W0)=W0))))))),
% 155.49/20.04 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W1,sK2_skl(W0))],[f158])).
% 155.49/20.04 fof(f160,plain,(
% 155.49/20.04 ![X0]: (~aNaturalNumber0(X0)|~isPrime0(X0)|~X0=sz00)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f159])).
% 155.49/20.04 fof(f172,plain,(
% 155.49/20.04 aNaturalNumber0(xn)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f39])).
% 155.49/20.04 fof(f173,plain,(
% 155.49/20.04 aNaturalNumber0(xm)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f39])).
% 155.49/20.04 fof(f174,plain,(
% 155.49/20.04 aNaturalNumber0(xp)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f39])).
% 155.49/20.04 fof(f177,plain,(
% 155.49/20.04 isPrime0(xp)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f41])).
% 155.49/20.04 fof(f178,plain,(
% 155.49/20.04 doDivides0(xp,sdtasdt0(xn,xm))),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f41])).
% 155.49/20.04 fof(f180,plain,(
% 155.49/20.04 ~sdtlseqdt0(xp,xm)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f43])).
% 155.49/20.04 fof(f185,plain,(
% 155.49/20.04 xk=sdtsldt0(sdtasdt0(xn,xm),xp)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f45])).
% 155.49/20.04 fof(f191,plain,(
% 155.49/20.04 aNaturalNumber0(xr)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f48])).
% 155.49/20.04 fof(f195,plain,(
% 155.49/20.04 doDivides0(xr,sdtasdt0(xn,xm))),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f49])).
% 155.49/20.04 fof(f198,plain,(
% 155.49/20.04 sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f51])).
% 155.49/20.04 fof(f199,plain,(
% 155.49/20.04 ~sdtasdt0(xp,xm)=sdtasdt0(xp,xk)),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f51])).
% 155.49/20.04 fof(f200,plain,(
% 155.49/20.04 sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk))),
% 155.49/20.04 inference(cnf_transformation,[status(thm)],[f51])).
% 155.49/20.04 fof(f207,plain,(
% 155.49/20.04 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(sdtasdt0(X0,X1))|doDivides0(X0,sdtasdt0(X0,X1))|~aNaturalNumber0(X1))),
% 155.49/20.04 inference(destructive_equality_resolution,[status(thm)],[f140])).
% 155.49/20.04 fof(f208,plain,(
% 155.49/20.04 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=sz00|~doDivides0(X0,X1)|aNaturalNumber0(sdtsldt0(X1,X0)))),
% 155.49/20.04 inference(destructive_equality_resolution,[status(thm)],[f144])).
% 155.49/20.04 fof(f209,plain,(
% 155.49/20.04 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=sz00|~doDivides0(X0,X1)|X1=sdtasdt0(X0,sdtsldt0(X1,X0)))),
% 155.49/20.04 inference(destructive_equality_resolution,[status(thm)],[f145])).
% 155.49/20.04 fof(f211,plain,(
% 155.49/20.04 ~aNaturalNumber0(sz00)|~isPrime0(sz00)),
% 155.49/20.04 inference(destructive_equality_resolution,[status(thm)],[f160])).
% 155.49/20.04 fof(f221,plain,(
% 155.49/20.04 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtasdt0(xp,X0)))),
% 155.49/20.04 inference(resolution,[status(thm)],[f174,f63])).
% 155.49/20.04 fof(f268,plain,(
% 155.49/20.04 sdtasdt0(xr,sz00)=sz00),
% 155.49/20.04 inference(resolution,[status(thm)],[f191,f79])).
% 155.49/20.04 fof(f322,definition,(
% 155.49/20.04 sQ2_spl <=> (xp=sz00)),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f323,plain,(
% 155.49/20.04 xp=sz00|~sQ2_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f322])).
% 155.49/20.04 fof(f452,plain,(
% 155.49/20.04 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtasdt0(xp,X0)))),
% 155.49/20.04 inference(resolution,[status(thm)],[f174,f63])).
% 155.49/20.04 fof(f516,plain,(
% 155.49/20.04 sdtasdt0(xm,sz00)=sz00),
% 155.49/20.04 inference(resolution,[status(thm)],[f173,f79])).
% 155.49/20.04 fof(f517,plain,(
% 155.49/20.04 xm=sdtasdt0(sz10,xm)),
% 155.49/20.04 inference(resolution,[status(thm)],[f173,f77])).
% 155.49/20.04 fof(f518,plain,(
% 155.49/20.04 sdtasdt0(xm,sz10)=xm),
% 155.49/20.04 inference(resolution,[status(thm)],[f173,f76])).
% 155.49/20.04 fof(f813,plain,(
% 155.49/20.04 ![X0,X1]: (~aNaturalNumber0(X0)|doDivides0(X0,sdtasdt0(X0,X1))|~aNaturalNumber0(X1))),
% 155.49/20.04 inference(forward_subsumption_resolution,[status(thm)],[f207,f63])).
% 155.49/20.04 fof(f815,plain,(
% 155.49/20.04 ![X0]: (doDivides0(xm,sdtasdt0(xm,X0))|~aNaturalNumber0(X0))),
% 155.49/20.04 inference(resolution,[status(thm)],[f813,f173])).
% 155.49/20.04 fof(f856,plain,(
% 155.49/20.04 isPrime0(sz00)|~sQ2_spl),
% 155.49/20.04 inference(backward_demodulation,[status(thm)],[f323,f177])).
% 155.49/20.04 fof(f860,plain,(
% 155.49/20.04 ~isPrime0(sz00)),
% 155.49/20.04 inference(forward_subsumption_resolution,[status(thm)],[f211,f57])).
% 155.49/20.04 fof(f862,plain,(
% 155.49/20.04 $false|~sQ2_spl),
% 155.49/20.04 inference(forward_subsumption_resolution,[status(thm)],[f856,f860])).
% 155.49/20.04 fof(f863,plain,(
% 155.49/20.04 ~sQ2_spl),
% 155.49/20.04 inference(contradiction_clause,[status(thm)],[f862])).
% 155.49/20.04 fof(f1327,definition,(
% 155.49/20.04 sQ142_spl <=> (aNaturalNumber0(xp))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f1329,plain,(
% 155.49/20.04 ~aNaturalNumber0(xp)|sQ142_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f1327])).
% 155.49/20.04 fof(f1518,definition,(
% 155.49/20.04 sQ172_spl <=> (aNaturalNumber0(sdtasdt0(xp,xk)))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f1606,plain,(
% 155.49/20.04 $false|sQ142_spl),
% 155.49/20.04 inference(forward_subsumption_resolution,[status(thm)],[f1329,f174])).
% 155.49/20.04 fof(f1607,plain,(
% 155.49/20.04 sQ142_spl),
% 155.49/20.04 inference(contradiction_clause,[status(thm)],[f1606])).
% 155.49/20.04 fof(f1753,plain,(
% 155.49/20.04 sdtasdt0(xr,sz00)=sz00),
% 155.49/20.04 inference(resolution,[status(thm)],[f191,f79])).
% 155.49/20.04 fof(f1864,plain,(
% 155.49/20.04 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtasdt0(xn,X0)))),
% 155.49/20.04 inference(resolution,[status(thm)],[f172,f63])).
% 155.49/20.04 fof(f1901,definition,(
% 155.49/20.04 sQ224_spl <=> (aNaturalNumber0(xm))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f1902,plain,(
% 155.49/20.04 aNaturalNumber0(xm)|~sQ224_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f1901])).
% 155.49/20.04 fof(f1903,plain,(
% 155.49/20.04 ~aNaturalNumber0(xm)|sQ224_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f1901])).
% 155.49/20.04 fof(f2805,plain,(
% 155.49/20.04 $false|sQ224_spl),
% 155.49/20.04 inference(forward_subsumption_resolution,[status(thm)],[f173,f1903])).
% 155.49/20.04 fof(f2806,plain,(
% 155.49/20.04 sQ224_spl),
% 155.49/20.04 inference(contradiction_clause,[status(thm)],[f2805])).
% 155.49/20.04 fof(f2811,plain,(
% 155.49/20.04 ~aNaturalNumber0(sdtasdt0(xp,xm))|~aNaturalNumber0(sdtasdt0(xp,xk))|~sdtlseqdt0(sdtasdt0(xp,xk),sdtasdt0(xp,xm))|sdtasdt0(xp,xm)=sdtasdt0(xp,xk)),
% 155.49/20.04 inference(resolution,[status(thm)],[f200,f110])).
% 155.49/20.04 fof(f2816,definition,(
% 155.49/20.04 sQ369_spl <=> (aNaturalNumber0(sdtasdt0(xp,xm)))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f2819,definition,(
% 155.49/20.04 sQ370_spl <=> (sdtasdt0(xp,xm)=sdtasdt0(xp,xk))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ370_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f2820,plain,(
% 155.49/20.04 sdtasdt0(xp,xm)=sdtasdt0(xp,xk)|~sQ370_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f2819])).
% 155.49/20.04 fof(f2838,definition,(
% 155.49/20.04 sQ375_spl <=> (sdtlseqdt0(sdtasdt0(xp,xk),sdtasdt0(xp,xm)))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ375_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f2840,plain,(
% 155.49/20.04 ~sdtlseqdt0(sdtasdt0(xp,xk),sdtasdt0(xp,xm))|sQ375_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f2838])).
% 155.49/20.04 fof(f2841,plain,(
% 155.49/20.04 ~sQ369_spl|~sQ172_spl|~sQ375_spl|sQ370_spl),
% 155.49/20.04 inference(split_clause,[status(thm)],[f2811,f2816,f1518,f2838,f2819])).
% 155.49/20.04 fof(f4398,definition,(
% 155.49/20.04 sQ538_spl <=> (doDivides0(xr,sz00))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ538_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f4400,plain,(
% 155.49/20.04 ~doDivides0(xr,sz00)|sQ538_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f4398])).
% 155.49/20.04 fof(f4636,plain,(
% 155.49/20.04 aNaturalNumber0(sdtasdt0(xp,xm))|~sQ224_spl),
% 155.49/20.04 inference(resolution,[status(thm)],[f1902,f221])).
% 155.49/20.04 fof(f7211,plain,(
% 155.49/20.04 ![X0]: (doDivides0(xr,sdtasdt0(xr,X0))|~aNaturalNumber0(X0))),
% 155.49/20.04 inference(resolution,[status(thm)],[f191,f813])).
% 155.49/20.04 fof(f8481,definition,(
% 155.49/20.04 sQ850_spl <=> (aNaturalNumber0(sdtasdt0(xn,xm)))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ850_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f8531,plain,(
% 155.49/20.04 ~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xn,xm))|xp=sz00|sdtasdt0(xn,xm)=sdtasdt0(xp,sdtsldt0(sdtasdt0(xn,xm),xp))),
% 155.49/20.04 inference(resolution,[status(thm)],[f178,f209])).
% 155.49/20.04 fof(f8532,plain,(
% 155.49/20.04 ~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xn,xm))|xp=sz00|aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xp))),
% 155.49/20.04 inference(resolution,[status(thm)],[f178,f208])).
% 155.49/20.04 fof(f8555,definition,(
% 155.49/20.04 sQ867_spl <=> (sdtasdt0(xn,xm)=sdtasdt0(xp,sdtsldt0(sdtasdt0(xn,xm),xp)))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ867_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f8556,plain,(
% 155.49/20.04 sdtasdt0(xn,xm)=sdtasdt0(xp,sdtsldt0(sdtasdt0(xn,xm),xp))|~sQ867_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f8555])).
% 155.49/20.04 fof(f8558,plain,(
% 155.49/20.04 ~sQ142_spl|~sQ850_spl|sQ2_spl|sQ867_spl),
% 155.49/20.04 inference(split_clause,[status(thm)],[f8531,f1327,f8481,f322,f8555])).
% 155.49/20.04 fof(f8559,definition,(
% 155.49/20.04 sQ868_spl <=> (aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xp)))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ868_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f8560,plain,(
% 155.49/20.04 aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xp))|~sQ868_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f8559])).
% 155.49/20.04 fof(f8562,plain,(
% 155.49/20.04 ~sQ142_spl|~sQ850_spl|sQ2_spl|sQ868_spl),
% 155.49/20.04 inference(split_clause,[status(thm)],[f8532,f1327,f8481,f322,f8559])).
% 155.49/20.04 fof(f17443,plain,(
% 155.49/20.04 sQ369_spl|~sQ224_spl),
% 155.49/20.04 inference(split_clause,[status(thm)],[f4636,f2816,f1901])).
% 155.49/20.04 fof(f19886,definition,(
% 155.49/20.04 sQ1964_spl <=> (sdtasdt0(xr,sz00)=sz10)),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ1964_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f19887,plain,(
% 155.49/20.04 sdtasdt0(xr,sz00)=sz10|~sQ1964_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f19886])).
% 155.49/20.04 fof(f19901,definition,(
% 155.49/20.04 sQ1968_spl <=> (isPrime0(sdtasdt0(xr,sz00)))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ1968_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f19902,plain,(
% 155.49/20.04 isPrime0(sdtasdt0(xr,sz00))|~sQ1968_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f19901])).
% 155.49/20.04 fof(f20037,plain,(
% 155.49/20.04 doDivides0(xr,sdtasdt0(xr,sz00))),
% 155.49/20.04 inference(resolution,[status(thm)],[f7211,f57])).
% 155.49/20.04 fof(f20039,plain,(
% 155.49/20.04 doDivides0(xr,sz00)),
% 155.49/20.04 inference(forward_demodulation,[status(thm)],[f268,f20037])).
% 155.49/20.04 fof(f22146,definition,(
% 155.49/20.04 sQ2085_spl <=> (sdtlseqdt0(xp,sdtasdt0(sz10,xm)))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ2085_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f22147,plain,(
% 155.49/20.04 sdtlseqdt0(xp,sdtasdt0(sz10,xm))|~sQ2085_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f22146])).
% 155.49/20.04 fof(f22836,definition,(
% 155.49/20.04 sQ2136_spl <=> (doDivides0(xm,xm))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ2136_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f22838,plain,(
% 155.49/20.04 ~doDivides0(xm,xm)|sQ2136_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f22836])).
% 155.49/20.04 fof(f25021,definition,(
% 155.49/20.04 sQ2244_spl <=> (doDivides0(xm,sz00))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ2244_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f25023,plain,(
% 155.49/20.04 ~doDivides0(xm,sz00)|sQ2244_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f25021])).
% 155.49/20.04 fof(f25074,plain,(
% 155.49/20.04 aNaturalNumber0(sdtasdt0(xn,xm))|~sQ224_spl),
% 155.49/20.04 inference(resolution,[status(thm)],[f1864,f1902])).
% 155.49/20.04 fof(f25091,plain,(
% 155.49/20.04 sQ850_spl|~sQ224_spl),
% 155.49/20.04 inference(split_clause,[status(thm)],[f25074,f8481,f1901])).
% 155.49/20.04 fof(f27501,plain,(
% 155.49/20.04 $false|~sQ370_spl),
% 155.49/20.04 inference(forward_subsumption_resolution,[status(thm)],[f2820,f199])).
% 155.49/20.04 fof(f27502,plain,(
% 155.49/20.04 ~sQ370_spl),
% 155.49/20.04 inference(contradiction_clause,[status(thm)],[f27501])).
% 155.49/20.04 fof(f32387,plain,(
% 155.49/20.04 $false|sQ538_spl),
% 155.49/20.04 inference(forward_subsumption_resolution,[status(thm)],[f4400,f20039])).
% 155.49/20.04 fof(f32388,plain,(
% 155.49/20.04 sQ538_spl),
% 155.49/20.04 inference(contradiction_clause,[status(thm)],[f32387])).
% 155.49/20.04 fof(f36646,plain,(
% 155.49/20.04 sz00=sz10|~sQ1964_spl),
% 155.49/20.04 inference(forward_demodulation,[status(thm)],[f1753,f19887])).
% 155.49/20.04 fof(f36647,plain,(
% 155.49/20.04 $false|~sQ1964_spl),
% 155.49/20.04 inference(forward_subsumption_resolution,[status(thm)],[f36646,f59])).
% 155.49/20.04 fof(f36648,plain,(
% 155.49/20.04 ~sQ1964_spl),
% 155.49/20.04 inference(contradiction_clause,[status(thm)],[f36647])).
% 155.49/20.04 fof(f36681,plain,(
% 155.49/20.04 isPrime0(sz00)|~sQ1968_spl),
% 155.49/20.04 inference(forward_demodulation,[status(thm)],[f1753,f19902])).
% 155.49/20.04 fof(f36682,plain,(
% 155.49/20.04 $false|~sQ1968_spl),
% 155.49/20.04 inference(forward_subsumption_resolution,[status(thm)],[f36681,f860])).
% 155.49/20.04 fof(f36683,plain,(
% 155.49/20.04 ~sQ1968_spl),
% 155.49/20.04 inference(contradiction_clause,[status(thm)],[f36682])).
% 155.49/20.04 fof(f36756,plain,(
% 155.49/20.04 sdtlseqdt0(xp,xm)|~sQ2085_spl),
% 155.49/20.04 inference(forward_demodulation,[status(thm)],[f517,f22147])).
% 155.49/20.04 fof(f36757,plain,(
% 155.49/20.04 $false|~sQ2085_spl),
% 155.49/20.04 inference(forward_subsumption_resolution,[status(thm)],[f36756,f180])).
% 155.49/20.04 fof(f36758,plain,(
% 155.49/20.04 ~sQ2085_spl),
% 155.49/20.04 inference(contradiction_clause,[status(thm)],[f36757])).
% 155.49/20.04 fof(f37516,definition,(
% 155.49/20.04 sQ3293_spl <=> (doDivides0(xr,sdtasdt0(xn,xm)))),
% 155.49/20.04 introduced(definition,[new_symbols(definition,[sQ3293_spl])],[split_symbol_definition])).
% 155.49/20.04 fof(f37518,plain,(
% 155.49/20.04 ~doDivides0(xr,sdtasdt0(xn,xm))|sQ3293_spl),
% 155.49/20.04 inference(component_clause,[status(thm)],[f37516])).
% 155.49/20.04 fof(f37523,plain,(
% 155.49/20.04 $false|sQ3293_spl),
% 155.49/20.04 inference(forward_subsumption_resolution,[status(thm)],[f37518,f195])).
% 155.49/20.04 fof(f37524,plain,(
% 155.49/20.04 sQ3293_spl),
% 155.49/20.04 inference(contradiction_clause,[status(thm)],[f37523])).
% 155.49/20.04 fof(f38906,plain,(
% 155.49/20.04 doDivides0(xm,sdtasdt0(xm,sz10))),
% 155.49/20.04 inference(resolution,[status(thm)],[f815,f58])).
% 155.49/20.04 fof(f38907,plain,(
% 155.49/20.04 doDivides0(xm,sdtasdt0(xm,sz00))),
% 155.49/20.04 inference(resolution,[status(thm)],[f815,f57])).
% 155.49/20.04 fof(f38908,plain,(
% 155.49/20.04 doDivides0(xm,xm)),
% 155.49/20.04 inference(forward_demodulation,[status(thm)],[f518,f38906])).
% 155.49/20.04 fof(f38909,plain,(
% 155.49/20.04 $false|sQ2136_spl),
% 155.49/20.04 inference(forward_subsumption_resolution,[status(thm)],[f38908,f22838])).
% 155.49/20.04 fof(f38910,plain,(
% 155.49/20.04 sQ2136_spl),
% 155.49/20.04 inference(contradiction_clause,[status(thm)],[f38909])).
% 155.49/20.04 fof(f38911,plain,(
% 155.49/20.04 doDivides0(xm,sz00)),
% 155.49/20.04 inference(forward_demodulation,[status(thm)],[f516,f38907])).
% 155.49/20.04 fof(f38912,plain,(
% 155.49/20.04 $false|sQ2244_spl),
% 155.49/20.04 inference(forward_subsumption_resolution,[status(thm)],[f38911,f25023])).
% 155.49/20.10 fof(f38913,plain,(
% 155.49/20.10 sQ2244_spl),
% 155.49/20.10 inference(contradiction_clause,[status(thm)],[f38912])).
% 155.49/20.10 fof(f41056,plain,(
% 155.49/20.10 sdtasdt0(xn,xm)=sdtasdt0(xp,xk)|~sQ867_spl),
% 155.49/20.10 inference(forward_demodulation,[status(thm)],[f185,f8556])).
% 155.49/20.10 fof(f41154,plain,(
% 155.49/20.10 aNaturalNumber0(xk)|~sQ868_spl),
% 155.49/20.10 inference(forward_demodulation,[status(thm)],[f185,f8560])).
% 155.49/20.10 fof(f41252,plain,(
% 155.49/20.10 aNaturalNumber0(sdtasdt0(xp,xk))|~sQ868_spl),
% 155.49/20.10 inference(resolution,[status(thm)],[f41154,f452])).
% 155.49/20.10 fof(f41324,plain,(
% 155.49/20.10 sQ172_spl|~sQ868_spl),
% 155.49/20.10 inference(split_clause,[status(thm)],[f41252,f1518,f8559])).
% 155.49/20.10 fof(f41349,plain,(
% 155.49/20.10 ~sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))|~sQ867_spl|sQ375_spl),
% 155.49/20.10 inference(forward_demodulation,[status(thm)],[f41056,f2840])).
% 155.49/20.10 fof(f41350,plain,(
% 155.49/20.10 $false|~sQ867_spl|sQ375_spl),
% 155.49/20.10 inference(forward_subsumption_resolution,[status(thm)],[f41349,f198])).
% 155.49/20.10 fof(f41351,plain,(
% 155.49/20.10 ~sQ867_spl|sQ375_spl),
% 155.49/20.10 inference(contradiction_clause,[status(thm)],[f41350])).
% 155.49/20.10 fof(f41352,plain,(
% 155.49/20.10 $false),
% 155.49/20.10 inference(sat_refutation,[status(thm)],[f863,f1607,f2806,f2841,f8558,f8562,f17443,f25091,f27502,f32388,f36648,f36683,f36758,f37524,f38910,f38913,f41324,f41351])).
% 155.49/20.10 % SZS output end CNFRefutation for theBenchmark.p
% 43.78/20.15 % Elapsed time: 19.758835 seconds
% 43.78/20.15 % CPU time: 156.341051 seconds
% 43.78/20.15 % Total memory used: 801.924 MB
% 43.78/20.15 % Net memory used: 738.088 MB
%------------------------------------------------------------------------------