MAYBE

Problem:
 a__incr(nil()) -> nil()
 a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
 a__adx(nil()) -> nil()
 a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
 a__nats() -> a__adx(a__zeros())
 a__zeros() -> cons(0(),zeros())
 a__head(cons(X,L)) -> mark(X)
 a__tail(cons(X,L)) -> mark(L)
 mark(incr(X)) -> a__incr(mark(X))
 mark(adx(X)) -> a__adx(mark(X))
 mark(nats()) -> a__nats()
 mark(zeros()) -> a__zeros()
 mark(head(X)) -> a__head(mark(X))
 mark(tail(X)) -> a__tail(mark(X))
 mark(nil()) -> nil()
 mark(cons(X1,X2)) -> cons(mark(X1),X2)
 mark(s(X)) -> s(mark(X))
 mark(0()) -> 0()
 a__incr(X) -> incr(X)
 a__adx(X) -> adx(X)
 a__nats() -> nats()
 a__zeros() -> zeros()
 a__head(X) -> head(X)
 a__tail(X) -> tail(X)

Proof:
 DP Processor:
  DPs:
   a__incr#(cons(X,L)) -> mark#(X)
   a__adx#(cons(X,L)) -> mark#(X)
   a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
   a__nats#() -> a__zeros#()
   a__nats#() -> a__adx#(a__zeros())
   a__head#(cons(X,L)) -> mark#(X)
   a__tail#(cons(X,L)) -> mark#(L)
   mark#(incr(X)) -> mark#(X)
   mark#(incr(X)) -> a__incr#(mark(X))
   mark#(adx(X)) -> mark#(X)
   mark#(adx(X)) -> a__adx#(mark(X))
   mark#(nats()) -> a__nats#()
   mark#(zeros()) -> a__zeros#()
   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__incr(nil()) -> nil()
   a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
   a__adx(nil()) -> nil()
   a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
   a__nats() -> a__adx(a__zeros())
   a__zeros() -> cons(0(),zeros())
   a__head(cons(X,L)) -> mark(X)
   a__tail(cons(X,L)) -> mark(L)
   mark(incr(X)) -> a__incr(mark(X))
   mark(adx(X)) -> a__adx(mark(X))
   mark(nats()) -> a__nats()
   mark(zeros()) -> a__zeros()
   mark(head(X)) -> a__head(mark(X))
   mark(tail(X)) -> a__tail(mark(X))
   mark(nil()) -> nil()
   mark(cons(X1,X2)) -> cons(mark(X1),X2)
   mark(s(X)) -> s(mark(X))
   mark(0()) -> 0()
   a__incr(X) -> incr(X)
   a__adx(X) -> adx(X)
   a__nats() -> nats()
   a__zeros() -> zeros()
   a__head(X) -> head(X)
   a__tail(X) -> tail(X)
  EDG Processor:
   DPs:
    a__incr#(cons(X,L)) -> mark#(X)
    a__adx#(cons(X,L)) -> mark#(X)
    a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
    a__nats#() -> a__zeros#()
    a__nats#() -> a__adx#(a__zeros())
    a__head#(cons(X,L)) -> mark#(X)
    a__tail#(cons(X,L)) -> mark#(L)
    mark#(incr(X)) -> mark#(X)
    mark#(incr(X)) -> a__incr#(mark(X))
    mark#(adx(X)) -> mark#(X)
    mark#(adx(X)) -> a__adx#(mark(X))
    mark#(nats()) -> a__nats#()
    mark#(zeros()) -> a__zeros#()
    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__incr(nil()) -> nil()
    a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
    a__adx(nil()) -> nil()
    a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
    a__nats() -> a__adx(a__zeros())
    a__zeros() -> cons(0(),zeros())
    a__head(cons(X,L)) -> mark(X)
    a__tail(cons(X,L)) -> mark(L)
    mark(incr(X)) -> a__incr(mark(X))
    mark(adx(X)) -> a__adx(mark(X))
    mark(nats()) -> a__nats()
    mark(zeros()) -> a__zeros()
    mark(head(X)) -> a__head(mark(X))
    mark(tail(X)) -> a__tail(mark(X))
    mark(nil()) -> nil()
    mark(cons(X1,X2)) -> cons(mark(X1),X2)
    mark(s(X)) -> s(mark(X))
    mark(0()) -> 0()
    a__incr(X) -> incr(X)
    a__adx(X) -> adx(X)
    a__nats() -> nats()
    a__zeros() -> zeros()
    a__head(X) -> head(X)
    a__tail(X) -> tail(X)
   graph:
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(incr(X)) -> mark#(X)
    a__tail#(cons(X,L)) -> mark#(L) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(adx(X)) -> mark#(X)
    a__tail#(cons(X,L)) -> mark#(L) ->
    mark#(adx(X)) -> a__adx#(mark(X))
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(nats()) -> a__nats#()
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(zeros()) -> a__zeros#()
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(head(X)) -> mark#(X)
    a__tail#(cons(X,L)) -> mark#(L) ->
    mark#(head(X)) -> a__head#(mark(X))
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(tail(X)) -> mark#(X)
    a__tail#(cons(X,L)) -> mark#(L) ->
    mark#(tail(X)) -> a__tail#(mark(X))
    a__tail#(cons(X,L)) -> mark#(L) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    a__tail#(cons(X,L)) -> mark#(L) -> mark#(s(X)) -> mark#(X)
    a__head#(cons(X,L)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    a__head#(cons(X,L)) -> mark#(X) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    a__head#(cons(X,L)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    a__head#(cons(X,L)) -> mark#(X) ->
    mark#(adx(X)) -> a__adx#(mark(X))
    a__head#(cons(X,L)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    a__head#(cons(X,L)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    a__head#(cons(X,L)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    a__head#(cons(X,L)) -> mark#(X) ->
    mark#(head(X)) -> a__head#(mark(X))
    a__head#(cons(X,L)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    a__head#(cons(X,L)) -> mark#(X) ->
    mark#(tail(X)) -> a__tail#(mark(X))
    a__head#(cons(X,L)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    a__head#(cons(X,L)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    a__nats#() -> a__adx#(a__zeros()) ->
    a__adx#(cons(X,L)) -> mark#(X)
    a__nats#() -> a__adx#(a__zeros()) ->
    a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    a__adx#(cons(X,L)) -> mark#(X) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    a__adx#(cons(X,L)) -> mark#(X) ->
    mark#(adx(X)) -> a__adx#(mark(X))
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    a__adx#(cons(X,L)) -> mark#(X) ->
    mark#(head(X)) -> a__head#(mark(X))
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    a__adx#(cons(X,L)) -> mark#(X) ->
    mark#(tail(X)) -> a__tail#(mark(X))
    a__adx#(cons(X,L)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    a__adx#(cons(X,L)) -> mark#(X) ->
    mark#(s(X)) -> mark#(X)
    a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L))) ->
    a__incr#(cons(X,L)) -> mark#(X)
    mark#(tail(X)) -> a__tail#(mark(X)) ->
    a__tail#(cons(X,L)) -> mark#(L)
    mark#(tail(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
    mark#(tail(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    mark#(tail(X)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    mark#(tail(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    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#(tail(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(tail(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(head(X)) -> a__head#(mark(X)) ->
    a__head#(cons(X,L)) -> mark#(X)
    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#(adx(X)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    mark#(head(X)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    mark#(head(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    mark#(head(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(head(X)) -> a__head#(mark(X))
    mark#(head(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(head(X)) -> mark#(X) -> mark#(tail(X)) -> a__tail#(mark(X))
    mark#(head(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(head(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(nats()) -> a__nats#() -> a__nats#() -> a__zeros#()
    mark#(nats()) -> a__nats#() ->
    a__nats#() -> a__adx#(a__zeros())
    mark#(adx(X)) -> a__adx#(mark(X)) ->
    a__adx#(cons(X,L)) -> mark#(X)
    mark#(adx(X)) -> a__adx#(mark(X)) ->
    a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
    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)) -> 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#(nats()) -> a__nats#()
    mark#(adx(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    mark#(adx(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(head(X)) -> a__head#(mark(X))
    mark#(adx(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(adx(X)) -> mark#(X) -> mark#(tail(X)) -> a__tail#(mark(X))
    mark#(adx(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(adx(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    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#(adx(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    mark#(incr(X)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    mark#(incr(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    mark#(incr(X)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(head(X)) -> a__head#(mark(X))
    mark#(incr(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(incr(X)) -> mark#(X) -> mark#(tail(X)) -> a__tail#(mark(X))
    mark#(incr(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(incr(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(incr(X)) -> a__incr#(mark(X)) -> a__incr#(cons(X,L)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(incr(X)) -> a__incr#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(adx(X)) -> a__adx#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    mark#(s(X)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    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))
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    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#(adx(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(adx(X)) -> a__adx#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(nats()) -> a__nats#()
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(zeros()) -> a__zeros#()
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(head(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(head(X)) -> a__head#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tail(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(tail(X)) -> a__tail#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(incr(X)) -> mark#(X)
    a__incr#(cons(X,L)) -> mark#(X) ->
    mark#(incr(X)) -> a__incr#(mark(X))
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(adx(X)) -> mark#(X)
    a__incr#(cons(X,L)) -> mark#(X) ->
    mark#(adx(X)) -> a__adx#(mark(X))
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(nats()) -> a__nats#()
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(zeros()) -> a__zeros#()
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(head(X)) -> mark#(X)
    a__incr#(cons(X,L)) -> mark#(X) ->
    mark#(head(X)) -> a__head#(mark(X))
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    a__incr#(cons(X,L)) -> mark#(X) ->
    mark#(tail(X)) -> a__tail#(mark(X))
    a__incr#(cons(X,L)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    a__incr#(cons(X,L)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
   Restore Modifier:
    DPs:
     a__incr#(cons(X,L)) -> mark#(X)
     a__adx#(cons(X,L)) -> mark#(X)
     a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
     a__nats#() -> a__zeros#()
     a__nats#() -> a__adx#(a__zeros())
     a__head#(cons(X,L)) -> mark#(X)
     a__tail#(cons(X,L)) -> mark#(L)
     mark#(incr(X)) -> mark#(X)
     mark#(incr(X)) -> a__incr#(mark(X))
     mark#(adx(X)) -> mark#(X)
     mark#(adx(X)) -> a__adx#(mark(X))
     mark#(nats()) -> a__nats#()
     mark#(zeros()) -> a__zeros#()
     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__incr(nil()) -> nil()
     a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
     a__adx(nil()) -> nil()
     a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
     a__nats() -> a__adx(a__zeros())
     a__zeros() -> cons(0(),zeros())
     a__head(cons(X,L)) -> mark(X)
     a__tail(cons(X,L)) -> mark(L)
     mark(incr(X)) -> a__incr(mark(X))
     mark(adx(X)) -> a__adx(mark(X))
     mark(nats()) -> a__nats()
     mark(zeros()) -> a__zeros()
     mark(head(X)) -> a__head(mark(X))
     mark(tail(X)) -> a__tail(mark(X))
     mark(nil()) -> nil()
     mark(cons(X1,X2)) -> cons(mark(X1),X2)
     mark(s(X)) -> s(mark(X))
     mark(0()) -> 0()
     a__incr(X) -> incr(X)
     a__adx(X) -> adx(X)
     a__nats() -> nats()
     a__zeros() -> zeros()
     a__head(X) -> head(X)
     a__tail(X) -> tail(X)
    SCC Processor:
     #sccs: 1
     #rules: 17
     #arcs: 130/361
     DPs:
      a__tail#(cons(X,L)) -> mark#(L)
      mark#(s(X)) -> mark#(X)
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(tail(X)) -> a__tail#(mark(X))
      mark#(tail(X)) -> mark#(X)
      mark#(head(X)) -> a__head#(mark(X))
      a__head#(cons(X,L)) -> mark#(X)
      mark#(head(X)) -> mark#(X)
      mark#(nats()) -> a__nats#()
      a__nats#() -> a__adx#(a__zeros())
      a__adx#(cons(X,L)) -> a__incr#(cons(mark(X),adx(L)))
      a__incr#(cons(X,L)) -> mark#(X)
      mark#(adx(X)) -> a__adx#(mark(X))
      a__adx#(cons(X,L)) -> mark#(X)
      mark#(adx(X)) -> mark#(X)
      mark#(incr(X)) -> a__incr#(mark(X))
      mark#(incr(X)) -> mark#(X)
     TRS:
      a__incr(nil()) -> nil()
      a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L))
      a__adx(nil()) -> nil()
      a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L)))
      a__nats() -> a__adx(a__zeros())
      a__zeros() -> cons(0(),zeros())
      a__head(cons(X,L)) -> mark(X)
      a__tail(cons(X,L)) -> mark(L)
      mark(incr(X)) -> a__incr(mark(X))
      mark(adx(X)) -> a__adx(mark(X))
      mark(nats()) -> a__nats()
      mark(zeros()) -> a__zeros()
      mark(head(X)) -> a__head(mark(X))
      mark(tail(X)) -> a__tail(mark(X))
      mark(nil()) -> nil()
      mark(cons(X1,X2)) -> cons(mark(X1),X2)
      mark(s(X)) -> s(mark(X))
      mark(0()) -> 0()
      a__incr(X) -> incr(X)
      a__adx(X) -> adx(X)
      a__nats() -> nats()
      a__zeros() -> zeros()
      a__head(X) -> head(X)
      a__tail(X) -> tail(X)
     Open