First order logic formalization problem

Question

I have to formalize the following problem for the SPASS theorem prover (first order logic): "On an island there are exactly two type of people: knights, who always say the truth, and knaves, who always lie. On this island there are three people: A, B, C. A says that A, B, C are knaves. B says that there is exactly one knight among them. What can we say about A, B, C?"

Now, my question isn't regarding SPASS syntax or functioning, so the only thing we have to keep it in mind for, it's that, in order to make it prove some conjectures, we need to have a set of formulae which are axioms and a set of formulae which are conjectures (that are the ones it will need to prove).

SOLUTION

Given the unary predicates $C(x)$="being a knight" and $F(x)$="being a knave", and the constants $A$, $B$, $C$ (which are functions with arity $0$)

AXIOMS

(1) $C(x) \implies \neg F(x)$ ("a person is either a knight or a knave")

Now, from the statement "A says that A, B, C are knaves" we get two possibilities: either A is a knight and A, B, C are knaves or B is a knave and it's not true that A, B, C are knaves.

(2) $C(A) \implies (F(A) \land F(B) \land F(C))$

(3) $F(A) \implies \neg (F(A) \land F(B) \land F(C))$

From the statement "B says that there is exactly one knight among them" we get two possibilities: either A is a knight and one between them is a knight, or B is a knave and it's not true that one between them is a knight.

(4) $C(B) \implies ((C(A) \land F(B) \land F(C)) \lor (F(A) \land C(B) \land F(C)) \lor (F(A) \land F(B) \land C(C)))$

(5) $F(B) \implies \neg ((C(A) \land F(B) \land F(C)) \lor (F(A) \land C(B) \land F(C)) \lor (F(A) \land F(B) \land C(C)))$

CONJECTURES

(6) $F(A) \land C(B) \land F(C)$ (in the solutions there is a comment near this conjecture that says "example")

QUESTIONS

1. My solution for the axioms was nearly the same, but I created three axioms: $(1)$, "$(2) \lor (3)$", "$(4) \lor (5)$". My reasoning was that since (2) and (3) where two possibilites deriving from the same statement, it was right to put them in a single statement with a "or". Is it wrong? What happens if I do this?

2. Since the question is "what can we say about A, B, C", why is there a single statement as a conjecture, which is one possibility for $A, B, C$? SPASS should only be able to say if it's true or false, so shouldn't we theoretically include every possibility for $(A, B, C)$ in the conjectures and see which one is right? My guess is that that's true but it's too long so we logically derived the solution to the "puzzle" and proposed that as a conjecture.

• Note: this might be related to SPASS since I don't know if writing all the possible conjectures behaves in my (hypothetical) manner, so that it proves only the right one