TRS:
 {          fact(X) -> if(zero(X), s(0()), prod(X, fact(p(X)))),
        add(0(), X) -> X,
       add(s(X), Y) -> s(add(X, Y)),
       prod(0(), X) -> 0(),
      prod(s(X), Y) -> add(Y, prod(X, Y)),
   if(true(), X, Y) -> X,
  if(false(), X, Y) -> Y,
          zero(0()) -> true(),
         zero(s(X)) -> false(),
            p(s(X)) -> X}
 Fail