We can list all the possible combinations of values for each variable, and check that, for each combination, if the left part of the sequent is true then the right part is also true.

Working with variables, you will have to test cases.

The problem here are quantifiers, since now there's a domain involved. And we're not able to list some of the possible existing domains, since a domain can have infinite elements.

Daniel Clemente Laboreo 2005-05-17