Input TRS:
    1: f(g(f(a()),h(a(),f(a())))) -> f(h(g(f(a()),a()),g(f(a()),f(a()))))
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 1
     a()	weight: 0
     h(x1,x2)	weight: (/ 71313 2) + 2 * x1 + x2
     f(x1)	weight: (/ 1 16) + x1
     g(x1,x2)	weight: x1 + 2 * x2
Number of strict rules: 0
YES