Consider the TRS R consisting of the rewrite rule

1: f(f(a,f(x,a)),a) -> f(a,f(f(x,a),a))

There are 2 dependency pairs:

2: F(f(a,f(x,a)),a) -> F(a,f(f(x,a),a))
3: F(f(a,f(x,a)),a) -> F(f(x,a),a)

The approximated dependency graph contains one SCC:
{3}.

- Consider the SCC {3}.
By taking the polynomial interpretation
[a] = 1
and [f](x,y) = [F](x,y) = x + y + 1,
rule 1
is weakly decreasing and
rule 3
is strictly decreasing.

Hence the TRS is terminating.