MAYBE
Time: 0.019718
TRS:
 {          a__adx X -> adx X,
   a__adx cons(X, Y) -> a__incr cons(X, adx Y),
          a__zeros() -> cons(0(), zeros()),
          a__zeros() -> zeros(),
           a__nats() -> a__adx a__zeros(),
           a__nats() -> nats(),
           a__incr X -> incr X,
  a__incr cons(X, Y) -> cons(s X, incr Y),
   mark cons(X1, X2) -> cons(X1, X2),
            mark 0() -> 0(),
        mark zeros() -> a__zeros(),
            mark s X -> s X,
         mark incr X -> a__incr mark X,
          mark adx X -> a__adx mark X,
         mark nats() -> a__nats(),
           mark hd X -> a__hd mark X,
           mark tl X -> a__tl mark X,
             a__hd X -> hd X,
    a__hd cons(X, Y) -> mark X,
             a__tl X -> tl X,
    a__tl cons(X, Y) -> mark Y}
 DP:
  DP:
   {a__adx# cons(X, Y) -> a__incr# cons(X, adx Y),
            a__nats#() -> a__adx# a__zeros(),
            a__nats#() -> a__zeros#(),
         mark# zeros() -> a__zeros#(),
          mark# incr X -> a__incr# mark X,
          mark# incr X -> mark# X,
           mark# adx X -> a__adx# mark X,
           mark# adx X -> mark# X,
          mark# nats() -> a__nats#(),
            mark# hd X -> mark# X,
            mark# hd X -> a__hd# mark X,
            mark# tl X -> mark# X,
            mark# tl X -> a__tl# mark X,
     a__hd# cons(X, Y) -> mark# X,
     a__tl# cons(X, Y) -> mark# Y}
  TRS:
  {          a__adx X -> adx X,
    a__adx cons(X, Y) -> a__incr cons(X, adx Y),
           a__zeros() -> cons(0(), zeros()),
           a__zeros() -> zeros(),
            a__nats() -> a__adx a__zeros(),
            a__nats() -> nats(),
            a__incr X -> incr X,
   a__incr cons(X, Y) -> cons(s X, incr Y),
    mark cons(X1, X2) -> cons(X1, X2),
             mark 0() -> 0(),
         mark zeros() -> a__zeros(),
             mark s X -> s X,
          mark incr X -> a__incr mark X,
           mark adx X -> a__adx mark X,
          mark nats() -> a__nats(),
            mark hd X -> a__hd mark X,
            mark tl X -> a__tl mark X,
              a__hd X -> hd X,
     a__hd cons(X, Y) -> mark X,
              a__tl X -> tl X,
     a__tl cons(X, Y) -> mark Y}
  UR:
   {          a__adx X -> adx X,
     a__adx cons(X, Y) -> a__incr cons(X, adx Y),
            a__zeros() -> cons(0(), zeros()),
            a__zeros() -> zeros(),
             a__nats() -> a__adx a__zeros(),
             a__nats() -> nats(),
             a__incr X -> incr X,
    a__incr cons(X, Y) -> cons(s X, incr Y),
     mark cons(X1, X2) -> cons(X1, X2),
              mark 0() -> 0(),
          mark zeros() -> a__zeros(),
              mark s X -> s X,
           mark incr X -> a__incr mark X,
            mark adx X -> a__adx mark X,
           mark nats() -> a__nats(),
             mark hd X -> a__hd mark X,
             mark tl X -> a__tl mark X,
               a__hd X -> hd X,
      a__hd cons(X, Y) -> mark X,
               a__tl X -> tl X,
      a__tl cons(X, Y) -> mark Y}
   EDG:
    {(mark# hd X -> a__hd# mark X, a__hd# cons(X, Y) -> mark# X)
     (mark# nats() -> a__nats#(), a__nats#() -> a__zeros#())
     (mark# nats() -> a__nats#(), a__nats#() -> a__adx# a__zeros())
     (mark# adx X -> mark# X, mark# tl X -> a__tl# mark X)
     (mark# adx X -> mark# X, mark# tl X -> mark# X)
     (mark# adx X -> mark# X, mark# hd X -> a__hd# mark X)
     (mark# adx X -> mark# X, mark# hd X -> mark# X)
     (mark# adx X -> mark# X, mark# nats() -> a__nats#())
     (mark# adx X -> mark# X, mark# adx X -> mark# X)
     (mark# adx X -> mark# X, mark# adx X -> a__adx# mark X)
     (mark# adx X -> mark# X, mark# incr X -> mark# X)
     (mark# adx X -> mark# X, mark# incr X -> a__incr# mark X)
     (mark# adx X -> mark# X, mark# zeros() -> a__zeros#())
     (mark# tl X -> mark# X, mark# tl X -> a__tl# mark X)
     (mark# tl X -> mark# X, mark# tl X -> mark# X)
     (mark# tl X -> mark# X, mark# hd X -> a__hd# mark X)
     (mark# tl X -> mark# X, mark# hd X -> mark# X)
     (mark# tl X -> mark# X, mark# nats() -> a__nats#())
     (mark# tl X -> mark# X, mark# adx X -> mark# X)
     (mark# tl X -> mark# X, mark# adx X -> a__adx# mark X)
     (mark# tl X -> mark# X, mark# incr X -> mark# X)
     (mark# tl X -> mark# X, mark# incr X -> a__incr# mark X)
     (mark# tl X -> mark# X, mark# zeros() -> a__zeros#())
     (a__nats#() -> a__adx# a__zeros(), a__adx# cons(X, Y) -> a__incr# cons(X, adx Y))
     (a__hd# cons(X, Y) -> mark# X, mark# zeros() -> a__zeros#())
     (a__hd# cons(X, Y) -> mark# X, mark# incr X -> a__incr# mark X)
     (a__hd# cons(X, Y) -> mark# X, mark# incr X -> mark# X)
     (a__hd# cons(X, Y) -> mark# X, mark# adx X -> a__adx# mark X)
     (a__hd# cons(X, Y) -> mark# X, mark# adx X -> mark# X)
     (a__hd# cons(X, Y) -> mark# X, mark# nats() -> a__nats#())
     (a__hd# cons(X, Y) -> mark# X, mark# hd X -> mark# X)
     (a__hd# cons(X, Y) -> mark# X, mark# hd X -> a__hd# mark X)
     (a__hd# cons(X, Y) -> mark# X, mark# tl X -> mark# X)
     (a__hd# cons(X, Y) -> mark# X, mark# tl X -> a__tl# mark X)
     (mark# hd X -> mark# X, mark# zeros() -> a__zeros#())
     (mark# hd X -> mark# X, mark# incr X -> a__incr# mark X)
     (mark# hd X -> mark# X, mark# incr X -> mark# X)
     (mark# hd X -> mark# X, mark# adx X -> a__adx# mark X)
     (mark# hd X -> mark# X, mark# adx X -> mark# X)
     (mark# hd X -> mark# X, mark# nats() -> a__nats#())
     (mark# hd X -> mark# X, mark# hd X -> mark# X)
     (mark# hd X -> mark# X, mark# hd X -> a__hd# mark X)
     (mark# hd X -> mark# X, mark# tl X -> mark# X)
     (mark# hd X -> mark# X, mark# tl X -> a__tl# mark X)
     (mark# incr X -> mark# X, mark# zeros() -> a__zeros#())
     (mark# incr X -> mark# X, mark# incr X -> a__incr# mark X)
     (mark# incr X -> mark# X, mark# incr X -> mark# X)
     (mark# incr X -> mark# X, mark# adx X -> a__adx# mark X)
     (mark# incr X -> mark# X, mark# adx X -> mark# X)
     (mark# incr X -> mark# X, mark# nats() -> a__nats#())
     (mark# incr X -> mark# X, mark# hd X -> mark# X)
     (mark# incr X -> mark# X, mark# hd X -> a__hd# mark X)
     (mark# incr X -> mark# X, mark# tl X -> mark# X)
     (mark# incr X -> mark# X, mark# tl X -> a__tl# mark X)
     (mark# tl X -> a__tl# mark X, a__tl# cons(X, Y) -> mark# Y)
     (mark# adx X -> a__adx# mark X, a__adx# cons(X, Y) -> a__incr# cons(X, adx Y))
     (a__tl# cons(X, Y) -> mark# Y, mark# zeros() -> a__zeros#())
     (a__tl# cons(X, Y) -> mark# Y, mark# incr X -> a__incr# mark X)
     (a__tl# cons(X, Y) -> mark# Y, mark# incr X -> mark# X)
     (a__tl# cons(X, Y) -> mark# Y, mark# adx X -> a__adx# mark X)
     (a__tl# cons(X, Y) -> mark# Y, mark# adx X -> mark# X)
     (a__tl# cons(X, Y) -> mark# Y, mark# nats() -> a__nats#())
     (a__tl# cons(X, Y) -> mark# Y, mark# hd X -> mark# X)
     (a__tl# cons(X, Y) -> mark# Y, mark# hd X -> a__hd# mark X)
     (a__tl# cons(X, Y) -> mark# Y, mark# tl X -> mark# X)
     (a__tl# cons(X, Y) -> mark# Y, mark# tl X -> a__tl# mark X)}
    STATUS:
     arrows: 0.706667
     SCCS (1):
      Scc:
       {     mark# incr X -> mark# X,
              mark# adx X -> mark# X,
               mark# hd X -> mark# X,
               mark# hd X -> a__hd# mark X,
               mark# tl X -> mark# X,
               mark# tl X -> a__tl# mark X,
        a__hd# cons(X, Y) -> mark# X,
        a__tl# cons(X, Y) -> mark# Y}
      
      SCC (8):
       Strict:
        {     mark# incr X -> mark# X,
               mark# adx X -> mark# X,
                mark# hd X -> mark# X,
                mark# hd X -> a__hd# mark X,
                mark# tl X -> mark# X,
                mark# tl X -> a__tl# mark X,
         a__hd# cons(X, Y) -> mark# X,
         a__tl# cons(X, Y) -> mark# Y}
       Weak:
       {          a__adx X -> adx X,
         a__adx cons(X, Y) -> a__incr cons(X, adx Y),
                a__zeros() -> cons(0(), zeros()),
                a__zeros() -> zeros(),
                 a__nats() -> a__adx a__zeros(),
                 a__nats() -> nats(),
                 a__incr X -> incr X,
        a__incr cons(X, Y) -> cons(s X, incr Y),
         mark cons(X1, X2) -> cons(X1, X2),
                  mark 0() -> 0(),
              mark zeros() -> a__zeros(),
                  mark s X -> s X,
               mark incr X -> a__incr mark X,
                mark adx X -> a__adx mark X,
               mark nats() -> a__nats(),
                 mark hd X -> a__hd mark X,
                 mark tl X -> a__tl mark X,
                   a__hd X -> hd X,
          a__hd cons(X, Y) -> mark X,
                   a__tl X -> tl X,
          a__tl cons(X, Y) -> mark Y}
       Open