또 다시 충족 가능성

앨리스는 얼마 전 하드웨어 설계 회사에 들어갔다. 맡은 일 가운데 하나는 제작된 집적 회로에서 결함을 찾아내는 것인데, 이 검사는 결국 논리식 하나가 충족 가능한지 판정하는 문제로 귀결된다.

논리식은 곱항 정규형(CNF)으로 주어진다. 변수는 $X_1$부터 $X_n$까지다. 리터럴은 변수 $X_i$ 또는 그 부정 $\sim X_i$다. 절은 리터럴을 논리합으로 이은 것이고, 논리식은 $m$개의 절을 모두 논리곱으로 이은 것이다.

각 변수에 참이나 거짓을 배정해서 모든 절을 동시에 참으로 만드는 방법이 있는지 판정하는 프로그램을 작성하라.

첫째 줄에 테스트 케이스의 개수 $T$가 주어진다. $T$는 5보다 크지 않다.

각 테스트 케이스의 첫째 줄에 변수의 개수 $n$과 절의 개수 $m$이 주어진다($1 \le n \le 20$, $1 \le m \le 100$). 이어지는 $m$개의 줄에 절이 한 줄에 하나씩 주어진다.

각 절은 리터럴을 논리합으로 이은 형태다. 리터럴은 $X_i$ 또는 $\sim X_i$이고 $1 \le i \le n$이다. 논리합은 문자 v로 적으며, 양옆의 리터럴과 공백 한 칸으로 구분한다. 한 절에 같은 변수가 여러 번 나올 수 있고, 한 변수의 두 극성이 함께 나올 수도 있다.

각 테스트 케이스마다 모든 절을 참으로 만드는 배정이 있으면 satisfiable을, 없으면 unsatisfiable을 한 줄에 출력한다.