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