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) a__g(X) -> a__h(X)
(2) a__c -> d
(3) a__h(d) -> a__g(c)
(4) mark(g(X)) -> a__g(X)
(5) mark(h(X)) -> a__h(X)
(6) mark(c) -> a__c
(7) mark(d) -> d
(8) a__g(X) -> g(X)
(9) a__h(X) -> h(X)
(10) a__c -> c

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

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

[3]  Use following polynomial interpretation:
[a__c] = 3
rest default

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

[4]  Use following polynomial interpretation:
[d] = 3
rest default

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

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

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

[6]  Use following polynomial interpretation:
[a__h(x)] = x + 1
rest default

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

[7]  Since there are no remaining rules, termination is proved!

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