Consider the TRS R consisting of the rewrite rules

1: p1 + p1 -> p2
2: p1 + (p2 + p2) -> p5
3: p5 + p5 -> p10
4: (x + y) + z -> x + (y + z)
5: p1 + (p1 + x) -> p2 + x
6: p1 + (p2 + (p2 + x)) -> p5 + x
7: p2 + p1 -> p1 + p2
8: p2 + (p1 + x) -> p1 + (p2 + x)
9: p2 + (p2 + p2) -> p1 + p5
10: p2 + (p2 + (p2 + x)) -> p1 + (p5 + x)
11: p5 + p1 -> p1 + p5
12: p5 + (p1 + x) -> p1 + (p5 + x)
13: p5 + p2 -> p2 + p5
14: p5 + (p2 + x) -> p2 + (p5 + x)
15: p5 + (p5 + x) -> p10 + x
16: p10 + p1 -> p1 + p10
17: p10 + (p1 + x) -> p1 + (p10 + x)
18: p10 + p2 -> p2 + p10
19: p10 + (p2 + x) -> p2 + (p10 + x)
20: p10 + p5 -> p5 + p10
21: p10 + (p5 + x) -> p5 + (p10 + x)

There are 26 dependency pairs:

22: (x + y) +# z -> x +# (y + z)
23: (x + y) +# z -> y +# z
24: p1 +# (p1 + x) -> p2 +# x
25: p1 +# (p2 + (p2 + x)) -> p5 +# x
26: p2 +# p1 -> p1 +# p2
27: p2 +# (p1 + x) -> p1 +# (p2 + x)
28: p2 +# (p1 + x) -> p2 +# x
29: p2 +# (p2 + p2) -> p1 +# p5
30: p2 +# (p2 + (p2 + x)) -> p1 +# (p5 + x)
31: p2 +# (p2 + (p2 + x)) -> p5 +# x
32: p5 +# p1 -> p1 +# p5
33: p5 +# (p1 + x) -> p1 +# (p5 + x)
34: p5 +# (p1 + x) -> p5 +# x
35: p5 +# p2 -> p2 +# p5
36: p5 +# (p2 + x) -> p2 +# (p5 + x)
37: p5 +# (p2 + x) -> p5 +# x
38: p5 +# (p5 + x) -> p10 +# x
39: p10 +# p1 -> p1 +# p10
40: p10 +# (p1 + x) -> p1 +# (p10 + x)
41: p10 +# (p1 + x) -> p10 +# x
42: p10 +# p2 -> p2 +# p10
43: p10 +# (p2 + x) -> p2 +# (p10 + x)
44: p10 +# (p2 + x) -> p10 +# x
45: p10 +# p5 -> p5 +# p10
46: p10 +# (p5 + x) -> p5 +# (p10 + x)
47: p10 +# (p5 + x) -> p10 +# x

The approximated dependency graph contains 2 SCCs:
{24,25,27,28,30,31,33,34,36-38,40,41,43,44,46,47}
and {22}.

- Consider the SCC {24,25,27,28,30,31,33,34,36-38,40,41,43,44,46,47}.
By taking the polynomial interpretation
[p1] = [p10] = [p2] = [p5] = [y] = [z] = 1
and [+](x,y) = [+#](x,y) = x + y + 1,
the rules in {4,7,8,11-14,16-21,27,33,36,40,43,46}
are weakly decreasing and
the rules in {1-3,5,6,9,10,15,24,25,28,30,31,34,37,38,41,44,47}
are strictly decreasing.

- Consider the SCC {22}.
By taking the polynomial interpretation
[p1] = [p10] = [p2] = [p5] = [y] = [z] = 1,
[+#](x,y) = x + 1
and [+](x,y) = x + y + 1,
the rules in {4,7,8,11-14,16-21}
are weakly decreasing and
the rules in {1-3,5,6,9,10,15,22}
are strictly decreasing.

Hence the TRS is terminating.