MAYBE
MAYBE
TRS:
 {
           flatten(nil()) -> nil(),
      flatten(flatten(x)) -> flatten(x),
         flatten(unit(x)) -> flatten(x),
        flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
  flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
             ++(x, nil()) -> x,
             ++(nil(), y) -> y,
          ++(++(x, y), z) -> ++(x, ++(y, z)),
               rev(nil()) -> nil(),
             rev(unit(x)) -> unit(x),
            rev(++(x, y)) -> ++(rev(y), rev(x)),
              rev(rev(x)) -> x
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
             flatten(nil()) -> nil(),
        flatten(flatten(x)) -> flatten(x),
           flatten(unit(x)) -> flatten(x),
          flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
    flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
               ++(x, nil()) -> x,
               ++(nil(), y) -> y,
            ++(++(x, y), z) -> ++(x, ++(y, z)),
                 rev(nil()) -> nil(),
               rev(unit(x)) -> unit(x),
              rev(++(x, y)) -> ++(rev(y), rev(x)),
                rev(rev(x)) -> x
   }
  Fail