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