MAYBE
Time: 0.654610
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}
 DP:
  DP:
   {       flatten# unit x -> flatten# x,
         flatten# ++(x, y) -> flatten# x,
         flatten# ++(x, y) -> flatten# y,
         flatten# ++(x, y) -> ++#(flatten x, flatten y),
    flatten# ++(unit x, y) -> flatten# x,
    flatten# ++(unit x, y) -> flatten# y,
    flatten# ++(unit x, y) -> ++#(flatten x, flatten y),
          ++#(++(x, y), z) -> ++#(x, ++(y, z)),
          ++#(++(x, y), z) -> ++#(y, z),
             rev# ++(x, y) -> ++#(rev y, rev x),
             rev# ++(x, y) -> rev# x,
             rev# ++(x, y) -> rev# y}
  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}
  EDG:
   {(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# y, flatten# ++(unit x, y) -> ++#(flatten x, flatten y))
    (flatten# ++(x, y) -> flatten# y, flatten# ++(unit x, y) -> flatten# y)
    (flatten# ++(x, y) -> flatten# y, flatten# ++(unit x, y) -> flatten# x)
    (flatten# ++(x, y) -> flatten# y, flatten# ++(x, y) -> ++#(flatten x, flatten y))
    (flatten# ++(x, y) -> flatten# y, flatten# ++(x, y) -> flatten# y)
    (flatten# ++(x, y) -> flatten# y, flatten# ++(x, y) -> flatten# x)
    (flatten# ++(x, y) -> flatten# y, flatten# unit x -> flatten# 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# y, rev# ++(x, y) -> ++#(rev y, rev x))
    (++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(y, z))
    (++#(++(x, y), z) -> ++#(y, z), ++#(++(x, y), z) -> ++#(x, ++(y, z)))
    (flatten# ++(x, y) -> flatten# x, flatten# ++(unit x, y) -> ++#(flatten x, flatten y))
    (flatten# ++(x, y) -> flatten# x, flatten# ++(unit x, y) -> flatten# y)
    (flatten# ++(x, y) -> flatten# x, flatten# ++(unit x, y) -> flatten# x)
    (flatten# ++(x, y) -> flatten# x, flatten# ++(x, y) -> ++#(flatten x, flatten y))
    (flatten# ++(x, y) -> flatten# x, flatten# ++(x, y) -> flatten# y)
    (flatten# ++(x, y) -> flatten# x, flatten# ++(x, y) -> flatten# x)
    (flatten# ++(x, y) -> flatten# x, flatten# unit x -> flatten# 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# x, rev# ++(x, y) -> ++#(rev y, rev x))
    (flatten# ++(unit x, y) -> flatten# x, flatten# unit x -> flatten# x)
    (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# ++(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# ++(unit x, y) -> ++#(flatten x, flatten y))
    (flatten# unit x -> flatten# x, flatten# unit x -> flatten# x)
    (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# ++(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# ++(unit x, y) -> ++#(flatten x, flatten y))
    (++#(++(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# y, flatten# unit x -> flatten# x)
    (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# ++(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# ++(unit x, y) -> ++#(flatten x, flatten y))
    (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))
    (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))}
   STATUS:
    arrows: 0.645833
    SCCS (3):
     Scc:
      {rev# ++(x, y) -> rev# x,
       rev# ++(x, y) -> rev# y}
     Scc:
      {       flatten# unit x -> flatten# x,
            flatten# ++(x, y) -> flatten# x,
            flatten# ++(x, y) -> flatten# y,
       flatten# ++(unit x, y) -> flatten# x,
       flatten# ++(unit x, y) -> flatten# y}
     Scc:
      {++#(++(x, y), z) -> ++#(x, ++(y, z)),
       ++#(++(x, y), z) -> ++#(y, z)}
     
     SCC (2):
      Strict:
       {rev# ++(x, y) -> rev# x,
        rev# ++(x, y) -> rev# y}
      Weak:
      {        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}
      Open
     SCC (5):
      Strict:
       {       flatten# unit x -> flatten# x,
             flatten# ++(x, y) -> flatten# x,
             flatten# ++(x, y) -> flatten# y,
        flatten# ++(unit x, y) -> flatten# x,
        flatten# ++(unit x, y) -> flatten# y}
      Weak:
      {        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}
      Open
     
     
     
     SCC (2):
      Strict:
       {++#(++(x, y), z) -> ++#(x, ++(y, z)),
        ++#(++(x, y), z) -> ++#(y, z)}
      Weak:
      {        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}
      Open