Consider the TRS R consisting of the rewrite rules

1: or(true,y) -> true
2: or(x,true) -> true
3: or(false,false) -> false
4: mem(x,nil) -> false
5: mem(x,set(y)) -> x = y
6: mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))

There are 3 dependency pairs:

7: MEM(x,union(y,z)) -> OR(mem(x,y),mem(x,z))
8: MEM(x,union(y,z)) -> MEM(x,y)
9: MEM(x,union(y,z)) -> MEM(x,z)

The approximated dependency graph contains one SCC:
{8,9}.

- Consider the SCC {8,9}.
There are no usable rules.
By taking the polynomial interpretation
[MEM](x,y) = [union](x,y) = x + y + 1,
the rules in {8,9}
are strictly decreasing.

Hence the TRS is terminating.