YES

Problem:
 a__f(f(X)) -> a__c(f(g(f(X))))
 a__c(X) -> d(X)
 a__h(X) -> a__c(d(X))
 mark(f(X)) -> a__f(mark(X))
 mark(c(X)) -> a__c(X)
 mark(h(X)) -> a__h(mark(X))
 mark(g(X)) -> g(X)
 mark(d(X)) -> d(X)
 a__f(X) -> f(X)
 a__c(X) -> c(X)
 a__h(X) -> h(X)

Proof:
 Arctic Interpretation Processor:
  dimension: 1
  interpretation:
   [h](x0) = x0,
   
   [c](x0) = x0,
   
   [mark](x0) = 2x0,
   
   [a__h](x0) = x0,
   
   [d](x0) = x0,
   
   [a__c](x0) = x0,
   
   [g](x0) = x0,
   
   [a__f](x0) = x0,
   
   [f](x0) = x0
  orientation:
   a__f(f(X)) = X >= X = a__c(f(g(f(X))))
   
   a__c(X) = X >= X = d(X)
   
   a__h(X) = X >= X = a__c(d(X))
   
   mark(f(X)) = 2X >= 2X = a__f(mark(X))
   
   mark(c(X)) = 2X >= X = a__c(X)
   
   mark(h(X)) = 2X >= 2X = a__h(mark(X))
   
   mark(g(X)) = 2X >= X = g(X)
   
   mark(d(X)) = 2X >= X = d(X)
   
   a__f(X) = X >= X = f(X)
   
   a__c(X) = X >= X = c(X)
   
   a__h(X) = X >= X = h(X)
  problem:
   a__f(f(X)) -> a__c(f(g(f(X))))
   a__c(X) -> d(X)
   a__h(X) -> a__c(d(X))
   mark(f(X)) -> a__f(mark(X))
   mark(h(X)) -> a__h(mark(X))
   a__f(X) -> f(X)
   a__c(X) -> c(X)
   a__h(X) -> h(X)
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [h](x0) = 1x0,
    
    [c](x0) = x0,
    
    [mark](x0) = x0,
    
    [a__h](x0) = 1x0,
    
    [d](x0) = x0,
    
    [a__c](x0) = x0,
    
    [g](x0) = x0,
    
    [a__f](x0) = 8x0,
    
    [f](x0) = 8x0
   orientation:
    a__f(f(X)) = 16X >= 16X = a__c(f(g(f(X))))
    
    a__c(X) = X >= X = d(X)
    
    a__h(X) = 1X >= X = a__c(d(X))
    
    mark(f(X)) = 8X >= 8X = a__f(mark(X))
    
    mark(h(X)) = 1X >= 1X = a__h(mark(X))
    
    a__f(X) = 8X >= 8X = f(X)
    
    a__c(X) = X >= X = c(X)
    
    a__h(X) = 1X >= 1X = h(X)
   problem:
    a__f(f(X)) -> a__c(f(g(f(X))))
    a__c(X) -> d(X)
    mark(f(X)) -> a__f(mark(X))
    mark(h(X)) -> a__h(mark(X))
    a__f(X) -> f(X)
    a__c(X) -> c(X)
    a__h(X) -> h(X)
   Arctic Interpretation Processor:
    dimension: 2
    interpretation:
               [0  0 ]  
     [h](x0) = [-& -&]x0,
     
               [1  -&]  
     [c](x0) = [-& -&]x0,
     
                  [0 0]  
     [mark](x0) = [0 0]x0,
     
                  [0  0 ]  
     [a__h](x0) = [-& -&]x0,
     
               [0  -&]  
     [d](x0) = [-& -&]x0,
     
                  [1  -&]  
     [a__c](x0) = [-& -&]x0,
     
               [0  -&]  
     [g](x0) = [2  -&]x0,
     
                  [0 0]  
     [a__f](x0) = [3 3]x0,
     
               [0 0]  
     [f](x0) = [3 3]x0
    orientation:
                  [3 3]     [3  3 ]                    
     a__f(f(X)) = [6 6]X >= [-& -&]X = a__c(f(g(f(X))))
     
               [1  -&]     [0  -&]        
     a__c(X) = [-& -&]X >= [-& -&]X = d(X)
     
                  [3 3]     [0 0]                 
     mark(f(X)) = [3 3]X >= [3 3]X = a__f(mark(X))
     
                  [0 0]     [0  0 ]                 
     mark(h(X)) = [0 0]X >= [-& -&]X = a__h(mark(X))
     
               [0 0]     [0 0]        
     a__f(X) = [3 3]X >= [3 3]X = f(X)
     
               [1  -&]     [1  -&]        
     a__c(X) = [-& -&]X >= [-& -&]X = c(X)
     
               [0  0 ]     [0  0 ]        
     a__h(X) = [-& -&]X >= [-& -&]X = h(X)
    problem:
     a__f(f(X)) -> a__c(f(g(f(X))))
     mark(f(X)) -> a__f(mark(X))
     mark(h(X)) -> a__h(mark(X))
     a__f(X) -> f(X)
     a__c(X) -> c(X)
     a__h(X) -> h(X)
    Arctic Interpretation Processor:
     dimension: 2
     interpretation:
                [0  0 ]  
      [h](x0) = [0  -&]x0,
      
                [0  -&]  
      [c](x0) = [0  -&]x0,
      
                   [0  -&]  
      [mark](x0) = [0  0 ]x0,
      
                   [0  0 ]  
      [a__h](x0) = [0  -&]x0,
      
                   [1  -&]  
      [a__c](x0) = [1  -&]x0,
      
                [0  -&]  
      [g](x0) = [0  -&]x0,
      
                   [0 0]  
      [a__f](x0) = [2 2]x0,
      
                [0 0]  
      [f](x0) = [2 2]x0
     orientation:
                   [2 2]     [1 1]                    
      a__f(f(X)) = [4 4]X >= [1 1]X = a__c(f(g(f(X))))
      
                   [0 0]     [0 0]                 
      mark(f(X)) = [2 2]X >= [2 2]X = a__f(mark(X))
      
                   [0 0]     [0  0 ]                 
      mark(h(X)) = [0 0]X >= [0  -&]X = a__h(mark(X))
      
                [0 0]     [0 0]        
      a__f(X) = [2 2]X >= [2 2]X = f(X)
      
                [1  -&]     [0  -&]        
      a__c(X) = [1  -&]X >= [0  -&]X = c(X)
      
                [0  0 ]     [0  0 ]        
      a__h(X) = [0  -&]X >= [0  -&]X = h(X)
     problem:
      mark(f(X)) -> a__f(mark(X))
      mark(h(X)) -> a__h(mark(X))
      a__f(X) -> f(X)
      a__h(X) -> h(X)
     KBO Processor:
      weight function:
       w0 = 1
       w(h) = w(mark) = w(a__h) = w(a__f) = w(f) = 1
      precedence:
       mark > a__h ~ a__f > h ~ f
      problem:
       
      Qed