YES
Time: 0.006059
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)}
  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))}
   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:
       
     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)}
    SPSC:
     Simple Projection:
      pi(reverse#) = 0
     Strict:
      {}
     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)}
    SPSC:
     Simple Projection:
      pi(app#) = 0
     Strict:
      {}
     Qed