- : 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(isNeList(activate(V)))
[5] U12(tt) -> tt
[6] U21(tt,V1,V2) -> U22(isList(activate(V1)),activate(V2))
[7] U22(tt,V2) -> U23(isList(activate(V2)))
[8] U23(tt) -> tt
[9] U31(tt,V) -> U32(isQid(activate(V)))
[10] U32(tt) -> tt
[11] U41(tt,V1,V2) -> U42(isList(activate(V1)),activate(V2))
[12] U42(tt,V2) -> U43(isNeList(activate(V2)))
[13] U43(tt) -> tt
[14] U51(tt,V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
[15] U52(tt,V2) -> U53(isList(activate(V2)))
[16] U53(tt) -> tt
[17] U61(tt,V) -> U62(isQid(activate(V)))
[18] U62(tt) -> tt
[19] U71(tt,V) -> U72(isNePal(activate(V)))
[20] U72(tt) -> tt
[21] and(tt,X) -> activate(X)
[22] isList(V) -> U11(isPalListKind(activate(V)),activate(V))
[23] isList(n__nil) -> tt
[24] isList(n____(V1,V2)) ->
 U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),
  activate(V1),activate(V2))
[25] isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
[26] isNeList(n____(V1,V2)) ->
 U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),
  activate(V1),activate(V2))
[27] isNeList(n____(V1,V2)) ->
 U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),
  activate(V1),activate(V2))
[28] isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
[29] isNePal(n____(I,n____(P,I))) ->
 and(and(isQid(activate(I)),n__isPalListKind(activate(I))),
  n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
[30] isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
[31] isPal(n__nil) -> tt
[32] isPalListKind(n__a) -> tt
[33] isPalListKind(n__e) -> tt
[34] isPalListKind(n__i) -> tt
[35] isPalListKind(n__nil) -> tt
[36] isPalListKind(n__o) -> tt
[37] isPalListKind(n__u) -> tt
[38] isPalListKind(n____(V1,V2)) ->
 and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
[39] isQid(n__a) -> tt
[40] isQid(n__e) -> tt
[41] isQid(n__i) -> tt
[42] isQid(n__o) -> tt
[43] isQid(n__u) -> tt
[44] nil -> n__nil
[45] __(X1,X2) -> n____(X1,X2)
[46] isPalListKind(X) -> n__isPalListKind(X)
[47] and(X1,X2) -> n__and(X1,X2)
[48] isPal(X) -> n__isPal(X)
[49] a -> n__a
[50] e -> n__e
[51] i -> n__i
[52] o -> n__o
[53] u -> n__u
[54] activate(n__nil) -> nil
[55] activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
[56] activate(n__isPalListKind(X)) -> isPalListKind(X)
[57] activate(n__and(X1,X2)) -> and(activate(X1),X2)
[58] activate(n__isPal(X)) -> isPal(X)
[59] activate(n__a) -> a
[60] activate(n__e) -> e
[61] activate(n__i) -> i
[62] activate(n__o) -> o
[63] activate(n__u) -> u
[64] 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(isNeList(activate(V)))>
<Marked_U11(tt,V) , Marked_isNeList(activate(V))>
<Marked_U11(tt,V) , Marked_activate(V)>
<Marked_U21(tt,V1,V2) , Marked_U22(isList(activate(V1)),activate(V2))>
<Marked_U21(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U21(tt,V1,V2) , Marked_activate(V1)>
<Marked_U21(tt,V1,V2) , Marked_activate(V2)>
<Marked_U22(tt,V2) , Marked_U23(isList(activate(V2)))>
<Marked_U22(tt,V2) , Marked_isList(activate(V2))>
<Marked_U22(tt,V2) , Marked_activate(V2)>
<Marked_U31(tt,V) , Marked_U32(isQid(activate(V)))>
<Marked_U31(tt,V) , Marked_isQid(activate(V))>
<Marked_U31(tt,V) , Marked_activate(V)>
<Marked_U41(tt,V1,V2) , Marked_U42(isList(activate(V1)),activate(V2))>
<Marked_U41(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U41(tt,V1,V2) , Marked_activate(V1)>
<Marked_U41(tt,V1,V2) , Marked_activate(V2)>
<Marked_U42(tt,V2) , Marked_U43(isNeList(activate(V2)))>
<Marked_U42(tt,V2) , Marked_isNeList(activate(V2))>
<Marked_U42(tt,V2) , Marked_activate(V2)>
<Marked_U51(tt,V1,V2) , Marked_U52(isNeList(activate(V1)),activate(V2))>
<Marked_U51(tt,V1,V2) , Marked_isNeList(activate(V1))>
<Marked_U51(tt,V1,V2) , Marked_activate(V1)>
<Marked_U51(tt,V1,V2) , Marked_activate(V2)>
<Marked_U52(tt,V2) , Marked_U53(isList(activate(V2)))>
<Marked_U52(tt,V2) , Marked_isList(activate(V2))>
<Marked_U52(tt,V2) , Marked_activate(V2)>
<Marked_U61(tt,V) , Marked_U62(isQid(activate(V)))>
<Marked_U61(tt,V) , Marked_isQid(activate(V))>
<Marked_U61(tt,V) , Marked_activate(V)>
<Marked_U71(tt,V) , Marked_U72(isNePal(activate(V)))>
<Marked_U71(tt,V) , Marked_isNePal(activate(V))>
<Marked_U71(tt,V) , Marked_activate(V)>
<Marked_and(tt,X) , Marked_activate(X)>
<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(and(isPalListKind(activate(V1)),
                                           n__isPalListKind(activate(V2))),
                                activate(V1),activate(V2))>
<Marked_isList(n____(V1,V2)) , Marked_and(isPalListKind(activate(V1)),
                                n__isPalListKind(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(V2)>
<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(and(isPalListKind(activate(V1)),
                                             n__isPalListKind(activate(V2))),
                                  activate(V1),activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_and(isPalListKind(activate(V1)),
                                  n__isPalListKind(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(V2)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNeList(n____(V1,V2)) , Marked_U51(and(isPalListKind(activate(V1)),
                                             n__isPalListKind(activate(V2))),
                                  activate(V1),activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_and(isPalListKind(activate(V1)),
                                  n__isPalListKind(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(V2)>
<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,n____(P,I))) , Marked_and(and(isQid(activate(I)),
                                                   n__isPalListKind(activate(I)))
                                                   ,
                                        n__and(n__isPal(activate(P)),
                                         n__isPalListKind(activate(P))))>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_and(isQid(activate(I)),
                                        n__isPalListKind(activate(I)))>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_isQid(activate(I))>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)>
<Marked_isPal(V) , Marked_U71(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_and(isPalListKind(activate(V1)),
                                       n__isPalListKind(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___(activate(X1),activate(X2))>
<Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
<Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
<Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
<Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
<Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
<Marked_activate(n__isPal(X)) , Marked_isPal(X)>
<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 3 components:

{  <Marked_isNeList(n____(V1,V2)) , Marked_U51(and(isPalListKind(activate(V1)),
                                                n__isPalListKind(activate(V2))),
                                     activate(V1),activate(V2))> 
      --> <Marked_U51(tt,V1,V2) , Marked_isNeList(activate(V1))>
  <Marked_isNeList(n____(V1,V2)) , Marked_U51(and(isPalListKind(activate(V1)),
                                               n__isPalListKind(activate(V2))),
                                    activate(V1),activate(V2))> 
     --> <Marked_U51(tt,V1,V2) , Marked_U52(isNeList(activate(V1)),
                                  activate(V2))>
  <Marked_isNeList(n____(V1,V2)) , Marked_U41(and(isPalListKind(activate(V1)),
                                               n__isPalListKind(activate(V2))),
                                    activate(V1),activate(V2))> 
     --> <Marked_U41(tt,V1,V2) , Marked_isList(activate(V1))>
  <Marked_isNeList(n____(V1,V2)) , Marked_U41(and(isPalListKind(activate(V1)),
                                               n__isPalListKind(activate(V2))),
                                    activate(V1),activate(V2))> 
     --> <Marked_U41(tt,V1,V2) , Marked_U42(isList(activate(V1)),activate(V2))>
  <Marked_isList(n____(V1,V2)) , Marked_U21(and(isPalListKind(activate(V1)),
                                             n__isPalListKind(activate(V2))),
                                  activate(V1),activate(V2))> 
     --> <Marked_U21(tt,V1,V2) , Marked_isList(activate(V1))>
  <Marked_isList(n____(V1,V2)) , Marked_U21(and(isPalListKind(activate(V1)),
                                             n__isPalListKind(activate(V2))),
                                  activate(V1),activate(V2))> 
     --> <Marked_U21(tt,V1,V2) , Marked_U22(isList(activate(V1)),activate(V2))>
  <Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))> 
     --> <Marked_U11(tt,V) , Marked_isNeList(activate(V))>
  <Marked_U52(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_U21(and(isPalListKind(
                                                        activate(V1)),
                                                    n__isPalListKind(
                                                     activate(V2))),
                                         activate(V1),activate(V2))>
  <Marked_U52(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
  <Marked_U51(tt,V1,V2) , Marked_isNeList(activate(V1))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U51(and(isPalListKind(
                                                          activate(V1)),
                                                      n__isPalListKind(
                                                       activate(V2))),
                                           activate(V1),activate(V2))>
  <Marked_U51(tt,V1,V2) , Marked_isNeList(activate(V1))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U41(and(isPalListKind(
                                                          activate(V1)),
                                                      n__isPalListKind(
                                                       activate(V2))),
                                           activate(V1),activate(V2))>
  <Marked_U51(tt,V1,V2) , Marked_U52(isNeList(activate(V1)),activate(V2))> 
     --> <Marked_U52(tt,V2) , Marked_isList(activate(V2))>
  <Marked_U42(tt,V2) , Marked_isNeList(activate(V2))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U51(and(isPalListKind(
                                                          activate(V1)),
                                                      n__isPalListKind(
                                                       activate(V2))),
                                           activate(V1),activate(V2))>
  <Marked_U42(tt,V2) , Marked_isNeList(activate(V2))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U41(and(isPalListKind(
                                                          activate(V1)),
                                                      n__isPalListKind(
                                                       activate(V2))),
                                           activate(V1),activate(V2))>
  <Marked_U41(tt,V1,V2) , Marked_isList(activate(V1))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_U21(and(isPalListKind(
                                                        activate(V1)),
                                                    n__isPalListKind(
                                                     activate(V2))),
                                         activate(V1),activate(V2))>
  <Marked_U41(tt,V1,V2) , Marked_isList(activate(V1))> 
     --> <Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
  <Marked_U41(tt,V1,V2) , Marked_U42(isList(activate(V1)),activate(V2))> 
     --> <Marked_U42(tt,V2) , Marked_isNeList(activate(V2))>
  <Marked_U22(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_U21(and(isPalListKind(
                                                        activate(V1)),
                                                    n__isPalListKind(
                                                     activate(V2))),
                                         activate(V1),activate(V2))>
  <Marked_U22(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
  <Marked_U21(tt,V1,V2) , Marked_isList(activate(V1))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_U21(and(isPalListKind(
                                                        activate(V1)),
                                                    n__isPalListKind(
                                                     activate(V2))),
                                         activate(V1),activate(V2))>
  <Marked_U21(tt,V1,V2) , Marked_isList(activate(V1))> 
     --> <Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
  <Marked_U21(tt,V1,V2) , Marked_U22(isList(activate(V1)),activate(V2))> 
     --> <Marked_U22(tt,V2) , Marked_isList(activate(V2))>
  <Marked_U11(tt,V) , Marked_isNeList(activate(V))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U51(and(isPalListKind(
                                                          activate(V1)),
                                                      n__isPalListKind(
                                                       activate(V2))),
                                           activate(V1),activate(V2))>
  <Marked_U11(tt,V) , Marked_isNeList(activate(V))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U41(and(isPalListKind(
                                                          activate(V1)),
                                                      n__isPalListKind(
                                                       activate(V2))),
                                           activate(V1),activate(V2))>
}

{  <Marked_activate(n__isPal(X)) , Marked_isPal(X)> 
      --> <Marked_isPal(V) , Marked_activate(V)>
  <Marked_activate(n__isPal(X)) , Marked_isPal(X)> 
     --> <Marked_isPal(V) , Marked_activate(V)>
  <Marked_activate(n__isPal(X)) , Marked_isPal(X)> 
     --> <Marked_isPal(V) , Marked_isPalListKind(activate(V))>
  <Marked_activate(n__isPal(X)) , Marked_isPal(X)> 
     --> <Marked_isPal(V) , Marked_U71(isPalListKind(activate(V)),activate(V))>
  <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V2)>
  <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V1)>
  <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_isPalListKind(activate(
                                                                    V1))>
  <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_and(isPalListKind(
                                                           activate(V1)),
                                                n__isPalListKind(activate(V2)))>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X2)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X2)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X2)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X2)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X2)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X2)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_isPalListKind(activate(V1))> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_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_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_and(isPalListKind(
                                                           activate(V1)),
                                                n__isPalListKind(activate(V2)))>
  <Marked_isPalListKind(n____(V1,V2)) , Marked_and(isPalListKind(activate(V1)),
                                         n__isPalListKind(activate(V2)))> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isPal(V) , Marked_isPalListKind(activate(V))> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V2)>
  <Marked_isPal(V) , Marked_isPalListKind(activate(V))> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V1)>
  <Marked_isPal(V) , Marked_isPalListKind(activate(V))> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_isPalListKind(activate(
                                                                    V1))>
  <Marked_isPal(V) , Marked_isPalListKind(activate(V))> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_and(isPalListKind(
                                                           activate(V1)),
                                                n__isPalListKind(activate(V2)))>
  <Marked_isPal(V) , Marked_U71(isPalListKind(activate(V)),activate(V))> 
     --> <Marked_U71(tt,V) , Marked_activate(V)>
  <Marked_isPal(V) , Marked_U71(isPalListKind(activate(V)),activate(V))> 
     --> <Marked_U71(tt,V) , Marked_isNePal(activate(V))>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_and(isQid(activate(I)),
                                          n__isPalListKind(activate(I)))> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_and(and(isQid(activate(I)),
                                                     n__isPalListKind(
                                                      activate(I))),
                                          n__and(n__isPal(activate(P)),
                                           n__isPalListKind(activate(P))))> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(V) , Marked_isPalListKind(activate(V))> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V2)>
  <Marked_isNePal(V) , Marked_isPalListKind(activate(V))> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_activate(V1)>
  <Marked_isNePal(V) , Marked_isPalListKind(activate(V))> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_isPalListKind(activate(
                                                                    V1))>
  <Marked_isNePal(V) , Marked_isPalListKind(activate(V))> 
     --> <Marked_isPalListKind(n____(V1,V2)) , Marked_and(isPalListKind(
                                                           activate(V1)),
                                                n__isPalListKind(activate(V2)))>
  <Marked_isNePal(V) , Marked_U61(isPalListKind(activate(V)),activate(V))> 
     --> <Marked_U61(tt,V) , Marked_activate(V)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_U71(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_U71(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_U71(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_U71(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_U71(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_U71(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_U71(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)>
  <Marked_U71(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)>
  <Marked_U71(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)>
  <Marked_U71(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)>
  <Marked_U71(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(n____(I,n____(P,I))) , Marked_and(isQid(activate(I)),
                                                 n__isPalListKind(activate(I)))>
  <Marked_U71(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(n____(I,n____(P,I))) , Marked_and(and(isQid(
                                                                activate(
                                                                 I)),
                                                            n__isPalListKind(
                                                             activate(
                                                              I))),
                                                 n__and(n__isPal(activate(P)),
                                                  n__isPalListKind(activate(P))))
                                                 >
  <Marked_U71(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(V) , Marked_activate(V)>
  <Marked_U71(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(V) , Marked_activate(V)>
  <Marked_U71(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(V) , Marked_isPalListKind(activate(V))>
  <Marked_U71(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(V) , Marked_U61(isPalListKind(activate(V)),
                               activate(V))>
  <Marked_U61(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_U61(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_U61(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_U61(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
  <Marked_U61(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_U61(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
}

{  <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) >= tt ;
  isNeList(n____(V1,V2)) >= U41(and(isPalListKind(activate(V1)),
                                 n__isPalListKind(activate(V2))),activate(V1),
                             activate(V2)) ;
  isNeList(n____(V1,V2)) >= U51(and(isPalListKind(activate(V1)),
                                 n__isPalListKind(activate(V2))),activate(V1),
                             activate(V2)) ;
  isNeList(V) >= U31(isPalListKind(activate(V)),activate(V)) ;
  activate(n__nil) >= nil ;
  activate(n__isPalListKind(X)) >= isPalListKind(X) ;
  activate(n____(X1,X2)) >= __(activate(X1),activate(X2)) ;
  activate(n__and(X1,X2)) >= and(activate(X1),X2) ;
  activate(n__isPal(X)) >= isPal(X) ;
  activate(n__a) >= a ;
  activate(n__e) >= e ;
  activate(n__i) >= i ;
  activate(n__o) >= o ;
  activate(n__u) >= u ;
  activate(X) >= X ;
  U11(tt,V) >= U12(isNeList(activate(V))) ;
  U22(tt,V2) >= U23(isList(activate(V2))) ;
  isList(n__nil) >= tt ;
  isList(n____(V1,V2)) >= U21(and(isPalListKind(activate(V1)),
                               n__isPalListKind(activate(V2))),activate(V1),
                           activate(V2)) ;
  isList(V) >= U11(isPalListKind(activate(V)),activate(V)) ;
  U21(tt,V1,V2) >= U22(isList(activate(V1)),activate(V2)) ;
  U23(tt) >= tt ;
  U32(tt) >= tt ;
  isQid(n__a) >= tt ;
  isQid(n__e) >= tt ;
  isQid(n__i) >= tt ;
  isQid(n__o) >= tt ;
  isQid(n__u) >= tt ;
  U31(tt,V) >= U32(isQid(activate(V))) ;
  U42(tt,V2) >= U43(isNeList(activate(V2))) ;
  U41(tt,V1,V2) >= U42(isList(activate(V1)),activate(V2)) ;
  U43(tt) >= tt ;
  U52(tt,V2) >= U53(isList(activate(V2))) ;
  U51(tt,V1,V2) >= U52(isNeList(activate(V1)),activate(V2)) ;
  U53(tt) >= tt ;
  U62(tt) >= tt ;
  U61(tt,V) >= U62(isQid(activate(V))) ;
  U72(tt) >= tt ;
  isNePal(n____(I,n____(P,I))) >= and(and(isQid(activate(I)),
                                       n__isPalListKind(activate(I))),
                                   n__and(n__isPal(activate(P)),
                                    n__isPalListKind(activate(P)))) ;
  isNePal(V) >= U61(isPalListKind(activate(V)),activate(V)) ;
  U71(tt,V) >= U72(isNePal(activate(V))) ;
  and(tt,X) >= activate(X) ;
  and(X1,X2) >= n__and(X1,X2) ;
  isPalListKind(n__nil) >= tt ;
  isPalListKind(n____(V1,V2)) >= and(isPalListKind(activate(V1)),
                                  n__isPalListKind(activate(V2))) ;
  isPalListKind(n__a) >= tt ;
  isPalListKind(n__e) >= tt ;
  isPalListKind(n__i) >= tt ;
  isPalListKind(n__o) >= tt ;
  isPalListKind(n__u) >= tt ;
  isPalListKind(X) >= n__isPalListKind(X) ;
  isPal(n__nil) >= tt ;
  isPal(X) >= n__isPal(X) ;
  isPal(V) >= U71(isPalListKind(activate(V)),activate(V)) ;
  a >= n__a ;
  e >= n__e ;
  i >= n__i ;
  o >= n__o ;
  u >= n__u ;
  Marked_isNeList(n____(V1,V2)) >= Marked_U51(and(isPalListKind(activate(V1)),
                                               n__isPalListKind(activate(V2))),
                                    activate(V1),activate(V2)) ;
  Marked_isNeList(n____(V1,V2)) >= Marked_U41(and(isPalListKind(activate(V1)),
                                               n__isPalListKind(activate(V2))),
                                    activate(V1),activate(V2)) ;
  Marked_U51(tt,V1,V2) >= Marked_isNeList(activate(V1)) ;
  Marked_U51(tt,V1,V2) >= Marked_U52(isNeList(activate(V1)),activate(V2)) ;
  Marked_U41(tt,V1,V2) >= Marked_isList(activate(V1)) ;
  Marked_U41(tt,V1,V2) >= Marked_U42(isList(activate(V1)),activate(V2)) ;
  Marked_isList(n____(V1,V2)) >= Marked_U21(and(isPalListKind(activate(V1)),
                                             n__isPalListKind(activate(V2))),
                                  activate(V1),activate(V2)) ;
  Marked_isList(V) >= Marked_U11(isPalListKind(activate(V)),activate(V)) ;
  Marked_U21(tt,V1,V2) >= Marked_isList(activate(V1)) ;
  Marked_U21(tt,V1,V2) >= Marked_U22(isList(activate(V1)),activate(V2)) ;
  Marked_U11(tt,V) >= Marked_isNeList(activate(V)) ;
  Marked_U52(tt,V2) >= Marked_isList(activate(V2)) ;
  Marked_U42(tt,V2) >= Marked_isNeList(activate(V2)) ;
  Marked_U22(tt,V2) >= Marked_isList(activate(V2)) ;
 }
 + Disjunctions:{ 
{
  Marked_isNeList(n____(V1,V2)) > Marked_U51(and(isPalListKind(activate(V1)),
                                              n__isPalListKind(activate(V2))),
                                   activate(V1),activate(V2)) ;
 }
{
  Marked_isNeList(n____(V1,V2)) > Marked_U41(and(isPalListKind(activate(V1)),
                                              n__isPalListKind(activate(V2))),
                                   activate(V1),activate(V2)) ;
 }
{
  Marked_U51(tt,V1,V2) > Marked_isNeList(activate(V1)) ;
 }
{
  Marked_U51(tt,V1,V2) > Marked_U52(isNeList(activate(V1)),activate(V2)) ;
 }
{
  Marked_U41(tt,V1,V2) > Marked_isList(activate(V1)) ;
 }
{
  Marked_U41(tt,V1,V2) > Marked_U42(isList(activate(V1)),activate(V2)) ;
 }
{
  Marked_isList(n____(V1,V2)) > Marked_U21(and(isPalListKind(activate(V1)),
                                            n__isPalListKind(activate(V2))),
                                 activate(V1),activate(V2)) ;
 }
{
  Marked_isList(V) > Marked_U11(isPalListKind(activate(V)),activate(V)) ;
 }
{
  Marked_U21(tt,V1,V2) > Marked_isList(activate(V1)) ;
 }
{
  Marked_U21(tt,V1,V2) > Marked_U22(isList(activate(V1)),activate(V2)) ;
 }
{
  Marked_U11(tt,V) > Marked_isNeList(activate(V)) ;
 }
{
  Marked_U52(tt,V2) > Marked_isList(activate(V2)) ;
 }
{
  Marked_U42(tt,V2) > Marked_isNeList(activate(V2)) ;
 }
{
  Marked_U22(tt,V2) > Marked_isList(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) >= tt
constraint: isNeList(n____(V1,V2)) >= U41(and(isPalListKind(activate(V1)),
                                           n__isPalListKind(activate(V2))),
                                       activate(V1),activate(V2))
constraint: isNeList(n____(V1,V2)) >= U51(and(isPalListKind(activate(V1)),
                                           n__isPalListKind(activate(V2))),
                                       activate(V1),activate(V2))
constraint: isNeList(V) >= U31(isPalListKind(activate(V)),activate(V))
constraint: activate(n__nil) >= nil
constraint: activate(n__isPalListKind(X)) >= isPalListKind(X)
constraint: activate(n____(X1,X2)) >= __(activate(X1),activate(X2))
constraint: activate(n__and(X1,X2)) >= and(activate(X1),X2)
constraint: activate(n__isPal(X)) >= isPal(X)
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(isNeList(activate(V)))
constraint: U22(tt,V2) >= U23(isList(activate(V2)))
constraint: isList(n__nil) >= tt
constraint: isList(n____(V1,V2)) >= U21(and(isPalListKind(activate(V1)),
                                         n__isPalListKind(activate(V2))),
                                     activate(V1),activate(V2))
constraint: isList(V) >= U11(isPalListKind(activate(V)),activate(V))
constraint: U21(tt,V1,V2) >= U22(isList(activate(V1)),activate(V2))
constraint: U23(tt) >= tt
constraint: U32(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: U31(tt,V) >= U32(isQid(activate(V)))
constraint: U42(tt,V2) >= U43(isNeList(activate(V2)))
constraint: U41(tt,V1,V2) >= U42(isList(activate(V1)),activate(V2))
constraint: U43(tt) >= tt
constraint: U52(tt,V2) >= U53(isList(activate(V2)))
constraint: U51(tt,V1,V2) >= U52(isNeList(activate(V1)),activate(V2))
constraint: U53(tt) >= tt
constraint: U62(tt) >= tt
constraint: U61(tt,V) >= U62(isQid(activate(V)))
constraint: U72(tt) >= tt
constraint: isNePal(n____(I,n____(P,I))) >= and(and(isQid(activate(I)),
                                                 n__isPalListKind(activate(I))),
                                             n__and(n__isPal(activate(P)),
                                              n__isPalListKind(activate(P))))
constraint: isNePal(V) >= U61(isPalListKind(activate(V)),activate(V))
constraint: U71(tt,V) >= U72(isNePal(activate(V)))
constraint: and(tt,X) >= activate(X)
constraint: and(X1,X2) >= n__and(X1,X2)
constraint: isPalListKind(n__nil) >= tt
constraint: isPalListKind(n____(V1,V2)) >= and(isPalListKind(activate(V1)),
                                            n__isPalListKind(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: isPalListKind(X) >= n__isPalListKind(X)
constraint: isPal(n__nil) >= tt
constraint: isPal(X) >= n__isPal(X)
constraint: isPal(V) >= U71(isPalListKind(activate(V)),activate(V))
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(and(isPalListKind(
                                                             activate(
                                                              V1)),
                                                         n__isPalListKind(
                                                          activate(V2))),
                                              activate(V1),activate(V2))
constraint: Marked_isNeList(n____(V1,V2)) >= Marked_U41(and(isPalListKind(
                                                             activate(
                                                              V1)),
                                                         n__isPalListKind(
                                                          activate(V2))),
                                              activate(V1),activate(V2))
constraint: Marked_U51(tt,V1,V2) >= Marked_isNeList(activate(V1))
constraint: Marked_U51(tt,V1,V2) >= Marked_U52(isNeList(activate(V1)),
                                     activate(V2))
constraint: Marked_U41(tt,V1,V2) >= Marked_isList(activate(V1))
constraint: Marked_U41(tt,V1,V2) >= Marked_U42(isList(activate(V1)),
                                     activate(V2))
constraint: Marked_isList(n____(V1,V2)) >= Marked_U21(and(isPalListKind(
                                                           activate(V1)),
                                                       n__isPalListKind(
                                                        activate(V2))),
                                            activate(V1),activate(V2))
constraint: Marked_isList(V) >= Marked_U11(isPalListKind(activate(V)),
                                 activate(V))
constraint: Marked_U21(tt,V1,V2) >= Marked_isList(activate(V1))
constraint: Marked_U21(tt,V1,V2) >= Marked_U22(isList(activate(V1)),
                                     activate(V2))
constraint: Marked_U11(tt,V) >= Marked_isNeList(activate(V))
constraint: Marked_U52(tt,V2) >= Marked_isList(activate(V2))
constraint: Marked_U42(tt,V2) >= Marked_isNeList(activate(V2))
constraint: Marked_U22(tt,V2) >= Marked_isList(activate(V2))
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) >= tt ;
  isNeList(n____(V1,V2)) >= U41(and(isPalListKind(activate(V1)),
                                 n__isPalListKind(activate(V2))),activate(V1),
                             activate(V2)) ;
  isNeList(n____(V1,V2)) >= U51(and(isPalListKind(activate(V1)),
                                 n__isPalListKind(activate(V2))),activate(V1),
                             activate(V2)) ;
  isNeList(V) >= U31(isPalListKind(activate(V)),activate(V)) ;
  activate(n__nil) >= nil ;
  activate(n__isPalListKind(X)) >= isPalListKind(X) ;
  activate(n____(X1,X2)) >= __(activate(X1),activate(X2)) ;
  activate(n__and(X1,X2)) >= and(activate(X1),X2) ;
  activate(n__isPal(X)) >= isPal(X) ;
  activate(n__a) >= a ;
  activate(n__e) >= e ;
  activate(n__i) >= i ;
  activate(n__o) >= o ;
  activate(n__u) >= u ;
  activate(X) >= X ;
  U11(tt,V) >= U12(isNeList(activate(V))) ;
  U22(tt,V2) >= U23(isList(activate(V2))) ;
  isList(n__nil) >= tt ;
  isList(n____(V1,V2)) >= U21(and(isPalListKind(activate(V1)),
                               n__isPalListKind(activate(V2))),activate(V1),
                           activate(V2)) ;
  isList(V) >= U11(isPalListKind(activate(V)),activate(V)) ;
  U21(tt,V1,V2) >= U22(isList(activate(V1)),activate(V2)) ;
  U23(tt) >= tt ;
  U32(tt) >= tt ;
  isQid(n__a) >= tt ;
  isQid(n__e) >= tt ;
  isQid(n__i) >= tt ;
  isQid(n__o) >= tt ;
  isQid(n__u) >= tt ;
  U31(tt,V) >= U32(isQid(activate(V))) ;
  U42(tt,V2) >= U43(isNeList(activate(V2))) ;
  U41(tt,V1,V2) >= U42(isList(activate(V1)),activate(V2)) ;
  U43(tt) >= tt ;
  U52(tt,V2) >= U53(isList(activate(V2))) ;
  U51(tt,V1,V2) >= U52(isNeList(activate(V1)),activate(V2)) ;
  U53(tt) >= tt ;
  U62(tt) >= tt ;
  U61(tt,V) >= U62(isQid(activate(V))) ;
  U72(tt) >= tt ;
  isNePal(n____(I,n____(P,I))) >= and(and(isQid(activate(I)),
                                       n__isPalListKind(activate(I))),
                                   n__and(n__isPal(activate(P)),
                                    n__isPalListKind(activate(P)))) ;
  isNePal(V) >= U61(isPalListKind(activate(V)),activate(V)) ;
  U71(tt,V) >= U72(isNePal(activate(V))) ;
  and(tt,X) >= activate(X) ;
  and(X1,X2) >= n__and(X1,X2) ;
  isPalListKind(n__nil) >= tt ;
  isPalListKind(n____(V1,V2)) >= and(isPalListKind(activate(V1)),
                                  n__isPalListKind(activate(V2))) ;
  isPalListKind(n__a) >= tt ;
  isPalListKind(n__e) >= tt ;
  isPalListKind(n__i) >= tt ;
  isPalListKind(n__o) >= tt ;
  isPalListKind(n__u) >= tt ;
  isPalListKind(X) >= n__isPalListKind(X) ;
  isPal(n__nil) >= tt ;
  isPal(X) >= n__isPal(X) ;
  isPal(V) >= U71(isPalListKind(activate(V)),activate(V)) ;
  a >= n__a ;
  e >= n__e ;
  i >= n__i ;
  o >= n__o ;
  u >= n__u ;
  Marked_activate(n__isPalListKind(X)) >= Marked_isPalListKind(X) ;
  Marked_activate(n____(X1,X2)) >= Marked_activate(X1) ;
  Marked_activate(n____(X1,X2)) >= Marked_activate(X2) ;
  Marked_activate(n__and(X1,X2)) >= Marked_activate(X1) ;
  Marked_activate(n__and(X1,X2)) >= Marked_and(activate(X1),X2) ;
  Marked_activate(n__isPal(X)) >= Marked_isPal(X) ;
  Marked_isPal(V) >= Marked_activate(V) ;
  Marked_isPal(V) >= Marked_isPalListKind(activate(V)) ;
  Marked_isPal(V) >= Marked_U71(isPalListKind(activate(V)),activate(V)) ;
  Marked_and(tt,X) >= Marked_activate(X) ;
  Marked_isPalListKind(n____(V1,V2)) >= Marked_activate(V1) ;
  Marked_isPalListKind(n____(V1,V2)) >= Marked_activate(V2) ;
  Marked_isPalListKind(n____(V1,V2)) >= Marked_and(isPalListKind(activate(V1)),
                                         n__isPalListKind(activate(V2))) ;
  Marked_isPalListKind(n____(V1,V2)) >= Marked_isPalListKind(activate(V1)) ;
  Marked_U71(tt,V) >= Marked_activate(V) ;
  Marked_U71(tt,V) >= Marked_isNePal(activate(V)) ;
  Marked_isNePal(n____(I,n____(P,I))) >= Marked_activate(I) ;
  Marked_isNePal(n____(I,n____(P,I))) >= Marked_activate(P) ;
  Marked_isNePal(n____(I,n____(P,I))) >= Marked_and(isQid(activate(I)),
                                          n__isPalListKind(activate(I))) ;
  Marked_isNePal(n____(I,n____(P,I))) >= Marked_and(and(isQid(activate(I)),
                                                     n__isPalListKind(
                                                      activate(I))),
                                          n__and(n__isPal(activate(P)),
                                           n__isPalListKind(activate(P)))) ;
  Marked_isNePal(V) >= Marked_activate(V) ;
  Marked_isNePal(V) >= Marked_isPalListKind(activate(V)) ;
  Marked_isNePal(V) >= Marked_U61(isPalListKind(activate(V)),activate(V)) ;
  Marked_U61(tt,V) >= Marked_activate(V) ;
 }
 + Disjunctions:{ 
{
  Marked_activate(n__isPalListKind(X)) > Marked_isPalListKind(X) ;
 }
{
  Marked_activate(n____(X1,X2)) > Marked_activate(X1) ;
 }
{
  Marked_activate(n____(X1,X2)) > Marked_activate(X2) ;
 }
{
  Marked_activate(n__and(X1,X2)) > Marked_activate(X1) ;
 }
{
  Marked_activate(n__and(X1,X2)) > Marked_and(activate(X1),X2) ;
 }
{
  Marked_activate(n__isPal(X)) > Marked_isPal(X) ;
 }
{
  Marked_isPal(V) > Marked_activate(V) ;
 }
{
  Marked_isPal(V) > Marked_isPalListKind(activate(V)) ;
 }
{
  Marked_isPal(V) > Marked_U71(isPalListKind(activate(V)),activate(V)) ;
 }
{
  Marked_and(tt,X) > Marked_activate(X) ;
 }
{
  Marked_isPalListKind(n____(V1,V2)) > Marked_activate(V1) ;
 }
{
  Marked_isPalListKind(n____(V1,V2)) > Marked_activate(V2) ;
 }
{
  Marked_isPalListKind(n____(V1,V2)) > Marked_and(isPalListKind(activate(V1)),
                                        n__isPalListKind(activate(V2))) ;
 }
{
  Marked_isPalListKind(n____(V1,V2)) > Marked_isPalListKind(activate(V1)) ;
 }
{
  Marked_U71(tt,V) > Marked_activate(V) ;
 }
{
  Marked_U71(tt,V) > Marked_isNePal(activate(V)) ;
 }
{
  Marked_isNePal(n____(I,n____(P,I))) > Marked_activate(I) ;
 }
{
  Marked_isNePal(n____(I,n____(P,I))) > Marked_activate(P) ;
 }
{
  Marked_isNePal(n____(I,n____(P,I))) > Marked_and(isQid(activate(I)),
                                         n__isPalListKind(activate(I))) ;
 }
{
  Marked_isNePal(n____(I,n____(P,I))) > Marked_and(and(isQid(activate(I)),
                                                    n__isPalListKind(
                                                     activate(I))),
                                         n__and(n__isPal(activate(P)),
                                          n__isPalListKind(activate(P)))) ;
 }
{
  Marked_isNePal(V) > Marked_activate(V) ;
 }
{
  Marked_isNePal(V) > Marked_isPalListKind(activate(V)) ;
 }
{
  Marked_isNePal(V) > Marked_U61(isPalListKind(activate(V)),activate(V)) ;
 }
{
  Marked_U61(tt,V) > Marked_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) >= tt
constraint: isNeList(n____(V1,V2)) >= U41(and(isPalListKind(activate(V1)),
                                           n__isPalListKind(activate(V2))),
                                       activate(V1),activate(V2))
constraint: isNeList(n____(V1,V2)) >= U51(and(isPalListKind(activate(V1)),
                                           n__isPalListKind(activate(V2))),
                                       activate(V1),activate(V2))
constraint: isNeList(V) >= U31(isPalListKind(activate(V)),activate(V))
constraint: activate(n__nil) >= nil
constraint: activate(n__isPalListKind(X)) >= isPalListKind(X)
constraint: activate(n____(X1,X2)) >= __(activate(X1),activate(X2))
constraint: activate(n__and(X1,X2)) >= and(activate(X1),X2)
constraint: activate(n__isPal(X)) >= isPal(X)
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(isNeList(activate(V)))
constraint: U22(tt,V2) >= U23(isList(activate(V2)))
constraint: isList(n__nil) >= tt
constraint: isList(n____(V1,V2)) >= U21(and(isPalListKind(activate(V1)),
                                         n__isPalListKind(activate(V2))),
                                     activate(V1),activate(V2))
constraint: isList(V) >= U11(isPalListKind(activate(V)),activate(V))
constraint: U21(tt,V1,V2) >= U22(isList(activate(V1)),activate(V2))
constraint: U23(tt) >= tt
constraint: U32(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: U31(tt,V) >= U32(isQid(activate(V)))
constraint: U42(tt,V2) >= U43(isNeList(activate(V2)))
constraint: U41(tt,V1,V2) >= U42(isList(activate(V1)),activate(V2))
constraint: U43(tt) >= tt
constraint: U52(tt,V2) >= U53(isList(activate(V2)))
constraint: U51(tt,V1,V2) >= U52(isNeList(activate(V1)),activate(V2))
constraint: U53(tt) >= tt
constraint: U62(tt) >= tt
constraint: U61(tt,V) >= U62(isQid(activate(V)))
constraint: U72(tt) >= tt
constraint: isNePal(n____(I,n____(P,I))) >= and(and(isQid(activate(I)),
                                                 n__isPalListKind(activate(I))),
                                             n__and(n__isPal(activate(P)),
                                              n__isPalListKind(activate(P))))
constraint: isNePal(V) >= U61(isPalListKind(activate(V)),activate(V))
constraint: U71(tt,V) >= U72(isNePal(activate(V)))
constraint: and(tt,X) >= activate(X)
constraint: and(X1,X2) >= n__and(X1,X2)
constraint: isPalListKind(n__nil) >= tt
constraint: isPalListKind(n____(V1,V2)) >= and(isPalListKind(activate(V1)),
                                            n__isPalListKind(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: isPalListKind(X) >= n__isPalListKind(X)
constraint: isPal(n__nil) >= tt
constraint: isPal(X) >= n__isPal(X)
constraint: isPal(V) >= U71(isPalListKind(activate(V)),activate(V))
constraint: a >= n__a
constraint: e >= n__e
constraint: i >= n__i
constraint: o >= n__o
constraint: u >= n__u
constraint: Marked_activate(n__isPalListKind(X)) >= Marked_isPalListKind(X)
constraint: Marked_activate(n____(X1,X2)) >= Marked_activate(X1)
constraint: Marked_activate(n____(X1,X2)) >= Marked_activate(X2)
constraint: Marked_activate(n__and(X1,X2)) >= Marked_activate(X1)
constraint: Marked_activate(n__and(X1,X2)) >= Marked_and(activate(X1),X2)
constraint: Marked_activate(n__isPal(X)) >= Marked_isPal(X)
constraint: Marked_isPal(V) >= Marked_activate(V)
constraint: Marked_isPal(V) >= Marked_isPalListKind(activate(V))
constraint: Marked_isPal(V) >= Marked_U71(isPalListKind(activate(V)),
                                activate(V))
constraint: Marked_and(tt,X) >= Marked_activate(X)
constraint: Marked_isPalListKind(n____(V1,V2)) >= Marked_activate(V1)
constraint: Marked_isPalListKind(n____(V1,V2)) >= Marked_activate(V2)
constraint: Marked_isPalListKind(n____(V1,V2)) >= Marked_and(isPalListKind(
                                                              activate(
                                                               V1)),
                                                   n__isPalListKind(activate(
                                                                    V2)))
constraint: Marked_isPalListKind(n____(V1,V2)) >= Marked_isPalListKind(
                                                   activate(V1))
constraint: Marked_U71(tt,V) >= Marked_activate(V)
constraint: Marked_U71(tt,V) >= Marked_isNePal(activate(V))
constraint: Marked_isNePal(n____(I,n____(P,I))) >= Marked_activate(I)
constraint: Marked_isNePal(n____(I,n____(P,I))) >= Marked_activate(P)
constraint: Marked_isNePal(n____(I,n____(P,I))) >= Marked_and(isQid(activate(I)),
                                                    n__isPalListKind(
                                                     activate(I)))
constraint: Marked_isNePal(n____(I,n____(P,I))) >= Marked_and(and(isQid(
                                                                   activate(
                                                                    I)),
                                                               n__isPalListKind(
                                                                activate(
                                                                 I))),
                                                    n__and(n__isPal(activate(P)),
                                                     n__isPalListKind(
                                                      activate(P))))
constraint: Marked_isNePal(V) >= Marked_activate(V)
constraint: Marked_isNePal(V) >= Marked_isPalListKind(activate(V))
constraint: Marked_isNePal(V) >= Marked_U61(isPalListKind(activate(V)),
                                  activate(V))
constraint: Marked_U61(tt,V) >= Marked_activate(V)
APPLY CRITERIA (Subterm criterion)

ST: Marked___ -> 1

APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_activate(n__isPal(X)) , Marked_isPal(X)> 
      --> <Marked_isPal(V) , Marked_activate(V)>
  <Marked_activate(n__isPal(X)) , Marked_isPal(X)> 
     --> <Marked_isPal(V) , Marked_activate(V)>
  <Marked_activate(n__isPal(X)) , Marked_isPal(X)> 
     --> <Marked_isPal(V) , Marked_U71(isPalListKind(activate(V)),activate(V))>
  <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isPal(V) , Marked_U71(isPalListKind(activate(V)),activate(V))> 
     --> <Marked_U71(tt,V) , Marked_activate(V)>
  <Marked_isPal(V) , Marked_U71(isPalListKind(activate(V)),activate(V))> 
     --> <Marked_U71(tt,V) , Marked_isNePal(activate(V))>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_isNePal(V) , Marked_U61(isPalListKind(activate(V)),activate(V))> 
     --> <Marked_U61(tt,V) , Marked_activate(V)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_U71(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_U71(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_U71(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_U71(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(V) , Marked_activate(V)>
  <Marked_U71(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(V) , Marked_activate(V)>
  <Marked_U71(tt,V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(V) , Marked_U61(isPalListKind(activate(V)),
                               activate(V))>
  <Marked_U61(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_U61(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_U61(tt,V) , Marked_activate(V)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
}
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) >= tt ;
  isNeList(n____(V1,V2)) >= U41(and(isPalListKind(activate(V1)),
                                 n__isPalListKind(activate(V2))),activate(V1),
                             activate(V2)) ;
  isNeList(n____(V1,V2)) >= U51(and(isPalListKind(activate(V1)),
                                 n__isPalListKind(activate(V2))),activate(V1),
                             activate(V2)) ;
  isNeList(V) >= U31(isPalListKind(activate(V)),activate(V)) ;
  activate(n__nil) >= nil ;
  activate(n__isPalListKind(X)) >= isPalListKind(X) ;
  activate(n____(X1,X2)) >= __(activate(X1),activate(X2)) ;
  activate(n__and(X1,X2)) >= and(activate(X1),X2) ;
  activate(n__isPal(X)) >= isPal(X) ;
  activate(n__a) >= a ;
  activate(n__e) >= e ;
  activate(n__i) >= i ;
  activate(n__o) >= o ;
  activate(n__u) >= u ;
  activate(X) >= X ;
  U11(tt,V) >= U12(isNeList(activate(V))) ;
  U22(tt,V2) >= U23(isList(activate(V2))) ;
  isList(n__nil) >= tt ;
  isList(n____(V1,V2)) >= U21(and(isPalListKind(activate(V1)),
                               n__isPalListKind(activate(V2))),activate(V1),
                           activate(V2)) ;
  isList(V) >= U11(isPalListKind(activate(V)),activate(V)) ;
  U21(tt,V1,V2) >= U22(isList(activate(V1)),activate(V2)) ;
  U23(tt) >= tt ;
  U32(tt) >= tt ;
  isQid(n__a) >= tt ;
  isQid(n__e) >= tt ;
  isQid(n__i) >= tt ;
  isQid(n__o) >= tt ;
  isQid(n__u) >= tt ;
  U31(tt,V) >= U32(isQid(activate(V))) ;
  U42(tt,V2) >= U43(isNeList(activate(V2))) ;
  U41(tt,V1,V2) >= U42(isList(activate(V1)),activate(V2)) ;
  U43(tt) >= tt ;
  U52(tt,V2) >= U53(isList(activate(V2))) ;
  U51(tt,V1,V2) >= U52(isNeList(activate(V1)),activate(V2)) ;
  U53(tt) >= tt ;
  U62(tt) >= tt ;
  U61(tt,V) >= U62(isQid(activate(V))) ;
  U72(tt) >= tt ;
  isNePal(n____(I,n____(P,I))) >= and(and(isQid(activate(I)),
                                       n__isPalListKind(activate(I))),
                                   n__and(n__isPal(activate(P)),
                                    n__isPalListKind(activate(P)))) ;
  isNePal(V) >= U61(isPalListKind(activate(V)),activate(V)) ;
  U71(tt,V) >= U72(isNePal(activate(V))) ;
  and(tt,X) >= activate(X) ;
  and(X1,X2) >= n__and(X1,X2) ;
  isPalListKind(n__nil) >= tt ;
  isPalListKind(n____(V1,V2)) >= and(isPalListKind(activate(V1)),
                                  n__isPalListKind(activate(V2))) ;
  isPalListKind(n__a) >= tt ;
  isPalListKind(n__e) >= tt ;
  isPalListKind(n__i) >= tt ;
  isPalListKind(n__o) >= tt ;
  isPalListKind(n__u) >= tt ;
  isPalListKind(X) >= n__isPalListKind(X) ;
  isPal(n__nil) >= tt ;
  isPal(X) >= n__isPal(X) ;
  isPal(V) >= U71(isPalListKind(activate(V)),activate(V)) ;
  a >= n__a ;
  e >= n__e ;
  i >= n__i ;
  o >= n__o ;
  u >= n__u ;
  Marked_activate(n__and(X1,X2)) >= Marked_activate(X1) ;
  Marked_activate(n__and(X1,X2)) >= Marked_and(activate(X1),X2) ;
  Marked_activate(n__isPal(X)) >= Marked_isPal(X) ;
  Marked_isPal(V) >= Marked_activate(V) ;
  Marked_isPal(V) >= Marked_U71(isPalListKind(activate(V)),activate(V)) ;
  Marked_and(tt,X) >= Marked_activate(X) ;
  Marked_U71(tt,V) >= Marked_activate(V) ;
  Marked_U71(tt,V) >= Marked_isNePal(activate(V)) ;
  Marked_isNePal(V) >= Marked_activate(V) ;
  Marked_isNePal(V) >= Marked_U61(isPalListKind(activate(V)),activate(V)) ;
  Marked_U61(tt,V) >= Marked_activate(V) ;
 }
 + Disjunctions:{ 
{
  Marked_activate(n__and(X1,X2)) > Marked_activate(X1) ;
 }
{
  Marked_activate(n__and(X1,X2)) > Marked_and(activate(X1),X2) ;
 }
{
  Marked_activate(n__isPal(X)) > Marked_isPal(X) ;
 }
{
  Marked_isPal(V) > Marked_activate(V) ;
 }
{
  Marked_isPal(V) > Marked_U71(isPalListKind(activate(V)),activate(V)) ;
 }
{
  Marked_and(tt,X) > Marked_activate(X) ;
 }
{
  Marked_U71(tt,V) > Marked_activate(V) ;
 }
{
  Marked_U71(tt,V) > Marked_isNePal(activate(V)) ;
 }
{
  Marked_isNePal(V) > Marked_activate(V) ;
 }
{
  Marked_isNePal(V) > Marked_U61(isPalListKind(activate(V)),activate(V)) ;
 }
{
  Marked_U61(tt,V) > Marked_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) >= tt
constraint: isNeList(n____(V1,V2)) >= U41(and(isPalListKind(activate(V1)),
                                           n__isPalListKind(activate(V2))),
                                       activate(V1),activate(V2))
constraint: isNeList(n____(V1,V2)) >= U51(and(isPalListKind(activate(V1)),
                                           n__isPalListKind(activate(V2))),
                                       activate(V1),activate(V2))
constraint: isNeList(V) >= U31(isPalListKind(activate(V)),activate(V))
constraint: activate(n__nil) >= nil
constraint: activate(n__isPalListKind(X)) >= isPalListKind(X)
constraint: activate(n____(X1,X2)) >= __(activate(X1),activate(X2))
constraint: activate(n__and(X1,X2)) >= and(activate(X1),X2)
constraint: activate(n__isPal(X)) >= isPal(X)
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(isNeList(activate(V)))
constraint: U22(tt,V2) >= U23(isList(activate(V2)))
constraint: isList(n__nil) >= tt
constraint: isList(n____(V1,V2)) >= U21(and(isPalListKind(activate(V1)),
                                         n__isPalListKind(activate(V2))),
                                     activate(V1),activate(V2))
constraint: isList(V) >= U11(isPalListKind(activate(V)),activate(V))
constraint: U21(tt,V1,V2) >= U22(isList(activate(V1)),activate(V2))
constraint: U23(tt) >= tt
constraint: U32(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: U31(tt,V) >= U32(isQid(activate(V)))
constraint: U42(tt,V2) >= U43(isNeList(activate(V2)))
constraint: U41(tt,V1,V2) >= U42(isList(activate(V1)),activate(V2))
constraint: U43(tt) >= tt
constraint: U52(tt,V2) >= U53(isList(activate(V2)))
constraint: U51(tt,V1,V2) >= U52(isNeList(activate(V1)),activate(V2))
constraint: U53(tt) >= tt
constraint: U62(tt) >= tt
constraint: U61(tt,V) >= U62(isQid(activate(V)))
constraint: U72(tt) >= tt
constraint: isNePal(n____(I,n____(P,I))) >= and(and(isQid(activate(I)),
                                                 n__isPalListKind(activate(I))),
                                             n__and(n__isPal(activate(P)),
                                              n__isPalListKind(activate(P))))
constraint: isNePal(V) >= U61(isPalListKind(activate(V)),activate(V))
constraint: U71(tt,V) >= U72(isNePal(activate(V)))
constraint: and(tt,X) >= activate(X)
constraint: and(X1,X2) >= n__and(X1,X2)
constraint: isPalListKind(n__nil) >= tt
constraint: isPalListKind(n____(V1,V2)) >= and(isPalListKind(activate(V1)),
                                            n__isPalListKind(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: isPalListKind(X) >= n__isPalListKind(X)
constraint: isPal(n__nil) >= tt
constraint: isPal(X) >= n__isPal(X)
constraint: isPal(V) >= U71(isPalListKind(activate(V)),activate(V))
constraint: a >= n__a
constraint: e >= n__e
constraint: i >= n__i
constraint: o >= n__o
constraint: u >= n__u
constraint: Marked_activate(n__and(X1,X2)) >= Marked_activate(X1)
constraint: Marked_activate(n__and(X1,X2)) >= Marked_and(activate(X1),X2)
constraint: Marked_activate(n__isPal(X)) >= Marked_isPal(X)
constraint: Marked_isPal(V) >= Marked_activate(V)
constraint: Marked_isPal(V) >= Marked_U71(isPalListKind(activate(V)),
                                activate(V))
constraint: Marked_and(tt,X) >= Marked_activate(X)
constraint: Marked_U71(tt,V) >= Marked_activate(V)
constraint: Marked_U71(tt,V) >= Marked_isNePal(activate(V))
constraint: Marked_isNePal(V) >= Marked_activate(V)
constraint: Marked_isNePal(V) >= Marked_U61(isPalListKind(activate(V)),
                                  activate(V))
constraint: Marked_U61(tt,V) >= Marked_activate(V)
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)> 
      --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
  <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
}
APPLY CRITERIA (Subterm criterion)

ST: Marked_activate -> 1
Marked_and -> 2

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(isNeList(activate(V)))
[5] U12(tt) -> tt
[6] U21(tt,V1,V2) -> U22(isList(activate(V1)),activate(V2))
[7] U22(tt,V2) -> U23(isList(activate(V2)))
[8] U23(tt) -> tt
[9] U31(tt,V) -> U32(isQid(activate(V)))
[10] U32(tt) -> tt
[11] U41(tt,V1,V2) -> U42(isList(activate(V1)),activate(V2))
[12] U42(tt,V2) -> U43(isNeList(activate(V2)))
[13] U43(tt) -> tt
[14] U51(tt,V1,V2) -> U52(isNeList(activate(V1)),activate(V2))
[15] U52(tt,V2) -> U53(isList(activate(V2)))
[16] U53(tt) -> tt
[17] U61(tt,V) -> U62(isQid(activate(V)))
[18] U62(tt) -> tt
[19] U71(tt,V) -> U72(isNePal(activate(V)))
[20] U72(tt) -> tt
[21] and(tt,X) -> activate(X)
[22] isList(V) -> U11(isPalListKind(activate(V)),activate(V))
[23] isList(n__nil) -> tt
[24] isList(n____(V1,V2)) ->
 U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),
  activate(V1),activate(V2))
[25] isNeList(V) -> U31(isPalListKind(activate(V)),activate(V))
[26] isNeList(n____(V1,V2)) ->
 U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),
  activate(V1),activate(V2))
[27] isNeList(n____(V1,V2)) ->
 U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),
  activate(V1),activate(V2))
[28] isNePal(V) -> U61(isPalListKind(activate(V)),activate(V))
[29] isNePal(n____(I,n____(P,I))) ->
 and(and(isQid(activate(I)),n__isPalListKind(activate(I))),
  n__and(n__isPal(activate(P)),n__isPalListKind(activate(P))))
[30] isPal(V) -> U71(isPalListKind(activate(V)),activate(V))
[31] isPal(n__nil) -> tt
[32] isPalListKind(n__a) -> tt
[33] isPalListKind(n__e) -> tt
[34] isPalListKind(n__i) -> tt
[35] isPalListKind(n__nil) -> tt
[36] isPalListKind(n__o) -> tt
[37] isPalListKind(n__u) -> tt
[38] isPalListKind(n____(V1,V2)) ->
 and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2)))
[39] isQid(n__a) -> tt
[40] isQid(n__e) -> tt
[41] isQid(n__i) -> tt
[42] isQid(n__o) -> tt
[43] isQid(n__u) -> tt
[44] nil -> n__nil
[45] __(X1,X2) -> n____(X1,X2)
[46] isPalListKind(X) -> n__isPalListKind(X)
[47] and(X1,X2) -> n__and(X1,X2)
[48] isPal(X) -> n__isPal(X)
[49] a -> n__a
[50] e -> n__e
[51] i -> n__i
[52] o -> n__o
[53] u -> n__u
[54] activate(n__nil) -> nil
[55] activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
[56] activate(n__isPalListKind(X)) -> isPalListKind(X)
[57] activate(n__and(X1,X2)) -> and(activate(X1),X2)
[58] activate(n__isPal(X)) -> isPal(X)
[59] activate(n__a) -> a
[60] activate(n__e) -> e
[61] activate(n__i) -> i
[62] activate(n__o) -> o
[63] activate(n__u) -> u
[64] 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(isNeList(activate(V)))>
<Marked_U11(tt,V) , Marked_isNeList(activate(V))>
<Marked_U11(tt,V) , Marked_activate(V)>
<Marked_U21(tt,V1,V2) , Marked_U22(isList(activate(V1)),activate(V2))>
<Marked_U21(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U21(tt,V1,V2) , Marked_activate(V1)>
<Marked_U21(tt,V1,V2) , Marked_activate(V2)>
<Marked_U22(tt,V2) , Marked_U23(isList(activate(V2)))>
<Marked_U22(tt,V2) , Marked_isList(activate(V2))>
<Marked_U22(tt,V2) , Marked_activate(V2)>
<Marked_U31(tt,V) , Marked_U32(isQid(activate(V)))>
<Marked_U31(tt,V) , Marked_isQid(activate(V))>
<Marked_U31(tt,V) , Marked_activate(V)>
<Marked_U41(tt,V1,V2) , Marked_U42(isList(activate(V1)),activate(V2))>
<Marked_U41(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U41(tt,V1,V2) , Marked_activate(V1)>
<Marked_U41(tt,V1,V2) , Marked_activate(V2)>
<Marked_U42(tt,V2) , Marked_U43(isNeList(activate(V2)))>
<Marked_U42(tt,V2) , Marked_isNeList(activate(V2))>
<Marked_U42(tt,V2) , Marked_activate(V2)>
<Marked_U51(tt,V1,V2) , Marked_U52(isNeList(activate(V1)),activate(V2))>
<Marked_U51(tt,V1,V2) , Marked_isNeList(activate(V1))>
<Marked_U51(tt,V1,V2) , Marked_activate(V1)>
<Marked_U51(tt,V1,V2) , Marked_activate(V2)>
<Marked_U52(tt,V2) , Marked_U53(isList(activate(V2)))>
<Marked_U52(tt,V2) , Marked_isList(activate(V2))>
<Marked_U52(tt,V2) , Marked_activate(V2)>
<Marked_U61(tt,V) , Marked_U62(isQid(activate(V)))>
<Marked_U61(tt,V) , Marked_isQid(activate(V))>
<Marked_U61(tt,V) , Marked_activate(V)>
<Marked_U71(tt,V) , Marked_U72(isNePal(activate(V)))>
<Marked_U71(tt,V) , Marked_isNePal(activate(V))>
<Marked_U71(tt,V) , Marked_activate(V)>
<Marked_and(tt,X) , Marked_activate(X)>
<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(and(isPalListKind(activate(V1)),
                                           n__isPalListKind(activate(V2))),
                                activate(V1),activate(V2))>
<Marked_isList(n____(V1,V2)) , Marked_and(isPalListKind(activate(V1)),
                                n__isPalListKind(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(V2)>
<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(and(isPalListKind(activate(V1)),
                                             n__isPalListKind(activate(V2))),
                                  activate(V1),activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_and(isPalListKind(activate(V1)),
                                  n__isPalListKind(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(V2)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNeList(n____(V1,V2)) , Marked_U51(and(isPalListKind(activate(V1)),
                                             n__isPalListKind(activate(V2))),
                                  activate(V1),activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_and(isPalListKind(activate(V1)),
                                  n__isPalListKind(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(V2)>
<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,n____(P,I))) , Marked_and(and(isQid(activate(I)),
                                                   n__isPalListKind(activate(I)))
                                                   ,
                                        n__and(n__isPal(activate(P)),
                                         n__isPalListKind(activate(P))))>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_and(isQid(activate(I)),
                                        n__isPalListKind(activate(I)))>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_isQid(activate(I))>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)>
<Marked_isPal(V) , Marked_U71(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_and(isPalListKind(activate(V1)),
                                       n__isPalListKind(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___(activate(X1),activate(X2))>
<Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
<Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
<Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
<Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
<Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
<Marked_activate(n__isPal(X)) , Marked_isPal(X)>
<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_isNeList(activate(V))>
<Marked_U21(tt,V1,V2) , Marked_U22(isList(activate(V1)),activate(V2))>
<Marked_U21(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U22(tt,V2) , Marked_isList(activate(V2))>
<Marked_U41(tt,V1,V2) , Marked_U42(isList(activate(V1)),activate(V2))>
<Marked_U41(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U42(tt,V2) , Marked_isNeList(activate(V2))>
<Marked_U51(tt,V1,V2) , Marked_U52(isNeList(activate(V1)),activate(V2))>
<Marked_U51(tt,V1,V2) , Marked_isNeList(activate(V1))>
<Marked_U52(tt,V2) , Marked_isList(activate(V2))>
<Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
<Marked_isList(n____(V1,V2)) , Marked_U21(and(isPalListKind(activate(V1)),
                                           n__isPalListKind(activate(V2))),
                                activate(V1),activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_U41(and(isPalListKind(activate(V1)),
                                             n__isPalListKind(activate(V2))),
                                  activate(V1),activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_U51(and(isPalListKind(activate(V1)),
                                             n__isPalListKind(activate(V2))),
                                  activate(V1),activate(V2))>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ __ ] (X0,X1) = 1*X1 + 2*X0 + 1; 
 [ Marked_U11 ] (X0,X1) = 2*X1; 
 [ isPal ] (X0) = 0; 
 [ U43 ] (X0) = 0; 
 [ isList ] (X0) = 0; 
 [ i ] () = 0; 
 [ U71 ] (X0,X1) = 0; 
 [ activate ] (X0) = 1*X0; 
 [ Marked_U52 ] (X0,X1) = 2*X1; 
 [ n__o ] () = 0; 
 [ U62 ] (X0) = 0; 
 [ isQid ] (X0) = 0; 
 [ n__isPalListKind ] (X0) = 0; 
 [ Marked_U41 ] (X0,X1,X2) = 2*X2 + 2*X1; 
 [ U12 ] (X0) = 0; 
 [ n__e ] () = 0; 
 [ U51 ] (X0,X1,X2) = 0; 
 [ U23 ] (X0) = 0; 
 [ u ] () = 0; 
 [ isPalListKind ] (X0) = 0; 
 [ Marked_isNeList ] (X0) = 2*X0; 
 [ tt ] () = 0; 
 [ Marked_U42 ] (X0,X1) = 2*X1; 
 [ a ] () = 0; 
 [ U72 ] (X0) = 0; 
 [ U42 ] (X0,X1) = 0; 
 [ n__and ] (X0,X1) = 2*X1; 
 [ Marked_isList ] (X0) = 2*X0; 
 [ nil ] () = 0; 
 [ n__a ] () = 0; 
 [ U52 ] (X0,X1) = 0; 
 [ U21 ] (X0,X1,X2) = 0; 
 [ Marked_U22 ] (X0,X1) = 2*X1; 
 [ o ] () = 0; 
 [ and ] (X0,X1) = 2*X1; 
 [ U11 ] (X0,X1) = 0; 
 [ n__u ] () = 0; 
 [ U61 ] (X0,X1) = 0; 
 [ U31 ] (X0,X1) = 0; 
 [ n____ ] (X0,X1) = 1*X1 + 2*X0 + 1; 
 [ isNeList ] (X0) = 2; 
 [ n__i ] () = 0; 
 [ U53 ] (X0) = 0; 
 [ U32 ] (X0) = 0; 
 [ n__nil ] () = 0; 
 [ Marked_U51 ] (X0,X1,X2) = 2*X2 + 2*X1 + 1; 
 [ U22 ] (X0,X1) = 0; 
 [ e ] () = 0; 
 [ isNePal ] (X0) = 0; 
 [ U41 ] (X0,X1,X2) = 2; 
 [ n__isPal ] (X0) = 0; 
 [ Marked_U21 ] (X0,X1,X2) = 2*X2 + 2*X1; 
 removing <Marked_U51(tt,V1,V2),Marked_U52(isNeList(activate(V1)),activate(V2))><
Marked_U51(tt,V1,V2),Marked_isNeList(activate(V1))><Marked_isList(n____(V1,V2)),
Marked_U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),
 activate(V1),activate(V2))><Marked_isNeList(n____(V1,V2)),Marked_U41(
                                                            and(isPalListKind(
                                                                 activate(
                                                                  V1)),
                                                             n__isPalListKind(
                                                              activate(
                                                               V2))),
                                                            activate(V1),
                                                            activate(V2))><
Marked_isNeList(n____(V1,V2)),Marked_U51(and(isPalListKind(activate(V1)),
                                          n__isPalListKind(activate(V2))),
                               activate(V1),activate(V2))>
 [ {
      
     DP termination of:
     <Marked_U11(tt,V) , Marked_isNeList(activate(V))>
<Marked_U21(tt,V1,V2) , Marked_U22(isList(activate(V1)),activate(V2))>
<Marked_U21(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U22(tt,V2) , Marked_isList(activate(V2))>
<Marked_U41(tt,V1,V2) , Marked_U42(isList(activate(V1)),activate(V2))>
<Marked_U41(tt,V1,V2) , Marked_isList(activate(V1))>
<Marked_U42(tt,V2) , Marked_isNeList(activate(V2))>
<Marked_U52(tt,V2) , Marked_isList(activate(V2))>
<Marked_isList(V) , Marked_U11(isPalListKind(activate(V)),activate(V))>
 ,
 CRITERION: SG
 [  ]} 
 ]} 
{
 
DP termination of:
<Marked_U61(tt,V) , Marked_activate(V)>
<Marked_U71(tt,V) , Marked_isNePal(activate(V))>
<Marked_U71(tt,V) , Marked_activate(V)>
<Marked_and(tt,X) , Marked_activate(X)>
<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,n____(P,I))) , Marked_and(and(isQid(activate(I)),
                                                   n__isPalListKind(activate(I)))
                                                   ,
                                        n__and(n__isPal(activate(P)),
                                         n__isPalListKind(activate(P))))>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_and(isQid(activate(I)),
                                        n__isPalListKind(activate(I)))>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)>
<Marked_isPal(V) , Marked_U71(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_and(isPalListKind(activate(V1)),
                                       n__isPalListKind(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____(X1,X2)) , Marked_activate(X1)>
<Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
<Marked_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
<Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
<Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
<Marked_activate(n__isPal(X)) , Marked_isPal(X)>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ __ ] (X0,X1) = 1*X1 + 3*X0 + 1; 
 [ isPal ] (X0) = 2*X0; 
 [ U43 ] (X0) = 0; 
 [ isList ] (X0) = 0; 
 [ i ] () = 0; 
 [ U71 ] (X0,X1) = 0; 
 [ Marked_isNePal ] (X0) = 1*X0; 
 [ activate ] (X0) = 1*X0; 
 [ n__o ] () = 0; 
 [ U62 ] (X0) = 0; 
 [ isQid ] (X0) = 0; 
 [ n__isPalListKind ] (X0) = 1*X0; 
 [ U12 ] (X0) = 0; 
 [ n__e ] () = 0; 
 [ U51 ] (X0,X1,X2) = 0; 
 [ Marked_and ] (X0,X1) = 1*X1; 
 [ U23 ] (X0) = 0; 
 [ u ] () = 0; 
 [ isPalListKind ] (X0) = 1*X0; 
 [ tt ] () = 0; 
 [ a ] () = 0; 
 [ U72 ] (X0) = 0; 
 [ U42 ] (X0,X1) = 0; 
 [ n__and ] (X0,X1) = 1*X1 + 1*X0; 
 [ nil ] () = 0; 
 [ n__a ] () = 0; 
 [ U52 ] (X0,X1) = 0; 
 [ Marked_isPal ] (X0) = 2*X0; 
 [ U21 ] (X0,X1,X2) = 0; 
 [ o ] () = 0; 
 [ and ] (X0,X1) = 1*X1 + 1*X0; 
 [ Marked_U61 ] (X0,X1) = 1*X1; 
 [ U11 ] (X0,X1) = 0; 
 [ n__u ] () = 0; 
 [ U61 ] (X0,X1) = 0; 
 [ U31 ] (X0,X1) = 0; 
 [ n____ ] (X0,X1) = 1*X1 + 3*X0 + 1; 
 [ isNeList ] (X0) = 3*X0 + 1; 
 [ n__i ] () = 0; 
 [ U53 ] (X0) = 0; 
 [ Marked_isPalListKind ] (X0) = 1*X0; 
 [ U32 ] (X0) = 0; 
 [ Marked_activate ] (X0) = 1*X0; 
 [ n__nil ] () = 0; 
 [ U22 ] (X0,X1) = 0; 
 [ e ] () = 0; 
 [ isNePal ] (X0) = 1*X0; 
 [ Marked_U71 ] (X0,X1) = 2*X1; 
 [ U41 ] (X0,X1,X2) = 1*X1; 
 [ n__isPal ] (X0) = 2*X0; 
 removing <Marked_isNePal(n____(I,n____(P,I))),Marked_and(and(isQid(activate(I)),
                                                           n__isPalListKind(
                                                            activate(
                                                             I))),
                                                n__and(n__isPal(activate(P)),
                                                 n__isPalListKind(activate(P))))><
Marked_isNePal(n____(I,n____(P,I))),Marked_and(isQid(activate(I)),
                                     n__isPalListKind(activate(I)))><
Marked_isNePal(n____(I,n____(P,I))),Marked_activate(I)><Marked_isNePal(
                                                         n____(I,n____(P,I))),
Marked_activate(I)><Marked_isNePal(n____(I,n____(P,I))),Marked_activate(P)><
Marked_isNePal(n____(I,n____(P,I))),Marked_activate(P)><Marked_isPalListKind(
                                                         n____(V1,V2)),
Marked_and(isPalListKind(activate(V1)),n__isPalListKind(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____(X1,X2)),Marked_activate(X1)><
Marked_activate(n____(X1,X2)),Marked_activate(X2)>
 [ {
      
     DP termination of:
     <Marked_U61(tt,V) , Marked_activate(V)>
<Marked_U71(tt,V) , Marked_isNePal(activate(V))>
<Marked_U71(tt,V) , Marked_activate(V)>
<Marked_and(tt,X) , Marked_activate(X)>
<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_isPal(V) , Marked_U71(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_activate(n__isPalListKind(X)) , Marked_isPalListKind(X)>
<Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
<Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
<Marked_activate(n__isPal(X)) , Marked_isPal(X)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_U61(tt,V) , Marked_activate(V)>
<Marked_U71(tt,V) , Marked_isNePal(activate(V))>
<Marked_U71(tt,V) , Marked_activate(V)>
<Marked_and(tt,X) , Marked_activate(X)>
<Marked_isNePal(V) , Marked_U61(isPalListKind(activate(V)),activate(V))>
<Marked_isNePal(V) , Marked_activate(V)>
<Marked_isNePal(V) , Marked_activate(V)>
<Marked_isPal(V) , Marked_U71(isPalListKind(activate(V)),activate(V))>
<Marked_isPal(V) , Marked_activate(V)>
<Marked_isPal(V) , Marked_activate(V)>
<Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
<Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
<Marked_activate(n__isPal(X)) , Marked_isPal(X)>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ __ ] (X0,X1) = 1*X1 + 2*X0; 
 [ isPal ] (X0) = 2*X0 + 2; 
 [ U43 ] (X0) = 0; 
 [ isList ] (X0) = 2*X0; 
 [ i ] () = 0; 
 [ U71 ] (X0,X1) = 0; 
 [ Marked_isNePal ] (X0) = 2*X0 + 2; 
 [ activate ] (X0) = 1*X0; 
 [ n__o ] () = 0; 
 [ U62 ] (X0) = 0; 
 [ isQid ] (X0) = 3*X0; 
 [ n__isPalListKind ] (X0) = 0; 
 [ U12 ] (X0) = 0; 
 [ n__e ] () = 0; 
 [ U51 ] (X0,X1,X2) = 0; 
 [ Marked_and ] (X0,X1) = 2*X1 + 1; 
 [ U23 ] (X0) = 0; 
 [ u ] () = 0; 
 [ isPalListKind ] (X0) = 0; 
 [ tt ] () = 0; 
 [ a ] () = 0; 
 [ U72 ] (X0) = 0; 
 [ U42 ] (X0,X1) = 0; 
 [ n__and ] (X0,X1) = 1*X1 + 1*X0; 
 [ nil ] () = 0; 
 [ n__a ] () = 0; 
 [ U52 ] (X0,X1) = 0; 
 [ Marked_isPal ] (X0) = 2*X0 + 2; 
 [ U21 ] (X0,X1,X2) = 2*X1; 
 [ o ] () = 0; 
 [ and ] (X0,X1) = 1*X1 + 1*X0; 
 [ Marked_U61 ] (X0,X1) = 2*X1 + 2; 
 [ U11 ] (X0,X1) = 0; 
 [ n__u ] () = 0; 
 [ U61 ] (X0,X1) = 0; 
 [ U31 ] (X0,X1) = 0; 
 [ n____ ] (X0,X1) = 1*X1 + 2*X0; 
 [ isNeList ] (X0) = 0; 
 [ n__i ] () = 0; 
 [ U53 ] (X0) = 0; 
 [ U32 ] (X0) = 0; 
 [ Marked_activate ] (X0) = 2*X0 + 1; 
 [ n__nil ] () = 0; 
 [ U22 ] (X0,X1) = 0; 
 [ e ] () = 0; 
 [ isNePal ] (X0) = 1*X0 + 2; 
 [ Marked_U71 ] (X0,X1) = 2*X1 + 2; 
 [ U41 ] (X0,X1,X2) = 0; 
 [ n__isPal ] (X0) = 2*X0 + 2; 
 removing <Marked_U61(tt,V),Marked_activate(V)><Marked_U71(tt,V),Marked_activate(
                                                                  V)><
Marked_isNePal(V),Marked_activate(V)><Marked_isNePal(V),Marked_activate(V)><
Marked_isPal(V),Marked_activate(V)><Marked_isPal(V),Marked_activate(V)><
Marked_activate(n__isPal(X)),Marked_isPal(X)>
 [ {
      
     DP termination of:
     <Marked_U71(tt,V) , Marked_isNePal(activate(V))>
<Marked_and(tt,X) , Marked_activate(X)>
<Marked_isNePal(V) , Marked_U61(isPalListKind(activate(V)),activate(V))>
<Marked_isPal(V) , Marked_U71(isPalListKind(activate(V)),activate(V))>
<Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
<Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_and(tt,X) , Marked_activate(X)>
<Marked_activate(n__and(X1,X2)) , Marked_and(activate(X1),X2)>
<Marked_activate(n__and(X1,X2)) , Marked_activate(X1)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
     <Marked_and(tt,X) , Marked_activate(X)>
 ,
 CRITERION: SG
 [  ]} 
 ]} 
 ]} 
 ]} 
 ]} 
 ]} 
{
 
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.317296 seconds (real time)
Cime Exit Status: 0