MAYBE

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))
  Open