YES
  TPA v.1.0

Result: TRS is terminating

Default interpretations for symbols are not printed. For polynomial interpretations
and semantic labelling over N\{0,1} defaults are 2 for constants, identity for unary
symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans)
defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols.

[1]  TRS loaded from input file:
(1) ackin(0,X) -> ackout(s(X))
(2) ackin(s(X),0) -> u11(ackin(X,s(0)))
(3) u11(ackout(X)) -> ackout(X)
(4) ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X)
(5) u21(ackout(X),Y) -> u22(ackin(Y,X))
(6) u22(ackout(X)) -> ackout(X)

[2]  Label this TRS using following interpretation over N\{0,1}:
[ackin(x,y)] = 2
[ackout(x)] = 2
[s(x)] = 7x
[u21(x,y)] = 2
rest default

  This interpretation is a model and yields following TRS:
(1) ackin{2,i}(0,X) -> ackout{7i}(s{i}(X))
(2) ackin{7i,2}(s{i}(X),0) -> u11{2}(ackin{i,14}(X,s{2}(0)))
(3) u11{2}(ackout{i}(X)) -> ackout{i}(X)
(4) ackin{7i,7j}(s{i}(X),s{j}(Y)) -> u21{2,i}(ackin{7i,j}(s{i}(X),Y),X)
(5) u21{2,j}(ackout{i}(X),Y) -> u22{2}(ackin{j,i}(Y,X))
(6) u22{2}(ackout{i}(X)) -> ackout{i}(X)

[3]  All the rules of this TRS can be oriented with RPO with the following precedence:
Status: ackin: Lex-LR, 
Precedence:
ackin{i,j} = ackin{k,l} for all i, j, k, l
ackin{i,j} > ackout{k} for all i, j, k
ackin{i,j} > s{k} for all i, j, k
ackin{i,j} > u11{k} for all i, j, k
ackin{i,j} > u21{k,l} for i > k+l
u21{i,j} > ackin{k,l} for i+j > k
s{i} = s{k} for all i, k
u21{i,j} > u22{k} for all i, j, k


../tpdb/TRS/Rubio/ackclaude.trs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory