FOL, solve using resolution. Consider the following puzzle: On the island of

knights and knaves, knights always tell the truth, while knaves always lie. You are approached by

two people. The first one says: We are both knaves. What are they actually?

The puzzle is formalized to the knowledge base below:

$1.$ the inhabitants are either knights or knaves: Vx$|$inhabitant$($x$)$ knave$($x$)$ V knight $($x$)]$

$2.$ one cannot be a knight and a knave in the same time: Vx$[$knight $($x$)$ # $-$knavex$)]$

$3.$ a message m$($x$)$ said by a knight x is always true and a message m$($x$)$ said by a knave x is

always false: Vx $[$knight $($x$)$ m$($x$)]$ and Vx $[$knave$($x$)-$m$($x$)]$

$4.$ there are two inhabitants, lets say a and b: inhabitant$($a$)$ and inhabitant b$)$

$5.$ The message of inhabitant a is $\text{'}$We are both knaves': m$($a$)$ # $[$knave$($a$)$ V knave$($b$)]$

Can you prove by resolution knave$($a$)$ and knight $($b$)?$

Solution that does not use resolution gets no credit