MAYBE
Time: 1.759489
TRS:
 {            +(x, +(y, z)) -> +(+(x, y), z),
  +(+(x, *(y, z)), *(y, u)) -> +(x, *(y, +(z, u))),
              *(x, +(y, z)) -> +(*(x, y), *(x, z))}
 DP:
  DP:
   {            +#(x, +(y, z)) -> +#(x, y),
                +#(x, +(y, z)) -> +#(+(x, y), z),
    +#(+(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)) -> +#(*(x, y), *(x, z)),
                *#(x, +(y, z)) -> *#(x, y),
                *#(x, +(y, z)) -> *#(x, z)}
  TRS:
  {            +(x, +(y, z)) -> +(+(x, y), z),
   +(+(x, *(y, z)), *(y, u)) -> +(x, *(y, +(z, u))),
               *(x, +(y, z)) -> +(*(x, y), *(x, z))}
  UR:
   {            +(x, +(y, z)) -> +(+(x, y), z),
    +(+(x, *(y, z)), *(y, u)) -> +(x, *(y, +(z, u))),
                *(x, +(y, z)) -> +(*(x, y), *(x, z)),
                      a(w, v) -> w,
                      a(w, v) -> v}
   EDG:
    {(+#(+(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)), *(y, u)) -> +#(x, *(y, +(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)) -> +#(*(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)), *(y, u)) -> +#(x, *(y, +(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)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z))
     (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y))
     (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)))
     (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z))
     (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(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, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z))
     (+#(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)) -> +#(z, u))
     (+#(x, +(y, z)) -> +#(+(x, y), z), +#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u)))
     (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y))
     (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z))
     (+#(x, +(y, z)) -> +#(x, y), +#(+(x, *(y, z)), *(y, u)) -> +#(x, *(y, +(z, u))))
     (+#(x, +(y, z)) -> +#(x, y), +#(+(x, *(y, z)), *(y, u)) -> +#(z, u))
     (+#(x, +(y, z)) -> +#(x, y), +#(+(x, *(y, z)), *(y, u)) -> *#(y, +(z, u)))
     (+#(+(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)) -> +#(x, *(y, +(z, u))), +#(x, +(y, z)) -> +#(x, y))
     (+#(+(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)), *(y, u)) -> +#(x, *(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)), *(y, u)) -> *#(y, +(z, u)))}
    STATUS:
     arrows: 0.468750
     SCCS (1):
      Scc:
       {            +#(x, +(y, z)) -> +#(x, y),
                    +#(x, +(y, z)) -> +#(+(x, y), z),
        +#(+(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)) -> +#(*(x, y), *(x, z)),
                    *#(x, +(y, z)) -> *#(x, y),
                    *#(x, +(y, z)) -> *#(x, z)}
      
      SCC (8):
       Strict:
        {            +#(x, +(y, z)) -> +#(x, y),
                     +#(x, +(y, z)) -> +#(+(x, y), z),
         +#(+(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)) -> +#(*(x, y), *(x, z)),
                     *#(x, +(y, z)) -> *#(x, y),
                     *#(x, +(y, z)) -> *#(x, z)}
       Weak:
       {            +(x, +(y, z)) -> +(+(x, y), z),
        +(+(x, *(y, z)), *(y, u)) -> +(x, *(y, +(z, u))),
                    *(x, +(y, z)) -> +(*(x, y), *(x, z))}
       Open