YES

We show the termination of the TRS R:

  __(__(X,Y),Z) -> __(X,__(Y,Z))
  __(X,nil()) -> X
  __(nil(),X) -> X
  U11(tt(),V) -> U12(isPalListKind(activate(V)),activate(V))
  U12(tt(),V) -> U13(isNeList(activate(V)))
  U13(tt()) -> tt()
  U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
  U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
  U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
  U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2))
  U25(tt(),V2) -> U26(isList(activate(V2)))
  U26(tt()) -> tt()
  U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V))
  U32(tt(),V) -> U33(isQid(activate(V)))
  U33(tt()) -> tt()
  U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
  U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
  U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
  U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2))
  U45(tt(),V2) -> U46(isNeList(activate(V2)))
  U46(tt()) -> tt()
  U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
  U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
  U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
  U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2))
  U55(tt(),V2) -> U56(isList(activate(V2)))
  U56(tt()) -> tt()
  U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V))
  U62(tt(),V) -> U63(isQid(activate(V)))
  U63(tt()) -> tt()
  U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P))
  U72(tt(),P) -> U73(isPal(activate(P)),activate(P))
  U73(tt(),P) -> U74(isPalListKind(activate(P)))
  U74(tt()) -> tt()
  U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V))
  U82(tt(),V) -> U83(isNePal(activate(V)))
  U83(tt()) -> tt()
  U91(tt(),V2) -> U92(isPalListKind(activate(V2)))
  U92(tt()) -> tt()
  isList(V) -> U11(isPalListKind(activate(V)),activate(V))
  isList(n__nil()) -> tt()
  isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2))
  isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
  isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
  isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
  isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
  isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P))
  isPal(V) -> U81(isPalListKind(activate(V)),activate(V))
  isPal(n__nil()) -> tt()
  isPalListKind(n__a()) -> tt()
  isPalListKind(n__e()) -> tt()
  isPalListKind(n__i()) -> tt()
  isPalListKind(n__nil()) -> tt()
  isPalListKind(n__o()) -> tt()
  isPalListKind(n__u()) -> tt()
  isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2))
  isQid(n__a()) -> tt()
  isQid(n__e()) -> tt()
  isQid(n__i()) -> tt()
  isQid(n__o()) -> tt()
  isQid(n__u()) -> tt()
  nil() -> n__nil()
  __(X1,X2) -> n____(X1,X2)
  a() -> n__a()
  e() -> n__e()
  i() -> n__i()
  o() -> n__o()
  u() -> n__u()
  activate(n__nil()) -> nil()
  activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
  activate(n__a()) -> a()
  activate(n__e()) -> e()
  activate(n__i()) -> i()
  activate(n__o()) -> o()
  activate(n__u()) -> u()
  activate(X) -> X

-- SCC decomposition.

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

p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z))
p2: __#(__(X,Y),Z) -> __#(Y,Z)
p3: U11#(tt(),V) -> U12#(isPalListKind(activate(V)),activate(V))
p4: U11#(tt(),V) -> isPalListKind#(activate(V))
p5: U11#(tt(),V) -> activate#(V)
p6: U12#(tt(),V) -> U13#(isNeList(activate(V)))
p7: U12#(tt(),V) -> isNeList#(activate(V))
p8: U12#(tt(),V) -> activate#(V)
p9: U21#(tt(),V1,V2) -> U22#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p10: U21#(tt(),V1,V2) -> isPalListKind#(activate(V1))
p11: U21#(tt(),V1,V2) -> activate#(V1)
p12: U21#(tt(),V1,V2) -> activate#(V2)
p13: U22#(tt(),V1,V2) -> U23#(isPalListKind(activate(V2)),activate(V1),activate(V2))
p14: U22#(tt(),V1,V2) -> isPalListKind#(activate(V2))
p15: U22#(tt(),V1,V2) -> activate#(V2)
p16: U22#(tt(),V1,V2) -> activate#(V1)
p17: U23#(tt(),V1,V2) -> U24#(isPalListKind(activate(V2)),activate(V1),activate(V2))
p18: U23#(tt(),V1,V2) -> isPalListKind#(activate(V2))
p19: U23#(tt(),V1,V2) -> activate#(V2)
p20: U23#(tt(),V1,V2) -> activate#(V1)
p21: U24#(tt(),V1,V2) -> U25#(isList(activate(V1)),activate(V2))
p22: U24#(tt(),V1,V2) -> isList#(activate(V1))
p23: U24#(tt(),V1,V2) -> activate#(V1)
p24: U24#(tt(),V1,V2) -> activate#(V2)
p25: U25#(tt(),V2) -> U26#(isList(activate(V2)))
p26: U25#(tt(),V2) -> isList#(activate(V2))
p27: U25#(tt(),V2) -> activate#(V2)
p28: U31#(tt(),V) -> U32#(isPalListKind(activate(V)),activate(V))
p29: U31#(tt(),V) -> isPalListKind#(activate(V))
p30: U31#(tt(),V) -> activate#(V)
p31: U32#(tt(),V) -> U33#(isQid(activate(V)))
p32: U32#(tt(),V) -> isQid#(activate(V))
p33: U32#(tt(),V) -> activate#(V)
p34: U41#(tt(),V1,V2) -> U42#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p35: U41#(tt(),V1,V2) -> isPalListKind#(activate(V1))
p36: U41#(tt(),V1,V2) -> activate#(V1)
p37: U41#(tt(),V1,V2) -> activate#(V2)
p38: U42#(tt(),V1,V2) -> U43#(isPalListKind(activate(V2)),activate(V1),activate(V2))
p39: U42#(tt(),V1,V2) -> isPalListKind#(activate(V2))
p40: U42#(tt(),V1,V2) -> activate#(V2)
p41: U42#(tt(),V1,V2) -> activate#(V1)
p42: U43#(tt(),V1,V2) -> U44#(isPalListKind(activate(V2)),activate(V1),activate(V2))
p43: U43#(tt(),V1,V2) -> isPalListKind#(activate(V2))
p44: U43#(tt(),V1,V2) -> activate#(V2)
p45: U43#(tt(),V1,V2) -> activate#(V1)
p46: U44#(tt(),V1,V2) -> U45#(isList(activate(V1)),activate(V2))
p47: U44#(tt(),V1,V2) -> isList#(activate(V1))
p48: U44#(tt(),V1,V2) -> activate#(V1)
p49: U44#(tt(),V1,V2) -> activate#(V2)
p50: U45#(tt(),V2) -> U46#(isNeList(activate(V2)))
p51: U45#(tt(),V2) -> isNeList#(activate(V2))
p52: U45#(tt(),V2) -> activate#(V2)
p53: U51#(tt(),V1,V2) -> U52#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p54: U51#(tt(),V1,V2) -> isPalListKind#(activate(V1))
p55: U51#(tt(),V1,V2) -> activate#(V1)
p56: U51#(tt(),V1,V2) -> activate#(V2)
p57: U52#(tt(),V1,V2) -> U53#(isPalListKind(activate(V2)),activate(V1),activate(V2))
p58: U52#(tt(),V1,V2) -> isPalListKind#(activate(V2))
p59: U52#(tt(),V1,V2) -> activate#(V2)
p60: U52#(tt(),V1,V2) -> activate#(V1)
p61: U53#(tt(),V1,V2) -> U54#(isPalListKind(activate(V2)),activate(V1),activate(V2))
p62: U53#(tt(),V1,V2) -> isPalListKind#(activate(V2))
p63: U53#(tt(),V1,V2) -> activate#(V2)
p64: U53#(tt(),V1,V2) -> activate#(V1)
p65: U54#(tt(),V1,V2) -> U55#(isNeList(activate(V1)),activate(V2))
p66: U54#(tt(),V1,V2) -> isNeList#(activate(V1))
p67: U54#(tt(),V1,V2) -> activate#(V1)
p68: U54#(tt(),V1,V2) -> activate#(V2)
p69: U55#(tt(),V2) -> U56#(isList(activate(V2)))
p70: U55#(tt(),V2) -> isList#(activate(V2))
p71: U55#(tt(),V2) -> activate#(V2)
p72: U61#(tt(),V) -> U62#(isPalListKind(activate(V)),activate(V))
p73: U61#(tt(),V) -> isPalListKind#(activate(V))
p74: U61#(tt(),V) -> activate#(V)
p75: U62#(tt(),V) -> U63#(isQid(activate(V)))
p76: U62#(tt(),V) -> isQid#(activate(V))
p77: U62#(tt(),V) -> activate#(V)
p78: U71#(tt(),I,P) -> U72#(isPalListKind(activate(I)),activate(P))
p79: U71#(tt(),I,P) -> isPalListKind#(activate(I))
p80: U71#(tt(),I,P) -> activate#(I)
p81: U71#(tt(),I,P) -> activate#(P)
p82: U72#(tt(),P) -> U73#(isPal(activate(P)),activate(P))
p83: U72#(tt(),P) -> isPal#(activate(P))
p84: U72#(tt(),P) -> activate#(P)
p85: U73#(tt(),P) -> U74#(isPalListKind(activate(P)))
p86: U73#(tt(),P) -> isPalListKind#(activate(P))
p87: U73#(tt(),P) -> activate#(P)
p88: U81#(tt(),V) -> U82#(isPalListKind(activate(V)),activate(V))
p89: U81#(tt(),V) -> isPalListKind#(activate(V))
p90: U81#(tt(),V) -> activate#(V)
p91: U82#(tt(),V) -> U83#(isNePal(activate(V)))
p92: U82#(tt(),V) -> isNePal#(activate(V))
p93: U82#(tt(),V) -> activate#(V)
p94: U91#(tt(),V2) -> U92#(isPalListKind(activate(V2)))
p95: U91#(tt(),V2) -> isPalListKind#(activate(V2))
p96: U91#(tt(),V2) -> activate#(V2)
p97: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V))
p98: isList#(V) -> isPalListKind#(activate(V))
p99: isList#(V) -> activate#(V)
p100: isList#(n____(V1,V2)) -> U21#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p101: isList#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p102: isList#(n____(V1,V2)) -> activate#(V1)
p103: isList#(n____(V1,V2)) -> activate#(V2)
p104: isNeList#(V) -> U31#(isPalListKind(activate(V)),activate(V))
p105: isNeList#(V) -> isPalListKind#(activate(V))
p106: isNeList#(V) -> activate#(V)
p107: isNeList#(n____(V1,V2)) -> U41#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p108: isNeList#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p109: isNeList#(n____(V1,V2)) -> activate#(V1)
p110: isNeList#(n____(V1,V2)) -> activate#(V2)
p111: isNeList#(n____(V1,V2)) -> U51#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p112: isNeList#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p113: isNeList#(n____(V1,V2)) -> activate#(V1)
p114: isNeList#(n____(V1,V2)) -> activate#(V2)
p115: isNePal#(V) -> U61#(isPalListKind(activate(V)),activate(V))
p116: isNePal#(V) -> isPalListKind#(activate(V))
p117: isNePal#(V) -> activate#(V)
p118: isNePal#(n____(I,n____(P,I))) -> U71#(isQid(activate(I)),activate(I),activate(P))
p119: isNePal#(n____(I,n____(P,I))) -> isQid#(activate(I))
p120: isNePal#(n____(I,n____(P,I))) -> activate#(I)
p121: isNePal#(n____(I,n____(P,I))) -> activate#(P)
p122: isPal#(V) -> U81#(isPalListKind(activate(V)),activate(V))
p123: isPal#(V) -> isPalListKind#(activate(V))
p124: isPal#(V) -> activate#(V)
p125: isPalListKind#(n____(V1,V2)) -> U91#(isPalListKind(activate(V1)),activate(V2))
p126: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p127: isPalListKind#(n____(V1,V2)) -> activate#(V1)
p128: isPalListKind#(n____(V1,V2)) -> activate#(V2)
p129: activate#(n__nil()) -> nil#()
p130: activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2))
p131: activate#(n____(X1,X2)) -> activate#(X1)
p132: activate#(n____(X1,X2)) -> activate#(X2)
p133: activate#(n__a()) -> a#()
p134: activate#(n__e()) -> e#()
p135: activate#(n__i()) -> i#()
p136: activate#(n__o()) -> o#()
p137: activate#(n__u()) -> u#()

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isPalListKind(activate(V)),activate(V))
r5: U12(tt(),V) -> U13(isNeList(activate(V)))
r6: U13(tt()) -> tt()
r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2))
r11: U25(tt(),V2) -> U26(isList(activate(V2)))
r12: U26(tt()) -> tt()
r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V))
r14: U32(tt(),V) -> U33(isQid(activate(V)))
r15: U33(tt()) -> tt()
r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2))
r20: U45(tt(),V2) -> U46(isNeList(activate(V2)))
r21: U46(tt()) -> tt()
r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2))
r26: U55(tt(),V2) -> U56(isList(activate(V2)))
r27: U56(tt()) -> tt()
r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V))
r29: U62(tt(),V) -> U63(isQid(activate(V)))
r30: U63(tt()) -> tt()
r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P))
r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P))
r33: U73(tt(),P) -> U74(isPalListKind(activate(P)))
r34: U74(tt()) -> tt()
r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V))
r36: U82(tt(),V) -> U83(isNePal(activate(V)))
r37: U83(tt()) -> tt()
r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2)))
r39: U92(tt()) -> tt()
r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r41: isList(n__nil()) -> tt()
r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2))
r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r47: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P))
r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V))
r49: isPal(n__nil()) -> tt()
r50: isPalListKind(n__a()) -> tt()
r51: isPalListKind(n__e()) -> tt()
r52: isPalListKind(n__i()) -> tt()
r53: isPalListKind(n__nil()) -> tt()
r54: isPalListKind(n__o()) -> tt()
r55: isPalListKind(n__u()) -> tt()
r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2))
r57: isQid(n__a()) -> tt()
r58: isQid(n__e()) -> tt()
r59: isQid(n__i()) -> tt()
r60: isQid(n__o()) -> tt()
r61: isQid(n__u()) -> tt()
r62: nil() -> n__nil()
r63: __(X1,X2) -> n____(X1,X2)
r64: a() -> n__a()
r65: e() -> n__e()
r66: i() -> n__i()
r67: o() -> n__o()
r68: u() -> n__u()
r69: activate(n__nil()) -> nil()
r70: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r71: activate(n__a()) -> a()
r72: activate(n__e()) -> e()
r73: activate(n__i()) -> i()
r74: activate(n__o()) -> o()
r75: activate(n__u()) -> u()
r76: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p78, p83, p88, p92, p118, p122}
  {p3, p7, p9, p13, p17, p21, p22, p26, p34, p38, p42, p46, p47, p51, p53, p57, p61, p65, p66, p70, p97, p100, p107, p111}
  {p95, p125, p126}
  {p131, p132}
  {p1, p2}


-- Reduction pair.

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

p1: U82#(tt(),V) -> isNePal#(activate(V))
p2: isNePal#(n____(I,n____(P,I))) -> U71#(isQid(activate(I)),activate(I),activate(P))
p3: U71#(tt(),I,P) -> U72#(isPalListKind(activate(I)),activate(P))
p4: U72#(tt(),P) -> isPal#(activate(P))
p5: isPal#(V) -> U81#(isPalListKind(activate(V)),activate(V))
p6: U81#(tt(),V) -> U82#(isPalListKind(activate(V)),activate(V))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isPalListKind(activate(V)),activate(V))
r5: U12(tt(),V) -> U13(isNeList(activate(V)))
r6: U13(tt()) -> tt()
r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2))
r11: U25(tt(),V2) -> U26(isList(activate(V2)))
r12: U26(tt()) -> tt()
r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V))
r14: U32(tt(),V) -> U33(isQid(activate(V)))
r15: U33(tt()) -> tt()
r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2))
r20: U45(tt(),V2) -> U46(isNeList(activate(V2)))
r21: U46(tt()) -> tt()
r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2))
r26: U55(tt(),V2) -> U56(isList(activate(V2)))
r27: U56(tt()) -> tt()
r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V))
r29: U62(tt(),V) -> U63(isQid(activate(V)))
r30: U63(tt()) -> tt()
r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P))
r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P))
r33: U73(tt(),P) -> U74(isPalListKind(activate(P)))
r34: U74(tt()) -> tt()
r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V))
r36: U82(tt(),V) -> U83(isNePal(activate(V)))
r37: U83(tt()) -> tt()
r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2)))
r39: U92(tt()) -> tt()
r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r41: isList(n__nil()) -> tt()
r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2))
r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r47: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P))
r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V))
r49: isPal(n__nil()) -> tt()
r50: isPalListKind(n__a()) -> tt()
r51: isPalListKind(n__e()) -> tt()
r52: isPalListKind(n__i()) -> tt()
r53: isPalListKind(n__nil()) -> tt()
r54: isPalListKind(n__o()) -> tt()
r55: isPalListKind(n__u()) -> tt()
r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2))
r57: isQid(n__a()) -> tt()
r58: isQid(n__e()) -> tt()
r59: isQid(n__i()) -> tt()
r60: isQid(n__o()) -> tt()
r61: isQid(n__u()) -> tt()
r62: nil() -> n__nil()
r63: __(X1,X2) -> n____(X1,X2)
r64: a() -> n__a()
r65: e() -> n__e()
r66: i() -> n__i()
r67: o() -> n__o()
r68: u() -> n__u()
r69: activate(n__nil()) -> nil()
r70: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r71: activate(n__a()) -> a()
r72: activate(n__e()) -> e()
r73: activate(n__i()) -> i()
r74: activate(n__o()) -> o()
r75: activate(n__u()) -> u()
r76: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r38, r39, 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        U82#_A(x1,x2) = ((0,1),(1,0)) x2 + (3,0)
        tt_A() = (1,7)
        isNePal#_A(x1) = ((0,1),(1,0)) x1 + (2,0)
        activate_A(x1) = x1
        n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (1,0)
        U71#_A(x1,x2,x3) = ((0,1),(1,0)) x1 + ((0,1),(1,0)) x3
        isQid_A(x1) = ((1,0),(1,0)) x1 + (1,1)
        U72#_A(x1,x2) = ((0,1),(1,0)) x2 + (6,0)
        isPalListKind_A(x1) = ((0,1),(0,0)) x1 + (4,7)
        isPal#_A(x1) = ((0,1),(1,0)) x1 + (5,0)
        U81#_A(x1,x2) = ((0,1),(1,0)) x2 + (4,0)
        U92_A(x1) = (2,7)
        ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (1,0)
        nil_A() = (1,1)
        U91_A(x1,x2) = (3,7)
        n__nil_A() = (1,1)
        a_A() = (6,1)
        n__a_A() = (6,1)
        e_A() = (6,1)
        n__e_A() = (6,1)
        i_A() = (6,1)
        n__i_A() = (6,1)
        o_A() = (6,1)
        n__o_A() = (6,1)
        u_A() = (6,1)
        n__u_A() = (6,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        U82#_A(x1,x2) = (3,3)
        tt_A() = (1,4)
        isNePal#_A(x1) = (2,0)
        activate_A(x1) = ((1,1),(1,1)) x1 + (2,1)
        n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (3,5)
        U71#_A(x1,x2,x3) = (1,0)
        isQid_A(x1) = ((0,0),(1,1)) x1 + (2,3)
        U72#_A(x1,x2) = (0,0)
        isPalListKind_A(x1) = (2,1)
        isPal#_A(x1) = (1,1)
        U81#_A(x1,x2) = (4,2)
        U92_A(x1) = (2,3)
        ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (4,5)
        nil_A() = (1,1)
        U91_A(x1,x2) = (3,2)
        n__nil_A() = (0,0)
        a_A() = (1,1)
        n__a_A() = (0,0)
        e_A() = (1,1)
        n__e_A() = (0,0)
        i_A() = (2,1)
        n__i_A() = (0,0)
        o_A() = (2,1)
        n__o_A() = (0,0)
        u_A() = (1,1)
        n__u_A() = (0,0)
    

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: U52#(tt(),V1,V2) -> U53#(isPalListKind(activate(V2)),activate(V1),activate(V2))
p2: U53#(tt(),V1,V2) -> U54#(isPalListKind(activate(V2)),activate(V1),activate(V2))
p3: U54#(tt(),V1,V2) -> isNeList#(activate(V1))
p4: isNeList#(n____(V1,V2)) -> U51#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p5: U51#(tt(),V1,V2) -> U52#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p6: isNeList#(n____(V1,V2)) -> U41#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p7: U41#(tt(),V1,V2) -> U42#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p8: U42#(tt(),V1,V2) -> U43#(isPalListKind(activate(V2)),activate(V1),activate(V2))
p9: U43#(tt(),V1,V2) -> U44#(isPalListKind(activate(V2)),activate(V1),activate(V2))
p10: U44#(tt(),V1,V2) -> isList#(activate(V1))
p11: isList#(n____(V1,V2)) -> U21#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p12: U21#(tt(),V1,V2) -> U22#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p13: U22#(tt(),V1,V2) -> U23#(isPalListKind(activate(V2)),activate(V1),activate(V2))
p14: U23#(tt(),V1,V2) -> U24#(isPalListKind(activate(V2)),activate(V1),activate(V2))
p15: U24#(tt(),V1,V2) -> isList#(activate(V1))
p16: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V))
p17: U11#(tt(),V) -> U12#(isPalListKind(activate(V)),activate(V))
p18: U12#(tt(),V) -> isNeList#(activate(V))
p19: U24#(tt(),V1,V2) -> U25#(isList(activate(V1)),activate(V2))
p20: U25#(tt(),V2) -> isList#(activate(V2))
p21: U44#(tt(),V1,V2) -> U45#(isList(activate(V1)),activate(V2))
p22: U45#(tt(),V2) -> isNeList#(activate(V2))
p23: U54#(tt(),V1,V2) -> U55#(isNeList(activate(V1)),activate(V2))
p24: U55#(tt(),V2) -> isList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isPalListKind(activate(V)),activate(V))
r5: U12(tt(),V) -> U13(isNeList(activate(V)))
r6: U13(tt()) -> tt()
r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2))
r11: U25(tt(),V2) -> U26(isList(activate(V2)))
r12: U26(tt()) -> tt()
r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V))
r14: U32(tt(),V) -> U33(isQid(activate(V)))
r15: U33(tt()) -> tt()
r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2))
r20: U45(tt(),V2) -> U46(isNeList(activate(V2)))
r21: U46(tt()) -> tt()
r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2))
r26: U55(tt(),V2) -> U56(isList(activate(V2)))
r27: U56(tt()) -> tt()
r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V))
r29: U62(tt(),V) -> U63(isQid(activate(V)))
r30: U63(tt()) -> tt()
r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P))
r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P))
r33: U73(tt(),P) -> U74(isPalListKind(activate(P)))
r34: U74(tt()) -> tt()
r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V))
r36: U82(tt(),V) -> U83(isNePal(activate(V)))
r37: U83(tt()) -> tt()
r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2)))
r39: U92(tt()) -> tt()
r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r41: isList(n__nil()) -> tt()
r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2))
r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r47: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P))
r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V))
r49: isPal(n__nil()) -> tt()
r50: isPalListKind(n__a()) -> tt()
r51: isPalListKind(n__e()) -> tt()
r52: isPalListKind(n__i()) -> tt()
r53: isPalListKind(n__nil()) -> tt()
r54: isPalListKind(n__o()) -> tt()
r55: isPalListKind(n__u()) -> tt()
r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2))
r57: isQid(n__a()) -> tt()
r58: isQid(n__e()) -> tt()
r59: isQid(n__i()) -> tt()
r60: isQid(n__o()) -> tt()
r61: isQid(n__u()) -> tt()
r62: nil() -> n__nil()
r63: __(X1,X2) -> n____(X1,X2)
r64: a() -> n__a()
r65: e() -> n__e()
r66: i() -> n__i()
r67: o() -> n__o()
r68: u() -> n__u()
r69: activate(n__nil()) -> nil()
r70: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r71: activate(n__a()) -> a()
r72: activate(n__e()) -> e()
r73: activate(n__i()) -> i()
r74: activate(n__o()) -> o()
r75: activate(n__u()) -> u()
r76: activate(X) -> 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, r38, r39, r40, r41, r42, r43, r44, r45, 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        U52#_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (7,0)
        tt_A() = (1,1)
        U53#_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (6,0)
        isPalListKind_A(x1) = ((1,1),(0,0)) x1 + (0,1)
        activate_A(x1) = ((1,1),(0,1)) x1 + (9,0)
        U54#_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (5,0)
        isNeList#_A(x1) = ((0,1),(0,0)) x1
        n_____A(x1,x2) = x1 + x2 + (4,9)
        U51#_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (8,0)
        U41#_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (7,0)
        U42#_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (6,0)
        U43#_A(x1,x2,x3) = ((0,1),(0,0)) x1 + ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (4,0)
        U44#_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (4,0)
        isList#_A(x1) = ((0,1),(0,0)) x1 + (3,0)
        U21#_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (12,0)
        U22#_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (12,0)
        U23#_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (3,0)
        U24#_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (3,0)
        U11#_A(x1,x2) = ((0,1),(0,0)) x2 + (2,0)
        U12#_A(x1,x2) = ((0,1),(0,0)) x2 + (1,0)
        U25#_A(x1,x2) = ((0,1),(0,0)) x2 + (3,0)
        isList_A(x1) = ((0,1),(1,0)) x1 + (5,1)
        U45#_A(x1,x2) = ((0,1),(0,0)) x2 + (1,0)
        U55#_A(x1,x2) = ((0,1),(0,0)) x2 + (4,0)
        isNeList_A(x1) = ((0,1),(0,0)) x1 + (5,1)
        U26_A(x1) = (2,1)
        U46_A(x1) = (2,1)
        U56_A(x1) = (2,1)
        U25_A(x1,x2) = (3,1)
        U45_A(x1,x2) = (3,1)
        U55_A(x1,x2) = (3,1)
        U24_A(x1,x2,x3) = (4,1)
        U44_A(x1,x2,x3) = (4,1)
        U54_A(x1,x2,x3) = (4,1)
        U13_A(x1) = (2,1)
        U23_A(x1,x2,x3) = (5,1)
        U33_A(x1) = (2,1)
        U43_A(x1,x2,x3) = (5,1)
        U53_A(x1,x2,x3) = (5,1)
        isQid_A(x1) = ((0,0),(1,0)) x1 + (2,0)
        n__a_A() = (1,1)
        n__e_A() = (1,1)
        n__i_A() = (1,1)
        n__o_A() = (1,1)
        n__u_A() = (1,1)
        U12_A(x1,x2) = (3,1)
        U22_A(x1,x2,x3) = ((0,1),(0,0)) x2 + (6,1)
        U32_A(x1,x2) = x1 + (3,0)
        U42_A(x1,x2,x3) = (6,1)
        U52_A(x1,x2,x3) = (6,1)
        U92_A(x1) = (2,1)
        ___A(x1,x2) = x1 + x2 + (4,9)
        nil_A() = (1,1)
        U11_A(x1,x2) = (4,1)
        U21_A(x1,x2,x3) = ((0,1),(0,0)) x2 + ((0,1),(0,0)) x3 + (7,1)
        U31_A(x1,x2) = x1 + (4,0)
        U41_A(x1,x2,x3) = ((0,1),(0,0)) x2 + (7,1)
        U51_A(x1,x2,x3) = (7,1)
        U91_A(x1,x2) = x2 + (3,1)
        n__nil_A() = (1,1)
        a_A() = (11,1)
        e_A() = (2,1)
        i_A() = (2,1)
        o_A() = (2,1)
        u_A() = (11,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        U52#_A(x1,x2,x3) = (8,7)
        tt_A() = (6,8)
        U53#_A(x1,x2,x3) = (0,8)
        isPalListKind_A(x1) = ((1,0),(1,0)) x1
        activate_A(x1) = ((1,1),(1,1)) x1 + (2,1)
        U54#_A(x1,x2,x3) = (1,0)
        isNeList#_A(x1) = (6,5)
        n_____A(x1,x2) = x1
        U51#_A(x1,x2,x3) = (7,6)
        U41#_A(x1,x2,x3) = (7,6)
        U42#_A(x1,x2,x3) = (0,7)
        U43#_A(x1,x2,x3) = (1,8)
        U44#_A(x1,x2,x3) = (4,9)
        isList#_A(x1) = (3,2)
        U21#_A(x1,x2,x3) = (3,0)
        U22#_A(x1,x2,x3) = (3,0)
        U23#_A(x1,x2,x3) = (3,2)
        U24#_A(x1,x2,x3) = (3,2)
        U11#_A(x1,x2) = (4,3)
        U12#_A(x1,x2) = (5,4)
        U25#_A(x1,x2) = (3,2)
        isList_A(x1) = (7,1)
        U45#_A(x1,x2) = (5,10)
        U55#_A(x1,x2) = (2,1)
        isNeList_A(x1) = (1,1)
        U26_A(x1) = (3,7)
        U46_A(x1) = (5,7)
        U56_A(x1) = (2,7)
        U25_A(x1,x2) = (2,6)
        U45_A(x1,x2) = (4,6)
        U55_A(x1,x2) = (1,6)
        U24_A(x1,x2,x3) = (1,5)
        U44_A(x1,x2,x3) = (3,5)
        U54_A(x1,x2,x3) = (0,5)
        U13_A(x1) = (7,4)
        U23_A(x1,x2,x3) = (0,4)
        U33_A(x1) = (0,4)
        U43_A(x1,x2,x3) = (2,4)
        U53_A(x1,x2,x3) = (4,4)
        isQid_A(x1) = (6,1)
        n__a_A() = (7,1)
        n__e_A() = (1,1)
        n__i_A() = (1,1)
        n__o_A() = (8,1)
        n__u_A() = (1,1)
        U12_A(x1,x2) = (0,3)
        U22_A(x1,x2,x3) = (9,3)
        U32_A(x1,x2) = (1,3)
        U42_A(x1,x2,x3) = (1,3)
        U52_A(x1,x2,x3) = (3,3)
        U92_A(x1) = (0,2)
        ___A(x1,x2) = x1
        nil_A() = (1,1)
        U11_A(x1,x2) = (1,2)
        U21_A(x1,x2,x3) = (8,2)
        U31_A(x1,x2) = (0,2)
        U41_A(x1,x2,x3) = (0,2)
        U51_A(x1,x2,x3) = (2,2)
        U91_A(x1,x2) = (1,1)
        n__nil_A() = (0,0)
        a_A() = (6,1)
        e_A() = (5,0)
        i_A() = (5,0)
        o_A() = (12,11)
        u_A() = (2,3)
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p13, p16, p17, p18, p21, p22, p23, p24

We remove them from the problem.

-- SCC decomposition.

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

p1: isList#(n____(V1,V2)) -> U21#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p2: U21#(tt(),V1,V2) -> U22#(isPalListKind(activate(V1)),activate(V1),activate(V2))
p3: U23#(tt(),V1,V2) -> U24#(isPalListKind(activate(V2)),activate(V1),activate(V2))
p4: U24#(tt(),V1,V2) -> isList#(activate(V1))
p5: U24#(tt(),V1,V2) -> U25#(isList(activate(V1)),activate(V2))
p6: U25#(tt(),V2) -> isList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isPalListKind(activate(V)),activate(V))
r5: U12(tt(),V) -> U13(isNeList(activate(V)))
r6: U13(tt()) -> tt()
r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2))
r11: U25(tt(),V2) -> U26(isList(activate(V2)))
r12: U26(tt()) -> tt()
r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V))
r14: U32(tt(),V) -> U33(isQid(activate(V)))
r15: U33(tt()) -> tt()
r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2))
r20: U45(tt(),V2) -> U46(isNeList(activate(V2)))
r21: U46(tt()) -> tt()
r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2))
r26: U55(tt(),V2) -> U56(isList(activate(V2)))
r27: U56(tt()) -> tt()
r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V))
r29: U62(tt(),V) -> U63(isQid(activate(V)))
r30: U63(tt()) -> tt()
r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P))
r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P))
r33: U73(tt(),P) -> U74(isPalListKind(activate(P)))
r34: U74(tt()) -> tt()
r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V))
r36: U82(tt(),V) -> U83(isNePal(activate(V)))
r37: U83(tt()) -> tt()
r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2)))
r39: U92(tt()) -> tt()
r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r41: isList(n__nil()) -> tt()
r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2))
r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r47: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P))
r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V))
r49: isPal(n__nil()) -> tt()
r50: isPalListKind(n__a()) -> tt()
r51: isPalListKind(n__e()) -> tt()
r52: isPalListKind(n__i()) -> tt()
r53: isPalListKind(n__nil()) -> tt()
r54: isPalListKind(n__o()) -> tt()
r55: isPalListKind(n__u()) -> tt()
r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2))
r57: isQid(n__a()) -> tt()
r58: isQid(n__e()) -> tt()
r59: isQid(n__i()) -> tt()
r60: isQid(n__o()) -> tt()
r61: isQid(n__u()) -> tt()
r62: nil() -> n__nil()
r63: __(X1,X2) -> n____(X1,X2)
r64: a() -> n__a()
r65: e() -> n__e()
r66: i() -> n__i()
r67: o() -> n__o()
r68: u() -> n__u()
r69: activate(n__nil()) -> nil()
r70: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r71: activate(n__a()) -> a()
r72: activate(n__e()) -> e()
r73: activate(n__i()) -> i()
r74: activate(n__o()) -> o()
r75: activate(n__u()) -> u()
r76: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  (no SCCs)

-- Reduction pair.

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

p1: isPalListKind#(n____(V1,V2)) -> U91#(isPalListKind(activate(V1)),activate(V2))
p2: U91#(tt(),V2) -> isPalListKind#(activate(V2))
p3: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isPalListKind(activate(V)),activate(V))
r5: U12(tt(),V) -> U13(isNeList(activate(V)))
r6: U13(tt()) -> tt()
r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2))
r11: U25(tt(),V2) -> U26(isList(activate(V2)))
r12: U26(tt()) -> tt()
r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V))
r14: U32(tt(),V) -> U33(isQid(activate(V)))
r15: U33(tt()) -> tt()
r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2))
r20: U45(tt(),V2) -> U46(isNeList(activate(V2)))
r21: U46(tt()) -> tt()
r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2))
r26: U55(tt(),V2) -> U56(isList(activate(V2)))
r27: U56(tt()) -> tt()
r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V))
r29: U62(tt(),V) -> U63(isQid(activate(V)))
r30: U63(tt()) -> tt()
r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P))
r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P))
r33: U73(tt(),P) -> U74(isPalListKind(activate(P)))
r34: U74(tt()) -> tt()
r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V))
r36: U82(tt(),V) -> U83(isNePal(activate(V)))
r37: U83(tt()) -> tt()
r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2)))
r39: U92(tt()) -> tt()
r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r41: isList(n__nil()) -> tt()
r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2))
r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r47: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P))
r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V))
r49: isPal(n__nil()) -> tt()
r50: isPalListKind(n__a()) -> tt()
r51: isPalListKind(n__e()) -> tt()
r52: isPalListKind(n__i()) -> tt()
r53: isPalListKind(n__nil()) -> tt()
r54: isPalListKind(n__o()) -> tt()
r55: isPalListKind(n__u()) -> tt()
r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2))
r57: isQid(n__a()) -> tt()
r58: isQid(n__e()) -> tt()
r59: isQid(n__i()) -> tt()
r60: isQid(n__o()) -> tt()
r61: isQid(n__u()) -> tt()
r62: nil() -> n__nil()
r63: __(X1,X2) -> n____(X1,X2)
r64: a() -> n__a()
r65: e() -> n__e()
r66: i() -> n__i()
r67: o() -> n__o()
r68: u() -> n__u()
r69: activate(n__nil()) -> nil()
r70: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r71: activate(n__a()) -> a()
r72: activate(n__e()) -> e()
r73: activate(n__i()) -> i()
r74: activate(n__o()) -> o()
r75: activate(n__u()) -> u()
r76: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r38, r39, r50, r51, r52, r53, r54, r55, r56, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        isPalListKind#_A(x1) = ((0,1),(0,0)) x1
        n_____A(x1,x2) = x1 + x2 + (2,2)
        U91#_A(x1,x2) = ((0,1),(0,0)) x2 + (1,0)
        isPalListKind_A(x1) = x1 + (2,1)
        activate_A(x1) = ((1,1),(0,1)) x1 + (1,0)
        tt_A() = (1,1)
        U92_A(x1) = (2,1)
        ___A(x1,x2) = x1 + x2 + (3,2)
        nil_A() = (2,1)
        U91_A(x1,x2) = x1 + (3,0)
        n__nil_A() = (1,1)
        a_A() = (1,1)
        n__a_A() = (0,1)
        e_A() = (2,1)
        n__e_A() = (1,1)
        i_A() = (1,1)
        n__i_A() = (0,1)
        o_A() = (0,1)
        n__o_A() = (0,1)
        u_A() = (1,1)
        n__u_A() = (0,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        isPalListKind#_A(x1) = (1,1)
        n_____A(x1,x2) = x1 + (1,2)
        U91#_A(x1,x2) = (0,0)
        isPalListKind_A(x1) = x1
        activate_A(x1) = ((1,1),(0,1)) x1 + (1,1)
        tt_A() = (2,5)
        U92_A(x1) = (1,4)
        ___A(x1,x2) = x1 + (2,1)
        nil_A() = (5,1)
        U91_A(x1,x2) = (0,3)
        n__nil_A() = (1,2)
        a_A() = (0,2)
        n__a_A() = (1,0)
        e_A() = (4,0)
        n__e_A() = (1,1)
        i_A() = (4,3)
        n__i_A() = (1,1)
        o_A() = (3,0)
        n__o_A() = (1,0)
        u_A() = (0,0)
        n__u_A() = (1,1)
    

The next rules are strictly ordered:

  p1, p2, p3

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: activate#(n____(X1,X2)) -> activate#(X2)
p2: activate#(n____(X1,X2)) -> activate#(X1)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isPalListKind(activate(V)),activate(V))
r5: U12(tt(),V) -> U13(isNeList(activate(V)))
r6: U13(tt()) -> tt()
r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2))
r11: U25(tt(),V2) -> U26(isList(activate(V2)))
r12: U26(tt()) -> tt()
r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V))
r14: U32(tt(),V) -> U33(isQid(activate(V)))
r15: U33(tt()) -> tt()
r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2))
r20: U45(tt(),V2) -> U46(isNeList(activate(V2)))
r21: U46(tt()) -> tt()
r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2))
r26: U55(tt(),V2) -> U56(isList(activate(V2)))
r27: U56(tt()) -> tt()
r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V))
r29: U62(tt(),V) -> U63(isQid(activate(V)))
r30: U63(tt()) -> tt()
r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P))
r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P))
r33: U73(tt(),P) -> U74(isPalListKind(activate(P)))
r34: U74(tt()) -> tt()
r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V))
r36: U82(tt(),V) -> U83(isNePal(activate(V)))
r37: U83(tt()) -> tt()
r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2)))
r39: U92(tt()) -> tt()
r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r41: isList(n__nil()) -> tt()
r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2))
r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r47: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P))
r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V))
r49: isPal(n__nil()) -> tt()
r50: isPalListKind(n__a()) -> tt()
r51: isPalListKind(n__e()) -> tt()
r52: isPalListKind(n__i()) -> tt()
r53: isPalListKind(n__nil()) -> tt()
r54: isPalListKind(n__o()) -> tt()
r55: isPalListKind(n__u()) -> tt()
r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2))
r57: isQid(n__a()) -> tt()
r58: isQid(n__e()) -> tt()
r59: isQid(n__i()) -> tt()
r60: isQid(n__o()) -> tt()
r61: isQid(n__u()) -> tt()
r62: nil() -> n__nil()
r63: __(X1,X2) -> n____(X1,X2)
r64: a() -> n__a()
r65: e() -> n__e()
r66: i() -> n__i()
r67: o() -> n__o()
r68: u() -> n__u()
r69: activate(n__nil()) -> nil()
r70: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r71: activate(n__a()) -> a()
r72: activate(n__e()) -> e()
r73: activate(n__i()) -> i()
r74: activate(n__o()) -> o()
r75: activate(n__u()) -> u()
r76: activate(X) -> 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^2
      order: standard order
      interpretations:
        activate#_A(x1) = ((1,1),(1,1)) x1
        n_____A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (1,1)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        activate#_A(x1) = ((1,1),(1,0)) x1
        n_____A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,0)) x2 + (1,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

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: __#(__(X,Y),Z) -> __#(X,__(Y,Z))
p2: __#(__(X,Y),Z) -> __#(Y,Z)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isPalListKind(activate(V)),activate(V))
r5: U12(tt(),V) -> U13(isNeList(activate(V)))
r6: U13(tt()) -> tt()
r7: U21(tt(),V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
r8: U22(tt(),V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
r9: U23(tt(),V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
r10: U24(tt(),V1,V2) -> U25(isList(activate(V1)),activate(V2))
r11: U25(tt(),V2) -> U26(isList(activate(V2)))
r12: U26(tt()) -> tt()
r13: U31(tt(),V) -> U32(isPalListKind(activate(V)),activate(V))
r14: U32(tt(),V) -> U33(isQid(activate(V)))
r15: U33(tt()) -> tt()
r16: U41(tt(),V1,V2) -> U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
r17: U42(tt(),V1,V2) -> U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
r18: U43(tt(),V1,V2) -> U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
r19: U44(tt(),V1,V2) -> U45(isList(activate(V1)),activate(V2))
r20: U45(tt(),V2) -> U46(isNeList(activate(V2)))
r21: U46(tt()) -> tt()
r22: U51(tt(),V1,V2) -> U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
r23: U52(tt(),V1,V2) -> U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
r24: U53(tt(),V1,V2) -> U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
r25: U54(tt(),V1,V2) -> U55(isNeList(activate(V1)),activate(V2))
r26: U55(tt(),V2) -> U56(isList(activate(V2)))
r27: U56(tt()) -> tt()
r28: U61(tt(),V) -> U62(isPalListKind(activate(V)),activate(V))
r29: U62(tt(),V) -> U63(isQid(activate(V)))
r30: U63(tt()) -> tt()
r31: U71(tt(),I,P) -> U72(isPalListKind(activate(I)),activate(P))
r32: U72(tt(),P) -> U73(isPal(activate(P)),activate(P))
r33: U73(tt(),P) -> U74(isPalListKind(activate(P)))
r34: U74(tt()) -> tt()
r35: U81(tt(),V) -> U82(isPalListKind(activate(V)),activate(V))
r36: U82(tt(),V) -> U83(isNePal(activate(V)))
r37: U83(tt()) -> tt()
r38: U91(tt(),V2) -> U92(isPalListKind(activate(V2)))
r39: U92(tt()) -> tt()
r40: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r41: isList(n__nil()) -> tt()
r42: isList(n____(V1,V2)) -> U21(isPalListKind(activate(V1)),activate(V1),activate(V2))
r43: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r44: isNeList(n____(V1,V2)) -> U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
r45: isNeList(n____(V1,V2)) -> U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
r46: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r47: isNePal(n____(I,n____(P,I))) -> U71(isQid(activate(I)),activate(I),activate(P))
r48: isPal(V) -> U81(isPalListKind(activate(V)),activate(V))
r49: isPal(n__nil()) -> tt()
r50: isPalListKind(n__a()) -> tt()
r51: isPalListKind(n__e()) -> tt()
r52: isPalListKind(n__i()) -> tt()
r53: isPalListKind(n__nil()) -> tt()
r54: isPalListKind(n__o()) -> tt()
r55: isPalListKind(n__u()) -> tt()
r56: isPalListKind(n____(V1,V2)) -> U91(isPalListKind(activate(V1)),activate(V2))
r57: isQid(n__a()) -> tt()
r58: isQid(n__e()) -> tt()
r59: isQid(n__i()) -> tt()
r60: isQid(n__o()) -> tt()
r61: isQid(n__u()) -> tt()
r62: nil() -> n__nil()
r63: __(X1,X2) -> n____(X1,X2)
r64: a() -> n__a()
r65: e() -> n__e()
r66: i() -> n__i()
r67: o() -> n__o()
r68: u() -> n__u()
r69: activate(n__nil()) -> nil()
r70: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r71: activate(n__a()) -> a()
r72: activate(n__e()) -> e()
r73: activate(n__i()) -> i()
r74: activate(n__o()) -> o()
r75: activate(n__u()) -> u()
r76: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r63

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        __#_A(x1,x2) = ((1,1),(1,1)) x1 + x2
        ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (1,1)
        nil_A() = (1,1)
        n_____A(x1,x2) = (0,0)
    
    2. matrix interpretations:
    
      carrier: N^2
      order: standard order
      interpretations:
        __#_A(x1,x2) = ((0,1),(0,1)) x1 + ((1,0),(1,1)) x2
        ___A(x1,x2) = ((1,0),(1,1)) x1 + ((1,1),(0,0)) x2 + (1,2)
        nil_A() = (1,1)
        n_____A(x1,x2) = (2,3)
    

The next rules are strictly ordered:

  p1, p2

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