YES
Time: 0.002398
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()}
  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())))}
   EDG:
    {(rev# .(x, y) -> ++#(rev y, .(x, nil())), ++#(.(x, y), z) -> ++#(y, z))}
    EDG:
     {(rev# .(x, y) -> ++#(rev y, .(x, nil())), ++#(.(x, y), z) -> ++#(y, z))}
     STATUS:
      arrows: 0.888889
      SCCS (0):