- : 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 (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 (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___(X1,X2) ;
  Marked___(active(X1),X2) >= Marked___(X1,X2) ;
  Marked___(X1,mark(X2)) >= Marked___(X1,X2) ;
  Marked___(X1,active(X2)) >= Marked___(X1,X2) ;
 }
 + Disjunctions:{ 
{
  Marked___(mark(X1),X2) > Marked___(X1,X2) ;
 }
{
  Marked___(active(X1),X2) > Marked___(X1,X2) ;
 }
{
  Marked___(X1,mark(X2)) > Marked___(X1,X2) ;
 }
{
  Marked___(X1,active(X2)) > Marked___(X1,X2) ;
 }
 } 
=== 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
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
Entering rpo_solver
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 15.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 15.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
=== TIMER virtual : 50.000000 ===
trying sub matrices of size: 1
Matrix interpretation constraints generated.
Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. 
Termination constraints generated.
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 50.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
No solution found for these constraints.
APPLY CRITERIA (ID_CRIT)
NOT SOLVED
No proof found
Cime worked for 10.359585 seconds (real time)
Cime Exit Status: 0