MAYBE
Time: 1.060241
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}
  UR:
   {          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)}
   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))
    }
    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#(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)
      (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))
      (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#(mark X1, X2) -> sel#(X1, X2))
      (active# sel(X1, X2) -> sel#(active X1, X2), sel#(ok X1, ok X2) -> sel#(X1, X2))
      (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))
      (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))
      (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.864645
      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