YES
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:
  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))}
  EDG:
   {(*#(+(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)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, z))
    (*#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, oplus(y, z)) -> *#(x, y))
    (*#(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, y), *#(x, oplus(y, z)) -> *#(x, y))
    (*#(x, oplus(y, z)) -> *#(x, y), *#(x, oplus(y, z)) -> *#(x, z))
    (*#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(x, z))
    (*#(x, oplus(y, z)) -> *#(x, y), *#(+(x, y), z) -> *#(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))}
   SCCS:
    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:
     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))}
     SPSC:
      Simple Projection:
       pi(*#) = 1
      Strict:
       {    *#(x, *(y, z)) -> *#(otimes(x, y), z),
        *#(x, oplus(y, z)) -> *#(x, z),
            *#(+(x, y), z) -> *#(x, z),
            *#(+(x, y), z) -> *#(y, z)}
      EDG:
       {(*#(x, oplus(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(y, z))
        (*#(x, oplus(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z))
        (*#(x, oplus(y, z)) -> *#(x, z), *#(x, oplus(y, z)) -> *#(x, z))
        (*#(x, oplus(y, z)) -> *#(x, z), *#(x, *(y, z)) -> *#(otimes(x, y), z))
        (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z))
        (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(x, z))
        (*#(+(x, y), z) -> *#(y, z), *#(x, oplus(y, z)) -> *#(x, z))
        (*#(+(x, y), z) -> *#(y, z), *#(x, *(y, z)) -> *#(otimes(x, y), z))
        (*#(+(x, y), z) -> *#(x, z), *#(x, *(y, z)) -> *#(otimes(x, y), z))
        (*#(+(x, y), z) -> *#(x, z), *#(x, oplus(y, z)) -> *#(x, z))
        (*#(+(x, y), z) -> *#(x, z), *#(+(x, y), z) -> *#(x, z))
        (*#(+(x, 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, z))}
       SCCS:
        Scc:
         {    *#(x, *(y, z)) -> *#(otimes(x, y), z),
          *#(x, oplus(y, z)) -> *#(x, z),
              *#(+(x, y), z) -> *#(x, z),
              *#(+(x, y), z) -> *#(y, z)}
        SCC:
         Strict:
          {    *#(x, *(y, z)) -> *#(otimes(x, y), z),
           *#(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))}
         SPSC:
          Simple Projection:
           pi(*#) = 1
          Strict:
           {*#(x, *(y, z)) -> *#(otimes(x, y), z),
            *#(+(x, y), z) -> *#(x, z),
            *#(+(x, y), z) -> *#(y, z)}
          EDG:
           {(*#(+(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, *(y, z)) -> *#(otimes(x, y), z))
            (*#(+(x, y), z) -> *#(y, z), *#(x, *(y, z)) -> *#(otimes(x, y), z))
            (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(x, z))
            (*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z))
            (*#(x, *(y, z)) -> *#(otimes(x, y), z), *#(x, *(y, z)) -> *#(otimes(x, y), z))}
           SCCS:
            Scc:
             {*#(+(x, y), z) -> *#(x, z),
              *#(+(x, y), z) -> *#(y, z)}
            Scc:
             {*#(x, *(y, z)) -> *#(otimes(x, y), z)}
            SCC:
             Strict:
              {*#(+(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))}
             SPSC:
              Simple Projection:
               pi(*#) = 0
              Strict:
               {*#(+(x, y), z) -> *#(y, z)}
              EDG:
               {(*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z))}
               SCCS:
                Scc:
                 {*#(+(x, y), z) -> *#(y, z)}
                SCC:
                 Strict:
                  {*#(+(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))}
                 SPSC:
                  Simple Projection:
                   pi(*#) = 0
                  Strict:
                   {}
                  Qed
            SCC:
             Strict:
              {*#(x, *(y, z)) -> *#(otimes(x, 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))}
             SPSC:
              Simple Projection:
               pi(*#) = 1
              Strict:
               {}
              Qed