Consider the TRS R consisting of the rewrite rules

1: pred(s(x)) -> x
2: minus(x,0) -> x
3: minus(x,s(y)) -> pred(minus(x,y))
4: quot(0,s(y)) -> 0
5: quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
6: log(s(0)) -> 0
7: log(s(s(x))) -> s(log(s(quot(x,s(s(0))))))

There are 6 dependency pairs:

8: MINUS(x,s(y)) -> PRED(minus(x,y))
9: MINUS(x,s(y)) -> MINUS(x,y)
10: QUOT(s(x),s(y)) -> QUOT(minus(x,y),s(y))
11: QUOT(s(x),s(y)) -> MINUS(x,y)
12: LOG(s(s(x))) -> LOG(s(quot(x,s(s(0)))))
13: LOG(s(s(x))) -> QUOT(x,s(s(0)))

The approximated dependency graph contains 3 SCCs:
{9},
{10}
and {12}.

- Consider the SCC {9}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [MINUS](x,y) = x + y + 1,
rule 9
is strictly decreasing.

- Consider the SCC {10}.
The usable rules are {1-3}.
By taking the polynomial interpretation
[0] = 1,
[minus](x,y) = [pred](x) = x,
[s](x) = x + 1
and [QUOT](x,y) = x + y + 1,
the rules in {2,3}
are weakly decreasing and
the rules in {1,10}
are strictly decreasing.

- Consider the SCC {12}.
The usable rules are {1-5}.
By taking the polynomial interpretation
[0] = 1,
[minus](x,y) = [pred](x) = [quot](x,y) = x
and [LOG](x) = [s](x) = x + 1,
the rules in {2-5}
are weakly decreasing and
the rules in {1,12}
are strictly decreasing.

Hence the TRS is terminating.