  We investigate the equational theory of Kleene algebra terms with variable
complements -- (language) complement where it applies only to variables --
w.r.t. languages. While the equational theory w.r.t. languages coincides with
the language equivalence (under the standard language valuation) for Kleene
algebra terms, this coincidence is broken if we extend the terms with
complements. In this paper, we prove the decidability of some fragments of the
equational theory: the universality problem is coNP-complete, and the
inequational theory t <= s is coNP-complete when t does not contain
Kleene-star. To this end, we introduce words-to-letters valuations; they are
sufficient valuations for the equational theory and ease us in investigating
the equational theory w.r.t. languages. Additionally, we prove that for words
with variable complements, the equational theory coincides with the word
equivalence.
