Code golf: Solve a Knights and Knaves logic problem by parsing English 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
Python, 491 chars

Works by converting each line to a Python expression, and eveluating it.
The knave and knight are evaluated as 0 and 1. For the two people, we try both options.
For example, Joe: Steve is a knave becomes Joe==(Steve==knave). This way, if Joe is a knave, the result is true only if he's lying.
You get ugly errors when it's impossible or undecided. If impossible, r[0] is an index error, because r is empty. If undecidable, concatenating r[1:] to a list of strings causes trouble.

import sys
def p():
    a=s.pop(0)
    try:return{"both":"(%s*%s)","either":"(%s|%s)","neither":"(1-(%s|%s))"}[a.lower()]%(p(),p())
    except KeyError:r=s[2];del s[:4];return"(%s==%s)"%((a,m)[a=="I"],r)
x=[];w=[]
for l in sys.stdin:
    m,l=l.split(":");w+=[m]
    for s in l.split("."):
        s=s.split()
        while s:x+=["%s==%s"%(m,p())]
k=("knave","knight")
r=[a for a in[{w[0]:z,w[1]:1-z}for z in(0,1)]if all(eval(l,{k[0]:0,k[1]:1},a)for l in x)]
print"\n".join(x+" is the "+k[r[0][x]]+"."for x in w+r[1:])