MAYBE
Time: 0.003231
TRS:
 { plus(x, 0()) -> x,
   plus(x, s y) -> s plus(x, y),
  times(x, 0()) -> 0(),
  times(0(), y) -> 0(),
  times(s x, y) -> plus(times(x, y), y),
        p s 0() -> 0(),
        p s s x -> s p s x,
        fac s x -> times(fac p s x, s x)}
 DP:
  DP:
   { plus#(x, s y) -> plus#(x, y),
    times#(s x, y) -> plus#(times(x, y), y),
    times#(s x, y) -> times#(x, y),
          p# s s x -> p# s x,
          fac# s x -> times#(fac p s x, s x),
          fac# s x -> p# s x,
          fac# s x -> fac# p s x}
  TRS:
  { plus(x, 0()) -> x,
    plus(x, s y) -> s plus(x, y),
   times(x, 0()) -> 0(),
   times(0(), y) -> 0(),
   times(s x, y) -> plus(times(x, y), y),
         p s 0() -> 0(),
         p s s x -> s p s x,
         fac s x -> times(fac p s x, s x)}
  UR:
   { plus(x, 0()) -> x,
     plus(x, s y) -> s plus(x, y),
    times(x, 0()) -> 0(),
    times(0(), y) -> 0(),
    times(s x, y) -> plus(times(x, y), y),
          p s 0() -> 0(),
          p s s x -> s p s x,
          fac s x -> times(fac p s x, s x),
          a(z, w) -> z,
          a(z, w) -> w}
   EDG:
    {(times#(s x, y) -> plus#(times(x, y), y), plus#(x, s y) -> plus#(x, y))
     (plus#(x, s y) -> plus#(x, y), plus#(x, s y) -> plus#(x, y))
     (p# s s x -> p# s x, p# s s x -> p# s x)
     (fac# s x -> p# s x, p# s s x -> p# s x)
     (times#(s x, y) -> times#(x, y), times#(s x, y) -> plus#(times(x, y), y))
     (times#(s x, y) -> times#(x, y), times#(s x, y) -> times#(x, y))
     (fac# s x -> times#(fac p s x, s x), times#(s x, y) -> plus#(times(x, y), y))
     (fac# s x -> times#(fac p s x, s x), times#(s x, y) -> times#(x, y))
     (fac# s x -> fac# p s x, fac# s x -> times#(fac p s x, s x))
     (fac# s x -> fac# p s x, fac# s x -> p# s x)
     (fac# s x -> fac# p s x, fac# s x -> fac# p s x)}
    STATUS:
     arrows: 0.775510
     SCCS (4):
      Scc:
       {fac# s x -> fac# p s x}
      Scc:
       {p# s s x -> p# s x}
      Scc:
       {times#(s x, y) -> times#(x, y)}
      Scc:
       {plus#(x, s y) -> plus#(x, y)}
      
      SCC (1):
       Strict:
        {fac# s x -> fac# p s x}
       Weak:
       { plus(x, 0()) -> x,
         plus(x, s y) -> s plus(x, y),
        times(x, 0()) -> 0(),
        times(0(), y) -> 0(),
        times(s x, y) -> plus(times(x, y), y),
              p s 0() -> 0(),
              p s s x -> s p s x,
              fac s x -> times(fac p s x, s x)}
       Open
      
      SCC (1):
       Strict:
        {p# s s x -> p# s x}
       Weak:
       { plus(x, 0()) -> x,
         plus(x, s y) -> s plus(x, y),
        times(x, 0()) -> 0(),
        times(0(), y) -> 0(),
        times(s x, y) -> plus(times(x, y), y),
              p s 0() -> 0(),
              p s s x -> s p s x,
              fac s x -> times(fac p s x, s x)}
       Open
      
      SCC (1):
       Strict:
        {times#(s x, y) -> times#(x, y)}
       Weak:
       { plus(x, 0()) -> x,
         plus(x, s y) -> s plus(x, y),
        times(x, 0()) -> 0(),
        times(0(), y) -> 0(),
        times(s x, y) -> plus(times(x, y), y),
              p s 0() -> 0(),
              p s s x -> s p s x,
              fac s x -> times(fac p s x, s x)}
       Open
      
      SCC (1):
       Strict:
        {plus#(x, s y) -> plus#(x, y)}
       Weak:
       { plus(x, 0()) -> x,
         plus(x, s y) -> s plus(x, y),
        times(x, 0()) -> 0(),
        times(0(), y) -> 0(),
        times(s x, y) -> plus(times(x, y), y),
              p s 0() -> 0(),
              p s s x -> s p s x,
              fac s x -> times(fac p s x, s x)}
       Open