잃어버린 논리

구스타프는 2-충족 가능성 문제(2-SAT)에 관한 글을 읽고 있다. 2-SAT은 불리언 변수에 참과 거짓 값을 배정해 제약 조건 목록을 모두 만족시키는 잘 알려진 문제이고, 각 제약 조건은 변수 두 개가 들어가는 간단한 논리식이다.

변수는 $x_1, x_2, \ldots, x_n$의 $n$개이며, 각 변수는 0(거짓) 또는 1(참) 값을 가진다. 제약 조건은 $a \to b$ 꼴의 식이고, $a$와 $b$는 각각 변수 또는 부정된 변수이다. 여기서 $\to$는 논리적 함의이다. 즉 $a \to b$는 $a$가 1이고 $b$가 0일 때만 0이다. 변수 $a$의 부정은 $!a$로 쓴다.

변수에 값을 배정했을 때 제약 조건의 값이 1이면 그 제약 조건이 만족된다고 한다. 구스타프는 제약 조건 목록을 만들었고, 모든 제약 조건을 만족하는 배정이 정확히 세 가지라는 사실을 올바르게 알아냈다. 그는 세 배정을 모두 적어 두었지만 안타깝게도 제약 조건 목록을 잃어버렸다.

변수 $n$개에 대한 배정 세 개가 주어진다. 주어진 세 배정만이 모든 제약 조건을 만족하는 배정이 되도록 하는, 제약 조건 500개 이하로 이루어진 목록을 구하라. 이런 목록은 여러 개일 수 있으므로 출력 절에 적힌 규칙으로 정해지는 목록 하나를 출력해야 한다.

첫째 줄에 변수의 개수 $n$ ($2 \le n \le 50$)이 주어진다. 다음 세 줄에 배정이 한 줄에 하나씩 주어진다. $k$번째 줄에는 정수 $n$개 $v_{1k}, v_{2k}, \ldots, v_{nk}$가 공백으로 구분되어 주어진다. 각 $v_{ik}$는 0 또는 1이며, $k$번째 배정에서 변수 $x_i$의 값이다. 세 배정은 모두 서로 다르다.

조건을 만족하는 목록이 없으면 정수 -1 하나만 한 줄에 출력한다.

그렇지 않으면 첫째 줄에 제약 조건의 개수 $m$ ($1 \le m \le 500$)을 출력하고, 다음 $m$개 줄 중 $k$번째 줄에 $k$번째 제약 조건을 출력한다. 각 제약 조건은 다음 규칙으로 만든 문자열이다.

• 변수는 "xi" 꼴의 문자열이다. $i$는 1 이상 $n$ 이하의 정수이며 앞에 0을 붙이지 않는다.
• 리터럴은 변수 하나, 또는 변수 앞에 "!" 문자를 붙인 문자열이다.
• 제약 조건은 "a -> b" 꼴의 문자열이고, a와 b는 리터럴이다. 함의 기호는 빼기 문자와 ">" 문자로 이루어지며, 함의 기호 앞과 뒤에 공백이 정확히 하나씩 있다.

목록이 존재하면 다음 규칙으로 만든 목록을 그대로 출력해야 한다. 아래 식에서 $i$, $j$, $r$, $p$, $q$ 자리에는 실제 변수 번호를 쓴다.

1. 세 배정에서 값이 모두 같은 변수를 상수 변수라고 한다. 상수 변수 $x_i$를 $i$가 작은 것부터 보면서, 값이 0이면 xi -> !xi를, 값이 1이면 !xi -> xi를 출력한다.
2. 상수 변수가 아닌 변수에서는 세 배정 중 정확히 하나가 나머지 둘과 값이 다르다. 그 배정의 번호(1, 2, 3)가 같은 변수끼리 한 그룹으로 묶고, 각 그룹에서 번호가 가장 작은 변수를 그 그룹의 대표라고 한다. 대표가 아닌 비상수 변수 $x_j$를 $j$가 작은 것부터 보면서, 같은 그룹의 대표를 $x_r$이라 하자. 세 배정 모두에서 $x_j$와 $x_r$의 값이 같으면 xr -> xj와 xj -> xr을, 세 배정 모두에서 값이 다르면 xr -> !xj와 !xj -> xr을 이 순서대로 출력한다.
3. 마지막으로 서로 다른 두 대표 $x_p$, $x_q$ ($p < q$)의 쌍을 $p$가 작은 순서로, $p$가 같으면 $q$가 작은 순서로 본다. 각 쌍에서 세 배정에 나타나지 않는 값의 조합 $x_p = u$, $x_q = w$를 금지하는 제약 조건 A -> B를 하나 출력한다. 여기서 A는 $u = 1$이면 xp, $u = 0$이면 !xp이고, B는 $w = 1$이면 !xq, $w = 0$이면 xq이다.