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(isNeList(activate(V)))
  U12(tt()) -> tt()
  U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
  U22(tt(),V2) -> U23(isList(activate(V2)))
  U23(tt()) -> tt()
  U31(tt(),V) -> U32(isQid(activate(V)))
  U32(tt()) -> tt()
  U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
  U42(tt(),V2) -> U43(isNeList(activate(V2)))
  U43(tt()) -> tt()
  U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
  U52(tt(),V2) -> U53(isList(activate(V2)))
  U53(tt()) -> tt()
  U61(tt(),V) -> U62(isQid(activate(V)))
  U62(tt()) -> tt()
  U71(tt(),V) -> U72(isNePal(activate(V)))
  U72(tt()) -> tt()
  and(tt(),X) -> activate(X)
  isList(V) -> U11(isPalListKind(activate(V)),activate(V))
  isList(n__nil()) -> tt()
  isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
  isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
  isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
  isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
  isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
  isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
  isPal(V) -> U71(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)) -> and(isPalListKind(activate(V1)),n__isPalListKind(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)
  isPalListKind(X) -> n__isPalListKind(X)
  and(X1,X2) -> n__and(X1,X2)
  isPal(X) -> n__isPal(X)
  a() -> n__a()
  e() -> n__e()
  i() -> n__i()
  o() -> n__o()
  u() -> n__u()
  activate(n__nil()) -> nil()
  activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
  activate(n__isPalListKind(X)) -> isPalListKind(X)
  activate(n__and(X1,X2)) -> and(activate(X1),X2)
  activate(n__isPal(X)) -> isPal(X)
  activate(n__a()) -> a()
  activate(n__e()) -> e()
  activate(n__i()) -> i()
  activate(n__o()) -> o()
  activate(n__u()) -> u()
  activate(X) -> X

-- SCC 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#(isNeList(activate(V)))
p4: U11#(tt(),V) -> isNeList#(activate(V))
p5: U11#(tt(),V) -> activate#(V)
p6: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2))
p7: U21#(tt(),V1,V2) -> isList#(activate(V1))
p8: U21#(tt(),V1,V2) -> activate#(V1)
p9: U21#(tt(),V1,V2) -> activate#(V2)
p10: U22#(tt(),V2) -> U23#(isList(activate(V2)))
p11: U22#(tt(),V2) -> isList#(activate(V2))
p12: U22#(tt(),V2) -> activate#(V2)
p13: U31#(tt(),V) -> U32#(isQid(activate(V)))
p14: U31#(tt(),V) -> isQid#(activate(V))
p15: U31#(tt(),V) -> activate#(V)
p16: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2))
p17: U41#(tt(),V1,V2) -> isList#(activate(V1))
p18: U41#(tt(),V1,V2) -> activate#(V1)
p19: U41#(tt(),V1,V2) -> activate#(V2)
p20: U42#(tt(),V2) -> U43#(isNeList(activate(V2)))
p21: U42#(tt(),V2) -> isNeList#(activate(V2))
p22: U42#(tt(),V2) -> activate#(V2)
p23: U51#(tt(),V1,V2) -> U52#(isNeList(activate(V1)),activate(V2))
p24: U51#(tt(),V1,V2) -> isNeList#(activate(V1))
p25: U51#(tt(),V1,V2) -> activate#(V1)
p26: U51#(tt(),V1,V2) -> activate#(V2)
p27: U52#(tt(),V2) -> U53#(isList(activate(V2)))
p28: U52#(tt(),V2) -> isList#(activate(V2))
p29: U52#(tt(),V2) -> activate#(V2)
p30: U61#(tt(),V) -> U62#(isQid(activate(V)))
p31: U61#(tt(),V) -> isQid#(activate(V))
p32: U61#(tt(),V) -> activate#(V)
p33: U71#(tt(),V) -> U72#(isNePal(activate(V)))
p34: U71#(tt(),V) -> isNePal#(activate(V))
p35: U71#(tt(),V) -> activate#(V)
p36: and#(tt(),X) -> activate#(X)
p37: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V))
p38: isList#(V) -> isPalListKind#(activate(V))
p39: isList#(V) -> activate#(V)
p40: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p41: isList#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
p42: isList#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p43: isList#(n____(V1,V2)) -> activate#(V1)
p44: isList#(n____(V1,V2)) -> activate#(V2)
p45: isNeList#(V) -> U31#(isPalListKind(activate(V)),activate(V))
p46: isNeList#(V) -> isPalListKind#(activate(V))
p47: isNeList#(V) -> activate#(V)
p48: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p49: isNeList#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
p50: isNeList#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p51: isNeList#(n____(V1,V2)) -> activate#(V1)
p52: isNeList#(n____(V1,V2)) -> activate#(V2)
p53: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p54: isNeList#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
p55: isNeList#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p56: isNeList#(n____(V1,V2)) -> activate#(V1)
p57: isNeList#(n____(V1,V2)) -> activate#(V2)
p58: isNePal#(V) -> U61#(isPalListKind(activate(V)),activate(V))
p59: isNePal#(V) -> isPalListKind#(activate(V))
p60: isNePal#(V) -> activate#(V)
p61: isNePal#(n____(I,n____(P,I))) -> and#(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
p62: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPalListKind(activate(I)))
p63: isNePal#(n____(I,n____(P,I))) -> isQid#(activate(I))
p64: isNePal#(n____(I,n____(P,I))) -> activate#(I)
p65: isNePal#(n____(I,n____(P,I))) -> activate#(P)
p66: isPal#(V) -> U71#(isPalListKind(activate(V)),activate(V))
p67: isPal#(V) -> isPalListKind#(activate(V))
p68: isPal#(V) -> activate#(V)
p69: isPalListKind#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
p70: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p71: isPalListKind#(n____(V1,V2)) -> activate#(V1)
p72: isPalListKind#(n____(V1,V2)) -> activate#(V2)
p73: activate#(n__nil()) -> nil#()
p74: activate#(n____(X1,X2)) -> __#(activate(X1),activate(X2))
p75: activate#(n____(X1,X2)) -> activate#(X1)
p76: activate#(n____(X1,X2)) -> activate#(X2)
p77: activate#(n__isPalListKind(X)) -> isPalListKind#(X)
p78: activate#(n__and(X1,X2)) -> and#(activate(X1),X2)
p79: activate#(n__and(X1,X2)) -> activate#(X1)
p80: activate#(n__isPal(X)) -> isPal#(X)
p81: activate#(n__a()) -> a#()
p82: activate#(n__e()) -> e#()
p83: activate#(n__i()) -> i#()
p84: activate#(n__o()) -> o#()
p85: 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(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p4, p6, p7, p11, p16, p17, p21, p23, p24, p28, p37, p40, p48, p53}
  {p32, p34, p35, p36, p58, p59, p60, p61, p62, p64, p65, p66, p67, p68, p69, p70, p71, p72, p75, p76, p77, p78, p79, p80}
  {p1, p2}


-- Reduction pair.

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

p1: U52#(tt(),V2) -> isList#(activate(V2))
p2: isList#(n____(V1,V2)) -> U21#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p3: U21#(tt(),V1,V2) -> isList#(activate(V1))
p4: isList#(V) -> U11#(isPalListKind(activate(V)),activate(V))
p5: U11#(tt(),V) -> isNeList#(activate(V))
p6: isNeList#(n____(V1,V2)) -> U51#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p7: U51#(tt(),V1,V2) -> isNeList#(activate(V1))
p8: isNeList#(n____(V1,V2)) -> U41#(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
p9: U41#(tt(),V1,V2) -> isList#(activate(V1))
p10: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2))
p11: U42#(tt(),V2) -> isNeList#(activate(V2))
p12: U51#(tt(),V1,V2) -> U52#(isNeList(activate(V1)),activate(V2))
p13: U21#(tt(),V1,V2) -> U22#(isList(activate(V1)),activate(V2))
p14: U22#(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(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: 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, 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            U52#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (2,59)
            tt_A() = (3,53)
            isList#_A(x1) = ((1,0),(0,0)) x1 + (4,58)
            activate_A(x1) = ((1,0),(1,1)) x1 + (0,19)
            n_____A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,0)) x2 + (13,7)
            U21#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,0)) x3 + (14,57)
            and_A(x1,x2) = ((1,0),(0,0)) x2 + (1,37)
            isPalListKind_A(x1) = ((1,0),(1,1)) x1 + (10,16)
            n__isPalListKind_A(x1) = ((1,0),(1,1)) x1 + (10,16)
            U11#_A(x1,x2) = ((1,0),(0,0)) x2 + (3,57)
            isNeList#_A(x1) = ((1,0),(0,0)) x1 + (2,56)
            U51#_A(x1,x2,x3) = ((1,0),(1,1)) x2 + ((1,0),(1,1)) x3 + (14,57)
            U41#_A(x1,x2,x3) = ((1,0),(0,0)) x2 + ((1,0),(0,0)) x3 + (14,55)
            U42#_A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (1,4)
            isList_A(x1) = x1 + (10,31)
            isNeList_A(x1) = ((0,0),(1,0)) x1 + (7,21)
            U22#_A(x1,x2) = x1 + ((1,0),(1,0)) x2 + (2,6)
            U62_A(x1) = (4,54)
            U61_A(x1,x2) = ((0,0),(1,0)) x1 + (6,52)
            isQid_A(x1) = (5,110)
            U23_A(x1) = ((0,0),(1,0)) x1 + (4,44)
            U43_A(x1) = (4,0)
            U53_A(x1) = (4,54)
            U72_A(x1) = (4,83)
            isNePal_A(x1) = ((1,0),(1,1)) x1 + (7,63)
            n__and_A(x1,x2) = ((1,0),(0,0)) x2 + (1,18)
            n__isPal_A(x1) = x1 + (34,83)
            U12_A(x1) = x1 + (1,1)
            U22_A(x1,x2) = ((1,0),(1,1)) x2 + (5,55)
            U32_A(x1) = (4,1)
            U42_A(x1,x2) = (5,0)
            U52_A(x1,x2) = (5,17)
            U71_A(x1,x2) = ((1,0),(0,0)) x1 + (4,83)
            n__a_A() = (4,54)
            n__e_A() = (1,54)
            n__i_A() = (0,54)
            n__o_A() = (1,1)
            n__u_A() = (38,0)
            ___A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (13,8)
            nil_A() = (38,1)
            U11_A(x1,x2) = (9,23)
            U21_A(x1,x2,x3) = ((1,0),(0,0)) x3 + (9,49)
            U31_A(x1,x2) = (6,20)
            U41_A(x1,x2,x3) = ((0,0),(1,0)) x3 + (6,6)
            U51_A(x1,x2,x3) = (6,18)
            isPal_A(x1) = ((1,0),(1,1)) x1 + (34,84)
            n__nil_A() = (38,0)
            a_A() = (4,76)
            e_A() = (1,54)
            i_A() = (0,72)
            o_A() = (1,2)
            u_A() = (38,0)
    
      precedence:
      
        isQid = n__e = a = e > U51# > U43 = U42 > U21# > U52# = isList# = U11# = isNeList# = U42# = U22# > U22 = U21 > U53 > tt = U23 = U72 = n__i > U41# = n__isPal = isPal > n__o = __ = U11 > n____ = n__a > i > and = isList = U61 = isNePal = n__and = n__nil = o > U62 > activate = n__u = u > isPalListKind = n__isPalListKind > U71 > isNeList = U32 = nil = U31 > U41 > U51 > U52 > U12
      
      partial status:
    
        pi(U52#) = []
        pi(tt) = []
        pi(isList#) = []
        pi(activate) = [1]
        pi(n____) = []
        pi(U21#) = [2]
        pi(and) = []
        pi(isPalListKind) = [1]
        pi(n__isPalListKind) = [1]
        pi(U11#) = []
        pi(isNeList#) = []
        pi(U51#) = [2, 3]
        pi(U41#) = []
        pi(U42#) = [1]
        pi(isList) = []
        pi(isNeList) = []
        pi(U22#) = [1]
        pi(U62) = []
        pi(U61) = []
        pi(isQid) = []
        pi(U23) = []
        pi(U43) = []
        pi(U53) = []
        pi(U72) = []
        pi(isNePal) = [1]
        pi(n__and) = []
        pi(n__isPal) = []
        pi(U12) = [1]
        pi(U22) = []
        pi(U32) = []
        pi(U42) = []
        pi(U52) = []
        pi(U71) = []
        pi(n__a) = []
        pi(n__e) = []
        pi(n__i) = []
        pi(n__o) = []
        pi(n__u) = []
        pi(__) = []
        pi(nil) = []
        pi(U11) = []
        pi(U21) = []
        pi(U31) = []
        pi(U41) = []
        pi(U51) = []
        pi(isPal) = [1]
        pi(n__nil) = []
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            U52#_A(x1,x2) = (11,11)
            tt_A() = (10,10)
            isList#_A(x1) = (10,9)
            activate_A(x1) = (9,7)
            n_____A(x1,x2) = (5,10)
            U21#_A(x1,x2,x3) = (4,9)
            and_A(x1,x2) = (6,8)
            isPalListKind_A(x1) = (8,6)
            n__isPalListKind_A(x1) = (2,5)
            U11#_A(x1,x2) = (8,6)
            isNeList#_A(x1) = (7,12)
            U51#_A(x1,x2,x3) = (15,12)
            U41#_A(x1,x2,x3) = (6,8)
            U42#_A(x1,x2) = x1 + (1,3)
            isList_A(x1) = (2,3)
            isNeList_A(x1) = (14,4)
            U22#_A(x1,x2) = ((1,0),(1,1)) x1 + (1,1)
            U62_A(x1) = (0,0)
            U61_A(x1,x2) = (6,1)
            isQid_A(x1) = (13,11)
            U23_A(x1) = (11,11)
            U43_A(x1) = (11,0)
            U53_A(x1) = (11,11)
            U72_A(x1) = (11,11)
            isNePal_A(x1) = (7,3)
            n__and_A(x1,x2) = (1,1)
            n__isPal_A(x1) = (1,11)
            U12_A(x1) = (11,1)
            U22_A(x1,x2) = (11,12)
            U32_A(x1) = (11,11)
            U42_A(x1,x2) = (11,0)
            U52_A(x1,x2) = (12,12)
            U71_A(x1,x2) = (12,4)
            n__a_A() = (1,0)
            n__e_A() = (1,1)
            n__i_A() = (1,1)
            n__o_A() = (1,1)
            n__u_A() = (0,0)
            ___A(x1,x2) = (10,11)
            nil_A() = (1,8)
            U11_A(x1,x2) = (12,2)
            U21_A(x1,x2,x3) = (1,11)
            U31_A(x1,x2) = (12,3)
            U41_A(x1,x2,x3) = (0,3)
            U51_A(x1,x2,x3) = (13,13)
            isPal_A(x1) = ((1,0),(1,1)) x1 + (13,5)
            n__nil_A() = (1,1)
            a_A() = (2,1)
            e_A() = (2,0)
            i_A() = (9,2)
            o_A() = (2,6)
            u_A() = (0,0)
    
      precedence:
      
        isNeList# = U51# = isNeList = U23 = n__isPal = nil > U41# > U52# > isList# = u > U21# = e > i > U41 > U61 = a > U31 > __ > n__e > U32 > isQid > U21 > U52 > U72 > U53 > U11# > tt = activate > U11 > n__o = n__u = o > n__nil > n__a > U42# > isPal > isPalListKind > and = n__i > U42 > U71 > U12 > n__and > U51 > U22 > U43 > U62 > isNePal > U22# > n__isPalListKind > n____ = isList
      
      partial status:
    
        pi(U52#) = []
        pi(tt) = []
        pi(isList#) = []
        pi(activate) = []
        pi(n____) = []
        pi(U21#) = []
        pi(and) = []
        pi(isPalListKind) = []
        pi(n__isPalListKind) = []
        pi(U11#) = []
        pi(isNeList#) = []
        pi(U51#) = []
        pi(U41#) = []
        pi(U42#) = []
        pi(isList) = []
        pi(isNeList) = []
        pi(U22#) = [1]
        pi(U62) = []
        pi(U61) = []
        pi(isQid) = []
        pi(U23) = []
        pi(U43) = []
        pi(U53) = []
        pi(U72) = []
        pi(isNePal) = []
        pi(n__and) = []
        pi(n__isPal) = []
        pi(U12) = []
        pi(U22) = []
        pi(U32) = []
        pi(U42) = []
        pi(U52) = []
        pi(U71) = []
        pi(n__a) = []
        pi(n__e) = []
        pi(n__i) = []
        pi(n__o) = []
        pi(n__u) = []
        pi(__) = []
        pi(nil) = []
        pi(U11) = []
        pi(U21) = []
        pi(U31) = []
        pi(U41) = []
        pi(U51) = []
        pi(isPal) = []
        pi(n__nil) = []
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
    

The next rules are strictly ordered:

  p2, p3, p4, p6, p8, p9, p11, p13

We remove them from the problem.

-- SCC decomposition.

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

p1: U52#(tt(),V2) -> isList#(activate(V2))
p2: U11#(tt(),V) -> isNeList#(activate(V))
p3: U51#(tt(),V1,V2) -> isNeList#(activate(V1))
p4: U41#(tt(),V1,V2) -> U42#(isList(activate(V1)),activate(V2))
p5: U51#(tt(),V1,V2) -> U52#(isNeList(activate(V1)),activate(V2))
p6: U22#(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(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: 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: isPal#(V) -> activate#(V)
p2: activate#(n__isPal(X)) -> isPal#(X)
p3: isPal#(V) -> isPalListKind#(activate(V))
p4: isPalListKind#(n____(V1,V2)) -> activate#(V2)
p5: activate#(n__and(X1,X2)) -> activate#(X1)
p6: activate#(n__and(X1,X2)) -> and#(activate(X1),X2)
p7: and#(tt(),X) -> activate#(X)
p8: activate#(n__isPalListKind(X)) -> isPalListKind#(X)
p9: isPalListKind#(n____(V1,V2)) -> activate#(V1)
p10: activate#(n____(X1,X2)) -> activate#(X2)
p11: activate#(n____(X1,X2)) -> activate#(X1)
p12: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p13: isPalListKind#(n____(V1,V2)) -> and#(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
p14: isPal#(V) -> U71#(isPalListKind(activate(V)),activate(V))
p15: U71#(tt(),V) -> activate#(V)
p16: U71#(tt(),V) -> isNePal#(activate(V))
p17: isNePal#(n____(I,n____(P,I))) -> activate#(P)
p18: isNePal#(n____(I,n____(P,I))) -> activate#(I)
p19: isNePal#(n____(I,n____(P,I))) -> and#(isQid(activate(I)),n__isPalListKind(activate(I)))
p20: isNePal#(n____(I,n____(P,I))) -> and#(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
p21: isNePal#(V) -> activate#(V)
p22: isNePal#(V) -> isPalListKind#(activate(V))
p23: isNePal#(V) -> U61#(isPalListKind(activate(V)),activate(V))
p24: U61#(tt(),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(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r17, r18, r19, r20, r21, 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            isPal#_A(x1) = ((1,1),(0,0)) x1 + (5,41)
            activate#_A(x1) = ((0,1),(0,0)) x1 + (1,41)
            n__isPal_A(x1) = ((0,1),(1,1)) x1 + (29,5)
            isPalListKind#_A(x1) = ((0,1),(0,0)) x1 + (2,41)
            activate_A(x1) = x1
            n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (14,20)
            n__and_A(x1,x2) = x1 + x2 + (2,8)
            and#_A(x1,x2) = ((0,1),(0,0)) x1 + ((0,1),(0,0)) x2 + (1,41)
            tt_A() = (0,3)
            n__isPalListKind_A(x1) = ((1,1),(0,1)) x1 + (0,6)
            isPalListKind_A(x1) = ((1,1),(0,1)) x1 + (0,6)
            U71#_A(x1,x2) = ((1,1),(0,0)) x2 + (4,41)
            isNePal#_A(x1) = ((1,1),(0,0)) x1 + (3,41)
            isQid_A(x1) = ((0,0),(1,0)) x1 + (25,0)
            and_A(x1,x2) = x1 + x2 + (2,8)
            U61#_A(x1,x2) = ((0,1),(0,0)) x2 + (2,41)
            U62_A(x1) = (1,5)
            U61_A(x1,x2) = ((0,0),(1,0)) x2 + (2,5)
            U72_A(x1) = (1,4)
            isNePal_A(x1) = ((1,1),(1,1)) x1 + (3,5)
            U71_A(x1,x2) = (2,4)
            ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (14,20)
            nil_A() = (0,0)
            isPal_A(x1) = ((0,1),(1,1)) x1 + (29,5)
            n__nil_A() = (0,0)
            a_A() = (3,0)
            n__a_A() = (3,0)
            e_A() = (3,0)
            n__e_A() = (3,0)
            i_A() = (3,3)
            n__i_A() = (3,3)
            o_A() = (3,1)
            n__o_A() = (3,1)
            u_A() = (3,1)
            n__u_A() = (3,1)
    
      precedence:
      
        U71# = e = n__e > isNePal# = U61# > n__isPal = isQid = U72 = U71 = isPal = u = n__u > activate = __ = a = n__a = i = o = n__o > isPalListKind# = n__and = tt = n__isPalListKind = isPalListKind = and = U62 = U61 = isNePal = n__i > and# > nil > n__nil > n____ > activate# > isPal#
      
      partial status:
    
        pi(isPal#) = []
        pi(activate#) = []
        pi(n__isPal) = []
        pi(isPalListKind#) = []
        pi(activate) = [1]
        pi(n____) = [1, 2]
        pi(n__and) = []
        pi(and#) = []
        pi(tt) = []
        pi(n__isPalListKind) = [1]
        pi(isPalListKind) = [1]
        pi(U71#) = []
        pi(isNePal#) = []
        pi(isQid) = []
        pi(and) = [1]
        pi(U61#) = []
        pi(U62) = []
        pi(U61) = []
        pi(U72) = []
        pi(isNePal) = [1]
        pi(U71) = []
        pi(__) = [1, 2]
        pi(nil) = []
        pi(isPal) = []
        pi(n__nil) = []
        pi(a) = []
        pi(n__a) = []
        pi(e) = []
        pi(n__e) = []
        pi(i) = []
        pi(n__i) = []
        pi(o) = []
        pi(n__o) = []
        pi(u) = []
        pi(n__u) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: standard order
          interpretations:
            isPal#_A(x1) = (8,0)
            activate#_A(x1) = (2,0)
            n__isPal_A(x1) = (7,0)
            isPalListKind#_A(x1) = (3,0)
            activate_A(x1) = ((1,0),(0,0)) x1 + (12,3)
            n_____A(x1,x2) = ((0,1),(1,1)) x2 + (0,11)
            n__and_A(x1,x2) = (0,0)
            and#_A(x1,x2) = (1,0)
            tt_A() = (3,1)
            n__isPalListKind_A(x1) = (4,2)
            isPalListKind_A(x1) = (9,3)
            U71#_A(x1,x2) = (9,1)
            isNePal#_A(x1) = (5,1)
            isQid_A(x1) = (6,3)
            and_A(x1,x2) = (10,2)
            U61#_A(x1,x2) = (3,1)
            U62_A(x1) = (0,0)
            U61_A(x1,x2) = (13,3)
            U72_A(x1) = (3,1)
            isNePal_A(x1) = ((0,1),(0,0)) x1 + (14,3)
            U71_A(x1,x2) = (18,3)
            ___A(x1,x2) = ((0,1),(0,0)) x2 + (9,0)
            nil_A() = (1,1)
            isPal_A(x1) = (19,3)
            n__nil_A() = (0,0)
            a_A() = (2,1)
            n__a_A() = (1,0)
            e_A() = (12,2)
            n__e_A() = (0,1)
            i_A() = (2,1)
            n__i_A() = (1,0)
            o_A() = (13,1)
            n__o_A() = (1,0)
            u_A() = (1,1)
            n__u_A() = (0,0)
    
      precedence:
      
        isNePal > U61 > isQid > n____ > activate = isPalListKind = and > isPal > U71 > n__and > o > tt = U72 = a = n__a = e = n__e = n__o = u > nil = n__nil = n__u > __ > isPal# > U71# > isPalListKind# > isNePal# > U61# > activate# > n__isPalListKind > and# > n__isPal = U62 = i = n__i
      
      partial status:
    
        pi(isPal#) = []
        pi(activate#) = []
        pi(n__isPal) = []
        pi(isPalListKind#) = []
        pi(activate) = []
        pi(n____) = []
        pi(n__and) = []
        pi(and#) = []
        pi(tt) = []
        pi(n__isPalListKind) = []
        pi(isPalListKind) = []
        pi(U71#) = []
        pi(isNePal#) = []
        pi(isQid) = []
        pi(and) = []
        pi(U61#) = []
        pi(U62) = []
        pi(U61) = []
        pi(U72) = []
        pi(isNePal) = []
        pi(U71) = []
        pi(__) = []
        pi(nil) = []
        pi(isPal) = []
        pi(n__nil) = []
        pi(a) = []
        pi(n__a) = []
        pi(e) = []
        pi(n__e) = []
        pi(i) = []
        pi(n__i) = []
        pi(o) = []
        pi(n__o) = []
        pi(u) = []
        pi(n__u) = []
    

The next rules are strictly ordered:

  p1, p2, p3, p6, p7, p8, p9, p13, p14, p15, p16, p17, p18, p19, p20, p21, p24

We remove them from the problem.

-- SCC decomposition.

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

p1: isPalListKind#(n____(V1,V2)) -> activate#(V2)
p2: activate#(n__and(X1,X2)) -> activate#(X1)
p3: activate#(n____(X1,X2)) -> activate#(X2)
p4: activate#(n____(X1,X2)) -> activate#(X1)
p5: isPalListKind#(n____(V1,V2)) -> isPalListKind#(activate(V1))
p6: isNePal#(V) -> isPalListKind#(activate(V))
p7: isNePal#(V) -> U61#(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(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p5}
  {p2, p3, p4}


-- Reduction pair.

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

p1: 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(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r17, r18, r19, r20, r21, 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

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            isPalListKind#_A(x1) = x1 + (1,12)
            n_____A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (52,13)
            activate_A(x1) = ((1,0),(1,1)) x1 + (0,2)
            U62_A(x1) = (11,9)
            tt_A() = (10,11)
            U61_A(x1,x2) = x2 + (12,8)
            isQid_A(x1) = (13,10)
            n__a_A() = (1,0)
            n__e_A() = (0,1)
            n__i_A() = (0,1)
            n__o_A() = (1,1)
            n__u_A() = (1,1)
            U72_A(x1) = (11,12)
            isNePal_A(x1) = ((1,0),(0,0)) x1 + (13,9)
            isPalListKind_A(x1) = ((1,0),(1,0)) x1 + (10,12)
            and_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (1,4)
            n__isPalListKind_A(x1) = ((1,0),(0,0)) x1 + (10,1)
            n__and_A(x1,x2) = ((1,0),(0,0)) x1 + x2 + (1,3)
            n__isPal_A(x1) = ((0,0),(1,0)) x1 + (15,27)
            U71_A(x1,x2) = ((0,0),(1,0)) x2 + (14,13)
            ___A(x1,x2) = ((1,0),(1,0)) x1 + x2 + (52,51)
            nil_A() = (0,13)
            isPal_A(x1) = ((0,0),(1,0)) x1 + (15,28)
            n__nil_A() = (0,12)
            a_A() = (1,1)
            e_A() = (0,2)
            i_A() = (0,2)
            o_A() = (1,2)
            u_A() = (1,2)
    
      precedence:
      
        isQid > isNePal > isPalListKind# = activate = e = i = o = u > U62 > isPal > n__isPal > a > n__a > U61 > n__i > U71 > U72 > isPalListKind > n__o > tt = __ > n____ = n__isPalListKind > n__e = n__u = and = nil = n__nil > n__and
      
      partial status:
    
        pi(isPalListKind#) = [1]
        pi(n____) = [2]
        pi(activate) = [1]
        pi(U62) = []
        pi(tt) = []
        pi(U61) = []
        pi(isQid) = []
        pi(n__a) = []
        pi(n__e) = []
        pi(n__i) = []
        pi(n__o) = []
        pi(n__u) = []
        pi(U72) = []
        pi(isNePal) = []
        pi(isPalListKind) = []
        pi(and) = []
        pi(n__isPalListKind) = []
        pi(n__and) = []
        pi(n__isPal) = []
        pi(U71) = []
        pi(__) = []
        pi(nil) = []
        pi(isPal) = []
        pi(n__nil) = []
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            isPalListKind#_A(x1) = x1 + (1,12)
            n_____A(x1,x2) = ((1,0),(1,1)) x2 + (7,0)
            activate_A(x1) = (5,11)
            U62_A(x1) = (0,0)
            tt_A() = (0,0)
            U61_A(x1,x2) = (0,0)
            isQid_A(x1) = (0,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)
            U72_A(x1) = (0,0)
            isNePal_A(x1) = (4,10)
            isPalListKind_A(x1) = (2,9)
            and_A(x1,x2) = (1,8)
            n__isPalListKind_A(x1) = (0,0)
            n__and_A(x1,x2) = (0,0)
            n__isPal_A(x1) = (3,8)
            U71_A(x1,x2) = (0,0)
            ___A(x1,x2) = (0,1)
            nil_A() = (2,2)
            isPal_A(x1) = (3,10)
            n__nil_A() = (1,1)
            a_A() = (2,2)
            e_A() = (2,2)
            i_A() = (2,2)
            o_A() = (2,2)
            u_A() = (1,1)
    
      precedence:
      
        i > U71 > o > __ > u > n__i > n__e > n__nil > e > isPal > nil > activate > isPalListKind# > U72 > n____ = U62 = tt = U61 = isQid = n__a = n__o = n__u = isNePal = isPalListKind = and = n__isPalListKind = n__and = n__isPal = a
      
      partial status:
    
        pi(isPalListKind#) = [1]
        pi(n____) = [2]
        pi(activate) = []
        pi(U62) = []
        pi(tt) = []
        pi(U61) = []
        pi(isQid) = []
        pi(n__a) = []
        pi(n__e) = []
        pi(n__i) = []
        pi(n__o) = []
        pi(n__u) = []
        pi(U72) = []
        pi(isNePal) = []
        pi(isPalListKind) = []
        pi(and) = []
        pi(n__isPalListKind) = []
        pi(n__and) = []
        pi(n__isPal) = []
        pi(U71) = []
        pi(__) = []
        pi(nil) = []
        pi(isPal) = []
        pi(n__nil) = []
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
    

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

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: activate(X) -> X

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            activate#_A(x1) = x1
            n__and_A(x1,x2) = x1 + x2 + (1,1)
            n_____A(x1,x2) = x1 + ((1,0),(1,1)) x2 + (1,1)
    
      precedence:
      
        activate# = n____ > n__and
      
      partial status:
    
        pi(activate#) = [1]
        pi(n__and) = [1, 2]
        pi(n____) = [1, 2]
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            activate#_A(x1) = x1 + (1,1)
            n__and_A(x1,x2) = x1 + x2 + (2,2)
            n_____A(x1,x2) = x1 + x2 + (2,2)
    
      precedence:
      
        activate# = n__and > n____
      
      partial status:
    
        pi(activate#) = []
        pi(n__and) = []
        pi(n____) = [2]
    

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

p1: activate#(n__and(X1,X2)) -> activate#(X1)
p2: activate#(n____(X1,X2)) -> activate#(X2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

p1: activate#(n__and(X1,X2)) -> activate#(X1)
p2: activate#(n____(X1,X2)) -> activate#(X2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: activate(X) -> X

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            activate#_A(x1) = ((1,0),(0,0)) x1
            n__and_A(x1,x2) = x1 + x2 + (1,1)
            n_____A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (1,1)
    
      precedence:
      
        n__and > activate# = n____
      
      partial status:
    
        pi(activate#) = []
        pi(n__and) = [1, 2]
        pi(n____) = [1]
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            activate#_A(x1) = (0,0)
            n__and_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (1,1)
            n_____A(x1,x2) = (1,1)
    
      precedence:
      
        activate# = n__and = n____
      
      partial status:
    
        pi(activate#) = []
        pi(n__and) = [2]
        pi(n____) = []
    

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: activate#(n____(X1,X2)) -> activate#(X2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: activate#(n____(X1,X2)) -> activate#(X2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt(),V) -> U12(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: activate(X) -> X

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            activate#_A(x1) = x1 + (1,2)
            n_____A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (2,1)
    
      precedence:
      
        activate# > n____
      
      partial status:
    
        pi(activate#) = [1]
        pi(n____) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            activate#_A(x1) = (0,0)
            n_____A(x1,x2) = (1,1)
    
      precedence:
      
        activate# > n____
      
      partial status:
    
        pi(activate#) = []
        pi(n____) = []
    

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: __#(__(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(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r45

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            __#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (1,1)
            ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (2,2)
            nil_A() = (1,1)
            n_____A(x1,x2) = (0,0)
    
      precedence:
      
        __# = __ = nil = n____
      
      partial status:
    
        pi(__#) = []
        pi(__) = []
        pi(nil) = []
        pi(n____) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            __#_A(x1,x2) = (0,0)
            ___A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (1,1)
            nil_A() = (1,1)
            n_____A(x1,x2) = (0,0)
    
      precedence:
      
        __# = __ = nil = n____
      
      partial status:
    
        pi(__#) = []
        pi(__) = []
        pi(nil) = []
        pi(n____) = []
    

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

p1: __#(__(X,Y),Z) -> __#(X,__(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(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: __#(__(X,Y),Z) -> __#(X,__(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(isNeList(activate(V)))
r5: U12(tt()) -> tt()
r6: U21(tt(),V1,V2) -> U22(isList(activate(V1)),activate(V2))
r7: U22(tt(),V2) -> U23(isList(activate(V2)))
r8: U23(tt()) -> tt()
r9: U31(tt(),V) -> U32(isQid(activate(V)))
r10: U32(tt()) -> tt()
r11: U41(tt(),V1,V2) -> U42(isList(activate(V1)),activate(V2))
r12: U42(tt(),V2) -> U43(isNeList(activate(V2)))
r13: U43(tt()) -> tt()
r14: U51(tt(),V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
r15: U52(tt(),V2) -> U53(isList(activate(V2)))
r16: U53(tt()) -> tt()
r17: U61(tt(),V) -> U62(isQid(activate(V)))
r18: U62(tt()) -> tt()
r19: U71(tt(),V) -> U72(isNePal(activate(V)))
r20: U72(tt()) -> tt()
r21: and(tt(),X) -> activate(X)
r22: isList(V) -> U11(isPalListKind(activate(V)),activate(V))
r23: isList(n__nil()) -> tt()
r24: isList(n____(V1,V2)) -> U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r25: isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
r26: isNeList(n____(V1,V2)) -> U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r27: isNeList(n____(V1,V2)) -> U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2))
r28: isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
r29: isNePal(n____(I,n____(P,I))) -> and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
r30: isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
r31: isPal(n__nil()) -> tt()
r32: isPalListKind(n__a()) -> tt()
r33: isPalListKind(n__e()) -> tt()
r34: isPalListKind(n__i()) -> tt()
r35: isPalListKind(n__nil()) -> tt()
r36: isPalListKind(n__o()) -> tt()
r37: isPalListKind(n__u()) -> tt()
r38: isPalListKind(n____(V1,V2)) -> and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
r39: isQid(n__a()) -> tt()
r40: isQid(n__e()) -> tt()
r41: isQid(n__i()) -> tt()
r42: isQid(n__o()) -> tt()
r43: isQid(n__u()) -> tt()
r44: nil() -> n__nil()
r45: __(X1,X2) -> n____(X1,X2)
r46: isPalListKind(X) -> n__isPalListKind(X)
r47: and(X1,X2) -> n__and(X1,X2)
r48: isPal(X) -> n__isPal(X)
r49: a() -> n__a()
r50: e() -> n__e()
r51: i() -> n__i()
r52: o() -> n__o()
r53: u() -> n__u()
r54: activate(n__nil()) -> nil()
r55: activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
r56: activate(n__isPalListKind(X)) -> isPalListKind(X)
r57: activate(n__and(X1,X2)) -> and(activate(X1),X2)
r58: activate(n__isPal(X)) -> isPal(X)
r59: activate(n__a()) -> a()
r60: activate(n__e()) -> e()
r61: activate(n__i()) -> i()
r62: activate(n__o()) -> o()
r63: activate(n__u()) -> u()
r64: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r45

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            __#_A(x1,x2) = ((1,0),(1,0)) x1
            ___A(x1,x2) = x1 + x2 + (2,3)
            nil_A() = (1,1)
            n_____A(x1,x2) = (1,1)
    
      precedence:
      
        __ > __# = nil = n____
      
      partial status:
    
        pi(__#) = []
        pi(__) = [1, 2]
        pi(nil) = []
        pi(n____) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            __#_A(x1,x2) = (0,0)
            ___A(x1,x2) = x1 + x2 + (1,1)
            nil_A() = (1,1)
            n_____A(x1,x2) = (0,0)
    
      precedence:
      
        __# = __ = nil = n____
      
      partial status:
    
        pi(__#) = []
        pi(__) = []
        pi(nil) = []
        pi(n____) = []
    

The next rules are strictly ordered:

  p1

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