MAYBE

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:
      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#(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#(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#(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)
     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#(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#(active(X1),X2) -> cons#(X1,X2)
       mark#(zeros()) -> active#(zeros()) ->
       active#(zeros()) -> cons#(0(),zeros())
       mark#(zeros()) -> active#(zeros()) ->
       active#(zeros()) -> mark#(cons(0(),zeros()))
       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))
      Restore Modifier:
       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)
       SCC Processor:
        #sccs: 1
        #rules: 6
        #arcs: 34/289
        DPs:
         mark#(tail(X)) -> 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())
         active#(zeros()) -> mark#(cons(0(),zeros()))
        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)
        Open