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