MAYBE

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

Proof:
 DP Processor:
  DPs:
   incr#(cons(X,L)) -> incr#(L)
   adx#(cons(X,L)) -> adx#(L)
   adx#(cons(X,L)) -> incr#(cons(X,adx(L)))
   nats#() -> zeros#()
   nats#() -> adx#(zeros())
   zeros#() -> zeros#()
  TRS:
   incr(nil()) -> nil()
   incr(cons(X,L)) -> cons(s(X),incr(L))
   adx(nil()) -> nil()
   adx(cons(X,L)) -> incr(cons(X,adx(L)))
   nats() -> adx(zeros())
   zeros() -> cons(0(),zeros())
   head(cons(X,L)) -> X
   tail(cons(X,L)) -> L
  Usable Rule Processor:
   DPs:
    incr#(cons(X,L)) -> incr#(L)
    adx#(cons(X,L)) -> adx#(L)
    adx#(cons(X,L)) -> incr#(cons(X,adx(L)))
    nats#() -> zeros#()
    nats#() -> adx#(zeros())
    zeros#() -> zeros#()
   TRS:
    adx(nil()) -> nil()
    adx(cons(X,L)) -> incr(cons(X,adx(L)))
    incr(cons(X,L)) -> cons(s(X),incr(L))
    incr(nil()) -> nil()
    zeros() -> cons(0(),zeros())
   TDG Processor:
    DPs:
     incr#(cons(X,L)) -> incr#(L)
     adx#(cons(X,L)) -> adx#(L)
     adx#(cons(X,L)) -> incr#(cons(X,adx(L)))
     nats#() -> zeros#()
     nats#() -> adx#(zeros())
     zeros#() -> zeros#()
    TRS:
     adx(nil()) -> nil()
     adx(cons(X,L)) -> incr(cons(X,adx(L)))
     incr(cons(X,L)) -> cons(s(X),incr(L))
     incr(nil()) -> nil()
     zeros() -> cons(0(),zeros())
    graph:
     zeros#() -> zeros#() -> zeros#() -> zeros#()
     nats#() -> zeros#() -> zeros#() -> zeros#()
     nats#() -> adx#(zeros()) -> adx#(cons(X,L)) -> incr#(cons(X,adx(L)))
     nats#() -> adx#(zeros()) -> adx#(cons(X,L)) -> adx#(L)
     adx#(cons(X,L)) -> adx#(L) ->
     adx#(cons(X,L)) -> incr#(cons(X,adx(L)))
     adx#(cons(X,L)) -> adx#(L) ->
     adx#(cons(X,L)) -> adx#(L)
     adx#(cons(X,L)) -> incr#(cons(X,adx(L))) ->
     incr#(cons(X,L)) -> incr#(L)
     incr#(cons(X,L)) -> incr#(L) -> incr#(cons(X,L)) -> incr#(L)
    Restore Modifier:
     DPs:
      incr#(cons(X,L)) -> incr#(L)
      adx#(cons(X,L)) -> adx#(L)
      adx#(cons(X,L)) -> incr#(cons(X,adx(L)))
      nats#() -> zeros#()
      nats#() -> adx#(zeros())
      zeros#() -> zeros#()
     TRS:
      incr(nil()) -> nil()
      incr(cons(X,L)) -> cons(s(X),incr(L))
      adx(nil()) -> nil()
      adx(cons(X,L)) -> incr(cons(X,adx(L)))
      nats() -> adx(zeros())
      zeros() -> cons(0(),zeros())
      head(cons(X,L)) -> X
      tail(cons(X,L)) -> L
     SCC Processor:
      #sccs: 3
      #rules: 3
      #arcs: 8/36
      DPs:
       adx#(cons(X,L)) -> adx#(L)
      TRS:
       incr(nil()) -> nil()
       incr(cons(X,L)) -> cons(s(X),incr(L))
       adx(nil()) -> nil()
       adx(cons(X,L)) -> incr(cons(X,adx(L)))
       nats() -> adx(zeros())
       zeros() -> cons(0(),zeros())
       head(cons(X,L)) -> X
       tail(cons(X,L)) -> L
      Open
      
      DPs:
       incr#(cons(X,L)) -> incr#(L)
      TRS:
       incr(nil()) -> nil()
       incr(cons(X,L)) -> cons(s(X),incr(L))
       adx(nil()) -> nil()
       adx(cons(X,L)) -> incr(cons(X,adx(L)))
       nats() -> adx(zeros())
       zeros() -> cons(0(),zeros())
       head(cons(X,L)) -> X
       tail(cons(X,L)) -> L
      Open
      
      DPs:
       zeros#() -> zeros#()
      TRS:
       incr(nil()) -> nil()
       incr(cons(X,L)) -> cons(s(X),incr(L))
       adx(nil()) -> nil()
       adx(cons(X,L)) -> incr(cons(X,adx(L)))
       nats() -> adx(zeros())
       zeros() -> cons(0(),zeros())
       head(cons(X,L)) -> X
       tail(cons(X,L)) -> L
      Open