MAYBE

Problem:
 from(X) -> cons(X,n__from(s(X)))
 length(n__nil()) -> 0()
 length(n__cons(X,Y)) -> s(length1(activate(Y)))
 length1(X) -> length(activate(X))
 from(X) -> n__from(X)
 nil() -> n__nil()
 cons(X1,X2) -> n__cons(X1,X2)
 activate(n__from(X)) -> from(X)
 activate(n__nil()) -> nil()
 activate(n__cons(X1,X2)) -> cons(X1,X2)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   from#(X) -> cons#(X,n__from(s(X)))
   length#(n__cons(X,Y)) -> activate#(Y)
   length#(n__cons(X,Y)) -> length1#(activate(Y))
   length1#(X) -> activate#(X)
   length1#(X) -> length#(activate(X))
   activate#(n__from(X)) -> from#(X)
   activate#(n__nil()) -> nil#()
   activate#(n__cons(X1,X2)) -> cons#(X1,X2)
  TRS:
   from(X) -> cons(X,n__from(s(X)))
   length(n__nil()) -> 0()
   length(n__cons(X,Y)) -> s(length1(activate(Y)))
   length1(X) -> length(activate(X))
   from(X) -> n__from(X)
   nil() -> n__nil()
   cons(X1,X2) -> n__cons(X1,X2)
   activate(n__from(X)) -> from(X)
   activate(n__nil()) -> nil()
   activate(n__cons(X1,X2)) -> cons(X1,X2)
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    from#(X) -> cons#(X,n__from(s(X)))
    length#(n__cons(X,Y)) -> activate#(Y)
    length#(n__cons(X,Y)) -> length1#(activate(Y))
    length1#(X) -> activate#(X)
    length1#(X) -> length#(activate(X))
    activate#(n__from(X)) -> from#(X)
    activate#(n__nil()) -> nil#()
    activate#(n__cons(X1,X2)) -> cons#(X1,X2)
   TRS:
    f17(x,y) -> x
    f17(x,y) -> y
    activate(n__from(X)) -> from(X)
    activate(n__nil()) -> nil()
    activate(n__cons(X1,X2)) -> cons(X1,X2)
    activate(X) -> X
    from(X) -> cons(X,n__from(s(X)))
    from(X) -> n__from(X)
    cons(X1,X2) -> n__cons(X1,X2)
    nil() -> n__nil()
   EDG Processor:
    DPs:
     from#(X) -> cons#(X,n__from(s(X)))
     length#(n__cons(X,Y)) -> activate#(Y)
     length#(n__cons(X,Y)) -> length1#(activate(Y))
     length1#(X) -> activate#(X)
     length1#(X) -> length#(activate(X))
     activate#(n__from(X)) -> from#(X)
     activate#(n__nil()) -> nil#()
     activate#(n__cons(X1,X2)) -> cons#(X1,X2)
    TRS:
     f17(x,y) -> x
     f17(x,y) -> y
     activate(n__from(X)) -> from(X)
     activate(n__nil()) -> nil()
     activate(n__cons(X1,X2)) -> cons(X1,X2)
     activate(X) -> X
     from(X) -> cons(X,n__from(s(X)))
     from(X) -> n__from(X)
     cons(X1,X2) -> n__cons(X1,X2)
     nil() -> n__nil()
    graph:
     length1#(X) -> activate#(X) -> activate#(n__from(X)) -> from#(X)
     length1#(X) -> activate#(X) -> activate#(n__nil()) -> nil#()
     length1#(X) -> activate#(X) ->
     activate#(n__cons(X1,X2)) -> cons#(X1,X2)
     length1#(X) -> length#(activate(X)) ->
     length#(n__cons(X,Y)) -> activate#(Y)
     length1#(X) -> length#(activate(X)) ->
     length#(n__cons(X,Y)) -> length1#(activate(Y))
     activate#(n__from(X)) -> from#(X) ->
     from#(X) -> cons#(X,n__from(s(X)))
     length#(n__cons(X,Y)) -> length1#(activate(Y)) ->
     length1#(X) -> activate#(X)
     length#(n__cons(X,Y)) -> length1#(activate(Y)) ->
     length1#(X) -> length#(activate(X))
     length#(n__cons(X,Y)) -> activate#(Y) ->
     activate#(n__from(X)) -> from#(X)
     length#(n__cons(X,Y)) -> activate#(Y) ->
     activate#(n__nil()) -> nil#()
     length#(n__cons(X,Y)) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> cons#(X1,X2)
    Restore Modifier:
     DPs:
      from#(X) -> cons#(X,n__from(s(X)))
      length#(n__cons(X,Y)) -> activate#(Y)
      length#(n__cons(X,Y)) -> length1#(activate(Y))
      length1#(X) -> activate#(X)
      length1#(X) -> length#(activate(X))
      activate#(n__from(X)) -> from#(X)
      activate#(n__nil()) -> nil#()
      activate#(n__cons(X1,X2)) -> cons#(X1,X2)
     TRS:
      from(X) -> cons(X,n__from(s(X)))
      length(n__nil()) -> 0()
      length(n__cons(X,Y)) -> s(length1(activate(Y)))
      length1(X) -> length(activate(X))
      from(X) -> n__from(X)
      nil() -> n__nil()
      cons(X1,X2) -> n__cons(X1,X2)
      activate(n__from(X)) -> from(X)
      activate(n__nil()) -> nil()
      activate(n__cons(X1,X2)) -> cons(X1,X2)
      activate(X) -> X
     SCC Processor:
      #sccs: 1
      #rules: 2
      #arcs: 11/64
      DPs:
       length1#(X) -> length#(activate(X))
       length#(n__cons(X,Y)) -> length1#(activate(Y))
      TRS:
       from(X) -> cons(X,n__from(s(X)))
       length(n__nil()) -> 0()
       length(n__cons(X,Y)) -> s(length1(activate(Y)))
       length1(X) -> length(activate(X))
       from(X) -> n__from(X)
       nil() -> n__nil()
       cons(X1,X2) -> n__cons(X1,X2)
       activate(n__from(X)) -> from(X)
       activate(n__nil()) -> nil()
       activate(n__cons(X1,X2)) -> cons(X1,X2)
       activate(X) -> X
      Open