Consider the TRS R consisting of the rewrite rules

1: c(z,x,a) -> f(b(b(f(z),z),x))
2: b(y,b(z,a)) -> f(b(c(f(a),y,z),z))
3: f(c(c(z,a,a),x,a)) -> z

There are 8 dependency pairs:

4: C(z,x,a) -> F(b(b(f(z),z),x))
5: C(z,x,a) -> B(b(f(z),z),x)
6: C(z,x,a) -> B(f(z),z)
7: C(z,x,a) -> F(z)
8: B(y,b(z,a)) -> F(b(c(f(a),y,z),z))
9: B(y,b(z,a)) -> B(c(f(a),y,z),z)
10: B(y,b(z,a)) -> C(f(a),y,z)
11: B(y,b(z,a)) -> F(a)

The approximated dependency graph contains one SCC:
{5,6,9,10}.

- Consider the SCC {5,6,9,10}.
By taking the polynomial interpretation
[a] = 0,
[C](x,y,z) = 2x + y + 1,
[b](x,y) = [c](x,y,z) = x + 1,
[B](x,y) = x + y
and [f](x) = x - 1,
we obtain a quasi-model of RR.
Furthermore, the dependency pairs in {5,9,10}
are weakly decreasing and
dependency pair 6
is strictly decreasing.
There is one new SCC.

- Consider the SCC {5,9,10}.
By taking the polynomial interpretation
[a] = 1,
[b](x,y) = [c](x,y,z) = x + 1,
[B](x,y) = x + y,
[C](x,y,z) = x + y + z
and [f](x) = x - 1,
we obtain a quasi-model of RR.
Furthermore, the dependency pairs in {5,9}
are weakly decreasing and
dependency pair 10
is strictly decreasing.
There is one new SCC.

- Consider the SCC {9}.
By taking the polynomial interpretation
[a] = 0,
[b](x,y) = [c](x,y,z) = x + 1,
[f](x) = x - 1
and [B](x,y) = y,
we obtain a quasi-model of RR.
Furthermore, dependency pair 9
is strictly decreasing.



Hence the TRS is terminating.