%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX043+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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 03:13:35 PM UTC 2026
% Result : Theorem 46.78s 6.36s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX043+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n010.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.36 % DateTime : Mon Sep 21 10:23:56 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 46.78/6.36 % Refutation found
% 46.78/6.36 % SZS status Theorem for theBenchmark: Theorem is valid
% 46.78/6.36 % SZS output start CNFRefutation for theBenchmark
% 46.78/6.36 fof(f1,axiom,(
% 46.78/6.36 (! [Xx3] : '0' != s(Xx3) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f13,axiom,(
% 46.78/6.36 (! [Xx17] :~ ( nat_succeeds(Xx17)& nat_fails(Xx17) ) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f21,axiom,(
% 46.78/6.36 (! [Xx1,Xx2] :( '@=<_succeeds'(Xx1,Xx2)<=> ( (? [Xx3,Xx4] :( Xx1 = s(Xx3)& Xx2 = s(Xx4)& '@=<_succeeds'(Xx3,Xx4) ))| Xx1 = '0' ) ) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f22,axiom,(
% 46.78/6.36 (! [Xx1,Xx2] :( '@=<_fails'(Xx1,Xx2)<=> ( (! [Xx3,Xx4] :( Xx1 != s(Xx3)| Xx2 != s(Xx4)| '@=<_fails'(Xx3,Xx4) ))& Xx1 != '0' ) ) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f28,axiom,(
% 46.78/6.36 (! [Xx1] :( nat_fails(Xx1)<=> ( (! [Xx2] :( Xx1 != s(Xx2)| nat_fails(Xx2) ))& Xx1 != '0' ) ) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f32,axiom,(
% 46.78/6.36 (! [Xx] :( nat_succeeds(Xx)=> nat_terminates(Xx) ) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f33,axiom,(
% 46.78/6.36 (! [Xx] :( nat_succeeds(Xx)=> gr(Xx) ) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f45,axiom,(
% 46.78/6.36 (! [Xy] : '@+'('0',Xy) = Xy )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f46,axiom,(
% 46.78/6.36 (! [Xx,Xy] :( nat_succeeds(Xx)=> '@+'(s(Xx),Xy) = s('@+'(Xx,Xy)) ) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f73,axiom,(
% 46.78/6.36 (! [Xx,Xy] :( '@<_succeeds'(Xx,Xy)=> nat_succeeds(Xx) ) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f74,axiom,(
% 46.78/6.36 (! [Xx,Xy] :( '@<_succeeds'(Xx,Xy)=> (? [Xz] : Xy = s(Xz) )) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f79,axiom,(
% 46.78/6.36 (! [Xx] :( nat_succeeds(Xx)=> ~ '@<_succeeds'(Xx,Xx) ) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f86,axiom,(
% 46.78/6.36 (! [Xx,Xy] :( '@=<_succeeds'(Xx,Xy)=> nat_succeeds(Xx) ) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f97,axiom,(
% 46.78/6.36 (! [Xx,Xy,Xz] :( ( '@=<_succeeds'(Xx,Xy)& '@<_succeeds'(Xy,Xz) )=> '@<_succeeds'(Xx,Xz) ) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f107,axiom,(
% 46.78/6.36 ( (! [Xx] :( ( (? [Xx2] :( Xx = s(Xx2)& nat_succeeds(Xx2)& (! [Xy,Xz] :( '@=<_succeeds'(Xy,Xz)=> '@=<_succeeds'('@+'(Xx2,Xy),'@+'(Xx2,Xz)) ) )))| Xx = '0' )=> (! [Xy,Xz] :( '@=<_succeeds'(Xy,Xz)=> '@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ) )))=> (! [Xx] :( nat_succeeds(Xx)=> (! [Xy,Xz] :( '@=<_succeeds'(Xy,Xz)=> '@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ) )) )) ),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f108,conjecture,(
% 46.78/6.36 (! [Xx,Xy,Xz] :( ( nat_succeeds(Xx)& '@=<_succeeds'(Xy,Xz) )=> '@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ) )),
% 46.78/6.36 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 46.78/6.36 fof(f109,negated_conjecture,(
% 46.78/6.36 ~((! [Xx,Xy,Xz] :( ( nat_succeeds(Xx)& '@=<_succeeds'(Xy,Xz) )=> '@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz)) ) ))),
% 46.78/6.36 inference(negated_conjecture,[status(cth)],[f108])).
% 46.78/6.36 fof(f110,plain,(
% 46.78/6.36 ![X0]: (~'0'=s(X0))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f1])).
% 46.78/6.36 fof(f134,plain,(
% 46.78/6.36 ![Xx17]: (~nat_succeeds(Xx17)|~nat_fails(Xx17))),
% 46.78/6.36 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 46.78/6.36 fof(f135,plain,(
% 46.78/6.36 ![X0]: (~nat_succeeds(X0)|~nat_fails(X0))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f134])).
% 46.78/6.36 fof(f191,plain,(
% 46.78/6.36 ![Xx1,Xx2]: ((~'@=<_succeeds'(Xx1,Xx2)|((?[Xx3,Xx4]: ((Xx1=s(Xx3)&Xx2=s(Xx4))&'@=<_succeeds'(Xx3,Xx4)))|Xx1='0'))&('@=<_succeeds'(Xx1,Xx2)|((![Xx3,Xx4]: ((~Xx1=s(Xx3)|~Xx2=s(Xx4))|~'@=<_succeeds'(Xx3,Xx4)))&~Xx1='0')))),
% 46.78/6.36 inference(NNF_transformation,[status(thm)],[f21])).
% 46.78/6.36 fof(f192,plain,(
% 46.78/6.36 (![Xx1,Xx2]: (~'@=<_succeeds'(Xx1,Xx2)|((?[Xx3,Xx4]: ((Xx1=s(Xx3)&Xx2=s(Xx4))&'@=<_succeeds'(Xx3,Xx4)))|Xx1='0')))&(![Xx1,Xx2]: ('@=<_succeeds'(Xx1,Xx2)|((![Xx3,Xx4]: ((~Xx1=s(Xx3)|~Xx2=s(Xx4))|~'@=<_succeeds'(Xx3,Xx4)))&~Xx1='0')))),
% 46.78/6.36 inference(miniscoping,[status(thm)],[f191])).
% 46.78/6.36 fof(f193,plain,(
% 46.78/6.36 (![Xx1,Xx2]: (~'@=<_succeeds'(Xx1,Xx2)|(((Xx1=s(sK13_skl(Xx2,Xx1))&Xx2=s(sK14_skl(Xx2,Xx1)))&'@=<_succeeds'(sK13_skl(Xx2,Xx1),sK14_skl(Xx2,Xx1)))|Xx1='0')))&(![Xx1,Xx2]: ('@=<_succeeds'(Xx1,Xx2)|((![Xx3,Xx4]: ((~Xx1=s(Xx3)|~Xx2=s(Xx4))|~'@=<_succeeds'(Xx3,Xx4)))&~Xx1='0')))),
% 46.78/6.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(Xx3,sK13_skl(Xx2,Xx1)),skolemize(Xx4,sK14_skl(Xx2,Xx1))],[f192])).
% 46.78/6.36 fof(f197,plain,(
% 46.78/6.36 ![X0,X1,X2,X3]: ('@=<_succeeds'(X0,X1)|~X0=s(X2)|~X1=s(X3)|~'@=<_succeeds'(X2,X3))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f193])).
% 46.78/6.36 fof(f198,plain,(
% 46.78/6.36 ![X0,X1]: ('@=<_succeeds'(X0,X1)|~X0='0')),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f193])).
% 46.78/6.36 fof(f199,plain,(
% 46.78/6.36 ![Xx1,Xx2]: ((~'@=<_fails'(Xx1,Xx2)|((![Xx3,Xx4]: ((~Xx1=s(Xx3)|~Xx2=s(Xx4))|'@=<_fails'(Xx3,Xx4)))&~Xx1='0'))&('@=<_fails'(Xx1,Xx2)|((?[Xx3,Xx4]: ((Xx1=s(Xx3)&Xx2=s(Xx4))&~'@=<_fails'(Xx3,Xx4)))|Xx1='0')))),
% 46.78/6.36 inference(NNF_transformation,[status(thm)],[f22])).
% 46.78/6.36 fof(f200,plain,(
% 46.78/6.36 (![Xx1,Xx2]: (~'@=<_fails'(Xx1,Xx2)|((![Xx3,Xx4]: ((~Xx1=s(Xx3)|~Xx2=s(Xx4))|'@=<_fails'(Xx3,Xx4)))&~Xx1='0')))&(![Xx1,Xx2]: ('@=<_fails'(Xx1,Xx2)|((?[Xx3,Xx4]: ((Xx1=s(Xx3)&Xx2=s(Xx4))&~'@=<_fails'(Xx3,Xx4)))|Xx1='0')))),
% 46.78/6.36 inference(miniscoping,[status(thm)],[f199])).
% 46.78/6.36 fof(f201,plain,(
% 46.78/6.36 (![Xx1,Xx2]: (~'@=<_fails'(Xx1,Xx2)|((![Xx3,Xx4]: ((~Xx1=s(Xx3)|~Xx2=s(Xx4))|'@=<_fails'(Xx3,Xx4)))&~Xx1='0')))&(![Xx1,Xx2]: ('@=<_fails'(Xx1,Xx2)|(((Xx1=s(sK15_skl(Xx2,Xx1))&Xx2=s(sK16_skl(Xx2,Xx1)))&~'@=<_fails'(sK15_skl(Xx2,Xx1),sK16_skl(Xx2,Xx1)))|Xx1='0')))),
% 46.78/6.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(Xx3,sK15_skl(Xx2,Xx1)),skolemize(Xx4,sK16_skl(Xx2,Xx1))],[f200])).
% 46.78/6.36 fof(f203,plain,(
% 46.78/6.36 ![X0,X1]: (~'@=<_fails'(X0,X1)|~X0='0')),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f201])).
% 46.78/6.36 fof(f248,plain,(
% 46.78/6.36 ![Xx1]: ((~nat_fails(Xx1)|((![Xx2]: (~Xx1=s(Xx2)|nat_fails(Xx2)))&~Xx1='0'))&(nat_fails(Xx1)|((?[Xx2]: (Xx1=s(Xx2)&~nat_fails(Xx2)))|Xx1='0')))),
% 46.78/6.36 inference(NNF_transformation,[status(thm)],[f28])).
% 46.78/6.36 fof(f249,plain,(
% 46.78/6.36 (![Xx1]: (~nat_fails(Xx1)|((![Xx2]: (~Xx1=s(Xx2)|nat_fails(Xx2)))&~Xx1='0')))&(![Xx1]: (nat_fails(Xx1)|((?[Xx2]: (Xx1=s(Xx2)&~nat_fails(Xx2)))|Xx1='0')))),
% 46.78/6.36 inference(miniscoping,[status(thm)],[f248])).
% 46.78/6.36 fof(f250,plain,(
% 46.78/6.36 (![Xx1]: (~nat_fails(Xx1)|((![Xx2]: (~Xx1=s(Xx2)|nat_fails(Xx2)))&~Xx1='0')))&(![Xx1]: (nat_fails(Xx1)|((Xx1=s(sK28_skl(Xx1))&~nat_fails(sK28_skl(Xx1)))|Xx1='0')))),
% 46.78/6.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl]),skolemize(Xx2,sK28_skl(Xx1))],[f249])).
% 46.78/6.36 fof(f252,plain,(
% 46.78/6.36 ![X0]: (~nat_fails(X0)|~X0='0')),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f250])).
% 46.78/6.36 fof(f272,plain,(
% 46.78/6.36 ![Xx]: (~nat_succeeds(Xx)|nat_terminates(Xx))),
% 46.78/6.36 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 46.78/6.36 fof(f273,plain,(
% 46.78/6.36 ![X0]: (~nat_succeeds(X0)|nat_terminates(X0))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f272])).
% 46.78/6.36 fof(f274,plain,(
% 46.78/6.36 ![Xx]: (~nat_succeeds(Xx)|gr(Xx))),
% 46.78/6.36 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 46.78/6.36 fof(f275,plain,(
% 46.78/6.36 ![X0]: (~nat_succeeds(X0)|gr(X0))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f274])).
% 46.78/6.36 fof(f309,plain,(
% 46.78/6.36 ![X0]: ('@+'('0',X0)=X0)),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f45])).
% 46.78/6.36 fof(f310,plain,(
% 46.78/6.36 ![Xx,Xy]: (~nat_succeeds(Xx)|'@+'(s(Xx),Xy)=s('@+'(Xx,Xy)))),
% 46.78/6.36 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 46.78/6.36 fof(f311,plain,(
% 46.78/6.36 ![Xx]: (~nat_succeeds(Xx)|(![Xy]: '@+'(s(Xx),Xy)=s('@+'(Xx,Xy))))),
% 46.78/6.36 inference(miniscoping,[status(thm)],[f310])).
% 46.78/6.36 fof(f312,plain,(
% 46.78/6.36 ![X0,X1]: (~nat_succeeds(X0)|'@+'(s(X0),X1)=s('@+'(X0,X1)))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f311])).
% 46.78/6.36 fof(f375,plain,(
% 46.78/6.36 ![Xx,Xy]: (~'@<_succeeds'(Xx,Xy)|nat_succeeds(Xx))),
% 46.78/6.36 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 46.78/6.36 fof(f376,plain,(
% 46.78/6.36 ![Xx]: ((![Xy]: ~'@<_succeeds'(Xx,Xy))|nat_succeeds(Xx))),
% 46.78/6.36 inference(miniscoping,[status(thm)],[f375])).
% 46.78/6.36 fof(f377,plain,(
% 46.78/6.36 ![X0,X1]: (~'@<_succeeds'(X0,X1)|nat_succeeds(X0))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f376])).
% 46.78/6.36 fof(f378,plain,(
% 46.78/6.36 ![Xx,Xy]: (~'@<_succeeds'(Xx,Xy)|(?[Xz]: Xy=s(Xz)))),
% 46.78/6.36 inference(pre_NNF_transformation,[status(thm)],[f74])).
% 46.78/6.36 fof(f379,plain,(
% 46.78/6.36 ![Xy]: ((![Xx]: ~'@<_succeeds'(Xx,Xy))|(?[Xz]: Xy=s(Xz)))),
% 46.78/6.36 inference(miniscoping,[status(thm)],[f378])).
% 46.78/6.36 fof(f380,plain,(
% 46.78/6.36 ![Xy]: ((![Xx]: ~'@<_succeeds'(Xx,Xy))|Xy=s(sK32_skl(Xy)))),
% 46.78/6.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK32_skl]),skolemize(Xz,sK32_skl(Xy))],[f379])).
% 46.78/6.36 fof(f381,plain,(
% 46.78/6.36 ![X0,X1]: (~'@<_succeeds'(X0,X1)|X1=s(sK32_skl(X1)))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f380])).
% 46.78/6.36 fof(f392,plain,(
% 46.78/6.36 ![Xx]: (~nat_succeeds(Xx)|~'@<_succeeds'(Xx,Xx))),
% 46.78/6.36 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 46.78/6.36 fof(f393,plain,(
% 46.78/6.36 ![X0]: (~nat_succeeds(X0)|~'@<_succeeds'(X0,X0))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f392])).
% 46.78/6.36 fof(f408,plain,(
% 46.78/6.36 ![Xx,Xy]: (~'@=<_succeeds'(Xx,Xy)|nat_succeeds(Xx))),
% 46.78/6.36 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 46.78/6.36 fof(f409,plain,(
% 46.78/6.36 ![Xx]: ((![Xy]: ~'@=<_succeeds'(Xx,Xy))|nat_succeeds(Xx))),
% 46.78/6.36 inference(miniscoping,[status(thm)],[f408])).
% 46.78/6.36 fof(f410,plain,(
% 46.78/6.36 ![X0,X1]: (~'@=<_succeeds'(X0,X1)|nat_succeeds(X0))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f409])).
% 46.78/6.36 fof(f435,plain,(
% 46.78/6.36 ![Xx,Xy,Xz]: ((~'@=<_succeeds'(Xx,Xy)|~'@<_succeeds'(Xy,Xz))|'@<_succeeds'(Xx,Xz))),
% 46.78/6.36 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 46.78/6.36 fof(f436,plain,(
% 46.78/6.36 ![Xx,Xz]: ((![Xy]: (~'@=<_succeeds'(Xx,Xy)|~'@<_succeeds'(Xy,Xz)))|'@<_succeeds'(Xx,Xz))),
% 46.78/6.36 inference(miniscoping,[status(thm)],[f435])).
% 46.78/6.36 fof(f437,plain,(
% 46.78/6.36 ![X0,X1,X2]: (~'@=<_succeeds'(X0,X1)|~'@<_succeeds'(X1,X2)|'@<_succeeds'(X0,X2))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f436])).
% 46.78/6.36 fof(f459,plain,(
% 46.78/6.36 (?[Xx]: (((?[Xx2]: ((Xx=s(Xx2)&nat_succeeds(Xx2))&(![Xy,Xz]: (~'@=<_succeeds'(Xy,Xz)|'@=<_succeeds'('@+'(Xx2,Xy),'@+'(Xx2,Xz))))))|Xx='0')&(?[Xy,Xz]: ('@=<_succeeds'(Xy,Xz)&~'@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz))))))|(![Xx]: (~nat_succeeds(Xx)|(![Xy,Xz]: (~'@=<_succeeds'(Xy,Xz)|'@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz))))))),
% 46.78/6.36 inference(pre_NNF_transformation,[status(thm)],[f107])).
% 46.78/6.36 fof(f460,plain,(
% 46.78/6.36 ((((sK37_skl=s(sK38_skl)&nat_succeeds(sK38_skl))&(![Xy,Xz]: (~'@=<_succeeds'(Xy,Xz)|'@=<_succeeds'('@+'(sK38_skl,Xy),'@+'(sK38_skl,Xz)))))|sK37_skl='0')&('@=<_succeeds'(sK39_skl,sK40_skl)&~'@=<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl))))|(![Xx]: (~nat_succeeds(Xx)|(![Xy,Xz]: (~'@=<_succeeds'(Xy,Xz)|'@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz))))))),
% 46.78/6.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK37_skl,sK38_skl,sK39_skl,sK40_skl]),skolemize(Xx,sK37_skl),skolemize(Xx2,sK38_skl),skolemize(Xy,sK39_skl),skolemize(Xz,sK40_skl)],[f459])).
% 46.78/6.36 fof(f461,plain,(
% 46.78/6.36 ![X0,X1,X2]: (sK37_skl=s(sK38_skl)|sK37_skl='0'|~nat_succeeds(X0)|~'@=<_succeeds'(X1,X2)|'@=<_succeeds'('@+'(X0,X1),'@+'(X0,X2)))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f460])).
% 46.78/6.36 fof(f462,plain,(
% 46.78/6.36 ![X0,X1,X2]: (nat_succeeds(sK38_skl)|sK37_skl='0'|~nat_succeeds(X0)|~'@=<_succeeds'(X1,X2)|'@=<_succeeds'('@+'(X0,X1),'@+'(X0,X2)))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f460])).
% 46.78/6.36 fof(f463,plain,(
% 46.78/6.36 ![X0,X1,X2,X3,X4]: (~'@=<_succeeds'(X0,X1)|'@=<_succeeds'('@+'(sK38_skl,X0),'@+'(sK38_skl,X1))|sK37_skl='0'|~nat_succeeds(X2)|~'@=<_succeeds'(X3,X4)|'@=<_succeeds'('@+'(X2,X3),'@+'(X2,X4)))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f460])).
% 46.78/6.36 fof(f464,plain,(
% 46.78/6.36 ![X0,X1,X2]: ('@=<_succeeds'(sK39_skl,sK40_skl)|~nat_succeeds(X0)|~'@=<_succeeds'(X1,X2)|'@=<_succeeds'('@+'(X0,X1),'@+'(X0,X2)))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f460])).
% 46.78/6.36 fof(f465,plain,(
% 46.78/6.36 ![X0,X1,X2]: (~'@=<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl))|~nat_succeeds(X0)|~'@=<_succeeds'(X1,X2)|'@=<_succeeds'('@+'(X0,X1),'@+'(X0,X2)))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f460])).
% 46.78/6.36 fof(f466,plain,(
% 46.78/6.36 (?[Xx,Xy,Xz]: ((nat_succeeds(Xx)&'@=<_succeeds'(Xy,Xz))&~'@=<_succeeds'('@+'(Xx,Xy),'@+'(Xx,Xz))))),
% 46.78/6.36 inference(pre_NNF_transformation,[status(thm)],[f109])).
% 46.78/6.36 fof(f467,plain,(
% 46.78/6.36 ((nat_succeeds(sK41_skl)&'@=<_succeeds'(sK42_skl,sK43_skl))&~'@=<_succeeds'('@+'(sK41_skl,sK42_skl),'@+'(sK41_skl,sK43_skl)))),
% 46.78/6.36 inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl,sK42_skl,sK43_skl]),skolemize(Xx,sK41_skl),skolemize(Xy,sK42_skl),skolemize(Xz,sK43_skl)],[f466])).
% 46.78/6.36 fof(f468,plain,(
% 46.78/6.36 nat_succeeds(sK41_skl)),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f467])).
% 46.78/6.36 fof(f469,plain,(
% 46.78/6.36 '@=<_succeeds'(sK42_skl,sK43_skl)),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f467])).
% 46.78/6.36 fof(f470,plain,(
% 46.78/6.36 ~'@=<_succeeds'('@+'(sK41_skl,sK42_skl),'@+'(sK41_skl,sK43_skl))),
% 46.78/6.36 inference(cnf_transformation,[status(thm)],[f467])).
% 46.78/6.36 fof(f507,definition,(
% 46.78/6.36 sQ0_spl <=> (sK37_skl=s(sK38_skl))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f508,plain,(
% 46.78/6.36 sK37_skl=s(sK38_skl)|~sQ0_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f507])).
% 46.78/6.36 fof(f510,definition,(
% 46.78/6.36 sQ1_spl <=> (sK37_skl='0')),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f511,plain,(
% 46.78/6.36 sK37_skl='0'|~sQ1_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f510])).
% 46.78/6.36 fof(f513,definition,(
% 46.78/6.36 ![X0,X1,X2]: (sQ2_spl <=> (~nat_succeeds(X0)|~'@=<_succeeds'(X1,X2)|'@=<_succeeds'('@+'(X0,X1),'@+'(X0,X2))))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f514,plain,(
% 46.78/6.36 ![X0,X1,X2]: (~nat_succeeds(X0)|~'@=<_succeeds'(X1,X2)|'@=<_succeeds'('@+'(X0,X1),'@+'(X0,X2))|~sQ2_spl)),
% 46.78/6.36 inference(component_clause,[status(thm)],[f513])).
% 46.78/6.36 fof(f516,plain,(
% 46.78/6.36 sQ0_spl|sQ1_spl|sQ2_spl),
% 46.78/6.36 inference(split_clause,[status(thm)],[f461,f507,f510,f513])).
% 46.78/6.36 fof(f517,definition,(
% 46.78/6.36 sQ3_spl <=> (nat_succeeds(sK38_skl))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f518,plain,(
% 46.78/6.36 nat_succeeds(sK38_skl)|~sQ3_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f517])).
% 46.78/6.36 fof(f520,plain,(
% 46.78/6.36 sQ3_spl|sQ1_spl|sQ2_spl),
% 46.78/6.36 inference(split_clause,[status(thm)],[f462,f517,f510,f513])).
% 46.78/6.36 fof(f521,definition,(
% 46.78/6.36 ![X0,X1]: (sQ4_spl <=> (~'@=<_succeeds'(X0,X1)|'@=<_succeeds'('@+'(sK38_skl,X0),'@+'(sK38_skl,X1))))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f522,plain,(
% 46.78/6.36 ![X0,X1]: (~'@=<_succeeds'(X0,X1)|'@=<_succeeds'('@+'(sK38_skl,X0),'@+'(sK38_skl,X1))|~sQ4_spl)),
% 46.78/6.36 inference(component_clause,[status(thm)],[f521])).
% 46.78/6.36 fof(f524,plain,(
% 46.78/6.36 sQ4_spl|sQ1_spl|sQ2_spl),
% 46.78/6.36 inference(split_clause,[status(thm)],[f463,f521,f510,f513])).
% 46.78/6.36 fof(f525,definition,(
% 46.78/6.36 sQ5_spl <=> ('@=<_succeeds'(sK39_skl,sK40_skl))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f526,plain,(
% 46.78/6.36 '@=<_succeeds'(sK39_skl,sK40_skl)|~sQ5_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f525])).
% 46.78/6.36 fof(f528,plain,(
% 46.78/6.36 sQ5_spl|sQ2_spl),
% 46.78/6.36 inference(split_clause,[status(thm)],[f464,f525,f513])).
% 46.78/6.36 fof(f529,definition,(
% 46.78/6.36 sQ6_spl <=> ('@=<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl)))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f531,plain,(
% 46.78/6.36 ~'@=<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl))|sQ6_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f529])).
% 46.78/6.36 fof(f532,plain,(
% 46.78/6.36 ~sQ6_spl|sQ2_spl),
% 46.78/6.36 inference(split_clause,[status(thm)],[f465,f529,f513])).
% 46.78/6.36 fof(f540,plain,(
% 46.78/6.36 ![X0,X1]: ('@=<_succeeds'(s(X0),s(X1))|~'@=<_succeeds'(X0,X1))),
% 46.78/6.36 inference(destructive_equality_resolution,[status(thm)],[f197])).
% 46.78/6.36 fof(f541,plain,(
% 46.78/6.36 ![X0]: ('@=<_succeeds'('0',X0))),
% 46.78/6.36 inference(destructive_equality_resolution,[status(thm)],[f198])).
% 46.78/6.36 fof(f543,plain,(
% 46.78/6.36 ![X0]: (~'@=<_fails'('0',X0))),
% 46.78/6.36 inference(destructive_equality_resolution,[status(thm)],[f203])).
% 46.78/6.36 fof(f551,plain,(
% 46.78/6.36 ~nat_fails('0')),
% 46.78/6.36 inference(destructive_equality_resolution,[status(thm)],[f252])).
% 46.78/6.36 fof(f562,plain,(
% 46.78/6.36 nat_succeeds(sK42_skl)),
% 46.78/6.36 inference(resolution,[status(thm)],[f410,f469])).
% 46.78/6.36 fof(f600,plain,(
% 46.78/6.36 nat_terminates(sK41_skl)),
% 46.78/6.36 inference(resolution,[status(thm)],[f273,f468])).
% 46.78/6.36 fof(f620,plain,(
% 46.78/6.36 gr(sK41_skl)),
% 46.78/6.36 inference(resolution,[status(thm)],[f275,f468])).
% 46.78/6.36 fof(f682,definition,(
% 46.78/6.36 sQ16_spl <=> (nat_fails('0'))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f683,plain,(
% 46.78/6.36 nat_fails('0')|~sQ16_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f682])).
% 46.78/6.36 fof(f703,definition,(
% 46.78/6.36 sQ22_spl <=> (nat_fails(sK42_skl))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f704,plain,(
% 46.78/6.36 nat_fails(sK42_skl)|~sQ22_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f703])).
% 46.78/6.36 fof(f1852,definition,(
% 46.78/6.36 sQ84_spl <=> (nat_terminates(sK41_skl))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f1854,plain,(
% 46.78/6.36 ~nat_terminates(sK41_skl)|sQ84_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f1852])).
% 46.78/6.36 fof(f1857,definition,(
% 46.78/6.36 sQ85_spl <=> (gr(sK41_skl))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f1859,plain,(
% 46.78/6.36 ~gr(sK41_skl)|sQ85_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f1857])).
% 46.78/6.36 fof(f1880,plain,(
% 46.78/6.36 ![X0]: (~'@<_succeeds'(X0,X0))),
% 46.78/6.36 inference(forward_subsumption_resolution,[status(thm)],[f393,f377])).
% 46.78/6.36 fof(f1914,definition,(
% 46.78/6.36 sQ90_spl <=> ('@<_succeeds'('0','0'))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f1915,plain,(
% 46.78/6.36 '@<_succeeds'('0','0')|~sQ90_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f1914])).
% 46.78/6.36 fof(f2539,plain,(
% 46.78/6.36 nat_terminates(sK42_skl)),
% 46.78/6.36 inference(resolution,[status(thm)],[f562,f273])).
% 46.78/6.36 fof(f2569,plain,(
% 46.78/6.36 ![X0,X1]: (~'@=<_succeeds'(X0,X1)|'@=<_succeeds'('@+'(sK41_skl,X0),'@+'(sK41_skl,X1))|~sQ2_spl)),
% 46.78/6.36 inference(resolution,[status(thm)],[f514,f468])).
% 46.78/6.36 fof(f2670,definition,(
% 46.78/6.36 sQ108_spl <=> ('@<_succeeds'(sK41_skl,'0'))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f2671,plain,(
% 46.78/6.36 '@<_succeeds'(sK41_skl,'0')|~sQ108_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f2670])).
% 46.78/6.36 fof(f2734,definition,(
% 46.78/6.36 ![X0]: (sQ112_spl <=> ('0'=s(sK15_skl(X0,'0'))))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f2735,plain,(
% 46.78/6.36 ![X0]: ('0'=s(sK15_skl(X0,'0'))|~sQ112_spl)),
% 46.78/6.36 inference(component_clause,[status(thm)],[f2734])).
% 46.78/6.36 fof(f2867,definition,(
% 46.78/6.36 sQ129_spl <=> ('0'=s(sK28_skl('0')))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f2868,plain,(
% 46.78/6.36 '0'=s(sK28_skl('0'))|~sQ129_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f2867])).
% 46.78/6.36 fof(f2914,definition,(
% 46.78/6.36 sQ132_spl <=> ('0'=s(sK27_skl('0')))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f2915,plain,(
% 46.78/6.36 '0'=s(sK27_skl('0'))|~sQ132_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f2914])).
% 46.78/6.36 fof(f3021,definition,(
% 46.78/6.36 sQ135_spl <=> ('@<_succeeds'(sK42_skl,sK42_skl))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f3022,plain,(
% 46.78/6.36 '@<_succeeds'(sK42_skl,sK42_skl)|~sQ135_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f3021])).
% 46.78/6.36 fof(f3524,plain,(
% 46.78/6.36 nat_succeeds(sK42_skl)),
% 46.78/6.36 inference(resolution,[status(thm)],[f469,f410])).
% 46.78/6.36 fof(f4041,plain,(
% 46.78/6.36 '@=<_succeeds'('@+'(sK41_skl,sK42_skl),'@+'(sK41_skl,sK43_skl))|~sQ2_spl),
% 46.78/6.36 inference(resolution,[status(thm)],[f2569,f469])).
% 46.78/6.36 fof(f4047,plain,(
% 46.78/6.36 $false|~sQ2_spl),
% 46.78/6.36 inference(forward_subsumption_resolution,[status(thm)],[f4041,f470])).
% 46.78/6.36 fof(f4048,plain,(
% 46.78/6.36 ~sQ2_spl),
% 46.78/6.36 inference(contradiction_clause,[status(thm)],[f4047])).
% 46.78/6.36 fof(f4071,definition,(
% 46.78/6.36 sQ162_spl <=> (s(sK42_skl)='0')),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f4072,plain,(
% 46.78/6.36 s(sK42_skl)='0'|~sQ162_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f4071])).
% 46.78/6.36 fof(f4086,definition,(
% 46.78/6.36 ![X0]: (sQ163_spl <=> (X0=s(sK14_skl(X0,sK37_skl))))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f4087,plain,(
% 46.78/6.36 ![X0]: (X0=s(sK14_skl(X0,sK37_skl))|~sQ163_spl)),
% 46.78/6.36 inference(component_clause,[status(thm)],[f4086])).
% 46.78/6.36 fof(f4099,plain,(
% 46.78/6.36 $false|~sQ162_spl),
% 46.78/6.36 inference(forward_subsumption_resolution,[status(thm)],[f4072,f110])).
% 46.78/6.36 fof(f4100,plain,(
% 46.78/6.36 ~sQ162_spl),
% 46.78/6.36 inference(contradiction_clause,[status(thm)],[f4099])).
% 46.78/6.36 fof(f4200,plain,(
% 46.78/6.36 ![X0]: ('@+'(s(sK38_skl),X0)=s('@+'(sK38_skl,X0))|~sQ3_spl)),
% 46.78/6.36 inference(resolution,[status(thm)],[f518,f312])).
% 46.78/6.36 fof(f4926,plain,(
% 46.78/6.36 ~nat_succeeds(sK42_skl)|~sQ22_spl),
% 46.78/6.36 inference(resolution,[status(thm)],[f704,f135])).
% 46.78/6.36 fof(f4927,plain,(
% 46.78/6.36 $false|~sQ22_spl),
% 46.78/6.36 inference(forward_subsumption_resolution,[status(thm)],[f4926,f3524])).
% 46.78/6.36 fof(f4928,plain,(
% 46.78/6.36 ~sQ22_spl),
% 46.78/6.36 inference(contradiction_clause,[status(thm)],[f4927])).
% 46.78/6.36 fof(f4935,plain,(
% 46.78/6.36 ![X0,X1]: (~'@<_succeeds'(X0,X1)|'@<_succeeds'('0',X1))),
% 46.78/6.36 inference(resolution,[status(thm)],[f541,f437])).
% 46.78/6.36 fof(f5018,plain,(
% 46.78/6.36 $false|~sQ135_spl),
% 46.78/6.36 inference(forward_subsumption_resolution,[status(thm)],[f3022,f1880])).
% 46.78/6.36 fof(f5019,plain,(
% 46.78/6.36 ~sQ135_spl),
% 46.78/6.36 inference(contradiction_clause,[status(thm)],[f5018])).
% 46.78/6.36 fof(f5389,definition,(
% 46.78/6.36 sQ222_spl <=> ('@<_succeeds'(sK39_skl,sK39_skl))),
% 46.78/6.36 introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition])).
% 46.78/6.36 fof(f5390,plain,(
% 46.78/6.36 '@<_succeeds'(sK39_skl,sK39_skl)|~sQ222_spl),
% 46.78/6.36 inference(component_clause,[status(thm)],[f5389])).
% 46.78/6.36 fof(f5400,plain,(
% 46.78/6.36 $false|~sQ222_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f5390,f1880])).
% 46.78/6.37 fof(f5401,plain,(
% 46.78/6.37 ~sQ222_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f5400])).
% 46.78/6.37 fof(f6088,definition,(
% 46.78/6.37 ![X0]: (sQ248_spl <=> (X0=s(sK16_skl(X0,sK39_skl))))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f6089,plain,(
% 46.78/6.37 ![X0]: (X0=s(sK16_skl(X0,sK39_skl))|~sQ248_spl)),
% 46.78/6.37 inference(component_clause,[status(thm)],[f6088])).
% 46.78/6.37 fof(f6122,definition,(
% 46.78/6.37 sQ251_spl <=> (gr(sK42_skl))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ251_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f6124,plain,(
% 46.78/6.37 ~gr(sK42_skl)|sQ251_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f6122])).
% 46.78/6.37 fof(f8014,plain,(
% 46.78/6.37 ![X0]: ('@+'(sK37_skl,X0)=X0|~sQ1_spl)),
% 46.78/6.37 inference(backward_demodulation,[status(thm)],[f511,f309])).
% 46.78/6.37 fof(f8077,definition,(
% 46.78/6.37 sQ270_spl <=> ('@<_succeeds'(sK37_skl,sK37_skl))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f8078,plain,(
% 46.78/6.37 '@<_succeeds'(sK37_skl,sK37_skl)|~sQ270_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f8077])).
% 46.78/6.37 fof(f8082,plain,(
% 46.78/6.37 $false|~sQ270_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f8078,f1880])).
% 46.78/6.37 fof(f8083,plain,(
% 46.78/6.37 ~sQ270_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f8082])).
% 46.78/6.37 fof(f8528,definition,(
% 46.78/6.37 sQ278_spl <=> ('@<_succeeds'(sK38_skl,sK38_skl))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ278_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f8529,plain,(
% 46.78/6.37 '@<_succeeds'(sK38_skl,sK38_skl)|~sQ278_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f8528])).
% 46.78/6.37 fof(f8541,plain,(
% 46.78/6.37 $false|~sQ278_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f8529,f1880])).
% 46.78/6.37 fof(f8542,plain,(
% 46.78/6.37 ~sQ278_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f8541])).
% 46.78/6.37 fof(f8778,definition,(
% 46.78/6.37 ![X0]: (sQ283_spl <=> (X0=s(sK16_skl(X0,sK38_skl))))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f8779,plain,(
% 46.78/6.37 ![X0]: (X0=s(sK16_skl(X0,sK38_skl))|~sQ283_spl)),
% 46.78/6.37 inference(component_clause,[status(thm)],[f8778])).
% 46.78/6.37 fof(f9670,plain,(
% 46.78/6.37 $false|sQ84_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f1854,f600])).
% 46.78/6.37 fof(f9671,plain,(
% 46.78/6.37 sQ84_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f9670])).
% 46.78/6.37 fof(f10641,plain,(
% 46.78/6.37 $false|sQ85_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f1859,f620])).
% 46.78/6.37 fof(f10642,plain,(
% 46.78/6.37 sQ85_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f10641])).
% 46.78/6.37 fof(f10673,plain,(
% 46.78/6.37 '@=<_succeeds'('@+'(sK38_skl,sK39_skl),'@+'(sK38_skl,sK40_skl))|~sQ4_spl|~sQ5_spl),
% 46.78/6.37 inference(resolution,[status(thm)],[f522,f526])).
% 46.78/6.37 fof(f10686,definition,(
% 46.78/6.37 sQ368_spl <=> ('0'=s(sK29_skl('0')))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ368_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f10687,plain,(
% 46.78/6.37 '0'=s(sK29_skl('0'))|~sQ368_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f10686])).
% 46.78/6.37 fof(f11480,definition,(
% 46.78/6.37 ![X0]: (sQ411_spl <=> ('0'=s(sK22_skl(s(X0),'0'))))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ411_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f11481,plain,(
% 46.78/6.37 ![X0]: ('0'=s(sK22_skl(s(X0),'0'))|~sQ411_spl)),
% 46.78/6.37 inference(component_clause,[status(thm)],[f11480])).
% 46.78/6.37 fof(f11484,plain,(
% 46.78/6.37 $false|~sQ411_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f11481,f110])).
% 46.78/6.37 fof(f11485,plain,(
% 46.78/6.37 ~sQ411_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f11484])).
% 46.78/6.37 fof(f11624,definition,(
% 46.78/6.37 sQ415_spl <=> (s(sK39_skl)='0')),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ415_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f11625,plain,(
% 46.78/6.37 s(sK39_skl)='0'|~sQ415_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f11624])).
% 46.78/6.37 fof(f11636,plain,(
% 46.78/6.37 $false|~sQ415_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f11625,f110])).
% 46.78/6.37 fof(f11637,plain,(
% 46.78/6.37 ~sQ415_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f11636])).
% 46.78/6.37 fof(f11839,definition,(
% 46.78/6.37 sQ428_spl <=> (nat_terminates(sK42_skl))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f11841,plain,(
% 46.78/6.37 ~nat_terminates(sK42_skl)|sQ428_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f11839])).
% 46.78/6.37 fof(f11898,plain,(
% 46.78/6.37 '@<_succeeds'('0','0')|~sQ108_spl),
% 46.78/6.37 inference(resolution,[status(thm)],[f2671,f4935])).
% 46.78/6.37 fof(f11915,plain,(
% 46.78/6.37 $false|~sQ108_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f11898,f1880])).
% 46.78/6.37 fof(f11916,plain,(
% 46.78/6.37 ~sQ108_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f11915])).
% 46.78/6.37 fof(f12248,definition,(
% 46.78/6.37 ![X0]: (sQ440_spl <=> ('0'=s(sK2_skl('0',X0,'0'))))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ440_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f12249,plain,(
% 46.78/6.37 ![X0]: ('0'=s(sK2_skl('0',X0,'0'))|~sQ440_spl)),
% 46.78/6.37 inference(component_clause,[status(thm)],[f12248])).
% 46.78/6.37 fof(f12252,plain,(
% 46.78/6.37 $false|~sQ440_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f12249,f110])).
% 46.78/6.37 fof(f12253,plain,(
% 46.78/6.37 ~sQ440_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f12252])).
% 46.78/6.37 fof(f12276,definition,(
% 46.78/6.37 ![X0]: (sQ442_spl <=> ('0'=s(sK9_skl(X0,X0,'0'))))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ442_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f12277,plain,(
% 46.78/6.37 ![X0]: ('0'=s(sK9_skl(X0,X0,'0'))|~sQ442_spl)),
% 46.78/6.37 inference(component_clause,[status(thm)],[f12276])).
% 46.78/6.37 fof(f12280,plain,(
% 46.78/6.37 $false|~sQ442_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f12277,f110])).
% 46.78/6.37 fof(f12281,plain,(
% 46.78/6.37 ~sQ442_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f12280])).
% 46.78/6.37 fof(f12975,plain,(
% 46.78/6.37 gr(sK42_skl)),
% 46.78/6.37 inference(resolution,[status(thm)],[f3524,f275])).
% 46.78/6.37 fof(f15397,plain,(
% 46.78/6.37 $false|~sQ248_spl),
% 46.78/6.37 inference(resolution,[status(thm)],[f6089,f110])).
% 46.78/6.37 fof(f15439,plain,(
% 46.78/6.37 ~sQ248_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f15397])).
% 46.78/6.37 fof(f15442,plain,(
% 46.78/6.37 $false|~sQ163_spl),
% 46.78/6.37 inference(resolution,[status(thm)],[f4087,f110])).
% 46.78/6.37 fof(f15484,plain,(
% 46.78/6.37 ~sQ163_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f15442])).
% 46.78/6.37 fof(f15902,plain,(
% 46.78/6.37 $false|sQ251_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f6124,f12975])).
% 46.78/6.37 fof(f15903,plain,(
% 46.78/6.37 sQ251_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f15902])).
% 46.78/6.37 fof(f15904,plain,(
% 46.78/6.37 $false|sQ428_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f11841,f2539])).
% 46.78/6.37 fof(f15905,plain,(
% 46.78/6.37 sQ428_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f15904])).
% 46.78/6.37 fof(f16573,plain,(
% 46.78/6.37 ![X0]: ('@+'(sK37_skl,X0)=s('@+'(sK38_skl,X0))|~sQ0_spl|~sQ3_spl)),
% 46.78/6.37 inference(forward_demodulation,[status(thm)],[f508,f4200])).
% 46.78/6.37 fof(f17094,plain,(
% 46.78/6.37 $false|~sQ368_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f10687,f110])).
% 46.78/6.37 fof(f17095,plain,(
% 46.78/6.37 ~sQ368_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f17094])).
% 46.78/6.37 fof(f17813,plain,(
% 46.78/6.37 $false|~sQ283_spl),
% 46.78/6.37 inference(resolution,[status(thm)],[f8779,f110])).
% 46.78/6.37 fof(f17856,plain,(
% 46.78/6.37 ~sQ283_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f17813])).
% 46.78/6.37 fof(f18127,definition,(
% 46.78/6.37 sQ771_spl <=> ('0'=s(sK22_skl(sK37_skl,'0')))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ771_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f18128,plain,(
% 46.78/6.37 '0'=s(sK22_skl(sK37_skl,'0'))|~sQ771_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f18127])).
% 46.78/6.37 fof(f18144,definition,(
% 46.78/6.37 sQ775_spl <=> ('0'=s(sK25_skl(sK37_skl,'0')))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ775_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f18145,plain,(
% 46.78/6.37 '0'=s(sK25_skl(sK37_skl,'0'))|~sQ775_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f18144])).
% 46.78/6.37 fof(f18148,plain,(
% 46.78/6.37 $false|~sQ771_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f18128,f110])).
% 46.78/6.37 fof(f18149,plain,(
% 46.78/6.37 ~sQ771_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f18148])).
% 46.78/6.37 fof(f18150,plain,(
% 46.78/6.37 $false|~sQ775_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f18145,f110])).
% 46.78/6.37 fof(f18151,plain,(
% 46.78/6.37 ~sQ775_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f18150])).
% 46.78/6.37 fof(f18934,definition,(
% 46.78/6.37 sQ841_spl <=> ('0'=s(sK22_skl(sK41_skl,'0')))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ841_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f18935,plain,(
% 46.78/6.37 '0'=s(sK22_skl(sK41_skl,'0'))|~sQ841_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f18934])).
% 46.78/6.37 fof(f18951,definition,(
% 46.78/6.37 sQ845_spl <=> ('0'=s(sK25_skl(sK41_skl,'0')))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ845_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f18952,plain,(
% 46.78/6.37 '0'=s(sK25_skl(sK41_skl,'0'))|~sQ845_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f18951])).
% 46.78/6.37 fof(f18955,plain,(
% 46.78/6.37 $false|~sQ841_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f18935,f110])).
% 46.78/6.37 fof(f18956,plain,(
% 46.78/6.37 ~sQ841_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f18955])).
% 46.78/6.37 fof(f18957,plain,(
% 46.78/6.37 $false|~sQ845_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f18952,f110])).
% 46.78/6.37 fof(f18958,plain,(
% 46.78/6.37 ~sQ845_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f18957])).
% 46.78/6.37 fof(f19630,definition,(
% 46.78/6.37 sQ900_spl <=> ('@=<_fails'('0',sK38_skl))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ900_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f19631,plain,(
% 46.78/6.37 '@=<_fails'('0',sK38_skl)|~sQ900_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f19630])).
% 46.78/6.37 fof(f19681,plain,(
% 46.78/6.37 $false|~sQ90_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f1915,f1880])).
% 46.78/6.37 fof(f19682,plain,(
% 46.78/6.37 ~sQ90_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f19681])).
% 46.78/6.37 fof(f19683,plain,(
% 46.78/6.37 $false|~sQ900_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f19631,f543])).
% 46.78/6.37 fof(f19684,plain,(
% 46.78/6.37 ~sQ900_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f19683])).
% 46.78/6.37 fof(f20210,definition,(
% 46.78/6.37 sQ951_spl <=> ('0'=s(sK22_skl(sK39_skl,'0')))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ951_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f20211,plain,(
% 46.78/6.37 '0'=s(sK22_skl(sK39_skl,'0'))|~sQ951_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f20210])).
% 46.78/6.37 fof(f20227,definition,(
% 46.78/6.37 sQ955_spl <=> ('0'=s(sK25_skl(sK39_skl,'0')))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ955_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f20228,plain,(
% 46.78/6.37 '0'=s(sK25_skl(sK39_skl,'0'))|~sQ955_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f20227])).
% 46.78/6.37 fof(f20231,plain,(
% 46.78/6.37 $false|~sQ951_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f20211,f110])).
% 46.78/6.37 fof(f20232,plain,(
% 46.78/6.37 ~sQ951_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f20231])).
% 46.78/6.37 fof(f20233,plain,(
% 46.78/6.37 $false|~sQ955_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f20228,f110])).
% 46.78/6.37 fof(f20234,plain,(
% 46.78/6.37 ~sQ955_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f20233])).
% 46.78/6.37 fof(f20286,definition,(
% 46.78/6.37 sQ956_spl <=> ('0'=s(sK22_skl(sK40_skl,'0')))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ956_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f20287,plain,(
% 46.78/6.37 '0'=s(sK22_skl(sK40_skl,'0'))|~sQ956_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f20286])).
% 46.78/6.37 fof(f20303,definition,(
% 46.78/6.37 sQ960_spl <=> ('0'=s(sK25_skl(sK40_skl,'0')))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ960_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f20304,plain,(
% 46.78/6.37 '0'=s(sK25_skl(sK40_skl,'0'))|~sQ960_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f20303])).
% 46.78/6.37 fof(f20307,plain,(
% 46.78/6.37 $false|~sQ956_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f20287,f110])).
% 46.78/6.37 fof(f20308,plain,(
% 46.78/6.37 ~sQ956_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f20307])).
% 46.78/6.37 fof(f20309,plain,(
% 46.78/6.37 $false|~sQ960_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f20304,f110])).
% 46.78/6.37 fof(f20310,plain,(
% 46.78/6.37 ~sQ960_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f20309])).
% 46.78/6.37 fof(f20349,plain,(
% 46.78/6.37 $false|~sQ132_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f2915,f110])).
% 46.78/6.37 fof(f20350,plain,(
% 46.78/6.37 ~sQ132_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f20349])).
% 46.78/6.37 fof(f20351,plain,(
% 46.78/6.37 $false|~sQ129_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f2868,f110])).
% 46.78/6.37 fof(f20352,plain,(
% 46.78/6.37 ~sQ129_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f20351])).
% 46.78/6.37 fof(f20353,plain,(
% 46.78/6.37 $false|~sQ112_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f2735,f110])).
% 46.78/6.37 fof(f20354,plain,(
% 46.78/6.37 ~sQ112_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f20353])).
% 46.78/6.37 fof(f20356,plain,(
% 46.78/6.37 $false|~sQ16_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f683,f551])).
% 46.78/6.37 fof(f20357,plain,(
% 46.78/6.37 ~sQ16_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f20356])).
% 46.78/6.37 fof(f20796,plain,(
% 46.78/6.37 ~'@=<_succeeds'('@+'(sK37_skl,sK39_skl),sK40_skl)|~sQ1_spl|sQ6_spl),
% 46.78/6.37 inference(backward_demodulation,[status(thm)],[f8014,f531])).
% 46.78/6.37 fof(f20797,plain,(
% 46.78/6.37 ~'@=<_succeeds'(sK39_skl,sK40_skl)|~sQ1_spl|sQ6_spl),
% 46.78/6.37 inference(forward_demodulation,[status(thm)],[f8014,f20796])).
% 46.78/6.37 fof(f20798,plain,(
% 46.78/6.37 $false|~sQ5_spl|~sQ1_spl|sQ6_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f20797,f526])).
% 46.78/6.37 fof(f20799,plain,(
% 46.78/6.37 ~sQ5_spl|~sQ1_spl|sQ6_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f20798])).
% 46.78/6.37 fof(f21981,definition,(
% 46.78/6.37 sQ989_spl <=> ('0'=s(sK37_skl))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ989_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f21982,plain,(
% 46.78/6.37 '0'=s(sK37_skl)|~sQ989_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f21981])).
% 46.78/6.37 fof(f22000,plain,(
% 46.78/6.37 $false|~sQ989_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f21982,f110])).
% 46.78/6.37 fof(f22001,plain,(
% 46.78/6.37 ~sQ989_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f22000])).
% 46.78/6.37 fof(f22792,definition,(
% 46.78/6.37 sQ1012_spl <=> ('0'=s(sK16_skl('0',sK38_skl)))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ1012_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f22793,plain,(
% 46.78/6.37 '0'=s(sK16_skl('0',sK38_skl))|~sQ1012_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f22792])).
% 46.78/6.37 fof(f22804,definition,(
% 46.78/6.37 sQ1015_spl <=> ('0'=s(sK14_skl('0',sK38_skl)))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ1015_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f22805,plain,(
% 46.78/6.37 '0'=s(sK14_skl('0',sK38_skl))|~sQ1015_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f22804])).
% 46.78/6.37 fof(f22812,plain,(
% 46.78/6.37 $false|~sQ1015_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f22805,f110])).
% 46.78/6.37 fof(f22813,plain,(
% 46.78/6.37 ~sQ1015_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f22812])).
% 46.78/6.37 fof(f22814,plain,(
% 46.78/6.37 $false|~sQ1012_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f22793,f110])).
% 46.78/6.37 fof(f22815,plain,(
% 46.78/6.37 ~sQ1012_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f22814])).
% 46.78/6.37 fof(f23635,definition,(
% 46.78/6.37 sQ1051_spl <=> ('@<_succeeds'(sK37_skl,'0'))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ1051_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f23636,plain,(
% 46.78/6.37 '@<_succeeds'(sK37_skl,'0')|~sQ1051_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f23635])).
% 46.78/6.37 fof(f28722,definition,(
% 46.78/6.37 sQ1221_spl <=> ('0'=s(sK14_skl('0',sK37_skl)))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ1221_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f28723,plain,(
% 46.78/6.37 '0'=s(sK14_skl('0',sK37_skl))|~sQ1221_spl),
% 46.78/6.37 inference(component_clause,[status(thm)],[f28722])).
% 46.78/6.37 fof(f28729,plain,(
% 46.78/6.37 $false|~sQ1221_spl),
% 46.78/6.37 inference(forward_subsumption_resolution,[status(thm)],[f28723,f110])).
% 46.78/6.37 fof(f28730,plain,(
% 46.78/6.37 ~sQ1221_spl),
% 46.78/6.37 inference(contradiction_clause,[status(thm)],[f28729])).
% 46.78/6.37 fof(f28811,definition,(
% 46.78/6.37 sQ1229_spl <=> ('0'=s(sK22_skl(sK38_skl,'0')))),
% 46.78/6.37 introduced(definition,[new_symbols(definition,[sQ1229_spl])],[split_symbol_definition])).
% 46.78/6.37 fof(f28812,plain,(
% 46.78/6.37 '0'=s(sK22_skl(sK38_skl,'0'))|~sQ1229_spl),
% 10.49/6.41 inference(component_clause,[status(thm)],[f28811])).
% 10.49/6.41 fof(f28819,definition,(
% 10.49/6.41 sQ1231_spl <=> ('0'=s(sK25_skl(sK38_skl,'0')))),
% 10.49/6.41 introduced(definition,[new_symbols(definition,[sQ1231_spl])],[split_symbol_definition])).
% 10.49/6.41 fof(f28820,plain,(
% 10.49/6.41 '0'=s(sK25_skl(sK38_skl,'0'))|~sQ1231_spl),
% 10.49/6.41 inference(component_clause,[status(thm)],[f28819])).
% 10.49/6.41 fof(f28823,plain,(
% 10.49/6.41 $false|~sQ1231_spl),
% 10.49/6.41 inference(forward_subsumption_resolution,[status(thm)],[f28820,f110])).
% 10.49/6.41 fof(f28824,plain,(
% 10.49/6.41 ~sQ1231_spl),
% 10.49/6.41 inference(contradiction_clause,[status(thm)],[f28823])).
% 10.49/6.41 fof(f28825,plain,(
% 10.49/6.41 $false|~sQ1229_spl),
% 10.49/6.41 inference(forward_subsumption_resolution,[status(thm)],[f28812,f110])).
% 10.49/6.41 fof(f28826,plain,(
% 10.49/6.41 ~sQ1229_spl),
% 10.49/6.41 inference(contradiction_clause,[status(thm)],[f28825])).
% 10.49/6.41 fof(f29513,plain,(
% 10.49/6.41 '0'=s(sK32_skl('0'))|~sQ1051_spl),
% 10.49/6.41 inference(resolution,[status(thm)],[f23636,f381])).
% 10.49/6.41 fof(f29528,plain,(
% 10.49/6.41 $false|~sQ1051_spl),
% 10.49/6.41 inference(forward_subsumption_resolution,[status(thm)],[f29513,f110])).
% 10.49/6.41 fof(f29529,plain,(
% 10.49/6.41 ~sQ1051_spl),
% 10.49/6.41 inference(contradiction_clause,[status(thm)],[f29528])).
% 10.49/6.41 fof(f29972,plain,(
% 10.49/6.41 '@=<_succeeds'(s('@+'(sK38_skl,sK39_skl)),s('@+'(sK38_skl,sK40_skl)))|~sQ4_spl|~sQ5_spl),
% 10.49/6.41 inference(resolution,[status(thm)],[f10673,f540])).
% 10.49/6.41 fof(f29978,plain,(
% 10.49/6.41 '@=<_succeeds'('@+'(sK37_skl,sK39_skl),s('@+'(sK38_skl,sK40_skl)))|~sQ0_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl),
% 10.49/6.41 inference(forward_demodulation,[status(thm)],[f16573,f29972])).
% 10.49/6.41 fof(f29979,plain,(
% 10.49/6.41 '@=<_succeeds'('@+'(sK37_skl,sK39_skl),'@+'(sK37_skl,sK40_skl))|~sQ0_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl),
% 10.49/6.41 inference(forward_demodulation,[status(thm)],[f16573,f29978])).
% 10.49/6.41 fof(f29980,plain,(
% 10.49/6.41 $false|sQ6_spl|~sQ0_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl),
% 10.49/6.41 inference(forward_subsumption_resolution,[status(thm)],[f29979,f531])).
% 10.49/6.41 fof(f29981,plain,(
% 10.49/6.41 sQ6_spl|~sQ0_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl),
% 10.49/6.41 inference(contradiction_clause,[status(thm)],[f29980])).
% 10.49/6.41 fof(f29982,plain,(
% 10.49/6.41 $false),
% 10.49/6.41 inference(sat_refutation,[status(thm)],[f516,f520,f524,f528,f532,f4048,f4100,f4928,f5019,f5401,f8083,f8542,f9671,f10642,f11485,f11637,f11916,f12253,f12281,f15439,f15484,f15903,f15905,f17095,f17856,f18149,f18151,f18956,f18958,f19682,f19684,f20232,f20234,f20308,f20310,f20350,f20352,f20354,f20357,f20799,f22001,f22813,f22815,f28730,f28824,f28826,f29529,f29981])).
% 10.49/6.41 % SZS output end CNFRefutation for theBenchmark.p
% 10.49/6.44 % Elapsed time: 6.061835 seconds
% 10.49/6.44 % CPU time: 47.714175 seconds
% 10.49/6.44 % Total memory used: 472.526 MB
% 10.49/6.44 % Net memory used: 427.195 MB
%------------------------------------------------------------------------------