MAYBE
Time: 0.002481
TRS:
 { if(true(), X, Y) -> X,
  if(false(), X, Y) -> Y,
           zero s X -> false(),
           zero 0() -> true(),
       prod(s X, Y) -> add(Y, prod(X, Y)),
       prod(0(), X) -> 0(),
             fact X -> if(zero X, s 0(), prod(X, fact p X)),
              p s X -> X,
        add(s X, Y) -> s add(X, Y),
        add(0(), X) -> X}
 DP:
  DP:
   {prod#(s X, Y) -> prod#(X, Y),
    prod#(s X, Y) -> add#(Y, prod(X, Y)),
          fact# X -> if#(zero X, s 0(), prod(X, fact p X)),
          fact# X -> zero# X,
          fact# X -> prod#(X, fact p X),
          fact# X -> fact# p X,
          fact# X -> p# X,
     add#(s X, Y) -> add#(X, Y)}
  TRS:
  { if(true(), X, Y) -> X,
   if(false(), X, Y) -> Y,
            zero s X -> false(),
            zero 0() -> true(),
        prod(s X, Y) -> add(Y, prod(X, Y)),
        prod(0(), X) -> 0(),
              fact X -> if(zero X, s 0(), prod(X, fact p X)),
               p s X -> X,
         add(s X, Y) -> s add(X, Y),
         add(0(), X) -> X}
  UR:
   { if(true(), X, Y) -> X,
    if(false(), X, Y) -> Y,
             zero s X -> false(),
             zero 0() -> true(),
         prod(s X, Y) -> add(Y, prod(X, Y)),
         prod(0(), X) -> 0(),
               fact X -> if(zero X, s 0(), prod(X, fact p X)),
                p s X -> X,
          add(s X, Y) -> s add(X, Y),
          add(0(), X) -> X,
              a(x, y) -> x,
              a(x, y) -> y}
   EDG:
    {(prod#(s X, Y) -> add#(Y, prod(X, Y)), add#(s X, Y) -> add#(X, Y))
     (fact# X -> fact# p X, fact# X -> p# X)
     (fact# X -> fact# p X, fact# X -> fact# p X)
     (fact# X -> fact# p X, fact# X -> prod#(X, fact p X))
     (fact# X -> fact# p X, fact# X -> zero# X)
     (fact# X -> fact# p X, fact# X -> if#(zero X, s 0(), prod(X, fact p X)))
     (add#(s X, Y) -> add#(X, Y), add#(s X, Y) -> add#(X, Y))
     (prod#(s X, Y) -> prod#(X, Y), prod#(s X, Y) -> prod#(X, Y))
     (prod#(s X, Y) -> prod#(X, Y), prod#(s X, Y) -> add#(Y, prod(X, Y)))
     (fact# X -> prod#(X, fact p X), prod#(s X, Y) -> prod#(X, Y))
     (fact# X -> prod#(X, fact p X), prod#(s X, Y) -> add#(Y, prod(X, Y)))}
    STATUS:
     arrows: 0.828125
     SCCS (3):
      Scc:
       {fact# X -> fact# p X}
      Scc:
       {prod#(s X, Y) -> prod#(X, Y)}
      Scc:
       {add#(s X, Y) -> add#(X, Y)}
      
      SCC (1):
       Strict:
        {fact# X -> fact# p X}
       Weak:
       { if(true(), X, Y) -> X,
        if(false(), X, Y) -> Y,
                 zero s X -> false(),
                 zero 0() -> true(),
             prod(s X, Y) -> add(Y, prod(X, Y)),
             prod(0(), X) -> 0(),
                   fact X -> if(zero X, s 0(), prod(X, fact p X)),
                    p s X -> X,
              add(s X, Y) -> s add(X, Y),
              add(0(), X) -> X}
       Open
      
      
      
      
      SCC (1):
       Strict:
        {prod#(s X, Y) -> prod#(X, Y)}
       Weak:
       { if(true(), X, Y) -> X,
        if(false(), X, Y) -> Y,
                 zero s X -> false(),
                 zero 0() -> true(),
             prod(s X, Y) -> add(Y, prod(X, Y)),
             prod(0(), X) -> 0(),
                   fact X -> if(zero X, s 0(), prod(X, fact p X)),
                    p s X -> X,
              add(s X, Y) -> s add(X, Y),
              add(0(), X) -> X}
       Open
      
      SCC (1):
       Strict:
        {add#(s X, Y) -> add#(X, Y)}
       Weak:
       { if(true(), X, Y) -> X,
        if(false(), X, Y) -> Y,
                 zero s X -> false(),
                 zero 0() -> true(),
             prod(s X, Y) -> add(Y, prod(X, Y)),
             prod(0(), X) -> 0(),
                   fact X -> if(zero X, s 0(), prod(X, fact p X)),
                    p s X -> X,
              add(s X, Y) -> s add(X, Y),
              add(0(), X) -> X}
       Open