MAYBE
Time: 0.087104
TRS:
 {            mark cons(X1, X2) -> active cons(mark X1, X2),
                    mark from X -> active from mark X,
                       mark s X -> active s mark X,
                     mark nil() -> active nil(),
             mark first(X1, X2) -> active first(mark X1, mark X2),
                       mark 0() -> active 0(),
               mark sel(X1, X2) -> active sel(mark X1, mark X2),
              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),
                    from mark X -> from X,
                  from active X -> from X,
                       s mark X -> s X,
                     s active X -> s X,
                  active from X -> mark cons(X, from s X),
  active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
           active first(0(), Z) -> mark nil(),
    active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
    active sel(0(), cons(X, Z)) -> mark X,
             first(X1, mark X2) -> first(X1, X2),
           first(X1, active X2) -> first(X1, X2),
             first(mark X1, X2) -> first(X1, X2),
           first(active X1, X2) -> first(X1, 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)}
 DP:
  DP:
   {            mark# cons(X1, X2) -> mark# X1,
                mark# cons(X1, X2) -> cons#(mark X1, X2),
                mark# cons(X1, X2) -> active# cons(mark X1, X2),
                      mark# from X -> mark# X,
                      mark# from X -> from# mark X,
                      mark# from X -> active# from mark X,
                         mark# s X -> mark# X,
                         mark# s X -> s# mark X,
                         mark# s X -> active# s mark X,
                       mark# nil() -> active# nil(),
               mark# first(X1, X2) -> mark# X1,
               mark# first(X1, X2) -> mark# X2,
               mark# first(X1, X2) -> active# first(mark X1, mark X2),
               mark# first(X1, X2) -> first#(mark X1, mark X2),
                         mark# 0() -> active# 0(),
                 mark# sel(X1, X2) -> mark# X1,
                 mark# sel(X1, X2) -> mark# X2,
                 mark# sel(X1, X2) -> active# sel(mark X1, mark X2),
                 mark# sel(X1, X2) -> sel#(mark X1, mark X2),
                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),
                      from# mark X -> from# X,
                    from# active X -> from# X,
                         s# mark X -> s# X,
                       s# active X -> s# X,
                    active# from X -> mark# cons(X, from s X),
                    active# from X -> cons#(X, from s X),
                    active# from X -> from# s X,
                    active# from X -> s# X,
    active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)),
    active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)),
    active# first(s X, cons(Y, Z)) -> first#(X, Z),
             active# first(0(), Z) -> mark# nil(),
      active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z),
      active# sel(s X, cons(Y, Z)) -> sel#(X, Z),
      active# sel(0(), cons(X, Z)) -> mark# X,
               first#(X1, mark X2) -> first#(X1, X2),
             first#(X1, active X2) -> first#(X1, X2),
               first#(mark X1, X2) -> first#(X1, X2),
             first#(active X1, X2) -> first#(X1, 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)}
  TRS:
  {            mark cons(X1, X2) -> active cons(mark X1, X2),
                     mark from X -> active from mark X,
                        mark s X -> active s mark X,
                      mark nil() -> active nil(),
              mark first(X1, X2) -> active first(mark X1, mark X2),
                        mark 0() -> active 0(),
                mark sel(X1, X2) -> active sel(mark X1, mark X2),
               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),
                     from mark X -> from X,
                   from active X -> from X,
                        s mark X -> s X,
                      s active X -> s X,
                   active from X -> mark cons(X, from s X),
   active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
            active first(0(), Z) -> mark nil(),
     active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
     active sel(0(), cons(X, Z)) -> mark X,
              first(X1, mark X2) -> first(X1, X2),
            first(X1, active X2) -> first(X1, X2),
              first(mark X1, X2) -> first(X1, X2),
            first(active X1, X2) -> first(X1, 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)}
  EDG:
   {
    (mark# from X -> from# mark X, from# active X -> from# X)
    (mark# from X -> from# mark X, from# mark X -> from# X)
    (active# from X -> from# s X, from# active X -> from# X)
    (active# from X -> from# s X, from# mark X -> from# X)
    (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))
    (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))
    (first#(X1, active X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2))
    (first#(X1, active X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
    (first#(X1, active X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2))
    (first#(X1, active X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
    (first#(active X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2))
    (first#(active X1, X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
    (first#(active X1, X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2))
    (first#(active X1, X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(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))
    (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# sel(X1, X2) -> mark# X2)
    (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X2, mark# 0() -> active# 0())
    (mark# sel(X1, X2) -> mark# X2, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (mark# sel(X1, X2) -> mark# X2, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (mark# sel(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X2)
    (mark# sel(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X2, mark# nil() -> active# nil())
    (mark# sel(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# s X -> s# mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# s X -> mark# X)
    (mark# sel(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# from X -> from# mark X)
    (mark# sel(X1, X2) -> mark# X2, mark# from X -> mark# X)
    (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# cons(X1, X2) -> mark# X1)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# sel(X1, X2) -> sel#(mark X1, mark X2))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# sel(X1, X2) -> mark# X2)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# sel(X1, X2) -> mark# X1)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> first#(mark X1, mark X2))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> mark# X2)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# first(X1, X2) -> mark# X1)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# s X -> active# s mark X)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# s X -> s# mark X)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# s X -> mark# X)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# from X -> active# from mark X)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# from X -> from# mark X)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# from X -> mark# X)
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> cons#(mark X1, X2))
    (active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)), mark# cons(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
    (mark# s X -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
    (mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# 0() -> active# 0())
    (mark# s X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (mark# s X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X2)
    (mark# s X -> mark# X, mark# first(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# nil() -> active# nil())
    (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# from X -> active# from mark X)
    (mark# s X -> mark# X, mark# from X -> from# mark X)
    (mark# s X -> mark# X, mark# from X -> mark# X)
    (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (from# active X -> from# X, from# active X -> from# X)
    (from# active X -> from# X, from# mark X -> from# X)
    (s# active X -> s# X, s# active X -> s# X)
    (s# active X -> s# X, s# mark X -> s# X)
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# 0() -> active# 0())
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# first(X1, X2) -> mark# X2)
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# first(X1, X2) -> mark# X1)
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# nil() -> active# nil())
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# s X -> active# s mark X)
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# s X -> s# mark X)
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# s X -> mark# X)
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# from X -> active# from mark X)
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# from X -> from# mark X)
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# from X -> mark# X)
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (active# sel(0(), cons(X, Z)) -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sel(0(), cons(X, Z)) -> mark# X)
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z))
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(0(), Z) -> mark# nil())
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(s X, cons(Y, Z)) -> first#(X, Z))
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> s# X)
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> from# s X)
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> cons#(X, from s X))
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> mark# cons(X, from s X))
    (mark# from X -> active# from mark X, active# sel(0(), cons(X, Z)) -> mark# X)
    (mark# from X -> active# from mark X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (mark# from X -> active# from mark X, active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z))
    (mark# from X -> active# from mark X, active# first(0(), Z) -> mark# nil())
    (mark# from X -> active# from mark X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
    (mark# from X -> active# from mark X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
    (mark# from X -> active# from mark X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
    (mark# from X -> active# from mark X, active# from X -> s# X)
    (mark# from X -> active# from mark X, active# from X -> from# s X)
    (mark# from X -> active# from mark X, active# from X -> cons#(X, from s X))
    (mark# from X -> active# from mark X, active# from X -> mark# cons(X, from s X))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# sel(0(), cons(X, Z)) -> mark# X)
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(0(), Z) -> mark# nil())
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> first#(X, Z))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# from X -> s# X)
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# from X -> from# s X)
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# from X -> cons#(X, from s X))
    (mark# first(X1, X2) -> active# first(mark X1, mark X2), active# from X -> mark# cons(X, from s X))
    (active# from X -> mark# cons(X, from s X), mark# sel(X1, X2) -> sel#(mark X1, mark X2))
    (active# from X -> mark# cons(X, from s X), mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
    (active# from X -> mark# cons(X, from s X), mark# sel(X1, X2) -> mark# X2)
    (active# from X -> mark# cons(X, from s X), mark# sel(X1, X2) -> mark# X1)
    (active# from X -> mark# cons(X, from s X), mark# first(X1, X2) -> first#(mark X1, mark X2))
    (active# from X -> mark# cons(X, from s X), mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (active# from X -> mark# cons(X, from s X), mark# first(X1, X2) -> mark# X2)
    (active# from X -> mark# cons(X, from s X), mark# first(X1, X2) -> mark# X1)
    (active# from X -> mark# cons(X, from s X), mark# s X -> active# s mark X)
    (active# from X -> mark# cons(X, from s X), mark# s X -> s# mark X)
    (active# from X -> mark# cons(X, from s X), mark# s X -> mark# X)
    (active# from X -> mark# cons(X, from s X), mark# from X -> active# from mark X)
    (active# from X -> mark# cons(X, from s X), mark# from X -> from# mark X)
    (active# from X -> mark# cons(X, from s X), mark# from X -> mark# X)
    (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> cons#(mark X1, X2))
    (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> mark# X1)
    (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# sel(X1, X2) -> mark# X2)
    (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
    (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
    (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
    (mark# cons(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
    (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil())
    (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# from X -> from# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X)
    (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# cons(X1, X2) -> mark# X1)
    (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# sel(X1, X2) -> mark# X2)
    (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X1, mark# 0() -> active# 0())
    (mark# sel(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (mark# sel(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (mark# sel(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
    (mark# sel(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
    (mark# sel(X1, X2) -> mark# X1, mark# nil() -> active# nil())
    (mark# sel(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
    (mark# sel(X1, X2) -> mark# X1, mark# s X -> s# mark X)
    (mark# sel(X1, X2) -> mark# X1, mark# s X -> mark# X)
    (mark# sel(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
    (mark# sel(X1, X2) -> mark# X1, mark# from X -> from# mark X)
    (mark# sel(X1, X2) -> mark# X1, mark# from X -> mark# X)
    (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# cons(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# first(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# first(X1, X2) -> mark# X1, mark# from X -> mark# X)
    (mark# first(X1, X2) -> mark# X1, mark# from X -> from# mark X)
    (mark# first(X1, X2) -> mark# X1, mark# from X -> active# from mark X)
    (mark# first(X1, X2) -> mark# X1, mark# s X -> mark# X)
    (mark# first(X1, X2) -> mark# X1, mark# s X -> s# mark X)
    (mark# first(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
    (mark# first(X1, X2) -> mark# X1, mark# nil() -> active# nil())
    (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> mark# X2)
    (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (mark# first(X1, X2) -> mark# X1, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (mark# first(X1, X2) -> mark# X1, mark# 0() -> active# 0())
    (mark# first(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
    (mark# first(X1, X2) -> mark# X1, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
    (mark# first(X1, X2) -> mark# X1, mark# sel(X1, X2) -> sel#(mark X1, mark 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))
    (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# from X -> mark# cons(X, from s X))
    (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# from X -> cons#(X, from s X))
    (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# from X -> from# s X)
    (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# from X -> s# X)
    (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
    (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
    (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# first(s X, cons(Y, Z)) -> first#(X, Z))
    (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# first(0(), Z) -> mark# nil())
    (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z))
    (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(0(), cons(X, Z)) -> mark# X)
    (mark# s X -> active# s mark X, active# from X -> mark# cons(X, from s X))
    (mark# s X -> active# s mark X, active# from X -> cons#(X, from s X))
    (mark# s X -> active# s mark X, active# from X -> from# s X)
    (mark# s X -> active# s mark X, active# from X -> s# X)
    (mark# s X -> active# s mark X, active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)))
    (mark# s X -> active# s mark X, active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)))
    (mark# s X -> active# s mark X, active# first(s X, cons(Y, Z)) -> first#(X, Z))
    (mark# s X -> active# s mark X, active# first(0(), Z) -> mark# nil())
    (mark# s X -> active# s mark X, active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z))
    (mark# s X -> active# s mark X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (mark# s X -> active# s mark X, active# sel(0(), cons(X, Z)) -> mark# X)
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# cons(X1, X2) -> mark# X1)
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# cons(X1, X2) -> cons#(mark X1, X2))
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# from X -> mark# X)
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# from X -> from# mark X)
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# from X -> active# from mark X)
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# s X -> mark# X)
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# s X -> s# mark X)
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# s X -> active# s mark X)
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# first(X1, X2) -> mark# X1)
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# first(X1, X2) -> mark# X2)
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# first(X1, X2) -> first#(mark X1, mark X2))
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> mark# X1)
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> mark# X2)
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
    (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> sel#(mark X1, mark X2))
    (active# from X -> cons#(X, from s X), cons#(X1, mark X2) -> cons#(X1, X2))
    (active# from X -> cons#(X, from s X), cons#(X1, active X2) -> cons#(X1, X2))
    (s# mark X -> s# X, s# mark X -> s# X)
    (s# mark X -> s# X, s# active X -> s# X)
    (from# mark X -> from# X, from# mark X -> from# X)
    (from# mark X -> from# X, from# active X -> from# X)
    (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# from X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# from X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# from X -> mark# X, mark# from X -> mark# X)
    (mark# from X -> mark# X, mark# from X -> from# mark X)
    (mark# from X -> mark# X, mark# from X -> active# from mark X)
    (mark# from X -> mark# X, mark# s X -> mark# X)
    (mark# from X -> mark# X, mark# s X -> s# mark X)
    (mark# from X -> mark# X, mark# s X -> active# s mark X)
    (mark# from X -> mark# X, mark# nil() -> active# nil())
    (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X1)
    (mark# from X -> mark# X, mark# first(X1, X2) -> mark# X2)
    (mark# from X -> mark# X, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (mark# from X -> mark# X, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (mark# from X -> mark# X, mark# 0() -> active# 0())
    (mark# from X -> mark# X, mark# sel(X1, X2) -> mark# X1)
    (mark# from X -> mark# X, mark# sel(X1, X2) -> mark# X2)
    (mark# from X -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
    (mark# from X -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2))
    (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(X1, mark X2) -> cons#(X1, X2))
    (active# first(s X, cons(Y, Z)) -> cons#(Y, first(X, Z)), cons#(X1, active X2) -> cons#(X1, X2))
    (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# first(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# first(X1, X2) -> mark# X2, mark# from X -> mark# X)
    (mark# first(X1, X2) -> mark# X2, mark# from X -> from# mark X)
    (mark# first(X1, X2) -> mark# X2, mark# from X -> active# from mark X)
    (mark# first(X1, X2) -> mark# X2, mark# s X -> mark# X)
    (mark# first(X1, X2) -> mark# X2, mark# s X -> s# mark X)
    (mark# first(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
    (mark# first(X1, X2) -> mark# X2, mark# nil() -> active# nil())
    (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> mark# X2)
    (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> active# first(mark X1, mark X2))
    (mark# first(X1, X2) -> mark# X2, mark# first(X1, X2) -> first#(mark X1, mark X2))
    (mark# first(X1, X2) -> mark# X2, mark# 0() -> active# 0())
    (mark# first(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
    (mark# first(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
    (mark# first(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2))
    (mark# first(X1, X2) -> mark# X2, mark# sel(X1, X2) -> sel#(mark X1, mark 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))
    (first#(mark X1, X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
    (first#(mark X1, X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2))
    (first#(mark X1, X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
    (first#(mark X1, X2) -> first#(X1, X2), first#(active X1, X2) -> first#(X1, X2))
    (first#(X1, mark X2) -> first#(X1, X2), first#(X1, mark X2) -> first#(X1, X2))
    (first#(X1, mark X2) -> first#(X1, X2), first#(X1, active X2) -> first#(X1, X2))
    (first#(X1, mark X2) -> first#(X1, X2), first#(mark X1, X2) -> first#(X1, X2))
    (first#(X1, mark X2) -> first#(X1, X2), first#(active X1, X2) -> first#(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))
    (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(X1, mark X2) -> first#(X1, X2))
    (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(X1, active X2) -> first#(X1, X2))
    (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(mark X1, X2) -> first#(X1, X2))
    (mark# first(X1, X2) -> first#(mark X1, mark X2), first#(active X1, X2) -> first#(X1, X2))
    (mark# s X -> s# mark X, s# mark X -> s# X)
    (mark# s X -> s# mark X, s# active X -> s# X)
    (active# first(0(), Z) -> mark# nil(), mark# nil() -> active# nil())
   }
   STATUS:
    arrows: 0.841682
    SCCS (6):
     Scc:
      {            mark# cons(X1, X2) -> mark# X1,
                   mark# cons(X1, X2) -> active# cons(mark X1, X2),
                         mark# from X -> mark# X,
                         mark# from X -> active# from mark X,
                            mark# s X -> mark# X,
                            mark# s X -> active# s mark X,
                  mark# first(X1, X2) -> mark# X1,
                  mark# first(X1, X2) -> mark# X2,
                  mark# first(X1, X2) -> active# first(mark X1, mark X2),
                    mark# sel(X1, X2) -> mark# X1,
                    mark# sel(X1, X2) -> mark# X2,
                    mark# sel(X1, X2) -> active# sel(mark X1, mark X2),
                       active# from X -> mark# cons(X, from s X),
       active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)),
         active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z),
         active# sel(0(), cons(X, Z)) -> mark# X}
     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:
      {  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:
      {  first#(X1, mark X2) -> first#(X1, X2),
       first#(X1, active X2) -> first#(X1, X2),
         first#(mark X1, X2) -> first#(X1, X2),
       first#(active X1, X2) -> first#(X1, X2)}
     Scc:
      {  s# mark X -> s# X,
       s# active X -> s# X}
     Scc:
      {  from# mark X -> from# X,
       from# active X -> from# X}
     
     SCC (16):
      Strict:
       {            mark# cons(X1, X2) -> mark# X1,
                    mark# cons(X1, X2) -> active# cons(mark X1, X2),
                          mark# from X -> mark# X,
                          mark# from X -> active# from mark X,
                             mark# s X -> mark# X,
                             mark# s X -> active# s mark X,
                   mark# first(X1, X2) -> mark# X1,
                   mark# first(X1, X2) -> mark# X2,
                   mark# first(X1, X2) -> active# first(mark X1, mark X2),
                     mark# sel(X1, X2) -> mark# X1,
                     mark# sel(X1, X2) -> mark# X2,
                     mark# sel(X1, X2) -> active# sel(mark X1, mark X2),
                        active# from X -> mark# cons(X, from s X),
        active# first(s X, cons(Y, Z)) -> mark# cons(Y, first(X, Z)),
          active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z),
          active# sel(0(), cons(X, Z)) -> mark# X}
      Weak:
      {            mark cons(X1, X2) -> active cons(mark X1, X2),
                         mark from X -> active from mark X,
                            mark s X -> active s mark X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                            mark 0() -> active 0(),
                    mark sel(X1, X2) -> active sel(mark X1, mark X2),
                   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),
                         from mark X -> from X,
                       from active X -> from X,
                            s mark X -> s X,
                          s active X -> s X,
                       active from X -> mark cons(X, from s X),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                active first(0(), Z) -> mark nil(),
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
         active sel(0(), cons(X, Z)) -> mark X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, 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)}
      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 cons(X1, X2) -> active cons(mark X1, X2),
                         mark from X -> active from mark X,
                            mark s X -> active s mark X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                            mark 0() -> active 0(),
                    mark sel(X1, X2) -> active sel(mark X1, mark X2),
                   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),
                         from mark X -> from X,
                       from active X -> from X,
                            s mark X -> s X,
                          s active X -> s X,
                       active from X -> mark cons(X, from s X),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                active first(0(), Z) -> mark nil(),
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
         active sel(0(), cons(X, Z)) -> mark X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, 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)}
      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 cons(X1, X2) -> active cons(mark X1, X2),
                         mark from X -> active from mark X,
                            mark s X -> active s mark X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                            mark 0() -> active 0(),
                    mark sel(X1, X2) -> active sel(mark X1, mark X2),
                   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),
                         from mark X -> from X,
                       from active X -> from X,
                            s mark X -> s X,
                          s active X -> s X,
                       active from X -> mark cons(X, from s X),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                active first(0(), Z) -> mark nil(),
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
         active sel(0(), cons(X, Z)) -> mark X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, 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)}
      Open
     
     SCC (4):
      Strict:
       {  first#(X1, mark X2) -> first#(X1, X2),
        first#(X1, active X2) -> first#(X1, X2),
          first#(mark X1, X2) -> first#(X1, X2),
        first#(active X1, X2) -> first#(X1, X2)}
      Weak:
      {            mark cons(X1, X2) -> active cons(mark X1, X2),
                         mark from X -> active from mark X,
                            mark s X -> active s mark X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                            mark 0() -> active 0(),
                    mark sel(X1, X2) -> active sel(mark X1, mark X2),
                   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),
                         from mark X -> from X,
                       from active X -> from X,
                            s mark X -> s X,
                          s active X -> s X,
                       active from X -> mark cons(X, from s X),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                active first(0(), Z) -> mark nil(),
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
         active sel(0(), cons(X, Z)) -> mark X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, 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)}
      Open
     
     
     SCC (2):
      Strict:
       {  s# mark X -> s# X,
        s# active X -> s# X}
      Weak:
      {            mark cons(X1, X2) -> active cons(mark X1, X2),
                         mark from X -> active from mark X,
                            mark s X -> active s mark X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                            mark 0() -> active 0(),
                    mark sel(X1, X2) -> active sel(mark X1, mark X2),
                   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),
                         from mark X -> from X,
                       from active X -> from X,
                            s mark X -> s X,
                          s active X -> s X,
                       active from X -> mark cons(X, from s X),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                active first(0(), Z) -> mark nil(),
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
         active sel(0(), cons(X, Z)) -> mark X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, 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)}
      Open
     
     SCC (2):
      Strict:
       {  from# mark X -> from# X,
        from# active X -> from# X}
      Weak:
      {            mark cons(X1, X2) -> active cons(mark X1, X2),
                         mark from X -> active from mark X,
                            mark s X -> active s mark X,
                          mark nil() -> active nil(),
                  mark first(X1, X2) -> active first(mark X1, mark X2),
                            mark 0() -> active 0(),
                    mark sel(X1, X2) -> active sel(mark X1, mark X2),
                   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),
                         from mark X -> from X,
                       from active X -> from X,
                            s mark X -> s X,
                          s active X -> s X,
                       active from X -> mark cons(X, from s X),
       active first(s X, cons(Y, Z)) -> mark cons(Y, first(X, Z)),
                active first(0(), Z) -> mark nil(),
         active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
         active sel(0(), cons(X, Z)) -> mark X,
                  first(X1, mark X2) -> first(X1, X2),
                first(X1, active X2) -> first(X1, X2),
                  first(mark X1, X2) -> first(X1, X2),
                first(active X1, X2) -> first(X1, 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)}
      Open