On the island of knights and knaves, a judge presides over the trial of two inhabitants, X and Y, accused of a crime. At the opening of the proceedings, it is not known whether X and Y are both innocent, both guilty, or one innocent and the other guilty. Eight islanders, J, K, L, M, N, O, P, and Q, are heard as witnesses. They make the following statements: J says, I am a knight. K remains silent. L says, J is a knave. M says, K is a knave. N says, L and M are both knights. O says, J and K are not both knaves. P says, N and O are either both knights or both knaves. Q says, P and I are either both knights or both knaves, and V and W are not both guilty.

Write a Python script using the z3 library. Your script should determine which, if any, of X and Y are guilty. Introduce variables j, k, . . . , and q to denote the truthfulness of J, K, . . . , and Q, respectively. Use variables x and y to denote the guilt of x and y, respectively. keep in mind that you are only asked whether X and Y are guilty. You have a unique solution to the puzzle if the values of x and y are implied by the given constraints, even though the truth of some witness statements remains uncertain.