Input TRS:
    1: active(c()) -> mark(f(g(c())))
    2: active(f(g(X))) -> mark(g(X))
    3: mark(c()) -> active(c())
    4: mark(f(X)) -> active(f(X))
    5: mark(g(X)) -> active(g(X))
    6: f(mark(X)) -> f(X)
    7: f(active(X)) -> f(X)
    8: g(mark(X)) -> g(X)
    9: g(active(X)) -> g(X)
Number of strict rules: 9
Direct Order(PosReal,>,Poly) ... removes: 8 7 9 6
     c()	weight: 0
     f(x1)	weight: x1
  mark(x1)	weight: (/ 1 4) + x1
active(x1)	weight: (/ 1 4) + x1
     g(x1)	weight: x1
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... failed.
Freezing mark active
1: active❆1_c() -> mark❆1_f(g(c()))
2: active❆1_f(g(X)) -> mark❆1_g(X)
3: mark❆1_c() -> active❆1_c()
4: mark❆1_f(X) -> active❆1_f(X)
5: mark❆1_g(X) -> active❆1_g(X)
10: active(c()) ->= active❆1_c()
11: active(g(_1)) ->= active❆1_g(_1)
12: active(f(_1)) ->= active❆1_f(_1)
13: mark(c()) ->= mark❆1_c()
14: mark(g(_1)) ->= mark❆1_g(_1)
15: mark(f(_1)) ->= mark❆1_f(_1)
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 15 10 14 12 11 13
mark❆1_c()	weight: 0
     c()	weight: 0
     f(x1)	weight: (/ 1 4) + x1
mark❆1_f(x1)	weight: x1
  mark(x1)	weight: (/ 1 4) + x1
active❆1_c()	weight: 0
active(x1)	weight: (/ 1 4) + 2 * x1
active❆1_g(x1)	weight: x1
mark❆1_g(x1)	weight: x1
active❆1_f(x1)	weight: x1
     g(x1)	weight: x1
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #active❆1_f(g(X)) -> #mark❆1_g(X)
   #2: #mark❆1_c() -> #active❆1_c()
   #3: #active❆1_c() -> #mark❆1_f(g(c()))
   #4: #mark❆1_f(X) -> #active❆1_f(X)
Number of SCCs: 0, DPs: 0, edges: 0
YES