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