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

TRS termination of:
[1] active(fib(N)) -> mark(sel(N,fib1(s(0),s(0))))
[2] active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
[3] active(add(0,X)) -> mark(X)
[4] active(add(s(X),Y)) -> mark(s(add(X,Y)))
[5] active(sel(0,cons(X,XS))) -> mark(X)
[6] active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
[7] mark(fib(X)) -> active(fib(mark(X)))
[8] mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2)))
[9] mark(fib1(X1,X2)) -> active(fib1(mark(X1),mark(X2)))
[10] mark(s(X)) -> active(s(mark(X)))
[11] mark(0) -> active(0)
[12] mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
[13] mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
[14] fib(mark(X)) -> fib(X)
[15] fib(active(X)) -> fib(X)
[16] sel(mark(X1),X2) -> sel(X1,X2)
[17] sel(X1,mark(X2)) -> sel(X1,X2)
[18] sel(active(X1),X2) -> sel(X1,X2)
[19] sel(X1,active(X2)) -> sel(X1,X2)
[20] fib1(mark(X1),X2) -> fib1(X1,X2)
[21] fib1(X1,mark(X2)) -> fib1(X1,X2)
[22] fib1(active(X1),X2) -> fib1(X1,X2)
[23] fib1(X1,active(X2)) -> fib1(X1,X2)
[24] s(mark(X)) -> s(X)
[25] s(active(X)) -> s(X)
[26] cons(mark(X1),X2) -> cons(X1,X2)
[27] cons(X1,mark(X2)) -> cons(X1,X2)
[28] cons(active(X1),X2) -> cons(X1,X2)
[29] cons(X1,active(X2)) -> cons(X1,X2)
[30] add(mark(X1),X2) -> add(X1,X2)
[31] add(X1,mark(X2)) -> add(X1,X2)
[32] add(active(X1),X2) -> add(X1,X2)
[33] add(X1,active(X2)) -> add(X1,X2)


Sub problem: 
guided: 

DP termination of:
<Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))>
<Marked_active(fib(N)) , Marked_sel(N,fib1(s(0),s(0)))>
<Marked_active(fib(N)) , Marked_fib1(s(0),s(0))>
<Marked_active(fib(N)) , Marked_s(0)>
<Marked_active(fib(N)) , Marked_s(0)>
<Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))>
<Marked_active(fib1(X,Y)) , Marked_cons(X,fib1(Y,add(X,Y)))>
<Marked_active(fib1(X,Y)) , Marked_fib1(Y,add(X,Y))>
<Marked_active(fib1(X,Y)) , Marked_add(X,Y)>
<Marked_active(add(0,X)) , Marked_mark(X)>
<Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))>
<Marked_active(add(s(X),Y)) , Marked_s(add(X,Y))>
<Marked_active(add(s(X),Y)) , Marked_add(X,Y)>
<Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)>
<Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))>
<Marked_active(sel(s(N),cons(X,XS))) , Marked_sel(N,XS)>
<Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
<Marked_mark(fib(X)) , Marked_fib(mark(X))>
<Marked_mark(fib(X)) , Marked_mark(X)>
<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(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
<Marked_mark(fib1(X1,X2)) , Marked_fib1(mark(X1),mark(X2))>
<Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
<Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
<Marked_mark(s(X)) , Marked_active(s(mark(X)))>
<Marked_mark(s(X)) , Marked_s(mark(X))>
<Marked_mark(s(X)) , Marked_mark(X)>
<Marked_mark(0) , Marked_active(0)>
<Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
<Marked_mark(cons(X1,X2)) , Marked_cons(mark(X1),X2)>
<Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
<Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
<Marked_mark(add(X1,X2)) , Marked_add(mark(X1),mark(X2))>
<Marked_mark(add(X1,X2)) , Marked_mark(X1)>
<Marked_mark(add(X1,X2)) , Marked_mark(X2)>
<Marked_fib(mark(X)) , Marked_fib(X)>
<Marked_fib(active(X)) , Marked_fib(X)>
<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_fib1(mark(X1),X2) , Marked_fib1(X1,X2)>
<Marked_fib1(X1,mark(X2)) , Marked_fib1(X1,X2)>
<Marked_fib1(active(X1),X2) , Marked_fib1(X1,X2)>
<Marked_fib1(X1,active(X2)) , Marked_fib1(X1,X2)>
<Marked_s(mark(X)) , Marked_s(X)>
<Marked_s(active(X)) , Marked_s(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_add(mark(X1),X2) , Marked_add(X1,X2)>
<Marked_add(X1,mark(X2)) , Marked_add(X1,X2)>
<Marked_add(active(X1),X2) , Marked_add(X1,X2)>
<Marked_add(X1,active(X2)) , Marked_add(X1,X2)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 7 components:

{  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
      --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib(X)) , Marked_mark(X)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib(X)) , Marked_mark(X)>
  <Marked_mark(add(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))> 
     --> <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))>
  <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))> 
     --> <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)>
  <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))> 
     --> <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))>
  <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))> 
     --> <Marked_active(add(0,X)) , Marked_mark(X)>
  <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))> 
     --> <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))>
  <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))> 
     --> <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib(X)) , Marked_mark(X)>
  <Marked_mark(cons(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))> 
     --> <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))>
  <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))> 
     --> <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)>
  <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))> 
     --> <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))>
  <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))> 
     --> <Marked_active(add(0,X)) , Marked_mark(X)>
  <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))> 
     --> <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))>
  <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))> 
     --> <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_mark(s(X)) , Marked_mark(X)> --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(fib(X)) , Marked_mark(X)>
  <Marked_mark(s(X)) , Marked_mark(X)> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_mark(s(X)) , Marked_active(s(mark(X)))> 
     --> <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))>
  <Marked_mark(s(X)) , Marked_active(s(mark(X)))> 
     --> <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)>
  <Marked_mark(s(X)) , Marked_active(s(mark(X)))> 
     --> <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))>
  <Marked_mark(s(X)) , Marked_active(s(mark(X)))> 
     --> <Marked_active(add(0,X)) , Marked_mark(X)>
  <Marked_mark(s(X)) , Marked_active(s(mark(X)))> 
     --> <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))>
  <Marked_mark(s(X)) , Marked_active(s(mark(X)))> 
     --> <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib(X)) , Marked_mark(X)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib(X)) , Marked_mark(X)>
  <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))> 
     --> <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))>
  <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))> 
     --> <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)>
  <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))> 
     --> <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))>
  <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))> 
     --> <Marked_active(add(0,X)) , Marked_mark(X)>
  <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))> 
     --> <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))>
  <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))> 
     --> <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),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(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(fib(X)) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X2)> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(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(fib(X)) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_mark(X1)> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(add(0,X)) , Marked_mark(X)>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))>
  <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))> 
     --> <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(fib(X)) , Marked_mark(X)>
  <Marked_mark(fib(X)) , Marked_mark(X)> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))> 
     --> <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))>
  <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))> 
     --> <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)>
  <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))> 
     --> <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))>
  <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))> 
     --> <Marked_active(add(0,X)) , Marked_mark(X)>
  <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))> 
     --> <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))>
  <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))> 
     --> <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(fib(X)) , Marked_mark(X)>
  <Marked_active(sel(s(N),cons(X,XS))) , Marked_mark(sel(N,XS))> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(fib(X)) , Marked_mark(X)>
  <Marked_active(sel(0,cons(X,XS))) , Marked_mark(X)> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(fib(X)) , Marked_mark(X)>
  <Marked_active(add(s(X),Y)) , Marked_mark(s(add(X,Y)))> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(fib(X)) , Marked_mark(X)>
  <Marked_active(add(0,X)) , Marked_mark(X)> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(fib(X)) , Marked_mark(X)>
  <Marked_active(fib1(X,Y)) , Marked_mark(cons(X,fib1(Y,add(X,Y))))> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X2)>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(add(X1,X2)) , Marked_mark(X1)>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(add(X1,X2)) , Marked_active(add(mark(X1),mark(X2)))>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(cons(X1,X2)) , Marked_mark(X1)>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(cons(X1,X2)) , Marked_active(cons(mark(X1),X2))>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(s(X)) , Marked_mark(X)>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(s(X)) , Marked_active(s(mark(X)))>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X2)>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_mark(X1)>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(fib1(X1,X2)) , Marked_active(fib1(mark(X1),mark(X2)))>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X2)>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_mark(X1)>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(sel(X1,X2)) , Marked_active(sel(mark(X1),mark(X2)))>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(fib(X)) , Marked_mark(X)>
  <Marked_active(fib(N)) , Marked_mark(sel(N,fib1(s(0),s(0))))> 
     --> <Marked_mark(fib(X)) , Marked_active(fib(mark(X)))>
}

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

{  <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_fib1(X1,active(X2)) , Marked_fib1(X1,X2)> 
      --> <Marked_fib1(X1,active(X2)) , Marked_fib1(X1,X2)>
  <Marked_fib1(X1,active(X2)) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(active(X1),X2) , Marked_fib1(X1,X2)>
  <Marked_fib1(X1,active(X2)) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(X1,mark(X2)) , Marked_fib1(X1,X2)>
  <Marked_fib1(X1,active(X2)) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(mark(X1),X2) , Marked_fib1(X1,X2)>
  <Marked_fib1(active(X1),X2) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(X1,active(X2)) , Marked_fib1(X1,X2)>
  <Marked_fib1(active(X1),X2) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(active(X1),X2) , Marked_fib1(X1,X2)>
  <Marked_fib1(active(X1),X2) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(X1,mark(X2)) , Marked_fib1(X1,X2)>
  <Marked_fib1(active(X1),X2) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(mark(X1),X2) , Marked_fib1(X1,X2)>
  <Marked_fib1(X1,mark(X2)) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(X1,active(X2)) , Marked_fib1(X1,X2)>
  <Marked_fib1(X1,mark(X2)) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(active(X1),X2) , Marked_fib1(X1,X2)>
  <Marked_fib1(X1,mark(X2)) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(X1,mark(X2)) , Marked_fib1(X1,X2)>
  <Marked_fib1(X1,mark(X2)) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(mark(X1),X2) , Marked_fib1(X1,X2)>
  <Marked_fib1(mark(X1),X2) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(X1,active(X2)) , Marked_fib1(X1,X2)>
  <Marked_fib1(mark(X1),X2) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(active(X1),X2) , Marked_fib1(X1,X2)>
  <Marked_fib1(mark(X1),X2) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(X1,mark(X2)) , Marked_fib1(X1,X2)>
  <Marked_fib1(mark(X1),X2) , Marked_fib1(X1,X2)> 
     --> <Marked_fib1(mark(X1),X2) , Marked_fib1(X1,X2)>
}

{  <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_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_add(X1,active(X2)) , Marked_add(X1,X2)> 
      --> <Marked_add(X1,active(X2)) , Marked_add(X1,X2)>
  <Marked_add(X1,active(X2)) , Marked_add(X1,X2)> 
     --> <Marked_add(active(X1),X2) , Marked_add(X1,X2)>
  <Marked_add(X1,active(X2)) , Marked_add(X1,X2)> 
     --> <Marked_add(X1,mark(X2)) , Marked_add(X1,X2)>
  <Marked_add(X1,active(X2)) , Marked_add(X1,X2)> 
     --> <Marked_add(mark(X1),X2) , Marked_add(X1,X2)>
  <Marked_add(active(X1),X2) , Marked_add(X1,X2)> 
     --> <Marked_add(X1,active(X2)) , Marked_add(X1,X2)>
  <Marked_add(active(X1),X2) , Marked_add(X1,X2)> 
     --> <Marked_add(active(X1),X2) , Marked_add(X1,X2)>
  <Marked_add(active(X1),X2) , Marked_add(X1,X2)> 
     --> <Marked_add(X1,mark(X2)) , Marked_add(X1,X2)>
  <Marked_add(active(X1),X2) , Marked_add(X1,X2)> 
     --> <Marked_add(mark(X1),X2) , Marked_add(X1,X2)>
  <Marked_add(X1,mark(X2)) , Marked_add(X1,X2)> 
     --> <Marked_add(X1,active(X2)) , Marked_add(X1,X2)>
  <Marked_add(X1,mark(X2)) , Marked_add(X1,X2)> 
     --> <Marked_add(active(X1),X2) , Marked_add(X1,X2)>
  <Marked_add(X1,mark(X2)) , Marked_add(X1,X2)> 
     --> <Marked_add(X1,mark(X2)) , Marked_add(X1,X2)>
  <Marked_add(X1,mark(X2)) , Marked_add(X1,X2)> 
     --> <Marked_add(mark(X1),X2) , Marked_add(X1,X2)>
  <Marked_add(mark(X1),X2) , Marked_add(X1,X2)> 
     --> <Marked_add(X1,active(X2)) , Marked_add(X1,X2)>
  <Marked_add(mark(X1),X2) , Marked_add(X1,X2)> 
     --> <Marked_add(active(X1),X2) , Marked_add(X1,X2)>
  <Marked_add(mark(X1),X2) , Marked_add(X1,X2)> 
     --> <Marked_add(X1,mark(X2)) , Marked_add(X1,X2)>
  <Marked_add(mark(X1),X2) , Marked_add(X1,X2)> 
     --> <Marked_add(mark(X1),X2) , Marked_add(X1,X2)>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  mark(sel(X1,X2)) >= active(sel(mark(X1),mark(X2))) ;
  mark(fib1(X1,X2)) >= active(fib1(mark(X1),mark(X2))) ;
  mark(s(X)) >= active(s(mark(X))) ;
  mark(0) >= active(0) ;
  mark(fib(X)) >= active(fib(mark(X))) ;
  mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ;
  mark(add(X1,X2)) >= active(add(mark(X1),mark(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) ;
  fib1(mark(X1),X2) >= fib1(X1,X2) ;
  fib1(active(X1),X2) >= fib1(X1,X2) ;
  fib1(X1,mark(X2)) >= fib1(X1,X2) ;
  fib1(X1,active(X2)) >= fib1(X1,X2) ;
  s(mark(X)) >= s(X) ;
  s(active(X)) >= s(X) ;
  active(sel(s(N),cons(X,XS))) >= mark(sel(N,XS)) ;
  active(sel(0,cons(X,XS))) >= mark(X) ;
  active(fib1(X,Y)) >= mark(cons(X,fib1(Y,add(X,Y)))) ;
  active(fib(N)) >= mark(sel(N,fib1(s(0),s(0)))) ;
  active(add(s(X),Y)) >= mark(s(add(X,Y))) ;
  active(add(0,X)) >= mark(X) ;
  fib(mark(X)) >= fib(X) ;
  fib(active(X)) >= fib(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) ;
  add(mark(X1),X2) >= add(X1,X2) ;
  add(active(X1),X2) >= add(X1,X2) ;
  add(X1,mark(X2)) >= add(X1,X2) ;
  add(X1,active(X2)) >= add(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(fib1(X1,X2)) >= Marked_mark(X1) ;
  Marked_mark(fib1(X1,X2)) >= Marked_mark(X2) ;
  Marked_mark(fib1(X1,X2)) >= Marked_active(fib1(mark(X1),mark(X2))) ;
  Marked_mark(s(X)) >= Marked_mark(X) ;
  Marked_mark(s(X)) >= Marked_active(s(mark(X))) ;
  Marked_mark(fib(X)) >= Marked_mark(X) ;
  Marked_mark(fib(X)) >= Marked_active(fib(mark(X))) ;
  Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ;
  Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) ;
  Marked_mark(add(X1,X2)) >= Marked_mark(X1) ;
  Marked_mark(add(X1,X2)) >= Marked_mark(X2) ;
  Marked_mark(add(X1,X2)) >= Marked_active(add(mark(X1),mark(X2))) ;
  Marked_active(sel(s(N),cons(X,XS))) >= Marked_mark(sel(N,XS)) ;
  Marked_active(sel(0,cons(X,XS))) >= Marked_mark(X) ;
  Marked_active(fib1(X,Y)) >= Marked_mark(cons(X,fib1(Y,add(X,Y)))) ;
  Marked_active(fib(N)) >= Marked_mark(sel(N,fib1(s(0),s(0)))) ;
  Marked_active(add(s(X),Y)) >= Marked_mark(s(add(X,Y))) ;
  Marked_active(add(0,X)) >= Marked_mark(X) ;
 }
 + Disjunctions:{ 
{
  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(fib1(X1,X2)) > Marked_mark(X1) ;
 }
{
  Marked_mark(fib1(X1,X2)) > Marked_mark(X2) ;
 }
{
  Marked_mark(fib1(X1,X2)) > Marked_active(fib1(mark(X1),mark(X2))) ;
 }
{
  Marked_mark(s(X)) > Marked_mark(X) ;
 }
{
  Marked_mark(s(X)) > Marked_active(s(mark(X))) ;
 }
{
  Marked_mark(fib(X)) > Marked_mark(X) ;
 }
{
  Marked_mark(fib(X)) > Marked_active(fib(mark(X))) ;
 }
{
  Marked_mark(cons(X1,X2)) > Marked_mark(X1) ;
 }
{
  Marked_mark(cons(X1,X2)) > Marked_active(cons(mark(X1),X2)) ;
 }
{
  Marked_mark(add(X1,X2)) > Marked_mark(X1) ;
 }
{
  Marked_mark(add(X1,X2)) > Marked_mark(X2) ;
 }
{
  Marked_mark(add(X1,X2)) > Marked_active(add(mark(X1),mark(X2))) ;
 }
{
  Marked_active(sel(s(N),cons(X,XS))) > Marked_mark(sel(N,XS)) ;
 }
{
  Marked_active(sel(0,cons(X,XS))) > Marked_mark(X) ;
 }
{
  Marked_active(fib1(X,Y)) > Marked_mark(cons(X,fib1(Y,add(X,Y)))) ;
 }
{
  Marked_active(fib(N)) > Marked_mark(sel(N,fib1(s(0),s(0)))) ;
 }
{
  Marked_active(add(s(X),Y)) > Marked_mark(s(add(X,Y))) ;
 }
{
  Marked_active(add(0,X)) > Marked_mark(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(sel(X1,X2)) >= active(sel(mark(X1),mark(X2)))
constraint: mark(fib1(X1,X2)) >= active(fib1(mark(X1),mark(X2)))
constraint: mark(s(X)) >= active(s(mark(X)))
constraint: mark(0) >= active(0)
constraint: mark(fib(X)) >= active(fib(mark(X)))
constraint: mark(cons(X1,X2)) >= active(cons(mark(X1),X2))
constraint: mark(add(X1,X2)) >= active(add(mark(X1),mark(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: fib1(mark(X1),X2) >= fib1(X1,X2)
constraint: fib1(active(X1),X2) >= fib1(X1,X2)
constraint: fib1(X1,mark(X2)) >= fib1(X1,X2)
constraint: fib1(X1,active(X2)) >= fib1(X1,X2)
constraint: s(mark(X)) >= s(X)
constraint: s(active(X)) >= s(X)
constraint: active(sel(s(N),cons(X,XS))) >= mark(sel(N,XS))
constraint: active(sel(0,cons(X,XS))) >= mark(X)
constraint: active(fib1(X,Y)) >= mark(cons(X,fib1(Y,add(X,Y))))
constraint: active(fib(N)) >= mark(sel(N,fib1(s(0),s(0))))
constraint: active(add(s(X),Y)) >= mark(s(add(X,Y)))
constraint: active(add(0,X)) >= mark(X)
constraint: fib(mark(X)) >= fib(X)
constraint: fib(active(X)) >= fib(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: add(mark(X1),X2) >= add(X1,X2)
constraint: add(active(X1),X2) >= add(X1,X2)
constraint: add(X1,mark(X2)) >= add(X1,X2)
constraint: add(X1,active(X2)) >= add(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(fib1(X1,X2)) >= Marked_mark(X1)
constraint: Marked_mark(fib1(X1,X2)) >= Marked_mark(X2)
constraint: Marked_mark(fib1(X1,X2)) >= Marked_active(fib1(mark(X1),mark(X2)))
constraint: Marked_mark(s(X)) >= Marked_mark(X)
constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X)))
constraint: Marked_mark(fib(X)) >= Marked_mark(X)
constraint: Marked_mark(fib(X)) >= Marked_active(fib(mark(X)))
constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1)
constraint: Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2))
constraint: Marked_mark(add(X1,X2)) >= Marked_mark(X1)
constraint: Marked_mark(add(X1,X2)) >= Marked_mark(X2)
constraint: Marked_mark(add(X1,X2)) >= Marked_active(add(mark(X1),mark(X2)))
constraint: Marked_active(sel(s(N),cons(X,XS))) >= Marked_mark(sel(N,XS))
constraint: Marked_active(sel(0,cons(X,XS))) >= Marked_mark(X)
constraint: Marked_active(fib1(X,Y)) >= Marked_mark(cons(X,fib1(Y,add(X,Y))))
constraint: Marked_active(fib(N)) >= Marked_mark(sel(N,fib1(s(0),s(0))))
constraint: Marked_active(add(s(X),Y)) >= Marked_mark(s(add(X,Y)))
constraint: Marked_active(add(0,X)) >= Marked_mark(X)
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  mark(sel(X1,X2)) >= active(sel(mark(X1),mark(X2))) ;
  mark(fib1(X1,X2)) >= active(fib1(mark(X1),mark(X2))) ;
  mark(s(X)) >= active(s(mark(X))) ;
  mark(0) >= active(0) ;
  mark(fib(X)) >= active(fib(mark(X))) ;
  mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ;
  mark(add(X1,X2)) >= active(add(mark(X1),mark(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) ;
  fib1(mark(X1),X2) >= fib1(X1,X2) ;
  fib1(active(X1),X2) >= fib1(X1,X2) ;
  fib1(X1,mark(X2)) >= fib1(X1,X2) ;
  fib1(X1,active(X2)) >= fib1(X1,X2) ;
  s(mark(X)) >= s(X) ;
  s(active(X)) >= s(X) ;
  active(sel(s(N),cons(X,XS))) >= mark(sel(N,XS)) ;
  active(sel(0,cons(X,XS))) >= mark(X) ;
  active(fib1(X,Y)) >= mark(cons(X,fib1(Y,add(X,Y)))) ;
  active(fib(N)) >= mark(sel(N,fib1(s(0),s(0)))) ;
  active(add(s(X),Y)) >= mark(s(add(X,Y))) ;
  active(add(0,X)) >= mark(X) ;
  fib(mark(X)) >= fib(X) ;
  fib(active(X)) >= fib(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) ;
  add(mark(X1),X2) >= add(X1,X2) ;
  add(active(X1),X2) >= add(X1,X2) ;
  add(X1,mark(X2)) >= add(X1,X2) ;
  add(X1,active(X2)) >= add(X1,X2) ;
  Marked_fib(mark(X)) >= Marked_fib(X) ;
  Marked_fib(active(X)) >= Marked_fib(X) ;
 }
 + Disjunctions:{ 
{
  Marked_fib(mark(X)) > Marked_fib(X) ;
 }
{
  Marked_fib(active(X)) > Marked_fib(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 : 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 timeout reached
=== 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 53.345314 seconds (real time)
Cime Exit Status: 0