MAYBE
Time: 0.009911
TRS:
 {             incr X -> n__incr X,
           incr nil() -> nil(),
      incr cons(X, L) -> cons(s X, n__incr activate L),
           activate X -> X,
   activate n__incr X -> incr activate X,
    activate n__adx X -> adx activate X,
  activate n__zeros() -> zeros(),
                adx X -> n__adx X,
            adx nil() -> nil(),
       adx cons(X, L) -> incr cons(X, n__adx activate L),
              zeros() -> cons(0(), n__zeros()),
              zeros() -> n__zeros(),
               nats() -> adx zeros(),
      head cons(X, L) -> X,
      tail cons(X, L) -> activate L}
 DP:
  DP:
   {    incr# cons(X, L) -> activate# L,
     activate# n__incr X -> incr# activate X,
     activate# n__incr X -> activate# X,
      activate# n__adx X -> activate# X,
      activate# n__adx X -> adx# activate X,
    activate# n__zeros() -> zeros#(),
         adx# cons(X, L) -> incr# cons(X, n__adx activate L),
         adx# cons(X, L) -> activate# L,
                 nats#() -> adx# zeros(),
                 nats#() -> zeros#(),
        tail# cons(X, L) -> activate# L}
  TRS:
  {             incr X -> n__incr X,
            incr nil() -> nil(),
       incr cons(X, L) -> cons(s X, n__incr activate L),
            activate X -> X,
    activate n__incr X -> incr activate X,
     activate n__adx X -> adx activate X,
   activate n__zeros() -> zeros(),
                 adx X -> n__adx X,
             adx nil() -> nil(),
        adx cons(X, L) -> incr cons(X, n__adx activate L),
               zeros() -> cons(0(), n__zeros()),
               zeros() -> n__zeros(),
                nats() -> adx zeros(),
       head cons(X, L) -> X,
       tail cons(X, L) -> activate L}
  UR:
   {             incr X -> n__incr X,
             incr nil() -> nil(),
        incr cons(X, L) -> cons(s X, n__incr activate L),
             activate X -> X,
     activate n__incr X -> incr activate X,
      activate n__adx X -> adx activate X,
    activate n__zeros() -> zeros(),
                  adx X -> n__adx X,
              adx nil() -> nil(),
         adx cons(X, L) -> incr cons(X, n__adx activate L),
                zeros() -> cons(0(), n__zeros()),
                zeros() -> n__zeros()}
   EDG:
    {(activate# n__adx X -> activate# X, activate# n__zeros() -> zeros#())
     (activate# n__adx X -> activate# X, activate# n__adx X -> adx# activate X)
     (activate# n__adx X -> activate# X, activate# n__adx X -> activate# X)
     (activate# n__adx X -> activate# X, activate# n__incr X -> activate# X)
     (activate# n__adx X -> activate# X, activate# n__incr X -> incr# activate X)
     (adx# cons(X, L) -> activate# L, activate# n__zeros() -> zeros#())
     (adx# cons(X, L) -> activate# L, activate# n__adx X -> adx# activate X)
     (adx# cons(X, L) -> activate# L, activate# n__adx X -> activate# X)
     (adx# cons(X, L) -> activate# L, activate# n__incr X -> activate# X)
     (adx# cons(X, L) -> activate# L, activate# n__incr X -> incr# activate X)
     (nats#() -> adx# zeros(), adx# cons(X, L) -> activate# L)
     (nats#() -> adx# zeros(), adx# cons(X, L) -> incr# cons(X, n__adx activate L))
     (activate# n__incr X -> incr# activate X, incr# cons(X, L) -> activate# L)
     (activate# n__adx X -> adx# activate X, adx# cons(X, L) -> incr# cons(X, n__adx activate L))
     (activate# n__adx X -> adx# activate X, adx# cons(X, L) -> activate# L)
     (adx# cons(X, L) -> incr# cons(X, n__adx activate L), incr# cons(X, L) -> activate# L)
     (tail# cons(X, L) -> activate# L, activate# n__incr X -> incr# activate X)
     (tail# cons(X, L) -> activate# L, activate# n__incr X -> activate# X)
     (tail# cons(X, L) -> activate# L, activate# n__adx X -> activate# X)
     (tail# cons(X, L) -> activate# L, activate# n__adx X -> adx# activate X)
     (tail# cons(X, L) -> activate# L, activate# n__zeros() -> zeros#())
     (incr# cons(X, L) -> activate# L, activate# n__incr X -> incr# activate X)
     (incr# cons(X, L) -> activate# L, activate# n__incr X -> activate# X)
     (incr# cons(X, L) -> activate# L, activate# n__adx X -> activate# X)
     (incr# cons(X, L) -> activate# L, activate# n__adx X -> adx# activate X)
     (incr# cons(X, L) -> activate# L, activate# n__zeros() -> zeros#())
     (activate# n__incr X -> activate# X, activate# n__incr X -> incr# activate X)
     (activate# n__incr X -> activate# X, activate# n__incr X -> activate# X)
     (activate# n__incr X -> activate# X, activate# n__adx X -> activate# X)
     (activate# n__incr X -> activate# X, activate# n__adx X -> adx# activate X)
     (activate# n__incr X -> activate# X, activate# n__zeros() -> zeros#())}
    STATUS:
     arrows: 0.743802
     SCCS (1):
      Scc:
       {   incr# cons(X, L) -> activate# L,
        activate# n__incr X -> incr# activate X,
        activate# n__incr X -> activate# X,
         activate# n__adx X -> activate# X,
         activate# n__adx X -> adx# activate X,
            adx# cons(X, L) -> incr# cons(X, n__adx activate L),
            adx# cons(X, L) -> activate# L}
      
      
      
      
      SCC (7):
       Strict:
        {   incr# cons(X, L) -> activate# L,
         activate# n__incr X -> incr# activate X,
         activate# n__incr X -> activate# X,
          activate# n__adx X -> activate# X,
          activate# n__adx X -> adx# activate X,
             adx# cons(X, L) -> incr# cons(X, n__adx activate L),
             adx# cons(X, L) -> activate# L}
       Weak:
       {             incr X -> n__incr X,
                 incr nil() -> nil(),
            incr cons(X, L) -> cons(s X, n__incr activate L),
                 activate X -> X,
         activate n__incr X -> incr activate X,
          activate n__adx X -> adx activate X,
        activate n__zeros() -> zeros(),
                      adx X -> n__adx X,
                  adx nil() -> nil(),
             adx cons(X, L) -> incr cons(X, n__adx activate L),
                    zeros() -> cons(0(), n__zeros()),
                    zeros() -> n__zeros(),
                     nats() -> adx zeros(),
            head cons(X, L) -> X,
            tail cons(X, L) -> activate L}
       Open