YES

We show the termination of the TRS R:

  __(__(X,Y),Z) -> __(X,__(Y,Z))
  __(X,nil()) -> X
  __(nil(),X) -> X
  U11(tt()) -> tt()
  U21(tt(),V2) -> U22(isList(activate(V2)))
  U22(tt()) -> tt()
  U31(tt()) -> tt()
  U41(tt(),V2) -> U42(isNeList(activate(V2)))
  U42(tt()) -> tt()
  U51(tt(),V2) -> U52(isList(activate(V2)))
  U52(tt()) -> tt()
  U61(tt()) -> tt()
  U71(tt(),P) -> U72(isPal(activate(P)))
  U72(tt()) -> tt()
  U81(tt()) -> tt()
  isList(V) -> U11(isNeList(activate(V)))
  isList(n__nil()) -> tt()
  isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
  isNeList(V) -> U31(isQid(activate(V)))
  isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
  isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
  isNePal(V) -> U61(isQid(activate(V)))
  isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
  isPal(V) -> U81(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)
  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__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: U21#(tt(),V2) -> U22#(isList(activate(V2)))
p4: U21#(tt(),V2) -> isList#(activate(V2))
p5: U21#(tt(),V2) -> activate#(V2)
p6: U41#(tt(),V2) -> U42#(isNeList(activate(V2)))
p7: U41#(tt(),V2) -> isNeList#(activate(V2))
p8: U41#(tt(),V2) -> activate#(V2)
p9: U51#(tt(),V2) -> U52#(isList(activate(V2)))
p10: U51#(tt(),V2) -> isList#(activate(V2))
p11: U51#(tt(),V2) -> activate#(V2)
p12: U71#(tt(),P) -> U72#(isPal(activate(P)))
p13: U71#(tt(),P) -> isPal#(activate(P))
p14: U71#(tt(),P) -> activate#(P)
p15: isList#(V) -> U11#(isNeList(activate(V)))
p16: isList#(V) -> isNeList#(activate(V))
p17: isList#(V) -> activate#(V)
p18: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p19: isList#(n____(V1,V2)) -> isList#(activate(V1))
p20: isList#(n____(V1,V2)) -> activate#(V1)
p21: isList#(n____(V1,V2)) -> activate#(V2)
p22: isNeList#(V) -> U31#(isQid(activate(V)))
p23: isNeList#(V) -> isQid#(activate(V))
p24: isNeList#(V) -> activate#(V)
p25: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))
p26: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p27: isNeList#(n____(V1,V2)) -> activate#(V1)
p28: isNeList#(n____(V1,V2)) -> activate#(V2)
p29: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p30: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p31: isNeList#(n____(V1,V2)) -> activate#(V1)
p32: isNeList#(n____(V1,V2)) -> activate#(V2)
p33: isNePal#(V) -> U61#(isQid(activate(V)))
p34: isNePal#(V) -> isQid#(activate(V))
p35: isNePal#(V) -> activate#(V)
p36: isNePal#(n____(I,__(P,I))) -> U71#(isQid(activate(I)),activate(P))
p37: isNePal#(n____(I,__(P,I))) -> isQid#(activate(I))
p38: isNePal#(n____(I,__(P,I))) -> activate#(I)
p39: isNePal#(n____(I,__(P,I))) -> activate#(P)
p40: isPal#(V) -> U81#(isNePal(activate(V)))
p41: isPal#(V) -> isNePal#(activate(V))
p42: isPal#(V) -> activate#(V)
p43: activate#(n__nil()) -> nil#()
p44: activate#(n____(X1,X2)) -> __#(X1,X2)
p45: activate#(n__a()) -> a#()
p46: activate#(n__e()) -> e#()
p47: activate#(n__i()) -> i#()
p48: activate#(n__o()) -> o#()
p49: activate#(n__u()) -> u#()

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p13, p36, p41}
  {p4, p7, p10, p16, p18, p19, p25, p26, p29, p30}
  {p1, p2}


-- Reduction pair.

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

p1: isPal#(V) -> isNePal#(activate(V))
p2: isNePal#(n____(I,__(P,I))) -> U71#(isQid(activate(I)),activate(P))
p3: U71#(tt(),P) -> isPal#(activate(P))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        isPal#_A(x1) = max{5, x1 - 4}
        isNePal#_A(x1) = max{1, x1 - 12}
        activate_A(x1) = max{7, x1 + 5}
        n_____A(x1,x2) = max{58, x1 + 26, x2 - 1}
        ___A(x1,x2) = max{63, x1 + 31, x2}
        U71#_A(x1,x2) = max{x1 - 78, x2 + 6}
        isQid_A(x1) = x1 + 84
        tt_A = 82
        nil_A = 1
        n__nil_A = 0
        a_A = 8
        n__a_A = 4
        e_A = 8
        n__e_A = 4
        i_A = 8
        n__i_A = 4
        o_A = 8
        n__o_A = 4
        u_A = 8
        n__u_A = 7
  
    precedence:
    
      isNePal# = activate = n____ = __ = U71# = isQid = tt = nil = n__nil = a = n__a = e = n__e = i = n__i = o > isPal# = n__o = u = n__u
    
    partial status:
  
      pi(isPal#) = []
      pi(isNePal#) = []
      pi(activate) = [1]
      pi(n____) = [1]
      pi(__) = [1, 2]
      pi(U71#) = [2]
      pi(isQid) = []
      pi(tt) = []
      pi(nil) = []
      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:

  p1

We remove them from the problem.

-- SCC decomposition.

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

p1: isNePal#(n____(I,__(P,I))) -> U71#(isQid(activate(I)),activate(P))
p2: U71#(tt(),P) -> isPal#(activate(P))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  (no SCCs)

-- Reduction pair.

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

p1: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(n____(V1,V2)) -> isList#(activate(V1))
p4: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p5: U21#(tt(),V2) -> isList#(activate(V2))
p6: isList#(V) -> isNeList#(activate(V))
p7: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p8: isNeList#(n____(V1,V2)) -> isList#(activate(V1))
p9: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))
p10: U41#(tt(),V2) -> isNeList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        isNeList#_A(x1) = x1 + 43
        n_____A(x1,x2) = max{35, x1 + 18, x2}
        U51#_A(x1,x2) = max{x1 + 33, x2 + 43}
        isNeList_A(x1) = x1 + 9
        activate_A(x1) = x1
        tt_A = 6
        isList#_A(x1) = x1 + 43
        U21#_A(x1,x2) = max{x1 - 29, x2 + 43}
        isList_A(x1) = x1 + 28
        U41#_A(x1,x2) = max{x1 + 6, x2 + 43}
        U22_A(x1) = max{27, x1 - 1}
        U42_A(x1) = max{7, x1 - 33}
        U52_A(x1) = 7
        ___A(x1,x2) = max{35, x1 + 18, x2}
        nil_A = 7
        U11_A(x1) = max{7, x1 + 1}
        U21_A(x1,x2) = max{x1 - 29, x2 + 28}
        U31_A(x1) = max{7, x1 + 1}
        U41_A(x1,x2) = max{x1 - 29, x2 + 8}
        U51_A(x1,x2) = max{19, x1}
        isQid_A(x1) = max{7, x1 + 1}
        n__a_A = 7
        n__e_A = 7
        n__i_A = 7
        n__o_A = 7
        n__u_A = 7
        n__nil_A = 7
        a_A = 7
        e_A = 7
        i_A = 7
        o_A = 7
        u_A = 7
  
    precedence:
    
      tt = U11 = U41 > activate > isNeList# = U51# = isList# = U21# = U41# > n____ = __ > isNeList > U42 > U52 > U31 > isList > U22 = U21 > nil > U51 = isQid = n__nil > n__e = n__i = n__u = a = e = i = o = u > n__a = n__o
    
    partial status:
  
      pi(isNeList#) = []
      pi(n____) = [1, 2]
      pi(U51#) = []
      pi(isNeList) = [1]
      pi(activate) = [1]
      pi(tt) = []
      pi(isList#) = []
      pi(U21#) = []
      pi(isList) = [1]
      pi(U41#) = []
      pi(U22) = []
      pi(U42) = []
      pi(U52) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(U11) = []
      pi(U21) = []
      pi(U31) = [1]
      pi(U41) = []
      pi(U51) = [1]
      pi(isQid) = [1]
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(n____(V1,V2)) -> isList#(activate(V1))
p4: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p5: U21#(tt(),V2) -> isList#(activate(V2))
p6: isList#(V) -> isNeList#(activate(V))
p7: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p8: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))
p9: U41#(tt(),V2) -> isNeList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: 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: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(V) -> isNeList#(activate(V))
p4: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))
p5: U41#(tt(),V2) -> isNeList#(activate(V2))
p6: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p7: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p8: U21#(tt(),V2) -> isList#(activate(V2))
p9: isList#(n____(V1,V2)) -> isList#(activate(V1))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        isNeList#_A(x1) = x1 + 8
        n_____A(x1,x2) = max{x1 + 7, x2}
        U51#_A(x1,x2) = max{x1 - 25, x2 + 8}
        isNeList_A(x1) = max{24, x1 + 19}
        activate_A(x1) = max{4, x1}
        tt_A = 38
        isList#_A(x1) = max{12, x1 + 8}
        U41#_A(x1,x2) = max{x1 - 26, x2 + 8}
        isList_A(x1) = max{38, x1 + 16}
        U21#_A(x1,x2) = max{12, x2 + 8}
        U22_A(x1) = max{6, x1}
        U42_A(x1) = max{1, x1}
        U52_A(x1) = max{17, x1 + 1}
        ___A(x1,x2) = max{x1 + 7, x2}
        nil_A = 4
        U11_A(x1) = 38
        U21_A(x1,x2) = max{x1, x2 + 16}
        U31_A(x1) = x1 + 1
        U41_A(x1,x2) = max{25, x2 + 19}
        U51_A(x1,x2) = max{x1 + 2, x2 + 18}
        isQid_A(x1) = x1 + 16
        n__a_A = 39
        n__e_A = 23
        n__i_A = 23
        n__o_A = 39
        n__u_A = 23
        n__nil_A = 3
        a_A = 39
        e_A = 23
        i_A = 23
        o_A = 39
        u_A = 23
  
    precedence:
    
      isNeList = U42 = U41 > activate > __ > isNeList# = U51# = isList# = U41# = isList = U21# = U22 = U21 = U31 = o > n__o > n____ = U11 = U51 > tt = U52 = isQid > nil = n__e = n__i = e = i > n__a = n__u = a = u > n__nil
    
    partial status:
  
      pi(isNeList#) = []
      pi(n____) = [2]
      pi(U51#) = []
      pi(isNeList) = [1]
      pi(activate) = [1]
      pi(tt) = []
      pi(isList#) = []
      pi(U41#) = []
      pi(isList) = []
      pi(U21#) = []
      pi(U22) = []
      pi(U42) = []
      pi(U52) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(U11) = []
      pi(U21) = []
      pi(U31) = []
      pi(U41) = []
      pi(U51) = []
      pi(isQid) = [1]
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p9

We remove them from the problem.

-- SCC decomposition.

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

p1: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(V) -> isNeList#(activate(V))
p4: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))
p5: U41#(tt(),V2) -> isNeList#(activate(V2))
p6: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p7: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p8: U21#(tt(),V2) -> isList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p4: U21#(tt(),V2) -> isList#(activate(V2))
p5: isList#(V) -> isNeList#(activate(V))
p6: isNeList#(n____(V1,V2)) -> isNeList#(activate(V1))
p7: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))
p8: U41#(tt(),V2) -> isNeList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        isNeList#_A(x1) = max{1, x1 - 2}
        n_____A(x1,x2) = max{x1 + 23, x2}
        U51#_A(x1,x2) = max{21, x1 + 1, x2 - 2}
        isNeList_A(x1) = x1 + 20
        activate_A(x1) = x1
        tt_A = 7
        isList#_A(x1) = max{1, x1 - 2}
        U21#_A(x1,x2) = max{2, x1 - 52, x2 - 2}
        isList_A(x1) = max{49, x1 + 44}
        U41#_A(x1,x2) = max{21, x2 - 2}
        U22_A(x1) = max{24, x1 - 45}
        U42_A(x1) = max{19, x1 - 11}
        U52_A(x1) = max{19, x1 - 30}
        ___A(x1,x2) = max{x1 + 23, x2}
        nil_A = 1
        U11_A(x1) = x1 + 23
        U21_A(x1,x2) = max{24, x1 - 6, x2 - 1}
        U31_A(x1) = max{19, x1 - 1}
        U41_A(x1,x2) = max{25, x1 - 25, x2 + 20}
        U51_A(x1,x2) = max{x1 + 12, x2 + 19}
        isQid_A(x1) = max{21, x1 - 1}
        n__a_A = 1
        n__e_A = 9
        n__i_A = 9
        n__o_A = 1
        n__u_A = 6
        n__nil_A = 1
        a_A = 1
        e_A = 9
        i_A = 9
        o_A = 1
        u_A = 6
  
    precedence:
    
      isNeList# = n____ = U51# = isNeList = activate = tt = isList# = U21# = isList = U41# = U22 = U42 = U52 = __ = nil = U11 = U21 = U31 = U41 = U51 = isQid = n__a = n__e = n__i = n__o = n__u = n__nil = a = e = i = o = u
    
    partial status:
  
      pi(isNeList#) = []
      pi(n____) = [1, 2]
      pi(U51#) = []
      pi(isNeList) = [1]
      pi(activate) = [1]
      pi(tt) = []
      pi(isList#) = []
      pi(U21#) = []
      pi(isList) = []
      pi(U41#) = []
      pi(U22) = []
      pi(U42) = []
      pi(U52) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(U11) = []
      pi(U21) = []
      pi(U31) = []
      pi(U41) = []
      pi(U51) = [1, 2]
      pi(isQid) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(n__nil) = []
      pi(a) = []
      pi(e) = []
      pi(i) = []
      pi(o) = []
      pi(u) = []

The next rules are strictly ordered:

  p6

We remove them from the problem.

-- SCC decomposition.

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

p1: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p4: U21#(tt(),V2) -> isList#(activate(V2))
p5: isList#(V) -> isNeList#(activate(V))
p6: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))
p7: U41#(tt(),V2) -> isNeList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The estimated dependency graph contains the following SCCs:

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


-- Reduction pair.

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

p1: isNeList#(n____(V1,V2)) -> U51#(isNeList(activate(V1)),activate(V2))
p2: U51#(tt(),V2) -> isList#(activate(V2))
p3: isList#(V) -> isNeList#(activate(V))
p4: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))
p5: U41#(tt(),V2) -> isNeList#(activate(V2))
p6: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p7: U21#(tt(),V2) -> isList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        isNeList#_A(x1) = max{5, x1}
        n_____A(x1,x2) = max{x1 + 48, x2}
        U51#_A(x1,x2) = max{5, x1, x2}
        isNeList_A(x1) = x1 + 8
        activate_A(x1) = max{5, x1}
        tt_A = 2
        isList#_A(x1) = max{5, x1}
        U41#_A(x1,x2) = max{6, x1, x2}
        isList_A(x1) = x1 + 30
        U21#_A(x1,x2) = max{48, x1 + 13, x2}
        U22_A(x1) = 49
        U42_A(x1) = max{1, x1}
        U52_A(x1) = max{3, x1 - 48}
        ___A(x1,x2) = max{x1 + 48, x2}
        nil_A = 1
        U11_A(x1) = 30
        U21_A(x1,x2) = max{49, x1 - 36}
        U31_A(x1) = max{1, x1}
        U41_A(x1,x2) = max{x1 + 12, x2 + 8}
        U51_A(x1,x2) = max{x1 - 14, x2 + 8}
        isQid_A(x1) = x1 + 2
        n__a_A = 3
        n__e_A = 1
        n__i_A = 3
        n__o_A = 3
        n__u_A = 1
        n__nil_A = 1
        a_A = 4
        e_A = 4
        i_A = 4
        o_A = 4
        u_A = 2
  
    precedence:
    
      n____ = isNeList = isList = __ = U11 > U52 = U51 > nil = n__nil > U51# = tt = U41# = U21# = U42 = U31 = U41 = isQid > isList# > isNeList# = activate = U22 = U21 = n__a = a = e = i > u > n__e = n__i = n__o = n__u = o
    
    partial status:
  
      pi(isNeList#) = [1]
      pi(n____) = [1, 2]
      pi(U51#) = [1, 2]
      pi(isNeList) = [1]
      pi(activate) = [1]
      pi(tt) = []
      pi(isList#) = [1]
      pi(U41#) = [1, 2]
      pi(isList) = []
      pi(U21#) = [2]
      pi(U22) = []
      pi(U42) = []
      pi(U52) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(U11) = []
      pi(U21) = []
      pi(U31) = [1]
      pi(U41) = []
      pi(U51) = [2]
      pi(isQid) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      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: U51#(tt(),V2) -> isList#(activate(V2))
p2: isList#(V) -> isNeList#(activate(V))
p3: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))
p4: U41#(tt(),V2) -> isNeList#(activate(V2))
p5: isList#(n____(V1,V2)) -> U21#(isList(activate(V1)),activate(V2))
p6: U21#(tt(),V2) -> isList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  {p5, p6}
  {p3, p4}


-- Reduction pair.

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

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

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        U21#_A(x1,x2) = max{x1 + 1, x2}
        tt_A = 6
        isList#_A(x1) = max{1, x1}
        activate_A(x1) = x1
        n_____A(x1,x2) = max{x1 + 8, x2}
        isList_A(x1) = x1 + 7
        U42_A(x1) = 11
        U52_A(x1) = max{7, x1 - 9}
        U22_A(x1) = max{7, x1 - 8}
        U31_A(x1) = max{7, x1 - 4}
        U41_A(x1,x2) = max{20, x1 - 8, x2 + 12}
        isNeList_A(x1) = x1 + 12
        U51_A(x1,x2) = max{9, x1 - 1, x2 - 1}
        isQid_A(x1) = x1 + 13
        n__a_A = 7
        n__e_A = 1
        n__i_A = 1
        n__o_A = 7
        n__u_A = 7
        ___A(x1,x2) = max{x1 + 8, x2}
        nil_A = 1
        U11_A(x1) = max{7, x1 - 5}
        U21_A(x1,x2) = max{9, x1 - 1, x2}
        n__nil_A = 1
        a_A = 7
        e_A = 1
        i_A = 1
        o_A = 7
        u_A = 7
  
    precedence:
    
      U52 = U22 = U31 > U51 = n__u = u > U42 = isQid > tt = n____ = isList = U41 = isNeList = __ > U21# > activate = n__o = o > n__a = nil = U11 = U21 = a > isList# = n__e = n__i = n__nil = e = i
    
    partial status:
  
      pi(U21#) = [1, 2]
      pi(tt) = []
      pi(isList#) = [1]
      pi(activate) = [1]
      pi(n____) = [1, 2]
      pi(isList) = []
      pi(U42) = []
      pi(U52) = []
      pi(U22) = []
      pi(U31) = []
      pi(U41) = []
      pi(isNeList) = [1]
      pi(U51) = []
      pi(isQid) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(U11) = []
      pi(U21) = []
      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: U21#(tt(),V2) -> isList#(activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  (no SCCs)

-- Reduction pair.

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

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

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r16, r17, r18, r19, r20, r21, r26, r27, r28, r29, r30, r31, r32, r33, r34, r35, r36, r37, r38, r39, r40, r41, r42, r43, r44, r45

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        isNeList#_A(x1) = x1
        n_____A(x1,x2) = max{x1 + 30, x2}
        U41#_A(x1,x2) = max{5, x1 + 4, x2}
        isList_A(x1) = max{2, x1 - 1}
        activate_A(x1) = max{5, x1}
        tt_A = 0
        U42_A(x1) = 0
        U52_A(x1) = x1 + 2
        U22_A(x1) = 1
        U31_A(x1) = max{21, x1 - 7}
        U41_A(x1,x2) = max{36, x1 + 32}
        isNeList_A(x1) = max{21, x1 + 17}
        U51_A(x1,x2) = max{31, x1 + 14, x2 + 5}
        isQid_A(x1) = max{23, x1 + 18}
        n__a_A = 6
        n__e_A = 6
        n__i_A = 6
        n__o_A = 6
        n__u_A = 1
        ___A(x1,x2) = max{x1 + 30, x2}
        nil_A = 6
        U11_A(x1) = max{2, x1 - 20}
        U21_A(x1,x2) = max{x1 + 25, x2 - 7}
        n__nil_A = 6
        a_A = 6
        e_A = 6
        i_A = 6
        o_A = 6
        u_A = 2
  
    precedence:
    
      n____ = __ = u > U41# > isNeList# = isList = activate = tt = U42 = U52 = U22 = U31 = U41 = isNeList = U51 = isQid = n__a = n__e = n__i = n__o = n__u = nil = U11 = U21 = n__nil = a = e = i = o
    
    partial status:
  
      pi(isNeList#) = [1]
      pi(n____) = [1, 2]
      pi(U41#) = [1, 2]
      pi(isList) = []
      pi(activate) = [1]
      pi(tt) = []
      pi(U42) = []
      pi(U52) = []
      pi(U22) = []
      pi(U31) = []
      pi(U41) = []
      pi(isNeList) = []
      pi(U51) = []
      pi(isQid) = []
      pi(n__a) = []
      pi(n__e) = []
      pi(n__i) = []
      pi(n__o) = []
      pi(n__u) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(U11) = []
      pi(U21) = []
      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: isNeList#(n____(V1,V2)) -> U41#(isList(activate(V1)),activate(V2))

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The estimated dependency graph contains the following SCCs:

  (no SCCs)

-- 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: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  r1, r2, r3, r32

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        __#_A(x1,x2) = max{0, x1 - 5}
        ___A(x1,x2) = max{6, x1 + 4, x2}
        nil_A = 0
        n_____A(x1,x2) = max{x1 + 1, x2}
  
    precedence:
    
      __# = __ = nil = n____
    
    partial status:
  
      pi(__#) = []
      pi(__) = [1, 2]
      pi(nil) = []
      pi(n____) = [1]

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: __#(__(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: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: 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) -> __#(Y,Z)

and R consists of:

r1: __(__(X,Y),Z) -> __(X,__(Y,Z))
r2: __(X,nil()) -> X
r3: __(nil(),X) -> X
r4: U11(tt()) -> tt()
r5: U21(tt(),V2) -> U22(isList(activate(V2)))
r6: U22(tt()) -> tt()
r7: U31(tt()) -> tt()
r8: U41(tt(),V2) -> U42(isNeList(activate(V2)))
r9: U42(tt()) -> tt()
r10: U51(tt(),V2) -> U52(isList(activate(V2)))
r11: U52(tt()) -> tt()
r12: U61(tt()) -> tt()
r13: U71(tt(),P) -> U72(isPal(activate(P)))
r14: U72(tt()) -> tt()
r15: U81(tt()) -> tt()
r16: isList(V) -> U11(isNeList(activate(V)))
r17: isList(n__nil()) -> tt()
r18: isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
r19: isNeList(V) -> U31(isQid(activate(V)))
r20: isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
r21: isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
r22: isNePal(V) -> U61(isQid(activate(V)))
r23: isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
r24: isPal(V) -> U81(isNePal(activate(V)))
r25: isPal(n__nil()) -> tt()
r26: isQid(n__a()) -> tt()
r27: isQid(n__e()) -> tt()
r28: isQid(n__i()) -> tt()
r29: isQid(n__o()) -> tt()
r30: isQid(n__u()) -> tt()
r31: nil() -> n__nil()
r32: __(X1,X2) -> n____(X1,X2)
r33: a() -> n__a()
r34: e() -> n__e()
r35: i() -> n__i()
r36: o() -> n__o()
r37: u() -> n__u()
r38: activate(n__nil()) -> nil()
r39: activate(n____(X1,X2)) -> __(X1,X2)
r40: activate(n__a()) -> a()
r41: activate(n__e()) -> e()
r42: activate(n__i()) -> i()
r43: activate(n__o()) -> o()
r44: activate(n__u()) -> u()
r45: activate(X) -> X

The set of usable rules consists of

  (no rules)

Take the reduction pair:

  weighted path order
  
    base order:
  
      max/plus interpretations on natural numbers:
      
        __#_A(x1,x2) = max{x1 + 1, x2 + 1}
        ___A(x1,x2) = x2
  
    precedence:
    
      __# = __
    
    partial status:
  
      pi(__#) = [1]
      pi(__) = [2]

The next rules are strictly ordered:

  p1

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