YES TRS: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z))) a____(X,nil()) -> mark(X) a____(nil(),X) -> mark(X) a__U11(tt()) -> tt() a__U21(tt(),V2) -> a__U22(a__isList(V2)) a__U22(tt()) -> tt() a__U31(tt()) -> tt() a__U41(tt(),V2) -> a__U42(a__isNeList(V2)) a__U42(tt()) -> tt() a__U51(tt(),V2) -> a__U52(a__isList(V2)) a__U52(tt()) -> tt() a__U61(tt()) -> tt() a__U71(tt(),P) -> a__U72(a__isPal(P)) a__U72(tt()) -> tt() a__U81(tt()) -> tt() a__isList(V) -> a__U11(a__isNeList(V)) a__isList(nil()) -> tt() a__isList(__(V1,V2)) -> a__U21(a__isList(V1),V2) a__isNeList(V) -> a__U31(a__isQid(V)) a__isNeList(__(V1,V2)) -> a__U41(a__isList(V1),V2) a__isNeList(__(V1,V2)) -> a__U51(a__isNeList(V1),V2) a__isNePal(V) -> a__U61(a__isQid(V)) a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),P) a__isPal(V) -> a__U81(a__isNePal(V)) a__isPal(nil()) -> tt() a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(U11(X)) -> a__U11(mark(X)) mark(U21(X1,X2)) -> a__U21(mark(X1),X2) mark(U22(X)) -> a__U22(mark(X)) mark(isList(X)) -> a__isList(X) mark(U31(X)) -> a__U31(mark(X)) mark(U41(X1,X2)) -> a__U41(mark(X1),X2) mark(U42(X)) -> a__U42(mark(X)) mark(isNeList(X)) -> a__isNeList(X) mark(U51(X1,X2)) -> a__U51(mark(X1),X2) mark(U52(X)) -> a__U52(mark(X)) mark(U61(X)) -> a__U61(mark(X)) mark(U71(X1,X2)) -> a__U71(mark(X1),X2) mark(U72(X)) -> a__U72(mark(X)) mark(isPal(X)) -> a__isPal(X) mark(U81(X)) -> a__U81(mark(X)) mark(isQid(X)) -> a__isQid(X) mark(isNePal(X)) -> a__isNePal(X) mark(nil()) -> nil() mark(tt()) -> tt() mark(a()) -> a() mark(e()) -> e() mark(i()) -> i() mark(o()) -> o() mark(u()) -> u() a____(X1,X2) -> __(X1,X2) a__U11(X) -> U11(X) a__U21(X1,X2) -> U21(X1,X2) a__U22(X) -> U22(X) a__isList(X) -> isList(X) a__U31(X) -> U31(X) a__U41(X1,X2) -> U41(X1,X2) a__U42(X) -> U42(X) a__isNeList(X) -> isNeList(X) a__U51(X1,X2) -> U51(X1,X2) a__U52(X) -> U52(X) a__U61(X) -> U61(X) a__U71(X1,X2) -> U71(X1,X2) a__U72(X) -> U72(X) a__isPal(X) -> isPal(X) a__U81(X) -> U81(X) a__isQid(X) -> isQid(X) a__isNePal(X) -> isNePal(X) linear polynomial interpretations on N: a_____A(x1,x2) = x1 + x2 + 3 a____#_A(x1,x2) = x1 + x2 + 3 ___A(x1,x2) = x1 + x2 + 3 __#_A(x1,x2) = x1 + x2 + 3 mark_A(x1) = x1 mark#_A(x1) = x1 nil_A = 4 nil#_A = 4 a__U11_A(x1) = x1 a__U11#_A(x1) = x1 tt_A = 3 tt#_A = 3 a__U21_A(x1,x2) = x1 + x2 a__U21#_A(x1,x2) = x1 + x2 a__U22_A(x1) = x1 a__U22#_A(x1) = x1 a__isList_A(x1) = x1 + 2 a__isList#_A(x1) = x1 + 2 a__U31_A(x1) = x1 a__U31#_A(x1) = x1 a__U41_A(x1,x2) = x1 + x2 a__U41#_A(x1,x2) = x1 + x2 a__U42_A(x1) = x1 a__U42#_A(x1) = x1 a__isNeList_A(x1) = x1 + 1 a__isNeList#_A(x1) = x1 + 1 a__U51_A(x1,x2) = x1 + x2 a__U51#_A(x1,x2) = x1 + x2 a__U52_A(x1) = x1 a__U52#_A(x1) = x1 a__U61_A(x1) = x1 a__U61#_A(x1) = x1 a__U71_A(x1,x2) = x1 + x2 a__U71#_A(x1,x2) = x1 + x2 a__U72_A(x1) = x1 a__U72#_A(x1) = x1 a__isPal_A(x1) = x1 + 2 a__isPal#_A(x1) = x1 + 2 a__U81_A(x1) = x1 a__U81#_A(x1) = x1 a__isQid_A(x1) = x1 a__isQid#_A(x1) = x1 a__isNePal_A(x1) = x1 + 1 a__isNePal#_A(x1) = x1 + 1 a_A = 4 a#_A = 4 e_A = 4 e#_A = 4 i_A = 4 i#_A = 4 o_A = 4 o#_A = 4 u_A = 4 u#_A = 4 U11_A(x1) = x1 U11#_A(x1) = x1 U21_A(x1,x2) = x1 + x2 U21#_A(x1,x2) = x1 + x2 U22_A(x1) = x1 U22#_A(x1) = x1 isList_A(x1) = x1 + 2 isList#_A(x1) = x1 + 2 U31_A(x1) = x1 U31#_A(x1) = x1 U41_A(x1,x2) = x1 + x2 U41#_A(x1,x2) = x1 + x2 U42_A(x1) = x1 U42#_A(x1) = x1 isNeList_A(x1) = x1 + 1 isNeList#_A(x1) = x1 + 1 U51_A(x1,x2) = x1 + x2 U51#_A(x1,x2) = x1 + x2 U52_A(x1) = x1 U52#_A(x1) = x1 U61_A(x1) = x1 U61#_A(x1) = x1 U71_A(x1,x2) = x1 + x2 U71#_A(x1,x2) = x1 + x2 U72_A(x1) = x1 U72#_A(x1) = x1 isPal_A(x1) = x1 + 2 isPal#_A(x1) = x1 + 2 U81_A(x1) = x1 U81#_A(x1) = x1 isQid_A(x1) = x1 isQid#_A(x1) = x1 isNePal_A(x1) = x1 + 1 isNePal#_A(x1) = x1 + 1 precedence: a = e = i = o = u > tt > mark > a____ = nil = a__isPal > __ = a__U81 = a__isNePal = isPal > a__isNeList = a__U61 = a__U71 = U81 = isNePal > a__U31 = a__U41 = a__U51 = a__U72 = a__isQid = isNeList = U61 = U71 > a__isList = a__U42 = a__U52 = U31 = U41 = U51 = U72 = isQid > a__U11 = a__U21 = isList = U42 = U52 > a__U22 = U11 = U21 > U22