![image](https://hackmd.io/_uploads/rkGv7JdBZg.png) # BLISK: When Your Public Key Learns Boolean Logic Welcome to **[BLISK](https://eprint.iacr.org/2026/088)** -- **B**oolean circuit **L**ogic **I**ntegrated into the **S**ingle **K**ey. It's like teaching your public key to understand complex relationship drama, except the drama is your organization's approval hierarchy. ## Limitations of Threshold Signatures Let's be honest. [Threshold signatures](https://eprint.iacr.org/2020/852.pdf) are great. They're efficient. They're elegant. They allow the production of a single signature from multiple parties. But they have one critical limitation: *they can only count*. A 3-of-5 threshold signature says: "I don't care who exactly signs the transaction, as long as 3 of you (5) must do it". But real organizations don't work that way. Real policies look like: - the CEO **OR** the CFO must approve, **AND** at least one board member - two executives **AND** compliance officer **AND** (legal **OR** counsel officer) - Carol can send the payment if (Alice **OR** Bob) approves* - ... > **Carol is a 6-year-old child of Alice and Bob, so we need to be careful about her desires. At the same time, Bob shouldn't be able to cooperate with Alice and pay for the dentist's services instead of the pink unicorn without Carol's approval.* To understand why we provided such examples, try expressing `(A ∨ B) ∧ (C ∨ D)` with a $k$-of-$n$ threshold signature. Go ahead, we will wait. *[elevator music plays]* You can't. That's the fundamental limitation. Threshold schemes can express cardinality but not the structure. > *We will use a Boolean circuit with OR (∨) and AND(∧) gates as a method to express the policy. Sometimes we will use (and draw) *trees* instead of the circuit, but note that it's the same.* ## BLISK: AND is a Multisig, OR is a Shared Secret Here's where it gets beautiful. BLISK noticed something hiding in plain sight: - $n$-of-$n$ multisignatures naturally implement an AND gate: all participants must contribute for a signature to be valid. That's literally what "and" means - key agreement protocols implement OR: in a key agreement (like Diffie-Hellman), any single participant can derive the shared secret. That's literally what "or" means So what if we just... composed them? ![Screenshot 2026-01-13 at 18.52.15](https://hackmd.io/_uploads/HJi8ug4B-l.png) >*In this blog, we show an example with MuSig2 and ECDH combination. But in practice, you can use any combination, including post-quantum primitives, as we mention in the paper.* ## The Math of Primitives *All good, it doesn't bite* Let's see how this actually works. We'll use the `secp256k1` curve with the generator $G, s.t.\langle G\rangle = \mathbb{G}$ and build up from primitives. Let $\mathsf{sk} \in \mathbb{F}_q$ be a private key (scalar) and $\mathsf{pk} = [\mathsf{sk}]G \in \mathbb{G}$ be a public key (EC point). $\mathcal{H}$ is a hash function. ### Primitive 1 - AND For AND gates, we use a key aggregation. Given public keys $\mathsf{pk}_A$ and $\mathsf{pk}_B$: $$\mathsf{pk}_\land=\mathsf{KeyAgg}(\mathsf{pk}_A,\mathsf{pk}_B) = [a_A]\mathsf{pk}_A + [a_B]\mathsf{pk}_B,$$ where $a_i = \mathcal{H}(\{\mathsf{pk}_A, \mathsf{pk}_B\},\mathsf{pk}_i)$ prevents rogue key attacks. This is just MuSig2 key aggregation technique. >*The key aggregation method may vary depending on the multisignature scheme. We will finally present an example with MuSig2; that's why we refer to it here.* ### Primitive 2 - OR For OR gates, we use a key agreement protocol (ECDH for simplification). Given public keys $\mathsf{pk}_A$ and $\mathsf{pk}_B$: $$\mathsf{sk}_\lor=\mathcal{H}([\mathsf{sk}_A]\mathsf{pk}_B)=\mathcal{H}([\mathsf{sk}_B]\mathsf{pk}_A)$$ Either Alice or Bob can compute this shared secret. The corresponding public key is calculated as $$\mathsf{pk}_\lor=[\mathsf{sk}_\lor]G$$ >*Instead of ECDH you can use also Key Encapsulation Mechanisms (KEM), even post-quantum ones such as new FIPS203* ### All Together That's basically it. We can combine it arbitrarily (not really, ha-ha, but we'll explain why later) to express any logic we want. What is clear from our primitives is that each node in the policy tree gets mapped to a public key, and the root public key is what you put on-chain. ![Screenshot 2026-01-13 at 18.47.22](https://hackmd.io/_uploads/rymUPg4Hbe.png) Only participants who meet the policy requirements need to participate. They combine their signatures according to the tree structure and produce a standard aggregated signature. The verifier? They just check one signature against one public key. An entire ignorance of organizational complexity. ![Screenshot 2026-01-13 at 18.51.10](https://hackmd.io/_uploads/SkzXdxNHZe.png) >*We see that Alice can't collaborate with Bob and create a valid signature over the aggregated public key. To do this, any of them needs to access $\mathcal{H}([\mathsf{sk}_C]\mathsf{pk}_D)$, which isn't possible if Carol's or Dave's keys aren't compromised.* ### Nuance #1. Conjunctive Normal Form There's a catch to why we can (but not really) combine gates arbitrarily: BLISK requires policies in Conjunctive Normal Form (CNF) -- an AND of ORs, with the root being a single AND gate. Why? Because the signing protocol relies on the key aggregation at the top level. We aggregate keys with AND semantics: all aggregated keys must contribute a partial signature. So we need the root to be AND, and its children to be OR gates (which get resolved to single keys via key agreement). Any monotone Boolean formula can be converted to CNF using the distributive law: $$(A \land B) \lor C = (A \lor C) \land (B \lor C)$$ For an example of a 2-of-3 threshold signature: ![Screenshot 2026-01-12 at 18.49.31](https://hackmd.io/_uploads/ry3DUsGrZg.png) But beware: CNF conversion can blow up exponentially. For most real-world policies, this is fine, but don't try to encode a 50-of-100 threshold = your circuit will explode. The good news? The BLISK compiler (*the first implicit reference to our PoC implementation*) handles this automatically. Write your policy in whatever form makes sense, and let the compiler normalize it. ### Nuance #2. Resolution Aspects OR gates, unfortunately, don't resolve themselves. Someone needs to compute the shared secret and publish the corresponding public key. This is the resolution process. Key insight: resolution is sequential. You can't resolve a parent OR gate until its children are resolved (if they're also OR gates). The process flows bottom-up through the tree. Who resolves what? Any participant who can derive the shared secret. For a 2-way OR gate over Alice and Bob, either one can resolve it. For a 3-way OR gate $(A \lor B \lor C)$, we typically structure it as nested 2-way gates: $((A \lor B) \lor C)$. Alice can resolve the outer gate (using her key and the inner gate's public key), OR anyone from the inner gate can resolve their part first. > *We consider only fan-2 OR gates so higher-degree disjunctions must be encoded as binary trees, which logic resembles so called tree-based continuous group tree agreement protocols such as [ART](https://hackmd.io/5LMmER7hRYa4CGJTMJaNIg) or [MLS](https://eprint.iacr.org/2020/1327.pdf).* In practice: - the first participant to accept the policy resolves all gates they can access - subsequent participants resolve the remaining gates - once all gates are resolved, the circuit is active and the root public key is determined > *This is why we use the "policy acceptance" operation later: each participant explicitly opts in by resolving their accessible nodes.* ### Nuance #3. Verifiable Operations Here's the trust problem: when Alice says "I resolved this OR gate and here's the public key $\mathsf{pk}_\lor$", how do we know she did it correctly? She could have just generated a random key that only she controls (or even which cancels the sibling key in the circuit). That would break the whole "OR" semantics -- Bob couldn't sign even though he's supposed to be able to. The solution: zero-knowledge proofs. When resolving an OR gate, the resolver must provide proof that: - They control one of the child keys (membership proof) - The derived secret was computed correctly via key agreement - The published public key matches the derived secret This makes all operations publicly verifiable. Anyone can verify that the circuit was compiled correctly without relying on the resolver. The same mechanism enables verifiable key rotation: when Alice updates her key, she proves that the new OR-gate keys were derived correctly from it. > *The idea of verifiable key agreement trees came from the [0-ART paper](https://eprint.iacr.org/2025/1874).* ## Generalizing BLISK So, the BLISK multisignature consists of the following steps: 1. **Parameters setup.** The participants select the curve, hash function, underlying signature scheme (and corresponding key-aggregation technique), key-agreement protocol, proving system, etc. 2. **Key generation.** Each participant generates their own key pair. What makes the BLISK construction interesting is that users don't need to generate a fresh key material and can connect their long-term keys to the specific BLISK signature instance (that's where DKG sucks =)). 3. **Policy initialization.** Users form the boolean policy circuit -- how exactly their common-created account/address must be controlled. The circuit is inactive; it has only defined leaves and the structure, and all internal wires aren't defined. 4. **Policy acceptance.** Each user confirms the policy by resolving the list of nodes they can. To make a resolution process verifiable, the user needs to provide appropriate proof. The policy circuit becomes active when all its nodes are resolved. 5. **Key aggregation.** When the policy circuit is resolved, we can obtain the common (aggregated) public key. You can transfer money to this key, and it can be spent only if the policy rules are executed. 6. **Signature generation**. The subset of quorum (that satisfies the policy) can produce the signature of a transaction or message verifiable by a single aggregated public key. The signature verification procedure doesn't differ from the single signature verification. 7. **Signature verification**. It is literally Schnorr signature verification with a signle verification key set as a root policy tree public key. 8. **Key rotation.** Each user can update their key in the tree. The update process is non-interactive (here DKG sucks again), doesn't require fresh key material, and is verifiable. ## Example: Implementing 3-of-5 Threshold with BLISK ### Policy creation Let's see how to express a 3-of-5 threshold over signers $\{A,B,C,D,E\}$ using BLISK (let's say our goal to create 3-of-5 multisig on Bitcoin). A 3-of-5 threshold means: at least 3 of the 5 participants must sign. In Boolean logic, this is the disjunction of all possible 3-person combinations: `(A ∧ B ∧ C) ∨ (A ∧ B ∧ D) ∨ (A ∧ B ∧ E) ∨ (A ∧ C ∧ D) ∨ (A ∧ C ∧ E) ∨ (A ∧ D ∧ E) ∨ (B ∧ C ∧ D) ∨ (B ∧ C ∧ E) ∨ (B ∧ D ∧ E) ∨ (C ∧ D ∧ E)` That's $(\frac{5}{3})=10$ combination. In CNF (Conjunctive Normal Form), we flip it: the policy is satisfied iff NO pair is completely absent. This gives us: `(A ∨ B ∨ C) ∧ (A ∨ B ∨ D) ∧ (A ∨ B ∨ E) ∧ (A ∨ C ∨ D) ∧ (A ∨ C ∨ E) ∧ (A ∨ D ∨ E) ∧ (B ∨ C ∨ D) ∧ (B ∨ C ∨ E) ∧ (B ∨ D ∨ E) ∧ (C ∨ D ∨ E)` The circuit structure is following: ![Screenshot 2026-01-12 at 16.15.01](https://hackmd.io/_uploads/BkQ-fKfH-l.png) In the BLISK reference implementation, you'd write this as (while we were publishing this blog, @juja256 added the threshold operator, so now you can define it as `(policy threshold_3_of_5 (threshold 3 A B C D E))`): ``` (policy threshold_3_of_5 (and (or A B C) (or A B D) (or A B E) (or A C D) (or A C E) (or A D E) (or B C D) (or B C E) (or B D E) (or C D E))) ``` > *The second implicit reference to PoC* ### Key Generation First of all, each party $x \in \{A,B,C,D,E\}$ generates their own `secp256k1` key pair. $$\mathsf{sk}_x \xleftarrow{\$} \mathbb{F}_q, \quad \mathsf{pk}_x = [\mathsf{sk}_x]G$$ ### Policy initialization The coordinator creates an inactive circuit based on quorum public keys: ![Screenshot 2026-01-12 at 13.55.21](https://hackmd.io/_uploads/HyDrbwGHbx.png) Thus, each internal wire corresponds to the user's public key. However, the circuit isn't active because the internal nodes aren't defined (we denote them with '$\bot$'). After each user accepts the policy, we will receive the complete active circuit and a root public key. ### Policy acceptance After the initial inactive circuit is formed, it must be accepted (resolved) by each user to be active. The acceptance process is sequential and consists of calculating the public key in the node that each child can access. So, let's start with Alice. Alice can resolve 12 nodes as shown in the picture below: ![Screenshot 2026-01-12 at 16.15.46](https://hackmd.io/_uploads/rJA7ftGrZx.png) To resolve a node, the user needs to derive a secret and public key for the specific node (using Diffie-Hellman) and prove they did it correctly. So Alice does: $$ \begin{gather} \mathsf{DH}(A,B) \gets [\mathsf{dh}(A,B)]G = \mathcal{H}([\mathsf{sk}_A]\mathsf{pk}_B)G = \mathcal{H}([\mathsf{sk}_B]\mathsf{pk}_A)G, \\ ... \\ \mathsf{DH}(A,D) \gets [\mathsf{dh}(A,D)]G = \mathcal{H}([\mathsf{sk}_A]\mathsf{pk}_D)G = \mathcal{H}([\mathsf{sk}_D]\mathsf{pk}_A)G, \\ \mathsf{DH}(AB,C) \gets [\mathsf{dh}(AB,C)]G = \mathcal{H}([\mathcal{H}([\mathsf{sk}_A]\mathsf{pk}_B)]\mathsf{pk}_C)G = \mathcal{H}([\mathsf{sk}_C]\mathsf{DH}(A,B))G, \\ ... \\ \\ \mathsf{DH}(AD,E) \gets [\mathsf{dh}(AD,E)]G = \mathcal{H}([\mathcal{H}([\mathsf{sk}_A]\mathsf{pk}_D)]\mathsf{pk}_E)G = \mathcal{H}([\mathsf{sk}_E]\mathsf{DH}(A,D))G \end{gather} $$ And provides a corresponding proof $\pi_{\mathcal{R}}$ for nodes' public keys correctness. Yes, relation $\mathcal{R}$ consists of 12 subrelations, each corresponding to the correctness of a specific node. When such proofs are provided (and verified), Bob decides which nodes he can resolve (it doesn't make sense to resolve the nodes which are already resolved by Alice). ![Screenshot 2026-01-12 at 16.18.06](https://hackmd.io/_uploads/ryu2GYzS-g.png) We can see that Bob needs to cover only 6 nodes, so the proof is much easier than Alice's. We have only 3 nodes left (including the root node). Any of $\{C,D,E\}$ can resolve them. Let Carol do it. ### Key aggregation Carol can complete the setup procedure by resolving the last two nodes (the root public key can then be calculated/aggregated publicly). ![Screenshot 2026-01-12 at 16.25.06](https://hackmd.io/_uploads/HkCvNKzSbg.png) > *Despite we don't require D and E to participate in policy acceptance procedure, on the practice it would be great if Dave and Eve prove they control appropriate secret keys, so we can require them to sign some setup message for policy acceptance.* We have no empty nodes anymore, and consider the policy as active. So we can calculate a common public key (and send BTC to it). We do it by the MuSig2 key aggregation technique, but for all top OR gates we have in the circuit (see the picture above). ### Signature generation Let's prove the signature works for a quorum of 3. For example, we have Bob, Dave, and Eve, who decide to sign the transaction. We still follow the MuSig2 signature scheme. #### Nonce Commitment Here's where it gets real. We noted that our aggregated key comprises 10 components (10 top OR gates). We require nonces for each of the 10 partial signatures. MuSig2 uses $\nu = 4$ nonces per signature share. So each signer generates nonces for each gate they're responsible for. Having the order $Bob \to Dave \to Eve$, we can notice Bob can uniquely derive the key for 6 nodes, Dave for 3 more, and Eve can produce the final signature share. Each needs to generate an appropriate number of nonces. ``` let R ← [10][4] // empty nonce matrix // Bob: for gate in [1, 2, 3, 7, 8, 9]: for l = 1 to 4: rB[gate, l] ← random scalar RB[gate, l] = rB[gate, l]G R[gate, l] = RB[gate, l] // 24 nonce points total // Dave: for gate in [4, 6, 10]: for l = 1 to 4: rD[gate, l] ← random scalar RD[gate, l] = rD[gate, l]G R[gate, l] = RD[gate, l] // 12 nonce points total // Eve: for gate = 5: for l = 1 to 4: rE[gate, l] ← random scalar RE[gate, l] = rE[gate, l]G R[gate, l] = RE[gate, l] // 4 nonce points total ``` #### Signature share calculation Having the commited nonces each party can calculate the nonce coefficient as $$b = \mathcal{H}(\mathsf{pk}_{agg}, \{R_{gate,l}\},m)$$ and compute a final nonce point as: $$R = \sum_{gate = 1}^{10}\sum_{l=1}^4 [b^{(l-1)}]\cdot R_{gate, l}$$ The signature challenge is $$c = \mathcal{H}(\mathsf{pk}_{agg}, R, m)$$ Then Bob, Dave and Eve calculate signature shares for all gates they are responsible for: $$ \begin{gather*} s_{gate1}^{Bob} = (\sum_{l=1}^4 b^{(l-1)}rB_{gate1})+c\cdot a_{ABC}\cdot\mathcal{H}(\mathcal{H}[[\mathsf{sk}_B]\mathsf{pk}_A]\cdot\mathsf{pk}_C), \\... \\ s_{gate5}^{Eve} = (\sum_{l=1}^4 b^{(l-1)}rE_{gate5})+c\cdot a_{ACE}\cdot\mathcal{H}([\mathsf{sk}_E]\mathsf{pk}_{AC}), \end{gather*} $$ where $a_{ABC}$ and $a_{ACE}$ corresponding coefficient needed for key aggregation and $\mathsf{pk}_{AC} = \mathsf{DH}(A,C)$ is a public key corresponding to the secret share established between Alice and Carol (picture below for clarity). ![Screenshot 2026-01-12 at 21.06.16](https://hackmd.io/_uploads/Bk1IUpGrWg.png) After each share for the top OR gates is created we can simply aggregate them to $$s = \sum_{i=1}^{10} s_{gate\ i}$$ The signature verification corresponds to usual single Schnorr signature verification. >*Homework. Try selecting any other quorum of 3 and verify whether the signature can be created (all top OR gate nodes must be painted over).* #### The Cherry on Top: Key Rotation Alice wants to update her public key in the policy tree. In traditional threshold schemes, you'd need to run DKG all over again with everyone. In BLISK? Alice generates a new key pair and publishes a key update: The update proof contains: - A signature from Alice's old key (proving she authorized it) - A ZK proof that the new OR-gate keys were correctly derived Other participants don't need to do anything except verify the proof. Non-interactive (you already know what DKG does). ## Example 2: More Complex Policies We have shown that BLISK works for the cases of threshold signature but without DKG. Now let's have some fun. Here are real-world policies that would make threshold signatures cry. Corporate treasury with the policy: "CFO required, plus either (CEO or 2-of-3 board members)". Having our expression syntax: ``` (policy corporate_treasury (and CFO (or CEO (and BM1 BM2) (and BM1 BM3) (and BM2 BM3)))) ``` Or simply `CFO ∧ (CEO ∨ BM1 ∨ BM2) ∧ (CEO ∨ BM2 ∨ BM3) ∧ (CEO ∨ BM1 ∨ BM3)` Try to build such a policy on your side! > *The third implicit reference to our compiler!* ## The Caveats (Because Nothing Is Free) - CNF Blowup: Converting arbitrary formulas to CNF can exponentially increase size. In practice, most real policies are manageable, but be aware. |Threshold|DNF Clauses C(n,k)|CNF Clauses C(n,m)| |---|---|---| | 2-of-3 | 3 | 3 | | 3-of-4 | 4 | 6 | | 2-of-4 | 6 | 4 | | 11-of-15 | 1365 | 3003 | | 13-of-15 | 105 | 455 | Here is an example for 11-of-15 policy. ``` Policy 'Threshold 11/15' Parsing time: 8.445µs Key generation time: 1.38785ms Compilation time: 336.16233ms Compiled S-Expression: (and (or (or A B) (or C (or D E))) (or (or A B) (or C (or D F))) (or (or A B) (or C (or D G))) (or (or A B) (or C (or D H))) (or (or A B) (or C (or D I))) (or (or A B) (or C (or D J))) (or (or A B) (or C (or D K))) (or (or A B) (or C (or D L))) (or (or A B) (or C (or D M))) (or (or A B) (or C (or D N))) (or (or A B) (or C (or D O))) (or (or A B) (or C (or E F))) (or (or A B) (or C (or E G))) (or (or A B) (or C (or E H))) (or (or A B) (or C (or E I))) (or (or A B) (or C (or E J))) (or (or A B) (or C (or E K))) (or (or A B) (or C (or E L))) (or (or A B) (or C (or E M))) (or (or A B) (or C (or E N))) (or (or A B) (or C (or E O))) (or (or A B) (or C (or F G))) (or (or A B) (or C (or F H))) (or (or A B) (or C (or F I))) (or (or A B) (or C (or F J))) (or (or A B) (or C (or F K))) (or (or A B) (or C (or F L))) (or (or A B) (or C (or F M))) (or (or A B) (or C (or F N))) (or (or A B) (or C (or F O))) (or (or A B) (or C (or G H))) (or (or A B) (or C (or G I))) (or (or A B) (or C (or G J))) (or (or A B) (or C (or G K))) (or (or A B) (or C (or G L))) (or (or A B) (or C (or G M))) (or (or A B) (or C (or G N))) (or (or A B) (or C (or G O))) (or (or A B) (or C (or H I))) (or (or A B) (or C (or H J))) (or (or A B) (or C (or H K))) (or (or A B) (or C (or H L))) (or (or A B) (or C (or H M))) (or (or A B) (or C (or H N))) (or (or A B) (or C (or H O))) (or (or A B) (or C (or I J))) (or (or A B) (or C (or I K))) (or (or A B) (or C (or I L))) (or (or A B) (or C (or I M))) (or (or A B) (or C (or I N))) (or (or A B) (or C (or I O))) (or (or A B) (or C (or J K))) (or (or A B) (or C (or J L))) (or (or A B) (or C (or J M))) (or (or A B) (or C (or J N))) (or (or A B) (or C (or J O))) (or (or A B) (or C (or K L))) (or (or A B) (or C (or K M))) (or (or A B) (or C (or K N))) (or (or A B) (or C (or K O))) (or (or A B) (or C (or L M))) (or (or A B) (or C (or L N))) (or (or A B) (or C (or L O))) (or (or A B) (or C (or M N))) (or (or A B) (or C (or M O))) (or (or A B) (or C (or N O))) (or (or A B) (or D (or E F))) (or (or A B) (or D (or E G))) (or (or A B) (or D (or E H))) (or (or A B) (or D (or E I))) (or (or A B) (or D (or E J))) (or (or A B) (or D (or E K))) (or (or A B) (or D (or E L))) (or (or A B) (or D (or E M))) (or (or A B) (or D (or E N))) (or (or A B) (or D (or E O))) (or (or A B) (or D (or F G))) (or (or A B) (or D (or F H))) (or (or A B) (or D (or F I))) (or (or A B) (or D (or F J))) (or (or A B) (or D (or F K))) (or (or A B) (or D (or F L))) (or (or A B) (or D (or F M))) (or (or A B) (or D (or F N))) (or (or A B) (or D (or F O))) (or (or A B) (or D (or G H))) (or (or A B) (or D (or G I))) (or (or A B) (or D (or G J))) (or (or A B) (or D (or G K))) (or (or A B) (or D (or G L))) (or (or A B) (or D (or G M))) (or (or A B) (or D (or G N))) (or (or A B) (or D (or G O))) (or (or A B) (or D (or H I))) (or (or A B) (or D (or H J))) (or (or A B) (or D (or H K))) (or (or A B) (or D (or H L))) (or (or A B) (or D (or H M))) (or (or A B) (or D (or H N))) (or (or A B) (or D (or H O))) (or (or A B) (or D (or I J))) (or (or A B) (or D (or I K))) (or (or A B) (or D (or I L))) (or (or A B) (or D (or I M))) (or (or A B) (or D (or I N))) (or (or A B) (or D (or I O))) (or (or A B) (or D (or J K))) (or (or A B) (or D (or J L))) (or (or A B) (or D (or J M))) (or (or A B) (or D (or J N))) (or (or A B) (or D (or J O))) (or (or A B) (or D (or K L))) (or (or A B) (or D (or K M))) (or (or A B) (or D (or K N))) (or (or A B) (or D (or K O))) (or (or A B) (or D (or L M))) (or (or A B) (or D (or L N))) (or (or A B) (or D (or L O))) (or (or A B) (or D (or M N))) (or (or A B) (or D (or M O))) (or (or A B) (or D (or N O))) (or (or A B) (or E (or F G))) (or (or A B) (or E (or F H))) (or (or A B) (or E (or F I))) (or (or A B) (or E (or F J))) (or (or A B) (or E (or F K))) (or (or A B) (or E (or F L))) (or (or A B) (or E (or F M))) (or (or A B) (or E (or F N))) (or (or A B) (or E (or F O))) (or (or A B) (or E (or G H))) (or (or A B) (or E (or G I))) (or (or A B) (or E (or G J))) (or (or A B) (or E (or G K))) (or (or A B) (or E (or G L))) (or (or A B) (or E (or G M))) (or (or A B) (or E (or G N))) (or (or A B) (or E (or G O))) (or (or A B) (or E (or H I))) (or (or A B) (or E (or H J))) (or (or A B) (or E (or H K))) (or (or A B) (or E (or H L))) (or (or A B) (or E (or H M))) (or (or A B) (or E (or H N))) (or (or A B) (or E (or H O))) (or (or A B) (or E (or I J))) (or (or A B) (or E (or I K))) (or (or A B) (or E (or I L))) (or (or A B) (or E (or I M))) (or (or A B) (or E (or I N))) (or (or A B) (or E (or I O))) (or (or A B) (or E (or J K))) (or (or A B) (or E (or J L))) (or (or A B) (or E (or J M))) (or (or A B) (or E (or J N))) (or (or A B) (or E (or J O))) (or (or A B) (or E (or K L))) (or (or A B) (or E (or K M))) (or (or A B) (or E (or K N))) (or (or A B) (or E (or K O))) (or (or A B) (or E (or L M))) (or (or A B) (or E (or L N))) (or (or A B) (or E (or L O))) (or (or A B) (or E (or M N))) (or (or A B) (or E (or M O))) (or (or A B) (or E (or N O))) (or (or A B) (or F (or G H))) (or (or A B) (or F (or G I))) (or (or A B) (or F (or G J))) (or (or A B) (or F (or G K))) (or (or A B) (or F (or G L))) (or (or A B) (or F (or G M))) (or (or A B) (or F (or G N))) (or (or A B) (or F (or G O))) (or (or A B) (or F (or H I))) (or (or A B) (or F (or H J))) (or (or A B) (or F (or H K))) (or (or A B) (or F (or H L))) (or (or A B) (or F (or H M))) (or (or A B) (or F (or H N))) (or (or A B) (or F (or H O))) (or (or A B) (or F (or I J))) (or (or A B) (or F (or I K))) (or (or A B) (or F (or I L))) (or (or A B) (or F (or I M))) (or (or A B) (or F (or I N))) (or (or A B) (or F (or I O))) (or (or A B) (or F (or J K))) (or (or A B) (or F (or J L))) (or (or A B) (or F (or J M))) (or (or A B) (or F (or J N))) (or (or A B) (or F (or J O))) (or (or A B) (or F (or K L))) (or (or A B) (or F (or K M))) (or (or A B) (or F (or K N))) (or (or A B) (or F (or K O))) (or (or A B) (or F (or L M))) (or (or A B) (or F (or L N))) (or (or A B) (or F (or L O))) (or (or A B) (or F (or M N))) (or (or A B) (or F (or M O))) (or (or A B) (or F (or N O))) (or (or A B) (or G (or H I))) (or (or A B) (or G (or H J))) (or (or A B) (or G (or H K))) (or (or A B) (or G (or H L))) (or (or A B) (or G (or H M))) (or (or A B) (or G (or H N))) (or (or A B) (or G (or H O))) (or (or A B) (or G (or I J))) (or (or A B) (or G (or I K))) (or (or A B) (or G (or I L))) (or (or A B) (or G (or I M))) (or (or A B) (or G (or I N))) (or (or A B) (or G (or I O))) (or (or A B) (or G (or J K))) (or (or A B) (or G (or J L))) (or (or A B) (or G (or J M))) (or (or A B) (or G (or J N))) (or (or A B) (or G (or J O))) (or (or A B) (or G (or K L))) (or (or A B) (or G (or K M))) (or (or A B) (or G (or K N))) (or (or A B) (or G (or K O))) (or (or A B) (or G (or L M))) (or (or A B) (or G (or L N))) (or (or A B) (or G (or L O))) (or (or A B) (or G (or M N))) (or (or A B) (or G (or M O))) (or (or A B) (or G (or N O))) (or (or A B) (or H (or I J))) (or (or A B) (or H (or I K))) (or (or A B) (or H (or I L))) (or (or A B) (or H (or I M))) (or (or A B) (or H (or I N))) (or (or A B) (or H (or I O))) (or (or A B) (or H (or J K))) (or (or A B) (or H (or J L))) (or (or A B) (or H (or J M))) (or (or A B) (or H (or J N))) (or (or A B) (or H (or J O))) (or (or A B) (or H (or K L))) (or (or A B) (or H (or K M))) (or (or A B) (or H (or K N))) (or (or A B) (or H (or K O))) (or (or A B) (or H (or L M))) (or (or A B) (or H (or L N))) (or (or A B) (or H (or L O))) (or (or A B) (or H (or M N))) (or (or A B) (or H (or M O))) (or (or A B) (or H (or N O))) (or (or A B) (or I (or J K))) (or (or A B) (or I (or J L))) (or (or A B) (or I (or J M))) (or (or A B) (or I (or J N))) (or (or A B) (or I (or J O))) (or (or A B) (or I (or K L))) (or (or A B) (or I (or K M))) (or (or A B) (or I (or K N))) (or (or A B) (or I (or K O))) (or (or A B) (or I (or L M))) (or (or A B) (or I (or L N))) (or (or A B) (or I (or L O))) (or (or A B) (or I (or M N))) (or (or A B) (or I (or M O))) (or (or A B) (or I (or N O))) (or (or A B) (or J (or K L))) (or (or A B) (or J (or K M))) (or (or A B) (or J (or K N))) (or (or A B) (or J (or K O))) (or (or A B) (or J (or L M))) (or (or A B) (or J (or L N))) (or (or A B) (or J (or L O))) (or (or A B) (or J (or M N))) (or (or A B) (or J (or M O))) (or (or A B) (or J (or N O))) (or (or A B) (or K (or L M))) (or (or A B) (or K (or L N))) (or (or A B) (or K (or L O))) (or (or A B) (or K (or M N))) (or (or A B) (or K (or M O))) (or (or A B) (or K (or N O))) (or (or A B) (or L (or M N))) (or (or A B) (or L (or M O))) (or (or A B) (or L (or N O))) (or (or A B) (or M (or N O))) (or (or A C) (or D (or E F))) (or (or A C) (or D (or E G))) (or (or A C) (or D (or E H))) (or (or A C) (or D (or E I))) (or (or A C) (or D (or E J))) (or (or A C) (or D (or E K))) (or (or A C) (or D (or E L))) (or (or A C) (or D (or E M))) (or (or A C) (or D (or E N))) (or (or A C) (or D (or E O))) (or (or A C) (or D (or F G))) (or (or A C) (or D (or F H))) (or (or A C) (or D (or F I))) (or (or A C) (or D (or F J))) (or (or A C) (or D (or F K))) (or (or A C) (or D (or F L))) (or (or A C) (or D (or F M))) (or (or A C) (or D (or F N))) (or (or A C) (or D (or F O))) (or (or A C) (or D (or G H))) (or (or A C) (or D (or G I))) (or (or A C) (or D (or G J))) (or (or A C) (or D (or G K))) (or (or A C) (or D (or G L))) (or (or A C) (or D (or G M))) (or (or A C) (or D (or G N))) (or (or A C) (or D (or G O))) (or (or A C) (or D (or H I))) (or (or A C) (or D (or H J))) (or (or A C) (or D (or H K))) (or (or A C) (or D (or H L))) (or (or A C) (or D (or H M))) (or (or A C) (or D (or H N))) (or (or A C) (or D (or H O))) (or (or A C) (or D (or I J))) (or (or A C) (or D (or I K))) (or (or A C) (or D (or I L))) (or (or A C) (or D (or I M))) (or (or A C) (or D (or I N))) (or (or A C) (or D (or I O))) (or (or A C) (or D (or J K))) (or (or A C) (or D (or J L))) (or (or A C) (or D (or J M))) (or (or A C) (or D (or J N))) (or (or A C) (or D (or J O))) (or (or A C) (or D (or K L))) (or (or A C) (or D (or K M))) (or (or A C) (or D (or K N))) (or (or A C) (or D (or K O))) (or (or A C) (or D (or L M))) (or (or A C) (or D (or L N))) (or (or A C) (or D (or L O))) (or (or A C) (or D (or M N))) (or (or A C) (or D (or M O))) (or (or A C) (or D (or N O))) (or (or A C) (or E (or F G))) (or (or A C) (or E (or F H))) (or (or A C) (or E (or F I))) (or (or A C) (or E (or F J))) (or (or A C) (or E (or F K))) (or (or A C) (or E (or F L))) (or (or A C) (or E (or F M))) (or (or A C) (or E (or F N))) (or (or A C) (or E (or F O))) (or (or A C) (or E (or G H))) (or (or A C) (or E (or G I))) (or (or A C) (or E (or G J))) (or (or A C) (or E (or G K))) (or (or A C) (or E (or G L))) (or (or A C) (or E (or G M))) (or (or A C) (or E (or G N))) (or (or A C) (or E (or G O))) (or (or A C) (or E (or H I))) (or (or A C) (or E (or H J))) (or (or A C) (or E (or H K))) (or (or A C) (or E (or H L))) (or (or A C) (or E (or H M))) (or (or A C) (or E (or H N))) (or (or A C) (or E (or H O))) (or (or A C) (or E (or I J))) (or (or A C) (or E (or I K))) (or (or A C) (or E (or I L))) (or (or A C) (or E (or I M))) (or (or A C) (or E (or I N))) (or (or A C) (or E (or I O))) (or (or A C) (or E (or J K))) (or (or A C) (or E (or J L))) (or (or A C) (or E (or J M))) (or (or A C) (or E (or J N))) (or (or A C) (or E (or J O))) (or (or A C) (or E (or K L))) (or (or A C) (or E (or K M))) (or (or A C) (or E (or K N))) (or (or A C) (or E (or K O))) (or (or A C) (or E (or L M))) (or (or A C) (or E (or L N))) (or (or A C) (or E (or L O))) (or (or A C) (or E (or M N))) (or (or A C) (or E (or M O))) (or (or A C) (or E (or N O))) (or (or A C) (or F (or G H))) (or (or A C) (or F (or G I))) (or (or A C) (or F (or G J))) (or (or A C) (or F (or G K))) (or (or A C) (or F (or G L))) (or (or A C) (or F (or G M))) (or (or A C) (or F (or G N))) (or (or A C) (or F (or G O))) (or (or A C) (or F (or H I))) (or (or A C) (or F (or H J))) (or (or A C) (or F (or H K))) (or (or A C) (or F (or H L))) (or (or A C) (or F (or H M))) (or (or A C) (or F (or H N))) (or (or A C) (or F (or H O))) (or (or A C) (or F (or I J))) (or (or A C) (or F (or I K))) (or (or A C) (or F (or I L))) (or (or A C) (or F (or I M))) (or (or A C) (or F (or I N))) (or (or A C) (or F (or I O))) (or (or A C) (or F (or J K))) (or (or A C) (or F (or J L))) (or (or A C) (or F (or J M))) (or (or A C) (or F (or J N))) (or (or A C) (or F (or J O))) (or (or A C) (or F (or K L))) (or (or A C) (or F (or K M))) (or (or A C) (or F (or K N))) (or (or A C) (or F (or K O))) (or (or A C) (or F (or L M))) (or (or A C) (or F (or L N))) (or (or A C) (or F (or L O))) (or (or A C) (or F (or M N))) (or (or A C) (or F (or M O))) (or (or A C) (or F (or N O))) (or (or A C) (or G (or H I))) (or (or A C) (or G (or H J))) (or (or A C) (or G (or H K))) (or (or A C) (or G (or H L))) (or (or A C) (or G (or H M))) (or (or A C) (or G (or H N))) (or (or A C) (or G (or H O))) (or (or A C) (or G (or I J))) (or (or A C) (or G (or I K))) (or (or A C) (or G (or I L))) (or (or A C) (or G (or I M))) (or (or A C) (or G (or I N))) (or (or A C) (or G (or I O))) (or (or A C) (or G (or J K))) (or (or A C) (or G (or J L))) (or (or A C) (or G (or J M))) (or (or A C) (or G (or J N))) (or (or A C) (or G (or J O))) (or (or A C) (or G (or K L))) (or (or A C) (or G (or K M))) (or (or A C) (or G (or K N))) (or (or A C) (or G (or K O))) (or (or A C) (or G (or L M))) (or (or A C) (or G (or L N))) (or (or A C) (or G (or L O))) (or (or A C) (or G (or M N))) (or (or A C) (or G (or M O))) (or (or A C) (or G (or N O))) (or (or A C) (or H (or I J))) (or (or A C) (or H (or I K))) (or (or A C) (or H (or I L))) (or (or A C) (or H (or I M))) (or (or A C) (or H (or I N))) (or (or A C) (or H (or I O))) (or (or A C) (or H (or J K))) (or (or A C) (or H (or J L))) (or (or A C) (or H (or J M))) (or (or A C) (or H (or J N))) (or (or A C) (or H (or J O))) (or (or A C) (or H (or K L))) (or (or A C) (or H (or K M))) (or (or A C) (or H (or K N))) (or (or A C) (or H (or K O))) (or (or A C) (or H (or L M))) (or (or A C) (or H (or L N))) (or (or A C) (or H (or L O))) (or (or A C) (or H (or M N))) (or (or A C) (or H (or M O))) (or (or A C) (or H (or N O))) (or (or A C) (or I (or J K))) (or (or A C) (or I (or J L))) (or (or A C) (or I (or J M))) (or (or A C) (or I (or J N))) (or (or A C) (or I (or J O))) (or (or A C) (or I (or K L))) (or (or A C) (or I (or K M))) (or (or A C) (or I (or K N))) (or (or A C) (or I (or K O))) (or (or A C) (or I (or L M))) (or (or A C) (or I (or L N))) (or (or A C) (or I (or L O))) (or (or A C) (or I (or M N))) (or (or A C) (or I (or M O))) (or (or A C) (or I (or N O))) (or (or A C) (or J (or K L))) (or (or A C) (or J (or K M))) (or (or A C) (or J (or K N))) (or (or A C) (or J (or K O))) (or (or A C) (or J (or L M))) (or (or A C) (or J (or L N))) (or (or A C) (or J (or L O))) (or (or A C) (or J (or M N))) (or (or A C) (or J (or M O))) (or (or A C) (or J (or N O))) (or (or A C) (or K (or L M))) (or (or A C) (or K (or L N))) (or (or A C) (or K (or L O))) (or (or A C) (or K (or M N))) (or (or A C) (or K (or M O))) (or (or A C) (or K (or N O))) (or (or A C) (or L (or M N))) (or (or A C) (or L (or M O))) (or (or A C) (or L (or N O))) (or (or A C) (or M (or N O))) (or (or A D) (or E (or F G))) (or (or A D) (or E (or F H))) (or (or A D) (or E (or F I))) (or (or A D) (or E (or F J))) (or (or A D) (or E (or F K))) (or (or A D) (or E (or F L))) (or (or A D) (or E (or F M))) (or (or A D) (or E (or F N))) (or (or A D) (or E (or F O))) (or (or A D) (or E (or G H))) (or (or A D) (or E (or G I))) (or (or A D) (or E (or G J))) (or (or A D) (or E (or G K))) (or (or A D) (or E (or G L))) (or (or A D) (or E (or G M))) (or (or A D) (or E (or G N))) (or (or A D) (or E (or G O))) (or (or A D) (or E (or H I))) (or (or A D) (or E (or H J))) (or (or A D) (or E (or H K))) (or (or A D) (or E (or H L))) (or (or A D) (or E (or H M))) (or (or A D) (or E (or H N))) (or (or A D) (or E (or H O))) (or (or A D) (or E (or I J))) (or (or A D) (or E (or I K))) (or (or A D) (or E (or I L))) (or (or A D) (or E (or I M))) (or (or A D) (or E (or I N))) (or (or A D) (or E (or I O))) (or (or A D) (or E (or J K))) (or (or A D) (or E (or J L))) (or (or A D) (or E (or J M))) (or (or A D) (or E (or J N))) (or (or A D) (or E (or J O))) (or (or A D) (or E (or K L))) (or (or A D) (or E (or K M))) (or (or A D) (or E (or K N))) (or (or A D) (or E (or K O))) (or (or A D) (or E (or L M))) (or (or A D) (or E (or L N))) (or (or A D) (or E (or L O))) (or (or A D) (or E (or M N))) (or (or A D) (or E (or M O))) (or (or A D) (or E (or N O))) (or (or A D) (or F (or G H))) (or (or A D) (or F (or G I))) (or (or A D) (or F (or G J))) (or (or A D) (or F (or G K))) (or (or A D) (or F (or G L))) (or (or A D) (or F (or G M))) (or (or A D) (or F (or G N))) (or (or A D) (or F (or G O))) (or (or A D) (or F (or H I))) (or (or A D) (or F (or H J))) (or (or A D) (or F (or H K))) (or (or A D) (or F (or H L))) (or (or A D) (or F (or H M))) (or (or A D) (or F (or H N))) (or (or A D) (or F (or H O))) (or (or A D) (or F (or I J))) (or (or A D) (or F (or I K))) (or (or A D) (or F (or I L))) (or (or A D) (or F (or I M))) (or (or A D) (or F (or I N))) (or (or A D) (or F (or I O))) (or (or A D) (or F (or J K))) (or (or A D) (or F (or J L))) (or (or A D) (or F (or J M))) (or (or A D) (or F (or J N))) (or (or A D) (or F (or J O))) (or (or A D) (or F (or K L))) (or (or A D) (or F (or K M))) (or (or A D) (or F (or K N))) (or (or A D) (or F (or K O))) (or (or A D) (or F (or L M))) (or (or A D) (or F (or L N))) (or (or A D) (or F (or L O))) (or (or A D) (or F (or M N))) (or (or A D) (or F (or M O))) (or (or A D) (or F (or N O))) (or (or A D) (or G (or H I))) (or (or A D) (or G (or H J))) (or (or A D) (or G (or H K))) (or (or A D) (or G (or H L))) (or (or A D) (or G (or H M))) (or (or A D) (or G (or H N))) (or (or A D) (or G (or H O))) (or (or A D) (or G (or I J))) (or (or A D) (or G (or I K))) (or (or A D) (or G (or I L))) (or (or A D) (or G (or I M))) (or (or A D) (or G (or I N))) (or (or A D) (or G (or I O))) (or (or A D) (or G (or J K))) (or (or A D) (or G (or J L))) (or (or A D) (or G (or J M))) (or (or A D) (or G (or J N))) (or (or A D) (or G (or J O))) (or (or A D) (or G (or K L))) (or (or A D) (or G (or K M))) (or (or A D) (or G (or K N))) (or (or A D) (or G (or K O))) (or (or A D) (or G (or L M))) (or (or A D) (or G (or L N))) (or (or A D) (or G (or L O))) (or (or A D) (or G (or M N))) (or (or A D) (or G (or M O))) (or (or A D) (or G (or N O))) (or (or A D) (or H (or I J))) (or (or A D) (or H (or I K))) (or (or A D) (or H (or I L))) (or (or A D) (or H (or I M))) (or (or A D) (or H (or I N))) (or (or A D) (or H (or I O))) (or (or A D) (or H (or J K))) (or (or A D) (or H (or J L))) (or (or A D) (or H (or J M))) (or (or A D) (or H (or J N))) (or (or A D) (or H (or J O))) (or (or A D) (or H (or K L))) (or (or A D) (or H (or K M))) (or (or A D) (or H (or K N))) (or (or A D) (or H (or K O))) (or (or A D) (or H (or L M))) (or (or A D) (or H (or L N))) (or (or A D) (or H (or L O))) (or (or A D) (or H (or M N))) (or (or A D) (or H (or M O))) (or (or A D) (or H (or N O))) (or (or A D) (or I (or J K))) (or (or A D) (or I (or J L))) (or (or A D) (or I (or J M))) (or (or A D) (or I (or J N))) (or (or A D) (or I (or J O))) (or (or A D) (or I (or K L))) (or (or A D) (or I (or K M))) (or (or A D) (or I (or K N))) (or (or A D) (or I (or K O))) (or (or A D) (or I (or L M))) (or (or A D) (or I (or L N))) (or (or A D) (or I (or L O))) (or (or A D) (or I (or M N))) (or (or A D) (or I (or M O))) (or (or A D) (or I (or N O))) (or (or A D) (or J (or K L))) (or (or A D) (or J (or K M))) (or (or A D) (or J (or K N))) (or (or A D) (or J (or K O))) (or (or A D) (or J (or L M))) (or (or A D) (or J (or L N))) (or (or A D) (or J (or L O))) (or (or A D) (or J (or M N))) (or (or A D) (or J (or M O))) (or (or A D) (or J (or N O))) (or (or A D) (or K (or L M))) (or (or A D) (or K (or L N))) (or (or A D) (or K (or L O))) (or (or A D) (or K (or M N))) (or (or A D) (or K (or M O))) (or (or A D) (or K (or N O))) (or (or A D) (or L (or M N))) (or (or A D) (or L (or M O))) (or (or A D) (or L (or N O))) (or (or A D) (or M (or N O))) (or (or A E) (or F (or G H))) (or (or A E) (or F (or G I))) (or (or A E) (or F (or G J))) (or (or A E) (or F (or G K))) (or (or A E) (or F (or G L))) (or (or A E) (or F (or G M))) (or (or A E) (or F (or G N))) (or (or A E) (or F (or G O))) (or (or A E) (or F (or H I))) (or (or A E) (or F (or H J))) (or (or A E) (or F (or H K))) (or (or A E) (or F (or H L))) (or (or A E) (or F (or H M))) (or (or A E) (or F (or H N))) (or (or A E) (or F (or H O))) (or (or A E) (or F (or I J))) (or (or A E) (or F (or I K))) (or (or A E) (or F (or I L))) (or (or A E) (or F (or I M))) (or (or A E) (or F (or I N))) (or (or A E) (or F (or I O))) (or (or A E) (or F (or J K))) (or (or A E) (or F (or J L))) (or (or A E) (or F (or J M))) (or (or A E) (or F (or J N))) (or (or A E) (or F (or J O))) (or (or A E) (or F (or K L))) (or (or A E) (or F (or K M))) (or (or A E) (or F (or K N))) (or (or A E) (or F (or K O))) (or (or A E) (or F (or L M))) (or (or A E) (or F (or L N))) (or (or A E) (or F (or L O))) (or (or A E) (or F (or M N))) (or (or A E) (or F (or M O))) (or (or A E) (or F (or N O))) (or (or A E) (or G (or H I))) (or (or A E) (or G (or H J))) (or (or A E) (or G (or H K))) (or (or A E) (or G (or H L))) (or (or A E) (or G (or H M))) (or (or A E) (or G (or H N))) (or (or A E) (or G (or H O))) (or (or A E) (or G (or I J))) (or (or A E) (or G (or I K))) (or (or A E) (or G (or I L))) (or (or A E) (or G (or I M))) (or (or A E) (or G (or I N))) (or (or A E) (or G (or I O))) (or (or A E) (or G (or J K))) (or (or A E) (or G (or J L))) (or (or A E) (or G (or J M))) (or (or A E) (or G (or J N))) (or (or A E) (or G (or J O))) (or (or A E) (or G (or K L))) (or (or A E) (or G (or K M))) (or (or A E) (or G (or K N))) (or (or A E) (or G (or K O))) (or (or A E) (or G (or L M))) (or (or A E) (or G (or L N))) (or (or A E) (or G (or L O))) (or (or A E) (or G (or M N))) (or (or A E) (or G (or M O))) (or (or A E) (or G (or N O))) (or (or A E) (or H (or I J))) (or (or A E) (or H (or I K))) (or (or A E) (or H (or I L))) (or (or A E) (or H (or I M))) (or (or A E) (or H (or I N))) (or (or A E) (or H (or I O))) (or (or A E) (or H (or J K))) (or (or A E) (or H (or J L))) (or (or A E) (or H (or J M))) (or (or A E) (or H (or J N))) (or (or A E) (or H (or J O))) (or (or A E) (or H (or K L))) (or (or A E) (or H (or K M))) (or (or A E) (or H (or K N))) (or (or A E) (or H (or K O))) (or (or A E) (or H (or L M))) (or (or A E) (or H (or L N))) (or (or A E) (or H (or L O))) (or (or A E) (or H (or M N))) (or (or A E) (or H (or M O))) (or (or A E) (or H (or N O))) (or (or A E) (or I (or J K))) (or (or A E) (or I (or J L))) (or (or A E) (or I (or J M))) (or (or A E) (or I (or J N))) (or (or A E) (or I (or J O))) (or (or A E) (or I (or K L))) (or (or A E) (or I (or K M))) (or (or A E) (or I (or K N))) (or (or A E) (or I (or K O))) (or (or A E) (or I (or L M))) (or (or A E) (or I (or L N))) (or (or A E) (or I (or L O))) (or (or A E) (or I (or M N))) (or (or A E) (or I (or M O))) (or (or A E) (or I (or N O))) (or (or A E) (or J (or K L))) (or (or A E) (or J (or K M))) (or (or A E) (or J (or K N))) (or (or A E) (or J (or K O))) (or (or A E) (or J (or L M))) (or (or A E) (or J (or L N))) (or (or A E) (or J (or L O))) (or (or A E) (or J (or M N))) (or (or A E) (or J (or M O))) (or (or A E) (or J (or N O))) (or (or A E) (or K (or L M))) (or (or A E) (or K (or L N))) (or (or A E) (or K (or L O))) (or (or A E) (or K (or M N))) (or (or A E) (or K (or M O))) (or (or A E) (or K (or N O))) (or (or A E) (or L (or M N))) (or (or A E) (or L (or M O))) (or (or A E) (or L (or N O))) (or (or A E) (or M (or N O))) (or (or A F) (or G (or H I))) (or (or A F) (or G (or H J))) (or (or A F) (or G (or H K))) (or (or A F) (or G (or H L))) (or (or A F) (or G (or H M))) (or (or A F) (or G (or H N))) (or (or A F) (or G (or H O))) (or (or A F) (or G (or I J))) (or (or A F) (or G (or I K))) (or (or A F) (or G (or I L))) (or (or A F) (or G (or I M))) (or (or A F) (or G (or I N))) (or (or A F) (or G (or I O))) (or (or A F) (or G (or J K))) (or (or A F) (or G (or J L))) (or (or A F) (or G (or J M))) (or (or A F) (or G (or J N))) (or (or A F) (or G (or J O))) (or (or A F) (or G (or K L))) (or (or A F) (or G (or K M))) (or (or A F) (or G (or K N))) (or (or A F) (or G (or K O))) (or (or A F) (or G (or L M))) (or (or A F) (or G (or L N))) (or (or A F) (or G (or L O))) (or (or A F) (or G (or M N))) (or (or A F) (or G (or M O))) (or (or A F) (or G (or N O))) (or (or A F) (or H (or I J))) (or (or A F) (or H (or I K))) (or (or A F) (or H (or I L))) (or (or A F) (or H (or I M))) (or (or A F) (or H (or I N))) (or (or A F) (or H (or I O))) (or (or A F) (or H (or J K))) (or (or A F) (or H (or J L))) (or (or A F) (or H (or J M))) (or (or A F) (or H (or J N))) (or (or A F) (or H (or J O))) (or (or A F) (or H (or K L))) (or (or A F) (or H (or K M))) (or (or A F) (or H (or K N))) (or (or A F) (or H (or K O))) (or (or A F) (or H (or L M))) (or (or A F) (or H (or L N))) (or (or A F) (or H (or L O))) (or (or A F) (or H (or M N))) (or (or A F) (or H (or M O))) (or (or A F) (or H (or N O))) (or (or A F) (or I (or J K))) (or (or A F) (or I (or J L))) (or (or A F) (or I (or J M))) (or (or A F) (or I (or J N))) (or (or A F) (or I (or J O))) (or (or A F) (or I (or K L))) (or (or A F) (or I (or K M))) (or (or A F) (or I (or K N))) (or (or A F) (or I (or K O))) (or (or A F) (or I (or L M))) (or (or A F) (or I (or L N))) (or (or A F) (or I (or L O))) (or (or A F) (or I (or M N))) (or (or A F) (or I (or M O))) (or (or A F) (or I (or N O))) (or (or A F) (or J (or K L))) (or (or A F) (or J (or K M))) (or (or A F) (or J (or K N))) (or (or A F) (or J (or K O))) (or (or A F) (or J (or L M))) (or (or A F) (or J (or L N))) (or (or A F) (or J (or L O))) (or (or A F) (or J (or M N))) (or (or A F) (or J (or M O))) (or (or A F) (or J (or N O))) (or (or A F) (or K (or L M))) (or (or A F) (or K (or L N))) (or (or A F) (or K (or L O))) (or (or A F) (or K (or M N))) (or (or A F) (or K (or M O))) (or (or A F) (or K (or N O))) (or (or A F) (or L (or M N))) (or (or A F) (or L (or M O))) (or (or A F) (or L (or N O))) (or (or A F) (or M (or N O))) (or (or A G) (or H (or I J))) (or (or A G) (or H (or I K))) (or (or A G) (or H (or I L))) (or (or A G) (or H (or I M))) (or (or A G) (or H (or I N))) (or (or A G) (or H (or I O))) (or (or A G) (or H (or J K))) (or (or A G) (or H (or J L))) (or (or A G) (or H (or J M))) (or (or A G) (or H (or J N))) (or (or A G) (or H (or J O))) (or (or A G) (or H (or K L))) (or (or A G) (or H (or K M))) (or (or A G) (or H (or K N))) (or (or A G) (or H (or K O))) (or (or A G) (or H (or L M))) (or (or A G) (or H (or L N))) (or (or A G) (or H (or L O))) (or (or A G) (or H (or M N))) (or (or A G) (or H (or M O))) (or (or A G) (or H (or N O))) (or (or A G) (or I (or J K))) (or (or A G) (or I (or J L))) (or (or A G) (or I (or J M))) (or (or A G) (or I (or J N))) (or (or A G) (or I (or J O))) (or (or A G) (or I (or K L))) (or (or A G) (or I (or K M))) (or (or A G) (or I (or K N))) (or (or A G) (or I (or K O))) (or (or A G) (or I (or L M))) (or (or A G) (or I (or L N))) (or (or A G) (or I (or L O))) (or (or A G) (or I (or M N))) (or (or A G) (or I (or M O))) (or (or A G) (or I (or N O))) (or (or A G) (or J (or K L))) (or (or A G) (or J (or K M))) (or (or A G) (or J (or K N))) (or (or A G) (or J (or K O))) (or (or A G) (or J (or L M))) (or (or A G) (or J (or L N))) (or (or A G) (or J (or L O))) (or (or A G) (or J (or M N))) (or (or A G) (or J (or M O))) (or (or A G) (or J (or N O))) (or (or A G) (or K (or L M))) (or (or A G) (or K (or L N))) (or (or A G) (or K (or L O))) (or (or A G) (or K (or M N))) (or (or A G) (or K (or M O))) (or (or A G) (or K (or N O))) (or (or A G) (or L (or M N))) (or (or A G) (or L (or M O))) (or (or A G) (or L (or N O))) (or (or A G) (or M (or N O))) (or (or A H) (or I (or J K))) (or (or A H) (or I (or J L))) (or (or A H) (or I (or J M))) (or (or A H) (or I (or J N))) (or (or A H) (or I (or J O))) (or (or A H) (or I (or K L))) (or (or A H) (or I (or K M))) (or (or A H) (or I (or K N))) (or (or A H) (or I (or K O))) (or (or A H) (or I (or L M))) (or (or A H) (or I (or L N))) (or (or A H) (or I (or L O))) (or (or A H) (or I (or M N))) (or (or A H) (or I (or M O))) (or (or A H) (or I (or N O))) (or (or A H) (or J (or K L))) (or (or A H) (or J (or K M))) (or (or A H) (or J (or K N))) (or (or A H) (or J (or K O))) (or (or A H) (or J (or L M))) (or (or A H) (or J (or L N))) (or (or A H) (or J (or L O))) (or (or A H) (or J (or M N))) (or (or A H) (or J (or M O))) (or (or A H) (or J (or N O))) (or (or A H) (or K (or L M))) (or (or A H) (or K (or L N))) (or (or A H) (or K (or L O))) (or (or A H) (or K (or M N))) (or (or A H) (or K (or M O))) (or (or A H) (or K (or N O))) (or (or A H) (or L (or M N))) (or (or A H) (or L (or M O))) (or (or A H) (or L (or N O))) (or (or A H) (or M (or N O))) (or (or A I) (or J (or K L))) (or (or A I) (or J (or K M))) (or (or A I) (or J (or K N))) (or (or A I) (or J (or K O))) (or (or A I) (or J (or L M))) (or (or A I) (or J (or L N))) (or (or A I) (or J (or L O))) (or (or A I) (or J (or M N))) (or (or A I) (or J (or M O))) (or (or A I) (or J (or N O))) (or (or A I) (or K (or L M))) (or (or A I) (or K (or L N))) (or (or A I) (or K (or L O))) (or (or A I) (or K (or M N))) (or (or A I) (or K (or M O))) (or (or A I) (or K (or N O))) (or (or A I) (or L (or M N))) (or (or A I) (or L (or M O))) (or (or A I) (or L (or N O))) (or (or A I) (or M (or N O))) (or (or A J) (or K (or L M))) (or (or A J) (or K (or L N))) (or (or A J) (or K (or L O))) (or (or A J) (or K (or M N))) (or (or A J) (or K (or M O))) (or (or A J) (or K (or N O))) (or (or A J) (or L (or M N))) (or (or A J) (or L (or M O))) (or (or A J) (or L (or N O))) (or (or A J) (or M (or N O))) (or (or A K) (or L (or M N))) (or (or A K) (or L (or M O))) (or (or A K) (or L (or N O))) (or (or A K) (or M (or N O))) (or (or A L) (or M (or N O))) (or (or B C) (or D (or E F))) (or (or B C) (or D (or E G))) (or (or B C) (or D (or E H))) (or (or B C) (or D (or E I))) (or (or B C) (or D (or E J))) (or (or B C) (or D (or E K))) (or (or B C) (or D (or E L))) (or (or B C) (or D (or E M))) (or (or B C) (or D (or E N))) (or (or B C) (or D (or E O))) (or (or B C) (or D (or F G))) (or (or B C) (or D (or F H))) (or (or B C) (or D (or F I))) (or (or B C) (or D (or F J))) (or (or B C) (or D (or F K))) (or (or B C) (or D (or F L))) (or (or B C) (or D (or F M))) (or (or B C) (or D (or F N))) (or (or B C) (or D (or F O))) (or (or B C) (or D (or G H))) (or (or B C) (or D (or G I))) (or (or B C) (or D (or G J))) (or (or B C) (or D (or G K))) (or (or B C) (or D (or G L))) (or (or B C) (or D (or G M))) (or (or B C) (or D (or G N))) (or (or B C) (or D (or G O))) (or (or B C) (or D (or H I))) (or (or B C) (or D (or H J))) (or (or B C) (or D (or H K))) (or (or B C) (or D (or H L))) (or (or B C) (or D (or H M))) (or (or B C) (or D (or H N))) (or (or B C) (or D (or H O))) (or (or B C) (or D (or I J))) (or (or B C) (or D (or I K))) (or (or B C) (or D (or I L))) (or (or B C) (or D (or I M))) (or (or B C) (or D (or I N))) (or (or B C) (or D (or I O))) (or (or B C) (or D (or J K))) (or (or B C) (or D (or J L))) (or (or B C) (or D (or J M))) (or (or B C) (or D (or J N))) (or (or B C) (or D (or J O))) (or (or B C) (or D (or K L))) (or (or B C) (or D (or K M))) (or (or B C) (or D (or K N))) (or (or B C) (or D (or K O))) (or (or B C) (or D (or L M))) (or (or B C) (or D (or L N))) (or (or B C) (or D (or L O))) (or (or B C) (or D (or M N))) (or (or B C) (or D (or M O))) (or (or B C) (or D (or N O))) (or (or B C) (or E (or F G))) (or (or B C) (or E (or F H))) (or (or B C) (or E (or F I))) (or (or B C) (or E (or F J))) (or (or B C) (or E (or F K))) (or (or B C) (or E (or F L))) (or (or B C) (or E (or F M))) (or (or B C) (or E (or F N))) (or (or B C) (or E (or F O))) (or (or B C) (or E (or G H))) (or (or B C) (or E (or G I))) (or (or B C) (or E (or G J))) (or (or B C) (or E (or G K))) (or (or B C) (or E (or G L))) (or (or B C) (or E (or G M))) (or (or B C) (or E (or G N))) (or (or B C) (or E (or G O))) (or (or B C) (or E (or H I))) (or (or B C) (or E (or H J))) (or (or B C) (or E (or H K))) (or (or B C) (or E (or H L))) (or (or B C) (or E (or H M))) (or (or B C) (or E (or H N))) (or (or B C) (or E (or H O))) (or (or B C) (or E (or I J))) (or (or B C) (or E (or I K))) (or (or B C) (or E (or I L))) (or (or B C) (or E (or I M))) (or (or B C) (or E (or I N))) (or (or B C) (or E (or I O))) (or (or B C) (or E (or J K))) (or (or B C) (or E (or J L))) (or (or B C) (or E (or J M))) (or (or B C) (or E (or J N))) (or (or B C) (or E (or J O))) (or (or B C) (or E (or K L))) (or (or B C) (or E (or K M))) (or (or B C) (or E (or K N))) (or (or B C) (or E (or K O))) (or (or B C) (or E (or L M))) (or (or B C) (or E (or L N))) (or (or B C) (or E (or L O))) (or (or B C) (or E (or M N))) (or (or B C) (or E (or M O))) (or (or B C) (or E (or N O))) (or (or B C) (or F (or G H))) (or (or B C) (or F (or G I))) (or (or B C) (or F (or G J))) (or (or B C) (or F (or G K))) (or (or B C) (or F (or G L))) (or (or B C) (or F (or G M))) (or (or B C) (or F (or G N))) (or (or B C) (or F (or G O))) (or (or B C) (or F (or H I))) (or (or B C) (or F (or H J))) (or (or B C) (or F (or H K))) (or (or B C) (or F (or H L))) (or (or B C) (or F (or H M))) (or (or B C) (or F (or H N))) (or (or B C) (or F (or H O))) (or (or B C) (or F (or I J))) (or (or B C) (or F (or I K))) (or (or B C) (or F (or I L))) (or (or B C) (or F (or I M))) (or (or B C) (or F (or I N))) (or (or B C) (or F (or I O))) (or (or B C) (or F (or J K))) (or (or B C) (or F (or J L))) (or (or B C) (or F (or J M))) (or (or B C) (or F (or J N))) (or (or B C) (or F (or J O))) (or (or B C) (or F (or K L))) (or (or B C) (or F (or K M))) (or (or B C) (or F (or K N))) (or (or B C) (or F (or K O))) (or (or B C) (or F (or L M))) (or (or B C) (or F (or L N))) (or (or B C) (or F (or L O))) (or (or B C) (or F (or M N))) (or (or B C) (or F (or M O))) (or (or B C) (or F (or N O))) (or (or B C) (or G (or H I))) (or (or B C) (or G (or H J))) (or (or B C) (or G (or H K))) (or (or B C) (or G (or H L))) (or (or B C) (or G (or H M))) (or (or B C) (or G (or H N))) (or (or B C) (or G (or H O))) (or (or B C) (or G (or I J))) (or (or B C) (or G (or I K))) (or (or B C) (or G (or I L))) (or (or B C) (or G (or I M))) (or (or B C) (or G (or I N))) (or (or B C) (or G (or I O))) (or (or B C) (or G (or J K))) (or (or B C) (or G (or J L))) (or (or B C) (or G (or J M))) (or (or B C) (or G (or J N))) (or (or B C) (or G (or J O))) (or (or B C) (or G (or K L))) (or (or B C) (or G (or K M))) (or (or B C) (or G (or K N))) (or (or B C) (or G (or K O))) (or (or B C) (or G (or L M))) (or (or B C) (or G (or L N))) (or (or B C) (or G (or L O))) (or (or B C) (or G (or M N))) (or (or B C) (or G (or M O))) (or (or B C) (or G (or N O))) (or (or B C) (or H (or I J))) (or (or B C) (or H (or I K))) (or (or B C) (or H (or I L))) (or (or B C) (or H (or I M))) (or (or B C) (or H (or I N))) (or (or B C) (or H (or I O))) (or (or B C) (or H (or J K))) (or (or B C) (or H (or J L))) (or (or B C) (or H (or J M))) (or (or B C) (or H (or J N))) (or (or B C) (or H (or J O))) (or (or B C) (or H (or K L))) (or (or B C) (or H (or K M))) (or (or B C) (or H (or K N))) (or (or B C) (or H (or K O))) (or (or B C) (or H (or L M))) (or (or B C) (or H (or L N))) (or (or B C) (or H (or L O))) (or (or B C) (or H (or M N))) (or (or B C) (or H (or M O))) (or (or B C) (or H (or N O))) (or (or B C) (or I (or J K))) (or (or B C) (or I (or J L))) (or (or B C) (or I (or J M))) (or (or B C) (or I (or J N))) (or (or B C) (or I (or J O))) (or (or B C) (or I (or K L))) (or (or B C) (or I (or K M))) (or (or B C) (or I (or K N))) (or (or B C) (or I (or K O))) (or (or B C) (or I (or L M))) (or (or B C) (or I (or L N))) (or (or B C) (or I (or L O))) (or (or B C) (or I (or M N))) (or (or B C) (or I (or M O))) (or (or B C) (or I (or N O))) (or (or B C) (or J (or K L))) (or (or B C) (or J (or K M))) (or (or B C) (or J (or K N))) (or (or B C) (or J (or K O))) (or (or B C) (or J (or L M))) (or (or B C) (or J (or L N))) (or (or B C) (or J (or L O))) (or (or B C) (or J (or M N))) (or (or B C) (or J (or M O))) (or (or B C) (or J (or N O))) (or (or B C) (or K (or L M))) (or (or B C) (or K (or L N))) (or (or B C) (or K (or L O))) (or (or B C) (or K (or M N))) (or (or B C) (or K (or M O))) (or (or B C) (or K (or N O))) (or (or B C) (or L (or M N))) (or (or B C) (or L (or M O))) (or (or B C) (or L (or N O))) (or (or B C) (or M (or N O))) (or (or B D) (or E (or F G))) (or (or B D) (or E (or F H))) (or (or B D) (or E (or F I))) (or (or B D) (or E (or F J))) (or (or B D) (or E (or F K))) (or (or B D) (or E (or F L))) (or (or B D) (or E (or F M))) (or (or B D) (or E (or F N))) (or (or B D) (or E (or F O))) (or (or B D) (or E (or G H))) (or (or B D) (or E (or G I))) (or (or B D) (or E (or G J))) (or (or B D) (or E (or G K))) (or (or B D) (or E (or G L))) (or (or B D) (or E (or G M))) (or (or B D) (or E (or G N))) (or (or B D) (or E (or G O))) (or (or B D) (or E (or H I))) (or (or B D) (or E (or H J))) (or (or B D) (or E (or H K))) (or (or B D) (or E (or H L))) (or (or B D) (or E (or H M))) (or (or B D) (or E (or H N))) (or (or B D) (or E (or H O))) (or (or B D) (or E (or I J))) (or (or B D) (or E (or I K))) (or (or B D) (or E (or I L))) (or (or B D) (or E (or I M))) (or (or B D) (or E (or I N))) (or (or B D) (or E (or I O))) (or (or B D) (or E (or J K))) (or (or B D) (or E (or J L))) (or (or B D) (or E (or J M))) (or (or B D) (or E (or J N))) (or (or B D) (or E (or J O))) (or (or B D) (or E (or K L))) (or (or B D) (or E (or K M))) (or (or B D) (or E (or K N))) (or (or B D) (or E (or K O))) (or (or B D) (or E (or L M))) (or (or B D) (or E (or L N))) (or (or B D) (or E (or L O))) (or (or B D) (or E (or M N))) (or (or B D) (or E (or M O))) (or (or B D) (or E (or N O))) (or (or B D) (or F (or G H))) (or (or B D) (or F (or G I))) (or (or B D) (or F (or G J))) (or (or B D) (or F (or G K))) (or (or B D) (or F (or G L))) (or (or B D) (or F (or G M))) (or (or B D) (or F (or G N))) (or (or B D) (or F (or G O))) (or (or B D) (or F (or H I))) (or (or B D) (or F (or H J))) (or (or B D) (or F (or H K))) (or (or B D) (or F (or H L))) (or (or B D) (or F (or H M))) (or (or B D) (or F (or H N))) (or (or B D) (or F (or H O))) (or (or B D) (or F (or I J))) (or (or B D) (or F (or I K))) (or (or B D) (or F (or I L))) (or (or B D) (or F (or I M))) (or (or B D) (or F (or I N))) (or (or B D) (or F (or I O))) (or (or B D) (or F (or J K))) (or (or B D) (or F (or J L))) (or (or B D) (or F (or J M))) (or (or B D) (or F (or J N))) (or (or B D) (or F (or J O))) (or (or B D) (or F (or K L))) (or (or B D) (or F (or K M))) (or (or B D) (or F (or K N))) (or (or B D) (or F (or K O))) (or (or B D) (or F (or L M))) (or (or B D) (or F (or L N))) (or (or B D) (or F (or L O))) (or (or B D) (or F (or M N))) (or (or B D) (or F (or M O))) (or (or B D) (or F (or N O))) (or (or B D) (or G (or H I))) (or (or B D) (or G (or H J))) (or (or B D) (or G (or H K))) (or (or B D) (or G (or H L))) (or (or B D) (or G (or H M))) (or (or B D) (or G (or H N))) (or (or B D) (or G (or H O))) (or (or B D) (or G (or I J))) (or (or B D) (or G (or I K))) (or (or B D) (or G (or I L))) (or (or B D) (or G (or I M))) (or (or B D) (or G (or I N))) (or (or B D) (or G (or I O))) (or (or B D) (or G (or J K))) (or (or B D) (or G (or J L))) (or (or B D) (or G (or J M))) (or (or B D) (or G (or J N))) (or (or B D) (or G (or J O))) (or (or B D) (or G (or K L))) (or (or B D) (or G (or K M))) (or (or B D) (or G (or K N))) (or (or B D) (or G (or K O))) (or (or B D) (or G (or L M))) (or (or B D) (or G (or L N))) (or (or B D) (or G (or L O))) (or (or B D) (or G (or M N))) (or (or B D) (or G (or M O))) (or (or B D) (or G (or N O))) (or (or B D) (or H (or I J))) (or (or B D) (or H (or I K))) (or (or B D) (or H (or I L))) (or (or B D) (or H (or I M))) (or (or B D) (or H (or I N))) (or (or B D) (or H (or I O))) (or (or B D) (or H (or J K))) (or (or B D) (or H (or J L))) (or (or B D) (or H (or J M))) (or (or B D) (or H (or J N))) (or (or B D) (or H (or J O))) (or (or B D) (or H (or K L))) (or (or B D) (or H (or K M))) (or (or B D) (or H (or K N))) (or (or B D) (or H (or K O))) (or (or B D) (or H (or L M))) (or (or B D) (or H (or L N))) (or (or B D) (or H (or L O))) (or (or B D) (or H (or M N))) (or (or B D) (or H (or M O))) (or (or B D) (or H (or N O))) (or (or B D) (or I (or J K))) (or (or B D) (or I (or J L))) (or (or B D) (or I (or J M))) (or (or B D) (or I (or J N))) (or (or B D) (or I (or J O))) (or (or B D) (or I (or K L))) (or (or B D) (or I (or K M))) (or (or B D) (or I (or K N))) (or (or B D) (or I (or K O))) (or (or B D) (or I (or L M))) (or (or B D) (or I (or L N))) (or (or B D) (or I (or L O))) (or (or B D) (or I (or M N))) (or (or B D) (or I (or M O))) (or (or B D) (or I (or N O))) (or (or B D) (or J (or K L))) (or (or B D) (or J (or K M))) (or (or B D) (or J (or K N))) (or (or B D) (or J (or K O))) (or (or B D) (or J (or L M))) (or (or B D) (or J (or L N))) (or (or B D) (or J (or L O))) (or (or B D) (or J (or M N))) (or (or B D) (or J (or M O))) (or (or B D) (or J (or N O))) (or (or B D) (or K (or L M))) (or (or B D) (or K (or L N))) (or (or B D) (or K (or L O))) (or (or B D) (or K (or M N))) (or (or B D) (or K (or M O))) (or (or B D) (or K (or N O))) (or (or B D) (or L (or M N))) (or (or B D) (or L (or M O))) (or (or B D) (or L (or N O))) (or (or B D) (or M (or N O))) (or (or B E) (or F (or G H))) (or (or B E) (or F (or G I))) (or (or B E) (or F (or G J))) (or (or B E) (or F (or G K))) (or (or B E) (or F (or G L))) (or (or B E) (or F (or G M))) (or (or B E) (or F (or G N))) (or (or B E) (or F (or G O))) (or (or B E) (or F (or H I))) (or (or B E) (or F (or H J))) (or (or B E) (or F (or H K))) (or (or B E) (or F (or H L))) (or (or B E) (or F (or H M))) (or (or B E) (or F (or H N))) (or (or B E) (or F (or H O))) (or (or B E) (or F (or I J))) (or (or B E) (or F (or I K))) (or (or B E) (or F (or I L))) (or (or B E) (or F (or I M))) (or (or B E) (or F (or I N))) (or (or B E) (or F (or I O))) (or (or B E) (or F (or J K))) (or (or B E) (or F (or J L))) (or (or B E) (or F (or J M))) (or (or B E) (or F (or J N))) (or (or B E) (or F (or J O))) (or (or B E) (or F (or K L))) (or (or B E) (or F (or K M))) (or (or B E) (or F (or K N))) (or (or B E) (or F (or K O))) (or (or B E) (or F (or L M))) (or (or B E) (or F (or L N))) (or (or B E) (or F (or L O))) (or (or B E) (or F (or M N))) (or (or B E) (or F (or M O))) (or (or B E) (or F (or N O))) (or (or B E) (or G (or H I))) (or (or B E) (or G (or H J))) (or (or B E) (or G (or H K))) (or (or B E) (or G (or H L))) (or (or B E) (or G (or H M))) (or (or B E) (or G (or H N))) (or (or B E) (or G (or H O))) (or (or B E) (or G (or I J))) (or (or B E) (or G (or I K))) (or (or B E) (or G (or I L))) (or (or B E) (or G (or I M))) (or (or B E) (or G (or I N))) (or (or B E) (or G (or I O))) (or (or B E) (or G (or J K))) (or (or B E) (or G (or J L))) (or (or B E) (or G (or J M))) (or (or B E) (or G (or J N))) (or (or B E) (or G (or J O))) (or (or B E) (or G (or K L))) (or (or B E) (or G (or K M))) (or (or B E) (or G (or K N))) (or (or B E) (or G (or K O))) (or (or B E) (or G (or L M))) (or (or B E) (or G (or L N))) (or (or B E) (or G (or L O))) (or (or B E) (or G (or M N))) (or (or B E) (or G (or M O))) (or (or B E) (or G (or N O))) (or (or B E) (or H (or I J))) (or (or B E) (or H (or I K))) (or (or B E) (or H (or I L))) (or (or B E) (or H (or I M))) (or (or B E) (or H (or I N))) (or (or B E) (or H (or I O))) (or (or B E) (or H (or J K))) (or (or B E) (or H (or J L))) (or (or B E) (or H (or J M))) (or (or B E) (or H (or J N))) (or (or B E) (or H (or J O))) (or (or B E) (or H (or K L))) (or (or B E) (or H (or K M))) (or (or B E) (or H (or K N))) (or (or B E) (or H (or K O))) (or (or B E) (or H (or L M))) (or (or B E) (or H (or L N))) (or (or B E) (or H (or L O))) (or (or B E) (or H (or M N))) (or (or B E) (or H (or M O))) (or (or B E) (or H (or N O))) (or (or B E) (or I (or J K))) (or (or B E) (or I (or J L))) (or (or B E) (or I (or J M))) (or (or B E) (or I (or J N))) (or (or B E) (or I (or J O))) (or (or B E) (or I (or K L))) (or (or B E) (or I (or K M))) (or (or B E) (or I (or K N))) (or (or B E) (or I (or K O))) (or (or B E) (or I (or L M))) (or (or B E) (or I (or L N))) (or (or B E) (or I (or L O))) (or (or B E) (or I (or M N))) (or (or B E) (or I (or M O))) (or (or B E) (or I (or N O))) (or (or B E) (or J (or K L))) (or (or B E) (or J (or K M))) (or (or B E) (or J (or K N))) (or (or B E) (or J (or K O))) (or (or B E) (or J (or L M))) (or (or B E) (or J (or L N))) (or (or B E) (or J (or L O))) (or (or B E) (or J (or M N))) (or (or B E) (or J (or M O))) (or (or B E) (or J (or N O))) (or (or B E) (or K (or L M))) (or (or B E) (or K (or L N))) (or (or B E) (or K (or L O))) (or (or B E) (or K (or M N))) (or (or B E) (or K (or M O))) (or (or B E) (or K (or N O))) (or (or B E) (or L (or M N))) (or (or B E) (or L (or M O))) (or (or B E) (or L (or N O))) (or (or B E) (or M (or N O))) (or (or B F) (or G (or H I))) (or (or B F) (or G (or H J))) (or (or B F) (or G (or H K))) (or (or B F) (or G (or H L))) (or (or B F) (or G (or H M))) (or (or B F) (or G (or H N))) (or (or B F) (or G (or H O))) (or (or B F) (or G (or I J))) (or (or B F) (or G (or I K))) (or (or B F) (or G (or I L))) (or (or B F) (or G (or I M))) (or (or B F) (or G (or I N))) (or (or B F) (or G (or I O))) (or (or B F) (or G (or J K))) (or (or B F) (or G (or J L))) (or (or B F) (or G (or J M))) (or (or B F) (or G (or J N))) (or (or B F) (or G (or J O))) (or (or B F) (or G (or K L))) (or (or B F) (or G (or K M))) (or (or B F) (or G (or K N))) (or (or B F) (or G (or K O))) (or (or B F) (or G (or L M))) (or (or B F) (or G (or L N))) (or (or B F) (or G (or L O))) (or (or B F) (or G (or M N))) (or (or B F) (or G (or M O))) (or (or B F) (or G (or N O))) (or (or B F) (or H (or I J))) (or (or B F) (or H (or I K))) (or (or B F) (or H (or I L))) (or (or B F) (or H (or I M))) (or (or B F) (or H (or I N))) (or (or B F) (or H (or I O))) (or (or B F) (or H (or J K))) (or (or B F) (or H (or J L))) (or (or B F) (or H (or J M))) (or (or B F) (or H (or J N))) (or (or B F) (or H (or J O))) (or (or B F) (or H (or K L))) (or (or B F) (or H (or K M))) (or (or B F) (or H (or K N))) (or (or B F) (or H (or K O))) (or (or B F) (or H (or L M))) (or (or B F) (or H (or L N))) (or (or B F) (or H (or L O))) (or (or B F) (or H (or M N))) (or (or B F) (or H (or M O))) (or (or B F) (or H (or N O))) (or (or B F) (or I (or J K))) (or (or B F) (or I (or J L))) (or (or B F) (or I (or J M))) (or (or B F) (or I (or J N))) (or (or B F) (or I (or J O))) (or (or B F) (or I (or K L))) (or (or B F) (or I (or K M))) (or (or B F) (or I (or K N))) (or (or B F) (or I (or K O))) (or (or B F) (or I (or L M))) (or (or B F) (or I (or L N))) (or (or B F) (or I (or L O))) (or (or B F) (or I (or M N))) (or (or B F) (or I (or M O))) (or (or B F) (or I (or N O))) (or (or B F) (or J (or K L))) (or (or B F) (or J (or K M))) (or (or B F) (or J (or K N))) (or (or B F) (or J (or K O))) (or (or B F) (or J (or L M))) (or (or B F) (or J (or L N))) (or (or B F) (or J (or L O))) (or (or B F) (or J (or M N))) (or (or B F) (or J (or M O))) (or (or B F) (or J (or N O))) (or (or B F) (or K (or L M))) (or (or B F) (or K (or L N))) (or (or B F) (or K (or L O))) (or (or B F) (or K (or M N))) (or (or B F) (or K (or M O))) (or (or B F) (or K (or N O))) (or (or B F) (or L (or M N))) (or (or B F) (or L (or M O))) (or (or B F) (or L (or N O))) (or (or B F) (or M (or N O))) (or (or B G) (or H (or I J))) (or (or B G) (or H (or I K))) (or (or B G) (or H (or I L))) (or (or B G) (or H (or I M))) (or (or B G) (or H (or I N))) (or (or B G) (or H (or I O))) (or (or B G) (or H (or J K))) (or (or B G) (or H (or J L))) (or (or B G) (or H (or J M))) (or (or B G) (or H (or J N))) (or (or B G) (or H (or J O))) (or (or B G) (or H (or K L))) (or (or B G) (or H (or K M))) (or (or B G) (or H (or K N))) (or (or B G) (or H (or K O))) (or (or B G) (or H (or L M))) (or (or B G) (or H (or L N))) (or (or B G) (or H (or L O))) (or (or B G) (or H (or M N))) (or (or B G) (or H (or M O))) (or (or B G) (or H (or N O))) (or (or B G) (or I (or J K))) (or (or B G) (or I (or J L))) (or (or B G) (or I (or J M))) (or (or B G) (or I (or J N))) (or (or B G) (or I (or J O))) (or (or B G) (or I (or K L))) (or (or B G) (or I (or K M))) (or (or B G) (or I (or K N))) (or (or B G) (or I (or K O))) (or (or B G) (or I (or L M))) (or (or B G) (or I (or L N))) (or (or B G) (or I (or L O))) (or (or B G) (or I (or M N))) (or (or B G) (or I (or M O))) (or (or B G) (or I (or N O))) (or (or B G) (or J (or K L))) (or (or B G) (or J (or K M))) (or (or B G) (or J (or K N))) (or (or B G) (or J (or K O))) (or (or B G) (or J (or L M))) (or (or B G) (or J (or L N))) (or (or B G) (or J (or L O))) (or (or B G) (or J (or M N))) (or (or B G) (or J (or M O))) (or (or B G) (or J (or N O))) (or (or B G) (or K (or L M))) (or (or B G) (or K (or L N))) (or (or B G) (or K (or L O))) (or (or B G) (or K (or M N))) (or (or B G) (or K (or M O))) (or (or B G) (or K (or N O))) (or (or B G) (or L (or M N))) (or (or B G) (or L (or M O))) (or (or B G) (or L (or N O))) (or (or B G) (or M (or N O))) (or (or B H) (or I (or J K))) (or (or B H) (or I (or J L))) (or (or B H) (or I (or J M))) (or (or B H) (or I (or J N))) (or (or B H) (or I (or J O))) (or (or B H) (or I (or K L))) (or (or B H) (or I (or K M))) (or (or B H) (or I (or K N))) (or (or B H) (or I (or K O))) (or (or B H) (or I (or L M))) (or (or B H) (or I (or L N))) (or (or B H) (or I (or L O))) (or (or B H) (or I (or M N))) (or (or B H) (or I (or M O))) (or (or B H) (or I (or N O))) (or (or B H) (or J (or K L))) (or (or B H) (or J (or K M))) (or (or B H) (or J (or K N))) (or (or B H) (or J (or K O))) (or (or B H) (or J (or L M))) (or (or B H) (or J (or L N))) (or (or B H) (or J (or L O))) (or (or B H) (or J (or M N))) (or (or B H) (or J (or M O))) (or (or B H) (or J (or N O))) (or (or B H) (or K (or L M))) (or (or B H) (or K (or L N))) (or (or B H) (or K (or L O))) (or (or B H) (or K (or M N))) (or (or B H) (or K (or M O))) (or (or B H) (or K (or N O))) (or (or B H) (or L (or M N))) (or (or B H) (or L (or M O))) (or (or B H) (or L (or N O))) (or (or B H) (or M (or N O))) (or (or B I) (or J (or K L))) (or (or B I) (or J (or K M))) (or (or B I) (or J (or K N))) (or (or B I) (or J (or K O))) (or (or B I) (or J (or L M))) (or (or B I) (or J (or L N))) (or (or B I) (or J (or L O))) (or (or B I) (or J (or M N))) (or (or B I) (or J (or M O))) (or (or B I) (or J (or N O))) (or (or B I) (or K (or L M))) (or (or B I) (or K (or L N))) (or (or B I) (or K (or L O))) (or (or B I) (or K (or M N))) (or (or B I) (or K (or M O))) (or (or B I) (or K (or N O))) (or (or B I) (or L (or M N))) (or (or B I) (or L (or M O))) (or (or B I) (or L (or N O))) (or (or B I) (or M (or N O))) (or (or B J) (or K (or L M))) (or (or B J) (or K (or L N))) (or (or B J) (or K (or L O))) (or (or B J) (or K (or M N))) (or (or B J) (or K (or M O))) (or (or B J) (or K (or N O))) (or (or B J) (or L (or M N))) (or (or B J) (or L (or M O))) (or (or B J) (or L (or N O))) (or (or B J) (or M (or N O))) (or (or B K) (or L (or M N))) (or (or B K) (or L (or M O))) (or (or B K) (or L (or N O))) (or (or B K) (or M (or N O))) (or (or B L) (or M (or N O))) (or (or C D) (or E (or F G))) (or (or C D) (or E (or F H))) (or (or C D) (or E (or F I))) (or (or C D) (or E (or F J))) (or (or C D) (or E (or F K))) (or (or C D) (or E (or F L))) (or (or C D) (or E (or F M))) (or (or C D) (or E (or F N))) (or (or C D) (or E (or F O))) (or (or C D) (or E (or G H))) (or (or C D) (or E (or G I))) (or (or C D) (or E (or G J))) (or (or C D) (or E (or G K))) (or (or C D) (or E (or G L))) (or (or C D) (or E (or G M))) (or (or C D) (or E (or G N))) (or (or C D) (or E (or G O))) (or (or C D) (or E (or H I))) (or (or C D) (or E (or H J))) (or (or C D) (or E (or H K))) (or (or C D) (or E (or H L))) (or (or C D) (or E (or H M))) (or (or C D) (or E (or H N))) (or (or C D) (or E (or H O))) (or (or C D) (or E (or I J))) (or (or C D) (or E (or I K))) (or (or C D) (or E (or I L))) (or (or C D) (or E (or I M))) (or (or C D) (or E (or I N))) (or (or C D) (or E (or I O))) (or (or C D) (or E (or J K))) (or (or C D) (or E (or J L))) (or (or C D) (or E (or J M))) (or (or C D) (or E (or J N))) (or (or C D) (or E (or J O))) (or (or C D) (or E (or K L))) (or (or C D) (or E (or K M))) (or (or C D) (or E (or K N))) (or (or C D) (or E (or K O))) (or (or C D) (or E (or L M))) (or (or C D) (or E (or L N))) (or (or C D) (or E (or L O))) (or (or C D) (or E (or M N))) (or (or C D) (or E (or M O))) (or (or C D) (or E (or N O))) (or (or C D) (or F (or G H))) (or (or C D) (or F (or G I))) (or (or C D) (or F (or G J))) (or (or C D) (or F (or G K))) (or (or C D) (or F (or G L))) (or (or C D) (or F (or G M))) (or (or C D) (or F (or G N))) (or (or C D) (or F (or G O))) (or (or C D) (or F (or H I))) (or (or C D) (or F (or H J))) (or (or C D) (or F (or H K))) (or (or C D) (or F (or H L))) (or (or C D) (or F (or H M))) (or (or C D) (or F (or H N))) (or (or C D) (or F (or H O))) (or (or C D) (or F (or I J))) (or (or C D) (or F (or I K))) (or (or C D) (or F (or I L))) (or (or C D) (or F (or I M))) (or (or C D) (or F (or I N))) (or (or C D) (or F (or I O))) (or (or C D) (or F (or J K))) (or (or C D) (or F (or J L))) (or (or C D) (or F (or J M))) (or (or C D) (or F (or J N))) (or (or C D) (or F (or J O))) (or (or C D) (or F (or K L))) (or (or C D) (or F (or K M))) (or (or C D) (or F (or K N))) (or (or C D) (or F (or K O))) (or (or C D) (or F (or L M))) (or (or C D) (or F (or L N))) (or (or C D) (or F (or L O))) (or (or C D) (or F (or M N))) (or (or C D) (or F (or M O))) (or (or C D) (or F (or N O))) (or (or C D) (or G (or H I))) (or (or C D) (or G (or H J))) (or (or C D) (or G (or H K))) (or (or C D) (or G (or H L))) (or (or C D) (or G (or H M))) (or (or C D) (or G (or H N))) (or (or C D) (or G (or H O))) (or (or C D) (or G (or I J))) (or (or C D) (or G (or I K))) (or (or C D) (or G (or I L))) (or (or C D) (or G (or I M))) (or (or C D) (or G (or I N))) (or (or C D) (or G (or I O))) (or (or C D) (or G (or J K))) (or (or C D) (or G (or J L))) (or (or C D) (or G (or J M))) (or (or C D) (or G (or J N))) (or (or C D) (or G (or J O))) (or (or C D) (or G (or K L))) (or (or C D) (or G (or K M))) (or (or C D) (or G (or K N))) (or (or C D) (or G (or K O))) (or (or C D) (or G (or L M))) (or (or C D) (or G (or L N))) (or (or C D) (or G (or L O))) (or (or C D) (or G (or M N))) (or (or C D) (or G (or M O))) (or (or C D) (or G (or N O))) (or (or C D) (or H (or I J))) (or (or C D) (or H (or I K))) (or (or C D) (or H (or I L))) (or (or C D) (or H (or I M))) (or (or C D) (or H (or I N))) (or (or C D) (or H (or I O))) (or (or C D) (or H (or J K))) (or (or C D) (or H (or J L))) (or (or C D) (or H (or J M))) (or (or C D) (or H (or J N))) (or (or C D) (or H (or J O))) (or (or C D) (or H (or K L))) (or (or C D) (or H (or K M))) (or (or C D) (or H (or K N))) (or (or C D) (or H (or K O))) (or (or C D) (or H (or L M))) (or (or C D) (or H (or L N))) (or (or C D) (or H (or L O))) (or (or C D) (or H (or M N))) (or (or C D) (or H (or M O))) (or (or C D) (or H (or N O))) (or (or C D) (or I (or J K))) (or (or C D) (or I (or J L))) (or (or C D) (or I (or J M))) (or (or C D) (or I (or J N))) (or (or C D) (or I (or J O))) (or (or C D) (or I (or K L))) (or (or C D) (or I (or K M))) (or (or C D) (or I (or K N))) (or (or C D) (or I (or K O))) (or (or C D) (or I (or L M))) (or (or C D) (or I (or L N))) (or (or C D) (or I (or L O))) (or (or C D) (or I (or M N))) (or (or C D) (or I (or M O))) (or (or C D) (or I (or N O))) (or (or C D) (or J (or K L))) (or (or C D) (or J (or K M))) (or (or C D) (or J (or K N))) (or (or C D) (or J (or K O))) (or (or C D) (or J (or L M))) (or (or C D) (or J (or L N))) (or (or C D) (or J (or L O))) (or (or C D) (or J (or M N))) (or (or C D) (or J (or M O))) (or (or C D) (or J (or N O))) (or (or C D) (or K (or L M))) (or (or C D) (or K (or L N))) (or (or C D) (or K (or L O))) (or (or C D) (or K (or M N))) (or (or C D) (or K (or M O))) (or (or C D) (or K (or N O))) (or (or C D) (or L (or M N))) (or (or C D) (or L (or M O))) (or (or C D) (or L (or N O))) (or (or C D) (or M (or N O))) (or (or C E) (or F (or G H))) (or (or C E) (or F (or G I))) (or (or C E) (or F (or G J))) (or (or C E) (or F (or G K))) (or (or C E) (or F (or G L))) (or (or C E) (or F (or G M))) (or (or C E) (or F (or G N))) (or (or C E) (or F (or G O))) (or (or C E) (or F (or H I))) (or (or C E) (or F (or H J))) (or (or C E) (or F (or H K))) (or (or C E) (or F (or H L))) (or (or C E) (or F (or H M))) (or (or C E) (or F (or H N))) (or (or C E) (or F (or H O))) (or (or C E) (or F (or I J))) (or (or C E) (or F (or I K))) (or (or C E) (or F (or I L))) (or (or C E) (or F (or I M))) (or (or C E) (or F (or I N))) (or (or C E) (or F (or I O))) (or (or C E) (or F (or J K))) (or (or C E) (or F (or J L))) (or (or C E) (or F (or J M))) (or (or C E) (or F (or J N))) (or (or C E) (or F (or J O))) (or (or C E) (or F (or K L))) (or (or C E) (or F (or K M))) (or (or C E) (or F (or K N))) (or (or C E) (or F (or K O))) (or (or C E) (or F (or L M))) (or (or C E) (or F (or L N))) (or (or C E) (or F (or L O))) (or (or C E) (or F (or M N))) (or (or C E) (or F (or M O))) (or (or C E) (or F (or N O))) (or (or C E) (or G (or H I))) (or (or C E) (or G (or H J))) (or (or C E) (or G (or H K))) (or (or C E) (or G (or H L))) (or (or C E) (or G (or H M))) (or (or C E) (or G (or H N))) (or (or C E) (or G (or H O))) (or (or C E) (or G (or I J))) (or (or C E) (or G (or I K))) (or (or C E) (or G (or I L))) (or (or C E) (or G (or I M))) (or (or C E) (or G (or I N))) (or (or C E) (or G (or I O))) (or (or C E) (or G (or J K))) (or (or C E) (or G (or J L))) (or (or C E) (or G (or J M))) (or (or C E) (or G (or J N))) (or (or C E) (or G (or J O))) (or (or C E) (or G (or K L))) (or (or C E) (or G (or K M))) (or (or C E) (or G (or K N))) (or (or C E) (or G (or K O))) (or (or C E) (or G (or L M))) (or (or C E) (or G (or L N))) (or (or C E) (or G (or L O))) (or (or C E) (or G (or M N))) (or (or C E) (or G (or M O))) (or (or C E) (or G (or N O))) (or (or C E) (or H (or I J))) (or (or C E) (or H (or I K))) (or (or C E) (or H (or I L))) (or (or C E) (or H (or I M))) (or (or C E) (or H (or I N))) (or (or C E) (or H (or I O))) (or (or C E) (or H (or J K))) (or (or C E) (or H (or J L))) (or (or C E) (or H (or J M))) (or (or C E) (or H (or J N))) (or (or C E) (or H (or J O))) (or (or C E) (or H (or K L))) (or (or C E) (or H (or K M))) (or (or C E) (or H (or K N))) (or (or C E) (or H (or K O))) (or (or C E) (or H (or L M))) (or (or C E) (or H (or L N))) (or (or C E) (or H (or L O))) (or (or C E) (or H (or M N))) (or (or C E) (or H (or M O))) (or (or C E) (or H (or N O))) (or (or C E) (or I (or J K))) (or (or C E) (or I (or J L))) (or (or C E) (or I (or J M))) (or (or C E) (or I (or J N))) (or (or C E) (or I (or J O))) (or (or C E) (or I (or K L))) (or (or C E) (or I (or K M))) (or (or C E) (or I (or K N))) (or (or C E) (or I (or K O))) (or (or C E) (or I (or L M))) (or (or C E) (or I (or L N))) (or (or C E) (or I (or L O))) (or (or C E) (or I (or M N))) (or (or C E) (or I (or M O))) (or (or C E) (or I (or N O))) (or (or C E) (or J (or K L))) (or (or C E) (or J (or K M))) (or (or C E) (or J (or K N))) (or (or C E) (or J (or K O))) (or (or C E) (or J (or L M))) (or (or C E) (or J (or L N))) (or (or C E) (or J (or L O))) (or (or C E) (or J (or M N))) (or (or C E) (or J (or M O))) (or (or C E) (or J (or N O))) (or (or C E) (or K (or L M))) (or (or C E) (or K (or L N))) (or (or C E) (or K (or L O))) (or (or C E) (or K (or M N))) (or (or C E) (or K (or M O))) (or (or C E) (or K (or N O))) (or (or C E) (or L (or M N))) (or (or C E) (or L (or M O))) (or (or C E) (or L (or N O))) (or (or C E) (or M (or N O))) (or (or C F) (or G (or H I))) (or (or C F) (or G (or H J))) (or (or C F) (or G (or H K))) (or (or C F) (or G (or H L))) (or (or C F) (or G (or H M))) (or (or C F) (or G (or H N))) (or (or C F) (or G (or H O))) (or (or C F) (or G (or I J))) (or (or C F) (or G (or I K))) (or (or C F) (or G (or I L))) (or (or C F) (or G (or I M))) (or (or C F) (or G (or I N))) (or (or C F) (or G (or I O))) (or (or C F) (or G (or J K))) (or (or C F) (or G (or J L))) (or (or C F) (or G (or J M))) (or (or C F) (or G (or J N))) (or (or C F) (or G (or J O))) (or (or C F) (or G (or K L))) (or (or C F) (or G (or K M))) (or (or C F) (or G (or K N))) (or (or C F) (or G (or K O))) (or (or C F) (or G (or L M))) (or (or C F) (or G (or L N))) (or (or C F) (or G (or L O))) (or (or C F) (or G (or M N))) (or (or C F) (or G (or M O))) (or (or C F) (or G (or N O))) (or (or C F) (or H (or I J))) (or (or C F) (or H (or I K))) (or (or C F) (or H (or I L))) (or (or C F) (or H (or I M))) (or (or C F) (or H (or I N))) (or (or C F) (or H (or I O))) (or (or C F) (or H (or J K))) (or (or C F) (or H (or J L))) (or (or C F) (or H (or J M))) (or (or C F) (or H (or J N))) (or (or C F) (or H (or J O))) (or (or C F) (or H (or K L))) (or (or C F) (or H (or K M))) (or (or C F) (or H (or K N))) (or (or C F) (or H (or K O))) (or (or C F) (or H (or L M))) (or (or C F) (or H (or L N))) (or (or C F) (or H (or L O))) (or (or C F) (or H (or M N))) (or (or C F) (or H (or M O))) (or (or C F) (or H (or N O))) (or (or C F) (or I (or J K))) (or (or C F) (or I (or J L))) (or (or C F) (or I (or J M))) (or (or C F) (or I (or J N))) (or (or C F) (or I (or J O))) (or (or C F) (or I (or K L))) (or (or C F) (or I (or K M))) (or (or C F) (or I (or K N))) (or (or C F) (or I (or K O))) (or (or C F) (or I (or L M))) (or (or C F) (or I (or L N))) (or (or C F) (or I (or L O))) (or (or C F) (or I (or M N))) (or (or C F) (or I (or M O))) (or (or C F) (or I (or N O))) (or (or C F) (or J (or K L))) (or (or C F) (or J (or K M))) (or (or C F) (or J (or K N))) (or (or C F) (or J (or K O))) (or (or C F) (or J (or L M))) (or (or C F) (or J (or L N))) (or (or C F) (or J (or L O))) (or (or C F) (or J (or M N))) (or (or C F) (or J (or M O))) (or (or C F) (or J (or N O))) (or (or C F) (or K (or L M))) (or (or C F) (or K (or L N))) (or (or C F) (or K (or L O))) (or (or C F) (or K (or M N))) (or (or C F) (or K (or M O))) (or (or C F) (or K (or N O))) (or (or C F) (or L (or M N))) (or (or C F) (or L (or M O))) (or (or C F) (or L (or N O))) (or (or C F) (or M (or N O))) (or (or C G) (or H (or I J))) (or (or C G) (or H (or I K))) (or (or C G) (or H (or I L))) (or (or C G) (or H (or I M))) (or (or C G) (or H (or I N))) (or (or C G) (or H (or I O))) (or (or C G) (or H (or J K))) (or (or C G) (or H (or J L))) (or (or C G) (or H (or J M))) (or (or C G) (or H (or J N))) (or (or C G) (or H (or J O))) (or (or C G) (or H (or K L))) (or (or C G) (or H (or K M))) (or (or C G) (or H (or K N))) (or (or C G) (or H (or K O))) (or (or C G) (or H (or L M))) (or (or C G) (or H (or L N))) (or (or C G) (or H (or L O))) (or (or C G) (or H (or M N))) (or (or C G) (or H (or M O))) (or (or C G) (or H (or N O))) (or (or C G) (or I (or J K))) (or (or C G) (or I (or J L))) (or (or C G) (or I (or J M))) (or (or C G) (or I (or J N))) (or (or C G) (or I (or J O))) (or (or C G) (or I (or K L))) (or (or C G) (or I (or K M))) (or (or C G) (or I (or K N))) (or (or C G) (or I (or K O))) (or (or C G) (or I (or L M))) (or (or C G) (or I (or L N))) (or (or C G) (or I (or L O))) (or (or C G) (or I (or M N))) (or (or C G) (or I (or M O))) (or (or C G) (or I (or N O))) (or (or C G) (or J (or K L))) (or (or C G) (or J (or K M))) (or (or C G) (or J (or K N))) (or (or C G) (or J (or K O))) (or (or C G) (or J (or L M))) (or (or C G) (or J (or L N))) (or (or C G) (or J (or L O))) (or (or C G) (or J (or M N))) (or (or C G) (or J (or M O))) (or (or C G) (or J (or N O))) (or (or C G) (or K (or L M))) (or (or C G) (or K (or L N))) (or (or C G) (or K (or L O))) (or (or C G) (or K (or M N))) (or (or C G) (or K (or M O))) (or (or C G) (or K (or N O))) (or (or C G) (or L (or M N))) (or (or C G) (or L (or M O))) (or (or C G) (or L (or N O))) (or (or C G) (or M (or N O))) (or (or C H) (or I (or J K))) (or (or C H) (or I (or J L))) (or (or C H) (or I (or J M))) (or (or C H) (or I (or J N))) (or (or C H) (or I (or J O))) (or (or C H) (or I (or K L))) (or (or C H) (or I (or K M))) (or (or C H) (or I (or K N))) (or (or C H) (or I (or K O))) (or (or C H) (or I (or L M))) (or (or C H) (or I (or L N))) (or (or C H) (or I (or L O))) (or (or C H) (or I (or M N))) (or (or C H) (or I (or M O))) (or (or C H) (or I (or N O))) (or (or C H) (or J (or K L))) (or (or C H) (or J (or K M))) (or (or C H) (or J (or K N))) (or (or C H) (or J (or K O))) (or (or C H) (or J (or L M))) (or (or C H) (or J (or L N))) (or (or C H) (or J (or L O))) (or (or C H) (or J (or M N))) (or (or C H) (or J (or M O))) (or (or C H) (or J (or N O))) (or (or C H) (or K (or L M))) (or (or C H) (or K (or L N))) (or (or C H) (or K (or L O))) (or (or C H) (or K (or M N))) (or (or C H) (or K (or M O))) (or (or C H) (or K (or N O))) (or (or C H) (or L (or M N))) (or (or C H) (or L (or M O))) (or (or C H) (or L (or N O))) (or (or C H) (or M (or N O))) (or (or C I) (or J (or K L))) (or (or C I) (or J (or K M))) (or (or C I) (or J (or K N))) (or (or C I) (or J (or K O))) (or (or C I) (or J (or L M))) (or (or C I) (or J (or L N))) (or (or C I) (or J (or L O))) (or (or C I) (or J (or M N))) (or (or C I) (or J (or M O))) (or (or C I) (or J (or N O))) (or (or C I) (or K (or L M))) (or (or C I) (or K (or L N))) (or (or C I) (or K (or L O))) (or (or C I) (or K (or M N))) (or (or C I) (or K (or M O))) (or (or C I) (or K (or N O))) (or (or C I) (or L (or M N))) (or (or C I) (or L (or M O))) (or (or C I) (or L (or N O))) (or (or C I) (or M (or N O))) (or (or C J) (or K (or L M))) (or (or C J) (or K (or L N))) (or (or C J) (or K (or L O))) (or (or C J) (or K (or M N))) (or (or C J) (or K (or M O))) (or (or C J) (or K (or N O))) (or (or C J) (or L (or M N))) (or (or C J) (or L (or M O))) (or (or C J) (or L (or N O))) (or (or C J) (or M (or N O))) (or (or C K) (or L (or M N))) (or (or C K) (or L (or M O))) (or (or C K) (or L (or N O))) (or (or C K) (or M (or N O))) (or (or C L) (or M (or N O))) (or (or D E) (or F (or G H))) (or (or D E) (or F (or G I))) (or (or D E) (or F (or G J))) (or (or D E) (or F (or G K))) (or (or D E) (or F (or G L))) (or (or D E) (or F (or G M))) (or (or D E) (or F (or G N))) (or (or D E) (or F (or G O))) (or (or D E) (or F (or H I))) (or (or D E) (or F (or H J))) (or (or D E) (or F (or H K))) (or (or D E) (or F (or H L))) (or (or D E) (or F (or H M))) (or (or D E) (or F (or H N))) (or (or D E) (or F (or H O))) (or (or D E) (or F (or I J))) (or (or D E) (or F (or I K))) (or (or D E) (or F (or I L))) (or (or D E) (or F (or I M))) (or (or D E) (or F (or I N))) (or (or D E) (or F (or I O))) (or (or D E) (or F (or J K))) (or (or D E) (or F (or J L))) (or (or D E) (or F (or J M))) (or (or D E) (or F (or J N))) (or (or D E) (or F (or J O))) (or (or D E) (or F (or K L))) (or (or D E) (or F (or K M))) (or (or D E) (or F (or K N))) (or (or D E) (or F (or K O))) (or (or D E) (or F (or L M))) (or (or D E) (or F (or L N))) (or (or D E) (or F (or L O))) (or (or D E) (or F (or M N))) (or (or D E) (or F (or M O))) (or (or D E) (or F (or N O))) (or (or D E) (or G (or H I))) (or (or D E) (or G (or H J))) (or (or D E) (or G (or H K))) (or (or D E) (or G (or H L))) (or (or D E) (or G (or H M))) (or (or D E) (or G (or H N))) (or (or D E) (or G (or H O))) (or (or D E) (or G (or I J))) (or (or D E) (or G (or I K))) (or (or D E) (or G (or I L))) (or (or D E) (or G (or I M))) (or (or D E) (or G (or I N))) (or (or D E) (or G (or I O))) (or (or D E) (or G (or J K))) (or (or D E) (or G (or J L))) (or (or D E) (or G (or J M))) (or (or D E) (or G (or J N))) (or (or D E) (or G (or J O))) (or (or D E) (or G (or K L))) (or (or D E) (or G (or K M))) (or (or D E) (or G (or K N))) (or (or D E) (or G (or K O))) (or (or D E) (or G (or L M))) (or (or D E) (or G (or L N))) (or (or D E) (or G (or L O))) (or (or D E) (or G (or M N))) (or (or D E) (or G (or M O))) (or (or D E) (or G (or N O))) (or (or D E) (or H (or I J))) (or (or D E) (or H (or I K))) (or (or D E) (or H (or I L))) (or (or D E) (or H (or I M))) (or (or D E) (or H (or I N))) (or (or D E) (or H (or I O))) (or (or D E) (or H (or J K))) (or (or D E) (or H (or J L))) (or (or D E) (or H (or J M))) (or (or D E) (or H (or J N))) (or (or D E) (or H (or J O))) (or (or D E) (or H (or K L))) (or (or D E) (or H (or K M))) (or (or D E) (or H (or K N))) (or (or D E) (or H (or K O))) (or (or D E) (or H (or L M))) (or (or D E) (or H (or L N))) (or (or D E) (or H (or L O))) (or (or D E) (or H (or M N))) (or (or D E) (or H (or M O))) (or (or D E) (or H (or N O))) (or (or D E) (or I (or J K))) (or (or D E) (or I (or J L))) (or (or D E) (or I (or J M))) (or (or D E) (or I (or J N))) (or (or D E) (or I (or J O))) (or (or D E) (or I (or K L))) (or (or D E) (or I (or K M))) (or (or D E) (or I (or K N))) (or (or D E) (or I (or K O))) (or (or D E) (or I (or L M))) (or (or D E) (or I (or L N))) (or (or D E) (or I (or L O))) (or (or D E) (or I (or M N))) (or (or D E) (or I (or M O))) (or (or D E) (or I (or N O))) (or (or D E) (or J (or K L))) (or (or D E) (or J (or K M))) (or (or D E) (or J (or K N))) (or (or D E) (or J (or K O))) (or (or D E) (or J (or L M))) (or (or D E) (or J (or L N))) (or (or D E) (or J (or L O))) (or (or D E) (or J (or M N))) (or (or D E) (or J (or M O))) (or (or D E) (or J (or N O))) (or (or D E) (or K (or L M))) (or (or D E) (or K (or L N))) (or (or D E) (or K (or L O))) (or (or D E) (or K (or M N))) (or (or D E) (or K (or M O))) (or (or D E) (or K (or N O))) (or (or D E) (or L (or M N))) (or (or D E) (or L (or M O))) (or (or D E) (or L (or N O))) (or (or D E) (or M (or N O))) (or (or D F) (or G (or H I))) (or (or D F) (or G (or H J))) (or (or D F) (or G (or H K))) (or (or D F) (or G (or H L))) (or (or D F) (or G (or H M))) (or (or D F) (or G (or H N))) (or (or D F) (or G (or H O))) (or (or D F) (or G (or I J))) (or (or D F) (or G (or I K))) (or (or D F) (or G (or I L))) (or (or D F) (or G (or I M))) (or (or D F) (or G (or I N))) (or (or D F) (or G (or I O))) (or (or D F) (or G (or J K))) (or (or D F) (or G (or J L))) (or (or D F) (or G (or J M))) (or (or D F) (or G (or J N))) (or (or D F) (or G (or J O))) (or (or D F) (or G (or K L))) (or (or D F) (or G (or K M))) (or (or D F) (or G (or K N))) (or (or D F) (or G (or K O))) (or (or D F) (or G (or L M))) (or (or D F) (or G (or L N))) (or (or D F) (or G (or L O))) (or (or D F) (or G (or M N))) (or (or D F) (or G (or M O))) (or (or D F) (or G (or N O))) (or (or D F) (or H (or I J))) (or (or D F) (or H (or I K))) (or (or D F) (or H (or I L))) (or (or D F) (or H (or I M))) (or (or D F) (or H (or I N))) (or (or D F) (or H (or I O))) (or (or D F) (or H (or J K))) (or (or D F) (or H (or J L))) (or (or D F) (or H (or J M))) (or (or D F) (or H (or J N))) (or (or D F) (or H (or J O))) (or (or D F) (or H (or K L))) (or (or D F) (or H (or K M))) (or (or D F) (or H (or K N))) (or (or D F) (or H (or K O))) (or (or D F) (or H (or L M))) (or (or D F) (or H (or L N))) (or (or D F) (or H (or L O))) (or (or D F) (or H (or M N))) (or (or D F) (or H (or M O))) (or (or D F) (or H (or N O))) (or (or D F) (or I (or J K))) (or (or D F) (or I (or J L))) (or (or D F) (or I (or J M))) (or (or D F) (or I (or J N))) (or (or D F) (or I (or J O))) (or (or D F) (or I (or K L))) (or (or D F) (or I (or K M))) (or (or D F) (or I (or K N))) (or (or D F) (or I (or K O))) (or (or D F) (or I (or L M))) (or (or D F) (or I (or L N))) (or (or D F) (or I (or L O))) (or (or D F) (or I (or M N))) (or (or D F) (or I (or M O))) (or (or D F) (or I (or N O))) (or (or D F) (or J (or K L))) (or (or D F) (or J (or K M))) (or (or D F) (or J (or K N))) (or (or D F) (or J (or K O))) (or (or D F) (or J (or L M))) (or (or D F) (or J (or L N))) (or (or D F) (or J (or L O))) (or (or D F) (or J (or M N))) (or (or D F) (or J (or M O))) (or (or D F) (or J (or N O))) (or (or D F) (or K (or L M))) (or (or D F) (or K (or L N))) (or (or D F) (or K (or L O))) (or (or D F) (or K (or M N))) (or (or D F) (or K (or M O))) (or (or D F) (or K (or N O))) (or (or D F) (or L (or M N))) (or (or D F) (or L (or M O))) (or (or D F) (or L (or N O))) (or (or D F) (or M (or N O))) (or (or D G) (or H (or I J))) (or (or D G) (or H (or I K))) (or (or D G) (or H (or I L))) (or (or D G) (or H (or I M))) (or (or D G) (or H (or I N))) (or (or D G) (or H (or I O))) (or (or D G) (or H (or J K))) (or (or D G) (or H (or J L))) (or (or D G) (or H (or J M))) (or (or D G) (or H (or J N))) (or (or D G) (or H (or J O))) (or (or D G) (or H (or K L))) (or (or D G) (or H (or K M))) (or (or D G) (or H (or K N))) (or (or D G) (or H (or K O))) (or (or D G) (or H (or L M))) (or (or D G) (or H (or L N))) (or (or D G) (or H (or L O))) (or (or D G) (or H (or M N))) (or (or D G) (or H (or M O))) (or (or D G) (or H (or N O))) (or (or D G) (or I (or J K))) (or (or D G) (or I (or J L))) (or (or D G) (or I (or J M))) (or (or D G) (or I (or J N))) (or (or D G) (or I (or J O))) (or (or D G) (or I (or K L))) (or (or D G) (or I (or K M))) (or (or D G) (or I (or K N))) (or (or D G) (or I (or K O))) (or (or D G) (or I (or L M))) (or (or D G) (or I (or L N))) (or (or D G) (or I (or L O))) (or (or D G) (or I (or M N))) (or (or D G) (or I (or M O))) (or (or D G) (or I (or N O))) (or (or D G) (or J (or K L))) (or (or D G) (or J (or K M))) (or (or D G) (or J (or K N))) (or (or D G) (or J (or K O))) (or (or D G) (or J (or L M))) (or (or D G) (or J (or L N))) (or (or D G) (or J (or L O))) (or (or D G) (or J (or M N))) (or (or D G) (or J (or M O))) (or (or D G) (or J (or N O))) (or (or D G) (or K (or L M))) (or (or D G) (or K (or L N))) (or (or D G) (or K (or L O))) (or (or D G) (or K (or M N))) (or (or D G) (or K (or M O))) (or (or D G) (or K (or N O))) (or (or D G) (or L (or M N))) (or (or D G) (or L (or M O))) (or (or D G) (or L (or N O))) (or (or D G) (or M (or N O))) (or (or D H) (or I (or J K))) (or (or D H) (or I (or J L))) (or (or D H) (or I (or J M))) (or (or D H) (or I (or J N))) (or (or D H) (or I (or J O))) (or (or D H) (or I (or K L))) (or (or D H) (or I (or K M))) (or (or D H) (or I (or K N))) (or (or D H) (or I (or K O))) (or (or D H) (or I (or L M))) (or (or D H) (or I (or L N))) (or (or D H) (or I (or L O))) (or (or D H) (or I (or M N))) (or (or D H) (or I (or M O))) (or (or D H) (or I (or N O))) (or (or D H) (or J (or K L))) (or (or D H) (or J (or K M))) (or (or D H) (or J (or K N))) (or (or D H) (or J (or K O))) (or (or D H) (or J (or L M))) (or (or D H) (or J (or L N))) (or (or D H) (or J (or L O))) (or (or D H) (or J (or M N))) (or (or D H) (or J (or M O))) (or (or D H) (or J (or N O))) (or (or D H) (or K (or L M))) (or (or D H) (or K (or L N))) (or (or D H) (or K (or L O))) (or (or D H) (or K (or M N))) (or (or D H) (or K (or M O))) (or (or D H) (or K (or N O))) (or (or D H) (or L (or M N))) (or (or D H) (or L (or M O))) (or (or D H) (or L (or N O))) (or (or D H) (or M (or N O))) (or (or D I) (or J (or K L))) (or (or D I) (or J (or K M))) (or (or D I) (or J (or K N))) (or (or D I) (or J (or K O))) (or (or D I) (or J (or L M))) (or (or D I) (or J (or L N))) (or (or D I) (or J (or L O))) (or (or D I) (or J (or M N))) (or (or D I) (or J (or M O))) (or (or D I) (or J (or N O))) (or (or D I) (or K (or L M))) (or (or D I) (or K (or L N))) (or (or D I) (or K (or L O))) (or (or D I) (or K (or M N))) (or (or D I) (or K (or M O))) (or (or D I) (or K (or N O))) (or (or D I) (or L (or M N))) (or (or D I) (or L (or M O))) (or (or D I) (or L (or N O))) (or (or D I) (or M (or N O))) (or (or D J) (or K (or L M))) (or (or D J) (or K (or L N))) (or (or D J) (or K (or L O))) (or (or D J) (or K (or M N))) (or (or D J) (or K (or M O))) (or (or D J) (or K (or N O))) (or (or D J) (or L (or M N))) (or (or D J) (or L (or M O))) (or (or D J) (or L (or N O))) (or (or D J) (or M (or N O))) (or (or D K) (or L (or M N))) (or (or D K) (or L (or M O))) (or (or D K) (or L (or N O))) (or (or D K) (or M (or N O))) (or (or D L) (or M (or N O))) (or (or E F) (or G (or H I))) (or (or E F) (or G (or H J))) (or (or E F) (or G (or H K))) (or (or E F) (or G (or H L))) (or (or E F) (or G (or H M))) (or (or E F) (or G (or H N))) (or (or E F) (or G (or H O))) (or (or E F) (or G (or I J))) (or (or E F) (or G (or I K))) (or (or E F) (or G (or I L))) (or (or E F) (or G (or I M))) (or (or E F) (or G (or I N))) (or (or E F) (or G (or I O))) (or (or E F) (or G (or J K))) (or (or E F) (or G (or J L))) (or (or E F) (or G (or J M))) (or (or E F) (or G (or J N))) (or (or E F) (or G (or J O))) (or (or E F) (or G (or K L))) (or (or E F) (or G (or K M))) (or (or E F) (or G (or K N))) (or (or E F) (or G (or K O))) (or (or E F) (or G (or L M))) (or (or E F) (or G (or L N))) (or (or E F) (or G (or L O))) (or (or E F) (or G (or M N))) (or (or E F) (or G (or M O))) (or (or E F) (or G (or N O))) (or (or E F) (or H (or I J))) (or (or E F) (or H (or I K))) (or (or E F) (or H (or I L))) (or (or E F) (or H (or I M))) (or (or E F) (or H (or I N))) (or (or E F) (or H (or I O))) (or (or E F) (or H (or J K))) (or (or E F) (or H (or J L))) (or (or E F) (or H (or J M))) (or (or E F) (or H (or J N))) (or (or E F) (or H (or J O))) (or (or E F) (or H (or K L))) (or (or E F) (or H (or K M))) (or (or E F) (or H (or K N))) (or (or E F) (or H (or K O))) (or (or E F) (or H (or L M))) (or (or E F) (or H (or L N))) (or (or E F) (or H (or L O))) (or (or E F) (or H (or M N))) (or (or E F) (or H (or M O))) (or (or E F) (or H (or N O))) (or (or E F) (or I (or J K))) (or (or E F) (or I (or J L))) (or (or E F) (or I (or J M))) (or (or E F) (or I (or J N))) (or (or E F) (or I (or J O))) (or (or E F) (or I (or K L))) (or (or E F) (or I (or K M))) (or (or E F) (or I (or K N))) (or (or E F) (or I (or K O))) (or (or E F) (or I (or L M))) (or (or E F) (or I (or L N))) (or (or E F) (or I (or L O))) (or (or E F) (or I (or M N))) (or (or E F) (or I (or M O))) (or (or E F) (or I (or N O))) (or (or E F) (or J (or K L))) (or (or E F) (or J (or K M))) (or (or E F) (or J (or K N))) (or (or E F) (or J (or K O))) (or (or E F) (or J (or L M))) (or (or E F) (or J (or L N))) (or (or E F) (or J (or L O))) (or (or E F) (or J (or M N))) (or (or E F) (or J (or M O))) (or (or E F) (or J (or N O))) (or (or E F) (or K (or L M))) (or (or E F) (or K (or L N))) (or (or E F) (or K (or L O))) (or (or E F) (or K (or M N))) (or (or E F) (or K (or M O))) (or (or E F) (or K (or N O))) (or (or E F) (or L (or M N))) (or (or E F) (or L (or M O))) (or (or E F) (or L (or N O))) (or (or E F) (or M (or N O))) (or (or E G) (or H (or I J))) (or (or E G) (or H (or I K))) (or (or E G) (or H (or I L))) (or (or E G) (or H (or I M))) (or (or E G) (or H (or I N))) (or (or E G) (or H (or I O))) (or (or E G) (or H (or J K))) (or (or E G) (or H (or J L))) (or (or E G) (or H (or J M))) (or (or E G) (or H (or J N))) (or (or E G) (or H (or J O))) (or (or E G) (or H (or K L))) (or (or E G) (or H (or K M))) (or (or E G) (or H (or K N))) (or (or E G) (or H (or K O))) (or (or E G) (or H (or L M))) (or (or E G) (or H (or L N))) (or (or E G) (or H (or L O))) (or (or E G) (or H (or M N))) (or (or E G) (or H (or M O))) (or (or E G) (or H (or N O))) (or (or E G) (or I (or J K))) (or (or E G) (or I (or J L))) (or (or E G) (or I (or J M))) (or (or E G) (or I (or J N))) (or (or E G) (or I (or J O))) (or (or E G) (or I (or K L))) (or (or E G) (or I (or K M))) (or (or E G) (or I (or K N))) (or (or E G) (or I (or K O))) (or (or E G) (or I (or L M))) (or (or E G) (or I (or L N))) (or (or E G) (or I (or L O))) (or (or E G) (or I (or M N))) (or (or E G) (or I (or M O))) (or (or E G) (or I (or N O))) (or (or E G) (or J (or K L))) (or (or E G) (or J (or K M))) (or (or E G) (or J (or K N))) (or (or E G) (or J (or K O))) (or (or E G) (or J (or L M))) (or (or E G) (or J (or L N))) (or (or E G) (or J (or L O))) (or (or E G) (or J (or M N))) (or (or E G) (or J (or M O))) (or (or E G) (or J (or N O))) (or (or E G) (or K (or L M))) (or (or E G) (or K (or L N))) (or (or E G) (or K (or L O))) (or (or E G) (or K (or M N))) (or (or E G) (or K (or M O))) (or (or E G) (or K (or N O))) (or (or E G) (or L (or M N))) (or (or E G) (or L (or M O))) (or (or E G) (or L (or N O))) (or (or E G) (or M (or N O))) (or (or E H) (or I (or J K))) (or (or E H) (or I (or J L))) (or (or E H) (or I (or J M))) (or (or E H) (or I (or J N))) (or (or E H) (or I (or J O))) (or (or E H) (or I (or K L))) (or (or E H) (or I (or K M))) (or (or E H) (or I (or K N))) (or (or E H) (or I (or K O))) (or (or E H) (or I (or L M))) (or (or E H) (or I (or L N))) (or (or E H) (or I (or L O))) (or (or E H) (or I (or M N))) (or (or E H) (or I (or M O))) (or (or E H) (or I (or N O))) (or (or E H) (or J (or K L))) (or (or E H) (or J (or K M))) (or (or E H) (or J (or K N))) (or (or E H) (or J (or K O))) (or (or E H) (or J (or L M))) (or (or E H) (or J (or L N))) (or (or E H) (or J (or L O))) (or (or E H) (or J (or M N))) (or (or E H) (or J (or M O))) (or (or E H) (or J (or N O))) (or (or E H) (or K (or L M))) (or (or E H) (or K (or L N))) (or (or E H) (or K (or L O))) (or (or E H) (or K (or M N))) (or (or E H) (or K (or M O))) (or (or E H) (or K (or N O))) (or (or E H) (or L (or M N))) (or (or E H) (or L (or M O))) (or (or E H) (or L (or N O))) (or (or E H) (or M (or N O))) (or (or E I) (or J (or K L))) (or (or E I) (or J (or K M))) (or (or E I) (or J (or K N))) (or (or E I) (or J (or K O))) (or (or E I) (or J (or L M))) (or (or E I) (or J (or L N))) (or (or E I) (or J (or L O))) (or (or E I) (or J (or M N))) (or (or E I) (or J (or M O))) (or (or E I) (or J (or N O))) (or (or E I) (or K (or L M))) (or (or E I) (or K (or L N))) (or (or E I) (or K (or L O))) (or (or E I) (or K (or M N))) (or (or E I) (or K (or M O))) (or (or E I) (or K (or N O))) (or (or E I) (or L (or M N))) (or (or E I) (or L (or M O))) (or (or E I) (or L (or N O))) (or (or E I) (or M (or N O))) (or (or E J) (or K (or L M))) (or (or E J) (or K (or L N))) (or (or E J) (or K (or L O))) (or (or E J) (or K (or M N))) (or (or E J) (or K (or M O))) (or (or E J) (or K (or N O))) (or (or E J) (or L (or M N))) (or (or E J) (or L (or M O))) (or (or E J) (or L (or N O))) (or (or E J) (or M (or N O))) (or (or E K) (or L (or M N))) (or (or E K) (or L (or M O))) (or (or E K) (or L (or N O))) (or (or E K) (or M (or N O))) (or (or E L) (or M (or N O))) (or (or F G) (or H (or I J))) (or (or F G) (or H (or I K))) (or (or F G) (or H (or I L))) (or (or F G) (or H (or I M))) (or (or F G) (or H (or I N))) (or (or F G) (or H (or I O))) (or (or F G) (or H (or J K))) (or (or F G) (or H (or J L))) (or (or F G) (or H (or J M))) (or (or F G) (or H (or J N))) (or (or F G) (or H (or J O))) (or (or F G) (or H (or K L))) (or (or F G) (or H (or K M))) (or (or F G) (or H (or K N))) (or (or F G) (or H (or K O))) (or (or F G) (or H (or L M))) (or (or F G) (or H (or L N))) (or (or F G) (or H (or L O))) (or (or F G) (or H (or M N))) (or (or F G) (or H (or M O))) (or (or F G) (or H (or N O))) (or (or F G) (or I (or J K))) (or (or F G) (or I (or J L))) (or (or F G) (or I (or J M))) (or (or F G) (or I (or J N))) (or (or F G) (or I (or J O))) (or (or F G) (or I (or K L))) (or (or F G) (or I (or K M))) (or (or F G) (or I (or K N))) (or (or F G) (or I (or K O))) (or (or F G) (or I (or L M))) (or (or F G) (or I (or L N))) (or (or F G) (or I (or L O))) (or (or F G) (or I (or M N))) (or (or F G) (or I (or M O))) (or (or F G) (or I (or N O))) (or (or F G) (or J (or K L))) (or (or F G) (or J (or K M))) (or (or F G) (or J (or K N))) (or (or F G) (or J (or K O))) (or (or F G) (or J (or L M))) (or (or F G) (or J (or L N))) (or (or F G) (or J (or L O))) (or (or F G) (or J (or M N))) (or (or F G) (or J (or M O))) (or (or F G) (or J (or N O))) (or (or F G) (or K (or L M))) (or (or F G) (or K (or L N))) (or (or F G) (or K (or L O))) (or (or F G) (or K (or M N))) (or (or F G) (or K (or M O))) (or (or F G) (or K (or N O))) (or (or F G) (or L (or M N))) (or (or F G) (or L (or M O))) (or (or F G) (or L (or N O))) (or (or F G) (or M (or N O))) (or (or F H) (or I (or J K))) (or (or F H) (or I (or J L))) (or (or F H) (or I (or J M))) (or (or F H) (or I (or J N))) (or (or F H) (or I (or J O))) (or (or F H) (or I (or K L))) (or (or F H) (or I (or K M))) (or (or F H) (or I (or K N))) (or (or F H) (or I (or K O))) (or (or F H) (or I (or L M))) (or (or F H) (or I (or L N))) (or (or F H) (or I (or L O))) (or (or F H) (or I (or M N))) (or (or F H) (or I (or M O))) (or (or F H) (or I (or N O))) (or (or F H) (or J (or K L))) (or (or F H) (or J (or K M))) (or (or F H) (or J (or K N))) (or (or F H) (or J (or K O))) (or (or F H) (or J (or L M))) (or (or F H) (or J (or L N))) (or (or F H) (or J (or L O))) (or (or F H) (or J (or M N))) (or (or F H) (or J (or M O))) (or (or F H) (or J (or N O))) (or (or F H) (or K (or L M))) (or (or F H) (or K (or L N))) (or (or F H) (or K (or L O))) (or (or F H) (or K (or M N))) (or (or F H) (or K (or M O))) (or (or F H) (or K (or N O))) (or (or F H) (or L (or M N))) (or (or F H) (or L (or M O))) (or (or F H) (or L (or N O))) (or (or F H) (or M (or N O))) (or (or F I) (or J (or K L))) (or (or F I) (or J (or K M))) (or (or F I) (or J (or K N))) (or (or F I) (or J (or K O))) (or (or F I) (or J (or L M))) (or (or F I) (or J (or L N))) (or (or F I) (or J (or L O))) (or (or F I) (or J (or M N))) (or (or F I) (or J (or M O))) (or (or F I) (or J (or N O))) (or (or F I) (or K (or L M))) (or (or F I) (or K (or L N))) (or (or F I) (or K (or L O))) (or (or F I) (or K (or M N))) (or (or F I) (or K (or M O))) (or (or F I) (or K (or N O))) (or (or F I) (or L (or M N))) (or (or F I) (or L (or M O))) (or (or F I) (or L (or N O))) (or (or F I) (or M (or N O))) (or (or F J) (or K (or L M))) (or (or F J) (or K (or L N))) (or (or F J) (or K (or L O))) (or (or F J) (or K (or M N))) (or (or F J) (or K (or M O))) (or (or F J) (or K (or N O))) (or (or F J) (or L (or M N))) (or (or F J) (or L (or M O))) (or (or F J) (or L (or N O))) (or (or F J) (or M (or N O))) (or (or F K) (or L (or M N))) (or (or F K) (or L (or M O))) (or (or F K) (or L (or N O))) (or (or F K) (or M (or N O))) (or (or F L) (or M (or N O))) (or (or G H) (or I (or J K))) (or (or G H) (or I (or J L))) (or (or G H) (or I (or J M))) (or (or G H) (or I (or J N))) (or (or G H) (or I (or J O))) (or (or G H) (or I (or K L))) (or (or G H) (or I (or K M))) (or (or G H) (or I (or K N))) (or (or G H) (or I (or K O))) (or (or G H) (or I (or L M))) (or (or G H) (or I (or L N))) (or (or G H) (or I (or L O))) (or (or G H) (or I (or M N))) (or (or G H) (or I (or M O))) (or (or G H) (or I (or N O))) (or (or G H) (or J (or K L))) (or (or G H) (or J (or K M))) (or (or G H) (or J (or K N))) (or (or G H) (or J (or K O))) (or (or G H) (or J (or L M))) (or (or G H) (or J (or L N))) (or (or G H) (or J (or L O))) (or (or G H) (or J (or M N))) (or (or G H) (or J (or M O))) (or (or G H) (or J (or N O))) (or (or G H) (or K (or L M))) (or (or G H) (or K (or L N))) (or (or G H) (or K (or L O))) (or (or G H) (or K (or M N))) (or (or G H) (or K (or M O))) (or (or G H) (or K (or N O))) (or (or G H) (or L (or M N))) (or (or G H) (or L (or M O))) (or (or G H) (or L (or N O))) (or (or G H) (or M (or N O))) (or (or G I) (or J (or K L))) (or (or G I) (or J (or K M))) (or (or G I) (or J (or K N))) (or (or G I) (or J (or K O))) (or (or G I) (or J (or L M))) (or (or G I) (or J (or L N))) (or (or G I) (or J (or L O))) (or (or G I) (or J (or M N))) (or (or G I) (or J (or M O))) (or (or G I) (or J (or N O))) (or (or G I) (or K (or L M))) (or (or G I) (or K (or L N))) (or (or G I) (or K (or L O))) (or (or G I) (or K (or M N))) (or (or G I) (or K (or M O))) (or (or G I) (or K (or N O))) (or (or G I) (or L (or M N))) (or (or G I) (or L (or M O))) (or (or G I) (or L (or N O))) (or (or G I) (or M (or N O))) (or (or G J) (or K (or L M))) (or (or G J) (or K (or L N))) (or (or G J) (or K (or L O))) (or (or G J) (or K (or M N))) (or (or G J) (or K (or M O))) (or (or G J) (or K (or N O))) (or (or G J) (or L (or M N))) (or (or G J) (or L (or M O))) (or (or G J) (or L (or N O))) (or (or G J) (or M (or N O))) (or (or G K) (or L (or M N))) (or (or G K) (or L (or M O))) (or (or G K) (or L (or N O))) (or (or G K) (or M (or N O))) (or (or G L) (or M (or N O))) (or (or H I) (or J (or K L))) (or (or H I) (or J (or K M))) (or (or H I) (or J (or K N))) (or (or H I) (or J (or K O))) (or (or H I) (or J (or L M))) (or (or H I) (or J (or L N))) (or (or H I) (or J (or L O))) (or (or H I) (or J (or M N))) (or (or H I) (or J (or M O))) (or (or H I) (or J (or N O))) (or (or H I) (or K (or L M))) (or (or H I) (or K (or L N))) (or (or H I) (or K (or L O))) (or (or H I) (or K (or M N))) (or (or H I) (or K (or M O))) (or (or H I) (or K (or N O))) (or (or H I) (or L (or M N))) (or (or H I) (or L (or M O))) (or (or H I) (or L (or N O))) (or (or H I) (or M (or N O))) (or (or H J) (or K (or L M))) (or (or H J) (or K (or L N))) (or (or H J) (or K (or L O))) (or (or H J) (or K (or M N))) (or (or H J) (or K (or M O))) (or (or H J) (or K (or N O))) (or (or H J) (or L (or M N))) (or (or H J) (or L (or M O))) (or (or H J) (or L (or N O))) (or (or H J) (or M (or N O))) (or (or H K) (or L (or M N))) (or (or H K) (or L (or M O))) (or (or H K) (or L (or N O))) (or (or H K) (or M (or N O))) (or (or H L) (or M (or N O))) (or (or I J) (or K (or L M))) (or (or I J) (or K (or L N))) (or (or I J) (or K (or L O))) (or (or I J) (or K (or M N))) (or (or I J) (or K (or M O))) (or (or I J) (or K (or N O))) (or (or I J) (or L (or M N))) (or (or I J) (or L (or M O))) (or (or I J) (or L (or N O))) (or (or I J) (or M (or N O))) (or (or I K) (or L (or M N))) (or (or I K) (or L (or M O))) (or (or I K) (or L (or N O))) (or (or I K) (or M (or N O))) (or (or I L) (or M (or N O))) (or (or J K) (or L (or M N))) (or (or J K) (or L (or M O))) (or (or J K) (or L (or N O))) (or (or J K) (or M (or N O))) (or (or J L) (or M (or N O))) (or (or K L) (or M (or N O)))) Policy metrics: width=3003, depth=9 Resolution time: 25.233160585s test signer::tests::test_threshold_signature has been running for over 60 seconds Signers creation time: 47.936777817s Generate nonces time 10.685056119s Process nonces time 33.181015477s Aggregate nonces time: 5.947102132s Signature phase2 time: 7.271503ms Verification time: 164.057µs ``` >*Despite our compiler being pretty cool, it's not production-ready. It means we didn't do any optimizations and didn't parallelize the signature and proof generation. All is run in one thread. Sorry!* - Monotone Only: No negations. You can't express "NOT Alice." > *P.S. This is fundamental to the cryptographic realizability, not a bug!* > *P.P.S Having a NOT gate would allow us to compile literally any Boolean circuit (thus any other P-class problem) into the BLISK circuit, creating tremendous possibilities such as "one-key verifiable virtual machines" and other exotic constructions such as implication "if Alice signed, then Bob must too". But yeah, we simply do not know yet how to represent the NOT gate* - Proof System Choice: OR gates require zero-knowledge proofs to make a resolution publicly verifiable. Your choice of proof system (SNARKs, Bulletproofs, etc.) affects setup assumptions and verification costs. In our reference example it's Bulletproofs. - Liveness: Like any multisig, if required participants go offline, you can't sign. BLISK doesn't solve the coordination problem; it just makes the authorization problem more expressive. ## Getting started Finally, here is a clear reference to our compiler! ``` https://github.com/zero-art-rs/blisk ``` Follow the How-To guide in `README.md`, play around, experiment, benchmark, make PRs, and give feedback! ## Conclusion BLISK takes two well-understood primitives, multisignatures and key agreement, and composes them into something surprisingly powerful. It's a reminder that sometimes the best innovations aren't new primitives but new ways of combining existing ones. The next time someone asks you to implement "CEO or (CFO and 2 board members)," you don't have to implement if through a smart contract. You can just compile it into a key. And that's pretty cool!