eolymp
bolt
Попробуйте наш новый интерфейс для отправки задач
Задачи

Выполнимость снова!

Выполнимость снова!

Лимит времени 1 секунда
Лимит использования памяти 128 MiB

Алиса недавно начала работать над аппаратной разработкой компании, ее работа состоит в определении дефектов в готовых интегральных схемах. Выявление этих дефектов сводится к решению задачи выполнимости. Помогите Алисе написать программу, которая решает эту задачу.

Входные данные

Первая строка содержит количество тестов, не большее 5. Первая строка каждого теста содержит два числа n (1n20) и m (1m100), где n - количество переменных, а m - количество правил. Каждая из следующих m строк задает одно правило. Каждое правило представляет собой дизъюнкцию литералов вида X[i] или ~X[i] для некоторого i (1in), где ~X[i] обозначает отрицание литерала X[i]. Оператор "or" обозначается символом v и отделяется от литералов одним пробелом.

Выходные данные

Для каждого теста вывести в отдельной строке satisfiable если формула выполняемая и unsatisfiable иначе.

Пример

Входные данные #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
Выходные данные #1
satisfiable
unsatisfiable
Источник 2014 ACM North America - Rocky Mountain, Problem J