MAYBE
Time: 0.000965
TRS:
 {     rev nil() -> nil(),
     rev .(x, y) -> ++(rev y, .(x, nil())),
    ++(nil(), y) -> y,
  ++(.(x, y), z) -> .(x, ++(y, z)),
     car .(x, y) -> x,
     cdr .(x, y) -> y,
      null nil() -> true(),
    null .(x, y) -> false()}
 DP:
  DP:
   {   rev# .(x, y) -> rev# y,
       rev# .(x, y) -> ++#(rev y, .(x, nil())),
    ++#(.(x, y), z) -> ++#(y, z)}
  TRS:
  {     rev nil() -> nil(),
      rev .(x, y) -> ++(rev y, .(x, nil())),
     ++(nil(), y) -> y,
   ++(.(x, y), z) -> .(x, ++(y, z)),
      car .(x, y) -> x,
      cdr .(x, y) -> y,
       null nil() -> true(),
     null .(x, y) -> false()}
  UR:
   {     rev nil() -> nil(),
       rev .(x, y) -> ++(rev y, .(x, nil())),
      ++(nil(), y) -> y,
    ++(.(x, y), z) -> .(x, ++(y, z))}
   EDG:
    {(++#(.(x, y), z) -> ++#(y, z), ++#(.(x, y), z) -> ++#(y, z))
     (rev# .(x, y) -> ++#(rev y, .(x, nil())), ++#(.(x, y), z) -> ++#(y, z))
     (rev# .(x, y) -> rev# y, rev# .(x, y) -> rev# y)
     (rev# .(x, y) -> rev# y, rev# .(x, y) -> ++#(rev y, .(x, nil())))}
    STATUS:
     arrows: 0.555556
     SCCS (2):
      Scc:
       {rev# .(x, y) -> rev# y}
      Scc:
       {++#(.(x, y), z) -> ++#(y, z)}
      
      SCC (1):
       Strict:
        {rev# .(x, y) -> rev# y}
       Weak:
       {     rev nil() -> nil(),
           rev .(x, y) -> ++(rev y, .(x, nil())),
          ++(nil(), y) -> y,
        ++(.(x, y), z) -> .(x, ++(y, z)),
           car .(x, y) -> x,
           cdr .(x, y) -> y,
            null nil() -> true(),
          null .(x, y) -> false()}
       Open
      
      SCC (1):
       Strict:
        {++#(.(x, y), z) -> ++#(y, z)}
       Weak:
       {     rev nil() -> nil(),
           rev .(x, y) -> ++(rev y, .(x, nil())),
          ++(nil(), y) -> y,
        ++(.(x, y), z) -> .(x, ++(y, z)),
           car .(x, y) -> x,
           cdr .(x, y) -> y,
            null nil() -> true(),
          null .(x, y) -> false()}
       Open