MAYBE

Problem:
 app(nil(),y) -> y
 app(add(n,x),y) -> add(n,app(x,y))
 reverse(nil()) -> nil()
 reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
 shuffle(nil()) -> nil()
 shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))

Proof:
 Complexity Transformation Processor:
  strict:
   app(nil(),y) -> y
   app(add(n,x),y) -> add(n,app(x,y))
   reverse(nil()) -> nil()
   reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
   shuffle(nil()) -> nil()
   shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [shuffle](x0) = x0,
     
     [reverse](x0) = x0 + 1,
     
     [add](x0, x1) = x0 + x1,
     
     [app](x0, x1) = x0 + x1,
     
     [nil] = 0
    orientation:
     app(nil(),y) = y >= y = y
     
     app(add(n,x),y) = n + x + y >= n + x + y = add(n,app(x,y))
     
     reverse(nil()) = 1 >= 0 = nil()
     
     reverse(add(n,x)) = n + x + 1 >= n + x + 1 = app(reverse(x),add(n,nil()))
     
     shuffle(nil()) = 0 >= 0 = nil()
     
     shuffle(add(n,x)) = n + x >= n + x + 1 = add(n,shuffle(reverse(x)))
    problem:
     strict:
      app(nil(),y) -> y
      app(add(n,x),y) -> add(n,app(x,y))
      reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
      shuffle(nil()) -> nil()
      shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
     weak:
      reverse(nil()) -> nil()
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [shuffle](x0) = x0,
       
       [reverse](x0) = x0,
       
       [add](x0, x1) = x0 + x1 + 1,
       
       [app](x0, x1) = x0 + x1 + 1,
       
       [nil] = 1
      orientation:
       app(nil(),y) = y + 2 >= y = y
       
       app(add(n,x),y) = n + x + y + 2 >= n + x + y + 2 = add(n,app(x,y))
       
       reverse(add(n,x)) = n + x + 1 >= n + x + 3 = app(reverse(x),add(n,nil()))
       
       shuffle(nil()) = 1 >= 1 = nil()
       
       shuffle(add(n,x)) = n + x + 1 >= n + x + 1 = add(n,shuffle(reverse(x)))
       
       reverse(nil()) = 1 >= 1 = nil()
      problem:
       strict:
        app(add(n,x),y) -> add(n,app(x,y))
        reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
        shuffle(nil()) -> nil()
        shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       weak:
        app(nil(),y) -> y
        reverse(nil()) -> nil()
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [shuffle](x0) = x0 + 1,
         
         [reverse](x0) = x0,
         
         [add](x0, x1) = x0 + x1,
         
         [app](x0, x1) = x0 + x1,
         
         [nil] = 0
        orientation:
         app(add(n,x),y) = n + x + y >= n + x + y = add(n,app(x,y))
         
         reverse(add(n,x)) = n + x >= n + x = app(reverse(x),add(n,nil()))
         
         shuffle(nil()) = 1 >= 0 = nil()
         
         shuffle(add(n,x)) = n + x + 1 >= n + x + 1 = add(n,shuffle(reverse(x)))
         
         app(nil(),y) = y >= y = y
         
         reverse(nil()) = 0 >= 0 = nil()
        problem:
         strict:
          app(add(n,x),y) -> add(n,app(x,y))
          reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
          shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
         weak:
          shuffle(nil()) -> nil()
          app(nil(),y) -> y
          reverse(nil()) -> nil()
        Matrix Interpretation Processor:
         dimension: 2
         max_matrix:
          [1 1]
          [0 1]
          interpretation:
                           [1 1]  
           [shuffle](x0) = [0 1]x0,
           
                             
           [reverse](x0) = x0,
           
                           [1 1]          [0]
           [add](x0, x1) = [0 0]x0 + x1 + [1],
           
                                  
           [app](x0, x1) = x0 + x1,
           
                   [0]
           [nil] = [0]
          orientation:
                             [1 1]            [0]    [1 1]            [0]                  
           app(add(n,x),y) = [0 0]n + x + y + [1] >= [0 0]n + x + y + [1] = add(n,app(x,y))
           
                               [1 1]        [0]    [1 1]        [0]                               
           reverse(add(n,x)) = [0 0]n + x + [1] >= [0 0]n + x + [1] = app(reverse(x),add(n,nil()))
           
                               [1 1]    [1 1]    [1]    [1 1]    [1 1]    [0]                             
           shuffle(add(n,x)) = [0 0]n + [0 1]x + [1] >= [0 0]n + [0 1]x + [1] = add(n,shuffle(reverse(x)))
           
                            [0]    [0]        
           shuffle(nil()) = [0] >= [0] = nil()
           
                                    
           app(nil(),y) = y >= y = y
           
                            [0]    [0]        
           reverse(nil()) = [0] >= [0] = nil()
          problem:
           strict:
            app(add(n,x),y) -> add(n,app(x,y))
            reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
           weak:
            shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
            shuffle(nil()) -> nil()
            app(nil(),y) -> y
            reverse(nil()) -> nil()
          Open