YES
Time: 0.008353
TRS:
 {  p s x -> x,
  fac s x -> times(s x, fac p s x),
  fac 0() -> s 0()}
 DP:
  DP:
   {fac# s x -> p# s x,
    fac# s x -> fac# p s x}
  TRS:
  {  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 (1):
    Scc:
     {fac# s x -> fac# p s x}
    SCC (1):
     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