# 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) ) )).
%------------------------------------------------------------------------------