Input TRS:
    1: f(f(a(),f(a(),a())),x) -> f(x,f(f(a(),a()),a()))
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... failed.
Freezing f
1: f❆2_a(f❆1_a(a()),x) -> f(x,f❆2_a(a(),a()))
2: f(a(),_1) ->= f❆1_a(_1)
3: f(f❆1_a(_1),_2) ->= f❆2_a(_1,_2)
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 3
     a()	weight: 0
f❆2_a(x1,x2)	weight: (/ 1 4) + x1 + x2
     f(x1,x2)	weight: (/ 1 4) + x1 + x2
f❆1_a(x1)	weight: (/ 1 4) + x1
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 1 2
     a()	weight: 0
f❆2_a(x1,x2)	weight: (/ 1 8) + 2 * x1 + x2
     f(x1,x2)	weight: (/ 3 8) + x1 + x2
f❆1_a(x1)	weight: (/ 1 4) + x1
Number of strict rules: 0
YES