MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            f0(x,y,z) -> d()
            f0(0(),y,x) -> f1(x,y,x)
            f1(x,y,z) -> c()
            f1(x,y,z) -> f2(x,y,z)
            f2(x,1(),z) -> f0(x,z,z)
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
            ifTimes(true(),i,x,y,z) -> z
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
            times(x,y) -> timesIter(0(),x,y,0())
            timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4} / {0/0,1/0,c/0,d/0
            ,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0,f1,f2,ge,ifPlus,ifTimes,inc,isZero,p,plus,times
            ,timesIter} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          f0#(x,y,z) -> c_1()
          f0#(0(),y,x) -> c_2(f1#(x,y,x))
          f1#(x,y,z) -> c_3()
          f1#(x,y,z) -> c_4(f2#(x,y,z))
          f2#(x,1(),z) -> c_5(f0#(x,z,z))
          ge#(x,0()) -> c_6()
          ge#(0(),s(y)) -> c_7()
          ge#(s(x),s(y)) -> c_8(ge#(x,y))
          ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
          ifPlus#(true(),x,y) -> c_10(p#(y))
          ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
          ifTimes#(true(),i,x,y,z) -> c_12()
          inc#(x) -> c_13()
          inc#(0()) -> c_14()
          inc#(s(x)) -> c_15(inc#(x))
          isZero#(0()) -> c_16()
          isZero#(s(0())) -> c_17()
          isZero#(s(s(x))) -> c_18(isZero#(s(x)))
          p#(0()) -> c_19()
          p#(s(x)) -> c_20()
          p#(s(s(x))) -> c_21(p#(s(x)))
          plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
          times#(x,y) -> c_23(timesIter#(0(),x,y,0()))
          timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            f0#(x,y,z) -> c_1()
            f0#(0(),y,x) -> c_2(f1#(x,y,x))
            f1#(x,y,z) -> c_3()
            f1#(x,y,z) -> c_4(f2#(x,y,z))
            f2#(x,1(),z) -> c_5(f0#(x,z,z))
            ge#(x,0()) -> c_6()
            ge#(0(),s(y)) -> c_7()
            ge#(s(x),s(y)) -> c_8(ge#(x,y))
            ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
            ifPlus#(true(),x,y) -> c_10(p#(y))
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            ifTimes#(true(),i,x,y,z) -> c_12()
            inc#(x) -> c_13()
            inc#(0()) -> c_14()
            inc#(s(x)) -> c_15(inc#(x))
            isZero#(0()) -> c_16()
            isZero#(s(0())) -> c_17()
            isZero#(s(s(x))) -> c_18(isZero#(s(x)))
            p#(0()) -> c_19()
            p#(s(x)) -> c_20()
            p#(s(s(x))) -> c_21(p#(s(x)))
            plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
            times#(x,y) -> c_23(timesIter#(0(),x,y,0()))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
        - Weak TRS:
            f0(x,y,z) -> d()
            f0(0(),y,x) -> f1(x,y,x)
            f1(x,y,z) -> c()
            f1(x,y,z) -> f2(x,y,z)
            f2(x,1(),z) -> f0(x,z,z)
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
            ifTimes(true(),i,x,y,z) -> z
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
            times(x,y) -> timesIter(0(),x,y,0())
            timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          ge(x,0()) -> true()
          ge(0(),s(y)) -> false()
          ge(s(x),s(y)) -> ge(x,y)
          ifPlus(false(),x,y) -> plus(p(x),y)
          ifPlus(true(),x,y) -> p(y)
          inc(x) -> s(x)
          inc(0()) -> s(0())
          inc(s(x)) -> s(inc(x))
          isZero(0()) -> true()
          isZero(s(0())) -> false()
          isZero(s(s(x))) -> isZero(s(x))
          p(0()) -> 0()
          p(s(x)) -> x
          p(s(s(x))) -> s(p(s(x)))
          plus(x,y) -> ifPlus(isZero(x),x,inc(y))
          f0#(x,y,z) -> c_1()
          f0#(0(),y,x) -> c_2(f1#(x,y,x))
          f1#(x,y,z) -> c_3()
          f1#(x,y,z) -> c_4(f2#(x,y,z))
          f2#(x,1(),z) -> c_5(f0#(x,z,z))
          ge#(x,0()) -> c_6()
          ge#(0(),s(y)) -> c_7()
          ge#(s(x),s(y)) -> c_8(ge#(x,y))
          ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
          ifPlus#(true(),x,y) -> c_10(p#(y))
          ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
          ifTimes#(true(),i,x,y,z) -> c_12()
          inc#(x) -> c_13()
          inc#(0()) -> c_14()
          inc#(s(x)) -> c_15(inc#(x))
          isZero#(0()) -> c_16()
          isZero#(s(0())) -> c_17()
          isZero#(s(s(x))) -> c_18(isZero#(s(x)))
          p#(0()) -> c_19()
          p#(s(x)) -> c_20()
          p#(s(s(x))) -> c_21(p#(s(x)))
          plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
          times#(x,y) -> c_23(timesIter#(0(),x,y,0()))
          timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            f0#(x,y,z) -> c_1()
            f0#(0(),y,x) -> c_2(f1#(x,y,x))
            f1#(x,y,z) -> c_3()
            f1#(x,y,z) -> c_4(f2#(x,y,z))
            f2#(x,1(),z) -> c_5(f0#(x,z,z))
            ge#(x,0()) -> c_6()
            ge#(0(),s(y)) -> c_7()
            ge#(s(x),s(y)) -> c_8(ge#(x,y))
            ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
            ifPlus#(true(),x,y) -> c_10(p#(y))
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            ifTimes#(true(),i,x,y,z) -> c_12()
            inc#(x) -> c_13()
            inc#(0()) -> c_14()
            inc#(s(x)) -> c_15(inc#(x))
            isZero#(0()) -> c_16()
            isZero#(s(0())) -> c_17()
            isZero#(s(s(x))) -> c_18(isZero#(s(x)))
            p#(0()) -> c_19()
            p#(s(x)) -> c_20()
            p#(s(s(x))) -> c_21(p#(s(x)))
            plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
            times#(x,y) -> c_23(timesIter#(0(),x,y,0()))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,3,6,7,12,13,14,16,17,19,20}
        by application of
          Pre({1,3,6,7,12,13,14,16,17,19,20}) = {2,5,8,9,10,11,15,18,21,22,24}.
        Here rules are labelled as follows:
          1: f0#(x,y,z) -> c_1()
          2: f0#(0(),y,x) -> c_2(f1#(x,y,x))
          3: f1#(x,y,z) -> c_3()
          4: f1#(x,y,z) -> c_4(f2#(x,y,z))
          5: f2#(x,1(),z) -> c_5(f0#(x,z,z))
          6: ge#(x,0()) -> c_6()
          7: ge#(0(),s(y)) -> c_7()
          8: ge#(s(x),s(y)) -> c_8(ge#(x,y))
          9: ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
          10: ifPlus#(true(),x,y) -> c_10(p#(y))
          11: ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
          12: ifTimes#(true(),i,x,y,z) -> c_12()
          13: inc#(x) -> c_13()
          14: inc#(0()) -> c_14()
          15: inc#(s(x)) -> c_15(inc#(x))
          16: isZero#(0()) -> c_16()
          17: isZero#(s(0())) -> c_17()
          18: isZero#(s(s(x))) -> c_18(isZero#(s(x)))
          19: p#(0()) -> c_19()
          20: p#(s(x)) -> c_20()
          21: p#(s(s(x))) -> c_21(p#(s(x)))
          22: plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
          23: times#(x,y) -> c_23(timesIter#(0(),x,y,0()))
          24: timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            f0#(0(),y,x) -> c_2(f1#(x,y,x))
            f1#(x,y,z) -> c_4(f2#(x,y,z))
            f2#(x,1(),z) -> c_5(f0#(x,z,z))
            ge#(s(x),s(y)) -> c_8(ge#(x,y))
            ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
            ifPlus#(true(),x,y) -> c_10(p#(y))
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            inc#(s(x)) -> c_15(inc#(x))
            isZero#(s(s(x))) -> c_18(isZero#(s(x)))
            p#(s(s(x))) -> c_21(p#(s(x)))
            plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
            times#(x,y) -> c_23(timesIter#(0(),x,y,0()))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
        - Weak DPs:
            f0#(x,y,z) -> c_1()
            f1#(x,y,z) -> c_3()
            ge#(x,0()) -> c_6()
            ge#(0(),s(y)) -> c_7()
            ifTimes#(true(),i,x,y,z) -> c_12()
            inc#(x) -> c_13()
            inc#(0()) -> c_14()
            isZero#(0()) -> c_16()
            isZero#(s(0())) -> c_17()
            p#(0()) -> c_19()
            p#(s(x)) -> c_20()
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:f0#(0(),y,x) -> c_2(f1#(x,y,x))
             -->_1 f1#(x,y,z) -> c_4(f2#(x,y,z)):2
             -->_1 f1#(x,y,z) -> c_3():15
          
          2:S:f1#(x,y,z) -> c_4(f2#(x,y,z))
             -->_1 f2#(x,1(),z) -> c_5(f0#(x,z,z)):3
          
          3:S:f2#(x,1(),z) -> c_5(f0#(x,z,z))
             -->_1 f0#(x,y,z) -> c_1():14
             -->_1 f0#(0(),y,x) -> c_2(f1#(x,y,x)):1
          
          4:S:ge#(s(x),s(y)) -> c_8(ge#(x,y))
             -->_1 ge#(0(),s(y)) -> c_7():17
             -->_1 ge#(x,0()) -> c_6():16
             -->_1 ge#(s(x),s(y)) -> c_8(ge#(x,y)):4
          
          5:S:ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
             -->_1 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):11
             -->_2 p#(s(s(x))) -> c_21(p#(s(x))):10
             -->_2 p#(s(x)) -> c_20():24
             -->_2 p#(0()) -> c_19():23
          
          6:S:ifPlus#(true(),x,y) -> c_10(p#(y))
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):10
             -->_1 p#(s(x)) -> c_20():24
             -->_1 p#(0()) -> c_19():23
          
          7:S:ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
             -->_1 timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x)):13
             -->_3 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):11
             -->_2 inc#(s(x)) -> c_15(inc#(x)):8
             -->_2 inc#(0()) -> c_14():20
             -->_2 inc#(x) -> c_13():19
          
          8:S:inc#(s(x)) -> c_15(inc#(x))
             -->_1 inc#(0()) -> c_14():20
             -->_1 inc#(x) -> c_13():19
             -->_1 inc#(s(x)) -> c_15(inc#(x)):8
          
          9:S:isZero#(s(s(x))) -> c_18(isZero#(s(x)))
             -->_1 isZero#(s(0())) -> c_17():22
             -->_1 isZero#(s(s(x))) -> c_18(isZero#(s(x))):9
          
          10:S:p#(s(s(x))) -> c_21(p#(s(x)))
             -->_1 p#(s(x)) -> c_20():24
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):10
          
          11:S:plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
             -->_2 isZero#(s(0())) -> c_17():22
             -->_2 isZero#(0()) -> c_16():21
             -->_3 inc#(0()) -> c_14():20
             -->_3 inc#(x) -> c_13():19
             -->_2 isZero#(s(s(x))) -> c_18(isZero#(s(x))):9
             -->_3 inc#(s(x)) -> c_15(inc#(x)):8
             -->_1 ifPlus#(true(),x,y) -> c_10(p#(y)):6
             -->_1 ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x)):5
          
          12:S:times#(x,y) -> c_23(timesIter#(0(),x,y,0()))
             -->_1 timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x)):13
          
          13:S:timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
             -->_1 ifTimes#(true(),i,x,y,z) -> c_12():18
             -->_2 ge#(0(),s(y)) -> c_7():17
             -->_2 ge#(x,0()) -> c_6():16
             -->_1 ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y)):7
             -->_2 ge#(s(x),s(y)) -> c_8(ge#(x,y)):4
          
          14:W:f0#(x,y,z) -> c_1()
             
          
          15:W:f1#(x,y,z) -> c_3()
             
          
          16:W:ge#(x,0()) -> c_6()
             
          
          17:W:ge#(0(),s(y)) -> c_7()
             
          
          18:W:ifTimes#(true(),i,x,y,z) -> c_12()
             
          
          19:W:inc#(x) -> c_13()
             
          
          20:W:inc#(0()) -> c_14()
             
          
          21:W:isZero#(0()) -> c_16()
             
          
          22:W:isZero#(s(0())) -> c_17()
             
          
          23:W:p#(0()) -> c_19()
             
          
          24:W:p#(s(x)) -> c_20()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          18: ifTimes#(true(),i,x,y,z) -> c_12()
          23: p#(0()) -> c_19()
          24: p#(s(x)) -> c_20()
          19: inc#(x) -> c_13()
          20: inc#(0()) -> c_14()
          21: isZero#(0()) -> c_16()
          22: isZero#(s(0())) -> c_17()
          16: ge#(x,0()) -> c_6()
          17: ge#(0(),s(y)) -> c_7()
          15: f1#(x,y,z) -> c_3()
          14: f0#(x,y,z) -> c_1()
* Step 5: RemoveHeads MAYBE
    + Considered Problem:
        - Strict DPs:
            f0#(0(),y,x) -> c_2(f1#(x,y,x))
            f1#(x,y,z) -> c_4(f2#(x,y,z))
            f2#(x,1(),z) -> c_5(f0#(x,z,z))
            ge#(s(x),s(y)) -> c_8(ge#(x,y))
            ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
            ifPlus#(true(),x,y) -> c_10(p#(y))
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            inc#(s(x)) -> c_15(inc#(x))
            isZero#(s(s(x))) -> c_18(isZero#(s(x)))
            p#(s(s(x))) -> c_21(p#(s(x)))
            plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
            times#(x,y) -> c_23(timesIter#(0(),x,y,0()))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:f0#(0(),y,x) -> c_2(f1#(x,y,x))
           -->_1 f1#(x,y,z) -> c_4(f2#(x,y,z)):2
        
        2:S:f1#(x,y,z) -> c_4(f2#(x,y,z))
           -->_1 f2#(x,1(),z) -> c_5(f0#(x,z,z)):3
        
        3:S:f2#(x,1(),z) -> c_5(f0#(x,z,z))
           -->_1 f0#(0(),y,x) -> c_2(f1#(x,y,x)):1
        
        4:S:ge#(s(x),s(y)) -> c_8(ge#(x,y))
           -->_1 ge#(s(x),s(y)) -> c_8(ge#(x,y)):4
        
        5:S:ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
           -->_1 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):11
           -->_2 p#(s(s(x))) -> c_21(p#(s(x))):10
        
        6:S:ifPlus#(true(),x,y) -> c_10(p#(y))
           -->_1 p#(s(s(x))) -> c_21(p#(s(x))):10
        
        7:S:ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
           -->_1 timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x)):13
           -->_3 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):11
           -->_2 inc#(s(x)) -> c_15(inc#(x)):8
        
        8:S:inc#(s(x)) -> c_15(inc#(x))
           -->_1 inc#(s(x)) -> c_15(inc#(x)):8
        
        9:S:isZero#(s(s(x))) -> c_18(isZero#(s(x)))
           -->_1 isZero#(s(s(x))) -> c_18(isZero#(s(x))):9
        
        10:S:p#(s(s(x))) -> c_21(p#(s(x)))
           -->_1 p#(s(s(x))) -> c_21(p#(s(x))):10
        
        11:S:plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
           -->_2 isZero#(s(s(x))) -> c_18(isZero#(s(x))):9
           -->_3 inc#(s(x)) -> c_15(inc#(x)):8
           -->_1 ifPlus#(true(),x,y) -> c_10(p#(y)):6
           -->_1 ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x)):5
        
        12:S:times#(x,y) -> c_23(timesIter#(0(),x,y,0()))
           -->_1 timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x)):13
        
        13:S:timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
           -->_1 ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y)):7
           -->_2 ge#(s(x),s(y)) -> c_8(ge#(x,y)):4
        
        
        Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
        
        [(12,times#(x,y) -> c_23(timesIter#(0(),x,y,0())))]
* Step 6: Decompose MAYBE
    + Considered Problem:
        - Strict DPs:
            f0#(0(),y,x) -> c_2(f1#(x,y,x))
            f1#(x,y,z) -> c_4(f2#(x,y,z))
            f2#(x,1(),z) -> c_5(f0#(x,z,z))
            ge#(s(x),s(y)) -> c_8(ge#(x,y))
            ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
            ifPlus#(true(),x,y) -> c_10(p#(y))
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            inc#(s(x)) -> c_15(inc#(x))
            isZero#(s(s(x))) -> c_18(isZero#(s(x)))
            p#(s(s(x))) -> c_21(p#(s(x)))
            plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
    + Details:
        We analyse the complexity of following sub-problems (R) and (S).
        Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
        
        Problem (R)
          - Strict DPs:
              f0#(0(),y,x) -> c_2(f1#(x,y,x))
              f1#(x,y,z) -> c_4(f2#(x,y,z))
              f2#(x,1(),z) -> c_5(f0#(x,z,z))
          - Weak DPs:
              ge#(s(x),s(y)) -> c_8(ge#(x,y))
              ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
              ifPlus#(true(),x,y) -> c_10(p#(y))
              ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
              inc#(s(x)) -> c_15(inc#(x))
              isZero#(s(s(x))) -> c_18(isZero#(s(x)))
              p#(s(s(x))) -> c_21(p#(s(x)))
              plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
              timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
          - Weak TRS:
              ge(x,0()) -> true()
              ge(0(),s(y)) -> false()
              ge(s(x),s(y)) -> ge(x,y)
              ifPlus(false(),x,y) -> plus(p(x),y)
              ifPlus(true(),x,y) -> p(y)
              inc(x) -> s(x)
              inc(0()) -> s(0())
              inc(s(x)) -> s(inc(x))
              isZero(0()) -> true()
              isZero(s(0())) -> false()
              isZero(s(s(x))) -> isZero(s(x))
              p(0()) -> 0()
              p(s(x)) -> x
              p(s(s(x))) -> s(p(s(x)))
              plus(x,y) -> ifPlus(isZero(x),x,inc(y))
          - Signature:
              {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
              ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0
              ,false/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0
              ,c_14/0,c_15/1,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
              ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
        
        Problem (S)
          - Strict DPs:
              ge#(s(x),s(y)) -> c_8(ge#(x,y))
              ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
              ifPlus#(true(),x,y) -> c_10(p#(y))
              ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
              inc#(s(x)) -> c_15(inc#(x))
              isZero#(s(s(x))) -> c_18(isZero#(s(x)))
              p#(s(s(x))) -> c_21(p#(s(x)))
              plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
              timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
          - Weak DPs:
              f0#(0(),y,x) -> c_2(f1#(x,y,x))
              f1#(x,y,z) -> c_4(f2#(x,y,z))
              f2#(x,1(),z) -> c_5(f0#(x,z,z))
          - Weak TRS:
              ge(x,0()) -> true()
              ge(0(),s(y)) -> false()
              ge(s(x),s(y)) -> ge(x,y)
              ifPlus(false(),x,y) -> plus(p(x),y)
              ifPlus(true(),x,y) -> p(y)
              inc(x) -> s(x)
              inc(0()) -> s(0())
              inc(s(x)) -> s(inc(x))
              isZero(0()) -> true()
              isZero(s(0())) -> false()
              isZero(s(s(x))) -> isZero(s(x))
              p(0()) -> 0()
              p(s(x)) -> x
              p(s(s(x))) -> s(p(s(x)))
              plus(x,y) -> ifPlus(isZero(x),x,inc(y))
          - Signature:
              {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
              ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0
              ,false/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0
              ,c_14/0,c_15/1,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
              ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
** Step 6.a:1: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            f0#(0(),y,x) -> c_2(f1#(x,y,x))
            f1#(x,y,z) -> c_4(f2#(x,y,z))
            f2#(x,1(),z) -> c_5(f0#(x,z,z))
        - Weak DPs:
            ge#(s(x),s(y)) -> c_8(ge#(x,y))
            ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
            ifPlus#(true(),x,y) -> c_10(p#(y))
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            inc#(s(x)) -> c_15(inc#(x))
            isZero#(s(s(x))) -> c_18(isZero#(s(x)))
            p#(s(s(x))) -> c_21(p#(s(x)))
            plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:f0#(0(),y,x) -> c_2(f1#(x,y,x))
             -->_1 f1#(x,y,z) -> c_4(f2#(x,y,z)):2
          
          2:S:f1#(x,y,z) -> c_4(f2#(x,y,z))
             -->_1 f2#(x,1(),z) -> c_5(f0#(x,z,z)):3
          
          3:S:f2#(x,1(),z) -> c_5(f0#(x,z,z))
             -->_1 f0#(0(),y,x) -> c_2(f1#(x,y,x)):1
          
          4:W:ge#(s(x),s(y)) -> c_8(ge#(x,y))
             -->_1 ge#(s(x),s(y)) -> c_8(ge#(x,y)):4
          
          5:W:ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
             -->_1 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):11
             -->_2 p#(s(s(x))) -> c_21(p#(s(x))):10
          
          6:W:ifPlus#(true(),x,y) -> c_10(p#(y))
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):10
          
          7:W:ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
             -->_1 timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x)):13
             -->_3 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):11
             -->_2 inc#(s(x)) -> c_15(inc#(x)):8
          
          8:W:inc#(s(x)) -> c_15(inc#(x))
             -->_1 inc#(s(x)) -> c_15(inc#(x)):8
          
          9:W:isZero#(s(s(x))) -> c_18(isZero#(s(x)))
             -->_1 isZero#(s(s(x))) -> c_18(isZero#(s(x))):9
          
          10:W:p#(s(s(x))) -> c_21(p#(s(x)))
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):10
          
          11:W:plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
             -->_1 ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x)):5
             -->_1 ifPlus#(true(),x,y) -> c_10(p#(y)):6
             -->_3 inc#(s(x)) -> c_15(inc#(x)):8
             -->_2 isZero#(s(s(x))) -> c_18(isZero#(s(x))):9
          
          13:W:timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
             -->_2 ge#(s(x),s(y)) -> c_8(ge#(x,y)):4
             -->_1 ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y)):7
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          7: ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
          13: timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
          5: ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
          11: plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
          6: ifPlus#(true(),x,y) -> c_10(p#(y))
          10: p#(s(s(x))) -> c_21(p#(s(x)))
          8: inc#(s(x)) -> c_15(inc#(x))
          9: isZero#(s(s(x))) -> c_18(isZero#(s(x)))
          4: ge#(s(x),s(y)) -> c_8(ge#(x,y))
** Step 6.a:2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            f0#(0(),y,x) -> c_2(f1#(x,y,x))
            f1#(x,y,z) -> c_4(f2#(x,y,z))
            f2#(x,1(),z) -> c_5(f0#(x,z,z))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          f0#(0(),y,x) -> c_2(f1#(x,y,x))
          f1#(x,y,z) -> c_4(f2#(x,y,z))
          f2#(x,1(),z) -> c_5(f0#(x,z,z))
** Step 6.a:3: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          f0#(0(),y,x) -> c_2(f1#(x,y,x))
          f1#(x,y,z) -> c_4(f2#(x,y,z))
          f2#(x,1(),z) -> c_5(f0#(x,z,z))
      - Signature:
          {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
          ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
          ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
          ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
          ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
** Step 6.b:1: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            ge#(s(x),s(y)) -> c_8(ge#(x,y))
            ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
            ifPlus#(true(),x,y) -> c_10(p#(y))
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            inc#(s(x)) -> c_15(inc#(x))
            isZero#(s(s(x))) -> c_18(isZero#(s(x)))
            p#(s(s(x))) -> c_21(p#(s(x)))
            plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
        - Weak DPs:
            f0#(0(),y,x) -> c_2(f1#(x,y,x))
            f1#(x,y,z) -> c_4(f2#(x,y,z))
            f2#(x,1(),z) -> c_5(f0#(x,z,z))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:ge#(s(x),s(y)) -> c_8(ge#(x,y))
             -->_1 ge#(s(x),s(y)) -> c_8(ge#(x,y)):1
          
          2:S:ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
             -->_1 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):8
             -->_2 p#(s(s(x))) -> c_21(p#(s(x))):7
          
          3:S:ifPlus#(true(),x,y) -> c_10(p#(y))
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):7
          
          4:S:ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
             -->_1 timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x)):9
             -->_3 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):8
             -->_2 inc#(s(x)) -> c_15(inc#(x)):5
          
          5:S:inc#(s(x)) -> c_15(inc#(x))
             -->_1 inc#(s(x)) -> c_15(inc#(x)):5
          
          6:S:isZero#(s(s(x))) -> c_18(isZero#(s(x)))
             -->_1 isZero#(s(s(x))) -> c_18(isZero#(s(x))):6
          
          7:S:p#(s(s(x))) -> c_21(p#(s(x)))
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):7
          
          8:S:plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
             -->_2 isZero#(s(s(x))) -> c_18(isZero#(s(x))):6
             -->_3 inc#(s(x)) -> c_15(inc#(x)):5
             -->_1 ifPlus#(true(),x,y) -> c_10(p#(y)):3
             -->_1 ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x)):2
          
          9:S:timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
             -->_1 ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y)):4
             -->_2 ge#(s(x),s(y)) -> c_8(ge#(x,y)):1
          
          10:W:f0#(0(),y,x) -> c_2(f1#(x,y,x))
             -->_1 f1#(x,y,z) -> c_4(f2#(x,y,z)):11
          
          11:W:f1#(x,y,z) -> c_4(f2#(x,y,z))
             -->_1 f2#(x,1(),z) -> c_5(f0#(x,z,z)):12
          
          12:W:f2#(x,1(),z) -> c_5(f0#(x,z,z))
             -->_1 f0#(0(),y,x) -> c_2(f1#(x,y,x)):10
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          10: f0#(0(),y,x) -> c_2(f1#(x,y,x))
          12: f2#(x,1(),z) -> c_5(f0#(x,z,z))
          11: f1#(x,y,z) -> c_4(f2#(x,y,z))
** Step 6.b:2: Decompose MAYBE
    + Considered Problem:
        - Strict DPs:
            ge#(s(x),s(y)) -> c_8(ge#(x,y))
            ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
            ifPlus#(true(),x,y) -> c_10(p#(y))
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            inc#(s(x)) -> c_15(inc#(x))
            isZero#(s(s(x))) -> c_18(isZero#(s(x)))
            p#(s(s(x))) -> c_21(p#(s(x)))
            plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
    + Details:
        We analyse the complexity of following sub-problems (R) and (S).
        Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
        
        Problem (R)
          - Strict DPs:
              ge#(s(x),s(y)) -> c_8(ge#(x,y))
          - Weak DPs:
              ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
              ifPlus#(true(),x,y) -> c_10(p#(y))
              ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
              inc#(s(x)) -> c_15(inc#(x))
              isZero#(s(s(x))) -> c_18(isZero#(s(x)))
              p#(s(s(x))) -> c_21(p#(s(x)))
              plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
              timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
          - Weak TRS:
              ge(x,0()) -> true()
              ge(0(),s(y)) -> false()
              ge(s(x),s(y)) -> ge(x,y)
              ifPlus(false(),x,y) -> plus(p(x),y)
              ifPlus(true(),x,y) -> p(y)
              inc(x) -> s(x)
              inc(0()) -> s(0())
              inc(s(x)) -> s(inc(x))
              isZero(0()) -> true()
              isZero(s(0())) -> false()
              isZero(s(s(x))) -> isZero(s(x))
              p(0()) -> 0()
              p(s(x)) -> x
              p(s(s(x))) -> s(p(s(x)))
              plus(x,y) -> ifPlus(isZero(x),x,inc(y))
          - Signature:
              {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
              ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0
              ,false/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0
              ,c_14/0,c_15/1,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
              ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
        
        Problem (S)
          - Strict DPs:
              ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
              ifPlus#(true(),x,y) -> c_10(p#(y))
              ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
              inc#(s(x)) -> c_15(inc#(x))
              isZero#(s(s(x))) -> c_18(isZero#(s(x)))
              p#(s(s(x))) -> c_21(p#(s(x)))
              plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
              timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
          - Weak DPs:
              ge#(s(x),s(y)) -> c_8(ge#(x,y))
          - Weak TRS:
              ge(x,0()) -> true()
              ge(0(),s(y)) -> false()
              ge(s(x),s(y)) -> ge(x,y)
              ifPlus(false(),x,y) -> plus(p(x),y)
              ifPlus(true(),x,y) -> p(y)
              inc(x) -> s(x)
              inc(0()) -> s(0())
              inc(s(x)) -> s(inc(x))
              isZero(0()) -> true()
              isZero(s(0())) -> false()
              isZero(s(s(x))) -> isZero(s(x))
              p(0()) -> 0()
              p(s(x)) -> x
              p(s(s(x))) -> s(p(s(x)))
              plus(x,y) -> ifPlus(isZero(x),x,inc(y))
          - Signature:
              {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
              ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0
              ,false/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0
              ,c_14/0,c_15/1,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
              ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
*** Step 6.b:2.a:1: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            ge#(s(x),s(y)) -> c_8(ge#(x,y))
        - Weak DPs:
            ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
            ifPlus#(true(),x,y) -> c_10(p#(y))
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            inc#(s(x)) -> c_15(inc#(x))
            isZero#(s(s(x))) -> c_18(isZero#(s(x)))
            p#(s(s(x))) -> c_21(p#(s(x)))
            plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:ge#(s(x),s(y)) -> c_8(ge#(x,y))
             -->_1 ge#(s(x),s(y)) -> c_8(ge#(x,y)):1
          
          2:W:ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
             -->_1 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):8
             -->_2 p#(s(s(x))) -> c_21(p#(s(x))):7
          
          3:W:ifPlus#(true(),x,y) -> c_10(p#(y))
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):7
          
          4:W:ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
             -->_1 timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x)):9
             -->_3 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):8
             -->_2 inc#(s(x)) -> c_15(inc#(x)):5
          
          5:W:inc#(s(x)) -> c_15(inc#(x))
             -->_1 inc#(s(x)) -> c_15(inc#(x)):5
          
          6:W:isZero#(s(s(x))) -> c_18(isZero#(s(x)))
             -->_1 isZero#(s(s(x))) -> c_18(isZero#(s(x))):6
          
          7:W:p#(s(s(x))) -> c_21(p#(s(x)))
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):7
          
          8:W:plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
             -->_1 ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x)):2
             -->_1 ifPlus#(true(),x,y) -> c_10(p#(y)):3
             -->_3 inc#(s(x)) -> c_15(inc#(x)):5
             -->_2 isZero#(s(s(x))) -> c_18(isZero#(s(x))):6
          
          9:W:timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
             -->_2 ge#(s(x),s(y)) -> c_8(ge#(x,y)):1
             -->_1 ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y)):4
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          2: ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
          8: plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
          3: ifPlus#(true(),x,y) -> c_10(p#(y))
          7: p#(s(s(x))) -> c_21(p#(s(x)))
          5: inc#(s(x)) -> c_15(inc#(x))
          6: isZero#(s(s(x))) -> c_18(isZero#(s(x)))
*** Step 6.b:2.a:2: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            ge#(s(x),s(y)) -> c_8(ge#(x,y))
        - Weak DPs:
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:ge#(s(x),s(y)) -> c_8(ge#(x,y))
             -->_1 ge#(s(x),s(y)) -> c_8(ge#(x,y)):1
          
          4:W:ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
             -->_1 timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x)):9
          
          9:W:timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
             -->_2 ge#(s(x),s(y)) -> c_8(ge#(x,y)):1
             -->_1 ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y)):4
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)))
*** Step 6.b:2.a:3: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          ge#(s(x),s(y)) -> c_8(ge#(x,y))
      - Weak DPs:
          ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)))
          timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
      - Weak TRS:
          ge(x,0()) -> true()
          ge(0(),s(y)) -> false()
          ge(s(x),s(y)) -> ge(x,y)
          ifPlus(false(),x,y) -> plus(p(x),y)
          ifPlus(true(),x,y) -> p(y)
          inc(x) -> s(x)
          inc(0()) -> s(0())
          inc(s(x)) -> s(inc(x))
          isZero(0()) -> true()
          isZero(s(0())) -> false()
          isZero(s(s(x))) -> isZero(s(x))
          p(0()) -> 0()
          p(s(x)) -> x
          p(s(s(x))) -> s(p(s(x)))
          plus(x,y) -> ifPlus(isZero(x),x,inc(y))
      - Signature:
          {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
          ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
          ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0,c_15/1
          ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
          ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
*** Step 6.b:2.b:1: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
            ifPlus#(true(),x,y) -> c_10(p#(y))
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            inc#(s(x)) -> c_15(inc#(x))
            isZero#(s(s(x))) -> c_18(isZero#(s(x)))
            p#(s(s(x))) -> c_21(p#(s(x)))
            plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
        - Weak DPs:
            ge#(s(x),s(y)) -> c_8(ge#(x,y))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
             -->_1 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):7
             -->_2 p#(s(s(x))) -> c_21(p#(s(x))):6
          
          2:S:ifPlus#(true(),x,y) -> c_10(p#(y))
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):6
          
          3:S:ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
             -->_1 timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x)):8
             -->_3 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):7
             -->_2 inc#(s(x)) -> c_15(inc#(x)):4
          
          4:S:inc#(s(x)) -> c_15(inc#(x))
             -->_1 inc#(s(x)) -> c_15(inc#(x)):4
          
          5:S:isZero#(s(s(x))) -> c_18(isZero#(s(x)))
             -->_1 isZero#(s(s(x))) -> c_18(isZero#(s(x))):5
          
          6:S:p#(s(s(x))) -> c_21(p#(s(x)))
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):6
          
          7:S:plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
             -->_2 isZero#(s(s(x))) -> c_18(isZero#(s(x))):5
             -->_3 inc#(s(x)) -> c_15(inc#(x)):4
             -->_1 ifPlus#(true(),x,y) -> c_10(p#(y)):2
             -->_1 ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x)):1
          
          8:S:timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
             -->_2 ge#(s(x),s(y)) -> c_8(ge#(x,y)):9
             -->_1 ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y)):3
          
          9:W:ge#(s(x),s(y)) -> c_8(ge#(x,y))
             -->_1 ge#(s(x),s(y)) -> c_8(ge#(x,y)):9
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          9: ge#(s(x),s(y)) -> c_8(ge#(x,y))
*** Step 6.b:2.b:2: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
            ifPlus#(true(),x,y) -> c_10(p#(y))
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            inc#(s(x)) -> c_15(inc#(x))
            isZero#(s(s(x))) -> c_18(isZero#(s(x)))
            p#(s(s(x))) -> c_21(p#(s(x)))
            plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
             -->_1 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):7
             -->_2 p#(s(s(x))) -> c_21(p#(s(x))):6
          
          2:S:ifPlus#(true(),x,y) -> c_10(p#(y))
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):6
          
          3:S:ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
             -->_1 timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x)):8
             -->_3 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):7
             -->_2 inc#(s(x)) -> c_15(inc#(x)):4
          
          4:S:inc#(s(x)) -> c_15(inc#(x))
             -->_1 inc#(s(x)) -> c_15(inc#(x)):4
          
          5:S:isZero#(s(s(x))) -> c_18(isZero#(s(x)))
             -->_1 isZero#(s(s(x))) -> c_18(isZero#(s(x))):5
          
          6:S:p#(s(s(x))) -> c_21(p#(s(x)))
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):6
          
          7:S:plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
             -->_2 isZero#(s(s(x))) -> c_18(isZero#(s(x))):5
             -->_3 inc#(s(x)) -> c_15(inc#(x)):4
             -->_1 ifPlus#(true(),x,y) -> c_10(p#(y)):2
             -->_1 ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x)):1
          
          8:S:timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z),ge#(i,x))
             -->_1 ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y)):3
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z))
*** Step 6.b:2.b:3: Decompose MAYBE
    + Considered Problem:
        - Strict DPs:
            ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
            ifPlus#(true(),x,y) -> c_10(p#(y))
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            inc#(s(x)) -> c_15(inc#(x))
            isZero#(s(s(x))) -> c_18(isZero#(s(x)))
            p#(s(s(x))) -> c_21(p#(s(x)))
            plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
    + Details:
        We analyse the complexity of following sub-problems (R) and (S).
        Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
        
        Problem (R)
          - Strict DPs:
              ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
              ifPlus#(true(),x,y) -> c_10(p#(y))
              inc#(s(x)) -> c_15(inc#(x))
              isZero#(s(s(x))) -> c_18(isZero#(s(x)))
              p#(s(s(x))) -> c_21(p#(s(x)))
              plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
          - Weak DPs:
              ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
              timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z))
          - Weak TRS:
              ge(x,0()) -> true()
              ge(0(),s(y)) -> false()
              ge(s(x),s(y)) -> ge(x,y)
              ifPlus(false(),x,y) -> plus(p(x),y)
              ifPlus(true(),x,y) -> p(y)
              inc(x) -> s(x)
              inc(0()) -> s(0())
              inc(s(x)) -> s(inc(x))
              isZero(0()) -> true()
              isZero(s(0())) -> false()
              isZero(s(s(x))) -> isZero(s(x))
              p(0()) -> 0()
              p(s(x)) -> x
              p(s(s(x))) -> s(p(s(x)))
              plus(x,y) -> ifPlus(isZero(x),x,inc(y))
          - Signature:
              {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
              ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0
              ,false/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0
              ,c_14/0,c_15/1,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/1}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
              ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
        
        Problem (S)
          - Strict DPs:
              ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
              timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z))
          - Weak DPs:
              ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
              ifPlus#(true(),x,y) -> c_10(p#(y))
              inc#(s(x)) -> c_15(inc#(x))
              isZero#(s(s(x))) -> c_18(isZero#(s(x)))
              p#(s(s(x))) -> c_21(p#(s(x)))
              plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
          - Weak TRS:
              ge(x,0()) -> true()
              ge(0(),s(y)) -> false()
              ge(s(x),s(y)) -> ge(x,y)
              ifPlus(false(),x,y) -> plus(p(x),y)
              ifPlus(true(),x,y) -> p(y)
              inc(x) -> s(x)
              inc(0()) -> s(0())
              inc(s(x)) -> s(inc(x))
              isZero(0()) -> true()
              isZero(s(0())) -> false()
              isZero(s(s(x))) -> isZero(s(x))
              p(0()) -> 0()
              p(s(x)) -> x
              p(s(s(x))) -> s(p(s(x)))
              plus(x,y) -> ifPlus(isZero(x),x,inc(y))
          - Signature:
              {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
              ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0
              ,false/0,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0
              ,c_14/0,c_15/1,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/1}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
              ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
**** Step 6.b:2.b:3.a:1: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
          ifPlus#(true(),x,y) -> c_10(p#(y))
          inc#(s(x)) -> c_15(inc#(x))
          isZero#(s(s(x))) -> c_18(isZero#(s(x)))
          p#(s(s(x))) -> c_21(p#(s(x)))
          plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
      - Weak DPs:
          ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
          timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z))
      - Weak TRS:
          ge(x,0()) -> true()
          ge(0(),s(y)) -> false()
          ge(s(x),s(y)) -> ge(x,y)
          ifPlus(false(),x,y) -> plus(p(x),y)
          ifPlus(true(),x,y) -> p(y)
          inc(x) -> s(x)
          inc(0()) -> s(0())
          inc(s(x)) -> s(inc(x))
          isZero(0()) -> true()
          isZero(s(0())) -> false()
          isZero(s(s(x))) -> isZero(s(x))
          p(0()) -> 0()
          p(s(x)) -> x
          p(s(s(x))) -> s(p(s(x)))
          plus(x,y) -> ifPlus(isZero(x),x,inc(y))
      - Signature:
          {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
          ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
          ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
          ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
          ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
**** Step 6.b:2.b:3.b:1: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z))
        - Weak DPs:
            ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
            ifPlus#(true(),x,y) -> c_10(p#(y))
            inc#(s(x)) -> c_15(inc#(x))
            isZero#(s(s(x))) -> c_18(isZero#(s(x)))
            p#(s(s(x))) -> c_21(p#(s(x)))
            plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
             -->_3 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):8
             -->_2 inc#(s(x)) -> c_15(inc#(x)):5
             -->_1 timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z)):2
          
          2:S:timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z))
             -->_1 ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y)):1
          
          3:W:ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
             -->_1 plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y)):8
             -->_2 p#(s(s(x))) -> c_21(p#(s(x))):7
          
          4:W:ifPlus#(true(),x,y) -> c_10(p#(y))
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):7
          
          5:W:inc#(s(x)) -> c_15(inc#(x))
             -->_1 inc#(s(x)) -> c_15(inc#(x)):5
          
          6:W:isZero#(s(s(x))) -> c_18(isZero#(s(x)))
             -->_1 isZero#(s(s(x))) -> c_18(isZero#(s(x))):6
          
          7:W:p#(s(s(x))) -> c_21(p#(s(x)))
             -->_1 p#(s(s(x))) -> c_21(p#(s(x))):7
          
          8:W:plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
             -->_2 isZero#(s(s(x))) -> c_18(isZero#(s(x))):6
             -->_3 inc#(s(x)) -> c_15(inc#(x)):5
             -->_1 ifPlus#(true(),x,y) -> c_10(p#(y)):4
             -->_1 ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x)):3
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          8: plus#(x,y) -> c_22(ifPlus#(isZero(x),x,inc(y)),isZero#(x),inc#(y))
          3: ifPlus#(false(),x,y) -> c_9(plus#(p(x),y),p#(x))
          4: ifPlus#(true(),x,y) -> c_10(p#(y))
          7: p#(s(s(x))) -> c_21(p#(s(x)))
          5: inc#(s(x)) -> c_15(inc#(x))
          6: isZero#(s(s(x))) -> c_18(isZero#(s(x)))
**** Step 6.b:2.b:3.b:2: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
            timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z))
        - Weak TRS:
            ge(x,0()) -> true()
            ge(0(),s(y)) -> false()
            ge(s(x),s(y)) -> ge(x,y)
            ifPlus(false(),x,y) -> plus(p(x),y)
            ifPlus(true(),x,y) -> p(y)
            inc(x) -> s(x)
            inc(0()) -> s(0())
            inc(s(x)) -> s(inc(x))
            isZero(0()) -> true()
            isZero(s(0())) -> false()
            isZero(s(s(x))) -> isZero(s(x))
            p(0()) -> 0()
            p(s(x)) -> x
            p(s(s(x))) -> s(p(s(x)))
            plus(x,y) -> ifPlus(isZero(x),x,inc(y))
        - Signature:
            {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
            ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
            ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/3,c_12/0,c_13/0,c_14/0,c_15/1
            ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
            ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y))
             -->_1 timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z)):2
          
          2:S:timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z))
             -->_1 ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)),inc#(i),plus#(z,y)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)))
**** Step 6.b:2.b:3.b:3: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          ifTimes#(false(),i,x,y,z) -> c_11(timesIter#(inc(i),x,y,plus(z,y)))
          timesIter#(i,x,y,z) -> c_24(ifTimes#(ge(i,x),i,x,y,z))
      - Weak TRS:
          ge(x,0()) -> true()
          ge(0(),s(y)) -> false()
          ge(s(x),s(y)) -> ge(x,y)
          ifPlus(false(),x,y) -> plus(p(x),y)
          ifPlus(true(),x,y) -> p(y)
          inc(x) -> s(x)
          inc(0()) -> s(0())
          inc(s(x)) -> s(inc(x))
          isZero(0()) -> true()
          isZero(s(0())) -> false()
          isZero(s(s(x))) -> isZero(s(x))
          p(0()) -> 0()
          p(s(x)) -> x
          p(s(s(x))) -> s(p(s(x)))
          plus(x,y) -> ifPlus(isZero(x),x,inc(y))
      - Signature:
          {f0/3,f1/3,f2/3,ge/2,ifPlus/3,ifTimes/5,inc/1,isZero/1,p/1,plus/2,times/2,timesIter/4,f0#/3,f1#/3,f2#/3
          ,ge#/2,ifPlus#/3,ifTimes#/5,inc#/1,isZero#/1,p#/1,plus#/2,times#/2,timesIter#/4} / {0/0,1/0,c/0,d/0,false/0
          ,s/1,true/0,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2,c_10/1,c_11/1,c_12/0,c_13/0,c_14/0,c_15/1
          ,c_16/0,c_17/0,c_18/1,c_19/0,c_20/0,c_21/1,c_22/3,c_23/1,c_24/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {f0#,f1#,f2#,ge#,ifPlus#,ifTimes#,inc#,isZero#,p#,plus#
          ,times#,timesIter#} and constructors {0,1,c,d,false,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE