MAYBE
Time: 0.085179
TRS:
 {                 mark true() -> active true(),
               mark eq(X1, X2) -> active eq(X1, X2),
                      mark 0() -> active 0(),
                      mark s X -> active s X,
                  mark false() -> active false(),
             mark cons(X1, X2) -> active cons(X1, X2),
                    mark inf X -> active inf mark X,
                    mark nil() -> active nil(),
             mark take(X1, X2) -> active take(mark X1, mark X2),
                 mark length X -> active length mark X,
               active eq(X, Y) -> mark false(),
           active eq(0(), 0()) -> mark true(),
           active eq(s X, s Y) -> mark eq(X, Y),
                  active inf X -> mark cons(X, inf s X),
           active take(0(), X) -> mark nil(),
  active take(s X, cons(Y, L)) -> mark cons(Y, take(X, L)),
      active length cons(X, L) -> mark s length L,
           active length nil() -> mark 0(),
               eq(X1, mark X2) -> eq(X1, X2),
             eq(X1, active X2) -> eq(X1, X2),
               eq(mark X1, X2) -> eq(X1, X2),
             eq(active X1, X2) -> eq(X1, X2),
                      s mark X -> s X,
                    s active X -> s 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),
                    inf mark X -> inf X,
                  inf active X -> inf 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),
                 length mark X -> length X,
               length active X -> length X}
 DP:
  DP:
   {                 mark# true() -> active# true(),
                 mark# eq(X1, X2) -> active# eq(X1, X2),
                        mark# 0() -> active# 0(),
                        mark# s X -> active# s X,
                    mark# false() -> active# false(),
               mark# cons(X1, X2) -> active# cons(X1, X2),
                      mark# inf X -> mark# X,
                      mark# inf X -> active# inf mark X,
                      mark# inf X -> inf# mark X,
                      mark# nil() -> active# nil(),
               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),
                   mark# length X -> mark# X,
                   mark# length X -> active# length mark X,
                   mark# length X -> length# mark X,
                 active# eq(X, Y) -> mark# false(),
             active# eq(0(), 0()) -> mark# true(),
             active# eq(s X, s Y) -> mark# eq(X, Y),
             active# eq(s X, s Y) -> eq#(X, Y),
                    active# inf X -> mark# cons(X, inf s X),
                    active# inf X -> s# X,
                    active# inf X -> cons#(X, inf s X),
                    active# inf X -> inf# s X,
             active# take(0(), X) -> mark# nil(),
    active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)),
    active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)),
    active# take(s X, cons(Y, L)) -> take#(X, L),
        active# length cons(X, L) -> mark# s length L,
        active# length cons(X, L) -> s# length L,
        active# length cons(X, L) -> length# L,
             active# length nil() -> mark# 0(),
                 eq#(X1, mark X2) -> eq#(X1, X2),
               eq#(X1, active X2) -> eq#(X1, X2),
                 eq#(mark X1, X2) -> eq#(X1, X2),
               eq#(active X1, X2) -> eq#(X1, X2),
                        s# mark X -> s# X,
                      s# active X -> s# 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),
                      inf# mark X -> inf# X,
                    inf# active X -> inf# 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),
                   length# mark X -> length# X,
                 length# active X -> length# X}
  TRS:
  {                 mark true() -> active true(),
                mark eq(X1, X2) -> active eq(X1, X2),
                       mark 0() -> active 0(),
                       mark s X -> active s X,
                   mark false() -> active false(),
              mark cons(X1, X2) -> active cons(X1, X2),
                     mark inf X -> active inf mark X,
                     mark nil() -> active nil(),
              mark take(X1, X2) -> active take(mark X1, mark X2),
                  mark length X -> active length mark X,
                active eq(X, Y) -> mark false(),
            active eq(0(), 0()) -> mark true(),
            active eq(s X, s Y) -> mark eq(X, Y),
                   active inf X -> mark cons(X, inf s X),
            active take(0(), X) -> mark nil(),
   active take(s X, cons(Y, L)) -> mark cons(Y, take(X, L)),
       active length cons(X, L) -> mark s length L,
            active length nil() -> mark 0(),
                eq(X1, mark X2) -> eq(X1, X2),
              eq(X1, active X2) -> eq(X1, X2),
                eq(mark X1, X2) -> eq(X1, X2),
              eq(active X1, X2) -> eq(X1, X2),
                       s mark X -> s X,
                     s active X -> s 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),
                     inf mark X -> inf X,
                   inf active X -> inf 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),
                  length mark X -> length X,
                length active X -> length X}
  UR:
   {                 mark true() -> active true(),
                 mark eq(X1, X2) -> active eq(X1, X2),
                        mark 0() -> active 0(),
                        mark s X -> active s X,
                    mark false() -> active false(),
               mark cons(X1, X2) -> active cons(X1, X2),
                      mark inf X -> active inf mark X,
                      mark nil() -> active nil(),
               mark take(X1, X2) -> active take(mark X1, mark X2),
                   mark length X -> active length mark X,
                 active eq(X, Y) -> mark false(),
             active eq(0(), 0()) -> mark true(),
             active eq(s X, s Y) -> mark eq(X, Y),
                    active inf X -> mark cons(X, inf s X),
             active take(0(), X) -> mark nil(),
    active take(s X, cons(Y, L)) -> mark cons(Y, take(X, L)),
        active length cons(X, L) -> mark s length L,
             active length nil() -> mark 0(),
                 eq(X1, mark X2) -> eq(X1, X2),
               eq(X1, active X2) -> eq(X1, X2),
                 eq(mark X1, X2) -> eq(X1, X2),
               eq(active X1, X2) -> eq(X1, X2),
                        s mark X -> s X,
                      s active X -> s 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),
                      inf mark X -> inf X,
                    inf active X -> inf 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),
                   length mark X -> length X,
                 length active X -> length X,
                         a(x, y) -> x,
                         a(x, y) -> y}
   EDG:
    {
     (mark# take(X1, X2) -> mark# X1, mark# length X -> length# mark X)
     (mark# take(X1, X2) -> mark# X1, mark# length X -> active# length mark X)
     (mark# take(X1, X2) -> mark# X1, mark# length X -> mark# X)
     (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> take#(mark X1, 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) -> mark# X2)
     (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# nil() -> active# nil())
     (mark# take(X1, X2) -> mark# X1, mark# inf X -> inf# mark X)
     (mark# take(X1, X2) -> mark# X1, mark# inf X -> active# inf mark X)
     (mark# take(X1, X2) -> mark# X1, mark# inf X -> mark# X)
     (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2))
     (mark# take(X1, X2) -> mark# X1, mark# false() -> active# false())
     (mark# take(X1, X2) -> mark# X1, mark# s X -> active# s X)
     (mark# take(X1, X2) -> mark# X1, mark# 0() -> active# 0())
     (mark# take(X1, X2) -> mark# X1, mark# eq(X1, X2) -> active# eq(X1, X2))
     (mark# take(X1, X2) -> mark# X1, mark# true() -> active# true())
     (mark# inf X -> mark# X, mark# length X -> length# mark X)
     (mark# inf X -> mark# X, mark# length X -> active# length mark X)
     (mark# inf X -> mark# X, mark# length X -> mark# X)
     (mark# inf X -> mark# X, mark# take(X1, X2) -> take#(mark X1, mark X2))
     (mark# inf X -> mark# X, mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (mark# inf X -> mark# X, mark# take(X1, X2) -> mark# X2)
     (mark# inf X -> mark# X, mark# take(X1, X2) -> mark# X1)
     (mark# inf X -> mark# X, mark# nil() -> active# nil())
     (mark# inf X -> mark# X, mark# inf X -> inf# mark X)
     (mark# inf X -> mark# X, mark# inf X -> active# inf mark X)
     (mark# inf X -> mark# X, mark# inf X -> mark# X)
     (mark# inf X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2))
     (mark# inf X -> mark# X, mark# false() -> active# false())
     (mark# inf X -> mark# X, mark# s X -> active# s X)
     (mark# inf X -> mark# X, mark# 0() -> active# 0())
     (mark# inf X -> mark# X, mark# eq(X1, X2) -> active# eq(X1, X2))
     (mark# inf X -> mark# X, mark# true() -> active# true())
     (active# inf X -> s# X, s# active X -> s# X)
     (active# inf X -> s# X, s# mark X -> s# X)
     (s# active X -> s# X, s# active X -> s# X)
     (s# active X -> s# X, s# mark X -> s# X)
     (inf# active X -> inf# X, inf# active X -> inf# X)
     (inf# active X -> inf# X, inf# mark X -> inf# X)
     (length# active X -> length# X, length# active X -> length# X)
     (length# active X -> length# X, length# mark X -> length# X)
     (mark# length X -> active# length mark X, active# length nil() -> mark# 0())
     (mark# length X -> active# length mark X, active# length cons(X, L) -> length# L)
     (mark# length X -> active# length mark X, active# length cons(X, L) -> s# length L)
     (mark# length X -> active# length mark X, active# length cons(X, L) -> mark# s length L)
     (mark# length X -> active# length mark X, active# take(s X, cons(Y, L)) -> take#(X, L))
     (mark# length X -> active# length mark X, active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
     (mark# length X -> active# length mark X, active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
     (mark# length X -> active# length mark X, active# take(0(), X) -> mark# nil())
     (mark# length X -> active# length mark X, active# inf X -> inf# s X)
     (mark# length X -> active# length mark X, active# inf X -> cons#(X, inf s X))
     (mark# length X -> active# length mark X, active# inf X -> s# X)
     (mark# length X -> active# length mark X, active# inf X -> mark# cons(X, inf s X))
     (mark# length X -> active# length mark X, active# eq(s X, s Y) -> eq#(X, Y))
     (mark# length X -> active# length mark X, active# eq(s X, s Y) -> mark# eq(X, Y))
     (mark# length X -> active# length mark X, active# eq(0(), 0()) -> mark# true())
     (mark# length X -> active# length mark X, active# eq(X, Y) -> mark# false())
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# length nil() -> mark# 0())
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# length cons(X, L) -> length# L)
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# length cons(X, L) -> s# length L)
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# length cons(X, L) -> mark# s length L)
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# take(s X, cons(Y, L)) -> take#(X, L))
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# take(0(), X) -> mark# nil())
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# inf X -> inf# s X)
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# inf X -> cons#(X, inf s X))
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# inf X -> s# X)
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# inf X -> mark# cons(X, inf s X))
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(s X, s Y) -> eq#(X, Y))
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(s X, s Y) -> mark# eq(X, Y))
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(0(), 0()) -> mark# true())
     (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(X, Y) -> mark# false())
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# length X -> length# mark X)
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# length X -> active# length mark X)
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# length X -> mark# X)
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# take(X1, X2) -> take#(mark X1, mark X2))
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# take(X1, X2) -> mark# X2)
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# take(X1, X2) -> mark# X1)
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# nil() -> active# nil())
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# inf X -> inf# mark X)
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# inf X -> active# inf mark X)
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# inf X -> mark# X)
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# cons(X1, X2) -> active# cons(X1, X2))
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# false() -> active# false())
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# s X -> active# s X)
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# 0() -> active# 0())
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# eq(X1, X2) -> active# eq(X1, X2))
     (active# eq(s X, s Y) -> mark# eq(X, Y), mark# true() -> active# true())
     (mark# true() -> active# true(), active# length nil() -> mark# 0())
     (mark# true() -> active# true(), active# length cons(X, L) -> length# L)
     (mark# true() -> active# true(), active# length cons(X, L) -> s# length L)
     (mark# true() -> active# true(), active# length cons(X, L) -> mark# s length L)
     (mark# true() -> active# true(), active# take(s X, cons(Y, L)) -> take#(X, L))
     (mark# true() -> active# true(), active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
     (mark# true() -> active# true(), active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
     (mark# true() -> active# true(), active# take(0(), X) -> mark# nil())
     (mark# true() -> active# true(), active# inf X -> inf# s X)
     (mark# true() -> active# true(), active# inf X -> cons#(X, inf s X))
     (mark# true() -> active# true(), active# inf X -> s# X)
     (mark# true() -> active# true(), active# inf X -> mark# cons(X, inf s X))
     (mark# true() -> active# true(), active# eq(s X, s Y) -> eq#(X, Y))
     (mark# true() -> active# true(), active# eq(s X, s Y) -> mark# eq(X, Y))
     (mark# true() -> active# true(), active# eq(0(), 0()) -> mark# true())
     (mark# true() -> active# true(), active# eq(X, Y) -> mark# false())
     (mark# false() -> active# false(), active# length nil() -> mark# 0())
     (mark# false() -> active# false(), active# length cons(X, L) -> length# L)
     (mark# false() -> active# false(), active# length cons(X, L) -> s# length L)
     (mark# false() -> active# false(), active# length cons(X, L) -> mark# s length L)
     (mark# false() -> active# false(), active# take(s X, cons(Y, L)) -> take#(X, L))
     (mark# false() -> active# false(), active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
     (mark# false() -> active# false(), active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
     (mark# false() -> active# false(), active# take(0(), X) -> mark# nil())
     (mark# false() -> active# false(), active# inf X -> inf# s X)
     (mark# false() -> active# false(), active# inf X -> cons#(X, inf s X))
     (mark# false() -> active# false(), active# inf X -> s# X)
     (mark# false() -> active# false(), active# inf X -> mark# cons(X, inf s X))
     (mark# false() -> active# false(), active# eq(s X, s Y) -> eq#(X, Y))
     (mark# false() -> active# false(), active# eq(s X, s Y) -> mark# eq(X, Y))
     (mark# false() -> active# false(), active# eq(0(), 0()) -> mark# true())
     (mark# false() -> active# false(), active# eq(X, Y) -> mark# false())
     (active# eq(X, Y) -> mark# false(), mark# length X -> length# mark X)
     (active# eq(X, Y) -> mark# false(), mark# length X -> active# length mark X)
     (active# eq(X, Y) -> mark# false(), mark# length X -> mark# X)
     (active# eq(X, Y) -> mark# false(), mark# take(X1, X2) -> take#(mark X1, mark X2))
     (active# eq(X, Y) -> mark# false(), mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (active# eq(X, Y) -> mark# false(), mark# take(X1, X2) -> mark# X2)
     (active# eq(X, Y) -> mark# false(), mark# take(X1, X2) -> mark# X1)
     (active# eq(X, Y) -> mark# false(), mark# nil() -> active# nil())
     (active# eq(X, Y) -> mark# false(), mark# inf X -> inf# mark X)
     (active# eq(X, Y) -> mark# false(), mark# inf X -> active# inf mark X)
     (active# eq(X, Y) -> mark# false(), mark# inf X -> mark# X)
     (active# eq(X, Y) -> mark# false(), mark# cons(X1, X2) -> active# cons(X1, X2))
     (active# eq(X, Y) -> mark# false(), mark# false() -> active# false())
     (active# eq(X, Y) -> mark# false(), mark# s X -> active# s X)
     (active# eq(X, Y) -> mark# false(), mark# 0() -> active# 0())
     (active# eq(X, Y) -> mark# false(), mark# eq(X1, X2) -> active# eq(X1, X2))
     (active# eq(X, Y) -> mark# false(), mark# true() -> active# true())
     (active# take(0(), X) -> mark# nil(), mark# length X -> length# mark X)
     (active# take(0(), X) -> mark# nil(), mark# length X -> active# length mark X)
     (active# take(0(), X) -> mark# nil(), mark# length X -> mark# X)
     (active# take(0(), X) -> mark# nil(), mark# take(X1, X2) -> take#(mark X1, mark X2))
     (active# take(0(), X) -> mark# nil(), mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (active# take(0(), X) -> mark# nil(), mark# take(X1, X2) -> mark# X2)
     (active# take(0(), X) -> mark# nil(), mark# take(X1, X2) -> mark# X1)
     (active# take(0(), X) -> mark# nil(), mark# nil() -> active# nil())
     (active# take(0(), X) -> mark# nil(), mark# inf X -> inf# mark X)
     (active# take(0(), X) -> mark# nil(), mark# inf X -> active# inf mark X)
     (active# take(0(), X) -> mark# nil(), mark# inf X -> mark# X)
     (active# take(0(), X) -> mark# nil(), mark# cons(X1, X2) -> active# cons(X1, X2))
     (active# take(0(), X) -> mark# nil(), mark# false() -> active# false())
     (active# take(0(), X) -> mark# nil(), mark# s X -> active# s X)
     (active# take(0(), X) -> mark# nil(), mark# 0() -> active# 0())
     (active# take(0(), X) -> mark# nil(), mark# eq(X1, X2) -> active# eq(X1, X2))
     (active# take(0(), X) -> mark# nil(), mark# true() -> active# true())
     (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# s X -> active# s X, active# length nil() -> mark# 0())
     (mark# s X -> active# s X, active# length cons(X, L) -> length# L)
     (mark# s X -> active# s X, active# length cons(X, L) -> s# length L)
     (mark# s X -> active# s X, active# length cons(X, L) -> mark# s length L)
     (mark# s X -> active# s X, active# take(s X, cons(Y, L)) -> take#(X, L))
     (mark# s X -> active# s X, active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
     (mark# s X -> active# s X, active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
     (mark# s X -> active# s X, active# take(0(), X) -> mark# nil())
     (mark# s X -> active# s X, active# inf X -> inf# s X)
     (mark# s X -> active# s X, active# inf X -> cons#(X, inf s X))
     (mark# s X -> active# s X, active# inf X -> s# X)
     (mark# s X -> active# s X, active# inf X -> mark# cons(X, inf s X))
     (mark# s X -> active# s X, active# eq(s X, s Y) -> eq#(X, Y))
     (mark# s X -> active# s X, active# eq(s X, s Y) -> mark# eq(X, Y))
     (mark# s X -> active# s X, active# eq(0(), 0()) -> mark# true())
     (mark# s X -> active# s X, active# eq(X, Y) -> mark# false())
     (mark# length X -> length# mark X, length# active X -> length# X)
     (mark# length X -> length# mark X, length# mark X -> length# X)
     (active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)), cons#(active X1, X2) -> cons#(X1, X2))
     (active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)), cons#(X1, active X2) -> cons#(X1, X2))
     (active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)), cons#(X1, mark X2) -> cons#(X1, X2))
     (eq#(X1, mark X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
     (eq#(X1, mark X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
     (eq#(X1, mark X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
     (eq#(X1, mark X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
     (eq#(mark X1, X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
     (eq#(mark X1, X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
     (eq#(mark X1, X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
     (eq#(mark X1, X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
     (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))
     (take#(X1, mark X2) -> take#(X1, X2), take#(active X1, 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#(X1, active X2) -> take#(X1, X2))
     (take#(X1, mark X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
     (take#(mark X1, X2) -> take#(X1, X2), take#(active X1, 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#(X1, active X2) -> take#(X1, X2))
     (take#(mark X1, X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
     (active# take(s X, cons(Y, L)) -> take#(X, L), take#(active X1, X2) -> take#(X1, X2))
     (active# take(s X, cons(Y, L)) -> take#(X, L), take#(mark X1, X2) -> take#(X1, X2))
     (active# take(s X, cons(Y, L)) -> take#(X, L), take#(X1, active X2) -> take#(X1, X2))
     (active# take(s X, cons(Y, L)) -> take#(X, L), take#(X1, mark X2) -> take#(X1, X2))
     (active# inf X -> mark# cons(X, inf s X), mark# length X -> length# mark X)
     (active# inf X -> mark# cons(X, inf s X), mark# length X -> active# length mark X)
     (active# inf X -> mark# cons(X, inf s X), mark# length X -> mark# X)
     (active# inf X -> mark# cons(X, inf s X), mark# take(X1, X2) -> take#(mark X1, mark X2))
     (active# inf X -> mark# cons(X, inf s X), mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (active# inf X -> mark# cons(X, inf s X), mark# take(X1, X2) -> mark# X2)
     (active# inf X -> mark# cons(X, inf s X), mark# take(X1, X2) -> mark# X1)
     (active# inf X -> mark# cons(X, inf s X), mark# nil() -> active# nil())
     (active# inf X -> mark# cons(X, inf s X), mark# inf X -> inf# mark X)
     (active# inf X -> mark# cons(X, inf s X), mark# inf X -> active# inf mark X)
     (active# inf X -> mark# cons(X, inf s X), mark# inf X -> mark# X)
     (active# inf X -> mark# cons(X, inf s X), mark# cons(X1, X2) -> active# cons(X1, X2))
     (active# inf X -> mark# cons(X, inf s X), mark# false() -> active# false())
     (active# inf X -> mark# cons(X, inf s X), mark# s X -> active# s X)
     (active# inf X -> mark# cons(X, inf s X), mark# 0() -> active# 0())
     (active# inf X -> mark# cons(X, inf s X), mark# eq(X1, X2) -> active# eq(X1, X2))
     (active# inf X -> mark# cons(X, inf s X), mark# true() -> active# true())
     (active# inf X -> cons#(X, inf s X), cons#(X1, mark X2) -> cons#(X1, X2))
     (active# inf X -> cons#(X, inf s X), cons#(X1, active X2) -> cons#(X1, X2))
     (active# inf X -> cons#(X, inf s X), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# inf X -> cons#(X, inf s X), cons#(active X1, X2) -> cons#(X1, X2))
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# eq(X, Y) -> mark# false())
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# eq(0(), 0()) -> mark# true())
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# eq(s X, s Y) -> mark# eq(X, Y))
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# eq(s X, s Y) -> eq#(X, Y))
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# inf X -> mark# cons(X, inf s X))
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# inf X -> s# X)
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# inf X -> cons#(X, inf s X))
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# inf X -> inf# s X)
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(0(), X) -> mark# nil())
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s X, cons(Y, L)) -> take#(X, L))
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length cons(X, L) -> mark# s length L)
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length cons(X, L) -> s# length L)
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length cons(X, L) -> length# L)
     (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length nil() -> mark# 0())
     (take#(active X1, X2) -> take#(X1, X2), take#(X1, mark 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#(mark X1, X2) -> take#(X1, X2))
     (take#(active X1, X2) -> take#(X1, X2), take#(active X1, X2) -> take#(X1, X2))
     (take#(X1, active X2) -> take#(X1, X2), take#(X1, mark 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#(mark X1, X2) -> take#(X1, X2))
     (take#(X1, active X2) -> take#(X1, X2), take#(active X1, X2) -> take#(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))
     (eq#(active X1, X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
     (eq#(active X1, X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
     (eq#(active X1, X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
     (eq#(active X1, X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
     (eq#(X1, active X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
     (eq#(X1, active X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
     (eq#(X1, active X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
     (eq#(X1, active X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# true() -> active# true())
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# eq(X1, X2) -> active# eq(X1, X2))
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# 0() -> active# 0())
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# s X -> active# s X)
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# false() -> active# false())
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# cons(X1, X2) -> active# cons(X1, X2))
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# inf X -> mark# X)
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# inf X -> active# inf mark X)
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# inf X -> inf# mark X)
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# nil() -> active# nil())
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# take(X1, X2) -> mark# X1)
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# take(X1, X2) -> mark# X2)
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# take(X1, X2) -> take#(mark X1, mark X2))
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# length X -> mark# X)
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# length X -> active# length mark X)
     (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# length X -> length# mark X)
     (active# inf X -> inf# s X, inf# mark X -> inf# X)
     (active# inf X -> inf# s X, inf# active X -> inf# X)
     (mark# inf X -> inf# mark X, inf# mark X -> inf# X)
     (mark# inf X -> inf# mark X, inf# active X -> inf# X)
     (active# length cons(X, L) -> s# length L, s# mark X -> s# X)
     (active# length cons(X, L) -> s# length L, s# active X -> s# X)
     (active# length nil() -> mark# 0(), mark# true() -> active# true())
     (active# length nil() -> mark# 0(), mark# eq(X1, X2) -> active# eq(X1, X2))
     (active# length nil() -> mark# 0(), mark# 0() -> active# 0())
     (active# length nil() -> mark# 0(), mark# s X -> active# s X)
     (active# length nil() -> mark# 0(), mark# false() -> active# false())
     (active# length nil() -> mark# 0(), mark# cons(X1, X2) -> active# cons(X1, X2))
     (active# length nil() -> mark# 0(), mark# inf X -> mark# X)
     (active# length nil() -> mark# 0(), mark# inf X -> active# inf mark X)
     (active# length nil() -> mark# 0(), mark# inf X -> inf# mark X)
     (active# length nil() -> mark# 0(), mark# nil() -> active# nil())
     (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))
     (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# eq(0(), 0()) -> mark# true(), mark# true() -> active# true())
     (active# eq(0(), 0()) -> mark# true(), mark# eq(X1, X2) -> active# eq(X1, X2))
     (active# eq(0(), 0()) -> mark# true(), mark# 0() -> active# 0())
     (active# eq(0(), 0()) -> mark# true(), mark# s X -> active# s X)
     (active# eq(0(), 0()) -> mark# true(), mark# false() -> active# false())
     (active# eq(0(), 0()) -> mark# true(), mark# cons(X1, X2) -> active# cons(X1, X2))
     (active# eq(0(), 0()) -> mark# true(), mark# inf X -> mark# X)
     (active# eq(0(), 0()) -> mark# true(), mark# inf X -> active# inf mark X)
     (active# eq(0(), 0()) -> mark# true(), mark# inf X -> inf# mark X)
     (active# eq(0(), 0()) -> mark# true(), mark# nil() -> active# nil())
     (active# eq(0(), 0()) -> mark# true(), mark# take(X1, X2) -> mark# X1)
     (active# eq(0(), 0()) -> mark# true(), mark# take(X1, X2) -> mark# X2)
     (active# eq(0(), 0()) -> mark# true(), mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (active# eq(0(), 0()) -> mark# true(), mark# take(X1, X2) -> take#(mark X1, mark X2))
     (active# eq(0(), 0()) -> mark# true(), mark# length X -> mark# X)
     (active# eq(0(), 0()) -> mark# true(), mark# length X -> active# length mark X)
     (active# eq(0(), 0()) -> mark# true(), mark# length X -> length# mark X)
     (mark# nil() -> active# nil(), active# eq(X, Y) -> mark# false())
     (mark# nil() -> active# nil(), active# eq(0(), 0()) -> mark# true())
     (mark# nil() -> active# nil(), active# eq(s X, s Y) -> mark# eq(X, Y))
     (mark# nil() -> active# nil(), active# eq(s X, s Y) -> eq#(X, Y))
     (mark# nil() -> active# nil(), active# inf X -> mark# cons(X, inf s X))
     (mark# nil() -> active# nil(), active# inf X -> s# X)
     (mark# nil() -> active# nil(), active# inf X -> cons#(X, inf s X))
     (mark# nil() -> active# nil(), active# inf X -> inf# s X)
     (mark# nil() -> active# nil(), active# take(0(), X) -> mark# nil())
     (mark# nil() -> active# nil(), active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
     (mark# nil() -> active# nil(), active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
     (mark# nil() -> active# nil(), active# take(s X, cons(Y, L)) -> take#(X, L))
     (mark# nil() -> active# nil(), active# length cons(X, L) -> mark# s length L)
     (mark# nil() -> active# nil(), active# length cons(X, L) -> s# length L)
     (mark# nil() -> active# nil(), active# length cons(X, L) -> length# L)
     (mark# nil() -> active# nil(), active# length nil() -> mark# 0())
     (mark# 0() -> active# 0(), active# eq(X, Y) -> mark# false())
     (mark# 0() -> active# 0(), active# eq(0(), 0()) -> mark# true())
     (mark# 0() -> active# 0(), active# eq(s X, s Y) -> mark# eq(X, Y))
     (mark# 0() -> active# 0(), active# eq(s X, s Y) -> eq#(X, Y))
     (mark# 0() -> active# 0(), active# inf X -> mark# cons(X, inf s X))
     (mark# 0() -> active# 0(), active# inf X -> s# X)
     (mark# 0() -> active# 0(), active# inf X -> cons#(X, inf s X))
     (mark# 0() -> active# 0(), active# inf X -> inf# s X)
     (mark# 0() -> active# 0(), active# take(0(), X) -> mark# nil())
     (mark# 0() -> active# 0(), active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
     (mark# 0() -> active# 0(), active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
     (mark# 0() -> active# 0(), active# take(s X, cons(Y, L)) -> take#(X, L))
     (mark# 0() -> active# 0(), active# length cons(X, L) -> mark# s length L)
     (mark# 0() -> active# 0(), active# length cons(X, L) -> s# length L)
     (mark# 0() -> active# 0(), active# length cons(X, L) -> length# L)
     (mark# 0() -> active# 0(), active# length nil() -> mark# 0())
     (active# eq(s X, s Y) -> eq#(X, Y), eq#(X1, mark X2) -> eq#(X1, X2))
     (active# eq(s X, s Y) -> eq#(X, Y), eq#(X1, active X2) -> eq#(X1, X2))
     (active# eq(s X, s Y) -> eq#(X, Y), eq#(mark X1, X2) -> eq#(X1, X2))
     (active# eq(s X, s Y) -> eq#(X, Y), eq#(active X1, X2) -> eq#(X1, X2))
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# eq(X, Y) -> mark# false())
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# eq(0(), 0()) -> mark# true())
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# eq(s X, s Y) -> mark# eq(X, Y))
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# eq(s X, s Y) -> eq#(X, Y))
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# inf X -> mark# cons(X, inf s X))
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# inf X -> s# X)
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# inf X -> cons#(X, inf s X))
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# inf X -> inf# s X)
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# take(0(), X) -> mark# nil())
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# take(s X, cons(Y, L)) -> take#(X, L))
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# length cons(X, L) -> mark# s length L)
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# length cons(X, L) -> s# length L)
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# length cons(X, L) -> length# L)
     (mark# cons(X1, X2) -> active# cons(X1, X2), active# length nil() -> mark# 0())
     (active# length cons(X, L) -> mark# s length L, mark# true() -> active# true())
     (active# length cons(X, L) -> mark# s length L, mark# eq(X1, X2) -> active# eq(X1, X2))
     (active# length cons(X, L) -> mark# s length L, mark# 0() -> active# 0())
     (active# length cons(X, L) -> mark# s length L, mark# s X -> active# s X)
     (active# length cons(X, L) -> mark# s length L, mark# false() -> active# false())
     (active# length cons(X, L) -> mark# s length L, mark# cons(X1, X2) -> active# cons(X1, X2))
     (active# length cons(X, L) -> mark# s length L, mark# inf X -> mark# X)
     (active# length cons(X, L) -> mark# s length L, mark# inf X -> active# inf mark X)
     (active# length cons(X, L) -> mark# s length L, mark# inf X -> inf# mark X)
     (active# length cons(X, L) -> mark# s length L, mark# nil() -> active# nil())
     (active# length cons(X, L) -> mark# s length L, mark# take(X1, X2) -> mark# X1)
     (active# length cons(X, L) -> mark# s length L, mark# take(X1, X2) -> mark# X2)
     (active# length cons(X, L) -> mark# s length L, mark# take(X1, X2) -> active# take(mark X1, mark X2))
     (active# length cons(X, L) -> mark# s length L, mark# take(X1, X2) -> take#(mark X1, mark X2))
     (active# length cons(X, L) -> mark# s length L, mark# length X -> mark# X)
     (active# length cons(X, L) -> mark# s length L, mark# length X -> active# length mark X)
     (active# length cons(X, L) -> mark# s length L, mark# length X -> length# mark X)
     (mark# inf X -> active# inf mark X, active# eq(X, Y) -> mark# false())
     (mark# inf X -> active# inf mark X, active# eq(0(), 0()) -> mark# true())
     (mark# inf X -> active# inf mark X, active# eq(s X, s Y) -> mark# eq(X, Y))
     (mark# inf X -> active# inf mark X, active# eq(s X, s Y) -> eq#(X, Y))
     (mark# inf X -> active# inf mark X, active# inf X -> mark# cons(X, inf s X))
     (mark# inf X -> active# inf mark X, active# inf X -> s# X)
     (mark# inf X -> active# inf mark X, active# inf X -> cons#(X, inf s X))
     (mark# inf X -> active# inf mark X, active# inf X -> inf# s X)
     (mark# inf X -> active# inf mark X, active# take(0(), X) -> mark# nil())
     (mark# inf X -> active# inf mark X, active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
     (mark# inf X -> active# inf mark X, active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
     (mark# inf X -> active# inf mark X, active# take(s X, cons(Y, L)) -> take#(X, L))
     (mark# inf X -> active# inf mark X, active# length cons(X, L) -> mark# s length L)
     (mark# inf X -> active# inf mark X, active# length cons(X, L) -> s# length L)
     (mark# inf X -> active# inf mark X, active# length cons(X, L) -> length# L)
     (mark# inf X -> active# inf mark X, active# length nil() -> mark# 0())
     (length# mark X -> length# X, length# mark X -> length# X)
     (length# mark X -> length# X, length# active X -> length# X)
     (inf# mark X -> inf# X, inf# mark X -> inf# X)
     (inf# mark X -> inf# X, inf# active X -> inf# X)
     (s# mark X -> s# X, s# mark X -> s# X)
     (s# mark X -> s# X, s# active X -> s# X)
     (mark# length X -> mark# X, mark# true() -> active# true())
     (mark# length X -> mark# X, mark# eq(X1, X2) -> active# eq(X1, X2))
     (mark# length X -> mark# X, mark# 0() -> active# 0())
     (mark# length X -> mark# X, mark# s X -> active# s X)
     (mark# length X -> mark# X, mark# false() -> active# false())
     (mark# length X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2))
     (mark# length X -> mark# X, mark# inf X -> mark# X)
     (mark# length X -> mark# X, mark# inf X -> active# inf mark X)
     (mark# length X -> mark# X, mark# inf X -> inf# mark X)
     (mark# length X -> mark# X, mark# nil() -> active# nil())
     (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X1)
     (mark# length X -> mark# X, mark# take(X1, X2) -> 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) -> take#(mark X1, mark X2))
     (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)
     (active# length cons(X, L) -> length# L, length# mark X -> length# X)
     (active# length cons(X, L) -> length# L, length# active X -> length# X)
     (mark# take(X1, X2) -> mark# X2, mark# true() -> active# true())
     (mark# take(X1, X2) -> mark# X2, mark# eq(X1, X2) -> active# eq(X1, X2))
     (mark# take(X1, X2) -> mark# X2, mark# 0() -> active# 0())
     (mark# take(X1, X2) -> mark# X2, mark# s X -> active# s X)
     (mark# take(X1, X2) -> mark# X2, mark# false() -> active# false())
     (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(X1, X2))
     (mark# take(X1, X2) -> mark# X2, mark# inf X -> mark# X)
     (mark# take(X1, X2) -> mark# X2, mark# inf X -> active# inf mark X)
     (mark# take(X1, X2) -> mark# X2, mark# inf X -> inf# mark X)
     (mark# take(X1, X2) -> mark# X2, mark# nil() -> active# nil())
     (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# 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)
    }
    EDG:
     {
      (mark# take(X1, X2) -> mark# X1, mark# length X -> length# mark X)
      (mark# take(X1, X2) -> mark# X1, mark# length X -> active# length mark X)
      (mark# take(X1, X2) -> mark# X1, mark# length X -> mark# X)
      (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> take#(mark X1, 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) -> mark# X2)
      (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
      (mark# take(X1, X2) -> mark# X1, mark# nil() -> active# nil())
      (mark# take(X1, X2) -> mark# X1, mark# inf X -> inf# mark X)
      (mark# take(X1, X2) -> mark# X1, mark# inf X -> active# inf mark X)
      (mark# take(X1, X2) -> mark# X1, mark# inf X -> mark# X)
      (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2))
      (mark# take(X1, X2) -> mark# X1, mark# false() -> active# false())
      (mark# take(X1, X2) -> mark# X1, mark# s X -> active# s X)
      (mark# take(X1, X2) -> mark# X1, mark# 0() -> active# 0())
      (mark# take(X1, X2) -> mark# X1, mark# eq(X1, X2) -> active# eq(X1, X2))
      (mark# take(X1, X2) -> mark# X1, mark# true() -> active# true())
      (mark# inf X -> mark# X, mark# length X -> length# mark X)
      (mark# inf X -> mark# X, mark# length X -> active# length mark X)
      (mark# inf X -> mark# X, mark# length X -> mark# X)
      (mark# inf X -> mark# X, mark# take(X1, X2) -> take#(mark X1, mark X2))
      (mark# inf X -> mark# X, mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (mark# inf X -> mark# X, mark# take(X1, X2) -> mark# X2)
      (mark# inf X -> mark# X, mark# take(X1, X2) -> mark# X1)
      (mark# inf X -> mark# X, mark# nil() -> active# nil())
      (mark# inf X -> mark# X, mark# inf X -> inf# mark X)
      (mark# inf X -> mark# X, mark# inf X -> active# inf mark X)
      (mark# inf X -> mark# X, mark# inf X -> mark# X)
      (mark# inf X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2))
      (mark# inf X -> mark# X, mark# false() -> active# false())
      (mark# inf X -> mark# X, mark# s X -> active# s X)
      (mark# inf X -> mark# X, mark# 0() -> active# 0())
      (mark# inf X -> mark# X, mark# eq(X1, X2) -> active# eq(X1, X2))
      (mark# inf X -> mark# X, mark# true() -> active# true())
      (active# inf X -> s# X, s# active X -> s# X)
      (active# inf X -> s# X, s# mark X -> s# X)
      (s# active X -> s# X, s# active X -> s# X)
      (s# active X -> s# X, s# mark X -> s# X)
      (inf# active X -> inf# X, inf# active X -> inf# X)
      (inf# active X -> inf# X, inf# mark X -> inf# X)
      (length# active X -> length# X, length# active X -> length# X)
      (length# active X -> length# X, length# mark X -> length# X)
      (mark# length X -> active# length mark X, active# length nil() -> mark# 0())
      (mark# length X -> active# length mark X, active# length cons(X, L) -> length# L)
      (mark# length X -> active# length mark X, active# length cons(X, L) -> s# length L)
      (mark# length X -> active# length mark X, active# length cons(X, L) -> mark# s length L)
      (mark# length X -> active# length mark X, active# take(s X, cons(Y, L)) -> take#(X, L))
      (mark# length X -> active# length mark X, active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
      (mark# length X -> active# length mark X, active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
      (mark# length X -> active# length mark X, active# take(0(), X) -> mark# nil())
      (mark# length X -> active# length mark X, active# inf X -> inf# s X)
      (mark# length X -> active# length mark X, active# inf X -> cons#(X, inf s X))
      (mark# length X -> active# length mark X, active# inf X -> s# X)
      (mark# length X -> active# length mark X, active# inf X -> mark# cons(X, inf s X))
      (mark# length X -> active# length mark X, active# eq(s X, s Y) -> eq#(X, Y))
      (mark# length X -> active# length mark X, active# eq(s X, s Y) -> mark# eq(X, Y))
      (mark# length X -> active# length mark X, active# eq(0(), 0()) -> mark# true())
      (mark# length X -> active# length mark X, active# eq(X, Y) -> mark# false())
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# length nil() -> mark# 0())
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# length cons(X, L) -> length# L)
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# length cons(X, L) -> s# length L)
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# length cons(X, L) -> mark# s length L)
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# take(s X, cons(Y, L)) -> take#(X, L))
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# take(0(), X) -> mark# nil())
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# inf X -> inf# s X)
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# inf X -> cons#(X, inf s X))
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# inf X -> s# X)
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# inf X -> mark# cons(X, inf s X))
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(s X, s Y) -> eq#(X, Y))
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(s X, s Y) -> mark# eq(X, Y))
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(0(), 0()) -> mark# true())
      (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(X, Y) -> mark# false())
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# length X -> length# mark X)
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# length X -> active# length mark X)
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# length X -> mark# X)
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# take(X1, X2) -> take#(mark X1, mark X2))
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# take(X1, X2) -> mark# X2)
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# take(X1, X2) -> mark# X1)
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# nil() -> active# nil())
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# inf X -> inf# mark X)
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# inf X -> active# inf mark X)
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# inf X -> mark# X)
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# cons(X1, X2) -> active# cons(X1, X2))
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# false() -> active# false())
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# s X -> active# s X)
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# 0() -> active# 0())
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# eq(X1, X2) -> active# eq(X1, X2))
      (active# eq(s X, s Y) -> mark# eq(X, Y), mark# true() -> active# true())
      (active# eq(X, Y) -> mark# false(), mark# false() -> active# false())
      (active# take(0(), X) -> mark# nil(), mark# nil() -> active# nil())
      (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# s X -> active# s X, active# length nil() -> mark# 0())
      (mark# s X -> active# s X, active# length cons(X, L) -> length# L)
      (mark# s X -> active# s X, active# length cons(X, L) -> s# length L)
      (mark# s X -> active# s X, active# length cons(X, L) -> mark# s length L)
      (mark# s X -> active# s X, active# take(s X, cons(Y, L)) -> take#(X, L))
      (mark# s X -> active# s X, active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
      (mark# s X -> active# s X, active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
      (mark# s X -> active# s X, active# take(0(), X) -> mark# nil())
      (mark# s X -> active# s X, active# inf X -> inf# s X)
      (mark# s X -> active# s X, active# inf X -> cons#(X, inf s X))
      (mark# s X -> active# s X, active# inf X -> s# X)
      (mark# s X -> active# s X, active# inf X -> mark# cons(X, inf s X))
      (mark# s X -> active# s X, active# eq(s X, s Y) -> eq#(X, Y))
      (mark# s X -> active# s X, active# eq(s X, s Y) -> mark# eq(X, Y))
      (mark# s X -> active# s X, active# eq(0(), 0()) -> mark# true())
      (mark# s X -> active# s X, active# eq(X, Y) -> mark# false())
      (mark# length X -> length# mark X, length# active X -> length# X)
      (mark# length X -> length# mark X, length# mark X -> length# X)
      (active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)), cons#(active X1, X2) -> cons#(X1, X2))
      (active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)), cons#(mark X1, X2) -> cons#(X1, X2))
      (active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)), cons#(X1, active X2) -> cons#(X1, X2))
      (active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)), cons#(X1, mark X2) -> cons#(X1, X2))
      (eq#(X1, mark X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
      (eq#(X1, mark X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
      (eq#(X1, mark X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
      (eq#(X1, mark X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
      (eq#(mark X1, X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
      (eq#(mark X1, X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
      (eq#(mark X1, X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
      (eq#(mark X1, X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
      (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))
      (take#(X1, mark X2) -> take#(X1, X2), take#(active X1, 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#(X1, active X2) -> take#(X1, X2))
      (take#(X1, mark X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
      (take#(mark X1, X2) -> take#(X1, X2), take#(active X1, 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#(X1, active X2) -> take#(X1, X2))
      (take#(mark X1, X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
      (active# take(s X, cons(Y, L)) -> take#(X, L), take#(active X1, X2) -> take#(X1, X2))
      (active# take(s X, cons(Y, L)) -> take#(X, L), take#(mark X1, X2) -> take#(X1, X2))
      (active# take(s X, cons(Y, L)) -> take#(X, L), take#(X1, active X2) -> take#(X1, X2))
      (active# take(s X, cons(Y, L)) -> take#(X, L), take#(X1, mark X2) -> take#(X1, X2))
      (active# inf X -> mark# cons(X, inf s X), mark# length X -> length# mark X)
      (active# inf X -> mark# cons(X, inf s X), mark# length X -> active# length mark X)
      (active# inf X -> mark# cons(X, inf s X), mark# length X -> mark# X)
      (active# inf X -> mark# cons(X, inf s X), mark# take(X1, X2) -> take#(mark X1, mark X2))
      (active# inf X -> mark# cons(X, inf s X), mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (active# inf X -> mark# cons(X, inf s X), mark# take(X1, X2) -> mark# X2)
      (active# inf X -> mark# cons(X, inf s X), mark# take(X1, X2) -> mark# X1)
      (active# inf X -> mark# cons(X, inf s X), mark# nil() -> active# nil())
      (active# inf X -> mark# cons(X, inf s X), mark# inf X -> inf# mark X)
      (active# inf X -> mark# cons(X, inf s X), mark# inf X -> active# inf mark X)
      (active# inf X -> mark# cons(X, inf s X), mark# inf X -> mark# X)
      (active# inf X -> mark# cons(X, inf s X), mark# cons(X1, X2) -> active# cons(X1, X2))
      (active# inf X -> mark# cons(X, inf s X), mark# false() -> active# false())
      (active# inf X -> mark# cons(X, inf s X), mark# s X -> active# s X)
      (active# inf X -> mark# cons(X, inf s X), mark# 0() -> active# 0())
      (active# inf X -> mark# cons(X, inf s X), mark# eq(X1, X2) -> active# eq(X1, X2))
      (active# inf X -> mark# cons(X, inf s X), mark# true() -> active# true())
      (active# inf X -> cons#(X, inf s X), cons#(X1, mark X2) -> cons#(X1, X2))
      (active# inf X -> cons#(X, inf s X), cons#(X1, active X2) -> cons#(X1, X2))
      (active# inf X -> cons#(X, inf s X), cons#(mark X1, X2) -> cons#(X1, X2))
      (active# inf X -> cons#(X, inf s X), cons#(active X1, X2) -> cons#(X1, X2))
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# eq(X, Y) -> mark# false())
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# eq(0(), 0()) -> mark# true())
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# eq(s X, s Y) -> mark# eq(X, Y))
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# eq(s X, s Y) -> eq#(X, Y))
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# inf X -> mark# cons(X, inf s X))
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# inf X -> s# X)
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# inf X -> cons#(X, inf s X))
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# inf X -> inf# s X)
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(0(), X) -> mark# nil())
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s X, cons(Y, L)) -> take#(X, L))
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length cons(X, L) -> mark# s length L)
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length cons(X, L) -> s# length L)
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length cons(X, L) -> length# L)
      (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# length nil() -> mark# 0())
      (take#(active X1, X2) -> take#(X1, X2), take#(X1, mark 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#(mark X1, X2) -> take#(X1, X2))
      (take#(active X1, X2) -> take#(X1, X2), take#(active X1, X2) -> take#(X1, X2))
      (take#(X1, active X2) -> take#(X1, X2), take#(X1, mark 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#(mark X1, X2) -> take#(X1, X2))
      (take#(X1, active X2) -> take#(X1, X2), take#(active X1, X2) -> take#(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))
      (eq#(active X1, X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
      (eq#(active X1, X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
      (eq#(active X1, X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
      (eq#(active X1, X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
      (eq#(X1, active X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
      (eq#(X1, active X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
      (eq#(X1, active X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
      (eq#(X1, active X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# true() -> active# true())
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# eq(X1, X2) -> active# eq(X1, X2))
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# 0() -> active# 0())
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# s X -> active# s X)
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# false() -> active# false())
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# cons(X1, X2) -> active# cons(X1, X2))
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# inf X -> mark# X)
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# inf X -> active# inf mark X)
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# inf X -> inf# mark X)
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# nil() -> active# nil())
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# take(X1, X2) -> mark# X1)
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# take(X1, X2) -> mark# X2)
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# take(X1, X2) -> take#(mark X1, mark X2))
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# length X -> mark# X)
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# length X -> active# length mark X)
      (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# length X -> length# mark X)
      (active# inf X -> inf# s X, inf# mark X -> inf# X)
      (active# inf X -> inf# s X, inf# active X -> inf# X)
      (mark# inf X -> inf# mark X, inf# mark X -> inf# X)
      (mark# inf X -> inf# mark X, inf# active X -> inf# X)
      (active# length cons(X, L) -> s# length L, s# mark X -> s# X)
      (active# length cons(X, L) -> s# length L, s# active X -> s# X)
      (active# length nil() -> mark# 0(), mark# 0() -> active# 0())
      (active# eq(0(), 0()) -> mark# true(), mark# true() -> active# true())
      (active# eq(s X, s Y) -> eq#(X, Y), eq#(X1, mark X2) -> eq#(X1, X2))
      (active# eq(s X, s Y) -> eq#(X, Y), eq#(X1, active X2) -> eq#(X1, X2))
      (active# eq(s X, s Y) -> eq#(X, Y), eq#(mark X1, X2) -> eq#(X1, X2))
      (active# eq(s X, s Y) -> eq#(X, Y), eq#(active X1, X2) -> eq#(X1, X2))
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# eq(X, Y) -> mark# false())
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# eq(0(), 0()) -> mark# true())
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# eq(s X, s Y) -> mark# eq(X, Y))
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# eq(s X, s Y) -> eq#(X, Y))
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# inf X -> mark# cons(X, inf s X))
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# inf X -> s# X)
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# inf X -> cons#(X, inf s X))
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# inf X -> inf# s X)
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# take(0(), X) -> mark# nil())
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# take(s X, cons(Y, L)) -> take#(X, L))
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# length cons(X, L) -> mark# s length L)
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# length cons(X, L) -> s# length L)
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# length cons(X, L) -> length# L)
      (mark# cons(X1, X2) -> active# cons(X1, X2), active# length nil() -> mark# 0())
      (active# length cons(X, L) -> mark# s length L, mark# true() -> active# true())
      (active# length cons(X, L) -> mark# s length L, mark# eq(X1, X2) -> active# eq(X1, X2))
      (active# length cons(X, L) -> mark# s length L, mark# 0() -> active# 0())
      (active# length cons(X, L) -> mark# s length L, mark# s X -> active# s X)
      (active# length cons(X, L) -> mark# s length L, mark# false() -> active# false())
      (active# length cons(X, L) -> mark# s length L, mark# cons(X1, X2) -> active# cons(X1, X2))
      (active# length cons(X, L) -> mark# s length L, mark# inf X -> mark# X)
      (active# length cons(X, L) -> mark# s length L, mark# inf X -> active# inf mark X)
      (active# length cons(X, L) -> mark# s length L, mark# inf X -> inf# mark X)
      (active# length cons(X, L) -> mark# s length L, mark# nil() -> active# nil())
      (active# length cons(X, L) -> mark# s length L, mark# take(X1, X2) -> mark# X1)
      (active# length cons(X, L) -> mark# s length L, mark# take(X1, X2) -> mark# X2)
      (active# length cons(X, L) -> mark# s length L, mark# take(X1, X2) -> active# take(mark X1, mark X2))
      (active# length cons(X, L) -> mark# s length L, mark# take(X1, X2) -> take#(mark X1, mark X2))
      (active# length cons(X, L) -> mark# s length L, mark# length X -> mark# X)
      (active# length cons(X, L) -> mark# s length L, mark# length X -> active# length mark X)
      (active# length cons(X, L) -> mark# s length L, mark# length X -> length# mark X)
      (mark# inf X -> active# inf mark X, active# eq(X, Y) -> mark# false())
      (mark# inf X -> active# inf mark X, active# eq(0(), 0()) -> mark# true())
      (mark# inf X -> active# inf mark X, active# eq(s X, s Y) -> mark# eq(X, Y))
      (mark# inf X -> active# inf mark X, active# eq(s X, s Y) -> eq#(X, Y))
      (mark# inf X -> active# inf mark X, active# inf X -> mark# cons(X, inf s X))
      (mark# inf X -> active# inf mark X, active# inf X -> s# X)
      (mark# inf X -> active# inf mark X, active# inf X -> cons#(X, inf s X))
      (mark# inf X -> active# inf mark X, active# inf X -> inf# s X)
      (mark# inf X -> active# inf mark X, active# take(0(), X) -> mark# nil())
      (mark# inf X -> active# inf mark X, active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
      (mark# inf X -> active# inf mark X, active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
      (mark# inf X -> active# inf mark X, active# take(s X, cons(Y, L)) -> take#(X, L))
      (mark# inf X -> active# inf mark X, active# length cons(X, L) -> mark# s length L)
      (mark# inf X -> active# inf mark X, active# length cons(X, L) -> s# length L)
      (mark# inf X -> active# inf mark X, active# length cons(X, L) -> length# L)
      (mark# inf X -> active# inf mark X, active# length nil() -> mark# 0())
      (length# mark X -> length# X, length# mark X -> length# X)
      (length# mark X -> length# X, length# active X -> length# X)
      (inf# mark X -> inf# X, inf# mark X -> inf# X)
      (inf# mark X -> inf# X, inf# active X -> inf# X)
      (s# mark X -> s# X, s# mark X -> s# X)
      (s# mark X -> s# X, s# active X -> s# X)
      (mark# length X -> mark# X, mark# true() -> active# true())
      (mark# length X -> mark# X, mark# eq(X1, X2) -> active# eq(X1, X2))
      (mark# length X -> mark# X, mark# 0() -> active# 0())
      (mark# length X -> mark# X, mark# s X -> active# s X)
      (mark# length X -> mark# X, mark# false() -> active# false())
      (mark# length X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2))
      (mark# length X -> mark# X, mark# inf X -> mark# X)
      (mark# length X -> mark# X, mark# inf X -> active# inf mark X)
      (mark# length X -> mark# X, mark# inf X -> inf# mark X)
      (mark# length X -> mark# X, mark# nil() -> active# nil())
      (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X1)
      (mark# length X -> mark# X, mark# take(X1, X2) -> 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) -> take#(mark X1, mark X2))
      (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)
      (active# length cons(X, L) -> length# L, length# mark X -> length# X)
      (active# length cons(X, L) -> length# L, length# active X -> length# X)
      (mark# take(X1, X2) -> mark# X2, mark# true() -> active# true())
      (mark# take(X1, X2) -> mark# X2, mark# eq(X1, X2) -> active# eq(X1, X2))
      (mark# take(X1, X2) -> mark# X2, mark# 0() -> active# 0())
      (mark# take(X1, X2) -> mark# X2, mark# s X -> active# s X)
      (mark# take(X1, X2) -> mark# X2, mark# false() -> active# false())
      (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(X1, X2))
      (mark# take(X1, X2) -> mark# X2, mark# inf X -> mark# X)
      (mark# take(X1, X2) -> mark# X2, mark# inf X -> active# inf mark X)
      (mark# take(X1, X2) -> mark# X2, mark# inf X -> inf# mark X)
      (mark# take(X1, X2) -> mark# X2, mark# nil() -> active# nil())
      (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# 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)
     }
     EDG:
      {
       (mark# take(X1, X2) -> mark# X1, mark# length X -> length# mark X)
       (mark# take(X1, X2) -> mark# X1, mark# length X -> active# length mark X)
       (mark# take(X1, X2) -> mark# X1, mark# length X -> mark# X)
       (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> take#(mark X1, 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) -> mark# X2)
       (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
       (mark# take(X1, X2) -> mark# X1, mark# nil() -> active# nil())
       (mark# take(X1, X2) -> mark# X1, mark# inf X -> inf# mark X)
       (mark# take(X1, X2) -> mark# X1, mark# inf X -> active# inf mark X)
       (mark# take(X1, X2) -> mark# X1, mark# inf X -> mark# X)
       (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2))
       (mark# take(X1, X2) -> mark# X1, mark# false() -> active# false())
       (mark# take(X1, X2) -> mark# X1, mark# s X -> active# s X)
       (mark# take(X1, X2) -> mark# X1, mark# 0() -> active# 0())
       (mark# take(X1, X2) -> mark# X1, mark# eq(X1, X2) -> active# eq(X1, X2))
       (mark# take(X1, X2) -> mark# X1, mark# true() -> active# true())
       (mark# inf X -> mark# X, mark# length X -> length# mark X)
       (mark# inf X -> mark# X, mark# length X -> active# length mark X)
       (mark# inf X -> mark# X, mark# length X -> mark# X)
       (mark# inf X -> mark# X, mark# take(X1, X2) -> take#(mark X1, mark X2))
       (mark# inf X -> mark# X, mark# take(X1, X2) -> active# take(mark X1, mark X2))
       (mark# inf X -> mark# X, mark# take(X1, X2) -> mark# X2)
       (mark# inf X -> mark# X, mark# take(X1, X2) -> mark# X1)
       (mark# inf X -> mark# X, mark# nil() -> active# nil())
       (mark# inf X -> mark# X, mark# inf X -> inf# mark X)
       (mark# inf X -> mark# X, mark# inf X -> active# inf mark X)
       (mark# inf X -> mark# X, mark# inf X -> mark# X)
       (mark# inf X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2))
       (mark# inf X -> mark# X, mark# false() -> active# false())
       (mark# inf X -> mark# X, mark# s X -> active# s X)
       (mark# inf X -> mark# X, mark# 0() -> active# 0())
       (mark# inf X -> mark# X, mark# eq(X1, X2) -> active# eq(X1, X2))
       (mark# inf X -> mark# X, mark# true() -> active# true())
       (active# inf X -> s# X, s# active X -> s# X)
       (active# inf X -> s# X, s# mark X -> s# X)
       (s# active X -> s# X, s# active X -> s# X)
       (s# active X -> s# X, s# mark X -> s# X)
       (inf# active X -> inf# X, inf# active X -> inf# X)
       (inf# active X -> inf# X, inf# mark X -> inf# X)
       (length# active X -> length# X, length# active X -> length# X)
       (length# active X -> length# X, length# mark X -> length# X)
       (mark# length X -> active# length mark X, active# length nil() -> mark# 0())
       (mark# length X -> active# length mark X, active# length cons(X, L) -> length# L)
       (mark# length X -> active# length mark X, active# length cons(X, L) -> s# length L)
       (mark# length X -> active# length mark X, active# length cons(X, L) -> mark# s length L)
       (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(s X, s Y) -> eq#(X, Y))
       (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(s X, s Y) -> mark# eq(X, Y))
       (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(0(), 0()) -> mark# true())
       (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(X, Y) -> mark# false())
       (active# eq(s X, s Y) -> mark# eq(X, Y), mark# eq(X1, X2) -> active# eq(X1, X2))
       (active# eq(X, Y) -> mark# false(), mark# false() -> active# false())
       (active# take(0(), X) -> mark# nil(), mark# nil() -> active# nil())
       (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# length X -> length# mark X, length# active X -> length# X)
       (mark# length X -> length# mark X, length# mark X -> length# X)
       (active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)), cons#(active X1, X2) -> cons#(X1, X2))
       (active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)), cons#(mark X1, X2) -> cons#(X1, X2))
       (eq#(X1, mark X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
       (eq#(X1, mark X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
       (eq#(X1, mark X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
       (eq#(X1, mark X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
       (eq#(mark X1, X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
       (eq#(mark X1, X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
       (eq#(mark X1, X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
       (eq#(mark X1, X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
       (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))
       (take#(X1, mark X2) -> take#(X1, X2), take#(active X1, 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#(X1, active X2) -> take#(X1, X2))
       (take#(X1, mark X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
       (take#(mark X1, X2) -> take#(X1, X2), take#(active X1, 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#(X1, active X2) -> take#(X1, X2))
       (take#(mark X1, X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
       (active# take(s X, cons(Y, L)) -> take#(X, L), take#(active X1, X2) -> take#(X1, X2))
       (active# take(s X, cons(Y, L)) -> take#(X, L), take#(mark X1, X2) -> take#(X1, X2))
       (active# take(s X, cons(Y, L)) -> take#(X, L), take#(X1, active X2) -> take#(X1, X2))
       (active# take(s X, cons(Y, L)) -> take#(X, L), take#(X1, mark X2) -> take#(X1, X2))
       (active# inf X -> mark# cons(X, inf s X), mark# cons(X1, X2) -> active# cons(X1, X2))
       (active# inf X -> cons#(X, inf s X), cons#(mark X1, X2) -> cons#(X1, X2))
       (active# inf X -> cons#(X, inf s X), cons#(active X1, X2) -> cons#(X1, X2))
       (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(0(), X) -> mark# nil())
       (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
       (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
       (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s X, cons(Y, L)) -> take#(X, L))
       (take#(active X1, X2) -> take#(X1, X2), take#(X1, mark 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#(mark X1, X2) -> take#(X1, X2))
       (take#(active X1, X2) -> take#(X1, X2), take#(active X1, X2) -> take#(X1, X2))
       (take#(X1, active X2) -> take#(X1, X2), take#(X1, mark 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#(mark X1, X2) -> take#(X1, X2))
       (take#(X1, active X2) -> take#(X1, X2), take#(active X1, X2) -> take#(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))
       (eq#(active X1, X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
       (eq#(active X1, X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
       (eq#(active X1, X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
       (eq#(active X1, X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
       (eq#(X1, active X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
       (eq#(X1, active X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
       (eq#(X1, active X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
       (eq#(X1, active X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
       (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# cons(X1, X2) -> active# cons(X1, X2))
       (mark# inf X -> inf# mark X, inf# mark X -> inf# X)
       (mark# inf X -> inf# mark X, inf# active X -> inf# X)
       (active# length nil() -> mark# 0(), mark# 0() -> active# 0())
       (active# eq(0(), 0()) -> mark# true(), mark# true() -> active# true())
       (active# eq(s X, s Y) -> eq#(X, Y), eq#(X1, mark X2) -> eq#(X1, X2))
       (active# eq(s X, s Y) -> eq#(X, Y), eq#(X1, active X2) -> eq#(X1, X2))
       (active# eq(s X, s Y) -> eq#(X, Y), eq#(mark X1, X2) -> eq#(X1, X2))
       (active# eq(s X, s Y) -> eq#(X, Y), eq#(active X1, X2) -> eq#(X1, X2))
       (active# length cons(X, L) -> mark# s length L, mark# s X -> active# s X)
       (mark# inf X -> active# inf mark X, active# inf X -> mark# cons(X, inf s X))
       (mark# inf X -> active# inf mark X, active# inf X -> s# X)
       (mark# inf X -> active# inf mark X, active# inf X -> cons#(X, inf s X))
       (mark# inf X -> active# inf mark X, active# inf X -> inf# s X)
       (length# mark X -> length# X, length# mark X -> length# X)
       (length# mark X -> length# X, length# active X -> length# X)
       (inf# mark X -> inf# X, inf# mark X -> inf# X)
       (inf# mark X -> inf# X, inf# active X -> inf# X)
       (s# mark X -> s# X, s# mark X -> s# X)
       (s# mark X -> s# X, s# active X -> s# X)
       (mark# length X -> mark# X, mark# true() -> active# true())
       (mark# length X -> mark# X, mark# eq(X1, X2) -> active# eq(X1, X2))
       (mark# length X -> mark# X, mark# 0() -> active# 0())
       (mark# length X -> mark# X, mark# s X -> active# s X)
       (mark# length X -> mark# X, mark# false() -> active# false())
       (mark# length X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2))
       (mark# length X -> mark# X, mark# inf X -> mark# X)
       (mark# length X -> mark# X, mark# inf X -> active# inf mark X)
       (mark# length X -> mark# X, mark# inf X -> inf# mark X)
       (mark# length X -> mark# X, mark# nil() -> active# nil())
       (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X1)
       (mark# length X -> mark# X, mark# take(X1, X2) -> 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) -> take#(mark X1, mark X2))
       (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)
       (active# length cons(X, L) -> length# L, length# mark X -> length# X)
       (active# length cons(X, L) -> length# L, length# active X -> length# X)
       (mark# take(X1, X2) -> mark# X2, mark# true() -> active# true())
       (mark# take(X1, X2) -> mark# X2, mark# eq(X1, X2) -> active# eq(X1, X2))
       (mark# take(X1, X2) -> mark# X2, mark# 0() -> active# 0())
       (mark# take(X1, X2) -> mark# X2, mark# s X -> active# s X)
       (mark# take(X1, X2) -> mark# X2, mark# false() -> active# false())
       (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(X1, X2))
       (mark# take(X1, X2) -> mark# X2, mark# inf X -> mark# X)
       (mark# take(X1, X2) -> mark# X2, mark# inf X -> active# inf mark X)
       (mark# take(X1, X2) -> mark# X2, mark# inf X -> inf# mark X)
       (mark# take(X1, X2) -> mark# X2, mark# nil() -> active# nil())
       (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# 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)
      }
      EDG:
       {
        (mark# take(X1, X2) -> mark# X1, mark# length X -> length# mark X)
        (mark# take(X1, X2) -> mark# X1, mark# length X -> active# length mark X)
        (mark# take(X1, X2) -> mark# X1, mark# length X -> mark# X)
        (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> take#(mark X1, 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) -> mark# X2)
        (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
        (mark# take(X1, X2) -> mark# X1, mark# nil() -> active# nil())
        (mark# take(X1, X2) -> mark# X1, mark# inf X -> inf# mark X)
        (mark# take(X1, X2) -> mark# X1, mark# inf X -> active# inf mark X)
        (mark# take(X1, X2) -> mark# X1, mark# inf X -> mark# X)
        (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2))
        (mark# take(X1, X2) -> mark# X1, mark# false() -> active# false())
        (mark# take(X1, X2) -> mark# X1, mark# s X -> active# s X)
        (mark# take(X1, X2) -> mark# X1, mark# 0() -> active# 0())
        (mark# take(X1, X2) -> mark# X1, mark# eq(X1, X2) -> active# eq(X1, X2))
        (mark# take(X1, X2) -> mark# X1, mark# true() -> active# true())
        (mark# inf X -> mark# X, mark# length X -> length# mark X)
        (mark# inf X -> mark# X, mark# length X -> active# length mark X)
        (mark# inf X -> mark# X, mark# length X -> mark# X)
        (mark# inf X -> mark# X, mark# take(X1, X2) -> take#(mark X1, mark X2))
        (mark# inf X -> mark# X, mark# take(X1, X2) -> active# take(mark X1, mark X2))
        (mark# inf X -> mark# X, mark# take(X1, X2) -> mark# X2)
        (mark# inf X -> mark# X, mark# take(X1, X2) -> mark# X1)
        (mark# inf X -> mark# X, mark# nil() -> active# nil())
        (mark# inf X -> mark# X, mark# inf X -> inf# mark X)
        (mark# inf X -> mark# X, mark# inf X -> active# inf mark X)
        (mark# inf X -> mark# X, mark# inf X -> mark# X)
        (mark# inf X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2))
        (mark# inf X -> mark# X, mark# false() -> active# false())
        (mark# inf X -> mark# X, mark# s X -> active# s X)
        (mark# inf X -> mark# X, mark# 0() -> active# 0())
        (mark# inf X -> mark# X, mark# eq(X1, X2) -> active# eq(X1, X2))
        (mark# inf X -> mark# X, mark# true() -> active# true())
        (active# inf X -> s# X, s# active X -> s# X)
        (active# inf X -> s# X, s# mark X -> s# X)
        (s# active X -> s# X, s# active X -> s# X)
        (s# active X -> s# X, s# mark X -> s# X)
        (inf# active X -> inf# X, inf# active X -> inf# X)
        (inf# active X -> inf# X, inf# mark X -> inf# X)
        (length# active X -> length# X, length# active X -> length# X)
        (length# active X -> length# X, length# mark X -> length# X)
        (mark# length X -> active# length mark X, active# length nil() -> mark# 0())
        (mark# length X -> active# length mark X, active# length cons(X, L) -> length# L)
        (mark# length X -> active# length mark X, active# length cons(X, L) -> s# length L)
        (mark# length X -> active# length mark X, active# length cons(X, L) -> mark# s length L)
        (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(s X, s Y) -> eq#(X, Y))
        (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(s X, s Y) -> mark# eq(X, Y))
        (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(0(), 0()) -> mark# true())
        (mark# eq(X1, X2) -> active# eq(X1, X2), active# eq(X, Y) -> mark# false())
        (active# eq(s X, s Y) -> mark# eq(X, Y), mark# eq(X1, X2) -> active# eq(X1, X2))
        (active# eq(X, Y) -> mark# false(), mark# false() -> active# false())
        (active# take(0(), X) -> mark# nil(), mark# nil() -> active# nil())
        (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# length X -> length# mark X, length# active X -> length# X)
        (mark# length X -> length# mark X, length# mark X -> length# X)
        (active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)), cons#(active X1, X2) -> cons#(X1, X2))
        (active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)), cons#(mark X1, X2) -> cons#(X1, X2))
        (eq#(X1, mark X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
        (eq#(X1, mark X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
        (eq#(X1, mark X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
        (eq#(X1, mark X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
        (eq#(mark X1, X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
        (eq#(mark X1, X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
        (eq#(mark X1, X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
        (eq#(mark X1, X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
        (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))
        (take#(X1, mark X2) -> take#(X1, X2), take#(active X1, 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#(X1, active X2) -> take#(X1, X2))
        (take#(X1, mark X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
        (take#(mark X1, X2) -> take#(X1, X2), take#(active X1, 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#(X1, active X2) -> take#(X1, X2))
        (take#(mark X1, X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
        (active# take(s X, cons(Y, L)) -> take#(X, L), take#(active X1, X2) -> take#(X1, X2))
        (active# take(s X, cons(Y, L)) -> take#(X, L), take#(mark X1, X2) -> take#(X1, X2))
        (active# take(s X, cons(Y, L)) -> take#(X, L), take#(X1, active X2) -> take#(X1, X2))
        (active# take(s X, cons(Y, L)) -> take#(X, L), take#(X1, mark X2) -> take#(X1, X2))
        (active# inf X -> mark# cons(X, inf s X), mark# cons(X1, X2) -> active# cons(X1, X2))
        (active# inf X -> cons#(X, inf s X), cons#(mark X1, X2) -> cons#(X1, X2))
        (active# inf X -> cons#(X, inf s X), cons#(active X1, X2) -> cons#(X1, X2))
        (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(0(), X) -> mark# nil())
        (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)))
        (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s X, cons(Y, L)) -> cons#(Y, take(X, L)))
        (mark# take(X1, X2) -> active# take(mark X1, mark X2), active# take(s X, cons(Y, L)) -> take#(X, L))
        (take#(active X1, X2) -> take#(X1, X2), take#(X1, mark 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#(mark X1, X2) -> take#(X1, X2))
        (take#(active X1, X2) -> take#(X1, X2), take#(active X1, X2) -> take#(X1, X2))
        (take#(X1, active X2) -> take#(X1, X2), take#(X1, mark 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#(mark X1, X2) -> take#(X1, X2))
        (take#(X1, active X2) -> take#(X1, X2), take#(active X1, X2) -> take#(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))
        (eq#(active X1, X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
        (eq#(active X1, X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
        (eq#(active X1, X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
        (eq#(active X1, X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
        (eq#(X1, active X2) -> eq#(X1, X2), eq#(X1, mark X2) -> eq#(X1, X2))
        (eq#(X1, active X2) -> eq#(X1, X2), eq#(X1, active X2) -> eq#(X1, X2))
        (eq#(X1, active X2) -> eq#(X1, X2), eq#(mark X1, X2) -> eq#(X1, X2))
        (eq#(X1, active X2) -> eq#(X1, X2), eq#(active X1, X2) -> eq#(X1, X2))
        (active# take(s X, cons(Y, L)) -> mark# cons(Y, take(X, L)), mark# cons(X1, X2) -> active# cons(X1, X2))
        (mark# inf X -> inf# mark X, inf# mark X -> inf# X)
        (mark# inf X -> inf# mark X, inf# active X -> inf# X)
        (active# length nil() -> mark# 0(), mark# 0() -> active# 0())
        (active# eq(0(), 0()) -> mark# true(), mark# true() -> active# true())
        (active# eq(s X, s Y) -> eq#(X, Y), eq#(X1, mark X2) -> eq#(X1, X2))
        (active# eq(s X, s Y) -> eq#(X, Y), eq#(X1, active X2) -> eq#(X1, X2))
        (active# eq(s X, s Y) -> eq#(X, Y), eq#(mark X1, X2) -> eq#(X1, X2))
        (active# eq(s X, s Y) -> eq#(X, Y), eq#(active X1, X2) -> eq#(X1, X2))
        (active# length cons(X, L) -> mark# s length L, mark# s X -> active# s X)
        (mark# inf X -> active# inf mark X, active# inf X -> mark# cons(X, inf s X))
        (mark# inf X -> active# inf mark X, active# inf X -> s# X)
        (mark# inf X -> active# inf mark X, active# inf X -> cons#(X, inf s X))
        (mark# inf X -> active# inf mark X, active# inf X -> inf# s X)
        (length# mark X -> length# X, length# mark X -> length# X)
        (length# mark X -> length# X, length# active X -> length# X)
        (inf# mark X -> inf# X, inf# mark X -> inf# X)
        (inf# mark X -> inf# X, inf# active X -> inf# X)
        (s# mark X -> s# X, s# mark X -> s# X)
        (s# mark X -> s# X, s# active X -> s# X)
        (mark# length X -> mark# X, mark# true() -> active# true())
        (mark# length X -> mark# X, mark# eq(X1, X2) -> active# eq(X1, X2))
        (mark# length X -> mark# X, mark# 0() -> active# 0())
        (mark# length X -> mark# X, mark# s X -> active# s X)
        (mark# length X -> mark# X, mark# false() -> active# false())
        (mark# length X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2))
        (mark# length X -> mark# X, mark# inf X -> mark# X)
        (mark# length X -> mark# X, mark# inf X -> active# inf mark X)
        (mark# length X -> mark# X, mark# inf X -> inf# mark X)
        (mark# length X -> mark# X, mark# nil() -> active# nil())
        (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X1)
        (mark# length X -> mark# X, mark# take(X1, X2) -> 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) -> take#(mark X1, mark X2))
        (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)
        (active# length cons(X, L) -> length# L, length# mark X -> length# X)
        (active# length cons(X, L) -> length# L, length# active X -> length# X)
        (mark# take(X1, X2) -> mark# X2, mark# true() -> active# true())
        (mark# take(X1, X2) -> mark# X2, mark# eq(X1, X2) -> active# eq(X1, X2))
        (mark# take(X1, X2) -> mark# X2, mark# 0() -> active# 0())
        (mark# take(X1, X2) -> mark# X2, mark# s X -> active# s X)
        (mark# take(X1, X2) -> mark# X2, mark# false() -> active# false())
        (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(X1, X2))
        (mark# take(X1, X2) -> mark# X2, mark# inf X -> mark# X)
        (mark# take(X1, X2) -> mark# X2, mark# inf X -> active# inf mark X)
        (mark# take(X1, X2) -> mark# X2, mark# inf X -> inf# mark X)
        (mark# take(X1, X2) -> mark# X2, mark# nil() -> active# nil())
        (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# 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)
       }
       STATUS:
        arrows: 0.932334
        SCCS (8):
         Scc:
          {       mark# inf X -> mark# X,
           mark# take(X1, X2) -> mark# X1,
           mark# take(X1, X2) -> mark# X2,
               mark# length X -> mark# X}
         Scc:
          {  length# mark X -> length# X,
           length# active X -> length# X}
         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:
          {  inf# mark X -> inf# X,
           inf# active X -> inf# X}
         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:
          {  s# mark X -> s# X,
           s# active X -> s# X}
         Scc:
          {    mark# eq(X1, X2) -> active# eq(X1, X2),
           active# eq(s X, s Y) -> mark# eq(X, Y)}
         Scc:
          {  eq#(X1, mark X2) -> eq#(X1, X2),
           eq#(X1, active X2) -> eq#(X1, X2),
             eq#(mark X1, X2) -> eq#(X1, X2),
           eq#(active X1, X2) -> eq#(X1, X2)}
         
         SCC (4):
          Strict:
           {       mark# inf X -> mark# X,
            mark# take(X1, X2) -> mark# X1,
            mark# take(X1, X2) -> mark# X2,
                mark# length X -> mark# X}
          Weak:
          {                 mark true() -> active true(),
                        mark eq(X1, X2) -> active eq(X1, X2),
                               mark 0() -> active 0(),
                               mark s X -> active s X,
                           mark false() -> active false(),
                      mark cons(X1, X2) -> active cons(X1, X2),
                             mark inf X -> active inf mark X,
                             mark nil() -> active nil(),
                      mark take(X1, X2) -> active take(mark X1, mark X2),
                          mark length X -> active length mark X,
                        active eq(X, Y) -> mark false(),
                    active eq(0(), 0()) -> mark true(),
                    active eq(s X, s Y) -> mark eq(X, Y),
                           active inf X -> mark cons(X, inf s X),
                    active take(0(), X) -> mark nil(),
           active take(s X, cons(Y, L)) -> mark cons(Y, take(X, L)),
               active length cons(X, L) -> mark s length L,
                    active length nil() -> mark 0(),
                        eq(X1, mark X2) -> eq(X1, X2),
                      eq(X1, active X2) -> eq(X1, X2),
                        eq(mark X1, X2) -> eq(X1, X2),
                      eq(active X1, X2) -> eq(X1, X2),
                               s mark X -> s X,
                             s active X -> s 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),
                             inf mark X -> inf X,
                           inf active X -> inf 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),
                          length mark X -> length X,
                        length active X -> length X}
          Open
         
         
         
         
         SCC (2):
          Strict:
           {  length# mark X -> length# X,
            length# active X -> length# X}
          Weak:
          {                 mark true() -> active true(),
                        mark eq(X1, X2) -> active eq(X1, X2),
                               mark 0() -> active 0(),
                               mark s X -> active s X,
                           mark false() -> active false(),
                      mark cons(X1, X2) -> active cons(X1, X2),
                             mark inf X -> active inf mark X,
                             mark nil() -> active nil(),
                      mark take(X1, X2) -> active take(mark X1, mark X2),
                          mark length X -> active length mark X,
                        active eq(X, Y) -> mark false(),
                    active eq(0(), 0()) -> mark true(),
                    active eq(s X, s Y) -> mark eq(X, Y),
                           active inf X -> mark cons(X, inf s X),
                    active take(0(), X) -> mark nil(),
           active take(s X, cons(Y, L)) -> mark cons(Y, take(X, L)),
               active length cons(X, L) -> mark s length L,
                    active length nil() -> mark 0(),
                        eq(X1, mark X2) -> eq(X1, X2),
                      eq(X1, active X2) -> eq(X1, X2),
                        eq(mark X1, X2) -> eq(X1, X2),
                      eq(active X1, X2) -> eq(X1, X2),
                               s mark X -> s X,
                             s active X -> s 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),
                             inf mark X -> inf X,
                           inf active X -> inf 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),
                          length mark X -> length X,
                        length active X -> length X}
          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 true() -> active true(),
                        mark eq(X1, X2) -> active eq(X1, X2),
                               mark 0() -> active 0(),
                               mark s X -> active s X,
                           mark false() -> active false(),
                      mark cons(X1, X2) -> active cons(X1, X2),
                             mark inf X -> active inf mark X,
                             mark nil() -> active nil(),
                      mark take(X1, X2) -> active take(mark X1, mark X2),
                          mark length X -> active length mark X,
                        active eq(X, Y) -> mark false(),
                    active eq(0(), 0()) -> mark true(),
                    active eq(s X, s Y) -> mark eq(X, Y),
                           active inf X -> mark cons(X, inf s X),
                    active take(0(), X) -> mark nil(),
           active take(s X, cons(Y, L)) -> mark cons(Y, take(X, L)),
               active length cons(X, L) -> mark s length L,
                    active length nil() -> mark 0(),
                        eq(X1, mark X2) -> eq(X1, X2),
                      eq(X1, active X2) -> eq(X1, X2),
                        eq(mark X1, X2) -> eq(X1, X2),
                      eq(active X1, X2) -> eq(X1, X2),
                               s mark X -> s X,
                             s active X -> s 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),
                             inf mark X -> inf X,
                           inf active X -> inf 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),
                          length mark X -> length X,
                        length active X -> length X}
          Open
         
         
         
         
         
         SCC (2):
          Strict:
           {  inf# mark X -> inf# X,
            inf# active X -> inf# X}
          Weak:
          {                 mark true() -> active true(),
                        mark eq(X1, X2) -> active eq(X1, X2),
                               mark 0() -> active 0(),
                               mark s X -> active s X,
                           mark false() -> active false(),
                      mark cons(X1, X2) -> active cons(X1, X2),
                             mark inf X -> active inf mark X,
                             mark nil() -> active nil(),
                      mark take(X1, X2) -> active take(mark X1, mark X2),
                          mark length X -> active length mark X,
                        active eq(X, Y) -> mark false(),
                    active eq(0(), 0()) -> mark true(),
                    active eq(s X, s Y) -> mark eq(X, Y),
                           active inf X -> mark cons(X, inf s X),
                    active take(0(), X) -> mark nil(),
           active take(s X, cons(Y, L)) -> mark cons(Y, take(X, L)),
               active length cons(X, L) -> mark s length L,
                    active length nil() -> mark 0(),
                        eq(X1, mark X2) -> eq(X1, X2),
                      eq(X1, active X2) -> eq(X1, X2),
                        eq(mark X1, X2) -> eq(X1, X2),
                      eq(active X1, X2) -> eq(X1, X2),
                               s mark X -> s X,
                             s active X -> s 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),
                             inf mark X -> inf X,
                           inf active X -> inf 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),
                          length mark X -> length X,
                        length active X -> length 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 true() -> active true(),
                        mark eq(X1, X2) -> active eq(X1, X2),
                               mark 0() -> active 0(),
                               mark s X -> active s X,
                           mark false() -> active false(),
                      mark cons(X1, X2) -> active cons(X1, X2),
                             mark inf X -> active inf mark X,
                             mark nil() -> active nil(),
                      mark take(X1, X2) -> active take(mark X1, mark X2),
                          mark length X -> active length mark X,
                        active eq(X, Y) -> mark false(),
                    active eq(0(), 0()) -> mark true(),
                    active eq(s X, s Y) -> mark eq(X, Y),
                           active inf X -> mark cons(X, inf s X),
                    active take(0(), X) -> mark nil(),
           active take(s X, cons(Y, L)) -> mark cons(Y, take(X, L)),
               active length cons(X, L) -> mark s length L,
                    active length nil() -> mark 0(),
                        eq(X1, mark X2) -> eq(X1, X2),
                      eq(X1, active X2) -> eq(X1, X2),
                        eq(mark X1, X2) -> eq(X1, X2),
                      eq(active X1, X2) -> eq(X1, X2),
                               s mark X -> s X,
                             s active X -> s 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),
                             inf mark X -> inf X,
                           inf active X -> inf 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),
                          length mark X -> length X,
                        length active X -> length X}
          Open
         
         SCC (2):
          Strict:
           {  s# mark X -> s# X,
            s# active X -> s# X}
          Weak:
          {                 mark true() -> active true(),
                        mark eq(X1, X2) -> active eq(X1, X2),
                               mark 0() -> active 0(),
                               mark s X -> active s X,
                           mark false() -> active false(),
                      mark cons(X1, X2) -> active cons(X1, X2),
                             mark inf X -> active inf mark X,
                             mark nil() -> active nil(),
                      mark take(X1, X2) -> active take(mark X1, mark X2),
                          mark length X -> active length mark X,
                        active eq(X, Y) -> mark false(),
                    active eq(0(), 0()) -> mark true(),
                    active eq(s X, s Y) -> mark eq(X, Y),
                           active inf X -> mark cons(X, inf s X),
                    active take(0(), X) -> mark nil(),
           active take(s X, cons(Y, L)) -> mark cons(Y, take(X, L)),
               active length cons(X, L) -> mark s length L,
                    active length nil() -> mark 0(),
                        eq(X1, mark X2) -> eq(X1, X2),
                      eq(X1, active X2) -> eq(X1, X2),
                        eq(mark X1, X2) -> eq(X1, X2),
                      eq(active X1, X2) -> eq(X1, X2),
                               s mark X -> s X,
                             s active X -> s 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),
                             inf mark X -> inf X,
                           inf active X -> inf 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),
                          length mark X -> length X,
                        length active X -> length X}
          Open
         
         
         
         
         SCC (2):
          Strict:
           {    mark# eq(X1, X2) -> active# eq(X1, X2),
            active# eq(s X, s Y) -> mark# eq(X, Y)}
          Weak:
          {                 mark true() -> active true(),
                        mark eq(X1, X2) -> active eq(X1, X2),
                               mark 0() -> active 0(),
                               mark s X -> active s X,
                           mark false() -> active false(),
                      mark cons(X1, X2) -> active cons(X1, X2),
                             mark inf X -> active inf mark X,
                             mark nil() -> active nil(),
                      mark take(X1, X2) -> active take(mark X1, mark X2),
                          mark length X -> active length mark X,
                        active eq(X, Y) -> mark false(),
                    active eq(0(), 0()) -> mark true(),
                    active eq(s X, s Y) -> mark eq(X, Y),
                           active inf X -> mark cons(X, inf s X),
                    active take(0(), X) -> mark nil(),
           active take(s X, cons(Y, L)) -> mark cons(Y, take(X, L)),
               active length cons(X, L) -> mark s length L,
                    active length nil() -> mark 0(),
                        eq(X1, mark X2) -> eq(X1, X2),
                      eq(X1, active X2) -> eq(X1, X2),
                        eq(mark X1, X2) -> eq(X1, X2),
                      eq(active X1, X2) -> eq(X1, X2),
                               s mark X -> s X,
                             s active X -> s 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),
                             inf mark X -> inf X,
                           inf active X -> inf 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),
                          length mark X -> length X,
                        length active X -> length X}
          Open
         
         SCC (4):
          Strict:
           {  eq#(X1, mark X2) -> eq#(X1, X2),
            eq#(X1, active X2) -> eq#(X1, X2),
              eq#(mark X1, X2) -> eq#(X1, X2),
            eq#(active X1, X2) -> eq#(X1, X2)}
          Weak:
          {                 mark true() -> active true(),
                        mark eq(X1, X2) -> active eq(X1, X2),
                               mark 0() -> active 0(),
                               mark s X -> active s X,
                           mark false() -> active false(),
                      mark cons(X1, X2) -> active cons(X1, X2),
                             mark inf X -> active inf mark X,
                             mark nil() -> active nil(),
                      mark take(X1, X2) -> active take(mark X1, mark X2),
                          mark length X -> active length mark X,
                        active eq(X, Y) -> mark false(),
                    active eq(0(), 0()) -> mark true(),
                    active eq(s X, s Y) -> mark eq(X, Y),
                           active inf X -> mark cons(X, inf s X),
                    active take(0(), X) -> mark nil(),
           active take(s X, cons(Y, L)) -> mark cons(Y, take(X, L)),
               active length cons(X, L) -> mark s length L,
                    active length nil() -> mark 0(),
                        eq(X1, mark X2) -> eq(X1, X2),
                      eq(X1, active X2) -> eq(X1, X2),
                        eq(mark X1, X2) -> eq(X1, X2),
                      eq(active X1, X2) -> eq(X1, X2),
                               s mark X -> s X,
                             s active X -> s 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),
                             inf mark X -> inf X,
                           inf active X -> inf 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),
                          length mark X -> length X,
                        length active X -> length X}
          Open