MAYBE
Time: 0.012399
TRS:
 {          cons(mark X1, X2) -> mark cons(X1, X2),
           cons(ok X1, ok X2) -> ok cons(X1, X2),
                     f mark X -> mark f X,
                       f ok X -> ok f X,
                     g mark X -> mark g X,
                       g ok X -> ok g X,
          active cons(X1, X2) -> cons(active X1, X2),
                   active f X -> mark cons(X, f g X),
                   active f X -> f active X,
                   active g X -> g active X,
                 active g s X -> mark s s g X,
                 active g 0() -> mark s 0(),
                   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,
                     s mark X -> mark s X,
                       s ok X -> ok s 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 f X -> f proper X,
                   proper g X -> g proper X,
                   proper s X -> s proper X,
                   proper 0() -> ok 0(),
           proper sel(X1, X2) -> sel(proper X1, proper X2),
                   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),
                       f# mark X -> f# X,
                         f# ok X -> f# X,
                       g# mark X -> g# X,
                         g# ok X -> g# X,
            active# cons(X1, X2) -> cons#(active X1, X2),
            active# cons(X1, X2) -> active# X1,
                     active# f X -> cons#(X, f g X),
                     active# f X -> f# g X,
                     active# f X -> f# active X,
                     active# f X -> g# X,
                     active# f X -> active# X,
                     active# g X -> g# active X,
                     active# g X -> active# X,
                   active# g s X -> g# X,
                   active# g s X -> s# g X,
                   active# g s X -> s# s g X,
                   active# g 0() -> s# 0(),
                     active# s X -> active# X,
                     active# s X -> s# 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),
                       s# mark X -> s# X,
                         s# ok X -> s# X,
               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# f X -> f# proper X,
                     proper# f X -> proper# X,
                     proper# g X -> g# proper X,
                     proper# g 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),
                      f mark X -> mark f X,
                        f ok X -> ok f X,
                      g mark X -> mark g X,
                        g ok X -> ok g X,
           active cons(X1, X2) -> cons(active X1, X2),
                    active f X -> mark cons(X, f g X),
                    active f X -> f active X,
                    active g X -> g active X,
                  active g s X -> mark s s g X,
                  active g 0() -> mark s 0(),
                    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,
                      s mark X -> mark s X,
                        s ok X -> ok s 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 f X -> f proper X,
                    proper g X -> g proper X,
                    proper s X -> s proper X,
                    proper 0() -> ok 0(),
            proper sel(X1, X2) -> sel(proper X1, proper X2),
                    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# f X -> f# g X, f# ok X -> f# X)
    (active# f X -> f# g X, f# mark X -> f# X)
    (active# g X -> g# active X, g# ok X -> g# X)
    (active# g X -> g# active X, g# mark X -> g# X)
    (active# s X -> s# active X, s# ok X -> s# X)
    (active# s X -> s# active X, s# mark X -> s# X)
    (proper# g X -> g# proper X, g# ok X -> g# X)
    (proper# g X -> g# proper X, g# mark X -> g# X)
    (top# mark X -> top# proper X, top# ok X -> top# active X)
    (top# mark X -> top# proper X, top# ok X -> active# X)
    (top# mark X -> top# proper X, top# mark X -> top# proper X)
    (top# mark X -> top# proper X, top# mark X -> proper# X)
    (active# sel(X1, X2) -> sel#(X1, active X2), sel#(ok X1, ok 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#(X1, mark X2) -> sel#(X1, X2))
    (proper# sel(X1, X2) -> sel#(proper X1, proper X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
    (proper# sel(X1, X2) -> sel#(proper X1, proper X2), sel#(mark X1, X2) -> sel#(X1, X2))
    (proper# sel(X1, X2) -> sel#(proper X1, proper X2), sel#(X1, mark X2) -> sel#(X1, X2))
    (proper# cons(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X2, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# cons(X1, X2) -> proper# X2, proper# g X -> proper# X)
    (proper# cons(X1, X2) -> proper# X2, proper# g X -> g# proper X)
    (proper# cons(X1, X2) -> proper# X2, proper# f X -> proper# X)
    (proper# cons(X1, X2) -> proper# X2, proper# f X -> f# proper X)
    (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper 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 -> s# active X)
    (active# cons(X1, X2) -> active# X1, active# s X -> active# X)
    (active# cons(X1, X2) -> active# X1, active# g 0() -> s# 0())
    (active# cons(X1, X2) -> active# X1, active# g s X -> s# s g X)
    (active# cons(X1, X2) -> active# X1, active# g s X -> s# g X)
    (active# cons(X1, X2) -> active# X1, active# g s X -> g# X)
    (active# cons(X1, X2) -> active# X1, active# g X -> active# X)
    (active# cons(X1, X2) -> active# X1, active# g X -> g# active X)
    (active# cons(X1, X2) -> active# X1, active# f X -> active# X)
    (active# cons(X1, X2) -> active# X1, active# f X -> g# X)
    (active# cons(X1, X2) -> active# X1, active# f X -> f# active X)
    (active# cons(X1, X2) -> active# X1, active# f X -> f# g X)
    (active# cons(X1, X2) -> active# X1, active# f X -> cons#(X, f g 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# g X -> proper# X)
    (proper# cons(X1, X2) -> proper# X1, proper# g X -> g# proper X)
    (proper# cons(X1, X2) -> proper# X1, proper# f X -> proper# X)
    (proper# cons(X1, X2) -> proper# X1, proper# f X -> f# 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# g s X -> s# s g X, s# ok X -> s# X)
    (active# g s X -> s# s g X, s# mark X -> s# X)
    (active# f X -> cons#(X, f g X), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (active# f X -> cons#(X, f g X), cons#(mark X1, X2) -> cons#(X1, X2))
    (f# ok X -> f# X, f# ok X -> f# X)
    (f# ok X -> f# X, f# mark X -> f# X)
    (g# ok X -> g# X, g# ok X -> g# X)
    (g# ok X -> g# X, g# mark X -> g# X)
    (active# f X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (active# f X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# f X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# f X -> active# X, active# sel(X1, X2) -> active# X2)
    (active# f X -> active# X, active# sel(X1, X2) -> active# X1)
    (active# f X -> active# X, active# s X -> s# active X)
    (active# f X -> active# X, active# s X -> active# X)
    (active# f X -> active# X, active# g 0() -> s# 0())
    (active# f X -> active# X, active# g s X -> s# s g X)
    (active# f X -> active# X, active# g s X -> s# g X)
    (active# f X -> active# X, active# g s X -> g# X)
    (active# f X -> active# X, active# g X -> active# X)
    (active# f X -> active# X, active# g X -> g# active X)
    (active# f X -> active# X, active# f X -> active# X)
    (active# f X -> active# X, active# f X -> g# X)
    (active# f X -> active# X, active# f X -> f# active X)
    (active# f X -> active# X, active# f X -> f# g X)
    (active# f X -> active# X, active# f X -> cons#(X, f g X))
    (active# f X -> active# X, active# cons(X1, X2) -> active# X1)
    (active# f X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# g s X -> g# X, g# ok X -> g# X)
    (active# g s X -> g# X, g# mark X -> g# X)
    (s# mark X -> s# X, s# ok X -> s# X)
    (s# mark X -> s# X, s# mark X -> s# X)
    (proper# f X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (proper# f X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (proper# f X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# f X -> proper# X, proper# s X -> proper# X)
    (proper# f X -> proper# X, proper# s X -> s# proper X)
    (proper# f X -> proper# X, proper# g X -> proper# X)
    (proper# f X -> proper# X, proper# g X -> g# proper X)
    (proper# f X -> proper# X, proper# f X -> proper# X)
    (proper# f X -> proper# X, proper# f X -> f# proper X)
    (proper# f X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# f X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# f X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# s X -> proper# X)
    (proper# s X -> proper# X, proper# s X -> s# proper X)
    (proper# s X -> proper# X, proper# g X -> proper# X)
    (proper# s X -> proper# X, proper# g X -> g# proper X)
    (proper# s X -> proper# X, proper# f X -> proper# X)
    (proper# s X -> proper# X, proper# f X -> f# proper X)
    (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (top# ok X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (top# ok X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
    (top# ok X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
    (top# ok X -> active# X, active# sel(X1, X2) -> active# X2)
    (top# ok X -> active# X, active# sel(X1, X2) -> active# X1)
    (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# g 0() -> s# 0())
    (top# ok X -> active# X, active# g s X -> s# s g X)
    (top# ok X -> active# X, active# g s X -> s# g X)
    (top# ok X -> active# X, active# g s X -> g# X)
    (top# ok X -> active# X, active# g X -> active# X)
    (top# ok X -> active# X, active# g X -> g# active X)
    (top# ok X -> active# X, active# f X -> active# X)
    (top# ok X -> active# X, active# f X -> g# X)
    (top# ok X -> active# X, active# f X -> f# active X)
    (top# ok X -> active# X, active# f X -> f# g X)
    (top# ok X -> active# X, active# f X -> cons#(X, f g X))
    (top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (active# sel(X1, X2) -> sel#(active X1, X2), sel#(X1, mark 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#(ok X1, ok X2) -> sel#(X1, X2))
    (active# g 0() -> s# 0(), s# mark X -> s# X)
    (active# g 0() -> s# 0(), s# ok X -> s# X)
    (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (top# mark X -> proper# X, proper# f X -> f# proper X)
    (top# mark X -> proper# X, proper# f X -> proper# X)
    (top# mark X -> proper# X, proper# g X -> g# proper X)
    (top# mark X -> proper# X, proper# g X -> proper# X)
    (top# mark X -> proper# X, proper# s X -> s# proper X)
    (top# mark X -> proper# X, proper# s X -> proper# X)
    (top# mark X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (proper# g X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# g X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# g X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# g X -> proper# X, proper# f X -> f# proper X)
    (proper# g X -> proper# X, proper# f X -> proper# X)
    (proper# g X -> proper# X, proper# g X -> g# proper X)
    (proper# g X -> proper# X, proper# g X -> proper# X)
    (proper# g X -> proper# X, proper# s X -> s# proper X)
    (proper# g X -> proper# X, proper# s X -> proper# X)
    (proper# g X -> proper# X, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# g X -> proper# X, proper# sel(X1, X2) -> proper# X1)
    (proper# g X -> proper# X, proper# sel(X1, X2) -> proper# X2)
    (s# ok X -> s# X, s# mark X -> s# X)
    (s# ok X -> s# X, s# ok X -> s# X)
    (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# f X -> cons#(X, f g X))
    (active# s X -> active# X, active# f X -> f# g X)
    (active# s X -> active# X, active# f X -> f# active X)
    (active# s X -> active# X, active# f X -> g# X)
    (active# s X -> active# X, active# f X -> active# X)
    (active# s X -> active# X, active# g X -> g# active X)
    (active# s X -> active# X, active# g X -> active# X)
    (active# s X -> active# X, active# g s X -> g# X)
    (active# s X -> active# X, active# g s X -> s# g X)
    (active# s X -> active# X, active# g s X -> s# s g X)
    (active# s X -> active# X, active# g 0() -> s# 0())
    (active# s X -> active# X, active# s X -> active# X)
    (active# s X -> active# X, active# s X -> s# active X)
    (active# s X -> active# X, active# 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# g X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# g X -> active# X, active# cons(X1, X2) -> active# X1)
    (active# g X -> active# X, active# f X -> cons#(X, f g X))
    (active# g X -> active# X, active# f X -> f# g X)
    (active# g X -> active# X, active# f X -> f# active X)
    (active# g X -> active# X, active# f X -> g# X)
    (active# g X -> active# X, active# f X -> active# X)
    (active# g X -> active# X, active# g X -> g# active X)
    (active# g X -> active# X, active# g X -> active# X)
    (active# g X -> active# X, active# g s X -> g# X)
    (active# g X -> active# X, active# g s X -> s# g X)
    (active# g X -> active# X, active# g s X -> s# s g X)
    (active# g X -> active# X, active# g 0() -> s# 0())
    (active# g X -> active# X, active# s X -> active# X)
    (active# g X -> active# X, active# s X -> s# active X)
    (active# g X -> active# X, active# sel(X1, X2) -> active# X1)
    (active# g X -> active# X, active# sel(X1, X2) -> active# X2)
    (active# g X -> active# X, active# sel(X1, X2) -> sel#(X1, active X2))
    (active# g X -> active# X, active# sel(X1, X2) -> sel#(active X1, X2))
    (active# g X -> active# X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (active# f X -> g# X, g# mark X -> g# X)
    (active# f X -> g# X, g# ok X -> g# X)
    (g# mark X -> g# X, g# mark X -> g# X)
    (g# mark X -> g# X, g# ok X -> g# X)
    (f# mark X -> f# X, f# mark X -> f# X)
    (f# mark X -> f# X, f# ok X -> f# X)
    (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))
    (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# f X -> f# proper X)
    (proper# sel(X1, X2) -> proper# X1, proper# f X -> proper# X)
    (proper# sel(X1, X2) -> proper# X1, proper# g X -> g# proper X)
    (proper# sel(X1, X2) -> proper# X1, proper# g 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# f X -> cons#(X, f g X))
    (active# sel(X1, X2) -> active# X1, active# f X -> f# g X)
    (active# sel(X1, X2) -> active# X1, active# f X -> f# active X)
    (active# sel(X1, X2) -> active# X1, active# f X -> g# X)
    (active# sel(X1, X2) -> active# X1, active# f X -> active# X)
    (active# sel(X1, X2) -> active# X1, active# g X -> g# active X)
    (active# sel(X1, X2) -> active# X1, active# g X -> active# X)
    (active# sel(X1, X2) -> active# X1, active# g s X -> g# X)
    (active# sel(X1, X2) -> active# X1, active# g s X -> s# g X)
    (active# sel(X1, X2) -> active# X1, active# g s X -> s# s g X)
    (active# sel(X1, X2) -> active# X1, active# g 0() -> s# 0())
    (active# sel(X1, X2) -> active# X1, active# s X -> active# X)
    (active# sel(X1, X2) -> active# X1, active# s X -> s# 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))
    (proper# sel(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# sel(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
    (proper# sel(X1, X2) -> proper# X2, proper# f X -> f# proper X)
    (proper# sel(X1, X2) -> proper# X2, proper# f X -> proper# X)
    (proper# sel(X1, X2) -> proper# X2, proper# g X -> g# proper X)
    (proper# sel(X1, X2) -> proper# X2, proper# g X -> proper# X)
    (proper# sel(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# sel(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# sel(X1, X2) -> proper# X2, proper# sel(X1, X2) -> sel#(proper X1, proper X2))
    (proper# sel(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X1)
    (proper# sel(X1, X2) -> proper# X2, proper# sel(X1, X2) -> proper# X2)
    (active# sel(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# sel(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X2, active# f X -> cons#(X, f g X))
    (active# sel(X1, X2) -> active# X2, active# f X -> f# g X)
    (active# sel(X1, X2) -> active# X2, active# f X -> f# active X)
    (active# sel(X1, X2) -> active# X2, active# f X -> g# X)
    (active# sel(X1, X2) -> active# X2, active# f X -> active# X)
    (active# sel(X1, X2) -> active# X2, active# g X -> g# active X)
    (active# sel(X1, X2) -> active# X2, active# g X -> active# X)
    (active# sel(X1, X2) -> active# X2, active# g s X -> g# X)
    (active# sel(X1, X2) -> active# X2, active# g s X -> s# g X)
    (active# sel(X1, X2) -> active# X2, active# g s X -> s# s g X)
    (active# sel(X1, X2) -> active# X2, active# g 0() -> s# 0())
    (active# sel(X1, X2) -> active# X2, active# s X -> active# X)
    (active# sel(X1, X2) -> active# X2, active# s X -> s# active X)
    (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> active# X1)
    (active# sel(X1, X2) -> active# X2, active# sel(X1, X2) -> active# 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) -> sel#(active X1, X2))
    (active# sel(X1, X2) -> active# X2, active# sel(s X, cons(Y, Z)) -> sel#(X, Z))
    (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (top# ok X -> top# active X, top# mark X -> proper# X)
    (top# ok X -> top# active X, top# mark X -> top# proper X)
    (top# ok X -> top# active X, top# ok X -> active# X)
    (top# ok X -> top# active X, top# ok X -> top# active X)
    (proper# s X -> s# proper X, s# mark X -> s# X)
    (proper# s X -> s# proper X, s# ok X -> s# X)
    (proper# f X -> f# proper X, f# mark X -> f# X)
    (proper# f X -> f# proper X, f# ok X -> f# X)
    (active# g s X -> s# g X, s# mark X -> s# X)
    (active# g s X -> s# g X, s# ok X -> s# X)
    (active# f X -> f# active X, f# mark X -> f# X)
    (active# f X -> f# active X, f# ok X -> f# X)
    (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.859212
    SCCS (8):
     Scc:
      {top# mark X -> top# proper X,
         top# ok X -> top# active X}
     Scc:
      {active# cons(X1, X2) -> active# X1,
                active# f X -> active# X,
                active# g X -> active# X,
                active# s X -> active# X,
        active# sel(X1, X2) -> active# X1,
        active# sel(X1, X2) -> active# X2}
     Scc:
      {proper# cons(X1, X2) -> proper# X1,
       proper# cons(X1, X2) -> proper# X2,
                proper# f X -> proper# X,
                proper# g X -> proper# X,
                proper# s X -> proper# X,
        proper# sel(X1, X2) -> proper# X1,
        proper# sel(X1, X2) -> proper# X2}
     Scc:
      {s# mark X -> s# X,
         s# ok X -> s# X}
     Scc:
      {g# mark X -> g# X,
         g# ok X -> g# X}
     Scc:
      {f# mark X -> f# X,
         f# ok X -> f# 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),
                          f mark X -> mark f X,
                            f ok X -> ok f X,
                          g mark X -> mark g X,
                            g ok X -> ok g X,
               active cons(X1, X2) -> cons(active X1, X2),
                        active f X -> mark cons(X, f g X),
                        active f X -> f active X,
                        active g X -> g active X,
                      active g s X -> mark s s g X,
                      active g 0() -> mark s 0(),
                        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,
                          s mark X -> mark s X,
                            s ok X -> ok s 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 f X -> f proper X,
                        proper g X -> g proper X,
                        proper s X -> s proper X,
                        proper 0() -> ok 0(),
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open
     
     SCC (6):
      Strict:
       {active# cons(X1, X2) -> active# X1,
                 active# f X -> active# X,
                 active# g 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),
                          f mark X -> mark f X,
                            f ok X -> ok f X,
                          g mark X -> mark g X,
                            g ok X -> ok g X,
               active cons(X1, X2) -> cons(active X1, X2),
                        active f X -> mark cons(X, f g X),
                        active f X -> f active X,
                        active g X -> g active X,
                      active g s X -> mark s s g X,
                      active g 0() -> mark s 0(),
                        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,
                          s mark X -> mark s X,
                            s ok X -> ok s 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 f X -> f proper X,
                        proper g X -> g proper X,
                        proper s X -> s proper X,
                        proper 0() -> ok 0(),
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open
     
     
     
     
     
     
     
     
     
     
     SCC (7):
      Strict:
       {proper# cons(X1, X2) -> proper# X1,
        proper# cons(X1, X2) -> proper# X2,
                 proper# f X -> proper# X,
                 proper# g 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),
                          f mark X -> mark f X,
                            f ok X -> ok f X,
                          g mark X -> mark g X,
                            g ok X -> ok g X,
               active cons(X1, X2) -> cons(active X1, X2),
                        active f X -> mark cons(X, f g X),
                        active f X -> f active X,
                        active g X -> g active X,
                      active g s X -> mark s s g X,
                      active g 0() -> mark s 0(),
                        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,
                          s mark X -> mark s X,
                            s ok X -> ok s 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 f X -> f proper X,
                        proper g X -> g proper X,
                        proper s X -> s proper X,
                        proper 0() -> ok 0(),
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open
     
     
     
     
     
     
     
     SCC (2):
      Strict:
       {s# mark X -> s# X,
          s# ok X -> s# X}
      Weak:
      {          cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                          f mark X -> mark f X,
                            f ok X -> ok f X,
                          g mark X -> mark g X,
                            g ok X -> ok g X,
               active cons(X1, X2) -> cons(active X1, X2),
                        active f X -> mark cons(X, f g X),
                        active f X -> f active X,
                        active g X -> g active X,
                      active g s X -> mark s s g X,
                      active g 0() -> mark s 0(),
                        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,
                          s mark X -> mark s X,
                            s ok X -> ok s 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 f X -> f proper X,
                        proper g X -> g proper X,
                        proper s X -> s proper X,
                        proper 0() -> ok 0(),
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open
     
     SCC (2):
      Strict:
       {g# mark X -> g# X,
          g# ok X -> g# X}
      Weak:
      {          cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                          f mark X -> mark f X,
                            f ok X -> ok f X,
                          g mark X -> mark g X,
                            g ok X -> ok g X,
               active cons(X1, X2) -> cons(active X1, X2),
                        active f X -> mark cons(X, f g X),
                        active f X -> f active X,
                        active g X -> g active X,
                      active g s X -> mark s s g X,
                      active g 0() -> mark s 0(),
                        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,
                          s mark X -> mark s X,
                            s ok X -> ok s 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 f X -> f proper X,
                        proper g X -> g proper X,
                        proper s X -> s proper X,
                        proper 0() -> ok 0(),
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open
     
     
     SCC (2):
      Strict:
       {f# mark X -> f# X,
          f# ok X -> f# X}
      Weak:
      {          cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                          f mark X -> mark f X,
                            f ok X -> ok f X,
                          g mark X -> mark g X,
                            g ok X -> ok g X,
               active cons(X1, X2) -> cons(active X1, X2),
                        active f X -> mark cons(X, f g X),
                        active f X -> f active X,
                        active g X -> g active X,
                      active g s X -> mark s s g X,
                      active g 0() -> mark s 0(),
                        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,
                          s mark X -> mark s X,
                            s ok X -> ok s 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 f X -> f proper X,
                        proper g X -> g proper X,
                        proper s X -> s proper X,
                        proper 0() -> ok 0(),
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open
     SCC (3):
      Strict:
       { sel#(X1, mark X2) -> sel#(X1, X2),
         sel#(mark X1, X2) -> sel#(X1, X2),
        sel#(ok X1, ok X2) -> sel#(X1, X2)}
      Weak:
      {          cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                          f mark X -> mark f X,
                            f ok X -> ok f X,
                          g mark X -> mark g X,
                            g ok X -> ok g X,
               active cons(X1, X2) -> cons(active X1, X2),
                        active f X -> mark cons(X, f g X),
                        active f X -> f active X,
                        active g X -> g active X,
                      active g s X -> mark s s g X,
                      active g 0() -> mark s 0(),
                        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,
                          s mark X -> mark s X,
                            s ok X -> ok s 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 f X -> f proper X,
                        proper g X -> g proper X,
                        proper s X -> s proper X,
                        proper 0() -> ok 0(),
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open
     SCC (2):
      Strict:
       { cons#(mark X1, X2) -> cons#(X1, X2),
        cons#(ok X1, ok X2) -> cons#(X1, X2)}
      Weak:
      {          cons(mark X1, X2) -> mark cons(X1, X2),
                cons(ok X1, ok X2) -> ok cons(X1, X2),
                          f mark X -> mark f X,
                            f ok X -> ok f X,
                          g mark X -> mark g X,
                            g ok X -> ok g X,
               active cons(X1, X2) -> cons(active X1, X2),
                        active f X -> mark cons(X, f g X),
                        active f X -> f active X,
                        active g X -> g active X,
                      active g s X -> mark s s g X,
                      active g 0() -> mark s 0(),
                        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,
                          s mark X -> mark s X,
                            s ok X -> ok s 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 f X -> f proper X,
                        proper g X -> g proper X,
                        proper s X -> s proper X,
                        proper 0() -> ok 0(),
                proper sel(X1, X2) -> sel(proper X1, proper X2),
                        top mark X -> top proper X,
                          top ok X -> top active X}
      Open