YES TRS: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isList(X)) -> isList(X), activate(n____(X1, X2)) -> __(activate(X1), activate(X2)), activate(n__isNeList(X)) -> isNeList(X), activate(n__isPal(X)) -> isPal(X), activate(n__a()) -> a(), activate(n__e()) -> e(), activate(n__i()) -> i(), activate(n__o()) -> o(), activate(n__u()) -> u(), and(tt(), X) -> activate(X), isNeList(X) -> n__isNeList(X), isNeList(V) -> isQid(activate(V)), isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))), isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))), isList(X) -> n__isList(X), isList(V) -> isNeList(activate(V)), isList(n__nil()) -> tt(), isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), isNePal(V) -> isQid(activate(V)), isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))), isPal(X) -> n__isPal(X), isPal(V) -> isNePal(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), activate#(n__nil()) -> nil#(), activate#(n__isList(X)) -> isList#(X), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2)), activate#(n____(X1, X2)) -> activate#(X1), activate#(n____(X1, X2)) -> activate#(X2), activate#(n__isNeList(X)) -> isNeList#(X), activate#(n__isPal(X)) -> isPal#(X), activate#(n__a()) -> a#(), activate#(n__e()) -> e#(), activate#(n__i()) -> i#(), activate#(n__o()) -> o#(), activate#(n__u()) -> u#(), and#(tt(), X) -> activate#(X), isNeList#(V) -> activate#(V), isNeList#(V) -> isQid#(activate(V)), isNeList#(n____(V1, V2)) -> activate#(V1), isNeList#(n____(V1, V2)) -> activate#(V2), isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2))), isNeList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isNeList(activate(V2))), isNeList#(n____(V1, V2)) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> activate#(V), isList#(V) -> isNeList#(activate(V)), isList#(n____(V1, V2)) -> activate#(V1), isList#(n____(V1, V2)) -> activate#(V2), isList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2))), isList#(n____(V1, V2)) -> isList#(activate(V1)), isNePal#(V) -> activate#(V), isNePal#(V) -> isQid#(activate(V)), isNePal#(n____(I, n____(P, I))) -> activate#(I), isNePal#(n____(I, n____(P, I))) -> activate#(P), isNePal#(n____(I, n____(P, I))) -> and#(isQid(activate(I)), n__isPal(activate(P))), isNePal#(n____(I, n____(P, I))) -> isQid#(activate(I)), isPal#(V) -> activate#(V), isPal#(V) -> isNePal#(activate(V))} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isList(X)) -> isList(X), activate(n____(X1, X2)) -> __(activate(X1), activate(X2)), activate(n__isNeList(X)) -> isNeList(X), activate(n__isPal(X)) -> isPal(X), activate(n__a()) -> a(), activate(n__e()) -> e(), activate(n__i()) -> i(), activate(n__o()) -> o(), activate(n__u()) -> u(), and(tt(), X) -> activate(X), isNeList(X) -> n__isNeList(X), isNeList(V) -> isQid(activate(V)), isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))), isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))), isList(X) -> n__isList(X), isList(V) -> isNeList(activate(V)), isList(n__nil()) -> tt(), isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), isNePal(V) -> isQid(activate(V)), isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))), isPal(X) -> n__isPal(X), isPal(V) -> isNePal(activate(V)), isPal(n__nil()) -> tt(), a() -> n__a(), e() -> n__e(), i() -> n__i(), o() -> n__o(), u() -> n__u()} EDG: { (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__isPal(X)) -> isPal#(X)) (isList#(V) -> activate#(V), activate#(n__isNeList(X)) -> isNeList#(X)) (isList#(V) -> activate#(V), activate#(n____(X1, X2)) -> activate#(X2)) (isList#(V) -> activate#(V), activate#(n____(X1, X2)) -> activate#(X1)) (isList#(V) -> activate#(V), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2))) (isList#(V) -> activate#(V), activate#(n__isList(X)) -> isList#(X)) (isList#(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__isPal(X)) -> isPal#(X)) (isPal#(V) -> activate#(V), activate#(n__isNeList(X)) -> isNeList#(X)) (isPal#(V) -> activate#(V), activate#(n____(X1, X2)) -> activate#(X2)) (isPal#(V) -> activate#(V), activate#(n____(X1, X2)) -> activate#(X1)) (isPal#(V) -> activate#(V), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2))) (isPal#(V) -> activate#(V), activate#(n__isList(X)) -> isList#(X)) (isPal#(V) -> activate#(V), activate#(n__nil()) -> nil#()) (isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> isList#(activate(V1))) (isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2)))) (isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> activate#(V2)) (isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> activate#(V1)) (isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> isNeList#(activate(V))) (isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> activate#(V)) (activate#(n__isList(X)) -> isList#(X), isList#(n____(V1, V2)) -> isList#(activate(V1))) (activate#(n__isList(X)) -> isList#(X), isList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2)))) (activate#(n__isList(X)) -> isList#(X), isList#(n____(V1, V2)) -> activate#(V2)) (activate#(n__isList(X)) -> isList#(X), isList#(n____(V1, V2)) -> activate#(V1)) (activate#(n__isList(X)) -> isList#(X), isList#(V) -> isNeList#(activate(V))) (activate#(n__isList(X)) -> isList#(X), isList#(V) -> activate#(V)) (activate#(n__isPal(X)) -> isPal#(X), isPal#(V) -> isNePal#(activate(V))) (activate#(n__isPal(X)) -> isPal#(X), isPal#(V) -> activate#(V)) (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__isPal(X)) -> isPal#(X)) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__isNeList(X)) -> isNeList#(X)) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> activate#(X2)) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> activate#(X1)) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2))) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__isList(X)) -> isList#(X)) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n__u()) -> u#()) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n__o()) -> o#()) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n__i()) -> i#()) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n__e()) -> e#()) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n__a()) -> a#()) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n__isPal(X)) -> isPal#(X)) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n__isNeList(X)) -> isNeList#(X)) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n____(X1, X2)) -> activate#(X2)) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n____(X1, X2)) -> activate#(X1)) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2))) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n__isList(X)) -> isList#(X)) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n__nil()) -> nil#()) (isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2))), and#(tt(), X) -> activate#(X)) (isList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2))), 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__isPal(X)) -> isPal#(X)) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__isNeList(X)) -> isNeList#(X)) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> activate#(X2)) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> activate#(X1)) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2))) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__isList(X)) -> isList#(X)) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#()) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n__u()) -> u#()) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n__o()) -> o#()) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n__i()) -> i#()) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n__e()) -> e#()) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n__a()) -> a#()) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n__isPal(X)) -> isPal#(X)) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n__isNeList(X)) -> isNeList#(X)) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n____(X1, X2)) -> activate#(X2)) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n____(X1, X2)) -> activate#(X1)) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2))) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n__isList(X)) -> isList#(X)) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n__nil()) -> nil#()) (__#(__(X, Y), Z) -> __#(Y, Z), __#(__(X, Y), Z) -> __#(Y, Z)) (__#(__(X, Y), Z) -> __#(Y, Z), __#(__(X, Y), Z) -> __#(X, __(Y, Z))) (__#(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(__(X, Y), Z) -> __#(X, __(Y, Z))) (__#(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(__(X, Y), Z) -> __#(Y, Z)) (isNePal#(n____(I, n____(P, I))) -> activate#(I), activate#(n__nil()) -> nil#()) (isNePal#(n____(I, n____(P, I))) -> activate#(I), activate#(n__isList(X)) -> isList#(X)) (isNePal#(n____(I, n____(P, I))) -> activate#(I), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2))) (isNePal#(n____(I, n____(P, I))) -> activate#(I), activate#(n____(X1, X2)) -> activate#(X1)) (isNePal#(n____(I, n____(P, I))) -> activate#(I), activate#(n____(X1, X2)) -> activate#(X2)) (isNePal#(n____(I, n____(P, I))) -> activate#(I), activate#(n__isNeList(X)) -> isNeList#(X)) (isNePal#(n____(I, n____(P, I))) -> activate#(I), activate#(n__isPal(X)) -> isPal#(X)) (isNePal#(n____(I, n____(P, I))) -> activate#(I), activate#(n__a()) -> a#()) (isNePal#(n____(I, n____(P, I))) -> activate#(I), activate#(n__e()) -> e#()) (isNePal#(n____(I, n____(P, I))) -> activate#(I), activate#(n__i()) -> i#()) (isNePal#(n____(I, n____(P, I))) -> activate#(I), activate#(n__o()) -> o#()) (isNePal#(n____(I, n____(P, I))) -> activate#(I), activate#(n__u()) -> u#()) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#()) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__isList(X)) -> isList#(X)) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2))) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> activate#(X1)) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> activate#(X2)) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__isNeList(X)) -> isNeList#(X)) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__isPal(X)) -> isPal#(X)) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__a()) -> a#()) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__e()) -> e#()) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__i()) -> i#()) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__o()) -> o#()) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__u()) -> u#()) (isNePal#(n____(I, n____(P, I))) -> and#(isQid(activate(I)), n__isPal(activate(P))), and#(tt(), X) -> activate#(X)) (isNeList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isNeList(activate(V2))), and#(tt(), X) -> activate#(X)) (activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2)), __#(__(X, Y), Z) -> __#(X, __(Y, Z))) (activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2)), __#(__(X, Y), Z) -> __#(Y, Z)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#()) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__isList(X)) -> isList#(X)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2))) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> activate#(X1)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> activate#(X2)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__isNeList(X)) -> isNeList#(X)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__isPal(X)) -> isPal#(X)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__a()) -> a#()) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__e()) -> e#()) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__i()) -> i#()) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__o()) -> o#()) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__u()) -> u#()) (isPal#(V) -> isNePal#(activate(V)), isNePal#(V) -> activate#(V)) (isPal#(V) -> isNePal#(activate(V)), isNePal#(V) -> isQid#(activate(V))) (isPal#(V) -> isNePal#(activate(V)), isNePal#(n____(I, n____(P, I))) -> activate#(I)) (isPal#(V) -> isNePal#(activate(V)), isNePal#(n____(I, n____(P, I))) -> activate#(P)) (isPal#(V) -> isNePal#(activate(V)), isNePal#(n____(I, n____(P, I))) -> and#(isQid(activate(I)), n__isPal(activate(P)))) (isPal#(V) -> isNePal#(activate(V)), isNePal#(n____(I, n____(P, I))) -> isQid#(activate(I))) (isList#(V) -> isNeList#(activate(V)), isNeList#(V) -> activate#(V)) (isList#(V) -> isNeList#(activate(V)), isNeList#(V) -> isQid#(activate(V))) (isList#(V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> activate#(V1)) (isList#(V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> activate#(V2)) (isList#(V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2)))) (isList#(V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isNeList(activate(V2)))) (isList#(V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> isNeList#(activate(V1))) (isList#(V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> isList#(activate(V1))) (and#(tt(), X) -> activate#(X), activate#(n__nil()) -> nil#()) (and#(tt(), X) -> activate#(X), activate#(n__isList(X)) -> isList#(X)) (and#(tt(), X) -> activate#(X), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2))) (and#(tt(), X) -> activate#(X), activate#(n____(X1, X2)) -> activate#(X1)) (and#(tt(), X) -> activate#(X), activate#(n____(X1, X2)) -> activate#(X2)) (and#(tt(), X) -> activate#(X), activate#(n__isNeList(X)) -> isNeList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isPal(X)) -> isPal#(X)) (and#(tt(), X) -> activate#(X), activate#(n__a()) -> a#()) (and#(tt(), X) -> activate#(X), activate#(n__e()) -> e#()) (and#(tt(), X) -> activate#(X), activate#(n__i()) -> i#()) (and#(tt(), X) -> activate#(X), activate#(n__o()) -> o#()) (and#(tt(), X) -> activate#(X), activate#(n__u()) -> u#()) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(V) -> activate#(V)) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(V) -> isQid#(activate(V))) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(n____(V1, V2)) -> activate#(V1)) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(n____(V1, V2)) -> activate#(V2)) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2)))) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isNeList(activate(V2)))) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(n____(V1, V2)) -> isNeList#(activate(V1))) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(n____(V1, V2)) -> isList#(activate(V1))) (isList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> activate#(V)) (isList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> isNeList#(activate(V))) (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#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2)))) (isList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> isList#(activate(V1))) (isNeList#(n____(V1, V2)) -> isNeList#(activate(V1)), isNeList#(V) -> activate#(V)) (isNeList#(n____(V1, V2)) -> isNeList#(activate(V1)), isNeList#(V) -> isQid#(activate(V))) (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)) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2)))) (isNeList#(n____(V1, V2)) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isNeList(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)) -> isList#(activate(V1))) (isNePal#(n____(I, n____(P, I))) -> activate#(P), activate#(n__nil()) -> nil#()) (isNePal#(n____(I, n____(P, I))) -> activate#(P), activate#(n__isList(X)) -> isList#(X)) (isNePal#(n____(I, n____(P, I))) -> activate#(P), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2))) (isNePal#(n____(I, n____(P, I))) -> activate#(P), activate#(n____(X1, X2)) -> activate#(X1)) (isNePal#(n____(I, n____(P, I))) -> activate#(P), activate#(n____(X1, X2)) -> activate#(X2)) (isNePal#(n____(I, n____(P, I))) -> activate#(P), activate#(n__isNeList(X)) -> isNeList#(X)) (isNePal#(n____(I, n____(P, I))) -> activate#(P), activate#(n__isPal(X)) -> isPal#(X)) (isNePal#(n____(I, n____(P, I))) -> activate#(P), activate#(n__a()) -> a#()) (isNePal#(n____(I, n____(P, I))) -> activate#(P), activate#(n__e()) -> e#()) (isNePal#(n____(I, n____(P, I))) -> activate#(P), activate#(n__i()) -> i#()) (isNePal#(n____(I, n____(P, I))) -> activate#(P), activate#(n__o()) -> o#()) (isNePal#(n____(I, n____(P, I))) -> activate#(P), activate#(n__u()) -> u#()) (isNePal#(V) -> activate#(V), activate#(n__nil()) -> nil#()) (isNePal#(V) -> activate#(V), activate#(n__isList(X)) -> isList#(X)) (isNePal#(V) -> activate#(V), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2))) (isNePal#(V) -> activate#(V), activate#(n____(X1, X2)) -> activate#(X1)) (isNePal#(V) -> activate#(V), activate#(n____(X1, X2)) -> activate#(X2)) (isNePal#(V) -> activate#(V), activate#(n__isNeList(X)) -> isNeList#(X)) (isNePal#(V) -> activate#(V), activate#(n__isPal(X)) -> isPal#(X)) (isNePal#(V) -> activate#(V), activate#(n__a()) -> a#()) (isNePal#(V) -> activate#(V), activate#(n__e()) -> e#()) (isNePal#(V) -> activate#(V), activate#(n__i()) -> i#()) (isNePal#(V) -> activate#(V), activate#(n__o()) -> o#()) (isNePal#(V) -> activate#(V), activate#(n__u()) -> u#()) (isNeList#(V) -> activate#(V), activate#(n__nil()) -> nil#()) (isNeList#(V) -> activate#(V), activate#(n__isList(X)) -> isList#(X)) (isNeList#(V) -> activate#(V), activate#(n____(X1, X2)) -> __#(activate(X1), activate(X2))) (isNeList#(V) -> activate#(V), activate#(n____(X1, X2)) -> activate#(X1)) (isNeList#(V) -> activate#(V), activate#(n____(X1, X2)) -> activate#(X2)) (isNeList#(V) -> activate#(V), activate#(n__isNeList(X)) -> isNeList#(X)) (isNeList#(V) -> activate#(V), activate#(n__isPal(X)) -> isPal#(X)) (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: { activate#(n__isList(X)) -> isList#(X), activate#(n____(X1, X2)) -> activate#(X1), activate#(n____(X1, X2)) -> activate#(X2), activate#(n__isNeList(X)) -> isNeList#(X), activate#(n__isPal(X)) -> isPal#(X), and#(tt(), X) -> activate#(X), isNeList#(V) -> activate#(V), isNeList#(n____(V1, V2)) -> activate#(V1), isNeList#(n____(V1, V2)) -> activate#(V2), isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2))), isNeList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isNeList(activate(V2))), isNeList#(n____(V1, V2)) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> activate#(V), isList#(V) -> isNeList#(activate(V)), isList#(n____(V1, V2)) -> activate#(V1), isList#(n____(V1, V2)) -> activate#(V2), isList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2))), isList#(n____(V1, V2)) -> isList#(activate(V1)), isNePal#(V) -> activate#(V), isNePal#(n____(I, n____(P, I))) -> activate#(I), isNePal#(n____(I, n____(P, I))) -> activate#(P), isNePal#(n____(I, n____(P, I))) -> and#(isQid(activate(I)), n__isPal(activate(P))), isPal#(V) -> activate#(V), isPal#(V) -> isNePal#(activate(V))} Scc: {__#(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(__(X, Y), Z) -> __#(Y, Z)} SCC: Strict: { activate#(n__isList(X)) -> isList#(X), activate#(n____(X1, X2)) -> activate#(X1), activate#(n____(X1, X2)) -> activate#(X2), activate#(n__isNeList(X)) -> isNeList#(X), activate#(n__isPal(X)) -> isPal#(X), and#(tt(), X) -> activate#(X), isNeList#(V) -> activate#(V), isNeList#(n____(V1, V2)) -> activate#(V1), isNeList#(n____(V1, V2)) -> activate#(V2), isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2))), isNeList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isNeList(activate(V2))), isNeList#(n____(V1, V2)) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> activate#(V), isList#(V) -> isNeList#(activate(V)), isList#(n____(V1, V2)) -> activate#(V1), isList#(n____(V1, V2)) -> activate#(V2), isList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2))), isList#(n____(V1, V2)) -> isList#(activate(V1)), isNePal#(V) -> activate#(V), isNePal#(n____(I, n____(P, I))) -> activate#(I), isNePal#(n____(I, n____(P, I))) -> activate#(P), isNePal#(n____(I, n____(P, I))) -> and#(isQid(activate(I)), n__isPal(activate(P))), isPal#(V) -> activate#(V), isPal#(V) -> isNePal#(activate(V))} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isList(X)) -> isList(X), activate(n____(X1, X2)) -> __(activate(X1), activate(X2)), activate(n__isNeList(X)) -> isNeList(X), activate(n__isPal(X)) -> isPal(X), activate(n__a()) -> a(), activate(n__e()) -> e(), activate(n__i()) -> i(), activate(n__o()) -> o(), activate(n__u()) -> u(), and(tt(), X) -> activate(X), isNeList(X) -> n__isNeList(X), isNeList(V) -> isQid(activate(V)), isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))), isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))), isList(X) -> n__isList(X), isList(V) -> isNeList(activate(V)), isList(n__nil()) -> tt(), isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), isNePal(V) -> isQid(activate(V)), isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))), isPal(X) -> n__isPal(X), isPal(V) -> isNePal(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) = [0], pi(n__isPal) = [0], pi(isNePal#) = [0], pi(isNePal) = [0], pi(n__isNeList) = 0, pi(isQid) = [], pi(n____) = [0,1], pi(n__isList) = 0, pi(n__nil) = [], pi(isList#) = 0, pi(isList) = 0, pi(isNeList#) = 0, pi(isNeList) = 0, pi(tt) = [], pi(and#) = 1, pi(and) = 1, pi(activate#) = 0, pi(activate) = 0, pi(nil) = [], pi(__) = [0,1] Usable Rules: {} Interpretation: [isPal#](x0) = x0 + 1, [isNePal#](x0) = x0 + 1, [n____](x0, x1) = x0 + x1, [n__isPal](x0) = x0 + 1 Strict: { activate#(n__isList(X)) -> isList#(X), activate#(n____(X1, X2)) -> activate#(X1), activate#(n____(X1, X2)) -> activate#(X2), activate#(n__isNeList(X)) -> isNeList#(X), activate#(n__isPal(X)) -> isPal#(X), and#(tt(), X) -> activate#(X), isNeList#(V) -> activate#(V), isNeList#(n____(V1, V2)) -> activate#(V1), isNeList#(n____(V1, V2)) -> activate#(V2), isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2))), isNeList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isNeList(activate(V2))), isNeList#(n____(V1, V2)) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> activate#(V), isList#(V) -> isNeList#(activate(V)), isList#(n____(V1, V2)) -> activate#(V1), isList#(n____(V1, V2)) -> activate#(V2), isList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2))), isList#(n____(V1, V2)) -> isList#(activate(V1)), isNePal#(n____(I, n____(P, I))) -> and#(isQid(activate(I)), n__isPal(activate(P))), isPal#(V) -> isNePal#(activate(V))} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isList(X)) -> isList(X), activate(n____(X1, X2)) -> __(activate(X1), activate(X2)), activate(n__isNeList(X)) -> isNeList(X), activate(n__isPal(X)) -> isPal(X), activate(n__a()) -> a(), activate(n__e()) -> e(), activate(n__i()) -> i(), activate(n__o()) -> o(), activate(n__u()) -> u(), and(tt(), X) -> activate(X), isNeList(X) -> n__isNeList(X), isNeList(V) -> isQid(activate(V)), isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))), isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))), isList(X) -> n__isList(X), isList(V) -> isNeList(activate(V)), isList(n__nil()) -> tt(), isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), isNePal(V) -> isQid(activate(V)), isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))), isPal(X) -> n__isPal(X), isPal(V) -> isNePal(activate(V)), isPal(n__nil()) -> tt(), a() -> n__a(), e() -> n__e(), i() -> n__i(), o() -> n__o(), u() -> n__u()} EDG: {(isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> isList#(activate(V1))) (isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2)))) (isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> activate#(V2)) (isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> activate#(V1)) (isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> isNeList#(activate(V))) (isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> activate#(V)) (isList#(V) -> isNeList#(activate(V)), isNeList#(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)) -> and#(isList(activate(V1)), n__isNeList(activate(V2)))) (isList#(V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2)))) (isList#(V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> activate#(V2)) (isList#(V) -> isNeList#(activate(V)), isNeList#(n____(V1, V2)) -> activate#(V1)) (isList#(V) -> isNeList#(activate(V)), isNeList#(V) -> activate#(V)) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n__isPal(X)) -> isPal#(X)) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n__isNeList(X)) -> isNeList#(X)) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n____(X1, X2)) -> activate#(X2)) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n____(X1, X2)) -> activate#(X1)) (activate#(n____(X1, X2)) -> activate#(X2), activate#(n__isList(X)) -> isList#(X)) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__isPal(X)) -> isPal#(X)) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__isNeList(X)) -> isNeList#(X)) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> activate#(X2)) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> activate#(X1)) (isNeList#(n____(V1, V2)) -> activate#(V2), activate#(n__isList(X)) -> isList#(X)) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__isPal(X)) -> isPal#(X)) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__isNeList(X)) -> isNeList#(X)) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> activate#(X2)) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> activate#(X1)) (isNeList#(n____(V1, V2)) -> activate#(V1), activate#(n__isList(X)) -> isList#(X)) (isNeList#(V) -> activate#(V), activate#(n__isPal(X)) -> isPal#(X)) (isNeList#(V) -> activate#(V), activate#(n__isNeList(X)) -> isNeList#(X)) (isNeList#(V) -> activate#(V), activate#(n____(X1, X2)) -> activate#(X2)) (isNeList#(V) -> activate#(V), activate#(n____(X1, X2)) -> activate#(X1)) (isNeList#(V) -> activate#(V), activate#(n__isList(X)) -> isList#(X)) (activate#(n__isList(X)) -> isList#(X), isList#(n____(V1, V2)) -> isList#(activate(V1))) (activate#(n__isList(X)) -> isList#(X), isList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2)))) (activate#(n__isList(X)) -> isList#(X), isList#(n____(V1, V2)) -> activate#(V2)) (activate#(n__isList(X)) -> isList#(X), isList#(n____(V1, V2)) -> activate#(V1)) (activate#(n__isList(X)) -> isList#(X), isList#(V) -> isNeList#(activate(V))) (activate#(n__isList(X)) -> isList#(X), isList#(V) -> activate#(V)) (activate#(n__isPal(X)) -> isPal#(X), isPal#(V) -> isNePal#(activate(V))) (isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2))), and#(tt(), X) -> activate#(X)) (isList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2))), and#(tt(), X) -> activate#(X)) (isNePal#(n____(I, n____(P, I))) -> and#(isQid(activate(I)), n__isPal(activate(P))), and#(tt(), X) -> activate#(X)) (isNeList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isNeList(activate(V2))), and#(tt(), X) -> activate#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isList(X)) -> isList#(X)) (and#(tt(), X) -> activate#(X), activate#(n____(X1, X2)) -> activate#(X1)) (and#(tt(), X) -> activate#(X), activate#(n____(X1, X2)) -> activate#(X2)) (and#(tt(), X) -> activate#(X), activate#(n__isNeList(X)) -> isNeList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isPal(X)) -> isPal#(X)) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(V) -> activate#(V)) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(n____(V1, V2)) -> activate#(V1)) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(n____(V1, V2)) -> activate#(V2)) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2)))) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isNeList(activate(V2)))) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(n____(V1, V2)) -> isNeList#(activate(V1))) (activate#(n__isNeList(X)) -> isNeList#(X), isNeList#(n____(V1, V2)) -> isList#(activate(V1))) (isList#(V) -> activate#(V), activate#(n__isList(X)) -> isList#(X)) (isList#(V) -> activate#(V), activate#(n____(X1, X2)) -> activate#(X1)) (isList#(V) -> activate#(V), activate#(n____(X1, X2)) -> activate#(X2)) (isList#(V) -> activate#(V), activate#(n__isNeList(X)) -> isNeList#(X)) (isList#(V) -> activate#(V), activate#(n__isPal(X)) -> isPal#(X)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__isList(X)) -> isList#(X)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> activate#(X1)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n____(X1, X2)) -> activate#(X2)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__isNeList(X)) -> isNeList#(X)) (isList#(n____(V1, V2)) -> activate#(V1), activate#(n__isPal(X)) -> isPal#(X)) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__isList(X)) -> isList#(X)) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> activate#(X1)) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n____(X1, X2)) -> activate#(X2)) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__isNeList(X)) -> isNeList#(X)) (isList#(n____(V1, V2)) -> activate#(V2), activate#(n__isPal(X)) -> isPal#(X)) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n__isList(X)) -> isList#(X)) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n____(X1, X2)) -> activate#(X1)) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n____(X1, X2)) -> activate#(X2)) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n__isNeList(X)) -> isNeList#(X)) (activate#(n____(X1, X2)) -> activate#(X1), activate#(n__isPal(X)) -> isPal#(X)) (isPal#(V) -> isNePal#(activate(V)), isNePal#(n____(I, n____(P, I))) -> and#(isQid(activate(I)), n__isPal(activate(P)))) (isList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> activate#(V)) (isList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> isNeList#(activate(V))) (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#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2)))) (isList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(n____(V1, V2)) -> isList#(activate(V1))) (isNeList#(n____(V1, V2)) -> isNeList#(activate(V1)), isNeList#(V) -> activate#(V)) (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)) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2)))) (isNeList#(n____(V1, V2)) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isNeList(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)) -> isList#(activate(V1)))} SCCS: Scc: { activate#(n__isList(X)) -> isList#(X), activate#(n____(X1, X2)) -> activate#(X1), activate#(n____(X1, X2)) -> activate#(X2), activate#(n__isNeList(X)) -> isNeList#(X), activate#(n__isPal(X)) -> isPal#(X), and#(tt(), X) -> activate#(X), isNeList#(V) -> activate#(V), isNeList#(n____(V1, V2)) -> activate#(V1), isNeList#(n____(V1, V2)) -> activate#(V2), isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2))), isNeList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isNeList(activate(V2))), isNeList#(n____(V1, V2)) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> activate#(V), isList#(V) -> isNeList#(activate(V)), isList#(n____(V1, V2)) -> activate#(V1), isList#(n____(V1, V2)) -> activate#(V2), isList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2))), isList#(n____(V1, V2)) -> isList#(activate(V1)), isNePal#(n____(I, n____(P, I))) -> and#(isQid(activate(I)), n__isPal(activate(P))), isPal#(V) -> isNePal#(activate(V))} SCC: Strict: { activate#(n__isList(X)) -> isList#(X), activate#(n____(X1, X2)) -> activate#(X1), activate#(n____(X1, X2)) -> activate#(X2), activate#(n__isNeList(X)) -> isNeList#(X), activate#(n__isPal(X)) -> isPal#(X), and#(tt(), X) -> activate#(X), isNeList#(V) -> activate#(V), isNeList#(n____(V1, V2)) -> activate#(V1), isNeList#(n____(V1, V2)) -> activate#(V2), isNeList#(n____(V1, V2)) -> and#(isNeList(activate(V1)), n__isList(activate(V2))), isNeList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isNeList(activate(V2))), isNeList#(n____(V1, V2)) -> isNeList#(activate(V1)), isNeList#(n____(V1, V2)) -> isList#(activate(V1)), isList#(V) -> activate#(V), isList#(V) -> isNeList#(activate(V)), isList#(n____(V1, V2)) -> activate#(V1), isList#(n____(V1, V2)) -> activate#(V2), isList#(n____(V1, V2)) -> and#(isList(activate(V1)), n__isList(activate(V2))), isList#(n____(V1, V2)) -> isList#(activate(V1)), isNePal#(n____(I, n____(P, I))) -> and#(isQid(activate(I)), n__isPal(activate(P))), isPal#(V) -> isNePal#(activate(V))} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isList(X)) -> isList(X), activate(n____(X1, X2)) -> __(activate(X1), activate(X2)), activate(n__isNeList(X)) -> isNeList(X), activate(n__isPal(X)) -> isPal(X), activate(n__a()) -> a(), activate(n__e()) -> e(), activate(n__i()) -> i(), activate(n__o()) -> o(), activate(n__u()) -> u(), and(tt(), X) -> activate(X), isNeList(X) -> n__isNeList(X), isNeList(V) -> isQid(activate(V)), isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))), isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))), isList(X) -> n__isList(X), isList(V) -> isNeList(activate(V)), isList(n__nil()) -> tt(), isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), isNePal(V) -> isQid(activate(V)), isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))), isPal(X) -> n__isPal(X), isPal(V) -> isNePal(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) = [0], pi(n__isPal) = [0], pi(isNePal#) = 0, pi(isNePal) = 0, pi(n__isNeList) = [0], pi(isQid) = [], pi(n____) = [0,1], pi(n__isList) = [0], pi(n__nil) = [], pi(isList#) = [0], pi(isList) = [0], pi(isNeList#) = [0], pi(isNeList) = [0], pi(tt) = [], pi(and#) = 1, pi(and) = 1, pi(activate#) = 0, pi(activate) = 0, pi(nil) = [], pi(__) = [0,1] Usable Rules: {} Interpretation: [isList#](x0) = x0 + 1, [isNeList#](x0) = x0 + 1, [n____](x0, x1) = x0 + x1 + 1, [n__isPal](x0) = x0 + 1, [n__isNeList](x0) = x0 + 1, [n__isList](x0) = x0 + 1 Strict: { activate#(n__isList(X)) -> isList#(X), activate#(n__isNeList(X)) -> isNeList#(X), and#(tt(), X) -> activate#(X), isList#(V) -> isNeList#(activate(V)), isPal#(V) -> isNePal#(activate(V))} Weak: { __(X, nil()) -> X, __(X1, X2) -> n____(X1, X2), __(__(X, Y), Z) -> __(X, __(Y, Z)), __(nil(), X) -> X, nil() -> n__nil(), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isList(X)) -> isList(X), activate(n____(X1, X2)) -> __(activate(X1), activate(X2)), activate(n__isNeList(X)) -> isNeList(X), activate(n__isPal(X)) -> isPal(X), activate(n__a()) -> a(), activate(n__e()) -> e(), activate(n__i()) -> i(), activate(n__o()) -> o(), activate(n__u()) -> u(), and(tt(), X) -> activate(X), isNeList(X) -> n__isNeList(X), isNeList(V) -> isQid(activate(V)), isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))), isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))), isList(X) -> n__isList(X), isList(V) -> isNeList(activate(V)), isList(n__nil()) -> tt(), isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), isNePal(V) -> isQid(activate(V)), isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))), isPal(X) -> n__isPal(X), isPal(V) -> isNePal(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__isList(X)) -> isList#(X)) (and#(tt(), X) -> activate#(X), activate#(n__isNeList(X)) -> isNeList#(X)) (activate#(n__isList(X)) -> isList#(X), isList#(V) -> isNeList#(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(), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isList(X)) -> isList(X), activate(n____(X1, X2)) -> __(activate(X1), activate(X2)), activate(n__isNeList(X)) -> isNeList(X), activate(n__isPal(X)) -> isPal(X), activate(n__a()) -> a(), activate(n__e()) -> e(), activate(n__i()) -> i(), activate(n__o()) -> o(), activate(n__u()) -> u(), and(tt(), X) -> activate(X), isNeList(X) -> n__isNeList(X), isNeList(V) -> isQid(activate(V)), isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))), isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))), isList(X) -> n__isList(X), isList(V) -> isNeList(activate(V)), isList(n__nil()) -> tt(), isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), isNePal(V) -> isQid(activate(V)), isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))), isPal(X) -> n__isPal(X), isPal(V) -> isNePal(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(), activate(X) -> X, activate(n__nil()) -> nil(), activate(n__isList(X)) -> isList(X), activate(n____(X1, X2)) -> __(activate(X1), activate(X2)), activate(n__isNeList(X)) -> isNeList(X), activate(n__isPal(X)) -> isPal(X), activate(n__a()) -> a(), activate(n__e()) -> e(), activate(n__i()) -> i(), activate(n__o()) -> o(), activate(n__u()) -> u(), and(tt(), X) -> activate(X), isNeList(X) -> n__isNeList(X), isNeList(V) -> isQid(activate(V)), isNeList(n____(V1, V2)) -> and(isNeList(activate(V1)), n__isList(activate(V2))), isNeList(n____(V1, V2)) -> and(isList(activate(V1)), n__isNeList(activate(V2))), isList(X) -> n__isList(X), isList(V) -> isNeList(activate(V)), isList(n__nil()) -> tt(), isList(n____(V1, V2)) -> and(isList(activate(V1)), n__isList(activate(V2))), isQid(n__a()) -> tt(), isQid(n__e()) -> tt(), isQid(n__i()) -> tt(), isQid(n__o()) -> tt(), isQid(n__u()) -> tt(), isNePal(V) -> isQid(activate(V)), isNePal(n____(I, n____(P, I))) -> and(isQid(activate(I)), n__isPal(activate(P))), isPal(X) -> n__isPal(X), isPal(V) -> isNePal(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