MAYBE
Trs:
 {     ifplus(true(), x, y) -> y,
      ifplus(false(), x, y) -> s(plus(p(x), y)),
                isZero(0()) -> true(),
               isZero(s(x)) -> false(),
      iftimes(true(), x, y) -> 0(),
     iftimes(false(), x, y) -> plus(y, times(p(x), y)),
                 plus(x, y) -> ifplus(isZero(x), x, y),
                     p(0()) -> 0(),
                    p(s(x)) -> x,
          shorter(nil(), y) -> true(),
   shorter(cons(x, l), 0()) -> false(),
  shorter(cons(x, l), s(y)) -> shorter(l, y),
           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))),
                cddr(nil()) -> nil(),
       cddr(cons(x, nil())) -> nil(),
  cddr(cons(x, cons(y, l))) -> l,
  cadr(cons(x, cons(y, l))) -> y,
            car(cons(x, l)) -> x,
                times(x, y) -> iftimes(isZero(x), x, y),
                    prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l)}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open