MAYBE
MAYBE
TRS:
 {
                    isEmpty(empty()) -> true(),
              isEmpty(node(l, x, r)) -> false(),
                       left(empty()) -> empty(),
                 left(node(l, x, r)) -> l,
                      right(empty()) -> empty(),
                right(node(l, x, r)) -> r,
                 elem(node(l, x, r)) -> x,
            append(cons(y(), ys), x) -> cons(y(), append(ys, x)),
                    append(nil(), x) -> cons(x, nil()),
         if(true(), b, n, m, xs, ys) -> xs,
   if(false(), true(), n, m, xs, ys) -> listify(n, ys),
  if(false(), false(), n, m, xs, ys) -> listify(m, xs),
                      listify(n, xs) ->
  if(
    isEmpty(n), isEmpty(left(n)), right(n),
    node(
        left(left(n)), elem(left(n)), node(right(left(n)), elem(n), right(n))
    ), xs, append(xs, n)
  ),
                           toList(n) -> listify(n, nil())
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                      isEmpty(empty()) -> true(),
                isEmpty(node(l, x, r)) -> false(),
                         left(empty()) -> empty(),
                   left(node(l, x, r)) -> l,
                        right(empty()) -> empty(),
                  right(node(l, x, r)) -> r,
                   elem(node(l, x, r)) -> x,
              append(cons(y(), ys), x) -> cons(y(), append(ys, x)),
                      append(nil(), x) -> cons(x, nil()),
           if(true(), b, n, m, xs, ys) -> xs,
     if(false(), true(), n, m, xs, ys) -> listify(n, ys),
    if(false(), false(), n, m, xs, ys) -> listify(m, xs),
                        listify(n, xs) ->
    if(
      isEmpty(n), isEmpty(left(n)), right(n),
      node(
          left(left(n)), elem(left(n)),
          node(right(left(n)), elem(n), right(n))
      ), xs, append(xs, n)
    ),
                             toList(n) -> listify(n, nil())
   }
  Fail