Yet Satisfiability Again

Time limit1sMemory limit256 MB

Summary

Decide whether a CNF formula over at most 20 variables and 100 clauses has an assignment that satisfies every clause.

Level: Easy3 of 10
Topics: Brute force, Bit manipulation
Solved: No attempts yet

Problem

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.

Input

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.

Output

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

Examples2

Example 1

Input

2
3 3
X1 v X2
~X1
~X2 v X3
3 5
X1 v X2 v X3
X1 v ~X2
X2 v ~X3
X3 v ~X1
~X1 v ~X2 v ~X3

Expected output

satisfiable
unsatisfiable

Example 2

Input

3
1 1
X1
1 2
X1
~X1
2 1
X1 v ~X1

Expected output

satisfiable
unsatisfiable
satisfiable