MAYBE

Problem:
 from(X) -> cons(X,n__from(n__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)
 s(X) -> n__s(X)
 nil() -> n__nil()
 cons(X1,X2) -> n__cons(X1,X2)
 activate(n__from(X)) -> from(activate(X))
 activate(n__s(X)) -> s(activate(X))
 activate(n__nil()) -> nil()
 activate(n__cons(X1,X2)) -> cons(activate(X1),X2)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   from#(X) -> cons#(X,n__from(n__s(X)))
   length#(n__cons(X,Y)) -> activate#(Y)
   length#(n__cons(X,Y)) -> length1#(activate(Y))
   length#(n__cons(X,Y)) -> s#(length1(activate(Y)))
   length1#(X) -> activate#(X)
   length1#(X) -> length#(activate(X))
   activate#(n__from(X)) -> activate#(X)
   activate#(n__from(X)) -> from#(activate(X))
   activate#(n__s(X)) -> activate#(X)
   activate#(n__s(X)) -> s#(activate(X))
   activate#(n__nil()) -> nil#()
   activate#(n__cons(X1,X2)) -> activate#(X1)
   activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2)
  TRS:
   from(X) -> cons(X,n__from(n__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)
   s(X) -> n__s(X)
   nil() -> n__nil()
   cons(X1,X2) -> n__cons(X1,X2)
   activate(n__from(X)) -> from(activate(X))
   activate(n__s(X)) -> s(activate(X))
   activate(n__nil()) -> nil()
   activate(n__cons(X1,X2)) -> cons(activate(X1),X2)
   activate(X) -> X
  ADG Processor:
   DPs:
    from#(X) -> cons#(X,n__from(n__s(X)))
    length#(n__cons(X,Y)) -> activate#(Y)
    length#(n__cons(X,Y)) -> length1#(activate(Y))
    length#(n__cons(X,Y)) -> s#(length1(activate(Y)))
    length1#(X) -> activate#(X)
    length1#(X) -> length#(activate(X))
    activate#(n__from(X)) -> activate#(X)
    activate#(n__from(X)) -> from#(activate(X))
    activate#(n__s(X)) -> activate#(X)
    activate#(n__s(X)) -> s#(activate(X))
    activate#(n__nil()) -> nil#()
    activate#(n__cons(X1,X2)) -> activate#(X1)
    activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2)
   TRS:
    from(X) -> cons(X,n__from(n__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)
    s(X) -> n__s(X)
    nil() -> n__nil()
    cons(X1,X2) -> n__cons(X1,X2)
    activate(n__from(X)) -> from(activate(X))
    activate(n__s(X)) -> s(activate(X))
    activate(n__nil()) -> nil()
    activate(n__cons(X1,X2)) -> cons(activate(X1),X2)
    activate(X) -> X
   graph:
    length1#(X) -> activate#(X) -> activate#(n__from(X)) -> activate#(X)
    length1#(X) -> activate#(X) ->
    activate#(n__from(X)) -> from#(activate(X))
    length1#(X) -> activate#(X) -> activate#(n__s(X)) -> activate#(X)
    length1#(X) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X))
    length1#(X) -> activate#(X) -> activate#(n__nil()) -> nil#()
    length1#(X) -> activate#(X) ->
    activate#(n__cons(X1,X2)) -> activate#(X1)
    length1#(X) -> activate#(X) ->
    activate#(n__cons(X1,X2)) -> cons#(activate(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))
    length1#(X) -> length#(activate(X)) ->
    length#(n__cons(X,Y)) -> s#(length1(activate(Y)))
    activate#(n__cons(X1,X2)) -> activate#(X1) ->
    activate#(n__from(X)) -> activate#(X)
    activate#(n__cons(X1,X2)) -> activate#(X1) ->
    activate#(n__from(X)) -> from#(activate(X))
    activate#(n__cons(X1,X2)) -> activate#(X1) ->
    activate#(n__s(X)) -> activate#(X)
    activate#(n__cons(X1,X2)) -> activate#(X1) ->
    activate#(n__s(X)) -> s#(activate(X))
    activate#(n__cons(X1,X2)) -> activate#(X1) ->
    activate#(n__nil()) -> nil#()
    activate#(n__cons(X1,X2)) -> activate#(X1) ->
    activate#(n__cons(X1,X2)) -> activate#(X1)
    activate#(n__cons(X1,X2)) -> activate#(X1) ->
    activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2)
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__from(X)) -> activate#(X)
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__from(X)) -> from#(activate(X))
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__s(X)) -> activate#(X)
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__s(X)) -> s#(activate(X))
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__nil()) -> nil#()
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__cons(X1,X2)) -> activate#(X1)
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2)
    activate#(n__from(X)) -> from#(activate(X)) ->
    from#(X) -> cons#(X,n__from(n__s(X)))
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__from(X)) -> activate#(X)
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__from(X)) -> from#(activate(X))
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__s(X)) -> activate#(X)
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__s(X)) -> s#(activate(X))
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__nil()) -> nil#()
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__cons(X1,X2)) -> activate#(X1)
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2)
    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)) -> activate#(X)
    length#(n__cons(X,Y)) -> activate#(Y) ->
    activate#(n__from(X)) -> from#(activate(X))
    length#(n__cons(X,Y)) -> activate#(Y) ->
    activate#(n__s(X)) -> activate#(X)
    length#(n__cons(X,Y)) -> activate#(Y) ->
    activate#(n__s(X)) -> s#(activate(X))
    length#(n__cons(X,Y)) -> activate#(Y) ->
    activate#(n__nil()) -> nil#()
    length#(n__cons(X,Y)) -> activate#(Y) ->
    activate#(n__cons(X1,X2)) -> activate#(X1)
    length#(n__cons(X,Y)) -> activate#(Y) -> activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2)
   SCC Processor:
    #sccs: 2
    #rules: 5
    #arcs: 41/169
    DPs:
     length1#(X) -> length#(activate(X))
     length#(n__cons(X,Y)) -> length1#(activate(Y))
    TRS:
     from(X) -> cons(X,n__from(n__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)
     s(X) -> n__s(X)
     nil() -> n__nil()
     cons(X1,X2) -> n__cons(X1,X2)
     activate(n__from(X)) -> from(activate(X))
     activate(n__s(X)) -> s(activate(X))
     activate(n__nil()) -> nil()
     activate(n__cons(X1,X2)) -> cons(activate(X1),X2)
     activate(X) -> X
    Open
    
    DPs:
     activate#(n__cons(X1,X2)) -> activate#(X1)
     activate#(n__s(X)) -> activate#(X)
     activate#(n__from(X)) -> activate#(X)
    TRS:
     from(X) -> cons(X,n__from(n__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)
     s(X) -> n__s(X)
     nil() -> n__nil()
     cons(X1,X2) -> n__cons(X1,X2)
     activate(n__from(X)) -> from(activate(X))
     activate(n__s(X)) -> s(activate(X))
     activate(n__nil()) -> nil()
     activate(n__cons(X1,X2)) -> cons(activate(X1),X2)
     activate(X) -> X
    Open