MAYBE Problem: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X and(tt(),X) -> activate(X) isList(V) -> isNeList(activate(V)) isList(n__nil()) -> tt() isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) isNeList(V) -> isQid(activate(V)) isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) isNePal(V) -> isQid(activate(V)) isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) isPal(V) -> isNePal(activate(V)) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() __(X1,X2) -> n____(X1,X2) isList(X) -> n__isList(X) isNeList(X) -> n__isNeList(X) isPal(X) -> n__isPal(X) a() -> n__a() e() -> n__e() i() -> n__i() o() -> n__o() u() -> n__u() activate(n__nil()) -> nil() activate(n____(X1,X2)) -> __(X1,X2) activate(n__isList(X)) -> isList(X) 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() activate(X) -> X Proof: DP Processor: DPs: __#(__(X,Y),Z) -> __#(Y,Z) __#(__(X,Y),Z) -> __#(X,__(Y,Z)) and#(tt(),X) -> activate#(X) isList#(V) -> activate#(V) isList#(V) -> isNeList#(activate(V)) isList#(n____(V1,V2)) -> activate#(V2) isList#(n____(V1,V2)) -> activate#(V1) isList#(n____(V1,V2)) -> isList#(activate(V1)) isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) isNeList#(V) -> activate#(V) isNeList#(V) -> isQid#(activate(V)) isNeList#(n____(V1,V2)) -> activate#(V2) isNeList#(n____(V1,V2)) -> activate#(V1) isNeList#(n____(V1,V2)) -> isList#(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)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) isNePal#(V) -> activate#(V) isNePal#(V) -> isQid#(activate(V)) isNePal#(n____(I,__(P,I))) -> activate#(P) isNePal#(n____(I,__(P,I))) -> activate#(I) isNePal#(n____(I,__(P,I))) -> isQid#(activate(I)) isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) isPal#(V) -> activate#(V) isPal#(V) -> isNePal#(activate(V)) activate#(n__nil()) -> nil#() activate#(n____(X1,X2)) -> __#(X1,X2) activate#(n__isList(X)) -> isList#(X) 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#() TRS: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X and(tt(),X) -> activate(X) isList(V) -> isNeList(activate(V)) isList(n__nil()) -> tt() isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) isNeList(V) -> isQid(activate(V)) isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) isNePal(V) -> isQid(activate(V)) isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) isPal(V) -> isNePal(activate(V)) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() __(X1,X2) -> n____(X1,X2) isList(X) -> n__isList(X) isNeList(X) -> n__isNeList(X) isPal(X) -> n__isPal(X) a() -> n__a() e() -> n__e() i() -> n__i() o() -> n__o() u() -> n__u() activate(n__nil()) -> nil() activate(n____(X1,X2)) -> __(X1,X2) activate(n__isList(X)) -> isList(X) 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() activate(X) -> X EDG Processor: DPs: __#(__(X,Y),Z) -> __#(Y,Z) __#(__(X,Y),Z) -> __#(X,__(Y,Z)) and#(tt(),X) -> activate#(X) isList#(V) -> activate#(V) isList#(V) -> isNeList#(activate(V)) isList#(n____(V1,V2)) -> activate#(V2) isList#(n____(V1,V2)) -> activate#(V1) isList#(n____(V1,V2)) -> isList#(activate(V1)) isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) isNeList#(V) -> activate#(V) isNeList#(V) -> isQid#(activate(V)) isNeList#(n____(V1,V2)) -> activate#(V2) isNeList#(n____(V1,V2)) -> activate#(V1) isNeList#(n____(V1,V2)) -> isList#(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)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) isNePal#(V) -> activate#(V) isNePal#(V) -> isQid#(activate(V)) isNePal#(n____(I,__(P,I))) -> activate#(P) isNePal#(n____(I,__(P,I))) -> activate#(I) isNePal#(n____(I,__(P,I))) -> isQid#(activate(I)) isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) isPal#(V) -> activate#(V) isPal#(V) -> isNePal#(activate(V)) activate#(n__nil()) -> nil#() activate#(n____(X1,X2)) -> __#(X1,X2) activate#(n__isList(X)) -> isList#(X) 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#() TRS: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X and(tt(),X) -> activate(X) isList(V) -> isNeList(activate(V)) isList(n__nil()) -> tt() isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) isNeList(V) -> isQid(activate(V)) isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) isNePal(V) -> isQid(activate(V)) isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) isPal(V) -> isNePal(activate(V)) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() __(X1,X2) -> n____(X1,X2) isList(X) -> n__isList(X) isNeList(X) -> n__isNeList(X) isPal(X) -> n__isPal(X) a() -> n__a() e() -> n__e() i() -> n__i() o() -> n__o() u() -> n__u() activate(n__nil()) -> nil() activate(n____(X1,X2)) -> __(X1,X2) activate(n__isList(X)) -> isList(X) 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() activate(X) -> X graph: 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,__(P,I))) -> activate#(P) isPal#(V) -> isNePal#(activate(V)) -> isNePal#(n____(I,__(P,I))) -> activate#(I) isPal#(V) -> isNePal#(activate(V)) -> isNePal#(n____(I,__(P,I))) -> isQid#(activate(I)) isPal#(V) -> isNePal#(activate(V)) -> isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) isPal#(V) -> activate#(V) -> activate#(n__nil()) -> nil#() isPal#(V) -> activate#(V) -> activate#(n____(X1,X2)) -> __#(X1,X2) isPal#(V) -> activate#(V) -> activate#(n__isList(X)) -> isList#(X) isPal#(V) -> activate#(V) -> activate#(n__isNeList(X)) -> isNeList#(X) isPal#(V) -> activate#(V) -> activate#(n__isPal(X)) -> isPal#(X) isPal#(V) -> activate#(V) -> activate#(n__a()) -> a#() isPal#(V) -> activate#(V) -> activate#(n__e()) -> e#() isPal#(V) -> activate#(V) -> activate#(n__i()) -> i#() isPal#(V) -> activate#(V) -> activate#(n__o()) -> o#() isPal#(V) -> activate#(V) -> activate#(n__u()) -> u#() isNePal#(n____(I,__(P,I))) -> activate#(P) -> activate#(n__nil()) -> nil#() isNePal#(n____(I,__(P,I))) -> activate#(P) -> activate#(n____(X1,X2)) -> __#(X1,X2) isNePal#(n____(I,__(P,I))) -> activate#(P) -> activate#(n__isList(X)) -> isList#(X) isNePal#(n____(I,__(P,I))) -> activate#(P) -> activate#(n__isNeList(X)) -> isNeList#(X) isNePal#(n____(I,__(P,I))) -> activate#(P) -> activate#(n__isPal(X)) -> isPal#(X) isNePal#(n____(I,__(P,I))) -> activate#(P) -> activate#(n__a()) -> a#() isNePal#(n____(I,__(P,I))) -> activate#(P) -> activate#(n__e()) -> e#() isNePal#(n____(I,__(P,I))) -> activate#(P) -> activate#(n__i()) -> i#() isNePal#(n____(I,__(P,I))) -> activate#(P) -> activate#(n__o()) -> o#() isNePal#(n____(I,__(P,I))) -> activate#(P) -> activate#(n__u()) -> u#() isNePal#(n____(I,__(P,I))) -> activate#(I) -> activate#(n__nil()) -> nil#() isNePal#(n____(I,__(P,I))) -> activate#(I) -> activate#(n____(X1,X2)) -> __#(X1,X2) isNePal#(n____(I,__(P,I))) -> activate#(I) -> activate#(n__isList(X)) -> isList#(X) isNePal#(n____(I,__(P,I))) -> activate#(I) -> activate#(n__isNeList(X)) -> isNeList#(X) isNePal#(n____(I,__(P,I))) -> activate#(I) -> activate#(n__isPal(X)) -> isPal#(X) 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#() isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) -> and#(tt(),X) -> activate#(X) isNePal#(V) -> activate#(V) -> activate#(n__nil()) -> nil#() isNePal#(V) -> activate#(V) -> activate#(n____(X1,X2)) -> __#(X1,X2) isNePal#(V) -> activate#(V) -> activate#(n__isList(X)) -> isList#(X) 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#(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#(V2) isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) -> isNeList#(n____(V1,V2)) -> activate#(V1) isNeList#(n____(V1,V2)) -> isNeList#(activate(V1)) -> isNeList#(n____(V1,V2)) -> isList#(activate(V1)) 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)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) isNeList#(n____(V1,V2)) -> isList#(activate(V1)) -> isList#(V) -> activate#(V) isNeList#(n____(V1,V2)) -> isList#(activate(V1)) -> isList#(V) -> isNeList#(activate(V)) 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#(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)) -> activate#(V2) -> activate#(n__nil()) -> nil#() isNeList#(n____(V1,V2)) -> activate#(V2) -> activate#(n____(X1,X2)) -> __#(X1,X2) isNeList#(n____(V1,V2)) -> activate#(V2) -> activate#(n__isList(X)) -> isList#(X) isNeList#(n____(V1,V2)) -> activate#(V2) -> activate#(n__isNeList(X)) -> isNeList#(X) isNeList#(n____(V1,V2)) -> activate#(V2) -> activate#(n__isPal(X)) -> isPal#(X) isNeList#(n____(V1,V2)) -> activate#(V2) -> activate#(n__a()) -> a#() isNeList#(n____(V1,V2)) -> activate#(V2) -> activate#(n__e()) -> e#() isNeList#(n____(V1,V2)) -> activate#(V2) -> activate#(n__i()) -> i#() isNeList#(n____(V1,V2)) -> activate#(V2) -> activate#(n__o()) -> o#() isNeList#(n____(V1,V2)) -> activate#(V2) -> activate#(n__u()) -> u#() isNeList#(n____(V1,V2)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isNeList#(n____(V1,V2)) -> activate#(V1) -> activate#(n____(X1,X2)) -> __#(X1,X2) isNeList#(n____(V1,V2)) -> activate#(V1) -> activate#(n__isList(X)) -> isList#(X) isNeList#(n____(V1,V2)) -> activate#(V1) -> activate#(n__isNeList(X)) -> isNeList#(X) isNeList#(n____(V1,V2)) -> activate#(V1) -> activate#(n__isPal(X)) -> isPal#(X) 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#() isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) -> and#(tt(),X) -> activate#(X) isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2))) -> and#(tt(),X) -> activate#(X) isNeList#(V) -> activate#(V) -> activate#(n__nil()) -> nil#() isNeList#(V) -> activate#(V) -> activate#(n____(X1,X2)) -> __#(X1,X2) isNeList#(V) -> activate#(V) -> activate#(n__isList(X)) -> isList#(X) 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#() 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#(V2) isList#(n____(V1,V2)) -> isList#(activate(V1)) -> isList#(n____(V1,V2)) -> activate#(V1) isList#(n____(V1,V2)) -> isList#(activate(V1)) -> isList#(n____(V1,V2)) -> isList#(activate(V1)) isList#(n____(V1,V2)) -> isList#(activate(V1)) -> isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) isList#(n____(V1,V2)) -> activate#(V2) -> activate#(n__nil()) -> nil#() isList#(n____(V1,V2)) -> activate#(V2) -> activate#(n____(X1,X2)) -> __#(X1,X2) isList#(n____(V1,V2)) -> activate#(V2) -> activate#(n__isList(X)) -> isList#(X) 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#() isList#(n____(V1,V2)) -> activate#(V1) -> activate#(n__nil()) -> nil#() isList#(n____(V1,V2)) -> activate#(V1) -> activate#(n____(X1,X2)) -> __#(X1,X2) isList#(n____(V1,V2)) -> activate#(V1) -> activate#(n__isList(X)) -> isList#(X) 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#() isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) -> and#(tt(),X) -> activate#(X) 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#(V2) isList#(V) -> isNeList#(activate(V)) -> isNeList#(n____(V1,V2)) -> activate#(V1) isList#(V) -> isNeList#(activate(V)) -> isNeList#(n____(V1,V2)) -> isList#(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)) -> isNeList#(activate(V1)) isList#(V) -> isNeList#(activate(V)) -> isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) isList#(V) -> activate#(V) -> activate#(n__nil()) -> nil#() isList#(V) -> activate#(V) -> activate#(n____(X1,X2)) -> __#(X1,X2) isList#(V) -> activate#(V) -> activate#(n__isList(X)) -> isList#(X) isList#(V) -> activate#(V) -> activate#(n__isNeList(X)) -> isNeList#(X) isList#(V) -> activate#(V) -> activate#(n__isPal(X)) -> isPal#(X) 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#() activate#(n__isPal(X)) -> isPal#(X) -> isPal#(V) -> activate#(V) activate#(n__isPal(X)) -> isPal#(X) -> isPal#(V) -> isNePal#(activate(V)) 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#(V2) activate#(n__isNeList(X)) -> isNeList#(X) -> isNeList#(n____(V1,V2)) -> activate#(V1) activate#(n__isNeList(X)) -> isNeList#(X) -> isNeList#(n____(V1,V2)) -> isList#(activate(V1)) 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)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) activate#(n__isList(X)) -> isList#(X) -> isList#(V) -> activate#(V) activate#(n__isList(X)) -> isList#(X) -> isList#(V) -> isNeList#(activate(V)) 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#(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____(X1,X2)) -> __#(X1,X2) -> __#(__(X,Y),Z) -> __#(Y,Z) activate#(n____(X1,X2)) -> __#(X1,X2) -> __#(__(X,Y),Z) -> __#(X,__(Y,Z)) and#(tt(),X) -> activate#(X) -> activate#(n__nil()) -> nil#() and#(tt(),X) -> activate#(X) -> activate#(n____(X1,X2)) -> __#(X1,X2) and#(tt(),X) -> activate#(X) -> activate#(n__isList(X)) -> isList#(X) 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#() __#(__(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) -> __#(Y,Z) __#(__(X,Y),Z) -> __#(X,__(Y,Z)) -> __#(__(X,Y),Z) -> __#(X,__(Y,Z)) Restore Modifier: DPs: __#(__(X,Y),Z) -> __#(Y,Z) __#(__(X,Y),Z) -> __#(X,__(Y,Z)) and#(tt(),X) -> activate#(X) isList#(V) -> activate#(V) isList#(V) -> isNeList#(activate(V)) isList#(n____(V1,V2)) -> activate#(V2) isList#(n____(V1,V2)) -> activate#(V1) isList#(n____(V1,V2)) -> isList#(activate(V1)) isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2))) isNeList#(V) -> activate#(V) isNeList#(V) -> isQid#(activate(V)) isNeList#(n____(V1,V2)) -> activate#(V2) isNeList#(n____(V1,V2)) -> activate#(V1) isNeList#(n____(V1,V2)) -> isList#(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)) -> and#(isNeList(activate(V1)),n__isList(activate(V2))) isNePal#(V) -> activate#(V) isNePal#(V) -> isQid#(activate(V)) isNePal#(n____(I,__(P,I))) -> activate#(P) isNePal#(n____(I,__(P,I))) -> activate#(I) isNePal#(n____(I,__(P,I))) -> isQid#(activate(I)) isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) isPal#(V) -> activate#(V) isPal#(V) -> isNePal#(activate(V)) activate#(n__nil()) -> nil#() activate#(n____(X1,X2)) -> __#(X1,X2) activate#(n__isList(X)) -> isList#(X) 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#() TRS: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X and(tt(),X) -> activate(X) isList(V) -> isNeList(activate(V)) isList(n__nil()) -> tt() isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) isNeList(V) -> isQid(activate(V)) isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) isNePal(V) -> isQid(activate(V)) isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) isPal(V) -> isNePal(activate(V)) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() __(X1,X2) -> n____(X1,X2) isList(X) -> n__isList(X) isNeList(X) -> n__isNeList(X) isPal(X) -> n__isPal(X) a() -> n__a() e() -> n__e() i() -> n__i() o() -> n__o() u() -> n__u() activate(n__nil()) -> nil() activate(n____(X1,X2)) -> __(X1,X2) activate(n__isList(X)) -> isList(X) 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() activate(X) -> X SCC Processor: #sccs: 2 #rules: 25 #arcs: 170/1225 DPs: isPal#(V) -> isNePal#(activate(V)) isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P))) and#(tt(),X) -> activate#(X) activate#(n__isPal(X)) -> isPal#(X) isPal#(V) -> activate#(V) activate#(n__isNeList(X)) -> isNeList#(X) 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)) -> 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)) -> activate#(V1) activate#(n__isList(X)) -> isList#(X) isList#(n____(V1,V2)) -> activate#(V2) isList#(V) -> isNeList#(activate(V)) isNeList#(n____(V1,V2)) -> activate#(V1) isNeList#(n____(V1,V2)) -> activate#(V2) isNeList#(V) -> activate#(V) isList#(V) -> activate#(V) isNePal#(n____(I,__(P,I))) -> activate#(I) isNePal#(n____(I,__(P,I))) -> activate#(P) isNePal#(V) -> activate#(V) TRS: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X and(tt(),X) -> activate(X) isList(V) -> isNeList(activate(V)) isList(n__nil()) -> tt() isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) isNeList(V) -> isQid(activate(V)) isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) isNePal(V) -> isQid(activate(V)) isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) isPal(V) -> isNePal(activate(V)) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() __(X1,X2) -> n____(X1,X2) isList(X) -> n__isList(X) isNeList(X) -> n__isNeList(X) isPal(X) -> n__isPal(X) a() -> n__a() e() -> n__e() i() -> n__i() o() -> n__o() u() -> n__u() activate(n__nil()) -> nil() activate(n____(X1,X2)) -> __(X1,X2) activate(n__isList(X)) -> isList(X) 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() activate(X) -> X Open DPs: __#(__(X,Y),Z) -> __#(X,__(Y,Z)) __#(__(X,Y),Z) -> __#(Y,Z) TRS: __(__(X,Y),Z) -> __(X,__(Y,Z)) __(X,nil()) -> X __(nil(),X) -> X and(tt(),X) -> activate(X) isList(V) -> isNeList(activate(V)) isList(n__nil()) -> tt() isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2))) isNeList(V) -> isQid(activate(V)) isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2))) isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2))) isNePal(V) -> isQid(activate(V)) isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P))) isPal(V) -> isNePal(activate(V)) isPal(n__nil()) -> tt() isQid(n__a()) -> tt() isQid(n__e()) -> tt() isQid(n__i()) -> tt() isQid(n__o()) -> tt() isQid(n__u()) -> tt() nil() -> n__nil() __(X1,X2) -> n____(X1,X2) isList(X) -> n__isList(X) isNeList(X) -> n__isNeList(X) isPal(X) -> n__isPal(X) a() -> n__a() e() -> n__e() i() -> n__i() o() -> n__o() u() -> n__u() activate(n__nil()) -> nil() activate(n____(X1,X2)) -> __(X1,X2) activate(n__isList(X)) -> isList(X) 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() activate(X) -> X Open