MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { +(x, 0()) -> x
  , +(x, s(y)) -> s(+(x, y))
  , *(x, 0()) -> 0()
  , *(x, s(y)) -> +(*(x, y), x)
  , ge(x, 0()) -> true()
  , ge(0(), s(y)) -> false()
  , ge(s(x), s(y)) -> ge(x, y)
  , -(x, 0()) -> x
  , -(s(x), s(y)) -> -(x, y)
  , fact(x) -> iffact(x, ge(x, s(s(0()))))
  , iffact(x, true()) -> *(x, fact(-(x, s(0()))))
  , iffact(x, false()) -> s(0()) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..