A Theorem with Nice Axioms

Iokaste is a parent of Oedipus. Iokaste is a parent of Polyneikes. Oedipus is a parent of Polyneikes. Polyneikes is a parent of Thersandros. Oedipus is a patricide. Thersandros is not a patricide. Prove that Iokaste is a parent of a patricide that is a parent of somebody who is not a patricide. (PUZ128+1)

%------------------------------------------------------------------------------
%----Iokaste is a parent of Oedipus.
fof(iokaste_oedipus,axiom,(
    parent_of(iokaste,oedipus) )).

%----Iokaste is a parent of Polyneikes.
fof(iokaste_polyneikes,axiom,(
    parent_of(iokaste,polyneikes) )).

%----Oedipus is a parent of Polyneikes.
fof(oedipus_polyneikes,axiom,(
    parent_of(oedipus,polyneikes) )).

%----Polyneikes is a parent of Thersandros.
fof(polyneikes_thersandros,axiom,(
    parent_of(polyneikes,thersandros) )).

%----Oedipus is a patricide.
fof(oedipus_patricidal,axiom,(
    patricide(oedipus) )).

%----Thersandros is not a patricide.
fof(thersandros_not_patricidal,axiom,(
    ~ patricide(thersandros) )).

%----Prove that Iokaste is a parent of a patricide who is a parent of
%----somebody who is not a patricide.
fof(iokaste_parent_particide_parent_not_patricide,conjecture,(
    ? [P,NP] :
      ( parent_of(iokaste,P)
      & patricide(P)
      & parent_of(P,NP)
      & ~ patricide(NP) ) )).
%------------------------------------------------------------------------------