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