Consider the TRS R consisting of the rewrite rules

1: a__c -> a__f(g(c))
2: a__f(g(X)) -> g(X)
3: mark(c) -> a__c
4: mark(f(X)) -> a__f(X)
5: mark(g(X)) -> g(X)
6: a__c -> c
7: a__f(X) -> f(X)

There are 3 dependency pairs:

8: A__C -> A__F(g(c))
9: MARK(c) -> A__C
10: MARK(f(X)) -> A__F(X)

The approximated dependency graph contains no SCCs
and hence the TRS is trivially terminating.