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