Input TRS:
    1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
    2: active(__(X,nil())) -> mark(X)
    3: active(__(nil(),X)) -> mark(X)
    4: active(and(tt(),X)) -> mark(X)
    5: active(isList(V)) -> mark(isNeList(V))
    6: active(isList(nil())) -> mark(tt())
    7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
    8: active(isNeList(V)) -> mark(isQid(V))
    9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
    10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
    11: active(isNePal(V)) -> mark(isQid(V))
    12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
    13: active(isPal(V)) -> mark(isNePal(V))
    14: active(isPal(nil())) -> mark(tt())
    15: active(isQid(a())) -> mark(tt())
    16: active(isQid(e())) -> mark(tt())
    17: active(isQid(i())) -> mark(tt())
    18: active(isQid(o())) -> mark(tt())
    19: active(isQid(u())) -> mark(tt())
    20: active(__(X1,X2)) -> __(active(X1),X2)
    21: active(__(X1,X2)) -> __(X1,active(X2))
    22: active(and(X1,X2)) -> and(active(X1),X2)
    23: __(mark(X1),X2) -> mark(__(X1,X2))
    24: __(X1,mark(X2)) -> mark(__(X1,X2))
    25: and(mark(X1),X2) -> mark(and(X1,X2))
    26: proper(__(X1,X2)) -> __(proper(X1),proper(X2))
    27: proper(nil()) -> ok(nil())
    28: proper(and(X1,X2)) -> and(proper(X1),proper(X2))
    29: proper(tt()) -> ok(tt())
    30: proper(isList(X)) -> isList(proper(X))
    31: proper(isNeList(X)) -> isNeList(proper(X))
    32: proper(isQid(X)) -> isQid(proper(X))
    33: proper(isNePal(X)) -> isNePal(proper(X))
    34: proper(isPal(X)) -> isPal(proper(X))
    35: proper(a()) -> ok(a())
    36: proper(e()) -> ok(e())
    37: proper(i()) -> ok(i())
    38: proper(o()) -> ok(o())
    39: proper(u()) -> ok(u())
    40: __(ok(X1),ok(X2)) -> ok(__(X1,X2))
    41: and(ok(X1),ok(X2)) -> ok(and(X1,X2))
    42: isList(ok(X)) -> ok(isList(X))
    43: isNeList(ok(X)) -> ok(isNeList(X))
    44: isQid(ok(X)) -> ok(isQid(X))
    45: isNePal(ok(X)) -> ok(isNePal(X))
    46: isPal(ok(X)) -> ok(isPal(X))
    47: top(mark(X)) -> top(proper(X))
    48: top(ok(X)) -> top(active(X))
Number of strict rules: 48
Direct Order(PosReal,>,Poly) ... removes: 18 4 15 8 3 16 19 17 5 10 7 14 12 11 9 13 6 2
     a()	weight: 0
isNeList(x1)	weight: (/ 1 4) + x1
 isPal(x1)	weight: (/ 22435 8) + x1
     u()	weight: 0
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 1 8) + x1 + x2
isNePal(x1)	weight: (/ 11217 4) + x1
 isQid(x1)	weight: (/ 1 8) + x1
     o()	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: x1
isList(x1)	weight: (/ 231499 8) + x1
   nil()	weight: 0
  mark(x1)	weight: x1
     i()	weight: 0
     e()	weight: 0
active(x1)	weight: x1
    tt()	weight: 0
    __(x1,x2)	weight: (/ 231501 8) + x1 + x2
Number of strict rules: 30
Direct Order(PosReal,>,Poly) ... removes: 1
     a()	weight: 0
isNeList(x1)	weight: (/ 1 16) + x1
 isPal(x1)	weight: (/ 1 16) + x1
     u()	weight: 0
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 1 16) + x1 + x2
isNePal(x1)	weight: (/ 1 16) + x1
 isQid(x1)	weight: (/ 1 16) + x1
     o()	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: x1
isList(x1)	weight: (/ 1 16) + x1
   nil()	weight: 0
  mark(x1)	weight: x1
     i()	weight: 0
     e()	weight: 0
active(x1)	weight: x1
    tt()	weight: 0
    __(x1,x2)	weight: (/ 1 8) + 2 * x1 + x2
Number of strict rules: 29
Direct Order(PosReal,>,Poly) ... removes: 23 47
     a()	weight: 0
isNeList(x1)	weight: x1
 isPal(x1)	weight: (/ 3 64) + x1
     u()	weight: 0
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 1 32) + x1 + x2
isNePal(x1)	weight: x1
 isQid(x1)	weight: x1
     o()	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: x1
isList(x1)	weight: x1
   nil()	weight: 0
  mark(x1)	weight: (/ 3 64) + x1
     i()	weight: 0
     e()	weight: 0
active(x1)	weight: x1
    tt()	weight: 0
    __(x1,x2)	weight: (/ 1 16) + 2 * x1 + x2
Number of strict rules: 27
Direct Order(PosReal,>,Poly) ... removes: 26
     a()	weight: 0
isNeList(x1)	weight: x1
 isPal(x1)	weight: x1
     u()	weight: 0
   top(x1)	weight: x1
   and(x1,x2)	weight: x1 + x2
isNePal(x1)	weight: x1
 isQid(x1)	weight: x1
     o()	weight: 0
proper(x1)	weight: 2 * x1
    ok(x1)	weight: x1
isList(x1)	weight: x1
   nil()	weight: 0
  mark(x1)	weight: (/ 1 16) + x1
     i()	weight: 0
     e()	weight: 0
active(x1)	weight: x1
    tt()	weight: 0
    __(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 26
Direct Order(PosReal,>,Poly) ... removes: 32 34 33 30 31
     a()	weight: 0
isNeList(x1)	weight: (/ 1 32) + x1
 isPal(x1)	weight: (/ 1 32) + x1
     u()	weight: 0
   top(x1)	weight: x1
   and(x1,x2)	weight: x1 + x2
isNePal(x1)	weight: (/ 1 32) + x1
 isQid(x1)	weight: (/ 1 32) + x1
     o()	weight: 0
proper(x1)	weight: 2 * x1
    ok(x1)	weight: x1
isList(x1)	weight: (/ 1 32) + x1
   nil()	weight: 0
  mark(x1)	weight: (/ 5 32) + x1
     i()	weight: 0
     e()	weight: 0
active(x1)	weight: x1
    tt()	weight: 0
    __(x1,x2)	weight: (/ 1 8) + x1 + x2
Number of strict rules: 21
Direct Order(PosReal,>,Poly) ... removes: 24
     a()	weight: 0
isNeList(x1)	weight: (/ 1 32) + x1
 isPal(x1)	weight: (/ 1 32) + x1
     u()	weight: 0
   top(x1)	weight: x1
   and(x1,x2)	weight: x1 + x2
isNePal(x1)	weight: (/ 1 32) + x1
 isQid(x1)	weight: (/ 1 32) + x1
     o()	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: x1
isList(x1)	weight: (/ 1 32) + x1
   nil()	weight: 0
  mark(x1)	weight: (/ 5 32) + x1
     i()	weight: 0
     e()	weight: 0
active(x1)	weight: x1
    tt()	weight: 0
    __(x1,x2)	weight: (/ 1 8) + x1 + 2 * x2
Number of strict rules: 20
Direct Order(PosReal,>,Poly) ... removes: 28
     a()	weight: 0
isNeList(x1)	weight: (/ 1 16) + x1
 isPal(x1)	weight: (/ 1 16) + x1
     u()	weight: 0
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 1 16) + x1 + x2
isNePal(x1)	weight: (/ 1 16) + x1
 isQid(x1)	weight: (/ 1 16) + x1
     o()	weight: 0
proper(x1)	weight: 2 * x1
    ok(x1)	weight: x1
isList(x1)	weight: (/ 1 16) + x1
   nil()	weight: 0
  mark(x1)	weight: (/ 1 8) + x1
     i()	weight: 0
     e()	weight: 0
active(x1)	weight: x1
    tt()	weight: 0
    __(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 19
Direct Order(PosReal,>,Poly) ... removes: 36 27 39 38 37 35 29
     a()	weight: 0
isNeList(x1)	weight: x1
 isPal(x1)	weight: (/ 1 8) + x1
     u()	weight: 0
   top(x1)	weight: x1
   and(x1,x2)	weight: x1 + x2
isNePal(x1)	weight: (/ 1 8) + x1
 isQid(x1)	weight: (/ 1 8) + x1
     o()	weight: 0
proper(x1)	weight: (/ 1 8) + x1
    ok(x1)	weight: x1
isList(x1)	weight: (/ 1 8) + x1
   nil()	weight: 0
  mark(x1)	weight: (/ 1 4) + x1
     i()	weight: 0
     e()	weight: 0
active(x1)	weight: x1
    tt()	weight: 0
    __(x1,x2)	weight: (/ 1 8) + x1 + x2
Number of strict rules: 12
Direct Order(PosReal,>,Poly) ... removes: 25
     a()	weight: 0
isNeList(x1)	weight: x1
 isPal(x1)	weight: x1
     u()	weight: 0
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 1 16) + 2 * x1 + x2
isNePal(x1)	weight: x1
 isQid(x1)	weight: x1
     o()	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: x1
isList(x1)	weight: x1
   nil()	weight: 0
  mark(x1)	weight: (/ 1 8) + x1
     i()	weight: 0
     e()	weight: 0
active(x1)	weight: x1
    tt()	weight: 0
    __(x1,x2)	weight: (/ 1 16) + x1 + x2
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... removes: 21 22 44 20 45 40 48 41 42 46 43
     a()	weight: 0
isNeList(x1)	weight: (/ 1 8) + 2 * x1
 isPal(x1)	weight: 2 * x1
     u()	weight: 0
   top(x1)	weight: x1
   and(x1,x2)	weight: (/ 1 4) + 2 * x1 + 2 * x2
isNePal(x1)	weight: (/ 150713 8) + 2 * x1
 isQid(x1)	weight: (/ 113653 4) + 2 * x1
     o()	weight: 0
proper(x1)	weight: x1
    ok(x1)	weight: (/ 227307 8) + 2 * x1
isList(x1)	weight: (/ 101041 8) + 2 * x1
   nil()	weight: 0
  mark(x1)	weight: (/ 227307 4) + x1
     i()	weight: 0
     e()	weight: 0
active(x1)	weight: (/ 1 8) + 2 * x1
    tt()	weight: 0
    __(x1,x2)	weight: (/ 25325 4) + 2 * x1 + 2 * x2
Number of strict rules: 0
YES