MAYBE

Problem:
 a__nats() -> a__adx(a__zeros())
 a__zeros() -> cons(0(),zeros())
 a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
 a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
 a__hd(cons(X,Y)) -> mark(X)
 a__tl(cons(X,Y)) -> mark(Y)
 mark(nats()) -> a__nats()
 mark(adx(X)) -> a__adx(mark(X))
 mark(zeros()) -> a__zeros()
 mark(incr(X)) -> a__incr(mark(X))
 mark(hd(X)) -> a__hd(mark(X))
 mark(tl(X)) -> a__tl(mark(X))
 mark(cons(X1,X2)) -> cons(X1,X2)
 mark(0()) -> 0()
 mark(s(X)) -> s(X)
 a__nats() -> nats()
 a__adx(X) -> adx(X)
 a__zeros() -> zeros()
 a__incr(X) -> incr(X)
 a__hd(X) -> hd(X)
 a__tl(X) -> tl(X)

Proof:
 DP Processor:
  DPs:
   a__nats#() -> a__zeros#()
   a__nats#() -> a__adx#(a__zeros())
   a__adx#(cons(X,Y)) -> a__incr#(cons(X,adx(Y)))
   a__hd#(cons(X,Y)) -> mark#(X)
   a__tl#(cons(X,Y)) -> mark#(Y)
   mark#(nats()) -> a__nats#()
   mark#(adx(X)) -> mark#(X)
   mark#(adx(X)) -> a__adx#(mark(X))
   mark#(zeros()) -> a__zeros#()
   mark#(incr(X)) -> mark#(X)
   mark#(incr(X)) -> a__incr#(mark(X))
   mark#(hd(X)) -> mark#(X)
   mark#(hd(X)) -> a__hd#(mark(X))
   mark#(tl(X)) -> mark#(X)
   mark#(tl(X)) -> a__tl#(mark(X))
  TRS:
   a__nats() -> a__adx(a__zeros())
   a__zeros() -> cons(0(),zeros())
   a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
   a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
   a__hd(cons(X,Y)) -> mark(X)
   a__tl(cons(X,Y)) -> mark(Y)
   mark(nats()) -> a__nats()
   mark(adx(X)) -> a__adx(mark(X))
   mark(zeros()) -> a__zeros()
   mark(incr(X)) -> a__incr(mark(X))
   mark(hd(X)) -> a__hd(mark(X))
   mark(tl(X)) -> a__tl(mark(X))
   mark(cons(X1,X2)) -> cons(X1,X2)
   mark(0()) -> 0()
   mark(s(X)) -> s(X)
   a__nats() -> nats()
   a__adx(X) -> adx(X)
   a__zeros() -> zeros()
   a__incr(X) -> incr(X)
   a__hd(X) -> hd(X)
   a__tl(X) -> tl(X)
  CDG Processor:
   DPs:
    a__nats#() -> a__zeros#()
    a__nats#() -> a__adx#(a__zeros())
    a__adx#(cons(X,Y)) -> a__incr#(cons(X,adx(Y)))
    a__hd#(cons(X,Y)) -> mark#(X)
    a__tl#(cons(X,Y)) -> mark#(Y)
    mark#(nats()) -> a__nats#()
    mark#(adx(X)) -> mark#(X)
    mark#(adx(X)) -> a__adx#(mark(X))
    mark#(zeros()) -> a__zeros#()
    mark#(incr(X)) -> mark#(X)
    mark#(incr(X)) -> a__incr#(mark(X))
    mark#(hd(X)) -> mark#(X)
    mark#(hd(X)) -> a__hd#(mark(X))
    mark#(tl(X)) -> mark#(X)
    mark#(tl(X)) -> a__tl#(mark(X))
   TRS:
    a__nats() -> a__adx(a__zeros())
    a__zeros() -> cons(0(),zeros())
    a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
    a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
    a__hd(cons(X,Y)) -> mark(X)
    a__tl(cons(X,Y)) -> mark(Y)
    mark(nats()) -> a__nats()
    mark(adx(X)) -> a__adx(mark(X))
    mark(zeros()) -> a__zeros()
    mark(incr(X)) -> a__incr(mark(X))
    mark(hd(X)) -> a__hd(mark(X))
    mark(tl(X)) -> a__tl(mark(X))
    mark(cons(X1,X2)) -> cons(X1,X2)
    mark(0()) -> 0()
    mark(s(X)) -> s(X)
    a__nats() -> nats()
    a__adx(X) -> adx(X)
    a__zeros() -> zeros()
    a__incr(X) -> incr(X)
    a__hd(X) -> hd(X)
    a__tl(X) -> tl(X)
   graph:
    a__tl#(cons(X,Y)) -> mark#(Y) -> mark#(adx(X)) -> mark#(X)
    a__tl#(cons(X,Y)) -> mark#(Y) -> mark#(adx(X)) -> a__adx#(mark(X))
    a__tl#(cons(X,Y)) -> mark#(Y) -> mark#(zeros()) -> a__zeros#()
    a__tl#(cons(X,Y)) -> mark#(Y) -> mark#(incr(X)) -> mark#(X)
    a__tl#(cons(X,Y)) -> mark#(Y) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    mark#(tl(X)) -> a__tl#(mark(X)) -> a__tl#(cons(X,Y)) -> mark#(Y)
    mark#(tl(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(tl(X)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    mark#(tl(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    mark#(tl(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(tl(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
    mark#(hd(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(hd(X)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    mark#(hd(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    mark#(hd(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(hd(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
    mark#(hd(X)) -> a__hd#(mark(X)) -> a__hd#(cons(X,Y)) -> mark#(X)
    mark#(nats()) -> a__nats#() -> a__nats#() -> a__zeros#()
    mark#(nats()) -> a__nats#() -> a__nats#() -> a__adx#(a__zeros())
    mark#(adx(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    mark#(adx(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    mark#(adx(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    mark#(adx(X)) -> a__adx#(mark(X)) ->
    a__adx#(cons(X,Y)) -> a__incr#(cons(X,adx(Y)))
    mark#(incr(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    mark#(incr(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    mark#(incr(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
    a__hd#(cons(X,Y)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    a__hd#(cons(X,Y)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    a__hd#(cons(X,Y)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    a__hd#(cons(X,Y)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    a__hd#(cons(X,Y)) -> mark#(X) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    a__nats#() -> a__adx#(a__zeros()) -> a__adx#(cons(X,Y)) -> a__incr#(cons(X,adx(Y)))
   Restore Modifier:
    DPs:
     a__nats#() -> a__zeros#()
     a__nats#() -> a__adx#(a__zeros())
     a__adx#(cons(X,Y)) -> a__incr#(cons(X,adx(Y)))
     a__hd#(cons(X,Y)) -> mark#(X)
     a__tl#(cons(X,Y)) -> mark#(Y)
     mark#(nats()) -> a__nats#()
     mark#(adx(X)) -> mark#(X)
     mark#(adx(X)) -> a__adx#(mark(X))
     mark#(zeros()) -> a__zeros#()
     mark#(incr(X)) -> mark#(X)
     mark#(incr(X)) -> a__incr#(mark(X))
     mark#(hd(X)) -> mark#(X)
     mark#(hd(X)) -> a__hd#(mark(X))
     mark#(tl(X)) -> mark#(X)
     mark#(tl(X)) -> a__tl#(mark(X))
    TRS:
     a__nats() -> a__adx(a__zeros())
     a__zeros() -> cons(0(),zeros())
     a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
     a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
     a__hd(cons(X,Y)) -> mark(X)
     a__tl(cons(X,Y)) -> mark(Y)
     mark(nats()) -> a__nats()
     mark(adx(X)) -> a__adx(mark(X))
     mark(zeros()) -> a__zeros()
     mark(incr(X)) -> a__incr(mark(X))
     mark(hd(X)) -> a__hd(mark(X))
     mark(tl(X)) -> a__tl(mark(X))
     mark(cons(X1,X2)) -> cons(X1,X2)
     mark(0()) -> 0()
     mark(s(X)) -> s(X)
     a__nats() -> nats()
     a__adx(X) -> adx(X)
     a__zeros() -> zeros()
     a__incr(X) -> incr(X)
     a__hd(X) -> hd(X)
     a__tl(X) -> tl(X)
    SCC Processor:
     #sccs: 1
     #rules: 2
     #arcs: 36/225
     DPs:
      mark#(incr(X)) -> mark#(X)
      mark#(adx(X)) -> mark#(X)
     TRS:
      a__nats() -> a__adx(a__zeros())
      a__zeros() -> cons(0(),zeros())
      a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
      a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
      a__hd(cons(X,Y)) -> mark(X)
      a__tl(cons(X,Y)) -> mark(Y)
      mark(nats()) -> a__nats()
      mark(adx(X)) -> a__adx(mark(X))
      mark(zeros()) -> a__zeros()
      mark(incr(X)) -> a__incr(mark(X))
      mark(hd(X)) -> a__hd(mark(X))
      mark(tl(X)) -> a__tl(mark(X))
      mark(cons(X1,X2)) -> cons(X1,X2)
      mark(0()) -> 0()
      mark(s(X)) -> s(X)
      a__nats() -> nats()
      a__adx(X) -> adx(X)
      a__zeros() -> zeros()
      a__incr(X) -> incr(X)
      a__hd(X) -> hd(X)
      a__tl(X) -> tl(X)
     Open