Input TRS:
    1: a__f(f(a())) -> a__f(g(f(a())))
    2: mark(f(X)) -> a__f(mark(X))
    3: mark(a()) -> a()
    4: mark(g(X)) -> g(X)
    5: a__f(X) -> f(X)
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 4 3
     a()	weight: 0
  a__f(x1)	weight: (/ 1 8) + x1
     f(x1)	weight: (/ 1 8) + x1
  mark(x1)	weight: (/ 1 8) + x1
     g(x1)	weight: x1
Number of strict rules: 3
Direct Order(PosReal,>,Poly) ... removes: 5 2
     a()	weight: 0
  a__f(x1)	weight: (/ 84955 4) + x1
     f(x1)	weight: (/ 42477 2) + x1
  mark(x1)	weight: (/ 1 4) + 2 * x1
     g(x1)	weight: x1
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... failed.
Freezing a__f
1: a__f❆1_f(a()) -> a__f❆1_g(f(a()))
6: a__f(g(_1)) ->= a__f❆1_g(_1)
7: a__f(f(_1)) ->= a__f❆1_f(_1)
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 1 7 6
     a()	weight: 0
  a__f(x1)	weight: (/ 1 2) + 2 * x1
a__f❆1_g(x1)	weight: 2 * x1
     f(x1)	weight: (/ 1 4) + x1
  mark(x1)	weight: x1
     g(x1)	weight: (/ 153 4) + x1
a__f❆1_f(x1)	weight: (/ 3 4) + x1
Number of strict rules: 0
YES