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