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