YES

Problem:
 active(fst(0(),Z)) -> mark(nil())
 active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
 active(from(X)) -> mark(cons(X,from(s(X))))
 active(add(0(),X)) -> mark(X)
 active(add(s(X),Y)) -> mark(s(add(X,Y)))
 active(len(nil())) -> mark(0())
 active(len(cons(X,Z))) -> mark(s(len(Z)))
 mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
 mark(0()) -> active(0())
 mark(nil()) -> active(nil())
 mark(s(X)) -> active(s(X))
 mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
 mark(from(X)) -> active(from(mark(X)))
 mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
 mark(len(X)) -> active(len(mark(X)))
 fst(mark(X1),X2) -> fst(X1,X2)
 fst(X1,mark(X2)) -> fst(X1,X2)
 fst(active(X1),X2) -> fst(X1,X2)
 fst(X1,active(X2)) -> fst(X1,X2)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(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)
 from(mark(X)) -> from(X)
 from(active(X)) -> from(X)
 add(mark(X1),X2) -> add(X1,X2)
 add(X1,mark(X2)) -> add(X1,X2)
 add(active(X1),X2) -> add(X1,X2)
 add(X1,active(X2)) -> add(X1,X2)
 len(mark(X)) -> len(X)
 len(active(X)) -> len(X)

Proof:
 DP Processor:
  DPs:
   active#(fst(0(),Z)) -> mark#(nil())
   active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z)
   active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z))
   active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
   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#(add(0(),X)) -> mark#(X)
   active#(add(s(X),Y)) -> add#(X,Y)
   active#(add(s(X),Y)) -> s#(add(X,Y))
   active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
   active#(len(nil())) -> mark#(0())
   active#(len(cons(X,Z))) -> len#(Z)
   active#(len(cons(X,Z))) -> s#(len(Z))
   active#(len(cons(X,Z))) -> mark#(s(len(Z)))
   mark#(fst(X1,X2)) -> mark#(X2)
   mark#(fst(X1,X2)) -> mark#(X1)
   mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
   mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
   mark#(0()) -> active#(0())
   mark#(nil()) -> active#(nil())
   mark#(s(X)) -> active#(s(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#(from(X)) -> mark#(X)
   mark#(from(X)) -> from#(mark(X))
   mark#(from(X)) -> active#(from(mark(X)))
   mark#(add(X1,X2)) -> mark#(X2)
   mark#(add(X1,X2)) -> mark#(X1)
   mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
   mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
   mark#(len(X)) -> mark#(X)
   mark#(len(X)) -> len#(mark(X))
   mark#(len(X)) -> active#(len(mark(X)))
   fst#(mark(X1),X2) -> fst#(X1,X2)
   fst#(X1,mark(X2)) -> fst#(X1,X2)
   fst#(active(X1),X2) -> fst#(X1,X2)
   fst#(X1,active(X2)) -> fst#(X1,X2)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(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)
   from#(mark(X)) -> from#(X)
   from#(active(X)) -> from#(X)
   add#(mark(X1),X2) -> add#(X1,X2)
   add#(X1,mark(X2)) -> add#(X1,X2)
   add#(active(X1),X2) -> add#(X1,X2)
   add#(X1,active(X2)) -> add#(X1,X2)
   len#(mark(X)) -> len#(X)
   len#(active(X)) -> len#(X)
  TRS:
   active(fst(0(),Z)) -> mark(nil())
   active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
   active(from(X)) -> mark(cons(X,from(s(X))))
   active(add(0(),X)) -> mark(X)
   active(add(s(X),Y)) -> mark(s(add(X,Y)))
   active(len(nil())) -> mark(0())
   active(len(cons(X,Z))) -> mark(s(len(Z)))
   mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
   mark(0()) -> active(0())
   mark(nil()) -> active(nil())
   mark(s(X)) -> active(s(X))
   mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
   mark(from(X)) -> active(from(mark(X)))
   mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
   mark(len(X)) -> active(len(mark(X)))
   fst(mark(X1),X2) -> fst(X1,X2)
   fst(X1,mark(X2)) -> fst(X1,X2)
   fst(active(X1),X2) -> fst(X1,X2)
   fst(X1,active(X2)) -> fst(X1,X2)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(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)
   from(mark(X)) -> from(X)
   from(active(X)) -> from(X)
   add(mark(X1),X2) -> add(X1,X2)
   add(X1,mark(X2)) -> add(X1,X2)
   add(active(X1),X2) -> add(X1,X2)
   add(X1,active(X2)) -> add(X1,X2)
   len(mark(X)) -> len(X)
   len(active(X)) -> len(X)
  TDG Processor:
   DPs:
    active#(fst(0(),Z)) -> mark#(nil())
    active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z)
    active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z))
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
    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#(add(0(),X)) -> mark#(X)
    active#(add(s(X),Y)) -> add#(X,Y)
    active#(add(s(X),Y)) -> s#(add(X,Y))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    active#(len(nil())) -> mark#(0())
    active#(len(cons(X,Z))) -> len#(Z)
    active#(len(cons(X,Z))) -> s#(len(Z))
    active#(len(cons(X,Z))) -> mark#(s(len(Z)))
    mark#(fst(X1,X2)) -> mark#(X2)
    mark#(fst(X1,X2)) -> mark#(X1)
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    mark#(0()) -> active#(0())
    mark#(nil()) -> active#(nil())
    mark#(s(X)) -> active#(s(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#(from(X)) -> mark#(X)
    mark#(from(X)) -> from#(mark(X))
    mark#(from(X)) -> active#(from(mark(X)))
    mark#(add(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(len(X)) -> mark#(X)
    mark#(len(X)) -> len#(mark(X))
    mark#(len(X)) -> active#(len(mark(X)))
    fst#(mark(X1),X2) -> fst#(X1,X2)
    fst#(X1,mark(X2)) -> fst#(X1,X2)
    fst#(active(X1),X2) -> fst#(X1,X2)
    fst#(X1,active(X2)) -> fst#(X1,X2)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(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)
    from#(mark(X)) -> from#(X)
    from#(active(X)) -> from#(X)
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2)
    len#(mark(X)) -> len#(X)
    len#(active(X)) -> len#(X)
   TRS:
    active(fst(0(),Z)) -> mark(nil())
    active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
    active(from(X)) -> mark(cons(X,from(s(X))))
    active(add(0(),X)) -> mark(X)
    active(add(s(X),Y)) -> mark(s(add(X,Y)))
    active(len(nil())) -> mark(0())
    active(len(cons(X,Z))) -> mark(s(len(Z)))
    mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
    mark(0()) -> active(0())
    mark(nil()) -> active(nil())
    mark(s(X)) -> active(s(X))
    mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
    mark(from(X)) -> active(from(mark(X)))
    mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
    mark(len(X)) -> active(len(mark(X)))
    fst(mark(X1),X2) -> fst(X1,X2)
    fst(X1,mark(X2)) -> fst(X1,X2)
    fst(active(X1),X2) -> fst(X1,X2)
    fst(X1,active(X2)) -> fst(X1,X2)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(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)
    from(mark(X)) -> from(X)
    from(active(X)) -> from(X)
    add(mark(X1),X2) -> add(X1,X2)
    add(X1,mark(X2)) -> add(X1,X2)
    add(active(X1),X2) -> add(X1,X2)
    add(X1,active(X2)) -> add(X1,X2)
    len(mark(X)) -> len(X)
    len(active(X)) -> len(X)
   graph:
    len#(mark(X)) -> len#(X) -> len#(active(X)) -> len#(X)
    len#(mark(X)) -> len#(X) -> len#(mark(X)) -> len#(X)
    len#(active(X)) -> len#(X) -> len#(active(X)) -> len#(X)
    len#(active(X)) -> len#(X) -> len#(mark(X)) -> len#(X)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(active(X1),X2) -> add#(X1,X2)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(mark(X1),X2) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2) ->
    add#(active(X1),X2) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(active(X1),X2) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(active(X1),X2) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(X1,mark(X2)) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2) ->
    add#(active(X1),X2) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    add#(X1,active(X2)) -> add#(X1,X2) ->
    add#(mark(X1),X2) -> add#(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)
    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)
    fst#(mark(X1),X2) -> fst#(X1,X2) ->
    fst#(X1,active(X2)) -> fst#(X1,X2)
    fst#(mark(X1),X2) -> fst#(X1,X2) ->
    fst#(active(X1),X2) -> fst#(X1,X2)
    fst#(mark(X1),X2) -> fst#(X1,X2) ->
    fst#(X1,mark(X2)) -> fst#(X1,X2)
    fst#(mark(X1),X2) -> fst#(X1,X2) ->
    fst#(mark(X1),X2) -> fst#(X1,X2)
    fst#(active(X1),X2) -> fst#(X1,X2) ->
    fst#(X1,active(X2)) -> fst#(X1,X2)
    fst#(active(X1),X2) -> fst#(X1,X2) ->
    fst#(active(X1),X2) -> fst#(X1,X2)
    fst#(active(X1),X2) -> fst#(X1,X2) ->
    fst#(X1,mark(X2)) -> fst#(X1,X2)
    fst#(active(X1),X2) -> fst#(X1,X2) ->
    fst#(mark(X1),X2) -> fst#(X1,X2)
    fst#(X1,mark(X2)) -> fst#(X1,X2) ->
    fst#(X1,active(X2)) -> fst#(X1,X2)
    fst#(X1,mark(X2)) -> fst#(X1,X2) ->
    fst#(active(X1),X2) -> fst#(X1,X2)
    fst#(X1,mark(X2)) -> fst#(X1,X2) ->
    fst#(X1,mark(X2)) -> fst#(X1,X2)
    fst#(X1,mark(X2)) -> fst#(X1,X2) ->
    fst#(mark(X1),X2) -> fst#(X1,X2)
    fst#(X1,active(X2)) -> fst#(X1,X2) ->
    fst#(X1,active(X2)) -> fst#(X1,X2)
    fst#(X1,active(X2)) -> fst#(X1,X2) ->
    fst#(active(X1),X2) -> fst#(X1,X2)
    fst#(X1,active(X2)) -> fst#(X1,X2) ->
    fst#(X1,mark(X2)) -> fst#(X1,X2)
    fst#(X1,active(X2)) -> fst#(X1,X2) ->
    fst#(mark(X1),X2) -> fst#(X1,X2)
    mark#(len(X)) -> len#(mark(X)) -> len#(active(X)) -> len#(X)
    mark#(len(X)) -> len#(mark(X)) -> len#(mark(X)) -> len#(X)
    mark#(len(X)) -> mark#(X) -> mark#(len(X)) -> active#(len(mark(X)))
    mark#(len(X)) -> mark#(X) -> mark#(len(X)) -> len#(mark(X))
    mark#(len(X)) -> mark#(X) -> mark#(len(X)) -> mark#(X)
    mark#(len(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(len(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(len(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(len(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(len(X)) -> mark#(X) -> mark#(from(X)) -> active#(from(mark(X)))
    mark#(len(X)) -> mark#(X) -> mark#(from(X)) -> from#(mark(X))
    mark#(len(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
    mark#(len(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(len(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(len(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(len(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
    mark#(len(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
    mark#(len(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(len(X)) -> mark#(X) ->
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    mark#(len(X)) -> mark#(X) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    mark#(len(X)) -> mark#(X) -> mark#(fst(X1,X2)) -> mark#(X1)
    mark#(len(X)) -> mark#(X) ->
    mark#(fst(X1,X2)) -> mark#(X2)
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(len(cons(X,Z))) -> mark#(s(len(Z)))
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(len(cons(X,Z))) -> s#(len(Z))
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(len(cons(X,Z))) -> len#(Z)
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(len(nil())) -> mark#(0())
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(from(X)) -> from#(s(X))
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(from(X)) -> s#(X)
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z))
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z)
    mark#(len(X)) -> active#(len(mark(X))) ->
    active#(fst(0(),Z)) -> mark#(nil())
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2)) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2)) ->
    add#(active(X1),X2) -> add#(X1,X2)
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2)) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2)) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(len(X)) -> active#(len(mark(X)))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(len(X)) -> len#(mark(X))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(len(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(from(X)) -> active#(from(mark(X)))
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(from(X)) -> from#(mark(X))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(from(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> active#(s(X))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(nil()) -> active#(nil())
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    mark#(add(X1,X2)) -> mark#(X2) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(fst(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X2) -> mark#(fst(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(len(X)) -> active#(len(mark(X)))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(len(X)) -> len#(mark(X))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(len(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> active#(from(mark(X)))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> from#(mark(X))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(nil()) -> active#(nil())
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    mark#(add(X1,X2)) -> mark#(X1) -> mark#(fst(X1,X2)) -> mark#(X1)
    mark#(add(X1,X2)) -> mark#(X1) ->
    mark#(fst(X1,X2)) -> mark#(X2)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(len(cons(X,Z))) -> mark#(s(len(Z)))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(len(cons(X,Z))) -> s#(len(Z))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(len(cons(X,Z))) -> len#(Z)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(len(nil())) -> mark#(0())
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(from(X)) -> from#(s(X))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(from(X)) -> s#(X)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z))
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z)
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
    active#(fst(0(),Z)) -> mark#(nil())
    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)) -> mark#(X) -> mark#(len(X)) -> active#(len(mark(X)))
    mark#(from(X)) -> mark#(X) -> mark#(len(X)) -> len#(mark(X))
    mark#(from(X)) -> mark#(X) -> mark#(len(X)) -> mark#(X)
    mark#(from(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(from(X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(from(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(from(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
    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)) -> 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#(s(X)) -> active#(s(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#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    mark#(from(X)) -> mark#(X) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    mark#(from(X)) -> mark#(X) -> mark#(fst(X1,X2)) -> mark#(X1)
    mark#(from(X)) -> mark#(X) ->
    mark#(fst(X1,X2)) -> mark#(X2)
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(len(cons(X,Z))) -> mark#(s(len(Z)))
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(len(cons(X,Z))) -> s#(len(Z))
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(len(cons(X,Z))) -> len#(Z)
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(len(nil())) -> mark#(0())
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(add(0(),X)) -> mark#(X)
    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)
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z))
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z)
    mark#(from(X)) -> active#(from(mark(X))) ->
    active#(fst(0(),Z)) -> mark#(nil())
    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)) -> mark#(X1) ->
    mark#(len(X)) -> active#(len(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(len(X)) -> len#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(len(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> mark#(X2)
    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)) -> 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#(s(X)) -> active#(s(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#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(fst(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(fst(X1,X2)) -> mark#(X2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(len(cons(X,Z))) -> mark#(s(len(Z)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(len(cons(X,Z))) -> s#(len(Z))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(len(cons(X,Z))) -> len#(Z)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(len(nil())) -> mark#(0())
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(add(0(),X)) -> mark#(X)
    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#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(fst(0(),Z)) -> mark#(nil())
    mark#(s(X)) -> active#(s(X)) ->
    active#(len(cons(X,Z))) -> mark#(s(len(Z)))
    mark#(s(X)) -> active#(s(X)) ->
    active#(len(cons(X,Z))) -> s#(len(Z))
    mark#(s(X)) -> active#(s(X)) -> active#(len(cons(X,Z))) -> len#(Z)
    mark#(s(X)) -> active#(s(X)) -> active#(len(nil())) -> mark#(0())
    mark#(s(X)) -> active#(s(X)) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(s(X)) -> active#(s(X)) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(s(X)) -> active#(s(X)) -> active#(add(s(X),Y)) -> add#(X,Y)
    mark#(s(X)) -> active#(s(X)) -> active#(add(0(),X)) -> mark#(X)
    mark#(s(X)) -> active#(s(X)) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(s(X)) -> active#(s(X)) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(s(X)) -> active#(s(X)) -> active#(from(X)) -> from#(s(X))
    mark#(s(X)) -> active#(s(X)) -> active#(from(X)) -> s#(X)
    mark#(s(X)) -> active#(s(X)) ->
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
    mark#(s(X)) -> active#(s(X)) ->
    active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z))
    mark#(s(X)) -> active#(s(X)) ->
    active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z)
    mark#(s(X)) -> active#(s(X)) ->
    active#(fst(0(),Z)) -> mark#(nil())
    mark#(nil()) -> active#(nil()) ->
    active#(len(cons(X,Z))) -> mark#(s(len(Z)))
    mark#(nil()) -> active#(nil()) ->
    active#(len(cons(X,Z))) -> s#(len(Z))
    mark#(nil()) -> active#(nil()) ->
    active#(len(cons(X,Z))) -> len#(Z)
    mark#(nil()) -> active#(nil()) ->
    active#(len(nil())) -> mark#(0())
    mark#(nil()) -> active#(nil()) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(nil()) -> active#(nil()) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(nil()) -> active#(nil()) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(nil()) -> active#(nil()) -> active#(add(0(),X)) -> mark#(X)
    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#(nil()) -> active#(nil()) ->
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
    mark#(nil()) -> active#(nil()) ->
    active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z))
    mark#(nil()) -> active#(nil()) ->
    active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z)
    mark#(nil()) -> active#(nil()) ->
    active#(fst(0(),Z)) -> mark#(nil())
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2)) ->
    fst#(X1,active(X2)) -> fst#(X1,X2)
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2)) ->
    fst#(active(X1),X2) -> fst#(X1,X2)
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2)) ->
    fst#(X1,mark(X2)) -> fst#(X1,X2)
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2)) ->
    fst#(mark(X1),X2) -> fst#(X1,X2)
    mark#(fst(X1,X2)) -> mark#(X2) ->
    mark#(len(X)) -> active#(len(mark(X)))
    mark#(fst(X1,X2)) -> mark#(X2) -> mark#(len(X)) -> len#(mark(X))
    mark#(fst(X1,X2)) -> mark#(X2) -> mark#(len(X)) -> mark#(X)
    mark#(fst(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(fst(X1,X2)) -> mark#(X2) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(fst(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(fst(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(fst(X1,X2)) -> mark#(X2) ->
    mark#(from(X)) -> active#(from(mark(X)))
    mark#(fst(X1,X2)) -> mark#(X2) ->
    mark#(from(X)) -> from#(mark(X))
    mark#(fst(X1,X2)) -> mark#(X2) -> mark#(from(X)) -> mark#(X)
    mark#(fst(X1,X2)) -> mark#(X2) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(fst(X1,X2)) -> mark#(X2) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(fst(X1,X2)) -> mark#(X2) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(fst(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> active#(s(X))
    mark#(fst(X1,X2)) -> mark#(X2) -> mark#(nil()) -> active#(nil())
    mark#(fst(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
    mark#(fst(X1,X2)) -> mark#(X2) ->
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    mark#(fst(X1,X2)) -> mark#(X2) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    mark#(fst(X1,X2)) -> mark#(X2) -> mark#(fst(X1,X2)) -> mark#(X1)
    mark#(fst(X1,X2)) -> mark#(X2) -> mark#(fst(X1,X2)) -> mark#(X2)
    mark#(fst(X1,X2)) -> mark#(X1) ->
    mark#(len(X)) -> active#(len(mark(X)))
    mark#(fst(X1,X2)) -> mark#(X1) -> mark#(len(X)) -> len#(mark(X))
    mark#(fst(X1,X2)) -> mark#(X1) -> mark#(len(X)) -> mark#(X)
    mark#(fst(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    mark#(fst(X1,X2)) -> mark#(X1) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    mark#(fst(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X1)
    mark#(fst(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X2)
    mark#(fst(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> active#(from(mark(X)))
    mark#(fst(X1,X2)) -> mark#(X1) ->
    mark#(from(X)) -> from#(mark(X))
    mark#(fst(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X)
    mark#(fst(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(fst(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(fst(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(fst(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
    mark#(fst(X1,X2)) -> mark#(X1) -> mark#(nil()) -> active#(nil())
    mark#(fst(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(fst(X1,X2)) -> mark#(X1) ->
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    mark#(fst(X1,X2)) -> mark#(X1) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    mark#(fst(X1,X2)) -> mark#(X1) -> mark#(fst(X1,X2)) -> mark#(X1)
    mark#(fst(X1,X2)) -> mark#(X1) ->
    mark#(fst(X1,X2)) -> mark#(X2)
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(len(cons(X,Z))) -> mark#(s(len(Z)))
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(len(cons(X,Z))) -> s#(len(Z))
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(len(cons(X,Z))) -> len#(Z)
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(len(nil())) -> mark#(0())
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(add(s(X),Y)) -> add#(X,Y)
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(add(0(),X)) -> mark#(X)
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(from(X)) -> cons#(X,from(s(X)))
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(from(X)) -> from#(s(X))
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(from(X)) -> s#(X)
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z))
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z)
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
    active#(fst(0(),Z)) -> mark#(nil())
    mark#(0()) -> active#(0()) ->
    active#(len(cons(X,Z))) -> mark#(s(len(Z)))
    mark#(0()) -> active#(0()) -> active#(len(cons(X,Z))) -> s#(len(Z))
    mark#(0()) -> active#(0()) -> active#(len(cons(X,Z))) -> len#(Z)
    mark#(0()) -> active#(0()) -> active#(len(nil())) -> mark#(0())
    mark#(0()) -> active#(0()) ->
    active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
    mark#(0()) -> active#(0()) -> active#(add(s(X),Y)) -> s#(add(X,Y))
    mark#(0()) -> active#(0()) -> active#(add(s(X),Y)) -> add#(X,Y)
    mark#(0()) -> active#(0()) -> active#(add(0(),X)) -> mark#(X)
    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#(0()) -> active#(0()) ->
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
    mark#(0()) -> active#(0()) ->
    active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z))
    mark#(0()) -> active#(0()) ->
    active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z)
    mark#(0()) -> active#(0()) ->
    active#(fst(0(),Z)) -> mark#(nil())
    active#(len(cons(X,Z))) -> len#(Z) ->
    len#(active(X)) -> len#(X)
    active#(len(cons(X,Z))) -> len#(Z) ->
    len#(mark(X)) -> len#(X)
    active#(len(cons(X,Z))) -> s#(len(Z)) ->
    s#(active(X)) -> s#(X)
    active#(len(cons(X,Z))) -> s#(len(Z)) ->
    s#(mark(X)) -> s#(X)
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(len(X)) -> active#(len(mark(X)))
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(len(X)) -> len#(mark(X))
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(len(X)) -> mark#(X)
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(from(X)) -> active#(from(mark(X)))
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(from(X)) -> from#(mark(X))
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(from(X)) -> mark#(X)
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(s(X)) -> active#(s(X))
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(nil()) -> active#(nil())
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(0()) -> active#(0())
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(fst(X1,X2)) -> mark#(X1)
    active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
    mark#(fst(X1,X2)) -> mark#(X2)
    active#(len(nil())) -> mark#(0()) ->
    mark#(len(X)) -> active#(len(mark(X)))
    active#(len(nil())) -> mark#(0()) ->
    mark#(len(X)) -> len#(mark(X))
    active#(len(nil())) -> mark#(0()) -> mark#(len(X)) -> mark#(X)
    active#(len(nil())) -> mark#(0()) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(len(nil())) -> mark#(0()) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(len(nil())) -> mark#(0()) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(len(nil())) -> mark#(0()) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(len(nil())) -> mark#(0()) ->
    mark#(from(X)) -> active#(from(mark(X)))
    active#(len(nil())) -> mark#(0()) ->
    mark#(from(X)) -> from#(mark(X))
    active#(len(nil())) -> mark#(0()) ->
    mark#(from(X)) -> mark#(X)
    active#(len(nil())) -> mark#(0()) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(len(nil())) -> mark#(0()) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(len(nil())) -> mark#(0()) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(len(nil())) -> mark#(0()) ->
    mark#(s(X)) -> active#(s(X))
    active#(len(nil())) -> mark#(0()) ->
    mark#(nil()) -> active#(nil())
    active#(len(nil())) -> mark#(0()) ->
    mark#(0()) -> active#(0())
    active#(len(nil())) -> mark#(0()) ->
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    active#(len(nil())) -> mark#(0()) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    active#(len(nil())) -> mark#(0()) ->
    mark#(fst(X1,X2)) -> mark#(X1)
    active#(len(nil())) -> mark#(0()) ->
    mark#(fst(X1,X2)) -> mark#(X2)
    active#(add(s(X),Y)) -> add#(X,Y) ->
    add#(X1,active(X2)) -> add#(X1,X2)
    active#(add(s(X),Y)) -> add#(X,Y) ->
    add#(active(X1),X2) -> add#(X1,X2)
    active#(add(s(X),Y)) -> add#(X,Y) ->
    add#(X1,mark(X2)) -> add#(X1,X2)
    active#(add(s(X),Y)) -> add#(X,Y) ->
    add#(mark(X1),X2) -> add#(X1,X2)
    active#(add(s(X),Y)) -> s#(add(X,Y)) ->
    s#(active(X)) -> s#(X)
    active#(add(s(X),Y)) -> s#(add(X,Y)) ->
    s#(mark(X)) -> s#(X)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(len(X)) -> active#(len(mark(X)))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(len(X)) -> len#(mark(X))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(len(X)) -> mark#(X)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(from(X)) -> active#(from(mark(X)))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(from(X)) -> from#(mark(X))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(from(X)) -> mark#(X)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(s(X)) -> active#(s(X))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(nil()) -> active#(nil())
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(0()) -> active#(0())
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(fst(X1,X2)) -> mark#(X1)
    active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
    mark#(fst(X1,X2)) -> mark#(X2)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(len(X)) -> active#(len(mark(X)))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(len(X)) -> len#(mark(X))
    active#(add(0(),X)) -> mark#(X) -> mark#(len(X)) -> mark#(X)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(from(X)) -> active#(from(mark(X)))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(from(X)) -> from#(mark(X))
    active#(add(0(),X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(add(0(),X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(nil()) -> active#(nil())
    active#(add(0(),X)) -> mark#(X) -> mark#(0()) -> active#(0())
    active#(add(0(),X)) -> mark#(X) ->
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    active#(add(0(),X)) -> mark#(X) ->
    mark#(fst(X1,X2)) -> mark#(X1)
    active#(add(0(),X)) -> mark#(X) ->
    mark#(fst(X1,X2)) -> mark#(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)
    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)) -> mark#(cons(X,from(s(X)))) ->
    mark#(len(X)) -> active#(len(mark(X)))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(len(X)) -> len#(mark(X))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(len(X)) -> mark#(X)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(add(X1,X2)) -> mark#(X2)
    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)) -> 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#(s(X)) -> active#(s(X))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(nil()) -> active#(nil())
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(0()) -> active#(0())
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(fst(X1,X2)) -> mark#(X1)
    active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
    mark#(fst(X1,X2)) -> mark#(X2)
    active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z)) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z)) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z)) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(fst(s(X),cons(Y,Z))) -> cons#(Y,fst(X,Z)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z) ->
    fst#(X1,active(X2)) -> fst#(X1,X2)
    active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z) ->
    fst#(active(X1),X2) -> fst#(X1,X2)
    active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z) ->
    fst#(X1,mark(X2)) -> fst#(X1,X2)
    active#(fst(s(X),cons(Y,Z))) -> fst#(X,Z) ->
    fst#(mark(X1),X2) -> fst#(X1,X2)
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(len(X)) -> active#(len(mark(X)))
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(len(X)) -> len#(mark(X))
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(len(X)) -> mark#(X)
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(from(X)) -> active#(from(mark(X)))
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(from(X)) -> from#(mark(X))
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(from(X)) -> mark#(X)
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(s(X)) -> active#(s(X))
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(nil()) -> active#(nil())
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(0()) -> active#(0())
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(fst(X1,X2)) -> mark#(X1)
    active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
    mark#(fst(X1,X2)) -> mark#(X2)
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(len(X)) -> active#(len(mark(X)))
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(len(X)) -> len#(mark(X))
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(len(X)) -> mark#(X)
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(add(X1,X2)) -> add#(mark(X1),mark(X2))
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(add(X1,X2)) -> mark#(X1)
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(add(X1,X2)) -> mark#(X2)
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(from(X)) -> active#(from(mark(X)))
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(from(X)) -> from#(mark(X))
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(from(X)) -> mark#(X)
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(s(X)) -> active#(s(X))
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(nil()) -> active#(nil())
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(0()) -> active#(0())
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(fst(X1,X2)) -> fst#(mark(X1),mark(X2))
    active#(fst(0(),Z)) -> mark#(nil()) ->
    mark#(fst(X1,X2)) -> mark#(X1)
    active#(fst(0(),Z)) -> mark#(nil()) -> mark#(fst(X1,X2)) -> mark#(X2)
   SCC Processor:
    #sccs: 7
    #rules: 40
    #arcs: 510/2916
    DPs:
     mark#(len(X)) -> mark#(X)
     mark#(fst(X1,X2)) -> mark#(X2)
     mark#(fst(X1,X2)) -> mark#(X1)
     mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
     active#(fst(0(),Z)) -> mark#(nil())
     mark#(0()) -> active#(0())
     active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
     mark#(nil()) -> active#(nil())
     active#(from(X)) -> mark#(cons(X,from(s(X))))
     mark#(s(X)) -> active#(s(X))
     active#(add(0(),X)) -> mark#(X)
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
     mark#(from(X)) -> mark#(X)
     mark#(from(X)) -> active#(from(mark(X)))
     active#(len(nil())) -> mark#(0())
     mark#(add(X1,X2)) -> mark#(X2)
     mark#(add(X1,X2)) -> mark#(X1)
     mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
     active#(len(cons(X,Z))) -> mark#(s(len(Z)))
     mark#(len(X)) -> active#(len(mark(X)))
    TRS:
     active(fst(0(),Z)) -> mark(nil())
     active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(len(nil())) -> mark(0())
     active(len(cons(X,Z))) -> mark(s(len(Z)))
     mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
     mark(0()) -> active(0())
     mark(nil()) -> active(nil())
     mark(s(X)) -> active(s(X))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(from(X)) -> active(from(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(len(X)) -> active(len(mark(X)))
     fst(mark(X1),X2) -> fst(X1,X2)
     fst(X1,mark(X2)) -> fst(X1,X2)
     fst(active(X1),X2) -> fst(X1,X2)
     fst(X1,active(X2)) -> fst(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(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)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     len(mark(X)) -> len(X)
     len(active(X)) -> len(X)
    EDG Processor:
     DPs:
      mark#(len(X)) -> mark#(X)
      mark#(fst(X1,X2)) -> mark#(X2)
      mark#(fst(X1,X2)) -> mark#(X1)
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
      active#(fst(0(),Z)) -> mark#(nil())
      mark#(0()) -> active#(0())
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
      mark#(nil()) -> active#(nil())
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(s(X)) -> active#(s(X))
      active#(add(0(),X)) -> mark#(X)
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(from(X)) -> mark#(X)
      mark#(from(X)) -> active#(from(mark(X)))
      active#(len(nil())) -> mark#(0())
      mark#(add(X1,X2)) -> mark#(X2)
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      active#(len(cons(X,Z))) -> mark#(s(len(Z)))
      mark#(len(X)) -> active#(len(mark(X)))
     TRS:
      active(fst(0(),Z)) -> mark(nil())
      active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
      active(from(X)) -> mark(cons(X,from(s(X))))
      active(add(0(),X)) -> mark(X)
      active(add(s(X),Y)) -> mark(s(add(X,Y)))
      active(len(nil())) -> mark(0())
      active(len(cons(X,Z))) -> mark(s(len(Z)))
      mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
      mark(0()) -> active(0())
      mark(nil()) -> active(nil())
      mark(s(X)) -> active(s(X))
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(from(X)) -> active(from(mark(X)))
      mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
      mark(len(X)) -> active(len(mark(X)))
      fst(mark(X1),X2) -> fst(X1,X2)
      fst(X1,mark(X2)) -> fst(X1,X2)
      fst(active(X1),X2) -> fst(X1,X2)
      fst(X1,active(X2)) -> fst(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(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)
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
      add(mark(X1),X2) -> add(X1,X2)
      add(X1,mark(X2)) -> add(X1,X2)
      add(active(X1),X2) -> add(X1,X2)
      add(X1,active(X2)) -> add(X1,X2)
      len(mark(X)) -> len(X)
      len(active(X)) -> len(X)
     graph:
      mark#(len(X)) -> mark#(X) -> mark#(fst(X1,X2)) -> mark#(X2)
      mark#(len(X)) -> mark#(X) -> mark#(fst(X1,X2)) -> mark#(X1)
      mark#(len(X)) -> mark#(X) ->
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
      mark#(len(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      mark#(len(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
      mark#(len(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
      mark#(len(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
      mark#(len(X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(len(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
      mark#(len(X)) -> mark#(X) ->
      mark#(from(X)) -> active#(from(mark(X)))
      mark#(len(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
      mark#(len(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
      mark#(len(X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(len(X)) -> mark#(X) -> mark#(len(X)) -> mark#(X)
      mark#(len(X)) -> mark#(X) ->
      mark#(len(X)) -> active#(len(mark(X)))
      mark#(len(X)) -> active#(len(mark(X))) ->
      active#(fst(0(),Z)) -> mark#(nil())
      mark#(len(X)) -> active#(len(mark(X))) ->
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
      mark#(len(X)) -> active#(len(mark(X))) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(len(X)) -> active#(len(mark(X))) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(len(X)) -> active#(len(mark(X))) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(len(X)) -> active#(len(mark(X))) ->
      active#(len(nil())) -> mark#(0())
      mark#(len(X)) -> active#(len(mark(X))) ->
      active#(len(cons(X,Z))) -> mark#(s(len(Z)))
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(fst(X1,X2)) -> mark#(X2)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(fst(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
      mark#(add(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(nil()) -> active#(nil())
      mark#(add(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> active#(s(X))
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(add(X1,X2)) -> mark#(X2) -> mark#(from(X)) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(from(X)) -> active#(from(mark(X)))
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> mark#(X2)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(add(X1,X2)) -> mark#(X2) -> mark#(len(X)) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X2) ->
      mark#(len(X)) -> active#(len(mark(X)))
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(fst(X1,X2)) -> mark#(X2)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(fst(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
      mark#(add(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(nil()) -> active#(nil())
      mark#(add(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(add(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(from(X)) -> active#(from(mark(X)))
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X2)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(add(X1,X2)) -> mark#(X1) -> mark#(len(X)) -> mark#(X)
      mark#(add(X1,X2)) -> mark#(X1) ->
      mark#(len(X)) -> active#(len(mark(X)))
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(fst(0(),Z)) -> mark#(nil())
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(len(nil())) -> mark#(0())
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
      active#(len(cons(X,Z))) -> mark#(s(len(Z)))
      mark#(from(X)) -> mark#(X) -> mark#(fst(X1,X2)) -> mark#(X2)
      mark#(from(X)) -> mark#(X) -> mark#(fst(X1,X2)) -> mark#(X1)
      mark#(from(X)) -> mark#(X) ->
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
      mark#(from(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      mark#(from(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
      mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
      mark#(from(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
      mark#(from(X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(from(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
      mark#(from(X)) -> mark#(X) ->
      mark#(from(X)) -> active#(from(mark(X)))
      mark#(from(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
      mark#(from(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
      mark#(from(X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(from(X)) -> mark#(X) -> mark#(len(X)) -> mark#(X)
      mark#(from(X)) -> mark#(X) ->
      mark#(len(X)) -> active#(len(mark(X)))
      mark#(from(X)) -> active#(from(mark(X))) ->
      active#(fst(0(),Z)) -> mark#(nil())
      mark#(from(X)) -> active#(from(mark(X))) ->
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
      mark#(from(X)) -> active#(from(mark(X))) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(from(X)) -> active#(from(mark(X))) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(from(X)) -> active#(from(mark(X))) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(from(X)) -> active#(from(mark(X))) ->
      active#(len(nil())) -> mark#(0())
      mark#(from(X)) -> active#(from(mark(X))) ->
      active#(len(cons(X,Z))) -> mark#(s(len(Z)))
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(fst(X1,X2)) -> mark#(X2)
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(fst(X1,X2)) -> mark#(X1)
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
      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#(s(X)) -> active#(s(X))
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(cons(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X)
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(from(X)) -> active#(from(mark(X)))
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X2)
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(cons(X1,X2)) -> mark#(X1) -> mark#(len(X)) -> mark#(X)
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(len(X)) -> active#(len(mark(X)))
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
      active#(fst(0(),Z)) -> mark#(nil())
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
      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#(add(0(),X)) -> mark#(X)
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
      active#(len(nil())) -> mark#(0())
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
      active#(len(cons(X,Z))) -> mark#(s(len(Z)))
      mark#(s(X)) -> active#(s(X)) ->
      active#(fst(0(),Z)) -> mark#(nil())
      mark#(s(X)) -> active#(s(X)) ->
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
      mark#(s(X)) -> active#(s(X)) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(s(X)) -> active#(s(X)) -> active#(add(0(),X)) -> mark#(X)
      mark#(s(X)) -> active#(s(X)) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(s(X)) -> active#(s(X)) -> active#(len(nil())) -> mark#(0())
      mark#(s(X)) -> active#(s(X)) ->
      active#(len(cons(X,Z))) -> mark#(s(len(Z)))
      mark#(fst(X1,X2)) -> mark#(X2) ->
      mark#(fst(X1,X2)) -> mark#(X2)
      mark#(fst(X1,X2)) -> mark#(X2) ->
      mark#(fst(X1,X2)) -> mark#(X1)
      mark#(fst(X1,X2)) -> mark#(X2) ->
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
      mark#(fst(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
      mark#(fst(X1,X2)) -> mark#(X2) ->
      mark#(nil()) -> active#(nil())
      mark#(fst(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> active#(s(X))
      mark#(fst(X1,X2)) -> mark#(X2) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(fst(X1,X2)) -> mark#(X2) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(fst(X1,X2)) -> mark#(X2) -> mark#(from(X)) -> mark#(X)
      mark#(fst(X1,X2)) -> mark#(X2) ->
      mark#(from(X)) -> active#(from(mark(X)))
      mark#(fst(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> mark#(X2)
      mark#(fst(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(fst(X1,X2)) -> mark#(X2) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(fst(X1,X2)) -> mark#(X2) -> mark#(len(X)) -> mark#(X)
      mark#(fst(X1,X2)) -> mark#(X2) ->
      mark#(len(X)) -> active#(len(mark(X)))
      mark#(fst(X1,X2)) -> mark#(X1) ->
      mark#(fst(X1,X2)) -> mark#(X2)
      mark#(fst(X1,X2)) -> mark#(X1) ->
      mark#(fst(X1,X2)) -> mark#(X1)
      mark#(fst(X1,X2)) -> mark#(X1) ->
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
      mark#(fst(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
      mark#(fst(X1,X2)) -> mark#(X1) ->
      mark#(nil()) -> active#(nil())
      mark#(fst(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
      mark#(fst(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(fst(X1,X2)) -> mark#(X1) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(fst(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X)
      mark#(fst(X1,X2)) -> mark#(X1) ->
      mark#(from(X)) -> active#(from(mark(X)))
      mark#(fst(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X2)
      mark#(fst(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> mark#(X1)
      mark#(fst(X1,X2)) -> mark#(X1) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      mark#(fst(X1,X2)) -> mark#(X1) -> mark#(len(X)) -> mark#(X)
      mark#(fst(X1,X2)) -> mark#(X1) ->
      mark#(len(X)) -> active#(len(mark(X)))
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
      active#(fst(0(),Z)) -> mark#(nil())
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
      active#(add(0(),X)) -> mark#(X)
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
      active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
      active#(len(nil())) -> mark#(0())
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
      active#(len(cons(X,Z))) -> mark#(s(len(Z)))
      active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
      mark#(fst(X1,X2)) -> mark#(X2)
      active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
      mark#(fst(X1,X2)) -> mark#(X1)
      active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
      active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
      mark#(s(X)) -> active#(s(X))
      active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
      mark#(from(X)) -> mark#(X)
      active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
      mark#(from(X)) -> active#(from(mark(X)))
      active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
      mark#(add(X1,X2)) -> mark#(X2)
      active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
      mark#(len(X)) -> mark#(X)
      active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
      mark#(len(X)) -> active#(len(mark(X)))
      active#(len(nil())) -> mark#(0()) ->
      mark#(0()) -> active#(0())
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(fst(X1,X2)) -> mark#(X2)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(fst(X1,X2)) -> mark#(X1)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(s(X)) -> active#(s(X))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(from(X)) -> mark#(X)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(from(X)) -> active#(from(mark(X)))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(add(X1,X2)) -> mark#(X2)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(len(X)) -> mark#(X)
      active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
      mark#(len(X)) -> active#(len(mark(X)))
      active#(add(0(),X)) -> mark#(X) ->
      mark#(fst(X1,X2)) -> mark#(X2)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(fst(X1,X2)) -> mark#(X1)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
      active#(add(0(),X)) -> mark#(X) -> mark#(0()) -> active#(0())
      active#(add(0(),X)) -> mark#(X) ->
      mark#(nil()) -> active#(nil())
      active#(add(0(),X)) -> mark#(X) ->
      mark#(s(X)) -> active#(s(X))
      active#(add(0(),X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      active#(add(0(),X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(from(X)) -> active#(from(mark(X)))
      active#(add(0(),X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> mark#(X2)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      active#(add(0(),X)) -> mark#(X) -> mark#(len(X)) -> mark#(X)
      active#(add(0(),X)) -> mark#(X) ->
      mark#(len(X)) -> active#(len(mark(X)))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(fst(X1,X2)) -> mark#(X2)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(fst(X1,X2)) -> mark#(X1)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(s(X)) -> active#(s(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)) -> active#(cons(mark(X1),X2))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(from(X)) -> mark#(X)
      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#(add(X1,X2)) -> mark#(X2)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(len(X)) -> mark#(X)
      active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
      mark#(len(X)) -> active#(len(mark(X)))
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
      mark#(fst(X1,X2)) -> mark#(X2)
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
      mark#(fst(X1,X2)) -> mark#(X1)
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
      mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
      mark#(s(X)) -> active#(s(X))
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
      mark#(from(X)) -> mark#(X)
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
      mark#(from(X)) -> active#(from(mark(X)))
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
      mark#(add(X1,X2)) -> mark#(X2)
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
      mark#(add(X1,X2)) -> mark#(X1)
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
      mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
      mark#(len(X)) -> mark#(X)
      active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
      mark#(len(X)) -> active#(len(mark(X)))
      active#(fst(0(),Z)) -> mark#(nil()) -> mark#(nil()) -> active#(nil())
     CDG Processor:
      DPs:
       mark#(len(X)) -> mark#(X)
       mark#(fst(X1,X2)) -> mark#(X2)
       mark#(fst(X1,X2)) -> mark#(X1)
       mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
       active#(fst(0(),Z)) -> mark#(nil())
       mark#(0()) -> active#(0())
       active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
       mark#(nil()) -> active#(nil())
       active#(from(X)) -> mark#(cons(X,from(s(X))))
       mark#(s(X)) -> active#(s(X))
       active#(add(0(),X)) -> mark#(X)
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
       mark#(from(X)) -> mark#(X)
       mark#(from(X)) -> active#(from(mark(X)))
       active#(len(nil())) -> mark#(0())
       mark#(add(X1,X2)) -> mark#(X2)
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       active#(len(cons(X,Z))) -> mark#(s(len(Z)))
       mark#(len(X)) -> active#(len(mark(X)))
      TRS:
       active(fst(0(),Z)) -> mark(nil())
       active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(len(nil())) -> mark(0())
       active(len(cons(X,Z))) -> mark(s(len(Z)))
       mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
       mark(0()) -> active(0())
       mark(nil()) -> active(nil())
       mark(s(X)) -> active(s(X))
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(from(X)) -> active(from(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(len(X)) -> active(len(mark(X)))
       fst(mark(X1),X2) -> fst(X1,X2)
       fst(X1,mark(X2)) -> fst(X1,X2)
       fst(active(X1),X2) -> fst(X1,X2)
       fst(X1,active(X2)) -> fst(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(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)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       len(mark(X)) -> len(X)
       len(active(X)) -> len(X)
      graph:
       mark#(len(X)) -> mark#(X) -> mark#(len(X)) -> active#(len(mark(X)))
       mark#(len(X)) -> mark#(X) -> mark#(len(X)) -> mark#(X)
       mark#(len(X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(len(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
       mark#(len(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
       mark#(len(X)) -> mark#(X) ->
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(len(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
       mark#(len(X)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(len(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
       mark#(len(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(X))
       mark#(len(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
       mark#(len(X)) -> mark#(X) -> mark#(0()) -> active#(0())
       mark#(len(X)) -> mark#(X) ->
       mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
       mark#(len(X)) -> mark#(X) -> mark#(fst(X1,X2)) -> mark#(X1)
       mark#(len(X)) -> mark#(X) ->
       mark#(fst(X1,X2)) -> mark#(X2)
       mark#(len(X)) -> active#(len(mark(X))) ->
       active#(len(cons(X,Z))) -> mark#(s(len(Z)))
       mark#(len(X)) -> active#(len(mark(X))) ->
       active#(len(nil())) -> mark#(0())
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(len(X)) -> active#(len(mark(X)))
       mark#(add(X1,X2)) -> mark#(X2) -> mark#(len(X)) -> mark#(X)
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> mark#(X2)
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(add(X1,X2)) -> mark#(X2) -> mark#(from(X)) -> mark#(X)
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> active#(s(X))
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(nil()) -> active#(nil())
       mark#(add(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(fst(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X2) ->
       mark#(fst(X1,X2)) -> mark#(X2)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(len(X)) -> active#(len(mark(X)))
       mark#(add(X1,X2)) -> mark#(X1) -> mark#(len(X)) -> mark#(X)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X2)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(add(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(nil()) -> active#(nil())
       mark#(add(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(fst(X1,X2)) -> mark#(X1)
       mark#(add(X1,X2)) -> mark#(X1) ->
       mark#(fst(X1,X2)) -> mark#(X2)
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
       active#(add(s(X),Y)) -> mark#(s(add(X,Y)))
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2))) ->
       active#(add(0(),X)) -> mark#(X)
       mark#(from(X)) -> mark#(X) ->
       mark#(len(X)) -> active#(len(mark(X)))
       mark#(from(X)) -> mark#(X) -> mark#(len(X)) -> mark#(X)
       mark#(from(X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(from(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1)
       mark#(from(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2)
       mark#(from(X)) -> mark#(X) ->
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(from(X)) -> mark#(X) -> mark#(from(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)) -> mark#(X1)
       mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(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#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
       mark#(from(X)) -> mark#(X) -> mark#(fst(X1,X2)) -> mark#(X1)
       mark#(from(X)) -> mark#(X) ->
       mark#(fst(X1,X2)) -> mark#(X2)
       mark#(from(X)) -> active#(from(mark(X))) ->
       active#(from(X)) -> mark#(cons(X,from(s(X))))
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(len(X)) -> active#(len(mark(X)))
       mark#(cons(X1,X2)) -> mark#(X1) -> mark#(len(X)) -> mark#(X)
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X2)
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(cons(X1,X2)) -> mark#(X1) -> mark#(from(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)) -> mark#(X1)
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(s(X)) -> active#(s(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#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(fst(X1,X2)) -> mark#(X1)
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(fst(X1,X2)) -> mark#(X2)
       mark#(fst(X1,X2)) -> mark#(X2) ->
       mark#(len(X)) -> active#(len(mark(X)))
       mark#(fst(X1,X2)) -> mark#(X2) -> mark#(len(X)) -> mark#(X)
       mark#(fst(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(fst(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(fst(X1,X2)) -> mark#(X2) ->
       mark#(add(X1,X2)) -> mark#(X2)
       mark#(fst(X1,X2)) -> mark#(X2) ->
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(fst(X1,X2)) -> mark#(X2) -> mark#(from(X)) -> mark#(X)
       mark#(fst(X1,X2)) -> mark#(X2) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(fst(X1,X2)) -> mark#(X2) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(fst(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> active#(s(X))
       mark#(fst(X1,X2)) -> mark#(X2) ->
       mark#(nil()) -> active#(nil())
       mark#(fst(X1,X2)) -> mark#(X2) -> mark#(0()) -> active#(0())
       mark#(fst(X1,X2)) -> mark#(X2) ->
       mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
       mark#(fst(X1,X2)) -> mark#(X2) ->
       mark#(fst(X1,X2)) -> mark#(X1)
       mark#(fst(X1,X2)) -> mark#(X2) ->
       mark#(fst(X1,X2)) -> mark#(X2)
       mark#(fst(X1,X2)) -> mark#(X1) ->
       mark#(len(X)) -> active#(len(mark(X)))
       mark#(fst(X1,X2)) -> mark#(X1) -> mark#(len(X)) -> mark#(X)
       mark#(fst(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       mark#(fst(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X1)
       mark#(fst(X1,X2)) -> mark#(X1) ->
       mark#(add(X1,X2)) -> mark#(X2)
       mark#(fst(X1,X2)) -> mark#(X1) ->
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(fst(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X)
       mark#(fst(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(fst(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(fst(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> active#(s(X))
       mark#(fst(X1,X2)) -> mark#(X1) ->
       mark#(nil()) -> active#(nil())
       mark#(fst(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
       mark#(fst(X1,X2)) -> mark#(X1) ->
       mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
       mark#(fst(X1,X2)) -> mark#(X1) ->
       mark#(fst(X1,X2)) -> mark#(X1)
       mark#(fst(X1,X2)) -> mark#(X1) ->
       mark#(fst(X1,X2)) -> mark#(X2)
       mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
       active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
       mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2))) ->
       active#(fst(0(),Z)) -> mark#(nil())
       active#(len(cons(X,Z))) -> mark#(s(len(Z))) ->
       mark#(s(X)) -> active#(s(X))
       active#(len(nil())) -> mark#(0()) ->
       mark#(0()) -> active#(0())
       active#(add(s(X),Y)) -> mark#(s(add(X,Y))) ->
       mark#(s(X)) -> active#(s(X))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(len(X)) -> active#(len(mark(X)))
       active#(add(0(),X)) -> mark#(X) -> mark#(len(X)) -> mark#(X)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> mark#(X1)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(add(X1,X2)) -> mark#(X2)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(from(X)) -> active#(from(mark(X)))
       active#(add(0(),X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(s(X)) -> active#(s(X))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(nil()) -> active#(nil())
       active#(add(0(),X)) -> mark#(X) -> mark#(0()) -> active#(0())
       active#(add(0(),X)) -> mark#(X) ->
       mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
       active#(add(0(),X)) -> mark#(X) ->
       mark#(fst(X1,X2)) -> mark#(X1)
       active#(add(0(),X)) -> mark#(X) ->
       mark#(fst(X1,X2)) -> mark#(X2)
       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)) -> mark#(X1)
       active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z))) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       active#(fst(0(),Z)) -> mark#(nil()) -> mark#(nil()) -> active#(nil())
      SCC Processor:
       #sccs: 1
       #rules: 13
       #arcs: 135/484
       DPs:
        mark#(len(X)) -> mark#(X)
        mark#(fst(X1,X2)) -> mark#(X2)
        mark#(fst(X1,X2)) -> mark#(X1)
        mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
        active#(fst(s(X),cons(Y,Z))) -> mark#(cons(Y,fst(X,Z)))
        mark#(cons(X1,X2)) -> mark#(X1)
        mark#(from(X)) -> mark#(X)
        mark#(from(X)) -> active#(from(mark(X)))
        active#(from(X)) -> mark#(cons(X,from(s(X))))
        mark#(add(X1,X2)) -> mark#(X2)
        mark#(add(X1,X2)) -> mark#(X1)
        mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
        active#(add(0(),X)) -> mark#(X)
       TRS:
        active(fst(0(),Z)) -> mark(nil())
        active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
        active(from(X)) -> mark(cons(X,from(s(X))))
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(len(nil())) -> mark(0())
        active(len(cons(X,Z))) -> mark(s(len(Z)))
        mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
        mark(0()) -> active(0())
        mark(nil()) -> active(nil())
        mark(s(X)) -> active(s(X))
        mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
        mark(from(X)) -> active(from(mark(X)))
        mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
        mark(len(X)) -> active(len(mark(X)))
        fst(mark(X1),X2) -> fst(X1,X2)
        fst(X1,mark(X2)) -> fst(X1,X2)
        fst(active(X1),X2) -> fst(X1,X2)
        fst(X1,active(X2)) -> fst(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(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)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
        len(mark(X)) -> len(X)
        len(active(X)) -> len(X)
       KBO Processor:
        argument filtering:
         pi(0) = []
         pi(fst) = [0,1]
         pi(active) = 0
         pi(nil) = []
         pi(mark) = 0
         pi(s) = []
         pi(cons) = 0
         pi(from) = 0
         pi(add) = [0,1]
         pi(len) = [0]
         pi(active#) = 0
         pi(mark#) = 0
        weight function:
         w0 = 1
         w(len) = w(add) = w(cons) = w(s) = w(nil) = w(active) = w(fst) = w(
         0) = 1
         w(mark#) = w(active#) = w(from) = w(mark) = 0
        precedence:
         mark# ~ active# ~ len ~ add ~ from ~ cons ~ s ~ mark ~ nil ~ active ~ fst ~ 0
        problem:
         DPs:
          mark#(fst(X1,X2)) -> active#(fst(mark(X1),mark(X2)))
          mark#(cons(X1,X2)) -> mark#(X1)
          mark#(from(X)) -> mark#(X)
          mark#(from(X)) -> active#(from(mark(X)))
          active#(from(X)) -> mark#(cons(X,from(s(X))))
          mark#(add(X1,X2)) -> active#(add(mark(X1),mark(X2)))
         TRS:
          active(fst(0(),Z)) -> mark(nil())
          active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
          active(from(X)) -> mark(cons(X,from(s(X))))
          active(add(0(),X)) -> mark(X)
          active(add(s(X),Y)) -> mark(s(add(X,Y)))
          active(len(nil())) -> mark(0())
          active(len(cons(X,Z))) -> mark(s(len(Z)))
          mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
          mark(0()) -> active(0())
          mark(nil()) -> active(nil())
          mark(s(X)) -> active(s(X))
          mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
          mark(from(X)) -> active(from(mark(X)))
          mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
          mark(len(X)) -> active(len(mark(X)))
          fst(mark(X1),X2) -> fst(X1,X2)
          fst(X1,mark(X2)) -> fst(X1,X2)
          fst(active(X1),X2) -> fst(X1,X2)
          fst(X1,active(X2)) -> fst(X1,X2)
          s(mark(X)) -> s(X)
          s(active(X)) -> s(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)
          from(mark(X)) -> from(X)
          from(active(X)) -> from(X)
          add(mark(X1),X2) -> add(X1,X2)
          add(X1,mark(X2)) -> add(X1,X2)
          add(active(X1),X2) -> add(X1,X2)
          add(X1,active(X2)) -> add(X1,X2)
          len(mark(X)) -> len(X)
          len(active(X)) -> len(X)
        SCC Processor:
         #sccs: 1
         #rules: 4
         #arcs: 85/36
         DPs:
          mark#(from(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))))
         TRS:
          active(fst(0(),Z)) -> mark(nil())
          active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
          active(from(X)) -> mark(cons(X,from(s(X))))
          active(add(0(),X)) -> mark(X)
          active(add(s(X),Y)) -> mark(s(add(X,Y)))
          active(len(nil())) -> mark(0())
          active(len(cons(X,Z))) -> mark(s(len(Z)))
          mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
          mark(0()) -> active(0())
          mark(nil()) -> active(nil())
          mark(s(X)) -> active(s(X))
          mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
          mark(from(X)) -> active(from(mark(X)))
          mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
          mark(len(X)) -> active(len(mark(X)))
          fst(mark(X1),X2) -> fst(X1,X2)
          fst(X1,mark(X2)) -> fst(X1,X2)
          fst(active(X1),X2) -> fst(X1,X2)
          fst(X1,active(X2)) -> fst(X1,X2)
          s(mark(X)) -> s(X)
          s(active(X)) -> s(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)
          from(mark(X)) -> from(X)
          from(active(X)) -> from(X)
          add(mark(X1),X2) -> add(X1,X2)
          add(X1,mark(X2)) -> add(X1,X2)
          add(active(X1),X2) -> add(X1,X2)
          add(X1,active(X2)) -> add(X1,X2)
          len(mark(X)) -> len(X)
          len(active(X)) -> len(X)
         KBO Processor:
          argument filtering:
           pi(0) = []
           pi(fst) = [1]
           pi(active) = 0
           pi(nil) = []
           pi(mark) = 0
           pi(s) = []
           pi(cons) = 0
           pi(from) = [0]
           pi(add) = [1]
           pi(len) = []
           pi(active#) = 0
           pi(mark#) = 0
          weight function:
           w0 = 1
           w(len) = w(s) = w(nil) = w(active) = w(0) = 1
           w(mark#) = w(active#) = w(add) = w(from) = w(cons) = w(mark) = w(
           fst) = 0
          precedence:
           len ~ add ~ from ~ fst > mark# ~ active# ~ cons ~ s ~ mark ~ nil ~ active ~ 0
          problem:
           DPs:
            mark#(cons(X1,X2)) -> mark#(X1)
            mark#(from(X)) -> active#(from(mark(X)))
           TRS:
            active(fst(0(),Z)) -> mark(nil())
            active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
            active(from(X)) -> mark(cons(X,from(s(X))))
            active(add(0(),X)) -> mark(X)
            active(add(s(X),Y)) -> mark(s(add(X,Y)))
            active(len(nil())) -> mark(0())
            active(len(cons(X,Z))) -> mark(s(len(Z)))
            mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
            mark(0()) -> active(0())
            mark(nil()) -> active(nil())
            mark(s(X)) -> active(s(X))
            mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
            mark(from(X)) -> active(from(mark(X)))
            mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
            mark(len(X)) -> active(len(mark(X)))
            fst(mark(X1),X2) -> fst(X1,X2)
            fst(X1,mark(X2)) -> fst(X1,X2)
            fst(active(X1),X2) -> fst(X1,X2)
            fst(X1,active(X2)) -> fst(X1,X2)
            s(mark(X)) -> s(X)
            s(active(X)) -> s(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)
            from(mark(X)) -> from(X)
            from(active(X)) -> from(X)
            add(mark(X1),X2) -> add(X1,X2)
            add(X1,mark(X2)) -> add(X1,X2)
            add(active(X1),X2) -> add(X1,X2)
            add(X1,active(X2)) -> add(X1,X2)
            len(mark(X)) -> len(X)
            len(active(X)) -> len(X)
          SCC Processor:
           #sccs: 1
           #rules: 1
           #arcs: 8/4
           DPs:
            mark#(cons(X1,X2)) -> mark#(X1)
           TRS:
            active(fst(0(),Z)) -> mark(nil())
            active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
            active(from(X)) -> mark(cons(X,from(s(X))))
            active(add(0(),X)) -> mark(X)
            active(add(s(X),Y)) -> mark(s(add(X,Y)))
            active(len(nil())) -> mark(0())
            active(len(cons(X,Z))) -> mark(s(len(Z)))
            mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
            mark(0()) -> active(0())
            mark(nil()) -> active(nil())
            mark(s(X)) -> active(s(X))
            mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
            mark(from(X)) -> active(from(mark(X)))
            mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
            mark(len(X)) -> active(len(mark(X)))
            fst(mark(X1),X2) -> fst(X1,X2)
            fst(X1,mark(X2)) -> fst(X1,X2)
            fst(active(X1),X2) -> fst(X1,X2)
            fst(X1,active(X2)) -> fst(X1,X2)
            s(mark(X)) -> s(X)
            s(active(X)) -> s(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)
            from(mark(X)) -> from(X)
            from(active(X)) -> from(X)
            add(mark(X1),X2) -> add(X1,X2)
            add(X1,mark(X2)) -> add(X1,X2)
            add(active(X1),X2) -> add(X1,X2)
            add(X1,active(X2)) -> add(X1,X2)
            len(mark(X)) -> len(X)
            len(active(X)) -> len(X)
           Subterm Criterion Processor:
            simple projection:
             pi(mark#) = 0
            problem:
             DPs:
              
             TRS:
              active(fst(0(),Z)) -> mark(nil())
              active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
              active(from(X)) -> mark(cons(X,from(s(X))))
              active(add(0(),X)) -> mark(X)
              active(add(s(X),Y)) -> mark(s(add(X,Y)))
              active(len(nil())) -> mark(0())
              active(len(cons(X,Z))) -> mark(s(len(Z)))
              mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
              mark(0()) -> active(0())
              mark(nil()) -> active(nil())
              mark(s(X)) -> active(s(X))
              mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
              mark(from(X)) -> active(from(mark(X)))
              mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
              mark(len(X)) -> active(len(mark(X)))
              fst(mark(X1),X2) -> fst(X1,X2)
              fst(X1,mark(X2)) -> fst(X1,X2)
              fst(active(X1),X2) -> fst(X1,X2)
              fst(X1,active(X2)) -> fst(X1,X2)
              s(mark(X)) -> s(X)
              s(active(X)) -> s(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)
              from(mark(X)) -> from(X)
              from(active(X)) -> from(X)
              add(mark(X1),X2) -> add(X1,X2)
              add(X1,mark(X2)) -> add(X1,X2)
              add(active(X1),X2) -> add(X1,X2)
              add(X1,active(X2)) -> add(X1,X2)
              len(mark(X)) -> len(X)
              len(active(X)) -> len(X)
            Qed
    
    DPs:
     fst#(mark(X1),X2) -> fst#(X1,X2)
     fst#(X1,mark(X2)) -> fst#(X1,X2)
     fst#(active(X1),X2) -> fst#(X1,X2)
     fst#(X1,active(X2)) -> fst#(X1,X2)
    TRS:
     active(fst(0(),Z)) -> mark(nil())
     active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(len(nil())) -> mark(0())
     active(len(cons(X,Z))) -> mark(s(len(Z)))
     mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
     mark(0()) -> active(0())
     mark(nil()) -> active(nil())
     mark(s(X)) -> active(s(X))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(from(X)) -> active(from(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(len(X)) -> active(len(mark(X)))
     fst(mark(X1),X2) -> fst(X1,X2)
     fst(X1,mark(X2)) -> fst(X1,X2)
     fst(active(X1),X2) -> fst(X1,X2)
     fst(X1,active(X2)) -> fst(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(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)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     len(mark(X)) -> len(X)
     len(active(X)) -> len(X)
    Subterm Criterion Processor:
     simple projection:
      pi(fst#) = 1
     problem:
      DPs:
       fst#(mark(X1),X2) -> fst#(X1,X2)
       fst#(active(X1),X2) -> fst#(X1,X2)
      TRS:
       active(fst(0(),Z)) -> mark(nil())
       active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(len(nil())) -> mark(0())
       active(len(cons(X,Z))) -> mark(s(len(Z)))
       mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
       mark(0()) -> active(0())
       mark(nil()) -> active(nil())
       mark(s(X)) -> active(s(X))
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(from(X)) -> active(from(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(len(X)) -> active(len(mark(X)))
       fst(mark(X1),X2) -> fst(X1,X2)
       fst(X1,mark(X2)) -> fst(X1,X2)
       fst(active(X1),X2) -> fst(X1,X2)
       fst(X1,active(X2)) -> fst(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(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)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       len(mark(X)) -> len(X)
       len(active(X)) -> len(X)
     Subterm Criterion Processor:
      simple projection:
       pi(fst#) = 0
      problem:
       DPs:
        
       TRS:
        active(fst(0(),Z)) -> mark(nil())
        active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
        active(from(X)) -> mark(cons(X,from(s(X))))
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(len(nil())) -> mark(0())
        active(len(cons(X,Z))) -> mark(s(len(Z)))
        mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
        mark(0()) -> active(0())
        mark(nil()) -> active(nil())
        mark(s(X)) -> active(s(X))
        mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
        mark(from(X)) -> active(from(mark(X)))
        mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
        mark(len(X)) -> active(len(mark(X)))
        fst(mark(X1),X2) -> fst(X1,X2)
        fst(X1,mark(X2)) -> fst(X1,X2)
        fst(active(X1),X2) -> fst(X1,X2)
        fst(X1,active(X2)) -> fst(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(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)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
        len(mark(X)) -> len(X)
        len(active(X)) -> len(X)
      Qed
    
    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(fst(0(),Z)) -> mark(nil())
     active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(len(nil())) -> mark(0())
     active(len(cons(X,Z))) -> mark(s(len(Z)))
     mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
     mark(0()) -> active(0())
     mark(nil()) -> active(nil())
     mark(s(X)) -> active(s(X))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(from(X)) -> active(from(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(len(X)) -> active(len(mark(X)))
     fst(mark(X1),X2) -> fst(X1,X2)
     fst(X1,mark(X2)) -> fst(X1,X2)
     fst(active(X1),X2) -> fst(X1,X2)
     fst(X1,active(X2)) -> fst(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(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)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     len(mark(X)) -> len(X)
     len(active(X)) -> len(X)
    Subterm Criterion Processor:
     simple projection:
      pi(cons#) = 1
     problem:
      DPs:
       cons#(mark(X1),X2) -> cons#(X1,X2)
       cons#(active(X1),X2) -> cons#(X1,X2)
      TRS:
       active(fst(0(),Z)) -> mark(nil())
       active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(len(nil())) -> mark(0())
       active(len(cons(X,Z))) -> mark(s(len(Z)))
       mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
       mark(0()) -> active(0())
       mark(nil()) -> active(nil())
       mark(s(X)) -> active(s(X))
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(from(X)) -> active(from(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(len(X)) -> active(len(mark(X)))
       fst(mark(X1),X2) -> fst(X1,X2)
       fst(X1,mark(X2)) -> fst(X1,X2)
       fst(active(X1),X2) -> fst(X1,X2)
       fst(X1,active(X2)) -> fst(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(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)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       len(mark(X)) -> len(X)
       len(active(X)) -> len(X)
     Subterm Criterion Processor:
      simple projection:
       pi(cons#) = 0
      problem:
       DPs:
        
       TRS:
        active(fst(0(),Z)) -> mark(nil())
        active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
        active(from(X)) -> mark(cons(X,from(s(X))))
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(len(nil())) -> mark(0())
        active(len(cons(X,Z))) -> mark(s(len(Z)))
        mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
        mark(0()) -> active(0())
        mark(nil()) -> active(nil())
        mark(s(X)) -> active(s(X))
        mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
        mark(from(X)) -> active(from(mark(X)))
        mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
        mark(len(X)) -> active(len(mark(X)))
        fst(mark(X1),X2) -> fst(X1,X2)
        fst(X1,mark(X2)) -> fst(X1,X2)
        fst(active(X1),X2) -> fst(X1,X2)
        fst(X1,active(X2)) -> fst(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(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)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
        len(mark(X)) -> len(X)
        len(active(X)) -> len(X)
      Qed
    
    DPs:
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
    TRS:
     active(fst(0(),Z)) -> mark(nil())
     active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(len(nil())) -> mark(0())
     active(len(cons(X,Z))) -> mark(s(len(Z)))
     mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
     mark(0()) -> active(0())
     mark(nil()) -> active(nil())
     mark(s(X)) -> active(s(X))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(from(X)) -> active(from(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(len(X)) -> active(len(mark(X)))
     fst(mark(X1),X2) -> fst(X1,X2)
     fst(X1,mark(X2)) -> fst(X1,X2)
     fst(active(X1),X2) -> fst(X1,X2)
     fst(X1,active(X2)) -> fst(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(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)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     len(mark(X)) -> len(X)
     len(active(X)) -> len(X)
    Subterm Criterion Processor:
     simple projection:
      pi(s#) = 0
     problem:
      DPs:
       
      TRS:
       active(fst(0(),Z)) -> mark(nil())
       active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(len(nil())) -> mark(0())
       active(len(cons(X,Z))) -> mark(s(len(Z)))
       mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
       mark(0()) -> active(0())
       mark(nil()) -> active(nil())
       mark(s(X)) -> active(s(X))
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(from(X)) -> active(from(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(len(X)) -> active(len(mark(X)))
       fst(mark(X1),X2) -> fst(X1,X2)
       fst(X1,mark(X2)) -> fst(X1,X2)
       fst(active(X1),X2) -> fst(X1,X2)
       fst(X1,active(X2)) -> fst(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(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)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       len(mark(X)) -> len(X)
       len(active(X)) -> len(X)
     Qed
    
    DPs:
     from#(mark(X)) -> from#(X)
     from#(active(X)) -> from#(X)
    TRS:
     active(fst(0(),Z)) -> mark(nil())
     active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(len(nil())) -> mark(0())
     active(len(cons(X,Z))) -> mark(s(len(Z)))
     mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
     mark(0()) -> active(0())
     mark(nil()) -> active(nil())
     mark(s(X)) -> active(s(X))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(from(X)) -> active(from(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(len(X)) -> active(len(mark(X)))
     fst(mark(X1),X2) -> fst(X1,X2)
     fst(X1,mark(X2)) -> fst(X1,X2)
     fst(active(X1),X2) -> fst(X1,X2)
     fst(X1,active(X2)) -> fst(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(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)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     len(mark(X)) -> len(X)
     len(active(X)) -> len(X)
    Subterm Criterion Processor:
     simple projection:
      pi(from#) = 0
     problem:
      DPs:
       
      TRS:
       active(fst(0(),Z)) -> mark(nil())
       active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(len(nil())) -> mark(0())
       active(len(cons(X,Z))) -> mark(s(len(Z)))
       mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
       mark(0()) -> active(0())
       mark(nil()) -> active(nil())
       mark(s(X)) -> active(s(X))
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(from(X)) -> active(from(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(len(X)) -> active(len(mark(X)))
       fst(mark(X1),X2) -> fst(X1,X2)
       fst(X1,mark(X2)) -> fst(X1,X2)
       fst(active(X1),X2) -> fst(X1,X2)
       fst(X1,active(X2)) -> fst(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(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)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       len(mark(X)) -> len(X)
       len(active(X)) -> len(X)
     Qed
    
    DPs:
     add#(mark(X1),X2) -> add#(X1,X2)
     add#(X1,mark(X2)) -> add#(X1,X2)
     add#(active(X1),X2) -> add#(X1,X2)
     add#(X1,active(X2)) -> add#(X1,X2)
    TRS:
     active(fst(0(),Z)) -> mark(nil())
     active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(len(nil())) -> mark(0())
     active(len(cons(X,Z))) -> mark(s(len(Z)))
     mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
     mark(0()) -> active(0())
     mark(nil()) -> active(nil())
     mark(s(X)) -> active(s(X))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(from(X)) -> active(from(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(len(X)) -> active(len(mark(X)))
     fst(mark(X1),X2) -> fst(X1,X2)
     fst(X1,mark(X2)) -> fst(X1,X2)
     fst(active(X1),X2) -> fst(X1,X2)
     fst(X1,active(X2)) -> fst(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(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)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     len(mark(X)) -> len(X)
     len(active(X)) -> len(X)
    Subterm Criterion Processor:
     simple projection:
      pi(add#) = 1
     problem:
      DPs:
       add#(mark(X1),X2) -> add#(X1,X2)
       add#(active(X1),X2) -> add#(X1,X2)
      TRS:
       active(fst(0(),Z)) -> mark(nil())
       active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(len(nil())) -> mark(0())
       active(len(cons(X,Z))) -> mark(s(len(Z)))
       mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
       mark(0()) -> active(0())
       mark(nil()) -> active(nil())
       mark(s(X)) -> active(s(X))
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(from(X)) -> active(from(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(len(X)) -> active(len(mark(X)))
       fst(mark(X1),X2) -> fst(X1,X2)
       fst(X1,mark(X2)) -> fst(X1,X2)
       fst(active(X1),X2) -> fst(X1,X2)
       fst(X1,active(X2)) -> fst(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(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)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       len(mark(X)) -> len(X)
       len(active(X)) -> len(X)
     Subterm Criterion Processor:
      simple projection:
       pi(add#) = 0
      problem:
       DPs:
        
       TRS:
        active(fst(0(),Z)) -> mark(nil())
        active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
        active(from(X)) -> mark(cons(X,from(s(X))))
        active(add(0(),X)) -> mark(X)
        active(add(s(X),Y)) -> mark(s(add(X,Y)))
        active(len(nil())) -> mark(0())
        active(len(cons(X,Z))) -> mark(s(len(Z)))
        mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
        mark(0()) -> active(0())
        mark(nil()) -> active(nil())
        mark(s(X)) -> active(s(X))
        mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
        mark(from(X)) -> active(from(mark(X)))
        mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
        mark(len(X)) -> active(len(mark(X)))
        fst(mark(X1),X2) -> fst(X1,X2)
        fst(X1,mark(X2)) -> fst(X1,X2)
        fst(active(X1),X2) -> fst(X1,X2)
        fst(X1,active(X2)) -> fst(X1,X2)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(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)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
        add(mark(X1),X2) -> add(X1,X2)
        add(X1,mark(X2)) -> add(X1,X2)
        add(active(X1),X2) -> add(X1,X2)
        add(X1,active(X2)) -> add(X1,X2)
        len(mark(X)) -> len(X)
        len(active(X)) -> len(X)
      Qed
    
    DPs:
     len#(mark(X)) -> len#(X)
     len#(active(X)) -> len#(X)
    TRS:
     active(fst(0(),Z)) -> mark(nil())
     active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
     active(from(X)) -> mark(cons(X,from(s(X))))
     active(add(0(),X)) -> mark(X)
     active(add(s(X),Y)) -> mark(s(add(X,Y)))
     active(len(nil())) -> mark(0())
     active(len(cons(X,Z))) -> mark(s(len(Z)))
     mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
     mark(0()) -> active(0())
     mark(nil()) -> active(nil())
     mark(s(X)) -> active(s(X))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(from(X)) -> active(from(mark(X)))
     mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
     mark(len(X)) -> active(len(mark(X)))
     fst(mark(X1),X2) -> fst(X1,X2)
     fst(X1,mark(X2)) -> fst(X1,X2)
     fst(active(X1),X2) -> fst(X1,X2)
     fst(X1,active(X2)) -> fst(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(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)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
     add(mark(X1),X2) -> add(X1,X2)
     add(X1,mark(X2)) -> add(X1,X2)
     add(active(X1),X2) -> add(X1,X2)
     add(X1,active(X2)) -> add(X1,X2)
     len(mark(X)) -> len(X)
     len(active(X)) -> len(X)
    Subterm Criterion Processor:
     simple projection:
      pi(len#) = 0
     problem:
      DPs:
       
      TRS:
       active(fst(0(),Z)) -> mark(nil())
       active(fst(s(X),cons(Y,Z))) -> mark(cons(Y,fst(X,Z)))
       active(from(X)) -> mark(cons(X,from(s(X))))
       active(add(0(),X)) -> mark(X)
       active(add(s(X),Y)) -> mark(s(add(X,Y)))
       active(len(nil())) -> mark(0())
       active(len(cons(X,Z))) -> mark(s(len(Z)))
       mark(fst(X1,X2)) -> active(fst(mark(X1),mark(X2)))
       mark(0()) -> active(0())
       mark(nil()) -> active(nil())
       mark(s(X)) -> active(s(X))
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(from(X)) -> active(from(mark(X)))
       mark(add(X1,X2)) -> active(add(mark(X1),mark(X2)))
       mark(len(X)) -> active(len(mark(X)))
       fst(mark(X1),X2) -> fst(X1,X2)
       fst(X1,mark(X2)) -> fst(X1,X2)
       fst(active(X1),X2) -> fst(X1,X2)
       fst(X1,active(X2)) -> fst(X1,X2)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(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)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
       add(mark(X1),X2) -> add(X1,X2)
       add(X1,mark(X2)) -> add(X1,X2)
       add(active(X1),X2) -> add(X1,X2)
       add(X1,active(X2)) -> add(X1,X2)
       len(mark(X)) -> len(X)
       len(active(X)) -> len(X)
     Qed