YES

We show the termination of the TRS R:

  active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
  active(__(X,nil())) -> mark(X)
  active(__(nil(),X)) -> mark(X)
  active(and(tt(),X)) -> mark(X)
  active(isList(V)) -> mark(isNeList(V))
  active(isList(nil())) -> mark(tt())
  active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
  active(isNeList(V)) -> mark(isQid(V))
  active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
  active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
  active(isNePal(V)) -> mark(isQid(V))
  active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
  active(isPal(V)) -> mark(isNePal(V))
  active(isPal(nil())) -> mark(tt())
  active(isQid(a())) -> mark(tt())
  active(isQid(e())) -> mark(tt())
  active(isQid(i())) -> mark(tt())
  active(isQid(o())) -> mark(tt())
  active(isQid(u())) -> mark(tt())
  mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
  mark(nil()) -> active(nil())
  mark(and(X1,X2)) -> active(and(mark(X1),X2))
  mark(tt()) -> active(tt())
  mark(isList(X)) -> active(isList(X))
  mark(isNeList(X)) -> active(isNeList(X))
  mark(isQid(X)) -> active(isQid(X))
  mark(isNePal(X)) -> active(isNePal(X))
  mark(isPal(X)) -> active(isPal(X))
  mark(a()) -> active(a())
  mark(e()) -> active(e())
  mark(i()) -> active(i())
  mark(o()) -> active(o())
  mark(u()) -> active(u())
  __(mark(X1),X2) -> __(X1,X2)
  __(X1,mark(X2)) -> __(X1,X2)
  __(active(X1),X2) -> __(X1,X2)
  __(X1,active(X2)) -> __(X1,X2)
  and(mark(X1),X2) -> and(X1,X2)
  and(X1,mark(X2)) -> and(X1,X2)
  and(active(X1),X2) -> and(X1,X2)
  and(X1,active(X2)) -> and(X1,X2)
  isList(mark(X)) -> isList(X)
  isList(active(X)) -> isList(X)
  isNeList(mark(X)) -> isNeList(X)
  isNeList(active(X)) -> isNeList(X)
  isQid(mark(X)) -> isQid(X)
  isQid(active(X)) -> isQid(X)
  isNePal(mark(X)) -> isNePal(X)
  isNePal(active(X)) -> isNePal(X)
  isPal(mark(X)) -> isPal(X)
  isPal(active(X)) -> isPal(X)

-- SCC decomposition.

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

p1: active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
p2: active#(__(__(X,Y),Z)) -> __#(X,__(Y,Z))
p3: active#(__(__(X,Y),Z)) -> __#(Y,Z)
p4: active#(__(X,nil())) -> mark#(X)
p5: active#(__(nil(),X)) -> mark#(X)
p6: active#(and(tt(),X)) -> mark#(X)
p7: active#(isList(V)) -> mark#(isNeList(V))
p8: active#(isList(V)) -> isNeList#(V)
p9: active#(isList(nil())) -> mark#(tt())
p10: active#(isList(__(V1,V2))) -> mark#(and(isList(V1),isList(V2)))
p11: active#(isList(__(V1,V2))) -> and#(isList(V1),isList(V2))
p12: active#(isList(__(V1,V2))) -> isList#(V1)
p13: active#(isList(__(V1,V2))) -> isList#(V2)
p14: active#(isNeList(V)) -> mark#(isQid(V))
p15: active#(isNeList(V)) -> isQid#(V)
p16: active#(isNeList(__(V1,V2))) -> mark#(and(isList(V1),isNeList(V2)))
p17: active#(isNeList(__(V1,V2))) -> and#(isList(V1),isNeList(V2))
p18: active#(isNeList(__(V1,V2))) -> isList#(V1)
p19: active#(isNeList(__(V1,V2))) -> isNeList#(V2)
p20: active#(isNeList(__(V1,V2))) -> mark#(and(isNeList(V1),isList(V2)))
p21: active#(isNeList(__(V1,V2))) -> and#(isNeList(V1),isList(V2))
p22: active#(isNeList(__(V1,V2))) -> isNeList#(V1)
p23: active#(isNeList(__(V1,V2))) -> isList#(V2)
p24: active#(isNePal(V)) -> mark#(isQid(V))
p25: active#(isNePal(V)) -> isQid#(V)
p26: active#(isNePal(__(I,__(P,I)))) -> mark#(and(isQid(I),isPal(P)))
p27: active#(isNePal(__(I,__(P,I)))) -> and#(isQid(I),isPal(P))
p28: active#(isNePal(__(I,__(P,I)))) -> isQid#(I)
p29: active#(isNePal(__(I,__(P,I)))) -> isPal#(P)
p30: active#(isPal(V)) -> mark#(isNePal(V))
p31: active#(isPal(V)) -> isNePal#(V)
p32: active#(isPal(nil())) -> mark#(tt())
p33: active#(isQid(a())) -> mark#(tt())
p34: active#(isQid(e())) -> mark#(tt())
p35: active#(isQid(i())) -> mark#(tt())
p36: active#(isQid(o())) -> mark#(tt())
p37: active#(isQid(u())) -> mark#(tt())
p38: mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
p39: mark#(__(X1,X2)) -> __#(mark(X1),mark(X2))
p40: mark#(__(X1,X2)) -> mark#(X1)
p41: mark#(__(X1,X2)) -> mark#(X2)
p42: mark#(nil()) -> active#(nil())
p43: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p44: mark#(and(X1,X2)) -> and#(mark(X1),X2)
p45: mark#(and(X1,X2)) -> mark#(X1)
p46: mark#(tt()) -> active#(tt())
p47: mark#(isList(X)) -> active#(isList(X))
p48: mark#(isNeList(X)) -> active#(isNeList(X))
p49: mark#(isQid(X)) -> active#(isQid(X))
p50: mark#(isNePal(X)) -> active#(isNePal(X))
p51: mark#(isPal(X)) -> active#(isPal(X))
p52: mark#(a()) -> active#(a())
p53: mark#(e()) -> active#(e())
p54: mark#(i()) -> active#(i())
p55: mark#(o()) -> active#(o())
p56: mark#(u()) -> active#(u())
p57: __#(mark(X1),X2) -> __#(X1,X2)
p58: __#(X1,mark(X2)) -> __#(X1,X2)
p59: __#(active(X1),X2) -> __#(X1,X2)
p60: __#(X1,active(X2)) -> __#(X1,X2)
p61: and#(mark(X1),X2) -> and#(X1,X2)
p62: and#(X1,mark(X2)) -> and#(X1,X2)
p63: and#(active(X1),X2) -> and#(X1,X2)
p64: and#(X1,active(X2)) -> and#(X1,X2)
p65: isList#(mark(X)) -> isList#(X)
p66: isList#(active(X)) -> isList#(X)
p67: isNeList#(mark(X)) -> isNeList#(X)
p68: isNeList#(active(X)) -> isNeList#(X)
p69: isQid#(mark(X)) -> isQid#(X)
p70: isQid#(active(X)) -> isQid#(X)
p71: isNePal#(mark(X)) -> isNePal#(X)
p72: isNePal#(active(X)) -> isNePal#(X)
p73: isPal#(mark(X)) -> isPal#(X)
p74: isPal#(active(X)) -> isPal#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r21: mark(nil()) -> active(nil())
r22: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r23: mark(tt()) -> active(tt())
r24: mark(isList(X)) -> active(isList(X))
r25: mark(isNeList(X)) -> active(isNeList(X))
r26: mark(isQid(X)) -> active(isQid(X))
r27: mark(isNePal(X)) -> active(isNePal(X))
r28: mark(isPal(X)) -> active(isPal(X))
r29: mark(a()) -> active(a())
r30: mark(e()) -> active(e())
r31: mark(i()) -> active(i())
r32: mark(o()) -> active(o())
r33: mark(u()) -> active(u())
r34: __(mark(X1),X2) -> __(X1,X2)
r35: __(X1,mark(X2)) -> __(X1,X2)
r36: __(active(X1),X2) -> __(X1,X2)
r37: __(X1,active(X2)) -> __(X1,X2)
r38: and(mark(X1),X2) -> and(X1,X2)
r39: and(X1,mark(X2)) -> and(X1,X2)
r40: and(active(X1),X2) -> and(X1,X2)
r41: and(X1,active(X2)) -> and(X1,X2)
r42: isList(mark(X)) -> isList(X)
r43: isList(active(X)) -> isList(X)
r44: isNeList(mark(X)) -> isNeList(X)
r45: isNeList(active(X)) -> isNeList(X)
r46: isQid(mark(X)) -> isQid(X)
r47: isQid(active(X)) -> isQid(X)
r48: isNePal(mark(X)) -> isNePal(X)
r49: isNePal(active(X)) -> isNePal(X)
r50: isPal(mark(X)) -> isPal(X)
r51: isPal(active(X)) -> isPal(X)

The estimated dependency graph contains the following SCCs:

  {p1, p4, p5, p6, p7, p10, p14, p16, p20, p24, p26, p30, p38, p40, p41, p43, p45, p47, p48, p49, p50, p51}
  {p57, p58, p59, p60}
  {p67, p68}
  {p61, p62, p63, p64}
  {p65, p66}
  {p69, p70}
  {p73, p74}
  {p71, p72}


-- Reduction pair.

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

p1: active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
p2: mark#(isPal(X)) -> active#(isPal(X))
p3: active#(isPal(V)) -> mark#(isNePal(V))
p4: mark#(isNePal(X)) -> active#(isNePal(X))
p5: active#(isNePal(__(I,__(P,I)))) -> mark#(and(isQid(I),isPal(P)))
p6: mark#(isQid(X)) -> active#(isQid(X))
p7: active#(isNePal(V)) -> mark#(isQid(V))
p8: mark#(isNeList(X)) -> active#(isNeList(X))
p9: active#(isNeList(__(V1,V2))) -> mark#(and(isNeList(V1),isList(V2)))
p10: mark#(isList(X)) -> active#(isList(X))
p11: active#(isNeList(__(V1,V2))) -> mark#(and(isList(V1),isNeList(V2)))
p12: mark#(and(X1,X2)) -> mark#(X1)
p13: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p14: active#(isNeList(V)) -> mark#(isQid(V))
p15: mark#(__(X1,X2)) -> mark#(X2)
p16: mark#(__(X1,X2)) -> mark#(X1)
p17: mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
p18: active#(isList(__(V1,V2))) -> mark#(and(isList(V1),isList(V2)))
p19: active#(isList(V)) -> mark#(isNeList(V))
p20: active#(and(tt(),X)) -> mark#(X)
p21: active#(__(nil(),X)) -> mark#(X)
p22: active#(__(X,nil())) -> mark#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r21: mark(nil()) -> active(nil())
r22: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r23: mark(tt()) -> active(tt())
r24: mark(isList(X)) -> active(isList(X))
r25: mark(isNeList(X)) -> active(isNeList(X))
r26: mark(isQid(X)) -> active(isQid(X))
r27: mark(isNePal(X)) -> active(isNePal(X))
r28: mark(isPal(X)) -> active(isPal(X))
r29: mark(a()) -> active(a())
r30: mark(e()) -> active(e())
r31: mark(i()) -> active(i())
r32: mark(o()) -> active(o())
r33: mark(u()) -> active(u())
r34: __(mark(X1),X2) -> __(X1,X2)
r35: __(X1,mark(X2)) -> __(X1,X2)
r36: __(active(X1),X2) -> __(X1,X2)
r37: __(X1,active(X2)) -> __(X1,X2)
r38: and(mark(X1),X2) -> and(X1,X2)
r39: and(X1,mark(X2)) -> and(X1,X2)
r40: and(active(X1),X2) -> and(X1,X2)
r41: and(X1,active(X2)) -> and(X1,X2)
r42: isList(mark(X)) -> isList(X)
r43: isList(active(X)) -> isList(X)
r44: isNeList(mark(X)) -> isNeList(X)
r45: isNeList(active(X)) -> isNeList(X)
r46: isQid(mark(X)) -> isQid(X)
r47: isQid(active(X)) -> isQid(X)
r48: isNePal(mark(X)) -> isNePal(X)
r49: isNePal(active(X)) -> isNePal(X)
r50: isPal(mark(X)) -> isPal(X)
r51: isPal(active(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, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      isList > __ > isQid > isPal > mark > active > o > u > i > e > a > and > active# > mark# > nil > tt > isNeList > isNePal
    
    argument filter:
  
      pi(active#) = 1
      pi(__) = [1, 2]
      pi(mark#) = 1
      pi(isPal) = [1]
      pi(isNePal) = [1]
      pi(and) = [1, 2]
      pi(isQid) = 1
      pi(isNeList) = 1
      pi(isList) = 1
      pi(mark) = 1
      pi(tt) = []
      pi(nil) = []
      pi(active) = 1
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p1, p3, p5, p7, p9, p11, p12, p15, p16, p18, p20, p21, p22
  r1, r2, r3, r4, r6, r7, r9, r10, r11, 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: mark#(isPal(X)) -> active#(isPal(X))
p2: mark#(isNePal(X)) -> active#(isNePal(X))
p3: mark#(isQid(X)) -> active#(isQid(X))
p4: mark#(isNeList(X)) -> active#(isNeList(X))
p5: mark#(isList(X)) -> active#(isList(X))
p6: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p7: active#(isNeList(V)) -> mark#(isQid(V))
p8: mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
p9: active#(isList(V)) -> mark#(isNeList(V))

and R consists of:

r1: active(isList(V)) -> mark(isNeList(V))
r2: active(isNeList(V)) -> mark(isQid(V))
r3: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r4: mark(nil()) -> active(nil())
r5: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r6: mark(tt()) -> active(tt())
r7: mark(isList(X)) -> active(isList(X))
r8: mark(isNeList(X)) -> active(isNeList(X))
r9: mark(isQid(X)) -> active(isQid(X))
r10: mark(isNePal(X)) -> active(isNePal(X))
r11: mark(isPal(X)) -> active(isPal(X))
r12: mark(a()) -> active(a())
r13: mark(e()) -> active(e())
r14: mark(i()) -> active(i())
r15: mark(o()) -> active(o())
r16: mark(u()) -> active(u())
r17: __(mark(X1),X2) -> __(X1,X2)
r18: __(X1,mark(X2)) -> __(X1,X2)
r19: __(active(X1),X2) -> __(X1,X2)
r20: __(X1,active(X2)) -> __(X1,X2)
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: isList(mark(X)) -> isList(X)
r26: isList(active(X)) -> isList(X)
r27: isNeList(mark(X)) -> isNeList(X)
r28: isNeList(active(X)) -> isNeList(X)
r29: isQid(mark(X)) -> isQid(X)
r30: isQid(active(X)) -> isQid(X)
r31: isNePal(mark(X)) -> isNePal(X)
r32: isNePal(active(X)) -> isNePal(X)
r33: isPal(mark(X)) -> isPal(X)
r34: isPal(active(X)) -> isPal(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2, p3, p4, p5, p6, p7, p8, p9}


-- Reduction pair.

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

p1: mark#(isPal(X)) -> active#(isPal(X))
p2: active#(isList(V)) -> mark#(isNeList(V))
p3: mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
p4: active#(isNeList(V)) -> mark#(isQid(V))
p5: mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
p6: mark#(isList(X)) -> active#(isList(X))
p7: mark#(isNeList(X)) -> active#(isNeList(X))
p8: mark#(isQid(X)) -> active#(isQid(X))
p9: mark#(isNePal(X)) -> active#(isNePal(X))

and R consists of:

r1: active(isList(V)) -> mark(isNeList(V))
r2: active(isNeList(V)) -> mark(isQid(V))
r3: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r4: mark(nil()) -> active(nil())
r5: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r6: mark(tt()) -> active(tt())
r7: mark(isList(X)) -> active(isList(X))
r8: mark(isNeList(X)) -> active(isNeList(X))
r9: mark(isQid(X)) -> active(isQid(X))
r10: mark(isNePal(X)) -> active(isNePal(X))
r11: mark(isPal(X)) -> active(isPal(X))
r12: mark(a()) -> active(a())
r13: mark(e()) -> active(e())
r14: mark(i()) -> active(i())
r15: mark(o()) -> active(o())
r16: mark(u()) -> active(u())
r17: __(mark(X1),X2) -> __(X1,X2)
r18: __(X1,mark(X2)) -> __(X1,X2)
r19: __(active(X1),X2) -> __(X1,X2)
r20: __(X1,active(X2)) -> __(X1,X2)
r21: and(mark(X1),X2) -> and(X1,X2)
r22: and(X1,mark(X2)) -> and(X1,X2)
r23: and(active(X1),X2) -> and(X1,X2)
r24: and(X1,active(X2)) -> and(X1,X2)
r25: isList(mark(X)) -> isList(X)
r26: isList(active(X)) -> isList(X)
r27: isNeList(mark(X)) -> isNeList(X)
r28: isNeList(active(X)) -> isNeList(X)
r29: isQid(mark(X)) -> isQid(X)
r30: isQid(active(X)) -> isQid(X)
r31: isNePal(mark(X)) -> isNePal(X)
r32: isNePal(active(X)) -> isNePal(X)
r33: isPal(mark(X)) -> isPal(X)
r34: isPal(active(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

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      active > u > o > i > e > a > tt > nil > active# > isNePal > and > isQid > __ > isList > isNeList > isPal > mark > mark#
    
    argument filter:
  
      pi(mark#) = [1]
      pi(isPal) = 1
      pi(active#) = 1
      pi(isList) = [1]
      pi(isNeList) = [1]
      pi(__) = []
      pi(mark) = [1]
      pi(isQid) = 1
      pi(and) = [2]
      pi(isNePal) = [1]
      pi(active) = 1
      pi(nil) = []
      pi(tt) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

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

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) -> __#(X1,X2)
p2: __#(X1,active(X2)) -> __#(X1,X2)
p3: __#(active(X1),X2) -> __#(X1,X2)
p4: __#(X1,mark(X2)) -> __#(X1,X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r21: mark(nil()) -> active(nil())
r22: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r23: mark(tt()) -> active(tt())
r24: mark(isList(X)) -> active(isList(X))
r25: mark(isNeList(X)) -> active(isNeList(X))
r26: mark(isQid(X)) -> active(isQid(X))
r27: mark(isNePal(X)) -> active(isNePal(X))
r28: mark(isPal(X)) -> active(isPal(X))
r29: mark(a()) -> active(a())
r30: mark(e()) -> active(e())
r31: mark(i()) -> active(i())
r32: mark(o()) -> active(o())
r33: mark(u()) -> active(u())
r34: __(mark(X1),X2) -> __(X1,X2)
r35: __(X1,mark(X2)) -> __(X1,X2)
r36: __(active(X1),X2) -> __(X1,X2)
r37: __(X1,active(X2)) -> __(X1,X2)
r38: and(mark(X1),X2) -> and(X1,X2)
r39: and(X1,mark(X2)) -> and(X1,X2)
r40: and(active(X1),X2) -> and(X1,X2)
r41: and(X1,active(X2)) -> and(X1,X2)
r42: isList(mark(X)) -> isList(X)
r43: isList(active(X)) -> isList(X)
r44: isNeList(mark(X)) -> isNeList(X)
r45: isNeList(active(X)) -> isNeList(X)
r46: isQid(mark(X)) -> isQid(X)
r47: isQid(active(X)) -> isQid(X)
r48: isNePal(mark(X)) -> isNePal(X)
r49: isNePal(active(X)) -> isNePal(X)
r50: isPal(mark(X)) -> isPal(X)
r51: isPal(active(X)) -> isPal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      __# > active > mark
    
    argument filter:
  
      pi(__#) = 2
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p2, p4

We remove them from the problem.

-- SCC decomposition.

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

p1: __#(mark(X1),X2) -> __#(X1,X2)
p2: __#(active(X1),X2) -> __#(X1,X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r21: mark(nil()) -> active(nil())
r22: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r23: mark(tt()) -> active(tt())
r24: mark(isList(X)) -> active(isList(X))
r25: mark(isNeList(X)) -> active(isNeList(X))
r26: mark(isQid(X)) -> active(isQid(X))
r27: mark(isNePal(X)) -> active(isNePal(X))
r28: mark(isPal(X)) -> active(isPal(X))
r29: mark(a()) -> active(a())
r30: mark(e()) -> active(e())
r31: mark(i()) -> active(i())
r32: mark(o()) -> active(o())
r33: mark(u()) -> active(u())
r34: __(mark(X1),X2) -> __(X1,X2)
r35: __(X1,mark(X2)) -> __(X1,X2)
r36: __(active(X1),X2) -> __(X1,X2)
r37: __(X1,active(X2)) -> __(X1,X2)
r38: and(mark(X1),X2) -> and(X1,X2)
r39: and(X1,mark(X2)) -> and(X1,X2)
r40: and(active(X1),X2) -> and(X1,X2)
r41: and(X1,active(X2)) -> and(X1,X2)
r42: isList(mark(X)) -> isList(X)
r43: isList(active(X)) -> isList(X)
r44: isNeList(mark(X)) -> isNeList(X)
r45: isNeList(active(X)) -> isNeList(X)
r46: isQid(mark(X)) -> isQid(X)
r47: isQid(active(X)) -> isQid(X)
r48: isNePal(mark(X)) -> isNePal(X)
r49: isNePal(active(X)) -> isNePal(X)
r50: isPal(mark(X)) -> isPal(X)
r51: isPal(active(X)) -> isPal(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

p1: __#(mark(X1),X2) -> __#(X1,X2)
p2: __#(active(X1),X2) -> __#(X1,X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r21: mark(nil()) -> active(nil())
r22: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r23: mark(tt()) -> active(tt())
r24: mark(isList(X)) -> active(isList(X))
r25: mark(isNeList(X)) -> active(isNeList(X))
r26: mark(isQid(X)) -> active(isQid(X))
r27: mark(isNePal(X)) -> active(isNePal(X))
r28: mark(isPal(X)) -> active(isPal(X))
r29: mark(a()) -> active(a())
r30: mark(e()) -> active(e())
r31: mark(i()) -> active(i())
r32: mark(o()) -> active(o())
r33: mark(u()) -> active(u())
r34: __(mark(X1),X2) -> __(X1,X2)
r35: __(X1,mark(X2)) -> __(X1,X2)
r36: __(active(X1),X2) -> __(X1,X2)
r37: __(X1,active(X2)) -> __(X1,X2)
r38: and(mark(X1),X2) -> and(X1,X2)
r39: and(X1,mark(X2)) -> and(X1,X2)
r40: and(active(X1),X2) -> and(X1,X2)
r41: and(X1,active(X2)) -> and(X1,X2)
r42: isList(mark(X)) -> isList(X)
r43: isList(active(X)) -> isList(X)
r44: isNeList(mark(X)) -> isNeList(X)
r45: isNeList(active(X)) -> isNeList(X)
r46: isQid(mark(X)) -> isQid(X)
r47: isQid(active(X)) -> isQid(X)
r48: isNePal(mark(X)) -> isNePal(X)
r49: isNePal(active(X)) -> isNePal(X)
r50: isPal(mark(X)) -> isPal(X)
r51: isPal(active(X)) -> isPal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      __# > active > mark
    
    argument filter:
  
      pi(__#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2

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: isNeList#(mark(X)) -> isNeList#(X)
p2: isNeList#(active(X)) -> isNeList#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r21: mark(nil()) -> active(nil())
r22: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r23: mark(tt()) -> active(tt())
r24: mark(isList(X)) -> active(isList(X))
r25: mark(isNeList(X)) -> active(isNeList(X))
r26: mark(isQid(X)) -> active(isQid(X))
r27: mark(isNePal(X)) -> active(isNePal(X))
r28: mark(isPal(X)) -> active(isPal(X))
r29: mark(a()) -> active(a())
r30: mark(e()) -> active(e())
r31: mark(i()) -> active(i())
r32: mark(o()) -> active(o())
r33: mark(u()) -> active(u())
r34: __(mark(X1),X2) -> __(X1,X2)
r35: __(X1,mark(X2)) -> __(X1,X2)
r36: __(active(X1),X2) -> __(X1,X2)
r37: __(X1,active(X2)) -> __(X1,X2)
r38: and(mark(X1),X2) -> and(X1,X2)
r39: and(X1,mark(X2)) -> and(X1,X2)
r40: and(active(X1),X2) -> and(X1,X2)
r41: and(X1,active(X2)) -> and(X1,X2)
r42: isList(mark(X)) -> isList(X)
r43: isList(active(X)) -> isList(X)
r44: isNeList(mark(X)) -> isNeList(X)
r45: isNeList(active(X)) -> isNeList(X)
r46: isQid(mark(X)) -> isQid(X)
r47: isQid(active(X)) -> isQid(X)
r48: isNePal(mark(X)) -> isNePal(X)
r49: isNePal(active(X)) -> isNePal(X)
r50: isPal(mark(X)) -> isPal(X)
r51: isPal(active(X)) -> isPal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      isNeList# > active > mark
    
    argument filter:
  
      pi(isNeList#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51

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: and#(mark(X1),X2) -> and#(X1,X2)
p2: and#(X1,active(X2)) -> and#(X1,X2)
p3: and#(active(X1),X2) -> and#(X1,X2)
p4: and#(X1,mark(X2)) -> and#(X1,X2)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r21: mark(nil()) -> active(nil())
r22: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r23: mark(tt()) -> active(tt())
r24: mark(isList(X)) -> active(isList(X))
r25: mark(isNeList(X)) -> active(isNeList(X))
r26: mark(isQid(X)) -> active(isQid(X))
r27: mark(isNePal(X)) -> active(isNePal(X))
r28: mark(isPal(X)) -> active(isPal(X))
r29: mark(a()) -> active(a())
r30: mark(e()) -> active(e())
r31: mark(i()) -> active(i())
r32: mark(o()) -> active(o())
r33: mark(u()) -> active(u())
r34: __(mark(X1),X2) -> __(X1,X2)
r35: __(X1,mark(X2)) -> __(X1,X2)
r36: __(active(X1),X2) -> __(X1,X2)
r37: __(X1,active(X2)) -> __(X1,X2)
r38: and(mark(X1),X2) -> and(X1,X2)
r39: and(X1,mark(X2)) -> and(X1,X2)
r40: and(active(X1),X2) -> and(X1,X2)
r41: and(X1,active(X2)) -> and(X1,X2)
r42: isList(mark(X)) -> isList(X)
r43: isList(active(X)) -> isList(X)
r44: isNeList(mark(X)) -> isNeList(X)
r45: isNeList(active(X)) -> isNeList(X)
r46: isQid(mark(X)) -> isQid(X)
r47: isQid(active(X)) -> isQid(X)
r48: isNePal(mark(X)) -> isNePal(X)
r49: isNePal(active(X)) -> isNePal(X)
r50: isPal(mark(X)) -> isPal(X)
r51: isPal(active(X)) -> isPal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      and# > active > mark
    
    argument filter:
  
      pi(and#) = 2
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p2, p4

We remove them from the problem.

-- SCC decomposition.

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

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

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r21: mark(nil()) -> active(nil())
r22: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r23: mark(tt()) -> active(tt())
r24: mark(isList(X)) -> active(isList(X))
r25: mark(isNeList(X)) -> active(isNeList(X))
r26: mark(isQid(X)) -> active(isQid(X))
r27: mark(isNePal(X)) -> active(isNePal(X))
r28: mark(isPal(X)) -> active(isPal(X))
r29: mark(a()) -> active(a())
r30: mark(e()) -> active(e())
r31: mark(i()) -> active(i())
r32: mark(o()) -> active(o())
r33: mark(u()) -> active(u())
r34: __(mark(X1),X2) -> __(X1,X2)
r35: __(X1,mark(X2)) -> __(X1,X2)
r36: __(active(X1),X2) -> __(X1,X2)
r37: __(X1,active(X2)) -> __(X1,X2)
r38: and(mark(X1),X2) -> and(X1,X2)
r39: and(X1,mark(X2)) -> and(X1,X2)
r40: and(active(X1),X2) -> and(X1,X2)
r41: and(X1,active(X2)) -> and(X1,X2)
r42: isList(mark(X)) -> isList(X)
r43: isList(active(X)) -> isList(X)
r44: isNeList(mark(X)) -> isNeList(X)
r45: isNeList(active(X)) -> isNeList(X)
r46: isQid(mark(X)) -> isQid(X)
r47: isQid(active(X)) -> isQid(X)
r48: isNePal(mark(X)) -> isNePal(X)
r49: isNePal(active(X)) -> isNePal(X)
r50: isPal(mark(X)) -> isPal(X)
r51: isPal(active(X)) -> isPal(X)

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

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

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

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r21: mark(nil()) -> active(nil())
r22: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r23: mark(tt()) -> active(tt())
r24: mark(isList(X)) -> active(isList(X))
r25: mark(isNeList(X)) -> active(isNeList(X))
r26: mark(isQid(X)) -> active(isQid(X))
r27: mark(isNePal(X)) -> active(isNePal(X))
r28: mark(isPal(X)) -> active(isPal(X))
r29: mark(a()) -> active(a())
r30: mark(e()) -> active(e())
r31: mark(i()) -> active(i())
r32: mark(o()) -> active(o())
r33: mark(u()) -> active(u())
r34: __(mark(X1),X2) -> __(X1,X2)
r35: __(X1,mark(X2)) -> __(X1,X2)
r36: __(active(X1),X2) -> __(X1,X2)
r37: __(X1,active(X2)) -> __(X1,X2)
r38: and(mark(X1),X2) -> and(X1,X2)
r39: and(X1,mark(X2)) -> and(X1,X2)
r40: and(active(X1),X2) -> and(X1,X2)
r41: and(X1,active(X2)) -> and(X1,X2)
r42: isList(mark(X)) -> isList(X)
r43: isList(active(X)) -> isList(X)
r44: isNeList(mark(X)) -> isNeList(X)
r45: isNeList(active(X)) -> isNeList(X)
r46: isQid(mark(X)) -> isQid(X)
r47: isQid(active(X)) -> isQid(X)
r48: isNePal(mark(X)) -> isNePal(X)
r49: isNePal(active(X)) -> isNePal(X)
r50: isPal(mark(X)) -> isPal(X)
r51: isPal(active(X)) -> isPal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      and# > active > mark
    
    argument filter:
  
      pi(and#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2

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: isList#(mark(X)) -> isList#(X)
p2: isList#(active(X)) -> isList#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r21: mark(nil()) -> active(nil())
r22: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r23: mark(tt()) -> active(tt())
r24: mark(isList(X)) -> active(isList(X))
r25: mark(isNeList(X)) -> active(isNeList(X))
r26: mark(isQid(X)) -> active(isQid(X))
r27: mark(isNePal(X)) -> active(isNePal(X))
r28: mark(isPal(X)) -> active(isPal(X))
r29: mark(a()) -> active(a())
r30: mark(e()) -> active(e())
r31: mark(i()) -> active(i())
r32: mark(o()) -> active(o())
r33: mark(u()) -> active(u())
r34: __(mark(X1),X2) -> __(X1,X2)
r35: __(X1,mark(X2)) -> __(X1,X2)
r36: __(active(X1),X2) -> __(X1,X2)
r37: __(X1,active(X2)) -> __(X1,X2)
r38: and(mark(X1),X2) -> and(X1,X2)
r39: and(X1,mark(X2)) -> and(X1,X2)
r40: and(active(X1),X2) -> and(X1,X2)
r41: and(X1,active(X2)) -> and(X1,X2)
r42: isList(mark(X)) -> isList(X)
r43: isList(active(X)) -> isList(X)
r44: isNeList(mark(X)) -> isNeList(X)
r45: isNeList(active(X)) -> isNeList(X)
r46: isQid(mark(X)) -> isQid(X)
r47: isQid(active(X)) -> isQid(X)
r48: isNePal(mark(X)) -> isNePal(X)
r49: isNePal(active(X)) -> isNePal(X)
r50: isPal(mark(X)) -> isPal(X)
r51: isPal(active(X)) -> isPal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      isList# > active > mark
    
    argument filter:
  
      pi(isList#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51

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: isQid#(mark(X)) -> isQid#(X)
p2: isQid#(active(X)) -> isQid#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r21: mark(nil()) -> active(nil())
r22: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r23: mark(tt()) -> active(tt())
r24: mark(isList(X)) -> active(isList(X))
r25: mark(isNeList(X)) -> active(isNeList(X))
r26: mark(isQid(X)) -> active(isQid(X))
r27: mark(isNePal(X)) -> active(isNePal(X))
r28: mark(isPal(X)) -> active(isPal(X))
r29: mark(a()) -> active(a())
r30: mark(e()) -> active(e())
r31: mark(i()) -> active(i())
r32: mark(o()) -> active(o())
r33: mark(u()) -> active(u())
r34: __(mark(X1),X2) -> __(X1,X2)
r35: __(X1,mark(X2)) -> __(X1,X2)
r36: __(active(X1),X2) -> __(X1,X2)
r37: __(X1,active(X2)) -> __(X1,X2)
r38: and(mark(X1),X2) -> and(X1,X2)
r39: and(X1,mark(X2)) -> and(X1,X2)
r40: and(active(X1),X2) -> and(X1,X2)
r41: and(X1,active(X2)) -> and(X1,X2)
r42: isList(mark(X)) -> isList(X)
r43: isList(active(X)) -> isList(X)
r44: isNeList(mark(X)) -> isNeList(X)
r45: isNeList(active(X)) -> isNeList(X)
r46: isQid(mark(X)) -> isQid(X)
r47: isQid(active(X)) -> isQid(X)
r48: isNePal(mark(X)) -> isNePal(X)
r49: isNePal(active(X)) -> isNePal(X)
r50: isPal(mark(X)) -> isPal(X)
r51: isPal(active(X)) -> isPal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      isQid# > active > mark
    
    argument filter:
  
      pi(isQid#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51

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: isPal#(mark(X)) -> isPal#(X)
p2: isPal#(active(X)) -> isPal#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r21: mark(nil()) -> active(nil())
r22: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r23: mark(tt()) -> active(tt())
r24: mark(isList(X)) -> active(isList(X))
r25: mark(isNeList(X)) -> active(isNeList(X))
r26: mark(isQid(X)) -> active(isQid(X))
r27: mark(isNePal(X)) -> active(isNePal(X))
r28: mark(isPal(X)) -> active(isPal(X))
r29: mark(a()) -> active(a())
r30: mark(e()) -> active(e())
r31: mark(i()) -> active(i())
r32: mark(o()) -> active(o())
r33: mark(u()) -> active(u())
r34: __(mark(X1),X2) -> __(X1,X2)
r35: __(X1,mark(X2)) -> __(X1,X2)
r36: __(active(X1),X2) -> __(X1,X2)
r37: __(X1,active(X2)) -> __(X1,X2)
r38: and(mark(X1),X2) -> and(X1,X2)
r39: and(X1,mark(X2)) -> and(X1,X2)
r40: and(active(X1),X2) -> and(X1,X2)
r41: and(X1,active(X2)) -> and(X1,X2)
r42: isList(mark(X)) -> isList(X)
r43: isList(active(X)) -> isList(X)
r44: isNeList(mark(X)) -> isNeList(X)
r45: isNeList(active(X)) -> isNeList(X)
r46: isQid(mark(X)) -> isQid(X)
r47: isQid(active(X)) -> isQid(X)
r48: isNePal(mark(X)) -> isNePal(X)
r49: isNePal(active(X)) -> isNePal(X)
r50: isPal(mark(X)) -> isPal(X)
r51: isPal(active(X)) -> isPal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      isPal# > active > mark
    
    argument filter:
  
      pi(isPal#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51

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: isNePal#(mark(X)) -> isNePal#(X)
p2: isNePal#(active(X)) -> isNePal#(X)

and R consists of:

r1: active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
r2: active(__(X,nil())) -> mark(X)
r3: active(__(nil(),X)) -> mark(X)
r4: active(and(tt(),X)) -> mark(X)
r5: active(isList(V)) -> mark(isNeList(V))
r6: active(isList(nil())) -> mark(tt())
r7: active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
r8: active(isNeList(V)) -> mark(isQid(V))
r9: active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
r10: active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
r11: active(isNePal(V)) -> mark(isQid(V))
r12: active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
r13: active(isPal(V)) -> mark(isNePal(V))
r14: active(isPal(nil())) -> mark(tt())
r15: active(isQid(a())) -> mark(tt())
r16: active(isQid(e())) -> mark(tt())
r17: active(isQid(i())) -> mark(tt())
r18: active(isQid(o())) -> mark(tt())
r19: active(isQid(u())) -> mark(tt())
r20: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r21: mark(nil()) -> active(nil())
r22: mark(and(X1,X2)) -> active(and(mark(X1),X2))
r23: mark(tt()) -> active(tt())
r24: mark(isList(X)) -> active(isList(X))
r25: mark(isNeList(X)) -> active(isNeList(X))
r26: mark(isQid(X)) -> active(isQid(X))
r27: mark(isNePal(X)) -> active(isNePal(X))
r28: mark(isPal(X)) -> active(isPal(X))
r29: mark(a()) -> active(a())
r30: mark(e()) -> active(e())
r31: mark(i()) -> active(i())
r32: mark(o()) -> active(o())
r33: mark(u()) -> active(u())
r34: __(mark(X1),X2) -> __(X1,X2)
r35: __(X1,mark(X2)) -> __(X1,X2)
r36: __(active(X1),X2) -> __(X1,X2)
r37: __(X1,active(X2)) -> __(X1,X2)
r38: and(mark(X1),X2) -> and(X1,X2)
r39: and(X1,mark(X2)) -> and(X1,X2)
r40: and(active(X1),X2) -> and(X1,X2)
r41: and(X1,active(X2)) -> and(X1,X2)
r42: isList(mark(X)) -> isList(X)
r43: isList(active(X)) -> isList(X)
r44: isNeList(mark(X)) -> isNeList(X)
r45: isNeList(active(X)) -> isNeList(X)
r46: isQid(mark(X)) -> isQid(X)
r47: isQid(active(X)) -> isQid(X)
r48: isNePal(mark(X)) -> isNePal(X)
r49: isNePal(active(X)) -> isNePal(X)
r50: isPal(mark(X)) -> isPal(X)
r51: isPal(active(X)) -> isPal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic path order with precedence:
  
    precedence:
    
      isNePal# > active > mark
    
    argument filter:
  
      pi(isNePal#) = 1
      pi(mark) = [1]
      pi(active) = [1]

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45, r46, r47, r48, r49, r50, r51

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