Background
There are two people, Bill and John. One of them is a knight, which always tells the truth, and the other is a knave, which always tells a lie. You don't know who is the knight and who is the knave. Each person then says several statements about who is the knave and who is the knight. Using this information, you must come to a conclusion as to who is the knight and who is the knave.
The Knights and Knaves logic problem is based on Booleen algebra. The words that a person says form a Booleen satisfiability problem. The knave's statements must always be false and the other knight's statements must always be true.
John says "Both I am a knave and Bill is a knave". If John were the knight, then this statement would be false, so he can't be the knight. If he were the knave and Bill were the knight, this statement would still be false, even thought the first part is true. So, John is the knave.
The Challenge
Your challenge is to write the shortest program possible that will take a list of statements made by each person and will figure out who is the knave and who is the knight. There are a lot of details to cover, so this problem is described in three sections.
Input
Input will be two lines followed by a newline. Each line will give the name of one of the characters, followed by a colon, followed by several sentences said by that person. If one person is the knight, then all of his sentences will be true, and all of the knave's sentences will be false. The first letter of a sentence will always be capitalized, and every sentence will end with a period. Here is an example:
Joe: Both I am a knight and neither Steve is a knave nor I am a knave.
Steve: Joe is a knave. Either Joe is a knight or I am a knight.
Parsing
Each sentence consists of at least one clause. Each clause contains one of several things (hopefully you can understand my notation):
both [clause] and [clause]
either [clause] or [clause]
neither [clause] nor [clause]
[I am | (other person's name) is] a [knight | knave]
This is unambigious becuase it can be understood in a way similar to Polish notation. Here is an example of a sentence:
Both I am a knight and neither Steve is a knave nor I am a knave.
The translation into Booleen algebra is straightforward. The "both" statements are ANDs, the "either" statements are XORs, and the "neither" statements are NORs.
(I am a knight) AND ((Steve is a knave) NOR (I am a knave))
Output
Output will consist of two lines. Each line consists of a person's name (in order) and then says whether he is the knight or the knave. There will always be one knight and one knave. Here is the output for the above example:
Joe is the knave.
Steve is the knight.
If the problem is unsolvable (either you can't tell who is what, or there is no solution), then your program can do anything EXCEPT produce a valid output.
More examples
Input
Sir Lancelot: Either both I am a knight and Merlin is a knave or both I am a knave and Merlin is a knight.
Merlin: Either both I am a knight and Sir Lancelot is a knight or both I am a knave and Sir Lancelot is a knave.
Output
Sir Lancelot is the knight.
Merlin is the knave.
Input
David: Neither I am a knave nor Patrick is a knight. Either I am a knight or Patrick is a knave.
Patrick: Either I am a knight or both I am a knight and David is a knight.
Output
David is the knave.
Patrick is the knight.
Input
Lizard: I am a knight.
Spock: I am a knave.
One possible output
Rock Paper Scissors
Rules, Regulations and Notes
- Standard code golf rules apply
- Your program must be only made up of printable ASCII
- All input and output will be from STDIN and STDOUT