Input TRS:
    1: empty(nil()) -> true()
    2: empty(cons(x,y)) -> false()
    3: tail(nil()) -> nil()
    4: tail(cons(x,y)) -> y
    5: head(cons(x,y)) -> x
    6: zero(0()) -> true()
    7: zero(s(x)) -> false()
    8: p(0()) -> 0()
    9: p(s(0())) -> 0()
    10: p(s(s(x))) -> s(p(s(x)))
    11: intlist(x) -> if_intlist(empty(x),x)
    12: if_intlist(true(),x) -> nil()
    13: if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
    14: int(x,y) -> if_int(zero(x),zero(y),x,y)
    15: if_int(true(),b,x,y) -> if1(b,x,y)
    16: if_int(false(),b,x,y) -> if2(b,x,y)
    17: if1(true(),x,y) -> cons(0(),nil())
    18: if1(false(),x,y) -> cons(0(),int(s(0()),y))
    19: if2(true(),x,y) -> nil()
    20: if2(false(),x,y) -> intlist(int(p(x),p(y)))
Number of strict rules: 20
Direct Order(PosReal,>,Poly) ... failed.
Freezing p
1: empty(nil()) -> true()
2: empty(cons(x,y)) -> false()
3: tail(nil()) -> nil()
4: tail(cons(x,y)) -> y
5: head(cons(x,y)) -> x
6: zero(0()) -> true()
7: zero(s(x)) -> false()
8: p❆1_0() -> 0()
9: p❆1_s(0()) -> 0()
10: p❆1_s(s(x)) -> s(p❆1_s(x))
11: intlist(x) -> if_intlist(empty(x),x)
12: if_intlist(true(),x) -> nil()
13: if_intlist(false(),x) -> cons(s(head(x)),intlist(tail(x)))
14: int(x,y) -> if_int(zero(x),zero(y),x,y)
15: if_int(true(),b,x,y) -> if1(b,x,y)
16: if_int(false(),b,x,y) -> if2(b,x,y)
17: if1(true(),x,y) -> cons(0(),nil())
18: if1(false(),x,y) -> cons(0(),int(s(0()),y))
19: if2(true(),x,y) -> nil()
20: if2(false(),x,y) -> intlist(int(p(x),p(y)))
21: p(0()) ->= p❆1_0()
22: p(s(_1)) ->= p❆1_s(_1)
Number of strict rules: 20
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #if_intlist(false(),x) -> #head(x)
   #2: #if_intlist(false(),x) -> #intlist(tail(x))
   #3: #if_intlist(false(),x) -> #tail(x)
   #4: #intlist(x) -> #if_intlist(empty(x),x)
   #5: #intlist(x) -> #empty(x)
   #6: #int(x,y) -> #if_int(zero(x),zero(y),x,y)
   #7: #int(x,y) -> #zero(x)
   #8: #int(x,y) -> #zero(y)
   #9: #if2(false(),x,y) -> #intlist(int(p(x),p(y)))
   #10: #if2(false(),x,y) -> #int(p(x),p(y))
   #11: #if2(false(),x,y) -> #p(x)
   #12: #if2(false(),x,y) -> #p(y)
   #13: #p❆1_s(s(x)) -> #p❆1_s(x)
   #14: #p(s(_1)) ->? #p❆1_s(_1)
   #15: #p(0()) ->? #p❆1_0()
   #16: #if_int(false(),b,x,y) -> #if2(b,x,y)
   #17: #if_int(true(),b,x,y) -> #if1(b,x,y)
   #18: #if1(false(),x,y) -> #int(s(0()),y)
Number of SCCs: 3, DPs: 8, edges: 9
	SCC { #13 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
  zero(x1)	weight: 0
#empty(x1)	weight: 0
#intlist(x1)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
if_int(x1,x2,x3,x4)	weight: 0
p❆1_s(x1)	weight: 0
#if_int(x1,x2,x3,x4)	weight: 0
#p❆1_0()	weight: 0
   if1(x1,x2,x3)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
   #p(x1)	weight: 0
#p❆1_s(x1)	weight: x1
  true()	weight: 0
 #if1(x1,x2,x3)	weight: 0
   if2(x1,x2,x3)	weight: 0
     p(x1)	weight: 0
  tail(x1)	weight: 0
     0()	weight: 0
p❆1_0()	weight: 0
   nil()	weight: 0
intlist(x1)	weight: 0
#tail(x1)	weight: 0
#if_intlist(x1,x2)	weight: 0
   int(x1,x2)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
 empty(x1)	weight: 0
#zero(x1)	weight: 0
 #if2(x1,x2,x3)	weight: 0
if_intlist(x1,x2)	weight: 0
 #int(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #13
Number of SCCs: 2, DPs: 7, edges: 8
	SCC { #2 #4 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
  zero(x1)	weight: 0
#empty(x1)	weight: 0
#intlist(x1)	weight: max{0, (/ 3 8) + x1}
     s(x1)	weight: 0
if_int(x1,x2,x3,x4)	weight: 0
p❆1_s(x1)	weight: 0
#if_int(x1,x2,x3,x4)	weight: 0
#p❆1_0()	weight: 0
   if1(x1,x2,x3)	weight: 0
 false()	weight: (/ 1 4)
#head(x1)	weight: 0
   #p(x1)	weight: 0
#p❆1_s(x1)	weight: 0
  true()	weight: 0
 #if1(x1,x2,x3)	weight: 0
   if2(x1,x2,x3)	weight: 0
     p(x1)	weight: 0
  tail(x1)	weight: max{0, (- (/ 1 4)) + x1}
     0()	weight: 0
p❆1_0()	weight: 0
   nil()	weight: 0
intlist(x1)	weight: 0
#tail(x1)	weight: 0
#if_intlist(x1,x2)	weight: max{0, (/ 1 4) + x1, (/ 1 8) + x2}
   int(x1,x2)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: max{0, (/ 3 8) + x2}
 empty(x1)	weight: max{0, (- (/ 1 8)) + x1}
#zero(x1)	weight: 0
 #if2(x1,x2,x3)	weight: 0
if_intlist(x1,x2)	weight: 0
 #int(x1,x2)	weight: 0
    Usable rules: { 1..4 }
    Removed DPs: #4
Number of SCCs: 1, DPs: 5, edges: 6
	SCC { #6 #10 #16..18 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
  zero(x1)	weight: max{0, (- (/ 1 8)) + x1}
#empty(x1)	weight: 0
#intlist(x1)	weight: max{0, x1}
     s(x1)	weight: max{0, (/ 13 16) + x1}
if_int(x1,x2,x3,x4)	weight: 0
p❆1_s(x1)	weight: max{0, (/ 1 16) + x1}
#if_int(x1,x2,x3,x4)	weight: max{0, (/ 1 2) + x2, (/ 1 16) + x3, (/ 9 16) + x4}
#p❆1_0()	weight: 0
   if1(x1,x2,x3)	weight: 0
 false()	weight: (/ 11 16)
#head(x1)	weight: 0
   #p(x1)	weight: 0
#p❆1_s(x1)	weight: 0
  true()	weight: 0
 #if1(x1,x2,x3)	weight: max{0, (/ 7 16) + x1, (- (/ 1 16)) + x2, (/ 9 16) + x3}
   if2(x1,x2,x3)	weight: 0
     p(x1)	weight: max{0, (- (/ 5 16)) + x1}
  tail(x1)	weight: max{0, (- (/ 1 8)) + x1}
     0()	weight: 0
p❆1_0()	weight: 0
   nil()	weight: 0
intlist(x1)	weight: 0
#tail(x1)	weight: 0
#if_intlist(x1,x2)	weight: 0
   int(x1,x2)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: max{0, (/ 3 4) + x2}
 empty(x1)	weight: max{0, (- (/ 1 16)) + x1}
#zero(x1)	weight: 0
 #if2(x1,x2,x3)	weight: max{0, (- (/ 1 16)) + x1, x2, (/ 1 4) + x3}
if_intlist(x1,x2)	weight: 0
 #int(x1,x2)	weight: max{0, (/ 5 16) + x1, (/ 9 16) + x2}
    Usable rules: { 6..10 21 22 }
    Removed DPs: #16
Number of SCCs: 1, DPs: 3, edges: 3
	SCC { #6 #17 #18 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
  zero(x1)	weight: x1
#empty(x1)	weight: 0
#intlist(x1)	weight: (/ 1 2)
     s(x1)	weight: 0
if_int(x1,x2,x3,x4)	weight: 0
p❆1_s(x1)	weight: (/ 1 2)
#if_int(x1,x2,x3,x4)	weight: max{0, x1}
#p❆1_0()	weight: 0
   if1(x1,x2,x3)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
   #p(x1)	weight: 0
#p❆1_s(x1)	weight: 0
  true()	weight: (/ 1 2)
 #if1(x1,x2,x3)	weight: 0
   if2(x1,x2,x3)	weight: 0
     p(x1)	weight: (/ 1 2)
  tail(x1)	weight: 0
     0()	weight: (/ 1 2)
p❆1_0()	weight: (/ 1 2)
   nil()	weight: (/ 1 4)
intlist(x1)	weight: 0
#tail(x1)	weight: 0
#if_intlist(x1,x2)	weight: 0
   int(x1,x2)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: max{(/ 1 4) + x2, (/ 1 4) + x1}
 empty(x1)	weight: x1
#zero(x1)	weight: 0
 #if2(x1,x2,x3)	weight: 0
if_intlist(x1,x2)	weight: 0
 #int(x1,x2)	weight: max{0, x1}
    Usable rules: { 6 7 }
    Removed DPs: #17
Number of SCCs: 0, DPs: 0, edges: 0
YES