proving that a set of formulas is satisfiable I have to prove that the following set of formulas is satisfiable.


*

*$\neg \exists x\ p(x,x)$

*$\forall x\ \exists y\ (p(x,y)\land \neg \exists z\ (p(x,z)\land p(z,y)))$

*$\exists x\ \neg \exists y\ p(y,x)$

*$\exists x\ (\exists y\ p(y,x) \land \neg \exists y\ (p(y,x) \land \neg \exists z\ (p(x,z)\land p(z,y))))$


My approach is trying to draw a directed graph where the predicate p(x,y) is a directed from a node to some other node.
The problem I find is that the set of formulas is too complicated for me to draw a graph. 
My questions are:
Q1: How can I simplify the set of formulas, I feel like some of the formulas are needless(they are contained in other formulas of the set)
Q2: How would you advice me in dealing with such kind of problems, are there some general strategies? Are there any other ways of solving that kind of problems except trying to draw a directed graph?
Thanks in advance!
 A: Q1: Yes, simplifying is always good, but the only thing that makes things a little more clear to me was to replace the $\neg \exists y\ (p(y,x) \land \neg \exists z\ (p(x,z)\land p(z,y)))$ part in the fourth sentence with its equivalent $\forall y\ (p(y,x) \to \exists z\ (p(x,z)\land p(z,y)))$
Q2: There are some programs that try and find models. Truth trees (or tableaux methods) are one such example, but they can easily fall victim to combinatorial explosion, and if they only have finite sized models, most of these techniques fail completely.  Trying to draw a directed graph is a very good idea to at least get some insight into the problem.  In fact, that's exactly what I did to come up with the following model:

1: 'Nothing points to itself' -> True
2: 'Everything x points to something y, but there is no '2-step' to go from x to that y' -> True
3: There is something with no incoming arrow -> True (1)
4: There is something x that has an incoming arrow from y, and if there is an arrow from anything y to that something x, then there is a '2-step' going from x back to y -> True (for both 3 and 4)
A: The most popular method is Tableau method. 

The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics (Girle 2000).

You can find it more about that in this link.
