Input TRS:
    1: ack_in(|0|(),n) -> ack_out(s(n))
    2: ack_in(s(m),|0|()) -> u11(ack_in(m,s(|0|())))
    3: u11(ack_out(n)) -> ack_out(n)
    4: ack_in(s(m),s(n)) -> u21(ack_in(s(m),n),m)
    5: u21(ack_out(n),m) -> u22(ack_in(m,n))
    6: u22(ack_out(n)) -> ack_out(n)
Number of strict rules: 6
Direct Order(PosReal,>,Poly) ... failed.
Freezing ack_in
1: ack_in❆1_|0|(n) -> ack_out(s(n))
2: ack_in❆1_s(m,|0|()) -> u11(ack_in(m,s(|0|())))
3: u11(ack_out(n)) -> ack_out(n)
4: ack_in❆1_s(m,s(n)) -> u21(ack_in❆1_s(m,n),m)
5: u21(ack_out(n),m) -> u22(ack_in(m,n))
6: u22(ack_out(n)) -> ack_out(n)
7: ack_in(|0|(),_1) ->= ack_in❆1_|0|(_1)
8: ack_in(s(_1),_2) ->= ack_in❆1_s(_1,_2)
Number of strict rules: 6
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #ack_in❆1_s(m,|0|()) -> #u11(ack_in(m,s(|0|())))
   #2: #ack_in❆1_s(m,|0|()) -> #ack_in(m,s(|0|()))
   #3: #ack_in(|0|(),_1) ->? #ack_in❆1_|0|(_1)
   #4: #u21(ack_out(n),m) -> #u22(ack_in(m,n))
   #5: #u21(ack_out(n),m) -> #ack_in(m,n)
   #6: #ack_in(s(_1),_2) ->? #ack_in❆1_s(_1,_2)
   #7: #ack_in❆1_s(m,s(n)) -> #u21(ack_in❆1_s(m,n),m)
   #8: #ack_in❆1_s(m,s(n)) -> #ack_in❆1_s(m,n)
Number of SCCs: 1, DPs: 5, edges: 9
	SCC { #2 #5..8 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
ack_in❆1_s(x1,x2)	weight: (/ 1 8) + x2
 #u22(x1)	weight: 0
#ack_in(x1,x2)	weight: x1
     s(x1)	weight: (/ 3 16) + x1
#ack_in❆1_|0|(x1)	weight: 0
 #u21(x1,x2)	weight: (/ 1 16) + x2
 #u11(x1)	weight: 0
ack_out(x1)	weight: (/ 1 4)
   u11(x1)	weight: (/ 3 16)
   u21(x1,x2)	weight: (/ 1 4) + x1
   u22(x1)	weight: (/ 1 2) + x1
ack_in❆1_|0|(x1)	weight: (/ 1 8)
#ack_in❆1_s(x1,x2)	weight: (/ 1 8) + x1
ack_in(x1,x2)	weight: (/ 1 16)
    Usable rules: { }
    Removed DPs: #2 #5..7
Number of SCCs: 1, DPs: 1, edges: 1
	SCC { #8 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
ack_in❆1_s(x1,x2)	weight: (/ 1 8) + x2
 #u22(x1)	weight: 0
#ack_in(x1,x2)	weight: 0
     s(x1)	weight: (/ 3 16) + x1
#ack_in❆1_|0|(x1)	weight: 0
 #u21(x1,x2)	weight: (/ 1 16)
 #u11(x1)	weight: 0
ack_out(x1)	weight: (/ 1 4)
   u11(x1)	weight: (/ 3 16)
   u21(x1,x2)	weight: (/ 1 4) + x1
   u22(x1)	weight: (/ 1 2) + x1
ack_in❆1_|0|(x1)	weight: (/ 1 8)
#ack_in❆1_s(x1,x2)	weight: (/ 1 8) + x2
ack_in(x1,x2)	weight: (/ 1 16)
    Usable rules: { }
    Removed DPs: #8
Number of SCCs: 0, DPs: 0, edges: 0
YES