MAYBE
Time: 0.064001
TRS:
 {          a__nats() -> cons(0(), incr nats()),
            a__nats() -> nats(),
           a__pairs() -> cons(0(), incr odds()),
           a__pairs() -> pairs(),
            a__incr X -> incr X,
  a__incr cons(X, XS) -> cons(s mark X, incr XS),
            a__odds() -> odds(),
            a__odds() -> a__incr a__pairs(),
    mark cons(X1, X2) -> cons(mark X1, X2),
             mark 0() -> 0(),
          mark incr X -> a__incr mark X,
          mark nats() -> a__nats(),
          mark odds() -> a__odds(),
             mark s X -> s mark X,
         mark pairs() -> a__pairs(),
          mark head X -> a__head mark X,
          mark tail X -> a__tail mark X,
            a__head X -> head X,
  a__head cons(X, XS) -> mark X,
            a__tail X -> tail X,
  a__tail cons(X, XS) -> mark XS}
 DP:
  DP:
   {a__incr# cons(X, XS) -> mark# X,
              a__odds#() -> a__pairs#(),
              a__odds#() -> a__incr# a__pairs(),
      mark# cons(X1, X2) -> mark# X1,
            mark# incr X -> a__incr# mark X,
            mark# incr X -> mark# X,
            mark# nats() -> a__nats#(),
            mark# odds() -> a__odds#(),
               mark# s X -> mark# X,
           mark# pairs() -> a__pairs#(),
            mark# head X -> mark# X,
            mark# head X -> a__head# mark X,
            mark# tail X -> mark# X,
            mark# tail X -> a__tail# mark X,
    a__head# cons(X, XS) -> mark# X,
    a__tail# cons(X, XS) -> mark# XS}
  TRS:
  {          a__nats() -> cons(0(), incr nats()),
             a__nats() -> nats(),
            a__pairs() -> cons(0(), incr odds()),
            a__pairs() -> pairs(),
             a__incr X -> incr X,
   a__incr cons(X, XS) -> cons(s mark X, incr XS),
             a__odds() -> odds(),
             a__odds() -> a__incr a__pairs(),
     mark cons(X1, X2) -> cons(mark X1, X2),
              mark 0() -> 0(),
           mark incr X -> a__incr mark X,
           mark nats() -> a__nats(),
           mark odds() -> a__odds(),
              mark s X -> s mark X,
          mark pairs() -> a__pairs(),
           mark head X -> a__head mark X,
           mark tail X -> a__tail mark X,
             a__head X -> head X,
   a__head cons(X, XS) -> mark X,
             a__tail X -> tail X,
   a__tail cons(X, XS) -> mark XS}
  EDG:
   {(mark# incr X -> mark# X, mark# tail X -> a__tail# mark X)
    (mark# incr X -> mark# X, mark# tail X -> mark# X)
    (mark# incr X -> mark# X, mark# head X -> a__head# mark X)
    (mark# incr X -> mark# X, mark# head X -> mark# X)
    (mark# incr X -> mark# X, mark# pairs() -> a__pairs#())
    (mark# incr X -> mark# X, mark# s X -> mark# X)
    (mark# incr X -> mark# X, mark# odds() -> a__odds#())
    (mark# incr X -> mark# X, mark# nats() -> a__nats#())
    (mark# incr X -> mark# X, mark# incr X -> mark# X)
    (mark# incr X -> mark# X, mark# incr X -> a__incr# mark X)
    (mark# incr X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# head X -> mark# X, mark# tail X -> a__tail# mark X)
    (mark# head X -> mark# X, mark# tail X -> mark# X)
    (mark# head X -> mark# X, mark# head X -> a__head# mark X)
    (mark# head X -> mark# X, mark# head X -> mark# X)
    (mark# head X -> mark# X, mark# pairs() -> a__pairs#())
    (mark# head X -> mark# X, mark# s X -> mark# X)
    (mark# head X -> mark# X, mark# odds() -> a__odds#())
    (mark# head X -> mark# X, mark# nats() -> a__nats#())
    (mark# head X -> mark# X, mark# incr X -> mark# X)
    (mark# head X -> mark# X, mark# incr X -> a__incr# mark X)
    (mark# head X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (a__head# cons(X, XS) -> mark# X, mark# tail X -> a__tail# mark X)
    (a__head# cons(X, XS) -> mark# X, mark# tail X -> mark# X)
    (a__head# cons(X, XS) -> mark# X, mark# head X -> a__head# mark X)
    (a__head# cons(X, XS) -> mark# X, mark# head X -> mark# X)
    (a__head# cons(X, XS) -> mark# X, mark# pairs() -> a__pairs#())
    (a__head# cons(X, XS) -> mark# X, mark# s X -> mark# X)
    (a__head# cons(X, XS) -> mark# X, mark# odds() -> a__odds#())
    (a__head# cons(X, XS) -> mark# X, mark# nats() -> a__nats#())
    (a__head# cons(X, XS) -> mark# X, mark# incr X -> mark# X)
    (a__head# cons(X, XS) -> mark# X, mark# incr X -> a__incr# mark X)
    (a__head# cons(X, XS) -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# incr X -> a__incr# mark X, a__incr# cons(X, XS) -> mark# X)
    (mark# tail X -> a__tail# mark X, a__tail# cons(X, XS) -> mark# XS)
    (mark# cons(X1, X2) -> mark# X1, mark# tail X -> a__tail# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# tail X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# head X -> a__head# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# head X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# pairs() -> a__pairs#())
    (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# odds() -> a__odds#())
    (mark# cons(X1, X2) -> mark# X1, mark# nats() -> a__nats#())
    (mark# cons(X1, X2) -> mark# X1, mark# incr X -> mark# X)
    (mark# cons(X1, X2) -> mark# X1, mark# incr X -> a__incr# mark X)
    (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
    (a__tail# cons(X, XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
    (a__tail# cons(X, XS) -> mark# XS, mark# incr X -> a__incr# mark X)
    (a__tail# cons(X, XS) -> mark# XS, mark# incr X -> mark# X)
    (a__tail# cons(X, XS) -> mark# XS, mark# nats() -> a__nats#())
    (a__tail# cons(X, XS) -> mark# XS, mark# odds() -> a__odds#())
    (a__tail# cons(X, XS) -> mark# XS, mark# s X -> mark# X)
    (a__tail# cons(X, XS) -> mark# XS, mark# pairs() -> a__pairs#())
    (a__tail# cons(X, XS) -> mark# XS, mark# head X -> mark# X)
    (a__tail# cons(X, XS) -> mark# XS, mark# head X -> a__head# mark X)
    (a__tail# cons(X, XS) -> mark# XS, mark# tail X -> mark# X)
    (a__tail# cons(X, XS) -> mark# XS, mark# tail X -> a__tail# mark X)
    (mark# odds() -> a__odds#(), a__odds#() -> a__pairs#())
    (mark# odds() -> a__odds#(), a__odds#() -> a__incr# a__pairs())
    (mark# head X -> a__head# mark X, a__head# cons(X, XS) -> mark# X)
    (a__odds#() -> a__incr# a__pairs(), a__incr# cons(X, XS) -> mark# X)
    (mark# tail X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# tail X -> mark# X, mark# incr X -> a__incr# mark X)
    (mark# tail X -> mark# X, mark# incr X -> mark# X)
    (mark# tail X -> mark# X, mark# nats() -> a__nats#())
    (mark# tail X -> mark# X, mark# odds() -> a__odds#())
    (mark# tail X -> mark# X, mark# s X -> mark# X)
    (mark# tail X -> mark# X, mark# pairs() -> a__pairs#())
    (mark# tail X -> mark# X, mark# head X -> mark# X)
    (mark# tail X -> mark# X, mark# head X -> a__head# mark X)
    (mark# tail X -> mark# X, mark# tail X -> mark# X)
    (mark# tail X -> mark# X, mark# tail X -> a__tail# mark X)
    (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# incr X -> a__incr# mark X)
    (mark# s X -> mark# X, mark# incr X -> mark# X)
    (mark# s X -> mark# X, mark# nats() -> a__nats#())
    (mark# s X -> mark# X, mark# odds() -> a__odds#())
    (mark# s X -> mark# X, mark# s X -> mark# X)
    (mark# s X -> mark# X, mark# pairs() -> a__pairs#())
    (mark# s X -> mark# X, mark# head X -> mark# X)
    (mark# s X -> mark# X, mark# head X -> a__head# mark X)
    (mark# s X -> mark# X, mark# tail X -> mark# X)
    (mark# s X -> mark# X, mark# tail X -> a__tail# mark X)
    (a__incr# cons(X, XS) -> mark# X, mark# cons(X1, X2) -> mark# X1)
    (a__incr# cons(X, XS) -> mark# X, mark# incr X -> a__incr# mark X)
    (a__incr# cons(X, XS) -> mark# X, mark# incr X -> mark# X)
    (a__incr# cons(X, XS) -> mark# X, mark# nats() -> a__nats#())
    (a__incr# cons(X, XS) -> mark# X, mark# odds() -> a__odds#())
    (a__incr# cons(X, XS) -> mark# X, mark# s X -> mark# X)
    (a__incr# cons(X, XS) -> mark# X, mark# pairs() -> a__pairs#())
    (a__incr# cons(X, XS) -> mark# X, mark# head X -> mark# X)
    (a__incr# cons(X, XS) -> mark# X, mark# head X -> a__head# mark X)
    (a__incr# cons(X, XS) -> mark# X, mark# tail X -> mark# X)
    (a__incr# cons(X, XS) -> mark# X, mark# tail X -> a__tail# mark X)}
   STATUS:
    arrows: 0.632812
    SCCS (1):
     Scc:
      {a__incr# cons(X, XS) -> mark# X,
                 a__odds#() -> a__incr# a__pairs(),
         mark# cons(X1, X2) -> mark# X1,
               mark# incr X -> a__incr# mark X,
               mark# incr X -> mark# X,
               mark# odds() -> a__odds#(),
                  mark# s X -> mark# X,
               mark# head X -> mark# X,
               mark# head X -> a__head# mark X,
               mark# tail X -> mark# X,
               mark# tail X -> a__tail# mark X,
       a__head# cons(X, XS) -> mark# X,
       a__tail# cons(X, XS) -> mark# XS}
     
     SCC (13):
      Strict:
       {a__incr# cons(X, XS) -> mark# X,
                  a__odds#() -> a__incr# a__pairs(),
          mark# cons(X1, X2) -> mark# X1,
                mark# incr X -> a__incr# mark X,
                mark# incr X -> mark# X,
                mark# odds() -> a__odds#(),
                   mark# s X -> mark# X,
                mark# head X -> mark# X,
                mark# head X -> a__head# mark X,
                mark# tail X -> mark# X,
                mark# tail X -> a__tail# mark X,
        a__head# cons(X, XS) -> mark# X,
        a__tail# cons(X, XS) -> mark# XS}
      Weak:
      {          a__nats() -> cons(0(), incr nats()),
                 a__nats() -> nats(),
                a__pairs() -> cons(0(), incr odds()),
                a__pairs() -> pairs(),
                 a__incr X -> incr X,
       a__incr cons(X, XS) -> cons(s mark X, incr XS),
                 a__odds() -> odds(),
                 a__odds() -> a__incr a__pairs(),
         mark cons(X1, X2) -> cons(mark X1, X2),
                  mark 0() -> 0(),
               mark incr X -> a__incr mark X,
               mark nats() -> a__nats(),
               mark odds() -> a__odds(),
                  mark s X -> s mark X,
              mark pairs() -> a__pairs(),
               mark head X -> a__head mark X,
               mark tail X -> a__tail mark X,
                 a__head X -> head X,
       a__head cons(X, XS) -> mark X,
                 a__tail X -> tail X,
       a__tail cons(X, XS) -> mark XS}
      Open