YES

Problem:
 p(s(x)) -> x
 fac(0()) -> s(0())
 fac(s(x)) -> times(s(x),fac(p(s(x))))

Proof:
 DP Processor:
  DPs:
   fac#(s(x)) -> p#(s(x))
   fac#(s(x)) -> fac#(p(s(x)))
  TRS:
   p(s(x)) -> x
   fac(0()) -> s(0())
   fac(s(x)) -> times(s(x),fac(p(s(x))))
  EDG Processor:
   DPs:
    fac#(s(x)) -> p#(s(x))
    fac#(s(x)) -> fac#(p(s(x)))
   TRS:
    p(s(x)) -> x
    fac(0()) -> s(0())
    fac(s(x)) -> times(s(x),fac(p(s(x))))
   graph:
    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)))
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 2/4
    DPs:
     fac#(s(x)) -> fac#(p(s(x)))
    TRS:
     p(s(x)) -> x
     fac(0()) -> s(0())
     fac(s(x)) -> times(s(x),fac(p(s(x))))
    Bounds Processor:
     bound: 2
     enrichment: roof
     automaton:
      final states: {8}
      transitions:
       fac{#,2}(16) -> 8*
       times0(7,7) -> 7*
       times1(11,14) -> 14,7
       s1(7) -> 11*
       s1(13) -> 7*
       fac1(12) -> 14*
       p1(7) -> 12*
       p1(11) -> 12*
       01() -> 13*
       fac{#,1}(12) -> 8*
       times2(15,18) -> 14*
       fac{#,0}(7) -> 8*
       s2(17) -> 18,14
       s2(13) -> 15*
       s0(7) -> 7*
       fac2(16) -> 18*
       p0(7) -> 7*
       p2(15) -> 16*
       fac0(7) -> 7*
       02() -> 17*
       00() -> 7*
       7 -> 12*
       13 -> 16,7
     problem:
      DPs:
       
      TRS:
       p(s(x)) -> x
       fac(0()) -> s(0())
       fac(s(x)) -> times(s(x),fac(p(s(x))))
     Qed