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