TRS:
 {        plus(0(), x) -> x,
         plus(s(x), y) -> s(plus(x, y)),
         times(0(), y) -> 0(),
        times(s(x), y) -> plus(y, times(x, y)),
               p(s(x)) -> x,
                p(0()) -> 0(),
         minus(x, 0()) -> x,
         minus(0(), x) -> 0(),
        minus(x, s(y)) -> p(minus(x, y)),
           isZero(0()) -> true(),
          isZero(s(x)) -> false(),
         facIter(x, y) -> if(isZero(x), minus(x, s(0())), y, times(y, x)),
   if(true(), x, y, z) -> y,
  if(false(), x, y, z) -> facIter(x, z),
          factorial(x) -> facIter(x, s(0()))}
 Fail