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: 18 1 3 19 2
     h(x1)	weight: x1
     d(x1)	weight: (/ 1 16) + x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 213169 16) + x1
     f(x1)	weight: (/ 1 16) + x1
proper(x1)	weight: (/ 1 16) + x1
    ok(x1)	weight: (/ 106587 8) + x1
  mark(x1)	weight: (/ 1 8) + x1
active(x1)	weight: (/ 213173 16) + x1
     g(x1)	weight: (/ 1 16) + x1
Number of strict rules: 14
Direct Order(PosReal,>,Poly) ... removes: 16
     h(x1)	weight: x1
     d(x1)	weight: (/ 1 8) + 2 * x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 1 8) + x1
     f(x1)	weight: (/ 291289 8) + x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 3 8) + x1
  mark(x1)	weight: (/ 1 8) + x1
active(x1)	weight: (/ 3 8) + x1
     g(x1)	weight: (/ 1 8) + x1
Number of strict rules: 13
Direct Order(PosReal,>,Poly) ... removes: 15
     h(x1)	weight: x1
     d(x1)	weight: (/ 1 4) + 2 * x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 124445 4) + x1
     f(x1)	weight: (/ 145645 4) + x1
proper(x1)	weight: x1
    ok(x1)	weight: 92167 + x1
  mark(x1)	weight: (/ 1 4) + x1
active(x1)	weight: 92167 + x1
     g(x1)	weight: (/ 98577 4) + 2 * x1
Number of strict rules: 12
Direct Order(PosReal,>,Poly) ... removes: 8 10 12 11 9
     h(x1)	weight: (/ 1 16) + x1
     d(x1)	weight: (/ 1 16) + x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 364065 16) + x1
     f(x1)	weight: (/ 1 16) + x1
proper(x1)	weight: 2 * x1
    ok(x1)	weight: (/ 91017 4) + x1
  mark(x1)	weight: (/ 1 16) + x1
active(x1)	weight: (/ 91017 4) + x1
     g(x1)	weight: (/ 1 16) + 2 * x1
Number of strict rules: 7
Direct Order(PosReal,>,Poly) ... removes: 13 6
     h(x1)	weight: 11197 + x1
     d(x1)	weight: (/ 1 4) + x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 11197 2) + x1
     f(x1)	weight: (/ 155477 4) + 2 * x1
proper(x1)	weight: 2 * x1
    ok(x1)	weight: (/ 52853 4) + x1
  mark(x1)	weight: (/ 22393 4) + x1
active(x1)	weight: x1
     g(x1)	weight: (/ 1 4) + 2 * x1
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 14
     h(x1)	weight: (/ 5 16) + x1
     d(x1)	weight: (/ 1 16) + x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 1 8) + 2 * x1
     f(x1)	weight: (/ 317201 16) + 2 * x1
proper(x1)	weight: 2 * x1
    ok(x1)	weight: (/ 211409 16) + x1
  mark(x1)	weight: (/ 1 16) + x1
active(x1)	weight: x1
     g(x1)	weight: (/ 1 16) + 2 * x1
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... removes: 17 7
     h(x1)	weight: (/ 1 32) + 2 * x1
     d(x1)	weight: (/ 1 32) + x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 1 32) + 2 * x1
     f(x1)	weight: (/ 1 32) + 2 * x1
proper(x1)	weight: 2 * x1
    ok(x1)	weight: (/ 422817 32) + x1
  mark(x1)	weight: (/ 1 16) + 2 * x1
active(x1)	weight: x1
     g(x1)	weight: (/ 1 32) + 2 * x1
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... removes: 4 5
     h(x1)	weight: (/ 1 32) + 2 * x1
     d(x1)	weight: (/ 1 32) + x1
   top(x1)	weight: x1
     c(x1)	weight: (/ 1 32) + 2 * x1
     f(x1)	weight: (/ 1 32) + x1
proper(x1)	weight: 2 * x1
    ok(x1)	weight: (/ 422817 32) + x1
  mark(x1)	weight: (/ 1 32) + 2 * x1
active(x1)	weight: 2 * x1
     g(x1)	weight: (/ 1 32) + 2 * x1
Number of strict rules: 0
YES