MAYBE

Problem:
 incr(nil()) -> nil()
 incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
 adx(nil()) -> nil()
 adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
 nats() -> adx(zeros())
 zeros() -> cons(0(),n__zeros())
 head(cons(X,L)) -> X
 tail(cons(X,L)) -> activate(L)
 incr(X) -> n__incr(X)
 adx(X) -> n__adx(X)
 zeros() -> n__zeros()
 activate(n__incr(X)) -> incr(activate(X))
 activate(n__adx(X)) -> adx(activate(X))
 activate(n__zeros()) -> zeros()
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   incr#(cons(X,L)) -> activate#(L)
   adx#(cons(X,L)) -> activate#(L)
   adx#(cons(X,L)) -> incr#(cons(X,n__adx(activate(L))))
   nats#() -> zeros#()
   nats#() -> adx#(zeros())
   tail#(cons(X,L)) -> activate#(L)
   activate#(n__incr(X)) -> activate#(X)
   activate#(n__incr(X)) -> incr#(activate(X))
   activate#(n__adx(X)) -> activate#(X)
   activate#(n__adx(X)) -> adx#(activate(X))
   activate#(n__zeros()) -> zeros#()
  TRS:
   incr(nil()) -> nil()
   incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
   adx(nil()) -> nil()
   adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
   nats() -> adx(zeros())
   zeros() -> cons(0(),n__zeros())
   head(cons(X,L)) -> X
   tail(cons(X,L)) -> activate(L)
   incr(X) -> n__incr(X)
   adx(X) -> n__adx(X)
   zeros() -> n__zeros()
   activate(n__incr(X)) -> incr(activate(X))
   activate(n__adx(X)) -> adx(activate(X))
   activate(n__zeros()) -> zeros()
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    incr#(cons(X,L)) -> activate#(L)
    adx#(cons(X,L)) -> activate#(L)
    adx#(cons(X,L)) -> incr#(cons(X,n__adx(activate(L))))
    nats#() -> zeros#()
    nats#() -> adx#(zeros())
    tail#(cons(X,L)) -> activate#(L)
    activate#(n__incr(X)) -> activate#(X)
    activate#(n__incr(X)) -> incr#(activate(X))
    activate#(n__adx(X)) -> activate#(X)
    activate#(n__adx(X)) -> adx#(activate(X))
    activate#(n__zeros()) -> zeros#()
   TRS:
    activate(n__incr(X)) -> incr(activate(X))
    activate(n__adx(X)) -> adx(activate(X))
    activate(n__zeros()) -> zeros()
    activate(X) -> X
    incr(nil()) -> nil()
    incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
    incr(X) -> n__incr(X)
    adx(nil()) -> nil()
    adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
    adx(X) -> n__adx(X)
    zeros() -> cons(0(),n__zeros())
    zeros() -> n__zeros()
   EDG Processor:
    DPs:
     incr#(cons(X,L)) -> activate#(L)
     adx#(cons(X,L)) -> activate#(L)
     adx#(cons(X,L)) -> incr#(cons(X,n__adx(activate(L))))
     nats#() -> zeros#()
     nats#() -> adx#(zeros())
     tail#(cons(X,L)) -> activate#(L)
     activate#(n__incr(X)) -> activate#(X)
     activate#(n__incr(X)) -> incr#(activate(X))
     activate#(n__adx(X)) -> activate#(X)
     activate#(n__adx(X)) -> adx#(activate(X))
     activate#(n__zeros()) -> zeros#()
    TRS:
     activate(n__incr(X)) -> incr(activate(X))
     activate(n__adx(X)) -> adx(activate(X))
     activate(n__zeros()) -> zeros()
     activate(X) -> X
     incr(nil()) -> nil()
     incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
     incr(X) -> n__incr(X)
     adx(nil()) -> nil()
     adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
     adx(X) -> n__adx(X)
     zeros() -> cons(0(),n__zeros())
     zeros() -> n__zeros()
    graph:
     tail#(cons(X,L)) -> activate#(L) ->
     activate#(n__incr(X)) -> activate#(X)
     tail#(cons(X,L)) -> activate#(L) ->
     activate#(n__incr(X)) -> incr#(activate(X))
     tail#(cons(X,L)) -> activate#(L) ->
     activate#(n__adx(X)) -> activate#(X)
     tail#(cons(X,L)) -> activate#(L) ->
     activate#(n__adx(X)) -> adx#(activate(X))
     tail#(cons(X,L)) -> activate#(L) -> activate#(n__zeros()) -> zeros#()
     nats#() -> adx#(zeros()) -> adx#(cons(X,L)) -> activate#(L)
     nats#() -> adx#(zeros()) ->
     adx#(cons(X,L)) -> incr#(cons(X,n__adx(activate(L))))
     adx#(cons(X,L)) -> activate#(L) ->
     activate#(n__incr(X)) -> activate#(X)
     adx#(cons(X,L)) -> activate#(L) ->
     activate#(n__incr(X)) -> incr#(activate(X))
     adx#(cons(X,L)) -> activate#(L) ->
     activate#(n__adx(X)) -> activate#(X)
     adx#(cons(X,L)) -> activate#(L) ->
     activate#(n__adx(X)) -> adx#(activate(X))
     adx#(cons(X,L)) -> activate#(L) ->
     activate#(n__zeros()) -> zeros#()
     adx#(cons(X,L)) -> incr#(cons(X,n__adx(activate(L)))) ->
     incr#(cons(X,L)) -> activate#(L)
     activate#(n__adx(X)) -> adx#(activate(X)) ->
     adx#(cons(X,L)) -> activate#(L)
     activate#(n__adx(X)) -> adx#(activate(X)) ->
     adx#(cons(X,L)) -> incr#(cons(X,n__adx(activate(L))))
     activate#(n__adx(X)) -> activate#(X) ->
     activate#(n__incr(X)) -> activate#(X)
     activate#(n__adx(X)) -> activate#(X) ->
     activate#(n__incr(X)) -> incr#(activate(X))
     activate#(n__adx(X)) -> activate#(X) ->
     activate#(n__adx(X)) -> activate#(X)
     activate#(n__adx(X)) -> activate#(X) ->
     activate#(n__adx(X)) -> adx#(activate(X))
     activate#(n__adx(X)) -> activate#(X) ->
     activate#(n__zeros()) -> zeros#()
     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__adx(X)) -> activate#(X)
     activate#(n__incr(X)) -> activate#(X) ->
     activate#(n__adx(X)) -> adx#(activate(X))
     activate#(n__incr(X)) -> activate#(X) ->
     activate#(n__zeros()) -> zeros#()
     activate#(n__incr(X)) -> incr#(activate(X)) ->
     incr#(cons(X,L)) -> activate#(L)
     incr#(cons(X,L)) -> activate#(L) ->
     activate#(n__incr(X)) -> activate#(X)
     incr#(cons(X,L)) -> activate#(L) ->
     activate#(n__incr(X)) -> incr#(activate(X))
     incr#(cons(X,L)) -> activate#(L) ->
     activate#(n__adx(X)) -> activate#(X)
     incr#(cons(X,L)) -> activate#(L) ->
     activate#(n__adx(X)) -> adx#(activate(X))
     incr#(cons(X,L)) -> activate#(L) -> activate#(n__zeros()) -> zeros#()
    Restore Modifier:
     DPs:
      incr#(cons(X,L)) -> activate#(L)
      adx#(cons(X,L)) -> activate#(L)
      adx#(cons(X,L)) -> incr#(cons(X,n__adx(activate(L))))
      nats#() -> zeros#()
      nats#() -> adx#(zeros())
      tail#(cons(X,L)) -> activate#(L)
      activate#(n__incr(X)) -> activate#(X)
      activate#(n__incr(X)) -> incr#(activate(X))
      activate#(n__adx(X)) -> activate#(X)
      activate#(n__adx(X)) -> adx#(activate(X))
      activate#(n__zeros()) -> zeros#()
     TRS:
      incr(nil()) -> nil()
      incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
      adx(nil()) -> nil()
      adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
      nats() -> adx(zeros())
      zeros() -> cons(0(),n__zeros())
      head(cons(X,L)) -> X
      tail(cons(X,L)) -> activate(L)
      incr(X) -> n__incr(X)
      adx(X) -> n__adx(X)
      zeros() -> n__zeros()
      activate(n__incr(X)) -> incr(activate(X))
      activate(n__adx(X)) -> adx(activate(X))
      activate(n__zeros()) -> zeros()
      activate(X) -> X
     SCC Processor:
      #sccs: 1
      #rules: 7
      #arcs: 31/121
      DPs:
       activate#(n__adx(X)) -> adx#(activate(X))
       adx#(cons(X,L)) -> incr#(cons(X,n__adx(activate(L))))
       incr#(cons(X,L)) -> activate#(L)
       activate#(n__adx(X)) -> activate#(X)
       activate#(n__incr(X)) -> incr#(activate(X))
       activate#(n__incr(X)) -> activate#(X)
       adx#(cons(X,L)) -> activate#(L)
      TRS:
       incr(nil()) -> nil()
       incr(cons(X,L)) -> cons(s(X),n__incr(activate(L)))
       adx(nil()) -> nil()
       adx(cons(X,L)) -> incr(cons(X,n__adx(activate(L))))
       nats() -> adx(zeros())
       zeros() -> cons(0(),n__zeros())
       head(cons(X,L)) -> X
       tail(cons(X,L)) -> activate(L)
       incr(X) -> n__incr(X)
       adx(X) -> n__adx(X)
       zeros() -> n__zeros()
       activate(n__incr(X)) -> incr(activate(X))
       activate(n__adx(X)) -> adx(activate(X))
       activate(n__zeros()) -> zeros()
       activate(X) -> X
      Open