# [CERC2016] Lost Logic

## 题面翻译

给定 $3$ 组随机布尔变量 $v_{i,1},...,v_{i,n}(1\leq i\leq 3)$，每组均为 $n$ 个。你需要构造关于布尔变量 $x_1,...,x_n$ 的若干组**条件**，使得满足全部条件的布尔变量赋值**有且仅有** $(v_{i,1},...,v_{i,n})(1\leq i\leq 3)$ 这 $3$ 组。

由于机器限制，你所构造每组条件的形式均应为：$A\rightarrow B$。这组条件的限制了：当 $A$ 为 $1$ 时 $B$ 一定为 $1$。其中，$A,B$ 可能形如：

- $x_i$：表示第 $i$ 个变量的值。
- $!x_i$：表示第 $i$ 个变量取反后的值。

例如，如果你构造了 $x_1\rightarrow x_2$，那么表示你规定 $x_1=1$ 时必有 $x_2=1$；如果你构造了 $!x_1\rightarrow x_2$，那么你规定了 $x_1=0$ 时必有 $x_2=1$。你需要找到一种使用不超过 $500$ 组条件来满足题意的方法，或者判定这样的条件组合不可能存在。如果有多组解，输出任意一组均可。

数据保证 $2\leq n\leq 50,v_{i,j}\in\{0,1\}(1\leq i\leq 3,1\leq j\leq n)$。

## 题目描述

Gustav is reading about *2-satisfiability*, a well known problem of assigning truth values to boolean
variables in order to satisfy a list of *constraints* — simple logical formulas involving two variables each.

We are using $n$ variables $x_1, x_2, \cdots , x_n$ that can take on values $0$ (false) and $1$ (true). A constraint is a
formula of the form $a\to b$ where both $a$ and $b$ are possibly negated variables. As usual, $\to$ denotes
logical implication: $a \to b$ is $0$ only when $a$ is $1$ and $b$ is $0$. The negation of variable $a$ is denoted by $!a$.

Given an assignment of values to variables, we say that the constraint is *satisfied* if it evaluates to $1$.
Gustav has constructed a list of constraints and correctly concluded that there are *exactly three* different
assignments of values to variables that satisfy all the constraints. Gustav has wrote down all three
assignments but has, unfortunately, lost the list of constraints.
Given three assignments of $n$ values to variables, find any list consisting of at most $500$ constrains such
that the three given assignments are the *only* assignments that satisfy all the constraints.

## 输入格式

The first line contains an integer $n (2 \leq n \leq 50)$ — the number of variables. Three lines follow, each
describing one assignment. The $k$-th line contains $n$ space-separated integers $v_1^k,v_2^k,\cdots,v_n^k$, where each $v_i^k$ is either $0$ or $1$ and denotes the value of the variable $x_i$ in the $k$-th assignment. All three assignments will be different.

## 输出格式

If there is no solution output a single line containing the integer $−1$.
Otherwise, the first line should contain an integer $m$ where $1 \leq m \leq 500$ — the number of constraints
in your solution. The $k$-th of the following $m$ lines should contain the $k$-th constraint. Each constraint
should be a string constructed according to the following rules:

- A *variable* is a string of the form “$\texttt{x}i$” where $i$ is an integer between $1$ and $n$ inclusive written
  without leading zeros.
- A *literal* is a string consisting of a variable possibly preceded by the “$\texttt{!}$” character.
- A *constraint* is a string of the form “$a\texttt{ -> }b$” where both $a$ and $b$ are literals. The implication sign
  consists of the “minus” character and the “greater-than” character and there is a single space
  character both before and after the implication sign.

## 样例 #1

### 样例输入 #1

```
3
0 0 0
0 1 0
1 0 0
```

### 样例输出 #1

```
3
x1 -> !x2
x3 -> x1
x3 -> x2
```

## 样例 #2

### 样例输入 #2

```
4
0 0 1 0
1 0 0 0
1 0 1 1
```

### 样例输出 #2

```
-1
```