MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            a() -> b()
            a() -> c()
            head(cons(x,xs)) -> x
            head(nil()) -> error()
            ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
            ifPlus(true(),x,y,z) -> y
            ifSum(false(),xs,x,y) -> sumIter(tail(xs),y)
            ifSum(true(),xs,x,y) -> x
            isempty(cons(x,xs)) -> false()
            isempty(nil()) -> true()
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            plus(x,y) -> plusIter(x,y,0())
            plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
            sum(xs) -> sumIter(xs,0())
            sumIter(xs,x) -> ifSum(isempty(xs),xs,x,plus(x,head(xs)))
            tail(cons(x,xs)) -> xs
            tail(nil()) -> nil()
        - Signature:
            {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1} / {0/0,b/0,c/0,cons/2
            ,error/0,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a,head,ifPlus,ifSum,isempty,le,plus,plusIter,sum,sumIter
            ,tail} and constructors {0,b,c,cons,error,false,nil,s,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          a#() -> c_1()
          a#() -> c_2()
          head#(cons(x,xs)) -> c_3()
          head#(nil()) -> c_4()
          ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
          ifPlus#(true(),x,y,z) -> c_6()
          ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y),tail#(xs))
          ifSum#(true(),xs,x,y) -> c_8()
          isempty#(cons(x,xs)) -> c_9()
          isempty#(nil()) -> c_10()
          le#(0(),y) -> c_11()
          le#(s(x),0()) -> c_12()
          le#(s(x),s(y)) -> c_13(le#(x,y))
          plus#(x,y) -> c_14(plusIter#(x,y,0()))
          plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
          sum#(xs) -> c_16(sumIter#(xs,0()))
          sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),isempty#(xs),plus#(x,head(xs)),head#(xs))
          tail#(cons(x,xs)) -> c_18()
          tail#(nil()) -> c_19()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            a#() -> c_1()
            a#() -> c_2()
            head#(cons(x,xs)) -> c_3()
            head#(nil()) -> c_4()
            ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
            ifPlus#(true(),x,y,z) -> c_6()
            ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y),tail#(xs))
            ifSum#(true(),xs,x,y) -> c_8()
            isempty#(cons(x,xs)) -> c_9()
            isempty#(nil()) -> c_10()
            le#(0(),y) -> c_11()
            le#(s(x),0()) -> c_12()
            le#(s(x),s(y)) -> c_13(le#(x,y))
            plus#(x,y) -> c_14(plusIter#(x,y,0()))
            plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
            sum#(xs) -> c_16(sumIter#(xs,0()))
            sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),isempty#(xs),plus#(x,head(xs)),head#(xs))
            tail#(cons(x,xs)) -> c_18()
            tail#(nil()) -> c_19()
        - Weak TRS:
            a() -> b()
            a() -> c()
            head(cons(x,xs)) -> x
            head(nil()) -> error()
            ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
            ifPlus(true(),x,y,z) -> y
            ifSum(false(),xs,x,y) -> sumIter(tail(xs),y)
            ifSum(true(),xs,x,y) -> x
            isempty(cons(x,xs)) -> false()
            isempty(nil()) -> true()
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            plus(x,y) -> plusIter(x,y,0())
            plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
            sum(xs) -> sumIter(xs,0())
            sumIter(xs,x) -> ifSum(isempty(xs),xs,x,plus(x,head(xs)))
            tail(cons(x,xs)) -> xs
            tail(nil()) -> nil()
        - Signature:
            {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1,a#/0,head#/1,ifPlus#/4
            ,ifSum#/4,isempty#/1,le#/2,plus#/2,plusIter#/3,sum#/1,sumIter#/2,tail#/1} / {0/0,b/0,c/0,cons/2,error/0
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1
            ,c_14/1,c_15/2,c_16/1,c_17/4,c_18/0,c_19/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#,head#,ifPlus#,ifSum#,isempty#,le#,plus#,plusIter#,sum#
            ,sumIter#,tail#} and constructors {0,b,c,cons,error,false,nil,s,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          head(cons(x,xs)) -> x
          head(nil()) -> error()
          ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
          ifPlus(true(),x,y,z) -> y
          isempty(cons(x,xs)) -> false()
          isempty(nil()) -> true()
          le(0(),y) -> true()
          le(s(x),0()) -> false()
          le(s(x),s(y)) -> le(x,y)
          plus(x,y) -> plusIter(x,y,0())
          plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
          tail(cons(x,xs)) -> xs
          tail(nil()) -> nil()
          a#() -> c_1()
          a#() -> c_2()
          head#(cons(x,xs)) -> c_3()
          head#(nil()) -> c_4()
          ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
          ifPlus#(true(),x,y,z) -> c_6()
          ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y),tail#(xs))
          ifSum#(true(),xs,x,y) -> c_8()
          isempty#(cons(x,xs)) -> c_9()
          isempty#(nil()) -> c_10()
          le#(0(),y) -> c_11()
          le#(s(x),0()) -> c_12()
          le#(s(x),s(y)) -> c_13(le#(x,y))
          plus#(x,y) -> c_14(plusIter#(x,y,0()))
          plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
          sum#(xs) -> c_16(sumIter#(xs,0()))
          sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),isempty#(xs),plus#(x,head(xs)),head#(xs))
          tail#(cons(x,xs)) -> c_18()
          tail#(nil()) -> c_19()
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            a#() -> c_1()
            a#() -> c_2()
            head#(cons(x,xs)) -> c_3()
            head#(nil()) -> c_4()
            ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
            ifPlus#(true(),x,y,z) -> c_6()
            ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y),tail#(xs))
            ifSum#(true(),xs,x,y) -> c_8()
            isempty#(cons(x,xs)) -> c_9()
            isempty#(nil()) -> c_10()
            le#(0(),y) -> c_11()
            le#(s(x),0()) -> c_12()
            le#(s(x),s(y)) -> c_13(le#(x,y))
            plus#(x,y) -> c_14(plusIter#(x,y,0()))
            plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
            sum#(xs) -> c_16(sumIter#(xs,0()))
            sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),isempty#(xs),plus#(x,head(xs)),head#(xs))
            tail#(cons(x,xs)) -> c_18()
            tail#(nil()) -> c_19()
        - Weak TRS:
            head(cons(x,xs)) -> x
            head(nil()) -> error()
            ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
            ifPlus(true(),x,y,z) -> y
            isempty(cons(x,xs)) -> false()
            isempty(nil()) -> true()
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            plus(x,y) -> plusIter(x,y,0())
            plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
            tail(cons(x,xs)) -> xs
            tail(nil()) -> nil()
        - Signature:
            {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1,a#/0,head#/1,ifPlus#/4
            ,ifSum#/4,isempty#/1,le#/2,plus#/2,plusIter#/3,sum#/1,sumIter#/2,tail#/1} / {0/0,b/0,c/0,cons/2,error/0
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1
            ,c_14/1,c_15/2,c_16/1,c_17/4,c_18/0,c_19/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#,head#,ifPlus#,ifSum#,isempty#,le#,plus#,plusIter#,sum#
            ,sumIter#,tail#} and constructors {0,b,c,cons,error,false,nil,s,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,2,3,4,6,8,9,10,11,12,18,19}
        by application of
          Pre({1,2,3,4,6,8,9,10,11,12,18,19}) = {7,13,15,17}.
        Here rules are labelled as follows:
          1: a#() -> c_1()
          2: a#() -> c_2()
          3: head#(cons(x,xs)) -> c_3()
          4: head#(nil()) -> c_4()
          5: ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
          6: ifPlus#(true(),x,y,z) -> c_6()
          7: ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y),tail#(xs))
          8: ifSum#(true(),xs,x,y) -> c_8()
          9: isempty#(cons(x,xs)) -> c_9()
          10: isempty#(nil()) -> c_10()
          11: le#(0(),y) -> c_11()
          12: le#(s(x),0()) -> c_12()
          13: le#(s(x),s(y)) -> c_13(le#(x,y))
          14: plus#(x,y) -> c_14(plusIter#(x,y,0()))
          15: plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
          16: sum#(xs) -> c_16(sumIter#(xs,0()))
          17: sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs)))
                                    ,isempty#(xs)
                                    ,plus#(x,head(xs))
                                    ,head#(xs))
          18: tail#(cons(x,xs)) -> c_18()
          19: tail#(nil()) -> c_19()
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
            ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y),tail#(xs))
            le#(s(x),s(y)) -> c_13(le#(x,y))
            plus#(x,y) -> c_14(plusIter#(x,y,0()))
            plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
            sum#(xs) -> c_16(sumIter#(xs,0()))
            sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),isempty#(xs),plus#(x,head(xs)),head#(xs))
        - Weak DPs:
            a#() -> c_1()
            a#() -> c_2()
            head#(cons(x,xs)) -> c_3()
            head#(nil()) -> c_4()
            ifPlus#(true(),x,y,z) -> c_6()
            ifSum#(true(),xs,x,y) -> c_8()
            isempty#(cons(x,xs)) -> c_9()
            isempty#(nil()) -> c_10()
            le#(0(),y) -> c_11()
            le#(s(x),0()) -> c_12()
            tail#(cons(x,xs)) -> c_18()
            tail#(nil()) -> c_19()
        - Weak TRS:
            head(cons(x,xs)) -> x
            head(nil()) -> error()
            ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
            ifPlus(true(),x,y,z) -> y
            isempty(cons(x,xs)) -> false()
            isempty(nil()) -> true()
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            plus(x,y) -> plusIter(x,y,0())
            plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
            tail(cons(x,xs)) -> xs
            tail(nil()) -> nil()
        - Signature:
            {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1,a#/0,head#/1,ifPlus#/4
            ,ifSum#/4,isempty#/1,le#/2,plus#/2,plusIter#/3,sum#/1,sumIter#/2,tail#/1} / {0/0,b/0,c/0,cons/2,error/0
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1
            ,c_14/1,c_15/2,c_16/1,c_17/4,c_18/0,c_19/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#,head#,ifPlus#,ifSum#,isempty#,le#,plus#,plusIter#,sum#
            ,sumIter#,tail#} and constructors {0,b,c,cons,error,false,nil,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
             -->_1 plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z)):5
          
          2:S:ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y),tail#(xs))
             -->_1 sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs)))
                                         ,isempty#(xs)
                                         ,plus#(x,head(xs))
                                         ,head#(xs)):7
             -->_2 tail#(nil()) -> c_19():19
             -->_2 tail#(cons(x,xs)) -> c_18():18
          
          3:S:le#(s(x),s(y)) -> c_13(le#(x,y))
             -->_1 le#(s(x),0()) -> c_12():17
             -->_1 le#(0(),y) -> c_11():16
             -->_1 le#(s(x),s(y)) -> c_13(le#(x,y)):3
          
          4:S:plus#(x,y) -> c_14(plusIter#(x,y,0()))
             -->_1 plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z)):5
          
          5:S:plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
             -->_2 le#(s(x),0()) -> c_12():17
             -->_2 le#(0(),y) -> c_11():16
             -->_1 ifPlus#(true(),x,y,z) -> c_6():12
             -->_2 le#(s(x),s(y)) -> c_13(le#(x,y)):3
             -->_1 ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z))):1
          
          6:S:sum#(xs) -> c_16(sumIter#(xs,0()))
             -->_1 sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs)))
                                         ,isempty#(xs)
                                         ,plus#(x,head(xs))
                                         ,head#(xs)):7
          
          7:S:sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs)))
                                    ,isempty#(xs)
                                    ,plus#(x,head(xs))
                                    ,head#(xs))
             -->_2 isempty#(nil()) -> c_10():15
             -->_2 isempty#(cons(x,xs)) -> c_9():14
             -->_1 ifSum#(true(),xs,x,y) -> c_8():13
             -->_4 head#(nil()) -> c_4():11
             -->_4 head#(cons(x,xs)) -> c_3():10
             -->_3 plus#(x,y) -> c_14(plusIter#(x,y,0())):4
             -->_1 ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y),tail#(xs)):2
          
          8:W:a#() -> c_1()
             
          
          9:W:a#() -> c_2()
             
          
          10:W:head#(cons(x,xs)) -> c_3()
             
          
          11:W:head#(nil()) -> c_4()
             
          
          12:W:ifPlus#(true(),x,y,z) -> c_6()
             
          
          13:W:ifSum#(true(),xs,x,y) -> c_8()
             
          
          14:W:isempty#(cons(x,xs)) -> c_9()
             
          
          15:W:isempty#(nil()) -> c_10()
             
          
          16:W:le#(0(),y) -> c_11()
             
          
          17:W:le#(s(x),0()) -> c_12()
             
          
          18:W:tail#(cons(x,xs)) -> c_18()
             
          
          19:W:tail#(nil()) -> c_19()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          9: a#() -> c_2()
          8: a#() -> c_1()
          18: tail#(cons(x,xs)) -> c_18()
          19: tail#(nil()) -> c_19()
          10: head#(cons(x,xs)) -> c_3()
          11: head#(nil()) -> c_4()
          13: ifSum#(true(),xs,x,y) -> c_8()
          14: isempty#(cons(x,xs)) -> c_9()
          15: isempty#(nil()) -> c_10()
          12: ifPlus#(true(),x,y,z) -> c_6()
          16: le#(0(),y) -> c_11()
          17: le#(s(x),0()) -> c_12()
* Step 5: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
            ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y),tail#(xs))
            le#(s(x),s(y)) -> c_13(le#(x,y))
            plus#(x,y) -> c_14(plusIter#(x,y,0()))
            plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
            sum#(xs) -> c_16(sumIter#(xs,0()))
            sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),isempty#(xs),plus#(x,head(xs)),head#(xs))
        - Weak TRS:
            head(cons(x,xs)) -> x
            head(nil()) -> error()
            ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
            ifPlus(true(),x,y,z) -> y
            isempty(cons(x,xs)) -> false()
            isempty(nil()) -> true()
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            plus(x,y) -> plusIter(x,y,0())
            plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
            tail(cons(x,xs)) -> xs
            tail(nil()) -> nil()
        - Signature:
            {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1,a#/0,head#/1,ifPlus#/4
            ,ifSum#/4,isempty#/1,le#/2,plus#/2,plusIter#/3,sum#/1,sumIter#/2,tail#/1} / {0/0,b/0,c/0,cons/2,error/0
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/2,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1
            ,c_14/1,c_15/2,c_16/1,c_17/4,c_18/0,c_19/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#,head#,ifPlus#,ifSum#,isempty#,le#,plus#,plusIter#,sum#
            ,sumIter#,tail#} and constructors {0,b,c,cons,error,false,nil,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
             -->_1 plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z)):5
          
          2:S:ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y),tail#(xs))
             -->_1 sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs)))
                                         ,isempty#(xs)
                                         ,plus#(x,head(xs))
                                         ,head#(xs)):7
          
          3:S:le#(s(x),s(y)) -> c_13(le#(x,y))
             -->_1 le#(s(x),s(y)) -> c_13(le#(x,y)):3
          
          4:S:plus#(x,y) -> c_14(plusIter#(x,y,0()))
             -->_1 plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z)):5
          
          5:S:plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
             -->_2 le#(s(x),s(y)) -> c_13(le#(x,y)):3
             -->_1 ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z))):1
          
          6:S:sum#(xs) -> c_16(sumIter#(xs,0()))
             -->_1 sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs)))
                                         ,isempty#(xs)
                                         ,plus#(x,head(xs))
                                         ,head#(xs)):7
          
          7:S:sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs)))
                                    ,isempty#(xs)
                                    ,plus#(x,head(xs))
                                    ,head#(xs))
             -->_3 plus#(x,y) -> c_14(plusIter#(x,y,0())):4
             -->_1 ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y),tail#(xs)):2
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
          sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs)))
* Step 6: RemoveHeads MAYBE
    + Considered Problem:
        - Strict DPs:
            ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
            ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
            le#(s(x),s(y)) -> c_13(le#(x,y))
            plus#(x,y) -> c_14(plusIter#(x,y,0()))
            plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
            sum#(xs) -> c_16(sumIter#(xs,0()))
            sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs)))
        - Weak TRS:
            head(cons(x,xs)) -> x
            head(nil()) -> error()
            ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
            ifPlus(true(),x,y,z) -> y
            isempty(cons(x,xs)) -> false()
            isempty(nil()) -> true()
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            plus(x,y) -> plusIter(x,y,0())
            plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
            tail(cons(x,xs)) -> xs
            tail(nil()) -> nil()
        - Signature:
            {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1,a#/0,head#/1,ifPlus#/4
            ,ifSum#/4,isempty#/1,le#/2,plus#/2,plusIter#/3,sum#/1,sumIter#/2,tail#/1} / {0/0,b/0,c/0,cons/2,error/0
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1
            ,c_14/1,c_15/2,c_16/1,c_17/2,c_18/0,c_19/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#,head#,ifPlus#,ifSum#,isempty#,le#,plus#,plusIter#,sum#
            ,sumIter#,tail#} and constructors {0,b,c,cons,error,false,nil,s,true}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
           -->_1 plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z)):5
        
        2:S:ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
           -->_1 sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs))):7
        
        3:S:le#(s(x),s(y)) -> c_13(le#(x,y))
           -->_1 le#(s(x),s(y)) -> c_13(le#(x,y)):3
        
        4:S:plus#(x,y) -> c_14(plusIter#(x,y,0()))
           -->_1 plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z)):5
        
        5:S:plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
           -->_2 le#(s(x),s(y)) -> c_13(le#(x,y)):3
           -->_1 ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z))):1
        
        6:S:sum#(xs) -> c_16(sumIter#(xs,0()))
           -->_1 sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs))):7
        
        7:S:sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs)))
           -->_2 plus#(x,y) -> c_14(plusIter#(x,y,0())):4
           -->_1 ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y)):2
        
        
        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).
        
        [(6,sum#(xs) -> c_16(sumIter#(xs,0())))]
* Step 7: Decompose MAYBE
    + Considered Problem:
        - Strict DPs:
            ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
            ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
            le#(s(x),s(y)) -> c_13(le#(x,y))
            plus#(x,y) -> c_14(plusIter#(x,y,0()))
            plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
            sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs)))
        - Weak TRS:
            head(cons(x,xs)) -> x
            head(nil()) -> error()
            ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
            ifPlus(true(),x,y,z) -> y
            isempty(cons(x,xs)) -> false()
            isempty(nil()) -> true()
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            plus(x,y) -> plusIter(x,y,0())
            plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
            tail(cons(x,xs)) -> xs
            tail(nil()) -> nil()
        - Signature:
            {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1,a#/0,head#/1,ifPlus#/4
            ,ifSum#/4,isempty#/1,le#/2,plus#/2,plusIter#/3,sum#/1,sumIter#/2,tail#/1} / {0/0,b/0,c/0,cons/2,error/0
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1
            ,c_14/1,c_15/2,c_16/1,c_17/2,c_18/0,c_19/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#,head#,ifPlus#,ifSum#,isempty#,le#,plus#,plusIter#,sum#
            ,sumIter#,tail#} and constructors {0,b,c,cons,error,false,nil,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,z) -> c_5(plusIter#(x,s(y),s(z)))
              le#(s(x),s(y)) -> c_13(le#(x,y))
              plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
          - Weak DPs:
              ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
              plus#(x,y) -> c_14(plusIter#(x,y,0()))
              sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs)))
          - Weak TRS:
              head(cons(x,xs)) -> x
              head(nil()) -> error()
              ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
              ifPlus(true(),x,y,z) -> y
              isempty(cons(x,xs)) -> false()
              isempty(nil()) -> true()
              le(0(),y) -> true()
              le(s(x),0()) -> false()
              le(s(x),s(y)) -> le(x,y)
              plus(x,y) -> plusIter(x,y,0())
              plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
              tail(cons(x,xs)) -> xs
              tail(nil()) -> nil()
          - Signature:
              {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1,a#/0,head#/1
              ,ifPlus#/4,ifSum#/4,isempty#/1,le#/2,plus#/2,plusIter#/3,sum#/1,sumIter#/2,tail#/1} / {0/0,b/0,c/0,cons/2
              ,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0
              ,c_12/0,c_13/1,c_14/1,c_15/2,c_16/1,c_17/2,c_18/0,c_19/0}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {a#,head#,ifPlus#,ifSum#,isempty#,le#,plus#,plusIter#
              ,sum#,sumIter#,tail#} and constructors {0,b,c,cons,error,false,nil,s,true}
        
        Problem (S)
          - Strict DPs:
              ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
              plus#(x,y) -> c_14(plusIter#(x,y,0()))
              sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs)))
          - Weak DPs:
              ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
              le#(s(x),s(y)) -> c_13(le#(x,y))
              plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
          - Weak TRS:
              head(cons(x,xs)) -> x
              head(nil()) -> error()
              ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
              ifPlus(true(),x,y,z) -> y
              isempty(cons(x,xs)) -> false()
              isempty(nil()) -> true()
              le(0(),y) -> true()
              le(s(x),0()) -> false()
              le(s(x),s(y)) -> le(x,y)
              plus(x,y) -> plusIter(x,y,0())
              plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
              tail(cons(x,xs)) -> xs
              tail(nil()) -> nil()
          - Signature:
              {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1,a#/0,head#/1
              ,ifPlus#/4,ifSum#/4,isempty#/1,le#/2,plus#/2,plusIter#/3,sum#/1,sumIter#/2,tail#/1} / {0/0,b/0,c/0,cons/2
              ,error/0,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0
              ,c_12/0,c_13/1,c_14/1,c_15/2,c_16/1,c_17/2,c_18/0,c_19/0}
          - Obligation:
              innermost runtime complexity wrt. defined symbols {a#,head#,ifPlus#,ifSum#,isempty#,le#,plus#,plusIter#
              ,sum#,sumIter#,tail#} and constructors {0,b,c,cons,error,false,nil,s,true}
** Step 7.a:1: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
          le#(s(x),s(y)) -> c_13(le#(x,y))
          plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
      - Weak DPs:
          ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
          plus#(x,y) -> c_14(plusIter#(x,y,0()))
          sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs)))
      - Weak TRS:
          head(cons(x,xs)) -> x
          head(nil()) -> error()
          ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
          ifPlus(true(),x,y,z) -> y
          isempty(cons(x,xs)) -> false()
          isempty(nil()) -> true()
          le(0(),y) -> true()
          le(s(x),0()) -> false()
          le(s(x),s(y)) -> le(x,y)
          plus(x,y) -> plusIter(x,y,0())
          plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
          tail(cons(x,xs)) -> xs
          tail(nil()) -> nil()
      - Signature:
          {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1,a#/0,head#/1,ifPlus#/4
          ,ifSum#/4,isempty#/1,le#/2,plus#/2,plusIter#/3,sum#/1,sumIter#/2,tail#/1} / {0/0,b/0,c/0,cons/2,error/0
          ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1
          ,c_14/1,c_15/2,c_16/1,c_17/2,c_18/0,c_19/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {a#,head#,ifPlus#,ifSum#,isempty#,le#,plus#,plusIter#,sum#
          ,sumIter#,tail#} and constructors {0,b,c,cons,error,false,nil,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
** Step 7.b:1: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
            plus#(x,y) -> c_14(plusIter#(x,y,0()))
            sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs)))
        - Weak DPs:
            ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
            le#(s(x),s(y)) -> c_13(le#(x,y))
            plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
        - Weak TRS:
            head(cons(x,xs)) -> x
            head(nil()) -> error()
            ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
            ifPlus(true(),x,y,z) -> y
            isempty(cons(x,xs)) -> false()
            isempty(nil()) -> true()
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            plus(x,y) -> plusIter(x,y,0())
            plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
            tail(cons(x,xs)) -> xs
            tail(nil()) -> nil()
        - Signature:
            {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1,a#/0,head#/1,ifPlus#/4
            ,ifSum#/4,isempty#/1,le#/2,plus#/2,plusIter#/3,sum#/1,sumIter#/2,tail#/1} / {0/0,b/0,c/0,cons/2,error/0
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1
            ,c_14/1,c_15/2,c_16/1,c_17/2,c_18/0,c_19/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#,head#,ifPlus#,ifSum#,isempty#,le#,plus#,plusIter#,sum#
            ,sumIter#,tail#} and constructors {0,b,c,cons,error,false,nil,s,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2}
        by application of
          Pre({2}) = {3}.
        Here rules are labelled as follows:
          1: ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
          2: plus#(x,y) -> c_14(plusIter#(x,y,0()))
          3: sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs)))
          4: ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
          5: le#(s(x),s(y)) -> c_13(le#(x,y))
          6: plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
** Step 7.b:2: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
            sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs)))
        - Weak DPs:
            ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
            le#(s(x),s(y)) -> c_13(le#(x,y))
            plus#(x,y) -> c_14(plusIter#(x,y,0()))
            plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
        - Weak TRS:
            head(cons(x,xs)) -> x
            head(nil()) -> error()
            ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
            ifPlus(true(),x,y,z) -> y
            isempty(cons(x,xs)) -> false()
            isempty(nil()) -> true()
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            plus(x,y) -> plusIter(x,y,0())
            plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
            tail(cons(x,xs)) -> xs
            tail(nil()) -> nil()
        - Signature:
            {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1,a#/0,head#/1,ifPlus#/4
            ,ifSum#/4,isempty#/1,le#/2,plus#/2,plusIter#/3,sum#/1,sumIter#/2,tail#/1} / {0/0,b/0,c/0,cons/2,error/0
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1
            ,c_14/1,c_15/2,c_16/1,c_17/2,c_18/0,c_19/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#,head#,ifPlus#,ifSum#,isempty#,le#,plus#,plusIter#,sum#
            ,sumIter#,tail#} and constructors {0,b,c,cons,error,false,nil,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
             -->_1 sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs))):2
          
          2:S:sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs)))
             -->_2 plus#(x,y) -> c_14(plusIter#(x,y,0())):5
             -->_1 ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y)):1
          
          3:W:ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
             -->_1 plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z)):6
          
          4:W:le#(s(x),s(y)) -> c_13(le#(x,y))
             -->_1 le#(s(x),s(y)) -> c_13(le#(x,y)):4
          
          5:W:plus#(x,y) -> c_14(plusIter#(x,y,0()))
             -->_1 plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z)):6
          
          6:W:plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
             -->_2 le#(s(x),s(y)) -> c_13(le#(x,y)):4
             -->_1 ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z))):3
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          5: plus#(x,y) -> c_14(plusIter#(x,y,0()))
          6: plusIter#(x,y,z) -> c_15(ifPlus#(le(x,z),x,y,z),le#(x,z))
          3: ifPlus#(false(),x,y,z) -> c_5(plusIter#(x,s(y),s(z)))
          4: le#(s(x),s(y)) -> c_13(le#(x,y))
** Step 7.b:3: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
            sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs)))
        - Weak TRS:
            head(cons(x,xs)) -> x
            head(nil()) -> error()
            ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
            ifPlus(true(),x,y,z) -> y
            isempty(cons(x,xs)) -> false()
            isempty(nil()) -> true()
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            plus(x,y) -> plusIter(x,y,0())
            plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
            tail(cons(x,xs)) -> xs
            tail(nil()) -> nil()
        - Signature:
            {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1,a#/0,head#/1,ifPlus#/4
            ,ifSum#/4,isempty#/1,le#/2,plus#/2,plusIter#/3,sum#/1,sumIter#/2,tail#/1} / {0/0,b/0,c/0,cons/2,error/0
            ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1
            ,c_14/1,c_15/2,c_16/1,c_17/2,c_18/0,c_19/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#,head#,ifPlus#,ifSum#,isempty#,le#,plus#,plusIter#,sum#
            ,sumIter#,tail#} and constructors {0,b,c,cons,error,false,nil,s,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
             -->_1 sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs))):2
          
          2:S:sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))),plus#(x,head(xs)))
             -->_1 ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))))
** Step 7.b:4: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          ifSum#(false(),xs,x,y) -> c_7(sumIter#(tail(xs),y))
          sumIter#(xs,x) -> c_17(ifSum#(isempty(xs),xs,x,plus(x,head(xs))))
      - Weak TRS:
          head(cons(x,xs)) -> x
          head(nil()) -> error()
          ifPlus(false(),x,y,z) -> plusIter(x,s(y),s(z))
          ifPlus(true(),x,y,z) -> y
          isempty(cons(x,xs)) -> false()
          isempty(nil()) -> true()
          le(0(),y) -> true()
          le(s(x),0()) -> false()
          le(s(x),s(y)) -> le(x,y)
          plus(x,y) -> plusIter(x,y,0())
          plusIter(x,y,z) -> ifPlus(le(x,z),x,y,z)
          tail(cons(x,xs)) -> xs
          tail(nil()) -> nil()
      - Signature:
          {a/0,head/1,ifPlus/4,ifSum/4,isempty/1,le/2,plus/2,plusIter/3,sum/1,sumIter/2,tail/1,a#/0,head#/1,ifPlus#/4
          ,ifSum#/4,isempty#/1,le#/2,plus#/2,plusIter#/3,sum#/1,sumIter#/2,tail#/1} / {0/0,b/0,c/0,cons/2,error/0
          ,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/1
          ,c_14/1,c_15/2,c_16/1,c_17/1,c_18/0,c_19/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {a#,head#,ifPlus#,ifSum#,isempty#,le#,plus#,plusIter#,sum#
          ,sumIter#,tail#} and constructors {0,b,c,cons,error,false,nil,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE