- : 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) -> U12(isPalListKind)
[5] U12(tt) -> U13(isNeList)
[6] U13(tt) -> tt
[7] U21(tt) -> U22(isPalListKind)
[8] U22(tt) -> U23(isPalListKind)
[9] U23(tt) -> U24(isPalListKind)
[10] U24(tt) -> U25(isList)
[11] U25(tt) -> U26(isList)
[12] U26(tt) -> tt
[13] U31(tt) -> U32(isPalListKind)
[14] U32(tt) -> U33(isQid)
[15] U33(tt) -> tt
[16] U41(tt) -> U42(isPalListKind)
[17] U42(tt) -> U43(isPalListKind)
[18] U43(tt) -> U44(isPalListKind)
[19] U44(tt) -> U45(isList)
[20] U45(tt) -> U46(isNeList)
[21] U46(tt) -> tt
[22] U51(tt) -> U52(isPalListKind)
[23] U52(tt) -> U53(isPalListKind)
[24] U53(tt) -> U54(isPalListKind)
[25] U54(tt) -> U55(isNeList)
[26] U55(tt) -> U56(isList)
[27] U56(tt) -> tt
[28] U61(tt) -> U62(isPalListKind)
[29] U62(tt) -> U63(isQid)
[30] U63(tt) -> tt
[31] U71(tt) -> U72(isPalListKind)
[32] U72(tt) -> U73(isPal)
[33] U73(tt) -> U74(isPalListKind)
[34] U74(tt) -> tt
[35] U81(tt) -> U82(isPalListKind)
[36] U82(tt) -> U83(isNePal)
[37] U83(tt) -> tt
[38] U91(tt) -> U92(isPalListKind)
[39] U92(tt) -> tt
[40] isList -> U11(isPalListKind)
[41] isList -> tt
[42] isList -> U21(isPalListKind)
[43] isNeList -> U31(isPalListKind)
[44] isNeList -> U41(isPalListKind)
[45] isNeList -> U51(isPalListKind)
[46] isNePal -> U61(isPalListKind)
[47] isNePal -> U71(isQid)
[48] isPal -> U81(isPalListKind)
[49] isPal -> tt
[50] isPalListKind -> tt
[51] isPalListKind -> tt
[52] isPalListKind -> tt
[53] isPalListKind -> tt
[54] isPalListKind -> tt
[55] isPalListKind -> tt
[56] isPalListKind -> U91(isPalListKind)
[57] isQid -> tt
[58] isQid -> tt
[59] isQid -> tt
[60] isQid -> tt
[61] isQid -> tt


Sub problem: 
guided: 

DP termination of:
<Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))>
<Marked___(__(X,Y),Z) , Marked___(Y,Z)>
<Marked_U11(tt) , Marked_U12(isPalListKind)>
<Marked_U11(tt) , Marked_isPalListKind>
<Marked_U12(tt) , Marked_U13(isNeList)>
<Marked_U12(tt) , Marked_isNeList>
<Marked_U21(tt) , Marked_U22(isPalListKind)>
<Marked_U21(tt) , Marked_isPalListKind>
<Marked_U22(tt) , Marked_U23(isPalListKind)>
<Marked_U22(tt) , Marked_isPalListKind>
<Marked_U23(tt) , Marked_U24(isPalListKind)>
<Marked_U23(tt) , Marked_isPalListKind>
<Marked_U24(tt) , Marked_U25(isList)>
<Marked_U24(tt) , Marked_isList>
<Marked_U25(tt) , Marked_U26(isList)>
<Marked_U25(tt) , Marked_isList>
<Marked_U31(tt) , Marked_U32(isPalListKind)>
<Marked_U31(tt) , Marked_isPalListKind>
<Marked_U32(tt) , Marked_U33(isQid)>
<Marked_U32(tt) , Marked_isQid>
<Marked_U41(tt) , Marked_U42(isPalListKind)>
<Marked_U41(tt) , Marked_isPalListKind>
<Marked_U42(tt) , Marked_U43(isPalListKind)>
<Marked_U42(tt) , Marked_isPalListKind>
<Marked_U43(tt) , Marked_U44(isPalListKind)>
<Marked_U43(tt) , Marked_isPalListKind>
<Marked_U44(tt) , Marked_U45(isList)>
<Marked_U44(tt) , Marked_isList>
<Marked_U45(tt) , Marked_U46(isNeList)>
<Marked_U45(tt) , Marked_isNeList>
<Marked_U51(tt) , Marked_U52(isPalListKind)>
<Marked_U51(tt) , Marked_isPalListKind>
<Marked_U52(tt) , Marked_U53(isPalListKind)>
<Marked_U52(tt) , Marked_isPalListKind>
<Marked_U53(tt) , Marked_U54(isPalListKind)>
<Marked_U53(tt) , Marked_isPalListKind>
<Marked_U54(tt) , Marked_U55(isNeList)>
<Marked_U54(tt) , Marked_isNeList>
<Marked_U55(tt) , Marked_U56(isList)>
<Marked_U55(tt) , Marked_isList>
<Marked_U61(tt) , Marked_U62(isPalListKind)>
<Marked_U61(tt) , Marked_isPalListKind>
<Marked_U62(tt) , Marked_U63(isQid)>
<Marked_U62(tt) , Marked_isQid>
<Marked_U71(tt) , Marked_U72(isPalListKind)>
<Marked_U71(tt) , Marked_isPalListKind>
<Marked_U72(tt) , Marked_U73(isPal)>
<Marked_U72(tt) , Marked_isPal>
<Marked_U73(tt) , Marked_U74(isPalListKind)>
<Marked_U73(tt) , Marked_isPalListKind>
<Marked_U81(tt) , Marked_U82(isPalListKind)>
<Marked_U81(tt) , Marked_isPalListKind>
<Marked_U82(tt) , Marked_U83(isNePal)>
<Marked_U82(tt) , Marked_isNePal>
<Marked_U91(tt) , Marked_U92(isPalListKind)>
<Marked_U91(tt) , Marked_isPalListKind>
<Marked_isList , Marked_U11(isPalListKind)>
<Marked_isList , Marked_isPalListKind>
<Marked_isList , Marked_U21(isPalListKind)>
<Marked_isList , Marked_isPalListKind>
<Marked_isNeList , Marked_U31(isPalListKind)>
<Marked_isNeList , Marked_isPalListKind>
<Marked_isNeList , Marked_U41(isPalListKind)>
<Marked_isNeList , Marked_isPalListKind>
<Marked_isNeList , Marked_U51(isPalListKind)>
<Marked_isNeList , Marked_isPalListKind>
<Marked_isNePal , Marked_U61(isPalListKind)>
<Marked_isNePal , Marked_isPalListKind>
<Marked_isNePal , Marked_U71(isQid)>
<Marked_isNePal , Marked_isQid>
<Marked_isPal , Marked_U81(isPalListKind)>
<Marked_isPal , Marked_isPalListKind>
<Marked_isPalListKind , Marked_U91(isPalListKind)>
<Marked_isPalListKind , Marked_isPalListKind>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 4 components:

{  <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))>
}

{  <Marked_isNeList , Marked_U51(isPalListKind)> 
      --> <Marked_U51(tt) , Marked_U52(isPalListKind)>
  <Marked_isNeList , Marked_U41(isPalListKind)> 
     --> <Marked_U41(tt) , Marked_U42(isPalListKind)>
  <Marked_isList , Marked_U21(isPalListKind)> 
     --> <Marked_U21(tt) , Marked_U22(isPalListKind)>
  <Marked_isList , Marked_U11(isPalListKind)> 
     --> <Marked_U11(tt) , Marked_U12(isPalListKind)>
  <Marked_U55(tt) , Marked_isList> 
     --> <Marked_isList , Marked_U21(isPalListKind)>
  <Marked_U55(tt) , Marked_isList> 
     --> <Marked_isList , Marked_U11(isPalListKind)>
  <Marked_U54(tt) , Marked_isNeList> 
     --> <Marked_isNeList , Marked_U51(isPalListKind)>
  <Marked_U54(tt) , Marked_isNeList> 
     --> <Marked_isNeList , Marked_U41(isPalListKind)>
  <Marked_U54(tt) , Marked_U55(isNeList)> --> <Marked_U55(tt) , Marked_isList>
  <Marked_U53(tt) , Marked_U54(isPalListKind)> 
     --> <Marked_U54(tt) , Marked_isNeList>
  <Marked_U53(tt) , Marked_U54(isPalListKind)> 
     --> <Marked_U54(tt) , Marked_U55(isNeList)>
  <Marked_U52(tt) , Marked_U53(isPalListKind)> 
     --> <Marked_U53(tt) , Marked_U54(isPalListKind)>
  <Marked_U51(tt) , Marked_U52(isPalListKind)> 
     --> <Marked_U52(tt) , Marked_U53(isPalListKind)>
  <Marked_U45(tt) , Marked_isNeList> 
     --> <Marked_isNeList , Marked_U51(isPalListKind)>
  <Marked_U45(tt) , Marked_isNeList> 
     --> <Marked_isNeList , Marked_U41(isPalListKind)>
  <Marked_U44(tt) , Marked_isList> 
     --> <Marked_isList , Marked_U21(isPalListKind)>
  <Marked_U44(tt) , Marked_isList> 
     --> <Marked_isList , Marked_U11(isPalListKind)>
  <Marked_U44(tt) , Marked_U45(isList)> --> <Marked_U45(tt) , Marked_isNeList>
  <Marked_U43(tt) , Marked_U44(isPalListKind)> 
     --> <Marked_U44(tt) , Marked_isList>
  <Marked_U43(tt) , Marked_U44(isPalListKind)> 
     --> <Marked_U44(tt) , Marked_U45(isList)>
  <Marked_U42(tt) , Marked_U43(isPalListKind)> 
     --> <Marked_U43(tt) , Marked_U44(isPalListKind)>
  <Marked_U41(tt) , Marked_U42(isPalListKind)> 
     --> <Marked_U42(tt) , Marked_U43(isPalListKind)>
  <Marked_U25(tt) , Marked_isList> 
     --> <Marked_isList , Marked_U21(isPalListKind)>
  <Marked_U25(tt) , Marked_isList> 
     --> <Marked_isList , Marked_U11(isPalListKind)>
  <Marked_U24(tt) , Marked_isList> 
     --> <Marked_isList , Marked_U21(isPalListKind)>
  <Marked_U24(tt) , Marked_isList> 
     --> <Marked_isList , Marked_U11(isPalListKind)>
  <Marked_U24(tt) , Marked_U25(isList)> --> <Marked_U25(tt) , Marked_isList>
  <Marked_U23(tt) , Marked_U24(isPalListKind)> 
     --> <Marked_U24(tt) , Marked_isList>
  <Marked_U23(tt) , Marked_U24(isPalListKind)> 
     --> <Marked_U24(tt) , Marked_U25(isList)>
  <Marked_U22(tt) , Marked_U23(isPalListKind)> 
     --> <Marked_U23(tt) , Marked_U24(isPalListKind)>
  <Marked_U21(tt) , Marked_U22(isPalListKind)> 
     --> <Marked_U22(tt) , Marked_U23(isPalListKind)>
  <Marked_U12(tt) , Marked_isNeList> 
     --> <Marked_isNeList , Marked_U51(isPalListKind)>
  <Marked_U12(tt) , Marked_isNeList> 
     --> <Marked_isNeList , Marked_U41(isPalListKind)>
  <Marked_U11(tt) , Marked_U12(isPalListKind)> 
     --> <Marked_U12(tt) , Marked_isNeList>
}

{  <Marked_isPal , Marked_U81(isPalListKind)> 
      --> <Marked_U81(tt) , Marked_U82(isPalListKind)>
  <Marked_isNePal , Marked_U71(isQid)> 
     --> <Marked_U71(tt) , Marked_U72(isPalListKind)>
  <Marked_U82(tt) , Marked_isNePal> --> <Marked_isNePal , Marked_U71(isQid)>
  <Marked_U81(tt) , Marked_U82(isPalListKind)> 
     --> <Marked_U82(tt) , Marked_isNePal>
  <Marked_U72(tt) , Marked_isPal> 
     --> <Marked_isPal , Marked_U81(isPalListKind)>
  <Marked_U71(tt) , Marked_U72(isPalListKind)> 
     --> <Marked_U72(tt) , Marked_isPal>
}

{  <Marked_isPalListKind , Marked_isPalListKind> 
      --> <Marked_isPalListKind , Marked_isPalListKind>
  <Marked_isPalListKind , Marked_isPalListKind> 
     --> <Marked_isPalListKind , Marked_U91(isPalListKind)>
  <Marked_isPalListKind , Marked_U91(isPalListKind)> 
     --> <Marked_U91(tt) , Marked_isPalListKind>
  <Marked_U91(tt) , Marked_isPalListKind> 
     --> <Marked_isPalListKind , Marked_isPalListKind>
  <Marked_U91(tt) , Marked_isPalListKind> 
     --> <Marked_isPalListKind , Marked_U91(isPalListKind)>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  __(__(X,Y),Z) >= __(X,__(Y,Z)) ;
  __(nil,X) >= X ;
  __(X,nil) >= X ;
  U12(tt) >= U13(isNeList) ;
  isPalListKind >= tt ;
  isPalListKind >= U91(isPalListKind) ;
  U11(tt) >= U12(isPalListKind) ;
  U13(tt) >= tt ;
  isNeList >= U31(isPalListKind) ;
  isNeList >= U41(isPalListKind) ;
  isNeList >= U51(isPalListKind) ;
  U22(tt) >= U23(isPalListKind) ;
  U21(tt) >= U22(isPalListKind) ;
  U23(tt) >= U24(isPalListKind) ;
  U24(tt) >= U25(isList) ;
  U25(tt) >= U26(isList) ;
  isList >= U11(isPalListKind) ;
  isList >= tt ;
  isList >= U21(isPalListKind) ;
  U26(tt) >= tt ;
  U32(tt) >= U33(isQid) ;
  U31(tt) >= U32(isPalListKind) ;
  U33(tt) >= tt ;
  isQid >= tt ;
  U42(tt) >= U43(isPalListKind) ;
  U41(tt) >= U42(isPalListKind) ;
  U43(tt) >= U44(isPalListKind) ;
  U44(tt) >= U45(isList) ;
  U45(tt) >= U46(isNeList) ;
  U46(tt) >= tt ;
  U52(tt) >= U53(isPalListKind) ;
  U51(tt) >= U52(isPalListKind) ;
  U53(tt) >= U54(isPalListKind) ;
  U54(tt) >= U55(isNeList) ;
  U55(tt) >= U56(isList) ;
  U56(tt) >= tt ;
  U62(tt) >= U63(isQid) ;
  U61(tt) >= U62(isPalListKind) ;
  U63(tt) >= tt ;
  U72(tt) >= U73(isPal) ;
  U71(tt) >= U72(isPalListKind) ;
  U73(tt) >= U74(isPalListKind) ;
  isPal >= tt ;
  isPal >= U81(isPalListKind) ;
  U74(tt) >= tt ;
  U82(tt) >= U83(isNePal) ;
  U81(tt) >= U82(isPalListKind) ;
  U83(tt) >= tt ;
  isNePal >= U61(isPalListKind) ;
  isNePal >= U71(isQid) ;
  U92(tt) >= tt ;
  U91(tt) >= U92(isPalListKind) ;
  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: U12(tt) >= U13(isNeList)
constraint: isPalListKind >= tt
constraint: isPalListKind >= U91(isPalListKind)
constraint: U11(tt) >= U12(isPalListKind)
constraint: U13(tt) >= tt
constraint: isNeList >= U31(isPalListKind)
constraint: isNeList >= U41(isPalListKind)
constraint: isNeList >= U51(isPalListKind)
constraint: U22(tt) >= U23(isPalListKind)
constraint: U21(tt) >= U22(isPalListKind)
constraint: U23(tt) >= U24(isPalListKind)
constraint: U24(tt) >= U25(isList)
constraint: U25(tt) >= U26(isList)
constraint: isList >= U11(isPalListKind)
constraint: isList >= tt
constraint: isList >= U21(isPalListKind)
constraint: U26(tt) >= tt
constraint: U32(tt) >= U33(isQid)
constraint: U31(tt) >= U32(isPalListKind)
constraint: U33(tt) >= tt
constraint: isQid >= tt
constraint: U42(tt) >= U43(isPalListKind)
constraint: U41(tt) >= U42(isPalListKind)
constraint: U43(tt) >= U44(isPalListKind)
constraint: U44(tt) >= U45(isList)
constraint: U45(tt) >= U46(isNeList)
constraint: U46(tt) >= tt
constraint: U52(tt) >= U53(isPalListKind)
constraint: U51(tt) >= U52(isPalListKind)
constraint: U53(tt) >= U54(isPalListKind)
constraint: U54(tt) >= U55(isNeList)
constraint: U55(tt) >= U56(isList)
constraint: U56(tt) >= tt
constraint: U62(tt) >= U63(isQid)
constraint: U61(tt) >= U62(isPalListKind)
constraint: U63(tt) >= tt
constraint: U72(tt) >= U73(isPal)
constraint: U71(tt) >= U72(isPalListKind)
constraint: U73(tt) >= U74(isPalListKind)
constraint: isPal >= tt
constraint: isPal >= U81(isPalListKind)
constraint: U74(tt) >= tt
constraint: U82(tt) >= U83(isNePal)
constraint: U81(tt) >= U82(isPalListKind)
constraint: U83(tt) >= tt
constraint: isNePal >= U61(isPalListKind)
constraint: isNePal >= U71(isQid)
constraint: U92(tt) >= tt
constraint: U91(tt) >= U92(isPalListKind)
constraint: Marked___(__(X,Y),Z) >= Marked___(X,__(Y,Z))
constraint: Marked___(__(X,Y),Z) >= Marked___(Y,Z)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  __(__(X,Y),Z) >= __(X,__(Y,Z)) ;
  __(nil,X) >= X ;
  __(X,nil) >= X ;
  U12(tt) >= U13(isNeList) ;
  isPalListKind >= tt ;
  isPalListKind >= U91(isPalListKind) ;
  U11(tt) >= U12(isPalListKind) ;
  U13(tt) >= tt ;
  isNeList >= U31(isPalListKind) ;
  isNeList >= U41(isPalListKind) ;
  isNeList >= U51(isPalListKind) ;
  U22(tt) >= U23(isPalListKind) ;
  U21(tt) >= U22(isPalListKind) ;
  U23(tt) >= U24(isPalListKind) ;
  U24(tt) >= U25(isList) ;
  U25(tt) >= U26(isList) ;
  isList >= U11(isPalListKind) ;
  isList >= tt ;
  isList >= U21(isPalListKind) ;
  U26(tt) >= tt ;
  U32(tt) >= U33(isQid) ;
  U31(tt) >= U32(isPalListKind) ;
  U33(tt) >= tt ;
  isQid >= tt ;
  U42(tt) >= U43(isPalListKind) ;
  U41(tt) >= U42(isPalListKind) ;
  U43(tt) >= U44(isPalListKind) ;
  U44(tt) >= U45(isList) ;
  U45(tt) >= U46(isNeList) ;
  U46(tt) >= tt ;
  U52(tt) >= U53(isPalListKind) ;
  U51(tt) >= U52(isPalListKind) ;
  U53(tt) >= U54(isPalListKind) ;
  U54(tt) >= U55(isNeList) ;
  U55(tt) >= U56(isList) ;
  U56(tt) >= tt ;
  U62(tt) >= U63(isQid) ;
  U61(tt) >= U62(isPalListKind) ;
  U63(tt) >= tt ;
  U72(tt) >= U73(isPal) ;
  U71(tt) >= U72(isPalListKind) ;
  U73(tt) >= U74(isPalListKind) ;
  isPal >= tt ;
  isPal >= U81(isPalListKind) ;
  U74(tt) >= tt ;
  U82(tt) >= U83(isNePal) ;
  U81(tt) >= U82(isPalListKind) ;
  U83(tt) >= tt ;
  isNePal >= U61(isPalListKind) ;
  isNePal >= U71(isQid) ;
  U92(tt) >= tt ;
  U91(tt) >= U92(isPalListKind) ;
  Marked_isNeList >= Marked_U51(isPalListKind) ;
  Marked_isNeList >= Marked_U41(isPalListKind) ;
  Marked_U51(tt) >= Marked_U52(isPalListKind) ;
  Marked_U41(tt) >= Marked_U42(isPalListKind) ;
  Marked_isList >= Marked_U21(isPalListKind) ;
  Marked_isList >= Marked_U11(isPalListKind) ;
  Marked_U21(tt) >= Marked_U22(isPalListKind) ;
  Marked_U11(tt) >= Marked_U12(isPalListKind) ;
  Marked_U55(tt) >= Marked_isList ;
  Marked_U54(tt) >= Marked_isNeList ;
  Marked_U54(tt) >= Marked_U55(isNeList) ;
  Marked_U53(tt) >= Marked_U54(isPalListKind) ;
  Marked_U52(tt) >= Marked_U53(isPalListKind) ;
  Marked_U45(tt) >= Marked_isNeList ;
  Marked_U44(tt) >= Marked_isList ;
  Marked_U44(tt) >= Marked_U45(isList) ;
  Marked_U43(tt) >= Marked_U44(isPalListKind) ;
  Marked_U42(tt) >= Marked_U43(isPalListKind) ;
  Marked_U25(tt) >= Marked_isList ;
  Marked_U24(tt) >= Marked_isList ;
  Marked_U24(tt) >= Marked_U25(isList) ;
  Marked_U23(tt) >= Marked_U24(isPalListKind) ;
  Marked_U22(tt) >= Marked_U23(isPalListKind) ;
  Marked_U12(tt) >= Marked_isNeList ;
 }
 + Disjunctions:{ 
{
  Marked_isNeList > Marked_U51(isPalListKind) ;
 }
{
  Marked_isNeList > Marked_U41(isPalListKind) ;
 }
{
  Marked_U51(tt) > Marked_U52(isPalListKind) ;
 }
{
  Marked_U41(tt) > Marked_U42(isPalListKind) ;
 }
{
  Marked_isList > Marked_U21(isPalListKind) ;
 }
{
  Marked_isList > Marked_U11(isPalListKind) ;
 }
{
  Marked_U21(tt) > Marked_U22(isPalListKind) ;
 }
{
  Marked_U11(tt) > Marked_U12(isPalListKind) ;
 }
{
  Marked_U55(tt) > Marked_isList ;
 }
{
  Marked_U54(tt) > Marked_isNeList ;
 }
{
  Marked_U54(tt) > Marked_U55(isNeList) ;
 }
{
  Marked_U53(tt) > Marked_U54(isPalListKind) ;
 }
{
  Marked_U52(tt) > Marked_U53(isPalListKind) ;
 }
{
  Marked_U45(tt) > Marked_isNeList ;
 }
{
  Marked_U44(tt) > Marked_isList ;
 }
{
  Marked_U44(tt) > Marked_U45(isList) ;
 }
{
  Marked_U43(tt) > Marked_U44(isPalListKind) ;
 }
{
  Marked_U42(tt) > Marked_U43(isPalListKind) ;
 }
{
  Marked_U25(tt) > Marked_isList ;
 }
{
  Marked_U24(tt) > Marked_isList ;
 }
{
  Marked_U24(tt) > Marked_U25(isList) ;
 }
{
  Marked_U23(tt) > Marked_U24(isPalListKind) ;
 }
{
  Marked_U22(tt) > Marked_U23(isPalListKind) ;
 }
{
  Marked_U12(tt) > Marked_isNeList ;
 }
 } 
=== 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 ===
Time out for these parameters.
=== 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 26.670573 seconds (real time)
Cime Exit Status: 0