YES
Time: 0.003589
TRS:
 {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
        times(X, s Y) -> plus(X, times(Y, X))}
 DP:
  DP:
   {plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)),
    plus#(plus(X, Y), Z) -> plus#(Y, Z),
          times#(X, s Y) -> plus#(X, times(Y, X)),
          times#(X, s Y) -> times#(Y, X)}
  TRS:
  {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
         times(X, s Y) -> plus(X, times(Y, X))}
  EDG:
   {(plus#(plus(X, Y), Z) -> plus#(Y, Z), plus#(plus(X, Y), Z) -> plus#(Y, Z))
    (plus#(plus(X, Y), Z) -> plus#(Y, Z), plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)))
    (times#(X, s Y) -> times#(Y, X), times#(X, s Y) -> times#(Y, X))
    (times#(X, s Y) -> times#(Y, X), times#(X, s Y) -> plus#(X, times(Y, X)))
    (times#(X, s Y) -> plus#(X, times(Y, X)), plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)))
    (times#(X, s Y) -> plus#(X, times(Y, X)), plus#(plus(X, Y), Z) -> plus#(Y, Z))
    (plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)), plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)))
    (plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)), plus#(plus(X, Y), Z) -> plus#(Y, Z))}
   SCCS (2):
    Scc:
     {times#(X, s Y) -> times#(Y, X)}
    Scc:
     {plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)),
      plus#(plus(X, Y), Z) -> plus#(Y, Z)}
    SCC (1):
     Strict:
      {times#(X, s Y) -> times#(Y, X)}
     Weak:
     {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
            times(X, s Y) -> plus(X, times(Y, X))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [plus](x0, x1) = x0 + x1 + 1,
       
       [times](x0, x1) = 1,
       
       [s](x0) = x0 + 1,
       
       [times#](x0, x1) = x0 + x1
      Strict:
       times#(X, s Y) -> times#(Y, X)
       1 + 1X + 1Y >= 0 + 1X + 1Y
      Weak:
       
     Qed
   SCC (2):
    Strict:
     {plus#(plus(X, Y), Z) -> plus#(X, plus(Y, Z)),
      plus#(plus(X, Y), Z) -> plus#(Y, Z)}
    Weak:
    {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
           times(X, s Y) -> plus(X, times(Y, X))}
    SPSC:
     Simple Projection:
      pi(plus#) = 0
     Strict:
      {plus#(plus(X, Y), Z) -> plus#(Y, Z)}
     EDG:
      {(plus#(plus(X, Y), Z) -> plus#(Y, Z), plus#(plus(X, Y), Z) -> plus#(Y, Z))}
      SCCS (1):
       Scc:
        {plus#(plus(X, Y), Z) -> plus#(Y, Z)}
       SCC (1):
        Strict:
         {plus#(plus(X, Y), Z) -> plus#(Y, Z)}
        Weak:
        {plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)),
               times(X, s Y) -> plus(X, times(Y, X))}
        SPSC:
         Simple Projection:
          pi(plus#) = 0
         Strict:
          {}
         Qed