MAYBE
Time: 0.001954
TRS:
 {    p s x -> x,
   fact s x -> *(s x, fact p s x),
   fact 0() -> s 0(),
  *(s x, y) -> +(*(x, y), y),
  *(0(), y) -> 0(),
  +(x, s y) -> s +(x, y),
  +(x, 0()) -> x}
 DP:
  DP:
   { fact# s x -> p# s x,
     fact# s x -> fact# p s x,
     fact# s x -> *#(s x, fact p s x),
    *#(s x, y) -> *#(x, y),
    *#(s x, y) -> +#(*(x, y), y),
    +#(x, s y) -> +#(x, y)}
  TRS:
  {    p s x -> x,
    fact s x -> *(s x, fact p s x),
    fact 0() -> s 0(),
   *(s x, y) -> +(*(x, y), y),
   *(0(), y) -> 0(),
   +(x, s y) -> s +(x, y),
   +(x, 0()) -> x}
  UR:
   {    p s x -> x,
     fact s x -> *(s x, fact p s x),
     fact 0() -> s 0(),
    *(s x, y) -> +(*(x, y), y),
    *(0(), y) -> 0(),
    +(x, s y) -> s +(x, y),
    +(x, 0()) -> x,
      a(z, w) -> z,
      a(z, w) -> w}
   EDG:
    {(*#(s x, y) -> *#(x, y), *#(s x, y) -> +#(*(x, y), y))
     (*#(s x, y) -> *#(x, y), *#(s x, y) -> *#(x, y))
     (fact# s x -> *#(s x, fact p s x), *#(s x, y) -> +#(*(x, y), y))
     (fact# s x -> *#(s x, fact p s x), *#(s x, y) -> *#(x, y))
     (*#(s x, y) -> +#(*(x, y), y), +#(x, s y) -> +#(x, y))
     (+#(x, s y) -> +#(x, y), +#(x, s y) -> +#(x, y))
     (fact# s x -> fact# p s x, fact# s x -> p# s x)
     (fact# s x -> fact# p s x, fact# s x -> fact# p s x)
     (fact# s x -> fact# p s x, fact# s x -> *#(s x, fact p s x))}
    STATUS:
     arrows: 0.750000
     SCCS (3):
      Scc:
       {fact# s x -> fact# p s x}
      Scc:
       {*#(s x, y) -> *#(x, y)}
      Scc:
       {+#(x, s y) -> +#(x, y)}
      
      SCC (1):
       Strict:
        {fact# s x -> fact# p s x}
       Weak:
       {    p s x -> x,
         fact s x -> *(s x, fact p s x),
         fact 0() -> s 0(),
        *(s x, y) -> +(*(x, y), y),
        *(0(), y) -> 0(),
        +(x, s y) -> s +(x, y),
        +(x, 0()) -> x}
       Open
      
      SCC (1):
       Strict:
        {*#(s x, y) -> *#(x, y)}
       Weak:
       {    p s x -> x,
         fact s x -> *(s x, fact p s x),
         fact 0() -> s 0(),
        *(s x, y) -> +(*(x, y), y),
        *(0(), y) -> 0(),
        +(x, s y) -> s +(x, y),
        +(x, 0()) -> x}
       Open
      
      SCC (1):
       Strict:
        {+#(x, s y) -> +#(x, y)}
       Weak:
       {    p s x -> x,
         fact s x -> *(s x, fact p s x),
         fact 0() -> s 0(),
        *(s x, y) -> +(*(x, y), y),
        *(0(), y) -> 0(),
        +(x, s y) -> s +(x, y),
        +(x, 0()) -> x}
       Open