(VAR x y z)
(RULES
  +(x,y) -> +(y,x)
  *(+(x,y),z) -> +(*(x,z),*(y,z))
  *(+(y,x),z) -> +(*(x,z),*(y,z))
)
(COMMENT from \cite{NM16})