Is non-monotonic reasoning always harder?

Although it has been shown that non-monotonic reasoning is presumably harder than classical reasoning, there are cases where a non-monotonic treatment actually simplifies matters. Indeed, one of the reasons for considering non-monotonic systems is the hope of speeding up reasoning, and not to slow it down. In this paper, we consider proof lengths in a cut-free sequent calculus, and we show that the application of circumscription (or completion) to certain first-order formulae leads to a non-elementary speed-up of proof length. This is possible because the introduction of the completion formula can simulate the cut rule.