MAYBE
Time: 1.544607
TRS:
 {            mark nil() -> active nil(),
             mark incr X -> active incr mark X,
       mark cons(X1, X2) -> active cons(mark X1, X2),
                mark s X -> active s mark X,
              mark adx X -> active adx mark X,
            mark zeros() -> active zeros(),
             mark nats() -> active nats(),
                mark 0() -> active 0(),
             mark head X -> active head mark X,
             mark tail X -> active tail mark X,
       active incr nil() -> mark nil(),
  active incr cons(X, L) -> mark cons(s X, incr L),
        active adx nil() -> mark nil(),
   active adx cons(X, L) -> mark incr cons(X, adx L),
          active zeros() -> mark cons(0(), zeros()),
           active nats() -> mark adx zeros(),
  active head cons(X, L) -> mark X,
  active tail cons(X, L) -> mark L,
             incr mark X -> incr X,
           incr active X -> incr X,
       cons(X1, mark X2) -> cons(X1, X2),
     cons(X1, active X2) -> cons(X1, X2),
       cons(mark X1, X2) -> cons(X1, X2),
     cons(active X1, X2) -> cons(X1, X2),
                s mark X -> s X,
              s active X -> s X,
              adx mark X -> adx X,
            adx active X -> adx X,
             head mark X -> head X,
           head active X -> head X,
             tail mark X -> tail X,
           tail active X -> tail X}
 DP:
  DP:
   {            mark# nil() -> active# nil(),
               mark# incr X -> mark# X,
               mark# incr X -> active# incr mark X,
               mark# incr X -> incr# mark X,
         mark# cons(X1, X2) -> mark# X1,
         mark# cons(X1, X2) -> active# cons(mark X1, X2),
         mark# cons(X1, X2) -> cons#(mark X1, X2),
                  mark# s X -> mark# X,
                  mark# s X -> active# s mark X,
                  mark# s X -> s# mark X,
                mark# adx X -> mark# X,
                mark# adx X -> active# adx mark X,
                mark# adx X -> adx# mark X,
              mark# zeros() -> active# zeros(),
               mark# nats() -> active# nats(),
                  mark# 0() -> active# 0(),
               mark# head X -> mark# X,
               mark# head X -> active# head mark X,
               mark# head X -> head# mark X,
               mark# tail X -> mark# X,
               mark# tail X -> active# tail mark X,
               mark# tail X -> tail# mark X,
         active# incr nil() -> mark# nil(),
    active# incr cons(X, L) -> mark# cons(s X, incr L),
    active# incr cons(X, L) -> incr# L,
    active# incr cons(X, L) -> cons#(s X, incr L),
    active# incr cons(X, L) -> s# X,
          active# adx nil() -> mark# nil(),
     active# adx cons(X, L) -> mark# incr cons(X, adx L),
     active# adx cons(X, L) -> incr# cons(X, adx L),
     active# adx cons(X, L) -> cons#(X, adx L),
     active# adx cons(X, L) -> adx# L,
            active# zeros() -> mark# cons(0(), zeros()),
            active# zeros() -> cons#(0(), zeros()),
             active# nats() -> mark# adx zeros(),
             active# nats() -> adx# zeros(),
    active# head cons(X, L) -> mark# X,
    active# tail cons(X, L) -> mark# L,
               incr# mark X -> incr# X,
             incr# active X -> incr# X,
         cons#(X1, mark X2) -> cons#(X1, X2),
       cons#(X1, active X2) -> cons#(X1, X2),
         cons#(mark X1, X2) -> cons#(X1, X2),
       cons#(active X1, X2) -> cons#(X1, X2),
                  s# mark X -> s# X,
                s# active X -> s# X,
                adx# mark X -> adx# X,
              adx# active X -> adx# X,
               head# mark X -> head# X,
             head# active X -> head# X,
               tail# mark X -> tail# X,
             tail# active X -> tail# X}
  TRS:
  {            mark nil() -> active nil(),
              mark incr X -> active incr mark X,
        mark cons(X1, X2) -> active cons(mark X1, X2),
                 mark s X -> active s mark X,
               mark adx X -> active adx mark X,
             mark zeros() -> active zeros(),
              mark nats() -> active nats(),
                 mark 0() -> active 0(),
              mark head X -> active head mark X,
              mark tail X -> active tail mark X,
        active incr nil() -> mark nil(),
   active incr cons(X, L) -> mark cons(s X, incr L),
         active adx nil() -> mark nil(),
    active adx cons(X, L) -> mark incr cons(X, adx L),
           active zeros() -> mark cons(0(), zeros()),
            active nats() -> mark adx zeros(),
   active head cons(X, L) -> mark X,
   active tail cons(X, L) -> mark L,
              incr mark X -> incr X,
            incr active X -> incr X,
        cons(X1, mark X2) -> cons(X1, X2),
      cons(X1, active X2) -> cons(X1, X2),
        cons(mark X1, X2) -> cons(X1, X2),
      cons(active X1, X2) -> cons(X1, X2),
                 s mark X -> s X,
               s active X -> s X,
               adx mark X -> adx X,
             adx active X -> adx X,
              head mark X -> head X,
            head active X -> head X,
              tail mark X -> tail X,
            tail active X -> tail X}
  UR:
   {            mark nil() -> active nil(),
               mark incr X -> active incr mark X,
         mark cons(X1, X2) -> active cons(mark X1, X2),
                  mark s X -> active s mark X,
                mark adx X -> active adx mark X,
              mark zeros() -> active zeros(),
               mark nats() -> active nats(),
                  mark 0() -> active 0(),
               mark head X -> active head mark X,
               mark tail X -> active tail mark X,
         active incr nil() -> mark nil(),
    active incr cons(X, L) -> mark cons(s X, incr L),
          active adx nil() -> mark nil(),
     active adx cons(X, L) -> mark incr cons(X, adx L),
            active zeros() -> mark cons(0(), zeros()),
             active nats() -> mark adx zeros(),
    active head cons(X, L) -> mark X,
    active tail cons(X, L) -> mark L,
               incr mark X -> incr X,
             incr active X -> incr X,
         cons(X1, mark X2) -> cons(X1, X2),
       cons(X1, active X2) -> cons(X1, X2),
         cons(mark X1, X2) -> cons(X1, X2),
       cons(active X1, X2) -> cons(X1, X2),
                  s mark X -> s X,
                s active X -> s X,
                adx mark X -> adx X,
              adx active X -> adx X,
               head mark X -> head X,
             head active X -> head X,
               tail mark X -> tail X,
             tail active X -> tail X}
   EDG:
    {
     (mark# zeros() -> active# zeros(), active# zeros() -> cons#(0(), zeros()))
     (mark# zeros() -> active# zeros(), active# zeros() -> mark# cons(0(), zeros()))
     (active# adx nil() -> mark# nil(), mark# nil() -> active# nil())
     (mark# incr X -> mark# X, mark# tail X -> tail# mark X)
     (mark# incr X -> mark# X, mark# tail X -> active# tail mark X)
     (mark# incr X -> mark# X, mark# tail X -> mark# X)
     (mark# incr X -> mark# X, mark# head X -> head# mark X)
     (mark# incr X -> mark# X, mark# head X -> active# head mark X)
     (mark# incr X -> mark# X, mark# head X -> mark# X)
     (mark# incr X -> mark# X, mark# 0() -> active# 0())
     (mark# incr X -> mark# X, mark# nats() -> active# nats())
     (mark# incr X -> mark# X, mark# zeros() -> active# zeros())
     (mark# incr X -> mark# X, mark# adx X -> adx# mark X)
     (mark# incr X -> mark# X, mark# adx X -> active# adx mark X)
     (mark# incr X -> mark# X, mark# adx X -> mark# X)
     (mark# incr X -> mark# X, mark# s X -> s# mark X)
     (mark# incr X -> mark# X, mark# s X -> active# s mark X)
     (mark# incr X -> mark# X, mark# s X -> mark# X)
     (mark# incr X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# incr X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# incr X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# incr X -> mark# X, mark# incr X -> incr# mark X)
     (mark# incr X -> mark# X, mark# incr X -> active# incr mark X)
     (mark# incr X -> mark# X, mark# incr X -> mark# X)
     (mark# incr X -> mark# X, mark# nil() -> active# nil())
     (mark# adx X -> mark# X, mark# tail X -> tail# mark X)
     (mark# adx X -> mark# X, mark# tail X -> active# tail mark X)
     (mark# adx X -> mark# X, mark# tail X -> mark# X)
     (mark# adx X -> mark# X, mark# head X -> head# mark X)
     (mark# adx X -> mark# X, mark# head X -> active# head mark X)
     (mark# adx X -> mark# X, mark# head X -> mark# X)
     (mark# adx X -> mark# X, mark# 0() -> active# 0())
     (mark# adx X -> mark# X, mark# nats() -> active# nats())
     (mark# adx X -> mark# X, mark# zeros() -> active# zeros())
     (mark# adx X -> mark# X, mark# adx X -> adx# mark X)
     (mark# adx X -> mark# X, mark# adx X -> active# adx mark X)
     (mark# adx X -> mark# X, mark# adx X -> mark# X)
     (mark# adx X -> mark# X, mark# s X -> s# mark X)
     (mark# adx X -> mark# X, mark# s X -> active# s mark X)
     (mark# adx X -> mark# X, mark# s X -> mark# X)
     (mark# adx X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# adx X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# adx X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# adx X -> mark# X, mark# incr X -> incr# mark X)
     (mark# adx X -> mark# X, mark# incr X -> active# incr mark X)
     (mark# adx X -> mark# X, mark# incr X -> mark# X)
     (mark# adx X -> mark# X, mark# nil() -> active# nil())
     (mark# tail X -> mark# X, mark# tail X -> tail# mark X)
     (mark# tail X -> mark# X, mark# tail X -> active# tail mark X)
     (mark# tail X -> mark# X, mark# tail X -> mark# X)
     (mark# tail X -> mark# X, mark# head X -> head# mark X)
     (mark# tail X -> mark# X, mark# head X -> active# head mark X)
     (mark# tail X -> mark# X, mark# head X -> mark# X)
     (mark# tail X -> mark# X, mark# 0() -> active# 0())
     (mark# tail X -> mark# X, mark# nats() -> active# nats())
     (mark# tail X -> mark# X, mark# zeros() -> active# zeros())
     (mark# tail X -> mark# X, mark# adx X -> adx# mark X)
     (mark# tail X -> mark# X, mark# adx X -> active# adx mark X)
     (mark# tail X -> mark# X, mark# adx X -> mark# X)
     (mark# tail X -> mark# X, mark# s X -> s# mark X)
     (mark# tail X -> mark# X, mark# s X -> active# s mark X)
     (mark# tail X -> mark# X, mark# s X -> mark# X)
     (mark# tail X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# tail X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# tail X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# tail X -> mark# X, mark# incr X -> incr# mark X)
     (mark# tail X -> mark# X, mark# incr X -> active# incr mark X)
     (mark# tail X -> mark# X, mark# incr X -> mark# X)
     (mark# tail X -> mark# X, mark# nil() -> active# nil())
     (active# head cons(X, L) -> mark# X, mark# tail X -> tail# mark X)
     (active# head cons(X, L) -> mark# X, mark# tail X -> active# tail mark X)
     (active# head cons(X, L) -> mark# X, mark# tail X -> mark# X)
     (active# head cons(X, L) -> mark# X, mark# head X -> head# mark X)
     (active# head cons(X, L) -> mark# X, mark# head X -> active# head mark X)
     (active# head cons(X, L) -> mark# X, mark# head X -> mark# X)
     (active# head cons(X, L) -> mark# X, mark# 0() -> active# 0())
     (active# head cons(X, L) -> mark# X, mark# nats() -> active# nats())
     (active# head cons(X, L) -> mark# X, mark# zeros() -> active# zeros())
     (active# head cons(X, L) -> mark# X, mark# adx X -> adx# mark X)
     (active# head cons(X, L) -> mark# X, mark# adx X -> active# adx mark X)
     (active# head cons(X, L) -> mark# X, mark# adx X -> mark# X)
     (active# head cons(X, L) -> mark# X, mark# s X -> s# mark X)
     (active# head cons(X, L) -> mark# X, mark# s X -> active# s mark X)
     (active# head cons(X, L) -> mark# X, mark# s X -> mark# X)
     (active# head cons(X, L) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# head cons(X, L) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# head cons(X, L) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (active# head cons(X, L) -> mark# X, mark# incr X -> incr# mark X)
     (active# head cons(X, L) -> mark# X, mark# incr X -> active# incr mark X)
     (active# head cons(X, L) -> mark# X, mark# incr X -> mark# X)
     (active# head cons(X, L) -> mark# X, mark# nil() -> active# nil())
     (mark# head X -> active# head mark X, active# tail cons(X, L) -> mark# L)
     (mark# head X -> active# head mark X, active# head cons(X, L) -> mark# X)
     (mark# head X -> active# head mark X, active# nats() -> adx# zeros())
     (mark# head X -> active# head mark X, active# nats() -> mark# adx zeros())
     (mark# head X -> active# head mark X, active# zeros() -> cons#(0(), zeros()))
     (mark# head X -> active# head mark X, active# zeros() -> mark# cons(0(), zeros()))
     (mark# head X -> active# head mark X, active# adx cons(X, L) -> adx# L)
     (mark# head X -> active# head mark X, active# adx cons(X, L) -> cons#(X, adx L))
     (mark# head X -> active# head mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# head X -> active# head mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# head X -> active# head mark X, active# adx nil() -> mark# nil())
     (mark# head X -> active# head mark X, active# incr cons(X, L) -> s# X)
     (mark# head X -> active# head mark X, active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# head X -> active# head mark X, active# incr cons(X, L) -> incr# L)
     (mark# head X -> active# head mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# head X -> active# head mark X, active# incr nil() -> mark# nil())
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# tail X -> tail# mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# tail X -> active# tail mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# tail X -> mark# X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# head X -> head# mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# head X -> active# head mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# head X -> mark# X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# 0() -> active# 0())
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# nats() -> active# nats())
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# zeros() -> active# zeros())
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# adx X -> adx# mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# adx X -> active# adx mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# adx X -> mark# X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# s X -> s# mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# s X -> active# s mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# s X -> mark# X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# cons(X1, X2) -> mark# X1)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# incr X -> incr# mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# incr X -> active# incr mark X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# incr X -> mark# X)
     (active# adx cons(X, L) -> mark# incr cons(X, adx L), mark# nil() -> active# nil())
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (active# tail cons(X, L) -> mark# L, mark# tail X -> tail# mark X)
     (active# tail cons(X, L) -> mark# L, mark# tail X -> active# tail mark X)
     (active# tail cons(X, L) -> mark# L, mark# tail X -> mark# X)
     (active# tail cons(X, L) -> mark# L, mark# head X -> head# mark X)
     (active# tail cons(X, L) -> mark# L, mark# head X -> active# head mark X)
     (active# tail cons(X, L) -> mark# L, mark# head X -> mark# X)
     (active# tail cons(X, L) -> mark# L, mark# 0() -> active# 0())
     (active# tail cons(X, L) -> mark# L, mark# nats() -> active# nats())
     (active# tail cons(X, L) -> mark# L, mark# zeros() -> active# zeros())
     (active# tail cons(X, L) -> mark# L, mark# adx X -> adx# mark X)
     (active# tail cons(X, L) -> mark# L, mark# adx X -> active# adx mark X)
     (active# tail cons(X, L) -> mark# L, mark# adx X -> mark# X)
     (active# tail cons(X, L) -> mark# L, mark# s X -> s# mark X)
     (active# tail cons(X, L) -> mark# L, mark# s X -> active# s mark X)
     (active# tail cons(X, L) -> mark# L, mark# s X -> mark# X)
     (active# tail cons(X, L) -> mark# L, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# tail cons(X, L) -> mark# L, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# tail cons(X, L) -> mark# L, mark# cons(X1, X2) -> mark# X1)
     (active# tail cons(X, L) -> mark# L, mark# incr X -> incr# mark X)
     (active# tail cons(X, L) -> mark# L, mark# incr X -> active# incr mark X)
     (active# tail cons(X, L) -> mark# L, mark# incr X -> mark# X)
     (active# tail cons(X, L) -> mark# L, mark# nil() -> active# nil())
     (mark# incr X -> incr# mark X, incr# active X -> incr# X)
     (mark# incr X -> incr# mark X, incr# mark X -> incr# X)
     (mark# adx X -> adx# mark X, adx# active X -> adx# X)
     (mark# adx X -> adx# mark X, adx# mark X -> adx# X)
     (mark# tail X -> tail# mark X, tail# active X -> tail# X)
     (mark# tail X -> tail# mark X, tail# mark X -> tail# X)
     (mark# head X -> head# mark X, head# mark X -> head# X)
     (mark# head X -> head# mark X, head# active X -> head# X)
     (mark# s X -> s# mark X, s# mark X -> s# X)
     (mark# s X -> s# mark X, s# active X -> s# X)
     (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> mark# X1)
     (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# zeros() -> mark# cons(0(), zeros()), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# zeros() -> mark# cons(0(), zeros()), mark# 0() -> active# 0())
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# nil() -> active# nil())
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# incr X -> mark# X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# incr X -> active# incr mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# incr X -> incr# mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# cons(X1, X2) -> mark# X1)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# s X -> mark# X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# s X -> active# s mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# s X -> s# mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# adx X -> mark# X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# adx X -> active# adx mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# adx X -> adx# mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# zeros() -> active# zeros())
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# nats() -> active# nats())
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# 0() -> active# 0())
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# head X -> mark# X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# head X -> active# head mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# head X -> head# mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# tail X -> mark# X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# tail X -> active# tail mark X)
     (active# incr cons(X, L) -> mark# cons(s X, incr L), mark# tail X -> tail# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil())
     (mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# incr X -> active# incr mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# incr X -> incr# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# adx X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# adx X -> active# adx mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# adx X -> adx# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> active# zeros())
     (mark# cons(X1, X2) -> mark# X1, mark# nats() -> active# nats())
     (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
     (mark# cons(X1, X2) -> mark# X1, mark# head X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# head X -> active# head mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# head X -> head# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> active# tail mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> tail# mark X)
     (active# nats() -> mark# adx zeros(), mark# incr X -> mark# X)
     (active# nats() -> mark# adx zeros(), mark# incr X -> active# incr mark X)
     (active# nats() -> mark# adx zeros(), mark# incr X -> incr# mark X)
     (active# nats() -> mark# adx zeros(), mark# cons(X1, X2) -> mark# X1)
     (active# nats() -> mark# adx zeros(), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# nats() -> mark# adx zeros(), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# nats() -> mark# adx zeros(), mark# s X -> mark# X)
     (active# nats() -> mark# adx zeros(), mark# s X -> active# s mark X)
     (active# nats() -> mark# adx zeros(), mark# s X -> s# mark X)
     (active# nats() -> mark# adx zeros(), mark# adx X -> mark# X)
     (active# nats() -> mark# adx zeros(), mark# adx X -> active# adx mark X)
     (active# nats() -> mark# adx zeros(), mark# adx X -> adx# mark X)
     (active# nats() -> mark# adx zeros(), mark# zeros() -> active# zeros())
     (active# nats() -> mark# adx zeros(), mark# 0() -> active# 0())
     (mark# tail X -> active# tail mark X, active# incr nil() -> mark# nil())
     (mark# tail X -> active# tail mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# tail X -> active# tail mark X, active# incr cons(X, L) -> incr# L)
     (mark# tail X -> active# tail mark X, active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# tail X -> active# tail mark X, active# incr cons(X, L) -> s# X)
     (mark# tail X -> active# tail mark X, active# adx nil() -> mark# nil())
     (mark# tail X -> active# tail mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# tail X -> active# tail mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# tail X -> active# tail mark X, active# adx cons(X, L) -> cons#(X, adx L))
     (mark# tail X -> active# tail mark X, active# adx cons(X, L) -> adx# L)
     (mark# tail X -> active# tail mark X, active# zeros() -> mark# cons(0(), zeros()))
     (mark# tail X -> active# tail mark X, active# zeros() -> cons#(0(), zeros()))
     (mark# tail X -> active# tail mark X, active# nats() -> mark# adx zeros())
     (mark# tail X -> active# tail mark X, active# nats() -> adx# zeros())
     (mark# tail X -> active# tail mark X, active# head cons(X, L) -> mark# X)
     (mark# tail X -> active# tail mark X, active# tail cons(X, L) -> mark# L)
     (mark# adx X -> active# adx mark X, active# incr nil() -> mark# nil())
     (mark# adx X -> active# adx mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# adx X -> active# adx mark X, active# incr cons(X, L) -> incr# L)
     (mark# adx X -> active# adx mark X, active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# adx X -> active# adx mark X, active# incr cons(X, L) -> s# X)
     (mark# adx X -> active# adx mark X, active# adx nil() -> mark# nil())
     (mark# adx X -> active# adx mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# adx X -> active# adx mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# adx X -> active# adx mark X, active# adx cons(X, L) -> cons#(X, adx L))
     (mark# adx X -> active# adx mark X, active# adx cons(X, L) -> adx# L)
     (mark# adx X -> active# adx mark X, active# zeros() -> mark# cons(0(), zeros()))
     (mark# adx X -> active# adx mark X, active# zeros() -> cons#(0(), zeros()))
     (mark# adx X -> active# adx mark X, active# nats() -> mark# adx zeros())
     (mark# adx X -> active# adx mark X, active# nats() -> adx# zeros())
     (mark# adx X -> active# adx mark X, active# head cons(X, L) -> mark# X)
     (mark# adx X -> active# adx mark X, active# tail cons(X, L) -> mark# L)
     (mark# incr X -> active# incr mark X, active# incr nil() -> mark# nil())
     (mark# incr X -> active# incr mark X, active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# incr X -> active# incr mark X, active# incr cons(X, L) -> incr# L)
     (mark# incr X -> active# incr mark X, active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# incr X -> active# incr mark X, active# incr cons(X, L) -> s# X)
     (mark# incr X -> active# incr mark X, active# adx nil() -> mark# nil())
     (mark# incr X -> active# incr mark X, active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# incr X -> active# incr mark X, active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# incr X -> active# incr mark X, active# adx cons(X, L) -> cons#(X, adx L))
     (mark# incr X -> active# incr mark X, active# adx cons(X, L) -> adx# L)
     (mark# incr X -> active# incr mark X, active# zeros() -> mark# cons(0(), zeros()))
     (mark# incr X -> active# incr mark X, active# zeros() -> cons#(0(), zeros()))
     (mark# incr X -> active# incr mark X, active# nats() -> mark# adx zeros())
     (mark# incr X -> active# incr mark X, active# nats() -> adx# zeros())
     (mark# incr X -> active# incr mark X, active# head cons(X, L) -> mark# X)
     (mark# incr X -> active# incr mark X, active# tail cons(X, L) -> mark# L)
     (mark# head X -> mark# X, mark# nil() -> active# nil())
     (mark# head X -> mark# X, mark# incr X -> mark# X)
     (mark# head X -> mark# X, mark# incr X -> active# incr mark X)
     (mark# head X -> mark# X, mark# incr X -> incr# mark X)
     (mark# head X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# head X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# head X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# head X -> mark# X, mark# s X -> mark# X)
     (mark# head X -> mark# X, mark# s X -> active# s mark X)
     (mark# head X -> mark# X, mark# s X -> s# mark X)
     (mark# head X -> mark# X, mark# adx X -> mark# X)
     (mark# head X -> mark# X, mark# adx X -> active# adx mark X)
     (mark# head X -> mark# X, mark# adx X -> adx# mark X)
     (mark# head X -> mark# X, mark# zeros() -> active# zeros())
     (mark# head X -> mark# X, mark# nats() -> active# nats())
     (mark# head X -> mark# X, mark# 0() -> active# 0())
     (mark# head X -> mark# X, mark# head X -> mark# X)
     (mark# head X -> mark# X, mark# head X -> active# head mark X)
     (mark# head X -> mark# X, mark# head X -> head# mark X)
     (mark# head X -> mark# X, mark# tail X -> mark# X)
     (mark# head X -> mark# X, mark# tail X -> active# tail mark X)
     (mark# head X -> mark# X, mark# tail X -> tail# mark X)
     (mark# s X -> mark# X, mark# nil() -> active# nil())
     (mark# s X -> mark# X, mark# incr X -> mark# X)
     (mark# s X -> mark# X, mark# incr X -> active# incr mark X)
     (mark# s X -> mark# X, mark# incr X -> incr# mark X)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# s X -> active# s mark X)
     (mark# s X -> mark# X, mark# s X -> s# mark X)
     (mark# s X -> mark# X, mark# adx X -> mark# X)
     (mark# s X -> mark# X, mark# adx X -> active# adx mark X)
     (mark# s X -> mark# X, mark# adx X -> adx# mark X)
     (mark# s X -> mark# X, mark# zeros() -> active# zeros())
     (mark# s X -> mark# X, mark# nats() -> active# nats())
     (mark# s X -> mark# X, mark# 0() -> active# 0())
     (mark# s X -> mark# X, mark# head X -> mark# X)
     (mark# s X -> mark# X, mark# head X -> active# head mark X)
     (mark# s X -> mark# X, mark# head X -> head# mark X)
     (mark# s X -> mark# X, mark# tail X -> mark# X)
     (mark# s X -> mark# X, mark# tail X -> active# tail mark X)
     (mark# s X -> mark# X, mark# tail X -> tail# mark X)
     (active# incr nil() -> mark# nil(), mark# nil() -> active# nil())
     (mark# nats() -> active# nats(), active# incr cons(X, L) -> mark# cons(s X, incr L))
     (mark# nats() -> active# nats(), active# incr cons(X, L) -> incr# L)
     (mark# nats() -> active# nats(), active# incr cons(X, L) -> cons#(s X, incr L))
     (mark# nats() -> active# nats(), active# incr cons(X, L) -> s# X)
     (mark# nats() -> active# nats(), active# adx cons(X, L) -> mark# incr cons(X, adx L))
     (mark# nats() -> active# nats(), active# adx cons(X, L) -> incr# cons(X, adx L))
     (mark# nats() -> active# nats(), active# adx cons(X, L) -> cons#(X, adx L))
     (mark# nats() -> active# nats(), active# adx cons(X, L) -> adx# L)
     (mark# nats() -> active# nats(), active# zeros() -> mark# cons(0(), zeros()))
     (mark# nats() -> active# nats(), active# zeros() -> cons#(0(), zeros()))
     (mark# nats() -> active# nats(), active# nats() -> mark# adx zeros())
     (mark# nats() -> active# nats(), active# nats() -> adx# zeros())
    }
    STATUS:
     arrows: 0.877959
     SCCS (1):
      Scc:
       {           mark# incr X -> mark# X,
                   mark# incr X -> active# incr mark X,
             mark# cons(X1, X2) -> mark# X1,
                      mark# s X -> mark# X,
                    mark# adx X -> mark# X,
                    mark# adx X -> active# adx mark X,
                  mark# zeros() -> active# zeros(),
                   mark# nats() -> active# nats(),
                   mark# head X -> mark# X,
                   mark# head X -> active# head mark X,
                   mark# tail X -> mark# X,
                   mark# tail X -> active# tail mark X,
        active# incr cons(X, L) -> mark# cons(s X, incr L),
         active# adx cons(X, L) -> mark# incr cons(X, adx L),
                active# zeros() -> mark# cons(0(), zeros()),
                 active# nats() -> mark# adx zeros(),
        active# head cons(X, L) -> mark# X,
        active# tail cons(X, L) -> mark# L}
      
      
      
      SCC (18):
       Strict:
        {           mark# incr X -> mark# X,
                    mark# incr X -> active# incr mark X,
              mark# cons(X1, X2) -> mark# X1,
                       mark# s X -> mark# X,
                     mark# adx X -> mark# X,
                     mark# adx X -> active# adx mark X,
                   mark# zeros() -> active# zeros(),
                    mark# nats() -> active# nats(),
                    mark# head X -> mark# X,
                    mark# head X -> active# head mark X,
                    mark# tail X -> mark# X,
                    mark# tail X -> active# tail mark X,
         active# incr cons(X, L) -> mark# cons(s X, incr L),
          active# adx cons(X, L) -> mark# incr cons(X, adx L),
                 active# zeros() -> mark# cons(0(), zeros()),
                  active# nats() -> mark# adx zeros(),
         active# head cons(X, L) -> mark# X,
         active# tail cons(X, L) -> mark# L}
       Weak:
       {            mark nil() -> active nil(),
                   mark incr X -> active incr mark X,
             mark cons(X1, X2) -> active cons(mark X1, X2),
                      mark s X -> active s mark X,
                    mark adx X -> active adx mark X,
                  mark zeros() -> active zeros(),
                   mark nats() -> active nats(),
                      mark 0() -> active 0(),
                   mark head X -> active head mark X,
                   mark tail X -> active tail mark X,
             active incr nil() -> mark nil(),
        active incr cons(X, L) -> mark cons(s X, incr L),
              active adx nil() -> mark nil(),
         active adx cons(X, L) -> mark incr cons(X, adx L),
                active zeros() -> mark cons(0(), zeros()),
                 active nats() -> mark adx zeros(),
        active head cons(X, L) -> mark X,
        active tail cons(X, L) -> mark L,
                   incr mark X -> incr X,
                 incr active X -> incr X,
             cons(X1, mark X2) -> cons(X1, X2),
           cons(X1, active X2) -> cons(X1, X2),
             cons(mark X1, X2) -> cons(X1, X2),
           cons(active X1, X2) -> cons(X1, X2),
                      s mark X -> s X,
                    s active X -> s X,
                    adx mark X -> adx X,
                  adx active X -> adx X,
                   head mark X -> head X,
                 head active X -> head X,
                   tail mark X -> tail X,
                 tail active X -> tail X}
       Open