YES

Problem:
 flatten(nil()) -> nil()
 flatten(unit(x)) -> flatten(x)
 flatten(++(x,y)) -> ++(flatten(x),flatten(y))
 flatten(++(unit(x),y)) -> ++(flatten(x),flatten(y))
 flatten(flatten(x)) -> flatten(x)
 rev(nil()) -> nil()
 rev(unit(x)) -> unit(x)
 rev(++(x,y)) -> ++(rev(y),rev(x))
 rev(rev(x)) -> x
 ++(x,nil()) -> x
 ++(nil(),y) -> y
 ++(++(x,y),z) -> ++(x,++(y,z))

Proof:
 DP Processor:
  DPs:
   flatten#(unit(x)) -> flatten#(x)
   flatten#(++(x,y)) -> flatten#(y)
   flatten#(++(x,y)) -> flatten#(x)
   flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
   flatten#(++(unit(x),y)) -> flatten#(y)
   flatten#(++(unit(x),y)) -> flatten#(x)
   flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
   rev#(++(x,y)) -> rev#(x)
   rev#(++(x,y)) -> rev#(y)
   rev#(++(x,y)) -> ++#(rev(y),rev(x))
   ++#(++(x,y),z) -> ++#(y,z)
   ++#(++(x,y),z) -> ++#(x,++(y,z))
  TRS:
   flatten(nil()) -> nil()
   flatten(unit(x)) -> flatten(x)
   flatten(++(x,y)) -> ++(flatten(x),flatten(y))
   flatten(++(unit(x),y)) -> ++(flatten(x),flatten(y))
   flatten(flatten(x)) -> flatten(x)
   rev(nil()) -> nil()
   rev(unit(x)) -> unit(x)
   rev(++(x,y)) -> ++(rev(y),rev(x))
   rev(rev(x)) -> x
   ++(x,nil()) -> x
   ++(nil(),y) -> y
   ++(++(x,y),z) -> ++(x,++(y,z))
  TDG Processor:
   DPs:
    flatten#(unit(x)) -> flatten#(x)
    flatten#(++(x,y)) -> flatten#(y)
    flatten#(++(x,y)) -> flatten#(x)
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(unit(x),y)) -> flatten#(y)
    flatten#(++(unit(x),y)) -> flatten#(x)
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
    rev#(++(x,y)) -> rev#(x)
    rev#(++(x,y)) -> rev#(y)
    rev#(++(x,y)) -> ++#(rev(y),rev(x))
    ++#(++(x,y),z) -> ++#(y,z)
    ++#(++(x,y),z) -> ++#(x,++(y,z))
   TRS:
    flatten(nil()) -> nil()
    flatten(unit(x)) -> flatten(x)
    flatten(++(x,y)) -> ++(flatten(x),flatten(y))
    flatten(++(unit(x),y)) -> ++(flatten(x),flatten(y))
    flatten(flatten(x)) -> flatten(x)
    rev(nil()) -> nil()
    rev(unit(x)) -> unit(x)
    rev(++(x,y)) -> ++(rev(y),rev(x))
    rev(rev(x)) -> x
    ++(x,nil()) -> x
    ++(nil(),y) -> y
    ++(++(x,y),z) -> ++(x,++(y,z))
   graph:
    rev#(++(x,y)) -> rev#(y) -> rev#(++(x,y)) -> ++#(rev(y),rev(x))
    rev#(++(x,y)) -> rev#(y) -> rev#(++(x,y)) -> rev#(y)
    rev#(++(x,y)) -> rev#(y) -> rev#(++(x,y)) -> rev#(x)
    rev#(++(x,y)) -> rev#(x) -> rev#(++(x,y)) -> ++#(rev(y),rev(x))
    rev#(++(x,y)) -> rev#(x) -> rev#(++(x,y)) -> rev#(y)
    rev#(++(x,y)) -> rev#(x) -> rev#(++(x,y)) -> rev#(x)
    rev#(++(x,y)) -> ++#(rev(y),rev(x)) ->
    ++#(++(x,y),z) -> ++#(x,++(y,z))
    rev#(++(x,y)) -> ++#(rev(y),rev(x)) -> ++#(++(x,y),z) -> ++#(y,z)
    ++#(++(x,y),z) -> ++#(y,z) -> ++#(++(x,y),z) -> ++#(x,++(y,z))
    ++#(++(x,y),z) -> ++#(y,z) -> ++#(++(x,y),z) -> ++#(y,z)
    ++#(++(x,y),z) -> ++#(x,++(y,z)) ->
    ++#(++(x,y),z) -> ++#(x,++(y,z))
    ++#(++(x,y),z) -> ++#(x,++(y,z)) ->
    ++#(++(x,y),z) -> ++#(y,z)
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y)) ->
    ++#(++(x,y),z) -> ++#(x,++(y,z))
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y)) ->
    ++#(++(x,y),z) -> ++#(y,z)
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(++(unit(x),y)) -> flatten#(x)
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(++(unit(x),y)) -> flatten#(y)
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(++(x,y)) -> flatten#(x)
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(++(x,y)) -> flatten#(y)
    flatten#(++(unit(x),y)) -> flatten#(y) ->
    flatten#(unit(x)) -> flatten#(x)
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> flatten#(x)
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> flatten#(y)
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(++(x,y)) -> flatten#(x)
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(++(x,y)) -> flatten#(y)
    flatten#(++(unit(x),y)) -> flatten#(x) ->
    flatten#(unit(x)) -> flatten#(x)
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y)) ->
    ++#(++(x,y),z) -> ++#(x,++(y,z))
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y)) ->
    ++#(++(x,y),z) -> ++#(y,z)
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(++(unit(x),y)) -> flatten#(x)
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(++(unit(x),y)) -> flatten#(y)
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(++(x,y)) -> flatten#(x)
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(++(x,y)) -> flatten#(y)
    flatten#(++(x,y)) -> flatten#(y) ->
    flatten#(unit(x)) -> flatten#(x)
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> flatten#(x)
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> flatten#(y)
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(++(x,y)) -> flatten#(x)
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(++(x,y)) -> flatten#(y)
    flatten#(++(x,y)) -> flatten#(x) ->
    flatten#(unit(x)) -> flatten#(x)
    flatten#(unit(x)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
    flatten#(unit(x)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> flatten#(x)
    flatten#(unit(x)) -> flatten#(x) ->
    flatten#(++(unit(x),y)) -> flatten#(y)
    flatten#(unit(x)) -> flatten#(x) ->
    flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
    flatten#(unit(x)) -> flatten#(x) ->
    flatten#(++(x,y)) -> flatten#(x)
    flatten#(unit(x)) -> flatten#(x) ->
    flatten#(++(x,y)) -> flatten#(y)
    flatten#(unit(x)) -> flatten#(x) -> flatten#(unit(x)) -> flatten#(x)
   CDG Processor:
    DPs:
     flatten#(unit(x)) -> flatten#(x)
     flatten#(++(x,y)) -> flatten#(y)
     flatten#(++(x,y)) -> flatten#(x)
     flatten#(++(x,y)) -> ++#(flatten(x),flatten(y))
     flatten#(++(unit(x),y)) -> flatten#(y)
     flatten#(++(unit(x),y)) -> flatten#(x)
     flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y))
     rev#(++(x,y)) -> rev#(x)
     rev#(++(x,y)) -> rev#(y)
     rev#(++(x,y)) -> ++#(rev(y),rev(x))
     ++#(++(x,y),z) -> ++#(y,z)
     ++#(++(x,y),z) -> ++#(x,++(y,z))
    TRS:
     flatten(nil()) -> nil()
     flatten(unit(x)) -> flatten(x)
     flatten(++(x,y)) -> ++(flatten(x),flatten(y))
     flatten(++(unit(x),y)) -> ++(flatten(x),flatten(y))
     flatten(flatten(x)) -> flatten(x)
     rev(nil()) -> nil()
     rev(unit(x)) -> unit(x)
     rev(++(x,y)) -> ++(rev(y),rev(x))
     rev(rev(x)) -> x
     ++(x,nil()) -> x
     ++(nil(),y) -> y
     ++(++(x,y),z) -> ++(x,++(y,z))
    graph:
     rev#(++(x,y)) -> ++#(rev(y),rev(x)) ->
     ++#(++(x,y),z) -> ++#(y,z)
     rev#(++(x,y)) -> ++#(rev(y),rev(x)) ->
     ++#(++(x,y),z) -> ++#(x,++(y,z))
     flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y)) ->
     ++#(++(x,y),z) -> ++#(y,z)
     flatten#(++(unit(x),y)) -> ++#(flatten(x),flatten(y)) ->
     ++#(++(x,y),z) -> ++#(x,++(y,z))
     flatten#(++(x,y)) -> ++#(flatten(x),flatten(y)) ->
     ++#(++(x,y),z) -> ++#(y,z)
     flatten#(++(x,y)) -> ++#(flatten(x),flatten(y)) -> ++#(++(x,y),z) -> ++#(x,++(y,z))
    SCC Processor:
     #sccs: 0
     #rules: 0
     #arcs: 6/144