First Order Logic Inference. Proof of sentence. I need to find a proof for my goal, given some assumptions. The assumptions and the goal were translated from English sentences.
My Assumptions (Knowledge Base)

*

*John, Mary, Helen, George are the only members of Club1
$\mathtt{Member(Club1,John) ∧ Member(Club1,Mary) ∧ -Member(Club1,Helen) ∧ Member(Club1,George)}$



*John is Mary's husband
$\mathtt{Married(John,Mary)}$



*George is Helen's brother
$\mathtt{Siblings(Goerge,Helen)}$



*The husband or the wife of each person is also a part of the same club
$\mathtt{(∀x)(∀y)(∀s)(Married(x,y) \& Member(s,x) → Member(s,y))}$

My Goal (Φ)
Helen is not married
$\mathtt{(∀x)(¬(Married(x,Helen))}$

With common logic we can prove that Helen is not married. But the above assumptions can't prove my goal with propositional logic. I need to add my own assumptions, so that I can prove my goal.
What assumptions should I add to my Knowledge Base to prove φ ?
I tried the following ones , but they are not enough:
$\mathtt{(∀x)(∀y)(Siblings(x,y) \to -Married(x,y))}$
$\mathtt{(∀x)(∀y)(∀z)( Married(x,y) \to -Married(x,z) \& -Married(y,z))}$
The above assumptions tells that if two atoms are siblings then they can't be marry each other and if they can't marry more than one person.
I am using prover9 to prove my goal, but I can't find what else does it need to prove it.
Here is what I have done.

 A: You also need:
$\forall x (Member(Club1,x) \rightarrow (x = John \lor x = Mary \lor x = Helen \lor x = George))$
Since these four are the only members of the club, i.e. there are no others!
Also, let's make sure they are all different people:
$John \not = Mary$
$John \not = Helen$
$John \not = George$
$Mary \not= Helen$
$Mary \not = George$
$Helen \not = George$
Also, I think the puzzle assumes no gay marriage, so:
$\forall x \forall y ((Male(x) \land Married(x,y) \rightarrow Female(y))$
$\forall x \forall y ((Female(x) \land Married(x,y) \rightarrow Male(y))$
And so you'll also want to add:
$Male(John)$
$Female(Mary)$
$Female(Helen)$
$Male(George)$
$\forall x (Male(x) \leftrightarrow \neg Female(x))$
Finally, your last sentence where you try to say that someone cannot be married to more than one person isn't correct; it should be:
$\forall x \forall y \forall z (Married(x,y) \color{red}{ \land z \not = y}) \rightarrow \neg Married(x,z))$
and to use that, you'll probably also need:
$\forall x \forall y (Married(x,y) \rightarrow Married(y,x))$
A: Finally , the answer :

and the proof:

