MAYBE
Time: 45.514047
TRS:
 {            sel(X1, mark X2) -> mark sel(X1, X2),
              sel(mark X1, X2) -> mark sel(X1, X2),
             sel(ok X1, ok X2) -> ok sel(X1, X2),
             fib1(X1, mark X2) -> mark fib1(X1, X2),
             fib1(mark X1, X2) -> mark fib1(X1, X2),
            fib1(ok X1, ok X2) -> ok fib1(X1, X2),
                      s mark X -> mark s X,
                        s ok X -> ok s X,
            active sel(X1, X2) -> sel(X1, active X2),
            active sel(X1, X2) -> sel(active X1, 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 fib1(X1, X2) -> fib1(X1, active X2),
           active fib1(X1, X2) -> fib1(active X1, X2),
                    active s X -> s active X,
                  active fib N -> mark sel(N, fib1(s 0(), s 0())),
                  active fib X -> fib active X,
           active cons(X1, X2) -> cons(active X1, X2),
            active add(X1, X2) -> add(X1, active X2),
            active add(X1, X2) -> add(active X1, X2),
            active add(s X, Y) -> mark s add(X, Y),
            active add(0(), X) -> mark X,
                    fib mark X -> mark fib X,
                      fib ok X -> ok fib X,
             cons(mark X1, X2) -> mark cons(X1, X2),
            cons(ok X1, ok X2) -> ok cons(X1, X2),
              add(X1, mark X2) -> mark add(X1, X2),
              add(mark X1, X2) -> mark add(X1, X2),
             add(ok X1, ok X2) -> ok add(X1, X2),
            proper sel(X1, X2) -> sel(proper X1, proper X2),
           proper fib1(X1, X2) -> fib1(proper X1, proper X2),
                    proper s X -> s proper X,
                    proper 0() -> ok 0(),
                  proper fib X -> fib proper X,
           proper cons(X1, X2) -> cons(proper X1, proper X2),
            proper add(X1, X2) -> add(proper X1, proper X2),
                    top mark X -> top proper X,
                      top ok X -> top active X}
 DP:
  DP:
   {            sel#(X1, mark X2) -> sel#(X1, X2),
                sel#(mark X1, X2) -> sel#(X1, X2),
               sel#(ok X1, ok X2) -> sel#(X1, X2),
               fib1#(X1, mark X2) -> fib1#(X1, X2),
               fib1#(mark X1, X2) -> fib1#(X1, X2),
              fib1#(ok X1, ok X2) -> fib1#(X1, X2),
                        s# mark X -> s# X,
                          s# ok X -> s# X,
              active# sel(X1, X2) -> sel#(X1, active X2),
              active# sel(X1, X2) -> sel#(active X1, X2),
              active# sel(X1, X2) -> active# X1,
              active# sel(X1, X2) -> active# X2,
    active# sel(s N, cons(X, XS)) -> sel#(N, XS),
               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# fib1(X1, X2) -> fib1#(X1, active X2),
             active# fib1(X1, X2) -> fib1#(active X1, X2),
             active# fib1(X1, X2) -> active# X1,
             active# fib1(X1, X2) -> active# X2,
                      active# s X -> s# active X,
                      active# s X -> active# X,
                    active# fib N -> sel#(N, fib1(s 0(), s 0())),
                    active# fib N -> fib1#(s 0(), s 0()),
                    active# fib N -> s# 0(),
                    active# fib X -> active# X,
                    active# fib X -> fib# active X,
             active# cons(X1, X2) -> active# X1,
             active# cons(X1, X2) -> cons#(active X1, X2),
              active# add(X1, X2) -> active# X1,
              active# add(X1, X2) -> active# X2,
              active# add(X1, X2) -> add#(X1, active X2),
              active# add(X1, X2) -> add#(active X1, X2),
              active# add(s X, Y) -> s# add(X, Y),
              active# add(s X, Y) -> add#(X, Y),
                      fib# mark X -> fib# X,
                        fib# ok X -> fib# X,
               cons#(mark X1, X2) -> cons#(X1, X2),
              cons#(ok X1, ok X2) -> cons#(X1, X2),
                add#(X1, mark X2) -> add#(X1, X2),
                add#(mark X1, X2) -> add#(X1, X2),
               add#(ok X1, ok X2) -> add#(X1, X2),
              proper# sel(X1, X2) -> sel#(proper X1, proper X2),
              proper# sel(X1, X2) -> proper# X1,
              proper# sel(X1, X2) -> proper# X2,
             proper# fib1(X1, X2) -> fib1#(proper X1, proper X2),
             proper# fib1(X1, X2) -> proper# X1,
             proper# fib1(X1, X2) -> proper# X2,
                      proper# s X -> s# proper X,
                      proper# s X -> proper# X,
                    proper# fib X -> fib# proper X,
                    proper# fib X -> proper# X,
             proper# cons(X1, X2) -> cons#(proper X1, proper X2),
             proper# cons(X1, X2) -> proper# X1,
             proper# cons(X1, X2) -> proper# X2,
              proper# add(X1, X2) -> add#(proper X1, proper X2),
              proper# add(X1, X2) -> proper# X1,
              proper# add(X1, X2) -> proper# X2,
                      top# mark X -> proper# X,
                      top# mark X -> top# proper X,
                        top# ok X -> active# X,
                        top# ok X -> top# active X}
  TRS:
  {            sel(X1, mark X2) -> mark sel(X1, X2),
               sel(mark X1, X2) -> mark sel(X1, X2),
              sel(ok X1, ok X2) -> ok sel(X1, X2),
              fib1(X1, mark X2) -> mark fib1(X1, X2),
              fib1(mark X1, X2) -> mark fib1(X1, X2),
             fib1(ok X1, ok X2) -> ok fib1(X1, X2),
                       s mark X -> mark s X,
                         s ok X -> ok s X,
             active sel(X1, X2) -> sel(X1, active X2),
             active sel(X1, X2) -> sel(active X1, 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 fib1(X1, X2) -> fib1(X1, active X2),
            active fib1(X1, X2) -> fib1(active X1, X2),
                     active s X -> s active X,
                   active fib N -> mark sel(N, fib1(s 0(), s 0())),
                   active fib X -> fib active X,
            active cons(X1, X2) -> cons(active X1, X2),
             active add(X1, X2) -> add(X1, active X2),
             active add(X1, X2) -> add(active X1, X2),
             active add(s X, Y) -> mark s add(X, Y),
             active add(0(), X) -> mark X,
                     fib mark X -> mark fib X,
                       fib ok X -> ok fib X,
              cons(mark X1, X2) -> mark cons(X1, X2),
             cons(ok X1, ok X2) -> ok cons(X1, X2),
               add(X1, mark X2) -> mark add(X1, X2),
               add(mark X1, X2) -> mark add(X1, X2),
              add(ok X1, ok X2) -> ok add(X1, X2),
             proper sel(X1, X2) -> sel(proper X1, proper X2),
            proper fib1(X1, X2) -> fib1(proper X1, proper X2),
                     proper s X -> s proper X,
                     proper 0() -> ok 0(),
                   proper fib X -> fib proper X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
             proper add(X1, X2) -> add(proper X1, proper X2),
                     top mark X -> top proper X,
                       top ok X -> top active X}
  EDG:
   {
    (active# fib1(X1, X2) -> fib1#(X1, active X2), fib1#(ok X1, ok X2) -> fib1#(X1, X2))
    (active# fib1(X1, X2) -> fib1#(X1, active X2), fib1#(mark X1, X2) -> fib1#(X1, X2))
    (active# fib1(X1, X2) -> fib1#(X1, active X2), fib1#(X1, mark X2) -> fib1#(X1, X2))
    (proper# sel(X1, X2) -> sel#(proper X1, proper X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
    (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))), cons#(ok X1, ok 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) -> fib1#(Y, add(X, Y)), fib1#(ok X1, ok 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, mark X2) -> fib1#(X1, X2))
    (active# add(s X, Y) -> add#(X, Y), add#(ok X1, ok 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, mark X2) -> add#(X1, X2))
    (active# fib1(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
    (active# fib1(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
    (active# fib1(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
    (active# fib1(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
    (active# fib1(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
    (active# fib1(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
    (active# fib1(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# fib1(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
    (active# fib1(X1, X2) -> active# X1, active# fib X -> fib# active X)
    (active# fib1(X1, X2) -> active# X1, active# fib X -> active# X)
    (active# fib1(X1, X2) -> active# X1, active# fib N -> s# 0())
    (active# fib1(X1, X2) -> active# X1, active# fib N -> fib1#(s 0(), s 0()))
    (active# fib1(X1, X2) -> active# X1, active# fib N -> sel#(N, fib1(s 0(), s 0())))
    (active# fib1(X1, X2) -> active# X1, active# s X -> active# X)
    (active# fib1(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# fib1(X1, X2) -> active# X1, active# fib1(X1, X2) -> active# X2)
    (active# fib1(X1, X2) -> active# X1, active# fib1(X1, X2) -> active# X1)
    (active# fib1(X1, X2) -> active# X1, active# fib1(X1, X2) -> fib1#(active X1, X2))
    (active# fib1(X1, X2) -> active# X1, active# fib1(X1, X2) -> fib1#(X1, active X2))
    (active# fib1(X1, X2) -> active# X1, active# fib1(X, Y) -> add#(X, Y))
    (active# fib1(X1, X2) -> active# X1, active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
    (active# fib1(X1, X2) -> active# X1, active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
    (active# fib1(X1, X2) -> active# X1, active# sel(s N, cons(X, XS)) -> sel#(N, XS))
    (active# fib1(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X2)
    (active# fib1(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X1)
    (active# fib1(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# fib1(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
    (active# add(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
    (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
    (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
    (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
    (active# add(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
    (active# add(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# add(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
    (active# add(X1, X2) -> active# X1, active# fib X -> fib# active X)
    (active# add(X1, X2) -> active# X1, active# fib X -> active# X)
    (active# add(X1, X2) -> active# X1, active# fib N -> s# 0())
    (active# add(X1, X2) -> active# X1, active# fib N -> fib1#(s 0(), s 0()))
    (active# add(X1, X2) -> active# X1, active# fib N -> sel#(N, fib1(s 0(), s 0())))
    (active# add(X1, X2) -> active# X1, active# s X -> active# X)
    (active# add(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# add(X1, X2) -> active# X1, active# fib1(X1, X2) -> active# X2)
    (active# add(X1, X2) -> active# X1, active# fib1(X1, X2) -> active# X1)
    (active# add(X1, X2) -> active# X1, active# fib1(X1, X2) -> fib1#(active X1, X2))
    (active# add(X1, X2) -> active# X1, active# fib1(X1, X2) -> fib1#(X1, active X2))
    (active# add(X1, X2) -> active# X1, active# fib1(X, Y) -> add#(X, Y))
    (active# add(X1, X2) -> active# X1, active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
    (active# add(X1, X2) -> active# X1, active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
    (active# add(X1, X2) -> active# X1, active# sel(s N, cons(X, XS)) -> sel#(N, XS))
    (active# add(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X2)
    (active# add(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X1)
    (active# add(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# add(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(X1, active X2))
    (proper# fib1(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
    (proper# fib1(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
    (proper# fib1(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
    (proper# fib1(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
    (proper# fib1(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
    (proper# fib1(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# fib1(X1, X2) -> proper# X1, proper# fib X -> proper# X)
    (proper# fib1(X1, X2) -> proper# X1, proper# fib X -> fib# proper X)
    (proper# fib1(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# fib1(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# fib1(X1, X2) -> proper# X1, proper# fib1(X1, X2) -> proper# X2)
    (proper# fib1(X1, X2) -> proper# X1, proper# fib1(X1, X2) -> proper# X1)
    (proper# fib1(X1, X2) -> proper# X1, proper# fib1(X1, X2) -> fib1#(proper X1, proper X2))
    (proper# fib1(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X2)
    (proper# fib1(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X1)
    (proper# fib1(X1, X2) -> proper# X1, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# add(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
    (proper# add(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
    (proper# add(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
    (proper# add(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
    (proper# add(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
    (proper# add(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# add(X1, X2) -> proper# X1, proper# fib X -> proper# X)
    (proper# add(X1, X2) -> proper# X1, proper# fib X -> fib# proper X)
    (proper# add(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# add(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# add(X1, X2) -> proper# X1, proper# fib1(X1, X2) -> proper# X2)
    (proper# add(X1, X2) -> proper# X1, proper# fib1(X1, X2) -> proper# X1)
    (proper# add(X1, X2) -> proper# X1, proper# fib1(X1, X2) -> fib1#(proper X1, proper X2))
    (proper# add(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X2)
    (proper# add(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X1)
    (proper# add(X1, X2) -> proper# X1, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (active# sel(X1, X2) -> sel#(active X1, X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
    (active# sel(X1, X2) -> sel#(active X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
    (active# sel(X1, X2) -> sel#(active X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
    (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (sel#(mark X1, X2) -> sel#(X1, X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
    (sel#(mark X1, X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
    (sel#(mark X1, X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
    (fib1#(X1, mark X2) -> fib1#(X1, X2), fib1#(ok X1, ok X2) -> fib1#(X1, X2))
    (fib1#(X1, mark X2) -> fib1#(X1, X2), fib1#(mark X1, X2) -> fib1#(X1, X2))
    (fib1#(X1, mark X2) -> fib1#(X1, X2), fib1#(X1, mark X2) -> fib1#(X1, X2))
    (fib1#(ok X1, ok X2) -> fib1#(X1, X2), fib1#(ok X1, ok X2) -> fib1#(X1, X2))
    (fib1#(ok X1, ok X2) -> fib1#(X1, X2), fib1#(mark X1, X2) -> fib1#(X1, X2))
    (fib1#(ok X1, ok X2) -> fib1#(X1, X2), fib1#(X1, mark X2) -> fib1#(X1, X2))
    (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (add#(mark X1, X2) -> add#(X1, X2), add#(ok X1, ok X2) -> add#(X1, X2))
    (add#(mark X1, X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
    (add#(mark X1, X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
    (s# mark X -> s# X, s# ok X -> s# X)
    (s# mark X -> s# X, s# mark X -> s# X)
    (active# s X -> active# X, active# add(s X, Y) -> add#(X, Y))
    (active# s X -> active# X, active# add(s X, Y) -> s# add(X, Y))
    (active# s X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
    (active# s X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
    (active# s X -> active# X, active# add(X1, X2) -> active# X2)
    (active# s X -> active# X, active# add(X1, X2) -> active# X1)
    (active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# s X -> active# X, active# cons(X1, X2) -> active# X1)
    (active# s X -> active# X, active# fib X -> fib# active X)
    (active# s X -> active# X, active# fib X -> active# X)
    (active# s X -> active# X, active# fib N -> s# 0())
    (active# s X -> active# X, active# fib N -> fib1#(s 0(), s 0()))
    (active# s X -> active# X, active# fib N -> sel#(N, fib1(s 0(), s 0())))
    (active# s X -> active# X, active# s X -> active# X)
    (active# s X -> active# X, active# s X -> s# active X)
    (active# s X -> active# X, active# fib1(X1, X2) -> active# X2)
    (active# s X -> active# X, active# fib1(X1, X2) -> active# X1)
    (active# s X -> active# X, active# fib1(X1, X2) -> fib1#(active X1, X2))
    (active# s X -> active# X, active# fib1(X1, X2) -> fib1#(X1, active X2))
    (active# s X -> active# X, active# fib1(X, Y) -> add#(X, Y))
    (active# s X -> active# X, active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
    (active# s X -> active# X, active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
    (active# s X -> active# X, active# sel(s N, cons(X, XS)) -> sel#(N, XS))
    (active# s X -> active# X, active# sel(X1, X2) -> active# X2)
    (active# s X -> active# X, active# sel(X1, X2) -> active# X1)
    (active# s X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# s X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
    (fib# mark X -> fib# X, fib# ok X -> fib# X)
    (fib# mark X -> fib# X, fib# mark X -> fib# X)
    (proper# s X -> proper# X, proper# add(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# add(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# fib X -> proper# X)
    (proper# s X -> proper# X, proper# fib X -> fib# proper X)
    (proper# s X -> proper# X, proper# s X -> proper# X)
    (proper# s X -> proper# X, proper# s X -> s# proper X)
    (proper# s X -> proper# X, proper# fib1(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# fib1(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# fib1(X1, X2) -> fib1#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X2)
    (top# mark X -> proper# X, proper# add(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# fib X -> proper# X)
    (top# mark X -> proper# X, proper# fib X -> fib# proper X)
    (top# mark X -> proper# X, proper# s X -> proper# X)
    (top# mark X -> proper# X, proper# s X -> s# proper X)
    (top# mark X -> proper# X, proper# fib1(X1, X2) -> proper# X2)
    (top# mark X -> proper# X, proper# fib1(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# fib1(X1, X2) -> fib1#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (top# mark X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (active# sel(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
    (active# sel(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
    (active# sel(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
    (active# sel(X1, X2) -> active# X2, active# add(X1, X2) -> add#(X1, active X2))
    (active# sel(X1, X2) -> active# X2, active# add(X1, X2) -> active# X2)
    (active# sel(X1, X2) -> active# X2, active# add(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# sel(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X2, active# fib X -> fib# active X)
    (active# sel(X1, X2) -> active# X2, active# fib X -> active# X)
    (active# sel(X1, X2) -> active# X2, active# fib N -> s# 0())
    (active# sel(X1, X2) -> active# X2, active# fib N -> fib1#(s 0(), s 0()))
    (active# sel(X1, X2) -> active# X2, active# fib N -> sel#(N, fib1(s 0(), s 0())))
    (active# sel(X1, X2) -> active# X2, active# s X -> active# X)
    (active# sel(X1, X2) -> active# X2, active# s X -> s# active X)
    (active# sel(X1, X2) -> active# X2, active# fib1(X1, X2) -> active# X2)
    (active# sel(X1, X2) -> active# X2, active# fib1(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X2, active# fib1(X1, X2) -> fib1#(active X1, X2))
    (active# sel(X1, X2) -> active# X2, active# fib1(X1, X2) -> fib1#(X1, active X2))
    (active# sel(X1, X2) -> active# X2, active# fib1(X, Y) -> add#(X, Y))
    (active# sel(X1, X2) -> active# X2, active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
    (active# sel(X1, X2) -> active# X2, active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
    (active# sel(X1, X2) -> active# X2, active# sel(s N, cons(X, XS)) -> sel#(N, XS))
    (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X2)
    (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
    (active# add(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
    (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
    (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> add#(X1, active X2))
    (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> active# X2)
    (active# add(X1, X2) -> active# X2, active# add(X1, X2) -> active# X1)
    (active# add(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# add(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
    (active# add(X1, X2) -> active# X2, active# fib X -> fib# active X)
    (active# add(X1, X2) -> active# X2, active# fib X -> active# X)
    (active# add(X1, X2) -> active# X2, active# fib N -> s# 0())
    (active# add(X1, X2) -> active# X2, active# fib N -> fib1#(s 0(), s 0()))
    (active# add(X1, X2) -> active# X2, active# fib N -> sel#(N, fib1(s 0(), s 0())))
    (active# add(X1, X2) -> active# X2, active# s X -> active# X)
    (active# add(X1, X2) -> active# X2, active# s X -> s# active X)
    (active# add(X1, X2) -> active# X2, active# fib1(X1, X2) -> active# X2)
    (active# add(X1, X2) -> active# X2, active# fib1(X1, X2) -> active# X1)
    (active# add(X1, X2) -> active# X2, active# fib1(X1, X2) -> fib1#(active X1, X2))
    (active# add(X1, X2) -> active# X2, active# fib1(X1, X2) -> fib1#(X1, active X2))
    (active# add(X1, X2) -> active# X2, active# fib1(X, Y) -> add#(X, Y))
    (active# add(X1, X2) -> active# X2, active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
    (active# add(X1, X2) -> active# X2, active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
    (active# add(X1, X2) -> active# X2, active# sel(s N, cons(X, XS)) -> sel#(N, XS))
    (active# add(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X2)
    (active# add(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X1)
    (active# add(X1, X2) -> active# X2, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# add(X1, X2) -> active# X2, active# sel(X1, X2) -> sel#(X1, active X2))
    (proper# fib1(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
    (proper# fib1(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
    (proper# fib1(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
    (proper# fib1(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
    (proper# fib1(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
    (proper# fib1(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# fib1(X1, X2) -> proper# X2, proper# fib X -> proper# X)
    (proper# fib1(X1, X2) -> proper# X2, proper# fib X -> fib# proper X)
    (proper# fib1(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# fib1(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# fib1(X1, X2) -> proper# X2, proper# fib1(X1, X2) -> proper# X2)
    (proper# fib1(X1, X2) -> proper# X2, proper# fib1(X1, X2) -> proper# X1)
    (proper# fib1(X1, X2) -> proper# X2, proper# fib1(X1, X2) -> fib1#(proper X1, proper X2))
    (proper# fib1(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X2)
    (proper# fib1(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X1)
    (proper# fib1(X1, X2) -> proper# X2, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# add(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
    (proper# add(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
    (proper# add(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
    (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
    (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
    (proper# add(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# add(X1, X2) -> proper# X2, proper# fib X -> proper# X)
    (proper# add(X1, X2) -> proper# X2, proper# fib X -> fib# proper X)
    (proper# add(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# add(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# add(X1, X2) -> proper# X2, proper# fib1(X1, X2) -> proper# X2)
    (proper# add(X1, X2) -> proper# X2, proper# fib1(X1, X2) -> proper# X1)
    (proper# add(X1, X2) -> proper# X2, proper# fib1(X1, X2) -> fib1#(proper X1, proper X2))
    (proper# add(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X2)
    (proper# add(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X1)
    (proper# add(X1, X2) -> proper# X2, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (active# add(s X, Y) -> s# add(X, Y), s# ok X -> s# X)
    (active# add(s X, Y) -> s# add(X, Y), s# mark X -> s# X)
    (active# fib X -> fib# active X, fib# ok X -> fib# X)
    (active# fib X -> fib# active X, fib# mark X -> fib# X)
    (proper# fib X -> fib# proper X, fib# ok X -> fib# X)
    (top# ok X -> top# active X, top# ok X -> top# active X)
    (top# ok X -> top# active X, top# ok X -> active# X)
    (top# ok X -> top# active X, top# mark X -> top# proper X)
    (top# ok X -> top# active X, top# mark X -> proper# X)
    (top# mark X -> top# proper X, top# ok X -> active# X)
    (top# mark X -> top# proper X, top# ok X -> top# active X)
    (proper# s X -> s# proper X, s# ok X -> s# X)
    (active# s X -> s# active X, s# mark X -> s# X)
    (active# s X -> s# active X, s# ok X -> s# X)
    (proper# cons(X1, X2) -> proper# X2, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X2, proper# fib1(X1, X2) -> fib1#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X2, proper# fib1(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X2, proper# fib1(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# cons(X1, X2) -> proper# X2, proper# fib X -> fib# proper X)
    (proper# cons(X1, X2) -> proper# X2, proper# fib X -> proper# X)
    (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
    (proper# sel(X1, X2) -> proper# X2, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# sel(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X2)
    (proper# sel(X1, X2) -> proper# X2, proper# fib1(X1, X2) -> fib1#(proper X1, proper X2))
    (proper# sel(X1, X2) -> proper# X2, proper# fib1(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X2, proper# fib1(X1, X2) -> proper# X2)
    (proper# sel(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# sel(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# sel(X1, X2) -> proper# X2, proper# fib X -> fib# proper X)
    (proper# sel(X1, X2) -> proper# X2, proper# fib X -> proper# X)
    (proper# sel(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# sel(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
    (proper# sel(X1, X2) -> proper# X2, proper# add(X1, X2) -> add#(proper X1, proper X2))
    (proper# sel(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X2, proper# add(X1, X2) -> proper# X2)
    (active# fib1(X1, X2) -> active# X2, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# fib1(X1, X2) -> active# X2, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# fib1(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X1)
    (active# fib1(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X2)
    (active# fib1(X1, X2) -> active# X2, active# sel(s N, cons(X, XS)) -> sel#(N, XS))
    (active# fib1(X1, X2) -> active# X2, active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
    (active# fib1(X1, X2) -> active# X2, active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
    (active# fib1(X1, X2) -> active# X2, active# fib1(X, Y) -> add#(X, Y))
    (active# fib1(X1, X2) -> active# X2, active# fib1(X1, X2) -> fib1#(X1, active X2))
    (active# fib1(X1, X2) -> active# X2, active# fib1(X1, X2) -> fib1#(active X1, X2))
    (active# fib1(X1, X2) -> active# X2, active# fib1(X1, X2) -> active# X1)
    (active# fib1(X1, X2) -> active# X2, active# fib1(X1, X2) -> active# X2)
    (active# fib1(X1, X2) -> active# X2, active# s X -> s# active X)
    (active# fib1(X1, X2) -> active# X2, active# s X -> active# X)
    (active# fib1(X1, X2) -> active# X2, active# fib N -> sel#(N, fib1(s 0(), s 0())))
    (active# fib1(X1, X2) -> active# X2, active# fib N -> fib1#(s 0(), s 0()))
    (active# fib1(X1, X2) -> active# X2, active# fib N -> s# 0())
    (active# fib1(X1, X2) -> active# X2, active# fib X -> active# X)
    (active# fib1(X1, X2) -> active# X2, active# fib X -> fib# active X)
    (active# fib1(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
    (active# fib1(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# fib1(X1, X2) -> active# X2, active# add(X1, X2) -> active# X1)
    (active# fib1(X1, X2) -> active# X2, active# add(X1, X2) -> active# X2)
    (active# fib1(X1, X2) -> active# X2, active# add(X1, X2) -> add#(X1, active X2))
    (active# fib1(X1, X2) -> active# X2, active# add(X1, X2) -> add#(active X1, X2))
    (active# fib1(X1, X2) -> active# X2, active# add(s X, Y) -> s# add(X, Y))
    (active# fib1(X1, X2) -> active# X2, active# add(s X, Y) -> add#(X, Y))
    (top# ok X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
    (top# ok X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
    (top# ok X -> active# X, active# sel(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# sel(X1, X2) -> active# X2)
    (top# ok X -> active# X, active# sel(s N, cons(X, XS)) -> sel#(N, XS))
    (top# ok X -> active# X, active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
    (top# ok X -> active# X, active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
    (top# ok X -> active# X, active# fib1(X, Y) -> add#(X, Y))
    (top# ok X -> active# X, active# fib1(X1, X2) -> fib1#(X1, active X2))
    (top# ok X -> active# X, active# fib1(X1, X2) -> fib1#(active X1, X2))
    (top# ok X -> active# X, active# fib1(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# fib1(X1, X2) -> active# X2)
    (top# ok X -> active# X, active# s X -> s# active X)
    (top# ok X -> active# X, active# s X -> active# X)
    (top# ok X -> active# X, active# fib N -> sel#(N, fib1(s 0(), s 0())))
    (top# ok X -> active# X, active# fib N -> fib1#(s 0(), s 0()))
    (top# ok X -> active# X, active# fib N -> s# 0())
    (top# ok X -> active# X, active# fib X -> active# X)
    (top# ok X -> active# X, active# fib X -> fib# active X)
    (top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (top# ok X -> active# X, active# add(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# add(X1, X2) -> active# X2)
    (top# ok X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
    (top# ok X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
    (top# ok X -> active# X, active# add(s X, Y) -> s# add(X, Y))
    (top# ok X -> active# X, active# add(s X, Y) -> add#(X, Y))
    (proper# fib X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# fib X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (proper# fib X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (proper# fib X -> proper# X, proper# fib1(X1, X2) -> fib1#(proper X1, proper X2))
    (proper# fib X -> proper# X, proper# fib1(X1, X2) -> proper# X1)
    (proper# fib X -> proper# X, proper# fib1(X1, X2) -> proper# X2)
    (proper# fib X -> proper# X, proper# s X -> s# proper X)
    (proper# fib X -> proper# X, proper# s X -> proper# X)
    (proper# fib X -> proper# X, proper# fib X -> fib# proper X)
    (proper# fib X -> proper# X, proper# fib X -> proper# X)
    (proper# fib X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# fib X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# fib X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# fib X -> proper# X, proper# add(X1, X2) -> add#(proper X1, proper X2))
    (proper# fib X -> proper# X, proper# add(X1, X2) -> proper# X1)
    (proper# fib X -> proper# X, proper# add(X1, X2) -> proper# X2)
    (fib# ok X -> fib# X, fib# mark X -> fib# X)
    (fib# ok X -> fib# X, fib# ok X -> fib# X)
    (active# fib X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# fib X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# fib X -> active# X, active# sel(X1, X2) -> active# X1)
    (active# fib X -> active# X, active# sel(X1, X2) -> active# X2)
    (active# fib X -> active# X, active# sel(s N, cons(X, XS)) -> sel#(N, XS))
    (active# fib X -> active# X, active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
    (active# fib X -> active# X, active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
    (active# fib X -> active# X, active# fib1(X, Y) -> add#(X, Y))
    (active# fib X -> active# X, active# fib1(X1, X2) -> fib1#(X1, active X2))
    (active# fib X -> active# X, active# fib1(X1, X2) -> fib1#(active X1, X2))
    (active# fib X -> active# X, active# fib1(X1, X2) -> active# X1)
    (active# fib X -> active# X, active# fib1(X1, X2) -> active# X2)
    (active# fib X -> active# X, active# s X -> s# active X)
    (active# fib X -> active# X, active# s X -> active# X)
    (active# fib X -> active# X, active# fib N -> sel#(N, fib1(s 0(), s 0())))
    (active# fib X -> active# X, active# fib N -> fib1#(s 0(), s 0()))
    (active# fib X -> active# X, active# fib N -> s# 0())
    (active# fib X -> active# X, active# fib X -> active# X)
    (active# fib X -> active# X, active# fib X -> fib# active X)
    (active# fib X -> active# X, active# cons(X1, X2) -> active# X1)
    (active# fib X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# fib X -> active# X, active# add(X1, X2) -> active# X1)
    (active# fib X -> active# X, active# add(X1, X2) -> active# X2)
    (active# fib X -> active# X, active# add(X1, X2) -> add#(X1, active X2))
    (active# fib X -> active# X, active# add(X1, X2) -> add#(active X1, X2))
    (active# fib X -> active# X, active# add(s X, Y) -> s# add(X, Y))
    (active# fib X -> active# X, active# add(s X, Y) -> add#(X, Y))
    (s# ok X -> s# X, s# mark X -> s# X)
    (s# ok X -> s# X, s# ok X -> s# X)
    (add#(ok X1, ok X2) -> add#(X1, X2), add#(X1, mark X2) -> add#(X1, X2))
    (add#(ok X1, ok X2) -> add#(X1, X2), add#(mark X1, X2) -> add#(X1, X2))
    (add#(ok X1, ok X2) -> add#(X1, X2), add#(ok X1, ok 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#(mark X1, X2) -> add#(X1, X2))
    (add#(X1, mark X2) -> add#(X1, X2), add#(ok X1, ok X2) -> add#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (fib1#(mark X1, X2) -> fib1#(X1, X2), fib1#(X1, mark 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#(ok X1, ok X2) -> fib1#(X1, X2))
    (sel#(ok X1, ok X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
    (sel#(ok X1, ok X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
    (sel#(ok X1, ok X2) -> sel#(X1, X2), sel#(ok X1, ok 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#(mark X1, X2) -> sel#(X1, X2))
    (sel#(X1, mark X2) -> sel#(X1, X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
    (active# add(X1, X2) -> add#(active X1, X2), add#(X1, mark X2) -> add#(X1, X2))
    (active# add(X1, X2) -> add#(active X1, X2), add#(mark X1, X2) -> add#(X1, X2))
    (active# add(X1, X2) -> add#(active X1, X2), add#(ok X1, ok X2) -> add#(X1, X2))
    (active# fib1(X1, X2) -> fib1#(active X1, X2), fib1#(X1, mark X2) -> fib1#(X1, X2))
    (active# fib1(X1, X2) -> fib1#(active X1, X2), fib1#(mark X1, X2) -> fib1#(X1, X2))
    (active# fib1(X1, X2) -> fib1#(active X1, X2), fib1#(ok X1, ok X2) -> fib1#(X1, X2))
    (active# 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#(mark X1, X2) -> sel#(X1, X2))
    (active# sel(s N, cons(X, XS)) -> sel#(N, XS), sel#(ok X1, ok X2) -> sel#(X1, X2))
    (proper# cons(X1, X2) -> proper# X1, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X1, proper# fib1(X1, X2) -> fib1#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X1, proper# fib1(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X1, proper# fib1(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# cons(X1, X2) -> proper# X1, proper# fib X -> fib# proper X)
    (proper# cons(X1, X2) -> proper# X1, proper# fib X -> proper# X)
    (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
    (proper# sel(X1, X2) -> proper# X1, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# sel(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X2)
    (proper# sel(X1, X2) -> proper# X1, proper# fib1(X1, X2) -> fib1#(proper X1, proper X2))
    (proper# sel(X1, X2) -> proper# X1, proper# fib1(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X1, proper# fib1(X1, X2) -> proper# X2)
    (proper# sel(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# sel(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# sel(X1, X2) -> proper# X1, proper# fib X -> fib# proper X)
    (proper# sel(X1, X2) -> proper# X1, proper# fib X -> proper# X)
    (proper# sel(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# sel(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
    (proper# sel(X1, X2) -> proper# X1, proper# add(X1, X2) -> add#(proper X1, proper X2))
    (proper# sel(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X1, proper# add(X1, X2) -> proper# X2)
    (active# cons(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# cons(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# cons(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X1)
    (active# cons(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X2)
    (active# cons(X1, X2) -> active# X1, active# sel(s N, cons(X, XS)) -> sel#(N, XS))
    (active# cons(X1, X2) -> active# X1, active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
    (active# cons(X1, X2) -> active# X1, active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
    (active# cons(X1, X2) -> active# X1, active# fib1(X, Y) -> add#(X, Y))
    (active# cons(X1, X2) -> active# X1, active# fib1(X1, X2) -> fib1#(X1, active X2))
    (active# cons(X1, X2) -> active# X1, active# fib1(X1, X2) -> fib1#(active X1, X2))
    (active# cons(X1, X2) -> active# X1, active# fib1(X1, X2) -> active# X1)
    (active# cons(X1, X2) -> active# X1, active# fib1(X1, X2) -> active# X2)
    (active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# cons(X1, X2) -> active# X1, active# s X -> active# X)
    (active# cons(X1, X2) -> active# X1, active# fib N -> sel#(N, fib1(s 0(), s 0())))
    (active# cons(X1, X2) -> active# X1, active# fib N -> fib1#(s 0(), s 0()))
    (active# cons(X1, X2) -> active# X1, active# fib N -> s# 0())
    (active# cons(X1, X2) -> active# X1, active# fib X -> active# X)
    (active# cons(X1, X2) -> active# X1, active# fib X -> fib# active X)
    (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
    (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# cons(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
    (active# cons(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
    (active# cons(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
    (active# cons(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
    (active# cons(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
    (active# cons(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
    (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X2)
    (active# sel(X1, X2) -> active# X1, active# sel(s N, cons(X, XS)) -> sel#(N, XS))
    (active# sel(X1, X2) -> active# X1, active# fib1(X, Y) -> fib1#(Y, add(X, Y)))
    (active# sel(X1, X2) -> active# X1, active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))))
    (active# sel(X1, X2) -> active# X1, active# fib1(X, Y) -> add#(X, Y))
    (active# sel(X1, X2) -> active# X1, active# fib1(X1, X2) -> fib1#(X1, active X2))
    (active# sel(X1, X2) -> active# X1, active# fib1(X1, X2) -> fib1#(active X1, X2))
    (active# sel(X1, X2) -> active# X1, active# fib1(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X1, active# fib1(X1, X2) -> active# X2)
    (active# sel(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# sel(X1, X2) -> active# X1, active# s X -> active# X)
    (active# sel(X1, X2) -> active# X1, active# fib N -> sel#(N, fib1(s 0(), s 0())))
    (active# sel(X1, X2) -> active# X1, active# fib N -> fib1#(s 0(), s 0()))
    (active# sel(X1, X2) -> active# X1, active# fib N -> s# 0())
    (active# sel(X1, X2) -> active# X1, active# fib X -> active# X)
    (active# sel(X1, X2) -> active# X1, active# fib X -> fib# active X)
    (active# sel(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# sel(X1, X2) -> active# X1, active# add(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X1, active# add(X1, X2) -> active# X2)
    (active# sel(X1, X2) -> active# X1, active# add(X1, X2) -> add#(X1, active X2))
    (active# sel(X1, X2) -> active# X1, active# add(X1, X2) -> add#(active X1, X2))
    (active# sel(X1, X2) -> active# X1, active# add(s X, Y) -> s# add(X, Y))
    (active# sel(X1, X2) -> active# X1, active# add(s X, Y) -> add#(X, Y))
    (active# fib1(X, Y) -> add#(X, Y), add#(X1, mark 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#(ok X1, ok X2) -> add#(X1, X2))
    (active# fib N -> sel#(N, fib1(s 0(), s 0())), sel#(mark X1, X2) -> sel#(X1, X2))
    (proper# add(X1, X2) -> add#(proper X1, proper X2), add#(ok X1, ok X2) -> add#(X1, X2))
    (proper# fib1(X1, X2) -> fib1#(proper X1, proper X2), fib1#(ok X1, ok X2) -> fib1#(X1, X2))
    (active# add(X1, X2) -> add#(X1, active X2), add#(X1, mark X2) -> add#(X1, X2))
    (active# add(X1, X2) -> add#(X1, active X2), add#(mark X1, X2) -> add#(X1, X2))
    (active# add(X1, X2) -> add#(X1, active X2), add#(ok X1, ok X2) -> add#(X1, X2))
    (active# sel(X1, X2) -> sel#(X1, active X2), sel#(X1, mark X2) -> sel#(X1, X2))
    (active# sel(X1, X2) -> sel#(X1, active X2), sel#(mark X1, X2) -> sel#(X1, X2))
    (active# sel(X1, X2) -> sel#(X1, active X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
   }
   STATUS:
    arrows: 0.860042
    SCCS (9):
     Scc:
      {top# mark X -> top# proper X,
         top# ok X -> top# active X}
     Scc:
      { proper# sel(X1, X2) -> proper# X1,
        proper# sel(X1, X2) -> proper# X2,
       proper# fib1(X1, X2) -> proper# X1,
       proper# fib1(X1, X2) -> proper# X2,
                proper# s X -> proper# X,
              proper# fib X -> proper# X,
       proper# cons(X1, X2) -> proper# X1,
       proper# cons(X1, X2) -> proper# X2,
        proper# add(X1, X2) -> proper# X1,
        proper# add(X1, X2) -> proper# X2}
     Scc:
      { active# sel(X1, X2) -> active# X1,
        active# sel(X1, X2) -> active# X2,
       active# fib1(X1, X2) -> active# X1,
       active# fib1(X1, X2) -> active# X2,
                active# s X -> active# X,
              active# fib X -> active# X,
       active# cons(X1, X2) -> active# X1,
        active# add(X1, X2) -> active# X1,
        active# add(X1, X2) -> active# X2}
     Scc:
      {fib# mark X -> fib# X,
         fib# ok X -> fib# X}
     Scc:
      {s# mark X -> s# X,
         s# ok X -> s# X}
     Scc:
      { cons#(mark X1, X2) -> cons#(X1, X2),
       cons#(ok X1, ok X2) -> cons#(X1, X2)}
     Scc:
      { add#(X1, mark X2) -> add#(X1, X2),
        add#(mark X1, X2) -> add#(X1, X2),
       add#(ok X1, ok X2) -> add#(X1, X2)}
     Scc:
      { fib1#(X1, mark X2) -> fib1#(X1, X2),
        fib1#(mark X1, X2) -> fib1#(X1, X2),
       fib1#(ok X1, ok X2) -> fib1#(X1, X2)}
     Scc:
      { sel#(X1, mark X2) -> sel#(X1, X2),
        sel#(mark X1, X2) -> sel#(X1, X2),
       sel#(ok X1, ok X2) -> sel#(X1, X2)}
     
     SCC (2):
      Strict:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Weak:
      {            sel(X1, mark X2) -> mark sel(X1, X2),
                   sel(mark X1, X2) -> mark sel(X1, X2),
                  sel(ok X1, ok X2) -> ok sel(X1, X2),
                  fib1(X1, mark X2) -> mark fib1(X1, X2),
                  fib1(mark X1, X2) -> mark fib1(X1, X2),
                 fib1(ok X1, ok X2) -> ok fib1(X1, X2),
                           s mark X -> mark s X,
                             s ok X -> ok s X,
                 active sel(X1, X2) -> sel(X1, active X2),
                 active sel(X1, X2) -> sel(active X1, 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 fib1(X1, X2) -> fib1(X1, active X2),
                active fib1(X1, X2) -> fib1(active X1, X2),
                         active s X -> s active X,
                       active fib N -> mark sel(N, fib1(s 0(), s 0())),
                       active fib X -> fib active X,
                active cons(X1, X2) -> cons(active X1, X2),
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                         fib mark X -> mark fib X,
                           fib ok X -> ok fib X,
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                 proper sel(X1, X2) -> sel(proper X1, proper X2),
                proper fib1(X1, X2) -> fib1(proper X1, proper X2),
                         proper s X -> s proper X,
                         proper 0() -> ok 0(),
                       proper fib X -> fib proper X,
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper add(X1, X2) -> add(proper X1, proper X2),
                         top mark X -> top proper X,
                           top ok X -> top active X}
      Open
     
     
     SCC (10):
      Strict:
       { proper# sel(X1, X2) -> proper# X1,
         proper# sel(X1, X2) -> proper# X2,
        proper# fib1(X1, X2) -> proper# X1,
        proper# fib1(X1, X2) -> proper# X2,
                 proper# s X -> proper# X,
               proper# fib X -> proper# X,
        proper# cons(X1, X2) -> proper# X1,
        proper# cons(X1, X2) -> proper# X2,
         proper# add(X1, X2) -> proper# X1,
         proper# add(X1, X2) -> proper# X2}
      Weak:
      {            sel(X1, mark X2) -> mark sel(X1, X2),
                   sel(mark X1, X2) -> mark sel(X1, X2),
                  sel(ok X1, ok X2) -> ok sel(X1, X2),
                  fib1(X1, mark X2) -> mark fib1(X1, X2),
                  fib1(mark X1, X2) -> mark fib1(X1, X2),
                 fib1(ok X1, ok X2) -> ok fib1(X1, X2),
                           s mark X -> mark s X,
                             s ok X -> ok s X,
                 active sel(X1, X2) -> sel(X1, active X2),
                 active sel(X1, X2) -> sel(active X1, 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 fib1(X1, X2) -> fib1(X1, active X2),
                active fib1(X1, X2) -> fib1(active X1, X2),
                         active s X -> s active X,
                       active fib N -> mark sel(N, fib1(s 0(), s 0())),
                       active fib X -> fib active X,
                active cons(X1, X2) -> cons(active X1, X2),
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                         fib mark X -> mark fib X,
                           fib ok X -> ok fib X,
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                 proper sel(X1, X2) -> sel(proper X1, proper X2),
                proper fib1(X1, X2) -> fib1(proper X1, proper X2),
                         proper s X -> s proper X,
                         proper 0() -> ok 0(),
                       proper fib X -> fib proper X,
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper add(X1, X2) -> add(proper X1, proper X2),
                         top mark X -> top proper X,
                           top ok X -> top active X}
      Open
     
     
     SCC (9):
      Strict:
       { active# sel(X1, X2) -> active# X1,
         active# sel(X1, X2) -> active# X2,
        active# fib1(X1, X2) -> active# X1,
        active# fib1(X1, X2) -> active# X2,
                 active# s X -> active# X,
               active# fib X -> active# X,
        active# cons(X1, X2) -> active# X1,
         active# add(X1, X2) -> active# X1,
         active# add(X1, X2) -> active# X2}
      Weak:
      {            sel(X1, mark X2) -> mark sel(X1, X2),
                   sel(mark X1, X2) -> mark sel(X1, X2),
                  sel(ok X1, ok X2) -> ok sel(X1, X2),
                  fib1(X1, mark X2) -> mark fib1(X1, X2),
                  fib1(mark X1, X2) -> mark fib1(X1, X2),
                 fib1(ok X1, ok X2) -> ok fib1(X1, X2),
                           s mark X -> mark s X,
                             s ok X -> ok s X,
                 active sel(X1, X2) -> sel(X1, active X2),
                 active sel(X1, X2) -> sel(active X1, 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 fib1(X1, X2) -> fib1(X1, active X2),
                active fib1(X1, X2) -> fib1(active X1, X2),
                         active s X -> s active X,
                       active fib N -> mark sel(N, fib1(s 0(), s 0())),
                       active fib X -> fib active X,
                active cons(X1, X2) -> cons(active X1, X2),
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                         fib mark X -> mark fib X,
                           fib ok X -> ok fib X,
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                 proper sel(X1, X2) -> sel(proper X1, proper X2),
                proper fib1(X1, X2) -> fib1(proper X1, proper X2),
                         proper s X -> s proper X,
                         proper 0() -> ok 0(),
                       proper fib X -> fib proper X,
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper add(X1, X2) -> add(proper X1, proper X2),
                         top mark X -> top proper X,
                           top ok X -> top active X}
      Open
     
     
     
     
     SCC (2):
      Strict:
       {fib# mark X -> fib# X,
          fib# ok X -> fib# X}
      Weak:
      {            sel(X1, mark X2) -> mark sel(X1, X2),
                   sel(mark X1, X2) -> mark sel(X1, X2),
                  sel(ok X1, ok X2) -> ok sel(X1, X2),
                  fib1(X1, mark X2) -> mark fib1(X1, X2),
                  fib1(mark X1, X2) -> mark fib1(X1, X2),
                 fib1(ok X1, ok X2) -> ok fib1(X1, X2),
                           s mark X -> mark s X,
                             s ok X -> ok s X,
                 active sel(X1, X2) -> sel(X1, active X2),
                 active sel(X1, X2) -> sel(active X1, 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 fib1(X1, X2) -> fib1(X1, active X2),
                active fib1(X1, X2) -> fib1(active X1, X2),
                         active s X -> s active X,
                       active fib N -> mark sel(N, fib1(s 0(), s 0())),
                       active fib X -> fib active X,
                active cons(X1, X2) -> cons(active X1, X2),
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                         fib mark X -> mark fib X,
                           fib ok X -> ok fib X,
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                 proper sel(X1, X2) -> sel(proper X1, proper X2),
                proper fib1(X1, X2) -> fib1(proper X1, proper X2),
                         proper s X -> s proper X,
                         proper 0() -> ok 0(),
                       proper fib X -> fib proper X,
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper add(X1, X2) -> add(proper X1, proper X2),
                         top mark X -> top proper X,
                           top ok X -> top active X}
      Open
     
     
     
     SCC (2):
      Strict:
       {s# mark X -> s# X,
          s# ok X -> s# X}
      Weak:
      {            sel(X1, mark X2) -> mark sel(X1, X2),
                   sel(mark X1, X2) -> mark sel(X1, X2),
                  sel(ok X1, ok X2) -> ok sel(X1, X2),
                  fib1(X1, mark X2) -> mark fib1(X1, X2),
                  fib1(mark X1, X2) -> mark fib1(X1, X2),
                 fib1(ok X1, ok X2) -> ok fib1(X1, X2),
                           s mark X -> mark s X,
                             s ok X -> ok s X,
                 active sel(X1, X2) -> sel(X1, active X2),
                 active sel(X1, X2) -> sel(active X1, 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 fib1(X1, X2) -> fib1(X1, active X2),
                active fib1(X1, X2) -> fib1(active X1, X2),
                         active s X -> s active X,
                       active fib N -> mark sel(N, fib1(s 0(), s 0())),
                       active fib X -> fib active X,
                active cons(X1, X2) -> cons(active X1, X2),
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                         fib mark X -> mark fib X,
                           fib ok X -> ok fib X,
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                 proper sel(X1, X2) -> sel(proper X1, proper X2),
                proper fib1(X1, X2) -> fib1(proper X1, proper X2),
                         proper s X -> s proper X,
                         proper 0() -> ok 0(),
                       proper fib X -> fib proper X,
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper add(X1, X2) -> add(proper X1, proper X2),
                         top mark X -> top proper X,
                           top ok X -> top active X}
      Open
     
     
     
     
     
     
     
     
     
     
     SCC (2):
      Strict:
       { cons#(mark X1, X2) -> cons#(X1, X2),
        cons#(ok X1, ok X2) -> cons#(X1, X2)}
      Weak:
      {            sel(X1, mark X2) -> mark sel(X1, X2),
                   sel(mark X1, X2) -> mark sel(X1, X2),
                  sel(ok X1, ok X2) -> ok sel(X1, X2),
                  fib1(X1, mark X2) -> mark fib1(X1, X2),
                  fib1(mark X1, X2) -> mark fib1(X1, X2),
                 fib1(ok X1, ok X2) -> ok fib1(X1, X2),
                           s mark X -> mark s X,
                             s ok X -> ok s X,
                 active sel(X1, X2) -> sel(X1, active X2),
                 active sel(X1, X2) -> sel(active X1, 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 fib1(X1, X2) -> fib1(X1, active X2),
                active fib1(X1, X2) -> fib1(active X1, X2),
                         active s X -> s active X,
                       active fib N -> mark sel(N, fib1(s 0(), s 0())),
                       active fib X -> fib active X,
                active cons(X1, X2) -> cons(active X1, X2),
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                         fib mark X -> mark fib X,
                           fib ok X -> ok fib X,
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                 proper sel(X1, X2) -> sel(proper X1, proper X2),
                proper fib1(X1, X2) -> fib1(proper X1, proper X2),
                         proper s X -> s proper X,
                         proper 0() -> ok 0(),
                       proper fib X -> fib proper X,
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper add(X1, X2) -> add(proper X1, proper X2),
                         top mark X -> top proper X,
                           top ok X -> top active X}
      Open
     
     
     
     SCC (3):
      Strict:
       { add#(X1, mark X2) -> add#(X1, X2),
         add#(mark X1, X2) -> add#(X1, X2),
        add#(ok X1, ok X2) -> add#(X1, X2)}
      Weak:
      {            sel(X1, mark X2) -> mark sel(X1, X2),
                   sel(mark X1, X2) -> mark sel(X1, X2),
                  sel(ok X1, ok X2) -> ok sel(X1, X2),
                  fib1(X1, mark X2) -> mark fib1(X1, X2),
                  fib1(mark X1, X2) -> mark fib1(X1, X2),
                 fib1(ok X1, ok X2) -> ok fib1(X1, X2),
                           s mark X -> mark s X,
                             s ok X -> ok s X,
                 active sel(X1, X2) -> sel(X1, active X2),
                 active sel(X1, X2) -> sel(active X1, 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 fib1(X1, X2) -> fib1(X1, active X2),
                active fib1(X1, X2) -> fib1(active X1, X2),
                         active s X -> s active X,
                       active fib N -> mark sel(N, fib1(s 0(), s 0())),
                       active fib X -> fib active X,
                active cons(X1, X2) -> cons(active X1, X2),
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                         fib mark X -> mark fib X,
                           fib ok X -> ok fib X,
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                 proper sel(X1, X2) -> sel(proper X1, proper X2),
                proper fib1(X1, X2) -> fib1(proper X1, proper X2),
                         proper s X -> s proper X,
                         proper 0() -> ok 0(),
                       proper fib X -> fib proper X,
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper add(X1, X2) -> add(proper X1, proper X2),
                         top mark X -> top proper X,
                           top ok X -> top active X}
      Open
     
     SCC (3):
      Strict:
       { fib1#(X1, mark X2) -> fib1#(X1, X2),
         fib1#(mark X1, X2) -> fib1#(X1, X2),
        fib1#(ok X1, ok X2) -> fib1#(X1, X2)}
      Weak:
      {            sel(X1, mark X2) -> mark sel(X1, X2),
                   sel(mark X1, X2) -> mark sel(X1, X2),
                  sel(ok X1, ok X2) -> ok sel(X1, X2),
                  fib1(X1, mark X2) -> mark fib1(X1, X2),
                  fib1(mark X1, X2) -> mark fib1(X1, X2),
                 fib1(ok X1, ok X2) -> ok fib1(X1, X2),
                           s mark X -> mark s X,
                             s ok X -> ok s X,
                 active sel(X1, X2) -> sel(X1, active X2),
                 active sel(X1, X2) -> sel(active X1, 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 fib1(X1, X2) -> fib1(X1, active X2),
                active fib1(X1, X2) -> fib1(active X1, X2),
                         active s X -> s active X,
                       active fib N -> mark sel(N, fib1(s 0(), s 0())),
                       active fib X -> fib active X,
                active cons(X1, X2) -> cons(active X1, X2),
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                         fib mark X -> mark fib X,
                           fib ok X -> ok fib X,
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                 proper sel(X1, X2) -> sel(proper X1, proper X2),
                proper fib1(X1, X2) -> fib1(proper X1, proper X2),
                         proper s X -> s proper X,
                         proper 0() -> ok 0(),
                       proper fib X -> fib proper X,
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper add(X1, X2) -> add(proper X1, proper X2),
                         top mark X -> top proper X,
                           top ok X -> top active X}
      Open
     
     SCC (3):
      Strict:
       { sel#(X1, mark X2) -> sel#(X1, X2),
         sel#(mark X1, X2) -> sel#(X1, X2),
        sel#(ok X1, ok X2) -> sel#(X1, X2)}
      Weak:
      {            sel(X1, mark X2) -> mark sel(X1, X2),
                   sel(mark X1, X2) -> mark sel(X1, X2),
                  sel(ok X1, ok X2) -> ok sel(X1, X2),
                  fib1(X1, mark X2) -> mark fib1(X1, X2),
                  fib1(mark X1, X2) -> mark fib1(X1, X2),
                 fib1(ok X1, ok X2) -> ok fib1(X1, X2),
                           s mark X -> mark s X,
                             s ok X -> ok s X,
                 active sel(X1, X2) -> sel(X1, active X2),
                 active sel(X1, X2) -> sel(active X1, 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 fib1(X1, X2) -> fib1(X1, active X2),
                active fib1(X1, X2) -> fib1(active X1, X2),
                         active s X -> s active X,
                       active fib N -> mark sel(N, fib1(s 0(), s 0())),
                       active fib X -> fib active X,
                active cons(X1, X2) -> cons(active X1, X2),
                 active add(X1, X2) -> add(X1, active X2),
                 active add(X1, X2) -> add(active X1, X2),
                 active add(s X, Y) -> mark s add(X, Y),
                 active add(0(), X) -> mark X,
                         fib mark X -> mark fib X,
                           fib ok X -> ok fib X,
                  cons(mark X1, X2) -> mark cons(X1, X2),
                 cons(ok X1, ok X2) -> ok cons(X1, X2),
                   add(X1, mark X2) -> mark add(X1, X2),
                   add(mark X1, X2) -> mark add(X1, X2),
                  add(ok X1, ok X2) -> ok add(X1, X2),
                 proper sel(X1, X2) -> sel(proper X1, proper X2),
                proper fib1(X1, X2) -> fib1(proper X1, proper X2),
                         proper s X -> s proper X,
                         proper 0() -> ok 0(),
                       proper fib X -> fib proper X,
                proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper add(X1, X2) -> add(proper X1, proper X2),
                         top mark X -> top proper X,
                           top ok X -> top active X}
      Open