I just stumbled upon this old question by chance, and I thought maybe you should have a look at Alexandre Miquel's thesis if you haven't already done so (and if you can read French). Conjecture 9.7.12 on page 329 (331 of PDF) suggests that the Calculus of Constructions with universes should be equiconsistent with Zermelo set theory with universes (assuming I'm not misreading—I'm easily confused between all these theories), which at least gives some lower bound.

I just stumbled upon this old question by chance, and I thought maybe you should have a look at Alexandre Miquel's thesis if you haven't already done so (and if you can read French). Conjecture 9.7.12 on page 329 (331 of PDF) suggests that the Calculus of Constructions with universes should be equiconsistent with Zermelo set theory with universes (assuming I'm not misreading—I'm easily confused between all these theories), which at least gives some lower bound.