MAYBE
Time: 0.010518
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 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()}
 DP:
  DP:
   {   mark# cons(X1, X2) -> mark# X1,
            mark# zeros() -> a__zeros#(),
                mark# s X -> mark# X,
        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}
  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 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()}
  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 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()}
   EDG:
    {(mark# cons(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# length X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (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# 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# 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# 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# 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# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X)
     (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)
     (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# 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)
     (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# 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)}
    STATUS:
     arrows: 0.530000
     SCCS (1):
      Scc:
       {   mark# cons(X1, X2) -> mark# X1,
                    mark# s X -> mark# X,
            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}
      
      SCC (9):
       Strict:
        {   mark# cons(X1, X2) -> mark# X1,
                     mark# s X -> mark# X,
             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}
       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 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()}
       Open