%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM504+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 : n004.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 0.21s 1.09s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM504+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.48 % Computer : n004.cluster.edu
% 0.17/0.48 % Model : x86_64 x86_64
% 0.17/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.48 % Memory : 8046.5625MB
% 0.17/0.48 % OS : Linux 6.8.0-71-generic
% 0.17/0.48 % CPULimit : 300
% 0.17/0.48 % WCLimit : 300
% 0.17/0.48 % DateTime : Mon Sep 21 02:35:50 UTC 2026
% 0.17/0.48 % CPUTime :
% 0.17/0.53 % Drodi V4.1.1
% 0.21/1.09 % Refutation found
% 0.21/1.09 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/1.09 % SZS output start CNFRefutation for theBenchmark
% 0.21/1.09 fof(f2,axiom,(
% 0.21/1.09 aNaturalNumber0(sz00) ),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f3,axiom,(
% 0.21/1.09 ( aNaturalNumber0(sz10)& sz10 != sz00 ) ),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f4,axiom,(
% 0.21/1.09 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtpldt0(W0,W1)) ) )),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f5,axiom,(
% 0.21/1.09 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtasdt0(W0,W1)) ) )),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f18,definition,(
% 0.21/1.09 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( sdtlseqdt0(W0,W1)<=> (? [W2] :( aNaturalNumber0(W2)& sdtpldt0(W0,W2) = W1 ) )) ) )),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f21,axiom,(
% 0.21/1.09 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W1,W0) )=> W0 = W1 ) ) )),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f37,definition,(
% 0.21/1.09 (! [W0] :( aNaturalNumber0(W0)=> ( isPrime0(W0)<=> ( W0 != sz00& W0 != sz10& (! [W1] :( ( aNaturalNumber0(W1)& doDivides0(W1,W0) )=> ( W1 = sz10| W1 = W0 ) ) )) ) ) )),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f39,hypothesis,(
% 0.21/1.09 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp) ) ),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f41,hypothesis,(
% 0.21/1.09 ( xp != sz00& xp != sz10& (! [W0] :( ( aNaturalNumber0(W0)& ( (? [W1] :( aNaturalNumber0(W1)& xp = sdtasdt0(W0,W1) ))| doDivides0(W0,xp) ) )=> ( W0 = sz10| W0 = xp ) ))& isPrime0(xp)& (? [W0] :( aNaturalNumber0(W0)& sdtasdt0(xn,xm) = sdtasdt0(xp,W0) ))& doDivides0(xp,sdtasdt0(xn,xm)) ) ),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f45,hypothesis,(
% 0.21/1.09 ( aNaturalNumber0(xk)& sdtasdt0(xn,xm) = sdtasdt0(xp,xk)& xk = sdtsldt0(sdtasdt0(xn,xm),xp) ) ),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f48,hypothesis,(
% 0.21/1.09 ( aNaturalNumber0(xr)& (? [W0] :( aNaturalNumber0(W0)& xk = sdtasdt0(xr,W0) ))& doDivides0(xr,xk)& xr != sz00& xr != sz10& (! [W0] :( ( aNaturalNumber0(W0)& ( (? [W1] :( aNaturalNumber0(W1)& xr = sdtasdt0(W0,W1) ))| doDivides0(W0,xr) ) )=> ( W0 = sz10| W0 = xr ) ))& isPrime0(xr) ) ),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f49,hypothesis,(
% 0.21/1.09 ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xr,W0) = xk ))& (? [W0] :( aNaturalNumber0(W0)& sdtasdt0(xn,xm) = sdtasdt0(xr,W0) ))& doDivides0(xr,sdtasdt0(xn,xm)) ) ),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f50,hypothesis,(
% 0.21/1.09 ( (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xp,W0) = xk ))& sdtlseqdt0(xp,xk) ) ),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f51,hypothesis,(
% 0.21/1.09 ( sdtasdt0(xn,xm) != sdtasdt0(xp,xm)& (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(sdtasdt0(xn,xm),W0) = sdtasdt0(xp,xm) ))& sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))& sdtasdt0(xp,xm) != sdtasdt0(xp,xk)& (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(sdtasdt0(xp,xm),W0) = sdtasdt0(xp,xk) ))& sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk)) ) ),
% 0.21/1.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/1.09 fof(f57,plain,(
% 0.21/1.09 aNaturalNumber0(sz00)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f2])).
% 0.21/1.09 fof(f58,plain,(
% 0.21/1.09 aNaturalNumber0(sz10)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f3])).
% 0.21/1.09 fof(f60,plain,(
% 0.21/1.09 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtpldt0(W0,W1)))),
% 0.21/1.09 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.21/1.09 fof(f61,plain,(
% 0.21/1.09 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtpldt0(X0,X1)))),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f60])).
% 0.21/1.09 fof(f62,plain,(
% 0.21/1.09 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtasdt0(W0,W1)))),
% 0.21/1.09 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.21/1.09 fof(f63,plain,(
% 0.21/1.09 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtasdt0(X0,X1)))),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f62])).
% 0.21/1.09 fof(f95,plain,(
% 0.21/1.09 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(sdtlseqdt0(W0,W1)<=>(?[W2]: (aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1))))),
% 0.21/1.09 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.21/1.09 fof(f96,plain,(
% 0.21/1.09 ![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)))))),
% 0.21/1.09 inference(NNF_transformation,[status(thm)],[f95])).
% 0.21/1.09 fof(f97,plain,(
% 0.21/1.09 ![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)))))),
% 0.21/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W2,sK0_skl(W1,W0))],[f96])).
% 0.21/1.09 fof(f100,plain,(
% 0.21/1.09 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtlseqdt0(X0,X1)|~aNaturalNumber0(X2)|~sdtpldt0(X0,X2)=X1)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f97])).
% 0.21/1.09 fof(f109,plain,(
% 0.21/1.09 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W0))|W0=W1))),
% 0.21/1.09 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.21/1.09 fof(f110,plain,(
% 0.21/1.09 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X1,X0)|X0=X1)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f109])).
% 0.21/1.09 fof(f157,plain,(
% 0.21/1.09 ![W0]: (~aNaturalNumber0(W0)|(isPrime0(W0)<=>((~W0=sz00&~W0=sz10)&(![W1]: ((~aNaturalNumber0(W1)|~doDivides0(W1,W0))|(W1=sz10|W1=W0))))))),
% 0.21/1.09 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.21/1.09 fof(f158,plain,(
% 0.21/1.09 ![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)))))))),
% 0.21/1.09 inference(NNF_transformation,[status(thm)],[f157])).
% 0.21/1.09 fof(f159,plain,(
% 0.21/1.09 ![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))))))),
% 0.21/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W1,sK2_skl(W0))],[f158])).
% 0.21/1.09 fof(f160,plain,(
% 0.21/1.09 ![X0]: (~aNaturalNumber0(X0)|~isPrime0(X0)|~X0=sz00)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f159])).
% 0.21/1.09 fof(f161,plain,(
% 0.21/1.09 ![X0]: (~aNaturalNumber0(X0)|~isPrime0(X0)|~X0=sz10)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f159])).
% 0.21/1.09 fof(f174,plain,(
% 0.21/1.09 aNaturalNumber0(xp)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f39])).
% 0.21/1.09 fof(f186,plain,(
% 0.21/1.09 ((((~xp=sz00&~xp=sz10)&(![W0]: ((~aNaturalNumber0(W0)|((![W1]: (~aNaturalNumber0(W1)|~xp=sdtasdt0(W0,W1)))&~doDivides0(W0,xp)))|(W0=sz10|W0=xp))))&isPrime0(xp))&(?[W0]: (aNaturalNumber0(W0)&sdtasdt0(xn,xm)=sdtasdt0(xp,W0))))&doDivides0(xp,sdtasdt0(xn,xm))),
% 0.21/1.09 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.21/1.09 fof(f187,plain,(
% 0.21/1.09 ((((~xp=sz00&~xp=sz10)&(![W0]: ((~aNaturalNumber0(W0)|((![W1]: (~aNaturalNumber0(W1)|~xp=sdtasdt0(W0,W1)))&~doDivides0(W0,xp)))|(W0=sz10|W0=xp))))&isPrime0(xp))&(aNaturalNumber0(sK5_skl)&sdtasdt0(xn,xm)=sdtasdt0(xp,sK5_skl)))&doDivides0(xp,sdtasdt0(xn,xm))),
% 0.21/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(W0,sK5_skl)],[f186])).
% 0.21/1.09 fof(f193,plain,(
% 0.21/1.09 aNaturalNumber0(sK5_skl)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f187])).
% 0.21/1.09 fof(f212,plain,(
% 0.21/1.09 sdtasdt0(xn,xm)=sdtasdt0(xp,xk)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f45])).
% 0.21/1.09 fof(f219,plain,(
% 0.21/1.09 (((((aNaturalNumber0(xr)&(?[W0]: (aNaturalNumber0(W0)&xk=sdtasdt0(xr,W0))))&doDivides0(xr,xk))&~xr=sz00)&~xr=sz10)&(![W0]: ((~aNaturalNumber0(W0)|((![W1]: (~aNaturalNumber0(W1)|~xr=sdtasdt0(W0,W1)))&~doDivides0(W0,xr)))|(W0=sz10|W0=xr))))&isPrime0(xr)),
% 0.21/1.09 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 0.21/1.09 fof(f220,plain,(
% 0.21/1.09 (((((aNaturalNumber0(xr)&(aNaturalNumber0(sK8_skl)&xk=sdtasdt0(xr,sK8_skl)))&doDivides0(xr,xk))&~xr=sz00)&~xr=sz10)&(![W0]: ((~aNaturalNumber0(W0)|((![W1]: (~aNaturalNumber0(W1)|~xr=sdtasdt0(W0,W1)))&~doDivides0(W0,xr)))|(W0=sz10|W0=xr))))&isPrime0(xr)),
% 0.21/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(W0,sK8_skl)],[f219])).
% 0.21/1.09 fof(f223,plain,(
% 0.21/1.09 xk=sdtasdt0(xr,sK8_skl)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f220])).
% 0.21/1.09 fof(f224,plain,(
% 0.21/1.09 doDivides0(xr,xk)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f220])).
% 0.21/1.09 fof(f226,plain,(
% 0.21/1.09 ~xr=sz10),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f220])).
% 0.21/1.09 fof(f230,plain,(
% 0.21/1.09 ((aNaturalNumber0(sK9_skl)&sdtpldt0(xr,sK9_skl)=xk)&(aNaturalNumber0(sK10_skl)&sdtasdt0(xn,xm)=sdtasdt0(xr,sK10_skl)))&doDivides0(xr,sdtasdt0(xn,xm))),
% 0.21/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,sK10_skl]),skolemize(W0,sK9_skl),skolemize(W0,sK10_skl)],[f49])).
% 0.21/1.09 fof(f234,plain,(
% 0.21/1.09 sdtasdt0(xn,xm)=sdtasdt0(xr,sK10_skl)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f230])).
% 0.21/1.09 fof(f236,plain,(
% 0.21/1.09 (aNaturalNumber0(sK11_skl)&sdtpldt0(xp,sK11_skl)=xk)&sdtlseqdt0(xp,xk)),
% 0.21/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(W0,sK11_skl)],[f50])).
% 0.21/1.09 fof(f237,plain,(
% 0.21/1.09 aNaturalNumber0(sK11_skl)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f236])).
% 0.21/1.09 fof(f238,plain,(
% 0.21/1.09 sdtpldt0(xp,sK11_skl)=xk),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f236])).
% 0.21/1.09 fof(f240,plain,(
% 0.21/1.09 ((((~sdtasdt0(xn,xm)=sdtasdt0(xp,xm)&(aNaturalNumber0(sK12_skl)&sdtpldt0(sdtasdt0(xn,xm),sK12_skl)=sdtasdt0(xp,xm)))&sdtlseqdt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm)))&~sdtasdt0(xp,xm)=sdtasdt0(xp,xk))&(aNaturalNumber0(sK13_skl)&sdtpldt0(sdtasdt0(xp,xm),sK13_skl)=sdtasdt0(xp,xk)))&sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk))),
% 0.21/1.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(W0,sK12_skl),skolemize(W0,sK13_skl)],[f51])).
% 0.21/1.09 fof(f241,plain,(
% 0.21/1.09 ~sdtasdt0(xn,xm)=sdtasdt0(xp,xm)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f240])).
% 0.21/1.09 fof(f242,plain,(
% 0.21/1.09 aNaturalNumber0(sK12_skl)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f240])).
% 0.21/1.09 fof(f243,plain,(
% 0.21/1.09 sdtpldt0(sdtasdt0(xn,xm),sK12_skl)=sdtasdt0(xp,xm)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f240])).
% 0.21/1.09 fof(f245,plain,(
% 0.21/1.09 ~sdtasdt0(xp,xm)=sdtasdt0(xp,xk)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f240])).
% 0.21/1.09 fof(f246,plain,(
% 0.21/1.09 aNaturalNumber0(sK13_skl)),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f240])).
% 0.21/1.09 fof(f248,plain,(
% 0.21/1.09 sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xp,xk))),
% 0.21/1.09 inference(cnf_transformation,[status(thm)],[f240])).
% 0.21/1.09 fof(f269,plain,(
% 0.21/1.09 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(sdtpldt0(X0,X1))|sdtlseqdt0(X0,sdtpldt0(X0,X1))|~aNaturalNumber0(X1))),
% 0.21/1.09 inference(destructive_equality_resolution,[status(thm)],[f100])).
% 0.21/1.09 fof(f279,plain,(
% 0.21/1.09 ~aNaturalNumber0(sz00)|~isPrime0(sz00)),
% 0.21/1.09 inference(destructive_equality_resolution,[status(thm)],[f160])).
% 0.21/1.09 fof(f280,plain,(
% 0.21/1.09 ~aNaturalNumber0(sz10)|~isPrime0(sz10)),
% 0.21/1.09 inference(destructive_equality_resolution,[status(thm)],[f161])).
% 0.21/1.09 fof(f465,plain,(
% 0.21/1.09 ![X0,X1]: (~aNaturalNumber0(X0)|sdtlseqdt0(X0,sdtpldt0(X0,X1))|~aNaturalNumber0(X1))),
% 0.21/1.09 inference(forward_subsumption_resolution,[status(thm)],[f269,f61])).
% 0.21/1.09 fof(f554,plain,(
% 0.21/1.09 ~isPrime0(sz00)),
% 0.21/1.09 inference(forward_subsumption_resolution,[status(thm)],[f279,f57])).
% 0.21/1.09 fof(f555,plain,(
% 0.21/1.09 ~isPrime0(sz10)),
% 0.21/1.09 inference(forward_subsumption_resolution,[status(thm)],[f280,f58])).
% 0.21/1.09 fof(f560,definition,(
% 0.21/1.09 sQ16_spl <=> (isPrime0(sz10))),
% 0.21/1.09 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.21/1.09 fof(f561,plain,(
% 0.21/1.09 isPrime0(sz10)|~sQ16_spl),
% 0.21/1.09 inference(component_clause,[status(thm)],[f560])).
% 0.21/1.09 fof(f567,definition,(
% 0.21/1.09 sQ18_spl <=> (isPrime0(sz00))),
% 0.21/1.09 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.21/1.09 fof(f568,plain,(
% 0.21/1.09 isPrime0(sz00)|~sQ18_spl),
% 0.21/1.09 inference(component_clause,[status(thm)],[f567])).
% 0.21/1.09 fof(f926,definition,(
% 0.21/1.09 sQ70_spl <=> (aNaturalNumber0(xp))),
% 0.21/1.09 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.21/1.09 fof(f928,plain,(
% 0.21/1.09 ~aNaturalNumber0(xp)|sQ70_spl),
% 0.21/1.09 inference(component_clause,[status(thm)],[f926])).
% 0.21/1.09 fof(f933,plain,(
% 0.21/1.09 $false|sQ70_spl),
% 0.21/1.09 inference(forward_subsumption_resolution,[status(thm)],[f928,f174])).
% 0.21/1.09 fof(f934,plain,(
% 0.21/1.09 sQ70_spl),
% 0.21/1.09 inference(contradiction_clause,[status(thm)],[f933])).
% 0.21/1.09 fof(f1081,definition,(
% 0.21/1.09 sQ93_spl <=> (aNaturalNumber0(sK5_skl))),
% 0.21/1.09 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 0.21/1.09 fof(f1083,plain,(
% 0.21/1.09 ~aNaturalNumber0(sK5_skl)|sQ93_spl),
% 0.21/1.09 inference(component_clause,[status(thm)],[f1081])).
% 0.21/1.09 fof(f1750,definition,(
% 0.21/1.09 sQ195_spl <=> (xr=sz10)),
% 0.21/1.09 introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition])).
% 0.21/1.09 fof(f1751,plain,(
% 0.21/1.09 xr=sz10|~sQ195_spl),
% 0.21/1.09 inference(component_clause,[status(thm)],[f1750])).
% 0.21/1.09 fof(f1926,definition,(
% 0.21/1.09 sQ227_spl <=> (aNaturalNumber0(xk))),
% 0.21/1.09 introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition])).
% 0.21/1.09 fof(f2255,plain,(
% 0.21/1.09 sdtasdt0(xr,sK10_skl)=sdtasdt0(xp,xk)),
% 0.21/1.09 inference(backward_demodulation,[status(thm)],[f234,f212])).
% 0.21/1.09 fof(f2271,definition,(
% 0.21/1.09 sQ277_spl <=> (aNaturalNumber0(sdtasdt0(xr,sK10_skl)))),
% 0.21/1.09 introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition])).
% 0.21/1.09 fof(f2440,plain,(
% 0.21/1.09 ~aNaturalNumber0(xp)|~aNaturalNumber0(sK11_skl)|aNaturalNumber0(xk)),
% 0.21/1.09 inference(paramodulation,[status(thm)],[f238,f61])).
% 0.21/1.09 fof(f2441,definition,(
% 0.21/1.09 sQ303_spl <=> (aNaturalNumber0(sK11_skl))),
% 0.21/1.09 introduced(definition,[new_symbols(definition,[sQ303_spl])],[split_symbol_definition])).
% 0.21/1.09 fof(f2443,plain,(
% 0.21/1.09 ~aNaturalNumber0(sK11_skl)|sQ303_spl),
% 0.21/1.09 inference(component_clause,[status(thm)],[f2441])).
% 0.21/1.09 fof(f2485,plain,(
% 0.21/1.09 ~sQ70_spl|~sQ303_spl|sQ227_spl),
% 0.21/1.09 inference(split_clause,[status(thm)],[f2440,f926,f2441,f1926])).
% 0.21/1.09 fof(f2486,plain,(
% 0.21/1.09 $false|sQ303_spl),
% 0.21/1.09 inference(forward_subsumption_resolution,[status(thm)],[f2443,f237])).
% 0.21/1.09 fof(f2487,plain,(
% 0.21/1.09 sQ303_spl),
% 0.21/1.09 inference(contradiction_clause,[status(thm)],[f2486])).
% 0.21/1.09 fof(f2547,plain,(
% 0.21/1.09 ~sdtasdt0(xr,sK10_skl)=sdtasdt0(xp,xm)),
% 0.21/1.09 inference(forward_demodulation,[status(thm)],[f234,f241])).
% 0.21/1.09 fof(f2650,plain,(
% 0.21/1.09 sdtpldt0(sdtasdt0(xr,sK10_skl),sK12_skl)=sdtasdt0(xp,xm)),
% 0.21/1.09 inference(forward_demodulation,[status(thm)],[f234,f243])).
% 0.21/1.09 fof(f2659,plain,(
% 0.21/1.09 ~aNaturalNumber0(sdtasdt0(xr,sK10_skl))|sdtlseqdt0(sdtasdt0(xr,sK10_skl),sdtasdt0(xp,xm))|~aNaturalNumber0(sK12_skl)),
% 0.21/1.09 inference(paramodulation,[status(thm)],[f2650,f465])).
% 0.21/1.09 fof(f2662,plain,(
% 0.21/1.09 ~aNaturalNumber0(sdtasdt0(xr,sK10_skl))|~aNaturalNumber0(sK12_skl)|aNaturalNumber0(sdtasdt0(xp,xm))),
% 0.21/1.09 inference(paramodulation,[status(thm)],[f2650,f61])).
% 0.21/1.09 fof(f2663,definition,(
% 0.21/1.09 sQ340_spl <=> (aNaturalNumber0(sK12_skl))),
% 0.21/1.09 introduced(definition,[new_symbols(definition,[sQ340_spl])],[split_symbol_definition])).
% 0.21/1.09 fof(f2665,plain,(
% 0.21/1.09 ~aNaturalNumber0(sK12_skl)|sQ340_spl),
% 0.21/1.09 inference(component_clause,[status(thm)],[f2663])).
% 0.21/1.09 fof(f2694,definition,(
% 0.21/1.09 sQ348_spl <=> (sdtlseqdt0(sdtasdt0(xr,sK10_skl),sdtasdt0(xp,xm)))),
% 0.21/1.09 introduced(definition,[new_symbols(definition,[sQ348_spl])],[split_symbol_definition])).
% 0.21/1.09 fof(f2701,plain,(
% 0.21/1.09 ~sQ277_spl|sQ348_spl|~sQ340_spl),
% 0.21/1.09 inference(split_clause,[status(thm)],[f2659,f2271,f2694,f2663])).
% 0.21/1.09 fof(f2707,definition,(
% 0.21/1.09 sQ351_spl <=> (aNaturalNumber0(sdtasdt0(xp,xm)))),
% 0.21/1.09 introduced(definition,[new_symbols(definition,[sQ351_spl])],[split_symbol_definition])).
% 0.21/1.09 fof(f2710,plain,(
% 0.21/1.09 ~sQ277_spl|~sQ340_spl|sQ351_spl),
% 0.21/1.09 inference(split_clause,[status(thm)],[f2662,f2271,f2663,f2707])).
% 0.21/1.09 fof(f2711,plain,(
% 0.21/1.09 $false|sQ340_spl),
% 0.21/1.09 inference(forward_subsumption_resolution,[status(thm)],[f2665,f242])).
% 0.21/1.09 fof(f2712,plain,(
% 0.21/1.09 sQ340_spl),
% 0.21/1.09 inference(contradiction_clause,[status(thm)],[f2711])).
% 0.21/1.09 fof(f2726,definition,(
% 0.21/1.09 sQ352_spl <=> (sdtasdt0(xr,sK10_skl)=sdtasdt0(xp,xm))),
% 0.21/1.09 introduced(definition,[new_symbols(definition,[sQ352_spl])],[split_symbol_definition])).
% 0.21/1.09 fof(f2727,plain,(
% 0.21/1.09 sdtasdt0(xr,sK10_skl)=sdtasdt0(xp,xm)|~sQ352_spl),
% 0.21/1.09 inference(component_clause,[status(thm)],[f2726])).
% 0.21/1.09 fof(f2773,plain,(
% 0.21/1.09 $false|~sQ352_spl),
% 0.21/1.09 inference(forward_subsumption_resolution,[status(thm)],[f2727,f2547])).
% 0.21/1.09 fof(f2774,plain,(
% 0.21/1.09 ~sQ352_spl),
% 0.21/1.09 inference(contradiction_clause,[status(thm)],[f2773])).
% 0.21/1.09 fof(f2889,definition,(
% 0.21/1.10 sQ378_spl <=> (aNaturalNumber0(sK13_skl))),
% 0.21/1.10 introduced(definition,[new_symbols(definition,[sQ378_spl])],[split_symbol_definition])).
% 0.21/1.10 fof(f2891,plain,(
% 0.21/1.10 ~aNaturalNumber0(sK13_skl)|sQ378_spl),
% 0.21/1.10 inference(component_clause,[status(thm)],[f2889])).
% 0.21/1.10 fof(f2934,plain,(
% 0.21/1.10 $false|sQ378_spl),
% 0.21/1.10 inference(forward_subsumption_resolution,[status(thm)],[f2891,f246])).
% 0.21/1.10 fof(f2935,plain,(
% 0.21/1.10 sQ378_spl),
% 0.21/1.10 inference(contradiction_clause,[status(thm)],[f2934])).
% 0.21/1.10 fof(f2948,definition,(
% 0.21/1.10 sQ389_spl <=> (sdtasdt0(xp,xm)=sdtasdt0(xp,xk))),
% 0.21/1.10 introduced(definition,[new_symbols(definition,[sQ389_spl])],[split_symbol_definition])).
% 0.21/1.10 fof(f2949,plain,(
% 0.21/1.10 sdtasdt0(xp,xm)=sdtasdt0(xp,xk)|~sQ389_spl),
% 0.21/1.10 inference(component_clause,[status(thm)],[f2948])).
% 0.21/1.10 fof(f2995,plain,(
% 0.21/1.10 $false|~sQ389_spl),
% 0.21/1.10 inference(forward_subsumption_resolution,[status(thm)],[f2949,f245])).
% 0.21/1.10 fof(f2996,plain,(
% 0.21/1.10 ~sQ389_spl),
% 0.21/1.10 inference(contradiction_clause,[status(thm)],[f2995])).
% 0.21/1.10 fof(f3088,plain,(
% 0.21/1.10 $false|~sQ195_spl),
% 0.21/1.10 inference(forward_subsumption_resolution,[status(thm)],[f1751,f226])).
% 0.21/1.10 fof(f3089,plain,(
% 0.21/1.10 ~sQ195_spl),
% 0.21/1.10 inference(contradiction_clause,[status(thm)],[f3088])).
% 0.21/1.10 fof(f3091,plain,(
% 0.21/1.10 $false|~sQ18_spl),
% 0.21/1.10 inference(forward_subsumption_resolution,[status(thm)],[f568,f554])).
% 0.21/1.10 fof(f3092,plain,(
% 0.21/1.10 ~sQ18_spl),
% 0.21/1.10 inference(contradiction_clause,[status(thm)],[f3091])).
% 0.21/1.10 fof(f3093,plain,(
% 0.21/1.10 $false|~sQ16_spl),
% 0.21/1.10 inference(forward_subsumption_resolution,[status(thm)],[f561,f555])).
% 0.21/1.10 fof(f3094,plain,(
% 0.21/1.10 ~sQ16_spl),
% 0.21/1.10 inference(contradiction_clause,[status(thm)],[f3093])).
% 0.21/1.10 fof(f3105,definition,(
% 0.21/1.10 sQ419_spl <=> (doDivides0(xr,sdtasdt0(xr,sK8_skl)))),
% 0.21/1.10 introduced(definition,[new_symbols(definition,[sQ419_spl])],[split_symbol_definition])).
% 0.21/1.10 fof(f3107,plain,(
% 0.21/1.10 ~doDivides0(xr,sdtasdt0(xr,sK8_skl))|sQ419_spl),
% 0.21/1.10 inference(component_clause,[status(thm)],[f3105])).
% 0.21/1.10 fof(f3117,plain,(
% 0.21/1.10 ~doDivides0(xr,xk)|sQ419_spl),
% 0.21/1.10 inference(forward_demodulation,[status(thm)],[f223,f3107])).
% 0.21/1.10 fof(f3118,plain,(
% 0.21/1.10 $false|sQ419_spl),
% 0.21/1.10 inference(forward_subsumption_resolution,[status(thm)],[f3117,f224])).
% 0.21/1.10 fof(f3119,plain,(
% 0.21/1.10 sQ419_spl),
% 0.21/1.10 inference(contradiction_clause,[status(thm)],[f3118])).
% 0.21/1.10 fof(f3164,plain,(
% 0.21/1.10 $false|sQ93_spl),
% 0.21/1.10 inference(forward_subsumption_resolution,[status(thm)],[f1083,f193])).
% 0.21/1.10 fof(f3165,plain,(
% 0.21/1.10 sQ93_spl),
% 0.21/1.10 inference(contradiction_clause,[status(thm)],[f3164])).
% 0.21/1.10 fof(f3169,plain,(
% 0.21/1.10 sdtlseqdt0(sdtasdt0(xp,xm),sdtasdt0(xr,sK10_skl))),
% 0.21/1.10 inference(backward_demodulation,[status(thm)],[f2255,f248])).
% 0.21/1.10 fof(f3179,plain,(
% 0.21/1.10 ~aNaturalNumber0(xp)|~aNaturalNumber0(xk)|aNaturalNumber0(sdtasdt0(xr,sK10_skl))),
% 0.21/1.10 inference(paramodulation,[status(thm)],[f2255,f63])).
% 0.21/1.10 fof(f3204,plain,(
% 0.21/1.10 ~sQ70_spl|~sQ227_spl|sQ277_spl),
% 0.21/1.10 inference(split_clause,[status(thm)],[f3179,f926,f1926,f2271])).
% 0.21/1.10 fof(f3399,plain,(
% 0.21/1.10 ~aNaturalNumber0(sdtasdt0(xr,sK10_skl))|~aNaturalNumber0(sdtasdt0(xp,xm))|~sdtlseqdt0(sdtasdt0(xr,sK10_skl),sdtasdt0(xp,xm))|sdtasdt0(xr,sK10_skl)=sdtasdt0(xp,xm)),
% 0.21/1.10 inference(resolution,[status(thm)],[f3169,f110])).
% 0.21/1.10 fof(f3428,plain,(
% 0.21/1.10 ~sQ277_spl|~sQ351_spl|~sQ348_spl|sQ352_spl),
% 0.21/1.10 inference(split_clause,[status(thm)],[f3399,f2271,f2707,f2694,f2726])).
% 0.21/1.10 fof(f3445,plain,(
% 0.21/1.10 $false),
% 0.21/1.10 inference(sat_refutation,[status(thm)],[f934,f2485,f2487,f2701,f2710,f2712,f2774,f2935,f2996,f3089,f3092,f3094,f3119,f3165,f3204,f3428])).
% 0.21/1.10 % SZS output end CNFRefutation for theBenchmark.p
% 0.30/1.12 % Elapsed time: 0.614130 seconds
% 0.30/1.12 % CPU time: 4.323880 seconds
% 0.30/1.12 % Total memory used: 140.412 MB
% 0.30/1.12 % Net memory used: 137.074 MB
%------------------------------------------------------------------------------