MAYBE
Time: 0.003283
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 tail X -> tail active X,
  active tail cons(X, XS) -> mark XS,
              tail mark X -> mark tail X,
                tail ok X -> ok tail X,
      proper cons(X1, X2) -> cons(proper X1, proper X2),
               proper 0() -> ok 0(),
           proper zeros() -> ok zeros(),
            proper tail X -> tail 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),
    active# cons(X1, X2) -> cons#(active X1, X2),
    active# cons(X1, X2) -> active# X1,
         active# zeros() -> cons#(0(), zeros()),
          active# tail X -> active# X,
          active# tail X -> tail# active X,
            tail# mark X -> tail# X,
              tail# ok X -> tail# X,
    proper# cons(X1, X2) -> cons#(proper X1, proper X2),
    proper# cons(X1, X2) -> proper# X1,
    proper# cons(X1, X2) -> proper# X2,
          proper# tail X -> tail# proper X,
          proper# tail 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 tail X -> tail active X,
   active tail cons(X, XS) -> mark XS,
               tail mark X -> mark tail X,
                 tail ok X -> ok tail X,
       proper cons(X1, X2) -> cons(proper X1, proper X2),
                proper 0() -> ok 0(),
            proper zeros() -> ok zeros(),
             proper tail X -> tail proper X,
                top mark X -> top proper X,
                  top ok X -> top active X}
  UR:
   {      cons(mark X1, X2) -> mark cons(X1, X2),
         cons(ok X1, ok X2) -> ok cons(X1, X2),
        active cons(X1, X2) -> cons(active X1, X2),
             active zeros() -> mark cons(0(), zeros()),
              active tail X -> tail active X,
    active tail cons(X, XS) -> mark XS,
                tail mark X -> mark tail X,
                  tail ok X -> ok tail X,
        proper cons(X1, X2) -> cons(proper X1, proper X2),
                 proper 0() -> ok 0(),
             proper zeros() -> ok zeros(),
              proper tail X -> tail proper X}
   EDG:
    {(active# cons(X1, X2) -> active# X1, active# tail X -> tail# active X)
     (active# cons(X1, X2) -> active# X1, active# tail X -> active# X)
     (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# zeros() -> cons#(0(), zeros()), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (active# zeros() -> cons#(0(), zeros()), cons#(mark X1, X2) -> cons#(X1, X2))
     (proper# tail X -> tail# proper X, tail# ok X -> tail# X)
     (proper# tail X -> tail# proper X, tail# mark X -> tail# 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)
     (tail# mark X -> tail# X, tail# ok X -> tail# X)
     (tail# mark X -> tail# X, tail# mark X -> tail# X)
     (proper# tail X -> proper# X, proper# tail X -> proper# X)
     (proper# tail X -> proper# X, proper# tail X -> tail# proper X)
     (proper# tail X -> proper# X, proper# cons(X1, X2) -> proper# X2)
     (proper# tail X -> proper# X, proper# cons(X1, X2) -> proper# X1)
     (proper# tail X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
     (top# ok X -> active# X, active# tail X -> tail# active X)
     (top# ok X -> active# X, active# tail X -> active# X)
     (top# ok X -> active# X, active# zeros() -> cons#(0(), zeros()))
     (top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# cons(X1, X2) -> cons#(active 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#(mark X1, X2) -> cons#(X1, X2))
     (proper# cons(X1, X2) -> proper# X2, proper# tail X -> proper# X)
     (proper# cons(X1, X2) -> proper# X2, proper# tail X -> tail# 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))
     (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))
     (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
     (top# 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# tail X -> tail# proper X)
     (top# mark X -> proper# X, proper# tail X -> proper# X)
     (tail# ok X -> tail# X, tail# mark X -> tail# X)
     (tail# ok X -> tail# X, tail# ok X -> tail# X)
     (active# tail X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
     (active# tail X -> active# X, active# cons(X1, X2) -> active# X1)
     (active# tail X -> active# X, active# zeros() -> cons#(0(), zeros()))
     (active# tail X -> active# X, active# tail X -> active# X)
     (active# tail X -> active# X, active# tail X -> tail# active 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)
     (active# tail X -> tail# active X, tail# mark X -> tail# X)
     (active# tail X -> tail# active X, tail# ok X -> tail# X)
     (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# tail X -> tail# proper X)
     (proper# cons(X1, X2) -> proper# X1, proper# tail X -> proper# X)
     (active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))}
    STATUS:
     arrows: 0.811728
     SCCS (5):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {proper# cons(X1, X2) -> proper# X1,
        proper# cons(X1, X2) -> proper# X2,
              proper# tail X -> proper# X}
      Scc:
       {active# cons(X1, X2) -> active# X1,
              active# tail X -> active# X}
      Scc:
       {tail# mark X -> tail# X,
          tail# ok X -> tail# 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),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
                  active tail X -> tail active X,
        active tail cons(X, XS) -> mark XS,
                    tail mark X -> mark tail X,
                      tail ok X -> ok tail X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
                  proper tail X -> tail proper X,
                     top mark X -> top proper X,
                       top ok X -> top active X}
       Open
      
      
      SCC (3):
       Strict:
        {proper# cons(X1, X2) -> proper# X1,
         proper# cons(X1, X2) -> proper# X2,
               proper# tail 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 tail X -> tail active X,
        active tail cons(X, XS) -> mark XS,
                    tail mark X -> mark tail X,
                      tail ok X -> ok tail X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
                  proper tail X -> tail proper X,
                     top mark X -> top proper X,
                       top ok X -> top active X}
       Open
      
      
      SCC (2):
       Strict:
        {active# cons(X1, X2) -> active# X1,
               active# tail 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 tail X -> tail active X,
        active tail cons(X, XS) -> mark XS,
                    tail mark X -> mark tail X,
                      tail ok X -> ok tail X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
                  proper tail X -> tail proper X,
                     top mark X -> top proper X,
                       top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        {tail# mark X -> tail# X,
           tail# ok X -> tail# 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 tail X -> tail active X,
        active tail cons(X, XS) -> mark XS,
                    tail mark X -> mark tail X,
                      tail ok X -> ok tail X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
                  proper tail X -> tail 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),
            active cons(X1, X2) -> cons(active X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
                  active tail X -> tail active X,
        active tail cons(X, XS) -> mark XS,
                    tail mark X -> mark tail X,
                      tail ok X -> ok tail X,
            proper cons(X1, X2) -> cons(proper X1, proper X2),
                     proper 0() -> ok 0(),
                 proper zeros() -> ok zeros(),
                  proper tail X -> tail proper X,
                     top mark X -> top proper X,
                       top ok X -> top active X}
       Open