YES

Problem:
 times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
 times(x,0()) -> 0()
 times(x,s(y)) -> plus(times(x,y),x)
 plus(x,0()) -> x
 plus(x,s(y)) -> s(plus(x,y))

Proof:
 DP Processor:
  DPs:
   times#(x,plus(y,s(z))) -> times#(x,s(z))
   times#(x,plus(y,s(z))) -> times#(s(z),0())
   times#(x,plus(y,s(z))) -> plus#(y,times(s(z),0()))
   times#(x,plus(y,s(z))) -> times#(x,plus(y,times(s(z),0())))
   times#(x,plus(y,s(z))) -> plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
   times#(x,s(y)) -> times#(x,y)
   times#(x,s(y)) -> plus#(times(x,y),x)
   plus#(x,s(y)) -> plus#(x,y)
  TRS:
   times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
   times(x,0()) -> 0()
   times(x,s(y)) -> plus(times(x,y),x)
   plus(x,0()) -> x
   plus(x,s(y)) -> s(plus(x,y))
  EDG Processor:
   DPs:
    times#(x,plus(y,s(z))) -> times#(x,s(z))
    times#(x,plus(y,s(z))) -> times#(s(z),0())
    times#(x,plus(y,s(z))) -> plus#(y,times(s(z),0()))
    times#(x,plus(y,s(z))) -> times#(x,plus(y,times(s(z),0())))
    times#(x,plus(y,s(z))) -> plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
    times#(x,s(y)) -> times#(x,y)
    times#(x,s(y)) -> plus#(times(x,y),x)
    plus#(x,s(y)) -> plus#(x,y)
   TRS:
    times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
    times(x,0()) -> 0()
    times(x,s(y)) -> plus(times(x,y),x)
    plus(x,0()) -> x
    plus(x,s(y)) -> s(plus(x,y))
   graph:
    plus#(x,s(y)) -> plus#(x,y) ->
    plus#(x,s(y)) -> plus#(x,y)
    times#(x,plus(y,s(z))) -> plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z))) ->
    plus#(x,s(y)) -> plus#(x,y)
    times#(x,plus(y,s(z))) -> plus#(y,times(s(z),0())) ->
    plus#(x,s(y)) -> plus#(x,y)
    times#(x,plus(y,s(z))) -> times#(x,plus(y,times(s(z),0()))) ->
    times#(x,plus(y,s(z))) -> times#(x,s(z))
    times#(x,plus(y,s(z))) -> times#(x,plus(y,times(s(z),0()))) ->
    times#(x,plus(y,s(z))) -> times#(s(z),0())
    times#(x,plus(y,s(z))) -> times#(x,plus(y,times(s(z),0()))) ->
    times#(x,plus(y,s(z))) -> plus#(y,times(s(z),0()))
    times#(x,plus(y,s(z))) -> times#(x,plus(y,times(s(z),0()))) ->
    times#(x,plus(y,s(z))) -> times#(x,plus(y,times(s(z),0())))
    times#(x,plus(y,s(z))) -> times#(x,plus(y,times(s(z),0()))) ->
    times#(x,plus(y,s(z))) -> plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
    times#(x,plus(y,s(z))) -> times#(x,plus(y,times(s(z),0()))) ->
    times#(x,s(y)) -> times#(x,y)
    times#(x,plus(y,s(z))) -> times#(x,plus(y,times(s(z),0()))) ->
    times#(x,s(y)) -> plus#(times(x,y),x)
    times#(x,plus(y,s(z))) -> times#(x,s(z)) ->
    times#(x,s(y)) -> times#(x,y)
    times#(x,plus(y,s(z))) -> times#(x,s(z)) ->
    times#(x,s(y)) -> plus#(times(x,y),x)
    times#(x,s(y)) -> plus#(times(x,y),x) ->
    plus#(x,s(y)) -> plus#(x,y)
    times#(x,s(y)) -> times#(x,y) ->
    times#(x,plus(y,s(z))) -> times#(x,s(z))
    times#(x,s(y)) -> times#(x,y) ->
    times#(x,plus(y,s(z))) -> times#(s(z),0())
    times#(x,s(y)) -> times#(x,y) ->
    times#(x,plus(y,s(z))) -> plus#(y,times(s(z),0()))
    times#(x,s(y)) -> times#(x,y) ->
    times#(x,plus(y,s(z))) -> times#(x,plus(y,times(s(z),0())))
    times#(x,s(y)) -> times#(x,y) ->
    times#(x,plus(y,s(z))) -> plus#(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
    times#(x,s(y)) -> times#(x,y) -> times#(x,s(y)) -> times#(x,y)
    times#(x,s(y)) -> times#(x,y) -> times#(x,s(y)) -> plus#(times(x,y),x)
   SCC Processor:
    #sccs: 2
    #rules: 4
    #arcs: 20/64
    DPs:
     times#(x,plus(y,s(z))) -> times#(x,plus(y,times(s(z),0())))
     times#(x,s(y)) -> times#(x,y)
     times#(x,plus(y,s(z))) -> times#(x,s(z))
    TRS:
     times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
     times(x,0()) -> 0()
     times(x,s(y)) -> plus(times(x,y),x)
     plus(x,0()) -> x
     plus(x,s(y)) -> s(plus(x,y))
    Usable Rule Processor:
     DPs:
      times#(x,plus(y,s(z))) -> times#(x,plus(y,times(s(z),0())))
      times#(x,s(y)) -> times#(x,y)
      times#(x,plus(y,s(z))) -> times#(x,s(z))
     TRS:
      times(x,0()) -> 0()
      plus(x,0()) -> x
      plus(x,s(y)) -> s(plus(x,y))
     Bounds Processor:
      bound: 1
      enrichment: match-dp
      automaton:
       final states: {7}
       transitions:
        00() -> 2,9,1
        times{#,1}(3,29) -> 5,6
        times{#,1}(5,29) -> 5,6
        times{#,1}(2,29) -> 5,6
        times{#,1}(4,27) -> 5*
        times{#,1}(4,29) -> 5,6
        times{#,1}(6,27) -> 7*
        times{#,1}(1,27) -> 5*
        times{#,1}(6,29) -> 7*
        times{#,1}(1,29) -> 5,6
        plus1(2,28) -> 29*
        plus1(4,28) -> 29*
        plus1(1,28) -> 29*
        plus1(3,28) -> 29*
        plus1(5,28) -> 29*
        times1(27,26) -> 28*
        s1(5) -> 27*
        s1(2) -> 27*
        s1(4) -> 27*
        s1(1) -> 27*
        s1(3) -> 27*
        01() -> 28,26
        times{#,0}(3,1) -> 5*
        times{#,0}(3,3) -> 5*
        times{#,0}(3,5) -> 5*
        times{#,0}(4,2) -> 5*
        times{#,0}(4,4) -> 5*
        times{#,0}(5,1) -> 5*
        times{#,0}(5,3) -> 5*
        times{#,0}(5,5) -> 5*
        times{#,0}(1,2) -> 5*
        times{#,0}(1,4) -> 5*
        times{#,0}(6,10) -> 7*
        times{#,0}(2,1) -> 5*
        times{#,0}(2,3) -> 5*
        times{#,0}(2,5) -> 5*
        times{#,0}(3,2) -> 5*
        times{#,0}(3,4) -> 5*
        times{#,0}(4,1) -> 5*
        times{#,0}(4,3) -> 5*
        times{#,0}(4,5) -> 5*
        times{#,0}(5,2) -> 5*
        times{#,0}(5,4) -> 5*
        times{#,0}(1,1) -> 5*
        times{#,0}(1,3) -> 5*
        times{#,0}(1,5) -> 5*
        times{#,0}(2,2) -> 5*
        times{#,0}(2,4) -> 5*
        plus0(3,1) -> 4*
        plus0(3,3) -> 4*
        plus0(3,5) -> 4*
        plus0(4,2) -> 4*
        plus0(4,4) -> 4*
        plus0(5,1) -> 4*
        plus0(5,3) -> 4*
        plus0(5,5) -> 4*
        plus0(1,2) -> 4*
        plus0(1,4) -> 4*
        plus0(2,1) -> 4*
        plus0(2,3) -> 4*
        plus0(2,5) -> 4*
        plus0(3,2) -> 4*
        plus0(3,4) -> 4*
        plus0(4,1) -> 4*
        plus0(4,3) -> 4*
        plus0(4,5) -> 4*
        plus0(5,2) -> 4*
        plus0(5,4) -> 4*
        plus0(1,1) -> 4*
        plus0(1,3) -> 4*
        plus0(1,5) -> 4*
        plus0(6,9) -> 10*
        plus0(2,2) -> 4*
        plus0(2,4) -> 4*
        s0(5) -> 3*
        s0(2) -> 3*
        s0(4) -> 3*
        s0(6) -> 8*
        s0(1) -> 3*
        s0(3) -> 3*
        times0(8,1) -> 9*
        times0(3,1) -> 2*
        times0(3,3) -> 2*
        times0(3,5) -> 2*
        times0(4,2) -> 2*
        times0(4,4) -> 2*
        times0(5,1) -> 2*
        times0(5,3) -> 2*
        times0(5,5) -> 2*
        times0(1,2) -> 2*
        times0(1,4) -> 2*
        times0(2,1) -> 2*
        times0(2,3) -> 2*
        times0(2,5) -> 2*
        times0(3,2) -> 2*
        times0(3,4) -> 2*
        times0(4,1) -> 2*
        times0(4,3) -> 2*
        times0(4,5) -> 2*
        times0(5,2) -> 2*
        times0(5,4) -> 2*
        times0(1,1) -> 2*
        times0(1,3) -> 2*
        times0(1,5) -> 2*
        times0(2,2) -> 2*
        times0(2,4) -> 2*
        1 -> 29,4,6
        2 -> 4,6
        3 -> 29,4,6
        4 -> 29,6
        5 -> 29,4,6
        6 -> 10*
      problem:
       DPs:
        times#(x,s(y)) -> times#(x,y)
        times#(x,plus(y,s(z))) -> times#(x,s(z))
       TRS:
        times(x,0()) -> 0()
        plus(x,0()) -> x
        plus(x,s(y)) -> s(plus(x,y))
      Restore Modifier:
       DPs:
        times#(x,s(y)) -> times#(x,y)
        times#(x,plus(y,s(z))) -> times#(x,s(z))
       TRS:
        times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
        times(x,0()) -> 0()
        times(x,s(y)) -> plus(times(x,y),x)
        plus(x,0()) -> x
        plus(x,s(y)) -> s(plus(x,y))
       Subterm Criterion Processor:
        simple projection:
         pi(times#) = 1
        problem:
         DPs:
          
         TRS:
          times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
          times(x,0()) -> 0()
          times(x,s(y)) -> plus(times(x,y),x)
          plus(x,0()) -> x
          plus(x,s(y)) -> s(plus(x,y))
        Qed
    
    DPs:
     plus#(x,s(y)) -> plus#(x,y)
    TRS:
     times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
     times(x,0()) -> 0()
     times(x,s(y)) -> plus(times(x,y),x)
     plus(x,0()) -> x
     plus(x,s(y)) -> s(plus(x,y))
    Subterm Criterion Processor:
     simple projection:
      pi(plus#) = 1
     problem:
      DPs:
       
      TRS:
       times(x,plus(y,s(z))) -> plus(times(x,plus(y,times(s(z),0()))),times(x,s(z)))
       times(x,0()) -> 0()
       times(x,s(y)) -> plus(times(x,y),x)
       plus(x,0()) -> x
       plus(x,s(y)) -> s(plus(x,y))
     Qed