MAYBE
Time: 0.008129
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:
  DP:
   {   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)}
  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)}
  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)
    (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))
    (prod# l -> shorter#(l, s 0()), shorter#(cons(x, l), s y) -> shorter#(l, y))
    (if#(false(), b, l) -> if2#(b, l), if2#(false(), l) -> prod# cons(times(car l, cadr l), cddr 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) -> cadr# l)
    (if#(false(), b, l) -> if2#(b, l), if2#(false(), l) -> cddr# l)
    (if#(false(), b, l) -> if2#(b, l), if2#(false(), l) -> car# l)
    (if#(false(), b, l) -> if2#(b, l), if2#(true(), l) -> car# l)
    (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()))
    (prod# l -> if#(shorter(l, 0()), shorter(l, s 0()), l), if#(false(), b, l) -> if2#(b, l))
    (shorter#(cons(x, l), s y) -> shorter#(l, y), shorter#(cons(x, l), s y) -> shorter#(l, y))
    (iftimes#(false(), x, y) -> plus#(y, times(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))
    (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))
    (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))}
   STATUS:
    arrows: 0.937500
    SCCS (4):
     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 (3):
      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)}
      Open
     
     SCC (1):
      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)}
      Open
     
     
     
     
     
     
     SCC (2):
      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)}
      Open
     
     
     SCC (2):
      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)}
      Open