MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            goal(xs) -> permute(xs)
            mapconsapp(x,Nil(),rest) -> rest
            mapconsapp(x',Cons(x,xs),rest) -> Cons(Cons(x',x),mapconsapp(x',xs,rest))
            permute(Cons(x,xs)) -> select(x,Nil(),xs)
            permute(Nil()) -> Cons(Nil(),Nil())
            revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
            revapp(Nil(),rest) -> rest
            select(x,revprefix,Nil()) -> mapconsapp(x,permute(revapp(revprefix,Nil())),Nil())
            select(x',revprefix,Cons(x,xs)) -> mapconsapp(x'
                                                         ,permute(revapp(revprefix,Cons(x,xs)))
                                                         ,select(x,Cons(x',revprefix),xs))
        - Signature:
            {goal/1,mapconsapp/3,permute/1,revapp/2,select/3} / {Cons/2,Nil/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {goal,mapconsapp,permute,revapp
            ,select} and constructors {Cons,Nil}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          goal#(xs) -> c_1(permute#(xs))
          mapconsapp#(x,Nil(),rest) -> c_2()
          mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest))
          permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs))
          permute#(Nil()) -> c_5()
          revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest)))
          revapp#(Nil(),rest) -> c_7()
          select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                           ,permute#(revapp(revprefix,Nil()))
                                           ,revapp#(revprefix,Nil()))
          select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                             ,permute(revapp(revprefix,Cons(x,xs)))
                                                             ,select(x,Cons(x',revprefix),xs))
                                                 ,permute#(revapp(revprefix,Cons(x,xs)))
                                                 ,revapp#(revprefix,Cons(x,xs))
                                                 ,select#(x,Cons(x',revprefix),xs))
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: UsableRules MAYBE
    + Considered Problem:
        - Strict DPs:
            goal#(xs) -> c_1(permute#(xs))
            mapconsapp#(x,Nil(),rest) -> c_2()
            mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest))
            permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs))
            permute#(Nil()) -> c_5()
            revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest)))
            revapp#(Nil(),rest) -> c_7()
            select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                             ,permute#(revapp(revprefix,Nil()))
                                             ,revapp#(revprefix,Nil()))
            select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                               ,permute(revapp(revprefix,Cons(x,xs)))
                                                               ,select(x,Cons(x',revprefix),xs))
                                                   ,permute#(revapp(revprefix,Cons(x,xs)))
                                                   ,revapp#(revprefix,Cons(x,xs))
                                                   ,select#(x,Cons(x',revprefix),xs))
        - Weak TRS:
            goal(xs) -> permute(xs)
            mapconsapp(x,Nil(),rest) -> rest
            mapconsapp(x',Cons(x,xs),rest) -> Cons(Cons(x',x),mapconsapp(x',xs,rest))
            permute(Cons(x,xs)) -> select(x,Nil(),xs)
            permute(Nil()) -> Cons(Nil(),Nil())
            revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
            revapp(Nil(),rest) -> rest
            select(x,revprefix,Nil()) -> mapconsapp(x,permute(revapp(revprefix,Nil())),Nil())
            select(x',revprefix,Cons(x,xs)) -> mapconsapp(x'
                                                         ,permute(revapp(revprefix,Cons(x,xs)))
                                                         ,select(x,Cons(x',revprefix),xs))
        - Signature:
            {goal/1,mapconsapp/3,permute/1,revapp/2,select/3,goal#/1,mapconsapp#/3,permute#/1,revapp#/2
            ,select#/3} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0,c_8/3,c_9/4}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {goal#,mapconsapp#,permute#,revapp#
            ,select#} and constructors {Cons,Nil}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          mapconsapp(x,Nil(),rest) -> rest
          mapconsapp(x',Cons(x,xs),rest) -> Cons(Cons(x',x),mapconsapp(x',xs,rest))
          permute(Cons(x,xs)) -> select(x,Nil(),xs)
          permute(Nil()) -> Cons(Nil(),Nil())
          revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
          revapp(Nil(),rest) -> rest
          select(x,revprefix,Nil()) -> mapconsapp(x,permute(revapp(revprefix,Nil())),Nil())
          select(x',revprefix,Cons(x,xs)) -> mapconsapp(x'
                                                       ,permute(revapp(revprefix,Cons(x,xs)))
                                                       ,select(x,Cons(x',revprefix),xs))
          goal#(xs) -> c_1(permute#(xs))
          mapconsapp#(x,Nil(),rest) -> c_2()
          mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest))
          permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs))
          permute#(Nil()) -> c_5()
          revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest)))
          revapp#(Nil(),rest) -> c_7()
          select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                           ,permute#(revapp(revprefix,Nil()))
                                           ,revapp#(revprefix,Nil()))
          select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                             ,permute(revapp(revprefix,Cons(x,xs)))
                                                             ,select(x,Cons(x',revprefix),xs))
                                                 ,permute#(revapp(revprefix,Cons(x,xs)))
                                                 ,revapp#(revprefix,Cons(x,xs))
                                                 ,select#(x,Cons(x',revprefix),xs))
* Step 3: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            goal#(xs) -> c_1(permute#(xs))
            mapconsapp#(x,Nil(),rest) -> c_2()
            mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest))
            permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs))
            permute#(Nil()) -> c_5()
            revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest)))
            revapp#(Nil(),rest) -> c_7()
            select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                             ,permute#(revapp(revprefix,Nil()))
                                             ,revapp#(revprefix,Nil()))
            select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                               ,permute(revapp(revprefix,Cons(x,xs)))
                                                               ,select(x,Cons(x',revprefix),xs))
                                                   ,permute#(revapp(revprefix,Cons(x,xs)))
                                                   ,revapp#(revprefix,Cons(x,xs))
                                                   ,select#(x,Cons(x',revprefix),xs))
        - Weak TRS:
            mapconsapp(x,Nil(),rest) -> rest
            mapconsapp(x',Cons(x,xs),rest) -> Cons(Cons(x',x),mapconsapp(x',xs,rest))
            permute(Cons(x,xs)) -> select(x,Nil(),xs)
            permute(Nil()) -> Cons(Nil(),Nil())
            revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
            revapp(Nil(),rest) -> rest
            select(x,revprefix,Nil()) -> mapconsapp(x,permute(revapp(revprefix,Nil())),Nil())
            select(x',revprefix,Cons(x,xs)) -> mapconsapp(x'
                                                         ,permute(revapp(revprefix,Cons(x,xs)))
                                                         ,select(x,Cons(x',revprefix),xs))
        - Signature:
            {goal/1,mapconsapp/3,permute/1,revapp/2,select/3,goal#/1,mapconsapp#/3,permute#/1,revapp#/2
            ,select#/3} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0,c_8/3,c_9/4}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {goal#,mapconsapp#,permute#,revapp#
            ,select#} and constructors {Cons,Nil}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {2,5,7}
        by application of
          Pre({2,5,7}) = {1,3,6,8,9}.
        Here rules are labelled as follows:
          1: goal#(xs) -> c_1(permute#(xs))
          2: mapconsapp#(x,Nil(),rest) -> c_2()
          3: mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest))
          4: permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs))
          5: permute#(Nil()) -> c_5()
          6: revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest)))
          7: revapp#(Nil(),rest) -> c_7()
          8: select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                              ,permute#(revapp(revprefix,Nil()))
                                              ,revapp#(revprefix,Nil()))
          9: select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                                ,permute(revapp(revprefix,Cons(x,xs)))
                                                                ,select(x,Cons(x',revprefix),xs))
                                                    ,permute#(revapp(revprefix,Cons(x,xs)))
                                                    ,revapp#(revprefix,Cons(x,xs))
                                                    ,select#(x,Cons(x',revprefix),xs))
* Step 4: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            goal#(xs) -> c_1(permute#(xs))
            mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest))
            permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs))
            revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest)))
            select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                             ,permute#(revapp(revprefix,Nil()))
                                             ,revapp#(revprefix,Nil()))
            select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                               ,permute(revapp(revprefix,Cons(x,xs)))
                                                               ,select(x,Cons(x',revprefix),xs))
                                                   ,permute#(revapp(revprefix,Cons(x,xs)))
                                                   ,revapp#(revprefix,Cons(x,xs))
                                                   ,select#(x,Cons(x',revprefix),xs))
        - Weak DPs:
            mapconsapp#(x,Nil(),rest) -> c_2()
            permute#(Nil()) -> c_5()
            revapp#(Nil(),rest) -> c_7()
        - Weak TRS:
            mapconsapp(x,Nil(),rest) -> rest
            mapconsapp(x',Cons(x,xs),rest) -> Cons(Cons(x',x),mapconsapp(x',xs,rest))
            permute(Cons(x,xs)) -> select(x,Nil(),xs)
            permute(Nil()) -> Cons(Nil(),Nil())
            revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
            revapp(Nil(),rest) -> rest
            select(x,revprefix,Nil()) -> mapconsapp(x,permute(revapp(revprefix,Nil())),Nil())
            select(x',revprefix,Cons(x,xs)) -> mapconsapp(x'
                                                         ,permute(revapp(revprefix,Cons(x,xs)))
                                                         ,select(x,Cons(x',revprefix),xs))
        - Signature:
            {goal/1,mapconsapp/3,permute/1,revapp/2,select/3,goal#/1,mapconsapp#/3,permute#/1,revapp#/2
            ,select#/3} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0,c_8/3,c_9/4}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {goal#,mapconsapp#,permute#,revapp#
            ,select#} and constructors {Cons,Nil}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:goal#(xs) -> c_1(permute#(xs))
             -->_1 permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs)):3
             -->_1 permute#(Nil()) -> c_5():8
          
          2:S:mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest))
             -->_1 mapconsapp#(x,Nil(),rest) -> c_2():7
             -->_1 mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest)):2
          
          3:S:permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs))
             -->_1 select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                                      ,permute(revapp(revprefix,Cons(x,xs)))
                                                                      ,select(x,Cons(x',revprefix),xs))
                                                          ,permute#(revapp(revprefix,Cons(x,xs)))
                                                          ,revapp#(revprefix,Cons(x,xs))
                                                          ,select#(x,Cons(x',revprefix),xs)):6
             -->_1 select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                                    ,permute#(revapp(revprefix,Nil()))
                                                    ,revapp#(revprefix,Nil())):5
          
          4:S:revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest)))
             -->_1 revapp#(Nil(),rest) -> c_7():9
             -->_1 revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest))):4
          
          5:S:select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                               ,permute#(revapp(revprefix,Nil()))
                                               ,revapp#(revprefix,Nil()))
             -->_3 revapp#(Nil(),rest) -> c_7():9
             -->_2 permute#(Nil()) -> c_5():8
             -->_1 mapconsapp#(x,Nil(),rest) -> c_2():7
             -->_3 revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest))):4
             -->_2 permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs)):3
             -->_1 mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest)):2
          
          6:S:select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                                 ,permute(revapp(revprefix,Cons(x,xs)))
                                                                 ,select(x,Cons(x',revprefix),xs))
                                                     ,permute#(revapp(revprefix,Cons(x,xs)))
                                                     ,revapp#(revprefix,Cons(x,xs))
                                                     ,select#(x,Cons(x',revprefix),xs))
             -->_3 revapp#(Nil(),rest) -> c_7():9
             -->_2 permute#(Nil()) -> c_5():8
             -->_1 mapconsapp#(x,Nil(),rest) -> c_2():7
             -->_4 select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                                      ,permute(revapp(revprefix,Cons(x,xs)))
                                                                      ,select(x,Cons(x',revprefix),xs))
                                                          ,permute#(revapp(revprefix,Cons(x,xs)))
                                                          ,revapp#(revprefix,Cons(x,xs))
                                                          ,select#(x,Cons(x',revprefix),xs)):6
             -->_4 select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                                    ,permute#(revapp(revprefix,Nil()))
                                                    ,revapp#(revprefix,Nil())):5
             -->_3 revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest))):4
             -->_2 permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs)):3
             -->_1 mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest)):2
          
          7:W:mapconsapp#(x,Nil(),rest) -> c_2()
             
          
          8:W:permute#(Nil()) -> c_5()
             
          
          9:W:revapp#(Nil(),rest) -> c_7()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          7: mapconsapp#(x,Nil(),rest) -> c_2()
          8: permute#(Nil()) -> c_5()
          9: revapp#(Nil(),rest) -> c_7()
* Step 5: RemoveHeads MAYBE
    + Considered Problem:
        - Strict DPs:
            goal#(xs) -> c_1(permute#(xs))
            mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest))
            permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs))
            revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest)))
            select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                             ,permute#(revapp(revprefix,Nil()))
                                             ,revapp#(revprefix,Nil()))
            select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                               ,permute(revapp(revprefix,Cons(x,xs)))
                                                               ,select(x,Cons(x',revprefix),xs))
                                                   ,permute#(revapp(revprefix,Cons(x,xs)))
                                                   ,revapp#(revprefix,Cons(x,xs))
                                                   ,select#(x,Cons(x',revprefix),xs))
        - Weak TRS:
            mapconsapp(x,Nil(),rest) -> rest
            mapconsapp(x',Cons(x,xs),rest) -> Cons(Cons(x',x),mapconsapp(x',xs,rest))
            permute(Cons(x,xs)) -> select(x,Nil(),xs)
            permute(Nil()) -> Cons(Nil(),Nil())
            revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
            revapp(Nil(),rest) -> rest
            select(x,revprefix,Nil()) -> mapconsapp(x,permute(revapp(revprefix,Nil())),Nil())
            select(x',revprefix,Cons(x,xs)) -> mapconsapp(x'
                                                         ,permute(revapp(revprefix,Cons(x,xs)))
                                                         ,select(x,Cons(x',revprefix),xs))
        - Signature:
            {goal/1,mapconsapp/3,permute/1,revapp/2,select/3,goal#/1,mapconsapp#/3,permute#/1,revapp#/2
            ,select#/3} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0,c_8/3,c_9/4}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {goal#,mapconsapp#,permute#,revapp#
            ,select#} and constructors {Cons,Nil}
    + Applied Processor:
        RemoveHeads
    + Details:
        Consider the dependency graph
        
        1:S:goal#(xs) -> c_1(permute#(xs))
           -->_1 permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs)):3
        
        2:S:mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest))
           -->_1 mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest)):2
        
        3:S:permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs))
           -->_1 select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                                    ,permute(revapp(revprefix,Cons(x,xs)))
                                                                    ,select(x,Cons(x',revprefix),xs))
                                                        ,permute#(revapp(revprefix,Cons(x,xs)))
                                                        ,revapp#(revprefix,Cons(x,xs))
                                                        ,select#(x,Cons(x',revprefix),xs)):6
           -->_1 select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                                  ,permute#(revapp(revprefix,Nil()))
                                                  ,revapp#(revprefix,Nil())):5
        
        4:S:revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest)))
           -->_1 revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest))):4
        
        5:S:select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                             ,permute#(revapp(revprefix,Nil()))
                                             ,revapp#(revprefix,Nil()))
           -->_3 revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest))):4
           -->_2 permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs)):3
           -->_1 mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest)):2
        
        6:S:select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                               ,permute(revapp(revprefix,Cons(x,xs)))
                                                               ,select(x,Cons(x',revprefix),xs))
                                                   ,permute#(revapp(revprefix,Cons(x,xs)))
                                                   ,revapp#(revprefix,Cons(x,xs))
                                                   ,select#(x,Cons(x',revprefix),xs))
           -->_4 select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                                    ,permute(revapp(revprefix,Cons(x,xs)))
                                                                    ,select(x,Cons(x',revprefix),xs))
                                                        ,permute#(revapp(revprefix,Cons(x,xs)))
                                                        ,revapp#(revprefix,Cons(x,xs))
                                                        ,select#(x,Cons(x',revprefix),xs)):6
           -->_4 select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                                  ,permute#(revapp(revprefix,Nil()))
                                                  ,revapp#(revprefix,Nil())):5
           -->_3 revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest))):4
           -->_2 permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs)):3
           -->_1 mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest)):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).
        
        [(1,goal#(xs) -> c_1(permute#(xs)))]
* Step 6: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          mapconsapp#(x',Cons(x,xs),rest) -> c_3(mapconsapp#(x',xs,rest))
          permute#(Cons(x,xs)) -> c_4(select#(x,Nil(),xs))
          revapp#(Cons(x,xs),rest) -> c_6(revapp#(xs,Cons(x,rest)))
          select#(x,revprefix,Nil()) -> c_8(mapconsapp#(x,permute(revapp(revprefix,Nil())),Nil())
                                           ,permute#(revapp(revprefix,Nil()))
                                           ,revapp#(revprefix,Nil()))
          select#(x',revprefix,Cons(x,xs)) -> c_9(mapconsapp#(x'
                                                             ,permute(revapp(revprefix,Cons(x,xs)))
                                                             ,select(x,Cons(x',revprefix),xs))
                                                 ,permute#(revapp(revprefix,Cons(x,xs)))
                                                 ,revapp#(revprefix,Cons(x,xs))
                                                 ,select#(x,Cons(x',revprefix),xs))
      - Weak TRS:
          mapconsapp(x,Nil(),rest) -> rest
          mapconsapp(x',Cons(x,xs),rest) -> Cons(Cons(x',x),mapconsapp(x',xs,rest))
          permute(Cons(x,xs)) -> select(x,Nil(),xs)
          permute(Nil()) -> Cons(Nil(),Nil())
          revapp(Cons(x,xs),rest) -> revapp(xs,Cons(x,rest))
          revapp(Nil(),rest) -> rest
          select(x,revprefix,Nil()) -> mapconsapp(x,permute(revapp(revprefix,Nil())),Nil())
          select(x',revprefix,Cons(x,xs)) -> mapconsapp(x'
                                                       ,permute(revapp(revprefix,Cons(x,xs)))
                                                       ,select(x,Cons(x',revprefix),xs))
      - Signature:
          {goal/1,mapconsapp/3,permute/1,revapp/2,select/3,goal#/1,mapconsapp#/3,permute#/1,revapp#/2
          ,select#/3} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/1,c_7/0,c_8/3,c_9/4}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {goal#,mapconsapp#,permute#,revapp#
          ,select#} and constructors {Cons,Nil}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE