Simple Bounded LTL Model Checking