MAYBE
Time: 0.004919
TRS:
 {                 concat(leaf(), Y) -> Y,
               concat(cons(U, V), Y) -> cons(U, concat(V, Y)),
               lessleaves(X, leaf()) -> false(),
      lessleaves(leaf(), cons(W, Z)) -> true(),
  lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))}
 DP:
  DP:
   {             concat#(cons(U, V), Y) -> concat#(V, Y),
    lessleaves#(cons(U, V), cons(W, Z)) -> concat#(U, V),
    lessleaves#(cons(U, V), cons(W, Z)) -> concat#(W, Z),
    lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z))}
  TRS:
  {                 concat(leaf(), Y) -> Y,
                concat(cons(U, V), Y) -> cons(U, concat(V, Y)),
                lessleaves(X, leaf()) -> false(),
       lessleaves(leaf(), cons(W, Z)) -> true(),
   lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))}
  EDG:
   {(lessleaves#(cons(U, V), cons(W, Z)) -> concat#(U, V), concat#(cons(U, V), Y) -> concat#(V, Y))
    (concat#(cons(U, V), Y) -> concat#(V, Y), concat#(cons(U, V), Y) -> concat#(V, Y))
    (lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z)), lessleaves#(cons(U, V), cons(W, Z)) -> concat#(U, V))
    (lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z)), lessleaves#(cons(U, V), cons(W, Z)) -> concat#(W, Z))
    (lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z)), lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z)))
    (lessleaves#(cons(U, V), cons(W, Z)) -> concat#(W, Z), concat#(cons(U, V), Y) -> concat#(V, Y))}
   STATUS:
    arrows: 0.625000
    SCCS (2):
     Scc:
      {lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z))}
     Scc:
      {concat#(cons(U, V), Y) -> concat#(V, Y)}
     
     SCC (1):
      Strict:
       {lessleaves#(cons(U, V), cons(W, Z)) -> lessleaves#(concat(U, V), concat(W, Z))}
      Weak:
      {                 concat(leaf(), Y) -> Y,
                    concat(cons(U, V), Y) -> cons(U, concat(V, Y)),
                    lessleaves(X, leaf()) -> false(),
           lessleaves(leaf(), cons(W, Z)) -> true(),
       lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))}
      Open
     
     
     SCC (1):
      Strict:
       {concat#(cons(U, V), Y) -> concat#(V, Y)}
      Weak:
      {                 concat(leaf(), Y) -> Y,
                    concat(cons(U, V), Y) -> cons(U, concat(V, Y)),
                    lessleaves(X, leaf()) -> false(),
           lessleaves(leaf(), cons(W, Z)) -> true(),
       lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z))}
      Open