Bounded variable elimination is one of the most important preprocessing techniques in
SAT solving. It benefits from discovering functional dependencies in the form of definitions encoded in the CNF. While the original approach relied on syntactic pattern matching our new approach uses cores produced by an embedded SAT solver. In contrast to a similar semantic approach in Lingeling based on BDD algorithms, our new approach is able to generate DRAT proofs. We further discuss design choices for our embedded SAT solver Kitten. xperiments with Kissat show the ffectiveness of this approach.