MAYBE
Time: 0.002070
TRS:
 {      rev nil() -> nil(),
        rev rev x -> x,
     rev ++(x, y) -> ++(rev y, rev x),
     ++(x, nil()) -> x,
  ++(x, ++(y, z)) -> ++(++(x, y), z),
     ++(nil(), y) -> y,
   ++(.(x, y), z) -> .(x, ++(y, z)),
           make x -> .(x, nil())}
 DP:
  DP:
   {   rev# ++(x, y) -> rev# x,
       rev# ++(x, y) -> rev# y,
       rev# ++(x, y) -> ++#(rev y, rev x),
    ++#(x, ++(y, z)) -> ++#(x, y),
    ++#(x, ++(y, z)) -> ++#(++(x, y), z),
     ++#(.(x, y), z) -> ++#(y, z)}
  TRS:
  {      rev nil() -> nil(),
         rev rev x -> x,
      rev ++(x, y) -> ++(rev y, rev x),
      ++(x, nil()) -> x,
   ++(x, ++(y, z)) -> ++(++(x, y), z),
      ++(nil(), y) -> y,
    ++(.(x, y), z) -> .(x, ++(y, z)),
            make x -> .(x, nil())}
  UR:
   {      rev nil() -> nil(),
          rev rev x -> x,
       rev ++(x, y) -> ++(rev y, rev x),
       ++(x, nil()) -> x,
    ++(x, ++(y, z)) -> ++(++(x, y), z),
       ++(nil(), y) -> y,
     ++(.(x, y), z) -> .(x, ++(y, z))}
   EDG:
    {(++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z))
     (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(++(x, y), z))
     (++#(.(x, y), z) -> ++#(y, z), ++#(x, ++(y, z)) -> ++#(x, y))
     (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))
     (rev# ++(x, y) -> ++#(rev y, rev x), ++#(x, ++(y, z)) -> ++#(x, y))
     (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)
     (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(x, ++(y, z)) -> ++#(x, y))
     (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(x, ++(y, z)) -> ++#(++(x, y), z))
     (++#(x, ++(y, z)) -> ++#(++(x, y), z), ++#(.(x, y), z) -> ++#(y, z))
     (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(x, y))
     (++#(x, ++(y, z)) -> ++#(x, y), ++#(x, ++(y, z)) -> ++#(++(x, y), z))
     (++#(x, ++(y, z)) -> ++#(x, y), ++#(.(x, y), z) -> ++#(y, z))
     (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> rev# x)
     (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> rev# y)
     (rev# ++(x, y) -> rev# y, rev# ++(x, y) -> ++#(rev y, rev x))}
    STATUS:
     arrows: 0.500000
     SCCS (2):
      Scc:
       {rev# ++(x, y) -> rev# x,
        rev# ++(x, y) -> rev# y}
      Scc:
       {++#(x, ++(y, z)) -> ++#(x, y),
        ++#(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:
       {      rev nil() -> nil(),
              rev rev x -> x,
           rev ++(x, y) -> ++(rev y, rev x),
           ++(x, nil()) -> x,
        ++(x, ++(y, z)) -> ++(++(x, y), z),
           ++(nil(), y) -> y,
         ++(.(x, y), z) -> .(x, ++(y, z)),
                 make x -> .(x, nil())}
       Open
      
      SCC (3):
       Strict:
        {++#(x, ++(y, z)) -> ++#(x, y),
         ++#(x, ++(y, z)) -> ++#(++(x, y), z),
          ++#(.(x, y), z) -> ++#(y, z)}
       Weak:
       {      rev nil() -> nil(),
              rev rev x -> x,
           rev ++(x, y) -> ++(rev y, rev x),
           ++(x, nil()) -> x,
        ++(x, ++(y, z)) -> ++(++(x, y), z),
           ++(nil(), y) -> y,
         ++(.(x, y), z) -> .(x, ++(y, z)),
                 make x -> .(x, nil())}
       Open