TRS:
 {  p(s(x)) -> x,
   fac(0()) -> s(0()),
  fac(s(x)) -> times(s(x), fac(p(s(x))))}
 Fail