*** 1 Progress [(?,O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
        append(Nil(),ys) -> ys
        goal(xs) -> shuffle(xs)
        reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
        reverse(Nil()) -> Nil()
        shuffle(Cons(x,xs)) -> Cons(x,shuffle(reverse(xs)))
        shuffle(Nil()) -> Nil()
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {append/2,goal/1,reverse/1,shuffle/1} / {Cons/2,Nil/0}
      Obligation:
        Innermost
        basic terms: {append,goal,reverse,shuffle}/{Cons,Nil}
    Applied Processor:
      DependencyPairs {dpKind_ = DT}
    Proof:
      We add the following dependency tuples:
      
      Strict DPs
        append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
        append#(Nil(),ys) -> c_2()
        goal#(xs) -> c_3(shuffle#(xs))
        reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
        reverse#(Nil()) -> c_5()
        shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
        shuffle#(Nil()) -> c_7()
      Weak DPs
        
      
      and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
        append#(Nil(),ys) -> c_2()
        goal#(xs) -> c_3(shuffle#(xs))
        reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
        reverse#(Nil()) -> c_5()
        shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
        shuffle#(Nil()) -> c_7()
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
        append(Nil(),ys) -> ys
        goal(xs) -> shuffle(xs)
        reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
        reverse(Nil()) -> Nil()
        shuffle(Cons(x,xs)) -> Cons(x,shuffle(reverse(xs)))
        shuffle(Nil()) -> Nil()
      Signature:
        {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
      Obligation:
        Innermost
        basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
    Applied Processor:
      UsableRules
    Proof:
      We replace rewrite rules by usable rules:
        append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
        append(Nil(),ys) -> ys
        reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
        reverse(Nil()) -> Nil()
        append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
        append#(Nil(),ys) -> c_2()
        goal#(xs) -> c_3(shuffle#(xs))
        reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
        reverse#(Nil()) -> c_5()
        shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
        shuffle#(Nil()) -> c_7()
*** 1.1.1 Progress [(?,O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
        append#(Nil(),ys) -> c_2()
        goal#(xs) -> c_3(shuffle#(xs))
        reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
        reverse#(Nil()) -> c_5()
        shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
        shuffle#(Nil()) -> c_7()
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
        append(Nil(),ys) -> ys
        reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
        reverse(Nil()) -> Nil()
      Signature:
        {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
      Obligation:
        Innermost
        basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
    Applied Processor:
      PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    Proof:
      We estimate the number of application of
        {2,5,7}
      by application of
        Pre({2,5,7}) = {1,3,4,6}.
      Here rules are labelled as follows:
        1: append#(Cons(x,xs),ys) ->     
             c_1(append#(xs,ys))         
        2: append#(Nil(),ys) -> c_2()    
        3: goal#(xs) -> c_3(shuffle#(xs))
        4: reverse#(Cons(x,xs)) ->       
             c_4(append#(reverse(xs)     
                        ,Cons(x,Nil()))  
                ,reverse#(xs))           
        5: reverse#(Nil()) -> c_5()      
        6: shuffle#(Cons(x,xs)) ->       
             c_6(shuffle#(reverse(xs))   
                ,reverse#(xs))           
        7: shuffle#(Nil()) -> c_7()      
*** 1.1.1.1 Progress [(?,O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
        goal#(xs) -> c_3(shuffle#(xs))
        reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
        shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
      Strict TRS Rules:
        
      Weak DP Rules:
        append#(Nil(),ys) -> c_2()
        reverse#(Nil()) -> c_5()
        shuffle#(Nil()) -> c_7()
      Weak TRS Rules:
        append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
        append(Nil(),ys) -> ys
        reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
        reverse(Nil()) -> Nil()
      Signature:
        {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
      Obligation:
        Innermost
        basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
    Applied Processor:
      RemoveWeakSuffixes
    Proof:
      Consider the dependency graph
        1:S:append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
           -->_1 append#(Nil(),ys) -> c_2():5
           -->_1 append#(Cons(x,xs),ys) -> c_1(append#(xs,ys)):1
        
        2:S:goal#(xs) -> c_3(shuffle#(xs))
           -->_1 shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs)):4
           -->_1 shuffle#(Nil()) -> c_7():7
        
        3:S:reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
           -->_2 reverse#(Nil()) -> c_5():6
           -->_1 append#(Nil(),ys) -> c_2():5
           -->_2 reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs)):3
           -->_1 append#(Cons(x,xs),ys) -> c_1(append#(xs,ys)):1
        
        4:S:shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
           -->_1 shuffle#(Nil()) -> c_7():7
           -->_2 reverse#(Nil()) -> c_5():6
           -->_1 shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs)):4
           -->_2 reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs)):3
        
        5:W:append#(Nil(),ys) -> c_2()
           
        
        6:W:reverse#(Nil()) -> c_5()
           
        
        7:W:shuffle#(Nil()) -> c_7()
           
        
      The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
        6: reverse#(Nil()) -> c_5()  
        7: shuffle#(Nil()) -> c_7()  
        5: append#(Nil(),ys) -> c_2()
*** 1.1.1.1.1 Progress [(?,O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
        goal#(xs) -> c_3(shuffle#(xs))
        reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
        shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
        append(Nil(),ys) -> ys
        reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
        reverse(Nil()) -> Nil()
      Signature:
        {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
      Obligation:
        Innermost
        basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
    Applied Processor:
      RemoveHeads
    Proof:
      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:goal#(xs) -> c_3(shuffle#(xs))
         -->_1 shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs)):4
      
      3:S:reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
         -->_2 reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs)):3
         -->_1 append#(Cons(x,xs),ys) -> c_1(append#(xs,ys)):1
      
      4:S:shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
         -->_1 shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs)):4
         -->_2 reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs)):3
      
      
      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).
      
      [(2,goal#(xs) -> c_3(shuffle#(xs)))]
*** 1.1.1.1.1.1 Progress [(?,O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
        reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
        shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
        append(Nil(),ys) -> ys
        reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
        reverse(Nil()) -> Nil()
      Signature:
        {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
      Obligation:
        Innermost
        basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
    Applied Processor:
      Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
    Proof:
      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 DP Rules:
          append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
        Strict TRS Rules:
          
        Weak DP Rules:
          reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
          shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
        Weak TRS Rules:
          append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
          append(Nil(),ys) -> ys
          reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
          reverse(Nil()) -> Nil()
        Signature:
          {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
        Obligation:
          Innermost
          basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
      
      Problem (S)
        Strict DP Rules:
          reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
          shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
        Strict TRS Rules:
          
        Weak DP Rules:
          append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
        Weak TRS Rules:
          append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
          append(Nil(),ys) -> ys
          reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
          reverse(Nil()) -> Nil()
        Signature:
          {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
        Obligation:
          Innermost
          basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
  *** 1.1.1.1.1.1.1 Progress [(?,O(n^3))]  ***
      Considered Problem:
        Strict DP Rules:
          append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
        Strict TRS Rules:
          
        Weak DP Rules:
          reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
          shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
        Weak TRS Rules:
          append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
          append(Nil(),ys) -> ys
          reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
          reverse(Nil()) -> Nil()
        Signature:
          {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
        Obligation:
          Innermost
          basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
      Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing}
      Proof:
        We decompose the input problem according to the dependency graph into the upper component
          shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
        and a lower component
          append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
          reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
        Further, following extension rules are added to the lower component.
          shuffle#(Cons(x,xs)) -> reverse#(xs)
          shuffle#(Cons(x,xs)) -> shuffle#(reverse(xs))
    *** 1.1.1.1.1.1.1.1 Progress [(?,O(n^1))]  ***
        Considered Problem:
          Strict DP Rules:
            shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
          Strict TRS Rules:
            
          Weak DP Rules:
            
          Weak TRS Rules:
            append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
            append(Nil(),ys) -> ys
            reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
            reverse(Nil()) -> Nil()
          Signature:
            {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
          Obligation:
            Innermost
            basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
        Applied Processor:
          PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
        Proof:
          We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
            1: shuffle#(Cons(x,xs)) ->    
                 c_6(shuffle#(reverse(xs))
                    ,reverse#(xs))        
            
          The strictly oriented rules are moved into the weak component.
      *** 1.1.1.1.1.1.1.1.1 Progress [(?,O(n^1))]  ***
          Considered Problem:
            Strict DP Rules:
              shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
            Strict TRS Rules:
              
            Weak DP Rules:
              
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
          Proof:
            We apply a matrix interpretation of kind constructor based matrix interpretation:
            The following argument positions are considered usable:
              uargs(c_6) = {1}
            
            Following symbols are considered usable:
              {append,reverse,append#,goal#,reverse#,shuffle#}
            TcT has computed the following interpretation:
                  p(Cons) = [1] x2 + [1]         
                   p(Nil) = [0]                  
                p(append) = [1] x1 + [1] x2 + [0]
                  p(goal) = [1] x1 + [4]         
               p(reverse) = [1] x1 + [0]         
               p(shuffle) = [1] x1 + [1]         
               p(append#) = [1] x1 + [8] x2 + [1]
                 p(goal#) = [4] x1 + [0]         
              p(reverse#) = [2] x1 + [0]         
              p(shuffle#) = [2] x1 + [6]         
                   p(c_1) = [1] x1 + [1]         
                   p(c_2) = [0]                  
                   p(c_3) = [0]                  
                   p(c_4) = [4] x1 + [1] x2 + [1]
                   p(c_5) = [0]                  
                   p(c_6) = [1] x1 + [1]         
                   p(c_7) = [1]                  
            
            Following rules are strictly oriented:
            shuffle#(Cons(x,xs)) = [2] xs + [8]             
                                 > [2] xs + [7]             
                                 = c_6(shuffle#(reverse(xs))
                                      ,reverse#(xs))        
            
            
            Following rules are (at-least) weakly oriented:
            append(Cons(x,xs),ys) =  [1] xs + [1] ys + [1]
                                  >= [1] xs + [1] ys + [1]
                                  =  Cons(x,append(xs,ys))
            
                 append(Nil(),ys) =  [1] ys + [0]         
                                  >= [1] ys + [0]         
                                  =  ys                   
            
              reverse(Cons(x,xs)) =  [1] xs + [1]         
                                  >= [1] xs + [1]         
                                  =  append(reverse(xs)   
                                           ,Cons(x,Nil()))
            
                   reverse(Nil()) =  [0]                  
                                  >= [0]                  
                                  =  Nil()                
            
      *** 1.1.1.1.1.1.1.1.1.1 Progress [(?,O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            Assumption
          Proof:
            ()
      
      *** 1.1.1.1.1.1.1.1.2 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            RemoveWeakSuffixes
          Proof:
            Consider the dependency graph
              1:W:shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
                 -->_1 shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs)):1
              
            The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
              1: shuffle#(Cons(x,xs)) ->    
                   c_6(shuffle#(reverse(xs))
                      ,reverse#(xs))        
      *** 1.1.1.1.1.1.1.1.2.1 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            EmptyProcessor
          Proof:
            The problem is already closed. The intended complexity is O(1).
      
    *** 1.1.1.1.1.1.1.2 Progress [(?,O(n^2))]  ***
        Considered Problem:
          Strict DP Rules:
            append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
          Strict TRS Rules:
            
          Weak DP Rules:
            reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
            shuffle#(Cons(x,xs)) -> reverse#(xs)
            shuffle#(Cons(x,xs)) -> shuffle#(reverse(xs))
          Weak TRS Rules:
            append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
            append(Nil(),ys) -> ys
            reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
            reverse(Nil()) -> Nil()
          Signature:
            {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
          Obligation:
            Innermost
            basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
        Applied Processor:
          PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
        Proof:
          We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
            1: append#(Cons(x,xs),ys) ->
                 c_1(append#(xs,ys))    
            
          The strictly oriented rules are moved into the weak component.
      *** 1.1.1.1.1.1.1.2.1 Progress [(?,O(n^2))]  ***
          Considered Problem:
            Strict DP Rules:
              append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
            Strict TRS Rules:
              
            Weak DP Rules:
              reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
              shuffle#(Cons(x,xs)) -> reverse#(xs)
              shuffle#(Cons(x,xs)) -> shuffle#(reverse(xs))
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
          Proof:
            We apply a polynomial interpretation of kind constructor-based(mixed(2)):
            The following argument positions are considered usable:
              uargs(c_1) = {1},
              uargs(c_4) = {1,2}
            
            Following symbols are considered usable:
              {append,reverse,append#,goal#,reverse#,shuffle#}
            TcT has computed the following interpretation:
                  p(Cons) = 1 + x1 + x2      
                   p(Nil) = 0                
                p(append) = x1 + x2          
                  p(goal) = 1 + 2*x1^2       
               p(reverse) = 1 + x1           
               p(shuffle) = 4*x1 + x1^2      
               p(append#) = 4*x1             
                 p(goal#) = 2 + x1^2         
              p(reverse#) = 1 + 6*x1 + 2*x1^2
              p(shuffle#) = 3*x1^2           
                   p(c_1) = 1 + x1           
                   p(c_2) = 0                
                   p(c_3) = x1               
                   p(c_4) = 1 + x1 + x2      
                   p(c_5) = 1                
                   p(c_6) = 1                
                   p(c_7) = 1                
            
            Following rules are strictly oriented:
            append#(Cons(x,xs),ys) = 4 + 4*x + 4*xs     
                                   > 1 + 4*xs           
                                   = c_1(append#(xs,ys))
            
            
            Following rules are (at-least) weakly oriented:
             reverse#(Cons(x,xs)) =  9 + 10*x + 4*x*xs + 2*x^2 + 10*xs + 2*xs^2
                                  >= 6 + 10*xs + 2*xs^2                        
                                  =  c_4(append#(reverse(xs)                   
                                                ,Cons(x,Nil()))                
                                        ,reverse#(xs))                         
            
             shuffle#(Cons(x,xs)) =  3 + 6*x + 6*x*xs + 3*x^2 + 6*xs + 3*xs^2  
                                  >= 1 + 6*xs + 2*xs^2                         
                                  =  reverse#(xs)                              
            
             shuffle#(Cons(x,xs)) =  3 + 6*x + 6*x*xs + 3*x^2 + 6*xs + 3*xs^2  
                                  >= 3 + 6*xs + 3*xs^2                         
                                  =  shuffle#(reverse(xs))                     
            
            append(Cons(x,xs),ys) =  1 + x + xs + ys                           
                                  >= 1 + x + xs + ys                           
                                  =  Cons(x,append(xs,ys))                     
            
                 append(Nil(),ys) =  ys                                        
                                  >= ys                                        
                                  =  ys                                        
            
              reverse(Cons(x,xs)) =  2 + x + xs                                
                                  >= 2 + x + xs                                
                                  =  append(reverse(xs)                        
                                           ,Cons(x,Nil()))                     
            
                   reverse(Nil()) =  1                                         
                                  >= 0                                         
                                  =  Nil()                                     
            
      *** 1.1.1.1.1.1.1.2.1.1 Progress [(?,O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
              reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
              shuffle#(Cons(x,xs)) -> reverse#(xs)
              shuffle#(Cons(x,xs)) -> shuffle#(reverse(xs))
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            Assumption
          Proof:
            ()
      
      *** 1.1.1.1.1.1.1.2.2 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
              reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
              shuffle#(Cons(x,xs)) -> reverse#(xs)
              shuffle#(Cons(x,xs)) -> shuffle#(reverse(xs))
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            RemoveWeakSuffixes
          Proof:
            Consider the dependency graph
              1:W:append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
                 -->_1 append#(Cons(x,xs),ys) -> c_1(append#(xs,ys)):1
              
              2:W:reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
                 -->_2 reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs)):2
                 -->_1 append#(Cons(x,xs),ys) -> c_1(append#(xs,ys)):1
              
              3:W:shuffle#(Cons(x,xs)) -> reverse#(xs)
                 -->_1 reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs)):2
              
              4:W:shuffle#(Cons(x,xs)) -> shuffle#(reverse(xs))
                 -->_1 shuffle#(Cons(x,xs)) -> shuffle#(reverse(xs)):4
                 -->_1 shuffle#(Cons(x,xs)) -> reverse#(xs):3
              
            The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
              4: shuffle#(Cons(x,xs)) ->     
                   shuffle#(reverse(xs))     
              3: shuffle#(Cons(x,xs)) ->     
                   reverse#(xs)              
              2: reverse#(Cons(x,xs)) ->     
                   c_4(append#(reverse(xs)   
                              ,Cons(x,Nil()))
                      ,reverse#(xs))         
              1: append#(Cons(x,xs),ys) ->   
                   c_1(append#(xs,ys))       
      *** 1.1.1.1.1.1.1.2.2.1 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            EmptyProcessor
          Proof:
            The problem is already closed. The intended complexity is O(1).
      
  *** 1.1.1.1.1.1.2 Progress [(?,O(n^2))]  ***
      Considered Problem:
        Strict DP Rules:
          reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
          shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
        Strict TRS Rules:
          
        Weak DP Rules:
          append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
        Weak TRS Rules:
          append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
          append(Nil(),ys) -> ys
          reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
          reverse(Nil()) -> Nil()
        Signature:
          {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
        Obligation:
          Innermost
          basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
      Applied Processor:
        RemoveWeakSuffixes
      Proof:
        Consider the dependency graph
          1:S:reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
             -->_1 append#(Cons(x,xs),ys) -> c_1(append#(xs,ys)):3
             -->_2 reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs)):1
          
          2:S:shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
             -->_1 shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs)):2
             -->_2 reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs)):1
          
          3:W:append#(Cons(x,xs),ys) -> c_1(append#(xs,ys))
             -->_1 append#(Cons(x,xs),ys) -> c_1(append#(xs,ys)):3
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          3: append#(Cons(x,xs),ys) ->
               c_1(append#(xs,ys))    
  *** 1.1.1.1.1.1.2.1 Progress [(?,O(n^2))]  ***
      Considered Problem:
        Strict DP Rules:
          reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
          shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
        Strict TRS Rules:
          
        Weak DP Rules:
          
        Weak TRS Rules:
          append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
          append(Nil(),ys) -> ys
          reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
          reverse(Nil()) -> Nil()
        Signature:
          {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0}
        Obligation:
          Innermost
          basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
      Applied Processor:
        SimplifyRHS
      Proof:
        Consider the dependency graph
          1:S:reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs))
             -->_2 reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs)):1
          
          2:S:shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
             -->_1 shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs)):2
             -->_2 reverse#(Cons(x,xs)) -> c_4(append#(reverse(xs),Cons(x,Nil())),reverse#(xs)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          reverse#(Cons(x,xs)) -> c_4(reverse#(xs))
  *** 1.1.1.1.1.1.2.1.1 Progress [(?,O(n^2))]  ***
      Considered Problem:
        Strict DP Rules:
          reverse#(Cons(x,xs)) -> c_4(reverse#(xs))
          shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
        Strict TRS Rules:
          
        Weak DP Rules:
          
        Weak TRS Rules:
          append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
          append(Nil(),ys) -> ys
          reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
          reverse(Nil()) -> Nil()
        Signature:
          {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0}
        Obligation:
          Innermost
          basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
      Applied Processor:
        Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
      Proof:
        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 DP Rules:
            reverse#(Cons(x,xs)) -> c_4(reverse#(xs))
          Strict TRS Rules:
            
          Weak DP Rules:
            shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
          Weak TRS Rules:
            append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
            append(Nil(),ys) -> ys
            reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
            reverse(Nil()) -> Nil()
          Signature:
            {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0}
          Obligation:
            Innermost
            basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
        
        Problem (S)
          Strict DP Rules:
            shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
          Strict TRS Rules:
            
          Weak DP Rules:
            reverse#(Cons(x,xs)) -> c_4(reverse#(xs))
          Weak TRS Rules:
            append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
            append(Nil(),ys) -> ys
            reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
            reverse(Nil()) -> Nil()
          Signature:
            {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0}
          Obligation:
            Innermost
            basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
    *** 1.1.1.1.1.1.2.1.1.1 Progress [(?,O(n^2))]  ***
        Considered Problem:
          Strict DP Rules:
            reverse#(Cons(x,xs)) -> c_4(reverse#(xs))
          Strict TRS Rules:
            
          Weak DP Rules:
            shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
          Weak TRS Rules:
            append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
            append(Nil(),ys) -> ys
            reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
            reverse(Nil()) -> Nil()
          Signature:
            {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0}
          Obligation:
            Innermost
            basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
        Applied Processor:
          PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
        Proof:
          We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
            1: reverse#(Cons(x,xs)) ->
                 c_4(reverse#(xs))    
            
          The strictly oriented rules are moved into the weak component.
      *** 1.1.1.1.1.1.2.1.1.1.1 Progress [(?,O(n^2))]  ***
          Considered Problem:
            Strict DP Rules:
              reverse#(Cons(x,xs)) -> c_4(reverse#(xs))
            Strict TRS Rules:
              
            Weak DP Rules:
              shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
          Proof:
            We apply a polynomial interpretation of kind constructor-based(mixed(2)):
            The following argument positions are considered usable:
              uargs(c_4) = {1},
              uargs(c_6) = {1,2}
            
            Following symbols are considered usable:
              {append,reverse,append#,goal#,reverse#,shuffle#}
            TcT has computed the following interpretation:
                  p(Cons) = 1 + x2                        
                   p(Nil) = 0                             
                p(append) = x1 + x2                       
                  p(goal) = x1                            
               p(reverse) = x1                            
               p(shuffle) = 1 + x1                        
               p(append#) = 4 + x1*x2 + x1^2 + x2 + 2*x2^2
                 p(goal#) = 1 + 4*x1                      
              p(reverse#) = 1 + x1                        
              p(shuffle#) = 2 + 2*x1^2                    
                   p(c_1) = 0                             
                   p(c_2) = 0                             
                   p(c_3) = 1                             
                   p(c_4) = x1                            
                   p(c_5) = 0                             
                   p(c_6) = 1 + x1 + x2                   
                   p(c_7) = 0                             
            
            Following rules are strictly oriented:
            reverse#(Cons(x,xs)) = 2 + xs           
                                 > 1 + xs           
                                 = c_4(reverse#(xs))
            
            
            Following rules are (at-least) weakly oriented:
             shuffle#(Cons(x,xs)) =  4 + 4*xs + 2*xs^2        
                                  >= 4 + xs + 2*xs^2          
                                  =  c_6(shuffle#(reverse(xs))
                                        ,reverse#(xs))        
            
            append(Cons(x,xs),ys) =  1 + xs + ys              
                                  >= 1 + xs + ys              
                                  =  Cons(x,append(xs,ys))    
            
                 append(Nil(),ys) =  ys                       
                                  >= ys                       
                                  =  ys                       
            
              reverse(Cons(x,xs)) =  1 + xs                   
                                  >= 1 + xs                   
                                  =  append(reverse(xs)       
                                           ,Cons(x,Nil()))    
            
                   reverse(Nil()) =  0                        
                                  >= 0                        
                                  =  Nil()                    
            
      *** 1.1.1.1.1.1.2.1.1.1.1.1 Progress [(?,O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              reverse#(Cons(x,xs)) -> c_4(reverse#(xs))
              shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            Assumption
          Proof:
            ()
      
      *** 1.1.1.1.1.1.2.1.1.1.2 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              reverse#(Cons(x,xs)) -> c_4(reverse#(xs))
              shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            RemoveWeakSuffixes
          Proof:
            Consider the dependency graph
              1:W:reverse#(Cons(x,xs)) -> c_4(reverse#(xs))
                 -->_1 reverse#(Cons(x,xs)) -> c_4(reverse#(xs)):1
              
              2:W:shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
                 -->_1 shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs)):2
                 -->_2 reverse#(Cons(x,xs)) -> c_4(reverse#(xs)):1
              
            The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
              2: shuffle#(Cons(x,xs)) ->    
                   c_6(shuffle#(reverse(xs))
                      ,reverse#(xs))        
              1: reverse#(Cons(x,xs)) ->    
                   c_4(reverse#(xs))        
      *** 1.1.1.1.1.1.2.1.1.1.2.1 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            EmptyProcessor
          Proof:
            The problem is already closed. The intended complexity is O(1).
      
    *** 1.1.1.1.1.1.2.1.1.2 Progress [(?,O(n^1))]  ***
        Considered Problem:
          Strict DP Rules:
            shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
          Strict TRS Rules:
            
          Weak DP Rules:
            reverse#(Cons(x,xs)) -> c_4(reverse#(xs))
          Weak TRS Rules:
            append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
            append(Nil(),ys) -> ys
            reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
            reverse(Nil()) -> Nil()
          Signature:
            {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0}
          Obligation:
            Innermost
            basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
        Applied Processor:
          RemoveWeakSuffixes
        Proof:
          Consider the dependency graph
            1:S:shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
               -->_2 reverse#(Cons(x,xs)) -> c_4(reverse#(xs)):2
               -->_1 shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs)):1
            
            2:W:reverse#(Cons(x,xs)) -> c_4(reverse#(xs))
               -->_1 reverse#(Cons(x,xs)) -> c_4(reverse#(xs)):2
            
          The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
            2: reverse#(Cons(x,xs)) ->
                 c_4(reverse#(xs))    
    *** 1.1.1.1.1.1.2.1.1.2.1 Progress [(?,O(n^1))]  ***
        Considered Problem:
          Strict DP Rules:
            shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
          Strict TRS Rules:
            
          Weak DP Rules:
            
          Weak TRS Rules:
            append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
            append(Nil(),ys) -> ys
            reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
            reverse(Nil()) -> Nil()
          Signature:
            {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {Cons/2,Nil/0,c_1/1,c_2/0,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0}
          Obligation:
            Innermost
            basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
        Applied Processor:
          SimplifyRHS
        Proof:
          Consider the dependency graph
            1:S:shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs))
               -->_1 shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)),reverse#(xs)):1
            
          Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
            shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)))
    *** 1.1.1.1.1.1.2.1.1.2.1.1 Progress [(?,O(n^1))]  ***
        Considered Problem:
          Strict DP Rules:
            shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)))
          Strict TRS Rules:
            
          Weak DP Rules:
            
          Weak TRS Rules:
            append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
            append(Nil(),ys) -> ys
            reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
            reverse(Nil()) -> Nil()
          Signature:
            {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {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}
          Obligation:
            Innermost
            basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
        Applied Processor:
          PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
        Proof:
          We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
            1: shuffle#(Cons(x,xs)) ->     
                 c_6(shuffle#(reverse(xs)))
            
          The strictly oriented rules are moved into the weak component.
      *** 1.1.1.1.1.1.2.1.1.2.1.1.1 Progress [(?,O(n^1))]  ***
          Considered Problem:
            Strict DP Rules:
              shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)))
            Strict TRS Rules:
              
            Weak DP Rules:
              
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {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}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
          Proof:
            We apply a matrix interpretation of kind constructor based matrix interpretation:
            The following argument positions are considered usable:
              uargs(c_6) = {1}
            
            Following symbols are considered usable:
              {append,reverse,append#,goal#,reverse#,shuffle#}
            TcT has computed the following interpretation:
                  p(Cons) = [1] x2 + [1]         
                   p(Nil) = [0]                  
                p(append) = [1] x1 + [1] x2 + [0]
                  p(goal) = [1]                  
               p(reverse) = [1] x1 + [0]         
               p(shuffle) = [1] x1 + [1]         
               p(append#) = [1] x1 + [2] x2 + [0]
                 p(goal#) = [1] x1 + [1]         
              p(reverse#) = [0]                  
              p(shuffle#) = [10] x1 + [1]        
                   p(c_1) = [0]                  
                   p(c_2) = [1]                  
                   p(c_3) = [4] x1 + [1]         
                   p(c_4) = [1] x1 + [2]         
                   p(c_5) = [0]                  
                   p(c_6) = [1] x1 + [0]         
                   p(c_7) = [0]                  
            
            Following rules are strictly oriented:
            shuffle#(Cons(x,xs)) = [10] xs + [11]            
                                 > [10] xs + [1]             
                                 = c_6(shuffle#(reverse(xs)))
            
            
            Following rules are (at-least) weakly oriented:
            append(Cons(x,xs),ys) =  [1] xs + [1] ys + [1]
                                  >= [1] xs + [1] ys + [1]
                                  =  Cons(x,append(xs,ys))
            
                 append(Nil(),ys) =  [1] ys + [0]         
                                  >= [1] ys + [0]         
                                  =  ys                   
            
              reverse(Cons(x,xs)) =  [1] xs + [1]         
                                  >= [1] xs + [1]         
                                  =  append(reverse(xs)   
                                           ,Cons(x,Nil()))
            
                   reverse(Nil()) =  [0]                  
                                  >= [0]                  
                                  =  Nil()                
            
      *** 1.1.1.1.1.1.2.1.1.2.1.1.1.1 Progress [(?,O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)))
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {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}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            Assumption
          Proof:
            ()
      
      *** 1.1.1.1.1.1.2.1.1.2.1.1.2 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)))
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {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}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            RemoveWeakSuffixes
          Proof:
            Consider the dependency graph
              1:W:shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs)))
                 -->_1 shuffle#(Cons(x,xs)) -> c_6(shuffle#(reverse(xs))):1
              
            The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
              1: shuffle#(Cons(x,xs)) ->     
                   c_6(shuffle#(reverse(xs)))
      *** 1.1.1.1.1.1.2.1.1.2.1.1.2.1 Progress [(O(1),O(1))]  ***
          Considered Problem:
            Strict DP Rules:
              
            Strict TRS Rules:
              
            Weak DP Rules:
              
            Weak TRS Rules:
              append(Cons(x,xs),ys) -> Cons(x,append(xs,ys))
              append(Nil(),ys) -> ys
              reverse(Cons(x,xs)) -> append(reverse(xs),Cons(x,Nil()))
              reverse(Nil()) -> Nil()
            Signature:
              {append/2,goal/1,reverse/1,shuffle/1,append#/2,goal#/1,reverse#/1,shuffle#/1} / {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}
            Obligation:
              Innermost
              basic terms: {append#,goal#,reverse#,shuffle#}/{Cons,Nil}
          Applied Processor:
            EmptyProcessor
          Proof:
            The problem is already closed. The intended complexity is O(1).