MAYBE
Time: 0.006226
TRS:
 {           sum nil() -> 0(),
     sum cons(0(), xs) -> sum xs,
     sum cons(s x, xs) -> s sum cons(x, xs),
        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)}
 DP:
  DP:
   {   sum# cons(0(), xs) -> sum# xs,
       sum# cons(s x, xs) -> sum# cons(x, xs),
          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)}
  TRS:
  {           sum nil() -> 0(),
      sum cons(0(), xs) -> sum xs,
      sum cons(s x, xs) -> s sum cons(x, xs),
         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)}
  EDG:
   {(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))
    (sum# cons(s x, xs) -> sum# cons(x, xs), sum# cons(s x, xs) -> sum# cons(x, xs))
    (sum# cons(s x, xs) -> sum# cons(x, xs), sum# cons(0(), xs) -> sum# xs)
    (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))
    (sum# cons(0(), xs) -> sum# xs, sum# cons(0(), xs) -> sum# xs)
    (sum# cons(0(), xs) -> sum# xs, sum# cons(s x, xs) -> sum# cons(x, xs))
    (times#(x, y) -> sum# generate(x, y), sum# cons(0(), xs) -> sum# xs)
    (times#(x, y) -> sum# generate(x, y), sum# cons(s x, xs) -> sum# cons(x, xs))
    (gen#(x, y, z) -> ge#(z, x), ge#(s x, s y) -> ge#(x, y))
    (times#(x, y) -> generate#(x, y), generate#(x, y) -> gen#(x, y, 0()))
    (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))}
   EDG:
    {(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))
     (sum# cons(s x, xs) -> sum# cons(x, xs), sum# cons(s x, xs) -> sum# cons(x, xs))
     (sum# cons(s x, xs) -> sum# cons(x, xs), sum# cons(0(), xs) -> sum# xs)
     (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))
     (sum# cons(0(), xs) -> sum# xs, sum# cons(0(), xs) -> sum# xs)
     (sum# cons(0(), xs) -> sum# xs, sum# cons(s x, xs) -> sum# cons(x, xs))
     (times#(x, y) -> sum# generate(x, y), sum# cons(0(), xs) -> sum# xs)
     (times#(x, y) -> sum# generate(x, y), sum# cons(s x, xs) -> sum# cons(x, xs))
     (gen#(x, y, z) -> ge#(z, x), ge#(s x, s y) -> ge#(x, y))
     (times#(x, y) -> generate#(x, y), generate#(x, y) -> gen#(x, y, 0()))
     (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))}
    EDG:
     {(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))
      (sum# cons(s x, xs) -> sum# cons(x, xs), sum# cons(s x, xs) -> sum# cons(x, xs))
      (sum# cons(s x, xs) -> sum# cons(x, xs), sum# cons(0(), xs) -> sum# xs)
      (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))
      (sum# cons(0(), xs) -> sum# xs, sum# cons(0(), xs) -> sum# xs)
      (sum# cons(0(), xs) -> sum# xs, sum# cons(s x, xs) -> sum# cons(x, xs))
      (times#(x, y) -> sum# generate(x, y), sum# cons(0(), xs) -> sum# xs)
      (times#(x, y) -> sum# generate(x, y), sum# cons(s x, xs) -> sum# cons(x, xs))
      (gen#(x, y, z) -> ge#(z, x), ge#(s x, s y) -> ge#(x, y))
      (times#(x, y) -> generate#(x, y), generate#(x, y) -> gen#(x, y, 0()))
      (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))}
     STATUS:
      arrows: 0.827160
      SCCS (3):
       Scc:
        {sum# cons(0(), xs) -> sum# xs,
         sum# cons(s x, xs) -> sum# cons(x, xs)}
       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 (2):
        Strict:
         {sum# cons(0(), xs) -> sum# xs,
          sum# cons(s x, xs) -> sum# cons(x, xs)}
        Weak:
        {           sum nil() -> 0(),
            sum cons(0(), xs) -> sum xs,
            sum cons(s x, xs) -> s sum cons(x, xs),
               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)}
        Open
       
       
       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 nil() -> 0(),
            sum cons(0(), xs) -> sum xs,
            sum cons(s x, xs) -> s sum cons(x, xs),
               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)}
        Open
       
       SCC (1):
        Strict:
         {ge#(s x, s y) -> ge#(x, y)}
        Weak:
        {           sum nil() -> 0(),
            sum cons(0(), xs) -> sum xs,
            sum cons(s x, xs) -> s sum cons(x, xs),
               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)}
        Open