YES
Time: 0.031649
TRS:
 {    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)}
 DP:
  DP:
   {app#(add(n, x), y) -> app#(x, y),
    reverse# add(n, x) -> app#(reverse x, add(n, nil())),
    reverse# add(n, x) -> reverse# x,
    shuffle# add(n, x) -> reverse# x,
    shuffle# add(n, x) -> shuffle# reverse x}
  TRS:
  {    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)}
  UR:
   {    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()))}
   EDG:
    {(reverse# add(n, x) -> reverse# x, reverse# add(n, x) -> reverse# x)
     (reverse# add(n, x) -> reverse# x, reverse# add(n, x) -> app#(reverse x, add(n, nil())))
     (shuffle# add(n, x) -> shuffle# reverse x, shuffle# add(n, x) -> shuffle# reverse x)
     (shuffle# add(n, x) -> shuffle# reverse x, shuffle# add(n, x) -> reverse# x)
     (reverse# add(n, x) -> app#(reverse x, add(n, nil())), app#(add(n, x), y) -> app#(x, y))
     (shuffle# add(n, x) -> reverse# x, reverse# add(n, x) -> app#(reverse x, add(n, nil())))
     (shuffle# add(n, x) -> reverse# x, reverse# add(n, x) -> reverse# x)
     (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y))}
    STATUS:
     arrows: 0.680000
     SCCS (3):
      Scc:
       {shuffle# add(n, x) -> shuffle# reverse x}
      Scc:
       {reverse# add(n, x) -> reverse# x}
      Scc:
       {app#(add(n, x), y) -> app#(x, y)}
      
      SCC (1):
       Strict:
        {shuffle# add(n, x) -> shuffle# reverse x}
       Weak:
       {    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)}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [app](x0, x1) = x0 + x1,
         
         [add](x0, x1) = x0 + 1,
         
         [reverse](x0) = x0,
         
         [shuffle](x0) = 0,
         
         [nil] = 0,
         
         [shuffle#](x0) = x0
        Strict:
         shuffle# add(n, x) -> shuffle# reverse x
         1 + 0n + 1x >= 0 + 1x
        Weak:
         shuffle add(n, x) -> add(n, shuffle reverse x)
         0 + 0n + 0x >= 1 + 0n + 0x
         shuffle nil() -> nil()
         0 >= 0
         reverse add(n, x) -> app(reverse x, add(n, nil()))
         1 + 0n + 1x >= 1 + 0n + 1x
         reverse nil() -> nil()
         0 >= 0
         app(add(n, x), y) -> add(n, app(x, y))
         1 + 1y + 0n + 1x >= 1 + 1y + 0n + 1x
         app(nil(), y) -> y
         0 + 1y >= 1y
       Qed
     
     SCC (1):
      Strict:
       {reverse# add(n, x) -> reverse# x}
      Weak:
      {    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)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [app](x0, x1) = x0 + 1,
        
        [add](x0, x1) = x0 + 1,
        
        [reverse](x0) = x0 + 1,
        
        [shuffle](x0) = x0 + 1,
        
        [nil] = 1,
        
        [reverse#](x0) = x0
       Strict:
        reverse# add(n, x) -> reverse# x
        1 + 0n + 1x >= 0 + 1x
       Weak:
        shuffle add(n, x) -> add(n, shuffle reverse x)
        2 + 0n + 1x >= 3 + 0n + 1x
        shuffle nil() -> nil()
        2 >= 1
        reverse add(n, x) -> app(reverse x, add(n, nil()))
        2 + 0n + 1x >= 2 + 0n + 1x
        reverse nil() -> nil()
        2 >= 1
        app(add(n, x), y) -> add(n, app(x, y))
        2 + 0y + 0n + 1x >= 2 + 0y + 0n + 1x
        app(nil(), y) -> y
        2 + 0y >= 1y
      Qed
     
     SCC (1):
      Strict:
       {app#(add(n, x), y) -> app#(x, y)}
      Weak:
      {    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)}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [app](x0, x1) = x0 + 1,
        
        [add](x0, x1) = x0 + 1,
        
        [reverse](x0) = x0 + 1,
        
        [shuffle](x0) = x0 + 1,
        
        [nil] = 1,
        
        [app#](x0, x1) = x0
       Strict:
        app#(add(n, x), y) -> app#(x, y)
        1 + 0y + 0n + 1x >= 0 + 0y + 1x
       Weak:
        shuffle add(n, x) -> add(n, shuffle reverse x)
        2 + 0n + 1x >= 3 + 0n + 1x
        shuffle nil() -> nil()
        2 >= 1
        reverse add(n, x) -> app(reverse x, add(n, nil()))
        2 + 0n + 1x >= 2 + 0n + 1x
        reverse nil() -> nil()
        2 >= 1
        app(add(n, x), y) -> add(n, app(x, y))
        2 + 0y + 0n + 1x >= 2 + 0y + 0n + 1x
        app(nil(), y) -> y
        2 + 0y >= 1y
      Qed