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: weight(cons(n,cons(m,x))) -> weight(sum(cons(n,cons(m,x)),cons(0(),x)))
    5: weight(cons(n,nil())) -> n
Number of strict rules: 5
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: weight(cons(n,cons(m,x))) -> weight(sum❆1_cons(n,cons(m,x),cons(0(),x)))
5: weight(cons(n,nil())) -> n
6: sum(cons(_1,_2),_3) ->= sum❆1_cons(_1,_2,_3)
7: sum(nil(),_1) ->= sum❆1_nil(_1)
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 4 3 5 7 6 2
     s(x1)	weight: (/ 1 32) + x1
sum❆1_cons(x1,x2,x3)	weight: (/ 3 32) + x1 + x2 + x3
   sum(x1,x2)	weight: (/ 1 16) + x1 + x2
     0()	weight: 0
   nil()	weight: 0
weight(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 8) + x1 + 2 * x2
sum❆1_nil(x1)	weight: (/ 1 32) + x1
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 1
     s(x1)	weight: (/ 1 16) + x1
sum❆1_cons(x1,x2,x3)	weight: (/ 3 16) + 2 * x1 + x2 + x3
   sum(x1,x2)	weight: (/ 1 8) + x1 + x2
     0()	weight: 0
   nil()	weight: 0
weight(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 4) + x1 + 2 * x2
sum❆1_nil(x1)	weight: (/ 1 16) + x1
Number of strict rules: 0
YES