- : 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) -> U22(isList)
[6] U22(tt) -> tt
[7] U31(tt) -> tt
[8] U41(tt) -> U42(isNeList)
[9] U42(tt) -> tt
[10] U51(tt) -> U52(isList)
[11] U52(tt) -> tt
[12] U61(tt) -> tt
[13] U71(tt) -> U72(isPal)
[14] U72(tt) -> tt
[15] U81(tt) -> tt
[16] isList -> U11(isNeList)
[17] isList -> tt
[18] isList -> U21(isList)
[19] isNeList -> U31(isQid)
[20] isNeList -> U41(isList)
[21] isNeList -> U51(isNeList)
[22] isNePal -> U61(isQid)
[23] isNePal -> U71(isQid)
[24] isPal -> U81(isNePal)
[25] isPal -> tt
[26] isQid -> tt
[27] isQid -> tt
[28] isQid -> tt
[29] isQid -> tt
[30] isQid -> tt


Sub problem: 
guided: 

DP termination of:
<Marked___(__(X,Y),Z) , Marked___(X,__(Y,Z))>
<Marked___(__(X,Y),Z) , Marked___(Y,Z)>
<Marked_U21(tt) , Marked_U22(isList)>
<Marked_U21(tt) , Marked_isList>
<Marked_U41(tt) , Marked_U42(isNeList)>
<Marked_U41(tt) , Marked_isNeList>
<Marked_U51(tt) , Marked_U52(isList)>
<Marked_U51(tt) , Marked_isList>
<Marked_U71(tt) , Marked_U72(isPal)>
<Marked_U71(tt) , Marked_isPal>
<Marked_isList , Marked_U11(isNeList)>
<Marked_isList , Marked_isNeList>
<Marked_isList , Marked_U21(isList)>
<Marked_isList , Marked_isList>
<Marked_isNeList , Marked_U31(isQid)>
<Marked_isNeList , Marked_isQid>
<Marked_isNeList , Marked_U41(isList)>
<Marked_isNeList , Marked_isList>
<Marked_isNeList , Marked_U51(isNeList)>
<Marked_isNeList , Marked_isNeList>
<Marked_isNePal , Marked_U61(isQid)>
<Marked_isNePal , Marked_isQid>
<Marked_isNePal , Marked_U71(isQid)>
<Marked_isNePal , Marked_isQid>
<Marked_isPal , Marked_U81(isNePal)>
<Marked_isPal , Marked_isNePal>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 3 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_isNeList> --> <Marked_isNeList , Marked_isNeList>
  <Marked_isNeList , Marked_isNeList> 
     --> <Marked_isNeList , Marked_U51(isNeList)>
  <Marked_isNeList , Marked_isNeList> --> <Marked_isNeList , Marked_isList>
  <Marked_isNeList , Marked_isNeList> 
     --> <Marked_isNeList , Marked_U41(isList)>
  <Marked_isNeList , Marked_U51(isNeList)> --> <Marked_U51(tt) , Marked_isList>
  <Marked_isNeList , Marked_isList> --> <Marked_isList , Marked_isList>
  <Marked_isNeList , Marked_isList> --> <Marked_isList , Marked_U21(isList)>
  <Marked_isNeList , Marked_isList> --> <Marked_isList , Marked_isNeList>
  <Marked_isNeList , Marked_U41(isList)> --> <Marked_U41(tt) , Marked_isNeList>
  <Marked_isList , Marked_isList> --> <Marked_isList , Marked_isList>
  <Marked_isList , Marked_isList> --> <Marked_isList , Marked_U21(isList)>
  <Marked_isList , Marked_isList> --> <Marked_isList , Marked_isNeList>
  <Marked_isList , Marked_U21(isList)> --> <Marked_U21(tt) , Marked_isList>
  <Marked_isList , Marked_isNeList> --> <Marked_isNeList , Marked_isNeList>
  <Marked_isList , Marked_isNeList> 
     --> <Marked_isNeList , Marked_U51(isNeList)>
  <Marked_isList , Marked_isNeList> --> <Marked_isNeList , Marked_isList>
  <Marked_isList , Marked_isNeList> --> <Marked_isNeList , Marked_U41(isList)>
  <Marked_U51(tt) , Marked_isList> --> <Marked_isList , Marked_isList>
  <Marked_U51(tt) , Marked_isList> --> <Marked_isList , Marked_U21(isList)>
  <Marked_U51(tt) , Marked_isList> --> <Marked_isList , Marked_isNeList>
  <Marked_U41(tt) , Marked_isNeList> --> <Marked_isNeList , Marked_isNeList>
  <Marked_U41(tt) , Marked_isNeList> 
     --> <Marked_isNeList , Marked_U51(isNeList)>
  <Marked_U41(tt) , Marked_isNeList> --> <Marked_isNeList , Marked_isList>
  <Marked_U41(tt) , Marked_isNeList> --> <Marked_isNeList , Marked_U41(isList)>
  <Marked_U21(tt) , Marked_isList> --> <Marked_isList , Marked_isList>
  <Marked_U21(tt) , Marked_isList> --> <Marked_isList , Marked_U21(isList)>
  <Marked_U21(tt) , Marked_isList> --> <Marked_isList , Marked_isNeList>
}

{  <Marked_isPal , Marked_isNePal> --> <Marked_isNePal , Marked_U71(isQid)>
  <Marked_isNePal , Marked_U71(isQid)> --> <Marked_U71(tt) , Marked_isPal>
  <Marked_U71(tt) , Marked_isPal> --> <Marked_isPal , Marked_isNePal>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  __(__(X,Y),Z) >= __(X,__(Y,Z)) ;
  __(nil,X) >= X ;
  __(X,nil) >= X ;
  U11(tt) >= tt ;
  U22(tt) >= tt ;
  isList >= tt ;
  isList >= U11(isNeList) ;
  isList >= U21(isList) ;
  U21(tt) >= U22(isList) ;
  U31(tt) >= tt ;
  U42(tt) >= tt ;
  isNeList >= U31(isQid) ;
  isNeList >= U41(isList) ;
  isNeList >= U51(isNeList) ;
  U41(tt) >= U42(isNeList) ;
  U52(tt) >= tt ;
  U51(tt) >= U52(isList) ;
  U61(tt) >= tt ;
  U72(tt) >= tt ;
  isPal >= tt ;
  isPal >= U81(isNePal) ;
  U71(tt) >= U72(isPal) ;
  U81(tt) >= tt ;
  isQid >= tt ;
  isNePal >= U61(isQid) ;
  isNePal >= U71(isQid) ;
  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: U11(tt) >= tt
constraint: U22(tt) >= tt
constraint: isList >= tt
constraint: isList >= U11(isNeList)
constraint: isList >= U21(isList)
constraint: U21(tt) >= U22(isList)
constraint: U31(tt) >= tt
constraint: U42(tt) >= tt
constraint: isNeList >= U31(isQid)
constraint: isNeList >= U41(isList)
constraint: isNeList >= U51(isNeList)
constraint: U41(tt) >= U42(isNeList)
constraint: U52(tt) >= tt
constraint: U51(tt) >= U52(isList)
constraint: U61(tt) >= tt
constraint: U72(tt) >= tt
constraint: isPal >= tt
constraint: isPal >= U81(isNePal)
constraint: U71(tt) >= U72(isPal)
constraint: U81(tt) >= tt
constraint: isQid >= tt
constraint: isNePal >= U61(isQid)
constraint: isNePal >= U71(isQid)
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 ;
  U11(tt) >= tt ;
  U22(tt) >= tt ;
  isList >= tt ;
  isList >= U11(isNeList) ;
  isList >= U21(isList) ;
  U21(tt) >= U22(isList) ;
  U31(tt) >= tt ;
  U42(tt) >= tt ;
  isNeList >= U31(isQid) ;
  isNeList >= U41(isList) ;
  isNeList >= U51(isNeList) ;
  U41(tt) >= U42(isNeList) ;
  U52(tt) >= tt ;
  U51(tt) >= U52(isList) ;
  U61(tt) >= tt ;
  U72(tt) >= tt ;
  isPal >= tt ;
  isPal >= U81(isNePal) ;
  U71(tt) >= U72(isPal) ;
  U81(tt) >= tt ;
  isQid >= tt ;
  isNePal >= U61(isQid) ;
  isNePal >= U71(isQid) ;
  Marked_isNeList >= Marked_isNeList ;
  Marked_isNeList >= Marked_U51(isNeList) ;
  Marked_isNeList >= Marked_U41(isList) ;
  Marked_isNeList >= Marked_isList ;
  Marked_U51(tt) >= Marked_isList ;
  Marked_U41(tt) >= Marked_isNeList ;
  Marked_isList >= Marked_isNeList ;
  Marked_isList >= Marked_isList ;
  Marked_isList >= Marked_U21(isList) ;
  Marked_U21(tt) >= Marked_isList ;
 }
 + Disjunctions:{ 
{
  Marked_isNeList > Marked_isNeList ;
 }
{
  Marked_isNeList > Marked_U51(isNeList) ;
 }
{
  Marked_isNeList > Marked_U41(isList) ;
 }
{
  Marked_isNeList > Marked_isList ;
 }
{
  Marked_U51(tt) > Marked_isList ;
 }
{
  Marked_U41(tt) > Marked_isNeList ;
 }
{
  Marked_isList > Marked_isNeList ;
 }
{
  Marked_isList > Marked_isList ;
 }
{
  Marked_isList > Marked_U21(isList) ;
 }
{
  Marked_U21(tt) > Marked_isList ;
 }
 } 
=== 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 ===
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 25.501298 seconds (real time)
Cime Exit Status: 0