MAYBE
Time: 0.006190
TRS:
 {                  sum xs -> sum2(xs, 0()),
            generate(x, y) -> gen(x, y, 0()),
               times(x, y) -> sum generate(x, y),
              gen(x, y, z) -> if(ge(z, x), x, y, z),
       if(true(), x, y, z) -> nil(),
      if(false(), x, y, z) -> cons(y, gen(x, y, s z)),
                ge(x, 0()) -> true(),
              ge(0(), s y) -> false(),
              ge(s x, s y) -> ge(x, y),
               sum2(xs, y) -> ifsum(isNil xs, isZero head xs, xs, y),
   ifsum(true(), b, xs, y) -> y,
  ifsum(false(), b, xs, y) -> ifsum2(b, xs, y),
               isNil nil() -> true(),
         isNil cons(x, xs) -> false(),
                isZero 0() -> true(),
              isZero s 0() -> false(),
              isZero s s x -> isZero s x,
                head nil() -> error(),
          head cons(x, xs) -> x,
     ifsum2(true(), xs, y) -> sum2(tail xs, y),
    ifsum2(false(), xs, y) -> sum2(cons(p head xs, tail xs), s y),
                tail nil() -> nil(),
          tail cons(x, xs) -> xs,
                     p 0() -> s s 0(),
                   p s 0() -> 0(),
                   p s s x -> s p s x,
                       a() -> c(),
                       a() -> d()}
 DP:
  DP:
   {                  sum# xs -> sum2#(xs, 0()),
              generate#(x, y) -> gen#(x, y, 0()),
                 times#(x, y) -> sum# generate(x, y),
                 times#(x, y) -> generate#(x, y),
                gen#(x, y, z) -> if#(ge(z, x), x, y, z),
                gen#(x, y, z) -> ge#(z, x),
        if#(false(), x, y, z) -> gen#(x, y, s z),
                ge#(s x, s y) -> ge#(x, y),
                 sum2#(xs, y) -> ifsum#(isNil xs, isZero head xs, xs, y),
                 sum2#(xs, y) -> isNil# xs,
                 sum2#(xs, y) -> isZero# head xs,
                 sum2#(xs, y) -> head# xs,
    ifsum#(false(), b, xs, y) -> ifsum2#(b, xs, y),
                isZero# s s x -> isZero# s x,
       ifsum2#(true(), xs, y) -> sum2#(tail xs, y),
       ifsum2#(true(), xs, y) -> tail# xs,
      ifsum2#(false(), xs, y) -> sum2#(cons(p head xs, tail xs), s y),
      ifsum2#(false(), xs, y) -> head# xs,
      ifsum2#(false(), xs, y) -> tail# xs,
      ifsum2#(false(), xs, y) -> p# head xs,
                     p# s s x -> p# s x}
  TRS:
  {                  sum xs -> sum2(xs, 0()),
             generate(x, y) -> gen(x, y, 0()),
                times(x, y) -> sum generate(x, y),
               gen(x, y, z) -> if(ge(z, x), x, y, z),
        if(true(), x, y, z) -> nil(),
       if(false(), x, y, z) -> cons(y, gen(x, y, s z)),
                 ge(x, 0()) -> true(),
               ge(0(), s y) -> false(),
               ge(s x, s y) -> ge(x, y),
                sum2(xs, y) -> ifsum(isNil xs, isZero head xs, xs, y),
    ifsum(true(), b, xs, y) -> y,
   ifsum(false(), b, xs, y) -> ifsum2(b, xs, y),
                isNil nil() -> true(),
          isNil cons(x, xs) -> false(),
                 isZero 0() -> true(),
               isZero s 0() -> false(),
               isZero s s x -> isZero s x,
                 head nil() -> error(),
           head cons(x, xs) -> x,
      ifsum2(true(), xs, y) -> sum2(tail xs, y),
     ifsum2(false(), xs, y) -> sum2(cons(p head xs, tail xs), s y),
                 tail nil() -> nil(),
           tail cons(x, xs) -> xs,
                      p 0() -> s s 0(),
                    p s 0() -> 0(),
                    p s s x -> s p s x,
                        a() -> c(),
                        a() -> d()}
  UR:
   {      generate(x, y) -> gen(x, y, 0()),
            gen(x, y, z) -> if(ge(z, x), x, y, z),
     if(true(), x, y, z) -> nil(),
    if(false(), x, y, z) -> cons(y, gen(x, y, s z)),
              ge(x, 0()) -> true(),
            ge(0(), s y) -> false(),
            ge(s x, s y) -> ge(x, y),
             isNil nil() -> true(),
       isNil cons(x, xs) -> false(),
              isZero 0() -> true(),
            isZero s 0() -> false(),
            isZero s s x -> isZero s x,
              head nil() -> error(),
        head cons(x, xs) -> x,
              tail nil() -> nil(),
        tail cons(x, xs) -> xs,
                   p 0() -> s s 0(),
                 p s 0() -> 0(),
                 p s s x -> s p s x,
                 b(w, v) -> w,
                 b(w, v) -> v}
   EDG:
    {(times#(x, y) -> sum# generate(x, y), sum# xs -> sum2#(xs, 0()))
     (gen#(x, y, z) -> ge#(z, x), ge#(s x, s y) -> ge#(x, y))
     (sum2#(xs, y) -> isZero# head xs, isZero# s s x -> isZero# s x)
     (isZero# s s x -> isZero# s x, isZero# s s x -> isZero# s x)
     (times#(x, y) -> generate#(x, y), generate#(x, y) -> gen#(x, y, 0()))
     (if#(false(), x, y, z) -> gen#(x, y, s z), gen#(x, y, z) -> ge#(z, x))
     (if#(false(), x, y, z) -> gen#(x, y, s z), gen#(x, y, z) -> if#(ge(z, x), x, y, z))
     (sum2#(xs, y) -> ifsum#(isNil xs, isZero head xs, xs, y), ifsum#(false(), b, xs, y) -> ifsum2#(b, xs, y))
     (ifsum#(false(), b, xs, y) -> ifsum2#(b, xs, y), ifsum2#(true(), xs, y) -> sum2#(tail xs, y))
     (ifsum#(false(), b, xs, y) -> ifsum2#(b, xs, y), ifsum2#(true(), xs, y) -> tail# xs)
     (ifsum#(false(), b, xs, y) -> ifsum2#(b, xs, y), ifsum2#(false(), xs, y) -> sum2#(cons(p head xs, tail xs), s y))
     (ifsum#(false(), b, xs, y) -> ifsum2#(b, xs, y), ifsum2#(false(), xs, y) -> head# xs)
     (ifsum#(false(), b, xs, y) -> ifsum2#(b, xs, y), ifsum2#(false(), xs, y) -> tail# xs)
     (ifsum#(false(), b, xs, y) -> ifsum2#(b, xs, y), ifsum2#(false(), xs, y) -> p# head xs)
     (gen#(x, y, z) -> if#(ge(z, x), x, y, z), if#(false(), x, y, z) -> gen#(x, y, s z))
     (ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
     (ifsum2#(false(), xs, y) -> sum2#(cons(p head xs, tail xs), s y), sum2#(xs, y) -> ifsum#(isNil xs, isZero head xs, xs, y))
     (ifsum2#(false(), xs, y) -> sum2#(cons(p head xs, tail xs), s y), sum2#(xs, y) -> isNil# xs)
     (ifsum2#(false(), xs, y) -> sum2#(cons(p head xs, tail xs), s y), sum2#(xs, y) -> isZero# head xs)
     (ifsum2#(false(), xs, y) -> sum2#(cons(p head xs, tail xs), s y), sum2#(xs, y) -> head# xs)
     (p# s s x -> p# s x, p# s s x -> p# s x)
     (ifsum2#(false(), xs, y) -> p# head xs, p# s s x -> p# s x)
     (generate#(x, y) -> gen#(x, y, 0()), gen#(x, y, z) -> if#(ge(z, x), x, y, z))
     (generate#(x, y) -> gen#(x, y, 0()), gen#(x, y, z) -> ge#(z, x))
     (ifsum2#(true(), xs, y) -> sum2#(tail xs, y), sum2#(xs, y) -> ifsum#(isNil xs, isZero head xs, xs, y))
     (ifsum2#(true(), xs, y) -> sum2#(tail xs, y), sum2#(xs, y) -> isNil# xs)
     (ifsum2#(true(), xs, y) -> sum2#(tail xs, y), sum2#(xs, y) -> isZero# head xs)
     (ifsum2#(true(), xs, y) -> sum2#(tail xs, y), sum2#(xs, y) -> head# xs)
     (sum# xs -> sum2#(xs, 0()), sum2#(xs, y) -> ifsum#(isNil xs, isZero head xs, xs, y))
     (sum# xs -> sum2#(xs, 0()), sum2#(xs, y) -> isNil# xs)
     (sum# xs -> sum2#(xs, 0()), sum2#(xs, y) -> isZero# head xs)
     (sum# xs -> sum2#(xs, 0()), sum2#(xs, y) -> head# xs)}
    STATUS:
     arrows: 0.927438
     SCCS (5):
      Scc:
       {        gen#(x, y, z) -> if#(ge(z, x), x, y, z),
        if#(false(), x, y, z) -> gen#(x, y, s z)}
      Scc:
       {ge#(s x, s y) -> ge#(x, y)}
      Scc:
       {             sum2#(xs, y) -> ifsum#(isNil xs, isZero head xs, xs, y),
        ifsum#(false(), b, xs, y) -> ifsum2#(b, xs, y),
           ifsum2#(true(), xs, y) -> sum2#(tail xs, y),
          ifsum2#(false(), xs, y) -> sum2#(cons(p head xs, tail xs), s y)}
      Scc:
       {p# s s x -> p# s x}
      Scc:
       {isZero# s s x -> isZero# s x}
      
      
      
      SCC (2):
       Strict:
        {        gen#(x, y, z) -> if#(ge(z, x), x, y, z),
         if#(false(), x, y, z) -> gen#(x, y, s z)}
       Weak:
       {                  sum xs -> sum2(xs, 0()),
                  generate(x, y) -> gen(x, y, 0()),
                     times(x, y) -> sum generate(x, y),
                    gen(x, y, z) -> if(ge(z, x), x, y, z),
             if(true(), x, y, z) -> nil(),
            if(false(), x, y, z) -> cons(y, gen(x, y, s z)),
                      ge(x, 0()) -> true(),
                    ge(0(), s y) -> false(),
                    ge(s x, s y) -> ge(x, y),
                     sum2(xs, y) -> ifsum(isNil xs, isZero head xs, xs, y),
         ifsum(true(), b, xs, y) -> y,
        ifsum(false(), b, xs, y) -> ifsum2(b, xs, y),
                     isNil nil() -> true(),
               isNil cons(x, xs) -> false(),
                      isZero 0() -> true(),
                    isZero s 0() -> false(),
                    isZero s s x -> isZero s x,
                      head nil() -> error(),
                head cons(x, xs) -> x,
           ifsum2(true(), xs, y) -> sum2(tail xs, y),
          ifsum2(false(), xs, y) -> sum2(cons(p head xs, tail xs), s y),
                      tail nil() -> nil(),
                tail cons(x, xs) -> xs,
                           p 0() -> s s 0(),
                         p s 0() -> 0(),
                         p s s x -> s p s x,
                             a() -> c(),
                             a() -> d()}
       Open
      
      SCC (1):
       Strict:
        {ge#(s x, s y) -> ge#(x, y)}
       Weak:
       {                  sum xs -> sum2(xs, 0()),
                  generate(x, y) -> gen(x, y, 0()),
                     times(x, y) -> sum generate(x, y),
                    gen(x, y, z) -> if(ge(z, x), x, y, z),
             if(true(), x, y, z) -> nil(),
            if(false(), x, y, z) -> cons(y, gen(x, y, s z)),
                      ge(x, 0()) -> true(),
                    ge(0(), s y) -> false(),
                    ge(s x, s y) -> ge(x, y),
                     sum2(xs, y) -> ifsum(isNil xs, isZero head xs, xs, y),
         ifsum(true(), b, xs, y) -> y,
        ifsum(false(), b, xs, y) -> ifsum2(b, xs, y),
                     isNil nil() -> true(),
               isNil cons(x, xs) -> false(),
                      isZero 0() -> true(),
                    isZero s 0() -> false(),
                    isZero s s x -> isZero s x,
                      head nil() -> error(),
                head cons(x, xs) -> x,
           ifsum2(true(), xs, y) -> sum2(tail xs, y),
          ifsum2(false(), xs, y) -> sum2(cons(p head xs, tail xs), s y),
                      tail nil() -> nil(),
                tail cons(x, xs) -> xs,
                           p 0() -> s s 0(),
                         p s 0() -> 0(),
                         p s s x -> s p s x,
                             a() -> c(),
                             a() -> d()}
       Open
      
      
      SCC (4):
       Strict:
        {             sum2#(xs, y) -> ifsum#(isNil xs, isZero head xs, xs, y),
         ifsum#(false(), b, xs, y) -> ifsum2#(b, xs, y),
            ifsum2#(true(), xs, y) -> sum2#(tail xs, y),
           ifsum2#(false(), xs, y) -> sum2#(cons(p head xs, tail xs), s y)}
       Weak:
       {                  sum xs -> sum2(xs, 0()),
                  generate(x, y) -> gen(x, y, 0()),
                     times(x, y) -> sum generate(x, y),
                    gen(x, y, z) -> if(ge(z, x), x, y, z),
             if(true(), x, y, z) -> nil(),
            if(false(), x, y, z) -> cons(y, gen(x, y, s z)),
                      ge(x, 0()) -> true(),
                    ge(0(), s y) -> false(),
                    ge(s x, s y) -> ge(x, y),
                     sum2(xs, y) -> ifsum(isNil xs, isZero head xs, xs, y),
         ifsum(true(), b, xs, y) -> y,
        ifsum(false(), b, xs, y) -> ifsum2(b, xs, y),
                     isNil nil() -> true(),
               isNil cons(x, xs) -> false(),
                      isZero 0() -> true(),
                    isZero s 0() -> false(),
                    isZero s s x -> isZero s x,
                      head nil() -> error(),
                head cons(x, xs) -> x,
           ifsum2(true(), xs, y) -> sum2(tail xs, y),
          ifsum2(false(), xs, y) -> sum2(cons(p head xs, tail xs), s y),
                      tail nil() -> nil(),
                tail cons(x, xs) -> xs,
                           p 0() -> s s 0(),
                         p s 0() -> 0(),
                         p s s x -> s p s x,
                             a() -> c(),
                             a() -> d()}
       Open
      
      SCC (1):
       Strict:
        {p# s s x -> p# s x}
       Weak:
       {                  sum xs -> sum2(xs, 0()),
                  generate(x, y) -> gen(x, y, 0()),
                     times(x, y) -> sum generate(x, y),
                    gen(x, y, z) -> if(ge(z, x), x, y, z),
             if(true(), x, y, z) -> nil(),
            if(false(), x, y, z) -> cons(y, gen(x, y, s z)),
                      ge(x, 0()) -> true(),
                    ge(0(), s y) -> false(),
                    ge(s x, s y) -> ge(x, y),
                     sum2(xs, y) -> ifsum(isNil xs, isZero head xs, xs, y),
         ifsum(true(), b, xs, y) -> y,
        ifsum(false(), b, xs, y) -> ifsum2(b, xs, y),
                     isNil nil() -> true(),
               isNil cons(x, xs) -> false(),
                      isZero 0() -> true(),
                    isZero s 0() -> false(),
                    isZero s s x -> isZero s x,
                      head nil() -> error(),
                head cons(x, xs) -> x,
           ifsum2(true(), xs, y) -> sum2(tail xs, y),
          ifsum2(false(), xs, y) -> sum2(cons(p head xs, tail xs), s y),
                      tail nil() -> nil(),
                tail cons(x, xs) -> xs,
                           p 0() -> s s 0(),
                         p s 0() -> 0(),
                         p s s x -> s p s x,
                             a() -> c(),
                             a() -> d()}
       Open
      
      
      
      
      
      SCC (1):
       Strict:
        {isZero# s s x -> isZero# s x}
       Weak:
       {                  sum xs -> sum2(xs, 0()),
                  generate(x, y) -> gen(x, y, 0()),
                     times(x, y) -> sum generate(x, y),
                    gen(x, y, z) -> if(ge(z, x), x, y, z),
             if(true(), x, y, z) -> nil(),
            if(false(), x, y, z) -> cons(y, gen(x, y, s z)),
                      ge(x, 0()) -> true(),
                    ge(0(), s y) -> false(),
                    ge(s x, s y) -> ge(x, y),
                     sum2(xs, y) -> ifsum(isNil xs, isZero head xs, xs, y),
         ifsum(true(), b, xs, y) -> y,
        ifsum(false(), b, xs, y) -> ifsum2(b, xs, y),
                     isNil nil() -> true(),
               isNil cons(x, xs) -> false(),
                      isZero 0() -> true(),
                    isZero s 0() -> false(),
                    isZero s s x -> isZero s x,
                      head nil() -> error(),
                head cons(x, xs) -> x,
           ifsum2(true(), xs, y) -> sum2(tail xs, y),
          ifsum2(false(), xs, y) -> sum2(cons(p head xs, tail xs), s y),
                      tail nil() -> nil(),
                tail cons(x, xs) -> xs,
                           p 0() -> s s 0(),
                         p s 0() -> 0(),
                         p s s x -> s p s x,
                             a() -> c(),
                             a() -> d()}
       Open