(VAR x)
(RULES
a(b(a(x))) -> b(a(x))
c(x) -> a(x)
c(x) -> b(x)
)