Two-variable logic with counting is decidable

We prove that the satisfiability and the finite satisfiability problems for C² are decidable. C² is first-order logic with only two variables in the presence of arbitrary counting quantifiers 3^⩾m,m⩾1. It considerably extends L² plain first-order with only two variables, which is known to be decidable by a result of Mortimer´s. Unlike L², C² does not have the finite model property