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) a__nats -> a__adx(a__zeros)
(2) a__zeros -> cons(0,zeros)
(3) a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
(4) a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
(5) a__hd(cons(X,Y)) -> mark(X)
(6) a__tl(cons(X,Y)) -> mark(Y)
(7) mark(nats) -> a__nats
(8) mark(adx(X)) -> a__adx(mark(X))
(9) mark(zeros) -> a__zeros
(10) mark(incr(X)) -> a__incr(mark(X))
(11) mark(hd(X)) -> a__hd(mark(X))
(12) mark(tl(X)) -> a__tl(mark(X))
(13) mark(cons(X1,X2)) -> cons(X1,X2)
(14) mark(0) -> 0
(15) mark(s(X)) -> s(X)
(16) a__nats -> nats
(17) a__adx(X) -> adx(X)
(18) a__zeros -> zeros
(19) a__incr(X) -> incr(X)
(20) a__hd(X) -> hd(X)
(21) a__tl(X) -> tl(X)

[2]  Use following polynomial interpretation:
[a__tl(x)] = x + 1
[tl(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(6)

[3]  Use following polynomial interpretation:
[a__hd(x)] = x + 1
[hd(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(5)

[4]  Use following polynomial interpretation:
[mark(x)] = x + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(7), (9), (13)-(15)

[5]  Use following polynomial interpretation:
[a__nats] = 3
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1), (16)

[6]  Use following polynomial interpretation:
[a__zeros] = 3
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(2), (18)

[7]  All the rules of this TRS can be oriented with RPO with the following precedence:
Precedence:
a__adx > cons
a__adx > a__incr
a__adx > adx
mark > a__adx
a__incr > cons
a__incr > s
a__incr > incr
mark > a__incr
mark > a__hd
a__hd > hd
mark > a__tl
a__tl > tl


../tpdb/TRS/TRCSR/ExIntrod_GM04_GM.trs, 0.02, Y
Couldn't open file <60>: 60: No such file or directory