MAYBE
Time: 0.001053
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)}
       Open
      
      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)}
       Open
      
      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)}
       Open