Encodings of Bounded LTL Model Checking in Effectively Propositional Logic