Trouver des modèles pour une séquente

Question

J'essaie de générer des modèles pour la séquente suivante.

$$ existe x existe y forall z (z = x lor z = y) $$

Ce que j'ai trouvé, c'est ceci.

$$ a = {0,1 } $$

Donc, dans ce modèle, pour toutes les valeurs de $ z $, il existe $ x $ tel que $ z = x $ ou il existe $ y $ tel que $ z = y $. Ce modèle est-il correct? Quels autres modèles y a-t-il qui satisfont cela?