MAYBE

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

Proof:
 DP Processor:
  DPs:
   +#(*(x,y),*(x,z)) -> +#(y,z)
   +#(+(x,y),z) -> +#(y,z)
   +#(+(x,y),z) -> +#(x,+(y,z))
   +#(*(x,y),+(*(x,z),u())) -> +#(y,z)
   +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u())
  TRS:
   +(*(x,y),*(x,z)) -> *(x,+(y,z))
   +(+(x,y),z) -> +(x,+(y,z))
   +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u())
  SCC Processor:
   #sccs: 1
   #rules: 5
   #arcs: 25/25
   DPs:
    +#(*(x,y),*(x,z)) -> +#(y,z)
    +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z))
    +#(*(x,y),+(*(x,z),u())) -> +#(y,z)
    +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u())
   TRS:
    +(*(x,y),*(x,z)) -> *(x,+(y,z))
    +(+(x,y),z) -> +(x,+(y,z))
    +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u())
   Open