MAYBE
Time: 0.244269
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())}
  UR:
   { 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)),
          a(z, w) -> z,
          a(z, w) -> w}
   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())}
       Fail
      
      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())}
       Fail
      
      
      
      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())}
       Fail
      
      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())}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [plus](x0, x1) = x0 + 1,
         
         [times](x0, x1) = x0 + 1,
         
         [fac](x0, x1) = x0 + 1,
         
         [s](x0) = x0 + 1,
         
         [p](x0) = 0,
         
         [factorial](x0) = 0,
         
         [0] = 1,
         
         [p#](x0) = x0
        Strict:
         p# s s x -> p# s x
         2 + 1x >= 1 + 1x
        Weak:
         factorial x -> fac(x, s 0())
         0 + 0x >= 1 + 1x
         fac(s x, y) -> fac(p s x, times(s x, y))
         2 + 1x + 0y >= 1 + 0x + 0y
         fac(0(), x) -> x
         2 + 0x >= 1x
         times(s x, y) -> plus(y, times(p s x, y))
         2 + 1x + 0y >= 1 + 0x + 1y
         times(0(), y) -> 0()
         2 + 0y >= 1
         p s s x -> s p s x
         0 + 0x >= 1 + 0x
         p s 0() -> 0()
         0 >= 1
         plus(s x, y) -> s plus(p s x, y)
         2 + 1x + 0y >= 2 + 0x + 0y
         plus(0(), x) -> x
         2 + 0x >= 1x
       Qed