Beth Tableaux

Your program must decide whether a given propositional (boolean) formula $E$ is valid — that is, whether it evaluates to $\mathbf{1}$ (true) under every assignment of boolean values to its variables. If $E$ is not valid, then it evaluates to $\mathbf{0}$ (false) for at least one assignment, and your program must also report such a falsifying assignment.

A naive method tries all $2^k$ assignments of the $k$ variables, which is hopeless for large $k$ and unlike the way people actually reason about formulas. The classical Beth tableau (semantic tableau) method searches for a counterexample directly: it keeps two collections of sub-formulas — those we are trying to make true and those we are trying to make false — and repeatedly breaks each compound formula down by its outermost connective. If every branch runs into a contradiction (the same formula forced both true and false, or $\mathbf{0}$ forced true, or $\mathbf{1}$ forced false), the formula is valid; a branch that survives with no contradiction gives a falsifying assignment (variables forced true get $\mathbf{1}$, those forced false get $\mathbf{0}$). You may use any correct method — only the final answer is checked.

Syntax. Formulas are built as follows, with the connectives listed from the highest priority to the lowest:

• Constants $\mathbf{1}$ (true) and $\mathbf{0}$ (false).
• Variables: the letters A–Z and a–z. They are case-sensitive, so A and a are different variables.
• Parentheses: if $E$ is a formula, then so is $(E)$.
• Negation: $\neg E$.
• Conjunction $E_1 \wedge E_2 \wedge \cdots \wedge E_n$, evaluated left to right: $E_1 \wedge E_2 \wedge E_3 = (E_1 \wedge E_2) \wedge E_3$.
• Disjunction $E_1 \vee E_2 \vee \cdots \vee E_n$, also evaluated left to right.
• Implication $E_1 \Rightarrow E_2$, evaluated right to left: $E_1 \Rightarrow E_2 \Rightarrow E_3$ means $E_1 \Rightarrow (E_2 \Rightarrow E_3)$.
• Equivalence $E_1 \equiv E_2 \equiv \cdots \equiv E_n$, defined as $(E_1 \equiv E_2) \wedge (E_2 \equiv E_3) \wedge \cdots \wedge (E_{n-1} \equiv E_n)$.

The connectives have their usual truth tables: $\neg$ is logical NOT, $\wedge$ is AND, $\vee$ is OR, $A \Rightarrow B$ equals $\neg A \vee B$, and $A \equiv B$ is true exactly when $A$ and $B$ have the same value.

A single line containing the formula, written as a string of tokens: 0, 1, the letters A–Z and a–z, (, ), ~, &, |, =>, and =. The last five tokens stand for $\neg$, $\wedge$, $\vee$, $\Rightarrow$, and $\equiv$ respectively. Tokens may be separated by any number of spaces. The line contains at most $1000$ characters, and the formula is guaranteed to be syntactically correct.

Print exactly one line.

• If the formula is valid, print true.
• Otherwise print false. If the formula contains at least one variable, append : followed by the lexicographically smallest falsifying assignment. Sort the variables in ascending order by character code (so uppercase letters come before lowercase), and among all assignments that make the formula equal to $\mathbf{0}$ choose the one whose bit vector is smallest, reading the first variable as the most significant bit and taking $0 < 1$. Write the assignment as var=value pairs joined by , (a comma and a space), for example false: A=0, B=1. If the formula has no variables at all, print just false.