Input TRS:
    1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
    2: a____(X,nil()) -> mark(X)
    3: a____(nil(),X) -> mark(X)
    4: a__U11(tt()) -> tt()
    5: a__U21(tt(),V2) -> a__U22(a__isList(V2))
    6: a__U22(tt()) -> tt()
    7: a__U31(tt()) -> tt()
    8: a__U41(tt(),V2) -> a__U42(a__isNeList(V2))
    9: a__U42(tt()) -> tt()
    10: a__U51(tt(),V2) -> a__U52(a__isList(V2))
    11: a__U52(tt()) -> tt()
    12: a__U61(tt()) -> tt()
    13: a__U71(tt(),P) -> a__U72(a__isPal(P))
    14: a__U72(tt()) -> tt()
    15: a__U81(tt()) -> tt()
    16: a__isList(V) -> a__U11(a__isNeList(V))
    17: a__isList(nil()) -> tt()
    18: a__isList(__(V1,V2)) -> a__U21(a__isList(V1),V2)
    19: a__isNeList(V) -> a__U31(a__isQid(V))
    20: a__isNeList(__(V1,V2)) -> a__U41(a__isList(V1),V2)
    21: a__isNeList(__(V1,V2)) -> a__U51(a__isNeList(V1),V2)
    22: a__isNePal(V) -> a__U61(a__isQid(V))
    23: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),P)
    24: a__isPal(V) -> a__U81(a__isNePal(V))
    25: a__isPal(nil()) -> tt()
    26: a__isQid(a()) -> tt()
    27: a__isQid(e()) -> tt()
    28: a__isQid(i()) -> tt()
    29: a__isQid(o()) -> tt()
    30: a__isQid(u()) -> tt()
    31: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
    32: mark(U11(X)) -> a__U11(mark(X))
    33: mark(U21(X1,X2)) -> a__U21(mark(X1),X2)
    34: mark(U22(X)) -> a__U22(mark(X))
    35: mark(isList(X)) -> a__isList(X)
    36: mark(U31(X)) -> a__U31(mark(X))
    37: mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
    38: mark(U42(X)) -> a__U42(mark(X))
    39: mark(isNeList(X)) -> a__isNeList(X)
    40: mark(U51(X1,X2)) -> a__U51(mark(X1),X2)
    41: mark(U52(X)) -> a__U52(mark(X))
    42: mark(U61(X)) -> a__U61(mark(X))
    43: mark(U71(X1,X2)) -> a__U71(mark(X1),X2)
    44: mark(U72(X)) -> a__U72(mark(X))
    45: mark(isPal(X)) -> a__isPal(X)
    46: mark(U81(X)) -> a__U81(mark(X))
    47: mark(isQid(X)) -> a__isQid(X)
    48: mark(isNePal(X)) -> a__isNePal(X)
    49: mark(nil()) -> nil()
    50: mark(tt()) -> tt()
    51: mark(a()) -> a()
    52: mark(e()) -> e()
    53: mark(i()) -> i()
    54: mark(o()) -> o()
    55: mark(u()) -> u()
    56: a____(X1,X2) -> __(X1,X2)
    57: a__U11(X) -> U11(X)
    58: a__U21(X1,X2) -> U21(X1,X2)
    59: a__U22(X) -> U22(X)
    60: a__isList(X) -> isList(X)
    61: a__U31(X) -> U31(X)
    62: a__U41(X1,X2) -> U41(X1,X2)
    63: a__U42(X) -> U42(X)
    64: a__isNeList(X) -> isNeList(X)
    65: a__U51(X1,X2) -> U51(X1,X2)
    66: a__U52(X) -> U52(X)
    67: a__U61(X) -> U61(X)
    68: a__U71(X1,X2) -> U71(X1,X2)
    69: a__U72(X) -> U72(X)
    70: a__isPal(X) -> isPal(X)
    71: a__U81(X) -> U81(X)
    72: a__isQid(X) -> isQid(X)
    73: a__isNePal(X) -> isNePal(X)
Number of strict rules: 73
Direct Order(PosReal,>,Poly) ... removes: 18 4 15 8 1 3 16 21 26 17 27 28 5 10 7 20 25 30 14 12 23 24 11 9 13 6 29 2
     a()	weight: 0
   U21(x1,x2)	weight: (/ 3 16) + x1 + x2
   U11(x1)	weight: (/ 1 32) + x1
isNeList(x1)	weight: (/ 1 16) + x1
 isPal(x1)	weight: (/ 3 16) + 2 * x1
   U42(x1)	weight: (/ 1 32) + x1
     u()	weight: 0
   U71(x1,x2)	weight: (/ 1 4) + x1 + 2 * x2
a__U22(x1)	weight: (/ 1 32) + x1
isNePal(x1)	weight: (/ 1 16) + x1
   U72(x1)	weight: (/ 1 32) + x1
a__U31(x1)	weight: (/ 1 32) + x1
a__U51(x1,x2)	weight: (/ 3 16) + x1 + x2
a__U81(x1)	weight: (/ 1 32) + 2 * x1
 isQid(x1)	weight: (/ 1 32) + x1
 a____(x1,x2)	weight: (/ 7 32) + 2 * x1 + x2
a__U41(x1,x2)	weight: (/ 1 8) + x1 + x2
a__isList(x1)	weight: (/ 1 8) + x1
a__isNeList(x1)	weight: (/ 1 16) + x1
     o()	weight: 0
isList(x1)	weight: (/ 1 8) + x1
a__U21(x1,x2)	weight: (/ 3 16) + x1 + x2
   nil()	weight: 0
  mark(x1)	weight: x1
a__U72(x1)	weight: (/ 1 32) + x1
a__isNePal(x1)	weight: (/ 1 16) + x1
a__U11(x1)	weight: (/ 1 32) + x1
a__U42(x1)	weight: (/ 1 32) + x1
a__U52(x1)	weight: (/ 1 32) + x1
     i()	weight: 0
   U52(x1)	weight: (/ 1 32) + x1
   U61(x1)	weight: (/ 1 32) + x1
     e()	weight: 0
   U31(x1)	weight: (/ 1 32) + x1
a__U71(x1,x2)	weight: (/ 1 4) + x1 + 2 * x2
a__isPal(x1)	weight: (/ 3 16) + 2 * x1
a__U61(x1)	weight: (/ 1 32) + x1
   U81(x1)	weight: (/ 1 32) + 2 * x1
    tt()	weight: 0
a__isQid(x1)	weight: (/ 1 32) + x1
   U22(x1)	weight: (/ 1 32) + x1
   U51(x1,x2)	weight: (/ 3 16) + x1 + x2
   U41(x1,x2)	weight: (/ 1 8) + x1 + x2
    __(x1,x2)	weight: (/ 7 32) + 2 * x1 + x2
Number of strict rules: 45
Direct Order(PosReal,>,Poly) ... removes: 19 22
     a()	weight: 0
   U21(x1,x2)	weight: (/ 7 32) + x1 + x2
   U11(x1)	weight: (/ 1 32) + x1
isNeList(x1)	weight: (/ 3 32) + x1
 isPal(x1)	weight: (/ 1 4) + 2 * x1
   U42(x1)	weight: (/ 1 32) + x1
     u()	weight: 0
   U71(x1,x2)	weight: (/ 5 16) + x1 + 2 * x2
a__U22(x1)	weight: (/ 1 32) + x1
isNePal(x1)	weight: (/ 3 32) + x1
   U72(x1)	weight: (/ 1 32) + x1
a__U31(x1)	weight: (/ 1 32) + x1
a__U51(x1,x2)	weight: (/ 7 32) + x1 + x2
a__U81(x1)	weight: (/ 1 32) + 2 * x1
 isQid(x1)	weight: (/ 1 32) + x1
 a____(x1,x2)	weight: (/ 7 32) + 2 * x1 + x2
a__U41(x1,x2)	weight: (/ 1 8) + x1 + x2
a__isList(x1)	weight: (/ 5 32) + x1
a__isNeList(x1)	weight: (/ 3 32) + x1
     o()	weight: 0
isList(x1)	weight: (/ 5 32) + x1
a__U21(x1,x2)	weight: (/ 7 32) + x1 + x2
   nil()	weight: 0
  mark(x1)	weight: x1
a__U72(x1)	weight: (/ 1 32) + x1
a__isNePal(x1)	weight: (/ 3 32) + x1
a__U11(x1)	weight: (/ 1 32) + x1
a__U42(x1)	weight: (/ 1 32) + x1
a__U52(x1)	weight: (/ 1 32) + x1
     i()	weight: 0
   U52(x1)	weight: (/ 1 32) + x1
   U61(x1)	weight: (/ 1 32) + x1
     e()	weight: 0
   U31(x1)	weight: (/ 1 32) + x1
a__U71(x1,x2)	weight: (/ 5 16) + x1 + 2 * x2
a__isPal(x1)	weight: (/ 1 4) + 2 * x1
a__U61(x1)	weight: (/ 1 32) + x1
   U81(x1)	weight: (/ 1 32) + 2 * x1
    tt()	weight: 0
a__isQid(x1)	weight: (/ 1 32) + x1
   U22(x1)	weight: (/ 1 32) + x1
   U51(x1,x2)	weight: (/ 7 32) + x1 + x2
   U41(x1,x2)	weight: (/ 1 8) + x1 + x2
    __(x1,x2)	weight: (/ 7 32) + 2 * x1 + x2
Number of strict rules: 43
Direct Order(PosReal,>,Poly) ... removes: 68 63 60 65 72 64 39 62 56 69 57 67 59 61 48 71 47 73 66 35
     a()	weight: 0
   U21(x1,x2)	weight: x1 + x2
   U11(x1)	weight: (/ 1 16) + 2 * x1
isNeList(x1)	weight: (/ 1 4) + x1
 isPal(x1)	weight: 2 * x1
   U42(x1)	weight: (/ 1 16) + x1
     u()	weight: 0
   U71(x1,x2)	weight: (/ 3 32) + x1 + 2 * x2
a__U22(x1)	weight: (/ 1 8) + x1
isNePal(x1)	weight: (/ 438003 16) + x1
   U72(x1)	weight: (/ 1 16) + x1
a__U31(x1)	weight: (/ 1 8) + x1
a__U51(x1,x2)	weight: (/ 7 8) + x1 + x2
a__U81(x1)	weight: (/ 1 8) + x1
 isQid(x1)	weight: (/ 1 8) + x1
 a____(x1,x2)	weight: (/ 7 4) + x1 + x2
a__U41(x1,x2)	weight: (/ 7 16) + x1 + x2
a__isList(x1)	weight: (/ 3 4) + x1
a__isNeList(x1)	weight: (/ 5 16) + x1
     o()	weight: 0
isList(x1)	weight: (/ 13 32) + x1
a__U21(x1,x2)	weight: x1 + x2
   nil()	weight: 0
  mark(x1)	weight: 2 * x1
a__U72(x1)	weight: (/ 1 8) + x1
a__isNePal(x1)	weight: (/ 876005 16) + x1
a__U11(x1)	weight: (/ 1 8) + 2 * x1
a__U42(x1)	weight: (/ 1 8) + x1
a__U52(x1)	weight: (/ 1 8) + x1
     i()	weight: 0
   U52(x1)	weight: (/ 1 16) + x1
   U61(x1)	weight: (/ 438001 16) + x1
     e()	weight: 0
   U31(x1)	weight: (/ 1 16) + x1
a__U71(x1,x2)	weight: (/ 3 16) + x1 + 2 * x2
a__isPal(x1)	weight: 2 * x1
a__U61(x1)	weight: (/ 438001 8) + x1
   U81(x1)	weight: (/ 1 16) + x1
    tt()	weight: 0
a__isQid(x1)	weight: (/ 3 16) + x1
   U22(x1)	weight: (/ 1 16) + x1
   U51(x1,x2)	weight: (/ 7 16) + x1 + x2
   U41(x1,x2)	weight: (/ 7 32) + x1 + x2
    __(x1,x2)	weight: (/ 7 8) + x1 + x2
Number of strict rules: 23
Direct Order(PosReal,>,Poly) ... removes: 36 32 34 44 31 40 38 37 41 42 46 43
     a()	weight: 0
   U21(x1,x2)	weight: x1 + x2
   U11(x1)	weight: (/ 1 16) + 2 * x1
isNeList(x1)	weight: (/ 3 16) + x1
 isPal(x1)	weight: 2 * x1
   U42(x1)	weight: (/ 1 16) + x1
     u()	weight: 0
   U71(x1,x2)	weight: (/ 3 32) + x1 + 2 * x2
a__U22(x1)	weight: (/ 1 16) + x1
isNePal(x1)	weight: (/ 876005 32) + x1
   U72(x1)	weight: (/ 1 16) + 2 * x1
a__U31(x1)	weight: (/ 1 16) + x1
a__U51(x1,x2)	weight: (/ 5 8) + x1 + x2
a__U81(x1)	weight: (/ 1 16) + x1
 isQid(x1)	weight: (/ 1 8) + x1
 a____(x1,x2)	weight: (/ 19 16) + x1 + x2
a__U41(x1,x2)	weight: (/ 5 16) + x1 + x2
a__isList(x1)	weight: (/ 9 16) + x1
a__isNeList(x1)	weight: (/ 1 4) + x1
     o()	weight: 0
isList(x1)	weight: (/ 5 16) + x1
a__U21(x1,x2)	weight: x1 + x2
   nil()	weight: 0
  mark(x1)	weight: 2 * x1
a__U72(x1)	weight: (/ 1 16) + x1
a__isNePal(x1)	weight: (/ 219001 4) + x1
a__U11(x1)	weight: (/ 1 16) + 2 * x1
a__U42(x1)	weight: (/ 1 16) + x1
a__U52(x1)	weight: (/ 1 16) + x1
     i()	weight: 0
   U52(x1)	weight: (/ 1 16) + x1
   U61(x1)	weight: (/ 438001 16) + x1
     e()	weight: 0
   U31(x1)	weight: (/ 1 16) + x1
a__U71(x1,x2)	weight: (/ 1 8) + x1 + 2 * x2
a__isPal(x1)	weight: 2 * x1
a__U61(x1)	weight: (/ 876001 16) + x1
   U81(x1)	weight: (/ 1 16) + x1
    tt()	weight: 0
a__isQid(x1)	weight: (/ 3 16) + x1
   U22(x1)	weight: (/ 1 16) + x1
   U51(x1,x2)	weight: (/ 11 32) + x1 + x2
   U41(x1,x2)	weight: (/ 3 16) + x1 + x2
    __(x1,x2)	weight: (/ 5 8) + x1 + x2
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... removes: 45 70
     a()	weight: 0
   U21(x1,x2)	weight: x1 + x2
   U11(x1)	weight: (/ 1 16) + 2 * x1
isNeList(x1)	weight: (/ 1 16) + x1
 isPal(x1)	weight: (/ 1 8) + 2 * x1
   U42(x1)	weight: (/ 1 16) + x1
     u()	weight: 0
   U71(x1,x2)	weight: (/ 5 32) + x1 + 2 * x2
a__U22(x1)	weight: (/ 1 16) + x1
isNePal(x1)	weight: (/ 1 8) + x1
   U72(x1)	weight: (/ 1 16) + 2 * x1
a__U31(x1)	weight: (/ 1 16) + x1
a__U51(x1,x2)	weight: (/ 3 8) + x1 + x2
a__U81(x1)	weight: (/ 1 16) + x1
 isQid(x1)	weight: (/ 1 16) + x1
 a____(x1,x2)	weight: (/ 3 4) + x1 + x2
a__U41(x1,x2)	weight: (/ 3 16) + x1 + x2
a__isList(x1)	weight: (/ 5 16) + x1
a__isNeList(x1)	weight: (/ 1 8) + x1
     o()	weight: 0
isList(x1)	weight: (/ 5 32) + x1
a__U21(x1,x2)	weight: x1 + x2
   nil()	weight: 0
  mark(x1)	weight: 2 * x1
a__U72(x1)	weight: (/ 1 16) + x1
a__isNePal(x1)	weight: (/ 3 16) + x1
a__U11(x1)	weight: (/ 1 16) + 2 * x1
a__U42(x1)	weight: (/ 1 16) + x1
a__U52(x1)	weight: (/ 1 16) + x1
     i()	weight: 0
   U52(x1)	weight: (/ 1 16) + x1
   U61(x1)	weight: (/ 1 16) + x1
     e()	weight: 0
   U31(x1)	weight: (/ 1 16) + x1
a__U71(x1,x2)	weight: (/ 5 16) + x1 + 2 * x2
a__isPal(x1)	weight: (/ 3 16) + 2 * x1
a__U61(x1)	weight: (/ 1 8) + x1
   U81(x1)	weight: (/ 1 16) + x1
    tt()	weight: 0
a__isQid(x1)	weight: (/ 1 16) + x1
   U22(x1)	weight: (/ 1 16) + x1
   U51(x1,x2)	weight: (/ 3 16) + x1 + x2
   U41(x1,x2)	weight: (/ 3 32) + x1 + x2
    __(x1,x2)	weight: (/ 3 8) + x1 + x2
Number of strict rules: 9
Direct Order(PosReal,>,Poly) ... removes: 33 58
     a()	weight: 0
   U21(x1,x2)	weight: (/ 1 8) + x1 + x2
   U11(x1)	weight: (/ 1 16) + 2 * x1
isNeList(x1)	weight: (/ 1 16) + x1
 isPal(x1)	weight: (/ 1 16) + 2 * x1
   U42(x1)	weight: (/ 1 16) + x1
     u()	weight: 0
   U71(x1,x2)	weight: (/ 1 8) + x1 + 2 * x2
a__U22(x1)	weight: (/ 1 16) + x1
isNePal(x1)	weight: (/ 1 8) + x1
   U72(x1)	weight: (/ 1 16) + 2 * x1
a__U31(x1)	weight: (/ 1 16) + x1
a__U51(x1,x2)	weight: (/ 3 8) + x1 + x2
a__U81(x1)	weight: (/ 1 16) + x1
 isQid(x1)	weight: (/ 1 16) + x1
 a____(x1,x2)	weight: (/ 3 4) + x1 + x2
a__U41(x1,x2)	weight: (/ 3 16) + x1 + x2
a__isList(x1)	weight: (/ 5 16) + x1
a__isNeList(x1)	weight: (/ 1 8) + x1
     o()	weight: 0
isList(x1)	weight: (/ 5 32) + x1
a__U21(x1,x2)	weight: (/ 3 16) + x1 + x2
   nil()	weight: 0
  mark(x1)	weight: 2 * x1
a__U72(x1)	weight: (/ 1 16) + x1
a__isNePal(x1)	weight: (/ 3 16) + x1
a__U11(x1)	weight: (/ 1 16) + 2 * x1
a__U42(x1)	weight: (/ 1 16) + x1
a__U52(x1)	weight: (/ 1 16) + x1
     i()	weight: 0
   U52(x1)	weight: (/ 1 16) + x1
   U61(x1)	weight: (/ 1 16) + x1
     e()	weight: 0
   U31(x1)	weight: (/ 1 16) + x1
a__U71(x1,x2)	weight: (/ 1 4) + x1 + 2 * x2
a__isPal(x1)	weight: (/ 1 8) + 2 * x1
a__U61(x1)	weight: (/ 1 8) + x1
   U81(x1)	weight: (/ 1 16) + x1
    tt()	weight: 0
a__isQid(x1)	weight: (/ 1 16) + x1
   U22(x1)	weight: (/ 1 16) + x1
   U51(x1,x2)	weight: (/ 3 16) + x1 + x2
   U41(x1,x2)	weight: (/ 3 32) + x1 + x2
    __(x1,x2)	weight: (/ 3 8) + x1 + x2
Number of strict rules: 7
Direct Order(PosReal,>,Poly) ... removes: 50 54 49 52 51 55 53
     a()	weight: 0
   U21(x1,x2)	weight: (/ 1 32) + x1 + x2
   U11(x1)	weight: (/ 1 64) + 2 * x1
isNeList(x1)	weight: (/ 1 64) + x1
 isPal(x1)	weight: (/ 1 64) + 2 * x1
   U42(x1)	weight: (/ 1 64) + x1
     u()	weight: 0
   U71(x1,x2)	weight: (/ 7 128) + x1 + 2 * x2
a__U22(x1)	weight: (/ 1 64) + 2 * x1
isNePal(x1)	weight: (/ 1 64) + x1
   U72(x1)	weight: (/ 1 64) + 2 * x1
a__U31(x1)	weight: (/ 1 64) + 2 * x1
a__U51(x1,x2)	weight: (/ 7 64) + x1 + x2
a__U81(x1)	weight: (/ 1 64) + x1
 isQid(x1)	weight: (/ 1 64) + x1
 a____(x1,x2)	weight: (/ 1 8) + x1 + 2 * x2
a__U41(x1,x2)	weight: (/ 3 64) + 2 * x1 + x2
a__isList(x1)	weight: (/ 3 64) + x1
a__isNeList(x1)	weight: (/ 1 64) + x1
     o()	weight: 0
isList(x1)	weight: (/ 1 64) + x1
a__U21(x1,x2)	weight: (/ 3 64) + x1 + x2
   nil()	weight: 0
  mark(x1)	weight: (/ 1 64) + 2 * x1
a__U72(x1)	weight: (/ 1 64) + 2 * x1
a__isNePal(x1)	weight: (/ 1 32) + x1
a__U11(x1)	weight: (/ 1 64) + 2 * x1
a__U42(x1)	weight: (/ 1 64) + 2 * x1
a__U52(x1)	weight: (/ 1 64) + 2 * x1
     i()	weight: 0
   U52(x1)	weight: (/ 1 64) + x1
   U61(x1)	weight: (/ 1 64) + x1
     e()	weight: 0
   U31(x1)	weight: (/ 1 64) + x1
a__U71(x1,x2)	weight: (/ 3 32) + 2 * x1 + 2 * x2
a__isPal(x1)	weight: (/ 1 32) + 2 * x1
a__U61(x1)	weight: (/ 1 32) + x1
   U81(x1)	weight: (/ 1 64) + x1
    tt()	weight: 0
a__isQid(x1)	weight: x1
   U22(x1)	weight: (/ 1 64) + x1
   U51(x1,x2)	weight: (/ 7 128) + x1 + x2
   U41(x1,x2)	weight: (/ 1 32) + x1 + x2
    __(x1,x2)	weight: (/ 1 8) + x1 + x2
Number of strict rules: 0
YES