MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            a() -> c()
            a() -> d()
            append(cons(n,l1),l2) -> cons(n,append(l1,l2))
            append(nil(),l2) -> l2
            if(false(),false(),l,t,n) -> lessE(l,t,s(n))
            if(false(),true(),l,t,n) -> t
            if(true(),b,l,t,n) -> l
            le(0(),m) -> true()
            le(s(n),0()) -> false()
            le(s(n),s(m)) -> le(n,m)
            length(cons(n,l)) -> s(length(l))
            length(nil()) -> 0()
            lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
            lessElements(l,t) -> lessE(l,t,0())
            toList(leaf()) -> nil()
            toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
        - Signature:
            {a/0,append/2,if/5,le/2,length/1,lessE/3,lessElements/2,toList/1} / {0/0,c/0,cons/2,d/0,false/0,leaf/0,nil/0
            ,node/3,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a,append,if,le,length,lessE,lessElements
            ,toList} and constructors {0,c,cons,d,false,leaf,nil,node,s,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          a#() -> c_1()
          a#() -> c_2()
          append#(cons(n,l1),l2) -> c_3(append#(l1,l2))
          append#(nil(),l2) -> c_4()
          if#(false(),false(),l,t,n) -> c_5(lessE#(l,t,s(n)))
          if#(false(),true(),l,t,n) -> c_6()
          if#(true(),b,l,t,n) -> c_7()
          le#(0(),m) -> c_8()
          le#(s(n),0()) -> c_9()
          le#(s(n),s(m)) -> c_10(le#(n,m))
          length#(cons(n,l)) -> c_11(length#(l))
          length#(nil()) -> c_12()
          lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                               ,le#(length(l),n)
                               ,length#(l)
                               ,le#(length(toList(t)),n)
                               ,length#(toList(t))
                               ,toList#(t))
          lessElements#(l,t) -> c_14(lessE#(l,t,0()))
          toList#(leaf()) -> c_15()
          toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            a#() -> c_1()
            a#() -> c_2()
            append#(cons(n,l1),l2) -> c_3(append#(l1,l2))
            append#(nil(),l2) -> c_4()
            if#(false(),false(),l,t,n) -> c_5(lessE#(l,t,s(n)))
            if#(false(),true(),l,t,n) -> c_6()
            if#(true(),b,l,t,n) -> c_7()
            le#(0(),m) -> c_8()
            le#(s(n),0()) -> c_9()
            le#(s(n),s(m)) -> c_10(le#(n,m))
            length#(cons(n,l)) -> c_11(length#(l))
            length#(nil()) -> c_12()
            lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                                 ,le#(length(l),n)
                                 ,length#(l)
                                 ,le#(length(toList(t)),n)
                                 ,length#(toList(t))
                                 ,toList#(t))
            lessElements#(l,t) -> c_14(lessE#(l,t,0()))
            toList#(leaf()) -> c_15()
            toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2))
        - Weak TRS:
            a() -> c()
            a() -> d()
            append(cons(n,l1),l2) -> cons(n,append(l1,l2))
            append(nil(),l2) -> l2
            if(false(),false(),l,t,n) -> lessE(l,t,s(n))
            if(false(),true(),l,t,n) -> t
            if(true(),b,l,t,n) -> l
            le(0(),m) -> true()
            le(s(n),0()) -> false()
            le(s(n),s(m)) -> le(n,m)
            length(cons(n,l)) -> s(length(l))
            length(nil()) -> 0()
            lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n)
            lessElements(l,t) -> lessE(l,t,0())
            toList(leaf()) -> nil()
            toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
        - Signature:
            {a/0,append/2,if/5,le/2,length/1,lessE/3,lessElements/2,toList/1,a#/0,append#/2,if#/5,le#/2,length#/1
            ,lessE#/3,lessElements#/2,toList#/1} / {0/0,c/0,cons/2,d/0,false/0,leaf/0,nil/0,node/3,s/1,true/0,c_1/0
            ,c_2/0,c_3/1,c_4/0,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/6,c_14/1,c_15/0,c_16/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#,append#,if#,le#,length#,lessE#,lessElements#
            ,toList#} and constructors {0,c,cons,d,false,leaf,nil,node,s,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          append(cons(n,l1),l2) -> cons(n,append(l1,l2))
          append(nil(),l2) -> l2
          le(0(),m) -> true()
          le(s(n),0()) -> false()
          le(s(n),s(m)) -> le(n,m)
          length(cons(n,l)) -> s(length(l))
          length(nil()) -> 0()
          toList(leaf()) -> nil()
          toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
          a#() -> c_1()
          a#() -> c_2()
          append#(cons(n,l1),l2) -> c_3(append#(l1,l2))
          append#(nil(),l2) -> c_4()
          if#(false(),false(),l,t,n) -> c_5(lessE#(l,t,s(n)))
          if#(false(),true(),l,t,n) -> c_6()
          if#(true(),b,l,t,n) -> c_7()
          le#(0(),m) -> c_8()
          le#(s(n),0()) -> c_9()
          le#(s(n),s(m)) -> c_10(le#(n,m))
          length#(cons(n,l)) -> c_11(length#(l))
          length#(nil()) -> c_12()
          lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                               ,le#(length(l),n)
                               ,length#(l)
                               ,le#(length(toList(t)),n)
                               ,length#(toList(t))
                               ,toList#(t))
          lessElements#(l,t) -> c_14(lessE#(l,t,0()))
          toList#(leaf()) -> c_15()
          toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2))
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            a#() -> c_1()
            a#() -> c_2()
            append#(cons(n,l1),l2) -> c_3(append#(l1,l2))
            append#(nil(),l2) -> c_4()
            if#(false(),false(),l,t,n) -> c_5(lessE#(l,t,s(n)))
            if#(false(),true(),l,t,n) -> c_6()
            if#(true(),b,l,t,n) -> c_7()
            le#(0(),m) -> c_8()
            le#(s(n),0()) -> c_9()
            le#(s(n),s(m)) -> c_10(le#(n,m))
            length#(cons(n,l)) -> c_11(length#(l))
            length#(nil()) -> c_12()
            lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                                 ,le#(length(l),n)
                                 ,length#(l)
                                 ,le#(length(toList(t)),n)
                                 ,length#(toList(t))
                                 ,toList#(t))
            lessElements#(l,t) -> c_14(lessE#(l,t,0()))
            toList#(leaf()) -> c_15()
            toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2))
        - Weak TRS:
            append(cons(n,l1),l2) -> cons(n,append(l1,l2))
            append(nil(),l2) -> l2
            le(0(),m) -> true()
            le(s(n),0()) -> false()
            le(s(n),s(m)) -> le(n,m)
            length(cons(n,l)) -> s(length(l))
            length(nil()) -> 0()
            toList(leaf()) -> nil()
            toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
        - Signature:
            {a/0,append/2,if/5,le/2,length/1,lessE/3,lessElements/2,toList/1,a#/0,append#/2,if#/5,le#/2,length#/1
            ,lessE#/3,lessElements#/2,toList#/1} / {0/0,c/0,cons/2,d/0,false/0,leaf/0,nil/0,node/3,s/1,true/0,c_1/0
            ,c_2/0,c_3/1,c_4/0,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/6,c_14/1,c_15/0,c_16/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#,append#,if#,le#,length#,lessE#,lessElements#
            ,toList#} and constructors {0,c,cons,d,false,leaf,nil,node,s,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,2,4,6,7,8,9,12,15}
        by application of
          Pre({1,2,4,6,7,8,9,12,15}) = {3,10,11,13,16}.
        Here rules are labelled as follows:
          1: a#() -> c_1()
          2: a#() -> c_2()
          3: append#(cons(n,l1),l2) -> c_3(append#(l1,l2))
          4: append#(nil(),l2) -> c_4()
          5: if#(false(),false(),l,t,n) -> c_5(lessE#(l,t,s(n)))
          6: if#(false(),true(),l,t,n) -> c_6()
          7: if#(true(),b,l,t,n) -> c_7()
          8: le#(0(),m) -> c_8()
          9: le#(s(n),0()) -> c_9()
          10: le#(s(n),s(m)) -> c_10(le#(n,m))
          11: length#(cons(n,l)) -> c_11(length#(l))
          12: length#(nil()) -> c_12()
          13: lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                                   ,le#(length(l),n)
                                   ,length#(l)
                                   ,le#(length(toList(t)),n)
                                   ,length#(toList(t))
                                   ,toList#(t))
          14: lessElements#(l,t) -> c_14(lessE#(l,t,0()))
          15: toList#(leaf()) -> c_15()
          16: toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2))
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            append#(cons(n,l1),l2) -> c_3(append#(l1,l2))
            if#(false(),false(),l,t,n) -> c_5(lessE#(l,t,s(n)))
            le#(s(n),s(m)) -> c_10(le#(n,m))
            length#(cons(n,l)) -> c_11(length#(l))
            lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                                 ,le#(length(l),n)
                                 ,length#(l)
                                 ,le#(length(toList(t)),n)
                                 ,length#(toList(t))
                                 ,toList#(t))
            lessElements#(l,t) -> c_14(lessE#(l,t,0()))
            toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2))
        - Weak DPs:
            a#() -> c_1()
            a#() -> c_2()
            append#(nil(),l2) -> c_4()
            if#(false(),true(),l,t,n) -> c_6()
            if#(true(),b,l,t,n) -> c_7()
            le#(0(),m) -> c_8()
            le#(s(n),0()) -> c_9()
            length#(nil()) -> c_12()
            toList#(leaf()) -> c_15()
        - Weak TRS:
            append(cons(n,l1),l2) -> cons(n,append(l1,l2))
            append(nil(),l2) -> l2
            le(0(),m) -> true()
            le(s(n),0()) -> false()
            le(s(n),s(m)) -> le(n,m)
            length(cons(n,l)) -> s(length(l))
            length(nil()) -> 0()
            toList(leaf()) -> nil()
            toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
        - Signature:
            {a/0,append/2,if/5,le/2,length/1,lessE/3,lessElements/2,toList/1,a#/0,append#/2,if#/5,le#/2,length#/1
            ,lessE#/3,lessElements#/2,toList#/1} / {0/0,c/0,cons/2,d/0,false/0,leaf/0,nil/0,node/3,s/1,true/0,c_1/0
            ,c_2/0,c_3/1,c_4/0,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/6,c_14/1,c_15/0,c_16/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#,append#,if#,le#,length#,lessE#,lessElements#
            ,toList#} and constructors {0,c,cons,d,false,leaf,nil,node,s,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:append#(cons(n,l1),l2) -> c_3(append#(l1,l2))
             -->_1 append#(nil(),l2) -> c_4():10
             -->_1 append#(cons(n,l1),l2) -> c_3(append#(l1,l2)):1
          
          2:S:if#(false(),false(),l,t,n) -> c_5(lessE#(l,t,s(n)))
             -->_1 lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                                        ,le#(length(l),n)
                                        ,length#(l)
                                        ,le#(length(toList(t)),n)
                                        ,length#(toList(t))
                                        ,toList#(t)):5
          
          3:S:le#(s(n),s(m)) -> c_10(le#(n,m))
             -->_1 le#(s(n),0()) -> c_9():14
             -->_1 le#(0(),m) -> c_8():13
             -->_1 le#(s(n),s(m)) -> c_10(le#(n,m)):3
          
          4:S:length#(cons(n,l)) -> c_11(length#(l))
             -->_1 length#(nil()) -> c_12():15
             -->_1 length#(cons(n,l)) -> c_11(length#(l)):4
          
          5:S:lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                                   ,le#(length(l),n)
                                   ,length#(l)
                                   ,le#(length(toList(t)),n)
                                   ,length#(toList(t))
                                   ,toList#(t))
             -->_6 toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2)):7
             -->_6 toList#(leaf()) -> c_15():16
             -->_5 length#(nil()) -> c_12():15
             -->_3 length#(nil()) -> c_12():15
             -->_4 le#(s(n),0()) -> c_9():14
             -->_2 le#(s(n),0()) -> c_9():14
             -->_4 le#(0(),m) -> c_8():13
             -->_2 le#(0(),m) -> c_8():13
             -->_1 if#(true(),b,l,t,n) -> c_7():12
             -->_1 if#(false(),true(),l,t,n) -> c_6():11
             -->_5 length#(cons(n,l)) -> c_11(length#(l)):4
             -->_3 length#(cons(n,l)) -> c_11(length#(l)):4
             -->_4 le#(s(n),s(m)) -> c_10(le#(n,m)):3
             -->_2 le#(s(n),s(m)) -> c_10(le#(n,m)):3
             -->_1 if#(false(),false(),l,t,n) -> c_5(lessE#(l,t,s(n))):2
          
          6:S:lessElements#(l,t) -> c_14(lessE#(l,t,0()))
             -->_1 lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                                        ,le#(length(l),n)
                                        ,length#(l)
                                        ,le#(length(toList(t)),n)
                                        ,length#(toList(t))
                                        ,toList#(t)):5
          
          7:S:toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2))
             -->_3 toList#(leaf()) -> c_15():16
             -->_2 toList#(leaf()) -> c_15():16
             -->_1 append#(nil(),l2) -> c_4():10
             -->_3 toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2)):7
             -->_2 toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2)):7
             -->_1 append#(cons(n,l1),l2) -> c_3(append#(l1,l2)):1
          
          8:W:a#() -> c_1()
             
          
          9:W:a#() -> c_2()
             
          
          10:W:append#(nil(),l2) -> c_4()
             
          
          11:W:if#(false(),true(),l,t,n) -> c_6()
             
          
          12:W:if#(true(),b,l,t,n) -> c_7()
             
          
          13:W:le#(0(),m) -> c_8()
             
          
          14:W:le#(s(n),0()) -> c_9()
             
          
          15:W:length#(nil()) -> c_12()
             
          
          16:W:toList#(leaf()) -> c_15()
             
          
        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()
          11: if#(false(),true(),l,t,n) -> c_6()
          12: if#(true(),b,l,t,n) -> c_7()
          13: le#(0(),m) -> c_8()
          14: le#(s(n),0()) -> c_9()
          15: length#(nil()) -> c_12()
          16: toList#(leaf()) -> c_15()
          10: append#(nil(),l2) -> c_4()
* Step 5: RemoveHeads MAYBE
    + Considered Problem:
        - Strict DPs:
            append#(cons(n,l1),l2) -> c_3(append#(l1,l2))
            if#(false(),false(),l,t,n) -> c_5(lessE#(l,t,s(n)))
            le#(s(n),s(m)) -> c_10(le#(n,m))
            length#(cons(n,l)) -> c_11(length#(l))
            lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                                 ,le#(length(l),n)
                                 ,length#(l)
                                 ,le#(length(toList(t)),n)
                                 ,length#(toList(t))
                                 ,toList#(t))
            lessElements#(l,t) -> c_14(lessE#(l,t,0()))
            toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2))
        - Weak TRS:
            append(cons(n,l1),l2) -> cons(n,append(l1,l2))
            append(nil(),l2) -> l2
            le(0(),m) -> true()
            le(s(n),0()) -> false()
            le(s(n),s(m)) -> le(n,m)
            length(cons(n,l)) -> s(length(l))
            length(nil()) -> 0()
            toList(leaf()) -> nil()
            toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
        - Signature:
            {a/0,append/2,if/5,le/2,length/1,lessE/3,lessElements/2,toList/1,a#/0,append#/2,if#/5,le#/2,length#/1
            ,lessE#/3,lessElements#/2,toList#/1} / {0/0,c/0,cons/2,d/0,false/0,leaf/0,nil/0,node/3,s/1,true/0,c_1/0
            ,c_2/0,c_3/1,c_4/0,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/6,c_14/1,c_15/0,c_16/3}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a#,append#,if#,le#,length#,lessE#,lessElements#
            ,toList#} and constructors {0,c,cons,d,false,leaf,nil,node,s,true}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:append#(cons(n,l1),l2) -> c_3(append#(l1,l2))
           -->_1 append#(cons(n,l1),l2) -> c_3(append#(l1,l2)):1
        
        2:S:if#(false(),false(),l,t,n) -> c_5(lessE#(l,t,s(n)))
           -->_1 lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                                      ,le#(length(l),n)
                                      ,length#(l)
                                      ,le#(length(toList(t)),n)
                                      ,length#(toList(t))
                                      ,toList#(t)):5
        
        3:S:le#(s(n),s(m)) -> c_10(le#(n,m))
           -->_1 le#(s(n),s(m)) -> c_10(le#(n,m)):3
        
        4:S:length#(cons(n,l)) -> c_11(length#(l))
           -->_1 length#(cons(n,l)) -> c_11(length#(l)):4
        
        5:S:lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                                 ,le#(length(l),n)
                                 ,length#(l)
                                 ,le#(length(toList(t)),n)
                                 ,length#(toList(t))
                                 ,toList#(t))
           -->_6 toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2)):7
           -->_5 length#(cons(n,l)) -> c_11(length#(l)):4
           -->_3 length#(cons(n,l)) -> c_11(length#(l)):4
           -->_4 le#(s(n),s(m)) -> c_10(le#(n,m)):3
           -->_2 le#(s(n),s(m)) -> c_10(le#(n,m)):3
           -->_1 if#(false(),false(),l,t,n) -> c_5(lessE#(l,t,s(n))):2
        
        6:S:lessElements#(l,t) -> c_14(lessE#(l,t,0()))
           -->_1 lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                                      ,le#(length(l),n)
                                      ,length#(l)
                                      ,le#(length(toList(t)),n)
                                      ,length#(toList(t))
                                      ,toList#(t)):5
        
        7:S:toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2))
           -->_3 toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2)):7
           -->_2 toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2)):7
           -->_1 append#(cons(n,l1),l2) -> c_3(append#(l1,l2)):1
        
        
        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,lessElements#(l,t) -> c_14(lessE#(l,t,0())))]
* Step 6: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          append#(cons(n,l1),l2) -> c_3(append#(l1,l2))
          if#(false(),false(),l,t,n) -> c_5(lessE#(l,t,s(n)))
          le#(s(n),s(m)) -> c_10(le#(n,m))
          length#(cons(n,l)) -> c_11(length#(l))
          lessE#(l,t,n) -> c_13(if#(le(length(l),n),le(length(toList(t)),n),l,t,n)
                               ,le#(length(l),n)
                               ,length#(l)
                               ,le#(length(toList(t)),n)
                               ,length#(toList(t))
                               ,toList#(t))
          toList#(node(t1,n,t2)) -> c_16(append#(toList(t1),cons(n,toList(t2))),toList#(t1),toList#(t2))
      - Weak TRS:
          append(cons(n,l1),l2) -> cons(n,append(l1,l2))
          append(nil(),l2) -> l2
          le(0(),m) -> true()
          le(s(n),0()) -> false()
          le(s(n),s(m)) -> le(n,m)
          length(cons(n,l)) -> s(length(l))
          length(nil()) -> 0()
          toList(leaf()) -> nil()
          toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2)))
      - Signature:
          {a/0,append/2,if/5,le/2,length/1,lessE/3,lessElements/2,toList/1,a#/0,append#/2,if#/5,le#/2,length#/1
          ,lessE#/3,lessElements#/2,toList#/1} / {0/0,c/0,cons/2,d/0,false/0,leaf/0,nil/0,node/3,s/1,true/0,c_1/0
          ,c_2/0,c_3/1,c_4/0,c_5/1,c_6/0,c_7/0,c_8/0,c_9/0,c_10/1,c_11/1,c_12/0,c_13/6,c_14/1,c_15/0,c_16/3}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {a#,append#,if#,le#,length#,lessE#,lessElements#
          ,toList#} and constructors {0,c,cons,d,false,leaf,nil,node,s,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE