MAYBE
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:
  Strict:
   {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)}
  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}
  EDG:
   {(prod#(s(X), Y) -> add#(Y, prod(X, Y)), add#(s(X), Y) -> add#(X, Y))
    (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) -> fact#(p(X)), fact#(X) -> if#(zero(X), s(0()), prod(X, fact(p(X)))))
    (fact#(X) -> fact#(p(X)), fact#(X) -> zero#(X))
    (fact#(X) -> fact#(p(X)), fact#(X) -> prod#(X, fact(p(X))))
    (fact#(X) -> fact#(p(X)), fact#(X) -> fact#(p(X)))
    (fact#(X) -> fact#(p(X)), fact#(X) -> p#(X))
    (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)))}
   SCCS:
    Scc:
     {add#(s(X), Y) -> add#(X, Y)}
    Scc:
     {fact#(X) -> fact#(p(X))}
    Scc:
     {prod#(s(X), Y) -> prod#(X, Y)}
    SCC:
     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}
     SPSC:
      Simple Projection:
       pi(add#) = 0
      Strict:
       {}
      Qed
    SCC:
     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}
     Fail
    SCC:
     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}
     SPSC:
      Simple Projection:
       pi(prod#) = 0
      Strict:
       {}
      Qed