Input TRS:
    1: active(f(f(X))) -> mark(c(f(g(f(X)))))
    2: active(c(X)) -> mark(d(X))
    3: active(h(X)) -> mark(c(d(X)))
    4: active(f(X)) -> f(active(X))
    5: active(h(X)) -> h(active(X))
    6: f(mark(X)) -> mark(f(X))
    7: h(mark(X)) -> mark(h(X))
    8: proper(f(X)) -> f(proper(X))
    9: proper(c(X)) -> c(proper(X))
    10: proper(g(X)) -> g(proper(X))
    11: proper(d(X)) -> d(proper(X))
    12: proper(h(X)) -> h(proper(X))
    13: f(ok(X)) -> ok(f(X))
    14: c(ok(X)) -> ok(c(X))
    15: g(ok(X)) -> ok(g(X))
    16: d(ok(X)) -> ok(d(X))
    17: h(ok(X)) -> ok(h(X))
    18: top(mark(X)) -> top(proper(X))
    19: top(ok(X)) -> top(active(X))
Number of strict rules: 19
Direct Order(PosReal,>,Poly) ... removes: 3 19 17 13
     h(x1)	weight: (/ 1 16) + 2 * x1
     d(x1)	weight: x1
   top(x1)	weight: x1
     c(x1)	weight: x1
     f(x1)	weight: (/ 1 16) + 2 * x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 8) + 2 * x1
  mark(x1)	weight: x1
active(x1)	weight: x1
     g(x1)	weight: x1
Number of strict rules: 15
Direct Order(PosReal,>,Poly) ... removes: 4 16 5 14
     h(x1)	weight: (/ 1 16) + x1
     d(x1)	weight: 2 * x1
   top(x1)	weight: x1
     c(x1)	weight: 2 * x1
     f(x1)	weight: (/ 1 16) + x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 16) + x1
  mark(x1)	weight: x1
active(x1)	weight: 2 * x1
     g(x1)	weight: x1
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... removes: 1
     h(x1)	weight: (/ 1 16) + x1
     d(x1)	weight: x1
   top(x1)	weight: 2 * x1
     c(x1)	weight: x1
     f(x1)	weight: (/ 1 16) + x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 16) + x1
  mark(x1)	weight: x1
active(x1)	weight: 2 * x1
     g(x1)	weight: x1
Number of strict rules: 10
Direct Order(PosReal,>,Poly) ... removes: 2
     h(x1)	weight: (/ 1 16) + x1
     d(x1)	weight: x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 1 16) + x1
     f(x1)	weight: (/ 1 16) + x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 16) + x1
  mark(x1)	weight: x1
active(x1)	weight: x1
     g(x1)	weight: x1
Number of strict rules: 9
Direct Order(PosReal,>,Poly) ... removes: 15
     h(x1)	weight: (/ 1 16) + x1
     d(x1)	weight: x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 1 16) + x1
     f(x1)	weight: (/ 1 16) + x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 3 16) + x1
  mark(x1)	weight: x1
active(x1)	weight: (/ 1 16) + x1
     g(x1)	weight: (/ 565169 16) + 2 * x1
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... removes: 10 11
     h(x1)	weight: x1
     d(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: x1
     c(x1)	weight: x1
     f(x1)	weight: x1
proper(x1)	weight: 2 * x1
    ok(x1)	weight: (/ 1 2) + x1
  mark(x1)	weight: 2 * x1
active(x1)	weight: (/ 1 2) + x1
     g(x1)	weight: (/ 3 8) + x1
Number of strict rules: 6
Direct Order(PosReal,>,Poly) ... removes: 9
     h(x1)	weight: x1
     d(x1)	weight: (/ 1 16) + x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 1 16) + x1
     f(x1)	weight: x1
proper(x1)	weight: 2 * x1
    ok(x1)	weight: (/ 1 4) + x1
  mark(x1)	weight: 2 * x1
active(x1)	weight: (/ 1 4) + x1
     g(x1)	weight: (/ 3 32) + x1
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 18 6
     h(x1)	weight: (/ 1 16) + x1
     d(x1)	weight: (/ 1 16) + x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 1 16) + x1
     f(x1)	weight: (/ 1 16) + 2 * x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 227081 8) + x1
  mark(x1)	weight: (/ 454161 16) + x1
active(x1)	weight: (/ 227081 8) + x1
     g(x1)	weight: (/ 1 16) + x1
Number of strict rules: 3
Direct Order(PosReal,>,Poly) ... removes: 8 12
     h(x1)	weight: (/ 1 16) + x1
     d(x1)	weight: (/ 1 16) + x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 1 16) + x1
     f(x1)	weight: (/ 1 16) + x1
proper(x1)	weight: 2 * x1
    ok(x1)	weight: (/ 1 8) + x1
  mark(x1)	weight: (/ 1 16) + x1
active(x1)	weight: (/ 1 8) + x1
     g(x1)	weight: (/ 1 16) + x1
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 7
     h(x1)	weight: (/ 1 8) + 2 * x1
     d(x1)	weight: (/ 1 16) + x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 1 16) + x1
     f(x1)	weight: (/ 1 16) + x1
proper(x1)	weight: 2 * x1
    ok(x1)	weight: (/ 1 16) + x1
  mark(x1)	weight: (/ 1 16) + x1
active(x1)	weight: (/ 1 16) + x1
     g(x1)	weight: (/ 1 16) + x1
Number of strict rules: 0
YES