Consider the TRS R consisting of the rewrite rules

1: ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X)
2: u21(ackout(X),Y) -> u22(ackin(Y,X))

There are 3 dependency pairs:

3: ACKIN(s(X),s(Y)) -> U21(ackin(s(X),Y),X)
4: ACKIN(s(X),s(Y)) -> ACKIN(s(X),Y)
5: U21(ackout(X),Y) -> ACKIN(Y,X)

Consider the SCC {3-5}.
By taking the polynomial interpretation
[ackout](x) = [s](x) = [u21](x,y) = [u22](x) = x + 1,
[ACKIN](x,y) = [U21](x,y) = x + y + 1
and [ackin](x,y) = y + 1,
the rules in {1,2}
are weakly decreasing and
the rules in {3-5}
are strictly decreasing.
Hence the TRS is terminating.