YES
TRS:
 {   p(s(x)) -> x,
  fact(s(x)) -> *(s(x), fact(p(s(x)))),
   fact(0()) -> s(0()),
  *(s(x), y) -> +(*(x, y), y),
   *(0(), y) -> 0(),
  +(x, s(y)) -> s(+(x, y)),
   +(x, 0()) -> x}
 DP:
  Strict:
   {fact#(s(x)) -> p#(s(x)),
    fact#(s(x)) -> fact#(p(s(x))),
    fact#(s(x)) -> *#(s(x), fact(p(s(x)))),
    *#(s(x), y) -> *#(x, y),
    *#(s(x), y) -> +#(*(x, y), y),
    +#(x, s(y)) -> +#(x, y)}
  Weak:
  {   p(s(x)) -> x,
   fact(s(x)) -> *(s(x), fact(p(s(x)))),
    fact(0()) -> s(0()),
   *(s(x), y) -> +(*(x, y), y),
    *(0(), y) -> 0(),
   +(x, s(y)) -> s(+(x, y)),
    +(x, 0()) -> x}
  EDG:
   {(*#(s(x), y) -> *#(x, y), *#(s(x), y) -> +#(*(x, y), y))
    (*#(s(x), y) -> *#(x, y), *#(s(x), y) -> *#(x, y))
    (fact#(s(x)) -> *#(s(x), fact(p(s(x)))), *#(s(x), y) -> +#(*(x, y), y))
    (fact#(s(x)) -> *#(s(x), fact(p(s(x)))), *#(s(x), y) -> *#(x, y))
    (*#(s(x), y) -> +#(*(x, y), y), +#(x, s(y)) -> +#(x, y))
    (+#(x, s(y)) -> +#(x, y), +#(x, s(y)) -> +#(x, y))
    (fact#(s(x)) -> fact#(p(s(x))), fact#(s(x)) -> p#(s(x)))
    (fact#(s(x)) -> fact#(p(s(x))), fact#(s(x)) -> fact#(p(s(x))))
    (fact#(s(x)) -> fact#(p(s(x))), fact#(s(x)) -> *#(s(x), fact(p(s(x)))))}
   SCCS:
    Scc:
     {+#(x, s(y)) -> +#(x, y)}
    Scc:
     {*#(s(x), y) -> *#(x, y)}
    Scc:
     {fact#(s(x)) -> fact#(p(s(x)))}
    SCC:
     Strict:
      {+#(x, s(y)) -> +#(x, y)}
     Weak:
     {   p(s(x)) -> x,
      fact(s(x)) -> *(s(x), fact(p(s(x)))),
       fact(0()) -> s(0()),
      *(s(x), y) -> +(*(x, y), y),
       *(0(), y) -> 0(),
      +(x, s(y)) -> s(+(x, y)),
       +(x, 0()) -> x}
     SPSC:
      Simple Projection:
       pi(+#) = 1
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {*#(s(x), y) -> *#(x, y)}
     Weak:
     {   p(s(x)) -> x,
      fact(s(x)) -> *(s(x), fact(p(s(x)))),
       fact(0()) -> s(0()),
      *(s(x), y) -> +(*(x, y), y),
       *(0(), y) -> 0(),
      +(x, s(y)) -> s(+(x, y)),
       +(x, 0()) -> x}
     SPSC:
      Simple Projection:
       pi(*#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {fact#(s(x)) -> fact#(p(s(x)))}
     Weak:
     {   p(s(x)) -> x,
      fact(s(x)) -> *(s(x), fact(p(s(x)))),
       fact(0()) -> s(0()),
      *(s(x), y) -> +(*(x, y), y),
       *(0(), y) -> 0(),
      +(x, s(y)) -> s(+(x, y)),
       +(x, 0()) -> x}
     UR:
      {p(s(x)) -> x}
      BOUND:
       Bound: match(-raise)-DP-bounded by 1
       Automaton:
        {fact#_1(13) -> 14*
         fact#_0(10) -> 4*
             s_1(17) -> 18*
             s_1(15) -> 16*
             s_1(11) -> 12*
             s_0(10) -> 9*
              s_0(9) -> 9*
              s_0(7) -> 9*
             p_1(12) -> 13*
             p_0(10) -> 7*
              p_0(9) -> 10*
              p_0(7) -> 7*
                  18 -> 12*
                  17 -> 13*
                  16 -> 12*
                  15 -> 13*
                  14 -> 4*
                  11 -> 13*
                  10 -> 17 | 7
                   9 -> 15 | 10 | 7
                   7 -> 11 | 10}
       Strict:
        {}
       Qed