YES

Problem:
 active(f(0())) -> mark(cons(0(),f(s(0()))))
 active(f(s(0()))) -> mark(f(p(s(0()))))
 active(p(s(X))) -> mark(X)
 mark(f(X)) -> active(f(mark(X)))
 mark(0()) -> active(0())
 mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
 mark(s(X)) -> active(s(mark(X)))
 mark(p(X)) -> active(p(mark(X)))
 f(mark(X)) -> f(X)
 f(active(X)) -> f(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)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 p(mark(X)) -> p(X)
 p(active(X)) -> p(X)

Proof:
 Matrix Interpretation Processor: dim=3
  
  interpretation:
             [1 1 0]  
   [p](x0) = [0 0 0]x0
             [1 1 0]  ,
   
                [1 1 0]  
   [mark](x0) = [0 0 0]x0
                [0 0 1]  ,
   
                    [1 1 0]     [1 0 0]  
   [cons](x0, x1) = [0 0 1]x0 + [0 0 1]x1
                    [0 0 0]     [1 0 0]  ,
   
             [1 1 0]     [0]
   [s](x0) = [0 0 1]x0 + [0]
             [0 0 0]     [1],
   
                  [1 1 0]  
   [active](x0) = [0 0 0]x0
                  [0 0 1]  ,
   
             [1 1 0]  
   [f](x0) = [0 0 1]x0
             [0 0 0]  ,
   
         [0]
   [0] = [0]
         [0]
  orientation:
                    [0]    [0]                            
   active(f(0())) = [0] >= [0] = mark(cons(0(),f(s(0()))))
                    [0]    [0]                            
   
                       [1]    [0]                     
   active(f(s(0()))) = [0] >= [0] = mark(f(p(s(0()))))
                       [0]    [0]                     
   
                     [1 1 1]     [1 1 0]           
   active(p(s(X))) = [0 0 0]X >= [0 0 0]X = mark(X)
                     [1 1 1]     [0 0 1]           
   
                [1 1 1]     [1 1 1]                      
   mark(f(X)) = [0 0 0]X >= [0 0 0]X = active(f(mark(X)))
                [0 0 0]     [0 0 0]                      
   
               [0]    [0]              
   mark(0()) = [0] >= [0] = active(0())
               [0]    [0]              
   
                       [1 1 1]     [1 0 1]      [1 1 1]     [1 0 1]                              
   mark(cons(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = active(cons(mark(X1),X2))
                       [0 0 0]     [1 0 0]      [0 0 0]     [1 0 0]                              
   
                [1 1 1]    [0]    [1 1 1]    [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 0]                      
   mark(p(X)) = [0 0 0]X >= [0 0 0]X = active(p(mark(X)))
                [1 1 0]     [1 1 0]                      
   
                [1 1 0]     [1 1 0]        
   f(mark(X)) = [0 0 1]X >= [0 0 1]X = f(X)
                [0 0 0]     [0 0 0]        
   
                  [1 1 0]     [1 1 0]        
   f(active(X)) = [0 0 1]X >= [0 0 1]X = f(X)
                  [0 0 0]     [0 0 0]        
   
                       [1 1 0]     [1 0 0]      [1 1 0]     [1 0 0]                
   cons(mark(X1),X2) = [0 0 1]X1 + [0 0 1]X2 >= [0 0 1]X1 + [0 0 1]X2 = cons(X1,X2)
                       [0 0 0]     [1 0 0]      [0 0 0]     [1 0 0]                
   
                       [1 1 0]     [1 1 0]      [1 1 0]     [1 0 0]                
   cons(X1,mark(X2)) = [0 0 1]X1 + [0 0 1]X2 >= [0 0 1]X1 + [0 0 1]X2 = cons(X1,X2)
                       [0 0 0]     [1 1 0]      [0 0 0]     [1 0 0]                
   
                         [1 1 0]     [1 0 0]      [1 1 0]     [1 0 0]                
   cons(active(X1),X2) = [0 0 1]X1 + [0 0 1]X2 >= [0 0 1]X1 + [0 0 1]X2 = cons(X1,X2)
                         [0 0 0]     [1 0 0]      [0 0 0]     [1 0 0]                
   
                         [1 1 0]     [1 1 0]      [1 1 0]     [1 0 0]                
   cons(X1,active(X2)) = [0 0 1]X1 + [0 0 1]X2 >= [0 0 1]X1 + [0 0 1]X2 = cons(X1,X2)
                         [0 0 0]     [1 1 0]      [0 0 0]     [1 0 0]                
   
                [1 1 0]    [0]    [1 1 0]    [0]       
   s(mark(X)) = [0 0 1]X + [0] >= [0 0 1]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 1]X + [0] >= [0 0 1]X + [0] = s(X)
                  [0 0 0]    [1]    [0 0 0]    [1]       
   
                [1 1 0]     [1 1 0]        
   p(mark(X)) = [0 0 0]X >= [0 0 0]X = p(X)
                [1 1 0]     [1 1 0]        
   
                  [1 1 0]     [1 1 0]        
   p(active(X)) = [0 0 0]X >= [0 0 0]X = p(X)
                  [1 1 0]     [1 1 0]        
  problem:
   active(f(0())) -> mark(cons(0(),f(s(0()))))
   active(p(s(X))) -> mark(X)
   mark(f(X)) -> active(f(mark(X)))
   mark(0()) -> active(0())
   mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
   mark(s(X)) -> active(s(mark(X)))
   mark(p(X)) -> active(p(mark(X)))
   f(mark(X)) -> f(X)
   f(active(X)) -> f(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)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   p(mark(X)) -> p(X)
   p(active(X)) -> p(X)
  Matrix Interpretation Processor: dim=3
   
   interpretation:
              [1 1 1]     [1]
    [p](x0) = [1 0 0]x0 + [0]
              [0 0 0]     [0],
    
                 [1 0 0]  
    [mark](x0) = [0 0 0]x0
                 [0 1 1]  ,
    
                     [1 1 1]     [1 1 1]  
    [cons](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                     [0 0 0]     [0 0 0]  ,
    
              [1 1 1]  
    [s](x0) = [0 0 0]x0
              [0 0 0]  ,
    
                   [1 0 0]  
    [active](x0) = [0 0 1]x0
                   [0 1 0]  ,
    
              [1 0 0]  
    [f](x0) = [0 0 0]x0
              [0 0 0]  ,
    
          [0]
    [0] = [0]
          [0]
   orientation:
                     [0]    [0]                            
    active(f(0())) = [0] >= [0] = mark(cons(0(),f(s(0()))))
                     [0]    [0]                            
    
                      [1 1 1]    [1]    [1 0 0]           
    active(p(s(X))) = [0 0 0]X + [0] >= [0 0 0]X = mark(X)
                      [1 1 1]    [0]    [0 1 1]           
    
                 [1 0 0]     [1 0 0]                      
    mark(f(X)) = [0 0 0]X >= [0 0 0]X = active(f(mark(X)))
                 [0 0 0]     [0 0 0]                      
    
                [0]    [0]              
    mark(0()) = [0] >= [0] = active(0())
                [0]    [0]              
    
                        [1 1 1]     [1 1 1]      [1 1 1]     [1 1 1]                              
    mark(cons(X1,X2)) = [0 0 0]X1 + [0 0 0]X2 >= [0 0 0]X1 + [0 0 0]X2 = active(cons(mark(X1),X2))
                        [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]                              
    
                 [1 1 1]     [1 1 1]                      
    mark(s(X)) = [0 0 0]X >= [0 0 0]X = active(s(mark(X)))
                 [0 0 0]     [0 0 0]                      
    
                 [1 1 1]    [1]    [1 1 1]    [1]                     
    mark(p(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(p(mark(X)))
                 [1 0 0]    [0]    [1 0 0]    [0]                     
    
                 [1 0 0]     [1 0 0]        
    f(mark(X)) = [0 0 0]X >= [0 0 0]X = f(X)
                 [0 0 0]     [0 0 0]        
    
                   [1 0 0]     [1 0 0]        
    f(active(X)) = [0 0 0]X >= [0 0 0]X = f(X)
                   [0 0 0]     [0 0 0]        
    
                        [1 1 1]     [1 1 1]      [1 1 1]     [1 1 1]                
    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 1]     [1 1 1]      [1 1 1]     [1 1 1]                
    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 1]     [1 1 1]      [1 1 1]     [1 1 1]                
    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 1]     [1 1 1]      [1 1 1]     [1 1 1]                
    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 1]     [1 1 1]        
    s(mark(X)) = [0 0 0]X >= [0 0 0]X = s(X)
                 [0 0 0]     [0 0 0]        
    
                   [1 1 1]     [1 1 1]        
    s(active(X)) = [0 0 0]X >= [0 0 0]X = s(X)
                   [0 0 0]     [0 0 0]        
    
                 [1 1 1]    [1]    [1 1 1]    [1]       
    p(mark(X)) = [1 0 0]X + [0] >= [1 0 0]X + [0] = p(X)
                 [0 0 0]    [0]    [0 0 0]    [0]       
    
                   [1 1 1]    [1]    [1 1 1]    [1]       
    p(active(X)) = [1 0 0]X + [0] >= [1 0 0]X + [0] = p(X)
                   [0 0 0]    [0]    [0 0 0]    [0]       
   problem:
    active(f(0())) -> mark(cons(0(),f(s(0()))))
    mark(f(X)) -> active(f(mark(X)))
    mark(0()) -> active(0())
    mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
    mark(s(X)) -> active(s(mark(X)))
    mark(p(X)) -> active(p(mark(X)))
    f(mark(X)) -> f(X)
    f(active(X)) -> f(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)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    p(mark(X)) -> p(X)
    p(active(X)) -> p(X)
   DP Processor:
    DPs:
     active#(f(0())) -> s#(0())
     active#(f(0())) -> f#(s(0()))
     active#(f(0())) -> cons#(0(),f(s(0())))
     active#(f(0())) -> mark#(cons(0(),f(s(0()))))
     mark#(f(X)) -> mark#(X)
     mark#(f(X)) -> f#(mark(X))
     mark#(f(X)) -> active#(f(mark(X)))
     mark#(0()) -> active#(0())
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     mark#(s(X)) -> mark#(X)
     mark#(s(X)) -> s#(mark(X))
     mark#(s(X)) -> active#(s(mark(X)))
     mark#(p(X)) -> mark#(X)
     mark#(p(X)) -> p#(mark(X))
     mark#(p(X)) -> active#(p(mark(X)))
     f#(mark(X)) -> f#(X)
     f#(active(X)) -> f#(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)
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
     p#(mark(X)) -> p#(X)
     p#(active(X)) -> p#(X)
    TRS:
     active(f(0())) -> mark(cons(0(),f(s(0()))))
     mark(f(X)) -> active(f(mark(X)))
     mark(0()) -> active(0())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(s(X)) -> active(s(mark(X)))
     mark(p(X)) -> active(p(mark(X)))
     f(mark(X)) -> f(X)
     f(active(X)) -> f(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)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     p(mark(X)) -> p(X)
     p(active(X)) -> p(X)
    TDG Processor:
     DPs:
      active#(f(0())) -> s#(0())
      active#(f(0())) -> f#(s(0()))
      active#(f(0())) -> cons#(0(),f(s(0())))
      active#(f(0())) -> mark#(cons(0(),f(s(0()))))
      mark#(f(X)) -> mark#(X)
      mark#(f(X)) -> f#(mark(X))
      mark#(f(X)) -> active#(f(mark(X)))
      mark#(0()) -> active#(0())
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(s(X)) -> mark#(X)
      mark#(s(X)) -> s#(mark(X))
      mark#(s(X)) -> active#(s(mark(X)))
      mark#(p(X)) -> mark#(X)
      mark#(p(X)) -> p#(mark(X))
      mark#(p(X)) -> active#(p(mark(X)))
      f#(mark(X)) -> f#(X)
      f#(active(X)) -> f#(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)
      s#(mark(X)) -> s#(X)
      s#(active(X)) -> s#(X)
      p#(mark(X)) -> p#(X)
      p#(active(X)) -> p#(X)
     TRS:
      active(f(0())) -> mark(cons(0(),f(s(0()))))
      mark(f(X)) -> active(f(mark(X)))
      mark(0()) -> active(0())
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(s(X)) -> active(s(mark(X)))
      mark(p(X)) -> active(p(mark(X)))
      f(mark(X)) -> f(X)
      f(active(X)) -> f(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)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      p(mark(X)) -> p(X)
      p(active(X)) -> p(X)
     graph:
      p#(mark(X)) -> p#(X) -> p#(active(X)) -> p#(X)
      p#(mark(X)) -> p#(X) -> p#(mark(X)) -> p#(X)
      p#(active(X)) -> p#(X) -> p#(active(X)) -> p#(X)
      p#(active(X)) -> p#(X) -> p#(mark(X)) -> p#(X)
      mark#(p(X)) -> p#(mark(X)) -> p#(active(X)) -> p#(X)
      mark#(p(X)) -> p#(mark(X)) -> p#(mark(X)) -> p#(X)
      mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
      mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> p#(mark(X))
      mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
      mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
      mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
      mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
      mark#(p(X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(p(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
      mark#(p(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
      mark#(p(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      mark#(p(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X)))
      mark#(p(X)) -> mark#(X) -> mark#(f(X)) -> f#(mark(X))
      mark#(p(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X)
      mark#(p(X)) -> active#(p(mark(X))) ->
      active#(f(0())) -> mark#(cons(0(),f(s(0()))))
      mark#(p(X)) -> active#(p(mark(X))) ->
      active#(f(0())) -> cons#(0(),f(s(0())))
      mark#(p(X)) -> active#(p(mark(X))) ->
      active#(f(0())) -> f#(s(0()))
      mark#(p(X)) -> active#(p(mark(X))) ->
      active#(f(0())) -> s#(0())
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(p(X)) -> active#(p(mark(X)))
      mark#(cons(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> p#(mark(X))
      mark#(cons(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> mark#(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#(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#(0()) -> active#(0())
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(f(X)) -> active#(f(mark(X)))
      mark#(cons(X1,X2)) -> mark#(X1) -> mark#(f(X)) -> f#(mark(X))
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(f(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#(f(0())) -> mark#(cons(0(),f(s(0()))))
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
      active#(f(0())) -> cons#(0(),f(s(0())))
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
      active#(f(0())) -> f#(s(0()))
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
      active#(f(0())) -> s#(0())
      mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
      mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> p#(mark(X))
      mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> mark#(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#(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#(0()) -> active#(0())
      mark#(s(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X)))
      mark#(s(X)) -> mark#(X) -> mark#(f(X)) -> f#(mark(X))
      mark#(s(X)) -> mark#(X) -> mark#(f(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#(f(0())) -> mark#(cons(0(),f(s(0()))))
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(f(0())) -> cons#(0(),f(s(0())))
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(f(0())) -> f#(s(0()))
      mark#(s(X)) -> active#(s(mark(X))) -> active#(f(0())) -> s#(0())
      mark#(f(X)) -> mark#(X) -> mark#(p(X)) -> active#(p(mark(X)))
      mark#(f(X)) -> mark#(X) -> mark#(p(X)) -> p#(mark(X))
      mark#(f(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
      mark#(f(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
      mark#(f(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
      mark#(f(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
      mark#(f(X)) -> mark#(X) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      mark#(f(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
      mark#(f(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
      mark#(f(X)) -> mark#(X) -> mark#(0()) -> active#(0())
      mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X)))
      mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> f#(mark(X))
      mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X)
      mark#(f(X)) -> f#(mark(X)) -> f#(active(X)) -> f#(X)
      mark#(f(X)) -> f#(mark(X)) -> f#(mark(X)) -> f#(X)
      mark#(f(X)) -> active#(f(mark(X))) ->
      active#(f(0())) -> mark#(cons(0(),f(s(0()))))
      mark#(f(X)) -> active#(f(mark(X))) ->
      active#(f(0())) -> cons#(0(),f(s(0())))
      mark#(f(X)) -> active#(f(mark(X))) ->
      active#(f(0())) -> f#(s(0()))
      mark#(f(X)) -> active#(f(mark(X))) -> active#(f(0())) -> s#(0())
      mark#(0()) -> active#(0()) ->
      active#(f(0())) -> mark#(cons(0(),f(s(0()))))
      mark#(0()) -> active#(0()) ->
      active#(f(0())) -> cons#(0(),f(s(0())))
      mark#(0()) -> active#(0()) -> active#(f(0())) -> f#(s(0()))
      mark#(0()) -> active#(0()) -> active#(f(0())) -> s#(0())
      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)
      f#(mark(X)) -> f#(X) -> f#(active(X)) -> f#(X)
      f#(mark(X)) -> f#(X) -> f#(mark(X)) -> f#(X)
      f#(active(X)) -> f#(X) -> f#(active(X)) -> f#(X)
      f#(active(X)) -> f#(X) -> f#(mark(X)) -> f#(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#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
      mark#(p(X)) -> active#(p(mark(X)))
      active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
      mark#(p(X)) -> p#(mark(X))
      active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
      mark#(p(X)) -> mark#(X)
      active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
      mark#(s(X)) -> active#(s(mark(X)))
      active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
      mark#(s(X)) -> s#(mark(X))
      active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
      mark#(s(X)) -> mark#(X)
      active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
      mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
      active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
      mark#(0()) -> active#(0())
      active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
      mark#(f(X)) -> active#(f(mark(X)))
      active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
      mark#(f(X)) -> f#(mark(X))
      active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
      mark#(f(X)) -> mark#(X)
      active#(f(0())) -> cons#(0(),f(s(0()))) ->
      cons#(X1,active(X2)) -> cons#(X1,X2)
      active#(f(0())) -> cons#(0(),f(s(0()))) ->
      cons#(active(X1),X2) -> cons#(X1,X2)
      active#(f(0())) -> cons#(0(),f(s(0()))) ->
      cons#(X1,mark(X2)) -> cons#(X1,X2)
      active#(f(0())) -> cons#(0(),f(s(0()))) ->
      cons#(mark(X1),X2) -> cons#(X1,X2)
      active#(f(0())) -> f#(s(0())) -> f#(active(X)) -> f#(X)
      active#(f(0())) -> f#(s(0())) -> f#(mark(X)) -> f#(X)
      active#(f(0())) -> s#(0()) -> s#(active(X)) -> s#(X)
      active#(f(0())) -> s#(0()) -> s#(mark(X)) -> s#(X)
     SCC Processor:
      #sccs: 5
      #rules: 20
      #arcs: 131/729
      DPs:
       mark#(p(X)) -> mark#(X)
       mark#(f(X)) -> mark#(X)
       mark#(f(X)) -> active#(f(mark(X)))
       active#(f(0())) -> mark#(cons(0(),f(s(0()))))
       mark#(0()) -> active#(0())
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       mark#(s(X)) -> mark#(X)
       mark#(s(X)) -> active#(s(mark(X)))
       mark#(p(X)) -> active#(p(mark(X)))
      TRS:
       active(f(0())) -> mark(cons(0(),f(s(0()))))
       mark(f(X)) -> active(f(mark(X)))
       mark(0()) -> active(0())
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(s(X)) -> active(s(mark(X)))
       mark(p(X)) -> active(p(mark(X)))
       f(mark(X)) -> f(X)
       f(active(X)) -> f(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)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       p(mark(X)) -> p(X)
       p(active(X)) -> p(X)
      EDG Processor:
       DPs:
        mark#(p(X)) -> mark#(X)
        mark#(f(X)) -> mark#(X)
        mark#(f(X)) -> active#(f(mark(X)))
        active#(f(0())) -> mark#(cons(0(),f(s(0()))))
        mark#(0()) -> active#(0())
        mark#(cons(X1,X2)) -> mark#(X1)
        mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
        mark#(s(X)) -> mark#(X)
        mark#(s(X)) -> active#(s(mark(X)))
        mark#(p(X)) -> active#(p(mark(X)))
       TRS:
        active(f(0())) -> mark(cons(0(),f(s(0()))))
        mark(f(X)) -> active(f(mark(X)))
        mark(0()) -> active(0())
        mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
        mark(s(X)) -> active(s(mark(X)))
        mark(p(X)) -> active(p(mark(X)))
        f(mark(X)) -> f(X)
        f(active(X)) -> f(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)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
        p(mark(X)) -> p(X)
        p(active(X)) -> p(X)
       graph:
        mark#(p(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X)
        mark#(p(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X)))
        mark#(p(X)) -> mark#(X) -> mark#(0()) -> active#(0())
        mark#(p(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
        mark#(p(X)) -> mark#(X) ->
        mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
        mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
        mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
        mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
        mark#(p(X)) -> mark#(X) ->
        mark#(p(X)) -> active#(p(mark(X)))
        mark#(p(X)) -> active#(p(mark(X))) ->
        active#(f(0())) -> mark#(cons(0(),f(s(0()))))
        mark#(cons(X1,X2)) -> mark#(X1) -> mark#(f(X)) -> mark#(X)
        mark#(cons(X1,X2)) -> mark#(X1) ->
        mark#(f(X)) -> active#(f(mark(X)))
        mark#(cons(X1,X2)) -> mark#(X1) ->
        mark#(0()) -> active#(0())
        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#(s(X)) -> mark#(X)
        mark#(cons(X1,X2)) -> mark#(X1) ->
        mark#(s(X)) -> active#(s(mark(X)))
        mark#(cons(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> mark#(X)
        mark#(cons(X1,X2)) -> mark#(X1) ->
        mark#(p(X)) -> active#(p(mark(X)))
        mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
        active#(f(0())) -> mark#(cons(0(),f(s(0()))))
        mark#(s(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X)
        mark#(s(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X)))
        mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
        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#(s(X)) -> mark#(X)
        mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
        mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
        mark#(s(X)) -> mark#(X) ->
        mark#(p(X)) -> active#(p(mark(X)))
        mark#(s(X)) -> active#(s(mark(X))) ->
        active#(f(0())) -> mark#(cons(0(),f(s(0()))))
        mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X)
        mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X)))
        mark#(f(X)) -> mark#(X) -> mark#(0()) -> active#(0())
        mark#(f(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
        mark#(f(X)) -> mark#(X) ->
        mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
        mark#(f(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
        mark#(f(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
        mark#(f(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X)
        mark#(f(X)) -> mark#(X) ->
        mark#(p(X)) -> active#(p(mark(X)))
        mark#(f(X)) -> active#(f(mark(X))) ->
        active#(f(0())) -> mark#(cons(0(),f(s(0()))))
        active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
        mark#(cons(X1,X2)) -> mark#(X1)
        active#(f(0())) -> mark#(cons(0(),f(s(0())))) ->
        mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       SCC Processor:
        #sccs: 1
        #rules: 9
        #arcs: 42/100
        DPs:
         mark#(p(X)) -> mark#(X)
         mark#(p(X)) -> active#(p(mark(X)))
         active#(f(0())) -> mark#(cons(0(),f(s(0()))))
         mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
         mark#(cons(X1,X2)) -> mark#(X1)
         mark#(s(X)) -> active#(s(mark(X)))
         mark#(s(X)) -> mark#(X)
         mark#(f(X)) -> active#(f(mark(X)))
         mark#(f(X)) -> mark#(X)
        TRS:
         active(f(0())) -> mark(cons(0(),f(s(0()))))
         mark(f(X)) -> active(f(mark(X)))
         mark(0()) -> active(0())
         mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
         mark(s(X)) -> active(s(mark(X)))
         mark(p(X)) -> active(p(mark(X)))
         f(mark(X)) -> f(X)
         f(active(X)) -> f(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)
         s(mark(X)) -> s(X)
         s(active(X)) -> s(X)
         p(mark(X)) -> p(X)
         p(active(X)) -> p(X)
        Arctic Interpretation Processor:
         dimension: 1
         interpretation:
          [mark#](x0) = x0 + 0,
          
          [active#](x0) = x0 + 0,
          
          [p](x0) = x0 + 0,
          
          [mark](x0) = x0 + 0,
          
          [cons](x0, x1) = x0 + 0,
          
          [s](x0) = x0 + 0,
          
          [active](x0) = x0 + 0,
          
          [f](x0) = 1x0 + 1,
          
          [0] = 6
         orientation:
          mark#(p(X)) = X + 0 >= X + 0 = mark#(X)
          
          mark#(p(X)) = X + 0 >= X + 0 = active#(p(mark(X)))
          
          active#(f(0())) = 7 >= 6 = mark#(cons(0(),f(s(0()))))
          
          mark#(cons(X1,X2)) = X1 + 0 >= X1 + 0 = active#(cons(mark(X1),X2))
          
          mark#(cons(X1,X2)) = X1 + 0 >= X1 + 0 = mark#(X1)
          
          mark#(s(X)) = X + 0 >= X + 0 = active#(s(mark(X)))
          
          mark#(s(X)) = X + 0 >= X + 0 = mark#(X)
          
          mark#(f(X)) = 1X + 1 >= 1X + 1 = active#(f(mark(X)))
          
          mark#(f(X)) = 1X + 1 >= X + 0 = mark#(X)
          
          active(f(0())) = 7 >= 6 = mark(cons(0(),f(s(0()))))
          
          mark(f(X)) = 1X + 1 >= 1X + 1 = active(f(mark(X)))
          
          mark(0()) = 6 >= 6 = active(0())
          
          mark(cons(X1,X2)) = X1 + 0 >= X1 + 0 = active(cons(mark(X1),X2))
          
          mark(s(X)) = X + 0 >= X + 0 = active(s(mark(X)))
          
          mark(p(X)) = X + 0 >= X + 0 = active(p(mark(X)))
          
          f(mark(X)) = 1X + 1 >= 1X + 1 = f(X)
          
          f(active(X)) = 1X + 1 >= 1X + 1 = f(X)
          
          cons(mark(X1),X2) = X1 + 0 >= X1 + 0 = cons(X1,X2)
          
          cons(X1,mark(X2)) = X1 + 0 >= X1 + 0 = cons(X1,X2)
          
          cons(active(X1),X2) = X1 + 0 >= X1 + 0 = cons(X1,X2)
          
          cons(X1,active(X2)) = X1 + 0 >= X1 + 0 = cons(X1,X2)
          
          s(mark(X)) = X + 0 >= X + 0 = s(X)
          
          s(active(X)) = X + 0 >= X + 0 = s(X)
          
          p(mark(X)) = X + 0 >= X + 0 = p(X)
          
          p(active(X)) = X + 0 >= X + 0 = p(X)
         problem:
          DPs:
           mark#(p(X)) -> mark#(X)
           mark#(p(X)) -> active#(p(mark(X)))
           mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
           mark#(cons(X1,X2)) -> mark#(X1)
           mark#(s(X)) -> active#(s(mark(X)))
           mark#(s(X)) -> mark#(X)
           mark#(f(X)) -> active#(f(mark(X)))
          TRS:
           active(f(0())) -> mark(cons(0(),f(s(0()))))
           mark(f(X)) -> active(f(mark(X)))
           mark(0()) -> active(0())
           mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
           mark(s(X)) -> active(s(mark(X)))
           mark(p(X)) -> active(p(mark(X)))
           f(mark(X)) -> f(X)
           f(active(X)) -> f(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)
           s(mark(X)) -> s(X)
           s(active(X)) -> s(X)
           p(mark(X)) -> p(X)
           p(active(X)) -> p(X)
         SCC Processor:
          #sccs: 1
          #rules: 3
          #arcs: 38/49
          DPs:
           mark#(p(X)) -> mark#(X)
           mark#(s(X)) -> mark#(X)
           mark#(cons(X1,X2)) -> mark#(X1)
          TRS:
           active(f(0())) -> mark(cons(0(),f(s(0()))))
           mark(f(X)) -> active(f(mark(X)))
           mark(0()) -> active(0())
           mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
           mark(s(X)) -> active(s(mark(X)))
           mark(p(X)) -> active(p(mark(X)))
           f(mark(X)) -> f(X)
           f(active(X)) -> f(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)
           s(mark(X)) -> s(X)
           s(active(X)) -> s(X)
           p(mark(X)) -> p(X)
           p(active(X)) -> p(X)
          Subterm Criterion Processor:
           simple projection:
            pi(mark#) = 0
           problem:
            DPs:
             
            TRS:
             active(f(0())) -> mark(cons(0(),f(s(0()))))
             mark(f(X)) -> active(f(mark(X)))
             mark(0()) -> active(0())
             mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
             mark(s(X)) -> active(s(mark(X)))
             mark(p(X)) -> active(p(mark(X)))
             f(mark(X)) -> f(X)
             f(active(X)) -> f(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)
             s(mark(X)) -> s(X)
             s(active(X)) -> s(X)
             p(mark(X)) -> p(X)
             p(active(X)) -> p(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(f(0())) -> mark(cons(0(),f(s(0()))))
       mark(f(X)) -> active(f(mark(X)))
       mark(0()) -> active(0())
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(s(X)) -> active(s(mark(X)))
       mark(p(X)) -> active(p(mark(X)))
       f(mark(X)) -> f(X)
       f(active(X)) -> f(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)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       p(mark(X)) -> p(X)
       p(active(X)) -> p(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(f(0())) -> mark(cons(0(),f(s(0()))))
         mark(f(X)) -> active(f(mark(X)))
         mark(0()) -> active(0())
         mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
         mark(s(X)) -> active(s(mark(X)))
         mark(p(X)) -> active(p(mark(X)))
         f(mark(X)) -> f(X)
         f(active(X)) -> f(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)
         s(mark(X)) -> s(X)
         s(active(X)) -> s(X)
         p(mark(X)) -> p(X)
         p(active(X)) -> p(X)
       Subterm Criterion Processor:
        simple projection:
         pi(cons#) = 0
        problem:
         DPs:
          
         TRS:
          active(f(0())) -> mark(cons(0(),f(s(0()))))
          mark(f(X)) -> active(f(mark(X)))
          mark(0()) -> active(0())
          mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
          mark(s(X)) -> active(s(mark(X)))
          mark(p(X)) -> active(p(mark(X)))
          f(mark(X)) -> f(X)
          f(active(X)) -> f(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)
          s(mark(X)) -> s(X)
          s(active(X)) -> s(X)
          p(mark(X)) -> p(X)
          p(active(X)) -> p(X)
        Qed
      
      DPs:
       s#(mark(X)) -> s#(X)
       s#(active(X)) -> s#(X)
      TRS:
       active(f(0())) -> mark(cons(0(),f(s(0()))))
       mark(f(X)) -> active(f(mark(X)))
       mark(0()) -> active(0())
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(s(X)) -> active(s(mark(X)))
       mark(p(X)) -> active(p(mark(X)))
       f(mark(X)) -> f(X)
       f(active(X)) -> f(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)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       p(mark(X)) -> p(X)
       p(active(X)) -> p(X)
      Subterm Criterion Processor:
       simple projection:
        pi(s#) = 0
       problem:
        DPs:
         
        TRS:
         active(f(0())) -> mark(cons(0(),f(s(0()))))
         mark(f(X)) -> active(f(mark(X)))
         mark(0()) -> active(0())
         mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
         mark(s(X)) -> active(s(mark(X)))
         mark(p(X)) -> active(p(mark(X)))
         f(mark(X)) -> f(X)
         f(active(X)) -> f(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)
         s(mark(X)) -> s(X)
         s(active(X)) -> s(X)
         p(mark(X)) -> p(X)
         p(active(X)) -> p(X)
       Qed
      
      DPs:
       f#(mark(X)) -> f#(X)
       f#(active(X)) -> f#(X)
      TRS:
       active(f(0())) -> mark(cons(0(),f(s(0()))))
       mark(f(X)) -> active(f(mark(X)))
       mark(0()) -> active(0())
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(s(X)) -> active(s(mark(X)))
       mark(p(X)) -> active(p(mark(X)))
       f(mark(X)) -> f(X)
       f(active(X)) -> f(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)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       p(mark(X)) -> p(X)
       p(active(X)) -> p(X)
      Subterm Criterion Processor:
       simple projection:
        pi(f#) = 0
       problem:
        DPs:
         
        TRS:
         active(f(0())) -> mark(cons(0(),f(s(0()))))
         mark(f(X)) -> active(f(mark(X)))
         mark(0()) -> active(0())
         mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
         mark(s(X)) -> active(s(mark(X)))
         mark(p(X)) -> active(p(mark(X)))
         f(mark(X)) -> f(X)
         f(active(X)) -> f(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)
         s(mark(X)) -> s(X)
         s(active(X)) -> s(X)
         p(mark(X)) -> p(X)
         p(active(X)) -> p(X)
       Qed
      
      DPs:
       p#(mark(X)) -> p#(X)
       p#(active(X)) -> p#(X)
      TRS:
       active(f(0())) -> mark(cons(0(),f(s(0()))))
       mark(f(X)) -> active(f(mark(X)))
       mark(0()) -> active(0())
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(s(X)) -> active(s(mark(X)))
       mark(p(X)) -> active(p(mark(X)))
       f(mark(X)) -> f(X)
       f(active(X)) -> f(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)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
       p(mark(X)) -> p(X)
       p(active(X)) -> p(X)
      Subterm Criterion Processor:
       simple projection:
        pi(p#) = 0
       problem:
        DPs:
         
        TRS:
         active(f(0())) -> mark(cons(0(),f(s(0()))))
         mark(f(X)) -> active(f(mark(X)))
         mark(0()) -> active(0())
         mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
         mark(s(X)) -> active(s(mark(X)))
         mark(p(X)) -> active(p(mark(X)))
         f(mark(X)) -> f(X)
         f(active(X)) -> f(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)
         s(mark(X)) -> s(X)
         s(active(X)) -> s(X)
         p(mark(X)) -> p(X)
         p(active(X)) -> p(X)
       Qed