YES

Problem:
 plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
 times(X,s(Y)) -> plus(X,times(Y,X))

Proof:
 DP Processor:
  DPs:
   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)) -> plus#(X,times(Y,X))
  TRS:
   plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
   times(X,s(Y)) -> plus(X,times(Y,X))
  TDG Processor:
   DPs:
    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)) -> plus#(X,times(Y,X))
   TRS:
    plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
    times(X,s(Y)) -> plus(X,times(Y,X))
   graph:
    times#(X,s(Y)) -> times#(Y,X) ->
    times#(X,s(Y)) -> plus#(X,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)) ->
    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#(Y,Z) ->
    plus#(plus(X,Y),Z) -> plus#(X,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)) ->
    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)
   SCC Processor:
    #sccs: 2
    #rules: 3
    #arcs: 8/16
    DPs:
     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))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [times#](x0, x1) = 4x0 + 1x1,
      
      [times](x0, x1) = 3x0 + 1x1 + 0,
      
      [s](x0) = 4x0 + -1,
      
      [plus](x0, x1) = 2x0 + -2
     orientation:
      times#(X,s(Y)) = 4X + 5Y + 0 >= 1X + 4Y = times#(Y,X)
      
      plus(plus(X,Y),Z) = 4X + 0 >= 2X + -2 = plus(X,plus(Y,Z))
      
      times(X,s(Y)) = 3X + 5Y + 0 >= 2X + -2 = plus(X,times(Y,X))
     problem:
      DPs:
       
      TRS:
       plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
       times(X,s(Y)) -> plus(X,times(Y,X))
     Qed
    
    DPs:
     plus#(plus(X,Y),Z) -> plus#(Y,Z)
     plus#(plus(X,Y),Z) -> plus#(X,plus(Y,Z))
    TRS:
     plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
     times(X,s(Y)) -> plus(X,times(Y,X))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [plus#](x0, x1) = x0,
      
      [times](x0, x1) = 6x0 + 2x1 + 4,
      
      [s](x0) = 3x0 + 6,
      
      [plus](x0, x1) = 4x0 + x1 + 5
     orientation:
      plus#(plus(X,Y),Z) = 4X + Y + 5 >= Y = plus#(Y,Z)
      
      plus#(plus(X,Y),Z) = 4X + Y + 5 >= X = plus#(X,plus(Y,Z))
      
      plus(plus(X,Y),Z) = 16X + 4Y + Z + 25 >= 4X + 4Y + Z + 10 = plus(X,plus(Y,Z))
      
      times(X,s(Y)) = 6X + 6Y + 16 >= 6X + 6Y + 9 = plus(X,times(Y,X))
     problem:
      DPs:
       
      TRS:
       plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
       times(X,s(Y)) -> plus(X,times(Y,X))
     Qed