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(U11(tt())) -> mark(tt())
  active(U21(tt(),V2)) -> mark(U22(isList(V2)))
  active(U22(tt())) -> mark(tt())
  active(U31(tt())) -> mark(tt())
  active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
  active(U42(tt())) -> mark(tt())
  active(U51(tt(),V2)) -> mark(U52(isList(V2)))
  active(U52(tt())) -> mark(tt())
  active(U61(tt())) -> mark(tt())
  active(U71(tt(),P)) -> mark(U72(isPal(P)))
  active(U72(tt())) -> mark(tt())
  active(U81(tt())) -> mark(tt())
  active(isList(V)) -> mark(U11(isNeList(V)))
  active(isList(nil())) -> mark(tt())
  active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
  active(isNeList(V)) -> mark(U31(isQid(V)))
  active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
  active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
  active(isNePal(V)) -> mark(U61(isQid(V)))
  active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
  active(isPal(V)) -> mark(U81(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(U11(X)) -> active(U11(mark(X)))
  mark(tt()) -> active(tt())
  mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
  mark(U22(X)) -> active(U22(mark(X)))
  mark(isList(X)) -> active(isList(X))
  mark(U31(X)) -> active(U31(mark(X)))
  mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
  mark(U42(X)) -> active(U42(mark(X)))
  mark(isNeList(X)) -> active(isNeList(X))
  mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
  mark(U52(X)) -> active(U52(mark(X)))
  mark(U61(X)) -> active(U61(mark(X)))
  mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
  mark(U72(X)) -> active(U72(mark(X)))
  mark(isPal(X)) -> active(isPal(X))
  mark(U81(X)) -> active(U81(mark(X)))
  mark(isQid(X)) -> active(isQid(X))
  mark(isNePal(X)) -> active(isNePal(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)
  U11(mark(X)) -> U11(X)
  U11(active(X)) -> U11(X)
  U21(mark(X1),X2) -> U21(X1,X2)
  U21(X1,mark(X2)) -> U21(X1,X2)
  U21(active(X1),X2) -> U21(X1,X2)
  U21(X1,active(X2)) -> U21(X1,X2)
  U22(mark(X)) -> U22(X)
  U22(active(X)) -> U22(X)
  isList(mark(X)) -> isList(X)
  isList(active(X)) -> isList(X)
  U31(mark(X)) -> U31(X)
  U31(active(X)) -> U31(X)
  U41(mark(X1),X2) -> U41(X1,X2)
  U41(X1,mark(X2)) -> U41(X1,X2)
  U41(active(X1),X2) -> U41(X1,X2)
  U41(X1,active(X2)) -> U41(X1,X2)
  U42(mark(X)) -> U42(X)
  U42(active(X)) -> U42(X)
  isNeList(mark(X)) -> isNeList(X)
  isNeList(active(X)) -> isNeList(X)
  U51(mark(X1),X2) -> U51(X1,X2)
  U51(X1,mark(X2)) -> U51(X1,X2)
  U51(active(X1),X2) -> U51(X1,X2)
  U51(X1,active(X2)) -> U51(X1,X2)
  U52(mark(X)) -> U52(X)
  U52(active(X)) -> U52(X)
  U61(mark(X)) -> U61(X)
  U61(active(X)) -> U61(X)
  U71(mark(X1),X2) -> U71(X1,X2)
  U71(X1,mark(X2)) -> U71(X1,X2)
  U71(active(X1),X2) -> U71(X1,X2)
  U71(X1,active(X2)) -> U71(X1,X2)
  U72(mark(X)) -> U72(X)
  U72(active(X)) -> U72(X)
  isPal(mark(X)) -> isPal(X)
  isPal(active(X)) -> isPal(X)
  U81(mark(X)) -> U81(X)
  U81(active(X)) -> U81(X)
  isQid(mark(X)) -> isQid(X)
  isQid(active(X)) -> isQid(X)
  isNePal(mark(X)) -> isNePal(X)
  isNePal(active(X)) -> isNePal(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#(U11(tt())) -> mark#(tt())
p7: active#(U21(tt(),V2)) -> mark#(U22(isList(V2)))
p8: active#(U21(tt(),V2)) -> U22#(isList(V2))
p9: active#(U21(tt(),V2)) -> isList#(V2)
p10: active#(U22(tt())) -> mark#(tt())
p11: active#(U31(tt())) -> mark#(tt())
p12: active#(U41(tt(),V2)) -> mark#(U42(isNeList(V2)))
p13: active#(U41(tt(),V2)) -> U42#(isNeList(V2))
p14: active#(U41(tt(),V2)) -> isNeList#(V2)
p15: active#(U42(tt())) -> mark#(tt())
p16: active#(U51(tt(),V2)) -> mark#(U52(isList(V2)))
p17: active#(U51(tt(),V2)) -> U52#(isList(V2))
p18: active#(U51(tt(),V2)) -> isList#(V2)
p19: active#(U52(tt())) -> mark#(tt())
p20: active#(U61(tt())) -> mark#(tt())
p21: active#(U71(tt(),P)) -> mark#(U72(isPal(P)))
p22: active#(U71(tt(),P)) -> U72#(isPal(P))
p23: active#(U71(tt(),P)) -> isPal#(P)
p24: active#(U72(tt())) -> mark#(tt())
p25: active#(U81(tt())) -> mark#(tt())
p26: active#(isList(V)) -> mark#(U11(isNeList(V)))
p27: active#(isList(V)) -> U11#(isNeList(V))
p28: active#(isList(V)) -> isNeList#(V)
p29: active#(isList(nil())) -> mark#(tt())
p30: active#(isList(__(V1,V2))) -> mark#(U21(isList(V1),V2))
p31: active#(isList(__(V1,V2))) -> U21#(isList(V1),V2)
p32: active#(isList(__(V1,V2))) -> isList#(V1)
p33: active#(isNeList(V)) -> mark#(U31(isQid(V)))
p34: active#(isNeList(V)) -> U31#(isQid(V))
p35: active#(isNeList(V)) -> isQid#(V)
p36: active#(isNeList(__(V1,V2))) -> mark#(U41(isList(V1),V2))
p37: active#(isNeList(__(V1,V2))) -> U41#(isList(V1),V2)
p38: active#(isNeList(__(V1,V2))) -> isList#(V1)
p39: active#(isNeList(__(V1,V2))) -> mark#(U51(isNeList(V1),V2))
p40: active#(isNeList(__(V1,V2))) -> U51#(isNeList(V1),V2)
p41: active#(isNeList(__(V1,V2))) -> isNeList#(V1)
p42: active#(isNePal(V)) -> mark#(U61(isQid(V)))
p43: active#(isNePal(V)) -> U61#(isQid(V))
p44: active#(isNePal(V)) -> isQid#(V)
p45: active#(isNePal(__(I,__(P,I)))) -> mark#(U71(isQid(I),P))
p46: active#(isNePal(__(I,__(P,I)))) -> U71#(isQid(I),P)
p47: active#(isNePal(__(I,__(P,I)))) -> isQid#(I)
p48: active#(isPal(V)) -> mark#(U81(isNePal(V)))
p49: active#(isPal(V)) -> U81#(isNePal(V))
p50: active#(isPal(V)) -> isNePal#(V)
p51: active#(isPal(nil())) -> mark#(tt())
p52: active#(isQid(a())) -> mark#(tt())
p53: active#(isQid(e())) -> mark#(tt())
p54: active#(isQid(i())) -> mark#(tt())
p55: active#(isQid(o())) -> mark#(tt())
p56: active#(isQid(u())) -> mark#(tt())
p57: mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
p58: mark#(__(X1,X2)) -> __#(mark(X1),mark(X2))
p59: mark#(__(X1,X2)) -> mark#(X1)
p60: mark#(__(X1,X2)) -> mark#(X2)
p61: mark#(nil()) -> active#(nil())
p62: mark#(U11(X)) -> active#(U11(mark(X)))
p63: mark#(U11(X)) -> U11#(mark(X))
p64: mark#(U11(X)) -> mark#(X)
p65: mark#(tt()) -> active#(tt())
p66: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p67: mark#(U21(X1,X2)) -> U21#(mark(X1),X2)
p68: mark#(U21(X1,X2)) -> mark#(X1)
p69: mark#(U22(X)) -> active#(U22(mark(X)))
p70: mark#(U22(X)) -> U22#(mark(X))
p71: mark#(U22(X)) -> mark#(X)
p72: mark#(isList(X)) -> active#(isList(X))
p73: mark#(U31(X)) -> active#(U31(mark(X)))
p74: mark#(U31(X)) -> U31#(mark(X))
p75: mark#(U31(X)) -> mark#(X)
p76: mark#(U41(X1,X2)) -> active#(U41(mark(X1),X2))
p77: mark#(U41(X1,X2)) -> U41#(mark(X1),X2)
p78: mark#(U41(X1,X2)) -> mark#(X1)
p79: mark#(U42(X)) -> active#(U42(mark(X)))
p80: mark#(U42(X)) -> U42#(mark(X))
p81: mark#(U42(X)) -> mark#(X)
p82: mark#(isNeList(X)) -> active#(isNeList(X))
p83: mark#(U51(X1,X2)) -> active#(U51(mark(X1),X2))
p84: mark#(U51(X1,X2)) -> U51#(mark(X1),X2)
p85: mark#(U51(X1,X2)) -> mark#(X1)
p86: mark#(U52(X)) -> active#(U52(mark(X)))
p87: mark#(U52(X)) -> U52#(mark(X))
p88: mark#(U52(X)) -> mark#(X)
p89: mark#(U61(X)) -> active#(U61(mark(X)))
p90: mark#(U61(X)) -> U61#(mark(X))
p91: mark#(U61(X)) -> mark#(X)
p92: mark#(U71(X1,X2)) -> active#(U71(mark(X1),X2))
p93: mark#(U71(X1,X2)) -> U71#(mark(X1),X2)
p94: mark#(U71(X1,X2)) -> mark#(X1)
p95: mark#(U72(X)) -> active#(U72(mark(X)))
p96: mark#(U72(X)) -> U72#(mark(X))
p97: mark#(U72(X)) -> mark#(X)
p98: mark#(isPal(X)) -> active#(isPal(X))
p99: mark#(U81(X)) -> active#(U81(mark(X)))
p100: mark#(U81(X)) -> U81#(mark(X))
p101: mark#(U81(X)) -> mark#(X)
p102: mark#(isQid(X)) -> active#(isQid(X))
p103: mark#(isNePal(X)) -> active#(isNePal(X))
p104: mark#(a()) -> active#(a())
p105: mark#(e()) -> active#(e())
p106: mark#(i()) -> active#(i())
p107: mark#(o()) -> active#(o())
p108: mark#(u()) -> active#(u())
p109: __#(mark(X1),X2) -> __#(X1,X2)
p110: __#(X1,mark(X2)) -> __#(X1,X2)
p111: __#(active(X1),X2) -> __#(X1,X2)
p112: __#(X1,active(X2)) -> __#(X1,X2)
p113: U11#(mark(X)) -> U11#(X)
p114: U11#(active(X)) -> U11#(X)
p115: U21#(mark(X1),X2) -> U21#(X1,X2)
p116: U21#(X1,mark(X2)) -> U21#(X1,X2)
p117: U21#(active(X1),X2) -> U21#(X1,X2)
p118: U21#(X1,active(X2)) -> U21#(X1,X2)
p119: U22#(mark(X)) -> U22#(X)
p120: U22#(active(X)) -> U22#(X)
p121: isList#(mark(X)) -> isList#(X)
p122: isList#(active(X)) -> isList#(X)
p123: U31#(mark(X)) -> U31#(X)
p124: U31#(active(X)) -> U31#(X)
p125: U41#(mark(X1),X2) -> U41#(X1,X2)
p126: U41#(X1,mark(X2)) -> U41#(X1,X2)
p127: U41#(active(X1),X2) -> U41#(X1,X2)
p128: U41#(X1,active(X2)) -> U41#(X1,X2)
p129: U42#(mark(X)) -> U42#(X)
p130: U42#(active(X)) -> U42#(X)
p131: isNeList#(mark(X)) -> isNeList#(X)
p132: isNeList#(active(X)) -> isNeList#(X)
p133: U51#(mark(X1),X2) -> U51#(X1,X2)
p134: U51#(X1,mark(X2)) -> U51#(X1,X2)
p135: U51#(active(X1),X2) -> U51#(X1,X2)
p136: U51#(X1,active(X2)) -> U51#(X1,X2)
p137: U52#(mark(X)) -> U52#(X)
p138: U52#(active(X)) -> U52#(X)
p139: U61#(mark(X)) -> U61#(X)
p140: U61#(active(X)) -> U61#(X)
p141: U71#(mark(X1),X2) -> U71#(X1,X2)
p142: U71#(X1,mark(X2)) -> U71#(X1,X2)
p143: U71#(active(X1),X2) -> U71#(X1,X2)
p144: U71#(X1,active(X2)) -> U71#(X1,X2)
p145: U72#(mark(X)) -> U72#(X)
p146: U72#(active(X)) -> U72#(X)
p147: isPal#(mark(X)) -> isPal#(X)
p148: isPal#(active(X)) -> isPal#(X)
p149: U81#(mark(X)) -> U81#(X)
p150: U81#(active(X)) -> U81#(X)
p151: isQid#(mark(X)) -> isQid#(X)
p152: isQid#(active(X)) -> isQid#(X)
p153: isNePal#(mark(X)) -> isNePal#(X)
p154: 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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The estimated dependency graph contains the following SCCs:

  {p1, p4, p5, p7, p12, p16, p21, p26, p30, p33, p36, p39, p42, p45, p48, p57, p59, p60, p62, p64, p66, p68, p69, p71, p72, p73, p75, p76, p78, p79, p81, p82, p83, p85, p86, p88, p89, p91, p92, p94, p95, p97, p98, p99, p101, p102, p103}
  {p109, p110, p111, p112}
  {p119, p120}
  {p121, p122}
  {p129, p130}
  {p131, p132}
  {p137, p138}
  {p145, p146}
  {p147, p148}
  {p113, p114}
  {p115, p116, p117, p118}
  {p123, p124}
  {p151, p152}
  {p125, p126, p127, p128}
  {p133, p134, p135, p136}
  {p139, p140}
  {p141, p142, p143, p144}
  {p149, p150}
  {p153, p154}


-- Reduction pair.

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

p1: active#(__(__(X,Y),Z)) -> mark#(__(X,__(Y,Z)))
p2: mark#(isNePal(X)) -> active#(isNePal(X))
p3: active#(isPal(V)) -> mark#(U81(isNePal(V)))
p4: mark#(isQid(X)) -> active#(isQid(X))
p5: active#(isNePal(__(I,__(P,I)))) -> mark#(U71(isQid(I),P))
p6: mark#(U81(X)) -> mark#(X)
p7: mark#(U81(X)) -> active#(U81(mark(X)))
p8: active#(isNePal(V)) -> mark#(U61(isQid(V)))
p9: mark#(isPal(X)) -> active#(isPal(X))
p10: active#(isNeList(__(V1,V2))) -> mark#(U51(isNeList(V1),V2))
p11: mark#(U72(X)) -> mark#(X)
p12: mark#(U72(X)) -> active#(U72(mark(X)))
p13: active#(isNeList(__(V1,V2))) -> mark#(U41(isList(V1),V2))
p14: mark#(U71(X1,X2)) -> mark#(X1)
p15: mark#(U71(X1,X2)) -> active#(U71(mark(X1),X2))
p16: active#(isNeList(V)) -> mark#(U31(isQid(V)))
p17: mark#(U61(X)) -> mark#(X)
p18: mark#(U61(X)) -> active#(U61(mark(X)))
p19: active#(isList(__(V1,V2))) -> mark#(U21(isList(V1),V2))
p20: mark#(U52(X)) -> mark#(X)
p21: mark#(U52(X)) -> active#(U52(mark(X)))
p22: active#(isList(V)) -> mark#(U11(isNeList(V)))
p23: mark#(U51(X1,X2)) -> mark#(X1)
p24: mark#(U51(X1,X2)) -> active#(U51(mark(X1),X2))
p25: active#(U71(tt(),P)) -> mark#(U72(isPal(P)))
p26: mark#(isNeList(X)) -> active#(isNeList(X))
p27: active#(U51(tt(),V2)) -> mark#(U52(isList(V2)))
p28: mark#(U42(X)) -> mark#(X)
p29: mark#(U42(X)) -> active#(U42(mark(X)))
p30: active#(U41(tt(),V2)) -> mark#(U42(isNeList(V2)))
p31: mark#(U41(X1,X2)) -> mark#(X1)
p32: mark#(U41(X1,X2)) -> active#(U41(mark(X1),X2))
p33: active#(U21(tt(),V2)) -> mark#(U22(isList(V2)))
p34: mark#(U31(X)) -> mark#(X)
p35: mark#(U31(X)) -> active#(U31(mark(X)))
p36: active#(__(nil(),X)) -> mark#(X)
p37: mark#(isList(X)) -> active#(isList(X))
p38: active#(__(X,nil())) -> mark#(X)
p39: mark#(U22(X)) -> mark#(X)
p40: mark#(U22(X)) -> active#(U22(mark(X)))
p41: mark#(U21(X1,X2)) -> mark#(X1)
p42: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p43: mark#(U11(X)) -> mark#(X)
p44: mark#(U11(X)) -> active#(U11(mark(X)))
p45: mark#(__(X1,X2)) -> mark#(X2)
p46: mark#(__(X1,X2)) -> mark#(X1)
p47: mark#(__(X1,X2)) -> active#(__(mark(X1),mark(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(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, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        mark# > U11 > U52 > __ > U21 > active > U41 > U71 > U51 > U72 > isQid > U81 > active# > isList > U61 > U31 > isPal > u > o > mark > isNeList > i > e > a > nil > U22 > U42 > tt > isNePal
      
      argument filter:
    
        pi(active#) = 1
        pi(__) = [1, 2]
        pi(mark#) = 1
        pi(isNePal) = 1
        pi(isPal) = 1
        pi(U81) = 1
        pi(isQid) = 1
        pi(U71) = [1, 2]
        pi(mark) = 1
        pi(U61) = 1
        pi(isNeList) = 1
        pi(U51) = [1, 2]
        pi(U72) = [1]
        pi(U41) = [1, 2]
        pi(isList) = [1]
        pi(U31) = 1
        pi(U21) = [1, 2]
        pi(U52) = 1
        pi(U11) = 1
        pi(tt) = []
        pi(U42) = [1]
        pi(U22) = [1]
        pi(nil) = []
        pi(active) = 1
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U51 > U81 > tt > u > o > i > a > nil > U42 > U41 > isNeList > U11 > U31 > isPal > e > active > mark > U52 > U22 > U21 > isList > U61 > U71 > active# > mark# > U72 > isQid > isNePal > __
      
      argument filter:
    
        pi(active#) = 1
        pi(__) = 2
        pi(mark#) = 1
        pi(isNePal) = [1]
        pi(isPal) = [1]
        pi(U81) = 1
        pi(isQid) = 1
        pi(U71) = 1
        pi(mark) = 1
        pi(U61) = 1
        pi(isNeList) = 1
        pi(U51) = 1
        pi(U72) = [1]
        pi(U41) = 2
        pi(isList) = []
        pi(U31) = 1
        pi(U21) = 2
        pi(U52) = [1]
        pi(U11) = 1
        pi(tt) = []
        pi(U42) = []
        pi(U22) = [1]
        pi(nil) = []
        pi(active) = 1
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
    

The next rules are strictly ordered:

  p1, p3, p5, p8, p10, p11, p13, p14, p19, p20, p22, p23, p25, p27, p28, p30, p31, p33, p36, p38, p39, p41, p45, p46

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(isNePal(X)) -> active#(isNePal(X))
p2: mark#(isQid(X)) -> active#(isQid(X))
p3: mark#(U81(X)) -> mark#(X)
p4: mark#(U81(X)) -> active#(U81(mark(X)))
p5: mark#(isPal(X)) -> active#(isPal(X))
p6: mark#(U72(X)) -> active#(U72(mark(X)))
p7: mark#(U71(X1,X2)) -> active#(U71(mark(X1),X2))
p8: active#(isNeList(V)) -> mark#(U31(isQid(V)))
p9: mark#(U61(X)) -> mark#(X)
p10: mark#(U61(X)) -> active#(U61(mark(X)))
p11: mark#(U52(X)) -> active#(U52(mark(X)))
p12: mark#(U51(X1,X2)) -> active#(U51(mark(X1),X2))
p13: mark#(isNeList(X)) -> active#(isNeList(X))
p14: mark#(U42(X)) -> active#(U42(mark(X)))
p15: mark#(U41(X1,X2)) -> active#(U41(mark(X1),X2))
p16: mark#(U31(X)) -> mark#(X)
p17: mark#(U31(X)) -> active#(U31(mark(X)))
p18: mark#(isList(X)) -> active#(isList(X))
p19: mark#(U22(X)) -> active#(U22(mark(X)))
p20: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p21: mark#(U11(X)) -> mark#(X)
p22: mark#(U11(X)) -> active#(U11(mark(X)))
p23: mark#(__(X1,X2)) -> active#(__(mark(X1),mark(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(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, p23}


-- Reduction pair.

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

p1: mark#(isNePal(X)) -> active#(isNePal(X))
p2: active#(isNeList(V)) -> mark#(U31(isQid(V)))
p3: mark#(__(X1,X2)) -> active#(__(mark(X1),mark(X2)))
p4: mark#(U11(X)) -> active#(U11(mark(X)))
p5: mark#(U11(X)) -> mark#(X)
p6: mark#(U21(X1,X2)) -> active#(U21(mark(X1),X2))
p7: mark#(U22(X)) -> active#(U22(mark(X)))
p8: mark#(isList(X)) -> active#(isList(X))
p9: mark#(U31(X)) -> active#(U31(mark(X)))
p10: mark#(U31(X)) -> mark#(X)
p11: mark#(U41(X1,X2)) -> active#(U41(mark(X1),X2))
p12: mark#(U42(X)) -> active#(U42(mark(X)))
p13: mark#(isNeList(X)) -> active#(isNeList(X))
p14: mark#(U51(X1,X2)) -> active#(U51(mark(X1),X2))
p15: mark#(U52(X)) -> active#(U52(mark(X)))
p16: mark#(U61(X)) -> active#(U61(mark(X)))
p17: mark#(U61(X)) -> mark#(X)
p18: mark#(U71(X1,X2)) -> active#(U71(mark(X1),X2))
p19: mark#(U72(X)) -> active#(U72(mark(X)))
p20: mark#(isPal(X)) -> active#(isPal(X))
p21: mark#(U81(X)) -> active#(U81(mark(X)))
p22: mark#(U81(X)) -> mark#(X)
p23: mark#(isQid(X)) -> active#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(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, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        __ > u > o > U81 > U21 > U71 > isPal > isList > isNeList > isNePal > isQid > U51 > U52 > U41 > U42 > U22 > mark > tt > active > i > e > a > nil > U72 > active# > mark# > U61 > U11 > U31
      
      argument filter:
    
        pi(mark#) = [1]
        pi(isNePal) = [1]
        pi(active#) = 1
        pi(isNeList) = [1]
        pi(U31) = [1]
        pi(isQid) = [1]
        pi(__) = [1, 2]
        pi(mark) = 1
        pi(U11) = 1
        pi(U21) = [1, 2]
        pi(U22) = []
        pi(isList) = [1]
        pi(U41) = [1]
        pi(U42) = []
        pi(U51) = [2]
        pi(U52) = []
        pi(U61) = [1]
        pi(U71) = [1, 2]
        pi(U72) = 1
        pi(isPal) = [1]
        pi(U81) = 1
        pi(active) = 1
        pi(nil) = []
        pi(tt) = []
        pi(a) = []
        pi(e) = []
        pi(i) = []
        pi(o) = []
        pi(u) = []
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        mark > o > U42 > active > e > a > nil > U81 > isPal > U72 > U71 > U61 > u > U52 > isNeList > tt > i > active# > isList > U51 > U41 > U22 > U21 > U11 > isQid > __ > U31 > isNePal > mark#
      
      argument filter:
    
        pi(mark#) = 1
        pi(isNePal) = [1]
        pi(active#) = 1
        pi(isNeList) = 1
        pi(U31) = 1
        pi(isQid) = [1]
        pi(__) = []
        pi(mark) = 1
        pi(U11) = 1
        pi(U21) = 1
        pi(U22) = []
        pi(isList) = [1]
        pi(U41) = 1
        pi(U42) = []
        pi(U51) = [2]
        pi(U52) = []
        pi(U61) = 1
        pi(U71) = 1
        pi(U72) = []
        pi(isPal) = [1]
        pi(U81) = [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, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23

We remove them from the problem.

-- SCC decomposition.

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

p1: mark#(U11(X)) -> 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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(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#(U11(X)) -> 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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U11 > mark#
      
      argument filter:
    
        pi(mark#) = [1]
        pi(U11) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U11 > mark#
      
      argument filter:
    
        pi(mark#) = [1]
        pi(U11) = [1]
    

The next rules are strictly ordered:

  p1
  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, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        __# > active > mark
      
      argument filter:
    
        pi(__#) = 2
        pi(mark) = [1]
        pi(active) = [1]
    
    2. 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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        __# > active > mark
      
      argument filter:
    
        pi(__#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. 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: U22#(mark(X)) -> U22#(X)
p2: U22#(active(X)) -> U22#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U22# > active > mark
      
      argument filter:
    
        pi(U22#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U22# > active > mark
      
      argument filter:
    
        pi(U22#) = 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, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        isList# > active > mark
      
      argument filter:
    
        pi(isList#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. 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, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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: U42#(mark(X)) -> U42#(X)
p2: U42#(active(X)) -> U42#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U42# > active > mark
      
      argument filter:
    
        pi(U42#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U42# > active > mark
      
      argument filter:
    
        pi(U42#) = 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, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        isNeList# > active > mark
      
      argument filter:
    
        pi(isNeList#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. 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, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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: U52#(mark(X)) -> U52#(X)
p2: U52#(active(X)) -> U52#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U52# > active > mark
      
      argument filter:
    
        pi(U52#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U52# > active > mark
      
      argument filter:
    
        pi(U52#) = 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, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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: U72#(mark(X)) -> U72#(X)
p2: U72#(active(X)) -> U72#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U72# > active > mark
      
      argument filter:
    
        pi(U72#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U72# > active > mark
      
      argument filter:
    
        pi(U72#) = 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, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        isPal# > active > mark
      
      argument filter:
    
        pi(isPal#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. 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, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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: U11#(mark(X)) -> U11#(X)
p2: U11#(active(X)) -> U11#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U11# > active > mark
      
      argument filter:
    
        pi(U11#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U11# > active > mark
      
      argument filter:
    
        pi(U11#) = 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, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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: U21#(mark(X1),X2) -> U21#(X1,X2)
p2: U21#(X1,active(X2)) -> U21#(X1,X2)
p3: U21#(active(X1),X2) -> U21#(X1,X2)
p4: U21#(X1,mark(X2)) -> U21#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U21# > active > mark
      
      argument filter:
    
        pi(U21#) = 2
        pi(mark) = [1]
        pi(active) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U21# > active > mark
      
      argument filter:
    
        pi(U21#) = 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: U21#(mark(X1),X2) -> U21#(X1,X2)
p2: U21#(active(X1),X2) -> U21#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(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: U21#(mark(X1),X2) -> U21#(X1,X2)
p2: U21#(active(X1),X2) -> U21#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U21# > active > mark
      
      argument filter:
    
        pi(U21#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U21# > active > mark
      
      argument filter:
    
        pi(U21#) = 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: U31#(mark(X)) -> U31#(X)
p2: U31#(active(X)) -> U31#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U31# > active > mark
      
      argument filter:
    
        pi(U31#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U31# > active > mark
      
      argument filter:
    
        pi(U31#) = 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, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        isQid# > active > mark
      
      argument filter:
    
        pi(isQid#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. 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, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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: U41#(mark(X1),X2) -> U41#(X1,X2)
p2: U41#(X1,active(X2)) -> U41#(X1,X2)
p3: U41#(active(X1),X2) -> U41#(X1,X2)
p4: U41#(X1,mark(X2)) -> U41#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U41# > active > mark
      
      argument filter:
    
        pi(U41#) = 2
        pi(mark) = [1]
        pi(active) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U41# > active > mark
      
      argument filter:
    
        pi(U41#) = 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: U41#(mark(X1),X2) -> U41#(X1,X2)
p2: U41#(active(X1),X2) -> U41#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(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: U41#(mark(X1),X2) -> U41#(X1,X2)
p2: U41#(active(X1),X2) -> U41#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U41# > active > mark
      
      argument filter:
    
        pi(U41#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U41# > active > mark
      
      argument filter:
    
        pi(U41#) = 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: U51#(mark(X1),X2) -> U51#(X1,X2)
p2: U51#(X1,active(X2)) -> U51#(X1,X2)
p3: U51#(active(X1),X2) -> U51#(X1,X2)
p4: U51#(X1,mark(X2)) -> U51#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U51# > active > mark
      
      argument filter:
    
        pi(U51#) = 2
        pi(mark) = [1]
        pi(active) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U51# > active > mark
      
      argument filter:
    
        pi(U51#) = 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: U51#(mark(X1),X2) -> U51#(X1,X2)
p2: U51#(active(X1),X2) -> U51#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(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: U51#(mark(X1),X2) -> U51#(X1,X2)
p2: U51#(active(X1),X2) -> U51#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U51# > active > mark
      
      argument filter:
    
        pi(U51#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U51# > active > mark
      
      argument filter:
    
        pi(U51#) = 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: U61#(mark(X)) -> U61#(X)
p2: U61#(active(X)) -> U61#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U61# > active > mark
      
      argument filter:
    
        pi(U61#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U61# > active > mark
      
      argument filter:
    
        pi(U61#) = 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, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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: U71#(mark(X1),X2) -> U71#(X1,X2)
p2: U71#(X1,active(X2)) -> U71#(X1,X2)
p3: U71#(active(X1),X2) -> U71#(X1,X2)
p4: U71#(X1,mark(X2)) -> U71#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U71# > active > mark
      
      argument filter:
    
        pi(U71#) = 2
        pi(mark) = [1]
        pi(active) = [1]
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U71# > active > mark
      
      argument filter:
    
        pi(U71#) = 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: U71#(mark(X1),X2) -> U71#(X1,X2)
p2: U71#(active(X1),X2) -> U71#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(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: U71#(mark(X1),X2) -> U71#(X1,X2)
p2: U71#(active(X1),X2) -> U71#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U71# > active > mark
      
      argument filter:
    
        pi(U71#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U71# > active > mark
      
      argument filter:
    
        pi(U71#) = 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: U81#(mark(X)) -> U81#(X)
p2: U81#(active(X)) -> U81#(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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        U81# > active > mark
      
      argument filter:
    
        pi(U81#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        U81# > active > mark
      
      argument filter:
    
        pi(U81#) = 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, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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(U11(tt())) -> mark(tt())
r5: active(U21(tt(),V2)) -> mark(U22(isList(V2)))
r6: active(U22(tt())) -> mark(tt())
r7: active(U31(tt())) -> mark(tt())
r8: active(U41(tt(),V2)) -> mark(U42(isNeList(V2)))
r9: active(U42(tt())) -> mark(tt())
r10: active(U51(tt(),V2)) -> mark(U52(isList(V2)))
r11: active(U52(tt())) -> mark(tt())
r12: active(U61(tt())) -> mark(tt())
r13: active(U71(tt(),P)) -> mark(U72(isPal(P)))
r14: active(U72(tt())) -> mark(tt())
r15: active(U81(tt())) -> mark(tt())
r16: active(isList(V)) -> mark(U11(isNeList(V)))
r17: active(isList(nil())) -> mark(tt())
r18: active(isList(__(V1,V2))) -> mark(U21(isList(V1),V2))
r19: active(isNeList(V)) -> mark(U31(isQid(V)))
r20: active(isNeList(__(V1,V2))) -> mark(U41(isList(V1),V2))
r21: active(isNeList(__(V1,V2))) -> mark(U51(isNeList(V1),V2))
r22: active(isNePal(V)) -> mark(U61(isQid(V)))
r23: active(isNePal(__(I,__(P,I)))) -> mark(U71(isQid(I),P))
r24: active(isPal(V)) -> mark(U81(isNePal(V)))
r25: active(isPal(nil())) -> mark(tt())
r26: active(isQid(a())) -> mark(tt())
r27: active(isQid(e())) -> mark(tt())
r28: active(isQid(i())) -> mark(tt())
r29: active(isQid(o())) -> mark(tt())
r30: active(isQid(u())) -> mark(tt())
r31: mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
r32: mark(nil()) -> active(nil())
r33: mark(U11(X)) -> active(U11(mark(X)))
r34: mark(tt()) -> active(tt())
r35: mark(U21(X1,X2)) -> active(U21(mark(X1),X2))
r36: mark(U22(X)) -> active(U22(mark(X)))
r37: mark(isList(X)) -> active(isList(X))
r38: mark(U31(X)) -> active(U31(mark(X)))
r39: mark(U41(X1,X2)) -> active(U41(mark(X1),X2))
r40: mark(U42(X)) -> active(U42(mark(X)))
r41: mark(isNeList(X)) -> active(isNeList(X))
r42: mark(U51(X1,X2)) -> active(U51(mark(X1),X2))
r43: mark(U52(X)) -> active(U52(mark(X)))
r44: mark(U61(X)) -> active(U61(mark(X)))
r45: mark(U71(X1,X2)) -> active(U71(mark(X1),X2))
r46: mark(U72(X)) -> active(U72(mark(X)))
r47: mark(isPal(X)) -> active(isPal(X))
r48: mark(U81(X)) -> active(U81(mark(X)))
r49: mark(isQid(X)) -> active(isQid(X))
r50: mark(isNePal(X)) -> active(isNePal(X))
r51: mark(a()) -> active(a())
r52: mark(e()) -> active(e())
r53: mark(i()) -> active(i())
r54: mark(o()) -> active(o())
r55: mark(u()) -> active(u())
r56: __(mark(X1),X2) -> __(X1,X2)
r57: __(X1,mark(X2)) -> __(X1,X2)
r58: __(active(X1),X2) -> __(X1,X2)
r59: __(X1,active(X2)) -> __(X1,X2)
r60: U11(mark(X)) -> U11(X)
r61: U11(active(X)) -> U11(X)
r62: U21(mark(X1),X2) -> U21(X1,X2)
r63: U21(X1,mark(X2)) -> U21(X1,X2)
r64: U21(active(X1),X2) -> U21(X1,X2)
r65: U21(X1,active(X2)) -> U21(X1,X2)
r66: U22(mark(X)) -> U22(X)
r67: U22(active(X)) -> U22(X)
r68: isList(mark(X)) -> isList(X)
r69: isList(active(X)) -> isList(X)
r70: U31(mark(X)) -> U31(X)
r71: U31(active(X)) -> U31(X)
r72: U41(mark(X1),X2) -> U41(X1,X2)
r73: U41(X1,mark(X2)) -> U41(X1,X2)
r74: U41(active(X1),X2) -> U41(X1,X2)
r75: U41(X1,active(X2)) -> U41(X1,X2)
r76: U42(mark(X)) -> U42(X)
r77: U42(active(X)) -> U42(X)
r78: isNeList(mark(X)) -> isNeList(X)
r79: isNeList(active(X)) -> isNeList(X)
r80: U51(mark(X1),X2) -> U51(X1,X2)
r81: U51(X1,mark(X2)) -> U51(X1,X2)
r82: U51(active(X1),X2) -> U51(X1,X2)
r83: U51(X1,active(X2)) -> U51(X1,X2)
r84: U52(mark(X)) -> U52(X)
r85: U52(active(X)) -> U52(X)
r86: U61(mark(X)) -> U61(X)
r87: U61(active(X)) -> U61(X)
r88: U71(mark(X1),X2) -> U71(X1,X2)
r89: U71(X1,mark(X2)) -> U71(X1,X2)
r90: U71(active(X1),X2) -> U71(X1,X2)
r91: U71(X1,active(X2)) -> U71(X1,X2)
r92: U72(mark(X)) -> U72(X)
r93: U72(active(X)) -> U72(X)
r94: isPal(mark(X)) -> isPal(X)
r95: isPal(active(X)) -> isPal(X)
r96: U81(mark(X)) -> U81(X)
r97: U81(active(X)) -> U81(X)
r98: isQid(mark(X)) -> isQid(X)
r99: isQid(active(X)) -> isQid(X)
r100: isNePal(mark(X)) -> isNePal(X)
r101: isNePal(active(X)) -> isNePal(X)

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. lexicographic path order with precedence:
    
      precedence:
      
        isNePal# > active > mark
      
      argument filter:
    
        pi(isNePal#) = 1
        pi(mark) = 1
        pi(active) = 1
    
    2. 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, r52, r53, r54, r55, r56, r57, r58, r59, r60, r61, r62, r63, r64, r65, r66, r67, r68, r69, r70, r71, r72, r73, r74, r75, r76, r77, r78, r79, r80, r81, r82, r83, r84, r85, r86, r87, r88, r89, r90, r91, r92, r93, r94, r95, r96, r97, r98, r99, r100, r101

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