%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM529+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 : n020.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:07 PM UTC 2026
% Result : Theorem 10.38s 1.82s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM529+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.08/0.35 % Computer : n020.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 02:38:48 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 10.38/1.82 % Refutation found
% 10.38/1.82 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.38/1.82 % SZS output start CNFRefutation for theBenchmark
% 10.38/1.82 fof(f12,axiom,(
% 10.38/1.82 (! [W0] :( aNaturalNumber0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 10.38/1.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.38/1.82 fof(f29,axiom,(
% 10.38/1.82 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( ( W0 != W1& sdtlseqdt0(W0,W1) )=> iLess0(W0,W1) ) ) )),
% 10.38/1.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.38/1.82 fof(f31,definition,(
% 10.38/1.82 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( ( W0 != sz00& doDivides0(W0,W1) )=> (! [W2] :( W2 = sdtsldt0(W1,W0)<=> ( aNaturalNumber0(W2)& W1 = sdtasdt0(W0,W2) ) ) )) ) )),
% 10.38/1.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.38/1.82 fof(f37,definition,(
% 10.38/1.82 (! [W0] :( aNaturalNumber0(W0)=> ( isPrime0(W0)<=> ( W0 != sz00& W0 != sz10& (! [W1] :( ( aNaturalNumber0(W1)& doDivides0(W1,W0) )=> ( W1 = sz10| W1 = W0 ) ) )) ) ) )),
% 10.38/1.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.38/1.82 fof(f40,hypothesis,(
% 10.38/1.82 ( aNaturalNumber0(xn)& aNaturalNumber0(xm)& aNaturalNumber0(xp)& xn != sz00& xm != sz00& xp != sz00 ) ),
% 10.38/1.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.38/1.82 fof(f41,hypothesis,(
% 10.38/1.82 (! [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)=> ~ isPrime0(W2) ) ) ) )),
% 10.38/1.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.38/1.82 fof(f43,hypothesis,(
% 10.38/1.82 isPrime0(xp) ),
% 10.38/1.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.38/1.82 fof(f44,hypothesis,(
% 10.38/1.82 ( doDivides0(xp,sdtasdt0(xn,xn))& doDivides0(xp,xn) ) ),
% 10.38/1.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.38/1.82 fof(f45,hypothesis,(
% 10.38/1.82 xq = sdtsldt0(xn,xp) ),
% 10.38/1.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.38/1.82 fof(f46,hypothesis,(
% 10.38/1.82 sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(xq,xq)) ),
% 10.38/1.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.38/1.82 fof(f47,hypothesis,(
% 10.38/1.82 ( xm != xn& sdtlseqdt0(xm,xn) ) ),
% 10.38/1.82 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.38/1.82 fof(f74,plain,(
% 10.38/1.82 ![W0]: (~aNaturalNumber0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 10.38/1.82 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 10.38/1.82 fof(f75,plain,(
% 10.38/1.82 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f74])).
% 10.38/1.82 fof(f129,plain,(
% 10.38/1.82 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((W0=W1|~sdtlseqdt0(W0,W1))|iLess0(W0,W1)))),
% 10.38/1.82 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 10.38/1.82 fof(f130,plain,(
% 10.38/1.82 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=X1|~sdtlseqdt0(X0,X1)|iLess0(X0,X1))),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f129])).
% 10.38/1.82 fof(f137,plain,(
% 10.38/1.82 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((W0=sz00|~doDivides0(W0,W1))|(![W2]: (W2=sdtsldt0(W1,W0)<=>(aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2))))))),
% 10.38/1.82 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 10.38/1.82 fof(f138,plain,(
% 10.38/1.82 ![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)))))))),
% 10.38/1.82 inference(NNF_transformation,[status(thm)],[f137])).
% 10.38/1.82 fof(f139,plain,(
% 10.38/1.82 ![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)))))))),
% 10.38/1.82 inference(miniscoping,[status(thm)],[f138])).
% 10.38/1.82 fof(f140,plain,(
% 10.38/1.82 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=sz00|~doDivides0(X0,X1)|~X2=sdtsldt0(X1,X0)|aNaturalNumber0(X2))),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f139])).
% 10.38/1.82 fof(f141,plain,(
% 10.38/1.82 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=sz00|~doDivides0(X0,X1)|~X2=sdtsldt0(X1,X0)|X1=sdtasdt0(X0,X2))),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f139])).
% 10.38/1.82 fof(f153,plain,(
% 10.38/1.82 ![W0]: (~aNaturalNumber0(W0)|(isPrime0(W0)<=>((~W0=sz00&~W0=sz10)&(![W1]: ((~aNaturalNumber0(W1)|~doDivides0(W1,W0))|(W1=sz10|W1=W0))))))),
% 10.38/1.82 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 10.38/1.82 fof(f154,plain,(
% 10.38/1.82 ![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)))))))),
% 10.38/1.82 inference(NNF_transformation,[status(thm)],[f153])).
% 10.38/1.82 fof(f155,plain,(
% 10.38/1.82 ![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))))))),
% 10.38/1.82 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W1,sK2_skl(W0))],[f154])).
% 10.38/1.82 fof(f156,plain,(
% 10.38/1.82 ![X0]: (~aNaturalNumber0(X0)|~isPrime0(X0)|~X0=sz00)),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f155])).
% 10.38/1.82 fof(f170,plain,(
% 10.38/1.82 aNaturalNumber0(xn)),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f40])).
% 10.38/1.82 fof(f171,plain,(
% 10.38/1.82 aNaturalNumber0(xm)),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f40])).
% 10.38/1.82 fof(f172,plain,(
% 10.38/1.82 aNaturalNumber0(xp)),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f40])).
% 10.38/1.82 fof(f173,plain,(
% 10.38/1.82 ~xn=sz00),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f40])).
% 10.38/1.82 fof(f174,plain,(
% 10.38/1.82 ~xm=sz00),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f40])).
% 10.38/1.82 fof(f176,plain,(
% 10.38/1.82 ![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)|~isPrime0(W2))))),
% 10.38/1.82 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 10.38/1.82 fof(f177,plain,(
% 10.38/1.82 ![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))),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f176])).
% 10.38/1.82 fof(f179,plain,(
% 10.38/1.82 isPrime0(xp)),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f43])).
% 10.38/1.82 fof(f181,plain,(
% 10.38/1.82 doDivides0(xp,xn)),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f44])).
% 10.38/1.82 fof(f182,plain,(
% 10.38/1.82 xq=sdtsldt0(xn,xp)),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f45])).
% 10.38/1.82 fof(f183,plain,(
% 10.38/1.82 sdtasdt0(xm,xm)=sdtasdt0(xp,sdtasdt0(xq,xq))),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f46])).
% 10.38/1.82 fof(f184,plain,(
% 10.38/1.82 ~xm=xn),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f47])).
% 10.38/1.82 fof(f185,plain,(
% 10.38/1.82 sdtlseqdt0(xm,xn)),
% 10.38/1.82 inference(cnf_transformation,[status(thm)],[f47])).
% 10.38/1.82 fof(f264,plain,(
% 10.38/1.82 sdtasdt0(xp,sz00)=sz00),
% 10.38/1.82 inference(resolution,[status(thm)],[f75,f172])).
% 10.38/1.82 fof(f269,plain,(
% 10.38/1.82 ~aNaturalNumber0(xp)|~xp=sz00),
% 10.38/1.82 inference(resolution,[status(thm)],[f156,f179])).
% 10.38/1.82 fof(f270,definition,(
% 10.38/1.82 sQ0_spl <=> (aNaturalNumber0(xp))),
% 10.38/1.82 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 10.38/1.82 fof(f272,plain,(
% 10.38/1.82 ~aNaturalNumber0(xp)|sQ0_spl),
% 10.38/1.82 inference(component_clause,[status(thm)],[f270])).
% 10.38/1.82 fof(f273,definition,(
% 10.38/1.82 sQ1_spl <=> (xp=sz00)),
% 10.38/1.82 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 10.38/1.82 fof(f276,plain,(
% 10.38/1.82 ~sQ0_spl|~sQ1_spl),
% 10.38/1.82 inference(split_clause,[status(thm)],[f269,f270,f273])).
% 10.38/1.82 fof(f277,plain,(
% 10.38/1.82 $false|sQ0_spl),
% 10.38/1.82 inference(forward_subsumption_resolution,[status(thm)],[f272,f172])).
% 10.38/1.82 fof(f278,plain,(
% 10.38/1.82 sQ0_spl),
% 10.38/1.82 inference(contradiction_clause,[status(thm)],[f277])).
% 10.38/1.82 fof(f746,definition,(
% 10.38/1.82 sQ6_spl <=> (aNaturalNumber0(xn))),
% 10.38/1.82 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 10.38/1.82 fof(f748,plain,(
% 10.38/1.82 ~aNaturalNumber0(xn)|sQ6_spl),
% 10.38/1.82 inference(component_clause,[status(thm)],[f746])).
% 10.38/1.82 fof(f753,definition,(
% 10.38/1.82 sQ8_spl <=> (aNaturalNumber0(xm))),
% 10.38/1.82 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 10.38/1.82 fof(f755,plain,(
% 10.38/1.82 ~aNaturalNumber0(xm)|sQ8_spl),
% 10.38/1.82 inference(component_clause,[status(thm)],[f753])).
% 10.38/1.82 fof(f804,plain,(
% 10.38/1.82 $false|sQ6_spl),
% 10.38/1.82 inference(forward_subsumption_resolution,[status(thm)],[f748,f170])).
% 10.38/1.82 fof(f805,plain,(
% 10.38/1.82 sQ6_spl),
% 10.38/1.82 inference(contradiction_clause,[status(thm)],[f804])).
% 10.38/1.82 fof(f806,plain,(
% 10.38/1.82 $false|sQ8_spl),
% 10.38/1.82 inference(forward_subsumption_resolution,[status(thm)],[f755,f171])).
% 10.38/1.82 fof(f807,plain,(
% 10.38/1.82 sQ8_spl),
% 10.38/1.82 inference(contradiction_clause,[status(thm)],[f806])).
% 10.38/1.82 fof(f963,definition,(
% 10.38/1.82 sQ42_spl <=> (xm=sz00)),
% 10.38/1.82 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 10.38/1.82 fof(f964,plain,(
% 10.38/1.82 xm=sz00|~sQ42_spl),
% 10.38/1.82 inference(component_clause,[status(thm)],[f963])).
% 10.38/1.82 fof(f1006,plain,(
% 10.38/1.82 $false|~sQ42_spl),
% 10.38/1.82 inference(forward_subsumption_resolution,[status(thm)],[f964,f174])).
% 10.38/1.82 fof(f1007,plain,(
% 10.38/1.82 ~sQ42_spl),
% 10.38/1.82 inference(contradiction_clause,[status(thm)],[f1006])).
% 10.38/1.82 fof(f3527,definition,(
% 10.38/1.82 sQ289_spl <=> (xn=xm)),
% 10.38/1.82 introduced(definition,[new_symbols(definition,[sQ289_spl])],[split_symbol_definition])).
% 10.38/1.82 fof(f3528,plain,(
% 10.38/1.82 xn=xm|~sQ289_spl),
% 10.38/1.82 inference(component_clause,[status(thm)],[f3527])).
% 10.38/1.82 fof(f3716,plain,(
% 10.38/1.82 $false|~sQ289_spl),
% 10.38/1.82 inference(forward_subsumption_resolution,[status(thm)],[f3528,f184])).
% 10.38/1.82 fof(f3717,plain,(
% 10.38/1.82 ~sQ289_spl),
% 10.38/1.82 inference(contradiction_clause,[status(thm)],[f3716])).
% 10.38/1.82 fof(f5814,plain,(
% 10.38/1.82 ~aNaturalNumber0(xm)|~aNaturalNumber0(xn)|xm=xn|iLess0(xm,xn)),
% 10.38/1.82 inference(resolution,[status(thm)],[f130,f185])).
% 10.38/1.82 fof(f5856,definition,(
% 10.38/1.82 sQ610_spl <=> (iLess0(xm,xn))),
% 10.38/1.82 introduced(definition,[new_symbols(definition,[sQ610_spl])],[split_symbol_definition])).
% 10.38/1.82 fof(f5859,plain,(
% 10.38/1.82 ~sQ8_spl|~sQ6_spl|sQ289_spl|sQ610_spl),
% 10.38/1.82 inference(split_clause,[status(thm)],[f5814,f753,f746,f3527,f5856])).
% 10.38/1.82 fof(f7011,definition,(
% 10.38/1.82 sQ713_spl <=> (isPrime0(xp))),
% 10.38/1.82 introduced(definition,[new_symbols(definition,[sQ713_spl])],[split_symbol_definition])).
% 10.38/1.82 fof(f7013,plain,(
% 10.38/1.82 ~isPrime0(xp)|sQ713_spl),
% 10.38/1.82 inference(component_clause,[status(thm)],[f7011])).
% 10.38/1.82 fof(f8049,plain,(
% 10.38/1.82 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|X0=sz00|X1=sz00|~sdtasdt0(X2,sdtasdt0(X1,X1))=sdtasdt0(X0,X0)|~iLess0(X0,xn)|~isPrime0(X2))),
% 10.38/1.82 inference(forward_subsumption_resolution,[status(thm)],[f177,f156])).
% 10.38/1.82 fof(f8110,definition,(
% 10.38/1.82 sQ824_spl <=> (aNaturalNumber0(xq))),
% 10.38/1.82 introduced(definition,[new_symbols(definition,[sQ824_spl])],[split_symbol_definition])).
% 10.38/1.82 fof(f8113,definition,(
% 10.38/1.82 sQ825_spl <=> (xq=sz00)),
% 10.38/1.82 introduced(definition,[new_symbols(definition,[sQ825_spl])],[split_symbol_definition])).
% 10.38/1.82 fof(f8114,plain,(
% 10.38/1.82 xq=sz00|~sQ825_spl),
% 10.38/1.82 inference(component_clause,[status(thm)],[f8113])).
% 10.38/1.82 fof(f11947,definition,(
% 10.38/1.82 sQ1081_spl <=> (doDivides0(xp,xn))),
% 10.38/1.82 introduced(definition,[new_symbols(definition,[sQ1081_spl])],[split_symbol_definition])).
% 10.38/1.82 fof(f11949,plain,(
% 10.38/1.82 ~doDivides0(xp,xn)|sQ1081_spl),
% 10.38/1.82 inference(component_clause,[status(thm)],[f11947])).
% 10.38/1.82 fof(f14051,plain,(
% 10.38/1.82 ~aNaturalNumber0(xp)|~aNaturalNumber0(xn)|xp=sz00|~doDivides0(xp,xn)|aNaturalNumber0(xq)),
% 10.38/1.82 inference(resolution,[status(thm)],[f140,f182])).
% 10.38/1.82 fof(f14054,plain,(
% 10.38/1.82 ~sQ0_spl|~sQ6_spl|sQ1_spl|~sQ1081_spl|sQ824_spl),
% 10.38/1.82 inference(split_clause,[status(thm)],[f14051,f270,f746,f273,f11947,f8110])).
% 10.38/1.82 fof(f14332,plain,(
% 10.38/1.82 $false|sQ1081_spl),
% 10.38/1.82 inference(forward_subsumption_resolution,[status(thm)],[f11949,f181])).
% 10.38/1.82 fof(f14333,plain,(
% 10.38/1.82 sQ1081_spl),
% 10.38/1.82 inference(contradiction_clause,[status(thm)],[f14332])).
% 10.38/1.82 fof(f15902,plain,(
% 10.38/1.82 $false|sQ713_spl),
% 10.38/1.82 inference(forward_subsumption_resolution,[status(thm)],[f7013,f179])).
% 10.38/1.82 fof(f15903,plain,(
% 10.38/1.82 sQ713_spl),
% 10.38/1.82 inference(contradiction_clause,[status(thm)],[f15902])).
% 10.38/1.82 fof(f15960,plain,(
% 10.38/1.82 sz00=sdtsldt0(xn,xp)|~sQ825_spl),
% 10.38/1.82 inference(forward_demodulation,[status(thm)],[f8114,f182])).
% 10.38/1.82 fof(f15961,plain,(
% 10.38/1.82 ~aNaturalNumber0(xp)|~aNaturalNumber0(xn)|xp=sz00|~doDivides0(xp,xn)|xn=sdtasdt0(xp,sz00)|~sQ825_spl),
% 10.38/1.82 inference(resolution,[status(thm)],[f15960,f141])).
% 10.38/1.82 fof(f15965,definition,(
% 10.38/1.82 sQ1332_spl <=> (xn=sdtasdt0(xp,sz00))),
% 10.38/1.82 introduced(definition,[new_symbols(definition,[sQ1332_spl])],[split_symbol_definition])).
% 10.38/1.82 fof(f15966,plain,(
% 10.38/1.82 xn=sdtasdt0(xp,sz00)|~sQ1332_spl),
% 10.38/1.82 inference(component_clause,[status(thm)],[f15965])).
% 10.38/1.82 fof(f15968,plain,(
% 10.38/1.82 ~sQ0_spl|~sQ6_spl|sQ1_spl|~sQ1081_spl|sQ1332_spl|~sQ825_spl),
% 10.38/1.82 inference(split_clause,[status(thm)],[f15961,f270,f746,f273,f11947,f15965,f8113])).
% 11.27/1.84 fof(f15978,plain,(
% 11.27/1.84 xn=sz00|~sQ1332_spl),
% 11.27/1.84 inference(forward_demodulation,[status(thm)],[f264,f15966])).
% 11.27/1.84 fof(f15979,plain,(
% 11.27/1.84 $false|~sQ1332_spl),
% 11.27/1.84 inference(forward_subsumption_resolution,[status(thm)],[f15978,f173])).
% 11.27/1.84 fof(f15980,plain,(
% 11.27/1.84 ~sQ1332_spl),
% 11.27/1.84 inference(contradiction_clause,[status(thm)],[f15979])).
% 11.27/1.84 fof(f16005,plain,(
% 11.27/1.84 ~aNaturalNumber0(xm)|~aNaturalNumber0(xq)|~aNaturalNumber0(xp)|xm=sz00|xq=sz00|~iLess0(xm,xn)|~isPrime0(xp)),
% 11.27/1.84 inference(resolution,[status(thm)],[f183,f8049])).
% 11.27/1.84 fof(f16019,plain,(
% 11.27/1.84 ~sQ8_spl|~sQ824_spl|~sQ0_spl|sQ42_spl|sQ825_spl|~sQ610_spl|~sQ713_spl),
% 11.27/1.84 inference(split_clause,[status(thm)],[f16005,f753,f8110,f270,f963,f8113,f5856,f7011])).
% 11.27/1.84 fof(f16047,plain,(
% 11.27/1.84 $false),
% 11.27/1.84 inference(sat_refutation,[status(thm)],[f276,f278,f805,f807,f1007,f3717,f5859,f14054,f14333,f15903,f15968,f15980,f16019])).
% 11.27/1.84 % SZS output end CNFRefutation for theBenchmark.p
% 11.27/1.85 % Elapsed time: 1.488390 seconds
% 11.27/1.85 % CPU time: 11.547718 seconds
% 11.27/1.85 % Total memory used: 210.391 MB
% 11.27/1.85 % Net memory used: 201.001 MB
%------------------------------------------------------------------------------