YES

Problem:
 __(__(X,Y),Z) -> __(X,__(Y,Z))
 __(X,nil()) -> X
 __(nil(),X) -> X
 and(tt(),X) -> activate(X)
 isList(V) -> isNeList(activate(V))
 isList(n__nil()) -> tt()
 isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
 isNeList(V) -> isQid(activate(V))
 isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
 isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
 isNePal(V) -> isQid(activate(V))
 isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
 isPal(V) -> isNePal(activate(V))
 isPal(n__nil()) -> tt()
 isQid(n__a()) -> tt()
 isQid(n__e()) -> tt()
 isQid(n__i()) -> tt()
 isQid(n__o()) -> tt()
 isQid(n__u()) -> tt()
 nil() -> n__nil()
 __(X1,X2) -> n____(X1,X2)
 isList(X) -> n__isList(X)
 isNeList(X) -> n__isNeList(X)
 isPal(X) -> n__isPal(X)
 a() -> n__a()
 e() -> n__e()
 i() -> n__i()
 o() -> n__o()
 u() -> n__u()
 activate(n__nil()) -> nil()
 activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
 activate(n__isList(X)) -> isList(X)
 activate(n__isNeList(X)) -> isNeList(X)
 activate(n__isPal(X)) -> isPal(X)
 activate(n__a()) -> a()
 activate(n__e()) -> e()
 activate(n__i()) -> i()
 activate(n__o()) -> o()
 activate(n__u()) -> u()
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   __#(__(X,Y),Z) -> __#(Y,Z)
   __#(__(X,Y),Z) -> __#(X,__(Y,Z))
   and#(tt(),X) -> activate#(X)
   isList#(V) -> activate#(V)
   isList#(V) -> isNeList#(activate(V))
   isList#(n____(V1,V2)) -> activate#(V2)
   isList#(n____(V1,V2)) -> activate#(V1)
   isList#(n____(V1,V2)) -> isList#(activate(V1))
   isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
   isNeList#(V) -> activate#(V)
   isNeList#(V) -> isQid#(activate(V))
   isNeList#(n____(V1,V2)) -> activate#(V2)
   isNeList#(n____(V1,V2)) -> activate#(V1)
   isNeList#(n____(V1,V2)) -> isList#(activate(V1))
   isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
   isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
   isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2)))
   isNePal#(V) -> activate#(V)
   isNePal#(V) -> isQid#(activate(V))
   isNePal#(n____(I,n____(P,I))) -> activate#(P)
   isNePal#(n____(I,n____(P,I))) -> activate#(I)
   isNePal#(n____(I,n____(P,I))) -> isQid#(activate(I))
   isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P)))
   isPal#(V) -> activate#(V)
   isPal#(V) -> isNePal#(activate(V))
   activate#(n__nil()) -> nil#()
   activate#(n____(X1,X2)) -> activate#(X2)
   activate#(n____(X1,X2)) -> activate#(X1)
   activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2))
   activate#(n__isList(X)) -> isList#(X)
   activate#(n__isNeList(X)) -> isNeList#(X)
   activate#(n__isPal(X)) -> isPal#(X)
   activate#(n__a()) -> a#()
   activate#(n__e()) -> e#()
   activate#(n__i()) -> i#()
   activate#(n__o()) -> o#()
   activate#(n__u()) -> u#()
  TRS:
   __(__(X,Y),Z) -> __(X,__(Y,Z))
   __(X,nil()) -> X
   __(nil(),X) -> X
   and(tt(),X) -> activate(X)
   isList(V) -> isNeList(activate(V))
   isList(n__nil()) -> tt()
   isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
   isNeList(V) -> isQid(activate(V))
   isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
   isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
   isNePal(V) -> isQid(activate(V))
   isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
   isPal(V) -> isNePal(activate(V))
   isPal(n__nil()) -> tt()
   isQid(n__a()) -> tt()
   isQid(n__e()) -> tt()
   isQid(n__i()) -> tt()
   isQid(n__o()) -> tt()
   isQid(n__u()) -> tt()
   nil() -> n__nil()
   __(X1,X2) -> n____(X1,X2)
   isList(X) -> n__isList(X)
   isNeList(X) -> n__isNeList(X)
   isPal(X) -> n__isPal(X)
   a() -> n__a()
   e() -> n__e()
   i() -> n__i()
   o() -> n__o()
   u() -> n__u()
   activate(n__nil()) -> nil()
   activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
   activate(n__isList(X)) -> isList(X)
   activate(n__isNeList(X)) -> isNeList(X)
   activate(n__isPal(X)) -> isPal(X)
   activate(n__a()) -> a()
   activate(n__e()) -> e()
   activate(n__i()) -> i()
   activate(n__o()) -> o()
   activate(n__u()) -> u()
   activate(X) -> X
  Matrix Interpretation Processor: dim=1
   
   usable rules:
    __(__(X,Y),Z) -> __(X,__(Y,Z))
    __(X,nil()) -> X
    __(nil(),X) -> X
    and(tt(),X) -> activate(X)
    isList(V) -> isNeList(activate(V))
    isList(n__nil()) -> tt()
    isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
    isNeList(V) -> isQid(activate(V))
    isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
    isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
    isNePal(V) -> isQid(activate(V))
    isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
    isPal(V) -> isNePal(activate(V))
    isPal(n__nil()) -> tt()
    isQid(n__a()) -> tt()
    isQid(n__e()) -> tt()
    isQid(n__i()) -> tt()
    isQid(n__o()) -> tt()
    isQid(n__u()) -> tt()
    nil() -> n__nil()
    __(X1,X2) -> n____(X1,X2)
    isList(X) -> n__isList(X)
    isNeList(X) -> n__isNeList(X)
    isPal(X) -> n__isPal(X)
    a() -> n__a()
    e() -> n__e()
    i() -> n__i()
    o() -> n__o()
    u() -> n__u()
    activate(n__nil()) -> nil()
    activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
    activate(n__isList(X)) -> isList(X)
    activate(n__isNeList(X)) -> isNeList(X)
    activate(n__isPal(X)) -> isPal(X)
    activate(n__a()) -> a()
    activate(n__e()) -> e()
    activate(n__i()) -> i()
    activate(n__o()) -> o()
    activate(n__u()) -> u()
    activate(X) -> X
   interpretation:
    [u#] = 0,
    
    [o#] = 0,
    
    [i#] = 0,
    
    [e#] = 0,
    
    [a#] = 0,
    
    [nil#] = 0,
    
    [isPal#](x0) = 7x0 + 7,
    
    [isNePal#](x0) = 6x0 + 6,
    
    [isQid#](x0) = 0,
    
    [isNeList#](x0) = 4x0 + 5,
    
    [isList#](x0) = 4x0 + 7,
    
    [activate#](x0) = 4x0 + 4,
    
    [and#](x0, x1) = 3x0 + 4x1 + 1,
    
    [__#](x0, x1) = 4x0,
    
    [u] = 4,
    
    [o] = 4,
    
    [i] = 4,
    
    [e] = 4,
    
    [a] = 4,
    
    [n__u] = 4,
    
    [n__o] = 4,
    
    [n__i] = 4,
    
    [n__e] = 4,
    
    [n__a] = 4,
    
    [isPal](x0) = 4x0 + 1,
    
    [n__isPal](x0) = 4x0 + 1,
    
    [isNePal](x0) = 2x0,
    
    [n__isNeList](x0) = x0 + 1,
    
    [isQid](x0) = x0,
    
    [n__isList](x0) = x0 + 1,
    
    [n____](x0, x1) = 3x0 + x1 + 1,
    
    [n__nil] = 3,
    
    [isNeList](x0) = x0 + 1,
    
    [isList](x0) = x0 + 1,
    
    [activate](x0) = x0,
    
    [and](x0, x1) = x1 + 1,
    
    [tt] = 4,
    
    [nil] = 3,
    
    [__](x0, x1) = 3x0 + x1 + 1
   orientation:
    __#(__(X,Y),Z) = 12X + 4Y + 4 >= 4Y = __#(Y,Z)
    
    __#(__(X,Y),Z) = 12X + 4Y + 4 >= 4X = __#(X,__(Y,Z))
    
    and#(tt(),X) = 4X + 13 >= 4X + 4 = activate#(X)
    
    isList#(V) = 4V + 7 >= 4V + 4 = activate#(V)
    
    isList#(V) = 4V + 7 >= 4V + 5 = isNeList#(activate(V))
    
    isList#(n____(V1,V2)) = 12V1 + 4V2 + 11 >= 4V2 + 4 = activate#(V2)
    
    isList#(n____(V1,V2)) = 12V1 + 4V2 + 11 >= 4V1 + 4 = activate#(V1)
    
    isList#(n____(V1,V2)) = 12V1 + 4V2 + 11 >= 4V1 + 7 = isList#(activate(V1))
    
    isList#(n____(V1,V2)) = 12V1 + 4V2 + 11 >= 3V1 + 4V2 + 8 = and#(isList(activate(V1)),n__isList(activate(V2)))
    
    isNeList#(V) = 4V + 5 >= 4V + 4 = activate#(V)
    
    isNeList#(V) = 4V + 5 >= 0 = isQid#(activate(V))
    
    isNeList#(n____(V1,V2)) = 12V1 + 4V2 + 9 >= 4V2 + 4 = activate#(V2)
    
    isNeList#(n____(V1,V2)) = 12V1 + 4V2 + 9 >= 4V1 + 4 = activate#(V1)
    
    isNeList#(n____(V1,V2)) = 12V1 + 4V2 + 9 >= 4V1 + 7 = isList#(activate(V1))
    
    isNeList#(n____(V1,V2)) = 12V1 + 4V2 + 9 >= 3V1 + 4V2 + 8 = and#(isList(activate(V1)),n__isNeList(activate(V2)))
    
    isNeList#(n____(V1,V2)) = 12V1 + 4V2 + 9 >= 4V1 + 5 = isNeList#(activate(V1))
    
    isNeList#(n____(V1,V2)) = 12V1 + 4V2 + 9 >= 3V1 + 4V2 + 8 = and#(isNeList(activate(V1)),n__isList(activate(V2)))
    
    isNePal#(V) = 6V + 6 >= 4V + 4 = activate#(V)
    
    isNePal#(V) = 6V + 6 >= 0 = isQid#(activate(V))
    
    isNePal#(n____(I,n____(P,I))) = 24I + 18P + 18 >= 4P + 4 = activate#(P)
    
    isNePal#(n____(I,n____(P,I))) = 24I + 18P + 18 >= 4I + 4 = activate#(I)
    
    isNePal#(n____(I,n____(P,I))) = 24I + 18P + 18 >= 0 = isQid#(activate(I))
    
    isNePal#(n____(I,n____(P,I))) = 24I + 18P + 18 >= 3I + 16P + 5 = and#(isQid(activate(I)),n__isPal(activate(P)))
    
    isPal#(V) = 7V + 7 >= 4V + 4 = activate#(V)
    
    isPal#(V) = 7V + 7 >= 6V + 6 = isNePal#(activate(V))
    
    activate#(n__nil()) = 16 >= 0 = nil#()
    
    activate#(n____(X1,X2)) = 12X1 + 4X2 + 8 >= 4X2 + 4 = activate#(X2)
    
    activate#(n____(X1,X2)) = 12X1 + 4X2 + 8 >= 4X1 + 4 = activate#(X1)
    
    activate#(n____(X1,X2)) = 12X1 + 4X2 + 8 >= 4X1 = __#(activate(X1),activate(X2))
    
    activate#(n__isList(X)) = 4X + 8 >= 4X + 7 = isList#(X)
    
    activate#(n__isNeList(X)) = 4X + 8 >= 4X + 5 = isNeList#(X)
    
    activate#(n__isPal(X)) = 16X + 8 >= 7X + 7 = isPal#(X)
    
    activate#(n__a()) = 20 >= 0 = a#()
    
    activate#(n__e()) = 20 >= 0 = e#()
    
    activate#(n__i()) = 20 >= 0 = i#()
    
    activate#(n__o()) = 20 >= 0 = o#()
    
    activate#(n__u()) = 20 >= 0 = u#()
    
    __(__(X,Y),Z) = 9X + 3Y + Z + 4 >= 3X + 3Y + Z + 2 = __(X,__(Y,Z))
    
    __(X,nil()) = 3X + 4 >= X = X
    
    __(nil(),X) = X + 10 >= X = X
    
    and(tt(),X) = X + 1 >= X = activate(X)
    
    isList(V) = V + 1 >= V + 1 = isNeList(activate(V))
    
    isList(n__nil()) = 4 >= 4 = tt()
    
    isList(n____(V1,V2)) = 3V1 + V2 + 2 >= V2 + 2 = and(isList(activate(V1)),n__isList(activate(V2)))
    
    isNeList(V) = V + 1 >= V = isQid(activate(V))
    
    isNeList(n____(V1,V2)) = 3V1 + V2 + 2 >= V2 + 2 = and(isList(activate(V1)),n__isNeList(activate(V2)))
    
    isNeList(n____(V1,V2)) = 3V1 + V2 + 2 >= V2 + 2 = and(isNeList(activate(V1)),n__isList(activate(V2)))
    
    isNePal(V) = 2V >= V = isQid(activate(V))
    
    isNePal(n____(I,n____(P,I))) = 8I + 6P + 4 >= 4P + 2 = and(isQid(activate(I)),n__isPal(activate(P)))
    
    isPal(V) = 4V + 1 >= 2V = isNePal(activate(V))
    
    isPal(n__nil()) = 13 >= 4 = tt()
    
    isQid(n__a()) = 4 >= 4 = tt()
    
    isQid(n__e()) = 4 >= 4 = tt()
    
    isQid(n__i()) = 4 >= 4 = tt()
    
    isQid(n__o()) = 4 >= 4 = tt()
    
    isQid(n__u()) = 4 >= 4 = tt()
    
    nil() = 3 >= 3 = n__nil()
    
    __(X1,X2) = 3X1 + X2 + 1 >= 3X1 + X2 + 1 = n____(X1,X2)
    
    isList(X) = X + 1 >= X + 1 = n__isList(X)
    
    isNeList(X) = X + 1 >= X + 1 = n__isNeList(X)
    
    isPal(X) = 4X + 1 >= 4X + 1 = n__isPal(X)
    
    a() = 4 >= 4 = n__a()
    
    e() = 4 >= 4 = n__e()
    
    i() = 4 >= 4 = n__i()
    
    o() = 4 >= 4 = n__o()
    
    u() = 4 >= 4 = n__u()
    
    activate(n__nil()) = 3 >= 3 = nil()
    
    activate(n____(X1,X2)) = 3X1 + X2 + 1 >= 3X1 + X2 + 1 = __(activate(X1),activate(X2))
    
    activate(n__isList(X)) = X + 1 >= X + 1 = isList(X)
    
    activate(n__isNeList(X)) = X + 1 >= X + 1 = isNeList(X)
    
    activate(n__isPal(X)) = 4X + 1 >= 4X + 1 = isPal(X)
    
    activate(n__a()) = 4 >= 4 = a()
    
    activate(n__e()) = 4 >= 4 = e()
    
    activate(n__i()) = 4 >= 4 = i()
    
    activate(n__o()) = 4 >= 4 = o()
    
    activate(n__u()) = 4 >= 4 = u()
    
    activate(X) = X >= X = X
   problem:
    DPs:
     
    TRS:
     __(__(X,Y),Z) -> __(X,__(Y,Z))
     __(X,nil()) -> X
     __(nil(),X) -> X
     and(tt(),X) -> activate(X)
     isList(V) -> isNeList(activate(V))
     isList(n__nil()) -> tt()
     isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
     isNeList(V) -> isQid(activate(V))
     isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
     isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
     isNePal(V) -> isQid(activate(V))
     isNePal(n____(I,n____(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
     isPal(V) -> isNePal(activate(V))
     isPal(n__nil()) -> tt()
     isQid(n__a()) -> tt()
     isQid(n__e()) -> tt()
     isQid(n__i()) -> tt()
     isQid(n__o()) -> tt()
     isQid(n__u()) -> tt()
     nil() -> n__nil()
     __(X1,X2) -> n____(X1,X2)
     isList(X) -> n__isList(X)
     isNeList(X) -> n__isNeList(X)
     isPal(X) -> n__isPal(X)
     a() -> n__a()
     e() -> n__e()
     i() -> n__i()
     o() -> n__o()
     u() -> n__u()
     activate(n__nil()) -> nil()
     activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
     activate(n__isList(X)) -> isList(X)
     activate(n__isNeList(X)) -> isNeList(X)
     activate(n__isPal(X)) -> isPal(X)
     activate(n__a()) -> a()
     activate(n__e()) -> e()
     activate(n__i()) -> i()
     activate(n__o()) -> o()
     activate(n__u()) -> u()
     activate(X) -> X
   Qed