Conjecture (1) of [Ma83] is confirmed here by the following result: if 3 ≤ α < ω, then there is a finite relation algebra of dimension α, which is not a relation algebra of dimension α + 1. A logical consequence of this theorem is that for every finite α ≥ 3 there is a formula of the form S ⊆ T (asserting that one binary relation is included in another), which is provable with α + 1 variables, but not provable with only α variables (using a special sequent calculus designed for deducing properties of binary relations).
