MAYBE

Problem:
 car(cons(x,l)) -> x
 cddr(nil()) -> nil()
 cddr(cons(x,nil())) -> nil()
 cddr(cons(x,cons(y,l))) -> l
 cadr(cons(x,cons(y,l))) -> y
 isZero(0()) -> true()
 isZero(s(x)) -> false()
 plus(x,y) -> ifplus(isZero(x),x,y)
 ifplus(true(),x,y) -> y
 ifplus(false(),x,y) -> s(plus(p(x),y))
 times(x,y) -> iftimes(isZero(x),x,y)
 iftimes(true(),x,y) -> 0()
 iftimes(false(),x,y) -> plus(y,times(p(x),y))
 p(s(x)) -> x
 p(0()) -> 0()
 shorter(nil(),y) -> true()
 shorter(cons(x,l),0()) -> false()
 shorter(cons(x,l),s(y)) -> shorter(l,y)
 prod(l) -> if(shorter(l,0()),shorter(l,s(0())),l)
 if(true(),b,l) -> s(0())
 if(false(),b,l) -> if2(b,l)
 if2(true(),l) -> car(l)
 if2(false(),l) -> prod(cons(times(car(l),cadr(l)),cddr(l)))

Proof:
 DP Processor:
  DPs:
   plus#(x,y) -> isZero#(x)
   plus#(x,y) -> ifplus#(isZero(x),x,y)
   ifplus#(false(),x,y) -> p#(x)
   ifplus#(false(),x,y) -> plus#(p(x),y)
   times#(x,y) -> isZero#(x)
   times#(x,y) -> iftimes#(isZero(x),x,y)
   iftimes#(false(),x,y) -> p#(x)
   iftimes#(false(),x,y) -> times#(p(x),y)
   iftimes#(false(),x,y) -> plus#(y,times(p(x),y))
   shorter#(cons(x,l),s(y)) -> shorter#(l,y)
   prod#(l) -> shorter#(l,s(0()))
   prod#(l) -> shorter#(l,0())
   prod#(l) -> if#(shorter(l,0()),shorter(l,s(0())),l)
   if#(false(),b,l) -> if2#(b,l)
   if2#(true(),l) -> car#(l)
   if2#(false(),l) -> cddr#(l)
   if2#(false(),l) -> cadr#(l)
   if2#(false(),l) -> car#(l)
   if2#(false(),l) -> times#(car(l),cadr(l))
   if2#(false(),l) -> prod#(cons(times(car(l),cadr(l)),cddr(l)))
  TRS:
   car(cons(x,l)) -> x
   cddr(nil()) -> nil()
   cddr(cons(x,nil())) -> nil()
   cddr(cons(x,cons(y,l))) -> l
   cadr(cons(x,cons(y,l))) -> y
   isZero(0()) -> true()
   isZero(s(x)) -> false()
   plus(x,y) -> ifplus(isZero(x),x,y)
   ifplus(true(),x,y) -> y
   ifplus(false(),x,y) -> s(plus(p(x),y))
   times(x,y) -> iftimes(isZero(x),x,y)
   iftimes(true(),x,y) -> 0()
   iftimes(false(),x,y) -> plus(y,times(p(x),y))
   p(s(x)) -> x
   p(0()) -> 0()
   shorter(nil(),y) -> true()
   shorter(cons(x,l),0()) -> false()
   shorter(cons(x,l),s(y)) -> shorter(l,y)
   prod(l) -> if(shorter(l,0()),shorter(l,s(0())),l)
   if(true(),b,l) -> s(0())
   if(false(),b,l) -> if2(b,l)
   if2(true(),l) -> car(l)
   if2(false(),l) -> prod(cons(times(car(l),cadr(l)),cddr(l)))
  Usable Rule Processor:
   DPs:
    plus#(x,y) -> isZero#(x)
    plus#(x,y) -> ifplus#(isZero(x),x,y)
    ifplus#(false(),x,y) -> p#(x)
    ifplus#(false(),x,y) -> plus#(p(x),y)
    times#(x,y) -> isZero#(x)
    times#(x,y) -> iftimes#(isZero(x),x,y)
    iftimes#(false(),x,y) -> p#(x)
    iftimes#(false(),x,y) -> times#(p(x),y)
    iftimes#(false(),x,y) -> plus#(y,times(p(x),y))
    shorter#(cons(x,l),s(y)) -> shorter#(l,y)
    prod#(l) -> shorter#(l,s(0()))
    prod#(l) -> shorter#(l,0())
    prod#(l) -> if#(shorter(l,0()),shorter(l,s(0())),l)
    if#(false(),b,l) -> if2#(b,l)
    if2#(true(),l) -> car#(l)
    if2#(false(),l) -> cddr#(l)
    if2#(false(),l) -> cadr#(l)
    if2#(false(),l) -> car#(l)
    if2#(false(),l) -> times#(car(l),cadr(l))
    if2#(false(),l) -> prod#(cons(times(car(l),cadr(l)),cddr(l)))
   TRS:
    isZero(0()) -> true()
    isZero(s(x)) -> false()
    p(s(x)) -> x
    p(0()) -> 0()
    times(x,y) -> iftimes(isZero(x),x,y)
    iftimes(true(),x,y) -> 0()
    iftimes(false(),x,y) -> plus(y,times(p(x),y))
    plus(x,y) -> ifplus(isZero(x),x,y)
    ifplus(true(),x,y) -> y
    ifplus(false(),x,y) -> s(plus(p(x),y))
    shorter(nil(),y) -> true()
    shorter(cons(x,l),s(y)) -> shorter(l,y)
    shorter(cons(x,l),0()) -> false()
    cadr(cons(x,cons(y,l))) -> y
    car(cons(x,l)) -> x
    cddr(nil()) -> nil()
    cddr(cons(x,nil())) -> nil()
    cddr(cons(x,cons(y,l))) -> l
   Open