##### Woburn Challenge 2001 - Suicidal

So that was enough craziness. Three whole days of no studying was just
too much and so orientation week was cut back to only days (or was
it?). Today is the first day of class – discrete math. The students are
divided into groups of about and are each given a -CNF formula (ie.
a formula in conjunctive normal form with variables per clause – e.g.,
`(a OR b) AND (c OR a) AND (x OR NOT y)`

) for which they have to find a
solution. Being engineers not in the math stream, they set out to solve
the formula using the only method they know: brute force (ie. trying all
possible combinations for all the variables). There are however twists
on this sinister day.

- Word has leaked out that this so-called "class" is really another test of their orientation week and that there is a mole within their group who is sabotaging their efforts to find a solution to the formula.
- They have discovered that not all CNF formulas are satisfiable.

Therefore the following question arises: are they unable to find a solution because a) they are stupid, b) the mole is sabotaging their efforts or c) the formula is unsatisfiable.

Furthermore, being Waterloo keeners, they want to solve this problem in time or less, where is the number of clauses in the formula and is the base logarithm.

#### Input Specification

Several -CNF formulas: variables will be characters, `&`

is `AND`

, `|`

is `OR`

and `!`

is `NOT`

; blank line denotes end of input. There will be spaces
between `|`

and `&`

and brackets around each clause. There will be at most
variables per formula.

#### Output Specification

If a formula is satisfiable, print out `satisfiable`

.

Otherwise, output `unsatisfiable`

.

#### Sample Input

```
(a | b) & (a | c)
(a | a) & (!a | !a)
```

#### Sample Output

```
satisfiable
unsatisfiable
```

## Comments