Input TRS:
    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))
Number of strict rules: 21
Direct Order(PosReal,>,Poly) ... removes: 4 15 1 3 5 10 9 6 2
    p5()	weight: 0
   p10()	weight: 0
    p2()	weight: 0
     +(x1,x2)	weight: (/ 1 8) + 2 * x1 + x2
    p1()	weight: 0
Number of strict rules: 12
Direct Order(PosReal,>,Poly) ... failed.
Freezing +
7: +❆1_p2(p1()) -> +❆1_p1(p2())
8: +❆1_p2(+❆1_p1(x)) -> +❆1_p1(+❆1_p2(x))
11: +❆1_p5(p1()) -> +❆1_p1(p5())
12: +❆1_p5(+❆1_p1(x)) -> +❆1_p1(+❆1_p5(x))
13: +❆1_p5(p2()) -> +❆1_p2(p5())
14: +❆1_p5(+❆1_p2(x)) -> +❆1_p2(+❆1_p5(x))
16: +❆1_p10(p1()) -> +❆1_p1(p10())
17: +❆1_p10(+❆1_p1(x)) -> +❆1_p1(+❆1_p10(x))
18: +❆1_p10(p2()) -> +❆1_p2(p10())
19: +❆1_p10(+❆1_p2(x)) -> +❆1_p2(+❆1_p10(x))
20: +❆1_p10(p5()) -> +❆1_p5(p10())
21: +❆1_p10(+❆1_p5(x)) -> +❆1_p5(+❆1_p10(x))
22: +(p10(),_1) ->= +❆1_p10(_1)
23: +(p2(),_1) ->= +❆1_p2(_1)
24: +(p5(),_1) ->= +❆1_p5(_1)
25: +(p1(),_1) ->= +❆1_p1(_1)
Number of strict rules: 12
Direct Order(PosReal,>,Poly) ... removes: 22 25 23 24
+❆1_p1(x1)	weight: (/ 4875 2) + 2 * x1
+❆1_p2(x1)	weight: (/ 4875 2) + 2 * x1
+❆1_p5(x1)	weight: (/ 4875 2) + 2 * x1
    p5()	weight: 0
+❆1_p10(x1)	weight: (/ 4875 2) + 2 * x1
   p10()	weight: 0
    p2()	weight: 0
     +(x1,x2)	weight: 2438 + x1 + 2 * x2
    p1()	weight: 0
Number of strict rules: 12
Direct Order(PosReal,>,Poly) ... removes: 8 16 17 7 12 11
+❆1_p1(x1)	weight: (/ 1 4) + x1
+❆1_p2(x1)	weight: (/ 17711 2) + 2 * x1
+❆1_p5(x1)	weight: (/ 17711 2) + 2 * x1
    p5()	weight: 0
+❆1_p10(x1)	weight: (/ 17711 2) + 2 * x1
   p10()	weight: 0
    p2()	weight: 0
     +(x1,x2)	weight: (/ 35423 4) + x1 + 2 * x2
    p1()	weight: 0
Number of strict rules: 6
Direct Order(PosReal,>,Poly) ... removes: 18 20 13
+❆1_p1(x1)	weight: x1
+❆1_p2(x1)	weight: (/ 1 8) + x1
+❆1_p5(x1)	weight: (/ 1 4) + x1
    p5()	weight: 0
+❆1_p10(x1)	weight: (/ 3 8) + x1
   p10()	weight: 0
    p2()	weight: 0
     +(x1,x2)	weight: (/ 3 8) + x1 + 2 * x2
    p1()	weight: 0
Number of strict rules: 3
Direct Order(PosReal,>,Poly) ... removes: 14
+❆1_p1(x1)	weight: x1
+❆1_p2(x1)	weight: (/ 1 8) + x1
+❆1_p5(x1)	weight: (/ 1 4) + 2 * x1
    p5()	weight: 0
+❆1_p10(x1)	weight: x1
   p10()	weight: 0
    p2()	weight: 0
     +(x1,x2)	weight: (/ 3 8) + x1 + 2 * x2
    p1()	weight: 0
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... removes: 19
+❆1_p1(x1)	weight: (/ 1 8) + x1
+❆1_p2(x1)	weight: (/ 1 4) + 2 * x1
+❆1_p5(x1)	weight: x1
    p5()	weight: 0
+❆1_p10(x1)	weight: (/ 1 8) + 2 * x1
   p10()	weight: 0
    p2()	weight: 0
     +(x1,x2)	weight: (/ 1 4) + x1 + 2 * x2
    p1()	weight: 0
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 21
+❆1_p1(x1)	weight: (/ 16731 2) + x1
+❆1_p2(x1)	weight: (/ 33463 4) + 2 * x1
+❆1_p5(x1)	weight: (/ 33461 4) + x1
    p5()	weight: 0
+❆1_p10(x1)	weight: (/ 16731 2) + 2 * x1
   p10()	weight: 0
    p2()	weight: 0
     +(x1,x2)	weight: (/ 33463 4) + x1 + 2 * x2
    p1()	weight: 0
Number of strict rules: 0
YES