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