Consider the TRS R consisting of the rewrite rules

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

There are 6 dependency pairs:

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

The approximated dependency graph contains 2 SCCs:
{8}
and {4}.

- Consider the SCC {8}.
By taking the polynomial interpretation
[a] = 0,
[f](x) = 3x + 2,
[c](x,y,z) = 3x + 3y + 3,
[F](x) = x + 1
and [b](x,y) = x + 2y + 3,
the rules in {1-3,8}
are strictly decreasing.

- Consider the SCC {4}.
By taking the polynomial interpretation
[a] = 0,
[f](x) = 3x + 2,
[c](x,y,z) = 3x + 3y + 3,
[F](x) = x + 1
and [b](x,y) = x + 2y + 3,
the rules in {1-4}
are strictly decreasing.

Hence the TRS is terminating.