MAYBE
Trs:
 {        f(a(), y) -> a(),
          f(b(), y) -> b(),
      f(+(x, y), z) -> +(f(x, z), f(y, z)),
        +(a(), b()) -> +(b(), a()),
  +(a(), +(b(), z)) -> +(b(), +(a(), z)),
      +(+(x, y), z) -> +(x, +(y, z))}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open