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