Consider the TRS R consisting of the rewrite rules 1: not(and(x,y)) -> or(not(x),not(y)) 2: not(or(x,y)) -> and(not(x),not(y)) 3: and(x,or(y,z)) -> or(and(x,y),and(x,z)) There are 7 dependency pairs: 4: NOT(and(x,y)) -> NOT(x) 5: NOT(and(x,y)) -> NOT(y) 6: NOT(or(x,y)) -> AND(not(x),not(y)) 7: NOT(or(x,y)) -> NOT(x) 8: NOT(or(x,y)) -> NOT(y) 9: AND(x,or(y,z)) -> AND(x,y) 10: AND(x,or(y,z)) -> AND(x,z) The approximated dependency graph contains 2 SCCs: {9,10} and {4,5,7,8}. - Consider the SCC {9,10}. There are no usable rules. By taking the polynomial interpretation [AND](x,y) = [or](x,y) = x + y + 1, the rules in {9,10} are strictly decreasing. - Consider the SCC {4,5,7,8}. There are no usable rules. By taking the polynomial interpretation [NOT](x) = x + 1 and [and](x,y) = [or](x,y) = x + y + 1, the rules in {4,5,7,8} are strictly decreasing. Hence the TRS is terminating.