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#(active(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()) -> 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))
    SCC Processor:
     #sccs: 3
     #rules: 13
     #arcs: 55/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)) -> 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)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [mark#](x0) = 1,
       
       [active#](x0) = x0,
       
       [tail](x0) = 1,
       
       [mark](x0) = 1,
       
       [cons](x0, x1) = 0,
       
       [0] = 0,
       
       [active](x0) = x0,
       
       [zeros] = 1
      orientation:
       mark#(tail(X)) = 1 >= 1 = mark#(X)
       
       mark#(tail(X)) = 1 >= 1 = active#(tail(mark(X)))
       
       active#(tail(cons(X,XS))) = 1 >= 1 = mark#(XS)
       
       mark#(cons(X1,X2)) = 1 >= 0 = active#(cons(mark(X1),X2))
       
       mark#(cons(X1,X2)) = 1 >= 1 = mark#(X1)
       
       mark#(zeros()) = 1 >= 1 = active#(zeros())
       
       active#(zeros()) = 1 >= 1 = mark#(cons(0(),zeros()))
       
       active(zeros()) = 1 >= 1 = mark(cons(0(),zeros()))
       
       active(tail(cons(X,XS))) = 1 >= 1 = mark(XS)
       
       mark(zeros()) = 1 >= 1 = active(zeros())
       
       mark(cons(X1,X2)) = 1 >= 0 = active(cons(mark(X1),X2))
       
       mark(0()) = 1 >= 0 = active(0())
       
       mark(tail(X)) = 1 >= 1 = active(tail(mark(X)))
       
       cons(mark(X1),X2) = 0 >= 0 = cons(X1,X2)
       
       cons(X1,mark(X2)) = 0 >= 0 = cons(X1,X2)
       
       cons(active(X1),X2) = 0 >= 0 = cons(X1,X2)
       
       cons(X1,active(X2)) = 0 >= 0 = cons(X1,X2)
       
       tail(mark(X)) = 1 >= 1 = tail(X)
       
       tail(active(X)) = 1 >= 1 = 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)) -> 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)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [mark#](x0) = x0,
        
        [active#](x0) = x0,
        
        [tail](x0) = x0 + 1,
        
        [mark](x0) = x0,
        
        [cons](x0, x1) = x0 + x1,
        
        [0] = 0,
        
        [active](x0) = x0,
        
        [zeros] = 0
       orientation:
        mark#(tail(X)) = X + 1 >= X = mark#(X)
        
        mark#(tail(X)) = X + 1 >= X + 1 = active#(tail(mark(X)))
        
        active#(tail(cons(X,XS))) = X + XS + 1 >= XS = mark#(XS)
        
        mark#(cons(X1,X2)) = X1 + X2 >= X1 = mark#(X1)
        
        mark#(zeros()) = 0 >= 0 = active#(zeros())
        
        active#(zeros()) = 0 >= 0 = mark#(cons(0(),zeros()))
        
        active(zeros()) = 0 >= 0 = mark(cons(0(),zeros()))
        
        active(tail(cons(X,XS))) = X + XS + 1 >= XS = mark(XS)
        
        mark(zeros()) = 0 >= 0 = active(zeros())
        
        mark(cons(X1,X2)) = X1 + X2 >= X1 + X2 = active(cons(mark(X1),X2))
        
        mark(0()) = 0 >= 0 = active(0())
        
        mark(tail(X)) = X + 1 >= X + 1 = active(tail(mark(X)))
        
        cons(mark(X1),X2) = X1 + X2 >= X1 + X2 = cons(X1,X2)
        
        cons(X1,mark(X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2)
        
        cons(active(X1),X2) = X1 + X2 >= X1 + X2 = cons(X1,X2)
        
        cons(X1,active(X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2)
        
        tail(mark(X)) = X + 1 >= X + 1 = tail(X)
        
        tail(active(X)) = X + 1 >= X + 1 = tail(X)
       problem:
        DPs:
         mark#(tail(X)) -> active#(tail(mark(X)))
         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)
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [mark#](x0) = x0,
         
         [active#](x0) = 0,
         
         [tail](x0) = x0 + 1,
         
         [mark](x0) = x0,
         
         [cons](x0, x1) = x0 + x1,
         
         [0] = 0,
         
         [active](x0) = x0,
         
         [zeros] = 0
        orientation:
         mark#(tail(X)) = X + 1 >= 0 = active#(tail(mark(X)))
         
         mark#(cons(X1,X2)) = X1 + X2 >= X1 = mark#(X1)
         
         mark#(zeros()) = 0 >= 0 = active#(zeros())
         
         active#(zeros()) = 0 >= 0 = mark#(cons(0(),zeros()))
         
         active(zeros()) = 0 >= 0 = mark(cons(0(),zeros()))
         
         active(tail(cons(X,XS))) = X + XS + 1 >= XS = mark(XS)
         
         mark(zeros()) = 0 >= 0 = active(zeros())
         
         mark(cons(X1,X2)) = X1 + X2 >= X1 + X2 = active(cons(mark(X1),X2))
         
         mark(0()) = 0 >= 0 = active(0())
         
         mark(tail(X)) = X + 1 >= X + 1 = active(tail(mark(X)))
         
         cons(mark(X1),X2) = X1 + X2 >= X1 + X2 = cons(X1,X2)
         
         cons(X1,mark(X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2)
         
         cons(active(X1),X2) = X1 + X2 >= X1 + X2 = cons(X1,X2)
         
         cons(X1,active(X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2)
         
         tail(mark(X)) = X + 1 >= X + 1 = tail(X)
         
         tail(active(X)) = X + 1 >= X + 1 = tail(X)
        problem:
         DPs:
          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
     
     DPs:
      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)
     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
     
     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)
     Open