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:

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

The next rules are strictly ordered:

  p2, p12, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p28, p29, p30, p31, p32, p33, p34, p35, 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)
p4: mark#(U83(X)) -> mark#(X)
p5: mark#(U82(X1,X2)) -> mark#(X1)
p6: mark#(U81(X1,X2)) -> mark#(X1)
p7: mark#(U74(X)) -> mark#(X)
p8: mark#(U73(X1,X2)) -> mark#(X1)
p9: mark#(U72(X1,X2)) -> mark#(X1)
p10: mark#(U71(X1,X2,X3)) -> mark#(X1)
p11: mark#(U62(X1,X2)) -> mark#(X1)
p12: mark#(U61(X1,X2)) -> mark#(X1)
p13: mark#(U56(X)) -> mark#(X)
p14: mark#(U33(X)) -> mark#(X)
p15: mark#(U13(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, p8, p9, p10, p11, p12, p13, p14, p15}


-- 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:

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

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#(U13(X)) -> mark#(X)
p3: mark#(U33(X)) -> mark#(X)
p4: mark#(U56(X)) -> mark#(X)
p5: mark#(U61(X1,X2)) -> mark#(X1)
p6: mark#(U62(X1,X2)) -> mark#(X1)
p7: mark#(U71(X1,X2,X3)) -> mark#(X1)
p8: mark#(U72(X1,X2)) -> mark#(X1)
p9: mark#(U73(X1,X2)) -> mark#(X1)
p10: mark#(U74(X)) -> mark#(X)
p11: mark#(U81(X1,X2)) -> mark#(X1)
p12: mark#(U82(X1,X2)) -> mark#(X1)
p13: mark#(U83(X)) -> mark#(X)
p14: 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 reduction pair:

  matrix interpretations:
  
    carrier: N^2
    order: lexicographic order
    interpretations:
      mark#_A(x1) = ((1,0),(1,0)) x1
      U92_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      U13_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      U33_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      U56_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      U61_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,1)
      U62_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,1)
      U71_A(x1,x2,x3) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (1,1)
      U72_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,1)
      U73_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,1)
      U74_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      U81_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,1)
      U82_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,1)
      U83_A(x1) = ((1,0),(1,1)) x1 + (1,1)
      U91_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (1,1)

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14

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:

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

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:

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

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:

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

The next rules are strictly ordered:

  p1, p2, p3

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