%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM475+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 : n011.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:42:59 PM UTC 2026
% Result : Theorem 59.39s 7.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM475+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.09/0.36 % Computer : n011.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:33:26 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 59.39/7.97 % Refutation found
% 59.39/7.97 % SZS status Theorem for theBenchmark: Theorem is valid
% 59.39/7.97 % SZS output start CNFRefutation for theBenchmark
% 59.39/7.97 fof(f2,axiom,(
% 59.39/7.97 aNaturalNumber0(sz00) ),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f4,axiom,(
% 59.39/7.97 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtpldt0(W0,W1)) ) )),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f5,axiom,(
% 59.39/7.97 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> aNaturalNumber0(sdtasdt0(W0,W1)) ) )),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f14,axiom,(
% 59.39/7.97 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2)| sdtpldt0(W1,W0) = sdtpldt0(W2,W0) )=> W1 = W2 ) ) )),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f19,definition,(
% 59.39/7.97 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( sdtlseqdt0(W0,W1)=> (! [W2] :( W2 = sdtmndt0(W1,W0)<=> ( aNaturalNumber0(W2)& sdtpldt0(W0,W2) = W1 ) ) )) ) )),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f20,axiom,(
% 59.39/7.97 (! [W0] :( aNaturalNumber0(W0)=> sdtlseqdt0(W0,W0) ) )),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f31,definition,(
% 59.39/7.97 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> ( ( W0 != sz00& doDivides0(W0,W1) )=> (! [W2] :( W2 = sdtsldt0(W1,W0)<=> ( aNaturalNumber0(W2)& W1 = sdtasdt0(W0,W2) ) ) )) ) )),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f34,hypothesis,(
% 59.39/7.97 ( aNaturalNumber0(xl)& aNaturalNumber0(xm)& aNaturalNumber0(xn) ) ),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f35,hypothesis,(
% 59.39/7.97 ( doDivides0(xl,xm)& doDivides0(xl,sdtpldt0(xm,xn)) ) ),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f36,hypothesis,(
% 59.39/7.97 xl != sz00 ),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f37,hypothesis,(
% 59.39/7.97 xp = sdtsldt0(xm,xl) ),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f38,hypothesis,(
% 59.39/7.97 xq = sdtsldt0(sdtpldt0(xm,xn),xl) ),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f39,hypothesis,(
% 59.39/7.97 sdtlseqdt0(xp,xq) ),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f40,hypothesis,(
% 59.39/7.97 xr = sdtmndt0(xq,xp) ),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f41,hypothesis,(
% 59.39/7.97 sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr)) = sdtpldt0(sdtasdt0(xl,xp),xn) ),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f42,conjecture,(
% 59.39/7.97 xn = sdtasdt0(xl,xr) ),
% 59.39/7.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 59.39/7.97 fof(f43,negated_conjecture,(
% 59.39/7.97 ~(xn = sdtasdt0(xl,xr) )),
% 59.39/7.97 inference(negated_conjecture,[status(cth)],[f42])).
% 59.39/7.97 fof(f47,plain,(
% 59.39/7.97 aNaturalNumber0(sz00)),
% 59.39/7.97 inference(cnf_transformation,[status(thm)],[f2])).
% 59.39/7.97 fof(f50,plain,(
% 59.39/7.97 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtpldt0(W0,W1)))),
% 59.39/7.97 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 59.39/7.97 fof(f51,plain,(
% 59.39/7.97 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtpldt0(X0,X1)))),
% 59.39/7.97 inference(cnf_transformation,[status(thm)],[f50])).
% 59.39/7.97 fof(f52,plain,(
% 59.39/7.97 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|aNaturalNumber0(sdtasdt0(W0,W1)))),
% 59.39/7.97 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 59.39/7.97 fof(f53,plain,(
% 59.39/7.97 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|aNaturalNumber0(sdtasdt0(X0,X1)))),
% 59.39/7.97 inference(cnf_transformation,[status(thm)],[f52])).
% 59.39/7.97 fof(f74,plain,(
% 59.39/7.97 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|((~sdtpldt0(W0,W1)=sdtpldt0(W0,W2)&~sdtpldt0(W1,W0)=sdtpldt0(W2,W0))|W1=W2))),
% 59.39/7.97 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 59.39/7.97 fof(f75,plain,(
% 59.39/7.97 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtpldt0(X0,X1)=sdtpldt0(X0,X2)|X1=X2)),
% 59.39/7.97 inference(cnf_transformation,[status(thm)],[f74])).
% 59.39/7.97 fof(f91,plain,(
% 59.39/7.97 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(~sdtlseqdt0(W0,W1)|(![W2]: (W2=sdtmndt0(W1,W0)<=>(aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1)))))),
% 59.39/7.98 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 59.39/7.98 fof(f92,plain,(
% 59.39/7.98 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(~sdtlseqdt0(W0,W1)|(![W2]: ((~W2=sdtmndt0(W1,W0)|(aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1))&(W2=sdtmndt0(W1,W0)|(~aNaturalNumber0(W2)|~sdtpldt0(W0,W2)=W1))))))),
% 59.39/7.98 inference(NNF_transformation,[status(thm)],[f91])).
% 59.39/7.98 fof(f93,plain,(
% 59.39/7.98 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|(~sdtlseqdt0(W0,W1)|((![W2]: (~W2=sdtmndt0(W1,W0)|(aNaturalNumber0(W2)&sdtpldt0(W0,W2)=W1)))&(![W2]: (W2=sdtmndt0(W1,W0)|(~aNaturalNumber0(W2)|~sdtpldt0(W0,W2)=W1))))))),
% 59.39/7.98 inference(miniscoping,[status(thm)],[f92])).
% 59.39/7.98 fof(f94,plain,(
% 59.39/7.98 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~sdtlseqdt0(X0,X1)|~X2=sdtmndt0(X1,X0)|aNaturalNumber0(X2))),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f93])).
% 59.39/7.98 fof(f97,plain,(
% 59.39/7.98 ![W0]: (~aNaturalNumber0(W0)|sdtlseqdt0(W0,W0))),
% 59.39/7.98 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 59.39/7.98 fof(f98,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|sdtlseqdt0(X0,X0))),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f97])).
% 59.39/7.98 fof(f131,plain,(
% 59.39/7.98 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|((W0=sz00|~doDivides0(W0,W1))|(![W2]: (W2=sdtsldt0(W1,W0)<=>(aNaturalNumber0(W2)&W1=sdtasdt0(W0,W2))))))),
% 59.39/7.98 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 59.39/7.98 fof(f132,plain,(
% 59.39/7.98 ![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)))))))),
% 59.39/7.98 inference(NNF_transformation,[status(thm)],[f131])).
% 59.39/7.98 fof(f133,plain,(
% 59.39/7.98 ![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)))))))),
% 59.39/7.98 inference(miniscoping,[status(thm)],[f132])).
% 59.39/7.98 fof(f134,plain,(
% 59.39/7.98 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=sz00|~doDivides0(X0,X1)|~X2=sdtsldt0(X1,X0)|aNaturalNumber0(X2))),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f133])).
% 59.39/7.98 fof(f141,plain,(
% 59.39/7.98 aNaturalNumber0(xl)),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f34])).
% 59.39/7.98 fof(f142,plain,(
% 59.39/7.98 aNaturalNumber0(xm)),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f34])).
% 59.39/7.98 fof(f143,plain,(
% 59.39/7.98 aNaturalNumber0(xn)),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f34])).
% 59.39/7.98 fof(f144,plain,(
% 59.39/7.98 doDivides0(xl,xm)),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f35])).
% 59.39/7.98 fof(f145,plain,(
% 59.39/7.98 doDivides0(xl,sdtpldt0(xm,xn))),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f35])).
% 59.39/7.98 fof(f146,plain,(
% 59.39/7.98 ~xl=sz00),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f36])).
% 59.39/7.98 fof(f147,plain,(
% 59.39/7.98 xp=sdtsldt0(xm,xl)),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f37])).
% 59.39/7.98 fof(f148,plain,(
% 59.39/7.98 xq=sdtsldt0(sdtpldt0(xm,xn),xl)),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f38])).
% 59.39/7.98 fof(f149,plain,(
% 59.39/7.98 sdtlseqdt0(xp,xq)),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f39])).
% 59.39/7.98 fof(f150,plain,(
% 59.39/7.98 xr=sdtmndt0(xq,xp)),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f40])).
% 59.39/7.98 fof(f151,plain,(
% 59.39/7.98 sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr))=sdtpldt0(sdtasdt0(xl,xp),xn)),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f41])).
% 59.39/7.98 fof(f152,plain,(
% 59.39/7.98 ~xn=sdtasdt0(xl,xr)),
% 59.39/7.98 inference(cnf_transformation,[status(thm)],[f43])).
% 59.39/7.98 fof(f154,plain,(
% 59.39/7.98 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~sdtlseqdt0(X0,X1)|aNaturalNumber0(sdtmndt0(X1,X0)))),
% 59.39/7.98 inference(destructive_equality_resolution,[status(thm)],[f94])).
% 59.39/7.98 fof(f160,plain,(
% 59.39/7.98 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|X0=sz00|~doDivides0(X0,X1)|aNaturalNumber0(sdtsldt0(X1,X0)))),
% 59.39/7.98 inference(destructive_equality_resolution,[status(thm)],[f134])).
% 59.39/7.98 fof(f170,definition,(
% 59.39/7.98 sQ0_spl <=> (aNaturalNumber0(xl))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f172,plain,(
% 59.39/7.98 ~aNaturalNumber0(xl)|sQ0_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f170])).
% 59.39/7.98 fof(f173,definition,(
% 59.39/7.98 sQ1_spl <=> (aNaturalNumber0(xn))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f175,plain,(
% 59.39/7.98 ~aNaturalNumber0(xn)|sQ1_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f173])).
% 59.39/7.98 fof(f214,definition,(
% 59.39/7.98 sQ3_spl <=> (aNaturalNumber0(sdtasdt0(xl,xp)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f216,plain,(
% 59.39/7.98 ~aNaturalNumber0(sdtasdt0(xl,xp))|sQ3_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f214])).
% 59.39/7.98 fof(f217,definition,(
% 59.39/7.98 sQ4_spl <=> (aNaturalNumber0(sdtasdt0(xl,xr)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f219,plain,(
% 59.39/7.98 ~aNaturalNumber0(sdtasdt0(xl,xr))|sQ4_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f217])).
% 59.39/7.98 fof(f263,plain,(
% 59.39/7.98 ~aNaturalNumber0(xl)|~aNaturalNumber0(xr)|sQ4_spl),
% 59.39/7.98 inference(resolution,[status(thm)],[f219,f53])).
% 59.39/7.98 fof(f264,definition,(
% 59.39/7.98 sQ6_spl <=> (aNaturalNumber0(xr))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f266,plain,(
% 59.39/7.98 ~aNaturalNumber0(xr)|sQ6_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f264])).
% 59.39/7.98 fof(f267,plain,(
% 59.39/7.98 ~sQ0_spl|~sQ6_spl|sQ4_spl),
% 59.39/7.98 inference(split_clause,[status(thm)],[f263,f170,f264,f217])).
% 59.39/7.98 fof(f268,plain,(
% 59.39/7.98 $false|sQ0_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f172,f141])).
% 59.39/7.98 fof(f269,plain,(
% 59.39/7.98 sQ0_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f268])).
% 59.39/7.98 fof(f270,plain,(
% 59.39/7.98 $false|sQ1_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f175,f143])).
% 59.39/7.98 fof(f271,plain,(
% 59.39/7.98 sQ1_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f270])).
% 59.39/7.98 fof(f359,definition,(
% 59.39/7.98 sQ11_spl <=> (aNaturalNumber0(xm))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f361,plain,(
% 59.39/7.98 ~aNaturalNumber0(xm)|sQ11_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f359])).
% 59.39/7.98 fof(f366,plain,(
% 59.39/7.98 $false|sQ11_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f361,f142])).
% 59.39/7.98 fof(f367,plain,(
% 59.39/7.98 sQ11_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f366])).
% 59.39/7.98 fof(f1163,definition,(
% 59.39/7.98 sQ48_spl <=> (sdtlseqdt0(xn,xn))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f1165,plain,(
% 59.39/7.98 ~sdtlseqdt0(xn,xn)|sQ48_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f1163])).
% 59.39/7.98 fof(f1180,definition,(
% 59.39/7.98 sQ49_spl <=> (sdtlseqdt0(xl,xl))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f1182,plain,(
% 59.39/7.98 ~sdtlseqdt0(xl,xl)|sQ49_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f1180])).
% 59.39/7.98 fof(f1185,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtasdt0(X0,xl)))),
% 59.39/7.98 inference(resolution,[status(thm)],[f53,f141])).
% 59.39/7.98 fof(f1186,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtasdt0(X0,xn)))),
% 59.39/7.98 inference(resolution,[status(thm)],[f53,f143])).
% 59.39/7.98 fof(f1319,definition,(
% 59.39/7.98 sQ51_spl <=> (aNaturalNumber0(xp))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f1321,plain,(
% 59.39/7.98 ~aNaturalNumber0(xp)|sQ51_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f1319])).
% 59.39/7.98 fof(f1322,definition,(
% 59.39/7.98 sQ52_spl <=> (aNaturalNumber0(xq))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f1324,plain,(
% 59.39/7.98 ~aNaturalNumber0(xq)|sQ52_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f1322])).
% 59.39/7.98 fof(f1400,plain,(
% 59.39/7.98 aNaturalNumber0(sdtasdt0(xn,xn))),
% 59.39/7.98 inference(resolution,[status(thm)],[f1186,f143])).
% 59.39/7.98 fof(f1833,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtpldt0(X0,xm)))),
% 59.39/7.98 inference(resolution,[status(thm)],[f51,f142])).
% 59.39/7.98 fof(f1836,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtpldt0(X0,xl)))),
% 59.39/7.98 inference(resolution,[status(thm)],[f51,f141])).
% 59.39/7.98 fof(f1837,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|aNaturalNumber0(sdtpldt0(X0,xn)))),
% 59.39/7.98 inference(resolution,[status(thm)],[f51,f143])).
% 59.39/7.98 fof(f1861,definition,(
% 59.39/7.98 sQ63_spl <=> (aNaturalNumber0(sdtpldt0(xm,xn)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f1863,plain,(
% 59.39/7.98 ~aNaturalNumber0(sdtpldt0(xm,xn))|sQ63_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f1861])).
% 59.39/7.98 fof(f2004,plain,(
% 59.39/7.98 aNaturalNumber0(sdtpldt0(xl,xl))),
% 59.39/7.98 inference(resolution,[status(thm)],[f1836,f141])).
% 59.39/7.98 fof(f2164,plain,(
% 59.39/7.98 aNaturalNumber0(sdtpldt0(xm,xn))),
% 59.39/7.98 inference(resolution,[status(thm)],[f1837,f142])).
% 59.39/7.98 fof(f2169,plain,(
% 59.39/7.98 $false|sQ63_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f2164,f1863])).
% 59.39/7.98 fof(f2170,plain,(
% 59.39/7.98 sQ63_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f2169])).
% 59.39/7.98 fof(f2525,plain,(
% 59.39/7.98 ~aNaturalNumber0(xl)|~aNaturalNumber0(xm)|xl=sz00|aNaturalNumber0(sdtsldt0(xm,xl))),
% 59.39/7.98 inference(resolution,[status(thm)],[f160,f144])).
% 59.39/7.98 fof(f2526,plain,(
% 59.39/7.98 ~aNaturalNumber0(xl)|~aNaturalNumber0(sdtpldt0(xm,xn))|xl=sz00|aNaturalNumber0(sdtsldt0(sdtpldt0(xm,xn),xl))),
% 59.39/7.98 inference(resolution,[status(thm)],[f160,f145])).
% 59.39/7.98 fof(f2527,definition,(
% 59.39/7.98 sQ67_spl <=> (xl=sz00)),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f2528,plain,(
% 59.39/7.98 xl=sz00|~sQ67_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f2527])).
% 59.39/7.98 fof(f2530,definition,(
% 59.39/7.98 sQ68_spl <=> (aNaturalNumber0(sdtsldt0(xm,xl)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f2531,plain,(
% 59.39/7.98 aNaturalNumber0(sdtsldt0(xm,xl))|~sQ68_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f2530])).
% 59.39/7.98 fof(f2533,plain,(
% 59.39/7.98 ~sQ0_spl|~sQ11_spl|sQ67_spl|sQ68_spl),
% 59.39/7.98 inference(split_clause,[status(thm)],[f2525,f170,f359,f2527,f2530])).
% 59.39/7.98 fof(f2534,definition,(
% 59.39/7.98 sQ69_spl <=> (aNaturalNumber0(sdtsldt0(sdtpldt0(xm,xn),xl)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f2535,plain,(
% 59.39/7.98 aNaturalNumber0(sdtsldt0(sdtpldt0(xm,xn),xl))|~sQ69_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f2534])).
% 59.39/7.98 fof(f2537,plain,(
% 59.39/7.98 ~sQ0_spl|~sQ63_spl|sQ67_spl|sQ69_spl),
% 59.39/7.98 inference(split_clause,[status(thm)],[f2526,f170,f1861,f2527,f2534])).
% 59.39/7.98 fof(f2538,plain,(
% 59.39/7.98 $false|~sQ67_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f2528,f146])).
% 59.39/7.98 fof(f2539,plain,(
% 59.39/7.98 ~sQ67_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f2538])).
% 59.39/7.98 fof(f2540,plain,(
% 59.39/7.98 aNaturalNumber0(xq)|~sQ69_spl),
% 59.39/7.98 inference(forward_demodulation,[status(thm)],[f148,f2535])).
% 59.39/7.98 fof(f2541,plain,(
% 59.39/7.98 $false|sQ52_spl|~sQ69_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f2540,f1324])).
% 59.39/7.98 fof(f2542,plain,(
% 59.39/7.98 sQ52_spl|~sQ69_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f2541])).
% 59.39/7.98 fof(f2543,plain,(
% 59.39/7.98 aNaturalNumber0(xp)|~sQ68_spl),
% 59.39/7.98 inference(forward_demodulation,[status(thm)],[f147,f2531])).
% 59.39/7.98 fof(f2544,plain,(
% 59.39/7.98 $false|sQ51_spl|~sQ68_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f2543,f1321])).
% 59.39/7.98 fof(f2545,plain,(
% 59.39/7.98 sQ51_spl|~sQ68_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f2544])).
% 59.39/7.98 fof(f3195,plain,(
% 59.39/7.98 aNaturalNumber0(sdtpldt0(xn,xm))),
% 59.39/7.98 inference(resolution,[status(thm)],[f143,f1833])).
% 59.39/7.98 fof(f3202,plain,(
% 59.39/7.98 aNaturalNumber0(sdtasdt0(xn,xl))),
% 59.39/7.98 inference(resolution,[status(thm)],[f143,f1185])).
% 59.39/7.98 fof(f3296,definition,(
% 59.39/7.98 ![X0]: (sQ155_spl <=> (~aNaturalNumber0(X0)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f3297,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sQ155_spl)),
% 59.39/7.98 inference(component_clause,[status(thm)],[f3296])).
% 59.39/7.98 fof(f3443,plain,(
% 59.39/7.98 ~aNaturalNumber0(sdtasdt0(xl,xp))|~aNaturalNumber0(sdtasdt0(xl,xr))|~aNaturalNumber0(xn)|sdtasdt0(xl,xr)=xn),
% 59.39/7.98 inference(resolution,[status(thm)],[f151,f75])).
% 59.39/7.98 fof(f3449,definition,(
% 59.39/7.98 sQ159_spl <=> (sdtasdt0(xl,xr)=xn)),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f3450,plain,(
% 59.39/7.98 sdtasdt0(xl,xr)=xn|~sQ159_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f3449])).
% 59.39/7.98 fof(f3452,plain,(
% 59.39/7.98 ~sQ3_spl|~sQ4_spl|~sQ1_spl|sQ159_spl),
% 59.39/7.98 inference(split_clause,[status(thm)],[f3443,f214,f217,f173,f3449])).
% 59.39/7.98 fof(f3464,plain,(
% 59.39/7.98 $false|~sQ159_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f3450,f152])).
% 59.39/7.98 fof(f3465,plain,(
% 59.39/7.98 ~sQ159_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f3464])).
% 59.39/7.98 fof(f3466,plain,(
% 59.39/7.98 $false|~sQ155_spl),
% 59.39/7.98 inference(backward_subsumption_resolution,[status(thm)],[f141,f3297])).
% 59.39/7.98 fof(f3476,plain,(
% 59.39/7.98 ~sQ155_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f3466])).
% 59.39/7.98 fof(f3985,plain,(
% 59.39/7.98 ~aNaturalNumber0(xp)|~aNaturalNumber0(xq)|aNaturalNumber0(sdtmndt0(xq,xp))),
% 59.39/7.98 inference(resolution,[status(thm)],[f149,f154])).
% 59.39/7.98 fof(f3989,definition,(
% 59.39/7.98 sQ183_spl <=> (aNaturalNumber0(sdtmndt0(xq,xp)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f3990,plain,(
% 59.39/7.98 aNaturalNumber0(sdtmndt0(xq,xp))|~sQ183_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f3989])).
% 59.39/7.98 fof(f3992,plain,(
% 59.39/7.98 ~sQ51_spl|~sQ52_spl|sQ183_spl),
% 59.39/7.98 inference(split_clause,[status(thm)],[f3985,f1319,f1322,f3989])).
% 59.39/7.98 fof(f5078,definition,(
% 59.39/7.98 ![X0]: (sQ276_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(xq,X0)=sdtpldt0(xq,X0)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ276_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f5079,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(xq,X0)=sdtpldt0(xq,X0)|~sQ276_spl)),
% 59.39/7.98 inference(component_clause,[status(thm)],[f5078])).
% 59.39/7.98 fof(f5082,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sQ276_spl)),
% 59.39/7.98 inference(trivial_equality_resolution,[status(thm)],[f5079])).
% 59.39/7.98 fof(f5092,plain,(
% 59.39/7.98 $false|~sQ276_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f47,f5082])).
% 59.39/7.98 fof(f5093,plain,(
% 59.39/7.98 ~sQ276_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f5092])).
% 59.39/7.98 fof(f6373,plain,(
% 59.39/7.98 sdtlseqdt0(xm,xm)),
% 59.39/7.98 inference(resolution,[status(thm)],[f98,f142])).
% 59.39/7.98 fof(f6414,plain,(
% 59.39/7.98 sdtlseqdt0(xl,xl)),
% 59.39/7.98 inference(resolution,[status(thm)],[f141,f98])).
% 59.39/7.98 fof(f6698,plain,(
% 59.39/7.98 sdtlseqdt0(xn,xn)),
% 59.39/7.98 inference(resolution,[status(thm)],[f143,f98])).
% 59.39/7.98 fof(f6966,definition,(
% 59.39/7.98 sQ360_spl <=> (sdtlseqdt0(xm,xm))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f6968,plain,(
% 59.39/7.98 ~sdtlseqdt0(xm,xm)|sQ360_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f6966])).
% 59.39/7.98 fof(f6982,plain,(
% 59.39/7.98 $false|sQ360_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f6968,f6373])).
% 59.39/7.98 fof(f6983,plain,(
% 59.39/7.98 sQ360_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f6982])).
% 59.39/7.98 fof(f7104,plain,(
% 59.39/7.98 $false|sQ48_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f1165,f6698])).
% 59.39/7.98 fof(f7105,plain,(
% 59.39/7.98 sQ48_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f7104])).
% 59.39/7.98 fof(f7525,plain,(
% 59.39/7.98 $false|sQ49_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f1182,f6414])).
% 59.39/7.98 fof(f7526,plain,(
% 59.39/7.98 sQ49_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f7525])).
% 59.39/7.98 fof(f7797,definition,(
% 59.39/7.98 ![X0]: (sQ412_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(X0,sdtpldt0(xq,xm))=sdtpldt0(X0,sdtpldt0(xq,xm))))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ412_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f7798,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(X0,sdtpldt0(xq,xm))=sdtpldt0(X0,sdtpldt0(xq,xm))|~sQ412_spl)),
% 59.39/7.98 inference(component_clause,[status(thm)],[f7797])).
% 59.39/7.98 fof(f7818,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sQ412_spl)),
% 59.39/7.98 inference(trivial_equality_resolution,[status(thm)],[f7798])).
% 59.39/7.98 fof(f7824,plain,(
% 59.39/7.98 $false|~sQ412_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f141,f7818])).
% 59.39/7.98 fof(f7825,plain,(
% 59.39/7.98 ~sQ412_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f7824])).
% 59.39/7.98 fof(f12157,definition,(
% 59.39/7.98 ![X0]: (sQ624_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(sdtmndt0(xl,xl),X0)=sdtpldt0(sdtmndt0(xl,xl),X0)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ624_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f12158,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(sdtmndt0(xl,xl),X0)=sdtpldt0(sdtmndt0(xl,xl),X0)|~sQ624_spl)),
% 59.39/7.98 inference(component_clause,[status(thm)],[f12157])).
% 59.39/7.98 fof(f12161,definition,(
% 59.39/7.98 ![X0]: (sQ625_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(sK0_skl(xl,xl),X0)=sdtpldt0(sK0_skl(xl,xl),X0)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ625_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f12162,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(sK0_skl(xl,xl),X0)=sdtpldt0(sK0_skl(xl,xl),X0)|~sQ625_spl)),
% 59.39/7.98 inference(component_clause,[status(thm)],[f12161])).
% 59.39/7.98 fof(f12168,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sQ625_spl)),
% 59.39/7.98 inference(trivial_equality_resolution,[status(thm)],[f12162])).
% 59.39/7.98 fof(f12169,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sQ624_spl)),
% 59.39/7.98 inference(trivial_equality_resolution,[status(thm)],[f12158])).
% 59.39/7.98 fof(f12190,plain,(
% 59.39/7.98 $false|~sQ625_spl),
% 59.39/7.98 inference(backward_subsumption_resolution,[status(thm)],[f143,f12168])).
% 59.39/7.98 fof(f12198,plain,(
% 59.39/7.98 ~sQ625_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f12190])).
% 59.39/7.98 fof(f12199,plain,(
% 59.39/7.98 $false|~sQ624_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f143,f12169])).
% 59.39/7.98 fof(f12200,plain,(
% 59.39/7.98 ~sQ624_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f12199])).
% 59.39/7.98 fof(f13072,definition,(
% 59.39/7.98 ![X0]: (sQ676_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(X0,sdtsldt0(xq,sz10))=sdtpldt0(X0,sdtsldt0(xq,sz10))))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ676_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f13073,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(X0,sdtsldt0(xq,sz10))=sdtpldt0(X0,sdtsldt0(xq,sz10))|~sQ676_spl)),
% 59.39/7.98 inference(component_clause,[status(thm)],[f13072])).
% 59.39/7.98 fof(f13085,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sQ676_spl)),
% 59.39/7.98 inference(trivial_equality_resolution,[status(thm)],[f13073])).
% 59.39/7.98 fof(f13095,plain,(
% 59.39/7.98 $false|~sQ676_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f141,f13085])).
% 59.39/7.98 fof(f13096,plain,(
% 59.39/7.98 ~sQ676_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f13095])).
% 59.39/7.98 fof(f13295,definition,(
% 59.39/7.98 ![X0]: (sQ693_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(sdtasdt0(xl,xl),X0)=sdtpldt0(sdtasdt0(xl,xl),X0)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ693_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f13296,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(sdtasdt0(xl,xl),X0)=sdtpldt0(sdtasdt0(xl,xl),X0)|~sQ693_spl)),
% 59.39/7.98 inference(component_clause,[status(thm)],[f13295])).
% 59.39/7.98 fof(f13299,definition,(
% 59.39/7.98 ![X0]: (sQ694_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(sdtasdt0(xl,xr),X0)=sdtpldt0(sdtasdt0(xl,xr),X0)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ694_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f13300,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(sdtasdt0(xl,xr),X0)=sdtpldt0(sdtasdt0(xl,xr),X0)|~sQ694_spl)),
% 59.39/7.98 inference(component_clause,[status(thm)],[f13299])).
% 59.39/7.98 fof(f13308,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sQ694_spl)),
% 59.39/7.98 inference(trivial_equality_resolution,[status(thm)],[f13300])).
% 59.39/7.98 fof(f13309,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sQ693_spl)),
% 59.39/7.98 inference(trivial_equality_resolution,[status(thm)],[f13296])).
% 59.39/7.98 fof(f13311,plain,(
% 59.39/7.98 $false|~sQ694_spl),
% 59.39/7.98 inference(backward_subsumption_resolution,[status(thm)],[f2004,f13308])).
% 59.39/7.98 fof(f13318,plain,(
% 59.39/7.98 ~sQ694_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f13311])).
% 59.39/7.98 fof(f13319,plain,(
% 59.39/7.98 $false|~sQ693_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f141,f13309])).
% 59.39/7.98 fof(f13320,plain,(
% 59.39/7.98 ~sQ693_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f13319])).
% 59.39/7.98 fof(f13865,plain,(
% 59.39/7.98 aNaturalNumber0(xr)|~sQ183_spl),
% 59.39/7.98 inference(forward_demodulation,[status(thm)],[f150,f3990])).
% 59.39/7.98 fof(f13866,plain,(
% 59.39/7.98 $false|sQ6_spl|~sQ183_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f13865,f266])).
% 59.39/7.98 fof(f13867,plain,(
% 59.39/7.98 sQ6_spl|~sQ183_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f13866])).
% 59.39/7.98 fof(f14497,definition,(
% 59.39/7.98 ![X0]: (sQ747_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(xr,X0)=sdtpldt0(xr,X0)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ747_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f14498,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(xr,X0)=sdtpldt0(xr,X0)|~sQ747_spl)),
% 59.39/7.98 inference(component_clause,[status(thm)],[f14497])).
% 59.39/7.98 fof(f14501,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sQ747_spl)),
% 59.39/7.98 inference(trivial_equality_resolution,[status(thm)],[f14498])).
% 59.39/7.98 fof(f14502,plain,(
% 59.39/7.98 $false|~sQ747_spl),
% 59.39/7.98 inference(backward_subsumption_resolution,[status(thm)],[f47,f14501])).
% 59.39/7.98 fof(f14508,plain,(
% 59.39/7.98 ~sQ747_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f14502])).
% 59.39/7.98 fof(f14642,definition,(
% 59.39/7.98 ![X0]: (sQ750_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(X0,sK0_skl(xq,xm))=sdtpldt0(X0,sK0_skl(xq,xm))))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ750_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f14643,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(X0,sK0_skl(xq,xm))=sdtpldt0(X0,sK0_skl(xq,xm))|~sQ750_spl)),
% 59.39/7.98 inference(component_clause,[status(thm)],[f14642])).
% 59.39/7.98 fof(f14669,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sQ750_spl)),
% 59.39/7.98 inference(trivial_equality_resolution,[status(thm)],[f14643])).
% 59.39/7.98 fof(f14717,plain,(
% 59.39/7.98 $false|~sQ750_spl),
% 59.39/7.98 inference(backward_subsumption_resolution,[status(thm)],[f3202,f14669])).
% 59.39/7.98 fof(f14728,plain,(
% 59.39/7.98 ~sQ750_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f14717])).
% 59.39/7.98 fof(f17890,definition,(
% 59.39/7.98 ![X0]: (sQ890_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(sK0_skl(xq,xm),X0)=sdtpldt0(sK0_skl(xq,xm),X0)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ890_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f17891,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(sK0_skl(xq,xm),X0)=sdtpldt0(sK0_skl(xq,xm),X0)|~sQ890_spl)),
% 59.39/7.98 inference(component_clause,[status(thm)],[f17890])).
% 59.39/7.98 fof(f17895,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sQ890_spl)),
% 59.39/7.98 inference(trivial_equality_resolution,[status(thm)],[f17891])).
% 59.39/7.98 fof(f17898,plain,(
% 59.39/7.98 $false|~sQ890_spl),
% 59.39/7.98 inference(backward_subsumption_resolution,[status(thm)],[f142,f17895])).
% 59.39/7.98 fof(f17902,plain,(
% 59.39/7.98 ~sQ890_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f17898])).
% 59.39/7.98 fof(f19895,definition,(
% 59.39/7.98 ![X0]: (sQ968_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(X0,sdtasdt0(xq,xq))=sdtpldt0(X0,sdtasdt0(xq,xq))))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ968_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f19896,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(X0,sdtasdt0(xq,xq))=sdtpldt0(X0,sdtasdt0(xq,xq))|~sQ968_spl)),
% 59.39/7.98 inference(component_clause,[status(thm)],[f19895])).
% 59.39/7.98 fof(f19900,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sQ968_spl)),
% 59.39/7.98 inference(trivial_equality_resolution,[status(thm)],[f19896])).
% 59.39/7.98 fof(f19902,plain,(
% 59.39/7.98 $false|~sQ968_spl),
% 59.39/7.98 inference(backward_subsumption_resolution,[status(thm)],[f142,f19900])).
% 59.39/7.98 fof(f19907,plain,(
% 59.39/7.98 ~sQ968_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f19902])).
% 59.39/7.98 fof(f21975,definition,(
% 59.39/7.98 ![X0]: (sQ1022_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(sdtasdt0(xn,xn),X0)=sdtpldt0(sdtasdt0(xn,xn),X0)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ1022_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f21976,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(sdtasdt0(xn,xn),X0)=sdtpldt0(sdtasdt0(xn,xn),X0)|~sQ1022_spl)),
% 59.39/7.98 inference(component_clause,[status(thm)],[f21975])).
% 59.39/7.98 fof(f21997,plain,(
% 59.39/7.98 ![X0]: (~aNaturalNumber0(X0)|~sQ1022_spl)),
% 59.39/7.98 inference(trivial_equality_resolution,[status(thm)],[f21976])).
% 59.39/7.98 fof(f21998,plain,(
% 59.39/7.98 $false|~sQ1022_spl),
% 59.39/7.98 inference(backward_subsumption_resolution,[status(thm)],[f1400,f21997])).
% 59.39/7.98 fof(f22005,plain,(
% 59.39/7.98 ~sQ1022_spl),
% 59.39/7.98 inference(contradiction_clause,[status(thm)],[f21998])).
% 59.39/7.98 fof(f22079,definition,(
% 59.39/7.98 sQ1030_spl <=> (doDivides0(xl,sdtpldt0(xm,xn)))),
% 59.39/7.98 introduced(definition,[new_symbols(definition,[sQ1030_spl])],[split_symbol_definition])).
% 59.39/7.98 fof(f22081,plain,(
% 59.39/7.98 ~doDivides0(xl,sdtpldt0(xm,xn))|sQ1030_spl),
% 59.39/7.98 inference(component_clause,[status(thm)],[f22079])).
% 59.39/7.98 fof(f22084,plain,(
% 59.39/7.98 $false|sQ1030_spl),
% 59.39/7.98 inference(forward_subsumption_resolution,[status(thm)],[f22081,f145])).
% 59.39/7.99 fof(f22085,plain,(
% 59.39/7.99 sQ1030_spl),
% 59.39/7.99 inference(contradiction_clause,[status(thm)],[f22084])).
% 59.39/7.99 fof(f22656,definition,(
% 59.39/7.99 ![X0]: (sQ1052_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(X0,sdtpldt0(xl,xl))=sdtpldt0(X0,sdtpldt0(xl,xl))))),
% 59.39/7.99 introduced(definition,[new_symbols(definition,[sQ1052_spl])],[split_symbol_definition])).
% 59.39/7.99 fof(f22657,plain,(
% 59.39/7.99 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(X0,sdtpldt0(xl,xl))=sdtpldt0(X0,sdtpldt0(xl,xl))|~sQ1052_spl)),
% 59.39/7.99 inference(component_clause,[status(thm)],[f22656])).
% 59.39/7.99 fof(f22668,plain,(
% 59.39/7.99 ![X0]: (~aNaturalNumber0(X0)|~sQ1052_spl)),
% 59.39/7.99 inference(trivial_equality_resolution,[status(thm)],[f22657])).
% 59.39/7.99 fof(f22689,plain,(
% 59.39/7.99 $false|~sQ1052_spl),
% 59.39/7.99 inference(backward_subsumption_resolution,[status(thm)],[f47,f22668])).
% 59.39/7.99 fof(f22701,plain,(
% 59.39/7.99 ~sQ1052_spl),
% 59.39/7.99 inference(contradiction_clause,[status(thm)],[f22689])).
% 59.39/7.99 fof(f23328,definition,(
% 59.39/7.99 ![X0]: (sQ1077_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(sdtpldt0(xn,xm),X0)=sdtpldt0(sdtpldt0(xn,xm),X0)))),
% 59.39/7.99 introduced(definition,[new_symbols(definition,[sQ1077_spl])],[split_symbol_definition])).
% 59.39/8.02 fof(f23329,plain,(
% 59.39/8.02 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(sdtpldt0(xn,xm),X0)=sdtpldt0(sdtpldt0(xn,xm),X0)|~sQ1077_spl)),
% 59.39/8.02 inference(component_clause,[status(thm)],[f23328])).
% 59.39/8.02 fof(f23336,plain,(
% 59.39/8.02 ![X0]: (~aNaturalNumber0(X0)|~sQ1077_spl)),
% 59.39/8.02 inference(trivial_equality_resolution,[status(thm)],[f23329])).
% 59.39/8.02 fof(f23337,plain,(
% 59.39/8.02 $false|~sQ1077_spl),
% 59.39/8.02 inference(backward_subsumption_resolution,[status(thm)],[f3195,f23336])).
% 59.39/8.02 fof(f23345,plain,(
% 59.39/8.02 ~sQ1077_spl),
% 59.39/8.02 inference(contradiction_clause,[status(thm)],[f23337])).
% 59.39/8.02 fof(f25460,definition,(
% 59.39/8.02 ![X0]: (sQ1175_spl <=> (~aNaturalNumber0(X0)|~sdtpldt0(sdtmndt0(xq,xq),X0)=sdtpldt0(sdtmndt0(xq,xq),X0)))),
% 59.39/8.02 introduced(definition,[new_symbols(definition,[sQ1175_spl])],[split_symbol_definition])).
% 59.39/8.02 fof(f25461,plain,(
% 59.39/8.02 ![X0]: (~aNaturalNumber0(X0)|~sdtpldt0(sdtmndt0(xq,xq),X0)=sdtpldt0(sdtmndt0(xq,xq),X0)|~sQ1175_spl)),
% 59.39/8.02 inference(component_clause,[status(thm)],[f25460])).
% 59.39/8.02 fof(f25475,plain,(
% 59.39/8.02 ![X0]: (~aNaturalNumber0(X0)|~sQ1175_spl)),
% 59.39/8.02 inference(trivial_equality_resolution,[status(thm)],[f25461])).
% 59.39/8.02 fof(f25488,plain,(
% 59.39/8.02 $false|~sQ1175_spl),
% 59.39/8.02 inference(forward_subsumption_resolution,[status(thm)],[f143,f25475])).
% 59.39/8.02 fof(f25489,plain,(
% 59.39/8.02 ~sQ1175_spl),
% 59.39/8.02 inference(contradiction_clause,[status(thm)],[f25488])).
% 59.39/8.02 fof(f26601,plain,(
% 59.39/8.02 ~aNaturalNumber0(xl)|~aNaturalNumber0(xp)|sQ3_spl),
% 59.39/8.02 inference(resolution,[status(thm)],[f216,f53])).
% 59.39/8.02 fof(f26602,plain,(
% 59.39/8.02 ~sQ0_spl|~sQ51_spl|sQ3_spl),
% 59.39/8.02 inference(split_clause,[status(thm)],[f26601,f170,f1319,f214])).
% 59.39/8.02 fof(f26603,plain,(
% 59.39/8.02 $false),
% 59.39/8.02 inference(sat_refutation,[status(thm)],[f267,f269,f271,f367,f2170,f2533,f2537,f2539,f2542,f2545,f3452,f3465,f3476,f3992,f5093,f6983,f7105,f7526,f7825,f12198,f12200,f13096,f13318,f13320,f13867,f14508,f14728,f17902,f19907,f22005,f22085,f22701,f23345,f25489,f26602])).
% 59.39/8.02 % SZS output end CNFRefutation for theBenchmark.p
% 59.39/8.03 % Elapsed time: 7.655036 seconds
% 59.39/8.03 % CPU time: 60.131439 seconds
% 59.39/8.03 % Total memory used: 410.216 MB
% 59.39/8.03 % Net memory used: 384.490 MB
%------------------------------------------------------------------------------