I have tried to prove, in first order logic, that every satisfiable sentence (without function symbols) with at most two variables has a finite model. My attempts were unsuccessful.
This is an exercise from the (wider) model theory book written by Hodges (Encyclopedia of Mathematics and its Applications, Volume 42 - Model Theory, page 111). It follows an exercise about Immerman's pebble game, probably as an application.
It's easy to see that proving the following problem will suffice: given a structure A, prove that for every number n, there is a finite structure B such that player II has a winning strategy in immerman's pebble game of length n with 2 pebbles (between A and B).