MAYBE
Time: 1.072504
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,
              mark take(X1, X2) -> active take(mark X1, mark X2),
              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(),
           active take(0(), IL) -> mark nil(),
  active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
               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,
              take(X1, mark X2) -> take(X1, X2),
            take(X1, active X2) -> take(X1, X2),
              take(mark X1, X2) -> take(X1, X2),
            take(active X1, X2) -> take(X1, X2)}
 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,
                mark# take(X1, X2) -> mark# X1,
                mark# take(X1, X2) -> mark# X2,
                mark# take(X1, X2) -> active# take(mark X1, mark X2),
                mark# take(X1, X2) -> take#(mark X1, mark X2),
                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(),
             active# take(0(), IL) -> mark# nil(),
    active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)),
    active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)),
    active# take(s M, cons(N, IL)) -> take#(M, IL),
                 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,
                take#(X1, mark X2) -> take#(X1, X2),
              take#(X1, active X2) -> take#(X1, X2),
                take#(mark X1, X2) -> take#(X1, X2),
              take#(active X1, X2) -> take#(X1, X2)}
  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,
               mark take(X1, X2) -> active take(mark X1, mark X2),
               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(),
            active take(0(), IL) -> mark nil(),
   active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
                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,
               take(X1, mark X2) -> take(X1, X2),
             take(X1, active X2) -> take(X1, X2),
               take(mark X1, X2) -> take(X1, X2),
             take(active X1, X2) -> take(X1, X2)}
  UR:
   {            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,
                mark take(X1, X2) -> active take(mark X1, mark X2),
                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(),
             active take(0(), IL) -> mark nil(),
    active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
                 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,
                take(X1, mark X2) -> take(X1, X2),
              take(X1, active X2) -> take(X1, X2),
                take(mark X1, X2) -> take(X1, X2),
              take(active X1, X2) -> take(X1, X2)}
   EDG:
    {
     (mark# length X -> length# mark X, length# active X -> length# X)
     (mark# length X -> length# mark X, length# mark X -> length# X)
     (mark# take(X1, X2) -> take#(mark X1, mark X2), take#(active X1, X2) -> take#(X1, X2))
     (mark# take(X1, X2) -> take#(mark X1, mark X2), take#(mark X1, X2) -> take#(X1, X2))
     (mark# take(X1, X2) -> take#(mark X1, mark X2), take#(X1, active X2) -> take#(X1, X2))
     (mark# take(X1, X2) -> take#(mark X1, mark X2), take#(X1, mark X2) -> take#(X1, X2))
     (mark# and(X1, X2) -> and#(mark X1, X2), and#(active X1, 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#(X1, active X2) -> and#(X1, X2))
     (mark# and(X1, X2) -> and#(mark X1, X2), and#(X1, mark X2) -> and#(X1, X2))
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s M, cons(N, IL)) -> take#(M, IL))
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(0(), IL) -> mark# nil())
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length nil() -> mark# 0())
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length cons(N, L) -> s# length L)
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length cons(N, L) -> length# L)
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length cons(N, L) -> mark# s length L)
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# and(tt(), X) -> mark# X)
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# zeros() -> cons#(0(), zeros()))
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# zeros() -> mark# cons(0(), zeros()))
     (active# zeros() -> cons#(0(), zeros()), cons#(active X1, X2) -> cons#(X1, X2))
     (active# zeros() -> cons#(0(), zeros()), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# zeros() -> cons#(0(), zeros()), cons#(X1, active X2) -> cons#(X1, X2))
     (active# zeros() -> cons#(0(), zeros()), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, 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#(X1, active X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, 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#(X1, active X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (and#(X1, active X2) -> and#(X1, X2), and#(active X1, 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#(X1, active X2) -> and#(X1, X2))
     (and#(X1, active X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
     (and#(active X1, X2) -> and#(X1, X2), and#(active X1, 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#(X1, active X2) -> and#(X1, X2))
     (and#(active X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
     (take#(X1, active X2) -> take#(X1, X2), take#(active X1, X2) -> take#(X1, X2))
     (take#(X1, active X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
     (take#(X1, active X2) -> take#(X1, X2), take#(X1, active X2) -> take#(X1, X2))
     (take#(X1, active X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
     (take#(active X1, X2) -> take#(X1, X2), take#(active X1, X2) -> take#(X1, X2))
     (take#(active X1, X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
     (take#(active X1, X2) -> take#(X1, X2), take#(X1, active X2) -> take#(X1, X2))
     (take#(active X1, X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
     (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> take#(mark X1, mark X2))
     (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (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)
     (active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)), cons#(active X1, X2) -> cons#(X1, X2))
     (active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)), cons#(X1, active X2) -> cons#(X1, X2))
     (active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)), cons#(X1, mark X2) -> cons#(X1, X2))
     (mark# s X -> active# s mark X, active# take(s M, cons(N, IL)) -> take#(M, IL))
     (mark# s X -> active# s mark X, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
     (mark# s X -> active# s mark X, active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
     (mark# s X -> active# s mark X, active# take(0(), IL) -> mark# nil())
     (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)
     (mark# s X -> active# s mark X, active# zeros() -> cons#(0(), zeros()))
     (mark# s X -> active# s mark X, active# zeros() -> mark# cons(0(), zeros()))
     (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# and(X1, X2) -> active# and(mark X1, X2), active# take(s M, cons(N, IL)) -> take#(M, IL))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# take(0(), IL) -> mark# nil())
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# length nil() -> mark# 0())
     (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 cons(N, L) -> length# L)
     (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# and(tt(), X) -> mark# X)
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# zeros() -> cons#(0(), zeros()))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# zeros() -> mark# cons(0(), zeros()))
     (mark# length X -> mark# X, mark# take(X1, X2) -> take#(mark X1, mark X2))
     (mark# length X -> mark# X, mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X2)
     (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X1)
     (mark# length X -> mark# X, mark# s X -> s# mark X)
     (mark# length X -> mark# X, mark# s X -> active# s mark X)
     (mark# length X -> mark# X, mark# s X -> mark# X)
     (mark# length X -> mark# X, mark# nil() -> active# nil())
     (mark# length X -> mark# X, mark# length X -> length# mark X)
     (mark# length X -> mark# X, mark# length X -> active# length mark X)
     (mark# length X -> mark# X, mark# length X -> mark# X)
     (mark# length X -> mark# X, mark# tt() -> active# tt())
     (mark# length X -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
     (mark# length X -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
     (mark# length X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# length X -> mark# X, mark# zeros() -> active# zeros())
     (mark# length X -> mark# X, mark# 0() -> active# 0())
     (mark# length X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# length X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# length X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (active# and(tt(), X) -> mark# X, mark# take(X1, X2) -> take#(mark X1, mark X2))
     (active# and(tt(), X) -> mark# X, mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (active# and(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X2)
     (active# and(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X1)
     (active# and(tt(), X) -> mark# X, mark# s X -> s# mark X)
     (active# and(tt(), X) -> mark# X, mark# s X -> active# s mark X)
     (active# and(tt(), X) -> mark# X, mark# s X -> mark# X)
     (active# and(tt(), X) -> mark# X, mark# nil() -> active# nil())
     (active# and(tt(), X) -> mark# X, mark# length X -> length# mark X)
     (active# and(tt(), X) -> mark# X, mark# length X -> active# length mark X)
     (active# and(tt(), X) -> mark# X, mark# length X -> mark# X)
     (active# and(tt(), X) -> mark# X, mark# tt() -> active# tt())
     (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
     (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) -> mark# X1)
     (active# and(tt(), X) -> mark# X, mark# zeros() -> active# zeros())
     (active# and(tt(), X) -> mark# X, mark# 0() -> active# 0())
     (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (length# active X -> length# X, length# active X -> length# X)
     (length# active X -> length# X, length# mark X -> length# X)
     (s# active X -> s# X, s# active X -> s# X)
     (s# active X -> s# X, s# mark X -> s# X)
     (mark# zeros() -> active# zeros(), active# take(s M, cons(N, IL)) -> take#(M, IL))
     (mark# zeros() -> active# zeros(), active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
     (mark# zeros() -> active# zeros(), active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
     (mark# zeros() -> active# zeros(), active# take(0(), IL) -> mark# nil())
     (mark# zeros() -> active# zeros(), active# length nil() -> mark# 0())
     (mark# zeros() -> active# zeros(), active# length cons(N, L) -> s# length L)
     (mark# zeros() -> active# zeros(), active# length cons(N, L) -> length# L)
     (mark# zeros() -> active# zeros(), active# length cons(N, L) -> mark# s length L)
     (mark# zeros() -> active# zeros(), active# and(tt(), X) -> mark# X)
     (mark# zeros() -> active# zeros(), active# zeros() -> cons#(0(), zeros()))
     (mark# zeros() -> active# zeros(), active# zeros() -> mark# cons(0(), zeros()))
     (mark# nil() -> active# nil(), active# take(s M, cons(N, IL)) -> take#(M, IL))
     (mark# nil() -> active# nil(), active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
     (mark# nil() -> active# nil(), active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
     (mark# nil() -> active# nil(), active# take(0(), IL) -> mark# nil())
     (mark# nil() -> active# nil(), active# length nil() -> mark# 0())
     (mark# nil() -> active# nil(), active# length cons(N, L) -> s# length L)
     (mark# nil() -> active# nil(), active# length cons(N, L) -> length# L)
     (mark# nil() -> active# nil(), active# length cons(N, L) -> mark# s length L)
     (mark# nil() -> active# nil(), active# and(tt(), X) -> mark# X)
     (mark# nil() -> active# nil(), active# zeros() -> cons#(0(), zeros()))
     (mark# nil() -> active# nil(), active# zeros() -> mark# cons(0(), zeros()))
     (active# take(0(), IL) -> mark# nil(), mark# take(X1, X2) -> take#(mark X1, mark X2))
     (active# take(0(), IL) -> mark# nil(), mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (active# take(0(), IL) -> mark# nil(), mark# take(X1, X2) -> mark# X2)
     (active# take(0(), IL) -> mark# nil(), mark# take(X1, X2) -> mark# X1)
     (active# take(0(), IL) -> mark# nil(), mark# s X -> s# mark X)
     (active# take(0(), IL) -> mark# nil(), mark# s X -> active# s mark X)
     (active# take(0(), IL) -> mark# nil(), mark# s X -> mark# X)
     (active# take(0(), IL) -> mark# nil(), mark# nil() -> active# nil())
     (active# take(0(), IL) -> mark# nil(), mark# length X -> length# mark X)
     (active# take(0(), IL) -> mark# nil(), mark# length X -> active# length mark X)
     (active# take(0(), IL) -> mark# nil(), mark# length X -> mark# X)
     (active# take(0(), IL) -> mark# nil(), mark# tt() -> active# tt())
     (active# take(0(), IL) -> mark# nil(), mark# and(X1, X2) -> and#(mark X1, X2))
     (active# take(0(), IL) -> mark# nil(), mark# and(X1, X2) -> active# and(mark X1, X2))
     (active# take(0(), IL) -> mark# nil(), mark# and(X1, X2) -> mark# X1)
     (active# take(0(), IL) -> mark# nil(), mark# zeros() -> active# zeros())
     (active# take(0(), IL) -> mark# nil(), mark# 0() -> active# 0())
     (active# take(0(), IL) -> mark# nil(), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# take(0(), IL) -> mark# nil(), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# take(0(), IL) -> mark# nil(), mark# cons(X1, X2) -> mark# X1)
     (active# take(s M, cons(N, IL)) -> take#(M, IL), take#(X1, mark X2) -> take#(X1, X2))
     (active# take(s M, cons(N, IL)) -> take#(M, IL), take#(X1, active X2) -> take#(X1, X2))
     (active# take(s M, cons(N, IL)) -> take#(M, IL), take#(mark X1, X2) -> take#(X1, X2))
     (active# take(s M, cons(N, IL)) -> take#(M, IL), take#(active X1, X2) -> take#(X1, X2))
     (active# length nil() -> mark# 0(), mark# cons(X1, X2) -> mark# X1)
     (active# length nil() -> mark# 0(), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# length nil() -> mark# 0(), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# length nil() -> mark# 0(), mark# 0() -> active# 0())
     (active# length nil() -> mark# 0(), mark# zeros() -> active# zeros())
     (active# length nil() -> mark# 0(), mark# and(X1, X2) -> mark# X1)
     (active# length nil() -> mark# 0(), mark# and(X1, X2) -> active# and(mark X1, X2))
     (active# length nil() -> mark# 0(), mark# and(X1, X2) -> and#(mark X1, X2))
     (active# length nil() -> mark# 0(), mark# tt() -> active# tt())
     (active# length nil() -> mark# 0(), mark# length X -> mark# X)
     (active# length nil() -> mark# 0(), mark# length X -> active# length mark X)
     (active# length nil() -> mark# 0(), mark# length X -> length# mark X)
     (active# length nil() -> mark# 0(), mark# nil() -> active# nil())
     (active# length nil() -> mark# 0(), mark# s X -> mark# X)
     (active# length nil() -> mark# 0(), mark# s X -> active# s mark X)
     (active# length nil() -> mark# 0(), mark# s X -> s# mark X)
     (active# length nil() -> mark# 0(), mark# take(X1, X2) -> mark# X1)
     (active# length nil() -> mark# 0(), mark# take(X1, X2) -> mark# X2)
     (active# length nil() -> mark# 0(), mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (active# length nil() -> mark# 0(), mark# take(X1, X2) -> take#(mark X1, mark X2))
     (mark# tt() -> active# tt(), active# zeros() -> mark# cons(0(), zeros()))
     (mark# tt() -> active# tt(), active# zeros() -> cons#(0(), zeros()))
     (mark# tt() -> active# tt(), active# and(tt(), X) -> mark# X)
     (mark# tt() -> active# tt(), active# length cons(N, L) -> mark# s length L)
     (mark# tt() -> active# tt(), active# length cons(N, L) -> length# L)
     (mark# tt() -> active# tt(), active# length cons(N, L) -> s# length L)
     (mark# tt() -> active# tt(), active# length nil() -> mark# 0())
     (mark# tt() -> active# tt(), active# take(0(), IL) -> mark# nil())
     (mark# tt() -> active# tt(), active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
     (mark# tt() -> active# tt(), active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
     (mark# tt() -> active# tt(), active# take(s M, cons(N, IL)) -> take#(M, IL))
     (mark# 0() -> active# 0(), active# zeros() -> mark# cons(0(), zeros()))
     (mark# 0() -> active# 0(), active# zeros() -> cons#(0(), zeros()))
     (mark# 0() -> active# 0(), active# and(tt(), X) -> mark# X)
     (mark# 0() -> active# 0(), active# length cons(N, L) -> mark# s length L)
     (mark# 0() -> active# 0(), active# length cons(N, L) -> length# L)
     (mark# 0() -> active# 0(), active# length cons(N, L) -> s# length L)
     (mark# 0() -> active# 0(), active# length nil() -> mark# 0())
     (mark# 0() -> active# 0(), active# take(0(), IL) -> mark# nil())
     (mark# 0() -> active# 0(), active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
     (mark# 0() -> active# 0(), active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
     (mark# 0() -> active# 0(), active# take(s M, cons(N, IL)) -> take#(M, IL))
     (s# mark X -> s# X, s# mark X -> s# X)
     (s# mark X -> s# X, s# active X -> s# X)
     (length# mark X -> length# X, length# mark X -> length# X)
     (length# mark X -> length# X, length# active X -> length# X)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# s X -> mark# X, mark# 0() -> active# 0())
     (mark# s X -> mark# X, mark# zeros() -> active# zeros())
     (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
     (mark# s X -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
     (mark# s X -> mark# X, mark# tt() -> active# tt())
     (mark# s X -> mark# X, mark# length X -> mark# X)
     (mark# s X -> mark# X, mark# length X -> active# length mark X)
     (mark# s X -> mark# X, mark# length X -> length# mark X)
     (mark# s X -> mark# X, mark# nil() -> active# nil())
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# s X -> active# s mark X)
     (mark# s X -> mark# X, mark# s X -> s# mark X)
     (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (mark# s X -> mark# X, mark# take(X1, X2) -> take#(mark X1, mark X2))
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# cons(X1, X2) -> mark# X1)
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# 0() -> active# 0())
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# zeros() -> active# zeros())
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# and(X1, X2) -> mark# X1)
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# and(X1, X2) -> active# and(mark X1, X2))
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# and(X1, X2) -> and#(mark X1, X2))
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# tt() -> active# tt())
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# length X -> mark# X)
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# length X -> active# length mark X)
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# length X -> length# mark X)
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# nil() -> active# nil())
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# s X -> mark# X)
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# s X -> active# s mark X)
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# s X -> s# mark X)
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# take(X1, X2) -> mark# X1)
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# take(X1, X2) -> mark# X2)
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# take(X1, X2) -> take#(mark X1, mark X2))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# zeros() -> mark# cons(0(), zeros()))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# zeros() -> cons#(0(), zeros()))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# and(tt(), X) -> mark# X)
     (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# length cons(N, L) -> length# L)
     (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 nil() -> mark# 0())
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# take(0(), IL) -> mark# nil())
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
     (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# take(s M, cons(N, IL)) -> take#(M, IL))
     (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# 0() -> active# 0())
     (active# length cons(N, L) -> mark# s length L, mark# zeros() -> active# zeros())
     (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# tt() -> active# tt())
     (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# nil() -> active# nil())
     (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)
     (active# length cons(N, L) -> mark# s length L, mark# take(X1, X2) -> mark# X1)
     (active# length cons(N, L) -> mark# s length L, mark# take(X1, X2) -> mark# X2)
     (active# length cons(N, L) -> mark# s length L, mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (active# length cons(N, L) -> mark# s length L, mark# take(X1, X2) -> take#(mark X1, mark X2))
     (mark# length X -> active# length mark X, active# zeros() -> mark# cons(0(), zeros()))
     (mark# length X -> active# length mark X, active# zeros() -> cons#(0(), zeros()))
     (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# length X -> active# length mark X, active# take(0(), IL) -> mark# nil())
     (mark# length X -> active# length mark X, active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
     (mark# length X -> active# length mark X, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
     (mark# length X -> active# length mark X, active# take(s M, cons(N, IL)) -> take#(M, IL))
     (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# take(X1, X2) -> mark# X1, mark# 0() -> active# 0())
     (mark# take(X1, X2) -> mark# X1, mark# zeros() -> active# zeros())
     (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2))
     (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
     (mark# take(X1, X2) -> mark# X1, mark# tt() -> active# tt())
     (mark# take(X1, X2) -> mark# X1, mark# length X -> mark# X)
     (mark# take(X1, X2) -> mark# X1, mark# length X -> active# length mark X)
     (mark# take(X1, X2) -> mark# X1, mark# length X -> length# mark X)
     (mark# take(X1, X2) -> mark# X1, mark# nil() -> active# nil())
     (mark# take(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# take(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# take(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> take#(mark X1, mark X2))
     (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)
     (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> take#(mark X1, mark X2))
     (take#(mark X1, X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
     (take#(mark X1, X2) -> take#(X1, X2), take#(X1, active X2) -> take#(X1, X2))
     (take#(mark X1, X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
     (take#(mark X1, X2) -> take#(X1, X2), take#(active X1, X2) -> take#(X1, X2))
     (take#(X1, mark X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
     (take#(X1, mark X2) -> take#(X1, X2), take#(X1, active X2) -> take#(X1, X2))
     (take#(X1, mark X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
     (take#(X1, mark X2) -> take#(X1, X2), take#(active X1, X2) -> take#(X1, X2))
     (and#(mark X1, X2) -> and#(X1, X2), and#(X1, mark 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#(mark X1, X2) -> and#(X1, X2))
     (and#(mark X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
     (and#(X1, mark X2) -> and#(X1, X2), and#(X1, mark 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#(mark X1, X2) -> and#(X1, X2))
     (and#(X1, mark X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> mark# X1)
     (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# zeros() -> mark# cons(0(), zeros()), mark# 0() -> active# 0())
     (active# zeros() -> mark# cons(0(), zeros()), mark# zeros() -> active# zeros())
     (active# zeros() -> mark# cons(0(), zeros()), mark# and(X1, X2) -> mark# X1)
     (active# zeros() -> mark# cons(0(), zeros()), mark# and(X1, X2) -> active# and(mark X1, X2))
     (active# zeros() -> mark# cons(0(), zeros()), mark# and(X1, X2) -> and#(mark X1, X2))
     (active# zeros() -> mark# cons(0(), zeros()), mark# tt() -> active# tt())
     (active# zeros() -> mark# cons(0(), zeros()), mark# length X -> mark# X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# length X -> active# length mark X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# length X -> length# mark X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# nil() -> active# nil())
     (active# zeros() -> mark# cons(0(), zeros()), mark# s X -> mark# X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# s X -> active# s mark X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# s X -> s# mark X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# take(X1, X2) -> mark# X1)
     (active# zeros() -> mark# cons(0(), zeros()), mark# take(X1, X2) -> mark# X2)
     (active# zeros() -> mark# cons(0(), zeros()), mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (active# zeros() -> mark# cons(0(), zeros()), mark# take(X1, X2) -> take#(mark X1, mark X2))
     (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# take(X1, X2) -> mark# X2, mark# 0() -> active# 0())
     (mark# take(X1, X2) -> mark# X2, mark# zeros() -> active# zeros())
     (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> active# and(mark X1, X2))
     (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> and#(mark X1, X2))
     (mark# take(X1, X2) -> mark# X2, mark# tt() -> active# tt())
     (mark# take(X1, X2) -> mark# X2, mark# length X -> mark# X)
     (mark# take(X1, X2) -> mark# X2, mark# length X -> active# length mark X)
     (mark# take(X1, X2) -> mark# X2, mark# length X -> length# mark X)
     (mark# take(X1, X2) -> mark# X2, mark# nil() -> active# nil())
     (mark# take(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# take(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
     (mark# take(X1, X2) -> mark# X2, mark# s X -> s# mark X)
     (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2)
     (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> take#(mark X1, mark X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (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)
    }
    EDG:
     {
      (mark# length X -> length# mark X, length# active X -> length# X)
      (mark# length X -> length# mark X, length# mark X -> length# X)
      (mark# take(X1, X2) -> take#(mark X1, mark X2), take#(active X1, X2) -> take#(X1, X2))
      (mark# take(X1, X2) -> take#(mark X1, mark X2), take#(mark X1, X2) -> take#(X1, X2))
      (mark# take(X1, X2) -> take#(mark X1, mark X2), take#(X1, active X2) -> take#(X1, X2))
      (mark# take(X1, X2) -> take#(mark X1, mark X2), take#(X1, mark X2) -> take#(X1, X2))
      (mark# and(X1, X2) -> and#(mark X1, X2), and#(active X1, X2) -> and#(X1, X2))
      (mark# and(X1, X2) -> and#(mark X1, X2), and#(mark X1, X2) -> and#(X1, X2))
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s M, cons(N, IL)) -> take#(M, IL))
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(0(), IL) -> mark# nil())
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length nil() -> mark# 0())
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length cons(N, L) -> s# length L)
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length cons(N, L) -> length# L)
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length cons(N, L) -> mark# s length L)
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# and(tt(), X) -> mark# X)
      (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, 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#(X1, active X2) -> cons#(X1, X2))
      (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
      (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, 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#(X1, active X2) -> cons#(X1, X2))
      (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
      (and#(X1, active X2) -> and#(X1, X2), and#(active X1, 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#(X1, active X2) -> and#(X1, X2))
      (and#(X1, active X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
      (and#(active X1, X2) -> and#(X1, X2), and#(active X1, 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#(X1, active X2) -> and#(X1, X2))
      (and#(active X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
      (take#(X1, active X2) -> take#(X1, X2), take#(active X1, X2) -> take#(X1, X2))
      (take#(X1, active X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
      (take#(X1, active X2) -> take#(X1, X2), take#(X1, active X2) -> take#(X1, X2))
      (take#(X1, active X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
      (take#(active X1, X2) -> take#(X1, X2), take#(active X1, X2) -> take#(X1, X2))
      (take#(active X1, X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
      (take#(active X1, X2) -> take#(X1, X2), take#(X1, active X2) -> take#(X1, X2))
      (take#(active X1, X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
      (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> take#(mark X1, mark X2))
      (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
      (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
      (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)
      (active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)), cons#(X1, active X2) -> cons#(X1, X2))
      (active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)), cons#(X1, mark X2) -> cons#(X1, X2))
      (mark# s X -> active# s mark X, active# take(s M, cons(N, IL)) -> take#(M, IL))
      (mark# s X -> active# s mark X, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
      (mark# s X -> active# s mark X, active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
      (mark# s X -> active# s mark X, active# take(0(), IL) -> mark# nil())
      (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)
      (mark# and(X1, X2) -> active# and(mark X1, X2), active# take(s M, cons(N, IL)) -> take#(M, IL))
      (mark# and(X1, X2) -> active# and(mark X1, X2), active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
      (mark# and(X1, X2) -> active# and(mark X1, X2), active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
      (mark# and(X1, X2) -> active# and(mark X1, X2), active# take(0(), IL) -> mark# nil())
      (mark# and(X1, X2) -> active# and(mark X1, X2), active# length nil() -> mark# 0())
      (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 cons(N, L) -> length# L)
      (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# and(tt(), X) -> mark# X)
      (mark# length X -> mark# X, mark# take(X1, X2) -> take#(mark X1, mark X2))
      (mark# length X -> mark# X, mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X2)
      (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X1)
      (mark# length X -> mark# X, mark# s X -> s# mark X)
      (mark# length X -> mark# X, mark# s X -> active# s mark X)
      (mark# length X -> mark# X, mark# s X -> mark# X)
      (mark# length X -> mark# X, mark# nil() -> active# nil())
      (mark# length X -> mark# X, mark# length X -> length# mark X)
      (mark# length X -> mark# X, mark# length X -> active# length mark X)
      (mark# length X -> mark# X, mark# length X -> mark# X)
      (mark# length X -> mark# X, mark# tt() -> active# tt())
      (mark# length X -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
      (mark# length X -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
      (mark# length X -> mark# X, mark# and(X1, X2) -> mark# X1)
      (mark# length X -> mark# X, mark# zeros() -> active# zeros())
      (mark# length X -> mark# X, mark# 0() -> active# 0())
      (mark# length X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# length X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# length X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (active# and(tt(), X) -> mark# X, mark# take(X1, X2) -> take#(mark X1, mark X2))
      (active# and(tt(), X) -> mark# X, mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (active# and(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X2)
      (active# and(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X1)
      (active# and(tt(), X) -> mark# X, mark# s X -> s# mark X)
      (active# and(tt(), X) -> mark# X, mark# s X -> active# s mark X)
      (active# and(tt(), X) -> mark# X, mark# s X -> mark# X)
      (active# and(tt(), X) -> mark# X, mark# nil() -> active# nil())
      (active# and(tt(), X) -> mark# X, mark# length X -> length# mark X)
      (active# and(tt(), X) -> mark# X, mark# length X -> active# length mark X)
      (active# and(tt(), X) -> mark# X, mark# length X -> mark# X)
      (active# and(tt(), X) -> mark# X, mark# tt() -> active# tt())
      (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
      (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) -> mark# X1)
      (active# and(tt(), X) -> mark# X, mark# zeros() -> active# zeros())
      (active# and(tt(), X) -> mark# X, mark# 0() -> active# 0())
      (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (active# and(tt(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (length# active X -> length# X, length# active X -> length# X)
      (length# active X -> length# X, length# mark X -> length# X)
      (s# active X -> s# X, s# active X -> s# X)
      (s# active X -> s# X, s# mark X -> s# X)
      (mark# zeros() -> active# zeros(), active# zeros() -> cons#(0(), zeros()))
      (mark# zeros() -> active# zeros(), active# zeros() -> mark# cons(0(), zeros()))
      (active# take(0(), IL) -> mark# nil(), mark# nil() -> active# nil())
      (active# length nil() -> mark# 0(), mark# 0() -> active# 0())
      (s# mark X -> s# X, s# mark X -> s# X)
      (s# mark X -> s# X, s# active X -> s# X)
      (length# mark X -> length# X, length# mark X -> length# X)
      (length# mark X -> length# X, length# active X -> length# X)
      (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# s X -> mark# X, mark# 0() -> active# 0())
      (mark# s X -> mark# X, mark# zeros() -> active# zeros())
      (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
      (mark# s X -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
      (mark# s X -> mark# X, mark# tt() -> active# tt())
      (mark# s X -> mark# X, mark# length X -> mark# X)
      (mark# s X -> mark# X, mark# length X -> active# length mark X)
      (mark# s X -> mark# X, mark# length X -> length# mark X)
      (mark# s X -> mark# X, mark# nil() -> active# nil())
      (mark# s X -> mark# X, mark# s X -> mark# X)
      (mark# s X -> mark# X, mark# s X -> active# s mark X)
      (mark# s X -> mark# X, mark# s X -> s# mark X)
      (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X2)
      (mark# s X -> mark# X, mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (mark# s X -> mark# X, mark# take(X1, X2) -> take#(mark X1, mark X2))
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# cons(X1, X2) -> mark# X1)
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# cons(X1, X2) -> cons#(mark X1, X2))
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# and(X1, X2) -> mark# X1)
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# and(X1, X2) -> active# and(mark X1, X2))
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# and(X1, X2) -> and#(mark X1, X2))
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# length X -> mark# X)
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# length X -> active# length mark X)
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# length X -> length# mark X)
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# s X -> mark# X)
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# s X -> active# s mark X)
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# s X -> s# mark X)
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# take(X1, X2) -> mark# X1)
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# take(X1, X2) -> mark# X2)
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)), mark# take(X1, X2) -> take#(mark X1, mark X2))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# and(tt(), X) -> mark# X)
      (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# length cons(N, L) -> length# L)
      (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 nil() -> mark# 0())
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# take(0(), IL) -> mark# nil())
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
      (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# take(s M, cons(N, IL)) -> take#(M, IL))
      (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)
      (active# length cons(N, L) -> mark# s length L, mark# take(X1, X2) -> mark# X1)
      (active# length cons(N, L) -> mark# s length L, mark# take(X1, X2) -> mark# X2)
      (active# length cons(N, L) -> mark# s length L, mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (active# length cons(N, L) -> mark# s length L, mark# take(X1, X2) -> take#(mark X1, mark X2))
      (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# length X -> active# length mark X, active# take(0(), IL) -> mark# nil())
      (mark# length X -> active# length mark X, active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL)))
      (mark# length X -> active# length mark X, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
      (mark# length X -> active# length mark X, active# take(s M, cons(N, IL)) -> take#(M, IL))
      (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# take(X1, X2) -> mark# X1, mark# 0() -> active# 0())
      (mark# take(X1, X2) -> mark# X1, mark# zeros() -> active# zeros())
      (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
      (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2))
      (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
      (mark# take(X1, X2) -> mark# X1, mark# tt() -> active# tt())
      (mark# take(X1, X2) -> mark# X1, mark# length X -> mark# X)
      (mark# take(X1, X2) -> mark# X1, mark# length X -> active# length mark X)
      (mark# take(X1, X2) -> mark# X1, mark# length X -> length# mark X)
      (mark# take(X1, X2) -> mark# X1, mark# nil() -> active# nil())
      (mark# take(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# take(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
      (mark# take(X1, X2) -> mark# X1, mark# s X -> s# mark X)
      (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
      (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
      (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> take#(mark X1, mark X2))
      (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)
      (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
      (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> take#(mark X1, mark X2))
      (take#(mark X1, X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
      (take#(mark X1, X2) -> take#(X1, X2), take#(X1, active X2) -> take#(X1, X2))
      (take#(mark X1, X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
      (take#(mark X1, X2) -> take#(X1, X2), take#(active X1, X2) -> take#(X1, X2))
      (take#(X1, mark X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
      (take#(X1, mark X2) -> take#(X1, X2), take#(X1, active X2) -> take#(X1, X2))
      (take#(X1, mark X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
      (take#(X1, mark X2) -> take#(X1, X2), take#(active X1, X2) -> take#(X1, X2))
      (and#(mark X1, X2) -> and#(X1, X2), and#(X1, mark 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#(mark X1, X2) -> and#(X1, X2))
      (and#(mark X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
      (and#(X1, mark X2) -> and#(X1, X2), and#(X1, mark 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#(mark X1, X2) -> and#(X1, X2))
      (and#(X1, mark X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
      (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2))
      (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
      (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2))
      (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
      (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> mark# X1)
      (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> cons#(mark X1, X2))
      (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
      (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2))
      (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2))
      (mark# take(X1, X2) -> mark# X2, mark# 0() -> active# 0())
      (mark# take(X1, X2) -> mark# X2, mark# zeros() -> active# zeros())
      (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
      (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> active# and(mark X1, X2))
      (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> and#(mark X1, X2))
      (mark# take(X1, X2) -> mark# X2, mark# tt() -> active# tt())
      (mark# take(X1, X2) -> mark# X2, mark# length X -> mark# X)
      (mark# take(X1, X2) -> mark# X2, mark# length X -> active# length mark X)
      (mark# take(X1, X2) -> mark# X2, mark# length X -> length# mark X)
      (mark# take(X1, X2) -> mark# X2, mark# nil() -> active# nil())
      (mark# take(X1, X2) -> mark# X2, mark# s X -> mark# X)
      (mark# take(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
      (mark# take(X1, X2) -> mark# X2, mark# s X -> s# mark X)
      (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1)
      (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2)
      (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> take#(mark X1, mark 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#(active X1, X2) -> cons#(X1, X2))
      (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)
     }
     STATUS:
      arrows: 0.869624
      SCCS (4):
       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,
                     mark# take(X1, X2) -> mark# X1,
                     mark# take(X1, X2) -> mark# X2,
                     mark# take(X1, X2) -> active# take(mark X1, mark X2),
                        active# zeros() -> mark# cons(0(), zeros()),
                   active# and(tt(), X) -> mark# X,
              active# length cons(N, L) -> mark# s length L,
         active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL))}
       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:
        {  take#(X1, mark X2) -> take#(X1, X2),
         take#(X1, active X2) -> take#(X1, X2),
           take#(mark X1, X2) -> take#(X1, X2),
         take#(active X1, X2) -> take#(X1, X2)}
       
       SCC (16):
        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,
                      mark# take(X1, X2) -> mark# X1,
                      mark# take(X1, X2) -> mark# X2,
                      mark# take(X1, X2) -> active# take(mark X1, mark X2),
                         active# zeros() -> mark# cons(0(), zeros()),
                    active# and(tt(), X) -> mark# X,
               active# length cons(N, L) -> mark# s length L,
          active# take(s M, cons(N, IL)) -> mark# cons(N, take(M, IL))}
        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,
                     mark take(X1, X2) -> active take(mark X1, mark X2),
                     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(),
                  active take(0(), IL) -> mark nil(),
         active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
                      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,
                     take(X1, mark X2) -> take(X1, X2),
                   take(X1, active X2) -> take(X1, X2),
                     take(mark X1, X2) -> take(X1, X2),
                   take(active X1, X2) -> take(X1, X2)}
        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,
                     mark take(X1, X2) -> active take(mark X1, mark X2),
                     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(),
                  active take(0(), IL) -> mark nil(),
         active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
                      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,
                     take(X1, mark X2) -> take(X1, X2),
                   take(X1, active X2) -> take(X1, X2),
                     take(mark X1, X2) -> take(X1, X2),
                   take(active X1, X2) -> take(X1, X2)}
        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,
                     mark take(X1, X2) -> active take(mark X1, mark X2),
                     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(),
                  active take(0(), IL) -> mark nil(),
         active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
                      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,
                     take(X1, mark X2) -> take(X1, X2),
                   take(X1, active X2) -> take(X1, X2),
                     take(mark X1, X2) -> take(X1, X2),
                   take(active X1, X2) -> take(X1, X2)}
        Open
       
       SCC (4):
        Strict:
         {  take#(X1, mark X2) -> take#(X1, X2),
          take#(X1, active X2) -> take#(X1, X2),
            take#(mark X1, X2) -> take#(X1, X2),
          take#(active X1, X2) -> take#(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,
                     mark take(X1, X2) -> active take(mark X1, mark X2),
                     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(),
                  active take(0(), IL) -> mark nil(),
         active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
                      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,
                     take(X1, mark X2) -> take(X1, X2),
                   take(X1, active X2) -> take(X1, X2),
                     take(mark X1, X2) -> take(X1, X2),
                   take(active X1, X2) -> take(X1, X2)}
        Open