MAYBE
Time: 0.024438
TRS:
 {              adx X -> n__adx X,
       adx cons(X, Y) -> incr cons(activate X, n__adx activate Y),
              zeros() -> cons(n__0(), n__zeros()),
              zeros() -> n__zeros(),
               nats() -> adx zeros(),
           activate X -> X,
      activate n__0() -> 0(),
  activate n__zeros() -> zeros(),
      activate n__s X -> s X,
   activate n__incr X -> incr X,
    activate n__adx X -> adx X,
               incr X -> n__incr X,
      incr cons(X, Y) -> cons(n__s activate X, n__incr activate Y),
        hd cons(X, Y) -> activate X,
        tl cons(X, Y) -> activate Y,
                  0() -> n__0(),
                  s X -> n__s X}
 DP:
  DP:
   {     adx# cons(X, Y) -> activate# X,
         adx# cons(X, Y) -> activate# Y,
         adx# cons(X, Y) -> incr# cons(activate X, n__adx activate Y),
                 nats#() -> adx# zeros(),
                 nats#() -> zeros#(),
        activate# n__0() -> 0#(),
    activate# n__zeros() -> zeros#(),
        activate# n__s X -> s# X,
     activate# n__incr X -> incr# X,
      activate# n__adx X -> adx# X,
        incr# cons(X, Y) -> activate# X,
        incr# cons(X, Y) -> activate# Y,
          hd# cons(X, Y) -> activate# X,
          tl# cons(X, Y) -> activate# Y}
  TRS:
  {              adx X -> n__adx X,
        adx cons(X, Y) -> incr cons(activate X, n__adx activate Y),
               zeros() -> cons(n__0(), n__zeros()),
               zeros() -> n__zeros(),
                nats() -> adx zeros(),
            activate X -> X,
       activate n__0() -> 0(),
   activate n__zeros() -> zeros(),
       activate n__s X -> s X,
    activate n__incr X -> incr X,
     activate n__adx X -> adx X,
                incr X -> n__incr X,
       incr cons(X, Y) -> cons(n__s activate X, n__incr activate Y),
         hd cons(X, Y) -> activate X,
         tl cons(X, Y) -> activate Y,
                   0() -> n__0(),
                   s X -> n__s X}
  UR:
   {              adx X -> n__adx X,
         adx cons(X, Y) -> incr cons(activate X, n__adx activate Y),
                zeros() -> cons(n__0(), n__zeros()),
                zeros() -> n__zeros(),
             activate X -> X,
        activate n__0() -> 0(),
    activate n__zeros() -> zeros(),
        activate n__s X -> s X,
     activate n__incr X -> incr X,
      activate n__adx X -> adx X,
                 incr X -> n__incr X,
        incr cons(X, Y) -> cons(n__s activate X, n__incr activate Y),
                    0() -> n__0(),
                    s X -> n__s X}
   EDG:
    {(incr# cons(X, Y) -> activate# Y, activate# n__adx X -> adx# X)
     (incr# cons(X, Y) -> activate# Y, activate# n__incr X -> incr# X)
     (incr# cons(X, Y) -> activate# Y, activate# n__s X -> s# X)
     (incr# cons(X, Y) -> activate# Y, activate# n__zeros() -> zeros#())
     (incr# cons(X, Y) -> activate# Y, activate# n__0() -> 0#())
     (adx# cons(X, Y) -> activate# X, activate# n__adx X -> adx# X)
     (adx# cons(X, Y) -> activate# X, activate# n__incr X -> incr# X)
     (adx# cons(X, Y) -> activate# X, activate# n__s X -> s# X)
     (adx# cons(X, Y) -> activate# X, activate# n__zeros() -> zeros#())
     (adx# cons(X, Y) -> activate# X, activate# n__0() -> 0#())
     (activate# n__adx X -> adx# X, adx# cons(X, Y) -> incr# cons(activate X, n__adx activate Y))
     (activate# n__adx X -> adx# X, adx# cons(X, Y) -> activate# Y)
     (activate# n__adx X -> adx# X, adx# cons(X, Y) -> activate# X)
     (hd# cons(X, Y) -> activate# X, activate# n__adx X -> adx# X)
     (hd# cons(X, Y) -> activate# X, activate# n__incr X -> incr# X)
     (hd# cons(X, Y) -> activate# X, activate# n__s X -> s# X)
     (hd# cons(X, Y) -> activate# X, activate# n__zeros() -> zeros#())
     (hd# cons(X, Y) -> activate# X, activate# n__0() -> 0#())
     (nats#() -> adx# zeros(), adx# cons(X, Y) -> incr# cons(activate X, n__adx activate Y))
     (nats#() -> adx# zeros(), adx# cons(X, Y) -> activate# Y)
     (nats#() -> adx# zeros(), adx# cons(X, Y) -> activate# X)
     (adx# cons(X, Y) -> incr# cons(activate X, n__adx activate Y), incr# cons(X, Y) -> activate# X)
     (adx# cons(X, Y) -> incr# cons(activate X, n__adx activate Y), incr# cons(X, Y) -> activate# Y)
     (incr# cons(X, Y) -> activate# X, activate# n__0() -> 0#())
     (incr# cons(X, Y) -> activate# X, activate# n__zeros() -> zeros#())
     (incr# cons(X, Y) -> activate# X, activate# n__s X -> s# X)
     (incr# cons(X, Y) -> activate# X, activate# n__incr X -> incr# X)
     (incr# cons(X, Y) -> activate# X, activate# n__adx X -> adx# X)
     (activate# n__incr X -> incr# X, incr# cons(X, Y) -> activate# X)
     (activate# n__incr X -> incr# X, incr# cons(X, Y) -> activate# Y)
     (tl# cons(X, Y) -> activate# Y, activate# n__0() -> 0#())
     (tl# cons(X, Y) -> activate# Y, activate# n__zeros() -> zeros#())
     (tl# cons(X, Y) -> activate# Y, activate# n__s X -> s# X)
     (tl# cons(X, Y) -> activate# Y, activate# n__incr X -> incr# X)
     (tl# cons(X, Y) -> activate# Y, activate# n__adx X -> adx# X)
     (adx# cons(X, Y) -> activate# Y, activate# n__0() -> 0#())
     (adx# cons(X, Y) -> activate# Y, activate# n__zeros() -> zeros#())
     (adx# cons(X, Y) -> activate# Y, activate# n__s X -> s# X)
     (adx# cons(X, Y) -> activate# Y, activate# n__incr X -> incr# X)
     (adx# cons(X, Y) -> activate# Y, activate# n__adx X -> adx# X)}
    STATUS:
     arrows: 0.795918
     SCCS (1):
      Scc:
       {    adx# cons(X, Y) -> activate# X,
            adx# cons(X, Y) -> activate# Y,
            adx# cons(X, Y) -> incr# cons(activate X, n__adx activate Y),
        activate# n__incr X -> incr# X,
         activate# n__adx X -> adx# X,
           incr# cons(X, Y) -> activate# X,
           incr# cons(X, Y) -> activate# Y}
      
      
      
      
      
      SCC (7):
       Strict:
        {    adx# cons(X, Y) -> activate# X,
             adx# cons(X, Y) -> activate# Y,
             adx# cons(X, Y) -> incr# cons(activate X, n__adx activate Y),
         activate# n__incr X -> incr# X,
          activate# n__adx X -> adx# X,
            incr# cons(X, Y) -> activate# X,
            incr# cons(X, Y) -> activate# Y}
       Weak:
       {              adx X -> n__adx X,
             adx cons(X, Y) -> incr cons(activate X, n__adx activate Y),
                    zeros() -> cons(n__0(), n__zeros()),
                    zeros() -> n__zeros(),
                     nats() -> adx zeros(),
                 activate X -> X,
            activate n__0() -> 0(),
        activate n__zeros() -> zeros(),
            activate n__s X -> s X,
         activate n__incr X -> incr X,
          activate n__adx X -> adx X,
                     incr X -> n__incr X,
            incr cons(X, Y) -> cons(n__s activate X, n__incr activate Y),
              hd cons(X, Y) -> activate X,
              tl cons(X, Y) -> activate Y,
                        0() -> n__0(),
                        s X -> n__s X}
       Open