MAYBE
Time: 3.310214
TRS:
 {          cons(mark X1, X2) -> mark cons(X1, X2),
           cons(ok X1, ok X2) -> ok cons(X1, X2),
                  from mark X -> mark from X,
                    from ok X -> ok from X,
                     s mark X -> mark s X,
                       s ok X -> ok s X,
          active cons(X1, X2) -> cons(active X1, X2),
                active from X -> mark cons(X, from s X),
                active from X -> from active X,
                   active s X -> s active X,
           active sel(X1, X2) -> sel(X1, active X2),
           active sel(X1, X2) -> sel(active X1, X2),
  active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
  active sel(0(), cons(X, Y)) -> mark X,
             sel(X1, mark X2) -> mark sel(X1, X2),
             sel(mark X1, X2) -> mark sel(X1, X2),
            sel(ok X1, ok X2) -> ok sel(X1, X2),
          proper cons(X1, X2) -> cons(proper X1, proper X2),
                proper from X -> from proper X,
                   proper s X -> s proper X,
           proper sel(X1, X2) -> sel(proper X1, proper X2),
                   proper 0() -> ok 0(),
                   top mark X -> top proper X,
                     top ok X -> top active X}
 DP:
  DP:
   {          cons#(mark X1, X2) -> cons#(X1, X2),
             cons#(ok X1, ok X2) -> cons#(X1, X2),
                    from# mark X -> from# X,
                      from# ok X -> from# X,
                       s# mark X -> s# X,
                         s# ok X -> s# X,
            active# cons(X1, X2) -> cons#(active X1, X2),
            active# cons(X1, X2) -> active# X1,
                  active# from X -> cons#(X, from s X),
                  active# from X -> from# s X,
                  active# from X -> from# active X,
                  active# from X -> s# X,
                  active# from X -> active# X,
                     active# s X -> s# active X,
                     active# s X -> active# X,
             active# sel(X1, X2) -> active# X1,
             active# sel(X1, X2) -> active# X2,
             active# sel(X1, X2) -> sel#(X1, active X2),
             active# sel(X1, X2) -> sel#(active X1, X2),
    active# sel(s X, cons(Y, Z)) -> sel#(X, Z),
               sel#(X1, mark X2) -> sel#(X1, X2),
               sel#(mark X1, X2) -> sel#(X1, X2),
              sel#(ok X1, ok X2) -> sel#(X1, X2),
            proper# cons(X1, X2) -> cons#(proper X1, proper X2),
            proper# cons(X1, X2) -> proper# X1,
            proper# cons(X1, X2) -> proper# X2,
                  proper# from X -> from# proper X,
                  proper# from X -> proper# X,
                     proper# s X -> s# proper X,
                     proper# s X -> proper# X,
             proper# sel(X1, X2) -> sel#(proper X1, proper X2),
             proper# sel(X1, X2) -> proper# X1,
             proper# sel(X1, X2) -> proper# X2,
                     top# mark X -> proper# X,
                     top# mark X -> top# proper X,
                       top# ok X -> active# X,
                       top# ok X -> top# active X}
  TRS:
  {          cons(mark X1, X2) -> mark cons(X1, X2),
            cons(ok X1, ok X2) -> ok cons(X1, X2),
                   from mark X -> mark from X,
                     from ok X -> ok from X,
                      s mark X -> mark s X,
                        s ok X -> ok s X,
           active cons(X1, X2) -> cons(active X1, X2),
                 active from X -> mark cons(X, from s X),
                 active from X -> from active X,
                    active s X -> s active X,
            active sel(X1, X2) -> sel(X1, active X2),
            active sel(X1, X2) -> sel(active X1, X2),
   active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
   active sel(0(), cons(X, Y)) -> mark X,
              sel(X1, mark X2) -> mark sel(X1, X2),
              sel(mark X1, X2) -> mark sel(X1, X2),
             sel(ok X1, ok X2) -> ok sel(X1, X2),
           proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper from X -> from proper X,
                    proper s X -> s proper X,
            proper sel(X1, X2) -> sel(proper X1, proper X2),
                    proper 0() -> ok 0(),
                    top mark X -> top proper X,
                      top ok X -> top active X}
  EDG:
   {
    (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (sel#(mark X1, X2) -> sel#(X1, X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
    (sel#(mark X1, X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
    (sel#(mark X1, X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
    (active# cons(X1, X2) -> active# X1, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (active# cons(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# cons(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# cons(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X2)
    (active# cons(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X1)
    (active# cons(X1, X2) -> active# X1, active# s X -> active# X)
    (active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# cons(X1, X2) -> active# X1, active# from X -> active# X)
    (active# cons(X1, X2) -> active# X1, active# from X -> s# X)
    (active# cons(X1, X2) -> active# X1, active# from X -> from# active X)
    (active# cons(X1, X2) -> active# X1, active# from X -> from# s X)
    (active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
    (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
    (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
    (proper# cons(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X1, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# cons(X1, X2) -> proper# X1, proper# from X -> proper# X)
    (proper# cons(X1, X2) -> proper# X1, proper# from X -> from# proper X)
    (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (active# from X -> from# s X, from# ok X -> from# X)
    (active# from X -> from# s X, from# mark X -> from# X)
    (active# s X -> s# active X, s# ok X -> s# X)
    (active# s X -> s# active X, s# mark X -> s# X)
    (proper# s X -> s# proper X, s# ok X -> s# X)
    (top# ok X -> top# active X, top# ok X -> top# active X)
    (top# ok X -> top# active X, top# ok X -> active# X)
    (top# ok X -> top# active X, top# mark X -> top# proper X)
    (top# ok X -> top# active X, top# mark X -> proper# X)
    (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (active# from X -> cons#(X, from s X), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
    (from# ok X -> from# X, from# ok X -> from# X)
    (from# ok X -> from# X, from# mark X -> from# X)
    (s# ok X -> s# X, s# ok X -> s# X)
    (s# ok X -> s# X, s# mark X -> s# X)
    (active# from X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (active# from X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# from X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# from X -> active# X, active# sel(X1, X2) -> active# X2)
    (active# from X -> active# X, active# sel(X1, X2) -> active# X1)
    (active# from X -> active# X, active# s X -> active# X)
    (active# from X -> active# X, active# s X -> s# active X)
    (active# from X -> active# X, active# from X -> active# X)
    (active# from X -> active# X, active# from X -> s# X)
    (active# from X -> active# X, active# from X -> from# active X)
    (active# from X -> active# X, active# from X -> from# s X)
    (active# from X -> active# X, active# from X -> cons#(X, from s X))
    (active# from X -> active# X, active# cons(X1, X2) -> active# X1)
    (active# from X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (proper# from X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (proper# from X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (proper# from X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# from X -> proper# X, proper# s X -> proper# X)
    (proper# from X -> proper# X, proper# s X -> s# proper X)
    (proper# from X -> proper# X, proper# from X -> proper# X)
    (proper# from X -> proper# X, proper# from X -> from# proper X)
    (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (top# mark X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# s X -> proper# X)
    (top# mark X -> proper# X, proper# s X -> s# proper X)
    (top# mark X -> proper# X, proper# from X -> proper# X)
    (top# mark X -> proper# X, proper# from X -> from# proper X)
    (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (active# sel(X1, X2) -> active# X2, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X2)
    (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X2, active# s X -> active# X)
    (active# sel(X1, X2) -> active# X2, active# s X -> s# active X)
    (active# sel(X1, X2) -> active# X2, active# from X -> active# X)
    (active# sel(X1, X2) -> active# X2, active# from X -> s# X)
    (active# sel(X1, X2) -> active# X2, active# from X -> from# active X)
    (active# sel(X1, X2) -> active# X2, active# from X -> from# s X)
    (active# sel(X1, X2) -> active# X2, active# from X -> cons#(X, from s X))
    (active# sel(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
    (proper# sel(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X2)
    (proper# sel(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X2, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# sel(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# sel(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# sel(X1, X2) -> proper# X2, proper# from X -> proper# X)
    (proper# sel(X1, X2) -> proper# X2, proper# from X -> from# proper X)
    (proper# sel(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
    (proper# sel(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (active# sel(X1, X2) -> sel#(active X1, X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
    (active# sel(X1, X2) -> sel#(active X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
    (active# sel(X1, X2) -> sel#(active X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
    (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(X1, mark X2) -> sel#(X1, X2))
    (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(mark X1, X2) -> sel#(X1, X2))
    (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(ok X1, ok X2) -> sel#(X1, X2))
    (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X2, proper# from X -> from# proper X)
    (proper# cons(X1, X2) -> proper# X2, proper# from X -> proper# X)
    (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# cons(X1, X2) -> proper# X2, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X2)
    (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# from X -> cons#(X, from s X))
    (top# ok X -> active# X, active# from X -> from# s X)
    (top# ok X -> active# X, active# from X -> from# active X)
    (top# ok X -> active# X, active# from X -> s# X)
    (top# ok X -> active# X, active# from X -> active# X)
    (top# ok X -> active# X, active# s X -> s# active X)
    (top# ok X -> active# X, active# s X -> active# X)
    (top# ok X -> active# X, active# sel(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# sel(X1, X2) -> active# X2)
    (top# ok X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
    (top# ok X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
    (top# ok X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# from X -> from# proper X)
    (proper# s X -> proper# X, proper# from X -> proper# X)
    (proper# s X -> proper# X, proper# s X -> s# proper X)
    (proper# s X -> proper# X, proper# s X -> proper# X)
    (proper# s X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# s X -> active# X, active# cons(X1, X2) -> active# X1)
    (active# s X -> active# X, active# from X -> cons#(X, from s X))
    (active# s X -> active# X, active# from X -> from# s X)
    (active# s X -> active# X, active# from X -> from# active X)
    (active# s X -> active# X, active# from X -> s# X)
    (active# s X -> active# X, active# from X -> active# X)
    (active# s X -> active# X, active# s X -> s# active X)
    (active# s X -> active# X, active# s X -> active# X)
    (active# s X -> active# X, active# sel(X1, X2) -> active# X1)
    (active# s X -> active# X, active# sel(X1, X2) -> active# X2)
    (active# s X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# s X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# s X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (active# from X -> s# X, s# mark X -> s# X)
    (active# from X -> s# X, s# ok X -> s# X)
    (s# mark X -> s# X, s# mark X -> s# X)
    (s# mark X -> s# X, s# ok X -> s# X)
    (from# mark X -> from# X, from# mark X -> from# X)
    (from# mark X -> from# X, from# ok X -> from# X)
    (proper# sel(X1, X2) -> sel#(proper X1, proper X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
    (active# sel(X1, X2) -> sel#(X1, active X2), sel#(X1, mark X2) -> sel#(X1, X2))
    (active# sel(X1, X2) -> sel#(X1, active X2), sel#(mark X1, X2) -> sel#(X1, X2))
    (active# sel(X1, X2) -> sel#(X1, active X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
    (top# mark X -> top# proper X, top# ok X -> active# X)
    (top# mark X -> top# proper X, top# ok X -> top# active X)
    (proper# from X -> from# proper X, from# ok X -> from# X)
    (active# from X -> from# active X, from# mark X -> from# X)
    (active# from X -> from# active X, from# ok X -> from# X)
    (proper# sel(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# sel(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
    (proper# sel(X1, X2) -> proper# X1, proper# from X -> from# proper X)
    (proper# sel(X1, X2) -> proper# X1, proper# from X -> proper# X)
    (proper# sel(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# sel(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# sel(X1, X2) -> proper# X1, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# sel(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X1, proper# sel(X1, X2) -> proper# X2)
    (active# sel(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# sel(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
    (active# sel(X1, X2) -> active# X1, active# from X -> from# s X)
    (active# sel(X1, X2) -> active# X1, active# from X -> from# active X)
    (active# sel(X1, X2) -> active# X1, active# from X -> s# X)
    (active# sel(X1, X2) -> active# X1, active# from X -> active# X)
    (active# sel(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# sel(X1, X2) -> active# X1, active# s X -> active# X)
    (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> active# X2)
    (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# sel(X1, X2) -> active# X1, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# sel(X1, X2) -> active# X1, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (sel#(ok X1, ok X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
    (sel#(ok X1, ok X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
    (sel#(ok X1, ok X2) -> sel#(X1, X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
    (sel#(X1, mark X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2))
    (sel#(X1, mark X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2))
    (sel#(X1, mark X2) -> sel#(X1, X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
   }
   STATUS:
    arrows: 0.849525
    SCCS (7):
     Scc:
      {top# mark X -> top# proper X,
         top# ok X -> top# active X}
     Scc:
      {proper# cons(X1, X2) -> proper# X1,
       proper# cons(X1, X2) -> proper# X2,
             proper# from X -> proper# X,
                proper# s X -> proper# X,
        proper# sel(X1, X2) -> proper# X1,
        proper# sel(X1, X2) -> proper# X2}
     Scc:
      {active# cons(X1, X2) -> active# X1,
             active# from X -> active# X,
                active# s X -> active# X,
        active# sel(X1, X2) -> active# X1,
        active# sel(X1, X2) -> active# X2}
     Scc:
      {s# mark X -> s# X,
         s# ok X -> s# X}
     Scc:
      {from# mark X -> from# X,
         from# ok X -> from# X}
     Scc:
      { sel#(X1, mark X2) -> sel#(X1, X2),
        sel#(mark X1, X2) -> sel#(X1, X2),
       sel#(ok X1, ok X2) -> sel#(X1, X2)}
     Scc:
      { cons#(mark X1, X2) -> cons#(X1, X2),
       cons#(ok X1, ok X2) -> cons#(X1, X2)}
     
     SCC (2):
      Strict:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Weak:
      {          cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                       from mark X -> mark from X,
                         from ok X -> ok from X,
                          s mark X -> mark s X,
                            s ok X -> ok s X,
               active cons(X1, X2) -> cons(active X1, X2),
                     active from X -> mark cons(X, from s X),
                     active from X -> from active X,
                        active s X -> s active X,
                active sel(X1, X2) -> sel(X1, active X2),
                active sel(X1, X2) -> sel(active X1, X2),
       active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
       active sel(0(), cons(X, Y)) -> mark X,
                  sel(X1, mark X2) -> mark sel(X1, X2),
                  sel(mark X1, X2) -> mark sel(X1, X2),
                 sel(ok X1, ok X2) -> ok sel(X1, X2),
               proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper from X -> from proper X,
                        proper s X -> s proper X,
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open
     
     
     SCC (6):
      Strict:
       {proper# cons(X1, X2) -> proper# X1,
        proper# cons(X1, X2) -> proper# X2,
              proper# from X -> proper# X,
                 proper# s X -> proper# X,
         proper# sel(X1, X2) -> proper# X1,
         proper# sel(X1, X2) -> proper# X2}
      Weak:
      {          cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                       from mark X -> mark from X,
                         from ok X -> ok from X,
                          s mark X -> mark s X,
                            s ok X -> ok s X,
               active cons(X1, X2) -> cons(active X1, X2),
                     active from X -> mark cons(X, from s X),
                     active from X -> from active X,
                        active s X -> s active X,
                active sel(X1, X2) -> sel(X1, active X2),
                active sel(X1, X2) -> sel(active X1, X2),
       active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
       active sel(0(), cons(X, Y)) -> mark X,
                  sel(X1, mark X2) -> mark sel(X1, X2),
                  sel(mark X1, X2) -> mark sel(X1, X2),
                 sel(ok X1, ok X2) -> ok sel(X1, X2),
               proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper from X -> from proper X,
                        proper s X -> s proper X,
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open
     
     
     
     
     SCC (5):
      Strict:
       {active# cons(X1, X2) -> active# X1,
              active# from X -> active# X,
                 active# s X -> active# X,
         active# sel(X1, X2) -> active# X1,
         active# sel(X1, X2) -> active# X2}
      Weak:
      {          cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                       from mark X -> mark from X,
                         from ok X -> ok from X,
                          s mark X -> mark s X,
                            s ok X -> ok s X,
               active cons(X1, X2) -> cons(active X1, X2),
                     active from X -> mark cons(X, from s X),
                     active from X -> from active X,
                        active s X -> s active X,
                active sel(X1, X2) -> sel(X1, active X2),
                active sel(X1, X2) -> sel(active X1, X2),
       active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
       active sel(0(), cons(X, Y)) -> mark X,
                  sel(X1, mark X2) -> mark sel(X1, X2),
                  sel(mark X1, X2) -> mark sel(X1, X2),
                 sel(ok X1, ok X2) -> ok sel(X1, X2),
               proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper from X -> from proper X,
                        proper s X -> s proper X,
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open
     
     
     
     
     
     SCC (2):
      Strict:
       {s# mark X -> s# X,
          s# ok X -> s# X}
      Weak:
      {          cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                       from mark X -> mark from X,
                         from ok X -> ok from X,
                          s mark X -> mark s X,
                            s ok X -> ok s X,
               active cons(X1, X2) -> cons(active X1, X2),
                     active from X -> mark cons(X, from s X),
                     active from X -> from active X,
                        active s X -> s active X,
                active sel(X1, X2) -> sel(X1, active X2),
                active sel(X1, X2) -> sel(active X1, X2),
       active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
       active sel(0(), cons(X, Y)) -> mark X,
                  sel(X1, mark X2) -> mark sel(X1, X2),
                  sel(mark X1, X2) -> mark sel(X1, X2),
                 sel(ok X1, ok X2) -> ok sel(X1, X2),
               proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper from X -> from proper X,
                        proper s X -> s proper X,
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open
     
     
     SCC (2):
      Strict:
       {from# mark X -> from# X,
          from# ok X -> from# X}
      Weak:
      {          cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                       from mark X -> mark from X,
                         from ok X -> ok from X,
                          s mark X -> mark s X,
                            s ok X -> ok s X,
               active cons(X1, X2) -> cons(active X1, X2),
                     active from X -> mark cons(X, from s X),
                     active from X -> from active X,
                        active s X -> s active X,
                active sel(X1, X2) -> sel(X1, active X2),
                active sel(X1, X2) -> sel(active X1, X2),
       active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
       active sel(0(), cons(X, Y)) -> mark X,
                  sel(X1, mark X2) -> mark sel(X1, X2),
                  sel(mark X1, X2) -> mark sel(X1, X2),
                 sel(ok X1, ok X2) -> ok sel(X1, X2),
               proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper from X -> from proper X,
                        proper s X -> s proper X,
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open
     
     
     SCC (3):
      Strict:
       { sel#(X1, mark X2) -> sel#(X1, X2),
         sel#(mark X1, X2) -> sel#(X1, X2),
        sel#(ok X1, ok X2) -> sel#(X1, X2)}
      Weak:
      {          cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                       from mark X -> mark from X,
                         from ok X -> ok from X,
                          s mark X -> mark s X,
                            s ok X -> ok s X,
               active cons(X1, X2) -> cons(active X1, X2),
                     active from X -> mark cons(X, from s X),
                     active from X -> from active X,
                        active s X -> s active X,
                active sel(X1, X2) -> sel(X1, active X2),
                active sel(X1, X2) -> sel(active X1, X2),
       active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
       active sel(0(), cons(X, Y)) -> mark X,
                  sel(X1, mark X2) -> mark sel(X1, X2),
                  sel(mark X1, X2) -> mark sel(X1, X2),
                 sel(ok X1, ok X2) -> ok sel(X1, X2),
               proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper from X -> from proper X,
                        proper s X -> s proper X,
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open
     SCC (2):
      Strict:
       { cons#(mark X1, X2) -> cons#(X1, X2),
        cons#(ok X1, ok X2) -> cons#(X1, X2)}
      Weak:
      {          cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                       from mark X -> mark from X,
                         from ok X -> ok from X,
                          s mark X -> mark s X,
                            s ok X -> ok s X,
               active cons(X1, X2) -> cons(active X1, X2),
                     active from X -> mark cons(X, from s X),
                     active from X -> from active X,
                        active s X -> s active X,
                active sel(X1, X2) -> sel(X1, active X2),
                active sel(X1, X2) -> sel(active X1, X2),
       active sel(s X, cons(Y, Z)) -> mark sel(X, Z),
       active sel(0(), cons(X, Y)) -> mark X,
                  sel(X1, mark X2) -> mark sel(X1, X2),
                  sel(mark X1, X2) -> mark sel(X1, X2),
                 sel(ok X1, ok X2) -> ok sel(X1, X2),
               proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper from X -> from proper X,
                        proper s X -> s proper X,
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        proper 0() -> ok 0(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open