YES
TRS:
 {  p(s(x)) -> x,
  fac(s(x)) -> times(s(x), fac(p(s(x)))),
   fac(0()) -> s(0())}
 DP:
  Strict:
   {fac#(s(x)) -> p#(s(x)),
    fac#(s(x)) -> fac#(p(s(x)))}
  Weak:
  {  p(s(x)) -> x,
   fac(s(x)) -> times(s(x), fac(p(s(x)))),
    fac(0()) -> s(0())}
  EDG:
   {(fac#(s(x)) -> fac#(p(s(x))), fac#(s(x)) -> p#(s(x)))
    (fac#(s(x)) -> fac#(p(s(x))), fac#(s(x)) -> fac#(p(s(x))))}
   SCCS:
    Scc:
     {fac#(s(x)) -> fac#(p(s(x)))}
    SCC:
     Strict:
      {fac#(s(x)) -> fac#(p(s(x)))}
     Weak:
     {  p(s(x)) -> x,
      fac(s(x)) -> times(s(x), fac(p(s(x)))),
       fac(0()) -> s(0())}
     BOUND:
      Bound: roof(-raise)-bounded by 2
      Automaton:
       {times_2(7, 9) -> 5*
        times_1(3, 5) -> 5 | 1
        times_0(1, 1) -> 1*
            fac#_2(8) -> 1*
            fac#_1(4) -> 1*
            fac#_0(1) -> 1*
             fac_2(8) -> 9*
             fac_1(4) -> 5*
             fac_0(1) -> 1*
                0_2() -> 6*
                0_1() -> 2*
                0_0() -> 1*
               s_2(6) -> 9 | 5
               s_2(2) -> 7*
               s_1(2) -> 5 | 1
               s_1(1) -> 3*
               s_0(1) -> 1*
               p_2(7) -> 8*
               p_1(3) -> 4*
               p_0(1) -> 1*
                    2 -> 8 | 1
                    1 -> 4*}
      Strict:
       {}
      Qed