MAYBE
Time: 0.008905
TRS:
 {          a__zeros() -> cons(0(), zeros()),
            a__zeros() -> zeros(),
        a__U12(X1, X2) -> U12(X1, X2),
       a__U12(tt(), L) -> s a__length mark L,
        a__U11(X1, X2) -> U11(X1, X2),
       a__U11(tt(), L) -> a__U12(tt(), L),
           a__length X -> length X,
  a__length cons(N, L) -> a__U11(tt(), L),
       a__length nil() -> 0(),
     mark cons(X1, X2) -> cons(mark X1, X2),
              mark 0() -> 0(),
          mark zeros() -> a__zeros(),
             mark tt() -> tt(),
              mark s X -> s mark X,
            mark nil() -> nil(),
      mark U11(X1, X2) -> a__U11(mark X1, X2),
      mark U12(X1, X2) -> a__U12(mark X1, X2),
         mark length X -> a__length mark X}
 DP:
  DP:
   {     a__U12#(tt(), L) -> a__length# mark L,
         a__U12#(tt(), L) -> mark# L,
         a__U11#(tt(), L) -> a__U12#(tt(), L),
    a__length# cons(N, L) -> a__U11#(tt(), L),
       mark# cons(X1, X2) -> mark# X1,
            mark# zeros() -> a__zeros#(),
                mark# s X -> mark# X,
        mark# U11(X1, X2) -> a__U11#(mark X1, X2),
        mark# U11(X1, X2) -> mark# X1,
        mark# U12(X1, X2) -> a__U12#(mark X1, X2),
        mark# U12(X1, X2) -> mark# X1,
           mark# length X -> a__length# mark X,
           mark# length X -> mark# X}
  TRS:
  {          a__zeros() -> cons(0(), zeros()),
             a__zeros() -> zeros(),
         a__U12(X1, X2) -> U12(X1, X2),
        a__U12(tt(), L) -> s a__length mark L,
         a__U11(X1, X2) -> U11(X1, X2),
        a__U11(tt(), L) -> a__U12(tt(), L),
            a__length X -> length X,
   a__length cons(N, L) -> a__U11(tt(), L),
        a__length nil() -> 0(),
      mark cons(X1, X2) -> cons(mark X1, X2),
               mark 0() -> 0(),
           mark zeros() -> a__zeros(),
              mark tt() -> tt(),
               mark s X -> s mark X,
             mark nil() -> nil(),
       mark U11(X1, X2) -> a__U11(mark X1, X2),
       mark U12(X1, X2) -> a__U12(mark X1, X2),
          mark length X -> a__length mark X}
  UR:
   {          a__zeros() -> cons(0(), zeros()),
              a__zeros() -> zeros(),
          a__U12(X1, X2) -> U12(X1, X2),
         a__U12(tt(), L) -> s a__length mark L,
          a__U11(X1, X2) -> U11(X1, X2),
         a__U11(tt(), L) -> a__U12(tt(), L),
             a__length X -> length X,
    a__length cons(N, L) -> a__U11(tt(), L),
         a__length nil() -> 0(),
       mark cons(X1, X2) -> cons(mark X1, X2),
                mark 0() -> 0(),
            mark zeros() -> a__zeros(),
               mark tt() -> tt(),
                mark s X -> s mark X,
              mark nil() -> nil(),
        mark U11(X1, X2) -> a__U11(mark X1, X2),
        mark U12(X1, X2) -> a__U12(mark X1, X2),
           mark length X -> a__length mark X}
   EDG:
    {(mark# U11(X1, X2) -> a__U11#(mark X1, X2), a__U11#(tt(), L) -> a__U12#(tt(), L))
     (a__U11#(tt(), L) -> a__U12#(tt(), L), a__U12#(tt(), L) -> mark# L)
     (a__U11#(tt(), L) -> a__U12#(tt(), L), a__U12#(tt(), L) -> a__length# mark L)
     (mark# cons(X1, X2) -> mark# X1, mark# length X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (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)
     (mark# U12(X1, X2) -> mark# X1, mark# length X -> mark# X)
     (mark# U12(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)
     (mark# U12(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1)
     (mark# U12(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# U12(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1)
     (mark# U12(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (mark# U12(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# U12(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
     (mark# U12(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# length X -> mark# X, mark# length X -> mark# X)
     (mark# length X -> mark# X, mark# length X -> a__length# mark X)
     (mark# length X -> mark# X, mark# U12(X1, X2) -> mark# X1)
     (mark# length X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# length X -> mark# X, mark# U11(X1, X2) -> mark# X1)
     (mark# length X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (mark# length X -> mark# X, mark# s X -> mark# X)
     (mark# length X -> mark# X, mark# zeros() -> a__zeros#())
     (mark# length X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__U12#(tt(), L) -> a__length# mark L, a__length# cons(N, L) -> a__U11#(tt(), L))
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# zeros() -> a__zeros#())
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (mark# s X -> mark# X, mark# U11(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# s X -> mark# X, mark# U12(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# length X -> a__length# mark X, a__length# cons(N, L) -> a__U11#(tt(), L))
     (mark# U11(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# U11(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#())
     (mark# U11(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1)
     (mark# U11(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# U11(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1)
     (mark# U11(X1, X2) -> mark# X1, mark# length X -> a__length# mark X)
     (mark# U11(X1, X2) -> mark# X1, mark# length X -> mark# X)
     (a__length# cons(N, L) -> a__U11#(tt(), L), a__U11#(tt(), L) -> a__U12#(tt(), L))
     (mark# U12(X1, X2) -> a__U12#(mark X1, X2), a__U12#(tt(), L) -> a__length# mark L)
     (mark# U12(X1, X2) -> a__U12#(mark X1, X2), a__U12#(tt(), L) -> mark# L)
     (a__U12#(tt(), L) -> mark# L, mark# cons(X1, X2) -> mark# X1)
     (a__U12#(tt(), L) -> mark# L, mark# zeros() -> a__zeros#())
     (a__U12#(tt(), L) -> mark# L, mark# s X -> mark# X)
     (a__U12#(tt(), L) -> mark# L, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
     (a__U12#(tt(), L) -> mark# L, mark# U11(X1, X2) -> mark# X1)
     (a__U12#(tt(), L) -> mark# L, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__U12#(tt(), L) -> mark# L, mark# U12(X1, X2) -> mark# X1)
     (a__U12#(tt(), L) -> mark# L, mark# length X -> a__length# mark X)
     (a__U12#(tt(), L) -> mark# L, mark# length X -> mark# X)}
    STATUS:
     arrows: 0.633136
     SCCS (1):
      Scc:
       {     a__U12#(tt(), L) -> a__length# mark L,
             a__U12#(tt(), L) -> mark# L,
             a__U11#(tt(), L) -> a__U12#(tt(), L),
        a__length# cons(N, L) -> a__U11#(tt(), L),
           mark# cons(X1, X2) -> mark# X1,
                    mark# s X -> mark# X,
            mark# U11(X1, X2) -> a__U11#(mark X1, X2),
            mark# U11(X1, X2) -> mark# X1,
            mark# U12(X1, X2) -> a__U12#(mark X1, X2),
            mark# U12(X1, X2) -> mark# X1,
               mark# length X -> a__length# mark X,
               mark# length X -> mark# X}
      
      SCC (12):
       Strict:
        {     a__U12#(tt(), L) -> a__length# mark L,
              a__U12#(tt(), L) -> mark# L,
              a__U11#(tt(), L) -> a__U12#(tt(), L),
         a__length# cons(N, L) -> a__U11#(tt(), L),
            mark# cons(X1, X2) -> mark# X1,
                     mark# s X -> mark# X,
             mark# U11(X1, X2) -> a__U11#(mark X1, X2),
             mark# U11(X1, X2) -> mark# X1,
             mark# U12(X1, X2) -> a__U12#(mark X1, X2),
             mark# U12(X1, X2) -> mark# X1,
                mark# length X -> a__length# mark X,
                mark# length X -> mark# X}
       Weak:
       {          a__zeros() -> cons(0(), zeros()),
                  a__zeros() -> zeros(),
              a__U12(X1, X2) -> U12(X1, X2),
             a__U12(tt(), L) -> s a__length mark L,
              a__U11(X1, X2) -> U11(X1, X2),
             a__U11(tt(), L) -> a__U12(tt(), L),
                 a__length X -> length X,
        a__length cons(N, L) -> a__U11(tt(), L),
             a__length nil() -> 0(),
           mark cons(X1, X2) -> cons(mark X1, X2),
                    mark 0() -> 0(),
                mark zeros() -> a__zeros(),
                   mark tt() -> tt(),
                    mark s X -> s mark X,
                  mark nil() -> nil(),
            mark U11(X1, X2) -> a__U11(mark X1, X2),
            mark U12(X1, X2) -> a__U12(mark X1, X2),
               mark length X -> a__length mark X}
       Open