MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict 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)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..