MAYBE
Time: 0.070542
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))}
  UR:
   {        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)),
              a(w, v) -> w,
              a(w, v) -> v}
   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