YES

Problem:
 active(zeros()) -> mark(cons(0(),zeros()))
 active(tail(cons(X,XS))) -> mark(XS)
 mark(zeros()) -> active(zeros())
 mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
 mark(0()) -> active(0())
 mark(tail(X)) -> active(tail(mark(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)
 tail(mark(X)) -> tail(X)
 tail(active(X)) -> tail(X)

Proof:
 DP Processor:
  DPs:
   active#(zeros()) -> cons#(0(),zeros())
   active#(zeros()) -> mark#(cons(0(),zeros()))
   active#(tail(cons(X,XS))) -> mark#(XS)
   mark#(zeros()) -> active#(zeros())
   mark#(cons(X1,X2)) -> mark#(X1)
   mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
   mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
   mark#(0()) -> active#(0())
   mark#(tail(X)) -> mark#(X)
   mark#(tail(X)) -> tail#(mark(X))
   mark#(tail(X)) -> active#(tail(mark(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)
   tail#(mark(X)) -> tail#(X)
   tail#(active(X)) -> tail#(X)
  TRS:
   active(zeros()) -> mark(cons(0(),zeros()))
   active(tail(cons(X,XS))) -> mark(XS)
   mark(zeros()) -> active(zeros())
   mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
   mark(0()) -> active(0())
   mark(tail(X)) -> active(tail(mark(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)
   tail(mark(X)) -> tail(X)
   tail(active(X)) -> tail(X)
  TDG Processor:
   DPs:
    active#(zeros()) -> cons#(0(),zeros())
    active#(zeros()) -> mark#(cons(0(),zeros()))
    active#(tail(cons(X,XS))) -> mark#(XS)
    mark#(zeros()) -> active#(zeros())
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(0()) -> active#(0())
    mark#(tail(X)) -> mark#(X)
    mark#(tail(X)) -> tail#(mark(X))
    mark#(tail(X)) -> active#(tail(mark(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)
    tail#(mark(X)) -> tail#(X)
    tail#(active(X)) -> tail#(X)
   TRS:
    active(zeros()) -> mark(cons(0(),zeros()))
    active(tail(cons(X,XS))) -> mark(XS)
    mark(zeros()) -> active(zeros())
    mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
    mark(0()) -> active(0())
    mark(tail(X)) -> active(tail(mark(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)
    tail(mark(X)) -> tail(X)
    tail(active(X)) -> tail(X)
   graph:
    tail#(mark(X)) -> tail#(X) -> tail#(active(X)) -> tail#(X)
    tail#(mark(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X)
    tail#(active(X)) -> tail#(X) -> tail#(active(X)) -> tail#(X)
    tail#(active(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X)
    mark#(tail(X)) -> tail#(mark(X)) ->
    tail#(active(X)) -> tail#(X)
    mark#(tail(X)) -> tail#(mark(X)) -> tail#(mark(X)) -> tail#(X)
    mark#(tail(X)) -> mark#(X) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> tail#(mark(X))
    mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
    mark#(tail(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(tail(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(tail(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(tail(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(tail(X)) -> mark#(X) ->
    mark#(zeros()) -> active#(zeros())
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(tail(cons(X,XS))) -> mark#(XS)
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(tail(X)) -> active#(tail(mark(X))) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(tail(X)) -> tail#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tail(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    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#(zeros()) -> active#(zeros())
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(tail(cons(X,XS))) -> mark#(XS)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(0()) -> active#(0()) -> active#(tail(cons(X,XS))) -> mark#(XS)
    mark#(0()) -> active#(0()) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(0()) -> active#(0()) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(zeros()) -> active#(zeros()) ->
    active#(tail(cons(X,XS))) -> mark#(XS)
    mark#(zeros()) -> active#(zeros()) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(zeros()) -> active#(zeros()) ->
    active#(zeros()) -> cons#(0(),zeros())
    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)
    active#(tail(cons(X,XS))) -> mark#(XS) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    active#(tail(cons(X,XS))) -> mark#(XS) ->
    mark#(tail(X)) -> tail#(mark(X))
    active#(tail(cons(X,XS))) -> mark#(XS) ->
    mark#(tail(X)) -> mark#(X)
    active#(tail(cons(X,XS))) -> mark#(XS) ->
    mark#(0()) -> active#(0())
    active#(tail(cons(X,XS))) -> mark#(XS) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(tail(cons(X,XS))) -> mark#(XS) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(tail(cons(X,XS))) -> mark#(XS) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(tail(cons(X,XS))) -> mark#(XS) ->
    mark#(zeros()) -> active#(zeros())
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(tail(X)) -> active#(tail(mark(X)))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(tail(X)) -> tail#(mark(X))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(tail(X)) -> mark#(X)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(0()) -> active#(0())
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(zeros()) -> active#(zeros())
    active#(zeros()) -> cons#(0(),zeros()) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(zeros()) -> cons#(0(),zeros()) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(zeros()) -> cons#(0(),zeros()) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(zeros()) -> cons#(0(),zeros()) -> cons#(mark(X1),X2) -> cons#(X1,X2)
   EDG Processor:
    DPs:
     active#(zeros()) -> cons#(0(),zeros())
     active#(zeros()) -> mark#(cons(0(),zeros()))
     active#(tail(cons(X,XS))) -> mark#(XS)
     mark#(zeros()) -> active#(zeros())
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     mark#(0()) -> active#(0())
     mark#(tail(X)) -> mark#(X)
     mark#(tail(X)) -> tail#(mark(X))
     mark#(tail(X)) -> active#(tail(mark(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)
     tail#(mark(X)) -> tail#(X)
     tail#(active(X)) -> tail#(X)
    TRS:
     active(zeros()) -> mark(cons(0(),zeros()))
     active(tail(cons(X,XS))) -> mark(XS)
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(0()) -> active(0())
     mark(tail(X)) -> active(tail(mark(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)
     tail(mark(X)) -> tail(X)
     tail(active(X)) -> tail(X)
    graph:
     tail#(mark(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X)
     tail#(mark(X)) -> tail#(X) -> tail#(active(X)) -> tail#(X)
     tail#(active(X)) -> tail#(X) -> tail#(mark(X)) -> tail#(X)
     tail#(active(X)) -> tail#(X) -> tail#(active(X)) -> tail#(X)
     mark#(tail(X)) -> tail#(mark(X)) -> tail#(mark(X)) -> tail#(X)
     mark#(tail(X)) -> tail#(mark(X)) -> tail#(active(X)) -> tail#(X)
     mark#(tail(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros())
     mark#(tail(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
     mark#(tail(X)) -> mark#(X) ->
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     mark#(tail(X)) -> mark#(X) ->
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     mark#(tail(X)) -> mark#(X) -> mark#(0()) -> active#(0())
     mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
     mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> tail#(mark(X))
     mark#(tail(X)) -> mark#(X) ->
     mark#(tail(X)) -> active#(tail(mark(X)))
     mark#(tail(X)) -> active#(tail(mark(X))) ->
     active#(tail(cons(X,XS))) -> mark#(XS)
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(zeros()) -> active#(zeros())
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
     mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tail(X)) -> mark#(X)
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(tail(X)) -> tail#(mark(X))
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(tail(X)) -> active#(tail(mark(X)))
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
     cons#(X1,mark(X2)) -> cons#(X1,X2)
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
     cons#(active(X1),X2) -> cons#(X1,X2)
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
     cons#(X1,active(X2)) -> cons#(X1,X2)
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
     active#(tail(cons(X,XS))) -> mark#(XS)
     mark#(zeros()) -> active#(zeros()) ->
     active#(zeros()) -> cons#(0(),zeros())
     mark#(zeros()) -> active#(zeros()) ->
     active#(zeros()) -> mark#(cons(0(),zeros()))
     cons#(mark(X1),X2) -> cons#(X1,X2) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(mark(X1),X2) -> cons#(X1,X2) ->
     cons#(X1,mark(X2)) -> cons#(X1,X2)
     cons#(mark(X1),X2) -> cons#(X1,X2) ->
     cons#(active(X1),X2) -> cons#(X1,X2)
     cons#(mark(X1),X2) -> cons#(X1,X2) ->
     cons#(X1,active(X2)) -> cons#(X1,X2)
     cons#(active(X1),X2) -> cons#(X1,X2) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(active(X1),X2) -> cons#(X1,X2) ->
     cons#(X1,mark(X2)) -> cons#(X1,X2)
     cons#(active(X1),X2) -> cons#(X1,X2) ->
     cons#(active(X1),X2) -> cons#(X1,X2)
     cons#(active(X1),X2) -> cons#(X1,X2) ->
     cons#(X1,active(X2)) -> cons#(X1,X2)
     cons#(X1,mark(X2)) -> cons#(X1,X2) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(X1,mark(X2)) -> cons#(X1,X2) ->
     cons#(X1,mark(X2)) -> cons#(X1,X2)
     cons#(X1,mark(X2)) -> cons#(X1,X2) ->
     cons#(active(X1),X2) -> cons#(X1,X2)
     cons#(X1,mark(X2)) -> cons#(X1,X2) ->
     cons#(X1,active(X2)) -> cons#(X1,X2)
     cons#(X1,active(X2)) -> cons#(X1,X2) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(X1,active(X2)) -> cons#(X1,X2) ->
     cons#(X1,mark(X2)) -> cons#(X1,X2)
     cons#(X1,active(X2)) -> cons#(X1,X2) ->
     cons#(active(X1),X2) -> cons#(X1,X2)
     cons#(X1,active(X2)) -> cons#(X1,X2) ->
     cons#(X1,active(X2)) -> cons#(X1,X2)
     active#(tail(cons(X,XS))) -> mark#(XS) ->
     mark#(zeros()) -> active#(zeros())
     active#(tail(cons(X,XS))) -> mark#(XS) ->
     mark#(cons(X1,X2)) -> mark#(X1)
     active#(tail(cons(X,XS))) -> mark#(XS) ->
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     active#(tail(cons(X,XS))) -> mark#(XS) ->
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     active#(tail(cons(X,XS))) -> mark#(XS) ->
     mark#(0()) -> active#(0())
     active#(tail(cons(X,XS))) -> mark#(XS) ->
     mark#(tail(X)) -> mark#(X)
     active#(tail(cons(X,XS))) -> mark#(XS) ->
     mark#(tail(X)) -> tail#(mark(X))
     active#(tail(cons(X,XS))) -> mark#(XS) ->
     mark#(tail(X)) -> active#(tail(mark(X)))
     active#(zeros()) -> mark#(cons(0(),zeros())) ->
     mark#(cons(X1,X2)) -> mark#(X1)
     active#(zeros()) -> mark#(cons(0(),zeros())) ->
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     active#(zeros()) -> mark#(cons(0(),zeros())) ->
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    CDG Processor:
     DPs:
      active#(zeros()) -> cons#(0(),zeros())
      active#(zeros()) -> mark#(cons(0(),zeros()))
      active#(tail(cons(X,XS))) -> mark#(XS)
      mark#(zeros()) -> active#(zeros())
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(0()) -> active#(0())
      mark#(tail(X)) -> mark#(X)
      mark#(tail(X)) -> tail#(mark(X))
      mark#(tail(X)) -> active#(tail(mark(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)
      tail#(mark(X)) -> tail#(X)
      tail#(active(X)) -> tail#(X)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(tail(cons(X,XS))) -> mark(XS)
      mark(zeros()) -> active(zeros())
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(0()) -> active(0())
      mark(tail(X)) -> active(tail(mark(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)
      tail(mark(X)) -> tail(X)
      tail(active(X)) -> tail(X)
     graph:
      mark#(tail(X)) -> tail#(mark(X)) ->
      tail#(active(X)) -> tail#(X)
      mark#(tail(X)) -> tail#(mark(X)) -> tail#(mark(X)) -> tail#(X)
      mark#(tail(X)) -> mark#(X) ->
      mark#(tail(X)) -> active#(tail(mark(X)))
      mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> tail#(mark(X))
      mark#(tail(X)) -> mark#(X) -> mark#(tail(X)) -> mark#(X)
      mark#(tail(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      mark#(tail(X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(tail(X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
      mark#(tail(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
      mark#(tail(X)) -> mark#(X) ->
      mark#(zeros()) -> active#(zeros())
      mark#(tail(X)) -> active#(tail(mark(X))) ->
      active#(tail(cons(X,XS))) -> mark#(XS)
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(tail(X)) -> active#(tail(mark(X)))
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(tail(X)) -> tail#(mark(X))
      mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tail(X)) -> mark#(X)
      mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
      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#(zeros()) -> active#(zeros())
      mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
      cons#(active(X1),X2) -> cons#(X1,X2)
      mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
      cons#(mark(X1),X2) -> cons#(X1,X2)
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
      active#(tail(cons(X,XS))) -> mark#(XS)
      mark#(zeros()) -> active#(zeros()) ->
      active#(zeros()) -> mark#(cons(0(),zeros()))
      mark#(zeros()) -> active#(zeros()) ->
      active#(zeros()) -> cons#(0(),zeros())
      active#(tail(cons(X,XS))) -> mark#(XS) ->
      mark#(tail(X)) -> active#(tail(mark(X)))
      active#(tail(cons(X,XS))) -> mark#(XS) ->
      mark#(tail(X)) -> tail#(mark(X))
      active#(tail(cons(X,XS))) -> mark#(XS) ->
      mark#(tail(X)) -> mark#(X)
      active#(tail(cons(X,XS))) -> mark#(XS) ->
      mark#(0()) -> active#(0())
      active#(tail(cons(X,XS))) -> mark#(XS) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      active#(tail(cons(X,XS))) -> mark#(XS) ->
      mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
      active#(tail(cons(X,XS))) -> mark#(XS) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      active#(tail(cons(X,XS))) -> mark#(XS) ->
      mark#(zeros()) -> active#(zeros())
      active#(zeros()) -> mark#(cons(0(),zeros())) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      active#(zeros()) -> mark#(cons(0(),zeros())) ->
      mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
      active#(zeros()) -> mark#(cons(0(),zeros())) -> mark#(cons(X1,X2)) -> mark#(X1)
     SCC Processor:
      #sccs: 1
      #rules: 7
      #arcs: 35/289
      DPs:
       mark#(tail(X)) -> mark#(X)
       mark#(zeros()) -> active#(zeros())
       active#(zeros()) -> mark#(cons(0(),zeros()))
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       active#(tail(cons(X,XS))) -> mark#(XS)
       mark#(tail(X)) -> active#(tail(mark(X)))
      TRS:
       active(zeros()) -> mark(cons(0(),zeros()))
       active(tail(cons(X,XS))) -> mark(XS)
       mark(zeros()) -> active(zeros())
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(0()) -> active(0())
       mark(tail(X)) -> active(tail(mark(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)
       tail(mark(X)) -> tail(X)
       tail(active(X)) -> tail(X)
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [mark#](x0) = 2x0 + 1/2,
        
        [active#](x0) = 2x0,
        
        [tail](x0) = 2x0 + 2,
        
        [mark](x0) = x0,
        
        [cons](x0, x1) = 2x0 + 1/2x1 + 1/2,
        
        [0] = 0,
        
        [active](x0) = x0,
        
        [zeros] = 2
       orientation:
        mark#(tail(X)) = 4X + 9/2 >= 2X + 1/2 = mark#(X)
        
        mark#(zeros()) = 9/2 >= 4 = active#(zeros())
        
        active#(zeros()) = 4 >= 7/2 = mark#(cons(0(),zeros()))
        
        mark#(cons(X1,X2)) = 4X1 + X2 + 3/2 >= 2X1 + 1/2 = mark#(X1)
        
        mark#(cons(X1,X2)) = 4X1 + X2 + 3/2 >= 4X1 + X2 + 1 = active#(cons(mark(X1),X2))
        
        active#(tail(cons(X,XS))) = 8X + 2XS + 6 >= 2XS + 1/2 = mark#(XS)
        
        mark#(tail(X)) = 4X + 9/2 >= 4X + 4 = active#(tail(mark(X)))
        
        active(zeros()) = 2 >= 3/2 = mark(cons(0(),zeros()))
        
        active(tail(cons(X,XS))) = 4X + XS + 3 >= XS = mark(XS)
        
        mark(zeros()) = 2 >= 2 = active(zeros())
        
        mark(cons(X1,X2)) = 2X1 + 1/2X2 + 1/2 >= 2X1 + 1/2X2 + 1/2 = active(cons(mark(X1),X2))
        
        mark(0()) = 0 >= 0 = active(0())
        
        mark(tail(X)) = 2X + 2 >= 2X + 2 = active(tail(mark(X)))
        
        cons(mark(X1),X2) = 2X1 + 1/2X2 + 1/2 >= 2X1 + 1/2X2 + 1/2 = cons(X1,X2)
        
        cons(X1,mark(X2)) = 2X1 + 1/2X2 + 1/2 >= 2X1 + 1/2X2 + 1/2 = cons(X1,X2)
        
        cons(active(X1),X2) = 2X1 + 1/2X2 + 1/2 >= 2X1 + 1/2X2 + 1/2 = cons(X1,X2)
        
        cons(X1,active(X2)) = 2X1 + 1/2X2 + 1/2 >= 2X1 + 1/2X2 + 1/2 = cons(X1,X2)
        
        tail(mark(X)) = 2X + 2 >= 2X + 2 = tail(X)
        
        tail(active(X)) = 2X + 2 >= 2X + 2 = tail(X)
       problem:
        DPs:
         
        TRS:
         active(zeros()) -> mark(cons(0(),zeros()))
         active(tail(cons(X,XS))) -> mark(XS)
         mark(zeros()) -> active(zeros())
         mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
         mark(0()) -> active(0())
         mark(tail(X)) -> active(tail(mark(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)
         tail(mark(X)) -> tail(X)
         tail(active(X)) -> tail(X)
       Qed