MAYBE

Problem:
 active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
 active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
 active(add(0(),X)) -> mark(X)
 active(add(s(X),Y)) -> mark(s(add(X,Y)))
 active(sel(0(),cons(X,XS))) -> mark(X)
 active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
 active(fib(X)) -> fib(active(X))
 active(sel(X1,X2)) -> sel(active(X1),X2)
 active(sel(X1,X2)) -> sel(X1,active(X2))
 active(fib1(X1,X2)) -> fib1(active(X1),X2)
 active(fib1(X1,X2)) -> fib1(X1,active(X2))
 active(s(X)) -> s(active(X))
 active(cons(X1,X2)) -> cons(active(X1),X2)
 active(add(X1,X2)) -> add(active(X1),X2)
 active(add(X1,X2)) -> add(X1,active(X2))
 fib(mark(X)) -> mark(fib(X))
 sel(mark(X1),X2) -> mark(sel(X1,X2))
 sel(X1,mark(X2)) -> mark(sel(X1,X2))
 fib1(mark(X1),X2) -> mark(fib1(X1,X2))
 fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
 s(mark(X)) -> mark(s(X))
 cons(mark(X1),X2) -> mark(cons(X1,X2))
 add(mark(X1),X2) -> mark(add(X1,X2))
 add(X1,mark(X2)) -> mark(add(X1,X2))
 proper(fib(X)) -> fib(proper(X))
 proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
 proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
 proper(s(X)) -> s(proper(X))
 proper(0()) -> ok(0())
 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
 proper(add(X1,X2)) -> add(proper(X1),proper(X2))
 fib(ok(X)) -> ok(fib(X))
 sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
 fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
 s(ok(X)) -> ok(s(X))
 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
 add(ok(X1),ok(X2)) -> ok(add(X1,X2))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 DP Processor:
  DPs:
   active#(fib(N)) -> s#(0())
   active#(fib(N)) -> fib1#(s(0()),s(0()))
   active#(fib(N)) -> sel#(N,fib1(s(0()),s(0())))
   active#(fib1(X,Y)) -> add#(X,Y)
   active#(fib1(X,Y)) -> fib1#(Y,add(X,Y))
   active#(fib1(X,Y)) -> cons#(X,fib1(Y,add(X,Y)))
   active#(add(s(X),Y)) -> add#(X,Y)
   active#(add(s(X),Y)) -> s#(add(X,Y))
   active#(sel(s(N),cons(X,XS))) -> sel#(N,XS)
   active#(fib(X)) -> active#(X)
   active#(fib(X)) -> fib#(active(X))
   active#(sel(X1,X2)) -> active#(X1)
   active#(sel(X1,X2)) -> sel#(active(X1),X2)
   active#(sel(X1,X2)) -> active#(X2)
   active#(sel(X1,X2)) -> sel#(X1,active(X2))
   active#(fib1(X1,X2)) -> active#(X1)
   active#(fib1(X1,X2)) -> fib1#(active(X1),X2)
   active#(fib1(X1,X2)) -> active#(X2)
   active#(fib1(X1,X2)) -> fib1#(X1,active(X2))
   active#(s(X)) -> active#(X)
   active#(s(X)) -> s#(active(X))
   active#(cons(X1,X2)) -> active#(X1)
   active#(cons(X1,X2)) -> cons#(active(X1),X2)
   active#(add(X1,X2)) -> active#(X1)
   active#(add(X1,X2)) -> add#(active(X1),X2)
   active#(add(X1,X2)) -> active#(X2)
   active#(add(X1,X2)) -> add#(X1,active(X2))
   fib#(mark(X)) -> fib#(X)
   sel#(mark(X1),X2) -> sel#(X1,X2)
   sel#(X1,mark(X2)) -> sel#(X1,X2)
   fib1#(mark(X1),X2) -> fib1#(X1,X2)
   fib1#(X1,mark(X2)) -> fib1#(X1,X2)
   s#(mark(X)) -> s#(X)
   cons#(mark(X1),X2) -> cons#(X1,X2)
   add#(mark(X1),X2) -> add#(X1,X2)
   add#(X1,mark(X2)) -> add#(X1,X2)
   proper#(fib(X)) -> proper#(X)
   proper#(fib(X)) -> fib#(proper(X))
   proper#(sel(X1,X2)) -> proper#(X2)
   proper#(sel(X1,X2)) -> proper#(X1)
   proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2))
   proper#(fib1(X1,X2)) -> proper#(X2)
   proper#(fib1(X1,X2)) -> proper#(X1)
   proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2))
   proper#(s(X)) -> proper#(X)
   proper#(s(X)) -> s#(proper(X))
   proper#(cons(X1,X2)) -> proper#(X2)
   proper#(cons(X1,X2)) -> proper#(X1)
   proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
   proper#(add(X1,X2)) -> proper#(X2)
   proper#(add(X1,X2)) -> proper#(X1)
   proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
   fib#(ok(X)) -> fib#(X)
   sel#(ok(X1),ok(X2)) -> sel#(X1,X2)
   fib1#(ok(X1),ok(X2)) -> fib1#(X1,X2)
   s#(ok(X)) -> s#(X)
   cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
   add#(ok(X1),ok(X2)) -> add#(X1,X2)
   top#(mark(X)) -> proper#(X)
   top#(mark(X)) -> top#(proper(X))
   top#(ok(X)) -> active#(X)
   top#(ok(X)) -> top#(active(X))
  TRS:
   active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
   active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
   active(add(0(),X)) -> mark(X)
   active(add(s(X),Y)) -> mark(s(add(X,Y)))
   active(sel(0(),cons(X,XS))) -> mark(X)
   active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
   active(fib(X)) -> fib(active(X))
   active(sel(X1,X2)) -> sel(active(X1),X2)
   active(sel(X1,X2)) -> sel(X1,active(X2))
   active(fib1(X1,X2)) -> fib1(active(X1),X2)
   active(fib1(X1,X2)) -> fib1(X1,active(X2))
   active(s(X)) -> s(active(X))
   active(cons(X1,X2)) -> cons(active(X1),X2)
   active(add(X1,X2)) -> add(active(X1),X2)
   active(add(X1,X2)) -> add(X1,active(X2))
   fib(mark(X)) -> mark(fib(X))
   sel(mark(X1),X2) -> mark(sel(X1,X2))
   sel(X1,mark(X2)) -> mark(sel(X1,X2))
   fib1(mark(X1),X2) -> mark(fib1(X1,X2))
   fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
   s(mark(X)) -> mark(s(X))
   cons(mark(X1),X2) -> mark(cons(X1,X2))
   add(mark(X1),X2) -> mark(add(X1,X2))
   add(X1,mark(X2)) -> mark(add(X1,X2))
   proper(fib(X)) -> fib(proper(X))
   proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
   proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
   proper(s(X)) -> s(proper(X))
   proper(0()) -> ok(0())
   proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
   proper(add(X1,X2)) -> add(proper(X1),proper(X2))
   fib(ok(X)) -> ok(fib(X))
   sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
   fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
   s(ok(X)) -> ok(s(X))
   cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
   add(ok(X1),ok(X2)) -> ok(add(X1,X2))
   top(mark(X)) -> top(proper(X))
   top(ok(X)) -> top(active(X))
  EDG Processor:
   DPs:
    active#(fib(N)) -> s#(0())
    active#(fib(N)) -> fib1#(s(0()),s(0()))
    active#(fib(N)) -> sel#(N,fib1(s(0()),s(0())))
    active#(fib1(X,Y)) -> add#(X,Y)
    active#(fib1(X,Y)) -> fib1#(Y,add(X,Y))
    active#(fib1(X,Y)) -> cons#(X,fib1(Y,add(X,Y)))
    active#(add(s(X),Y)) -> add#(X,Y)
    active#(add(s(X),Y)) -> s#(add(X,Y))
    active#(sel(s(N),cons(X,XS))) -> sel#(N,XS)
    active#(fib(X)) -> active#(X)
    active#(fib(X)) -> fib#(active(X))
    active#(sel(X1,X2)) -> active#(X1)
    active#(sel(X1,X2)) -> sel#(active(X1),X2)
    active#(sel(X1,X2)) -> active#(X2)
    active#(sel(X1,X2)) -> sel#(X1,active(X2))
    active#(fib1(X1,X2)) -> active#(X1)
    active#(fib1(X1,X2)) -> fib1#(active(X1),X2)
    active#(fib1(X1,X2)) -> active#(X2)
    active#(fib1(X1,X2)) -> fib1#(X1,active(X2))
    active#(s(X)) -> active#(X)
    active#(s(X)) -> s#(active(X))
    active#(cons(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(add(X1,X2)) -> active#(X1)
    active#(add(X1,X2)) -> add#(active(X1),X2)
    active#(add(X1,X2)) -> active#(X2)
    active#(add(X1,X2)) -> add#(X1,active(X2))
    fib#(mark(X)) -> fib#(X)
    sel#(mark(X1),X2) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    fib1#(mark(X1),X2) -> fib1#(X1,X2)
    fib1#(X1,mark(X2)) -> fib1#(X1,X2)
    s#(mark(X)) -> s#(X)
    cons#(mark(X1),X2) -> cons#(X1,X2)
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2)
    proper#(fib(X)) -> proper#(X)
    proper#(fib(X)) -> fib#(proper(X))
    proper#(sel(X1,X2)) -> proper#(X2)
    proper#(sel(X1,X2)) -> proper#(X1)
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2))
    proper#(fib1(X1,X2)) -> proper#(X2)
    proper#(fib1(X1,X2)) -> proper#(X1)
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X)
    proper#(s(X)) -> s#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(add(X1,X2)) -> proper#(X2)
    proper#(add(X1,X2)) -> proper#(X1)
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
    fib#(ok(X)) -> fib#(X)
    sel#(ok(X1),ok(X2)) -> sel#(X1,X2)
    fib1#(ok(X1),ok(X2)) -> fib1#(X1,X2)
    s#(ok(X)) -> s#(X)
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    add#(ok(X1),ok(X2)) -> add#(X1,X2)
    top#(mark(X)) -> proper#(X)
    top#(mark(X)) -> top#(proper(X))
    top#(ok(X)) -> active#(X)
    top#(ok(X)) -> top#(active(X))
   TRS:
    active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
    active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
    active(add(0(),X)) -> mark(X)
    active(add(s(X),Y)) -> mark(s(add(X,Y)))
    active(sel(0(),cons(X,XS))) -> mark(X)
    active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
    active(fib(X)) -> fib(active(X))
    active(sel(X1,X2)) -> sel(active(X1),X2)
    active(sel(X1,X2)) -> sel(X1,active(X2))
    active(fib1(X1,X2)) -> fib1(active(X1),X2)
    active(fib1(X1,X2)) -> fib1(X1,active(X2))
    active(s(X)) -> s(active(X))
    active(cons(X1,X2)) -> cons(active(X1),X2)
    active(add(X1,X2)) -> add(active(X1),X2)
    active(add(X1,X2)) -> add(X1,active(X2))
    fib(mark(X)) -> mark(fib(X))
    sel(mark(X1),X2) -> mark(sel(X1,X2))
    sel(X1,mark(X2)) -> mark(sel(X1,X2))
    fib1(mark(X1),X2) -> mark(fib1(X1,X2))
    fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
    s(mark(X)) -> mark(s(X))
    cons(mark(X1),X2) -> mark(cons(X1,X2))
    add(mark(X1),X2) -> mark(add(X1,X2))
    add(X1,mark(X2)) -> mark(add(X1,X2))
    proper(fib(X)) -> fib(proper(X))
    proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
    proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
    proper(s(X)) -> s(proper(X))
    proper(0()) -> ok(0())
    proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
    proper(add(X1,X2)) -> add(proper(X1),proper(X2))
    fib(ok(X)) -> ok(fib(X))
    sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
    fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
    s(ok(X)) -> ok(s(X))
    cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    add(ok(X1),ok(X2)) -> ok(add(X1,X2))
    top(mark(X)) -> top(proper(X))
    top(ok(X)) -> top(active(X))
   graph:
    top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X)
    top#(ok(X)) -> top#(active(X)) ->
    top#(mark(X)) -> top#(proper(X))
    top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X)
    top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X))
    top#(ok(X)) -> active#(X) -> active#(fib(N)) -> s#(0())
    top#(ok(X)) -> active#(X) -> active#(fib(N)) -> fib1#(s(0()),s(0()))
    top#(ok(X)) -> active#(X) ->
    active#(fib(N)) -> sel#(N,fib1(s(0()),s(0())))
    top#(ok(X)) -> active#(X) -> active#(fib1(X,Y)) -> add#(X,Y)
    top#(ok(X)) -> active#(X) -> active#(fib1(X,Y)) -> fib1#(Y,add(X,Y))
    top#(ok(X)) -> active#(X) ->
    active#(fib1(X,Y)) -> cons#(X,fib1(Y,add(X,Y)))
    top#(ok(X)) -> active#(X) -> active#(add(s(X),Y)) -> add#(X,Y)
    top#(ok(X)) -> active#(X) -> active#(add(s(X),Y)) -> s#(add(X,Y))
    top#(ok(X)) -> active#(X) ->
    active#(sel(s(N),cons(X,XS))) -> sel#(N,XS)
    top#(ok(X)) -> active#(X) -> active#(fib(X)) -> active#(X)
    top#(ok(X)) -> active#(X) -> active#(fib(X)) -> fib#(active(X))
    top#(ok(X)) -> active#(X) -> active#(sel(X1,X2)) -> active#(X1)
    top#(ok(X)) -> active#(X) ->
    active#(sel(X1,X2)) -> sel#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(sel(X1,X2)) -> active#(X2)
    top#(ok(X)) -> active#(X) ->
    active#(sel(X1,X2)) -> sel#(X1,active(X2))
    top#(ok(X)) -> active#(X) -> active#(fib1(X1,X2)) -> active#(X1)
    top#(ok(X)) -> active#(X) ->
    active#(fib1(X1,X2)) -> fib1#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(fib1(X1,X2)) -> active#(X2)
    top#(ok(X)) -> active#(X) ->
    active#(fib1(X1,X2)) -> fib1#(X1,active(X2))
    top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    top#(ok(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
    top#(ok(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X1)
    top#(ok(X)) -> active#(X) ->
    active#(add(X1,X2)) -> add#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X2)
    top#(ok(X)) -> active#(X) ->
    active#(add(X1,X2)) -> add#(X1,active(X2))
    top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X)
    top#(mark(X)) -> top#(proper(X)) ->
    top#(mark(X)) -> top#(proper(X))
    top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X)
    top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> top#(active(X))
    top#(mark(X)) -> proper#(X) -> proper#(fib(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) -> proper#(fib(X)) -> fib#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(sel(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) -> proper#(sel(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) ->
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(fib1(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) -> proper#(fib1(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) ->
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) ->
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(fib(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(fib(X)) -> fib#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(sel(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(sel(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(fib1(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(fib1(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(add(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(add(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(fib(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(fib(X)) -> fib#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(sel(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(sel(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(fib1(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(fib1(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(add(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(add(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(fib(X)) -> proper#(X)
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(fib(X)) -> fib#(proper(X))
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(sel(X1,X2)) -> proper#(X2)
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(sel(X1,X2)) -> proper#(X1)
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2))
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(fib1(X1,X2)) -> proper#(X2)
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(fib1(X1,X2)) -> proper#(X1)
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2))
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(add(X1,X2)) -> proper#(X2)
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(add(X1,X2)) -> proper#(X1)
    proper#(add(X1,X2)) -> proper#(X2) ->
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(fib(X)) -> proper#(X)
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(fib(X)) -> fib#(proper(X))
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(sel(X1,X2)) -> proper#(X2)
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(sel(X1,X2)) -> proper#(X1)
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2))
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(fib1(X1,X2)) -> proper#(X2)
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(fib1(X1,X2)) -> proper#(X1)
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2))
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(add(X1,X2)) -> proper#(X2)
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(add(X1,X2)) -> proper#(X1)
    proper#(add(X1,X2)) -> proper#(X1) ->
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2)) ->
    add#(ok(X1),ok(X2)) -> add#(X1,X2)
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(fib(X)) -> proper#(X)
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(fib(X)) -> fib#(proper(X))
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(sel(X1,X2)) -> proper#(X2)
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(sel(X1,X2)) -> proper#(X1)
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2))
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(fib1(X1,X2)) -> proper#(X2)
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(fib1(X1,X2)) -> proper#(X1)
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2))
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(add(X1,X2)) -> proper#(X2)
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(add(X1,X2)) -> proper#(X1)
    proper#(sel(X1,X2)) -> proper#(X2) ->
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(fib(X)) -> proper#(X)
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(fib(X)) -> fib#(proper(X))
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(sel(X1,X2)) -> proper#(X2)
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(sel(X1,X2)) -> proper#(X1)
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2))
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(fib1(X1,X2)) -> proper#(X2)
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(fib1(X1,X2)) -> proper#(X1)
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2))
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(add(X1,X2)) -> proper#(X2)
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(add(X1,X2)) -> proper#(X1)
    proper#(sel(X1,X2)) -> proper#(X1) ->
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2)) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2)) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2)) ->
    sel#(ok(X1),ok(X2)) -> sel#(X1,X2)
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(fib(X)) -> proper#(X)
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(fib(X)) -> fib#(proper(X))
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(sel(X1,X2)) -> proper#(X2)
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(sel(X1,X2)) -> proper#(X1)
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2))
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(fib1(X1,X2)) -> proper#(X2)
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(fib1(X1,X2)) -> proper#(X1)
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2))
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(add(X1,X2)) -> proper#(X2)
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(add(X1,X2)) -> proper#(X1)
    proper#(fib1(X1,X2)) -> proper#(X2) ->
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(fib(X)) -> proper#(X)
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(fib(X)) -> fib#(proper(X))
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(sel(X1,X2)) -> proper#(X2)
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(sel(X1,X2)) -> proper#(X1)
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2))
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(fib1(X1,X2)) -> proper#(X2)
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(fib1(X1,X2)) -> proper#(X1)
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2))
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(add(X1,X2)) -> proper#(X2)
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(add(X1,X2)) -> proper#(X1)
    proper#(fib1(X1,X2)) -> proper#(X1) ->
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2)) ->
    fib1#(mark(X1),X2) -> fib1#(X1,X2)
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2)) ->
    fib1#(X1,mark(X2)) -> fib1#(X1,X2)
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2)) ->
    fib1#(ok(X1),ok(X2)) -> fib1#(X1,X2)
    proper#(s(X)) -> proper#(X) -> proper#(fib(X)) -> proper#(X)
    proper#(s(X)) -> proper#(X) -> proper#(fib(X)) -> fib#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(sel(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) -> proper#(sel(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) ->
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(fib1(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) -> proper#(fib1(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) ->
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) -> proper#(add(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) ->
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
    proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X)
    proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X)
    proper#(fib(X)) -> proper#(X) -> proper#(fib(X)) -> proper#(X)
    proper#(fib(X)) -> proper#(X) ->
    proper#(fib(X)) -> fib#(proper(X))
    proper#(fib(X)) -> proper#(X) ->
    proper#(sel(X1,X2)) -> proper#(X2)
    proper#(fib(X)) -> proper#(X) ->
    proper#(sel(X1,X2)) -> proper#(X1)
    proper#(fib(X)) -> proper#(X) ->
    proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2))
    proper#(fib(X)) -> proper#(X) ->
    proper#(fib1(X1,X2)) -> proper#(X2)
    proper#(fib(X)) -> proper#(X) ->
    proper#(fib1(X1,X2)) -> proper#(X1)
    proper#(fib(X)) -> proper#(X) ->
    proper#(fib1(X1,X2)) -> fib1#(proper(X1),proper(X2))
    proper#(fib(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    proper#(fib(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    proper#(fib(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(fib(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(fib(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(fib(X)) -> proper#(X) ->
    proper#(add(X1,X2)) -> proper#(X2)
    proper#(fib(X)) -> proper#(X) ->
    proper#(add(X1,X2)) -> proper#(X1)
    proper#(fib(X)) -> proper#(X) ->
    proper#(add(X1,X2)) -> add#(proper(X1),proper(X2))
    proper#(fib(X)) -> fib#(proper(X)) ->
    fib#(mark(X)) -> fib#(X)
    proper#(fib(X)) -> fib#(proper(X)) -> fib#(ok(X)) -> fib#(X)
    fib#(ok(X)) -> fib#(X) -> fib#(mark(X)) -> fib#(X)
    fib#(ok(X)) -> fib#(X) -> fib#(ok(X)) -> fib#(X)
    fib#(mark(X)) -> fib#(X) -> fib#(mark(X)) -> fib#(X)
    fib#(mark(X)) -> fib#(X) -> fib#(ok(X)) -> fib#(X)
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    add#(ok(X1),ok(X2)) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(ok(X1),ok(X2)) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(ok(X1),ok(X2)) -> add#(X1,X2) ->
    add#(ok(X1),ok(X2)) -> add#(X1,X2)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(ok(X1),ok(X2)) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(ok(X1),ok(X2)) -> add#(X1,X2)
    sel#(ok(X1),ok(X2)) -> sel#(X1,X2) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    sel#(ok(X1),ok(X2)) -> sel#(X1,X2) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    sel#(ok(X1),ok(X2)) -> sel#(X1,X2) ->
    sel#(ok(X1),ok(X2)) -> sel#(X1,X2)
    sel#(mark(X1),X2) -> sel#(X1,X2) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    sel#(mark(X1),X2) -> sel#(X1,X2) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    sel#(mark(X1),X2) -> sel#(X1,X2) ->
    sel#(ok(X1),ok(X2)) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    sel#(X1,mark(X2)) -> sel#(X1,X2) ->
    sel#(ok(X1),ok(X2)) -> sel#(X1,X2)
    fib1#(ok(X1),ok(X2)) -> fib1#(X1,X2) ->
    fib1#(mark(X1),X2) -> fib1#(X1,X2)
    fib1#(ok(X1),ok(X2)) -> fib1#(X1,X2) ->
    fib1#(X1,mark(X2)) -> fib1#(X1,X2)
    fib1#(ok(X1),ok(X2)) -> fib1#(X1,X2) ->
    fib1#(ok(X1),ok(X2)) -> fib1#(X1,X2)
    fib1#(mark(X1),X2) -> fib1#(X1,X2) ->
    fib1#(mark(X1),X2) -> fib1#(X1,X2)
    fib1#(mark(X1),X2) -> fib1#(X1,X2) ->
    fib1#(X1,mark(X2)) -> fib1#(X1,X2)
    fib1#(mark(X1),X2) -> fib1#(X1,X2) ->
    fib1#(ok(X1),ok(X2)) -> fib1#(X1,X2)
    fib1#(X1,mark(X2)) -> fib1#(X1,X2) ->
    fib1#(mark(X1),X2) -> fib1#(X1,X2)
    fib1#(X1,mark(X2)) -> fib1#(X1,X2) ->
    fib1#(X1,mark(X2)) -> fib1#(X1,X2)
    fib1#(X1,mark(X2)) -> fib1#(X1,X2) -> fib1#(ok(X1),ok(X2)) -> fib1#(X1,X2)
    s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
    active#(cons(X1,X2)) -> cons#(active(X1),X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(cons(X1,X2)) -> cons#(active(X1),X2) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(fib(N)) -> s#(0())
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(fib(N)) -> fib1#(s(0()),s(0()))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(fib(N)) -> sel#(N,fib1(s(0()),s(0())))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(fib1(X,Y)) -> add#(X,Y)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(fib1(X,Y)) -> fib1#(Y,add(X,Y))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(fib1(X,Y)) -> cons#(X,fib1(Y,add(X,Y)))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(sel(s(N),cons(X,XS))) -> sel#(N,XS)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(fib(X)) -> active#(X)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(fib(X)) -> fib#(active(X))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> sel#(active(X1),X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> active#(X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> sel#(X1,active(X2))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> fib1#(active(X1),X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> active#(X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> fib1#(X1,active(X2))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> add#(active(X1),X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> active#(X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> add#(X1,active(X2))
    active#(add(s(X),Y)) -> s#(add(X,Y)) ->
    s#(mark(X)) -> s#(X)
    active#(add(s(X),Y)) -> s#(add(X,Y)) ->
    s#(ok(X)) -> s#(X)
    active#(add(X1,X2)) -> add#(active(X1),X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    active#(add(X1,X2)) -> add#(active(X1),X2) ->
    add#(ok(X1),ok(X2)) -> add#(X1,X2)
    active#(add(X1,X2)) -> add#(X1,active(X2)) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    active#(add(X1,X2)) -> add#(X1,active(X2)) ->
    add#(ok(X1),ok(X2)) -> add#(X1,X2)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(fib(N)) -> s#(0())
    active#(add(X1,X2)) -> active#(X2) ->
    active#(fib(N)) -> fib1#(s(0()),s(0()))
    active#(add(X1,X2)) -> active#(X2) ->
    active#(fib(N)) -> sel#(N,fib1(s(0()),s(0())))
    active#(add(X1,X2)) -> active#(X2) ->
    active#(fib1(X,Y)) -> add#(X,Y)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(fib1(X,Y)) -> fib1#(Y,add(X,Y))
    active#(add(X1,X2)) -> active#(X2) ->
    active#(fib1(X,Y)) -> cons#(X,fib1(Y,add(X,Y)))
    active#(add(X1,X2)) -> active#(X2) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    active#(add(X1,X2)) -> active#(X2) ->
    active#(sel(s(N),cons(X,XS))) -> sel#(N,XS)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(fib(X)) -> active#(X)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(fib(X)) -> fib#(active(X))
    active#(add(X1,X2)) -> active#(X2) ->
    active#(sel(X1,X2)) -> active#(X1)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(sel(X1,X2)) -> sel#(active(X1),X2)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(sel(X1,X2)) -> active#(X2)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(sel(X1,X2)) -> sel#(X1,active(X2))
    active#(add(X1,X2)) -> active#(X2) ->
    active#(fib1(X1,X2)) -> active#(X1)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(fib1(X1,X2)) -> fib1#(active(X1),X2)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(fib1(X1,X2)) -> active#(X2)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(fib1(X1,X2)) -> fib1#(X1,active(X2))
    active#(add(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> active#(X)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> s#(active(X))
    active#(add(X1,X2)) -> active#(X2) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(add(X1,X2)) -> active#(X1)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(add(X1,X2)) -> add#(active(X1),X2)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(add(X1,X2)) -> active#(X2)
    active#(add(X1,X2)) -> active#(X2) ->
    active#(add(X1,X2)) -> add#(X1,active(X2))
    active#(add(X1,X2)) -> active#(X1) ->
    active#(fib(N)) -> s#(0())
    active#(add(X1,X2)) -> active#(X1) ->
    active#(fib(N)) -> fib1#(s(0()),s(0()))
    active#(add(X1,X2)) -> active#(X1) ->
    active#(fib(N)) -> sel#(N,fib1(s(0()),s(0())))
    active#(add(X1,X2)) -> active#(X1) ->
    active#(fib1(X,Y)) -> add#(X,Y)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(fib1(X,Y)) -> fib1#(Y,add(X,Y))
    active#(add(X1,X2)) -> active#(X1) ->
    active#(fib1(X,Y)) -> cons#(X,fib1(Y,add(X,Y)))
    active#(add(X1,X2)) -> active#(X1) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    active#(add(X1,X2)) -> active#(X1) ->
    active#(sel(s(N),cons(X,XS))) -> sel#(N,XS)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(fib(X)) -> active#(X)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(fib(X)) -> fib#(active(X))
    active#(add(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> active#(X1)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> sel#(active(X1),X2)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> active#(X2)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> sel#(X1,active(X2))
    active#(add(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> active#(X1)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> fib1#(active(X1),X2)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> active#(X2)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> fib1#(X1,active(X2))
    active#(add(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(add(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> active#(X1)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> add#(active(X1),X2)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> active#(X2)
    active#(add(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> add#(X1,active(X2))
    active#(sel(s(N),cons(X,XS))) -> sel#(N,XS) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    active#(sel(X1,X2)) -> sel#(active(X1),X2) ->
    sel#(mark(X1),X2) -> sel#(X1,X2)
    active#(sel(X1,X2)) -> sel#(active(X1),X2) ->
    sel#(ok(X1),ok(X2)) -> sel#(X1,X2)
    active#(sel(X1,X2)) -> sel#(X1,active(X2)) ->
    sel#(X1,mark(X2)) -> sel#(X1,X2)
    active#(sel(X1,X2)) -> sel#(X1,active(X2)) ->
    sel#(ok(X1),ok(X2)) -> sel#(X1,X2)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(fib(N)) -> s#(0())
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(fib(N)) -> fib1#(s(0()),s(0()))
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(fib(N)) -> sel#(N,fib1(s(0()),s(0())))
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(fib1(X,Y)) -> add#(X,Y)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(fib1(X,Y)) -> fib1#(Y,add(X,Y))
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(fib1(X,Y)) -> cons#(X,fib1(Y,add(X,Y)))
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(sel(s(N),cons(X,XS))) -> sel#(N,XS)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(fib(X)) -> active#(X)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(fib(X)) -> fib#(active(X))
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(sel(X1,X2)) -> active#(X1)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(sel(X1,X2)) -> sel#(active(X1),X2)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(sel(X1,X2)) -> active#(X2)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(sel(X1,X2)) -> sel#(X1,active(X2))
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(fib1(X1,X2)) -> active#(X1)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(fib1(X1,X2)) -> fib1#(active(X1),X2)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(fib1(X1,X2)) -> active#(X2)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(fib1(X1,X2)) -> fib1#(X1,active(X2))
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> active#(X)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> s#(active(X))
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(add(X1,X2)) -> active#(X1)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(add(X1,X2)) -> add#(active(X1),X2)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(add(X1,X2)) -> active#(X2)
    active#(sel(X1,X2)) -> active#(X2) ->
    active#(add(X1,X2)) -> add#(X1,active(X2))
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(fib(N)) -> s#(0())
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(fib(N)) -> fib1#(s(0()),s(0()))
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(fib(N)) -> sel#(N,fib1(s(0()),s(0())))
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(fib1(X,Y)) -> add#(X,Y)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(fib1(X,Y)) -> fib1#(Y,add(X,Y))
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(fib1(X,Y)) -> cons#(X,fib1(Y,add(X,Y)))
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(sel(s(N),cons(X,XS))) -> sel#(N,XS)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(fib(X)) -> active#(X)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(fib(X)) -> fib#(active(X))
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> active#(X1)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> sel#(active(X1),X2)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> active#(X2)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> sel#(X1,active(X2))
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> active#(X1)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> fib1#(active(X1),X2)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> active#(X2)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> fib1#(X1,active(X2))
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> active#(X1)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> add#(active(X1),X2)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> active#(X2)
    active#(sel(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> add#(X1,active(X2))
    active#(fib1(X1,X2)) -> fib1#(active(X1),X2) ->
    fib1#(mark(X1),X2) -> fib1#(X1,X2)
    active#(fib1(X1,X2)) -> fib1#(active(X1),X2) ->
    fib1#(ok(X1),ok(X2)) -> fib1#(X1,X2)
    active#(fib1(X1,X2)) -> fib1#(X1,active(X2)) ->
    fib1#(X1,mark(X2)) -> fib1#(X1,X2)
    active#(fib1(X1,X2)) -> fib1#(X1,active(X2)) ->
    fib1#(ok(X1),ok(X2)) -> fib1#(X1,X2)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(fib(N)) -> s#(0())
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(fib(N)) -> fib1#(s(0()),s(0()))
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(fib(N)) -> sel#(N,fib1(s(0()),s(0())))
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(fib1(X,Y)) -> add#(X,Y)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(fib1(X,Y)) -> fib1#(Y,add(X,Y))
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(fib1(X,Y)) -> cons#(X,fib1(Y,add(X,Y)))
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(sel(s(N),cons(X,XS))) -> sel#(N,XS)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(fib(X)) -> active#(X)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(fib(X)) -> fib#(active(X))
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(sel(X1,X2)) -> active#(X1)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(sel(X1,X2)) -> sel#(active(X1),X2)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(sel(X1,X2)) -> active#(X2)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(sel(X1,X2)) -> sel#(X1,active(X2))
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(fib1(X1,X2)) -> active#(X1)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(fib1(X1,X2)) -> fib1#(active(X1),X2)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(fib1(X1,X2)) -> active#(X2)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(fib1(X1,X2)) -> fib1#(X1,active(X2))
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> active#(X)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(s(X)) -> s#(active(X))
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(add(X1,X2)) -> active#(X1)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(add(X1,X2)) -> add#(active(X1),X2)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(add(X1,X2)) -> active#(X2)
    active#(fib1(X1,X2)) -> active#(X2) ->
    active#(add(X1,X2)) -> add#(X1,active(X2))
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(fib(N)) -> s#(0())
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(fib(N)) -> fib1#(s(0()),s(0()))
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(fib(N)) -> sel#(N,fib1(s(0()),s(0())))
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(fib1(X,Y)) -> add#(X,Y)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(fib1(X,Y)) -> fib1#(Y,add(X,Y))
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(fib1(X,Y)) -> cons#(X,fib1(Y,add(X,Y)))
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(sel(s(N),cons(X,XS))) -> sel#(N,XS)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(fib(X)) -> active#(X)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(fib(X)) -> fib#(active(X))
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> active#(X1)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> sel#(active(X1),X2)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> active#(X2)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(sel(X1,X2)) -> sel#(X1,active(X2))
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> active#(X1)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> fib1#(active(X1),X2)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> active#(X2)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(fib1(X1,X2)) -> fib1#(X1,active(X2))
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> active#(X1)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> add#(active(X1),X2)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> active#(X2)
    active#(fib1(X1,X2)) -> active#(X1) ->
    active#(add(X1,X2)) -> add#(X1,active(X2))
    active#(fib1(X,Y)) -> cons#(X,fib1(Y,add(X,Y))) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    active#(fib1(X,Y)) -> fib1#(Y,add(X,Y)) ->
    fib1#(X1,mark(X2)) -> fib1#(X1,X2)
    active#(fib1(X,Y)) -> fib1#(Y,add(X,Y)) ->
    fib1#(ok(X1),ok(X2)) -> fib1#(X1,X2)
    active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X)
    active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X)
    active#(s(X)) -> active#(X) -> active#(fib(N)) -> s#(0())
    active#(s(X)) -> active#(X) ->
    active#(fib(N)) -> fib1#(s(0()),s(0()))
    active#(s(X)) -> active#(X) ->
    active#(fib(N)) -> sel#(N,fib1(s(0()),s(0())))
    active#(s(X)) -> active#(X) -> active#(fib1(X,Y)) -> add#(X,Y)
    active#(s(X)) -> active#(X) ->
    active#(fib1(X,Y)) -> fib1#(Y,add(X,Y))
    active#(s(X)) -> active#(X) ->
    active#(fib1(X,Y)) -> cons#(X,fib1(Y,add(X,Y)))
    active#(s(X)) -> active#(X) -> active#(add(s(X),Y)) -> add#(X,Y)
    active#(s(X)) -> active#(X) -> active#(add(s(X),Y)) -> s#(add(X,Y))
    active#(s(X)) -> active#(X) ->
    active#(sel(s(N),cons(X,XS))) -> sel#(N,XS)
    active#(s(X)) -> active#(X) -> active#(fib(X)) -> active#(X)
    active#(s(X)) -> active#(X) -> active#(fib(X)) -> fib#(active(X))
    active#(s(X)) -> active#(X) -> active#(sel(X1,X2)) -> active#(X1)
    active#(s(X)) -> active#(X) ->
    active#(sel(X1,X2)) -> sel#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(sel(X1,X2)) -> active#(X2)
    active#(s(X)) -> active#(X) ->
    active#(sel(X1,X2)) -> sel#(X1,active(X2))
    active#(s(X)) -> active#(X) -> active#(fib1(X1,X2)) -> active#(X1)
    active#(s(X)) -> active#(X) ->
    active#(fib1(X1,X2)) -> fib1#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(fib1(X1,X2)) -> active#(X2)
    active#(s(X)) -> active#(X) ->
    active#(fib1(X1,X2)) -> fib1#(X1,active(X2))
    active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    active#(s(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
    active#(s(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X1)
    active#(s(X)) -> active#(X) ->
    active#(add(X1,X2)) -> add#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(add(X1,X2)) -> active#(X2)
    active#(s(X)) -> active#(X) ->
    active#(add(X1,X2)) -> add#(X1,active(X2))
    active#(fib(X)) -> fib#(active(X)) ->
    fib#(mark(X)) -> fib#(X)
    active#(fib(X)) -> fib#(active(X)) -> fib#(ok(X)) -> fib#(X)
    active#(fib(X)) -> active#(X) -> active#(fib(N)) -> s#(0())
    active#(fib(X)) -> active#(X) ->
    active#(fib(N)) -> fib1#(s(0()),s(0()))
    active#(fib(X)) -> active#(X) ->
    active#(fib(N)) -> sel#(N,fib1(s(0()),s(0())))
    active#(fib(X)) -> active#(X) -> active#(fib1(X,Y)) -> add#(X,Y)
    active#(fib(X)) -> active#(X) ->
    active#(fib1(X,Y)) -> fib1#(Y,add(X,Y))
    active#(fib(X)) -> active#(X) ->
    active#(fib1(X,Y)) -> cons#(X,fib1(Y,add(X,Y)))
    active#(fib(X)) -> active#(X) -> active#(add(s(X),Y)) -> add#(X,Y)
    active#(fib(X)) -> active#(X) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    active#(fib(X)) -> active#(X) ->
    active#(sel(s(N),cons(X,XS))) -> sel#(N,XS)
    active#(fib(X)) -> active#(X) -> active#(fib(X)) -> active#(X)
    active#(fib(X)) -> active#(X) ->
    active#(fib(X)) -> fib#(active(X))
    active#(fib(X)) -> active#(X) ->
    active#(sel(X1,X2)) -> active#(X1)
    active#(fib(X)) -> active#(X) ->
    active#(sel(X1,X2)) -> sel#(active(X1),X2)
    active#(fib(X)) -> active#(X) ->
    active#(sel(X1,X2)) -> active#(X2)
    active#(fib(X)) -> active#(X) ->
    active#(sel(X1,X2)) -> sel#(X1,active(X2))
    active#(fib(X)) -> active#(X) ->
    active#(fib1(X1,X2)) -> active#(X1)
    active#(fib(X)) -> active#(X) ->
    active#(fib1(X1,X2)) -> fib1#(active(X1),X2)
    active#(fib(X)) -> active#(X) ->
    active#(fib1(X1,X2)) -> active#(X2)
    active#(fib(X)) -> active#(X) ->
    active#(fib1(X1,X2)) -> fib1#(X1,active(X2))
    active#(fib(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    active#(fib(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    active#(fib(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(fib(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(fib(X)) -> active#(X) ->
    active#(add(X1,X2)) -> active#(X1)
    active#(fib(X)) -> active#(X) ->
    active#(add(X1,X2)) -> add#(active(X1),X2)
    active#(fib(X)) -> active#(X) ->
    active#(add(X1,X2)) -> active#(X2)
    active#(fib(X)) -> active#(X) -> active#(add(X1,X2)) -> add#(X1,active(X2))
   SCC Processor:
    #sccs: 9
    #rules: 36
    #arcs: 532/3844
    DPs:
     top#(ok(X)) -> top#(active(X))
     top#(mark(X)) -> top#(proper(X))
    TRS:
     active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
     active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(sel(0(),cons(X,XS))) -> mark(X)
     active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
     active(fib(X)) -> fib(active(X))
     active(sel(X1,X2)) -> sel(active(X1),X2)
     active(sel(X1,X2)) -> sel(X1,active(X2))
     active(fib1(X1,X2)) -> fib1(active(X1),X2)
     active(fib1(X1,X2)) -> fib1(X1,active(X2))
     active(s(X)) -> s(active(X))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(add(X1,X2)) -> add(active(X1),X2)
     active(add(X1,X2)) -> add(X1,active(X2))
     fib(mark(X)) -> mark(fib(X))
     sel(mark(X1),X2) -> mark(sel(X1,X2))
     sel(X1,mark(X2)) -> mark(sel(X1,X2))
     fib1(mark(X1),X2) -> mark(fib1(X1,X2))
     fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
     s(mark(X)) -> mark(s(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     add(mark(X1),X2) -> mark(add(X1,X2))
     add(X1,mark(X2)) -> mark(add(X1,X2))
     proper(fib(X)) -> fib(proper(X))
     proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
     proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
     proper(s(X)) -> s(proper(X))
     proper(0()) -> ok(0())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(add(X1,X2)) -> add(proper(X1),proper(X2))
     fib(ok(X)) -> ok(fib(X))
     sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
     fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
     s(ok(X)) -> ok(s(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     add(ok(X1),ok(X2)) -> ok(add(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     proper#(add(X1,X2)) -> proper#(X1)
     proper#(add(X1,X2)) -> proper#(X2)
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(s(X)) -> proper#(X)
     proper#(fib1(X1,X2)) -> proper#(X1)
     proper#(fib1(X1,X2)) -> proper#(X2)
     proper#(sel(X1,X2)) -> proper#(X1)
     proper#(sel(X1,X2)) -> proper#(X2)
     proper#(fib(X)) -> proper#(X)
    TRS:
     active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
     active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(sel(0(),cons(X,XS))) -> mark(X)
     active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
     active(fib(X)) -> fib(active(X))
     active(sel(X1,X2)) -> sel(active(X1),X2)
     active(sel(X1,X2)) -> sel(X1,active(X2))
     active(fib1(X1,X2)) -> fib1(active(X1),X2)
     active(fib1(X1,X2)) -> fib1(X1,active(X2))
     active(s(X)) -> s(active(X))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(add(X1,X2)) -> add(active(X1),X2)
     active(add(X1,X2)) -> add(X1,active(X2))
     fib(mark(X)) -> mark(fib(X))
     sel(mark(X1),X2) -> mark(sel(X1,X2))
     sel(X1,mark(X2)) -> mark(sel(X1,X2))
     fib1(mark(X1),X2) -> mark(fib1(X1,X2))
     fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
     s(mark(X)) -> mark(s(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     add(mark(X1),X2) -> mark(add(X1,X2))
     add(X1,mark(X2)) -> mark(add(X1,X2))
     proper(fib(X)) -> fib(proper(X))
     proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
     proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
     proper(s(X)) -> s(proper(X))
     proper(0()) -> ok(0())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(add(X1,X2)) -> add(proper(X1),proper(X2))
     fib(ok(X)) -> ok(fib(X))
     sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
     fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
     s(ok(X)) -> ok(s(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     add(ok(X1),ok(X2)) -> ok(add(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [proper#](x0) = x0 + 1,
      
      [top](x0) = 0,
      
      [ok](x0) = 0,
      
      [proper](x0) = x0,
      
      [cons](x0, x1) = x0 + x1 + 1,
      
      [add](x0, x1) = x0 + x1 + 1,
      
      [mark](x0) = 0,
      
      [sel](x0, x1) = x0 + x1,
      
      [fib1](x0, x1) = x0 + x1,
      
      [s](x0) = x0 + 1,
      
      [0] = 0,
      
      [active](x0) = x0 + 1,
      
      [fib](x0) = x0
     orientation:
      proper#(add(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1)
      
      proper#(add(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2)
      
      proper#(cons(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1)
      
      proper#(cons(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2)
      
      proper#(s(X)) = X + 2 >= X + 1 = proper#(X)
      
      proper#(fib1(X1,X2)) = X1 + X2 + 1 >= X1 + 1 = proper#(X1)
      
      proper#(fib1(X1,X2)) = X1 + X2 + 1 >= X2 + 1 = proper#(X2)
      
      proper#(sel(X1,X2)) = X1 + X2 + 1 >= X1 + 1 = proper#(X1)
      
      proper#(sel(X1,X2)) = X1 + X2 + 1 >= X2 + 1 = proper#(X2)
      
      proper#(fib(X)) = X + 1 >= X + 1 = proper#(X)
      
      active(fib(N)) = N + 1 >= 0 = mark(sel(N,fib1(s(0()),s(0()))))
      
      active(fib1(X,Y)) = X + Y + 1 >= 0 = mark(cons(X,fib1(Y,add(X,Y))))
      
      active(add(0(),X)) = X + 2 >= 0 = mark(X)
      
      active(add(s(X),Y)) = X + Y + 3 >= 0 = mark(s(add(X,Y)))
      
      active(sel(0(),cons(X,XS))) = X + XS + 2 >= 0 = mark(X)
      
      active(sel(s(N),cons(X,XS))) = N + X + XS + 3 >= 0 = mark(sel(N,XS))
      
      active(fib(X)) = X + 1 >= X + 1 = fib(active(X))
      
      active(sel(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = sel(active(X1),X2)
      
      active(sel(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = sel(X1,active(X2))
      
      active(fib1(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = fib1(active(X1),X2)
      
      active(fib1(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = fib1(X1,active(X2))
      
      active(s(X)) = X + 2 >= X + 2 = s(active(X))
      
      active(cons(X1,X2)) = X1 + X2 + 2 >= X1 + X2 + 2 = cons(active(X1),X2)
      
      active(add(X1,X2)) = X1 + X2 + 2 >= X1 + X2 + 2 = add(active(X1),X2)
      
      active(add(X1,X2)) = X1 + X2 + 2 >= X1 + X2 + 2 = add(X1,active(X2))
      
      fib(mark(X)) = 0 >= 0 = mark(fib(X))
      
      sel(mark(X1),X2) = X2 >= 0 = mark(sel(X1,X2))
      
      sel(X1,mark(X2)) = X1 >= 0 = mark(sel(X1,X2))
      
      fib1(mark(X1),X2) = X2 >= 0 = mark(fib1(X1,X2))
      
      fib1(X1,mark(X2)) = X1 >= 0 = mark(fib1(X1,X2))
      
      s(mark(X)) = 1 >= 0 = mark(s(X))
      
      cons(mark(X1),X2) = X2 + 1 >= 0 = mark(cons(X1,X2))
      
      add(mark(X1),X2) = X2 + 1 >= 0 = mark(add(X1,X2))
      
      add(X1,mark(X2)) = X1 + 1 >= 0 = mark(add(X1,X2))
      
      proper(fib(X)) = X >= X = fib(proper(X))
      
      proper(sel(X1,X2)) = X1 + X2 >= X1 + X2 = sel(proper(X1),proper(X2))
      
      proper(fib1(X1,X2)) = X1 + X2 >= X1 + X2 = fib1(proper(X1),proper(X2))
      
      proper(s(X)) = X + 1 >= X + 1 = s(proper(X))
      
      proper(0()) = 0 >= 0 = ok(0())
      
      proper(cons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = cons(proper(X1),proper(X2))
      
      proper(add(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = add(proper(X1),proper(X2))
      
      fib(ok(X)) = 0 >= 0 = ok(fib(X))
      
      sel(ok(X1),ok(X2)) = 0 >= 0 = ok(sel(X1,X2))
      
      fib1(ok(X1),ok(X2)) = 0 >= 0 = ok(fib1(X1,X2))
      
      s(ok(X)) = 1 >= 0 = ok(s(X))
      
      cons(ok(X1),ok(X2)) = 1 >= 0 = ok(cons(X1,X2))
      
      add(ok(X1),ok(X2)) = 1 >= 0 = ok(add(X1,X2))
      
      top(mark(X)) = 0 >= 0 = top(proper(X))
      
      top(ok(X)) = 0 >= 0 = top(active(X))
     problem:
      DPs:
       proper#(fib1(X1,X2)) -> proper#(X1)
       proper#(fib1(X1,X2)) -> proper#(X2)
       proper#(sel(X1,X2)) -> proper#(X1)
       proper#(sel(X1,X2)) -> proper#(X2)
       proper#(fib(X)) -> proper#(X)
      TRS:
       active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
       active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(sel(0(),cons(X,XS))) -> mark(X)
       active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
       active(fib(X)) -> fib(active(X))
       active(sel(X1,X2)) -> sel(active(X1),X2)
       active(sel(X1,X2)) -> sel(X1,active(X2))
       active(fib1(X1,X2)) -> fib1(active(X1),X2)
       active(fib1(X1,X2)) -> fib1(X1,active(X2))
       active(s(X)) -> s(active(X))
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(add(X1,X2)) -> add(active(X1),X2)
       active(add(X1,X2)) -> add(X1,active(X2))
       fib(mark(X)) -> mark(fib(X))
       sel(mark(X1),X2) -> mark(sel(X1,X2))
       sel(X1,mark(X2)) -> mark(sel(X1,X2))
       fib1(mark(X1),X2) -> mark(fib1(X1,X2))
       fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
       s(mark(X)) -> mark(s(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       add(mark(X1),X2) -> mark(add(X1,X2))
       add(X1,mark(X2)) -> mark(add(X1,X2))
       proper(fib(X)) -> fib(proper(X))
       proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
       proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
       proper(s(X)) -> s(proper(X))
       proper(0()) -> ok(0())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(add(X1,X2)) -> add(proper(X1),proper(X2))
       fib(ok(X)) -> ok(fib(X))
       sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
       fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
       s(ok(X)) -> ok(s(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       add(ok(X1),ok(X2)) -> ok(add(X1,X2))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [proper#](x0) = x0 + 1,
       
       [top](x0) = 0,
       
       [ok](x0) = x0,
       
       [proper](x0) = x0,
       
       [cons](x0, x1) = x1 + 1,
       
       [add](x0, x1) = x1 + 1,
       
       [mark](x0) = 0,
       
       [sel](x0, x1) = x0 + x1 + 1,
       
       [fib1](x0, x1) = x0 + x1 + 1,
       
       [s](x0) = 0,
       
       [0] = 1,
       
       [active](x0) = x0,
       
       [fib](x0) = x0
      orientation:
       proper#(fib1(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1)
       
       proper#(fib1(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2)
       
       proper#(sel(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = proper#(X1)
       
       proper#(sel(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = proper#(X2)
       
       proper#(fib(X)) = X + 1 >= X + 1 = proper#(X)
       
       active(fib(N)) = N >= 0 = mark(sel(N,fib1(s(0()),s(0()))))
       
       active(fib1(X,Y)) = X + Y + 1 >= 0 = mark(cons(X,fib1(Y,add(X,Y))))
       
       active(add(0(),X)) = X + 1 >= 0 = mark(X)
       
       active(add(s(X),Y)) = Y + 1 >= 0 = mark(s(add(X,Y)))
       
       active(sel(0(),cons(X,XS))) = XS + 3 >= 0 = mark(X)
       
       active(sel(s(N),cons(X,XS))) = XS + 2 >= 0 = mark(sel(N,XS))
       
       active(fib(X)) = X >= X = fib(active(X))
       
       active(sel(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = sel(active(X1),X2)
       
       active(sel(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = sel(X1,active(X2))
       
       active(fib1(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = fib1(active(X1),X2)
       
       active(fib1(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = fib1(X1,active(X2))
       
       active(s(X)) = 0 >= 0 = s(active(X))
       
       active(cons(X1,X2)) = X2 + 1 >= X2 + 1 = cons(active(X1),X2)
       
       active(add(X1,X2)) = X2 + 1 >= X2 + 1 = add(active(X1),X2)
       
       active(add(X1,X2)) = X2 + 1 >= X2 + 1 = add(X1,active(X2))
       
       fib(mark(X)) = 0 >= 0 = mark(fib(X))
       
       sel(mark(X1),X2) = X2 + 1 >= 0 = mark(sel(X1,X2))
       
       sel(X1,mark(X2)) = X1 + 1 >= 0 = mark(sel(X1,X2))
       
       fib1(mark(X1),X2) = X2 + 1 >= 0 = mark(fib1(X1,X2))
       
       fib1(X1,mark(X2)) = X1 + 1 >= 0 = mark(fib1(X1,X2))
       
       s(mark(X)) = 0 >= 0 = mark(s(X))
       
       cons(mark(X1),X2) = X2 + 1 >= 0 = mark(cons(X1,X2))
       
       add(mark(X1),X2) = X2 + 1 >= 0 = mark(add(X1,X2))
       
       add(X1,mark(X2)) = 1 >= 0 = mark(add(X1,X2))
       
       proper(fib(X)) = X >= X = fib(proper(X))
       
       proper(sel(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = sel(proper(X1),proper(X2))
       
       proper(fib1(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = fib1(proper(X1),proper(X2))
       
       proper(s(X)) = 0 >= 0 = s(proper(X))
       
       proper(0()) = 1 >= 1 = ok(0())
       
       proper(cons(X1,X2)) = X2 + 1 >= X2 + 1 = cons(proper(X1),proper(X2))
       
       proper(add(X1,X2)) = X2 + 1 >= X2 + 1 = add(proper(X1),proper(X2))
       
       fib(ok(X)) = X >= X = ok(fib(X))
       
       sel(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(sel(X1,X2))
       
       fib1(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(fib1(X1,X2))
       
       s(ok(X)) = 0 >= 0 = ok(s(X))
       
       cons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(cons(X1,X2))
       
       add(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(add(X1,X2))
       
       top(mark(X)) = 0 >= 0 = top(proper(X))
       
       top(ok(X)) = 0 >= 0 = top(active(X))
      problem:
       DPs:
        proper#(fib(X)) -> proper#(X)
       TRS:
        active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
        active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(sel(0(),cons(X,XS))) -> mark(X)
        active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
        active(fib(X)) -> fib(active(X))
        active(sel(X1,X2)) -> sel(active(X1),X2)
        active(sel(X1,X2)) -> sel(X1,active(X2))
        active(fib1(X1,X2)) -> fib1(active(X1),X2)
        active(fib1(X1,X2)) -> fib1(X1,active(X2))
        active(s(X)) -> s(active(X))
        active(cons(X1,X2)) -> cons(active(X1),X2)
        active(add(X1,X2)) -> add(active(X1),X2)
        active(add(X1,X2)) -> add(X1,active(X2))
        fib(mark(X)) -> mark(fib(X))
        sel(mark(X1),X2) -> mark(sel(X1,X2))
        sel(X1,mark(X2)) -> mark(sel(X1,X2))
        fib1(mark(X1),X2) -> mark(fib1(X1,X2))
        fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
        s(mark(X)) -> mark(s(X))
        cons(mark(X1),X2) -> mark(cons(X1,X2))
        add(mark(X1),X2) -> mark(add(X1,X2))
        add(X1,mark(X2)) -> mark(add(X1,X2))
        proper(fib(X)) -> fib(proper(X))
        proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
        proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
        proper(s(X)) -> s(proper(X))
        proper(0()) -> ok(0())
        proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
        proper(add(X1,X2)) -> add(proper(X1),proper(X2))
        fib(ok(X)) -> ok(fib(X))
        sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
        fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
        s(ok(X)) -> ok(s(X))
        cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
        add(ok(X1),ok(X2)) -> ok(add(X1,X2))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [proper#](x0) = x0 + 1,
        
        [top](x0) = 1,
        
        [ok](x0) = 0,
        
        [proper](x0) = x0,
        
        [cons](x0, x1) = 0,
        
        [add](x0, x1) = x0 + x1 + 1,
        
        [mark](x0) = 0,
        
        [sel](x0, x1) = 1,
        
        [fib1](x0, x1) = 0,
        
        [s](x0) = 1,
        
        [0] = 0,
        
        [active](x0) = x0,
        
        [fib](x0) = x0 + 1
       orientation:
        proper#(fib(X)) = X + 2 >= X + 1 = proper#(X)
        
        active(fib(N)) = N + 1 >= 0 = mark(sel(N,fib1(s(0()),s(0()))))
        
        active(fib1(X,Y)) = 0 >= 0 = mark(cons(X,fib1(Y,add(X,Y))))
        
        active(add(0(),X)) = X + 1 >= 0 = mark(X)
        
        active(add(s(X),Y)) = Y + 2 >= 0 = mark(s(add(X,Y)))
        
        active(sel(0(),cons(X,XS))) = 1 >= 0 = mark(X)
        
        active(sel(s(N),cons(X,XS))) = 1 >= 0 = mark(sel(N,XS))
        
        active(fib(X)) = X + 1 >= X + 1 = fib(active(X))
        
        active(sel(X1,X2)) = 1 >= 1 = sel(active(X1),X2)
        
        active(sel(X1,X2)) = 1 >= 1 = sel(X1,active(X2))
        
        active(fib1(X1,X2)) = 0 >= 0 = fib1(active(X1),X2)
        
        active(fib1(X1,X2)) = 0 >= 0 = fib1(X1,active(X2))
        
        active(s(X)) = 1 >= 1 = s(active(X))
        
        active(cons(X1,X2)) = 0 >= 0 = cons(active(X1),X2)
        
        active(add(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = add(active(X1),X2)
        
        active(add(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = add(X1,active(X2))
        
        fib(mark(X)) = 1 >= 0 = mark(fib(X))
        
        sel(mark(X1),X2) = 1 >= 0 = mark(sel(X1,X2))
        
        sel(X1,mark(X2)) = 1 >= 0 = mark(sel(X1,X2))
        
        fib1(mark(X1),X2) = 0 >= 0 = mark(fib1(X1,X2))
        
        fib1(X1,mark(X2)) = 0 >= 0 = mark(fib1(X1,X2))
        
        s(mark(X)) = 1 >= 0 = mark(s(X))
        
        cons(mark(X1),X2) = 0 >= 0 = mark(cons(X1,X2))
        
        add(mark(X1),X2) = X2 + 1 >= 0 = mark(add(X1,X2))
        
        add(X1,mark(X2)) = X1 + 1 >= 0 = mark(add(X1,X2))
        
        proper(fib(X)) = X + 1 >= X + 1 = fib(proper(X))
        
        proper(sel(X1,X2)) = 1 >= 1 = sel(proper(X1),proper(X2))
        
        proper(fib1(X1,X2)) = 0 >= 0 = fib1(proper(X1),proper(X2))
        
        proper(s(X)) = 1 >= 1 = s(proper(X))
        
        proper(0()) = 0 >= 0 = ok(0())
        
        proper(cons(X1,X2)) = 0 >= 0 = cons(proper(X1),proper(X2))
        
        proper(add(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = add(proper(X1),proper(X2))
        
        fib(ok(X)) = 1 >= 0 = ok(fib(X))
        
        sel(ok(X1),ok(X2)) = 1 >= 0 = ok(sel(X1,X2))
        
        fib1(ok(X1),ok(X2)) = 0 >= 0 = ok(fib1(X1,X2))
        
        s(ok(X)) = 1 >= 0 = ok(s(X))
        
        cons(ok(X1),ok(X2)) = 0 >= 0 = ok(cons(X1,X2))
        
        add(ok(X1),ok(X2)) = 1 >= 0 = ok(add(X1,X2))
        
        top(mark(X)) = 1 >= 1 = top(proper(X))
        
        top(ok(X)) = 1 >= 1 = top(active(X))
       problem:
        DPs:
         
        TRS:
         active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
         active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
         active(add(0(),X)) -> mark(X)
         active(add(s(X),Y)) -> mark(s(add(X,Y)))
         active(sel(0(),cons(X,XS))) -> mark(X)
         active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
         active(fib(X)) -> fib(active(X))
         active(sel(X1,X2)) -> sel(active(X1),X2)
         active(sel(X1,X2)) -> sel(X1,active(X2))
         active(fib1(X1,X2)) -> fib1(active(X1),X2)
         active(fib1(X1,X2)) -> fib1(X1,active(X2))
         active(s(X)) -> s(active(X))
         active(cons(X1,X2)) -> cons(active(X1),X2)
         active(add(X1,X2)) -> add(active(X1),X2)
         active(add(X1,X2)) -> add(X1,active(X2))
         fib(mark(X)) -> mark(fib(X))
         sel(mark(X1),X2) -> mark(sel(X1,X2))
         sel(X1,mark(X2)) -> mark(sel(X1,X2))
         fib1(mark(X1),X2) -> mark(fib1(X1,X2))
         fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
         s(mark(X)) -> mark(s(X))
         cons(mark(X1),X2) -> mark(cons(X1,X2))
         add(mark(X1),X2) -> mark(add(X1,X2))
         add(X1,mark(X2)) -> mark(add(X1,X2))
         proper(fib(X)) -> fib(proper(X))
         proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
         proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
         proper(s(X)) -> s(proper(X))
         proper(0()) -> ok(0())
         proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
         proper(add(X1,X2)) -> add(proper(X1),proper(X2))
         fib(ok(X)) -> ok(fib(X))
         sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
         fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
         s(ok(X)) -> ok(s(X))
         cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
         add(ok(X1),ok(X2)) -> ok(add(X1,X2))
         top(mark(X)) -> top(proper(X))
         top(ok(X)) -> top(active(X))
       Qed
    
    DPs:
     active#(add(X1,X2)) -> active#(X2)
     active#(add(X1,X2)) -> active#(X1)
     active#(cons(X1,X2)) -> active#(X1)
     active#(s(X)) -> active#(X)
     active#(fib1(X1,X2)) -> active#(X2)
     active#(fib1(X1,X2)) -> active#(X1)
     active#(sel(X1,X2)) -> active#(X2)
     active#(sel(X1,X2)) -> active#(X1)
     active#(fib(X)) -> active#(X)
    TRS:
     active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
     active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(sel(0(),cons(X,XS))) -> mark(X)
     active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
     active(fib(X)) -> fib(active(X))
     active(sel(X1,X2)) -> sel(active(X1),X2)
     active(sel(X1,X2)) -> sel(X1,active(X2))
     active(fib1(X1,X2)) -> fib1(active(X1),X2)
     active(fib1(X1,X2)) -> fib1(X1,active(X2))
     active(s(X)) -> s(active(X))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(add(X1,X2)) -> add(active(X1),X2)
     active(add(X1,X2)) -> add(X1,active(X2))
     fib(mark(X)) -> mark(fib(X))
     sel(mark(X1),X2) -> mark(sel(X1,X2))
     sel(X1,mark(X2)) -> mark(sel(X1,X2))
     fib1(mark(X1),X2) -> mark(fib1(X1,X2))
     fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
     s(mark(X)) -> mark(s(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     add(mark(X1),X2) -> mark(add(X1,X2))
     add(X1,mark(X2)) -> mark(add(X1,X2))
     proper(fib(X)) -> fib(proper(X))
     proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
     proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
     proper(s(X)) -> s(proper(X))
     proper(0()) -> ok(0())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(add(X1,X2)) -> add(proper(X1),proper(X2))
     fib(ok(X)) -> ok(fib(X))
     sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
     fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
     s(ok(X)) -> ok(s(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     add(ok(X1),ok(X2)) -> ok(add(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [active#](x0) = x0 + 1,
      
      [top](x0) = 0,
      
      [ok](x0) = 0,
      
      [proper](x0) = x0,
      
      [cons](x0, x1) = x0 + x1,
      
      [add](x0, x1) = x0 + x1 + 1,
      
      [mark](x0) = 0,
      
      [sel](x0, x1) = x0 + x1,
      
      [fib1](x0, x1) = x0 + x1,
      
      [s](x0) = x0,
      
      [0] = 0,
      
      [active](x0) = x0,
      
      [fib](x0) = x0
     orientation:
      active#(add(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = active#(X2)
      
      active#(add(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = active#(X1)
      
      active#(cons(X1,X2)) = X1 + X2 + 1 >= X1 + 1 = active#(X1)
      
      active#(s(X)) = X + 1 >= X + 1 = active#(X)
      
      active#(fib1(X1,X2)) = X1 + X2 + 1 >= X2 + 1 = active#(X2)
      
      active#(fib1(X1,X2)) = X1 + X2 + 1 >= X1 + 1 = active#(X1)
      
      active#(sel(X1,X2)) = X1 + X2 + 1 >= X2 + 1 = active#(X2)
      
      active#(sel(X1,X2)) = X1 + X2 + 1 >= X1 + 1 = active#(X1)
      
      active#(fib(X)) = X + 1 >= X + 1 = active#(X)
      
      active(fib(N)) = N >= 0 = mark(sel(N,fib1(s(0()),s(0()))))
      
      active(fib1(X,Y)) = X + Y >= 0 = mark(cons(X,fib1(Y,add(X,Y))))
      
      active(add(0(),X)) = X + 1 >= 0 = mark(X)
      
      active(add(s(X),Y)) = X + Y + 1 >= 0 = mark(s(add(X,Y)))
      
      active(sel(0(),cons(X,XS))) = X + XS >= 0 = mark(X)
      
      active(sel(s(N),cons(X,XS))) = N + X + XS >= 0 = mark(sel(N,XS))
      
      active(fib(X)) = X >= X = fib(active(X))
      
      active(sel(X1,X2)) = X1 + X2 >= X1 + X2 = sel(active(X1),X2)
      
      active(sel(X1,X2)) = X1 + X2 >= X1 + X2 = sel(X1,active(X2))
      
      active(fib1(X1,X2)) = X1 + X2 >= X1 + X2 = fib1(active(X1),X2)
      
      active(fib1(X1,X2)) = X1 + X2 >= X1 + X2 = fib1(X1,active(X2))
      
      active(s(X)) = X >= X = s(active(X))
      
      active(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(active(X1),X2)
      
      active(add(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = add(active(X1),X2)
      
      active(add(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = add(X1,active(X2))
      
      fib(mark(X)) = 0 >= 0 = mark(fib(X))
      
      sel(mark(X1),X2) = X2 >= 0 = mark(sel(X1,X2))
      
      sel(X1,mark(X2)) = X1 >= 0 = mark(sel(X1,X2))
      
      fib1(mark(X1),X2) = X2 >= 0 = mark(fib1(X1,X2))
      
      fib1(X1,mark(X2)) = X1 >= 0 = mark(fib1(X1,X2))
      
      s(mark(X)) = 0 >= 0 = mark(s(X))
      
      cons(mark(X1),X2) = X2 >= 0 = mark(cons(X1,X2))
      
      add(mark(X1),X2) = X2 + 1 >= 0 = mark(add(X1,X2))
      
      add(X1,mark(X2)) = X1 + 1 >= 0 = mark(add(X1,X2))
      
      proper(fib(X)) = X >= X = fib(proper(X))
      
      proper(sel(X1,X2)) = X1 + X2 >= X1 + X2 = sel(proper(X1),proper(X2))
      
      proper(fib1(X1,X2)) = X1 + X2 >= X1 + X2 = fib1(proper(X1),proper(X2))
      
      proper(s(X)) = X >= X = s(proper(X))
      
      proper(0()) = 0 >= 0 = ok(0())
      
      proper(cons(X1,X2)) = X1 + X2 >= X1 + X2 = cons(proper(X1),proper(X2))
      
      proper(add(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = add(proper(X1),proper(X2))
      
      fib(ok(X)) = 0 >= 0 = ok(fib(X))
      
      sel(ok(X1),ok(X2)) = 0 >= 0 = ok(sel(X1,X2))
      
      fib1(ok(X1),ok(X2)) = 0 >= 0 = ok(fib1(X1,X2))
      
      s(ok(X)) = 0 >= 0 = ok(s(X))
      
      cons(ok(X1),ok(X2)) = 0 >= 0 = ok(cons(X1,X2))
      
      add(ok(X1),ok(X2)) = 1 >= 0 = ok(add(X1,X2))
      
      top(mark(X)) = 0 >= 0 = top(proper(X))
      
      top(ok(X)) = 0 >= 0 = top(active(X))
     problem:
      DPs:
       active#(cons(X1,X2)) -> active#(X1)
       active#(s(X)) -> active#(X)
       active#(fib1(X1,X2)) -> active#(X2)
       active#(fib1(X1,X2)) -> active#(X1)
       active#(sel(X1,X2)) -> active#(X2)
       active#(sel(X1,X2)) -> active#(X1)
       active#(fib(X)) -> active#(X)
      TRS:
       active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
       active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(sel(0(),cons(X,XS))) -> mark(X)
       active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
       active(fib(X)) -> fib(active(X))
       active(sel(X1,X2)) -> sel(active(X1),X2)
       active(sel(X1,X2)) -> sel(X1,active(X2))
       active(fib1(X1,X2)) -> fib1(active(X1),X2)
       active(fib1(X1,X2)) -> fib1(X1,active(X2))
       active(s(X)) -> s(active(X))
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(add(X1,X2)) -> add(active(X1),X2)
       active(add(X1,X2)) -> add(X1,active(X2))
       fib(mark(X)) -> mark(fib(X))
       sel(mark(X1),X2) -> mark(sel(X1,X2))
       sel(X1,mark(X2)) -> mark(sel(X1,X2))
       fib1(mark(X1),X2) -> mark(fib1(X1,X2))
       fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
       s(mark(X)) -> mark(s(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       add(mark(X1),X2) -> mark(add(X1,X2))
       add(X1,mark(X2)) -> mark(add(X1,X2))
       proper(fib(X)) -> fib(proper(X))
       proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
       proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
       proper(s(X)) -> s(proper(X))
       proper(0()) -> ok(0())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(add(X1,X2)) -> add(proper(X1),proper(X2))
       fib(ok(X)) -> ok(fib(X))
       sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
       fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
       s(ok(X)) -> ok(s(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       add(ok(X1),ok(X2)) -> ok(add(X1,X2))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [active#](x0) = x0,
       
       [top](x0) = 0,
       
       [ok](x0) = x0,
       
       [proper](x0) = x0,
       
       [cons](x0, x1) = x0 + 1,
       
       [add](x0, x1) = 0,
       
       [mark](x0) = 0,
       
       [sel](x0, x1) = x0 + x1,
       
       [fib1](x0, x1) = x0 + x1 + 1,
       
       [s](x0) = x0,
       
       [0] = 1,
       
       [active](x0) = x0,
       
       [fib](x0) = x0
      orientation:
       active#(cons(X1,X2)) = X1 + 1 >= X1 = active#(X1)
       
       active#(s(X)) = X >= X = active#(X)
       
       active#(fib1(X1,X2)) = X1 + X2 + 1 >= X2 = active#(X2)
       
       active#(fib1(X1,X2)) = X1 + X2 + 1 >= X1 = active#(X1)
       
       active#(sel(X1,X2)) = X1 + X2 >= X2 = active#(X2)
       
       active#(sel(X1,X2)) = X1 + X2 >= X1 = active#(X1)
       
       active#(fib(X)) = X >= X = active#(X)
       
       active(fib(N)) = N >= 0 = mark(sel(N,fib1(s(0()),s(0()))))
       
       active(fib1(X,Y)) = X + Y + 1 >= 0 = mark(cons(X,fib1(Y,add(X,Y))))
       
       active(add(0(),X)) = 0 >= 0 = mark(X)
       
       active(add(s(X),Y)) = 0 >= 0 = mark(s(add(X,Y)))
       
       active(sel(0(),cons(X,XS))) = X + 2 >= 0 = mark(X)
       
       active(sel(s(N),cons(X,XS))) = N + X + 1 >= 0 = mark(sel(N,XS))
       
       active(fib(X)) = X >= X = fib(active(X))
       
       active(sel(X1,X2)) = X1 + X2 >= X1 + X2 = sel(active(X1),X2)
       
       active(sel(X1,X2)) = X1 + X2 >= X1 + X2 = sel(X1,active(X2))
       
       active(fib1(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = fib1(active(X1),X2)
       
       active(fib1(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = fib1(X1,active(X2))
       
       active(s(X)) = X >= X = s(active(X))
       
       active(cons(X1,X2)) = X1 + 1 >= X1 + 1 = cons(active(X1),X2)
       
       active(add(X1,X2)) = 0 >= 0 = add(active(X1),X2)
       
       active(add(X1,X2)) = 0 >= 0 = add(X1,active(X2))
       
       fib(mark(X)) = 0 >= 0 = mark(fib(X))
       
       sel(mark(X1),X2) = X2 >= 0 = mark(sel(X1,X2))
       
       sel(X1,mark(X2)) = X1 >= 0 = mark(sel(X1,X2))
       
       fib1(mark(X1),X2) = X2 + 1 >= 0 = mark(fib1(X1,X2))
       
       fib1(X1,mark(X2)) = X1 + 1 >= 0 = mark(fib1(X1,X2))
       
       s(mark(X)) = 0 >= 0 = mark(s(X))
       
       cons(mark(X1),X2) = 1 >= 0 = mark(cons(X1,X2))
       
       add(mark(X1),X2) = 0 >= 0 = mark(add(X1,X2))
       
       add(X1,mark(X2)) = 0 >= 0 = mark(add(X1,X2))
       
       proper(fib(X)) = X >= X = fib(proper(X))
       
       proper(sel(X1,X2)) = X1 + X2 >= X1 + X2 = sel(proper(X1),proper(X2))
       
       proper(fib1(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = fib1(proper(X1),proper(X2))
       
       proper(s(X)) = X >= X = s(proper(X))
       
       proper(0()) = 1 >= 1 = ok(0())
       
       proper(cons(X1,X2)) = X1 + 1 >= X1 + 1 = cons(proper(X1),proper(X2))
       
       proper(add(X1,X2)) = 0 >= 0 = add(proper(X1),proper(X2))
       
       fib(ok(X)) = X >= X = ok(fib(X))
       
       sel(ok(X1),ok(X2)) = X1 + X2 >= X1 + X2 = ok(sel(X1,X2))
       
       fib1(ok(X1),ok(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = ok(fib1(X1,X2))
       
       s(ok(X)) = X >= X = ok(s(X))
       
       cons(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(cons(X1,X2))
       
       add(ok(X1),ok(X2)) = 0 >= 0 = ok(add(X1,X2))
       
       top(mark(X)) = 0 >= 0 = top(proper(X))
       
       top(ok(X)) = 0 >= 0 = top(active(X))
      problem:
       DPs:
        active#(s(X)) -> active#(X)
        active#(sel(X1,X2)) -> active#(X2)
        active#(sel(X1,X2)) -> active#(X1)
        active#(fib(X)) -> active#(X)
       TRS:
        active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
        active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(sel(0(),cons(X,XS))) -> mark(X)
        active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
        active(fib(X)) -> fib(active(X))
        active(sel(X1,X2)) -> sel(active(X1),X2)
        active(sel(X1,X2)) -> sel(X1,active(X2))
        active(fib1(X1,X2)) -> fib1(active(X1),X2)
        active(fib1(X1,X2)) -> fib1(X1,active(X2))
        active(s(X)) -> s(active(X))
        active(cons(X1,X2)) -> cons(active(X1),X2)
        active(add(X1,X2)) -> add(active(X1),X2)
        active(add(X1,X2)) -> add(X1,active(X2))
        fib(mark(X)) -> mark(fib(X))
        sel(mark(X1),X2) -> mark(sel(X1,X2))
        sel(X1,mark(X2)) -> mark(sel(X1,X2))
        fib1(mark(X1),X2) -> mark(fib1(X1,X2))
        fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
        s(mark(X)) -> mark(s(X))
        cons(mark(X1),X2) -> mark(cons(X1,X2))
        add(mark(X1),X2) -> mark(add(X1,X2))
        add(X1,mark(X2)) -> mark(add(X1,X2))
        proper(fib(X)) -> fib(proper(X))
        proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
        proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
        proper(s(X)) -> s(proper(X))
        proper(0()) -> ok(0())
        proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
        proper(add(X1,X2)) -> add(proper(X1),proper(X2))
        fib(ok(X)) -> ok(fib(X))
        sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
        fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
        s(ok(X)) -> ok(s(X))
        cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
        add(ok(X1),ok(X2)) -> ok(add(X1,X2))
        top(mark(X)) -> top(proper(X))
        top(ok(X)) -> top(active(X))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [active#](x0) = x0 + 1,
        
        [top](x0) = 0,
        
        [ok](x0) = 1,
        
        [proper](x0) = x0,
        
        [cons](x0, x1) = 1,
        
        [add](x0, x1) = x0,
        
        [mark](x0) = 0,
        
        [sel](x0, x1) = x0 + x1,
        
        [fib1](x0, x1) = x1 + 1,
        
        [s](x0) = x0 + 1,
        
        [0] = 1,
        
        [active](x0) = x0,
        
        [fib](x0) = x0
       orientation:
        active#(s(X)) = X + 2 >= X + 1 = active#(X)
        
        active#(sel(X1,X2)) = X1 + X2 + 1 >= X2 + 1 = active#(X2)
        
        active#(sel(X1,X2)) = X1 + X2 + 1 >= X1 + 1 = active#(X1)
        
        active#(fib(X)) = X + 1 >= X + 1 = active#(X)
        
        active(fib(N)) = N >= 0 = mark(sel(N,fib1(s(0()),s(0()))))
        
        active(fib1(X,Y)) = Y + 1 >= 0 = mark(cons(X,fib1(Y,add(X,Y))))
        
        active(add(0(),X)) = 1 >= 0 = mark(X)
        
        active(add(s(X),Y)) = X + 1 >= 0 = mark(s(add(X,Y)))
        
        active(sel(0(),cons(X,XS))) = 2 >= 0 = mark(X)
        
        active(sel(s(N),cons(X,XS))) = N + 2 >= 0 = mark(sel(N,XS))
        
        active(fib(X)) = X >= X = fib(active(X))
        
        active(sel(X1,X2)) = X1 + X2 >= X1 + X2 = sel(active(X1),X2)
        
        active(sel(X1,X2)) = X1 + X2 >= X1 + X2 = sel(X1,active(X2))
        
        active(fib1(X1,X2)) = X2 + 1 >= X2 + 1 = fib1(active(X1),X2)
        
        active(fib1(X1,X2)) = X2 + 1 >= X2 + 1 = fib1(X1,active(X2))
        
        active(s(X)) = X + 1 >= X + 1 = s(active(X))
        
        active(cons(X1,X2)) = 1 >= 1 = cons(active(X1),X2)
        
        active(add(X1,X2)) = X1 >= X1 = add(active(X1),X2)
        
        active(add(X1,X2)) = X1 >= X1 = add(X1,active(X2))
        
        fib(mark(X)) = 0 >= 0 = mark(fib(X))
        
        sel(mark(X1),X2) = X2 >= 0 = mark(sel(X1,X2))
        
        sel(X1,mark(X2)) = X1 >= 0 = mark(sel(X1,X2))
        
        fib1(mark(X1),X2) = X2 + 1 >= 0 = mark(fib1(X1,X2))
        
        fib1(X1,mark(X2)) = 1 >= 0 = mark(fib1(X1,X2))
        
        s(mark(X)) = 1 >= 0 = mark(s(X))
        
        cons(mark(X1),X2) = 1 >= 0 = mark(cons(X1,X2))
        
        add(mark(X1),X2) = 0 >= 0 = mark(add(X1,X2))
        
        add(X1,mark(X2)) = X1 >= 0 = mark(add(X1,X2))
        
        proper(fib(X)) = X >= X = fib(proper(X))
        
        proper(sel(X1,X2)) = X1 + X2 >= X1 + X2 = sel(proper(X1),proper(X2))
        
        proper(fib1(X1,X2)) = X2 + 1 >= X2 + 1 = fib1(proper(X1),proper(X2))
        
        proper(s(X)) = X + 1 >= X + 1 = s(proper(X))
        
        proper(0()) = 1 >= 1 = ok(0())
        
        proper(cons(X1,X2)) = 1 >= 1 = cons(proper(X1),proper(X2))
        
        proper(add(X1,X2)) = X1 >= X1 = add(proper(X1),proper(X2))
        
        fib(ok(X)) = 1 >= 1 = ok(fib(X))
        
        sel(ok(X1),ok(X2)) = 2 >= 1 = ok(sel(X1,X2))
        
        fib1(ok(X1),ok(X2)) = 2 >= 1 = ok(fib1(X1,X2))
        
        s(ok(X)) = 2 >= 1 = ok(s(X))
        
        cons(ok(X1),ok(X2)) = 1 >= 1 = ok(cons(X1,X2))
        
        add(ok(X1),ok(X2)) = 1 >= 1 = ok(add(X1,X2))
        
        top(mark(X)) = 0 >= 0 = top(proper(X))
        
        top(ok(X)) = 0 >= 0 = top(active(X))
       problem:
        DPs:
         active#(sel(X1,X2)) -> active#(X2)
         active#(sel(X1,X2)) -> active#(X1)
         active#(fib(X)) -> active#(X)
        TRS:
         active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
         active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
         active(add(0(),X)) -> mark(X)
         active(add(s(X),Y)) -> mark(s(add(X,Y)))
         active(sel(0(),cons(X,XS))) -> mark(X)
         active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
         active(fib(X)) -> fib(active(X))
         active(sel(X1,X2)) -> sel(active(X1),X2)
         active(sel(X1,X2)) -> sel(X1,active(X2))
         active(fib1(X1,X2)) -> fib1(active(X1),X2)
         active(fib1(X1,X2)) -> fib1(X1,active(X2))
         active(s(X)) -> s(active(X))
         active(cons(X1,X2)) -> cons(active(X1),X2)
         active(add(X1,X2)) -> add(active(X1),X2)
         active(add(X1,X2)) -> add(X1,active(X2))
         fib(mark(X)) -> mark(fib(X))
         sel(mark(X1),X2) -> mark(sel(X1,X2))
         sel(X1,mark(X2)) -> mark(sel(X1,X2))
         fib1(mark(X1),X2) -> mark(fib1(X1,X2))
         fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
         s(mark(X)) -> mark(s(X))
         cons(mark(X1),X2) -> mark(cons(X1,X2))
         add(mark(X1),X2) -> mark(add(X1,X2))
         add(X1,mark(X2)) -> mark(add(X1,X2))
         proper(fib(X)) -> fib(proper(X))
         proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
         proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
         proper(s(X)) -> s(proper(X))
         proper(0()) -> ok(0())
         proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
         proper(add(X1,X2)) -> add(proper(X1),proper(X2))
         fib(ok(X)) -> ok(fib(X))
         sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
         fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
         s(ok(X)) -> ok(s(X))
         cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
         add(ok(X1),ok(X2)) -> ok(add(X1,X2))
         top(mark(X)) -> top(proper(X))
         top(ok(X)) -> top(active(X))
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [active#](x0) = x0 + 1,
         
         [top](x0) = 0,
         
         [ok](x0) = 0,
         
         [proper](x0) = x0,
         
         [cons](x0, x1) = 0,
         
         [add](x0, x1) = 1,
         
         [mark](x0) = 0,
         
         [sel](x0, x1) = x0 + x1 + 1,
         
         [fib1](x0, x1) = x1,
         
         [s](x0) = 0,
         
         [0] = 0,
         
         [active](x0) = x0,
         
         [fib](x0) = x0
        orientation:
         active#(sel(X1,X2)) = X1 + X2 + 2 >= X2 + 1 = active#(X2)
         
         active#(sel(X1,X2)) = X1 + X2 + 2 >= X1 + 1 = active#(X1)
         
         active#(fib(X)) = X + 1 >= X + 1 = active#(X)
         
         active(fib(N)) = N >= 0 = mark(sel(N,fib1(s(0()),s(0()))))
         
         active(fib1(X,Y)) = Y >= 0 = mark(cons(X,fib1(Y,add(X,Y))))
         
         active(add(0(),X)) = 1 >= 0 = mark(X)
         
         active(add(s(X),Y)) = 1 >= 0 = mark(s(add(X,Y)))
         
         active(sel(0(),cons(X,XS))) = 1 >= 0 = mark(X)
         
         active(sel(s(N),cons(X,XS))) = 1 >= 0 = mark(sel(N,XS))
         
         active(fib(X)) = X >= X = fib(active(X))
         
         active(sel(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = sel(active(X1),X2)
         
         active(sel(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = sel(X1,active(X2))
         
         active(fib1(X1,X2)) = X2 >= X2 = fib1(active(X1),X2)
         
         active(fib1(X1,X2)) = X2 >= X2 = fib1(X1,active(X2))
         
         active(s(X)) = 0 >= 0 = s(active(X))
         
         active(cons(X1,X2)) = 0 >= 0 = cons(active(X1),X2)
         
         active(add(X1,X2)) = 1 >= 1 = add(active(X1),X2)
         
         active(add(X1,X2)) = 1 >= 1 = add(X1,active(X2))
         
         fib(mark(X)) = 0 >= 0 = mark(fib(X))
         
         sel(mark(X1),X2) = X2 + 1 >= 0 = mark(sel(X1,X2))
         
         sel(X1,mark(X2)) = X1 + 1 >= 0 = mark(sel(X1,X2))
         
         fib1(mark(X1),X2) = X2 >= 0 = mark(fib1(X1,X2))
         
         fib1(X1,mark(X2)) = 0 >= 0 = mark(fib1(X1,X2))
         
         s(mark(X)) = 0 >= 0 = mark(s(X))
         
         cons(mark(X1),X2) = 0 >= 0 = mark(cons(X1,X2))
         
         add(mark(X1),X2) = 1 >= 0 = mark(add(X1,X2))
         
         add(X1,mark(X2)) = 1 >= 0 = mark(add(X1,X2))
         
         proper(fib(X)) = X >= X = fib(proper(X))
         
         proper(sel(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = sel(proper(X1),proper(X2))
         
         proper(fib1(X1,X2)) = X2 >= X2 = fib1(proper(X1),proper(X2))
         
         proper(s(X)) = 0 >= 0 = s(proper(X))
         
         proper(0()) = 0 >= 0 = ok(0())
         
         proper(cons(X1,X2)) = 0 >= 0 = cons(proper(X1),proper(X2))
         
         proper(add(X1,X2)) = 1 >= 1 = add(proper(X1),proper(X2))
         
         fib(ok(X)) = 0 >= 0 = ok(fib(X))
         
         sel(ok(X1),ok(X2)) = 1 >= 0 = ok(sel(X1,X2))
         
         fib1(ok(X1),ok(X2)) = 0 >= 0 = ok(fib1(X1,X2))
         
         s(ok(X)) = 0 >= 0 = ok(s(X))
         
         cons(ok(X1),ok(X2)) = 0 >= 0 = ok(cons(X1,X2))
         
         add(ok(X1),ok(X2)) = 1 >= 0 = ok(add(X1,X2))
         
         top(mark(X)) = 0 >= 0 = top(proper(X))
         
         top(ok(X)) = 0 >= 0 = top(active(X))
        problem:
         DPs:
          active#(fib(X)) -> active#(X)
         TRS:
          active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
          active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
          active(add(0(),X)) -> mark(X)
          active(add(s(X),Y)) -> mark(s(add(X,Y)))
          active(sel(0(),cons(X,XS))) -> mark(X)
          active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
          active(fib(X)) -> fib(active(X))
          active(sel(X1,X2)) -> sel(active(X1),X2)
          active(sel(X1,X2)) -> sel(X1,active(X2))
          active(fib1(X1,X2)) -> fib1(active(X1),X2)
          active(fib1(X1,X2)) -> fib1(X1,active(X2))
          active(s(X)) -> s(active(X))
          active(cons(X1,X2)) -> cons(active(X1),X2)
          active(add(X1,X2)) -> add(active(X1),X2)
          active(add(X1,X2)) -> add(X1,active(X2))
          fib(mark(X)) -> mark(fib(X))
          sel(mark(X1),X2) -> mark(sel(X1,X2))
          sel(X1,mark(X2)) -> mark(sel(X1,X2))
          fib1(mark(X1),X2) -> mark(fib1(X1,X2))
          fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
          s(mark(X)) -> mark(s(X))
          cons(mark(X1),X2) -> mark(cons(X1,X2))
          add(mark(X1),X2) -> mark(add(X1,X2))
          add(X1,mark(X2)) -> mark(add(X1,X2))
          proper(fib(X)) -> fib(proper(X))
          proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
          proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
          proper(s(X)) -> s(proper(X))
          proper(0()) -> ok(0())
          proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
          proper(add(X1,X2)) -> add(proper(X1),proper(X2))
          fib(ok(X)) -> ok(fib(X))
          sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
          fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
          s(ok(X)) -> ok(s(X))
          cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
          add(ok(X1),ok(X2)) -> ok(add(X1,X2))
          top(mark(X)) -> top(proper(X))
          top(ok(X)) -> top(active(X))
        Matrix Interpretation Processor:
         dimension: 1
         interpretation:
          [active#](x0) = x0 + 1,
          
          [top](x0) = 1,
          
          [ok](x0) = 0,
          
          [proper](x0) = x0,
          
          [cons](x0, x1) = 0,
          
          [add](x0, x1) = x0 + x1 + 1,
          
          [mark](x0) = 0,
          
          [sel](x0, x1) = 1,
          
          [fib1](x0, x1) = 0,
          
          [s](x0) = 1,
          
          [0] = 0,
          
          [active](x0) = x0,
          
          [fib](x0) = x0 + 1
         orientation:
          active#(fib(X)) = X + 2 >= X + 1 = active#(X)
          
          active(fib(N)) = N + 1 >= 0 = mark(sel(N,fib1(s(0()),s(0()))))
          
          active(fib1(X,Y)) = 0 >= 0 = mark(cons(X,fib1(Y,add(X,Y))))
          
          active(add(0(),X)) = X + 1 >= 0 = mark(X)
          
          active(add(s(X),Y)) = Y + 2 >= 0 = mark(s(add(X,Y)))
          
          active(sel(0(),cons(X,XS))) = 1 >= 0 = mark(X)
          
          active(sel(s(N),cons(X,XS))) = 1 >= 0 = mark(sel(N,XS))
          
          active(fib(X)) = X + 1 >= X + 1 = fib(active(X))
          
          active(sel(X1,X2)) = 1 >= 1 = sel(active(X1),X2)
          
          active(sel(X1,X2)) = 1 >= 1 = sel(X1,active(X2))
          
          active(fib1(X1,X2)) = 0 >= 0 = fib1(active(X1),X2)
          
          active(fib1(X1,X2)) = 0 >= 0 = fib1(X1,active(X2))
          
          active(s(X)) = 1 >= 1 = s(active(X))
          
          active(cons(X1,X2)) = 0 >= 0 = cons(active(X1),X2)
          
          active(add(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = add(active(X1),X2)
          
          active(add(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = add(X1,active(X2))
          
          fib(mark(X)) = 1 >= 0 = mark(fib(X))
          
          sel(mark(X1),X2) = 1 >= 0 = mark(sel(X1,X2))
          
          sel(X1,mark(X2)) = 1 >= 0 = mark(sel(X1,X2))
          
          fib1(mark(X1),X2) = 0 >= 0 = mark(fib1(X1,X2))
          
          fib1(X1,mark(X2)) = 0 >= 0 = mark(fib1(X1,X2))
          
          s(mark(X)) = 1 >= 0 = mark(s(X))
          
          cons(mark(X1),X2) = 0 >= 0 = mark(cons(X1,X2))
          
          add(mark(X1),X2) = X2 + 1 >= 0 = mark(add(X1,X2))
          
          add(X1,mark(X2)) = X1 + 1 >= 0 = mark(add(X1,X2))
          
          proper(fib(X)) = X + 1 >= X + 1 = fib(proper(X))
          
          proper(sel(X1,X2)) = 1 >= 1 = sel(proper(X1),proper(X2))
          
          proper(fib1(X1,X2)) = 0 >= 0 = fib1(proper(X1),proper(X2))
          
          proper(s(X)) = 1 >= 1 = s(proper(X))
          
          proper(0()) = 0 >= 0 = ok(0())
          
          proper(cons(X1,X2)) = 0 >= 0 = cons(proper(X1),proper(X2))
          
          proper(add(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = add(proper(X1),proper(X2))
          
          fib(ok(X)) = 1 >= 0 = ok(fib(X))
          
          sel(ok(X1),ok(X2)) = 1 >= 0 = ok(sel(X1,X2))
          
          fib1(ok(X1),ok(X2)) = 0 >= 0 = ok(fib1(X1,X2))
          
          s(ok(X)) = 1 >= 0 = ok(s(X))
          
          cons(ok(X1),ok(X2)) = 0 >= 0 = ok(cons(X1,X2))
          
          add(ok(X1),ok(X2)) = 1 >= 0 = ok(add(X1,X2))
          
          top(mark(X)) = 1 >= 1 = top(proper(X))
          
          top(ok(X)) = 1 >= 1 = top(active(X))
         problem:
          DPs:
           
          TRS:
           active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
           active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
           active(add(0(),X)) -> mark(X)
           active(add(s(X),Y)) -> mark(s(add(X,Y)))
           active(sel(0(),cons(X,XS))) -> mark(X)
           active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
           active(fib(X)) -> fib(active(X))
           active(sel(X1,X2)) -> sel(active(X1),X2)
           active(sel(X1,X2)) -> sel(X1,active(X2))
           active(fib1(X1,X2)) -> fib1(active(X1),X2)
           active(fib1(X1,X2)) -> fib1(X1,active(X2))
           active(s(X)) -> s(active(X))
           active(cons(X1,X2)) -> cons(active(X1),X2)
           active(add(X1,X2)) -> add(active(X1),X2)
           active(add(X1,X2)) -> add(X1,active(X2))
           fib(mark(X)) -> mark(fib(X))
           sel(mark(X1),X2) -> mark(sel(X1,X2))
           sel(X1,mark(X2)) -> mark(sel(X1,X2))
           fib1(mark(X1),X2) -> mark(fib1(X1,X2))
           fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
           s(mark(X)) -> mark(s(X))
           cons(mark(X1),X2) -> mark(cons(X1,X2))
           add(mark(X1),X2) -> mark(add(X1,X2))
           add(X1,mark(X2)) -> mark(add(X1,X2))
           proper(fib(X)) -> fib(proper(X))
           proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
           proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
           proper(s(X)) -> s(proper(X))
           proper(0()) -> ok(0())
           proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
           proper(add(X1,X2)) -> add(proper(X1),proper(X2))
           fib(ok(X)) -> ok(fib(X))
           sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
           fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
           s(ok(X)) -> ok(s(X))
           cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
           add(ok(X1),ok(X2)) -> ok(add(X1,X2))
           top(mark(X)) -> top(proper(X))
           top(ok(X)) -> top(active(X))
         Qed
    
    DPs:
     fib#(ok(X)) -> fib#(X)
     fib#(mark(X)) -> fib#(X)
    TRS:
     active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
     active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(sel(0(),cons(X,XS))) -> mark(X)
     active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
     active(fib(X)) -> fib(active(X))
     active(sel(X1,X2)) -> sel(active(X1),X2)
     active(sel(X1,X2)) -> sel(X1,active(X2))
     active(fib1(X1,X2)) -> fib1(active(X1),X2)
     active(fib1(X1,X2)) -> fib1(X1,active(X2))
     active(s(X)) -> s(active(X))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(add(X1,X2)) -> add(active(X1),X2)
     active(add(X1,X2)) -> add(X1,active(X2))
     fib(mark(X)) -> mark(fib(X))
     sel(mark(X1),X2) -> mark(sel(X1,X2))
     sel(X1,mark(X2)) -> mark(sel(X1,X2))
     fib1(mark(X1),X2) -> mark(fib1(X1,X2))
     fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
     s(mark(X)) -> mark(s(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     add(mark(X1),X2) -> mark(add(X1,X2))
     add(X1,mark(X2)) -> mark(add(X1,X2))
     proper(fib(X)) -> fib(proper(X))
     proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
     proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
     proper(s(X)) -> s(proper(X))
     proper(0()) -> ok(0())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(add(X1,X2)) -> add(proper(X1),proper(X2))
     fib(ok(X)) -> ok(fib(X))
     sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
     fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
     s(ok(X)) -> ok(s(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     add(ok(X1),ok(X2)) -> ok(add(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     sel#(ok(X1),ok(X2)) -> sel#(X1,X2)
     sel#(X1,mark(X2)) -> sel#(X1,X2)
     sel#(mark(X1),X2) -> sel#(X1,X2)
    TRS:
     active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
     active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(sel(0(),cons(X,XS))) -> mark(X)
     active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
     active(fib(X)) -> fib(active(X))
     active(sel(X1,X2)) -> sel(active(X1),X2)
     active(sel(X1,X2)) -> sel(X1,active(X2))
     active(fib1(X1,X2)) -> fib1(active(X1),X2)
     active(fib1(X1,X2)) -> fib1(X1,active(X2))
     active(s(X)) -> s(active(X))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(add(X1,X2)) -> add(active(X1),X2)
     active(add(X1,X2)) -> add(X1,active(X2))
     fib(mark(X)) -> mark(fib(X))
     sel(mark(X1),X2) -> mark(sel(X1,X2))
     sel(X1,mark(X2)) -> mark(sel(X1,X2))
     fib1(mark(X1),X2) -> mark(fib1(X1,X2))
     fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
     s(mark(X)) -> mark(s(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     add(mark(X1),X2) -> mark(add(X1,X2))
     add(X1,mark(X2)) -> mark(add(X1,X2))
     proper(fib(X)) -> fib(proper(X))
     proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
     proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
     proper(s(X)) -> s(proper(X))
     proper(0()) -> ok(0())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(add(X1,X2)) -> add(proper(X1),proper(X2))
     fib(ok(X)) -> ok(fib(X))
     sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
     fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
     s(ok(X)) -> ok(s(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     add(ok(X1),ok(X2)) -> ok(add(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     fib1#(ok(X1),ok(X2)) -> fib1#(X1,X2)
     fib1#(X1,mark(X2)) -> fib1#(X1,X2)
     fib1#(mark(X1),X2) -> fib1#(X1,X2)
    TRS:
     active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
     active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(sel(0(),cons(X,XS))) -> mark(X)
     active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
     active(fib(X)) -> fib(active(X))
     active(sel(X1,X2)) -> sel(active(X1),X2)
     active(sel(X1,X2)) -> sel(X1,active(X2))
     active(fib1(X1,X2)) -> fib1(active(X1),X2)
     active(fib1(X1,X2)) -> fib1(X1,active(X2))
     active(s(X)) -> s(active(X))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(add(X1,X2)) -> add(active(X1),X2)
     active(add(X1,X2)) -> add(X1,active(X2))
     fib(mark(X)) -> mark(fib(X))
     sel(mark(X1),X2) -> mark(sel(X1,X2))
     sel(X1,mark(X2)) -> mark(sel(X1,X2))
     fib1(mark(X1),X2) -> mark(fib1(X1,X2))
     fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
     s(mark(X)) -> mark(s(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     add(mark(X1),X2) -> mark(add(X1,X2))
     add(X1,mark(X2)) -> mark(add(X1,X2))
     proper(fib(X)) -> fib(proper(X))
     proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
     proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
     proper(s(X)) -> s(proper(X))
     proper(0()) -> ok(0())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(add(X1,X2)) -> add(proper(X1),proper(X2))
     fib(ok(X)) -> ok(fib(X))
     sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
     fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
     s(ok(X)) -> ok(s(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     add(ok(X1),ok(X2)) -> ok(add(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     s#(ok(X)) -> s#(X)
     s#(mark(X)) -> s#(X)
    TRS:
     active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
     active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(sel(0(),cons(X,XS))) -> mark(X)
     active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
     active(fib(X)) -> fib(active(X))
     active(sel(X1,X2)) -> sel(active(X1),X2)
     active(sel(X1,X2)) -> sel(X1,active(X2))
     active(fib1(X1,X2)) -> fib1(active(X1),X2)
     active(fib1(X1,X2)) -> fib1(X1,active(X2))
     active(s(X)) -> s(active(X))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(add(X1,X2)) -> add(active(X1),X2)
     active(add(X1,X2)) -> add(X1,active(X2))
     fib(mark(X)) -> mark(fib(X))
     sel(mark(X1),X2) -> mark(sel(X1,X2))
     sel(X1,mark(X2)) -> mark(sel(X1,X2))
     fib1(mark(X1),X2) -> mark(fib1(X1,X2))
     fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
     s(mark(X)) -> mark(s(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     add(mark(X1),X2) -> mark(add(X1,X2))
     add(X1,mark(X2)) -> mark(add(X1,X2))
     proper(fib(X)) -> fib(proper(X))
     proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
     proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
     proper(s(X)) -> s(proper(X))
     proper(0()) -> ok(0())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(add(X1,X2)) -> add(proper(X1),proper(X2))
     fib(ok(X)) -> ok(fib(X))
     sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
     fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
     s(ok(X)) -> ok(s(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     add(ok(X1),ok(X2)) -> ok(add(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open
    
    DPs:
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
     cons#(mark(X1),X2) -> cons#(X1,X2)
    TRS:
     active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
     active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(sel(0(),cons(X,XS))) -> mark(X)
     active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
     active(fib(X)) -> fib(active(X))
     active(sel(X1,X2)) -> sel(active(X1),X2)
     active(sel(X1,X2)) -> sel(X1,active(X2))
     active(fib1(X1,X2)) -> fib1(active(X1),X2)
     active(fib1(X1,X2)) -> fib1(X1,active(X2))
     active(s(X)) -> s(active(X))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(add(X1,X2)) -> add(active(X1),X2)
     active(add(X1,X2)) -> add(X1,active(X2))
     fib(mark(X)) -> mark(fib(X))
     sel(mark(X1),X2) -> mark(sel(X1,X2))
     sel(X1,mark(X2)) -> mark(sel(X1,X2))
     fib1(mark(X1),X2) -> mark(fib1(X1,X2))
     fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
     s(mark(X)) -> mark(s(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     add(mark(X1),X2) -> mark(add(X1,X2))
     add(X1,mark(X2)) -> mark(add(X1,X2))
     proper(fib(X)) -> fib(proper(X))
     proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
     proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
     proper(s(X)) -> s(proper(X))
     proper(0()) -> ok(0())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(add(X1,X2)) -> add(proper(X1),proper(X2))
     fib(ok(X)) -> ok(fib(X))
     sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
     fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
     s(ok(X)) -> ok(s(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     add(ok(X1),ok(X2)) -> ok(add(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [cons#](x0, x1) = x1 + 1,
      
      [top](x0) = 0,
      
      [ok](x0) = x0 + 1,
      
      [proper](x0) = 1,
      
      [cons](x0, x1) = x1,
      
      [add](x0, x1) = x0,
      
      [mark](x0) = 0,
      
      [sel](x0, x1) = x0,
      
      [fib1](x0, x1) = x1,
      
      [s](x0) = x0,
      
      [0] = 0,
      
      [active](x0) = x0,
      
      [fib](x0) = x0
     orientation:
      cons#(ok(X1),ok(X2)) = X2 + 2 >= X2 + 1 = cons#(X1,X2)
      
      cons#(mark(X1),X2) = X2 + 1 >= X2 + 1 = cons#(X1,X2)
      
      active(fib(N)) = N >= 0 = mark(sel(N,fib1(s(0()),s(0()))))
      
      active(fib1(X,Y)) = Y >= 0 = mark(cons(X,fib1(Y,add(X,Y))))
      
      active(add(0(),X)) = 0 >= 0 = mark(X)
      
      active(add(s(X),Y)) = X >= 0 = mark(s(add(X,Y)))
      
      active(sel(0(),cons(X,XS))) = 0 >= 0 = mark(X)
      
      active(sel(s(N),cons(X,XS))) = N >= 0 = mark(sel(N,XS))
      
      active(fib(X)) = X >= X = fib(active(X))
      
      active(sel(X1,X2)) = X1 >= X1 = sel(active(X1),X2)
      
      active(sel(X1,X2)) = X1 >= X1 = sel(X1,active(X2))
      
      active(fib1(X1,X2)) = X2 >= X2 = fib1(active(X1),X2)
      
      active(fib1(X1,X2)) = X2 >= X2 = fib1(X1,active(X2))
      
      active(s(X)) = X >= X = s(active(X))
      
      active(cons(X1,X2)) = X2 >= X2 = cons(active(X1),X2)
      
      active(add(X1,X2)) = X1 >= X1 = add(active(X1),X2)
      
      active(add(X1,X2)) = X1 >= X1 = add(X1,active(X2))
      
      fib(mark(X)) = 0 >= 0 = mark(fib(X))
      
      sel(mark(X1),X2) = 0 >= 0 = mark(sel(X1,X2))
      
      sel(X1,mark(X2)) = X1 >= 0 = mark(sel(X1,X2))
      
      fib1(mark(X1),X2) = X2 >= 0 = mark(fib1(X1,X2))
      
      fib1(X1,mark(X2)) = 0 >= 0 = mark(fib1(X1,X2))
      
      s(mark(X)) = 0 >= 0 = mark(s(X))
      
      cons(mark(X1),X2) = X2 >= 0 = mark(cons(X1,X2))
      
      add(mark(X1),X2) = 0 >= 0 = mark(add(X1,X2))
      
      add(X1,mark(X2)) = X1 >= 0 = mark(add(X1,X2))
      
      proper(fib(X)) = 1 >= 1 = fib(proper(X))
      
      proper(sel(X1,X2)) = 1 >= 1 = sel(proper(X1),proper(X2))
      
      proper(fib1(X1,X2)) = 1 >= 1 = fib1(proper(X1),proper(X2))
      
      proper(s(X)) = 1 >= 1 = s(proper(X))
      
      proper(0()) = 1 >= 1 = ok(0())
      
      proper(cons(X1,X2)) = 1 >= 1 = cons(proper(X1),proper(X2))
      
      proper(add(X1,X2)) = 1 >= 1 = add(proper(X1),proper(X2))
      
      fib(ok(X)) = X + 1 >= X + 1 = ok(fib(X))
      
      sel(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(sel(X1,X2))
      
      fib1(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(fib1(X1,X2))
      
      s(ok(X)) = X + 1 >= X + 1 = ok(s(X))
      
      cons(ok(X1),ok(X2)) = X2 + 1 >= X2 + 1 = ok(cons(X1,X2))
      
      add(ok(X1),ok(X2)) = X1 + 1 >= X1 + 1 = ok(add(X1,X2))
      
      top(mark(X)) = 0 >= 0 = top(proper(X))
      
      top(ok(X)) = 0 >= 0 = top(active(X))
     problem:
      DPs:
       cons#(mark(X1),X2) -> cons#(X1,X2)
      TRS:
       active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
       active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(sel(0(),cons(X,XS))) -> mark(X)
       active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
       active(fib(X)) -> fib(active(X))
       active(sel(X1,X2)) -> sel(active(X1),X2)
       active(sel(X1,X2)) -> sel(X1,active(X2))
       active(fib1(X1,X2)) -> fib1(active(X1),X2)
       active(fib1(X1,X2)) -> fib1(X1,active(X2))
       active(s(X)) -> s(active(X))
       active(cons(X1,X2)) -> cons(active(X1),X2)
       active(add(X1,X2)) -> add(active(X1),X2)
       active(add(X1,X2)) -> add(X1,active(X2))
       fib(mark(X)) -> mark(fib(X))
       sel(mark(X1),X2) -> mark(sel(X1,X2))
       sel(X1,mark(X2)) -> mark(sel(X1,X2))
       fib1(mark(X1),X2) -> mark(fib1(X1,X2))
       fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
       s(mark(X)) -> mark(s(X))
       cons(mark(X1),X2) -> mark(cons(X1,X2))
       add(mark(X1),X2) -> mark(add(X1,X2))
       add(X1,mark(X2)) -> mark(add(X1,X2))
       proper(fib(X)) -> fib(proper(X))
       proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
       proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
       proper(s(X)) -> s(proper(X))
       proper(0()) -> ok(0())
       proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
       proper(add(X1,X2)) -> add(proper(X1),proper(X2))
       fib(ok(X)) -> ok(fib(X))
       sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
       fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
       s(ok(X)) -> ok(s(X))
       cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
       add(ok(X1),ok(X2)) -> ok(add(X1,X2))
       top(mark(X)) -> top(proper(X))
       top(ok(X)) -> top(active(X))
     Open
    
    DPs:
     add#(ok(X1),ok(X2)) -> add#(X1,X2)
     add#(X1,mark(X2)) -> add#(X1,X2)
     add#(mark(X1),X2) -> add#(X1,X2)
    TRS:
     active(fib(N)) -> mark(sel(N,fib1(s(0()),s(0()))))
     active(fib1(X,Y)) -> mark(cons(X,fib1(Y,add(X,Y))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(sel(0(),cons(X,XS))) -> mark(X)
     active(sel(s(N),cons(X,XS))) -> mark(sel(N,XS))
     active(fib(X)) -> fib(active(X))
     active(sel(X1,X2)) -> sel(active(X1),X2)
     active(sel(X1,X2)) -> sel(X1,active(X2))
     active(fib1(X1,X2)) -> fib1(active(X1),X2)
     active(fib1(X1,X2)) -> fib1(X1,active(X2))
     active(s(X)) -> s(active(X))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(add(X1,X2)) -> add(active(X1),X2)
     active(add(X1,X2)) -> add(X1,active(X2))
     fib(mark(X)) -> mark(fib(X))
     sel(mark(X1),X2) -> mark(sel(X1,X2))
     sel(X1,mark(X2)) -> mark(sel(X1,X2))
     fib1(mark(X1),X2) -> mark(fib1(X1,X2))
     fib1(X1,mark(X2)) -> mark(fib1(X1,X2))
     s(mark(X)) -> mark(s(X))
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     add(mark(X1),X2) -> mark(add(X1,X2))
     add(X1,mark(X2)) -> mark(add(X1,X2))
     proper(fib(X)) -> fib(proper(X))
     proper(sel(X1,X2)) -> sel(proper(X1),proper(X2))
     proper(fib1(X1,X2)) -> fib1(proper(X1),proper(X2))
     proper(s(X)) -> s(proper(X))
     proper(0()) -> ok(0())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(add(X1,X2)) -> add(proper(X1),proper(X2))
     fib(ok(X)) -> ok(fib(X))
     sel(ok(X1),ok(X2)) -> ok(sel(X1,X2))
     fib1(ok(X1),ok(X2)) -> ok(fib1(X1,X2))
     s(ok(X)) -> ok(s(X))
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     add(ok(X1),ok(X2)) -> ok(add(X1,X2))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    Open