MAYBE

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

Proof:
 DP Processor:
  DPs:
   and#(tt(),X) -> activate#(X)
   length#(cons(N,L)) -> activate#(L)
   length#(cons(N,L)) -> length#(activate(L))
   activate#(n__zeros()) -> zeros#()
  TRS:
   zeros() -> cons(0(),n__zeros())
   and(tt(),X) -> activate(X)
   length(nil()) -> 0()
   length(cons(N,L)) -> s(length(activate(L)))
   zeros() -> n__zeros()
   activate(n__zeros()) -> zeros()
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    and#(tt(),X) -> activate#(X)
    length#(cons(N,L)) -> activate#(L)
    length#(cons(N,L)) -> length#(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:
     and#(tt(),X) -> activate#(X)
     length#(cons(N,L)) -> activate#(L)
     length#(cons(N,L)) -> length#(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)) -> length#(activate(L)) ->
     length#(cons(N,L)) -> activate#(L)
     length#(cons(N,L)) -> length#(activate(L)) ->
     length#(cons(N,L)) -> length#(activate(L))
     length#(cons(N,L)) -> activate#(L) ->
     activate#(n__zeros()) -> zeros#()
     and#(tt(),X) -> activate#(X) -> activate#(n__zeros()) -> zeros#()
    Restore Modifier:
     DPs:
      and#(tt(),X) -> activate#(X)
      length#(cons(N,L)) -> activate#(L)
      length#(cons(N,L)) -> length#(activate(L))
      activate#(n__zeros()) -> zeros#()
     TRS:
      zeros() -> cons(0(),n__zeros())
      and(tt(),X) -> activate(X)
      length(nil()) -> 0()
      length(cons(N,L)) -> s(length(activate(L)))
      zeros() -> n__zeros()
      activate(n__zeros()) -> zeros()
      activate(X) -> X
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 4/16
      DPs:
       length#(cons(N,L)) -> length#(activate(L))
      TRS:
       zeros() -> cons(0(),n__zeros())
       and(tt(),X) -> activate(X)
       length(nil()) -> 0()
       length(cons(N,L)) -> s(length(activate(L)))
       zeros() -> n__zeros()
       activate(n__zeros()) -> zeros()
       activate(X) -> X
      Open