%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM529+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 : n013.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:08 PM UTC 2026
% Result : Theorem 12.56s 2.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM529+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.38 % Computer : n013.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Mon Sep 21 02:37:21 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.43 % Drodi V4.1.1
% 12.56/2.62 % Refutation found
% 12.56/2.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.56/2.62 % SZS output start CNFRefutation for theBenchmark
% 12.56/2.62 fof(f2,axiom,(
% 12.56/2.62 aNaturalNumber0(sz00) ),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f3,axiom,(
% 12.56/2.62 ( aNaturalNumber0(sz10)& sz10 != sz00 ) ),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f4,axiom,(
% 12.56/2.62 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtpldt0(W0,W1)) ) )),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f9,axiom,(
% 12.56/2.62 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f12,axiom,(
% 12.56/2.62 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f15,axiom,(
% 12.56/2.62 (! [W0] :( aNaturalNumber0(W0)=> ( W0 != sz00=> (! [W1,W2] :( ( aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> ( ( sdtasdt0(W0,W1) = sdtasdt0(W0,W2)| sdtasdt0(W1,W0) = sdtasdt0(W2,W0) )=> W1 = W2 ) ) )) ) )),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f29,axiom,(
% 12.56/2.62 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( ( W0 != W1& sdtlseqdt0(W0,W1) )=> iLess0(W0,W1) ) ) )),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f40,hypothesis,(
% 12.56/2.62 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp)& xn != sz00& xm != sz00& xp != sz00 ) ),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f41,hypothesis,(
% 12.56/2.62 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2)& W0 != sz00& W1 != sz00& W2 != sz00 )=> ( sdtasdt0(W2,sdtasdt0(W1,W1)) = sdtasdt0(W0,W0)=> ( iLess0(W0,xn)=> ~ ( ( W2 != sz10& (! [W3] :( ( aNaturalNumber0(W3)& (? [W4] :( aNaturalNumber0(W4)& W2 = sdtasdt0(W3,W4) ))& doDivides0(W3,W2) )=> ( W3 = sz10| W3 = W2 ) ) ))| isPrime0(W2) ) ) ) ) )),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f42,hypothesis,(
% 12.56/2.62 sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn) ),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f43,hypothesis,(
% 12.56/2.62 ( xp != sz10& (! [W0] :( ( aNaturalNumber0(W0)& ( (? [W1] :( aNaturalNumber0(W1)& xp = sdtasdt0(W0,W1) ))| doDivides0(W0,xp) ) )=> ( W0 = sz10| W0 = xp ) ))& isPrime0(xp) ) ),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f44,hypothesis,(
% 12.56/2.62 ( (? [W0] :( aNaturalNumber0(W0)& sdtasdt0(xn,xn) = sdtasdt0(xp,W0) ))& doDivides0(xp,sdtasdt0(xn,xn))& (? [W0] :( aNaturalNumber0(W0)& xn = sdtasdt0(xp,W0) ))& doDivides0(xp,xn) ) ),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f45,hypothesis,(
% 12.56/2.62 ( aNaturalNumber0(xq)& xn = sdtasdt0(xp,xq)& xq = sdtsldt0(xn,xp) ) ),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f46,hypothesis,(
% 12.56/2.62 sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(xq,xq)) ),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f47,hypothesis,(
% 12.56/2.62 ( xm != xn& (? [W0] :( aNaturalNumber0(W0)& sdtpldt0(xm,W0) = xn ))& sdtlseqdt0(xm,xn) ) ),
% 12.56/2.62 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.62 fof(f53,plain,(
% 12.56/2.62 aNaturalNumber0(sz00)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f2])).
% 12.56/2.62 fof(f55,plain,(
% 12.56/2.62 ~sz10=sz00),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f3])).
% 12.56/2.62 fof(f56,plain,(
% 12.56/2.62 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtpldt0(W0,W1)))),
% 12.56/2.62 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 12.56/2.62 fof(f57,plain,(
% 12.56/2.62 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtpldt0(X0,X1)))),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f56])).
% 12.56/2.62 fof(f67,plain,(
% 12.56/2.62 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 12.56/2.62 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 12.56/2.62 fof(f68,plain,(
% 12.56/2.62 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f67])).
% 12.56/2.62 fof(f74,plain,(
% 12.56/2.62 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 12.56/2.62 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 12.56/2.62 fof(f75,plain,(
% 12.56/2.62 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f74])).
% 12.56/2.62 fof(f83,plain,(
% 12.56/2.62 ![W0]: (~aNaturalNumber0(W0)|(W0=sz00|(![W1,W2]: ((~aNaturalNumber0(W1)|~aNaturalNumber0(W2))|((~sdtasdt0(W0,W1)=sdtasdt0(W0,W2)&~sdtasdt0(W1,W0)=sdtasdt0(W2,W0))|W1=W2)))))),
% 12.56/2.62 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 12.56/2.62 fof(f85,plain,(
% 12.56/2.62 ![X0,X1,X2]: (~aNaturalNumber0(X0)|X0=sz00|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtasdt0(X1,X0)=sdtasdt0(X2,X0)|X1=X2)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f83])).
% 12.56/2.62 fof(f129,plain,(
% 12.56/2.62 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((W0=W1|~sdtlseqdt0(W0,W1))|iLess0(W0,W1)))),
% 12.56/2.62 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 12.56/2.62 fof(f130,plain,(
% 12.56/2.62 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=X1|~sdtlseqdt0(X0,X1)|iLess0(X0,X1))),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f129])).
% 12.56/2.62 fof(f170,plain,(
% 12.56/2.62 aNaturalNumber0(xn)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f40])).
% 12.56/2.62 fof(f171,plain,(
% 12.56/2.62 aNaturalNumber0(xm)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f40])).
% 12.56/2.62 fof(f172,plain,(
% 12.56/2.62 aNaturalNumber0(xp)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f40])).
% 12.56/2.62 fof(f173,plain,(
% 12.56/2.62 ~xn=sz00),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f40])).
% 12.56/2.62 fof(f174,plain,(
% 12.56/2.62 ~xm=sz00),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f40])).
% 12.56/2.62 fof(f175,plain,(
% 12.56/2.62 ~xp=sz00),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f40])).
% 12.56/2.62 fof(f176,plain,(
% 12.56/2.62 ![W0,W1,W2]: ((((((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|W0=sz00)|W1=sz00)|W2=sz00)|(~sdtasdt0(W2,sdtasdt0(W1,W1))=sdtasdt0(W0,W0)|(~iLess0(W0,xn)|((W2=sz10|(?[W3]: (((aNaturalNumber0(W3)&(?[W4]: (aNaturalNumber0(W4)&W2=sdtasdt0(W3,W4))))&doDivides0(W3,W2))&(~W3=sz10&~W3=W2))))&~isPrime0(W2)))))),
% 12.56/2.62 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 12.56/2.62 fof(f177,plain,(
% 12.56/2.62 ![W0,W1,W2]: ((((((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|W0=sz00)|W1=sz00)|W2=sz00)|(~sdtasdt0(W2,sdtasdt0(W1,W1))=sdtasdt0(W0,W0)|(~iLess0(W0,xn)|((W2=sz10|(((aNaturalNumber0(sK4_skl(W2,W1,W0))&(aNaturalNumber0(sK5_skl(W2,W1,W0))&W2=sdtasdt0(sK4_skl(W2,W1,W0),sK5_skl(W2,W1,W0))))&doDivides0(sK4_skl(W2,W1,W0),W2))&(~sK4_skl(W2,W1,W0)=sz10&~sK4_skl(W2,W1,W0)=W2)))&~isPrime0(W2)))))),
% 12.56/2.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl]),skolemize(W3,sK4_skl(W2,W1,W0)),skolemize(W4,sK5_skl(W2,W1,W0))],[f176])).
% 12.56/2.62 fof(f184,plain,(
% 12.56/2.62 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|X0=sz00|X1=sz00|X2=sz00|~sdtasdt0(X2,sdtasdt0(X1,X1))=sdtasdt0(X0,X0)|~iLess0(X0,xn)|~isPrime0(X2))),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f177])).
% 12.56/2.62 fof(f185,plain,(
% 12.56/2.62 sdtasdt0(xp,sdtasdt0(xm,xm))=sdtasdt0(xn,xn)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f42])).
% 12.56/2.62 fof(f186,plain,(
% 12.56/2.62 (~xp=sz10&(![W0]: ((~aNaturalNumber0(W0)|((![W1]: (~aNaturalNumber0(W1)|~xp=sdtasdt0(W0,W1)))&~doDivides0(W0,xp)))|(W0=sz10|W0=xp))))&isPrime0(xp)),
% 12.56/2.62 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 12.56/2.62 fof(f188,plain,(
% 12.56/2.62 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~xp=sdtasdt0(X0,X1)|X0=sz10|X0=xp)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f186])).
% 12.56/2.62 fof(f190,plain,(
% 12.56/2.62 isPrime0(xp)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f186])).
% 12.56/2.62 fof(f191,plain,(
% 12.56/2.62 (((aNaturalNumber0(sK6_skl)&sdtasdt0(xn,xn)=sdtasdt0(xp,sK6_skl))&doDivides0(xp,sdtasdt0(xn,xn)))&(aNaturalNumber0(sK7_skl)&xn=sdtasdt0(xp,sK7_skl)))&doDivides0(xp,xn)),
% 12.56/2.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl]),skolemize(W0,sK6_skl),skolemize(W0,sK7_skl)],[f44])).
% 12.56/2.62 fof(f192,plain,(
% 12.56/2.62 aNaturalNumber0(sK6_skl)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f191])).
% 12.56/2.62 fof(f195,plain,(
% 12.56/2.62 aNaturalNumber0(sK7_skl)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f191])).
% 12.56/2.62 fof(f198,plain,(
% 12.56/2.62 aNaturalNumber0(xq)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f45])).
% 12.56/2.62 fof(f199,plain,(
% 12.56/2.62 xn=sdtasdt0(xp,xq)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f45])).
% 12.56/2.62 fof(f201,plain,(
% 12.56/2.62 sdtasdt0(xm,xm)=sdtasdt0(xp,sdtasdt0(xq,xq))),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f46])).
% 12.56/2.62 fof(f202,plain,(
% 12.56/2.62 (~xm=xn&(aNaturalNumber0(sK8_skl)&sdtpldt0(xm,sK8_skl)=xn))&sdtlseqdt0(xm,xn)),
% 12.56/2.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(W0,sK8_skl)],[f47])).
% 12.56/2.62 fof(f203,plain,(
% 12.56/2.62 ~xm=xn),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f202])).
% 12.56/2.62 fof(f204,plain,(
% 12.56/2.62 aNaturalNumber0(sK8_skl)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f202])).
% 12.56/2.62 fof(f206,plain,(
% 12.56/2.62 sdtlseqdt0(xm,xn)),
% 12.56/2.62 inference(cnf_transformation,[status(thm)],[f202])).
% 12.56/2.62 fof(f220,plain,(
% 12.56/2.62 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtpldt0(sz00,X0)))),
% 12.56/2.62 inference(resolution,[status(thm)],[f57,f53])).
% 12.56/2.62 fof(f236,plain,(
% 12.56/2.62 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz00)=sdtasdt0(sz00,X0))),
% 12.56/2.62 inference(resolution,[status(thm)],[f68,f53])).
% 12.56/2.62 fof(f248,plain,(
% 12.56/2.62 sdtasdt0(sz00,sz00)=sz00),
% 12.56/2.62 inference(resolution,[status(thm)],[f75,f53])).
% 12.56/2.62 fof(f301,definition,(
% 12.56/2.62 sQ4_spl <=> (xn=sz00)),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f302,plain,(
% 12.56/2.62 xn=sz00|~sQ4_spl),
% 12.56/2.62 inference(component_clause,[status(thm)],[f301])).
% 12.56/2.62 fof(f357,definition,(
% 12.56/2.62 sQ16_spl <=> (xm=sz00)),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f358,plain,(
% 12.56/2.62 xm=sz00|~sQ16_spl),
% 12.56/2.62 inference(component_clause,[status(thm)],[f357])).
% 12.56/2.62 fof(f413,definition,(
% 12.56/2.62 sQ28_spl <=> (xp=sz00)),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f414,plain,(
% 12.56/2.62 xp=sz00|~sQ28_spl),
% 12.56/2.62 inference(component_clause,[status(thm)],[f413])).
% 12.56/2.62 fof(f431,definition,(
% 12.56/2.62 sQ33_spl <=> (isPrime0(xp))),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f433,plain,(
% 12.56/2.62 ~isPrime0(xp)|sQ33_spl),
% 12.56/2.62 inference(component_clause,[status(thm)],[f431])).
% 12.56/2.62 fof(f490,definition,(
% 12.56/2.62 sQ40_spl <=> (aNaturalNumber0(xn))),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f492,plain,(
% 12.56/2.62 ~aNaturalNumber0(xn)|sQ40_spl),
% 12.56/2.62 inference(component_clause,[status(thm)],[f490])).
% 12.56/2.62 fof(f493,definition,(
% 12.56/2.62 sQ41_spl <=> (aNaturalNumber0(xm))),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f495,plain,(
% 12.56/2.62 ~aNaturalNumber0(xm)|sQ41_spl),
% 12.56/2.62 inference(component_clause,[status(thm)],[f493])).
% 12.56/2.62 fof(f496,definition,(
% 12.56/2.62 sQ42_spl <=> (aNaturalNumber0(xp))),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f498,plain,(
% 12.56/2.62 ~aNaturalNumber0(xp)|sQ42_spl),
% 12.56/2.62 inference(component_clause,[status(thm)],[f496])).
% 12.56/2.62 fof(f582,plain,(
% 12.56/2.62 $false|sQ42_spl),
% 12.56/2.62 inference(forward_subsumption_resolution,[status(thm)],[f498,f172])).
% 12.56/2.62 fof(f583,plain,(
% 12.56/2.62 sQ42_spl),
% 12.56/2.62 inference(contradiction_clause,[status(thm)],[f582])).
% 12.56/2.62 fof(f738,plain,(
% 12.56/2.62 $false|sQ41_spl),
% 12.56/2.62 inference(forward_subsumption_resolution,[status(thm)],[f495,f171])).
% 12.56/2.62 fof(f739,plain,(
% 12.56/2.62 sQ41_spl),
% 12.56/2.62 inference(contradiction_clause,[status(thm)],[f738])).
% 12.56/2.62 fof(f740,plain,(
% 12.56/2.62 $false|sQ40_spl),
% 12.56/2.62 inference(forward_subsumption_resolution,[status(thm)],[f492,f170])).
% 12.56/2.62 fof(f741,plain,(
% 12.56/2.62 sQ40_spl),
% 12.56/2.62 inference(contradiction_clause,[status(thm)],[f740])).
% 12.56/2.62 fof(f742,plain,(
% 12.56/2.62 $false|sQ33_spl),
% 12.56/2.62 inference(forward_subsumption_resolution,[status(thm)],[f433,f190])).
% 12.56/2.62 fof(f743,plain,(
% 12.56/2.62 sQ33_spl),
% 12.56/2.62 inference(contradiction_clause,[status(thm)],[f742])).
% 12.56/2.62 fof(f812,definition,(
% 12.56/2.62 sQ107_spl <=> (xp=xn)),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f895,definition,(
% 12.56/2.62 sQ121_spl <=> (xq=sz00)),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f896,plain,(
% 12.56/2.62 xq=sz00|~sQ121_spl),
% 12.56/2.62 inference(component_clause,[status(thm)],[f895])).
% 12.56/2.62 fof(f949,definition,(
% 12.56/2.62 sQ133_spl <=> (aNaturalNumber0(xq))),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f951,plain,(
% 12.56/2.62 ~aNaturalNumber0(xq)|sQ133_spl),
% 12.56/2.62 inference(component_clause,[status(thm)],[f949])).
% 12.56/2.62 fof(f976,plain,(
% 12.56/2.62 $false|sQ133_spl),
% 12.56/2.62 inference(forward_subsumption_resolution,[status(thm)],[f951,f198])).
% 12.56/2.62 fof(f977,plain,(
% 12.56/2.62 sQ133_spl),
% 12.56/2.62 inference(contradiction_clause,[status(thm)],[f976])).
% 12.56/2.62 fof(f979,plain,(
% 12.56/2.62 ~aNaturalNumber0(xm)|~aNaturalNumber0(xq)|~aNaturalNumber0(xp)|xm=sz00|xq=sz00|xp=sz00|~iLess0(xm,xn)|~isPrime0(xp)),
% 12.56/2.62 inference(resolution,[status(thm)],[f201,f184])).
% 12.56/2.62 fof(f1000,definition,(
% 12.56/2.62 sQ139_spl <=> (iLess0(xm,xn))),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f1003,plain,(
% 12.56/2.62 ~sQ41_spl|~sQ133_spl|~sQ42_spl|sQ16_spl|sQ121_spl|sQ28_spl|~sQ139_spl|~sQ33_spl),
% 12.56/2.62 inference(split_clause,[status(thm)],[f979,f493,f949,f496,f357,f895,f413,f1000,f431])).
% 12.56/2.62 fof(f1180,plain,(
% 12.56/2.62 ~aNaturalNumber0(xm)|~aNaturalNumber0(xn)|xm=xn|iLess0(xm,xn)),
% 12.56/2.62 inference(resolution,[status(thm)],[f206,f130])).
% 12.56/2.62 fof(f1189,definition,(
% 12.56/2.62 sQ178_spl <=> (xm=xn)),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f1190,plain,(
% 12.56/2.62 xm=xn|~sQ178_spl),
% 12.56/2.62 inference(component_clause,[status(thm)],[f1189])).
% 12.56/2.62 fof(f1192,plain,(
% 12.56/2.62 ~sQ41_spl|~sQ40_spl|sQ178_spl|sQ139_spl),
% 12.56/2.62 inference(split_clause,[status(thm)],[f1180,f493,f490,f1189,f1000])).
% 12.56/2.62 fof(f1225,plain,(
% 12.56/2.62 $false|~sQ178_spl),
% 12.56/2.62 inference(forward_subsumption_resolution,[status(thm)],[f1190,f203])).
% 12.56/2.62 fof(f1226,plain,(
% 12.56/2.62 ~sQ178_spl),
% 12.56/2.62 inference(contradiction_clause,[status(thm)],[f1225])).
% 12.56/2.62 fof(f1234,plain,(
% 12.56/2.62 aNaturalNumber0(sdtpldt0(sz00,sK8_skl))),
% 12.56/2.62 inference(resolution,[status(thm)],[f220,f204])).
% 12.56/2.62 fof(f1236,plain,(
% 12.56/2.62 aNaturalNumber0(sdtpldt0(sz00,sK7_skl))),
% 12.56/2.62 inference(resolution,[status(thm)],[f220,f195])).
% 12.56/2.62 fof(f1237,plain,(
% 12.56/2.62 aNaturalNumber0(sdtpldt0(sz00,sK6_skl))),
% 12.56/2.62 inference(resolution,[status(thm)],[f220,f192])).
% 12.56/2.62 fof(f1238,plain,(
% 12.56/2.62 aNaturalNumber0(sdtpldt0(sz00,xp))),
% 12.56/2.62 inference(resolution,[status(thm)],[f220,f172])).
% 12.56/2.62 fof(f1356,definition,(
% 12.56/2.62 sQ190_spl <=> (aNaturalNumber0(sz00))),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f1358,plain,(
% 12.56/2.62 ~aNaturalNumber0(sz00)|sQ190_spl),
% 12.56/2.62 inference(component_clause,[status(thm)],[f1356])).
% 12.56/2.62 fof(f1373,definition,(
% 12.56/2.62 sQ194_spl <=> (sz10=sz00)),
% 12.56/2.62 introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 12.56/2.62 fof(f1374,plain,(
% 12.56/2.62 sz10=sz00|~sQ194_spl),
% 12.56/2.62 inference(component_clause,[status(thm)],[f1373])).
% 12.56/2.62 fof(f1517,plain,(
% 12.56/2.62 sdtasdt0(xp,sz00)=sdtasdt0(sz00,xp)),
% 12.56/2.62 inference(resolution,[status(thm)],[f236,f172])).
% 12.56/2.62 fof(f2049,plain,(
% 12.56/2.62 $false|~sQ194_spl),
% 12.56/2.62 inference(forward_subsumption_resolution,[status(thm)],[f1374,f55])).
% 12.56/2.62 fof(f2050,plain,(
% 12.56/2.62 ~sQ194_spl),
% 12.56/2.62 inference(contradiction_clause,[status(thm)],[f2049])).
% 12.56/2.62 fof(f2320,plain,(
% 12.56/2.62 $false|~sQ4_spl),
% 12.56/2.62 inference(forward_subsumption_resolution,[status(thm)],[f302,f173])).
% 12.56/2.62 fof(f2321,plain,(
% 12.56/2.62 ~sQ4_spl),
% 12.56/2.62 inference(contradiction_clause,[status(thm)],[f2320])).
% 12.56/2.62 fof(f2427,plain,(
% 12.56/2.62 $false|~sQ16_spl),
% 12.56/2.62 inference(forward_subsumption_resolution,[status(thm)],[f358,f174])).
% 12.56/2.62 fof(f2428,plain,(
% 12.56/2.62 ~sQ16_spl),
% 12.56/2.62 inference(contradiction_clause,[status(thm)],[f2427])).
% 12.56/2.62 fof(f2525,plain,(
% 12.56/2.62 $false|~sQ28_spl),
% 12.56/2.62 inference(forward_subsumption_resolution,[status(thm)],[f414,f175])).
% 12.56/2.62 fof(f2526,plain,(
% 12.56/2.62 ~sQ28_spl),
% 12.56/2.62 inference(contradiction_clause,[status(thm)],[f2525])).
% 12.56/2.62 fof(f3169,plain,(
% 12.56/2.62 sdtasdt0(xm,xm)=sdtasdt0(xp,sdtasdt0(xq,sz00))|~sQ121_spl),
% 12.56/2.62 inference(backward_demodulation,[status(thm)],[f896,f201])).
% 12.56/2.62 fof(f3171,plain,(
% 12.56/2.62 xn=sdtasdt0(xp,sz00)|~sQ121_spl),
% 12.56/2.62 inference(backward_demodulation,[status(thm)],[f896,f199])).
% 12.56/2.62 fof(f3175,plain,(
% 12.56/2.62 sdtasdt0(xm,xm)=sdtasdt0(xp,sdtasdt0(sz00,sz00))|~sQ121_spl),
% 12.56/2.62 inference(forward_demodulation,[status(thm)],[f896,f3169])).
% 12.56/2.62 fof(f3176,plain,(
% 12.56/2.62 sdtasdt0(xm,xm)=sdtasdt0(xp,sz00)|~sQ121_spl),
% 12.56/2.62 inference(forward_demodulation,[status(thm)],[f248,f3175])).
% 12.56/2.62 fof(f3567,plain,(
% 12.56/2.62 sdtasdt0(xp,xn)=sdtasdt0(xn,xn)|~sQ121_spl),
% 12.56/2.62 inference(backward_demodulation,[status(thm)],[f3569,f185])).
% 12.56/2.62 fof(f3569,plain,(
% 12.56/2.62 sdtasdt0(xm,xm)=xn|~sQ121_spl),
% 12.56/2.62 inference(forward_demodulation,[status(thm)],[f3171,f3176])).
% 12.56/2.62 fof(f6163,plain,(
% 12.56/2.62 ~aNaturalNumber0(xn)|xn=sz00|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)|xp=xn|~sQ121_spl),
% 12.56/2.64 inference(resolution,[status(thm)],[f3567,f85])).
% 12.56/2.64 fof(f6172,plain,(
% 12.56/2.64 ~sQ40_spl|sQ4_spl|~sQ42_spl|sQ107_spl|~sQ121_spl),
% 12.56/2.64 inference(split_clause,[status(thm)],[f6163,f490,f301,f496,f812,f895])).
% 12.56/2.64 fof(f9260,definition,(
% 12.56/2.64 sQ1018_spl <=> (aNaturalNumber0(sdtpldt0(sz00,sK8_skl)))),
% 12.56/2.64 introduced(definition,[new_symbols(definition,[sQ1018_spl])],[split_symbol_definition])).
% 12.56/2.64 fof(f9262,plain,(
% 12.56/2.64 ~aNaturalNumber0(sdtpldt0(sz00,sK8_skl))|sQ1018_spl),
% 12.56/2.64 inference(component_clause,[status(thm)],[f9260])).
% 12.56/2.64 fof(f9397,definition,(
% 12.56/2.64 sQ1022_spl <=> (aNaturalNumber0(sdtpldt0(sz00,sK7_skl)))),
% 12.56/2.64 introduced(definition,[new_symbols(definition,[sQ1022_spl])],[split_symbol_definition])).
% 12.56/2.64 fof(f9399,plain,(
% 12.56/2.64 ~aNaturalNumber0(sdtpldt0(sz00,sK7_skl))|sQ1022_spl),
% 12.56/2.64 inference(component_clause,[status(thm)],[f9397])).
% 12.56/2.64 fof(f9426,definition,(
% 12.56/2.64 sQ1026_spl <=> (aNaturalNumber0(sdtpldt0(sz00,sK6_skl)))),
% 12.56/2.64 introduced(definition,[new_symbols(definition,[sQ1026_spl])],[split_symbol_definition])).
% 12.56/2.64 fof(f9428,plain,(
% 12.56/2.64 ~aNaturalNumber0(sdtpldt0(sz00,sK6_skl))|sQ1026_spl),
% 12.56/2.64 inference(component_clause,[status(thm)],[f9426])).
% 12.56/2.64 fof(f9455,definition,(
% 12.56/2.64 sQ1030_spl <=> (aNaturalNumber0(sdtpldt0(sz00,xp)))),
% 12.56/2.64 introduced(definition,[new_symbols(definition,[sQ1030_spl])],[split_symbol_definition])).
% 12.56/2.64 fof(f9457,plain,(
% 12.56/2.64 ~aNaturalNumber0(sdtpldt0(sz00,xp))|sQ1030_spl),
% 12.56/2.64 inference(component_clause,[status(thm)],[f9455])).
% 12.56/2.64 fof(f10466,plain,(
% 12.56/2.64 $false|sQ190_spl),
% 12.56/2.64 inference(forward_subsumption_resolution,[status(thm)],[f1358,f53])).
% 12.56/2.64 fof(f10467,plain,(
% 12.56/2.64 sQ190_spl),
% 12.56/2.64 inference(contradiction_clause,[status(thm)],[f10466])).
% 12.56/2.64 fof(f10468,plain,(
% 12.56/2.64 $false|sQ1018_spl),
% 12.56/2.64 inference(forward_subsumption_resolution,[status(thm)],[f9262,f1234])).
% 12.56/2.64 fof(f10469,plain,(
% 12.56/2.64 sQ1018_spl),
% 12.56/2.64 inference(contradiction_clause,[status(thm)],[f10468])).
% 12.56/2.64 fof(f10470,plain,(
% 12.56/2.64 $false|sQ1022_spl),
% 12.56/2.64 inference(forward_subsumption_resolution,[status(thm)],[f9399,f1236])).
% 12.56/2.64 fof(f10471,plain,(
% 12.56/2.64 sQ1022_spl),
% 12.56/2.64 inference(contradiction_clause,[status(thm)],[f10470])).
% 12.56/2.64 fof(f10472,plain,(
% 12.56/2.64 $false|sQ1026_spl),
% 12.56/2.64 inference(forward_subsumption_resolution,[status(thm)],[f9428,f1237])).
% 12.56/2.64 fof(f10473,plain,(
% 12.56/2.64 sQ1026_spl),
% 12.56/2.64 inference(contradiction_clause,[status(thm)],[f10472])).
% 12.56/2.64 fof(f10474,plain,(
% 12.56/2.64 $false|sQ1030_spl),
% 12.56/2.64 inference(forward_subsumption_resolution,[status(thm)],[f9457,f1238])).
% 12.56/2.64 fof(f10475,plain,(
% 12.56/2.64 sQ1030_spl),
% 12.56/2.64 inference(contradiction_clause,[status(thm)],[f10474])).
% 12.56/2.64 fof(f11802,plain,(
% 12.56/2.64 xn=sdtasdt0(sz00,xp)|~sQ121_spl),
% 12.56/2.64 inference(forward_demodulation,[status(thm)],[f3171,f1517])).
% 12.56/2.64 fof(f11803,plain,(
% 12.56/2.64 ~aNaturalNumber0(sz00)|~aNaturalNumber0(xp)|~xp=xn|sz00=sz10|sz00=xp|~sQ121_spl),
% 12.56/2.64 inference(paramodulation,[status(thm)],[f11802,f188])).
% 12.56/2.64 fof(f11810,plain,(
% 12.56/2.64 ~sQ190_spl|~sQ42_spl|~sQ107_spl|sQ194_spl|sQ28_spl|~sQ121_spl),
% 12.56/2.64 inference(split_clause,[status(thm)],[f11803,f1356,f496,f812,f1373,f413,f895])).
% 12.56/2.64 fof(f11823,plain,(
% 12.56/2.64 $false),
% 12.56/2.64 inference(sat_refutation,[status(thm)],[f583,f739,f741,f743,f977,f1003,f1192,f1226,f2050,f2321,f2428,f2526,f6172,f10467,f10469,f10471,f10473,f10475,f11810])).
% 12.56/2.64 % SZS output end CNFRefutation for theBenchmark.p
% 13.45/2.67 % Elapsed time: 2.257418 seconds
% 13.45/2.67 % CPU time: 17.358446 seconds
% 13.45/2.67 % Total memory used: 194.173 MB
% 13.45/2.67 % Net memory used: 186.075 MB
%------------------------------------------------------------------------------