Small model property reflects in games and automata

Let's choose a logic theory having the small model property. I will show that the size of the small model used in the definition of the property can be directly used to show a limit on the number of maximal variables 1n an Aphrodite strategy in games for finding a proof. On the other hand I'll show that the size of the small model, with the numbers of variables and subformulas, can be used to construct a limit on the size of the set of eigenvariables of an Arcadian automaton.