# Semantic Tableaux in First-Order logic: How does it work?

I'm really struggling on how to resolve a Semantic Tableaux in FOL. I've read a lot of explanations but in simple I really don't understand the exact algorithm and I have not found something similar.

I know the basic rules, like instantiation of different constants for different existential quantifiers, don't eliminate universally quantified formulas and so on...

I think my problem is that I don't understand how and with which criteria the constants are substituted in the universally quantified formula.