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(X)) -> mark(g(h(f(X))))
(2) active(f(X)) -> f(active(X))
(3) active(h(X)) -> h(active(X))
(4) f(mark(X)) -> mark(f(X))
(5) h(mark(X)) -> mark(h(X))
(6) proper(f(X)) -> f(proper(X))
(7) proper(g(X)) -> g(proper(X))
(8) proper(h(X)) -> h(proper(X))
(9) f(ok(X)) -> ok(f(X))
(10) g(ok(X)) -> ok(g(X))
(11) h(ok(X)) -> ok(h(X))
(12) top(mark(X)) -> top(proper(X))
(13) top(ok(X)) -> top(active(X))

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

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

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

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

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

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

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


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