YES

Problem:
 f(x1) -> n(c(c(x1)))
 c(f(x1)) -> f(c(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) -> c#(x1)
   f#(x1) -> c#(c(x1))
   f#(x1) -> n#(c(c(x1)))
   c#(f(x1)) -> c#(x1)
   c#(f(x1)) -> c#(c(x1))
   c#(f(x1)) -> f#(c(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(c(x1)))
   c(f(x1)) -> f(c(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) -> c#(x1)
    f#(x1) -> c#(c(x1))
    f#(x1) -> n#(c(c(x1)))
    c#(f(x1)) -> c#(x1)
    c#(f(x1)) -> c#(c(x1))
    c#(f(x1)) -> f#(c(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(c(x1)))
    c(f(x1)) -> f(c(c(x1)))
    c(c(x1)) -> c(x1)
    n(s(x1)) -> f(s(s(x1)))
    n(f(x1)) -> f(n(x1))
   graph:
    n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> n#(c(c(x1)))
    n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> c#(c(x1))
    n#(s(x1)) -> f#(s(s(x1))) -> 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)) -> f#(n(x1)) -> f#(x1) -> n#(c(c(x1)))
    n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> c#(c(x1))
    n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> c#(x1)
    c#(f(x1)) -> c#(c(x1)) -> c#(f(x1)) -> f#(c(c(x1)))
    c#(f(x1)) -> c#(c(x1)) -> c#(f(x1)) -> c#(c(x1))
    c#(f(x1)) -> c#(c(x1)) -> c#(f(x1)) -> c#(x1)
    c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> f#(c(c(x1)))
    c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> c#(c(x1))
    c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> c#(x1)
    c#(f(x1)) -> f#(c(c(x1))) -> f#(x1) -> n#(c(c(x1)))
    c#(f(x1)) -> f#(c(c(x1))) -> f#(x1) -> c#(c(x1))
    c#(f(x1)) -> f#(c(c(x1))) -> f#(x1) -> c#(x1)
    f#(x1) -> n#(c(c(x1))) -> n#(f(x1)) -> f#(n(x1))
    f#(x1) -> n#(c(c(x1))) -> n#(f(x1)) -> n#(x1)
    f#(x1) -> n#(c(c(x1))) -> n#(s(x1)) -> f#(s(s(x1)))
    f#(x1) -> c#(c(x1)) -> c#(f(x1)) -> f#(c(c(x1)))
    f#(x1) -> c#(c(x1)) -> c#(f(x1)) -> c#(c(x1))
    f#(x1) -> c#(c(x1)) -> c#(f(x1)) -> c#(x1)
    f#(x1) -> c#(x1) -> c#(f(x1)) -> f#(c(c(x1)))
    f#(x1) -> c#(x1) -> c#(f(x1)) -> c#(c(x1))
    f#(x1) -> c#(x1) -> c#(f(x1)) -> c#(x1)
   EDG Processor:
    DPs:
     f#(x1) -> c#(x1)
     f#(x1) -> c#(c(x1))
     f#(x1) -> n#(c(c(x1)))
     c#(f(x1)) -> c#(x1)
     c#(f(x1)) -> c#(c(x1))
     c#(f(x1)) -> f#(c(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(c(x1)))
     c(f(x1)) -> f(c(c(x1)))
     c(c(x1)) -> c(x1)
     n(s(x1)) -> f(s(s(x1)))
     n(f(x1)) -> f(n(x1))
    graph:
     n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> c#(x1)
     n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> c#(c(x1))
     n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> n#(c(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) -> c#(x1)
     n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> c#(c(x1))
     n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> n#(c(c(x1)))
     c#(f(x1)) -> c#(c(x1)) -> c#(f(x1)) -> c#(x1)
     c#(f(x1)) -> c#(c(x1)) -> c#(f(x1)) -> c#(c(x1))
     c#(f(x1)) -> c#(c(x1)) -> c#(f(x1)) -> f#(c(c(x1)))
     c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> c#(x1)
     c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> c#(c(x1))
     c#(f(x1)) -> c#(x1) -> c#(f(x1)) -> f#(c(c(x1)))
     c#(f(x1)) -> f#(c(c(x1))) -> f#(x1) -> c#(x1)
     c#(f(x1)) -> f#(c(c(x1))) -> f#(x1) -> c#(c(x1))
     c#(f(x1)) -> f#(c(c(x1))) -> f#(x1) -> n#(c(c(x1)))
     f#(x1) -> n#(c(c(x1))) -> n#(f(x1)) -> n#(x1)
     f#(x1) -> n#(c(c(x1))) -> n#(f(x1)) -> f#(n(x1))
     f#(x1) -> c#(c(x1)) -> c#(f(x1)) -> c#(x1)
     f#(x1) -> c#(c(x1)) -> c#(f(x1)) -> c#(c(x1))
     f#(x1) -> c#(c(x1)) -> c#(f(x1)) -> f#(c(c(x1)))
     f#(x1) -> c#(x1) -> c#(f(x1)) -> c#(x1)
     f#(x1) -> c#(x1) -> c#(f(x1)) -> c#(c(x1))
     f#(x1) -> c#(x1) -> c#(f(x1)) -> f#(c(c(x1)))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [n#](x0) = x0,
      
      [c#](x0) = x0,
      
      [f#](x0) = x0,
      
      [s](x0) = x0 + -16,
      
      [n](x0) = 2x0 + 0,
      
      [c](x0) = x0,
      
      [f](x0) = 2x0 + 0
     orientation:
      f#(x1) = x1 >= x1 = c#(x1)
      
      f#(x1) = x1 >= x1 = c#(c(x1))
      
      f#(x1) = x1 >= x1 = n#(c(c(x1)))
      
      c#(f(x1)) = 2x1 + 0 >= x1 = c#(x1)
      
      c#(f(x1)) = 2x1 + 0 >= x1 = c#(c(x1))
      
      c#(f(x1)) = 2x1 + 0 >= x1 = f#(c(c(x1)))
      
      n#(s(x1)) = x1 + -16 >= x1 + -16 = f#(s(s(x1)))
      
      n#(f(x1)) = 2x1 + 0 >= x1 = n#(x1)
      
      n#(f(x1)) = 2x1 + 0 >= 2x1 + 0 = f#(n(x1))
      
      f(x1) = 2x1 + 0 >= 2x1 + 0 = n(c(c(x1)))
      
      c(f(x1)) = 2x1 + 0 >= 2x1 + 0 = f(c(c(x1)))
      
      c(c(x1)) = x1 >= x1 = c(x1)
      
      n(s(x1)) = 2x1 + 0 >= 2x1 + 0 = f(s(s(x1)))
      
      n(f(x1)) = 4x1 + 2 >= 4x1 + 2 = f(n(x1))
     problem:
      DPs:
       f#(x1) -> c#(x1)
       f#(x1) -> c#(c(x1))
       f#(x1) -> n#(c(c(x1)))
       n#(s(x1)) -> f#(s(s(x1)))
       n#(f(x1)) -> f#(n(x1))
      TRS:
       f(x1) -> n(c(c(x1)))
       c(f(x1)) -> f(c(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) -> c#(x1)
       f#(x1) -> c#(c(x1))
       f#(x1) -> n#(c(c(x1)))
       n#(s(x1)) -> f#(s(s(x1)))
       n#(f(x1)) -> f#(n(x1))
      TRS:
       f(x1) -> n(c(c(x1)))
       c(f(x1)) -> f(c(c(x1)))
       c(c(x1)) -> c(x1)
       n(s(x1)) -> f(s(s(x1)))
       n(f(x1)) -> f(n(x1))
      graph:
       n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> n#(c(c(x1)))
       n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> c#(c(x1))
       n#(s(x1)) -> f#(s(s(x1))) -> f#(x1) -> c#(x1)
       n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> n#(c(c(x1)))
       n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> c#(c(x1))
       n#(f(x1)) -> f#(n(x1)) -> f#(x1) -> c#(x1)
       f#(x1) -> n#(c(c(x1))) -> n#(f(x1)) -> f#(n(x1))
      SCC Processor:
       #sccs: 1
       #rules: 2
       #arcs: 7/25
       DPs:
        f#(x1) -> n#(c(c(x1)))
        n#(f(x1)) -> f#(n(x1))
       TRS:
        f(x1) -> n(c(c(x1)))
        c(f(x1)) -> f(c(c(x1)))
        c(c(x1)) -> c(x1)
        n(s(x1)) -> f(s(s(x1)))
        n(f(x1)) -> f(n(x1))
       Matrix Interpretation Processor: dim=4
        
        interpretation:
         [n#](x0) = [1 0 0 1]x0,
         
         [f#](x0) = [1 0 0 0]x0,
         
                   [0 0 0 0]     [0]
                   [0 0 1 0]     [0]
         [s](x0) = [1 0 0 0]x0 + [0]
                   [1 1 1 0]     [1],
         
                   [1 0 0 1]     [0]
                   [0 0 0 0]     [0]
         [n](x0) = [0 0 0 0]x0 + [1]
                   [0 0 0 1]     [0],
         
                   [1 0 0 0]     [0]
                   [0 0 0 0]     [1]
         [c](x0) = [0 0 0 0]x0 + [1]
                   [0 0 0 0]     [0],
         
                   [1 0 0 0]     [1]
                   [0 0 0 0]     [0]
         [f](x0) = [0 0 0 0]x0 + [1]
                   [0 0 0 1]     [0]
        orientation:
         f#(x1) = [1 0 0 0]x1 >= [1 0 0 0]x1 = n#(c(c(x1)))
         
         n#(f(x1)) = [1 0 0 1]x1 + [1] >= [1 0 0 1]x1 = f#(n(x1))
         
                 [1 0 0 0]     [1]    [1 0 0 0]     [0]              
                 [0 0 0 0]     [0]    [0 0 0 0]     [0]              
         f(x1) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = n(c(c(x1)))
                 [0 0 0 1]     [0]    [0 0 0 0]     [0]              
         
                    [1 0 0 0]     [1]    [1 0 0 0]     [1]              
                    [0 0 0 0]     [1]    [0 0 0 0]     [0]              
         c(f(x1)) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = f(c(c(x1)))
                    [0 0 0 0]     [0]    [0 0 0 0]     [0]              
         
                    [1 0 0 0]     [0]    [1 0 0 0]     [0]        
                    [0 0 0 0]     [1]    [0 0 0 0]     [1]        
         c(c(x1)) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = c(x1)
                    [0 0 0 0]     [0]    [0 0 0 0]     [0]        
         
                    [1 1 1 0]     [1]    [0 0 0 0]     [1]              
                    [0 0 0 0]     [0]    [0 0 0 0]     [0]              
         n(s(x1)) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = f(s(s(x1)))
                    [1 1 1 0]     [1]    [1 0 1 0]     [1]              
         
                    [1 0 0 1]     [1]    [1 0 0 1]     [1]           
                    [0 0 0 0]     [0]    [0 0 0 0]     [0]           
         n(f(x1)) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = f(n(x1))
                    [0 0 0 1]     [0]    [0 0 0 1]     [0]           
        problem:
         DPs:
          f#(x1) -> n#(c(c(x1)))
         TRS:
          f(x1) -> n(c(c(x1)))
          c(f(x1)) -> f(c(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#(c(c(x1)))
         TRS:
          f(x1) -> n(c(c(x1)))
          c(f(x1)) -> f(c(c(x1)))
          c(c(x1)) -> c(x1)
          n(s(x1)) -> f(s(s(x1)))
          n(f(x1)) -> f(n(x1))
         graph:
          
         Qed