MAYBE

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

Proof:
 DP Processor:
  DPs:
   +#(x,+(y,z)) -> +#(x,y)
   +#(x,+(y,z)) -> +#(+(x,y),z)
   *#(x,+(y,z)) -> *#(x,z)
   *#(x,+(y,z)) -> *#(x,y)
   *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
   +#(+(x,*(y,z)),*(y,u)) -> +#(z,u)
   +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u))
   +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u)))
  TRS:
   +(x,+(y,z)) -> +(+(x,y),z)
   *(x,+(y,z)) -> +(*(x,y),*(x,z))
   +(+(x,*(y,z)),*(y,u)) -> +(x,*(y,+(z,u)))
  TDG Processor:
   DPs:
    +#(x,+(y,z)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(+(x,y),z)
    *#(x,+(y,z)) -> *#(x,z)
    *#(x,+(y,z)) -> *#(x,y)
    *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
    +#(+(x,*(y,z)),*(y,u)) -> +#(z,u)
    +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u))
    +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u)))
   TRS:
    +(x,+(y,z)) -> +(+(x,y),z)
    *(x,+(y,z)) -> +(*(x,y),*(x,z))
    +(+(x,*(y,z)),*(y,u)) -> +(x,*(y,+(z,u)))
   graph:
    *#(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),*(x,z))
    *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,y)
    *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,z)
    *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) ->
    +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u)))
    *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) ->
    +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u))
    *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) ->
    +#(+(x,*(y,z)),*(y,u)) -> +#(z,u)
    *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) ->
    +#(x,+(y,z)) -> +#(+(x,y),z)
    *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) ->
    +#(x,+(y,z)) -> +#(x,y)
    +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) ->
    *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
    +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) ->
    *#(x,+(y,z)) -> *#(x,y)
    +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) ->
    *#(x,+(y,z)) -> *#(x,z)
    +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) ->
    +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u)))
    +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) ->
    +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u))
    +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) ->
    +#(+(x,*(y,z)),*(y,u)) -> +#(z,u)
    +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) ->
    +#(x,+(y,z)) -> +#(+(x,y),z)
    +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) ->
    +#(x,+(y,z)) -> +#(x,y)
    +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) ->
    +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u)))
    +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) ->
    +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u))
    +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) ->
    +#(+(x,*(y,z)),*(y,u)) -> +#(z,u)
    +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) ->
    +#(x,+(y,z)) -> +#(+(x,y),z)
    +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) ->
    +#(x,+(y,z)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(+(x,y),z) ->
    +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u)))
    +#(x,+(y,z)) -> +#(+(x,y),z) ->
    +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u))
    +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(+(x,*(y,z)),*(y,u)) -> +#(z,u)
    +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z)
    +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(x,y)
    +#(x,+(y,z)) -> +#(x,y) -> +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u)))
    +#(x,+(y,z)) -> +#(x,y) -> +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u))
    +#(x,+(y,z)) -> +#(x,y) -> +#(+(x,*(y,z)),*(y,u)) -> +#(z,u)
    +#(x,+(y,z)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(+(x,y),z)
    +#(x,+(y,z)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(x,y)
   Restore Modifier:
    DPs:
     +#(x,+(y,z)) -> +#(x,y)
     +#(x,+(y,z)) -> +#(+(x,y),z)
     *#(x,+(y,z)) -> *#(x,z)
     *#(x,+(y,z)) -> *#(x,y)
     *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
     +#(+(x,*(y,z)),*(y,u)) -> +#(z,u)
     +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u))
     +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u)))
    TRS:
     +(x,+(y,z)) -> +(+(x,y),z)
     *(x,+(y,z)) -> +(*(x,y),*(x,z))
     +(+(x,*(y,z)),*(y,u)) -> +(x,*(y,+(z,u)))
    SCC Processor:
     #sccs: 1
     #rules: 8
     #arcs: 34/64
     DPs:
      *#(x,+(y,z)) -> *#(x,z)
      *#(x,+(y,z)) -> *#(x,y)
      *#(x,+(y,z)) -> +#(*(x,y),*(x,z))
      +#(x,+(y,z)) -> +#(x,y)
      +#(x,+(y,z)) -> +#(+(x,y),z)
      +#(+(x,*(y,z)),*(y,u)) -> +#(z,u)
      +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u))
      +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u)))
     TRS:
      +(x,+(y,z)) -> +(+(x,y),z)
      *(x,+(y,z)) -> +(*(x,y),*(x,z))
      +(+(x,*(y,z)),*(y,u)) -> +(x,*(y,+(z,u)))
     Open