Is this tautology I have this example:
$\lnot \exists y P(y) \to ( \forall y (\exists x P(x) \to P(y)))$
I am doing it step by step: A: $\lnot \exists y P(y) \to ( \forall y (\exists x P(x) \to P(y)))$
B($\lnot$A) :$\lnot [\lnot \exists y P(y) \to ( \forall y (\exists x P(x) \to P(y)))]$
1: $\lnot \exists y P(y) \land \lnot ( \forall y (\exists x P(x) \to P(y)))$
2: $\forall \lnot y P(y) \land \exists y ( \lnot (\exists x P(x) \to P(y)))$
3: $\forall \lnot y P(y) \land \exists y ((\exists x P(x) \land \lnot  P(y)))$
4: $\forall \lnot y P(y) \land \exists y \exists x (( P(x) \land \lnot  P(y)))$
5: $\exists y \exists x [\forall \lnot z P(z) \land (( P(x) \land \lnot  P(y)))]$
6:  $\exists y \exists x \forall z[\lnot P(z) \land  P(x) \land \lnot  P(y)]$ 
7 SKOL(B):  $\forall z[\lnot P(z) \land  P(a) \land \lnot  P(b)]$
8: $C: =\lnot P(z) \land  P(a) \land \lnot  P(b)$
$\sum (C)=\{ \{ \lnot P(z)\} ,\{ P(a) \} , \{ \lnot  P(b) \} \}$
$gr(\sum (C))=\{ \{ \lnot P(b)\} ,\{ P(a) \} , \{ \lnot  P(b) \}... \}$
But i can't make empty clauseso its not tautology i guess. 
$\{ \lnot P(b)\} ,\{ P(b) \} = $ empty clause (that's example)
In my case i cant make empty clause so i guess its not tautology, am i right?
Try to solve this formule on your own. 
Thank you for answers.
A: It's a weird formula: if no element satisfies $P$ (so the left hand side holds), then for all $y$ the implication $(\exists x P(x)) \to P(y)$ is true. (An implication with a false left hand side is always true). So I'd think  this is a tautology. You cannot make it false in some model.
