MAYBE
Time: 0.004081
TRS:
 {        isLeaf leaf() -> true(),
      isLeaf cons(u, v) -> false(),
        left cons(u, v) -> u,
       right cons(u, v) -> v,
      concat(leaf(), y) -> y,
  concat(cons(u, v), y) -> cons(u, concat(v, y)),
   if1(b, true(), u, v) -> false(),
  if1(b, false(), u, v) -> if2(b, u, v),
      less_leaves(u, v) -> if1(isLeaf u, isLeaf v, u, v),
      if2(true(), u, v) -> true(),
     if2(false(), u, v) -> less_leaves(concat(left u, right u), concat(left v, right v))}
 DP:
  DP:
   {concat#(cons(u, v), y) -> concat#(v, y),
    if1#(b, false(), u, v) -> if2#(b, u, v),
        less_leaves#(u, v) -> isLeaf# u,
        less_leaves#(u, v) -> isLeaf# v,
        less_leaves#(u, v) -> if1#(isLeaf u, isLeaf v, u, v),
       if2#(false(), u, v) -> left# u,
       if2#(false(), u, v) -> left# v,
       if2#(false(), u, v) -> right# u,
       if2#(false(), u, v) -> right# v,
       if2#(false(), u, v) -> concat#(left u, right u),
       if2#(false(), u, v) -> concat#(left v, right v),
       if2#(false(), u, v) -> less_leaves#(concat(left u, right u), concat(left v, right v))}
  TRS:
  {        isLeaf leaf() -> true(),
       isLeaf cons(u, v) -> false(),
         left cons(u, v) -> u,
        right cons(u, v) -> v,
       concat(leaf(), y) -> y,
   concat(cons(u, v), y) -> cons(u, concat(v, y)),
    if1(b, true(), u, v) -> false(),
   if1(b, false(), u, v) -> if2(b, u, v),
       less_leaves(u, v) -> if1(isLeaf u, isLeaf v, u, v),
       if2(true(), u, v) -> true(),
      if2(false(), u, v) -> less_leaves(concat(left u, right u), concat(left v, right v))}
  EDG:
   {(if2#(false(), u, v) -> concat#(left u, right u), concat#(cons(u, v), y) -> concat#(v, y))
    (less_leaves#(u, v) -> if1#(isLeaf u, isLeaf v, u, v), if1#(b, false(), u, v) -> if2#(b, u, v))
    (if2#(false(), u, v) -> less_leaves#(concat(left u, right u), concat(left v, right v)), less_leaves#(u, v) -> isLeaf# u)
    (if2#(false(), u, v) -> less_leaves#(concat(left u, right u), concat(left v, right v)), less_leaves#(u, v) -> isLeaf# v)
    (if2#(false(), u, v) -> less_leaves#(concat(left u, right u), concat(left v, right v)), less_leaves#(u, v) -> if1#(isLeaf u, isLeaf v, u, v))
    (concat#(cons(u, v), y) -> concat#(v, y), concat#(cons(u, v), y) -> concat#(v, y))
    (if2#(false(), u, v) -> concat#(left v, right v), concat#(cons(u, v), y) -> concat#(v, y))
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> left# u)
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> left# v)
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> right# u)
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> right# v)
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> concat#(left u, right u))
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> concat#(left v, right v))
    (if1#(b, false(), u, v) -> if2#(b, u, v), if2#(false(), u, v) -> less_leaves#(concat(left u, right u), concat(left v, right v)))}
   STATUS:
    arrows: 0.902778
    SCCS (2):
     Scc:
      {if1#(b, false(), u, v) -> if2#(b, u, v),
           less_leaves#(u, v) -> if1#(isLeaf u, isLeaf v, u, v),
          if2#(false(), u, v) -> less_leaves#(concat(left u, right u), concat(left v, right v))}
     Scc:
      {concat#(cons(u, v), y) -> concat#(v, y)}
     
     SCC (3):
      Strict:
       {if1#(b, false(), u, v) -> if2#(b, u, v),
            less_leaves#(u, v) -> if1#(isLeaf u, isLeaf v, u, v),
           if2#(false(), u, v) -> less_leaves#(concat(left u, right u), concat(left v, right v))}
      Weak:
      {        isLeaf leaf() -> true(),
           isLeaf cons(u, v) -> false(),
             left cons(u, v) -> u,
            right cons(u, v) -> v,
           concat(leaf(), y) -> y,
       concat(cons(u, v), y) -> cons(u, concat(v, y)),
        if1(b, true(), u, v) -> false(),
       if1(b, false(), u, v) -> if2(b, u, v),
           less_leaves(u, v) -> if1(isLeaf u, isLeaf v, u, v),
           if2(true(), u, v) -> true(),
          if2(false(), u, v) -> less_leaves(concat(left u, right u), concat(left v, right v))}
      Open
     
     
     
     
     SCC (1):
      Strict:
       {concat#(cons(u, v), y) -> concat#(v, y)}
      Weak:
      {        isLeaf leaf() -> true(),
           isLeaf cons(u, v) -> false(),
             left cons(u, v) -> u,
            right cons(u, v) -> v,
           concat(leaf(), y) -> y,
       concat(cons(u, v), y) -> cons(u, concat(v, y)),
        if1(b, true(), u, v) -> false(),
       if1(b, false(), u, v) -> if2(b, u, v),
           less_leaves(u, v) -> if1(isLeaf u, isLeaf v, u, v),
           if2(true(), u, v) -> true(),
          if2(false(), u, v) -> less_leaves(concat(left u, right u), concat(left v, right v))}
      Open