MAYBE
Time: 0.018922
TRS:
 {       mark cons(X1, X2) -> active cons(mark X1, X2),
                  mark 0() -> active 0(),
              mark zeros() -> active zeros(),
          mark and(X1, X2) -> active and(mark X1, X2),
                 mark tt() -> active tt(),
             mark length X -> active length mark X,
                mark nil() -> active nil(),
                  mark s X -> active s mark X,
         cons(X1, mark X2) -> cons(X1, X2),
       cons(X1, active X2) -> cons(X1, X2),
         cons(mark X1, X2) -> cons(X1, X2),
       cons(active X1, X2) -> cons(X1, X2),
            active zeros() -> mark cons(0(), zeros()),
       active and(tt(), X) -> mark X,
  active length cons(N, L) -> mark s length L,
       active length nil() -> mark 0(),
          and(X1, mark X2) -> and(X1, X2),
        and(X1, active X2) -> and(X1, X2),
          and(mark X1, X2) -> and(X1, X2),
        and(active X1, X2) -> and(X1, X2),
             length mark X -> length X,
           length active X -> length X,
                  s mark X -> s X,
                s active X -> s X}
 DP:
  DP:
   {       mark# cons(X1, X2) -> mark# X1,
           mark# cons(X1, X2) -> cons#(mark X1, X2),
           mark# cons(X1, X2) -> active# cons(mark X1, X2),
                    mark# 0() -> active# 0(),
                mark# zeros() -> active# zeros(),
            mark# and(X1, X2) -> mark# X1,
            mark# and(X1, X2) -> active# and(mark X1, X2),
            mark# and(X1, X2) -> and#(mark X1, X2),
                   mark# tt() -> active# tt(),
               mark# length X -> mark# X,
               mark# length X -> active# length mark X,
               mark# length X -> length# mark X,
                  mark# nil() -> active# nil(),
                    mark# s X -> mark# X,
                    mark# s X -> active# s mark X,
                    mark# s X -> s# mark X,
           cons#(X1, mark X2) -> cons#(X1, X2),
         cons#(X1, active X2) -> cons#(X1, X2),
           cons#(mark X1, X2) -> cons#(X1, X2),
         cons#(active X1, X2) -> cons#(X1, X2),
              active# zeros() -> mark# cons(0(), zeros()),
              active# zeros() -> cons#(0(), zeros()),
         active# and(tt(), X) -> mark# X,
    active# length cons(N, L) -> mark# s length L,
    active# length cons(N, L) -> length# L,
    active# length cons(N, L) -> s# length L,
         active# length nil() -> mark# 0(),
            and#(X1, mark X2) -> and#(X1, X2),
          and#(X1, active X2) -> and#(X1, X2),
            and#(mark X1, X2) -> and#(X1, X2),
          and#(active X1, X2) -> and#(X1, X2),
               length# mark X -> length# X,
             length# active X -> length# X,
                    s# mark X -> s# X,
                  s# active X -> s# X}
  TRS:
  {       mark cons(X1, X2) -> active cons(mark X1, X2),
                   mark 0() -> active 0(),
               mark zeros() -> active zeros(),
           mark and(X1, X2) -> active and(mark X1, X2),
                  mark tt() -> active tt(),
              mark length X -> active length mark X,
                 mark nil() -> active nil(),
                   mark s X -> active s mark X,
          cons(X1, mark X2) -> cons(X1, X2),
        cons(X1, active X2) -> cons(X1, X2),
          cons(mark X1, X2) -> cons(X1, X2),
        cons(active X1, X2) -> cons(X1, X2),
             active zeros() -> mark cons(0(), zeros()),
        active and(tt(), X) -> mark X,
   active length cons(N, L) -> mark s length L,
        active length nil() -> mark 0(),
           and(X1, mark X2) -> and(X1, X2),
         and(X1, active X2) -> and(X1, X2),
           and(mark X1, X2) -> and(X1, X2),
         and(active X1, X2) -> and(X1, X2),
              length mark X -> length X,
            length active X -> length X,
                   s mark X -> s X,
                 s active X -> s X}
  EDG:
   {
    (mark# and(X1, X2) -> mark# X1, mark# s X -> s# mark X)
    (mark# and(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
    (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X)
    (mark# and(X1, X2) -> mark# X1, mark# nil() -> active# nil())
    (mark# and(X1, X2) -> mark# X1, mark# length X -> length# mark X)
    (mark# and(X1, X2) -> mark# X1, mark# length X -> active# length mark X)
    (mark# and(X1, X2) -> mark# X1, mark# length X -> mark# X)
    (mark# and(X1, X2) -> mark# X1, mark# tt() -> active# tt())
    (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
    (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2))
    (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
    (mark# and(X1, X2) -> mark# X1, mark# zeros() -> active# zeros())
    (mark# and(X1, X2) -> mark# X1, mark# 0() -> active# 0())
    (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
    (mark# zeros() -> active# zeros(), active# zeros() -> cons#(0(), zeros()))
    (mark# zeros() -> active# zeros(), active# zeros() -> mark# cons(0(), zeros()))
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# length nil() -> mark# 0())
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# length cons(N, L) -> s# length L)
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# length cons(N, L) -> length# L)
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# length cons(N, L) -> mark# s length L)
    (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# and(tt(), X) -> mark# X)
    (mark# s X -> mark# X, mark# s X -> s# mark X)
    (mark# s X -> mark# X, mark# s X -> active# s mark X)
    (mark# s X -> mark# X, mark# s X -> mark# X)
    (mark# s X -> mark# X, mark# nil() -> active# nil())
    (mark# s X -> mark# X, mark# length X -> length# mark X)
    (mark# s X -> mark# X, mark# length X -> active# length mark X)
    (mark# s X -> mark# X, mark# length X -> mark# X)
    (mark# s X -> mark# X, mark# tt() -> active# tt())
    (mark# s X -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
    (mark# s X -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
    (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# zeros() -> active# zeros())
    (mark# s X -> mark# X, mark# 0() -> active# 0())
    (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (length# mark X -> length# X, length# active X -> length# X)
    (length# mark X -> length# X, length# mark X -> length# X)
    (s# mark X -> s# X, s# active X -> s# X)
    (s# mark X -> s# X, s# mark X -> s# X)
    (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> cons#(mark X1, X2))
    (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> mark# X1)
    (mark# s X -> active# s mark X, active# length nil() -> mark# 0())
    (mark# s X -> active# s mark X, active# length cons(N, L) -> s# length L)
    (mark# s X -> active# s mark X, active# length cons(N, L) -> length# L)
    (mark# s X -> active# s mark X, active# length cons(N, L) -> mark# s length L)
    (mark# s X -> active# s mark X, active# and(tt(), X) -> mark# X)
    (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (and#(X1, mark X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (and#(X1, mark X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(X1, mark X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (and#(X1, mark X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (and#(mark X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(mark X1, X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (and#(mark X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (active# length cons(N, L) -> length# L, length# active X -> length# X)
    (active# length cons(N, L) -> length# L, length# mark X -> length# X)
    (mark# length X -> length# mark X, length# active X -> length# X)
    (mark# length X -> length# mark X, length# mark X -> length# X)
    (mark# s X -> s# mark X, s# mark X -> s# X)
    (mark# s X -> s# mark X, s# active X -> s# X)
    (active# length cons(N, L) -> s# length L, s# mark X -> s# X)
    (active# length cons(N, L) -> s# length L, s# active X -> s# X)
    (and#(active X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (and#(active X1, X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (and#(active X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(active X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (and#(X1, active X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (and#(X1, active X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (and#(X1, active X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(X1, active X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
    (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
    (active# length cons(N, L) -> mark# s length L, mark# cons(X1, X2) -> mark# X1)
    (active# length cons(N, L) -> mark# s length L, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (active# length cons(N, L) -> mark# s length L, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (active# length cons(N, L) -> mark# s length L, mark# and(X1, X2) -> mark# X1)
    (active# length cons(N, L) -> mark# s length L, mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# length cons(N, L) -> mark# s length L, mark# and(X1, X2) -> and#(mark X1, X2))
    (active# length cons(N, L) -> mark# s length L, mark# length X -> mark# X)
    (active# length cons(N, L) -> mark# s length L, mark# length X -> active# length mark X)
    (active# length cons(N, L) -> mark# s length L, mark# length X -> length# mark X)
    (active# length cons(N, L) -> mark# s length L, mark# s X -> mark# X)
    (active# length cons(N, L) -> mark# s length L, mark# s X -> active# s mark X)
    (active# length cons(N, L) -> mark# s length L, mark# s X -> s# mark X)
    (mark# length X -> active# length mark X, active# and(tt(), X) -> mark# X)
    (mark# length X -> active# length mark X, active# length cons(N, L) -> mark# s length L)
    (mark# length X -> active# length mark X, active# length cons(N, L) -> length# L)
    (mark# length X -> active# length mark X, active# length cons(N, L) -> s# length L)
    (mark# length X -> active# length mark X, active# length nil() -> mark# 0())
    (mark# and(X1, X2) -> and#(mark X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (mark# and(X1, X2) -> and#(mark X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (mark# and(X1, X2) -> and#(mark X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (mark# and(X1, X2) -> and#(mark X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (s# active X -> s# X, s# mark X -> s# X)
    (s# active X -> s# X, s# active X -> s# X)
    (length# active X -> length# X, length# mark X -> length# X)
    (length# active X -> length# X, length# active X -> length# X)
    (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (active# and(tt(), X) -> mark# X, mark# 0() -> active# 0())
    (active# and(tt(), X) -> mark# X, mark# zeros() -> active# zeros())
    (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
    (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
    (active# and(tt(), X) -> mark# X, mark# tt() -> active# tt())
    (active# and(tt(), X) -> mark# X, mark# length X -> mark# X)
    (active# and(tt(), X) -> mark# X, mark# length X -> active# length mark X)
    (active# and(tt(), X) -> mark# X, mark# length X -> length# mark X)
    (active# and(tt(), X) -> mark# X, mark# nil() -> active# nil())
    (active# and(tt(), X) -> mark# X, mark# s X -> mark# X)
    (active# and(tt(), X) -> mark# X, mark# s X -> active# s mark X)
    (active# and(tt(), X) -> mark# X, mark# s X -> s# mark X)
    (mark# length X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# length X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# length X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# length X -> mark# X, mark# 0() -> active# 0())
    (mark# length X -> mark# X, mark# zeros() -> active# zeros())
    (mark# length X -> mark# X, mark# and(X1, X2) -> mark# X1)
    (mark# length X -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
    (mark# length X -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
    (mark# length X -> mark# X, mark# tt() -> active# tt())
    (mark# length X -> mark# X, mark# length X -> mark# X)
    (mark# length X -> mark# X, mark# length X -> active# length mark X)
    (mark# length X -> mark# X, mark# length X -> length# mark X)
    (mark# length X -> mark# X, mark# nil() -> active# nil())
    (mark# length X -> mark# X, mark# s X -> mark# X)
    (mark# length X -> mark# X, mark# s X -> active# s mark X)
    (mark# length X -> mark# X, mark# s X -> s# mark X)
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# and(tt(), X) -> mark# X)
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# length cons(N, L) -> mark# s length L)
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# length cons(N, L) -> length# L)
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# length cons(N, L) -> s# length L)
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# length nil() -> mark# 0())
    (active# length nil() -> mark# 0(), mark# 0() -> active# 0())
    (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
    (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
    (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
    (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
    (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> active# zeros())
    (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
    (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2))
    (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
    (mark# cons(X1, X2) -> mark# X1, mark# tt() -> active# tt())
    (mark# cons(X1, X2) -> mark# X1, mark# length X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# length X -> active# length mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# length X -> length# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil())
    (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
   }
   STATUS:
    arrows: 0.857959
    SCCS (5):
     Scc:
      {       mark# cons(X1, X2) -> mark# X1,
              mark# cons(X1, X2) -> active# cons(mark X1, X2),
                   mark# zeros() -> active# zeros(),
               mark# and(X1, X2) -> mark# X1,
               mark# and(X1, X2) -> active# and(mark X1, X2),
                  mark# length X -> mark# X,
                  mark# length X -> active# length mark X,
                       mark# s X -> mark# X,
                       mark# s X -> active# s mark X,
                 active# zeros() -> mark# cons(0(), zeros()),
            active# and(tt(), X) -> mark# X,
       active# length cons(N, L) -> mark# s length L}
     Scc:
      {  s# mark X -> s# X,
       s# active X -> s# X}
     Scc:
      {  length# mark X -> length# X,
       length# active X -> length# X}
     Scc:
      {  and#(X1, mark X2) -> and#(X1, X2),
       and#(X1, active X2) -> and#(X1, X2),
         and#(mark X1, X2) -> and#(X1, X2),
       and#(active X1, X2) -> and#(X1, X2)}
     Scc:
      {  cons#(X1, mark X2) -> cons#(X1, X2),
       cons#(X1, active X2) -> cons#(X1, X2),
         cons#(mark X1, X2) -> cons#(X1, X2),
       cons#(active X1, X2) -> cons#(X1, X2)}
     
     SCC (12):
      Strict:
       {       mark# cons(X1, X2) -> mark# X1,
               mark# cons(X1, X2) -> active# cons(mark X1, X2),
                    mark# zeros() -> active# zeros(),
                mark# and(X1, X2) -> mark# X1,
                mark# and(X1, X2) -> active# and(mark X1, X2),
                   mark# length X -> mark# X,
                   mark# length X -> active# length mark X,
                        mark# s X -> mark# X,
                        mark# s X -> active# s mark X,
                  active# zeros() -> mark# cons(0(), zeros()),
             active# and(tt(), X) -> mark# X,
        active# length cons(N, L) -> mark# s length L}
      Weak:
      {       mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark 0() -> active 0(),
                   mark zeros() -> active zeros(),
               mark and(X1, X2) -> active and(mark X1, X2),
                      mark tt() -> active tt(),
                  mark length X -> active length mark X,
                     mark nil() -> active nil(),
                       mark s X -> active s mark X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
            active and(tt(), X) -> mark X,
       active length cons(N, L) -> mark s length L,
            active length nil() -> mark 0(),
               and(X1, mark X2) -> and(X1, X2),
             and(X1, active X2) -> and(X1, X2),
               and(mark X1, X2) -> and(X1, X2),
             and(active X1, X2) -> and(X1, X2),
                  length mark X -> length X,
                length active X -> length X,
                       s mark X -> s X,
                     s active X -> s X}
      Open
     
     
     
     
     
     SCC (2):
      Strict:
       {  s# mark X -> s# X,
        s# active X -> s# X}
      Weak:
      {       mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark 0() -> active 0(),
                   mark zeros() -> active zeros(),
               mark and(X1, X2) -> active and(mark X1, X2),
                      mark tt() -> active tt(),
                  mark length X -> active length mark X,
                     mark nil() -> active nil(),
                       mark s X -> active s mark X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
            active and(tt(), X) -> mark X,
       active length cons(N, L) -> mark s length L,
            active length nil() -> mark 0(),
               and(X1, mark X2) -> and(X1, X2),
             and(X1, active X2) -> and(X1, X2),
               and(mark X1, X2) -> and(X1, X2),
             and(active X1, X2) -> and(X1, X2),
                  length mark X -> length X,
                length active X -> length X,
                       s mark X -> s X,
                     s active X -> s X}
      Open
     
     SCC (2):
      Strict:
       {  length# mark X -> length# X,
        length# active X -> length# X}
      Weak:
      {       mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark 0() -> active 0(),
                   mark zeros() -> active zeros(),
               mark and(X1, X2) -> active and(mark X1, X2),
                      mark tt() -> active tt(),
                  mark length X -> active length mark X,
                     mark nil() -> active nil(),
                       mark s X -> active s mark X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
            active and(tt(), X) -> mark X,
       active length cons(N, L) -> mark s length L,
            active length nil() -> mark 0(),
               and(X1, mark X2) -> and(X1, X2),
             and(X1, active X2) -> and(X1, X2),
               and(mark X1, X2) -> and(X1, X2),
             and(active X1, X2) -> and(X1, X2),
                  length mark X -> length X,
                length active X -> length X,
                       s mark X -> s X,
                     s active X -> s X}
      Open
     
     
     SCC (4):
      Strict:
       {  and#(X1, mark X2) -> and#(X1, X2),
        and#(X1, active X2) -> and#(X1, X2),
          and#(mark X1, X2) -> and#(X1, X2),
        and#(active X1, X2) -> and#(X1, X2)}
      Weak:
      {       mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark 0() -> active 0(),
                   mark zeros() -> active zeros(),
               mark and(X1, X2) -> active and(mark X1, X2),
                      mark tt() -> active tt(),
                  mark length X -> active length mark X,
                     mark nil() -> active nil(),
                       mark s X -> active s mark X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
            active and(tt(), X) -> mark X,
       active length cons(N, L) -> mark s length L,
            active length nil() -> mark 0(),
               and(X1, mark X2) -> and(X1, X2),
             and(X1, active X2) -> and(X1, X2),
               and(mark X1, X2) -> and(X1, X2),
             and(active X1, X2) -> and(X1, X2),
                  length mark X -> length X,
                length active X -> length X,
                       s mark X -> s X,
                     s active X -> s X}
      Open
     
     
     
     SCC (4):
      Strict:
       {  cons#(X1, mark X2) -> cons#(X1, X2),
        cons#(X1, active X2) -> cons#(X1, X2),
          cons#(mark X1, X2) -> cons#(X1, X2),
        cons#(active X1, X2) -> cons#(X1, X2)}
      Weak:
      {       mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark 0() -> active 0(),
                   mark zeros() -> active zeros(),
               mark and(X1, X2) -> active and(mark X1, X2),
                      mark tt() -> active tt(),
                  mark length X -> active length mark X,
                     mark nil() -> active nil(),
                       mark s X -> active s mark X,
              cons(X1, mark X2) -> cons(X1, X2),
            cons(X1, active X2) -> cons(X1, X2),
              cons(mark X1, X2) -> cons(X1, X2),
            cons(active X1, X2) -> cons(X1, X2),
                 active zeros() -> mark cons(0(), zeros()),
            active and(tt(), X) -> mark X,
       active length cons(N, L) -> mark s length L,
            active length nil() -> mark 0(),
               and(X1, mark X2) -> and(X1, X2),
             and(X1, active X2) -> and(X1, X2),
               and(mark X1, X2) -> and(X1, X2),
             and(active X1, X2) -> and(X1, X2),
                  length mark X -> length X,
                length active X -> length X,
                       s mark X -> s X,
                     s active X -> s X}
      Open