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))
  TDG 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))
   graph:
    +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(y,z)
    *#(*(x,y),z) -> *#(y,z) -> *#(*(x,y),z) -> *#(x,*(y,z))
    *#(*(x,y),z) -> *#(y,z) -> *#(*(x,y),z) -> *#(y,z)
    *#(*(x,y),z) -> *#(y,z) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    *#(*(x,y),z) -> *#(y,z) -> *#(+(y,z),x) -> *#(x,y)
    *#(*(x,y),z) -> *#(y,z) -> *#(+(y,z),x) -> *#(x,z)
    *#(*(x,y),z) -> *#(y,z) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
    *#(*(x,y),z) -> *#(y,z) -> *#(x,+(y,z)) -> *#(x,y)
    *#(*(x,y),z) -> *#(y,z) -> *#(x,+(y,z)) -> *#(x,z)
    *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(x,*(y,z))
    *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(y,z)
    *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(+(y,z),x) -> *#(x,y)
    *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(+(y,z),x) -> *#(x,z)
    *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
    *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(x,+(y,z)) -> *#(x,y)
    *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(x,+(y,z)) -> *#(x,z)
    *#(+(y,z),x) -> +#(*(x,y),*(x,z)) ->
    +#(+(x,y),z) -> +#(x,+(y,z))
    *#(+(y,z),x) -> +#(*(x,y),*(x,z)) -> +#(+(x,y),z) -> +#(y,z)
    *#(+(y,z),x) -> *#(x,z) -> *#(*(x,y),z) -> *#(x,*(y,z))
    *#(+(y,z),x) -> *#(x,z) -> *#(*(x,y),z) -> *#(y,z)
    *#(+(y,z),x) -> *#(x,z) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    *#(+(y,z),x) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,y)
    *#(+(y,z),x) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,z)
    *#(+(y,z),x) -> *#(x,z) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
    *#(+(y,z),x) -> *#(x,z) -> *#(x,+(y,z)) -> *#(x,y)
    *#(+(y,z),x) -> *#(x,z) -> *#(x,+(y,z)) -> *#(x,z)
    *#(+(y,z),x) -> *#(x,y) -> *#(*(x,y),z) -> *#(x,*(y,z))
    *#(+(y,z),x) -> *#(x,y) -> *#(*(x,y),z) -> *#(y,z)
    *#(+(y,z),x) -> *#(x,y) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    *#(+(y,z),x) -> *#(x,y) -> *#(+(y,z),x) -> *#(x,y)
    *#(+(y,z),x) -> *#(x,y) -> *#(+(y,z),x) -> *#(x,z)
    *#(+(y,z),x) -> *#(x,y) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
    *#(+(y,z),x) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,y)
    *#(+(y,z),x) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,z)
    *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) ->
    +#(+(x,y),z) -> +#(x,+(y,z))
    *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(+(x,y),z) -> +#(y,z)
    *#(x,+(y,z)) -> *#(x,z) -> *#(*(x,y),z) -> *#(x,*(y,z))
    *#(x,+(y,z)) -> *#(x,z) -> *#(*(x,y),z) -> *#(y,z)
    *#(x,+(y,z)) -> *#(x,z) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    *#(x,+(y,z)) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,y)
    *#(x,+(y,z)) -> *#(x,z) -> *#(+(y,z),x) -> *#(x,z)
    *#(x,+(y,z)) -> *#(x,z) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
    *#(x,+(y,z)) -> *#(x,z) -> *#(x,+(y,z)) -> *#(x,y)
    *#(x,+(y,z)) -> *#(x,z) -> *#(x,+(y,z)) -> *#(x,z)
    *#(x,+(y,z)) -> *#(x,y) -> *#(*(x,y),z) -> *#(x,*(y,z))
    *#(x,+(y,z)) -> *#(x,y) -> *#(*(x,y),z) -> *#(y,z)
    *#(x,+(y,z)) -> *#(x,y) -> *#(+(y,z),x) -> +#(*(x,y),*(x,z))
    *#(x,+(y,z)) -> *#(x,y) -> *#(+(y,z),x) -> *#(x,y)
    *#(x,+(y,z)) -> *#(x,y) -> *#(+(y,z),x) -> *#(x,z)
    *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
    *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,y)
    *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,z)
   SCC Processor:
    #sccs: 2
    #rules: 8
    #arcs: 56/100
    DPs:
     *#(*(x,y),z) -> *#(y,z)
     *#(x,+(y,z)) -> *#(x,z)
     *#(x,+(y,z)) -> *#(x,y)
     *#(+(y,z),x) -> *#(x,z)
     *#(+(y,z),x) -> *#(x,y)
     *#(*(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
    
    DPs:
     +#(+(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))
    Subterm Criterion Processor:
     simple projection:
      pi(+#) = 0
     problem:
      DPs:
       
      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))
     Qed