YES
Time: 0.008716
TRS:
 {f s x -> s s f p s x,
  f 0() -> 0(),
  p s x -> x}
 DP:
  DP:
   {f# s x -> f# p s x,
    f# s x -> p# s x}
  TRS:
  {f s x -> s s f p s x,
   f 0() -> 0(),
   p s x -> x}
  EDG:
   {(f# s x -> f# p s x, f# s x -> f# p s x)
    (f# s x -> f# p s x, f# s x -> p# s x)}
   SCCS (1):
    Scc:
     {f# s x -> f# p s x}
    SCC (1):
     Strict:
      {f# s x -> f# p s x}
     Weak:
     {f s x -> s s f p s x,
      f 0() -> 0(),
      p s x -> x}
     BOUND:
      Bound: match(-raise)-DP-bounded by 1
      Automaton:
       {   0_0() -> 12*
         p_1(16) -> 17*
         p_0(14) -> 11*
         p_0(13) -> 14*
         p_0(12) -> 11*
         p_0(11) -> 11*
         p_0(10) -> 11*
        f#_1(17) -> 18*
        f#_0(14) -> 6*
         f_0(14) -> 10*
         f_0(13) -> 10*
         f_0(12) -> 10*
         f_0(11) -> 10*
         f_0(10) -> 10*
         s_1(25) -> 26*
         s_1(23) -> 24*
         s_1(21) -> 22*
         s_1(19) -> 20*
         s_1(15) -> 16*
         s_0(14) -> 13*
         s_0(13) -> 13*
         s_0(12) -> 13*
         s_0(11) -> 13*
         s_0(10) -> 13*
              26 -> 16*
              25 -> 17*
              24 -> 16*
              23 -> 17*
              22 -> 16*
              21 -> 17*
              20 -> 16*
              19 -> 17*
              18 -> 6*
              15 -> 17*
              14 -> 25 | 11
              13 -> 23 | 14 | 10
              12 -> 21 | 14 | 10
              11 -> 19 | 14
              10 -> 15 | 14 | 11}
      Strict:
       {}
      Qed