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(s(X),s(Y)) -> u21(ackin(s(X),Y),X)
(2) u21(ackout(X),Y) -> u22(ackin(Y,X))

[2]  Label this TRS using following interpretation that is a model:
[ackin(x,y)] = 0
[s(x)] = 0
[u21(x,y)] = 0
[ackout(x)] = 1
[u22(x)] = 0
rest default

  thus obtaining new TRS:
(1a) ackin$00(s$1(X),s$1(Y)) -> u21$01(ackin$01(s$1(X),Y),X)
(1b) ackin$00(s$0(X),s$1(Y)) -> u21$00(ackin$01(s$0(X),Y),X)
(1c) ackin$00(s$1(X),s$0(Y)) -> u21$01(ackin$00(s$1(X),Y),X)
(1d) ackin$00(s$0(X),s$0(Y)) -> u21$00(ackin$00(s$0(X),Y),X)
(2a) u21$11(ackout$1(X),Y) -> u22$0(ackin$11(Y,X))
(2b) u21$11(ackout$0(X),Y) -> u22$0(ackin$10(Y,X))
(2c) u21$10(ackout$1(X),Y) -> u22$0(ackin$01(Y,X))
(2d) u21$10(ackout$0(X),Y) -> u22$0(ackin$00(Y,X))

[3]  All the rules of this TRS can be oriented with RPO with the following precedence:
Precedence:
ackin$00 > u21$00
ackin$00 > u21$01
u21$10 > ackin$00
u21$10 > ackin$01
u21$10 > u22$0
u21$11 > ackin$10
u21$11 > ackin$11
u21$11 > u22$0
ackin$00 > ackin$01


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