Consider the TRS R consisting of the rewrite rules

1: a__f(X) -> g(h(f(X)))
2: mark(f(X)) -> a__f(mark(X))
3: mark(g(X)) -> g(X)
4: mark(h(X)) -> h(mark(X))
5: a__f(X) -> f(X)

There are 3 dependency pairs:

6: MARK(f(X)) -> A__F(mark(X))
7: MARK(f(X)) -> MARK(X)
8: MARK(h(X)) -> MARK(X)

The approximated dependency graph contains one SCC:
{7,8}.

- Consider the SCC {7,8}.
There are no usable rules.
By taking the polynomial interpretation
[f](x) = [h](x) = [MARK](x) = x + 1,
the rules in {7,8}
are strictly decreasing.

Hence the TRS is terminating.