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__and(tt(),X) -> mark(X)
  a__isList(V) -> a__isNeList(V)
  a__isList(nil()) -> tt()
  a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
  a__isNeList(V) -> a__isQid(V)
  a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
  a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
  a__isNePal(V) -> a__isQid(V)
  a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
  a__isPal(V) -> 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(and(X1,X2)) -> a__and(mark(X1),X2)
  mark(isList(X)) -> a__isList(X)
  mark(isNeList(X)) -> a__isNeList(X)
  mark(isQid(X)) -> a__isQid(X)
  mark(isNePal(X)) -> a__isNePal(X)
  mark(isPal(X)) -> a__isPal(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__and(X1,X2) -> and(X1,X2)
  a__isList(X) -> isList(X)
  a__isNeList(X) -> isNeList(X)
  a__isQid(X) -> isQid(X)
  a__isNePal(X) -> isNePal(X)
  a__isPal(X) -> isPal(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__and#(tt(),X) -> mark#(X)
p9: a__isList#(V) -> a__isNeList#(V)
p10: a__isList#(__(V1,V2)) -> a__and#(a__isList(V1),isList(V2))
p11: a__isList#(__(V1,V2)) -> a__isList#(V1)
p12: a__isNeList#(V) -> a__isQid#(V)
p13: a__isNeList#(__(V1,V2)) -> a__and#(a__isList(V1),isNeList(V2))
p14: a__isNeList#(__(V1,V2)) -> a__isList#(V1)
p15: a__isNeList#(__(V1,V2)) -> a__and#(a__isNeList(V1),isList(V2))
p16: a__isNeList#(__(V1,V2)) -> a__isNeList#(V1)
p17: a__isNePal#(V) -> a__isQid#(V)
p18: a__isNePal#(__(I,__(P,I))) -> a__and#(a__isQid(I),isPal(P))
p19: a__isNePal#(__(I,__(P,I))) -> a__isQid#(I)
p20: a__isPal#(V) -> a__isNePal#(V)
p21: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p22: mark#(__(X1,X2)) -> mark#(X1)
p23: mark#(__(X1,X2)) -> mark#(X2)
p24: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p25: mark#(and(X1,X2)) -> mark#(X1)
p26: mark#(isList(X)) -> a__isList#(X)
p27: mark#(isNeList(X)) -> a__isNeList#(X)
p28: mark#(isQid(X)) -> a__isQid#(X)
p29: mark#(isNePal(X)) -> a__isNePal#(X)
p30: mark#(isPal(X)) -> a__isPal#(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__and(tt(),X) -> mark(X)
r5: a__isList(V) -> a__isNeList(V)
r6: a__isList(nil()) -> tt()
r7: a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
r8: a__isNeList(V) -> a__isQid(V)
r9: a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
r10: a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
r11: a__isNePal(V) -> a__isQid(V)
r12: a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
r13: a__isPal(V) -> a__isNePal(V)
r14: a__isPal(nil()) -> tt()
r15: a__isQid(a()) -> tt()
r16: a__isQid(e()) -> tt()
r17: a__isQid(i()) -> tt()
r18: a__isQid(o()) -> tt()
r19: a__isQid(u()) -> tt()
r20: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r21: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r22: mark(isList(X)) -> a__isList(X)
r23: mark(isNeList(X)) -> a__isNeList(X)
r24: mark(isQid(X)) -> a__isQid(X)
r25: mark(isNePal(X)) -> a__isNePal(X)
r26: mark(isPal(X)) -> a__isPal(X)
r27: mark(nil()) -> nil()
r28: mark(tt()) -> tt()
r29: mark(a()) -> a()
r30: mark(e()) -> e()
r31: mark(i()) -> i()
r32: mark(o()) -> o()
r33: mark(u()) -> u()
r34: a____(X1,X2) -> __(X1,X2)
r35: a__and(X1,X2) -> and(X1,X2)
r36: a__isList(X) -> isList(X)
r37: a__isNeList(X) -> isNeList(X)
r38: a__isQid(X) -> isQid(X)
r39: a__isNePal(X) -> isNePal(X)
r40: a__isPal(X) -> isPal(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p13, p14, p15, p16, p18, p20, p21, p22, p23, p24, p25, p26, p27, p29, p30}


-- 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#(isPal(X)) -> a__isPal#(X)
p4: a__isPal#(V) -> a__isNePal#(V)
p5: a__isNePal#(__(I,__(P,I))) -> a__and#(a__isQid(I),isPal(P))
p6: a__and#(tt(),X) -> mark#(X)
p7: mark#(isNePal(X)) -> a__isNePal#(X)
p8: mark#(isNeList(X)) -> a__isNeList#(X)
p9: a__isNeList#(__(V1,V2)) -> a__isNeList#(V1)
p10: a__isNeList#(__(V1,V2)) -> a__and#(a__isNeList(V1),isList(V2))
p11: a__isNeList#(__(V1,V2)) -> a__isList#(V1)
p12: a__isList#(__(V1,V2)) -> a__isList#(V1)
p13: a__isList#(__(V1,V2)) -> a__and#(a__isList(V1),isList(V2))
p14: a__isList#(V) -> a__isNeList#(V)
p15: a__isNeList#(__(V1,V2)) -> a__and#(a__isList(V1),isNeList(V2))
p16: mark#(isList(X)) -> a__isList#(X)
p17: mark#(and(X1,X2)) -> mark#(X1)
p18: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p19: mark#(__(X1,X2)) -> mark#(X2)
p20: mark#(__(X1,X2)) -> mark#(X1)
p21: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p22: a____#(X,nil()) -> mark#(X)
p23: a____#(__(X,Y),Z) -> mark#(Z)
p24: a____#(__(X,Y),Z) -> mark#(Y)
p25: a____#(__(X,Y),Z) -> a____#(mark(Y),mark(Z))
p26: 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__and(tt(),X) -> mark(X)
r5: a__isList(V) -> a__isNeList(V)
r6: a__isList(nil()) -> tt()
r7: a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
r8: a__isNeList(V) -> a__isQid(V)
r9: a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
r10: a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
r11: a__isNePal(V) -> a__isQid(V)
r12: a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
r13: a__isPal(V) -> a__isNePal(V)
r14: a__isPal(nil()) -> tt()
r15: a__isQid(a()) -> tt()
r16: a__isQid(e()) -> tt()
r17: a__isQid(i()) -> tt()
r18: a__isQid(o()) -> tt()
r19: a__isQid(u()) -> tt()
r20: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r21: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r22: mark(isList(X)) -> a__isList(X)
r23: mark(isNeList(X)) -> a__isNeList(X)
r24: mark(isQid(X)) -> a__isQid(X)
r25: mark(isNePal(X)) -> a__isNePal(X)
r26: mark(isPal(X)) -> a__isPal(X)
r27: mark(nil()) -> nil()
r28: mark(tt()) -> tt()
r29: mark(a()) -> a()
r30: mark(e()) -> e()
r31: mark(i()) -> i()
r32: mark(o()) -> o()
r33: mark(u()) -> u()
r34: a____(X1,X2) -> __(X1,X2)
r35: a__and(X1,X2) -> and(X1,X2)
r36: a__isList(X) -> isList(X)
r37: a__isNeList(X) -> isNeList(X)
r38: a__isQid(X) -> isQid(X)
r39: a__isNePal(X) -> isNePal(X)
r40: a__isPal(X) -> isPal(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

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____#_A(x1,x2) = ((1,0),(1,0)) x1 + ((1,0),(1,0)) x2 + (0,21)
            ___A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (20,5)
            mark_A(x1) = ((1,0),(1,1)) x1 + (0,6)
            a_____A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (20,6)
            nil_A() = (8,0)
            mark#_A(x1) = ((1,0),(1,0)) x1 + (8,0)
            isPal_A(x1) = x1 + (25,0)
            a__isPal#_A(x1) = x1 + (3,2)
            a__isNePal#_A(x1) = ((1,0),(1,0)) x1 + (2,1)
            a__and#_A(x1,x2) = x2 + (16,5)
            a__isQid_A(x1) = ((1,0),(0,0)) x1 + (0,10)
            tt_A() = (7,9)
            isNePal_A(x1) = x1 + (2,0)
            isNeList_A(x1) = ((1,0),(1,1)) x1 + (4,15)
            a__isNeList#_A(x1) = ((1,0),(0,0)) x1 + (3,14)
            a__isNeList_A(x1) = ((1,0),(1,1)) x1 + (4,16)
            isList_A(x1) = x1 + (6,5)
            a__isList#_A(x1) = x1 + (7,15)
            a__isList_A(x1) = ((1,0),(1,1)) x1 + (6,17)
            and_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (9,1)
            a__and_A(x1,x2) = x1 + ((1,0),(0,0)) x2 + (9,2)
            a__isNePal_A(x1) = x1 + (2,8)
            a__isPal_A(x1) = x1 + (25,9)
            a_A() = (8,0)
            e_A() = (8,10)
            i_A() = (8,0)
            o_A() = (8,0)
            u_A() = (8,0)
            isQid_A(x1) = ((1,0),(0,0)) x1 + (0,5)
    
      precedence:
      
        a__isNePal# > a__isPal# > a____# = mark# = a__and# > mark = nil = a__isList = e = o = u > isNeList = a__isNeList > a__isPal > a____ = isPal > __ = a__isQid = tt = a__and = a__isNePal > isList = a > a__isNeList# > a__isList# > isNePal = and = isQid > i
      
      partial status:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = [1]
        pi(a____) = []
        pi(nil) = []
        pi(mark#) = []
        pi(isPal) = [1]
        pi(a__isPal#) = []
        pi(a__isNePal#) = []
        pi(a__and#) = [2]
        pi(a__isQid) = []
        pi(tt) = []
        pi(isNePal) = []
        pi(isNeList) = []
        pi(a__isNeList#) = []
        pi(a__isNeList) = [1]
        pi(isList) = [1]
        pi(a__isList#) = [1]
        pi(a__isList) = [1]
        pi(and) = []
        pi(a__and) = []
        pi(a__isNePal) = [1]
        pi(a__isPal) = []
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
        pi(isQid) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            a____#_A(x1,x2) = (0,0)
            ___A(x1,x2) = (5,3)
            mark_A(x1) = ((1,0),(1,1)) x1 + (6,7)
            a_____A(x1,x2) = (12,1)
            nil_A() = (2,2)
            mark#_A(x1) = (0,0)
            isPal_A(x1) = (0,0)
            a__isPal#_A(x1) = (2,2)
            a__isNePal#_A(x1) = (1,1)
            a__and#_A(x1,x2) = (0,0)
            a__isQid_A(x1) = (0,2)
            tt_A() = (0,1)
            isNePal_A(x1) = (0,0)
            isNeList_A(x1) = (0,0)
            a__isNeList#_A(x1) = (2,0)
            a__isNeList_A(x1) = ((0,0),(1,0)) x1
            isList_A(x1) = ((0,0),(1,0)) x1
            a__isList#_A(x1) = (1,0)
            a__isList_A(x1) = ((0,0),(1,0)) x1
            and_A(x1,x2) = (0,1)
            a__and_A(x1,x2) = (0,4)
            a__isNePal_A(x1) = (0,5)
            a__isPal_A(x1) = (0,6)
            a_A() = (1,2)
            e_A() = (1,2)
            i_A() = (0,2)
            o_A() = (1,0)
            u_A() = (1,2)
            isQid_A(x1) = (0,1)
    
      precedence:
      
        u > isQid > o > and > e > i > mark = a____ > a__isList = a__isPal > a__isNePal > a__isQid > a > __ = isNeList = a__isNeList = a__isList# > a__and > isPal > tt > a__isPal# = isNePal > nil > a____# = mark# = a__isNePal# = a__and# = a__isNeList# = isList
      
      partial status:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(nil) = []
        pi(mark#) = []
        pi(isPal) = []
        pi(a__isPal#) = []
        pi(a__isNePal#) = []
        pi(a__and#) = []
        pi(a__isQid) = []
        pi(tt) = []
        pi(isNePal) = []
        pi(isNeList) = []
        pi(a__isNeList#) = []
        pi(a__isNeList) = []
        pi(isList) = []
        pi(a__isList#) = []
        pi(a__isList) = []
        pi(and) = []
        pi(a__and) = []
        pi(a__isNePal) = []
        pi(a__isPal) = []
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
        pi(isQid) = []
    

The next rules are strictly ordered:

  p3, p4, p5, p7, p8, p9, p11, p12, p13, p14, p15, p16, p25

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: a____#(nil(),X) -> mark#(X)
p3: a__and#(tt(),X) -> mark#(X)
p4: a__isNeList#(__(V1,V2)) -> a__and#(a__isNeList(V1),isList(V2))
p5: mark#(and(X1,X2)) -> mark#(X1)
p6: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p7: mark#(__(X1,X2)) -> mark#(X2)
p8: mark#(__(X1,X2)) -> mark#(X1)
p9: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p10: a____#(X,nil()) -> mark#(X)
p11: a____#(__(X,Y),Z) -> mark#(Z)
p12: a____#(__(X,Y),Z) -> mark#(Y)
p13: 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__and(tt(),X) -> mark(X)
r5: a__isList(V) -> a__isNeList(V)
r6: a__isList(nil()) -> tt()
r7: a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
r8: a__isNeList(V) -> a__isQid(V)
r9: a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
r10: a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
r11: a__isNePal(V) -> a__isQid(V)
r12: a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
r13: a__isPal(V) -> a__isNePal(V)
r14: a__isPal(nil()) -> tt()
r15: a__isQid(a()) -> tt()
r16: a__isQid(e()) -> tt()
r17: a__isQid(i()) -> tt()
r18: a__isQid(o()) -> tt()
r19: a__isQid(u()) -> tt()
r20: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r21: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r22: mark(isList(X)) -> a__isList(X)
r23: mark(isNeList(X)) -> a__isNeList(X)
r24: mark(isQid(X)) -> a__isQid(X)
r25: mark(isNePal(X)) -> a__isNePal(X)
r26: mark(isPal(X)) -> a__isPal(X)
r27: mark(nil()) -> nil()
r28: mark(tt()) -> tt()
r29: mark(a()) -> a()
r30: mark(e()) -> e()
r31: mark(i()) -> i()
r32: mark(o()) -> o()
r33: mark(u()) -> u()
r34: a____(X1,X2) -> __(X1,X2)
r35: a__and(X1,X2) -> and(X1,X2)
r36: a__isList(X) -> isList(X)
r37: a__isNeList(X) -> isNeList(X)
r38: a__isQid(X) -> isQid(X)
r39: a__isNePal(X) -> isNePal(X)
r40: a__isPal(X) -> isPal(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p5, p6, p7, p8, p9, p10, p11, p12, p13}


-- 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____#(__(X,Y),Z) -> mark#(X)
p3: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p4: a____#(__(X,Y),Z) -> mark#(Y)
p5: mark#(__(X1,X2)) -> mark#(X1)
p6: mark#(__(X1,X2)) -> mark#(X2)
p7: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p8: a__and#(tt(),X) -> mark#(X)
p9: mark#(and(X1,X2)) -> mark#(X1)
p10: a____#(__(X,Y),Z) -> mark#(Z)
p11: a____#(X,nil()) -> mark#(X)
p12: a____#(nil(),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__and(tt(),X) -> mark(X)
r5: a__isList(V) -> a__isNeList(V)
r6: a__isList(nil()) -> tt()
r7: a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
r8: a__isNeList(V) -> a__isQid(V)
r9: a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
r10: a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
r11: a__isNePal(V) -> a__isQid(V)
r12: a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
r13: a__isPal(V) -> a__isNePal(V)
r14: a__isPal(nil()) -> tt()
r15: a__isQid(a()) -> tt()
r16: a__isQid(e()) -> tt()
r17: a__isQid(i()) -> tt()
r18: a__isQid(o()) -> tt()
r19: a__isQid(u()) -> tt()
r20: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r21: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r22: mark(isList(X)) -> a__isList(X)
r23: mark(isNeList(X)) -> a__isNeList(X)
r24: mark(isQid(X)) -> a__isQid(X)
r25: mark(isNePal(X)) -> a__isNePal(X)
r26: mark(isPal(X)) -> a__isPal(X)
r27: mark(nil()) -> nil()
r28: mark(tt()) -> tt()
r29: mark(a()) -> a()
r30: mark(e()) -> e()
r31: mark(i()) -> i()
r32: mark(o()) -> o()
r33: mark(u()) -> u()
r34: a____(X1,X2) -> __(X1,X2)
r35: a__and(X1,X2) -> and(X1,X2)
r36: a__isList(X) -> isList(X)
r37: a__isNeList(X) -> isNeList(X)
r38: a__isQid(X) -> isQid(X)
r39: a__isNePal(X) -> isNePal(X)
r40: a__isPal(X) -> isPal(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

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____#_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (15,39)
            ___A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (14,47)
            mark_A(x1) = ((1,0),(1,1)) x1 + (0,41)
            a_____A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(0,0)) x2 + (14,60)
            mark#_A(x1) = ((1,0),(1,1)) x1 + (2,19)
            and_A(x1,x2) = x1 + x2 + (3,19)
            a__and#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(1,1)) x2 + (0,41)
            tt_A() = (2,21)
            nil_A() = (0,42)
            a__and_A(x1,x2) = x1 + x2 + (3,21)
            a__isList_A(x1) = ((1,0),(1,1)) x1 + (5,24)
            a__isNeList_A(x1) = ((1,0),(1,1)) x1 + (4,23)
            isList_A(x1) = x1 + (5,1)
            a__isQid_A(x1) = (3,22)
            isNeList_A(x1) = ((1,0),(1,1)) x1 + (4,0)
            a__isNePal_A(x1) = ((1,0),(0,0)) x1 + (4,45)
            isPal_A(x1) = ((1,0),(0,0)) x1 + (23,1)
            a__isPal_A(x1) = ((1,0),(0,0)) x1 + (23,46)
            a_A() = (3,22)
            e_A() = (3,22)
            i_A() = (3,22)
            o_A() = (0,22)
            u_A() = (3,22)
            isQid_A(x1) = (3,0)
            isNePal_A(x1) = ((1,0),(0,0)) x1 + (4,1)
    
      precedence:
      
        a__isPal > a__isNePal > mark = a____ = a__and > nil > a__isList > a__isNeList > a__isQid > tt > and > u > a____# = isNeList = o > isNePal > mark# = a__and# > __ = isPal > isQid > a = e = i > isList
      
      partial status:
    
        pi(a____#) = [1]
        pi(__) = [1]
        pi(mark) = []
        pi(a____) = [1]
        pi(mark#) = [1]
        pi(and) = [1, 2]
        pi(a__and#) = [2]
        pi(tt) = []
        pi(nil) = []
        pi(a__and) = [1]
        pi(a__isList) = [1]
        pi(a__isNeList) = [1]
        pi(isList) = []
        pi(a__isQid) = []
        pi(isNeList) = []
        pi(a__isNePal) = []
        pi(isPal) = []
        pi(a__isPal) = []
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
        pi(isQid) = []
        pi(isNePal) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            a____#_A(x1,x2) = ((1,0),(1,0)) x1 + (2,1)
            ___A(x1,x2) = ((0,0),(1,0)) x1 + (4,13)
            mark_A(x1) = (11,19)
            a_____A(x1,x2) = (5,12)
            mark#_A(x1) = x1 + (8,5)
            and_A(x1,x2) = ((1,0),(1,1)) x1 + ((1,0),(1,1)) x2 + (2,0)
            a__and#_A(x1,x2) = x2 + (9,6)
            tt_A() = (2,20)
            nil_A() = (5,0)
            a__and_A(x1,x2) = ((1,0),(1,1)) x1 + (5,6)
            a__isList_A(x1) = ((1,0),(1,1)) x1 + (11,19)
            a__isNeList_A(x1) = ((1,0),(1,1)) x1 + (11,19)
            isList_A(x1) = (0,12)
            a__isQid_A(x1) = (3,5)
            isNeList_A(x1) = (1,1)
            a__isNePal_A(x1) = (9,15)
            isPal_A(x1) = (0,0)
            a__isPal_A(x1) = (10,16)
            a_A() = (1,0)
            e_A() = (1,0)
            i_A() = (3,21)
            o_A() = (1,0)
            u_A() = (1,0)
            isQid_A(x1) = (0,0)
            isNePal_A(x1) = (9,1)
    
      precedence:
      
        o > e > i = u > isNePal > tt > nil = a__isPal > isQid > a > a__isList = a__isNeList = isList = a__isQid > mark > a____ > a____# = __ = mark# = and = a__and > isNeList > a__and# > isPal > a__isNePal
      
      partial status:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(mark#) = [1]
        pi(and) = []
        pi(a__and#) = [2]
        pi(tt) = []
        pi(nil) = []
        pi(a__and) = [1]
        pi(a__isList) = []
        pi(a__isNeList) = []
        pi(isList) = []
        pi(a__isQid) = []
        pi(isNeList) = []
        pi(a__isNePal) = []
        pi(isPal) = []
        pi(a__isPal) = []
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
        pi(isQid) = []
        pi(isNePal) = []
    

The next rules are strictly ordered:

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

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)

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__and(tt(),X) -> mark(X)
r5: a__isList(V) -> a__isNeList(V)
r6: a__isList(nil()) -> tt()
r7: a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
r8: a__isNeList(V) -> a__isQid(V)
r9: a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
r10: a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
r11: a__isNePal(V) -> a__isQid(V)
r12: a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P))
r13: a__isPal(V) -> a__isNePal(V)
r14: a__isPal(nil()) -> tt()
r15: a__isQid(a()) -> tt()
r16: a__isQid(e()) -> tt()
r17: a__isQid(i()) -> tt()
r18: a__isQid(o()) -> tt()
r19: a__isQid(u()) -> tt()
r20: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r21: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r22: mark(isList(X)) -> a__isList(X)
r23: mark(isNeList(X)) -> a__isNeList(X)
r24: mark(isQid(X)) -> a__isQid(X)
r25: mark(isNePal(X)) -> a__isNePal(X)
r26: mark(isPal(X)) -> a__isPal(X)
r27: mark(nil()) -> nil()
r28: mark(tt()) -> tt()
r29: mark(a()) -> a()
r30: mark(e()) -> e()
r31: mark(i()) -> i()
r32: mark(o()) -> o()
r33: mark(u()) -> u()
r34: a____(X1,X2) -> __(X1,X2)
r35: a__and(X1,X2) -> and(X1,X2)
r36: a__isList(X) -> isList(X)
r37: a__isNeList(X) -> isNeList(X)
r38: a__isQid(X) -> isQid(X)
r39: a__isNePal(X) -> isNePal(X)
r40: a__isPal(X) -> isPal(X)

The estimated dependency graph contains the following SCCs:

  (no SCCs)