MAYBE
Time: 0.008287
TRS:
 {                      minus(x, 0()) -> x,
                      minus(s x, s y) -> minus(x, y),
                       quot(0(), s y) -> 0(),
                       quot(s x, s y) -> s quot(minus(x, y), s y),
                        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),
                    concat(leaf(), y) -> y,
                concat(cons(u, v), y) -> cons(u, concat(v, y)),
               less_leaves(x, leaf()) -> false(),
      less_leaves(leaf(), cons(w, z)) -> true(),
  less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
 DP:
  DP:
   {                    minus#(s x, s y) -> minus#(x, y),
                         quot#(s x, s y) -> minus#(x, y),
                         quot#(s x, s y) -> quot#(minus(x, y), s y),
                      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,
                  concat#(cons(u, v), y) -> concat#(v, y),
    less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v),
    less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z),
    less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))}
  TRS:
  {                      minus(x, 0()) -> x,
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                         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),
                     concat(leaf(), y) -> y,
                 concat(cons(u, v), y) -> cons(u, concat(v, y)),
                less_leaves(x, leaf()) -> false(),
       less_leaves(leaf(), cons(w, z)) -> true(),
   less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
  UR:
   {        minus(x, 0()) -> x,
          minus(s x, s y) -> minus(x, y),
            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())),
        concat(leaf(), y) -> y,
    concat(cons(u, v), y) -> cons(u, concat(v, y)),
                  a(t, s) -> t,
                  a(t, s) -> s}
   EDG:
    {(less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z), concat#(cons(u, v), y) -> concat#(v, y))
     (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)))
     (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z))
     (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v))
     (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (concat#(cons(u, v), y) -> concat#(v, y), concat#(cons(u, v), y) -> concat#(v, y))
     (shuffle# add(n, x) -> reverse# x, reverse# add(n, x) -> reverse# x)
     (shuffle# 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))
     (reverse# add(n, x) -> reverse# x, reverse# add(n, x) -> app#(reverse x, add(n, nil())))
     (reverse# 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))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v), concat#(cons(u, v), y) -> concat#(v, y))
     (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
     (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))}
    EDG:
     {(less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z), concat#(cons(u, v), y) -> concat#(v, y))
      (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)))
      (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z))
      (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v))
      (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
      (concat#(cons(u, v), y) -> concat#(v, y), concat#(cons(u, v), y) -> concat#(v, y))
      (shuffle# add(n, x) -> reverse# x, reverse# add(n, x) -> reverse# x)
      (shuffle# 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))
      (reverse# add(n, x) -> reverse# x, reverse# add(n, x) -> app#(reverse x, add(n, nil())))
      (reverse# 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))
      (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
      (less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v), concat#(cons(u, v), y) -> concat#(v, y))
      (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
      (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))}
     EDG:
      {(less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z), concat#(cons(u, v), y) -> concat#(v, y))
       (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)))
       (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z))
       (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v))
       (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
       (concat#(cons(u, v), y) -> concat#(v, y), concat#(cons(u, v), y) -> concat#(v, y))
       (shuffle# add(n, x) -> reverse# x, reverse# add(n, x) -> reverse# x)
       (shuffle# 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))
       (reverse# add(n, x) -> reverse# x, reverse# add(n, x) -> app#(reverse x, add(n, nil())))
       (reverse# 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))
       (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
       (less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v), concat#(cons(u, v), y) -> concat#(v, y))
       (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
       (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))}
      EDG:
       {(less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z), concat#(cons(u, v), y) -> concat#(v, y))
        (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)))
        (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(w, z))
        (less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z)), less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v))
        (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
        (concat#(cons(u, v), y) -> concat#(v, y), concat#(cons(u, v), y) -> concat#(v, y))
        (shuffle# add(n, x) -> reverse# x, reverse# add(n, x) -> reverse# x)
        (shuffle# 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))
        (reverse# add(n, x) -> reverse# x, reverse# add(n, x) -> app#(reverse x, add(n, nil())))
        (reverse# 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))
        (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
        (less_leaves#(cons(u, v), cons(w, z)) -> concat#(u, v), concat#(cons(u, v), y) -> concat#(v, y))
        (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
        (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))}
       STATUS:
        arrows: 0.875000
        SCCS (7):
         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:
          {less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))}
         Scc:
          {concat#(cons(u, v), y) -> concat#(v, y)}
         Scc:
          {quot#(s x, s y) -> quot#(minus(x, y), s y)}
         Scc:
          {minus#(s x, s y) -> minus#(x, y)}
         
         SCC (1):
          Strict:
           {shuffle# add(n, x) -> shuffle# reverse x}
          Weak:
          {                      minus(x, 0()) -> x,
                               minus(s x, s y) -> minus(x, y),
                                quot(0(), s y) -> 0(),
                                quot(s x, s y) -> s quot(minus(x, y), s y),
                                 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),
                             concat(leaf(), y) -> y,
                         concat(cons(u, v), y) -> cons(u, concat(v, y)),
                        less_leaves(x, leaf()) -> false(),
               less_leaves(leaf(), cons(w, z)) -> true(),
           less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
          Open
         
         SCC (1):
          Strict:
           {reverse# add(n, x) -> reverse# x}
          Weak:
          {                      minus(x, 0()) -> x,
                               minus(s x, s y) -> minus(x, y),
                                quot(0(), s y) -> 0(),
                                quot(s x, s y) -> s quot(minus(x, y), s y),
                                 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),
                             concat(leaf(), y) -> y,
                         concat(cons(u, v), y) -> cons(u, concat(v, y)),
                        less_leaves(x, leaf()) -> false(),
               less_leaves(leaf(), cons(w, z)) -> true(),
           less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
          Open
         
         SCC (1):
          Strict:
           {app#(add(n, x), y) -> app#(x, y)}
          Weak:
          {                      minus(x, 0()) -> x,
                               minus(s x, s y) -> minus(x, y),
                                quot(0(), s y) -> 0(),
                                quot(s x, s y) -> s quot(minus(x, y), s y),
                                 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),
                             concat(leaf(), y) -> y,
                         concat(cons(u, v), y) -> cons(u, concat(v, y)),
                        less_leaves(x, leaf()) -> false(),
               less_leaves(leaf(), cons(w, z)) -> true(),
           less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
          Open
         SCC (1):
          Strict:
           {less_leaves#(cons(u, v), cons(w, z)) -> less_leaves#(concat(u, v), concat(w, z))}
          Weak:
          {                      minus(x, 0()) -> x,
                               minus(s x, s y) -> minus(x, y),
                                quot(0(), s y) -> 0(),
                                quot(s x, s y) -> s quot(minus(x, y), s y),
                                 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),
                             concat(leaf(), y) -> y,
                         concat(cons(u, v), y) -> cons(u, concat(v, y)),
                        less_leaves(x, leaf()) -> false(),
               less_leaves(leaf(), cons(w, z)) -> true(),
           less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
          Open
         
         
         SCC (1):
          Strict:
           {concat#(cons(u, v), y) -> concat#(v, y)}
          Weak:
          {                      minus(x, 0()) -> x,
                               minus(s x, s y) -> minus(x, y),
                                quot(0(), s y) -> 0(),
                                quot(s x, s y) -> s quot(minus(x, y), s y),
                                 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),
                             concat(leaf(), y) -> y,
                         concat(cons(u, v), y) -> cons(u, concat(v, y)),
                        less_leaves(x, leaf()) -> false(),
               less_leaves(leaf(), cons(w, z)) -> true(),
           less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
          Open
         SCC (1):
          Strict:
           {quot#(s x, s y) -> quot#(minus(x, y), s y)}
          Weak:
          {                      minus(x, 0()) -> x,
                               minus(s x, s y) -> minus(x, y),
                                quot(0(), s y) -> 0(),
                                quot(s x, s y) -> s quot(minus(x, y), s y),
                                 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),
                             concat(leaf(), y) -> y,
                         concat(cons(u, v), y) -> cons(u, concat(v, y)),
                        less_leaves(x, leaf()) -> false(),
               less_leaves(leaf(), cons(w, z)) -> true(),
           less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
          Open
         
         SCC (1):
          Strict:
           {minus#(s x, s y) -> minus#(x, y)}
          Weak:
          {                      minus(x, 0()) -> x,
                               minus(s x, s y) -> minus(x, y),
                                quot(0(), s y) -> 0(),
                                quot(s x, s y) -> s quot(minus(x, y), s y),
                                 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),
                             concat(leaf(), y) -> y,
                         concat(cons(u, v), y) -> cons(u, concat(v, y)),
                        less_leaves(x, leaf()) -> false(),
               less_leaves(leaf(), cons(w, z)) -> true(),
           less_leaves(cons(u, v), cons(w, z)) -> less_leaves(concat(u, v), concat(w, z))}
          Open