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

TRS termination of:
[1] __(__(X,Y),Z) -> __(X,__(Y,Z))
[2] __(X,nil) -> X
[3] __(nil,X) -> X
[4] and(tt,X) -> activate(X)
[5] isList(V) -> isNeList(activate(V))
[6] isList(n__nil) -> tt
[7] isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
[8] isNeList(V) -> isQid(activate(V))
[9] isNeList(n____(V1,V2)) ->
 and(isList(activate(V1)),n__isNeList(activate(V2)))
[10] isNeList(n____(V1,V2)) ->
 and(isNeList(activate(V1)),n__isList(activate(V2)))
[11] isNePal(V) -> isQid(activate(V))
[12] isNePal(n____(I,n____(P,I))) ->
 and(isQid(activate(I)),n__isPal(activate(P)))
[13] isPal(V) -> isNePal(activate(V))
[14] isPal(n__nil) -> tt
[15] isQid(n__a) -> tt
[16] isQid(n__e) -> tt
[17] isQid(n__i) -> tt
[18] isQid(n__o) -> tt
[19] isQid(n__u) -> tt
[20] nil -> n__nil
[21] __(X1,X2) -> n____(X1,X2)
[22] isList(X) -> n__isList(X)
[23] isNeList(X) -> n__isNeList(X)
[24] isPal(X) -> n__isPal(X)
[25] a -> n__a
[26] e -> n__e
[27] i -> n__i
[28] o -> n__o
[29] u -> n__u
[30] activate(n__nil) -> nil
[31] activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
[32] activate(n__isList(X)) -> isList(X)
[33] activate(n__isNeList(X)) -> isNeList(X)
[34] activate(n__isPal(X)) -> isPal(X)
[35] activate(n__a) -> a
[36] activate(n__e) -> e
[37] activate(n__i) -> i
[38] activate(n__o) -> o
[39] activate(n__u) -> u
[40] activate(X) -> X


Sub problem: 
guided: 

DP termination of:
<Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))>
<Marked___(__(X,Y),Z) , Marked___(Y,Z)>
<Marked_and(tt,X) , Marked_activate(X)>
<Marked_isList(V) , Marked_isNeList(activate(V))>
<Marked_isList(V) , Marked_activate(V)>
<Marked_isList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                n__isList(activate(V2)))>
<Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))>
<Marked_isList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNeList(V) , Marked_isQid(activate(V))>
<Marked_isNeList(V) , Marked_activate(V)>
<Marked_isNeList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                  n__isNeList(activate(V2)))>
<Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNeList(n____(V1,V2)) , Marked_and(isNeList(activate(V1)),
                                  n__isList(activate(V2)))>
<Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNePal(V) , Marked_isQid(activate(V))>
<Marked_isNePal(V) , Marked_activate(V)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_and(isQid(activate(I)),
                                        n__isPal(activate(P)))>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_isQid(activate(I))>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)>
<Marked_isPal(V) , Marked_isNePal(activate(V))>
<Marked_isPal(V) , Marked_activate(V)>
<Marked_activate(n__nil) , Marked_nil>
<Marked_activate(n____(X1,X2)) , Marked___(activate(X1),activate(X2))>
<Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
<Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
<Marked_activate(n__isList(X)) , Marked_isList(X)>
<Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
<Marked_activate(n__isPal(X)) , Marked_isPal(X)>
<Marked_activate(n__a) , Marked_a>
<Marked_activate(n__e) , Marked_e>
<Marked_activate(n__i) , Marked_i>
<Marked_activate(n__o) , Marked_o>
<Marked_activate(n__u) , Marked_u>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 2 components:

{  <Marked_activate(n__isPal(X)) , Marked_isPal(X)> 
      --> <Marked_isPal(V) , Marked_activate(V)>
  <Marked_activate(n__isPal(X)) , Marked_isPal(X)> 
     --> <Marked_isPal(V) , Marked_isNePal(activate(V))>
  <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
  <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
  <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))>
  <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_and(isNeList(activate(V1)),
                                           n__isList(activate(V2)))>
  <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
  <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
  <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))>
  <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                           n__isNeList(activate(V2)))>
  <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)> 
     --> <Marked_isNeList(V) , Marked_activate(V)>
  <Marked_activate(n__isList(X)) , Marked_isList(X)> 
     --> <Marked_isList(n____(V1,V2)) , Marked_activate(V2)>
  <Marked_activate(n__isList(X)) , Marked_isList(X)> 
     --> <Marked_isList(n____(V1,V2)) , Marked_activate(V1)>
  <Marked_activate(n__isList(X)) , Marked_isList(X)> 
     --> <Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))>
  <Marked_activate(n__isList(X)) , Marked_isList(X)> 
     --> <Marked_isList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                         n__isList(activate(V2)))>
  <Marked_activate(n__isList(X)) , Marked_isList(X)> 
     --> <Marked_isList(V) , Marked_activate(V)>
  <Marked_activate(n__isList(X)) , Marked_isList(X)> 
     --> <Marked_isList(V) , Marked_isNeList(activate(V))>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X2)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X2)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X2)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X2)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X2)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_activate(n____(X1,X2)) , Marked_activate(X1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isPal(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isPal(V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)>
  <Marked_isPal(V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)>
  <Marked_isPal(V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(n____(I,n____(P,I))) , Marked_and(isQid(activate(I)),
                                                 n__isPal(activate(P)))>
  <Marked_isPal(V) , Marked_isNePal(activate(V))> 
     --> <Marked_isNePal(V) , Marked_activate(V)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isNePal(n____(I,n____(P,I))) , Marked_and(isQid(activate(I)),
                                          n__isPal(activate(P)))> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNePal(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
  <Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
  <Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))>
  <Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_and(isNeList(activate(V1)),
                                           n__isList(activate(V2)))>
  <Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
  <Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
  <Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))>
  <Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                           n__isNeList(activate(V2)))>
  <Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))> 
     --> <Marked_isNeList(V) , Marked_activate(V)>
  <Marked_isNeList(n____(V1,V2)) , Marked_and(isNeList(activate(V1)),
                                    n__isList(activate(V2)))> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_activate(V2)>
  <Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_activate(V1)>
  <Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))>
  <Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                         n__isList(activate(V2)))>
  <Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(V) , Marked_activate(V)>
  <Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(V) , Marked_isNeList(activate(V))>
  <Marked_isNeList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                    n__isNeList(activate(V2)))> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_isNeList(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isNeList(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_isNeList(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_isNeList(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isNeList(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_isList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_isList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isList(n____(V1,V2)) , Marked_activate(V2)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_isList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_isList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isList(n____(V1,V2)) , Marked_activate(V1)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_activate(V2)>
  <Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_activate(V1)>
  <Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))>
  <Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                         n__isList(activate(V2)))>
  <Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(V) , Marked_activate(V)>
  <Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(V) , Marked_isNeList(activate(V))>
  <Marked_isList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                  n__isList(activate(V2)))> 
     --> <Marked_and(tt,X) , Marked_activate(X)>
  <Marked_isList(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_isList(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_isList(V) , Marked_activate(V)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_isList(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_isList(V) , Marked_activate(V)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
  <Marked_isList(V) , Marked_isNeList(activate(V))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
  <Marked_isList(V) , Marked_isNeList(activate(V))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
  <Marked_isList(V) , Marked_isNeList(activate(V))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))>
  <Marked_isList(V) , Marked_isNeList(activate(V))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_and(isNeList(activate(V1)),
                                           n__isList(activate(V2)))>
  <Marked_isList(V) , Marked_isNeList(activate(V))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
  <Marked_isList(V) , Marked_isNeList(activate(V))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
  <Marked_isList(V) , Marked_isNeList(activate(V))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))>
  <Marked_isList(V) , Marked_isNeList(activate(V))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                           n__isNeList(activate(V2)))>
  <Marked_isList(V) , Marked_isNeList(activate(V))> 
     --> <Marked_isNeList(V) , Marked_activate(V)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__isPal(X)) , Marked_isPal(X)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n__isList(X)) , Marked_isList(X)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
  <Marked_and(tt,X) , Marked_activate(X)> 
     --> <Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
}

{  <Marked___(__(X,Y),Z) , Marked___(Y,Z)> 
      --> <Marked___(__(X,Y),Z) , Marked___(Y,Z)>
  <Marked___(__(X,Y),Z) , Marked___(Y,Z)> 
     --> <Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))>
  <Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))> 
     --> <Marked___(__(X,Y),Z) , Marked___(Y,Z)>
  <Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))> 
     --> <Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))>
}
APPLY CRITERIA (Subterm criterion)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  __(__(X,Y),Z) >= __(X,__(Y,Z)) ;
  __(nil,X) >= X ;
  __(X,nil) >= X ;
  __(X1,X2) >= n____(X1,X2) ;
  nil >= n__nil ;
  activate(n__nil) >= nil ;
  activate(n__isList(X)) >= isList(X) ;
  activate(n____(X1,X2)) >= __(activate(X1),activate(X2)) ;
  activate(n__isNeList(X)) >= isNeList(X) ;
  activate(n__isPal(X)) >= isPal(X) ;
  activate(n__a) >= a ;
  activate(n__e) >= e ;
  activate(n__i) >= i ;
  activate(n__o) >= o ;
  activate(n__u) >= u ;
  activate(X) >= X ;
  and(tt,X) >= activate(X) ;
  isNeList(n____(V1,V2)) >= and(isNeList(activate(V1)),n__isList(activate(V2))) ;
  isNeList(n____(V1,V2)) >= and(isList(activate(V1)),n__isNeList(activate(V2))) ;
  isNeList(X) >= n__isNeList(X) ;
  isNeList(V) >= isQid(activate(V)) ;
  isList(n__nil) >= tt ;
  isList(n____(V1,V2)) >= and(isList(activate(V1)),n__isList(activate(V2))) ;
  isList(X) >= n__isList(X) ;
  isList(V) >= isNeList(activate(V)) ;
  isQid(n__a) >= tt ;
  isQid(n__e) >= tt ;
  isQid(n__i) >= tt ;
  isQid(n__o) >= tt ;
  isQid(n__u) >= tt ;
  isNePal(n____(I,n____(P,I))) >= and(isQid(activate(I)),n__isPal(activate(P))) ;
  isNePal(V) >= isQid(activate(V)) ;
  isPal(n__nil) >= tt ;
  isPal(X) >= n__isPal(X) ;
  isPal(V) >= isNePal(activate(V)) ;
  a >= n__a ;
  e >= n__e ;
  i >= n__i ;
  o >= n__o ;
  u >= n__u ;
  Marked_activate(n__isList(X)) >= Marked_isList(X) ;
  Marked_activate(n____(X1,X2)) >= Marked_activate(X1) ;
  Marked_activate(n____(X1,X2)) >= Marked_activate(X2) ;
  Marked_activate(n__isNeList(X)) >= Marked_isNeList(X) ;
  Marked_activate(n__isPal(X)) >= Marked_isPal(X) ;
  Marked_isPal(V) >= Marked_activate(V) ;
  Marked_isPal(V) >= Marked_isNePal(activate(V)) ;
  Marked_isNeList(n____(V1,V2)) >= Marked_activate(V1) ;
  Marked_isNeList(n____(V1,V2)) >= Marked_activate(V2) ;
  Marked_isNeList(n____(V1,V2)) >= Marked_isNeList(activate(V1)) ;
  Marked_isNeList(n____(V1,V2)) >= Marked_isList(activate(V1)) ;
  Marked_isNeList(n____(V1,V2)) >= Marked_and(isNeList(activate(V1)),
                                    n__isList(activate(V2))) ;
  Marked_isNeList(n____(V1,V2)) >= Marked_and(isList(activate(V1)),
                                    n__isNeList(activate(V2))) ;
  Marked_isNeList(V) >= Marked_activate(V) ;
  Marked_isList(n____(V1,V2)) >= Marked_activate(V1) ;
  Marked_isList(n____(V1,V2)) >= Marked_activate(V2) ;
  Marked_isList(n____(V1,V2)) >= Marked_isList(activate(V1)) ;
  Marked_isList(n____(V1,V2)) >= Marked_and(isList(activate(V1)),
                                  n__isList(activate(V2))) ;
  Marked_isList(V) >= Marked_activate(V) ;
  Marked_isList(V) >= Marked_isNeList(activate(V)) ;
  Marked_isNePal(n____(I,n____(P,I))) >= Marked_activate(I) ;
  Marked_isNePal(n____(I,n____(P,I))) >= Marked_activate(P) ;
  Marked_isNePal(n____(I,n____(P,I))) >= Marked_and(isQid(activate(I)),
                                          n__isPal(activate(P))) ;
  Marked_isNePal(V) >= Marked_activate(V) ;
  Marked_and(tt,X) >= Marked_activate(X) ;
 }
 + Disjunctions:{ 
{
  Marked_activate(n__isList(X)) > Marked_isList(X) ;
 }
{
  Marked_activate(n____(X1,X2)) > Marked_activate(X1) ;
 }
{
  Marked_activate(n____(X1,X2)) > Marked_activate(X2) ;
 }
{
  Marked_activate(n__isNeList(X)) > Marked_isNeList(X) ;
 }
{
  Marked_activate(n__isPal(X)) > Marked_isPal(X) ;
 }
{
  Marked_isPal(V) > Marked_activate(V) ;
 }
{
  Marked_isPal(V) > Marked_isNePal(activate(V)) ;
 }
{
  Marked_isNeList(n____(V1,V2)) > Marked_activate(V1) ;
 }
{
  Marked_isNeList(n____(V1,V2)) > Marked_activate(V2) ;
 }
{
  Marked_isNeList(n____(V1,V2)) > Marked_isNeList(activate(V1)) ;
 }
{
  Marked_isNeList(n____(V1,V2)) > Marked_isList(activate(V1)) ;
 }
{
  Marked_isNeList(n____(V1,V2)) > Marked_and(isNeList(activate(V1)),
                                   n__isList(activate(V2))) ;
 }
{
  Marked_isNeList(n____(V1,V2)) > Marked_and(isList(activate(V1)),
                                   n__isNeList(activate(V2))) ;
 }
{
  Marked_isNeList(V) > Marked_activate(V) ;
 }
{
  Marked_isList(n____(V1,V2)) > Marked_activate(V1) ;
 }
{
  Marked_isList(n____(V1,V2)) > Marked_activate(V2) ;
 }
{
  Marked_isList(n____(V1,V2)) > Marked_isList(activate(V1)) ;
 }
{
  Marked_isList(n____(V1,V2)) > Marked_and(isList(activate(V1)),
                                 n__isList(activate(V2))) ;
 }
{
  Marked_isList(V) > Marked_activate(V) ;
 }
{
  Marked_isList(V) > Marked_isNeList(activate(V)) ;
 }
{
  Marked_isNePal(n____(I,n____(P,I))) > Marked_activate(I) ;
 }
{
  Marked_isNePal(n____(I,n____(P,I))) > Marked_activate(P) ;
 }
{
  Marked_isNePal(n____(I,n____(P,I))) > Marked_and(isQid(activate(I)),
                                         n__isPal(activate(P))) ;
 }
{
  Marked_isNePal(V) > Marked_activate(V) ;
 }
{
  Marked_and(tt,X) > Marked_activate(X) ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: __(__(X,Y),Z) >= __(X,__(Y,Z))
constraint: __(nil,X) >= X
constraint: __(X,nil) >= X
constraint: __(X1,X2) >= n____(X1,X2)
constraint: nil >= n__nil
constraint: activate(n__nil) >= nil
constraint: activate(n__isList(X)) >= isList(X)
constraint: activate(n____(X1,X2)) >= __(activate(X1),activate(X2))
constraint: activate(n__isNeList(X)) >= isNeList(X)
constraint: activate(n__isPal(X)) >= isPal(X)
constraint: activate(n__a) >= a
constraint: activate(n__e) >= e
constraint: activate(n__i) >= i
constraint: activate(n__o) >= o
constraint: activate(n__u) >= u
constraint: activate(X) >= X
constraint: and(tt,X) >= activate(X)
constraint: isNeList(n____(V1,V2)) >= and(isNeList(activate(V1)),
                                       n__isList(activate(V2)))
constraint: isNeList(n____(V1,V2)) >= and(isList(activate(V1)),
                                       n__isNeList(activate(V2)))
constraint: isNeList(X) >= n__isNeList(X)
constraint: isNeList(V) >= isQid(activate(V))
constraint: isList(n__nil) >= tt
constraint: isList(n____(V1,V2)) >= and(isList(activate(V1)),
                                     n__isList(activate(V2)))
constraint: isList(X) >= n__isList(X)
constraint: isList(V) >= isNeList(activate(V))
constraint: isQid(n__a) >= tt
constraint: isQid(n__e) >= tt
constraint: isQid(n__i) >= tt
constraint: isQid(n__o) >= tt
constraint: isQid(n__u) >= tt
constraint: isNePal(n____(I,n____(P,I))) >= and(isQid(activate(I)),
                                             n__isPal(activate(P)))
constraint: isNePal(V) >= isQid(activate(V))
constraint: isPal(n__nil) >= tt
constraint: isPal(X) >= n__isPal(X)
constraint: isPal(V) >= isNePal(activate(V))
constraint: a >= n__a
constraint: e >= n__e
constraint: i >= n__i
constraint: o >= n__o
constraint: u >= n__u
constraint: Marked_activate(n__isList(X)) >= Marked_isList(X)
constraint: Marked_activate(n____(X1,X2)) >= Marked_activate(X1)
constraint: Marked_activate(n____(X1,X2)) >= Marked_activate(X2)
constraint: Marked_activate(n__isNeList(X)) >= Marked_isNeList(X)
constraint: Marked_activate(n__isPal(X)) >= Marked_isPal(X)
constraint: Marked_isPal(V) >= Marked_activate(V)
constraint: Marked_isPal(V) >= Marked_isNePal(activate(V))
constraint: Marked_isNeList(n____(V1,V2)) >= Marked_activate(V1)
constraint: Marked_isNeList(n____(V1,V2)) >= Marked_activate(V2)
constraint: Marked_isNeList(n____(V1,V2)) >= Marked_isNeList(activate(V1))
constraint: Marked_isNeList(n____(V1,V2)) >= Marked_isList(activate(V1))
constraint: Marked_isNeList(n____(V1,V2)) >= Marked_and(isNeList(activate(V1)),
                                              n__isList(activate(V2)))
constraint: Marked_isNeList(n____(V1,V2)) >= Marked_and(isList(activate(V1)),
                                              n__isNeList(activate(V2)))
constraint: Marked_isNeList(V) >= Marked_activate(V)
constraint: Marked_isList(n____(V1,V2)) >= Marked_activate(V1)
constraint: Marked_isList(n____(V1,V2)) >= Marked_activate(V2)
constraint: Marked_isList(n____(V1,V2)) >= Marked_isList(activate(V1))
constraint: Marked_isList(n____(V1,V2)) >= Marked_and(isList(activate(V1)),
                                            n__isList(activate(V2)))
constraint: Marked_isList(V) >= Marked_activate(V)
constraint: Marked_isList(V) >= Marked_isNeList(activate(V))
constraint: Marked_isNePal(n____(I,n____(P,I))) >= Marked_activate(I)
constraint: Marked_isNePal(n____(I,n____(P,I))) >= Marked_activate(P)
constraint: Marked_isNePal(n____(I,n____(P,I))) >= Marked_and(isQid(activate(I)),
                                                    n__isPal(activate(P)))
constraint: Marked_isNePal(V) >= Marked_activate(V)
constraint: Marked_and(tt,X) >= Marked_activate(X)
APPLY CRITERIA (Subterm criterion)

ST: Marked___ -> 1

APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
SOLVED
{
 
TRS termination of:
[1] __(__(X,Y),Z) -> __(X,__(Y,Z))
[2] __(X,nil) -> X
[3] __(nil,X) -> X
[4] and(tt,X) -> activate(X)
[5] isList(V) -> isNeList(activate(V))
[6] isList(n__nil) -> tt
[7] isList(n____(V1,V2)) -> and(isList(activate(V1)),n__isList(activate(V2)))
[8] isNeList(V) -> isQid(activate(V))
[9] isNeList(n____(V1,V2)) ->
 and(isList(activate(V1)),n__isNeList(activate(V2)))
[10] isNeList(n____(V1,V2)) ->
 and(isNeList(activate(V1)),n__isList(activate(V2)))
[11] isNePal(V) -> isQid(activate(V))
[12] isNePal(n____(I,n____(P,I))) ->
 and(isQid(activate(I)),n__isPal(activate(P)))
[13] isPal(V) -> isNePal(activate(V))
[14] isPal(n__nil) -> tt
[15] isQid(n__a) -> tt
[16] isQid(n__e) -> tt
[17] isQid(n__i) -> tt
[18] isQid(n__o) -> tt
[19] isQid(n__u) -> tt
[20] nil -> n__nil
[21] __(X1,X2) -> n____(X1,X2)
[22] isList(X) -> n__isList(X)
[23] isNeList(X) -> n__isNeList(X)
[24] isPal(X) -> n__isPal(X)
[25] a -> n__a
[26] e -> n__e
[27] i -> n__i
[28] o -> n__o
[29] u -> n__u
[30] activate(n__nil) -> nil
[31] activate(n____(X1,X2)) -> __(activate(X1),activate(X2))
[32] activate(n__isList(X)) -> isList(X)
[33] activate(n__isNeList(X)) -> isNeList(X)
[34] activate(n__isPal(X)) -> isPal(X)
[35] activate(n__a) -> a
[36] activate(n__e) -> e
[37] activate(n__i) -> i
[38] activate(n__o) -> o
[39] activate(n__u) -> u
[40] activate(X) -> X
 ,
 CRITERION: MDP
 [ {
      
     DP termination of:
     <Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))>
<Marked___(__(X,Y),Z) , Marked___(Y,Z)>
<Marked_and(tt,X) , Marked_activate(X)>
<Marked_isList(V) , Marked_isNeList(activate(V))>
<Marked_isList(V) , Marked_activate(V)>
<Marked_isList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                n__isList(activate(V2)))>
<Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))>
<Marked_isList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNeList(V) , Marked_isQid(activate(V))>
<Marked_isNeList(V) , Marked_activate(V)>
<Marked_isNeList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                  n__isNeList(activate(V2)))>
<Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNeList(n____(V1,V2)) , Marked_and(isNeList(activate(V1)),
                                  n__isList(activate(V2)))>
<Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNePal(V) , Marked_isQid(activate(V))>
<Marked_isNePal(V) , Marked_activate(V)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_and(isQid(activate(I)),
                                        n__isPal(activate(P)))>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_isQid(activate(I))>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)>
<Marked_isPal(V) , Marked_isNePal(activate(V))>
<Marked_isPal(V) , Marked_activate(V)>
<Marked_activate(n__nil) , Marked_nil>
<Marked_activate(n____(X1,X2)) , Marked___(activate(X1),activate(X2))>
<Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
<Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
<Marked_activate(n__isList(X)) , Marked_isList(X)>
<Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
<Marked_activate(n__isPal(X)) , Marked_isPal(X)>
<Marked_activate(n__a) , Marked_a>
<Marked_activate(n__e) , Marked_e>
<Marked_activate(n__i) , Marked_i>
<Marked_activate(n__o) , Marked_o>
<Marked_activate(n__u) , Marked_u>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_and(tt,X) , Marked_activate(X)>
<Marked_isList(V) , Marked_isNeList(activate(V))>
<Marked_isList(V) , Marked_activate(V)>
<Marked_isList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                n__isList(activate(V2)))>
<Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))>
<Marked_isList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNeList(V) , Marked_activate(V)>
<Marked_isNeList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                  n__isNeList(activate(V2)))>
<Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNeList(n____(V1,V2)) , Marked_and(isNeList(activate(V1)),
                                  n__isList(activate(V2)))>
<Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V1)>
<Marked_isNeList(n____(V1,V2)) , Marked_activate(V2)>
<Marked_isNePal(V) , Marked_activate(V)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_and(isQid(activate(I)),
                                        n__isPal(activate(P)))>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,n____(P,I))) , Marked_activate(P)>
<Marked_isPal(V) , Marked_isNePal(activate(V))>
<Marked_isPal(V) , Marked_activate(V)>
<Marked_activate(n____(X1,X2)) , Marked_activate(X1)>
<Marked_activate(n____(X1,X2)) , Marked_activate(X2)>
<Marked_activate(n__isList(X)) , Marked_isList(X)>
<Marked_activate(n__isNeList(X)) , Marked_isNeList(X)>
<Marked_activate(n__isPal(X)) , Marked_isPal(X)>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ __ ] (X0,X1) = 1*X1 + 2*X0 + 2; 
 [ Marked_isNeList ] (X0) = 2*X0; 
 [ n__e ] () = 3; 
 [ n__isList ] (X0) = 1*X0 + 1; 
 [ u ] () = 2; 
 [ tt ] () = 3; 
 [ a ] () = 2; 
 [ isNePal ] (X0) = 2*X0 + 1; 
 [ activate ] (X0) = 1*X0; 
 [ n__o ] () = 2; 
 [ isQid ] (X0) = 1*X0 + 1; 
 [ isList ] (X0) = 1*X0 + 1; 
 [ Marked_and ] (X0,X1) = 2*X1 + 2*X0; 
 [ i ] () = 2; 
 [ isPal ] (X0) = 2*X0 + 3; 
 [ nil ] () = 2; 
 [ Marked_isList ] (X0) = 2*X0; 
 [ n__i ] () = 2; 
 [ n____ ] (X0,X1) = 1*X1 + 2*X0 + 2; 
 [ Marked_activate ] (X0) = 2*X0; 
 [ isNeList ] (X0) = 1*X0 + 1; 
 [ Marked_isNePal ] (X0) = 3*X0 + 2; 
 [ e ] () = 3; 
 [ n__isPal ] (X0) = 2*X0 + 3; 
 [ and ] (X0,X1) = 1*X1 + 1*X0 + 1; 
 [ n__u ] () = 2; 
 [ n__isNeList ] (X0) = 1*X0 + 1; 
 [ n__nil ] () = 2; 
 [ o ] () = 2; 
 [ n__a ] () = 2; 
 [ Marked_isPal ] (X0) = 3*X0 + 2; 
 removing <Marked_and(tt,X),Marked_activate(X)><Marked_isList(n____(V1,V2)),
Marked_isList(activate(V1))><Marked_isList(n____(V1,V2)),Marked_activate(V1)><
Marked_isList(n____(V1,V2)),Marked_activate(V2)><Marked_isNeList(n____(V1,V2)),
Marked_isList(activate(V1))><Marked_isNeList(n____(V1,V2)),Marked_activate(V1)><
Marked_isNeList(n____(V1,V2)),Marked_activate(V2)><Marked_isNeList(n____(V1,V2)),
Marked_isNeList(activate(V1))><Marked_isNeList(n____(V1,V2)),Marked_activate(
                                                              V1)><Marked_isNeList(
                                                                    n____(
                                                                    V1,
                                                                    V2)),
Marked_activate(V2)><Marked_isNePal(V),Marked_activate(V)><Marked_isNePal(
                                                            n____(I,n____(P,I))),
Marked_and(isQid(activate(I)),n__isPal(activate(P)))><Marked_isNePal(
                                                       n____(I,n____(P,I))),
Marked_activate(I)><Marked_isNePal(n____(I,n____(P,I))),Marked_activate(P)><
Marked_isPal(V),Marked_activate(V)><Marked_activate(n____(X1,X2)),Marked_activate(
                                                                   X1)><
Marked_activate(n____(X1,X2)),Marked_activate(X2)><Marked_activate(n__isList(X)),
Marked_isList(X)><Marked_activate(n__isNeList(X)),Marked_isNeList(X)><
Marked_activate(n__isPal(X)),Marked_isPal(X)>
 [ {
      
     DP termination of:
     <Marked_isList(V) , Marked_isNeList(activate(V))>
<Marked_isList(V) , Marked_activate(V)>
<Marked_isList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                n__isList(activate(V2)))>
<Marked_isNeList(V) , Marked_activate(V)>
<Marked_isNeList(n____(V1,V2)) , Marked_and(isList(activate(V1)),
                                  n__isNeList(activate(V2)))>
<Marked_isNeList(n____(V1,V2)) , Marked_and(isNeList(activate(V1)),
                                  n__isList(activate(V2)))>
<Marked_isPal(V) , Marked_isNePal(activate(V))>
 ,
 CRITERION: SG
 [  ]} 
 ]} 
{
 
DP termination of:
<Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))>
<Marked___(__(X,Y),Z) , Marked___(Y,Z)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
 ]} 
 ]} 

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