MAYBE
Time: 0.008538
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:
  DP:
   { 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())}
  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())}
  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)}
   STATUS:
    arrows: 0.800000
    SCCS (4):
     Scc:
      {fac#(s x, y) -> fac#(p s x, times(s x, y))}
     Scc:
      {times#(s x, y) -> times#(p s x, y)}
     Scc:
      {plus#(s x, y) -> plus#(p s x, y)}
     Scc:
      {p# s s x -> p# s x}
     
     
     SCC (1):
      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())}
      Open
     
     SCC (1):
      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())}
      Open
     
     
     
     SCC (1):
      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())}
      Open
     
     SCC (1):
      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())}
      Open