SAT solvers find satisfying assignments to Boolean formulas. The formulas are given in the conjunctive normal form:

• the formula is a conjunction of m clauses: c_1 \land c_2 \land \ldots
• each clause c_j is a disjunction of literals: \ell_1 \lor \ell_2 \lor \ldots
• each literal \ell_k is either a Boolean variable x_i or is negation \lnot x_i.

Here \land is the "AND" operation, \lor is the "OR" operation, and \lnot is the "NOT" operation. We will always assume that the variables are called x_1, x_2, \ldots, x_n.

For example, here is a Boolean formula in the conjunctive normal form; we have m = 3 clauses and n = 3 variables: (x_1 \lor x_2 \lor x_3) \land (\lnot x_1 \lor \lnot x_2 \lor \lnot x_3) \land (\lnot x_1 \lor x_2 \lor x_3). This formula is satisfiable; we can find the following variable assignment that makes the formula true: x_1 = \mathrm{false},\ x_2 = \mathrm{true},\ x_3 = \mathrm{true}. Such formulas are commonly represented in the standard DIMACS format: the first line contains the magic words "p" ("problem") and "cnf" ("conjunctive normal form"), and then it is followed by the number of variables n and the number of clauses m. This is followed by m lines, each describing one clause. The line contains just one number per literal: a positive literal x_i is written as i, and a negated literal \lnot x_i is written as -i. The clause is terminated with a 0.

For example, the above formula would be written as follows in the DIMACS format:

p cnf 3 3
1 2 3 0
-1 -2 -3 0
-1 2 3 0

Now we could take a commonly used SAT solver, for example "picosat", and ask it to solve this. We will get e.g. the following output:

s SATISFIABLE
v -1 2 3 0

Here the first line of output that starts with an "s" indicates that this formula was indeed satisfiable, and the second line of output that starts with a "v" gives the variable assingment. For each i = 1, \dotsc, n, we write i if x_i is true and -i if x_i is false. Again, the list is terminated with a 0.

Your task here is to write a SAT solver that solves formulas in certain special cases.

Input

The input is a Boolean formula in the conjunctive normal form, given in the DIMACS format.

Each clause will contain exactly 2 literals. (It is possible that the same variable occurs twice in one clause.)

Output

Output a satisfying assignment in a format similar to the one used in the "picosat" example above.

If a solution exists, there should be two lines of output: first one that says "s SATISFIABLE", and then one that starts with "v", then contains n values that indicate the satisfying assignment, and finally a "0".

If there is no solution, you should print out just one line that says "s UNSATISFIABLE".

Limits

• Number of variables: 3 \le n \le 5\cdot10^5
• Number of clause: 3 \le n \le 5\cdot10^5

Example 1

Input:

p cnf 4 5
2 -1 0
-1 -2 0
1 3 0
-2 -3 0
1 4 0

Output:

s SATISFIABLE
v -1 -2 3 4 0

Example 2

Input:

p cnf 3 4
1 2 0
1 -2 0
-1 3 0
-1 -3 0

Output:

s UNSATISFIABLE