MAYBE

Problem:
 a__nats() -> cons(0(),incr(nats()))
 a__pairs() -> cons(0(),incr(odds()))
 a__odds() -> a__incr(a__pairs())
 a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
 a__head(cons(X,XS)) -> mark(X)
 a__tail(cons(X,XS)) -> mark(XS)
 mark(nats()) -> a__nats()
 mark(incr(X)) -> a__incr(mark(X))
 mark(pairs()) -> a__pairs()
 mark(odds()) -> a__odds()
 mark(head(X)) -> a__head(mark(X))
 mark(tail(X)) -> a__tail(mark(X))
 mark(cons(X1,X2)) -> cons(mark(X1),X2)
 mark(0()) -> 0()
 mark(s(X)) -> s(mark(X))
 a__nats() -> nats()
 a__incr(X) -> incr(X)
 a__pairs() -> pairs()
 a__odds() -> odds()
 a__head(X) -> head(X)
 a__tail(X) -> tail(X)

Proof:
 DP Processor:
  DPs:
   a__odds#() -> a__pairs#()
   a__odds#() -> a__incr#(a__pairs())
   a__incr#(cons(X,XS)) -> mark#(X)
   a__head#(cons(X,XS)) -> mark#(X)
   a__tail#(cons(X,XS)) -> mark#(XS)
   mark#(nats()) -> a__nats#()
   mark#(incr(X)) -> mark#(X)
   mark#(incr(X)) -> a__incr#(mark(X))
   mark#(pairs()) -> a__pairs#()
   mark#(odds()) -> a__odds#()
   mark#(head(X)) -> mark#(X)
   mark#(head(X)) -> a__head#(mark(X))
   mark#(tail(X)) -> mark#(X)
   mark#(tail(X)) -> a__tail#(mark(X))
   mark#(cons(X1,X2)) -> mark#(X1)
   mark#(s(X)) -> mark#(X)
  TRS:
   a__nats() -> cons(0(),incr(nats()))
   a__pairs() -> cons(0(),incr(odds()))
   a__odds() -> a__incr(a__pairs())
   a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
   a__head(cons(X,XS)) -> mark(X)
   a__tail(cons(X,XS)) -> mark(XS)
   mark(nats()) -> a__nats()
   mark(incr(X)) -> a__incr(mark(X))
   mark(pairs()) -> a__pairs()
   mark(odds()) -> a__odds()
   mark(head(X)) -> a__head(mark(X))
   mark(tail(X)) -> a__tail(mark(X))
   mark(cons(X1,X2)) -> cons(mark(X1),X2)
   mark(0()) -> 0()
   mark(s(X)) -> s(mark(X))
   a__nats() -> nats()
   a__incr(X) -> incr(X)
   a__pairs() -> pairs()
   a__odds() -> odds()
   a__head(X) -> head(X)
   a__tail(X) -> tail(X)
  TDG Processor:
   DPs:
    a__odds#() -> a__pairs#()
    a__odds#() -> a__incr#(a__pairs())
    a__incr#(cons(X,XS)) -> mark#(X)
    a__head#(cons(X,XS)) -> mark#(X)
    a__tail#(cons(X,XS)) -> mark#(XS)
    mark#(nats()) -> a__nats#()
    mark#(incr(X)) -> mark#(X)
    mark#(incr(X)) -> a__incr#(mark(X))
    mark#(pairs()) -> a__pairs#()
    mark#(odds()) -> a__odds#()
    mark#(head(X)) -> mark#(X)
    mark#(head(X)) -> a__head#(mark(X))
    mark#(tail(X)) -> mark#(X)
    mark#(tail(X)) -> a__tail#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X)
   TRS:
    a__nats() -> cons(0(),incr(nats()))
    a__pairs() -> cons(0(),incr(odds()))
    a__odds() -> a__incr(a__pairs())
    a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
    a__head(cons(X,XS)) -> mark(X)
    a__tail(cons(X,XS)) -> mark(XS)
    mark(nats()) -> a__nats()
    mark(incr(X)) -> a__incr(mark(X))
    mark(pairs()) -> a__pairs()
    mark(odds()) -> a__odds()
    mark(head(X)) -> a__head(mark(X))
    mark(tail(X)) -> a__tail(mark(X))
    mark(cons(X1,X2)) -> cons(mark(X1),X2)
    mark(0()) -> 0()
    mark(s(X)) -> s(mark(X))
    a__nats() -> nats()
    a__incr(X) -> incr(X)
    a__pairs() -> pairs()
    a__odds() -> odds()
    a__head(X) -> head(X)
    a__tail(X) -> tail(X)
   graph:
    a__tail#(cons(X,XS)) -> mark#(XS) -> mark#(s(X)) -> mark#(X)
    a__tail#(cons(X,XS)) -> mark#(XS) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    a__tail#(cons(X,XS)) -> mark#(XS) ->
    mark#(tail(X)) -> a__tail#(mark(X))
    a__tail#(cons(X,XS)) -> mark#(XS) ->
    mark#(tail(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#(head(X)) -> mark#(X)
    a__tail#(cons(X,XS)) -> mark#(XS) ->
    mark#(odds()) -> a__odds#()
    a__tail#(cons(X,XS)) -> mark#(XS) ->
    mark#(pairs()) -> a__pairs#()
    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__head#(cons(X,XS)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    a__head#(cons(X,XS)) -> 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#(odds()) -> a__odds#()
    a__head#(cons(X,XS)) -> mark#(X) ->
    mark#(pairs()) -> a__pairs#()
    a__head#(cons(X,XS)) -> mark#(X) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    a__head#(cons(X,XS)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    a__head#(cons(X,XS)) -> mark#(X) ->
    mark#(nats()) -> a__nats#()
    mark#(tail(X)) -> a__tail#(mark(X)) ->
    a__tail#(cons(X,XS)) -> mark#(XS)
    mark#(tail(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> a__tail#(mark(X))
    mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(head(X)) -> a__head#(mark(X))
    mark#(tail(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(odds()) -> a__odds#()
    mark#(tail(X)) -> mark#(X) -> mark#(pairs()) -> a__pairs#()
    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#(head(X)) -> a__head#(mark(X)) ->
    a__head#(cons(X,XS)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(head(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#(odds()) -> a__odds#()
    mark#(head(X)) -> mark#(X) -> mark#(pairs()) -> a__pairs#()
    mark#(head(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
    mark#(head(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(tail(X)) -> a__tail#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> a__head#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(odds()) -> a__odds#()
    mark#(s(X)) -> mark#(X) -> mark#(pairs()) -> a__pairs#()
    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#(odds()) -> a__odds#() -> a__odds#() -> a__incr#(a__pairs())
    mark#(odds()) -> a__odds#() -> a__odds#() -> a__pairs#()
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    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#(odds()) -> a__odds#()
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(pairs()) -> a__pairs#()
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(incr(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(nats()) -> a__nats#()
    mark#(incr(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    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#(odds()) -> a__odds#()
    mark#(incr(X)) -> mark#(X) -> mark#(pairs()) -> a__pairs#()
    mark#(incr(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
    mark#(incr(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    mark#(incr(X)) -> a__incr#(mark(X)) ->
    a__incr#(cons(X,XS)) -> mark#(X)
    a__incr#(cons(X,XS)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    a__incr#(cons(X,XS)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    a__incr#(cons(X,XS)) -> mark#(X) ->
    mark#(tail(X)) -> a__tail#(mark(X))
    a__incr#(cons(X,XS)) -> mark#(X) -> mark#(tail(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#(head(X)) -> mark#(X)
    a__incr#(cons(X,XS)) -> mark#(X) -> mark#(odds()) -> a__odds#()
    a__incr#(cons(X,XS)) -> mark#(X) ->
    mark#(pairs()) -> a__pairs#()
    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__odds#() -> a__incr#(a__pairs()) -> a__incr#(cons(X,XS)) -> mark#(X)
   Restore Modifier:
    DPs:
     a__odds#() -> a__pairs#()
     a__odds#() -> a__incr#(a__pairs())
     a__incr#(cons(X,XS)) -> mark#(X)
     a__head#(cons(X,XS)) -> mark#(X)
     a__tail#(cons(X,XS)) -> mark#(XS)
     mark#(nats()) -> a__nats#()
     mark#(incr(X)) -> mark#(X)
     mark#(incr(X)) -> a__incr#(mark(X))
     mark#(pairs()) -> a__pairs#()
     mark#(odds()) -> a__odds#()
     mark#(head(X)) -> mark#(X)
     mark#(head(X)) -> a__head#(mark(X))
     mark#(tail(X)) -> mark#(X)
     mark#(tail(X)) -> a__tail#(mark(X))
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(s(X)) -> mark#(X)
    TRS:
     a__nats() -> cons(0(),incr(nats()))
     a__pairs() -> cons(0(),incr(odds()))
     a__odds() -> a__incr(a__pairs())
     a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
     a__head(cons(X,XS)) -> mark(X)
     a__tail(cons(X,XS)) -> mark(XS)
     mark(nats()) -> a__nats()
     mark(incr(X)) -> a__incr(mark(X))
     mark(pairs()) -> a__pairs()
     mark(odds()) -> a__odds()
     mark(head(X)) -> a__head(mark(X))
     mark(tail(X)) -> a__tail(mark(X))
     mark(cons(X1,X2)) -> cons(mark(X1),X2)
     mark(0()) -> 0()
     mark(s(X)) -> s(mark(X))
     a__nats() -> nats()
     a__incr(X) -> incr(X)
     a__pairs() -> pairs()
     a__odds() -> odds()
     a__head(X) -> head(X)
     a__tail(X) -> tail(X)
    SCC Processor:
     #sccs: 1
     #rules: 13
     #arcs: 94/256
     DPs:
      a__tail#(cons(X,XS)) -> mark#(XS)
      mark#(incr(X)) -> mark#(X)
      mark#(incr(X)) -> a__incr#(mark(X))
      a__incr#(cons(X,XS)) -> mark#(X)
      mark#(odds()) -> a__odds#()
      a__odds#() -> a__incr#(a__pairs())
      mark#(head(X)) -> mark#(X)
      mark#(head(X)) -> a__head#(mark(X))
      a__head#(cons(X,XS)) -> mark#(X)
      mark#(tail(X)) -> mark#(X)
      mark#(tail(X)) -> a__tail#(mark(X))
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(s(X)) -> mark#(X)
     TRS:
      a__nats() -> cons(0(),incr(nats()))
      a__pairs() -> cons(0(),incr(odds()))
      a__odds() -> a__incr(a__pairs())
      a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS))
      a__head(cons(X,XS)) -> mark(X)
      a__tail(cons(X,XS)) -> mark(XS)
      mark(nats()) -> a__nats()
      mark(incr(X)) -> a__incr(mark(X))
      mark(pairs()) -> a__pairs()
      mark(odds()) -> a__odds()
      mark(head(X)) -> a__head(mark(X))
      mark(tail(X)) -> a__tail(mark(X))
      mark(cons(X1,X2)) -> cons(mark(X1),X2)
      mark(0()) -> 0()
      mark(s(X)) -> s(mark(X))
      a__nats() -> nats()
      a__incr(X) -> incr(X)
      a__pairs() -> pairs()
      a__odds() -> odds()
      a__head(X) -> head(X)
      a__tail(X) -> tail(X)
     Open