TRS:
 {       lt(0(), s(x)) -> true(),
            lt(x, 0()) -> false(),
        lt(s(x), s(y)) -> lt(x, y),
         times(0(), y) -> 0(),
        times(s(x), y) -> plus(y, times(x, y)),
          plus(0(), y) -> y,
         plus(s(x), y) -> s(plus(x, y)),
                fac(x) -> loop(x, s(0()), s(0())),
         loop(x, c, y) -> if(lt(x, c), x, c, y),
  if(false(), x, c, y) -> loop(x, s(c), times(y, s(c))),
   if(true(), x, c, y) -> y}
 Fail