MAYBE
TRS:
 {         if(true(), X, Y) -> activate(X),
          if(false(), X, Y) -> activate(Y),
                  zero(0()) -> true(),
                 zero(s(X)) -> false(),
                    fact(X) -> if(zero(X), n__s(0()), n__prod(X, fact(p(X)))),
                    p(s(X)) -> X,
                add(0(), X) -> X,
               add(s(X), Y) -> s(add(X, Y)),
                       s(X) -> n__s(X),
               prod(X1, X2) -> n__prod(X1, X2),
               prod(0(), X) -> 0(),
              prod(s(X), Y) -> add(Y, prod(X, Y)),
                activate(X) -> X,
          activate(n__s(X)) -> s(X),
  activate(n__prod(X1, X2)) -> prod(X1, X2)}
 DP:
  Strict:
   {         if#(true(), X, Y) -> activate#(X),
            if#(false(), X, Y) -> activate#(Y),
                      fact#(X) -> if#(zero(X), n__s(0()), n__prod(X, fact(p(X)))),
                      fact#(X) -> zero#(X),
                      fact#(X) -> fact#(p(X)),
                      fact#(X) -> p#(X),
                 add#(s(X), Y) -> add#(X, Y),
                 add#(s(X), Y) -> s#(add(X, Y)),
                prod#(s(X), Y) -> add#(Y, prod(X, Y)),
                prod#(s(X), Y) -> prod#(X, Y),
            activate#(n__s(X)) -> s#(X),
    activate#(n__prod(X1, X2)) -> prod#(X1, X2)}
  Weak:
  {         if(true(), X, Y) -> activate(X),
           if(false(), X, Y) -> activate(Y),
                   zero(0()) -> true(),
                  zero(s(X)) -> false(),
                     fact(X) -> if(zero(X), n__s(0()), n__prod(X, fact(p(X)))),
                     p(s(X)) -> X,
                 add(0(), X) -> X,
                add(s(X), Y) -> s(add(X, Y)),
                        s(X) -> n__s(X),
                prod(X1, X2) -> n__prod(X1, X2),
                prod(0(), X) -> 0(),
               prod(s(X), Y) -> add(Y, prod(X, Y)),
                 activate(X) -> X,
           activate(n__s(X)) -> s(X),
   activate(n__prod(X1, X2)) -> prod(X1, X2)}
  EDG:
   {(prod#(s(X), Y) -> add#(Y, prod(X, Y)), add#(s(X), Y) -> s#(add(X, Y)))
    (prod#(s(X), Y) -> add#(Y, prod(X, Y)), add#(s(X), Y) -> add#(X, Y))
    (fact#(X) -> if#(zero(X), n__s(0()), n__prod(X, fact(p(X)))), if#(false(), X, Y) -> activate#(Y))
    (fact#(X) -> if#(zero(X), n__s(0()), n__prod(X, fact(p(X)))), if#(true(), X, Y) -> activate#(X))
    (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) -> p#(X))
    (fact#(X) -> fact#(p(X)), fact#(X) -> fact#(p(X)))
    (fact#(X) -> fact#(p(X)), fact#(X) -> zero#(X))
    (fact#(X) -> fact#(p(X)), fact#(X) -> if#(zero(X), n__s(0()), n__prod(X, fact(p(X)))))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__s(X)) -> s#(X))
    (if#(false(), X, Y) -> activate#(Y), activate#(n__prod(X1, X2)) -> prod#(X1, X2))
    (add#(s(X), Y) -> add#(X, Y), add#(s(X), Y) -> add#(X, Y))
    (add#(s(X), Y) -> add#(X, Y), add#(s(X), Y) -> s#(add(X, Y)))
    (activate#(n__prod(X1, X2)) -> prod#(X1, X2), prod#(s(X), Y) -> add#(Y, prod(X, Y)))
    (activate#(n__prod(X1, X2)) -> prod#(X1, X2), prod#(s(X), Y) -> prod#(X, Y))
    (if#(true(), X, Y) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (if#(true(), X, Y) -> activate#(X), activate#(n__prod(X1, X2)) -> prod#(X1, X2))}
   SCCS:
    Scc:
     {prod#(s(X), Y) -> prod#(X, Y)}
    Scc:
     {add#(s(X), Y) -> add#(X, Y)}
    Scc:
     {fact#(X) -> fact#(p(X))}
    SCC:
     Strict:
      {prod#(s(X), Y) -> prod#(X, Y)}
     Weak:
     {         if(true(), X, Y) -> activate(X),
              if(false(), X, Y) -> activate(Y),
                      zero(0()) -> true(),
                     zero(s(X)) -> false(),
                        fact(X) -> if(zero(X), n__s(0()), n__prod(X, fact(p(X)))),
                        p(s(X)) -> X,
                    add(0(), X) -> X,
                   add(s(X), Y) -> s(add(X, Y)),
                           s(X) -> n__s(X),
                   prod(X1, X2) -> n__prod(X1, X2),
                   prod(0(), X) -> 0(),
                  prod(s(X), Y) -> add(Y, prod(X, Y)),
                    activate(X) -> X,
              activate(n__s(X)) -> s(X),
      activate(n__prod(X1, X2)) -> prod(X1, X2)}
     SPSC:
      Simple Projection:
       pi(prod#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {add#(s(X), Y) -> add#(X, Y)}
     Weak:
     {         if(true(), X, Y) -> activate(X),
              if(false(), X, Y) -> activate(Y),
                      zero(0()) -> true(),
                     zero(s(X)) -> false(),
                        fact(X) -> if(zero(X), n__s(0()), n__prod(X, fact(p(X)))),
                        p(s(X)) -> X,
                    add(0(), X) -> X,
                   add(s(X), Y) -> s(add(X, Y)),
                           s(X) -> n__s(X),
                   prod(X1, X2) -> n__prod(X1, X2),
                   prod(0(), X) -> 0(),
                  prod(s(X), Y) -> add(Y, prod(X, Y)),
                    activate(X) -> X,
              activate(n__s(X)) -> s(X),
      activate(n__prod(X1, X2)) -> prod(X1, X2)}
     SPSC:
      Simple Projection:
       pi(add#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {fact#(X) -> fact#(p(X))}
     Weak:
     {         if(true(), X, Y) -> activate(X),
              if(false(), X, Y) -> activate(Y),
                      zero(0()) -> true(),
                     zero(s(X)) -> false(),
                        fact(X) -> if(zero(X), n__s(0()), n__prod(X, fact(p(X)))),
                        p(s(X)) -> X,
                    add(0(), X) -> X,
                   add(s(X), Y) -> s(add(X, Y)),
                           s(X) -> n__s(X),
                   prod(X1, X2) -> n__prod(X1, X2),
                   prod(0(), X) -> 0(),
                  prod(s(X), Y) -> add(Y, prod(X, Y)),
                    activate(X) -> X,
              activate(n__s(X)) -> s(X),
      activate(n__prod(X1, X2)) -> prod(X1, X2)}
     Fail