Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs