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