Consider the TRS R consisting of the rewrite rules

1: plus(x,0) -> x
2: plus(x,s(y)) -> s(plus(x,y))
3: times(0,y) -> 0
4: times(x,0) -> 0
5: times(s(x),y) -> plus(times(x,y),y)
6: p(s(s(x))) -> s(p(s(x)))
7: p(s(0)) -> 0
8: fac(s(x)) -> times(fac(p(s(x))),s(x))

There are 7 dependency pairs:

9: PLUS(x,s(y)) -> PLUS(x,y)
10: TIMES(s(x),y) -> PLUS(times(x,y),y)
11: TIMES(s(x),y) -> TIMES(x,y)
12: P(s(s(x))) -> P(s(x))
13: FAC(s(x)) -> TIMES(fac(p(s(x))),s(x))
14: FAC(s(x)) -> FAC(p(s(x)))
15: FAC(s(x)) -> P(s(x))

The approximated dependency graph contains 4 SCCs:
{12},
{9},
{11}
and {14}.

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

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

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

- Consider the SCC {14}.
The usable rules are {6,7}.
By taking the polynomial interpretation
[0] = 0,
[FAC](x) = x,
[s](x) = x + 1
and [p](x) = x - 1,
we obtain a quasi-model of the usable rules.
Furthermore, dependency pair 14
is strictly decreasing.

Hence the TRS is terminating.