MAYBE
Time: 0.014552
TRS:
 {       cons(mark X1, X2) -> mark cons(X1, X2),
        cons(ok X1, ok X2) -> ok cons(X1, X2),
       active cons(X1, X2) -> cons(active X1, X2),
            active zeros() -> mark cons(0(), zeros()),
        active U12(X1, X2) -> U12(active X1, X2),
       active U12(tt(), L) -> mark s length L,
        active U11(X1, X2) -> U11(active X1, X2),
       active U11(tt(), L) -> mark U12(tt(), L),
                active s X -> s active X,
           active length X -> length active X,
  active length cons(N, L) -> mark U11(tt(), L),
       active length nil() -> mark 0(),
          U12(mark X1, X2) -> mark U12(X1, X2),
         U12(ok X1, ok X2) -> ok U12(X1, X2),
          U11(mark X1, X2) -> mark U11(X1, X2),
         U11(ok X1, ok X2) -> ok U11(X1, X2),
                  s mark X -> mark s X,
                    s ok X -> ok s X,
             length mark X -> mark length X,
               length ok X -> ok length X,
       proper cons(X1, X2) -> cons(proper X1, proper X2),
                proper 0() -> ok 0(),
            proper zeros() -> ok zeros(),
        proper U12(X1, X2) -> U12(proper X1, proper X2),
               proper tt() -> ok tt(),
        proper U11(X1, X2) -> U11(proper X1, proper X2),
                proper s X -> s proper X,
           proper length X -> length proper X,
              proper nil() -> ok nil(),
                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),
         active# cons(X1, X2) -> cons#(active X1, X2),
         active# cons(X1, X2) -> active# X1,
              active# zeros() -> cons#(0(), zeros()),
          active# U12(X1, X2) -> active# X1,
          active# U12(X1, X2) -> U12#(active X1, X2),
         active# U12(tt(), L) -> s# length L,
         active# U12(tt(), L) -> length# L,
          active# U11(X1, X2) -> active# X1,
          active# U11(X1, X2) -> U11#(active X1, X2),
         active# U11(tt(), L) -> U12#(tt(), L),
                  active# s X -> active# X,
                  active# s X -> s# active X,
             active# length X -> active# X,
             active# length X -> length# active X,
    active# length cons(N, L) -> U11#(tt(), L),
            U12#(mark X1, X2) -> U12#(X1, X2),
           U12#(ok X1, ok X2) -> U12#(X1, X2),
            U11#(mark X1, X2) -> U11#(X1, X2),
           U11#(ok X1, ok X2) -> U11#(X1, X2),
                    s# mark X -> s# X,
                      s# ok X -> s# X,
               length# mark X -> length# X,
                 length# ok X -> length# X,
         proper# cons(X1, X2) -> cons#(proper X1, proper X2),
         proper# cons(X1, X2) -> proper# X1,
         proper# cons(X1, X2) -> proper# X2,
          proper# U12(X1, X2) -> U12#(proper X1, proper X2),
          proper# U12(X1, X2) -> proper# X1,
          proper# U12(X1, X2) -> proper# X2,
          proper# U11(X1, X2) -> U11#(proper X1, proper X2),
          proper# U11(X1, X2) -> proper# X1,
          proper# U11(X1, X2) -> proper# X2,
                  proper# s X -> s# proper X,
                  proper# s X -> proper# X,
             proper# length X -> length# proper X,
             proper# length 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),
        active cons(X1, X2) -> cons(active X1, X2),
             active zeros() -> mark cons(0(), zeros()),
         active U12(X1, X2) -> U12(active X1, X2),
        active U12(tt(), L) -> mark s length L,
         active U11(X1, X2) -> U11(active X1, X2),
        active U11(tt(), L) -> mark U12(tt(), L),
                 active s X -> s active X,
            active length X -> length active X,
   active length cons(N, L) -> mark U11(tt(), L),
        active length nil() -> mark 0(),
           U12(mark X1, X2) -> mark U12(X1, X2),
          U12(ok X1, ok X2) -> ok U12(X1, X2),
           U11(mark X1, X2) -> mark U11(X1, X2),
          U11(ok X1, ok X2) -> ok U11(X1, X2),
                   s mark X -> mark s X,
                     s ok X -> ok s X,
              length mark X -> mark length X,
                length ok X -> ok length X,
        proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper 0() -> ok 0(),
             proper zeros() -> ok zeros(),
         proper U12(X1, X2) -> U12(proper X1, proper X2),
                proper tt() -> ok tt(),
         proper U11(X1, X2) -> U11(proper X1, proper X2),
                 proper s X -> s proper X,
            proper length X -> length proper X,
               proper nil() -> ok nil(),
                 top mark X -> top proper X,
                   top ok X -> top active X}
  EDG:
   {
    (active# length X -> length# active X, length# ok X -> length# X)
    (active# length X -> length# active X, length# mark X -> length# X)
    (proper# length X -> length# proper X, length# ok X -> length# X)
    (proper# length X -> length# proper X, length# mark X -> length# 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)
    (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))
    (U12#(mark X1, X2) -> U12#(X1, X2), U12#(ok X1, ok X2) -> U12#(X1, X2))
    (U12#(mark X1, X2) -> U12#(X1, X2), U12#(mark X1, X2) -> U12#(X1, X2))
    (U11#(mark X1, X2) -> U11#(X1, X2), U11#(ok X1, ok X2) -> U11#(X1, X2))
    (U11#(mark X1, X2) -> U11#(X1, X2), U11#(mark X1, X2) -> U11#(X1, X2))
    (active# s X -> active# X, active# length cons(N, L) -> U11#(tt(), L))
    (active# s X -> active# X, active# length X -> length# active X)
    (active# s X -> active# X, active# length 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# U11(tt(), L) -> U12#(tt(), L))
    (active# s X -> active# X, active# U11(X1, X2) -> U11#(active X1, X2))
    (active# s X -> active# X, active# U11(X1, X2) -> active# X1)
    (active# s X -> active# X, active# U12(tt(), L) -> length# L)
    (active# s X -> active# X, active# U12(tt(), L) -> s# length L)
    (active# s X -> active# X, active# U12(X1, X2) -> U12#(active X1, X2))
    (active# s X -> active# X, active# U12(X1, X2) -> active# X1)
    (active# s X -> active# X, active# zeros() -> cons#(0(), zeros()))
    (active# s X -> active# X, active# cons(X1, X2) -> active# X1)
    (active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (s# mark X -> s# X, s# ok X -> s# X)
    (s# mark X -> s# X, s# mark X -> s# X)
    (length# mark X -> length# X, length# ok X -> length# X)
    (length# mark X -> length# X, length# mark X -> length# 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# U11(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# U11(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# U12(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# U12(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# U12(X1, X2) -> U12#(proper X1, proper X2))
    (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
    (proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
    (proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# length X -> proper# X)
    (top# mark X -> proper# X, proper# length X -> length# 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# U11(X1, X2) -> proper# X2)
    (top# mark X -> proper# X, proper# U11(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
    (top# mark X -> proper# X, proper# U12(X1, X2) -> proper# X2)
    (top# mark X -> proper# X, proper# U12(X1, X2) -> proper# X1)
    (top# mark X -> proper# X, proper# U12(X1, X2) -> U12#(proper X1, proper X2))
    (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# cons(X1, X2) -> active# X1, active# length cons(N, L) -> U11#(tt(), L))
    (active# cons(X1, X2) -> active# X1, active# length X -> length# active X)
    (active# cons(X1, X2) -> active# X1, active# length 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# U11(tt(), L) -> U12#(tt(), L))
    (active# cons(X1, X2) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
    (active# cons(X1, X2) -> active# X1, active# U11(X1, X2) -> active# X1)
    (active# cons(X1, X2) -> active# X1, active# U12(tt(), L) -> length# L)
    (active# cons(X1, X2) -> active# X1, active# U12(tt(), L) -> s# length L)
    (active# cons(X1, X2) -> active# X1, active# U12(X1, X2) -> U12#(active X1, X2))
    (active# cons(X1, X2) -> active# X1, active# U12(X1, X2) -> active# X1)
    (active# cons(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
    (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# U11(X1, X2) -> active# X1, active# length cons(N, L) -> U11#(tt(), L))
    (active# U11(X1, X2) -> active# X1, active# length X -> length# active X)
    (active# U11(X1, X2) -> active# X1, active# length X -> active# X)
    (active# U11(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# U11(X1, X2) -> active# X1, active# s X -> active# X)
    (active# U11(X1, X2) -> active# X1, active# U11(tt(), L) -> U12#(tt(), L))
    (active# U11(X1, X2) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
    (active# U11(X1, X2) -> active# X1, active# U11(X1, X2) -> active# X1)
    (active# U11(X1, X2) -> active# X1, active# U12(tt(), L) -> length# L)
    (active# U11(X1, X2) -> active# X1, active# U12(tt(), L) -> s# length L)
    (active# U11(X1, X2) -> active# X1, active# U12(X1, X2) -> U12#(active X1, X2))
    (active# U11(X1, X2) -> active# X1, active# U12(X1, X2) -> active# X1)
    (active# U11(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
    (active# U11(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
    (active# U11(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
    (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# U11(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X1, proper# U12(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X1, proper# U12(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X1, proper# U12(X1, X2) -> U12#(proper X1, proper X2))
    (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))
    (proper# U12(X1, X2) -> proper# X1, proper# length X -> proper# X)
    (proper# U12(X1, X2) -> proper# X1, proper# length X -> length# proper X)
    (proper# U12(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# U12(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# U12(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
    (proper# U12(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
    (proper# U12(X1, X2) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
    (proper# U12(X1, X2) -> proper# X1, proper# U12(X1, X2) -> proper# X2)
    (proper# U12(X1, X2) -> proper# X1, proper# U12(X1, X2) -> proper# X1)
    (proper# U12(X1, X2) -> proper# X1, proper# U12(X1, X2) -> U12#(proper X1, proper X2))
    (proper# U12(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
    (proper# U12(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
    (proper# U12(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# U11(X1, X2) -> proper# X1, proper# length X -> proper# X)
    (proper# U11(X1, X2) -> proper# X1, proper# length X -> length# proper X)
    (proper# U11(X1, X2) -> proper# X1, proper# s X -> proper# X)
    (proper# U11(X1, X2) -> proper# X1, proper# s X -> s# proper X)
    (proper# U11(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X2)
    (proper# U11(X1, X2) -> proper# X1, proper# U11(X1, X2) -> proper# X1)
    (proper# U11(X1, X2) -> proper# X1, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
    (proper# U11(X1, X2) -> proper# X1, proper# U12(X1, X2) -> proper# X2)
    (proper# U11(X1, X2) -> proper# X1, proper# U12(X1, X2) -> proper# X1)
    (proper# U11(X1, X2) -> proper# X1, proper# U12(X1, X2) -> U12#(proper X1, proper X2))
    (proper# U11(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
    (proper# U11(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
    (proper# U11(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# U12(X1, X2) -> proper# X2, proper# length X -> proper# X)
    (proper# U12(X1, X2) -> proper# X2, proper# length X -> length# proper X)
    (proper# U12(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# U12(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# U12(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
    (proper# U12(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
    (proper# U12(X1, X2) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
    (proper# U12(X1, X2) -> proper# X2, proper# U12(X1, X2) -> proper# X2)
    (proper# U12(X1, X2) -> proper# X2, proper# U12(X1, X2) -> proper# X1)
    (proper# U12(X1, X2) -> proper# X2, proper# U12(X1, X2) -> U12#(proper X1, proper X2))
    (proper# U12(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
    (proper# U12(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
    (proper# U12(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# U11(X1, X2) -> U11#(active X1, X2), U11#(ok X1, ok X2) -> U11#(X1, X2))
    (active# U11(X1, X2) -> U11#(active X1, X2), U11#(mark X1, X2) -> U11#(X1, X2))
    (active# U12(X1, X2) -> U12#(active X1, X2), U12#(mark X1, X2) -> U12#(X1, X2))
    (active# U12(X1, X2) -> U12#(active X1, X2), U12#(ok X1, ok X2) -> U12#(X1, X2))
    (proper# U11(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
    (proper# U11(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
    (proper# U11(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
    (proper# U11(X1, X2) -> proper# X2, proper# U12(X1, X2) -> U12#(proper X1, proper X2))
    (proper# U11(X1, X2) -> proper# X2, proper# U12(X1, X2) -> proper# X1)
    (proper# U11(X1, X2) -> proper# X2, proper# U12(X1, X2) -> proper# X2)
    (proper# U11(X1, X2) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
    (proper# U11(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
    (proper# U11(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
    (proper# U11(X1, X2) -> proper# X2, proper# s X -> s# proper X)
    (proper# U11(X1, X2) -> proper# X2, proper# s X -> proper# X)
    (proper# U11(X1, X2) -> proper# X2, proper# length X -> length# proper X)
    (proper# U11(X1, X2) -> proper# X2, proper# length X -> proper# 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# U12(X1, X2) -> U12#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X2, proper# U12(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X2, proper# U12(X1, X2) -> proper# X2)
    (proper# cons(X1, X2) -> proper# X2, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
    (proper# cons(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X1)
    (proper# cons(X1, X2) -> proper# X2, proper# U11(X1, X2) -> proper# X2)
    (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)
    (active# U12(tt(), L) -> length# L, length# mark X -> length# X)
    (active# U12(tt(), L) -> length# L, length# ok X -> length# X)
    (proper# U11(X1, X2) -> U11#(proper X1, proper X2), U11#(mark X1, X2) -> U11#(X1, X2))
    (proper# U11(X1, X2) -> U11#(proper X1, proper X2), U11#(ok X1, ok X2) -> U11#(X1, X2))
    (proper# U12(X1, X2) -> U12#(proper X1, proper X2), U12#(mark X1, X2) -> U12#(X1, X2))
    (proper# U12(X1, X2) -> U12#(proper X1, proper X2), U12#(ok X1, ok X2) -> U12#(X1, X2))
    (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# U12(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# U12(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
    (active# U12(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
    (active# U12(X1, X2) -> active# X1, active# U12(X1, X2) -> active# X1)
    (active# U12(X1, X2) -> active# X1, active# U12(X1, X2) -> U12#(active X1, X2))
    (active# U12(X1, X2) -> active# X1, active# U12(tt(), L) -> s# length L)
    (active# U12(X1, X2) -> active# X1, active# U12(tt(), L) -> length# L)
    (active# U12(X1, X2) -> active# X1, active# U11(X1, X2) -> active# X1)
    (active# U12(X1, X2) -> active# X1, active# U11(X1, X2) -> U11#(active X1, X2))
    (active# U12(X1, X2) -> active# X1, active# U11(tt(), L) -> U12#(tt(), L))
    (active# U12(X1, X2) -> active# X1, active# s X -> active# X)
    (active# U12(X1, X2) -> active# X1, active# s X -> s# active X)
    (active# U12(X1, X2) -> active# X1, active# length X -> active# X)
    (active# U12(X1, X2) -> active# X1, active# length X -> length# active X)
    (active# U12(X1, X2) -> active# X1, active# length cons(N, L) -> U11#(tt(), L))
    (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# zeros() -> cons#(0(), zeros()))
    (top# ok X -> active# X, active# U12(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# U12(X1, X2) -> U12#(active X1, X2))
    (top# ok X -> active# X, active# U12(tt(), L) -> s# length L)
    (top# ok X -> active# X, active# U12(tt(), L) -> length# L)
    (top# ok X -> active# X, active# U11(X1, X2) -> active# X1)
    (top# ok X -> active# X, active# U11(X1, X2) -> U11#(active X1, X2))
    (top# ok X -> active# X, active# U11(tt(), L) -> U12#(tt(), L))
    (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# length X -> active# X)
    (top# ok X -> active# X, active# length X -> length# active X)
    (top# ok X -> active# X, active# length cons(N, L) -> U11#(tt(), L))
    (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# U12(X1, X2) -> U12#(proper X1, proper X2))
    (proper# length X -> proper# X, proper# U12(X1, X2) -> proper# X1)
    (proper# length X -> proper# X, proper# U12(X1, X2) -> proper# X2)
    (proper# length X -> proper# X, proper# U11(X1, X2) -> U11#(proper X1, proper X2))
    (proper# length X -> proper# X, proper# U11(X1, X2) -> proper# X1)
    (proper# length X -> proper# X, proper# U11(X1, X2) -> proper# X2)
    (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)
    (length# ok X -> length# X, length# mark X -> length# X)
    (length# ok X -> length# X, length# ok X -> length# X)
    (s# ok X -> s# X, s# mark X -> s# X)
    (s# ok X -> s# X, s# ok X -> s# X)
    (active# length X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
    (active# length X -> active# X, active# cons(X1, X2) -> active# X1)
    (active# length X -> active# X, active# zeros() -> cons#(0(), zeros()))
    (active# length X -> active# X, active# U12(X1, X2) -> active# X1)
    (active# length X -> active# X, active# U12(X1, X2) -> U12#(active X1, X2))
    (active# length X -> active# X, active# U12(tt(), L) -> s# length L)
    (active# length X -> active# X, active# U12(tt(), L) -> length# L)
    (active# length X -> active# X, active# U11(X1, X2) -> active# X1)
    (active# length X -> active# X, active# U11(X1, X2) -> U11#(active X1, X2))
    (active# length X -> active# X, active# U11(tt(), L) -> U12#(tt(), L))
    (active# length X -> active# X, active# s X -> active# X)
    (active# length X -> active# X, active# s X -> s# active X)
    (active# length X -> active# X, active# length X -> active# X)
    (active# length X -> active# X, active# length X -> length# active X)
    (active# length X -> active# X, active# length cons(N, L) -> U11#(tt(), L))
    (U11#(ok X1, ok X2) -> U11#(X1, X2), U11#(mark X1, X2) -> U11#(X1, X2))
    (U11#(ok X1, ok X2) -> U11#(X1, X2), U11#(ok X1, ok X2) -> U11#(X1, X2))
    (U12#(ok X1, ok X2) -> U12#(X1, X2), U12#(mark X1, X2) -> U12#(X1, X2))
    (U12#(ok X1, ok X2) -> U12#(X1, X2), U12#(ok X1, ok X2) -> U12#(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))
    (active# U12(tt(), L) -> s# length L, s# mark X -> s# X)
    (active# U12(tt(), L) -> s# length L, s# ok X -> s# X)
    (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# 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)
   }
   STATUS:
    arrows: 0.853175
    SCCS (8):
     Scc:
      {top# mark X -> top# proper X,
         top# ok X -> top# active X}
     Scc:
      {active# cons(X1, X2) -> active# X1,
        active# U12(X1, X2) -> active# X1,
        active# U11(X1, X2) -> active# X1,
                active# s X -> active# X,
           active# length X -> active# X}
     Scc:
      {proper# cons(X1, X2) -> proper# X1,
       proper# cons(X1, X2) -> proper# X2,
        proper# U12(X1, X2) -> proper# X1,
        proper# U12(X1, X2) -> proper# X2,
        proper# U11(X1, X2) -> proper# X1,
        proper# U11(X1, X2) -> proper# X2,
                proper# s X -> proper# X,
           proper# length X -> proper# X}
     Scc:
      { U11#(mark X1, X2) -> U11#(X1, X2),
       U11#(ok X1, ok X2) -> U11#(X1, X2)}
     Scc:
      { U12#(mark X1, X2) -> U12#(X1, X2),
       U12#(ok X1, ok X2) -> U12#(X1, X2)}
     Scc:
      { cons#(mark X1, X2) -> cons#(X1, X2),
       cons#(ok X1, ok X2) -> cons#(X1, X2)}
     Scc:
      {length# mark X -> length# X,
         length# ok X -> length# X}
     Scc:
      {s# mark X -> s# X,
         s# ok X -> s# X}
     
     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),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active U12(X1, X2) -> U12(active X1, X2),
            active U12(tt(), L) -> mark s length L,
             active U11(X1, X2) -> U11(active X1, X2),
            active U11(tt(), L) -> mark U12(tt(), L),
                     active s X -> s active X,
                active length X -> length active X,
       active length cons(N, L) -> mark U11(tt(), L),
            active length nil() -> mark 0(),
               U12(mark X1, X2) -> mark U12(X1, X2),
              U12(ok X1, ok X2) -> ok U12(X1, X2),
               U11(mark X1, X2) -> mark U11(X1, X2),
              U11(ok X1, ok X2) -> ok U11(X1, X2),
                       s mark X -> mark s X,
                         s ok X -> ok s X,
                  length mark X -> mark length X,
                    length ok X -> ok length X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper U12(X1, X2) -> U12(proper X1, proper X2),
                    proper tt() -> ok tt(),
             proper U11(X1, X2) -> U11(proper X1, proper X2),
                     proper s X -> s proper X,
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     SCC (5):
      Strict:
       {active# cons(X1, X2) -> active# X1,
         active# U12(X1, X2) -> active# X1,
         active# U11(X1, X2) -> active# X1,
                 active# s X -> active# X,
            active# length X -> active# X}
      Weak:
      {       cons(mark X1, X2) -> mark cons(X1, X2),
             cons(ok X1, ok X2) -> ok cons(X1, X2),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active U12(X1, X2) -> U12(active X1, X2),
            active U12(tt(), L) -> mark s length L,
             active U11(X1, X2) -> U11(active X1, X2),
            active U11(tt(), L) -> mark U12(tt(), L),
                     active s X -> s active X,
                active length X -> length active X,
       active length cons(N, L) -> mark U11(tt(), L),
            active length nil() -> mark 0(),
               U12(mark X1, X2) -> mark U12(X1, X2),
              U12(ok X1, ok X2) -> ok U12(X1, X2),
               U11(mark X1, X2) -> mark U11(X1, X2),
              U11(ok X1, ok X2) -> ok U11(X1, X2),
                       s mark X -> mark s X,
                         s ok X -> ok s X,
                  length mark X -> mark length X,
                    length ok X -> ok length X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper U12(X1, X2) -> U12(proper X1, proper X2),
                    proper tt() -> ok tt(),
             proper U11(X1, X2) -> U11(proper X1, proper X2),
                     proper s X -> s proper X,
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     
     
     
     
     
     
     
     
     SCC (8):
      Strict:
       {proper# cons(X1, X2) -> proper# X1,
        proper# cons(X1, X2) -> proper# X2,
         proper# U12(X1, X2) -> proper# X1,
         proper# U12(X1, X2) -> proper# X2,
         proper# U11(X1, X2) -> proper# X1,
         proper# U11(X1, X2) -> proper# X2,
                 proper# s X -> proper# X,
            proper# length X -> proper# X}
      Weak:
      {       cons(mark X1, X2) -> mark cons(X1, X2),
             cons(ok X1, ok X2) -> ok cons(X1, X2),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active U12(X1, X2) -> U12(active X1, X2),
            active U12(tt(), L) -> mark s length L,
             active U11(X1, X2) -> U11(active X1, X2),
            active U11(tt(), L) -> mark U12(tt(), L),
                     active s X -> s active X,
                active length X -> length active X,
       active length cons(N, L) -> mark U11(tt(), L),
            active length nil() -> mark 0(),
               U12(mark X1, X2) -> mark U12(X1, X2),
              U12(ok X1, ok X2) -> ok U12(X1, X2),
               U11(mark X1, X2) -> mark U11(X1, X2),
              U11(ok X1, ok X2) -> ok U11(X1, X2),
                       s mark X -> mark s X,
                         s ok X -> ok s X,
                  length mark X -> mark length X,
                    length ok X -> ok length X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper U12(X1, X2) -> U12(proper X1, proper X2),
                    proper tt() -> ok tt(),
             proper U11(X1, X2) -> U11(proper X1, proper X2),
                     proper s X -> s proper X,
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     SCC (2):
      Strict:
       { U11#(mark X1, X2) -> U11#(X1, X2),
        U11#(ok X1, ok X2) -> U11#(X1, X2)}
      Weak:
      {       cons(mark X1, X2) -> mark cons(X1, X2),
             cons(ok X1, ok X2) -> ok cons(X1, X2),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active U12(X1, X2) -> U12(active X1, X2),
            active U12(tt(), L) -> mark s length L,
             active U11(X1, X2) -> U11(active X1, X2),
            active U11(tt(), L) -> mark U12(tt(), L),
                     active s X -> s active X,
                active length X -> length active X,
       active length cons(N, L) -> mark U11(tt(), L),
            active length nil() -> mark 0(),
               U12(mark X1, X2) -> mark U12(X1, X2),
              U12(ok X1, ok X2) -> ok U12(X1, X2),
               U11(mark X1, X2) -> mark U11(X1, X2),
              U11(ok X1, ok X2) -> ok U11(X1, X2),
                       s mark X -> mark s X,
                         s ok X -> ok s X,
                  length mark X -> mark length X,
                    length ok X -> ok length X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper U12(X1, X2) -> U12(proper X1, proper X2),
                    proper tt() -> ok tt(),
             proper U11(X1, X2) -> U11(proper X1, proper X2),
                     proper s X -> s proper X,
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     SCC (2):
      Strict:
       { U12#(mark X1, X2) -> U12#(X1, X2),
        U12#(ok X1, ok X2) -> U12#(X1, X2)}
      Weak:
      {       cons(mark X1, X2) -> mark cons(X1, X2),
             cons(ok X1, ok X2) -> ok cons(X1, X2),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active U12(X1, X2) -> U12(active X1, X2),
            active U12(tt(), L) -> mark s length L,
             active U11(X1, X2) -> U11(active X1, X2),
            active U11(tt(), L) -> mark U12(tt(), L),
                     active s X -> s active X,
                active length X -> length active X,
       active length cons(N, L) -> mark U11(tt(), L),
            active length nil() -> mark 0(),
               U12(mark X1, X2) -> mark U12(X1, X2),
              U12(ok X1, ok X2) -> ok U12(X1, X2),
               U11(mark X1, X2) -> mark U11(X1, X2),
              U11(ok X1, ok X2) -> ok U11(X1, X2),
                       s mark X -> mark s X,
                         s ok X -> ok s X,
                  length mark X -> mark length X,
                    length ok X -> ok length X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper U12(X1, X2) -> U12(proper X1, proper X2),
                    proper tt() -> ok tt(),
             proper U11(X1, X2) -> U11(proper X1, proper X2),
                     proper s X -> s proper X,
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     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),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active U12(X1, X2) -> U12(active X1, X2),
            active U12(tt(), L) -> mark s length L,
             active U11(X1, X2) -> U11(active X1, X2),
            active U11(tt(), L) -> mark U12(tt(), L),
                     active s X -> s active X,
                active length X -> length active X,
       active length cons(N, L) -> mark U11(tt(), L),
            active length nil() -> mark 0(),
               U12(mark X1, X2) -> mark U12(X1, X2),
              U12(ok X1, ok X2) -> ok U12(X1, X2),
               U11(mark X1, X2) -> mark U11(X1, X2),
              U11(ok X1, ok X2) -> ok U11(X1, X2),
                       s mark X -> mark s X,
                         s ok X -> ok s X,
                  length mark X -> mark length X,
                    length ok X -> ok length X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper U12(X1, X2) -> U12(proper X1, proper X2),
                    proper tt() -> ok tt(),
             proper U11(X1, X2) -> U11(proper X1, proper X2),
                     proper s X -> s proper X,
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open
     
     
     
     SCC (2):
      Strict:
       {length# mark X -> length# X,
          length# ok X -> length# X}
      Weak:
      {       cons(mark X1, X2) -> mark cons(X1, X2),
             cons(ok X1, ok X2) -> ok cons(X1, X2),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active U12(X1, X2) -> U12(active X1, X2),
            active U12(tt(), L) -> mark s length L,
             active U11(X1, X2) -> U11(active X1, X2),
            active U11(tt(), L) -> mark U12(tt(), L),
                     active s X -> s active X,
                active length X -> length active X,
       active length cons(N, L) -> mark U11(tt(), L),
            active length nil() -> mark 0(),
               U12(mark X1, X2) -> mark U12(X1, X2),
              U12(ok X1, ok X2) -> ok U12(X1, X2),
               U11(mark X1, X2) -> mark U11(X1, X2),
              U11(ok X1, ok X2) -> ok U11(X1, X2),
                       s mark X -> mark s X,
                         s ok X -> ok s X,
                  length mark X -> mark length X,
                    length ok X -> ok length X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper U12(X1, X2) -> U12(proper X1, proper X2),
                    proper tt() -> ok tt(),
             proper U11(X1, X2) -> U11(proper X1, proper X2),
                     proper s X -> s proper X,
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     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),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
             active U12(X1, X2) -> U12(active X1, X2),
            active U12(tt(), L) -> mark s length L,
             active U11(X1, X2) -> U11(active X1, X2),
            active U11(tt(), L) -> mark U12(tt(), L),
                     active s X -> s active X,
                active length X -> length active X,
       active length cons(N, L) -> mark U11(tt(), L),
            active length nil() -> mark 0(),
               U12(mark X1, X2) -> mark U12(X1, X2),
              U12(ok X1, ok X2) -> ok U12(X1, X2),
               U11(mark X1, X2) -> mark U11(X1, X2),
              U11(ok X1, ok X2) -> ok U11(X1, X2),
                       s mark X -> mark s X,
                         s ok X -> ok s X,
                  length mark X -> mark length X,
                    length ok X -> ok length X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
             proper U12(X1, X2) -> U12(proper X1, proper X2),
                    proper tt() -> ok tt(),
             proper U11(X1, X2) -> U11(proper X1, proper X2),
                     proper s X -> s proper X,
                proper length X -> length proper X,
                   proper nil() -> ok nil(),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      Open