How to reduce backtracking in propositional intuitionistic logic