L. Pinto & R. Dyckhoff, Loop-free construction of counter-models for intuitionistic propositional logic, in: Symposia Gaussiana, Conf. A, Eds.: Behara/Fritsch/Lintz, Walter de Gruyter & Co, Berlin, New York, 1995, pp 225-232..
should be amended by the addition (to the refutation calculus) of a rule for dealing with formulae of the form F->B in the antecedent (where "F" is absurdity, falsum). The rule is
Gamma =/=> Delta ---------------------- Gamma, F->B =/=> Delta
The omission of a corresponding rule from the proof calculus is deliberate: it is an instance of the admissible rule of weakening.