Input TRS:
    1: times(x,y) -> sum(generate(x,y))
    2: generate(x,y) -> gen(x,y,0())
    3: gen(x,y,z) -> if(ge(z,x),x,y,z)
    4: if(true(),x,y,z) -> nil()
    5: if(false(),x,y,z) -> cons(y,gen(x,y,s(z)))
    6: sum(xs) -> sum2(xs,0())
    7: sum2(xs,y) -> ifsum(isNil(xs),isZero(head(xs)),xs,y)
    8: ifsum(true(),b,xs,y) -> y
    9: ifsum(false(),b,xs,y) -> ifsum2(b,xs,y)
    10: ifsum2(true(),xs,y) -> sum2(tail(xs),y)
    11: ifsum2(false(),xs,y) -> sum2(cons(p(head(xs)),tail(xs)),s(y))
    12: isNil(nil()) -> true()
    13: isNil(cons(x,xs)) -> false()
    14: tail(nil()) -> nil()
    15: tail(cons(x,xs)) -> xs
    16: head(cons(x,xs)) -> x
    17: head(nil()) -> error()
    18: isZero(0()) -> true()
    19: isZero(s(0())) -> false()
    20: isZero(s(s(x))) -> isZero(s(x))
    21: p(0()) -> s(s(0()))
    22: p(s(0())) -> 0()
    23: p(s(s(x))) -> s(p(s(x)))
    24: ge(x,0()) -> true()
    25: ge(0(),s(y)) -> false()
    26: ge(s(x),s(y)) -> ge(x,y)
    27: a() -> c()
    28: a() -> d()
Number of strict rules: 28
Direct Order(PosReal,>,Poly) ... failed.
Freezing isZero p
1: times(x,y) -> sum(generate(x,y))
2: generate(x,y) -> gen(x,y,0())
3: gen(x,y,z) -> if(ge(z,x),x,y,z)
4: if(true(),x,y,z) -> nil()
5: if(false(),x,y,z) -> cons(y,gen(x,y,s(z)))
6: sum(xs) -> sum2(xs,0())
7: sum2(xs,y) -> ifsum(isNil(xs),isZero(head(xs)),xs,y)
8: ifsum(true(),b,xs,y) -> y
9: ifsum(false(),b,xs,y) -> ifsum2(b,xs,y)
10: ifsum2(true(),xs,y) -> sum2(tail(xs),y)
11: ifsum2(false(),xs,y) -> sum2(cons(p(head(xs)),tail(xs)),s(y))
12: isNil(nil()) -> true()
13: isNil(cons(x,xs)) -> false()
14: tail(nil()) -> nil()
15: tail(cons(x,xs)) -> xs
16: head(cons(x,xs)) -> x
17: head(nil()) -> error()
18: isZero❆1_0() -> true()
19: isZero❆1_s(0()) -> false()
20: isZero❆1_s(s(x)) -> isZero❆1_s(x)
21: p❆1_0() -> s(s(0()))
22: p❆1_s(0()) -> 0()
23: p❆1_s(s(x)) -> s(p❆1_s(x))
24: ge(x,0()) -> true()
25: ge(0(),s(y)) -> false()
26: ge(s(x),s(y)) -> ge(x,y)
27: a() -> c()
28: a() -> d()
29: p(0()) ->= p❆1_0()
30: p(s(_1)) ->= p❆1_s(_1)
31: isZero(0()) ->= isZero❆1_0()
32: isZero(s(_1)) ->= isZero❆1_s(_1)
Number of strict rules: 28
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #generate(x,y) -> #gen(x,y,0())
   #2: #p(0()) ->? #p❆1_0()
   #3: #sum(xs) -> #sum2(xs,0())
   #4: #ifsum(false(),b,xs,y) -> #ifsum2(b,xs,y)
   #5: #ifsum2(false(),xs,y) -> #sum2(cons(p(head(xs)),tail(xs)),s(y))
   #6: #ifsum2(false(),xs,y) -> #p(head(xs))
   #7: #ifsum2(false(),xs,y) -> #head(xs)
   #8: #ifsum2(false(),xs,y) -> #tail(xs)
   #9: #p❆1_s(s(x)) -> #p❆1_s(x)
   #10: #isZero(0()) ->? #isZero❆1_0()
   #11: #p(s(_1)) ->? #p❆1_s(_1)
   #12: #isZero❆1_s(s(x)) -> #isZero❆1_s(x)
   #13: #sum2(xs,y) -> #ifsum(isNil(xs),isZero(head(xs)),xs,y)
   #14: #sum2(xs,y) -> #isNil(xs)
   #15: #sum2(xs,y) -> #isZero(head(xs))
   #16: #sum2(xs,y) -> #head(xs)
   #17: #ifsum2(true(),xs,y) -> #sum2(tail(xs),y)
   #18: #ifsum2(true(),xs,y) -> #tail(xs)
   #19: #if(false(),x,y,z) -> #gen(x,y,s(z))
   #20: #isZero(s(_1)) ->? #isZero❆1_s(_1)
   #21: #ge(s(x),s(y)) -> #ge(x,y)
   #22: #gen(x,y,z) -> #if(ge(z,x),x,y,z)
   #23: #gen(x,y,z) -> #ge(z,x)
   #24: #times(x,y) -> #sum(generate(x,y))
   #25: #times(x,y) -> #generate(x,y)
Number of SCCs: 5, DPs: 9, edges: 10
	SCC { #12 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
     d()	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#isZero(x1)	weight: 0
#sum2(x1,x2)	weight: 0
p❆1_s(x1)	weight: 0
#generate(x1,x2)	weight: 0
#p❆1_0()	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
 isNil(x1)	weight: 0
  #ge(x1,x2)	weight: 0
  sum2(x1,x2)	weight: 0
     c()	weight: 0
   #p(x1)	weight: 0
#p❆1_s(x1)	weight: 0
  true()	weight: 0
   sum(x1)	weight: 0
 ifsum(x1,x2,x3,x4)	weight: 0
     p(x1)	weight: 0
  tail(x1)	weight: 0
 error()	weight: 0
#times(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4)	weight: 0
    ge(x1,x2)	weight: 0
 times(x1,x2)	weight: 0
p❆1_0()	weight: 0
#isZero❆1_s(x1)	weight: x1
   nil()	weight: 0
 #gen(x1,x2,x3)	weight: 0
#tail(x1)	weight: 0
#ifsum2(x1,x2,x3)	weight: 0
isZero❆1_0()	weight: 0
#isNil(x1)	weight: 0
   gen(x1,x2,x3)	weight: 0
#ifsum(x1,x2,x3,x4)	weight: 0
generate(x1,x2)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3,x4)	weight: 0
   #a()	weight: 0
#isZero❆1_0()	weight: 0
isZero❆1_s(x1)	weight: 0
isZero(x1)	weight: 0
ifsum2(x1,x2,x3)	weight: 0
 #sum(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #12
Number of SCCs: 4, DPs: 8, edges: 9
	SCC { #9 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
     d()	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#isZero(x1)	weight: 0
#sum2(x1,x2)	weight: 0
p❆1_s(x1)	weight: 0
#generate(x1,x2)	weight: 0
#p❆1_0()	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
 isNil(x1)	weight: 0
  #ge(x1,x2)	weight: 0
  sum2(x1,x2)	weight: 0
     c()	weight: 0
   #p(x1)	weight: 0
#p❆1_s(x1)	weight: x1
  true()	weight: 0
   sum(x1)	weight: 0
 ifsum(x1,x2,x3,x4)	weight: 0
     p(x1)	weight: 0
  tail(x1)	weight: 0
 error()	weight: 0
#times(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4)	weight: 0
    ge(x1,x2)	weight: 0
 times(x1,x2)	weight: 0
p❆1_0()	weight: 0
#isZero❆1_s(x1)	weight: 0
   nil()	weight: 0
 #gen(x1,x2,x3)	weight: 0
#tail(x1)	weight: 0
#ifsum2(x1,x2,x3)	weight: 0
isZero❆1_0()	weight: 0
#isNil(x1)	weight: 0
   gen(x1,x2,x3)	weight: 0
#ifsum(x1,x2,x3,x4)	weight: 0
generate(x1,x2)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3,x4)	weight: 0
   #a()	weight: 0
#isZero❆1_0()	weight: 0
isZero❆1_s(x1)	weight: 0
isZero(x1)	weight: 0
ifsum2(x1,x2,x3)	weight: 0
 #sum(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #9
Number of SCCs: 3, DPs: 7, edges: 8
	SCC { #21 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a()	weight: 0
     d()	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#isZero(x1)	weight: 0
#sum2(x1,x2)	weight: 0
p❆1_s(x1)	weight: 0
#generate(x1,x2)	weight: 0
#p❆1_0()	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
 isNil(x1)	weight: 0
  #ge(x1,x2)	weight: x2
  sum2(x1,x2)	weight: 0
     c()	weight: 0
   #p(x1)	weight: 0
#p❆1_s(x1)	weight: 0
  true()	weight: 0
   sum(x1)	weight: 0
 ifsum(x1,x2,x3,x4)	weight: 0
     p(x1)	weight: 0
  tail(x1)	weight: 0
 error()	weight: 0
#times(x1,x2)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4)	weight: 0
    ge(x1,x2)	weight: 0
 times(x1,x2)	weight: 0
p❆1_0()	weight: 0
#isZero❆1_s(x1)	weight: 0
   nil()	weight: 0
 #gen(x1,x2,x3)	weight: 0
#tail(x1)	weight: 0
#ifsum2(x1,x2,x3)	weight: 0
isZero❆1_0()	weight: 0
#isNil(x1)	weight: 0
   gen(x1,x2,x3)	weight: 0
#ifsum(x1,x2,x3,x4)	weight: 0
generate(x1,x2)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3,x4)	weight: 0
   #a()	weight: 0
#isZero❆1_0()	weight: 0
isZero❆1_s(x1)	weight: 0
isZero(x1)	weight: 0
ifsum2(x1,x2,x3)	weight: 0
 #sum(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #21
Number of SCCs: 2, DPs: 6, edges: 7
	SCC { #19 #22 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed.
Removing edges: failed.
Finding a loop...  failed.
MAYBE