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) 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)

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

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

[3]  All the rules of this TRS can be oriented with RPO with the following precedence:
Status: ack_in: Lex-LR, 
Precedence:
ack_in{i,j} = ack_in{k,l} for all i, j, k, l
ack_in{i,j} > ack_out{k} for all i, j, k
ack_in{i,j} > s{k} for all i, j, k
ack_in{i,j} > u11{k} for all i, j, k
ack_in{i,j} > u21{k,l} for i > k+l
u21{i,j} > ack_in{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/Cime/ack_prolog.trs, 0.01, Y
Couldn't open file <60>: 60: No such file or directory