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: 17 9
     s(x1)	weight: x1
   top(x1)	weight: x1
 |2nd|(x1)	weight: x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 47277 4) + 2 * x1
  from(x1)	weight: 2 * x1
  mark(x1)	weight: (/ 1 4) + x1
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 23639 2) + x1 + x2
Number of strict rules: 12
Direct Order(PosReal,>,Poly) ... removes: 8
     s(x1)	weight: x1
   top(x1)	weight: x1
 |2nd|(x1)	weight: x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 16) + 2 * x1
  from(x1)	weight: 2 * x1
  mark(x1)	weight: (/ 1 16) + x1
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 3 16) + 2 * x1 + x2
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... removes: 5
     s(x1)	weight: x1
   top(x1)	weight: x1
 |2nd|(x1)	weight: x1
proper(x1)	weight: x1
    ok(x1)	weight: (/ 1 32) + 2 * x1
  from(x1)	weight: (/ 1 32) + x1
  mark(x1)	weight: (/ 1 32) + x1
active(x1)	weight: 2 * x1
  cons(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 10
Direct Order(PosReal,>,Poly) ... removes: 10
     s(x1)	weight: 2 * x1
   top(x1)	weight: x1
 |2nd|(x1)	weight: x1
proper(x1)	weight: x1
    ok(x1)	weight: 2 * x1
  from(x1)	weight: (/ 1 16) + x1
  mark(x1)	weight: (/ 1 16) + x1
active(x1)	weight: 2 * x1
  cons(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 9
Direct Order(PosReal,>,Poly) ... removes: 15
     s(x1)	weight: 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: x1
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... removes: 12
     s(x1)	weight: x1
   top(x1)	weight: x1
 |2nd|(x1)	weight: 2 * 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: 7
Direct Order(PosReal,>,Poly) ... removes: 13
     s(x1)	weight: x1
   top(x1)	weight: x1
 |2nd|(x1)	weight: 2 * x1
proper(x1)	weight: 2 * x1
    ok(x1)	weight: (/ 1 16) + x1
  from(x1)	weight: (/ 1 16) + x1
  mark(x1)	weight: x1
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 6
Direct Order(PosReal,>,Poly) ... removes: 18
     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: x1
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... removes: 7
     s(x1)	weight: x1
   top(x1)	weight: x1
 |2nd|(x1)	weight: 2 * x1
proper(x1)	weight: x1
    ok(x1)	weight: x1
  from(x1)	weight: (/ 1 16) + x1
  mark(x1)	weight: (/ 5 16) + x1
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... removes: 14
     s(x1)	weight: (/ 1 8) + 2 * x1
   top(x1)	weight: x1
 |2nd|(x1)	weight: x1
proper(x1)	weight: (/ 1 16) + 2 * x1
    ok(x1)	weight: (/ 1 16) + x1
  from(x1)	weight: (/ 1 16) + x1
  mark(x1)	weight: (/ 3 16) + x1
active(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 3
Direct Order(PosReal,>,Poly) ... removes: 6
     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 16) + x1
  from(x1)	weight: (/ 1 16) + x1
  mark(x1)	weight: (/ 5 16) + x1
active(x1)	weight: 2 * x1
  cons(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... removes: 11
     s(x1)	weight: (/ 1 8) + 2 * x1
   top(x1)	weight: x1
 |2nd|(x1)	weight: (/ 1 8) + x1
proper(x1)	weight: (/ 1 4) + 2 * x1
    ok(x1)	weight: (/ 1 8) + x1
  from(x1)	weight: 2 * x1
  mark(x1)	weight: (/ 5 8) + x1
active(x1)	weight: (/ 1 8) + x1
  cons(x1,x2)	weight: (/ 1 8) + x1 + x2
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 3
     s(x1)	weight: (/ 1 8) + 2 * x1
   top(x1)	weight: x1
 |2nd|(x1)	weight: (/ 192521 8) + x1
proper(x1)	weight: (/ 1 4) + 2 * x1
    ok(x1)	weight: (/ 1 4) + x1
  from(x1)	weight: 2 * x1
  mark(x1)	weight: (/ 385049 8) + x1
active(x1)	weight: (/ 1 4) + 2 * x1
  cons(x1,x2)	weight: (/ 1 8) + x1 + x2
Number of strict rules: 0
YES