(STRATEGY
    INNERMOST)

(VAR
    I P V V1 V2 X X1 X2 Y Z)
(DATATYPES
    A = µX.< tt, n__nil, n____(X, X), n__isPalListKind(X), n__and(X, X), n__a, n__e, n__i, n__o, n__u >)
(SIGNATURES
    __ :: [A x A] -> A
    U11 :: [A x A] -> A
    U12 :: [A] -> A
    U21 :: [A x A x A] -> A
    U22 :: [A x A] -> A
    U23 :: [A] -> A
    U31 :: [A x A] -> A
    U32 :: [A] -> A
    U41 :: [A x A x A] -> A
    U42 :: [A x A] -> A
    U43 :: [A] -> A
    U51 :: [A x A x A] -> A
    U52 :: [A x A] -> A
    U53 :: [A] -> A
    U61 :: [A x A] -> A
    U62 :: [A] -> A
    U71 :: [A x A] -> A
    U72 :: [A] -> A
    and :: [A x A] -> A
    isList :: [A] -> A
    isNeList :: [A] -> A
    isNePal :: [A] -> A
    isPal :: [A] -> A
    isPalListKind :: [A] -> A
    isQid :: [A] -> A
    nil :: [] -> A
    a :: [] -> A
    e :: [] -> A
    i :: [] -> A
    o :: [] -> A
    u :: [] -> A
    activate :: [A] -> A)
(RULES
    __(__(X,Y),Z) -> __(X,__(Y,Z))
    __(X,nil()) -> X
    __(nil(),X) -> X
    U11(tt(),V) ->
      U12(isNeList(activate(V)))
    U12(tt()) -> tt()
    U21(tt(),V1,V2) ->
      U22(isList(activate(V1))
         ,activate(V2))
    U22(tt(),V2) ->
      U23(isList(activate(V2)))
    U23(tt()) -> tt()
    U31(tt(),V) ->
      U32(isQid(activate(V)))
    U32(tt()) -> tt()
    U41(tt(),V1,V2) ->
      U42(isList(activate(V1))
         ,activate(V2))
    U42(tt(),V2) ->
      U43(isNeList(activate(V2)))
    U43(tt()) -> tt()
    U51(tt(),V1,V2) ->
      U52(isNeList(activate(V1))
         ,activate(V2))
    U52(tt(),V2) ->
      U53(isList(activate(V2)))
    U53(tt()) -> tt()
    U61(tt(),V) ->
      U62(isQid(activate(V)))
    U62(tt()) -> tt()
    U71(tt(),V) ->
      U72(isNePal(activate(V)))
    U72(tt()) -> tt()
    and(tt(),X) -> activate(X)
    isList(V) ->
      U11(isPalListKind(activate(V))
         ,activate(V))
    isList(n__nil()) -> tt()
    isList(n____(V1,V2)) ->
      U21(and(isPalListKind(activate(V1))
             ,n__isPalListKind(activate(V2)))
         ,activate(V1)
         ,activate(V2))
    isNeList(V) ->
      U31(isPalListKind(activate(V))
         ,activate(V))
    isNeList(n____(V1,V2)) ->
      U41(and(isPalListKind(activate(V1))
             ,n__isPalListKind(activate(V2)))
         ,activate(V1)
         ,activate(V2))
    isNeList(n____(V1,V2)) ->
      U51(and(isPalListKind(activate(V1))
             ,n__isPalListKind(activate(V2)))
         ,activate(V1)
         ,activate(V2))
    isNePal(V) ->
      U61(isPalListKind(activate(V))
         ,activate(V))
    isNePal(n____(I,__(P,I))) ->
      and(and(isQid(activate(I))
             ,n__isPalListKind(activate(I)))
         ,n__and(isPal(activate(P))
                ,n__isPalListKind(activate(P))))
    isPal(V) ->
      U71(isPalListKind(activate(V))
         ,activate(V))
    isPal(n__nil()) -> tt()
    isPalListKind(n__a()) -> tt()
    isPalListKind(n__e()) -> tt()
    isPalListKind(n__i()) -> tt()
    isPalListKind(n__nil()) -> tt()
    isPalListKind(n__o()) -> tt()
    isPalListKind(n__u()) -> tt()
    isPalListKind(n____(V1,V2)) ->
      and(isPalListKind(activate(V1))
         ,n__isPalListKind(activate(V2)))
    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)
    isPalListKind(X) ->
      n__isPalListKind(X)
    and(X1,X2) -> n__and(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__isPalListKind(X)) ->
      isPalListKind(X)
    activate(n__and(X1,X2)) ->
      and(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)