MAYBE
Time: 0.039699
TRS:
 {             cons(mark X1, X2) -> mark cons(X1, X2),
              cons(ok X1, ok X2) -> ok cons(X1, X2),
                     from mark X -> mark from X,
                       from ok X -> ok from X,
                        s mark X -> mark s X,
                          s ok X -> ok s X,
             active cons(X1, X2) -> cons(active X1, X2),
                   active from X -> mark cons(X, from s X),
                   active from X -> from active X,
                      active s X -> s active X,
            active after(X1, X2) -> after(X1, active X2),
            active after(X1, X2) -> after(active X1, X2),
  active after(s N, cons(X, XS)) -> mark after(N, XS),
           active after(0(), XS) -> mark XS,
              after(X1, mark X2) -> mark after(X1, X2),
              after(mark X1, X2) -> mark after(X1, X2),
             after(ok X1, ok X2) -> ok after(X1, X2),
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper from X -> from proper X,
                      proper s X -> s proper X,
            proper after(X1, X2) -> after(proper X1, proper X2),
                      proper 0() -> ok 0(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
 DP:
  DP:
   {             cons#(mark X1, X2) -> cons#(X1, X2),
                cons#(ok X1, ok X2) -> cons#(X1, X2),
                       from# mark X -> from# X,
                         from# ok X -> from# X,
                          s# mark X -> s# X,
                            s# ok X -> s# X,
               active# cons(X1, X2) -> cons#(active X1, X2),
               active# cons(X1, X2) -> active# X1,
                     active# from X -> cons#(X, from s X),
                     active# from X -> from# s X,
                     active# from X -> from# active X,
                     active# from X -> s# X,
                     active# from X -> active# X,
                        active# s X -> s# active X,
                        active# s X -> active# X,
              active# after(X1, X2) -> active# X1,
              active# after(X1, X2) -> active# X2,
              active# after(X1, X2) -> after#(X1, active X2),
              active# after(X1, X2) -> after#(active X1, X2),
    active# after(s N, cons(X, XS)) -> after#(N, XS),
                after#(X1, mark X2) -> after#(X1, X2),
                after#(mark X1, X2) -> after#(X1, X2),
               after#(ok X1, ok X2) -> after#(X1, X2),
               proper# cons(X1, X2) -> cons#(proper X1, proper X2),
               proper# cons(X1, X2) -> proper# X1,
               proper# cons(X1, X2) -> proper# X2,
                     proper# from X -> from# proper X,
                     proper# from X -> proper# X,
                        proper# s X -> s# proper X,
                        proper# s X -> proper# X,
              proper# after(X1, X2) -> after#(proper X1, proper X2),
              proper# after(X1, X2) -> proper# X1,
              proper# after(X1, X2) -> proper# X2,
                        top# mark X -> proper# X,
                        top# mark X -> top# proper X,
                          top# ok X -> active# X,
                          top# ok X -> top# active X}
  TRS:
  {             cons(mark X1, X2) -> mark cons(X1, X2),
               cons(ok X1, ok X2) -> ok cons(X1, X2),
                      from mark X -> mark from X,
                        from ok X -> ok from X,
                         s mark X -> mark s X,
                           s ok X -> ok s X,
              active cons(X1, X2) -> cons(active X1, X2),
                    active from X -> mark cons(X, from s X),
                    active from X -> from active X,
                       active s X -> s active X,
             active after(X1, X2) -> after(X1, active X2),
             active after(X1, X2) -> after(active X1, X2),
   active after(s N, cons(X, XS)) -> mark after(N, XS),
            active after(0(), XS) -> mark XS,
               after(X1, mark X2) -> mark after(X1, X2),
               after(mark X1, X2) -> mark after(X1, X2),
              after(ok X1, ok X2) -> ok after(X1, X2),
              proper cons(X1, X2) -> cons(proper X1, proper X2),
                    proper from X -> from proper X,
                       proper s X -> s proper X,
             proper after(X1, X2) -> after(proper X1, proper X2),
                       proper 0() -> ok 0(),
                       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),
                       from mark X -> mark from X,
                         from ok X -> ok from X,
                          s mark X -> mark s X,
                            s ok X -> ok s X,
               active cons(X1, X2) -> cons(active X1, X2),
                     active from X -> mark cons(X, from s X),
                     active from X -> from active X,
                        active s X -> s active X,
              active after(X1, X2) -> after(X1, active X2),
              active after(X1, X2) -> after(active X1, X2),
    active after(s N, cons(X, XS)) -> mark after(N, XS),
             active after(0(), XS) -> mark XS,
                after(X1, mark X2) -> mark after(X1, X2),
                after(mark X1, X2) -> mark after(X1, X2),
               after(ok X1, ok X2) -> ok after(X1, X2),
               proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper from X -> from proper X,
                        proper s X -> s proper X,
              proper after(X1, X2) -> after(proper X1, proper X2),
                        proper 0() -> ok 0(),
                           a(x, y) -> x,
                           a(x, y) -> y}
   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))
     (after#(mark X1, X2) -> after#(X1, X2), after#(ok X1, ok X2) -> after#(X1, X2))
     (after#(mark X1, X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
     (after#(mark X1, X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
     (active# cons(X1, X2) -> active# X1, active# after(s N, cons(X, XS)) -> after#(N, XS))
     (active# cons(X1, X2) -> active# X1, active# after(X1, X2) -> after#(active X1, X2))
     (active# cons(X1, X2) -> active# X1, active# after(X1, X2) -> after#(X1, active X2))
     (active# cons(X1, X2) -> active# X1, active# after(X1, X2) -> active# X2)
     (active# cons(X1, X2) -> active# X1, active# after(X1, X2) -> active# X1)
     (active# cons(X1, X2) -> active# X1, active# s X -> active# X)
     (active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# cons(X1, X2) -> active# X1, active# from X -> active# X)
     (active# cons(X1, X2) -> active# X1, active# from X -> s# X)
     (active# cons(X1, X2) -> active# X1, active# from X -> from# active X)
     (active# cons(X1, X2) -> active# X1, active# from X -> from# s X)
     (active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
     (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
     (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
     (proper# cons(X1, X2) -> proper# X1, proper# after(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# after(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# after(X1, X2) -> after#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# from X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# from X -> from# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (active# from X -> from# s X, from# ok X -> from# X)
     (active# from X -> from# s X, from# mark X -> from# X)
     (active# s X -> s# active X, s# ok X -> s# X)
     (active# s X -> s# active X, s# mark X -> s# X)
     (proper# s X -> s# proper X, s# ok X -> s# X)
     (proper# s X -> s# proper X, s# mark X -> s# X)
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# from X -> cons#(X, from s X), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
     (from# ok X -> from# X, from# ok X -> from# X)
     (from# ok X -> from# X, from# mark X -> from# X)
     (s# ok X -> s# X, s# ok X -> s# X)
     (s# ok X -> s# X, s# mark X -> s# X)
     (active# from X -> active# X, active# after(s N, cons(X, XS)) -> after#(N, XS))
     (active# from X -> active# X, active# after(X1, X2) -> after#(active X1, X2))
     (active# from X -> active# X, active# after(X1, X2) -> after#(X1, active X2))
     (active# from X -> active# X, active# after(X1, X2) -> active# X2)
     (active# from X -> active# X, active# after(X1, X2) -> active# X1)
     (active# from X -> active# X, active# s X -> active# X)
     (active# from X -> active# X, active# s X -> s# active X)
     (active# from X -> active# X, active# from X -> active# X)
     (active# from X -> active# X, active# from X -> s# X)
     (active# from X -> active# X, active# from X -> from# active X)
     (active# from X -> active# X, active# from X -> from# s X)
     (active# from X -> active# X, active# from X -> cons#(X, from s X))
     (active# from X -> active# X, active# cons(X1, X2) -> active# X1)
     (active# from X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (proper# from X -> proper# X, proper# after(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# after(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# after(X1, X2) -> after#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# s X -> proper# X)
     (proper# from X -> proper# X, proper# s X -> s# proper X)
     (proper# from X -> proper# X, proper# from X -> proper# X)
     (proper# from X -> proper# X, proper# from X -> from# proper X)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# after(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# after(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# after(X1, X2) -> after#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# s X -> proper# X)
     (top# mark X -> proper# X, proper# s X -> s# proper X)
     (top# mark X -> proper# X, proper# from X -> proper# X)
     (top# mark X -> proper# X, proper# from X -> from# proper X)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (active# after(X1, X2) -> active# X2, active# after(s N, cons(X, XS)) -> after#(N, XS))
     (active# after(X1, X2) -> active# X2, active# after(X1, X2) -> after#(active X1, X2))
     (active# after(X1, X2) -> active# X2, active# after(X1, X2) -> after#(X1, active X2))
     (active# after(X1, X2) -> active# X2, active# after(X1, X2) -> active# X2)
     (active# after(X1, X2) -> active# X2, active# after(X1, X2) -> active# X1)
     (active# after(X1, X2) -> active# X2, active# s X -> active# X)
     (active# after(X1, X2) -> active# X2, active# s X -> s# active X)
     (active# after(X1, X2) -> active# X2, active# from X -> active# X)
     (active# after(X1, X2) -> active# X2, active# from X -> s# X)
     (active# after(X1, X2) -> active# X2, active# from X -> from# active X)
     (active# after(X1, X2) -> active# X2, active# from X -> from# s X)
     (active# after(X1, X2) -> active# X2, active# from X -> cons#(X, from s X))
     (active# after(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
     (active# after(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
     (proper# after(X1, X2) -> proper# X2, proper# after(X1, X2) -> proper# X2)
     (proper# after(X1, X2) -> proper# X2, proper# after(X1, X2) -> proper# X1)
     (proper# after(X1, X2) -> proper# X2, proper# after(X1, X2) -> after#(proper X1, proper X2))
     (proper# after(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# after(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# after(X1, X2) -> proper# X2, proper# from X -> proper# X)
     (proper# after(X1, X2) -> proper# X2, proper# from X -> from# proper X)
     (proper# after(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# after(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# after(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper 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# after(X1, X2) -> after#(active X1, X2), after#(X1, mark X2) -> after#(X1, X2))
     (active# after(X1, X2) -> after#(active X1, X2), after#(mark X1, X2) -> after#(X1, X2))
     (active# after(X1, X2) -> after#(active X1, X2), after#(ok X1, ok X2) -> after#(X1, X2))
     (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(X1, mark X2) -> after#(X1, X2))
     (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(mark X1, X2) -> after#(X1, X2))
     (active# after(s N, cons(X, XS)) -> after#(N, XS), after#(ok X1, ok X2) -> after#(X1, X2))
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
     (proper# cons(X1, X2) -> proper# X2, proper# from X -> from# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# from X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# after(X1, X2) -> after#(proper X1, proper X2))
     (proper# cons(X1, X2) -> proper# X2, proper# after(X1, X2) -> proper# X1)
     (proper# cons(X1, X2) -> proper# X2, proper# after(X1, X2) -> proper# X2)
     (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# from X -> cons#(X, from s X))
     (top# ok X -> active# X, active# from X -> from# s X)
     (top# ok X -> active# X, active# from X -> from# active X)
     (top# ok X -> active# X, active# from X -> s# X)
     (top# ok X -> active# X, active# from X -> active# X)
     (top# ok X -> active# X, active# s X -> s# active X)
     (top# ok X -> active# X, active# s X -> active# X)
     (top# ok X -> active# X, active# after(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# after(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# after(X1, X2) -> after#(X1, active X2))
     (top# ok X -> active# X, active# after(X1, X2) -> after#(active X1, X2))
     (top# ok X -> active# X, active# after(s N, cons(X, XS)) -> after#(N, XS))
     (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# from X -> from# proper X)
     (proper# s X -> proper# X, proper# from X -> proper# X)
     (proper# s X -> proper# X, proper# s X -> s# proper X)
     (proper# s X -> proper# X, proper# s X -> proper# X)
     (proper# s X -> proper# X, proper# after(X1, X2) -> after#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# after(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# after(X1, X2) -> proper# X2)
     (active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# s X -> active# X, active# cons(X1, X2) -> active# X1)
     (active# s X -> active# X, active# from X -> cons#(X, from s X))
     (active# s X -> active# X, active# from X -> from# s X)
     (active# s X -> active# X, active# from X -> from# active X)
     (active# s X -> active# X, active# from X -> s# X)
     (active# s X -> active# X, active# from X -> active# X)
     (active# s X -> active# X, active# s X -> s# active X)
     (active# s X -> active# X, active# s X -> active# X)
     (active# s X -> active# X, active# after(X1, X2) -> active# X1)
     (active# s X -> active# X, active# after(X1, X2) -> active# X2)
     (active# s X -> active# X, active# after(X1, X2) -> after#(X1, active X2))
     (active# s X -> active# X, active# after(X1, X2) -> after#(active X1, X2))
     (active# s X -> active# X, active# after(s N, cons(X, XS)) -> after#(N, XS))
     (active# from X -> s# X, s# mark X -> s# X)
     (active# from X -> s# X, s# ok X -> s# X)
     (s# mark X -> s# X, s# mark X -> s# X)
     (s# mark X -> s# X, s# ok X -> s# X)
     (from# mark X -> from# X, from# mark X -> from# X)
     (from# mark X -> from# X, from# ok X -> from# X)
     (proper# after(X1, X2) -> after#(proper X1, proper X2), after#(X1, mark X2) -> after#(X1, X2))
     (proper# after(X1, X2) -> after#(proper X1, proper X2), after#(mark X1, X2) -> after#(X1, X2))
     (proper# after(X1, X2) -> after#(proper X1, proper X2), after#(ok X1, ok X2) -> after#(X1, X2))
     (active# after(X1, X2) -> after#(X1, active X2), after#(X1, mark X2) -> after#(X1, X2))
     (active# after(X1, X2) -> after#(X1, active X2), after#(mark X1, X2) -> after#(X1, X2))
     (active# after(X1, X2) -> after#(X1, active X2), after#(ok X1, ok X2) -> after#(X1, X2))
     (top# mark X -> top# proper X, top# mark X -> proper# X)
     (top# mark X -> top# proper X, top# mark X -> top# proper X)
     (top# mark X -> top# proper X, top# ok X -> active# X)
     (top# mark X -> top# proper X, top# ok X -> top# active X)
     (proper# from X -> from# proper X, from# mark X -> from# X)
     (proper# from X -> from# proper X, from# ok X -> from# X)
     (active# from X -> from# active X, from# mark X -> from# X)
     (active# from X -> from# active X, from# ok X -> from# X)
     (proper# after(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# after(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
     (proper# after(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
     (proper# after(X1, X2) -> proper# X1, proper# from X -> from# proper X)
     (proper# after(X1, X2) -> proper# X1, proper# from X -> proper# X)
     (proper# after(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# after(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# after(X1, X2) -> proper# X1, proper# after(X1, X2) -> after#(proper X1, proper X2))
     (proper# after(X1, X2) -> proper# X1, proper# after(X1, X2) -> proper# X1)
     (proper# after(X1, X2) -> proper# X1, proper# after(X1, X2) -> proper# X2)
     (active# after(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# after(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
     (active# after(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
     (active# after(X1, X2) -> active# X1, active# from X -> from# s X)
     (active# after(X1, X2) -> active# X1, active# from X -> from# active X)
     (active# after(X1, X2) -> active# X1, active# from X -> s# X)
     (active# after(X1, X2) -> active# X1, active# from X -> active# X)
     (active# after(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# after(X1, X2) -> active# X1, active# s X -> active# X)
     (active# after(X1, X2) -> active# X1, active# after(X1, X2) -> active# X1)
     (active# after(X1, X2) -> active# X1, active# after(X1, X2) -> active# X2)
     (active# after(X1, X2) -> active# X1, active# after(X1, X2) -> after#(X1, active X2))
     (active# after(X1, X2) -> active# X1, active# after(X1, X2) -> after#(active X1, X2))
     (active# after(X1, X2) -> active# X1, active# after(s N, cons(X, XS)) -> after#(N, XS))
     (after#(ok X1, ok X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
     (after#(ok X1, ok X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
     (after#(ok X1, ok X2) -> after#(X1, X2), after#(ok X1, ok X2) -> after#(X1, X2))
     (after#(X1, mark X2) -> after#(X1, X2), after#(X1, mark X2) -> after#(X1, X2))
     (after#(X1, mark X2) -> after#(X1, X2), after#(mark X1, X2) -> after#(X1, X2))
     (after#(X1, mark X2) -> after#(X1, X2), after#(ok X1, ok X2) -> after#(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.844412
     SCCS (7):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       { proper# cons(X1, X2) -> proper# X1,
         proper# cons(X1, X2) -> proper# X2,
               proper# from X -> proper# X,
                  proper# s X -> proper# X,
        proper# after(X1, X2) -> proper# X1,
        proper# after(X1, X2) -> proper# X2}
      Scc:
       { active# cons(X1, X2) -> active# X1,
               active# from X -> active# X,
                  active# s X -> active# X,
        active# after(X1, X2) -> active# X1,
        active# after(X1, X2) -> active# X2}
      Scc:
       {s# mark X -> s# X,
          s# ok X -> s# X}
      Scc:
       {from# mark X -> from# X,
          from# ok X -> from# X}
      Scc:
       { after#(X1, mark X2) -> after#(X1, X2),
         after#(mark X1, X2) -> after#(X1, X2),
        after#(ok X1, ok X2) -> after#(X1, X2)}
      Scc:
       { cons#(mark X1, X2) -> cons#(X1, X2),
        cons#(ok X1, ok X2) -> cons#(X1, X2)}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {             cons(mark X1, X2) -> mark cons(X1, X2),
                    cons(ok X1, ok X2) -> ok cons(X1, X2),
                           from mark X -> mark from X,
                             from ok X -> ok from X,
                              s mark X -> mark s X,
                                s ok X -> ok s X,
                   active cons(X1, X2) -> cons(active X1, X2),
                         active from X -> mark cons(X, from s X),
                         active from X -> from active X,
                            active s X -> s active X,
                  active after(X1, X2) -> after(X1, active X2),
                  active after(X1, X2) -> after(active X1, X2),
        active after(s N, cons(X, XS)) -> mark after(N, XS),
                 active after(0(), XS) -> mark XS,
                    after(X1, mark X2) -> mark after(X1, X2),
                    after(mark X1, X2) -> mark after(X1, X2),
                   after(ok X1, ok X2) -> ok after(X1, X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                  proper after(X1, X2) -> after(proper X1, proper X2),
                            proper 0() -> ok 0(),
                            top mark X -> top proper X,
                              top ok X -> top active X}
       Open
      
      
      SCC (6):
       Strict:
        { proper# cons(X1, X2) -> proper# X1,
          proper# cons(X1, X2) -> proper# X2,
                proper# from X -> proper# X,
                   proper# s X -> proper# X,
         proper# after(X1, X2) -> proper# X1,
         proper# after(X1, X2) -> proper# X2}
       Weak:
       {             cons(mark X1, X2) -> mark cons(X1, X2),
                    cons(ok X1, ok X2) -> ok cons(X1, X2),
                           from mark X -> mark from X,
                             from ok X -> ok from X,
                              s mark X -> mark s X,
                                s ok X -> ok s X,
                   active cons(X1, X2) -> cons(active X1, X2),
                         active from X -> mark cons(X, from s X),
                         active from X -> from active X,
                            active s X -> s active X,
                  active after(X1, X2) -> after(X1, active X2),
                  active after(X1, X2) -> after(active X1, X2),
        active after(s N, cons(X, XS)) -> mark after(N, XS),
                 active after(0(), XS) -> mark XS,
                    after(X1, mark X2) -> mark after(X1, X2),
                    after(mark X1, X2) -> mark after(X1, X2),
                   after(ok X1, ok X2) -> ok after(X1, X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                  proper after(X1, X2) -> after(proper X1, proper X2),
                            proper 0() -> ok 0(),
                            top mark X -> top proper X,
                              top ok X -> top active X}
       Open
      
      
      
      
      SCC (5):
       Strict:
        { active# cons(X1, X2) -> active# X1,
                active# from X -> active# X,
                   active# s X -> active# X,
         active# after(X1, X2) -> active# X1,
         active# after(X1, X2) -> active# X2}
       Weak:
       {             cons(mark X1, X2) -> mark cons(X1, X2),
                    cons(ok X1, ok X2) -> ok cons(X1, X2),
                           from mark X -> mark from X,
                             from ok X -> ok from X,
                              s mark X -> mark s X,
                                s ok X -> ok s X,
                   active cons(X1, X2) -> cons(active X1, X2),
                         active from X -> mark cons(X, from s X),
                         active from X -> from active X,
                            active s X -> s active X,
                  active after(X1, X2) -> after(X1, active X2),
                  active after(X1, X2) -> after(active X1, X2),
        active after(s N, cons(X, XS)) -> mark after(N, XS),
                 active after(0(), XS) -> mark XS,
                    after(X1, mark X2) -> mark after(X1, X2),
                    after(mark X1, X2) -> mark after(X1, X2),
                   after(ok X1, ok X2) -> ok after(X1, X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                  proper after(X1, X2) -> after(proper X1, proper X2),
                            proper 0() -> ok 0(),
                            top mark X -> top proper X,
                              top ok X -> top active X}
       Open
      
      
      
      
      
      SCC (2):
       Strict:
        {s# mark X -> s# X,
           s# ok X -> s# X}
       Weak:
       {             cons(mark X1, X2) -> mark cons(X1, X2),
                    cons(ok X1, ok X2) -> ok cons(X1, X2),
                           from mark X -> mark from X,
                             from ok X -> ok from X,
                              s mark X -> mark s X,
                                s ok X -> ok s X,
                   active cons(X1, X2) -> cons(active X1, X2),
                         active from X -> mark cons(X, from s X),
                         active from X -> from active X,
                            active s X -> s active X,
                  active after(X1, X2) -> after(X1, active X2),
                  active after(X1, X2) -> after(active X1, X2),
        active after(s N, cons(X, XS)) -> mark after(N, XS),
                 active after(0(), XS) -> mark XS,
                    after(X1, mark X2) -> mark after(X1, X2),
                    after(mark X1, X2) -> mark after(X1, X2),
                   after(ok X1, ok X2) -> ok after(X1, X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                  proper after(X1, X2) -> after(proper X1, proper X2),
                            proper 0() -> ok 0(),
                            top mark X -> top proper X,
                              top ok X -> top active X}
       Open
      
      
      SCC (2):
       Strict:
        {from# mark X -> from# X,
           from# ok X -> from# X}
       Weak:
       {             cons(mark X1, X2) -> mark cons(X1, X2),
                    cons(ok X1, ok X2) -> ok cons(X1, X2),
                           from mark X -> mark from X,
                             from ok X -> ok from X,
                              s mark X -> mark s X,
                                s ok X -> ok s X,
                   active cons(X1, X2) -> cons(active X1, X2),
                         active from X -> mark cons(X, from s X),
                         active from X -> from active X,
                            active s X -> s active X,
                  active after(X1, X2) -> after(X1, active X2),
                  active after(X1, X2) -> after(active X1, X2),
        active after(s N, cons(X, XS)) -> mark after(N, XS),
                 active after(0(), XS) -> mark XS,
                    after(X1, mark X2) -> mark after(X1, X2),
                    after(mark X1, X2) -> mark after(X1, X2),
                   after(ok X1, ok X2) -> ok after(X1, X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                  proper after(X1, X2) -> after(proper X1, proper X2),
                            proper 0() -> ok 0(),
                            top mark X -> top proper X,
                              top ok X -> top active X}
       Open
      
      
      SCC (3):
       Strict:
        { after#(X1, mark X2) -> after#(X1, X2),
          after#(mark X1, X2) -> after#(X1, X2),
         after#(ok X1, ok X2) -> after#(X1, X2)}
       Weak:
       {             cons(mark X1, X2) -> mark cons(X1, X2),
                    cons(ok X1, ok X2) -> ok cons(X1, X2),
                           from mark X -> mark from X,
                             from ok X -> ok from X,
                              s mark X -> mark s X,
                                s ok X -> ok s X,
                   active cons(X1, X2) -> cons(active X1, X2),
                         active from X -> mark cons(X, from s X),
                         active from X -> from active X,
                            active s X -> s active X,
                  active after(X1, X2) -> after(X1, active X2),
                  active after(X1, X2) -> after(active X1, X2),
        active after(s N, cons(X, XS)) -> mark after(N, XS),
                 active after(0(), XS) -> mark XS,
                    after(X1, mark X2) -> mark after(X1, X2),
                    after(mark X1, X2) -> mark after(X1, X2),
                   after(ok X1, ok X2) -> ok after(X1, X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                  proper after(X1, X2) -> after(proper X1, proper X2),
                            proper 0() -> ok 0(),
                            top mark X -> top proper X,
                              top ok X -> top active X}
       Open
      SCC (2):
       Strict:
        { cons#(mark X1, X2) -> cons#(X1, X2),
         cons#(ok X1, ok X2) -> cons#(X1, X2)}
       Weak:
       {             cons(mark X1, X2) -> mark cons(X1, X2),
                    cons(ok X1, ok X2) -> ok cons(X1, X2),
                           from mark X -> mark from X,
                             from ok X -> ok from X,
                              s mark X -> mark s X,
                                s ok X -> ok s X,
                   active cons(X1, X2) -> cons(active X1, X2),
                         active from X -> mark cons(X, from s X),
                         active from X -> from active X,
                            active s X -> s active X,
                  active after(X1, X2) -> after(X1, active X2),
                  active after(X1, X2) -> after(active X1, X2),
        active after(s N, cons(X, XS)) -> mark after(N, XS),
                 active after(0(), XS) -> mark XS,
                    after(X1, mark X2) -> mark after(X1, X2),
                    after(mark X1, X2) -> mark after(X1, X2),
                   after(ok X1, ok X2) -> ok after(X1, X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                  proper after(X1, X2) -> after(proper X1, proper X2),
                            proper 0() -> ok 0(),
                            top mark X -> top proper X,
                              top ok X -> top active X}
       Open