Yet Satisfiability Again

Alice recently started working at a hardware design company. One of her jobs is finding defects in fabricated integrated circuits, and that check reduces to deciding whether a single logical formula is satisfiable.

The formula is given in conjunctive normal form. The variables are $X_1$ through $X_n$. A literal is a variable $X_i$ or its negation $\sim X_i$. A clause is a disjunction of literals, and the formula is the conjunction of all $m$ clauses.

Write a program that decides whether true and false can be assigned to the variables so that every clause is true at the same time.

The first line contains the number of test cases $T$. $T$ is not more than 5.

The first line of each test case contains the number of variables $n$ and the number of clauses $m$ ($1 \le n \le 20$, $1 \le m \le 100$). Then $m$ lines follow, one clause per line.

Each clause is a disjunction of literals. A literal is $X_i$ or $\sim X_i$ with $1 \le i \le n$. The disjunction operator is written as the character v and is separated from the literal on either side by a single space. The same variable may appear more than once in one clause, and both polarities of one variable may appear together.

For each test case, print satisfiable on its own line if some assignment makes every clause true, and unsatisfiable otherwise.