Consider the TRS R consisting of the rewrite rules

1: prime(0) -> false
2: prime(s(0)) -> false
3: prime(s(s(x))) -> prime1(s(s(x)),s(x))
4: prime1(x,0) -> false
5: prime1(x,s(0)) -> true
6: prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y)))
7: divp(x,y) -> rem(x,y) = 0

There are 3 dependency pairs:

8: PRIME(s(s(x))) -> PRIME1(s(s(x)),s(x))
9: PRIME1(x,s(s(y))) -> DIVP(s(s(y)),x)
10: PRIME1(x,s(s(y))) -> PRIME1(x,s(y))

The approximated dependency graph contains one SCC:
{10}.

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

Hence the TRS is terminating.