MAYBE
TRS:
 {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
              mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                      mark(s(X)) -> active(s(mark(X))),
                       mark(0()) -> active(0()),
                    mark(fib(X)) -> active(fib(mark(X))),
              mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
               mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
               sel(X1, mark(X2)) -> sel(X1, X2),
             sel(X1, active(X2)) -> sel(X1, X2),
               sel(mark(X1), X2) -> sel(X1, X2),
             sel(active(X1), X2) -> sel(X1, X2),
              fib1(X1, mark(X2)) -> fib1(X1, X2),
            fib1(X1, active(X2)) -> fib1(X1, X2),
              fib1(mark(X1), X2) -> fib1(X1, X2),
            fib1(active(X1), X2) -> fib1(X1, X2),
                      s(mark(X)) -> s(X),
                    s(active(X)) -> s(X),
  active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
   active(sel(0(), cons(X, XS))) -> mark(X),
              active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                  active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
            active(add(s(X), Y)) -> mark(s(add(X, Y))),
             active(add(0(), X)) -> mark(X),
                    fib(mark(X)) -> fib(X),
                  fib(active(X)) -> fib(X),
              cons(X1, mark(X2)) -> cons(X1, X2),
            cons(X1, active(X2)) -> cons(X1, X2),
              cons(mark(X1), X2) -> cons(X1, X2),
            cons(active(X1), X2) -> cons(X1, X2),
               add(X1, mark(X2)) -> add(X1, X2),
             add(X1, active(X2)) -> add(X1, X2),
               add(mark(X1), X2) -> add(X1, X2),
             add(active(X1), X2) -> add(X1, X2)}
 DP:
  Strict:
   {             mark#(sel(X1, X2)) -> mark#(X1),
                 mark#(sel(X1, X2)) -> mark#(X2),
                 mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)),
                 mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))),
                mark#(fib1(X1, X2)) -> mark#(X1),
                mark#(fib1(X1, X2)) -> mark#(X2),
                mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)),
                mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))),
                        mark#(s(X)) -> mark#(X),
                        mark#(s(X)) -> s#(mark(X)),
                        mark#(s(X)) -> active#(s(mark(X))),
                         mark#(0()) -> active#(0()),
                      mark#(fib(X)) -> mark#(X),
                      mark#(fib(X)) -> active#(fib(mark(X))),
                      mark#(fib(X)) -> fib#(mark(X)),
                mark#(cons(X1, X2)) -> mark#(X1),
                mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
                mark#(cons(X1, X2)) -> cons#(mark(X1), X2),
                 mark#(add(X1, X2)) -> mark#(X1),
                 mark#(add(X1, X2)) -> mark#(X2),
                 mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
                 mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)),
                 sel#(X1, mark(X2)) -> sel#(X1, X2),
               sel#(X1, active(X2)) -> sel#(X1, X2),
                 sel#(mark(X1), X2) -> sel#(X1, X2),
               sel#(active(X1), X2) -> sel#(X1, X2),
                fib1#(X1, mark(X2)) -> fib1#(X1, X2),
              fib1#(X1, active(X2)) -> fib1#(X1, X2),
                fib1#(mark(X1), X2) -> fib1#(X1, X2),
              fib1#(active(X1), X2) -> fib1#(X1, X2),
                        s#(mark(X)) -> s#(X),
                      s#(active(X)) -> s#(X),
    active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)),
    active#(sel(s(N), cons(X, XS))) -> sel#(N, XS),
     active#(sel(0(), cons(X, XS))) -> mark#(X),
                active#(fib1(X, Y)) -> mark#(cons(X, fib1(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#(fib1(X, Y)) -> add#(X, Y),
                    active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))),
                    active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))),
                    active#(fib(N)) -> fib1#(s(0()), s(0())),
                    active#(fib(N)) -> s#(0()),
              active#(add(s(X), Y)) -> mark#(s(add(X, Y))),
              active#(add(s(X), Y)) -> s#(add(X, Y)),
              active#(add(s(X), Y)) -> add#(X, Y),
               active#(add(0(), X)) -> mark#(X),
                      fib#(mark(X)) -> fib#(X),
                    fib#(active(X)) -> fib#(X),
                cons#(X1, mark(X2)) -> cons#(X1, X2),
              cons#(X1, active(X2)) -> cons#(X1, X2),
                cons#(mark(X1), X2) -> cons#(X1, X2),
              cons#(active(X1), X2) -> cons#(X1, X2),
                 add#(X1, mark(X2)) -> add#(X1, X2),
               add#(X1, active(X2)) -> add#(X1, X2),
                 add#(mark(X1), X2) -> add#(X1, X2),
               add#(active(X1), X2) -> add#(X1, X2)}
  Weak:
  {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
               mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                       mark(s(X)) -> active(s(mark(X))),
                        mark(0()) -> active(0()),
                     mark(fib(X)) -> active(fib(mark(X))),
               mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                sel(X1, mark(X2)) -> sel(X1, X2),
              sel(X1, active(X2)) -> sel(X1, X2),
                sel(mark(X1), X2) -> sel(X1, X2),
              sel(active(X1), X2) -> sel(X1, X2),
               fib1(X1, mark(X2)) -> fib1(X1, X2),
             fib1(X1, active(X2)) -> fib1(X1, X2),
               fib1(mark(X1), X2) -> fib1(X1, X2),
             fib1(active(X1), X2) -> fib1(X1, X2),
                       s(mark(X)) -> s(X),
                     s(active(X)) -> s(X),
   active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
    active(sel(0(), cons(X, XS))) -> mark(X),
               active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                   active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
             active(add(s(X), Y)) -> mark(s(add(X, Y))),
              active(add(0(), X)) -> mark(X),
                     fib(mark(X)) -> fib(X),
                   fib(active(X)) -> fib(X),
               cons(X1, mark(X2)) -> cons(X1, X2),
             cons(X1, active(X2)) -> cons(X1, X2),
               cons(mark(X1), X2) -> cons(X1, X2),
             cons(active(X1), X2) -> cons(X1, X2),
                add(X1, mark(X2)) -> add(X1, X2),
              add(X1, active(X2)) -> add(X1, X2),
                add(mark(X1), X2) -> add(X1, X2),
              add(active(X1), X2) -> add(X1, X2)}
  EDG:
   {
    (mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)), fib1#(active(X1), X2) -> fib1#(X1, X2))
    (mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)), fib1#(mark(X1), X2) -> fib1#(X1, X2))
    (mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)), fib1#(X1, active(X2)) -> fib1#(X1, X2))
    (mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)), fib1#(X1, mark(X2)) -> fib1#(X1, X2))
    (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(fib(X)) -> fib#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))))
    (mark#(s(X)) -> mark#(X), mark#(fib(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(0()) -> active#(0()))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
    (s#(mark(X)) -> s#(X), s#(active(X)) -> s#(X))
    (s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib(X)) -> fib#(mark(X)))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib(X)) -> mark#(X))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(0()) -> active#(0()))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(s(X)) -> s#(mark(X)))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(s(X)) -> mark#(X))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
    (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
    (fib#(mark(X)) -> fib#(X), fib#(active(X)) -> fib#(X))
    (fib#(mark(X)) -> fib#(X), fib#(mark(X)) -> fib#(X))
    (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(active(X1), X2) -> cons#(X1, X2))
    (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(X1, active(X2)) -> cons#(X1, X2))
    (mark#(cons(X1, X2)) -> cons#(mark(X1), X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(add(s(X), Y)) -> add#(X, Y))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib(N)) -> s#(0()))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib1(X, Y)) -> add#(X, Y))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(add(0(), X)) -> mark#(X))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(add(s(X), Y)) -> add#(X, Y))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib(N)) -> s#(0()))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib1(X, Y)) -> add#(X, Y))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(sel(0(), cons(X, XS))) -> mark#(X))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (mark#(fib(X)) -> active#(fib(mark(X))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> mark#(X2))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> mark#(X1))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(cons(X1, X2)) -> mark#(X1))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib(X)) -> fib#(mark(X)))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib(X)) -> active#(fib(mark(X))))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib(X)) -> mark#(X))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(s(X)) -> active#(s(mark(X))))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(s(X)) -> s#(mark(X)))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(s(X)) -> mark#(X))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> mark#(X2))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> mark#(X1))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(sel(X1, X2)) -> mark#(X2))
    (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(sel(X1, X2)) -> mark#(X1))
    (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2))
    (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))
    (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (sel#(active(X1), X2) -> sel#(X1, X2), sel#(active(X1), X2) -> sel#(X1, X2))
    (sel#(active(X1), X2) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
    (sel#(active(X1), X2) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))
    (sel#(active(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(active(X1), X2) -> fib1#(X1, X2))
    (fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2))
    (fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2))
    (fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2))
    (fib1#(active(X1), X2) -> fib1#(X1, X2), fib1#(active(X1), X2) -> fib1#(X1, X2))
    (fib1#(active(X1), X2) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2))
    (fib1#(active(X1), X2) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2))
    (fib1#(active(X1), X2) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2))
    (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
    (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
    (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (cons#(active(X1), X2) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
    (cons#(active(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
    (cons#(active(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (add#(X1, active(X2)) -> add#(X1, X2), add#(active(X1), X2) -> add#(X1, X2))
    (add#(X1, active(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
    (add#(X1, active(X2)) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))
    (add#(X1, active(X2)) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
    (add#(active(X1), X2) -> add#(X1, X2), add#(active(X1), X2) -> add#(X1, X2))
    (add#(active(X1), X2) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
    (add#(active(X1), X2) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))
    (add#(active(X1), X2) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> mark#(X2))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> mark#(X1))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(cons(X1, X2)) -> mark#(X1))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib(X)) -> fib#(mark(X)))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib(X)) -> active#(fib(mark(X))))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib(X)) -> mark#(X))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(s(X)) -> active#(s(mark(X))))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(s(X)) -> s#(mark(X)))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(s(X)) -> mark#(X))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> mark#(X2))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> mark#(X1))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> mark#(X2))
    (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib(X)) -> fib#(mark(X)))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib(X)) -> active#(fib(mark(X))))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib(X)) -> mark#(X))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0()))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X)))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X2))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X1))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(fib(X)) -> fib#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(fib(X)) -> active#(fib(mark(X))))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(fib(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0()))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib(X)) -> fib#(mark(X)))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X))))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0()))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X)))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(fib(X)) -> fib#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X))))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0()))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> mark#(X2))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> mark#(X1))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(cons(X1, X2)) -> mark#(X1))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib(X)) -> fib#(mark(X)))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib(X)) -> active#(fib(mark(X))))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib(X)) -> mark#(X))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(s(X)) -> active#(s(mark(X))))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(s(X)) -> s#(mark(X)))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(s(X)) -> mark#(X))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> mark#(X2))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> mark#(X1))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> mark#(X2))
    (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> mark#(X1))
    (active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))), sel#(active(X1), X2) -> sel#(X1, X2))
    (active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))), sel#(mark(X1), X2) -> sel#(X1, X2))
    (mark#(s(X)) -> s#(mark(X)), s#(active(X)) -> s#(X))
    (mark#(s(X)) -> s#(mark(X)), s#(mark(X)) -> s#(X))
    (active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)), fib1#(active(X1), X2) -> fib1#(X1, X2))
    (active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)), fib1#(mark(X1), X2) -> fib1#(X1, X2))
    (active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)), fib1#(X1, active(X2)) -> fib1#(X1, X2))
    (active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)), fib1#(X1, mark(X2)) -> fib1#(X1, X2))
    (active#(add(s(X), Y)) -> add#(X, Y), add#(active(X1), X2) -> add#(X1, X2))
    (active#(add(s(X), Y)) -> add#(X, Y), add#(mark(X1), X2) -> add#(X1, X2))
    (active#(add(s(X), Y)) -> add#(X, Y), add#(X1, active(X2)) -> add#(X1, X2))
    (active#(add(s(X), Y)) -> add#(X, Y), add#(X1, mark(X2)) -> add#(X1, X2))
    (active#(fib1(X, Y)) -> add#(X, Y), add#(X1, mark(X2)) -> add#(X1, X2))
    (active#(fib1(X, Y)) -> add#(X, Y), add#(X1, active(X2)) -> add#(X1, X2))
    (active#(fib1(X, Y)) -> add#(X, Y), add#(mark(X1), X2) -> add#(X1, X2))
    (active#(fib1(X, Y)) -> add#(X, Y), add#(active(X1), X2) -> add#(X1, X2))
    (mark#(fib(X)) -> fib#(mark(X)), fib#(mark(X)) -> fib#(X))
    (mark#(fib(X)) -> fib#(mark(X)), fib#(active(X)) -> fib#(X))
    (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(X1, active(X2)) -> sel#(X1, X2))
    (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(mark(X1), X2) -> sel#(X1, X2))
    (active#(sel(s(N), cons(X, XS))) -> sel#(N, XS), sel#(active(X1), X2) -> sel#(X1, X2))
    (active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))), cons#(X1, active(X2)) -> cons#(X1, X2))
    (active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))), cons#(mark(X1), X2) -> cons#(X1, X2))
    (active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))), cons#(active(X1), X2) -> cons#(X1, X2))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> mark#(X1))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> mark#(X2))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> mark#(X1))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> mark#(X2))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(s(X)) -> mark#(X))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(s(X)) -> s#(mark(X)))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(s(X)) -> active#(s(mark(X))))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib(X)) -> mark#(X))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib(X)) -> active#(fib(mark(X))))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib(X)) -> fib#(mark(X)))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(cons(X1, X2)) -> mark#(X1))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> mark#(X1))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> mark#(X2))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0()))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X))))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib(X)) -> fib#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> s#(mark(X)))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(0()) -> active#(0()))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X))))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib(X)) -> fib#(mark(X)))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X1))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X2))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(s(X)) -> s#(mark(X)))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(0()) -> active#(0()))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib(X)) -> mark#(X))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib(X)) -> active#(fib(mark(X))))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib(X)) -> fib#(mark(X)))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> add#(mark(X1), mark(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#(active(X)) -> s#(X))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(sel(0(), cons(X, XS))) -> mark#(X))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib1(X, Y)) -> add#(X, Y))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(fib(N)) -> s#(0()))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(add(s(X), Y)) -> add#(X, Y))
    (mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)), active#(add(0(), X)) -> mark#(X))
    (add#(mark(X1), X2) -> add#(X1, X2), add#(X1, mark(X2)) -> add#(X1, X2))
    (add#(mark(X1), X2) -> add#(X1, X2), add#(X1, active(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#(active(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#(X1, active(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#(active(X1), X2) -> add#(X1, X2))
    (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, active(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#(active(X1), X2) -> cons#(X1, X2))
    (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
    (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
    (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
    (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(active(X1), X2) -> cons#(X1, X2))
    (fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(X1, mark(X2)) -> fib1#(X1, X2))
    (fib1#(mark(X1), X2) -> fib1#(X1, X2), fib1#(X1, active(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#(active(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#(X1, active(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#(active(X1), X2) -> fib1#(X1, X2))
    (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (sel#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, active(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#(active(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#(X1, active(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#(active(X1), X2) -> sel#(X1, X2))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib1(X, Y)) -> add#(X, Y))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib(N)) -> s#(0()))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(s(X), Y)) -> add#(X, Y))
    (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X))
    (mark#(s(X)) -> active#(s(mark(X))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)))
    (mark#(s(X)) -> active#(s(mark(X))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (mark#(s(X)) -> active#(s(mark(X))), active#(sel(0(), cons(X, XS))) -> mark#(X))
    (mark#(s(X)) -> active#(s(mark(X))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))))
    (mark#(s(X)) -> active#(s(mark(X))), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (mark#(s(X)) -> active#(s(mark(X))), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (mark#(s(X)) -> active#(s(mark(X))), active#(fib1(X, Y)) -> add#(X, Y))
    (mark#(s(X)) -> active#(s(mark(X))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))))
    (mark#(s(X)) -> active#(s(mark(X))), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (mark#(s(X)) -> active#(s(mark(X))), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (mark#(s(X)) -> active#(s(mark(X))), active#(fib(N)) -> s#(0()))
    (mark#(s(X)) -> active#(s(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
    (mark#(s(X)) -> active#(s(mark(X))), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (mark#(s(X)) -> active#(s(mark(X))), active#(add(s(X), Y)) -> add#(X, Y))
    (mark#(s(X)) -> active#(s(mark(X))), active#(add(0(), X)) -> mark#(X))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> sel#(N, XS))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib1(X, Y)) -> fib1#(Y, add(X, Y)))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib1(X, Y)) -> cons#(X, fib1(Y, add(X, Y))))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib1(X, Y)) -> add#(X, Y))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib(N)) -> sel#(N, fib1(s(0()), s(0()))))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib(N)) -> fib1#(s(0()), s(0())))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib(N)) -> s#(0()))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(add(s(X), Y)) -> s#(add(X, Y)))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(add(s(X), Y)) -> add#(X, Y))
    (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X))
    (fib#(active(X)) -> fib#(X), fib#(mark(X)) -> fib#(X))
    (fib#(active(X)) -> fib#(X), fib#(active(X)) -> fib#(X))
    (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
    (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
    (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1))
    (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2))
    (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (active#(add(0(), X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (active#(add(0(), X)) -> mark#(X), mark#(s(X)) -> s#(mark(X)))
    (active#(add(0(), X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))))
    (active#(add(0(), X)) -> mark#(X), mark#(0()) -> active#(0()))
    (active#(add(0(), X)) -> mark#(X), mark#(fib(X)) -> mark#(X))
    (active#(add(0(), X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))))
    (active#(add(0(), X)) -> mark#(X), mark#(fib(X)) -> fib#(mark(X)))
    (active#(add(0(), X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (active#(add(0(), X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (active#(add(0(), X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (s#(active(X)) -> s#(X), s#(mark(X)) -> s#(X))
    (s#(active(X)) -> s#(X), s#(active(X)) -> s#(X))
    (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
    (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
    (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)))
    (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
    (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1))
    (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2))
    (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> fib1#(mark(X1), mark(X2)))
    (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
    (mark#(fib(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(fib(X)) -> mark#(X), mark#(s(X)) -> s#(mark(X)))
    (mark#(fib(X)) -> mark#(X), mark#(s(X)) -> active#(s(mark(X))))
    (mark#(fib(X)) -> mark#(X), mark#(0()) -> active#(0()))
    (mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> mark#(X))
    (mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))))
    (mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> fib#(mark(X)))
    (mark#(fib(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(fib(X)) -> mark#(X), mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)))
    (mark#(fib(X)) -> mark#(X), mark#(cons(X1, X2)) -> cons#(mark(X1), X2))
    (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
    (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
    (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
    (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)))
    (mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)), add#(X1, mark(X2)) -> add#(X1, X2))
    (mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)), add#(X1, active(X2)) -> add#(X1, X2))
    (mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)), add#(mark(X1), X2) -> add#(X1, X2))
    (mark#(add(X1, X2)) -> add#(mark(X1), mark(X2)), add#(active(X1), X2) -> add#(X1, X2))
    (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(X1, mark(X2)) -> sel#(X1, X2))
    (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(X1, active(X2)) -> sel#(X1, X2))
    (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(mark(X1), X2) -> sel#(X1, X2))
    (mark#(sel(X1, X2)) -> sel#(mark(X1), mark(X2)), sel#(active(X1), X2) -> sel#(X1, X2))
   }
   SCCS:
    Scc:
     {  add#(X1, mark(X2)) -> add#(X1, X2),
      add#(X1, active(X2)) -> add#(X1, X2),
        add#(mark(X1), X2) -> add#(X1, X2),
      add#(active(X1), X2) -> add#(X1, X2)}
    Scc:
     {  cons#(X1, mark(X2)) -> cons#(X1, X2),
      cons#(X1, active(X2)) -> cons#(X1, X2),
        cons#(mark(X1), X2) -> cons#(X1, X2),
      cons#(active(X1), X2) -> cons#(X1, X2)}
    Scc:
     {  fib#(mark(X)) -> fib#(X),
      fib#(active(X)) -> fib#(X)}
    Scc:
     {  s#(mark(X)) -> s#(X),
      s#(active(X)) -> s#(X)}
    Scc:
     {  fib1#(X1, mark(X2)) -> fib1#(X1, X2),
      fib1#(X1, active(X2)) -> fib1#(X1, X2),
        fib1#(mark(X1), X2) -> fib1#(X1, X2),
      fib1#(active(X1), X2) -> fib1#(X1, X2)}
    Scc:
     {  sel#(X1, mark(X2)) -> sel#(X1, X2),
      sel#(X1, active(X2)) -> sel#(X1, X2),
        sel#(mark(X1), X2) -> sel#(X1, X2),
      sel#(active(X1), X2) -> sel#(X1, X2)}
    Scc:
     {             mark#(sel(X1, X2)) -> mark#(X1),
                   mark#(sel(X1, X2)) -> mark#(X2),
                   mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))),
                  mark#(fib1(X1, X2)) -> mark#(X1),
                  mark#(fib1(X1, X2)) -> mark#(X2),
                  mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))),
                          mark#(s(X)) -> mark#(X),
                          mark#(s(X)) -> active#(s(mark(X))),
                        mark#(fib(X)) -> mark#(X),
                        mark#(fib(X)) -> active#(fib(mark(X))),
                  mark#(cons(X1, X2)) -> mark#(X1),
                  mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
                   mark#(add(X1, X2)) -> mark#(X1),
                   mark#(add(X1, X2)) -> mark#(X2),
                   mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
      active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)),
       active#(sel(0(), cons(X, XS))) -> mark#(X),
                  active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))),
                      active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))),
                active#(add(s(X), Y)) -> mark#(s(add(X, Y))),
                 active#(add(0(), X)) -> mark#(X)}
    SCC:
     Strict:
      {  add#(X1, mark(X2)) -> add#(X1, X2),
       add#(X1, active(X2)) -> add#(X1, X2),
         add#(mark(X1), X2) -> add#(X1, X2),
       add#(active(X1), X2) -> add#(X1, X2)}
     Weak:
     {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                  mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                          mark(s(X)) -> active(s(mark(X))),
                           mark(0()) -> active(0()),
                        mark(fib(X)) -> active(fib(mark(X))),
                  mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                   mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                   sel(X1, mark(X2)) -> sel(X1, X2),
                 sel(X1, active(X2)) -> sel(X1, X2),
                   sel(mark(X1), X2) -> sel(X1, X2),
                 sel(active(X1), X2) -> sel(X1, X2),
                  fib1(X1, mark(X2)) -> fib1(X1, X2),
                fib1(X1, active(X2)) -> fib1(X1, X2),
                  fib1(mark(X1), X2) -> fib1(X1, X2),
                fib1(active(X1), X2) -> fib1(X1, X2),
                          s(mark(X)) -> s(X),
                        s(active(X)) -> s(X),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> fib(X),
                      fib(active(X)) -> fib(X),
                  cons(X1, mark(X2)) -> cons(X1, X2),
                cons(X1, active(X2)) -> cons(X1, X2),
                  cons(mark(X1), X2) -> cons(X1, X2),
                cons(active(X1), X2) -> cons(X1, X2),
                   add(X1, mark(X2)) -> add(X1, X2),
                 add(X1, active(X2)) -> add(X1, X2),
                   add(mark(X1), X2) -> add(X1, X2),
                 add(active(X1), X2) -> add(X1, X2)}
     SPSC:
      Simple Projection:
       pi(add#) = 0
      Strict:
       {  add#(X1, mark(X2)) -> add#(X1, X2),
        add#(X1, active(X2)) -> add#(X1, X2),
          add#(mark(X1), X2) -> add#(X1, X2)}
      EDG:
       {(add#(X1, active(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))
        (add#(X1, active(X2)) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))
        (add#(X1, active(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#(mark(X1), X2) -> add#(X1, X2), add#(X1, active(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#(X1, mark(X2)) -> add#(X1, X2))
        (add#(X1, mark(X2)) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))
        (add#(X1, mark(X2)) -> add#(X1, X2), add#(mark(X1), X2) -> add#(X1, X2))}
       SCCS:
        Scc:
         {  add#(X1, mark(X2)) -> add#(X1, X2),
          add#(X1, active(X2)) -> add#(X1, X2),
            add#(mark(X1), X2) -> add#(X1, X2)}
        SCC:
         Strict:
          {  add#(X1, mark(X2)) -> add#(X1, X2),
           add#(X1, active(X2)) -> add#(X1, X2),
             add#(mark(X1), X2) -> add#(X1, X2)}
         Weak:
         {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                      mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                              mark(s(X)) -> active(s(mark(X))),
                               mark(0()) -> active(0()),
                            mark(fib(X)) -> active(fib(mark(X))),
                      mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                       mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                       sel(X1, mark(X2)) -> sel(X1, X2),
                     sel(X1, active(X2)) -> sel(X1, X2),
                       sel(mark(X1), X2) -> sel(X1, X2),
                     sel(active(X1), X2) -> sel(X1, X2),
                      fib1(X1, mark(X2)) -> fib1(X1, X2),
                    fib1(X1, active(X2)) -> fib1(X1, X2),
                      fib1(mark(X1), X2) -> fib1(X1, X2),
                    fib1(active(X1), X2) -> fib1(X1, X2),
                              s(mark(X)) -> s(X),
                            s(active(X)) -> s(X),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> fib(X),
                          fib(active(X)) -> fib(X),
                      cons(X1, mark(X2)) -> cons(X1, X2),
                    cons(X1, active(X2)) -> cons(X1, X2),
                      cons(mark(X1), X2) -> cons(X1, X2),
                    cons(active(X1), X2) -> cons(X1, X2),
                       add(X1, mark(X2)) -> add(X1, X2),
                     add(X1, active(X2)) -> add(X1, X2),
                       add(mark(X1), X2) -> add(X1, X2),
                     add(active(X1), X2) -> add(X1, X2)}
         SPSC:
          Simple Projection:
           pi(add#) = 0
          Strict:
           {  add#(X1, mark(X2)) -> add#(X1, X2),
            add#(X1, active(X2)) -> add#(X1, X2)}
          EDG:
           {(add#(X1, active(X2)) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))
            (add#(X1, active(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#(X1, mark(X2)) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))}
           SCCS:
            Scc:
             {  add#(X1, mark(X2)) -> add#(X1, X2),
              add#(X1, active(X2)) -> add#(X1, X2)}
            SCC:
             Strict:
              {  add#(X1, mark(X2)) -> add#(X1, X2),
               add#(X1, active(X2)) -> add#(X1, X2)}
             Weak:
             {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                          mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                                  mark(s(X)) -> active(s(mark(X))),
                                   mark(0()) -> active(0()),
                                mark(fib(X)) -> active(fib(mark(X))),
                          mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                           mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                           sel(X1, mark(X2)) -> sel(X1, X2),
                         sel(X1, active(X2)) -> sel(X1, X2),
                           sel(mark(X1), X2) -> sel(X1, X2),
                         sel(active(X1), X2) -> sel(X1, X2),
                          fib1(X1, mark(X2)) -> fib1(X1, X2),
                        fib1(X1, active(X2)) -> fib1(X1, X2),
                          fib1(mark(X1), X2) -> fib1(X1, X2),
                        fib1(active(X1), X2) -> fib1(X1, X2),
                                  s(mark(X)) -> s(X),
                                s(active(X)) -> s(X),
              active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
               active(sel(0(), cons(X, XS))) -> mark(X),
                          active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                              active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                         active(add(0(), X)) -> mark(X),
                                fib(mark(X)) -> fib(X),
                              fib(active(X)) -> fib(X),
                          cons(X1, mark(X2)) -> cons(X1, X2),
                        cons(X1, active(X2)) -> cons(X1, X2),
                          cons(mark(X1), X2) -> cons(X1, X2),
                        cons(active(X1), X2) -> cons(X1, X2),
                           add(X1, mark(X2)) -> add(X1, X2),
                         add(X1, active(X2)) -> add(X1, X2),
                           add(mark(X1), X2) -> add(X1, X2),
                         add(active(X1), X2) -> add(X1, X2)}
             SPSC:
              Simple Projection:
               pi(add#) = 1
              Strict:
               {add#(X1, active(X2)) -> add#(X1, X2)}
              EDG:
               {(add#(X1, active(X2)) -> add#(X1, X2), add#(X1, active(X2)) -> add#(X1, X2))}
               SCCS:
                Scc:
                 {add#(X1, active(X2)) -> add#(X1, X2)}
                SCC:
                 Strict:
                  {add#(X1, active(X2)) -> add#(X1, X2)}
                 Weak:
                 {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                              mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                                      mark(s(X)) -> active(s(mark(X))),
                                       mark(0()) -> active(0()),
                                    mark(fib(X)) -> active(fib(mark(X))),
                              mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                               mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                               sel(X1, mark(X2)) -> sel(X1, X2),
                             sel(X1, active(X2)) -> sel(X1, X2),
                               sel(mark(X1), X2) -> sel(X1, X2),
                             sel(active(X1), X2) -> sel(X1, X2),
                              fib1(X1, mark(X2)) -> fib1(X1, X2),
                            fib1(X1, active(X2)) -> fib1(X1, X2),
                              fib1(mark(X1), X2) -> fib1(X1, X2),
                            fib1(active(X1), X2) -> fib1(X1, X2),
                                      s(mark(X)) -> s(X),
                                    s(active(X)) -> s(X),
                  active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                   active(sel(0(), cons(X, XS))) -> mark(X),
                              active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                  active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                            active(add(s(X), Y)) -> mark(s(add(X, Y))),
                             active(add(0(), X)) -> mark(X),
                                    fib(mark(X)) -> fib(X),
                                  fib(active(X)) -> fib(X),
                              cons(X1, mark(X2)) -> cons(X1, X2),
                            cons(X1, active(X2)) -> cons(X1, X2),
                              cons(mark(X1), X2) -> cons(X1, X2),
                            cons(active(X1), X2) -> cons(X1, X2),
                               add(X1, mark(X2)) -> add(X1, X2),
                             add(X1, active(X2)) -> add(X1, X2),
                               add(mark(X1), X2) -> add(X1, X2),
                             add(active(X1), X2) -> add(X1, X2)}
                 SPSC:
                  Simple Projection:
                   pi(add#) = 1
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {  cons#(X1, mark(X2)) -> cons#(X1, X2),
       cons#(X1, active(X2)) -> cons#(X1, X2),
         cons#(mark(X1), X2) -> cons#(X1, X2),
       cons#(active(X1), X2) -> cons#(X1, X2)}
     Weak:
     {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                  mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                          mark(s(X)) -> active(s(mark(X))),
                           mark(0()) -> active(0()),
                        mark(fib(X)) -> active(fib(mark(X))),
                  mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                   mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                   sel(X1, mark(X2)) -> sel(X1, X2),
                 sel(X1, active(X2)) -> sel(X1, X2),
                   sel(mark(X1), X2) -> sel(X1, X2),
                 sel(active(X1), X2) -> sel(X1, X2),
                  fib1(X1, mark(X2)) -> fib1(X1, X2),
                fib1(X1, active(X2)) -> fib1(X1, X2),
                  fib1(mark(X1), X2) -> fib1(X1, X2),
                fib1(active(X1), X2) -> fib1(X1, X2),
                          s(mark(X)) -> s(X),
                        s(active(X)) -> s(X),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> fib(X),
                      fib(active(X)) -> fib(X),
                  cons(X1, mark(X2)) -> cons(X1, X2),
                cons(X1, active(X2)) -> cons(X1, X2),
                  cons(mark(X1), X2) -> cons(X1, X2),
                cons(active(X1), X2) -> cons(X1, X2),
                   add(X1, mark(X2)) -> add(X1, X2),
                 add(X1, active(X2)) -> add(X1, X2),
                   add(mark(X1), X2) -> add(X1, X2),
                 add(active(X1), X2) -> add(X1, X2)}
     SPSC:
      Simple Projection:
       pi(cons#) = 0
      Strict:
       {  cons#(X1, mark(X2)) -> cons#(X1, X2),
        cons#(X1, active(X2)) -> cons#(X1, X2),
          cons#(mark(X1), X2) -> cons#(X1, X2)}
      EDG:
       {(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
        (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
        (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
        (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
        (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
        (cons#(mark(X1), X2) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))
        (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
        (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
        (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(mark(X1), X2) -> cons#(X1, X2))}
       SCCS:
        Scc:
         {  cons#(X1, mark(X2)) -> cons#(X1, X2),
          cons#(X1, active(X2)) -> cons#(X1, X2),
            cons#(mark(X1), X2) -> cons#(X1, X2)}
        SCC:
         Strict:
          {  cons#(X1, mark(X2)) -> cons#(X1, X2),
           cons#(X1, active(X2)) -> cons#(X1, X2),
             cons#(mark(X1), X2) -> cons#(X1, X2)}
         Weak:
         {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                      mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                              mark(s(X)) -> active(s(mark(X))),
                               mark(0()) -> active(0()),
                            mark(fib(X)) -> active(fib(mark(X))),
                      mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                       mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                       sel(X1, mark(X2)) -> sel(X1, X2),
                     sel(X1, active(X2)) -> sel(X1, X2),
                       sel(mark(X1), X2) -> sel(X1, X2),
                     sel(active(X1), X2) -> sel(X1, X2),
                      fib1(X1, mark(X2)) -> fib1(X1, X2),
                    fib1(X1, active(X2)) -> fib1(X1, X2),
                      fib1(mark(X1), X2) -> fib1(X1, X2),
                    fib1(active(X1), X2) -> fib1(X1, X2),
                              s(mark(X)) -> s(X),
                            s(active(X)) -> s(X),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> fib(X),
                          fib(active(X)) -> fib(X),
                      cons(X1, mark(X2)) -> cons(X1, X2),
                    cons(X1, active(X2)) -> cons(X1, X2),
                      cons(mark(X1), X2) -> cons(X1, X2),
                    cons(active(X1), X2) -> cons(X1, X2),
                       add(X1, mark(X2)) -> add(X1, X2),
                     add(X1, active(X2)) -> add(X1, X2),
                       add(mark(X1), X2) -> add(X1, X2),
                     add(active(X1), X2) -> add(X1, X2)}
         SPSC:
          Simple Projection:
           pi(cons#) = 0
          Strict:
           {  cons#(X1, mark(X2)) -> cons#(X1, X2),
            cons#(X1, active(X2)) -> cons#(X1, X2)}
          EDG:
           {(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))
            (cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
            (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, mark(X2)) -> cons#(X1, X2))
            (cons#(X1, mark(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))}
           SCCS:
            Scc:
             {  cons#(X1, mark(X2)) -> cons#(X1, X2),
              cons#(X1, active(X2)) -> cons#(X1, X2)}
            SCC:
             Strict:
              {  cons#(X1, mark(X2)) -> cons#(X1, X2),
               cons#(X1, active(X2)) -> cons#(X1, X2)}
             Weak:
             {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                          mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                                  mark(s(X)) -> active(s(mark(X))),
                                   mark(0()) -> active(0()),
                                mark(fib(X)) -> active(fib(mark(X))),
                          mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                           mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                           sel(X1, mark(X2)) -> sel(X1, X2),
                         sel(X1, active(X2)) -> sel(X1, X2),
                           sel(mark(X1), X2) -> sel(X1, X2),
                         sel(active(X1), X2) -> sel(X1, X2),
                          fib1(X1, mark(X2)) -> fib1(X1, X2),
                        fib1(X1, active(X2)) -> fib1(X1, X2),
                          fib1(mark(X1), X2) -> fib1(X1, X2),
                        fib1(active(X1), X2) -> fib1(X1, X2),
                                  s(mark(X)) -> s(X),
                                s(active(X)) -> s(X),
              active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
               active(sel(0(), cons(X, XS))) -> mark(X),
                          active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                              active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                         active(add(0(), X)) -> mark(X),
                                fib(mark(X)) -> fib(X),
                              fib(active(X)) -> fib(X),
                          cons(X1, mark(X2)) -> cons(X1, X2),
                        cons(X1, active(X2)) -> cons(X1, X2),
                          cons(mark(X1), X2) -> cons(X1, X2),
                        cons(active(X1), X2) -> cons(X1, X2),
                           add(X1, mark(X2)) -> add(X1, X2),
                         add(X1, active(X2)) -> add(X1, X2),
                           add(mark(X1), X2) -> add(X1, X2),
                         add(active(X1), X2) -> add(X1, X2)}
             SPSC:
              Simple Projection:
               pi(cons#) = 1
              Strict:
               {cons#(X1, active(X2)) -> cons#(X1, X2)}
              EDG:
               {(cons#(X1, active(X2)) -> cons#(X1, X2), cons#(X1, active(X2)) -> cons#(X1, X2))}
               SCCS:
                Scc:
                 {cons#(X1, active(X2)) -> cons#(X1, X2)}
                SCC:
                 Strict:
                  {cons#(X1, active(X2)) -> cons#(X1, X2)}
                 Weak:
                 {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                              mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                                      mark(s(X)) -> active(s(mark(X))),
                                       mark(0()) -> active(0()),
                                    mark(fib(X)) -> active(fib(mark(X))),
                              mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                               mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                               sel(X1, mark(X2)) -> sel(X1, X2),
                             sel(X1, active(X2)) -> sel(X1, X2),
                               sel(mark(X1), X2) -> sel(X1, X2),
                             sel(active(X1), X2) -> sel(X1, X2),
                              fib1(X1, mark(X2)) -> fib1(X1, X2),
                            fib1(X1, active(X2)) -> fib1(X1, X2),
                              fib1(mark(X1), X2) -> fib1(X1, X2),
                            fib1(active(X1), X2) -> fib1(X1, X2),
                                      s(mark(X)) -> s(X),
                                    s(active(X)) -> s(X),
                  active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                   active(sel(0(), cons(X, XS))) -> mark(X),
                              active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                  active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                            active(add(s(X), Y)) -> mark(s(add(X, Y))),
                             active(add(0(), X)) -> mark(X),
                                    fib(mark(X)) -> fib(X),
                                  fib(active(X)) -> fib(X),
                              cons(X1, mark(X2)) -> cons(X1, X2),
                            cons(X1, active(X2)) -> cons(X1, X2),
                              cons(mark(X1), X2) -> cons(X1, X2),
                            cons(active(X1), X2) -> cons(X1, X2),
                               add(X1, mark(X2)) -> add(X1, X2),
                             add(X1, active(X2)) -> add(X1, X2),
                               add(mark(X1), X2) -> add(X1, X2),
                             add(active(X1), X2) -> add(X1, X2)}
                 SPSC:
                  Simple Projection:
                   pi(cons#) = 1
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {  fib#(mark(X)) -> fib#(X),
       fib#(active(X)) -> fib#(X)}
     Weak:
     {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                  mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                          mark(s(X)) -> active(s(mark(X))),
                           mark(0()) -> active(0()),
                        mark(fib(X)) -> active(fib(mark(X))),
                  mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                   mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                   sel(X1, mark(X2)) -> sel(X1, X2),
                 sel(X1, active(X2)) -> sel(X1, X2),
                   sel(mark(X1), X2) -> sel(X1, X2),
                 sel(active(X1), X2) -> sel(X1, X2),
                  fib1(X1, mark(X2)) -> fib1(X1, X2),
                fib1(X1, active(X2)) -> fib1(X1, X2),
                  fib1(mark(X1), X2) -> fib1(X1, X2),
                fib1(active(X1), X2) -> fib1(X1, X2),
                          s(mark(X)) -> s(X),
                        s(active(X)) -> s(X),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> fib(X),
                      fib(active(X)) -> fib(X),
                  cons(X1, mark(X2)) -> cons(X1, X2),
                cons(X1, active(X2)) -> cons(X1, X2),
                  cons(mark(X1), X2) -> cons(X1, X2),
                cons(active(X1), X2) -> cons(X1, X2),
                   add(X1, mark(X2)) -> add(X1, X2),
                 add(X1, active(X2)) -> add(X1, X2),
                   add(mark(X1), X2) -> add(X1, X2),
                 add(active(X1), X2) -> add(X1, X2)}
     SPSC:
      Simple Projection:
       pi(fib#) = 0
      Strict:
       {fib#(active(X)) -> fib#(X)}
      EDG:
       {(fib#(active(X)) -> fib#(X), fib#(active(X)) -> fib#(X))}
       SCCS:
        Scc:
         {fib#(active(X)) -> fib#(X)}
        SCC:
         Strict:
          {fib#(active(X)) -> fib#(X)}
         Weak:
         {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                      mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                              mark(s(X)) -> active(s(mark(X))),
                               mark(0()) -> active(0()),
                            mark(fib(X)) -> active(fib(mark(X))),
                      mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                       mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                       sel(X1, mark(X2)) -> sel(X1, X2),
                     sel(X1, active(X2)) -> sel(X1, X2),
                       sel(mark(X1), X2) -> sel(X1, X2),
                     sel(active(X1), X2) -> sel(X1, X2),
                      fib1(X1, mark(X2)) -> fib1(X1, X2),
                    fib1(X1, active(X2)) -> fib1(X1, X2),
                      fib1(mark(X1), X2) -> fib1(X1, X2),
                    fib1(active(X1), X2) -> fib1(X1, X2),
                              s(mark(X)) -> s(X),
                            s(active(X)) -> s(X),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> fib(X),
                          fib(active(X)) -> fib(X),
                      cons(X1, mark(X2)) -> cons(X1, X2),
                    cons(X1, active(X2)) -> cons(X1, X2),
                      cons(mark(X1), X2) -> cons(X1, X2),
                    cons(active(X1), X2) -> cons(X1, X2),
                       add(X1, mark(X2)) -> add(X1, X2),
                     add(X1, active(X2)) -> add(X1, X2),
                       add(mark(X1), X2) -> add(X1, X2),
                     add(active(X1), X2) -> add(X1, X2)}
         SPSC:
          Simple Projection:
           pi(fib#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  s#(mark(X)) -> s#(X),
       s#(active(X)) -> s#(X)}
     Weak:
     {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                  mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                          mark(s(X)) -> active(s(mark(X))),
                           mark(0()) -> active(0()),
                        mark(fib(X)) -> active(fib(mark(X))),
                  mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                   mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                   sel(X1, mark(X2)) -> sel(X1, X2),
                 sel(X1, active(X2)) -> sel(X1, X2),
                   sel(mark(X1), X2) -> sel(X1, X2),
                 sel(active(X1), X2) -> sel(X1, X2),
                  fib1(X1, mark(X2)) -> fib1(X1, X2),
                fib1(X1, active(X2)) -> fib1(X1, X2),
                  fib1(mark(X1), X2) -> fib1(X1, X2),
                fib1(active(X1), X2) -> fib1(X1, X2),
                          s(mark(X)) -> s(X),
                        s(active(X)) -> s(X),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> fib(X),
                      fib(active(X)) -> fib(X),
                  cons(X1, mark(X2)) -> cons(X1, X2),
                cons(X1, active(X2)) -> cons(X1, X2),
                  cons(mark(X1), X2) -> cons(X1, X2),
                cons(active(X1), X2) -> cons(X1, X2),
                   add(X1, mark(X2)) -> add(X1, X2),
                 add(X1, active(X2)) -> add(X1, X2),
                   add(mark(X1), X2) -> add(X1, X2),
                 add(active(X1), X2) -> add(X1, X2)}
     SPSC:
      Simple Projection:
       pi(s#) = 0
      Strict:
       {s#(mark(X)) -> s#(X)}
      EDG:
       {(s#(mark(X)) -> s#(X), s#(mark(X)) -> s#(X))}
       SCCS:
        Scc:
         {s#(mark(X)) -> s#(X)}
        SCC:
         Strict:
          {s#(mark(X)) -> s#(X)}
         Weak:
         {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                      mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                              mark(s(X)) -> active(s(mark(X))),
                               mark(0()) -> active(0()),
                            mark(fib(X)) -> active(fib(mark(X))),
                      mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                       mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                       sel(X1, mark(X2)) -> sel(X1, X2),
                     sel(X1, active(X2)) -> sel(X1, X2),
                       sel(mark(X1), X2) -> sel(X1, X2),
                     sel(active(X1), X2) -> sel(X1, X2),
                      fib1(X1, mark(X2)) -> fib1(X1, X2),
                    fib1(X1, active(X2)) -> fib1(X1, X2),
                      fib1(mark(X1), X2) -> fib1(X1, X2),
                    fib1(active(X1), X2) -> fib1(X1, X2),
                              s(mark(X)) -> s(X),
                            s(active(X)) -> s(X),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> fib(X),
                          fib(active(X)) -> fib(X),
                      cons(X1, mark(X2)) -> cons(X1, X2),
                    cons(X1, active(X2)) -> cons(X1, X2),
                      cons(mark(X1), X2) -> cons(X1, X2),
                    cons(active(X1), X2) -> cons(X1, X2),
                       add(X1, mark(X2)) -> add(X1, X2),
                     add(X1, active(X2)) -> add(X1, X2),
                       add(mark(X1), X2) -> add(X1, X2),
                     add(active(X1), X2) -> add(X1, X2)}
         SPSC:
          Simple Projection:
           pi(s#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  fib1#(X1, mark(X2)) -> fib1#(X1, X2),
       fib1#(X1, active(X2)) -> fib1#(X1, X2),
         fib1#(mark(X1), X2) -> fib1#(X1, X2),
       fib1#(active(X1), X2) -> fib1#(X1, X2)}
     Weak:
     {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                  mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                          mark(s(X)) -> active(s(mark(X))),
                           mark(0()) -> active(0()),
                        mark(fib(X)) -> active(fib(mark(X))),
                  mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                   mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                   sel(X1, mark(X2)) -> sel(X1, X2),
                 sel(X1, active(X2)) -> sel(X1, X2),
                   sel(mark(X1), X2) -> sel(X1, X2),
                 sel(active(X1), X2) -> sel(X1, X2),
                  fib1(X1, mark(X2)) -> fib1(X1, X2),
                fib1(X1, active(X2)) -> fib1(X1, X2),
                  fib1(mark(X1), X2) -> fib1(X1, X2),
                fib1(active(X1), X2) -> fib1(X1, X2),
                          s(mark(X)) -> s(X),
                        s(active(X)) -> s(X),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> fib(X),
                      fib(active(X)) -> fib(X),
                  cons(X1, mark(X2)) -> cons(X1, X2),
                cons(X1, active(X2)) -> cons(X1, X2),
                  cons(mark(X1), X2) -> cons(X1, X2),
                cons(active(X1), X2) -> cons(X1, X2),
                   add(X1, mark(X2)) -> add(X1, X2),
                 add(X1, active(X2)) -> add(X1, X2),
                   add(mark(X1), X2) -> add(X1, X2),
                 add(active(X1), X2) -> add(X1, X2)}
     SPSC:
      Simple Projection:
       pi(fib1#) = 0
      Strict:
       {  fib1#(X1, mark(X2)) -> fib1#(X1, X2),
        fib1#(X1, active(X2)) -> fib1#(X1, X2),
          fib1#(mark(X1), X2) -> fib1#(X1, X2)}
      EDG:
       {(fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2))
        (fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2))
        (fib1#(X1, active(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#(mark(X1), X2) -> fib1#(X1, X2), fib1#(X1, active(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#(X1, mark(X2)) -> fib1#(X1, X2))
        (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2))
        (fib1#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(mark(X1), X2) -> fib1#(X1, X2))}
       SCCS:
        Scc:
         {  fib1#(X1, mark(X2)) -> fib1#(X1, X2),
          fib1#(X1, active(X2)) -> fib1#(X1, X2),
            fib1#(mark(X1), X2) -> fib1#(X1, X2)}
        SCC:
         Strict:
          {  fib1#(X1, mark(X2)) -> fib1#(X1, X2),
           fib1#(X1, active(X2)) -> fib1#(X1, X2),
             fib1#(mark(X1), X2) -> fib1#(X1, X2)}
         Weak:
         {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                      mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                              mark(s(X)) -> active(s(mark(X))),
                               mark(0()) -> active(0()),
                            mark(fib(X)) -> active(fib(mark(X))),
                      mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                       mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                       sel(X1, mark(X2)) -> sel(X1, X2),
                     sel(X1, active(X2)) -> sel(X1, X2),
                       sel(mark(X1), X2) -> sel(X1, X2),
                     sel(active(X1), X2) -> sel(X1, X2),
                      fib1(X1, mark(X2)) -> fib1(X1, X2),
                    fib1(X1, active(X2)) -> fib1(X1, X2),
                      fib1(mark(X1), X2) -> fib1(X1, X2),
                    fib1(active(X1), X2) -> fib1(X1, X2),
                              s(mark(X)) -> s(X),
                            s(active(X)) -> s(X),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> fib(X),
                          fib(active(X)) -> fib(X),
                      cons(X1, mark(X2)) -> cons(X1, X2),
                    cons(X1, active(X2)) -> cons(X1, X2),
                      cons(mark(X1), X2) -> cons(X1, X2),
                    cons(active(X1), X2) -> cons(X1, X2),
                       add(X1, mark(X2)) -> add(X1, X2),
                     add(X1, active(X2)) -> add(X1, X2),
                       add(mark(X1), X2) -> add(X1, X2),
                     add(active(X1), X2) -> add(X1, X2)}
         SPSC:
          Simple Projection:
           pi(fib1#) = 0
          Strict:
           {  fib1#(X1, mark(X2)) -> fib1#(X1, X2),
            fib1#(X1, active(X2)) -> fib1#(X1, X2)}
          EDG:
           {(fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2))
            (fib1#(X1, active(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#(X1, mark(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2))}
           SCCS:
            Scc:
             {  fib1#(X1, mark(X2)) -> fib1#(X1, X2),
              fib1#(X1, active(X2)) -> fib1#(X1, X2)}
            SCC:
             Strict:
              {  fib1#(X1, mark(X2)) -> fib1#(X1, X2),
               fib1#(X1, active(X2)) -> fib1#(X1, X2)}
             Weak:
             {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                          mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                                  mark(s(X)) -> active(s(mark(X))),
                                   mark(0()) -> active(0()),
                                mark(fib(X)) -> active(fib(mark(X))),
                          mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                           mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                           sel(X1, mark(X2)) -> sel(X1, X2),
                         sel(X1, active(X2)) -> sel(X1, X2),
                           sel(mark(X1), X2) -> sel(X1, X2),
                         sel(active(X1), X2) -> sel(X1, X2),
                          fib1(X1, mark(X2)) -> fib1(X1, X2),
                        fib1(X1, active(X2)) -> fib1(X1, X2),
                          fib1(mark(X1), X2) -> fib1(X1, X2),
                        fib1(active(X1), X2) -> fib1(X1, X2),
                                  s(mark(X)) -> s(X),
                                s(active(X)) -> s(X),
              active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
               active(sel(0(), cons(X, XS))) -> mark(X),
                          active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                              active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                         active(add(0(), X)) -> mark(X),
                                fib(mark(X)) -> fib(X),
                              fib(active(X)) -> fib(X),
                          cons(X1, mark(X2)) -> cons(X1, X2),
                        cons(X1, active(X2)) -> cons(X1, X2),
                          cons(mark(X1), X2) -> cons(X1, X2),
                        cons(active(X1), X2) -> cons(X1, X2),
                           add(X1, mark(X2)) -> add(X1, X2),
                         add(X1, active(X2)) -> add(X1, X2),
                           add(mark(X1), X2) -> add(X1, X2),
                         add(active(X1), X2) -> add(X1, X2)}
             SPSC:
              Simple Projection:
               pi(fib1#) = 1
              Strict:
               {fib1#(X1, active(X2)) -> fib1#(X1, X2)}
              EDG:
               {(fib1#(X1, active(X2)) -> fib1#(X1, X2), fib1#(X1, active(X2)) -> fib1#(X1, X2))}
               SCCS:
                Scc:
                 {fib1#(X1, active(X2)) -> fib1#(X1, X2)}
                SCC:
                 Strict:
                  {fib1#(X1, active(X2)) -> fib1#(X1, X2)}
                 Weak:
                 {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                              mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                                      mark(s(X)) -> active(s(mark(X))),
                                       mark(0()) -> active(0()),
                                    mark(fib(X)) -> active(fib(mark(X))),
                              mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                               mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                               sel(X1, mark(X2)) -> sel(X1, X2),
                             sel(X1, active(X2)) -> sel(X1, X2),
                               sel(mark(X1), X2) -> sel(X1, X2),
                             sel(active(X1), X2) -> sel(X1, X2),
                              fib1(X1, mark(X2)) -> fib1(X1, X2),
                            fib1(X1, active(X2)) -> fib1(X1, X2),
                              fib1(mark(X1), X2) -> fib1(X1, X2),
                            fib1(active(X1), X2) -> fib1(X1, X2),
                                      s(mark(X)) -> s(X),
                                    s(active(X)) -> s(X),
                  active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                   active(sel(0(), cons(X, XS))) -> mark(X),
                              active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                  active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                            active(add(s(X), Y)) -> mark(s(add(X, Y))),
                             active(add(0(), X)) -> mark(X),
                                    fib(mark(X)) -> fib(X),
                                  fib(active(X)) -> fib(X),
                              cons(X1, mark(X2)) -> cons(X1, X2),
                            cons(X1, active(X2)) -> cons(X1, X2),
                              cons(mark(X1), X2) -> cons(X1, X2),
                            cons(active(X1), X2) -> cons(X1, X2),
                               add(X1, mark(X2)) -> add(X1, X2),
                             add(X1, active(X2)) -> add(X1, X2),
                               add(mark(X1), X2) -> add(X1, X2),
                             add(active(X1), X2) -> add(X1, X2)}
                 SPSC:
                  Simple Projection:
                   pi(fib1#) = 1
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {  sel#(X1, mark(X2)) -> sel#(X1, X2),
       sel#(X1, active(X2)) -> sel#(X1, X2),
         sel#(mark(X1), X2) -> sel#(X1, X2),
       sel#(active(X1), X2) -> sel#(X1, X2)}
     Weak:
     {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                  mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                          mark(s(X)) -> active(s(mark(X))),
                           mark(0()) -> active(0()),
                        mark(fib(X)) -> active(fib(mark(X))),
                  mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                   mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                   sel(X1, mark(X2)) -> sel(X1, X2),
                 sel(X1, active(X2)) -> sel(X1, X2),
                   sel(mark(X1), X2) -> sel(X1, X2),
                 sel(active(X1), X2) -> sel(X1, X2),
                  fib1(X1, mark(X2)) -> fib1(X1, X2),
                fib1(X1, active(X2)) -> fib1(X1, X2),
                  fib1(mark(X1), X2) -> fib1(X1, X2),
                fib1(active(X1), X2) -> fib1(X1, X2),
                          s(mark(X)) -> s(X),
                        s(active(X)) -> s(X),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> fib(X),
                      fib(active(X)) -> fib(X),
                  cons(X1, mark(X2)) -> cons(X1, X2),
                cons(X1, active(X2)) -> cons(X1, X2),
                  cons(mark(X1), X2) -> cons(X1, X2),
                cons(active(X1), X2) -> cons(X1, X2),
                   add(X1, mark(X2)) -> add(X1, X2),
                 add(X1, active(X2)) -> add(X1, X2),
                   add(mark(X1), X2) -> add(X1, X2),
                 add(active(X1), X2) -> add(X1, X2)}
     SPSC:
      Simple Projection:
       pi(sel#) = 0
      Strict:
       {  sel#(X1, mark(X2)) -> sel#(X1, X2),
        sel#(X1, active(X2)) -> sel#(X1, X2),
          sel#(mark(X1), X2) -> sel#(X1, X2)}
      EDG:
       {(sel#(X1, active(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))
        (sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))
        (sel#(X1, active(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#(mark(X1), X2) -> sel#(X1, X2), sel#(X1, active(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#(X1, mark(X2)) -> sel#(X1, X2))
        (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))
        (sel#(X1, mark(X2)) -> sel#(X1, X2), sel#(mark(X1), X2) -> sel#(X1, X2))}
       SCCS:
        Scc:
         {  sel#(X1, mark(X2)) -> sel#(X1, X2),
          sel#(X1, active(X2)) -> sel#(X1, X2),
            sel#(mark(X1), X2) -> sel#(X1, X2)}
        SCC:
         Strict:
          {  sel#(X1, mark(X2)) -> sel#(X1, X2),
           sel#(X1, active(X2)) -> sel#(X1, X2),
             sel#(mark(X1), X2) -> sel#(X1, X2)}
         Weak:
         {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                      mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                              mark(s(X)) -> active(s(mark(X))),
                               mark(0()) -> active(0()),
                            mark(fib(X)) -> active(fib(mark(X))),
                      mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                       mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                       sel(X1, mark(X2)) -> sel(X1, X2),
                     sel(X1, active(X2)) -> sel(X1, X2),
                       sel(mark(X1), X2) -> sel(X1, X2),
                     sel(active(X1), X2) -> sel(X1, X2),
                      fib1(X1, mark(X2)) -> fib1(X1, X2),
                    fib1(X1, active(X2)) -> fib1(X1, X2),
                      fib1(mark(X1), X2) -> fib1(X1, X2),
                    fib1(active(X1), X2) -> fib1(X1, X2),
                              s(mark(X)) -> s(X),
                            s(active(X)) -> s(X),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> fib(X),
                          fib(active(X)) -> fib(X),
                      cons(X1, mark(X2)) -> cons(X1, X2),
                    cons(X1, active(X2)) -> cons(X1, X2),
                      cons(mark(X1), X2) -> cons(X1, X2),
                    cons(active(X1), X2) -> cons(X1, X2),
                       add(X1, mark(X2)) -> add(X1, X2),
                     add(X1, active(X2)) -> add(X1, X2),
                       add(mark(X1), X2) -> add(X1, X2),
                     add(active(X1), X2) -> add(X1, X2)}
         SPSC:
          Simple Projection:
           pi(sel#) = 0
          Strict:
           {  sel#(X1, mark(X2)) -> sel#(X1, X2),
            sel#(X1, active(X2)) -> sel#(X1, X2)}
          EDG:
           {(sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))
            (sel#(X1, active(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#(X1, mark(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))}
           SCCS:
            Scc:
             {  sel#(X1, mark(X2)) -> sel#(X1, X2),
              sel#(X1, active(X2)) -> sel#(X1, X2)}
            SCC:
             Strict:
              {  sel#(X1, mark(X2)) -> sel#(X1, X2),
               sel#(X1, active(X2)) -> sel#(X1, X2)}
             Weak:
             {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                          mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                                  mark(s(X)) -> active(s(mark(X))),
                                   mark(0()) -> active(0()),
                                mark(fib(X)) -> active(fib(mark(X))),
                          mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                           mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                           sel(X1, mark(X2)) -> sel(X1, X2),
                         sel(X1, active(X2)) -> sel(X1, X2),
                           sel(mark(X1), X2) -> sel(X1, X2),
                         sel(active(X1), X2) -> sel(X1, X2),
                          fib1(X1, mark(X2)) -> fib1(X1, X2),
                        fib1(X1, active(X2)) -> fib1(X1, X2),
                          fib1(mark(X1), X2) -> fib1(X1, X2),
                        fib1(active(X1), X2) -> fib1(X1, X2),
                                  s(mark(X)) -> s(X),
                                s(active(X)) -> s(X),
              active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
               active(sel(0(), cons(X, XS))) -> mark(X),
                          active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                              active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                        active(add(s(X), Y)) -> mark(s(add(X, Y))),
                         active(add(0(), X)) -> mark(X),
                                fib(mark(X)) -> fib(X),
                              fib(active(X)) -> fib(X),
                          cons(X1, mark(X2)) -> cons(X1, X2),
                        cons(X1, active(X2)) -> cons(X1, X2),
                          cons(mark(X1), X2) -> cons(X1, X2),
                        cons(active(X1), X2) -> cons(X1, X2),
                           add(X1, mark(X2)) -> add(X1, X2),
                         add(X1, active(X2)) -> add(X1, X2),
                           add(mark(X1), X2) -> add(X1, X2),
                         add(active(X1), X2) -> add(X1, X2)}
             SPSC:
              Simple Projection:
               pi(sel#) = 1
              Strict:
               {sel#(X1, active(X2)) -> sel#(X1, X2)}
              EDG:
               {(sel#(X1, active(X2)) -> sel#(X1, X2), sel#(X1, active(X2)) -> sel#(X1, X2))}
               SCCS:
                Scc:
                 {sel#(X1, active(X2)) -> sel#(X1, X2)}
                SCC:
                 Strict:
                  {sel#(X1, active(X2)) -> sel#(X1, X2)}
                 Weak:
                 {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                              mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                                      mark(s(X)) -> active(s(mark(X))),
                                       mark(0()) -> active(0()),
                                    mark(fib(X)) -> active(fib(mark(X))),
                              mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                               mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                               sel(X1, mark(X2)) -> sel(X1, X2),
                             sel(X1, active(X2)) -> sel(X1, X2),
                               sel(mark(X1), X2) -> sel(X1, X2),
                             sel(active(X1), X2) -> sel(X1, X2),
                              fib1(X1, mark(X2)) -> fib1(X1, X2),
                            fib1(X1, active(X2)) -> fib1(X1, X2),
                              fib1(mark(X1), X2) -> fib1(X1, X2),
                            fib1(active(X1), X2) -> fib1(X1, X2),
                                      s(mark(X)) -> s(X),
                                    s(active(X)) -> s(X),
                  active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
                   active(sel(0(), cons(X, XS))) -> mark(X),
                              active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                                  active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                            active(add(s(X), Y)) -> mark(s(add(X, Y))),
                             active(add(0(), X)) -> mark(X),
                                    fib(mark(X)) -> fib(X),
                                  fib(active(X)) -> fib(X),
                              cons(X1, mark(X2)) -> cons(X1, X2),
                            cons(X1, active(X2)) -> cons(X1, X2),
                              cons(mark(X1), X2) -> cons(X1, X2),
                            cons(active(X1), X2) -> cons(X1, X2),
                               add(X1, mark(X2)) -> add(X1, X2),
                             add(X1, active(X2)) -> add(X1, X2),
                               add(mark(X1), X2) -> add(X1, X2),
                             add(active(X1), X2) -> add(X1, X2)}
                 SPSC:
                  Simple Projection:
                   pi(sel#) = 1
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {             mark#(sel(X1, X2)) -> mark#(X1),
                    mark#(sel(X1, X2)) -> mark#(X2),
                    mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))),
                   mark#(fib1(X1, X2)) -> mark#(X1),
                   mark#(fib1(X1, X2)) -> mark#(X2),
                   mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))),
                           mark#(s(X)) -> mark#(X),
                           mark#(s(X)) -> active#(s(mark(X))),
                         mark#(fib(X)) -> mark#(X),
                         mark#(fib(X)) -> active#(fib(mark(X))),
                   mark#(cons(X1, X2)) -> mark#(X1),
                   mark#(cons(X1, X2)) -> active#(cons(mark(X1), X2)),
                    mark#(add(X1, X2)) -> mark#(X1),
                    mark#(add(X1, X2)) -> mark#(X2),
                    mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
       active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)),
        active#(sel(0(), cons(X, XS))) -> mark#(X),
                   active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))),
                       active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))),
                 active#(add(s(X), Y)) -> mark#(s(add(X, Y))),
                  active#(add(0(), X)) -> mark#(X)}
     Weak:
     {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                  mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                          mark(s(X)) -> active(s(mark(X))),
                           mark(0()) -> active(0()),
                        mark(fib(X)) -> active(fib(mark(X))),
                  mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                   mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                   sel(X1, mark(X2)) -> sel(X1, X2),
                 sel(X1, active(X2)) -> sel(X1, X2),
                   sel(mark(X1), X2) -> sel(X1, X2),
                 sel(active(X1), X2) -> sel(X1, X2),
                  fib1(X1, mark(X2)) -> fib1(X1, X2),
                fib1(X1, active(X2)) -> fib1(X1, X2),
                  fib1(mark(X1), X2) -> fib1(X1, X2),
                fib1(active(X1), X2) -> fib1(X1, X2),
                          s(mark(X)) -> s(X),
                        s(active(X)) -> s(X),
      active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
       active(sel(0(), cons(X, XS))) -> mark(X),
                  active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                      active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                active(add(s(X), Y)) -> mark(s(add(X, Y))),
                 active(add(0(), X)) -> mark(X),
                        fib(mark(X)) -> fib(X),
                      fib(active(X)) -> fib(X),
                  cons(X1, mark(X2)) -> cons(X1, X2),
                cons(X1, active(X2)) -> cons(X1, X2),
                  cons(mark(X1), X2) -> cons(X1, X2),
                cons(active(X1), X2) -> cons(X1, X2),
                   add(X1, mark(X2)) -> add(X1, X2),
                 add(X1, active(X2)) -> add(X1, X2),
                   add(mark(X1), X2) -> add(X1, X2),
                 add(active(X1), X2) -> add(X1, X2)}
     POLY:
      Argument Filtering:
       pi(add) = [], pi(cons) = [], pi(fib) = [], pi(active#) = 0, pi(active) = [], pi(0) = [], pi(s) = [], pi(fib1) = [], pi(sel) = [], pi(mark#) = [], pi(mark) = []
      Usable Rules:
       {}
      Interpretation:
       [mark#] = 1,
       [add] = 1,
       [cons] = 0,
       [fib1] = 1,
       [sel] = 1,
       [fib] = 1,
       [s] = 0
      Strict:
       {             mark#(sel(X1, X2)) -> mark#(X1),
                     mark#(sel(X1, X2)) -> mark#(X2),
                     mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))),
                    mark#(fib1(X1, X2)) -> mark#(X1),
                    mark#(fib1(X1, X2)) -> mark#(X2),
                    mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))),
                            mark#(s(X)) -> mark#(X),
                          mark#(fib(X)) -> mark#(X),
                          mark#(fib(X)) -> active#(fib(mark(X))),
                    mark#(cons(X1, X2)) -> mark#(X1),
                     mark#(add(X1, X2)) -> mark#(X1),
                     mark#(add(X1, X2)) -> mark#(X2),
                     mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
        active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)),
         active#(sel(0(), cons(X, XS))) -> mark#(X),
                    active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))),
                        active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))),
                  active#(add(s(X), Y)) -> mark#(s(add(X, Y))),
                   active#(add(0(), X)) -> mark#(X)}
      Weak:
       {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                    mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                            mark(s(X)) -> active(s(mark(X))),
                             mark(0()) -> active(0()),
                          mark(fib(X)) -> active(fib(mark(X))),
                    mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                     mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                     sel(X1, mark(X2)) -> sel(X1, X2),
                   sel(X1, active(X2)) -> sel(X1, X2),
                     sel(mark(X1), X2) -> sel(X1, X2),
                   sel(active(X1), X2) -> sel(X1, X2),
                    fib1(X1, mark(X2)) -> fib1(X1, X2),
                  fib1(X1, active(X2)) -> fib1(X1, X2),
                    fib1(mark(X1), X2) -> fib1(X1, X2),
                  fib1(active(X1), X2) -> fib1(X1, X2),
                            s(mark(X)) -> s(X),
                          s(active(X)) -> s(X),
        active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
         active(sel(0(), cons(X, XS))) -> mark(X),
                    active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                        active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                  active(add(s(X), Y)) -> mark(s(add(X, Y))),
                   active(add(0(), X)) -> mark(X),
                          fib(mark(X)) -> fib(X),
                        fib(active(X)) -> fib(X),
                    cons(X1, mark(X2)) -> cons(X1, X2),
                  cons(X1, active(X2)) -> cons(X1, X2),
                    cons(mark(X1), X2) -> cons(X1, X2),
                  cons(active(X1), X2) -> cons(X1, X2),
                     add(X1, mark(X2)) -> add(X1, X2),
                   add(X1, active(X2)) -> add(X1, X2),
                     add(mark(X1), X2) -> add(X1, X2),
                   add(active(X1), X2) -> add(X1, X2)}
      EDG:
       {
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib(X)) -> active#(fib(mark(X))))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib(X)) -> mark#(X))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X2))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X1))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(sel(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(s(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))))
        (mark#(s(X)) -> mark#(X), mark#(fib(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2))
        (mark#(s(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(s(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(fib(X)) -> active#(fib(mark(X))))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(fib(X)) -> mark#(X))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X2))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(add(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1))
        (active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
        (active#(add(0(), X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
        (active#(add(0(), X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (active#(add(0(), X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))))
        (active#(add(0(), X)) -> mark#(X), mark#(fib(X)) -> mark#(X))
        (active#(add(0(), X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2))
        (active#(add(0(), X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1))
        (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
        (active#(add(0(), X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X))
        (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
        (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))))
        (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))))
        (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X))
        (mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)))
        (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X))
        (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
        (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))))
        (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))))
        (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X))
        (mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X))))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(sel(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X))))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1))
        (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> mark#(X2))
        (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(add(X1, X2)) -> mark#(X1))
        (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(cons(X1, X2)) -> mark#(X1))
        (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib(X)) -> active#(fib(mark(X))))
        (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib(X)) -> mark#(X))
        (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(s(X)) -> mark#(X))
        (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> mark#(X2))
        (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(fib1(X1, X2)) -> mark#(X1))
        (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> mark#(X2))
        (active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))), mark#(sel(X1, X2)) -> mark#(X1))
        (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> mark#(X1))
        (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> mark#(X2))
        (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> mark#(X1))
        (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> mark#(X2))
        (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(s(X)) -> mark#(X))
        (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib(X)) -> mark#(X))
        (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(fib(X)) -> active#(fib(mark(X))))
        (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(cons(X1, X2)) -> mark#(X1))
        (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> mark#(X1))
        (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> mark#(X2))
        (active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X))))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(add(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (mark#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(fib1(X1, X2)) -> mark#(X1), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X1))
        (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> mark#(X2))
        (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (mark#(fib1(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib(X)) -> mark#(X))
        (mark#(fib1(X1, X2)) -> mark#(X1), mark#(fib(X)) -> active#(fib(mark(X))))
        (mark#(fib1(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(fib1(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(fib1(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(fib1(X1, X2)) -> mark#(X1), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(sel(X1, X2)) -> mark#(X1))
        (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(sel(X1, X2)) -> mark#(X2))
        (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> mark#(X1))
        (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> mark#(X2))
        (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(s(X)) -> mark#(X))
        (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib(X)) -> mark#(X))
        (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(fib(X)) -> active#(fib(mark(X))))
        (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(cons(X1, X2)) -> mark#(X1))
        (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> mark#(X1))
        (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> mark#(X2))
        (active#(add(s(X), Y)) -> mark#(s(add(X, Y))), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (mark#(fib(X)) -> active#(fib(mark(X))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)))
        (mark#(fib(X)) -> active#(fib(mark(X))), active#(sel(0(), cons(X, XS))) -> mark#(X))
        (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))))
        (mark#(fib(X)) -> active#(fib(mark(X))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))))
        (mark#(fib(X)) -> active#(fib(mark(X))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
        (mark#(fib(X)) -> active#(fib(mark(X))), active#(add(0(), X)) -> mark#(X))
        (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)))
        (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(sel(0(), cons(X, XS))) -> mark#(X))
        (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))))
        (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))))
        (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(add(s(X), Y)) -> mark#(s(add(X, Y))))
        (mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))), active#(add(0(), X)) -> mark#(X))
        (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
        (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
        (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1))
        (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2))
        (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(s(X)) -> mark#(X))
        (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib(X)) -> mark#(X))
        (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))))
        (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
        (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
        (active#(sel(0(), cons(X, XS))) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(fib(X)) -> mark#(X), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X1))
        (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> mark#(X2))
        (mark#(fib(X)) -> mark#(X), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (mark#(fib(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> mark#(X))
        (mark#(fib(X)) -> mark#(X), mark#(fib(X)) -> active#(fib(mark(X))))
        (mark#(fib(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(fib(X)) -> mark#(X), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X1))
        (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> mark#(X2))
        (mark#(fib1(X1, X2)) -> mark#(X2), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X1))
        (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> mark#(X2))
        (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (mark#(fib1(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
        (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib(X)) -> mark#(X))
        (mark#(fib1(X1, X2)) -> mark#(X2), mark#(fib(X)) -> active#(fib(mark(X))))
        (mark#(fib1(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X1))
        (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> mark#(X2))
        (mark#(fib1(X1, X2)) -> mark#(X2), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
        (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> mark#(X1))
        (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> mark#(X2))
        (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))))
        (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> mark#(X1))
        (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> mark#(X2))
        (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))))
        (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(s(X)) -> mark#(X))
        (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib(X)) -> mark#(X))
        (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(fib(X)) -> active#(fib(mark(X))))
        (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(cons(X1, X2)) -> mark#(X1))
        (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> mark#(X1))
        (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> mark#(X2))
        (active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)), mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))))
       }
       SCCS:
        Scc:
         {             mark#(sel(X1, X2)) -> mark#(X1),
                       mark#(sel(X1, X2)) -> mark#(X2),
                       mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))),
                      mark#(fib1(X1, X2)) -> mark#(X1),
                      mark#(fib1(X1, X2)) -> mark#(X2),
                      mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))),
                              mark#(s(X)) -> mark#(X),
                            mark#(fib(X)) -> mark#(X),
                            mark#(fib(X)) -> active#(fib(mark(X))),
                      mark#(cons(X1, X2)) -> mark#(X1),
                       mark#(add(X1, X2)) -> mark#(X1),
                       mark#(add(X1, X2)) -> mark#(X2),
                       mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
          active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)),
           active#(sel(0(), cons(X, XS))) -> mark#(X),
                      active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))),
                          active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))),
                    active#(add(s(X), Y)) -> mark#(s(add(X, Y))),
                     active#(add(0(), X)) -> mark#(X)}
        SCC:
         Strict:
          {             mark#(sel(X1, X2)) -> mark#(X1),
                        mark#(sel(X1, X2)) -> mark#(X2),
                        mark#(sel(X1, X2)) -> active#(sel(mark(X1), mark(X2))),
                       mark#(fib1(X1, X2)) -> mark#(X1),
                       mark#(fib1(X1, X2)) -> mark#(X2),
                       mark#(fib1(X1, X2)) -> active#(fib1(mark(X1), mark(X2))),
                               mark#(s(X)) -> mark#(X),
                             mark#(fib(X)) -> mark#(X),
                             mark#(fib(X)) -> active#(fib(mark(X))),
                       mark#(cons(X1, X2)) -> mark#(X1),
                        mark#(add(X1, X2)) -> mark#(X1),
                        mark#(add(X1, X2)) -> mark#(X2),
                        mark#(add(X1, X2)) -> active#(add(mark(X1), mark(X2))),
           active#(sel(s(N), cons(X, XS))) -> mark#(sel(N, XS)),
            active#(sel(0(), cons(X, XS))) -> mark#(X),
                       active#(fib1(X, Y)) -> mark#(cons(X, fib1(Y, add(X, Y)))),
                           active#(fib(N)) -> mark#(sel(N, fib1(s(0()), s(0())))),
                     active#(add(s(X), Y)) -> mark#(s(add(X, Y))),
                      active#(add(0(), X)) -> mark#(X)}
         Weak:
         {             mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                      mark(fib1(X1, X2)) -> active(fib1(mark(X1), mark(X2))),
                              mark(s(X)) -> active(s(mark(X))),
                               mark(0()) -> active(0()),
                            mark(fib(X)) -> active(fib(mark(X))),
                      mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                       mark(add(X1, X2)) -> active(add(mark(X1), mark(X2))),
                       sel(X1, mark(X2)) -> sel(X1, X2),
                     sel(X1, active(X2)) -> sel(X1, X2),
                       sel(mark(X1), X2) -> sel(X1, X2),
                     sel(active(X1), X2) -> sel(X1, X2),
                      fib1(X1, mark(X2)) -> fib1(X1, X2),
                    fib1(X1, active(X2)) -> fib1(X1, X2),
                      fib1(mark(X1), X2) -> fib1(X1, X2),
                    fib1(active(X1), X2) -> fib1(X1, X2),
                              s(mark(X)) -> s(X),
                            s(active(X)) -> s(X),
          active(sel(s(N), cons(X, XS))) -> mark(sel(N, XS)),
           active(sel(0(), cons(X, XS))) -> mark(X),
                      active(fib1(X, Y)) -> mark(cons(X, fib1(Y, add(X, Y)))),
                          active(fib(N)) -> mark(sel(N, fib1(s(0()), s(0())))),
                    active(add(s(X), Y)) -> mark(s(add(X, Y))),
                     active(add(0(), X)) -> mark(X),
                            fib(mark(X)) -> fib(X),
                          fib(active(X)) -> fib(X),
                      cons(X1, mark(X2)) -> cons(X1, X2),
                    cons(X1, active(X2)) -> cons(X1, X2),
                      cons(mark(X1), X2) -> cons(X1, X2),
                    cons(active(X1), X2) -> cons(X1, X2),
                       add(X1, mark(X2)) -> add(X1, X2),
                     add(X1, active(X2)) -> add(X1, X2),
                       add(mark(X1), X2) -> add(X1, X2),
                     add(active(X1), X2) -> add(X1, X2)}
         Fail