Input TRS:
    1: a(f(),0()) -> a(s(),0())
    2: a(d(),0()) -> 0()
    3: a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x)))))
    4: a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x))))
    5: a(p(),a(s(),x)) -> x
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... failed.
Freezing a❆1_p a
1: a❆1_f(0()) -> a❆1_s(0())
2: a❆1_d(0()) -> 0()
3: a❆1_d(a❆1_s(x)) -> a❆1_s(a❆1_s(a❆1_d(a❆1_p❆1_a❆1_s(x))))
4: a❆1_f(a❆1_s(x)) -> a❆1_d(a❆1_f(a❆1_p❆1_a❆1_s(x)))
5: a❆1_p❆1_a❆1_s(x) -> x
6: a(p(),_1) ->= a❆1_p(_1)
7: a(d(),_1) ->= a❆1_d(_1)
8: a(s(),_1) ->= a❆1_s(_1)
9: a(f(),_1) ->= a❆1_f(_1)
10: a❆1_p(a❆1_s(_1)) ->= a❆1_p❆1_a❆1_s(_1)
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 8 10 7 9 6
     a(x1,x2)	weight: (/ 1 2) + x1 + x2
     d()	weight: 0
     s()	weight: 0
a❆1_f(x1)	weight: x1
     f()	weight: 0
     p()	weight: 0
a❆1_s(x1)	weight: x1
     0()	weight: 0
a❆1_p(x1)	weight: (/ 1 4) + x1
a❆1_p❆1_a❆1_s(x1)	weight: x1
a❆1_d(x1)	weight: x1
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 1
     a(x1,x2)	weight: (/ 1 2) + x1 + x2
     d()	weight: 0
     s()	weight: 0
a❆1_f(x1)	weight: (/ 1 4) + x1
     f()	weight: 0
     p()	weight: 0
a❆1_s(x1)	weight: x1
     0()	weight: 0
a❆1_p(x1)	weight: (/ 1 4) + x1
a❆1_p❆1_a❆1_s(x1)	weight: x1
a❆1_d(x1)	weight: x1
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #a❆1_d(a❆1_s(x)) -> #a❆1_d(a❆1_p❆1_a❆1_s(x))
   #2: #a❆1_d(a❆1_s(x)) -> #a❆1_p❆1_a❆1_s(x)
   #3: #a❆1_f(a❆1_s(x)) -> #a❆1_d(a❆1_f(a❆1_p❆1_a❆1_s(x)))
   #4: #a❆1_f(a❆1_s(x)) -> #a❆1_f(a❆1_p❆1_a❆1_s(x))
   #5: #a❆1_f(a❆1_s(x)) -> #a❆1_p❆1_a❆1_s(x)
Number of SCCs: 2, DPs: 2, edges: 2
	SCC { #1 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a(x1,x2)	weight: 0
     d()	weight: 0
     s()	weight: 0
a❆1_f(x1)	weight: 0
#a❆1_p❆1_a❆1_s(x1)	weight: 0
     f()	weight: 0
     p()	weight: 0
a❆1_s(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
a❆1_p(x1)	weight: 0
#a❆1_d(x1)	weight: x1
a❆1_p❆1_a❆1_s(x1)	weight: (/ 1 4) + x1
#a❆1_f(x1)	weight: 0
a❆1_d(x1)	weight: 0
    Usable rules: { 5 }
    Removed DPs: #1
Number of SCCs: 1, DPs: 1, edges: 1
	SCC { #4 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     a(x1,x2)	weight: 0
     d()	weight: 0
     s()	weight: 0
a❆1_f(x1)	weight: 0
#a❆1_p❆1_a❆1_s(x1)	weight: 0
     f()	weight: 0
     p()	weight: 0
a❆1_s(x1)	weight: (/ 1 2) + x1
     0()	weight: 0
a❆1_p(x1)	weight: 0
#a❆1_d(x1)	weight: x1
a❆1_p❆1_a❆1_s(x1)	weight: (/ 1 4) + x1
#a❆1_f(x1)	weight: x1
a❆1_d(x1)	weight: 0
    Usable rules: { 5 }
    Removed DPs: #4
Number of SCCs: 0, DPs: 0, edges: 0
YES