# Yet Satisfiability Again!

## Input

The first line of input contains a single integer, not more
than $5$, indicating the
number of test cases to follow. The first line of each test
case contains two integers $n$ and $m$ where $1 \le n \le 20$ indicates the number
of variables and $1 \le m \le
100$ indicates the number of clauses. Then, $m$ lines follow corresponding to each
clause. Each clause is a disjunction of literals in the form
`X`$i$ or
`~X`$i$ for some
$1 \le i \le n$, where
`~X`$i$ indicates
the negation of the literal `X`$i$. The βorβ operator is denoted by a
β`v`β character and is seperated from
literals with a single space.

## Output

For each test case, display `satisfiable` on a single line if there is a
satisfiable assignment; otherwise display `unsatisfiable`.

Sample Input 1 | Sample Output 1 |
---|---|

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 |
satisfiable unsatisfiable |