Consider the TRS R consisting of the rewrite rules 1: f(x,y) -> g1(x,x,y) 2: f(x,y) -> g1(y,x,x) 3: f(x,y) -> g2(x,y,y) 4: f(x,y) -> g2(y,y,x) 5: g1(x,x,y) -> h(x,y) 6: g1(y,x,x) -> h(x,y) 7: g2(x,y,y) -> h(x,y) 8: g2(y,y,x) -> h(x,y) 9: h(x,x) -> x There are 8 dependency pairs: 10: F(x,y) -> G1(x,x,y) 11: F(x,y) -> G1(y,x,x) 12: F(x,y) -> G2(x,y,y) 13: F(x,y) -> G2(y,y,x) 14: G1(x,x,y) -> H(x,y) 15: G1(y,x,x) -> H(x,y) 16: G2(x,y,y) -> H(x,y) 17: G2(y,y,x) -> H(x,y) The approximated dependency graph contains no SCCs and hence the TRS is trivially terminating.