Intuitionistic Strong Löb logic ISL is a well-known intuitionistic modal logic with a provability interpretation. We introduce GbuSL a terminating sequent calculus with the subformula property for ISL. GbuSL modifies the sequent calculus G3iSL for iSL based on G3i, by annotating the sequents to distinguish rule applications into an unblocked phase, where any rule can be backward applied, and a blocked phase where only right rules can be used. We prove that, if proof-search for a sequent s in GbuSL fails, then a Kripke countermodel for s can be constructed.