(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))))))