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