(VAR x y)
(RULES
car(.(x, y)) -> x
cdr(.(x, y)) -> y
.(car(x), cdr(x)) -> x
atom(.(x, y)) -> false
)
(COMMENT Example 3.16 in \cite{SK90})