MAYBE

Problem:
 zeros() -> cons(0(),n__zeros())
 U11(tt(),L) -> U12(tt(),activate(L))
 U12(tt(),L) -> s(length(activate(L)))
 length(nil()) -> 0()
 length(cons(N,L)) -> U11(tt(),activate(L))
 zeros() -> n__zeros()
 activate(n__zeros()) -> zeros()
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   U11#(tt(),L) -> activate#(L)
   U11#(tt(),L) -> U12#(tt(),activate(L))
   U12#(tt(),L) -> activate#(L)
   U12#(tt(),L) -> length#(activate(L))
   length#(cons(N,L)) -> activate#(L)
   length#(cons(N,L)) -> U11#(tt(),activate(L))
   activate#(n__zeros()) -> zeros#()
  TRS:
   zeros() -> cons(0(),n__zeros())
   U11(tt(),L) -> U12(tt(),activate(L))
   U12(tt(),L) -> s(length(activate(L)))
   length(nil()) -> 0()
   length(cons(N,L)) -> U11(tt(),activate(L))
   zeros() -> n__zeros()
   activate(n__zeros()) -> zeros()
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    U11#(tt(),L) -> activate#(L)
    U11#(tt(),L) -> U12#(tt(),activate(L))
    U12#(tt(),L) -> activate#(L)
    U12#(tt(),L) -> length#(activate(L))
    length#(cons(N,L)) -> activate#(L)
    length#(cons(N,L)) -> U11#(tt(),activate(L))
    activate#(n__zeros()) -> zeros#()
   TRS:
    activate(n__zeros()) -> zeros()
    activate(X) -> X
    zeros() -> cons(0(),n__zeros())
    zeros() -> n__zeros()
   EDG Processor:
    DPs:
     U11#(tt(),L) -> activate#(L)
     U11#(tt(),L) -> U12#(tt(),activate(L))
     U12#(tt(),L) -> activate#(L)
     U12#(tt(),L) -> length#(activate(L))
     length#(cons(N,L)) -> activate#(L)
     length#(cons(N,L)) -> U11#(tt(),activate(L))
     activate#(n__zeros()) -> zeros#()
    TRS:
     activate(n__zeros()) -> zeros()
     activate(X) -> X
     zeros() -> cons(0(),n__zeros())
     zeros() -> n__zeros()
    graph:
     length#(cons(N,L)) -> activate#(L) ->
     activate#(n__zeros()) -> zeros#()
     length#(cons(N,L)) -> U11#(tt(),activate(L)) ->
     U11#(tt(),L) -> activate#(L)
     length#(cons(N,L)) -> U11#(tt(),activate(L)) ->
     U11#(tt(),L) -> U12#(tt(),activate(L))
     U12#(tt(),L) -> length#(activate(L)) ->
     length#(cons(N,L)) -> activate#(L)
     U12#(tt(),L) -> length#(activate(L)) ->
     length#(cons(N,L)) -> U11#(tt(),activate(L))
     U12#(tt(),L) -> activate#(L) ->
     activate#(n__zeros()) -> zeros#()
     U11#(tt(),L) -> U12#(tt(),activate(L)) ->
     U12#(tt(),L) -> activate#(L)
     U11#(tt(),L) -> U12#(tt(),activate(L)) ->
     U12#(tt(),L) -> length#(activate(L))
     U11#(tt(),L) -> activate#(L) -> activate#(n__zeros()) -> zeros#()
    Restore Modifier:
     DPs:
      U11#(tt(),L) -> activate#(L)
      U11#(tt(),L) -> U12#(tt(),activate(L))
      U12#(tt(),L) -> activate#(L)
      U12#(tt(),L) -> length#(activate(L))
      length#(cons(N,L)) -> activate#(L)
      length#(cons(N,L)) -> U11#(tt(),activate(L))
      activate#(n__zeros()) -> zeros#()
     TRS:
      zeros() -> cons(0(),n__zeros())
      U11(tt(),L) -> U12(tt(),activate(L))
      U12(tt(),L) -> s(length(activate(L)))
      length(nil()) -> 0()
      length(cons(N,L)) -> U11(tt(),activate(L))
      zeros() -> n__zeros()
      activate(n__zeros()) -> zeros()
      activate(X) -> X
     SCC Processor:
      #sccs: 1
      #rules: 3
      #arcs: 9/49
      DPs:
       length#(cons(N,L)) -> U11#(tt(),activate(L))
       U11#(tt(),L) -> U12#(tt(),activate(L))
       U12#(tt(),L) -> length#(activate(L))
      TRS:
       zeros() -> cons(0(),n__zeros())
       U11(tt(),L) -> U12(tt(),activate(L))
       U12(tt(),L) -> s(length(activate(L)))
       length(nil()) -> 0()
       length(cons(N,L)) -> U11(tt(),activate(L))
       zeros() -> n__zeros()
       activate(n__zeros()) -> zeros()
       activate(X) -> X
      Open