MAYBE
Time: 1.024409
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 length cons(X, Y) -> mark s length1 Y,
       active length nil() -> mark 0(),
          active length1 X -> mark length X,
               length ok X -> ok length X,
              length1 ok X -> ok length1 X,
       proper cons(X1, X2) -> cons(proper X1, proper X2),
             proper from X -> from proper X,
                proper s X -> s proper X,
                proper 0() -> ok 0(),
           proper length X -> length proper X,
              proper nil() -> ok nil(),
          proper length1 X -> length1 proper X,
                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# length cons(X, Y) -> s# length1 Y,
    active# length cons(X, Y) -> length1# Y,
            active# length1 X -> length# X,
                 length# ok X -> length# X,
                length1# ok X -> length1# X,
         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# length X -> length# proper X,
             proper# length X -> proper# X,
            proper# length1 X -> length1# proper X,
            proper# length1 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:
  {       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 length cons(X, Y) -> mark s length1 Y,
        active length nil() -> mark 0(),
           active length1 X -> mark length X,
                length ok X -> ok length X,
               length1 ok X -> ok length1 X,
        proper cons(X1, X2) -> cons(proper X1, proper X2),
              proper from X -> from proper X,
                 proper s X -> s proper X,
                 proper 0() -> ok 0(),
            proper length X -> length proper X,
               proper nil() -> ok nil(),
           proper length1 X -> length1 proper X,
                 top mark X -> top proper X,
                   top ok X -> top active X}
  EDG:
   {
    (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# length1 X -> length# X)
    (active# from X -> active# X, active# length cons(X, Y) -> length1# Y)
    (active# from X -> active# X, active# length cons(X, Y) -> s# length1 Y)
    (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))
    (active# length1 X -> length# X, length# ok X -> length# X)
    (length1# ok X -> length1# X, length1# ok X -> length1# X)
    (proper# s X -> proper# X, proper# length1 X -> proper# X)
    (proper# s X -> proper# X, proper# length1 X -> length1# proper X)
    (proper# s X -> proper# X, proper# length X -> proper# X)
    (proper# s X -> proper# X, proper# length X -> length# proper X)
    (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# from X -> proper# X)
    (proper# s X -> proper# X, proper# from X -> from# 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))
    (proper# length1 X -> proper# X, proper# length1 X -> proper# X)
    (proper# length1 X -> proper# X, proper# length1 X -> length1# proper X)
    (proper# length1 X -> proper# X, proper# length X -> proper# X)
    (proper# length1 X -> proper# X, proper# length X -> length# proper X)
    (proper# length1 X -> proper# X, proper# s X -> proper# X)
    (proper# length1 X -> proper# X, proper# s X -> s# proper X)
    (proper# length1 X -> proper# X, proper# from X -> proper# X)
    (proper# length1 X -> proper# X, proper# from X -> from# proper X)
    (proper# length1 X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# length1 X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# length1 X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (top# ok X -> active# X, active# length1 X -> length# X)
    (top# ok X -> active# X, active# length cons(X, Y) -> length1# Y)
    (top# ok X -> active# X, active# length cons(X, Y) -> s# length1 Y)
    (top# ok X -> active# X, active# s X -> active# X)
    (top# ok X -> active# X, active# s X -> s# active X)
    (top# ok X -> active# X, active# from X -> active# X)
    (top# ok X -> active# X, active# from X -> 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 -> cons#(X, from s 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))
    (proper# cons(X1, X2) -> proper# X1, proper# length1 X -> proper# X)
    (proper# cons(X1, X2) -> proper# X1, proper# length1 X -> length1# proper X)
    (proper# cons(X1, X2) -> proper# X1, proper# length X -> proper# X)
    (proper# cons(X1, X2) -> proper# X1, proper# length X -> length# proper X)
    (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# 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# length cons(X, Y) -> s# length1 Y, s# ok X -> s# X)
    (active# length cons(X, Y) -> s# length1 Y, s# mark X -> s# X)
    (active# from X -> from# active X, from# ok X -> from# X)
    (active# from X -> from# active X, from# mark X -> from# X)
    (proper# from X -> from# proper X, from# ok X -> from# X)
    (proper# from X -> from# proper X, from# mark X -> from# X)
    (proper# length X -> length# proper X, length# ok X -> length# 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)
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok 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), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(ok X1, ok X2) -> cons#(X1, 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# length1 X -> length1# proper X, length1# ok X -> length1# X)
    (proper# s X -> s# proper X, s# mark X -> s# X)
    (proper# s X -> s# proper X, s# ok X -> s# 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# s X, from# mark X -> from# X)
    (active# from X -> from# s X, from# ok X -> from# X)
    (active# length cons(X, Y) -> length1# Y, length1# ok X -> length1# X)
    (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))
    (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
    (active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
    (active# cons(X1, X2) -> active# X1, active# from 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 -> s# X)
    (active# cons(X1, X2) -> active# X1, active# from X -> active# X)
    (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# length cons(X, Y) -> s# length1 Y)
    (active# cons(X1, X2) -> active# X1, active# length cons(X, Y) -> length1# Y)
    (active# cons(X1, X2) -> active# X1, active# length1 X -> length# 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# from X -> from# proper X)
    (top# mark X -> proper# X, proper# from 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# length X -> length# proper X)
    (top# mark X -> proper# X, proper# length X -> proper# X)
    (top# mark X -> proper# X, proper# length1 X -> length1# proper X)
    (top# mark X -> proper# X, proper# length1 X -> proper# X)
    (proper# length X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# length X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# length X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# length X -> proper# X, proper# from X -> from# proper X)
    (proper# length X -> proper# X, proper# from X -> proper# X)
    (proper# length X -> proper# X, proper# s X -> s# proper X)
    (proper# length X -> proper# X, proper# s X -> proper# X)
    (proper# length X -> proper# X, proper# length X -> length# proper X)
    (proper# length X -> proper# X, proper# length X -> proper# X)
    (proper# length X -> proper# X, proper# length1 X -> length1# proper X)
    (proper# length X -> proper# X, proper# length1 X -> proper# X)
    (proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# from X -> proper# X, proper# from X -> from# proper X)
    (proper# from X -> proper# X, proper# from X -> proper# X)
    (proper# from X -> proper# X, proper# s X -> s# proper X)
    (proper# from X -> proper# X, proper# s X -> proper# X)
    (proper# from X -> proper# X, proper# length X -> length# proper X)
    (proper# from X -> proper# X, proper# length X -> proper# X)
    (proper# from X -> proper# X, proper# length1 X -> length1# proper X)
    (proper# from X -> proper# X, proper# length1 X -> proper# X)
    (length# ok X -> length# X, length# ok X -> length# 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# 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# length cons(X, Y) -> s# length1 Y)
    (active# s X -> active# X, active# length cons(X, Y) -> length1# Y)
    (active# s X -> active# X, active# length1 X -> length# X)
    (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# 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# length X -> length# proper X)
    (proper# cons(X1, X2) -> proper# X2, proper# length X -> proper# X)
    (proper# cons(X1, X2) -> proper# X2, proper# length1 X -> length1# proper X)
    (proper# cons(X1, X2) -> proper# X2, proper# length1 X -> proper# X)
   }
   EDG:
    {
     (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# length1 X -> length# X)
     (active# from X -> active# X, active# length cons(X, Y) -> length1# Y)
     (active# from X -> active# X, active# length cons(X, Y) -> s# length1 Y)
     (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))
     (length1# ok X -> length1# X, length1# ok X -> length1# X)
     (proper# s X -> proper# X, proper# length1 X -> proper# X)
     (proper# s X -> proper# X, proper# length1 X -> length1# proper X)
     (proper# s X -> proper# X, proper# length X -> proper# X)
     (proper# s X -> proper# X, proper# length X -> length# proper X)
     (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# from X -> proper# X)
     (proper# s X -> proper# X, proper# from X -> from# 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))
     (proper# length1 X -> proper# X, proper# length1 X -> proper# X)
     (proper# length1 X -> proper# X, proper# length1 X -> length1# proper X)
     (proper# length1 X -> proper# X, proper# length X -> proper# X)
     (proper# length1 X -> proper# X, proper# length X -> length# proper X)
     (proper# length1 X -> proper# X, proper# s X -> proper# X)
     (proper# length1 X -> proper# X, proper# s X -> s# proper X)
     (proper# length1 X -> proper# X, proper# from X -> proper# X)
     (proper# length1 X -> proper# X, proper# from X -> from# proper X)
     (proper# length1 X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# length1 X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# length1 X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (top# ok X -> active# X, active# length1 X -> length# X)
     (top# ok X -> active# X, active# length cons(X, Y) -> length1# Y)
     (top# ok X -> active# X, active# length cons(X, Y) -> s# length1 Y)
     (top# ok X -> active# X, active# s X -> active# X)
     (top# ok X -> active# X, active# s X -> s# active X)
     (top# ok X -> active# X, active# from X -> active# X)
     (top# ok X -> active# X, active# from X -> 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 -> cons#(X, from s 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))
     (proper# cons(X1, X2) -> proper# X1, proper# length1 X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# length1 X -> length1# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# length X -> proper# X)
     (proper# cons(X1, X2) -> proper# X1, proper# length X -> length# proper X)
     (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# 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# length cons(X, Y) -> s# length1 Y, s# ok X -> s# X)
     (active# length cons(X, Y) -> s# length1 Y, s# mark X -> s# X)
     (active# from X -> from# active X, from# ok X -> from# X)
     (active# from X -> from# active X, from# mark X -> from# X)
     (proper# from X -> from# proper X, from# ok X -> from# X)
     (proper# from X -> from# proper X, from# mark X -> from# X)
     (proper# length X -> length# proper X, length# ok X -> length# 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)
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok 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), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(ok X1, ok X2) -> cons#(X1, 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# length1 X -> length1# proper X, length1# ok X -> length1# X)
     (proper# s X -> s# proper X, s# mark X -> s# X)
     (proper# s X -> s# proper X, s# ok X -> s# 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# s X, from# mark X -> from# X)
     (active# from X -> from# s X, from# ok X -> from# X)
     (active# length cons(X, Y) -> length1# Y, length1# ok X -> length1# X)
     (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))
     (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
     (active# cons(X1, X2) -> active# X1, active# from X -> cons#(X, from s X))
     (active# cons(X1, X2) -> active# X1, active# from 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 -> s# X)
     (active# cons(X1, X2) -> active# X1, active# from X -> active# X)
     (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# length cons(X, Y) -> s# length1 Y)
     (active# cons(X1, X2) -> active# X1, active# length cons(X, Y) -> length1# Y)
     (active# cons(X1, X2) -> active# X1, active# length1 X -> length# 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# from X -> from# proper X)
     (top# mark X -> proper# X, proper# from 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# length X -> length# proper X)
     (top# mark X -> proper# X, proper# length X -> proper# X)
     (top# mark X -> proper# X, proper# length1 X -> length1# proper X)
     (top# mark X -> proper# X, proper# length1 X -> proper# X)
     (proper# length X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# length X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# length X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# length X -> proper# X, proper# from X -> from# proper X)
     (proper# length X -> proper# X, proper# from X -> proper# X)
     (proper# length X -> proper# X, proper# s X -> s# proper X)
     (proper# length X -> proper# X, proper# s X -> proper# X)
     (proper# length X -> proper# X, proper# length X -> length# proper X)
     (proper# length X -> proper# X, proper# length X -> proper# X)
     (proper# length X -> proper# X, proper# length1 X -> length1# proper X)
     (proper# length X -> proper# X, proper# length1 X -> proper# X)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# from X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# from X -> proper# X, proper# from X -> from# proper X)
     (proper# from X -> proper# X, proper# from X -> proper# X)
     (proper# from X -> proper# X, proper# s X -> s# proper X)
     (proper# from X -> proper# X, proper# s X -> proper# X)
     (proper# from X -> proper# X, proper# length X -> length# proper X)
     (proper# from X -> proper# X, proper# length X -> proper# X)
     (proper# from X -> proper# X, proper# length1 X -> length1# proper X)
     (proper# from X -> proper# X, proper# length1 X -> proper# X)
     (length# ok X -> length# X, length# ok X -> length# 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# 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# length cons(X, Y) -> s# length1 Y)
     (active# s X -> active# X, active# length cons(X, Y) -> length1# Y)
     (active# s X -> active# X, active# length1 X -> length# 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# 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# length X -> length# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# length X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# length1 X -> length1# proper X)
     (proper# cons(X1, X2) -> proper# X2, proper# length1 X -> proper# X)
    }
    STATUS:
     arrows: 0.866939
     SCCS (8):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {active# cons(X1, X2) -> active# X1,
              active# from X -> active# X,
                 active# s X -> 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# length X -> proper# X,
           proper# length1 X -> proper# X}
      Scc:
       {length1# ok X -> length1# X}
      Scc:
       {length# ok X -> length# 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 (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 length cons(X, Y) -> mark s length1 Y,
             active length nil() -> mark 0(),
                active length1 X -> mark length X,
                     length ok X -> ok length X,
                    length1 ok X -> ok length1 X,
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper from X -> from proper X,
                      proper s X -> s proper X,
                      proper 0() -> ok 0(),
                 proper length X -> length proper X,
                    proper nil() -> ok nil(),
                proper length1 X -> length1 proper X,
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      
      SCC (3):
       Strict:
        {active# cons(X1, X2) -> active# X1,
               active# from X -> active# X,
                  active# s X -> 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 length cons(X, Y) -> mark s length1 Y,
             active length nil() -> mark 0(),
                active length1 X -> mark length X,
                     length ok X -> ok length X,
                    length1 ok X -> ok length1 X,
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper from X -> from proper X,
                      proper s X -> s proper X,
                      proper 0() -> ok 0(),
                 proper length X -> length proper X,
                    proper nil() -> ok nil(),
                proper length1 X -> length1 proper X,
                      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# length X -> proper# X,
            proper# length1 X -> proper# 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 length cons(X, Y) -> mark s length1 Y,
             active length nil() -> mark 0(),
                active length1 X -> mark length X,
                     length ok X -> ok length X,
                    length1 ok X -> ok length1 X,
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper from X -> from proper X,
                      proper s X -> s proper X,
                      proper 0() -> ok 0(),
                 proper length X -> length proper X,
                    proper nil() -> ok nil(),
                proper length1 X -> length1 proper X,
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      SCC (1):
       Strict:
        {length1# ok X -> length1# 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 length cons(X, Y) -> mark s length1 Y,
             active length nil() -> mark 0(),
                active length1 X -> mark length X,
                     length ok X -> ok length X,
                    length1 ok X -> ok length1 X,
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper from X -> from proper X,
                      proper s X -> s proper X,
                      proper 0() -> ok 0(),
                 proper length X -> length proper X,
                    proper nil() -> ok nil(),
                proper length1 X -> length1 proper X,
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      SCC (1):
       Strict:
        {length# ok X -> length# 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 length cons(X, Y) -> mark s length1 Y,
             active length nil() -> mark 0(),
                active length1 X -> mark length X,
                     length ok X -> ok length X,
                    length1 ok X -> ok length1 X,
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper from X -> from proper X,
                      proper s X -> s proper X,
                      proper 0() -> ok 0(),
                 proper length X -> length proper X,
                    proper nil() -> ok nil(),
                proper length1 X -> length1 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:
       {       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 length cons(X, Y) -> mark s length1 Y,
             active length nil() -> mark 0(),
                active length1 X -> mark length X,
                     length ok X -> ok length X,
                    length1 ok X -> ok length1 X,
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper from X -> from proper X,
                      proper s X -> s proper X,
                      proper 0() -> ok 0(),
                 proper length X -> length proper X,
                    proper nil() -> ok nil(),
                proper length1 X -> length1 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:
       {       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 length cons(X, Y) -> mark s length1 Y,
             active length nil() -> mark 0(),
                active length1 X -> mark length X,
                     length ok X -> ok length X,
                    length1 ok X -> ok length1 X,
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper from X -> from proper X,
                      proper s X -> s proper X,
                      proper 0() -> ok 0(),
                 proper length X -> length proper X,
                    proper nil() -> ok nil(),
                proper length1 X -> length1 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:
       {       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 length cons(X, Y) -> mark s length1 Y,
             active length nil() -> mark 0(),
                active length1 X -> mark length X,
                     length ok X -> ok length X,
                    length1 ok X -> ok length1 X,
             proper cons(X1, X2) -> cons(proper X1, proper X2),
                   proper from X -> from proper X,
                      proper s X -> s proper X,
                      proper 0() -> ok 0(),
                 proper length X -> length proper X,
                    proper nil() -> ok nil(),
                proper length1 X -> length1 proper X,
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open