YES

We show the termination of the TRS R:

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

-- SCC decomposition.

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

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

and R consists of:

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

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      a____#_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(0,0,0,0)) x1 + ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,1,0,0)) x2 + (0,3,0,1)
      ___A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(0,0,0,0)) x1 + ((1,0,0,0),(0,0,0,0),(1,0,0,0),(1,0,0,0)) x2 + (15,0,15,1)
      mark_A(x1) = ((1,0,0,0),(1,1,0,0),(0,1,0,0),(1,0,1,0)) x1 + (0,13,12,24)
      a_____A(x1,x2) = ((1,0,0,0),(1,1,0,0),(0,0,1,0),(1,0,0,0)) x1 + ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x2 + (15,14,0,54)
      nil_A() = (32,2,13,1)
      mark#_A(x1) = ((1,0,0,0),(1,0,0,0),(0,1,0,0),(0,0,1,0)) x1 + (14,0,31,0)
      U81_A(x1) = x1 + (2,1,12,0)
      U72_A(x1) = x1 + (0,20,18,0)
      U71_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,0,0),(0,1,1,0)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,0,0),(1,0,0,0)) x2 + (6,0,11,0)
      U61_A(x1) = ((1,0,0,0),(1,1,0,0),(1,0,1,0),(0,0,0,0)) x1
      U52_A(x1) = x1 + (1,18,1,34)
      U51_A(x1,x2) = x1 + x2 + (8,0,1,0)
      U42_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,0,0),(0,1,0,0)) x1 + (2,0,9,0)
      U41_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(1,1,0,0),(0,0,0,0)) x1 + ((1,0,0,0),(0,0,0,0),(1,0,0,0),(1,0,0,0)) x2 + (11,0,0,0)
      U31_A(x1) = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x1 + (5,0,6,35)
      U22_A(x1) = ((1,0,0,0),(0,0,0,0),(0,1,0,0),(0,1,1,0)) x1 + (8,0,10,42)
      U21_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(1,1,0,0),(0,0,0,0)) x1 + x2 + (15,0,1,0)
      U11_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,0,1,0)) x1 + (2,0,1,0)
      a__U11_A(x1) = ((1,0,0,0),(1,1,0,0),(1,0,1,0),(1,0,0,0)) x1 + (2,1,0,27)
      tt_A() = (10,18,10,33)
      a__U21_A(x1,x2) = x1 + x2 + (15,1,13,40)
      a__U22_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + (8,21,11,41)
      a__isList_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,0,0),(1,0,0,0)) x1 + (16,29,12,0)
      a__U31_A(x1) = x1 + (5,17,11,34)
      a__U41_A(x1,x2) = x1 + ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,0,0,0)) x2 + (11,24,12,35)
      a__U42_A(x1) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(0,0,0,0)) x1 + (2,1,0,34)
      a__isNeList_A(x1) = ((1,0,0,0),(1,0,0,0),(0,0,0,0),(1,1,0,0)) x1 + (13,16,13,21)
      a__U51_A(x1,x2) = x1 + x2 + (8,1,14,0)
      a__U52_A(x1) = x1 + (1,18,15,34)
      a__U61_A(x1) = ((1,0,0,0),(1,1,0,0),(1,0,1,0),(0,0,0,0)) x1
      a__U71_A(x1,x2) = x1 + x2 + (6,6,12,40)
      a__U72_A(x1) = x1 + (0,20,19,41)
      a__isPal_A(x1) = x1 + (16,3,13,32)
      a__U81_A(x1) = x1 + (2,2,12,32)
      a__isQid_A(x1) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(1,0,0,0)) x1 + (7,19,13,0)
      a__isNePal_A(x1) = x1 + (14,26,11,39)
      a_A() = (3,0,1,0)
      e_A() = (4,0,0,0)
      i_A() = (4,0,0,0)
      o_A() = (4,0,0,1)
      u_A() = (34,0,1,0)
      isList_A(x1) = x1 + (16,0,0,1)
      isNeList_A(x1) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + (13,0,1,21)
      isPal_A(x1) = ((1,0,0,0),(0,0,0,0),(0,1,0,0),(1,0,0,0)) x1 + (16,0,1,33)
      isQid_A(x1) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,1,0,0)) x1 + (7,0,0,0)
      isNePal_A(x1) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(1,0,0,0)) x1 + (14,0,0,40)

The next rules are strictly ordered:

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

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(U61(X)) -> mark#(X)

and R consists of:

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

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: mark#(U61(X)) -> mark#(X)

and R consists of:

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

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      mark#_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,1)) x1
      U61_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,0)) x1 + (1,0,0,1)

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: a__U21#(tt(),V2) -> a__isList#(V2)
p2: a__isList#(__(V1,V2)) -> a__isList#(V1)
p3: a__isList#(__(V1,V2)) -> a__U21#(a__isList(V1),V2)
p4: a__isList#(V) -> a__isNeList#(V)
p5: a__isNeList#(__(V1,V2)) -> a__isNeList#(V1)
p6: a__isNeList#(__(V1,V2)) -> a__U51#(a__isNeList(V1),V2)
p7: a__U51#(tt(),V2) -> a__isList#(V2)
p8: a__isNeList#(__(V1,V2)) -> a__isList#(V1)
p9: a__isNeList#(__(V1,V2)) -> a__U41#(a__isList(V1),V2)
p10: a__U41#(tt(),V2) -> a__isNeList#(V2)

and R consists of:

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

The set of usable rules consists of

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

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      a__U21#_A(x1,x2) = ((0,0,0,0),(1,0,0,0),(0,1,0,0),(0,0,1,0)) x1 + ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,1,0,0)) x2 + (1,2,10,7)
      tt_A() = (1,4,7,6)
      a__isList#_A(x1) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + (1,2,5,8)
      ___A(x1,x2) = ((1,0,0,0),(0,1,0,0),(1,1,0,0),(1,1,1,0)) x1 + ((1,0,0,0),(1,0,0,0),(1,1,0,0),(1,1,1,0)) x2 + (6,1,1,1)
      a__isList_A(x1) = ((0,0,0,0),(1,0,0,0),(1,1,0,0),(1,0,1,0)) x1 + (4,2,2,2)
      a__isNeList#_A(x1) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(1,1,0,0)) x1 + (0,1,0,0)
      a__U51#_A(x1,x2) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(1,1,0,0)) x1 + ((1,0,0,0),(0,1,0,0),(0,0,0,0),(0,0,1,0)) x2 + (1,0,3,1)
      a__isNeList_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(1,1,1,0)) x1 + (4,3,1,0)
      a__U41#_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(0,0,0,1)) x1 + ((1,0,0,0),(1,0,0,0),(1,1,0,0),(0,1,1,0)) x2 + (1,0,3,6)
      a__U22_A(x1) = (2,1,11,11)
      a__U42_A(x1) = ((1,0,0,0),(0,0,0,0),(1,0,0,0),(0,0,0,0)) x1 + (1,3,0,0)
      a__U52_A(x1) = ((1,0,0,0),(0,0,0,0),(0,0,0,0),(1,1,0,0)) x1 + (1,0,0,0)
      U22_A(x1) = (1,0,10,12)
      U42_A(x1) = ((0,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + (0,4,1,1)
      U52_A(x1) = ((0,0,0,0),(1,0,0,0),(0,0,0,0),(1,1,0,0)) x1 + (0,1,1,1)
      a__U11_A(x1) = (3,3,1,1)
      a__U21_A(x1,x2) = ((0,0,0,0),(1,0,0,0),(0,0,0,0),(0,0,0,0)) x1 + (3,5,10,10)
      a__U31_A(x1) = ((1,0,0,0),(0,1,0,0),(0,1,1,0),(1,0,1,1)) x1 + (1,1,0,0)
      a__U41_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,1)) x1 + x2 + (5,0,0,3)
      a__U51_A(x1,x2) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,1,1,0)) x1 + ((0,0,0,0),(0,0,0,0),(1,0,0,0),(1,1,0,0)) x2 + (5,8,9,1)
      a__isQid_A(x1) = ((1,0,0,0),(1,1,0,0),(1,1,1,0),(0,1,1,1)) x1 + (1,1,1,1)
      a_A() = (1,1,5,1)
      e_A() = (1,1,5,1)
      i_A() = (1,1,5,1)
      o_A() = (1,1,1,1)
      u_A() = (1,3,1,2)
      U11_A(x1) = (0,0,0,0)
      U21_A(x1,x2) = ((0,0,0,0),(1,0,0,0),(0,1,0,0),(0,0,0,0)) x1 + (0,6,11,11)
      U31_A(x1) = (0,0,1,1)
      U41_A(x1,x2) = x2 + (0,1,1,4)
      U51_A(x1,x2) = (0,0,0,0)
      isQid_A(x1) = (0,2,2,2)
      nil_A() = (2,0,1,1)
      isList_A(x1) = (0,3,0,3)
      isNeList_A(x1) = (3,0,0,1)

The next rules are strictly ordered:

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

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

-- Reduction pair.

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

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

and R consists of:

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

The set of usable rules consists of

  r26, r27, r28, r29, r30, r72

Take the reduction pair:

  matrix interpretations:
  
    carrier: N^4
    order: lexicographic order
    interpretations:
      a__U71#_A(x1,x2) = ((1,0,0,0),(1,1,0,0),(1,0,1,0),(1,0,1,0)) x1 + ((1,0,0,0),(0,0,0,0),(0,1,0,0),(0,0,0,0)) x2 + (0,1,3,3)
      tt_A() = (4,9,0,6)
      a__isPal#_A(x1) = ((1,0,0,0),(0,0,0,0),(0,1,0,0),(0,0,1,0)) x1 + (3,14,1,1)
      a__isNePal#_A(x1) = ((1,0,0,0),(0,1,0,0),(0,0,1,0),(0,0,1,0)) x1 + (2,0,0,0)
      ___A(x1,x2) = ((1,0,0,0),(0,0,0,0),(0,1,0,0),(1,1,1,0)) x1 + ((1,0,0,0),(0,1,0,0),(0,1,1,0),(0,1,1,1)) x2 + (0,1,1,1)
      a__isQid_A(x1) = ((1,0,0,0),(1,1,0,0),(0,1,1,0),(1,0,0,0)) x1 + (1,1,0,1)
      a_A() = (4,1,1,1)
      e_A() = (6,1,1,1)
      i_A() = (4,1,1,1)
      o_A() = (6,1,1,1)
      u_A() = (6,1,1,1)
      isQid_A(x1) = x1

The next rules are strictly ordered:

  p1, p2, p3

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