MAYBE
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:
  Strict:
   {                 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))}
  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()}
  EDG:
   {(times#(x, y) -> generate#(x, y), generate#(x, y) -> gen#(x, y, 0()))
    (sum2#(xs, y) -> isZero#(head(xs)), isZero#(s(s(x))) -> isZero#(s(x)))
    (generate#(x, y) -> gen#(x, y, 0()), gen#(x, y, z) -> ge#(z, x))
    (generate#(x, y) -> gen#(x, y, 0()), gen#(x, y, z) -> if#(ge(z, x), x, y, z))
    (isZero#(s(s(x))) -> isZero#(s(x)), isZero#(s(s(x))) -> isZero#(s(x)))
    (ifsum2#(false(), xs, y) -> sum2#(cons(p(head(xs)), tail(xs)), s(y)), sum2#(xs, y) -> head#(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) -> isNil#(xs))
    (ifsum2#(false(), xs, y) -> sum2#(cons(p(head(xs)), tail(xs)), s(y)), sum2#(xs, y) -> ifsum#(isNil(xs), isZero(head(xs)), xs, y))
    (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))
    (ifsum2#(true(), xs, y) -> sum2#(tail(xs), y), sum2#(xs, y) -> head#(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) -> isNil#(xs))
    (ifsum2#(true(), xs, y) -> sum2#(tail(xs), y), sum2#(xs, y) -> ifsum#(isNil(xs), isZero(head(xs)), xs, y))
    (gen#(x, y, z) -> ge#(z, x), ge#(s(x), s(y)) -> ge#(x, y))
    (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))
    (sum2#(xs, y) -> ifsum#(isNil(xs), isZero(head(xs)), xs, y), ifsum#(false(), b, xs, y) -> ifsum2#(b, xs, y))
    (gen#(x, y, z) -> if#(ge(z, x), x, y, z), if#(false(), x, y, z) -> gen#(x, y, s(z)))
    (p#(s(s(x))) -> p#(s(x)), p#(s(s(x))) -> p#(s(x)))
    (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)))
    (ifsum2#(false(), xs, y) -> p#(head(xs)), p#(s(s(x))) -> p#(s(x)))
    (ge#(s(x), s(y)) -> ge#(x, y), ge#(s(x), s(y)) -> ge#(x, y))
    (times#(x, y) -> sum#(generate(x, y)), sum#(xs) -> sum2#(xs, 0()))}
   SCCS:
    Scc:
     {p#(s(s(x))) -> p#(s(x))}
    Scc:
     {isZero#(s(s(x))) -> isZero#(s(x))}
    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:
     {ge#(s(x), s(y)) -> ge#(x, y)}
    Scc:
     {        gen#(x, y, z) -> if#(ge(z, x), x, y, z),
      if#(false(), x, y, z) -> gen#(x, y, s(z))}
    SCC:
     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()}
     SPSC:
      Simple Projection:
       pi(p#) = 0
      Strict:
       {}
      Qed
    SCC:
     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()}
     SPSC:
      Simple Projection:
       pi(isZero#) = 0
      Strict:
       {}
      Qed
    SCC:
     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()}
     Fail
    SCC:
     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()}
     SPSC:
      Simple Projection:
       pi(ge#) = 0
      Strict:
       {}
      Qed
    SCC:
     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()}
     Fail