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)))}
 DP:
  Strict:
   {    ifplus#(false(), x, y) -> plus#(p(x), y),
        ifplus#(false(), x, y) -> p#(x),
                   plus#(x, y) -> isZero#(x),
                   plus#(x, y) -> ifplus#(isZero(x), x, y),
       iftimes#(false(), x, y) -> plus#(y, times(p(x), y)),
       iftimes#(false(), x, y) -> p#(x),
       iftimes#(false(), x, y) -> times#(p(x), y),
                  times#(x, y) -> isZero#(x),
                  times#(x, y) -> iftimes#(isZero(x), x, y),
    shorter#(cons(x, l), s(y)) -> shorter#(l, y),
            if#(false(), b, l) -> if2#(b, l),
                      prod#(l) -> shorter#(l, 0()),
                      prod#(l) -> shorter#(l, s(0())),
                      prod#(l) -> if#(shorter(l, 0()), shorter(l, s(0())), l),
               if2#(true(), l) -> car#(l),
              if2#(false(), l) -> car#(l),
              if2#(false(), l) -> cddr#(l),
              if2#(false(), l) -> cadr#(l),
              if2#(false(), l) -> times#(car(l), cadr(l)),
              if2#(false(), l) -> prod#(cons(times(car(l), cadr(l)), cddr(l)))}
  Weak:
  {          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)))}
  EDG:
   {(ifplus#(false(), x, y) -> plus#(p(x), y), plus#(x, y) -> ifplus#(isZero(x), x, y))
    (ifplus#(false(), x, y) -> plus#(p(x), y), plus#(x, y) -> isZero#(x))
    (iftimes#(false(), x, y) -> plus#(y, times(p(x), y)), plus#(x, y) -> ifplus#(isZero(x), x, y))
    (iftimes#(false(), x, y) -> plus#(y, times(p(x), y)), plus#(x, y) -> isZero#(x))
    (shorter#(cons(x, l), s(y)) -> shorter#(l, y), shorter#(cons(x, l), s(y)) -> shorter#(l, y))
    (plus#(x, y) -> ifplus#(isZero(x), x, y), ifplus#(false(), x, y) -> p#(x))
    (plus#(x, y) -> ifplus#(isZero(x), x, y), ifplus#(false(), x, y) -> plus#(p(x), y))
    (if2#(false(), l) -> prod#(cons(times(car(l), cadr(l)), cddr(l))), prod#(l) -> if#(shorter(l, 0()), shorter(l, s(0())), l))
    (if2#(false(), l) -> prod#(cons(times(car(l), cadr(l)), cddr(l))), prod#(l) -> shorter#(l, s(0())))
    (if2#(false(), l) -> prod#(cons(times(car(l), cadr(l)), cddr(l))), prod#(l) -> shorter#(l, 0()))
    (times#(x, y) -> iftimes#(isZero(x), x, y), iftimes#(false(), x, y) -> plus#(y, times(p(x), y)))
    (times#(x, y) -> iftimes#(isZero(x), x, y), iftimes#(false(), x, y) -> p#(x))
    (times#(x, y) -> iftimes#(isZero(x), x, y), iftimes#(false(), x, y) -> times#(p(x), y))
    (if#(false(), b, l) -> if2#(b, l), if2#(true(), l) -> car#(l))
    (if#(false(), b, l) -> if2#(b, l), if2#(false(), l) -> car#(l))
    (if#(false(), b, l) -> if2#(b, l), if2#(false(), l) -> cddr#(l))
    (if#(false(), b, l) -> if2#(b, l), if2#(false(), l) -> cadr#(l))
    (if#(false(), b, l) -> if2#(b, l), if2#(false(), l) -> times#(car(l), cadr(l)))
    (if#(false(), b, l) -> if2#(b, l), if2#(false(), l) -> prod#(cons(times(car(l), cadr(l)), cddr(l))))
    (prod#(l) -> shorter#(l, s(0())), shorter#(cons(x, l), s(y)) -> shorter#(l, y))
    (prod#(l) -> if#(shorter(l, 0()), shorter(l, s(0())), l), if#(false(), b, l) -> if2#(b, l))
    (iftimes#(false(), x, y) -> times#(p(x), y), times#(x, y) -> isZero#(x))
    (iftimes#(false(), x, y) -> times#(p(x), y), times#(x, y) -> iftimes#(isZero(x), x, y))
    (if2#(false(), l) -> times#(car(l), cadr(l)), times#(x, y) -> isZero#(x))
    (if2#(false(), l) -> times#(car(l), cadr(l)), times#(x, y) -> iftimes#(isZero(x), x, y))}
   SCCS:
    Scc:
     {if#(false(), b, l) -> if2#(b, l),
                prod#(l) -> if#(shorter(l, 0()), shorter(l, s(0())), l),
        if2#(false(), l) -> prod#(cons(times(car(l), cadr(l)), cddr(l)))}
    Scc:
     {shorter#(cons(x, l), s(y)) -> shorter#(l, y)}
    Scc:
     {iftimes#(false(), x, y) -> times#(p(x), y),
                 times#(x, y) -> iftimes#(isZero(x), x, y)}
    Scc:
     {ifplus#(false(), x, y) -> plus#(p(x), y),
                 plus#(x, y) -> ifplus#(isZero(x), x, y)}
    SCC:
     Strict:
      {if#(false(), b, l) -> if2#(b, l),
                 prod#(l) -> if#(shorter(l, 0()), shorter(l, s(0())), l),
         if2#(false(), l) -> prod#(cons(times(car(l), cadr(l)), cddr(l)))}
     Weak:
     {          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
    SCC:
     Strict:
      {shorter#(cons(x, l), s(y)) -> shorter#(l, y)}
     Weak:
     {          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)))}
     SPSC:
      Simple Projection:
       pi(shorter#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {iftimes#(false(), x, y) -> times#(p(x), y),
                  times#(x, y) -> iftimes#(isZero(x), x, y)}
     Weak:
     {          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
    SCC:
     Strict:
      {ifplus#(false(), x, y) -> plus#(p(x), y),
                  plus#(x, y) -> ifplus#(isZero(x), x, y)}
     Weak:
     {          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