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