YES

Problem:
 active(2nd(cons(X,cons(Y,Z)))) -> mark(Y)
 active(from(X)) -> mark(cons(X,from(s(X))))
 mark(2nd(X)) -> active(2nd(mark(X)))
 mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
 mark(from(X)) -> active(from(mark(X)))
 mark(s(X)) -> active(s(mark(X)))
 2nd(mark(X)) -> 2nd(X)
 2nd(active(X)) -> 2nd(X)
 cons(mark(X1),X2) -> cons(X1,X2)
 cons(X1,mark(X2)) -> cons(X1,X2)
 cons(active(X1),X2) -> cons(X1,X2)
 cons(X1,active(X2)) -> cons(X1,X2)
 from(mark(X)) -> from(X)
 from(active(X)) -> from(X)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)

Proof:
 Matrix Interpretation Processor: dim=3
  
  interpretation:
             [1 1 0]     [0]
   [s](x0) = [0 0 0]x0 + [0]
             [0 0 0]     [1],
   
                [1 1 0]     [1]
   [from](x0) = [1 1 0]x0 + [0]
                [0 0 0]     [0],
   
                [1 1 0]     [0]
   [mark](x0) = [0 0 0]x0 + [0]
                [0 0 0]     [1],
   
                  [1 1 0]     [0]
   [active](x0) = [0 0 0]x0 + [0]
                  [0 0 0]     [1],
   
               [1 1 0]     [1]
   [2nd](x0) = [0 0 0]x0 + [0]
               [0 0 0]     [0],
   
                    [1 1 0]     [1 0 0]  
   [cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                    [0 0 0]     [0 0 0]  
  orientation:
                                    [1 1 0]    [1 1 0]    [1 0 0]    [1]    [1 1 0]    [0]          
   active(2nd(cons(X,cons(Y,Z)))) = [0 0 0]X + [0 0 0]Y + [0 0 0]Z + [0] >= [0 0 0]Y + [0] = mark(Y)
                                    [0 0 0]    [0 0 0]    [0 0 0]    [1]    [0 0 0]    [1]          
   
                     [2 2 0]    [1]    [2 2 0]    [1]                           
   active(from(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = mark(cons(X,from(s(X))))
                     [0 0 0]    [1]    [0 0 0]    [1]                           
   
                  [1 1 0]    [1]    [1 1 0]    [1]                       
   mark(2nd(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(2nd(mark(X)))
                  [0 0 0]    [1]    [0 0 0]    [1]                       
   
                       [1 1 0]     [1 0 0]     [0]    [1 1 0]     [1 0 0]     [0]                            
   mark(cons(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 + [0] >= [0 0 0]X1 + [0 0 0]X2 + [0] = active(cons(mark(X1),X2))
                       [0 0 0]     [0 0 0]     [1]    [0 0 0]     [0 0 0]     [1]                            
   
                   [2 2 0]    [1]    [2 2 0]    [1]                        
   mark(from(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(from(mark(X)))
                   [0 0 0]    [1]    [0 0 0]    [1]                        
   
                [1 1 0]    [0]    [1 1 0]    [0]                     
   mark(s(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(s(mark(X)))
                [0 0 0]    [1]    [0 0 0]    [1]                     
   
                  [1 1 0]    [1]    [1 1 0]    [1]         
   2nd(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = 2nd(X)
                  [0 0 0]    [0]    [0 0 0]    [0]         
   
                    [1 1 0]    [1]    [1 1 0]    [1]         
   2nd(active(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = 2nd(X)
                    [0 0 0]    [0]    [0 0 0]    [0]         
   
                       [1 1 0]     [1 0 0]      [1 1 0]     [1 0 0]                
   cons(mark(X1),X2) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2)
                       [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]                
   
                       [1 1 0]     [1 1 0]      [1 1 0]     [1 0 0]                
   cons(X1,mark(X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2)
                       [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]                
   
                         [1 1 0]     [1 0 0]      [1 1 0]     [1 0 0]                
   cons(active(X1),X2) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2)
                         [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]                
   
                         [1 1 0]     [1 1 0]      [1 1 0]     [1 0 0]                
   cons(X1,active(X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = cons(X1,X2)
                         [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]                
   
                   [1 1 0]    [1]    [1 1 0]    [1]          
   from(mark(X)) = [1 1 0]X + [0] >= [1 1 0]X + [0] = from(X)
                   [0 0 0]    [0]    [0 0 0]    [0]          
   
                     [1 1 0]    [1]    [1 1 0]    [1]          
   from(active(X)) = [1 1 0]X + [0] >= [1 1 0]X + [0] = from(X)
                     [0 0 0]    [0]    [0 0 0]    [0]          
   
                [1 1 0]    [0]    [1 1 0]    [0]       
   s(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = s(X)
                [0 0 0]    [1]    [0 0 0]    [1]       
   
                  [1 1 0]    [0]    [1 1 0]    [0]       
   s(active(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = s(X)
                  [0 0 0]    [1]    [0 0 0]    [1]       
  problem:
   active(from(X)) -> mark(cons(X,from(s(X))))
   mark(2nd(X)) -> active(2nd(mark(X)))
   mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
   mark(from(X)) -> active(from(mark(X)))
   mark(s(X)) -> active(s(mark(X)))
   2nd(mark(X)) -> 2nd(X)
   2nd(active(X)) -> 2nd(X)
   cons(mark(X1),X2) -> cons(X1,X2)
   cons(X1,mark(X2)) -> cons(X1,X2)
   cons(active(X1),X2) -> cons(X1,X2)
   cons(X1,active(X2)) -> cons(X1,X2)
   from(mark(X)) -> from(X)
   from(active(X)) -> from(X)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
  DP Processor:
   DPs:
    active#(from(X)) -> s#(X)
    active#(from(X)) -> from#(s(X))
    active#(from(X)) -> cons#(X,from(s(X)))
    active#(from(X)) -> mark#(cons(X,from(s(X))))
    mark#(2nd(X)) -> mark#(X)
    mark#(2nd(X)) -> 2nd#(mark(X))
    mark#(2nd(X)) -> active#(2nd(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(from(X)) -> mark#(X)
    mark#(from(X)) -> from#(mark(X))
    mark#(from(X)) -> active#(from(mark(X)))
    mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> active#(s(mark(X)))
    2nd#(mark(X)) -> 2nd#(X)
    2nd#(active(X)) -> 2nd#(X)
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2)
    from#(mark(X)) -> from#(X)
    from#(active(X)) -> from#(X)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
   TRS:
    active(from(X)) -> mark(cons(X,from(s(X))))
    mark(2nd(X)) -> active(2nd(mark(X)))
    mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
    mark(from(X)) -> active(from(mark(X)))
    mark(s(X)) -> active(s(mark(X)))
    2nd(mark(X)) -> 2nd(X)
    2nd(active(X)) -> 2nd(X)
    cons(mark(X1),X2) -> cons(X1,X2)
    cons(X1,mark(X2)) -> cons(X1,X2)
    cons(active(X1),X2) -> cons(X1,X2)
    cons(X1,active(X2)) -> cons(X1,X2)
    from(mark(X)) -> from(X)
    from(active(X)) -> from(X)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
   TDG Processor:
    DPs:
     active#(from(X)) -> s#(X)
     active#(from(X)) -> from#(s(X))
     active#(from(X)) -> cons#(X,from(s(X)))
     active#(from(X)) -> mark#(cons(X,from(s(X))))
     mark#(2nd(X)) -> mark#(X)
     mark#(2nd(X)) -> 2nd#(mark(X))
     mark#(2nd(X)) -> active#(2nd(mark(X)))
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     mark#(from(X)) -> mark#(X)
     mark#(from(X)) -> from#(mark(X))
     mark#(from(X)) -> active#(from(mark(X)))
     mark#(s(X)) -> mark#(X)
     mark#(s(X)) -> s#(mark(X))
     mark#(s(X)) -> active#(s(mark(X)))
     2nd#(mark(X)) -> 2nd#(X)
     2nd#(active(X)) -> 2nd#(X)
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(X1,mark(X2)) -> cons#(X1,X2)
     cons#(active(X1),X2) -> cons#(X1,X2)
     cons#(X1,active(X2)) -> cons#(X1,X2)
     from#(mark(X)) -> from#(X)
     from#(active(X)) -> from#(X)
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
    TRS:
     active(from(X)) -> mark(cons(X,from(s(X))))
     mark(2nd(X)) -> active(2nd(mark(X)))
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(from(X)) -> active(from(mark(X)))
     mark(s(X)) -> active(s(mark(X)))
     2nd(mark(X)) -> 2nd(X)
     2nd(active(X)) -> 2nd(X)
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     from(mark(X)) -> from(X)
     from(active(X)) -> from(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
    graph:
     2nd#(mark(X)) -> 2nd#(X) -> 2nd#(active(X)) -> 2nd#(X)
     2nd#(mark(X)) -> 2nd#(X) -> 2nd#(mark(X)) -> 2nd#(X)
     2nd#(active(X)) -> 2nd#(X) -> 2nd#(active(X)) -> 2nd#(X)
     2nd#(active(X)) -> 2nd#(X) -> 2nd#(mark(X)) -> 2nd#(X)
     mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
     mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
     mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
     mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> active#(from(mark(X)))
     mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> from#(mark(X))
     mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
     mark#(s(X)) -> mark#(X) ->
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
     mark#(s(X)) -> mark#(X) -> mark#(2nd(X)) -> active#(2nd(mark(X)))
     mark#(s(X)) -> mark#(X) -> mark#(2nd(X)) -> 2nd#(mark(X))
     mark#(s(X)) -> mark#(X) -> mark#(2nd(X)) -> mark#(X)
     mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X)
     mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X)
     mark#(s(X)) -> active#(s(mark(X))) ->
     active#(from(X)) -> mark#(cons(X,from(s(X))))
     mark#(s(X)) -> active#(s(mark(X))) ->
     active#(from(X)) -> cons#(X,from(s(X)))
     mark#(s(X)) -> active#(s(mark(X))) ->
     active#(from(X)) -> from#(s(X))
     mark#(s(X)) -> active#(s(mark(X))) -> active#(from(X)) -> s#(X)
     mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
     mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
     mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
     mark#(from(X)) -> mark#(X) ->
     mark#(from(X)) -> active#(from(mark(X)))
     mark#(from(X)) -> mark#(X) -> mark#(from(X)) -> from#(mark(X))
     mark#(from(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
     mark#(from(X)) -> mark#(X) ->
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     mark#(from(X)) -> mark#(X) ->
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     mark#(from(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
     mark#(from(X)) -> mark#(X) -> mark#(2nd(X)) -> active#(2nd(mark(X)))
     mark#(from(X)) -> mark#(X) -> mark#(2nd(X)) -> 2nd#(mark(X))
     mark#(from(X)) -> mark#(X) -> mark#(2nd(X)) -> mark#(X)
     mark#(from(X)) -> from#(mark(X)) ->
     from#(active(X)) -> from#(X)
     mark#(from(X)) -> from#(mark(X)) ->
     from#(mark(X)) -> from#(X)
     mark#(from(X)) -> active#(from(mark(X))) ->
     active#(from(X)) -> mark#(cons(X,from(s(X))))
     mark#(from(X)) -> active#(from(mark(X))) ->
     active#(from(X)) -> cons#(X,from(s(X)))
     mark#(from(X)) -> active#(from(mark(X))) ->
     active#(from(X)) -> from#(s(X))
     mark#(from(X)) -> active#(from(mark(X))) ->
     active#(from(X)) -> s#(X)
     mark#(2nd(X)) -> 2nd#(mark(X)) -> 2nd#(active(X)) -> 2nd#(X)
     mark#(2nd(X)) -> 2nd#(mark(X)) -> 2nd#(mark(X)) -> 2nd#(X)
     mark#(2nd(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
     mark#(2nd(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
     mark#(2nd(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
     mark#(2nd(X)) -> mark#(X) -> mark#(from(X)) -> active#(from(mark(X)))
     mark#(2nd(X)) -> mark#(X) -> mark#(from(X)) -> from#(mark(X))
     mark#(2nd(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
     mark#(2nd(X)) -> mark#(X) ->
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     mark#(2nd(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     mark#(2nd(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
     mark#(2nd(X)) -> mark#(X) -> mark#(2nd(X)) -> active#(2nd(mark(X)))
     mark#(2nd(X)) -> mark#(X) -> mark#(2nd(X)) -> 2nd#(mark(X))
     mark#(2nd(X)) -> mark#(X) -> mark#(2nd(X)) -> mark#(X)
     mark#(2nd(X)) -> active#(2nd(mark(X))) ->
     active#(from(X)) -> mark#(cons(X,from(s(X))))
     mark#(2nd(X)) -> active#(2nd(mark(X))) ->
     active#(from(X)) -> cons#(X,from(s(X)))
     mark#(2nd(X)) -> active#(2nd(mark(X))) ->
     active#(from(X)) -> from#(s(X))
     mark#(2nd(X)) -> active#(2nd(mark(X))) ->
     active#(from(X)) -> s#(X)
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(s(X)) -> active#(s(mark(X)))
     mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
     mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(from(X)) -> active#(from(mark(X)))
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(from(X)) -> from#(mark(X))
     mark#(cons(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X)
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(2nd(X)) -> active#(2nd(mark(X)))
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(2nd(X)) -> 2nd#(mark(X))
     mark#(cons(X1,X2)) -> mark#(X1) ->
     mark#(2nd(X)) -> mark#(X)
     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#(from(X)) -> mark#(cons(X,from(s(X))))
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
     active#(from(X)) -> cons#(X,from(s(X)))
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
     active#(from(X)) -> from#(s(X))
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
     active#(from(X)) -> s#(X)
     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)
     from#(mark(X)) -> from#(X) -> from#(active(X)) -> from#(X)
     from#(mark(X)) -> from#(X) -> from#(mark(X)) -> from#(X)
     from#(active(X)) -> from#(X) -> from#(active(X)) -> from#(X)
     from#(active(X)) -> from#(X) -> from#(mark(X)) -> from#(X)
     s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
     s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
     s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
     active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
     mark#(s(X)) -> active#(s(mark(X)))
     active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
     mark#(s(X)) -> s#(mark(X))
     active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
     mark#(s(X)) -> mark#(X)
     active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
     mark#(from(X)) -> active#(from(mark(X)))
     active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
     mark#(from(X)) -> from#(mark(X))
     active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
     mark#(from(X)) -> mark#(X)
     active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
     mark#(cons(X1,X2)) -> mark#(X1)
     active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
     mark#(2nd(X)) -> active#(2nd(mark(X)))
     active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
     mark#(2nd(X)) -> 2nd#(mark(X))
     active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
     mark#(2nd(X)) -> mark#(X)
     active#(from(X)) -> cons#(X,from(s(X))) ->
     cons#(X1,active(X2)) -> cons#(X1,X2)
     active#(from(X)) -> cons#(X,from(s(X))) ->
     cons#(active(X1),X2) -> cons#(X1,X2)
     active#(from(X)) -> cons#(X,from(s(X))) ->
     cons#(X1,mark(X2)) -> cons#(X1,X2)
     active#(from(X)) -> cons#(X,from(s(X))) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     active#(from(X)) -> from#(s(X)) -> from#(active(X)) -> from#(X)
     active#(from(X)) -> from#(s(X)) -> from#(mark(X)) -> from#(X)
     active#(from(X)) -> s#(X) -> s#(active(X)) -> s#(X)
     active#(from(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    SCC Processor:
     #sccs: 5
     #rules: 19
     #arcs: 122/676
     DPs:
      mark#(s(X)) -> mark#(X)
      mark#(2nd(X)) -> mark#(X)
      mark#(2nd(X)) -> active#(2nd(mark(X)))
      active#(from(X)) -> mark#(cons(X,from(s(X))))
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(from(X)) -> mark#(X)
      mark#(from(X)) -> active#(from(mark(X)))
      mark#(s(X)) -> active#(s(mark(X)))
     TRS:
      active(from(X)) -> mark(cons(X,from(s(X))))
      mark(2nd(X)) -> active(2nd(mark(X)))
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(from(X)) -> active(from(mark(X)))
      mark(s(X)) -> active(s(mark(X)))
      2nd(mark(X)) -> 2nd(X)
      2nd(active(X)) -> 2nd(X)
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
     CDG Processor:
      DPs:
       mark#(s(X)) -> mark#(X)
       mark#(2nd(X)) -> mark#(X)
       mark#(2nd(X)) -> active#(2nd(mark(X)))
       active#(from(X)) -> mark#(cons(X,from(s(X))))
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(from(X)) -> mark#(X)
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(s(X)) -> active#(s(mark(X)))
      TRS:
       active(from(X)) -> mark(cons(X,from(s(X))))
       mark(2nd(X)) -> active(2nd(mark(X)))
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(from(X)) -> active(from(mark(X)))
       mark(s(X)) -> active(s(mark(X)))
       2nd(mark(X)) -> 2nd(X)
       2nd(active(X)) -> 2nd(X)
       cons(mark(X1),X2) -> cons(X1,X2)
       cons(X1,mark(X2)) -> cons(X1,X2)
       cons(active(X1),X2) -> cons(X1,X2)
       cons(X1,active(X2)) -> cons(X1,X2)
       from(mark(X)) -> from(X)
       from(active(X)) -> from(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
      graph:
       mark#(s(X)) -> mark#(X) -> mark#(2nd(X)) -> mark#(X)
       mark#(s(X)) -> mark#(X) -> mark#(2nd(X)) -> active#(2nd(mark(X)))
       mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
       mark#(s(X)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
       mark#(s(X)) -> mark#(X) -> mark#(from(X)) -> active#(from(mark(X)))
       mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
       mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
       mark#(from(X)) -> mark#(X) -> mark#(2nd(X)) -> mark#(X)
       mark#(from(X)) -> mark#(X) ->
       mark#(2nd(X)) -> active#(2nd(mark(X)))
       mark#(from(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
       mark#(from(X)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(from(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
       mark#(from(X)) -> mark#(X) ->
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(from(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
       mark#(from(X)) -> mark#(X) ->
       mark#(s(X)) -> active#(s(mark(X)))
       mark#(from(X)) -> active#(from(mark(X))) ->
       active#(from(X)) -> mark#(cons(X,from(s(X))))
       mark#(2nd(X)) -> mark#(X) -> mark#(2nd(X)) -> mark#(X)
       mark#(2nd(X)) -> mark#(X) -> mark#(2nd(X)) -> active#(2nd(mark(X)))
       mark#(2nd(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
       mark#(2nd(X)) -> mark#(X) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(2nd(X)) -> mark#(X) -> mark#(from(X)) -> mark#(X)
       mark#(2nd(X)) -> mark#(X) ->
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(2nd(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
       mark#(2nd(X)) -> mark#(X) ->
       mark#(s(X)) -> active#(s(mark(X)))
       mark#(cons(X1,X2)) -> mark#(X1) -> mark#(2nd(X)) -> mark#(X)
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(2nd(X)) -> active#(2nd(mark(X)))
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(cons(X1,X2)) -> mark#(X1) -> mark#(from(X)) -> mark#(X)
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(from(X)) -> active#(from(mark(X)))
       mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
       mark#(cons(X1,X2)) -> mark#(X1) ->
       mark#(s(X)) -> active#(s(mark(X)))
       active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
       mark#(cons(X1,X2)) -> mark#(X1)
       active#(from(X)) -> mark#(cons(X,from(s(X)))) ->
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      SCC Processor:
       #sccs: 1
       #rules: 6
       #arcs: 35/81
       DPs:
        mark#(s(X)) -> mark#(X)
        mark#(from(X)) -> active#(from(mark(X)))
        active#(from(X)) -> mark#(cons(X,from(s(X))))
        mark#(cons(X1,X2)) -> mark#(X1)
        mark#(from(X)) -> mark#(X)
        mark#(2nd(X)) -> mark#(X)
       TRS:
        active(from(X)) -> mark(cons(X,from(s(X))))
        mark(2nd(X)) -> active(2nd(mark(X)))
        mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
        mark(from(X)) -> active(from(mark(X)))
        mark(s(X)) -> active(s(mark(X)))
        2nd(mark(X)) -> 2nd(X)
        2nd(active(X)) -> 2nd(X)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
       KBO Processor:
        argument filtering:
         pi(cons) = [0]
         pi(2nd) = [0]
         pi(active) = 0
         pi(mark) = 0
         pi(from) = [0]
         pi(s) = [0]
         pi(active#) = 0
         pi(mark#) = 0
        usable rules:
         active(from(X)) -> mark(cons(X,from(s(X))))
         mark(2nd(X)) -> active(2nd(mark(X)))
         mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
         mark(from(X)) -> active(from(mark(X)))
         mark(s(X)) -> active(s(mark(X)))
         2nd(mark(X)) -> 2nd(X)
         2nd(active(X)) -> 2nd(X)
         cons(mark(X1),X2) -> cons(X1,X2)
         cons(X1,mark(X2)) -> cons(X1,X2)
         cons(active(X1),X2) -> cons(X1,X2)
         cons(X1,active(X2)) -> cons(X1,X2)
         from(mark(X)) -> from(X)
         from(active(X)) -> from(X)
         s(mark(X)) -> s(X)
         s(active(X)) -> s(X)
        weight function:
         w0 = 1
         w(mark#) = w(active#) = w(s) = w(from) = w(2nd) = 1
         w(mark) = w(active) = w(cons) = 0
        precedence:
         mark# > active# ~ s ~ from ~ mark ~ active ~ 2nd ~ cons
        problem:
         DPs:
          mark#(from(X)) -> active#(from(mark(X)))
         TRS:
          active(from(X)) -> mark(cons(X,from(s(X))))
          mark(2nd(X)) -> active(2nd(mark(X)))
          mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
          mark(from(X)) -> active(from(mark(X)))
          mark(s(X)) -> active(s(mark(X)))
          2nd(mark(X)) -> 2nd(X)
          2nd(active(X)) -> 2nd(X)
          cons(mark(X1),X2) -> cons(X1,X2)
          cons(X1,mark(X2)) -> cons(X1,X2)
          cons(active(X1),X2) -> cons(X1,X2)
          cons(X1,active(X2)) -> cons(X1,X2)
          from(mark(X)) -> from(X)
          from(active(X)) -> from(X)
          s(mark(X)) -> s(X)
          s(active(X)) -> s(X)
        Restore Modifier:
         DPs:
          mark#(from(X)) -> active#(from(mark(X)))
         TRS:
          active(from(X)) -> mark(cons(X,from(s(X))))
          mark(2nd(X)) -> active(2nd(mark(X)))
          mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
          mark(from(X)) -> active(from(mark(X)))
          mark(s(X)) -> active(s(mark(X)))
          2nd(mark(X)) -> 2nd(X)
          2nd(active(X)) -> 2nd(X)
          cons(mark(X1),X2) -> cons(X1,X2)
          cons(X1,mark(X2)) -> cons(X1,X2)
          cons(active(X1),X2) -> cons(X1,X2)
          cons(X1,active(X2)) -> cons(X1,X2)
          from(mark(X)) -> from(X)
          from(active(X)) -> from(X)
          s(mark(X)) -> s(X)
          s(active(X)) -> s(X)
         SCC Processor:
          #sccs: 0
          #rules: 0
          #arcs: 22/1
          
     
     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(from(X)) -> mark(cons(X,from(s(X))))
      mark(2nd(X)) -> active(2nd(mark(X)))
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(from(X)) -> active(from(mark(X)))
      mark(s(X)) -> active(s(mark(X)))
      2nd(mark(X)) -> 2nd(X)
      2nd(active(X)) -> 2nd(X)
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(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(from(X)) -> mark(cons(X,from(s(X))))
        mark(2nd(X)) -> active(2nd(mark(X)))
        mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
        mark(from(X)) -> active(from(mark(X)))
        mark(s(X)) -> active(s(mark(X)))
        2nd(mark(X)) -> 2nd(X)
        2nd(active(X)) -> 2nd(X)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
      Subterm Criterion Processor:
       simple projection:
        pi(cons#) = 0
       problem:
        DPs:
         
        TRS:
         active(from(X)) -> mark(cons(X,from(s(X))))
         mark(2nd(X)) -> active(2nd(mark(X)))
         mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
         mark(from(X)) -> active(from(mark(X)))
         mark(s(X)) -> active(s(mark(X)))
         2nd(mark(X)) -> 2nd(X)
         2nd(active(X)) -> 2nd(X)
         cons(mark(X1),X2) -> cons(X1,X2)
         cons(X1,mark(X2)) -> cons(X1,X2)
         cons(active(X1),X2) -> cons(X1,X2)
         cons(X1,active(X2)) -> cons(X1,X2)
         from(mark(X)) -> from(X)
         from(active(X)) -> from(X)
         s(mark(X)) -> s(X)
         s(active(X)) -> s(X)
       Qed
     
     DPs:
      from#(mark(X)) -> from#(X)
      from#(active(X)) -> from#(X)
     TRS:
      active(from(X)) -> mark(cons(X,from(s(X))))
      mark(2nd(X)) -> active(2nd(mark(X)))
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(from(X)) -> active(from(mark(X)))
      mark(s(X)) -> active(s(mark(X)))
      2nd(mark(X)) -> 2nd(X)
      2nd(active(X)) -> 2nd(X)
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
     Subterm Criterion Processor:
      simple projection:
       pi(from#) = 0
      problem:
       DPs:
        
       TRS:
        active(from(X)) -> mark(cons(X,from(s(X))))
        mark(2nd(X)) -> active(2nd(mark(X)))
        mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
        mark(from(X)) -> active(from(mark(X)))
        mark(s(X)) -> active(s(mark(X)))
        2nd(mark(X)) -> 2nd(X)
        2nd(active(X)) -> 2nd(X)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
      Qed
     
     DPs:
      s#(mark(X)) -> s#(X)
      s#(active(X)) -> s#(X)
     TRS:
      active(from(X)) -> mark(cons(X,from(s(X))))
      mark(2nd(X)) -> active(2nd(mark(X)))
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(from(X)) -> active(from(mark(X)))
      mark(s(X)) -> active(s(mark(X)))
      2nd(mark(X)) -> 2nd(X)
      2nd(active(X)) -> 2nd(X)
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
     Subterm Criterion Processor:
      simple projection:
       pi(s#) = 0
      problem:
       DPs:
        
       TRS:
        active(from(X)) -> mark(cons(X,from(s(X))))
        mark(2nd(X)) -> active(2nd(mark(X)))
        mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
        mark(from(X)) -> active(from(mark(X)))
        mark(s(X)) -> active(s(mark(X)))
        2nd(mark(X)) -> 2nd(X)
        2nd(active(X)) -> 2nd(X)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
      Qed
     
     DPs:
      2nd#(mark(X)) -> 2nd#(X)
      2nd#(active(X)) -> 2nd#(X)
     TRS:
      active(from(X)) -> mark(cons(X,from(s(X))))
      mark(2nd(X)) -> active(2nd(mark(X)))
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(from(X)) -> active(from(mark(X)))
      mark(s(X)) -> active(s(mark(X)))
      2nd(mark(X)) -> 2nd(X)
      2nd(active(X)) -> 2nd(X)
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      from(mark(X)) -> from(X)
      from(active(X)) -> from(X)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
     Subterm Criterion Processor:
      simple projection:
       pi(2nd#) = 0
      problem:
       DPs:
        
       TRS:
        active(from(X)) -> mark(cons(X,from(s(X))))
        mark(2nd(X)) -> active(2nd(mark(X)))
        mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
        mark(from(X)) -> active(from(mark(X)))
        mark(s(X)) -> active(s(mark(X)))
        2nd(mark(X)) -> 2nd(X)
        2nd(active(X)) -> 2nd(X)
        cons(mark(X1),X2) -> cons(X1,X2)
        cons(X1,mark(X2)) -> cons(X1,X2)
        cons(active(X1),X2) -> cons(X1,X2)
        cons(X1,active(X2)) -> cons(X1,X2)
        from(mark(X)) -> from(X)
        from(active(X)) -> from(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
      Qed