Consider the TRS R consisting of the rewrite rules

1: min(X,0) -> X
2: min(s(X),s(Y)) -> min(X,Y)
3: quot(0,s(Y)) -> 0
4: quot(s(X),s(Y)) -> s(quot(min(X,Y),s(Y)))
5: log(s(0)) -> 0
6: log(s(s(X))) -> s(log(s(quot(X,s(s(0))))))

There are 5 dependency pairs:

7: MIN(s(X),s(Y)) -> MIN(X,Y)
8: QUOT(s(X),s(Y)) -> QUOT(min(X,Y),s(Y))
9: QUOT(s(X),s(Y)) -> MIN(X,Y)
10: LOG(s(s(X))) -> LOG(s(quot(X,s(s(0)))))
11: LOG(s(s(X))) -> QUOT(X,s(s(0)))

The approximated dependency graph contains 3 SCCs:
{7},
{8}
and {10}.

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

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

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

Hence the TRS is terminating.