I would like to use First Order Logic to express that two people are brothers when they are two different persons (two IDs of my database) who share both surnames, but not the first names. This is because occassionally I may have two records in my database with different ID but actually correspond to the same person. My clause looks like this, but I need to convert it to a definite clause in order to reason with it.
(everything here are variables, no constants)
BROTHERS(id1, id2) ==> SURNAME1(id1, x)
& SURNAME1(id2, x)
& SURNAME2(id1, y)
& SURNAME2(id2, y)
& ~(NAME(id1, z) & NAME(id2, z))
I have thought about splitting this implication in two but I cannot express "the names must be different when the IDs are different". Putting the negation inside and changing & by | may be the first step but still not a definite clause. Maybe I am missing something obvious...