YES

We show the termination of the TRS R:

  a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
  a____(X,nil()) -> mark(X)
  a____(nil(),X) -> mark(X)
  a__U11(tt()) -> tt()
  a__U21(tt(),V2) -> a__U22(a__isList(V2))
  a__U22(tt()) -> tt()
  a__U31(tt()) -> tt()
  a__U41(tt(),V2) -> a__U42(a__isNeList(V2))
  a__U42(tt()) -> tt()
  a__U51(tt(),V2) -> a__U52(a__isList(V2))
  a__U52(tt()) -> tt()
  a__U61(tt()) -> tt()
  a__U71(tt(),P) -> a__U72(a__isPal(P))
  a__U72(tt()) -> tt()
  a__U81(tt()) -> tt()
  a__isList(V) -> a__U11(a__isNeList(V))
  a__isList(nil()) -> tt()
  a__isList(__(V1,V2)) -> a__U21(a__isList(V1),V2)
  a__isNeList(V) -> a__U31(a__isQid(V))
  a__isNeList(__(V1,V2)) -> a__U41(a__isList(V1),V2)
  a__isNeList(__(V1,V2)) -> a__U51(a__isNeList(V1),V2)
  a__isNePal(V) -> a__U61(a__isQid(V))
  a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),P)
  a__isPal(V) -> a__U81(a__isNePal(V))
  a__isPal(nil()) -> tt()
  a__isQid(a()) -> tt()
  a__isQid(e()) -> tt()
  a__isQid(i()) -> tt()
  a__isQid(o()) -> tt()
  a__isQid(u()) -> tt()
  mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
  mark(U11(X)) -> a__U11(mark(X))
  mark(U21(X1,X2)) -> a__U21(mark(X1),X2)
  mark(U22(X)) -> a__U22(mark(X))
  mark(isList(X)) -> a__isList(X)
  mark(U31(X)) -> a__U31(mark(X))
  mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
  mark(U42(X)) -> a__U42(mark(X))
  mark(isNeList(X)) -> a__isNeList(X)
  mark(U51(X1,X2)) -> a__U51(mark(X1),X2)
  mark(U52(X)) -> a__U52(mark(X))
  mark(U61(X)) -> a__U61(mark(X))
  mark(U71(X1,X2)) -> a__U71(mark(X1),X2)
  mark(U72(X)) -> a__U72(mark(X))
  mark(isPal(X)) -> a__isPal(X)
  mark(U81(X)) -> a__U81(mark(X))
  mark(isQid(X)) -> a__isQid(X)
  mark(isNePal(X)) -> a__isNePal(X)
  mark(nil()) -> nil()
  mark(tt()) -> tt()
  mark(a()) -> a()
  mark(e()) -> e()
  mark(i()) -> i()
  mark(o()) -> o()
  mark(u()) -> u()
  a____(X1,X2) -> __(X1,X2)
  a__U11(X) -> U11(X)
  a__U21(X1,X2) -> U21(X1,X2)
  a__U22(X) -> U22(X)
  a__isList(X) -> isList(X)
  a__U31(X) -> U31(X)
  a__U41(X1,X2) -> U41(X1,X2)
  a__U42(X) -> U42(X)
  a__isNeList(X) -> isNeList(X)
  a__U51(X1,X2) -> U51(X1,X2)
  a__U52(X) -> U52(X)
  a__U61(X) -> U61(X)
  a__U71(X1,X2) -> U71(X1,X2)
  a__U72(X) -> U72(X)
  a__isPal(X) -> isPal(X)
  a__U81(X) -> U81(X)
  a__isQid(X) -> isQid(X)
  a__isNePal(X) -> isNePal(X)

-- SCC decomposition.

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

p1: a____#(__(X,Y),Z) -> a____#(mark(X),a____(mark(Y),mark(Z)))
p2: a____#(__(X,Y),Z) -> mark#(X)
p3: a____#(__(X,Y),Z) -> a____#(mark(Y),mark(Z))
p4: a____#(__(X,Y),Z) -> mark#(Y)
p5: a____#(__(X,Y),Z) -> mark#(Z)
p6: a____#(X,nil()) -> mark#(X)
p7: a____#(nil(),X) -> mark#(X)
p8: a__U21#(tt(),V2) -> a__U22#(a__isList(V2))
p9: a__U21#(tt(),V2) -> a__isList#(V2)
p10: a__U41#(tt(),V2) -> a__U42#(a__isNeList(V2))
p11: a__U41#(tt(),V2) -> a__isNeList#(V2)
p12: a__U51#(tt(),V2) -> a__U52#(a__isList(V2))
p13: a__U51#(tt(),V2) -> a__isList#(V2)
p14: a__U71#(tt(),P) -> a__U72#(a__isPal(P))
p15: a__U71#(tt(),P) -> a__isPal#(P)
p16: a__isList#(V) -> a__U11#(a__isNeList(V))
p17: a__isList#(V) -> a__isNeList#(V)
p18: a__isList#(__(V1,V2)) -> a__U21#(a__isList(V1),V2)
p19: a__isList#(__(V1,V2)) -> a__isList#(V1)
p20: a__isNeList#(V) -> a__U31#(a__isQid(V))
p21: a__isNeList#(V) -> a__isQid#(V)
p22: a__isNeList#(__(V1,V2)) -> a__U41#(a__isList(V1),V2)
p23: a__isNeList#(__(V1,V2)) -> a__isList#(V1)
p24: a__isNeList#(__(V1,V2)) -> a__U51#(a__isNeList(V1),V2)
p25: a__isNeList#(__(V1,V2)) -> a__isNeList#(V1)
p26: a__isNePal#(V) -> a__U61#(a__isQid(V))
p27: a__isNePal#(V) -> a__isQid#(V)
p28: a__isNePal#(__(I,__(P,I))) -> a__U71#(a__isQid(I),P)
p29: a__isNePal#(__(I,__(P,I))) -> a__isQid#(I)
p30: a__isPal#(V) -> a__U81#(a__isNePal(V))
p31: a__isPal#(V) -> a__isNePal#(V)
p32: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p33: mark#(__(X1,X2)) -> mark#(X1)
p34: mark#(__(X1,X2)) -> mark#(X2)
p35: mark#(U11(X)) -> a__U11#(mark(X))
p36: mark#(U11(X)) -> mark#(X)
p37: mark#(U21(X1,X2)) -> a__U21#(mark(X1),X2)
p38: mark#(U21(X1,X2)) -> mark#(X1)
p39: mark#(U22(X)) -> a__U22#(mark(X))
p40: mark#(U22(X)) -> mark#(X)
p41: mark#(isList(X)) -> a__isList#(X)
p42: mark#(U31(X)) -> a__U31#(mark(X))
p43: mark#(U31(X)) -> mark#(X)
p44: mark#(U41(X1,X2)) -> a__U41#(mark(X1),X2)
p45: mark#(U41(X1,X2)) -> mark#(X1)
p46: mark#(U42(X)) -> a__U42#(mark(X))
p47: mark#(U42(X)) -> mark#(X)
p48: mark#(isNeList(X)) -> a__isNeList#(X)
p49: mark#(U51(X1,X2)) -> a__U51#(mark(X1),X2)
p50: mark#(U51(X1,X2)) -> mark#(X1)
p51: mark#(U52(X)) -> a__U52#(mark(X))
p52: mark#(U52(X)) -> mark#(X)
p53: mark#(U61(X)) -> a__U61#(mark(X))
p54: mark#(U61(X)) -> mark#(X)
p55: mark#(U71(X1,X2)) -> a__U71#(mark(X1),X2)
p56: mark#(U71(X1,X2)) -> mark#(X1)
p57: mark#(U72(X)) -> a__U72#(mark(X))
p58: mark#(U72(X)) -> mark#(X)
p59: mark#(isPal(X)) -> a__isPal#(X)
p60: mark#(U81(X)) -> a__U81#(mark(X))
p61: mark#(U81(X)) -> mark#(X)
p62: mark#(isQid(X)) -> a__isQid#(X)
p63: mark#(isNePal(X)) -> a__isNePal#(X)

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt()) -> tt()
r5: a__U21(tt(),V2) -> a__U22(a__isList(V2))
r6: a__U22(tt()) -> tt()
r7: a__U31(tt()) -> tt()
r8: a__U41(tt(),V2) -> a__U42(a__isNeList(V2))
r9: a__U42(tt()) -> tt()
r10: a__U51(tt(),V2) -> a__U52(a__isList(V2))
r11: a__U52(tt()) -> tt()
r12: a__U61(tt()) -> tt()
r13: a__U71(tt(),P) -> a__U72(a__isPal(P))
r14: a__U72(tt()) -> tt()
r15: a__U81(tt()) -> tt()
r16: a__isList(V) -> a__U11(a__isNeList(V))
r17: a__isList(nil()) -> tt()
r18: a__isList(__(V1,V2)) -> a__U21(a__isList(V1),V2)
r19: a__isNeList(V) -> a__U31(a__isQid(V))
r20: a__isNeList(__(V1,V2)) -> a__U41(a__isList(V1),V2)
r21: a__isNeList(__(V1,V2)) -> a__U51(a__isNeList(V1),V2)
r22: a__isNePal(V) -> a__U61(a__isQid(V))
r23: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),P)
r24: a__isPal(V) -> a__U81(a__isNePal(V))
r25: a__isPal(nil()) -> tt()
r26: a__isQid(a()) -> tt()
r27: a__isQid(e()) -> tt()
r28: a__isQid(i()) -> tt()
r29: a__isQid(o()) -> tt()
r30: a__isQid(u()) -> tt()
r31: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r32: mark(U11(X)) -> a__U11(mark(X))
r33: mark(U21(X1,X2)) -> a__U21(mark(X1),X2)
r34: mark(U22(X)) -> a__U22(mark(X))
r35: mark(isList(X)) -> a__isList(X)
r36: mark(U31(X)) -> a__U31(mark(X))
r37: mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
r38: mark(U42(X)) -> a__U42(mark(X))
r39: mark(isNeList(X)) -> a__isNeList(X)
r40: mark(U51(X1,X2)) -> a__U51(mark(X1),X2)
r41: mark(U52(X)) -> a__U52(mark(X))
r42: mark(U61(X)) -> a__U61(mark(X))
r43: mark(U71(X1,X2)) -> a__U71(mark(X1),X2)
r44: mark(U72(X)) -> a__U72(mark(X))
r45: mark(isPal(X)) -> a__isPal(X)
r46: mark(U81(X)) -> a__U81(mark(X))
r47: mark(isQid(X)) -> a__isQid(X)
r48: mark(isNePal(X)) -> a__isNePal(X)
r49: mark(nil()) -> nil()
r50: mark(tt()) -> tt()
r51: mark(a()) -> a()
r52: mark(e()) -> e()
r53: mark(i()) -> i()
r54: mark(o()) -> o()
r55: mark(u()) -> u()
r56: a____(X1,X2) -> __(X1,X2)
r57: a__U11(X) -> U11(X)
r58: a__U21(X1,X2) -> U21(X1,X2)
r59: a__U22(X) -> U22(X)
r60: a__isList(X) -> isList(X)
r61: a__U31(X) -> U31(X)
r62: a__U41(X1,X2) -> U41(X1,X2)
r63: a__U42(X) -> U42(X)
r64: a__isNeList(X) -> isNeList(X)
r65: a__U51(X1,X2) -> U51(X1,X2)
r66: a__U52(X) -> U52(X)
r67: a__U61(X) -> U61(X)
r68: a__U71(X1,X2) -> U71(X1,X2)
r69: a__U72(X) -> U72(X)
r70: a__isPal(X) -> isPal(X)
r71: a__U81(X) -> U81(X)
r72: a__isQid(X) -> isQid(X)
r73: a__isNePal(X) -> isNePal(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p32, p33, p34, p36, p38, p40, p43, p45, p47, p50, p52, p54, p56, p58, p61}
  {p9, p11, p13, p17, p18, p19, p22, p23, p24, p25}
  {p15, p28, p31}


-- Reduction pair.

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

p1: a____#(__(X,Y),Z) -> a____#(mark(X),a____(mark(Y),mark(Z)))
p2: a____#(nil(),X) -> mark#(X)
p3: mark#(U81(X)) -> mark#(X)
p4: mark#(U72(X)) -> mark#(X)
p5: mark#(U71(X1,X2)) -> mark#(X1)
p6: mark#(U61(X)) -> mark#(X)
p7: mark#(U52(X)) -> mark#(X)
p8: mark#(U51(X1,X2)) -> mark#(X1)
p9: mark#(U42(X)) -> mark#(X)
p10: mark#(U41(X1,X2)) -> mark#(X1)
p11: mark#(U31(X)) -> mark#(X)
p12: mark#(U22(X)) -> mark#(X)
p13: mark#(U21(X1,X2)) -> mark#(X1)
p14: mark#(U11(X)) -> mark#(X)
p15: mark#(__(X1,X2)) -> mark#(X2)
p16: mark#(__(X1,X2)) -> mark#(X1)
p17: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p18: a____#(X,nil()) -> mark#(X)
p19: a____#(__(X,Y),Z) -> mark#(Z)
p20: a____#(__(X,Y),Z) -> mark#(Y)
p21: a____#(__(X,Y),Z) -> a____#(mark(Y),mark(Z))
p22: a____#(__(X,Y),Z) -> mark#(X)

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt()) -> tt()
r5: a__U21(tt(),V2) -> a__U22(a__isList(V2))
r6: a__U22(tt()) -> tt()
r7: a__U31(tt()) -> tt()
r8: a__U41(tt(),V2) -> a__U42(a__isNeList(V2))
r9: a__U42(tt()) -> tt()
r10: a__U51(tt(),V2) -> a__U52(a__isList(V2))
r11: a__U52(tt()) -> tt()
r12: a__U61(tt()) -> tt()
r13: a__U71(tt(),P) -> a__U72(a__isPal(P))
r14: a__U72(tt()) -> tt()
r15: a__U81(tt()) -> tt()
r16: a__isList(V) -> a__U11(a__isNeList(V))
r17: a__isList(nil()) -> tt()
r18: a__isList(__(V1,V2)) -> a__U21(a__isList(V1),V2)
r19: a__isNeList(V) -> a__U31(a__isQid(V))
r20: a__isNeList(__(V1,V2)) -> a__U41(a__isList(V1),V2)
r21: a__isNeList(__(V1,V2)) -> a__U51(a__isNeList(V1),V2)
r22: a__isNePal(V) -> a__U61(a__isQid(V))
r23: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),P)
r24: a__isPal(V) -> a__U81(a__isNePal(V))
r25: a__isPal(nil()) -> tt()
r26: a__isQid(a()) -> tt()
r27: a__isQid(e()) -> tt()
r28: a__isQid(i()) -> tt()
r29: a__isQid(o()) -> tt()
r30: a__isQid(u()) -> tt()
r31: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r32: mark(U11(X)) -> a__U11(mark(X))
r33: mark(U21(X1,X2)) -> a__U21(mark(X1),X2)
r34: mark(U22(X)) -> a__U22(mark(X))
r35: mark(isList(X)) -> a__isList(X)
r36: mark(U31(X)) -> a__U31(mark(X))
r37: mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
r38: mark(U42(X)) -> a__U42(mark(X))
r39: mark(isNeList(X)) -> a__isNeList(X)
r40: mark(U51(X1,X2)) -> a__U51(mark(X1),X2)
r41: mark(U52(X)) -> a__U52(mark(X))
r42: mark(U61(X)) -> a__U61(mark(X))
r43: mark(U71(X1,X2)) -> a__U71(mark(X1),X2)
r44: mark(U72(X)) -> a__U72(mark(X))
r45: mark(isPal(X)) -> a__isPal(X)
r46: mark(U81(X)) -> a__U81(mark(X))
r47: mark(isQid(X)) -> a__isQid(X)
r48: mark(isNePal(X)) -> a__isNePal(X)
r49: mark(nil()) -> nil()
r50: mark(tt()) -> tt()
r51: mark(a()) -> a()
r52: mark(e()) -> e()
r53: mark(i()) -> i()
r54: mark(o()) -> o()
r55: mark(u()) -> u()
r56: a____(X1,X2) -> __(X1,X2)
r57: a__U11(X) -> U11(X)
r58: a__U21(X1,X2) -> U21(X1,X2)
r59: a__U22(X) -> U22(X)
r60: a__isList(X) -> isList(X)
r61: a__U31(X) -> U31(X)
r62: a__U41(X1,X2) -> U41(X1,X2)
r63: a__U42(X) -> U42(X)
r64: a__isNeList(X) -> isNeList(X)
r65: a__U51(X1,X2) -> U51(X1,X2)
r66: a__U52(X) -> U52(X)
r67: a__U61(X) -> U61(X)
r68: a__U71(X1,X2) -> U71(X1,X2)
r69: a__U72(X) -> U72(X)
r70: a__isPal(X) -> isPal(X)
r71: a__U81(X) -> U81(X)
r72: a__isQid(X) -> isQid(X)
r73: a__isNePal(X) -> isNePal(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a____#_A(x1,x2) = x1 + x2 + 1
        ___A(x1,x2) = x1 + x2 + 7
        mark_A(x1) = x1
        a_____A(x1,x2) = x1 + x2 + 7
        nil_A() = 0
        mark#_A(x1) = x1
        U81_A(x1) = x1 + 1
        U72_A(x1) = x1
        U71_A(x1,x2) = x1 + x2 + 5
        U61_A(x1) = x1 + 1
        U52_A(x1) = x1 + 1
        U51_A(x1,x2) = x1 + x2 + 6
        U42_A(x1) = x1 + 1
        U41_A(x1,x2) = x1 + x2 + 4
        U31_A(x1) = x1 + 1
        U22_A(x1) = x1
        U21_A(x1,x2) = x1 + x2 + 4
        U11_A(x1) = x1 + 1
        a__U11_A(x1) = x1 + 1
        tt_A() = 0
        a__U21_A(x1,x2) = x1 + x2 + 4
        a__U22_A(x1) = x1
        a__isList_A(x1) = x1 + 4
        a__U31_A(x1) = x1 + 1
        a__U41_A(x1,x2) = x1 + x2 + 4
        a__U42_A(x1) = x1 + 1
        a__isNeList_A(x1) = x1 + 2
        a__U51_A(x1,x2) = x1 + x2 + 6
        a__U52_A(x1) = x1 + 1
        a__U61_A(x1) = x1 + 1
        a__U71_A(x1,x2) = x1 + x2 + 5
        a__U72_A(x1) = x1
        a__isPal_A(x1) = x1 + 4
        a__U81_A(x1) = x1 + 1
        a__isQid_A(x1) = 0
        a__isNePal_A(x1) = x1 + 2
        a_A() = 1
        e_A() = 1
        i_A() = 1
        o_A() = 1
        u_A() = 1
        isList_A(x1) = x1 + 4
        isNeList_A(x1) = x1 + 2
        isPal_A(x1) = x1 + 4
        isQid_A(x1) = 0
        isNePal_A(x1) = x1 + 2
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        a__U61 > mark > U31 > a____ > __ > a____# > a__isNePal > isNePal > a__isQid > isQid > a__isNeList > a__isList > a__isPal > isPal > a__U51 > a__U52 > a__U21 > a__U22 > isNeList > isList > u > o > i > e > a > a__U71 > a__U72 > tt > a__U81 > a__U31 > a__U42 > a__U41 > a__U11 > U11 > U21 > U22 > U41 > U42 > U51 > U52 > U61 > U71 > U72 > U81 > nil > mark#
      
      argument filter:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(nil) = []
        pi(mark#) = []
        pi(U81) = []
        pi(U72) = []
        pi(U71) = 1
        pi(U61) = 1
        pi(U52) = []
        pi(U51) = 1
        pi(U42) = []
        pi(U41) = []
        pi(U31) = 1
        pi(U22) = []
        pi(U21) = []
        pi(U11) = 1
        pi(a__U11) = 1
        pi(tt) = []
        pi(a__U21) = []
        pi(a__U22) = []
        pi(a__isList) = []
        pi(a__U31) = 1
        pi(a__U41) = []
        pi(a__U42) = []
        pi(a__isNeList) = []
        pi(a__U51) = 1
        pi(a__U52) = []
        pi(a__U61) = 1
        pi(a__U71) = 1
        pi(a__U72) = []
        pi(a__isPal) = []
        pi(a__U81) = []
        pi(a__isQid) = []
        pi(a__isNePal) = []
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
        pi(isList) = []
        pi(isNeList) = []
        pi(isPal) = []
        pi(isQid) = []
        pi(isNePal) = []
    

The next rules are strictly ordered:

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

We remove them from the problem.

-- SCC decomposition.

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

p1: a____#(__(X,Y),Z) -> a____#(mark(X),a____(mark(Y),mark(Z)))
p2: mark#(U72(X)) -> mark#(X)
p3: mark#(U22(X)) -> mark#(X)

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt()) -> tt()
r5: a__U21(tt(),V2) -> a__U22(a__isList(V2))
r6: a__U22(tt()) -> tt()
r7: a__U31(tt()) -> tt()
r8: a__U41(tt(),V2) -> a__U42(a__isNeList(V2))
r9: a__U42(tt()) -> tt()
r10: a__U51(tt(),V2) -> a__U52(a__isList(V2))
r11: a__U52(tt()) -> tt()
r12: a__U61(tt()) -> tt()
r13: a__U71(tt(),P) -> a__U72(a__isPal(P))
r14: a__U72(tt()) -> tt()
r15: a__U81(tt()) -> tt()
r16: a__isList(V) -> a__U11(a__isNeList(V))
r17: a__isList(nil()) -> tt()
r18: a__isList(__(V1,V2)) -> a__U21(a__isList(V1),V2)
r19: a__isNeList(V) -> a__U31(a__isQid(V))
r20: a__isNeList(__(V1,V2)) -> a__U41(a__isList(V1),V2)
r21: a__isNeList(__(V1,V2)) -> a__U51(a__isNeList(V1),V2)
r22: a__isNePal(V) -> a__U61(a__isQid(V))
r23: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),P)
r24: a__isPal(V) -> a__U81(a__isNePal(V))
r25: a__isPal(nil()) -> tt()
r26: a__isQid(a()) -> tt()
r27: a__isQid(e()) -> tt()
r28: a__isQid(i()) -> tt()
r29: a__isQid(o()) -> tt()
r30: a__isQid(u()) -> tt()
r31: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r32: mark(U11(X)) -> a__U11(mark(X))
r33: mark(U21(X1,X2)) -> a__U21(mark(X1),X2)
r34: mark(U22(X)) -> a__U22(mark(X))
r35: mark(isList(X)) -> a__isList(X)
r36: mark(U31(X)) -> a__U31(mark(X))
r37: mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
r38: mark(U42(X)) -> a__U42(mark(X))
r39: mark(isNeList(X)) -> a__isNeList(X)
r40: mark(U51(X1,X2)) -> a__U51(mark(X1),X2)
r41: mark(U52(X)) -> a__U52(mark(X))
r42: mark(U61(X)) -> a__U61(mark(X))
r43: mark(U71(X1,X2)) -> a__U71(mark(X1),X2)
r44: mark(U72(X)) -> a__U72(mark(X))
r45: mark(isPal(X)) -> a__isPal(X)
r46: mark(U81(X)) -> a__U81(mark(X))
r47: mark(isQid(X)) -> a__isQid(X)
r48: mark(isNePal(X)) -> a__isNePal(X)
r49: mark(nil()) -> nil()
r50: mark(tt()) -> tt()
r51: mark(a()) -> a()
r52: mark(e()) -> e()
r53: mark(i()) -> i()
r54: mark(o()) -> o()
r55: mark(u()) -> u()
r56: a____(X1,X2) -> __(X1,X2)
r57: a__U11(X) -> U11(X)
r58: a__U21(X1,X2) -> U21(X1,X2)
r59: a__U22(X) -> U22(X)
r60: a__isList(X) -> isList(X)
r61: a__U31(X) -> U31(X)
r62: a__U41(X1,X2) -> U41(X1,X2)
r63: a__U42(X) -> U42(X)
r64: a__isNeList(X) -> isNeList(X)
r65: a__U51(X1,X2) -> U51(X1,X2)
r66: a__U52(X) -> U52(X)
r67: a__U61(X) -> U61(X)
r68: a__U71(X1,X2) -> U71(X1,X2)
r69: a__U72(X) -> U72(X)
r70: a__isPal(X) -> isPal(X)
r71: a__U81(X) -> U81(X)
r72: a__isQid(X) -> isQid(X)
r73: a__isNePal(X) -> isNePal(X)

The estimated dependency graph contains the following SCCs:

  {p1}
  {p2, p3}


-- Reduction pair.

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

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

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt()) -> tt()
r5: a__U21(tt(),V2) -> a__U22(a__isList(V2))
r6: a__U22(tt()) -> tt()
r7: a__U31(tt()) -> tt()
r8: a__U41(tt(),V2) -> a__U42(a__isNeList(V2))
r9: a__U42(tt()) -> tt()
r10: a__U51(tt(),V2) -> a__U52(a__isList(V2))
r11: a__U52(tt()) -> tt()
r12: a__U61(tt()) -> tt()
r13: a__U71(tt(),P) -> a__U72(a__isPal(P))
r14: a__U72(tt()) -> tt()
r15: a__U81(tt()) -> tt()
r16: a__isList(V) -> a__U11(a__isNeList(V))
r17: a__isList(nil()) -> tt()
r18: a__isList(__(V1,V2)) -> a__U21(a__isList(V1),V2)
r19: a__isNeList(V) -> a__U31(a__isQid(V))
r20: a__isNeList(__(V1,V2)) -> a__U41(a__isList(V1),V2)
r21: a__isNeList(__(V1,V2)) -> a__U51(a__isNeList(V1),V2)
r22: a__isNePal(V) -> a__U61(a__isQid(V))
r23: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),P)
r24: a__isPal(V) -> a__U81(a__isNePal(V))
r25: a__isPal(nil()) -> tt()
r26: a__isQid(a()) -> tt()
r27: a__isQid(e()) -> tt()
r28: a__isQid(i()) -> tt()
r29: a__isQid(o()) -> tt()
r30: a__isQid(u()) -> tt()
r31: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r32: mark(U11(X)) -> a__U11(mark(X))
r33: mark(U21(X1,X2)) -> a__U21(mark(X1),X2)
r34: mark(U22(X)) -> a__U22(mark(X))
r35: mark(isList(X)) -> a__isList(X)
r36: mark(U31(X)) -> a__U31(mark(X))
r37: mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
r38: mark(U42(X)) -> a__U42(mark(X))
r39: mark(isNeList(X)) -> a__isNeList(X)
r40: mark(U51(X1,X2)) -> a__U51(mark(X1),X2)
r41: mark(U52(X)) -> a__U52(mark(X))
r42: mark(U61(X)) -> a__U61(mark(X))
r43: mark(U71(X1,X2)) -> a__U71(mark(X1),X2)
r44: mark(U72(X)) -> a__U72(mark(X))
r45: mark(isPal(X)) -> a__isPal(X)
r46: mark(U81(X)) -> a__U81(mark(X))
r47: mark(isQid(X)) -> a__isQid(X)
r48: mark(isNePal(X)) -> a__isNePal(X)
r49: mark(nil()) -> nil()
r50: mark(tt()) -> tt()
r51: mark(a()) -> a()
r52: mark(e()) -> e()
r53: mark(i()) -> i()
r54: mark(o()) -> o()
r55: mark(u()) -> u()
r56: a____(X1,X2) -> __(X1,X2)
r57: a__U11(X) -> U11(X)
r58: a__U21(X1,X2) -> U21(X1,X2)
r59: a__U22(X) -> U22(X)
r60: a__isList(X) -> isList(X)
r61: a__U31(X) -> U31(X)
r62: a__U41(X1,X2) -> U41(X1,X2)
r63: a__U42(X) -> U42(X)
r64: a__isNeList(X) -> isNeList(X)
r65: a__U51(X1,X2) -> U51(X1,X2)
r66: a__U52(X) -> U52(X)
r67: a__U61(X) -> U61(X)
r68: a__U71(X1,X2) -> U71(X1,X2)
r69: a__U72(X) -> U72(X)
r70: a__isPal(X) -> isPal(X)
r71: a__U81(X) -> U81(X)
r72: a__isQid(X) -> isQid(X)
r73: a__isNePal(X) -> isNePal(X)

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a____#_A(x1,x2) = x1
        ___A(x1,x2) = x1 + x2 + 3
        mark_A(x1) = x1
        a_____A(x1,x2) = x1 + x2 + 3
        a__U11_A(x1) = 2
        tt_A() = 1
        a__U21_A(x1,x2) = x1 + x2 + 2
        a__U22_A(x1) = 2
        a__isList_A(x1) = x1 + 3
        a__U31_A(x1) = 2
        a__U41_A(x1,x2) = 3
        a__U42_A(x1) = 2
        a__isNeList_A(x1) = 4
        a__U51_A(x1,x2) = 3
        a__U52_A(x1) = 2
        a__U61_A(x1) = 2
        a__U71_A(x1,x2) = x2 + 7
        a__U72_A(x1) = x1 + 1
        a__isPal_A(x1) = x1 + 5
        a__U81_A(x1) = x1 + 1
        nil_A() = 1
        a__isQid_A(x1) = 2
        a__isNePal_A(x1) = x1 + 3
        a_A() = 1
        e_A() = 1
        i_A() = 1
        o_A() = 1
        u_A() = 1
        U11_A(x1) = 2
        U21_A(x1,x2) = x1 + x2 + 2
        U22_A(x1) = 2
        isList_A(x1) = x1 + 3
        U31_A(x1) = 2
        U41_A(x1,x2) = 3
        U42_A(x1) = 2
        isNeList_A(x1) = 4
        U51_A(x1,x2) = 3
        U52_A(x1) = 2
        U61_A(x1) = 2
        U71_A(x1,x2) = x2 + 7
        U72_A(x1) = x1 + 1
        isPal_A(x1) = x1 + 5
        U81_A(x1) = x1 + 1
        isQid_A(x1) = 2
        isNePal_A(x1) = x1 + 3
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        a__U81 > U81 > mark > a__U61 > a__isNePal > isNePal > a__isQid > isQid > a__isPal > isPal > U72 > a__U41 > a__U71 > U71 > U61 > a__U52 > U52 > a__isList > a__U51 > U51 > a__U31 > a__isNeList > isNeList > a__U42 > U42 > U41 > U31 > isList > a__U22 > U22 > a__U21 > U21 > a__U11 > U11 > tt > u > o > i > e > a > nil > a__U72 > a____ > __ > a____#
      
      argument filter:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(a__U11) = []
        pi(tt) = []
        pi(a__U21) = []
        pi(a__U22) = []
        pi(a__isList) = []
        pi(a__U31) = []
        pi(a__U41) = []
        pi(a__U42) = []
        pi(a__isNeList) = []
        pi(a__U51) = []
        pi(a__U52) = []
        pi(a__U61) = []
        pi(a__U71) = []
        pi(a__U72) = 1
        pi(a__isPal) = []
        pi(a__U81) = 1
        pi(nil) = []
        pi(a__isQid) = []
        pi(a__isNePal) = []
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
        pi(U11) = []
        pi(U21) = []
        pi(U22) = []
        pi(isList) = []
        pi(U31) = []
        pi(U41) = []
        pi(U42) = []
        pi(isNeList) = []
        pi(U51) = []
        pi(U52) = []
        pi(U61) = []
        pi(U71) = []
        pi(U72) = 1
        pi(isPal) = []
        pi(U81) = 1
        pi(isQid) = []
        pi(isNePal) = []
    

The next rules are strictly ordered:

  p1

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

-- Reduction pair.

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

p1: mark#(U72(X)) -> mark#(X)
p2: mark#(U22(X)) -> mark#(X)

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt()) -> tt()
r5: a__U21(tt(),V2) -> a__U22(a__isList(V2))
r6: a__U22(tt()) -> tt()
r7: a__U31(tt()) -> tt()
r8: a__U41(tt(),V2) -> a__U42(a__isNeList(V2))
r9: a__U42(tt()) -> tt()
r10: a__U51(tt(),V2) -> a__U52(a__isList(V2))
r11: a__U52(tt()) -> tt()
r12: a__U61(tt()) -> tt()
r13: a__U71(tt(),P) -> a__U72(a__isPal(P))
r14: a__U72(tt()) -> tt()
r15: a__U81(tt()) -> tt()
r16: a__isList(V) -> a__U11(a__isNeList(V))
r17: a__isList(nil()) -> tt()
r18: a__isList(__(V1,V2)) -> a__U21(a__isList(V1),V2)
r19: a__isNeList(V) -> a__U31(a__isQid(V))
r20: a__isNeList(__(V1,V2)) -> a__U41(a__isList(V1),V2)
r21: a__isNeList(__(V1,V2)) -> a__U51(a__isNeList(V1),V2)
r22: a__isNePal(V) -> a__U61(a__isQid(V))
r23: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),P)
r24: a__isPal(V) -> a__U81(a__isNePal(V))
r25: a__isPal(nil()) -> tt()
r26: a__isQid(a()) -> tt()
r27: a__isQid(e()) -> tt()
r28: a__isQid(i()) -> tt()
r29: a__isQid(o()) -> tt()
r30: a__isQid(u()) -> tt()
r31: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r32: mark(U11(X)) -> a__U11(mark(X))
r33: mark(U21(X1,X2)) -> a__U21(mark(X1),X2)
r34: mark(U22(X)) -> a__U22(mark(X))
r35: mark(isList(X)) -> a__isList(X)
r36: mark(U31(X)) -> a__U31(mark(X))
r37: mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
r38: mark(U42(X)) -> a__U42(mark(X))
r39: mark(isNeList(X)) -> a__isNeList(X)
r40: mark(U51(X1,X2)) -> a__U51(mark(X1),X2)
r41: mark(U52(X)) -> a__U52(mark(X))
r42: mark(U61(X)) -> a__U61(mark(X))
r43: mark(U71(X1,X2)) -> a__U71(mark(X1),X2)
r44: mark(U72(X)) -> a__U72(mark(X))
r45: mark(isPal(X)) -> a__isPal(X)
r46: mark(U81(X)) -> a__U81(mark(X))
r47: mark(isQid(X)) -> a__isQid(X)
r48: mark(isNePal(X)) -> a__isNePal(X)
r49: mark(nil()) -> nil()
r50: mark(tt()) -> tt()
r51: mark(a()) -> a()
r52: mark(e()) -> e()
r53: mark(i()) -> i()
r54: mark(o()) -> o()
r55: mark(u()) -> u()
r56: a____(X1,X2) -> __(X1,X2)
r57: a__U11(X) -> U11(X)
r58: a__U21(X1,X2) -> U21(X1,X2)
r59: a__U22(X) -> U22(X)
r60: a__isList(X) -> isList(X)
r61: a__U31(X) -> U31(X)
r62: a__U41(X1,X2) -> U41(X1,X2)
r63: a__U42(X) -> U42(X)
r64: a__isNeList(X) -> isNeList(X)
r65: a__U51(X1,X2) -> U51(X1,X2)
r66: a__U52(X) -> U52(X)
r67: a__U61(X) -> U61(X)
r68: a__U71(X1,X2) -> U71(X1,X2)
r69: a__U72(X) -> U72(X)
r70: a__isPal(X) -> isPal(X)
r71: a__U81(X) -> U81(X)
r72: a__isQid(X) -> isQid(X)
r73: a__isNePal(X) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        mark#_A(x1) = x1
        U72_A(x1) = x1 + 1
        U22_A(x1) = x1 + 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        mark# > U22 > U72
      
      argument filter:
    
        pi(mark#) = 1
        pi(U72) = [1]
        pi(U22) = [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

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

-- Reduction pair.

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

p1: a__U21#(tt(),V2) -> a__isList#(V2)
p2: a__isList#(__(V1,V2)) -> a__isList#(V1)
p3: a__isList#(__(V1,V2)) -> a__U21#(a__isList(V1),V2)
p4: a__isList#(V) -> a__isNeList#(V)
p5: a__isNeList#(__(V1,V2)) -> a__isNeList#(V1)
p6: a__isNeList#(__(V1,V2)) -> a__U51#(a__isNeList(V1),V2)
p7: a__U51#(tt(),V2) -> a__isList#(V2)
p8: a__isNeList#(__(V1,V2)) -> a__isList#(V1)
p9: a__isNeList#(__(V1,V2)) -> a__U41#(a__isList(V1),V2)
p10: a__U41#(tt(),V2) -> a__isNeList#(V2)

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt()) -> tt()
r5: a__U21(tt(),V2) -> a__U22(a__isList(V2))
r6: a__U22(tt()) -> tt()
r7: a__U31(tt()) -> tt()
r8: a__U41(tt(),V2) -> a__U42(a__isNeList(V2))
r9: a__U42(tt()) -> tt()
r10: a__U51(tt(),V2) -> a__U52(a__isList(V2))
r11: a__U52(tt()) -> tt()
r12: a__U61(tt()) -> tt()
r13: a__U71(tt(),P) -> a__U72(a__isPal(P))
r14: a__U72(tt()) -> tt()
r15: a__U81(tt()) -> tt()
r16: a__isList(V) -> a__U11(a__isNeList(V))
r17: a__isList(nil()) -> tt()
r18: a__isList(__(V1,V2)) -> a__U21(a__isList(V1),V2)
r19: a__isNeList(V) -> a__U31(a__isQid(V))
r20: a__isNeList(__(V1,V2)) -> a__U41(a__isList(V1),V2)
r21: a__isNeList(__(V1,V2)) -> a__U51(a__isNeList(V1),V2)
r22: a__isNePal(V) -> a__U61(a__isQid(V))
r23: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),P)
r24: a__isPal(V) -> a__U81(a__isNePal(V))
r25: a__isPal(nil()) -> tt()
r26: a__isQid(a()) -> tt()
r27: a__isQid(e()) -> tt()
r28: a__isQid(i()) -> tt()
r29: a__isQid(o()) -> tt()
r30: a__isQid(u()) -> tt()
r31: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r32: mark(U11(X)) -> a__U11(mark(X))
r33: mark(U21(X1,X2)) -> a__U21(mark(X1),X2)
r34: mark(U22(X)) -> a__U22(mark(X))
r35: mark(isList(X)) -> a__isList(X)
r36: mark(U31(X)) -> a__U31(mark(X))
r37: mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
r38: mark(U42(X)) -> a__U42(mark(X))
r39: mark(isNeList(X)) -> a__isNeList(X)
r40: mark(U51(X1,X2)) -> a__U51(mark(X1),X2)
r41: mark(U52(X)) -> a__U52(mark(X))
r42: mark(U61(X)) -> a__U61(mark(X))
r43: mark(U71(X1,X2)) -> a__U71(mark(X1),X2)
r44: mark(U72(X)) -> a__U72(mark(X))
r45: mark(isPal(X)) -> a__isPal(X)
r46: mark(U81(X)) -> a__U81(mark(X))
r47: mark(isQid(X)) -> a__isQid(X)
r48: mark(isNePal(X)) -> a__isNePal(X)
r49: mark(nil()) -> nil()
r50: mark(tt()) -> tt()
r51: mark(a()) -> a()
r52: mark(e()) -> e()
r53: mark(i()) -> i()
r54: mark(o()) -> o()
r55: mark(u()) -> u()
r56: a____(X1,X2) -> __(X1,X2)
r57: a__U11(X) -> U11(X)
r58: a__U21(X1,X2) -> U21(X1,X2)
r59: a__U22(X) -> U22(X)
r60: a__isList(X) -> isList(X)
r61: a__U31(X) -> U31(X)
r62: a__U41(X1,X2) -> U41(X1,X2)
r63: a__U42(X) -> U42(X)
r64: a__isNeList(X) -> isNeList(X)
r65: a__U51(X1,X2) -> U51(X1,X2)
r66: a__U52(X) -> U52(X)
r67: a__U61(X) -> U61(X)
r68: a__U71(X1,X2) -> U71(X1,X2)
r69: a__U72(X) -> U72(X)
r70: a__isPal(X) -> isPal(X)
r71: a__U81(X) -> U81(X)
r72: a__isQid(X) -> isQid(X)
r73: a__isNePal(X) -> isNePal(X)

The set of usable rules consists of

  r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r72

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a__U21#_A(x1,x2) = x1 + x2 + 1
        tt_A() = 1
        a__isList#_A(x1) = x1 + 1
        ___A(x1,x2) = x1 + x2 + 7
        a__isList_A(x1) = x1 + 5
        a__isNeList#_A(x1) = x1
        a__U51#_A(x1,x2) = x1 + x2 + 1
        a__isNeList_A(x1) = x1 + 3
        a__U41#_A(x1,x2) = x2 + 1
        a__U22_A(x1) = x1 + 1
        a__U42_A(x1) = x1 + 1
        a__U52_A(x1) = x1 + 1
        U22_A(x1) = 0
        U42_A(x1) = 0
        U52_A(x1) = 0
        a__U11_A(x1) = x1 + 1
        a__U21_A(x1,x2) = x1 + x2 + 6
        a__U31_A(x1) = x1 + 1
        a__U41_A(x1,x2) = x1 + x2 + 4
        a__U51_A(x1,x2) = x1 + x2 + 6
        a__isQid_A(x1) = x1 + 1
        a_A() = 1
        e_A() = 1
        i_A() = 1
        o_A() = 1
        u_A() = 1
        U11_A(x1) = 0
        U21_A(x1,x2) = 5
        U31_A(x1) = 0
        U41_A(x1,x2) = 0
        U51_A(x1,x2) = 5
        isQid_A(x1) = 0
        nil_A() = 1
        isList_A(x1) = 0
        isNeList_A(x1) = 0
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        isList > a__U52 > a__isNeList# > U11 > __ > tt > nil > isQid > U51 > U41 > U31 > U21 > u > o > i > e > a > a__isQid > a__U51 > a__U41 > U22 > a__isList# > a__U21# > isNeList > a__U31 > a__U42 > a__U22 > a__U21 > a__U11 > U52 > U42 > a__U41# > a__isNeList > a__U51# > a__isList
      
      argument filter:
    
        pi(a__U21#) = 2
        pi(tt) = []
        pi(a__isList#) = 1
        pi(__) = 2
        pi(a__isList) = [1]
        pi(a__isNeList#) = 1
        pi(a__U51#) = [1, 2]
        pi(a__isNeList) = []
        pi(a__U41#) = 2
        pi(a__U22) = 1
        pi(a__U42) = 1
        pi(a__U52) = 1
        pi(U22) = []
        pi(U42) = []
        pi(U52) = []
        pi(a__U11) = [1]
        pi(a__U21) = 1
        pi(a__U31) = [1]
        pi(a__U41) = [1, 2]
        pi(a__U51) = [2]
        pi(a__isQid) = 1
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
        pi(U11) = []
        pi(U21) = []
        pi(U31) = []
        pi(U41) = []
        pi(U51) = []
        pi(isQid) = []
        pi(nil) = []
        pi(isList) = []
        pi(isNeList) = []
    

The next rules are strictly ordered:

  p1, p2, p3, p4, p5, p6, p7, p8, p9, p10

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

-- Reduction pair.

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

p1: a__U71#(tt(),P) -> a__isPal#(P)
p2: a__isPal#(V) -> a__isNePal#(V)
p3: a__isNePal#(__(I,__(P,I))) -> a__U71#(a__isQid(I),P)

and R consists of:

r1: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r2: a____(X,nil()) -> mark(X)
r3: a____(nil(),X) -> mark(X)
r4: a__U11(tt()) -> tt()
r5: a__U21(tt(),V2) -> a__U22(a__isList(V2))
r6: a__U22(tt()) -> tt()
r7: a__U31(tt()) -> tt()
r8: a__U41(tt(),V2) -> a__U42(a__isNeList(V2))
r9: a__U42(tt()) -> tt()
r10: a__U51(tt(),V2) -> a__U52(a__isList(V2))
r11: a__U52(tt()) -> tt()
r12: a__U61(tt()) -> tt()
r13: a__U71(tt(),P) -> a__U72(a__isPal(P))
r14: a__U72(tt()) -> tt()
r15: a__U81(tt()) -> tt()
r16: a__isList(V) -> a__U11(a__isNeList(V))
r17: a__isList(nil()) -> tt()
r18: a__isList(__(V1,V2)) -> a__U21(a__isList(V1),V2)
r19: a__isNeList(V) -> a__U31(a__isQid(V))
r20: a__isNeList(__(V1,V2)) -> a__U41(a__isList(V1),V2)
r21: a__isNeList(__(V1,V2)) -> a__U51(a__isNeList(V1),V2)
r22: a__isNePal(V) -> a__U61(a__isQid(V))
r23: a__isNePal(__(I,__(P,I))) -> a__U71(a__isQid(I),P)
r24: a__isPal(V) -> a__U81(a__isNePal(V))
r25: a__isPal(nil()) -> tt()
r26: a__isQid(a()) -> tt()
r27: a__isQid(e()) -> tt()
r28: a__isQid(i()) -> tt()
r29: a__isQid(o()) -> tt()
r30: a__isQid(u()) -> tt()
r31: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r32: mark(U11(X)) -> a__U11(mark(X))
r33: mark(U21(X1,X2)) -> a__U21(mark(X1),X2)
r34: mark(U22(X)) -> a__U22(mark(X))
r35: mark(isList(X)) -> a__isList(X)
r36: mark(U31(X)) -> a__U31(mark(X))
r37: mark(U41(X1,X2)) -> a__U41(mark(X1),X2)
r38: mark(U42(X)) -> a__U42(mark(X))
r39: mark(isNeList(X)) -> a__isNeList(X)
r40: mark(U51(X1,X2)) -> a__U51(mark(X1),X2)
r41: mark(U52(X)) -> a__U52(mark(X))
r42: mark(U61(X)) -> a__U61(mark(X))
r43: mark(U71(X1,X2)) -> a__U71(mark(X1),X2)
r44: mark(U72(X)) -> a__U72(mark(X))
r45: mark(isPal(X)) -> a__isPal(X)
r46: mark(U81(X)) -> a__U81(mark(X))
r47: mark(isQid(X)) -> a__isQid(X)
r48: mark(isNePal(X)) -> a__isNePal(X)
r49: mark(nil()) -> nil()
r50: mark(tt()) -> tt()
r51: mark(a()) -> a()
r52: mark(e()) -> e()
r53: mark(i()) -> i()
r54: mark(o()) -> o()
r55: mark(u()) -> u()
r56: a____(X1,X2) -> __(X1,X2)
r57: a__U11(X) -> U11(X)
r58: a__U21(X1,X2) -> U21(X1,X2)
r59: a__U22(X) -> U22(X)
r60: a__isList(X) -> isList(X)
r61: a__U31(X) -> U31(X)
r62: a__U41(X1,X2) -> U41(X1,X2)
r63: a__U42(X) -> U42(X)
r64: a__isNeList(X) -> isNeList(X)
r65: a__U51(X1,X2) -> U51(X1,X2)
r66: a__U52(X) -> U52(X)
r67: a__U61(X) -> U61(X)
r68: a__U71(X1,X2) -> U71(X1,X2)
r69: a__U72(X) -> U72(X)
r70: a__isPal(X) -> isPal(X)
r71: a__U81(X) -> U81(X)
r72: a__isQid(X) -> isQid(X)
r73: a__isNePal(X) -> isNePal(X)

The set of usable rules consists of

  r26, r27, r28, r29, r30, r72

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. matrix interpretations:
    
      carrier: N^1
      order: standard order
      interpretations:
        a__U71#_A(x1,x2) = x1 + x2
        tt_A() = 2
        a__isPal#_A(x1) = x1 + 1
        a__isNePal#_A(x1) = x1
        ___A(x1,x2) = x1 + x2 + 1
        a__isQid_A(x1) = x1 + 1
        a_A() = 2
        e_A() = 2
        i_A() = 2
        o_A() = 2
        u_A() = 2
        isQid_A(x1) = 0
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        isQid > tt > u > o > i > e > a > a__isQid > a__U71# > __ > a__isNePal# > a__isPal#
      
      argument filter:
    
        pi(a__U71#) = 1
        pi(tt) = []
        pi(a__isPal#) = []
        pi(a__isNePal#) = [1]
        pi(__) = 1
        pi(a__isQid) = 1
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
        pi(isQid) = []
    

The next rules are strictly ordered:

  p1, p2, p3

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