(VAR x y z)
(RULES
a(b(x)) -> b(a(a(x)))
b(c(x)) -> c(b(b(x)))
c(a(x)) -> a(c(c(x)))
u(a(x)) -> x
v(b(x)) -> x
w(c(x)) -> x
a(u(x)) -> x
b(v(x)) -> x
c(w(x)) -> x
)
(COMMENT Example 4.32 in \cite{SK90})