YES
Time: 0.002293
TRS:
 {*(x, +(y, z)) -> +(*(x, y), *(x, z)),
      *(x, 1()) -> x,
  *(+(x, y), z) -> +(*(x, z), *(y, z)),
      *(1(), y) -> y}
 DP:
  DP:
   {*#(x, +(y, z)) -> *#(x, y),
    *#(x, +(y, z)) -> *#(x, z),
    *#(+(x, y), z) -> *#(x, z),
    *#(+(x, y), z) -> *#(y, z)}
  TRS:
  {*(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 (1):
    Scc:
     {*#(x, +(y, z)) -> *#(x, y),
      *#(x, +(y, z)) -> *#(x, z),
      *#(+(x, y), z) -> *#(x, z),
      *#(+(x, y), z) -> *#(y, z)}
    SCC (4):
     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(*#) = 1
      Strict:
       {*#(x, +(y, z)) -> *#(x, 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)) -> *#(x, z))
        (*#(+(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, z))
        (*#(x, +(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(x, z))
        (*#(x, +(y, z)) -> *#(x, z), *#(+(x, y), z) -> *#(y, z))}
       SCCS (1):
        Scc:
         {*#(x, +(y, z)) -> *#(x, z),
          *#(+(x, y), z) -> *#(x, z),
          *#(+(x, y), z) -> *#(y, z)}
        SCC (3):
         Strict:
          {*#(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(*#) = 1
          Strict:
           {*#(+(x, y), z) -> *#(x, z),
            *#(+(x, y), z) -> *#(y, z)}
          EDG:
           {(*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, 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) -> *#(y, z))}
           SCCS (1):
            Scc:
             {*#(+(x, y), z) -> *#(x, z),
              *#(+(x, y), z) -> *#(y, z)}
            SCC (2):
             Strict:
              {*#(+(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) -> *#(y, z)}
              EDG:
               {(*#(+(x, y), z) -> *#(y, z), *#(+(x, y), z) -> *#(y, z))}
               SCCS (1):
                Scc:
                 {*#(+(x, y), z) -> *#(y, z)}
                SCC (1):
                 Strict:
                  {*#(+(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:
                   {}
                  Qed