On the Completeness of Theory-Based Variants of Resolution