MAYBE

Problem:
 *(x,+(y,z)) -> +(*(x,y),*(x,z))
 *(+(y,z),x) -> +(*(x,y),*(x,z))
 *(*(x,y),z) -> *(x,*(y,z))
 +(+(x,y),z) -> +(x,+(y,z))

Proof:
 DP Processor:
  DPs:
   *#(x,+(y,z)) -> *#(x,z)
   *#(x,+(y,z)) -> *#(x,y)
   *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
   *#(+(y,z),x) -> *#(x,z)
   *#(+(y,z),x) -> *#(x,y)
   *#(+(y,z),x) -> +#(*(x,y),*(x,z))
   *#(*(x,y),z) -> *#(y,z)
   *#(*(x,y),z) -> *#(x,*(y,z))
   +#(+(x,y),z) -> +#(y,z)
   +#(+(x,y),z) -> +#(x,+(y,z))
  TRS:
   *(x,+(y,z)) -> +(*(x,y),*(x,z))
   *(+(y,z),x) -> +(*(x,y),*(x,z))
   *(*(x,y),z) -> *(x,*(y,z))
   +(+(x,y),z) -> +(x,+(y,z))
  Open