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