YES TRS: { a____(X, nil()) -> mark(X), a____(X1, X2) -> __(X1, X2), a____(__(X, Y), Z) -> a____(mark(X), a____(mark(Y), mark(Z))), a____(nil(), X) -> mark(X), mark(__(X1, X2)) -> a____(mark(X1), mark(X2)), mark(nil()) -> nil(), mark(tt()) -> tt(), mark(isList(X)) -> a__isList(X), mark(isNeList(X)) -> a__isNeList(X), mark(isPal(X)) -> a__isPal(X), mark(a()) -> a(), mark(e()) -> e(), mark(i()) -> i(), mark(o()) -> o(), mark(u()) -> u(), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(isQid(X)) -> a__isQid(X), mark(isNePal(X)) -> a__isNePal(X), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark(X), a__isNeList(X) -> isNeList(X), a__isNeList(V) -> a__isQid(V), a__isNeList(__(V1, V2)) -> a__and(a__isNeList(V1), isList(V2)), a__isNeList(__(V1, V2)) -> a__and(a__isList(V1), isNeList(V2)), a__isList(X) -> isList(X), a__isList(V) -> a__isNeList(V), a__isList(__(V1, V2)) -> a__and(a__isList(V1), isList(V2)), a__isList(nil()) -> tt(), a__isQid(X) -> isQid(X), a__isQid(a()) -> tt(), a__isQid(e()) -> tt(), a__isQid(i()) -> tt(), a__isQid(o()) -> tt(), a__isQid(u()) -> tt(), a__isNePal(X) -> isNePal(X), a__isNePal(V) -> a__isQid(V), a__isNePal(__(I, __(P, I))) -> a__and(a__isQid(I), isPal(P)), a__isPal(X) -> isPal(X), a__isPal(V) -> a__isNePal(V), a__isPal(nil()) -> tt()} DP: Strict: { a____#(X, nil()) -> mark#(X), a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z))), a____#(__(X, Y), Z) -> a____#(mark(Y), mark(Z)), a____#(__(X, Y), Z) -> mark#(X), a____#(__(X, Y), Z) -> mark#(Y), a____#(__(X, Y), Z) -> mark#(Z), a____#(nil(), X) -> mark#(X), mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2)), mark#(__(X1, X2)) -> mark#(X1), mark#(__(X1, X2)) -> mark#(X2), mark#(isList(X)) -> a__isList#(X), mark#(isNeList(X)) -> a__isNeList#(X), mark#(isPal(X)) -> a__isPal#(X), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), mark#(isQid(X)) -> a__isQid#(X), mark#(isNePal(X)) -> a__isNePal#(X), a__and#(tt(), X) -> mark#(X), a__isNeList#(V) -> a__isQid#(V), a__isNeList#(__(V1, V2)) -> a__and#(a__isNeList(V1), isList(V2)), a__isNeList#(__(V1, V2)) -> a__and#(a__isList(V1), isNeList(V2)), a__isNeList#(__(V1, V2)) -> a__isNeList#(V1), a__isNeList#(__(V1, V2)) -> a__isList#(V1), a__isList#(V) -> a__isNeList#(V), a__isList#(__(V1, V2)) -> a__and#(a__isList(V1), isList(V2)), a__isList#(__(V1, V2)) -> a__isList#(V1), a__isNePal#(V) -> a__isQid#(V), a__isNePal#(__(I, __(P, I))) -> a__and#(a__isQid(I), isPal(P)), a__isNePal#(__(I, __(P, I))) -> a__isQid#(I), a__isPal#(V) -> a__isNePal#(V)} Weak: { a____(X, nil()) -> mark(X), a____(X1, X2) -> __(X1, X2), a____(__(X, Y), Z) -> a____(mark(X), a____(mark(Y), mark(Z))), a____(nil(), X) -> mark(X), mark(__(X1, X2)) -> a____(mark(X1), mark(X2)), mark(nil()) -> nil(), mark(tt()) -> tt(), mark(isList(X)) -> a__isList(X), mark(isNeList(X)) -> a__isNeList(X), mark(isPal(X)) -> a__isPal(X), mark(a()) -> a(), mark(e()) -> e(), mark(i()) -> i(), mark(o()) -> o(), mark(u()) -> u(), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(isQid(X)) -> a__isQid(X), mark(isNePal(X)) -> a__isNePal(X), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark(X), a__isNeList(X) -> isNeList(X), a__isNeList(V) -> a__isQid(V), a__isNeList(__(V1, V2)) -> a__and(a__isNeList(V1), isList(V2)), a__isNeList(__(V1, V2)) -> a__and(a__isList(V1), isNeList(V2)), a__isList(X) -> isList(X), a__isList(V) -> a__isNeList(V), a__isList(__(V1, V2)) -> a__and(a__isList(V1), isList(V2)), a__isList(nil()) -> tt(), a__isQid(X) -> isQid(X), a__isQid(a()) -> tt(), a__isQid(e()) -> tt(), a__isQid(i()) -> tt(), a__isQid(o()) -> tt(), a__isQid(u()) -> tt(), a__isNePal(X) -> isNePal(X), a__isNePal(V) -> a__isQid(V), a__isNePal(__(I, __(P, I))) -> a__and(a__isQid(I), isPal(P)), a__isPal(X) -> isPal(X), a__isPal(V) -> a__isNePal(V), a__isPal(nil()) -> tt()} EDG: { (a____#(__(X, Y), Z) -> a____#(mark(Y), mark(Z)), a____#(nil(), X) -> mark#(X)) (a____#(__(X, Y), Z) -> a____#(mark(Y), mark(Z)), a____#(__(X, Y), Z) -> mark#(Z)) (a____#(__(X, Y), Z) -> a____#(mark(Y), mark(Z)), a____#(__(X, Y), Z) -> mark#(Y)) (a____#(__(X, Y), Z) -> a____#(mark(Y), mark(Z)), a____#(__(X, Y), Z) -> mark#(X)) (a____#(__(X, Y), Z) -> a____#(mark(Y), mark(Z)), a____#(__(X, Y), Z) -> a____#(mark(Y), mark(Z))) (a____#(__(X, Y), Z) -> a____#(mark(Y), mark(Z)), a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z)))) (a____#(__(X, Y), Z) -> a____#(mark(Y), mark(Z)), a____#(X, nil()) -> mark#(X)) (a__isNeList#(__(V1, V2)) -> a__and#(a__isNeList(V1), isList(V2)), a__and#(tt(), X) -> mark#(X)) (a__isList#(__(V1, V2)) -> a__and#(a__isList(V1), isList(V2)), a__and#(tt(), X) -> mark#(X)) (mark#(__(X1, X2)) -> mark#(X1), mark#(isNePal(X)) -> a__isNePal#(X)) (mark#(__(X1, X2)) -> mark#(X1), mark#(isQid(X)) -> a__isQid#(X)) (mark#(__(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(__(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(__(X1, X2)) -> mark#(X1), mark#(isPal(X)) -> a__isPal#(X)) (mark#(__(X1, X2)) -> mark#(X1), mark#(isNeList(X)) -> a__isNeList#(X)) (mark#(__(X1, X2)) -> mark#(X1), mark#(isList(X)) -> a__isList#(X)) (mark#(__(X1, X2)) -> mark#(X1), mark#(__(X1, X2)) -> mark#(X2)) (mark#(__(X1, X2)) -> mark#(X1), mark#(__(X1, X2)) -> mark#(X1)) (mark#(__(X1, X2)) -> mark#(X1), mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2))) (a____#(__(X, Y), Z) -> mark#(Y), mark#(isNePal(X)) -> a__isNePal#(X)) (a____#(__(X, Y), Z) -> mark#(Y), mark#(isQid(X)) -> a__isQid#(X)) (a____#(__(X, Y), Z) -> mark#(Y), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a____#(__(X, Y), Z) -> mark#(Y), mark#(and(X1, X2)) -> mark#(X1)) (a____#(__(X, Y), Z) -> mark#(Y), mark#(isPal(X)) -> a__isPal#(X)) (a____#(__(X, Y), Z) -> mark#(Y), mark#(isNeList(X)) -> a__isNeList#(X)) (a____#(__(X, Y), Z) -> mark#(Y), mark#(isList(X)) -> a__isList#(X)) (a____#(__(X, Y), Z) -> mark#(Y), mark#(__(X1, X2)) -> mark#(X2)) (a____#(__(X, Y), Z) -> mark#(Y), mark#(__(X1, X2)) -> mark#(X1)) (a____#(__(X, Y), Z) -> mark#(Y), mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2))) (a__isNeList#(__(V1, V2)) -> a__isNeList#(V1), a__isNeList#(__(V1, V2)) -> a__isList#(V1)) (a__isNeList#(__(V1, V2)) -> a__isNeList#(V1), a__isNeList#(__(V1, V2)) -> a__isNeList#(V1)) (a__isNeList#(__(V1, V2)) -> a__isNeList#(V1), a__isNeList#(__(V1, V2)) -> a__and#(a__isList(V1), isNeList(V2))) (a__isNeList#(__(V1, V2)) -> a__isNeList#(V1), a__isNeList#(__(V1, V2)) -> a__and#(a__isNeList(V1), isList(V2))) (a__isNeList#(__(V1, V2)) -> a__isNeList#(V1), a__isNeList#(V) -> a__isQid#(V)) (a__isList#(__(V1, V2)) -> a__isList#(V1), a__isList#(__(V1, V2)) -> a__isList#(V1)) (a__isList#(__(V1, V2)) -> a__isList#(V1), a__isList#(__(V1, V2)) -> a__and#(a__isList(V1), isList(V2))) (a__isList#(__(V1, V2)) -> a__isList#(V1), a__isList#(V) -> a__isNeList#(V)) (a____#(__(X, Y), Z) -> mark#(X), mark#(isNePal(X)) -> a__isNePal#(X)) (a____#(__(X, Y), Z) -> mark#(X), mark#(isQid(X)) -> a__isQid#(X)) (a____#(__(X, Y), Z) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a____#(__(X, Y), Z) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (a____#(__(X, Y), Z) -> mark#(X), mark#(isPal(X)) -> a__isPal#(X)) (a____#(__(X, Y), Z) -> mark#(X), mark#(isNeList(X)) -> a__isNeList#(X)) (a____#(__(X, Y), Z) -> mark#(X), mark#(isList(X)) -> a__isList#(X)) (a____#(__(X, Y), Z) -> mark#(X), mark#(__(X1, X2)) -> mark#(X2)) (a____#(__(X, Y), Z) -> mark#(X), mark#(__(X1, X2)) -> mark#(X1)) (a____#(__(X, Y), Z) -> mark#(X), mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2))) (mark#(isList(X)) -> a__isList#(X), a__isList#(__(V1, V2)) -> a__isList#(V1)) (mark#(isList(X)) -> a__isList#(X), a__isList#(__(V1, V2)) -> a__and#(a__isList(V1), isList(V2))) (mark#(isList(X)) -> a__isList#(X), a__isList#(V) -> a__isNeList#(V)) (mark#(isPal(X)) -> a__isPal#(X), a__isPal#(V) -> a__isNePal#(V)) (mark#(isNePal(X)) -> a__isNePal#(X), a__isNePal#(__(I, __(P, I))) -> a__isQid#(I)) (mark#(isNePal(X)) -> a__isNePal#(X), a__isNePal#(__(I, __(P, I))) -> a__and#(a__isQid(I), isPal(P))) (mark#(isNePal(X)) -> a__isNePal#(X), a__isNePal#(V) -> a__isQid#(V)) (a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z))), a____#(nil(), X) -> mark#(X)) (a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z))), a____#(__(X, Y), Z) -> mark#(Z)) (a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z))), a____#(__(X, Y), Z) -> mark#(Y)) (a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z))), a____#(__(X, Y), Z) -> mark#(X)) (a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z))), a____#(__(X, Y), Z) -> a____#(mark(Y), mark(Z))) (a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z))), a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z)))) (a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z))), a____#(X, nil()) -> mark#(X)) (a__isList#(V) -> a__isNeList#(V), a__isNeList#(__(V1, V2)) -> a__isList#(V1)) (a__isList#(V) -> a__isNeList#(V), a__isNeList#(__(V1, V2)) -> a__isNeList#(V1)) (a__isList#(V) -> a__isNeList#(V), a__isNeList#(__(V1, V2)) -> a__and#(a__isList(V1), isNeList(V2))) (a__isList#(V) -> a__isNeList#(V), a__isNeList#(__(V1, V2)) -> a__and#(a__isNeList(V1), isList(V2))) (a__isList#(V) -> a__isNeList#(V), a__isNeList#(V) -> a__isQid#(V)) (a__isPal#(V) -> a__isNePal#(V), a__isNePal#(__(I, __(P, I))) -> a__isQid#(I)) (a__isPal#(V) -> a__isNePal#(V), a__isNePal#(__(I, __(P, I))) -> a__and#(a__isQid(I), isPal(P))) (a__isPal#(V) -> a__isNePal#(V), a__isNePal#(V) -> a__isQid#(V)) (mark#(__(X1, X2)) -> mark#(X2), mark#(isNePal(X)) -> a__isNePal#(X)) (mark#(__(X1, X2)) -> mark#(X2), mark#(isQid(X)) -> a__isQid#(X)) (mark#(__(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(__(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1)) (mark#(__(X1, X2)) -> mark#(X2), mark#(isPal(X)) -> a__isPal#(X)) (mark#(__(X1, X2)) -> mark#(X2), mark#(isNeList(X)) -> a__isNeList#(X)) (mark#(__(X1, X2)) -> mark#(X2), mark#(isList(X)) -> a__isList#(X)) (mark#(__(X1, X2)) -> mark#(X2), mark#(__(X1, X2)) -> mark#(X2)) (mark#(__(X1, X2)) -> mark#(X2), mark#(__(X1, X2)) -> mark#(X1)) (mark#(__(X1, X2)) -> mark#(X2), mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2))) (a__and#(tt(), X) -> mark#(X), mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2))) (a__and#(tt(), X) -> mark#(X), mark#(__(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(__(X1, X2)) -> mark#(X2)) (a__and#(tt(), X) -> mark#(X), mark#(isList(X)) -> a__isList#(X)) (a__and#(tt(), X) -> mark#(X), mark#(isNeList(X)) -> a__isNeList#(X)) (a__and#(tt(), X) -> mark#(X), mark#(isPal(X)) -> a__isPal#(X)) (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a__and#(tt(), X) -> mark#(X), mark#(isQid(X)) -> a__isQid#(X)) (a__and#(tt(), X) -> mark#(X), mark#(isNePal(X)) -> a__isNePal#(X)) (mark#(isNeList(X)) -> a__isNeList#(X), a__isNeList#(V) -> a__isQid#(V)) (mark#(isNeList(X)) -> a__isNeList#(X), a__isNeList#(__(V1, V2)) -> a__and#(a__isNeList(V1), isList(V2))) (mark#(isNeList(X)) -> a__isNeList#(X), a__isNeList#(__(V1, V2)) -> a__and#(a__isList(V1), isNeList(V2))) (mark#(isNeList(X)) -> a__isNeList#(X), a__isNeList#(__(V1, V2)) -> a__isNeList#(V1)) (mark#(isNeList(X)) -> a__isNeList#(X), a__isNeList#(__(V1, V2)) -> a__isList#(V1)) (a____#(nil(), X) -> mark#(X), mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2))) (a____#(nil(), X) -> mark#(X), mark#(__(X1, X2)) -> mark#(X1)) (a____#(nil(), X) -> mark#(X), mark#(__(X1, X2)) -> mark#(X2)) (a____#(nil(), X) -> mark#(X), mark#(isList(X)) -> a__isList#(X)) (a____#(nil(), X) -> mark#(X), mark#(isNeList(X)) -> a__isNeList#(X)) (a____#(nil(), X) -> mark#(X), mark#(isPal(X)) -> a__isPal#(X)) (a____#(nil(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (a____#(nil(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a____#(nil(), X) -> mark#(X), mark#(isQid(X)) -> a__isQid#(X)) (a____#(nil(), X) -> mark#(X), mark#(isNePal(X)) -> a__isNePal#(X)) (a____#(X, nil()) -> mark#(X), mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2))) (a____#(X, nil()) -> mark#(X), mark#(__(X1, X2)) -> mark#(X1)) (a____#(X, nil()) -> mark#(X), mark#(__(X1, X2)) -> mark#(X2)) (a____#(X, nil()) -> mark#(X), mark#(isList(X)) -> a__isList#(X)) (a____#(X, nil()) -> mark#(X), mark#(isNeList(X)) -> a__isNeList#(X)) (a____#(X, nil()) -> mark#(X), mark#(isPal(X)) -> a__isPal#(X)) (a____#(X, nil()) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1)) (a____#(X, nil()) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a____#(X, nil()) -> mark#(X), mark#(isQid(X)) -> a__isQid#(X)) (a____#(X, nil()) -> mark#(X), mark#(isNePal(X)) -> a__isNePal#(X)) (a__isNeList#(__(V1, V2)) -> a__isList#(V1), a__isList#(V) -> a__isNeList#(V)) (a__isNeList#(__(V1, V2)) -> a__isList#(V1), a__isList#(__(V1, V2)) -> a__and#(a__isList(V1), isList(V2))) (a__isNeList#(__(V1, V2)) -> a__isList#(V1), a__isList#(__(V1, V2)) -> a__isList#(V1)) (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(tt(), X) -> mark#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2))) (mark#(and(X1, X2)) -> mark#(X1), mark#(__(X1, X2)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(__(X1, X2)) -> mark#(X2)) (mark#(and(X1, X2)) -> mark#(X1), mark#(isList(X)) -> a__isList#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(isNeList(X)) -> a__isNeList#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(isPal(X)) -> a__isPal#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (mark#(and(X1, X2)) -> mark#(X1), mark#(isQid(X)) -> a__isQid#(X)) (mark#(and(X1, X2)) -> mark#(X1), mark#(isNePal(X)) -> a__isNePal#(X)) (a__isNePal#(__(I, __(P, I))) -> a__and#(a__isQid(I), isPal(P)), a__and#(tt(), X) -> mark#(X)) (a__isNeList#(__(V1, V2)) -> a__and#(a__isList(V1), isNeList(V2)), a__and#(tt(), X) -> mark#(X)) (mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2)), a____#(X, nil()) -> mark#(X)) (mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2)), a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z)))) (mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2)), a____#(__(X, Y), Z) -> a____#(mark(Y), mark(Z))) (mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2)), a____#(__(X, Y), Z) -> mark#(X)) (mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2)), a____#(__(X, Y), Z) -> mark#(Y)) (mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2)), a____#(__(X, Y), Z) -> mark#(Z)) (mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2)), a____#(nil(), X) -> mark#(X)) (a____#(__(X, Y), Z) -> mark#(Z), mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2))) (a____#(__(X, Y), Z) -> mark#(Z), mark#(__(X1, X2)) -> mark#(X1)) (a____#(__(X, Y), Z) -> mark#(Z), mark#(__(X1, X2)) -> mark#(X2)) (a____#(__(X, Y), Z) -> mark#(Z), mark#(isList(X)) -> a__isList#(X)) (a____#(__(X, Y), Z) -> mark#(Z), mark#(isNeList(X)) -> a__isNeList#(X)) (a____#(__(X, Y), Z) -> mark#(Z), mark#(isPal(X)) -> a__isPal#(X)) (a____#(__(X, Y), Z) -> mark#(Z), mark#(and(X1, X2)) -> mark#(X1)) (a____#(__(X, Y), Z) -> mark#(Z), mark#(and(X1, X2)) -> a__and#(mark(X1), X2)) (a____#(__(X, Y), Z) -> mark#(Z), mark#(isQid(X)) -> a__isQid#(X)) (a____#(__(X, Y), Z) -> mark#(Z), mark#(isNePal(X)) -> a__isNePal#(X)) } SCCS: Scc: { a____#(X, nil()) -> mark#(X), a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z))), a____#(__(X, Y), Z) -> a____#(mark(Y), mark(Z)), a____#(__(X, Y), Z) -> mark#(X), a____#(__(X, Y), Z) -> mark#(Y), a____#(__(X, Y), Z) -> mark#(Z), a____#(nil(), X) -> mark#(X), mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2)), mark#(__(X1, X2)) -> mark#(X1), mark#(__(X1, X2)) -> mark#(X2), mark#(isList(X)) -> a__isList#(X), mark#(isNeList(X)) -> a__isNeList#(X), mark#(isPal(X)) -> a__isPal#(X), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), mark#(isNePal(X)) -> a__isNePal#(X), a__and#(tt(), X) -> mark#(X), a__isNeList#(__(V1, V2)) -> a__and#(a__isNeList(V1), isList(V2)), a__isNeList#(__(V1, V2)) -> a__and#(a__isList(V1), isNeList(V2)), a__isNeList#(__(V1, V2)) -> a__isNeList#(V1), a__isNeList#(__(V1, V2)) -> a__isList#(V1), a__isList#(V) -> a__isNeList#(V), a__isList#(__(V1, V2)) -> a__and#(a__isList(V1), isList(V2)), a__isList#(__(V1, V2)) -> a__isList#(V1), a__isNePal#(__(I, __(P, I))) -> a__and#(a__isQid(I), isPal(P)), a__isPal#(V) -> a__isNePal#(V)} SCC: Strict: { a____#(X, nil()) -> mark#(X), a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z))), a____#(__(X, Y), Z) -> a____#(mark(Y), mark(Z)), a____#(__(X, Y), Z) -> mark#(X), a____#(__(X, Y), Z) -> mark#(Y), a____#(__(X, Y), Z) -> mark#(Z), a____#(nil(), X) -> mark#(X), mark#(__(X1, X2)) -> a____#(mark(X1), mark(X2)), mark#(__(X1, X2)) -> mark#(X1), mark#(__(X1, X2)) -> mark#(X2), mark#(isList(X)) -> a__isList#(X), mark#(isNeList(X)) -> a__isNeList#(X), mark#(isPal(X)) -> a__isPal#(X), mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2), mark#(isNePal(X)) -> a__isNePal#(X), a__and#(tt(), X) -> mark#(X), a__isNeList#(__(V1, V2)) -> a__and#(a__isNeList(V1), isList(V2)), a__isNeList#(__(V1, V2)) -> a__and#(a__isList(V1), isNeList(V2)), a__isNeList#(__(V1, V2)) -> a__isNeList#(V1), a__isNeList#(__(V1, V2)) -> a__isList#(V1), a__isList#(V) -> a__isNeList#(V), a__isList#(__(V1, V2)) -> a__and#(a__isList(V1), isList(V2)), a__isList#(__(V1, V2)) -> a__isList#(V1), a__isNePal#(__(I, __(P, I))) -> a__and#(a__isQid(I), isPal(P)), a__isPal#(V) -> a__isNePal#(V)} Weak: { a____(X, nil()) -> mark(X), a____(X1, X2) -> __(X1, X2), a____(__(X, Y), Z) -> a____(mark(X), a____(mark(Y), mark(Z))), a____(nil(), X) -> mark(X), mark(__(X1, X2)) -> a____(mark(X1), mark(X2)), mark(nil()) -> nil(), mark(tt()) -> tt(), mark(isList(X)) -> a__isList(X), mark(isNeList(X)) -> a__isNeList(X), mark(isPal(X)) -> a__isPal(X), mark(a()) -> a(), mark(e()) -> e(), mark(i()) -> i(), mark(o()) -> o(), mark(u()) -> u(), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(isQid(X)) -> a__isQid(X), mark(isNePal(X)) -> a__isNePal(X), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark(X), a__isNeList(X) -> isNeList(X), a__isNeList(V) -> a__isQid(V), a__isNeList(__(V1, V2)) -> a__and(a__isNeList(V1), isList(V2)), a__isNeList(__(V1, V2)) -> a__and(a__isList(V1), isNeList(V2)), a__isList(X) -> isList(X), a__isList(V) -> a__isNeList(V), a__isList(__(V1, V2)) -> a__and(a__isList(V1), isList(V2)), a__isList(nil()) -> tt(), a__isQid(X) -> isQid(X), a__isQid(a()) -> tt(), a__isQid(e()) -> tt(), a__isQid(i()) -> tt(), a__isQid(o()) -> tt(), a__isQid(u()) -> tt(), a__isNePal(X) -> isNePal(X), a__isNePal(V) -> a__isQid(V), a__isNePal(__(I, __(P, I))) -> a__and(a__isQid(I), isPal(P)), a__isPal(X) -> isPal(X), a__isPal(V) -> a__isNePal(V), a__isPal(nil()) -> tt()} POLY: Argument Filtering: pi(isNePal) = [0], pi(isQid) = 0, pi(and) = [0,1], pi(u) = [], pi(o) = [], pi(i) = [], pi(e) = [], pi(a) = [], pi(a__isPal#) = 0, pi(a__isPal) = [0], pi(isPal) = [0], pi(a__isNePal#) = 0, pi(a__isNePal) = [0], pi(isNeList) = 0, pi(a__isQid) = 0, pi(isList) = 0, pi(a__isList#) = 0, pi(a__isList) = 0, pi(a__isNeList#) = 0, pi(a__isNeList) = 0, pi(tt) = [], pi(a__and#) = [0,1], pi(a__and) = [0,1], pi(nil) = [], pi(__) = [0,1], pi(mark#) = [0], pi(mark) = 0, pi(a____#) = [0,1], pi(a____) = [0,1] Usable Rules: {} Interpretation: [a__and#](x0, x1) = x0 + x1, [a____#](x0, x1) = x0 + x1 + 1, [mark#](x0) = x0 + 1, [and](x0, x1) = x0 + x1, [__](x0, x1) = x0 + x1 + 1, [a____](x0, x1) = x0 + x1 + 1, [isNePal](x0) = x0 + 1, [isPal](x0) = x0 + 1, [tt] = 1, [nil] = 1 Strict: {a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z))), mark#(and(X1, X2)) -> mark#(X1), a__and#(tt(), X) -> mark#(X), a__isList#(V) -> a__isNeList#(V), a__isPal#(V) -> a__isNePal#(V)} Weak: { a____(X, nil()) -> mark(X), a____(X1, X2) -> __(X1, X2), a____(__(X, Y), Z) -> a____(mark(X), a____(mark(Y), mark(Z))), a____(nil(), X) -> mark(X), mark(__(X1, X2)) -> a____(mark(X1), mark(X2)), mark(nil()) -> nil(), mark(tt()) -> tt(), mark(isList(X)) -> a__isList(X), mark(isNeList(X)) -> a__isNeList(X), mark(isPal(X)) -> a__isPal(X), mark(a()) -> a(), mark(e()) -> e(), mark(i()) -> i(), mark(o()) -> o(), mark(u()) -> u(), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(isQid(X)) -> a__isQid(X), mark(isNePal(X)) -> a__isNePal(X), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark(X), a__isNeList(X) -> isNeList(X), a__isNeList(V) -> a__isQid(V), a__isNeList(__(V1, V2)) -> a__and(a__isNeList(V1), isList(V2)), a__isNeList(__(V1, V2)) -> a__and(a__isList(V1), isNeList(V2)), a__isList(X) -> isList(X), a__isList(V) -> a__isNeList(V), a__isList(__(V1, V2)) -> a__and(a__isList(V1), isList(V2)), a__isList(nil()) -> tt(), a__isQid(X) -> isQid(X), a__isQid(a()) -> tt(), a__isQid(e()) -> tt(), a__isQid(i()) -> tt(), a__isQid(o()) -> tt(), a__isQid(u()) -> tt(), a__isNePal(X) -> isNePal(X), a__isNePal(V) -> a__isQid(V), a__isNePal(__(I, __(P, I))) -> a__and(a__isQid(I), isPal(P)), a__isPal(X) -> isPal(X), a__isPal(V) -> a__isNePal(V), a__isPal(nil()) -> tt()} EDG: {(a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z))), a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z)))) (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1)) (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))} SCCS: Scc: {mark#(and(X1, X2)) -> mark#(X1)} Scc: {a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z)))} SCC: Strict: {mark#(and(X1, X2)) -> mark#(X1)} Weak: { a____(X, nil()) -> mark(X), a____(X1, X2) -> __(X1, X2), a____(__(X, Y), Z) -> a____(mark(X), a____(mark(Y), mark(Z))), a____(nil(), X) -> mark(X), mark(__(X1, X2)) -> a____(mark(X1), mark(X2)), mark(nil()) -> nil(), mark(tt()) -> tt(), mark(isList(X)) -> a__isList(X), mark(isNeList(X)) -> a__isNeList(X), mark(isPal(X)) -> a__isPal(X), mark(a()) -> a(), mark(e()) -> e(), mark(i()) -> i(), mark(o()) -> o(), mark(u()) -> u(), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(isQid(X)) -> a__isQid(X), mark(isNePal(X)) -> a__isNePal(X), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark(X), a__isNeList(X) -> isNeList(X), a__isNeList(V) -> a__isQid(V), a__isNeList(__(V1, V2)) -> a__and(a__isNeList(V1), isList(V2)), a__isNeList(__(V1, V2)) -> a__and(a__isList(V1), isNeList(V2)), a__isList(X) -> isList(X), a__isList(V) -> a__isNeList(V), a__isList(__(V1, V2)) -> a__and(a__isList(V1), isList(V2)), a__isList(nil()) -> tt(), a__isQid(X) -> isQid(X), a__isQid(a()) -> tt(), a__isQid(e()) -> tt(), a__isQid(i()) -> tt(), a__isQid(o()) -> tt(), a__isQid(u()) -> tt(), a__isNePal(X) -> isNePal(X), a__isNePal(V) -> a__isQid(V), a__isNePal(__(I, __(P, I))) -> a__and(a__isQid(I), isPal(P)), a__isPal(X) -> isPal(X), a__isPal(V) -> a__isNePal(V), a__isPal(nil()) -> tt()} SPSC: Simple Projection: pi(mark#) = 0 Strict: {} Qed SCC: Strict: {a____#(__(X, Y), Z) -> a____#(mark(X), a____(mark(Y), mark(Z)))} Weak: { a____(X, nil()) -> mark(X), a____(X1, X2) -> __(X1, X2), a____(__(X, Y), Z) -> a____(mark(X), a____(mark(Y), mark(Z))), a____(nil(), X) -> mark(X), mark(__(X1, X2)) -> a____(mark(X1), mark(X2)), mark(nil()) -> nil(), mark(tt()) -> tt(), mark(isList(X)) -> a__isList(X), mark(isNeList(X)) -> a__isNeList(X), mark(isPal(X)) -> a__isPal(X), mark(a()) -> a(), mark(e()) -> e(), mark(i()) -> i(), mark(o()) -> o(), mark(u()) -> u(), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(isQid(X)) -> a__isQid(X), mark(isNePal(X)) -> a__isNePal(X), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark(X), a__isNeList(X) -> isNeList(X), a__isNeList(V) -> a__isQid(V), a__isNeList(__(V1, V2)) -> a__and(a__isNeList(V1), isList(V2)), a__isNeList(__(V1, V2)) -> a__and(a__isList(V1), isNeList(V2)), a__isList(X) -> isList(X), a__isList(V) -> a__isNeList(V), a__isList(__(V1, V2)) -> a__and(a__isList(V1), isList(V2)), a__isList(nil()) -> tt(), a__isQid(X) -> isQid(X), a__isQid(a()) -> tt(), a__isQid(e()) -> tt(), a__isQid(i()) -> tt(), a__isQid(o()) -> tt(), a__isQid(u()) -> tt(), a__isNePal(X) -> isNePal(X), a__isNePal(V) -> a__isQid(V), a__isNePal(__(I, __(P, I))) -> a__and(a__isQid(I), isPal(P)), a__isPal(X) -> isPal(X), a__isPal(V) -> a__isNePal(V), a__isPal(nil()) -> tt()} POLY: Argument Filtering: pi(isNePal) = [], pi(isQid) = [], pi(and) = 1, pi(u) = [], pi(o) = [], pi(i) = [], pi(e) = [], pi(a) = [], pi(a__isPal) = [], pi(isPal) = [], pi(a__isNePal) = [], pi(isNeList) = [], pi(a__isQid) = [], pi(isList) = [], pi(a__isList) = [], pi(a__isNeList) = [], pi(tt) = [], pi(a__and) = 1, pi(nil) = [], pi(__) = [0,1], pi(mark) = 0, pi(a____#) = 0, pi(a____) = [0,1] Usable Rules: {} Interpretation: [__](x0, x1) = x0 + x1 + 1 Strict: {} Weak: { a____(X, nil()) -> mark(X), a____(X1, X2) -> __(X1, X2), a____(__(X, Y), Z) -> a____(mark(X), a____(mark(Y), mark(Z))), a____(nil(), X) -> mark(X), mark(__(X1, X2)) -> a____(mark(X1), mark(X2)), mark(nil()) -> nil(), mark(tt()) -> tt(), mark(isList(X)) -> a__isList(X), mark(isNeList(X)) -> a__isNeList(X), mark(isPal(X)) -> a__isPal(X), mark(a()) -> a(), mark(e()) -> e(), mark(i()) -> i(), mark(o()) -> o(), mark(u()) -> u(), mark(and(X1, X2)) -> a__and(mark(X1), X2), mark(isQid(X)) -> a__isQid(X), mark(isNePal(X)) -> a__isNePal(X), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark(X), a__isNeList(X) -> isNeList(X), a__isNeList(V) -> a__isQid(V), a__isNeList(__(V1, V2)) -> a__and(a__isNeList(V1), isList(V2)), a__isNeList(__(V1, V2)) -> a__and(a__isList(V1), isNeList(V2)), a__isList(X) -> isList(X), a__isList(V) -> a__isNeList(V), a__isList(__(V1, V2)) -> a__and(a__isList(V1), isList(V2)), a__isList(nil()) -> tt(), a__isQid(X) -> isQid(X), a__isQid(a()) -> tt(), a__isQid(e()) -> tt(), a__isQid(i()) -> tt(), a__isQid(o()) -> tt(), a__isQid(u()) -> tt(), a__isNePal(X) -> isNePal(X), a__isNePal(V) -> a__isQid(V), a__isNePal(__(I, __(P, I))) -> a__and(a__isQid(I), isPal(P)), a__isPal(X) -> isPal(X), a__isPal(V) -> a__isNePal(V), a__isPal(nil()) -> tt()} Qed