Input TRS:
    1: isEmpty(cons(x,xs)) -> false()
    2: isEmpty(nil()) -> true()
    3: isZero(0()) -> true()
    4: isZero(s(x)) -> false()
    5: head(cons(x,xs)) -> x
    6: tail(cons(x,xs)) -> xs
    7: tail(nil()) -> nil()
    8: p(s(s(x))) -> s(p(s(x)))
    9: p(s(0())) -> 0()
    10: p(0()) -> 0()
    11: inc(s(x)) -> s(inc(x))
    12: inc(0()) -> s(0())
    13: sumList(xs,y) -> if(isEmpty(xs),isZero(head(xs)),y,tail(xs),cons(p(head(xs)),tail(xs)),inc(y))
    14: if(true(),b,y,xs,ys,x) -> y
    15: if(false(),true(),y,xs,ys,x) -> sumList(xs,y)
    16: if(false(),false(),y,xs,ys,x) -> sumList(ys,x)
    17: sum(xs) -> sumList(xs,0())
Number of strict rules: 17
Direct Order(PosReal,>,Poly) ... failed.
Freezing p
1: isEmpty(cons(x,xs)) -> false()
2: isEmpty(nil()) -> true()
3: isZero(0()) -> true()
4: isZero(s(x)) -> false()
5: head(cons(x,xs)) -> x
6: tail(cons(x,xs)) -> xs
7: tail(nil()) -> nil()
8: p❆1_s(s(x)) -> s(p❆1_s(x))
9: p❆1_s(0()) -> 0()
10: p❆1_0() -> 0()
11: inc(s(x)) -> s(inc(x))
12: inc(0()) -> s(0())
13: sumList(xs,y) -> if(isEmpty(xs),isZero(head(xs)),y,tail(xs),cons(p(head(xs)),tail(xs)),inc(y))
14: if(true(),b,y,xs,ys,x) -> y
15: if(false(),true(),y,xs,ys,x) -> sumList(xs,y)
16: if(false(),false(),y,xs,ys,x) -> sumList(ys,x)
17: sum(xs) -> sumList(xs,0())
18: p(0()) ->= p❆1_0()
19: p(s(_1)) ->= p❆1_s(_1)
Number of strict rules: 17
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #sumList(xs,y) -> #if(isEmpty(xs),isZero(head(xs)),y,tail(xs),cons(p(head(xs)),tail(xs)),inc(y))
   #2: #sumList(xs,y) -> #isEmpty(xs)
   #3: #sumList(xs,y) -> #isZero(head(xs))
   #4: #sumList(xs,y) -> #head(xs)
   #5: #sumList(xs,y) -> #tail(xs)
   #6: #sumList(xs,y) -> #p(head(xs))
   #7: #sumList(xs,y) -> #head(xs)
   #8: #sumList(xs,y) -> #tail(xs)
   #9: #sumList(xs,y) -> #inc(y)
   #10: #inc(s(x)) -> #inc(x)
   #11: #sum(xs) -> #sumList(xs,0())
   #12: #p(s(_1)) ->? #p❆1_s(_1)
   #13: #if(false(),false(),y,xs,ys,x) -> #sumList(ys,x)
   #14: #p❆1_s(s(x)) -> #p❆1_s(x)
   #15: #if(false(),true(),y,xs,ys,x) -> #sumList(xs,y)
   #16: #p(0()) ->? #p❆1_0()
Number of SCCs: 3, DPs: 5, edges: 6
	SCC { #10 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
sumList(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#isZero(x1)	weight: 0
#sumList(x1,x2)	weight: 0
p❆1_s(x1)	weight: 0
#isEmpty(x1)	weight: 0
#p❆1_0()	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
isEmpty(x1)	weight: 0
 #inc(x1)	weight: x1
   #p(x1)	weight: 0
   inc(x1)	weight: 0
#p❆1_s(x1)	weight: 0
  true()	weight: 0
   sum(x1)	weight: 0
     p(x1)	weight: 0
  tail(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4,x5,x6)	weight: 0
p❆1_0()	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3,x4,x5,x6)	weight: 0
isZero(x1)	weight: 0
 #sum(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #10
Number of SCCs: 2, DPs: 4, edges: 5
	SCC { #14 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
sumList(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#isZero(x1)	weight: 0
#sumList(x1,x2)	weight: 0
p❆1_s(x1)	weight: 0
#isEmpty(x1)	weight: 0
#p❆1_0()	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
isEmpty(x1)	weight: 0
 #inc(x1)	weight: 0
   #p(x1)	weight: 0
   inc(x1)	weight: 0
#p❆1_s(x1)	weight: x1
  true()	weight: 0
   sum(x1)	weight: 0
     p(x1)	weight: 0
  tail(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3,x4,x5,x6)	weight: 0
p❆1_0()	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3,x4,x5,x6)	weight: 0
isZero(x1)	weight: 0
 #sum(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #14
Number of SCCs: 1, DPs: 3, edges: 4
	SCC { #1 #13 #15 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
sumList(x1,x2)	weight: 0
     s(x1)	weight: (max (/ 5 8) 0)
#isZero(x1)	weight: 0
#sumList(x1,x2)	weight: max{0, (- (/ 1 4)) + x1}
p❆1_s(x1)	weight: (max (/ 5 8) 0)
#isEmpty(x1)	weight: 0
#p❆1_0()	weight: 0
 false()	weight: (/ 1 4)
#head(x1)	weight: 0
isEmpty(x1)	weight: (max (/ 1 2) 0)
 #inc(x1)	weight: 0
   #p(x1)	weight: 0
   inc(x1)	weight: (max (- (/ 1 8)) 0)
#p❆1_s(x1)	weight: 0
  true()	weight: (/ 1 4)
   sum(x1)	weight: 0
     p(x1)	weight: max{0, x1}
  tail(x1)	weight: max{0, (- (/ 1 4)) + x1}
     0()	weight: (/ 5 8)
    if(x1,x2,x3,x4,x5,x6)	weight: 0
p❆1_0()	weight: (/ 5 8)
   nil()	weight: 0
#tail(x1)	weight: 0
  head(x1)	weight: max{0, (/ 1 8) + x1}
  cons(x1,x2)	weight: max{0, (- (/ 1 8)) + x1, (/ 1 4) + x2}
  #if(x1,x2,x3,x4,x5,x6)	weight: max{0, (- (/ 1 8)) + x2, x4, (- (/ 1 4)) + x5}
isZero(x1)	weight: max{0, (- (/ 3 8)) + x1}
 #sum(x1)	weight: 0
    Usable rules: { 3..10 18 19 }
    Removed DPs: #15
Number of SCCs: 1, DPs: 2, edges: 2
	SCC { #1 #13 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
sumList(x1,x2)	weight: 0
     s(x1)	weight: max{0, (/ 9 16) + x1}
#isZero(x1)	weight: 0
#sumList(x1,x2)	weight: max{0, (- (/ 1 4)) + x1}
p❆1_s(x1)	weight: max{0, (/ 1 4) + x1}
#isEmpty(x1)	weight: 0
#p❆1_0()	weight: 0
 false()	weight: (/ 1 8)
#head(x1)	weight: 0
isEmpty(x1)	weight: max{0, (/ 1 4) + x1}
 #inc(x1)	weight: 0
   #p(x1)	weight: 0
   inc(x1)	weight: (max (- (/ 9 16)) 0)
#p❆1_s(x1)	weight: 0
  true()	weight: 0
   sum(x1)	weight: 0
     p(x1)	weight: max{0, (- (/ 5 16)) + x1}
  tail(x1)	weight: (max (- (/ 1 16)) 0)
     0()	weight: 0
    if(x1,x2,x3,x4,x5,x6)	weight: 0
p❆1_0()	weight: 0
   nil()	weight: (/ 1 16)
#tail(x1)	weight: 0
  head(x1)	weight: max{0, (/ 3 16) + x1}
  cons(x1,x2)	weight: max{0, (- (/ 3 16)) + x1}
  #if(x1,x2,x3,x4,x5,x6)	weight: max{0, (- (/ 1 16)) + x2, x5}
isZero(x1)	weight: max{0, (- (/ 7 16)) + x1}
 #sum(x1)	weight: 0
    Usable rules: { 3..5 8..10 18 19 }
    Removed DPs: #13
Number of SCCs: 0, DPs: 0, edges: 0
YES