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,__(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)) -> __(X1,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,__(P,I))) -> activate#(P)
   isNePal#(n____(I,__(P,I))) -> activate#(I)
   isNePal#(n____(I,__(P,I))) -> isQid#(activate(I))
   isNePal#(n____(I,__(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)) -> __#(X1,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,__(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)) -> __(X1,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,__(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)) -> __(X1,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) = x0 + 5/2,
    
    [isNePal#](x0) = 1/2x0 + 2,
    
    [isQid#](x0) = 0,
    
    [isNeList#](x0) = 1/2x0 + 2,
    
    [isList#](x0) = 1/2x0 + 5/2,
    
    [activate#](x0) = 1/2x0 + 3/2,
    
    [and#](x0, x1) = 1/2x0 + 1/2x1 + 1/2,
    
    [__#](x0, x1) = x0 + 2,
    
    [u] = 3,
    
    [o] = 3,
    
    [i] = 3,
    
    [e] = 3,
    
    [a] = 3,
    
    [n__u] = 3,
    
    [n__o] = 3,
    
    [n__i] = 3,
    
    [n__e] = 3,
    
    [n__a] = 3,
    
    [isPal](x0) = 2x0 + 3,
    
    [n__isPal](x0) = 2x0 + 3,
    
    [isNePal](x0) = x0 + 1/2,
    
    [n__isNeList](x0) = x0 + 2,
    
    [isQid](x0) = x0,
    
    [n__isList](x0) = x0 + 3,
    
    [n____](x0, x1) = 2x0 + x1 + 3,
    
    [n__nil] = 2,
    
    [isNeList](x0) = x0 + 2,
    
    [isList](x0) = x0 + 3,
    
    [activate](x0) = x0,
    
    [and](x0, x1) = x1 + 1/2,
    
    [tt] = 3,
    
    [nil] = 2,
    
    [__](x0, x1) = 2x0 + x1 + 3
   orientation:
    __#(__(X,Y),Z) = 2X + Y + 5 >= Y + 2 = __#(Y,Z)
    
    __#(__(X,Y),Z) = 2X + Y + 5 >= X + 2 = __#(X,__(Y,Z))
    
    and#(tt(),X) = 1/2X + 2 >= 1/2X + 3/2 = activate#(X)
    
    isList#(V) = 1/2V + 5/2 >= 1/2V + 3/2 = activate#(V)
    
    isList#(V) = 1/2V + 5/2 >= 1/2V + 2 = isNeList#(activate(V))
    
    isList#(n____(V1,V2)) = V1 + 1/2V2 + 4 >= 1/2V2 + 3/2 = activate#(V2)
    
    isList#(n____(V1,V2)) = V1 + 1/2V2 + 4 >= 1/2V1 + 3/2 = activate#(V1)
    
    isList#(n____(V1,V2)) = V1 + 1/2V2 + 4 >= 1/2V1 + 5/2 = isList#(activate(V1))
    
    isList#(n____(V1,V2)) = V1 + 1/2V2 + 4 >= 1/2V1 + 1/2V2 + 7/2 = and#(isList(activate(V1)),n__isList(activate(V2)))
    
    isNeList#(V) = 1/2V + 2 >= 1/2V + 3/2 = activate#(V)
    
    isNeList#(V) = 1/2V + 2 >= 0 = isQid#(activate(V))
    
    isNeList#(n____(V1,V2)) = V1 + 1/2V2 + 7/2 >= 1/2V2 + 3/2 = activate#(V2)
    
    isNeList#(n____(V1,V2)) = V1 + 1/2V2 + 7/2 >= 1/2V1 + 3/2 = activate#(V1)
    
    isNeList#(n____(V1,V2)) = V1 + 1/2V2 + 7/2 >= 1/2V1 + 5/2 = isList#(activate(V1))
    
    isNeList#(n____(V1,V2)) = V1 + 1/2V2 + 7/2 >= 1/2V1 + 1/2V2 + 3 = and#(isList(activate(V1)),n__isNeList(activate(V2)))
    
    isNeList#(n____(V1,V2)) = V1 + 1/2V2 + 7/2 >= 1/2V1 + 2 = isNeList#(activate(V1))
    
    isNeList#(n____(V1,V2)) = V1 + 1/2V2 + 7/2 >= 1/2V1 + 1/2V2 + 3 = and#(isNeList(activate(V1)),n__isList(activate(V2)))
    
    isNePal#(V) = 1/2V + 2 >= 1/2V + 3/2 = activate#(V)
    
    isNePal#(V) = 1/2V + 2 >= 0 = isQid#(activate(V))
    
    isNePal#(n____(I,__(P,I))) = 3/2I + P + 5 >= 1/2P + 3/2 = activate#(P)
    
    isNePal#(n____(I,__(P,I))) = 3/2I + P + 5 >= 1/2I + 3/2 = activate#(I)
    
    isNePal#(n____(I,__(P,I))) = 3/2I + P + 5 >= 0 = isQid#(activate(I))
    
    isNePal#(n____(I,__(P,I))) = 3/2I + P + 5 >= 1/2I + P + 2 = and#(isQid(activate(I)),n__isPal(activate(P)))
    
    isPal#(V) = V + 5/2 >= 1/2V + 3/2 = activate#(V)
    
    isPal#(V) = V + 5/2 >= 1/2V + 2 = isNePal#(activate(V))
    
    activate#(n__nil()) = 5/2 >= 0 = nil#()
    
    activate#(n____(X1,X2)) = X1 + 1/2X2 + 3 >= X1 + 2 = __#(X1,X2)
    
    activate#(n__isList(X)) = 1/2X + 3 >= 1/2X + 5/2 = isList#(X)
    
    activate#(n__isNeList(X)) = 1/2X + 5/2 >= 1/2X + 2 = isNeList#(X)
    
    activate#(n__isPal(X)) = X + 3 >= X + 5/2 = isPal#(X)
    
    activate#(n__a()) = 3 >= 0 = a#()
    
    activate#(n__e()) = 3 >= 0 = e#()
    
    activate#(n__i()) = 3 >= 0 = i#()
    
    activate#(n__o()) = 3 >= 0 = o#()
    
    activate#(n__u()) = 3 >= 0 = u#()
    
    __(__(X,Y),Z) = 4X + 2Y + Z + 9 >= 2X + 2Y + Z + 6 = __(X,__(Y,Z))
    
    __(X,nil()) = 2X + 5 >= X = X
    
    __(nil(),X) = X + 7 >= X = X
    
    and(tt(),X) = X + 1/2 >= X = activate(X)
    
    isList(V) = V + 3 >= V + 2 = isNeList(activate(V))
    
    isList(n__nil()) = 5 >= 3 = tt()
    
    isList(n____(V1,V2)) = 2V1 + V2 + 6 >= V2 + 7/2 = and(isList(activate(V1)),n__isList(activate(V2)))
    
    isNeList(V) = V + 2 >= V = isQid(activate(V))
    
    isNeList(n____(V1,V2)) = 2V1 + V2 + 5 >= V2 + 5/2 = and(isList(activate(V1)),n__isNeList(activate(V2)))
    
    isNeList(n____(V1,V2)) = 2V1 + V2 + 5 >= V2 + 7/2 = and(isNeList(activate(V1)),n__isList(activate(V2)))
    
    isNePal(V) = V + 1/2 >= V = isQid(activate(V))
    
    isNePal(n____(I,__(P,I))) = 3I + 2P + 13/2 >= 2P + 7/2 = and(isQid(activate(I)),n__isPal(activate(P)))
    
    isPal(V) = 2V + 3 >= V + 1/2 = isNePal(activate(V))
    
    isPal(n__nil()) = 7 >= 3 = tt()
    
    isQid(n__a()) = 3 >= 3 = tt()
    
    isQid(n__e()) = 3 >= 3 = tt()
    
    isQid(n__i()) = 3 >= 3 = tt()
    
    isQid(n__o()) = 3 >= 3 = tt()
    
    isQid(n__u()) = 3 >= 3 = tt()
    
    nil() = 2 >= 2 = n__nil()
    
    __(X1,X2) = 2X1 + X2 + 3 >= 2X1 + X2 + 3 = n____(X1,X2)
    
    isList(X) = X + 3 >= X + 3 = n__isList(X)
    
    isNeList(X) = X + 2 >= X + 2 = n__isNeList(X)
    
    isPal(X) = 2X + 3 >= 2X + 3 = n__isPal(X)
    
    a() = 3 >= 3 = n__a()
    
    e() = 3 >= 3 = n__e()
    
    i() = 3 >= 3 = n__i()
    
    o() = 3 >= 3 = n__o()
    
    u() = 3 >= 3 = n__u()
    
    activate(n__nil()) = 2 >= 2 = nil()
    
    activate(n____(X1,X2)) = 2X1 + X2 + 3 >= 2X1 + X2 + 3 = __(X1,X2)
    
    activate(n__isList(X)) = X + 3 >= X + 3 = isList(X)
    
    activate(n__isNeList(X)) = X + 2 >= X + 2 = isNeList(X)
    
    activate(n__isPal(X)) = 2X + 3 >= 2X + 3 = isPal(X)
    
    activate(n__a()) = 3 >= 3 = a()
    
    activate(n__e()) = 3 >= 3 = e()
    
    activate(n__i()) = 3 >= 3 = i()
    
    activate(n__o()) = 3 >= 3 = o()
    
    activate(n__u()) = 3 >= 3 = 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,__(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)) -> __(X1,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