I have three formulas $$ \sigma_1=\exists y \forall z (\exists x \neg p(z,g(x)) \implies q(g(y),z)) \\ \sigma_2=\forall y \forall z (\exists x q(y,f(x)) \implies p(z,y)) \& \forall x \forall y(p(x,y) \implies r(y)) \\ \sigma_3=\exists x \exists y \exists z (p(f(x),z)\&r(g(y))) $$
Here p,q,r are predicate symbols, and f, g are functional symbols.
I now that $\{ \sigma_1, \sigma_2, \neg \sigma_3 \}$ is not satisfiable, so I negate the third formula and I get $$ \sigma_3=\forall x \forall y \forall z (\neg p(f(x),z)\lor \neg r(g(y))) $$
For $\sigma_1$ and $\sigma_2$ I get
$$ \sigma_1 \equiv \exists y \forall z (\forall x p(z,g(x)) \lor q(g(y),z)) \equiv \exists y \forall z \forall x(p(z,g(x)) \lor q(g(y),z)) \equiv \forall z \forall x(p(z,g(x)) \lor q(g(c),z)) $$
In the last formula I have skolemized the $\exists y$ quantifier with a constant.
$$ \sigma_2 \equiv \forall y \forall z (\exists x q(y,f(x)) \implies p(z,y)) \& \forall x \forall y(p(x,y) \implies r(y)) \equiv \forall y \forall z (\forall x \neg q(y,f(x)) \lor p(z,y)) \& \forall x \forall y(\neg p(x,y) \lor r(y)) \equiv \forall y \forall z \forall x \forall z \forall t (\neg q(y,f(x)) \lor p(z,y)) \& (\neg p(z,t) \lor r(t)) \\ $$
I was able to get the following sets of literals (assuming my method was correct) $$ 1. \{p(z,g(x)), q), g(c), z)\} \\ 2. \{\neg q(y,f(x)), p(z,y)\} \\ 3. \{\neg p(z,t), r(t)\} \\ 4. \{\neg p(f(x),z), \neg r(g(y))\} $$
From there I've started using the resolution method trying to find the empty disjunct $\blacksquare $ but I got stuck and can't get to $\blacksquare$.
Edit:
After writing down the clauses until I got stuck as suggested I got the following solution, assuming it's correct
- Using 1 with [z/x] substitution and 3 with [t/g(x)] substitution I got $\{q(g(c),z),r(g(x))\}$
- From 2. and 4. I got $\{\neg q(y,f(x)),\neg r(g(y))\}$
- from 2 and 3[t/y] I got $\{\neg q(y,f(x)), r(y)\}$
- From 1 and 4 I got $\{q(g(c), f(x)), \neg r(g(y))\}$
- From 5[z/f(x)] and 8[y/x] - $\{q(g(c),f(x))\}$
- From 7[y/g(c)] and 9 - $\{r(g(c))\}$
- From 8 and 9 - $\{\neg r(g(y))\}$
- From 11[y/c] and 7 - $\blacksquare$
Thanks in advance!
HINT
First, it really helps to make sure you have unique variable names, because otherwise you run the risk of two completely different variables ending up with the same variable name, thus possibly preventing possible resolutions to go through. So, I would change your clauses to:
$$ \{p(x_1,g(x_2)), q(g(c), x_1)\}, \{\neg q(x_3,f(x_4)), p(x_5,x_3)\}, \{\neg p(x_6,x_7), r(x_7)\}, \{\neg p(f(x_8),x_9), \neg r(g(x_{10}))\} $$
Second, when you resolve the first two clauses on the $q$ and $\neg q$ terms, use variable substitutions so that the two $p$ terms become exactly alike, so that instead of 2, you end up with just 1 term. So, to resolve $\{p(x_1,g(x_2)), q(g(c), x_1)\}$ and $\{\neg q(x_3,f(x_4)), p(x_5,x_3)\}$, use the substitutions $g(c)/x_3, f(x_4)/x_1, f(x_4)/x_5, c/x_2$, so the resolvent clause is just $\{ p(f(x_4),g(c) \}$.
Likewise, using substitutions $g(x_{10})/x_7, g(x_{10})/x_9, f(x_8)/x_6$, the third and fourth clause resolve to just $\{ \neg p(f(x_8),g(x_{10})) \}$
And now you can resolve the two clauses you just got to the empty clause by using $x_4/x_8, c/x_{10}$