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

[2]  Label this TRS using following interpretation that is a quasi-model:
[mark(x)] = 0
[d] = 1
[top(x)] = 0
rest default

  thus obtaining new TRS:
(1a) active$1(g$1(X)) -> mark$1(h$1(X))
(1b) active$0(g$0(X)) -> mark$0(h$0(X))
(2a) active$0(c) -> mark$1(d)
(3a) active$1(h$1(d)) -> mark$0(g$0(c))
(4a) proper$1(g$1(X)) -> g$1(proper$1(X))
(4b) proper$0(g$0(X)) -> g$0(proper$0(X))
(5a) proper$1(h$1(X)) -> h$1(proper$1(X))
(5b) proper$0(h$0(X)) -> h$0(proper$0(X))
(6a) proper$0(c) -> ok$0(c)
(7a) proper$1(d) -> ok$1(d)
(8a) g$1(ok$1(X)) -> ok$1(g$1(X))
(8b) g$0(ok$0(X)) -> ok$0(g$0(X))
(9a) h$1(ok$1(X)) -> ok$1(h$1(X))
(9b) h$0(ok$0(X)) -> ok$0(h$0(X))
(10a) top$0(mark$1(X)) -> top$1(proper$1(X))
(10b) top$0(mark$0(X)) -> top$0(proper$0(X))
(11a) top$1(ok$1(X)) -> top$1(active$1(X))
(11b) top$0(ok$0(X)) -> top$0(active$0(X))
(D1) g$1(x) ->= g$0(x)
(D2) h$1(x) ->= h$0(x)
(D3) mark$1(x) ->= mark$0(x)
(D4) proper$1(x) ->= proper$0(x)
(D5) ok$1(x) ->= ok$0(x)
(D6) active$1(x) ->= active$0(x)
(D7) top$1(x) ->= top$0(x)

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

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

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

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

[5]  Unlabel this TRS to obtain the one consisting of the rules:
(1)-(2), (4)-(11)

[6]  Use following polynomial interpretation:
[c] = 3
rest default

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

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

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

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

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

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

  Remove rules with left hand side strictly bigger than right hand side:
(6)-(7)

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

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

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


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