MAYBE
Time: 0.003718
TRS:
 {        rev nil() -> nil(),
       rev ++(x, y) -> ++(rev1(x, y), rev2(x, y)),
     rev1(x, nil()) -> x,
  rev1(x, ++(y, z)) -> rev1(y, z),
     rev2(x, nil()) -> nil(),
  rev2(x, ++(y, z)) -> rev ++(x, rev rev2(y, z))}
 DP:
  DP:
   {     rev# ++(x, y) -> rev1#(x, y),
         rev# ++(x, y) -> rev2#(x, y),
    rev1#(x, ++(y, z)) -> rev1#(y, z),
    rev2#(x, ++(y, z)) -> rev# ++(x, rev rev2(y, z)),
    rev2#(x, ++(y, z)) -> rev# rev2(y, z),
    rev2#(x, ++(y, z)) -> rev2#(y, z)}
  TRS:
  {        rev nil() -> nil(),
        rev ++(x, y) -> ++(rev1(x, y), rev2(x, y)),
      rev1(x, nil()) -> x,
   rev1(x, ++(y, z)) -> rev1(y, z),
      rev2(x, nil()) -> nil(),
   rev2(x, ++(y, z)) -> rev ++(x, rev rev2(y, z))}
  EDG:
   {(rev2#(x, ++(y, z)) -> rev2#(y, z), rev2#(x, ++(y, z)) -> rev2#(y, z))
    (rev2#(x, ++(y, z)) -> rev2#(y, z), rev2#(x, ++(y, z)) -> rev# rev2(y, z))
    (rev2#(x, ++(y, z)) -> rev2#(y, z), rev2#(x, ++(y, z)) -> rev# ++(x, rev rev2(y, z)))
    (rev# ++(x, y) -> rev2#(x, y), rev2#(x, ++(y, z)) -> rev2#(y, z))
    (rev# ++(x, y) -> rev2#(x, y), rev2#(x, ++(y, z)) -> rev# rev2(y, z))
    (rev# ++(x, y) -> rev2#(x, y), rev2#(x, ++(y, z)) -> rev# ++(x, rev rev2(y, z)))
    (rev2#(x, ++(y, z)) -> rev# rev2(y, z), rev# ++(x, y) -> rev2#(x, y))
    (rev2#(x, ++(y, z)) -> rev# rev2(y, z), rev# ++(x, y) -> rev1#(x, y))
    (rev2#(x, ++(y, z)) -> rev# ++(x, rev rev2(y, z)), rev# ++(x, y) -> rev1#(x, y))
    (rev2#(x, ++(y, z)) -> rev# ++(x, rev rev2(y, z)), rev# ++(x, y) -> rev2#(x, y))
    (rev# ++(x, y) -> rev1#(x, y), rev1#(x, ++(y, z)) -> rev1#(y, z))
    (rev1#(x, ++(y, z)) -> rev1#(y, z), rev1#(x, ++(y, z)) -> rev1#(y, z))}
   STATUS:
    arrows: 0.666667
    SCCS (2):
     Scc:
      {     rev# ++(x, y) -> rev2#(x, y),
       rev2#(x, ++(y, z)) -> rev# ++(x, rev rev2(y, z)),
       rev2#(x, ++(y, z)) -> rev# rev2(y, z),
       rev2#(x, ++(y, z)) -> rev2#(y, z)}
     Scc:
      {rev1#(x, ++(y, z)) -> rev1#(y, z)}
     
     SCC (4):
      Strict:
       {     rev# ++(x, y) -> rev2#(x, y),
        rev2#(x, ++(y, z)) -> rev# ++(x, rev rev2(y, z)),
        rev2#(x, ++(y, z)) -> rev# rev2(y, z),
        rev2#(x, ++(y, z)) -> rev2#(y, z)}
      Weak:
      {        rev nil() -> nil(),
            rev ++(x, y) -> ++(rev1(x, y), rev2(x, y)),
          rev1(x, nil()) -> x,
       rev1(x, ++(y, z)) -> rev1(y, z),
          rev2(x, nil()) -> nil(),
       rev2(x, ++(y, z)) -> rev ++(x, rev rev2(y, z))}
      Open
     
     SCC (1):
      Strict:
       {rev1#(x, ++(y, z)) -> rev1#(y, z)}
      Weak:
      {        rev nil() -> nil(),
            rev ++(x, y) -> ++(rev1(x, y), rev2(x, y)),
          rev1(x, nil()) -> x,
       rev1(x, ++(y, z)) -> rev1(y, z),
          rev2(x, nil()) -> nil(),
       rev2(x, ++(y, z)) -> rev ++(x, rev rev2(y, z))}
      Open