MAYBE

Problem:
 nats() -> cons(0(),n__incr(n__nats()))
 pairs() -> cons(0(),n__incr(n__odds()))
 odds() -> incr(pairs())
 incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
 head(cons(X,XS)) -> X
 tail(cons(X,XS)) -> activate(XS)
 incr(X) -> n__incr(X)
 nats() -> n__nats()
 odds() -> n__odds()
 activate(n__incr(X)) -> incr(activate(X))
 activate(n__nats()) -> nats()
 activate(n__odds()) -> odds()
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   odds#() -> pairs#()
   odds#() -> incr#(pairs())
   incr#(cons(X,XS)) -> activate#(XS)
   tail#(cons(X,XS)) -> activate#(XS)
   activate#(n__incr(X)) -> activate#(X)
   activate#(n__incr(X)) -> incr#(activate(X))
   activate#(n__nats()) -> nats#()
   activate#(n__odds()) -> odds#()
  TRS:
   nats() -> cons(0(),n__incr(n__nats()))
   pairs() -> cons(0(),n__incr(n__odds()))
   odds() -> incr(pairs())
   incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
   head(cons(X,XS)) -> X
   tail(cons(X,XS)) -> activate(XS)
   incr(X) -> n__incr(X)
   nats() -> n__nats()
   odds() -> n__odds()
   activate(n__incr(X)) -> incr(activate(X))
   activate(n__nats()) -> nats()
   activate(n__odds()) -> odds()
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    odds#() -> pairs#()
    odds#() -> incr#(pairs())
    incr#(cons(X,XS)) -> activate#(XS)
    tail#(cons(X,XS)) -> activate#(XS)
    activate#(n__incr(X)) -> activate#(X)
    activate#(n__incr(X)) -> incr#(activate(X))
    activate#(n__nats()) -> nats#()
    activate#(n__odds()) -> odds#()
   TRS:
    pairs() -> cons(0(),n__incr(n__odds()))
    activate(n__incr(X)) -> incr(activate(X))
    activate(n__nats()) -> nats()
    activate(n__odds()) -> odds()
    activate(X) -> X
    incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
    incr(X) -> n__incr(X)
    nats() -> cons(0(),n__incr(n__nats()))
    nats() -> n__nats()
    odds() -> incr(pairs())
    odds() -> n__odds()
   EDG Processor:
    DPs:
     odds#() -> pairs#()
     odds#() -> incr#(pairs())
     incr#(cons(X,XS)) -> activate#(XS)
     tail#(cons(X,XS)) -> activate#(XS)
     activate#(n__incr(X)) -> activate#(X)
     activate#(n__incr(X)) -> incr#(activate(X))
     activate#(n__nats()) -> nats#()
     activate#(n__odds()) -> odds#()
    TRS:
     pairs() -> cons(0(),n__incr(n__odds()))
     activate(n__incr(X)) -> incr(activate(X))
     activate(n__nats()) -> nats()
     activate(n__odds()) -> odds()
     activate(X) -> X
     incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
     incr(X) -> n__incr(X)
     nats() -> cons(0(),n__incr(n__nats()))
     nats() -> n__nats()
     odds() -> incr(pairs())
     odds() -> n__odds()
    graph:
     tail#(cons(X,XS)) -> activate#(XS) ->
     activate#(n__incr(X)) -> activate#(X)
     tail#(cons(X,XS)) -> activate#(XS) ->
     activate#(n__incr(X)) -> incr#(activate(X))
     tail#(cons(X,XS)) -> activate#(XS) ->
     activate#(n__nats()) -> nats#()
     tail#(cons(X,XS)) -> activate#(XS) ->
     activate#(n__odds()) -> odds#()
     activate#(n__odds()) -> odds#() -> odds#() -> pairs#()
     activate#(n__odds()) -> odds#() ->
     odds#() -> incr#(pairs())
     activate#(n__incr(X)) -> activate#(X) ->
     activate#(n__incr(X)) -> activate#(X)
     activate#(n__incr(X)) -> activate#(X) ->
     activate#(n__incr(X)) -> incr#(activate(X))
     activate#(n__incr(X)) -> activate#(X) ->
     activate#(n__nats()) -> nats#()
     activate#(n__incr(X)) -> activate#(X) ->
     activate#(n__odds()) -> odds#()
     activate#(n__incr(X)) -> incr#(activate(X)) ->
     incr#(cons(X,XS)) -> activate#(XS)
     incr#(cons(X,XS)) -> activate#(XS) ->
     activate#(n__incr(X)) -> activate#(X)
     incr#(cons(X,XS)) -> activate#(XS) ->
     activate#(n__incr(X)) -> incr#(activate(X))
     incr#(cons(X,XS)) -> activate#(XS) ->
     activate#(n__nats()) -> nats#()
     incr#(cons(X,XS)) -> activate#(XS) -> activate#(n__odds()) -> odds#()
     odds#() -> incr#(pairs()) -> incr#(cons(X,XS)) -> activate#(XS)
    Restore Modifier:
     DPs:
      odds#() -> pairs#()
      odds#() -> incr#(pairs())
      incr#(cons(X,XS)) -> activate#(XS)
      tail#(cons(X,XS)) -> activate#(XS)
      activate#(n__incr(X)) -> activate#(X)
      activate#(n__incr(X)) -> incr#(activate(X))
      activate#(n__nats()) -> nats#()
      activate#(n__odds()) -> odds#()
     TRS:
      nats() -> cons(0(),n__incr(n__nats()))
      pairs() -> cons(0(),n__incr(n__odds()))
      odds() -> incr(pairs())
      incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
      head(cons(X,XS)) -> X
      tail(cons(X,XS)) -> activate(XS)
      incr(X) -> n__incr(X)
      nats() -> n__nats()
      odds() -> n__odds()
      activate(n__incr(X)) -> incr(activate(X))
      activate(n__nats()) -> nats()
      activate(n__odds()) -> odds()
      activate(X) -> X
     SCC Processor:
      #sccs: 1
      #rules: 5
      #arcs: 16/64
      DPs:
       activate#(n__odds()) -> odds#()
       odds#() -> incr#(pairs())
       incr#(cons(X,XS)) -> activate#(XS)
       activate#(n__incr(X)) -> incr#(activate(X))
       activate#(n__incr(X)) -> activate#(X)
      TRS:
       nats() -> cons(0(),n__incr(n__nats()))
       pairs() -> cons(0(),n__incr(n__odds()))
       odds() -> incr(pairs())
       incr(cons(X,XS)) -> cons(s(X),n__incr(activate(XS)))
       head(cons(X,XS)) -> X
       tail(cons(X,XS)) -> activate(XS)
       incr(X) -> n__incr(X)
       nats() -> n__nats()
       odds() -> n__odds()
       activate(n__incr(X)) -> incr(activate(X))
       activate(n__nats()) -> nats()
       activate(n__odds()) -> odds()
       activate(X) -> X
      Open