Input TRS:
    1: ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X)
    2: u21(ackout(X),Y) -> u22(ackin(Y,X))
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... failed.
Freezing ackin
1: ackin❆1_s(X,s(Y)) -> u21(ackin❆1_s(X,Y),X)
2: u21(ackout(X),Y) -> u22(ackin(Y,X))
3: ackin(s(_1),_2) ->= ackin❆1_s(_1,_2)
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #u21(ackout(X),Y) -> #ackin(Y,X)
   #2: #ackin(s(_1),_2) ->? #ackin❆1_s(_1,_2)
   #3: #ackin❆1_s(X,s(Y)) -> #u21(ackin❆1_s(X,Y),X)
   #4: #ackin❆1_s(X,s(Y)) -> #ackin❆1_s(X,Y)
Number of SCCs: 1, DPs: 1, edges: 1
	SCC { #4 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#ackin(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
 #u21(x1,x2)	weight: 0
ackout(x1)	weight: 0
   u21(x1,x2)	weight: 0
#ackin❆1_s(x1,x2)	weight: x2
   u22(x1)	weight: 0
ackin❆1_s(x1,x2)	weight: 0
 ackin(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #4
Number of SCCs: 0, DPs: 0, edges: 0
YES