- : unit = ()
- : unit = ()
h : heuristic = <heuristic>
- : unit = ()
APPLY CRITERIA (Marked dependency pairs)

TRS termination of:
[1] __(__(X,Y),Z) -> __(X,__(Y,Z))
[2] __(X,nil) -> X
[3] __(nil,X) -> X
[4] U11(tt,V) -> U12(isPalListKind(activate(V)),activate(V))
[5] U12(tt,V) -> U13(isNeList(activate(V)))
[6] U13(tt) -> tt
[7] U21(tt,V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
[8] U22(tt,V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
[9] U23(tt,V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
[10] U24(tt,V1,V2) -> U25(isList(activate(V1)),activate(V2))
[11] U25(tt,V2) -> U26(isList(activate(V2)))
[12] U26(tt) -> tt
[13] U31(tt,V) -> U32(isPalListKind(activate(V)),activate(V))
[14] U32(tt,V) -> U33(isQid(activate(V)))
[15] U33(tt) -> tt
[16] U41(tt,V1,V2) ->
 U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
[17] U42(tt,V1,V2) ->
 U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
[18] U43(tt,V1,V2) ->
 U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
[19] U44(tt,V1,V2) -> U45(isList(activate(V1)),activate(V2))
[20] U45(tt,V2) -> U46(isNeList(activate(V2)))
[21] U46(tt) -> tt
[22] U51(tt,V1,V2) ->
 U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
[23] U52(tt,V1,V2) ->
 U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
[24] U53(tt,V1,V2) ->
 U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
[25] U54(tt,V1,V2) -> U55(isNeList(activate(V1)),activate(V2))
[26] U55(tt,V2) -> U56(isList(activate(V2)))
[27] U56(tt) -> tt
[28] U61(tt,V) -> U62(isPalListKind(activate(V)),activate(V))
[29] U62(tt,V) -> U63(isQid(activate(V)))
[30] U63(tt) -> tt
[31] U71(tt,I,P) -> U72(isPalListKind(activate(I)),activate(P))
[32] U72(tt,P) -> U73(isPal(activate(P)),activate(P))
[33] U73(tt,P) -> U74(isPalListKind(activate(P)))
[34] U74(tt) -> tt
[35] U81(tt,V) -> U82(isPalListKind(activate(V)),activate(V))
[36] U82(tt,V) -> U83(isNePal(activate(V)))
[37] U83(tt) -> tt
[38] U91(tt,V2) -> U92(isPalListKind(activate(V2)))
[39] U92(tt) -> tt
[40] isList(V) -> U11(isPalListKind(activate(V)),activate(V))
[41] isList(n__nil) -> tt
[42] isList(n____(V1,V2)) ->
 U21(isPalListKind(activate(V1)),activate(V1),activate(V2))
[43] isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
[44] isNeList(n____(V1,V2)) ->
 U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
[45] isNeList(n____(V1,V2)) ->
 U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
[46] isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
[47] isNePal(n____(I,__(P,I))) ->
 U71(isQid(activate(I)),activate(I),activate(P))
[48] isPal(V) -> U81(isPalListKind(activate(V)),activate(V))
[49] isPal(n__nil) -> tt
[50] isPalListKind(n__a) -> tt
[51] isPalListKind(n__e) -> tt
[52] isPalListKind(n__i) -> tt
[53] isPalListKind(n__nil) -> tt
[54] isPalListKind(n__o) -> tt
[55] isPalListKind(n__u) -> tt
[56] isPalListKind(n____(V1,V2)) ->
 U91(isPalListKind(activate(V1)),activate(V2))
[57] isQid(n__a) -> tt
[58] isQid(n__e) -> tt
[59] isQid(n__i) -> tt
[60] isQid(n__o) -> tt
[61] isQid(n__u) -> tt
[62] nil -> n__nil
[63] __(X1,X2) -> n____(X1,X2)
[64] a -> n__a
[65] e -> n__e
[66] i -> n__i
[67] o -> n__o
[68] u -> n__u
[69] activate(n__nil) -> nil
[70] activate(n____(X1,X2)) -> __(X1,X2)
[71] activate(n__a) -> a
[72] activate(n__e) -> e
[73] activate(n__i) -> i
[74] activate(n__o) -> o
[75] activate(n__u) -> u
[76] activate(X) -> X


Sub problem: 
guided: 

DP termination of:
<Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))>
<Marked___(__(X,Y),Z) , Marked___(Y,Z)>
<Marked_U11(tt,V) , Marked_U12(isPalListKind(activate(V)),activate(V))>
<Marked_U11(tt,V) , Marked_isPalListKind(activate(V))>
<Marked_U11(tt,V) , Marked_activate(V)>
<Marked_U11(tt,V) , Marked_activate(V)>
<Marked_U12(tt,V) , Marked_U13(isNeList(activate(V)))>
<Marked_U12(tt,V) , Marked_isNeList(activate(V))>
<Marked_U12(tt,V) , Marked_activate(V)>
<Marked_U21(tt,V1,V2) , Marked_U22(isPalListKind(activate(V1)),activate(V1),
                         activate(V2))>
<Marked_U21(tt,V1,V2) , Marked_isPalListKind(activate(V1))>
<Marked_U21(tt,V1,V2) , Marked_activate(V1)>
<Marked_U21(tt,V1,V2) , Marked_activate(V1)>
<Marked_U21(tt,V1,V2) , Marked_activate(V2)>
<Marked_U22(tt,V1,V2) , Marked_U23(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U22(tt,V1,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U22(tt,V1,V2) , Marked_activate(V2)>
<Marked_U22(tt,V1,V2) , Marked_activate(V1)>
<Marked_U22(tt,V1,V2) , Marked_activate(V2)>
<Marked_U23(tt,V1,V2) , Marked_U24(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U23(tt,V1,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U23(tt,V1,V2) , Marked_activate(V2)>
<Marked_U23(tt,V1,V2) , Marked_activate(V1)>
<Marked_U23(tt,V1,V2) , Marked_activate(V2)>
<Marked_U24(tt,V1,V2) , Marked_U25(isList(activate(V1)),activate(V2))>
<Marked_U24(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U24(tt,V1,V2) , Marked_activate(V1)>
<Marked_U24(tt,V1,V2) , Marked_activate(V2)>
<Marked_U25(tt,V2) , Marked_U26(isList(activate(V2)))>
<Marked_U25(tt,V2) , Marked_isList(activate(V2))>
<Marked_U25(tt,V2) , Marked_activate(V2)>
<Marked_U31(tt,V) , Marked_U32(isPalListKind(activate(V)),activate(V))>
<Marked_U31(tt,V) , Marked_isPalListKind(activate(V))>
<Marked_U31(tt,V) , Marked_activate(V)>
<Marked_U31(tt,V) , Marked_activate(V)>
<Marked_U32(tt,V) , Marked_U33(isQid(activate(V)))>
<Marked_U32(tt,V) , Marked_isQid(activate(V))>
<Marked_U32(tt,V) , Marked_activate(V)>
<Marked_U41(tt,V1,V2) , Marked_U42(isPalListKind(activate(V1)),activate(V1),
                         activate(V2))>
<Marked_U41(tt,V1,V2) , Marked_isPalListKind(activate(V1))>
<Marked_U41(tt,V1,V2) , Marked_activate(V1)>
<Marked_U41(tt,V1,V2) , Marked_activate(V1)>
<Marked_U41(tt,V1,V2) , Marked_activate(V2)>
<Marked_U42(tt,V1,V2) , Marked_U43(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U42(tt,V1,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U42(tt,V1,V2) , Marked_activate(V2)>
<Marked_U42(tt,V1,V2) , Marked_activate(V1)>
<Marked_U42(tt,V1,V2) , Marked_activate(V2)>
<Marked_U43(tt,V1,V2) , Marked_U44(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U43(tt,V1,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U43(tt,V1,V2) , Marked_activate(V2)>
<Marked_U43(tt,V1,V2) , Marked_activate(V1)>
<Marked_U43(tt,V1,V2) , Marked_activate(V2)>
<Marked_U44(tt,V1,V2) , Marked_U45(isList(activate(V1)),activate(V2))>
<Marked_U44(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U44(tt,V1,V2) , Marked_activate(V1)>
<Marked_U44(tt,V1,V2) , Marked_activate(V2)>
<Marked_U45(tt,V2) , Marked_U46(isNeList(activate(V2)))>
<Marked_U45(tt,V2) , Marked_isNeList(activate(V2))>
<Marked_U45(tt,V2) , Marked_activate(V2)>
<Marked_U51(tt,V1,V2) , Marked_U52(isPalListKind(activate(V1)),activate(V1),
                         activate(V2))>
<Marked_U51(tt,V1,V2) , Marked_isPalListKind(activate(V1))>
<Marked_U51(tt,V1,V2) , Marked_activate(V1)>
<Marked_U51(tt,V1,V2) , Marked_activate(V1)>
<Marked_U51(tt,V1,V2) , Marked_activate(V2)>
<Marked_U52(tt,V1,V2) , Marked_U53(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U52(tt,V1,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U52(tt,V1,V2) , Marked_activate(V2)>
<Marked_U52(tt,V1,V2) , Marked_activate(V1)>
<Marked_U52(tt,V1,V2) , Marked_activate(V2)>
<Marked_U53(tt,V1,V2) , Marked_U54(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U53(tt,V1,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U53(tt,V1,V2) , Marked_activate(V2)>
<Marked_U53(tt,V1,V2) , Marked_activate(V1)>
<Marked_U53(tt,V1,V2) , Marked_activate(V2)>
<Marked_U54(tt,V1,V2) , Marked_U55(isNeList(activate(V1)),activate(V2))>
<Marked_U54(tt,V1,V2) , Marked_isNeList(activate(V1))>
<Marked_U54(tt,V1,V2) , Marked_activate(V1)>
<Marked_U54(tt,V1,V2) , Marked_activate(V2)>
<Marked_U55(tt,V2) , Marked_U56(isList(activate(V2)))>
<Marked_U55(tt,V2) , Marked_isList(activate(V2))>
<Marked_U55(tt,V2) , Marked_activate(V2)>
<Marked_U61(tt,V) , Marked_U62(isPalListKind(activate(V)),activate(V))>
<Marked_U61(tt,V) , Marked_isPalListKind(activate(V))>
<Marked_U61(tt,V) , Marked_activate(V)>
<Marked_U61(tt,V) , Marked_activate(V)>
<Marked_U62(tt,V) , Marked_U63(isQid(activate(V)))>
<Marked_U62(tt,V) , Marked_isQid(activate(V))>
<Marked_U62(tt,V) , Marked_activate(V)>
<Marked_U71(tt,I,P) , Marked_U72(isPalListKind(activate(I)),activate(P))>
<Marked_U71(tt,I,P) , Marked_isPalListKind(activate(I))>
<Marked_U71(tt,I,P) , Marked_activate(I)>
<Marked_U71(tt,I,P) , Marked_activate(P)>
<Marked_U72(tt,P) , Marked_U73(isPal(activate(P)),activate(P))>
<Marked_U72(tt,P) , Marked_isPal(activate(P))>
<Marked_U72(tt,P) , Marked_activate(P)>
<Marked_U72(tt,P) , Marked_activate(P)>
<Marked_U73(tt,P) , Marked_U74(isPalListKind(activate(P)))>
<Marked_U73(tt,P) , Marked_isPalListKind(activate(P))>
<Marked_U73(tt,P) , Marked_activate(P)>
<Marked_U81(tt,V) , Marked_U82(isPalListKind(activate(V)),activate(V))>
<Marked_U81(tt,V) , Marked_isPalListKind(activate(V))>
<Marked_U81(tt,V) , Marked_activate(V)>
<Marked_U81(tt,V) , Marked_activate(V)>
<Marked_U82(tt,V) , Marked_U83(isNePal(activate(V)))>
<Marked_U82(tt,V) , Marked_isNePal(activate(V))>
<Marked_U82(tt,V) , Marked_activate(V)>
<Marked_U91(tt,V2) , Marked_U92(isPalListKind(activate(V2)))>
<Marked_U91(tt,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U91(tt,V2) , Marked_activate(V2)>
<Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
<Marked_isList(V) , Marked_isPalListKind(activate(V))>
<Marked_isList(V) , Marked_activate(V)>
<Marked_isList(V) , Marked_activate(V)>
<Marked_isList(n____(V1,V2)) , Marked_U21(isPalListKind(activate(V1)),
                                activate(V1),activate(V2))>
<Marked_isList(n____(V1,V2)) , Marked_isPalListKind(activate(V1))>
<Marked_isList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNeList(V) , Marked_U31(isPalListKind(activate(V)),activate(V))>
<Marked_isNeList(V) , Marked_isPalListKind(activate(V))>
<Marked_isNeList(V) , Marked_activate(V)>
<Marked_isNeList(V) , Marked_activate(V)>
<Marked_isNeList(n____(V1,V2)) , Marked_U41(isPalListKind(activate(V1)),
                                  activate(V1),activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_isPalListKind(activate(V1))>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNeList(n____(V1,V2)) , Marked_U51(isPalListKind(activate(V1)),
                                  activate(V1),activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_isPalListKind(activate(V1))>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNePal(V) , Marked_U61(isPalListKind(activate(V)),activate(V))>
<Marked_isNePal(V) , Marked_isPalListKind(activate(V))>
<Marked_isNePal(V) , Marked_activate(V)>
<Marked_isNePal(V) , Marked_activate(V)>
<Marked_isNePal(n____(I,__(P,I))) , Marked_U71(isQid(activate(I)),activate(I),
                                     activate(P))>
<Marked_isNePal(n____(I,__(P,I))) , Marked_isQid(activate(I))>
<Marked_isNePal(n____(I,__(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,__(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,__(P,I))) , Marked_activate(P)>
<Marked_isPal(V) , Marked_U81(isPalListKind(activate(V)),activate(V))>
<Marked_isPal(V) , Marked_isPalListKind(activate(V))>
<Marked_isPal(V) , Marked_activate(V)>
<Marked_isPal(V) , Marked_activate(V)>
<Marked_isPalListKind(n____(V1,V2)) , Marked_U91(isPalListKind(activate(V1)),
                                       activate(V2))>
<Marked_isPalListKind(n____(V1,V2)) , Marked_isPalListKind(activate(V1))>
<Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V2)>
<Marked_activate(n__nil) , Marked_nil>
<Marked_activate(n____(X1,X2)) , Marked___(X1,X2)>
<Marked_activate(n__a) , Marked_a>
<Marked_activate(n__e) , Marked_e>
<Marked_activate(n__i) , Marked_i>
<Marked_activate(n__o) , Marked_o>
<Marked_activate(n__u) , Marked_u>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 4 components:

{  <Marked_isNeList(n____(V1,V2)) , Marked_U51(isPalListKind(activate(V1)),
                                     activate(V1),activate(V2))> 
      --> <Marked_U51(tt,V1,V2) , Marked_U52(isPalListKind(activate(V1)),
                                   activate(V1),activate(V2))>
  <Marked_isNeList(n____(V1,V2)) , Marked_U41(isPalListKind(activate(V1)),
                                    activate(V1),activate(V2))> 
     --> <Marked_U41(tt,V1,V2) , Marked_U42(isPalListKind(activate(V1)),
                                  activate(V1),activate(V2))>
  <Marked_isList(n____(V1,V2)) , Marked_U21(isPalListKind(activate(V1)),
                                  activate(V1),activate(V2))> 
     --> <Marked_U21(tt,V1,V2) , Marked_U22(isPalListKind(activate(V1)),
                                  activate(V1),activate(V2))>
  <Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))> 
     --> <Marked_U11(tt,V) , Marked_U12(isPalListKind(activate(V)),activate(V))>
  <Marked_U55(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_U21(isPalListKind(activate(V1)),
                                         activate(V1),activate(V2))>
  <Marked_U55(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
  <Marked_U54(tt,V1,V2) , Marked_isNeList(activate(V1))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U51(isPalListKind(activate(V1)),
                                           activate(V1),activate(V2))>
  <Marked_U54(tt,V1,V2) , Marked_isNeList(activate(V1))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U41(isPalListKind(activate(V1)),
                                           activate(V1),activate(V2))>
  <Marked_U54(tt,V1,V2) , Marked_U55(isNeList(activate(V1)),activate(V2))> 
     --> <Marked_U55(tt,V2) , Marked_isList(activate(V2))>
  <Marked_U53(tt,V1,V2) , Marked_U54(isPalListKind(activate(V2)),activate(V1),
                           activate(V2))> 
     --> <Marked_U54(tt,V1,V2) , Marked_isNeList(activate(V1))>
  <Marked_U53(tt,V1,V2) , Marked_U54(isPalListKind(activate(V2)),activate(V1),
                           activate(V2))> 
     --> <Marked_U54(tt,V1,V2) , Marked_U55(isNeList(activate(V1)),
                                  activate(V2))>
  <Marked_U52(tt,V1,V2) , Marked_U53(isPalListKind(activate(V2)),activate(V1),
                           activate(V2))> 
     --> <Marked_U53(tt,V1,V2) , Marked_U54(isPalListKind(activate(V2)),
                                  activate(V1),activate(V2))>
  <Marked_U51(tt,V1,V2) , Marked_U52(isPalListKind(activate(V1)),activate(V1),
                           activate(V2))> 
     --> <Marked_U52(tt,V1,V2) , Marked_U53(isPalListKind(activate(V2)),
                                  activate(V1),activate(V2))>
  <Marked_U45(tt,V2) , Marked_isNeList(activate(V2))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U51(isPalListKind(activate(V1)),
                                           activate(V1),activate(V2))>
  <Marked_U45(tt,V2) , Marked_isNeList(activate(V2))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U41(isPalListKind(activate(V1)),
                                           activate(V1),activate(V2))>
  <Marked_U44(tt,V1,V2) , Marked_isList(activate(V1))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_U21(isPalListKind(activate(V1)),
                                         activate(V1),activate(V2))>
  <Marked_U44(tt,V1,V2) , Marked_isList(activate(V1))> 
     --> <Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
  <Marked_U44(tt,V1,V2) , Marked_U45(isList(activate(V1)),activate(V2))> 
     --> <Marked_U45(tt,V2) , Marked_isNeList(activate(V2))>
  <Marked_U43(tt,V1,V2) , Marked_U44(isPalListKind(activate(V2)),activate(V1),
                           activate(V2))> 
     --> <Marked_U44(tt,V1,V2) , Marked_isList(activate(V1))>
  <Marked_U43(tt,V1,V2) , Marked_U44(isPalListKind(activate(V2)),activate(V1),
                           activate(V2))> 
     --> <Marked_U44(tt,V1,V2) , Marked_U45(isList(activate(V1)),activate(V2))>
  <Marked_U42(tt,V1,V2) , Marked_U43(isPalListKind(activate(V2)),activate(V1),
                           activate(V2))> 
     --> <Marked_U43(tt,V1,V2) , Marked_U44(isPalListKind(activate(V2)),
                                  activate(V1),activate(V2))>
  <Marked_U41(tt,V1,V2) , Marked_U42(isPalListKind(activate(V1)),activate(V1),
                           activate(V2))> 
     --> <Marked_U42(tt,V1,V2) , Marked_U43(isPalListKind(activate(V2)),
                                  activate(V1),activate(V2))>
  <Marked_U25(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_U21(isPalListKind(activate(V1)),
                                         activate(V1),activate(V2))>
  <Marked_U25(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
  <Marked_U24(tt,V1,V2) , Marked_isList(activate(V1))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_U21(isPalListKind(activate(V1)),
                                         activate(V1),activate(V2))>
  <Marked_U24(tt,V1,V2) , Marked_isList(activate(V1))> 
     --> <Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
  <Marked_U24(tt,V1,V2) , Marked_U25(isList(activate(V1)),activate(V2))> 
     --> <Marked_U25(tt,V2) , Marked_isList(activate(V2))>
  <Marked_U23(tt,V1,V2) , Marked_U24(isPalListKind(activate(V2)),activate(V1),
                           activate(V2))> 
     --> <Marked_U24(tt,V1,V2) , Marked_isList(activate(V1))>
  <Marked_U23(tt,V1,V2) , Marked_U24(isPalListKind(activate(V2)),activate(V1),
                           activate(V2))> 
     --> <Marked_U24(tt,V1,V2) , Marked_U25(isList(activate(V1)),activate(V2))>
  <Marked_U22(tt,V1,V2) , Marked_U23(isPalListKind(activate(V2)),activate(V1),
                           activate(V2))> 
     --> <Marked_U23(tt,V1,V2) , Marked_U24(isPalListKind(activate(V2)),
                                  activate(V1),activate(V2))>
  <Marked_U21(tt,V1,V2) , Marked_U22(isPalListKind(activate(V1)),activate(V1),
                           activate(V2))> 
     --> <Marked_U22(tt,V1,V2) , Marked_U23(isPalListKind(activate(V2)),
                                  activate(V1),activate(V2))>
  <Marked_U12(tt,V) , Marked_isNeList(activate(V))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U51(isPalListKind(activate(V1)),
                                           activate(V1),activate(V2))>
  <Marked_U12(tt,V) , Marked_isNeList(activate(V))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U41(isPalListKind(activate(V1)),
                                           activate(V1),activate(V2))>
  <Marked_U11(tt,V) , Marked_U12(isPalListKind(activate(V)),activate(V))> 
     --> <Marked_U12(tt,V) , Marked_isNeList(activate(V))>
}

{  <Marked_isPal(V) , Marked_U81(isPalListKind(activate(V)),activate(V))> 
      --> <Marked_U81(tt,V) , Marked_U82(isPalListKind(activate(V)),
                               activate(V))>
  <Marked_isNePal(n____(I,__(P,I))) , Marked_U71(isQid(activate(I)),
                                       activate(I),activate(P))> 
     --> <Marked_U71(tt,I,P) , Marked_U72(isPalListKind(activate(I)),
                                activate(P))>
  <Marked_U82(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(n____(I,__(P,I))) , Marked_U71(isQid(activate(I)),
                                              activate(I),activate(P))>
  <Marked_U81(tt,V) , Marked_U82(isPalListKind(activate(V)),activate(V))> 
     --> <Marked_U82(tt,V) , Marked_isNePal(activate(V))>
  <Marked_U72(tt,P) , Marked_isPal(activate(P))> 
     --> <Marked_isPal(V) , Marked_U81(isPalListKind(activate(V)),activate(V))>
  <Marked_U71(tt,I,P) , Marked_U72(isPalListKind(activate(I)),activate(P))> 
     --> <Marked_U72(tt,P) , Marked_isPal(activate(P))>
}

{  <Marked_isPalListKind(n____(V1,V2)) , Marked_isPalListKind(activate(V1))> 
      --> <Marked_isPalListKind(n____(V1,V2)) , Marked_isPalListKind(
                                                 activate(V1))>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_isPalListKind(activate(V1))> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_U91(isPalListKind(
                                                           activate(V1)),
                                                activate(V2))>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_U91(isPalListKind(activate(V1)),
                                         activate(V2))> 
     --> <Marked_U91(tt,V2) , Marked_isPalListKind(activate(V2))>
  <Marked_U91(tt,V2) , Marked_isPalListKind(activate(V2))> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_isPalListKind(activate(
                                                                    V1))>
  <Marked_U91(tt,V2) , Marked_isPalListKind(activate(V2))> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_U91(isPalListKind(
                                                           activate(V1)),
                                                activate(V2))>
}

{  <Marked___(__(X,Y),Z) , Marked___(Y,Z)> 
      --> <Marked___(__(X,Y),Z) , Marked___(Y,Z)>
  <Marked___(__(X,Y),Z) , Marked___(Y,Z)> 
     --> <Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))>
  <Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))> 
     --> <Marked___(__(X,Y),Z) , Marked___(Y,Z)>
  <Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))> 
     --> <Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))>
}
APPLY CRITERIA (Subterm criterion)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  __(__(X,Y),Z) >= __(X,__(Y,Z)) ;
  __(nil,X) >= X ;
  __(X,nil) >= X ;
  __(X1,X2) >= n____(X1,X2) ;
  nil >= n__nil ;
  U12(tt,V) >= U13(isNeList(activate(V))) ;
  isPalListKind(n__nil) >= tt ;
  isPalListKind(n____(V1,V2)) >= U91(isPalListKind(activate(V1)),activate(V2)) ;
  isPalListKind(n__a) >= tt ;
  isPalListKind(n__e) >= tt ;
  isPalListKind(n__i) >= tt ;
  isPalListKind(n__o) >= tt ;
  isPalListKind(n__u) >= tt ;
  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 ;
  U11(tt,V) >= U12(isPalListKind(activate(V)),activate(V)) ;
  U13(tt) >= tt ;
  isNeList(n____(V1,V2)) >= U41(isPalListKind(activate(V1)),activate(V1),
                             activate(V2)) ;
  isNeList(n____(V1,V2)) >= U51(isPalListKind(activate(V1)),activate(V1),
                             activate(V2)) ;
  isNeList(V) >= U31(isPalListKind(activate(V)),activate(V)) ;
  U22(tt,V1,V2) >= U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U21(tt,V1,V2) >= U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) ;
  U23(tt,V1,V2) >= U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U24(tt,V1,V2) >= U25(isList(activate(V1)),activate(V2)) ;
  U25(tt,V2) >= U26(isList(activate(V2))) ;
  isList(n__nil) >= tt ;
  isList(n____(V1,V2)) >= U21(isPalListKind(activate(V1)),activate(V1),
                           activate(V2)) ;
  isList(V) >= U11(isPalListKind(activate(V)),activate(V)) ;
  U26(tt) >= tt ;
  U32(tt,V) >= U33(isQid(activate(V))) ;
  U31(tt,V) >= U32(isPalListKind(activate(V)),activate(V)) ;
  U33(tt) >= tt ;
  isQid(n__a) >= tt ;
  isQid(n__e) >= tt ;
  isQid(n__i) >= tt ;
  isQid(n__o) >= tt ;
  isQid(n__u) >= tt ;
  U42(tt,V1,V2) >= U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U41(tt,V1,V2) >= U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) ;
  U43(tt,V1,V2) >= U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U44(tt,V1,V2) >= U45(isList(activate(V1)),activate(V2)) ;
  U45(tt,V2) >= U46(isNeList(activate(V2))) ;
  U46(tt) >= tt ;
  U52(tt,V1,V2) >= U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U51(tt,V1,V2) >= U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) ;
  U53(tt,V1,V2) >= U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U54(tt,V1,V2) >= U55(isNeList(activate(V1)),activate(V2)) ;
  U55(tt,V2) >= U56(isList(activate(V2))) ;
  U56(tt) >= tt ;
  U62(tt,V) >= U63(isQid(activate(V))) ;
  U61(tt,V) >= U62(isPalListKind(activate(V)),activate(V)) ;
  U63(tt) >= tt ;
  U72(tt,P) >= U73(isPal(activate(P)),activate(P)) ;
  U71(tt,I,P) >= U72(isPalListKind(activate(I)),activate(P)) ;
  U73(tt,P) >= U74(isPalListKind(activate(P))) ;
  isPal(n__nil) >= tt ;
  isPal(V) >= U81(isPalListKind(activate(V)),activate(V)) ;
  U74(tt) >= tt ;
  U82(tt,V) >= U83(isNePal(activate(V))) ;
  U81(tt,V) >= U82(isPalListKind(activate(V)),activate(V)) ;
  U83(tt) >= tt ;
  isNePal(n____(I,__(P,I))) >= U71(isQid(activate(I)),activate(I),activate(P)) ;
  isNePal(V) >= U61(isPalListKind(activate(V)),activate(V)) ;
  U92(tt) >= tt ;
  U91(tt,V2) >= U92(isPalListKind(activate(V2))) ;
  a >= n__a ;
  e >= n__e ;
  i >= n__i ;
  o >= n__o ;
  u >= n__u ;
  Marked_isNeList(n____(V1,V2)) >= Marked_U51(isPalListKind(activate(V1)),
                                    activate(V1),activate(V2)) ;
  Marked_isNeList(n____(V1,V2)) >= Marked_U41(isPalListKind(activate(V1)),
                                    activate(V1),activate(V2)) ;
  Marked_U51(tt,V1,V2) >= Marked_U52(isPalListKind(activate(V1)),activate(V1),
                           activate(V2)) ;
  Marked_U41(tt,V1,V2) >= Marked_U42(isPalListKind(activate(V1)),activate(V1),
                           activate(V2)) ;
  Marked_isList(n____(V1,V2)) >= Marked_U21(isPalListKind(activate(V1)),
                                  activate(V1),activate(V2)) ;
  Marked_isList(V) >= Marked_U11(isPalListKind(activate(V)),activate(V)) ;
  Marked_U21(tt,V1,V2) >= Marked_U22(isPalListKind(activate(V1)),activate(V1),
                           activate(V2)) ;
  Marked_U11(tt,V) >= Marked_U12(isPalListKind(activate(V)),activate(V)) ;
  Marked_U55(tt,V2) >= Marked_isList(activate(V2)) ;
  Marked_U54(tt,V1,V2) >= Marked_isNeList(activate(V1)) ;
  Marked_U54(tt,V1,V2) >= Marked_U55(isNeList(activate(V1)),activate(V2)) ;
  Marked_U53(tt,V1,V2) >= Marked_U54(isPalListKind(activate(V2)),activate(V1),
                           activate(V2)) ;
  Marked_U52(tt,V1,V2) >= Marked_U53(isPalListKind(activate(V2)),activate(V1),
                           activate(V2)) ;
  Marked_U45(tt,V2) >= Marked_isNeList(activate(V2)) ;
  Marked_U44(tt,V1,V2) >= Marked_isList(activate(V1)) ;
  Marked_U44(tt,V1,V2) >= Marked_U45(isList(activate(V1)),activate(V2)) ;
  Marked_U43(tt,V1,V2) >= Marked_U44(isPalListKind(activate(V2)),activate(V1),
                           activate(V2)) ;
  Marked_U42(tt,V1,V2) >= Marked_U43(isPalListKind(activate(V2)),activate(V1),
                           activate(V2)) ;
  Marked_U25(tt,V2) >= Marked_isList(activate(V2)) ;
  Marked_U24(tt,V1,V2) >= Marked_isList(activate(V1)) ;
  Marked_U24(tt,V1,V2) >= Marked_U25(isList(activate(V1)),activate(V2)) ;
  Marked_U23(tt,V1,V2) >= Marked_U24(isPalListKind(activate(V2)),activate(V1),
                           activate(V2)) ;
  Marked_U22(tt,V1,V2) >= Marked_U23(isPalListKind(activate(V2)),activate(V1),
                           activate(V2)) ;
  Marked_U12(tt,V) >= Marked_isNeList(activate(V)) ;
 }
 + Disjunctions:{ 
{
  Marked_isNeList(n____(V1,V2)) > Marked_U51(isPalListKind(activate(V1)),
                                   activate(V1),activate(V2)) ;
 }
{
  Marked_isNeList(n____(V1,V2)) > Marked_U41(isPalListKind(activate(V1)),
                                   activate(V1),activate(V2)) ;
 }
{
  Marked_U51(tt,V1,V2) > Marked_U52(isPalListKind(activate(V1)),activate(V1),
                          activate(V2)) ;
 }
{
  Marked_U41(tt,V1,V2) > Marked_U42(isPalListKind(activate(V1)),activate(V1),
                          activate(V2)) ;
 }
{
  Marked_isList(n____(V1,V2)) > Marked_U21(isPalListKind(activate(V1)),
                                 activate(V1),activate(V2)) ;
 }
{
  Marked_isList(V) > Marked_U11(isPalListKind(activate(V)),activate(V)) ;
 }
{
  Marked_U21(tt,V1,V2) > Marked_U22(isPalListKind(activate(V1)),activate(V1),
                          activate(V2)) ;
 }
{
  Marked_U11(tt,V) > Marked_U12(isPalListKind(activate(V)),activate(V)) ;
 }
{
  Marked_U55(tt,V2) > Marked_isList(activate(V2)) ;
 }
{
  Marked_U54(tt,V1,V2) > Marked_isNeList(activate(V1)) ;
 }
{
  Marked_U54(tt,V1,V2) > Marked_U55(isNeList(activate(V1)),activate(V2)) ;
 }
{
  Marked_U53(tt,V1,V2) > Marked_U54(isPalListKind(activate(V2)),activate(V1),
                          activate(V2)) ;
 }
{
  Marked_U52(tt,V1,V2) > Marked_U53(isPalListKind(activate(V2)),activate(V1),
                          activate(V2)) ;
 }
{
  Marked_U45(tt,V2) > Marked_isNeList(activate(V2)) ;
 }
{
  Marked_U44(tt,V1,V2) > Marked_isList(activate(V1)) ;
 }
{
  Marked_U44(tt,V1,V2) > Marked_U45(isList(activate(V1)),activate(V2)) ;
 }
{
  Marked_U43(tt,V1,V2) > Marked_U44(isPalListKind(activate(V2)),activate(V1),
                          activate(V2)) ;
 }
{
  Marked_U42(tt,V1,V2) > Marked_U43(isPalListKind(activate(V2)),activate(V1),
                          activate(V2)) ;
 }
{
  Marked_U25(tt,V2) > Marked_isList(activate(V2)) ;
 }
{
  Marked_U24(tt,V1,V2) > Marked_isList(activate(V1)) ;
 }
{
  Marked_U24(tt,V1,V2) > Marked_U25(isList(activate(V1)),activate(V2)) ;
 }
{
  Marked_U23(tt,V1,V2) > Marked_U24(isPalListKind(activate(V2)),activate(V1),
                          activate(V2)) ;
 }
{
  Marked_U22(tt,V1,V2) > Marked_U23(isPalListKind(activate(V2)),activate(V1),
                          activate(V2)) ;
 }
{
  Marked_U12(tt,V) > Marked_isNeList(activate(V)) ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: __(__(X,Y),Z) >= __(X,__(Y,Z))
constraint: __(nil,X) >= X
constraint: __(X,nil) >= X
constraint: __(X1,X2) >= n____(X1,X2)
constraint: nil >= n__nil
constraint: U12(tt,V) >= U13(isNeList(activate(V)))
constraint: isPalListKind(n__nil) >= tt
constraint: isPalListKind(n____(V1,V2)) >= U91(isPalListKind(activate(V1)),
                                            activate(V2))
constraint: isPalListKind(n__a) >= tt
constraint: isPalListKind(n__e) >= tt
constraint: isPalListKind(n__i) >= tt
constraint: isPalListKind(n__o) >= tt
constraint: isPalListKind(n__u) >= tt
constraint: activate(n__nil) >= nil
constraint: activate(n____(X1,X2)) >= __(X1,X2)
constraint: activate(n__a) >= a
constraint: activate(n__e) >= e
constraint: activate(n__i) >= i
constraint: activate(n__o) >= o
constraint: activate(n__u) >= u
constraint: activate(X) >= X
constraint: U11(tt,V) >= U12(isPalListKind(activate(V)),activate(V))
constraint: U13(tt) >= tt
constraint: isNeList(n____(V1,V2)) >= U41(isPalListKind(activate(V1)),
                                       activate(V1),activate(V2))
constraint: isNeList(n____(V1,V2)) >= U51(isPalListKind(activate(V1)),
                                       activate(V1),activate(V2))
constraint: isNeList(V) >= U31(isPalListKind(activate(V)),activate(V))
constraint: U22(tt,V1,V2) >= U23(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U21(tt,V1,V2) >= U22(isPalListKind(activate(V1)),activate(V1),
                              activate(V2))
constraint: U23(tt,V1,V2) >= U24(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U24(tt,V1,V2) >= U25(isList(activate(V1)),activate(V2))
constraint: U25(tt,V2) >= U26(isList(activate(V2)))
constraint: isList(n__nil) >= tt
constraint: isList(n____(V1,V2)) >= U21(isPalListKind(activate(V1)),
                                     activate(V1),activate(V2))
constraint: isList(V) >= U11(isPalListKind(activate(V)),activate(V))
constraint: U26(tt) >= tt
constraint: U32(tt,V) >= U33(isQid(activate(V)))
constraint: U31(tt,V) >= U32(isPalListKind(activate(V)),activate(V))
constraint: U33(tt) >= tt
constraint: isQid(n__a) >= tt
constraint: isQid(n__e) >= tt
constraint: isQid(n__i) >= tt
constraint: isQid(n__o) >= tt
constraint: isQid(n__u) >= tt
constraint: U42(tt,V1,V2) >= U43(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U41(tt,V1,V2) >= U42(isPalListKind(activate(V1)),activate(V1),
                              activate(V2))
constraint: U43(tt,V1,V2) >= U44(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U44(tt,V1,V2) >= U45(isList(activate(V1)),activate(V2))
constraint: U45(tt,V2) >= U46(isNeList(activate(V2)))
constraint: U46(tt) >= tt
constraint: U52(tt,V1,V2) >= U53(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U51(tt,V1,V2) >= U52(isPalListKind(activate(V1)),activate(V1),
                              activate(V2))
constraint: U53(tt,V1,V2) >= U54(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U54(tt,V1,V2) >= U55(isNeList(activate(V1)),activate(V2))
constraint: U55(tt,V2) >= U56(isList(activate(V2)))
constraint: U56(tt) >= tt
constraint: U62(tt,V) >= U63(isQid(activate(V)))
constraint: U61(tt,V) >= U62(isPalListKind(activate(V)),activate(V))
constraint: U63(tt) >= tt
constraint: U72(tt,P) >= U73(isPal(activate(P)),activate(P))
constraint: U71(tt,I,P) >= U72(isPalListKind(activate(I)),activate(P))
constraint: U73(tt,P) >= U74(isPalListKind(activate(P)))
constraint: isPal(n__nil) >= tt
constraint: isPal(V) >= U81(isPalListKind(activate(V)),activate(V))
constraint: U74(tt) >= tt
constraint: U82(tt,V) >= U83(isNePal(activate(V)))
constraint: U81(tt,V) >= U82(isPalListKind(activate(V)),activate(V))
constraint: U83(tt) >= tt
constraint: isNePal(n____(I,__(P,I))) >= U71(isQid(activate(I)),activate(I),
                                          activate(P))
constraint: isNePal(V) >= U61(isPalListKind(activate(V)),activate(V))
constraint: U92(tt) >= tt
constraint: U91(tt,V2) >= U92(isPalListKind(activate(V2)))
constraint: a >= n__a
constraint: e >= n__e
constraint: i >= n__i
constraint: o >= n__o
constraint: u >= n__u
constraint: Marked_isNeList(n____(V1,V2)) >= Marked_U51(isPalListKind(
                                                         activate(V1)),
                                              activate(V1),activate(V2))
constraint: Marked_isNeList(n____(V1,V2)) >= Marked_U41(isPalListKind(
                                                         activate(V1)),
                                              activate(V1),activate(V2))
constraint: Marked_U51(tt,V1,V2) >= Marked_U52(isPalListKind(activate(V1)),
                                     activate(V1),activate(V2))
constraint: Marked_U41(tt,V1,V2) >= Marked_U42(isPalListKind(activate(V1)),
                                     activate(V1),activate(V2))
constraint: Marked_isList(n____(V1,V2)) >= Marked_U21(isPalListKind(activate(
                                                                    V1)),
                                            activate(V1),activate(V2))
constraint: Marked_isList(V) >= Marked_U11(isPalListKind(activate(V)),
                                 activate(V))
constraint: Marked_U21(tt,V1,V2) >= Marked_U22(isPalListKind(activate(V1)),
                                     activate(V1),activate(V2))
constraint: Marked_U11(tt,V) >= Marked_U12(isPalListKind(activate(V)),
                                 activate(V))
constraint: Marked_U55(tt,V2) >= Marked_isList(activate(V2))
constraint: Marked_U54(tt,V1,V2) >= Marked_isNeList(activate(V1))
constraint: Marked_U54(tt,V1,V2) >= Marked_U55(isNeList(activate(V1)),
                                     activate(V2))
constraint: Marked_U53(tt,V1,V2) >= Marked_U54(isPalListKind(activate(V2)),
                                     activate(V1),activate(V2))
constraint: Marked_U52(tt,V1,V2) >= Marked_U53(isPalListKind(activate(V2)),
                                     activate(V1),activate(V2))
constraint: Marked_U45(tt,V2) >= Marked_isNeList(activate(V2))
constraint: Marked_U44(tt,V1,V2) >= Marked_isList(activate(V1))
constraint: Marked_U44(tt,V1,V2) >= Marked_U45(isList(activate(V1)),
                                     activate(V2))
constraint: Marked_U43(tt,V1,V2) >= Marked_U44(isPalListKind(activate(V2)),
                                     activate(V1),activate(V2))
constraint: Marked_U42(tt,V1,V2) >= Marked_U43(isPalListKind(activate(V2)),
                                     activate(V1),activate(V2))
constraint: Marked_U25(tt,V2) >= Marked_isList(activate(V2))
constraint: Marked_U24(tt,V1,V2) >= Marked_isList(activate(V1))
constraint: Marked_U24(tt,V1,V2) >= Marked_U25(isList(activate(V1)),
                                     activate(V2))
constraint: Marked_U23(tt,V1,V2) >= Marked_U24(isPalListKind(activate(V2)),
                                     activate(V1),activate(V2))
constraint: Marked_U22(tt,V1,V2) >= Marked_U23(isPalListKind(activate(V2)),
                                     activate(V1),activate(V2))
constraint: Marked_U12(tt,V) >= Marked_isNeList(activate(V))
APPLY CRITERIA (Subterm criterion)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  __(__(X,Y),Z) >= __(X,__(Y,Z)) ;
  __(nil,X) >= X ;
  __(X,nil) >= X ;
  __(X1,X2) >= n____(X1,X2) ;
  nil >= n__nil ;
  U12(tt,V) >= U13(isNeList(activate(V))) ;
  isPalListKind(n__nil) >= tt ;
  isPalListKind(n____(V1,V2)) >= U91(isPalListKind(activate(V1)),activate(V2)) ;
  isPalListKind(n__a) >= tt ;
  isPalListKind(n__e) >= tt ;
  isPalListKind(n__i) >= tt ;
  isPalListKind(n__o) >= tt ;
  isPalListKind(n__u) >= tt ;
  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 ;
  U11(tt,V) >= U12(isPalListKind(activate(V)),activate(V)) ;
  U13(tt) >= tt ;
  isNeList(n____(V1,V2)) >= U41(isPalListKind(activate(V1)),activate(V1),
                             activate(V2)) ;
  isNeList(n____(V1,V2)) >= U51(isPalListKind(activate(V1)),activate(V1),
                             activate(V2)) ;
  isNeList(V) >= U31(isPalListKind(activate(V)),activate(V)) ;
  U22(tt,V1,V2) >= U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U21(tt,V1,V2) >= U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) ;
  U23(tt,V1,V2) >= U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U24(tt,V1,V2) >= U25(isList(activate(V1)),activate(V2)) ;
  U25(tt,V2) >= U26(isList(activate(V2))) ;
  isList(n__nil) >= tt ;
  isList(n____(V1,V2)) >= U21(isPalListKind(activate(V1)),activate(V1),
                           activate(V2)) ;
  isList(V) >= U11(isPalListKind(activate(V)),activate(V)) ;
  U26(tt) >= tt ;
  U32(tt,V) >= U33(isQid(activate(V))) ;
  U31(tt,V) >= U32(isPalListKind(activate(V)),activate(V)) ;
  U33(tt) >= tt ;
  isQid(n__a) >= tt ;
  isQid(n__e) >= tt ;
  isQid(n__i) >= tt ;
  isQid(n__o) >= tt ;
  isQid(n__u) >= tt ;
  U42(tt,V1,V2) >= U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U41(tt,V1,V2) >= U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) ;
  U43(tt,V1,V2) >= U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U44(tt,V1,V2) >= U45(isList(activate(V1)),activate(V2)) ;
  U45(tt,V2) >= U46(isNeList(activate(V2))) ;
  U46(tt) >= tt ;
  U52(tt,V1,V2) >= U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U51(tt,V1,V2) >= U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) ;
  U53(tt,V1,V2) >= U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U54(tt,V1,V2) >= U55(isNeList(activate(V1)),activate(V2)) ;
  U55(tt,V2) >= U56(isList(activate(V2))) ;
  U56(tt) >= tt ;
  U62(tt,V) >= U63(isQid(activate(V))) ;
  U61(tt,V) >= U62(isPalListKind(activate(V)),activate(V)) ;
  U63(tt) >= tt ;
  U72(tt,P) >= U73(isPal(activate(P)),activate(P)) ;
  U71(tt,I,P) >= U72(isPalListKind(activate(I)),activate(P)) ;
  U73(tt,P) >= U74(isPalListKind(activate(P))) ;
  isPal(n__nil) >= tt ;
  isPal(V) >= U81(isPalListKind(activate(V)),activate(V)) ;
  U74(tt) >= tt ;
  U82(tt,V) >= U83(isNePal(activate(V))) ;
  U81(tt,V) >= U82(isPalListKind(activate(V)),activate(V)) ;
  U83(tt) >= tt ;
  isNePal(n____(I,__(P,I))) >= U71(isQid(activate(I)),activate(I),activate(P)) ;
  isNePal(V) >= U61(isPalListKind(activate(V)),activate(V)) ;
  U92(tt) >= tt ;
  U91(tt,V2) >= U92(isPalListKind(activate(V2))) ;
  a >= n__a ;
  e >= n__e ;
  i >= n__i ;
  o >= n__o ;
  u >= n__u ;
  Marked_isPal(V) >= Marked_U81(isPalListKind(activate(V)),activate(V)) ;
  Marked_U81(tt,V) >= Marked_U82(isPalListKind(activate(V)),activate(V)) ;
  Marked_isNePal(n____(I,__(P,I))) >= Marked_U71(isQid(activate(I)),
                                       activate(I),activate(P)) ;
  Marked_U71(tt,I,P) >= Marked_U72(isPalListKind(activate(I)),activate(P)) ;
  Marked_U82(tt,V) >= Marked_isNePal(activate(V)) ;
  Marked_U72(tt,P) >= Marked_isPal(activate(P)) ;
 }
 + Disjunctions:{ 
{
  Marked_isPal(V) > Marked_U81(isPalListKind(activate(V)),activate(V)) ;
 }
{
  Marked_U81(tt,V) > Marked_U82(isPalListKind(activate(V)),activate(V)) ;
 }
{
  Marked_isNePal(n____(I,__(P,I))) > Marked_U71(isQid(activate(I)),activate(I),
                                      activate(P)) ;
 }
{
  Marked_U71(tt,I,P) > Marked_U72(isPalListKind(activate(I)),activate(P)) ;
 }
{
  Marked_U82(tt,V) > Marked_isNePal(activate(V)) ;
 }
{
  Marked_U72(tt,P) > Marked_isPal(activate(P)) ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: __(__(X,Y),Z) >= __(X,__(Y,Z))
constraint: __(nil,X) >= X
constraint: __(X,nil) >= X
constraint: __(X1,X2) >= n____(X1,X2)
constraint: nil >= n__nil
constraint: U12(tt,V) >= U13(isNeList(activate(V)))
constraint: isPalListKind(n__nil) >= tt
constraint: isPalListKind(n____(V1,V2)) >= U91(isPalListKind(activate(V1)),
                                            activate(V2))
constraint: isPalListKind(n__a) >= tt
constraint: isPalListKind(n__e) >= tt
constraint: isPalListKind(n__i) >= tt
constraint: isPalListKind(n__o) >= tt
constraint: isPalListKind(n__u) >= tt
constraint: activate(n__nil) >= nil
constraint: activate(n____(X1,X2)) >= __(X1,X2)
constraint: activate(n__a) >= a
constraint: activate(n__e) >= e
constraint: activate(n__i) >= i
constraint: activate(n__o) >= o
constraint: activate(n__u) >= u
constraint: activate(X) >= X
constraint: U11(tt,V) >= U12(isPalListKind(activate(V)),activate(V))
constraint: U13(tt) >= tt
constraint: isNeList(n____(V1,V2)) >= U41(isPalListKind(activate(V1)),
                                       activate(V1),activate(V2))
constraint: isNeList(n____(V1,V2)) >= U51(isPalListKind(activate(V1)),
                                       activate(V1),activate(V2))
constraint: isNeList(V) >= U31(isPalListKind(activate(V)),activate(V))
constraint: U22(tt,V1,V2) >= U23(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U21(tt,V1,V2) >= U22(isPalListKind(activate(V1)),activate(V1),
                              activate(V2))
constraint: U23(tt,V1,V2) >= U24(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U24(tt,V1,V2) >= U25(isList(activate(V1)),activate(V2))
constraint: U25(tt,V2) >= U26(isList(activate(V2)))
constraint: isList(n__nil) >= tt
constraint: isList(n____(V1,V2)) >= U21(isPalListKind(activate(V1)),
                                     activate(V1),activate(V2))
constraint: isList(V) >= U11(isPalListKind(activate(V)),activate(V))
constraint: U26(tt) >= tt
constraint: U32(tt,V) >= U33(isQid(activate(V)))
constraint: U31(tt,V) >= U32(isPalListKind(activate(V)),activate(V))
constraint: U33(tt) >= tt
constraint: isQid(n__a) >= tt
constraint: isQid(n__e) >= tt
constraint: isQid(n__i) >= tt
constraint: isQid(n__o) >= tt
constraint: isQid(n__u) >= tt
constraint: U42(tt,V1,V2) >= U43(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U41(tt,V1,V2) >= U42(isPalListKind(activate(V1)),activate(V1),
                              activate(V2))
constraint: U43(tt,V1,V2) >= U44(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U44(tt,V1,V2) >= U45(isList(activate(V1)),activate(V2))
constraint: U45(tt,V2) >= U46(isNeList(activate(V2)))
constraint: U46(tt) >= tt
constraint: U52(tt,V1,V2) >= U53(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U51(tt,V1,V2) >= U52(isPalListKind(activate(V1)),activate(V1),
                              activate(V2))
constraint: U53(tt,V1,V2) >= U54(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U54(tt,V1,V2) >= U55(isNeList(activate(V1)),activate(V2))
constraint: U55(tt,V2) >= U56(isList(activate(V2)))
constraint: U56(tt) >= tt
constraint: U62(tt,V) >= U63(isQid(activate(V)))
constraint: U61(tt,V) >= U62(isPalListKind(activate(V)),activate(V))
constraint: U63(tt) >= tt
constraint: U72(tt,P) >= U73(isPal(activate(P)),activate(P))
constraint: U71(tt,I,P) >= U72(isPalListKind(activate(I)),activate(P))
constraint: U73(tt,P) >= U74(isPalListKind(activate(P)))
constraint: isPal(n__nil) >= tt
constraint: isPal(V) >= U81(isPalListKind(activate(V)),activate(V))
constraint: U74(tt) >= tt
constraint: U82(tt,V) >= U83(isNePal(activate(V)))
constraint: U81(tt,V) >= U82(isPalListKind(activate(V)),activate(V))
constraint: U83(tt) >= tt
constraint: isNePal(n____(I,__(P,I))) >= U71(isQid(activate(I)),activate(I),
                                          activate(P))
constraint: isNePal(V) >= U61(isPalListKind(activate(V)),activate(V))
constraint: U92(tt) >= tt
constraint: U91(tt,V2) >= U92(isPalListKind(activate(V2)))
constraint: a >= n__a
constraint: e >= n__e
constraint: i >= n__i
constraint: o >= n__o
constraint: u >= n__u
constraint: Marked_isPal(V) >= Marked_U81(isPalListKind(activate(V)),
                                activate(V))
constraint: Marked_U81(tt,V) >= Marked_U82(isPalListKind(activate(V)),
                                 activate(V))
constraint: Marked_isNePal(n____(I,__(P,I))) >= Marked_U71(isQid(activate(I)),
                                                 activate(I),activate(P))
constraint: Marked_U71(tt,I,P) >= Marked_U72(isPalListKind(activate(I)),
                                   activate(P))
constraint: Marked_U82(tt,V) >= Marked_isNePal(activate(V))
constraint: Marked_U72(tt,P) >= Marked_isPal(activate(P))
APPLY CRITERIA (Subterm criterion)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  __(__(X,Y),Z) >= __(X,__(Y,Z)) ;
  __(nil,X) >= X ;
  __(X,nil) >= X ;
  __(X1,X2) >= n____(X1,X2) ;
  nil >= n__nil ;
  U12(tt,V) >= U13(isNeList(activate(V))) ;
  isPalListKind(n__nil) >= tt ;
  isPalListKind(n____(V1,V2)) >= U91(isPalListKind(activate(V1)),activate(V2)) ;
  isPalListKind(n__a) >= tt ;
  isPalListKind(n__e) >= tt ;
  isPalListKind(n__i) >= tt ;
  isPalListKind(n__o) >= tt ;
  isPalListKind(n__u) >= tt ;
  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 ;
  U11(tt,V) >= U12(isPalListKind(activate(V)),activate(V)) ;
  U13(tt) >= tt ;
  isNeList(n____(V1,V2)) >= U41(isPalListKind(activate(V1)),activate(V1),
                             activate(V2)) ;
  isNeList(n____(V1,V2)) >= U51(isPalListKind(activate(V1)),activate(V1),
                             activate(V2)) ;
  isNeList(V) >= U31(isPalListKind(activate(V)),activate(V)) ;
  U22(tt,V1,V2) >= U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U21(tt,V1,V2) >= U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) ;
  U23(tt,V1,V2) >= U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U24(tt,V1,V2) >= U25(isList(activate(V1)),activate(V2)) ;
  U25(tt,V2) >= U26(isList(activate(V2))) ;
  isList(n__nil) >= tt ;
  isList(n____(V1,V2)) >= U21(isPalListKind(activate(V1)),activate(V1),
                           activate(V2)) ;
  isList(V) >= U11(isPalListKind(activate(V)),activate(V)) ;
  U26(tt) >= tt ;
  U32(tt,V) >= U33(isQid(activate(V))) ;
  U31(tt,V) >= U32(isPalListKind(activate(V)),activate(V)) ;
  U33(tt) >= tt ;
  isQid(n__a) >= tt ;
  isQid(n__e) >= tt ;
  isQid(n__i) >= tt ;
  isQid(n__o) >= tt ;
  isQid(n__u) >= tt ;
  U42(tt,V1,V2) >= U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U41(tt,V1,V2) >= U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) ;
  U43(tt,V1,V2) >= U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U44(tt,V1,V2) >= U45(isList(activate(V1)),activate(V2)) ;
  U45(tt,V2) >= U46(isNeList(activate(V2))) ;
  U46(tt) >= tt ;
  U52(tt,V1,V2) >= U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U51(tt,V1,V2) >= U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) ;
  U53(tt,V1,V2) >= U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) ;
  U54(tt,V1,V2) >= U55(isNeList(activate(V1)),activate(V2)) ;
  U55(tt,V2) >= U56(isList(activate(V2))) ;
  U56(tt) >= tt ;
  U62(tt,V) >= U63(isQid(activate(V))) ;
  U61(tt,V) >= U62(isPalListKind(activate(V)),activate(V)) ;
  U63(tt) >= tt ;
  U72(tt,P) >= U73(isPal(activate(P)),activate(P)) ;
  U71(tt,I,P) >= U72(isPalListKind(activate(I)),activate(P)) ;
  U73(tt,P) >= U74(isPalListKind(activate(P))) ;
  isPal(n__nil) >= tt ;
  isPal(V) >= U81(isPalListKind(activate(V)),activate(V)) ;
  U74(tt) >= tt ;
  U82(tt,V) >= U83(isNePal(activate(V))) ;
  U81(tt,V) >= U82(isPalListKind(activate(V)),activate(V)) ;
  U83(tt) >= tt ;
  isNePal(n____(I,__(P,I))) >= U71(isQid(activate(I)),activate(I),activate(P)) ;
  isNePal(V) >= U61(isPalListKind(activate(V)),activate(V)) ;
  U92(tt) >= tt ;
  U91(tt,V2) >= U92(isPalListKind(activate(V2))) ;
  a >= n__a ;
  e >= n__e ;
  i >= n__i ;
  o >= n__o ;
  u >= n__u ;
  Marked_isPalListKind(n____(V1,V2)) >= Marked_isPalListKind(activate(V1)) ;
  Marked_isPalListKind(n____(V1,V2)) >= Marked_U91(isPalListKind(activate(V1)),
                                         activate(V2)) ;
  Marked_U91(tt,V2) >= Marked_isPalListKind(activate(V2)) ;
 }
 + Disjunctions:{ 
{
  Marked_isPalListKind(n____(V1,V2)) > Marked_isPalListKind(activate(V1)) ;
 }
{
  Marked_isPalListKind(n____(V1,V2)) > Marked_U91(isPalListKind(activate(V1)),
                                        activate(V2)) ;
 }
{
  Marked_U91(tt,V2) > Marked_isPalListKind(activate(V2)) ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: __(__(X,Y),Z) >= __(X,__(Y,Z))
constraint: __(nil,X) >= X
constraint: __(X,nil) >= X
constraint: __(X1,X2) >= n____(X1,X2)
constraint: nil >= n__nil
constraint: U12(tt,V) >= U13(isNeList(activate(V)))
constraint: isPalListKind(n__nil) >= tt
constraint: isPalListKind(n____(V1,V2)) >= U91(isPalListKind(activate(V1)),
                                            activate(V2))
constraint: isPalListKind(n__a) >= tt
constraint: isPalListKind(n__e) >= tt
constraint: isPalListKind(n__i) >= tt
constraint: isPalListKind(n__o) >= tt
constraint: isPalListKind(n__u) >= tt
constraint: activate(n__nil) >= nil
constraint: activate(n____(X1,X2)) >= __(X1,X2)
constraint: activate(n__a) >= a
constraint: activate(n__e) >= e
constraint: activate(n__i) >= i
constraint: activate(n__o) >= o
constraint: activate(n__u) >= u
constraint: activate(X) >= X
constraint: U11(tt,V) >= U12(isPalListKind(activate(V)),activate(V))
constraint: U13(tt) >= tt
constraint: isNeList(n____(V1,V2)) >= U41(isPalListKind(activate(V1)),
                                       activate(V1),activate(V2))
constraint: isNeList(n____(V1,V2)) >= U51(isPalListKind(activate(V1)),
                                       activate(V1),activate(V2))
constraint: isNeList(V) >= U31(isPalListKind(activate(V)),activate(V))
constraint: U22(tt,V1,V2) >= U23(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U21(tt,V1,V2) >= U22(isPalListKind(activate(V1)),activate(V1),
                              activate(V2))
constraint: U23(tt,V1,V2) >= U24(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U24(tt,V1,V2) >= U25(isList(activate(V1)),activate(V2))
constraint: U25(tt,V2) >= U26(isList(activate(V2)))
constraint: isList(n__nil) >= tt
constraint: isList(n____(V1,V2)) >= U21(isPalListKind(activate(V1)),
                                     activate(V1),activate(V2))
constraint: isList(V) >= U11(isPalListKind(activate(V)),activate(V))
constraint: U26(tt) >= tt
constraint: U32(tt,V) >= U33(isQid(activate(V)))
constraint: U31(tt,V) >= U32(isPalListKind(activate(V)),activate(V))
constraint: U33(tt) >= tt
constraint: isQid(n__a) >= tt
constraint: isQid(n__e) >= tt
constraint: isQid(n__i) >= tt
constraint: isQid(n__o) >= tt
constraint: isQid(n__u) >= tt
constraint: U42(tt,V1,V2) >= U43(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U41(tt,V1,V2) >= U42(isPalListKind(activate(V1)),activate(V1),
                              activate(V2))
constraint: U43(tt,V1,V2) >= U44(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U44(tt,V1,V2) >= U45(isList(activate(V1)),activate(V2))
constraint: U45(tt,V2) >= U46(isNeList(activate(V2)))
constraint: U46(tt) >= tt
constraint: U52(tt,V1,V2) >= U53(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U51(tt,V1,V2) >= U52(isPalListKind(activate(V1)),activate(V1),
                              activate(V2))
constraint: U53(tt,V1,V2) >= U54(isPalListKind(activate(V2)),activate(V1),
                              activate(V2))
constraint: U54(tt,V1,V2) >= U55(isNeList(activate(V1)),activate(V2))
constraint: U55(tt,V2) >= U56(isList(activate(V2)))
constraint: U56(tt) >= tt
constraint: U62(tt,V) >= U63(isQid(activate(V)))
constraint: U61(tt,V) >= U62(isPalListKind(activate(V)),activate(V))
constraint: U63(tt) >= tt
constraint: U72(tt,P) >= U73(isPal(activate(P)),activate(P))
constraint: U71(tt,I,P) >= U72(isPalListKind(activate(I)),activate(P))
constraint: U73(tt,P) >= U74(isPalListKind(activate(P)))
constraint: isPal(n__nil) >= tt
constraint: isPal(V) >= U81(isPalListKind(activate(V)),activate(V))
constraint: U74(tt) >= tt
constraint: U82(tt,V) >= U83(isNePal(activate(V)))
constraint: U81(tt,V) >= U82(isPalListKind(activate(V)),activate(V))
constraint: U83(tt) >= tt
constraint: isNePal(n____(I,__(P,I))) >= U71(isQid(activate(I)),activate(I),
                                          activate(P))
constraint: isNePal(V) >= U61(isPalListKind(activate(V)),activate(V))
constraint: U92(tt) >= tt
constraint: U91(tt,V2) >= U92(isPalListKind(activate(V2)))
constraint: a >= n__a
constraint: e >= n__e
constraint: i >= n__i
constraint: o >= n__o
constraint: u >= n__u
constraint: Marked_isPalListKind(n____(V1,V2)) >= Marked_isPalListKind(
                                                   activate(V1))
constraint: Marked_isPalListKind(n____(V1,V2)) >= Marked_U91(isPalListKind(
                                                              activate(
                                                               V1)),
                                                   activate(V2))
constraint: Marked_U91(tt,V2) >= Marked_isPalListKind(activate(V2))
APPLY CRITERIA (Subterm criterion)

ST: Marked___ -> 1

APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
SOLVED
{
 
TRS termination of:
[1] __(__(X,Y),Z) -> __(X,__(Y,Z))
[2] __(X,nil) -> X
[3] __(nil,X) -> X
[4] U11(tt,V) -> U12(isPalListKind(activate(V)),activate(V))
[5] U12(tt,V) -> U13(isNeList(activate(V)))
[6] U13(tt) -> tt
[7] U21(tt,V1,V2) -> U22(isPalListKind(activate(V1)),activate(V1),activate(V2))
[8] U22(tt,V1,V2) -> U23(isPalListKind(activate(V2)),activate(V1),activate(V2))
[9] U23(tt,V1,V2) -> U24(isPalListKind(activate(V2)),activate(V1),activate(V2))
[10] U24(tt,V1,V2) -> U25(isList(activate(V1)),activate(V2))
[11] U25(tt,V2) -> U26(isList(activate(V2)))
[12] U26(tt) -> tt
[13] U31(tt,V) -> U32(isPalListKind(activate(V)),activate(V))
[14] U32(tt,V) -> U33(isQid(activate(V)))
[15] U33(tt) -> tt
[16] U41(tt,V1,V2) ->
 U42(isPalListKind(activate(V1)),activate(V1),activate(V2))
[17] U42(tt,V1,V2) ->
 U43(isPalListKind(activate(V2)),activate(V1),activate(V2))
[18] U43(tt,V1,V2) ->
 U44(isPalListKind(activate(V2)),activate(V1),activate(V2))
[19] U44(tt,V1,V2) -> U45(isList(activate(V1)),activate(V2))
[20] U45(tt,V2) -> U46(isNeList(activate(V2)))
[21] U46(tt) -> tt
[22] U51(tt,V1,V2) ->
 U52(isPalListKind(activate(V1)),activate(V1),activate(V2))
[23] U52(tt,V1,V2) ->
 U53(isPalListKind(activate(V2)),activate(V1),activate(V2))
[24] U53(tt,V1,V2) ->
 U54(isPalListKind(activate(V2)),activate(V1),activate(V2))
[25] U54(tt,V1,V2) -> U55(isNeList(activate(V1)),activate(V2))
[26] U55(tt,V2) -> U56(isList(activate(V2)))
[27] U56(tt) -> tt
[28] U61(tt,V) -> U62(isPalListKind(activate(V)),activate(V))
[29] U62(tt,V) -> U63(isQid(activate(V)))
[30] U63(tt) -> tt
[31] U71(tt,I,P) -> U72(isPalListKind(activate(I)),activate(P))
[32] U72(tt,P) -> U73(isPal(activate(P)),activate(P))
[33] U73(tt,P) -> U74(isPalListKind(activate(P)))
[34] U74(tt) -> tt
[35] U81(tt,V) -> U82(isPalListKind(activate(V)),activate(V))
[36] U82(tt,V) -> U83(isNePal(activate(V)))
[37] U83(tt) -> tt
[38] U91(tt,V2) -> U92(isPalListKind(activate(V2)))
[39] U92(tt) -> tt
[40] isList(V) -> U11(isPalListKind(activate(V)),activate(V))
[41] isList(n__nil) -> tt
[42] isList(n____(V1,V2)) ->
 U21(isPalListKind(activate(V1)),activate(V1),activate(V2))
[43] isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
[44] isNeList(n____(V1,V2)) ->
 U41(isPalListKind(activate(V1)),activate(V1),activate(V2))
[45] isNeList(n____(V1,V2)) ->
 U51(isPalListKind(activate(V1)),activate(V1),activate(V2))
[46] isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
[47] isNePal(n____(I,__(P,I))) ->
 U71(isQid(activate(I)),activate(I),activate(P))
[48] isPal(V) -> U81(isPalListKind(activate(V)),activate(V))
[49] isPal(n__nil) -> tt
[50] isPalListKind(n__a) -> tt
[51] isPalListKind(n__e) -> tt
[52] isPalListKind(n__i) -> tt
[53] isPalListKind(n__nil) -> tt
[54] isPalListKind(n__o) -> tt
[55] isPalListKind(n__u) -> tt
[56] isPalListKind(n____(V1,V2)) ->
 U91(isPalListKind(activate(V1)),activate(V2))
[57] isQid(n__a) -> tt
[58] isQid(n__e) -> tt
[59] isQid(n__i) -> tt
[60] isQid(n__o) -> tt
[61] isQid(n__u) -> tt
[62] nil -> n__nil
[63] __(X1,X2) -> n____(X1,X2)
[64] a -> n__a
[65] e -> n__e
[66] i -> n__i
[67] o -> n__o
[68] u -> n__u
[69] activate(n__nil) -> nil
[70] activate(n____(X1,X2)) -> __(X1,X2)
[71] activate(n__a) -> a
[72] activate(n__e) -> e
[73] activate(n__i) -> i
[74] activate(n__o) -> o
[75] activate(n__u) -> u
[76] activate(X) -> X
 ,
 CRITERION: MDP
 [ {
      
     DP termination of:
     <Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))>
<Marked___(__(X,Y),Z) , Marked___(Y,Z)>
<Marked_U11(tt,V) , Marked_U12(isPalListKind(activate(V)),activate(V))>
<Marked_U11(tt,V) , Marked_isPalListKind(activate(V))>
<Marked_U11(tt,V) , Marked_activate(V)>
<Marked_U11(tt,V) , Marked_activate(V)>
<Marked_U12(tt,V) , Marked_U13(isNeList(activate(V)))>
<Marked_U12(tt,V) , Marked_isNeList(activate(V))>
<Marked_U12(tt,V) , Marked_activate(V)>
<Marked_U21(tt,V1,V2) , Marked_U22(isPalListKind(activate(V1)),activate(V1),
                         activate(V2))>
<Marked_U21(tt,V1,V2) , Marked_isPalListKind(activate(V1))>
<Marked_U21(tt,V1,V2) , Marked_activate(V1)>
<Marked_U21(tt,V1,V2) , Marked_activate(V1)>
<Marked_U21(tt,V1,V2) , Marked_activate(V2)>
<Marked_U22(tt,V1,V2) , Marked_U23(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U22(tt,V1,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U22(tt,V1,V2) , Marked_activate(V2)>
<Marked_U22(tt,V1,V2) , Marked_activate(V1)>
<Marked_U22(tt,V1,V2) , Marked_activate(V2)>
<Marked_U23(tt,V1,V2) , Marked_U24(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U23(tt,V1,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U23(tt,V1,V2) , Marked_activate(V2)>
<Marked_U23(tt,V1,V2) , Marked_activate(V1)>
<Marked_U23(tt,V1,V2) , Marked_activate(V2)>
<Marked_U24(tt,V1,V2) , Marked_U25(isList(activate(V1)),activate(V2))>
<Marked_U24(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U24(tt,V1,V2) , Marked_activate(V1)>
<Marked_U24(tt,V1,V2) , Marked_activate(V2)>
<Marked_U25(tt,V2) , Marked_U26(isList(activate(V2)))>
<Marked_U25(tt,V2) , Marked_isList(activate(V2))>
<Marked_U25(tt,V2) , Marked_activate(V2)>
<Marked_U31(tt,V) , Marked_U32(isPalListKind(activate(V)),activate(V))>
<Marked_U31(tt,V) , Marked_isPalListKind(activate(V))>
<Marked_U31(tt,V) , Marked_activate(V)>
<Marked_U31(tt,V) , Marked_activate(V)>
<Marked_U32(tt,V) , Marked_U33(isQid(activate(V)))>
<Marked_U32(tt,V) , Marked_isQid(activate(V))>
<Marked_U32(tt,V) , Marked_activate(V)>
<Marked_U41(tt,V1,V2) , Marked_U42(isPalListKind(activate(V1)),activate(V1),
                         activate(V2))>
<Marked_U41(tt,V1,V2) , Marked_isPalListKind(activate(V1))>
<Marked_U41(tt,V1,V2) , Marked_activate(V1)>
<Marked_U41(tt,V1,V2) , Marked_activate(V1)>
<Marked_U41(tt,V1,V2) , Marked_activate(V2)>
<Marked_U42(tt,V1,V2) , Marked_U43(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U42(tt,V1,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U42(tt,V1,V2) , Marked_activate(V2)>
<Marked_U42(tt,V1,V2) , Marked_activate(V1)>
<Marked_U42(tt,V1,V2) , Marked_activate(V2)>
<Marked_U43(tt,V1,V2) , Marked_U44(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U43(tt,V1,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U43(tt,V1,V2) , Marked_activate(V2)>
<Marked_U43(tt,V1,V2) , Marked_activate(V1)>
<Marked_U43(tt,V1,V2) , Marked_activate(V2)>
<Marked_U44(tt,V1,V2) , Marked_U45(isList(activate(V1)),activate(V2))>
<Marked_U44(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U44(tt,V1,V2) , Marked_activate(V1)>
<Marked_U44(tt,V1,V2) , Marked_activate(V2)>
<Marked_U45(tt,V2) , Marked_U46(isNeList(activate(V2)))>
<Marked_U45(tt,V2) , Marked_isNeList(activate(V2))>
<Marked_U45(tt,V2) , Marked_activate(V2)>
<Marked_U51(tt,V1,V2) , Marked_U52(isPalListKind(activate(V1)),activate(V1),
                         activate(V2))>
<Marked_U51(tt,V1,V2) , Marked_isPalListKind(activate(V1))>
<Marked_U51(tt,V1,V2) , Marked_activate(V1)>
<Marked_U51(tt,V1,V2) , Marked_activate(V1)>
<Marked_U51(tt,V1,V2) , Marked_activate(V2)>
<Marked_U52(tt,V1,V2) , Marked_U53(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U52(tt,V1,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U52(tt,V1,V2) , Marked_activate(V2)>
<Marked_U52(tt,V1,V2) , Marked_activate(V1)>
<Marked_U52(tt,V1,V2) , Marked_activate(V2)>
<Marked_U53(tt,V1,V2) , Marked_U54(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U53(tt,V1,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U53(tt,V1,V2) , Marked_activate(V2)>
<Marked_U53(tt,V1,V2) , Marked_activate(V1)>
<Marked_U53(tt,V1,V2) , Marked_activate(V2)>
<Marked_U54(tt,V1,V2) , Marked_U55(isNeList(activate(V1)),activate(V2))>
<Marked_U54(tt,V1,V2) , Marked_isNeList(activate(V1))>
<Marked_U54(tt,V1,V2) , Marked_activate(V1)>
<Marked_U54(tt,V1,V2) , Marked_activate(V2)>
<Marked_U55(tt,V2) , Marked_U56(isList(activate(V2)))>
<Marked_U55(tt,V2) , Marked_isList(activate(V2))>
<Marked_U55(tt,V2) , Marked_activate(V2)>
<Marked_U61(tt,V) , Marked_U62(isPalListKind(activate(V)),activate(V))>
<Marked_U61(tt,V) , Marked_isPalListKind(activate(V))>
<Marked_U61(tt,V) , Marked_activate(V)>
<Marked_U61(tt,V) , Marked_activate(V)>
<Marked_U62(tt,V) , Marked_U63(isQid(activate(V)))>
<Marked_U62(tt,V) , Marked_isQid(activate(V))>
<Marked_U62(tt,V) , Marked_activate(V)>
<Marked_U71(tt,I,P) , Marked_U72(isPalListKind(activate(I)),activate(P))>
<Marked_U71(tt,I,P) , Marked_isPalListKind(activate(I))>
<Marked_U71(tt,I,P) , Marked_activate(I)>
<Marked_U71(tt,I,P) , Marked_activate(P)>
<Marked_U72(tt,P) , Marked_U73(isPal(activate(P)),activate(P))>
<Marked_U72(tt,P) , Marked_isPal(activate(P))>
<Marked_U72(tt,P) , Marked_activate(P)>
<Marked_U72(tt,P) , Marked_activate(P)>
<Marked_U73(tt,P) , Marked_U74(isPalListKind(activate(P)))>
<Marked_U73(tt,P) , Marked_isPalListKind(activate(P))>
<Marked_U73(tt,P) , Marked_activate(P)>
<Marked_U81(tt,V) , Marked_U82(isPalListKind(activate(V)),activate(V))>
<Marked_U81(tt,V) , Marked_isPalListKind(activate(V))>
<Marked_U81(tt,V) , Marked_activate(V)>
<Marked_U81(tt,V) , Marked_activate(V)>
<Marked_U82(tt,V) , Marked_U83(isNePal(activate(V)))>
<Marked_U82(tt,V) , Marked_isNePal(activate(V))>
<Marked_U82(tt,V) , Marked_activate(V)>
<Marked_U91(tt,V2) , Marked_U92(isPalListKind(activate(V2)))>
<Marked_U91(tt,V2) , Marked_isPalListKind(activate(V2))>
<Marked_U91(tt,V2) , Marked_activate(V2)>
<Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
<Marked_isList(V) , Marked_isPalListKind(activate(V))>
<Marked_isList(V) , Marked_activate(V)>
<Marked_isList(V) , Marked_activate(V)>
<Marked_isList(n____(V1,V2)) , Marked_U21(isPalListKind(activate(V1)),
                                activate(V1),activate(V2))>
<Marked_isList(n____(V1,V2)) , Marked_isPalListKind(activate(V1))>
<Marked_isList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNeList(V) , Marked_U31(isPalListKind(activate(V)),activate(V))>
<Marked_isNeList(V) , Marked_isPalListKind(activate(V))>
<Marked_isNeList(V) , Marked_activate(V)>
<Marked_isNeList(V) , Marked_activate(V)>
<Marked_isNeList(n____(V1,V2)) , Marked_U41(isPalListKind(activate(V1)),
                                  activate(V1),activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_isPalListKind(activate(V1))>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNeList(n____(V1,V2)) , Marked_U51(isPalListKind(activate(V1)),
                                  activate(V1),activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_isPalListKind(activate(V1))>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNePal(V) , Marked_U61(isPalListKind(activate(V)),activate(V))>
<Marked_isNePal(V) , Marked_isPalListKind(activate(V))>
<Marked_isNePal(V) , Marked_activate(V)>
<Marked_isNePal(V) , Marked_activate(V)>
<Marked_isNePal(n____(I,__(P,I))) , Marked_U71(isQid(activate(I)),activate(I),
                                     activate(P))>
<Marked_isNePal(n____(I,__(P,I))) , Marked_isQid(activate(I))>
<Marked_isNePal(n____(I,__(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,__(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,__(P,I))) , Marked_activate(P)>
<Marked_isPal(V) , Marked_U81(isPalListKind(activate(V)),activate(V))>
<Marked_isPal(V) , Marked_isPalListKind(activate(V))>
<Marked_isPal(V) , Marked_activate(V)>
<Marked_isPal(V) , Marked_activate(V)>
<Marked_isPalListKind(n____(V1,V2)) , Marked_U91(isPalListKind(activate(V1)),
                                       activate(V2))>
<Marked_isPalListKind(n____(V1,V2)) , Marked_isPalListKind(activate(V1))>
<Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V2)>
<Marked_activate(n__nil) , Marked_nil>
<Marked_activate(n____(X1,X2)) , Marked___(X1,X2)>
<Marked_activate(n__a) , Marked_a>
<Marked_activate(n__e) , Marked_e>
<Marked_activate(n__i) , Marked_i>
<Marked_activate(n__o) , Marked_o>
<Marked_activate(n__u) , Marked_u>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_U11(tt,V) , Marked_U12(isPalListKind(activate(V)),activate(V))>
<Marked_U12(tt,V) , Marked_isNeList(activate(V))>
<Marked_U21(tt,V1,V2) , Marked_U22(isPalListKind(activate(V1)),activate(V1),
                         activate(V2))>
<Marked_U22(tt,V1,V2) , Marked_U23(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U23(tt,V1,V2) , Marked_U24(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U24(tt,V1,V2) , Marked_U25(isList(activate(V1)),activate(V2))>
<Marked_U24(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U25(tt,V2) , Marked_isList(activate(V2))>
<Marked_U41(tt,V1,V2) , Marked_U42(isPalListKind(activate(V1)),activate(V1),
                         activate(V2))>
<Marked_U42(tt,V1,V2) , Marked_U43(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U43(tt,V1,V2) , Marked_U44(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U44(tt,V1,V2) , Marked_U45(isList(activate(V1)),activate(V2))>
<Marked_U44(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U45(tt,V2) , Marked_isNeList(activate(V2))>
<Marked_U51(tt,V1,V2) , Marked_U52(isPalListKind(activate(V1)),activate(V1),
                         activate(V2))>
<Marked_U52(tt,V1,V2) , Marked_U53(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U53(tt,V1,V2) , Marked_U54(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U54(tt,V1,V2) , Marked_U55(isNeList(activate(V1)),activate(V2))>
<Marked_U54(tt,V1,V2) , Marked_isNeList(activate(V1))>
<Marked_U55(tt,V2) , Marked_isList(activate(V2))>
<Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
<Marked_isList(n____(V1,V2)) , Marked_U21(isPalListKind(activate(V1)),
                                activate(V1),activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_U41(isPalListKind(activate(V1)),
                                  activate(V1),activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_U51(isPalListKind(activate(V1)),
                                  activate(V1),activate(V2))>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ __ ] (X0,X1) = 1*X1 + 1*X0 + 1; 
 [ U62 ] (X0,X1) = 0; 
 [ Marked_U44 ] (X0,X1,X2) = 2*X2 + 2*X1; 
 [ U32 ] (X0,X1) = 0; 
 [ Marked_U11 ] (X0,X1) = 2*X1; 
 [ n__a ] () = 0; 
 [ isNeList ] (X0) = 3*X0 + 1; 
 [ U82 ] (X0,X1) = 0; 
 [ Marked_U23 ] (X0,X1,X2) = 2*X2 + 2*X1; 
 [ U45 ] (X0,X1) = 0; 
 [ o ] () = 0; 
 [ activate ] (X0) = 1*X0; 
 [ U71 ] (X0,X1,X2) = 1; 
 [ U42 ] (X0,X1,X2) = 2; 
 [ n__u ] () = 0; 
 [ U24 ] (X0,X1,X2) = 0; 
 [ Marked_U41 ] (X0,X1,X2) = 2*X2 + 2*X1; 
 [ U92 ] (X0) = 0; 
 [ U53 ] (X0,X1,X2) = 0; 
 [ Marked_U53 ] (X0,X1,X2) = 2*X2 + 2*X1; 
 [ U12 ] (X0,X1) = 0; 
 [ U63 ] (X0) = 0; 
 [ Marked_U42 ] (X0,X1,X2) = 2*X2 + 2*X1; 
 [ U33 ] (X0) = 0; 
 [ n__i ] () = 0; 
 [ U21 ] (X0,X1,X2) = 0; 
 [ Marked_isNeList ] (X0) = 2*X0; 
 [ U83 ] (X0) = 0; 
 [ U52 ] (X0,X1,X2) = 0; 
 [ Marked_U55 ] (X0,X1) = 2*X1; 
 [ tt ] () = 0; 
 [ isPal ] (X0) = 0; 
 [ Marked_U25 ] (X0,X1) = 2*X1; 
 [ U43 ] (X0,X1,X2) = 0; 
 [ e ] () = 0; 
 [ isList ] (X0) = 0; 
 [ Marked_isList ] (X0) = 2*X0; 
 [ n__nil ] () = 0; 
 [ U55 ] (X0,X1) = 0; 
 [ nil ] () = 0; 
 [ U61 ] (X0,X1) = 0; 
 [ Marked_U43 ] (X0,X1,X2) = 2*X2 + 2*X1; 
 [ U31 ] (X0,X1) = 0; 
 [ n__e ] () = 0; 
 [ U22 ] (X0,X1,X2) = 0; 
 [ U81 ] (X0,X1) = 0; 
 [ Marked_U22 ] (X0,X1,X2) = 2*X2 + 2*X1 + 2; 
 [ U46 ] (X0) = 0; 
 [ u ] () = 0; 
 [ U11 ] (X0,X1) = 0; 
 [ U73 ] (X0,X1) = 1; 
 [ U41 ] (X0,X1,X2) = 3*X1 + 2; 
 [ a ] () = 0; 
 [ U25 ] (X0,X1) = 0; 
 [ U91 ] (X0,X1) = 0; 
 [ U54 ] (X0,X1,X2) = 0; 
 [ Marked_U52 ] (X0,X1,X2) = 2*X2 + 2*X1; 
 [ isPalListKind ] (X0) = 0; 
 [ U72 ] (X0,X1) = 1; 
 [ isQid ] (X0) = 0; 
 [ n__o ] () = 0; 
 [ U23 ] (X0,X1,X2) = 0; 
 [ Marked_U51 ] (X0,X1,X2) = 2*X2 + 2*X1; 
 [ isNePal ] (X0) = 1; 
 [ Marked_U12 ] (X0,X1) = 2*X1; 
 [ U51 ] (X0,X1,X2) = 0; 
 [ Marked_U54 ] (X0,X1,X2) = 2*X2 + 2*X1; 
 [ U13 ] (X0) = 0; 
 [ U74 ] (X0) = 0; 
 [ Marked_U24 ] (X0,X1,X2) = 2*X2 + 2*X1; 
 [ U44 ] (X0,X1,X2) = 0; 
 [ i ] () = 0; 
 [ U26 ] (X0) = 0; 
 [ Marked_U21 ] (X0,X1,X2) = 2*X2 + 2*X1 + 2; 
 [ n____ ] (X0,X1) = 1*X1 + 1*X0 + 1; 
 [ U56 ] (X0) = 0; 
 [ Marked_U45 ] (X0,X1) = 2*X1; 
 removing <Marked_U22(tt,V1,V2),Marked_U23(isPalListKind(activate(V2)),
                                 activate(V1),activate(V2))><Marked_isNeList(
                                                              n____(V1,
                                                               V2)),Marked_U41(
                                                                    isPalListKind(
                                                                    activate(
                                                                    V1)),
                                                                    activate(
                                                                    V1),
                                                                    activate(
                                                                    V2))><
Marked_isNeList(n____(V1,V2)),Marked_U51(isPalListKind(activate(V1)),
                               activate(V1),activate(V2))>
 [ {
      
     DP termination of:
     <Marked_U11(tt,V) , Marked_U12(isPalListKind(activate(V)),activate(V))>
<Marked_U12(tt,V) , Marked_isNeList(activate(V))>
<Marked_U21(tt,V1,V2) , Marked_U22(isPalListKind(activate(V1)),activate(V1),
                         activate(V2))>
<Marked_U23(tt,V1,V2) , Marked_U24(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U24(tt,V1,V2) , Marked_U25(isList(activate(V1)),activate(V2))>
<Marked_U24(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U25(tt,V2) , Marked_isList(activate(V2))>
<Marked_U41(tt,V1,V2) , Marked_U42(isPalListKind(activate(V1)),activate(V1),
                         activate(V2))>
<Marked_U42(tt,V1,V2) , Marked_U43(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U43(tt,V1,V2) , Marked_U44(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U44(tt,V1,V2) , Marked_U45(isList(activate(V1)),activate(V2))>
<Marked_U44(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U45(tt,V2) , Marked_isNeList(activate(V2))>
<Marked_U51(tt,V1,V2) , Marked_U52(isPalListKind(activate(V1)),activate(V1),
                         activate(V2))>
<Marked_U52(tt,V1,V2) , Marked_U53(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U53(tt,V1,V2) , Marked_U54(isPalListKind(activate(V2)),activate(V1),
                         activate(V2))>
<Marked_U54(tt,V1,V2) , Marked_U55(isNeList(activate(V1)),activate(V2))>
<Marked_U54(tt,V1,V2) , Marked_isNeList(activate(V1))>
<Marked_U55(tt,V2) , Marked_isList(activate(V2))>
<Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
<Marked_isList(n____(V1,V2)) , Marked_U21(isPalListKind(activate(V1)),
                                activate(V1),activate(V2))>
 ,
 CRITERION: SG
 [  ]} 
 ]} 
{
 
DP termination of:
<Marked_U71(tt,I,P) , Marked_U72(isPalListKind(activate(I)),activate(P))>
<Marked_U72(tt,P) , Marked_isPal(activate(P))>
<Marked_U81(tt,V) , Marked_U82(isPalListKind(activate(V)),activate(V))>
<Marked_U82(tt,V) , Marked_isNePal(activate(V))>
<Marked_isNePal(n____(I,__(P,I))) , Marked_U71(isQid(activate(I)),activate(I),
                                     activate(P))>
<Marked_isPal(V) , Marked_U81(isPalListKind(activate(V)),activate(V))>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ __ ] (X0,X1) = 1*X1 + 2*X0 + 2; 
 [ U62 ] (X0,X1) = 1; 
 [ U32 ] (X0,X1) = 0; 
 [ n__a ] () = 0; 
 [ isNeList ] (X0) = 0; 
 [ Marked_U71 ] (X0,X1,X2) = 2*X2; 
 [ U82 ] (X0,X1) = 0; 
 [ U45 ] (X0,X1) = 0; 
 [ o ] () = 0; 
 [ activate ] (X0) = 1*X0; 
 [ U71 ] (X0,X1,X2) = 0; 
 [ U42 ] (X0,X1,X2) = 0; 
 [ n__u ] () = 0; 
 [ U24 ] (X0,X1,X2) = 0; 
 [ U92 ] (X0) = 0; 
 [ U53 ] (X0,X1,X2) = 0; 
 [ U12 ] (X0,X1) = 0; 
 [ U63 ] (X0) = 0; 
 [ U33 ] (X0) = 0; 
 [ n__i ] () = 0; 
 [ U21 ] (X0,X1,X2) = 0; 
 [ U83 ] (X0) = 0; 
 [ U52 ] (X0,X1,X2) = 0; 
 [ tt ] () = 0; 
 [ Marked_U81 ] (X0,X1) = 2*X1; 
 [ isPal ] (X0) = 0; 
 [ U43 ] (X0,X1,X2) = 0; 
 [ Marked_U72 ] (X0,X1) = 2*X1; 
 [ e ] () = 0; 
 [ isList ] (X0) = 2; 
 [ n__nil ] () = 0; 
 [ U55 ] (X0,X1) = 0; 
 [ nil ] () = 0; 
 [ U61 ] (X0,X1) = 1; 
 [ U31 ] (X0,X1) = 0; 
 [ n__e ] () = 0; 
 [ U22 ] (X0,X1,X2) = 0; 
 [ U81 ] (X0,X1) = 0; 
 [ U46 ] (X0) = 0; 
 [ u ] () = 0; 
 [ U11 ] (X0,X1) = 0; 
 [ Marked_isPal ] (X0) = 2*X0; 
 [ U73 ] (X0,X1) = 0; 
 [ U41 ] (X0,X1,X2) = 0; 
 [ a ] () = 0; 
 [ U25 ] (X0,X1) = 0; 
 [ U91 ] (X0,X1) = 0; 
 [ U54 ] (X0,X1,X2) = 0; 
 [ isPalListKind ] (X0) = 0; 
 [ U72 ] (X0,X1) = 0; 
 [ isQid ] (X0) = 0; 
 [ Marked_U82 ] (X0,X1) = 2*X1; 
 [ n__o ] () = 0; 
 [ U23 ] (X0,X1,X2) = 0; 
 [ isNePal ] (X0) = 1; 
 [ U51 ] (X0,X1,X2) = 0; 
 [ U13 ] (X0) = 0; 
 [ Marked_isNePal ] (X0) = 2*X0; 
 [ U74 ] (X0) = 0; 
 [ U44 ] (X0,X1,X2) = 0; 
 [ i ] () = 0; 
 [ U26 ] (X0) = 0; 
 [ n____ ] (X0,X1) = 1*X1 + 2*X0 + 2; 
 [ U56 ] (X0) = 0; 
 removing <Marked_isNePal(n____(I,__(P,I))),Marked_U71(isQid(activate(I)),
                                             activate(I),activate(P))>
 [ {
      
     DP termination of:
     <Marked_U71(tt,I,P) , Marked_U72(isPalListKind(activate(I)),activate(P))>
<Marked_U72(tt,P) , Marked_isPal(activate(P))>
<Marked_U81(tt,V) , Marked_U82(isPalListKind(activate(V)),activate(V))>
<Marked_U82(tt,V) , Marked_isNePal(activate(V))>
<Marked_isPal(V) , Marked_U81(isPalListKind(activate(V)),activate(V))>
 ,
 CRITERION: SG
 [  ]} 
 ]} 
{
 
DP termination of:
<Marked_U91(tt,V2) , Marked_isPalListKind(activate(V2))>
<Marked_isPalListKind(n____(V1,V2)) , Marked_U91(isPalListKind(activate(V1)),
                                       activate(V2))>
<Marked_isPalListKind(n____(V1,V2)) , Marked_isPalListKind(activate(V1))>
 ,
 CRITERION: ORD
 [ 
     Solution found:
     polynomial interpretation = 
      [ __ ] (X0,X1) = 3 + 1*X0 + 1*X1 + 0; 
 [ U62 ] (X0,X1) = 0; 
 [ U32 ] (X0,X1) = 0; 
 [ n__a ] () = 0; 
 [ isNeList ] (X0) = 0; 
 [ U82 ] (X0,X1) = 0; 
 [ U45 ] (X0,X1) = 0; 
 [ o ] () = 0; 
 [ activate ] (X0) = 1*X0 + 0; 
 [ Marked_U91 ] (X0,X1) = 3 + 2*X1 + 0; 
 [ U71 ] (X0,X1,X2) = 2 + 0; 
 [ U42 ] (X0,X1,X2) = 0; 
 [ n__u ] () = 0; 
 [ U24 ] (X0,X1,X2) = 0; 
 [ U92 ] (X0) = 0; 
 [ U53 ] (X0,X1,X2) = 0; 
 [ U12 ] (X0,X1) = 0; 
 [ U63 ] (X0) = 0; 
 [ U33 ] (X0) = 0; 
 [ n__i ] () = 0; 
 [ U21 ] (X0,X1,X2) = 0; 
 [ U83 ] (X0) = 0; 
 [ U52 ] (X0,X1,X2) = 0; 
 [ tt ] () = 0; 
 [ isPal ] (X0) = 0; 
 [ U43 ] (X0,X1,X2) = 0; 
 [ e ] () = 0; 
 [ isList ] (X0) = 0; 
 [ n__nil ] () = 0; 
 [ U55 ] (X0,X1) = 0; 
 [ nil ] () = 0; 
 [ U61 ] (X0,X1) = 2 + 0; 
 [ U31 ] (X0,X1) = 0; 
 [ n__e ] () = 0; 
 [ U22 ] (X0,X1,X2) = 0; 
 [ U81 ] (X0,X1) = 0; 
 [ U46 ] (X0) = 0; 
 [ u ] () = 0; 
 [ U11 ] (X0,X1) = 0; 
 [ U73 ] (X0,X1) = 0; 
 [ U41 ] (X0,X1,X2) = 0; 
 [ a ] () = 0; 
 [ U25 ] (X0,X1) = 0; 
 [ U91 ] (X0,X1) = 0; 
 [ U54 ] (X0,X1,X2) = 0; 
 [ isPalListKind ] (X0) = 0; 
 [ Marked_isPalListKind ] (X0) = 2 + 2*X0 + 0; 
 [ U72 ] (X0,X1) = 2 + 0; 
 [ isQid ] (X0) = 0; 
 [ n__o ] () = 0; 
 [ U23 ] (X0,X1,X2) = 0; 
 [ isNePal ] (X0) = 3 + 0; 
 [ U51 ] (X0,X1,X2) = 0; 
 [ U13 ] (X0) = 0; 
 [ U74 ] (X0) = 0; 
 [ U44 ] (X0,X1,X2) = 0; 
 [ i ] () = 0; 
 [ U26 ] (X0) = 0; 
 [ n____ ] (X0,X1) = 3 + 1*X0 + 1*X1 + 0; 
 [ U56 ] (X0) = 0; 
 ]} 
{
 
DP termination of:
<Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))>
<Marked___(__(X,Y),Z) , Marked___(Y,Z)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
 ]} 
 ]} 

Cime worked for 1.841371 seconds (real time)
Cime Exit Status: 0