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