YES
(VAR X)
(RULES 
a__g(X) -> a__h(X)
a__c -> d
a__h(d) -> a__g(c)
mark(g(X)) -> a__g(X)
mark(h(X)) -> a__h(X)
mark(c) -> a__c
mark(d) -> d
a__g(X) -> g(X)
a__h(X) -> h(X)
a__c -> c
)

Proving termination of rewriting for Ex1_Zan97_GM:

-> Dependency pairs:
nF_a__g(X) -> nF_a__h(X)
nF_a__h(d) -> nF_a__g(c)
nF_mark(g(X)) -> nF_a__g(X)
nF_mark(h(X)) -> nF_a__h(X)
nF_mark(c) -> nF_a__c

-> Proof of termination for Ex1_Zan97_GM_1:
-> -> Dependency pairs in cycle:
nF_a__g(X) -> nF_a__h(X)
nF_a__h(d) -> nF_a__g(c)

There are no usable rules.

Polynomial Interpretation:

[a__g](X) = 0
[a__h](X) = 0
[a__c] = 0
[d] = 1
[c] = 0
[mark](X) = 0
[g](X) = 0
[h](X) = 0
[nF_a__g](X) = X
[nF_a__h](X) = X

TIME: 5.9033e-2


SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.