MAYBE
Time: 0.001900
TRS:
 {            zeros() -> cons(0(), n__zeros()),
              zeros() -> n__zeros(),
           activate X -> X,
  activate n__zeros() -> zeros(),
         and(tt(), X) -> activate X,
    length cons(N, L) -> s length activate L,
         length nil() -> 0()}
 DP:
  DP:
   {activate# n__zeros() -> zeros#(),
           and#(tt(), X) -> activate# X,
      length# cons(N, L) -> activate# L,
      length# cons(N, L) -> length# activate L}
  TRS:
  {            zeros() -> cons(0(), n__zeros()),
               zeros() -> n__zeros(),
            activate X -> X,
   activate n__zeros() -> zeros(),
          and(tt(), X) -> activate X,
     length cons(N, L) -> s length activate L,
          length nil() -> 0()}
  EDG:
   {(length# cons(N, L) -> activate# L, activate# n__zeros() -> zeros#())
    (length# cons(N, L) -> length# activate L, length# cons(N, L) -> activate# L)
    (length# cons(N, L) -> length# activate L, length# cons(N, L) -> length# activate L)
    (and#(tt(), X) -> activate# X, activate# n__zeros() -> zeros#())}
   EDG:
    {(length# cons(N, L) -> activate# L, activate# n__zeros() -> zeros#())
     (length# cons(N, L) -> length# activate L, length# cons(N, L) -> activate# L)
     (length# cons(N, L) -> length# activate L, length# cons(N, L) -> length# activate L)
     (and#(tt(), X) -> activate# X, activate# n__zeros() -> zeros#())}
    EDG:
     {(length# cons(N, L) -> activate# L, activate# n__zeros() -> zeros#())
      (length# cons(N, L) -> length# activate L, length# cons(N, L) -> activate# L)
      (length# cons(N, L) -> length# activate L, length# cons(N, L) -> length# activate L)
      (and#(tt(), X) -> activate# X, activate# n__zeros() -> zeros#())}
     STATUS:
      arrows: 0.750000
      SCCS (1):
       Scc:
        {length# cons(N, L) -> length# activate L}
       
       SCC (1):
        Strict:
         {length# cons(N, L) -> length# activate L}
        Weak:
        {            zeros() -> cons(0(), n__zeros()),
                     zeros() -> n__zeros(),
                  activate X -> X,
         activate n__zeros() -> zeros(),
                and(tt(), X) -> activate X,
           length cons(N, L) -> s length activate L,
                length nil() -> 0()}
        Open