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(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
 plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x))
 plus(zero(),y) -> y
 plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y))))
 id(x) -> x
 if(true(),x,y) -> x
 if(false(),x,y) -> y
 not(x) -> if(x,false(),true())
 gt(s(x),zero()) -> true()
 gt(zero(),y) -> false()
 gt(s(x),s(y)) -> gt(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#(s(x),s(y)) -> id#(y)
   plus#(s(x),s(y)) -> id#(x)
   plus#(s(x),s(y)) -> not#(gt(x,y))
   plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y))
   plus#(s(x),s(y)) -> gt#(x,y)
   plus#(s(x),s(y)) -> if#(gt(x,y),x,y)
   plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))
   plus#(s(x),x) -> id#(x)
   plus#(s(x),x) -> gt#(x,x)
   plus#(s(x),x) -> if#(gt(x,x),id(x),id(x))
   plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x))
   plus#(id(x),s(y)) -> gt#(s(y),y)
   plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y))
   plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y)))
   not#(x) -> if#(x,false(),true())
   gt#(s(x),s(y)) -> gt#(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(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))
   plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x))
   plus(zero(),y) -> y
   plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y))))
   id(x) -> x
   if(true(),x,y) -> x
   if(false(),x,y) -> y
   not(x) -> if(x,false(),true())
   gt(s(x),zero()) -> true()
   gt(zero(),y) -> false()
   gt(s(x),s(y)) -> gt(x,y)
  Open