First-order logic: how-to produce interpretation where a given formula is false? 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.
 A: In general, finding an interpretation in which some sentence fails can be rather hard. But in this case, we have a very weak theory, and one of the predicates has no conditions on it.
We know that there are at least two things in any intepretation of this theory; there's a $B$ thing and an $A$ thing and nothing can be both. In fact ignoring the predicate $C$ entirely, we can make a model of the other axioms with exactly two elements. Then we figure out what we want $C$ to be. One can go even simpler than I did above and define $C:=\{\langle x,y\rangle: A(x)\vee\neg A(x).\wedge.A(y)\vee\neg A(y)\}$. Point is, we need $C(x,y)$ to be true when $A(x)$ is false; in this case, $C(x,y)$ is true of everything and we know one thing $A(x)$ is false of.
My inspiration for this intepretation was an intepretation in a natural language sense: a bag of Go stones with $A$ being "is a white stone", $B$ being "is a black stone" and $C(x,y)$ being defined as above. Trying to think of your predicates as predicates in some similar language is a good way to start getting ideas.
A: You are looking for a countermodel
A countermodel is a model (interpretation)  where all axioms are true and the statement you are investigating is false.
So in your case: when is $\forall x\forall y(C(x, y) \to A(x) )$ false?
It is false when $ \lnot \forall x\forall y(C(x, y) \to A(x) )$ is true.
When $\exists x \exists  y( \lnot(C(x, y) \to A(x) ))$ is true.
when $\exists x \exists  y( C(x, y) \land \lnot A(x) )$ is true.
And this is true when for some x and y (let change them to a and b, dont use variables that are not bounded)
C(a, b)  is true A(a) is false
Now you only have to check if this combination is invalidated by the axioms.
