MAYBE
Trs:
 {         +(x, 0()) -> x,
          +(x, s(y)) -> s(+(x, y)),
       ge(0(), s(y)) -> false(),
      ge(s(x), s(y)) -> ge(x, y),
          ge(x, 0()) -> true(),
       -(s(x), s(y)) -> -(x, y),
           -(x, 0()) -> x,
             fact(x) -> iffact(x, ge(x, s(s(0())))),
           *(x, 0()) -> 0(),
          *(x, s(y)) -> +(*(x, y), x),
   iffact(x, true()) -> *(x, fact(-(x, s(0())))),
  iffact(x, false()) -> s(0())}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open