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

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

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

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

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

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


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