MAYBE
Time: 14.952801
TRS:
 {      mark cons(X1, X2) -> active cons(mark X1, X2),
                 mark 0() -> active 0(),
              mark incr X -> active incr mark X,
              mark nats() -> active nats(),
              mark odds() -> active odds(),
             mark pairs() -> active pairs(),
                 mark s X -> active s mark X,
              mark head X -> active head mark X,
              mark tail X -> active tail mark 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),
              incr mark X -> incr X,
            incr active X -> incr X,
  active incr cons(X, XS) -> mark cons(s X, incr XS),
            active nats() -> mark cons(0(), incr nats()),
            active odds() -> mark incr pairs(),
           active pairs() -> mark cons(0(), incr odds()),
  active head cons(X, XS) -> mark X,
  active tail cons(X, XS) -> mark XS,
                 s mark X -> s X,
               s active X -> s X,
              head mark X -> head X,
            head active X -> head X,
              tail mark X -> tail X,
            tail active X -> tail X}
 DP:
  DP:
   {      mark# cons(X1, X2) -> mark# X1,
          mark# cons(X1, X2) -> cons#(mark X1, X2),
          mark# cons(X1, X2) -> active# cons(mark X1, X2),
                   mark# 0() -> active# 0(),
                mark# incr X -> mark# X,
                mark# incr X -> incr# mark X,
                mark# incr X -> active# incr mark X,
                mark# nats() -> active# nats(),
                mark# odds() -> active# odds(),
               mark# pairs() -> active# pairs(),
                   mark# s X -> mark# X,
                   mark# s X -> active# s mark X,
                   mark# s X -> s# mark X,
                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,
          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),
                incr# mark X -> incr# X,
              incr# active X -> incr# X,
    active# incr cons(X, XS) -> mark# cons(s X, incr XS),
    active# incr cons(X, XS) -> cons#(s X, incr XS),
    active# incr cons(X, XS) -> incr# XS,
    active# incr cons(X, XS) -> s# X,
              active# nats() -> mark# cons(0(), incr nats()),
              active# nats() -> cons#(0(), incr nats()),
              active# nats() -> incr# nats(),
              active# odds() -> mark# incr pairs(),
              active# odds() -> incr# pairs(),
             active# pairs() -> mark# cons(0(), incr odds()),
             active# pairs() -> cons#(0(), incr odds()),
             active# pairs() -> incr# odds(),
    active# head cons(X, XS) -> mark# X,
    active# tail cons(X, XS) -> mark# XS,
                   s# mark X -> s# X,
                 s# active X -> s# X,
                head# mark X -> head# X,
              head# active X -> head# X,
                tail# mark X -> tail# X,
              tail# active X -> tail# X}
  TRS:
  {      mark cons(X1, X2) -> active cons(mark X1, X2),
                  mark 0() -> active 0(),
               mark incr X -> active incr mark X,
               mark nats() -> active nats(),
               mark odds() -> active odds(),
              mark pairs() -> active pairs(),
                  mark s X -> active s mark X,
               mark head X -> active head mark X,
               mark tail X -> active tail mark 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),
               incr mark X -> incr X,
             incr active X -> incr X,
   active incr cons(X, XS) -> mark cons(s X, incr XS),
             active nats() -> mark cons(0(), incr nats()),
             active odds() -> mark incr pairs(),
            active pairs() -> mark cons(0(), incr odds()),
   active head cons(X, XS) -> mark X,
   active tail cons(X, XS) -> mark XS,
                  s mark X -> s X,
                s active X -> s X,
               head mark X -> head X,
             head active X -> head X,
               tail mark X -> tail X,
             tail active X -> tail X}
  UR:
   {      mark cons(X1, X2) -> active cons(mark X1, X2),
                   mark 0() -> active 0(),
                mark incr X -> active incr mark X,
                mark nats() -> active nats(),
                mark odds() -> active odds(),
               mark pairs() -> active pairs(),
                   mark s X -> active s mark X,
                mark head X -> active head mark X,
                mark tail X -> active tail mark 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),
                incr mark X -> incr X,
              incr active X -> incr X,
    active incr cons(X, XS) -> mark cons(s X, incr XS),
              active nats() -> mark cons(0(), incr nats()),
              active odds() -> mark incr pairs(),
             active pairs() -> mark cons(0(), incr odds()),
    active head cons(X, XS) -> mark X,
    active tail cons(X, XS) -> mark XS,
                   s mark X -> s X,
                 s active X -> s X,
                head mark X -> head X,
              head active X -> head X,
                tail mark X -> tail X,
              tail active X -> tail X}
   EDG:
    {
     (mark# tail X -> active# tail mark X, active# tail cons(X, XS) -> mark# XS)
     (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# 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# pairs() -> active# pairs())
     (mark# incr X -> mark# X, mark# odds() -> active# odds())
     (mark# incr X -> mark# X, mark# nats() -> active# nats())
     (mark# incr X -> mark# X, mark# incr X -> active# incr mark X)
     (mark# incr X -> mark# X, mark# incr X -> incr# mark X)
     (mark# incr X -> mark# X, mark# incr X -> mark# X)
     (mark# incr X -> mark# X, mark# 0() -> active# 0())
     (mark# incr X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# incr X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# incr X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# head X -> mark# X, mark# tail X -> tail# mark X)
     (mark# head X -> mark# X, mark# tail X -> active# tail mark X)
     (mark# head X -> mark# X, mark# tail X -> mark# X)
     (mark# head X -> mark# X, mark# head X -> head# mark X)
     (mark# head X -> mark# X, mark# head X -> active# head mark X)
     (mark# head X -> mark# X, mark# head X -> mark# X)
     (mark# head X -> mark# X, mark# s X -> s# mark X)
     (mark# head X -> mark# X, mark# s X -> active# s mark X)
     (mark# head X -> mark# X, mark# s X -> mark# X)
     (mark# head X -> mark# X, mark# pairs() -> active# pairs())
     (mark# head X -> mark# X, mark# odds() -> active# odds())
     (mark# head X -> mark# X, mark# nats() -> active# nats())
     (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# incr X -> mark# X)
     (mark# head X -> mark# X, mark# 0() -> active# 0())
     (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# cons(X1, X2) -> mark# X1)
     (incr# mark X -> incr# X, incr# active X -> incr# X)
     (incr# mark X -> incr# X, incr# mark X -> incr# X)
     (active# incr cons(X, XS) -> s# X, s# active X -> s# X)
     (active# incr cons(X, XS) -> s# X, s# mark X -> s# X)
     (s# mark X -> s# X, s# active X -> s# X)
     (s# mark X -> s# X, s# mark X -> s# X)
     (head# mark X -> head# X, head# active X -> head# X)
     (head# mark X -> head# X, head# mark X -> head# X)
     (tail# mark X -> tail# X, tail# active X -> tail# X)
     (tail# mark X -> tail# X, tail# mark X -> tail# X)
     (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# incr cons(X, XS) -> mark# cons(s X, incr XS), mark# cons(X1, X2) -> mark# X1)
     (active# pairs() -> mark# cons(0(), incr odds()), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# pairs() -> mark# cons(0(), incr odds()), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# pairs() -> mark# cons(0(), incr odds()), mark# cons(X1, X2) -> mark# X1)
     (active# tail cons(X, XS) -> mark# XS, mark# tail X -> tail# mark X)
     (active# tail cons(X, XS) -> mark# XS, mark# tail X -> active# tail mark X)
     (active# tail cons(X, XS) -> mark# XS, mark# tail X -> mark# X)
     (active# tail cons(X, XS) -> mark# XS, mark# head X -> head# mark X)
     (active# tail cons(X, XS) -> mark# XS, mark# head X -> active# head mark X)
     (active# tail cons(X, XS) -> mark# XS, mark# head X -> mark# X)
     (active# tail cons(X, XS) -> mark# XS, mark# s X -> s# mark X)
     (active# tail cons(X, XS) -> mark# XS, mark# s X -> active# s mark X)
     (active# tail cons(X, XS) -> mark# XS, mark# s X -> mark# X)
     (active# tail cons(X, XS) -> mark# XS, mark# pairs() -> active# pairs())
     (active# tail cons(X, XS) -> mark# XS, mark# odds() -> active# odds())
     (active# tail cons(X, XS) -> mark# XS, mark# nats() -> active# nats())
     (active# tail cons(X, XS) -> mark# XS, mark# incr X -> active# incr mark X)
     (active# tail cons(X, XS) -> mark# XS, mark# incr X -> incr# mark X)
     (active# tail cons(X, XS) -> mark# XS, mark# incr X -> mark# X)
     (active# tail cons(X, XS) -> mark# XS, mark# 0() -> active# 0())
     (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# tail cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> tail# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> active# tail mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# head X -> head# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# head X -> active# head mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# head X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# pairs() -> active# pairs())
     (mark# cons(X1, X2) -> mark# X1, mark# odds() -> active# odds())
     (mark# cons(X1, X2) -> mark# X1, mark# nats() -> active# nats())
     (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# incr X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0())
     (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# cons(X1, X2) -> mark# X1)
     (mark# s X -> s# mark X, s# active X -> s# X)
     (mark# s X -> s# mark X, s# mark X -> s# X)
     (mark# tail X -> tail# mark X, tail# active X -> tail# X)
     (mark# tail X -> tail# mark X, tail# mark X -> tail# X)
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (mark# odds() -> active# odds(), active# odds() -> incr# pairs())
     (mark# odds() -> active# odds(), active# odds() -> mark# incr pairs())
     (mark# pairs() -> active# pairs(), active# pairs() -> mark# cons(0(), incr odds()))
     (mark# pairs() -> active# pairs(), active# pairs() -> cons#(0(), incr odds()))
     (mark# pairs() -> active# pairs(), active# pairs() -> incr# odds())
     (mark# nats() -> active# nats(), active# nats() -> mark# cons(0(), incr nats()))
     (mark# nats() -> active# nats(), active# nats() -> cons#(0(), incr nats()))
     (mark# nats() -> active# nats(), active# nats() -> incr# nats())
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
     (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2))
     (mark# head X -> head# mark X, head# mark X -> head# X)
     (mark# head X -> head# mark X, head# active X -> head# X)
     (mark# incr X -> incr# mark X, incr# mark X -> incr# X)
     (mark# incr X -> incr# mark X, incr# active X -> incr# X)
     (active# incr cons(X, XS) -> incr# XS, incr# mark X -> incr# X)
     (active# incr cons(X, XS) -> incr# XS, incr# active X -> incr# X)
     (active# nats() -> mark# cons(0(), incr nats()), mark# cons(X1, X2) -> mark# X1)
     (active# nats() -> mark# cons(0(), incr nats()), mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# nats() -> mark# cons(0(), incr nats()), mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (tail# active X -> tail# X, tail# mark X -> tail# X)
     (tail# active X -> tail# X, tail# active X -> tail# X)
     (head# active X -> head# X, head# mark X -> head# X)
     (head# active X -> head# X, head# active X -> head# X)
     (s# active X -> s# X, s# mark X -> s# X)
     (s# active X -> s# X, s# active X -> s# X)
     (active# head cons(X, XS) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (active# head cons(X, XS) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (active# head cons(X, XS) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (active# head cons(X, XS) -> mark# X, mark# 0() -> active# 0())
     (active# head cons(X, XS) -> mark# X, mark# incr X -> mark# X)
     (active# head cons(X, XS) -> mark# X, mark# incr X -> incr# mark X)
     (active# head cons(X, XS) -> mark# X, mark# incr X -> active# incr mark X)
     (active# head cons(X, XS) -> mark# X, mark# nats() -> active# nats())
     (active# head cons(X, XS) -> mark# X, mark# odds() -> active# odds())
     (active# head cons(X, XS) -> mark# X, mark# pairs() -> active# pairs())
     (active# head cons(X, XS) -> mark# X, mark# s X -> mark# X)
     (active# head cons(X, XS) -> mark# X, mark# s X -> active# s mark X)
     (active# head cons(X, XS) -> mark# X, mark# s X -> s# mark X)
     (active# head cons(X, XS) -> mark# X, mark# head X -> mark# X)
     (active# head cons(X, XS) -> mark# X, mark# head X -> active# head mark X)
     (active# head cons(X, XS) -> mark# X, mark# head X -> head# mark X)
     (active# head cons(X, XS) -> mark# X, mark# tail X -> mark# X)
     (active# head cons(X, XS) -> mark# X, mark# tail X -> active# tail mark X)
     (active# head cons(X, XS) -> mark# X, mark# tail X -> tail# mark X)
     (incr# active X -> incr# X, incr# mark X -> incr# X)
     (incr# active X -> incr# X, incr# active X -> incr# X)
     (mark# tail X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (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# 0() -> active# 0())
     (mark# tail X -> mark# X, mark# incr X -> mark# X)
     (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# nats() -> active# nats())
     (mark# tail X -> mark# X, mark# odds() -> active# odds())
     (mark# tail X -> mark# X, mark# pairs() -> active# pairs())
     (mark# tail X -> mark# X, mark# s X -> mark# X)
     (mark# tail X -> mark# X, mark# s X -> active# s mark X)
     (mark# tail X -> mark# X, mark# s X -> s# mark X)
     (mark# tail X -> mark# X, mark# head X -> mark# X)
     (mark# tail X -> mark# X, mark# head X -> active# head mark X)
     (mark# tail X -> mark# X, mark# head X -> head# mark X)
     (mark# tail X -> mark# X, mark# tail X -> mark# X)
     (mark# tail X -> mark# X, mark# tail X -> active# tail mark X)
     (mark# tail X -> mark# X, mark# tail X -> tail# mark X)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2))
     (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2))
     (mark# s X -> mark# X, mark# 0() -> active# 0())
     (mark# s X -> mark# X, mark# incr X -> mark# X)
     (mark# s X -> mark# X, mark# incr X -> incr# mark X)
     (mark# s X -> mark# X, mark# incr X -> active# incr mark X)
     (mark# s X -> mark# X, mark# nats() -> active# nats())
     (mark# s X -> mark# X, mark# odds() -> active# odds())
     (mark# s X -> mark# X, mark# pairs() -> active# pairs())
     (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# 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# odds() -> mark# incr pairs(), mark# incr X -> mark# X)
     (active# odds() -> mark# incr pairs(), mark# incr X -> incr# mark X)
     (active# odds() -> mark# incr pairs(), mark# incr X -> active# incr mark X)
     (mark# head X -> active# head mark X, active# head cons(X, XS) -> mark# X)
     (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> mark# cons(s X, incr XS))
     (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> cons#(s X, incr XS))
     (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> incr# XS)
     (mark# incr X -> active# incr mark X, active# incr cons(X, XS) -> s# X)
    }
    STATUS:
     arrows: 0.897778
     SCCS (6):
      Scc:
       {      mark# cons(X1, X2) -> mark# X1,
                    mark# incr X -> mark# X,
                    mark# incr X -> active# incr mark X,
                    mark# nats() -> active# nats(),
                    mark# odds() -> active# odds(),
                   mark# pairs() -> active# pairs(),
                       mark# s X -> mark# X,
                    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, XS) -> mark# cons(s X, incr XS),
                  active# nats() -> mark# cons(0(), incr nats()),
                  active# odds() -> mark# incr pairs(),
                 active# pairs() -> mark# cons(0(), incr odds()),
        active# head cons(X, XS) -> mark# X,
        active# tail cons(X, XS) -> mark# XS}
      Scc:
       {  tail# mark X -> tail# X,
        tail# active X -> tail# X}
      Scc:
       {  head# mark X -> head# X,
        head# active X -> head# X}
      Scc:
       {  s# mark X -> s# X,
        s# active X -> s# X}
      Scc:
       {  incr# mark X -> incr# X,
        incr# active X -> incr# X}
      Scc:
       {  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)}
      
      SCC (17):
       Strict:
        {      mark# cons(X1, X2) -> mark# X1,
                     mark# incr X -> mark# X,
                     mark# incr X -> active# incr mark X,
                     mark# nats() -> active# nats(),
                     mark# odds() -> active# odds(),
                    mark# pairs() -> active# pairs(),
                        mark# s X -> mark# X,
                     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, XS) -> mark# cons(s X, incr XS),
                   active# nats() -> mark# cons(0(), incr nats()),
                   active# odds() -> mark# incr pairs(),
                  active# pairs() -> mark# cons(0(), incr odds()),
         active# head cons(X, XS) -> mark# X,
         active# tail cons(X, XS) -> mark# XS}
       Weak:
       {      mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark 0() -> active 0(),
                    mark incr X -> active incr mark X,
                    mark nats() -> active nats(),
                    mark odds() -> active odds(),
                   mark pairs() -> active pairs(),
                       mark s X -> active s mark X,
                    mark head X -> active head mark X,
                    mark tail X -> active tail mark 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),
                    incr mark X -> incr X,
                  incr active X -> incr X,
        active incr cons(X, XS) -> mark cons(s X, incr XS),
                  active nats() -> mark cons(0(), incr nats()),
                  active odds() -> mark incr pairs(),
                 active pairs() -> mark cons(0(), incr odds()),
        active head cons(X, XS) -> mark X,
        active tail cons(X, XS) -> mark XS,
                       s mark X -> s X,
                     s active X -> s X,
                    head mark X -> head X,
                  head active X -> head X,
                    tail mark X -> tail X,
                  tail active X -> tail X}
       Open
      
      
      
      
      SCC (2):
       Strict:
        {  tail# mark X -> tail# X,
         tail# active X -> tail# X}
       Weak:
       {      mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark 0() -> active 0(),
                    mark incr X -> active incr mark X,
                    mark nats() -> active nats(),
                    mark odds() -> active odds(),
                   mark pairs() -> active pairs(),
                       mark s X -> active s mark X,
                    mark head X -> active head mark X,
                    mark tail X -> active tail mark 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),
                    incr mark X -> incr X,
                  incr active X -> incr X,
        active incr cons(X, XS) -> mark cons(s X, incr XS),
                  active nats() -> mark cons(0(), incr nats()),
                  active odds() -> mark incr pairs(),
                 active pairs() -> mark cons(0(), incr odds()),
        active head cons(X, XS) -> mark X,
        active tail cons(X, XS) -> mark XS,
                       s mark X -> s X,
                     s active X -> s X,
                    head mark X -> head X,
                  head active X -> head X,
                    tail mark X -> tail X,
                  tail active X -> tail X}
       Open
      
      SCC (2):
       Strict:
        {  head# mark X -> head# X,
         head# active X -> head# X}
       Weak:
       {      mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark 0() -> active 0(),
                    mark incr X -> active incr mark X,
                    mark nats() -> active nats(),
                    mark odds() -> active odds(),
                   mark pairs() -> active pairs(),
                       mark s X -> active s mark X,
                    mark head X -> active head mark X,
                    mark tail X -> active tail mark 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),
                    incr mark X -> incr X,
                  incr active X -> incr X,
        active incr cons(X, XS) -> mark cons(s X, incr XS),
                  active nats() -> mark cons(0(), incr nats()),
                  active odds() -> mark incr pairs(),
                 active pairs() -> mark cons(0(), incr odds()),
        active head cons(X, XS) -> mark X,
        active tail cons(X, XS) -> mark XS,
                       s mark X -> s X,
                     s active X -> s X,
                    head mark X -> head X,
                  head active X -> head X,
                    tail mark X -> tail X,
                  tail active X -> tail X}
       Open
      
      SCC (2):
       Strict:
        {  s# mark X -> s# X,
         s# active X -> s# X}
       Weak:
       {      mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark 0() -> active 0(),
                    mark incr X -> active incr mark X,
                    mark nats() -> active nats(),
                    mark odds() -> active odds(),
                   mark pairs() -> active pairs(),
                       mark s X -> active s mark X,
                    mark head X -> active head mark X,
                    mark tail X -> active tail mark 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),
                    incr mark X -> incr X,
                  incr active X -> incr X,
        active incr cons(X, XS) -> mark cons(s X, incr XS),
                  active nats() -> mark cons(0(), incr nats()),
                  active odds() -> mark incr pairs(),
                 active pairs() -> mark cons(0(), incr odds()),
        active head cons(X, XS) -> mark X,
        active tail cons(X, XS) -> mark XS,
                       s mark X -> s X,
                     s active X -> s X,
                    head mark X -> head X,
                  head active X -> head X,
                    tail mark X -> tail X,
                  tail active X -> tail X}
       Open
      
      
      
      
      
      
      
      SCC (2):
       Strict:
        {  incr# mark X -> incr# X,
         incr# active X -> incr# X}
       Weak:
       {      mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark 0() -> active 0(),
                    mark incr X -> active incr mark X,
                    mark nats() -> active nats(),
                    mark odds() -> active odds(),
                   mark pairs() -> active pairs(),
                       mark s X -> active s mark X,
                    mark head X -> active head mark X,
                    mark tail X -> active tail mark 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),
                    incr mark X -> incr X,
                  incr active X -> incr X,
        active incr cons(X, XS) -> mark cons(s X, incr XS),
                  active nats() -> mark cons(0(), incr nats()),
                  active odds() -> mark incr pairs(),
                 active pairs() -> mark cons(0(), incr odds()),
        active head cons(X, XS) -> mark X,
        active tail cons(X, XS) -> mark XS,
                       s mark X -> s X,
                     s active X -> s X,
                    head mark X -> head X,
                  head active X -> head X,
                    tail mark X -> tail X,
                  tail active X -> tail X}
       Open
      
      
      
      SCC (4):
       Strict:
        {  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)}
       Weak:
       {      mark cons(X1, X2) -> active cons(mark X1, X2),
                       mark 0() -> active 0(),
                    mark incr X -> active incr mark X,
                    mark nats() -> active nats(),
                    mark odds() -> active odds(),
                   mark pairs() -> active pairs(),
                       mark s X -> active s mark X,
                    mark head X -> active head mark X,
                    mark tail X -> active tail mark 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),
                    incr mark X -> incr X,
                  incr active X -> incr X,
        active incr cons(X, XS) -> mark cons(s X, incr XS),
                  active nats() -> mark cons(0(), incr nats()),
                  active odds() -> mark incr pairs(),
                 active pairs() -> mark cons(0(), incr odds()),
        active head cons(X, XS) -> mark X,
        active tail cons(X, XS) -> mark XS,
                       s mark X -> s X,
                     s active X -> s X,
                    head mark X -> head X,
                  head active X -> head X,
                    tail mark X -> tail X,
                  tail active X -> tail X}
       Open