For example, given Theory T with predicates $$A(x), B(x), C(x,y), D(x,y), x=y$$ axioms $$\exists x.A(x) \land \exists x.B(x) \land \exists xy.C(x,y)\\ \forall x(A(x) \leftrightarrow \neg B(x)),$$ produce interpretation where formula $$\forall x\forall y(C(x, y) \to A(x))$$ is false.
How-do you solve problems like this? I have a suspicion that one should introduce objects into interpretation domain D and define their truth values (of course, following axioms) in a such way that there is object x that can produce true from predicate C while producing at the same time false from predicate A (the idea is that implication is false only in one case - when premise is true but consequence - false). Am I right?
Also I'm interested how does one prove that formula is satisfiable or not satisfiable in some interpretation and how does one produce interpretation that shows it.