Input TRS:
    1: active(2nd(cons(X,cons(Y,Z)))) -> mark(Y)
    2: active(from(X)) -> mark(cons(X,from(s(X))))
    3: active(2nd(X)) -> 2nd(active(X))
    4: active(cons(X1,X2)) -> cons(active(X1),X2)
    5: active(from(X)) -> from(active(X))
    6: active(s(X)) -> s(active(X))
    7: 2nd(mark(X)) -> mark(2nd(X))
    8: cons(mark(X1),X2) -> mark(cons(X1,X2))
    9: from(mark(X)) -> mark(from(X))
    10: s(mark(X)) -> mark(s(X))
    11: proper(2nd(X)) -> 2nd(proper(X))
    12: proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
    13: proper(from(X)) -> from(proper(X))
    14: proper(s(X)) -> s(proper(X))
    15: 2nd(ok(X)) -> ok(2nd(X))
    16: cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    17: from(ok(X)) -> ok(from(X))
    18: s(ok(X)) -> ok(s(X))
    19: top(mark(X)) -> top(proper(X))
    20: top(ok(X)) -> top(active(X))
Number of strict rules: 20
Direct Order(PosReal,>,Poly) ... removes: 4 1 16 19 20 2
     s(x1)	weight: x1
   top(x1)	weight: x1
   2nd(x1)	weight: x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 4) + 2 * x1
  from(x1)	weight: x1
  mark(x1)	weight: (/ 1 16) + x1
active(x1)	weight: (/ 3 16) + 2 * x1
  cons(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 14
Direct Order(PosReal,>,Poly) ... removes: 18 10
     s(x1)	weight: 2 * x1
   top(x1)	weight: x1
   2nd(x1)	weight: x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 16) + x1
  from(x1)	weight: x1
  mark(x1)	weight: (/ 1 16) + x1
active(x1)	weight: 2 * x1
  cons(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 12
Direct Order(PosReal,>,Poly) ... removes: 17
     s(x1)	weight: x1
   top(x1)	weight: x1
   2nd(x1)	weight: x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 16) + x1
  from(x1)	weight: 2 * x1
  mark(x1)	weight: x1
active(x1)	weight: 2 * x1
  cons(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... removes: 14 12
     s(x1)	weight: (/ 1 16) + x1
   top(x1)	weight: x1
   2nd(x1)	weight: x1
proper(x1)	weight: 2 * x1
    ok(x1)	weight: (/ 1 16) + x1
  from(x1)	weight: x1
  mark(x1)	weight: x1
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 9
Direct Order(PosReal,>,Poly) ... removes: 6
     s(x1)	weight: (/ 1 16) + x1
   top(x1)	weight: x1
   2nd(x1)	weight: x1
proper(x1)	weight: 2 * x1
    ok(x1)	weight: (/ 1 16) + x1
  from(x1)	weight: x1
  mark(x1)	weight: x1
active(x1)	weight: 2 * x1
  cons(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... removes: 8
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: x1
   2nd(x1)	weight: x1
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: (/ 1 8) + x1
  from(x1)	weight: x1
  mark(x1)	weight: (/ 1 8) + x1
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 125017 8) + 2 * x1 + 2 * x2
Number of strict rules: 7
Direct Order(PosReal,>,Poly) ... removes: 7 9
     s(x1)	weight: (/ 1 8) + x1
   top(x1)	weight: x1
   2nd(x1)	weight: 2 * x1
proper(x1)	weight: x1
    ok(x1)	weight: x1
  from(x1)	weight: 2 * x1
  mark(x1)	weight: (/ 1 8) + x1
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 125017 8) + 2 * x1 + x2
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 13
     s(x1)	weight: (/ 1 32) + 2 * x1
   top(x1)	weight: x1
   2nd(x1)	weight: x1
proper(x1)	weight: (/ 1 32) + 2 * x1
    ok(x1)	weight: (/ 1 32) + x1
  from(x1)	weight: (/ 1 32) + x1
  mark(x1)	weight: (/ 1 32) + x1
active(x1)	weight: (/ 1 32) + x1
  cons(x1,x2)	weight: (/ 1 16) + 2 * x1 + x2
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... removes: 5
     s(x1)	weight: (/ 1 16) + 2 * x1
   top(x1)	weight: x1
   2nd(x1)	weight: x1
proper(x1)	weight: (/ 1 16) + x1
    ok(x1)	weight: (/ 1 8) + x1
  from(x1)	weight: (/ 3 16) + 2 * x1
  mark(x1)	weight: (/ 3 16) + x1
active(x1)	weight: (/ 1 8) + 2 * x1
  cons(x1,x2)	weight: (/ 1 16) + 2 * x1 + x2
Number of strict rules: 3
Direct Order(PosReal,>,Poly) ... removes: 15
     s(x1)	weight: (/ 1 16) + x1
   top(x1)	weight: x1
   2nd(x1)	weight: 2 * x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 16) + x1
  from(x1)	weight: (/ 1 16) + x1
  mark(x1)	weight: (/ 1 16) + x1
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 16) + 2 * x1 + x2
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... removes: 11
     s(x1)	weight: (/ 1 32) + x1
   top(x1)	weight: x1
   2nd(x1)	weight: (/ 1 32) + x1
proper(x1)	weight: (/ 1 32) + 2 * x1
    ok(x1)	weight: (/ 1 32) + x1
  from(x1)	weight: (/ 1 32) + 2 * x1
  mark(x1)	weight: (/ 1 32) + x1
active(x1)	weight: (/ 1 32) + x1
  cons(x1,x2)	weight: (/ 1 16) + 2 * x1 + x2
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 3
     s(x1)	weight: (/ 1 32) + x1
   top(x1)	weight: x1
   2nd(x1)	weight: (/ 1 32) + x1
proper(x1)	weight: (/ 1 32) + 2 * x1
    ok(x1)	weight: (/ 3 32) + x1
  from(x1)	weight: (/ 1 32) + 2 * x1
  mark(x1)	weight: (/ 1 32) + x1
active(x1)	weight: (/ 3 32) + 2 * x1
  cons(x1,x2)	weight: (/ 1 16) + 2 * x1 + x2
Number of strict rules: 0
YES