YES

Problem:
 f(s(x1)) -> s(s(f(p(s(x1)))))
 f(0(x1)) -> 0(x1)
 p(s(x1)) -> x1

Proof:
 DP Processor:
  DPs:
   f#(s(x1)) -> p#(s(x1))
   f#(s(x1)) -> f#(p(s(x1)))
  TRS:
   f(s(x1)) -> s(s(f(p(s(x1)))))
   f(0(x1)) -> 0(x1)
   p(s(x1)) -> x1
  Usable Rule Processor:
   DPs:
    f#(s(x1)) -> p#(s(x1))
    f#(s(x1)) -> f#(p(s(x1)))
   TRS:
    p(s(x1)) -> x1
   Arctic Interpretation Processor:
    dimension: 2
    usable rules:
     p(s(x1)) -> x1
    interpretation:
     [p#](x0) = [-& 0 ]x0 + [0],
     
     [f#](x0) = [-& 1 ]x0 + [3],
     
               [-& 2 ]     [1]
     [p](x0) = [0  -4]x0 + [1],
     
               [-& 2 ]     [0]
     [s](x0) = [-1 3 ]x0 + [3]
    orientation:
     f#(s(x1)) = [0 4]x1 + [4] >= [-1 3 ]x1 + [3] = p#(s(x1))
     
     f#(s(x1)) = [0 4]x1 + [4] >= [-4 3 ]x1 + [3] = f#(p(s(x1)))
     
                [1  5 ]     [5]           
     p(s(x1)) = [-5 2 ]x1 + [1] >= x1 = x1
    problem:
     DPs:
      
     TRS:
      p(s(x1)) -> x1
    Qed