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(f(g(X),Y)) -> mark(f(X,f(g(X),Y)))
(2) active(f(X1,X2)) -> f(active(X1),X2)
(3) active(g(X)) -> g(active(X))
(4) f(mark(X1),X2) -> mark(f(X1,X2))
(5) g(mark(X)) -> mark(g(X))
(6) proper(f(X1,X2)) -> f(proper(X1),proper(X2))
(7) proper(g(X)) -> g(proper(X))
(8) f(ok(X1),ok(X2)) -> ok(f(X1,X2))
(9) g(ok(X)) -> ok(g(X))
(10) top(mark(X)) -> top(proper(X))
(11) 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), (8)

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

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

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

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

[5]  All the rules of this TRS can be oriented with RPO with the following precedence:
Precedence:
active > f
active > g
f > mark
proper > f
g > mark
proper > g
g > ok


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