MAYBE
MAYBE
TRS:
 {
            car(cons(x, l)) -> x,
  cddr(cons(x, cons(y, l))) -> l,
       cddr(cons(x, nil())) -> nil(),
                cddr(nil()) -> nil(),
  cadr(cons(x, cons(y, l))) -> y,
                isZero(0()) -> true(),
               isZero(s(x)) -> false(),
       ifplus(true(), x, y) -> y,
      ifplus(false(), x, y) -> s(plus(p(x), y)),
                 plus(x, y) -> ifplus(isZero(x), x, y),
                     p(0()) -> 0(),
                    p(s(x)) -> x,
      iftimes(true(), x, y) -> 0(),
     iftimes(false(), x, y) -> plus(y, times(p(x), y)),
                times(x, y) -> iftimes(isZero(x), x, y),
   shorter(cons(x, l), 0()) -> false(),
  shorter(cons(x, l), s(y)) -> shorter(l, y),
          shorter(nil(), y) -> true(),
           if(true(), b, l) -> s(0()),
          if(false(), b, l) -> if2(b, l),
                    prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l),
             if2(true(), l) -> car(l),
            if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l)))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
              car(cons(x, l)) -> x,
    cddr(cons(x, cons(y, l))) -> l,
         cddr(cons(x, nil())) -> nil(),
                  cddr(nil()) -> nil(),
    cadr(cons(x, cons(y, l))) -> y,
                  isZero(0()) -> true(),
                 isZero(s(x)) -> false(),
         ifplus(true(), x, y) -> y,
        ifplus(false(), x, y) -> s(plus(p(x), y)),
                   plus(x, y) -> ifplus(isZero(x), x, y),
                       p(0()) -> 0(),
                      p(s(x)) -> x,
        iftimes(true(), x, y) -> 0(),
       iftimes(false(), x, y) -> plus(y, times(p(x), y)),
                  times(x, y) -> iftimes(isZero(x), x, y),
     shorter(cons(x, l), 0()) -> false(),
    shorter(cons(x, l), s(y)) -> shorter(l, y),
            shorter(nil(), y) -> true(),
             if(true(), b, l) -> s(0()),
            if(false(), b, l) -> if2(b, l),
                      prod(l) -> if(shorter(l, 0()), shorter(l, s(0())), l),
               if2(true(), l) -> car(l),
              if2(false(), l) -> prod(cons(times(car(l), cadr(l)), cddr(l)))
   }
  Fail