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

TRS termination of:
[1] active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
[2] active(__(X,nil)) -> mark(X)
[3] active(__(nil,X)) -> mark(X)
[4] active(and(tt,X)) -> mark(X)
[5] active(isList(V)) -> mark(isNeList(V))
[6] active(isList(nil)) -> mark(tt)
[7] active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
[8] active(isNeList(V)) -> mark(isQid(V))
[9] active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
[10] active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
[11] active(isNePal(V)) -> mark(isQid(V))
[12] active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
[13] active(isPal(V)) -> mark(isNePal(V))
[14] active(isPal(nil)) -> mark(tt)
[15] active(isQid(a)) -> mark(tt)
[16] active(isQid(e)) -> mark(tt)
[17] active(isQid(i)) -> mark(tt)
[18] active(isQid(o)) -> mark(tt)
[19] active(isQid(u)) -> mark(tt)
[20] mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
[21] mark(nil) -> active(nil)
[22] mark(and(X1,X2)) -> active(and(mark(X1),X2))
[23] mark(tt) -> active(tt)
[24] mark(isList(X)) -> active(isList(X))
[25] mark(isNeList(X)) -> active(isNeList(X))
[26] mark(isQid(X)) -> active(isQid(X))
[27] mark(isNePal(X)) -> active(isNePal(X))
[28] mark(isPal(X)) -> active(isPal(X))
[29] mark(a) -> active(a)
[30] mark(e) -> active(e)
[31] mark(i) -> active(i)
[32] mark(o) -> active(o)
[33] mark(u) -> active(u)
[34] __(mark(X1),X2) -> __(X1,X2)
[35] __(X1,mark(X2)) -> __(X1,X2)
[36] __(active(X1),X2) -> __(X1,X2)
[37] __(X1,active(X2)) -> __(X1,X2)
[38] and(mark(X1),X2) -> and(X1,X2)
[39] and(X1,mark(X2)) -> and(X1,X2)
[40] and(active(X1),X2) -> and(X1,X2)
[41] and(X1,active(X2)) -> and(X1,X2)
[42] isList(mark(X)) -> isList(X)
[43] isList(active(X)) -> isList(X)
[44] isNeList(mark(X)) -> isNeList(X)
[45] isNeList(active(X)) -> isNeList(X)
[46] isQid(mark(X)) -> isQid(X)
[47] isQid(active(X)) -> isQid(X)
[48] isNePal(mark(X)) -> isNePal(X)
[49] isNePal(active(X)) -> isNePal(X)
[50] isPal(mark(X)) -> isPal(X)
[51] isPal(active(X)) -> isPal(X)


Sub problem: 
guided: 

DP termination of:
<Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
<Marked_active(__(__(X,Y),Z)) , Marked___(X,__(Y,Z))>
<Marked_active(__(__(X,Y),Z)) , Marked___(Y,Z)>
<Marked_active(__(X,nil)) , Marked_mark(X)>
<Marked_active(__(nil,X)) , Marked_mark(X)>
<Marked_active(and(tt,X)) , Marked_mark(X)>
<Marked_active(isList(V)) , Marked_mark(isNeList(V))>
<Marked_active(isList(V)) , Marked_isNeList(V)>
<Marked_active(isList(nil)) , Marked_mark(tt)>
<Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))>
<Marked_active(isList(__(V1,V2))) , Marked_and(isList(V1),isList(V2))>
<Marked_active(isList(__(V1,V2))) , Marked_isList(V1)>
<Marked_active(isList(__(V1,V2))) , Marked_isList(V2)>
<Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
<Marked_active(isNeList(V)) , Marked_isQid(V)>
<Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),isNeList(V2)))>
<Marked_active(isNeList(__(V1,V2))) , Marked_and(isList(V1),isNeList(V2))>
<Marked_active(isNeList(__(V1,V2))) , Marked_isList(V1)>
<Marked_active(isNeList(__(V1,V2))) , Marked_isNeList(V2)>
<Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),isList(V2)))>
<Marked_active(isNeList(__(V1,V2))) , Marked_and(isNeList(V1),isList(V2))>
<Marked_active(isNeList(__(V1,V2))) , Marked_isNeList(V1)>
<Marked_active(isNeList(__(V1,V2))) , Marked_isList(V2)>
<Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
<Marked_active(isNePal(V)) , Marked_isQid(V)>
<Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))>
<Marked_active(isNePal(__(I,__(P,I)))) , Marked_and(isQid(I),isPal(P))>
<Marked_active(isNePal(__(I,__(P,I)))) , Marked_isQid(I)>
<Marked_active(isNePal(__(I,__(P,I)))) , Marked_isPal(P)>
<Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
<Marked_active(isPal(V)) , Marked_isNePal(V)>
<Marked_active(isPal(nil)) , Marked_mark(tt)>
<Marked_active(isQid(a)) , Marked_mark(tt)>
<Marked_active(isQid(e)) , Marked_mark(tt)>
<Marked_active(isQid(i)) , Marked_mark(tt)>
<Marked_active(isQid(o)) , Marked_mark(tt)>
<Marked_active(isQid(u)) , Marked_mark(tt)>
<Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
<Marked_mark(__(X1,X2)) , Marked___(mark(X1),mark(X2))>
<Marked_mark(__(X1,X2)) , Marked_mark(X1)>
<Marked_mark(__(X1,X2)) , Marked_mark(X2)>
<Marked_mark(nil) , Marked_active(nil)>
<Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
<Marked_mark(and(X1,X2)) , Marked_and(mark(X1),X2)>
<Marked_mark(and(X1,X2)) , Marked_mark(X1)>
<Marked_mark(tt) , Marked_active(tt)>
<Marked_mark(isList(X)) , Marked_active(isList(X))>
<Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
<Marked_mark(isQid(X)) , Marked_active(isQid(X))>
<Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
<Marked_mark(isPal(X)) , Marked_active(isPal(X))>
<Marked_mark(a) , Marked_active(a)>
<Marked_mark(e) , Marked_active(e)>
<Marked_mark(i) , Marked_active(i)>
<Marked_mark(o) , Marked_active(o)>
<Marked_mark(u) , Marked_active(u)>
<Marked___(mark(X1),X2) , Marked___(X1,X2)>
<Marked___(X1,mark(X2)) , Marked___(X1,X2)>
<Marked___(active(X1),X2) , Marked___(X1,X2)>
<Marked___(X1,active(X2)) , Marked___(X1,X2)>
<Marked_and(mark(X1),X2) , Marked_and(X1,X2)>
<Marked_and(X1,mark(X2)) , Marked_and(X1,X2)>
<Marked_and(active(X1),X2) , Marked_and(X1,X2)>
<Marked_and(X1,active(X2)) , Marked_and(X1,X2)>
<Marked_isList(mark(X)) , Marked_isList(X)>
<Marked_isList(active(X)) , Marked_isList(X)>
<Marked_isNeList(mark(X)) , Marked_isNeList(X)>
<Marked_isNeList(active(X)) , Marked_isNeList(X)>
<Marked_isQid(mark(X)) , Marked_isQid(X)>
<Marked_isQid(active(X)) , Marked_isQid(X)>
<Marked_isNePal(mark(X)) , Marked_isNePal(X)>
<Marked_isNePal(active(X)) , Marked_isNePal(X)>
<Marked_isPal(mark(X)) , Marked_isPal(X)>
<Marked_isPal(active(X)) , Marked_isPal(X)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 8 components:

{  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
      --> <Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),
                                                               isPal(P)))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                            isList(V2)))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                            isNeList(V2)))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                          isList(V2)))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isList(V)) , Marked_mark(isNeList(V))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(and(tt,X)) , Marked_mark(X)>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(__(nil,X)) , Marked_mark(X)>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(__(X,nil)) , Marked_mark(X)>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),
                                                               isPal(P)))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                            isList(V2)))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                            isNeList(V2)))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                          isList(V2)))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isList(V)) , Marked_mark(isNeList(V))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(and(tt,X)) , Marked_mark(X)>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(__(nil,X)) , Marked_mark(X)>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(__(X,nil)) , Marked_mark(X)>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
  <Marked_mark(isQid(X)) , Marked_active(isQid(X))> 
     --> <Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
  <Marked_mark(isQid(X)) , Marked_active(isQid(X))> 
     --> <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),
                                                               isPal(P)))>
  <Marked_mark(isQid(X)) , Marked_active(isQid(X))> 
     --> <Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isQid(X)) , Marked_active(isQid(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                            isList(V2)))>
  <Marked_mark(isQid(X)) , Marked_active(isQid(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                            isNeList(V2)))>
  <Marked_mark(isQid(X)) , Marked_active(isQid(X))> 
     --> <Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isQid(X)) , Marked_active(isQid(X))> 
     --> <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                          isList(V2)))>
  <Marked_mark(isQid(X)) , Marked_active(isQid(X))> 
     --> <Marked_active(isList(V)) , Marked_mark(isNeList(V))>
  <Marked_mark(isQid(X)) , Marked_active(isQid(X))> 
     --> <Marked_active(and(tt,X)) , Marked_mark(X)>
  <Marked_mark(isQid(X)) , Marked_active(isQid(X))> 
     --> <Marked_active(__(nil,X)) , Marked_mark(X)>
  <Marked_mark(isQid(X)) , Marked_active(isQid(X))> 
     --> <Marked_active(__(X,nil)) , Marked_mark(X)>
  <Marked_mark(isQid(X)) , Marked_active(isQid(X))> 
     --> <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),
                                                               isPal(P)))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                            isList(V2)))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                            isNeList(V2)))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                          isList(V2)))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isList(V)) , Marked_mark(isNeList(V))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(and(tt,X)) , Marked_mark(X)>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(__(nil,X)) , Marked_mark(X)>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(__(X,nil)) , Marked_mark(X)>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),
                                                               isPal(P)))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                            isList(V2)))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                            isNeList(V2)))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                          isList(V2)))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isList(V)) , Marked_mark(isNeList(V))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(and(tt,X)) , Marked_mark(X)>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(__(nil,X)) , Marked_mark(X)>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(__(X,nil)) , Marked_mark(X)>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),
                                                               isPal(P)))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                            isList(V2)))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                            isNeList(V2)))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                          isList(V2)))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isList(V)) , Marked_mark(isNeList(V))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(and(tt,X)) , Marked_mark(X)>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(__(nil,X)) , Marked_mark(X)>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(__(X,nil)) , Marked_mark(X)>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),
                                                               isPal(P)))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                            isList(V2)))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                            isNeList(V2)))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                          isList(V2)))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isList(V)) , Marked_mark(isNeList(V))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(and(tt,X)) , Marked_mark(X)>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(__(nil,X)) , Marked_mark(X)>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(__(X,nil)) , Marked_mark(X)>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(isQid(X)) , Marked_active(isQid(X))>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
}

{  <Marked___(X1,active(X2)) , Marked___(X1,X2)> 
      --> <Marked___(X1,active(X2)) , Marked___(X1,X2)>
  <Marked___(X1,active(X2)) , Marked___(X1,X2)> 
     --> <Marked___(active(X1),X2) , Marked___(X1,X2)>
  <Marked___(X1,active(X2)) , Marked___(X1,X2)> 
     --> <Marked___(X1,mark(X2)) , Marked___(X1,X2)>
  <Marked___(X1,active(X2)) , Marked___(X1,X2)> 
     --> <Marked___(mark(X1),X2) , Marked___(X1,X2)>
  <Marked___(active(X1),X2) , Marked___(X1,X2)> 
     --> <Marked___(X1,active(X2)) , Marked___(X1,X2)>
  <Marked___(active(X1),X2) , Marked___(X1,X2)> 
     --> <Marked___(active(X1),X2) , Marked___(X1,X2)>
  <Marked___(active(X1),X2) , Marked___(X1,X2)> 
     --> <Marked___(X1,mark(X2)) , Marked___(X1,X2)>
  <Marked___(active(X1),X2) , Marked___(X1,X2)> 
     --> <Marked___(mark(X1),X2) , Marked___(X1,X2)>
  <Marked___(X1,mark(X2)) , Marked___(X1,X2)> 
     --> <Marked___(X1,active(X2)) , Marked___(X1,X2)>
  <Marked___(X1,mark(X2)) , Marked___(X1,X2)> 
     --> <Marked___(active(X1),X2) , Marked___(X1,X2)>
  <Marked___(X1,mark(X2)) , Marked___(X1,X2)> 
     --> <Marked___(X1,mark(X2)) , Marked___(X1,X2)>
  <Marked___(X1,mark(X2)) , Marked___(X1,X2)> 
     --> <Marked___(mark(X1),X2) , Marked___(X1,X2)>
  <Marked___(mark(X1),X2) , Marked___(X1,X2)> 
     --> <Marked___(X1,active(X2)) , Marked___(X1,X2)>
  <Marked___(mark(X1),X2) , Marked___(X1,X2)> 
     --> <Marked___(active(X1),X2) , Marked___(X1,X2)>
  <Marked___(mark(X1),X2) , Marked___(X1,X2)> 
     --> <Marked___(X1,mark(X2)) , Marked___(X1,X2)>
  <Marked___(mark(X1),X2) , Marked___(X1,X2)> 
     --> <Marked___(mark(X1),X2) , Marked___(X1,X2)>
}

{  <Marked_and(X1,active(X2)) , Marked_and(X1,X2)> 
      --> <Marked_and(X1,active(X2)) , Marked_and(X1,X2)>
  <Marked_and(X1,active(X2)) , Marked_and(X1,X2)> 
     --> <Marked_and(active(X1),X2) , Marked_and(X1,X2)>
  <Marked_and(X1,active(X2)) , Marked_and(X1,X2)> 
     --> <Marked_and(X1,mark(X2)) , Marked_and(X1,X2)>
  <Marked_and(X1,active(X2)) , Marked_and(X1,X2)> 
     --> <Marked_and(mark(X1),X2) , Marked_and(X1,X2)>
  <Marked_and(active(X1),X2) , Marked_and(X1,X2)> 
     --> <Marked_and(X1,active(X2)) , Marked_and(X1,X2)>
  <Marked_and(active(X1),X2) , Marked_and(X1,X2)> 
     --> <Marked_and(active(X1),X2) , Marked_and(X1,X2)>
  <Marked_and(active(X1),X2) , Marked_and(X1,X2)> 
     --> <Marked_and(X1,mark(X2)) , Marked_and(X1,X2)>
  <Marked_and(active(X1),X2) , Marked_and(X1,X2)> 
     --> <Marked_and(mark(X1),X2) , Marked_and(X1,X2)>
  <Marked_and(X1,mark(X2)) , Marked_and(X1,X2)> 
     --> <Marked_and(X1,active(X2)) , Marked_and(X1,X2)>
  <Marked_and(X1,mark(X2)) , Marked_and(X1,X2)> 
     --> <Marked_and(active(X1),X2) , Marked_and(X1,X2)>
  <Marked_and(X1,mark(X2)) , Marked_and(X1,X2)> 
     --> <Marked_and(X1,mark(X2)) , Marked_and(X1,X2)>
  <Marked_and(X1,mark(X2)) , Marked_and(X1,X2)> 
     --> <Marked_and(mark(X1),X2) , Marked_and(X1,X2)>
  <Marked_and(mark(X1),X2) , Marked_and(X1,X2)> 
     --> <Marked_and(X1,active(X2)) , Marked_and(X1,X2)>
  <Marked_and(mark(X1),X2) , Marked_and(X1,X2)> 
     --> <Marked_and(active(X1),X2) , Marked_and(X1,X2)>
  <Marked_and(mark(X1),X2) , Marked_and(X1,X2)> 
     --> <Marked_and(X1,mark(X2)) , Marked_and(X1,X2)>
  <Marked_and(mark(X1),X2) , Marked_and(X1,X2)> 
     --> <Marked_and(mark(X1),X2) , Marked_and(X1,X2)>
}

{  <Marked_isList(active(X)) , Marked_isList(X)> 
      --> <Marked_isList(active(X)) , Marked_isList(X)>
  <Marked_isList(active(X)) , Marked_isList(X)> 
     --> <Marked_isList(mark(X)) , Marked_isList(X)>
  <Marked_isList(mark(X)) , Marked_isList(X)> 
     --> <Marked_isList(active(X)) , Marked_isList(X)>
  <Marked_isList(mark(X)) , Marked_isList(X)> 
     --> <Marked_isList(mark(X)) , Marked_isList(X)>
}

{  <Marked_isNeList(active(X)) , Marked_isNeList(X)> 
      --> <Marked_isNeList(active(X)) , Marked_isNeList(X)>
  <Marked_isNeList(active(X)) , Marked_isNeList(X)> 
     --> <Marked_isNeList(mark(X)) , Marked_isNeList(X)>
  <Marked_isNeList(mark(X)) , Marked_isNeList(X)> 
     --> <Marked_isNeList(active(X)) , Marked_isNeList(X)>
  <Marked_isNeList(mark(X)) , Marked_isNeList(X)> 
     --> <Marked_isNeList(mark(X)) , Marked_isNeList(X)>
}

{  <Marked_isQid(active(X)) , Marked_isQid(X)> 
      --> <Marked_isQid(active(X)) , Marked_isQid(X)>
  <Marked_isQid(active(X)) , Marked_isQid(X)> 
     --> <Marked_isQid(mark(X)) , Marked_isQid(X)>
  <Marked_isQid(mark(X)) , Marked_isQid(X)> 
     --> <Marked_isQid(active(X)) , Marked_isQid(X)>
  <Marked_isQid(mark(X)) , Marked_isQid(X)> 
     --> <Marked_isQid(mark(X)) , Marked_isQid(X)>
}

{  <Marked_isNePal(active(X)) , Marked_isNePal(X)> 
      --> <Marked_isNePal(active(X)) , Marked_isNePal(X)>
  <Marked_isNePal(active(X)) , Marked_isNePal(X)> 
     --> <Marked_isNePal(mark(X)) , Marked_isNePal(X)>
  <Marked_isNePal(mark(X)) , Marked_isNePal(X)> 
     --> <Marked_isNePal(active(X)) , Marked_isNePal(X)>
  <Marked_isNePal(mark(X)) , Marked_isNePal(X)> 
     --> <Marked_isNePal(mark(X)) , Marked_isNePal(X)>
}

{  <Marked_isPal(active(X)) , Marked_isPal(X)> 
      --> <Marked_isPal(active(X)) , Marked_isPal(X)>
  <Marked_isPal(active(X)) , Marked_isPal(X)> 
     --> <Marked_isPal(mark(X)) , Marked_isPal(X)>
  <Marked_isPal(mark(X)) , Marked_isPal(X)> 
     --> <Marked_isPal(active(X)) , Marked_isPal(X)>
  <Marked_isPal(mark(X)) , Marked_isPal(X)> 
     --> <Marked_isPal(mark(X)) , Marked_isPal(X)>
}
APPLY CRITERIA (Subterm criterion)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  mark(__(X1,X2)) >= active(__(mark(X1),mark(X2))) ;
  mark(nil) >= active(nil) ;
  mark(and(X1,X2)) >= active(and(mark(X1),X2)) ;
  mark(tt) >= active(tt) ;
  mark(isNeList(X)) >= active(isNeList(X)) ;
  mark(isList(X)) >= active(isList(X)) ;
  mark(isQid(X)) >= active(isQid(X)) ;
  mark(isNePal(X)) >= active(isNePal(X)) ;
  mark(isPal(X)) >= active(isPal(X)) ;
  mark(a) >= active(a) ;
  mark(e) >= active(e) ;
  mark(i) >= active(i) ;
  mark(o) >= active(o) ;
  mark(u) >= active(u) ;
  __(mark(X1),X2) >= __(X1,X2) ;
  __(active(X1),X2) >= __(X1,X2) ;
  __(X1,mark(X2)) >= __(X1,X2) ;
  __(X1,active(X2)) >= __(X1,X2) ;
  active(__(__(X,Y),Z)) >= mark(__(X,__(Y,Z))) ;
  active(__(nil,X)) >= mark(X) ;
  active(__(X,nil)) >= mark(X) ;
  active(and(tt,X)) >= mark(X) ;
  active(isNeList(__(V1,V2))) >= mark(and(isNeList(V1),isList(V2))) ;
  active(isNeList(__(V1,V2))) >= mark(and(isList(V1),isNeList(V2))) ;
  active(isNeList(V)) >= mark(isQid(V)) ;
  active(isList(__(V1,V2))) >= mark(and(isList(V1),isList(V2))) ;
  active(isList(nil)) >= mark(tt) ;
  active(isList(V)) >= mark(isNeList(V)) ;
  active(isQid(a)) >= mark(tt) ;
  active(isQid(e)) >= mark(tt) ;
  active(isQid(i)) >= mark(tt) ;
  active(isQid(o)) >= mark(tt) ;
  active(isQid(u)) >= mark(tt) ;
  active(isNePal(__(I,__(P,I)))) >= mark(and(isQid(I),isPal(P))) ;
  active(isNePal(V)) >= mark(isQid(V)) ;
  active(isPal(nil)) >= mark(tt) ;
  active(isPal(V)) >= mark(isNePal(V)) ;
  and(mark(X1),X2) >= and(X1,X2) ;
  and(active(X1),X2) >= and(X1,X2) ;
  and(X1,mark(X2)) >= and(X1,X2) ;
  and(X1,active(X2)) >= and(X1,X2) ;
  isNeList(mark(X)) >= isNeList(X) ;
  isNeList(active(X)) >= isNeList(X) ;
  isList(mark(X)) >= isList(X) ;
  isList(active(X)) >= isList(X) ;
  isQid(mark(X)) >= isQid(X) ;
  isQid(active(X)) >= isQid(X) ;
  isNePal(mark(X)) >= isNePal(X) ;
  isNePal(active(X)) >= isNePal(X) ;
  isPal(mark(X)) >= isPal(X) ;
  isPal(active(X)) >= isPal(X) ;
  Marked_mark(__(X1,X2)) >= Marked_mark(X1) ;
  Marked_mark(__(X1,X2)) >= Marked_mark(X2) ;
  Marked_mark(__(X1,X2)) >= Marked_active(__(mark(X1),mark(X2))) ;
  Marked_mark(and(X1,X2)) >= Marked_mark(X1) ;
  Marked_mark(and(X1,X2)) >= Marked_active(and(mark(X1),X2)) ;
  Marked_mark(isNeList(X)) >= Marked_active(isNeList(X)) ;
  Marked_mark(isList(X)) >= Marked_active(isList(X)) ;
  Marked_mark(isQid(X)) >= Marked_active(isQid(X)) ;
  Marked_mark(isNePal(X)) >= Marked_active(isNePal(X)) ;
  Marked_mark(isPal(X)) >= Marked_active(isPal(X)) ;
  Marked_active(__(__(X,Y),Z)) >= Marked_mark(__(X,__(Y,Z))) ;
  Marked_active(__(nil,X)) >= Marked_mark(X) ;
  Marked_active(__(X,nil)) >= Marked_mark(X) ;
  Marked_active(and(tt,X)) >= Marked_mark(X) ;
  Marked_active(isNeList(__(V1,V2))) >= Marked_mark(and(isNeList(V1),
                                                     isList(V2))) ;
  Marked_active(isNeList(__(V1,V2))) >= Marked_mark(and(isList(V1),
                                                     isNeList(V2))) ;
  Marked_active(isNeList(V)) >= Marked_mark(isQid(V)) ;
  Marked_active(isList(__(V1,V2))) >= Marked_mark(and(isList(V1),isList(V2))) ;
  Marked_active(isList(V)) >= Marked_mark(isNeList(V)) ;
  Marked_active(isNePal(__(I,__(P,I)))) >= Marked_mark(and(isQid(I),isPal(P))) ;
  Marked_active(isNePal(V)) >= Marked_mark(isQid(V)) ;
  Marked_active(isPal(V)) >= Marked_mark(isNePal(V)) ;
 }
 + Disjunctions:{ 
{
  Marked_mark(__(X1,X2)) > Marked_mark(X1) ;
 }
{
  Marked_mark(__(X1,X2)) > Marked_mark(X2) ;
 }
{
  Marked_mark(__(X1,X2)) > Marked_active(__(mark(X1),mark(X2))) ;
 }
{
  Marked_mark(and(X1,X2)) > Marked_mark(X1) ;
 }
{
  Marked_mark(and(X1,X2)) > Marked_active(and(mark(X1),X2)) ;
 }
{
  Marked_mark(isNeList(X)) > Marked_active(isNeList(X)) ;
 }
{
  Marked_mark(isList(X)) > Marked_active(isList(X)) ;
 }
{
  Marked_mark(isQid(X)) > Marked_active(isQid(X)) ;
 }
{
  Marked_mark(isNePal(X)) > Marked_active(isNePal(X)) ;
 }
{
  Marked_mark(isPal(X)) > Marked_active(isPal(X)) ;
 }
{
  Marked_active(__(__(X,Y),Z)) > Marked_mark(__(X,__(Y,Z))) ;
 }
{
  Marked_active(__(nil,X)) > Marked_mark(X) ;
 }
{
  Marked_active(__(X,nil)) > Marked_mark(X) ;
 }
{
  Marked_active(and(tt,X)) > Marked_mark(X) ;
 }
{
  Marked_active(isNeList(__(V1,V2))) > Marked_mark(and(isNeList(V1),isList(V2))) ;
 }
{
  Marked_active(isNeList(__(V1,V2))) > Marked_mark(and(isList(V1),isNeList(V2))) ;
 }
{
  Marked_active(isNeList(V)) > Marked_mark(isQid(V)) ;
 }
{
  Marked_active(isList(__(V1,V2))) > Marked_mark(and(isList(V1),isList(V2))) ;
 }
{
  Marked_active(isList(V)) > Marked_mark(isNeList(V)) ;
 }
{
  Marked_active(isNePal(__(I,__(P,I)))) > Marked_mark(and(isQid(I),isPal(P))) ;
 }
{
  Marked_active(isNePal(V)) > Marked_mark(isQid(V)) ;
 }
{
  Marked_active(isPal(V)) > Marked_mark(isNePal(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: mark(__(X1,X2)) >= active(__(mark(X1),mark(X2)))
constraint: mark(nil) >= active(nil)
constraint: mark(and(X1,X2)) >= active(and(mark(X1),X2))
constraint: mark(tt) >= active(tt)
constraint: mark(isNeList(X)) >= active(isNeList(X))
constraint: mark(isList(X)) >= active(isList(X))
constraint: mark(isQid(X)) >= active(isQid(X))
constraint: mark(isNePal(X)) >= active(isNePal(X))
constraint: mark(isPal(X)) >= active(isPal(X))
constraint: mark(a) >= active(a)
constraint: mark(e) >= active(e)
constraint: mark(i) >= active(i)
constraint: mark(o) >= active(o)
constraint: mark(u) >= active(u)
constraint: __(mark(X1),X2) >= __(X1,X2)
constraint: __(active(X1),X2) >= __(X1,X2)
constraint: __(X1,mark(X2)) >= __(X1,X2)
constraint: __(X1,active(X2)) >= __(X1,X2)
constraint: active(__(__(X,Y),Z)) >= mark(__(X,__(Y,Z)))
constraint: active(__(nil,X)) >= mark(X)
constraint: active(__(X,nil)) >= mark(X)
constraint: active(and(tt,X)) >= mark(X)
constraint: active(isNeList(__(V1,V2))) >= mark(and(isNeList(V1),isList(V2)))
constraint: active(isNeList(__(V1,V2))) >= mark(and(isList(V1),isNeList(V2)))
constraint: active(isNeList(V)) >= mark(isQid(V))
constraint: active(isList(__(V1,V2))) >= mark(and(isList(V1),isList(V2)))
constraint: active(isList(nil)) >= mark(tt)
constraint: active(isList(V)) >= mark(isNeList(V))
constraint: active(isQid(a)) >= mark(tt)
constraint: active(isQid(e)) >= mark(tt)
constraint: active(isQid(i)) >= mark(tt)
constraint: active(isQid(o)) >= mark(tt)
constraint: active(isQid(u)) >= mark(tt)
constraint: active(isNePal(__(I,__(P,I)))) >= mark(and(isQid(I),isPal(P)))
constraint: active(isNePal(V)) >= mark(isQid(V))
constraint: active(isPal(nil)) >= mark(tt)
constraint: active(isPal(V)) >= mark(isNePal(V))
constraint: and(mark(X1),X2) >= and(X1,X2)
constraint: and(active(X1),X2) >= and(X1,X2)
constraint: and(X1,mark(X2)) >= and(X1,X2)
constraint: and(X1,active(X2)) >= and(X1,X2)
constraint: isNeList(mark(X)) >= isNeList(X)
constraint: isNeList(active(X)) >= isNeList(X)
constraint: isList(mark(X)) >= isList(X)
constraint: isList(active(X)) >= isList(X)
constraint: isQid(mark(X)) >= isQid(X)
constraint: isQid(active(X)) >= isQid(X)
constraint: isNePal(mark(X)) >= isNePal(X)
constraint: isNePal(active(X)) >= isNePal(X)
constraint: isPal(mark(X)) >= isPal(X)
constraint: isPal(active(X)) >= isPal(X)
constraint: Marked_mark(__(X1,X2)) >= Marked_mark(X1)
constraint: Marked_mark(__(X1,X2)) >= Marked_mark(X2)
constraint: Marked_mark(__(X1,X2)) >= Marked_active(__(mark(X1),mark(X2)))
constraint: Marked_mark(and(X1,X2)) >= Marked_mark(X1)
constraint: Marked_mark(and(X1,X2)) >= Marked_active(and(mark(X1),X2))
constraint: Marked_mark(isNeList(X)) >= Marked_active(isNeList(X))
constraint: Marked_mark(isList(X)) >= Marked_active(isList(X))
constraint: Marked_mark(isQid(X)) >= Marked_active(isQid(X))
constraint: Marked_mark(isNePal(X)) >= Marked_active(isNePal(X))
constraint: Marked_mark(isPal(X)) >= Marked_active(isPal(X))
constraint: Marked_active(__(__(X,Y),Z)) >= Marked_mark(__(X,__(Y,Z)))
constraint: Marked_active(__(nil,X)) >= Marked_mark(X)
constraint: Marked_active(__(X,nil)) >= Marked_mark(X)
constraint: Marked_active(and(tt,X)) >= Marked_mark(X)
constraint: Marked_active(isNeList(__(V1,V2))) >= Marked_mark(and(isNeList(V1),
                                                               isList(V2)))
constraint: Marked_active(isNeList(__(V1,V2))) >= Marked_mark(and(isList(V1),
                                                               isNeList(V2)))
constraint: Marked_active(isNeList(V)) >= Marked_mark(isQid(V))
constraint: Marked_active(isList(__(V1,V2))) >= Marked_mark(and(isList(V1),
                                                             isList(V2)))
constraint: Marked_active(isList(V)) >= Marked_mark(isNeList(V))
constraint: Marked_active(isNePal(__(I,__(P,I)))) >= Marked_mark(and(
                                                                  isQid(I),
                                                                  isPal(P)))
constraint: Marked_active(isNePal(V)) >= Marked_mark(isQid(V))
constraint: Marked_active(isPal(V)) >= Marked_mark(isNePal(V))
APPLY CRITERIA (Subterm criterion)

ST: Marked___ -> 2

APPLY CRITERIA (Subterm criterion)

ST: Marked_and -> 2

APPLY CRITERIA (Subterm criterion)

ST: Marked_isList -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_isNeList -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_isQid -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_isNePal -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_isPal -> 1

APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
      --> <Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),
                                                               isPal(P)))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                            isList(V2)))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                            isNeList(V2)))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                          isList(V2)))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(isList(V)) , Marked_mark(isNeList(V))>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(and(tt,X)) , Marked_mark(X)>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(__(nil,X)) , Marked_mark(X)>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(__(X,nil)) , Marked_mark(X)>
  <Marked_mark(isPal(X)) , Marked_active(isPal(X))> 
     --> <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),
                                                               isPal(P)))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                            isList(V2)))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                            isNeList(V2)))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                          isList(V2)))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(isList(V)) , Marked_mark(isNeList(V))>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(and(tt,X)) , Marked_mark(X)>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(__(nil,X)) , Marked_mark(X)>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(__(X,nil)) , Marked_mark(X)>
  <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))> 
     --> <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),
                                                               isPal(P)))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                            isList(V2)))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                            isNeList(V2)))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                          isList(V2)))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(isList(V)) , Marked_mark(isNeList(V))>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(and(tt,X)) , Marked_mark(X)>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(__(nil,X)) , Marked_mark(X)>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(__(X,nil)) , Marked_mark(X)>
  <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))> 
     --> <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),
                                                               isPal(P)))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                            isList(V2)))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                            isNeList(V2)))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                          isList(V2)))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(isList(V)) , Marked_mark(isNeList(V))>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(and(tt,X)) , Marked_mark(X)>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(__(nil,X)) , Marked_mark(X)>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(__(X,nil)) , Marked_mark(X)>
  <Marked_mark(isList(X)) , Marked_active(isList(X))> 
     --> <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),
                                                               isPal(P)))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                            isList(V2)))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                            isNeList(V2)))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                          isList(V2)))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(isList(V)) , Marked_mark(isNeList(V))>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(and(tt,X)) , Marked_mark(X)>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(__(nil,X)) , Marked_mark(X)>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(__(X,nil)) , Marked_mark(X)>
  <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))> 
     --> <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(__(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(__(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),
                                                               isPal(P)))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                            isList(V2)))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                            isNeList(V2)))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                          isList(V2)))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(isList(V)) , Marked_mark(isNeList(V))>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(and(tt,X)) , Marked_mark(X)>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(__(nil,X)) , Marked_mark(X)>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(__(X,nil)) , Marked_mark(X)>
  <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))> 
     --> <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isPal(V)) , Marked_mark(isNePal(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNePal(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),
                                                     isList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),
                                                     isNeList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isNeList(V)) , Marked_mark(isQid(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(isList(V)) , Marked_mark(isNeList(V))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(and(tt,X)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(__(nil,X)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(__(X,nil)) , Marked_mark(X)> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(isPal(X)) , Marked_active(isPal(X))>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(isList(X)) , Marked_active(isList(X))>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X2)>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_mark(X1)>
  <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))> 
     --> <Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
}
APPLY CRITERIA (Subterm criterion)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  mark(__(X1,X2)) >= active(__(mark(X1),mark(X2))) ;
  mark(nil) >= active(nil) ;
  mark(and(X1,X2)) >= active(and(mark(X1),X2)) ;
  mark(tt) >= active(tt) ;
  mark(isNeList(X)) >= active(isNeList(X)) ;
  mark(isList(X)) >= active(isList(X)) ;
  mark(isQid(X)) >= active(isQid(X)) ;
  mark(isNePal(X)) >= active(isNePal(X)) ;
  mark(isPal(X)) >= active(isPal(X)) ;
  mark(a) >= active(a) ;
  mark(e) >= active(e) ;
  mark(i) >= active(i) ;
  mark(o) >= active(o) ;
  mark(u) >= active(u) ;
  __(mark(X1),X2) >= __(X1,X2) ;
  __(active(X1),X2) >= __(X1,X2) ;
  __(X1,mark(X2)) >= __(X1,X2) ;
  __(X1,active(X2)) >= __(X1,X2) ;
  active(__(__(X,Y),Z)) >= mark(__(X,__(Y,Z))) ;
  active(__(nil,X)) >= mark(X) ;
  active(__(X,nil)) >= mark(X) ;
  active(and(tt,X)) >= mark(X) ;
  active(isNeList(__(V1,V2))) >= mark(and(isNeList(V1),isList(V2))) ;
  active(isNeList(__(V1,V2))) >= mark(and(isList(V1),isNeList(V2))) ;
  active(isNeList(V)) >= mark(isQid(V)) ;
  active(isList(__(V1,V2))) >= mark(and(isList(V1),isList(V2))) ;
  active(isList(nil)) >= mark(tt) ;
  active(isList(V)) >= mark(isNeList(V)) ;
  active(isQid(a)) >= mark(tt) ;
  active(isQid(e)) >= mark(tt) ;
  active(isQid(i)) >= mark(tt) ;
  active(isQid(o)) >= mark(tt) ;
  active(isQid(u)) >= mark(tt) ;
  active(isNePal(__(I,__(P,I)))) >= mark(and(isQid(I),isPal(P))) ;
  active(isNePal(V)) >= mark(isQid(V)) ;
  active(isPal(nil)) >= mark(tt) ;
  active(isPal(V)) >= mark(isNePal(V)) ;
  and(mark(X1),X2) >= and(X1,X2) ;
  and(active(X1),X2) >= and(X1,X2) ;
  and(X1,mark(X2)) >= and(X1,X2) ;
  and(X1,active(X2)) >= and(X1,X2) ;
  isNeList(mark(X)) >= isNeList(X) ;
  isNeList(active(X)) >= isNeList(X) ;
  isList(mark(X)) >= isList(X) ;
  isList(active(X)) >= isList(X) ;
  isQid(mark(X)) >= isQid(X) ;
  isQid(active(X)) >= isQid(X) ;
  isNePal(mark(X)) >= isNePal(X) ;
  isNePal(active(X)) >= isNePal(X) ;
  isPal(mark(X)) >= isPal(X) ;
  isPal(active(X)) >= isPal(X) ;
  Marked_mark(__(X1,X2)) >= Marked_mark(X1) ;
  Marked_mark(__(X1,X2)) >= Marked_mark(X2) ;
  Marked_mark(__(X1,X2)) >= Marked_active(__(mark(X1),mark(X2))) ;
  Marked_mark(and(X1,X2)) >= Marked_mark(X1) ;
  Marked_mark(and(X1,X2)) >= Marked_active(and(mark(X1),X2)) ;
  Marked_mark(isNeList(X)) >= Marked_active(isNeList(X)) ;
  Marked_mark(isList(X)) >= Marked_active(isList(X)) ;
  Marked_mark(isNePal(X)) >= Marked_active(isNePal(X)) ;
  Marked_mark(isPal(X)) >= Marked_active(isPal(X)) ;
  Marked_active(__(__(X,Y),Z)) >= Marked_mark(__(X,__(Y,Z))) ;
  Marked_active(__(nil,X)) >= Marked_mark(X) ;
  Marked_active(__(X,nil)) >= Marked_mark(X) ;
  Marked_active(and(tt,X)) >= Marked_mark(X) ;
  Marked_active(isNeList(__(V1,V2))) >= Marked_mark(and(isNeList(V1),
                                                     isList(V2))) ;
  Marked_active(isNeList(__(V1,V2))) >= Marked_mark(and(isList(V1),
                                                     isNeList(V2))) ;
  Marked_active(isNeList(V)) >= Marked_mark(isQid(V)) ;
  Marked_active(isList(__(V1,V2))) >= Marked_mark(and(isList(V1),isList(V2))) ;
  Marked_active(isList(V)) >= Marked_mark(isNeList(V)) ;
  Marked_active(isNePal(__(I,__(P,I)))) >= Marked_mark(and(isQid(I),isPal(P))) ;
  Marked_active(isNePal(V)) >= Marked_mark(isQid(V)) ;
  Marked_active(isPal(V)) >= Marked_mark(isNePal(V)) ;
 }
 + Disjunctions:{ 
{
  Marked_mark(__(X1,X2)) > Marked_mark(X1) ;
 }
{
  Marked_mark(__(X1,X2)) > Marked_mark(X2) ;
 }
{
  Marked_mark(__(X1,X2)) > Marked_active(__(mark(X1),mark(X2))) ;
 }
{
  Marked_mark(and(X1,X2)) > Marked_mark(X1) ;
 }
{
  Marked_mark(and(X1,X2)) > Marked_active(and(mark(X1),X2)) ;
 }
{
  Marked_mark(isNeList(X)) > Marked_active(isNeList(X)) ;
 }
{
  Marked_mark(isList(X)) > Marked_active(isList(X)) ;
 }
{
  Marked_mark(isNePal(X)) > Marked_active(isNePal(X)) ;
 }
{
  Marked_mark(isPal(X)) > Marked_active(isPal(X)) ;
 }
{
  Marked_active(__(__(X,Y),Z)) > Marked_mark(__(X,__(Y,Z))) ;
 }
{
  Marked_active(__(nil,X)) > Marked_mark(X) ;
 }
{
  Marked_active(__(X,nil)) > Marked_mark(X) ;
 }
{
  Marked_active(and(tt,X)) > Marked_mark(X) ;
 }
{
  Marked_active(isNeList(__(V1,V2))) > Marked_mark(and(isNeList(V1),isList(V2))) ;
 }
{
  Marked_active(isNeList(__(V1,V2))) > Marked_mark(and(isList(V1),isNeList(V2))) ;
 }
{
  Marked_active(isNeList(V)) > Marked_mark(isQid(V)) ;
 }
{
  Marked_active(isList(__(V1,V2))) > Marked_mark(and(isList(V1),isList(V2))) ;
 }
{
  Marked_active(isList(V)) > Marked_mark(isNeList(V)) ;
 }
{
  Marked_active(isNePal(__(I,__(P,I)))) > Marked_mark(and(isQid(I),isPal(P))) ;
 }
{
  Marked_active(isNePal(V)) > Marked_mark(isQid(V)) ;
 }
{
  Marked_active(isPal(V)) > Marked_mark(isNePal(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: mark(__(X1,X2)) >= active(__(mark(X1),mark(X2)))
constraint: mark(nil) >= active(nil)
constraint: mark(and(X1,X2)) >= active(and(mark(X1),X2))
constraint: mark(tt) >= active(tt)
constraint: mark(isNeList(X)) >= active(isNeList(X))
constraint: mark(isList(X)) >= active(isList(X))
constraint: mark(isQid(X)) >= active(isQid(X))
constraint: mark(isNePal(X)) >= active(isNePal(X))
constraint: mark(isPal(X)) >= active(isPal(X))
constraint: mark(a) >= active(a)
constraint: mark(e) >= active(e)
constraint: mark(i) >= active(i)
constraint: mark(o) >= active(o)
constraint: mark(u) >= active(u)
constraint: __(mark(X1),X2) >= __(X1,X2)
constraint: __(active(X1),X2) >= __(X1,X2)
constraint: __(X1,mark(X2)) >= __(X1,X2)
constraint: __(X1,active(X2)) >= __(X1,X2)
constraint: active(__(__(X,Y),Z)) >= mark(__(X,__(Y,Z)))
constraint: active(__(nil,X)) >= mark(X)
constraint: active(__(X,nil)) >= mark(X)
constraint: active(and(tt,X)) >= mark(X)
constraint: active(isNeList(__(V1,V2))) >= mark(and(isNeList(V1),isList(V2)))
constraint: active(isNeList(__(V1,V2))) >= mark(and(isList(V1),isNeList(V2)))
constraint: active(isNeList(V)) >= mark(isQid(V))
constraint: active(isList(__(V1,V2))) >= mark(and(isList(V1),isList(V2)))
constraint: active(isList(nil)) >= mark(tt)
constraint: active(isList(V)) >= mark(isNeList(V))
constraint: active(isQid(a)) >= mark(tt)
constraint: active(isQid(e)) >= mark(tt)
constraint: active(isQid(i)) >= mark(tt)
constraint: active(isQid(o)) >= mark(tt)
constraint: active(isQid(u)) >= mark(tt)
constraint: active(isNePal(__(I,__(P,I)))) >= mark(and(isQid(I),isPal(P)))
constraint: active(isNePal(V)) >= mark(isQid(V))
constraint: active(isPal(nil)) >= mark(tt)
constraint: active(isPal(V)) >= mark(isNePal(V))
constraint: and(mark(X1),X2) >= and(X1,X2)
constraint: and(active(X1),X2) >= and(X1,X2)
constraint: and(X1,mark(X2)) >= and(X1,X2)
constraint: and(X1,active(X2)) >= and(X1,X2)
constraint: isNeList(mark(X)) >= isNeList(X)
constraint: isNeList(active(X)) >= isNeList(X)
constraint: isList(mark(X)) >= isList(X)
constraint: isList(active(X)) >= isList(X)
constraint: isQid(mark(X)) >= isQid(X)
constraint: isQid(active(X)) >= isQid(X)
constraint: isNePal(mark(X)) >= isNePal(X)
constraint: isNePal(active(X)) >= isNePal(X)
constraint: isPal(mark(X)) >= isPal(X)
constraint: isPal(active(X)) >= isPal(X)
constraint: Marked_mark(__(X1,X2)) >= Marked_mark(X1)
constraint: Marked_mark(__(X1,X2)) >= Marked_mark(X2)
constraint: Marked_mark(__(X1,X2)) >= Marked_active(__(mark(X1),mark(X2)))
constraint: Marked_mark(and(X1,X2)) >= Marked_mark(X1)
constraint: Marked_mark(and(X1,X2)) >= Marked_active(and(mark(X1),X2))
constraint: Marked_mark(isNeList(X)) >= Marked_active(isNeList(X))
constraint: Marked_mark(isList(X)) >= Marked_active(isList(X))
constraint: Marked_mark(isNePal(X)) >= Marked_active(isNePal(X))
constraint: Marked_mark(isPal(X)) >= Marked_active(isPal(X))
constraint: Marked_active(__(__(X,Y),Z)) >= Marked_mark(__(X,__(Y,Z)))
constraint: Marked_active(__(nil,X)) >= Marked_mark(X)
constraint: Marked_active(__(X,nil)) >= Marked_mark(X)
constraint: Marked_active(and(tt,X)) >= Marked_mark(X)
constraint: Marked_active(isNeList(__(V1,V2))) >= Marked_mark(and(isNeList(V1),
                                                               isList(V2)))
constraint: Marked_active(isNeList(__(V1,V2))) >= Marked_mark(and(isList(V1),
                                                               isNeList(V2)))
constraint: Marked_active(isNeList(V)) >= Marked_mark(isQid(V))
constraint: Marked_active(isList(__(V1,V2))) >= Marked_mark(and(isList(V1),
                                                             isList(V2)))
constraint: Marked_active(isList(V)) >= Marked_mark(isNeList(V))
constraint: Marked_active(isNePal(__(I,__(P,I)))) >= Marked_mark(and(
                                                                  isQid(I),
                                                                  isPal(P)))
constraint: Marked_active(isNePal(V)) >= Marked_mark(isQid(V))
constraint: Marked_active(isPal(V)) >= Marked_mark(isNePal(V))
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_mark(and(X1,X2)) , Marked_mark(X1)> 
      --> <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
}
APPLY CRITERIA (Subterm criterion)

ST: Marked_mark -> 1

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

{  <Marked___(mark(X1),X2) , Marked___(X1,X2)> 
      --> <Marked___(mark(X1),X2) , Marked___(X1,X2)>
  <Marked___(mark(X1),X2) , Marked___(X1,X2)> 
     --> <Marked___(active(X1),X2) , Marked___(X1,X2)>
  <Marked___(active(X1),X2) , Marked___(X1,X2)> 
     --> <Marked___(mark(X1),X2) , Marked___(X1,X2)>
  <Marked___(active(X1),X2) , Marked___(X1,X2)> 
     --> <Marked___(active(X1),X2) , Marked___(X1,X2)>
}
APPLY CRITERIA (Subterm criterion)

ST: Marked___ -> 1

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

{  <Marked_and(mark(X1),X2) , Marked_and(X1,X2)> 
      --> <Marked_and(mark(X1),X2) , Marked_and(X1,X2)>
  <Marked_and(mark(X1),X2) , Marked_and(X1,X2)> 
     --> <Marked_and(active(X1),X2) , Marked_and(X1,X2)>
  <Marked_and(active(X1),X2) , Marked_and(X1,X2)> 
     --> <Marked_and(mark(X1),X2) , Marked_and(X1,X2)>
  <Marked_and(active(X1),X2) , Marked_and(X1,X2)> 
     --> <Marked_and(active(X1),X2) , Marked_and(X1,X2)>
}
APPLY CRITERIA (Subterm criterion)

ST: Marked_and -> 1

APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
SOLVED
{
 
TRS termination of:
[1] active(__(__(X,Y),Z)) -> mark(__(X,__(Y,Z)))
[2] active(__(X,nil)) -> mark(X)
[3] active(__(nil,X)) -> mark(X)
[4] active(and(tt,X)) -> mark(X)
[5] active(isList(V)) -> mark(isNeList(V))
[6] active(isList(nil)) -> mark(tt)
[7] active(isList(__(V1,V2))) -> mark(and(isList(V1),isList(V2)))
[8] active(isNeList(V)) -> mark(isQid(V))
[9] active(isNeList(__(V1,V2))) -> mark(and(isList(V1),isNeList(V2)))
[10] active(isNeList(__(V1,V2))) -> mark(and(isNeList(V1),isList(V2)))
[11] active(isNePal(V)) -> mark(isQid(V))
[12] active(isNePal(__(I,__(P,I)))) -> mark(and(isQid(I),isPal(P)))
[13] active(isPal(V)) -> mark(isNePal(V))
[14] active(isPal(nil)) -> mark(tt)
[15] active(isQid(a)) -> mark(tt)
[16] active(isQid(e)) -> mark(tt)
[17] active(isQid(i)) -> mark(tt)
[18] active(isQid(o)) -> mark(tt)
[19] active(isQid(u)) -> mark(tt)
[20] mark(__(X1,X2)) -> active(__(mark(X1),mark(X2)))
[21] mark(nil) -> active(nil)
[22] mark(and(X1,X2)) -> active(and(mark(X1),X2))
[23] mark(tt) -> active(tt)
[24] mark(isList(X)) -> active(isList(X))
[25] mark(isNeList(X)) -> active(isNeList(X))
[26] mark(isQid(X)) -> active(isQid(X))
[27] mark(isNePal(X)) -> active(isNePal(X))
[28] mark(isPal(X)) -> active(isPal(X))
[29] mark(a) -> active(a)
[30] mark(e) -> active(e)
[31] mark(i) -> active(i)
[32] mark(o) -> active(o)
[33] mark(u) -> active(u)
[34] __(mark(X1),X2) -> __(X1,X2)
[35] __(X1,mark(X2)) -> __(X1,X2)
[36] __(active(X1),X2) -> __(X1,X2)
[37] __(X1,active(X2)) -> __(X1,X2)
[38] and(mark(X1),X2) -> and(X1,X2)
[39] and(X1,mark(X2)) -> and(X1,X2)
[40] and(active(X1),X2) -> and(X1,X2)
[41] and(X1,active(X2)) -> and(X1,X2)
[42] isList(mark(X)) -> isList(X)
[43] isList(active(X)) -> isList(X)
[44] isNeList(mark(X)) -> isNeList(X)
[45] isNeList(active(X)) -> isNeList(X)
[46] isQid(mark(X)) -> isQid(X)
[47] isQid(active(X)) -> isQid(X)
[48] isNePal(mark(X)) -> isNePal(X)
[49] isNePal(active(X)) -> isNePal(X)
[50] isPal(mark(X)) -> isPal(X)
[51] isPal(active(X)) -> isPal(X)
 ,
 CRITERION: MDP
 [ {
      
     DP termination of:
     <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
<Marked_active(__(__(X,Y),Z)) , Marked___(X,__(Y,Z))>
<Marked_active(__(__(X,Y),Z)) , Marked___(Y,Z)>
<Marked_active(__(X,nil)) , Marked_mark(X)>
<Marked_active(__(nil,X)) , Marked_mark(X)>
<Marked_active(and(tt,X)) , Marked_mark(X)>
<Marked_active(isList(V)) , Marked_mark(isNeList(V))>
<Marked_active(isList(V)) , Marked_isNeList(V)>
<Marked_active(isList(nil)) , Marked_mark(tt)>
<Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))>
<Marked_active(isList(__(V1,V2))) , Marked_and(isList(V1),isList(V2))>
<Marked_active(isList(__(V1,V2))) , Marked_isList(V1)>
<Marked_active(isList(__(V1,V2))) , Marked_isList(V2)>
<Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
<Marked_active(isNeList(V)) , Marked_isQid(V)>
<Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),isNeList(V2)))>
<Marked_active(isNeList(__(V1,V2))) , Marked_and(isList(V1),isNeList(V2))>
<Marked_active(isNeList(__(V1,V2))) , Marked_isList(V1)>
<Marked_active(isNeList(__(V1,V2))) , Marked_isNeList(V2)>
<Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),isList(V2)))>
<Marked_active(isNeList(__(V1,V2))) , Marked_and(isNeList(V1),isList(V2))>
<Marked_active(isNeList(__(V1,V2))) , Marked_isNeList(V1)>
<Marked_active(isNeList(__(V1,V2))) , Marked_isList(V2)>
<Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
<Marked_active(isNePal(V)) , Marked_isQid(V)>
<Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))>
<Marked_active(isNePal(__(I,__(P,I)))) , Marked_and(isQid(I),isPal(P))>
<Marked_active(isNePal(__(I,__(P,I)))) , Marked_isQid(I)>
<Marked_active(isNePal(__(I,__(P,I)))) , Marked_isPal(P)>
<Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
<Marked_active(isPal(V)) , Marked_isNePal(V)>
<Marked_active(isPal(nil)) , Marked_mark(tt)>
<Marked_active(isQid(a)) , Marked_mark(tt)>
<Marked_active(isQid(e)) , Marked_mark(tt)>
<Marked_active(isQid(i)) , Marked_mark(tt)>
<Marked_active(isQid(o)) , Marked_mark(tt)>
<Marked_active(isQid(u)) , Marked_mark(tt)>
<Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
<Marked_mark(__(X1,X2)) , Marked___(mark(X1),mark(X2))>
<Marked_mark(__(X1,X2)) , Marked_mark(X1)>
<Marked_mark(__(X1,X2)) , Marked_mark(X2)>
<Marked_mark(nil) , Marked_active(nil)>
<Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
<Marked_mark(and(X1,X2)) , Marked_and(mark(X1),X2)>
<Marked_mark(and(X1,X2)) , Marked_mark(X1)>
<Marked_mark(tt) , Marked_active(tt)>
<Marked_mark(isList(X)) , Marked_active(isList(X))>
<Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
<Marked_mark(isQid(X)) , Marked_active(isQid(X))>
<Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
<Marked_mark(isPal(X)) , Marked_active(isPal(X))>
<Marked_mark(a) , Marked_active(a)>
<Marked_mark(e) , Marked_active(e)>
<Marked_mark(i) , Marked_active(i)>
<Marked_mark(o) , Marked_active(o)>
<Marked_mark(u) , Marked_active(u)>
<Marked___(mark(X1),X2) , Marked___(X1,X2)>
<Marked___(X1,mark(X2)) , Marked___(X1,X2)>
<Marked___(active(X1),X2) , Marked___(X1,X2)>
<Marked___(X1,active(X2)) , Marked___(X1,X2)>
<Marked_and(mark(X1),X2) , Marked_and(X1,X2)>
<Marked_and(X1,mark(X2)) , Marked_and(X1,X2)>
<Marked_and(active(X1),X2) , Marked_and(X1,X2)>
<Marked_and(X1,active(X2)) , Marked_and(X1,X2)>
<Marked_isList(mark(X)) , Marked_isList(X)>
<Marked_isList(active(X)) , Marked_isList(X)>
<Marked_isNeList(mark(X)) , Marked_isNeList(X)>
<Marked_isNeList(active(X)) , Marked_isNeList(X)>
<Marked_isQid(mark(X)) , Marked_isQid(X)>
<Marked_isQid(active(X)) , Marked_isQid(X)>
<Marked_isNePal(mark(X)) , Marked_isNePal(X)>
<Marked_isNePal(active(X)) , Marked_isNePal(X)>
<Marked_isPal(mark(X)) , Marked_isPal(X)>
<Marked_isPal(active(X)) , Marked_isPal(X)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
<Marked_active(__(X,nil)) , Marked_mark(X)>
<Marked_active(__(nil,X)) , Marked_mark(X)>
<Marked_active(and(tt,X)) , Marked_mark(X)>
<Marked_active(isList(V)) , Marked_mark(isNeList(V))>
<Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))>
<Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
<Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),isNeList(V2)))>
<Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),isList(V2)))>
<Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
<Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))>
<Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
<Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
<Marked_mark(__(X1,X2)) , Marked_mark(X1)>
<Marked_mark(__(X1,X2)) , Marked_mark(X2)>
<Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
<Marked_mark(and(X1,X2)) , Marked_mark(X1)>
<Marked_mark(isList(X)) , Marked_active(isList(X))>
<Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
<Marked_mark(isQid(X)) , Marked_active(isQid(X))>
<Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
<Marked_mark(isPal(X)) , Marked_active(isPal(X))>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ mark ] (X0) = 0; 
 [ isQid ] (X0) = 0; 
 [ Marked_active ] (X0) = 2*X0; 
 [ and ] (X0,X1) = 1; 
 [ e ] () = 0; 
 [ active ] (X0) = 0; 
 [ isPal ] (X0) = 1; 
 [ isNeList ] (X0) = 1; 
 [ o ] () = 0; 
 [ __ ] (X0,X1) = 1; 
 [ isNePal ] (X0) = 1; 
 [ tt ] () = 0; 
 [ i ] () = 0; 
 [ nil ] () = 0; 
 [ a ] () = 0; 
 [ isList ] (X0) = 1; 
 [ Marked_mark ] (X0) = 2; 
 [ u ] () = 0; 
 removing <Marked_mark(isQid(X)),Marked_active(isQid(X))>
 [ {
      
     DP termination of:
     <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
<Marked_active(__(X,nil)) , Marked_mark(X)>
<Marked_active(__(nil,X)) , Marked_mark(X)>
<Marked_active(and(tt,X)) , Marked_mark(X)>
<Marked_active(isList(V)) , Marked_mark(isNeList(V))>
<Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))>
<Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
<Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),isNeList(V2)))>
<Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),isList(V2)))>
<Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
<Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))>
<Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
<Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
<Marked_mark(__(X1,X2)) , Marked_mark(X1)>
<Marked_mark(__(X1,X2)) , Marked_mark(X2)>
<Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
<Marked_mark(and(X1,X2)) , Marked_mark(X1)>
<Marked_mark(isList(X)) , Marked_active(isList(X))>
<Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
<Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
<Marked_mark(isPal(X)) , Marked_active(isPal(X))>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_active(__(__(X,Y),Z)) , Marked_mark(__(X,__(Y,Z)))>
<Marked_active(__(X,nil)) , Marked_mark(X)>
<Marked_active(__(nil,X)) , Marked_mark(X)>
<Marked_active(and(tt,X)) , Marked_mark(X)>
<Marked_active(isList(V)) , Marked_mark(isNeList(V))>
<Marked_active(isList(__(V1,V2))) , Marked_mark(and(isList(V1),isList(V2)))>
<Marked_active(isNeList(V)) , Marked_mark(isQid(V))>
<Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isList(V1),isNeList(V2)))>
<Marked_active(isNeList(__(V1,V2))) , Marked_mark(and(isNeList(V1),isList(V2)))>
<Marked_active(isNePal(V)) , Marked_mark(isQid(V))>
<Marked_active(isNePal(__(I,__(P,I)))) , Marked_mark(and(isQid(I),isPal(P)))>
<Marked_active(isPal(V)) , Marked_mark(isNePal(V))>
<Marked_mark(__(X1,X2)) , Marked_active(__(mark(X1),mark(X2)))>
<Marked_mark(__(X1,X2)) , Marked_mark(X1)>
<Marked_mark(__(X1,X2)) , Marked_mark(X2)>
<Marked_mark(and(X1,X2)) , Marked_active(and(mark(X1),X2))>
<Marked_mark(and(X1,X2)) , Marked_mark(X1)>
<Marked_mark(isList(X)) , Marked_active(isList(X))>
<Marked_mark(isNeList(X)) , Marked_active(isNeList(X))>
<Marked_mark(isNePal(X)) , Marked_active(isNePal(X))>
<Marked_mark(isPal(X)) , Marked_active(isPal(X))>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ mark ] (X0) = 1*X0; 
 [ isQid ] (X0) = 1*X0; 
 [ Marked_active ] (X0) = 2*X0; 
 [ and ] (X0,X1) = 1*X1 + 1*X0; 
 [ e ] () = 1; 
 [ active ] (X0) = 1*X0; 
 [ isPal ] (X0) = 2*X0 + 2; 
 [ isNeList ] (X0) = 2*X0 + 2; 
 [ o ] () = 1; 
 [ __ ] (X0,X1) = 1*X1 + 2*X0 + 2; 
 [ isNePal ] (X0) = 1*X0 + 1; 
 [ tt ] () = 1; 
 [ i ] () = 1; 
 [ nil ] () = 0; 
 [ a ] () = 1; 
 [ isList ] (X0) = 2*X0 + 3; 
 [ Marked_mark ] (X0) = 2*X0 + 1; 
 [ u ] () = 2; 
 removing <Marked_active(__(__(X,Y),Z)),Marked_mark(__(X,__(Y,Z)))><Marked_active(
                                                                    __(
                                                                    X,
                                                                    nil)),
Marked_mark(X)><Marked_active(__(nil,X)),Marked_mark(X)><Marked_active(
                                                          and(tt,X)),
Marked_mark(X)><Marked_active(isList(V)),Marked_mark(isNeList(V))><Marked_active(
                                                                    isList(
                                                                    __(
                                                                    V1,
                                                                    V2))),
Marked_mark(and(isList(V1),isList(V2)))><Marked_active(isNeList(V)),Marked_mark(
                                                                    isQid(
                                                                    V))><
Marked_active(isNeList(__(V1,V2))),Marked_mark(and(isList(V1),isNeList(V2)))><
Marked_active(isNeList(__(V1,V2))),Marked_mark(and(isNeList(V1),isList(V2)))><
Marked_active(isNePal(V)),Marked_mark(isQid(V))><Marked_active(isNePal(
                                                                __(I,
                                                                 __(P,I)))),
Marked_mark(and(isQid(I),isPal(P)))><Marked_active(isPal(V)),Marked_mark(
                                                              isNePal(
                                                               V))><Marked_mark(
                                                                    __(
                                                                    X1,
                                                                    X2)),
Marked_active(__(mark(X1),mark(X2)))><Marked_mark(__(X1,X2)),Marked_mark(X1)><
Marked_mark(__(X1,X2)),Marked_mark(X2)><Marked_mark(and(X1,X2)),Marked_active(
                                                                 and(
                                                                  mark(X1),
                                                                  X2))><
Marked_mark(isList(X)),Marked_active(isList(X))><Marked_mark(isNeList(X)),
Marked_active(isNeList(X))><Marked_mark(isNePal(X)),Marked_active(isNePal(X))><
Marked_mark(isPal(X)),Marked_active(isPal(X))>
 [ {
      
     DP termination of:
     <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_mark(and(X1,X2)) , Marked_mark(X1)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
 ]} 
 ]} 
 ]} 
 ]} 
{
 
DP termination of:
<Marked___(mark(X1),X2) , Marked___(X1,X2)>
<Marked___(X1,mark(X2)) , Marked___(X1,X2)>
<Marked___(active(X1),X2) , Marked___(X1,X2)>
<Marked___(X1,active(X2)) , Marked___(X1,X2)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
     <Marked___(active(X1),X2) , Marked___(X1,X2)>
<Marked___(mark(X1),X2) , Marked___(X1,X2)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked___(active(X1),X2) , Marked___(X1,X2)>
<Marked___(mark(X1),X2) , Marked___(X1,X2)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
 ]} 
 ]} 
{
 
DP termination of:
<Marked_and(mark(X1),X2) , Marked_and(X1,X2)>
<Marked_and(X1,mark(X2)) , Marked_and(X1,X2)>
<Marked_and(active(X1),X2) , Marked_and(X1,X2)>
<Marked_and(X1,active(X2)) , Marked_and(X1,X2)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
     <Marked_and(active(X1),X2) , Marked_and(X1,X2)>
<Marked_and(mark(X1),X2) , Marked_and(X1,X2)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_and(active(X1),X2) , Marked_and(X1,X2)>
<Marked_and(mark(X1),X2) , Marked_and(X1,X2)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
 ]} 
 ]} 
{
 
DP termination of:
<Marked_isList(mark(X)) , Marked_isList(X)>
<Marked_isList(active(X)) , Marked_isList(X)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
{
 
DP termination of:
<Marked_isNeList(mark(X)) , Marked_isNeList(X)>
<Marked_isNeList(active(X)) , Marked_isNeList(X)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
{
 
DP termination of:
<Marked_isQid(mark(X)) , Marked_isQid(X)>
<Marked_isQid(active(X)) , Marked_isQid(X)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
{
 
DP termination of:
<Marked_isNePal(mark(X)) , Marked_isNePal(X)>
<Marked_isNePal(active(X)) , Marked_isNePal(X)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
{
 
DP termination of:
<Marked_isPal(mark(X)) , Marked_isPal(X)>
<Marked_isPal(active(X)) , Marked_isPal(X)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
 ]} 
 ]} 

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