Horn Clauses

Consider a set of boolean variables and a boolean formula over them. An assignment of values to the variables is called satisfying if the formula evaluates to true after every variable is replaced by its assigned value. A formula is called unsatisfiable if no satisfying assignment exists.

In general no polynomial-time algorithm is known that decides the satisfiability of an arbitrary boolean formula, although it has not been proven that none exists. The same is true for deciding whether a formula is unsatisfiable. Nevertheless, for certain restricted classes of formulae these questions can be answered in polynomial time. This problem is about one such class.

A literal is either a variable $x$ by itself (a positive literal) or its negation $\neg x$ (a negative literal). A clause is a disjunction (OR) of one or more literals. A Horn clause is a clause containing at most one positive literal.

Any Horn clause $\neg n_1 \lor \neg n_2 \lor \ldots \lor \neg n_k \lor p$ can be rewritten as an implication: $(n_1 \land n_2 \land \ldots \land n_k) \Rightarrow p$. The left-hand side is the antecedent and the right-hand side is the succedent. When the succedent is empty, treat it as the constant false; when the antecedent is empty, treat it as the constant true.

A formula here is a conjunction (AND) of one or more Horn clauses. For such formulae satisfiability can be decided in polynomial time. Write a program that does so.

The input consists of one or more formulae, each on its own line, written according to the grammar below. In the grammar, [ X ] means that X may be omitted, and { X } means that X may occur zero or more times. Characters in quotes stand for themselves.

       <char> → 'A' | 'B' | ... | 'Z'
   <variable> → <char> {<char>}
<horn-clause> → '(' [<variable> {'&'<variable>}] '=>'<variable>')'
              | '(' <variable> {'&'<variable>} '=>' [<variable>] ')'
    <formula> → <horn-clause> {'&'<horn-clause>}

Each variable name is a non-empty string of uppercase letters A–Z. Every formula occupies one line. The total length of the input does not exceed $20,000$ characters.

For each formula, print exactly one line.

If the formula is satisfiable, output its least satisfying assignment — the unique assignment obtained by setting every variable to false and then forcing a variable to true only when some clause requires it. Every satisfiable Horn formula has exactly one such minimal assignment. List every variable that occurs in the formula exactly once, in lexicographically ascending order of the variable name, formatting each as NAME=true or NAME=false, joined by commas with no spaces (for example A=true,B=false,C=false).

If the formula is unsatisfiable, output the single word unsatisfiable.