MAYBE
Time: 0.088409
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:
  DP:
   {            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)}
  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)}
  EDG:
   {
    (mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(active X1, 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#(X1, active X2) -> sel#(X1, X2))
    (mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(X1, mark X2) -> sel#(X1, X2))
    (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, 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#(X1, active X2) -> add#(X1, X2))
    (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(X1, X2))
    (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))
    (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)
    (mark# fib1(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, 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) -> mark# X2)
    (mark# fib1(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
    (mark# fib1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (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) -> mark# X1)
    (mark# fib1(X1, X2) -> mark# X2, mark# fib X -> fib# mark X)
    (mark# fib1(X1, X2) -> mark# X2, mark# fib X -> active# fib mark X)
    (mark# fib1(X1, X2) -> mark# X2, mark# fib X -> mark# X)
    (mark# fib1(X1, X2) -> mark# X2, mark# 0() -> active# 0())
    (mark# fib1(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
    (mark# fib1(X1, X2) -> mark# X2, mark# s X -> s# mark X)
    (mark# fib1(X1, X2) -> mark# X2, mark# s X -> mark# X)
    (mark# fib1(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> active# fib1(mark X1, 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) -> mark# X2)
    (mark# fib1(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X1)
    (mark# fib1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, 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) -> mark# X2)
    (mark# fib1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# add(0(), X) -> mark# X)
    (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(s X, Y) -> 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) -> active# cons(mark X1, X2), active# fib N -> 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 -> 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) -> active# cons(mark X1, X2), active# fib1(X, 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) -> 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) -> active# cons(mark X1, X2), active# sel(0(), cons(X, XS)) -> mark# X)
    (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(s N, cons(X, XS)) -> mark# sel(N, XS))
    (active# add(s X, Y) -> s# add(X, Y), s# active X -> s# X)
    (active# add(s X, Y) -> s# add(X, Y), s# mark X -> s# X)
    (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# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# add(X1, X2) -> 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) -> 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) -> 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) -> 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 -> fib# 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 -> 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# s X -> s# 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) -> 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) -> 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# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))), cons#(active X1, 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#(X1, active X2) -> cons#(X1, X2))
    (active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))), cons#(X1, mark X2) -> cons#(X1, X2))
    (active# fib1(X, Y) -> add#(X, Y), add#(active X1, 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#(X1, active X2) -> add#(X1, X2))
    (active# fib1(X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(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))
    (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)
    (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# fib X -> fib# mark X, fib# mark X -> fib# X)
    (mark# fib X -> fib# mark X, fib# active X -> fib# X)
    (active# add(s X, Y) -> add#(X, Y), add#(X1, mark 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#(mark X1, X2) -> add#(X1, X2))
    (active# add(s X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2))
    (active# fib N -> sel#(N, fib1(s 0(), s 0())), sel#(mark X1, X2) -> sel#(X1, X2))
    (active# fib N -> sel#(N, fib1(s 0(), s 0())), sel#(active X1, X2) -> sel#(X1, X2))
    (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) -> 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 -> 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) -> 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# 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# s X -> s# 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# 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# fib X -> 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# cons(X1, X2) -> active# cons(mark X1, X2))
    (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# 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))
    (active# fib N -> mark# sel(N, fib1(s 0(), s 0())), mark# add(X1, X2) -> add#(mark X1, mark 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#(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))
    (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))
    (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) -> 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)) -> 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) -> fib1#(mark X1, 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# s X -> 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)) -> 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# fib X -> 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# cons(X1, X2) -> active# cons(mark X1, X2))
    (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# 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))
    (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# add(X1, X2) -> add#(mark X1, mark X2))
    (mark# add(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
    (mark# add(X1, X2) -> mark# X2, mark# sel(X1, X2) -> 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) -> active# sel(mark X1, mark X2))
    (mark# add(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X1)
    (mark# add(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> 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) -> active# fib1(mark X1, mark X2))
    (mark# add(X1, X2) -> mark# X2, mark# s X -> mark# X)
    (mark# add(X1, X2) -> mark# X2, mark# s X -> s# mark X)
    (mark# add(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
    (mark# add(X1, X2) -> mark# X2, mark# 0() -> active# 0())
    (mark# add(X1, X2) -> mark# X2, mark# fib X -> mark# X)
    (mark# add(X1, X2) -> mark# X2, mark# fib X -> active# fib mark X)
    (mark# add(X1, X2) -> mark# X2, mark# fib X -> fib# mark X)
    (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
    (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) -> cons#(mark X1, X2))
    (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
    (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> 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) -> add#(mark X1, mark X2))
    (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> 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) -> active# sel(mark X1, mark X2))
    (mark# sel(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> 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) -> active# fib1(mark X1, mark X2))
    (mark# sel(X1, X2) -> mark# X2, mark# s X -> mark# X)
    (mark# sel(X1, X2) -> mark# X2, mark# s X -> s# mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# 0() -> active# 0())
    (mark# sel(X1, X2) -> mark# X2, mark# fib X -> mark# X)
    (mark# sel(X1, X2) -> mark# X2, mark# fib X -> active# fib mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# fib X -> fib# mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
    (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) -> cons#(mark X1, X2))
    (mark# sel(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X2, mark# add(X1, X2) -> 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) -> add#(mark X1, mark 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)
    (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# fib1(X1, X2) -> fib1#(mark X1, mark X2), fib1#(X1, mark 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#(mark X1, X2) -> fib1#(X1, X2))
    (mark# fib1(X1, X2) -> fib1#(mark X1, mark X2), fib1#(active X1, X2) -> fib1#(X1, X2))
    (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2))
    (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
   }
   EDG:
    {
     (mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(active X1, 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#(X1, active X2) -> sel#(X1, X2))
     (mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(X1, mark X2) -> sel#(X1, X2))
     (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, 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#(X1, active X2) -> add#(X1, X2))
     (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(X1, X2))
     (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))
     (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# 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())))
     (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)
     (mark# fib1(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, 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) -> mark# X2)
     (mark# fib1(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
     (mark# fib1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (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) -> mark# X1)
     (mark# fib1(X1, X2) -> mark# X2, mark# fib X -> fib# mark X)
     (mark# fib1(X1, X2) -> mark# X2, mark# fib X -> active# fib mark X)
     (mark# fib1(X1, X2) -> mark# X2, mark# fib X -> mark# X)
     (mark# fib1(X1, X2) -> mark# X2, mark# 0() -> active# 0())
     (mark# fib1(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
     (mark# fib1(X1, X2) -> mark# X2, mark# s X -> s# mark X)
     (mark# fib1(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# fib1(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> active# fib1(mark X1, 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) -> mark# X2)
     (mark# fib1(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X1)
     (mark# fib1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, 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) -> mark# X2)
     (mark# fib1(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# 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# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# cons(X1, X2) -> mark# X1)
     (active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))), cons#(active X1, 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) -> add#(X, Y), add#(active X1, 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#(X1, active X2) -> add#(X1, X2))
     (active# fib1(X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(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))
     (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)
     (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# fib X -> fib# mark X, fib# mark X -> fib# X)
     (mark# fib X -> fib# mark X, fib# active X -> fib# X)
     (active# add(s X, Y) -> add#(X, Y), add#(X1, mark 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#(mark X1, X2) -> add#(X1, X2))
     (active# add(s X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2))
     (active# fib N -> sel#(N, fib1(s 0(), s 0())), sel#(mark X1, X2) -> sel#(X1, X2))
     (active# fib N -> sel#(N, fib1(s 0(), s 0())), sel#(active X1, X2) -> sel#(X1, X2))
     (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) -> 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# 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))
     (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))
     (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) -> 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))
     (mark# add(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
     (mark# add(X1, X2) -> mark# X2, mark# sel(X1, X2) -> 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) -> active# sel(mark X1, mark X2))
     (mark# add(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X1)
     (mark# add(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> 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) -> active# fib1(mark X1, mark X2))
     (mark# add(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# add(X1, X2) -> mark# X2, mark# s X -> s# mark X)
     (mark# add(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
     (mark# add(X1, X2) -> mark# X2, mark# 0() -> active# 0())
     (mark# add(X1, X2) -> mark# X2, mark# fib X -> mark# X)
     (mark# add(X1, X2) -> mark# X2, mark# fib X -> active# fib mark X)
     (mark# add(X1, X2) -> mark# X2, mark# fib X -> fib# mark X)
     (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (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) -> cons#(mark X1, X2))
     (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
     (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> 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) -> add#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> 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) -> active# sel(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> 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) -> active# fib1(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# s X -> s# mark X)
     (mark# sel(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
     (mark# sel(X1, X2) -> mark# X2, mark# 0() -> active# 0())
     (mark# sel(X1, X2) -> mark# X2, mark# fib X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# fib X -> active# fib mark X)
     (mark# sel(X1, X2) -> mark# X2, mark# fib X -> fib# mark X)
     (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (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) -> cons#(mark X1, X2))
     (mark# sel(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# add(X1, X2) -> 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) -> add#(mark X1, mark X2))
     (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# 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)
     (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# fib1(X1, X2) -> fib1#(mark X1, mark X2), fib1#(X1, mark 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#(mark X1, X2) -> fib1#(X1, X2))
     (mark# fib1(X1, X2) -> fib1#(mark X1, mark X2), fib1#(active X1, X2) -> fib1#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    }
    EDG:
     {
      (mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(active X1, 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#(X1, active X2) -> sel#(X1, X2))
      (mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(X1, mark X2) -> sel#(X1, X2))
      (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(active X1, 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#(X1, active X2) -> add#(X1, X2))
      (mark# add(X1, X2) -> add#(mark X1, mark X2), add#(X1, mark X2) -> add#(X1, X2))
      (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))
      (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# 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())))
      (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)
      (mark# fib1(X1, X2) -> mark# X2, mark# add(X1, X2) -> add#(mark X1, 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) -> mark# X2)
      (mark# fib1(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
      (mark# fib1(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (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) -> mark# X1)
      (mark# fib1(X1, X2) -> mark# X2, mark# fib X -> fib# mark X)
      (mark# fib1(X1, X2) -> mark# X2, mark# fib X -> active# fib mark X)
      (mark# fib1(X1, X2) -> mark# X2, mark# fib X -> mark# X)
      (mark# fib1(X1, X2) -> mark# X2, mark# 0() -> active# 0())
      (mark# fib1(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
      (mark# fib1(X1, X2) -> mark# X2, mark# s X -> s# mark X)
      (mark# fib1(X1, X2) -> mark# X2, mark# s X -> mark# X)
      (mark# fib1(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> active# fib1(mark X1, 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) -> mark# X2)
      (mark# fib1(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X1)
      (mark# fib1(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, 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) -> mark# X2)
      (mark# fib1(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# 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# cons(X1, X2) -> active# cons(mark X1, X2))
      (active# fib1(X, Y) -> mark# cons(X, fib1(Y, add(X, Y))), mark# cons(X1, X2) -> mark# X1)
      (active# fib1(X, Y) -> cons#(X, fib1(Y, add(X, Y))), cons#(active X1, 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) -> add#(X, Y), add#(active X1, 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#(X1, active X2) -> add#(X1, X2))
      (active# fib1(X, Y) -> add#(X, Y), add#(X1, mark X2) -> add#(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))
      (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)
      (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# fib X -> fib# mark X, fib# mark X -> fib# X)
      (mark# fib X -> fib# mark X, fib# active X -> fib# X)
      (active# add(s X, Y) -> add#(X, Y), add#(X1, mark 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#(mark X1, X2) -> add#(X1, X2))
      (active# add(s X, Y) -> add#(X, Y), add#(active X1, X2) -> add#(X1, X2))
      (active# fib N -> sel#(N, fib1(s 0(), s 0())), sel#(mark X1, X2) -> sel#(X1, X2))
      (active# fib N -> sel#(N, fib1(s 0(), s 0())), sel#(active X1, X2) -> sel#(X1, X2))
      (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) -> 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# 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))
      (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))
      (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) -> 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))
      (mark# add(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
      (mark# add(X1, X2) -> mark# X2, mark# sel(X1, X2) -> 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) -> active# sel(mark X1, mark X2))
      (mark# add(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X1)
      (mark# add(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> 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) -> active# fib1(mark X1, mark X2))
      (mark# add(X1, X2) -> mark# X2, mark# s X -> mark# X)
      (mark# add(X1, X2) -> mark# X2, mark# s X -> s# mark X)
      (mark# add(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
      (mark# add(X1, X2) -> mark# X2, mark# 0() -> active# 0())
      (mark# add(X1, X2) -> mark# X2, mark# fib X -> mark# X)
      (mark# add(X1, X2) -> mark# X2, mark# fib X -> active# fib mark X)
      (mark# add(X1, X2) -> mark# X2, mark# fib X -> fib# mark X)
      (mark# add(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
      (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) -> cons#(mark X1, X2))
      (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
      (mark# add(X1, X2) -> mark# X2, mark# add(X1, X2) -> 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) -> add#(mark X1, mark X2))
      (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
      (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> 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) -> active# sel(mark X1, mark X2))
      (mark# sel(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> mark# X1)
      (mark# sel(X1, X2) -> mark# X2, mark# fib1(X1, X2) -> 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) -> active# fib1(mark X1, mark X2))
      (mark# sel(X1, X2) -> mark# X2, mark# s X -> mark# X)
      (mark# sel(X1, X2) -> mark# X2, mark# s X -> s# mark X)
      (mark# sel(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
      (mark# sel(X1, X2) -> mark# X2, mark# 0() -> active# 0())
      (mark# sel(X1, X2) -> mark# X2, mark# fib X -> mark# X)
      (mark# sel(X1, X2) -> mark# X2, mark# fib X -> active# fib mark X)
      (mark# sel(X1, X2) -> mark# X2, mark# fib X -> fib# mark X)
      (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
      (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) -> cons#(mark X1, X2))
      (mark# sel(X1, X2) -> mark# X2, mark# add(X1, X2) -> mark# X1)
      (mark# sel(X1, X2) -> mark# X2, mark# add(X1, X2) -> 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) -> add#(mark X1, mark X2))
      (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# 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)
      (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# fib1(X1, X2) -> fib1#(mark X1, mark X2), fib1#(X1, mark 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#(mark X1, X2) -> fib1#(X1, X2))
      (mark# fib1(X1, X2) -> fib1#(mark X1, mark X2), fib1#(active X1, X2) -> fib1#(X1, X2))
      (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2))
      (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     }
     STATUS:
      arrows: 0.882733
      SCCS (7):
       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:
        {  fib# mark X -> fib# X,
         fib# active X -> fib# X}
       Scc:
        {  s# mark X -> s# X,
         s# active X -> s# X}
       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:
        {  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:
        {  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 (19):
        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)}
        Open
       
       
       
       
       
       
       
       
       SCC (2):
        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)}
        Open
       
       
       
       
       
       
       SCC (2):
        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)}
        Open
       
       SCC (4):
        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)}
        Open
       
       SCC (4):
        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)}
        Open
       
       SCC (4):
        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)}
        Open
       
       SCC (4):
        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)}
        Open