Consider the TRS R consisting of the rewrite rules

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

There are 5 dependency pairs:

11: A__G(X) -> A__H(X)
12: A__H(d) -> A__G(c)
13: MARK(g(X)) -> A__G(X)
14: MARK(h(X)) -> A__H(X)
15: MARK(c) -> A__C

The approximated dependency graph contains one SCC:
{11,12}.

- Consider the SCC {11,12}.
There are no usable rules.
By taking the polynomial interpretation
[c] = 0,
[d] = 1
and [A__G](x) = [A__H](x) = x + 1,
rule 11
is weakly decreasing and
rule 12
is strictly decreasing.

Hence the TRS is terminating.