(VAR x )
(RULES f (f (a, f (x, a)), a) -> f (a, f (f (x, a), a)))