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) active(2nd(cons(X,cons(Y,Z)))) -> mark(Y)
(2) active(from(X)) -> mark(cons(X,from(s(X))))
(3) active(2nd(X)) -> 2nd(active(X))
(4) active(cons(X1,X2)) -> cons(active(X1),X2)
(5) active(from(X)) -> from(active(X))
(6) active(s(X)) -> s(active(X))
(7) 2nd(mark(X)) -> mark(2nd(X))
(8) cons(mark(X1),X2) -> mark(cons(X1,X2))
(9) from(mark(X)) -> mark(from(X))
(10) s(mark(X)) -> mark(s(X))
(11) proper(2nd(X)) -> 2nd(proper(X))
(12) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
(13) proper(from(X)) -> from(proper(X))
(14) proper(s(X)) -> s(proper(X))
(15) 2nd(ok(X)) -> ok(2nd(X))
(16) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
(17) from(ok(X)) -> ok(from(X))
(18) s(ok(X)) -> ok(s(X))
(19) top(mark(X)) -> top(proper(X))
(20) top(ok(X)) -> top(active(X))

[2]  Use following polynomial interpretation:
[active(x)] = 7x
[ok(x)] = 7x
rest default

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

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

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

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

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

[5]  All the rules of this TRS can be oriented with RPO with the following precedence:
Precedence:
active > 2nd
active > cons
active > from
active > s
2nd > mark
proper > 2nd
2nd > ok
cons > mark
proper > cons
from > mark
s > mark
proper > from
from > ok
proper > s
s > ok


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