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

[2]  Label this TRS using following interpretation that is a model:
[active(x)] = 1
[g(x)] = 1
[top(x)] = 0
rest default

  thus obtaining new TRS:
(1a) active$0(c) -> mark$1(f$1(g$0(c)))
(2a) active$1(f$1(g$1(X))) -> mark$1(g$1(X))
(2b) active$1(f$1(g$0(X))) -> mark$1(g$0(X))
(3a) proper$0(c) -> ok$0(c)
(4a) proper$1(f$1(X)) -> f$1(proper$1(X))
(4b) proper$0(f$0(X)) -> f$0(proper$0(X))
(5a) proper$1(g$1(X)) -> g$1(proper$1(X))
(5b) proper$1(g$0(X)) -> g$0(proper$0(X))
(6a) f$1(ok$1(X)) -> ok$1(f$1(X))
(6b) f$0(ok$0(X)) -> ok$0(f$0(X))
(7a) g$1(ok$1(X)) -> ok$1(g$1(X))
(7b) g$0(ok$0(X)) -> ok$1(g$0(X))
(8a) top$1(mark$1(X)) -> top$1(proper$1(X))
(8b) top$0(mark$0(X)) -> top$0(proper$0(X))
(9a) top$1(ok$1(X)) -> top$1(active$1(X))
(9b) top$0(ok$0(X)) -> top$1(active$0(X))

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

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

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

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

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

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

[6]  Unlabel this TRS to obtain the one consisting of the rules:
(2)-(9)

[7]  Use following polynomial interpretation:
[f(x)] = x + 1
rest default

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

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

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

[9]  Use following polynomial interpretation:
[proper(x)] = x + 1
rest default

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

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

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

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


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