Input TRS:
    1: active(and(tt(),X)) -> mark(X)
    2: active(plus(N,0())) -> mark(N)
    3: active(plus(N,s(M))) -> mark(s(plus(N,M)))
    4: active(and(X1,X2)) -> and(active(X1),X2)
    5: active(plus(X1,X2)) -> plus(active(X1),X2)
    6: active(plus(X1,X2)) -> plus(X1,active(X2))
    7: active(s(X)) -> s(active(X))
    8: and(mark(X1),X2) -> mark(and(X1,X2))
    9: plus(mark(X1),X2) -> mark(plus(X1,X2))
    10: plus(X1,mark(X2)) -> mark(plus(X1,X2))
    11: s(mark(X)) -> mark(s(X))
    12: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
    13: proper(tt()) -> ok(tt())
    14: proper(plus(X1,X2)) -> plus(proper(X1),proper(X2))
    15: proper(0()) -> ok(0())
    16: proper(s(X)) -> s(proper(X))
    17: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
    18: plus(ok(X1),ok(X2)) -> ok(plus(X1,X2))
    19: s(ok(X)) -> ok(s(X))
    20: top(mark(X)) -> top(proper(X))
    21: top(ok(X)) -> top(active(X))
Number of strict rules: 21
Direct Order(PosReal,>,Poly) ... removes: 1 2
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 1 8) + x1 + x2
proper(x1)	weight: x1
    ok(x1)	weight: x1
     0()	weight: 0
  mark(x1)	weight: x1
  plus(x1,x2)	weight: (/ 1 8) + x1 + x2
active(x1)	weight: x1
    tt()	weight: 0
Number of strict rules: 19
Direct Order(PosReal,>,Poly) ... removes: 3 10 20
     s(x1)	weight: (/ 28195 2) + x1
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 121481 4) + x1 + x2
proper(x1)	weight: x1
    ok(x1)	weight: x1
     0()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
  plus(x1,x2)	weight: x1 + 2 * x2
active(x1)	weight: x1
    tt()	weight: 0
Number of strict rules: 16
Direct Order(PosReal,>,Poly) ... removes: 16
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: x1
   and(x1,x2)	weight: x1 + x2
proper(x1)	weight: 2 * x1
    ok(x1)	weight: x1
     0()	weight: 0
  mark(x1)	weight: (/ 1 8) + x1
  plus(x1,x2)	weight: x1 + 2 * x2
active(x1)	weight: x1
    tt()	weight: 0
Number of strict rules: 15
Direct Order(PosReal,>,Poly) ... removes: 8
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 1 8) + 2 * x1 + x2
proper(x1)	weight: x1
    ok(x1)	weight: x1
     0()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
  plus(x1,x2)	weight: x1 + x2
active(x1)	weight: x1
    tt()	weight: 0
Number of strict rules: 14
Direct Order(PosReal,>,Poly) ... removes: 11
     s(x1)	weight: (/ 1 8) + 2 * x1
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 1 8) + 2 * x1 + x2
proper(x1)	weight: x1
    ok(x1)	weight: x1
     0()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
  plus(x1,x2)	weight: x1 + x2
active(x1)	weight: x1
    tt()	weight: 0
Number of strict rules: 13
Direct Order(PosReal,>,Poly) ... removes: 15 13
     s(x1)	weight: (/ 1 8) + 2 * x1
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 1 4) + 2 * x1 + x2
proper(x1)	weight: (/ 1 8) + 2 * x1
    ok(x1)	weight: x1
     0()	weight: 0
  mark(x1)	weight: (/ 3 8) + x1
  plus(x1,x2)	weight: (/ 1 8) + x1 + x2
active(x1)	weight: x1
    tt()	weight: 0
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... removes: 14 12
     s(x1)	weight: (/ 1 8) + 2 * x1
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 1 4) + x1 + x2
proper(x1)	weight: (/ 1 8) + 2 * x1
    ok(x1)	weight: x1
     0()	weight: 0
  mark(x1)	weight: (/ 3 8) + x1
  plus(x1,x2)	weight: (/ 1 4) + x1 + x2
active(x1)	weight: x1
    tt()	weight: 0
Number of strict rules: 9
Direct Order(PosReal,>,Poly) ... removes: 9
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 1 8) + x1 + x2
proper(x1)	weight: (/ 1 8) + 2 * x1
    ok(x1)	weight: x1
     0()	weight: 0
  mark(x1)	weight: (/ 3 8) + x1
  plus(x1,x2)	weight: (/ 1 4) + 2 * x1 + x2
active(x1)	weight: x1
    tt()	weight: 0
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... removes: 18 4 21 19 17 5 7 6
     s(x1)	weight: (/ 1 16) + 2 * x1
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 1 16) + 2 * x1 + x2
proper(x1)	weight: (/ 1 32) + 2 * x1
    ok(x1)	weight: (/ 862467 32) + 2 * x1
     0()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
  plus(x1,x2)	weight: (/ 3 32) + 2 * x1 + 2 * x2
active(x1)	weight: (/ 1 32) + 2 * x1
    tt()	weight: 0
Number of strict rules: 0
YES