Consider the TRS R consisting of the rewrite rules 1: f(f(x,y,z),u,f(x,y,v)) -> f(x,y,f(z,u,v)) 2: f(x,y,y) -> y 3: f(x,y,g(y)) -> x 4: f(x,x,y) -> x 5: f(g(x),x,y) -> y There are 2 dependency pairs: 6: F(f(x,y,z),u,f(x,y,v)) -> F(x,y,f(z,u,v)) 7: F(f(x,y,z),u,f(x,y,v)) -> F(z,u,v) Consider the SCC {6,7}. By taking the polynomial interpretation [g](x) = x + 1 and [f](x,y,z) = [F](x,y,z) = x + y + z + 1, the rules in {1-7} are strictly decreasing. Hence the TRS is terminating.