MAYBE
Time: 0.030944
TRS:
 {    *(x, *(y, z)) -> *(otimes(x, y), z),
  *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z)),
          *(1(), y) -> y,
      *(+(x, y), z) -> oplus(*(x, z), *(y, z))}
 DP:
  DP:
   {    *#(x, *(y, z)) -> *#(otimes(x, y), z),
    *#(x, oplus(y, z)) -> *#(x, y),
    *#(x, oplus(y, z)) -> *#(x, z),
        *#(+(x, y), z) -> *#(x, z),
        *#(+(x, y), z) -> *#(y, z)}
  TRS:
  {    *(x, *(y, z)) -> *(otimes(x, y), z),
   *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z)),
           *(1(), y) -> y,
       *(+(x, y), z) -> oplus(*(x, z), *(y, z))}
  EDG:
   {(*#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(y, z))
    (*#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(x, z))
    (*#(x, oplus(y, z)) -> *#(x, y), *#(x, oplus(y, z)) -> *#(x, z))
    (*#(x, oplus(y, z)) -> *#(x, y), *#(x, oplus(y, z)) -> *#(x, y))
    (*#(x, oplus(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(otimes(x, y), z))
    (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(y, z))
    (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(x, z))
    (*#(+(x, y), z) -> *#(x, z), *#(x, oplus(y, z)) -> *#(x, z))
    (*#(+(x, y), z) -> *#(x, z), *#(x, oplus(y, z)) -> *#(x, y))
    (*#(+(x, y), z) -> *#(x, z), *#(x, *(y, z)) -> *#(otimes(x, y), z))
    (*#(+(x, y), z) -> *#(y, z), *#(x, *(y, z)) -> *#(otimes(x, y), z))
    (*#(+(x, y), z) -> *#(y, z), *#(x, oplus(y, z)) -> *#(x, y))
    (*#(+(x, y), z) -> *#(y, z), *#(x, oplus(y, z)) -> *#(x, z))
    (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(x, z))
    (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z))
    (*#(x, oplus(y, z)) -> *#(x, z), *#(x, *(y, z)) -> *#(otimes(x, y), z))
    (*#(x, oplus(y, z)) -> *#(x, z), *#(x, oplus(y, z)) -> *#(x, y))
    (*#(x, oplus(y, z)) -> *#(x, z), *#(x, oplus(y, z)) -> *#(x, z))
    (*#(x, oplus(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z))
    (*#(x, oplus(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(y, z))
    (*#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, *(y, z)) -> *#(otimes(x, y), z))
    (*#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, y))
    (*#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, z))}
   STATUS:
    arrows: 0.080000
    SCCS (1):
     Scc:
      {    *#(x, *(y, z)) -> *#(otimes(x, y), z),
       *#(x, oplus(y, z)) -> *#(x, y),
       *#(x, oplus(y, z)) -> *#(x, z),
           *#(+(x, y), z) -> *#(x, z),
           *#(+(x, y), z) -> *#(y, z)}
     
     SCC (5):
      Strict:
       {    *#(x, *(y, z)) -> *#(otimes(x, y), z),
        *#(x, oplus(y, z)) -> *#(x, y),
        *#(x, oplus(y, z)) -> *#(x, z),
            *#(+(x, y), z) -> *#(x, z),
            *#(+(x, y), z) -> *#(y, z)}
      Weak:
      {    *(x, *(y, z)) -> *(otimes(x, y), z),
       *(x, oplus(y, z)) -> oplus(*(x, y), *(x, z)),
               *(1(), y) -> y,
           *(+(x, y), z) -> oplus(*(x, z), *(y, z))}
      Open