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__eq(0,0) -> true
(2) a__eq(s(X),s(Y)) -> a__eq(X,Y)
(3) a__eq(X,Y) -> false
(4) a__inf(X) -> cons(X,inf(s(X)))
(5) a__take(0,X) -> nil
(6) a__take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
(7) a__length(nil) -> 0
(8) a__length(cons(X,L)) -> s(length(L))
(9) mark(eq(X1,X2)) -> a__eq(X1,X2)
(10) mark(inf(X)) -> a__inf(mark(X))
(11) mark(take(X1,X2)) -> a__take(mark(X1),mark(X2))
(12) mark(length(X)) -> a__length(mark(X))
(13) mark(0) -> 0
(14) mark(true) -> true
(15) mark(s(X)) -> s(X)
(16) mark(false) -> false
(17) mark(cons(X1,X2)) -> cons(X1,X2)
(18) mark(nil) -> nil
(19) a__eq(X1,X2) -> eq(X1,X2)
(20) a__inf(X) -> inf(X)
(21) a__take(X1,X2) -> take(X1,X2)
(22) a__length(X) -> length(X)

[2]  All the rules of this TRS can be oriented with RPO with the following precedence:
Precedence:
a__eq > true
a__eq > false
mark > a__eq
a__eq > eq
a__length > 0
a__inf > s
a__length > s
a__inf > cons
a__inf > inf
mark > a__inf
a__take > cons
a__take > nil
a__take > take
mark > a__take
a__length > length
mark > a__length


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