MAYBE

Problem:
 active(from(X)) -> mark(cons(X,from(s(X))))
 active(length(nil())) -> mark(0())
 active(length(cons(X,Y))) -> mark(s(length1(Y)))
 active(length1(X)) -> mark(length(X))
 mark(from(X)) -> active(from(mark(X)))
 mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
 mark(s(X)) -> active(s(mark(X)))
 mark(length(X)) -> active(length(X))
 mark(nil()) -> active(nil())
 mark(0()) -> active(0())
 mark(length1(X)) -> active(length1(X))
 from(mark(X)) -> from(X)
 from(active(X)) -> from(X)
 cons(mark(X1),X2) -> cons(X1,X2)
 cons(X1,mark(X2)) -> cons(X1,X2)
 cons(active(X1),X2) -> cons(X1,X2)
 cons(X1,active(X2)) -> cons(X1,X2)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 length(mark(X)) -> length(X)
 length(active(X)) -> length(X)
 length1(mark(X)) -> length1(X)
 length1(active(X)) -> length1(X)

Proof:
 DP Processor:
  DPs:
   active#(from(X)) -> s#(X)
   active#(from(X)) -> from#(s(X))
   active#(from(X)) -> cons#(X,from(s(X)))
   active#(from(X)) -> mark#(cons(X,from(s(X))))
   active#(length(nil())) -> mark#(0())
   active#(length(cons(X,Y))) -> length1#(Y)
   active#(length(cons(X,Y))) -> s#(length1(Y))
   active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
   active#(length1(X)) -> length#(X)
   active#(length1(X)) -> mark#(length(X))
   mark#(from(X)) -> mark#(X)
   mark#(from(X)) -> from#(mark(X))
   mark#(from(X)) -> active#(from(mark(X)))
   mark#(cons(X1,X2)) -> mark#(X1)
   mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
   mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
   mark#(s(X)) -> mark#(X)
   mark#(s(X)) -> s#(mark(X))
   mark#(s(X)) -> active#(s(mark(X)))
   mark#(length(X)) -> active#(length(X))
   mark#(nil()) -> active#(nil())
   mark#(0()) -> active#(0())
   mark#(length1(X)) -> active#(length1(X))
   from#(mark(X)) -> from#(X)
   from#(active(X)) -> from#(X)
   cons#(mark(X1),X2) -> cons#(X1,X2)
   cons#(X1,mark(X2)) -> cons#(X1,X2)
   cons#(active(X1),X2) -> cons#(X1,X2)
   cons#(X1,active(X2)) -> cons#(X1,X2)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
   length#(mark(X)) -> length#(X)
   length#(active(X)) -> length#(X)
   length1#(mark(X)) -> length1#(X)
   length1#(active(X)) -> length1#(X)
  TRS:
   active(from(X)) -> mark(cons(X,from(s(X))))
   active(length(nil())) -> mark(0())
   active(length(cons(X,Y))) -> mark(s(length1(Y)))
   active(length1(X)) -> mark(length(X))
   mark(from(X)) -> active(from(mark(X)))
   mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
   mark(s(X)) -> active(s(mark(X)))
   mark(length(X)) -> active(length(X))
   mark(nil()) -> active(nil())
   mark(0()) -> active(0())
   mark(length1(X)) -> active(length1(X))
   from(mark(X)) -> from(X)
   from(active(X)) -> from(X)
   cons(mark(X1),X2) -> cons(X1,X2)
   cons(X1,mark(X2)) -> cons(X1,X2)
   cons(active(X1),X2) -> cons(X1,X2)
   cons(X1,active(X2)) -> cons(X1,X2)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   length(mark(X)) -> length(X)
   length(active(X)) -> length(X)
   length1(mark(X)) -> length1(X)
   length1(active(X)) -> length1(X)
  CDG Processor:
   DPs:
    active#(from(X)) -> s#(X)
    active#(from(X)) -> from#(s(X))
    active#(from(X)) -> cons#(X,from(s(X)))
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    active#(length(nil())) -> mark#(0())
    active#(length(cons(X,Y))) -> length1#(Y)
    active#(length(cons(X,Y))) -> s#(length1(Y))
    active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
    active#(length1(X)) -> length#(X)
    active#(length1(X)) -> mark#(length(X))
    mark#(from(X)) -> mark#(X)
    mark#(from(X)) -> from#(mark(X))
    mark#(from(X)) -> active#(from(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(length(X)) -> active#(length(X))
    mark#(nil()) -> active#(nil())
    mark#(0()) -> active#(0())
    mark#(length1(X)) -> active#(length1(X))
    from#(mark(X)) -> from#(X)
    from#(active(X)) -> from#(X)
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
    length#(mark(X)) -> length#(X)
    length#(active(X)) -> length#(X)
    length1#(mark(X)) -> length1#(X)
    length1#(active(X)) -> length1#(X)
   TRS:
    active(from(X)) -> mark(cons(X,from(s(X))))
    active(length(nil())) -> mark(0())
    active(length(cons(X,Y))) -> mark(s(length1(Y)))
    active(length1(X)) -> mark(length(X))
    mark(from(X)) -> active(from(mark(X)))
    mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
    mark(s(X)) -> active(s(mark(X)))
    mark(length(X)) -> active(length(X))
    mark(nil()) -> active(nil())
    mark(0()) -> active(0())
    mark(length1(X)) -> active(length1(X))
    from(mark(X)) -> from(X)
    from(active(X)) -> from(X)
    cons(mark(X1),X2) -> cons(X1,X2)
    cons(X1,mark(X2)) -> cons(X1,X2)
    cons(active(X1),X2) -> cons(X1,X2)
    cons(X1,active(X2)) -> cons(X1,X2)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    length(mark(X)) -> length(X)
    length(active(X)) -> length(X)
    length1(mark(X)) -> length1(X)
    length1(active(X)) -> length1(X)
   graph:
    length#(mark(X)) -> length#(X) -> length#(mark(X)) -> length#(X)
    length#(mark(X)) -> length#(X) ->
    length#(active(X)) -> length#(X)
    length#(active(X)) -> length#(X) ->
    length#(mark(X)) -> length#(X)
    length#(active(X)) -> length#(X) ->
    length#(active(X)) -> length#(X)
    length1#(mark(X)) -> length1#(X) ->
    length1#(mark(X)) -> length1#(X)
    length1#(mark(X)) -> length1#(X) ->
    length1#(active(X)) -> length1#(X)
    length1#(active(X)) -> length1#(X) ->
    length1#(mark(X)) -> length1#(X)
    length1#(active(X)) -> length1#(X) ->
    length1#(active(X)) -> length1#(X)
    mark#(length1(X)) -> active#(length1(X)) ->
    active#(length1(X)) -> length#(X)
    mark#(length1(X)) -> active#(length1(X)) ->
    active#(length1(X)) -> mark#(length(X))
    mark#(length(X)) -> active#(length(X)) ->
    active#(length(nil())) -> mark#(0())
    mark#(length(X)) -> active#(length(X)) ->
    active#(length(cons(X,Y))) -> length1#(Y)
    mark#(length(X)) -> active#(length(X)) ->
    active#(length(cons(X,Y))) -> s#(length1(Y))
    mark#(length(X)) -> active#(length(X)) ->
    active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> from#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> active#(from(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> active#(length(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(nil()) -> active#(nil())
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(length1(X)) -> active#(length1(X))
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> from#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> active#(from(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(length(X)) -> active#(length(X))
    mark#(s(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
    mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(s(X)) -> mark#(X) -> mark#(length1(X)) -> active#(length1(X))
    mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X)
    mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X)
    mark#(from(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
    mark#(from(X)) -> mark#(X) -> mark#(from(X)) -> from#(mark(X))
    mark#(from(X)) -> mark#(X) ->
    mark#(from(X)) -> active#(from(mark(X)))
    mark#(from(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(from(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(from(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(from(X)) -> mark#(X) -> mark#(length(X)) -> active#(length(X))
    mark#(from(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
    mark#(from(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(from(X)) -> mark#(X) ->
    mark#(length1(X)) -> active#(length1(X))
    mark#(from(X)) -> from#(mark(X)) -> from#(mark(X)) -> from#(X)
    mark#(from(X)) -> from#(mark(X)) ->
    from#(active(X)) -> from#(X)
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(from(X)) -> s#(X)
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(from(X)) -> from#(s(X))
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    from#(mark(X)) -> from#(X) -> from#(mark(X)) -> from#(X)
    from#(mark(X)) -> from#(X) -> from#(active(X)) -> from#(X)
    from#(active(X)) -> from#(X) -> from#(mark(X)) -> from#(X)
    from#(active(X)) -> from#(X) -> from#(active(X)) -> from#(X)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    active#(length1(X)) -> length#(X) ->
    length#(mark(X)) -> length#(X)
    active#(length1(X)) -> length#(X) ->
    length#(active(X)) -> length#(X)
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(length(X)) -> active#(length(X))
    active#(length(nil())) -> mark#(0()) ->
    mark#(0()) -> active#(0())
    active#(length(cons(X,Y))) -> length1#(Y) ->
    length1#(mark(X)) -> length1#(X)
    active#(length(cons(X,Y))) -> length1#(Y) ->
    length1#(active(X)) -> length1#(X)
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(s(X)) -> mark#(X)
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(from(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    active#(from(X)) -> s#(X) -> s#(active(X)) -> s#(X)
   Restore Modifier:
    DPs:
     active#(from(X)) -> s#(X)
     active#(from(X)) -> from#(s(X))
     active#(from(X)) -> cons#(X,from(s(X)))
     active#(from(X)) -> mark#(cons(X,from(s(X))))
     active#(length(nil())) -> mark#(0())
     active#(length(cons(X,Y))) -> length1#(Y)
     active#(length(cons(X,Y))) -> s#(length1(Y))
     active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
     active#(length1(X)) -> length#(X)
     active#(length1(X)) -> mark#(length(X))
     mark#(from(X)) -> mark#(X)
     mark#(from(X)) -> from#(mark(X))
     mark#(from(X)) -> active#(from(mark(X)))
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     mark#(s(X)) -> mark#(X)
     mark#(s(X)) -> s#(mark(X))
     mark#(s(X)) -> active#(s(mark(X)))
     mark#(length(X)) -> active#(length(X))
     mark#(nil()) -> active#(nil())
     mark#(0()) -> active#(0())
     mark#(length1(X)) -> active#(length1(X))
     from#(mark(X)) -> from#(X)
     from#(active(X)) -> from#(X)
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(X1,mark(X2)) -> cons#(X1,X2)
     cons#(active(X1),X2) -> cons#(X1,X2)
     cons#(X1,active(X2)) -> cons#(X1,X2)
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
     length#(mark(X)) -> length#(X)
     length#(active(X)) -> length#(X)
     length1#(mark(X)) -> length1#(X)
     length1#(active(X)) -> length1#(X)
    TRS:
     active(from(X)) -> mark(cons(X,from(s(X))))
     active(length(nil())) -> mark(0())
     active(length(cons(X,Y))) -> mark(s(length1(Y)))
     active(length1(X)) -> mark(length(X))
     mark(from(X)) -> active(from(mark(X)))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(s(X)) -> active(s(mark(X)))
     mark(length(X)) -> active(length(X))
     mark(nil()) -> active(nil())
     mark(0()) -> active(0())
     mark(length1(X)) -> active(length1(X))
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     length(mark(X)) -> length(X)
     length(active(X)) -> length(X)
     length1(mark(X)) -> length1(X)
     length1(active(X)) -> length1(X)
    SCC Processor:
     #sccs: 6
     #rules: 21
     #arcs: 105/1225
     DPs:
      mark#(length1(X)) -> active#(length1(X))
      active#(length1(X)) -> mark#(length(X))
      mark#(length(X)) -> active#(length(X))
      active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
      mark#(s(X)) -> mark#(X)
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(from(X)) -> active#(from(mark(X)))
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(from(X)) -> mark#(X)
     TRS:
      active(from(X)) -> mark(cons(X,from(s(X))))
      active(length(nil())) -> mark(0())
      active(length(cons(X,Y))) -> mark(s(length1(Y)))
      active(length1(X)) -> mark(length(X))
      mark(from(X)) -> active(from(mark(X)))
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(X))
      mark(nil()) -> active(nil())
      mark(0()) -> active(0())
      mark(length1(X)) -> active(length1(X))
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      length1(mark(X)) -> length1(X)
      length1(active(X)) -> length1(X)
     Open
     
     DPs:
      from#(active(X)) -> from#(X)
      from#(mark(X)) -> from#(X)
     TRS:
      active(from(X)) -> mark(cons(X,from(s(X))))
      active(length(nil())) -> mark(0())
      active(length(cons(X,Y))) -> mark(s(length1(Y)))
      active(length1(X)) -> mark(length(X))
      mark(from(X)) -> active(from(mark(X)))
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(X))
      mark(nil()) -> active(nil())
      mark(0()) -> active(0())
      mark(length1(X)) -> active(length1(X))
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      length1(mark(X)) -> length1(X)
      length1(active(X)) -> length1(X)
     Open
     
     DPs:
      cons#(X1,active(X2)) -> cons#(X1,X2)
      cons#(active(X1),X2) -> cons#(X1,X2)
      cons#(X1,mark(X2)) -> cons#(X1,X2)
      cons#(mark(X1),X2) -> cons#(X1,X2)
     TRS:
      active(from(X)) -> mark(cons(X,from(s(X))))
      active(length(nil())) -> mark(0())
      active(length(cons(X,Y))) -> mark(s(length1(Y)))
      active(length1(X)) -> mark(length(X))
      mark(from(X)) -> active(from(mark(X)))
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(X))
      mark(nil()) -> active(nil())
      mark(0()) -> active(0())
      mark(length1(X)) -> active(length1(X))
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      length1(mark(X)) -> length1(X)
      length1(active(X)) -> length1(X)
     Open
     
     DPs:
      s#(active(X)) -> s#(X)
      s#(mark(X)) -> s#(X)
     TRS:
      active(from(X)) -> mark(cons(X,from(s(X))))
      active(length(nil())) -> mark(0())
      active(length(cons(X,Y))) -> mark(s(length1(Y)))
      active(length1(X)) -> mark(length(X))
      mark(from(X)) -> active(from(mark(X)))
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(X))
      mark(nil()) -> active(nil())
      mark(0()) -> active(0())
      mark(length1(X)) -> active(length1(X))
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      length1(mark(X)) -> length1(X)
      length1(active(X)) -> length1(X)
     Open
     
     DPs:
      length1#(mark(X)) -> length1#(X)
      length1#(active(X)) -> length1#(X)
     TRS:
      active(from(X)) -> mark(cons(X,from(s(X))))
      active(length(nil())) -> mark(0())
      active(length(cons(X,Y))) -> mark(s(length1(Y)))
      active(length1(X)) -> mark(length(X))
      mark(from(X)) -> active(from(mark(X)))
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(X))
      mark(nil()) -> active(nil())
      mark(0()) -> active(0())
      mark(length1(X)) -> active(length1(X))
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      length1(mark(X)) -> length1(X)
      length1(active(X)) -> length1(X)
     Open
     
     DPs:
      length#(mark(X)) -> length#(X)
      length#(active(X)) -> length#(X)
     TRS:
      active(from(X)) -> mark(cons(X,from(s(X))))
      active(length(nil())) -> mark(0())
      active(length(cons(X,Y))) -> mark(s(length1(Y)))
      active(length1(X)) -> mark(length(X))
      mark(from(X)) -> active(from(mark(X)))
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(X))
      mark(nil()) -> active(nil())
      mark(0()) -> active(0())
      mark(length1(X)) -> active(length1(X))
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      length1(mark(X)) -> length1(X)
      length1(active(X)) -> length1(X)
     Open