TIMEOUT
MAYBE
Trs:
 {    flatten(flatten(x)) -> flatten(x),
         flatten(unit(x)) -> flatten(x),
           flatten(nil()) -> nil(),
  flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y)),
        flatten(++(x, y)) -> ++(flatten(x), flatten(y)),
             rev(unit(x)) -> unit(x),
              rev(rev(x)) -> x,
               rev(nil()) -> nil(),
            rev(++(x, y)) -> ++(rev(y), rev(x)),
             ++(nil(), y) -> y,
          ++(++(x, y), z) -> ++(x, ++(y, z)),
             ++(x, nil()) -> x}
 Open