YES
Time: 0.004479
TRS:
 {*(x, +(y, z)) -> +(*(x, y), *(x, z))}
 DP:
  DP:
   {*#(x, +(y, z)) -> *#(x, y),
    *#(x, +(y, z)) -> *#(x, z)}
  TRS:
  {*(x, +(y, z)) -> +(*(x, y), *(x, z))}
  UR:
   {}
   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))}
    STATUS:
     arrows: 0.000000
     SCCS (1):
      Scc:
       {*#(x, +(y, z)) -> *#(x, y),
        *#(x, +(y, z)) -> *#(x, z)}
      
      SCC (2):
       Strict:
        {*#(x, +(y, z)) -> *#(x, y),
         *#(x, +(y, z)) -> *#(x, z)}
       Weak:
       {*(x, +(y, z)) -> +(*(x, y), *(x, z))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [+](x0, x1) = x0 + x1 + 1,
         
         [*](x0, x1) = 0,
         
         [*#](x0, x1) = x0
        Strict:
         *#(x, +(y, z)) -> *#(x, z)
         1 + 0x + 1y + 1z >= 0 + 0x + 1z
         *#(x, +(y, z)) -> *#(x, y)
         1 + 0x + 1y + 1z >= 0 + 0x + 1y
        Weak:
         *(x, +(y, z)) -> +(*(x, y), *(x, z))
         0 + 0x + 0y + 0z >= 1 + 0x + 0y + 0z
       Qed