MAYBE
Time: 0.835052
TRS:
 {               a__zeros() -> cons(0(), zeros()),
                 a__zeros() -> zeros(),
          mark cons(X1, X2) -> cons(mark X1, X2),
                   mark 0() -> 0(),
               mark zeros() -> a__zeros(),
                  mark tt() -> tt(),
                 mark nil() -> nil(),
                   mark s X -> s mark X,
          mark take(X1, X2) -> a__take(mark X1, mark X2),
           mark and(X1, X2) -> a__and(mark X1, X2),
              mark length X -> a__length mark X,
             a__and(X1, X2) -> and(X1, X2),
            a__and(tt(), X) -> mark X,
                a__length X -> length X,
       a__length cons(N, L) -> s a__length mark L,
            a__length nil() -> 0(),
            a__take(X1, X2) -> take(X1, X2),
           a__take(0(), IL) -> nil(),
  a__take(s M, cons(N, IL)) -> cons(mark N, take(M, IL))}
 DP:
  DP:
   {        mark# cons(X1, X2) -> mark# X1,
                 mark# zeros() -> a__zeros#(),
                     mark# s X -> mark# X,
            mark# take(X1, X2) -> mark# X1,
            mark# take(X1, X2) -> mark# X2,
            mark# take(X1, X2) -> a__take#(mark X1, mark X2),
             mark# and(X1, X2) -> mark# X1,
             mark# and(X1, X2) -> a__and#(mark X1, X2),
                mark# length X -> mark# X,
                mark# length X -> a__length# mark X,
              a__and#(tt(), X) -> mark# X,
         a__length# cons(N, L) -> mark# L,
         a__length# cons(N, L) -> a__length# mark L,
    a__take#(s M, cons(N, IL)) -> mark# N}
  TRS:
  {               a__zeros() -> cons(0(), zeros()),
                  a__zeros() -> zeros(),
           mark cons(X1, X2) -> cons(mark X1, X2),
                    mark 0() -> 0(),
                mark zeros() -> a__zeros(),
                   mark tt() -> tt(),
                  mark nil() -> nil(),
                    mark s X -> s mark X,
           mark take(X1, X2) -> a__take(mark X1, mark X2),
            mark and(X1, X2) -> a__and(mark X1, X2),
               mark length X -> a__length mark X,
              a__and(X1, X2) -> and(X1, X2),
             a__and(tt(), X) -> mark X,
                 a__length X -> length X,
        a__length cons(N, L) -> s a__length mark L,
             a__length nil() -> 0(),
             a__take(X1, X2) -> take(X1, X2),
            a__take(0(), IL) -> nil(),
   a__take(s M, cons(N, IL)) -> cons(mark N, take(M, IL))}
  UR:
   {               a__zeros() -> cons(0(), zeros()),
                   a__zeros() -> zeros(),
            mark cons(X1, X2) -> cons(mark X1, X2),
                     mark 0() -> 0(),
                 mark zeros() -> a__zeros(),
                    mark tt() -> tt(),
                   mark nil() -> nil(),
                     mark s X -> s mark X,
            mark take(X1, X2) -> a__take(mark X1, mark X2),
             mark and(X1, X2) -> a__and(mark X1, X2),
                mark length X -> a__length mark X,
               a__and(X1, X2) -> and(X1, X2),
              a__and(tt(), X) -> mark X,
                  a__length X -> length X,
         a__length cons(N, L) -> s a__length mark L,
              a__length nil() -> 0(),
              a__take(X1, X2) -> take(X1, X2),
             a__take(0(), IL) -> nil(),
    a__take(s M, cons(N, IL)) -> cons(mark N, take(M, IL))}
   EDG:
    {(mark# take(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)
     (mark# take(X1, X2) -> mark# X1, mark# length X -> mark# X)
     (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__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# s X -> mark# X)
     (mark# take(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
     (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X)
     (a__length# cons(N, L) -> a__length# mark L, a__length# cons(N, L) -> a__length# mark L)
     (a__length# cons(N, L) -> a__length# mark L, a__length# cons(N, L) -> mark# L)
     (mark# take(X1, X2) -> mark# X2, mark# length X -> a__length# mark X)
     (mark# take(X1, X2) -> mark# X2, mark# length X -> mark# X)
     (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2)
     (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# take(X1, X2) -> mark# X2, mark# zeros() -> a__zeros#())
     (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (a__take#(s M, cons(N, IL)) -> mark# N, mark# length X -> a__length# mark X)
     (a__take#(s M, cons(N, IL)) -> mark# N, mark# length X -> mark# X)
     (a__take#(s M, cons(N, IL)) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__take#(s M, cons(N, IL)) -> mark# N, mark# and(X1, X2) -> mark# X1)
     (a__take#(s M, cons(N, IL)) -> mark# N, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__take#(s M, cons(N, IL)) -> mark# N, mark# take(X1, X2) -> mark# X2)
     (a__take#(s M, cons(N, IL)) -> mark# N, mark# take(X1, X2) -> mark# X1)
     (a__take#(s M, cons(N, IL)) -> mark# N, mark# s X -> mark# X)
     (a__take#(s M, cons(N, IL)) -> mark# N, mark# zeros() -> a__zeros#())
     (a__take#(s M, cons(N, IL)) -> mark# N, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# length X -> a__length# mark X)
     (mark# s X -> mark# X, mark# length X -> mark# X)
     (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# zeros() -> a__zeros#())
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# length X -> a__length# mark X)
     (a__and#(tt(), X) -> mark# X, mark# length X -> mark# X)
     (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X2)
     (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X)
     (a__and#(tt(), X) -> mark# X, mark# zeros() -> a__zeros#())
     (a__and#(tt(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# length X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# length X -> mark# X, mark# zeros() -> a__zeros#())
     (mark# length X -> mark# X, mark# s X -> mark# X)
     (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) -> a__take#(mark X1, mark X2))
     (mark# length X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# length X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# length X -> mark# X, mark# length X -> mark# X)
     (mark# length X -> mark# X, mark# length X -> a__length# mark X)
     (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(s M, cons(N, IL)) -> mark# N)
     (mark# length X -> a__length# mark X, a__length# cons(N, L) -> mark# L)
     (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__length# mark L)
     (a__length# cons(N, L) -> mark# L, mark# cons(X1, X2) -> mark# X1)
     (a__length# cons(N, L) -> mark# L, mark# zeros() -> a__zeros#())
     (a__length# cons(N, L) -> mark# L, mark# s X -> mark# X)
     (a__length# cons(N, L) -> mark# L, mark# take(X1, X2) -> mark# X1)
     (a__length# cons(N, L) -> mark# L, mark# take(X1, X2) -> mark# X2)
     (a__length# cons(N, L) -> mark# L, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__length# cons(N, L) -> mark# L, mark# and(X1, X2) -> mark# X1)
     (a__length# cons(N, L) -> mark# L, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__length# cons(N, L) -> mark# L, mark# length X -> mark# X)
     (a__length# cons(N, L) -> mark# L, mark# length X -> a__length# mark X)
     (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
     (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# and(X1, X2) -> mark# X1, mark# length X -> mark# X)
     (mark# and(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# length X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)}
    EDG:
     {(mark# take(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)
      (mark# take(X1, X2) -> mark# X1, mark# length X -> mark# X)
      (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
      (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
      (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__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# s X -> mark# X)
      (mark# take(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
      (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X)
      (a__length# cons(N, L) -> a__length# mark L, a__length# cons(N, L) -> a__length# mark L)
      (a__length# cons(N, L) -> a__length# mark L, a__length# cons(N, L) -> mark# L)
      (mark# take(X1, X2) -> mark# X2, mark# length X -> a__length# mark X)
      (mark# take(X1, X2) -> mark# X2, mark# length X -> mark# X)
      (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
      (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
      (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
      (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2)
      (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1)
      (mark# take(X1, X2) -> mark# X2, mark# s X -> mark# X)
      (mark# take(X1, X2) -> mark# X2, mark# zeros() -> a__zeros#())
      (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
      (a__take#(s M, cons(N, IL)) -> mark# N, mark# length X -> a__length# mark X)
      (a__take#(s M, cons(N, IL)) -> mark# N, mark# length X -> mark# X)
      (a__take#(s M, cons(N, IL)) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
      (a__take#(s M, cons(N, IL)) -> mark# N, mark# and(X1, X2) -> mark# X1)
      (a__take#(s M, cons(N, IL)) -> mark# N, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
      (a__take#(s M, cons(N, IL)) -> mark# N, mark# take(X1, X2) -> mark# X2)
      (a__take#(s M, cons(N, IL)) -> mark# N, mark# take(X1, X2) -> mark# X1)
      (a__take#(s M, cons(N, IL)) -> mark# N, mark# s X -> mark# X)
      (a__take#(s M, cons(N, IL)) -> mark# N, mark# zeros() -> a__zeros#())
      (a__take#(s M, cons(N, IL)) -> mark# N, mark# cons(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# length X -> a__length# mark X)
      (mark# s X -> mark# X, mark# length X -> mark# X)
      (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
      (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
      (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X2)
      (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1)
      (mark# s X -> mark# X, mark# s X -> mark# X)
      (mark# s X -> mark# X, mark# zeros() -> a__zeros#())
      (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (a__and#(tt(), X) -> mark# X, mark# length X -> a__length# mark X)
      (a__and#(tt(), X) -> mark# X, mark# length X -> mark# X)
      (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
      (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
      (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
      (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X2)
      (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X1)
      (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X)
      (a__and#(tt(), X) -> mark# X, mark# zeros() -> a__zeros#())
      (a__and#(tt(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# length X -> mark# X, mark# cons(X1, X2) -> mark# X1)
      (mark# length X -> mark# X, mark# zeros() -> a__zeros#())
      (mark# length X -> mark# X, mark# s X -> mark# X)
      (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) -> a__take#(mark X1, mark X2))
      (mark# length X -> mark# X, mark# and(X1, X2) -> mark# X1)
      (mark# length X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
      (mark# length X -> mark# X, mark# length X -> mark# X)
      (mark# length X -> mark# X, mark# length X -> a__length# mark X)
      (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(s M, cons(N, IL)) -> mark# N)
      (mark# length X -> a__length# mark X, a__length# cons(N, L) -> mark# L)
      (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__length# mark L)
      (a__length# cons(N, L) -> mark# L, mark# cons(X1, X2) -> mark# X1)
      (a__length# cons(N, L) -> mark# L, mark# zeros() -> a__zeros#())
      (a__length# cons(N, L) -> mark# L, mark# s X -> mark# X)
      (a__length# cons(N, L) -> mark# L, mark# take(X1, X2) -> mark# X1)
      (a__length# cons(N, L) -> mark# L, mark# take(X1, X2) -> mark# X2)
      (a__length# cons(N, L) -> mark# L, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
      (a__length# cons(N, L) -> mark# L, mark# and(X1, X2) -> mark# X1)
      (a__length# cons(N, L) -> mark# L, mark# and(X1, X2) -> a__and#(mark X1, X2))
      (a__length# cons(N, L) -> mark# L, mark# length X -> mark# X)
      (a__length# cons(N, L) -> mark# L, mark# length X -> a__length# mark X)
      (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (mark# and(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
      (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
      (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
      (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
      (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
      (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
      (mark# and(X1, X2) -> mark# X1, mark# length X -> mark# X)
      (mark# and(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)
      (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
      (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
      (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
      (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
      (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
      (mark# cons(X1, X2) -> mark# X1, mark# length X -> mark# X)
      (mark# cons(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)}
     EDG:
      {(mark# take(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)
       (mark# take(X1, X2) -> mark# X1, mark# length X -> mark# X)
       (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
       (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
       (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__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# s X -> mark# X)
       (mark# take(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
       (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
       (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X)
       (a__length# cons(N, L) -> a__length# mark L, a__length# cons(N, L) -> a__length# mark L)
       (a__length# cons(N, L) -> a__length# mark L, a__length# cons(N, L) -> mark# L)
       (mark# take(X1, X2) -> mark# X2, mark# length X -> a__length# mark X)
       (mark# take(X1, X2) -> mark# X2, mark# length X -> mark# X)
       (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
       (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
       (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
       (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2)
       (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1)
       (mark# take(X1, X2) -> mark# X2, mark# s X -> mark# X)
       (mark# take(X1, X2) -> mark# X2, mark# zeros() -> a__zeros#())
       (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
       (a__take#(s M, cons(N, IL)) -> mark# N, mark# length X -> a__length# mark X)
       (a__take#(s M, cons(N, IL)) -> mark# N, mark# length X -> mark# X)
       (a__take#(s M, cons(N, IL)) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
       (a__take#(s M, cons(N, IL)) -> mark# N, mark# and(X1, X2) -> mark# X1)
       (a__take#(s M, cons(N, IL)) -> mark# N, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
       (a__take#(s M, cons(N, IL)) -> mark# N, mark# take(X1, X2) -> mark# X2)
       (a__take#(s M, cons(N, IL)) -> mark# N, mark# take(X1, X2) -> mark# X1)
       (a__take#(s M, cons(N, IL)) -> mark# N, mark# s X -> mark# X)
       (a__take#(s M, cons(N, IL)) -> mark# N, mark# zeros() -> a__zeros#())
       (a__take#(s M, cons(N, IL)) -> mark# N, mark# cons(X1, X2) -> mark# X1)
       (mark# s X -> mark# X, mark# length X -> a__length# mark X)
       (mark# s X -> mark# X, mark# length X -> mark# X)
       (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
       (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1)
       (mark# s X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
       (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X2)
       (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1)
       (mark# s X -> mark# X, mark# s X -> mark# X)
       (mark# s X -> mark# X, mark# zeros() -> a__zeros#())
       (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (a__and#(tt(), X) -> mark# X, mark# length X -> a__length# mark X)
       (a__and#(tt(), X) -> mark# X, mark# length X -> mark# X)
       (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
       (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
       (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
       (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X2)
       (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X1)
       (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X)
       (a__and#(tt(), X) -> mark# X, mark# zeros() -> a__zeros#())
       (a__and#(tt(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# length X -> mark# X, mark# cons(X1, X2) -> mark# X1)
       (mark# length X -> mark# X, mark# zeros() -> a__zeros#())
       (mark# length X -> mark# X, mark# s X -> mark# X)
       (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) -> a__take#(mark X1, mark X2))
       (mark# length X -> mark# X, mark# and(X1, X2) -> mark# X1)
       (mark# length X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
       (mark# length X -> mark# X, mark# length X -> mark# X)
       (mark# length X -> mark# X, mark# length X -> a__length# mark X)
       (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(s M, cons(N, IL)) -> mark# N)
       (mark# length X -> a__length# mark X, a__length# cons(N, L) -> mark# L)
       (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__length# mark L)
       (a__length# cons(N, L) -> mark# L, mark# cons(X1, X2) -> mark# X1)
       (a__length# cons(N, L) -> mark# L, mark# zeros() -> a__zeros#())
       (a__length# cons(N, L) -> mark# L, mark# s X -> mark# X)
       (a__length# cons(N, L) -> mark# L, mark# take(X1, X2) -> mark# X1)
       (a__length# cons(N, L) -> mark# L, mark# take(X1, X2) -> mark# X2)
       (a__length# cons(N, L) -> mark# L, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
       (a__length# cons(N, L) -> mark# L, mark# and(X1, X2) -> mark# X1)
       (a__length# cons(N, L) -> mark# L, mark# and(X1, X2) -> a__and#(mark X1, X2))
       (a__length# cons(N, L) -> mark# L, mark# length X -> mark# X)
       (a__length# cons(N, L) -> mark# L, mark# length X -> a__length# mark X)
       (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
       (mark# and(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
       (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
       (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
       (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
       (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
       (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
       (mark# and(X1, X2) -> mark# X1, mark# length X -> mark# X)
       (mark# and(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)
       (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
       (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
       (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
       (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
       (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
       (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
       (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
       (mark# cons(X1, X2) -> mark# X1, mark# length X -> mark# X)
       (mark# cons(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)}
      EDG:
       {(mark# take(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)
        (mark# take(X1, X2) -> mark# X1, mark# length X -> mark# X)
        (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
        (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
        (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__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# s X -> mark# X)
        (mark# take(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
        (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
        (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X)
        (a__length# cons(N, L) -> a__length# mark L, a__length# cons(N, L) -> a__length# mark L)
        (a__length# cons(N, L) -> a__length# mark L, a__length# cons(N, L) -> mark# L)
        (mark# take(X1, X2) -> mark# X2, mark# length X -> a__length# mark X)
        (mark# take(X1, X2) -> mark# X2, mark# length X -> mark# X)
        (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
        (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
        (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
        (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2)
        (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1)
        (mark# take(X1, X2) -> mark# X2, mark# s X -> mark# X)
        (mark# take(X1, X2) -> mark# X2, mark# zeros() -> a__zeros#())
        (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
        (a__take#(s M, cons(N, IL)) -> mark# N, mark# length X -> a__length# mark X)
        (a__take#(s M, cons(N, IL)) -> mark# N, mark# length X -> mark# X)
        (a__take#(s M, cons(N, IL)) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
        (a__take#(s M, cons(N, IL)) -> mark# N, mark# and(X1, X2) -> mark# X1)
        (a__take#(s M, cons(N, IL)) -> mark# N, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
        (a__take#(s M, cons(N, IL)) -> mark# N, mark# take(X1, X2) -> mark# X2)
        (a__take#(s M, cons(N, IL)) -> mark# N, mark# take(X1, X2) -> mark# X1)
        (a__take#(s M, cons(N, IL)) -> mark# N, mark# s X -> mark# X)
        (a__take#(s M, cons(N, IL)) -> mark# N, mark# zeros() -> a__zeros#())
        (a__take#(s M, cons(N, IL)) -> mark# N, mark# cons(X1, X2) -> mark# X1)
        (mark# s X -> mark# X, mark# length X -> a__length# mark X)
        (mark# s X -> mark# X, mark# length X -> mark# X)
        (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
        (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1)
        (mark# s X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
        (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X2)
        (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1)
        (mark# s X -> mark# X, mark# s X -> mark# X)
        (mark# s X -> mark# X, mark# zeros() -> a__zeros#())
        (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (a__and#(tt(), X) -> mark# X, mark# length X -> a__length# mark X)
        (a__and#(tt(), X) -> mark# X, mark# length X -> mark# X)
        (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
        (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
        (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
        (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X2)
        (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X1)
        (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X)
        (a__and#(tt(), X) -> mark# X, mark# zeros() -> a__zeros#())
        (a__and#(tt(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (mark# length X -> mark# X, mark# cons(X1, X2) -> mark# X1)
        (mark# length X -> mark# X, mark# zeros() -> a__zeros#())
        (mark# length X -> mark# X, mark# s X -> mark# X)
        (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) -> a__take#(mark X1, mark X2))
        (mark# length X -> mark# X, mark# and(X1, X2) -> mark# X1)
        (mark# length X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
        (mark# length X -> mark# X, mark# length X -> mark# X)
        (mark# length X -> mark# X, mark# length X -> a__length# mark X)
        (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(s M, cons(N, IL)) -> mark# N)
        (mark# length X -> a__length# mark X, a__length# cons(N, L) -> mark# L)
        (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__length# mark L)
        (a__length# cons(N, L) -> mark# L, mark# cons(X1, X2) -> mark# X1)
        (a__length# cons(N, L) -> mark# L, mark# zeros() -> a__zeros#())
        (a__length# cons(N, L) -> mark# L, mark# s X -> mark# X)
        (a__length# cons(N, L) -> mark# L, mark# take(X1, X2) -> mark# X1)
        (a__length# cons(N, L) -> mark# L, mark# take(X1, X2) -> mark# X2)
        (a__length# cons(N, L) -> mark# L, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
        (a__length# cons(N, L) -> mark# L, mark# and(X1, X2) -> mark# X1)
        (a__length# cons(N, L) -> mark# L, mark# and(X1, X2) -> a__and#(mark X1, X2))
        (a__length# cons(N, L) -> mark# L, mark# length X -> mark# X)
        (a__length# cons(N, L) -> mark# L, mark# length X -> a__length# mark X)
        (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
        (mark# and(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
        (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X)
        (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
        (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
        (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
        (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
        (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
        (mark# and(X1, X2) -> mark# X1, mark# length X -> mark# X)
        (mark# and(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)
        (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
        (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
        (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
        (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
        (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
        (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
        (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
        (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
        (mark# cons(X1, X2) -> mark# X1, mark# length X -> mark# X)
        (mark# cons(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)}
       STATUS:
        arrows: 0.510204
        SCCS (1):
         Scc:
          {        mark# cons(X1, X2) -> mark# X1,
                            mark# s X -> mark# X,
                   mark# take(X1, X2) -> mark# X1,
                   mark# take(X1, X2) -> mark# X2,
                   mark# take(X1, X2) -> a__take#(mark X1, mark X2),
                    mark# and(X1, X2) -> mark# X1,
                    mark# and(X1, X2) -> a__and#(mark X1, X2),
                       mark# length X -> mark# X,
                       mark# length X -> a__length# mark X,
                     a__and#(tt(), X) -> mark# X,
                a__length# cons(N, L) -> mark# L,
                a__length# cons(N, L) -> a__length# mark L,
           a__take#(s M, cons(N, IL)) -> mark# N}
         
         SCC (13):
          Strict:
           {        mark# cons(X1, X2) -> mark# X1,
                             mark# s X -> mark# X,
                    mark# take(X1, X2) -> mark# X1,
                    mark# take(X1, X2) -> mark# X2,
                    mark# take(X1, X2) -> a__take#(mark X1, mark X2),
                     mark# and(X1, X2) -> mark# X1,
                     mark# and(X1, X2) -> a__and#(mark X1, X2),
                        mark# length X -> mark# X,
                        mark# length X -> a__length# mark X,
                      a__and#(tt(), X) -> mark# X,
                 a__length# cons(N, L) -> mark# L,
                 a__length# cons(N, L) -> a__length# mark L,
            a__take#(s M, cons(N, IL)) -> mark# N}
          Weak:
          {               a__zeros() -> cons(0(), zeros()),
                          a__zeros() -> zeros(),
                   mark cons(X1, X2) -> cons(mark X1, X2),
                            mark 0() -> 0(),
                        mark zeros() -> a__zeros(),
                           mark tt() -> tt(),
                          mark nil() -> nil(),
                            mark s X -> s mark X,
                   mark take(X1, X2) -> a__take(mark X1, mark X2),
                    mark and(X1, X2) -> a__and(mark X1, X2),
                       mark length X -> a__length mark X,
                      a__and(X1, X2) -> and(X1, X2),
                     a__and(tt(), X) -> mark X,
                         a__length X -> length X,
                a__length cons(N, L) -> s a__length mark L,
                     a__length nil() -> 0(),
                     a__take(X1, X2) -> take(X1, X2),
                    a__take(0(), IL) -> nil(),
           a__take(s M, cons(N, IL)) -> cons(mark N, take(M, IL))}
          Open