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