YES

Problem:
 f(x1) -> n(c(n(a(x1))))
 c(f(x1)) -> f(n(a(c(x1))))
 n(a(x1)) -> c(x1)
 c(c(x1)) -> c(x1)
 n(s(x1)) -> f(s(s(x1)))
 n(f(x1)) -> f(n(x1))

Proof:
 DP Processor:
  DPs:
   f#(x1) -> n#(a(x1))
   f#(x1) -> c#(n(a(x1)))
   f#(x1) -> n#(c(n(a(x1))))
   c#(f(x1)) -> c#(x1)
   c#(f(x1)) -> n#(a(c(x1)))
   c#(f(x1)) -> f#(n(a(c(x1))))
   n#(a(x1)) -> c#(x1)
   n#(s(x1)) -> f#(s(s(x1)))
   n#(f(x1)) -> n#(x1)
   n#(f(x1)) -> f#(n(x1))
  TRS:
   f(x1) -> n(c(n(a(x1))))
   c(f(x1)) -> f(n(a(c(x1))))
   n(a(x1)) -> c(x1)
   c(c(x1)) -> c(x1)
   n(s(x1)) -> f(s(s(x1)))
   n(f(x1)) -> f(n(x1))
  TDG Processor:
   DPs:
    f#(x1) -> n#(a(x1))
    f#(x1) -> c#(n(a(x1)))
    f#(x1) -> n#(c(n(a(x1))))
    c#(f(x1)) -> c#(x1)
    c#(f(x1)) -> n#(a(c(x1)))
    c#(f(x1)) -> f#(n(a(c(x1))))
    n#(a(x1)) -> c#(x1)
    n#(s(x1)) -> f#(s(s(x1)))
    n#(f(x1)) -> n#(x1)
    n#(f(x1)) -> f#(n(x1))
   TRS:
    f(x1) -> n(c(n(a(x1))))
    c(f(x1)) -> f(n(a(c(x1))))
    n(a(x1)) -> c(x1)
    c(c(x1)) -> c(x1)
    n(s(x1)) -> f(s(s(x1)))
    n(f(x1)) -> f(n(x1))
   graph:
    c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> f#(n(a(c(x1))))
    c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> n#(a(c(x1)))
    c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> c#(x1)
    c#(f(x1)) -> n#(a(c(x1))) -> n#(f(x1)) -> f#(n(x1))
    c#(f(x1)) -> n#(a(c(x1))) -> n#(f(x1)) -> n#(x1)
    c#(f(x1)) -> n#(a(c(x1))) -> n#(s(x1)) -> f#(s(s(x1)))
    c#(f(x1)) -> n#(a(c(x1))) -> n#(a(x1)) -> c#(x1)
    c#(f(x1)) -> f#(n(a(c(x1)))) -> f#(x1) -> n#(c(n(a(x1))))
    c#(f(x1)) -> f#(n(a(c(x1)))) -> f#(x1) -> c#(n(a(x1)))
    c#(f(x1)) -> f#(n(a(c(x1)))) -> f#(x1) -> n#(a(x1))
    n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> n#(c(n(a(x1))))
    n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> c#(n(a(x1)))
    n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> n#(a(x1))
    n#(a(x1)) -> c#(x1) -> c#(f(x1)) -> f#(n(a(c(x1))))
    n#(a(x1)) -> c#(x1) -> c#(f(x1)) -> n#(a(c(x1)))
    n#(a(x1)) -> c#(x1) -> c#(f(x1)) -> c#(x1)
    n#(f(x1)) -> n#(x1) -> n#(f(x1)) -> f#(n(x1))
    n#(f(x1)) -> n#(x1) -> n#(f(x1)) -> n#(x1)
    n#(f(x1)) -> n#(x1) -> n#(s(x1)) -> f#(s(s(x1)))
    n#(f(x1)) -> n#(x1) -> n#(a(x1)) -> c#(x1)
    n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> n#(c(n(a(x1))))
    n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> c#(n(a(x1)))
    n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> n#(a(x1))
    f#(x1) -> c#(n(a(x1))) -> c#(f(x1)) -> f#(n(a(c(x1))))
    f#(x1) -> c#(n(a(x1))) -> c#(f(x1)) -> n#(a(c(x1)))
    f#(x1) -> c#(n(a(x1))) -> c#(f(x1)) -> c#(x1)
    f#(x1) -> n#(c(n(a(x1)))) -> n#(f(x1)) -> f#(n(x1))
    f#(x1) -> n#(c(n(a(x1)))) -> n#(f(x1)) -> n#(x1)
    f#(x1) -> n#(c(n(a(x1)))) -> n#(s(x1)) -> f#(s(s(x1)))
    f#(x1) -> n#(c(n(a(x1)))) -> n#(a(x1)) -> c#(x1)
    f#(x1) -> n#(a(x1)) -> n#(f(x1)) -> f#(n(x1))
    f#(x1) -> n#(a(x1)) -> n#(f(x1)) -> n#(x1)
    f#(x1) -> n#(a(x1)) -> n#(s(x1)) -> f#(s(s(x1)))
    f#(x1) -> n#(a(x1)) -> n#(a(x1)) -> c#(x1)
   EDG Processor:
    DPs:
     f#(x1) -> n#(a(x1))
     f#(x1) -> c#(n(a(x1)))
     f#(x1) -> n#(c(n(a(x1))))
     c#(f(x1)) -> c#(x1)
     c#(f(x1)) -> n#(a(c(x1)))
     c#(f(x1)) -> f#(n(a(c(x1))))
     n#(a(x1)) -> c#(x1)
     n#(s(x1)) -> f#(s(s(x1)))
     n#(f(x1)) -> n#(x1)
     n#(f(x1)) -> f#(n(x1))
    TRS:
     f(x1) -> n(c(n(a(x1))))
     c(f(x1)) -> f(n(a(c(x1))))
     n(a(x1)) -> c(x1)
     c(c(x1)) -> c(x1)
     n(s(x1)) -> f(s(s(x1)))
     n(f(x1)) -> f(n(x1))
    graph:
     c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> c#(x1)
     c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> n#(a(c(x1)))
     c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> f#(n(a(c(x1))))
     c#(f(x1)) -> n#(a(c(x1))) -> n#(a(x1)) -> c#(x1)
     c#(f(x1)) -> f#(n(a(c(x1)))) -> f#(x1) -> n#(a(x1))
     c#(f(x1)) -> f#(n(a(c(x1)))) -> f#(x1) -> c#(n(a(x1)))
     c#(f(x1)) -> f#(n(a(c(x1)))) -> f#(x1) -> n#(c(n(a(x1))))
     n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> n#(a(x1))
     n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> c#(n(a(x1)))
     n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> n#(c(n(a(x1))))
     n#(a(x1)) -> c#(x1) -> c#(f(x1)) -> c#(x1)
     n#(a(x1)) -> c#(x1) -> c#(f(x1)) -> n#(a(c(x1)))
     n#(a(x1)) -> c#(x1) -> c#(f(x1)) -> f#(n(a(c(x1))))
     n#(f(x1)) -> n#(x1) -> n#(a(x1)) -> c#(x1)
     n#(f(x1)) -> n#(x1) -> n#(s(x1)) -> f#(s(s(x1)))
     n#(f(x1)) -> n#(x1) -> n#(f(x1)) -> n#(x1)
     n#(f(x1)) -> n#(x1) -> n#(f(x1)) -> f#(n(x1))
     n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> n#(a(x1))
     n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> c#(n(a(x1)))
     n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> n#(c(n(a(x1))))
     f#(x1) -> c#(n(a(x1))) -> c#(f(x1)) -> c#(x1)
     f#(x1) -> c#(n(a(x1))) -> c#(f(x1)) -> n#(a(c(x1)))
     f#(x1) -> c#(n(a(x1))) -> c#(f(x1)) -> f#(n(a(c(x1))))
     f#(x1) -> n#(c(n(a(x1)))) -> n#(f(x1)) -> n#(x1)
     f#(x1) -> n#(c(n(a(x1)))) -> n#(f(x1)) -> f#(n(x1))
     f#(x1) -> n#(a(x1)) -> n#(a(x1)) -> c#(x1)
    Matrix Interpretation Processor: dim=4
     
     interpretation:
      [c#](x0) = [0],
      
      [n#](x0) = [0 0 0 1]x0,
      
      [f#](x0) = [0],
      
                [0 0 0 1]     [0]
                [0 0 0 0]     [0]
      [s](x0) = [0 0 0 1]x0 + [0]
                [0 0 0 0]     [1],
      
                [1]
                [1]
      [c](x0) = [0]
                [0],
      
                [0 1 0 1]     [0]
                [0 0 0 0]     [1]
      [n](x0) = [0 0 0 0]x0 + [0]
                [0 0 0 1]     [0],
      
                [0]
                [1]
      [a](x0) = [0]
                [0],
      
                [0 0 0 0]     [1]
                [0 0 0 0]     [1]
      [f](x0) = [0 0 0 0]x0 + [0]
                [0 0 0 1]     [0]
     orientation:
      f#(x1) = [0] >= [0] = n#(a(x1))
      
      f#(x1) = [0] >= [0] = c#(n(a(x1)))
      
      f#(x1) = [0] >= [0] = n#(c(n(a(x1))))
      
      c#(f(x1)) = [0] >= [0] = c#(x1)
      
      c#(f(x1)) = [0] >= [0] = n#(a(c(x1)))
      
      c#(f(x1)) = [0] >= [0] = f#(n(a(c(x1))))
      
      n#(a(x1)) = [0] >= [0] = c#(x1)
      
      n#(s(x1)) = [1] >= [0] = f#(s(s(x1)))
      
      n#(f(x1)) = [0 0 0 1]x1 >= [0 0 0 1]x1 = n#(x1)
      
      n#(f(x1)) = [0 0 0 1]x1 >= [0] = f#(n(x1))
      
              [0 0 0 0]     [1]    [1]                 
              [0 0 0 0]     [1]    [1]                 
      f(x1) = [0 0 0 0]x1 + [0] >= [0] = n(c(n(a(x1))))
              [0 0 0 1]     [0]    [0]                 
      
                 [1]    [1]                 
                 [1]    [1]                 
      c(f(x1)) = [0] >= [0] = f(n(a(c(x1))))
                 [0]    [0]                 
      
                 [1]    [1]        
                 [1]    [1]        
      n(a(x1)) = [0] >= [0] = c(x1)
                 [0]    [0]        
      
                 [1]    [1]        
                 [1]    [1]        
      c(c(x1)) = [0] >= [0] = c(x1)
                 [0]    [0]        
      
                 [1]    [1]              
                 [1]    [1]              
      n(s(x1)) = [0] >= [0] = f(s(s(x1)))
                 [1]    [1]              
      
                 [0 0 0 1]     [1]    [0 0 0 0]     [1]           
                 [0 0 0 0]     [1]    [0 0 0 0]     [1]           
      n(f(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = f(n(x1))
                 [0 0 0 1]     [0]    [0 0 0 1]     [0]           
     problem:
      DPs:
       f#(x1) -> n#(a(x1))
       f#(x1) -> c#(n(a(x1)))
       f#(x1) -> n#(c(n(a(x1))))
       c#(f(x1)) -> c#(x1)
       c#(f(x1)) -> n#(a(c(x1)))
       c#(f(x1)) -> f#(n(a(c(x1))))
       n#(a(x1)) -> c#(x1)
       n#(f(x1)) -> n#(x1)
       n#(f(x1)) -> f#(n(x1))
      TRS:
       f(x1) -> n(c(n(a(x1))))
       c(f(x1)) -> f(n(a(c(x1))))
       n(a(x1)) -> c(x1)
       c(c(x1)) -> c(x1)
       n(s(x1)) -> f(s(s(x1)))
       n(f(x1)) -> f(n(x1))
     EDG Processor:
      DPs:
       f#(x1) -> n#(a(x1))
       f#(x1) -> c#(n(a(x1)))
       f#(x1) -> n#(c(n(a(x1))))
       c#(f(x1)) -> c#(x1)
       c#(f(x1)) -> n#(a(c(x1)))
       c#(f(x1)) -> f#(n(a(c(x1))))
       n#(a(x1)) -> c#(x1)
       n#(f(x1)) -> n#(x1)
       n#(f(x1)) -> f#(n(x1))
      TRS:
       f(x1) -> n(c(n(a(x1))))
       c(f(x1)) -> f(n(a(c(x1))))
       n(a(x1)) -> c(x1)
       c(c(x1)) -> c(x1)
       n(s(x1)) -> f(s(s(x1)))
       n(f(x1)) -> f(n(x1))
      graph:
       c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> f#(n(a(c(x1))))
       c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> n#(a(c(x1)))
       c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> c#(x1)
       c#(f(x1)) -> n#(a(c(x1))) -> n#(a(x1)) -> c#(x1)
       c#(f(x1)) -> f#(n(a(c(x1)))) -> f#(x1) -> n#(c(n(a(x1))))
       c#(f(x1)) -> f#(n(a(c(x1)))) -> f#(x1) -> c#(n(a(x1)))
       c#(f(x1)) -> f#(n(a(c(x1)))) -> f#(x1) -> n#(a(x1))
       n#(a(x1)) -> c#(x1) -> c#(f(x1)) -> f#(n(a(c(x1))))
       n#(a(x1)) -> c#(x1) -> c#(f(x1)) -> n#(a(c(x1)))
       n#(a(x1)) -> c#(x1) -> c#(f(x1)) -> c#(x1)
       n#(f(x1)) -> n#(x1) -> n#(f(x1)) -> f#(n(x1))
       n#(f(x1)) -> n#(x1) -> n#(f(x1)) -> n#(x1)
       n#(f(x1)) -> n#(x1) -> n#(a(x1)) -> c#(x1)
       n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> n#(c(n(a(x1))))
       n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> c#(n(a(x1)))
       n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> n#(a(x1))
       f#(x1) -> c#(n(a(x1))) -> c#(f(x1)) -> f#(n(a(c(x1))))
       f#(x1) -> c#(n(a(x1))) -> c#(f(x1)) -> n#(a(c(x1)))
       f#(x1) -> c#(n(a(x1))) -> c#(f(x1)) -> c#(x1)
       f#(x1) -> n#(c(n(a(x1)))) -> n#(f(x1)) -> f#(n(x1))
       f#(x1) -> n#(c(n(a(x1)))) -> n#(f(x1)) -> n#(x1)
       f#(x1) -> n#(a(x1)) -> n#(a(x1)) -> c#(x1)
      Matrix Interpretation Processor: dim=4
       
       interpretation:
        [c#](x0) = [0 0 0 1]x0,
        
        [n#](x0) = [0 1 1 1]x0,
        
        [f#](x0) = [1 0 0 1]x0 + [1],
        
                  [0 0 0 0]     [0]
                  [0 0 0 0]     [1]
        [s](x0) = [1 0 0 0]x0 + [0]
                  [1 0 1 0]     [0],
        
                  [0 0 0 0]  
                  [0 0 0 0]  
        [c](x0) = [0 0 0 0]x0
                  [0 0 0 1]  ,
        
                  [0 0 1 0]  
                  [0 1 0 0]  
        [n](x0) = [0 0 0 0]x0
                  [0 1 0 1]  ,
        
                  [0 0 0 0]  
                  [0 0 0 0]  
        [a](x0) = [0 0 0 0]x0
                  [0 0 0 1]  ,
        
                  [0 0 0 0]     [0]
                  [0 1 1 0]     [0]
        [f](x0) = [0 0 0 0]x0 + [0]
                  [0 0 0 1]     [1]
       orientation:
        f#(x1) = [1 0 0 1]x1 + [1] >= [0 0 0 1]x1 = n#(a(x1))
        
        f#(x1) = [1 0 0 1]x1 + [1] >= [0 0 0 1]x1 = c#(n(a(x1)))
        
        f#(x1) = [1 0 0 1]x1 + [1] >= [0 0 0 1]x1 = n#(c(n(a(x1))))
        
        c#(f(x1)) = [0 0 0 1]x1 + [1] >= [0 0 0 1]x1 = c#(x1)
        
        c#(f(x1)) = [0 0 0 1]x1 + [1] >= [0 0 0 1]x1 = n#(a(c(x1)))
        
        c#(f(x1)) = [0 0 0 1]x1 + [1] >= [0 0 0 1]x1 + [1] = f#(n(a(c(x1))))
        
        n#(a(x1)) = [0 0 0 1]x1 >= [0 0 0 1]x1 = c#(x1)
        
        n#(f(x1)) = [0 1 1 1]x1 + [1] >= [0 1 1 1]x1 = n#(x1)
        
        n#(f(x1)) = [0 1 1 1]x1 + [1] >= [0 1 1 1]x1 + [1] = f#(n(x1))
        
                [0 0 0 0]     [0]    [0 0 0 0]                   
                [0 1 1 0]     [0]    [0 0 0 0]                   
        f(x1) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 = n(c(n(a(x1))))
                [0 0 0 1]     [1]    [0 0 0 1]                   
        
                   [0 0 0 0]     [0]    [0 0 0 0]     [0]                 
                   [0 0 0 0]     [0]    [0 0 0 0]     [0]                 
        c(f(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = f(n(a(c(x1))))
                   [0 0 0 1]     [1]    [0 0 0 1]     [1]                 
        
                   [0 0 0 0]      [0 0 0 0]          
                   [0 0 0 0]      [0 0 0 0]          
        n(a(x1)) = [0 0 0 0]x1 >= [0 0 0 0]x1 = c(x1)
                   [0 0 0 1]      [0 0 0 1]          
        
                   [0 0 0 0]      [0 0 0 0]          
                   [0 0 0 0]      [0 0 0 0]          
        c(c(x1)) = [0 0 0 0]x1 >= [0 0 0 0]x1 = c(x1)
                   [0 0 0 1]      [0 0 0 1]          
        
                   [1 0 0 0]     [0]    [0 0 0 0]     [0]              
                   [0 0 0 0]     [1]    [0 0 0 0]     [1]              
        n(s(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = f(s(s(x1)))
                   [1 0 1 0]     [1]    [1 0 0 0]     [1]              
        
                   [0 0 0 0]     [0]    [0 0 0 0]     [0]           
                   [0 1 1 0]     [0]    [0 1 0 0]     [0]           
        n(f(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = f(n(x1))
                   [0 1 1 1]     [1]    [0 1 0 1]     [1]           
       problem:
        DPs:
         c#(f(x1)) -> f#(n(a(c(x1))))
         n#(a(x1)) -> c#(x1)
         n#(f(x1)) -> f#(n(x1))
        TRS:
         f(x1) -> n(c(n(a(x1))))
         c(f(x1)) -> f(n(a(c(x1))))
         n(a(x1)) -> c(x1)
         c(c(x1)) -> c(x1)
         n(s(x1)) -> f(s(s(x1)))
         n(f(x1)) -> f(n(x1))
       EDG Processor:
        DPs:
         c#(f(x1)) -> f#(n(a(c(x1))))
         n#(a(x1)) -> c#(x1)
         n#(f(x1)) -> f#(n(x1))
        TRS:
         f(x1) -> n(c(n(a(x1))))
         c(f(x1)) -> f(n(a(c(x1))))
         n(a(x1)) -> c(x1)
         c(c(x1)) -> c(x1)
         n(s(x1)) -> f(s(s(x1)))
         n(f(x1)) -> f(n(x1))
        graph:
         n#(a(x1)) -> c#(x1) -> c#(f(x1)) -> f#(n(a(c(x1))))
        CDG Processor:
         DPs:
          c#(f(x1)) -> f#(n(a(c(x1))))
          n#(a(x1)) -> c#(x1)
          n#(f(x1)) -> f#(n(x1))
         TRS:
          f(x1) -> n(c(n(a(x1))))
          c(f(x1)) -> f(n(a(c(x1))))
          n(a(x1)) -> c(x1)
          c(c(x1)) -> c(x1)
          n(s(x1)) -> f(s(s(x1)))
          n(f(x1)) -> f(n(x1))
         graph:
          
         Qed