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