YES

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

Proof:
 Matrix Interpretation Processor: dim=3
  
  interpretation:
             [1 1 0]  
   [p](x0) = [0 0 0]x0
             [0 0 0]  ,
   
                [1 1 0]  
   [mark](x0) = [0 0 0]x0
                [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]  ,
   
             [1 1 0]  
   [s](x0) = [0 0 0]x0
             [0 0 0]  ,
   
                  [1 1 0]  
   [active](x0) = [0 0 0]x0
                  [0 0 0]  ,
   
             [1 1 0]     [0]
   [f](x0) = [0 0 0]x0 + [1]
             [0 0 0]     [0],
   
         [0]
   [0] = [0]
         [0]
  orientation:
                    [1]    [0]                            
   active(f(0())) = [0] >= [0] = mark(cons(0(),f(s(0()))))
                    [0]    [0]                            
   
                       [1]    [1]                     
   active(f(s(0()))) = [0] >= [0] = mark(f(p(s(0()))))
                       [0]    [0]                     
   
                       [0]    [0]            
   active(p(s(0()))) = [0] >= [0] = mark(0())
                       [0]    [0]            
   
                [1 1 0]    [1]    [1 1 0]    [1]                     
   mark(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(f(mark(X)))
                [0 0 0]    [0]    [0 0 0]    [0]                     
   
               [0]    [0]              
   mark(0()) = [0] >= [0] = active(0())
               [0]    [0]              
   
                       [1 1 0]     [1 0 0]      [1 1 0]     [1 0 0]                              
   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 0]     [1 1 0]                      
   mark(s(X)) = [0 0 0]X >= [0 0 0]X = active(s(mark(X)))
                [0 0 0]     [0 0 0]                      
   
                [1 1 0]     [1 1 0]                      
   mark(p(X)) = [0 0 0]X >= [0 0 0]X = active(p(mark(X)))
                [0 0 0]     [0 0 0]                      
   
                [1 1 0]    [0]    [1 1 0]    [0]       
   f(mark(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = f(X)
                [0 0 0]    [0]    [0 0 0]    [0]       
   
                  [1 1 0]    [0]    [1 1 0]    [0]       
   f(active(X)) = [0 0 0]X + [1] >= [0 0 0]X + [1] = f(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 0]        
   s(mark(X)) = [0 0 0]X >= [0 0 0]X = s(X)
                [0 0 0]     [0 0 0]        
   
                  [1 1 0]     [1 1 0]        
   s(active(X)) = [0 0 0]X >= [0 0 0]X = s(X)
                  [0 0 0]     [0 0 0]        
   
                [1 1 0]     [1 1 0]        
   p(mark(X)) = [0 0 0]X >= [0 0 0]X = p(X)
                [0 0 0]     [0 0 0]        
   
                  [1 1 0]     [1 1 0]        
   p(active(X)) = [0 0 0]X >= [0 0 0]X = p(X)
                  [0 0 0]     [0 0 0]        
  problem:
   active(f(s(0()))) -> mark(f(p(s(0()))))
   active(p(s(0()))) -> mark(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)
  Matrix Interpretation Processor: dim=3
   
   interpretation:
              [1 0 0]  
    [p](x0) = [0 0 0]x0
              [0 0 0]  ,
    
                 [1 0 0]     [0]
    [mark](x0) = [0 0 0]x0 + [0]
                 [0 0 0]     [1],
    
                     [1 0 0]     [1 0 0]  
    [cons](x0, x1) = [1 0 0]x0 + [0 0 0]x1
                     [0 0 0]     [0 0 0]  ,
    
              [1 0 0]     [1]
    [s](x0) = [0 0 0]x0 + [0]
              [0 0 0]     [0],
    
                   [1 0 1]     [0]
    [active](x0) = [0 0 0]x0 + [0]
                   [0 0 0]     [1],
    
              [1 0 0]  
    [f](x0) = [0 0 0]x0
              [0 0 0]  ,
    
          [0]
    [0] = [0]
          [0]
   orientation:
                        [1]    [1]                     
    active(f(s(0()))) = [0] >= [0] = mark(f(p(s(0()))))
                        [1]    [1]                     
    
                        [1]    [0]            
    active(p(s(0()))) = [0] >= [0] = mark(0())
                        [1]    [1]            
    
                 [1 0 0]    [0]    [1 0 0]    [0]                     
    mark(f(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(f(mark(X)))
                 [0 0 0]    [1]    [0 0 0]    [1]                     
    
                [0]    [0]              
    mark(0()) = [0] >= [0] = active(0())
                [1]    [1]              
    
                        [1 0 0]     [1 0 0]     [0]    [1 0 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]                            
    
                 [1 0 0]    [1]    [1 0 0]    [1]                     
    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 0 0]    [0]    [1 0 0]    [0]                     
    mark(p(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = active(p(mark(X)))
                 [0 0 0]    [1]    [0 0 0]    [1]                     
    
                 [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 1]     [1 0 0]        
    f(active(X)) = [0 0 0]X >= [0 0 0]X = f(X)
                   [0 0 0]     [0 0 0]        
    
                        [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]                
    cons(mark(X1),X2) = [1 0 0]X1 + [0 0 0]X2 >= [1 0 0]X1 + [0 0 0]X2 = cons(X1,X2)
                        [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]                
    
                        [1 0 0]     [1 0 0]      [1 0 0]     [1 0 0]                
    cons(X1,mark(X2)) = [1 0 0]X1 + [0 0 0]X2 >= [1 0 0]X1 + [0 0 0]X2 = cons(X1,X2)
                        [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]                
    
                          [1 0 1]     [1 0 0]      [1 0 0]     [1 0 0]                
    cons(active(X1),X2) = [1 0 1]X1 + [0 0 0]X2 >= [1 0 0]X1 + [0 0 0]X2 = cons(X1,X2)
                          [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]                
    
                          [1 0 0]     [1 0 1]      [1 0 0]     [1 0 0]                
    cons(X1,active(X2)) = [1 0 0]X1 + [0 0 0]X2 >= [1 0 0]X1 + [0 0 0]X2 = cons(X1,X2)
                          [0 0 0]     [0 0 0]      [0 0 0]     [0 0 0]                
    
                 [1 0 0]    [1]    [1 0 0]    [1]       
    s(mark(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = s(X)
                 [0 0 0]    [0]    [0 0 0]    [0]       
    
                   [1 0 1]    [1]    [1 0 0]    [1]       
    s(active(X)) = [0 0 0]X + [0] >= [0 0 0]X + [0] = s(X)
                   [0 0 0]    [0]    [0 0 0]    [0]       
    
                 [1 0 0]     [1 0 0]        
    p(mark(X)) = [0 0 0]X >= [0 0 0]X = p(X)
                 [0 0 0]     [0 0 0]        
    
                   [1 0 1]     [1 0 0]        
    p(active(X)) = [0 0 0]X >= [0 0 0]X = p(X)
                   [0 0 0]     [0 0 0]        
   problem:
    active(f(s(0()))) -> mark(f(p(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)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [p](x0) = 2x0,
     
     [mark](x0) = 4x0,
     
     [cons](x0, x1) = 4x0 + x1 + 4,
     
     [s](x0) = 4x0,
     
     [active](x0) = x0,
     
     [f](x0) = 4x0,
     
     [0] = 0
    orientation:
     active(f(s(0()))) = 0 >= 0 = mark(f(p(s(0()))))
     
     mark(f(X)) = 16X >= 16X = active(f(mark(X)))
     
     mark(0()) = 0 >= 0 = active(0())
     
     mark(cons(X1,X2)) = 16X1 + 4X2 + 16 >= 16X1 + X2 + 4 = active(cons(mark(X1),X2))
     
     mark(s(X)) = 16X >= 16X = active(s(mark(X)))
     
     mark(p(X)) = 8X >= 8X = active(p(mark(X)))
     
     f(mark(X)) = 16X >= 4X = f(X)
     
     f(active(X)) = 4X >= 4X = f(X)
     
     cons(mark(X1),X2) = 16X1 + X2 + 4 >= 4X1 + X2 + 4 = cons(X1,X2)
     
     cons(X1,mark(X2)) = 4X1 + 4X2 + 4 >= 4X1 + X2 + 4 = cons(X1,X2)
     
     cons(active(X1),X2) = 4X1 + X2 + 4 >= 4X1 + X2 + 4 = cons(X1,X2)
     
     cons(X1,active(X2)) = 4X1 + X2 + 4 >= 4X1 + X2 + 4 = cons(X1,X2)
     
     s(mark(X)) = 16X >= 4X = s(X)
     
     s(active(X)) = 4X >= 4X = s(X)
     
     p(mark(X)) = 8X >= 2X = p(X)
     
     p(active(X)) = 2X >= 2X = p(X)
    problem:
     active(f(s(0()))) -> mark(f(p(s(0()))))
     mark(f(X)) -> active(f(mark(X)))
     mark(0()) -> active(0())
     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(s(0()))) -> p#(s(0()))
      active#(f(s(0()))) -> f#(p(s(0())))
      active#(f(s(0()))) -> mark#(f(p(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#(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(s(0()))) -> mark(f(p(s(0()))))
      mark(f(X)) -> active(f(mark(X)))
      mark(0()) -> active(0())
      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(s(0()))) -> p#(s(0()))
       active#(f(s(0()))) -> f#(p(s(0())))
       active#(f(s(0()))) -> mark#(f(p(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#(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(s(0()))) -> mark(f(p(s(0()))))
       mark(f(X)) -> active(f(mark(X)))
       mark(0()) -> active(0())
       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:
       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)
       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)
       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#(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)) -> p#(mark(X)) -> p#(active(X)) -> p#(X)
       mark#(p(X)) -> p#(mark(X)) -> p#(mark(X)) -> p#(X)
       mark#(p(X)) -> active#(p(mark(X))) ->
       active#(f(s(0()))) -> mark#(f(p(s(0()))))
       mark#(p(X)) -> active#(p(mark(X))) ->
       active#(f(s(0()))) -> f#(p(s(0())))
       mark#(p(X)) -> active#(p(mark(X))) ->
       active#(f(s(0()))) -> p#(s(0()))
       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)) -> 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#(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)) -> active#(s(mark(X))) ->
       active#(f(s(0()))) -> mark#(f(p(s(0()))))
       mark#(s(X)) -> active#(s(mark(X))) ->
       active#(f(s(0()))) -> f#(p(s(0())))
       mark#(s(X)) -> active#(s(mark(X))) ->
       active#(f(s(0()))) -> p#(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#(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(s(0()))) -> mark#(f(p(s(0()))))
       mark#(f(X)) -> active#(f(mark(X))) ->
       active#(f(s(0()))) -> f#(p(s(0())))
       mark#(f(X)) -> active#(f(mark(X))) ->
       active#(f(s(0()))) -> p#(s(0()))
       mark#(0()) -> active#(0()) ->
       active#(f(s(0()))) -> mark#(f(p(s(0()))))
       mark#(0()) -> active#(0()) -> active#(f(s(0()))) -> f#(p(s(0())))
       mark#(0()) -> active#(0()) -> active#(f(s(0()))) -> p#(s(0()))
       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)
       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)
       active#(f(s(0()))) -> mark#(f(p(s(0())))) ->
       mark#(p(X)) -> active#(p(mark(X)))
       active#(f(s(0()))) -> mark#(f(p(s(0())))) ->
       mark#(p(X)) -> p#(mark(X))
       active#(f(s(0()))) -> mark#(f(p(s(0())))) ->
       mark#(p(X)) -> mark#(X)
       active#(f(s(0()))) -> mark#(f(p(s(0())))) ->
       mark#(s(X)) -> active#(s(mark(X)))
       active#(f(s(0()))) -> mark#(f(p(s(0())))) ->
       mark#(s(X)) -> s#(mark(X))
       active#(f(s(0()))) -> mark#(f(p(s(0())))) ->
       mark#(s(X)) -> mark#(X)
       active#(f(s(0()))) -> mark#(f(p(s(0())))) ->
       mark#(0()) -> active#(0())
       active#(f(s(0()))) -> mark#(f(p(s(0())))) ->
       mark#(f(X)) -> active#(f(mark(X)))
       active#(f(s(0()))) -> mark#(f(p(s(0())))) ->
       mark#(f(X)) -> f#(mark(X))
       active#(f(s(0()))) -> mark#(f(p(s(0())))) ->
       mark#(f(X)) -> mark#(X)
       active#(f(s(0()))) -> f#(p(s(0()))) ->
       f#(active(X)) -> f#(X)
       active#(f(s(0()))) -> f#(p(s(0()))) -> f#(mark(X)) -> f#(X)
       active#(f(s(0()))) -> p#(s(0())) -> p#(active(X)) -> p#(X)
       active#(f(s(0()))) -> p#(s(0())) -> p#(mark(X)) -> p#(X)
      SCC Processor:
       #sccs: 5
       #rules: 18
       #arcs: 90/529
       DPs:
        mark#(p(X)) -> mark#(X)
        mark#(f(X)) -> mark#(X)
        mark#(f(X)) -> active#(f(mark(X)))
        active#(f(s(0()))) -> mark#(f(p(s(0()))))
        mark#(0()) -> active#(0())
        mark#(s(X)) -> mark#(X)
        mark#(s(X)) -> active#(s(mark(X)))
        mark#(p(X)) -> active#(p(mark(X)))
       TRS:
        active(f(s(0()))) -> mark(f(p(s(0()))))
        mark(f(X)) -> active(f(mark(X)))
        mark(0()) -> active(0())
        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(s(0()))) -> mark#(f(p(s(0()))))
         mark#(0()) -> active#(0())
         mark#(s(X)) -> mark#(X)
         mark#(s(X)) -> active#(s(mark(X)))
         mark#(p(X)) -> active#(p(mark(X)))
        TRS:
         active(f(s(0()))) -> mark(f(p(s(0()))))
         mark(f(X)) -> active(f(mark(X)))
         mark(0()) -> active(0())
         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#(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(s(0()))) -> mark#(f(p(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#(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(s(0()))) -> mark#(f(p(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#(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(s(0()))) -> mark#(f(p(s(0()))))
         active#(f(s(0()))) -> mark#(f(p(s(0())))) ->
         mark#(f(X)) -> mark#(X)
         active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(f(X)) -> active#(f(mark(X)))
        CDG Processor:
         DPs:
          mark#(p(X)) -> mark#(X)
          mark#(f(X)) -> mark#(X)
          mark#(f(X)) -> active#(f(mark(X)))
          active#(f(s(0()))) -> mark#(f(p(s(0()))))
          mark#(0()) -> active#(0())
          mark#(s(X)) -> mark#(X)
          mark#(s(X)) -> active#(s(mark(X)))
          mark#(p(X)) -> active#(p(mark(X)))
         TRS:
          active(f(s(0()))) -> mark(f(p(s(0()))))
          mark(f(X)) -> active(f(mark(X)))
          mark(0()) -> active(0())
          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#(p(X)) -> active#(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)) -> mark#(X)
          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)) -> mark#(X)
          mark#(p(X)) -> active#(p(mark(X))) ->
          active#(f(s(0()))) -> mark#(f(p(s(0()))))
          mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> active#(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)) -> mark#(X)
          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)) -> mark#(X)
          mark#(f(X)) -> mark#(X) -> mark#(p(X)) -> active#(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)) -> mark#(X)
          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)) -> mark#(X)
          mark#(f(X)) -> active#(f(mark(X))) ->
          active#(f(s(0()))) -> mark#(f(p(s(0()))))
          active#(f(s(0()))) -> mark#(f(p(s(0())))) ->
          mark#(f(X)) -> active#(f(mark(X)))
          active#(f(s(0()))) -> mark#(f(p(s(0())))) -> mark#(f(X)) -> mark#(X)
         SCC Processor:
          #sccs: 1
          #rules: 6
          #arcs: 25/64
          DPs:
           mark#(p(X)) -> mark#(X)
           mark#(f(X)) -> mark#(X)
           mark#(f(X)) -> active#(f(mark(X)))
           active#(f(s(0()))) -> mark#(f(p(s(0()))))
           mark#(s(X)) -> mark#(X)
           mark#(p(X)) -> active#(p(mark(X)))
          TRS:
           active(f(s(0()))) -> mark(f(p(s(0()))))
           mark(f(X)) -> active(f(mark(X)))
           mark(0()) -> active(0())
           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,
            
            [active#](x0) = x0 + 0,
            
            [p](x0) = x0 + 0,
            
            [mark](x0) = x0,
            
            [cons](x0, x1) = 1x0 + 8,
            
            [s](x0) = 4x0 + 0,
            
            [active](x0) = x0 + 0,
            
            [f](x0) = x0 + 0,
            
            [0] = 2
           orientation:
            mark#(p(X)) = X + 0 >= X = mark#(X)
            
            mark#(f(X)) = X + 0 >= X = mark#(X)
            
            mark#(f(X)) = X + 0 >= X + 0 = active#(f(mark(X)))
            
            active#(f(s(0()))) = 6 >= 6 = mark#(f(p(s(0()))))
            
            mark#(s(X)) = 4X + 0 >= X = mark#(X)
            
            mark#(p(X)) = X + 0 >= X + 0 = active#(p(mark(X)))
            
            active(f(s(0()))) = 6 >= 6 = mark(f(p(s(0()))))
            
            mark(f(X)) = X + 0 >= X + 0 = active(f(mark(X)))
            
            mark(0()) = 2 >= 2 = active(0())
            
            mark(s(X)) = 4X + 0 >= 4X + 0 = active(s(mark(X)))
            
            mark(p(X)) = X + 0 >= X + 0 = active(p(mark(X)))
            
            f(mark(X)) = X + 0 >= X + 0 = f(X)
            
            f(active(X)) = X + 0 >= X + 0 = f(X)
            
            cons(mark(X1),X2) = 1X1 + 8 >= 1X1 + 8 = cons(X1,X2)
            
            cons(X1,mark(X2)) = 1X1 + 8 >= 1X1 + 8 = cons(X1,X2)
            
            cons(active(X1),X2) = 1X1 + 8 >= 1X1 + 8 = cons(X1,X2)
            
            cons(X1,active(X2)) = 1X1 + 8 >= 1X1 + 8 = cons(X1,X2)
            
            s(mark(X)) = 4X + 0 >= 4X + 0 = s(X)
            
            s(active(X)) = 4X + 4 >= 4X + 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#(f(X)) -> mark#(X)
             mark#(f(X)) -> active#(f(mark(X)))
             active#(f(s(0()))) -> mark#(f(p(s(0()))))
             mark#(p(X)) -> active#(p(mark(X)))
            TRS:
             active(f(s(0()))) -> mark(f(p(s(0()))))
             mark(f(X)) -> active(f(mark(X)))
             mark(0()) -> active(0())
             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)
           KBO Processor:
            argument filtering:
             pi(0) = []
             pi(f) = [0]
             pi(active) = 0
             pi(s) = 0
             pi(cons) = 1
             pi(mark) = 0
             pi(p) = 0
             pi(active#) = 0
             pi(mark#) = 0
            weight function:
             w0 = 1
             w(p) = w(mark) = w(cons) = w(f) = w(0) = 1
             w(mark#) = w(active#) = w(s) = w(active) = 0
            precedence:
             mark# ~ active# ~ p ~ mark ~ cons ~ s ~ active ~ f ~ 0
            problem:
             DPs:
              mark#(p(X)) -> mark#(X)
              mark#(f(X)) -> active#(f(mark(X)))
              active#(f(s(0()))) -> mark#(f(p(s(0()))))
              mark#(p(X)) -> active#(p(mark(X)))
             TRS:
              active(f(s(0()))) -> mark(f(p(s(0()))))
              mark(f(X)) -> active(f(mark(X)))
              mark(0()) -> active(0())
              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: 2
             #rules: 3
             #arcs: 19/16
             DPs:
              mark#(p(X)) -> mark#(X)
             TRS:
              active(f(s(0()))) -> mark(f(p(s(0()))))
              mark(f(X)) -> active(f(mark(X)))
              mark(0()) -> active(0())
              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(s(0()))) -> mark(f(p(s(0()))))
                mark(f(X)) -> active(f(mark(X)))
                mark(0()) -> active(0())
                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:
              mark#(f(X)) -> active#(f(mark(X)))
              active#(f(s(0()))) -> mark#(f(p(s(0()))))
             TRS:
              active(f(s(0()))) -> mark(f(p(s(0()))))
              mark(f(X)) -> active(f(mark(X)))
              mark(0()) -> active(0())
              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) = 4x0 + 0,
               
               [active#](x0) = 3x0 + 4,
               
               [p](x0) = 0,
               
               [mark](x0) = x0 + 0,
               
               [cons](x0, x1) = x0 + 0,
               
               [s](x0) = 4x0 + 4,
               
               [active](x0) = x0 + 0,
               
               [f](x0) = x0 + 0,
               
               [0] = 0
              orientation:
               mark#(f(X)) = 4X + 4 >= 3X + 4 = active#(f(mark(X)))
               
               active#(f(s(0()))) = 7 >= 4 = mark#(f(p(s(0()))))
               
               active(f(s(0()))) = 4 >= 0 = mark(f(p(s(0()))))
               
               mark(f(X)) = X + 0 >= X + 0 = active(f(mark(X)))
               
               mark(0()) = 0 >= 0 = active(0())
               
               mark(s(X)) = 4X + 4 >= 4X + 4 = active(s(mark(X)))
               
               mark(p(X)) = 0 >= 0 = active(p(mark(X)))
               
               f(mark(X)) = X + 0 >= X + 0 = f(X)
               
               f(active(X)) = X + 0 >= X + 0 = 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)) = 4X + 4 >= 4X + 4 = s(X)
               
               s(active(X)) = 4X + 4 >= 4X + 4 = s(X)
               
               p(mark(X)) = 0 >= 0 = p(X)
               
               p(active(X)) = 0 >= 0 = p(X)
              problem:
               DPs:
                mark#(f(X)) -> active#(f(mark(X)))
               TRS:
                active(f(s(0()))) -> mark(f(p(s(0()))))
                mark(f(X)) -> active(f(mark(X)))
                mark(0()) -> active(0())
                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: 0
               #rules: 0
               #arcs: 2/1
               
       
       DPs:
        p#(mark(X)) -> p#(X)
        p#(active(X)) -> p#(X)
       TRS:
        active(f(s(0()))) -> mark(f(p(s(0()))))
        mark(f(X)) -> active(f(mark(X)))
        mark(0()) -> active(0())
        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(s(0()))) -> mark(f(p(s(0()))))
          mark(f(X)) -> active(f(mark(X)))
          mark(0()) -> active(0())
          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(s(0()))) -> mark(f(p(s(0()))))
        mark(f(X)) -> active(f(mark(X)))
        mark(0()) -> active(0())
        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(s(0()))) -> mark(f(p(s(0()))))
          mark(f(X)) -> active(f(mark(X)))
          mark(0()) -> active(0())
          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(s(0()))) -> mark(f(p(s(0()))))
        mark(f(X)) -> active(f(mark(X)))
        mark(0()) -> active(0())
        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(s(0()))) -> mark(f(p(s(0()))))
          mark(f(X)) -> active(f(mark(X)))
          mark(0()) -> active(0())
          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(s(0()))) -> mark(f(p(s(0()))))
        mark(f(X)) -> active(f(mark(X)))
        mark(0()) -> active(0())
        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(s(0()))) -> mark(f(p(s(0()))))
          mark(f(X)) -> active(f(mark(X)))
          mark(0()) -> active(0())
          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(s(0()))) -> mark(f(p(s(0()))))
           mark(f(X)) -> active(f(mark(X)))
           mark(0()) -> active(0())
           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