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) = 2x0 + x1,
      
      [times](x0, x1) = x0 + 3x1 + 0,
      
      [s](x0) = 3x0,
      
      [plus](x0, x1) = x0 + 0
     orientation:
      times#(X,s(Y)) = 2X + 3Y >= X + 2Y = times#(Y,X)
      
      plus(plus(X,Y),Z) = X + 0 >= X + 0 = plus(X,plus(Y,Z))
      
      times(X,s(Y)) = X + 6Y + 0 >= X + 0 = 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))
    Subterm Criterion Processor:
     simple projection:
      pi(plus#) = 0
     problem:
      DPs:
       
      TRS:
       plus(plus(X,Y),Z) -> plus(X,plus(Y,Z))
       times(X,s(Y)) -> plus(X,times(Y,X))
     Qed