YES

We show the termination of the TRS R:

  __(__(X,Y),Z) -> __(X,__(Y,Z))
  __(X,nil()) -> X
  __(nil(),X) -> X
  and(tt(),X) -> activate(X)
  isList(V) -> isNeList(activate(V))
  isList(n__nil()) -> tt()
  isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
  isNeList(V) -> isQid(activate(V))
  isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
  isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
  isNePal(V) -> isQid(activate(V))
  isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
  isPal(V) -> isNePal(activate(V))
  isPal(n__nil()) -> tt()
  isQid(n__a()) -> tt()
  isQid(n__e()) -> tt()
  isQid(n__i()) -> tt()
  isQid(n__o()) -> tt()
  isQid(n__u()) -> tt()
  nil() -> n__nil()
  __(X1,X2) -> n____(X1,X2)
  isList(X) -> n__isList(X)
  isNeList(X) -> n__isNeList(X)
  isPal(X) -> n__isPal(X)
  a() -> n__a()
  e() -> n__e()
  i() -> n__i()
  o() -> n__o()
  u() -> n__u()
  activate(n__nil()) -> nil()
  activate(n____(X1,X2)) -> __(X1,X2)
  activate(n__isList(X)) -> isList(X)
  activate(n__isNeList(X)) -> isNeList(X)
  activate(n__isPal(X)) -> isPal(X)
  activate(n__a()) -> a()
  activate(n__e()) -> e()
  activate(n__i()) -> i()
  activate(n__o()) -> o()
  activate(n__u()) -> u()
  activate(X) -> X

-- SCC decomposition.

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

p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z))
p2: __#(__(X,Y),Z) -> __#(Y,Z)
p3: and#(tt(),X) -> activate#(X)
p4: isList#(V) -> isNeList#(activate(V))
p5: isList#(V) -> activate#(V)
p6: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p7: isList#(n____(V1,V2)) -> isList#(activate(V1))
p8: isList#(n____(V1,V2)) -> activate#(V1)
p9: isList#(n____(V1,V2)) -> activate#(V2)
p10: isNeList#(V) -> isQid#(activate(V))
p11: isNeList#(V) -> activate#(V)
p12: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p13: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p14: isNeList#(n____(V1,V2)) -> activate#(V1)
p15: isNeList#(n____(V1,V2)) -> activate#(V2)
p16: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2)))
p17: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p18: isNeList#(n____(V1,V2)) -> activate#(V1)
p19: isNeList#(n____(V1,V2)) -> activate#(V2)
p20: isNePal#(V) -> isQid#(activate(V))
p21: isNePal#(V) -> activate#(V)
p22: isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P)))
p23: isNePal#(n____(I,__(P,I))) -> isQid#(activate(I))
p24: isNePal#(n____(I,__(P,I))) -> activate#(I)
p25: isNePal#(n____(I,__(P,I))) -> activate#(P)
p26: isPal#(V) -> isNePal#(activate(V))
p27: isPal#(V) -> activate#(V)
p28: activate#(n__nil()) -> nil#()
p29: activate#(n____(X1,X2)) -> __#(X1,X2)
p30: activate#(n__isList(X)) -> isList#(X)
p31: activate#(n__isNeList(X)) -> isNeList#(X)
p32: activate#(n__isPal(X)) -> isPal#(X)
p33: activate#(n__a()) -> a#()
p34: activate#(n__e()) -> e#()
p35: activate#(n__i()) -> i#()
p36: activate#(n__o()) -> o#()
p37: activate#(n__u()) -> u#()

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p3, p4, p5, p6, p7, p8, p9, p11, p12, p13, p14, p15, p16, p17, p18, p19, p21, p22, p24, p25, p26, p27, p30, p31, p32}
  {p1, p2}


-- Reduction pair.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isPal(X)) -> isPal#(X)
p3: isPal#(V) -> isNePal#(activate(V))
p4: isNePal#(n____(I,__(P,I))) -> activate#(P)
p5: activate#(n__isNeList(X)) -> isNeList#(X)
p6: isNeList#(n____(V1,V2)) -> activate#(V2)
p7: activate#(n__isList(X)) -> isList#(X)
p8: isList#(n____(V1,V2)) -> activate#(V2)
p9: isList#(n____(V1,V2)) -> activate#(V1)
p10: isList#(n____(V1,V2)) -> isList#(activate(V1))
p11: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p12: and#(tt(),X) -> activate#(X)
p13: isList#(V) -> activate#(V)
p14: isList#(V) -> isNeList#(activate(V))
p15: isNeList#(n____(V1,V2)) -> activate#(V1)
p16: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p17: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2)))
p18: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p19: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p20: isNeList#(V) -> activate#(V)
p21: isNePal#(n____(I,__(P,I))) -> activate#(I)
p22: isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P)))
p23: isNePal#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isPal#_A(x1) = ((0,1),(0,1)) x1 + (8,8)
          activate#_A(x1) = ((0,1),(0,1)) x1
          n__isPal_A(x1) = ((0,0),(0,1)) x1 + (5,39)
          isNePal#_A(x1) = ((0,1),(0,1)) x1 + (0,1)
          activate_A(x1) = x1 + (29,7)
          n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (31,26)
          ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (53,27)
          n__isNeList_A(x1) = ((0,0),(0,1)) x1 + (3,13)
          isNeList#_A(x1) = ((0,1),(0,1)) x1 + (4,0)
          n__isList_A(x1) = ((0,0),(0,1)) x1 + (3,13)
          isList#_A(x1) = ((0,1),(0,1)) x1 + (12,13)
          and#_A(x1,x2) = ((1,1),(1,1)) x2 + (1,3)
          isList_A(x1) = ((0,0),(0,1)) x1 + (32,20)
          tt_A() = (30,2)
          isNeList_A(x1) = ((0,0),(0,1)) x1 + (32,13)
          isQid_A(x1) = (31,6)
          isNePal_A(x1) = ((0,0),(0,1)) x1 + (34,6)
          and_A(x1,x2) = x2 + (29,7)
          nil_A() = (2,2)
          isPal_A(x1) = ((0,0),(0,1)) x1 + (34,39)
          n__nil_A() = (1,1)
          a_A() = (32,3)
          n__a_A() = (31,2)
          e_A() = (32,3)
          n__e_A() = (31,2)
          i_A() = (32,3)
          n__i_A() = (31,2)
          o_A() = (31,2)
          n__o_A() = (31,2)
          u_A() = (32,3)
          n__u_A() = (31,2)
  
    precedence:
    
      n__i > isPal# = activate# = isNePal# = isNeList# = n__isList = isList# = and# > activate = isList = isNeList = isNePal = and = nil = isPal = n__nil = a > n__isNeList > __ > n____ > n__isPal > tt = n__a = e = n__e = i = o = n__o > isQid = u = n__u
    
    partial status:
  
      pi(isPal#) = []
      pi(activate#) = []
      pi(n__isPal) = []
      pi(isNePal#) = []
      pi(activate) = []
      pi(n____) = [1, 2]
      pi(__) = [1, 2]
      pi(n__isNeList) = []
      pi(isNeList#) = []
      pi(n__isList) = []
      pi(isList#) = []
      pi(and#) = []
      pi(isList) = []
      pi(tt) = []
      pi(isNeList) = []
      pi(isQid) = []
      pi(isNePal) = []
      pi(and) = []
      pi(nil) = []
      pi(isPal) = []
      pi(n__nil) = []
      pi(a) = []
      pi(n__a) = []
      pi(e) = []
      pi(n__e) = []
      pi(i) = []
      pi(n__i) = []
      pi(o) = []
      pi(n__o) = []
      pi(u) = []
      pi(n__u) = []

The next rules are strictly ordered:

  p10

We remove them from the problem.

-- SCC decomposition.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isPal(X)) -> isPal#(X)
p3: isPal#(V) -> isNePal#(activate(V))
p4: isNePal#(n____(I,__(P,I))) -> activate#(P)
p5: activate#(n__isNeList(X)) -> isNeList#(X)
p6: isNeList#(n____(V1,V2)) -> activate#(V2)
p7: activate#(n__isList(X)) -> isList#(X)
p8: isList#(n____(V1,V2)) -> activate#(V2)
p9: isList#(n____(V1,V2)) -> activate#(V1)
p10: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p11: and#(tt(),X) -> activate#(X)
p12: isList#(V) -> activate#(V)
p13: isList#(V) -> isNeList#(activate(V))
p14: isNeList#(n____(V1,V2)) -> activate#(V1)
p15: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p16: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2)))
p17: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p18: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p19: isNeList#(V) -> activate#(V)
p20: isNePal#(n____(I,__(P,I))) -> activate#(I)
p21: isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P)))
p22: isNePal#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isList(X)) -> isList#(X)
p3: isList#(V) -> isNeList#(activate(V))
p4: isNeList#(V) -> activate#(V)
p5: activate#(n__isNeList(X)) -> isNeList#(X)
p6: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p7: and#(tt(),X) -> activate#(X)
p8: activate#(n__isPal(X)) -> isPal#(X)
p9: isPal#(V) -> isNePal#(activate(V))
p10: isNePal#(V) -> activate#(V)
p11: isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P)))
p12: isNePal#(n____(I,__(P,I))) -> activate#(I)
p13: isNePal#(n____(I,__(P,I))) -> activate#(P)
p14: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p15: isList#(V) -> activate#(V)
p16: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p17: isList#(n____(V1,V2)) -> activate#(V1)
p18: isList#(n____(V1,V2)) -> activate#(V2)
p19: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2)))
p20: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p21: isNeList#(n____(V1,V2)) -> activate#(V1)
p22: isNeList#(n____(V1,V2)) -> activate#(V2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isPal#_A(x1) = ((1,0),(1,1)) x1 + (84,8)
          activate#_A(x1) = ((1,0),(1,0)) x1 + (46,0)
          n__isList_A(x1) = ((1,1),(0,0)) x1 + (12,1)
          isList#_A(x1) = ((1,1),(1,1)) x1 + (57,8)
          isNeList#_A(x1) = ((1,1),(1,1)) x1 + (47,0)
          activate_A(x1) = x1 + (5,3)
          n__isNeList_A(x1) = ((1,1),(0,0)) x1 + (3,1)
          n_____A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (22,7)
          and#_A(x1,x2) = ((1,0),(1,0)) x2 + (47,0)
          isList_A(x1) = ((1,1),(0,0)) x1 + (13,4)
          tt_A() = (0,2)
          n__isPal_A(x1) = ((1,1),(0,0)) x1 + (38,61)
          isNePal#_A(x1) = ((1,0),(1,1)) x1 + (49,0)
          ___A(x1,x2) = ((1,1),(0,1)) x1 + x2 + (23,8)
          isQid_A(x1) = (0,4)
          isNeList_A(x1) = ((1,1),(0,0)) x1 + (4,4)
          isNePal_A(x1) = ((1,1),(0,0)) x1 + (1,64)
          and_A(x1,x2) = x2 + (12,3)
          nil_A() = (2,3)
          isPal_A(x1) = ((1,1),(0,0)) x1 + (39,64)
          n__nil_A() = (1,2)
          a_A() = (2,3)
          n__a_A() = (1,2)
          e_A() = (2,3)
          n__e_A() = (1,2)
          i_A() = (2,3)
          n__i_A() = (1,2)
          o_A() = (2,2)
          n__o_A() = (1,1)
          u_A() = (2,3)
          n__u_A() = (1,2)
  
    precedence:
    
      isNePal# > isPal# = activate# = n__isList = isList# = isNeList# = and# = __ = isNePal = nil = n__nil > isList > isNeList > activate = and > n__isNeList > n__isPal = isPal > n__e > n____ = tt = isQid = a = e = n__i = o = n__o = u = n__u > i > n__a
    
    partial status:
  
      pi(isPal#) = []
      pi(activate#) = []
      pi(n__isList) = []
      pi(isList#) = []
      pi(isNeList#) = []
      pi(activate) = [1]
      pi(n__isNeList) = []
      pi(n____) = []
      pi(and#) = []
      pi(isList) = []
      pi(tt) = []
      pi(n__isPal) = []
      pi(isNePal#) = [1]
      pi(__) = [1, 2]
      pi(isQid) = []
      pi(isNeList) = []
      pi(isNePal) = []
      pi(and) = [2]
      pi(nil) = []
      pi(isPal) = []
      pi(n__nil) = []
      pi(a) = []
      pi(n__a) = []
      pi(e) = []
      pi(n__e) = []
      pi(i) = []
      pi(n__i) = []
      pi(o) = []
      pi(n__o) = []
      pi(u) = []
      pi(n__u) = []

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

p1: isPal#(V) -> activate#(V)
p2: isList#(V) -> isNeList#(activate(V))
p3: isNeList#(V) -> activate#(V)
p4: activate#(n__isNeList(X)) -> isNeList#(X)
p5: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p6: and#(tt(),X) -> activate#(X)
p7: activate#(n__isPal(X)) -> isPal#(X)
p8: isPal#(V) -> isNePal#(activate(V))
p9: isNePal#(V) -> activate#(V)
p10: isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P)))
p11: isNePal#(n____(I,__(P,I))) -> activate#(I)
p12: isNePal#(n____(I,__(P,I))) -> activate#(P)
p13: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p14: isList#(V) -> activate#(V)
p15: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p16: isList#(n____(V1,V2)) -> activate#(V1)
p17: isList#(n____(V1,V2)) -> activate#(V2)
p18: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2)))
p19: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p20: isNeList#(n____(V1,V2)) -> activate#(V1)
p21: isNeList#(n____(V1,V2)) -> activate#(V2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> 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}


-- Reduction pair.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isPal(X)) -> isPal#(X)
p3: isPal#(V) -> isNePal#(activate(V))
p4: isNePal#(n____(I,__(P,I))) -> activate#(P)
p5: activate#(n__isNeList(X)) -> isNeList#(X)
p6: isNeList#(n____(V1,V2)) -> activate#(V2)
p7: isNeList#(n____(V1,V2)) -> activate#(V1)
p8: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p9: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2)))
p10: and#(tt(),X) -> activate#(X)
p11: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p12: isList#(n____(V1,V2)) -> activate#(V2)
p13: isList#(n____(V1,V2)) -> activate#(V1)
p14: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p15: isList#(V) -> activate#(V)
p16: isList#(V) -> isNeList#(activate(V))
p17: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p18: isNeList#(V) -> activate#(V)
p19: isNePal#(n____(I,__(P,I))) -> activate#(I)
p20: isNePal#(n____(I,__(P,I))) -> and#(isQid(activate(I)),n__isPal(activate(P)))
p21: isNePal#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isPal#_A(x1) = ((0,1),(0,0)) x1 + (79,4)
          activate#_A(x1) = ((0,1),(0,0)) x1 + (3,4)
          n__isPal_A(x1) = ((0,1),(0,1)) x1 + (235,157)
          isNePal#_A(x1) = ((0,1),(0,0)) x1 + (77,4)
          activate_A(x1) = x1 + (10,1)
          n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (116,79)
          ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (117,79)
          n__isNeList_A(x1) = ((1,1),(0,1)) x1 + (5,2)
          isNeList#_A(x1) = ((0,1),(0,0)) x1 + (4,4)
          and#_A(x1,x2) = ((0,1),(0,0)) x1 + ((0,1),(0,0)) x2 + (74,4)
          isNeList_A(x1) = ((1,1),(0,1)) x1 + (9,3)
          n__isList_A(x1) = ((1,1),(0,1)) x1 + (75,3)
          tt_A() = (2,2)
          isList#_A(x1) = ((0,1),(0,0)) x1 + (6,4)
          isList_A(x1) = ((1,1),(0,1)) x1 + (76,4)
          isQid_A(x1) = ((0,0),(0,1)) x1 + (3,1)
          isNePal_A(x1) = ((0,1),(0,1)) x1 + (91,2)
          and_A(x1,x2) = ((1,1),(0,0)) x1 + x2 + (7,1)
          nil_A() = (1,1)
          isPal_A(x1) = ((0,1),(0,1)) x1 + (236,157)
          n__nil_A() = (0,0)
          a_A() = (4,1)
          n__a_A() = (3,1)
          e_A() = (4,3)
          n__e_A() = (3,2)
          i_A() = (12,2)
          n__i_A() = (3,2)
          o_A() = (3,2)
          n__o_A() = (3,2)
          u_A() = (2,1)
          n__u_A() = (1,1)
  
    precedence:
    
      n__nil > isPal# = n__u > isNePal# > isNeList > n__isPal = activate = n____ = __ = isNePal = nil = isPal = a = n__a = i = u > n__isNeList = and > n__isList > o > e = n__e > activate# = isNeList# = and# = tt = isList# = isList = isQid = n__i = n__o
    
    partial status:
  
      pi(isPal#) = []
      pi(activate#) = []
      pi(n__isPal) = []
      pi(isNePal#) = []
      pi(activate) = []
      pi(n____) = []
      pi(__) = []
      pi(n__isNeList) = []
      pi(isNeList#) = []
      pi(and#) = []
      pi(isNeList) = []
      pi(n__isList) = [1]
      pi(tt) = []
      pi(isList#) = []
      pi(isList) = [1]
      pi(isQid) = []
      pi(isNePal) = []
      pi(and) = []
      pi(nil) = []
      pi(isPal) = []
      pi(n__nil) = []
      pi(a) = []
      pi(n__a) = []
      pi(e) = []
      pi(n__e) = []
      pi(i) = []
      pi(n__i) = []
      pi(o) = []
      pi(n__o) = []
      pi(u) = []
      pi(n__u) = []

The next rules are strictly ordered:

  p20

We remove them from the problem.

-- SCC decomposition.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isPal(X)) -> isPal#(X)
p3: isPal#(V) -> isNePal#(activate(V))
p4: isNePal#(n____(I,__(P,I))) -> activate#(P)
p5: activate#(n__isNeList(X)) -> isNeList#(X)
p6: isNeList#(n____(V1,V2)) -> activate#(V2)
p7: isNeList#(n____(V1,V2)) -> activate#(V1)
p8: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p9: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2)))
p10: and#(tt(),X) -> activate#(X)
p11: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p12: isList#(n____(V1,V2)) -> activate#(V2)
p13: isList#(n____(V1,V2)) -> activate#(V1)
p14: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p15: isList#(V) -> activate#(V)
p16: isList#(V) -> isNeList#(activate(V))
p17: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p18: isNeList#(V) -> activate#(V)
p19: isNePal#(n____(I,__(P,I))) -> activate#(I)
p20: isNePal#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> 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}


-- Reduction pair.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isNeList(X)) -> isNeList#(X)
p3: isNeList#(V) -> activate#(V)
p4: activate#(n__isPal(X)) -> isPal#(X)
p5: isPal#(V) -> isNePal#(activate(V))
p6: isNePal#(V) -> activate#(V)
p7: isNePal#(n____(I,__(P,I))) -> activate#(I)
p8: isNePal#(n____(I,__(P,I))) -> activate#(P)
p9: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p10: and#(tt(),X) -> activate#(X)
p11: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p12: isList#(V) -> isNeList#(activate(V))
p13: isNeList#(n____(V1,V2)) -> and#(isNeList(activate(V1)),n__isList(activate(V2)))
p14: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p15: isNeList#(n____(V1,V2)) -> activate#(V1)
p16: isNeList#(n____(V1,V2)) -> activate#(V2)
p17: isList#(V) -> activate#(V)
p18: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p19: isList#(n____(V1,V2)) -> activate#(V1)
p20: isList#(n____(V1,V2)) -> activate#(V2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isPal#_A(x1) = ((0,1),(0,1)) x1 + (15,1)
          activate#_A(x1) = ((0,1),(0,1)) x1 + (13,1)
          n__isNeList_A(x1) = ((0,1),(0,1)) x1 + (9,2)
          isNeList#_A(x1) = ((0,1),(0,1)) x1 + (14,3)
          n__isPal_A(x1) = ((1,1),(1,1)) x1 + (14,8)
          isNePal#_A(x1) = ((0,1),(0,1)) x1 + (14,1)
          activate_A(x1) = x1 + (7,0)
          n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (8,0)
          ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (10,0)
          and#_A(x1,x2) = ((0,1),(0,0)) x1 + ((0,1),(0,1)) x2 + (10,1)
          isList_A(x1) = ((0,1),(0,1)) x1 + (13,2)
          tt_A() = (4,7)
          isList#_A(x1) = ((0,1),(0,1)) x1 + (14,3)
          isNeList_A(x1) = ((0,1),(0,1)) x1 + (13,2)
          n__isList_A(x1) = ((0,1),(0,1)) x1 + (7,2)
          isNePal_A(x1) = ((1,1),(1,1)) x1 + (6,1)
          isQid_A(x1) = ((0,0),(0,1)) x1 + (5,1)
          and_A(x1,x2) = ((0,1),(0,0)) x1 + x2 + (1,0)
          nil_A() = (2,5)
          isPal_A(x1) = ((1,1),(1,1)) x1 + (14,8)
          n__nil_A() = (1,5)
          n__a_A() = (1,6)
          n__e_A() = (5,6)
          n__i_A() = (1,6)
          n__o_A() = (1,6)
          n__u_A() = (5,6)
          a_A() = (2,6)
          e_A() = (6,6)
          i_A() = (1,6)
          o_A() = (1,6)
          u_A() = (6,6)
  
    precedence:
    
      activate# > isNeList# = isList# > n__isPal = isNePal = isPal > n__isNeList = activate = n____ = __ = isList = isNeList > and > isQid > isPal# > isNePal# > n__isList = n__nil > and# = nil > n__a > tt = n__e = n__i = n__u = a = e = i = o = u > n__o
    
    partial status:
  
      pi(isPal#) = []
      pi(activate#) = []
      pi(n__isNeList) = []
      pi(isNeList#) = []
      pi(n__isPal) = []
      pi(isNePal#) = []
      pi(activate) = [1]
      pi(n____) = []
      pi(__) = [1, 2]
      pi(and#) = []
      pi(isList) = []
      pi(tt) = []
      pi(isList#) = []
      pi(isNeList) = []
      pi(n__isList) = []
      pi(isNePal) = []
      pi(isQid) = []
      pi(and) = []
      pi(nil) = []
      pi(isPal) = []
      pi(n__nil) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p13

We remove them from the problem.

-- SCC decomposition.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isNeList(X)) -> isNeList#(X)
p3: isNeList#(V) -> activate#(V)
p4: activate#(n__isPal(X)) -> isPal#(X)
p5: isPal#(V) -> isNePal#(activate(V))
p6: isNePal#(V) -> activate#(V)
p7: isNePal#(n____(I,__(P,I))) -> activate#(I)
p8: isNePal#(n____(I,__(P,I))) -> activate#(P)
p9: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p10: and#(tt(),X) -> activate#(X)
p11: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p12: isList#(V) -> isNeList#(activate(V))
p13: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p14: isNeList#(n____(V1,V2)) -> activate#(V1)
p15: isNeList#(n____(V1,V2)) -> activate#(V2)
p16: isList#(V) -> activate#(V)
p17: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p18: isList#(n____(V1,V2)) -> activate#(V1)
p19: isList#(n____(V1,V2)) -> activate#(V2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> 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}


-- Reduction pair.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isPal(X)) -> isPal#(X)
p3: isPal#(V) -> isNePal#(activate(V))
p4: isNePal#(n____(I,__(P,I))) -> activate#(P)
p5: activate#(n__isNeList(X)) -> isNeList#(X)
p6: isNeList#(n____(V1,V2)) -> activate#(V2)
p7: isNeList#(n____(V1,V2)) -> activate#(V1)
p8: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p9: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p10: isList#(n____(V1,V2)) -> activate#(V2)
p11: isList#(n____(V1,V2)) -> activate#(V1)
p12: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p13: and#(tt(),X) -> activate#(X)
p14: isList#(V) -> activate#(V)
p15: isList#(V) -> isNeList#(activate(V))
p16: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p17: isNeList#(V) -> activate#(V)
p18: isNePal#(n____(I,__(P,I))) -> activate#(I)
p19: isNePal#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isPal#_A(x1) = ((1,1),(0,0)) x1 + (31,42)
          activate#_A(x1) = ((0,1),(0,0)) x1 + (10,42)
          n__isPal_A(x1) = ((0,1),(1,1)) x1 + (17,22)
          isNePal#_A(x1) = ((1,1),(0,0)) x1 + (11,42)
          activate_A(x1) = x1 + (16,3)
          n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (10,41)
          ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (25,41)
          n__isNeList_A(x1) = ((0,1),(0,1)) x1 + (8,2)
          isNeList#_A(x1) = ((0,1),(0,0)) x1 + (11,42)
          isList#_A(x1) = ((0,1),(0,0)) x1 + (15,42)
          and#_A(x1,x2) = ((0,1),(0,0)) x2 + (11,42)
          isList_A(x1) = ((0,1),(0,1)) x1 + (12,16)
          n__isList_A(x1) = ((0,1),(0,1)) x1 + (8,16)
          tt_A() = (0,1)
          isNePal_A(x1) = ((0,1),(1,0)) x1 + (14,9)
          isQid_A(x1) = (0,1)
          and_A(x1,x2) = ((0,0),(0,1)) x1 + x2 + (16,2)
          n__a_A() = (1,1)
          n__e_A() = (1,1)
          n__i_A() = (1,1)
          n__o_A() = (1,1)
          n__u_A() = (1,1)
          nil_A() = (16,1)
          isNeList_A(x1) = ((0,1),(0,1)) x1 + (8,2)
          isPal_A(x1) = ((0,1),(1,1)) x1 + (17,25)
          n__nil_A() = (1,1)
          a_A() = (2,2)
          e_A() = (2,2)
          i_A() = (2,2)
          o_A() = (2,2)
          u_A() = (1,1)
  
    precedence:
    
      isPal# = activate# = isNePal# = isNeList# = isList# = and# = isList = n__isList > n__isNeList = isNePal = and = isNeList = isPal > tt = isQid > n__isPal > activate = n____ = __ > n__a = n__e = a > nil = n__nil = e > n__o = o > n__i = i > n__u = u
    
    partial status:
  
      pi(isPal#) = []
      pi(activate#) = []
      pi(n__isPal) = []
      pi(isNePal#) = []
      pi(activate) = [1]
      pi(n____) = [1, 2]
      pi(__) = [1, 2]
      pi(n__isNeList) = []
      pi(isNeList#) = []
      pi(isList#) = []
      pi(and#) = []
      pi(isList) = []
      pi(n__isList) = []
      pi(tt) = []
      pi(isNePal) = []
      pi(isQid) = []
      pi(and) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(nil) = []
      pi(isNeList) = []
      pi(isPal) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p4

We remove them from the problem.

-- SCC decomposition.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isPal(X)) -> isPal#(X)
p3: isPal#(V) -> isNePal#(activate(V))
p4: activate#(n__isNeList(X)) -> isNeList#(X)
p5: isNeList#(n____(V1,V2)) -> activate#(V2)
p6: isNeList#(n____(V1,V2)) -> activate#(V1)
p7: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p8: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p9: isList#(n____(V1,V2)) -> activate#(V2)
p10: isList#(n____(V1,V2)) -> activate#(V1)
p11: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p12: and#(tt(),X) -> activate#(X)
p13: isList#(V) -> activate#(V)
p14: isList#(V) -> isNeList#(activate(V))
p15: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p16: isNeList#(V) -> activate#(V)
p17: isNePal#(n____(I,__(P,I))) -> activate#(I)
p18: isNePal#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> 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}


-- Reduction pair.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isNeList(X)) -> isNeList#(X)
p3: isNeList#(V) -> activate#(V)
p4: activate#(n__isPal(X)) -> isPal#(X)
p5: isPal#(V) -> isNePal#(activate(V))
p6: isNePal#(V) -> activate#(V)
p7: isNePal#(n____(I,__(P,I))) -> activate#(I)
p8: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p9: and#(tt(),X) -> activate#(X)
p10: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p11: isList#(V) -> isNeList#(activate(V))
p12: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p13: isNeList#(n____(V1,V2)) -> activate#(V1)
p14: isNeList#(n____(V1,V2)) -> activate#(V2)
p15: isList#(V) -> activate#(V)
p16: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p17: isList#(n____(V1,V2)) -> activate#(V1)
p18: isList#(n____(V1,V2)) -> activate#(V2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isPal#_A(x1) = ((1,1),(1,1)) x1 + (79,72)
          activate#_A(x1) = ((1,1),(1,1)) x1 + (68,16)
          n__isNeList_A(x1) = ((0,1),(1,0)) x1 + (1,13)
          isNeList#_A(x1) = ((1,1),(1,1)) x1 + (69,30)
          n__isPal_A(x1) = ((0,1),(1,0)) x1 + (66,71)
          isNePal#_A(x1) = ((1,1),(1,1)) x1 + (69,16)
          activate_A(x1) = x1 + (7,2)
          n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (33,38)
          ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (34,39)
          and#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,1),(1,1)) x2 + (68,16)
          isList_A(x1) = ((0,1),(1,0)) x1 + (6,21)
          tt_A() = (1,1)
          isList#_A(x1) = ((1,1),(1,1)) x1 + (79,39)
          n__isList_A(x1) = ((0,1),(1,0)) x1 + (6,21)
          isNePal_A(x1) = ((0,1),(1,0)) x1 + (6,30)
          isQid_A(x1) = ((0,0),(1,0)) x1 + (2,0)
          and_A(x1,x2) = ((0,1),(0,0)) x1 + x2 + (7,19)
          n__a_A() = (2,1)
          n__e_A() = (2,1)
          n__i_A() = (2,1)
          n__o_A() = (2,1)
          n__u_A() = (2,1)
          nil_A() = (3,1)
          isNeList_A(x1) = ((0,1),(1,0)) x1 + (3,14)
          isPal_A(x1) = ((0,1),(1,0)) x1 + (67,72)
          n__nil_A() = (2,1)
          a_A() = (3,2)
          e_A() = (3,2)
          i_A() = (3,2)
          o_A() = (3,2)
          u_A() = (3,2)
  
    precedence:
    
      n__isNeList > isPal# = activate# = isNeList# = activate = __ = and# = isList = isList# = n__isList = isNePal = isQid = and = n__u = isPal = a = e > n__isPal = isNePal# = n____ = n__a = n__e > tt = n__i = n__o = nil = isNeList = n__nil = i = o = u
    
    partial status:
  
      pi(isPal#) = []
      pi(activate#) = []
      pi(n__isNeList) = []
      pi(isNeList#) = []
      pi(n__isPal) = []
      pi(isNePal#) = [1]
      pi(activate) = []
      pi(n____) = [1]
      pi(__) = [1, 2]
      pi(and#) = []
      pi(isList) = []
      pi(tt) = []
      pi(isList#) = []
      pi(n__isList) = []
      pi(isNePal) = []
      pi(isQid) = []
      pi(and) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(nil) = []
      pi(isNeList) = []
      pi(isPal) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p5

We remove them from the problem.

-- SCC decomposition.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isNeList(X)) -> isNeList#(X)
p3: isNeList#(V) -> activate#(V)
p4: activate#(n__isPal(X)) -> isPal#(X)
p5: isNePal#(V) -> activate#(V)
p6: isNePal#(n____(I,__(P,I))) -> activate#(I)
p7: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p8: and#(tt(),X) -> activate#(X)
p9: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p10: isList#(V) -> isNeList#(activate(V))
p11: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p12: isNeList#(n____(V1,V2)) -> activate#(V1)
p13: isNeList#(n____(V1,V2)) -> activate#(V2)
p14: isList#(V) -> activate#(V)
p15: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p16: isList#(n____(V1,V2)) -> activate#(V1)
p17: isList#(n____(V1,V2)) -> activate#(V2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: isPal#(V) -> activate#(V)
p2: activate#(n__isPal(X)) -> isPal#(X)
p3: activate#(n__isNeList(X)) -> isNeList#(X)
p4: isNeList#(n____(V1,V2)) -> activate#(V2)
p5: isNeList#(n____(V1,V2)) -> activate#(V1)
p6: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p7: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p8: isList#(n____(V1,V2)) -> activate#(V2)
p9: isList#(n____(V1,V2)) -> activate#(V1)
p10: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p11: and#(tt(),X) -> activate#(X)
p12: isList#(V) -> activate#(V)
p13: isList#(V) -> isNeList#(activate(V))
p14: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p15: isNeList#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isPal#_A(x1) = x1 + (35,1)
          activate#_A(x1) = x1
          n__isPal_A(x1) = ((1,1),(1,1)) x1 + (36,30)
          n__isNeList_A(x1) = ((1,0),(1,1)) x1 + (33,24)
          isNeList#_A(x1) = ((1,0),(1,1)) x1 + (20,1)
          n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (16,13)
          activate_A(x1) = x1 + (3,3)
          isList#_A(x1) = ((1,0),(1,1)) x1 + (30,7)
          and#_A(x1,x2) = x2
          isList_A(x1) = ((1,0),(1,1)) x1 + (44,33)
          n__isList_A(x1) = ((1,0),(1,1)) x1 + (42,30)
          tt_A() = (2,2)
          isNePal_A(x1) = ((0,1),(1,1)) x1 + (34,27)
          isQid_A(x1) = (33,27)
          ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (16,13)
          and_A(x1,x2) = x2 + (4,3)
          n__a_A() = (1,1)
          n__e_A() = (0,0)
          n__i_A() = (1,1)
          n__o_A() = (1,0)
          n__u_A() = (0,0)
          nil_A() = (1,1)
          isNeList_A(x1) = ((1,0),(1,1)) x1 + (34,27)
          isPal_A(x1) = ((1,1),(1,1)) x1 + (38,33)
          n__nil_A() = (0,0)
          a_A() = (3,2)
          e_A() = (2,1)
          i_A() = (3,2)
          o_A() = (2,3)
          u_A() = (2,3)
  
    precedence:
    
      isPal# = n__o > isNeList# = isList# > activate# = activate = and# = isList = isNePal = isQid = and = n__a = nil = isNeList = isPal > tt > n____ = __ > n__isPal = n__isNeList = n__isList = n__u = n__nil > n__e = e = i > o > a = u > n__i
    
    partial status:
  
      pi(isPal#) = []
      pi(activate#) = [1]
      pi(n__isPal) = []
      pi(n__isNeList) = []
      pi(isNeList#) = []
      pi(n____) = [1, 2]
      pi(activate) = []
      pi(isList#) = [1]
      pi(and#) = [2]
      pi(isList) = []
      pi(n__isList) = []
      pi(tt) = []
      pi(isNePal) = []
      pi(isQid) = []
      pi(__) = [1, 2]
      pi(and) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(nil) = []
      pi(isNeList) = []
      pi(isPal) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: activate#(n__isPal(X)) -> isPal#(X)
p2: activate#(n__isNeList(X)) -> isNeList#(X)
p3: isNeList#(n____(V1,V2)) -> activate#(V2)
p4: isNeList#(n____(V1,V2)) -> activate#(V1)
p5: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p6: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p7: isList#(n____(V1,V2)) -> activate#(V2)
p8: isList#(n____(V1,V2)) -> activate#(V1)
p9: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p10: and#(tt(),X) -> activate#(X)
p11: isList#(V) -> activate#(V)
p12: isList#(V) -> isNeList#(activate(V))
p13: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p14: isNeList#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: activate#(n__isNeList(X)) -> isNeList#(X)
p2: isNeList#(V) -> activate#(V)
p3: isNeList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isNeList(activate(V2)))
p4: and#(tt(),X) -> activate#(X)
p5: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p6: isList#(V) -> isNeList#(activate(V))
p7: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p8: isNeList#(n____(V1,V2)) -> activate#(V1)
p9: isNeList#(n____(V1,V2)) -> activate#(V2)
p10: isList#(V) -> activate#(V)
p11: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p12: isList#(n____(V1,V2)) -> activate#(V1)
p13: isList#(n____(V1,V2)) -> activate#(V2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          activate#_A(x1) = ((1,0),(0,0)) x1 + (4,2)
          n__isNeList_A(x1) = ((1,0),(1,1)) x1 + (29,1)
          isNeList#_A(x1) = ((1,0),(0,0)) x1 + (18,2)
          n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (19,0)
          and#_A(x1,x2) = ((1,0),(0,0)) x2 + (5,2)
          isList_A(x1) = ((1,0),(1,1)) x1 + (36,8)
          activate_A(x1) = x1 + (2,3)
          tt_A() = (3,0)
          isList#_A(x1) = ((1,0),(0,0)) x1 + (34,2)
          n__isList_A(x1) = ((1,0),(1,1)) x1 + (36,5)
          isNePal_A(x1) = ((1,0),(0,0)) x1 + (5,3)
          isQid_A(x1) = (4,0)
          ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (19,0)
          and_A(x1,x2) = ((0,0),(0,1)) x1 + x2 + (3,3)
          n__isPal_A(x1) = ((1,0),(0,0)) x1 + (16,0)
          n__a_A() = (4,1)
          n__e_A() = (4,1)
          n__i_A() = (4,1)
          n__o_A() = (4,1)
          n__u_A() = (4,1)
          nil_A() = (1,2)
          isNeList_A(x1) = ((1,0),(1,1)) x1 + (30,3)
          isPal_A(x1) = ((1,0),(0,0)) x1 + (16,3)
          n__nil_A() = (0,1)
          a_A() = (5,2)
          e_A() = (5,2)
          i_A() = (5,2)
          o_A() = (5,2)
          u_A() = (5,2)
  
    precedence:
    
      activate# = isNeList# = n____ = and# = isList = activate = isList# = isNePal = __ = and = n__a = n__i = n__u = isNeList = isPal = i > n__e > n__isNeList > n__isPal > n__o = a = o > tt > n__isList = isQid = n__nil > nil = e = u
    
    partial status:
  
      pi(activate#) = []
      pi(n__isNeList) = []
      pi(isNeList#) = []
      pi(n____) = []
      pi(and#) = []
      pi(isList) = []
      pi(activate) = []
      pi(tt) = []
      pi(isList#) = []
      pi(n__isList) = []
      pi(isNePal) = []
      pi(isQid) = []
      pi(__) = []
      pi(and) = []
      pi(n__isPal) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(nil) = []
      pi(isNeList) = []
      pi(isPal) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p3

We remove them from the problem.

-- SCC decomposition.

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

p1: activate#(n__isNeList(X)) -> isNeList#(X)
p2: isNeList#(V) -> activate#(V)
p3: and#(tt(),X) -> activate#(X)
p4: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p5: isList#(V) -> isNeList#(activate(V))
p6: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p7: isNeList#(n____(V1,V2)) -> activate#(V1)
p8: isNeList#(n____(V1,V2)) -> activate#(V2)
p9: isList#(V) -> activate#(V)
p10: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p11: isList#(n____(V1,V2)) -> activate#(V1)
p12: isList#(n____(V1,V2)) -> activate#(V2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: activate#(n__isNeList(X)) -> isNeList#(X)
p2: isNeList#(n____(V1,V2)) -> activate#(V2)
p3: isNeList#(n____(V1,V2)) -> activate#(V1)
p4: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p5: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p6: isList#(n____(V1,V2)) -> activate#(V2)
p7: isList#(n____(V1,V2)) -> activate#(V1)
p8: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p9: and#(tt(),X) -> activate#(X)
p10: isList#(V) -> activate#(V)
p11: isList#(V) -> isNeList#(activate(V))
p12: isNeList#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          activate#_A(x1) = ((0,1),(0,0)) x1 + (5,7)
          n__isNeList_A(x1) = ((0,1),(0,1)) x1 + (1,8)
          isNeList#_A(x1) = ((0,1),(0,0)) x1 + (12,7)
          n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2
          activate_A(x1) = x1
          isList#_A(x1) = ((0,1),(0,0)) x1 + (12,7)
          and#_A(x1,x2) = ((1,0),(0,0)) x1 + ((0,1),(0,0)) x2 + (2,7)
          isList_A(x1) = ((0,1),(0,1)) x1 + (1,8)
          n__isList_A(x1) = ((0,1),(0,1)) x1 + (1,8)
          tt_A() = (4,6)
          isNePal_A(x1) = ((0,1),(0,1)) x1 + (1,2)
          isQid_A(x1) = ((0,1),(0,1)) x1 + (0,2)
          ___A(x1,x2) = ((1,0),(1,1)) x1 + x2
          and_A(x1,x2) = x2
          n__isPal_A(x1) = ((1,1),(0,1)) x1 + (1,2)
          n__a_A() = (1,5)
          n__e_A() = (5,4)
          n__i_A() = (1,4)
          n__o_A() = (5,4)
          n__u_A() = (1,5)
          nil_A() = (5,6)
          isNeList_A(x1) = ((0,1),(0,1)) x1 + (1,8)
          isPal_A(x1) = ((1,1),(0,1)) x1 + (1,2)
          n__nil_A() = (5,6)
          a_A() = (1,5)
          e_A() = (5,4)
          i_A() = (1,4)
          o_A() = (5,4)
          u_A() = (1,5)
  
    precedence:
    
      activate# = n__isNeList = isNeList# = n____ = activate = isList# = and# = isList = n__isList = tt = isNePal = isQid = __ = and = n__isPal = n__a = n__e = n__i = n__o = n__u = nil = isNeList = isPal = n__nil = a = e = i = o = u
    
    partial status:
  
      pi(activate#) = []
      pi(n__isNeList) = []
      pi(isNeList#) = []
      pi(n____) = []
      pi(activate) = []
      pi(isList#) = []
      pi(and#) = []
      pi(isList) = []
      pi(n__isList) = []
      pi(tt) = []
      pi(isNePal) = []
      pi(isQid) = []
      pi(__) = []
      pi(and) = []
      pi(n__isPal) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(nil) = []
      pi(isNeList) = []
      pi(isPal) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

p1: activate#(n__isNeList(X)) -> isNeList#(X)
p2: isNeList#(n____(V1,V2)) -> activate#(V1)
p3: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p4: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p5: isList#(n____(V1,V2)) -> activate#(V2)
p6: isList#(n____(V1,V2)) -> activate#(V1)
p7: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p8: and#(tt(),X) -> activate#(X)
p9: isList#(V) -> activate#(V)
p10: isList#(V) -> isNeList#(activate(V))
p11: isNeList#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: activate#(n__isNeList(X)) -> isNeList#(X)
p2: isNeList#(V) -> activate#(V)
p3: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p4: isList#(V) -> isNeList#(activate(V))
p5: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p6: isNeList#(n____(V1,V2)) -> activate#(V1)
p7: isList#(V) -> activate#(V)
p8: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p9: and#(tt(),X) -> activate#(X)
p10: isList#(n____(V1,V2)) -> activate#(V1)
p11: isList#(n____(V1,V2)) -> activate#(V2)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          activate#_A(x1) = ((1,0),(0,0)) x1
          n__isNeList_A(x1) = ((1,1),(1,0)) x1 + (5,2)
          isNeList#_A(x1) = ((1,1),(0,0)) x1 + (1,0)
          n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (63,57)
          isList#_A(x1) = ((1,1),(0,0)) x1 + (44,0)
          activate_A(x1) = x1 + (4,16)
          and#_A(x1,x2) = ((1,0),(0,0)) x1 + ((1,0),(0,0)) x2 + (1,0)
          isList_A(x1) = ((1,1),(1,0)) x1 + (25,15)
          n__isList_A(x1) = ((1,1),(1,0)) x1 + (25,15)
          tt_A() = (2,2)
          isNePal_A(x1) = ((0,1),(0,0)) x1 + (3,147)
          isQid_A(x1) = (2,2)
          ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (64,73)
          and_A(x1,x2) = ((0,0),(1,0)) x1 + x2 + (4,14)
          n__isPal_A(x1) = ((0,1),(0,0)) x1 + (112,131)
          n__a_A() = (1,1)
          n__e_A() = (1,1)
          n__i_A() = (3,1)
          n__o_A() = (1,1)
          n__u_A() = (1,1)
          nil_A() = (3,2)
          isNeList_A(x1) = ((1,1),(1,0)) x1 + (5,2)
          isPal_A(x1) = ((0,1),(0,0)) x1 + (116,147)
          n__nil_A() = (3,2)
          a_A() = (2,2)
          e_A() = (2,2)
          i_A() = (4,2)
          o_A() = (2,2)
          u_A() = (2,2)
  
    precedence:
    
      isList = n__isList > n__isNeList = isNeList > activate = isNePal = and = isPal > __ = n__isPal = n__e = u > n__a > tt = isQid = nil > n__nil > n__i = n__o = a = e = i = o > activate# = isNeList# = n____ = isList# = and# = n__u
    
    partial status:
  
      pi(activate#) = []
      pi(n__isNeList) = []
      pi(isNeList#) = []
      pi(n____) = []
      pi(isList#) = []
      pi(activate) = [1]
      pi(and#) = []
      pi(isList) = []
      pi(n__isList) = []
      pi(tt) = []
      pi(isNePal) = []
      pi(isQid) = []
      pi(__) = [1, 2]
      pi(and) = [2]
      pi(n__isPal) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(nil) = []
      pi(isNeList) = []
      pi(isPal) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p11

We remove them from the problem.

-- SCC decomposition.

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

p1: activate#(n__isNeList(X)) -> isNeList#(X)
p2: isNeList#(V) -> activate#(V)
p3: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p4: isList#(V) -> isNeList#(activate(V))
p5: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p6: isNeList#(n____(V1,V2)) -> activate#(V1)
p7: isList#(V) -> activate#(V)
p8: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p9: and#(tt(),X) -> activate#(X)
p10: isList#(n____(V1,V2)) -> activate#(V1)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: activate#(n__isNeList(X)) -> isNeList#(X)
p2: isNeList#(n____(V1,V2)) -> activate#(V1)
p3: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p4: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p5: isList#(n____(V1,V2)) -> activate#(V1)
p6: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p7: and#(tt(),X) -> activate#(X)
p8: isList#(V) -> activate#(V)
p9: isList#(V) -> isNeList#(activate(V))
p10: isNeList#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          activate#_A(x1) = ((1,0),(0,0)) x1
          n__isNeList_A(x1) = x1 + (3,0)
          isNeList#_A(x1) = ((1,0),(0,0)) x1 + (3,0)
          n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (22,26)
          activate_A(x1) = x1 + (5,8)
          isList#_A(x1) = ((1,0),(0,0)) x1 + (18,0)
          and#_A(x1,x2) = ((1,0),(0,0)) x2 + (8,0)
          isList_A(x1) = x1 + (10,10)
          n__isList_A(x1) = x1 + (10,10)
          tt_A() = (2,2)
          isNePal_A(x1) = ((1,0),(1,0)) x1 + (4,2)
          isQid_A(x1) = (3,2)
          ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (23,26)
          and_A(x1,x2) = x2 + (6,8)
          n__isPal_A(x1) = ((1,0),(1,1)) x1 + (17,7)
          n__a_A() = (1,1)
          n__e_A() = (1,1)
          n__i_A() = (1,1)
          n__o_A() = (1,1)
          n__u_A() = (1,1)
          nil_A() = (5,2)
          isNeList_A(x1) = x1 + (4,2)
          isPal_A(x1) = ((1,0),(1,1)) x1 + (17,7)
          n__nil_A() = (0,1)
          a_A() = (2,1)
          e_A() = (2,2)
          i_A() = (2,2)
          o_A() = (1,1)
          u_A() = (2,2)
  
    precedence:
    
      n__a = a > n__isPal = isPal > isNePal > n__isNeList > n__o = o > activate = isList = n__isList = tt = isQid = isNeList > nil = n__nil > activate# = isNeList# = n____ = isList# = and# = __ > and > n__e = e > n__i = i > n__u = u
    
    partial status:
  
      pi(activate#) = []
      pi(n__isNeList) = []
      pi(isNeList#) = []
      pi(n____) = []
      pi(activate) = [1]
      pi(isList#) = []
      pi(and#) = []
      pi(isList) = []
      pi(n__isList) = []
      pi(tt) = []
      pi(isNePal) = []
      pi(isQid) = []
      pi(__) = [1, 2]
      pi(and) = [2]
      pi(n__isPal) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(nil) = []
      pi(isNeList) = []
      pi(isPal) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p8

We remove them from the problem.

-- SCC decomposition.

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

p1: activate#(n__isNeList(X)) -> isNeList#(X)
p2: isNeList#(n____(V1,V2)) -> activate#(V1)
p3: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p4: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p5: isList#(n____(V1,V2)) -> activate#(V1)
p6: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p7: and#(tt(),X) -> activate#(X)
p8: isList#(V) -> isNeList#(activate(V))
p9: isNeList#(V) -> activate#(V)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: activate#(n__isNeList(X)) -> isNeList#(X)
p2: isNeList#(V) -> activate#(V)
p3: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p4: isList#(V) -> isNeList#(activate(V))
p5: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p6: isNeList#(n____(V1,V2)) -> activate#(V1)
p7: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p8: and#(tt(),X) -> activate#(X)
p9: isList#(n____(V1,V2)) -> activate#(V1)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          activate#_A(x1) = ((1,0),(0,0)) x1 + (1,3)
          n__isNeList_A(x1) = ((1,0),(0,0)) x1 + (5,3)
          isNeList#_A(x1) = ((1,0),(0,0)) x1 + (1,3)
          n_____A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (13,3)
          isList#_A(x1) = ((1,0),(0,0)) x1 + (7,3)
          activate_A(x1) = x1 + (5,2)
          and#_A(x1,x2) = ((1,0),(0,0)) x2 + (2,3)
          isList_A(x1) = ((1,0),(0,0)) x1 + (16,5)
          n__isList_A(x1) = ((1,0),(0,0)) x1 + (12,3)
          tt_A() = (2,3)
          isNePal_A(x1) = ((0,1),(0,0)) x1 + (4,7)
          isQid_A(x1) = (3,3)
          ___A(x1,x2) = ((1,0),(1,1)) x1 + x2 + (14,3)
          and_A(x1,x2) = x2 + (5,2)
          n__isPal_A(x1) = ((0,1),(0,0)) x1 + (2,5)
          n__a_A() = (1,1)
          n__e_A() = (1,1)
          n__i_A() = (1,1)
          n__o_A() = (0,1)
          n__u_A() = (0,1)
          nil_A() = (4,4)
          isNeList_A(x1) = ((1,0),(0,0)) x1 + (10,5)
          isPal_A(x1) = ((0,1),(0,0)) x1 + (6,7)
          n__nil_A() = (3,3)
          a_A() = (1,1)
          e_A() = (6,2)
          i_A() = (2,2)
          o_A() = (5,2)
          u_A() = (5,2)
  
    precedence:
    
      activate# = n__isNeList = isNeList# = n____ = isList# = activate = and# = isList = isNePal = __ = and = n__isPal = nil = isNeList = isPal > tt = isQid > n__isList > n__i = n__u = i = u > n__o = n__nil = o > n__a = a > n__e = e
    
    partial status:
  
      pi(activate#) = []
      pi(n__isNeList) = []
      pi(isNeList#) = []
      pi(n____) = []
      pi(isList#) = []
      pi(activate) = []
      pi(and#) = []
      pi(isList) = []
      pi(n__isList) = []
      pi(tt) = []
      pi(isNePal) = []
      pi(isQid) = []
      pi(__) = []
      pi(and) = []
      pi(n__isPal) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(nil) = []
      pi(isNeList) = []
      pi(isPal) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: isNeList#(V) -> activate#(V)
p2: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p3: isList#(V) -> isNeList#(activate(V))
p4: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p5: isNeList#(n____(V1,V2)) -> activate#(V1)
p6: isList#(n____(V1,V2)) -> and#(isList(activate(V1)),n__isList(activate(V2)))
p7: and#(tt(),X) -> activate#(X)
p8: isList#(n____(V1,V2)) -> activate#(V1)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p2, p3, p4}


-- Reduction pair.

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

p1: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p2: isList#(V) -> isNeList#(activate(V))
p3: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isNeList#_A(x1) = ((1,0),(1,1)) x1 + (5,0)
          n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (6,0)
          isList#_A(x1) = ((1,0),(1,1)) x1 + (8,3)
          activate_A(x1) = x1 + (2,1)
          and_A(x1,x2) = ((1,0),(1,1)) x2 + (2,1)
          tt_A() = (0,0)
          isNePal_A(x1) = ((1,0),(1,1)) x1 + (3,1)
          isQid_A(x1) = (0,0)
          ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (7,1)
          n__isPal_A(x1) = ((1,0),(1,1)) x1 + (6,3)
          n__a_A() = (1,1)
          n__e_A() = (1,1)
          n__i_A() = (1,1)
          n__o_A() = (1,1)
          n__u_A() = (1,1)
          nil_A() = (0,1)
          isList_A(x1) = ((0,0),(1,1)) x1 + (2,5)
          isNeList_A(x1) = ((0,0),(1,1)) x1 + (2,2)
          n__nil_A() = (0,1)
          n__isList_A(x1) = ((0,0),(1,1)) x1 + (0,4)
          n__isNeList_A(x1) = ((0,0),(1,1)) x1 + (0,1)
          isPal_A(x1) = ((1,0),(1,1)) x1 + (7,4)
          a_A() = (2,2)
          e_A() = (2,2)
          i_A() = (2,2)
          o_A() = (2,2)
          u_A() = (2,2)
  
    precedence:
    
      isNeList# = n____ = isList# = activate = and = __ = n__isPal = n__a = n__e = n__o = n__u = isList = isNeList = n__isNeList = isPal = u > isNePal = isQid > n__i = nil = n__nil = n__isList = a = e = i > tt = o
    
    partial status:
  
      pi(isNeList#) = []
      pi(n____) = []
      pi(isList#) = []
      pi(activate) = []
      pi(and) = []
      pi(tt) = []
      pi(isNePal) = []
      pi(isQid) = []
      pi(__) = []
      pi(n__isPal) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(nil) = []
      pi(isList) = []
      pi(isNeList) = []
      pi(n__nil) = []
      pi(n__isList) = []
      pi(n__isNeList) = []
      pi(isPal) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

p1: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p2: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p2}


-- Reduction pair.

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

p1: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          isNeList#_A(x1) = ((1,0),(1,1)) x1 + (1,0)
          n_____A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (12,22)
          activate_A(x1) = x1 + (8,9)
          and_A(x1,x2) = x2 + (8,9)
          tt_A() = (2,0)
          isNePal_A(x1) = ((0,0),(1,0)) x1 + (13,0)
          isQid_A(x1) = (8,0)
          ___A(x1,x2) = ((1,1),(1,1)) x1 + x2 + (12,22)
          n__isPal_A(x1) = ((0,0),(1,0)) x1 + (5,7)
          n__a_A() = (1,1)
          n__e_A() = (1,1)
          n__i_A() = (1,1)
          n__o_A() = (1,1)
          n__u_A() = (1,0)
          nil_A() = (2,2)
          isList_A(x1) = ((0,0),(0,1)) x1 + (9,13)
          isNeList_A(x1) = ((0,0),(0,1)) x1 + (9,4)
          n__nil_A() = (1,1)
          n__isList_A(x1) = ((0,0),(0,1)) x1 + (1,4)
          n__isNeList_A(x1) = ((0,0),(0,1)) x1 + (1,2)
          isPal_A(x1) = ((0,0),(1,0)) x1 + (13,8)
          a_A() = (2,2)
          e_A() = (2,2)
          i_A() = (2,2)
          o_A() = (2,2)
          u_A() = (2,1)
  
    precedence:
    
      isNeList# = n____ = activate = and = tt = isNePal = isQid = __ = n__isPal = n__a = n__e = n__i = n__o = n__u = nil = isList = isNeList = n__nil = n__isList = n__isNeList = isPal = a = e = i = o = u
    
    partial status:
  
      pi(isNeList#) = []
      pi(n____) = []
      pi(activate) = []
      pi(and) = []
      pi(tt) = []
      pi(isNePal) = []
      pi(isQid) = []
      pi(__) = []
      pi(n__isPal) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(nil) = []
      pi(isList) = []
      pi(isNeList) = []
      pi(n__nil) = []
      pi(n__isList) = []
      pi(n__isNeList) = []
      pi(isPal) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p1

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

-- Reduction pair.

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

p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z))
p2: __#(__(X,Y),Z) -> __#(Y,Z)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r21

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          __#_A(x1,x2) = ((1,1),(1,1)) x1 + ((1,1),(1,1)) x2 + (3,2)
          ___A(x1,x2) = x1 + x2 + (2,1)
          nil_A() = (1,1)
          n_____A(x1,x2) = (1,1)
  
    precedence:
    
      __ > __# = nil = n____
    
    partial status:
  
      pi(__#) = [1]
      pi(__) = []
      pi(nil) = []
      pi(n____) = []

The next rules are strictly ordered:

  p2

We remove them from the problem.

-- SCC decomposition.

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

p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p1}


-- Reduction pair.

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

p1: __#(__(X,Y),Z) -> __#(X,__(Y,Z))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: and(tt(),X) -> activate(X)
r5: isList(V) -> isNeList(activate(V))
r6: isList(n__nil()) -> tt()
r7: isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
r8: isNeList(V) -> isQid(activate(V))
r9: isNeList(n____(V1,V2)) -> and(isList(activate(V1)),n__isNeList(activate(V2)))
r10: isNeList(n____(V1,V2)) -> and(isNeList(activate(V1)),n__isList(activate(V2)))
r11: isNePal(V) -> isQid(activate(V))
r12: isNePal(n____(I,__(P,I))) -> and(isQid(activate(I)),n__isPal(activate(P)))
r13: isPal(V) -> isNePal(activate(V))
r14: isPal(n__nil()) -> tt()
r15: isQid(n__a()) -> tt()
r16: isQid(n__e()) -> tt()
r17: isQid(n__i()) -> tt()
r18: isQid(n__o()) -> tt()
r19: isQid(n__u()) -> tt()
r20: nil() -> n__nil()
r21: __(X1,X2) -> n____(X1,X2)
r22: isList(X) -> n__isList(X)
r23: isNeList(X) -> n__isNeList(X)
r24: isPal(X) -> n__isPal(X)
r25: a() -> n__a()
r26: e() -> n__e()
r27: i() -> n__i()
r28: o() -> n__o()
r29: u() -> n__u()
r30: activate(n__nil()) -> nil()
r31: activate(n____(X1,X2)) -> __(X1,X2)
r32: activate(n__isList(X)) -> isList(X)
r33: activate(n__isNeList(X)) -> isNeList(X)
r34: activate(n__isPal(X)) -> isPal(X)
r35: activate(n__a()) -> a()
r36: activate(n__e()) -> e()
r37: activate(n__i()) -> i()
r38: activate(n__o()) -> o()
r39: activate(n__u()) -> u()
r40: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r21

Take the reduction pair:

  weighted path order
  
    base order:
  
      matrix interpretations:
      
        carrier: N^2
        order: standard order
        interpretations:
          __#_A(x1,x2) = ((1,1),(0,1)) x1 + (2,2)
          ___A(x1,x2) = x1 + x2 + (1,1)
          nil_A() = (1,1)
          n_____A(x1,x2) = (0,0)
  
    precedence:
    
      __ > __# = nil = n____
    
    partial status:
  
      pi(__#) = [1]
      pi(__) = []
      pi(nil) = []
      pi(n____) = []

The next rules are strictly ordered:

  p1

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