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

TRS termination of:
[1] active(dbl(0)) -> mark(0)
[2] active(dbl(s(X))) -> mark(s(s(dbl(X))))
[3] active(dbls(nil)) -> mark(nil)
[4] active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y)))
[5] active(sel(0,cons(X,Y))) -> mark(X)
[6] active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z))
[7] active(indx(nil,X)) -> mark(nil)
[8] active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z)))
[9] active(from(X)) -> mark(cons(X,from(s(X))))
[10] mark(dbl(X)) -> active(dbl(mark(X)))
[11] mark(0) -> active(0)
[12] mark(s(X)) -> active(s(X))
[13] mark(dbls(X)) -> active(dbls(mark(X)))
[14] mark(nil) -> active(nil)
[15] mark(cons(X1,X2)) -> active(cons(X1,X2))
[16] mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
[17] mark(indx(X1,X2)) -> active(indx(mark(X1),X2))
[18] mark(from(X)) -> active(from(X))
[19] dbl(mark(X)) -> dbl(X)
[20] dbl(active(X)) -> dbl(X)
[21] s(mark(X)) -> s(X)
[22] s(active(X)) -> s(X)
[23] dbls(mark(X)) -> dbls(X)
[24] dbls(active(X)) -> dbls(X)
[25] cons(mark(X1),X2) -> cons(X1,X2)
[26] cons(X1,mark(X2)) -> cons(X1,X2)
[27] cons(active(X1),X2) -> cons(X1,X2)
[28] cons(X1,active(X2)) -> cons(X1,X2)
[29] sel(mark(X1),X2) -> sel(X1,X2)
[30] sel(X1,mark(X2)) -> sel(X1,X2)
[31] sel(active(X1),X2) -> sel(X1,X2)
[32] sel(X1,active(X2)) -> sel(X1,X2)
[33] indx(mark(X1),X2) -> indx(X1,X2)
[34] indx(X1,mark(X2)) -> indx(X1,X2)
[35] indx(active(X1),X2) -> indx(X1,X2)
[36] indx(X1,active(X2)) -> indx(X1,X2)
[37] from(mark(X)) -> from(X)
[38] from(active(X)) -> from(X)


Sub problem: 
guided: 

DP termination of:
<Marked_active(dbl(0)) , Marked_mark(0)>
<Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))>
<Marked_active(dbl(s(X))) , Marked_s(s(dbl(X)))>
<Marked_active(dbl(s(X))) , Marked_s(dbl(X))>
<Marked_active(dbl(s(X))) , Marked_dbl(X)>
<Marked_active(dbls(nil)) , Marked_mark(nil)>
<Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))>
<Marked_active(dbls(cons(X,Y))) , Marked_cons(dbl(X),dbls(Y))>
<Marked_active(dbls(cons(X,Y))) , Marked_dbl(X)>
<Marked_active(dbls(cons(X,Y))) , Marked_dbls(Y)>
<Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)>
<Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))>
<Marked_active(sel(s(X),cons(Y,Z))) , Marked_sel(X,Z)>
<Marked_active(indx(nil,X)) , Marked_mark(nil)>
<Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))>
<Marked_active(indx(cons(X,Y),Z)) , Marked_cons(sel(X,Z),indx(Y,Z))>
<Marked_active(indx(cons(X,Y),Z)) , Marked_sel(X,Z)>
<Marked_active(indx(cons(X,Y),Z)) , Marked_indx(Y,Z)>
<Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))>
<Marked_active(from(X)) , Marked_cons(X,from(s(X)))>
<Marked_active(from(X)) , Marked_from(s(X))>
<Marked_active(from(X)) , Marked_s(X)>
<Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
<Marked_mark(dbl(X)) , Marked_dbl(mark(X))>
<Marked_mark(dbl(X)) , Marked_mark(X)>
<Marked_mark(0) , Marked_active(0)>
<Marked_mark(s(X)) , Marked_active(s(X))>
<Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
<Marked_mark(dbls(X)) , Marked_dbls(mark(X))>
<Marked_mark(dbls(X)) , Marked_mark(X)>
<Marked_mark(nil) , Marked_active(nil)>
<Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))>
<Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
<Marked_mark(sel(X1,X2)) , Marked_sel(mark(X1),mark(X2))>
<Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
<Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
<Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
<Marked_mark(indx(X1,X2)) , Marked_indx(mark(X1),X2)>
<Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
<Marked_mark(from(X)) , Marked_active(from(X))>
<Marked_dbl(mark(X)) , Marked_dbl(X)>
<Marked_dbl(active(X)) , Marked_dbl(X)>
<Marked_s(mark(X)) , Marked_s(X)>
<Marked_s(active(X)) , Marked_s(X)>
<Marked_dbls(mark(X)) , Marked_dbls(X)>
<Marked_dbls(active(X)) , Marked_dbls(X)>
<Marked_cons(mark(X1),X2) , Marked_cons(X1,X2)>
<Marked_cons(X1,mark(X2)) , Marked_cons(X1,X2)>
<Marked_cons(active(X1),X2) , Marked_cons(X1,X2)>
<Marked_cons(X1,active(X2)) , Marked_cons(X1,X2)>
<Marked_sel(mark(X1),X2) , Marked_sel(X1,X2)>
<Marked_sel(X1,mark(X2)) , Marked_sel(X1,X2)>
<Marked_sel(active(X1),X2) , Marked_sel(X1,X2)>
<Marked_sel(X1,active(X2)) , Marked_sel(X1,X2)>
<Marked_indx(mark(X1),X2) , Marked_indx(X1,X2)>
<Marked_indx(X1,mark(X2)) , Marked_indx(X1,X2)>
<Marked_indx(active(X1),X2) , Marked_indx(X1,X2)>
<Marked_indx(X1,active(X2)) , Marked_indx(X1,X2)>
<Marked_from(mark(X)) , Marked_from(X)>
<Marked_from(active(X)) , Marked_from(X)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 8 components:

{  <Marked_mark(from(X)) , Marked_active(from(X))> 
      --> <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))>
  <Marked_mark(from(X)) , Marked_active(from(X))> 
     --> <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),
                                                          indx(Y,Z)))>
  <Marked_mark(from(X)) , Marked_active(from(X))> 
     --> <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))>
  <Marked_mark(from(X)) , Marked_active(from(X))> 
     --> <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)>
  <Marked_mark(from(X)) , Marked_active(from(X))> 
     --> <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))>
  <Marked_mark(from(X)) , Marked_active(from(X))> 
     --> <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(s(X)) , Marked_active(s(X))>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))> 
     --> <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))>
  <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))> 
     --> <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),
                                                          indx(Y,Z)))>
  <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))> 
     --> <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))>
  <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))> 
     --> <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)>
  <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))> 
     --> <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))>
  <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))> 
     --> <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(s(X)) , Marked_active(s(X))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(s(X)) , Marked_active(s(X))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),
                                                          indx(Y,Z)))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))>
  <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))> 
     --> <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))>
  <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))> 
     --> <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),
                                                          indx(Y,Z)))>
  <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))> 
     --> <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))>
  <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))> 
     --> <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)>
  <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))> 
     --> <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))>
  <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))> 
     --> <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(s(X)) , Marked_active(s(X))>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))> 
     --> <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))>
  <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))> 
     --> <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),
                                                          indx(Y,Z)))>
  <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))> 
     --> <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))>
  <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))> 
     --> <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)>
  <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))> 
     --> <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))>
  <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))> 
     --> <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))>
  <Marked_mark(s(X)) , Marked_active(s(X))> 
     --> <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))>
  <Marked_mark(s(X)) , Marked_active(s(X))> 
     --> <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),
                                                          indx(Y,Z)))>
  <Marked_mark(s(X)) , Marked_active(s(X))> 
     --> <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))>
  <Marked_mark(s(X)) , Marked_active(s(X))> 
     --> <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)>
  <Marked_mark(s(X)) , Marked_active(s(X))> 
     --> <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))>
  <Marked_mark(s(X)) , Marked_active(s(X))> 
     --> <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(s(X)) , Marked_active(s(X))>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))> 
     --> <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))>
  <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))> 
     --> <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),
                                                          indx(Y,Z)))>
  <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))> 
     --> <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))>
  <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))> 
     --> <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)>
  <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))> 
     --> <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))>
  <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))> 
     --> <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(s(X)) , Marked_active(s(X))>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(s(X)) , Marked_active(s(X))>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(s(X)) , Marked_active(s(X))>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(s(X)) , Marked_active(s(X))>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(s(X)) , Marked_active(s(X))>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(X1,X2))>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(s(X)) , Marked_active(s(X))>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
}

{  <Marked_dbl(active(X)) , Marked_dbl(X)> 
      --> <Marked_dbl(active(X)) , Marked_dbl(X)>
  <Marked_dbl(active(X)) , Marked_dbl(X)> 
     --> <Marked_dbl(mark(X)) , Marked_dbl(X)>
  <Marked_dbl(mark(X)) , Marked_dbl(X)> 
     --> <Marked_dbl(active(X)) , Marked_dbl(X)>
  <Marked_dbl(mark(X)) , Marked_dbl(X)> 
     --> <Marked_dbl(mark(X)) , Marked_dbl(X)>
}

{  <Marked_s(active(X)) , Marked_s(X)> --> <Marked_s(active(X)) , Marked_s(X)>
  <Marked_s(active(X)) , Marked_s(X)> --> <Marked_s(mark(X)) , Marked_s(X)>
  <Marked_s(mark(X)) , Marked_s(X)> --> <Marked_s(active(X)) , Marked_s(X)>
  <Marked_s(mark(X)) , Marked_s(X)> --> <Marked_s(mark(X)) , Marked_s(X)>
}

{  <Marked_dbls(active(X)) , Marked_dbls(X)> 
      --> <Marked_dbls(active(X)) , Marked_dbls(X)>
  <Marked_dbls(active(X)) , Marked_dbls(X)> 
     --> <Marked_dbls(mark(X)) , Marked_dbls(X)>
  <Marked_dbls(mark(X)) , Marked_dbls(X)> 
     --> <Marked_dbls(active(X)) , Marked_dbls(X)>
  <Marked_dbls(mark(X)) , Marked_dbls(X)> 
     --> <Marked_dbls(mark(X)) , Marked_dbls(X)>
}

{  <Marked_cons(X1,active(X2)) , Marked_cons(X1,X2)> 
      --> <Marked_cons(X1,active(X2)) , Marked_cons(X1,X2)>
  <Marked_cons(X1,active(X2)) , Marked_cons(X1,X2)> 
     --> <Marked_cons(active(X1),X2) , Marked_cons(X1,X2)>
  <Marked_cons(X1,active(X2)) , Marked_cons(X1,X2)> 
     --> <Marked_cons(X1,mark(X2)) , Marked_cons(X1,X2)>
  <Marked_cons(X1,active(X2)) , Marked_cons(X1,X2)> 
     --> <Marked_cons(mark(X1),X2) , Marked_cons(X1,X2)>
  <Marked_cons(active(X1),X2) , Marked_cons(X1,X2)> 
     --> <Marked_cons(X1,active(X2)) , Marked_cons(X1,X2)>
  <Marked_cons(active(X1),X2) , Marked_cons(X1,X2)> 
     --> <Marked_cons(active(X1),X2) , Marked_cons(X1,X2)>
  <Marked_cons(active(X1),X2) , Marked_cons(X1,X2)> 
     --> <Marked_cons(X1,mark(X2)) , Marked_cons(X1,X2)>
  <Marked_cons(active(X1),X2) , Marked_cons(X1,X2)> 
     --> <Marked_cons(mark(X1),X2) , Marked_cons(X1,X2)>
  <Marked_cons(X1,mark(X2)) , Marked_cons(X1,X2)> 
     --> <Marked_cons(X1,active(X2)) , Marked_cons(X1,X2)>
  <Marked_cons(X1,mark(X2)) , Marked_cons(X1,X2)> 
     --> <Marked_cons(active(X1),X2) , Marked_cons(X1,X2)>
  <Marked_cons(X1,mark(X2)) , Marked_cons(X1,X2)> 
     --> <Marked_cons(X1,mark(X2)) , Marked_cons(X1,X2)>
  <Marked_cons(X1,mark(X2)) , Marked_cons(X1,X2)> 
     --> <Marked_cons(mark(X1),X2) , Marked_cons(X1,X2)>
  <Marked_cons(mark(X1),X2) , Marked_cons(X1,X2)> 
     --> <Marked_cons(X1,active(X2)) , Marked_cons(X1,X2)>
  <Marked_cons(mark(X1),X2) , Marked_cons(X1,X2)> 
     --> <Marked_cons(active(X1),X2) , Marked_cons(X1,X2)>
  <Marked_cons(mark(X1),X2) , Marked_cons(X1,X2)> 
     --> <Marked_cons(X1,mark(X2)) , Marked_cons(X1,X2)>
  <Marked_cons(mark(X1),X2) , Marked_cons(X1,X2)> 
     --> <Marked_cons(mark(X1),X2) , Marked_cons(X1,X2)>
}

{  <Marked_sel(X1,active(X2)) , Marked_sel(X1,X2)> 
      --> <Marked_sel(X1,active(X2)) , Marked_sel(X1,X2)>
  <Marked_sel(X1,active(X2)) , Marked_sel(X1,X2)> 
     --> <Marked_sel(active(X1),X2) , Marked_sel(X1,X2)>
  <Marked_sel(X1,active(X2)) , Marked_sel(X1,X2)> 
     --> <Marked_sel(X1,mark(X2)) , Marked_sel(X1,X2)>
  <Marked_sel(X1,active(X2)) , Marked_sel(X1,X2)> 
     --> <Marked_sel(mark(X1),X2) , Marked_sel(X1,X2)>
  <Marked_sel(active(X1),X2) , Marked_sel(X1,X2)> 
     --> <Marked_sel(X1,active(X2)) , Marked_sel(X1,X2)>
  <Marked_sel(active(X1),X2) , Marked_sel(X1,X2)> 
     --> <Marked_sel(active(X1),X2) , Marked_sel(X1,X2)>
  <Marked_sel(active(X1),X2) , Marked_sel(X1,X2)> 
     --> <Marked_sel(X1,mark(X2)) , Marked_sel(X1,X2)>
  <Marked_sel(active(X1),X2) , Marked_sel(X1,X2)> 
     --> <Marked_sel(mark(X1),X2) , Marked_sel(X1,X2)>
  <Marked_sel(X1,mark(X2)) , Marked_sel(X1,X2)> 
     --> <Marked_sel(X1,active(X2)) , Marked_sel(X1,X2)>
  <Marked_sel(X1,mark(X2)) , Marked_sel(X1,X2)> 
     --> <Marked_sel(active(X1),X2) , Marked_sel(X1,X2)>
  <Marked_sel(X1,mark(X2)) , Marked_sel(X1,X2)> 
     --> <Marked_sel(X1,mark(X2)) , Marked_sel(X1,X2)>
  <Marked_sel(X1,mark(X2)) , Marked_sel(X1,X2)> 
     --> <Marked_sel(mark(X1),X2) , Marked_sel(X1,X2)>
  <Marked_sel(mark(X1),X2) , Marked_sel(X1,X2)> 
     --> <Marked_sel(X1,active(X2)) , Marked_sel(X1,X2)>
  <Marked_sel(mark(X1),X2) , Marked_sel(X1,X2)> 
     --> <Marked_sel(active(X1),X2) , Marked_sel(X1,X2)>
  <Marked_sel(mark(X1),X2) , Marked_sel(X1,X2)> 
     --> <Marked_sel(X1,mark(X2)) , Marked_sel(X1,X2)>
  <Marked_sel(mark(X1),X2) , Marked_sel(X1,X2)> 
     --> <Marked_sel(mark(X1),X2) , Marked_sel(X1,X2)>
}

{  <Marked_indx(X1,active(X2)) , Marked_indx(X1,X2)> 
      --> <Marked_indx(X1,active(X2)) , Marked_indx(X1,X2)>
  <Marked_indx(X1,active(X2)) , Marked_indx(X1,X2)> 
     --> <Marked_indx(active(X1),X2) , Marked_indx(X1,X2)>
  <Marked_indx(X1,active(X2)) , Marked_indx(X1,X2)> 
     --> <Marked_indx(X1,mark(X2)) , Marked_indx(X1,X2)>
  <Marked_indx(X1,active(X2)) , Marked_indx(X1,X2)> 
     --> <Marked_indx(mark(X1),X2) , Marked_indx(X1,X2)>
  <Marked_indx(active(X1),X2) , Marked_indx(X1,X2)> 
     --> <Marked_indx(X1,active(X2)) , Marked_indx(X1,X2)>
  <Marked_indx(active(X1),X2) , Marked_indx(X1,X2)> 
     --> <Marked_indx(active(X1),X2) , Marked_indx(X1,X2)>
  <Marked_indx(active(X1),X2) , Marked_indx(X1,X2)> 
     --> <Marked_indx(X1,mark(X2)) , Marked_indx(X1,X2)>
  <Marked_indx(active(X1),X2) , Marked_indx(X1,X2)> 
     --> <Marked_indx(mark(X1),X2) , Marked_indx(X1,X2)>
  <Marked_indx(X1,mark(X2)) , Marked_indx(X1,X2)> 
     --> <Marked_indx(X1,active(X2)) , Marked_indx(X1,X2)>
  <Marked_indx(X1,mark(X2)) , Marked_indx(X1,X2)> 
     --> <Marked_indx(active(X1),X2) , Marked_indx(X1,X2)>
  <Marked_indx(X1,mark(X2)) , Marked_indx(X1,X2)> 
     --> <Marked_indx(X1,mark(X2)) , Marked_indx(X1,X2)>
  <Marked_indx(X1,mark(X2)) , Marked_indx(X1,X2)> 
     --> <Marked_indx(mark(X1),X2) , Marked_indx(X1,X2)>
  <Marked_indx(mark(X1),X2) , Marked_indx(X1,X2)> 
     --> <Marked_indx(X1,active(X2)) , Marked_indx(X1,X2)>
  <Marked_indx(mark(X1),X2) , Marked_indx(X1,X2)> 
     --> <Marked_indx(active(X1),X2) , Marked_indx(X1,X2)>
  <Marked_indx(mark(X1),X2) , Marked_indx(X1,X2)> 
     --> <Marked_indx(X1,mark(X2)) , Marked_indx(X1,X2)>
  <Marked_indx(mark(X1),X2) , Marked_indx(X1,X2)> 
     --> <Marked_indx(mark(X1),X2) , Marked_indx(X1,X2)>
}

{  <Marked_from(active(X)) , Marked_from(X)> 
      --> <Marked_from(active(X)) , Marked_from(X)>
  <Marked_from(active(X)) , Marked_from(X)> 
     --> <Marked_from(mark(X)) , Marked_from(X)>
  <Marked_from(mark(X)) , Marked_from(X)> 
     --> <Marked_from(active(X)) , Marked_from(X)>
  <Marked_from(mark(X)) , Marked_from(X)> 
     --> <Marked_from(mark(X)) , Marked_from(X)>
}
APPLY CRITERIA (Subterm criterion)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  mark(0) >= active(0) ;
  mark(dbl(X)) >= active(dbl(mark(X))) ;
  mark(s(X)) >= active(s(X)) ;
  mark(nil) >= active(nil) ;
  mark(dbls(X)) >= active(dbls(mark(X))) ;
  mark(cons(X1,X2)) >= active(cons(X1,X2)) ;
  mark(sel(X1,X2)) >= active(sel(mark(X1),mark(X2))) ;
  mark(indx(X1,X2)) >= active(indx(mark(X1),X2)) ;
  mark(from(X)) >= active(from(X)) ;
  active(dbl(0)) >= mark(0) ;
  active(dbl(s(X))) >= mark(s(s(dbl(X)))) ;
  active(dbls(nil)) >= mark(nil) ;
  active(dbls(cons(X,Y))) >= mark(cons(dbl(X),dbls(Y))) ;
  active(sel(0,cons(X,Y))) >= mark(X) ;
  active(sel(s(X),cons(Y,Z))) >= mark(sel(X,Z)) ;
  active(indx(nil,X)) >= mark(nil) ;
  active(indx(cons(X,Y),Z)) >= mark(cons(sel(X,Z),indx(Y,Z))) ;
  active(from(X)) >= mark(cons(X,from(s(X)))) ;
  dbl(mark(X)) >= dbl(X) ;
  dbl(active(X)) >= dbl(X) ;
  s(mark(X)) >= s(X) ;
  s(active(X)) >= s(X) ;
  dbls(mark(X)) >= dbls(X) ;
  dbls(active(X)) >= dbls(X) ;
  cons(mark(X1),X2) >= cons(X1,X2) ;
  cons(active(X1),X2) >= cons(X1,X2) ;
  cons(X1,mark(X2)) >= cons(X1,X2) ;
  cons(X1,active(X2)) >= cons(X1,X2) ;
  sel(mark(X1),X2) >= sel(X1,X2) ;
  sel(active(X1),X2) >= sel(X1,X2) ;
  sel(X1,mark(X2)) >= sel(X1,X2) ;
  sel(X1,active(X2)) >= sel(X1,X2) ;
  indx(mark(X1),X2) >= indx(X1,X2) ;
  indx(active(X1),X2) >= indx(X1,X2) ;
  indx(X1,mark(X2)) >= indx(X1,X2) ;
  indx(X1,active(X2)) >= indx(X1,X2) ;
  from(mark(X)) >= from(X) ;
  from(active(X)) >= from(X) ;
  Marked_mark(dbl(X)) >= Marked_mark(X) ;
  Marked_mark(dbl(X)) >= Marked_active(dbl(mark(X))) ;
  Marked_mark(s(X)) >= Marked_active(s(X)) ;
  Marked_mark(dbls(X)) >= Marked_mark(X) ;
  Marked_mark(dbls(X)) >= Marked_active(dbls(mark(X))) ;
  Marked_mark(cons(X1,X2)) >= Marked_active(cons(X1,X2)) ;
  Marked_mark(sel(X1,X2)) >= Marked_mark(X1) ;
  Marked_mark(sel(X1,X2)) >= Marked_mark(X2) ;
  Marked_mark(sel(X1,X2)) >= Marked_active(sel(mark(X1),mark(X2))) ;
  Marked_mark(indx(X1,X2)) >= Marked_mark(X1) ;
  Marked_mark(indx(X1,X2)) >= Marked_active(indx(mark(X1),X2)) ;
  Marked_mark(from(X)) >= Marked_active(from(X)) ;
  Marked_active(dbl(s(X))) >= Marked_mark(s(s(dbl(X)))) ;
  Marked_active(dbls(cons(X,Y))) >= Marked_mark(cons(dbl(X),dbls(Y))) ;
  Marked_active(sel(0,cons(X,Y))) >= Marked_mark(X) ;
  Marked_active(sel(s(X),cons(Y,Z))) >= Marked_mark(sel(X,Z)) ;
  Marked_active(indx(cons(X,Y),Z)) >= Marked_mark(cons(sel(X,Z),indx(Y,Z))) ;
  Marked_active(from(X)) >= Marked_mark(cons(X,from(s(X)))) ;
 }
 + Disjunctions:{ 
{
  Marked_mark(dbl(X)) > Marked_mark(X) ;
 }
{
  Marked_mark(dbl(X)) > Marked_active(dbl(mark(X))) ;
 }
{
  Marked_mark(s(X)) > Marked_active(s(X)) ;
 }
{
  Marked_mark(dbls(X)) > Marked_mark(X) ;
 }
{
  Marked_mark(dbls(X)) > Marked_active(dbls(mark(X))) ;
 }
{
  Marked_mark(cons(X1,X2)) > Marked_active(cons(X1,X2)) ;
 }
{
  Marked_mark(sel(X1,X2)) > Marked_mark(X1) ;
 }
{
  Marked_mark(sel(X1,X2)) > Marked_mark(X2) ;
 }
{
  Marked_mark(sel(X1,X2)) > Marked_active(sel(mark(X1),mark(X2))) ;
 }
{
  Marked_mark(indx(X1,X2)) > Marked_mark(X1) ;
 }
{
  Marked_mark(indx(X1,X2)) > Marked_active(indx(mark(X1),X2)) ;
 }
{
  Marked_mark(from(X)) > Marked_active(from(X)) ;
 }
{
  Marked_active(dbl(s(X))) > Marked_mark(s(s(dbl(X)))) ;
 }
{
  Marked_active(dbls(cons(X,Y))) > Marked_mark(cons(dbl(X),dbls(Y))) ;
 }
{
  Marked_active(sel(0,cons(X,Y))) > Marked_mark(X) ;
 }
{
  Marked_active(sel(s(X),cons(Y,Z))) > Marked_mark(sel(X,Z)) ;
 }
{
  Marked_active(indx(cons(X,Y),Z)) > Marked_mark(cons(sel(X,Z),indx(Y,Z))) ;
 }
{
  Marked_active(from(X)) > Marked_mark(cons(X,from(s(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: mark(0) >= active(0)
constraint: mark(dbl(X)) >= active(dbl(mark(X)))
constraint: mark(s(X)) >= active(s(X))
constraint: mark(nil) >= active(nil)
constraint: mark(dbls(X)) >= active(dbls(mark(X)))
constraint: mark(cons(X1,X2)) >= active(cons(X1,X2))
constraint: mark(sel(X1,X2)) >= active(sel(mark(X1),mark(X2)))
constraint: mark(indx(X1,X2)) >= active(indx(mark(X1),X2))
constraint: mark(from(X)) >= active(from(X))
constraint: active(dbl(0)) >= mark(0)
constraint: active(dbl(s(X))) >= mark(s(s(dbl(X))))
constraint: active(dbls(nil)) >= mark(nil)
constraint: active(dbls(cons(X,Y))) >= mark(cons(dbl(X),dbls(Y)))
constraint: active(sel(0,cons(X,Y))) >= mark(X)
constraint: active(sel(s(X),cons(Y,Z))) >= mark(sel(X,Z))
constraint: active(indx(nil,X)) >= mark(nil)
constraint: active(indx(cons(X,Y),Z)) >= mark(cons(sel(X,Z),indx(Y,Z)))
constraint: active(from(X)) >= mark(cons(X,from(s(X))))
constraint: dbl(mark(X)) >= dbl(X)
constraint: dbl(active(X)) >= dbl(X)
constraint: s(mark(X)) >= s(X)
constraint: s(active(X)) >= s(X)
constraint: dbls(mark(X)) >= dbls(X)
constraint: dbls(active(X)) >= dbls(X)
constraint: cons(mark(X1),X2) >= cons(X1,X2)
constraint: cons(active(X1),X2) >= cons(X1,X2)
constraint: cons(X1,mark(X2)) >= cons(X1,X2)
constraint: cons(X1,active(X2)) >= cons(X1,X2)
constraint: sel(mark(X1),X2) >= sel(X1,X2)
constraint: sel(active(X1),X2) >= sel(X1,X2)
constraint: sel(X1,mark(X2)) >= sel(X1,X2)
constraint: sel(X1,active(X2)) >= sel(X1,X2)
constraint: indx(mark(X1),X2) >= indx(X1,X2)
constraint: indx(active(X1),X2) >= indx(X1,X2)
constraint: indx(X1,mark(X2)) >= indx(X1,X2)
constraint: indx(X1,active(X2)) >= indx(X1,X2)
constraint: from(mark(X)) >= from(X)
constraint: from(active(X)) >= from(X)
constraint: Marked_mark(dbl(X)) >= Marked_mark(X)
constraint: Marked_mark(dbl(X)) >= Marked_active(dbl(mark(X)))
constraint: Marked_mark(s(X)) >= Marked_active(s(X))
constraint: Marked_mark(dbls(X)) >= Marked_mark(X)
constraint: Marked_mark(dbls(X)) >= Marked_active(dbls(mark(X)))
constraint: Marked_mark(cons(X1,X2)) >= Marked_active(cons(X1,X2))
constraint: Marked_mark(sel(X1,X2)) >= Marked_mark(X1)
constraint: Marked_mark(sel(X1,X2)) >= Marked_mark(X2)
constraint: Marked_mark(sel(X1,X2)) >= Marked_active(sel(mark(X1),mark(X2)))
constraint: Marked_mark(indx(X1,X2)) >= Marked_mark(X1)
constraint: Marked_mark(indx(X1,X2)) >= Marked_active(indx(mark(X1),X2))
constraint: Marked_mark(from(X)) >= Marked_active(from(X))
constraint: Marked_active(dbl(s(X))) >= Marked_mark(s(s(dbl(X))))
constraint: Marked_active(dbls(cons(X,Y))) >= Marked_mark(cons(dbl(X),dbls(Y)))
constraint: Marked_active(sel(0,cons(X,Y))) >= Marked_mark(X)
constraint: Marked_active(sel(s(X),cons(Y,Z))) >= Marked_mark(sel(X,Z))
constraint: Marked_active(indx(cons(X,Y),Z)) >= Marked_mark(cons(sel(X,Z),
                                                             indx(Y,Z)))
constraint: Marked_active(from(X)) >= Marked_mark(cons(X,from(s(X))))
APPLY CRITERIA (Subterm criterion)

ST: Marked_dbl -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_s -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_dbls -> 1

APPLY CRITERIA (Subterm criterion)

ST: Marked_cons -> 2

APPLY CRITERIA (Subterm criterion)

ST: Marked_sel -> 2

APPLY CRITERIA (Subterm criterion)

ST: Marked_indx -> 2

APPLY CRITERIA (Subterm criterion)

ST: Marked_from -> 1

APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_mark(from(X)) , Marked_active(from(X))> 
      --> <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))>
  <Marked_mark(from(X)) , Marked_active(from(X))> 
     --> <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),
                                                          indx(Y,Z)))>
  <Marked_mark(from(X)) , Marked_active(from(X))> 
     --> <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))>
  <Marked_mark(from(X)) , Marked_active(from(X))> 
     --> <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)>
  <Marked_mark(from(X)) , Marked_active(from(X))> 
     --> <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))>
  <Marked_mark(from(X)) , Marked_active(from(X))> 
     --> <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_mark(indx(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))> 
     --> <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))>
  <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))> 
     --> <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),
                                                          indx(Y,Z)))>
  <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))> 
     --> <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))>
  <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))> 
     --> <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)>
  <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))> 
     --> <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))>
  <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))> 
     --> <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),
                                                          indx(Y,Z)))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_mark(dbls(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))> 
     --> <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))>
  <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))> 
     --> <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),
                                                          indx(Y,Z)))>
  <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))> 
     --> <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))>
  <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))> 
     --> <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)>
  <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))> 
     --> <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))>
  <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))> 
     --> <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_mark(dbl(X)) , Marked_mark(X)> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))> 
     --> <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))>
  <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))> 
     --> <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),
                                                          indx(Y,Z)))>
  <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))> 
     --> <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))>
  <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))> 
     --> <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)>
  <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))> 
     --> <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))>
  <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))> 
     --> <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_active(from(X)) , Marked_mark(cons(X,from(s(X))))> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_active(indx(cons(X,Y),Z)) , Marked_mark(cons(sel(X,Z),indx(Y,Z)))> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_active(sel(s(X),cons(Y,Z))) , Marked_mark(sel(X,Z))> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_active(sel(0,cons(X,Y))) , Marked_mark(X)> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_active(dbls(cons(X,Y))) , Marked_mark(cons(dbl(X),dbls(Y)))> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(from(X)) , Marked_active(from(X))>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_mark(X1)>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(indx(X1,X2)) , Marked_active(indx(mark(X1),X2))>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(dbls(X)) , Marked_mark(X)>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(dbls(X)) , Marked_active(dbls(mark(X)))>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(dbl(X)) , Marked_mark(X)>
  <Marked_active(dbl(s(X))) , Marked_mark(s(s(dbl(X))))> 
     --> <Marked_mark(dbl(X)) , Marked_active(dbl(mark(X)))>
}
APPLY CRITERIA (Subterm criterion)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  mark(0) >= active(0) ;
  mark(dbl(X)) >= active(dbl(mark(X))) ;
  mark(s(X)) >= active(s(X)) ;
  mark(nil) >= active(nil) ;
  mark(dbls(X)) >= active(dbls(mark(X))) ;
  mark(cons(X1,X2)) >= active(cons(X1,X2)) ;
  mark(sel(X1,X2)) >= active(sel(mark(X1),mark(X2))) ;
  mark(indx(X1,X2)) >= active(indx(mark(X1),X2)) ;
  mark(from(X)) >= active(from(X)) ;
  active(dbl(0)) >= mark(0) ;
  active(dbl(s(X))) >= mark(s(s(dbl(X)))) ;
  active(dbls(nil)) >= mark(nil) ;
  active(dbls(cons(X,Y))) >= mark(cons(dbl(X),dbls(Y))) ;
  active(sel(0,cons(X,Y))) >= mark(X) ;
  active(sel(s(X),cons(Y,Z))) >= mark(sel(X,Z)) ;
  active(indx(nil,X)) >= mark(nil) ;
  active(indx(cons(X,Y),Z)) >= mark(cons(sel(X,Z),indx(Y,Z))) ;
  active(from(X)) >= mark(cons(X,from(s(X)))) ;
  dbl(mark(X)) >= dbl(X) ;
  dbl(active(X)) >= dbl(X) ;
  s(mark(X)) >= s(X) ;
  s(active(X)) >= s(X) ;
  dbls(mark(X)) >= dbls(X) ;
  dbls(active(X)) >= dbls(X) ;
  cons(mark(X1),X2) >= cons(X1,X2) ;
  cons(active(X1),X2) >= cons(X1,X2) ;
  cons(X1,mark(X2)) >= cons(X1,X2) ;
  cons(X1,active(X2)) >= cons(X1,X2) ;
  sel(mark(X1),X2) >= sel(X1,X2) ;
  sel(active(X1),X2) >= sel(X1,X2) ;
  sel(X1,mark(X2)) >= sel(X1,X2) ;
  sel(X1,active(X2)) >= sel(X1,X2) ;
  indx(mark(X1),X2) >= indx(X1,X2) ;
  indx(active(X1),X2) >= indx(X1,X2) ;
  indx(X1,mark(X2)) >= indx(X1,X2) ;
  indx(X1,active(X2)) >= indx(X1,X2) ;
  from(mark(X)) >= from(X) ;
  from(active(X)) >= from(X) ;
  Marked_mark(dbl(X)) >= Marked_mark(X) ;
  Marked_mark(dbl(X)) >= Marked_active(dbl(mark(X))) ;
  Marked_mark(dbls(X)) >= Marked_mark(X) ;
  Marked_mark(dbls(X)) >= Marked_active(dbls(mark(X))) ;
  Marked_mark(sel(X1,X2)) >= Marked_mark(X1) ;
  Marked_mark(sel(X1,X2)) >= Marked_mark(X2) ;
  Marked_mark(sel(X1,X2)) >= Marked_active(sel(mark(X1),mark(X2))) ;
  Marked_mark(indx(X1,X2)) >= Marked_mark(X1) ;
  Marked_mark(indx(X1,X2)) >= Marked_active(indx(mark(X1),X2)) ;
  Marked_mark(from(X)) >= Marked_active(from(X)) ;
  Marked_active(dbl(s(X))) >= Marked_mark(s(s(dbl(X)))) ;
  Marked_active(dbls(cons(X,Y))) >= Marked_mark(cons(dbl(X),dbls(Y))) ;
  Marked_active(sel(0,cons(X,Y))) >= Marked_mark(X) ;
  Marked_active(sel(s(X),cons(Y,Z))) >= Marked_mark(sel(X,Z)) ;
  Marked_active(indx(cons(X,Y),Z)) >= Marked_mark(cons(sel(X,Z),indx(Y,Z))) ;
  Marked_active(from(X)) >= Marked_mark(cons(X,from(s(X)))) ;
 }
 + Disjunctions:{ 
{
  Marked_mark(dbl(X)) > Marked_mark(X) ;
 }
{
  Marked_mark(dbl(X)) > Marked_active(dbl(mark(X))) ;
 }
{
  Marked_mark(dbls(X)) > Marked_mark(X) ;
 }
{
  Marked_mark(dbls(X)) > Marked_active(dbls(mark(X))) ;
 }
{
  Marked_mark(sel(X1,X2)) > Marked_mark(X1) ;
 }
{
  Marked_mark(sel(X1,X2)) > Marked_mark(X2) ;
 }
{
  Marked_mark(sel(X1,X2)) > Marked_active(sel(mark(X1),mark(X2))) ;
 }
{
  Marked_mark(indx(X1,X2)) > Marked_mark(X1) ;
 }
{
  Marked_mark(indx(X1,X2)) > Marked_active(indx(mark(X1),X2)) ;
 }
{
  Marked_mark(from(X)) > Marked_active(from(X)) ;
 }
{
  Marked_active(dbl(s(X))) > Marked_mark(s(s(dbl(X)))) ;
 }
{
  Marked_active(dbls(cons(X,Y))) > Marked_mark(cons(dbl(X),dbls(Y))) ;
 }
{
  Marked_active(sel(0,cons(X,Y))) > Marked_mark(X) ;
 }
{
  Marked_active(sel(s(X),cons(Y,Z))) > Marked_mark(sel(X,Z)) ;
 }
{
  Marked_active(indx(cons(X,Y),Z)) > Marked_mark(cons(sel(X,Z),indx(Y,Z))) ;
 }
{
  Marked_active(from(X)) > Marked_mark(cons(X,from(s(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
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
Entering rpo_solver
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 15.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 15.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
=== TIMER virtual : 50.000000 ===
trying sub matrices of size: 1
Matrix interpretation constraints generated.
Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. 
Termination constraints generated.
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 50.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
No solution found for these constraints.
APPLY CRITERIA (Simple graph)
Found the following constraints:
{
  mark(0) >= active(0) ;
  mark(dbl(X)) >= active(dbl(mark(X))) ;
  mark(s(X)) >= active(s(X)) ;
  mark(nil) >= active(nil) ;
  mark(dbls(X)) >= active(dbls(mark(X))) ;
  mark(cons(X1,X2)) >= active(cons(X1,X2)) ;
  mark(sel(X1,X2)) >= active(sel(mark(X1),mark(X2))) ;
  mark(indx(X1,X2)) >= active(indx(mark(X1),X2)) ;
  mark(from(X)) >= active(from(X)) ;
  active(dbl(0)) >= mark(0) ;
  active(dbl(s(X))) >= mark(s(s(dbl(X)))) ;
  active(dbls(nil)) >= mark(nil) ;
  active(dbls(cons(X,Y))) >= mark(cons(dbl(X),dbls(Y))) ;
  active(sel(0,cons(X,Y))) >= mark(X) ;
  active(sel(s(X),cons(Y,Z))) >= mark(sel(X,Z)) ;
  active(indx(nil,X)) >= mark(nil) ;
  active(indx(cons(X,Y),Z)) >= mark(cons(sel(X,Z),indx(Y,Z))) ;
  active(from(X)) >= mark(cons(X,from(s(X)))) ;
  dbl(mark(X)) >= dbl(X) ;
  dbl(active(X)) >= dbl(X) ;
  s(mark(X)) >= s(X) ;
  s(active(X)) >= s(X) ;
  dbls(mark(X)) >= dbls(X) ;
  dbls(active(X)) >= dbls(X) ;
  cons(mark(X1),X2) >= cons(X1,X2) ;
  cons(active(X1),X2) >= cons(X1,X2) ;
  cons(X1,mark(X2)) >= cons(X1,X2) ;
  cons(X1,active(X2)) >= cons(X1,X2) ;
  sel(mark(X1),X2) >= sel(X1,X2) ;
  sel(active(X1),X2) >= sel(X1,X2) ;
  sel(X1,mark(X2)) >= sel(X1,X2) ;
  sel(X1,active(X2)) >= sel(X1,X2) ;
  indx(mark(X1),X2) >= indx(X1,X2) ;
  indx(active(X1),X2) >= indx(X1,X2) ;
  indx(X1,mark(X2)) >= indx(X1,X2) ;
  indx(X1,active(X2)) >= indx(X1,X2) ;
  from(mark(X)) >= from(X) ;
  from(active(X)) >= from(X) ;
  Marked_mark(dbl(X)) > Marked_mark(X) ;
  Marked_mark(dbl(X)) > Marked_active(dbl(mark(X))) ;
  Marked_mark(dbls(X)) > Marked_mark(X) ;
  Marked_mark(dbls(X)) > Marked_active(dbls(mark(X))) ;
  Marked_mark(sel(X1,X2)) > Marked_mark(X1) ;
  Marked_mark(sel(X1,X2)) > Marked_mark(X2) ;
  Marked_mark(sel(X1,X2)) > Marked_active(sel(mark(X1),mark(X2))) ;
  Marked_mark(indx(X1,X2)) > Marked_mark(X1) ;
  Marked_mark(indx(X1,X2)) > Marked_active(indx(mark(X1),X2)) ;
  Marked_mark(from(X)) >= Marked_active(from(X)) ;
  Marked_active(dbl(s(X))) > Marked_mark(s(s(dbl(X)))) ;
  Marked_active(dbls(cons(X,Y))) > Marked_mark(cons(dbl(X),dbls(Y))) ;
  Marked_active(sel(0,cons(X,Y))) > Marked_mark(X) ;
  Marked_active(sel(s(X),cons(Y,Z))) > Marked_mark(sel(X,Z)) ;
  Marked_active(indx(cons(X,Y),Z)) > Marked_mark(cons(sel(X,Z),indx(Y,Z))) ;
  Marked_active(from(X)) > Marked_mark(cons(X,from(s(X)))) ;
 }

APPLY CRITERIA (SOLVE_ORD)
Trying to solve the following constraints:
{
  mark(0) >= active(0) ;
  mark(dbl(X)) >= active(dbl(mark(X))) ;
  mark(s(X)) >= active(s(X)) ;
  mark(nil) >= active(nil) ;
  mark(dbls(X)) >= active(dbls(mark(X))) ;
  mark(cons(X1,X2)) >= active(cons(X1,X2)) ;
  mark(sel(X1,X2)) >= active(sel(mark(X1),mark(X2))) ;
  mark(indx(X1,X2)) >= active(indx(mark(X1),X2)) ;
  mark(from(X)) >= active(from(X)) ;
  active(dbl(0)) >= mark(0) ;
  active(dbl(s(X))) >= mark(s(s(dbl(X)))) ;
  active(dbls(nil)) >= mark(nil) ;
  active(dbls(cons(X,Y))) >= mark(cons(dbl(X),dbls(Y))) ;
  active(sel(0,cons(X,Y))) >= mark(X) ;
  active(sel(s(X),cons(Y,Z))) >= mark(sel(X,Z)) ;
  active(indx(nil,X)) >= mark(nil) ;
  active(indx(cons(X,Y),Z)) >= mark(cons(sel(X,Z),indx(Y,Z))) ;
  active(from(X)) >= mark(cons(X,from(s(X)))) ;
  dbl(mark(X)) >= dbl(X) ;
  dbl(active(X)) >= dbl(X) ;
  s(mark(X)) >= s(X) ;
  s(active(X)) >= s(X) ;
  dbls(mark(X)) >= dbls(X) ;
  dbls(active(X)) >= dbls(X) ;
  cons(mark(X1),X2) >= cons(X1,X2) ;
  cons(active(X1),X2) >= cons(X1,X2) ;
  cons(X1,mark(X2)) >= cons(X1,X2) ;
  cons(X1,active(X2)) >= cons(X1,X2) ;
  sel(mark(X1),X2) >= sel(X1,X2) ;
  sel(active(X1),X2) >= sel(X1,X2) ;
  sel(X1,mark(X2)) >= sel(X1,X2) ;
  sel(X1,active(X2)) >= sel(X1,X2) ;
  indx(mark(X1),X2) >= indx(X1,X2) ;
  indx(active(X1),X2) >= indx(X1,X2) ;
  indx(X1,mark(X2)) >= indx(X1,X2) ;
  indx(X1,active(X2)) >= indx(X1,X2) ;
  from(mark(X)) >= from(X) ;
  from(active(X)) >= from(X) ;
  Marked_mark(dbl(X)) > Marked_mark(X) ;
  Marked_mark(dbl(X)) > Marked_active(dbl(mark(X))) ;
  Marked_mark(dbls(X)) > Marked_mark(X) ;
  Marked_mark(dbls(X)) > Marked_active(dbls(mark(X))) ;
  Marked_mark(sel(X1,X2)) > Marked_mark(X1) ;
  Marked_mark(sel(X1,X2)) > Marked_mark(X2) ;
  Marked_mark(sel(X1,X2)) > Marked_active(sel(mark(X1),mark(X2))) ;
  Marked_mark(indx(X1,X2)) > Marked_mark(X1) ;
  Marked_mark(indx(X1,X2)) > Marked_active(indx(mark(X1),X2)) ;
  Marked_mark(from(X)) >= Marked_active(from(X)) ;
  Marked_active(dbl(s(X))) > Marked_mark(s(s(dbl(X)))) ;
  Marked_active(dbls(cons(X,Y))) > Marked_mark(cons(dbl(X),dbls(Y))) ;
  Marked_active(sel(0,cons(X,Y))) > Marked_mark(X) ;
  Marked_active(sel(s(X),cons(Y,Z))) > Marked_mark(sel(X,Z)) ;
  Marked_active(indx(cons(X,Y),Z)) > Marked_mark(cons(sel(X,Z),indx(Y,Z))) ;
  Marked_active(from(X)) > Marked_mark(cons(X,from(s(X)))) ;
 }
 + Disjunctions:{ 
 } 
=== 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 ===
No solution found for these parameters.(704 bt (724) [389])
=== 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)
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_cons(mark(X1),X2) , Marked_cons(X1,X2)> 
      --> <Marked_cons(mark(X1),X2) , Marked_cons(X1,X2)>
  <Marked_cons(mark(X1),X2) , Marked_cons(X1,X2)> 
     --> <Marked_cons(active(X1),X2) , Marked_cons(X1,X2)>
  <Marked_cons(active(X1),X2) , Marked_cons(X1,X2)> 
     --> <Marked_cons(mark(X1),X2) , Marked_cons(X1,X2)>
  <Marked_cons(active(X1),X2) , Marked_cons(X1,X2)> 
     --> <Marked_cons(active(X1),X2) , Marked_cons(X1,X2)>
}
APPLY CRITERIA (Subterm criterion)

ST: Marked_cons -> 1

APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_sel(mark(X1),X2) , Marked_sel(X1,X2)> 
      --> <Marked_sel(mark(X1),X2) , Marked_sel(X1,X2)>
  <Marked_sel(mark(X1),X2) , Marked_sel(X1,X2)> 
     --> <Marked_sel(active(X1),X2) , Marked_sel(X1,X2)>
  <Marked_sel(active(X1),X2) , Marked_sel(X1,X2)> 
     --> <Marked_sel(mark(X1),X2) , Marked_sel(X1,X2)>
  <Marked_sel(active(X1),X2) , Marked_sel(X1,X2)> 
     --> <Marked_sel(active(X1),X2) , Marked_sel(X1,X2)>
}
APPLY CRITERIA (Subterm criterion)

ST: Marked_sel -> 1

APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_indx(mark(X1),X2) , Marked_indx(X1,X2)> 
      --> <Marked_indx(mark(X1),X2) , Marked_indx(X1,X2)>
  <Marked_indx(mark(X1),X2) , Marked_indx(X1,X2)> 
     --> <Marked_indx(active(X1),X2) , Marked_indx(X1,X2)>
  <Marked_indx(active(X1),X2) , Marked_indx(X1,X2)> 
     --> <Marked_indx(mark(X1),X2) , Marked_indx(X1,X2)>
  <Marked_indx(active(X1),X2) , Marked_indx(X1,X2)> 
     --> <Marked_indx(active(X1),X2) , Marked_indx(X1,X2)>
}
APPLY CRITERIA (Subterm criterion)

ST: Marked_indx -> 1

APPLY CRITERIA (Graph splitting)
Found 0 components:
APPLY CRITERIA (Graph splitting)
Found 0 components:
NOT SOLVED
No proof found
Cime worked for 91.456660 seconds (real time)
Cime Exit Status: 0