(VAR z)
(RULES
u(v(z)) -> x(f(z))
v(b(c(z))) -> g(z)
u(g(z)) -> o(z)
f(b(c(z))) -> a(b(b(c(z))))
w(a(z)) -> f(b(z))
w(f(z)) -> a(b(z))
x(a(z)) -> o(z)
o(b(z)) -> o(z)
o(c(z)) -> o(z)
x(f(z)) -> h(z)
h(b(z)) -> h(z)
h(c(z)) -> h(z)
)