%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWX034+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:34 PM UTC 2026
% Result : Theorem 106.75s 14.02s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX034+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n005.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 21 10:22:19 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.15/0.40 % Drodi V4.1.1
% 106.75/14.02 % Refutation found
% 106.75/14.02 % SZS status Theorem for theBenchmark: Theorem is valid
% 106.75/14.02 % SZS output start CNFRefutation for theBenchmark
% 106.75/14.02 fof(f1,axiom,(
% 106.75/14.02 (! [Xx3] : '0' != s(Xx3) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f2,axiom,(
% 106.75/14.02 (! [Xx4,Xx5] :( s(Xx4) = s(Xx5)=> Xx4 = Xx5 ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f4,axiom,(
% 106.75/14.02 (! [Xx6] :( gr(Xx6)<=> gr(s(Xx6)) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f5,axiom,(
% 106.75/14.02 (! [Xx7,Xx8,Xx9] :~ ( times_succeeds(Xx7,Xx8,Xx9)& times_fails(Xx7,Xx8,Xx9) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f11,axiom,(
% 106.75/14.02 (! [Xx15,Xx16] :~ ( '@<_succeeds'(Xx15,Xx16)& '@<_fails'(Xx15,Xx16) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f13,axiom,(
% 106.75/14.02 (! [Xx17] :~ ( nat_succeeds(Xx17)& nat_fails(Xx17) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f15,axiom,(
% 106.75/14.02 (! [Xx1,Xx2,Xx3] :( times_succeeds(Xx1,Xx2,Xx3)<=> ( (? [Xx4,Xx5] :( Xx1 = s(Xx4)& times_succeeds(Xx4,Xx2,Xx5)& plus_succeeds(Xx2,Xx5,Xx3) ))| ( Xx1 = '0'& Xx3 = '0' ) ) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f17,axiom,(
% 106.75/14.02 (! [Xx1,Xx2,Xx3] :( times_terminates(Xx1,Xx2,Xx3)<=> ( (! [Xx4,Xx5] :( $true& ( Xx1 != s(Xx4)| ( times_terminates(Xx4,Xx2,Xx5)& ( times_fails(Xx4,Xx2,Xx5)| plus_terminates(Xx2,Xx5,Xx3) ) ) ) ))& $true& ( Xx1 != '0'| $true ) ) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f18,axiom,(
% 106.75/14.02 (! [Xx1,Xx2,Xx3] :( plus_succeeds(Xx1,Xx2,Xx3)<=> ( (? [Xx4,Xx5] :( Xx1 = s(Xx4)& Xx3 = s(Xx5)& plus_succeeds(Xx4,Xx2,Xx5) ))| ( Xx1 = '0'& Xx3 = Xx2 ) ) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f22,axiom,(
% 106.75/14.02 (! [Xx1,Xx2] :( '@=<_fails'(Xx1,Xx2)<=> ( (! [Xx3,Xx4] :( Xx1 != s(Xx3)| Xx2 != s(Xx4)| '@=<_fails'(Xx3,Xx4) ))& Xx1 != '0' ) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f24,axiom,(
% 106.75/14.02 (! [Xx1,Xx2] :( '@<_succeeds'(Xx1,Xx2)<=> ( (? [Xx3,Xx4] :( Xx1 = s(Xx3)& Xx2 = s(Xx4)& '@<_succeeds'(Xx3,Xx4) ))| (? [Xx5] :( Xx1 = '0'& Xx2 = s(Xx5) ) )) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f26,axiom,(
% 106.75/14.02 (! [Xx1,Xx2] :( '@<_terminates'(Xx1,Xx2)<=> ( (! [Xx3,Xx4] :( $true& ( Xx1 != s(Xx3)| ( $true& ( Xx2 != s(Xx4)| '@<_terminates'(Xx3,Xx4) ) ) ) ))& (! [Xx5] :( $true& ( Xx1 != '0'| $true ) ) )) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f27,axiom,(
% 106.75/14.02 (! [Xx1] :( nat_succeeds(Xx1)<=> ( (? [Xx2] :( Xx1 = s(Xx2)& nat_succeeds(Xx2) ))| Xx1 = '0' ) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f33,axiom,(
% 106.75/14.02 (! [Xx] :( nat_succeeds(Xx)=> gr(Xx) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f34,axiom,(
% 106.75/14.02 (! [Xx,Xy,Xz] :( nat_succeeds(Xx)=> plus_terminates(Xx,Xy,Xz) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f43,axiom,(
% 106.75/14.02 (! [Xx,Xy] :( nat_succeeds(Xx)=> (? [Xz] : plus_succeeds(Xx,Xy,Xz) )) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f44,axiom,(
% 106.75/14.02 (! [Xx,Xy,Xz1,Xz2] :( ( plus_succeeds(Xx,Xy,Xz1)& plus_succeeds(Xx,Xy,Xz2) )=> Xz1 = Xz2 ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f45,axiom,(
% 106.75/14.02 (! [Xy] : '@+'('0',Xy) = Xy )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f47,axiom,(
% 106.75/14.02 (! [Xx,Xy] :( ( nat_succeeds(Xx)& nat_succeeds(Xy) )=> nat_succeeds('@+'(Xx,Xy)) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f49,axiom,(
% 106.75/14.02 (! [Xx] :( nat_succeeds(Xx)=> '@+'(Xx,'0') = Xx ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f57,axiom,(
% 106.75/14.02 ( (! [Xx] :( ( (? [Xx2] :( Xx = s(Xx2)& nat_succeeds(Xx2)& (! [Xy,Xz] :( nat_succeeds(Xy)=> times_terminates(Xx2,Xy,Xz) ) )))| Xx = '0' )=> (! [Xy,Xz] :( nat_succeeds(Xy)=> times_terminates(Xx,Xy,Xz) ) )))=> (! [Xx] :( nat_succeeds(Xx)=> (! [Xy,Xz] :( nat_succeeds(Xy)=> times_terminates(Xx,Xy,Xz) ) )) )) ),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f58,conjecture,(
% 106.75/14.02 (! [Xx,Xy,Xz] :( ( nat_succeeds(Xx)& nat_succeeds(Xy) )=> times_terminates(Xx,Xy,Xz) ) )),
% 106.75/14.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 106.75/14.02 fof(f59,negated_conjecture,(
% 106.75/14.02 ~((! [Xx,Xy,Xz] :( ( nat_succeeds(Xx)& nat_succeeds(Xy) )=> times_terminates(Xx,Xy,Xz) ) ))),
% 106.75/14.02 inference(negated_conjecture,[status(cth)],[f58])).
% 106.75/14.02 fof(f60,plain,(
% 106.75/14.02 ![X0]: (~'0'=s(X0))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f1])).
% 106.75/14.02 fof(f61,plain,(
% 106.75/14.02 ![Xx4,Xx5]: (~s(Xx4)=s(Xx5)|Xx4=Xx5)),
% 106.75/14.02 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 106.75/14.02 fof(f62,plain,(
% 106.75/14.02 ![X0,X1]: (~s(X0)=s(X1)|X0=X1)),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f61])).
% 106.75/14.02 fof(f64,plain,(
% 106.75/14.02 ![Xx6]: ((~gr(Xx6)|gr(s(Xx6)))&(gr(Xx6)|~gr(s(Xx6))))),
% 106.75/14.02 inference(NNF_transformation,[status(thm)],[f4])).
% 106.75/14.02 fof(f65,plain,(
% 106.75/14.02 (![Xx6]: (~gr(Xx6)|gr(s(Xx6))))&(![Xx6]: (gr(Xx6)|~gr(s(Xx6))))),
% 106.75/14.02 inference(miniscoping,[status(thm)],[f64])).
% 106.75/14.02 fof(f66,plain,(
% 106.75/14.02 ![X0]: (~gr(X0)|gr(s(X0)))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f65])).
% 106.75/14.02 fof(f68,plain,(
% 106.75/14.02 ![Xx7,Xx8,Xx9]: (~times_succeeds(Xx7,Xx8,Xx9)|~times_fails(Xx7,Xx8,Xx9))),
% 106.75/14.02 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 106.75/14.02 fof(f69,plain,(
% 106.75/14.02 ![X0,X1,X2]: (~times_succeeds(X0,X1,X2)|~times_fails(X0,X1,X2))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f68])).
% 106.75/14.02 fof(f80,plain,(
% 106.75/14.02 ![Xx15,Xx16]: (~'@<_succeeds'(Xx15,Xx16)|~'@<_fails'(Xx15,Xx16))),
% 106.75/14.02 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 106.75/14.02 fof(f81,plain,(
% 106.75/14.02 ![X0,X1]: (~'@<_succeeds'(X0,X1)|~'@<_fails'(X0,X1))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f80])).
% 106.75/14.02 fof(f84,plain,(
% 106.75/14.02 ![Xx17]: (~nat_succeeds(Xx17)|~nat_fails(Xx17))),
% 106.75/14.02 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 106.75/14.02 fof(f85,plain,(
% 106.75/14.02 ![X0]: (~nat_succeeds(X0)|~nat_fails(X0))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f84])).
% 106.75/14.02 fof(f88,definition,(
% 106.75/14.02 ![Xx1,Xx2,Xx3,Xx4,Xx5]: (sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1)<=>((Xx1=s(Xx4)×_succeeds(Xx4,Xx2,Xx5))&plus_succeeds(Xx2,Xx5,Xx3)))),
% 106.75/14.02 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 106.75/14.02 fof(f89,plain,(
% 106.75/14.02 ![Xx1,Xx2,Xx3]: (times_succeeds(Xx1,Xx2,Xx3)<=>((?[Xx4,Xx5]: sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1))|(Xx1='0'&Xx3='0')))),
% 106.75/14.02 inference(formula_renaming,[status(thm)],[f15,f88])).
% 106.75/14.02 fof(f90,plain,(
% 106.75/14.02 ![Xx1,Xx2,Xx3]: ((~times_succeeds(Xx1,Xx2,Xx3)|((?[Xx4,Xx5]: sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1))|(Xx1='0'&Xx3='0')))&(times_succeeds(Xx1,Xx2,Xx3)|((![Xx4,Xx5]: ~sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1))&(~Xx1='0'|~Xx3='0'))))),
% 106.75/14.02 inference(NNF_transformation,[status(thm)],[f89])).
% 106.75/14.02 fof(f91,plain,(
% 106.75/14.02 (![Xx1,Xx2,Xx3]: (~times_succeeds(Xx1,Xx2,Xx3)|((?[Xx4,Xx5]: sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1))|(Xx1='0'&Xx3='0'))))&(![Xx1,Xx2,Xx3]: (times_succeeds(Xx1,Xx2,Xx3)|((![Xx4,Xx5]: ~sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1))&(~Xx1='0'|~Xx3='0'))))),
% 106.75/14.02 inference(miniscoping,[status(thm)],[f90])).
% 106.75/14.02 fof(f92,plain,(
% 106.75/14.02 (![Xx1,Xx2,Xx3]: (~times_succeeds(Xx1,Xx2,Xx3)|(sP0_prd(sK1_skl(Xx3,Xx2,Xx1),sK0_skl(Xx3,Xx2,Xx1),Xx3,Xx2,Xx1)|(Xx1='0'&Xx3='0'))))&(![Xx1,Xx2,Xx3]: (times_succeeds(Xx1,Xx2,Xx3)|((![Xx4,Xx5]: ~sP0_prd(Xx5,Xx4,Xx3,Xx2,Xx1))&(~Xx1='0'|~Xx3='0'))))),
% 106.75/14.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Xx4,sK0_skl(Xx3,Xx2,Xx1)),skolemize(Xx5,sK1_skl(Xx3,Xx2,Xx1))],[f91])).
% 106.75/14.02 fof(f96,plain,(
% 106.75/14.02 ![X0,X1,X2]: (times_succeeds(X0,X1,X2)|~X0='0'|~X2='0')),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f92])).
% 106.75/14.02 fof(f106,plain,(
% 106.75/14.02 ![Xx1,Xx2,Xx3]: ((~times_terminates(Xx1,Xx2,Xx3)|(((![Xx4,Xx5]: ($true&(~Xx1=s(Xx4)|(times_terminates(Xx4,Xx2,Xx5)&(times_fails(Xx4,Xx2,Xx5)|plus_terminates(Xx2,Xx5,Xx3))))))&$true)&(~Xx1='0'|$true)))&(times_terminates(Xx1,Xx2,Xx3)|(((?[Xx4,Xx5]: ($false|(Xx1=s(Xx4)&(~times_terminates(Xx4,Xx2,Xx5)|(~times_fails(Xx4,Xx2,Xx5)&~plus_terminates(Xx2,Xx5,Xx3))))))|$false)|(Xx1='0'&$false))))),
% 106.75/14.02 inference(NNF_transformation,[status(thm)],[f17])).
% 106.75/14.02 fof(f107,plain,(
% 106.75/14.02 (![Xx1,Xx2,Xx3]: (~times_terminates(Xx1,Xx2,Xx3)|((($true&(![Xx4]: (~Xx1=s(Xx4)|((![Xx5]: times_terminates(Xx4,Xx2,Xx5))&(![Xx5]: (times_fails(Xx4,Xx2,Xx5)|plus_terminates(Xx2,Xx5,Xx3)))))))&$true)&(~Xx1='0'|$true))))&(![Xx1,Xx2,Xx3]: (times_terminates(Xx1,Xx2,Xx3)|((($false|(?[Xx4]: (Xx1=s(Xx4)&((?[Xx5]: ~times_terminates(Xx4,Xx2,Xx5))|(?[Xx5]: (~times_fails(Xx4,Xx2,Xx5)&~plus_terminates(Xx2,Xx5,Xx3)))))))|$false)|(Xx1='0'&$false))))),
% 106.75/14.02 inference(miniscoping,[status(thm)],[f106])).
% 106.75/14.02 fof(f108,plain,(
% 106.75/14.02 (![Xx1,Xx2,Xx3]: (~times_terminates(Xx1,Xx2,Xx3)|((($true&(![Xx4]: (~Xx1=s(Xx4)|((![Xx5]: times_terminates(Xx4,Xx2,Xx5))&(![Xx5]: (times_fails(Xx4,Xx2,Xx5)|plus_terminates(Xx2,Xx5,Xx3)))))))&$true)&(~Xx1='0'|$true))))&(![Xx1,Xx2,Xx3]: (times_terminates(Xx1,Xx2,Xx3)|((($false|(Xx1=s(sK4_skl(Xx3,Xx2,Xx1))&(~times_terminates(sK4_skl(Xx3,Xx2,Xx1),Xx2,sK5_skl(Xx3,Xx2,Xx1))|(~times_fails(sK4_skl(Xx3,Xx2,Xx1),Xx2,sK6_skl(Xx3,Xx2,Xx1))&~plus_terminates(Xx2,sK6_skl(Xx3,Xx2,Xx1),Xx3)))))|$false)|(Xx1='0'&$false))))),
% 106.75/14.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(Xx4,sK4_skl(Xx3,Xx2,Xx1)),skolemize(Xx5,sK5_skl(Xx3,Xx2,Xx1)),skolemize(Xx5,sK6_skl(Xx3,Xx2,Xx1))],[f107])).
% 106.75/14.02 fof(f109,plain,(
% 106.75/14.02 (![Xx1,Xx2,Xx3]: (~times_terminates(Xx1,Xx2,Xx3)|(![Xx4]: (~Xx1=s(Xx4)|((![Xx5]: times_terminates(Xx4,Xx2,Xx5))&(![Xx5]: (times_fails(Xx4,Xx2,Xx5)|plus_terminates(Xx2,Xx5,Xx3))))))))&(![Xx1,Xx2,Xx3]: (times_terminates(Xx1,Xx2,Xx3)|(?[Xx4]: (Xx1=s(sK4_skl(Xx3,Xx2,Xx1))&((?[Xx5]: ~times_terminates(sK4_skl(Xx3,Xx2,Xx1),Xx2,sK5_skl(Xx3,Xx2,Xx1)))|(?[Xx5]: (~times_fails(sK4_skl(Xx3,Xx2,Xx1),Xx2,sK6_skl(Xx3,Xx2,Xx1))&~plus_terminates(Xx2,sK6_skl(Xx3,Xx2,Xx1),Xx3))))))))),
% 106.75/14.02 inference(true_and_false_simplification,[status(thm)],[f108])).
% 106.75/14.02 fof(f112,plain,(
% 106.75/14.02 ![X0,X1,X2]: (times_terminates(X0,X1,X2)|X0=s(sK4_skl(X2,X1,X0)))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f109])).
% 106.75/14.02 fof(f114,plain,(
% 106.75/14.02 ![X0,X1,X2]: (times_terminates(X0,X1,X2)|~times_terminates(sK4_skl(X2,X1,X0),X1,sK5_skl(X2,X1,X0))|~plus_terminates(X1,sK6_skl(X2,X1,X0),X2))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f109])).
% 106.75/14.02 fof(f115,definition,(
% 106.75/14.02 ![Xx1,Xx2,Xx3,Xx4,Xx5]: (sP2_prd(Xx5,Xx4,Xx3,Xx2,Xx1)<=>((Xx1=s(Xx4)&Xx3=s(Xx5))&plus_succeeds(Xx4,Xx2,Xx5)))),
% 106.75/14.02 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 106.75/14.02 fof(f116,plain,(
% 106.75/14.02 ![Xx1,Xx2,Xx3]: (plus_succeeds(Xx1,Xx2,Xx3)<=>((?[Xx4,Xx5]: sP2_prd(Xx5,Xx4,Xx3,Xx2,Xx1))|(Xx1='0'&Xx3=Xx2)))),
% 106.75/14.02 inference(formula_renaming,[status(thm)],[f18,f115])).
% 106.75/14.02 fof(f117,plain,(
% 106.75/14.02 ![Xx1,Xx2,Xx3]: ((~plus_succeeds(Xx1,Xx2,Xx3)|((?[Xx4,Xx5]: sP2_prd(Xx5,Xx4,Xx3,Xx2,Xx1))|(Xx1='0'&Xx3=Xx2)))&(plus_succeeds(Xx1,Xx2,Xx3)|((![Xx4,Xx5]: ~sP2_prd(Xx5,Xx4,Xx3,Xx2,Xx1))&(~Xx1='0'|~Xx3=Xx2))))),
% 106.75/14.02 inference(NNF_transformation,[status(thm)],[f116])).
% 106.75/14.02 fof(f118,plain,(
% 106.75/14.02 (![Xx1,Xx2,Xx3]: (~plus_succeeds(Xx1,Xx2,Xx3)|((?[Xx4,Xx5]: sP2_prd(Xx5,Xx4,Xx3,Xx2,Xx1))|(Xx1='0'&Xx3=Xx2))))&(![Xx1,Xx2,Xx3]: (plus_succeeds(Xx1,Xx2,Xx3)|((![Xx4,Xx5]: ~sP2_prd(Xx5,Xx4,Xx3,Xx2,Xx1))&(~Xx1='0'|~Xx3=Xx2))))),
% 106.75/14.02 inference(miniscoping,[status(thm)],[f117])).
% 106.75/14.02 fof(f119,plain,(
% 106.75/14.02 (![Xx1,Xx2,Xx3]: (~plus_succeeds(Xx1,Xx2,Xx3)|(sP2_prd(sK8_skl(Xx3,Xx2,Xx1),sK7_skl(Xx3,Xx2,Xx1),Xx3,Xx2,Xx1)|(Xx1='0'&Xx3=Xx2))))&(![Xx1,Xx2,Xx3]: (plus_succeeds(Xx1,Xx2,Xx3)|((![Xx4,Xx5]: ~sP2_prd(Xx5,Xx4,Xx3,Xx2,Xx1))&(~Xx1='0'|~Xx3=Xx2))))),
% 106.75/14.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(Xx4,sK7_skl(Xx3,Xx2,Xx1)),skolemize(Xx5,sK8_skl(Xx3,Xx2,Xx1))],[f118])).
% 106.75/14.02 fof(f123,plain,(
% 106.75/14.02 ![X0,X1,X2]: (plus_succeeds(X0,X1,X2)|~X0='0'|~X2=X1)),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f119])).
% 106.75/14.02 fof(f149,plain,(
% 106.75/14.02 ![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')))),
% 106.75/14.02 inference(NNF_transformation,[status(thm)],[f22])).
% 106.75/14.02 fof(f150,plain,(
% 106.75/14.02 (![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')))),
% 106.75/14.02 inference(miniscoping,[status(thm)],[f149])).
% 106.75/14.02 fof(f151,plain,(
% 106.75/14.02 (![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')))),
% 106.75/14.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(Xx3,sK15_skl(Xx2,Xx1)),skolemize(Xx4,sK16_skl(Xx2,Xx1))],[f150])).
% 106.75/14.02 fof(f153,plain,(
% 106.75/14.02 ![X0,X1]: (~'@=<_fails'(X0,X1)|~X0='0')),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f151])).
% 106.75/14.02 fof(f165,definition,(
% 106.75/14.02 ![Xx1,Xx2,Xx3,Xx4]: (sP4_prd(Xx4,Xx3,Xx2,Xx1)<=>((Xx1=s(Xx3)&Xx2=s(Xx4))&'@<_succeeds'(Xx3,Xx4)))),
% 106.75/14.02 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 106.75/14.02 fof(f166,plain,(
% 106.75/14.02 ![Xx1,Xx2]: ('@<_succeeds'(Xx1,Xx2)<=>((?[Xx3,Xx4]: sP4_prd(Xx4,Xx3,Xx2,Xx1))|(?[Xx5]: (Xx1='0'&Xx2=s(Xx5)))))),
% 106.75/14.02 inference(formula_renaming,[status(thm)],[f24,f165])).
% 106.75/14.02 fof(f167,plain,(
% 106.75/14.02 ![Xx1,Xx2]: ((~'@<_succeeds'(Xx1,Xx2)|((?[Xx3,Xx4]: sP4_prd(Xx4,Xx3,Xx2,Xx1))|(?[Xx5]: (Xx1='0'&Xx2=s(Xx5)))))&('@<_succeeds'(Xx1,Xx2)|((![Xx3,Xx4]: ~sP4_prd(Xx4,Xx3,Xx2,Xx1))&(![Xx5]: (~Xx1='0'|~Xx2=s(Xx5))))))),
% 106.75/14.02 inference(NNF_transformation,[status(thm)],[f166])).
% 106.75/14.02 fof(f168,plain,(
% 106.75/14.02 (![Xx1,Xx2]: (~'@<_succeeds'(Xx1,Xx2)|((?[Xx3,Xx4]: sP4_prd(Xx4,Xx3,Xx2,Xx1))|(Xx1='0'&(?[Xx5]: Xx2=s(Xx5))))))&(![Xx1,Xx2]: ('@<_succeeds'(Xx1,Xx2)|((![Xx3,Xx4]: ~sP4_prd(Xx4,Xx3,Xx2,Xx1))&(~Xx1='0'|(![Xx5]: ~Xx2=s(Xx5))))))),
% 106.75/14.02 inference(miniscoping,[status(thm)],[f167])).
% 106.75/14.02 fof(f169,plain,(
% 106.75/14.02 (![Xx1,Xx2]: (~'@<_succeeds'(Xx1,Xx2)|(sP4_prd(sK20_skl(Xx2,Xx1),sK19_skl(Xx2,Xx1),Xx2,Xx1)|(Xx1='0'&Xx2=s(sK21_skl(Xx2,Xx1))))))&(![Xx1,Xx2]: ('@<_succeeds'(Xx1,Xx2)|((![Xx3,Xx4]: ~sP4_prd(Xx4,Xx3,Xx2,Xx1))&(~Xx1='0'|(![Xx5]: ~Xx2=s(Xx5))))))),
% 106.75/14.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl]),skolemize(Xx3,sK19_skl(Xx2,Xx1)),skolemize(Xx4,sK20_skl(Xx2,Xx1)),skolemize(Xx5,sK21_skl(Xx2,Xx1))],[f168])).
% 106.75/14.02 fof(f173,plain,(
% 106.75/14.02 ![X0,X1,X2]: ('@<_succeeds'(X0,X1)|~X0='0'|~X1=s(X2))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f169])).
% 106.75/14.02 fof(f183,plain,(
% 106.75/14.02 ![Xx1,Xx2]: ((~'@<_terminates'(Xx1,Xx2)|((![Xx3,Xx4]: ($true&(~Xx1=s(Xx3)|($true&(~Xx2=s(Xx4)|'@<_terminates'(Xx3,Xx4))))))&(![Xx5]: ($true&(~Xx1='0'|$true)))))&('@<_terminates'(Xx1,Xx2)|((?[Xx3,Xx4]: ($false|(Xx1=s(Xx3)&($false|(Xx2=s(Xx4)&~'@<_terminates'(Xx3,Xx4))))))|(?[Xx5]: ($false|(Xx1='0'&$false))))))),
% 106.75/14.02 inference(NNF_transformation,[status(thm)],[f26])).
% 106.75/14.02 fof(f184,plain,(
% 106.75/14.02 (![Xx1,Xx2]: (~'@<_terminates'(Xx1,Xx2)|(($true&(![Xx3]: (~Xx1=s(Xx3)|($true&(![Xx4]: (~Xx2=s(Xx4)|'@<_terminates'(Xx3,Xx4)))))))&($true&(~Xx1='0'|$true)))))&(![Xx1,Xx2]: ('@<_terminates'(Xx1,Xx2)|(($false|(?[Xx3]: (Xx1=s(Xx3)&($false|(?[Xx4]: (Xx2=s(Xx4)&~'@<_terminates'(Xx3,Xx4)))))))|($false|(Xx1='0'&$false)))))),
% 106.75/14.02 inference(miniscoping,[status(thm)],[f183])).
% 106.75/14.02 fof(f185,plain,(
% 106.75/14.02 (![Xx1,Xx2]: (~'@<_terminates'(Xx1,Xx2)|(($true&(![Xx3]: (~Xx1=s(Xx3)|($true&(![Xx4]: (~Xx2=s(Xx4)|'@<_terminates'(Xx3,Xx4)))))))&($true&(~Xx1='0'|$true)))))&(![Xx1,Xx2]: ('@<_terminates'(Xx1,Xx2)|(($false|(Xx1=s(sK25_skl(Xx2,Xx1))&($false|(Xx2=s(sK26_skl(Xx2,Xx1))&~'@<_terminates'(sK25_skl(Xx2,Xx1),sK26_skl(Xx2,Xx1))))))|($false|(Xx1='0'&$false)))))),
% 106.75/14.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl,sK26_skl]),skolemize(Xx3,sK25_skl(Xx2,Xx1)),skolemize(Xx4,sK26_skl(Xx2,Xx1))],[f184])).
% 106.75/14.02 fof(f186,plain,(
% 106.75/14.02 (![Xx1,Xx2]: (~'@<_terminates'(Xx1,Xx2)|(![Xx3]: (~Xx1=s(Xx3)|(![Xx4]: (~Xx2=s(Xx4)|'@<_terminates'(Xx3,Xx4)))))))&(![Xx1,Xx2]: ('@<_terminates'(Xx1,Xx2)|(?[Xx3]: (Xx1=s(sK25_skl(Xx2,Xx1))&(?[Xx4]: (Xx2=s(sK26_skl(Xx2,Xx1))&~'@<_terminates'(sK25_skl(Xx2,Xx1),sK26_skl(Xx2,Xx1))))))))),
% 106.75/14.02 inference(true_and_false_simplification,[status(thm)],[f185])).
% 106.75/14.02 fof(f189,plain,(
% 106.75/14.02 ![X0,X1]: ('@<_terminates'(X0,X1)|X1=s(sK26_skl(X1,X0)))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f186])).
% 106.75/14.02 fof(f191,plain,(
% 106.75/14.02 ![Xx1]: ((~nat_succeeds(Xx1)|((?[Xx2]: (Xx1=s(Xx2)&nat_succeeds(Xx2)))|Xx1='0'))&(nat_succeeds(Xx1)|((![Xx2]: (~Xx1=s(Xx2)|~nat_succeeds(Xx2)))&~Xx1='0')))),
% 106.75/14.02 inference(NNF_transformation,[status(thm)],[f27])).
% 106.75/14.02 fof(f192,plain,(
% 106.75/14.02 (![Xx1]: (~nat_succeeds(Xx1)|((?[Xx2]: (Xx1=s(Xx2)&nat_succeeds(Xx2)))|Xx1='0')))&(![Xx1]: (nat_succeeds(Xx1)|((![Xx2]: (~Xx1=s(Xx2)|~nat_succeeds(Xx2)))&~Xx1='0')))),
% 106.75/14.02 inference(miniscoping,[status(thm)],[f191])).
% 106.75/14.02 fof(f193,plain,(
% 106.75/14.02 (![Xx1]: (~nat_succeeds(Xx1)|((Xx1=s(sK27_skl(Xx1))&nat_succeeds(sK27_skl(Xx1)))|Xx1='0')))&(![Xx1]: (nat_succeeds(Xx1)|((![Xx2]: (~Xx1=s(Xx2)|~nat_succeeds(Xx2)))&~Xx1='0')))),
% 106.75/14.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(Xx2,sK27_skl(Xx1))],[f192])).
% 106.75/14.02 fof(f196,plain,(
% 106.75/14.02 ![X0,X1]: (nat_succeeds(X0)|~X0=s(X1)|~nat_succeeds(X1))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f193])).
% 106.75/14.02 fof(f197,plain,(
% 106.75/14.02 ![X0]: (nat_succeeds(X0)|~X0='0')),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f193])).
% 106.75/14.02 fof(f224,plain,(
% 106.75/14.02 ![Xx]: (~nat_succeeds(Xx)|gr(Xx))),
% 106.75/14.02 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 106.75/14.02 fof(f225,plain,(
% 106.75/14.02 ![X0]: (~nat_succeeds(X0)|gr(X0))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f224])).
% 106.75/14.02 fof(f226,plain,(
% 106.75/14.02 ![Xx,Xy,Xz]: (~nat_succeeds(Xx)|plus_terminates(Xx,Xy,Xz))),
% 106.75/14.02 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 106.75/14.02 fof(f227,plain,(
% 106.75/14.02 ![Xx]: (~nat_succeeds(Xx)|(![Xy,Xz]: plus_terminates(Xx,Xy,Xz)))),
% 106.75/14.02 inference(miniscoping,[status(thm)],[f226])).
% 106.75/14.02 fof(f228,plain,(
% 106.75/14.02 ![X0,X1,X2]: (~nat_succeeds(X0)|plus_terminates(X0,X1,X2))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f227])).
% 106.75/14.02 fof(f252,plain,(
% 106.75/14.02 ![Xx,Xy]: (~nat_succeeds(Xx)|(?[Xz]: plus_succeeds(Xx,Xy,Xz)))),
% 106.75/14.02 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 106.75/14.02 fof(f253,plain,(
% 106.75/14.02 ![Xx]: (~nat_succeeds(Xx)|(![Xy]: ?[Xz]: plus_succeeds(Xx,Xy,Xz)))),
% 106.75/14.02 inference(miniscoping,[status(thm)],[f252])).
% 106.75/14.02 fof(f254,plain,(
% 106.75/14.02 ![Xx]: (~nat_succeeds(Xx)|(![Xy]: plus_succeeds(Xx,Xy,sK30_skl(Xy,Xx))))),
% 106.75/14.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK30_skl]),skolemize(Xz,sK30_skl(Xy,Xx))],[f253])).
% 106.75/14.02 fof(f255,plain,(
% 106.75/14.02 ![X0,X1]: (~nat_succeeds(X0)|plus_succeeds(X0,X1,sK30_skl(X1,X0)))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f254])).
% 106.75/14.02 fof(f256,plain,(
% 106.75/14.02 ![Xx,Xy,Xz1,Xz2]: ((~plus_succeeds(Xx,Xy,Xz1)|~plus_succeeds(Xx,Xy,Xz2))|Xz1=Xz2)),
% 106.75/14.02 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 106.75/14.02 fof(f257,plain,(
% 106.75/14.02 ![Xz1,Xz2]: ((![Xx,Xy]: (~plus_succeeds(Xx,Xy,Xz1)|~plus_succeeds(Xx,Xy,Xz2)))|Xz1=Xz2)),
% 106.75/14.02 inference(miniscoping,[status(thm)],[f256])).
% 106.75/14.02 fof(f258,plain,(
% 106.75/14.02 ![X0,X1,X2,X3]: (~plus_succeeds(X0,X1,X2)|~plus_succeeds(X0,X1,X3)|X2=X3)),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f257])).
% 106.75/14.02 fof(f259,plain,(
% 106.75/14.02 ![X0]: ('@+'('0',X0)=X0)),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f45])).
% 106.75/14.02 fof(f263,plain,(
% 106.75/14.02 ![Xx,Xy]: ((~nat_succeeds(Xx)|~nat_succeeds(Xy))|nat_succeeds('@+'(Xx,Xy)))),
% 106.75/14.02 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 106.75/14.02 fof(f264,plain,(
% 106.75/14.02 ![X0,X1]: (~nat_succeeds(X0)|~nat_succeeds(X1)|nat_succeeds('@+'(X0,X1)))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f263])).
% 106.75/14.02 fof(f267,plain,(
% 106.75/14.02 ![Xx]: (~nat_succeeds(Xx)|'@+'(Xx,'0')=Xx)),
% 106.75/14.02 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 106.75/14.02 fof(f268,plain,(
% 106.75/14.02 ![X0]: (~nat_succeeds(X0)|'@+'(X0,'0')=X0)),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f267])).
% 106.75/14.02 fof(f288,plain,(
% 106.75/14.02 (?[Xx]: (((?[Xx2]: ((Xx=s(Xx2)&nat_succeeds(Xx2))&(![Xy,Xz]: (~nat_succeeds(Xy)|times_terminates(Xx2,Xy,Xz)))))|Xx='0')&(?[Xy,Xz]: (nat_succeeds(Xy)&~times_terminates(Xx,Xy,Xz)))))|(![Xx]: (~nat_succeeds(Xx)|(![Xy,Xz]: (~nat_succeeds(Xy)|times_terminates(Xx,Xy,Xz)))))),
% 106.75/14.02 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 106.75/14.02 fof(f289,plain,(
% 106.75/14.02 (?[Xx]: (((?[Xx2]: ((Xx=s(Xx2)&nat_succeeds(Xx2))&(![Xy]: (~nat_succeeds(Xy)|(![Xz]: times_terminates(Xx2,Xy,Xz))))))|Xx='0')&(?[Xy]: (nat_succeeds(Xy)&(?[Xz]: ~times_terminates(Xx,Xy,Xz))))))|(![Xx]: (~nat_succeeds(Xx)|(![Xy]: (~nat_succeeds(Xy)|(![Xz]: times_terminates(Xx,Xy,Xz))))))),
% 106.75/14.02 inference(miniscoping,[status(thm)],[f288])).
% 106.75/14.02 fof(f290,plain,(
% 106.75/14.02 ((((sK31_skl=s(sK32_skl)&nat_succeeds(sK32_skl))&(![Xy]: (~nat_succeeds(Xy)|(![Xz]: times_terminates(sK32_skl,Xy,Xz)))))|sK31_skl='0')&(nat_succeeds(sK33_skl)&~times_terminates(sK31_skl,sK33_skl,sK34_skl)))|(![Xx]: (~nat_succeeds(Xx)|(![Xy]: (~nat_succeeds(Xy)|(![Xz]: times_terminates(Xx,Xy,Xz))))))),
% 106.75/14.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK31_skl,sK32_skl,sK33_skl,sK34_skl]),skolemize(Xx,sK31_skl),skolemize(Xx2,sK32_skl),skolemize(Xy,sK33_skl),skolemize(Xz,sK34_skl)],[f289])).
% 106.75/14.02 fof(f291,plain,(
% 106.75/14.02 ![X0,X1,X2]: (sK31_skl=s(sK32_skl)|sK31_skl='0'|~nat_succeeds(X0)|~nat_succeeds(X1)|times_terminates(X0,X1,X2))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f290])).
% 106.75/14.02 fof(f293,plain,(
% 106.75/14.02 ![X0,X1,X2,X3,X4]: (~nat_succeeds(X0)|times_terminates(sK32_skl,X0,X1)|sK31_skl='0'|~nat_succeeds(X2)|~nat_succeeds(X3)|times_terminates(X2,X3,X4))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f290])).
% 106.75/14.02 fof(f294,plain,(
% 106.75/14.02 ![X0,X1,X2]: (nat_succeeds(sK33_skl)|~nat_succeeds(X0)|~nat_succeeds(X1)|times_terminates(X0,X1,X2))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f290])).
% 106.75/14.02 fof(f295,plain,(
% 106.75/14.02 ![X0,X1,X2]: (~times_terminates(sK31_skl,sK33_skl,sK34_skl)|~nat_succeeds(X0)|~nat_succeeds(X1)|times_terminates(X0,X1,X2))),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f290])).
% 106.75/14.02 fof(f296,plain,(
% 106.75/14.02 (?[Xx,Xy,Xz]: ((nat_succeeds(Xx)&nat_succeeds(Xy))&~times_terminates(Xx,Xy,Xz)))),
% 106.75/14.02 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 106.75/14.02 fof(f297,plain,(
% 106.75/14.02 ?[Xx,Xy]: ((nat_succeeds(Xx)&nat_succeeds(Xy))&(?[Xz]: ~times_terminates(Xx,Xy,Xz)))),
% 106.75/14.02 inference(miniscoping,[status(thm)],[f296])).
% 106.75/14.02 fof(f298,plain,(
% 106.75/14.02 ((nat_succeeds(sK35_skl)&nat_succeeds(sK36_skl))&~times_terminates(sK35_skl,sK36_skl,sK37_skl))),
% 106.75/14.02 inference(skolemize,[status(esa),new_symbols(skolem,[sK35_skl,sK36_skl,sK37_skl]),skolemize(Xx,sK35_skl),skolemize(Xy,sK36_skl),skolemize(Xz,sK37_skl)],[f297])).
% 106.75/14.02 fof(f299,plain,(
% 106.75/14.02 nat_succeeds(sK35_skl)),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f298])).
% 106.75/14.02 fof(f300,plain,(
% 106.75/14.02 nat_succeeds(sK36_skl)),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f298])).
% 106.75/14.02 fof(f301,plain,(
% 106.75/14.02 ~times_terminates(sK35_skl,sK36_skl,sK37_skl)),
% 106.75/14.02 inference(cnf_transformation,[status(thm)],[f298])).
% 106.75/14.02 fof(f338,definition,(
% 106.75/14.02 sQ0_spl <=> (sK31_skl=s(sK32_skl))),
% 106.75/14.02 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 106.75/14.02 fof(f339,plain,(
% 106.75/14.02 sK31_skl=s(sK32_skl)|~sQ0_spl),
% 106.75/14.02 inference(component_clause,[status(thm)],[f338])).
% 106.75/14.02 fof(f341,definition,(
% 106.75/14.02 sQ1_spl <=> (sK31_skl='0')),
% 106.75/14.02 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 106.75/14.02 fof(f342,plain,(
% 106.75/14.02 sK31_skl='0'|~sQ1_spl),
% 106.75/14.02 inference(component_clause,[status(thm)],[f341])).
% 106.75/14.02 fof(f344,definition,(
% 106.75/14.02 ![X0,X1,X2]: (sQ2_spl <=> (~nat_succeeds(X0)|~nat_succeeds(X1)|times_terminates(X0,X1,X2)))),
% 106.75/14.02 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 106.75/14.02 fof(f345,plain,(
% 106.75/14.02 ![X0,X1,X2]: (~nat_succeeds(X0)|~nat_succeeds(X1)|times_terminates(X0,X1,X2)|~sQ2_spl)),
% 106.75/14.02 inference(component_clause,[status(thm)],[f344])).
% 106.75/14.02 fof(f347,plain,(
% 106.75/14.02 sQ0_spl|sQ1_spl|sQ2_spl),
% 106.75/14.02 inference(split_clause,[status(thm)],[f291,f338,f341,f344])).
% 106.75/14.02 fof(f352,definition,(
% 106.75/14.02 ![X0,X1]: (sQ4_spl <=> (~nat_succeeds(X0)|times_terminates(sK32_skl,X0,X1)))),
% 106.75/14.02 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 106.75/14.02 fof(f353,plain,(
% 106.75/14.02 ![X0,X1]: (~nat_succeeds(X0)|times_terminates(sK32_skl,X0,X1)|~sQ4_spl)),
% 106.75/14.02 inference(component_clause,[status(thm)],[f352])).
% 106.75/14.02 fof(f355,plain,(
% 106.75/14.02 sQ4_spl|sQ1_spl|sQ2_spl),
% 106.75/14.02 inference(split_clause,[status(thm)],[f293,f352,f341,f344])).
% 106.75/14.02 fof(f356,definition,(
% 106.75/14.02 sQ5_spl <=> (nat_succeeds(sK33_skl))),
% 106.75/14.02 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 106.75/14.02 fof(f357,plain,(
% 106.75/14.02 nat_succeeds(sK33_skl)|~sQ5_spl),
% 106.75/14.02 inference(component_clause,[status(thm)],[f356])).
% 106.75/14.02 fof(f359,plain,(
% 106.75/14.02 sQ5_spl|sQ2_spl),
% 106.75/14.02 inference(split_clause,[status(thm)],[f294,f356,f344])).
% 106.75/14.02 fof(f360,definition,(
% 106.75/14.02 sQ6_spl <=> (times_terminates(sK31_skl,sK33_skl,sK34_skl))),
% 106.75/14.02 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 106.75/14.02 fof(f362,plain,(
% 106.75/14.02 ~times_terminates(sK31_skl,sK33_skl,sK34_skl)|sQ6_spl),
% 106.75/14.02 inference(component_clause,[status(thm)],[f360])).
% 106.75/14.02 fof(f363,plain,(
% 106.75/14.02 ~sQ6_spl|sQ2_spl),
% 106.75/14.02 inference(split_clause,[status(thm)],[f295,f360,f344])).
% 106.75/14.02 fof(f364,plain,(
% 106.75/14.02 ![X0,X1]: (plus_succeeds(X0,X1,X1)|~X0='0')),
% 106.75/14.02 inference(destructive_equality_resolution,[status(thm)],[f123])).
% 106.75/14.02 fof(f367,plain,(
% 106.75/14.02 ![X0]: (nat_succeeds(X0)|~X0=s(sK35_skl))),
% 106.75/14.02 inference(resolution,[status(thm)],[f196,f299])).
% 106.75/14.02 fof(f372,plain,(
% 106.75/14.02 nat_succeeds(s(sK35_skl))),
% 106.75/14.02 inference(equality_resolution,[status(thm)],[f367])).
% 106.75/14.02 fof(f377,plain,(
% 106.75/14.02 nat_succeeds('0')),
% 106.75/14.02 inference(equality_resolution,[status(thm)],[f197])).
% 106.75/14.02 fof(f400,plain,(
% 106.75/14.02 gr(s(sK35_skl))),
% 106.75/14.02 inference(resolution,[status(thm)],[f225,f372])).
% 106.75/14.02 fof(f437,definition,(
% 106.75/14.02 sQ14_spl <=> (nat_fails(s(sK35_skl)))),
% 106.75/14.02 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 106.75/14.02 fof(f438,plain,(
% 106.75/14.02 nat_fails(s(sK35_skl))|~sQ14_spl),
% 106.75/14.02 inference(component_clause,[status(thm)],[f437])).
% 106.75/14.02 fof(f513,plain,(
% 106.75/14.02 ![X0,X1]: (times_succeeds('@+'('0','0'),X0,X1)|~X1='0')),
% 106.75/14.02 inference(resolution,[status(thm)],[f96,f259])).
% 106.75/14.02 fof(f515,plain,(
% 106.75/14.02 ![X0,X1]: (times_succeeds('0',X0,X1)|~X1='0')),
% 106.75/14.02 inference(forward_demodulation,[status(thm)],[f259,f513])).
% 106.75/14.02 fof(f526,plain,(
% 106.75/14.02 ![X0]: (plus_succeeds('@+'('0','0'),X0,X0))),
% 106.75/14.02 inference(resolution,[status(thm)],[f364,f259])).
% 106.75/14.02 fof(f528,plain,(
% 106.75/14.02 ![X0]: (plus_succeeds('0',X0,X0))),
% 106.75/14.02 inference(forward_demodulation,[status(thm)],[f259,f526])).
% 106.75/14.02 fof(f555,plain,(
% 106.75/14.02 sK35_skl=s(sK4_skl(sK37_skl,sK36_skl,sK35_skl))),
% 106.75/14.02 inference(resolution,[status(thm)],[f112,f301])).
% 106.75/14.02 fof(f568,plain,(
% 106.75/14.02 ~'0'=sK35_skl),
% 106.75/14.02 inference(paramodulation,[status(thm)],[f555,f60])).
% 106.75/14.02 fof(f738,plain,(
% 106.75/14.02 '@+'(sK36_skl,'0')=sK36_skl),
% 106.75/14.02 inference(resolution,[status(thm)],[f268,f300])).
% 106.75/14.02 fof(f762,plain,(
% 106.75/14.02 ![X0]: (times_succeeds('0',X0,'@+'('0','0')))),
% 106.75/14.02 inference(resolution,[status(thm)],[f515,f259])).
% 106.75/14.02 fof(f764,plain,(
% 106.75/14.02 ![X0]: (times_succeeds('0',X0,'0'))),
% 106.75/14.02 inference(forward_demodulation,[status(thm)],[f259,f762])).
% 106.75/14.02 fof(f965,plain,(
% 106.75/14.02 ![X0,X1]: ('@<_succeeds'('@+'('0','0'),X0)|~X0=s(X1))),
% 106.75/14.02 inference(resolution,[status(thm)],[f173,f259])).
% 106.75/14.02 fof(f967,plain,(
% 106.75/14.02 ![X0,X1]: ('@<_succeeds'('0',X0)|~X0=s(X1))),
% 106.75/14.02 inference(forward_demodulation,[status(thm)],[f259,f965])).
% 106.75/14.02 fof(f986,plain,(
% 106.75/14.02 '@<_succeeds'('0',sK35_skl)),
% 106.75/14.02 inference(resolution,[status(thm)],[f967,f555])).
% 106.75/14.02 fof(f1609,plain,(
% 106.75/14.02 ![X0]: (plus_succeeds('0',X0,sK30_skl(X0,'0')))),
% 106.75/14.02 inference(resolution,[status(thm)],[f255,f377])).
% 106.75/14.02 fof(f1649,plain,(
% 106.75/14.02 ![X0,X1]: (~plus_succeeds('0',X0,X1)|X0=X1)),
% 106.75/14.02 inference(resolution,[status(thm)],[f258,f528])).
% 106.75/14.02 fof(f1673,plain,(
% 106.75/14.02 ![X0]: (~nat_succeeds(X0)|nat_succeeds('@+'(sK35_skl,X0)))),
% 106.75/14.02 inference(resolution,[status(thm)],[f264,f299])).
% 106.75/14.02 fof(f2413,definition,(
% 106.75/14.02 sQ158_spl <=> (nat_fails('@+'(sK35_skl,sK35_skl)))),
% 106.75/14.02 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 106.75/14.02 fof(f2414,plain,(
% 106.75/14.02 nat_fails('@+'(sK35_skl,sK35_skl))|~sQ158_spl),
% 106.75/14.02 inference(component_clause,[status(thm)],[f2413])).
% 106.75/14.02 fof(f2440,plain,(
% 106.75/14.02 ![X0,X1]: (~nat_succeeds(X0)|times_terminates(sK35_skl,X0,X1)|~sQ2_spl)),
% 106.75/14.02 inference(resolution,[status(thm)],[f345,f299])).
% 106.75/14.02 fof(f2538,plain,(
% 106.75/14.02 ~times_terminates('0',sK33_skl,sK34_skl)|~sQ1_spl|sQ6_spl),
% 106.75/14.02 inference(forward_demodulation,[status(thm)],[f342,f362])).
% 106.75/14.02 fof(f2541,plain,(
% 106.75/14.02 '0'=s(sK4_skl(sK34_skl,sK33_skl,'0'))|~sQ1_spl|sQ6_spl),
% 106.75/14.02 inference(resolution,[status(thm)],[f2538,f112])).
% 106.75/14.02 fof(f2544,plain,(
% 106.75/14.02 $false|~sQ1_spl|sQ6_spl),
% 106.75/14.02 inference(forward_subsumption_resolution,[status(thm)],[f2541,f60])).
% 106.75/14.02 fof(f2545,plain,(
% 106.75/14.02 ~sQ1_spl|sQ6_spl),
% 106.75/14.02 inference(contradiction_clause,[status(thm)],[f2544])).
% 106.75/14.02 fof(f2559,plain,(
% 106.75/14.02 ![X0]: (~sK31_skl=s(X0)|sK32_skl=X0|~sQ0_spl)),
% 106.75/14.02 inference(paramodulation,[status(thm)],[f339,f62])).
% 106.75/14.02 fof(f3542,definition,(
% 106.75/14.02 ![X0]: (sQ215_spl <=> (~X0=sK31_skl))),
% 106.75/14.02 introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 106.75/14.02 fof(f3543,plain,(
% 106.75/14.02 ![X0]: (~X0=sK31_skl|~sQ215_spl)),
% 106.75/14.02 inference(component_clause,[status(thm)],[f3542])).
% 106.75/14.02 fof(f3560,plain,(
% 106.75/14.02 $false|~sQ215_spl),
% 106.75/14.02 inference(resolution,[status(thm)],[f3543,f259])).
% 106.75/14.02 fof(f4872,plain,(
% 106.75/14.02 nat_succeeds('@+'(sK35_skl,sK35_skl))),
% 106.75/14.02 inference(resolution,[status(thm)],[f1673,f299])).
% 106.75/14.02 fof(f5097,plain,(
% 106.75/14.02 sK31_skl=s(sK4_skl(sK34_skl,sK33_skl,sK31_skl))|sQ6_spl),
% 106.75/14.02 inference(resolution,[status(thm)],[f362,f112])).
% 106.75/14.02 fof(f5202,plain,(
% 106.75/14.02 gr(s(s(sK35_skl)))),
% 106.75/14.02 inference(resolution,[status(thm)],[f400,f66])).
% 106.75/14.02 fof(f6998,plain,(
% 106.75/14.02 ![X0,X1]: (plus_terminates(sK33_skl,X0,X1)|~sQ5_spl)),
% 106.75/14.02 inference(resolution,[status(thm)],[f357,f228])).
% 106.75/14.02 fof(f7450,plain,(
% 106.75/14.02 sK32_skl=sK4_skl(sK34_skl,sK33_skl,sK31_skl)|sQ6_spl|~sQ0_spl),
% 106.75/14.02 inference(resolution,[status(thm)],[f5097,f2559])).
% 106.75/14.02 fof(f8273,plain,(
% 106.75/14.02 sK35_skl=s(sK4_skl(sK37_skl,sK36_skl,sK35_skl))),
% 106.75/14.02 inference(resolution,[status(thm)],[f301,f112])).
% 106.75/14.02 fof(f8742,plain,(
% 106.75/14.02 ~nat_succeeds(s(sK35_skl))|~sQ14_spl),
% 106.75/14.02 inference(resolution,[status(thm)],[f438,f85])).
% 106.75/14.02 fof(f8992,plain,(
% 106.75/14.02 ![X0]: (times_terminates(sK35_skl,sK36_skl,X0)|~sQ2_spl)),
% 106.75/14.02 inference(resolution,[status(thm)],[f2440,f300])).
% 106.75/14.02 fof(f10080,plain,(
% 106.75/14.02 ![X0]: (X0=sK30_skl(X0,'0'))),
% 106.75/14.02 inference(resolution,[status(thm)],[f1609,f1649])).
% 106.75/14.02 fof(f10964,definition,(
% 106.75/14.02 sQ437_spl <=> (times_fails('0',sK33_skl,'0'))),
% 106.75/14.02 introduced(definition,[new_symbols(definition,[sQ437_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f10965,plain,(
% 106.75/14.04 times_fails('0',sK33_skl,'0')|~sQ437_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f10964])).
% 106.75/14.04 fof(f11128,definition,(
% 106.75/14.04 sQ439_spl <=> ('0'=s(sK4_skl(sK34_skl,sK33_skl,'0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ439_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f11129,plain,(
% 106.75/14.04 '0'=s(sK4_skl(sK34_skl,sK33_skl,'0'))|~sQ439_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f11128])).
% 106.75/14.04 fof(f11734,definition,(
% 106.75/14.04 sQ444_spl <=> ('0'=s(sK2_skl('0',sK33_skl,'0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ444_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f11735,plain,(
% 106.75/14.04 '0'=s(sK2_skl('0',sK33_skl,'0'))|~sQ444_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f11734])).
% 106.75/14.04 fof(f11739,definition,(
% 106.75/14.04 sQ445_spl <=> ('0'=s(sK4_skl('0',sK33_skl,'0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ445_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f11740,plain,(
% 106.75/14.04 '0'=s(sK4_skl('0',sK33_skl,'0'))|~sQ445_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f11739])).
% 106.75/14.04 fof(f11817,plain,(
% 106.75/14.04 $false|~sQ2_spl),
% 106.75/14.04 inference(backward_subsumption_resolution,[status(thm)],[f301,f8992])).
% 106.75/14.04 fof(f11821,plain,(
% 106.75/14.04 ~sQ2_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f11817])).
% 106.75/14.04 fof(f12174,plain,(
% 106.75/14.04 ![X0]: (times_terminates(sK32_skl,sK33_skl,X0)|~sQ4_spl|~sQ5_spl)),
% 106.75/14.04 inference(resolution,[status(thm)],[f353,f357])).
% 106.75/14.04 fof(f13597,definition,(
% 106.75/14.04 sQ472_spl <=> ('@+'('0',sK35_skl)='0')),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ472_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f13598,plain,(
% 106.75/14.04 '@+'('0',sK35_skl)='0'|~sQ472_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f13597])).
% 106.75/14.04 fof(f13604,definition,(
% 106.75/14.04 sQ474_spl <=> (s(sK4_skl(sK37_skl,sK31_skl,sK35_skl))='0')),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ474_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f13605,plain,(
% 106.75/14.04 s(sK4_skl(sK37_skl,sK31_skl,sK35_skl))='0'|~sQ474_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f13604])).
% 106.75/14.04 fof(f13611,definition,(
% 106.75/14.04 sQ476_spl <=> (s(sK27_skl(sK35_skl))='0')),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ476_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f13612,plain,(
% 106.75/14.04 s(sK27_skl(sK35_skl))='0'|~sQ476_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f13611])).
% 106.75/14.04 fof(f13618,definition,(
% 106.75/14.04 sQ478_spl <=> (sK30_skl(sK35_skl,'0')='0')),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ478_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f13619,plain,(
% 106.75/14.04 sK30_skl(sK35_skl,'0')='0'|~sQ478_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f13618])).
% 106.75/14.04 fof(f13927,plain,(
% 106.75/14.04 $false|~sQ14_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f8742,f372])).
% 106.75/14.04 fof(f13928,plain,(
% 106.75/14.04 ~sQ14_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f13927])).
% 106.75/14.04 fof(f15153,definition,(
% 106.75/14.04 sQ553_spl <=> (s(sK28_skl(sK35_skl))='0')),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ553_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f15154,plain,(
% 106.75/14.04 s(sK28_skl(sK35_skl))='0'|~sQ553_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f15153])).
% 106.75/14.04 fof(f16204,definition,(
% 106.75/14.04 sQ595_spl <=> ('0'=s(sK11_skl(sK34_skl,sK6_skl(sK34_skl,'0',sK31_skl),'0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ595_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f16205,plain,(
% 106.75/14.04 '0'=s(sK11_skl(sK34_skl,sK6_skl(sK34_skl,'0',sK31_skl),'0'))|~sQ595_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f16204])).
% 106.75/14.04 fof(f17808,definition,(
% 106.75/14.04 ![X0]: (sQ657_spl <=> ('0'=s(sK2_skl('0',X0,'0'))))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ657_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f17809,plain,(
% 106.75/14.04 ![X0]: ('0'=s(sK2_skl('0',X0,'0'))|~sQ657_spl)),
% 106.75/14.04 inference(component_clause,[status(thm)],[f17808])).
% 106.75/14.04 fof(f17983,definition,(
% 106.75/14.04 ![X0]: (sQ669_spl <=> ('0'=s(sK9_skl(X0,X0,'0'))))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ669_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f17984,plain,(
% 106.75/14.04 ![X0]: ('0'=s(sK9_skl(X0,X0,'0'))|~sQ669_spl)),
% 106.75/14.04 inference(component_clause,[status(thm)],[f17983])).
% 106.75/14.04 fof(f18064,definition,(
% 106.75/14.04 sQ676_spl <=> (sK33_skl=sK33_skl)),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ676_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f18066,plain,(
% 106.75/14.04 ~sK33_skl=sK33_skl|sQ676_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f18064])).
% 106.75/14.04 fof(f18291,definition,(
% 106.75/14.04 sQ696_spl <=> (gr(s(s(sK35_skl))))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ696_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f18293,plain,(
% 106.75/14.04 ~gr(s(s(sK35_skl)))|sQ696_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f18291])).
% 106.75/14.04 fof(f18319,plain,(
% 106.75/14.04 $false|sQ696_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f18293,f5202])).
% 106.75/14.04 fof(f18320,plain,(
% 106.75/14.04 sQ696_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f18319])).
% 106.75/14.04 fof(f18800,definition,(
% 106.75/14.04 sQ720_spl <=> ('0'=s(sK22_skl(sK33_skl,'0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ720_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f18801,plain,(
% 106.75/14.04 '0'=s(sK22_skl(sK33_skl,'0'))|~sQ720_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f18800])).
% 106.75/14.04 fof(f18807,definition,(
% 106.75/14.04 sQ722_spl <=> ('0'=s(sK22_skl(sK31_skl,'0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ722_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f18808,plain,(
% 106.75/14.04 '0'=s(sK22_skl(sK31_skl,'0'))|~sQ722_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f18807])).
% 106.75/14.04 fof(f18814,definition,(
% 106.75/14.04 sQ724_spl <=> ('0'=s(sK22_skl(sK35_skl,'0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ724_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f18815,plain,(
% 106.75/14.04 '0'=s(sK22_skl(sK35_skl,'0'))|~sQ724_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f18814])).
% 106.75/14.04 fof(f18822,plain,(
% 106.75/14.04 $false|~sQ720_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f18801,f60])).
% 106.75/14.04 fof(f18823,plain,(
% 106.75/14.04 ~sQ720_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f18822])).
% 106.75/14.04 fof(f18824,plain,(
% 106.75/14.04 $false|~sQ722_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f18808,f60])).
% 106.75/14.04 fof(f18825,plain,(
% 106.75/14.04 ~sQ722_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f18824])).
% 106.75/14.04 fof(f18826,plain,(
% 106.75/14.04 $false|~sQ724_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f18815,f60])).
% 106.75/14.04 fof(f18827,plain,(
% 106.75/14.04 ~sQ724_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f18826])).
% 106.75/14.04 fof(f18964,definition,(
% 106.75/14.04 ![X0]: (sQ744_spl <=> ('0'=s(sK22_skl(s(X0),'0'))))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ744_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f18965,plain,(
% 106.75/14.04 ![X0]: ('0'=s(sK22_skl(s(X0),'0'))|~sQ744_spl)),
% 106.75/14.04 inference(component_clause,[status(thm)],[f18964])).
% 106.75/14.04 fof(f19427,plain,(
% 106.75/14.04 $false|~sQ553_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f15154,f60])).
% 106.75/14.04 fof(f19428,plain,(
% 106.75/14.04 ~sQ553_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f19427])).
% 106.75/14.04 fof(f19429,plain,(
% 106.75/14.04 sK35_skl='0'|~sQ472_spl),
% 106.75/14.04 inference(forward_demodulation,[status(thm)],[f259,f13598])).
% 106.75/14.04 fof(f19430,plain,(
% 106.75/14.04 $false|~sQ472_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f19429,f568])).
% 106.75/14.04 fof(f19431,plain,(
% 106.75/14.04 ~sQ472_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f19430])).
% 106.75/14.04 fof(f19432,plain,(
% 106.75/14.04 $false|~sQ476_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f13612,f60])).
% 106.75/14.04 fof(f19433,plain,(
% 106.75/14.04 ~sQ476_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f19432])).
% 106.75/14.04 fof(f19434,plain,(
% 106.75/14.04 sK35_skl='0'|~sQ478_spl),
% 106.75/14.04 inference(forward_demodulation,[status(thm)],[f10080,f13619])).
% 106.75/14.04 fof(f19435,plain,(
% 106.75/14.04 $false|~sQ478_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f19434,f568])).
% 106.75/14.04 fof(f19436,plain,(
% 106.75/14.04 ~sQ478_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f19435])).
% 106.75/14.04 fof(f19437,plain,(
% 106.75/14.04 $false|~sQ474_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f13605,f60])).
% 106.75/14.04 fof(f19438,plain,(
% 106.75/14.04 ~sQ474_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f19437])).
% 106.75/14.04 fof(f19991,definition,(
% 106.75/14.04 sQ843_spl <=> (s(s(sK33_skl))='0')),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ843_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f19992,plain,(
% 106.75/14.04 s(s(sK33_skl))='0'|~sQ843_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f19991])).
% 106.75/14.04 fof(f20013,plain,(
% 106.75/14.04 $false|~sQ843_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f19992,f60])).
% 106.75/14.04 fof(f20014,plain,(
% 106.75/14.04 ~sQ843_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f20013])).
% 106.75/14.04 fof(f21565,definition,(
% 106.75/14.04 sQ912_spl <=> ('0'=s(sK11_skl(sK37_skl,sK6_skl(sK37_skl,'0',sK35_skl),'0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ912_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f21566,plain,(
% 106.75/14.04 '0'=s(sK11_skl(sK37_skl,sK6_skl(sK37_skl,'0',sK35_skl),'0'))|~sQ912_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f21565])).
% 106.75/14.04 fof(f21927,definition,(
% 106.75/14.04 sQ920_spl <=> (s(sK4_skl(sK37_skl,sK36_skl,sK35_skl))='0')),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ920_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f21928,plain,(
% 106.75/14.04 s(sK4_skl(sK37_skl,sK36_skl,sK35_skl))='0'|~sQ920_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f21927])).
% 106.75/14.04 fof(f21967,plain,(
% 106.75/14.04 $false|~sQ920_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f21928,f60])).
% 106.75/14.04 fof(f21968,plain,(
% 106.75/14.04 ~sQ920_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f21967])).
% 106.75/14.04 fof(f22225,definition,(
% 106.75/14.04 sQ929_spl <=> (s(sK4_skl(sK37_skl,'0',sK35_skl))='0')),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ929_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f22226,plain,(
% 106.75/14.04 s(sK4_skl(sK37_skl,'0',sK35_skl))='0'|~sQ929_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f22225])).
% 106.75/14.04 fof(f22271,plain,(
% 106.75/14.04 $false|~sQ929_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f22226,f60])).
% 106.75/14.04 fof(f22272,plain,(
% 106.75/14.04 ~sQ929_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f22271])).
% 106.75/14.04 fof(f23649,plain,(
% 106.75/14.04 ~nat_succeeds('@+'(sK35_skl,sK35_skl))|~sQ158_spl),
% 106.75/14.04 inference(resolution,[status(thm)],[f2414,f85])).
% 106.75/14.04 fof(f23652,plain,(
% 106.75/14.04 $false|~sQ158_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f23649,f4872])).
% 106.75/14.04 fof(f23653,plain,(
% 106.75/14.04 ~sQ158_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f23652])).
% 106.75/14.04 fof(f24858,plain,(
% 106.75/14.04 $false|~sQ912_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f21566,f60])).
% 106.75/14.04 fof(f24859,plain,(
% 106.75/14.04 ~sQ912_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f24858])).
% 106.75/14.04 fof(f24896,plain,(
% 106.75/14.04 $false|~sQ744_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f18965,f60])).
% 106.75/14.04 fof(f24897,plain,(
% 106.75/14.04 ~sQ744_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f24896])).
% 106.75/14.04 fof(f24923,plain,(
% 106.75/14.04 $false|sQ676_spl),
% 106.75/14.04 inference(trivial_equality_resolution,[status(thm)],[f18066])).
% 106.75/14.04 fof(f24924,plain,(
% 106.75/14.04 sQ676_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f24923])).
% 106.75/14.04 fof(f24925,plain,(
% 106.75/14.04 $false|~sQ669_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f17984,f60])).
% 106.75/14.04 fof(f24926,plain,(
% 106.75/14.04 ~sQ669_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f24925])).
% 106.75/14.04 fof(f24927,plain,(
% 106.75/14.04 $false|~sQ657_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f17809,f60])).
% 106.75/14.04 fof(f24928,plain,(
% 106.75/14.04 ~sQ657_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f24927])).
% 106.75/14.04 fof(f27069,definition,(
% 106.75/14.04 sQ1023_spl <=> ('@<_terminates'('0','0'))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1023_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f27071,plain,(
% 106.75/14.04 ~'@<_terminates'('0','0')|sQ1023_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f27069])).
% 106.75/14.04 fof(f27308,definition,(
% 106.75/14.04 sQ1060_spl <=> ('@<_fails'('0',sK35_skl))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1060_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f27309,plain,(
% 106.75/14.04 '@<_fails'('0',sK35_skl)|~sQ1060_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f27308])).
% 106.75/14.04 fof(f27317,definition,(
% 106.75/14.04 sQ1062_spl <=> ('@=<_fails'('0','0'))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1062_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f27318,plain,(
% 106.75/14.04 '@=<_fails'('0','0')|~sQ1062_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f27317])).
% 106.75/14.04 fof(f27329,definition,(
% 106.75/14.04 sQ1064_spl <=> ('@=<_fails'('0',sK35_skl))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1064_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f27330,plain,(
% 106.75/14.04 '@=<_fails'('0',sK35_skl)|~sQ1064_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f27329])).
% 106.75/14.04 fof(f27340,definition,(
% 106.75/14.04 sQ1065_spl <=> ('0'=s(sK23_skl('0','0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1065_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f27341,plain,(
% 106.75/14.04 '0'=s(sK23_skl('0','0'))|~sQ1065_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f27340])).
% 106.75/14.04 fof(f27344,definition,(
% 106.75/14.04 sQ1066_spl <=> ('0'=s(sK24_skl('0','0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1066_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f27345,plain,(
% 106.75/14.04 '0'=s(sK24_skl('0','0'))|~sQ1066_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f27344])).
% 106.75/14.04 fof(f27348,definition,(
% 106.75/14.04 sQ1067_spl <=> ('0'=s(sK22_skl('0','0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1067_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f27349,plain,(
% 106.75/14.04 '0'=s(sK22_skl('0','0'))|~sQ1067_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f27348])).
% 106.75/14.04 fof(f27358,definition,(
% 106.75/14.04 sQ1069_spl <=> ('0'=s(sK21_skl('0','0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1069_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f27359,plain,(
% 106.75/14.04 '0'=s(sK21_skl('0','0'))|~sQ1069_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f27358])).
% 106.75/14.04 fof(f27363,plain,(
% 106.75/14.04 $false|~sQ1065_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f27341,f60])).
% 106.75/14.04 fof(f27364,plain,(
% 106.75/14.04 ~sQ1065_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f27363])).
% 106.75/14.04 fof(f27365,plain,(
% 106.75/14.04 $false|~sQ1067_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f27349,f60])).
% 106.75/14.04 fof(f27366,plain,(
% 106.75/14.04 ~sQ1067_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f27365])).
% 106.75/14.04 fof(f27367,plain,(
% 106.75/14.04 $false|~sQ1066_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f27345,f60])).
% 106.75/14.04 fof(f27368,plain,(
% 106.75/14.04 ~sQ1066_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f27367])).
% 106.75/14.04 fof(f27369,plain,(
% 106.75/14.04 $false|~sQ1069_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f27359,f60])).
% 106.75/14.04 fof(f27370,plain,(
% 106.75/14.04 ~sQ1069_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f27369])).
% 106.75/14.04 fof(f27380,plain,(
% 106.75/14.04 $false|~sQ595_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f16205,f60])).
% 106.75/14.04 fof(f27381,plain,(
% 106.75/14.04 ~sQ595_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f27380])).
% 106.75/14.04 fof(f27390,plain,(
% 106.75/14.04 $false|~sQ445_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f11740,f60])).
% 106.75/14.04 fof(f27391,plain,(
% 106.75/14.04 ~sQ445_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f27390])).
% 106.75/14.04 fof(f27392,plain,(
% 106.75/14.04 $false|~sQ444_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f11735,f60])).
% 106.75/14.04 fof(f27393,plain,(
% 106.75/14.04 ~sQ444_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f27392])).
% 106.75/14.04 fof(f27394,plain,(
% 106.75/14.04 $false|~sQ439_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f11129,f60])).
% 106.75/14.04 fof(f27395,plain,(
% 106.75/14.04 ~sQ439_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f27394])).
% 106.75/14.04 fof(f27406,plain,(
% 106.75/14.04 ~sQ215_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f3560])).
% 106.75/14.04 fof(f27791,plain,(
% 106.75/14.04 ~times_succeeds('0',sK33_skl,'0')|~sQ437_spl),
% 106.75/14.04 inference(resolution,[status(thm)],[f10965,f69])).
% 106.75/14.04 fof(f27793,plain,(
% 106.75/14.04 $false|~sQ437_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f27791,f764])).
% 106.75/14.04 fof(f27794,plain,(
% 106.75/14.04 ~sQ437_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f27793])).
% 106.75/14.04 fof(f28263,definition,(
% 106.75/14.04 ![X0]: (sQ1083_spl <=> (~X0=sK36_skl))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1083_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f28264,plain,(
% 106.75/14.04 ![X0]: (~X0=sK36_skl|~sQ1083_spl)),
% 106.75/14.04 inference(component_clause,[status(thm)],[f28263])).
% 106.75/14.04 fof(f28275,plain,(
% 106.75/14.04 $false|~sQ1083_spl),
% 106.75/14.04 inference(backward_subsumption_resolution,[status(thm)],[f738,f28264])).
% 106.75/14.04 fof(f28280,plain,(
% 106.75/14.04 ~sQ1083_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f28275])).
% 106.75/14.04 fof(f28518,plain,(
% 106.75/14.04 ~'@<_succeeds'('0',sK35_skl)|~sQ1060_spl),
% 106.75/14.04 inference(resolution,[status(thm)],[f27309,f81])).
% 106.75/14.04 fof(f28519,definition,(
% 106.75/14.04 ![X0]: (sQ1091_spl <=> (~sK35_skl=s(X0)))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1091_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f28520,plain,(
% 106.75/14.04 ![X0]: (~sK35_skl=s(X0)|~sQ1091_spl)),
% 106.75/14.04 inference(component_clause,[status(thm)],[f28519])).
% 106.75/14.04 fof(f28523,plain,(
% 106.75/14.04 $false|~sQ1060_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f28518,f986])).
% 106.75/14.04 fof(f28524,plain,(
% 106.75/14.04 ~sQ1060_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f28523])).
% 106.75/14.04 fof(f28525,plain,(
% 106.75/14.04 $false|~sQ1091_spl),
% 106.75/14.04 inference(backward_subsumption_resolution,[status(thm)],[f8273,f28520])).
% 106.75/14.04 fof(f28530,plain,(
% 106.75/14.04 ~sQ1091_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f28525])).
% 106.75/14.04 fof(f28532,plain,(
% 106.75/14.04 ~'0'='0'|~sQ1062_spl),
% 106.75/14.04 inference(resolution,[status(thm)],[f27318,f153])).
% 106.75/14.04 fof(f28534,plain,(
% 106.75/14.04 $false|~sQ1062_spl),
% 106.75/14.04 inference(trivial_equality_resolution,[status(thm)],[f28532])).
% 106.75/14.04 fof(f28535,plain,(
% 106.75/14.04 ~sQ1062_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f28534])).
% 106.75/14.04 fof(f28550,plain,(
% 106.75/14.04 ~'0'='0'|~sQ1064_spl),
% 106.75/14.04 inference(resolution,[status(thm)],[f27330,f153])).
% 106.75/14.04 fof(f28552,plain,(
% 106.75/14.04 $false|~sQ1064_spl),
% 106.75/14.04 inference(trivial_equality_resolution,[status(thm)],[f28550])).
% 106.75/14.04 fof(f28553,plain,(
% 106.75/14.04 ~sQ1064_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f28552])).
% 106.75/14.04 fof(f29211,definition,(
% 106.75/14.04 sQ1101_spl <=> ('0'=s(sK22_skl(sK36_skl,'0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1101_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f29212,plain,(
% 106.75/14.04 '0'=s(sK22_skl(sK36_skl,'0'))|~sQ1101_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f29211])).
% 106.75/14.04 fof(f29218,plain,(
% 106.75/14.04 $false|~sQ1101_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f29212,f60])).
% 106.75/14.04 fof(f29219,plain,(
% 106.75/14.04 ~sQ1101_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f29218])).
% 106.75/14.04 fof(f29881,plain,(
% 106.75/14.04 '0'=s(sK26_skl('0','0'))|sQ1023_spl),
% 106.75/14.04 inference(resolution,[status(thm)],[f27071,f189])).
% 106.75/14.04 fof(f29883,plain,(
% 106.75/14.04 $false|sQ1023_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f29881,f60])).
% 106.75/14.04 fof(f29884,plain,(
% 106.75/14.04 sQ1023_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f29883])).
% 106.75/14.04 fof(f30575,definition,(
% 106.75/14.04 sQ1145_spl <=> ('0'=s(sK25_skl(sK35_skl,'0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1145_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f30576,plain,(
% 106.75/14.04 '0'=s(sK25_skl(sK35_skl,'0'))|~sQ1145_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f30575])).
% 106.75/14.04 fof(f30579,plain,(
% 106.75/14.04 $false|~sQ1145_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f30576,f60])).
% 106.75/14.04 fof(f30580,plain,(
% 106.75/14.04 ~sQ1145_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f30579])).
% 106.75/14.04 fof(f30726,definition,(
% 106.75/14.04 sQ1152_spl <=> ('0'=s(sK18_skl('0','0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1152_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f30727,plain,(
% 106.75/14.04 '0'=s(sK18_skl('0','0'))|~sQ1152_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f30726])).
% 106.75/14.04 fof(f30730,definition,(
% 106.75/14.04 sQ1153_spl <=> ('0'=s(sK17_skl('0','0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1153_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f30731,plain,(
% 106.75/14.04 '0'=s(sK17_skl('0','0'))|~sQ1153_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f30730])).
% 106.75/14.04 fof(f30742,definition,(
% 106.75/14.04 sQ1156_spl <=> ('0'=s(sK16_skl('0','0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1156_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f30743,plain,(
% 106.75/14.04 '0'=s(sK16_skl('0','0'))|~sQ1156_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f30742])).
% 106.75/14.04 fof(f30746,definition,(
% 106.75/14.04 sQ1157_spl <=> ('0'=s(sK15_skl('0','0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1157_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f30747,plain,(
% 106.75/14.04 '0'=s(sK15_skl('0','0'))|~sQ1157_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f30746])).
% 106.75/14.04 fof(f30750,plain,(
% 106.75/14.04 $false|~sQ1157_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f30747,f60])).
% 106.75/14.04 fof(f30751,plain,(
% 106.75/14.04 ~sQ1157_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f30750])).
% 106.75/14.04 fof(f30752,plain,(
% 106.75/14.04 $false|~sQ1156_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f30743,f60])).
% 106.75/14.04 fof(f30753,plain,(
% 106.75/14.04 ~sQ1156_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f30752])).
% 106.75/14.04 fof(f30754,plain,(
% 106.75/14.04 $false|~sQ1153_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f30731,f60])).
% 106.75/14.04 fof(f30755,plain,(
% 106.75/14.04 ~sQ1153_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f30754])).
% 106.75/14.04 fof(f30756,plain,(
% 106.75/14.04 $false|~sQ1152_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f30727,f60])).
% 106.75/14.04 fof(f30757,plain,(
% 106.75/14.04 ~sQ1152_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f30756])).
% 106.75/14.04 fof(f30894,definition,(
% 106.75/14.04 sQ1165_spl <=> ('0'=s(sK17_skl(sK35_skl,'0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1165_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f30895,plain,(
% 106.75/14.04 '0'=s(sK17_skl(sK35_skl,'0'))|~sQ1165_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f30894])).
% 106.75/14.04 fof(f30910,definition,(
% 106.75/14.04 sQ1169_spl <=> ('0'=s(sK15_skl(sK35_skl,'0')))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1169_spl])],[split_symbol_definition])).
% 106.75/14.04 fof(f30911,plain,(
% 106.75/14.04 '0'=s(sK15_skl(sK35_skl,'0'))|~sQ1169_spl),
% 106.75/14.04 inference(component_clause,[status(thm)],[f30910])).
% 106.75/14.04 fof(f30914,plain,(
% 106.75/14.04 $false|~sQ1169_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f30911,f60])).
% 106.75/14.04 fof(f30915,plain,(
% 106.75/14.04 ~sQ1169_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f30914])).
% 106.75/14.04 fof(f30916,plain,(
% 106.75/14.04 $false|~sQ1165_spl),
% 106.75/14.04 inference(forward_subsumption_resolution,[status(thm)],[f30895,f60])).
% 106.75/14.04 fof(f30917,plain,(
% 106.75/14.04 ~sQ1165_spl),
% 106.75/14.04 inference(contradiction_clause,[status(thm)],[f30916])).
% 106.75/14.04 fof(f31517,definition,(
% 106.75/14.04 sQ1184_spl <=> (plus_terminates(sK33_skl,sK6_skl(sK34_skl,sK33_skl,sK31_skl),sK34_skl))),
% 106.75/14.04 introduced(definition,[new_symbols(definition,[sQ1184_spl])],[split_symbol_definition])).
% 107.49/14.04 fof(f31519,plain,(
% 107.49/14.04 ~plus_terminates(sK33_skl,sK6_skl(sK34_skl,sK33_skl,sK31_skl),sK34_skl)|sQ1184_spl),
% 107.49/14.04 inference(component_clause,[status(thm)],[f31517])).
% 107.49/14.04 fof(f31525,plain,(
% 107.49/14.04 $false|~sQ5_spl|sQ1184_spl),
% 107.49/14.04 inference(forward_subsumption_resolution,[status(thm)],[f31519,f6998])).
% 107.49/14.04 fof(f31526,plain,(
% 107.49/14.04 ~sQ5_spl|sQ1184_spl),
% 107.49/14.04 inference(contradiction_clause,[status(thm)],[f31525])).
% 107.49/14.04 fof(f31582,definition,(
% 107.49/14.04 sQ1189_spl <=> (s(sK4_skl(sK34_skl,sK33_skl,sK31_skl))='0')),
% 107.49/14.04 introduced(definition,[new_symbols(definition,[sQ1189_spl])],[split_symbol_definition])).
% 107.49/14.04 fof(f31583,plain,(
% 107.49/14.04 s(sK4_skl(sK34_skl,sK33_skl,sK31_skl))='0'|~sQ1189_spl),
% 107.49/14.04 inference(component_clause,[status(thm)],[f31582])).
% 107.49/14.04 fof(f31606,plain,(
% 107.49/14.04 $false|~sQ1189_spl),
% 107.49/14.04 inference(forward_subsumption_resolution,[status(thm)],[f31583,f60])).
% 107.49/14.04 fof(f31607,plain,(
% 107.49/14.04 ~sQ1189_spl),
% 107.49/14.04 inference(contradiction_clause,[status(thm)],[f31606])).
% 107.49/14.04 fof(f32789,definition,(
% 107.49/14.04 sQ1267_spl <=> ('@=<_fails'('0',sK33_skl))),
% 107.49/14.04 introduced(definition,[new_symbols(definition,[sQ1267_spl])],[split_symbol_definition])).
% 107.49/14.06 fof(f32790,plain,(
% 107.49/14.06 '@=<_fails'('0',sK33_skl)|~sQ1267_spl),
% 107.49/14.06 inference(component_clause,[status(thm)],[f32789])).
% 107.49/14.06 fof(f32900,plain,(
% 107.49/14.06 ~'0'='0'|~sQ1267_spl),
% 107.49/14.06 inference(resolution,[status(thm)],[f32790,f153])).
% 107.49/14.06 fof(f32902,plain,(
% 107.49/14.06 $false|~sQ1267_spl),
% 107.49/14.06 inference(trivial_equality_resolution,[status(thm)],[f32900])).
% 107.49/14.06 fof(f32903,plain,(
% 107.49/14.06 ~sQ1267_spl),
% 107.49/14.06 inference(contradiction_clause,[status(thm)],[f32902])).
% 107.49/14.06 fof(f32946,definition,(
% 107.49/14.06 sQ1285_spl <=> ('0'=s(sK17_skl(sK33_skl,'0')))),
% 107.49/14.06 introduced(definition,[new_symbols(definition,[sQ1285_spl])],[split_symbol_definition])).
% 107.49/14.06 fof(f32947,plain,(
% 107.49/14.06 '0'=s(sK17_skl(sK33_skl,'0'))|~sQ1285_spl),
% 107.49/14.06 inference(component_clause,[status(thm)],[f32946])).
% 107.49/14.06 fof(f32962,definition,(
% 107.49/14.06 sQ1289_spl <=> ('0'=s(sK15_skl(sK33_skl,'0')))),
% 107.49/14.06 introduced(definition,[new_symbols(definition,[sQ1289_spl])],[split_symbol_definition])).
% 107.49/14.06 fof(f32963,plain,(
% 107.49/14.06 '0'=s(sK15_skl(sK33_skl,'0'))|~sQ1289_spl),
% 107.49/14.06 inference(component_clause,[status(thm)],[f32962])).
% 107.49/14.11 fof(f32966,plain,(
% 107.49/14.11 $false|~sQ1289_spl),
% 107.49/14.11 inference(forward_subsumption_resolution,[status(thm)],[f32963,f60])).
% 107.49/14.11 fof(f32967,plain,(
% 107.49/14.11 ~sQ1289_spl),
% 107.49/14.11 inference(contradiction_clause,[status(thm)],[f32966])).
% 107.49/14.11 fof(f32968,plain,(
% 107.49/14.11 $false|~sQ1285_spl),
% 107.49/14.11 inference(forward_subsumption_resolution,[status(thm)],[f32947,f60])).
% 107.49/14.11 fof(f32969,plain,(
% 107.49/14.11 ~sQ1285_spl),
% 107.49/14.11 inference(contradiction_clause,[status(thm)],[f32968])).
% 107.49/14.11 fof(f33623,definition,(
% 107.49/14.11 sQ1305_spl <=> (s(sK32_skl)='0')),
% 107.49/14.11 introduced(definition,[new_symbols(definition,[sQ1305_spl])],[split_symbol_definition])).
% 107.49/14.11 fof(f33624,plain,(
% 107.49/14.11 s(sK32_skl)='0'|~sQ1305_spl),
% 107.49/14.11 inference(component_clause,[status(thm)],[f33623])).
% 107.49/14.11 fof(f33637,plain,(
% 107.49/14.11 $false|~sQ1305_spl),
% 107.49/14.11 inference(forward_subsumption_resolution,[status(thm)],[f33624,f60])).
% 107.49/14.11 fof(f33638,plain,(
% 107.49/14.11 ~sQ1305_spl),
% 107.49/14.11 inference(contradiction_clause,[status(thm)],[f33637])).
% 107.49/14.11 fof(f34881,definition,(
% 107.49/14.11 sQ1316_spl <=> ('0'=s(sK22_skl(sK32_skl,'0')))),
% 107.49/14.11 introduced(definition,[new_symbols(definition,[sQ1316_spl])],[split_symbol_definition])).
% 107.49/14.11 fof(f34882,plain,(
% 107.49/14.11 '0'=s(sK22_skl(sK32_skl,'0'))|~sQ1316_spl),
% 107.49/14.11 inference(component_clause,[status(thm)],[f34881])).
% 107.49/14.11 fof(f34890,plain,(
% 107.49/14.11 $false|~sQ1316_spl),
% 107.49/14.11 inference(forward_subsumption_resolution,[status(thm)],[f34882,f60])).
% 107.49/14.11 fof(f34891,plain,(
% 107.49/14.11 ~sQ1316_spl),
% 107.49/14.11 inference(contradiction_clause,[status(thm)],[f34890])).
% 107.49/14.11 fof(f35708,plain,(
% 107.49/14.11 times_terminates(sK31_skl,sK33_skl,sK34_skl)|~times_terminates(sK32_skl,sK33_skl,sK5_skl(sK34_skl,sK33_skl,sK31_skl))|~plus_terminates(sK33_skl,sK6_skl(sK34_skl,sK33_skl,sK31_skl),sK34_skl)|sQ6_spl|~sQ0_spl),
% 107.49/14.11 inference(paramodulation,[status(thm)],[f7450,f114])).
% 107.49/14.11 fof(f35719,definition,(
% 107.49/14.11 sQ1356_spl <=> (times_terminates(sK32_skl,sK33_skl,sK5_skl(sK34_skl,sK33_skl,sK31_skl)))),
% 107.49/14.11 introduced(definition,[new_symbols(definition,[sQ1356_spl])],[split_symbol_definition])).
% 107.49/14.11 fof(f35721,plain,(
% 107.49/14.11 ~times_terminates(sK32_skl,sK33_skl,sK5_skl(sK34_skl,sK33_skl,sK31_skl))|sQ1356_spl),
% 107.49/14.11 inference(component_clause,[status(thm)],[f35719])).
% 107.49/14.11 fof(f35722,plain,(
% 107.49/14.11 sQ6_spl|~sQ1356_spl|~sQ1184_spl|~sQ0_spl),
% 107.49/14.11 inference(split_clause,[status(thm)],[f35708,f360,f35719,f31517,f338])).
% 107.49/14.11 fof(f35724,plain,(
% 107.49/14.11 $false|~sQ4_spl|~sQ5_spl|sQ1356_spl),
% 107.49/14.11 inference(forward_subsumption_resolution,[status(thm)],[f35721,f12174])).
% 107.49/14.11 fof(f35725,plain,(
% 107.49/14.11 ~sQ4_spl|~sQ5_spl|sQ1356_spl),
% 107.49/14.11 inference(contradiction_clause,[status(thm)],[f35724])).
% 107.49/14.11 fof(f35726,plain,(
% 107.49/14.11 $false),
% 107.49/14.11 inference(sat_refutation,[status(thm)],[f347,f355,f359,f363,f2545,f11821,f13928,f18320,f18823,f18825,f18827,f19428,f19431,f19433,f19436,f19438,f20014,f21968,f22272,f23653,f24859,f24897,f24924,f24926,f24928,f27364,f27366,f27368,f27370,f27381,f27391,f27393,f27395,f27406,f27794,f28280,f28524,f28530,f28535,f28553,f29219,f29884,f30580,f30751,f30753,f30755,f30757,f30915,f30917,f31526,f31607,f32903,f32967,f32969,f33638,f34891,f35722,f35725])).
% 107.49/14.11 % SZS output end CNFRefutation for theBenchmark.p
% 15.14/14.14 % Elapsed time: 13.726409 seconds
% 15.14/14.14 % CPU time: 108.150541 seconds
% 15.14/14.14 % Total memory used: 581.997 MB
% 15.14/14.14 % Net memory used: 527.865 MB
%------------------------------------------------------------------------------