YES

Problem:
 __(__(X,Y),Z) -> __(X,__(Y,Z))
 __(X,nil()) -> X
 __(nil(),X) -> X
 U11(tt()) -> tt()
 U21(tt(),V2) -> U22(isList(activate(V2)))
 U22(tt()) -> tt()
 U31(tt()) -> tt()
 U41(tt(),V2) -> U42(isNeList(activate(V2)))
 U42(tt()) -> tt()
 U51(tt(),V2) -> U52(isList(activate(V2)))
 U52(tt()) -> tt()
 U61(tt()) -> tt()
 U71(tt(),P) -> U72(isPal(activate(P)))
 U72(tt()) -> tt()
 U81(tt()) -> tt()
 isList(V) -> U11(isNeList(activate(V)))
 isList(n__nil()) -> tt()
 isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
 isNeList(V) -> U31(isQid(activate(V)))
 isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
 isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
 isNePal(V) -> U61(isQid(activate(V)))
 isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
 isPal(V) -> U81(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)
 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__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))
   U21#(tt(),V2) -> activate#(V2)
   U21#(tt(),V2) -> isList#(activate(V2))
   U21#(tt(),V2) -> U22#(isList(activate(V2)))
   U41#(tt(),V2) -> activate#(V2)
   U41#(tt(),V2) -> isNeList#(activate(V2))
   U41#(tt(),V2) -> U42#(isNeList(activate(V2)))
   U51#(tt(),V2) -> activate#(V2)
   U51#(tt(),V2) -> isList#(activate(V2))
   U51#(tt(),V2) -> U52#(isList(activate(V2)))
   U71#(tt(),P) -> activate#(P)
   U71#(tt(),P) -> isPal#(activate(P))
   U71#(tt(),P) -> U72#(isPal(activate(P)))
   isList#(V) -> activate#(V)
   isList#(V) -> isNeList#(activate(V))
   isList#(V) -> U11#(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)) -> U21#(isList(activate(V1)),activate(V2))
   isNeList#(V) -> activate#(V)
   isNeList#(V) -> isQid#(activate(V))
   isNeList#(V) -> U31#(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)) -> U41#(isList(activate(V1)),activate(V2))
   isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
   isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
   isNePal#(V) -> activate#(V)
   isNePal#(V) -> isQid#(activate(V))
   isNePal#(V) -> U61#(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))) -> U71#(isQid(activate(I)),activate(P))
   isPal#(V) -> activate#(V)
   isPal#(V) -> isNePal#(activate(V))
   isPal#(V) -> U81#(isNePal(activate(V)))
   activate#(n__nil()) -> nil#()
   activate#(n____(X1,X2)) -> __#(X1,X2)
   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
   U11(tt()) -> tt()
   U21(tt(),V2) -> U22(isList(activate(V2)))
   U22(tt()) -> tt()
   U31(tt()) -> tt()
   U41(tt(),V2) -> U42(isNeList(activate(V2)))
   U42(tt()) -> tt()
   U51(tt(),V2) -> U52(isList(activate(V2)))
   U52(tt()) -> tt()
   U61(tt()) -> tt()
   U71(tt(),P) -> U72(isPal(activate(P)))
   U72(tt()) -> tt()
   U81(tt()) -> tt()
   isList(V) -> U11(isNeList(activate(V)))
   isList(n__nil()) -> tt()
   isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
   isNeList(V) -> U31(isQid(activate(V)))
   isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
   isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
   isNePal(V) -> U61(isQid(activate(V)))
   isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
   isPal(V) -> U81(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)
   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__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
   
   interpretation:
    [u#] = 0,
    
    [o#] = 0,
    
    [i#] = 0,
    
    [e#] = 0,
    
    [a#] = 0,
    
    [nil#] = 0,
    
    [isNePal#](x0) = 5x0 + 1,
    
    [isQid#](x0) = 0,
    
    [U81#](x0) = x0 + 1,
    
    [U72#](x0) = 2,
    
    [isPal#](x0) = 5x0 + 4,
    
    [U71#](x0, x1) = 5x1 + 5,
    
    [U61#](x0) = 0,
    
    [U52#](x0) = 0,
    
    [U51#](x0, x1) = x1 + 6,
    
    [U42#](x0) = 4,
    
    [isNeList#](x0) = x0 + 4,
    
    [U41#](x0, x1) = x1 + 5,
    
    [U31#](x0) = 2,
    
    [U22#](x0) = 2,
    
    [isList#](x0) = x0 + 5,
    
    [activate#](x0) = x0,
    
    [U21#](x0, x1) = x1 + 6,
    
    [U11#](x0) = 2,
    
    [__#](x0, x1) = x0,
    
    [u] = 1,
    
    [o] = 4,
    
    [i] = 2,
    
    [e] = 3,
    
    [a] = 4,
    
    [n__u] = 1,
    
    [n__o] = 4,
    
    [n__i] = 2,
    
    [n__e] = 3,
    
    [n__a] = 4,
    
    [isNePal](x0) = x0 + 2,
    
    [isQid](x0) = 6x0 + 2,
    
    [n____](x0, x1) = x0 + x1 + 3,
    
    [n__nil] = 1,
    
    [U81](x0) = x0 + 2,
    
    [U72](x0) = x0,
    
    [isPal](x0) = x0 + 4,
    
    [U71](x0, x1) = x1 + 5,
    
    [U61](x0) = 2,
    
    [U52](x0) = 0,
    
    [U51](x0, x1) = x0 + 2x1,
    
    [U42](x0) = x0,
    
    [isNeList](x0) = 6x0 + 7,
    
    [U41](x0, x1) = 3x0 + 6x1 + 7,
    
    [U31](x0) = x0 + 5,
    
    [U22](x0) = 1,
    
    [isList](x0) = 2x0,
    
    [activate](x0) = x0,
    
    [U21](x0, x1) = x1 + 6,
    
    [U11](x0) = 0,
    
    [tt] = 0,
    
    [nil] = 1,
    
    [__](x0, x1) = x0 + x1 + 3
   orientation:
    __#(__(X,Y),Z) = X + Y + 3 >= Y = __#(Y,Z)
    
    __#(__(X,Y),Z) = X + Y + 3 >= X = __#(X,__(Y,Z))
    
    U21#(tt(),V2) = V2 + 6 >= V2 = activate#(V2)
    
    U21#(tt(),V2) = V2 + 6 >= V2 + 5 = isList#(activate(V2))
    
    U21#(tt(),V2) = V2 + 6 >= 2 = U22#(isList(activate(V2)))
    
    U41#(tt(),V2) = V2 + 5 >= V2 = activate#(V2)
    
    U41#(tt(),V2) = V2 + 5 >= V2 + 4 = isNeList#(activate(V2))
    
    U41#(tt(),V2) = V2 + 5 >= 4 = U42#(isNeList(activate(V2)))
    
    U51#(tt(),V2) = V2 + 6 >= V2 = activate#(V2)
    
    U51#(tt(),V2) = V2 + 6 >= V2 + 5 = isList#(activate(V2))
    
    U51#(tt(),V2) = V2 + 6 >= 0 = U52#(isList(activate(V2)))
    
    U71#(tt(),P) = 5P + 5 >= P = activate#(P)
    
    U71#(tt(),P) = 5P + 5 >= 5P + 4 = isPal#(activate(P))
    
    U71#(tt(),P) = 5P + 5 >= 2 = U72#(isPal(activate(P)))
    
    isList#(V) = V + 5 >= V = activate#(V)
    
    isList#(V) = V + 5 >= V + 4 = isNeList#(activate(V))
    
    isList#(V) = V + 5 >= 2 = U11#(isNeList(activate(V)))
    
    isList#(n____(V1,V2)) = V1 + V2 + 8 >= V2 = activate#(V2)
    
    isList#(n____(V1,V2)) = V1 + V2 + 8 >= V1 = activate#(V1)
    
    isList#(n____(V1,V2)) = V1 + V2 + 8 >= V1 + 5 = isList#(activate(V1))
    
    isList#(n____(V1,V2)) = V1 + V2 + 8 >= V2 + 6 = U21#(isList(activate(V1)),activate(V2))
    
    isNeList#(V) = V + 4 >= V = activate#(V)
    
    isNeList#(V) = V + 4 >= 0 = isQid#(activate(V))
    
    isNeList#(V) = V + 4 >= 2 = U31#(isQid(activate(V)))
    
    isNeList#(n____(V1,V2)) = V1 + V2 + 7 >= V2 = activate#(V2)
    
    isNeList#(n____(V1,V2)) = V1 + V2 + 7 >= V1 = activate#(V1)
    
    isNeList#(n____(V1,V2)) = V1 + V2 + 7 >= V1 + 5 = isList#(activate(V1))
    
    isNeList#(n____(V1,V2)) = V1 + V2 + 7 >= V2 + 5 = U41#(isList(activate(V1)),activate(V2))
    
    isNeList#(n____(V1,V2)) = V1 + V2 + 7 >= V1 + 4 = isNeList#(activate(V1))
    
    isNeList#(n____(V1,V2)) = V1 + V2 + 7 >= V2 + 6 = U51#(isNeList(activate(V1)),activate(V2))
    
    isNePal#(V) = 5V + 1 >= V = activate#(V)
    
    isNePal#(V) = 5V + 1 >= 0 = isQid#(activate(V))
    
    isNePal#(V) = 5V + 1 >= 0 = U61#(isQid(activate(V)))
    
    isNePal#(n____(I,__(P,I))) = 10I + 5P + 31 >= P = activate#(P)
    
    isNePal#(n____(I,__(P,I))) = 10I + 5P + 31 >= I = activate#(I)
    
    isNePal#(n____(I,__(P,I))) = 10I + 5P + 31 >= 0 = isQid#(activate(I))
    
    isNePal#(n____(I,__(P,I))) = 10I + 5P + 31 >= 5P + 5 = U71#(isQid(activate(I)),activate(P))
    
    isPal#(V) = 5V + 4 >= V = activate#(V)
    
    isPal#(V) = 5V + 4 >= 5V + 1 = isNePal#(activate(V))
    
    isPal#(V) = 5V + 4 >= V + 3 = U81#(isNePal(activate(V)))
    
    activate#(n__nil()) = 1 >= 0 = nil#()
    
    activate#(n____(X1,X2)) = X1 + X2 + 3 >= X1 = __#(X1,X2)
    
    activate#(n__a()) = 4 >= 0 = a#()
    
    activate#(n__e()) = 3 >= 0 = e#()
    
    activate#(n__i()) = 2 >= 0 = i#()
    
    activate#(n__o()) = 4 >= 0 = o#()
    
    activate#(n__u()) = 1 >= 0 = u#()
    
    __(__(X,Y),Z) = X + Y + Z + 6 >= X + Y + Z + 6 = __(X,__(Y,Z))
    
    __(X,nil()) = X + 4 >= X = X
    
    __(nil(),X) = X + 4 >= X = X
    
    U11(tt()) = 0 >= 0 = tt()
    
    U21(tt(),V2) = V2 + 6 >= 1 = U22(isList(activate(V2)))
    
    U22(tt()) = 1 >= 0 = tt()
    
    U31(tt()) = 5 >= 0 = tt()
    
    U41(tt(),V2) = 6V2 + 7 >= 6V2 + 7 = U42(isNeList(activate(V2)))
    
    U42(tt()) = 0 >= 0 = tt()
    
    U51(tt(),V2) = 2V2 >= 0 = U52(isList(activate(V2)))
    
    U52(tt()) = 0 >= 0 = tt()
    
    U61(tt()) = 2 >= 0 = tt()
    
    U71(tt(),P) = P + 5 >= P + 4 = U72(isPal(activate(P)))
    
    U72(tt()) = 0 >= 0 = tt()
    
    U81(tt()) = 2 >= 0 = tt()
    
    isList(V) = 2V >= 0 = U11(isNeList(activate(V)))
    
    isList(n__nil()) = 2 >= 0 = tt()
    
    isList(n____(V1,V2)) = 2V1 + 2V2 + 6 >= V2 + 6 = U21(isList(activate(V1)),activate(V2))
    
    isNeList(V) = 6V + 7 >= 6V + 7 = U31(isQid(activate(V)))
    
    isNeList(n____(V1,V2)) = 6V1 + 6V2 + 25 >= 6V1 + 6V2 + 7 = U41(isList(activate(V1)),activate(V2))
    
    isNeList(n____(V1,V2)) = 6V1 + 6V2 + 25 >= 6V1 + 2V2 + 7 = U51(isNeList(activate(V1)),activate(V2))
    
    isNePal(V) = V + 2 >= 2 = U61(isQid(activate(V)))
    
    isNePal(n____(I,__(P,I))) = 2I + P + 8 >= P + 5 = U71(isQid(activate(I)),activate(P))
    
    isPal(V) = V + 4 >= V + 4 = U81(isNePal(activate(V)))
    
    isPal(n__nil()) = 5 >= 0 = tt()
    
    isQid(n__a()) = 26 >= 0 = tt()
    
    isQid(n__e()) = 20 >= 0 = tt()
    
    isQid(n__i()) = 14 >= 0 = tt()
    
    isQid(n__o()) = 26 >= 0 = tt()
    
    isQid(n__u()) = 8 >= 0 = tt()
    
    nil() = 1 >= 1 = n__nil()
    
    __(X1,X2) = X1 + X2 + 3 >= X1 + X2 + 3 = n____(X1,X2)
    
    a() = 4 >= 4 = n__a()
    
    e() = 3 >= 3 = n__e()
    
    i() = 2 >= 2 = n__i()
    
    o() = 4 >= 4 = n__o()
    
    u() = 1 >= 1 = n__u()
    
    activate(n__nil()) = 1 >= 1 = nil()
    
    activate(n____(X1,X2)) = X1 + X2 + 3 >= X1 + X2 + 3 = __(X1,X2)
    
    activate(n__a()) = 4 >= 4 = a()
    
    activate(n__e()) = 3 >= 3 = e()
    
    activate(n__i()) = 2 >= 2 = i()
    
    activate(n__o()) = 4 >= 4 = o()
    
    activate(n__u()) = 1 >= 1 = u()
    
    activate(X) = X >= X = X
   problem:
    DPs:
     
    TRS:
     __(__(X,Y),Z) -> __(X,__(Y,Z))
     __(X,nil()) -> X
     __(nil(),X) -> X
     U11(tt()) -> tt()
     U21(tt(),V2) -> U22(isList(activate(V2)))
     U22(tt()) -> tt()
     U31(tt()) -> tt()
     U41(tt(),V2) -> U42(isNeList(activate(V2)))
     U42(tt()) -> tt()
     U51(tt(),V2) -> U52(isList(activate(V2)))
     U52(tt()) -> tt()
     U61(tt()) -> tt()
     U71(tt(),P) -> U72(isPal(activate(P)))
     U72(tt()) -> tt()
     U81(tt()) -> tt()
     isList(V) -> U11(isNeList(activate(V)))
     isList(n__nil()) -> tt()
     isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
     isNeList(V) -> U31(isQid(activate(V)))
     isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
     isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
     isNePal(V) -> U61(isQid(activate(V)))
     isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
     isPal(V) -> U81(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)
     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__a()) -> a()
     activate(n__e()) -> e()
     activate(n__i()) -> i()
     activate(n__o()) -> o()
     activate(n__u()) -> u()
     activate(X) -> X
   Qed