& gpRule1 ^x ^y ^z (parent x y (parent y z (grandparent x z)) = [*]). & gpAxiom1 (parent Allan Brenda = [*]). & gpAxiom2 (parent Brenda Charles = [*]). & conclusion _. & X _. & Y _. & Z _. $(gpAxiom1 (gpAxiom2 conclusion) ; gpRule1 X Y Z).