Input TRS:
    1: sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y))
    2: sum(cons(0(),x),y) -> sum(x,y)
    3: sum(nil(),y) -> y
    4: empty(nil()) -> true()
    5: empty(cons(n,x)) -> false()
    6: tail(nil()) -> nil()
    7: tail(cons(n,x)) -> x
    8: head(cons(n,x)) -> n
    9: weight(x) -> if(empty(x),empty(tail(x)),x)
    10: if(true(),b,x) -> weight_undefined_error()
    11: if(false(),b,x) -> if2(b,x)
    12: if2(true(),x) -> head(x)
    13: if2(false(),x) -> weight(sum(x,cons(0(),tail(tail(x)))))
Number of strict rules: 13
Direct Order(PosReal,>,Poly) ... failed.
Freezing sum
1: sum❆1_cons(s(n),x,cons(m,y)) -> sum❆1_cons(n,x,cons(s(m),y))
2: sum❆1_cons(0(),x,y) -> sum(x,y)
3: sum❆1_nil(y) -> y
4: empty(nil()) -> true()
5: empty(cons(n,x)) -> false()
6: tail(nil()) -> nil()
7: tail(cons(n,x)) -> x
8: head(cons(n,x)) -> n
9: weight(x) -> if(empty(x),empty(tail(x)),x)
10: if(true(),b,x) -> weight_undefined_error()
11: if(false(),b,x) -> if2(b,x)
12: if2(true(),x) -> head(x)
13: if2(false(),x) -> weight(sum(x,cons(0(),tail(tail(x)))))
14: sum(cons(_1,_2),_3) ->= sum❆1_cons(_1,_2,_3)
15: sum(nil(),_1) ->= sum❆1_nil(_1)
Number of strict rules: 13
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #sum❆1_cons(0(),x,y) -> #sum(x,y)
   #2: #if2(false(),x) -> #weight(sum(x,cons(0(),tail(tail(x)))))
   #3: #if2(false(),x) -> #sum(x,cons(0(),tail(tail(x))))
   #4: #if2(false(),x) -> #tail(tail(x))
   #5: #if2(false(),x) -> #tail(x)
   #6: #weight(x) -> #if(empty(x),empty(tail(x)),x)
   #7: #weight(x) -> #empty(x)
   #8: #weight(x) -> #empty(tail(x))
   #9: #weight(x) -> #tail(x)
   #10: #if(false(),b,x) -> #if2(b,x)
   #11: #if2(true(),x) -> #head(x)
   #12: #sum(cons(_1,_2),_3) ->? #sum❆1_cons(_1,_2,_3)
   #13: #sum❆1_cons(s(n),x,cons(m,y)) -> #sum❆1_cons(n,x,cons(s(m),y))
   #14: #sum(nil(),_1) ->? #sum❆1_nil(_1)
Number of SCCs: 2, DPs: 6, edges: 8
	SCC { #2 #6 #10 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
#empty(x1)	weight: 0
     s(x1)	weight: (max (/ 1 16) 0)
#weight(x1)	weight: max{0, (- (/ 3 16)) + x1}
sum❆1_cons(x1,x2,x3)	weight: max{0, (- (/ 1 16)) + x2, (/ 1 16) + x3}
 false()	weight: (/ 11 16)
#head(x1)	weight: 0
#sum❆1_cons(x1,x2,x3)	weight: 0
  true()	weight: (/ 1 16)
   sum(x1,x2)	weight: max{0, (- (/ 11 16)) + x1, (/ 1 16) + x2}
   if2(x1,x2)	weight: 0
  tail(x1)	weight: max{0, (- (/ 7 16)) + x1}
     0()	weight: (/ 3 16)
    if(x1,x2,x3)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
weight_undefined_error()	weight: 0
weight(x1)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: max{0, (/ 5 8) + x2}
  #if(x1,x2,x3)	weight: max{0, (- (/ 17 16)) + x1, (- (/ 1 8)) + x2, (- (/ 1 4)) + x3}
 empty(x1)	weight: max{0, (/ 1 16) + x1}
 #sum(x1,x2)	weight: 0
sum❆1_nil(x1)	weight: max{0, (/ 1 16) + x1}
 #if2(x1,x2)	weight: max{0, (- (/ 1 8)) + x1, (- (/ 5 16)) + x2}
#sum❆1_nil(x1)	weight: 0
    Usable rules: { 1..7 14 15 }
    Removed DPs: #2
Number of SCCs: 1, DPs: 3, edges: 5
	SCC { #1 #12 #13 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#empty(x1)	weight: 0
     s(x1)	weight: (/ 1 4) + x1
#weight(x1)	weight: 0
sum❆1_cons(x1,x2,x3)	weight: x2
 false()	weight: 0
#head(x1)	weight: 0
#sum❆1_cons(x1,x2,x3)	weight: (/ 1 4) + x1 + x2
  true()	weight: 0
   sum(x1,x2)	weight: (/ 1 4) + x1
   if2(x1,x2)	weight: 0
  tail(x1)	weight: (/ 1 4) + x1
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
   nil()	weight: 0
#tail(x1)	weight: 0
weight_undefined_error()	weight: 0
weight(x1)	weight: 0
  head(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 2) + x1 + x2
  #if(x1,x2,x3)	weight: 0
 empty(x1)	weight: 0
 #sum(x1,x2)	weight: x1
sum❆1_nil(x1)	weight: (/ 1 2)
 #if2(x1,x2)	weight: 0
#sum❆1_nil(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #1 #12 #13
Number of SCCs: 0, DPs: 0, edges: 0
YES