MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            append(cons(x,xs),ys) -> cons(x,append(xs,ys))
            append(nil(),ys) -> ys
            dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
            dropLast(cons(x,nil())) -> nil()
            dropLast(nil()) -> nil()
            if(false(),xs,ys,zs) -> rev(xs,ys)
            if(true(),xs,ys,zs) -> zs
            isEmpty(cons(x,xs)) -> false()
            isEmpty(nil()) -> true()
            last(cons(x,cons(y,ys))) -> last(cons(y,ys))
            last(cons(x,nil())) -> x
            rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
            reverse(xs) -> rev(xs,nil())
        - Signature:
            {append/2,dropLast/1,if/4,isEmpty/1,last/1,rev/2,reverse/1} / {cons/2,false/0,nil/0,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append,dropLast,if,isEmpty,last,rev
            ,reverse} and constructors {cons,false,nil,true}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
          append#(nil(),ys) -> c_2()
          dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys)))
          dropLast#(cons(x,nil())) -> c_4()
          dropLast#(nil()) -> c_5()
          if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys))
          if#(true(),xs,ys,zs) -> c_7()
          isEmpty#(cons(x,xs)) -> c_8()
          isEmpty#(nil()) -> c_9()
          last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys)))
          last#(cons(x,nil())) -> c_11()
          rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                             ,isEmpty#(xs)
                             ,dropLast#(xs)
                             ,append#(ys,last(xs))
                             ,last#(xs))
          reverse#(xs) -> c_13(rev#(xs,nil()))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
            append#(nil(),ys) -> c_2()
            dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys)))
            dropLast#(cons(x,nil())) -> c_4()
            dropLast#(nil()) -> c_5()
            if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys))
            if#(true(),xs,ys,zs) -> c_7()
            isEmpty#(cons(x,xs)) -> c_8()
            isEmpty#(nil()) -> c_9()
            last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys)))
            last#(cons(x,nil())) -> c_11()
            rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                               ,isEmpty#(xs)
                               ,dropLast#(xs)
                               ,append#(ys,last(xs))
                               ,last#(xs))
            reverse#(xs) -> c_13(rev#(xs,nil()))
        - Weak TRS:
            append(cons(x,xs),ys) -> cons(x,append(xs,ys))
            append(nil(),ys) -> ys
            dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
            dropLast(cons(x,nil())) -> nil()
            dropLast(nil()) -> nil()
            if(false(),xs,ys,zs) -> rev(xs,ys)
            if(true(),xs,ys,zs) -> zs
            isEmpty(cons(x,xs)) -> false()
            isEmpty(nil()) -> true()
            last(cons(x,cons(y,ys))) -> last(cons(y,ys))
            last(cons(x,nil())) -> x
            rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
            reverse(xs) -> rev(xs,nil())
        - Signature:
            {append/2,dropLast/1,if/4,isEmpty/1,last/1,rev/2,reverse/1,append#/2,dropLast#/1,if#/4,isEmpty#/1,last#/1
            ,rev#/2,reverse#/1} / {cons/2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0
            ,c_10/1,c_11/0,c_12/5,c_13/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,dropLast#,if#,isEmpty#,last#,rev#
            ,reverse#} and constructors {cons,false,nil,true}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          append(cons(x,xs),ys) -> cons(x,append(xs,ys))
          append(nil(),ys) -> ys
          dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
          dropLast(cons(x,nil())) -> nil()
          dropLast(nil()) -> nil()
          isEmpty(cons(x,xs)) -> false()
          isEmpty(nil()) -> true()
          last(cons(x,cons(y,ys))) -> last(cons(y,ys))
          last(cons(x,nil())) -> x
          append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
          append#(nil(),ys) -> c_2()
          dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys)))
          dropLast#(cons(x,nil())) -> c_4()
          dropLast#(nil()) -> c_5()
          if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys))
          if#(true(),xs,ys,zs) -> c_7()
          isEmpty#(cons(x,xs)) -> c_8()
          isEmpty#(nil()) -> c_9()
          last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys)))
          last#(cons(x,nil())) -> c_11()
          rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                             ,isEmpty#(xs)
                             ,dropLast#(xs)
                             ,append#(ys,last(xs))
                             ,last#(xs))
          reverse#(xs) -> c_13(rev#(xs,nil()))
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
            append#(nil(),ys) -> c_2()
            dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys)))
            dropLast#(cons(x,nil())) -> c_4()
            dropLast#(nil()) -> c_5()
            if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys))
            if#(true(),xs,ys,zs) -> c_7()
            isEmpty#(cons(x,xs)) -> c_8()
            isEmpty#(nil()) -> c_9()
            last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys)))
            last#(cons(x,nil())) -> c_11()
            rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                               ,isEmpty#(xs)
                               ,dropLast#(xs)
                               ,append#(ys,last(xs))
                               ,last#(xs))
            reverse#(xs) -> c_13(rev#(xs,nil()))
        - Weak TRS:
            append(cons(x,xs),ys) -> cons(x,append(xs,ys))
            append(nil(),ys) -> ys
            dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
            dropLast(cons(x,nil())) -> nil()
            dropLast(nil()) -> nil()
            isEmpty(cons(x,xs)) -> false()
            isEmpty(nil()) -> true()
            last(cons(x,cons(y,ys))) -> last(cons(y,ys))
            last(cons(x,nil())) -> x
        - Signature:
            {append/2,dropLast/1,if/4,isEmpty/1,last/1,rev/2,reverse/1,append#/2,dropLast#/1,if#/4,isEmpty#/1,last#/1
            ,rev#/2,reverse#/1} / {cons/2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0
            ,c_10/1,c_11/0,c_12/5,c_13/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,dropLast#,if#,isEmpty#,last#,rev#
            ,reverse#} and constructors {cons,false,nil,true}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2,4,5,7,8,9,11}
        by application of
          Pre({2,4,5,7,8,9,11}) = {1,3,10,12}.
        Here rules are labelled as follows:
          1: append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
          2: append#(nil(),ys) -> c_2()
          3: dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys)))
          4: dropLast#(cons(x,nil())) -> c_4()
          5: dropLast#(nil()) -> c_5()
          6: if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys))
          7: if#(true(),xs,ys,zs) -> c_7()
          8: isEmpty#(cons(x,xs)) -> c_8()
          9: isEmpty#(nil()) -> c_9()
          10: last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys)))
          11: last#(cons(x,nil())) -> c_11()
          12: rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                                 ,isEmpty#(xs)
                                 ,dropLast#(xs)
                                 ,append#(ys,last(xs))
                                 ,last#(xs))
          13: reverse#(xs) -> c_13(rev#(xs,nil()))
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
            dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys)))
            if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys))
            last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys)))
            rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                               ,isEmpty#(xs)
                               ,dropLast#(xs)
                               ,append#(ys,last(xs))
                               ,last#(xs))
            reverse#(xs) -> c_13(rev#(xs,nil()))
        - Weak DPs:
            append#(nil(),ys) -> c_2()
            dropLast#(cons(x,nil())) -> c_4()
            dropLast#(nil()) -> c_5()
            if#(true(),xs,ys,zs) -> c_7()
            isEmpty#(cons(x,xs)) -> c_8()
            isEmpty#(nil()) -> c_9()
            last#(cons(x,nil())) -> c_11()
        - Weak TRS:
            append(cons(x,xs),ys) -> cons(x,append(xs,ys))
            append(nil(),ys) -> ys
            dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
            dropLast(cons(x,nil())) -> nil()
            dropLast(nil()) -> nil()
            isEmpty(cons(x,xs)) -> false()
            isEmpty(nil()) -> true()
            last(cons(x,cons(y,ys))) -> last(cons(y,ys))
            last(cons(x,nil())) -> x
        - Signature:
            {append/2,dropLast/1,if/4,isEmpty/1,last/1,rev/2,reverse/1,append#/2,dropLast#/1,if#/4,isEmpty#/1,last#/1
            ,rev#/2,reverse#/1} / {cons/2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0
            ,c_10/1,c_11/0,c_12/5,c_13/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,dropLast#,if#,isEmpty#,last#,rev#
            ,reverse#} and constructors {cons,false,nil,true}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
             -->_1 append#(nil(),ys) -> c_2():7
             -->_1 append#(cons(x,xs),ys) -> c_1(append#(xs,ys)):1
          
          2:S:dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys)))
             -->_1 dropLast#(cons(x,nil())) -> c_4():8
             -->_1 dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys))):2
          
          3:S:if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys))
             -->_1 rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                                      ,isEmpty#(xs)
                                      ,dropLast#(xs)
                                      ,append#(ys,last(xs))
                                      ,last#(xs)):5
          
          4:S:last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys)))
             -->_1 last#(cons(x,nil())) -> c_11():13
             -->_1 last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys))):4
          
          5:S:rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                                 ,isEmpty#(xs)
                                 ,dropLast#(xs)
                                 ,append#(ys,last(xs))
                                 ,last#(xs))
             -->_5 last#(cons(x,nil())) -> c_11():13
             -->_2 isEmpty#(nil()) -> c_9():12
             -->_2 isEmpty#(cons(x,xs)) -> c_8():11
             -->_1 if#(true(),xs,ys,zs) -> c_7():10
             -->_3 dropLast#(nil()) -> c_5():9
             -->_3 dropLast#(cons(x,nil())) -> c_4():8
             -->_4 append#(nil(),ys) -> c_2():7
             -->_5 last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys))):4
             -->_1 if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys)):3
             -->_3 dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys))):2
             -->_4 append#(cons(x,xs),ys) -> c_1(append#(xs,ys)):1
          
          6:S:reverse#(xs) -> c_13(rev#(xs,nil()))
             -->_1 rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                                      ,isEmpty#(xs)
                                      ,dropLast#(xs)
                                      ,append#(ys,last(xs))
                                      ,last#(xs)):5
          
          7:W:append#(nil(),ys) -> c_2()
             
          
          8:W:dropLast#(cons(x,nil())) -> c_4()
             
          
          9:W:dropLast#(nil()) -> c_5()
             
          
          10:W:if#(true(),xs,ys,zs) -> c_7()
             
          
          11:W:isEmpty#(cons(x,xs)) -> c_8()
             
          
          12:W:isEmpty#(nil()) -> c_9()
             
          
          13:W:last#(cons(x,nil())) -> c_11()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          9: dropLast#(nil()) -> c_5()
          10: if#(true(),xs,ys,zs) -> c_7()
          11: isEmpty#(cons(x,xs)) -> c_8()
          12: isEmpty#(nil()) -> c_9()
          13: last#(cons(x,nil())) -> c_11()
          8: dropLast#(cons(x,nil())) -> c_4()
          7: append#(nil(),ys) -> c_2()
* Step 5: SimplifyRHS MAYBE
    + Considered Problem:
        - Strict DPs:
            append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
            dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys)))
            if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys))
            last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys)))
            rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                               ,isEmpty#(xs)
                               ,dropLast#(xs)
                               ,append#(ys,last(xs))
                               ,last#(xs))
            reverse#(xs) -> c_13(rev#(xs,nil()))
        - Weak TRS:
            append(cons(x,xs),ys) -> cons(x,append(xs,ys))
            append(nil(),ys) -> ys
            dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
            dropLast(cons(x,nil())) -> nil()
            dropLast(nil()) -> nil()
            isEmpty(cons(x,xs)) -> false()
            isEmpty(nil()) -> true()
            last(cons(x,cons(y,ys))) -> last(cons(y,ys))
            last(cons(x,nil())) -> x
        - Signature:
            {append/2,dropLast/1,if/4,isEmpty/1,last/1,rev/2,reverse/1,append#/2,dropLast#/1,if#/4,isEmpty#/1,last#/1
            ,rev#/2,reverse#/1} / {cons/2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0
            ,c_10/1,c_11/0,c_12/5,c_13/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,dropLast#,if#,isEmpty#,last#,rev#
            ,reverse#} and constructors {cons,false,nil,true}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
             -->_1 append#(cons(x,xs),ys) -> c_1(append#(xs,ys)):1
          
          2:S:dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys)))
             -->_1 dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys))):2
          
          3:S:if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys))
             -->_1 rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                                      ,isEmpty#(xs)
                                      ,dropLast#(xs)
                                      ,append#(ys,last(xs))
                                      ,last#(xs)):5
          
          4:S:last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys)))
             -->_1 last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys))):4
          
          5:S:rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                                 ,isEmpty#(xs)
                                 ,dropLast#(xs)
                                 ,append#(ys,last(xs))
                                 ,last#(xs))
             -->_5 last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys))):4
             -->_1 if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys)):3
             -->_3 dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys))):2
             -->_4 append#(cons(x,xs),ys) -> c_1(append#(xs,ys)):1
          
          6:S:reverse#(xs) -> c_13(rev#(xs,nil()))
             -->_1 rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                                      ,isEmpty#(xs)
                                      ,dropLast#(xs)
                                      ,append#(ys,last(xs))
                                      ,last#(xs)):5
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                             ,dropLast#(xs)
                             ,append#(ys,last(xs))
                             ,last#(xs))
* Step 6: RemoveHeads MAYBE
    + Considered Problem:
        - Strict DPs:
            append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
            dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys)))
            if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys))
            last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys)))
            rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                               ,dropLast#(xs)
                               ,append#(ys,last(xs))
                               ,last#(xs))
            reverse#(xs) -> c_13(rev#(xs,nil()))
        - Weak TRS:
            append(cons(x,xs),ys) -> cons(x,append(xs,ys))
            append(nil(),ys) -> ys
            dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
            dropLast(cons(x,nil())) -> nil()
            dropLast(nil()) -> nil()
            isEmpty(cons(x,xs)) -> false()
            isEmpty(nil()) -> true()
            last(cons(x,cons(y,ys))) -> last(cons(y,ys))
            last(cons(x,nil())) -> x
        - Signature:
            {append/2,dropLast/1,if/4,isEmpty/1,last/1,rev/2,reverse/1,append#/2,dropLast#/1,if#/4,isEmpty#/1,last#/1
            ,rev#/2,reverse#/1} / {cons/2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0
            ,c_10/1,c_11/0,c_12/4,c_13/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {append#,dropLast#,if#,isEmpty#,last#,rev#
            ,reverse#} and constructors {cons,false,nil,true}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
           -->_1 append#(cons(x,xs),ys) -> c_1(append#(xs,ys)):1
        
        2:S:dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys)))
           -->_1 dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys))):2
        
        3:S:if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys))
           -->_1 rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                                    ,dropLast#(xs)
                                    ,append#(ys,last(xs))
                                    ,last#(xs)):5
        
        4:S:last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys)))
           -->_1 last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys))):4
        
        5:S:rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                               ,dropLast#(xs)
                               ,append#(ys,last(xs))
                               ,last#(xs))
           -->_4 last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys))):4
           -->_1 if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys)):3
           -->_2 dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys))):2
           -->_3 append#(cons(x,xs),ys) -> c_1(append#(xs,ys)):1
        
        6:S:reverse#(xs) -> c_13(rev#(xs,nil()))
           -->_1 rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                                    ,dropLast#(xs)
                                    ,append#(ys,last(xs))
                                    ,last#(xs)):5
        
        
        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,reverse#(xs) -> c_13(rev#(xs,nil())))]
* Step 7: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          append#(cons(x,xs),ys) -> c_1(append#(xs,ys))
          dropLast#(cons(x,cons(y,ys))) -> c_3(dropLast#(cons(y,ys)))
          if#(false(),xs,ys,zs) -> c_6(rev#(xs,ys))
          last#(cons(x,cons(y,ys))) -> c_10(last#(cons(y,ys)))
          rev#(xs,ys) -> c_12(if#(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
                             ,dropLast#(xs)
                             ,append#(ys,last(xs))
                             ,last#(xs))
      - Weak TRS:
          append(cons(x,xs),ys) -> cons(x,append(xs,ys))
          append(nil(),ys) -> ys
          dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
          dropLast(cons(x,nil())) -> nil()
          dropLast(nil()) -> nil()
          isEmpty(cons(x,xs)) -> false()
          isEmpty(nil()) -> true()
          last(cons(x,cons(y,ys))) -> last(cons(y,ys))
          last(cons(x,nil())) -> x
      - Signature:
          {append/2,dropLast/1,if/4,isEmpty/1,last/1,rev/2,reverse/1,append#/2,dropLast#/1,if#/4,isEmpty#/1,last#/1
          ,rev#/2,reverse#/1} / {cons/2,false/0,nil/0,true/0,c_1/1,c_2/0,c_3/1,c_4/0,c_5/0,c_6/1,c_7/0,c_8/0,c_9/0
          ,c_10/1,c_11/0,c_12/4,c_13/1}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {append#,dropLast#,if#,isEmpty#,last#,rev#
          ,reverse#} and constructors {cons,false,nil,true}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE