(VAR x y z ) (RULES b(a, b(c(z, x, y), a)) -> b(b(z, c(y, z, a)), x) f(c(a, b(b(z, a), y), x)) -> f(c(x, b(z, x), y)) c(f(c(a, y, a)), x, z) -> f(b(b(z, z), f(b(y, b(x, a))))) )