年度 3-SAT 竞赛又开始了，参赛者们需要在规定时间内尽可能多地解答 3-SAT 问题实例。3-SAT 是一个经典的 NP 完全问题，给定一个合取范式（conjunctive normal form）的布尔公式，其中包含一组子句，每个子句恰好由三个文字（literal）组成。每个文字要么正向引用一个变量，要么负向引用一个变量，变量可以被赋值为 True 或 False。问题在于是否存在一种变量赋值，使得每个子句的计算结果都为 True。任何子句都不会包含重复的文字（但一个子句可能同时包含 $\neg x_i$ 和 $x_i$）。3-SAT 实例的一个示例如下（来自样例输入 1）：

$(\neg x_1 \vee x_2 \vee x_3) \wedge (\neg x_1 \vee \neg x_2 \vee x_3) \wedge (x_1 \vee \neg x_2 \vee x_3) \wedge (x_1 \vee \neg x_2 \vee \neg x_3) \wedge (x_1 \vee x_2 \vee \neg x_3)$

术语说明

Øyvind 是竞赛的裁判，负责在比赛开始前验证其他裁判设计的题目实例的质量。Øyvind 讨厌少于 8 个子句的 3-SAT 实例，因为它们总是可满足的，无法给参赛者带来真正的挑战。因此，他会将此类问题实例视为“不令人满意”（unsatisfactory）。每当 Øyvind 遇到包含 8 个或更多子句的实例时，他知道判断该实例是否可满足是一个真正的挑战，因此他会将这些问题实例判定为“令人满意”（satisfactory）。给定一个 3-SAT 实例，你能帮助得出 Øyvind 的判断吗？

输入格式

输入为单个 3-SAT 问题实例。第一行包含两个空格分隔的整数：$m$ ($1 \le m \le 20$)，表示子句的数量；$n$ ($3 \le n \le 20$)，表示变量的数量。接下来有 $m$ 行，每行一个子句。每个子句由 3 个不同的空格分隔的整数组成，范围在 $[-n, n] \setminus \{0\}$ 之间。对于每个子句，这三个值对应于子句中的三个文字。如果文字为负，则表示如果对应的变量被设为 False，则该子句满足；如果文字为正，则表示如果对应的变量被设为 True，则该子句满足。

输出格式

如果 Øyvind 认为该 3-SAT 实例是“令人满意”的，则在一行中输出 “satisfactory”，否则输出 “unsatisfactory”。

样例

输入格式 1

5 3
-1 2 3
-1 -2 3
1 -2 3
1 -2 -3
1 2 -3

输出格式 1

unsatisfactory

输入格式 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

输出格式 2

satisfactory