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