YES
Time: 0.001094
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()}
 RUF:
  Strict:
   {     rev nil() -> nil(),
       rev .(x, y) -> ++(rev y, .(x, nil())),
      ++(nil(), y) -> y,
    ++(.(x, y), z) -> .(x, ++(y, z))}
  Weak:
   {}
  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))}
   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())))}
    SCCS (2):
     Scc:
      {++#(.(x, y), z) -> ++#(y, z)}
     Scc:
      {rev# .(x, y) -> rev# y}
     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))}
      SPSC:
       Simple Projection:
        pi(++#) = 0
       Strict:
        {}
       Qed
     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))}
      SPSC:
       Simple Projection:
        pi(rev#) = 0
       Strict:
        {}
       Qed