YES

We show the termination of the TRS R:

  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(),V) -> a__U12(a__isPalListKind(V),V)
  a__U12(tt(),V) -> a__U13(a__isNeList(V))
  a__U13(tt()) -> tt()
  a__U21(tt(),V1,V2) -> a__U22(a__isPalListKind(V1),V1,V2)
  a__U22(tt(),V1,V2) -> a__U23(a__isPalListKind(V2),V1,V2)
  a__U23(tt(),V1,V2) -> a__U24(a__isPalListKind(V2),V1,V2)
  a__U24(tt(),V1,V2) -> a__U25(a__isList(V1),V2)
  a__U25(tt(),V2) -> a__U26(a__isList(V2))
  a__U26(tt()) -> tt()
  a__U31(tt(),V) -> a__U32(a__isPalListKind(V),V)
  a__U32(tt(),V) -> a__U33(a__isQid(V))
  a__U33(tt()) -> tt()
  a__U41(tt(),V1,V2) -> a__U42(a__isPalListKind(V1),V1,V2)
  a__U42(tt(),V1,V2) -> a__U43(a__isPalListKind(V2),V1,V2)
  a__U43(tt(),V1,V2) -> a__U44(a__isPalListKind(V2),V1,V2)
  a__U44(tt(),V1,V2) -> a__U45(a__isList(V1),V2)
  a__U45(tt(),V2) -> a__U46(a__isNeList(V2))
  a__U46(tt()) -> tt()
  a__U51(tt(),V1,V2) -> a__U52(a__isPalListKind(V1),V1,V2)
  a__U52(tt(),V1,V2) -> a__U53(a__isPalListKind(V2),V1,V2)
  a__U53(tt(),V1,V2) -> a__U54(a__isPalListKind(V2),V1,V2)
  a__U54(tt(),V1,V2) -> a__U55(a__isNeList(V1),V2)
  a__U55(tt(),V2) -> a__U56(a__isList(V2))
  a__U56(tt()) -> tt()
  a__U61(tt(),V) -> a__U62(a__isPalListKind(V),V)
  a__U62(tt(),V) -> a__U63(a__isQid(V))
  a__U63(tt()) -> tt()
  a__U71(tt(),I,P) -> a__U72(a__isPalListKind(I),P)
  a__U72(tt(),P) -> a__U73(a__isPal(P),P)
  a__U73(tt(),P) -> a__U74(a__isPalListKind(P))
  a__U74(tt()) -> tt()
  a__U81(tt(),V) -> a__U82(a__isPalListKind(V),V)
  a__U82(tt(),V) -> a__U83(a__isNePal(V))
  a__U83(tt()) -> tt()
  a__U91(tt(),V2) -> a__U92(a__isPalListKind(V2))
  a__U92(tt()) -> tt()
  a__isList(V) -> a__U11(a__isPalListKind(V),V)
  a__isList(nil()) -> tt()
  a__isList(__(V1,V2)) -> a__U21(a__isPalListKind(V1),V1,V2)
  a__isNeList(V) -> a__U31(a__isPalListKind(V),V)
  a__isNeList(__(V1,V2)) -> a__U41(a__isPalListKind(V1),V1,V2)
  a__isNeList(__(V1,V2)) -> a__U51(a__isPalListKind(V1),V1,V2)
  a__isNePal(V) -> a__U61(a__isPalListKind(V),V)
  a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),I,P)
  a__isPal(V) -> a__U81(a__isPalListKind(V),V)
  a__isPal(nil()) -> tt()
  a__isPalListKind(a()) -> tt()
  a__isPalListKind(e()) -> tt()
  a__isPalListKind(i()) -> tt()
  a__isPalListKind(nil()) -> tt()
  a__isPalListKind(o()) -> tt()
  a__isPalListKind(u()) -> tt()
  a__isPalListKind(__(V1,V2)) -> a__U91(a__isPalListKind(V1),V2)
  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(X1,X2)) -> a__U11(mark(X1),X2)
  mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
  mark(isPalListKind(X)) -> a__isPalListKind(X)
  mark(U13(X)) -> a__U13(mark(X))
  mark(isNeList(X)) -> a__isNeList(X)
  mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
  mark(U22(X1,X2,X3)) -> a__U22(mark(X1),X2,X3)
  mark(U23(X1,X2,X3)) -> a__U23(mark(X1),X2,X3)
  mark(U24(X1,X2,X3)) -> a__U24(mark(X1),X2,X3)
  mark(U25(X1,X2)) -> a__U25(mark(X1),X2)
  mark(isList(X)) -> a__isList(X)
  mark(U26(X)) -> a__U26(mark(X))
  mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
  mark(U32(X1,X2)) -> a__U32(mark(X1),X2)
  mark(U33(X)) -> a__U33(mark(X))
  mark(isQid(X)) -> a__isQid(X)
  mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
  mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
  mark(U43(X1,X2,X3)) -> a__U43(mark(X1),X2,X3)
  mark(U44(X1,X2,X3)) -> a__U44(mark(X1),X2,X3)
  mark(U45(X1,X2)) -> a__U45(mark(X1),X2)
  mark(U46(X)) -> a__U46(mark(X))
  mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
  mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
  mark(U53(X1,X2,X3)) -> a__U53(mark(X1),X2,X3)
  mark(U54(X1,X2,X3)) -> a__U54(mark(X1),X2,X3)
  mark(U55(X1,X2)) -> a__U55(mark(X1),X2)
  mark(U56(X)) -> a__U56(mark(X))
  mark(U61(X1,X2)) -> a__U61(mark(X1),X2)
  mark(U62(X1,X2)) -> a__U62(mark(X1),X2)
  mark(U63(X)) -> a__U63(mark(X))
  mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
  mark(U72(X1,X2)) -> a__U72(mark(X1),X2)
  mark(U73(X1,X2)) -> a__U73(mark(X1),X2)
  mark(isPal(X)) -> a__isPal(X)
  mark(U74(X)) -> a__U74(mark(X))
  mark(U81(X1,X2)) -> a__U81(mark(X1),X2)
  mark(U82(X1,X2)) -> a__U82(mark(X1),X2)
  mark(U83(X)) -> a__U83(mark(X))
  mark(isNePal(X)) -> a__isNePal(X)
  mark(U91(X1,X2)) -> a__U91(mark(X1),X2)
  mark(U92(X)) -> a__U92(mark(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(X1,X2) -> U11(X1,X2)
  a__U12(X1,X2) -> U12(X1,X2)
  a__isPalListKind(X) -> isPalListKind(X)
  a__U13(X) -> U13(X)
  a__isNeList(X) -> isNeList(X)
  a__U21(X1,X2,X3) -> U21(X1,X2,X3)
  a__U22(X1,X2,X3) -> U22(X1,X2,X3)
  a__U23(X1,X2,X3) -> U23(X1,X2,X3)
  a__U24(X1,X2,X3) -> U24(X1,X2,X3)
  a__U25(X1,X2) -> U25(X1,X2)
  a__isList(X) -> isList(X)
  a__U26(X) -> U26(X)
  a__U31(X1,X2) -> U31(X1,X2)
  a__U32(X1,X2) -> U32(X1,X2)
  a__U33(X) -> U33(X)
  a__isQid(X) -> isQid(X)
  a__U41(X1,X2,X3) -> U41(X1,X2,X3)
  a__U42(X1,X2,X3) -> U42(X1,X2,X3)
  a__U43(X1,X2,X3) -> U43(X1,X2,X3)
  a__U44(X1,X2,X3) -> U44(X1,X2,X3)
  a__U45(X1,X2) -> U45(X1,X2)
  a__U46(X) -> U46(X)
  a__U51(X1,X2,X3) -> U51(X1,X2,X3)
  a__U52(X1,X2,X3) -> U52(X1,X2,X3)
  a__U53(X1,X2,X3) -> U53(X1,X2,X3)
  a__U54(X1,X2,X3) -> U54(X1,X2,X3)
  a__U55(X1,X2) -> U55(X1,X2)
  a__U56(X) -> U56(X)
  a__U61(X1,X2) -> U61(X1,X2)
  a__U62(X1,X2) -> U62(X1,X2)
  a__U63(X) -> U63(X)
  a__U71(X1,X2,X3) -> U71(X1,X2,X3)
  a__U72(X1,X2) -> U72(X1,X2)
  a__U73(X1,X2) -> U73(X1,X2)
  a__isPal(X) -> isPal(X)
  a__U74(X) -> U74(X)
  a__U81(X1,X2) -> U81(X1,X2)
  a__U82(X1,X2) -> U82(X1,X2)
  a__U83(X) -> U83(X)
  a__isNePal(X) -> isNePal(X)
  a__U91(X1,X2) -> U91(X1,X2)
  a__U92(X) -> U92(X)

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: a____#(__(X,Y),Z) -> a____#(mark(X),a____(mark(Y),mark(Z)))
p2: a____#(__(X,Y),Z) -> mark#(X)
p3: a____#(__(X,Y),Z) -> a____#(mark(Y),mark(Z))
p4: a____#(__(X,Y),Z) -> mark#(Y)
p5: a____#(__(X,Y),Z) -> mark#(Z)
p6: a____#(X,nil()) -> mark#(X)
p7: a____#(nil(),X) -> mark#(X)
p8: a__U11#(tt(),V) -> a__U12#(a__isPalListKind(V),V)
p9: a__U11#(tt(),V) -> a__isPalListKind#(V)
p10: a__U12#(tt(),V) -> a__U13#(a__isNeList(V))
p11: a__U12#(tt(),V) -> a__isNeList#(V)
p12: a__U21#(tt(),V1,V2) -> a__U22#(a__isPalListKind(V1),V1,V2)
p13: a__U21#(tt(),V1,V2) -> a__isPalListKind#(V1)
p14: a__U22#(tt(),V1,V2) -> a__U23#(a__isPalListKind(V2),V1,V2)
p15: a__U22#(tt(),V1,V2) -> a__isPalListKind#(V2)
p16: a__U23#(tt(),V1,V2) -> a__U24#(a__isPalListKind(V2),V1,V2)
p17: a__U23#(tt(),V1,V2) -> a__isPalListKind#(V2)
p18: a__U24#(tt(),V1,V2) -> a__U25#(a__isList(V1),V2)
p19: a__U24#(tt(),V1,V2) -> a__isList#(V1)
p20: a__U25#(tt(),V2) -> a__U26#(a__isList(V2))
p21: a__U25#(tt(),V2) -> a__isList#(V2)
p22: a__U31#(tt(),V) -> a__U32#(a__isPalListKind(V),V)
p23: a__U31#(tt(),V) -> a__isPalListKind#(V)
p24: a__U32#(tt(),V) -> a__U33#(a__isQid(V))
p25: a__U32#(tt(),V) -> a__isQid#(V)
p26: a__U41#(tt(),V1,V2) -> a__U42#(a__isPalListKind(V1),V1,V2)
p27: a__U41#(tt(),V1,V2) -> a__isPalListKind#(V1)
p28: a__U42#(tt(),V1,V2) -> a__U43#(a__isPalListKind(V2),V1,V2)
p29: a__U42#(tt(),V1,V2) -> a__isPalListKind#(V2)
p30: a__U43#(tt(),V1,V2) -> a__U44#(a__isPalListKind(V2),V1,V2)
p31: a__U43#(tt(),V1,V2) -> a__isPalListKind#(V2)
p32: a__U44#(tt(),V1,V2) -> a__U45#(a__isList(V1),V2)
p33: a__U44#(tt(),V1,V2) -> a__isList#(V1)
p34: a__U45#(tt(),V2) -> a__U46#(a__isNeList(V2))
p35: a__U45#(tt(),V2) -> a__isNeList#(V2)
p36: a__U51#(tt(),V1,V2) -> a__U52#(a__isPalListKind(V1),V1,V2)
p37: a__U51#(tt(),V1,V2) -> a__isPalListKind#(V1)
p38: a__U52#(tt(),V1,V2) -> a__U53#(a__isPalListKind(V2),V1,V2)
p39: a__U52#(tt(),V1,V2) -> a__isPalListKind#(V2)
p40: a__U53#(tt(),V1,V2) -> a__U54#(a__isPalListKind(V2),V1,V2)
p41: a__U53#(tt(),V1,V2) -> a__isPalListKind#(V2)
p42: a__U54#(tt(),V1,V2) -> a__U55#(a__isNeList(V1),V2)
p43: a__U54#(tt(),V1,V2) -> a__isNeList#(V1)
p44: a__U55#(tt(),V2) -> a__U56#(a__isList(V2))
p45: a__U55#(tt(),V2) -> a__isList#(V2)
p46: a__U61#(tt(),V) -> a__U62#(a__isPalListKind(V),V)
p47: a__U61#(tt(),V) -> a__isPalListKind#(V)
p48: a__U62#(tt(),V) -> a__U63#(a__isQid(V))
p49: a__U62#(tt(),V) -> a__isQid#(V)
p50: a__U71#(tt(),I,P) -> a__U72#(a__isPalListKind(I),P)
p51: a__U71#(tt(),I,P) -> a__isPalListKind#(I)
p52: a__U72#(tt(),P) -> a__U73#(a__isPal(P),P)
p53: a__U72#(tt(),P) -> a__isPal#(P)
p54: a__U73#(tt(),P) -> a__U74#(a__isPalListKind(P))
p55: a__U73#(tt(),P) -> a__isPalListKind#(P)
p56: a__U81#(tt(),V) -> a__U82#(a__isPalListKind(V),V)
p57: a__U81#(tt(),V) -> a__isPalListKind#(V)
p58: a__U82#(tt(),V) -> a__U83#(a__isNePal(V))
p59: a__U82#(tt(),V) -> a__isNePal#(V)
p60: a__U91#(tt(),V2) -> a__U92#(a__isPalListKind(V2))
p61: a__U91#(tt(),V2) -> a__isPalListKind#(V2)
p62: a__isList#(V) -> a__U11#(a__isPalListKind(V),V)
p63: a__isList#(V) -> a__isPalListKind#(V)
p64: a__isList#(__(V1,V2)) -> a__U21#(a__isPalListKind(V1),V1,V2)
p65: a__isList#(__(V1,V2)) -> a__isPalListKind#(V1)
p66: a__isNeList#(V) -> a__U31#(a__isPalListKind(V),V)
p67: a__isNeList#(V) -> a__isPalListKind#(V)
p68: a__isNeList#(__(V1,V2)) -> a__U41#(a__isPalListKind(V1),V1,V2)
p69: a__isNeList#(__(V1,V2)) -> a__isPalListKind#(V1)
p70: a__isNeList#(__(V1,V2)) -> a__U51#(a__isPalListKind(V1),V1,V2)
p71: a__isNeList#(__(V1,V2)) -> a__isPalListKind#(V1)
p72: a__isNePal#(V) -> a__U61#(a__isPalListKind(V),V)
p73: a__isNePal#(V) -> a__isPalListKind#(V)
p74: a__isNePal#(__(I,__(P,I))) -> a__U71#(a__isQid(I),I,P)
p75: a__isNePal#(__(I,__(P,I))) -> a__isQid#(I)
p76: a__isPal#(V) -> a__U81#(a__isPalListKind(V),V)
p77: a__isPal#(V) -> a__isPalListKind#(V)
p78: a__isPalListKind#(__(V1,V2)) -> a__U91#(a__isPalListKind(V1),V2)
p79: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1)
p80: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p81: mark#(__(X1,X2)) -> mark#(X1)
p82: mark#(__(X1,X2)) -> mark#(X2)
p83: mark#(U11(X1,X2)) -> a__U11#(mark(X1),X2)
p84: mark#(U11(X1,X2)) -> mark#(X1)
p85: mark#(U12(X1,X2)) -> a__U12#(mark(X1),X2)
p86: mark#(U12(X1,X2)) -> mark#(X1)
p87: mark#(isPalListKind(X)) -> a__isPalListKind#(X)
p88: mark#(U13(X)) -> a__U13#(mark(X))
p89: mark#(U13(X)) -> mark#(X)
p90: mark#(isNeList(X)) -> a__isNeList#(X)
p91: mark#(U21(X1,X2,X3)) -> a__U21#(mark(X1),X2,X3)
p92: mark#(U21(X1,X2,X3)) -> mark#(X1)
p93: mark#(U22(X1,X2,X3)) -> a__U22#(mark(X1),X2,X3)
p94: mark#(U22(X1,X2,X3)) -> mark#(X1)
p95: mark#(U23(X1,X2,X3)) -> a__U23#(mark(X1),X2,X3)
p96: mark#(U23(X1,X2,X3)) -> mark#(X1)
p97: mark#(U24(X1,X2,X3)) -> a__U24#(mark(X1),X2,X3)
p98: mark#(U24(X1,X2,X3)) -> mark#(X1)
p99: mark#(U25(X1,X2)) -> a__U25#(mark(X1),X2)
p100: mark#(U25(X1,X2)) -> mark#(X1)
p101: mark#(isList(X)) -> a__isList#(X)
p102: mark#(U26(X)) -> a__U26#(mark(X))
p103: mark#(U26(X)) -> mark#(X)
p104: mark#(U31(X1,X2)) -> a__U31#(mark(X1),X2)
p105: mark#(U31(X1,X2)) -> mark#(X1)
p106: mark#(U32(X1,X2)) -> a__U32#(mark(X1),X2)
p107: mark#(U32(X1,X2)) -> mark#(X1)
p108: mark#(U33(X)) -> a__U33#(mark(X))
p109: mark#(U33(X)) -> mark#(X)
p110: mark#(isQid(X)) -> a__isQid#(X)
p111: mark#(U41(X1,X2,X3)) -> a__U41#(mark(X1),X2,X3)
p112: mark#(U41(X1,X2,X3)) -> mark#(X1)
p113: mark#(U42(X1,X2,X3)) -> a__U42#(mark(X1),X2,X3)
p114: mark#(U42(X1,X2,X3)) -> mark#(X1)
p115: mark#(U43(X1,X2,X3)) -> a__U43#(mark(X1),X2,X3)
p116: mark#(U43(X1,X2,X3)) -> mark#(X1)
p117: mark#(U44(X1,X2,X3)) -> a__U44#(mark(X1),X2,X3)
p118: mark#(U44(X1,X2,X3)) -> mark#(X1)
p119: mark#(U45(X1,X2)) -> a__U45#(mark(X1),X2)
p120: mark#(U45(X1,X2)) -> mark#(X1)
p121: mark#(U46(X)) -> a__U46#(mark(X))
p122: mark#(U46(X)) -> mark#(X)
p123: mark#(U51(X1,X2,X3)) -> a__U51#(mark(X1),X2,X3)
p124: mark#(U51(X1,X2,X3)) -> mark#(X1)
p125: mark#(U52(X1,X2,X3)) -> a__U52#(mark(X1),X2,X3)
p126: mark#(U52(X1,X2,X3)) -> mark#(X1)
p127: mark#(U53(X1,X2,X3)) -> a__U53#(mark(X1),X2,X3)
p128: mark#(U53(X1,X2,X3)) -> mark#(X1)
p129: mark#(U54(X1,X2,X3)) -> a__U54#(mark(X1),X2,X3)
p130: mark#(U54(X1,X2,X3)) -> mark#(X1)
p131: mark#(U55(X1,X2)) -> a__U55#(mark(X1),X2)
p132: mark#(U55(X1,X2)) -> mark#(X1)
p133: mark#(U56(X)) -> a__U56#(mark(X))
p134: mark#(U56(X)) -> mark#(X)
p135: mark#(U61(X1,X2)) -> a__U61#(mark(X1),X2)
p136: mark#(U61(X1,X2)) -> mark#(X1)
p137: mark#(U62(X1,X2)) -> a__U62#(mark(X1),X2)
p138: mark#(U62(X1,X2)) -> mark#(X1)
p139: mark#(U63(X)) -> a__U63#(mark(X))
p140: mark#(U63(X)) -> mark#(X)
p141: mark#(U71(X1,X2,X3)) -> a__U71#(mark(X1),X2,X3)
p142: mark#(U71(X1,X2,X3)) -> mark#(X1)
p143: mark#(U72(X1,X2)) -> a__U72#(mark(X1),X2)
p144: mark#(U72(X1,X2)) -> mark#(X1)
p145: mark#(U73(X1,X2)) -> a__U73#(mark(X1),X2)
p146: mark#(U73(X1,X2)) -> mark#(X1)
p147: mark#(isPal(X)) -> a__isPal#(X)
p148: mark#(U74(X)) -> a__U74#(mark(X))
p149: mark#(U74(X)) -> mark#(X)
p150: mark#(U81(X1,X2)) -> a__U81#(mark(X1),X2)
p151: mark#(U81(X1,X2)) -> mark#(X1)
p152: mark#(U82(X1,X2)) -> a__U82#(mark(X1),X2)
p153: mark#(U82(X1,X2)) -> mark#(X1)
p154: mark#(U83(X)) -> a__U83#(mark(X))
p155: mark#(U83(X)) -> mark#(X)
p156: mark#(isNePal(X)) -> a__isNePal#(X)
p157: mark#(U91(X1,X2)) -> a__U91#(mark(X1),X2)
p158: mark#(U91(X1,X2)) -> mark#(X1)
p159: mark#(U92(X)) -> a__U92#(mark(X))
p160: mark#(U92(X)) -> mark#(X)

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt(),V) -> a__U12(a__isPalListKind(V),V)
r5: a__U12(tt(),V) -> a__U13(a__isNeList(V))
r6: a__U13(tt()) -> tt()
r7: a__U21(tt(),V1,V2) -> a__U22(a__isPalListKind(V1),V1,V2)
r8: a__U22(tt(),V1,V2) -> a__U23(a__isPalListKind(V2),V1,V2)
r9: a__U23(tt(),V1,V2) -> a__U24(a__isPalListKind(V2),V1,V2)
r10: a__U24(tt(),V1,V2) -> a__U25(a__isList(V1),V2)
r11: a__U25(tt(),V2) -> a__U26(a__isList(V2))
r12: a__U26(tt()) -> tt()
r13: a__U31(tt(),V) -> a__U32(a__isPalListKind(V),V)
r14: a__U32(tt(),V) -> a__U33(a__isQid(V))
r15: a__U33(tt()) -> tt()
r16: a__U41(tt(),V1,V2) -> a__U42(a__isPalListKind(V1),V1,V2)
r17: a__U42(tt(),V1,V2) -> a__U43(a__isPalListKind(V2),V1,V2)
r18: a__U43(tt(),V1,V2) -> a__U44(a__isPalListKind(V2),V1,V2)
r19: a__U44(tt(),V1,V2) -> a__U45(a__isList(V1),V2)
r20: a__U45(tt(),V2) -> a__U46(a__isNeList(V2))
r21: a__U46(tt()) -> tt()
r22: a__U51(tt(),V1,V2) -> a__U52(a__isPalListKind(V1),V1,V2)
r23: a__U52(tt(),V1,V2) -> a__U53(a__isPalListKind(V2),V1,V2)
r24: a__U53(tt(),V1,V2) -> a__U54(a__isPalListKind(V2),V1,V2)
r25: a__U54(tt(),V1,V2) -> a__U55(a__isNeList(V1),V2)
r26: a__U55(tt(),V2) -> a__U56(a__isList(V2))
r27: a__U56(tt()) -> tt()
r28: a__U61(tt(),V) -> a__U62(a__isPalListKind(V),V)
r29: a__U62(tt(),V) -> a__U63(a__isQid(V))
r30: a__U63(tt()) -> tt()
r31: a__U71(tt(),I,P) -> a__U72(a__isPalListKind(I),P)
r32: a__U72(tt(),P) -> a__U73(a__isPal(P),P)
r33: a__U73(tt(),P) -> a__U74(a__isPalListKind(P))
r34: a__U74(tt()) -> tt()
r35: a__U81(tt(),V) -> a__U82(a__isPalListKind(V),V)
r36: a__U82(tt(),V) -> a__U83(a__isNePal(V))
r37: a__U83(tt()) -> tt()
r38: a__U91(tt(),V2) -> a__U92(a__isPalListKind(V2))
r39: a__U92(tt()) -> tt()
r40: a__isList(V) -> a__U11(a__isPalListKind(V),V)
r41: a__isList(nil()) -> tt()
r42: a__isList(__(V1,V2)) -> a__U21(a__isPalListKind(V1),V1,V2)
r43: a__isNeList(V) -> a__U31(a__isPalListKind(V),V)
r44: a__isNeList(__(V1,V2)) -> a__U41(a__isPalListKind(V1),V1,V2)
r45: a__isNeList(__(V1,V2)) -> a__U51(a__isPalListKind(V1),V1,V2)
r46: a__isNePal(V) -> a__U61(a__isPalListKind(V),V)
r47: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),I,P)
r48: a__isPal(V) -> a__U81(a__isPalListKind(V),V)
r49: a__isPal(nil()) -> tt()
r50: a__isPalListKind(a()) -> tt()
r51: a__isPalListKind(e()) -> tt()
r52: a__isPalListKind(i()) -> tt()
r53: a__isPalListKind(nil()) -> tt()
r54: a__isPalListKind(o()) -> tt()
r55: a__isPalListKind(u()) -> tt()
r56: a__isPalListKind(__(V1,V2)) -> a__U91(a__isPalListKind(V1),V2)
r57: a__isQid(a()) -> tt()
r58: a__isQid(e()) -> tt()
r59: a__isQid(i()) -> tt()
r60: a__isQid(o()) -> tt()
r61: a__isQid(u()) -> tt()
r62: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r63: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r64: mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
r65: mark(isPalListKind(X)) -> a__isPalListKind(X)
r66: mark(U13(X)) -> a__U13(mark(X))
r67: mark(isNeList(X)) -> a__isNeList(X)
r68: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
r69: mark(U22(X1,X2,X3)) -> a__U22(mark(X1),X2,X3)
r70: mark(U23(X1,X2,X3)) -> a__U23(mark(X1),X2,X3)
r71: mark(U24(X1,X2,X3)) -> a__U24(mark(X1),X2,X3)
r72: mark(U25(X1,X2)) -> a__U25(mark(X1),X2)
r73: mark(isList(X)) -> a__isList(X)
r74: mark(U26(X)) -> a__U26(mark(X))
r75: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r76: mark(U32(X1,X2)) -> a__U32(mark(X1),X2)
r77: mark(U33(X)) -> a__U33(mark(X))
r78: mark(isQid(X)) -> a__isQid(X)
r79: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r80: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r81: mark(U43(X1,X2,X3)) -> a__U43(mark(X1),X2,X3)
r82: mark(U44(X1,X2,X3)) -> a__U44(mark(X1),X2,X3)
r83: mark(U45(X1,X2)) -> a__U45(mark(X1),X2)
r84: mark(U46(X)) -> a__U46(mark(X))
r85: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
r86: mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
r87: mark(U53(X1,X2,X3)) -> a__U53(mark(X1),X2,X3)
r88: mark(U54(X1,X2,X3)) -> a__U54(mark(X1),X2,X3)
r89: mark(U55(X1,X2)) -> a__U55(mark(X1),X2)
r90: mark(U56(X)) -> a__U56(mark(X))
r91: mark(U61(X1,X2)) -> a__U61(mark(X1),X2)
r92: mark(U62(X1,X2)) -> a__U62(mark(X1),X2)
r93: mark(U63(X)) -> a__U63(mark(X))
r94: mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
r95: mark(U72(X1,X2)) -> a__U72(mark(X1),X2)
r96: mark(U73(X1,X2)) -> a__U73(mark(X1),X2)
r97: mark(isPal(X)) -> a__isPal(X)
r98: mark(U74(X)) -> a__U74(mark(X))
r99: mark(U81(X1,X2)) -> a__U81(mark(X1),X2)
r100: mark(U82(X1,X2)) -> a__U82(mark(X1),X2)
r101: mark(U83(X)) -> a__U83(mark(X))
r102: mark(isNePal(X)) -> a__isNePal(X)
r103: mark(U91(X1,X2)) -> a__U91(mark(X1),X2)
r104: mark(U92(X)) -> a__U92(mark(X))
r105: mark(nil()) -> nil()
r106: mark(tt()) -> tt()
r107: mark(a()) -> a()
r108: mark(e()) -> e()
r109: mark(i()) -> i()
r110: mark(o()) -> o()
r111: mark(u()) -> u()
r112: a____(X1,X2) -> __(X1,X2)
r113: a__U11(X1,X2) -> U11(X1,X2)
r114: a__U12(X1,X2) -> U12(X1,X2)
r115: a__isPalListKind(X) -> isPalListKind(X)
r116: a__U13(X) -> U13(X)
r117: a__isNeList(X) -> isNeList(X)
r118: a__U21(X1,X2,X3) -> U21(X1,X2,X3)
r119: a__U22(X1,X2,X3) -> U22(X1,X2,X3)
r120: a__U23(X1,X2,X3) -> U23(X1,X2,X3)
r121: a__U24(X1,X2,X3) -> U24(X1,X2,X3)
r122: a__U25(X1,X2) -> U25(X1,X2)
r123: a__isList(X) -> isList(X)
r124: a__U26(X) -> U26(X)
r125: a__U31(X1,X2) -> U31(X1,X2)
r126: a__U32(X1,X2) -> U32(X1,X2)
r127: a__U33(X) -> U33(X)
r128: a__isQid(X) -> isQid(X)
r129: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r130: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r131: a__U43(X1,X2,X3) -> U43(X1,X2,X3)
r132: a__U44(X1,X2,X3) -> U44(X1,X2,X3)
r133: a__U45(X1,X2) -> U45(X1,X2)
r134: a__U46(X) -> U46(X)
r135: a__U51(X1,X2,X3) -> U51(X1,X2,X3)
r136: a__U52(X1,X2,X3) -> U52(X1,X2,X3)
r137: a__U53(X1,X2,X3) -> U53(X1,X2,X3)
r138: a__U54(X1,X2,X3) -> U54(X1,X2,X3)
r139: a__U55(X1,X2) -> U55(X1,X2)
r140: a__U56(X) -> U56(X)
r141: a__U61(X1,X2) -> U61(X1,X2)
r142: a__U62(X1,X2) -> U62(X1,X2)
r143: a__U63(X) -> U63(X)
r144: a__U71(X1,X2,X3) -> U71(X1,X2,X3)
r145: a__U72(X1,X2) -> U72(X1,X2)
r146: a__U73(X1,X2) -> U73(X1,X2)
r147: a__isPal(X) -> isPal(X)
r148: a__U74(X) -> U74(X)
r149: a__U81(X1,X2) -> U81(X1,X2)
r150: a__U82(X1,X2) -> U82(X1,X2)
r151: a__U83(X) -> U83(X)
r152: a__isNePal(X) -> isNePal(X)
r153: a__U91(X1,X2) -> U91(X1,X2)
r154: a__U92(X) -> U92(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p80, p81, p82, p84, p86, p89, p92, p94, p96, p98, p100, p103, p105, p107, p109, p112, p114, p116, p118, p120, p122, p124, p126, p128, p130, p132, p134, p136, p138, p140, p142, p144, p146, p149, p151, p153, p155, p158, p160}
  {p8, p11, p12, p14, p16, p18, p19, p21, p26, p28, p30, p32, p33, p35, p36, p38, p40, p42, p43, p45, p62, p64, p68, p70}
  {p50, p53, p56, p59, p74, p76}
  {p61, p78, p79}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: a____#(__(X,Y),Z) -> a____#(mark(X),a____(mark(Y),mark(Z)))
p2: a____#(nil(),X) -> mark#(X)
p3: mark#(U92(X)) -> mark#(X)
p4: mark#(U91(X1,X2)) -> mark#(X1)
p5: mark#(U83(X)) -> mark#(X)
p6: mark#(U82(X1,X2)) -> mark#(X1)
p7: mark#(U81(X1,X2)) -> mark#(X1)
p8: mark#(U74(X)) -> mark#(X)
p9: mark#(U73(X1,X2)) -> mark#(X1)
p10: mark#(U72(X1,X2)) -> mark#(X1)
p11: mark#(U71(X1,X2,X3)) -> mark#(X1)
p12: mark#(U63(X)) -> mark#(X)
p13: mark#(U62(X1,X2)) -> mark#(X1)
p14: mark#(U61(X1,X2)) -> mark#(X1)
p15: mark#(U56(X)) -> mark#(X)
p16: mark#(U55(X1,X2)) -> mark#(X1)
p17: mark#(U54(X1,X2,X3)) -> mark#(X1)
p18: mark#(U53(X1,X2,X3)) -> mark#(X1)
p19: mark#(U52(X1,X2,X3)) -> mark#(X1)
p20: mark#(U51(X1,X2,X3)) -> mark#(X1)
p21: mark#(U46(X)) -> mark#(X)
p22: mark#(U45(X1,X2)) -> mark#(X1)
p23: mark#(U44(X1,X2,X3)) -> mark#(X1)
p24: mark#(U43(X1,X2,X3)) -> mark#(X1)
p25: mark#(U42(X1,X2,X3)) -> mark#(X1)
p26: mark#(U41(X1,X2,X3)) -> mark#(X1)
p27: mark#(U33(X)) -> mark#(X)
p28: mark#(U32(X1,X2)) -> mark#(X1)
p29: mark#(U31(X1,X2)) -> mark#(X1)
p30: mark#(U26(X)) -> mark#(X)
p31: mark#(U25(X1,X2)) -> mark#(X1)
p32: mark#(U24(X1,X2,X3)) -> mark#(X1)
p33: mark#(U23(X1,X2,X3)) -> mark#(X1)
p34: mark#(U22(X1,X2,X3)) -> mark#(X1)
p35: mark#(U21(X1,X2,X3)) -> mark#(X1)
p36: mark#(U13(X)) -> mark#(X)
p37: mark#(U12(X1,X2)) -> mark#(X1)
p38: mark#(U11(X1,X2)) -> mark#(X1)
p39: mark#(__(X1,X2)) -> mark#(X2)
p40: mark#(__(X1,X2)) -> mark#(X1)
p41: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p42: a____#(X,nil()) -> mark#(X)
p43: a____#(__(X,Y),Z) -> mark#(Z)
p44: a____#(__(X,Y),Z) -> mark#(Y)
p45: a____#(__(X,Y),Z) -> a____#(mark(Y),mark(Z))
p46: a____#(__(X,Y),Z) -> mark#(X)

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt(),V) -> a__U12(a__isPalListKind(V),V)
r5: a__U12(tt(),V) -> a__U13(a__isNeList(V))
r6: a__U13(tt()) -> tt()
r7: a__U21(tt(),V1,V2) -> a__U22(a__isPalListKind(V1),V1,V2)
r8: a__U22(tt(),V1,V2) -> a__U23(a__isPalListKind(V2),V1,V2)
r9: a__U23(tt(),V1,V2) -> a__U24(a__isPalListKind(V2),V1,V2)
r10: a__U24(tt(),V1,V2) -> a__U25(a__isList(V1),V2)
r11: a__U25(tt(),V2) -> a__U26(a__isList(V2))
r12: a__U26(tt()) -> tt()
r13: a__U31(tt(),V) -> a__U32(a__isPalListKind(V),V)
r14: a__U32(tt(),V) -> a__U33(a__isQid(V))
r15: a__U33(tt()) -> tt()
r16: a__U41(tt(),V1,V2) -> a__U42(a__isPalListKind(V1),V1,V2)
r17: a__U42(tt(),V1,V2) -> a__U43(a__isPalListKind(V2),V1,V2)
r18: a__U43(tt(),V1,V2) -> a__U44(a__isPalListKind(V2),V1,V2)
r19: a__U44(tt(),V1,V2) -> a__U45(a__isList(V1),V2)
r20: a__U45(tt(),V2) -> a__U46(a__isNeList(V2))
r21: a__U46(tt()) -> tt()
r22: a__U51(tt(),V1,V2) -> a__U52(a__isPalListKind(V1),V1,V2)
r23: a__U52(tt(),V1,V2) -> a__U53(a__isPalListKind(V2),V1,V2)
r24: a__U53(tt(),V1,V2) -> a__U54(a__isPalListKind(V2),V1,V2)
r25: a__U54(tt(),V1,V2) -> a__U55(a__isNeList(V1),V2)
r26: a__U55(tt(),V2) -> a__U56(a__isList(V2))
r27: a__U56(tt()) -> tt()
r28: a__U61(tt(),V) -> a__U62(a__isPalListKind(V),V)
r29: a__U62(tt(),V) -> a__U63(a__isQid(V))
r30: a__U63(tt()) -> tt()
r31: a__U71(tt(),I,P) -> a__U72(a__isPalListKind(I),P)
r32: a__U72(tt(),P) -> a__U73(a__isPal(P),P)
r33: a__U73(tt(),P) -> a__U74(a__isPalListKind(P))
r34: a__U74(tt()) -> tt()
r35: a__U81(tt(),V) -> a__U82(a__isPalListKind(V),V)
r36: a__U82(tt(),V) -> a__U83(a__isNePal(V))
r37: a__U83(tt()) -> tt()
r38: a__U91(tt(),V2) -> a__U92(a__isPalListKind(V2))
r39: a__U92(tt()) -> tt()
r40: a__isList(V) -> a__U11(a__isPalListKind(V),V)
r41: a__isList(nil()) -> tt()
r42: a__isList(__(V1,V2)) -> a__U21(a__isPalListKind(V1),V1,V2)
r43: a__isNeList(V) -> a__U31(a__isPalListKind(V),V)
r44: a__isNeList(__(V1,V2)) -> a__U41(a__isPalListKind(V1),V1,V2)
r45: a__isNeList(__(V1,V2)) -> a__U51(a__isPalListKind(V1),V1,V2)
r46: a__isNePal(V) -> a__U61(a__isPalListKind(V),V)
r47: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),I,P)
r48: a__isPal(V) -> a__U81(a__isPalListKind(V),V)
r49: a__isPal(nil()) -> tt()
r50: a__isPalListKind(a()) -> tt()
r51: a__isPalListKind(e()) -> tt()
r52: a__isPalListKind(i()) -> tt()
r53: a__isPalListKind(nil()) -> tt()
r54: a__isPalListKind(o()) -> tt()
r55: a__isPalListKind(u()) -> tt()
r56: a__isPalListKind(__(V1,V2)) -> a__U91(a__isPalListKind(V1),V2)
r57: a__isQid(a()) -> tt()
r58: a__isQid(e()) -> tt()
r59: a__isQid(i()) -> tt()
r60: a__isQid(o()) -> tt()
r61: a__isQid(u()) -> tt()
r62: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r63: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r64: mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
r65: mark(isPalListKind(X)) -> a__isPalListKind(X)
r66: mark(U13(X)) -> a__U13(mark(X))
r67: mark(isNeList(X)) -> a__isNeList(X)
r68: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
r69: mark(U22(X1,X2,X3)) -> a__U22(mark(X1),X2,X3)
r70: mark(U23(X1,X2,X3)) -> a__U23(mark(X1),X2,X3)
r71: mark(U24(X1,X2,X3)) -> a__U24(mark(X1),X2,X3)
r72: mark(U25(X1,X2)) -> a__U25(mark(X1),X2)
r73: mark(isList(X)) -> a__isList(X)
r74: mark(U26(X)) -> a__U26(mark(X))
r75: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r76: mark(U32(X1,X2)) -> a__U32(mark(X1),X2)
r77: mark(U33(X)) -> a__U33(mark(X))
r78: mark(isQid(X)) -> a__isQid(X)
r79: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r80: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r81: mark(U43(X1,X2,X3)) -> a__U43(mark(X1),X2,X3)
r82: mark(U44(X1,X2,X3)) -> a__U44(mark(X1),X2,X3)
r83: mark(U45(X1,X2)) -> a__U45(mark(X1),X2)
r84: mark(U46(X)) -> a__U46(mark(X))
r85: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
r86: mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
r87: mark(U53(X1,X2,X3)) -> a__U53(mark(X1),X2,X3)
r88: mark(U54(X1,X2,X3)) -> a__U54(mark(X1),X2,X3)
r89: mark(U55(X1,X2)) -> a__U55(mark(X1),X2)
r90: mark(U56(X)) -> a__U56(mark(X))
r91: mark(U61(X1,X2)) -> a__U61(mark(X1),X2)
r92: mark(U62(X1,X2)) -> a__U62(mark(X1),X2)
r93: mark(U63(X)) -> a__U63(mark(X))
r94: mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
r95: mark(U72(X1,X2)) -> a__U72(mark(X1),X2)
r96: mark(U73(X1,X2)) -> a__U73(mark(X1),X2)
r97: mark(isPal(X)) -> a__isPal(X)
r98: mark(U74(X)) -> a__U74(mark(X))
r99: mark(U81(X1,X2)) -> a__U81(mark(X1),X2)
r100: mark(U82(X1,X2)) -> a__U82(mark(X1),X2)
r101: mark(U83(X)) -> a__U83(mark(X))
r102: mark(isNePal(X)) -> a__isNePal(X)
r103: mark(U91(X1,X2)) -> a__U91(mark(X1),X2)
r104: mark(U92(X)) -> a__U92(mark(X))
r105: mark(nil()) -> nil()
r106: mark(tt()) -> tt()
r107: mark(a()) -> a()
r108: mark(e()) -> e()
r109: mark(i()) -> i()
r110: mark(o()) -> o()
r111: mark(u()) -> u()
r112: a____(X1,X2) -> __(X1,X2)
r113: a__U11(X1,X2) -> U11(X1,X2)
r114: a__U12(X1,X2) -> U12(X1,X2)
r115: a__isPalListKind(X) -> isPalListKind(X)
r116: a__U13(X) -> U13(X)
r117: a__isNeList(X) -> isNeList(X)
r118: a__U21(X1,X2,X3) -> U21(X1,X2,X3)
r119: a__U22(X1,X2,X3) -> U22(X1,X2,X3)
r120: a__U23(X1,X2,X3) -> U23(X1,X2,X3)
r121: a__U24(X1,X2,X3) -> U24(X1,X2,X3)
r122: a__U25(X1,X2) -> U25(X1,X2)
r123: a__isList(X) -> isList(X)
r124: a__U26(X) -> U26(X)
r125: a__U31(X1,X2) -> U31(X1,X2)
r126: a__U32(X1,X2) -> U32(X1,X2)
r127: a__U33(X) -> U33(X)
r128: a__isQid(X) -> isQid(X)
r129: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r130: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r131: a__U43(X1,X2,X3) -> U43(X1,X2,X3)
r132: a__U44(X1,X2,X3) -> U44(X1,X2,X3)
r133: a__U45(X1,X2) -> U45(X1,X2)
r134: a__U46(X) -> U46(X)
r135: a__U51(X1,X2,X3) -> U51(X1,X2,X3)
r136: a__U52(X1,X2,X3) -> U52(X1,X2,X3)
r137: a__U53(X1,X2,X3) -> U53(X1,X2,X3)
r138: a__U54(X1,X2,X3) -> U54(X1,X2,X3)
r139: a__U55(X1,X2) -> U55(X1,X2)
r140: a__U56(X) -> U56(X)
r141: a__U61(X1,X2) -> U61(X1,X2)
r142: a__U62(X1,X2) -> U62(X1,X2)
r143: a__U63(X) -> U63(X)
r144: a__U71(X1,X2,X3) -> U71(X1,X2,X3)
r145: a__U72(X1,X2) -> U72(X1,X2)
r146: a__U73(X1,X2) -> U73(X1,X2)
r147: a__isPal(X) -> isPal(X)
r148: a__U74(X) -> U74(X)
r149: a__U81(X1,X2) -> U81(X1,X2)
r150: a__U82(X1,X2) -> U82(X1,X2)
r151: a__U83(X) -> U83(X)
r152: a__isNePal(X) -> isNePal(X)
r153: a__U91(X1,X2) -> U91(X1,X2)
r154: a__U92(X) -> U92(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101, r102, r103, r104, r105, r106, r107, r108, r109, r110, r111, r112, r113, r114, r115, r116, r117, r118, r119, r120, r121, r122, r123, r124, r125, r126, r127, r128, r129, r130, r131, r132, r133, r134, r135, r136, r137, r138, r139, r140, r141, r142, r143, r144, r145, r146, r147, r148, r149, r150, r151, r152, r153, r154

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a____#_A(x1,x2) = x1 + x2 + 15
        ___A(x1,x2) = x1 + x2 + 16
        mark_A(x1) = x1
        a_____A(x1,x2) = x1 + x2 + 16
        nil_A() = 1
        mark#_A(x1) = x1
        U92_A(x1) = x1
        U91_A(x1,x2) = x1
        U83_A(x1) = x1 + 1
        U82_A(x1,x2) = x1 + x2 + 7
        U81_A(x1,x2) = x1 + x2 + 8
        U74_A(x1) = x1 + 1
        U73_A(x1,x2) = x1 + 2
        U72_A(x1,x2) = x1 + x2 + 12
        U71_A(x1,x2,x3) = x1 + x3 + 13
        U63_A(x1) = x1 + 1
        U62_A(x1,x2) = x1 + 3
        U61_A(x1,x2) = x1 + 4
        U56_A(x1) = x1 + 1
        U55_A(x1,x2) = x1 + x2 + 11
        U54_A(x1,x2,x3) = x1 + x2 + x3 + 17
        U53_A(x1,x2,x3) = x1 + x2 + x3 + 18
        U52_A(x1,x2,x3) = x1 + x2 + x3 + 19
        U51_A(x1,x2,x3) = x1 + x2 + x3 + 20
        U46_A(x1) = x1 + 1
        U45_A(x1,x2) = x1 + x2 + 7
        U44_A(x1,x2,x3) = x1 + x2 + x3 + 17
        U43_A(x1,x2,x3) = x1 + x2 + x3 + 18
        U42_A(x1,x2,x3) = x1 + x2 + x3 + 19
        U41_A(x1,x2,x3) = x1 + x2 + x3 + 20
        U33_A(x1) = x1 + 1
        U32_A(x1,x2) = x1 + x2 + 3
        U31_A(x1,x2) = x1 + x2 + 4
        U26_A(x1) = x1 + 1
        U25_A(x1,x2) = x1 + x2 + 11
        U24_A(x1,x2,x3) = x1 + x2 + x3 + 21
        U23_A(x1,x2,x3) = x1 + x2 + x3 + 22
        U22_A(x1,x2,x3) = x1 + x2 + x3 + 23
        U21_A(x1,x2,x3) = x1 + x2 + x3 + 24
        U13_A(x1) = x1 + 1
        U12_A(x1,x2) = x1 + x2 + 7
        U11_A(x1,x2) = x1 + x2 + 8
        a__U11_A(x1,x2) = x1 + x2 + 8
        tt_A() = 1
        a__U12_A(x1,x2) = x1 + x2 + 7
        a__isPalListKind_A(x1) = 1
        a__U13_A(x1) = x1 + 1
        a__isNeList_A(x1) = x1 + 6
        a__U21_A(x1,x2,x3) = x1 + x2 + x3 + 24
        a__U22_A(x1,x2,x3) = x1 + x2 + x3 + 23
        a__U23_A(x1,x2,x3) = x1 + x2 + x3 + 22
        a__U24_A(x1,x2,x3) = x1 + x2 + x3 + 21
        a__U25_A(x1,x2) = x1 + x2 + 11
        a__isList_A(x1) = x1 + 10
        a__U26_A(x1) = x1 + 1
        a__U31_A(x1,x2) = x1 + x2 + 4
        a__U32_A(x1,x2) = x1 + x2 + 3
        a__U33_A(x1) = x1 + 1
        a__isQid_A(x1) = 2
        a__U41_A(x1,x2,x3) = x1 + x2 + x3 + 20
        a__U42_A(x1,x2,x3) = x1 + x2 + x3 + 19
        a__U43_A(x1,x2,x3) = x1 + x2 + x3 + 18
        a__U44_A(x1,x2,x3) = x1 + x2 + x3 + 17
        a__U45_A(x1,x2) = x1 + x2 + 7
        a__U46_A(x1) = x1 + 1
        a__U51_A(x1,x2,x3) = x1 + x2 + x3 + 20
        a__U52_A(x1,x2,x3) = x1 + x2 + x3 + 19
        a__U53_A(x1,x2,x3) = x1 + x2 + x3 + 18
        a__U54_A(x1,x2,x3) = x1 + x2 + x3 + 17
        a__U55_A(x1,x2) = x1 + x2 + 11
        a__U56_A(x1) = x1 + 1
        a__U61_A(x1,x2) = x1 + 4
        a__U62_A(x1,x2) = x1 + 3
        a__U63_A(x1) = x1 + 1
        a__U71_A(x1,x2,x3) = x1 + x3 + 13
        a__U72_A(x1,x2) = x1 + x2 + 12
        a__U73_A(x1,x2) = x1 + 2
        a__isPal_A(x1) = x1 + 10
        a__U74_A(x1) = x1 + 1
        a__U81_A(x1,x2) = x1 + x2 + 8
        a__U82_A(x1,x2) = x1 + x2 + 7
        a__U83_A(x1) = x1 + 1
        a__isNePal_A(x1) = x1 + 6
        a__U91_A(x1,x2) = x1
        a__U92_A(x1) = x1
        a_A() = 1
        e_A() = 1
        i_A() = 1
        o_A() = 1
        u_A() = 1
        isPalListKind_A(x1) = 1
        isNeList_A(x1) = x1 + 6
        isList_A(x1) = x1 + 10
        isQid_A(x1) = 2
        isPal_A(x1) = x1 + 10
        isNePal_A(x1) = x1 + 6
    
    2. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a____#_A(x1,x2) = x1 + 1
        ___A(x1,x2) = 14
        mark_A(x1) = 14
        a_____A(x1,x2) = 14
        nil_A() = 13
        mark#_A(x1) = 0
        U92_A(x1) = 1
        U91_A(x1,x2) = 1
        U83_A(x1) = 1
        U82_A(x1,x2) = 1
        U81_A(x1,x2) = 13
        U74_A(x1) = 1
        U73_A(x1,x2) = 11
        U72_A(x1,x2) = 1
        U71_A(x1,x2,x3) = 1
        U63_A(x1) = 1
        U62_A(x1,x2) = 1
        U61_A(x1,x2) = 3
        U56_A(x1) = 0
        U55_A(x1,x2) = 7
        U54_A(x1,x2,x3) = 1
        U53_A(x1,x2,x3) = 1
        U52_A(x1,x2,x3) = 1
        U51_A(x1,x2,x3) = 1
        U46_A(x1) = 1
        U45_A(x1,x2) = 2
        U44_A(x1,x2,x3) = 1
        U43_A(x1,x2,x3) = 1
        U42_A(x1,x2,x3) = 12
        U41_A(x1,x2,x3) = 1
        U33_A(x1) = 1
        U32_A(x1,x2) = 1
        U31_A(x1,x2) = 1
        U26_A(x1) = 1
        U25_A(x1,x2) = 0
        U24_A(x1,x2,x3) = 1
        U23_A(x1,x2,x3) = 12
        U22_A(x1,x2,x3) = 1
        U21_A(x1,x2,x3) = 1
        U13_A(x1) = 1
        U12_A(x1,x2) = 1
        U11_A(x1,x2) = 1
        a__U11_A(x1,x2) = 2
        tt_A() = 5
        a__U12_A(x1,x2) = 13
        a__isPalListKind_A(x1) = 7
        a__U13_A(x1) = 12
        a__isNeList_A(x1) = 12
        a__U21_A(x1,x2,x3) = 3
        a__U22_A(x1,x2,x3) = 2
        a__U23_A(x1,x2,x3) = 13
        a__U24_A(x1,x2,x3) = 2
        a__U25_A(x1,x2) = x1
        a__isList_A(x1) = 0
        a__U26_A(x1) = 2
        a__U31_A(x1,x2) = 11
        a__U32_A(x1,x2) = 13
        a__U33_A(x1) = 14
        a__isQid_A(x1) = 6
        a__U41_A(x1,x2,x3) = 13
        a__U42_A(x1,x2,x3) = 12
        a__U43_A(x1,x2,x3) = 11
        a__U44_A(x1,x2,x3) = 2
        a__U45_A(x1,x2) = 2
        a__U46_A(x1) = 3
        a__U51_A(x1,x2,x3) = 11
        a__U52_A(x1,x2,x3) = 10
        a__U53_A(x1,x2,x3) = 9
        a__U54_A(x1,x2,x3) = 8
        a__U55_A(x1,x2) = 7
        a__U56_A(x1) = 6
        a__U61_A(x1,x2) = 3
        a__U62_A(x1,x2) = 3
        a__U63_A(x1) = 4
        a__U71_A(x1,x2,x3) = 13
        a__U72_A(x1,x2) = 12
        a__U73_A(x1,x2) = 11
        a__isPal_A(x1) = 2
        a__U74_A(x1) = 10
        a__U81_A(x1,x2) = 13
        a__U82_A(x1,x2) = 13
        a__U83_A(x1) = 6
        a__isNePal_A(x1) = 2
        a__U91_A(x1,x2) = 6
        a__U92_A(x1) = 5
        a_A() = 1
        e_A() = 1
        i_A() = 14
        o_A() = 14
        u_A() = 1
        isPalListKind_A(x1) = 6
        isNeList_A(x1) = 1
        isList_A(x1) = 0
        isQid_A(x1) = 6
        isPal_A(x1) = 1
        isNePal_A(x1) = 1
    

The next rules are strictly ordered:

  p2, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, p29, p30, p31, p32, p33, p34, p35, p36, p37, p38, p39, p40, p41, p42, p43, p44, p45, p46

We remove them from the problem.

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: a____#(__(X,Y),Z) -> a____#(mark(X),a____(mark(Y),mark(Z)))
p2: mark#(U92(X)) -> mark#(X)
p3: mark#(U91(X1,X2)) -> mark#(X1)

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt(),V) -> a__U12(a__isPalListKind(V),V)
r5: a__U12(tt(),V) -> a__U13(a__isNeList(V))
r6: a__U13(tt()) -> tt()
r7: a__U21(tt(),V1,V2) -> a__U22(a__isPalListKind(V1),V1,V2)
r8: a__U22(tt(),V1,V2) -> a__U23(a__isPalListKind(V2),V1,V2)
r9: a__U23(tt(),V1,V2) -> a__U24(a__isPalListKind(V2),V1,V2)
r10: a__U24(tt(),V1,V2) -> a__U25(a__isList(V1),V2)
r11: a__U25(tt(),V2) -> a__U26(a__isList(V2))
r12: a__U26(tt()) -> tt()
r13: a__U31(tt(),V) -> a__U32(a__isPalListKind(V),V)
r14: a__U32(tt(),V) -> a__U33(a__isQid(V))
r15: a__U33(tt()) -> tt()
r16: a__U41(tt(),V1,V2) -> a__U42(a__isPalListKind(V1),V1,V2)
r17: a__U42(tt(),V1,V2) -> a__U43(a__isPalListKind(V2),V1,V2)
r18: a__U43(tt(),V1,V2) -> a__U44(a__isPalListKind(V2),V1,V2)
r19: a__U44(tt(),V1,V2) -> a__U45(a__isList(V1),V2)
r20: a__U45(tt(),V2) -> a__U46(a__isNeList(V2))
r21: a__U46(tt()) -> tt()
r22: a__U51(tt(),V1,V2) -> a__U52(a__isPalListKind(V1),V1,V2)
r23: a__U52(tt(),V1,V2) -> a__U53(a__isPalListKind(V2),V1,V2)
r24: a__U53(tt(),V1,V2) -> a__U54(a__isPalListKind(V2),V1,V2)
r25: a__U54(tt(),V1,V2) -> a__U55(a__isNeList(V1),V2)
r26: a__U55(tt(),V2) -> a__U56(a__isList(V2))
r27: a__U56(tt()) -> tt()
r28: a__U61(tt(),V) -> a__U62(a__isPalListKind(V),V)
r29: a__U62(tt(),V) -> a__U63(a__isQid(V))
r30: a__U63(tt()) -> tt()
r31: a__U71(tt(),I,P) -> a__U72(a__isPalListKind(I),P)
r32: a__U72(tt(),P) -> a__U73(a__isPal(P),P)
r33: a__U73(tt(),P) -> a__U74(a__isPalListKind(P))
r34: a__U74(tt()) -> tt()
r35: a__U81(tt(),V) -> a__U82(a__isPalListKind(V),V)
r36: a__U82(tt(),V) -> a__U83(a__isNePal(V))
r37: a__U83(tt()) -> tt()
r38: a__U91(tt(),V2) -> a__U92(a__isPalListKind(V2))
r39: a__U92(tt()) -> tt()
r40: a__isList(V) -> a__U11(a__isPalListKind(V),V)
r41: a__isList(nil()) -> tt()
r42: a__isList(__(V1,V2)) -> a__U21(a__isPalListKind(V1),V1,V2)
r43: a__isNeList(V) -> a__U31(a__isPalListKind(V),V)
r44: a__isNeList(__(V1,V2)) -> a__U41(a__isPalListKind(V1),V1,V2)
r45: a__isNeList(__(V1,V2)) -> a__U51(a__isPalListKind(V1),V1,V2)
r46: a__isNePal(V) -> a__U61(a__isPalListKind(V),V)
r47: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),I,P)
r48: a__isPal(V) -> a__U81(a__isPalListKind(V),V)
r49: a__isPal(nil()) -> tt()
r50: a__isPalListKind(a()) -> tt()
r51: a__isPalListKind(e()) -> tt()
r52: a__isPalListKind(i()) -> tt()
r53: a__isPalListKind(nil()) -> tt()
r54: a__isPalListKind(o()) -> tt()
r55: a__isPalListKind(u()) -> tt()
r56: a__isPalListKind(__(V1,V2)) -> a__U91(a__isPalListKind(V1),V2)
r57: a__isQid(a()) -> tt()
r58: a__isQid(e()) -> tt()
r59: a__isQid(i()) -> tt()
r60: a__isQid(o()) -> tt()
r61: a__isQid(u()) -> tt()
r62: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r63: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r64: mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
r65: mark(isPalListKind(X)) -> a__isPalListKind(X)
r66: mark(U13(X)) -> a__U13(mark(X))
r67: mark(isNeList(X)) -> a__isNeList(X)
r68: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
r69: mark(U22(X1,X2,X3)) -> a__U22(mark(X1),X2,X3)
r70: mark(U23(X1,X2,X3)) -> a__U23(mark(X1),X2,X3)
r71: mark(U24(X1,X2,X3)) -> a__U24(mark(X1),X2,X3)
r72: mark(U25(X1,X2)) -> a__U25(mark(X1),X2)
r73: mark(isList(X)) -> a__isList(X)
r74: mark(U26(X)) -> a__U26(mark(X))
r75: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r76: mark(U32(X1,X2)) -> a__U32(mark(X1),X2)
r77: mark(U33(X)) -> a__U33(mark(X))
r78: mark(isQid(X)) -> a__isQid(X)
r79: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r80: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r81: mark(U43(X1,X2,X3)) -> a__U43(mark(X1),X2,X3)
r82: mark(U44(X1,X2,X3)) -> a__U44(mark(X1),X2,X3)
r83: mark(U45(X1,X2)) -> a__U45(mark(X1),X2)
r84: mark(U46(X)) -> a__U46(mark(X))
r85: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
r86: mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
r87: mark(U53(X1,X2,X3)) -> a__U53(mark(X1),X2,X3)
r88: mark(U54(X1,X2,X3)) -> a__U54(mark(X1),X2,X3)
r89: mark(U55(X1,X2)) -> a__U55(mark(X1),X2)
r90: mark(U56(X)) -> a__U56(mark(X))
r91: mark(U61(X1,X2)) -> a__U61(mark(X1),X2)
r92: mark(U62(X1,X2)) -> a__U62(mark(X1),X2)
r93: mark(U63(X)) -> a__U63(mark(X))
r94: mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
r95: mark(U72(X1,X2)) -> a__U72(mark(X1),X2)
r96: mark(U73(X1,X2)) -> a__U73(mark(X1),X2)
r97: mark(isPal(X)) -> a__isPal(X)
r98: mark(U74(X)) -> a__U74(mark(X))
r99: mark(U81(X1,X2)) -> a__U81(mark(X1),X2)
r100: mark(U82(X1,X2)) -> a__U82(mark(X1),X2)
r101: mark(U83(X)) -> a__U83(mark(X))
r102: mark(isNePal(X)) -> a__isNePal(X)
r103: mark(U91(X1,X2)) -> a__U91(mark(X1),X2)
r104: mark(U92(X)) -> a__U92(mark(X))
r105: mark(nil()) -> nil()
r106: mark(tt()) -> tt()
r107: mark(a()) -> a()
r108: mark(e()) -> e()
r109: mark(i()) -> i()
r110: mark(o()) -> o()
r111: mark(u()) -> u()
r112: a____(X1,X2) -> __(X1,X2)
r113: a__U11(X1,X2) -> U11(X1,X2)
r114: a__U12(X1,X2) -> U12(X1,X2)
r115: a__isPalListKind(X) -> isPalListKind(X)
r116: a__U13(X) -> U13(X)
r117: a__isNeList(X) -> isNeList(X)
r118: a__U21(X1,X2,X3) -> U21(X1,X2,X3)
r119: a__U22(X1,X2,X3) -> U22(X1,X2,X3)
r120: a__U23(X1,X2,X3) -> U23(X1,X2,X3)
r121: a__U24(X1,X2,X3) -> U24(X1,X2,X3)
r122: a__U25(X1,X2) -> U25(X1,X2)
r123: a__isList(X) -> isList(X)
r124: a__U26(X) -> U26(X)
r125: a__U31(X1,X2) -> U31(X1,X2)
r126: a__U32(X1,X2) -> U32(X1,X2)
r127: a__U33(X) -> U33(X)
r128: a__isQid(X) -> isQid(X)
r129: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r130: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r131: a__U43(X1,X2,X3) -> U43(X1,X2,X3)
r132: a__U44(X1,X2,X3) -> U44(X1,X2,X3)
r133: a__U45(X1,X2) -> U45(X1,X2)
r134: a__U46(X) -> U46(X)
r135: a__U51(X1,X2,X3) -> U51(X1,X2,X3)
r136: a__U52(X1,X2,X3) -> U52(X1,X2,X3)
r137: a__U53(X1,X2,X3) -> U53(X1,X2,X3)
r138: a__U54(X1,X2,X3) -> U54(X1,X2,X3)
r139: a__U55(X1,X2) -> U55(X1,X2)
r140: a__U56(X) -> U56(X)
r141: a__U61(X1,X2) -> U61(X1,X2)
r142: a__U62(X1,X2) -> U62(X1,X2)
r143: a__U63(X) -> U63(X)
r144: a__U71(X1,X2,X3) -> U71(X1,X2,X3)
r145: a__U72(X1,X2) -> U72(X1,X2)
r146: a__U73(X1,X2) -> U73(X1,X2)
r147: a__isPal(X) -> isPal(X)
r148: a__U74(X) -> U74(X)
r149: a__U81(X1,X2) -> U81(X1,X2)
r150: a__U82(X1,X2) -> U82(X1,X2)
r151: a__U83(X) -> U83(X)
r152: a__isNePal(X) -> isNePal(X)
r153: a__U91(X1,X2) -> U91(X1,X2)
r154: a__U92(X) -> U92(X)

The estimated dependency graph contains the following SCCs:

  {p1}
  {p2, p3}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: a____#(__(X,Y),Z) -> a____#(mark(X),a____(mark(Y),mark(Z)))

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt(),V) -> a__U12(a__isPalListKind(V),V)
r5: a__U12(tt(),V) -> a__U13(a__isNeList(V))
r6: a__U13(tt()) -> tt()
r7: a__U21(tt(),V1,V2) -> a__U22(a__isPalListKind(V1),V1,V2)
r8: a__U22(tt(),V1,V2) -> a__U23(a__isPalListKind(V2),V1,V2)
r9: a__U23(tt(),V1,V2) -> a__U24(a__isPalListKind(V2),V1,V2)
r10: a__U24(tt(),V1,V2) -> a__U25(a__isList(V1),V2)
r11: a__U25(tt(),V2) -> a__U26(a__isList(V2))
r12: a__U26(tt()) -> tt()
r13: a__U31(tt(),V) -> a__U32(a__isPalListKind(V),V)
r14: a__U32(tt(),V) -> a__U33(a__isQid(V))
r15: a__U33(tt()) -> tt()
r16: a__U41(tt(),V1,V2) -> a__U42(a__isPalListKind(V1),V1,V2)
r17: a__U42(tt(),V1,V2) -> a__U43(a__isPalListKind(V2),V1,V2)
r18: a__U43(tt(),V1,V2) -> a__U44(a__isPalListKind(V2),V1,V2)
r19: a__U44(tt(),V1,V2) -> a__U45(a__isList(V1),V2)
r20: a__U45(tt(),V2) -> a__U46(a__isNeList(V2))
r21: a__U46(tt()) -> tt()
r22: a__U51(tt(),V1,V2) -> a__U52(a__isPalListKind(V1),V1,V2)
r23: a__U52(tt(),V1,V2) -> a__U53(a__isPalListKind(V2),V1,V2)
r24: a__U53(tt(),V1,V2) -> a__U54(a__isPalListKind(V2),V1,V2)
r25: a__U54(tt(),V1,V2) -> a__U55(a__isNeList(V1),V2)
r26: a__U55(tt(),V2) -> a__U56(a__isList(V2))
r27: a__U56(tt()) -> tt()
r28: a__U61(tt(),V) -> a__U62(a__isPalListKind(V),V)
r29: a__U62(tt(),V) -> a__U63(a__isQid(V))
r30: a__U63(tt()) -> tt()
r31: a__U71(tt(),I,P) -> a__U72(a__isPalListKind(I),P)
r32: a__U72(tt(),P) -> a__U73(a__isPal(P),P)
r33: a__U73(tt(),P) -> a__U74(a__isPalListKind(P))
r34: a__U74(tt()) -> tt()
r35: a__U81(tt(),V) -> a__U82(a__isPalListKind(V),V)
r36: a__U82(tt(),V) -> a__U83(a__isNePal(V))
r37: a__U83(tt()) -> tt()
r38: a__U91(tt(),V2) -> a__U92(a__isPalListKind(V2))
r39: a__U92(tt()) -> tt()
r40: a__isList(V) -> a__U11(a__isPalListKind(V),V)
r41: a__isList(nil()) -> tt()
r42: a__isList(__(V1,V2)) -> a__U21(a__isPalListKind(V1),V1,V2)
r43: a__isNeList(V) -> a__U31(a__isPalListKind(V),V)
r44: a__isNeList(__(V1,V2)) -> a__U41(a__isPalListKind(V1),V1,V2)
r45: a__isNeList(__(V1,V2)) -> a__U51(a__isPalListKind(V1),V1,V2)
r46: a__isNePal(V) -> a__U61(a__isPalListKind(V),V)
r47: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),I,P)
r48: a__isPal(V) -> a__U81(a__isPalListKind(V),V)
r49: a__isPal(nil()) -> tt()
r50: a__isPalListKind(a()) -> tt()
r51: a__isPalListKind(e()) -> tt()
r52: a__isPalListKind(i()) -> tt()
r53: a__isPalListKind(nil()) -> tt()
r54: a__isPalListKind(o()) -> tt()
r55: a__isPalListKind(u()) -> tt()
r56: a__isPalListKind(__(V1,V2)) -> a__U91(a__isPalListKind(V1),V2)
r57: a__isQid(a()) -> tt()
r58: a__isQid(e()) -> tt()
r59: a__isQid(i()) -> tt()
r60: a__isQid(o()) -> tt()
r61: a__isQid(u()) -> tt()
r62: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r63: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r64: mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
r65: mark(isPalListKind(X)) -> a__isPalListKind(X)
r66: mark(U13(X)) -> a__U13(mark(X))
r67: mark(isNeList(X)) -> a__isNeList(X)
r68: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
r69: mark(U22(X1,X2,X3)) -> a__U22(mark(X1),X2,X3)
r70: mark(U23(X1,X2,X3)) -> a__U23(mark(X1),X2,X3)
r71: mark(U24(X1,X2,X3)) -> a__U24(mark(X1),X2,X3)
r72: mark(U25(X1,X2)) -> a__U25(mark(X1),X2)
r73: mark(isList(X)) -> a__isList(X)
r74: mark(U26(X)) -> a__U26(mark(X))
r75: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r76: mark(U32(X1,X2)) -> a__U32(mark(X1),X2)
r77: mark(U33(X)) -> a__U33(mark(X))
r78: mark(isQid(X)) -> a__isQid(X)
r79: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r80: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r81: mark(U43(X1,X2,X3)) -> a__U43(mark(X1),X2,X3)
r82: mark(U44(X1,X2,X3)) -> a__U44(mark(X1),X2,X3)
r83: mark(U45(X1,X2)) -> a__U45(mark(X1),X2)
r84: mark(U46(X)) -> a__U46(mark(X))
r85: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
r86: mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
r87: mark(U53(X1,X2,X3)) -> a__U53(mark(X1),X2,X3)
r88: mark(U54(X1,X2,X3)) -> a__U54(mark(X1),X2,X3)
r89: mark(U55(X1,X2)) -> a__U55(mark(X1),X2)
r90: mark(U56(X)) -> a__U56(mark(X))
r91: mark(U61(X1,X2)) -> a__U61(mark(X1),X2)
r92: mark(U62(X1,X2)) -> a__U62(mark(X1),X2)
r93: mark(U63(X)) -> a__U63(mark(X))
r94: mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
r95: mark(U72(X1,X2)) -> a__U72(mark(X1),X2)
r96: mark(U73(X1,X2)) -> a__U73(mark(X1),X2)
r97: mark(isPal(X)) -> a__isPal(X)
r98: mark(U74(X)) -> a__U74(mark(X))
r99: mark(U81(X1,X2)) -> a__U81(mark(X1),X2)
r100: mark(U82(X1,X2)) -> a__U82(mark(X1),X2)
r101: mark(U83(X)) -> a__U83(mark(X))
r102: mark(isNePal(X)) -> a__isNePal(X)
r103: mark(U91(X1,X2)) -> a__U91(mark(X1),X2)
r104: mark(U92(X)) -> a__U92(mark(X))
r105: mark(nil()) -> nil()
r106: mark(tt()) -> tt()
r107: mark(a()) -> a()
r108: mark(e()) -> e()
r109: mark(i()) -> i()
r110: mark(o()) -> o()
r111: mark(u()) -> u()
r112: a____(X1,X2) -> __(X1,X2)
r113: a__U11(X1,X2) -> U11(X1,X2)
r114: a__U12(X1,X2) -> U12(X1,X2)
r115: a__isPalListKind(X) -> isPalListKind(X)
r116: a__U13(X) -> U13(X)
r117: a__isNeList(X) -> isNeList(X)
r118: a__U21(X1,X2,X3) -> U21(X1,X2,X3)
r119: a__U22(X1,X2,X3) -> U22(X1,X2,X3)
r120: a__U23(X1,X2,X3) -> U23(X1,X2,X3)
r121: a__U24(X1,X2,X3) -> U24(X1,X2,X3)
r122: a__U25(X1,X2) -> U25(X1,X2)
r123: a__isList(X) -> isList(X)
r124: a__U26(X) -> U26(X)
r125: a__U31(X1,X2) -> U31(X1,X2)
r126: a__U32(X1,X2) -> U32(X1,X2)
r127: a__U33(X) -> U33(X)
r128: a__isQid(X) -> isQid(X)
r129: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r130: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r131: a__U43(X1,X2,X3) -> U43(X1,X2,X3)
r132: a__U44(X1,X2,X3) -> U44(X1,X2,X3)
r133: a__U45(X1,X2) -> U45(X1,X2)
r134: a__U46(X) -> U46(X)
r135: a__U51(X1,X2,X3) -> U51(X1,X2,X3)
r136: a__U52(X1,X2,X3) -> U52(X1,X2,X3)
r137: a__U53(X1,X2,X3) -> U53(X1,X2,X3)
r138: a__U54(X1,X2,X3) -> U54(X1,X2,X3)
r139: a__U55(X1,X2) -> U55(X1,X2)
r140: a__U56(X) -> U56(X)
r141: a__U61(X1,X2) -> U61(X1,X2)
r142: a__U62(X1,X2) -> U62(X1,X2)
r143: a__U63(X) -> U63(X)
r144: a__U71(X1,X2,X3) -> U71(X1,X2,X3)
r145: a__U72(X1,X2) -> U72(X1,X2)
r146: a__U73(X1,X2) -> U73(X1,X2)
r147: a__isPal(X) -> isPal(X)
r148: a__U74(X) -> U74(X)
r149: a__U81(X1,X2) -> U81(X1,X2)
r150: a__U82(X1,X2) -> U82(X1,X2)
r151: a__U83(X) -> U83(X)
r152: a__isNePal(X) -> isNePal(X)
r153: a__U91(X1,X2) -> U91(X1,X2)
r154: a__U92(X) -> U92(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101, r102, r103, r104, r105, r106, r107, r108, r109, r110, r111, r112, r113, r114, r115, r116, r117, r118, r119, r120, r121, r122, r123, r124, r125, r126, r127, r128, r129, r130, r131, r132, r133, r134, r135, r136, r137, r138, r139, r140, r141, r142, r143, r144, r145, r146, r147, r148, r149, r150, r151, r152, r153, r154

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a____#_A(x1,x2) = x1
        ___A(x1,x2) = x1 + x2 + 7
        mark_A(x1) = x1
        a_____A(x1,x2) = x1 + x2 + 7
        a__U11_A(x1,x2) = x2 + 5
        tt_A() = 0
        a__U12_A(x1,x2) = x2 + 5
        a__isPalListKind_A(x1) = 1
        a__U13_A(x1) = x1 + 1
        a__isNeList_A(x1) = x1 + 3
        a__U21_A(x1,x2,x3) = x2 + x3 + 13
        a__U22_A(x1,x2,x3) = x1 + x3 + 6
        a__U23_A(x1,x2,x3) = x1 + 4
        a__U24_A(x1,x2,x3) = 3
        a__U25_A(x1,x2) = 2
        a__isList_A(x1) = x1 + 6
        a__U26_A(x1) = 1
        a__U31_A(x1,x2) = x2 + 2
        a__U32_A(x1,x2) = x1 + x2 + 1
        a__U33_A(x1) = 1
        a__isQid_A(x1) = 13
        a__U41_A(x1,x2,x3) = x2 + x3 + 9
        a__U42_A(x1,x2,x3) = x2 + x3 + 8
        a__U43_A(x1,x2,x3) = x2 + x3 + 7
        a__U44_A(x1,x2,x3) = x2 + x3 + 6
        a__U45_A(x1,x2) = x2 + 5
        a__U46_A(x1) = x1 + 1
        a__U51_A(x1,x2,x3) = x3 + 10
        a__U52_A(x1,x2,x3) = x3 + 6
        a__U53_A(x1,x2,x3) = x3 + 5
        a__U54_A(x1,x2,x3) = x1 + 3
        a__U55_A(x1,x2) = 2
        a__U56_A(x1) = 1
        a__U61_A(x1,x2) = 0
        a__U62_A(x1,x2) = 0
        a__U63_A(x1) = 0
        a__U71_A(x1,x2,x3) = x1 + x2 + 1
        a__U72_A(x1,x2) = 1
        a__U73_A(x1,x2) = 1
        a__isPal_A(x1) = x1 + 3
        a__U74_A(x1) = 1
        a__U81_A(x1,x2) = x2 + 2
        a__U82_A(x1,x2) = x2 + 1
        a__U83_A(x1) = 1
        a__isNePal_A(x1) = x1
        a__U91_A(x1,x2) = x1
        a__U92_A(x1) = 0
        nil_A() = 1
        a_A() = 1
        e_A() = 1
        i_A() = 1
        o_A() = 1
        u_A() = 1
        U11_A(x1,x2) = x2 + 5
        U12_A(x1,x2) = x2 + 5
        isPalListKind_A(x1) = 1
        U13_A(x1) = x1 + 1
        isNeList_A(x1) = x1 + 3
        U21_A(x1,x2,x3) = x2 + x3 + 13
        U22_A(x1,x2,x3) = x1 + x3 + 6
        U23_A(x1,x2,x3) = x1 + 4
        U24_A(x1,x2,x3) = 3
        U25_A(x1,x2) = 2
        isList_A(x1) = x1 + 6
        U26_A(x1) = 1
        U31_A(x1,x2) = x2 + 2
        U32_A(x1,x2) = x1 + x2 + 1
        U33_A(x1) = 1
        isQid_A(x1) = 13
        U41_A(x1,x2,x3) = x2 + x3 + 9
        U42_A(x1,x2,x3) = x2 + x3 + 8
        U43_A(x1,x2,x3) = x2 + x3 + 7
        U44_A(x1,x2,x3) = x2 + x3 + 6
        U45_A(x1,x2) = x2 + 5
        U46_A(x1) = x1 + 1
        U51_A(x1,x2,x3) = x3 + 10
        U52_A(x1,x2,x3) = x3 + 6
        U53_A(x1,x2,x3) = x3 + 5
        U54_A(x1,x2,x3) = x1 + 3
        U55_A(x1,x2) = 2
        U56_A(x1) = 1
        U61_A(x1,x2) = 0
        U62_A(x1,x2) = 0
        U63_A(x1) = 0
        U71_A(x1,x2,x3) = x1 + x2 + 1
        U72_A(x1,x2) = 1
        U73_A(x1,x2) = 1
        isPal_A(x1) = x1 + 3
        U74_A(x1) = 1
        U81_A(x1,x2) = x2 + 2
        U82_A(x1,x2) = x2 + 1
        U83_A(x1) = 1
        isNePal_A(x1) = x1
        U91_A(x1,x2) = x1
        U92_A(x1) = 0
    
    2. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a____#_A(x1,x2) = 0
        ___A(x1,x2) = 2
        mark_A(x1) = x1 + 2
        a_____A(x1,x2) = 3
        a__U11_A(x1,x2) = 3
        tt_A() = 8
        a__U12_A(x1,x2) = 2
        a__isPalListKind_A(x1) = 11
        a__U13_A(x1) = 3
        a__isNeList_A(x1) = x1 + 12
        a__U21_A(x1,x2,x3) = 2
        a__U22_A(x1,x2,x3) = x3 + 3
        a__U23_A(x1,x2,x3) = 4
        a__U24_A(x1,x2,x3) = 5
        a__U25_A(x1,x2) = 6
        a__isList_A(x1) = x1 + 4
        a__U26_A(x1) = 7
        a__U31_A(x1,x2) = x2 + 11
        a__U32_A(x1,x2) = 10
        a__U33_A(x1) = 9
        a__isQid_A(x1) = 7
        a__U41_A(x1,x2,x3) = x2 + 2
        a__U42_A(x1,x2,x3) = 3
        a__U43_A(x1,x2,x3) = x2 + 4
        a__U44_A(x1,x2,x3) = 5
        a__U45_A(x1,x2) = 6
        a__U46_A(x1) = 9
        a__U51_A(x1,x2,x3) = 2
        a__U52_A(x1,x2,x3) = 3
        a__U53_A(x1,x2,x3) = 4
        a__U54_A(x1,x2,x3) = 5
        a__U55_A(x1,x2) = 6
        a__U56_A(x1) = 7
        a__U61_A(x1,x2) = 11
        a__U62_A(x1,x2) = 10
        a__U63_A(x1) = 9
        a__U71_A(x1,x2,x3) = 9
        a__U72_A(x1,x2) = 9
        a__U73_A(x1,x2) = 9
        a__isPal_A(x1) = 9
        a__U74_A(x1) = 8
        a__U81_A(x1,x2) = 10
        a__U82_A(x1,x2) = 9
        a__U83_A(x1) = 8
        a__isNePal_A(x1) = 12
        a__U91_A(x1,x2) = 10
        a__U92_A(x1) = 9
        nil_A() = 5
        a_A() = 1
        e_A() = 1
        i_A() = 1
        o_A() = 1
        u_A() = 1
        U11_A(x1,x2) = 1
        U12_A(x1,x2) = 1
        isPalListKind_A(x1) = 10
        U13_A(x1) = 2
        isNeList_A(x1) = x1 + 11
        U21_A(x1,x2,x3) = 1
        U22_A(x1,x2,x3) = x3 + 2
        U23_A(x1,x2,x3) = 2
        U24_A(x1,x2,x3) = 4
        U25_A(x1,x2) = 4
        isList_A(x1) = x1 + 3
        U26_A(x1) = 5
        U31_A(x1,x2) = x2 + 10
        U32_A(x1,x2) = 9
        U33_A(x1) = 7
        isQid_A(x1) = 6
        U41_A(x1,x2,x3) = x2 + 1
        U42_A(x1,x2,x3) = 2
        U43_A(x1,x2,x3) = x2 + 2
        U44_A(x1,x2,x3) = 4
        U45_A(x1,x2) = 5
        U46_A(x1) = 8
        U51_A(x1,x2,x3) = 1
        U52_A(x1,x2,x3) = 2
        U53_A(x1,x2,x3) = 3
        U54_A(x1,x2,x3) = 3
        U55_A(x1,x2) = 5
        U56_A(x1) = 6
        U61_A(x1,x2) = 10
        U62_A(x1,x2) = 8
        U63_A(x1) = 8
        U71_A(x1,x2,x3) = 9
        U72_A(x1,x2) = 8
        U73_A(x1,x2) = 8
        isPal_A(x1) = 8
        U74_A(x1) = 7
        U81_A(x1,x2) = 9
        U82_A(x1,x2) = 8
        U83_A(x1) = 7
        isNePal_A(x1) = 11
        U91_A(x1,x2) = 9
        U92_A(x1) = 8
    

The next rules are strictly ordered:

  p1

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: mark#(U92(X)) -> mark#(X)
p2: mark#(U91(X1,X2)) -> mark#(X1)

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt(),V) -> a__U12(a__isPalListKind(V),V)
r5: a__U12(tt(),V) -> a__U13(a__isNeList(V))
r6: a__U13(tt()) -> tt()
r7: a__U21(tt(),V1,V2) -> a__U22(a__isPalListKind(V1),V1,V2)
r8: a__U22(tt(),V1,V2) -> a__U23(a__isPalListKind(V2),V1,V2)
r9: a__U23(tt(),V1,V2) -> a__U24(a__isPalListKind(V2),V1,V2)
r10: a__U24(tt(),V1,V2) -> a__U25(a__isList(V1),V2)
r11: a__U25(tt(),V2) -> a__U26(a__isList(V2))
r12: a__U26(tt()) -> tt()
r13: a__U31(tt(),V) -> a__U32(a__isPalListKind(V),V)
r14: a__U32(tt(),V) -> a__U33(a__isQid(V))
r15: a__U33(tt()) -> tt()
r16: a__U41(tt(),V1,V2) -> a__U42(a__isPalListKind(V1),V1,V2)
r17: a__U42(tt(),V1,V2) -> a__U43(a__isPalListKind(V2),V1,V2)
r18: a__U43(tt(),V1,V2) -> a__U44(a__isPalListKind(V2),V1,V2)
r19: a__U44(tt(),V1,V2) -> a__U45(a__isList(V1),V2)
r20: a__U45(tt(),V2) -> a__U46(a__isNeList(V2))
r21: a__U46(tt()) -> tt()
r22: a__U51(tt(),V1,V2) -> a__U52(a__isPalListKind(V1),V1,V2)
r23: a__U52(tt(),V1,V2) -> a__U53(a__isPalListKind(V2),V1,V2)
r24: a__U53(tt(),V1,V2) -> a__U54(a__isPalListKind(V2),V1,V2)
r25: a__U54(tt(),V1,V2) -> a__U55(a__isNeList(V1),V2)
r26: a__U55(tt(),V2) -> a__U56(a__isList(V2))
r27: a__U56(tt()) -> tt()
r28: a__U61(tt(),V) -> a__U62(a__isPalListKind(V),V)
r29: a__U62(tt(),V) -> a__U63(a__isQid(V))
r30: a__U63(tt()) -> tt()
r31: a__U71(tt(),I,P) -> a__U72(a__isPalListKind(I),P)
r32: a__U72(tt(),P) -> a__U73(a__isPal(P),P)
r33: a__U73(tt(),P) -> a__U74(a__isPalListKind(P))
r34: a__U74(tt()) -> tt()
r35: a__U81(tt(),V) -> a__U82(a__isPalListKind(V),V)
r36: a__U82(tt(),V) -> a__U83(a__isNePal(V))
r37: a__U83(tt()) -> tt()
r38: a__U91(tt(),V2) -> a__U92(a__isPalListKind(V2))
r39: a__U92(tt()) -> tt()
r40: a__isList(V) -> a__U11(a__isPalListKind(V),V)
r41: a__isList(nil()) -> tt()
r42: a__isList(__(V1,V2)) -> a__U21(a__isPalListKind(V1),V1,V2)
r43: a__isNeList(V) -> a__U31(a__isPalListKind(V),V)
r44: a__isNeList(__(V1,V2)) -> a__U41(a__isPalListKind(V1),V1,V2)
r45: a__isNeList(__(V1,V2)) -> a__U51(a__isPalListKind(V1),V1,V2)
r46: a__isNePal(V) -> a__U61(a__isPalListKind(V),V)
r47: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),I,P)
r48: a__isPal(V) -> a__U81(a__isPalListKind(V),V)
r49: a__isPal(nil()) -> tt()
r50: a__isPalListKind(a()) -> tt()
r51: a__isPalListKind(e()) -> tt()
r52: a__isPalListKind(i()) -> tt()
r53: a__isPalListKind(nil()) -> tt()
r54: a__isPalListKind(o()) -> tt()
r55: a__isPalListKind(u()) -> tt()
r56: a__isPalListKind(__(V1,V2)) -> a__U91(a__isPalListKind(V1),V2)
r57: a__isQid(a()) -> tt()
r58: a__isQid(e()) -> tt()
r59: a__isQid(i()) -> tt()
r60: a__isQid(o()) -> tt()
r61: a__isQid(u()) -> tt()
r62: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r63: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r64: mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
r65: mark(isPalListKind(X)) -> a__isPalListKind(X)
r66: mark(U13(X)) -> a__U13(mark(X))
r67: mark(isNeList(X)) -> a__isNeList(X)
r68: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
r69: mark(U22(X1,X2,X3)) -> a__U22(mark(X1),X2,X3)
r70: mark(U23(X1,X2,X3)) -> a__U23(mark(X1),X2,X3)
r71: mark(U24(X1,X2,X3)) -> a__U24(mark(X1),X2,X3)
r72: mark(U25(X1,X2)) -> a__U25(mark(X1),X2)
r73: mark(isList(X)) -> a__isList(X)
r74: mark(U26(X)) -> a__U26(mark(X))
r75: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r76: mark(U32(X1,X2)) -> a__U32(mark(X1),X2)
r77: mark(U33(X)) -> a__U33(mark(X))
r78: mark(isQid(X)) -> a__isQid(X)
r79: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r80: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r81: mark(U43(X1,X2,X3)) -> a__U43(mark(X1),X2,X3)
r82: mark(U44(X1,X2,X3)) -> a__U44(mark(X1),X2,X3)
r83: mark(U45(X1,X2)) -> a__U45(mark(X1),X2)
r84: mark(U46(X)) -> a__U46(mark(X))
r85: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
r86: mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
r87: mark(U53(X1,X2,X3)) -> a__U53(mark(X1),X2,X3)
r88: mark(U54(X1,X2,X3)) -> a__U54(mark(X1),X2,X3)
r89: mark(U55(X1,X2)) -> a__U55(mark(X1),X2)
r90: mark(U56(X)) -> a__U56(mark(X))
r91: mark(U61(X1,X2)) -> a__U61(mark(X1),X2)
r92: mark(U62(X1,X2)) -> a__U62(mark(X1),X2)
r93: mark(U63(X)) -> a__U63(mark(X))
r94: mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
r95: mark(U72(X1,X2)) -> a__U72(mark(X1),X2)
r96: mark(U73(X1,X2)) -> a__U73(mark(X1),X2)
r97: mark(isPal(X)) -> a__isPal(X)
r98: mark(U74(X)) -> a__U74(mark(X))
r99: mark(U81(X1,X2)) -> a__U81(mark(X1),X2)
r100: mark(U82(X1,X2)) -> a__U82(mark(X1),X2)
r101: mark(U83(X)) -> a__U83(mark(X))
r102: mark(isNePal(X)) -> a__isNePal(X)
r103: mark(U91(X1,X2)) -> a__U91(mark(X1),X2)
r104: mark(U92(X)) -> a__U92(mark(X))
r105: mark(nil()) -> nil()
r106: mark(tt()) -> tt()
r107: mark(a()) -> a()
r108: mark(e()) -> e()
r109: mark(i()) -> i()
r110: mark(o()) -> o()
r111: mark(u()) -> u()
r112: a____(X1,X2) -> __(X1,X2)
r113: a__U11(X1,X2) -> U11(X1,X2)
r114: a__U12(X1,X2) -> U12(X1,X2)
r115: a__isPalListKind(X) -> isPalListKind(X)
r116: a__U13(X) -> U13(X)
r117: a__isNeList(X) -> isNeList(X)
r118: a__U21(X1,X2,X3) -> U21(X1,X2,X3)
r119: a__U22(X1,X2,X3) -> U22(X1,X2,X3)
r120: a__U23(X1,X2,X3) -> U23(X1,X2,X3)
r121: a__U24(X1,X2,X3) -> U24(X1,X2,X3)
r122: a__U25(X1,X2) -> U25(X1,X2)
r123: a__isList(X) -> isList(X)
r124: a__U26(X) -> U26(X)
r125: a__U31(X1,X2) -> U31(X1,X2)
r126: a__U32(X1,X2) -> U32(X1,X2)
r127: a__U33(X) -> U33(X)
r128: a__isQid(X) -> isQid(X)
r129: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r130: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r131: a__U43(X1,X2,X3) -> U43(X1,X2,X3)
r132: a__U44(X1,X2,X3) -> U44(X1,X2,X3)
r133: a__U45(X1,X2) -> U45(X1,X2)
r134: a__U46(X) -> U46(X)
r135: a__U51(X1,X2,X3) -> U51(X1,X2,X3)
r136: a__U52(X1,X2,X3) -> U52(X1,X2,X3)
r137: a__U53(X1,X2,X3) -> U53(X1,X2,X3)
r138: a__U54(X1,X2,X3) -> U54(X1,X2,X3)
r139: a__U55(X1,X2) -> U55(X1,X2)
r140: a__U56(X) -> U56(X)
r141: a__U61(X1,X2) -> U61(X1,X2)
r142: a__U62(X1,X2) -> U62(X1,X2)
r143: a__U63(X) -> U63(X)
r144: a__U71(X1,X2,X3) -> U71(X1,X2,X3)
r145: a__U72(X1,X2) -> U72(X1,X2)
r146: a__U73(X1,X2) -> U73(X1,X2)
r147: a__isPal(X) -> isPal(X)
r148: a__U74(X) -> U74(X)
r149: a__U81(X1,X2) -> U81(X1,X2)
r150: a__U82(X1,X2) -> U82(X1,X2)
r151: a__U83(X) -> U83(X)
r152: a__isNePal(X) -> isNePal(X)
r153: a__U91(X1,X2) -> U91(X1,X2)
r154: a__U92(X) -> U92(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        mark#_A(x1) = x1
        U92_A(x1) = x1 + 1
        U91_A(x1,x2) = x1 + x2 + 1
    
    2. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        mark#_A(x1) = x1
        U92_A(x1) = x1 + 1
        U91_A(x1,x2) = x1 + x2 + 1
    

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101, r102, r103, r104, r105, r106, r107, r108, r109, r110, r111, r112, r113, r114, r115, r116, r117, r118, r119, r120, r121, r122, r123, r124, r125, r126, r127, r128, r129, r130, r131, r132, r133, r134, r135, r136, r137, r138, r139, r140, r141, r142, r143, r144, r145, r146, r147, r148, r149, r150, r151, r152, r153, r154

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: a__U11#(tt(),V) -> a__U12#(a__isPalListKind(V),V)
p2: a__U12#(tt(),V) -> a__isNeList#(V)
p3: a__isNeList#(__(V1,V2)) -> a__U51#(a__isPalListKind(V1),V1,V2)
p4: a__U51#(tt(),V1,V2) -> a__U52#(a__isPalListKind(V1),V1,V2)
p5: a__U52#(tt(),V1,V2) -> a__U53#(a__isPalListKind(V2),V1,V2)
p6: a__U53#(tt(),V1,V2) -> a__U54#(a__isPalListKind(V2),V1,V2)
p7: a__U54#(tt(),V1,V2) -> a__isNeList#(V1)
p8: a__isNeList#(__(V1,V2)) -> a__U41#(a__isPalListKind(V1),V1,V2)
p9: a__U41#(tt(),V1,V2) -> a__U42#(a__isPalListKind(V1),V1,V2)
p10: a__U42#(tt(),V1,V2) -> a__U43#(a__isPalListKind(V2),V1,V2)
p11: a__U43#(tt(),V1,V2) -> a__U44#(a__isPalListKind(V2),V1,V2)
p12: a__U44#(tt(),V1,V2) -> a__isList#(V1)
p13: a__isList#(__(V1,V2)) -> a__U21#(a__isPalListKind(V1),V1,V2)
p14: a__U21#(tt(),V1,V2) -> a__U22#(a__isPalListKind(V1),V1,V2)
p15: a__U22#(tt(),V1,V2) -> a__U23#(a__isPalListKind(V2),V1,V2)
p16: a__U23#(tt(),V1,V2) -> a__U24#(a__isPalListKind(V2),V1,V2)
p17: a__U24#(tt(),V1,V2) -> a__isList#(V1)
p18: a__isList#(V) -> a__U11#(a__isPalListKind(V),V)
p19: a__U24#(tt(),V1,V2) -> a__U25#(a__isList(V1),V2)
p20: a__U25#(tt(),V2) -> a__isList#(V2)
p21: a__U44#(tt(),V1,V2) -> a__U45#(a__isList(V1),V2)
p22: a__U45#(tt(),V2) -> a__isNeList#(V2)
p23: a__U54#(tt(),V1,V2) -> a__U55#(a__isNeList(V1),V2)
p24: a__U55#(tt(),V2) -> a__isList#(V2)

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt(),V) -> a__U12(a__isPalListKind(V),V)
r5: a__U12(tt(),V) -> a__U13(a__isNeList(V))
r6: a__U13(tt()) -> tt()
r7: a__U21(tt(),V1,V2) -> a__U22(a__isPalListKind(V1),V1,V2)
r8: a__U22(tt(),V1,V2) -> a__U23(a__isPalListKind(V2),V1,V2)
r9: a__U23(tt(),V1,V2) -> a__U24(a__isPalListKind(V2),V1,V2)
r10: a__U24(tt(),V1,V2) -> a__U25(a__isList(V1),V2)
r11: a__U25(tt(),V2) -> a__U26(a__isList(V2))
r12: a__U26(tt()) -> tt()
r13: a__U31(tt(),V) -> a__U32(a__isPalListKind(V),V)
r14: a__U32(tt(),V) -> a__U33(a__isQid(V))
r15: a__U33(tt()) -> tt()
r16: a__U41(tt(),V1,V2) -> a__U42(a__isPalListKind(V1),V1,V2)
r17: a__U42(tt(),V1,V2) -> a__U43(a__isPalListKind(V2),V1,V2)
r18: a__U43(tt(),V1,V2) -> a__U44(a__isPalListKind(V2),V1,V2)
r19: a__U44(tt(),V1,V2) -> a__U45(a__isList(V1),V2)
r20: a__U45(tt(),V2) -> a__U46(a__isNeList(V2))
r21: a__U46(tt()) -> tt()
r22: a__U51(tt(),V1,V2) -> a__U52(a__isPalListKind(V1),V1,V2)
r23: a__U52(tt(),V1,V2) -> a__U53(a__isPalListKind(V2),V1,V2)
r24: a__U53(tt(),V1,V2) -> a__U54(a__isPalListKind(V2),V1,V2)
r25: a__U54(tt(),V1,V2) -> a__U55(a__isNeList(V1),V2)
r26: a__U55(tt(),V2) -> a__U56(a__isList(V2))
r27: a__U56(tt()) -> tt()
r28: a__U61(tt(),V) -> a__U62(a__isPalListKind(V),V)
r29: a__U62(tt(),V) -> a__U63(a__isQid(V))
r30: a__U63(tt()) -> tt()
r31: a__U71(tt(),I,P) -> a__U72(a__isPalListKind(I),P)
r32: a__U72(tt(),P) -> a__U73(a__isPal(P),P)
r33: a__U73(tt(),P) -> a__U74(a__isPalListKind(P))
r34: a__U74(tt()) -> tt()
r35: a__U81(tt(),V) -> a__U82(a__isPalListKind(V),V)
r36: a__U82(tt(),V) -> a__U83(a__isNePal(V))
r37: a__U83(tt()) -> tt()
r38: a__U91(tt(),V2) -> a__U92(a__isPalListKind(V2))
r39: a__U92(tt()) -> tt()
r40: a__isList(V) -> a__U11(a__isPalListKind(V),V)
r41: a__isList(nil()) -> tt()
r42: a__isList(__(V1,V2)) -> a__U21(a__isPalListKind(V1),V1,V2)
r43: a__isNeList(V) -> a__U31(a__isPalListKind(V),V)
r44: a__isNeList(__(V1,V2)) -> a__U41(a__isPalListKind(V1),V1,V2)
r45: a__isNeList(__(V1,V2)) -> a__U51(a__isPalListKind(V1),V1,V2)
r46: a__isNePal(V) -> a__U61(a__isPalListKind(V),V)
r47: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),I,P)
r48: a__isPal(V) -> a__U81(a__isPalListKind(V),V)
r49: a__isPal(nil()) -> tt()
r50: a__isPalListKind(a()) -> tt()
r51: a__isPalListKind(e()) -> tt()
r52: a__isPalListKind(i()) -> tt()
r53: a__isPalListKind(nil()) -> tt()
r54: a__isPalListKind(o()) -> tt()
r55: a__isPalListKind(u()) -> tt()
r56: a__isPalListKind(__(V1,V2)) -> a__U91(a__isPalListKind(V1),V2)
r57: a__isQid(a()) -> tt()
r58: a__isQid(e()) -> tt()
r59: a__isQid(i()) -> tt()
r60: a__isQid(o()) -> tt()
r61: a__isQid(u()) -> tt()
r62: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r63: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r64: mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
r65: mark(isPalListKind(X)) -> a__isPalListKind(X)
r66: mark(U13(X)) -> a__U13(mark(X))
r67: mark(isNeList(X)) -> a__isNeList(X)
r68: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
r69: mark(U22(X1,X2,X3)) -> a__U22(mark(X1),X2,X3)
r70: mark(U23(X1,X2,X3)) -> a__U23(mark(X1),X2,X3)
r71: mark(U24(X1,X2,X3)) -> a__U24(mark(X1),X2,X3)
r72: mark(U25(X1,X2)) -> a__U25(mark(X1),X2)
r73: mark(isList(X)) -> a__isList(X)
r74: mark(U26(X)) -> a__U26(mark(X))
r75: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r76: mark(U32(X1,X2)) -> a__U32(mark(X1),X2)
r77: mark(U33(X)) -> a__U33(mark(X))
r78: mark(isQid(X)) -> a__isQid(X)
r79: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r80: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r81: mark(U43(X1,X2,X3)) -> a__U43(mark(X1),X2,X3)
r82: mark(U44(X1,X2,X3)) -> a__U44(mark(X1),X2,X3)
r83: mark(U45(X1,X2)) -> a__U45(mark(X1),X2)
r84: mark(U46(X)) -> a__U46(mark(X))
r85: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
r86: mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
r87: mark(U53(X1,X2,X3)) -> a__U53(mark(X1),X2,X3)
r88: mark(U54(X1,X2,X3)) -> a__U54(mark(X1),X2,X3)
r89: mark(U55(X1,X2)) -> a__U55(mark(X1),X2)
r90: mark(U56(X)) -> a__U56(mark(X))
r91: mark(U61(X1,X2)) -> a__U61(mark(X1),X2)
r92: mark(U62(X1,X2)) -> a__U62(mark(X1),X2)
r93: mark(U63(X)) -> a__U63(mark(X))
r94: mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
r95: mark(U72(X1,X2)) -> a__U72(mark(X1),X2)
r96: mark(U73(X1,X2)) -> a__U73(mark(X1),X2)
r97: mark(isPal(X)) -> a__isPal(X)
r98: mark(U74(X)) -> a__U74(mark(X))
r99: mark(U81(X1,X2)) -> a__U81(mark(X1),X2)
r100: mark(U82(X1,X2)) -> a__U82(mark(X1),X2)
r101: mark(U83(X)) -> a__U83(mark(X))
r102: mark(isNePal(X)) -> a__isNePal(X)
r103: mark(U91(X1,X2)) -> a__U91(mark(X1),X2)
r104: mark(U92(X)) -> a__U92(mark(X))
r105: mark(nil()) -> nil()
r106: mark(tt()) -> tt()
r107: mark(a()) -> a()
r108: mark(e()) -> e()
r109: mark(i()) -> i()
r110: mark(o()) -> o()
r111: mark(u()) -> u()
r112: a____(X1,X2) -> __(X1,X2)
r113: a__U11(X1,X2) -> U11(X1,X2)
r114: a__U12(X1,X2) -> U12(X1,X2)
r115: a__isPalListKind(X) -> isPalListKind(X)
r116: a__U13(X) -> U13(X)
r117: a__isNeList(X) -> isNeList(X)
r118: a__U21(X1,X2,X3) -> U21(X1,X2,X3)
r119: a__U22(X1,X2,X3) -> U22(X1,X2,X3)
r120: a__U23(X1,X2,X3) -> U23(X1,X2,X3)
r121: a__U24(X1,X2,X3) -> U24(X1,X2,X3)
r122: a__U25(X1,X2) -> U25(X1,X2)
r123: a__isList(X) -> isList(X)
r124: a__U26(X) -> U26(X)
r125: a__U31(X1,X2) -> U31(X1,X2)
r126: a__U32(X1,X2) -> U32(X1,X2)
r127: a__U33(X) -> U33(X)
r128: a__isQid(X) -> isQid(X)
r129: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r130: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r131: a__U43(X1,X2,X3) -> U43(X1,X2,X3)
r132: a__U44(X1,X2,X3) -> U44(X1,X2,X3)
r133: a__U45(X1,X2) -> U45(X1,X2)
r134: a__U46(X) -> U46(X)
r135: a__U51(X1,X2,X3) -> U51(X1,X2,X3)
r136: a__U52(X1,X2,X3) -> U52(X1,X2,X3)
r137: a__U53(X1,X2,X3) -> U53(X1,X2,X3)
r138: a__U54(X1,X2,X3) -> U54(X1,X2,X3)
r139: a__U55(X1,X2) -> U55(X1,X2)
r140: a__U56(X) -> U56(X)
r141: a__U61(X1,X2) -> U61(X1,X2)
r142: a__U62(X1,X2) -> U62(X1,X2)
r143: a__U63(X) -> U63(X)
r144: a__U71(X1,X2,X3) -> U71(X1,X2,X3)
r145: a__U72(X1,X2) -> U72(X1,X2)
r146: a__U73(X1,X2) -> U73(X1,X2)
r147: a__isPal(X) -> isPal(X)
r148: a__U74(X) -> U74(X)
r149: a__U81(X1,X2) -> U81(X1,X2)
r150: a__U82(X1,X2) -> U82(X1,X2)
r151: a__U83(X) -> U83(X)
r152: a__isNePal(X) -> isNePal(X)
r153: a__U91(X1,X2) -> U91(X1,X2)
r154: a__U92(X) -> U92(X)

The set of usable rules consists of

  r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r38, r39, r40, r41, r42, r43, r44, r45, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r113, r114, r115, r116, r117, r118, r119, r120, r121, r122, r123, r124, r125, r126, r127, r128, r129, r130, r131, r132, r133, r134, r135, r136, r137, r138, r139, r140, r153, r154

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a__U11#_A(x1,x2) = x2 + 5
        tt_A() = 1
        a__U12#_A(x1,x2) = x1 + x2
        a__isPalListKind_A(x1) = 4
        a__isNeList#_A(x1) = x1
        ___A(x1,x2) = x1 + x2 + 22
        a__U51#_A(x1,x2,x3) = x2 + x3 + 21
        a__U52#_A(x1,x2,x3) = x2 + x3 + 20
        a__U53#_A(x1,x2,x3) = x2 + x3 + 19
        a__U54#_A(x1,x2,x3) = x1 + x2 + x3 + 14
        a__U41#_A(x1,x2,x3) = x1 + x2 + x3 + 17
        a__U42#_A(x1,x2,x3) = x2 + x3 + 17
        a__U43#_A(x1,x2,x3) = x2 + x3 + 16
        a__U44#_A(x1,x2,x3) = x2 + x3 + 15
        a__isList#_A(x1) = x1 + 6
        a__U21#_A(x1,x2,x3) = x2 + x3 + 27
        a__U22#_A(x1,x2,x3) = x2 + x3 + 26
        a__U23#_A(x1,x2,x3) = x2 + x3 + 12
        a__U24#_A(x1,x2,x3) = x1 + x2 + x3 + 7
        a__U25#_A(x1,x2) = x2 + 7
        a__isList_A(x1) = x1 + 5
        a__U45#_A(x1,x2) = x2 + 1
        a__U55#_A(x1,x2) = x1 + x2 + 6
        a__isNeList_A(x1) = x1 + 8
        a__U26_A(x1) = 2
        a__U46_A(x1) = 2
        a__U56_A(x1) = x1 + 1
        U26_A(x1) = 0
        U46_A(x1) = 0
        U56_A(x1) = x1
        a__U25_A(x1,x2) = 3
        a__U45_A(x1,x2) = x2 + 3
        a__U55_A(x1,x2) = x2 + 7
        U25_A(x1,x2) = 0
        U45_A(x1,x2) = 0
        U55_A(x1,x2) = 0
        a__U24_A(x1,x2,x3) = 4
        a__U44_A(x1,x2,x3) = x1 + x3 + 3
        a__U54_A(x1,x2,x3) = x3 + 8
        U24_A(x1,x2,x3) = 0
        U44_A(x1,x2,x3) = x1 + x3 + 2
        U54_A(x1,x2,x3) = x3
        a__U13_A(x1) = 2
        a__U23_A(x1,x2,x3) = x1 + 4
        a__U33_A(x1) = x1 + 1
        a__U43_A(x1,x2,x3) = x1 + x3 + 7
        a__U53_A(x1,x2,x3) = x1 + x3 + 8
        a__isQid_A(x1) = x1 + 1
        a_A() = 1
        e_A() = 1
        i_A() = 1
        o_A() = 1
        u_A() = 1
        U13_A(x1) = 0
        U23_A(x1,x2,x3) = x1
        U33_A(x1) = 0
        isQid_A(x1) = 0
        U43_A(x1,x2,x3) = x3
        U53_A(x1,x2,x3) = 0
        a__U12_A(x1,x2) = x2 + 3
        a__U22_A(x1,x2,x3) = x3 + 9
        a__U32_A(x1,x2) = x2 + 3
        a__U42_A(x1,x2,x3) = x1 + x2 + x3 + 21
        a__U52_A(x1,x2,x3) = x3 + 13
        a__U92_A(x1) = 2
        U12_A(x1,x2) = 0
        U22_A(x1,x2,x3) = x3
        U32_A(x1,x2) = 0
        U42_A(x1,x2,x3) = x1
        U52_A(x1,x2,x3) = x3 + 12
        U92_A(x1) = 1
        a__U11_A(x1,x2) = x2 + 4
        a__U21_A(x1,x2,x3) = x1 + x3 + 9
        a__U31_A(x1,x2) = x1 + x2 + 3
        a__U41_A(x1,x2,x3) = x1 + x2 + x3 + 25
        a__U51_A(x1,x2,x3) = x1 + x3 + 13
        a__U91_A(x1,x2) = 3
        U11_A(x1,x2) = 0
        U21_A(x1,x2,x3) = 0
        U31_A(x1,x2) = 0
        U41_A(x1,x2,x3) = 0
        U51_A(x1,x2,x3) = 12
        U91_A(x1,x2) = 0
        nil_A() = 1
        isPalListKind_A(x1) = 0
        isNeList_A(x1) = 0
        isList_A(x1) = 0
    
    2. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a__U11#_A(x1,x2) = 4
        tt_A() = 4
        a__U12#_A(x1,x2) = x2 + 3
        a__isPalListKind_A(x1) = 1
        a__isNeList#_A(x1) = 2
        ___A(x1,x2) = x1 + x2 + 1
        a__U51#_A(x1,x2,x3) = x2 + x3 + 1
        a__U52#_A(x1,x2,x3) = 0
        a__U53#_A(x1,x2,x3) = 0
        a__U54#_A(x1,x2,x3) = x1 + x2
        a__U41#_A(x1,x2,x3) = x1 + x2
        a__U42#_A(x1,x2,x3) = x3 + 1
        a__U43#_A(x1,x2,x3) = 0
        a__U44#_A(x1,x2,x3) = 7
        a__isList#_A(x1) = x1 + 6
        a__U21#_A(x1,x2,x3) = 8
        a__U22#_A(x1,x2,x3) = 9
        a__U23#_A(x1,x2,x3) = x2 + 6
        a__U24#_A(x1,x2,x3) = 7
        a__U25#_A(x1,x2) = x2 + 5
        a__isList_A(x1) = x1 + 1
        a__U45#_A(x1,x2) = x2 + 1
        a__U55#_A(x1,x2) = 5
        a__isNeList_A(x1) = 3
        a__U26_A(x1) = 6
        a__U46_A(x1) = 6
        a__U56_A(x1) = 3
        U26_A(x1) = 0
        U46_A(x1) = 6
        U56_A(x1) = 4
        a__U25_A(x1,x2) = 5
        a__U45_A(x1,x2) = 5
        a__U55_A(x1,x2) = x2 + 2
        U25_A(x1,x2) = 4
        U45_A(x1,x2) = 6
        U55_A(x1,x2) = 0
        a__U24_A(x1,x2,x3) = 6
        a__U44_A(x1,x2,x3) = x1 + x3
        a__U54_A(x1,x2,x3) = 1
        U24_A(x1,x2,x3) = 7
        U44_A(x1,x2,x3) = x1 + x3 + 1
        U54_A(x1,x2,x3) = 0
        a__U13_A(x1) = 2
        a__U23_A(x1,x2,x3) = 5
        a__U33_A(x1) = 4
        a__U43_A(x1,x2,x3) = 7
        a__U53_A(x1,x2,x3) = 9
        a__isQid_A(x1) = 5
        a_A() = 0
        e_A() = 1
        i_A() = 1
        o_A() = 1
        u_A() = 1
        U13_A(x1) = 3
        U23_A(x1,x2,x3) = x1
        U33_A(x1) = 5
        isQid_A(x1) = 6
        U43_A(x1,x2,x3) = x3 + 8
        U53_A(x1,x2,x3) = 0
        a__U12_A(x1,x2) = 1
        a__U22_A(x1,x2,x3) = x3 + 4
        a__U32_A(x1,x2) = 5
        a__U42_A(x1,x2,x3) = 6
        a__U52_A(x1,x2,x3) = 8
        a__U92_A(x1) = 3
        U12_A(x1,x2) = 2
        U22_A(x1,x2,x3) = x3 + 3
        U32_A(x1,x2) = 6
        U42_A(x1,x2,x3) = x1 + 7
        U52_A(x1,x2,x3) = x3 + 9
        U92_A(x1) = 4
        a__U11_A(x1,x2) = 0
        a__U21_A(x1,x2,x3) = 3
        a__U31_A(x1,x2) = 6
        a__U41_A(x1,x2,x3) = x1 + 1
        a__U51_A(x1,x2,x3) = x1 + 3
        a__U91_A(x1,x2) = 2
        U11_A(x1,x2) = 1
        U21_A(x1,x2,x3) = 4
        U31_A(x1,x2) = 7
        U41_A(x1,x2,x3) = 0
        U51_A(x1,x2,x3) = 4
        U91_A(x1,x2) = 3
        nil_A() = 0
        isPalListKind_A(x1) = 2
        isNeList_A(x1) = 0
        isList_A(x1) = 2
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: a__U82#(tt(),V) -> a__isNePal#(V)
p2: a__isNePal#(__(I,__(P,I))) -> a__U71#(a__isQid(I),I,P)
p3: a__U71#(tt(),I,P) -> a__U72#(a__isPalListKind(I),P)
p4: a__U72#(tt(),P) -> a__isPal#(P)
p5: a__isPal#(V) -> a__U81#(a__isPalListKind(V),V)
p6: a__U81#(tt(),V) -> a__U82#(a__isPalListKind(V),V)

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt(),V) -> a__U12(a__isPalListKind(V),V)
r5: a__U12(tt(),V) -> a__U13(a__isNeList(V))
r6: a__U13(tt()) -> tt()
r7: a__U21(tt(),V1,V2) -> a__U22(a__isPalListKind(V1),V1,V2)
r8: a__U22(tt(),V1,V2) -> a__U23(a__isPalListKind(V2),V1,V2)
r9: a__U23(tt(),V1,V2) -> a__U24(a__isPalListKind(V2),V1,V2)
r10: a__U24(tt(),V1,V2) -> a__U25(a__isList(V1),V2)
r11: a__U25(tt(),V2) -> a__U26(a__isList(V2))
r12: a__U26(tt()) -> tt()
r13: a__U31(tt(),V) -> a__U32(a__isPalListKind(V),V)
r14: a__U32(tt(),V) -> a__U33(a__isQid(V))
r15: a__U33(tt()) -> tt()
r16: a__U41(tt(),V1,V2) -> a__U42(a__isPalListKind(V1),V1,V2)
r17: a__U42(tt(),V1,V2) -> a__U43(a__isPalListKind(V2),V1,V2)
r18: a__U43(tt(),V1,V2) -> a__U44(a__isPalListKind(V2),V1,V2)
r19: a__U44(tt(),V1,V2) -> a__U45(a__isList(V1),V2)
r20: a__U45(tt(),V2) -> a__U46(a__isNeList(V2))
r21: a__U46(tt()) -> tt()
r22: a__U51(tt(),V1,V2) -> a__U52(a__isPalListKind(V1),V1,V2)
r23: a__U52(tt(),V1,V2) -> a__U53(a__isPalListKind(V2),V1,V2)
r24: a__U53(tt(),V1,V2) -> a__U54(a__isPalListKind(V2),V1,V2)
r25: a__U54(tt(),V1,V2) -> a__U55(a__isNeList(V1),V2)
r26: a__U55(tt(),V2) -> a__U56(a__isList(V2))
r27: a__U56(tt()) -> tt()
r28: a__U61(tt(),V) -> a__U62(a__isPalListKind(V),V)
r29: a__U62(tt(),V) -> a__U63(a__isQid(V))
r30: a__U63(tt()) -> tt()
r31: a__U71(tt(),I,P) -> a__U72(a__isPalListKind(I),P)
r32: a__U72(tt(),P) -> a__U73(a__isPal(P),P)
r33: a__U73(tt(),P) -> a__U74(a__isPalListKind(P))
r34: a__U74(tt()) -> tt()
r35: a__U81(tt(),V) -> a__U82(a__isPalListKind(V),V)
r36: a__U82(tt(),V) -> a__U83(a__isNePal(V))
r37: a__U83(tt()) -> tt()
r38: a__U91(tt(),V2) -> a__U92(a__isPalListKind(V2))
r39: a__U92(tt()) -> tt()
r40: a__isList(V) -> a__U11(a__isPalListKind(V),V)
r41: a__isList(nil()) -> tt()
r42: a__isList(__(V1,V2)) -> a__U21(a__isPalListKind(V1),V1,V2)
r43: a__isNeList(V) -> a__U31(a__isPalListKind(V),V)
r44: a__isNeList(__(V1,V2)) -> a__U41(a__isPalListKind(V1),V1,V2)
r45: a__isNeList(__(V1,V2)) -> a__U51(a__isPalListKind(V1),V1,V2)
r46: a__isNePal(V) -> a__U61(a__isPalListKind(V),V)
r47: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),I,P)
r48: a__isPal(V) -> a__U81(a__isPalListKind(V),V)
r49: a__isPal(nil()) -> tt()
r50: a__isPalListKind(a()) -> tt()
r51: a__isPalListKind(e()) -> tt()
r52: a__isPalListKind(i()) -> tt()
r53: a__isPalListKind(nil()) -> tt()
r54: a__isPalListKind(o()) -> tt()
r55: a__isPalListKind(u()) -> tt()
r56: a__isPalListKind(__(V1,V2)) -> a__U91(a__isPalListKind(V1),V2)
r57: a__isQid(a()) -> tt()
r58: a__isQid(e()) -> tt()
r59: a__isQid(i()) -> tt()
r60: a__isQid(o()) -> tt()
r61: a__isQid(u()) -> tt()
r62: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r63: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r64: mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
r65: mark(isPalListKind(X)) -> a__isPalListKind(X)
r66: mark(U13(X)) -> a__U13(mark(X))
r67: mark(isNeList(X)) -> a__isNeList(X)
r68: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
r69: mark(U22(X1,X2,X3)) -> a__U22(mark(X1),X2,X3)
r70: mark(U23(X1,X2,X3)) -> a__U23(mark(X1),X2,X3)
r71: mark(U24(X1,X2,X3)) -> a__U24(mark(X1),X2,X3)
r72: mark(U25(X1,X2)) -> a__U25(mark(X1),X2)
r73: mark(isList(X)) -> a__isList(X)
r74: mark(U26(X)) -> a__U26(mark(X))
r75: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r76: mark(U32(X1,X2)) -> a__U32(mark(X1),X2)
r77: mark(U33(X)) -> a__U33(mark(X))
r78: mark(isQid(X)) -> a__isQid(X)
r79: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r80: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r81: mark(U43(X1,X2,X3)) -> a__U43(mark(X1),X2,X3)
r82: mark(U44(X1,X2,X3)) -> a__U44(mark(X1),X2,X3)
r83: mark(U45(X1,X2)) -> a__U45(mark(X1),X2)
r84: mark(U46(X)) -> a__U46(mark(X))
r85: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
r86: mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
r87: mark(U53(X1,X2,X3)) -> a__U53(mark(X1),X2,X3)
r88: mark(U54(X1,X2,X3)) -> a__U54(mark(X1),X2,X3)
r89: mark(U55(X1,X2)) -> a__U55(mark(X1),X2)
r90: mark(U56(X)) -> a__U56(mark(X))
r91: mark(U61(X1,X2)) -> a__U61(mark(X1),X2)
r92: mark(U62(X1,X2)) -> a__U62(mark(X1),X2)
r93: mark(U63(X)) -> a__U63(mark(X))
r94: mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
r95: mark(U72(X1,X2)) -> a__U72(mark(X1),X2)
r96: mark(U73(X1,X2)) -> a__U73(mark(X1),X2)
r97: mark(isPal(X)) -> a__isPal(X)
r98: mark(U74(X)) -> a__U74(mark(X))
r99: mark(U81(X1,X2)) -> a__U81(mark(X1),X2)
r100: mark(U82(X1,X2)) -> a__U82(mark(X1),X2)
r101: mark(U83(X)) -> a__U83(mark(X))
r102: mark(isNePal(X)) -> a__isNePal(X)
r103: mark(U91(X1,X2)) -> a__U91(mark(X1),X2)
r104: mark(U92(X)) -> a__U92(mark(X))
r105: mark(nil()) -> nil()
r106: mark(tt()) -> tt()
r107: mark(a()) -> a()
r108: mark(e()) -> e()
r109: mark(i()) -> i()
r110: mark(o()) -> o()
r111: mark(u()) -> u()
r112: a____(X1,X2) -> __(X1,X2)
r113: a__U11(X1,X2) -> U11(X1,X2)
r114: a__U12(X1,X2) -> U12(X1,X2)
r115: a__isPalListKind(X) -> isPalListKind(X)
r116: a__U13(X) -> U13(X)
r117: a__isNeList(X) -> isNeList(X)
r118: a__U21(X1,X2,X3) -> U21(X1,X2,X3)
r119: a__U22(X1,X2,X3) -> U22(X1,X2,X3)
r120: a__U23(X1,X2,X3) -> U23(X1,X2,X3)
r121: a__U24(X1,X2,X3) -> U24(X1,X2,X3)
r122: a__U25(X1,X2) -> U25(X1,X2)
r123: a__isList(X) -> isList(X)
r124: a__U26(X) -> U26(X)
r125: a__U31(X1,X2) -> U31(X1,X2)
r126: a__U32(X1,X2) -> U32(X1,X2)
r127: a__U33(X) -> U33(X)
r128: a__isQid(X) -> isQid(X)
r129: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r130: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r131: a__U43(X1,X2,X3) -> U43(X1,X2,X3)
r132: a__U44(X1,X2,X3) -> U44(X1,X2,X3)
r133: a__U45(X1,X2) -> U45(X1,X2)
r134: a__U46(X) -> U46(X)
r135: a__U51(X1,X2,X3) -> U51(X1,X2,X3)
r136: a__U52(X1,X2,X3) -> U52(X1,X2,X3)
r137: a__U53(X1,X2,X3) -> U53(X1,X2,X3)
r138: a__U54(X1,X2,X3) -> U54(X1,X2,X3)
r139: a__U55(X1,X2) -> U55(X1,X2)
r140: a__U56(X) -> U56(X)
r141: a__U61(X1,X2) -> U61(X1,X2)
r142: a__U62(X1,X2) -> U62(X1,X2)
r143: a__U63(X) -> U63(X)
r144: a__U71(X1,X2,X3) -> U71(X1,X2,X3)
r145: a__U72(X1,X2) -> U72(X1,X2)
r146: a__U73(X1,X2) -> U73(X1,X2)
r147: a__isPal(X) -> isPal(X)
r148: a__U74(X) -> U74(X)
r149: a__U81(X1,X2) -> U81(X1,X2)
r150: a__U82(X1,X2) -> U82(X1,X2)
r151: a__U83(X) -> U83(X)
r152: a__isNePal(X) -> isNePal(X)
r153: a__U91(X1,X2) -> U91(X1,X2)
r154: a__U92(X) -> U92(X)

The set of usable rules consists of

  r38, r39, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r115, r128, r153, r154

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a__U82#_A(x1,x2) = x2 + 3
        tt_A() = 5
        a__isNePal#_A(x1) = x1 + 2
        ___A(x1,x2) = x1 + x2
        a__U71#_A(x1,x2,x3) = x1 + x2 + x3
        a__isQid_A(x1) = x1 + 1
        a__U72#_A(x1,x2) = x1 + x2 + 1
        a__isPalListKind_A(x1) = x1 + 3
        a__isPal#_A(x1) = x1 + 5
        a__U81#_A(x1,x2) = x2 + 4
        a__U92_A(x1) = x1 + 1
        U92_A(x1) = 0
        a__U91_A(x1,x2) = x1 + x2
        U91_A(x1,x2) = 0
        a_A() = 5
        e_A() = 5
        i_A() = 5
        nil_A() = 3
        o_A() = 5
        u_A() = 5
        isPalListKind_A(x1) = 0
        isQid_A(x1) = 0
    
    2. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a__U82#_A(x1,x2) = 1
        tt_A() = 3
        a__isNePal#_A(x1) = 2
        ___A(x1,x2) = 1
        a__U71#_A(x1,x2,x3) = 5
        a__isQid_A(x1) = 2
        a__U72#_A(x1,x2) = x1
        a__isPalListKind_A(x1) = 4
        a__isPal#_A(x1) = 4
        a__U81#_A(x1,x2) = 0
        a__U92_A(x1) = 2
        U92_A(x1) = 0
        a__U91_A(x1,x2) = 1
        U91_A(x1,x2) = 0
        a_A() = 1
        e_A() = 1
        i_A() = 1
        nil_A() = 1
        o_A() = 1
        u_A() = 1
        isPalListKind_A(x1) = 5
        isQid_A(x1) = 3
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6

We remove them from the problem.  Then no dependency pair remains.

-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: a__isPalListKind#(__(V1,V2)) -> a__U91#(a__isPalListKind(V1),V2)
p2: a__U91#(tt(),V2) -> a__isPalListKind#(V2)
p3: a__isPalListKind#(__(V1,V2)) -> a__isPalListKind#(V1)

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt(),V) -> a__U12(a__isPalListKind(V),V)
r5: a__U12(tt(),V) -> a__U13(a__isNeList(V))
r6: a__U13(tt()) -> tt()
r7: a__U21(tt(),V1,V2) -> a__U22(a__isPalListKind(V1),V1,V2)
r8: a__U22(tt(),V1,V2) -> a__U23(a__isPalListKind(V2),V1,V2)
r9: a__U23(tt(),V1,V2) -> a__U24(a__isPalListKind(V2),V1,V2)
r10: a__U24(tt(),V1,V2) -> a__U25(a__isList(V1),V2)
r11: a__U25(tt(),V2) -> a__U26(a__isList(V2))
r12: a__U26(tt()) -> tt()
r13: a__U31(tt(),V) -> a__U32(a__isPalListKind(V),V)
r14: a__U32(tt(),V) -> a__U33(a__isQid(V))
r15: a__U33(tt()) -> tt()
r16: a__U41(tt(),V1,V2) -> a__U42(a__isPalListKind(V1),V1,V2)
r17: a__U42(tt(),V1,V2) -> a__U43(a__isPalListKind(V2),V1,V2)
r18: a__U43(tt(),V1,V2) -> a__U44(a__isPalListKind(V2),V1,V2)
r19: a__U44(tt(),V1,V2) -> a__U45(a__isList(V1),V2)
r20: a__U45(tt(),V2) -> a__U46(a__isNeList(V2))
r21: a__U46(tt()) -> tt()
r22: a__U51(tt(),V1,V2) -> a__U52(a__isPalListKind(V1),V1,V2)
r23: a__U52(tt(),V1,V2) -> a__U53(a__isPalListKind(V2),V1,V2)
r24: a__U53(tt(),V1,V2) -> a__U54(a__isPalListKind(V2),V1,V2)
r25: a__U54(tt(),V1,V2) -> a__U55(a__isNeList(V1),V2)
r26: a__U55(tt(),V2) -> a__U56(a__isList(V2))
r27: a__U56(tt()) -> tt()
r28: a__U61(tt(),V) -> a__U62(a__isPalListKind(V),V)
r29: a__U62(tt(),V) -> a__U63(a__isQid(V))
r30: a__U63(tt()) -> tt()
r31: a__U71(tt(),I,P) -> a__U72(a__isPalListKind(I),P)
r32: a__U72(tt(),P) -> a__U73(a__isPal(P),P)
r33: a__U73(tt(),P) -> a__U74(a__isPalListKind(P))
r34: a__U74(tt()) -> tt()
r35: a__U81(tt(),V) -> a__U82(a__isPalListKind(V),V)
r36: a__U82(tt(),V) -> a__U83(a__isNePal(V))
r37: a__U83(tt()) -> tt()
r38: a__U91(tt(),V2) -> a__U92(a__isPalListKind(V2))
r39: a__U92(tt()) -> tt()
r40: a__isList(V) -> a__U11(a__isPalListKind(V),V)
r41: a__isList(nil()) -> tt()
r42: a__isList(__(V1,V2)) -> a__U21(a__isPalListKind(V1),V1,V2)
r43: a__isNeList(V) -> a__U31(a__isPalListKind(V),V)
r44: a__isNeList(__(V1,V2)) -> a__U41(a__isPalListKind(V1),V1,V2)
r45: a__isNeList(__(V1,V2)) -> a__U51(a__isPalListKind(V1),V1,V2)
r46: a__isNePal(V) -> a__U61(a__isPalListKind(V),V)
r47: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),I,P)
r48: a__isPal(V) -> a__U81(a__isPalListKind(V),V)
r49: a__isPal(nil()) -> tt()
r50: a__isPalListKind(a()) -> tt()
r51: a__isPalListKind(e()) -> tt()
r52: a__isPalListKind(i()) -> tt()
r53: a__isPalListKind(nil()) -> tt()
r54: a__isPalListKind(o()) -> tt()
r55: a__isPalListKind(u()) -> tt()
r56: a__isPalListKind(__(V1,V2)) -> a__U91(a__isPalListKind(V1),V2)
r57: a__isQid(a()) -> tt()
r58: a__isQid(e()) -> tt()
r59: a__isQid(i()) -> tt()
r60: a__isQid(o()) -> tt()
r61: a__isQid(u()) -> tt()
r62: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r63: mark(U11(X1,X2)) -> a__U11(mark(X1),X2)
r64: mark(U12(X1,X2)) -> a__U12(mark(X1),X2)
r65: mark(isPalListKind(X)) -> a__isPalListKind(X)
r66: mark(U13(X)) -> a__U13(mark(X))
r67: mark(isNeList(X)) -> a__isNeList(X)
r68: mark(U21(X1,X2,X3)) -> a__U21(mark(X1),X2,X3)
r69: mark(U22(X1,X2,X3)) -> a__U22(mark(X1),X2,X3)
r70: mark(U23(X1,X2,X3)) -> a__U23(mark(X1),X2,X3)
r71: mark(U24(X1,X2,X3)) -> a__U24(mark(X1),X2,X3)
r72: mark(U25(X1,X2)) -> a__U25(mark(X1),X2)
r73: mark(isList(X)) -> a__isList(X)
r74: mark(U26(X)) -> a__U26(mark(X))
r75: mark(U31(X1,X2)) -> a__U31(mark(X1),X2)
r76: mark(U32(X1,X2)) -> a__U32(mark(X1),X2)
r77: mark(U33(X)) -> a__U33(mark(X))
r78: mark(isQid(X)) -> a__isQid(X)
r79: mark(U41(X1,X2,X3)) -> a__U41(mark(X1),X2,X3)
r80: mark(U42(X1,X2,X3)) -> a__U42(mark(X1),X2,X3)
r81: mark(U43(X1,X2,X3)) -> a__U43(mark(X1),X2,X3)
r82: mark(U44(X1,X2,X3)) -> a__U44(mark(X1),X2,X3)
r83: mark(U45(X1,X2)) -> a__U45(mark(X1),X2)
r84: mark(U46(X)) -> a__U46(mark(X))
r85: mark(U51(X1,X2,X3)) -> a__U51(mark(X1),X2,X3)
r86: mark(U52(X1,X2,X3)) -> a__U52(mark(X1),X2,X3)
r87: mark(U53(X1,X2,X3)) -> a__U53(mark(X1),X2,X3)
r88: mark(U54(X1,X2,X3)) -> a__U54(mark(X1),X2,X3)
r89: mark(U55(X1,X2)) -> a__U55(mark(X1),X2)
r90: mark(U56(X)) -> a__U56(mark(X))
r91: mark(U61(X1,X2)) -> a__U61(mark(X1),X2)
r92: mark(U62(X1,X2)) -> a__U62(mark(X1),X2)
r93: mark(U63(X)) -> a__U63(mark(X))
r94: mark(U71(X1,X2,X3)) -> a__U71(mark(X1),X2,X3)
r95: mark(U72(X1,X2)) -> a__U72(mark(X1),X2)
r96: mark(U73(X1,X2)) -> a__U73(mark(X1),X2)
r97: mark(isPal(X)) -> a__isPal(X)
r98: mark(U74(X)) -> a__U74(mark(X))
r99: mark(U81(X1,X2)) -> a__U81(mark(X1),X2)
r100: mark(U82(X1,X2)) -> a__U82(mark(X1),X2)
r101: mark(U83(X)) -> a__U83(mark(X))
r102: mark(isNePal(X)) -> a__isNePal(X)
r103: mark(U91(X1,X2)) -> a__U91(mark(X1),X2)
r104: mark(U92(X)) -> a__U92(mark(X))
r105: mark(nil()) -> nil()
r106: mark(tt()) -> tt()
r107: mark(a()) -> a()
r108: mark(e()) -> e()
r109: mark(i()) -> i()
r110: mark(o()) -> o()
r111: mark(u()) -> u()
r112: a____(X1,X2) -> __(X1,X2)
r113: a__U11(X1,X2) -> U11(X1,X2)
r114: a__U12(X1,X2) -> U12(X1,X2)
r115: a__isPalListKind(X) -> isPalListKind(X)
r116: a__U13(X) -> U13(X)
r117: a__isNeList(X) -> isNeList(X)
r118: a__U21(X1,X2,X3) -> U21(X1,X2,X3)
r119: a__U22(X1,X2,X3) -> U22(X1,X2,X3)
r120: a__U23(X1,X2,X3) -> U23(X1,X2,X3)
r121: a__U24(X1,X2,X3) -> U24(X1,X2,X3)
r122: a__U25(X1,X2) -> U25(X1,X2)
r123: a__isList(X) -> isList(X)
r124: a__U26(X) -> U26(X)
r125: a__U31(X1,X2) -> U31(X1,X2)
r126: a__U32(X1,X2) -> U32(X1,X2)
r127: a__U33(X) -> U33(X)
r128: a__isQid(X) -> isQid(X)
r129: a__U41(X1,X2,X3) -> U41(X1,X2,X3)
r130: a__U42(X1,X2,X3) -> U42(X1,X2,X3)
r131: a__U43(X1,X2,X3) -> U43(X1,X2,X3)
r132: a__U44(X1,X2,X3) -> U44(X1,X2,X3)
r133: a__U45(X1,X2) -> U45(X1,X2)
r134: a__U46(X) -> U46(X)
r135: a__U51(X1,X2,X3) -> U51(X1,X2,X3)
r136: a__U52(X1,X2,X3) -> U52(X1,X2,X3)
r137: a__U53(X1,X2,X3) -> U53(X1,X2,X3)
r138: a__U54(X1,X2,X3) -> U54(X1,X2,X3)
r139: a__U55(X1,X2) -> U55(X1,X2)
r140: a__U56(X) -> U56(X)
r141: a__U61(X1,X2) -> U61(X1,X2)
r142: a__U62(X1,X2) -> U62(X1,X2)
r143: a__U63(X) -> U63(X)
r144: a__U71(X1,X2,X3) -> U71(X1,X2,X3)
r145: a__U72(X1,X2) -> U72(X1,X2)
r146: a__U73(X1,X2) -> U73(X1,X2)
r147: a__isPal(X) -> isPal(X)
r148: a__U74(X) -> U74(X)
r149: a__U81(X1,X2) -> U81(X1,X2)
r150: a__U82(X1,X2) -> U82(X1,X2)
r151: a__U83(X) -> U83(X)
r152: a__isNePal(X) -> isNePal(X)
r153: a__U91(X1,X2) -> U91(X1,X2)
r154: a__U92(X) -> U92(X)

The set of usable rules consists of

  r38, r39, r50, r51, r52, r53, r54, r55, r56, r115, r153, r154

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a__isPalListKind#_A(x1) = x1
        ___A(x1,x2) = x1 + x2 + 3
        a__U91#_A(x1,x2) = x1 + x2
        a__isPalListKind_A(x1) = x1 + 1
        tt_A() = 1
        a__U92_A(x1) = x1 + 1
        U92_A(x1) = 0
        a__U91_A(x1,x2) = x1 + x2 + 2
        U91_A(x1,x2) = 0
        a_A() = 1
        e_A() = 1
        i_A() = 1
        nil_A() = 1
        o_A() = 1
        u_A() = 1
        isPalListKind_A(x1) = 0
    
    2. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a__isPalListKind#_A(x1) = 1
        ___A(x1,x2) = x1 + x2 + 1
        a__U91#_A(x1,x2) = 0
        a__isPalListKind_A(x1) = 1
        tt_A() = 4
        a__U92_A(x1) = 3
        U92_A(x1) = 4
        a__U91_A(x1,x2) = 2
        U91_A(x1,x2) = 3
        a_A() = 1
        e_A() = 1
        i_A() = 1
        nil_A() = 1
        o_A() = 1
        u_A() = 1
        isPalListKind_A(x1) = 0
    

The next rules are strictly ordered:

  p1, p2, p3

We remove them from the problem.  Then no dependency pair remains.