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)
  TDG 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#(active(X)) -> length#(X)
    length#(mark(X)) -> length#(X) ->
    length#(mark(X)) -> length#(X)
    length#(active(X)) -> length#(X) ->
    length#(active(X)) -> length#(X)
    length#(active(X)) -> length#(X) ->
    length#(mark(X)) -> length#(X)
    length1#(mark(X)) -> length1#(X) ->
    length1#(active(X)) -> length1#(X)
    length1#(mark(X)) -> length1#(X) ->
    length1#(mark(X)) -> length1#(X)
    length1#(active(X)) -> length1#(X) ->
    length1#(active(X)) -> length1#(X)
    length1#(active(X)) -> length1#(X) ->
    length1#(mark(X)) -> length1#(X)
    mark#(length1(X)) -> active#(length1(X)) ->
    active#(length1(X)) -> mark#(length(X))
    mark#(length1(X)) -> active#(length1(X)) ->
    active#(length1(X)) -> length#(X)
    mark#(length1(X)) -> active#(length1(X)) ->
    active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
    mark#(length1(X)) -> active#(length1(X)) ->
    active#(length(cons(X,Y))) -> s#(length1(Y))
    mark#(length1(X)) -> active#(length1(X)) ->
    active#(length(cons(X,Y))) -> length1#(Y)
    mark#(length1(X)) -> active#(length1(X)) ->
    active#(length(nil())) -> mark#(0())
    mark#(length1(X)) -> active#(length1(X)) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(length1(X)) -> active#(length1(X)) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(length1(X)) -> active#(length1(X)) ->
    active#(from(X)) -> from#(s(X))
    mark#(length1(X)) -> active#(length1(X)) -> active#(from(X)) -> s#(X)
    mark#(0()) -> active#(0()) -> active#(length1(X)) -> mark#(length(X))
    mark#(0()) -> active#(0()) -> active#(length1(X)) -> length#(X)
    mark#(0()) -> active#(0()) ->
    active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
    mark#(0()) -> active#(0()) ->
    active#(length(cons(X,Y))) -> s#(length1(Y))
    mark#(0()) -> active#(0()) ->
    active#(length(cons(X,Y))) -> length1#(Y)
    mark#(0()) -> active#(0()) -> active#(length(nil())) -> mark#(0())
    mark#(0()) -> active#(0()) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(0()) -> active#(0()) -> active#(from(X)) -> cons#(X,from(s(X)))
    mark#(0()) -> active#(0()) -> active#(from(X)) -> from#(s(X))
    mark#(0()) -> active#(0()) -> active#(from(X)) -> s#(X)
    mark#(length(X)) -> active#(length(X)) ->
    active#(length1(X)) -> mark#(length(X))
    mark#(length(X)) -> active#(length(X)) ->
    active#(length1(X)) -> length#(X)
    mark#(length(X)) -> active#(length(X)) ->
    active#(length(cons(X,Y))) -> mark#(s(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))) -> length1#(Y)
    mark#(length(X)) -> active#(length(X)) ->
    active#(length(nil())) -> mark#(0())
    mark#(length(X)) -> active#(length(X)) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(length(X)) -> active#(length(X)) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(length(X)) -> active#(length(X)) ->
    active#(from(X)) -> from#(s(X))
    mark#(length(X)) -> active#(length(X)) ->
    active#(from(X)) -> s#(X)
    mark#(nil()) -> active#(nil()) ->
    active#(length1(X)) -> mark#(length(X))
    mark#(nil()) -> active#(nil()) ->
    active#(length1(X)) -> length#(X)
    mark#(nil()) -> active#(nil()) ->
    active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
    mark#(nil()) -> active#(nil()) ->
    active#(length(cons(X,Y))) -> s#(length1(Y))
    mark#(nil()) -> active#(nil()) ->
    active#(length(cons(X,Y))) -> length1#(Y)
    mark#(nil()) -> active#(nil()) ->
    active#(length(nil())) -> mark#(0())
    mark#(nil()) -> active#(nil()) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(nil()) -> active#(nil()) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(nil()) -> active#(nil()) -> active#(from(X)) -> from#(s(X))
    mark#(nil()) -> active#(nil()) -> active#(from(X)) -> s#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(length1(X)) -> active#(length1(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(nil()) -> active#(nil())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> active#(length(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> active#(from(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> from#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(X1,active(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,mark(X2)) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length1(X)) -> mark#(length(X))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length1(X)) -> length#(X)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(cons(X,Y))) -> s#(length1(Y))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(cons(X,Y))) -> length1#(Y)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(nil())) -> mark#(0())
    mark#(cons(X1,X2)) -> active#(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)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(from(X)) -> from#(s(X))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(from(X)) -> s#(X)
    mark#(s(X)) -> mark#(X) -> mark#(length1(X)) -> active#(length1(X))
    mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(s(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
    mark#(s(X)) -> mark#(X) -> mark#(length(X)) -> active#(length(X))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> active#(from(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> from#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
    mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X)
    mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length1(X)) -> mark#(length(X))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length1(X)) -> length#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(cons(X,Y))) -> s#(length1(Y))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(cons(X,Y))) -> length1#(Y)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(nil())) -> mark#(0())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(from(X)) -> from#(s(X))
    mark#(s(X)) -> active#(s(mark(X))) -> active#(from(X)) -> s#(X)
    mark#(from(X)) -> mark#(X) ->
    mark#(length1(X)) -> active#(length1(X))
    mark#(from(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(from(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
    mark#(from(X)) -> mark#(X) -> mark#(length(X)) -> active#(length(X))
    mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(from(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(from(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(from(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(from(X)) -> mark#(X) ->
    mark#(from(X)) -> active#(from(mark(X)))
    mark#(from(X)) -> mark#(X) -> mark#(from(X)) -> from#(mark(X))
    mark#(from(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
    mark#(from(X)) -> from#(mark(X)) ->
    from#(active(X)) -> from#(X)
    mark#(from(X)) -> from#(mark(X)) ->
    from#(mark(X)) -> from#(X)
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(length1(X)) -> mark#(length(X))
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(length1(X)) -> length#(X)
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(length(cons(X,Y))) -> s#(length1(Y))
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(length(cons(X,Y))) -> length1#(Y)
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(length(nil())) -> mark#(0())
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(from(X)) -> mark#(cons(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)) -> from#(s(X))
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(from(X)) -> s#(X)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,active(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,mark(X2)) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,active(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,mark(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(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,mark(X2)) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(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,mark(X2)) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    from#(mark(X)) -> from#(X) -> from#(active(X)) -> from#(X)
    from#(mark(X)) -> from#(X) -> from#(mark(X)) -> from#(X)
    from#(active(X)) -> from#(X) -> from#(active(X)) -> from#(X)
    from#(active(X)) -> from#(X) -> from#(mark(X)) -> from#(X)
    s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    active#(length1(X)) -> length#(X) ->
    length#(active(X)) -> length#(X)
    active#(length1(X)) -> length#(X) ->
    length#(mark(X)) -> length#(X)
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(length1(X)) -> active#(length1(X))
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(0()) -> active#(0())
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(nil()) -> active#(nil())
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(length(X)) -> active#(length(X))
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(s(X)) -> s#(mark(X))
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(s(X)) -> mark#(X)
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(from(X)) -> active#(from(mark(X)))
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(from(X)) -> from#(mark(X))
    active#(length1(X)) -> mark#(length(X)) ->
    mark#(from(X)) -> mark#(X)
    active#(length(nil())) -> mark#(0()) ->
    mark#(length1(X)) -> active#(length1(X))
    active#(length(nil())) -> mark#(0()) ->
    mark#(0()) -> active#(0())
    active#(length(nil())) -> mark#(0()) ->
    mark#(nil()) -> active#(nil())
    active#(length(nil())) -> mark#(0()) ->
    mark#(length(X)) -> active#(length(X))
    active#(length(nil())) -> mark#(0()) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(length(nil())) -> mark#(0()) ->
    mark#(s(X)) -> s#(mark(X))
    active#(length(nil())) -> mark#(0()) ->
    mark#(s(X)) -> mark#(X)
    active#(length(nil())) -> mark#(0()) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(length(nil())) -> mark#(0()) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(length(nil())) -> mark#(0()) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(length(nil())) -> mark#(0()) ->
    mark#(from(X)) -> active#(from(mark(X)))
    active#(length(nil())) -> mark#(0()) ->
    mark#(from(X)) -> from#(mark(X))
    active#(length(nil())) -> mark#(0()) ->
    mark#(from(X)) -> mark#(X)
    active#(length(cons(X,Y))) -> length1#(Y) ->
    length1#(active(X)) -> length1#(X)
    active#(length(cons(X,Y))) -> length1#(Y) ->
    length1#(mark(X)) -> length1#(X)
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(length1(X)) -> active#(length1(X))
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(0()) -> active#(0())
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(nil()) -> active#(nil())
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(length(X)) -> active#(length(X))
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(s(X)) -> active#(s(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)) -> mark#(X)
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(from(X)) -> active#(from(mark(X)))
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(from(X)) -> from#(mark(X))
    active#(length(cons(X,Y))) -> mark#(s(length1(Y))) ->
    mark#(from(X)) -> mark#(X)
    active#(length(cons(X,Y))) -> s#(length1(Y)) ->
    s#(active(X)) -> s#(X)
    active#(length(cons(X,Y))) -> s#(length1(Y)) ->
    s#(mark(X)) -> s#(X)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(length1(X)) -> active#(length1(X))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(0()) -> active#(0())
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(nil()) -> active#(nil())
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(length(X)) -> active#(length(X))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(s(X)) -> mark#(X)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    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)) -> mark#(X1)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(from(X)) -> active#(from(mark(X)))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(from(X)) -> from#(mark(X))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(from(X)) -> mark#(X)
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(from(X)) -> cons#(X,from(s(X))) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(from(X)) -> from#(s(X)) -> from#(active(X)) -> from#(X)
    active#(from(X)) -> from#(s(X)) -> from#(mark(X)) -> from#(X)
    active#(from(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    active#(from(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
   SCC Processor:
    #sccs: 6
    #rules: 26
    #arcs: 215/1225
    DPs:
     mark#(length1(X)) -> active#(length1(X))
     active#(from(X)) -> mark#(cons(X,from(s(X))))
     mark#(from(X)) -> mark#(X)
     mark#(from(X)) -> active#(from(mark(X)))
     active#(length(nil())) -> mark#(0())
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
     mark#(s(X)) -> mark#(X)
     mark#(s(X)) -> active#(s(mark(X)))
     active#(length1(X)) -> mark#(length(X))
     mark#(length(X)) -> active#(length(X))
     mark#(nil()) -> active#(nil())
     mark#(0()) -> active#(0())
    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)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [mark#](x0) = 1,
      
      [active#](x0) = x0,
      
      [length1](x0) = 1,
      
      [0] = 1,
      
      [length](x0) = 1,
      
      [nil] = 0,
      
      [mark](x0) = 0,
      
      [cons](x0, x1) = 1,
      
      [s](x0) = 1,
      
      [active](x0) = 0,
      
      [from](x0) = 1
     orientation:
      mark#(length1(X)) = 1 >= 1 = active#(length1(X))
      
      active#(from(X)) = 1 >= 1 = mark#(cons(X,from(s(X))))
      
      mark#(from(X)) = 1 >= 1 = mark#(X)
      
      mark#(from(X)) = 1 >= 1 = active#(from(mark(X)))
      
      active#(length(nil())) = 1 >= 1 = mark#(0())
      
      mark#(cons(X1,X2)) = 1 >= 1 = mark#(X1)
      
      mark#(cons(X1,X2)) = 1 >= 1 = active#(cons(mark(X1),X2))
      
      active#(length(cons(X,Y))) = 1 >= 1 = mark#(s(length1(Y)))
      
      mark#(s(X)) = 1 >= 1 = mark#(X)
      
      mark#(s(X)) = 1 >= 1 = active#(s(mark(X)))
      
      active#(length1(X)) = 1 >= 1 = mark#(length(X))
      
      mark#(length(X)) = 1 >= 1 = active#(length(X))
      
      mark#(nil()) = 1 >= 0 = active#(nil())
      
      mark#(0()) = 1 >= 1 = active#(0())
      
      active(from(X)) = 0 >= 0 = mark(cons(X,from(s(X))))
      
      active(length(nil())) = 0 >= 0 = mark(0())
      
      active(length(cons(X,Y))) = 0 >= 0 = mark(s(length1(Y)))
      
      active(length1(X)) = 0 >= 0 = mark(length(X))
      
      mark(from(X)) = 0 >= 0 = active(from(mark(X)))
      
      mark(cons(X1,X2)) = 0 >= 0 = active(cons(mark(X1),X2))
      
      mark(s(X)) = 0 >= 0 = active(s(mark(X)))
      
      mark(length(X)) = 0 >= 0 = active(length(X))
      
      mark(nil()) = 0 >= 0 = active(nil())
      
      mark(0()) = 0 >= 0 = active(0())
      
      mark(length1(X)) = 0 >= 0 = active(length1(X))
      
      from(mark(X)) = 1 >= 1 = from(X)
      
      from(active(X)) = 1 >= 1 = from(X)
      
      cons(mark(X1),X2) = 1 >= 1 = cons(X1,X2)
      
      cons(X1,mark(X2)) = 1 >= 1 = cons(X1,X2)
      
      cons(active(X1),X2) = 1 >= 1 = cons(X1,X2)
      
      cons(X1,active(X2)) = 1 >= 1 = cons(X1,X2)
      
      s(mark(X)) = 1 >= 1 = s(X)
      
      s(active(X)) = 1 >= 1 = s(X)
      
      length(mark(X)) = 1 >= 1 = length(X)
      
      length(active(X)) = 1 >= 1 = length(X)
      
      length1(mark(X)) = 1 >= 1 = length1(X)
      
      length1(active(X)) = 1 >= 1 = length1(X)
     problem:
      DPs:
       mark#(length1(X)) -> active#(length1(X))
       active#(from(X)) -> mark#(cons(X,from(s(X))))
       mark#(from(X)) -> mark#(X)
       mark#(from(X)) -> active#(from(mark(X)))
       active#(length(nil())) -> mark#(0())
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
       mark#(s(X)) -> mark#(X)
       mark#(s(X)) -> active#(s(mark(X)))
       active#(length1(X)) -> mark#(length(X))
       mark#(length(X)) -> active#(length(X))
       mark#(0()) -> active#(0())
      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)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [mark#](x0) = 1,
       
       [active#](x0) = x0,
       
       [length1](x0) = 1,
       
       [0] = 1,
       
       [length](x0) = 1,
       
       [nil] = 0,
       
       [mark](x0) = 0,
       
       [cons](x0, x1) = 1,
       
       [s](x0) = 0,
       
       [active](x0) = 0,
       
       [from](x0) = 1
      orientation:
       mark#(length1(X)) = 1 >= 1 = active#(length1(X))
       
       active#(from(X)) = 1 >= 1 = mark#(cons(X,from(s(X))))
       
       mark#(from(X)) = 1 >= 1 = mark#(X)
       
       mark#(from(X)) = 1 >= 1 = active#(from(mark(X)))
       
       active#(length(nil())) = 1 >= 1 = mark#(0())
       
       mark#(cons(X1,X2)) = 1 >= 1 = mark#(X1)
       
       mark#(cons(X1,X2)) = 1 >= 1 = active#(cons(mark(X1),X2))
       
       active#(length(cons(X,Y))) = 1 >= 1 = mark#(s(length1(Y)))
       
       mark#(s(X)) = 1 >= 1 = mark#(X)
       
       mark#(s(X)) = 1 >= 0 = active#(s(mark(X)))
       
       active#(length1(X)) = 1 >= 1 = mark#(length(X))
       
       mark#(length(X)) = 1 >= 1 = active#(length(X))
       
       mark#(0()) = 1 >= 1 = active#(0())
       
       active(from(X)) = 0 >= 0 = mark(cons(X,from(s(X))))
       
       active(length(nil())) = 0 >= 0 = mark(0())
       
       active(length(cons(X,Y))) = 0 >= 0 = mark(s(length1(Y)))
       
       active(length1(X)) = 0 >= 0 = mark(length(X))
       
       mark(from(X)) = 0 >= 0 = active(from(mark(X)))
       
       mark(cons(X1,X2)) = 0 >= 0 = active(cons(mark(X1),X2))
       
       mark(s(X)) = 0 >= 0 = active(s(mark(X)))
       
       mark(length(X)) = 0 >= 0 = active(length(X))
       
       mark(nil()) = 0 >= 0 = active(nil())
       
       mark(0()) = 0 >= 0 = active(0())
       
       mark(length1(X)) = 0 >= 0 = active(length1(X))
       
       from(mark(X)) = 1 >= 1 = from(X)
       
       from(active(X)) = 1 >= 1 = from(X)
       
       cons(mark(X1),X2) = 1 >= 1 = cons(X1,X2)
       
       cons(X1,mark(X2)) = 1 >= 1 = cons(X1,X2)
       
       cons(active(X1),X2) = 1 >= 1 = cons(X1,X2)
       
       cons(X1,active(X2)) = 1 >= 1 = cons(X1,X2)
       
       s(mark(X)) = 0 >= 0 = s(X)
       
       s(active(X)) = 0 >= 0 = s(X)
       
       length(mark(X)) = 1 >= 1 = length(X)
       
       length(active(X)) = 1 >= 1 = length(X)
       
       length1(mark(X)) = 1 >= 1 = length1(X)
       
       length1(active(X)) = 1 >= 1 = length1(X)
      problem:
       DPs:
        mark#(length1(X)) -> active#(length1(X))
        active#(from(X)) -> mark#(cons(X,from(s(X))))
        mark#(from(X)) -> mark#(X)
        mark#(from(X)) -> active#(from(mark(X)))
        active#(length(nil())) -> mark#(0())
        mark#(cons(X1,X2)) -> mark#(X1)
        mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
        active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
        mark#(s(X)) -> mark#(X)
        active#(length1(X)) -> mark#(length(X))
        mark#(length(X)) -> active#(length(X))
        mark#(0()) -> active#(0())
       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)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [mark#](x0) = x0,
        
        [active#](x0) = x0,
        
        [length1](x0) = 0,
        
        [0] = 0,
        
        [length](x0) = 0,
        
        [nil] = 0,
        
        [mark](x0) = x0,
        
        [cons](x0, x1) = x0 + 1,
        
        [s](x0) = x0,
        
        [active](x0) = x0,
        
        [from](x0) = x0 + 1
       orientation:
        mark#(length1(X)) = 0 >= 0 = active#(length1(X))
        
        active#(from(X)) = X + 1 >= X + 1 = mark#(cons(X,from(s(X))))
        
        mark#(from(X)) = X + 1 >= X = mark#(X)
        
        mark#(from(X)) = X + 1 >= X + 1 = active#(from(mark(X)))
        
        active#(length(nil())) = 0 >= 0 = mark#(0())
        
        mark#(cons(X1,X2)) = X1 + 1 >= X1 = mark#(X1)
        
        mark#(cons(X1,X2)) = X1 + 1 >= X1 + 1 = active#(cons(mark(X1),X2))
        
        active#(length(cons(X,Y))) = 0 >= 0 = mark#(s(length1(Y)))
        
        mark#(s(X)) = X >= X = mark#(X)
        
        active#(length1(X)) = 0 >= 0 = mark#(length(X))
        
        mark#(length(X)) = 0 >= 0 = active#(length(X))
        
        mark#(0()) = 0 >= 0 = active#(0())
        
        active(from(X)) = X + 1 >= X + 1 = mark(cons(X,from(s(X))))
        
        active(length(nil())) = 0 >= 0 = mark(0())
        
        active(length(cons(X,Y))) = 0 >= 0 = mark(s(length1(Y)))
        
        active(length1(X)) = 0 >= 0 = mark(length(X))
        
        mark(from(X)) = X + 1 >= X + 1 = active(from(mark(X)))
        
        mark(cons(X1,X2)) = X1 + 1 >= X1 + 1 = active(cons(mark(X1),X2))
        
        mark(s(X)) = X >= X = active(s(mark(X)))
        
        mark(length(X)) = 0 >= 0 = active(length(X))
        
        mark(nil()) = 0 >= 0 = active(nil())
        
        mark(0()) = 0 >= 0 = active(0())
        
        mark(length1(X)) = 0 >= 0 = active(length1(X))
        
        from(mark(X)) = X + 1 >= X + 1 = from(X)
        
        from(active(X)) = X + 1 >= X + 1 = from(X)
        
        cons(mark(X1),X2) = X1 + 1 >= X1 + 1 = cons(X1,X2)
        
        cons(X1,mark(X2)) = X1 + 1 >= X1 + 1 = cons(X1,X2)
        
        cons(active(X1),X2) = X1 + 1 >= X1 + 1 = cons(X1,X2)
        
        cons(X1,active(X2)) = X1 + 1 >= X1 + 1 = cons(X1,X2)
        
        s(mark(X)) = X >= X = s(X)
        
        s(active(X)) = X >= X = s(X)
        
        length(mark(X)) = 0 >= 0 = length(X)
        
        length(active(X)) = 0 >= 0 = length(X)
        
        length1(mark(X)) = 0 >= 0 = length1(X)
        
        length1(active(X)) = 0 >= 0 = length1(X)
       problem:
        DPs:
         mark#(length1(X)) -> active#(length1(X))
         active#(from(X)) -> mark#(cons(X,from(s(X))))
         mark#(from(X)) -> active#(from(mark(X)))
         active#(length(nil())) -> mark#(0())
         mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
         active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
         mark#(s(X)) -> mark#(X)
         active#(length1(X)) -> mark#(length(X))
         mark#(length(X)) -> active#(length(X))
         mark#(0()) -> active#(0())
        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)
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [mark#](x0) = 1,
         
         [active#](x0) = x0,
         
         [length1](x0) = 1,
         
         [0] = 0,
         
         [length](x0) = 1,
         
         [nil] = 0,
         
         [mark](x0) = x0,
         
         [cons](x0, x1) = 0,
         
         [s](x0) = 0,
         
         [active](x0) = x0,
         
         [from](x0) = 1
        orientation:
         mark#(length1(X)) = 1 >= 1 = active#(length1(X))
         
         active#(from(X)) = 1 >= 1 = mark#(cons(X,from(s(X))))
         
         mark#(from(X)) = 1 >= 1 = active#(from(mark(X)))
         
         active#(length(nil())) = 1 >= 1 = mark#(0())
         
         mark#(cons(X1,X2)) = 1 >= 0 = active#(cons(mark(X1),X2))
         
         active#(length(cons(X,Y))) = 1 >= 1 = mark#(s(length1(Y)))
         
         mark#(s(X)) = 1 >= 1 = mark#(X)
         
         active#(length1(X)) = 1 >= 1 = mark#(length(X))
         
         mark#(length(X)) = 1 >= 1 = active#(length(X))
         
         mark#(0()) = 1 >= 0 = active#(0())
         
         active(from(X)) = 1 >= 0 = mark(cons(X,from(s(X))))
         
         active(length(nil())) = 1 >= 0 = mark(0())
         
         active(length(cons(X,Y))) = 1 >= 0 = mark(s(length1(Y)))
         
         active(length1(X)) = 1 >= 1 = mark(length(X))
         
         mark(from(X)) = 1 >= 1 = active(from(mark(X)))
         
         mark(cons(X1,X2)) = 0 >= 0 = active(cons(mark(X1),X2))
         
         mark(s(X)) = 0 >= 0 = active(s(mark(X)))
         
         mark(length(X)) = 1 >= 1 = active(length(X))
         
         mark(nil()) = 0 >= 0 = active(nil())
         
         mark(0()) = 0 >= 0 = active(0())
         
         mark(length1(X)) = 1 >= 1 = active(length1(X))
         
         from(mark(X)) = 1 >= 1 = from(X)
         
         from(active(X)) = 1 >= 1 = from(X)
         
         cons(mark(X1),X2) = 0 >= 0 = cons(X1,X2)
         
         cons(X1,mark(X2)) = 0 >= 0 = cons(X1,X2)
         
         cons(active(X1),X2) = 0 >= 0 = cons(X1,X2)
         
         cons(X1,active(X2)) = 0 >= 0 = cons(X1,X2)
         
         s(mark(X)) = 0 >= 0 = s(X)
         
         s(active(X)) = 0 >= 0 = s(X)
         
         length(mark(X)) = 1 >= 1 = length(X)
         
         length(active(X)) = 1 >= 1 = length(X)
         
         length1(mark(X)) = 1 >= 1 = length1(X)
         
         length1(active(X)) = 1 >= 1 = length1(X)
        problem:
         DPs:
          mark#(length1(X)) -> active#(length1(X))
          active#(from(X)) -> mark#(cons(X,from(s(X))))
          mark#(from(X)) -> active#(from(mark(X)))
          active#(length(nil())) -> mark#(0())
          active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
          mark#(s(X)) -> mark#(X)
          active#(length1(X)) -> mark#(length(X))
          mark#(length(X)) -> active#(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)
        Matrix Interpretation Processor:
         dimension: 1
         interpretation:
          [mark#](x0) = x0,
          
          [active#](x0) = 0,
          
          [length1](x0) = 0,
          
          [0] = 0,
          
          [length](x0) = 0,
          
          [nil] = 0,
          
          [mark](x0) = x0,
          
          [cons](x0, x1) = 0,
          
          [s](x0) = x0,
          
          [active](x0) = x0,
          
          [from](x0) = 1
         orientation:
          mark#(length1(X)) = 0 >= 0 = active#(length1(X))
          
          active#(from(X)) = 0 >= 0 = mark#(cons(X,from(s(X))))
          
          mark#(from(X)) = 1 >= 0 = active#(from(mark(X)))
          
          active#(length(nil())) = 0 >= 0 = mark#(0())
          
          active#(length(cons(X,Y))) = 0 >= 0 = mark#(s(length1(Y)))
          
          mark#(s(X)) = X >= X = mark#(X)
          
          active#(length1(X)) = 0 >= 0 = mark#(length(X))
          
          mark#(length(X)) = 0 >= 0 = active#(length(X))
          
          active(from(X)) = 1 >= 0 = mark(cons(X,from(s(X))))
          
          active(length(nil())) = 0 >= 0 = mark(0())
          
          active(length(cons(X,Y))) = 0 >= 0 = mark(s(length1(Y)))
          
          active(length1(X)) = 0 >= 0 = mark(length(X))
          
          mark(from(X)) = 1 >= 1 = active(from(mark(X)))
          
          mark(cons(X1,X2)) = 0 >= 0 = active(cons(mark(X1),X2))
          
          mark(s(X)) = X >= X = active(s(mark(X)))
          
          mark(length(X)) = 0 >= 0 = active(length(X))
          
          mark(nil()) = 0 >= 0 = active(nil())
          
          mark(0()) = 0 >= 0 = active(0())
          
          mark(length1(X)) = 0 >= 0 = active(length1(X))
          
          from(mark(X)) = 1 >= 1 = from(X)
          
          from(active(X)) = 1 >= 1 = from(X)
          
          cons(mark(X1),X2) = 0 >= 0 = cons(X1,X2)
          
          cons(X1,mark(X2)) = 0 >= 0 = cons(X1,X2)
          
          cons(active(X1),X2) = 0 >= 0 = cons(X1,X2)
          
          cons(X1,active(X2)) = 0 >= 0 = cons(X1,X2)
          
          s(mark(X)) = X >= X = s(X)
          
          s(active(X)) = X >= X = s(X)
          
          length(mark(X)) = 0 >= 0 = length(X)
          
          length(active(X)) = 0 >= 0 = length(X)
          
          length1(mark(X)) = 0 >= 0 = length1(X)
          
          length1(active(X)) = 0 >= 0 = length1(X)
         problem:
          DPs:
           mark#(length1(X)) -> active#(length1(X))
           active#(from(X)) -> mark#(cons(X,from(s(X))))
           active#(length(nil())) -> mark#(0())
           active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
           mark#(s(X)) -> mark#(X)
           active#(length1(X)) -> mark#(length(X))
           mark#(length(X)) -> active#(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)
         Matrix Interpretation Processor:
          dimension: 1
          interpretation:
           [mark#](x0) = 0,
           
           [active#](x0) = x0,
           
           [length1](x0) = 0,
           
           [0] = 0,
           
           [length](x0) = 0,
           
           [nil] = 0,
           
           [mark](x0) = 0,
           
           [cons](x0, x1) = 0,
           
           [s](x0) = 0,
           
           [active](x0) = 0,
           
           [from](x0) = 1
          orientation:
           mark#(length1(X)) = 0 >= 0 = active#(length1(X))
           
           active#(from(X)) = 1 >= 0 = mark#(cons(X,from(s(X))))
           
           active#(length(nil())) = 0 >= 0 = mark#(0())
           
           active#(length(cons(X,Y))) = 0 >= 0 = mark#(s(length1(Y)))
           
           mark#(s(X)) = 0 >= 0 = mark#(X)
           
           active#(length1(X)) = 0 >= 0 = mark#(length(X))
           
           mark#(length(X)) = 0 >= 0 = active#(length(X))
           
           active(from(X)) = 0 >= 0 = mark(cons(X,from(s(X))))
           
           active(length(nil())) = 0 >= 0 = mark(0())
           
           active(length(cons(X,Y))) = 0 >= 0 = mark(s(length1(Y)))
           
           active(length1(X)) = 0 >= 0 = mark(length(X))
           
           mark(from(X)) = 0 >= 0 = active(from(mark(X)))
           
           mark(cons(X1,X2)) = 0 >= 0 = active(cons(mark(X1),X2))
           
           mark(s(X)) = 0 >= 0 = active(s(mark(X)))
           
           mark(length(X)) = 0 >= 0 = active(length(X))
           
           mark(nil()) = 0 >= 0 = active(nil())
           
           mark(0()) = 0 >= 0 = active(0())
           
           mark(length1(X)) = 0 >= 0 = active(length1(X))
           
           from(mark(X)) = 1 >= 1 = from(X)
           
           from(active(X)) = 1 >= 1 = from(X)
           
           cons(mark(X1),X2) = 0 >= 0 = cons(X1,X2)
           
           cons(X1,mark(X2)) = 0 >= 0 = cons(X1,X2)
           
           cons(active(X1),X2) = 0 >= 0 = cons(X1,X2)
           
           cons(X1,active(X2)) = 0 >= 0 = cons(X1,X2)
           
           s(mark(X)) = 0 >= 0 = s(X)
           
           s(active(X)) = 0 >= 0 = s(X)
           
           length(mark(X)) = 0 >= 0 = length(X)
           
           length(active(X)) = 0 >= 0 = length(X)
           
           length1(mark(X)) = 0 >= 0 = length1(X)
           
           length1(active(X)) = 0 >= 0 = length1(X)
          problem:
           DPs:
            mark#(length1(X)) -> active#(length1(X))
            active#(length(nil())) -> mark#(0())
            active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
            mark#(s(X)) -> mark#(X)
            active#(length1(X)) -> mark#(length(X))
            mark#(length(X)) -> active#(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)
          Matrix Interpretation Processor:
           dimension: 1
           interpretation:
            [mark#](x0) = x0,
            
            [active#](x0) = x0,
            
            [length1](x0) = 1,
            
            [0] = 0,
            
            [length](x0) = 1,
            
            [nil] = 0,
            
            [mark](x0) = x0,
            
            [cons](x0, x1) = 0,
            
            [s](x0) = x0,
            
            [active](x0) = x0,
            
            [from](x0) = x0
           orientation:
            mark#(length1(X)) = 1 >= 1 = active#(length1(X))
            
            active#(length(nil())) = 1 >= 0 = mark#(0())
            
            active#(length(cons(X,Y))) = 1 >= 1 = mark#(s(length1(Y)))
            
            mark#(s(X)) = X >= X = mark#(X)
            
            active#(length1(X)) = 1 >= 1 = mark#(length(X))
            
            mark#(length(X)) = 1 >= 1 = active#(length(X))
            
            active(from(X)) = X >= 0 = mark(cons(X,from(s(X))))
            
            active(length(nil())) = 1 >= 0 = mark(0())
            
            active(length(cons(X,Y))) = 1 >= 1 = mark(s(length1(Y)))
            
            active(length1(X)) = 1 >= 1 = mark(length(X))
            
            mark(from(X)) = X >= X = active(from(mark(X)))
            
            mark(cons(X1,X2)) = 0 >= 0 = active(cons(mark(X1),X2))
            
            mark(s(X)) = X >= X = active(s(mark(X)))
            
            mark(length(X)) = 1 >= 1 = active(length(X))
            
            mark(nil()) = 0 >= 0 = active(nil())
            
            mark(0()) = 0 >= 0 = active(0())
            
            mark(length1(X)) = 1 >= 1 = active(length1(X))
            
            from(mark(X)) = X >= X = from(X)
            
            from(active(X)) = X >= X = from(X)
            
            cons(mark(X1),X2) = 0 >= 0 = cons(X1,X2)
            
            cons(X1,mark(X2)) = 0 >= 0 = cons(X1,X2)
            
            cons(active(X1),X2) = 0 >= 0 = cons(X1,X2)
            
            cons(X1,active(X2)) = 0 >= 0 = cons(X1,X2)
            
            s(mark(X)) = X >= X = s(X)
            
            s(active(X)) = X >= X = s(X)
            
            length(mark(X)) = 1 >= 1 = length(X)
            
            length(active(X)) = 1 >= 1 = length(X)
            
            length1(mark(X)) = 1 >= 1 = length1(X)
            
            length1(active(X)) = 1 >= 1 = length1(X)
           problem:
            DPs:
             mark#(length1(X)) -> active#(length1(X))
             active#(length(cons(X,Y))) -> mark#(s(length1(Y)))
             mark#(s(X)) -> mark#(X)
             active#(length1(X)) -> mark#(length(X))
             mark#(length(X)) -> active#(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
    
    DPs:
     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)
    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)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [cons#](x0, x1) = x0 + x1 + 1,
      
      [length1](x0) = 0,
      
      [0] = 0,
      
      [length](x0) = 0,
      
      [nil] = 0,
      
      [mark](x0) = x0 + 1,
      
      [cons](x0, x1) = 0,
      
      [s](x0) = 0,
      
      [active](x0) = x0 + 1,
      
      [from](x0) = 0
     orientation:
      cons#(mark(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 1 = cons#(X1,X2)
      
      cons#(X1,mark(X2)) = X1 + X2 + 2 >= X1 + X2 + 1 = cons#(X1,X2)
      
      cons#(active(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 1 = cons#(X1,X2)
      
      cons#(X1,active(X2)) = X1 + X2 + 2 >= X1 + X2 + 1 = cons#(X1,X2)
      
      active(from(X)) = 1 >= 1 = mark(cons(X,from(s(X))))
      
      active(length(nil())) = 1 >= 1 = mark(0())
      
      active(length(cons(X,Y))) = 1 >= 1 = mark(s(length1(Y)))
      
      active(length1(X)) = 1 >= 1 = mark(length(X))
      
      mark(from(X)) = 1 >= 1 = active(from(mark(X)))
      
      mark(cons(X1,X2)) = 1 >= 1 = active(cons(mark(X1),X2))
      
      mark(s(X)) = 1 >= 1 = active(s(mark(X)))
      
      mark(length(X)) = 1 >= 1 = active(length(X))
      
      mark(nil()) = 1 >= 1 = active(nil())
      
      mark(0()) = 1 >= 1 = active(0())
      
      mark(length1(X)) = 1 >= 1 = active(length1(X))
      
      from(mark(X)) = 0 >= 0 = from(X)
      
      from(active(X)) = 0 >= 0 = from(X)
      
      cons(mark(X1),X2) = 0 >= 0 = cons(X1,X2)
      
      cons(X1,mark(X2)) = 0 >= 0 = cons(X1,X2)
      
      cons(active(X1),X2) = 0 >= 0 = cons(X1,X2)
      
      cons(X1,active(X2)) = 0 >= 0 = cons(X1,X2)
      
      s(mark(X)) = 0 >= 0 = s(X)
      
      s(active(X)) = 0 >= 0 = s(X)
      
      length(mark(X)) = 0 >= 0 = length(X)
      
      length(active(X)) = 0 >= 0 = length(X)
      
      length1(mark(X)) = 0 >= 0 = length1(X)
      
      length1(active(X)) = 0 >= 0 = length1(X)
     problem:
      DPs:
       
      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)
     Qed
    
    DPs:
     from#(mark(X)) -> from#(X)
     from#(active(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)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [from#](x0) = x0 + 1,
      
      [length1](x0) = 0,
      
      [0] = 0,
      
      [length](x0) = 0,
      
      [nil] = 0,
      
      [mark](x0) = x0 + 1,
      
      [cons](x0, x1) = 0,
      
      [s](x0) = 0,
      
      [active](x0) = x0 + 1,
      
      [from](x0) = 0
     orientation:
      from#(mark(X)) = X + 2 >= X + 1 = from#(X)
      
      from#(active(X)) = X + 2 >= X + 1 = from#(X)
      
      active(from(X)) = 1 >= 1 = mark(cons(X,from(s(X))))
      
      active(length(nil())) = 1 >= 1 = mark(0())
      
      active(length(cons(X,Y))) = 1 >= 1 = mark(s(length1(Y)))
      
      active(length1(X)) = 1 >= 1 = mark(length(X))
      
      mark(from(X)) = 1 >= 1 = active(from(mark(X)))
      
      mark(cons(X1,X2)) = 1 >= 1 = active(cons(mark(X1),X2))
      
      mark(s(X)) = 1 >= 1 = active(s(mark(X)))
      
      mark(length(X)) = 1 >= 1 = active(length(X))
      
      mark(nil()) = 1 >= 1 = active(nil())
      
      mark(0()) = 1 >= 1 = active(0())
      
      mark(length1(X)) = 1 >= 1 = active(length1(X))
      
      from(mark(X)) = 0 >= 0 = from(X)
      
      from(active(X)) = 0 >= 0 = from(X)
      
      cons(mark(X1),X2) = 0 >= 0 = cons(X1,X2)
      
      cons(X1,mark(X2)) = 0 >= 0 = cons(X1,X2)
      
      cons(active(X1),X2) = 0 >= 0 = cons(X1,X2)
      
      cons(X1,active(X2)) = 0 >= 0 = cons(X1,X2)
      
      s(mark(X)) = 0 >= 0 = s(X)
      
      s(active(X)) = 0 >= 0 = s(X)
      
      length(mark(X)) = 0 >= 0 = length(X)
      
      length(active(X)) = 0 >= 0 = length(X)
      
      length1(mark(X)) = 0 >= 0 = length1(X)
      
      length1(active(X)) = 0 >= 0 = length1(X)
     problem:
      DPs:
       
      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)
     Qed
    
    DPs:
     s#(mark(X)) -> s#(X)
     s#(active(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)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [s#](x0) = x0 + 1,
      
      [length1](x0) = 0,
      
      [0] = 0,
      
      [length](x0) = 0,
      
      [nil] = 0,
      
      [mark](x0) = x0 + 1,
      
      [cons](x0, x1) = 0,
      
      [s](x0) = 0,
      
      [active](x0) = x0 + 1,
      
      [from](x0) = 0
     orientation:
      s#(mark(X)) = X + 2 >= X + 1 = s#(X)
      
      s#(active(X)) = X + 2 >= X + 1 = s#(X)
      
      active(from(X)) = 1 >= 1 = mark(cons(X,from(s(X))))
      
      active(length(nil())) = 1 >= 1 = mark(0())
      
      active(length(cons(X,Y))) = 1 >= 1 = mark(s(length1(Y)))
      
      active(length1(X)) = 1 >= 1 = mark(length(X))
      
      mark(from(X)) = 1 >= 1 = active(from(mark(X)))
      
      mark(cons(X1,X2)) = 1 >= 1 = active(cons(mark(X1),X2))
      
      mark(s(X)) = 1 >= 1 = active(s(mark(X)))
      
      mark(length(X)) = 1 >= 1 = active(length(X))
      
      mark(nil()) = 1 >= 1 = active(nil())
      
      mark(0()) = 1 >= 1 = active(0())
      
      mark(length1(X)) = 1 >= 1 = active(length1(X))
      
      from(mark(X)) = 0 >= 0 = from(X)
      
      from(active(X)) = 0 >= 0 = from(X)
      
      cons(mark(X1),X2) = 0 >= 0 = cons(X1,X2)
      
      cons(X1,mark(X2)) = 0 >= 0 = cons(X1,X2)
      
      cons(active(X1),X2) = 0 >= 0 = cons(X1,X2)
      
      cons(X1,active(X2)) = 0 >= 0 = cons(X1,X2)
      
      s(mark(X)) = 0 >= 0 = s(X)
      
      s(active(X)) = 0 >= 0 = s(X)
      
      length(mark(X)) = 0 >= 0 = length(X)
      
      length(active(X)) = 0 >= 0 = length(X)
      
      length1(mark(X)) = 0 >= 0 = length1(X)
      
      length1(active(X)) = 0 >= 0 = length1(X)
     problem:
      DPs:
       
      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)
     Qed
    
    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)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [length1#](x0) = x0 + 1,
      
      [length1](x0) = 0,
      
      [0] = 0,
      
      [length](x0) = 0,
      
      [nil] = 0,
      
      [mark](x0) = x0 + 1,
      
      [cons](x0, x1) = 0,
      
      [s](x0) = 0,
      
      [active](x0) = x0 + 1,
      
      [from](x0) = 0
     orientation:
      length1#(mark(X)) = X + 2 >= X + 1 = length1#(X)
      
      length1#(active(X)) = X + 2 >= X + 1 = length1#(X)
      
      active(from(X)) = 1 >= 1 = mark(cons(X,from(s(X))))
      
      active(length(nil())) = 1 >= 1 = mark(0())
      
      active(length(cons(X,Y))) = 1 >= 1 = mark(s(length1(Y)))
      
      active(length1(X)) = 1 >= 1 = mark(length(X))
      
      mark(from(X)) = 1 >= 1 = active(from(mark(X)))
      
      mark(cons(X1,X2)) = 1 >= 1 = active(cons(mark(X1),X2))
      
      mark(s(X)) = 1 >= 1 = active(s(mark(X)))
      
      mark(length(X)) = 1 >= 1 = active(length(X))
      
      mark(nil()) = 1 >= 1 = active(nil())
      
      mark(0()) = 1 >= 1 = active(0())
      
      mark(length1(X)) = 1 >= 1 = active(length1(X))
      
      from(mark(X)) = 0 >= 0 = from(X)
      
      from(active(X)) = 0 >= 0 = from(X)
      
      cons(mark(X1),X2) = 0 >= 0 = cons(X1,X2)
      
      cons(X1,mark(X2)) = 0 >= 0 = cons(X1,X2)
      
      cons(active(X1),X2) = 0 >= 0 = cons(X1,X2)
      
      cons(X1,active(X2)) = 0 >= 0 = cons(X1,X2)
      
      s(mark(X)) = 0 >= 0 = s(X)
      
      s(active(X)) = 0 >= 0 = s(X)
      
      length(mark(X)) = 0 >= 0 = length(X)
      
      length(active(X)) = 0 >= 0 = length(X)
      
      length1(mark(X)) = 0 >= 0 = length1(X)
      
      length1(active(X)) = 0 >= 0 = length1(X)
     problem:
      DPs:
       
      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)
     Qed
    
    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)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [length#](x0) = x0 + 1,
      
      [length1](x0) = 0,
      
      [0] = 0,
      
      [length](x0) = 0,
      
      [nil] = 0,
      
      [mark](x0) = x0 + 1,
      
      [cons](x0, x1) = 0,
      
      [s](x0) = 0,
      
      [active](x0) = x0 + 1,
      
      [from](x0) = 0
     orientation:
      length#(mark(X)) = X + 2 >= X + 1 = length#(X)
      
      length#(active(X)) = X + 2 >= X + 1 = length#(X)
      
      active(from(X)) = 1 >= 1 = mark(cons(X,from(s(X))))
      
      active(length(nil())) = 1 >= 1 = mark(0())
      
      active(length(cons(X,Y))) = 1 >= 1 = mark(s(length1(Y)))
      
      active(length1(X)) = 1 >= 1 = mark(length(X))
      
      mark(from(X)) = 1 >= 1 = active(from(mark(X)))
      
      mark(cons(X1,X2)) = 1 >= 1 = active(cons(mark(X1),X2))
      
      mark(s(X)) = 1 >= 1 = active(s(mark(X)))
      
      mark(length(X)) = 1 >= 1 = active(length(X))
      
      mark(nil()) = 1 >= 1 = active(nil())
      
      mark(0()) = 1 >= 1 = active(0())
      
      mark(length1(X)) = 1 >= 1 = active(length1(X))
      
      from(mark(X)) = 0 >= 0 = from(X)
      
      from(active(X)) = 0 >= 0 = from(X)
      
      cons(mark(X1),X2) = 0 >= 0 = cons(X1,X2)
      
      cons(X1,mark(X2)) = 0 >= 0 = cons(X1,X2)
      
      cons(active(X1),X2) = 0 >= 0 = cons(X1,X2)
      
      cons(X1,active(X2)) = 0 >= 0 = cons(X1,X2)
      
      s(mark(X)) = 0 >= 0 = s(X)
      
      s(active(X)) = 0 >= 0 = s(X)
      
      length(mark(X)) = 0 >= 0 = length(X)
      
      length(active(X)) = 0 >= 0 = length(X)
      
      length1(mark(X)) = 0 >= 0 = length1(X)
      
      length1(active(X)) = 0 >= 0 = length1(X)
     problem:
      DPs:
       
      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)
     Qed