Boolean Satisfiability

The Boolean satisfiability problem (SAT) is known to be a very hard problem in computer science. You are given a Boolean formula, and you decide whether its variables can be consistently replaced by the values true or false so that the formula evaluates to true. SAT is NP-complete, and it stays NP-complete for 3-CNF formulas (3-SAT). SAT for 2-CNF formulas (2-SAT), on the other hand, is in P.

#SAT is the extension of SAT. In #SAT you not only decide whether such a replacement exists, you count how many replacements make the formula true. That problem is #P-complete even for 2-CNF formulas. Here you solve #1-DNF-SAT, which is #SAT for 1-DNF formulas.

You are given a Boolean formula in 1-DNF form. It is a disjunction (logical or) of one or more clauses, each clause is exactly one literal, and each literal is either a variable or its negation (logical not).

Formally:

 ⟨formula⟩ ::= ⟨clause⟩ | ⟨formula⟩ ∨ ⟨clause⟩
  ⟨clause⟩ ::= ⟨literal⟩
 ⟨literal⟩ ::= ⟨variable⟩ | ¬ ⟨variable⟩
⟨variable⟩ ::= A . . . Z | a . . . z

Count the ways to replace every variable that occurs in the formula with true or false so that the formula evaluates to true. All occurrences of the same variable get the same value. A letter that does not occur in the formula is not a variable of the formula and is not assigned.

The only line of input contains a logical formula in 1-DNF form, no longer than 1000 symbols. The logical operations are written | (disjunction) and ~ (negation). The variables are A to Z and a to z, and uppercase and lowercase letters are different variables. The formula contains no spaces and no characters outside the grammar above.

Print a single integer, the answer to the #SAT problem for the given formula.