We present a terminating sequent calculus for the propositional Göinvertible; we argue that one may thus derive a calculus of refutations (in the traditional sense, not the sense used in some books on automated reasoning; thus a refutation is a syntactic structure showing non-provability rather than showing inconsistency) and that the refutation calculus is non-branching, hence the possibility of extracting linear counter-models. Thus, rule invertibility is a feature not only of classical logic but also of logics with linear characteristic models.