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))
  EDG 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)) -> 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#(Y,Z)
    times#(X,s(Y)) -> plus#(X,times(Y,X)) ->
    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#(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)
    plus#(plus(X,Y),Z) -> plus#(X,plus(Y,Z)) -> plus#(plus(X,Y),Z) -> plus#(X,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))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [times#](x0, x1) = x0 + x1 + 1,
      
      [times](x0, x1) = 0,
      
      [s](x0) = x0 + 1,
      
      [plus](x0, x1) = 0
     orientation:
      times#(X,s(Y)) = X + Y + 2 >= X + Y + 1 = times#(Y,X)
      
      plus(plus(X,Y),Z) = 0 >= 0 = plus(X,plus(Y,Z))
      
      times(X,s(Y)) = 0 >= 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#(X,plus(Y,Z))
     plus#(plus(X,Y),Z) -> 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