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

TRS termination of:
[1] __(__(X,Y),Z) -> __(X,__(Y,Z))
[2] __(X,nil) -> X
[3] __(nil,X) -> X
[4] U11(tt) -> tt
[5] U21(tt,V2) -> U22(isList(activate(V2)))
[6] U22(tt) -> tt
[7] U31(tt) -> tt
[8] U41(tt,V2) -> U42(isNeList(activate(V2)))
[9] U42(tt) -> tt
[10] U51(tt,V2) -> U52(isList(activate(V2)))
[11] U52(tt) -> tt
[12] U61(tt) -> tt
[13] U71(tt,P) -> U72(isPal(activate(P)))
[14] U72(tt) -> tt
[15] U81(tt) -> tt
[16] isList(V) -> U11(isNeList(activate(V)))
[17] isList(n__nil) -> tt
[18] isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
[19] isNeList(V) -> U31(isQid(activate(V)))
[20] isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
[21] isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
[22] isNePal(V) -> U61(isQid(activate(V)))
[23] isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
[24] isPal(V) -> U81(isNePal(activate(V)))
[25] isPal(n__nil) -> tt
[26] isQid(n__a) -> tt
[27] isQid(n__e) -> tt
[28] isQid(n__i) -> tt
[29] isQid(n__o) -> tt
[30] isQid(n__u) -> tt
[31] nil -> n__nil
[32] __(X1,X2) -> n____(X1,X2)
[33] a -> n__a
[34] e -> n__e
[35] i -> n__i
[36] o -> n__o
[37] u -> n__u
[38] activate(n__nil) -> nil
[39] activate(n____(X1,X2)) -> __(X1,X2)
[40] activate(n__a) -> a
[41] activate(n__e) -> e
[42] activate(n__i) -> i
[43] activate(n__o) -> o
[44] activate(n__u) -> u
[45] 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_U21(tt,V2) , Marked_U22(isList(activate(V2)))>
<Marked_U21(tt,V2) , Marked_isList(activate(V2))>
<Marked_U21(tt,V2) , Marked_activate(V2)>
<Marked_U41(tt,V2) , Marked_U42(isNeList(activate(V2)))>
<Marked_U41(tt,V2) , Marked_isNeList(activate(V2))>
<Marked_U41(tt,V2) , Marked_activate(V2)>
<Marked_U51(tt,V2) , Marked_U52(isList(activate(V2)))>
<Marked_U51(tt,V2) , Marked_isList(activate(V2))>
<Marked_U51(tt,V2) , Marked_activate(V2)>
<Marked_U71(tt,P) , Marked_U72(isPal(activate(P)))>
<Marked_U71(tt,P) , Marked_isPal(activate(P))>
<Marked_U71(tt,P) , Marked_activate(P)>
<Marked_isList(V) , Marked_U11(isNeList(activate(V)))>
<Marked_isList(V) , Marked_isNeList(activate(V))>
<Marked_isList(V) , Marked_activate(V)>
<Marked_isList(n____(V1,V2)) , Marked_U21(isList(activate(V1)),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_U31(isQid(activate(V)))>
<Marked_isNeList(V) , Marked_isQid(activate(V))>
<Marked_isNeList(V) , Marked_activate(V)>
<Marked_isNeList(n____(V1,V2)) , Marked_U41(isList(activate(V1)),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_U51(isNeList(activate(V1)),
                                  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_U61(isQid(activate(V)))>
<Marked_isNePal(V) , Marked_isQid(activate(V))>
<Marked_isNePal(V) , Marked_activate(V)>
<Marked_isNePal(n____(I,__(P,I))) , Marked_U71(isQid(activate(I)),activate(P))>
<Marked_isNePal(n____(I,__(P,I))) , Marked_isQid(activate(I))>
<Marked_isNePal(n____(I,__(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,__(P,I))) , Marked_activate(P)>
<Marked_isPal(V) , Marked_U81(isNePal(activate(V)))>
<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___(X1,X2)>
<Marked_activate(n__a) , Marked_a>
<Marked_activate(n__e) , Marked_e>
<Marked_activate(n__i) , Marked_i>
<Marked_activate(n__o) , Marked_o>
<Marked_activate(n__u) , Marked_u>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 3 components:

{  <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_U51(isNeList(activate(V1)),
                                           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_isNeList(activate(V1))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U41(isList(activate(V1)),
                                           activate(V2))>
  <Marked_isNeList(n____(V1,V2)) , Marked_U51(isNeList(activate(V1)),
                                    activate(V2))> 
     --> <Marked_U51(tt,V2) , Marked_isList(activate(V2))>
  <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_U21(isList(activate(V1)),
                                         activate(V2))>
  <Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(V) , Marked_isNeList(activate(V))>
  <Marked_isNeList(n____(V1,V2)) , Marked_U41(isList(activate(V1)),
                                    activate(V2))> 
     --> <Marked_U41(tt,V2) , Marked_isNeList(activate(V2))>
  <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_U21(isList(activate(V1)),
                                         activate(V2))>
  <Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))> 
     --> <Marked_isList(V) , Marked_isNeList(activate(V))>
  <Marked_isList(n____(V1,V2)) , Marked_U21(isList(activate(V1)),activate(V2))> 
     --> <Marked_U21(tt,V2) , Marked_isList(activate(V2))>
  <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_U51(isNeList(activate(V1)),
                                           activate(V2))>
  <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_U41(isList(activate(V1)),
                                           activate(V2))>
  <Marked_U51(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))>
  <Marked_U51(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_U21(isList(activate(V1)),
                                         activate(V2))>
  <Marked_U51(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(V) , Marked_isNeList(activate(V))>
  <Marked_U41(tt,V2) , Marked_isNeList(activate(V2))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))>
  <Marked_U41(tt,V2) , Marked_isNeList(activate(V2))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U51(isNeList(activate(V1)),
                                           activate(V2))>
  <Marked_U41(tt,V2) , Marked_isNeList(activate(V2))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))>
  <Marked_U41(tt,V2) , Marked_isNeList(activate(V2))> 
     --> <Marked_isNeList(n____(V1,V2)) , Marked_U41(isList(activate(V1)),
                                           activate(V2))>
  <Marked_U21(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))>
  <Marked_U21(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(n____(V1,V2)) , Marked_U21(isList(activate(V1)),
                                         activate(V2))>
  <Marked_U21(tt,V2) , Marked_isList(activate(V2))> 
     --> <Marked_isList(V) , Marked_isNeList(activate(V))>
}

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

{  <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 (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 ;
  U11(tt) >= tt ;
  U22(tt) >= tt ;
  isList(n__nil) >= tt ;
  isList(n____(V1,V2)) >= U21(isList(activate(V1)),activate(V2)) ;
  isList(V) >= U11(isNeList(activate(V))) ;
  activate(n__nil) >= nil ;
  activate(n____(X1,X2)) >= __(X1,X2) ;
  activate(n__a) >= a ;
  activate(n__e) >= e ;
  activate(n__i) >= i ;
  activate(n__o) >= o ;
  activate(n__u) >= u ;
  activate(X) >= X ;
  U21(tt,V2) >= U22(isList(activate(V2))) ;
  U31(tt) >= tt ;
  U42(tt) >= tt ;
  isNeList(n____(V1,V2)) >= U41(isList(activate(V1)),activate(V2)) ;
  isNeList(n____(V1,V2)) >= U51(isNeList(activate(V1)),activate(V2)) ;
  isNeList(V) >= U31(isQid(activate(V))) ;
  U41(tt,V2) >= U42(isNeList(activate(V2))) ;
  U52(tt) >= tt ;
  U51(tt,V2) >= U52(isList(activate(V2))) ;
  U61(tt) >= tt ;
  U72(tt) >= tt ;
  isPal(n__nil) >= tt ;
  isPal(V) >= U81(isNePal(activate(V))) ;
  U71(tt,P) >= U72(isPal(activate(P))) ;
  U81(tt) >= tt ;
  isQid(n__a) >= tt ;
  isQid(n__e) >= tt ;
  isQid(n__i) >= tt ;
  isQid(n__o) >= tt ;
  isQid(n__u) >= tt ;
  isNePal(n____(I,__(P,I))) >= U71(isQid(activate(I)),activate(P)) ;
  isNePal(V) >= U61(isQid(activate(V))) ;
  a >= n__a ;
  e >= n__e ;
  i >= n__i ;
  o >= n__o ;
  u >= n__u ;
  Marked_isNeList(n____(V1,V2)) >= Marked_isNeList(activate(V1)) ;
  Marked_isNeList(n____(V1,V2)) >= Marked_U51(isNeList(activate(V1)),
                                    activate(V2)) ;
  Marked_isNeList(n____(V1,V2)) >= Marked_U41(isList(activate(V1)),
                                    activate(V2)) ;
  Marked_isNeList(n____(V1,V2)) >= Marked_isList(activate(V1)) ;
  Marked_U51(tt,V2) >= Marked_isList(activate(V2)) ;
  Marked_U41(tt,V2) >= Marked_isNeList(activate(V2)) ;
  Marked_isList(n____(V1,V2)) >= Marked_isList(activate(V1)) ;
  Marked_isList(n____(V1,V2)) >= Marked_U21(isList(activate(V1)),activate(V2)) ;
  Marked_isList(V) >= Marked_isNeList(activate(V)) ;
  Marked_U21(tt,V2) >= Marked_isList(activate(V2)) ;
 }
 + Disjunctions:{ 
{
  Marked_isNeList(n____(V1,V2)) > Marked_isNeList(activate(V1)) ;
 }
{
  Marked_isNeList(n____(V1,V2)) > Marked_U51(isNeList(activate(V1)),
                                   activate(V2)) ;
 }
{
  Marked_isNeList(n____(V1,V2)) > Marked_U41(isList(activate(V1)),activate(V2)) ;
 }
{
  Marked_isNeList(n____(V1,V2)) > Marked_isList(activate(V1)) ;
 }
{
  Marked_U51(tt,V2) > Marked_isList(activate(V2)) ;
 }
{
  Marked_U41(tt,V2) > Marked_isNeList(activate(V2)) ;
 }
{
  Marked_isList(n____(V1,V2)) > Marked_isList(activate(V1)) ;
 }
{
  Marked_isList(n____(V1,V2)) > Marked_U21(isList(activate(V1)),activate(V2)) ;
 }
{
  Marked_isList(V) > Marked_isNeList(activate(V)) ;
 }
{
  Marked_U21(tt,V2) > Marked_isList(activate(V2)) ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: __(__(X,Y),Z) >= __(X,__(Y,Z))
constraint: __(nil,X) >= X
constraint: __(X,nil) >= X
constraint: __(X1,X2) >= n____(X1,X2)
constraint: nil >= n__nil
constraint: U11(tt) >= tt
constraint: U22(tt) >= tt
constraint: isList(n__nil) >= tt
constraint: isList(n____(V1,V2)) >= U21(isList(activate(V1)),activate(V2))
constraint: isList(V) >= U11(isNeList(activate(V)))
constraint: activate(n__nil) >= nil
constraint: activate(n____(X1,X2)) >= __(X1,X2)
constraint: activate(n__a) >= a
constraint: activate(n__e) >= e
constraint: activate(n__i) >= i
constraint: activate(n__o) >= o
constraint: activate(n__u) >= u
constraint: activate(X) >= X
constraint: U21(tt,V2) >= U22(isList(activate(V2)))
constraint: U31(tt) >= tt
constraint: U42(tt) >= tt
constraint: isNeList(n____(V1,V2)) >= U41(isList(activate(V1)),activate(V2))
constraint: isNeList(n____(V1,V2)) >= U51(isNeList(activate(V1)),activate(V2))
constraint: isNeList(V) >= U31(isQid(activate(V)))
constraint: U41(tt,V2) >= U42(isNeList(activate(V2)))
constraint: U52(tt) >= tt
constraint: U51(tt,V2) >= U52(isList(activate(V2)))
constraint: U61(tt) >= tt
constraint: U72(tt) >= tt
constraint: isPal(n__nil) >= tt
constraint: isPal(V) >= U81(isNePal(activate(V)))
constraint: U71(tt,P) >= U72(isPal(activate(P)))
constraint: U81(tt) >= tt
constraint: isQid(n__a) >= tt
constraint: isQid(n__e) >= tt
constraint: isQid(n__i) >= tt
constraint: isQid(n__o) >= tt
constraint: isQid(n__u) >= tt
constraint: isNePal(n____(I,__(P,I))) >= U71(isQid(activate(I)),activate(P))
constraint: isNePal(V) >= U61(isQid(activate(V)))
constraint: a >= n__a
constraint: e >= n__e
constraint: i >= n__i
constraint: o >= n__o
constraint: u >= n__u
constraint: Marked_isNeList(n____(V1,V2)) >= Marked_isNeList(activate(V1))
constraint: Marked_isNeList(n____(V1,V2)) >= Marked_U51(isNeList(activate(V1)),
                                              activate(V2))
constraint: Marked_isNeList(n____(V1,V2)) >= Marked_U41(isList(activate(V1)),
                                              activate(V2))
constraint: Marked_isNeList(n____(V1,V2)) >= Marked_isList(activate(V1))
constraint: Marked_U51(tt,V2) >= Marked_isList(activate(V2))
constraint: Marked_U41(tt,V2) >= Marked_isNeList(activate(V2))
constraint: Marked_isList(n____(V1,V2)) >= Marked_isList(activate(V1))
constraint: Marked_isList(n____(V1,V2)) >= Marked_U21(isList(activate(V1)),
                                            activate(V2))
constraint: Marked_isList(V) >= Marked_isNeList(activate(V))
constraint: Marked_U21(tt,V2) >= Marked_isList(activate(V2))
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 ;
  U11(tt) >= tt ;
  U22(tt) >= tt ;
  isList(n__nil) >= tt ;
  isList(n____(V1,V2)) >= U21(isList(activate(V1)),activate(V2)) ;
  isList(V) >= U11(isNeList(activate(V))) ;
  activate(n__nil) >= nil ;
  activate(n____(X1,X2)) >= __(X1,X2) ;
  activate(n__a) >= a ;
  activate(n__e) >= e ;
  activate(n__i) >= i ;
  activate(n__o) >= o ;
  activate(n__u) >= u ;
  activate(X) >= X ;
  U21(tt,V2) >= U22(isList(activate(V2))) ;
  U31(tt) >= tt ;
  U42(tt) >= tt ;
  isNeList(n____(V1,V2)) >= U41(isList(activate(V1)),activate(V2)) ;
  isNeList(n____(V1,V2)) >= U51(isNeList(activate(V1)),activate(V2)) ;
  isNeList(V) >= U31(isQid(activate(V))) ;
  U41(tt,V2) >= U42(isNeList(activate(V2))) ;
  U52(tt) >= tt ;
  U51(tt,V2) >= U52(isList(activate(V2))) ;
  U61(tt) >= tt ;
  U72(tt) >= tt ;
  isPal(n__nil) >= tt ;
  isPal(V) >= U81(isNePal(activate(V))) ;
  U71(tt,P) >= U72(isPal(activate(P))) ;
  U81(tt) >= tt ;
  isQid(n__a) >= tt ;
  isQid(n__e) >= tt ;
  isQid(n__i) >= tt ;
  isQid(n__o) >= tt ;
  isQid(n__u) >= tt ;
  isNePal(n____(I,__(P,I))) >= U71(isQid(activate(I)),activate(P)) ;
  isNePal(V) >= U61(isQid(activate(V))) ;
  a >= n__a ;
  e >= n__e ;
  i >= n__i ;
  o >= n__o ;
  u >= n__u ;
  Marked_isPal(V) >= Marked_isNePal(activate(V)) ;
  Marked_isNePal(n____(I,__(P,I))) >= Marked_U71(isQid(activate(I)),
                                       activate(P)) ;
  Marked_U71(tt,P) >= Marked_isPal(activate(P)) ;
 }
 + Disjunctions:{ 
{
  Marked_isPal(V) > Marked_isNePal(activate(V)) ;
 }
{
  Marked_isNePal(n____(I,__(P,I))) > Marked_U71(isQid(activate(I)),activate(P)) ;
 }
{
  Marked_U71(tt,P) > Marked_isPal(activate(P)) ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
Sat solver result read
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
constraint: __(__(X,Y),Z) >= __(X,__(Y,Z))
constraint: __(nil,X) >= X
constraint: __(X,nil) >= X
constraint: __(X1,X2) >= n____(X1,X2)
constraint: nil >= n__nil
constraint: U11(tt) >= tt
constraint: U22(tt) >= tt
constraint: isList(n__nil) >= tt
constraint: isList(n____(V1,V2)) >= U21(isList(activate(V1)),activate(V2))
constraint: isList(V) >= U11(isNeList(activate(V)))
constraint: activate(n__nil) >= nil
constraint: activate(n____(X1,X2)) >= __(X1,X2)
constraint: activate(n__a) >= a
constraint: activate(n__e) >= e
constraint: activate(n__i) >= i
constraint: activate(n__o) >= o
constraint: activate(n__u) >= u
constraint: activate(X) >= X
constraint: U21(tt,V2) >= U22(isList(activate(V2)))
constraint: U31(tt) >= tt
constraint: U42(tt) >= tt
constraint: isNeList(n____(V1,V2)) >= U41(isList(activate(V1)),activate(V2))
constraint: isNeList(n____(V1,V2)) >= U51(isNeList(activate(V1)),activate(V2))
constraint: isNeList(V) >= U31(isQid(activate(V)))
constraint: U41(tt,V2) >= U42(isNeList(activate(V2)))
constraint: U52(tt) >= tt
constraint: U51(tt,V2) >= U52(isList(activate(V2)))
constraint: U61(tt) >= tt
constraint: U72(tt) >= tt
constraint: isPal(n__nil) >= tt
constraint: isPal(V) >= U81(isNePal(activate(V)))
constraint: U71(tt,P) >= U72(isPal(activate(P)))
constraint: U81(tt) >= tt
constraint: isQid(n__a) >= tt
constraint: isQid(n__e) >= tt
constraint: isQid(n__i) >= tt
constraint: isQid(n__o) >= tt
constraint: isQid(n__u) >= tt
constraint: isNePal(n____(I,__(P,I))) >= U71(isQid(activate(I)),activate(P))
constraint: isNePal(V) >= U61(isQid(activate(V)))
constraint: a >= n__a
constraint: e >= n__e
constraint: i >= n__i
constraint: o >= n__o
constraint: u >= n__u
constraint: Marked_isPal(V) >= Marked_isNePal(activate(V))
constraint: Marked_isNePal(n____(I,__(P,I))) >= Marked_U71(isQid(activate(I)),
                                                 activate(P))
constraint: Marked_U71(tt,P) >= Marked_isPal(activate(P))
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 ;
  U11(tt) >= tt ;
  U22(tt) >= tt ;
  isList(n__nil) >= tt ;
  isList(n____(V1,V2)) >= U21(isList(activate(V1)),activate(V2)) ;
  isList(V) >= U11(isNeList(activate(V))) ;
  activate(n__nil) >= nil ;
  activate(n____(X1,X2)) >= __(X1,X2) ;
  activate(n__a) >= a ;
  activate(n__e) >= e ;
  activate(n__i) >= i ;
  activate(n__o) >= o ;
  activate(n__u) >= u ;
  activate(X) >= X ;
  U21(tt,V2) >= U22(isList(activate(V2))) ;
  U31(tt) >= tt ;
  U42(tt) >= tt ;
  isNeList(n____(V1,V2)) >= U41(isList(activate(V1)),activate(V2)) ;
  isNeList(n____(V1,V2)) >= U51(isNeList(activate(V1)),activate(V2)) ;
  isNeList(V) >= U31(isQid(activate(V))) ;
  U41(tt,V2) >= U42(isNeList(activate(V2))) ;
  U52(tt) >= tt ;
  U51(tt,V2) >= U52(isList(activate(V2))) ;
  U61(tt) >= tt ;
  U72(tt) >= tt ;
  isPal(n__nil) >= tt ;
  isPal(V) >= U81(isNePal(activate(V))) ;
  U71(tt,P) >= U72(isPal(activate(P))) ;
  U81(tt) >= tt ;
  isQid(n__a) >= tt ;
  isQid(n__e) >= tt ;
  isQid(n__i) >= tt ;
  isQid(n__o) >= tt ;
  isQid(n__u) >= tt ;
  isNePal(n____(I,__(P,I))) >= U71(isQid(activate(I)),activate(P)) ;
  isNePal(V) >= U61(isQid(activate(V))) ;
  a >= n__a ;
  e >= n__e ;
  i >= n__i ;
  o >= n__o ;
  u >= n__u ;
  Marked___(__(X,Y),Z) >= Marked___(X,__(Y,Z)) ;
  Marked___(__(X,Y),Z) >= Marked___(Y,Z) ;
 }
 + Disjunctions:{ 
{
  Marked___(__(X,Y),Z) > Marked___(X,__(Y,Z)) ;
 }
{
  Marked___(__(X,Y),Z) > Marked___(Y,Z) ;
 }
 } 
=== 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: U11(tt) >= tt
constraint: U22(tt) >= tt
constraint: isList(n__nil) >= tt
constraint: isList(n____(V1,V2)) >= U21(isList(activate(V1)),activate(V2))
constraint: isList(V) >= U11(isNeList(activate(V)))
constraint: activate(n__nil) >= nil
constraint: activate(n____(X1,X2)) >= __(X1,X2)
constraint: activate(n__a) >= a
constraint: activate(n__e) >= e
constraint: activate(n__i) >= i
constraint: activate(n__o) >= o
constraint: activate(n__u) >= u
constraint: activate(X) >= X
constraint: U21(tt,V2) >= U22(isList(activate(V2)))
constraint: U31(tt) >= tt
constraint: U42(tt) >= tt
constraint: isNeList(n____(V1,V2)) >= U41(isList(activate(V1)),activate(V2))
constraint: isNeList(n____(V1,V2)) >= U51(isNeList(activate(V1)),activate(V2))
constraint: isNeList(V) >= U31(isQid(activate(V)))
constraint: U41(tt,V2) >= U42(isNeList(activate(V2)))
constraint: U52(tt) >= tt
constraint: U51(tt,V2) >= U52(isList(activate(V2)))
constraint: U61(tt) >= tt
constraint: U72(tt) >= tt
constraint: isPal(n__nil) >= tt
constraint: isPal(V) >= U81(isNePal(activate(V)))
constraint: U71(tt,P) >= U72(isPal(activate(P)))
constraint: U81(tt) >= tt
constraint: isQid(n__a) >= tt
constraint: isQid(n__e) >= tt
constraint: isQid(n__i) >= tt
constraint: isQid(n__o) >= tt
constraint: isQid(n__u) >= tt
constraint: isNePal(n____(I,__(P,I))) >= U71(isQid(activate(I)),activate(P))
constraint: isNePal(V) >= U61(isQid(activate(V)))
constraint: a >= n__a
constraint: e >= n__e
constraint: i >= n__i
constraint: o >= n__o
constraint: u >= n__u
constraint: Marked___(__(X,Y),Z) >= Marked___(X,__(Y,Z))
constraint: Marked___(__(X,Y),Z) >= Marked___(Y,Z)
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
SOLVED
{
 
TRS termination of:
[1] __(__(X,Y),Z) -> __(X,__(Y,Z))
[2] __(X,nil) -> X
[3] __(nil,X) -> X
[4] U11(tt) -> tt
[5] U21(tt,V2) -> U22(isList(activate(V2)))
[6] U22(tt) -> tt
[7] U31(tt) -> tt
[8] U41(tt,V2) -> U42(isNeList(activate(V2)))
[9] U42(tt) -> tt
[10] U51(tt,V2) -> U52(isList(activate(V2)))
[11] U52(tt) -> tt
[12] U61(tt) -> tt
[13] U71(tt,P) -> U72(isPal(activate(P)))
[14] U72(tt) -> tt
[15] U81(tt) -> tt
[16] isList(V) -> U11(isNeList(activate(V)))
[17] isList(n__nil) -> tt
[18] isList(n____(V1,V2)) -> U21(isList(activate(V1)),activate(V2))
[19] isNeList(V) -> U31(isQid(activate(V)))
[20] isNeList(n____(V1,V2)) -> U41(isList(activate(V1)),activate(V2))
[21] isNeList(n____(V1,V2)) -> U51(isNeList(activate(V1)),activate(V2))
[22] isNePal(V) -> U61(isQid(activate(V)))
[23] isNePal(n____(I,__(P,I))) -> U71(isQid(activate(I)),activate(P))
[24] isPal(V) -> U81(isNePal(activate(V)))
[25] isPal(n__nil) -> tt
[26] isQid(n__a) -> tt
[27] isQid(n__e) -> tt
[28] isQid(n__i) -> tt
[29] isQid(n__o) -> tt
[30] isQid(n__u) -> tt
[31] nil -> n__nil
[32] __(X1,X2) -> n____(X1,X2)
[33] a -> n__a
[34] e -> n__e
[35] i -> n__i
[36] o -> n__o
[37] u -> n__u
[38] activate(n__nil) -> nil
[39] activate(n____(X1,X2)) -> __(X1,X2)
[40] activate(n__a) -> a
[41] activate(n__e) -> e
[42] activate(n__i) -> i
[43] activate(n__o) -> o
[44] activate(n__u) -> u
[45] activate(X) -> X
 ,
 CRITERION: MDP
 [ {
      
     DP termination of:
     <Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))>
<Marked___(__(X,Y),Z) , Marked___(Y,Z)>
<Marked_U21(tt,V2) , Marked_U22(isList(activate(V2)))>
<Marked_U21(tt,V2) , Marked_isList(activate(V2))>
<Marked_U21(tt,V2) , Marked_activate(V2)>
<Marked_U41(tt,V2) , Marked_U42(isNeList(activate(V2)))>
<Marked_U41(tt,V2) , Marked_isNeList(activate(V2))>
<Marked_U41(tt,V2) , Marked_activate(V2)>
<Marked_U51(tt,V2) , Marked_U52(isList(activate(V2)))>
<Marked_U51(tt,V2) , Marked_isList(activate(V2))>
<Marked_U51(tt,V2) , Marked_activate(V2)>
<Marked_U71(tt,P) , Marked_U72(isPal(activate(P)))>
<Marked_U71(tt,P) , Marked_isPal(activate(P))>
<Marked_U71(tt,P) , Marked_activate(P)>
<Marked_isList(V) , Marked_U11(isNeList(activate(V)))>
<Marked_isList(V) , Marked_isNeList(activate(V))>
<Marked_isList(V) , Marked_activate(V)>
<Marked_isList(n____(V1,V2)) , Marked_U21(isList(activate(V1)),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_U31(isQid(activate(V)))>
<Marked_isNeList(V) , Marked_isQid(activate(V))>
<Marked_isNeList(V) , Marked_activate(V)>
<Marked_isNeList(n____(V1,V2)) , Marked_U41(isList(activate(V1)),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_U51(isNeList(activate(V1)),
                                  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_U61(isQid(activate(V)))>
<Marked_isNePal(V) , Marked_isQid(activate(V))>
<Marked_isNePal(V) , Marked_activate(V)>
<Marked_isNePal(n____(I,__(P,I))) , Marked_U71(isQid(activate(I)),activate(P))>
<Marked_isNePal(n____(I,__(P,I))) , Marked_isQid(activate(I))>
<Marked_isNePal(n____(I,__(P,I))) , Marked_activate(I)>
<Marked_isNePal(n____(I,__(P,I))) , Marked_activate(P)>
<Marked_isPal(V) , Marked_U81(isNePal(activate(V)))>
<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___(X1,X2)>
<Marked_activate(n__a) , Marked_a>
<Marked_activate(n__e) , Marked_e>
<Marked_activate(n__i) , Marked_i>
<Marked_activate(n__o) , Marked_o>
<Marked_activate(n__u) , Marked_u>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_U21(tt,V2) , Marked_isList(activate(V2))>
<Marked_U41(tt,V2) , Marked_isNeList(activate(V2))>
<Marked_U51(tt,V2) , Marked_isList(activate(V2))>
<Marked_isList(V) , Marked_isNeList(activate(V))>
<Marked_isList(n____(V1,V2)) , Marked_U21(isList(activate(V1)),activate(V2))>
<Marked_isList(n____(V1,V2)) , Marked_isList(activate(V1))>
<Marked_isNeList(n____(V1,V2)) , Marked_U41(isList(activate(V1)),activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_isList(activate(V1))>
<Marked_isNeList(n____(V1,V2)) , Marked_U51(isNeList(activate(V1)),
                                  activate(V2))>
<Marked_isNeList(n____(V1,V2)) , Marked_isNeList(activate(V1))>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ __ ] (X0,X1) = 1*X1 + 2*X0 + 2; 
 [ u ] () = 2; 
 [ isPal ] (X0) = 2; 
 [ Marked_U51 ] (X0,X1) = 2*X1 + 2; 
 [ U31 ] (X0) = 1*X0; 
 [ n__e ] () = 1; 
 [ U22 ] (X0) = 1*X0; 
 [ n____ ] (X0,X1) = 1*X1 + 2*X0 + 2; 
 [ Marked_U21 ] (X0,X1) = 2*X1 + 1*X0 + 3; 
 [ U52 ] (X0) = 2; 
 [ a ] () = 1; 
 [ tt ] () = 2; 
 [ U81 ] (X0) = 2; 
 [ Marked_isList ] (X0) = 2*X0 + 2; 
 [ isNeList ] (X0) = 3*X0; 
 [ n__o ] () = 1; 
 [ activate ] (X0) = 1*X0; 
 [ isNePal ] (X0) = 2; 
 [ U61 ] (X0) = 2; 
 [ i ] () = 1; 
 [ nil ] () = 0; 
 [ U71 ] (X0,X1) = 2; 
 [ Marked_U41 ] (X0,X1) = 2*X1 + 1; 
 [ U42 ] (X0) = 1*X0; 
 [ n__i ] () = 1; 
 [ isList ] (X0) = 1*X0 + 3; 
 [ isQid ] (X0) = 2*X0; 
 [ U51 ] (X0,X1) = 1*X0; 
 [ e ] () = 1; 
 [ U11 ] (X0) = 2; 
 [ n__nil ] () = 0; 
 [ U41 ] (X0,X1) = 3*X1 + 2; 
 [ n__u ] () = 2; 
 [ U21 ] (X0,X1) = 1*X1 + 3; 
 [ n__a ] () = 1; 
 [ U72 ] (X0) = 2; 
 [ Marked_isNeList ] (X0) = 2*X0; 
 [ o ] () = 1; 
 removing <Marked_U21(tt,V2),Marked_isList(activate(V2))><Marked_U41(tt,V2),
Marked_isNeList(activate(V2))><Marked_isList(V),Marked_isNeList(activate(V))><
Marked_isList(n____(V1,V2)),Marked_isList(activate(V1))><Marked_isNeList(
                                                          n____(V1,V2)),
Marked_U41(isList(activate(V1)),activate(V2))><Marked_isNeList(n____(V1,V2)),
Marked_isList(activate(V1))><Marked_isNeList(n____(V1,V2)),Marked_U51(
                                                            isNeList(
                                                             activate(
                                                              V1)),
                                                            activate(V2))><
Marked_isNeList(n____(V1,V2)),Marked_isNeList(activate(V1))>
 [ {
      
     DP termination of:
     <Marked_U51(tt,V2) , Marked_isList(activate(V2))>
<Marked_isList(n____(V1,V2)) , Marked_U21(isList(activate(V1)),activate(V2))>
 ,
 CRITERION: SG
 [  ]} 
 ]} 
{
 
DP termination of:
<Marked_U71(tt,P) , Marked_isPal(activate(P))>
<Marked_isNePal(n____(I,__(P,I))) , Marked_U71(isQid(activate(I)),activate(P))>
<Marked_isPal(V) , Marked_isNePal(activate(V))>
 ,
 CRITERION: CG using polynomial interpretation = 
 [ __ ] (X0,X1) = 1*X1 + 2*X0 + 2; 
 [ u ] () = 0; 
 [ isPal ] (X0) = 0; 
 [ U31 ] (X0) = 0; 
 [ n__e ] () = 0; 
 [ U22 ] (X0) = 0; 
 [ n____ ] (X0,X1) = 1*X1 + 2*X0 + 2; 
 [ U52 ] (X0) = 0; 
 [ Marked_isNePal ] (X0) = 2*X0; 
 [ a ] () = 0; 
 [ tt ] () = 0; 
 [ U81 ] (X0) = 0; 
 [ isNeList ] (X0) = 0; 
 [ Marked_isPal ] (X0) = 2*X0; 
 [ n__o ] () = 0; 
 [ activate ] (X0) = 1*X0; 
 [ isNePal ] (X0) = 2; 
 [ U61 ] (X0) = 0; 
 [ i ] () = 0; 
 [ nil ] () = 0; 
 [ U71 ] (X0,X1) = 0; 
 [ U42 ] (X0) = 0; 
 [ n__i ] () = 0; 
 [ isList ] (X0) = 2*X0; 
 [ isQid ] (X0) = 0; 
 [ U51 ] (X0,X1) = 0; 
 [ Marked_U71 ] (X0,X1) = 2*X1; 
 [ e ] () = 0; 
 [ U11 ] (X0) = 0; 
 [ n__nil ] () = 0; 
 [ U41 ] (X0,X1) = 0; 
 [ n__u ] () = 0; 
 [ U21 ] (X0,X1) = 0; 
 [ n__a ] () = 0; 
 [ U72 ] (X0) = 0; 
 [ o ] () = 0; 
 removing <Marked_isNePal(n____(I,__(P,I))),Marked_U71(isQid(activate(I)),
                                             activate(P))>
 [ {
      
     DP termination of:
     <Marked_U71(tt,P) , Marked_isPal(activate(P))>
<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: ORD
 [ 
     Solution found:
     polynomial interpretation = 
      [ __ ] (X0,X1) = 3 + 1*X0 + 1*X1 + 0; 
 [ u ] () = 3 + 0; 
 [ isPal ] (X0) = 0; 
 [ U31 ] (X0) = 0; 
 [ n__e ] () = 0; 
 [ U22 ] (X0) = 0; 
 [ n____ ] (X0,X1) = 2 + 1*X0 + 1*X1 + 0; 
 [ U52 ] (X0) = 0; 
 [ a ] () = 3 + 0; 
 [ tt ] () = 0; 
 [ U81 ] (X0) = 0; 
 [ isNeList ] (X0) = 2 + 2*X0 + 0; 
 [ n__o ] () = 0; 
 [ activate ] (X0) = 3 + 1*X0 + 0; 
 [ isNePal ] (X0) = 1 + 3*X0 + 0; 
 [ U61 ] (X0) = 0; 
 [ i ] () = 3 + 0; 
 [ nil ] () = 3 + 0; 
 [ U71 ] (X0,X1) = 2 + 1*X0 + 0; 
 [ U42 ] (X0) = 0; 
 [ n__i ] () = 0; 
 [ isList ] (X0) = 2 + 0; 
 [ isQid ] (X0) = 3 + 1*X0 + 0; 
 [ U51 ] (X0,X1) = 0; 
 [ e ] () = 3 + 0; 
 [ U11 ] (X0) = 0; 
 [ n__nil ] () = 0; 
 [ U41 ] (X0,X1) = 3*X0 + 0; 
 [ n__u ] () = 0; 
 [ U21 ] (X0,X1) = 1*X0 + 0; 
 [ Marked___ ] (X0,X1) = 2*X0 + 0; 
 [ n__a ] () = 0; 
 [ U72 ] (X0) = 2 + 0; 
 [ o ] () = 3 + 0; 
 ]} 
 ]} 
 ]} 

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