# Problem C

Counting Clauses

It’s time for the annual 3-SAT competition, where the
contestants compete to answer as many instances of 3-SAT as
possible within the time limit. 3-SAT is a classic NP-complete
problem, where you are given a boolean formula in
*conjunctive normal form*, in which we have a set of
*clauses* each consisting of exactly three
*literals*. Each literal refer either positively or
negatively to a *variable*, which can be assigned a
value of either `True` or `False`. The question is whether there exists an
assignment to the variables such that every clause evaluates to
`True`. No clause will contain
duplicates of a literal (however it is possible that a clause
contain both $\neg x_ i$
and $x_ i$). An example of
a 3-SAT instance is shown below (from sample input
1):

## Input

The input is a single instance of the 3-SAT problem. The
first line is two space-separated integers: $m$ ($1
\leq m \leq 20$), the number of clauses and $n$ ($3
\leq n \leq 20$), the number of variables. Then
$m$ clauses follow, one
clause per line. Each clause consists of 3 distinct
space-separated integers in the range $[-n, n] \setminus \{ 0\} $. For each
clause, the three values correspond to the three literals in
the clause. If the literal is negative, that means that the
clause is satisfied if the corresponding variable is set to
`False`, and if it is positive the
clause is satisfied if the variable is set to `True`.

## Output

Print “`satisfactory`” on a single
line if Øyvind finds the 3-SAT instance to be satisfactory, and
“`unsatisfactory`” otherwise.

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

5 3 -1 2 3 -1 -2 3 1 -2 3 1 -2 -3 1 2 -3 |
unsatisfactory |

Sample Input 2 | Sample Output 2 |
---|---|

8 3 1 2 3 1 2 -3 1 -2 3 1 -2 -3 -1 2 3 -1 2 -3 -1 -2 3 -1 -2 -3 |
satisfactory |