%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM498+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 : n016.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:03 PM UTC 2026
% Result : Theorem 17.99s 2.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM498+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 : n016.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:39:37 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 17.99/2.80 % Refutation found
% 17.99/2.80 % SZS status Theorem for theBenchmark: Theorem is valid
% 17.99/2.80 % SZS output start CNFRefutation for theBenchmark
% 17.99/2.80 fof(f2,axiom,(
% 17.99/2.80 aNaturalNumber0(sz00) ),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f5,axiom,(
% 17.99/2.80 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtasdt0(W0,W1)) ) )),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f8,axiom,(
% 17.99/2.80 (! [W0] :( aNaturalNumber0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f11,axiom,(
% 17.99/2.80 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f12,axiom,(
% 17.99/2.80 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f17,axiom,(
% 17.99/2.80 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( sdtasdt0(W0,W1) = sz00=> ( W0 = sz00| W1 = sz00 ) ) ) )),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f18,definition,(
% 17.99/2.80 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( sdtlseqdt0(W0,W1)<=> (? [W2] :( aNaturalNumber0(W2)& sdtpldt0(W0,W2) = W1 ) )) ) )),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f21,axiom,(
% 17.99/2.80 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W1,W0) )=> W0 = W1 ) ) )),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f30,definition,(
% 17.99/2.80 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( doDivides0(W0,W1)<=> (? [W2] :( aNaturalNumber0(W2)& W1 = sdtasdt0(W0,W2) ) )) ) )),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f31,definition,(
% 17.99/2.80 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( ( W0 != sz00& doDivides0(W0,W1) )=> (! [W2] :( W2 = sdtsldt0(W1,W0)<=> ( aNaturalNumber0(W2)& W1 = sdtasdt0(W0,W2) ) ) )) ) )),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f37,definition,(
% 17.99/2.80 (! [W0] :( aNaturalNumber0(W0)=> ( isPrime0(W0)<=> ( W0 != sz00& W0 != sz10& (! [W1] :( ( aNaturalNumber0(W1)& doDivides0(W1,W0) )=> ( W1 = sz10| W1 = W0 ) ) )) ) ) )),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f39,hypothesis,(
% 17.99/2.80 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp) ) ),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f41,hypothesis,(
% 17.99/2.80 ( isPrime0(xp)& doDivides0(xp,sdtasdt0(xn,xm)) ) ),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f44,hypothesis,(
% 17.99/2.80 ( xn != xp& sdtlseqdt0(xn,xp)& xm != xp& sdtlseqdt0(xm,xp) ) ),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f45,hypothesis,(
% 17.99/2.80 xk = sdtsldt0(sdtasdt0(xn,xm),xp) ),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f46,conjecture,(
% 17.99/2.80 ( ( xk = sz00| xk = sz10 )=> ( doDivides0(xp,xn)| doDivides0(xp,xm) ) ) ),
% 17.99/2.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 17.99/2.80 fof(f47,negated_conjecture,(
% 17.99/2.80 ~(( ( xk = sz00| xk = sz10 )=> ( doDivides0(xp,xn)| doDivides0(xp,xm) ) ) )),
% 17.99/2.80 inference(negated_conjecture,[status(cth)],[f46])).
% 17.99/2.80 fof(f51,plain,(
% 17.99/2.80 aNaturalNumber0(sz00)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f2])).
% 17.99/2.80 fof(f56,plain,(
% 17.99/2.80 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtasdt0(W0,W1)))),
% 17.99/2.80 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 17.99/2.80 fof(f57,plain,(
% 17.99/2.80 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtasdt0(X0,X1)))),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f56])).
% 17.99/2.80 fof(f62,plain,(
% 17.99/2.80 ![W0]: (~aNaturalNumber0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 17.99/2.80 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 17.99/2.80 fof(f64,plain,(
% 17.99/2.80 ![X0]: (~aNaturalNumber0(X0)|X0=sdtpldt0(sz00,X0))),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f62])).
% 17.99/2.80 fof(f69,plain,(
% 17.99/2.80 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 17.99/2.80 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 17.99/2.80 fof(f70,plain,(
% 17.99/2.80 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz10)=X0)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f69])).
% 17.99/2.80 fof(f71,plain,(
% 17.99/2.80 ![X0]: (~aNaturalNumber0(X0)|X0=sdtasdt0(sz10,X0))),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f69])).
% 17.99/2.80 fof(f72,plain,(
% 17.99/2.80 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 17.99/2.80 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 17.99/2.80 fof(f73,plain,(
% 17.99/2.80 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f72])).
% 17.99/2.80 fof(f74,plain,(
% 17.99/2.80 ![X0]: (~aNaturalNumber0(X0)|sz00=sdtasdt0(sz00,X0))),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f72])).
% 17.99/2.80 fof(f87,plain,(
% 17.99/2.80 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(~sdtasdt0(W0,W1)=sz00|(W0=sz00|W1=sz00)))),
% 17.99/2.80 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 17.99/2.80 fof(f88,plain,(
% 17.99/2.80 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~sdtasdt0(X0,X1)=sz00|X0=sz00|X1=sz00)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f87])).
% 17.99/2.80 fof(f89,plain,(
% 17.99/2.80 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(sdtlseqdt0(W0,W1)<=>(?[W2]: (aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1))))),
% 17.99/2.80 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 17.99/2.80 fof(f90,plain,(
% 17.99/2.80 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~sdtlseqdt0(W0,W1)|(?[W2]: (aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1)))&(sdtlseqdt0(W0,W1)|(![W2]: (~aNaturalNumber0(W2)|~sdtpldt0(W0,W2)=W1)))))),
% 17.99/2.80 inference(NNF_transformation,[status(thm)],[f89])).
% 17.99/2.80 fof(f91,plain,(
% 17.99/2.80 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~sdtlseqdt0(W0,W1)|(aNaturalNumber0(sK0_skl(W1,W0))&sdtpldt0(W0,sK0_skl(W1,W0))=W1))&(sdtlseqdt0(W0,W1)|(![W2]: (~aNaturalNumber0(W2)|~sdtpldt0(W0,W2)=W1)))))),
% 17.99/2.80 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W2,sK0_skl(W1,W0))],[f90])).
% 17.99/2.80 fof(f94,plain,(
% 17.99/2.80 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtlseqdt0(X0,X1)|~aNaturalNumber0(X2)|~sdtpldt0(X0,X2)=X1)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f91])).
% 17.99/2.80 fof(f103,plain,(
% 17.99/2.80 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W0))|W0=W1))),
% 17.99/2.80 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 17.99/2.80 fof(f104,plain,(
% 17.99/2.80 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X1,X0)|X0=X1)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f103])).
% 17.99/2.80 fof(f129,plain,(
% 17.99/2.80 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(doDivides0(W0,W1)<=>(?[W2]: (aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2)))))),
% 17.99/2.80 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 17.99/2.80 fof(f130,plain,(
% 17.99/2.80 ![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))))))),
% 17.99/2.80 inference(NNF_transformation,[status(thm)],[f129])).
% 17.99/2.80 fof(f131,plain,(
% 17.99/2.80 ![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))))))),
% 17.99/2.80 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f130])).
% 17.99/2.80 fof(f134,plain,(
% 17.99/2.80 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|doDivides0(X0,X1)|~aNaturalNumber0(X2)|~X1=sdtasdt0(X0,X2))),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f131])).
% 17.99/2.80 fof(f135,plain,(
% 17.99/2.80 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((W0=sz00|~doDivides0(W0,W1))|(![W2]: (W2=sdtsldt0(W1,W0)<=>(aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2))))))),
% 17.99/2.80 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 17.99/2.80 fof(f136,plain,(
% 17.99/2.80 ![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)))))))),
% 17.99/2.80 inference(NNF_transformation,[status(thm)],[f135])).
% 17.99/2.80 fof(f137,plain,(
% 17.99/2.80 ![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)))))))),
% 17.99/2.80 inference(miniscoping,[status(thm)],[f136])).
% 17.99/2.80 fof(f139,plain,(
% 17.99/2.80 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=sz00|~doDivides0(X0,X1)|~X2=sdtsldt0(X1,X0)|X1=sdtasdt0(X0,X2))),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f137])).
% 17.99/2.80 fof(f151,plain,(
% 17.99/2.80 ![W0]: (~aNaturalNumber0(W0)|(isPrime0(W0)<=>((~W0=sz00&~W0=sz10)&(![W1]: ((~aNaturalNumber0(W1)|~doDivides0(W1,W0))|(W1=sz10|W1=W0))))))),
% 17.99/2.80 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 17.99/2.80 fof(f152,plain,(
% 17.99/2.80 ![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)))))))),
% 17.99/2.80 inference(NNF_transformation,[status(thm)],[f151])).
% 17.99/2.80 fof(f153,plain,(
% 17.99/2.80 ![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))))))),
% 17.99/2.80 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W1,sK2_skl(W0))],[f152])).
% 17.99/2.80 fof(f156,plain,(
% 17.99/2.80 ![X0,X1]: (~aNaturalNumber0(X0)|~isPrime0(X0)|~aNaturalNumber0(X1)|~doDivides0(X1,X0)|X1=sz10|X1=X0)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f153])).
% 17.99/2.80 fof(f166,plain,(
% 17.99/2.80 aNaturalNumber0(xn)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f39])).
% 17.99/2.80 fof(f167,plain,(
% 17.99/2.80 aNaturalNumber0(xm)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f39])).
% 17.99/2.80 fof(f168,plain,(
% 17.99/2.80 aNaturalNumber0(xp)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f39])).
% 17.99/2.80 fof(f171,plain,(
% 17.99/2.80 isPrime0(xp)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f41])).
% 17.99/2.80 fof(f172,plain,(
% 17.99/2.80 doDivides0(xp,sdtasdt0(xn,xm))),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f41])).
% 17.99/2.80 fof(f175,plain,(
% 17.99/2.80 ~xn=xp),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f44])).
% 17.99/2.80 fof(f178,plain,(
% 17.99/2.80 sdtlseqdt0(xm,xp)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f44])).
% 17.99/2.80 fof(f179,plain,(
% 17.99/2.80 xk=sdtsldt0(sdtasdt0(xn,xm),xp)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f45])).
% 17.99/2.80 fof(f180,plain,(
% 17.99/2.80 ((xk=sz00|xk=sz10)&(~doDivides0(xp,xn)&~doDivides0(xp,xm)))),
% 17.99/2.80 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 17.99/2.80 fof(f181,plain,(
% 17.99/2.80 xk=sz00|xk=sz10),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f180])).
% 17.99/2.80 fof(f182,plain,(
% 17.99/2.80 ~doDivides0(xp,xn)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f180])).
% 17.99/2.80 fof(f183,plain,(
% 17.99/2.80 ~doDivides0(xp,xm)),
% 17.99/2.80 inference(cnf_transformation,[status(thm)],[f180])).
% 17.99/2.80 fof(f184,definition,(
% 17.99/2.80 sQ0_spl <=> (xk=sz00)),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f185,plain,(
% 17.99/2.80 xk=sz00|~sQ0_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f184])).
% 17.99/2.80 fof(f187,definition,(
% 17.99/2.80 sQ1_spl <=> (xk=sz10)),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f188,plain,(
% 17.99/2.80 xk=sz10|~sQ1_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f187])).
% 17.99/2.80 fof(f190,plain,(
% 17.99/2.80 sQ0_spl|sQ1_spl),
% 17.99/2.80 inference(split_clause,[status(thm)],[f181,f184,f187])).
% 17.99/2.80 fof(f220,plain,(
% 17.99/2.80 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtasdt0(xn,X0)))),
% 17.99/2.80 inference(resolution,[status(thm)],[f57,f166])).
% 17.99/2.80 fof(f266,definition,(
% 17.99/2.80 sQ2_spl <=> (aNaturalNumber0(xp))),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f268,plain,(
% 17.99/2.80 ~aNaturalNumber0(xp)|sQ2_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f266])).
% 17.99/2.80 fof(f269,definition,(
% 17.99/2.80 sQ3_spl <=> (xp=sz00)),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f270,plain,(
% 17.99/2.80 xp=sz00|~sQ3_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f269])).
% 17.99/2.80 fof(f272,definition,(
% 17.99/2.80 sQ4_spl <=> (aNaturalNumber0(sz00))),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f274,plain,(
% 17.99/2.80 ~aNaturalNumber0(sz00)|sQ4_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f272])).
% 17.99/2.80 fof(f286,definition,(
% 17.99/2.80 sQ8_spl <=> (aNaturalNumber0(xm))),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f288,plain,(
% 17.99/2.80 ~aNaturalNumber0(xm)|sQ8_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f286])).
% 17.99/2.80 fof(f289,definition,(
% 17.99/2.80 sQ9_spl <=> (xm=sz00)),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f290,plain,(
% 17.99/2.80 xm=sz00|~sQ9_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f289])).
% 17.99/2.80 fof(f300,definition,(
% 17.99/2.80 sQ12_spl <=> (aNaturalNumber0(xn))),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f302,plain,(
% 17.99/2.80 ~aNaturalNumber0(xn)|sQ12_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f300])).
% 17.99/2.80 fof(f303,definition,(
% 17.99/2.80 sQ13_spl <=> (xn=sz00)),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f304,plain,(
% 17.99/2.80 xn=sz00|~sQ13_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f303])).
% 17.99/2.80 fof(f385,plain,(
% 17.99/2.80 $false|sQ4_spl),
% 17.99/2.80 inference(forward_subsumption_resolution,[status(thm)],[f274,f51])).
% 17.99/2.80 fof(f386,plain,(
% 17.99/2.80 sQ4_spl),
% 17.99/2.80 inference(contradiction_clause,[status(thm)],[f385])).
% 17.99/2.80 fof(f389,plain,(
% 17.99/2.80 $false|sQ2_spl),
% 17.99/2.80 inference(forward_subsumption_resolution,[status(thm)],[f268,f168])).
% 17.99/2.80 fof(f390,plain,(
% 17.99/2.80 sQ2_spl),
% 17.99/2.80 inference(contradiction_clause,[status(thm)],[f389])).
% 17.99/2.80 fof(f391,plain,(
% 17.99/2.80 $false|sQ8_spl),
% 17.99/2.80 inference(forward_subsumption_resolution,[status(thm)],[f288,f167])).
% 17.99/2.80 fof(f392,plain,(
% 17.99/2.80 sQ8_spl),
% 17.99/2.80 inference(contradiction_clause,[status(thm)],[f391])).
% 17.99/2.80 fof(f393,plain,(
% 17.99/2.80 $false|sQ12_spl),
% 17.99/2.80 inference(forward_subsumption_resolution,[status(thm)],[f302,f166])).
% 17.99/2.80 fof(f394,plain,(
% 17.99/2.80 sQ12_spl),
% 17.99/2.80 inference(contradiction_clause,[status(thm)],[f393])).
% 17.99/2.80 fof(f442,plain,(
% 17.99/2.80 ~doDivides0(xp,sz00)|~sQ13_spl),
% 17.99/2.80 inference(forward_demodulation,[status(thm)],[f304,f182])).
% 17.99/2.80 fof(f532,plain,(
% 17.99/2.80 sdtlseqdt0(xm,sz00)|~sQ3_spl),
% 17.99/2.80 inference(forward_demodulation,[status(thm)],[f270,f178])).
% 17.99/2.80 fof(f552,plain,(
% 17.99/2.80 xm=sdtpldt0(sz00,xm)),
% 17.99/2.80 inference(resolution,[status(thm)],[f64,f167])).
% 17.99/2.80 fof(f562,definition,(
% 17.99/2.80 sQ34_spl <=> (xn=sz10)),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f563,plain,(
% 17.99/2.80 xn=sz10|~sQ34_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f562])).
% 17.99/2.80 fof(f662,plain,(
% 17.99/2.80 sz00=sdtasdt0(sz00,xm)),
% 17.99/2.80 inference(resolution,[status(thm)],[f167,f74])).
% 17.99/2.80 fof(f686,plain,(
% 17.99/2.80 sdtasdt0(xp,sz00)=sz00),
% 17.99/2.80 inference(resolution,[status(thm)],[f168,f73])).
% 17.99/2.80 fof(f809,plain,(
% 17.99/2.80 xm=sdtasdt0(sz10,xm)),
% 17.99/2.80 inference(resolution,[status(thm)],[f167,f71])).
% 17.99/2.80 fof(f975,plain,(
% 17.99/2.80 sdtasdt0(xp,sz10)=xp),
% 17.99/2.80 inference(resolution,[status(thm)],[f168,f70])).
% 17.99/2.80 fof(f994,plain,(
% 17.99/2.80 sz00=sdtsldt0(sdtasdt0(xn,xm),xp)|~sQ0_spl),
% 17.99/2.80 inference(forward_demodulation,[status(thm)],[f185,f179])).
% 17.99/2.80 fof(f1290,plain,(
% 17.99/2.80 ~aNaturalNumber0(sz00)|~aNaturalNumber0(xm)|~sdtlseqdt0(sz00,xm)|sz00=xm|~sQ3_spl),
% 17.99/2.80 inference(resolution,[status(thm)],[f104,f532])).
% 17.99/2.80 fof(f1295,definition,(
% 17.99/2.80 sQ88_spl <=> (sdtlseqdt0(sz00,xm))),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f1298,plain,(
% 17.99/2.80 ~sQ4_spl|~sQ8_spl|~sQ88_spl|sQ9_spl|~sQ3_spl),
% 17.99/2.80 inference(split_clause,[status(thm)],[f1290,f272,f286,f1295,f289,f269])).
% 17.99/2.80 fof(f2337,definition,(
% 17.99/2.80 sQ197_spl <=> (doDivides0(xp,sz00))),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f2338,plain,(
% 17.99/2.80 doDivides0(xp,sz00)|~sQ197_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f2337])).
% 17.99/2.80 fof(f2449,plain,(
% 17.99/2.80 doDivides0(xp,sdtasdt0(sz00,xm))|~sQ13_spl),
% 17.99/2.80 inference(forward_demodulation,[status(thm)],[f304,f172])).
% 17.99/2.80 fof(f2657,plain,(
% 17.99/2.80 ~aNaturalNumber0(sz00)|~aNaturalNumber0(xm)|sdtlseqdt0(sz00,xm)|~aNaturalNumber0(xm)),
% 17.99/2.80 inference(resolution,[status(thm)],[f552,f94])).
% 17.99/2.80 fof(f2666,plain,(
% 17.99/2.80 ~sQ4_spl|~sQ8_spl|sQ88_spl),
% 17.99/2.80 inference(split_clause,[status(thm)],[f2657,f272,f286,f1295])).
% 17.99/2.80 fof(f3058,plain,(
% 17.99/2.80 doDivides0(xp,sz00)|~sQ13_spl),
% 17.99/2.80 inference(backward_demodulation,[status(thm)],[f662,f2449])).
% 17.99/2.80 fof(f3071,plain,(
% 17.99/2.80 $false|~sQ13_spl),
% 17.99/2.80 inference(forward_subsumption_resolution,[status(thm)],[f3058,f442])).
% 17.99/2.80 fof(f3072,plain,(
% 17.99/2.80 ~sQ13_spl),
% 17.99/2.80 inference(contradiction_clause,[status(thm)],[f3071])).
% 17.99/2.80 fof(f3212,plain,(
% 17.99/2.80 ~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xn,xm))|xp=sz00|~doDivides0(xp,sdtasdt0(xn,xm))|sdtasdt0(xn,xm)=sdtasdt0(xp,sz00)|~sQ0_spl),
% 17.99/2.80 inference(resolution,[status(thm)],[f994,f139])).
% 17.99/2.80 fof(f3216,definition,(
% 17.99/2.80 sQ280_spl <=> (aNaturalNumber0(sdtasdt0(xn,xm)))),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f3218,plain,(
% 17.99/2.80 ~aNaturalNumber0(sdtasdt0(xn,xm))|sQ280_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f3216])).
% 17.99/2.80 fof(f3219,definition,(
% 17.99/2.80 sQ281_spl <=> (doDivides0(xp,sdtasdt0(xn,xm)))),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ281_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f3221,plain,(
% 17.99/2.80 ~doDivides0(xp,sdtasdt0(xn,xm))|sQ281_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f3219])).
% 17.99/2.80 fof(f3222,definition,(
% 17.99/2.80 sQ282_spl <=> (sdtasdt0(xn,xm)=sdtasdt0(xp,sz00))),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f3223,plain,(
% 17.99/2.80 sdtasdt0(xn,xm)=sdtasdt0(xp,sz00)|~sQ282_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f3222])).
% 17.99/2.80 fof(f3225,plain,(
% 17.99/2.80 ~sQ2_spl|~sQ280_spl|sQ3_spl|~sQ281_spl|sQ282_spl|~sQ0_spl),
% 17.99/2.80 inference(split_clause,[status(thm)],[f3212,f266,f3216,f269,f3219,f3222,f184])).
% 17.99/2.80 fof(f3315,definition,(
% 17.99/2.80 sQ286_spl <=> (xn=xp)),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ286_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f3316,plain,(
% 17.99/2.80 xn=xp|~sQ286_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f3315])).
% 17.99/2.80 fof(f3343,plain,(
% 17.99/2.80 $false|~sQ286_spl),
% 17.99/2.80 inference(forward_subsumption_resolution,[status(thm)],[f3316,f175])).
% 17.99/2.80 fof(f3344,plain,(
% 17.99/2.80 ~sQ286_spl),
% 17.99/2.80 inference(contradiction_clause,[status(thm)],[f3343])).
% 17.99/2.80 fof(f3460,definition,(
% 17.99/2.80 sQ306_spl <=> (isPrime0(xp))),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ306_spl])],[split_symbol_definition])).
% 17.99/2.80 fof(f3462,plain,(
% 17.99/2.80 ~isPrime0(xp)|sQ306_spl),
% 17.99/2.80 inference(component_clause,[status(thm)],[f3460])).
% 17.99/2.80 fof(f4250,plain,(
% 17.99/2.80 ~doDivides0(xp,sz00)|~sQ9_spl),
% 17.99/2.80 inference(forward_demodulation,[status(thm)],[f290,f183])).
% 17.99/2.80 fof(f4309,plain,(
% 17.99/2.80 doDivides0(xp,sdtasdt0(sz10,xm))|~sQ34_spl),
% 17.99/2.80 inference(forward_demodulation,[status(thm)],[f563,f172])).
% 17.99/2.80 fof(f4673,plain,(
% 17.99/2.80 ~aNaturalNumber0(xp)|~aNaturalNumber0(sz00)|doDivides0(xp,sz00)|~aNaturalNumber0(sz00)),
% 17.99/2.80 inference(resolution,[status(thm)],[f686,f134])).
% 17.99/2.80 fof(f4681,plain,(
% 17.99/2.80 ~sQ2_spl|~sQ4_spl|sQ197_spl),
% 17.99/2.80 inference(split_clause,[status(thm)],[f4673,f266,f272,f2337])).
% 17.99/2.80 fof(f4773,plain,(
% 17.99/2.80 $false|~sQ197_spl|~sQ9_spl),
% 17.99/2.80 inference(forward_subsumption_resolution,[status(thm)],[f4250,f2338])).
% 17.99/2.80 fof(f4774,plain,(
% 17.99/2.80 ~sQ197_spl|~sQ9_spl),
% 17.99/2.80 inference(contradiction_clause,[status(thm)],[f4773])).
% 17.99/2.80 fof(f6236,plain,(
% 17.99/2.80 doDivides0(xp,xm)|~sQ34_spl),
% 17.99/2.80 inference(backward_demodulation,[status(thm)],[f809,f4309])).
% 17.99/2.80 fof(f6240,plain,(
% 17.99/2.80 $false|~sQ34_spl),
% 17.99/2.80 inference(forward_subsumption_resolution,[status(thm)],[f6236,f183])).
% 17.99/2.80 fof(f6241,plain,(
% 17.99/2.80 ~sQ34_spl),
% 17.99/2.80 inference(contradiction_clause,[status(thm)],[f6240])).
% 17.99/2.80 fof(f6277,plain,(
% 17.99/2.80 sdtasdt0(xn,xm)=sz00|~sQ282_spl),
% 17.99/2.80 inference(forward_demodulation,[status(thm)],[f686,f3223])).
% 17.99/2.80 fof(f10255,plain,(
% 17.99/2.80 aNaturalNumber0(sdtasdt0(xn,xm))),
% 17.99/2.80 inference(resolution,[status(thm)],[f220,f167])).
% 17.99/2.80 fof(f10267,plain,(
% 17.99/2.80 $false|sQ280_spl),
% 17.99/2.80 inference(forward_subsumption_resolution,[status(thm)],[f10255,f3218])).
% 17.99/2.80 fof(f10268,plain,(
% 17.99/2.80 sQ280_spl),
% 17.99/2.80 inference(contradiction_clause,[status(thm)],[f10267])).
% 17.99/2.80 fof(f10271,plain,(
% 17.99/2.80 $false|sQ281_spl),
% 17.99/2.80 inference(forward_subsumption_resolution,[status(thm)],[f3221,f172])).
% 17.99/2.80 fof(f10272,plain,(
% 17.99/2.80 sQ281_spl),
% 17.99/2.80 inference(contradiction_clause,[status(thm)],[f10271])).
% 17.99/2.80 fof(f10294,plain,(
% 17.99/2.80 sz10=sdtsldt0(sdtasdt0(xn,xm),xp)|~sQ1_spl),
% 17.99/2.80 inference(backward_demodulation,[status(thm)],[f188,f179])).
% 17.99/2.80 fof(f10537,plain,(
% 17.99/2.80 ~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xn,xm))|xp=sz00|~doDivides0(xp,sdtasdt0(xn,xm))|sdtasdt0(xn,xm)=sdtasdt0(xp,sz10)|~sQ1_spl),
% 17.99/2.80 inference(resolution,[status(thm)],[f10294,f139])).
% 17.99/2.80 fof(f10541,definition,(
% 17.99/2.80 sQ903_spl <=> (sdtasdt0(xn,xm)=sdtasdt0(xp,sz10))),
% 17.99/2.80 introduced(definition,[new_symbols(definition,[sQ903_spl])],[split_symbol_definition])).
% 17.99/2.81 fof(f10542,plain,(
% 17.99/2.81 sdtasdt0(xn,xm)=sdtasdt0(xp,sz10)|~sQ903_spl),
% 17.99/2.81 inference(component_clause,[status(thm)],[f10541])).
% 17.99/2.81 fof(f10544,plain,(
% 17.99/2.81 ~sQ2_spl|~sQ280_spl|sQ3_spl|~sQ281_spl|sQ903_spl|~sQ1_spl),
% 17.99/2.81 inference(split_clause,[status(thm)],[f10537,f266,f3216,f269,f3219,f10541,f187])).
% 17.99/2.81 fof(f10553,plain,(
% 17.99/2.81 sdtasdt0(xn,xm)=xp|~sQ903_spl),
% 17.99/2.81 inference(forward_demodulation,[status(thm)],[f975,f10542])).
% 17.99/2.81 fof(f11796,plain,(
% 17.99/2.81 ~aNaturalNumber0(xn)|~aNaturalNumber0(xp)|doDivides0(xn,xp)|~aNaturalNumber0(xm)|~sQ903_spl),
% 17.99/2.81 inference(resolution,[status(thm)],[f10553,f134])).
% 17.99/2.81 fof(f11803,definition,(
% 17.99/2.81 sQ1005_spl <=> (doDivides0(xn,xp))),
% 17.99/2.81 introduced(definition,[new_symbols(definition,[sQ1005_spl])],[split_symbol_definition])).
% 17.99/2.81 fof(f11804,plain,(
% 17.99/2.81 doDivides0(xn,xp)|~sQ1005_spl),
% 17.99/2.81 inference(component_clause,[status(thm)],[f11803])).
% 17.99/2.81 fof(f11806,plain,(
% 17.99/2.81 ~sQ12_spl|~sQ2_spl|sQ1005_spl|~sQ8_spl|~sQ903_spl),
% 17.99/2.81 inference(split_clause,[status(thm)],[f11796,f300,f266,f11803,f286,f10541])).
% 17.99/2.81 fof(f11824,plain,(
% 17.99/2.81 ~aNaturalNumber0(xp)|~isPrime0(xp)|~aNaturalNumber0(xn)|xn=sz10|xn=xp|~sQ1005_spl),
% 17.99/2.81 inference(resolution,[status(thm)],[f11804,f156])).
% 17.99/2.81 fof(f11837,plain,(
% 17.99/2.81 ~sQ2_spl|~sQ306_spl|~sQ12_spl|sQ34_spl|sQ286_spl|~sQ1005_spl),
% 17.99/2.81 inference(split_clause,[status(thm)],[f11824,f266,f3460,f300,f562,f3315,f11803])).
% 17.99/2.81 fof(f11854,plain,(
% 17.99/2.81 $false|sQ306_spl),
% 17.99/2.81 inference(forward_subsumption_resolution,[status(thm)],[f3462,f171])).
% 17.99/2.81 fof(f11855,plain,(
% 17.99/2.81 sQ306_spl),
% 17.99/2.81 inference(contradiction_clause,[status(thm)],[f11854])).
% 17.99/2.81 fof(f13746,plain,(
% 17.99/2.81 ~aNaturalNumber0(xn)|~aNaturalNumber0(xm)|xn=sz00|xm=sz00|~sQ282_spl),
% 17.99/2.81 inference(resolution,[status(thm)],[f6277,f88])).
% 17.99/2.81 fof(f13756,plain,(
% 17.99/2.81 ~sQ12_spl|~sQ8_spl|sQ13_spl|sQ9_spl|~sQ282_spl),
% 17.99/2.81 inference(split_clause,[status(thm)],[f13746,f300,f286,f303,f289,f3222])).
% 17.99/2.81 fof(f13772,plain,(
% 17.99/2.81 $false),
% 17.99/2.81 inference(sat_refutation,[status(thm)],[f190,f386,f390,f392,f394,f1298,f2666,f3072,f3225,f3344,f4681,f4774,f6241,f10268,f10272,f10544,f11806,f11837,f11855,f13756])).
% 17.99/2.81 % SZS output end CNFRefutation for theBenchmark.p
% 12.76/2.84 % Elapsed time: 2.457536 seconds
% 12.76/2.84 % CPU time: 18.948285 seconds
% 12.76/2.84 % Total memory used: 212.898 MB
% 12.76/2.84 % Net memory used: 202.329 MB
%------------------------------------------------------------------------------