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)
   SCC Processor:
    #sccs: 3
    #rules: 14
    #arcs: 74/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#(0()) -> active#(0())
     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)
    EDG Processor:
     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#(0()) -> active#(0())
      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)
     graph:
      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)) -> 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)) -> 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)) -> 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)) -> active#(tail(mark(X)))
      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()))
      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)) -> 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)) -> 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)) -> active#(cons(mark(X1),X2))
     SCC Processor:
      #sccs: 1
      #rules: 7
      #arcs: 23/64
      DPs:
       mark#(tail(X)) -> mark#(X)
       mark#(tail(X)) -> active#(tail(mark(X)))
       active#(tail(cons(X,XS))) -> mark#(XS)
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       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)
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [mark#](x0) = x0,
        
        [active#](x0) = x0,
        
        [tail](x0) = x0,
        
        [mark](x0) = x0,
        
        [cons](x0, x1) = 2x0 + x1,
        
        [0] = 3,
        
        [active](x0) = x0,
        
        [zeros] = 6
       orientation:
        mark#(tail(X)) = X >= X = mark#(X)
        
        mark#(tail(X)) = X >= X = active#(tail(mark(X)))
        
        active#(tail(cons(X,XS))) = 2X + XS >= XS = mark#(XS)
        
        mark#(cons(X1,X2)) = 2X1 + X2 >= 2X1 + X2 = active#(cons(mark(X1),X2))
        
        mark#(cons(X1,X2)) = 2X1 + X2 >= X1 = mark#(X1)
        
        mark#(zeros()) = 6 >= 6 = active#(zeros())
        
        active#(zeros()) = 6 >= 6 = mark#(cons(0(),zeros()))
        
        active(zeros()) = 6 >= 6 = mark(cons(0(),zeros()))
        
        active(tail(cons(X,XS))) = 2X + XS >= XS = mark(XS)
        
        mark(zeros()) = 6 >= 6 = active(zeros())
        
        mark(cons(X1,X2)) = 2X1 + X2 >= 2X1 + X2 = active(cons(mark(X1),X2))
        
        mark(0()) = 3 >= 3 = active(0())
        
        mark(tail(X)) = X >= X = active(tail(mark(X)))
        
        cons(mark(X1),X2) = 2X1 + X2 >= 2X1 + X2 = cons(X1,X2)
        
        cons(X1,mark(X2)) = 2X1 + X2 >= 2X1 + X2 = cons(X1,X2)
        
        cons(active(X1),X2) = 2X1 + X2 >= 2X1 + X2 = cons(X1,X2)
        
        cons(X1,active(X2)) = 2X1 + X2 >= 2X1 + X2 = cons(X1,X2)
        
        tail(mark(X)) = X >= X = tail(X)
        
        tail(active(X)) = X >= X = tail(X)
       problem:
        DPs:
         mark#(tail(X)) -> mark#(X)
         mark#(tail(X)) -> active#(tail(mark(X)))
         active#(tail(cons(X,XS))) -> mark#(XS)
         mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
         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)
       Arctic Interpretation Processor:
        dimension: 1
        interpretation:
         [mark#](x0) = x0 + 0,
         
         [active#](x0) = x0 + 0,
         
         [tail](x0) = 1x0,
         
         [mark](x0) = x0,
         
         [cons](x0, x1) = x0 + x1 + 0,
         
         [0] = 0,
         
         [active](x0) = x0,
         
         [zeros] = 4
        orientation:
         mark#(tail(X)) = 1X + 0 >= X + 0 = mark#(X)
         
         mark#(tail(X)) = 1X + 0 >= 1X + 0 = active#(tail(mark(X)))
         
         active#(tail(cons(X,XS))) = 1X + 1XS + 1 >= XS + 0 = mark#(XS)
         
         mark#(cons(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = active#(cons(mark(X1),X2))
         
         mark#(zeros()) = 4 >= 4 = active#(zeros())
         
         active#(zeros()) = 4 >= 4 = mark#(cons(0(),zeros()))
         
         active(zeros()) = 4 >= 4 = mark(cons(0(),zeros()))
         
         active(tail(cons(X,XS))) = 1X + 1XS + 1 >= XS = mark(XS)
         
         mark(zeros()) = 4 >= 4 = active(zeros())
         
         mark(cons(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = active(cons(mark(X1),X2))
         
         mark(0()) = 0 >= 0 = active(0())
         
         mark(tail(X)) = 1X >= 1X = active(tail(mark(X)))
         
         cons(mark(X1),X2) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
         
         cons(X1,mark(X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
         
         cons(active(X1),X2) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
         
         cons(X1,active(X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
         
         tail(mark(X)) = 1X >= 1X = tail(X)
         
         tail(active(X)) = 1X >= 1X = tail(X)
        problem:
         DPs:
          mark#(tail(X)) -> mark#(X)
          mark#(tail(X)) -> active#(tail(mark(X)))
          mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
          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)
        SCC Processor:
         #sccs: 1
         #rules: 1
         #arcs: 20/25
         DPs:
          mark#(tail(X)) -> 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)
         Subterm Criterion Processor:
          simple projection:
           pi(mark#) = 0
          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
    
    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(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)
    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(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)
     Subterm Criterion Processor:
      simple projection:
       pi(cons#) = 0
      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
    
    DPs:
     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)
    Subterm Criterion Processor:
     simple projection:
      pi(tail#) = 0
     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