MAYBE
Time: 0.009940
TRS:
 {fac s x -> *(fac p s x, s x),
  p s s x -> s p s x,
  p s 0() -> 0()}
 DP:
  DP:
   {fac# s x -> fac# p s x,
    fac# s x -> p# s x,
    p# s s x -> p# s x}
  TRS:
  {fac s x -> *(fac p s x, s x),
   p s s x -> s p s x,
   p s 0() -> 0()}
  EDG:
   {(fac# s x -> p# s x, p# s s x -> p# s x)
    (p# s s x -> p# s x, p# s s x -> p# s x)
    (fac# s x -> fac# p s x, fac# s x -> fac# p s x)
    (fac# s x -> fac# p s x, fac# s x -> p# s x)}
   STATUS:
    arrows: 0.555556
    SCCS (2):
     Scc:
      {fac# s x -> fac# p s x}
     Scc:
      {p# s s x -> p# s x}
     
     SCC (1):
      Strict:
       {fac# s x -> fac# p s x}
      Weak:
      {fac s x -> *(fac p s x, s x),
       p s s x -> s p s x,
       p s 0() -> 0()}
      Fail
     
     SCC (1):
      Strict:
       {p# s s x -> p# s x}
      Weak:
      {fac s x -> *(fac p s x, s x),
       p s s x -> s p s x,
       p s 0() -> 0()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [*](x0, x1) = x0 + 1,
        
        [fac](x0) = x0 + 1,
        
        [p](x0) = 0,
        
        [s](x0) = x0 + 1,
        
        [0] = 0,
        
        [p#](x0) = x0
       Strict:
        p# s s x -> p# s x
        2 + 1x >= 1 + 1x
       Weak:
        p s 0() -> 0()
        0 >= 0
        p s s x -> s p s x
        0 + 0x >= 1 + 0x
        fac s x -> *(fac p s x, s x)
        2 + 1x >= 2 + 1x
      Qed