MAYBE
Trs:
 {        *(1(), y) -> y,
      *(+(x, y), z) -> oplus(*(x, z), *(y, z)),
      *(x, *(y, z)) -> *(otimes(x, y), z),
  *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z))}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open