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:
    
        max/plus interpretations on natural numbers:
        
          a____#_A(x1,x2) = max{x1 + 98, x2 + 7}
          ___A(x1,x2) = max{183, x1 + 91, x2}
          mark_A(x1) = max{36, x1}
          a_____A(x1,x2) = max{183, x1 + 91, x2}
          nil_A = 89
          mark#_A(x1) = x1 + 7
          isPal_A(x1) = x1 + 44
          a__isPal#_A(x1) = x1 + 43
          a__isNePal#_A(x1) = max{42, x1 - 40}
          a__and#_A(x1,x2) = max{x1 - 33, x2 + 7}
          a__isQid_A(x1) = 32
          tt_A = 31
          isNePal_A(x1) = x1 + 37
          isNeList_A(x1) = 5
          a__isNeList#_A(x1) = 12
          a__isNeList_A(x1) = 36
          isList_A(x1) = 5
          a__isList#_A(x1) = 12
          a__isList_A(x1) = 36
          and_A(x1,x2) = max{36, x1, x2 + 30}
          a__and_A(x1,x2) = max{36, x1, x2 + 30}
          a__isNePal_A(x1) = x1 + 37
          a__isPal_A(x1) = x1 + 44
          a_A = 32
          e_A = 32
          i_A = 30
          o_A = 30
          u_A = 36
          isQid_A(x1) = 1
    
      precedence:
      
        a__isPal# > a__isNePal# > a > isQid > mark = a____ = a__isNeList = a__isList = a__and = e = o > isNeList = a__isNePal = a__isPal > isNePal > u > nil = a__isQid = isList > __ > a____# = mark# = a__and# = tt = a__isNeList# = a__isList# = i > and > isPal
      
      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) = [1]
        pi(a__isPal) = [1]
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
        pi(isQid) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a____#_A(x1,x2) = 27
          ___A(x1,x2) = 11
          mark_A(x1) = 32
          a_____A(x1,x2) = 32
          nil_A = 31
          mark#_A(x1) = 27
          isPal_A(x1) = 10
          a__isPal#_A(x1) = 27
          a__isNePal#_A(x1) = 33
          a__and#_A(x1,x2) = 27
          a__isQid_A(x1) = 38
          tt_A = 30
          isNePal_A(x1) = 30
          isNeList_A(x1) = 28
          a__isNeList#_A(x1) = 27
          a__isNeList_A(x1) = 32
          isList_A(x1) = 33
          a__isList#_A(x1) = 27
          a__isList_A(x1) = 32
          and_A(x1,x2) = 24
          a__and_A(x1,x2) = 32
          a__isNePal_A(x1) = 32
          a__isPal_A(x1) = 32
          a_A = 33
          e_A = 33
          i_A = 33
          o_A = 0
          u_A = 0
          isQid_A(x1) = 1
    
      precedence:
      
        i = o > isPal > mark = a____ = a__isNeList = a__isList = a__and = a__isNePal = a__isPal > isList > a____# = mark# = a__and# = a__isNeList# = a__isList# > u > __ = a__isNePal# > isNeList > a__isPal# > isNePal > a__isQid > e = isQid > nil > tt = and = a
      
      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

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: mark#(isNeList(X)) -> a__isNeList#(X)
p5: a__isNeList#(__(V1,V2)) -> a__isNeList#(V1)
p6: a__isNeList#(__(V1,V2)) -> a__and#(a__isNeList(V1),isList(V2))
p7: a__isNeList#(__(V1,V2)) -> a__isList#(V1)
p8: a__isList#(__(V1,V2)) -> a__isList#(V1)
p9: a__isList#(__(V1,V2)) -> a__and#(a__isList(V1),isList(V2))
p10: a__isList#(V) -> a__isNeList#(V)
p11: a__isNeList#(__(V1,V2)) -> a__and#(a__isList(V1),isNeList(V2))
p12: mark#(isList(X)) -> a__isList#(X)
p13: mark#(and(X1,X2)) -> mark#(X1)
p14: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
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__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, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22}


-- 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) -> a____#(mark(Y),mark(Z))
p5: a____#(__(X,Y),Z) -> mark#(Y)
p6: mark#(__(X1,X2)) -> mark#(X1)
p7: mark#(__(X1,X2)) -> mark#(X2)
p8: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p9: a__and#(tt(),X) -> mark#(X)
p10: mark#(and(X1,X2)) -> mark#(X1)
p11: mark#(isList(X)) -> a__isList#(X)
p12: a__isList#(V) -> a__isNeList#(V)
p13: a__isNeList#(__(V1,V2)) -> a__and#(a__isList(V1),isNeList(V2))
p14: a__isNeList#(__(V1,V2)) -> a__isList#(V1)
p15: a__isList#(__(V1,V2)) -> a__and#(a__isList(V1),isList(V2))
p16: a__isList#(__(V1,V2)) -> a__isList#(V1)
p17: a__isNeList#(__(V1,V2)) -> a__and#(a__isNeList(V1),isList(V2))
p18: a__isNeList#(__(V1,V2)) -> a__isNeList#(V1)
p19: mark#(isNeList(X)) -> a__isNeList#(X)
p20: a____#(__(X,Y),Z) -> mark#(Z)
p21: a____#(X,nil()) -> mark#(X)
p22: 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:
    
        max/plus interpretations on natural numbers:
        
          a____#_A(x1,x2) = max{x1 + 43, x2 + 17}
          ___A(x1,x2) = max{34, x1 + 26, x2}
          mark_A(x1) = max{8, x1}
          a_____A(x1,x2) = max{34, x1 + 26, x2}
          mark#_A(x1) = x1 + 17
          and_A(x1,x2) = max{14, x1 + 5, x2}
          a__and#_A(x1,x2) = max{x1 + 20, x2 + 17}
          tt_A = 0
          isList_A(x1) = x1 + 39
          a__isList#_A(x1) = x1 + 56
          a__isNeList#_A(x1) = x1 + 56
          a__isList_A(x1) = x1 + 39
          isNeList_A(x1) = x1 + 39
          a__isNeList_A(x1) = x1 + 39
          nil_A = 1
          a__and_A(x1,x2) = max{14, x1 + 5, x2}
          a__isNePal_A(x1) = max{8, x1}
          a__isQid_A(x1) = max{1, x1 - 6}
          isPal_A(x1) = max{27, x1 + 9}
          a__isPal_A(x1) = max{27, x1 + 9}
          a_A = 7
          e_A = 8
          i_A = 7
          o_A = 7
          u_A = 8
          isQid_A(x1) = max{0, x1 - 6}
          isNePal_A(x1) = x1
    
      precedence:
      
        a____# = __ = mark = a____ = mark# = and = a__and# = tt = isList = a__isList# = a__isNeList# = a__isList = isNeList = a__isNeList = nil = a__and = a__isNePal = a__isQid = isPal = a__isPal = a = e = i = o = u = isQid = isNePal
      
      partial status:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(mark#) = []
        pi(and) = []
        pi(a__and#) = []
        pi(tt) = []
        pi(isList) = []
        pi(a__isList#) = []
        pi(a__isNeList#) = []
        pi(a__isList) = []
        pi(isNeList) = []
        pi(a__isNeList) = []
        pi(nil) = []
        pi(a__and) = []
        pi(a__isNePal) = []
        pi(a__isQid) = []
        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:
    
        max/plus interpretations on natural numbers:
        
          a____#_A(x1,x2) = 20
          ___A(x1,x2) = 16
          mark_A(x1) = 16
          a_____A(x1,x2) = 16
          mark#_A(x1) = 20
          and_A(x1,x2) = 8
          a__and#_A(x1,x2) = 20
          tt_A = 14
          isList_A(x1) = 12
          a__isList#_A(x1) = 20
          a__isNeList#_A(x1) = 20
          a__isList_A(x1) = 16
          isNeList_A(x1) = 10
          a__isNeList_A(x1) = 16
          nil_A = 3
          a__and_A(x1,x2) = 16
          a__isNePal_A(x1) = 16
          a__isQid_A(x1) = 13
          isPal_A(x1) = 0
          a__isPal_A(x1) = 16
          a_A = 17
          e_A = 0
          i_A = 0
          o_A = 0
          u_A = 13
          isQid_A(x1) = 12
          isNePal_A(x1) = 1
    
      precedence:
      
        o = isNePal > a > a____# = mark = a____ = mark# = and = a__and# = tt = isList = a__isList# = a__isNeList# = a__isList = isNeList = a__isNeList = nil = a__and = i > u > a__isNePal = a__isPal = isQid > __ > a__isQid = isPal = e
      
      partial status:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(mark#) = []
        pi(and) = []
        pi(a__and#) = []
        pi(tt) = []
        pi(isList) = []
        pi(a__isList#) = []
        pi(a__isNeList#) = []
        pi(a__isList) = []
        pi(isNeList) = []
        pi(a__isNeList) = []
        pi(nil) = []
        pi(a__and) = []
        pi(a__isNePal) = []
        pi(a__isQid) = []
        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:

  p5, p10, p14, p18, p21

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____#(__(X,Y),Z) -> mark#(X)
p3: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p4: a____#(__(X,Y),Z) -> a____#(mark(Y),mark(Z))
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#(isList(X)) -> a__isList#(X)
p10: a__isList#(V) -> a__isNeList#(V)
p11: a__isNeList#(__(V1,V2)) -> a__and#(a__isList(V1),isNeList(V2))
p12: a__isList#(__(V1,V2)) -> a__and#(a__isList(V1),isList(V2))
p13: a__isList#(__(V1,V2)) -> a__isList#(V1)
p14: a__isNeList#(__(V1,V2)) -> a__and#(a__isNeList(V1),isList(V2))
p15: mark#(isNeList(X)) -> a__isNeList#(X)
p16: a____#(__(X,Y),Z) -> mark#(Z)
p17: 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 estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17}


-- 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#(isNeList(X)) -> a__isNeList#(X)
p4: a__isNeList#(__(V1,V2)) -> a__and#(a__isNeList(V1),isList(V2))
p5: a__and#(tt(),X) -> mark#(X)
p6: mark#(isList(X)) -> a__isList#(X)
p7: a__isList#(__(V1,V2)) -> a__isList#(V1)
p8: a__isList#(__(V1,V2)) -> a__and#(a__isList(V1),isList(V2))
p9: a__isList#(V) -> a__isNeList#(V)
p10: a__isNeList#(__(V1,V2)) -> a__and#(a__isList(V1),isNeList(V2))
p11: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p12: mark#(__(X1,X2)) -> mark#(X2)
p13: mark#(__(X1,X2)) -> mark#(X1)
p14: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p15: a____#(__(X,Y),Z) -> mark#(Z)
p16: a____#(__(X,Y),Z) -> a____#(mark(Y),mark(Z))
p17: 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:
    
        max/plus interpretations on natural numbers:
        
          a____#_A(x1,x2) = max{x1 + 7, x2}
          ___A(x1,x2) = max{13, x1 + 7, x2}
          mark_A(x1) = max{1, x1}
          a_____A(x1,x2) = max{13, x1 + 7, x2}
          nil_A = 4
          mark#_A(x1) = x1
          isNeList_A(x1) = x1 + 15
          a__isNeList#_A(x1) = x1 + 15
          a__and#_A(x1,x2) = max{x1 - 14, x2}
          a__isNeList_A(x1) = x1 + 15
          isList_A(x1) = max{27, x1 + 15}
          tt_A = 3
          a__isList#_A(x1) = max{16, x1 + 15}
          a__isList_A(x1) = max{27, x1 + 15}
          and_A(x1,x2) = max{x1, x2}
          a__and_A(x1,x2) = max{x1, x2}
          a__isNePal_A(x1) = max{11, x1 + 3}
          a__isQid_A(x1) = max{11, x1 + 2}
          isPal_A(x1) = max{12, x1 + 7}
          a__isPal_A(x1) = max{12, x1 + 7}
          a_A = 4
          e_A = 2
          i_A = 4
          o_A = 4
          u_A = 4
          isQid_A(x1) = max{11, x1 + 2}
          isNePal_A(x1) = max{11, x1 + 3}
    
      precedence:
      
        mark = a____ = nil = a__isNeList = a__isList = a__and = a__isNePal = a = e = i = isNePal > __ > isPal = a__isPal = o > isNeList = a__isQid > isQid > u > a____# = mark# = a__isNeList# = a__and# = isList = tt = a__isList# = and
      
      partial status:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(nil) = []
        pi(mark#) = []
        pi(isNeList) = []
        pi(a__isNeList#) = []
        pi(a__and#) = []
        pi(a__isNeList) = []
        pi(isList) = []
        pi(tt) = []
        pi(a__isList#) = []
        pi(a__isList) = []
        pi(and) = []
        pi(a__and) = []
        pi(a__isNePal) = []
        pi(a__isQid) = []
        pi(isPal) = [1]
        pi(a__isPal) = [1]
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
        pi(isQid) = []
        pi(isNePal) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a____#_A(x1,x2) = 2
          ___A(x1,x2) = 21
          mark_A(x1) = 21
          a_____A(x1,x2) = 21
          nil_A = 2
          mark#_A(x1) = 2
          isNeList_A(x1) = 18
          a__isNeList#_A(x1) = 2
          a__and#_A(x1,x2) = 2
          a__isNeList_A(x1) = 21
          isList_A(x1) = 20
          tt_A = 3
          a__isList#_A(x1) = 2
          a__isList_A(x1) = 21
          and_A(x1,x2) = 3
          a__and_A(x1,x2) = 21
          a__isNePal_A(x1) = 21
          a__isQid_A(x1) = 20
          isPal_A(x1) = 11
          a__isPal_A(x1) = 21
          a_A = 2
          e_A = 2
          i_A = 2
          o_A = 2
          u_A = 22
          isQid_A(x1) = 1
          isNePal_A(x1) = 1
    
      precedence:
      
        isNePal > tt > a____# = mark# = isNeList = a__isNeList# = a__and# = a__isList# > u = isQid > __ = mark = a____ = nil = a__isNeList = a__isList = a__and > and = i = o > isList > a__isNePal = a__isQid = isPal = a__isPal = a = e
      
      partial status:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(nil) = []
        pi(mark#) = []
        pi(isNeList) = []
        pi(a__isNeList#) = []
        pi(a__and#) = []
        pi(a__isNeList) = []
        pi(isList) = []
        pi(tt) = []
        pi(a__isList#) = []
        pi(a__isList) = []
        pi(and) = []
        pi(a__and) = []
        pi(a__isNePal) = []
        pi(a__isQid) = []
        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:

  p7, p13, p17

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: mark#(isNeList(X)) -> a__isNeList#(X)
p4: a__isNeList#(__(V1,V2)) -> a__and#(a__isNeList(V1),isList(V2))
p5: a__and#(tt(),X) -> mark#(X)
p6: mark#(isList(X)) -> a__isList#(X)
p7: a__isList#(__(V1,V2)) -> a__and#(a__isList(V1),isList(V2))
p8: a__isList#(V) -> a__isNeList#(V)
p9: a__isNeList#(__(V1,V2)) -> a__and#(a__isList(V1),isNeList(V2))
p10: mark#(and(X1,X2)) -> a__and#(mark(X1),X2)
p11: mark#(__(X1,X2)) -> mark#(X2)
p12: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p13: a____#(__(X,Y),Z) -> mark#(Z)
p14: a____#(__(X,Y),Z) -> 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__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, p12, p13, p14}


-- 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) -> a____#(mark(Y),mark(Z))
p3: a____#(__(X,Y),Z) -> mark#(Z)
p4: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p5: a____#(nil(),X) -> mark#(X)
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#(isList(X)) -> a__isList#(X)
p10: a__isList#(V) -> a__isNeList#(V)
p11: a__isNeList#(__(V1,V2)) -> a__and#(a__isList(V1),isNeList(V2))
p12: a__isNeList#(__(V1,V2)) -> a__and#(a__isNeList(V1),isList(V2))
p13: a__isList#(__(V1,V2)) -> a__and#(a__isList(V1),isList(V2))
p14: mark#(isNeList(X)) -> a__isNeList#(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:
    
        max/plus interpretations on natural numbers:
        
          a____#_A(x1,x2) = max{x1 + 20, x2 + 5}
          ___A(x1,x2) = max{30, x1 + 15, x2}
          mark_A(x1) = max{6, x1}
          a_____A(x1,x2) = max{30, x1 + 15, x2}
          mark#_A(x1) = x1 + 5
          nil_A = 6
          and_A(x1,x2) = max{x1, x2 + 6}
          a__and#_A(x1,x2) = max{x1 - 3, x2 + 5}
          tt_A = 6
          isList_A(x1) = 0
          a__isList#_A(x1) = 5
          a__isNeList#_A(x1) = 5
          a__isList_A(x1) = 6
          isNeList_A(x1) = 0
          a__isNeList_A(x1) = 6
          a__and_A(x1,x2) = max{x1, x2 + 6}
          a__isNePal_A(x1) = max{7, x1 + 2}
          a__isQid_A(x1) = 6
          isPal_A(x1) = x1 + 8
          a__isPal_A(x1) = x1 + 8
          a_A = 5
          e_A = 5
          i_A = 5
          o_A = 5
          u_A = 5
          isQid_A(x1) = 6
          isNePal_A(x1) = max{7, x1 + 2}
    
      precedence:
      
        a____# = __ = mark = a____ = mark# = nil = and = a__and# = tt = isList = a__isList# = a__isNeList# = a__isList = isNeList = a__isNeList = a__and = a__isNePal = a__isQid = isPal = a__isPal = a = e = i = o = u = isQid = isNePal
      
      partial status:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(mark#) = []
        pi(nil) = []
        pi(and) = []
        pi(a__and#) = []
        pi(tt) = []
        pi(isList) = []
        pi(a__isList#) = []
        pi(a__isNeList#) = []
        pi(a__isList) = []
        pi(isNeList) = []
        pi(a__isNeList) = []
        pi(a__and) = []
        pi(a__isNePal) = []
        pi(a__isQid) = []
        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:
    
        max/plus interpretations on natural numbers:
        
          a____#_A(x1,x2) = 9
          ___A(x1,x2) = 30
          mark_A(x1) = 55
          a_____A(x1,x2) = 55
          mark#_A(x1) = 9
          nil_A = 30
          and_A(x1,x2) = 27
          a__and#_A(x1,x2) = 9
          tt_A = 28
          isList_A(x1) = 25
          a__isList#_A(x1) = 9
          a__isNeList#_A(x1) = 9
          a__isList_A(x1) = 55
          isNeList_A(x1) = 23
          a__isNeList_A(x1) = 55
          a__and_A(x1,x2) = 55
          a__isNePal_A(x1) = 55
          a__isQid_A(x1) = 30
          isPal_A(x1) = 25
          a__isPal_A(x1) = 55
          a_A = 26
          e_A = 56
          i_A = 56
          o_A = 26
          u_A = 0
          isQid_A(x1) = 0
          isNePal_A(x1) = 25
    
      precedence:
      
        mark = a____ = a__isList = a__isNeList = a__and = a__isNePal = isPal = a__isPal > and = isNeList = u = isQid > isList > a____# = mark# = a__and# = a__isList# = a__isNeList# = isNePal > nil > a > __ = a__isQid > tt > e = i = o
      
      partial status:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(mark#) = []
        pi(nil) = []
        pi(and) = []
        pi(a__and#) = []
        pi(tt) = []
        pi(isList) = []
        pi(a__isList#) = []
        pi(a__isNeList#) = []
        pi(a__isList) = []
        pi(isNeList) = []
        pi(a__isNeList) = []
        pi(a__and) = []
        pi(a__isNePal) = []
        pi(a__isQid) = []
        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:

  p7

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____#(__(X,Y),Z) -> a____#(mark(Y),mark(Z))
p3: a____#(__(X,Y),Z) -> mark#(Z)
p4: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p5: a____#(nil(),X) -> mark#(X)
p6: mark#(__(X1,X2)) -> mark#(X2)
p7: a__and#(tt(),X) -> mark#(X)
p8: mark#(isList(X)) -> a__isList#(X)
p9: a__isList#(V) -> a__isNeList#(V)
p10: a__isNeList#(__(V1,V2)) -> a__and#(a__isList(V1),isNeList(V2))
p11: a__isNeList#(__(V1,V2)) -> a__and#(a__isNeList(V1),isList(V2))
p12: a__isList#(__(V1,V2)) -> a__and#(a__isList(V1),isList(V2))
p13: mark#(isNeList(X)) -> a__isNeList#(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, 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____#(nil(),X) -> mark#(X)
p3: mark#(isNeList(X)) -> a__isNeList#(X)
p4: a__isNeList#(__(V1,V2)) -> a__and#(a__isNeList(V1),isList(V2))
p5: a__and#(tt(),X) -> mark#(X)
p6: mark#(isList(X)) -> a__isList#(X)
p7: a__isList#(__(V1,V2)) -> a__and#(a__isList(V1),isList(V2))
p8: a__isList#(V) -> a__isNeList#(V)
p9: a__isNeList#(__(V1,V2)) -> a__and#(a__isList(V1),isNeList(V2))
p10: mark#(__(X1,X2)) -> mark#(X2)
p11: mark#(__(X1,X2)) -> a____#(mark(X1),mark(X2))
p12: a____#(__(X,Y),Z) -> mark#(Z)
p13: a____#(__(X,Y),Z) -> 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__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 + x2 + (6,1)
            ___A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (7,0)
            mark_A(x1) = ((1,0),(0,0)) x1 + (0,5)
            a_____A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (7,4)
            nil_A() = (7,1)
            mark#_A(x1) = x1 + (1,7)
            isNeList_A(x1) = ((1,0),(0,0)) x1 + (3,4)
            a__isNeList#_A(x1) = ((1,0),(0,0)) x1 + (4,1)
            a__and#_A(x1,x2) = ((1,0),(0,0)) x2 + (8,1)
            a__isNeList_A(x1) = ((1,0),(0,0)) x1 + (3,4)
            isList_A(x1) = ((1,0),(0,0)) x1 + (3,2)
            tt_A() = (8,2)
            a__isList#_A(x1) = ((1,0),(0,0)) x1 + (4,1)
            a__isList_A(x1) = ((1,0),(0,0)) x1 + (3,4)
            a__and_A(x1,x2) = ((1,0),(0,0)) x2 + (3,1)
            a__isNePal_A(x1) = ((1,0),(0,0)) x1 + (4,4)
            a__isQid_A(x1) = ((1,0),(0,0)) x1 + (2,3)
            isPal_A(x1) = ((1,0),(0,0)) x1 + (15,5)
            a__isPal_A(x1) = ((1,0),(0,0)) x1 + (15,5)
            a_A() = (9,5)
            e_A() = (9,5)
            i_A() = (7,5)
            o_A() = (9,5)
            u_A() = (9,1)
            and_A(x1,x2) = ((1,0),(0,0)) x2 + (3,1)
            isQid_A(x1) = ((1,0),(0,0)) x1 + (2,1)
            isNePal_A(x1) = ((1,0),(0,0)) x1 + (4,4)
    
      precedence:
      
        isList > mark > a__isList = isPal = a__isPal > a____ = tt > __ > o > u > a__isNePal = a > a__and > a__isNeList > isNeList = and > e = i > a__isList# > a__isNeList# > a__and# > a____# = nil = mark# = a__isQid = isQid = isNePal
      
      partial status:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(nil) = []
        pi(mark#) = []
        pi(isNeList) = []
        pi(a__isNeList#) = []
        pi(a__and#) = []
        pi(a__isNeList) = []
        pi(isList) = []
        pi(tt) = []
        pi(a__isList#) = []
        pi(a__isList) = []
        pi(a__and) = []
        pi(a__isNePal) = []
        pi(a__isQid) = []
        pi(isPal) = []
        pi(a__isPal) = []
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
        pi(and) = []
        pi(isQid) = []
        pi(isNePal) = []
    
    2. weighted path order
    
      base order:
    
        matrix interpretations:
        
          carrier: N^2
          order: lexicographic order
          interpretations:
            a____#_A(x1,x2) = (8,6)
            ___A(x1,x2) = (4,0)
            mark_A(x1) = (4,0)
            a_____A(x1,x2) = (4,0)
            nil_A() = (3,0)
            mark#_A(x1) = (8,5)
            isNeList_A(x1) = (1,0)
            a__isNeList#_A(x1) = (10,0)
            a__and#_A(x1,x2) = (9,6)
            a__isNeList_A(x1) = (3,2)
            isList_A(x1) = (5,1)
            tt_A() = (1,0)
            a__isList#_A(x1) = (7,4)
            a__isList_A(x1) = (6,3)
            a__and_A(x1,x2) = (2,1)
            a__isNePal_A(x1) = (3,0)
            a__isQid_A(x1) = (2,0)
            isPal_A(x1) = (3,0)
            a__isPal_A(x1) = (3,0)
            a_A() = (1,0)
            e_A() = (1,0)
            i_A() = (1,0)
            o_A() = (1,0)
            u_A() = (2,0)
            and_A(x1,x2) = (1,0)
            isQid_A(x1) = (1,1)
            isNePal_A(x1) = (2,0)
    
      precedence:
      
        a__isList > a____# > a__and > __ = mark = a____ = a__and# = isList > mark# > tt > isPal = a__isPal > isNePal > and > o > a > e = i > a__isNePal > u > a__isQid > a__isNeList > isNeList > isQid > nil > a__isList# > a__isNeList#
      
      partial status:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(nil) = []
        pi(mark#) = []
        pi(isNeList) = []
        pi(a__isNeList#) = []
        pi(a__and#) = []
        pi(a__isNeList) = []
        pi(isList) = []
        pi(tt) = []
        pi(a__isList#) = []
        pi(a__isList) = []
        pi(a__and) = []
        pi(a__isNePal) = []
        pi(a__isQid) = []
        pi(isPal) = []
        pi(a__isPal) = []
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
        pi(and) = []
        pi(isQid) = []
        pi(isNePal) = []
    

The next rules are strictly ordered:

  p3, p4, p5, p6, p7, p8, p9, p11

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: mark#(__(X1,X2)) -> mark#(X2)
p4: a____#(__(X,Y),Z) -> mark#(Z)
p5: a____#(__(X,Y),Z) -> 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__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, p5}
  {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)))
p2: a____#(__(X,Y),Z) -> 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__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:
    
        max/plus interpretations on natural numbers:
        
          a____#_A(x1,x2) = max{x1 + 25, x2 + 13}
          ___A(x1,x2) = max{x1 + 11, x2}
          mark_A(x1) = x1
          a_____A(x1,x2) = max{x1 + 11, x2}
          a__and_A(x1,x2) = max{7, x2}
          tt_A = 2
          a__isList_A(x1) = x1 + 6
          a__isNeList_A(x1) = x1 + 6
          nil_A = 3
          isList_A(x1) = x1 + 6
          a__isQid_A(x1) = x1 + 3
          isNeList_A(x1) = x1 + 6
          a__isNePal_A(x1) = x1 + 9
          isPal_A(x1) = x1 + 10
          a__isPal_A(x1) = x1 + 10
          a_A = 3
          e_A = 3
          i_A = 1
          o_A = 3
          u_A = 1
          and_A(x1,x2) = max{7, x2}
          isQid_A(x1) = x1 + 3
          isNePal_A(x1) = x1 + 9
    
      precedence:
      
        a____# = __ = mark = a____ = a__and = tt = a__isList = a__isNeList = nil = isList = a__isQid = isNeList = a__isNePal = isPal = a__isPal = a = e = i = o = u = and = isQid = isNePal
      
      partial status:
    
        pi(a____#) = [1, 2]
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(a__and) = []
        pi(tt) = []
        pi(a__isList) = []
        pi(a__isNeList) = []
        pi(nil) = []
        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(and) = []
        pi(isQid) = []
        pi(isNePal) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a____#_A(x1,x2) = max{x1 + 22, x2 + 20}
          ___A(x1,x2) = 10
          mark_A(x1) = 10
          a_____A(x1,x2) = 10
          a__and_A(x1,x2) = 10
          tt_A = 10
          a__isList_A(x1) = 10
          a__isNeList_A(x1) = 10
          nil_A = 10
          isList_A(x1) = 10
          a__isQid_A(x1) = 10
          isNeList_A(x1) = 10
          a__isNePal_A(x1) = 10
          isPal_A(x1) = 10
          a__isPal_A(x1) = 10
          a_A = 0
          e_A = 10
          i_A = 10
          o_A = 10
          u_A = 10
          and_A(x1,x2) = 10
          isQid_A(x1) = 9
          isNePal_A(x1) = 1
    
      precedence:
      
        a____# > isQid > __ = mark = a____ = a__and = a__isList = a__isNeList = and = isNePal > u > isList = e > a__isPal > isPal > a__isNePal = a > a__isQid > isNeList > nil = i > o > tt
      
      partial status:
    
        pi(a____#) = []
        pi(__) = []
        pi(mark) = []
        pi(a____) = []
        pi(a__and) = []
        pi(tt) = []
        pi(a__isList) = []
        pi(a__isNeList) = []
        pi(nil) = []
        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(and) = []
        pi(isQid) = []
        pi(isNePal) = []
    

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


-- Reduction pair.

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

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

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = x1 + 2
          ___A(x1,x2) = max{x1 + 2, x2 + 2}
    
      precedence:
      
        __ > mark#
      
      partial status:
    
        pi(mark#) = [1]
        pi(__) = [1, 2]
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          mark#_A(x1) = x1 + 3
          ___A(x1,x2) = max{x1 - 1, x2}
    
      precedence:
      
        mark# = __
      
      partial status:
    
        pi(mark#) = []
        pi(__) = [2]
    

The next rules are strictly ordered:

  p1

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