%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM483+3 : 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:01 PM UTC 2026
% Result : Theorem 229.75s 29.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM483+3 : 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.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 02:38:37 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 229.75/29.47 % Refutation found
% 229.75/29.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 229.75/29.47 % SZS output start CNFRefutation for theBenchmark
% 229.75/29.47 fof(f12,axiom,(
% 229.75/29.47 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 229.75/29.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 229.75/29.47 fof(f29,axiom,(
% 229.75/29.47 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( ( W0 != W1& sdtlseqdt0(W0,W1) )=> iLess0(W0,W1) ) ) )),
% 229.75/29.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 229.75/29.47 fof(f32,axiom,(
% 229.75/29.47 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> ( ( doDivides0(W0,W1)& doDivides0(W1,W2) )=> doDivides0(W0,W2) ) ) )),
% 229.75/29.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 229.75/29.47 fof(f35,axiom,(
% 229.75/29.47 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( ( doDivides0(W0,W1)& W1 != sz00 )=> sdtlseqdt0(W0,W1) ) ) )),
% 229.75/29.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 229.75/29.47 fof(f38,hypothesis,(
% 229.75/29.47 aNaturalNumber0(xk) ),
% 229.75/29.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 229.75/29.47 fof(f39,hypothesis,(
% 229.75/29.47 (! [W0] :( ( aNaturalNumber0(W0)& W0 != sz00& W0 != sz10 )=> ( iLess0(W0,xk)=> (? [W1] :( aNaturalNumber0(W1)& (? [W2] :( aNaturalNumber0(W2)& W0 = sdtasdt0(W1,W2) ))& doDivides0(W1,W0)& W1 != sz00& W1 != sz10& (! [W2] :( ( aNaturalNumber0(W2)& ( (? [W3] :( aNaturalNumber0(W3)& W1 = sdtasdt0(W2,W3) ))| doDivides0(W2,W1) ) )=> ( W2 = sz10| W2 = W1 ) ))& isPrime0(W1) ) )) ) )),
% 229.75/29.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 229.75/29.47 fof(f40,hypothesis,(
% 229.75/29.47 ( xk != sz00& xk != sz10 ) ),
% 229.75/29.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 229.75/29.47 fof(f41,hypothesis,(
% 229.75/29.47 ~ ( (! [W0] :( ( aNaturalNumber0(W0)& (? [W1] :( aNaturalNumber0(W1)& xk = sdtasdt0(W0,W1) ))& doDivides0(W0,xk) )=> ( W0 = sz10| W0 = xk ) ))| isPrime0(xk) ) ),
% 229.75/29.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 229.75/29.47 fof(f42,conjecture,(
% 229.75/29.47 (? [W0] :( aNaturalNumber0(W0)& ( (? [W1] :( aNaturalNumber0(W1)& xk = sdtasdt0(W0,W1) ))| doDivides0(W0,xk) )& ( ( W0 != sz00& W0 != sz10& (! [W1] :( ( aNaturalNumber0(W1)& (? [W2] :( aNaturalNumber0(W2)& W0 = sdtasdt0(W1,W2) ))& doDivides0(W1,W0) )=> ( W1 = sz10| W1 = W0 ) ) ))| isPrime0(W0) ) ) )),
% 229.75/29.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 229.75/29.47 fof(f43,negated_conjecture,(
% 229.75/29.47 ~((? [W0] :( aNaturalNumber0(W0)& ( (? [W1] :( aNaturalNumber0(W1)& xk = sdtasdt0(W0,W1) ))| doDivides0(W0,xk) )& ( ( W0 != sz00& W0 != sz10& (! [W1] :( ( aNaturalNumber0(W1)& (? [W2] :( aNaturalNumber0(W2)& W0 = sdtasdt0(W1,W2) ))& doDivides0(W1,W0) )=> ( W1 = sz10| W1 = W0 ) ) ))| isPrime0(W0) ) ) ))),
% 229.75/29.47 inference(negated_conjecture,[status(cth)],[f42])).
% 229.75/29.47 fof(f68,plain,(
% 229.75/29.47 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 229.75/29.47 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 229.75/29.47 fof(f70,plain,(
% 229.75/29.47 ![X0]: (~aNaturalNumber0(X0)|sz00=sdtasdt0(sz00,X0))),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f68])).
% 229.75/29.47 fof(f123,plain,(
% 229.75/29.47 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((W0=W1|~sdtlseqdt0(W0,W1))|iLess0(W0,W1)))),
% 229.75/29.47 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 229.75/29.47 fof(f124,plain,(
% 229.75/29.47 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=X1|~sdtlseqdt0(X0,X1)|iLess0(X0,X1))),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f123])).
% 229.75/29.47 fof(f137,plain,(
% 229.75/29.47 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|((~doDivides0(W0,W1)|~doDivides0(W1,W2))|doDivides0(W0,W2)))),
% 229.75/29.47 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 229.75/29.47 fof(f138,plain,(
% 229.75/29.47 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X0,X1)|~doDivides0(X1,X2)|doDivides0(X0,X2))),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f137])).
% 229.75/29.47 fof(f143,plain,(
% 229.75/29.47 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((~doDivides0(W0,W1)|W1=sz00)|sdtlseqdt0(W0,W1)))),
% 229.75/29.47 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 229.75/29.47 fof(f144,plain,(
% 229.75/29.47 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~doDivides0(X0,X1)|X1=sz00|sdtlseqdt0(X0,X1))),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f143])).
% 229.75/29.47 fof(f157,plain,(
% 229.75/29.47 aNaturalNumber0(xk)),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f38])).
% 229.75/29.47 fof(f158,plain,(
% 229.75/29.47 ![W0]: (((~aNaturalNumber0(W0)|W0=sz00)|W0=sz10)|(~iLess0(W0,xk)|(?[W1]: ((((((aNaturalNumber0(W1)&(?[W2]: (aNaturalNumber0(W2)&W0=sdtasdt0(W1,W2))))&doDivides0(W1,W0))&~W1=sz00)&~W1=sz10)&(![W2]: ((~aNaturalNumber0(W2)|((![W3]: (~aNaturalNumber0(W3)|~W1=sdtasdt0(W2,W3)))&~doDivides0(W2,W1)))|(W2=sz10|W2=W1))))&isPrime0(W1)))))),
% 229.75/29.47 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 229.75/29.47 fof(f159,plain,(
% 229.75/29.47 ![W0]: (((~aNaturalNumber0(W0)|W0=sz00)|W0=sz10)|(~iLess0(W0,xk)|((((((aNaturalNumber0(sK3_skl(W0))&(aNaturalNumber0(sK4_skl(W0))&W0=sdtasdt0(sK3_skl(W0),sK4_skl(W0))))&doDivides0(sK3_skl(W0),W0))&~sK3_skl(W0)=sz00)&~sK3_skl(W0)=sz10)&(![W2]: ((~aNaturalNumber0(W2)|((![W3]: (~aNaturalNumber0(W3)|~sK3_skl(W0)=sdtasdt0(W2,W3)))&~doDivides0(W2,sK3_skl(W0))))|(W2=sz10|W2=sK3_skl(W0)))))&isPrime0(sK3_skl(W0)))))),
% 229.75/29.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl]),skolemize(W1,sK3_skl(W0)),skolemize(W2,sK4_skl(W0))],[f158])).
% 229.75/29.47 fof(f160,plain,(
% 229.75/29.47 ![X0]: (~aNaturalNumber0(X0)|X0=sz00|X0=sz10|~iLess0(X0,xk)|aNaturalNumber0(sK3_skl(X0)))),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f159])).
% 229.75/29.47 fof(f163,plain,(
% 229.75/29.47 ![X0]: (~aNaturalNumber0(X0)|X0=sz00|X0=sz10|~iLess0(X0,xk)|doDivides0(sK3_skl(X0),X0))),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f159])).
% 229.75/29.47 fof(f168,plain,(
% 229.75/29.47 ![X0]: (~aNaturalNumber0(X0)|X0=sz00|X0=sz10|~iLess0(X0,xk)|isPrime0(sK3_skl(X0)))),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f159])).
% 229.75/29.47 fof(f169,plain,(
% 229.75/29.47 ~xk=sz00),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f40])).
% 229.75/29.47 fof(f171,plain,(
% 229.75/29.47 ((?[W0]: (((aNaturalNumber0(W0)&(?[W1]: (aNaturalNumber0(W1)&xk=sdtasdt0(W0,W1))))&doDivides0(W0,xk))&(~W0=sz10&~W0=xk)))&~isPrime0(xk))),
% 229.75/29.47 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 229.75/29.47 fof(f172,plain,(
% 229.75/29.47 (((aNaturalNumber0(sK5_skl)&(aNaturalNumber0(sK6_skl)&xk=sdtasdt0(sK5_skl,sK6_skl)))&doDivides0(sK5_skl,xk))&(~sK5_skl=sz10&~sK5_skl=xk))&~isPrime0(xk)),
% 229.75/29.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl]),skolemize(W0,sK5_skl),skolemize(W1,sK6_skl)],[f171])).
% 229.75/29.47 fof(f173,plain,(
% 229.75/29.47 aNaturalNumber0(sK5_skl)),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f172])).
% 229.75/29.47 fof(f174,plain,(
% 229.75/29.47 aNaturalNumber0(sK6_skl)),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f172])).
% 229.75/29.47 fof(f175,plain,(
% 229.75/29.47 xk=sdtasdt0(sK5_skl,sK6_skl)),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f172])).
% 229.75/29.47 fof(f176,plain,(
% 229.75/29.47 doDivides0(sK5_skl,xk)),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f172])).
% 229.75/29.47 fof(f177,plain,(
% 229.75/29.47 ~sK5_skl=sz10),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f172])).
% 229.75/29.47 fof(f178,plain,(
% 229.75/29.47 ~sK5_skl=xk),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f172])).
% 229.75/29.47 fof(f180,plain,(
% 229.75/29.47 (![W0]: ((~aNaturalNumber0(W0)|((![W1]: (~aNaturalNumber0(W1)|~xk=sdtasdt0(W0,W1)))&~doDivides0(W0,xk)))|(((W0=sz00|W0=sz10)|(?[W1]: (((aNaturalNumber0(W1)&(?[W2]: (aNaturalNumber0(W2)&W0=sdtasdt0(W1,W2))))&doDivides0(W1,W0))&(~W1=sz10&~W1=W0))))&~isPrime0(W0))))),
% 229.75/29.47 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 229.75/29.47 fof(f181,definition,(
% 229.75/29.47 ![W0]: (sP0_prd(W0)<=>((![W1]: (~aNaturalNumber0(W1)|~xk=sdtasdt0(W0,W1)))&~doDivides0(W0,xk)))),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 229.75/29.47 fof(f182,plain,(
% 229.75/29.47 ![W0]: ((~aNaturalNumber0(W0)|sP0_prd(W0))|(((W0=sz00|W0=sz10)|(?[W1]: (((aNaturalNumber0(W1)&(?[W2]: (aNaturalNumber0(W2)&W0=sdtasdt0(W1,W2))))&doDivides0(W1,W0))&(~W1=sz10&~W1=W0))))&~isPrime0(W0)))),
% 229.75/29.47 inference(formula_renaming,[status(thm)],[f180,f181])).
% 229.75/29.47 fof(f183,plain,(
% 229.75/29.47 ![W0]: ((~aNaturalNumber0(W0)|sP0_prd(W0))|(((W0=sz00|W0=sz10)|(((aNaturalNumber0(sK7_skl(W0))&(aNaturalNumber0(sK8_skl(W0))&W0=sdtasdt0(sK7_skl(W0),sK8_skl(W0))))&doDivides0(sK7_skl(W0),W0))&(~sK7_skl(W0)=sz10&~sK7_skl(W0)=W0)))&~isPrime0(W0)))),
% 229.75/29.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(W1,sK7_skl(W0)),skolemize(W2,sK8_skl(W0))],[f182])).
% 229.75/29.47 fof(f190,plain,(
% 229.75/29.47 ![X0]: (~aNaturalNumber0(X0)|sP0_prd(X0)|~isPrime0(X0))),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f183])).
% 229.75/29.47 fof(f191,plain,(
% 229.75/29.47 ![W0]: ((~sP0_prd(W0)|((![W1]: (~aNaturalNumber0(W1)|~xk=sdtasdt0(W0,W1)))&~doDivides0(W0,xk)))&(sP0_prd(W0)|((?[W1]: (aNaturalNumber0(W1)&xk=sdtasdt0(W0,W1)))|doDivides0(W0,xk))))),
% 229.75/29.47 inference(NNF_transformation,[status(thm)],[f181])).
% 229.75/29.47 fof(f192,plain,(
% 229.75/29.47 (![W0]: (~sP0_prd(W0)|((![W1]: (~aNaturalNumber0(W1)|~xk=sdtasdt0(W0,W1)))&~doDivides0(W0,xk))))&(![W0]: (sP0_prd(W0)|((?[W1]: (aNaturalNumber0(W1)&xk=sdtasdt0(W0,W1)))|doDivides0(W0,xk))))),
% 229.75/29.47 inference(miniscoping,[status(thm)],[f191])).
% 229.75/29.47 fof(f193,plain,(
% 229.75/29.47 (![W0]: (~sP0_prd(W0)|((![W1]: (~aNaturalNumber0(W1)|~xk=sdtasdt0(W0,W1)))&~doDivides0(W0,xk))))&(![W0]: (sP0_prd(W0)|((aNaturalNumber0(sK9_skl(W0))&xk=sdtasdt0(W0,sK9_skl(W0)))|doDivides0(W0,xk))))),
% 229.75/29.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(W1,sK9_skl(W0))],[f192])).
% 229.75/29.47 fof(f195,plain,(
% 229.75/29.47 ![X0]: (~sP0_prd(X0)|~doDivides0(X0,xk))),
% 229.75/29.47 inference(cnf_transformation,[status(thm)],[f193])).
% 229.75/29.47 fof(f231,definition,(
% 229.75/29.47 sQ8_spl <=> (xk=sz00)),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f232,plain,(
% 229.75/29.47 xk=sz00|~sQ8_spl),
% 229.75/29.47 inference(component_clause,[status(thm)],[f231])).
% 229.75/29.47 fof(f245,plain,(
% 229.75/29.47 $false|~sQ8_spl),
% 229.75/29.47 inference(forward_subsumption_resolution,[status(thm)],[f232,f169])).
% 229.75/29.47 fof(f246,plain,(
% 229.75/29.47 ~sQ8_spl),
% 229.75/29.47 inference(contradiction_clause,[status(thm)],[f245])).
% 229.75/29.47 fof(f287,definition,(
% 229.75/29.47 sQ20_spl <=> (sK5_skl=sz00)),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f288,plain,(
% 229.75/29.47 sK5_skl=sz00|~sQ20_spl),
% 229.75/29.47 inference(component_clause,[status(thm)],[f287])).
% 229.75/29.47 fof(f290,definition,(
% 229.75/29.47 sQ21_spl <=> (sK5_skl=sz10)),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f291,plain,(
% 229.75/29.47 sK5_skl=sz10|~sQ21_spl),
% 229.75/29.47 inference(component_clause,[status(thm)],[f290])).
% 229.75/29.47 fof(f313,plain,(
% 229.75/29.47 $false|~sQ21_spl),
% 229.75/29.47 inference(forward_subsumption_resolution,[status(thm)],[f291,f177])).
% 229.75/29.47 fof(f314,plain,(
% 229.75/29.47 ~sQ21_spl),
% 229.75/29.47 inference(contradiction_clause,[status(thm)],[f313])).
% 229.75/29.47 fof(f811,definition,(
% 229.75/29.47 sQ68_spl <=> (xk=sK5_skl)),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f812,plain,(
% 229.75/29.47 xk=sK5_skl|~sQ68_spl),
% 229.75/29.47 inference(component_clause,[status(thm)],[f811])).
% 229.75/29.47 fof(f818,plain,(
% 229.75/29.47 $false|~sQ68_spl),
% 229.75/29.47 inference(forward_subsumption_resolution,[status(thm)],[f812,f178])).
% 229.75/29.47 fof(f819,plain,(
% 229.75/29.47 ~sQ68_spl),
% 229.75/29.47 inference(contradiction_clause,[status(thm)],[f818])).
% 229.75/29.47 fof(f955,definition,(
% 229.75/29.47 sQ77_spl <=> (aNaturalNumber0(sK5_skl))),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f957,plain,(
% 229.75/29.47 ~aNaturalNumber0(sK5_skl)|sQ77_spl),
% 229.75/29.47 inference(component_clause,[status(thm)],[f955])).
% 229.75/29.47 fof(f958,definition,(
% 229.75/29.47 sQ78_spl <=> (aNaturalNumber0(xk))),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f960,plain,(
% 229.75/29.47 ~aNaturalNumber0(xk)|sQ78_spl),
% 229.75/29.47 inference(component_clause,[status(thm)],[f958])).
% 229.75/29.47 fof(f975,plain,(
% 229.75/29.47 $false|sQ77_spl),
% 229.75/29.47 inference(forward_subsumption_resolution,[status(thm)],[f957,f173])).
% 229.75/29.47 fof(f976,plain,(
% 229.75/29.47 sQ77_spl),
% 229.75/29.47 inference(contradiction_clause,[status(thm)],[f975])).
% 229.75/29.47 fof(f977,plain,(
% 229.75/29.47 $false|sQ78_spl),
% 229.75/29.47 inference(forward_subsumption_resolution,[status(thm)],[f960,f157])).
% 229.75/29.47 fof(f978,plain,(
% 229.75/29.47 sQ78_spl),
% 229.75/29.47 inference(contradiction_clause,[status(thm)],[f977])).
% 229.75/29.47 fof(f1084,plain,(
% 229.75/29.47 ![X0]: (~aNaturalNumber0(X0)|~aNaturalNumber0(sK5_skl)|~aNaturalNumber0(xk)|~doDivides0(X0,sK5_skl)|doDivides0(X0,xk))),
% 229.75/29.47 inference(resolution,[status(thm)],[f138,f176])).
% 229.75/29.47 fof(f1089,definition,(
% 229.75/29.47 ![X0]: (sQ97_spl <=> (~aNaturalNumber0(X0)|~doDivides0(X0,sK5_skl)|doDivides0(X0,xk)))),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f1090,plain,(
% 229.75/29.47 ![X0]: (~aNaturalNumber0(X0)|~doDivides0(X0,sK5_skl)|doDivides0(X0,xk)|~sQ97_spl)),
% 229.75/29.47 inference(component_clause,[status(thm)],[f1089])).
% 229.75/29.47 fof(f1092,plain,(
% 229.75/29.47 sQ97_spl|~sQ77_spl|~sQ78_spl),
% 229.75/29.47 inference(split_clause,[status(thm)],[f1084,f1089,f955,f958])).
% 229.75/29.47 fof(f1266,definition,(
% 229.75/29.47 sQ122_spl <=> (sdtlseqdt0(sK5_skl,xk))),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f1267,plain,(
% 229.75/29.47 sdtlseqdt0(sK5_skl,xk)|~sQ122_spl),
% 229.75/29.47 inference(component_clause,[status(thm)],[f1266])).
% 229.75/29.47 fof(f3217,plain,(
% 229.75/29.47 ~aNaturalNumber0(sK5_skl)|~aNaturalNumber0(xk)|sK5_skl=xk|iLess0(sK5_skl,xk)|~sQ122_spl),
% 229.75/29.47 inference(resolution,[status(thm)],[f1267,f124])).
% 229.75/29.47 fof(f3224,definition,(
% 229.75/29.47 sQ315_spl <=> (iLess0(sK5_skl,xk))),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f3225,plain,(
% 229.75/29.47 iLess0(sK5_skl,xk)|~sQ315_spl),
% 229.75/29.47 inference(component_clause,[status(thm)],[f3224])).
% 229.75/29.47 fof(f3227,plain,(
% 229.75/29.47 ~sQ77_spl|~sQ78_spl|sQ68_spl|sQ315_spl|~sQ122_spl),
% 229.75/29.47 inference(split_clause,[status(thm)],[f3217,f955,f958,f811,f3224,f1266])).
% 229.75/29.47 fof(f3259,plain,(
% 229.75/29.47 sz00=sdtasdt0(sz00,sK6_skl)),
% 229.75/29.47 inference(resolution,[status(thm)],[f70,f174])).
% 229.75/29.47 fof(f3389,plain,(
% 229.75/29.47 ~aNaturalNumber0(sK5_skl)|sK5_skl=sz00|sK5_skl=sz10|aNaturalNumber0(sK3_skl(sK5_skl))|~sQ315_spl),
% 229.75/29.47 inference(resolution,[status(thm)],[f3225,f160])).
% 229.75/29.47 fof(f3398,definition,(
% 229.75/29.47 sQ332_spl <=> (aNaturalNumber0(sK3_skl(sK5_skl)))),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f3401,plain,(
% 229.75/29.47 ~sQ77_spl|sQ20_spl|sQ21_spl|sQ332_spl|~sQ315_spl),
% 229.75/29.47 inference(split_clause,[status(thm)],[f3389,f955,f287,f290,f3398,f3224])).
% 229.75/29.47 fof(f3685,definition,(
% 229.75/29.47 sQ343_spl <=> (isPrime0(sK3_skl(sK5_skl)))),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ343_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f3686,plain,(
% 229.75/29.47 isPrime0(sK3_skl(sK5_skl))|~sQ343_spl),
% 229.75/29.47 inference(component_clause,[status(thm)],[f3685])).
% 229.75/29.47 fof(f3697,definition,(
% 229.75/29.47 sQ346_spl <=> (doDivides0(sK3_skl(sK5_skl),sK5_skl))),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f3698,plain,(
% 229.75/29.47 doDivides0(sK3_skl(sK5_skl),sK5_skl)|~sQ346_spl),
% 229.75/29.47 inference(component_clause,[status(thm)],[f3697])).
% 229.75/29.47 fof(f4041,plain,(
% 229.75/29.47 ~aNaturalNumber0(sK3_skl(sK5_skl))|sP0_prd(sK3_skl(sK5_skl))|~sQ343_spl),
% 229.75/29.47 inference(resolution,[status(thm)],[f3686,f190])).
% 229.75/29.47 fof(f4042,definition,(
% 229.75/29.47 sQ356_spl <=> (sP0_prd(sK3_skl(sK5_skl)))),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ356_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f4045,plain,(
% 229.75/29.47 ~sQ332_spl|sQ356_spl|~sQ343_spl),
% 229.75/29.47 inference(split_clause,[status(thm)],[f4041,f3398,f4042,f3685])).
% 229.75/29.47 fof(f9248,plain,(
% 229.75/29.47 sK5_skl=sdtasdt0(sz00,sK6_skl)|~sQ20_spl),
% 229.75/29.47 inference(forward_demodulation,[status(thm)],[f288,f3259])).
% 229.75/29.47 fof(f9249,plain,(
% 229.75/29.47 sK5_skl=sdtasdt0(sK5_skl,sK6_skl)|~sQ20_spl),
% 229.75/29.47 inference(forward_demodulation,[status(thm)],[f288,f9248])).
% 229.75/29.47 fof(f9747,plain,(
% 229.75/29.47 xk=sK5_skl|~sQ20_spl),
% 229.75/29.47 inference(forward_demodulation,[status(thm)],[f9249,f175])).
% 229.75/29.47 fof(f9748,plain,(
% 229.75/29.47 $false|~sQ20_spl),
% 229.75/29.47 inference(forward_subsumption_resolution,[status(thm)],[f9747,f178])).
% 229.75/29.47 fof(f9749,plain,(
% 229.75/29.47 ~sQ20_spl),
% 229.75/29.47 inference(contradiction_clause,[status(thm)],[f9748])).
% 229.75/29.47 fof(f10373,plain,(
% 229.75/29.47 ~aNaturalNumber0(sK5_skl)|~aNaturalNumber0(xk)|xk=sz00|sdtlseqdt0(sK5_skl,xk)),
% 229.75/29.47 inference(resolution,[status(thm)],[f144,f176])).
% 229.75/29.47 fof(f10381,plain,(
% 229.75/29.47 ~sQ77_spl|~sQ78_spl|sQ8_spl|sQ122_spl),
% 229.75/29.47 inference(split_clause,[status(thm)],[f10373,f955,f958,f231,f1266])).
% 229.75/29.47 fof(f11155,plain,(
% 229.75/29.47 ~aNaturalNumber0(sK5_skl)|sK5_skl=sz00|sK5_skl=sz10|doDivides0(sK3_skl(sK5_skl),sK5_skl)|~sQ315_spl),
% 229.75/29.47 inference(resolution,[status(thm)],[f3225,f163])).
% 229.75/29.47 fof(f11157,plain,(
% 229.75/29.47 ~aNaturalNumber0(sK5_skl)|sK5_skl=sz00|sK5_skl=sz10|isPrime0(sK3_skl(sK5_skl))|~sQ315_spl),
% 229.75/29.47 inference(resolution,[status(thm)],[f3225,f168])).
% 229.75/29.47 fof(f11165,plain,(
% 229.75/29.47 ~sQ77_spl|sQ20_spl|sQ21_spl|sQ346_spl|~sQ315_spl),
% 229.75/29.47 inference(split_clause,[status(thm)],[f11155,f955,f287,f290,f3697,f3224])).
% 229.75/29.47 fof(f11167,plain,(
% 229.75/29.47 ~sQ77_spl|sQ20_spl|sQ21_spl|sQ343_spl|~sQ315_spl),
% 229.75/29.47 inference(split_clause,[status(thm)],[f11157,f955,f287,f290,f3685,f3224])).
% 229.75/29.47 fof(f23137,definition,(
% 229.75/29.47 sQ1406_spl <=> (doDivides0(sK3_skl(sK5_skl),xk))),
% 229.75/29.47 introduced(definition,[new_symbols(definition,[sQ1406_spl])],[split_symbol_definition])).
% 229.75/29.47 fof(f23138,plain,(
% 229.75/29.47 doDivides0(sK3_skl(sK5_skl),xk)|~sQ1406_spl),
% 127.35/29.57 inference(component_clause,[status(thm)],[f23137])).
% 127.35/29.57 fof(f46150,plain,(
% 127.35/29.57 ~sP0_prd(sK3_skl(sK5_skl))|~sQ1406_spl),
% 127.35/29.57 inference(resolution,[status(thm)],[f23138,f195])).
% 127.35/29.57 fof(f46158,plain,(
% 127.35/29.57 ~sQ356_spl|~sQ1406_spl),
% 127.35/29.57 inference(split_clause,[status(thm)],[f46150,f4042,f23137])).
% 127.35/29.57 fof(f48444,plain,(
% 127.35/29.57 ~aNaturalNumber0(sK3_skl(sK5_skl))|doDivides0(sK3_skl(sK5_skl),xk)|~sQ97_spl|~sQ346_spl),
% 127.35/29.57 inference(resolution,[status(thm)],[f1090,f3698])).
% 127.35/29.57 fof(f48448,plain,(
% 127.35/29.57 ~sQ332_spl|sQ1406_spl|~sQ97_spl|~sQ346_spl),
% 127.35/29.57 inference(split_clause,[status(thm)],[f48444,f3398,f23137,f1089,f3697])).
% 127.35/29.57 fof(f48454,plain,(
% 127.35/29.57 $false),
% 127.35/29.57 inference(sat_refutation,[status(thm)],[f246,f314,f819,f976,f978,f1092,f3227,f3401,f4045,f9749,f10381,f11165,f11167,f46158,f48448])).
% 127.35/29.57 % SZS output end CNFRefutation for theBenchmark.p
% 179.67/29.64 % Elapsed time: 29.231587 seconds
% 179.67/29.64 % CPU time: 230.825523 seconds
% 179.67/29.64 % Total memory used: 812.546 MB
% 179.67/29.64 % Net memory used: 756.625 MB
%------------------------------------------------------------------------------