(VAR I P V V1 V2 X X1 X2 Y Z )
(RULES 
        a____(__(X, Y), Z) -> a____(mark(X), a____(mark(Y), mark(Z)))
        a____(X, nil) -> mark(X)
        a____(nil, X) -> mark(X)
        a__and(tt, X) -> mark(X)
        a__isList(V) -> a__isNeList(V)
        a__isList(nil) -> tt
        a__isList(__(V1, V2)) -> a__and(a__isList(V1), isList(V2))
        a__isNeList(V) -> a__isQid(V)
        a__isNeList(__(V1, V2)) -> a__and(a__isList(V1), isNeList(V2))
        a__isNeList(__(V1, V2)) -> a__and(a__isNeList(V1), isList(V2))
        a__isNePal(V) -> a__isQid(V)
        a__isNePal(__(I, __(P, I))) -> a__and(a__isQid(I), isPal(P))
        a__isPal(V) -> a__isNePal(V)
        a__isPal(nil) -> tt
        a__isQid(a) -> tt
        a__isQid(e) -> tt
        a__isQid(i) -> tt
        a__isQid(o) -> tt
        a__isQid(u) -> tt
        mark(__(X1, X2)) -> a____(mark(X1), mark(X2))
        mark(and(X1, X2)) -> a__and(mark(X1), X2)
        mark(isList(X)) -> a__isList(X)
        mark(isNeList(X)) -> a__isNeList(X)
        mark(isQid(X)) -> a__isQid(X)
        mark(isNePal(X)) -> a__isNePal(X)
        mark(isPal(X)) -> a__isPal(X)
        mark(nil) -> nil
        mark(tt) -> tt
        mark(a) -> a
        mark(e) -> e
        mark(i) -> i
        mark(o) -> o
        mark(u) -> u
        a____(X1, X2) -> __(X1, X2)
        a__and(X1, X2) -> and(X1, X2)
        a__isList(X) -> isList(X)
        a__isNeList(X) -> isNeList(X)
        a__isQid(X) -> isQid(X)
        a__isNePal(X) -> isNePal(X)
        a__isPal(X) -> isPal(X)
        
)