YES TRS: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), U12(tt()) -> tt(), 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)), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isPalListKind(X)) -> isPalListKind(X), activate(n____(X1, X2)) -> __(X1, X2), 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(), U11(tt(), V) -> U12(isNeList(activate(V))), U22(tt(), V2) -> U23(isList(activate(V2))), 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)), U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)), U23(tt()) -> tt(), U32(tt()) -> tt(), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), U31(tt(), V) -> U32(isQid(activate(V))), U42(tt(), V2) -> U43(isNeList(activate(V2))), U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)), U43(tt()) -> tt(), U52(tt(), V2) -> U53(isList(activate(V2))), U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt()) -> tt(), U61(tt(), V) -> U62(isQid(activate(V))), U72(tt()) -> tt(), 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)))), U71(tt(), V) -> U72(isNePal(activate(V))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isPalListKind(X) -> n__isPalListKind(X), isPalListKind(n__nil()) -> tt(), isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind(n__a()) -> tt(), isPalListKind(n__e()) -> tt(), isPalListKind(n__i()) -> tt(), isPalListKind(n__o()) -> tt(), isPalListKind(n__u()) -> tt(), isPal(V) -> U71(isPalListKind(activate(V)), activate(V)), isPal(n__nil()) -> tt(), a() -> n__a(), e() -> n__e(), i() -> n__i(), o() -> n__o(), u() -> n__u()} DP: Strict: { __#(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(__(X, Y), Z) -> __#(Y, Z), isNeList#(V) -> activate#(V), isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V)), isNeList#(V) -> isPalListKind#(activate(V)), isNeList#(n____(V1, V2)) -> activate#(V1), isNeList#(n____(V1, V2)) -> activate#(V2), 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)), isNeList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), activate#(n__nil()) -> nil#(), activate#(n__isPalListKind(X)) -> isPalListKind#(X), activate#(n____(X1, X2)) -> __#(X1, X2), 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#(), U11#(tt(), V) -> U12#(isNeList(activate(V))), U11#(tt(), V) -> isNeList#(activate(V)), U11#(tt(), V) -> activate#(V), U22#(tt(), V2) -> activate#(V2), U22#(tt(), V2) -> isList#(activate(V2)), U22#(tt(), V2) -> U23#(isList(activate(V2))), isList#(V) -> activate#(V), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)), isList#(V) -> isPalListKind#(activate(V)), isList#(n____(V1, V2)) -> activate#(V1), isList#(n____(V1, V2)) -> activate#(V2), isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), isList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), U21#(tt(), V1, V2) -> activate#(V1), U21#(tt(), V1, V2) -> activate#(V2), U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)), U21#(tt(), V1, V2) -> isList#(activate(V1)), U31#(tt(), V) -> activate#(V), U31#(tt(), V) -> U32#(isQid(activate(V))), U31#(tt(), V) -> isQid#(activate(V)), U42#(tt(), V2) -> isNeList#(activate(V2)), U42#(tt(), V2) -> activate#(V2), U42#(tt(), V2) -> U43#(isNeList(activate(V2))), U41#(tt(), V1, V2) -> activate#(V1), U41#(tt(), V1, V2) -> activate#(V2), U41#(tt(), V1, V2) -> isList#(activate(V1)), U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)), U52#(tt(), V2) -> activate#(V2), U52#(tt(), V2) -> isList#(activate(V2)), U52#(tt(), V2) -> U53#(isList(activate(V2))), U51#(tt(), V1, V2) -> isNeList#(activate(V1)), U51#(tt(), V1, V2) -> activate#(V1), U51#(tt(), V1, V2) -> activate#(V2), U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2)), U61#(tt(), V) -> activate#(V), U61#(tt(), V) -> isQid#(activate(V)), U61#(tt(), V) -> U62#(isQid(activate(V))), isNePal#(V) -> activate#(V), isNePal#(V) -> U61#(isPalListKind(activate(V)), activate(V)), isNePal#(V) -> isPalListKind#(activate(V)), isNePal#(n____(I, __(P, I))) -> activate#(I), isNePal#(n____(I, __(P, I))) -> activate#(P), isNePal#(n____(I, __(P, I))) -> isQid#(activate(I)), isNePal#(n____(I, __(P, I))) -> and#(isQid(activate(I)), n__isPalListKind(activate(I))), isNePal#(n____(I, __(P, I))) -> and#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))), isNePal#(n____(I, __(P, I))) -> isPal#(activate(P)), U71#(tt(), V) -> activate#(V), U71#(tt(), V) -> U72#(isNePal(activate(V))), U71#(tt(), V) -> isNePal#(activate(V)), and#(tt(), X) -> activate#(X), isPalListKind#(n____(V1, V2)) -> activate#(V1), isPalListKind#(n____(V1, V2)) -> activate#(V2), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPal#(V) -> activate#(V), isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V)), isPal#(V) -> isPalListKind#(activate(V))} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), U12(tt()) -> tt(), 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)), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isPalListKind(X)) -> isPalListKind(X), activate(n____(X1, X2)) -> __(X1, X2), 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(), U11(tt(), V) -> U12(isNeList(activate(V))), U22(tt(), V2) -> U23(isList(activate(V2))), 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)), U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)), U23(tt()) -> tt(), U32(tt()) -> tt(), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), U31(tt(), V) -> U32(isQid(activate(V))), U42(tt(), V2) -> U43(isNeList(activate(V2))), U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)), U43(tt()) -> tt(), U52(tt(), V2) -> U53(isList(activate(V2))), U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt()) -> tt(), U61(tt(), V) -> U62(isQid(activate(V))), U72(tt()) -> tt(), 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)))), U71(tt(), V) -> U72(isNePal(activate(V))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isPalListKind(X) -> n__isPalListKind(X), isPalListKind(n__nil()) -> tt(), isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind(n__a()) -> tt(), isPalListKind(n__e()) -> tt(), isPalListKind(n__i()) -> tt(), isPalListKind(n__o()) -> tt(), isPalListKind(n__u()) -> tt(), isPal(V) -> U71(isPalListKind(activate(V)), activate(V)), isPal(n__nil()) -> tt(), a() -> n__a(), e() -> n__e(), i() -> n__i(), o() -> n__o(), u() -> n__u()} EDG: { (U11#(tt(), V) -> activate#(V), activate#(n__u()) -> u#()) (U11#(tt(), V) -> activate#(V), activate#(n__o()) -> o#()) (U11#(tt(), V) -> activate#(V), activate#(n__i()) -> i#()) (U11#(tt(), V) -> activate#(V), activate#(n__e()) -> e#()) (U11#(tt(), V) -> activate#(V), activate#(n__a()) -> a#()) (U11#(tt(), V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U11#(tt(), V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2)) (U11#(tt(), V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (U11#(tt(), V) -> activate#(V), activate#(n__nil()) -> nil#()) (U31#(tt(), V) -> activate#(V), activate#(n__u()) -> u#()) (U31#(tt(), V) -> activate#(V), activate#(n__o()) -> o#()) (U31#(tt(), V) -> activate#(V), activate#(n__i()) -> i#()) (U31#(tt(), V) -> activate#(V), activate#(n__e()) -> e#()) (U31#(tt(), V) -> activate#(V), activate#(n__a()) -> a#()) (U31#(tt(), V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U31#(tt(), V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2)) (U31#(tt(), V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (U31#(tt(), V) -> activate#(V), activate#(n__nil()) -> nil#()) (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__and(X1, X2)) -> and#(X1, X2)) (isNePal#(V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2)) (isNePal#(V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (isNePal#(V) -> activate#(V), activate#(n__nil()) -> nil#()) (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__and(X1, X2)) -> and#(X1, X2)) (isPal#(V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2)) (isPal#(V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (isPal#(V) -> activate#(V), activate#(n__nil()) -> nil#()) (isNePal#(n____(I, __(P, I))) -> and#(and(isQid(activate(I)), n__isPalListKind(activate(I))), n__and(isPal(activate(P)), n__isPalListKind(activate(P)))), and#(tt(), X) -> activate#(X)) (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__and(X1, X2)) -> and#(X1, X2)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> __#(X1, X2)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__u()) -> u#()) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__o()) -> o#()) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__i()) -> i#()) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__e()) -> e#()) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__a()) -> a#()) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n____(X1, X2)) -> __#(X1, X2)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (U41#(tt(), V1, V2) -> activate#(V1), activate#(n__nil()) -> nil#()) (isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__u()) -> u#()) (isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__o()) -> o#()) (isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__i()) -> i#()) (isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__e()) -> e#()) (isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__a()) -> a#()) (isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> __#(X1, X2)) (isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (isPalListKind#(n____(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNeList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), and#(tt(), X) -> activate#(X)) (isNePal#(n____(I, __(P, I))) -> and#(isQid(activate(I)), n__isPalListKind(activate(I))), and#(tt(), X) -> activate#(X)) (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__and(X1, X2)) -> and#(X1, X2)) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2)) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#()) (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__and(X1, X2)) -> and#(X1, X2)) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2)) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#()) (U42#(tt(), V2) -> activate#(V2), activate#(n__u()) -> u#()) (U42#(tt(), V2) -> activate#(V2), activate#(n__o()) -> o#()) (U42#(tt(), V2) -> activate#(V2), activate#(n__i()) -> i#()) (U42#(tt(), V2) -> activate#(V2), activate#(n__e()) -> e#()) (U42#(tt(), V2) -> activate#(V2), activate#(n__a()) -> a#()) (U42#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U42#(tt(), V2) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2)) (U42#(tt(), V2) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (U42#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (U52#(tt(), V2) -> activate#(V2), activate#(n__u()) -> u#()) (U52#(tt(), V2) -> activate#(V2), activate#(n__o()) -> o#()) (U52#(tt(), V2) -> activate#(V2), activate#(n__i()) -> i#()) (U52#(tt(), V2) -> activate#(V2), activate#(n__e()) -> e#()) (U52#(tt(), V2) -> activate#(V2), activate#(n__a()) -> a#()) (U52#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U52#(tt(), V2) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2)) (U52#(tt(), V2) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (U52#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__u()) -> u#()) (isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__o()) -> o#()) (isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__i()) -> i#()) (isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__e()) -> e#()) (isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__a()) -> a#()) (isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2)) (isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (isPalListKind#(n____(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#()) (and#(tt(), X) -> activate#(X), activate#(n__u()) -> u#()) (and#(tt(), X) -> activate#(X), activate#(n__o()) -> o#()) (and#(tt(), X) -> activate#(X), activate#(n__i()) -> i#()) (and#(tt(), X) -> activate#(X), activate#(n__e()) -> e#()) (and#(tt(), X) -> activate#(X), activate#(n__a()) -> a#()) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(X1, X2)) (and#(tt(), X) -> activate#(X), activate#(n____(X1, X2)) -> __#(X1, X2)) (and#(tt(), X) -> activate#(X), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (and#(tt(), X) -> activate#(X), activate#(n__nil()) -> nil#()) (isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2))) (isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U51#(tt(), V1, V2) -> activate#(V2)) (isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U51#(tt(), V1, V2) -> activate#(V1)) (isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U51#(tt(), V1, V2) -> isNeList#(activate(V1))) (isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__u()) -> u#()) (isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__o()) -> o#()) (isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__i()) -> i#()) (isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__e()) -> e#()) (isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__a()) -> a#()) (isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n____(X1, X2)) -> __#(X1, X2)) (isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (isNePal#(n____(I, __(P, I))) -> activate#(P), activate#(n__nil()) -> nil#()) (isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V)), U31#(tt(), V) -> isQid#(activate(V))) (isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V)), U31#(tt(), V) -> U32#(isQid(activate(V)))) (isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V)), U31#(tt(), V) -> activate#(V)) (U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)), U22#(tt(), V2) -> U23#(isList(activate(V2)))) (U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)), U22#(tt(), V2) -> isList#(activate(V2))) (U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)), U22#(tt(), V2) -> activate#(V2)) (U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2)), U52#(tt(), V2) -> U53#(isList(activate(V2)))) (U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2)), U52#(tt(), V2) -> isList#(activate(V2))) (U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2)), U52#(tt(), V2) -> activate#(V2)) (U22#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (U22#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (U22#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) (U22#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> activate#(V2)) (U22#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> activate#(V1)) (U22#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> isPalListKind#(activate(V))) (U22#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V))) (U22#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> activate#(V)) (U52#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (U52#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (U52#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) (U52#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> activate#(V2)) (U52#(tt(), V2) -> isList#(activate(V2)), isList#(n____(V1, V2)) -> activate#(V1)) (U52#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> isPalListKind#(activate(V))) (U52#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V))) (U52#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> activate#(V)) (activate#(n____(X1, X2)) -> __#(X1, X2), __#(__(X, Y), Z) -> __#(Y, Z)) (activate#(n____(X1, X2)) -> __#(X1, X2), __#(__(X, Y), Z) -> __#(X, __(Y, Z))) (isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> activate#(V2)) (isList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> activate#(V1)) (U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) (U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> activate#(V2)) (U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> activate#(V1)) (U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> isPalListKind#(activate(V))) (U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V))) (U41#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> activate#(V)) (isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> activate#(V2)) (isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> activate#(V1)) (U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) (U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) (U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> activate#(V2)) (U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> activate#(V1)) (U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(V) -> isPalListKind#(activate(V))) (U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V))) (U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(V) -> activate#(V)) (isNePal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (isNePal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (isNePal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V2)) (isNePal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V1)) (isPal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (isPal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (isPal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V2)) (isPal#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V1)) (U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(V) -> activate#(V)) (U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(V) -> U61#(isPalListKind(activate(V)), activate(V))) (U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(V) -> isPalListKind#(activate(V))) (U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(n____(I, __(P, I))) -> activate#(I)) (U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(n____(I, __(P, I))) -> activate#(P)) (U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(n____(I, __(P, I))) -> isQid#(activate(I))) (U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(n____(I, __(P, I))) -> and#(isQid(activate(I)), n__isPalListKind(activate(I)))) (U71#(tt(), V) -> isNePal#(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))))) (U71#(tt(), V) -> isNePal#(activate(V)), isNePal#(n____(I, __(P, I))) -> isPal#(activate(P))) (isList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V1)) (isList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V2)) (isList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (isList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (isNeList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V1)) (isNeList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> activate#(V2)) (isNeList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (isNeList#(V) -> isPalListKind#(activate(V)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(V) -> activate#(V)) (U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V))) (U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(V) -> isPalListKind#(activate(V))) (U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> activate#(V1)) (U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> activate#(V2)) (U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) (U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) (U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (U51#(tt(), V1, V2) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> activate#(V)) (U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V))) (U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> isPalListKind#(activate(V))) (U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> activate#(V1)) (U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> activate#(V2)) (U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) (U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)) (isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> activate#(V1)) (isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> activate#(V2)) (isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1)), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(V) -> activate#(V)) (U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(V) -> U31#(isPalListKind(activate(V)), activate(V))) (U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(V) -> isPalListKind#(activate(V))) (U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(n____(V1, V2)) -> activate#(V1)) (U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(n____(V1, V2)) -> activate#(V2)) (U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) (U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) (U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (U42#(tt(), V2) -> isNeList#(activate(V2)), isNeList#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V)), U71#(tt(), V) -> activate#(V)) (isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V)), U71#(tt(), V) -> U72#(isNePal(activate(V)))) (isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V)), U71#(tt(), V) -> isNePal#(activate(V))) (isNePal#(V) -> U61#(isPalListKind(activate(V)), activate(V)), U61#(tt(), V) -> activate#(V)) (isNePal#(V) -> U61#(isPalListKind(activate(V)), activate(V)), U61#(tt(), V) -> isQid#(activate(V))) (isNePal#(V) -> U61#(isPalListKind(activate(V)), activate(V)), U61#(tt(), V) -> U62#(isQid(activate(V)))) (U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)), U42#(tt(), V2) -> isNeList#(activate(V2))) (U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)), U42#(tt(), V2) -> activate#(V2)) (U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)), U42#(tt(), V2) -> U43#(isNeList(activate(V2)))) (isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)), U11#(tt(), V) -> U12#(isNeList(activate(V)))) (isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)), U11#(tt(), V) -> isNeList#(activate(V))) (isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)), U11#(tt(), V) -> activate#(V)) (isNePal#(n____(I, __(P, I))) -> isPal#(activate(P)), isPal#(V) -> activate#(V)) (isNePal#(n____(I, __(P, I))) -> isPal#(activate(P)), isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V))) (isNePal#(n____(I, __(P, I))) -> isPal#(activate(P)), isPal#(V) -> isPalListKind#(activate(V))) (isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U21#(tt(), V1, V2) -> activate#(V1)) (isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U21#(tt(), V1, V2) -> activate#(V2)) (isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2))) (isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U21#(tt(), V1, V2) -> isList#(activate(V1))) (isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> activate#(V1)) (isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> activate#(V2)) (isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> isList#(activate(V1))) (isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2))) (isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__nil()) -> nil#()) (isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n____(X1, X2)) -> __#(X1, X2)) (isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__a()) -> a#()) (isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__e()) -> e#()) (isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__i()) -> i#()) (isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__o()) -> o#()) (isNePal#(n____(I, __(P, I))) -> activate#(I), activate#(n__u()) -> u#()) (activate#(n__isPalListKind(X)) -> isPalListKind#(X), isPalListKind#(n____(V1, V2)) -> activate#(V1)) (activate#(n__isPalListKind(X)) -> isPalListKind#(X), isPalListKind#(n____(V1, V2)) -> activate#(V2)) (activate#(n__isPalListKind(X)) -> isPalListKind#(X), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2)))) (activate#(n__isPalListKind(X)) -> isPalListKind#(X), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1))) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__a()) -> a#()) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__e()) -> e#()) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__i()) -> i#()) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__o()) -> o#()) (U51#(tt(), V1, V2) -> activate#(V2), activate#(n__u()) -> u#()) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__a()) -> a#()) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__e()) -> e#()) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__i()) -> i#()) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__o()) -> o#()) (U41#(tt(), V1, V2) -> activate#(V2), activate#(n__u()) -> u#()) (U21#(tt(), V1, V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (U21#(tt(), V1, V2) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (U21#(tt(), V1, V2) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2)) (U21#(tt(), V1, V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U21#(tt(), V1, V2) -> activate#(V2), activate#(n__a()) -> a#()) (U21#(tt(), V1, V2) -> activate#(V2), activate#(n__e()) -> e#()) (U21#(tt(), V1, V2) -> activate#(V2), activate#(n__i()) -> i#()) (U21#(tt(), V1, V2) -> activate#(V2), activate#(n__o()) -> o#()) (U21#(tt(), V1, V2) -> activate#(V2), activate#(n__u()) -> u#()) (U22#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#()) (U22#(tt(), V2) -> activate#(V2), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (U22#(tt(), V2) -> activate#(V2), activate#(n____(X1, X2)) -> __#(X1, X2)) (U22#(tt(), V2) -> activate#(V2), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U22#(tt(), V2) -> activate#(V2), activate#(n__a()) -> a#()) (U22#(tt(), V2) -> activate#(V2), activate#(n__e()) -> e#()) (U22#(tt(), V2) -> activate#(V2), activate#(n__i()) -> i#()) (U22#(tt(), V2) -> activate#(V2), activate#(n__o()) -> o#()) (U22#(tt(), V2) -> activate#(V2), activate#(n__u()) -> u#()) (isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), and#(tt(), X) -> activate#(X)) (isList#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), and#(tt(), X) -> activate#(X)) (__#(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(__(X, Y), Z) -> __#(X, __(Y, Z))) (__#(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(__(X, Y), Z) -> __#(Y, Z)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__nil()) -> nil#()) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n____(X1, X2)) -> __#(X1, X2)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__a()) -> a#()) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__e()) -> e#()) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__i()) -> i#()) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__o()) -> o#()) (U51#(tt(), V1, V2) -> activate#(V1), activate#(n__u()) -> u#()) (U21#(tt(), V1, V2) -> activate#(V1), activate#(n__nil()) -> nil#()) (U21#(tt(), V1, V2) -> activate#(V1), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (U21#(tt(), V1, V2) -> activate#(V1), activate#(n____(X1, X2)) -> __#(X1, X2)) (U21#(tt(), V1, V2) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U21#(tt(), V1, V2) -> activate#(V1), activate#(n__a()) -> a#()) (U21#(tt(), V1, V2) -> activate#(V1), activate#(n__e()) -> e#()) (U21#(tt(), V1, V2) -> activate#(V1), activate#(n__i()) -> i#()) (U21#(tt(), V1, V2) -> activate#(V1), activate#(n__o()) -> o#()) (U21#(tt(), V1, V2) -> activate#(V1), activate#(n__u()) -> u#()) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> __#(X1, X2)) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__a()) -> a#()) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__e()) -> e#()) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__i()) -> i#()) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__o()) -> o#()) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__u()) -> u#()) (__#(__(X, Y), Z) -> __#(Y, Z), __#(__(X, Y), Z) -> __#(X, __(Y, Z))) (__#(__(X, Y), Z) -> __#(Y, Z), __#(__(X, Y), Z) -> __#(Y, Z)) (U71#(tt(), V) -> activate#(V), activate#(n__nil()) -> nil#()) (U71#(tt(), V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (U71#(tt(), V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2)) (U71#(tt(), V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U71#(tt(), V) -> activate#(V), activate#(n__a()) -> a#()) (U71#(tt(), V) -> activate#(V), activate#(n__e()) -> e#()) (U71#(tt(), V) -> activate#(V), activate#(n__i()) -> i#()) (U71#(tt(), V) -> activate#(V), activate#(n__o()) -> o#()) (U71#(tt(), V) -> activate#(V), activate#(n__u()) -> u#()) (U61#(tt(), V) -> activate#(V), activate#(n__nil()) -> nil#()) (U61#(tt(), V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (U61#(tt(), V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2)) (U61#(tt(), V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2)) (U61#(tt(), V) -> activate#(V), activate#(n__a()) -> a#()) (U61#(tt(), V) -> activate#(V), activate#(n__e()) -> e#()) (U61#(tt(), V) -> activate#(V), activate#(n__i()) -> i#()) (U61#(tt(), V) -> activate#(V), activate#(n__o()) -> o#()) (U61#(tt(), V) -> activate#(V), activate#(n__u()) -> u#()) (isList#(V) -> activate#(V), activate#(n__nil()) -> nil#()) (isList#(V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (isList#(V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2)) (isList#(V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isList#(V) -> activate#(V), activate#(n__a()) -> a#()) (isList#(V) -> activate#(V), activate#(n__e()) -> e#()) (isList#(V) -> activate#(V), activate#(n__i()) -> i#()) (isList#(V) -> activate#(V), activate#(n__o()) -> o#()) (isList#(V) -> activate#(V), activate#(n__u()) -> u#()) (isNeList#(V) -> activate#(V), activate#(n__nil()) -> nil#()) (isNeList#(V) -> activate#(V), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (isNeList#(V) -> activate#(V), activate#(n____(X1, X2)) -> __#(X1, X2)) (isNeList#(V) -> activate#(V), activate#(n__and(X1, X2)) -> and#(X1, X2)) (isNeList#(V) -> activate#(V), activate#(n__a()) -> a#()) (isNeList#(V) -> activate#(V), activate#(n__e()) -> e#()) (isNeList#(V) -> activate#(V), activate#(n__i()) -> i#()) (isNeList#(V) -> activate#(V), activate#(n__o()) -> o#()) (isNeList#(V) -> activate#(V), activate#(n__u()) -> u#()) } SCCS: Scc: {isNePal#(n____(I, __(P, I))) -> isPal#(activate(P)), U71#(tt(), V) -> isNePal#(activate(V)), isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V))} Scc: {activate#(n__isPalListKind(X)) -> isPalListKind#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X), isPalListKind#(n____(V1, V2)) -> activate#(V1), isPalListKind#(n____(V1, V2)) -> activate#(V2), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1))} Scc: {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)), U11#(tt(), V) -> isNeList#(activate(V)), U22#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)), isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)), U21#(tt(), V1, V2) -> isList#(activate(V1)), U42#(tt(), V2) -> isNeList#(activate(V2)), U41#(tt(), V1, V2) -> isList#(activate(V1)), U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)), U52#(tt(), V2) -> isList#(activate(V2)), U51#(tt(), V1, V2) -> isNeList#(activate(V1)), U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2))} Scc: {__#(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(__(X, Y), Z) -> __#(Y, Z)} SCC: Strict: {isNePal#(n____(I, __(P, I))) -> isPal#(activate(P)), U71#(tt(), V) -> isNePal#(activate(V)), isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V))} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), U12(tt()) -> tt(), 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)), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isPalListKind(X)) -> isPalListKind(X), activate(n____(X1, X2)) -> __(X1, X2), 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(), U11(tt(), V) -> U12(isNeList(activate(V))), U22(tt(), V2) -> U23(isList(activate(V2))), 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)), U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)), U23(tt()) -> tt(), U32(tt()) -> tt(), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), U31(tt(), V) -> U32(isQid(activate(V))), U42(tt(), V2) -> U43(isNeList(activate(V2))), U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)), U43(tt()) -> tt(), U52(tt(), V2) -> U53(isList(activate(V2))), U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt()) -> tt(), U61(tt(), V) -> U62(isQid(activate(V))), U72(tt()) -> tt(), 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)))), U71(tt(), V) -> U72(isNePal(activate(V))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isPalListKind(X) -> n__isPalListKind(X), isPalListKind(n__nil()) -> tt(), isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind(n__a()) -> tt(), isPalListKind(n__e()) -> tt(), isPalListKind(n__i()) -> tt(), isPalListKind(n__o()) -> tt(), isPalListKind(n__u()) -> tt(), isPal(V) -> U71(isPalListKind(activate(V)), activate(V)), isPal(n__nil()) -> tt(), a() -> n__a(), e() -> n__e(), i() -> n__i(), o() -> n__o(), u() -> n__u()} POLY: Argument Filtering: pi(u) = [], pi(o) = [], pi(i) = [], pi(e) = [], pi(a) = [], pi(n__u) = [], pi(n__o) = [], pi(n__i) = [], pi(n__e) = [], pi(n__a) = [], pi(isPal#) = 0, pi(isPal) = [], pi(n__and) = 1, pi(n____) = [0,1], pi(n__isPalListKind) = [], pi(n__nil) = [], pi(isPalListKind) = [], pi(and) = 1, pi(U71#) = 1, pi(U71) = [], pi(isNePal#) = 0, pi(isNePal) = [], pi(U72) = [], pi(U61) = [], pi(U62) = [], pi(U53) = [], pi(U51) = [], pi(U52) = [], pi(U43) = [], pi(U41) = [], pi(U42) = [], pi(U31) = [], pi(isQid) = [], pi(U32) = [], pi(U23) = [], pi(U21) = [], pi(isList) = [], pi(U22) = [], pi(tt) = [], pi(U11) = [], pi(activate) = 0, pi(isNeList) = [], pi(U12) = [], pi(nil) = [], pi(__) = [0,1] Usable Rules: {} Interpretation: [n____](x0, x1) = x0 + x1 + 1, [__](x0, x1) = x0 + x1 + 1 Strict: {U71#(tt(), V) -> isNePal#(activate(V)), isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V))} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), U12(tt()) -> tt(), 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)), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isPalListKind(X)) -> isPalListKind(X), activate(n____(X1, X2)) -> __(X1, X2), 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(), U11(tt(), V) -> U12(isNeList(activate(V))), U22(tt(), V2) -> U23(isList(activate(V2))), 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)), U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)), U23(tt()) -> tt(), U32(tt()) -> tt(), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), U31(tt(), V) -> U32(isQid(activate(V))), U42(tt(), V2) -> U43(isNeList(activate(V2))), U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)), U43(tt()) -> tt(), U52(tt(), V2) -> U53(isList(activate(V2))), U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt()) -> tt(), U61(tt(), V) -> U62(isQid(activate(V))), U72(tt()) -> tt(), 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)))), U71(tt(), V) -> U72(isNePal(activate(V))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isPalListKind(X) -> n__isPalListKind(X), isPalListKind(n__nil()) -> tt(), isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind(n__a()) -> tt(), isPalListKind(n__e()) -> tt(), isPalListKind(n__i()) -> tt(), isPalListKind(n__o()) -> tt(), isPalListKind(n__u()) -> tt(), isPal(V) -> U71(isPalListKind(activate(V)), activate(V)), isPal(n__nil()) -> tt(), a() -> n__a(), e() -> n__e(), i() -> n__i(), o() -> n__o(), u() -> n__u()} EDG: {(isPal#(V) -> U71#(isPalListKind(activate(V)), activate(V)), U71#(tt(), V) -> isNePal#(activate(V)))} SCCS: Qed SCC: Strict: {activate#(n__isPalListKind(X)) -> isPalListKind#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X), isPalListKind#(n____(V1, V2)) -> activate#(V1), isPalListKind#(n____(V1, V2)) -> activate#(V2), isPalListKind#(n____(V1, V2)) -> and#(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind#(n____(V1, V2)) -> isPalListKind#(activate(V1))} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), U12(tt()) -> tt(), 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)), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isPalListKind(X)) -> isPalListKind(X), activate(n____(X1, X2)) -> __(X1, X2), 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(), U11(tt(), V) -> U12(isNeList(activate(V))), U22(tt(), V2) -> U23(isList(activate(V2))), 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)), U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)), U23(tt()) -> tt(), U32(tt()) -> tt(), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), U31(tt(), V) -> U32(isQid(activate(V))), U42(tt(), V2) -> U43(isNeList(activate(V2))), U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)), U43(tt()) -> tt(), U52(tt(), V2) -> U53(isList(activate(V2))), U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt()) -> tt(), U61(tt(), V) -> U62(isQid(activate(V))), U72(tt()) -> tt(), 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)))), U71(tt(), V) -> U72(isNePal(activate(V))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isPalListKind(X) -> n__isPalListKind(X), isPalListKind(n__nil()) -> tt(), isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind(n__a()) -> tt(), isPalListKind(n__e()) -> tt(), isPalListKind(n__i()) -> tt(), isPalListKind(n__o()) -> tt(), isPalListKind(n__u()) -> tt(), isPal(V) -> U71(isPalListKind(activate(V)), activate(V)), isPal(n__nil()) -> tt(), a() -> n__a(), e() -> n__e(), i() -> n__i(), o() -> n__o(), u() -> n__u()} POLY: Argument Filtering: pi(u) = [], pi(o) = [], pi(i) = [], pi(e) = [], pi(a) = [], pi(n__u) = [], pi(n__o) = [], pi(n__i) = [], pi(n__e) = [], pi(n__a) = [], pi(isPal) = [], pi(n__and) = 1, pi(n____) = [0,1], pi(n__isPalListKind) = 0, pi(n__nil) = [], pi(isPalListKind#) = 0, pi(isPalListKind) = 0, pi(and#) = 1, pi(and) = 1, pi(U71) = [], pi(isNePal) = [], pi(U72) = [], pi(U61) = [], pi(U62) = [], pi(U53) = [], pi(U51) = [], pi(U52) = [], pi(U43) = [], pi(U41) = [], pi(U42) = [], pi(U31) = [], pi(isQid) = [], pi(U32) = [], pi(U23) = [], pi(U21) = [], pi(isList) = [], pi(U22) = [], pi(tt) = [], pi(U11) = [], pi(activate#) = 0, pi(activate) = 0, pi(isNeList) = [], pi(U12) = [], pi(nil) = [], pi(__) = [0,1] Usable Rules: {} Interpretation: [n____](x0, x1) = x0 + x1 + 1 Strict: {activate#(n__isPalListKind(X)) -> isPalListKind#(X), activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), U12(tt()) -> tt(), 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)), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isPalListKind(X)) -> isPalListKind(X), activate(n____(X1, X2)) -> __(X1, X2), 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(), U11(tt(), V) -> U12(isNeList(activate(V))), U22(tt(), V2) -> U23(isList(activate(V2))), 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)), U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)), U23(tt()) -> tt(), U32(tt()) -> tt(), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), U31(tt(), V) -> U32(isQid(activate(V))), U42(tt(), V2) -> U43(isNeList(activate(V2))), U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)), U43(tt()) -> tt(), U52(tt(), V2) -> U53(isList(activate(V2))), U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt()) -> tt(), U61(tt(), V) -> U62(isQid(activate(V))), U72(tt()) -> tt(), 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)))), U71(tt(), V) -> U72(isNePal(activate(V))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isPalListKind(X) -> n__isPalListKind(X), isPalListKind(n__nil()) -> tt(), isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind(n__a()) -> tt(), isPalListKind(n__e()) -> tt(), isPalListKind(n__i()) -> tt(), isPalListKind(n__o()) -> tt(), isPalListKind(n__u()) -> tt(), isPal(V) -> U71(isPalListKind(activate(V)), activate(V)), isPal(n__nil()) -> tt(), a() -> n__a(), e() -> n__e(), i() -> n__i(), o() -> n__o(), u() -> n__u()} EDG: {(and#(tt(), X) -> activate#(X), activate#(n__isPalListKind(X)) -> isPalListKind#(X)) (and#(tt(), X) -> activate#(X), activate#(n__and(X1, X2)) -> and#(X1, X2)) (activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X))} SCCS: Scc: {activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)} SCC: Strict: {activate#(n__and(X1, X2)) -> and#(X1, X2), and#(tt(), X) -> activate#(X)} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), U12(tt()) -> tt(), 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)), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isPalListKind(X)) -> isPalListKind(X), activate(n____(X1, X2)) -> __(X1, X2), 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(), U11(tt(), V) -> U12(isNeList(activate(V))), U22(tt(), V2) -> U23(isList(activate(V2))), 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)), U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)), U23(tt()) -> tt(), U32(tt()) -> tt(), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), U31(tt(), V) -> U32(isQid(activate(V))), U42(tt(), V2) -> U43(isNeList(activate(V2))), U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)), U43(tt()) -> tt(), U52(tt(), V2) -> U53(isList(activate(V2))), U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt()) -> tt(), U61(tt(), V) -> U62(isQid(activate(V))), U72(tt()) -> tt(), 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)))), U71(tt(), V) -> U72(isNePal(activate(V))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isPalListKind(X) -> n__isPalListKind(X), isPalListKind(n__nil()) -> tt(), isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind(n__a()) -> tt(), isPalListKind(n__e()) -> tt(), isPalListKind(n__i()) -> tt(), isPalListKind(n__o()) -> tt(), isPalListKind(n__u()) -> tt(), isPal(V) -> U71(isPalListKind(activate(V)), activate(V)), isPal(n__nil()) -> tt(), a() -> n__a(), e() -> n__e(), i() -> n__i(), o() -> n__o(), u() -> n__u()} SPSC: Simple Projection: pi(and#) = 1, pi(activate#) = 0 Strict: {and#(tt(), X) -> activate#(X)} EDG: {} SCCS: Qed SCC: Strict: {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)), U11#(tt(), V) -> isNeList#(activate(V)), U22#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)), isList#(n____(V1, V2)) -> U21#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)), U21#(tt(), V1, V2) -> isList#(activate(V1)), U42#(tt(), V2) -> isNeList#(activate(V2)), U41#(tt(), V1, V2) -> isList#(activate(V1)), U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)), U52#(tt(), V2) -> isList#(activate(V2)), U51#(tt(), V1, V2) -> isNeList#(activate(V1)), U51#(tt(), V1, V2) -> U52#(isNeList(activate(V1)), activate(V2))} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), U12(tt()) -> tt(), 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)), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isPalListKind(X)) -> isPalListKind(X), activate(n____(X1, X2)) -> __(X1, X2), 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(), U11(tt(), V) -> U12(isNeList(activate(V))), U22(tt(), V2) -> U23(isList(activate(V2))), 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)), U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)), U23(tt()) -> tt(), U32(tt()) -> tt(), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), U31(tt(), V) -> U32(isQid(activate(V))), U42(tt(), V2) -> U43(isNeList(activate(V2))), U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)), U43(tt()) -> tt(), U52(tt(), V2) -> U53(isList(activate(V2))), U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt()) -> tt(), U61(tt(), V) -> U62(isQid(activate(V))), U72(tt()) -> tt(), 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)))), U71(tt(), V) -> U72(isNePal(activate(V))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isPalListKind(X) -> n__isPalListKind(X), isPalListKind(n__nil()) -> tt(), isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind(n__a()) -> tt(), isPalListKind(n__e()) -> tt(), isPalListKind(n__i()) -> tt(), isPalListKind(n__o()) -> tt(), isPalListKind(n__u()) -> tt(), isPal(V) -> U71(isPalListKind(activate(V)), activate(V)), isPal(n__nil()) -> tt(), a() -> n__a(), e() -> n__e(), i() -> n__i(), o() -> n__o(), u() -> n__u()} POLY: Argument Filtering: pi(u) = [], pi(o) = [], pi(i) = [], pi(e) = [], pi(a) = [], pi(n__u) = [], pi(n__o) = [], pi(n__i) = [], pi(n__e) = [], pi(n__a) = [], pi(isPal) = [], pi(n__and) = 1, pi(n____) = [0,1], pi(n__isPalListKind) = [], pi(n__nil) = [], pi(isPalListKind) = [], pi(and) = 1, pi(U71) = [], pi(isNePal) = [], pi(U72) = [], pi(U61) = [], pi(U62) = [], pi(U53) = [], pi(U51#) = [0,1,2], pi(U51) = [], pi(U52#) = [1], pi(U52) = [], pi(U43) = [], pi(U41#) = [0,1,2], pi(U41) = [], pi(U42#) = [0,1], pi(U42) = [], pi(U31) = [], pi(isQid) = [], pi(U32) = [], pi(U23) = 0, pi(U21#) = [0,1,2], pi(U21) = [0,2], pi(isList#) = [0], pi(isList) = [0], pi(U22#) = [0,1], pi(U22) = [1], pi(tt) = [], pi(U11#) = [1], pi(U11) = [], pi(activate) = 0, pi(isNeList#) = [0], pi(isNeList) = [], pi(U12) = [], pi(nil) = [], pi(__) = [0,1] Usable Rules: {} Interpretation: [U51#](x0, x1, x2) = x0 + x1 + x2 + 1, [U41#](x0, x1, x2) = x0 + x1 + x2 + 1, [U21#](x0, x1, x2) = x0 + x1 + x2, [U52#](x0) = x0 + 1, [U42#](x0, x1) = x0 + x1 + 1, [U22#](x0, x1) = x0 + x1, [U11#](x0) = x0 + 1, [isList#](x0) = x0 + 1, [isNeList#](x0) = x0 + 1, [n____](x0, x1) = x0 + x1 + 1, [n__isPalListKind] = 1, [isList](x0) = x0 + 1, [tt] = 1 Strict: {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)), U11#(tt(), V) -> isNeList#(activate(V)), U22#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)), U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)), U21#(tt(), V1, V2) -> isList#(activate(V1)), U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2)), U52#(tt(), V2) -> isList#(activate(V2))} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), U12(tt()) -> tt(), 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)), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isPalListKind(X)) -> isPalListKind(X), activate(n____(X1, X2)) -> __(X1, X2), 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(), U11(tt(), V) -> U12(isNeList(activate(V))), U22(tt(), V2) -> U23(isList(activate(V2))), 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)), U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)), U23(tt()) -> tt(), U32(tt()) -> tt(), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), U31(tt(), V) -> U32(isQid(activate(V))), U42(tt(), V2) -> U43(isNeList(activate(V2))), U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)), U43(tt()) -> tt(), U52(tt(), V2) -> U53(isList(activate(V2))), U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt()) -> tt(), U61(tt(), V) -> U62(isQid(activate(V))), U72(tt()) -> tt(), 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)))), U71(tt(), V) -> U72(isNePal(activate(V))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isPalListKind(X) -> n__isPalListKind(X), isPalListKind(n__nil()) -> tt(), isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind(n__a()) -> tt(), isPalListKind(n__e()) -> tt(), isPalListKind(n__i()) -> tt(), isPalListKind(n__o()) -> tt(), isPalListKind(n__u()) -> tt(), isPal(V) -> U71(isPalListKind(activate(V)), activate(V)), isPal(n__nil()) -> tt(), a() -> n__a(), e() -> n__e(), i() -> n__i(), o() -> n__o(), u() -> n__u()} EDG: {(U52#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V))) (U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> U51#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) (U11#(tt(), V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2))) (U21#(tt(), V1, V2) -> U22#(isList(activate(V1)), activate(V2)), U22#(tt(), V2) -> isList#(activate(V2))) (isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)), U11#(tt(), V) -> isNeList#(activate(V))) (isNeList#(n____(V1, V2)) -> U41#(and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), activate(V1), activate(V2)), U41#(tt(), V1, V2) -> U42#(isList(activate(V1)), activate(V2))) (U21#(tt(), V1, V2) -> isList#(activate(V1)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V))) (U22#(tt(), V2) -> isList#(activate(V2)), isList#(V) -> U11#(isPalListKind(activate(V)), activate(V)))} SCCS: Qed SCC: Strict: {__#(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(__(X, Y), Z) -> __#(Y, Z)} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), U12(tt()) -> tt(), 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)), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isPalListKind(X)) -> isPalListKind(X), activate(n____(X1, X2)) -> __(X1, X2), 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(), U11(tt(), V) -> U12(isNeList(activate(V))), U22(tt(), V2) -> U23(isList(activate(V2))), 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)), U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)), U23(tt()) -> tt(), U32(tt()) -> tt(), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), U31(tt(), V) -> U32(isQid(activate(V))), U42(tt(), V2) -> U43(isNeList(activate(V2))), U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)), U43(tt()) -> tt(), U52(tt(), V2) -> U53(isList(activate(V2))), U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt()) -> tt(), U61(tt(), V) -> U62(isQid(activate(V))), U72(tt()) -> tt(), 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)))), U71(tt(), V) -> U72(isNePal(activate(V))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isPalListKind(X) -> n__isPalListKind(X), isPalListKind(n__nil()) -> tt(), isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind(n__a()) -> tt(), isPalListKind(n__e()) -> tt(), isPalListKind(n__i()) -> tt(), isPalListKind(n__o()) -> tt(), isPalListKind(n__u()) -> tt(), isPal(V) -> U71(isPalListKind(activate(V)), activate(V)), isPal(n__nil()) -> tt(), a() -> n__a(), e() -> n__e(), i() -> n__i(), o() -> n__o(), u() -> n__u()} SPSC: Simple Projection: pi(__#) = 0 Strict: {__#(__(X, Y), Z) -> __#(Y, Z)} EDG: {(__#(__(X, Y), Z) -> __#(Y, Z), __#(__(X, Y), Z) -> __#(Y, Z))} SCCS: Scc: {__#(__(X, Y), Z) -> __#(Y, Z)} SCC: Strict: {__#(__(X, Y), Z) -> __#(Y, Z)} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), U12(tt()) -> tt(), 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)), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isPalListKind(X)) -> isPalListKind(X), activate(n____(X1, X2)) -> __(X1, X2), 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(), U11(tt(), V) -> U12(isNeList(activate(V))), U22(tt(), V2) -> U23(isList(activate(V2))), 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)), U21(tt(), V1, V2) -> U22(isList(activate(V1)), activate(V2)), U23(tt()) -> tt(), U32(tt()) -> tt(), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), U31(tt(), V) -> U32(isQid(activate(V))), U42(tt(), V2) -> U43(isNeList(activate(V2))), U41(tt(), V1, V2) -> U42(isList(activate(V1)), activate(V2)), U43(tt()) -> tt(), U52(tt(), V2) -> U53(isList(activate(V2))), U51(tt(), V1, V2) -> U52(isNeList(activate(V1)), activate(V2)), U53(tt()) -> tt(), U62(tt()) -> tt(), U61(tt(), V) -> U62(isQid(activate(V))), U72(tt()) -> tt(), 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)))), U71(tt(), V) -> U72(isNePal(activate(V))), and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate(X), isPalListKind(X) -> n__isPalListKind(X), isPalListKind(n__nil()) -> tt(), isPalListKind(n____(V1, V2)) -> and(isPalListKind(activate(V1)), n__isPalListKind(activate(V2))), isPalListKind(n__a()) -> tt(), isPalListKind(n__e()) -> tt(), isPalListKind(n__i()) -> tt(), isPalListKind(n__o()) -> tt(), isPalListKind(n__u()) -> tt(), isPal(V) -> U71(isPalListKind(activate(V)), activate(V)), isPal(n__nil()) -> tt(), a() -> n__a(), e() -> n__e(), i() -> n__i(), o() -> n__o(), u() -> n__u()} SPSC: Simple Projection: pi(__#) = 0 Strict: {} Qed