MAYBE
Time: 9.752394
TRS:
 {                   active 2nd X -> 2nd active X,
  active 2nd cons1(X, cons(Y, Z)) -> mark Y,
           active 2nd cons(X, X1) -> mark 2nd cons1(X, X1),
             active cons1(X1, X2) -> cons1(X1, active X2),
             active cons1(X1, X2) -> cons1(active X1, X2),
              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,
                       2nd mark X -> mark 2nd X,
                         2nd ok X -> ok 2nd X,
               cons1(X1, mark X2) -> mark cons1(X1, X2),
               cons1(mark X1, X2) -> mark cons1(X1, X2),
              cons1(ok X1, ok X2) -> ok cons1(X1, X2),
                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,
                     proper 2nd X -> 2nd proper X,
             proper cons1(X1, X2) -> cons1(proper X1, proper X2),
              proper cons(X1, X2) -> cons(proper X1, proper X2),
                    proper from X -> from proper X,
                       proper s X -> s proper X,
                       top mark X -> top proper X,
                         top ok X -> top active X}
 DP:
  DP:
   {          active# 2nd X -> active# X,
              active# 2nd X -> 2nd# active X,
    active# 2nd cons(X, X1) -> 2nd# cons1(X, X1),
    active# 2nd cons(X, X1) -> cons1#(X, X1),
      active# cons1(X1, X2) -> active# X1,
      active# cons1(X1, X2) -> active# X2,
      active# cons1(X1, X2) -> cons1#(X1, active X2),
      active# cons1(X1, X2) -> cons1#(active X1, X2),
       active# cons(X1, X2) -> active# X1,
       active# cons(X1, X2) -> cons#(active X1, X2),
             active# from X -> active# X,
             active# from X -> cons#(X, from s X),
             active# from X -> from# active X,
             active# from X -> from# s X,
             active# from X -> s# X,
                active# s X -> active# X,
                active# s X -> s# active X,
                2nd# mark X -> 2nd# X,
                  2nd# ok X -> 2nd# X,
        cons1#(X1, mark X2) -> cons1#(X1, X2),
        cons1#(mark X1, X2) -> cons1#(X1, X2),
       cons1#(ok X1, ok X2) -> cons1#(X1, X2),
         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,
              proper# 2nd X -> 2nd# proper X,
              proper# 2nd X -> proper# X,
      proper# cons1(X1, X2) -> cons1#(proper X1, proper X2),
      proper# cons1(X1, X2) -> proper# X1,
      proper# cons1(X1, X2) -> proper# 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,
                top# mark X -> proper# X,
                top# mark X -> top# proper X,
                  top# ok X -> active# X,
                  top# ok X -> top# active X}
  TRS:
  {                   active 2nd X -> 2nd active X,
   active 2nd cons1(X, cons(Y, Z)) -> mark Y,
            active 2nd cons(X, X1) -> mark 2nd cons1(X, X1),
              active cons1(X1, X2) -> cons1(X1, active X2),
              active cons1(X1, X2) -> cons1(active X1, X2),
               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,
                        2nd mark X -> mark 2nd X,
                          2nd ok X -> ok 2nd X,
                cons1(X1, mark X2) -> mark cons1(X1, X2),
                cons1(mark X1, X2) -> mark cons1(X1, X2),
               cons1(ok X1, ok X2) -> ok cons1(X1, X2),
                 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,
                      proper 2nd X -> 2nd proper X,
              proper cons1(X1, X2) -> cons1(proper X1, proper X2),
               proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper from X -> from proper X,
                        proper s X -> s proper X,
                        top mark X -> top proper X,
                          top ok X -> top active X}
  EDG:
   {
    (active# from X -> active# X, active# s X -> s# active X)
    (active# from X -> active# X, active# s X -> active# X)
    (active# from X -> active# X, active# from X -> s# X)
    (active# from X -> active# X, active# from X -> from# s X)
    (active# from X -> active# X, active# from X -> from# active X)
    (active# from X -> active# X, active# from X -> cons#(X, from s X))
    (active# from X -> active# X, active# from X -> active# X)
    (active# from X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# from X -> active# X, active# cons(X1, X2) -> active# X1)
    (active# from X -> active# X, active# cons1(X1, X2) -> cons1#(active X1, X2))
    (active# from X -> active# X, active# cons1(X1, X2) -> cons1#(X1, active X2))
    (active# from X -> active# X, active# cons1(X1, X2) -> active# X2)
    (active# from X -> active# X, active# cons1(X1, X2) -> active# X1)
    (active# from X -> active# X, active# 2nd cons(X, X1) -> cons1#(X, X1))
    (active# from X -> active# X, active# 2nd cons(X, X1) -> 2nd# cons1(X, X1))
    (active# from X -> active# X, active# 2nd X -> 2nd# active X)
    (active# from X -> active# X, active# 2nd 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# from X -> 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 -> cons#(X, from s X))
    (active# s X -> active# X, active# from X -> active# 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# cons1(X1, X2) -> cons1#(active X1, X2))
    (active# s X -> active# X, active# cons1(X1, X2) -> cons1#(X1, active X2))
    (active# s X -> active# X, active# cons1(X1, X2) -> active# X2)
    (active# s X -> active# X, active# cons1(X1, X2) -> active# X1)
    (active# s X -> active# X, active# 2nd cons(X, X1) -> cons1#(X, X1))
    (active# s X -> active# X, active# 2nd cons(X, X1) -> 2nd# cons1(X, X1))
    (active# s X -> active# X, active# 2nd X -> 2nd# active X)
    (active# s X -> active# X, active# 2nd X -> active# X)
    (2nd# ok X -> 2nd# X, 2nd# ok X -> 2nd# X)
    (2nd# ok X -> 2nd# X, 2nd# mark X -> 2nd# X)
    (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)
    (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))
    (proper# from X -> proper# X, proper# cons1(X1, X2) -> proper# X2)
    (proper# from X -> proper# X, proper# cons1(X1, X2) -> proper# X1)
    (proper# from X -> proper# X, proper# cons1(X1, X2) -> cons1#(proper X1, proper X2))
    (proper# from X -> proper# X, proper# 2nd X -> proper# X)
    (proper# from X -> proper# X, proper# 2nd X -> 2nd# proper X)
    (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))
    (top# mark X -> proper# X, proper# cons1(X1, X2) -> proper# X2)
    (top# mark X -> proper# X, proper# cons1(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# cons1(X1, X2) -> cons1#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# 2nd X -> proper# X)
    (top# mark X -> proper# X, proper# 2nd X -> 2nd# proper X)
    (active# cons1(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# cons1(X1, X2) -> active# X1, active# s X -> active# X)
    (active# cons1(X1, X2) -> active# X1, active# from X -> s# X)
    (active# cons1(X1, X2) -> active# X1, active# from X -> from# s X)
    (active# cons1(X1, X2) -> active# X1, active# from X -> from# active X)
    (active# cons1(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
    (active# cons1(X1, X2) -> active# X1, active# from X -> active# X)
    (active# cons1(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# cons1(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
    (active# cons1(X1, X2) -> active# X1, active# cons1(X1, X2) -> cons1#(active X1, X2))
    (active# cons1(X1, X2) -> active# X1, active# cons1(X1, X2) -> cons1#(X1, active X2))
    (active# cons1(X1, X2) -> active# X1, active# cons1(X1, X2) -> active# X2)
    (active# cons1(X1, X2) -> active# X1, active# cons1(X1, X2) -> active# X1)
    (active# cons1(X1, X2) -> active# X1, active# 2nd cons(X, X1) -> cons1#(X, X1))
    (active# cons1(X1, X2) -> active# X1, active# 2nd cons(X, X1) -> 2nd# cons1(X, X1))
    (active# cons1(X1, X2) -> active# X1, active# 2nd X -> 2nd# active X)
    (active# cons1(X1, X2) -> active# X1, active# 2nd X -> active# X)
    (proper# cons1(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# cons1(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# cons1(X1, X2) -> proper# X1, proper# from X -> proper# X)
    (proper# cons1(X1, X2) -> proper# X1, proper# from X -> from# proper X)
    (proper# cons1(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
    (proper# cons1(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
    (proper# cons1(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# cons1(X1, X2) -> proper# X1, proper# cons1(X1, X2) -> proper# X2)
    (proper# cons1(X1, X2) -> proper# X1, proper# cons1(X1, X2) -> proper# X1)
    (proper# cons1(X1, X2) -> proper# X1, proper# cons1(X1, X2) -> cons1#(proper X1, proper X2))
    (proper# cons1(X1, X2) -> proper# X1, proper# 2nd X -> proper# X)
    (proper# cons1(X1, X2) -> proper# X1, proper# 2nd X -> 2nd# proper X)
    (active# cons1(X1, X2) -> active# X2, active# s X -> s# active X)
    (active# cons1(X1, X2) -> active# X2, active# s X -> active# X)
    (active# cons1(X1, X2) -> active# X2, active# from X -> s# X)
    (active# cons1(X1, X2) -> active# X2, active# from X -> from# s X)
    (active# cons1(X1, X2) -> active# X2, active# from X -> from# active X)
    (active# cons1(X1, X2) -> active# X2, active# from X -> cons#(X, from s X))
    (active# cons1(X1, X2) -> active# X2, active# from X -> active# X)
    (active# cons1(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# cons1(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
    (active# cons1(X1, X2) -> active# X2, active# cons1(X1, X2) -> cons1#(active X1, X2))
    (active# cons1(X1, X2) -> active# X2, active# cons1(X1, X2) -> cons1#(X1, active X2))
    (active# cons1(X1, X2) -> active# X2, active# cons1(X1, X2) -> active# X2)
    (active# cons1(X1, X2) -> active# X2, active# cons1(X1, X2) -> active# X1)
    (active# cons1(X1, X2) -> active# X2, active# 2nd cons(X, X1) -> cons1#(X, X1))
    (active# cons1(X1, X2) -> active# X2, active# 2nd cons(X, X1) -> 2nd# cons1(X, X1))
    (active# cons1(X1, X2) -> active# X2, active# 2nd X -> 2nd# active X)
    (active# cons1(X1, X2) -> active# X2, active# 2nd X -> active# X)
    (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# from X -> proper# X)
    (proper# cons(X1, X2) -> proper# X2, proper# from X -> from# 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))
    (proper# cons(X1, X2) -> proper# X2, proper# cons1(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X2, proper# cons1(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X2, proper# cons1(X1, X2) -> cons1#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X2, proper# 2nd X -> proper# X)
    (proper# cons(X1, X2) -> proper# X2, proper# 2nd X -> 2nd# proper X)
    (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))
    (cons1#(X1, mark X2) -> cons1#(X1, X2), cons1#(ok X1, ok X2) -> cons1#(X1, X2))
    (cons1#(X1, mark X2) -> cons1#(X1, X2), cons1#(mark X1, X2) -> cons1#(X1, X2))
    (cons1#(X1, mark X2) -> cons1#(X1, X2), cons1#(X1, mark X2) -> cons1#(X1, X2))
    (cons1#(ok X1, ok X2) -> cons1#(X1, X2), cons1#(ok X1, ok X2) -> cons1#(X1, X2))
    (cons1#(ok X1, ok X2) -> cons1#(X1, X2), cons1#(mark X1, X2) -> cons1#(X1, X2))
    (cons1#(ok X1, ok X2) -> cons1#(X1, X2), cons1#(X1, mark X2) -> cons1#(X1, X2))
    (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))
    (active# cons1(X1, X2) -> cons1#(X1, active X2), cons1#(ok X1, ok X2) -> cons1#(X1, X2))
    (active# cons1(X1, X2) -> cons1#(X1, active X2), cons1#(mark X1, X2) -> cons1#(X1, X2))
    (active# cons1(X1, X2) -> cons1#(X1, active X2), cons1#(X1, mark X2) -> cons1#(X1, X2))
    (active# 2nd X -> 2nd# active X, 2nd# ok X -> 2nd# X)
    (active# 2nd X -> 2nd# active X, 2nd# mark X -> 2nd# X)
    (active# from X -> from# s X, from# ok X -> from# X)
    (active# from X -> from# s X, from# mark X -> from# 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)
    (active# s X -> s# active X, s# mark X -> s# X)
    (active# s X -> s# active X, s# ok X -> s# X)
    (active# from X -> from# active X, from# mark X -> from# X)
    (active# from X -> from# active X, from# ok X -> from# X)
    (active# 2nd cons(X, X1) -> 2nd# cons1(X, X1), 2nd# mark X -> 2nd# X)
    (active# 2nd cons(X, X1) -> 2nd# cons1(X, X1), 2nd# ok X -> 2nd# X)
    (active# 2nd cons(X, X1) -> cons1#(X, X1), cons1#(X1, mark X2) -> cons1#(X1, X2))
    (active# 2nd cons(X, X1) -> cons1#(X, X1), cons1#(mark X1, X2) -> cons1#(X1, X2))
    (active# 2nd cons(X, X1) -> cons1#(X, X1), cons1#(ok X1, ok X2) -> cons1#(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))
    (cons1#(mark X1, X2) -> cons1#(X1, X2), cons1#(X1, mark X2) -> cons1#(X1, X2))
    (cons1#(mark X1, X2) -> cons1#(X1, X2), cons1#(mark X1, X2) -> cons1#(X1, X2))
    (cons1#(mark X1, X2) -> cons1#(X1, X2), cons1#(ok X1, ok X2) -> cons1#(X1, X2))
    (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2))
    (active# from X -> cons#(X, from s X), cons#(ok X1, ok X2) -> cons#(X1, X2))
    (active# cons1(X1, X2) -> cons1#(active X1, X2), cons1#(X1, mark X2) -> cons1#(X1, X2))
    (active# cons1(X1, X2) -> cons1#(active X1, X2), cons1#(mark X1, X2) -> cons1#(X1, X2))
    (active# cons1(X1, X2) -> cons1#(active X1, X2), cons1#(ok X1, ok X2) -> cons1#(X1, X2))
    (proper# cons1(X1, X2) -> proper# X2, proper# 2nd X -> 2nd# proper X)
    (proper# cons1(X1, X2) -> proper# X2, proper# 2nd X -> proper# X)
    (proper# cons1(X1, X2) -> proper# X2, proper# cons1(X1, X2) -> cons1#(proper X1, proper X2))
    (proper# cons1(X1, X2) -> proper# X2, proper# cons1(X1, X2) -> proper# X1)
    (proper# cons1(X1, X2) -> proper# X2, proper# cons1(X1, X2) -> proper# X2)
    (proper# cons1(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# cons1(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
    (proper# cons1(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
    (proper# cons1(X1, X2) -> proper# X2, proper# from X -> from# proper X)
    (proper# cons1(X1, X2) -> proper# X2, proper# from X -> proper# X)
    (proper# cons1(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# cons1(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# cons(X1, X2) -> proper# X1, proper# 2nd X -> 2nd# proper X)
    (proper# cons(X1, X2) -> proper# X1, proper# 2nd X -> proper# X)
    (proper# cons(X1, X2) -> proper# X1, proper# cons1(X1, X2) -> cons1#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X1, proper# cons1(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X1, proper# cons1(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X1, proper# from X -> from# proper X)
    (proper# cons(X1, X2) -> proper# X1, proper# from X -> proper# X)
    (proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (active# cons(X1, X2) -> active# X1, active# 2nd X -> active# X)
    (active# cons(X1, X2) -> active# X1, active# 2nd X -> 2nd# active X)
    (active# cons(X1, X2) -> active# X1, active# 2nd cons(X, X1) -> 2nd# cons1(X, X1))
    (active# cons(X1, X2) -> active# X1, active# 2nd cons(X, X1) -> cons1#(X, X1))
    (active# cons(X1, X2) -> active# X1, active# cons1(X1, X2) -> active# X1)
    (active# cons(X1, X2) -> active# X1, active# cons1(X1, X2) -> active# X2)
    (active# cons(X1, X2) -> active# X1, active# cons1(X1, X2) -> cons1#(X1, active X2))
    (active# cons(X1, X2) -> active# X1, active# cons1(X1, X2) -> cons1#(active X1, X2))
    (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))
    (active# cons(X1, X2) -> active# X1, active# from X -> active# X)
    (active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from 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 -> s# X)
    (active# cons(X1, X2) -> active# X1, active# s X -> active# X)
    (active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
    (top# ok X -> active# X, active# 2nd X -> active# X)
    (top# ok X -> active# X, active# 2nd X -> 2nd# active X)
    (top# ok X -> active# X, active# 2nd cons(X, X1) -> 2nd# cons1(X, X1))
    (top# ok X -> active# X, active# 2nd cons(X, X1) -> cons1#(X, X1))
    (top# ok X -> active# X, active# cons1(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# cons1(X1, X2) -> active# X2)
    (top# ok X -> active# X, active# cons1(X1, X2) -> cons1#(X1, active X2))
    (top# ok X -> active# X, active# cons1(X1, X2) -> cons1#(active X1, X2))
    (top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (top# ok X -> active# X, active# from X -> active# X)
    (top# ok X -> active# X, active# from X -> cons#(X, from s X))
    (top# ok X -> active# X, active# from X -> from# active X)
    (top# ok X -> active# X, active# from X -> from# s X)
    (top# ok X -> active# X, active# from X -> s# X)
    (top# ok X -> active# X, active# s X -> active# X)
    (top# ok X -> active# X, active# s X -> s# active X)
    (proper# s X -> proper# X, proper# 2nd X -> 2nd# proper X)
    (proper# s X -> proper# X, proper# 2nd X -> proper# X)
    (proper# s X -> proper# X, proper# cons1(X1, X2) -> cons1#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# cons1(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# cons1(X1, X2) -> proper# X2)
    (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# 2nd X -> proper# X, proper# 2nd X -> 2nd# proper X)
    (proper# 2nd X -> proper# X, proper# 2nd X -> proper# X)
    (proper# 2nd X -> proper# X, proper# cons1(X1, X2) -> cons1#(proper X1, proper X2))
    (proper# 2nd X -> proper# X, proper# cons1(X1, X2) -> proper# X1)
    (proper# 2nd X -> proper# X, proper# cons1(X1, X2) -> proper# X2)
    (proper# 2nd X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# 2nd X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# 2nd X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# 2nd X -> proper# X, proper# from X -> from# proper X)
    (proper# 2nd X -> proper# X, proper# from X -> proper# X)
    (proper# 2nd X -> proper# X, proper# s X -> s# proper X)
    (proper# 2nd X -> proper# X, proper# s X -> proper# 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)
    (2nd# mark X -> 2nd# X, 2nd# mark X -> 2nd# X)
    (2nd# mark X -> 2nd# X, 2nd# ok X -> 2nd# X)
    (active# from X -> s# X, s# mark X -> s# X)
    (active# from X -> s# X, s# ok X -> s# X)
    (active# 2nd X -> active# X, active# 2nd X -> active# X)
    (active# 2nd X -> active# X, active# 2nd X -> 2nd# active X)
    (active# 2nd X -> active# X, active# 2nd cons(X, X1) -> 2nd# cons1(X, X1))
    (active# 2nd X -> active# X, active# 2nd cons(X, X1) -> cons1#(X, X1))
    (active# 2nd X -> active# X, active# cons1(X1, X2) -> active# X1)
    (active# 2nd X -> active# X, active# cons1(X1, X2) -> active# X2)
    (active# 2nd X -> active# X, active# cons1(X1, X2) -> cons1#(X1, active X2))
    (active# 2nd X -> active# X, active# cons1(X1, X2) -> cons1#(active X1, X2))
    (active# 2nd X -> active# X, active# cons(X1, X2) -> active# X1)
    (active# 2nd X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# 2nd X -> active# X, active# from X -> active# X)
    (active# 2nd X -> active# X, active# from X -> cons#(X, from s X))
    (active# 2nd X -> active# X, active# from X -> from# active X)
    (active# 2nd X -> active# X, active# from X -> from# s X)
    (active# 2nd X -> active# X, active# from X -> s# X)
    (active# 2nd X -> active# X, active# s X -> active# X)
    (active# 2nd X -> active# X, active# s X -> s# active X)
   }
   STATUS:
    arrows: 0.861054
    SCCS (8):
     Scc:
      {top# ok X -> top# active X}
     Scc:
      {        proper# 2nd X -> proper# X,
       proper# cons1(X1, X2) -> proper# X1,
       proper# cons1(X1, X2) -> proper# X2,
        proper# cons(X1, X2) -> proper# X1,
        proper# cons(X1, X2) -> proper# X2,
              proper# from X -> proper# X,
                 proper# s X -> proper# X}
     Scc:
      {        active# 2nd X -> active# X,
       active# cons1(X1, X2) -> active# X1,
       active# cons1(X1, X2) -> active# X2,
        active# cons(X1, X2) -> active# X1,
              active# from X -> active# X,
                 active# s X -> active# X}
     Scc:
      {s# mark X -> s# X,
         s# ok X -> s# X}
     Scc:
      {from# mark X -> from# X,
         from# ok X -> from# X}
     Scc:
      { cons#(mark X1, X2) -> cons#(X1, X2),
       cons#(ok X1, ok X2) -> cons#(X1, X2)}
     Scc:
      { cons1#(X1, mark X2) -> cons1#(X1, X2),
        cons1#(mark X1, X2) -> cons1#(X1, X2),
       cons1#(ok X1, ok X2) -> cons1#(X1, X2)}
     Scc:
      {2nd# mark X -> 2nd# X,
         2nd# ok X -> 2nd# X}
     
     SCC (1):
      Strict:
       {top# ok X -> top# active X}
      Weak:
      {                   active 2nd X -> 2nd active X,
       active 2nd cons1(X, cons(Y, Z)) -> mark Y,
                active 2nd cons(X, X1) -> mark 2nd cons1(X, X1),
                  active cons1(X1, X2) -> cons1(X1, active X2),
                  active cons1(X1, X2) -> cons1(active X1, X2),
                   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,
                            2nd mark X -> mark 2nd X,
                              2nd ok X -> ok 2nd X,
                    cons1(X1, mark X2) -> mark cons1(X1, X2),
                    cons1(mark X1, X2) -> mark cons1(X1, X2),
                   cons1(ok X1, ok X2) -> ok cons1(X1, X2),
                     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,
                          proper 2nd X -> 2nd proper X,
                  proper cons1(X1, X2) -> cons1(proper X1, proper X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                            top mark X -> top proper X,
                              top ok X -> top active X}
      Open
     
     
     
     SCC (7):
      Strict:
       {        proper# 2nd X -> proper# X,
        proper# cons1(X1, X2) -> proper# X1,
        proper# cons1(X1, X2) -> proper# X2,
         proper# cons(X1, X2) -> proper# X1,
         proper# cons(X1, X2) -> proper# X2,
               proper# from X -> proper# X,
                  proper# s X -> proper# X}
      Weak:
      {                   active 2nd X -> 2nd active X,
       active 2nd cons1(X, cons(Y, Z)) -> mark Y,
                active 2nd cons(X, X1) -> mark 2nd cons1(X, X1),
                  active cons1(X1, X2) -> cons1(X1, active X2),
                  active cons1(X1, X2) -> cons1(active X1, X2),
                   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,
                            2nd mark X -> mark 2nd X,
                              2nd ok X -> ok 2nd X,
                    cons1(X1, mark X2) -> mark cons1(X1, X2),
                    cons1(mark X1, X2) -> mark cons1(X1, X2),
                   cons1(ok X1, ok X2) -> ok cons1(X1, X2),
                     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,
                          proper 2nd X -> 2nd proper X,
                  proper cons1(X1, X2) -> cons1(proper X1, proper X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                            top mark X -> top proper X,
                              top ok X -> top active X}
      Open
     
     
     
     
     
     SCC (6):
      Strict:
       {        active# 2nd X -> active# X,
        active# cons1(X1, X2) -> active# X1,
        active# cons1(X1, X2) -> active# X2,
         active# cons(X1, X2) -> active# X1,
               active# from X -> active# X,
                  active# s X -> active# X}
      Weak:
      {                   active 2nd X -> 2nd active X,
       active 2nd cons1(X, cons(Y, Z)) -> mark Y,
                active 2nd cons(X, X1) -> mark 2nd cons1(X, X1),
                  active cons1(X1, X2) -> cons1(X1, active X2),
                  active cons1(X1, X2) -> cons1(active X1, X2),
                   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,
                            2nd mark X -> mark 2nd X,
                              2nd ok X -> ok 2nd X,
                    cons1(X1, mark X2) -> mark cons1(X1, X2),
                    cons1(mark X1, X2) -> mark cons1(X1, X2),
                   cons1(ok X1, ok X2) -> ok cons1(X1, X2),
                     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,
                          proper 2nd X -> 2nd proper X,
                  proper cons1(X1, X2) -> cons1(proper X1, proper X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                            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:
      {                   active 2nd X -> 2nd active X,
       active 2nd cons1(X, cons(Y, Z)) -> mark Y,
                active 2nd cons(X, X1) -> mark 2nd cons1(X, X1),
                  active cons1(X1, X2) -> cons1(X1, active X2),
                  active cons1(X1, X2) -> cons1(active X1, X2),
                   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,
                            2nd mark X -> mark 2nd X,
                              2nd ok X -> ok 2nd X,
                    cons1(X1, mark X2) -> mark cons1(X1, X2),
                    cons1(mark X1, X2) -> mark cons1(X1, X2),
                   cons1(ok X1, ok X2) -> ok cons1(X1, X2),
                     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,
                          proper 2nd X -> 2nd proper X,
                  proper cons1(X1, X2) -> cons1(proper X1, proper X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                            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:
      {                   active 2nd X -> 2nd active X,
       active 2nd cons1(X, cons(Y, Z)) -> mark Y,
                active 2nd cons(X, X1) -> mark 2nd cons1(X, X1),
                  active cons1(X1, X2) -> cons1(X1, active X2),
                  active cons1(X1, X2) -> cons1(active X1, X2),
                   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,
                            2nd mark X -> mark 2nd X,
                              2nd ok X -> ok 2nd X,
                    cons1(X1, mark X2) -> mark cons1(X1, X2),
                    cons1(mark X1, X2) -> mark cons1(X1, X2),
                   cons1(ok X1, ok X2) -> ok cons1(X1, X2),
                     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,
                          proper 2nd X -> 2nd proper X,
                  proper cons1(X1, X2) -> cons1(proper X1, proper X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                            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:
      {                   active 2nd X -> 2nd active X,
       active 2nd cons1(X, cons(Y, Z)) -> mark Y,
                active 2nd cons(X, X1) -> mark 2nd cons1(X, X1),
                  active cons1(X1, X2) -> cons1(X1, active X2),
                  active cons1(X1, X2) -> cons1(active X1, X2),
                   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,
                            2nd mark X -> mark 2nd X,
                              2nd ok X -> ok 2nd X,
                    cons1(X1, mark X2) -> mark cons1(X1, X2),
                    cons1(mark X1, X2) -> mark cons1(X1, X2),
                   cons1(ok X1, ok X2) -> ok cons1(X1, X2),
                     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,
                          proper 2nd X -> 2nd proper X,
                  proper cons1(X1, X2) -> cons1(proper X1, proper X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                            top mark X -> top proper X,
                              top ok X -> top active X}
      Open
     
     
     
     SCC (3):
      Strict:
       { cons1#(X1, mark X2) -> cons1#(X1, X2),
         cons1#(mark X1, X2) -> cons1#(X1, X2),
        cons1#(ok X1, ok X2) -> cons1#(X1, X2)}
      Weak:
      {                   active 2nd X -> 2nd active X,
       active 2nd cons1(X, cons(Y, Z)) -> mark Y,
                active 2nd cons(X, X1) -> mark 2nd cons1(X, X1),
                  active cons1(X1, X2) -> cons1(X1, active X2),
                  active cons1(X1, X2) -> cons1(active X1, X2),
                   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,
                            2nd mark X -> mark 2nd X,
                              2nd ok X -> ok 2nd X,
                    cons1(X1, mark X2) -> mark cons1(X1, X2),
                    cons1(mark X1, X2) -> mark cons1(X1, X2),
                   cons1(ok X1, ok X2) -> ok cons1(X1, X2),
                     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,
                          proper 2nd X -> 2nd proper X,
                  proper cons1(X1, X2) -> cons1(proper X1, proper X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                            top mark X -> top proper X,
                              top ok X -> top active X}
      Open
     
     
     SCC (2):
      Strict:
       {2nd# mark X -> 2nd# X,
          2nd# ok X -> 2nd# X}
      Weak:
      {                   active 2nd X -> 2nd active X,
       active 2nd cons1(X, cons(Y, Z)) -> mark Y,
                active 2nd cons(X, X1) -> mark 2nd cons1(X, X1),
                  active cons1(X1, X2) -> cons1(X1, active X2),
                  active cons1(X1, X2) -> cons1(active X1, X2),
                   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,
                            2nd mark X -> mark 2nd X,
                              2nd ok X -> ok 2nd X,
                    cons1(X1, mark X2) -> mark cons1(X1, X2),
                    cons1(mark X1, X2) -> mark cons1(X1, X2),
                   cons1(ok X1, ok X2) -> ok cons1(X1, X2),
                     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,
                          proper 2nd X -> 2nd proper X,
                  proper cons1(X1, X2) -> cons1(proper X1, proper X2),
                   proper cons(X1, X2) -> cons(proper X1, proper X2),
                         proper from X -> from proper X,
                            proper s X -> s proper X,
                            top mark X -> top proper X,
                              top ok X -> top active X}
      Open