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,n____(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)) -> __(activate(X1),activate(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:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [u] = 4,
   
   [o] = 2,
   
   [i] = 1,
   
   [e] = 1,
   
   [a] = 1,
   
   [n__u] = 4,
   
   [n__o] = 2,
   
   [n__i] = 1,
   
   [n__e] = 1,
   
   [n__a] = 1,
   
   [isNePal](x0) = x0 + 3,
   
   [isQid](x0) = x0,
   
   [n____](x0, x1) = 3x0 + x1 + 6,
   
   [n__nil] = 4,
   
   [U81](x0) = x0 + 1,
   
   [U72](x0) = 2x0,
   
   [isPal](x0) = x0 + 5,
   
   [U71](x0, x1) = 4x0 + 2x1 + 6,
   
   [U61](x0) = x0,
   
   [U52](x0) = x0,
   
   [U51](x0, x1) = 3x0 + x1 + 3,
   
   [U42](x0) = x0,
   
   [isNeList](x0) = x0,
   
   [U41](x0, x1) = x0 + x1,
   
   [U31](x0) = x0,
   
   [U22](x0) = x0,
   
   [isList](x0) = x0 + 6,
   
   [activate](x0) = x0,
   
   [U21](x0, x1) = x0 + x1 + 5,
   
   [U11](x0) = x0 + 3,
   
   [tt] = 1,
   
   [nil] = 4,
   
   [__](x0, x1) = 3x0 + x1 + 6
  orientation:
   __(__(X,Y),Z) = 9X + 3Y + Z + 24 >= 3X + 3Y + Z + 12 = __(X,__(Y,Z))
   
   __(X,nil()) = 3X + 10 >= X = X
   
   __(nil(),X) = X + 18 >= X = X
   
   U11(tt()) = 4 >= 1 = tt()
   
   U21(tt(),V2) = V2 + 6 >= V2 + 6 = U22(isList(activate(V2)))
   
   U22(tt()) = 1 >= 1 = tt()
   
   U31(tt()) = 1 >= 1 = tt()
   
   U41(tt(),V2) = V2 + 1 >= V2 = U42(isNeList(activate(V2)))
   
   U42(tt()) = 1 >= 1 = tt()
   
   U51(tt(),V2) = V2 + 6 >= V2 + 6 = U52(isList(activate(V2)))
   
   U52(tt()) = 1 >= 1 = tt()
   
   U61(tt()) = 1 >= 1 = tt()
   
   U71(tt(),P) = 2P + 10 >= 2P + 10 = U72(isPal(activate(P)))
   
   U72(tt()) = 2 >= 1 = tt()
   
   U81(tt()) = 2 >= 1 = tt()
   
   isList(V) = V + 6 >= V + 3 = U11(isNeList(activate(V)))
   
   isList(n__nil()) = 10 >= 1 = tt()
   
   isList(n____(V1,V2)) = 3V1 + V2 + 12 >= V1 + V2 + 11 = U21(isList(activate(V1)),activate(V2))
   
   isNeList(V) = V >= V = U31(isQid(activate(V)))
   
   isNeList(n____(V1,V2)) = 3V1 + V2 + 6 >= V1 + V2 + 6 = U41(isList(activate(V1)),activate(V2))
   
   isNeList(n____(V1,V2)) = 3V1 + V2 + 6 >= 3V1 + V2 + 3 = U51(isNeList(activate(V1)),activate(V2))
   
   isNePal(V) = V + 3 >= V = U61(isQid(activate(V)))
   
   isNePal(n____(I,n____(P,I))) = 4I + 3P + 15 >= 4I + 2P + 6 = U71(isQid(activate(I)),activate(P))
   
   isPal(V) = V + 5 >= V + 4 = U81(isNePal(activate(V)))
   
   isPal(n__nil()) = 9 >= 1 = tt()
   
   isQid(n__a()) = 1 >= 1 = tt()
   
   isQid(n__e()) = 1 >= 1 = tt()
   
   isQid(n__i()) = 1 >= 1 = tt()
   
   isQid(n__o()) = 2 >= 1 = tt()
   
   isQid(n__u()) = 4 >= 1 = tt()
   
   nil() = 4 >= 4 = n__nil()
   
   __(X1,X2) = 3X1 + X2 + 6 >= 3X1 + X2 + 6 = n____(X1,X2)
   
   a() = 1 >= 1 = n__a()
   
   e() = 1 >= 1 = n__e()
   
   i() = 1 >= 1 = n__i()
   
   o() = 2 >= 2 = n__o()
   
   u() = 4 >= 4 = n__u()
   
   activate(n__nil()) = 4 >= 4 = nil()
   
   activate(n____(X1,X2)) = 3X1 + X2 + 6 >= 3X1 + X2 + 6 = __(activate(X1),activate(X2))
   
   activate(n__a()) = 1 >= 1 = a()
   
   activate(n__e()) = 1 >= 1 = e()
   
   activate(n__i()) = 1 >= 1 = i()
   
   activate(n__o()) = 2 >= 2 = o()
   
   activate(n__u()) = 4 >= 4 = u()
   
   activate(X) = X >= X = X
  problem:
   U21(tt(),V2) -> U22(isList(activate(V2)))
   U22(tt()) -> tt()
   U31(tt()) -> tt()
   U42(tt()) -> tt()
   U51(tt(),V2) -> U52(isList(activate(V2)))
   U52(tt()) -> tt()
   U61(tt()) -> tt()
   U71(tt(),P) -> U72(isPal(activate(P)))
   isNeList(V) -> U31(isQid(activate(V)))
   isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
   isQid(n__a()) -> tt()
   isQid(n__e()) -> tt()
   isQid(n__i()) -> 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)) -> __(activate(X1),activate(X2))
   activate(n__a()) -> a()
   activate(n__e()) -> e()
   activate(n__i()) -> i()
   activate(n__o()) -> o()
   activate(n__u()) -> u()
   activate(X) -> X
  DP Processor:
   DPs:
    U21#(tt(),V2) -> activate#(V2)
    U21#(tt(),V2) -> U22#(isList(activate(V2)))
    U51#(tt(),V2) -> activate#(V2)
    U51#(tt(),V2) -> U52#(isList(activate(V2)))
    U71#(tt(),P) -> activate#(P)
    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)
    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__a()) -> a#()
    activate#(n__e()) -> e#()
    activate#(n__i()) -> i#()
    activate#(n__o()) -> o#()
    activate#(n__u()) -> u#()
   TRS:
    U21(tt(),V2) -> U22(isList(activate(V2)))
    U22(tt()) -> tt()
    U31(tt()) -> tt()
    U42(tt()) -> tt()
    U51(tt(),V2) -> U52(isList(activate(V2)))
    U52(tt()) -> tt()
    U61(tt()) -> tt()
    U71(tt(),P) -> U72(isPal(activate(P)))
    isNeList(V) -> U31(isQid(activate(V)))
    isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
    isQid(n__a()) -> tt()
    isQid(n__e()) -> tt()
    isQid(n__i()) -> 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)) -> __(activate(X1),activate(X2))
    activate(n__a()) -> a()
    activate(n__e()) -> e()
    activate(n__i()) -> i()
    activate(n__o()) -> o()
    activate(n__u()) -> u()
    activate(X) -> X
   TDG Processor:
    DPs:
     U21#(tt(),V2) -> activate#(V2)
     U21#(tt(),V2) -> U22#(isList(activate(V2)))
     U51#(tt(),V2) -> activate#(V2)
     U51#(tt(),V2) -> U52#(isList(activate(V2)))
     U71#(tt(),P) -> activate#(P)
     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)
     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__a()) -> a#()
     activate#(n__e()) -> e#()
     activate#(n__i()) -> i#()
     activate#(n__o()) -> o#()
     activate#(n__u()) -> u#()
    TRS:
     U21(tt(),V2) -> U22(isList(activate(V2)))
     U22(tt()) -> tt()
     U31(tt()) -> tt()
     U42(tt()) -> tt()
     U51(tt(),V2) -> U52(isList(activate(V2)))
     U52(tt()) -> tt()
     U61(tt()) -> tt()
     U71(tt(),P) -> U72(isPal(activate(P)))
     isNeList(V) -> U31(isQid(activate(V)))
     isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
     isQid(n__a()) -> tt()
     isQid(n__e()) -> tt()
     isQid(n__i()) -> 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)) -> __(activate(X1),activate(X2))
     activate(n__a()) -> a()
     activate(n__e()) -> e()
     activate(n__i()) -> i()
     activate(n__o()) -> o()
     activate(n__u()) -> u()
     activate(X) -> X
    graph:
     isNeList#(n____(V1,V2)) -> activate#(V2) ->
     activate#(n__u()) -> u#()
     isNeList#(n____(V1,V2)) -> activate#(V2) ->
     activate#(n__o()) -> o#()
     isNeList#(n____(V1,V2)) -> activate#(V2) ->
     activate#(n__i()) -> i#()
     isNeList#(n____(V1,V2)) -> activate#(V2) ->
     activate#(n__e()) -> e#()
     isNeList#(n____(V1,V2)) -> activate#(V2) ->
     activate#(n__a()) -> a#()
     isNeList#(n____(V1,V2)) -> activate#(V2) ->
     activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2))
     isNeList#(n____(V1,V2)) -> activate#(V2) ->
     activate#(n____(X1,X2)) -> activate#(X1)
     isNeList#(n____(V1,V2)) -> activate#(V2) ->
     activate#(n____(X1,X2)) -> activate#(X2)
     isNeList#(n____(V1,V2)) -> activate#(V2) ->
     activate#(n__nil()) -> nil#()
     isNeList#(n____(V1,V2)) -> activate#(V1) ->
     activate#(n__u()) -> u#()
     isNeList#(n____(V1,V2)) -> activate#(V1) ->
     activate#(n__o()) -> o#()
     isNeList#(n____(V1,V2)) -> activate#(V1) ->
     activate#(n__i()) -> i#()
     isNeList#(n____(V1,V2)) -> activate#(V1) ->
     activate#(n__e()) -> e#()
     isNeList#(n____(V1,V2)) -> activate#(V1) ->
     activate#(n__a()) -> a#()
     isNeList#(n____(V1,V2)) -> activate#(V1) ->
     activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2))
     isNeList#(n____(V1,V2)) -> activate#(V1) ->
     activate#(n____(X1,X2)) -> activate#(X1)
     isNeList#(n____(V1,V2)) -> activate#(V1) ->
     activate#(n____(X1,X2)) -> activate#(X2)
     isNeList#(n____(V1,V2)) -> activate#(V1) ->
     activate#(n__nil()) -> nil#()
     isNeList#(V) -> activate#(V) -> activate#(n__u()) -> u#()
     isNeList#(V) -> activate#(V) -> activate#(n__o()) -> o#()
     isNeList#(V) -> activate#(V) -> activate#(n__i()) -> i#()
     isNeList#(V) -> activate#(V) -> activate#(n__e()) -> e#()
     isNeList#(V) -> activate#(V) -> activate#(n__a()) -> a#()
     isNeList#(V) -> activate#(V) ->
     activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2))
     isNeList#(V) -> activate#(V) ->
     activate#(n____(X1,X2)) -> activate#(X1)
     isNeList#(V) -> activate#(V) ->
     activate#(n____(X1,X2)) -> activate#(X2)
     isNeList#(V) -> activate#(V) -> activate#(n__nil()) -> nil#()
     U71#(tt(),P) -> activate#(P) -> activate#(n__u()) -> u#()
     U71#(tt(),P) -> activate#(P) -> activate#(n__o()) -> o#()
     U71#(tt(),P) -> activate#(P) -> activate#(n__i()) -> i#()
     U71#(tt(),P) -> activate#(P) -> activate#(n__e()) -> e#()
     U71#(tt(),P) -> activate#(P) -> activate#(n__a()) -> a#()
     U71#(tt(),P) -> activate#(P) ->
     activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2))
     U71#(tt(),P) -> activate#(P) ->
     activate#(n____(X1,X2)) -> activate#(X1)
     U71#(tt(),P) -> activate#(P) ->
     activate#(n____(X1,X2)) -> activate#(X2)
     U71#(tt(),P) -> activate#(P) -> activate#(n__nil()) -> nil#()
     U51#(tt(),V2) -> activate#(V2) -> activate#(n__u()) -> u#()
     U51#(tt(),V2) -> activate#(V2) -> activate#(n__o()) -> o#()
     U51#(tt(),V2) -> activate#(V2) -> activate#(n__i()) -> i#()
     U51#(tt(),V2) -> activate#(V2) -> activate#(n__e()) -> e#()
     U51#(tt(),V2) -> activate#(V2) -> activate#(n__a()) -> a#()
     U51#(tt(),V2) -> activate#(V2) ->
     activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2))
     U51#(tt(),V2) -> activate#(V2) ->
     activate#(n____(X1,X2)) -> activate#(X1)
     U51#(tt(),V2) -> activate#(V2) ->
     activate#(n____(X1,X2)) -> activate#(X2)
     U51#(tt(),V2) -> activate#(V2) ->
     activate#(n__nil()) -> nil#()
     activate#(n____(X1,X2)) -> activate#(X2) ->
     activate#(n__u()) -> u#()
     activate#(n____(X1,X2)) -> activate#(X2) ->
     activate#(n__o()) -> o#()
     activate#(n____(X1,X2)) -> activate#(X2) ->
     activate#(n__i()) -> i#()
     activate#(n____(X1,X2)) -> activate#(X2) ->
     activate#(n__e()) -> e#()
     activate#(n____(X1,X2)) -> activate#(X2) ->
     activate#(n__a()) -> a#()
     activate#(n____(X1,X2)) -> activate#(X2) ->
     activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2))
     activate#(n____(X1,X2)) -> activate#(X2) ->
     activate#(n____(X1,X2)) -> activate#(X1)
     activate#(n____(X1,X2)) -> activate#(X2) ->
     activate#(n____(X1,X2)) -> activate#(X2)
     activate#(n____(X1,X2)) -> activate#(X2) ->
     activate#(n__nil()) -> nil#()
     activate#(n____(X1,X2)) -> activate#(X1) ->
     activate#(n__u()) -> u#()
     activate#(n____(X1,X2)) -> activate#(X1) ->
     activate#(n__o()) -> o#()
     activate#(n____(X1,X2)) -> activate#(X1) ->
     activate#(n__i()) -> i#()
     activate#(n____(X1,X2)) -> activate#(X1) ->
     activate#(n__e()) -> e#()
     activate#(n____(X1,X2)) -> activate#(X1) ->
     activate#(n__a()) -> a#()
     activate#(n____(X1,X2)) -> activate#(X1) ->
     activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2))
     activate#(n____(X1,X2)) -> activate#(X1) ->
     activate#(n____(X1,X2)) -> activate#(X1)
     activate#(n____(X1,X2)) -> activate#(X1) ->
     activate#(n____(X1,X2)) -> activate#(X2)
     activate#(n____(X1,X2)) -> activate#(X1) ->
     activate#(n__nil()) -> nil#()
     U21#(tt(),V2) -> activate#(V2) -> activate#(n__u()) -> u#()
     U21#(tt(),V2) -> activate#(V2) -> activate#(n__o()) -> o#()
     U21#(tt(),V2) -> activate#(V2) -> activate#(n__i()) -> i#()
     U21#(tt(),V2) -> activate#(V2) -> activate#(n__e()) -> e#()
     U21#(tt(),V2) -> activate#(V2) -> activate#(n__a()) -> a#()
     U21#(tt(),V2) -> activate#(V2) ->
     activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2))
     U21#(tt(),V2) -> activate#(V2) ->
     activate#(n____(X1,X2)) -> activate#(X1)
     U21#(tt(),V2) -> activate#(V2) ->
     activate#(n____(X1,X2)) -> activate#(X2)
     U21#(tt(),V2) -> activate#(V2) -> activate#(n__nil()) -> nil#()
    SCC Processor:
     #sccs: 1
     #rules: 2
     #arcs: 72/361
     DPs:
      activate#(n____(X1,X2)) -> activate#(X2)
      activate#(n____(X1,X2)) -> activate#(X1)
     TRS:
      U21(tt(),V2) -> U22(isList(activate(V2)))
      U22(tt()) -> tt()
      U31(tt()) -> tt()
      U42(tt()) -> tt()
      U51(tt(),V2) -> U52(isList(activate(V2)))
      U52(tt()) -> tt()
      U61(tt()) -> tt()
      U71(tt(),P) -> U72(isPal(activate(P)))
      isNeList(V) -> U31(isQid(activate(V)))
      isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
      isQid(n__a()) -> tt()
      isQid(n__e()) -> tt()
      isQid(n__i()) -> 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)) -> __(activate(X1),activate(X2))
      activate(n__a()) -> a()
      activate(n__e()) -> e()
      activate(n__i()) -> i()
      activate(n__o()) -> o()
      activate(n__u()) -> u()
      activate(X) -> X
     Subterm Criterion Processor:
      simple projection:
       pi(activate#) = 0
      problem:
       DPs:
        
       TRS:
        U21(tt(),V2) -> U22(isList(activate(V2)))
        U22(tt()) -> tt()
        U31(tt()) -> tt()
        U42(tt()) -> tt()
        U51(tt(),V2) -> U52(isList(activate(V2)))
        U52(tt()) -> tt()
        U61(tt()) -> tt()
        U71(tt(),P) -> U72(isPal(activate(P)))
        isNeList(V) -> U31(isQid(activate(V)))
        isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
        isQid(n__a()) -> tt()
        isQid(n__e()) -> tt()
        isQid(n__i()) -> 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)) -> __(activate(X1),activate(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