스티븐 쿡

스티븐 아서 쿡은 계산 복잡도를 연구하는 컴퓨터 과학자이자 수학자다. 논문 "The complexity of theorem-proving procedures"에서 P 대 NP 문제를 정확하게 서술했고, 불 만족 가능성 문제인 SAT가 NP-난해임을 증명했다. 1982년에는 튜링상을 받았다.

쿡과 레빈이 불 논리식 하나를 놓고 게임을 한다. 논리식에 나오는 변수는 처음에 모두 값이 정해지지 않은 상태다. 두 사람이 번갈아 한 번씩 두며, 쿡이 먼저 둔다. 자기 차례에는 아직 값이 정해지지 않은 변수 하나를 골라 참이나 거짓으로 고정한다. 모든 변수의 값이 정해졌을 때 논리식이 참이면 쿡이 이기고, 거짓이면 레빈이 이긴다.

두 사람 모두 최선을 다해 둔다. 누가 이기는지 판정하라.

첫째 줄에 테스트 케이스의 개수 $T$ ($1 \le T \le 20$)가 주어진다. 각 테스트 케이스는 두 줄로 이루어진다.

테스트 케이스의 첫째 줄에는 논리식에 들어 있는 변수의 개수 $n$ ($1 \le n \le 10$)이 주어진다. $i$번째 변수는 영어 알파벳 대문자의 $i$번째 글자로 쓴다. 즉 첫 번째 변수는 A이고 세 번째 변수는 C이다.

둘째 줄에는 길이가 256자 이하인 불 논리식이 주어진다. 불 논리식은 다음 다섯 가지 형태 중 하나다.

• var: var는 변수다.
• ( formula1 ): formula1은 불 논리식이다.
• not formula1: formula1은 불 논리식이다.
• formula1 or formula2: formula1과 formula2는 모두 불 논리식이다.
• formula1 and formula2: formula1과 formula2는 모두 불 논리식이다.

변수와 연산자 사이에는 공백이 있다. 연산자는 and, or, not과 괄호 () 네 가지이고, 앞의 세 가지는 소문자로 쓴다. 우선순위는 높은 쪽부터 (), not, and, or 순이다.

각 테스트 케이스마다 이긴 사람의 이름을 한 줄에 출력한다. Cook 또는 Levin이다.