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 monotone reduction pair:

  matrix interpretations:
  
    carrier: N^1
    order: standard order
    interpretations:
      a____#_A(x1,x2) = x1 + x2
      ___A(x1,x2) = x1 + x2 + 4
      mark_A(x1) = x1
      a_____A(x1,x2) = x1 + x2 + 4
      nil_A() = 5
      mark#_A(x1) = x1 + 4
      isPal_A(x1) = x1 + 3
      a__isPal#_A(x1) = x1 + 6
      a__isNePal#_A(x1) = x1 + 5
      a__and#_A(x1,x2) = x1 + x2 + 3
      a__isQid_A(x1) = x1 + 1
      tt_A() = 1
      isNePal_A(x1) = x1 + 1
      isNeList_A(x1) = x1 + 1
      a__isNeList#_A(x1) = x1 + 5
      a__isNeList_A(x1) = x1 + 1
      isList_A(x1) = x1 + 3
      a__isList#_A(x1) = x1 + 5
      a__isList_A(x1) = x1 + 3
      and_A(x1,x2) = x1 + x2 + 1
      a__and_A(x1,x2) = x1 + x2 + 1
      a__isNePal_A(x1) = x1 + 1
      a__isPal_A(x1) = x1 + 3
      a_A() = 1
      e_A() = 1
      i_A() = 1
      o_A() = 1
      u_A() = 1
      isQid_A(x1) = x1 + 1

The next rules are strictly ordered:

  p2, p3, p4, p5, p9, p10, p11, p12, p15, p16, p17, p18, p19, p20, p21, p22, p25
  r2, r3, r4, r5, r6, r12, r13, r14, r15, r16, r17, r18, r19

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__and#(tt(),X) -> mark#(X)
p3: mark#(isNePal(X)) -> a__isNePal#(X)
p4: mark#(isNeList(X)) -> a__isNeList#(X)
p5: a__isList#(__(V1,V2)) -> a__and#(a__isList(V1),isList(V2))
p6: a__isList#(V) -> a__isNeList#(V)
p7: a____#(__(X,Y),Z) -> mark#(Z)
p8: a____#(__(X,Y),Z) -> mark#(Y)
p9: a____#(__(X,Y),Z) -> mark#(X)

and R consists of:

r1: a__isNePal(V) -> a__isQid(V)
r2: a__and(X1,X2) -> and(X1,X2)
r3: a__isNePal(X) -> isNePal(X)
r4: a__isPal(X) -> isPal(X)
r5: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r6: a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
r7: a__isNeList(V) -> a__isQid(V)
r8: a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
r9: a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
r10: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r11: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r12: mark(isList(X)) -> a__isList(X)
r13: mark(isNeList(X)) -> a__isNeList(X)
r14: mark(isQid(X)) -> a__isQid(X)
r15: mark(isNePal(X)) -> a__isNePal(X)
r16: mark(isPal(X)) -> a__isPal(X)
r17: mark(nil()) -> nil()
r18: mark(tt()) -> tt()
r19: mark(a()) -> a()
r20: mark(e()) -> e()
r21: mark(i()) -> i()
r22: mark(o()) -> o()
r23: mark(u()) -> u()
r24: a____(X1,X2) -> __(X1,X2)
r25: a__isList(X) -> isList(X)
r26: a__isNeList(X) -> isNeList(X)
r27: a__isQid(X) -> isQid(X)

The estimated dependency graph contains the following SCCs:

  {p1}


-- 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__isNePal(V) -> a__isQid(V)
r2: a__and(X1,X2) -> and(X1,X2)
r3: a__isNePal(X) -> isNePal(X)
r4: a__isPal(X) -> isPal(X)
r5: a____(__(X,Y),Z) -> a____(mark(X),a____(mark(Y),mark(Z)))
r6: a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2))
r7: a__isNeList(V) -> a__isQid(V)
r8: a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2))
r9: a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2))
r10: mark(__(X1,X2)) -> a____(mark(X1),mark(X2))
r11: mark(and(X1,X2)) -> a__and(mark(X1),X2)
r12: mark(isList(X)) -> a__isList(X)
r13: mark(isNeList(X)) -> a__isNeList(X)
r14: mark(isQid(X)) -> a__isQid(X)
r15: mark(isNePal(X)) -> a__isNePal(X)
r16: mark(isPal(X)) -> a__isPal(X)
r17: mark(nil()) -> nil()
r18: mark(tt()) -> tt()
r19: mark(a()) -> a()
r20: mark(e()) -> e()
r21: mark(i()) -> i()
r22: mark(o()) -> o()
r23: mark(u()) -> u()
r24: a____(X1,X2) -> __(X1,X2)
r25: a__isList(X) -> isList(X)
r26: a__isNeList(X) -> isNeList(X)
r27: a__isQid(X) -> isQid(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

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^1
    order: standard order
    interpretations:
      a____#_A(x1,x2) = x1
      ___A(x1,x2) = x1 + 1
      mark_A(x1) = x1
      a_____A(x1,x2) = x1 + 1
      a__isNePal_A(x1) = x1
      a__isQid_A(x1) = x1
      a__and_A(x1,x2) = x1
      and_A(x1,x2) = x1
      isNePal_A(x1) = x1
      a__isPal_A(x1) = x1
      isPal_A(x1) = x1
      a__isList_A(x1) = 0
      isList_A(x1) = 0
      a__isNeList_A(x1) = x1
      isNeList_A(x1) = x1
      isQid_A(x1) = x1
      nil_A() = 0
      tt_A() = 0
      a_A() = 0
      e_A() = 0
      i_A() = 0
      o_A() = 0
      u_A() = 0

The next rules are strictly ordered:

  p1

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