MAYBE
TRS:
 { fac(s(x)) -> *(fac(p(s(x))), s(x)),
  p(s(s(x))) -> s(p(s(x))),
   p(s(0())) -> 0()}
 DP:
  Strict:
   { fac#(s(x)) -> fac#(p(s(x))),
     fac#(s(x)) -> p#(s(x)),
    p#(s(s(x))) -> p#(s(x))}
  Weak:
  { fac(s(x)) -> *(fac(p(s(x))), s(x)),
   p(s(s(x))) -> s(p(s(x))),
    p(s(0())) -> 0()}
  EDG:
   {(fac#(s(x)) -> p#(s(x)), p#(s(s(x))) -> p#(s(x)))
    (p#(s(s(x))) -> p#(s(x)), p#(s(s(x))) -> p#(s(x)))
    (fac#(s(x)) -> fac#(p(s(x))), fac#(s(x)) -> fac#(p(s(x))))
    (fac#(s(x)) -> fac#(p(s(x))), fac#(s(x)) -> p#(s(x)))}
   SCCS:
    Scc:
     {p#(s(s(x))) -> p#(s(x))}
    Scc:
     {fac#(s(x)) -> fac#(p(s(x)))}
    SCC:
     Strict:
      {p#(s(s(x))) -> p#(s(x))}
     Weak:
     { fac(s(x)) -> *(fac(p(s(x))), s(x)),
      p(s(s(x))) -> s(p(s(x))),
       p(s(0())) -> 0()}
     SPSC:
      Simple Projection:
       pi(p#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {fac#(s(x)) -> fac#(p(s(x)))}
     Weak:
     { fac(s(x)) -> *(fac(p(s(x))), s(x)),
      p(s(s(x))) -> s(p(s(x))),
       p(s(0())) -> 0()}
     Fail