YES TRS: ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X) u21(ackout(X),Y) -> u22(ackin(Y,X)) linear polynomial interpretations on N: ackin_A(x1,x2) = 1 ackin#_A(x1,x2) = x1 s_A(x1) = x1 + 2 s#_A(x1) = 0 u21_A(x1,x2) = x1 u21#_A(x1,x2) = x2 + 1 ackout_A(x1) = x1 + 1 ackout#_A(x1) = 0 u22_A(x1) = 0 u22#_A(x1) = 0 precedence: u21 = ackout = u22 > ackin > s