Satisfiability P93741

Write a program to find all the solutions to a set of $m$ three–literal clauses $c_1, \dots, c_m$ in conjunctive normal form.

For instance, $\{a = \mbox{\em true}, b = \mbox{\em false}, c = \mbox{\em true}, d = \mbox{\em true}\}$ is a possible solution for the three clauses $$a \enspace \mbox{or} \enspace b \enspace \mbox{or} \enspace c, \quad \mbox{not} \enspace a \enspace \mbox{or} \enspace b \enspace \mbox{or} \enspace c, \quad b \enspace \mbox{or} \enspace \mbox{not} \enspace c \enspace \mbox{or} \enspace d.$$

As another example, $\{a = \mbox{\em true}, b = \mbox{\em false}\}$ is a possible solution for the clause $$b \enspace \mbox{or} \enspace \mbox{not} \enspace a \enspace \mbox{or} \enspace a.$$ Stricktly speaking, this clause does not have three literals (in fact it is equal to true, which has no literals at all), but in this exercise it is allowed to have repeated literals in the same clause.

Input

Input consists of a natural number $1 \le n \le 20$, followed by a natural number $m > 0$, followed by $c_1, \dots, c_m$. The names of the variables are the first $n$ lowercase letters, and all of them appear in the input at least once. A negative literal is indicated by a minus symbol in front of the variable.

Output

Print all the possible solutions of the set of clauses. The literals of each solution must appear in alphabetical order. If there is no solution, print a hyphen.

Information about the checker

You can print the solutions to this exercise in any order.