Teaching models of computation

Dependencies for this notebook: graphviz executable installed on the system and on the path, networkx and graphviz python anaconda packages. (See here for the documentation of the latter package.)

Please run the utility code at the bottom of this notebook first.

You should be able to upload this notebook to the JupyterHub instance on canvas.

comment: In this notebook I use x_17 and not x17 for 3SAT and 3NAND formula to be more consistent with our notation for NAND. This is of course not very important.

Useful unicode symbols: φ ∨ ∧ ¬ ≠ Ψ

In [35]:
import graphviz
from graphviz import Graph
from graphviz import Digraph

import networkx as nx

import warnings

import math

import pydotplus

def nxgraph(G):
    P = pydotplus.graph_from_dot_data(G.source)
    return nx.drawing.nx_pydot.from_pydot(P)

In a typical "Theory of Computation" course, one introduces the notion of computation by the following models:

  1. Deterministic Finite automata, showing their equivalence to their non-deterministic variants and regular expressoins.

  2. Context Free Grammars (sometimes showing their equivalence to pushdown automata)

  3. Turing machines

For example, the first six chapters (until page 101) of the 1969 book Formal languages and their relation to automata by Aho and Ullman are titled Languages and their representations, Grammars, Finite automata and regular Grammars, Context Free Grammars, Pushdown Automata and Turing Machines. The first three chapters (until page 187) of Sipser's book are called Regular Languages, Context-Free Languages, and The Church-Turing Thesis (which defined Turing machines and their variants).

The rationale behind using this sequence is that (a) regular expressions and context free grammars are important and practically useful tools, (b) These models are in some sense "simpler" than Turing Machines (they are definitely weaker) and so proving theorems about them can get students used to arguing about computational models, and (c) There is an extremely well-written book by Sipser that makes teaching in this order easier for both instructors and students.

Yet, when I decided to redesign Harvard's Theory of Computation course I decided to change this "standard sequence" in several ways.

Reducing and deferring automata and context-free grammars

I do not start with automata, regular expressions and context free grammaers, and only discuss them briefly and much later in the course, specifically after we talk about uncomputability. The reasons behind this are the following:

  1. While Automata, Regular Expressions, and Context Free Grammars are useful topics in general, they are not central for modern theoretical computer science.

  2. The main practical motivation for non-Turing complete models such as regular expressions and context-free grammar is best understood after you've seen uncomputability and the Halting problem. We use regular expression for search or context-free grammars for programming language syntax precisely because we don't want our computer to go into an infinite loop when we execute a query or try to check for syntax error. Historically, these formalisms were also introduced after Turing machines.

  3. While doing simple proofs with automata and grammars certainly teaches students useful skills, this is by no means the only route to obtain those skills.

Using programming language as the central model

Rather than talk about "machines" or "devices" such as automata or Turing machines, I prefer to focus on models that are based on programming languages. I do this for several reasons:

  1. I think programming languages are more intuitive and connected to the practice of computing for today's students, almost all of whom have programming experience.

  2. Working with programming languages naturally lends itself to implementation such as a website where students can play with the computational models. Indeed this blog post itself is a Python Interactive Notebook, which you can play with here.

  3. To demonstrate the power of our seemingly simple models we often show students results such as the equivalence of one tape and multi-tape Turing machines, or one dimensional and two dimensional tapes. In the context of programming languages, this corresponds to showing how we can implement syntactic sugar by compiling (or "transpiling") code that uses, for example, two dimensional arrays, into code that only has one-dimensional arrays. These textual transformations are more intuitive, and also correspond more closely to current computing practice.

  4. Last but not least, one of the most important lessons of theory of computation is the duality of code and data, which means that we can think of our programs as simply strings of text that can be passed as input to other programs. This viewpoint is much more natural when our metaphor for computation is computer code (which is a string) as opposed to a physical device such as a "machine". The universal machine becomes an interpreter: a concept that is again already familiar to many students.

Our first model: Boolean Circuits

Rather than starting with automata, our first model is Boolean circuits. This means that we don't have to talk about infinite functions. However, Boolean circuits are rich enough to capture all our standard algorithms, and moreover we can already talk about representing circuits as strings and feeding them as input to other circuits.

Indeed, per the "programming language philosophy" above, we emphasize the straightline program viewpoint of circuits, which automatically comes with a string representation. In particular, this string representation makes the counting argument for circuit lower bounds almost trivial: the number of programs that can be described by programs of $s$ characters over an alphabet $\Sigma$ is clearly at most $|\Sigma|^s$.

The circuit model connects more easily to physical implementation of computing such as transistors and encoding 0's and 1's via electrical currents. It also enables us to make mathematical sense of statements such as "this cryptosystem has $128$ bits of security" or assertions about quantum superiority via finite experiments. Finally, starting with circuits puts us in a better shape for the proof of the Cook Levin Theorem.

To make life simpler, we choose one of the simplest universal bases for circuits, namely the basis consisting of the single function $NAND:\{0,1\}^2 \rightarrow \{0,1\}$ defined as $NAND(a,b)=\overline{a \wedge b}$. Thus, our first model is a programming language where every line has the form foo := bar NAND blah which corresponds to assigning to the variable foo the NAND of the values of the variables bar and blah.

For example, this is the NAND program corresponding to the XOR function:

In [3]:
xor =r'''u   := x_0 NAND x_1
v   := x_0 NAND u
w   := x_1 NAND u
y_0 := v   NAND w

For every assignment of the variables x_0 and x_1, at the end of the execution the variable y_0 will contain the XOR of these two variables.

It is very easy to write five lines of Python code to evaluate a NAND program:

In [4]:
# return a list of triples of the form ('foo','bar','blah')
# for every line of the form 'foo := bar NAND blah'  in the program P
def lines(P):
    lineslist = [line.split() for line in P.rstrip('\n').split('\n')]
    return [(foo,bar,blah) for (foo,_,bar,_,blah) in lineslist ]

# Evaluate a NAND program P. 
# Update the table of variables with new values
def NANDEVAL(P, vals = {} ):
    for (foo,bar,blah) in lines(P):
        # foo gets NAND of bar and blah (default to 0 if not in table)
        vals[foo] = 1 - vals.get(bar,0)*vals.get(blah,0)
    return vals

Let's try this out

In [5]:
vals = NANDEVAL(xor,{'x_0':0,'x_1':1})

Straightline programs of course can be easily described as a circuit, with the transformation again being few lines of Python.

In [6]:
# Transform a NAND program P into a Boolean circuit (i.e. DAG)
# with NAND gates
def circuit(P):
    G = Digraph()
    vertices = {}
    line = 0
    for (foo,bar,blah) in lines(P):
        vtx = f'{line}){foo}'
        vertices[foo] = vtx
        line += 1
    return G
In [7]:
%3 x_0 x_0 0)u 0)u x_0->0)u 1)v 1)v x_0->1)v 0)u->1)v 2)w 2)w 0)u->2)w x_1 x_1 x_1->0)u x_1->2)w 3)y_0 3)y_0 1)v->3)y_0 2)w->3)y_0

Syntactic sugar

Both in theory and practice there is a tension between expressiveness and simplicity of computational models. The model of NAND circuits (or equivalently, straightline programs) is pretty simple, but it can be shown to be expressive via various syntactic sugar transformations that show that we can implement concepts such as loops, functions, if statements, and more on top of it. The website nandpl.org contains an "unsweetener" that can compile a NAND program with syntactic sugar constructs into an equivalent one that doesn't use them. (We also have OCaml and Javascript thanks to the wonderful work of my teaching fellows Juan Esteller and Gabe Montague).

For example, the following is a "sugared" version of a NAND program to compute the majority or "at least two" function that on input three bits outputs 1 if and only if at least two of them are one.

In [8]:
atleasttwosweet=r'''def a := NOT(b) { 
  a := b NAND b

def a :=  AND(b, c) {
  a := NOT(b NAND c) 

def a := OR(b, c) { 
  a := NOT(b) NAND NOT(c) 

def a := ATLEASTTWO(b, c, d) { 
  a := OR(AND(b, c), OR(AND(b, d), AND(c, d)))

y_0 := ATLEASTTWO(x_0, x_1, x_2) 

And here is the "unsweetened" version, produced automatically:

In [9]:
atleasttwo =r'''upupunique_3 := x_0 NAND x_1
upunique_4 := upupunique_3 NAND upupunique_3
upupunique_3 := x_0 NAND x_2
upunique_5 := upupunique_3 NAND upupunique_3
upupunique_3 := x_1 NAND x_2
upunique_6 := upupunique_3 NAND upupunique_3
upupunique_0 := upunique_5 NAND upunique_5
upupunique_1 := upunique_6 NAND upunique_6
upunique_7 := upupunique_0 NAND upupunique_1
upupunique_0 := upunique_4 NAND upunique_4
upupunique_1 := upunique_7 NAND upunique_7
y_0 := upupunique_0 NAND upupunique_1
In [10]:

And the corresponding circuit:

In [11]:
%3 x_0 x_0 0)upupunique_3 0)upupunique_3 x_0->0)upupunique_3 2)upupunique_3 2)upupunique_3 x_0->2)upupunique_3 1)upunique_4 1)upunique_4 0)upupunique_3->1)upunique_4 0)upupunique_3->1)upunique_4 x_1 x_1 x_1->0)upupunique_3 4)upupunique_3 4)upupunique_3 x_1->4)upupunique_3 9)upupunique_0 9)upupunique_0 1)upunique_4->9)upupunique_0 1)upunique_4->9)upupunique_0 3)upunique_5 3)upunique_5 2)upupunique_3->3)upunique_5 2)upupunique_3->3)upunique_5 x_2 x_2 x_2->2)upupunique_3 x_2->4)upupunique_3 6)upupunique_0 6)upupunique_0 3)upunique_5->6)upupunique_0 3)upunique_5->6)upupunique_0 5)upunique_6 5)upunique_6 4)upupunique_3->5)upunique_6 4)upupunique_3->5)upunique_6 7)upupunique_1 7)upupunique_1 5)upunique_6->7)upupunique_1 5)upunique_6->7)upupunique_1 8)upunique_7 8)upunique_7 6)upupunique_0->8)upunique_7 7)upupunique_1->8)upunique_7 10)upupunique_1 10)upupunique_1 8)upunique_7->10)upupunique_1 8)upunique_7->10)upupunique_1 11)y_0 11)y_0 9)upupunique_0->11)y_0 10)upupunique_1->11)y_0

Infinite functions and Turing Machines / NAND++

To handle functions of unbounded inputs, we need to introduce loops. We do so by simply having a special variable loop that, if it is set to $1$, the program goes back to the beginning. To get the full power of Turing completeness we also need access to unbounded storage, which we do by allowing a special index variable i. If a line of code involves a variable foo_i then this is replaced by the current value of i.

You can think of i as corresponding to the "head" of a Turing machine's tape, and to get a model that is basically identical to a Turing machine one can then add operators that would increment and decrement i. For convenience, we will not use such operations but rather have i proceed obliviously according to the schedule $0,1,0,1,2,1,0,1,2,3,2,1,0,1,2,\ldots$ (that one student referred to as an "infinite Sabbath elevator"). That is, at time period t the value of i is index(t) defined as follows:

In [12]:
# Returns the value of the index variable i in  iteration number k
def index(t):
    r = math.floor(math.sqrt(t+1/4)-1/2)
    return (t-r*(r+1) if t <= (r+1)*(r+1) else (r+1)*(r+2)-t)

[index(t) for t in range(20)]
[0, 1, 0, 1, 2, 1, 0, 1, 2, 3, 2, 1, 0, 1, 2, 3, 4, 3, 2, 1]

For example, this is a NAND++ program that computes the AND function:

In [13]:
andpp = r'''y_0 := flag NAND flag
notx   := x_i NAND x_i
nottmp := validx_i NAND notx
notflag  := flag NAND flag
flag := notflag NAND nottmp
halt := validx_i NAND validx_i
loop := halt NAND halt

(The value validx_$j$ at some position $j$ is equal to $1$ if $j$ is smaller than the length of the input, and to $0$ otherwise. Such a marker is necessary to handle inputs of variable sizes.)

To evaluate a NAND++ program, we can use our NAND evaluator to repeatedly evaluate the corresponding NAND program until loop is false.

In [14]:
# Evaluate NAND++ program P on input x
    vals = {}
    for i in range(len(x)):
        vals[f'x_{i}'] = int(x[i])
        vals[f'validx_{i}'] = 1
    t = 0
    while True:
        vals = NANDEVAL(P.replace('_i',f'_{index(t)}'),vals)
        if not vals.get('loop',0): break
        t += 1
    return vals['y_0']
In [15]:

The NAND++ model can be easily shown equivalent to Turing machines and other models such as the $\lambda$ calculus, and we do so in the lectures.

RAM machines

When we refer to an $O(n^2)$ time algorithm in an algorithm class (or a whiteboard software development interview..), we don't mean running in $O(n^2)$ time on a Turing machine, but rather on a RAM model. I think it is important to convey the lesson that this can be made mathematically precise. Thus I also introduce a RAM variant which I call NAND<< (though am happy to consider suggestion for nicer names :) ). We show that this can be simulated up to polynomial overhead by NAND++/Turing machines, but use this for our formal definition of $TIME(T(n))$. One (very minor) advantage for the RAM model is that the unviersal machine only has a constant overhead, and so the time hierarchy theorem can be made tighter. Perhaps more significantly, this model is much closer to programming languages such as C/Python/JavaScript etc.. that students might be familiar with.

"Dictionary" of computational models

To sum up, we have three main computational models in this course:

  • NAND programs, which are the same as Boolean circuits (with NAND gates)

  • NAND++ programs, which are the same as Turing Machines (with a single tape and oblivious head movement)

  • NAND<< programs, which are the same as RAM machines

The Cook Levin Theorem

One advantage of working with models that are so close to Boolean circuits, is that the proof of the Cook-Levin Theorem becomes much simpler. We prove it by showing that for every $L \in \mathbf{NP}$,

$$L \leq_p NANDSAT \leq_p 3NAND \leq_p 3SAT$$

where $NANDSAT$ is CIRCUITSAT for circuits with NAND gates, and $3NAND$ is like $3SAT$ except that the constraints are of the form $(x_i = x_j NAND x_k)$.

The reduction of an arbitrary language/function in $\mathbf{NP}$ to $NANDSAT$ is almost trivial. It consists of taking a NAND++ program (think Turing machine) $P$, a time bound $T$, an instance $x\in \{0,1\}^n$ and a number $m$ corresponding to the witness length, and mapping it into a NAND program (think circuit) $Q$ with $m$ inputs such that $Q(w)=P(xw)$ for every $w\in \{0,1\}^m$ (assuming $P$ does not need more than $T$ steps).

In Python this is obtained by composing two steps:

  1. "Unrolling the loop" to map a NAND++ program $P$ of $\ell$ lines and a time bound $T$ into a NAND program $Q$ of $T\ell$ lines that is obtained by simply "copy pasting" $T$ copies of $P$.

  2. "Hardwiring the input" $x$ to the first $n$ inputs of $Q$ to obtain a program $Q_x$ such that $Q_x(w)=Q(xw)$.

In [16]:
# For "hardwiring" it is a sueful convention that we have variables "one" and "zero" that
# always have the values 1 and 0 respectively
def pref(P):
    return r'''notx_0 := x_0 NAND x_0
one := x_0 NAND notx_0
zero := one NAND one
In [17]:
andpp = pref(andpp)
notx_0 := x_0 NAND x_0
one := x_0 NAND notx_0
zero := one NAND one
y_0 := flag NAND flag
notx   := x_i NAND x_i
nottmp := validx_i NAND notx
notflag  := flag NAND flag
flag := notflag NAND nottmp
halt := validx_i NAND validx_i
loop := halt NAND halt

In [18]:
#Input: NAND++ "simple" prog P, time bound T, input length n
#Output: n-input NAND program of T|P| lines computing same function
def expand(P,T,n):
    result = ""
    for t in range(T):
        validx = ('one' if i<n else 'zero')
        result += P.replace('validx_i',validx).replace( '_i',f'_{i}')
    return result
In [19]:
# "hardwire" an input x to a NAND program Q
# return Q' s.t. Q'(y)=Q(xy)
def hardwire(Q,x):
    n = len(x)
    for i in range(n): Q = Q.replace(f'x_{i}',('one' if x[i]=='1' else 'zero'))
    for i in range(n,len(Q)): # move x_n,x_n+1,.... to x_0,x_1,...
        Q = Q.replace(f'x_{i}',f'x_{i-n}')
    return Q
In [20]:
# reduce F in NP to NANDSAT
# Input: x,T and and a NAND++ prog P s.t. 
#       F(x)=1 iff there exists y in {0,1}^m s.t. P(xy)=1 within T steps
# Output: Q s.t. NANDSAT(Q)=F(x)
def NP2NANDSAT_(P,T,m,x):
    Q = expand(P,T,len(x)+m)
    return hardwire(Q,x)
In [21]:
# This is the version of the function above that keeps track of y
# if it is given as extra input. Otherwise behaves identically.
# reduce F in NP to NANDSAT
# Input: x,T and and a NAND++ prog P s.t. 
#       F(x)=1 iff there exists y in {0,1}^m s.t. P(xy)=1 within T steps
# Output: Q s.t. NANDSAT(Q)=F(x)
def NP2NANDSAT(P,T,m,x,y=""):
    if y and len(y) != m: raise Exception
    Q = expand(P,T,len(x)+m)
    Q = hardwire(Q,x)
    return (Q,y) if y else Q
In [22]:
Q = NP2NANDSAT(andpp,17,3,"11")

Now reducing from $NANDSAT$ to $3NAND$ is done in the same way we typically reduce a circuit to a formula: introduce a variable for each line.

In [23]:
# Clause list of a 3CNF/3NAND formula  φ
def getclauses(φ):
    clauses =  φ.split("∧")
    res = []
    for c in clauses:
        (v0,_,v1,_,v2) = c.strip()[1:-1].split()
    return res

# number of variables of a formula φ
def numvars(φ):
    for n in range(len(φ)-1,0,-1):
        if φ.find(f'x_{n}')>= 0: return n+1
    raise Exception
In [24]:
# Reduce NANDSAT to 3NAND
# Input: NAND prog Q
# Output: 3NAND formula Ψ
#        s.t. Ψ satisfiable iff Q is
    n = numvars(Q); m = len(Q); varidx = {}; Ψ = ''
    #varidx[u] is index corresponding to last value of u
    ZERO = n+2 # assume "zero" is written to in line 2
    for i in range(n): varidx[f'x_{i}'] = i # setup x_0...x_n-1
    # vars x_n ... x_n+m-1 correspond to lines
    j= n
    for line in Q.rstrip('\n').split('\n'): 
        (u,_,v,_,w) = line.split() # line is "u := v NAND w"
        #add constraint x_j = x_l NAND x_k, where k, l correspond to last     
        #lines v and w were written to
        Ψ += f"(x_{j} = x_{varidx.get(v,ZERO)} NAND x_{varidx.get(w,ZERO)}) ∧ "
        varidx[u] = j # update last line u is written to
        j += 1
    # output should be one
    Ψ += f'(x_{varidx["y_0"]} = x_{ZERO} NAND x_{ZERO})'
    return Ψ

Though of course the resulting formula can be quite big:

In [25]:
'(x_3 = x_5 NAND x_5) ∧ (x_4 = x_5 NAND x_3) ∧ (x_5 = x_4 NAND x_4) ∧ (x_6 = x_5 NAND x_5) ∧ (x_7 = x_4 NAND x_4) ∧ (x_8 = x_4 NAND x_7) ∧ (x_9 = x_5 NAND x_5) ∧ (x_10 = x_9 NAND x_8) ∧ (x_11 = x_4 NAND x_4) ∧ (x_12 = x_11 NAND x_11) ∧ (x_13 = x_4 NAND x_4) ∧ (x_14 = x_4 NAND x_13) ∧ (x_15 = x_14 NAND x_14) ∧ (x_16 = x_10 NAND x_10) ∧ (x_17 = x_14 NAND x_14) ∧ (x_18 = x_14 NAND x_17) ∧ (x_19 = x_10 NAND x_10) ∧ (x_20 = x_19 NAND x_18) ∧ (x_21 = x_14 NAND x_14) ∧ (x_22 = x_21 NAND x_21) ∧ (x_23 = x_14 NAND x_14) ∧ (x_24 = x_14 NAND x_23) ∧ (x_25 = x_24 NAND x_24) ∧ (x_26 = x_20 NAND x_20) ∧ (x_27 = x_24 NAND x_24) ∧ (x_28 = x_24 NAND x_27) ∧ (x_29 = x_20 NAND x_20) ∧ (x_30 = x_29 NAND x_28) ∧ (x_31 = x_24 NAND x_24) ∧ (x_32 = x_31 NAND x_31) ∧ (x_33 = x_24 NAND x_24) ∧ (x_34 = x_24 NAND x_33) ∧ (x_35 = x_34 NAND x_34) ∧ (x_36 = x_30 NAND x_30) ∧ (x_37 = x_34 NAND x_34) ∧ (x_38 = x_34 NAND x_37) ∧ (x_39 = x_30 NAND x_30) ∧ (x_40 = x_39 NAND x_38) ∧ (x_41 = x_34 NAND x_34) ∧ (x_42 = x_41 NAND x_41) ∧ (x_43 = x_34 NAND x_34) ∧ (x_44 = x_34 NAND x_43) ∧ (x_45 = x_44 NAND x_44) ∧ (x_46 = x_40 NAND x_40) ∧ (x_47 = x_0 NAND x_0) ∧ (x_48 = x_44 NAND x_47) ∧ (x_49 = x_40 NAND x_40) ∧ (x_50 = x_49 NAND x_48) ∧ (x_51 = x_44 NAND x_44) ∧ (x_52 = x_51 NAND x_51) ∧ (x_53 = x_44 NAND x_44) ∧ (x_54 = x_44 NAND x_53) ∧ (x_55 = x_54 NAND x_54) ∧ (x_56 = x_50 NAND x_50) ∧ (x_57 = x_54 NAND x_54) ∧ (x_58 = x_54 NAND x_57) ∧ (x_59 = x_50 NAND x_50) ∧ (x_60 = x_59 NAND x_58) ∧ (x_61 = x_54 NAND x_54) ∧ (x_62 = x_61 NAND x_61) ∧ (x_63 = x_54 NAND x_54) ∧ (x_64 = x_54 NAND x_63) ∧ (x_65 = x_64 NAND x_64) ∧ (x_66 = x_60 NAND x_60) ∧ (x_67 = x_64 NAND x_64) ∧ (x_68 = x_64 NAND x_67) ∧ (x_69 = x_60 NAND x_60) ∧ (x_70 = x_69 NAND x_68) ∧ (x_71 = x_64 NAND x_64) ∧ (x_72 = x_71 NAND x_71) ∧ (x_73 = x_64 NAND x_64) ∧ (x_74 = x_64 NAND x_73) ∧ (x_75 = x_74 NAND x_74) ∧ (x_76 = x_70 NAND x_70) ∧ (x_77 = x_74 NAND x_74) ∧ (x_78 = x_74 NAND x_77) ∧ (x_79 = x_70 NAND x_70) ∧ (x_80 = x_79 NAND x_78) ∧ (x_81 = x_74 NAND x_74) ∧ (x_82 = x_81 NAND x_81) ∧ (x_83 = x_74 NAND x_74) ∧ (x_84 = x_74 NAND x_83) ∧ (x_85 = x_84 NAND x_84) ∧ (x_86 = x_80 NAND x_80) ∧ (x_87 = x_0 NAND x_0) ∧ (x_88 = x_84 NAND x_87) ∧ (x_89 = x_80 NAND x_80) ∧ (x_90 = x_89 NAND x_88) ∧ (x_91 = x_84 NAND x_84) ∧ (x_92 = x_91 NAND x_91) ∧ (x_93 = x_84 NAND x_84) ∧ (x_94 = x_84 NAND x_93) ∧ (x_95 = x_94 NAND x_94) ∧ (x_96 = x_90 NAND x_90) ∧ (x_97 = x_1 NAND x_1) ∧ (x_98 = x_94 NAND x_97) ∧ (x_99 = x_90 NAND x_90) ∧ (x_100 = x_99 NAND x_98) ∧ (x_101 = x_94 NAND x_94) ∧ (x_102 = x_101 NAND x_101) ∧ (x_103 = x_94 NAND x_94) ∧ (x_104 = x_94 NAND x_103) ∧ (x_105 = x_104 NAND x_104) ∧ (x_106 = x_100 NAND x_100) ∧ (x_107 = x_0 NAND x_0) ∧ (x_108 = x_104 NAND x_107) ∧ (x_109 = x_100 NAND x_100) ∧ (x_110 = x_109 NAND x_108) ∧ (x_111 = x_104 NAND x_104) ∧ (x_112 = x_111 NAND x_111) ∧ (x_113 = x_104 NAND x_104) ∧ (x_114 = x_104 NAND x_113) ∧ (x_115 = x_114 NAND x_114) ∧ (x_116 = x_110 NAND x_110) ∧ (x_117 = x_114 NAND x_114) ∧ (x_118 = x_114 NAND x_117) ∧ (x_119 = x_110 NAND x_110) ∧ (x_120 = x_119 NAND x_118) ∧ (x_121 = x_114 NAND x_114) ∧ (x_122 = x_121 NAND x_121) ∧ (x_123 = x_114 NAND x_114) ∧ (x_124 = x_114 NAND x_123) ∧ (x_125 = x_124 NAND x_124) ∧ (x_126 = x_120 NAND x_120) ∧ (x_127 = x_124 NAND x_124) ∧ (x_128 = x_124 NAND x_127) ∧ (x_129 = x_120 NAND x_120) ∧ (x_130 = x_129 NAND x_128) ∧ (x_131 = x_124 NAND x_124) ∧ (x_132 = x_131 NAND x_131) ∧ (x_133 = x_124 NAND x_124) ∧ (x_134 = x_124 NAND x_133) ∧ (x_135 = x_134 NAND x_134) ∧ (x_136 = x_130 NAND x_130) ∧ (x_137 = x_134 NAND x_134) ∧ (x_138 = x_134 NAND x_137) ∧ (x_139 = x_130 NAND x_130) ∧ (x_140 = x_139 NAND x_138) ∧ (x_141 = x_134 NAND x_134) ∧ (x_142 = x_141 NAND x_141) ∧ (x_143 = x_134 NAND x_134) ∧ (x_144 = x_134 NAND x_143) ∧ (x_145 = x_144 NAND x_144) ∧ (x_146 = x_140 NAND x_140) ∧ (x_147 = x_0 NAND x_0) ∧ (x_148 = x_144 NAND x_147) ∧ (x_149 = x_140 NAND x_140) ∧ (x_150 = x_149 NAND x_148) ∧ (x_151 = x_144 NAND x_144) ∧ (x_152 = x_151 NAND x_151) ∧ (x_153 = x_144 NAND x_144) ∧ (x_154 = x_144 NAND x_153) ∧ (x_155 = x_154 NAND x_154) ∧ (x_156 = x_150 NAND x_150) ∧ (x_157 = x_1 NAND x_1) ∧ (x_158 = x_154 NAND x_157) ∧ (x_159 = x_150 NAND x_150) ∧ (x_160 = x_159 NAND x_158) ∧ (x_161 = x_154 NAND x_154) ∧ (x_162 = x_161 NAND x_161) ∧ (x_163 = x_154 NAND x_154) ∧ (x_164 = x_154 NAND x_163) ∧ (x_165 = x_164 NAND x_164) ∧ (x_166 = x_160 NAND x_160) ∧ (x_167 = x_2 NAND x_2) ∧ (x_168 = x_164 NAND x_167) ∧ (x_169 = x_160 NAND x_160) ∧ (x_170 = x_169 NAND x_168) ∧ (x_171 = x_164 NAND x_164) ∧ (x_172 = x_171 NAND x_171) ∧ (x_166 = x_5 NAND x_5)'
In [26]:
# Version of input above that keeps track of satisfying assignment y if given
# Reduce NANDSAT to 3NAND
# Input: NAND prog Q
# Output: 3NAND formula Ψ
#        s.t. Ψ satisfiable iff Q is
def NANDSAT23NAND(Q,y=""):
    n = numvars(Q)
    m = len(Q.rstrip('\n').split('\n'))
    z = ["0"]*(m+n)
    varidx = {}
    Ψ = ''
    ZERO = n+2 # assume "zero" is written to in line 2
    for i in range(n): 
        varidx[f'x_{i}'] = i
        if y: z[i]=y[i]
    lastoutput = 0
    j= n
    for line in Q.rstrip('\n').split('\n'):
        if Ψ: Ψ += ' ∧ '
        (u,_,v,_,w) = line.split()
        if u=='y_0': lastoutput = j
        k = varidx.get(v,ZERO)
        l = varidx.get(w,ZERO)
        Ψ += f"(x_{j} = x_{k} NAND x_{l})"
        z[j] = "0" if z[k]=="1" and z[l]=="1" else "1"
        varidx[u] = j
        j += 1
    Ψ += f' ∧  (x_{lastoutput} = x_{ZERO} NAND x_{ZERO})'
    return  (Ψ, "".join(z)) if y else Ψ

Finally, reducing $3NAND$ to $3SAT$ just uses the fact that $a = b$ $NAND$ $c$ iff $(\neg a \vee \neg b \vee \neg c) \wedge (a \vee b) \wedge (a \vee c)$

In [27]:
# Evaluate 3CNF φ on assignment x 
# Both are represented as strings
def evalcnf(φ,x):

    def varval(v):
        return (1-int(x[int(v[3:])])  if v[0]=="¬" else int(x[int(v[2:])]))
    for (v0,v1,v2) in getclauses(φ):
        # print(c+str([varval(v0),varval(v1),varval(v2)]))
        if not varval(v0)+varval(v1)+varval(v2): return False
    return True

# Clause list of a 3CNF φ
def getclauses(φ):
    clauses =  φ.split("∧")
    res = []
    for c in clauses:
        (v0,_,v1,_,v2) = c.strip()[1:-1].split()
    return res

# number of variables of a formula φ
def numvars(φ):
    for n in range(len(φ)-1,0,-1):
        if φ.find('x_'+str(n))>= 0: return n+1
    raise Exception
In [28]:
# Reduce 3NAND to 3SAT
# Input: 3NAND formula Ψ
# Output: 3CNF formula φ
#        s.t.  φ satisfiable iff Ψ is
def NAND23SAT_(Ψ):
    φ = ""
    for (a,b,c) in getclauses(Ψ):
        φ += f'(¬{a} ∨ ¬{b} ∨ ¬{c}) ∧ ({a}{b}{b})   ∧ ({a}{c}{c})  ∧'
    return φ[:-1] # chop off redundant ∧
In [29]:
# Same as above but keeping track of assignment
def NAND23SAT(Ψ,y=""):
    φ = ""
    for (a,b,c) in getclauses(Ψ):
        φ += f'(¬{a} ∨ ¬{b} ∨ ¬{c}) ∧ ({a}{b}{b})   ∧ ({a}{c}{c})  ∧'
    return (φ[:-1],y) if y else φ[:-1] # chop off redundant ∧

We can plug on top of this the reductions from $3SAT$ to Independent Set and from Independent Set to Max Cut to get some pretty pictures. (To produce the figures below I use slightly modified versions of the reductions that are "Levin Reductions" in the sense that they keep track of the witness and use that to color the vertices corresponding to the independent set or maximum cut red.)

In [30]:
# Reduction φ ↦ G
def SAT2IS_(φ):
    n = numvars(φ) 
    G =Graph(engine='neato')
    # add pairs "x_i=0" and "x_i=1"
    for i in range(n): G.edge(f'x_{i}=0',f'x_{i}=1')
    # map "x_7" with index 5 to "5)x_7≠0", "¬x_12" with index 6 to "6)x_12≠1"
    def nodename(v,c): return str(c)+')'+(v[1:]+"≠1" if v[0]=="¬" else v+"≠0")
    #map "5)x_7≠0" to its neighbor "x_7=0"
    def neighbor(n):   return n.split(')')[1].split('≠')[0]+"="+n[-1]
    c = 0
    for C in getclauses(φ):
        (u,v,w) = (nodename(C[0],c),nodename(C[1],c+1),nodename(C[2],c+2))
        # add triangle of clause
        # connect each vertex to inconsistent neighbor
        c += 3
    return G
In [31]:
# same reduction but taking care of colors and keeping track what happens to an assignment
def SAT2IS(φ,x=""):
    S = []
    n = numvars(φ) 
    G =Graph(engine='neato')
    for i in range(n):
        u = f"x_{i}=0"
        v = f"x_{i}=1"
        G.node(u,style='filled',fillcolor=('red' if x and x[i]=="0" else 'green'))
        G.node(v,style='filled',fillcolor=('red' if x and x[i]=="1" else 'green'))
        if x: S.append(u if x[i]=='0' else v)
    def nodename(v):
        return ((v[1:],"≠1") if v[0]=="¬" else (v,"≠0"))
    cnum = 0
    for C in getclauses(φ):
        lastv = None
        found = False
        for v in C:
            (var,cond) = nodename(v)
            name = f'{cnum}){var}{cond}'
            cnum += 1
            color = 'lightblue'
            if x and (not found) and x[int(var[2:])]!=cond[1]:
                found = True
                color = 'red'
            if lastv: G.edge(lastv,name,len='1')
            lastv = name
    return (G if not x else (G,S))
In [32]:
# same reduction as above but handling colors and showing the resulting cut when the original graph has independent set
def IS2MAXCUT(G,I=[]):
    G =nxgraph(G)
    S = []
    H =Graph(engine='sfdp',graph_attr={'overlap':'false'})
    for v in G.nodes():
        color = ('red' if I and v in I else 'lightblue')
        ecol = 'black'
        pwidth = '1'
        if I and v in I: 
            ecol = 'red'
            pwidth = '2'
    j =0
    for (u,v) in G.edges():
        g1 = "e"+str(j)+"a"
        g2 = "e"+str(j)+"b"
        c1 = 'green'
        c2 = 'green'
        if I and (not u in I):
            c1 = 'red'
        if I and (not v in I):
            c2 = 'red'
        gadget = Graph("gadget"+str(j))
        gadget.edge(g1,g2,len="1",color=('red' if (g1 in S) != (g2 in I) else 'black'), penwidth=('2' if (g1 in S) != (g2 in I) else '1'))
        gadget.edge(u,g1,len="1", color=('red' if (g1 in S) != (u in I) else 'black'),penwidth =('2' if (g1 in S) != (u in S) else '1')  )
        gadget.edge(v,g2,len="1", color=('red' if (g2 in S) != (v in I) else 'black'),penwidth= ('2' if (g2 in S) != (v in S) else '1') )
        H.edge(g1,"source",color=('red' if (g1 in S)  else 'black'),penwidth=('2' if (g1 in S)  else '1')) # ,len="2.5"
        H.edge(g2,"source",color=('red' if (g2 in S)  else 'black'),penwidth= ('2' if (g2 in S)  else '1') )
        j +=1
    return (H,S) if I else H
In [33]:
%3 x_0=0 x_0=0 x_0=1 x_0=1 x_0=0--x_0=1 x_1=0 x_1=0 x_1=1 x_1=1 x_1=0--x_1=1 x_2=0 x_2=0 x_2=1 x_2=1 x_2=0--x_2=1 x_3=0 x_3=0 x_3=1 x_3=1 x_3=0--x_3=1 x_4=0 x_4=0 x_4=1 x_4=1 x_4=0--x_4=1 x_5=0 x_5=0 x_5=1 x_5=1 x_5=0--x_5=1 x_6=0 x_6=0 x_6=1 x_6=1 x_6=0--x_6=1 x_7=0 x_7=0 x_7=1 x_7=1 x_7=0--x_7=1 x_8=0 x_8=0 x_8=1 x_8=1 x_8=0--x_8=1 x_9=0 x_9=0 x_9=1 x_9=1 x_9=0--x_9=1 x_10=0 x_10=0 x_10=1 x_10=1 x_10=0--x_10=1 x_11=0 x_11=0 x_11=1 x_11=1 x_11=0--x_11=1 x_12=0 x_12=0 x_12=1 x_12=1 x_12=0--x_12=1 x_13=0 x_13=0 x_13=1 x_13=1 x_13=0--x_13=1 x_14=0 x_14=0 x_14=1 x_14=1 x_14=0--x_14=1 x_15=0 x_15=0 x_15=1 x_15=1 x_15=0--x_15=1 x_16=0 x_16=0 x_16=1 x_16=1 x_16=0--x_16=1 x_17=0 x_17=0 x_17=1 x_17=1 x_17=0--x_17=1 x_18=0 x_18=0 x_18=1 x_18=1 x_18=0--x_18=1 x_19=0 x_19=0 x_19=1 x_19=1 x_19=0--x_19=1 x_20=0 x_20=0 x_20=1 x_20=1 x_20=0--x_20=1 x_21=0 x_21=0 x_21=1 x_21=1 x_21=0--x_21=1 x_22=0 x_22=0 x_22=1 x_22=1 x_22=0--x_22=1 x_23=0 x_23=0 x_23=1 x_23=1 x_23=0--x_23=1 x_24=0 x_24=0 x_24=1 x_24=1 x_24=0--x_24=1 x_25=0 x_25=0 x_25=1 x_25=1 x_25=0--x_25=1 x_26=0 x_26=0 x_26=1 x_26=1 x_26=0--x_26=1 x_27=0 x_27=0 x_27=1 x_27=1 x_27=0--x_27=1 x_28=0 x_28=0 x_28=1 x_28=1 x_28=0--x_28=1 x_29=0 x_29=0 x_29=1 x_29=1 x_29=0--x_29=1 x_30=0 x_30=0 x_30=1 x_30=1 x_30=0--x_30=1 x_31=0 x_31=0 x_31=1 x_31=1 x_31=0--x_31=1 x_32=0 x_32=0 x_32=1 x_32=1 x_32=0--x_32=1 x_33=0 x_33=0 x_33=1 x_33=1 x_33=0--x_33=1 x_34=0 x_34=0 x_34=1 x_34=1 x_34=0--x_34=1 x_35=0 x_35=0 x_35=1 x_35=1 x_35=0--x_35=1 x_36=0 x_36=0 x_36=1 x_36=1 x_36=0--x_36=1 x_37=0 x_37=0 x_37=1 x_37=1 x_37=0--x_37=1 x_38=0 x_38=0 x_38=1 x_38=1 x_38=0--x_38=1 x_39=0 x_39=0 x_39=1 x_39=1 x_39=0--x_39=1 x_40=0 x_40=0 x_40=1 x_40=1 x_40=0--x_40=1 x_41=0 x_41=0 x_41=1 x_41=1 x_41=0--x_41=1 x_42=0 x_42=0 x_42=1 x_42=1 x_42=0--x_42=1 x_43=0 x_43=0 x_43=1 x_43=1 x_43=0--x_43=1 x_44=0 x_44=0 x_44=1 x_44=1 x_44=0--x_44=1 x_45=0 x_45=0 x_45=1 x_45=1 x_45=0--x_45=1 x_46=0 x_46=0 x_46=1 x_46=1 x_46=0--x_46=1 x_47=0 x_47=0 x_47=1 x_47=1 x_47=0--x_47=1 x_48=0 x_48=0 x_48=1 x_48=1 x_48=0--x_48=1 x_49=0 x_49=0 x_49=1 x_49=1 x_49=0--x_49=1 x_50=0 x_50=0 x_50=1 x_50=1 x_50=0--x_50=1 x_51=0 x_51=0 x_51=1 x_51=1 x_51=0--x_51=1 x_52=0 x_52=0 x_52=1 x_52=1 x_52=0--x_52=1 x_53=0 x_53=0 x_53=1 x_53=1 x_53=0--x_53=1 x_54=0 x_54=0 x_54=1 x_54=1 x_54=0--x_54=1 x_55=0 x_55=0 x_55=1 x_55=1 x_55=0--x_55=1 x_56=0 x_56=0 x_56=1 x_56=1 x_56=0--x_56=1 x_57=0 x_57=0 x_57=1 x_57=1 x_57=0--x_57=1 x_58=0 x_58=0 x_58=1 x_58=1 x_58=0--x_58=1 x_59=0 x_59=0 x_59=1 x_59=1 x_59=0--x_59=1 x_60=0 x_60=0 x_60=1 x_60=1 x_60=0--x_60=1 x_61=0 x_61=0 x_61=1 x_61=1 x_61=0--x_61=1 x_62=0 x_62=0 x_62=1 x_62=1 x_62=0--x_62=1 x_63=0 x_63=0 x_63=1 x_63=1 x_63=0--x_63=1 x_64=0 x_64=0 x_64=1 x_64=1 x_64=0--x_64=1 x_65=0 x_65=0 x_65=1 x_65=1 x_65=0--x_65=1 x_66=0 x_66=0 x_66=1 x_66=1 x_66=0--x_66=1 x_67=0 x_67=0 x_67=1 x_67=1 x_67=0--x_67=1 x_68=0 x_68=0 x_68=1 x_68=1 x_68=0--x_68=1 x_69=0 x_69=0 x_69=1 x_69=1 x_69=0--x_69=1 x_70=0 x_70=0 x_70=1 x_70=1 x_70=0--x_70=1 x_71=0 x_71=0 x_71=1 x_71=1 x_71=0--x_71=1 x_72=0 x_72=0 x_72=1 x_72=1 x_72=0--x_72=1 x_73=0 x_73=0 x_73=1 x_73=1 x_73=0--x_73=1 x_74=0 x_74=0 x_74=1 x_74=1 x_74=0--x_74=1 x_75=0 x_75=0 x_75=1 x_75=1 x_75=0--x_75=1 x_76=0 x_76=0 x_76=1 x_76=1 x_76=0--x_76=1 x_77=0 x_77=0 x_77=1 x_77=1 x_77=0--x_77=1 x_78=0 x_78=0 x_78=1 x_78=1 x_78=0--x_78=1 x_79=0 x_79=0 x_79=1 x_79=1 x_79=0--x_79=1 x_80=0 x_80=0 x_80=1 x_80=1 x_80=0--x_80=1 x_81=0 x_81=0 x_81=1 x_81=1 x_81=0--x_81=1 x_82=0 x_82=0 x_82=1 x_82=1 x_82=0--x_82=1 x_83=0 x_83=0 x_83=1 x_83=1 x_83=0--x_83=1 x_84=0 x_84=0 x_84=1 x_84=1 x_84=0--x_84=1 x_85=0 x_85=0 x_85=1 x_85=1 x_85=0--x_85=1 x_86=0 x_86=0 x_86=1 x_86=1 x_86=0--x_86=1 x_87=0 x_87=0 x_87=1 x_87=1 x_87=0--x_87=1 x_88=0 x_88=0 x_88=1 x_88=1 x_88=0--x_88=1 x_89=0 x_89=0 x_89=1 x_89=1 x_89=0--x_89=1 x_90=0 x_90=0 x_90=1 x_90=1 x_90=0--x_90=1 x_91=0 x_91=0 x_91=1 x_91=1 x_91=0--x_91=1 x_92=0 x_92=0 x_92=1 x_92=1 x_92=0--x_92=1 x_93=0 x_93=0 x_93=1 x_93=1 x_93=0--x_93=1 x_94=0 x_94=0 x_94=1 x_94=1 x_94=0--x_94=1 x_95=0 x_95=0 x_95=1 x_95=1 x_95=0--x_95=1 x_96=0 x_96=0 x_96=1 x_96=1 x_96=0--x_96=1 x_97=0 x_97=0 x_97=1 x_97=1 x_97=0--x_97=1 x_98=0 x_98=0 x_98=1 x_98=1 x_98=0--x_98=1 x_99=0 x_99=0 x_99=1 x_99=1 x_99=0--x_99=1 x_100=0 x_100=0 x_100=1 x_100=1 x_100=0--x_100=1 x_101=0 x_101=0 x_101=1 x_101=1 x_101=0--x_101=1 x_102=0 x_102=0 x_102=1 x_102=1 x_102=0--x_102=1 x_103=0 x_103=0 x_103=1 x_103=1 x_103=0--x_103=1 x_104=0 x_104=0 x_104=1 x_104=1 x_104=0--x_104=1 x_105=0 x_105=0 x_105=1 x_105=1 x_105=0--x_105=1 x_106=0 x_106=0 x_106=1 x_106=1 x_106=0--x_106=1 x_107=0 x_107=0 x_107=1 x_107=1 x_107=0--x_107=1 x_108=0 x_108=0 x_108=1 x_108=1 x_108=0--x_108=1 x_109=0 x_109=0 x_109=1 x_109=1 x_109=0--x_109=1 x_110=0 x_110=0 x_110=1 x_110=1 x_110=0--x_110=1 x_111=0 x_111=0 x_111=1 x_111=1 x_111=0--x_111=1 x_112=0 x_112=0 x_112=1 x_112=1 x_112=0--x_112=1 x_113=0 x_113=0 x_113=1 x_113=1 x_113=0--x_113=1 x_114=0 x_114=0 x_114=1 x_114=1 x_114=0--x_114=1 x_115=0 x_115=0 x_115=1 x_115=1 x_115=0--x_115=1 x_116=0 x_116=0 x_116=1 x_116=1 x_116=0--x_116=1 x_117=0 x_117=0 x_117=1 x_117=1 x_117=0--x_117=1 x_118=0 x_118=0 x_118=1 x_118=1 x_118=0--x_118=1 x_119=0 x_119=0 x_119=1 x_119=1 x_119=0--x_119=1 x_120=0 x_120=0 x_120=1 x_120=1 x_120=0--x_120=1 x_121=0 x_121=0 x_121=1 x_121=1 x_121=0--x_121=1 x_122=0 x_122=0 x_122=1 x_122=1 x_122=0--x_122=1 x_123=0 x_123=0 x_123=1 x_123=1 x_123=0--x_123=1 x_124=0 x_124=0 x_124=1 x_124=1 x_124=0--x_124=1 x_125=0 x_125=0 x_125=1 x_125=1 x_125=0--x_125=1 x_126=0 x_126=0 x_126=1 x_126=1 x_126=0--x_126=1 x_127=0 x_127=0 x_127=1 x_127=1 x_127=0--x_127=1 x_128=0 x_128=0 x_128=1 x_128=1 x_128=0--x_128=1 x_129=0 x_129=0 x_129=1 x_129=1 x_129=0--x_129=1 x_130=0 x_130=0 x_130=1 x_130=1 x_130=0--x_130=1 x_131=0 x_131=0 x_131=1 x_131=1 x_131=0--x_131=1 x_132=0 x_132=0 x_132=1 x_132=1 x_132=0--x_132=1 x_133=0 x_133=0 x_133=1 x_133=1 x_133=0--x_133=1 x_134=0 x_134=0 x_134=1 x_134=1 x_134=0--x_134=1 x_135=0 x_135=0 x_135=1 x_135=1 x_135=0--x_135=1 x_136=0 x_136=0 x_136=1 x_136=1 x_136=0--x_136=1 x_137=0 x_137=0 x_137=1 x_137=1 x_137=0--x_137=1 x_138=0 x_138=0 x_138=1 x_138=1 x_138=0--x_138=1 x_139=0 x_139=0 x_139=1 x_139=1 x_139=0--x_139=1 x_140=0 x_140=0 x_140=1 x_140=1 x_140=0--x_140=1 x_141=0 x_141=0 x_141=1 x_141=1 x_141=0--x_141=1 x_142=0 x_142=0 x_142=1 x_142=1 x_142=0--x_142=1 x_143=0 x_143=0 x_143=1 x_143=1 x_143=0--x_143=1 x_144=0 x_144=0 x_144=1 x_144=1 x_144=0--x_144=1 x_145=0 x_145=0 x_145=1 x_145=1 x_145=0--x_145=1 x_146=0 x_146=0 x_146=1 x_146=1 x_146=0--x_146=1 x_147=0 x_147=0 x_147=1 x_147=1 x_147=0--x_147=1 x_148=0 x_148=0 x_148=1 x_148=1 x_148=0--x_148=1 x_149=0 x_149=0 x_149=1 x_149=1 x_149=0--x_149=1 x_150=0 x_150=0 x_150=1 x_150=1 x_150=0--x_150=1 x_151=0 x_151=0 x_151=1 x_151=1 x_151=0--x_151=1 x_152=0 x_152=0 x_152=1 x_152=1 x_152=0--x_152=1 x_153=0 x_153=0 x_153=1 x_153=1 x_153=0--x_153=1 x_154=0 x_154=0 x_154=1 x_154=1 x_154=0--x_154=1 x_155=0 x_155=0 x_155=1 x_155=1 x_155=0--x_155=1 x_156=0 x_156=0 x_156=1 x_156=1 x_156=0--x_156=1 x_157=0 x_157=0 x_157=1 x_157=1 x_157=0--x_157=1 x_158=0 x_158=0 x_158=1 x_158=1 x_158=0--x_158=1 x_159=0 x_159=0 x_159=1 x_159=1 x_159=0--x_159=1 x_160=0 x_160=0 x_160=1 x_160=1 x_160=0--x_160=1 x_161=0 x_161=0 x_161=1 x_161=1 x_161=0--x_161=1 x_162=0 x_162=0 x_162=1 x_162=1 x_162=0--x_162=1 x_163=0 x_163=0 x_163=1 x_163=1 x_163=0--x_163=1 x_164=0 x_164=0 x_164=1 x_164=1 x_164=0--x_164=1 x_165=0 x_165=0 x_165=1 x_165=1 x_165=0--x_165=1 x_166=0 x_166=0 x_166=1 x_166=1 x_166=0--x_166=1 x_167=0 x_167=0 x_167=1 x_167=1 x_167=0--x_167=1 x_168=0 x_168=0 x_168=1 x_168=1 x_168=0--x_168=1 x_169=0 x_169=0 x_169=1 x_169=1 x_169=0--x_169=1 x_170=0 x_170=0 x_170=1 x_170=1 x_170=0--x_170=1 x_171=0 x_171=0 x_171=1 x_171=1 x_171=0--x_171=1 x_172=0 x_172=0 x_172=1 x_172=1 x_172=0--x_172=1 0)x_3≠1 x_3≠1 0)x_3≠1--x_3=1 1)x_5≠1 x_5≠1 0)x_3≠1--1)x_5≠1 2)x_5≠1 x_5≠1 0)x_3≠1--2)x_5≠1 1)x_5≠1--x_5=1 1)x_5≠1--2)x_5≠1 2)x_5≠1--x_5=1 3)x_3≠0 x_3≠0 3)x_3≠0--x_3=0 4)x_5≠0 x_5≠0 3)x_3≠0--4)x_5≠0 5)x_5≠0 x_5≠0 3)x_3≠0--5)x_5≠0 4)x_5≠0--x_5=0 4)x_5≠0--5)x_5≠0 5)x_5≠0--x_5=0 6)x_3≠0 x_3≠0 6)x_3≠0--x_3=0 7)x_5≠0 x_5≠0 6)x_3≠0--7)x_5≠0 8)x_5≠0 x_5≠0 6)x_3≠0--8)x_5≠0 7)x_5≠0--x_5=0 7)x_5≠0--8)x_5≠0 8)x_5≠0--x_5=0 9)x_4≠1 x_4≠1 9)x_4≠1--x_4=1 10)x_5≠1 x_5≠1 9)x_4≠1--10)x_5≠1 11)x_3≠1 x_3≠1 9)x_4≠1--11)x_3≠1 10)x_5≠1--x_5=1 10)x_5≠1--11)x_3≠1 11)x_3≠1--x_3=1 12)x_4≠0 x_4≠0 12)x_4≠0--x_4=0 13)x_5≠0 x_5≠0 12)x_4≠0--13)x_5≠0 14)x_5≠0 x_5≠0 12)x_4≠0--14)x_5≠0 13)x_5≠0--x_5=0 13)x_5≠0--14)x_5≠0 14)x_5≠0--x_5=0 15)x_4≠0 x_4≠0 15)x_4≠0--x_4=0 16)x_3≠0 x_3≠0 15)x_4≠0--16)x_3≠0 17)x_3≠0 x_3≠0 15)x_4≠0--17)x_3≠0 16)x_3≠0--x_3=0 16)x_3≠0--17)x_3≠0 17)x_3≠0--x_3=0 18)x_5≠1 x_5≠1 18)x_5≠1--x_5=1 19)x_4≠1 x_4≠1 18)x_5≠1--19)x_4≠1 20)x_4≠1 x_4≠1 18)x_5≠1--20)x_4≠1 19)x_4≠1--x_4=1 19)x_4≠1--20)x_4≠1 20)x_4≠1--x_4=1 21)x_5≠0 x_5≠0 21)x_5≠0--x_5=0 22)x_4≠0 x_4≠0 21)x_5≠0--22)x_4≠0 23)x_4≠0 x_4≠0 21)x_5≠0--23)x_4≠0 22)x_4≠0--x_4=0 22)x_4≠0--23)x_4≠0 23)x_4≠0--x_4=0 24)x_5≠0 x_5≠0 24)x_5≠0--x_5=0 25)x_4≠0 x_4≠0 24)x_5≠0--25)x_4≠0 26)x_4≠0 x_4≠0 24)x_5≠0--26)x_4≠0 25)x_4≠0--x_4=0 25)x_4≠0--26)x_4≠0 26)x_4≠0--x_4=0 27)x_6≠1 x_6≠1 27)x_6≠1--x_6=1 28)x_5≠1 x_5≠1 27)x_6≠1--28)x_5≠1 29)x_5≠1 x_5≠1 27)x_6≠1--29)x_5≠1 28)x_5≠1--x_5=1 28)x_5≠1--29)x_5≠1 29)x_5≠1--x_5=1 30)x_6≠0 x_6≠0 30)x_6≠0--x_6=0 31)x_5≠0 x_5≠0 30)x_6≠0--31)x_5≠0 32)x_5≠0 x_5≠0 30)x_6≠0--32)x_5≠0 31)x_5≠0--x_5=0 31)x_5≠0--32)x_5≠0 32)x_5≠0--x_5=0 33)x_6≠0 x_6≠0 33)x_6≠0--x_6=0 34)x_5≠0 x_5≠0 33)x_6≠0--34)x_5≠0 35)x_5≠0 x_5≠0 33)x_6≠0--35)x_5≠0 34)x_5≠0--x_5=0 34)x_5≠0--35)x_5≠0 35)x_5≠0--x_5=0 36)x_7≠1 x_7≠1 36)x_7≠1--x_7=1 37)x_4≠1 x_4≠1 36)x_7≠1--37)x_4≠1 38)x_4≠1 x_4≠1 36)x_7≠1--38)x_4≠1 37)x_4≠1--x_4=1 37)x_4≠1--38)x_4≠1 38)x_4≠1--x_4=1 39)x_7≠0 x_7≠0 39)x_7≠0--x_7=0 40)x_4≠0 x_4≠0 39)x_7≠0--40)x_4≠0 41)x_4≠0 x_4≠0 39)x_7≠0--41)x_4≠0 40)x_4≠0--x_4=0 40)x_4≠0--41)x_4≠0 41)x_4≠0--x_4=0 42)x_7≠0 x_7≠0 42)x_7≠0--x_7=0 43)x_4≠0 x_4≠0 42)x_7≠0--43)x_4≠0 44)x_4≠0 x_4≠0 42)x_7≠0--44)x_4≠0 43)x_4≠0--x_4=0 43)x_4≠0--44)x_4≠0 44)x_4≠0--x_4=0 45)x_8≠1 x_8≠1 45)x_8≠1--x_8=1 46)x_4≠1 x_4≠1 45)x_8≠1--46)x_4≠1 47)x_7≠1 x_7≠1 45)x_8≠1--47)x_7≠1 46)x_4≠1--x_4=1 46)x_4≠1--47)x_7≠1 47)x_7≠1--x_7=1 48)x_8≠0 x_8≠0 48)x_8≠0--x_8=0 49)x_4≠0 x_4≠0 48)x_8≠0--49)x_4≠0 50)x_4≠0 x_4≠0 48)x_8≠0--50)x_4≠0 49)x_4≠0--x_4=0 49)x_4≠0--50)x_4≠0 50)x_4≠0--x_4=0 51)x_8≠0 x_8≠0 51)x_8≠0--x_8=0 52)x_7≠0 x_7≠0 51)x_8≠0--52)x_7≠0 53)x_7≠0 x_7≠0 51)x_8≠0--53)x_7≠0 52)x_7≠0--x_7=0 52)x_7≠0--53)x_7≠0 53)x_7≠0--x_7=0 54)x_9≠1 x_9≠1 54)x_9≠1--x_9=1 55)x_5≠1 x_5≠1 54)x_9≠1--55)x_5≠1 56)x_5≠1 x_5≠1 54)x_9≠1--56)x_5≠1 55)x_5≠1--x_5=1 55)x_5≠1--56)x_5≠1 56)x_5≠1--x_5=1 57)x_9≠0 x_9≠0 57)x_9≠0--x_9=0 58)x_5≠0 x_5≠0 57)x_9≠0--58)x_5≠0 59)x_5≠0 x_5≠0 57)x_9≠0--59)x_5≠0 58)x_5≠0--x_5=0 58)x_5≠0--59)x_5≠0 59)x_5≠0--x_5=0 60)x_9≠0 x_9≠0 60)x_9≠0--x_9=0 61)x_5≠0 x_5≠0 60)x_9≠0--61)x_5≠0 62)x_5≠0 x_5≠0 60)x_9≠0--62)x_5≠0 61)x_5≠0--x_5=0 61)x_5≠0--62)x_5≠0 62)x_5≠0--x_5=0 63)x_10≠1 x_10≠1 63)x_10≠1--x_10=1 64)x_9≠1 x_9≠1 63)x_10≠1--64)x_9≠1 65)x_8≠1 x_8≠1 63)x_10≠1--65)x_8≠1 64)x_9≠1--x_9=1 64)x_9≠1--65)x_8≠1 65)x_8≠1--x_8=1 66)x_10≠0 x_10≠0 66)x_10≠0--x_10=0 67)x_9≠0 x_9≠0 66)x_10≠0--67)x_9≠0 68)x_9≠0 x_9≠0 66)x_10≠0--68)x_9≠0 67)x_9≠0--x_9=0 67)x_9≠0--68)x_9≠0 68)x_9≠0--x_9=0 69)x_10≠0 x_10≠0 69)x_10≠0--x_10=0 70)x_8≠0 x_8≠0 69)x_10≠0--70)x_8≠0 71)x_8≠0 x_8≠0 69)x_10≠0--71)x_8≠0 70)x_8≠0--x_8=0 70)x_8≠0--71)x_8≠0 71)x_8≠0--x_8=0 72)x_11≠1 x_11≠1 72)x_11≠1--x_11=1 73)x_4≠1 x_4≠1 72)x_11≠1--73)x_4≠1 74)x_4≠1 x_4≠1 72)x_11≠1--74)x_4≠1 73)x_4≠1--x_4=1 73)x_4≠1--74)x_4≠1 74)x_4≠1--x_4=1 75)x_11≠0 x_11≠0 75)x_11≠0--x_11=0 76)x_4≠0 x_4≠0 75)x_11≠0--76)x_4≠0 77)x_4≠0 x_4≠0 75)x_11≠0--77)x_4≠0 76)x_4≠0--x_4=0 76)x_4≠0--77)x_4≠0 77)x_4≠0--x_4=0 78)x_11≠0 x_11≠0 78)x_11≠0--x_11=0 79)x_4≠0 x_4≠0 78)x_11≠0--79)x_4≠0 80)x_4≠0 x_4≠0 78)x_11≠0--80)x_4≠0 79)x_4≠0--x_4=0 79)x_4≠0--80)x_4≠0 80)x_4≠0--x_4=0 81)x_12≠1 x_12≠1 81)x_12≠1--x_12=1 82)x_11≠1 x_11≠1 81)x_12≠1--82)x_11≠1 83)x_11≠1 x_11≠1 81)x_12≠1--83)x_11≠1 82)x_11≠1--x_11=1 82)x_11≠1--83)x_11≠1 83)x_11≠1--x_11=1 84)x_12≠0 x_12≠0 84)x_12≠0--x_12=0 85)x_11≠0 x_11≠0 84)x_12≠0--85)x_11≠0 86)x_11≠0 x_11≠0 84)x_12≠0--86)x_11≠0 85)x_11≠0--x_11=0 85)x_11≠0--86)x_11≠0 86)x_11≠0--x_11=0 87)x_12≠0 x_12≠0 87)x_12≠0--x_12=0 88)x_11≠0 x_11≠0 87)x_12≠0--88)x_11≠0 89)x_11≠0 x_11≠0 87)x_12≠0--89)x_11≠0 88)x_11≠0--x_11=0 88)x_11≠0--89)x_11≠0 89)x_11≠0--x_11=0 90)x_13≠1 x_13≠1 90)x_13≠1--x_13=1 91)x_4≠1 x_4≠1 90)x_13≠1--91)x_4≠1 92)x_4≠1 x_4≠1 90)x_13≠1--92)x_4≠1 91)x_4≠1--x_4=1 91)x_4≠1--92)x_4≠1 92)x_4≠1--x_4=1 93)x_13≠0 x_13≠0 93)x_13≠0--x_13=0 94)x_4≠0 x_4≠0 93)x_13≠0--94)x_4≠0 95)x_4≠0 x_4≠0 93)x_13≠0--95)x_4≠0 94)x_4≠0--x_4=0 94)x_4≠0--95)x_4≠0 95)x_4≠0--x_4=0 96)x_13≠0 x_13≠0 96)x_13≠0--x_13=0 97)x_4≠0 x_4≠0 96)x_13≠0--97)x_4≠0 98)x_4≠0 x_4≠0 96)x_13≠0--98)x_4≠0 97)x_4≠0--x_4=0 97)x_4≠0--98)x_4≠0 98)x_4≠0--x_4=0 99)x_14≠1 x_14≠1 99)x_14≠1--x_14=1 100)x_4≠1 x_4≠1 99)x_14≠1--100)x_4≠1 101)x_13≠1 x_13≠1 99)x_14≠1--101)x_13≠1 100)x_4≠1--x_4=1 100)x_4≠1--101)x_13≠1 101)x_13≠1--x_13=1 102)x_14≠0 x_14≠0 102)x_14≠0--x_14=0 103)x_4≠0 x_4≠0 102)x_14≠0--103)x_4≠0 104)x_4≠0 x_4≠0 102)x_14≠0--104)x_4≠0 103)x_4≠0--x_4=0 103)x_4≠0--104)x_4≠0 104)x_4≠0--x_4=0 105)x_14≠0 x_14≠0 105)x_14≠0--x_14=0 106)x_13≠0 x_13≠0 105)x_14≠0--106)x_13≠0 107)x_13≠0 x_13≠0 105)x_14≠0--107)x_13≠0 106)x_13≠0--x_13=0 106)x_13≠0--107)x_13≠0 107)x_13≠0--x_13=0 108)x_15≠1 x_15≠1 108)x_15≠1--x_15=1 109)x_14≠1 x_14≠1 108)x_15≠1--109)x_14≠1 110)x_14≠1 x_14≠1 108)x_15≠1--110)x_14≠1 109)x_14≠1--x_14=1 109)x_14≠1--110)x_14≠1 110)x_14≠1--x_14=1 111)x_15≠0 x_15≠0 111)x_15≠0--x_15=0 112)x_14≠0 x_14≠0 111)x_15≠0--112)x_14≠0 113)x_14≠0 x_14≠0 111)x_15≠0--113)x_14≠0 112)x_14≠0--x_14=0 112)x_14≠0--113)x_14≠0 113)x_14≠0--x_14=0 114)x_15≠0 x_15≠0 114)x_15≠0--x_15=0 115)x_14≠0 x_14≠0 114)x_15≠0--115)x_14≠0 116)x_14≠0 x_14≠0 114)x_15≠0--116)x_14≠0 115)x_14≠0--x_14=0 115)x_14≠0--116)x_14≠0 116)x_14≠0--x_14=0 117)x_16≠1 x_16≠1 117)x_16≠1--x_16=1 118)x_10≠1 x_10≠1 117)x_16≠1--118)x_10≠1 119)x_10≠1 x_10≠1 117)x_16≠1--119)x_10≠1 118)x_10≠1--x_10=1 118)x_10≠1--119)x_10≠1 119)x_10≠1--x_10=1 120)x_16≠0 x_16≠0 120)x_16≠0--x_16=0 121)x_10≠0 x_10≠0 120)x_16≠0--121)x_10≠0 122)x_10≠0 x_10≠0 120)x_16≠0--122)x_10≠0 121)x_10≠0--x_10=0 121)x_10≠0--122)x_10≠0 122)x_10≠0--x_10=0 123)x_16≠0 x_16≠0 123)x_16≠0--x_16=0 124)x_10≠0 x_10≠0 123)x_16≠0--124)x_10≠0 125)x_10≠0 x_10≠0 123)x_16≠0--125)x_10≠0 124)x_10≠0--x_10=0 124)x_10≠0--125)x_10≠0 125)x_10≠0--x_10=0 126)x_17≠1 x_17≠1 126)x_17≠1--x_17=1 127)x_14≠1 x_14≠1 126)x_17≠1--127)x_14≠1 128)x_14≠1 x_14≠1 126)x_17≠1--128)x_14≠1 127)x_14≠1--x_14=1 127)x_14≠1--128)x_14≠1 128)x_14≠1--x_14=1 129)x_17≠0 x_17≠0 129)x_17≠0--x_17=0 130)x_14≠0 x_14≠0 129)x_17≠0--130)x_14≠0 131)x_14≠0 x_14≠0 129)x_17≠0--131)x_14≠0 130)x_14≠0--x_14=0 130)x_14≠0--131)x_14≠0 131)x_14≠0--x_14=0 132)x_17≠0 x_17≠0 132)x_17≠0--x_17=0 133)x_14≠0 x_14≠0 132)x_17≠0--133)x_14≠0 134)x_14≠0 x_14≠0 132)x_17≠0--134)x_14≠0 133)x_14≠0--x_14=0 133)x_14≠0--134)x_14≠0 134)x_14≠0--x_14=0 135)x_18≠1 x_18≠1 135)x_18≠1--x_18=1 136)x_14≠1 x_14≠1 135)x_18≠1--136)x_14≠1 137)x_17≠1 x_17≠1 135)x_18≠1--137)x_17≠1 136)x_14≠1--x_14=1 136)x_14≠1--137)x_17≠1 137)x_17≠1--x_17=1 138)x_18≠0 x_18≠0 138)x_18≠0--x_18=0 139)x_14≠0 x_14≠0 138)x_18≠0--139)x_14≠0 140)x_14≠0 x_14≠0 138)x_18≠0--140)x_14≠0 139)x_14≠0--x_14=0 139)x_14≠0--140)x_14≠0 140)x_14≠0--x_14=0 141)x_18≠0 x_18≠0 141)x_18≠0--x_18=0 142)x_17≠0 x_17≠0 141)x_18≠0--142)x_17≠0 143)x_17≠0 x_17≠0 141)x_18≠0--143)x_17≠0 142)x_17≠0--x_17=0 142)x_17≠0--143)x_17≠0 143)x_17≠0--x_17=0 144)x_19≠1 x_19≠1 144)x_19≠1--x_19=1 145)x_10≠1 x_10≠1 144)x_19≠1--145)x_10≠1 146)x_10≠1 x_10≠1 144)x_19≠1--146)x_10≠1 145)x_10≠1--x_10=1 145)x_10≠1--146)x_10≠1 146)x_10≠1--x_10=1 147)x_19≠0 x_19≠0 147)x_19≠0--x_19=0 148)x_10≠0 x_10≠0 147)x_19≠0--148)x_10≠0 149)x_10≠0 x_10≠0 147)x_19≠0--149)x_10≠0 148)x_10≠0--x_10=0 148)x_10≠0--149)x_10≠0 149)x_10≠0--x_10=0 150)x_19≠0 x_19≠0 150)x_19≠0--x_19=0 151)x_10≠0 x_10≠0 150)x_19≠0--151)x_10≠0 152)x_10≠0 x_10≠0 150)x_19≠0--152)x_10≠0 151)x_10≠0--x_10=0 151)x_10≠0--152)x_10≠0 152)x_10≠0--x_10=0 153)x_20≠1 x_20≠1 153)x_20≠1--x_20=1 154)x_19≠1 x_19≠1 153)x_20≠1--154)x_19≠1 155)x_18≠1 x_18≠1 153)x_20≠1--155)x_18≠1 154)x_19≠1--x_19=1 154)x_19≠1--155)x_18≠1 155)x_18≠1--x_18=1 156)x_20≠0 x_20≠0 156)x_20≠0--x_20=0 157)x_19≠0 x_19≠0 156)x_20≠0--157)x_19≠0 158)x_19≠0 x_19≠0 156)x_20≠0--158)x_19≠0 157)x_19≠0--x_19=0 157)x_19≠0--158)x_19≠0 158)x_19≠0--x_19=0 159)x_20≠0 x_20≠0 159)x_20≠0--x_20=0 160)x_18≠0 x_18≠0 159)x_20≠0--160)x_18≠0 161)x_18≠0 x_18≠0 159)x_20≠0--161)x_18≠0 160)x_18≠0--x_18=0 160)x_18≠0--161)x_18≠0 161)x_18≠0--x_18=0 162)x_21≠1 x_21≠1 162)x_21≠1--x_21=1 163)x_14≠1 x_14≠1 162)x_21≠1--163)x_14≠1 164)x_14≠1 x_14≠1 162)x_21≠1--164)x_14≠1 163)x_14≠1--x_14=1 163)x_14≠1--164)x_14≠1 164)x_14≠1--x_14=1 165)x_21≠0 x_21≠0 165)x_21≠0--x_21=0 166)x_14≠0 x_14≠0 165)x_21≠0--166)x_14≠0 167)x_14≠0 x_14≠0 165)x_21≠0--167)x_14≠0 166)x_14≠0--x_14=0 166)x_14≠0--167)x_14≠0 167)x_14≠0--x_14=0 168)x_21≠0 x_21≠0 168)x_21≠0--x_21=0 169)x_14≠0 x_14≠0 168)x_21≠0--169)x_14≠0 170)x_14≠0 x_14≠0 168)x_21≠0--170)x_14≠0 169)x_14≠0--x_14=0 169)x_14≠0--170)x_14≠0 170)x_14≠0--x_14=0 171)x_22≠1 x_22≠1 171)x_22≠1--x_22=1 172)x_21≠1 x_21≠1 171)x_22≠1--172)x_21≠1 173)x_21≠1 x_21≠1 171)x_22≠1--173)x_21≠1 172)x_21≠1--x_21=1 172)x_21≠1--173)x_21≠1 173)x_21≠1--x_21=1 174)x_22≠0 x_22≠0 174)x_22≠0--x_22=0 175)x_21≠0 x_21≠0 174)x_22≠0--175)x_21≠0 176)x_21≠0 x_21≠0 174)x_22≠0--176)x_21≠0 175)x_21≠0--x_21=0 175)x_21≠0--176)x_21≠0 176)x_21≠0--x_21=0 177)x_22≠0 x_22≠0 177)x_22≠0--x_22=0 178)x_21≠0 x_21≠0 177)x_22≠0--178)x_21≠0 179)x_21≠0 x_21≠0 177)x_22≠0--179)x_21≠0 178)x_21≠0--x_21=0 178)x_21≠0--179)x_21≠0 179)x_21≠0--x_21=0 180)x_23≠1 x_23≠1 180)x_23≠1--x_23=1 181)x_14≠1 x_14≠1 180)x_23≠1--181)x_14≠1 182)x_14≠1 x_14≠1 180)x_23≠1--182)x_14≠1 181)x_14≠1--x_14=1 181)x_14≠1--182)x_14≠1 182)x_14≠1--x_14=1 183)x_23≠0 x_23≠0 183)x_23≠0--x_23=0 184)x_14≠0 x_14≠0 183)x_23≠0--184)x_14≠0 185)x_14≠0 x_14≠0 183)x_23≠0--185)x_14≠0 184)x_14≠0--x_14=0 184)x_14≠0--185)x_14≠0 185)x_14≠0--x_14=0 186)x_23≠0 x_23≠0 186)x_23≠0--x_23=0 187)x_14≠0 x_14≠0 186)x_23≠0--187)x_14≠0 188)x_14≠0 x_14≠0 186)x_23≠0--188)x_14≠0 187)x_14≠0--x_14=0 187)x_14≠0--188)x_14≠0 188)x_14≠0--x_14=0 189)x_24≠1 x_24≠1 189)x_24≠1--x_24=1 190)x_14≠1 x_14≠1 189)x_24≠1--190)x_14≠1 191)x_23≠1 x_23≠1 189)x_24≠1--191)x_23≠1 190)x_14≠1--x_14=1 190)x_14≠1--191)x_23≠1 191)x_23≠1--x_23=1 192)x_24≠0 x_24≠0 192)x_24≠0--x_24=0 193)x_14≠0 x_14≠0 192)x_24≠0--193)x_14≠0 194)x_14≠0 x_14≠0 192)x_24≠0--194)x_14≠0 193)x_14≠0--x_14=0 193)x_14≠0--194)x_14≠0 194)x_14≠0--x_14=0 195)x_24≠0 x_24≠0 195)x_24≠0--x_24=0 196)x_23≠0 x_23≠0 195)x_24≠0--196)x_23≠0 197)x_23≠0 x_23≠0 195)x_24≠0--197)x_23≠0 196)x_23≠0--x_23=0 196)x_23≠0--197)x_23≠0 197)x_23≠0--x_23=0 198)x_25≠1 x_25≠1 198)x_25≠1--x_25=1 199)x_24≠1 x_24≠1 198)x_25≠1--199)x_24≠1 200)x_24≠1 x_24≠1 198)x_25≠1--200)x_24≠1 199)x_24≠1--x_24=1 199)x_24≠1--200)x_24≠1 200)x_24≠1--x_24=1 201)x_25≠0 x_25≠0 201)x_25≠0--x_25=0 202)x_24≠0 x_24≠0 201)x_25≠0--202)x_24≠0 203)x_24≠0 x_24≠0 201)x_25≠0--203)x_24≠0 202)x_24≠0--x_24=0 202)x_24≠0--203)x_24≠0 203)x_24≠0--x_24=0 204)x_25≠0 x_25≠0 204)x_25≠0--x_25=0 205)x_24≠0 x_24≠0 204)x_25≠0--205)x_24≠0 206)x_24≠0 x_24≠0 204)x_25≠0--206)x_24≠0 205)x_24≠0--x_24=0 205)x_24≠0--206)x_24≠0 206)x_24≠0--x_24=0 207)x_26≠1 x_26≠1 207)x_26≠1--x_26=1 208)x_20≠1 x_20≠1 207)x_26≠1--208)x_20≠1 209)x_20≠1 x_20≠1 207)x_26≠1--209)x_20≠1 208)x_20≠1--x_20=1 208)x_20≠1--209)x_20≠1 209)x_20≠1--x_20=1 210)x_26≠0 x_26≠0 210)x_26≠0--x_26=0 211)x_20≠0 x_20≠0 210)x_26≠0--211)x_20≠0 212)x_20≠0 x_20≠0 210)x_26≠0--212)x_20≠0 211)x_20≠0--x_20=0 211)x_20≠0--212)x_20≠0 212)x_20≠0--x_20=0 213)x_26≠0 x_26≠0 213)x_26≠0--x_26=0 214)x_20≠0 x_20≠0 213)x_26≠0--214)x_20≠0 215)x_20≠0 x_20≠0 213)x_26≠0--215)x_20≠0 214)x_20≠0--x_20=0 214)x_20≠0--215)x_20≠0 215)x_20≠0--x_20=0 216)x_27≠1 x_27≠1 216)x_27≠1--x_27=1 217)x_24≠1 x_24≠1 216)x_27≠1--217)x_24≠1 218)x_24≠1 x_24≠1 216)x_27≠1--218)x_24≠1 217)x_24≠1--x_24=1 217)x_24≠1--218)x_24≠1 218)x_24≠1--x_24=1 219)x_27≠0 x_27≠0 219)x_27≠0--x_27=0 220)x_24≠0 x_24≠0 219)x_27≠0--220)x_24≠0 221)x_24≠0 x_24≠0 219)x_27≠0--221)x_24≠0 220)x_24≠0--x_24=0 220)x_24≠0--221)x_24≠0 221)x_24≠0--x_24=0 222)x_27≠0 x_27≠0 222)x_27≠0--x_27=0 223)x_24≠0 x_24≠0 222)x_27≠0--223)x_24≠0 224)x_24≠0 x_24≠0 222)x_27≠0--224)x_24≠0 223)x_24≠0--x_24=0 223)x_24≠0--224)x_24≠0 224)x_24≠0--x_24=0 225)x_28≠1 x_28≠1 225)x_28≠1--x_28=1 226)x_24≠1 x_24≠1 225)x_28≠1--226)x_24≠1 227)x_27≠1 x_27≠1 225)x_28≠1--227)x_27≠1 226)x_24≠1--x_24=1 226)x_24≠1--227)x_27≠1 227)x_27≠1--x_27=1 228)x_28≠0 x_28≠0 228)x_28≠0--x_28=0 229)x_24≠0 x_24≠0 228)x_28≠0--229)x_24≠0 230)x_24≠0 x_24≠0 228)x_28≠0--230)x_24≠0 229)x_24≠0--x_24=0 229)x_24≠0--230)x_24≠0 230)x_24≠0--x_24=0 231)x_28≠0 x_28≠0 231)x_28≠0--x_28=0 232)x_27≠0 x_27≠0 231)x_28≠0--232)x_27≠0 233)x_27≠0 x_27≠0 231)x_28≠0--233)x_27≠0 232)x_27≠0--x_27=0 232)x_27≠0--233)x_27≠0 233)x_27≠0--x_27=0 234)x_29≠1 x_29≠1 234)x_29≠1--x_29=1 235)x_20≠1 x_20≠1 234)x_29≠1--235)x_20≠1 236)x_20≠1 x_20≠1 234)x_29≠1--236)x_20≠1 235)x_20≠1--x_20=1 235)x_20≠1--236)x_20≠1 236)x_20≠1--x_20=1 237)x_29≠0 x_29≠0 237)x_29≠0--x_29=0 238)x_20≠0 x_20≠0 237)x_29≠0--238)x_20≠0 239)x_20≠0 x_20≠0 237)x_29≠0--239)x_20≠0 238)x_20≠0--x_20=0 238)x_20≠0--239)x_20≠0 239)x_20≠0--x_20=0 240)x_29≠0 x_29≠0 240)x_29≠0--x_29=0 241)x_20≠0 x_20≠0 240)x_29≠0--241)x_20≠0 242)x_20≠0 x_20≠0 240)x_29≠0--242)x_20≠0 241)x_20≠0--x_20=0 241)x_20≠0--242)x_20≠0 242)x_20≠0--x_20=0 243)x_30≠1 x_30≠1 243)x_30≠1--x_30=1 244)x_29≠1 x_29≠1 243)x_30≠1--244)x_29≠1 245)x_28≠1 x_28≠1 243)x_30≠1--245)x_28≠1 244)x_29≠1--x_29=1 244)x_29≠1--245)x_28≠1 245)x_28≠1--x_28=1 246)x_30≠0 x_30≠0 246)x_30≠0--x_30=0 247)x_29≠0 x_29≠0 246)x_30≠0--247)x_29≠0 248)x_29≠0 x_29≠0 246)x_30≠0--248)x_29≠0 247)x_29≠0--x_29=0 247)x_29≠0--248)x_29≠0 248)x_29≠0--x_29=0 249)x_30≠0 x_30≠0 249)x_30≠0--x_30=0 250)x_28≠0 x_28≠0 249)x_30≠0--250)x_28≠0 251)x_28≠0 x_28≠0 249)x_30≠0--251)x_28≠0 250)x_28≠0--x_28=0 250)x_28≠0--251)x_28≠0 251)x_28≠0--x_28=0 252)x_31≠1 x_31≠1 252)x_31≠1--x_31=1 253)x_24≠1 x_24≠1 252)x_31≠1--253)x_24≠1 254)x_24≠1 x_24≠1 252)x_31≠1--254)x_24≠1 253)x_24≠1--x_24=1 253)x_24≠1--254)x_24≠1 254)x_24≠1--x_24=1 255)x_31≠0 x_31≠0 255)x_31≠0--x_31=0 256)x_24≠0 x_24≠0 255)x_31≠0--256)x_24≠0 257)x_24≠0 x_24≠0 255)x_31≠0--257)x_24≠0 256)x_24≠0--x_24=0 256)x_24≠0--257)x_24≠0 257)x_24≠0--x_24=0 258)x_31≠0 x_31≠0 258)x_31≠0--x_31=0 259)x_24≠0 x_24≠0 258)x_31≠0--259)x_24≠0 260)x_24≠0 x_24≠0 258)x_31≠0--260)x_24≠0 259)x_24≠0--x_24=0 259)x_24≠0--260)x_24≠0 260)x_24≠0--x_24=0 261)x_32≠1 x_32≠1 261)x_32≠1--x_32=1 262)x_31≠1 x_31≠1 261)x_32≠1--262)x_31≠1 263)x_31≠1 x_31≠1 261)x_32≠1--263)x_31≠1 262)x_31≠1--x_31=1 262)x_31≠1--263)x_31≠1 263)x_31≠1--x_31=1 264)x_32≠0 x_32≠0 264)x_32≠0--x_32=0 265)x_31≠0 x_31≠0 264)x_32≠0--265)x_31≠0 266)x_31≠0 x_31≠0 264)x_32≠0--266)x_31≠0 265)x_31≠0--x_31=0 265)x_31≠0--266)x_31≠0 266)x_31≠0--x_31=0 267)x_32≠0 x_32≠0 267)x_32≠0--x_32=0 268)x_31≠0 x_31≠0 267)x_32≠0--268)x_31≠0 269)x_31≠0 x_31≠0 267)x_32≠0--269)x_31≠0 268)x_31≠0--x_31=0 268)x_31≠0--269)x_31≠0 269)x_31≠0--x_31=0 270)x_33≠1 x_33≠1 270)x_33≠1--x_33=1 271)x_24≠1 x_24≠1 270)x_33≠1--271)x_24≠1 272)x_24≠1 x_24≠1 270)x_33≠1--272)x_24≠1 271)x_24≠1--x_24=1 271)x_24≠1--272)x_24≠1 272)x_24≠1--x_24=1 273)x_33≠0 x_33≠0 273)x_33≠0--x_33=0 274)x_24≠0 x_24≠0 273)x_33≠0--274)x_24≠0 275)x_24≠0 x_24≠0 273)x_33≠0--275)x_24≠0 274)x_24≠0--x_24=0 274)x_24≠0--275)x_24≠0 275)x_24≠0--x_24=0 276)x_33≠0 x_33≠0 276)x_33≠0--x_33=0 277)x_24≠0 x_24≠0 276)x_33≠0--277)x_24≠0 278)x_24≠0 x_24≠0 276)x_33≠0--278)x_24≠0 277)x_24≠0--x_24=0 277)x_24≠0--278)x_24≠0 278)x_24≠0--x_24=0 279)x_34≠1 x_34≠1 279)x_34≠1--x_34=1 280)x_24≠1 x_24≠1 279)x_34≠1--280)x_24≠1 281)x_33≠1 x_33≠1 279)x_34≠1--281)x_33≠1 280)x_24≠1--x_24=1 280)x_24≠1--281)x_33≠1 281)x_33≠1--x_33=1 282)x_34≠0 x_34≠0 282)x_34≠0--x_34=0 283)x_24≠0 x_24≠0 282)x_34≠0--283)x_24≠0 284)x_24≠0 x_24≠0 282)x_34≠0--284)x_24≠0 283)x_24≠0--x_24=0 283)x_24≠0--284)x_24≠0 284)x_24≠0--x_24=0 285)x_34≠0 x_34≠0 285)x_34≠0--x_34=0 286)x_33≠0 x_33≠0 285)x_34≠0--286)x_33≠0 287)x_33≠0 x_33≠0 285)x_34≠0--287)x_33≠0 286)x_33≠0--x_33=0 286)x_33≠0--287)x_33≠0 287)x_33≠0--x_33=0 288)x_35≠1 x_35≠1 288)x_35≠1--x_35=1 289)x_34≠1 x_34≠1 288)x_35≠1--289)x_34≠1 290)x_34≠1 x_34≠1 288)x_35≠1--290)x_34≠1 289)x_34≠1--x_34=1 289)x_34≠1--290)x_34≠1 290)x_34≠1--x_34=1 291)x_35≠0 x_35≠0 291)x_35≠0--x_35=0 292)x_34≠0 x_34≠0 291)x_35≠0--292)x_34≠0 293)x_34≠0 x_34≠0 291)x_35≠0--293)x_34≠0 292)x_34≠0--x_34=0 292)x_34≠0--293)x_34≠0 293)x_34≠0--x_34=0 294)x_35≠0 x_35≠0 294)x_35≠0--x_35=0 295)x_34≠0 x_34≠0 294)x_35≠0--295)x_34≠0 296)x_34≠0 x_34≠0 294)x_35≠0--296)x_34≠0 295)x_34≠0--x_34=0 295)x_34≠0--296)x_34≠0 296)x_34≠0--x_34=0 297)x_36≠1 x_36≠1 297)x_36≠1--x_36=1 298)x_30≠1 x_30≠1 297)x_36≠1--298)x_30≠1 299)x_30≠1 x_30≠1 297)x_36≠1--299)x_30≠1 298)x_30≠1--x_30=1 298)x_30≠1--299)x_30≠1 299)x_30≠1--x_30=1 300)x_36≠0 x_36≠0 300)x_36≠0--x_36=0 301)x_30≠0 x_30≠0 300)x_36≠0--301)x_30≠0 302)x_30≠0 x_30≠0 300)x_36≠0--302)x_30≠0 301)x_30≠0--x_30=0 301)x_30≠0--302)x_30≠0 302)x_30≠0--x_30=0 303)x_36≠0 x_36≠0 303)x_36≠0--x_36=0 304)x_30≠0 x_30≠0 303)x_36≠0--304)x_30≠0 305)x_30≠0 x_30≠0 303)x_36≠0--305)x_30≠0 304)x_30≠0--x_30=0 304)x_30≠0--305)x_30≠0 305)x_30≠0--x_30=0 306)x_37≠1 x_37≠1 306)x_37≠1--x_37=1 307)x_34≠1 x_34≠1 306)x_37≠1--307)x_34≠1 308)x_34≠1 x_34≠1 306)x_37≠1--308)x_34≠1 307)x_34≠1--x_34=1 307)x_34≠1--308)x_34≠1 308)x_34≠1--x_34=1 309)x_37≠0 x_37≠0 309)x_37≠0--x_37=0 310)x_34≠0 x_34≠0 309)x_37≠0--310)x_34≠0 311)x_34≠0 x_34≠0 309)x_37≠0--311)x_34≠0 310)x_34≠0--x_34=0 310)x_34≠0--311)x_34≠0 311)x_34≠0--x_34=0 312)x_37≠0 x_37≠0 312)x_37≠0--x_37=0 313)x_34≠0 x_34≠0 312)x_37≠0--313)x_34≠0 314)x_34≠0 x_34≠0 312)x_37≠0--314)x_34≠0 313)x_34≠0--x_34=0 313)x_34≠0--314)x_34≠0 314)x_34≠0--x_34=0 315)x_38≠1 x_38≠1 315)x_38≠1--x_38=1 316)x_34≠1 x_34≠1 315)x_38≠1--316)x_34≠1 317)x_37≠1 x_37≠1 315)x_38≠1--317)x_37≠1 316)x_34≠1--x_34=1 316)x_34≠1--317)x_37≠1 317)x_37≠1--x_37=1 318)x_38≠0 x_38≠0 318)x_38≠0--x_38=0 319)x_34≠0 x_34≠0 318)x_38≠0--319)x_34≠0 320)x_34≠0 x_34≠0 318)x_38≠0--320)x_34≠0 319)x_34≠0--x_34=0 319)x_34≠0--320)x_34≠0 320)x_34≠0--x_34=0 321)x_38≠0 x_38≠0 321)x_38≠0--x_38=0 322)x_37≠0 x_37≠0 321)x_38≠0--322)x_37≠0 323)x_37≠0 x_37≠0 321)x_38≠0--323)x_37≠0 322)x_37≠0--x_37=0 322)x_37≠0--323)x_37≠0 323)x_37≠0--x_37=0 324)x_39≠1 x_39≠1 324)x_39≠1--x_39=1 325)x_30≠1 x_30≠1 324)x_39≠1--325)x_30≠1 326)x_30≠1 x_30≠1 324)x_39≠1--326)x_30≠1 325)x_30≠1--x_30=1 325)x_30≠1--326)x_30≠1 326)x_30≠1--x_30=1 327)x_39≠0 x_39≠0 327)x_39≠0--x_39=0 328)x_30≠0 x_30≠0 327)x_39≠0--328)x_30≠0 329)x_30≠0 x_30≠0 327)x_39≠0--329)x_30≠0 328)x_30≠0--x_30=0 328)x_30≠0--329)x_30≠0 329)x_30≠0--x_30=0 330)x_39≠0 x_39≠0 330)x_39≠0--x_39=0 331)x_30≠0 x_30≠0 330)x_39≠0--331)x_30≠0 332)x_30≠0 x_30≠0 330)x_39≠0--332)x_30≠0 331)x_30≠0--x_30=0 331)x_30≠0--332)x_30≠0 332)x_30≠0--x_30=0 333)x_40≠1 x_40≠1 333)x_40≠1--x_40=1 334)x_39≠1 x_39≠1 333)x_40≠1--334)x_39≠1 335)x_38≠1 x_38≠1 333)x_40≠1--335)x_38≠1 334)x_39≠1--x_39=1 334)x_39≠1--335)x_38≠1 335)x_38≠1--x_38=1 336)x_40≠0 x_40≠0 336)x_40≠0--x_40=0 337)x_39≠0 x_39≠0 336)x_40≠0--337)x_39≠0 338)x_39≠0 x_39≠0 336)x_40≠0--338)x_39≠0 337)x_39≠0--x_39=0 337)x_39≠0--338)x_39≠0 338)x_39≠0--x_39=0 339)x_40≠0 x_40≠0 339)x_40≠0--x_40=0 340)x_38≠0 x_38≠0 339)x_40≠0--340)x_38≠0 341)x_38≠0 x_38≠0 339)x_40≠0--341)x_38≠0 340)x_38≠0--x_38=0 340)x_38≠0--341)x_38≠0 341)x_38≠0--x_38=0 342)x_41≠1 x_41≠1 342)x_41≠1--x_41=1 343)x_34≠1 x_34≠1 342)x_41≠1--343)x_34≠1 344)x_34≠1 x_34≠1 342)x_41≠1--344)x_34≠1 343)x_34≠1--x_34=1 343)x_34≠1--344)x_34≠1 344)x_34≠1--x_34=1 345)x_41≠0 x_41≠0 345)x_41≠0--x_41=0 346)x_34≠0 x_34≠0 345)x_41≠0--346)x_34≠0 347)x_34≠0 x_34≠0 345)x_41≠0--347)x_34≠0 346)x_34≠0--x_34=0 346)x_34≠0--347)x_34≠0 347)x_34≠0--x_34=0 348)x_41≠0 x_41≠0 348)x_41≠0--x_41=0 349)x_34≠0 x_34≠0 348)x_41≠0--349)x_34≠0 350)x_34≠0 x_34≠0 348)x_41≠0--350)x_34≠0 349)x_34≠0--x_34=0 349)x_34≠0--350)x_34≠0 350)x_34≠0--x_34=0 351)x_42≠1 x_42≠1 351)x_42≠1--x_42=1 352)x_41≠1 x_41≠1 351)x_42≠1--352)x_41≠1 353)x_41≠1 x_41≠1 351)x_42≠1--353)x_41≠1 352)x_41≠1--x_41=1 352)x_41≠1--353)x_41≠1 353)x_41≠1--x_41=1 354)x_42≠0 x_42≠0 354)x_42≠0--x_42=0 355)x_41≠0 x_41≠0 354)x_42≠0--355)x_41≠0 356)x_41≠0 x_41≠0 354)x_42≠0--356)x_41≠0 355)x_41≠0--x_41=0 355)x_41≠0--356)x_41≠0 356)x_41≠0--x_41=0 357)x_42≠0 x_42≠0 357)x_42≠0--x_42=0 358)x_41≠0 x_41≠0 357)x_42≠0--358)x_41≠0 359)x_41≠0 x_41≠0 357)x_42≠0--359)x_41≠0 358)x_41≠0--x_41=0 358)x_41≠0--359)x_41≠0 359)x_41≠0--x_41=0 360)x_43≠1 x_43≠1 360)x_43≠1--x_43=1 361)x_34≠1 x_34≠1 360)x_43≠1--361)x_34≠1 362)x_34≠1 x_34≠1 360)x_43≠1--362)x_34≠1 361)x_34≠1--x_34=1 361)x_34≠1--362)x_34≠1 362)x_34≠1--x_34=1 363)x_43≠0 x_43≠0 363)x_43≠0--x_43=0 364)x_34≠0 x_34≠0 363)x_43≠0--364)x_34≠0 365)x_34≠0 x_34≠0 363)x_43≠0--365)x_34≠0 364)x_34≠0--x_34=0 364)x_34≠0--365)x_34≠0 365)x_34≠0--x_34=0 366)x_43≠0 x_43≠0 366)x_43≠0--x_43=0 367)x_34≠0 x_34≠0 366)x_43≠0--367)x_34≠0 368)x_34≠0 x_34≠0 366)x_43≠0--368)x_34≠0 367)x_34≠0--x_34=0 367)x_34≠0--368)x_34≠0 368)x_34≠0--x_34=0 369)x_44≠1 x_44≠1 369)x_44≠1--x_44=1 370)x_34≠1 x_34≠1 369)x_44≠1--370)x_34≠1 371)x_43≠1 x_43≠1 369)x_44≠1--371)x_43≠1 370)x_34≠1--x_34=1 370)x_34≠1--371)x_43≠1 371)x_43≠1--x_43=1 372)x_44≠0 x_44≠0 372)x_44≠0--x_44=0 373)x_34≠0 x_34≠0 372)x_44≠0--373)x_34≠0 374)x_34≠0 x_34≠0 372)x_44≠0--374)x_34≠0 373)x_34≠0--x_34=0 373)x_34≠0--374)x_34≠0 374)x_34≠0--x_34=0 375)x_44≠0 x_44≠0 375)x_44≠0--x_44=0 376)x_43≠0 x_43≠0 375)x_44≠0--376)x_43≠0 377)x_43≠0 x_43≠0 375)x_44≠0--377)x_43≠0 376)x_43≠0--x_43=0 376)x_43≠0--377)x_43≠0 377)x_43≠0--x_43=0 378)x_45≠1 x_45≠1 378)x_45≠1--x_45=1 379)x_44≠1 x_44≠1 378)x_45≠1--379)x_44≠1 380)x_44≠1 x_44≠1 378)x_45≠1--380)x_44≠1 379)x_44≠1--x_44=1 379)x_44≠1--380)x_44≠1 380)x_44≠1--x_44=1 381)x_45≠0 x_45≠0 381)x_45≠0--x_45=0 382)x_44≠0 x_44≠0 381)x_45≠0--382)x_44≠0 383)x_44≠0 x_44≠0 381)x_45≠0--383)x_44≠0 382)x_44≠0--x_44=0 382)x_44≠0--383)x_44≠0 383)x_44≠0--x_44=0 384)x_45≠0 x_45≠0 384)x_45≠0--x_45=0 385)x_44≠0 x_44≠0 384)x_45≠0--385)x_44≠0 386)x_44≠0 x_44≠0 384)x_45≠0--386)x_44≠0 385)x_44≠0--x_44=0 385)x_44≠0--386)x_44≠0 386)x_44≠0--x_44=0 387)x_46≠1 x_46≠1 387)x_46≠1--x_46=1 388)x_40≠1 x_40≠1 387)x_46≠1--388)x_40≠1 389)x_40≠1 x_40≠1 387)x_46≠1--389)x_40≠1 388)x_40≠1--x_40=1 388)x_40≠1--389)x_40≠1 389)x_40≠1--x_40=1 390)x_46≠0 x_46≠0 390)x_46≠0--x_46=0 391)x_40≠0 x_40≠0 390)x_46≠0--391)x_40≠0 392)x_40≠0 x_40≠0 390)x_46≠0--392)x_40≠0 391)x_40≠0--x_40=0 391)x_40≠0--392)x_40≠0 392)x_40≠0--x_40=0 393)x_46≠0 x_46≠0 393)x_46≠0--x_46=0 394)x_40≠0 x_40≠0 393)x_46≠0--394)x_40≠0 395)x_40≠0 x_40≠0 393)x_46≠0--395)x_40≠0 394)x_40≠0--x_40=0 394)x_40≠0--395)x_40≠0 395)x_40≠0--x_40=0 396)x_47≠1 x_47≠1 396)x_47≠1--x_47=1 397)x_0≠1 x_0≠1 396)x_47≠1--397)x_0≠1 398)x_0≠1 x_0≠1 396)x_47≠1--398)x_0≠1 397)x_0≠1--x_0=1 397)x_0≠1--398)x_0≠1 398)x_0≠1--x_0=1 399)x_47≠0 x_47≠0 399)x_47≠0--x_47=0 400)x_0≠0 x_0≠0 399)x_47≠0--400)x_0≠0 401)x_0≠0 x_0≠0 399)x_47≠0--401)x_0≠0 400)x_0≠0--x_0=0 400)x_0≠0--401)x_0≠0 401)x_0≠0--x_0=0 402)x_47≠0 x_47≠0 402)x_47≠0--x_47=0 403)x_0≠0 x_0≠0 402)x_47≠0--403)x_0≠0 404)x_0≠0 x_0≠0 402)x_47≠0--404)x_0≠0 403)x_0≠0--x_0=0 403)x_0≠0--404)x_0≠0 404)x_0≠0--x_0=0 405)x_48≠1 x_48≠1 405)x_48≠1--x_48=1 406)x_44≠1 x_44≠1 405)x_48≠1--406)x_44≠1 407)x_47≠1 x_47≠1 405)x_48≠1--407)x_47≠1 406)x_44≠1--x_44=1 406)x_44≠1--407)x_47≠1 407)x_47≠1--x_47=1 408)x_48≠0 x_48≠0 408)x_48≠0--x_48=0 409)x_44≠0 x_44≠0 408)x_48≠0--409)x_44≠0 410)x_44≠0 x_44≠0 408)x_48≠0--410)x_44≠0 409)x_44≠0--x_44=0 409)x_44≠0--410)x_44≠0 410)x_44≠0--x_44=0 411)x_48≠0 x_48≠0 411)x_48≠0--x_48=0 412)x_47≠0 x_47≠0 411)x_48≠0--412)x_47≠0 413)x_47≠0 x_47≠0 411)x_48≠0--413)x_47≠0 412)x_47≠0--x_47=0 412)x_47≠0--413)x_47≠0 413)x_47≠0--x_47=0 414)x_49≠1 x_49≠1 414)x_49≠1--x_49=1 415)x_40≠1 x_40≠1 414)x_49≠1--415)x_40≠1 416)x_40≠1 x_40≠1 414)x_49≠1--416)x_40≠1 415)x_40≠1--x_40=1 415)x_40≠1--416)x_40≠1 416)x_40≠1--x_40=1 417)x_49≠0 x_49≠0 417)x_49≠0--x_49=0 418)x_40≠0 x_40≠0 417)x_49≠0--418)x_40≠0 419)x_40≠0 x_40≠0 417)x_49≠0--419)x_40≠0 418)x_40≠0--x_40=0 418)x_40≠0--419)x_40≠0 419)x_40≠0--x_40=0 420)x_49≠0 x_49≠0 420)x_49≠0--x_49=0 421)x_40≠0 x_40≠0 420)x_49≠0--421)x_40≠0 422)x_40≠0 x_40≠0 420)x_49≠0--422)x_40≠0 421)x_40≠0--x_40=0 421)x_40≠0--422)x_40≠0 422)x_40≠0--x_40=0 423)x_50≠1 x_50≠1 423)x_50≠1--x_50=1 424)x_49≠1 x_49≠1 423)x_50≠1--424)x_49≠1 425)x_48≠1 x_48≠1 423)x_50≠1--425)x_48≠1 424)x_49≠1--x_49=1 424)x_49≠1--425)x_48≠1 425)x_48≠1--x_48=1 426)x_50≠0 x_50≠0 426)x_50≠0--x_50=0 427)x_49≠0 x_49≠0 426)x_50≠0--427)x_49≠0 428)x_49≠0 x_49≠0 426)x_50≠0--428)x_49≠0 427)x_49≠0--x_49=0 427)x_49≠0--428)x_49≠0 428)x_49≠0--x_49=0 429)x_50≠0 x_50≠0 429)x_50≠0--x_50=0 430)x_48≠0 x_48≠0 429)x_50≠0--430)x_48≠0 431)x_48≠0 x_48≠0 429)x_50≠0--431)x_48≠0 430)x_48≠0--x_48=0 430)x_48≠0--431)x_48≠0 431)x_48≠0--x_48=0 432)x_51≠1 x_51≠1 432)x_51≠1--x_51=1 433)x_44≠1 x_44≠1 432)x_51≠1--433)x_44≠1 434)x_44≠1 x_44≠1 432)x_51≠1--434)x_44≠1 433)x_44≠1--x_44=1 433)x_44≠1--434)x_44≠1 434)x_44≠1--x_44=1 435)x_51≠0 x_51≠0 435)x_51≠0--x_51=0 436)x_44≠0 x_44≠0 435)x_51≠0--436)x_44≠0 437)x_44≠0 x_44≠0 435)x_51≠0--437)x_44≠0 436)x_44≠0--x_44=0 436)x_44≠0--437)x_44≠0 437)x_44≠0--x_44=0 438)x_51≠0 x_51≠0 438)x_51≠0--x_51=0 439)x_44≠0 x_44≠0 438)x_51≠0--439)x_44≠0 440)x_44≠0 x_44≠0 438)x_51≠0--440)x_44≠0 439)x_44≠0--x_44=0 439)x_44≠0--440)x_44≠0 440)x_44≠0--x_44=0 441)x_52≠1 x_52≠1 441)x_52≠1--x_52=1 442)x_51≠1 x_51≠1 441)x_52≠1--442)x_51≠1 443)x_51≠1 x_51≠1 441)x_52≠1--443)x_51≠1 442)x_51≠1--x_51=1 442)x_51≠1--443)x_51≠1 443)x_51≠1--x_51=1 444)x_52≠0 x_52≠0 444)x_52≠0--x_52=0 445)x_51≠0 x_51≠0 444)x_52≠0--445)x_51≠0 446)x_51≠0 x_51≠0 444)x_52≠0--446)x_51≠0 445)x_51≠0--x_51=0 445)x_51≠0--446)x_51≠0 446)x_51≠0--x_51=0 447)x_52≠0 x_52≠0 447)x_52≠0--x_52=0 448)x_51≠0 x_51≠0 447)x_52≠0--448)x_51≠0 449)x_51≠0 x_51≠0 447)x_52≠0--449)x_51≠0 448)x_51≠0--x_51=0 448)x_51≠0--449)x_51≠0 449)x_51≠0--x_51=0 450)x_53≠1 x_53≠1 450)x_53≠1--x_53=1 451)x_44≠1 x_44≠1 450)x_53≠1--451)x_44≠1 452)x_44≠1 x_44≠1 450)x_53≠1--452)x_44≠1 451)x_44≠1--x_44=1 451)x_44≠1--452)x_44≠1 452)x_44≠1--x_44=1 453)x_53≠0 x_53≠0 453)x_53≠0--x_53=0 454)x_44≠0 x_44≠0 453)x_53≠0--454)x_44≠0 455)x_44≠0 x_44≠0 453)x_53≠0--455)x_44≠0 454)x_44≠0--x_44=0 454)x_44≠0--455)x_44≠0 455)x_44≠0--x_44=0 456)x_53≠0 x_53≠0 456)x_53≠0--x_53=0 457)x_44≠0 x_44≠0 456)x_53≠0--457)x_44≠0 458)x_44≠0 x_44≠0 456)x_53≠0--458)x_44≠0 457)x_44≠0--x_44=0 457)x_44≠0--458)x_44≠0 458)x_44≠0--x_44=0 459)x_54≠1 x_54≠1 459)x_54≠1--x_54=1 460)x_44≠1 x_44≠1 459)x_54≠1--460)x_44≠1 461)x_53≠1 x_53≠1 459)x_54≠1--461)x_53≠1 460)x_44≠1--x_44=1 460)x_44≠1--461)x_53≠1 461)x_53≠1--x_53=1 462)x_54≠0 x_54≠0 462)x_54≠0--x_54=0 463)x_44≠0 x_44≠0 462)x_54≠0--463)x_44≠0 464)x_44≠0 x_44≠0 462)x_54≠0--464)x_44≠0 463)x_44≠0--x_44=0 463)x_44≠0--464)x_44≠0 464)x_44≠0--x_44=0 465)x_54≠0 x_54≠0 465)x_54≠0--x_54=0 466)x_53≠0 x_53≠0 465)x_54≠0--466)x_53≠0 467)x_53≠0 x_53≠0 465)x_54≠0--467)x_53≠0 466)x_53≠0--x_53=0 466)x_53≠0--467)x_53≠0 467)x_53≠0--x_53=0 468)x_55≠1 x_55≠1 468)x_55≠1--x_55=1 469)x_54≠1 x_54≠1 468)x_55≠1--469)x_54≠1 470)x_54≠1 x_54≠1 468)x_55≠1--470)x_54≠1 469)x_54≠1--x_54=1 469)x_54≠1--470)x_54≠1 470)x_54≠1--x_54=1 471)x_55≠0 x_55≠0 471)x_55≠0--x_55=0 472)x_54≠0 x_54≠0 471)x_55≠0--472)x_54≠0 473)x_54≠0 x_54≠0 471)x_55≠0--473)x_54≠0 472)x_54≠0--x_54=0 472)x_54≠0--473)x_54≠0 473)x_54≠0--x_54=0 474)x_55≠0 x_55≠0 474)x_55≠0--x_55=0 475)x_54≠0 x_54≠0 474)x_55≠0--475)x_54≠0 476)x_54≠0 x_54≠0 474)x_55≠0--476)x_54≠0 475)x_54≠0--x_54=0 475)x_54≠0--476)x_54≠0 476)x_54≠0--x_54=0 477)x_56≠1 x_56≠1 477)x_56≠1--x_56=1 478)x_50≠1 x_50≠1 477)x_56≠1--478)x_50≠1 479)x_50≠1 x_50≠1 477)x_56≠1--479)x_50≠1 478)x_50≠1--x_50=1 478)x_50≠1--479)x_50≠1 479)x_50≠1--x_50=1 480)x_56≠0 x_56≠0 480)x_56≠0--x_56=0 481)x_50≠0 x_50≠0 480)x_56≠0--481)x_50≠0 482)x_50≠0 x_50≠0 480)x_56≠0--482)x_50≠0 481)x_50≠0--x_50=0 481)x_50≠0--482)x_50≠0 482)x_50≠0--x_50=0 483)x_56≠0 x_56≠0 483)x_56≠0--x_56=0 484)x_50≠0 x_50≠0 483)x_56≠0--484)x_50≠0 485)x_50≠0 x_50≠0 483)x_56≠0--485)x_50≠0 484)x_50≠0--x_50=0 484)x_50≠0--485)x_50≠0 485)x_50≠0--x_50=0 486)x_57≠1 x_57≠1 486)x_57≠1--x_57=1 487)x_54≠1 x_54≠1 486)x_57≠1--487)x_54≠1 488)x_54≠1 x_54≠1 486)x_57≠1--488)x_54≠1 487)x_54≠1--x_54=1 487)x_54≠1--488)x_54≠1 488)x_54≠1--x_54=1 489)x_57≠0 x_57≠0 489)x_57≠0--x_57=0 490)x_54≠0 x_54≠0 489)x_57≠0--490)x_54≠0 491)x_54≠0 x_54≠0 489)x_57≠0--491)x_54≠0 490)x_54≠0--x_54=0 490)x_54≠0--491)x_54≠0 491)x_54≠0--x_54=0 492)x_57≠0 x_57≠0 492)x_57≠0--x_57=0 493)x_54≠0 x_54≠0 492)x_57≠0--493)x_54≠0 494)x_54≠0 x_54≠0 492)x_57≠0--494)x_54≠0 493)x_54≠0--x_54=0 493)x_54≠0--494)x_54≠0 494)x_54≠0--x_54=0 495)x_58≠1 x_58≠1 495)x_58≠1--x_58=1 496)x_54≠1 x_54≠1 495)x_58≠1--496)x_54≠1 497)x_57≠1 x_57≠1 495)x_58≠1--497)x_57≠1 496)x_54≠1--x_54=1 496)x_54≠1--497)x_57≠1 497)x_57≠1--x_57=1 498)x_58≠0 x_58≠0 498)x_58≠0--x_58=0 499)x_54≠0 x_54≠0 498)x_58≠0--499)x_54≠0 500)x_54≠0 x_54≠0 498)x_58≠0--500)x_54≠0 499)x_54≠0--x_54=0 499)x_54≠0--500)x_54≠0 500)x_54≠0--x_54=0 501)x_58≠0 x_58≠0 501)x_58≠0--x_58=0 502)x_57≠0 x_57≠0 501)x_58≠0--502)x_57≠0 503)x_57≠0 x_57≠0 501)x_58≠0--503)x_57≠0 502)x_57≠0--x_57=0 502)x_57≠0--503)x_57≠0 503)x_57≠0--x_57=0 504)x_59≠1 x_59≠1 504)x_59≠1--x_59=1 505)x_50≠1 x_50≠1 504)x_59≠1--505)x_50≠1 506)x_50≠1 x_50≠1 504)x_59≠1--506)x_50≠1 505)x_50≠1--x_50=1 505)x_50≠1--506)x_50≠1 506)x_50≠1--x_50=1 507)x_59≠0 x_59≠0 507)x_59≠0--x_59=0 508)x_50≠0 x_50≠0 507)x_59≠0--508)x_50≠0 509)x_50≠0 x_50≠0 507)x_59≠0--509)x_50≠0 508)x_50≠0--x_50=0 508)x_50≠0--509)x_50≠0 509)x_50≠0--x_50=0 510)x_59≠0 x_59≠0 510)x_59≠0--x_59=0 511)x_50≠0 x_50≠0 510)x_59≠0--511)x_50≠0 512)x_50≠0 x_50≠0 510)x_59≠0--512)x_50≠0 511)x_50≠0--x_50=0 511)x_50≠0--512)x_50≠0 512)x_50≠0--x_50=0 513)x_60≠1 x_60≠1 513)x_60≠1--x_60=1 514)x_59≠1 x_59≠1 513)x_60≠1--514)x_59≠1 515)x_58≠1 x_58≠1 513)x_60≠1--515)x_58≠1 514)x_59≠1--x_59=1 514)x_59≠1--515)x_58≠1 515)x_58≠1--x_58=1 516)x_60≠0 x_60≠0 516)x_60≠0--x_60=0 517)x_59≠0 x_59≠0 516)x_60≠0--517)x_59≠0 518)x_59≠0 x_59≠0 516)x_60≠0--518)x_59≠0 517)x_59≠0--x_59=0 517)x_59≠0--518)x_59≠0 518)x_59≠0--x_59=0 519)x_60≠0 x_60≠0 519)x_60≠0--x_60=0 520)x_58≠0 x_58≠0 519)x_60≠0--520)x_58≠0 521)x_58≠0 x_58≠0 519)x_60≠0--521)x_58≠0 520)x_58≠0--x_58=0 520)x_58≠0--521)x_58≠0 521)x_58≠0--x_58=0 522)x_61≠1 x_61≠1 522)x_61≠1--x_61=1 523)x_54≠1 x_54≠1 522)x_61≠1--523)x_54≠1 524)x_54≠1 x_54≠1 522)x_61≠1--524)x_54≠1 523)x_54≠1--x_54=1 523)x_54≠1--524)x_54≠1 524)x_54≠1--x_54=1 525)x_61≠0 x_61≠0 525)x_61≠0--x_61=0 526)x_54≠0 x_54≠0 525)x_61≠0--526)x_54≠0 527)x_54≠0 x_54≠0 525)x_61≠0--527)x_54≠0 526)x_54≠0--x_54=0 526)x_54≠0--527)x_54≠0 527)x_54≠0--x_54=0 528)x_61≠0 x_61≠0 528)x_61≠0--x_61=0 529)x_54≠0 x_54≠0 528)x_61≠0--529)x_54≠0 530)x_54≠0 x_54≠0 528)x_61≠0--530)x_54≠0 529)x_54≠0--x_54=0 529)x_54≠0--530)x_54≠0 530)x_54≠0--x_54=0 531)x_62≠1 x_62≠1 531)x_62≠1--x_62=1 532)x_61≠1 x_61≠1 531)x_62≠1--532)x_61≠1 533)x_61≠1 x_61≠1 531)x_62≠1--533)x_61≠1 532)x_61≠1--x_61=1 532)x_61≠1--533)x_61≠1 533)x_61≠1--x_61=1 534)x_62≠0 x_62≠0 534)x_62≠0--x_62=0 535)x_61≠0 x_61≠0 534)x_62≠0--535)x_61≠0 536)x_61≠0 x_61≠0 534)x_62≠0--536)x_61≠0 535)x_61≠0--x_61=0 535)x_61≠0--536)x_61≠0 536)x_61≠0--x_61=0 537)x_62≠0 x_62≠0 537)x_62≠0--x_62=0 538)x_61≠0 x_61≠0 537)x_62≠0--538)x_61≠0 539)x_61≠0 x_61≠0 537)x_62≠0--539)x_61≠0 538)x_61≠0--x_61=0 538)x_61≠0--539)x_61≠0 539)x_61≠0--x_61=0 540)x_63≠1 x_63≠1 540)x_63≠1--x_63=1 541)x_54≠1 x_54≠1 540)x_63≠1--541)x_54≠1 542)x_54≠1 x_54≠1 540)x_63≠1--542)x_54≠1 541)x_54≠1--x_54=1 541)x_54≠1--542)x_54≠1 542)x_54≠1--x_54=1 543)x_63≠0 x_63≠0 543)x_63≠0--x_63=0 544)x_54≠0 x_54≠0 543)x_63≠0--544)x_54≠0 545)x_54≠0 x_54≠0 543)x_63≠0--545)x_54≠0 544)x_54≠0--x_54=0 544)x_54≠0--545)x_54≠0 545)x_54≠0--x_54=0 546)x_63≠0 x_63≠0 546)x_63≠0--x_63=0 547)x_54≠0 x_54≠0 546)x_63≠0--547)x_54≠0 548)x_54≠0 x_54≠0 546)x_63≠0--548)x_54≠0 547)x_54≠0--x_54=0 547)x_54≠0--548)x_54≠0 548)x_54≠0--x_54=0 549)x_64≠1 x_64≠1 549)x_64≠1--x_64=1 550)x_54≠1 x_54≠1 549)x_64≠1--550)x_54≠1 551)x_63≠1 x_63≠1 549)x_64≠1--551)x_63≠1 550)x_54≠1--x_54=1 550)x_54≠1--551)x_63≠1 551)x_63≠1--x_63=1 552)x_64≠0 x_64≠0 552)x_64≠0--x_64=0 553)x_54≠0 x_54≠0 552)x_64≠0--553)x_54≠0 554)x_54≠0 x_54≠0 552)x_64≠0--554)x_54≠0 553)x_54≠0--x_54=0 553)x_54≠0--554)x_54≠0 554)x_54≠0--x_54=0 555)x_64≠0 x_64≠0 555)x_64≠0--x_64=0 556)x_63≠0 x_63≠0 555)x_64≠0--556)x_63≠0 557)x_63≠0 x_63≠0 555)x_64≠0--557)x_63≠0 556)x_63≠0--x_63=0 556)x_63≠0--557)x_63≠0 557)x_63≠0--x_63=0 558)x_65≠1 x_65≠1 558)x_65≠1--x_65=1 559)x_64≠1 x_64≠1 558)x_65≠1--559)x_64≠1 560)x_64≠1 x_64≠1 558)x_65≠1--560)x_64≠1 559)x_64≠1--x_64=1 559)x_64≠1--560)x_64≠1 560)x_64≠1--x_64=1 561)x_65≠0 x_65≠0 561)x_65≠0--x_65=0 562)x_64≠0 x_64≠0 561)x_65≠0--562)x_64≠0 563)x_64≠0 x_64≠0 561)x_65≠0--563)x_64≠0 562)x_64≠0--x_64=0 562)x_64≠0--563)x_64≠0 563)x_64≠0--x_64=0 564)x_65≠0 x_65≠0 564)x_65≠0--x_65=0 565)x_64≠0 x_64≠0 564)x_65≠0--565)x_64≠0 566)x_64≠0 x_64≠0 564)x_65≠0--566)x_64≠0 565)x_64≠0--x_64=0 565)x_64≠0--566)x_64≠0 566)x_64≠0--x_64=0 567)x_66≠1 x_66≠1 567)x_66≠1--x_66=1 568)x_60≠1 x_60≠1 567)x_66≠1--568)x_60≠1 569)x_60≠1 x_60≠1 567)x_66≠1--569)x_60≠1 568)x_60≠1--x_60=1 568)x_60≠1--569)x_60≠1 569)x_60≠1--x_60=1 570)x_66≠0 x_66≠0 570)x_66≠0--x_66=0 571)x_60≠0 x_60≠0 570)x_66≠0--571)x_60≠0 572)x_60≠0 x_60≠0 570)x_66≠0--572)x_60≠0 571)x_60≠0--x_60=0 571)x_60≠0--572)x_60≠0 572)x_60≠0--x_60=0 573)x_66≠0 x_66≠0 573)x_66≠0--x_66=0 574)x_60≠0 x_60≠0 573)x_66≠0--574)x_60≠0 575)x_60≠0 x_60≠0 573)x_66≠0--575)x_60≠0 574)x_60≠0--x_60=0 574)x_60≠0--575)x_60≠0 575)x_60≠0--x_60=0 576)x_67≠1 x_67≠1 576)x_67≠1--x_67=1 577)x_64≠1 x_64≠1 576)x_67≠1--577)x_64≠1 578)x_64≠1 x_64≠1 576)x_67≠1--578)x_64≠1 577)x_64≠1--x_64=1 577)x_64≠1--578)x_64≠1 578)x_64≠1--x_64=1 579)x_67≠0 x_67≠0 579)x_67≠0--x_67=0 580)x_64≠0 x_64≠0 579)x_67≠0--580)x_64≠0 581)x_64≠0 x_64≠0 579)x_67≠0--581)x_64≠0 580)x_64≠0--x_64=0 580)x_64≠0--581)x_64≠0 581)x_64≠0--x_64=0 582)x_67≠0 x_67≠0 582)x_67≠0--x_67=0 583)x_64≠0 x_64≠0 582)x_67≠0--583)x_64≠0 584)x_64≠0 x_64≠0 582)x_67≠0--584)x_64≠0 583)x_64≠0--x_64=0 583)x_64≠0--584)x_64≠0 584)x_64≠0--x_64=0 585)x_68≠1 x_68≠1 585)x_68≠1--x_68=1 586)x_64≠1 x_64≠1 585)x_68≠1--586)x_64≠1 587)x_67≠1 x_67≠1 585)x_68≠1--587)x_67≠1 586)x_64≠1--x_64=1 586)x_64≠1--587)x_67≠1 587)x_67≠1--x_67=1 588)x_68≠0 x_68≠0 588)x_68≠0--x_68=0 589)x_64≠0 x_64≠0 588)x_68≠0--589)x_64≠0 590)x_64≠0 x_64≠0 588)x_68≠0--590)x_64≠0 589)x_64≠0--x_64=0 589)x_64≠0--590)x_64≠0 590)x_64≠0--x_64=0 591)x_68≠0 x_68≠0 591)x_68≠0--x_68=0 592)x_67≠0 x_67≠0 591)x_68≠0--592)x_67≠0 593)x_67≠0 x_67≠0 591)x_68≠0--593)x_67≠0 592)x_67≠0--x_67=0 592)x_67≠0--593)x_67≠0 593)x_67≠0--x_67=0 594)x_69≠1 x_69≠1 594)x_69≠1--x_69=1 595)x_60≠1 x_60≠1 594)x_69≠1--595)x_60≠1 596)x_60≠1 x_60≠1 594)x_69≠1--596)x_60≠1 595)x_60≠1--x_60=1 595)x_60≠1--596)x_60≠1 596)x_60≠1--x_60=1 597)x_69≠0 x_69≠0 597)x_69≠0--x_69=0 598)x_60≠0 x_60≠0 597)x_69≠0--598)x_60≠0 599)x_60≠0 x_60≠0 597)x_69≠0--599)x_60≠0 598)x_60≠0--x_60=0 598)x_60≠0--599)x_60≠0 599)x_60≠0--x_60=0 600)x_69≠0 x_69≠0 600)x_69≠0--x_69=0 601)x_60≠0 x_60≠0 600)x_69≠0--601)x_60≠0 602)x_60≠0 x_60≠0 600)x_69≠0--602)x_60≠0 601)x_60≠0--x_60=0 601)x_60≠0--602)x_60≠0 602)x_60≠0--x_60=0 603)x_70≠1 x_70≠1 603)x_70≠1--x_70=1 604)x_69≠1 x_69≠1 603)x_70≠1--604)x_69≠1 605)x_68≠1 x_68≠1 603)x_70≠1--605)x_68≠1 604)x_69≠1--x_69=1 604)x_69≠1--605)x_68≠1 605)x_68≠1--x_68=1 606)x_70≠0 x_70≠0 606)x_70≠0--x_70=0 607)x_69≠0 x_69≠0 606)x_70≠0--607)x_69≠0 608)x_69≠0 x_69≠0 606)x_70≠0--608)x_69≠0 607)x_69≠0--x_69=0 607)x_69≠0--608)x_69≠0 608)x_69≠0--x_69=0 609)x_70≠0 x_70≠0 609)x_70≠0--x_70=0 610)x_68≠0 x_68≠0 609)x_70≠0--610)x_68≠0 611)x_68≠0 x_68≠0 609)x_70≠0--611)x_68≠0 610)x_68≠0--x_68=0 610)x_68≠0--611)x_68≠0 611)x_68≠0--x_68=0 612)x_71≠1 x_71≠1 612)x_71≠1--x_71=1 613)x_64≠1 x_64≠1 612)x_71≠1--613)x_64≠1 614)x_64≠1 x_64≠1 612)x_71≠1--614)x_64≠1 613)x_64≠1--x_64=1 613)x_64≠1--614)x_64≠1 614)x_64≠1--x_64=1 615)x_71≠0 x_71≠0 615)x_71≠0--x_71=0 616)x_64≠0 x_64≠0 615)x_71≠0--616)x_64≠0 617)x_64≠0 x_64≠0 615)x_71≠0--617)x_64≠0 616)x_64≠0--x_64=0 616)x_64≠0--617)x_64≠0 617)x_64≠0--x_64=0 618)x_71≠0 x_71≠0 618)x_71≠0--x_71=0 619)x_64≠0 x_64≠0 618)x_71≠0--619)x_64≠0 620)x_64≠0 x_64≠0 618)x_71≠0--620)x_64≠0 619)x_64≠0--x_64=0 619)x_64≠0--620)x_64≠0 620)x_64≠0--x_64=0 621)x_72≠1 x_72≠1 621)x_72≠1--x_72=1 622)x_71≠1 x_71≠1 621)x_72≠1--622)x_71≠1 623)x_71≠1 x_71≠1 621)x_72≠1--623)x_71≠1 622)x_71≠1--x_71=1 622)x_71≠1--623)x_71≠1 623)x_71≠1--x_71=1 624)x_72≠0 x_72≠0 624)x_72≠0--x_72=0 625)x_71≠0 x_71≠0 624)x_72≠0--625)x_71≠0 626)x_71≠0 x_71≠0 624)x_72≠0--626)x_71≠0 625)x_71≠0--x_71=0 625)x_71≠0--626)x_71≠0 626)x_71≠0--x_71=0 627)x_72≠0 x_72≠0 627)x_72≠0--x_72=0 628)x_71≠0 x_71≠0 627)x_72≠0--628)x_71≠0 629)x_71≠0 x_71≠0 627)x_72≠0--629)x_71≠0 628)x_71≠0--x_71=0 628)x_71≠0--629)x_71≠0 629)x_71≠0--x_71=0 630)x_73≠1 x_73≠1 630)x_73≠1--x_73=1 631)x_64≠1 x_64≠1 630)x_73≠1--631)x_64≠1 632)x_64≠1 x_64≠1 630)x_73≠1--632)x_64≠1 631)x_64≠1--x_64=1 631)x_64≠1--632)x_64≠1 632)x_64≠1--x_64=1 633)x_73≠0 x_73≠0 633)x_73≠0--x_73=0 634)x_64≠0 x_64≠0 633)x_73≠0--634)x_64≠0 635)x_64≠0 x_64≠0 633)x_73≠0--635)x_64≠0 634)x_64≠0--x_64=0 634)x_64≠0--635)x_64≠0 635)x_64≠0--x_64=0 636)x_73≠0 x_73≠0 636)x_73≠0--x_73=0 637)x_64≠0 x_64≠0 636)x_73≠0--637)x_64≠0 638)x_64≠0 x_64≠0 636)x_73≠0--638)x_64≠0 637)x_64≠0--x_64=0 637)x_64≠0--638)x_64≠0 638)x_64≠0--x_64=0 639)x_74≠1 x_74≠1 639)x_74≠1--x_74=1 640)x_64≠1 x_64≠1 639)x_74≠1--640)x_64≠1 641)x_73≠1 x_73≠1 639)x_74≠1--641)x_73≠1 640)x_64≠1--x_64=1 640)x_64≠1--641)x_73≠1 641)x_73≠1--x_73=1 642)x_74≠0 x_74≠0 642)x_74≠0--x_74=0 643)x_64≠0 x_64≠0 642)x_74≠0--643)x_64≠0 644)x_64≠0 x_64≠0 642)x_74≠0--644)x_64≠0 643)x_64≠0--x_64=0 643)x_64≠0--644)x_64≠0 644)x_64≠0--x_64=0 645)x_74≠0 x_74≠0 645)x_74≠0--x_74=0 646)x_73≠0 x_73≠0 645)x_74≠0--646)x_73≠0 647)x_73≠0 x_73≠0 645)x_74≠0--647)x_73≠0 646)x_73≠0--x_73=0 646)x_73≠0--647)x_73≠0 647)x_73≠0--x_73=0 648)x_75≠1 x_75≠1 648)x_75≠1--x_75=1 649)x_74≠1 x_74≠1 648)x_75≠1--649)x_74≠1 650)x_74≠1 x_74≠1 648)x_75≠1--650)x_74≠1 649)x_74≠1--x_74=1 649)x_74≠1--650)x_74≠1 650)x_74≠1--x_74=1 651)x_75≠0 x_75≠0 651)x_75≠0--x_75=0 652)x_74≠0 x_74≠0 651)x_75≠0--652)x_74≠0 653)x_74≠0 x_74≠0 651)x_75≠0--653)x_74≠0 652)x_74≠0--x_74=0 652)x_74≠0--653)x_74≠0 653)x_74≠0--x_74=0 654)x_75≠0 x_75≠0 654)x_75≠0--x_75=0 655)x_74≠0 x_74≠0 654)x_75≠0--655)x_74≠0 656)x_74≠0 x_74≠0 654)x_75≠0--656)x_74≠0 655)x_74≠0--x_74=0 655)x_74≠0--656)x_74≠0 656)x_74≠0--x_74=0 657)x_76≠1 x_76≠1 657)x_76≠1--x_76=1 658)x_70≠1 x_70≠1 657)x_76≠1--658)x_70≠1 659)x_70≠1 x_70≠1 657)x_76≠1--659)x_70≠1 658)x_70≠1--x_70=1 658)x_70≠1--659)x_70≠1 659)x_70≠1--x_70=1 660)x_76≠0 x_76≠0 660)x_76≠0--x_76=0 661)x_70≠0 x_70≠0 660)x_76≠0--661)x_70≠0 662)x_70≠0 x_70≠0 660)x_76≠0--662)x_70≠0 661)x_70≠0--x_70=0 661)x_70≠0--662)x_70≠0 662)x_70≠0--x_70=0 663)x_76≠0 x_76≠0 663)x_76≠0--x_76=0 664)x_70≠0 x_70≠0 663)x_76≠0--664)x_70≠0 665)x_70≠0 x_70≠0 663)x_76≠0--665)x_70≠0 664)x_70≠0--x_70=0 664)x_70≠0--665)x_70≠0 665)x_70≠0--x_70=0 666)x_77≠1 x_77≠1 666)x_77≠1--x_77=1 667)x_74≠1 x_74≠1 666)x_77≠1--667)x_74≠1 668)x_74≠1 x_74≠1 666)x_77≠1--668)x_74≠1 667)x_74≠1--x_74=1 667)x_74≠1--668)x_74≠1 668)x_74≠1--x_74=1 669)x_77≠0 x_77≠0 669)x_77≠0--x_77=0 670)x_74≠0 x_74≠0 669)x_77≠0--670)x_74≠0 671)x_74≠0 x_74≠0 669)x_77≠0--671)x_74≠0 670)x_74≠0--x_74=0 670)x_74≠0--671)x_74≠0 671)x_74≠0--x_74=0 672)x_77≠0 x_77≠0 672)x_77≠0--x_77=0 673)x_74≠0 x_74≠0 672)x_77≠0--673)x_74≠0 674)x_74≠0 x_74≠0 672)x_77≠0--674)x_74≠0 673)x_74≠0--x_74=0 673)x_74≠0--674)x_74≠0 674)x_74≠0--x_74=0 675)x_78≠1 x_78≠1 675)x_78≠1--x_78=1 676)x_74≠1 x_74≠1 675)x_78≠1--676)x_74≠1 677)x_77≠1 x_77≠1 675)x_78≠1--677)x_77≠1 676)x_74≠1--x_74=1 676)x_74≠1--677)x_77≠1 677)x_77≠1--x_77=1 678)x_78≠0 x_78≠0 678)x_78≠0--x_78=0 679)x_74≠0 x_74≠0 678)x_78≠0--679)x_74≠0 680)x_74≠0 x_74≠0 678)x_78≠0--680)x_74≠0 679)x_74≠0--x_74=0 679)x_74≠0--680)x_74≠0 680)x_74≠0--x_74=0 681)x_78≠0 x_78≠0 681)x_78≠0--x_78=0 682)x_77≠0 x_77≠0 681)x_78≠0--682)x_77≠0 683)x_77≠0 x_77≠0 681)x_78≠0--683)x_77≠0 682)x_77≠0--x_77=0 682)x_77≠0--683)x_77≠0 683)x_77≠0--x_77=0 684)x_79≠1 x_79≠1 684)x_79≠1--x_79=1 685)x_70≠1 x_70≠1 684)x_79≠1--685)x_70≠1 686)x_70≠1 x_70≠1 684)x_79≠1--686)x_70≠1 685)x_70≠1--x_70=1 685)x_70≠1--686)x_70≠1 686)x_70≠1--x_70=1 687)x_79≠0 x_79≠0 687)x_79≠0--x_79=0 688)x_70≠0 x_70≠0 687)x_79≠0--688)x_70≠0 689)x_70≠0 x_70≠0 687)x_79≠0--689)x_70≠0 688)x_70≠0--x_70=0 688)x_70≠0--689)x_70≠0 689)x_70≠0--x_70=0 690)x_79≠0 x_79≠0 690)x_79≠0--x_79=0 691)x_70≠0 x_70≠0 690)x_79≠0--691)x_70≠0 692)x_70≠0 x_70≠0 690)x_79≠0--692)x_70≠0 691)x_70≠0--x_70=0 691)x_70≠0--692)x_70≠0 692)x_70≠0--x_70=0 693)x_80≠1 x_80≠1 693)x_80≠1--x_80=1 694)x_79≠1 x_79≠1 693)x_80≠1--694)x_79≠1 695)x_78≠1 x_78≠1 693)x_80≠1--695)x_78≠1 694)x_79≠1--x_79=1 694)x_79≠1--695)x_78≠1 695)x_78≠1--x_78=1 696)x_80≠0 x_80≠0 696)x_80≠0--x_80=0 697)x_79≠0 x_79≠0 696)x_80≠0--697)x_79≠0 698)x_79≠0 x_79≠0 696)x_80≠0--698)x_79≠0 697)x_79≠0--x_79=0 697)x_79≠0--698)x_79≠0 698)x_79≠0--x_79=0 699)x_80≠0 x_80≠0 699)x_80≠0--x_80=0 700)x_78≠0 x_78≠0 699)x_80≠0--700)x_78≠0 701)x_78≠0 x_78≠0 699)x_80≠0--701)x_78≠0 700)x_78≠0--x_78=0 700)x_78≠0--701)x_78≠0 701)x_78≠0--x_78=0 702)x_81≠1 x_81≠1 702)x_81≠1--x_81=1 703)x_74≠1 x_74≠1 702)x_81≠1--703)x_74≠1 704)x_74≠1 x_74≠1 702)x_81≠1--704)x_74≠1 703)x_74≠1--x_74=1 703)x_74≠1--704)x_74≠1 704)x_74≠1--x_74=1 705)x_81≠0 x_81≠0 705)x_81≠0--x_81=0 706)x_74≠0 x_74≠0 705)x_81≠0--706)x_74≠0 707)x_74≠0 x_74≠0 705)x_81≠0--707)x_74≠0 706)x_74≠0--x_74=0 706)x_74≠0--707)x_74≠0 707)x_74≠0--x_74=0 708)x_81≠0 x_81≠0 708)x_81≠0--x_81=0 709)x_74≠0 x_74≠0 708)x_81≠0--709)x_74≠0 710)x_74≠0 x_74≠0 708)x_81≠0--710)x_74≠0 709)x_74≠0--x_74=0 709)x_74≠0--710)x_74≠0 710)x_74≠0--x_74=0 711)x_82≠1 x_82≠1 711)x_82≠1--x_82=1 712)x_81≠1 x_81≠1 711)x_82≠1--712)x_81≠1 713)x_81≠1 x_81≠1 711)x_82≠1--713)x_81≠1 712)x_81≠1--x_81=1 712)x_81≠1--713)x_81≠1 713)x_81≠1--x_81=1 714)x_82≠0 x_82≠0 714)x_82≠0--x_82=0 715)x_81≠0 x_81≠0 714)x_82≠0--715)x_81≠0 716)x_81≠0 x_81≠0 714)x_82≠0--716)x_81≠0 715)x_81≠0--x_81=0 715)x_81≠0--716)x_81≠0 716)x_81≠0--x_81=0 717)x_82≠0 x_82≠0 717)x_82≠0--x_82=0 718)x_81≠0 x_81≠0 717)x_82≠0--718)x_81≠0 719)x_81≠0 x_81≠0 717)x_82≠0--719)x_81≠0 718)x_81≠0--x_81=0 718)x_81≠0--719)x_81≠0 719)x_81≠0--x_81=0 720)x_83≠1 x_83≠1 720)x_83≠1--x_83=1 721)x_74≠1 x_74≠1 720)x_83≠1--721)x_74≠1 722)x_74≠1 x_74≠1 720)x_83≠1--722)x_74≠1 721)x_74≠1--x_74=1 721)x_74≠1--722)x_74≠1 722)x_74≠1--x_74=1 723)x_83≠0 x_83≠0 723)x_83≠0--x_83=0 724)x_74≠0 x_74≠0 723)x_83≠0--724)x_74≠0 725)x_74≠0 x_74≠0 723)x_83≠0--725)x_74≠0 724)x_74≠0--x_74=0 724)x_74≠0--725)x_74≠0 725)x_74≠0--x_74=0 726)x_83≠0 x_83≠0 726)x_83≠0--x_83=0 727)x_74≠0 x_74≠0 726)x_83≠0--727)x_74≠0 728)x_74≠0 x_74≠0 726)x_83≠0--728)x_74≠0 727)x_74≠0--x_74=0 727)x_74≠0--728)x_74≠0 728)x_74≠0--x_74=0 729)x_84≠1 x_84≠1 729)x_84≠1--x_84=1 730)x_74≠1 x_74≠1 729)x_84≠1--730)x_74≠1 731)x_83≠1 x_83≠1 729)x_84≠1--731)x_83≠1 730)x_74≠1--x_74=1 730)x_74≠1--731)x_83≠1 731)x_83≠1--x_83=1 732)x_84≠0 x_84≠0 732)x_84≠0--x_84=0 733)x_74≠0 x_74≠0 732)x_84≠0--733)x_74≠0 734)x_74≠0 x_74≠0 732)x_84≠0--734)x_74≠0 733)x_74≠0--x_74=0 733)x_74≠0--734)x_74≠0 734)x_74≠0--x_74=0 735)x_84≠0 x_84≠0 735)x_84≠0--x_84=0 736)x_83≠0 x_83≠0 735)x_84≠0--736)x_83≠0 737)x_83≠0 x_83≠0 735)x_84≠0--737)x_83≠0 736)x_83≠0--x_83=0 736)x_83≠0--737)x_83≠0 737)x_83≠0--x_83=0 738)x_85≠1 x_85≠1 738)x_85≠1--x_85=1 739)x_84≠1 x_84≠1 738)x_85≠1--739)x_84≠1 740)x_84≠1 x_84≠1 738)x_85≠1--740)x_84≠1 739)x_84≠1--x_84=1 739)x_84≠1--740)x_84≠1 740)x_84≠1--x_84=1 741)x_85≠0 x_85≠0 741)x_85≠0--x_85=0 742)x_84≠0 x_84≠0 741)x_85≠0--742)x_84≠0 743)x_84≠0 x_84≠0 741)x_85≠0--743)x_84≠0 742)x_84≠0--x_84=0 742)x_84≠0--743)x_84≠0 743)x_84≠0--x_84=0 744)x_85≠0 x_85≠0 744)x_85≠0--x_85=0 745)x_84≠0 x_84≠0 744)x_85≠0--745)x_84≠0 746)x_84≠0 x_84≠0 744)x_85≠0--746)x_84≠0 745)x_84≠0--x_84=0 745)x_84≠0--746)x_84≠0 746)x_84≠0--x_84=0 747)x_86≠1 x_86≠1 747)x_86≠1--x_86=1 748)x_80≠1 x_80≠1 747)x_86≠1--748)x_80≠1 749)x_80≠1 x_80≠1 747)x_86≠1--749)x_80≠1 748)x_80≠1--x_80=1 748)x_80≠1--749)x_80≠1 749)x_80≠1--x_80=1 750)x_86≠0 x_86≠0 750)x_86≠0--x_86=0 751)x_80≠0 x_80≠0 750)x_86≠0--751)x_80≠0 752)x_80≠0 x_80≠0 750)x_86≠0--752)x_80≠0 751)x_80≠0--x_80=0 751)x_80≠0--752)x_80≠0 752)x_80≠0--x_80=0 753)x_86≠0 x_86≠0 753)x_86≠0--x_86=0 754)x_80≠0 x_80≠0 753)x_86≠0--754)x_80≠0 755)x_80≠0 x_80≠0 753)x_86≠0--755)x_80≠0 754)x_80≠0--x_80=0 754)x_80≠0--755)x_80≠0 755)x_80≠0--x_80=0 756)x_87≠1 x_87≠1 756)x_87≠1--x_87=1 757)x_0≠1 x_0≠1 756)x_87≠1--757)x_0≠1 758)x_0≠1 x_0≠1 756)x_87≠1--758)x_0≠1 757)x_0≠1--x_0=1 757)x_0≠1--758)x_0≠1 758)x_0≠1--x_0=1 759)x_87≠0 x_87≠0 759)x_87≠0--x_87=0 760)x_0≠0 x_0≠0 759)x_87≠0--760)x_0≠0 761)x_0≠0 x_0≠0 759)x_87≠0--761)x_0≠0 760)x_0≠0--x_0=0 760)x_0≠0--761)x_0≠0 761)x_0≠0--x_0=0 762)x_87≠0 x_87≠0 762)x_87≠0--x_87=0 763)x_0≠0 x_0≠0 762)x_87≠0--763)x_0≠0 764)x_0≠0 x_0≠0 762)x_87≠0--764)x_0≠0 763)x_0≠0--x_0=0 763)x_0≠0--764)x_0≠0 764)x_0≠0--x_0=0 765)x_88≠1 x_88≠1 765)x_88≠1--x_88=1 766)x_84≠1 x_84≠1 765)x_88≠1--766)x_84≠1 767)x_87≠1 x_87≠1 765)x_88≠1--767)x_87≠1 766)x_84≠1--x_84=1 766)x_84≠1--767)x_87≠1 767)x_87≠1--x_87=1 768)x_88≠0 x_88≠0 768)x_88≠0--x_88=0 769)x_84≠0 x_84≠0 768)x_88≠0--769)x_84≠0 770)x_84≠0 x_84≠0 768)x_88≠0--770)x_84≠0 769)x_84≠0--x_84=0 769)x_84≠0--770)x_84≠0 770)x_84≠0--x_84=0 771)x_88≠0 x_88≠0 771)x_88≠0--x_88=0 772)x_87≠0 x_87≠0 771)x_88≠0--772)x_87≠0 773)x_87≠0 x_87≠0 771)x_88≠0--773)x_87≠0 772)x_87≠0--x_87=0 772)x_87≠0--773)x_87≠0 773)x_87≠0--x_87=0 774)x_89≠1 x_89≠1 774)x_89≠1--x_89=1 775)x_80≠1 x_80≠1 774)x_89≠1--775)x_80≠1 776)x_80≠1 x_80≠1 774)x_89≠1--776)x_80≠1 775)x_80≠1--x_80=1 775)x_80≠1--776)x_80≠1 776)x_80≠1--x_80=1 777)x_89≠0 x_89≠0 777)x_89≠0--x_89=0 778)x_80≠0 x_80≠0 777)x_89≠0--778)x_80≠0 779)x_80≠0 x_80≠0 777)x_89≠0--779)x_80≠0 778)x_80≠0--x_80=0 778)x_80≠0--779)x_80≠0 779)x_80≠0--x_80=0 780)x_89≠0 x_89≠0 780)x_89≠0--x_89=0 781)x_80≠0 x_80≠0 780)x_89≠0--781)x_80≠0 782)x_80≠0 x_80≠0 780)x_89≠0--782)x_80≠0 781)x_80≠0--x_80=0 781)x_80≠0--782)x_80≠0 782)x_80≠0--x_80=0 783)x_90≠1 x_90≠1 783)x_90≠1--x_90=1 784)x_89≠1 x_89≠1 783)x_90≠1--784)x_89≠1 785)x_88≠1 x_88≠1 783)x_90≠1--785)x_88≠1 784)x_89≠1--x_89=1 784)x_89≠1--785)x_88≠1 785)x_88≠1--x_88=1 786)x_90≠0 x_90≠0 786)x_90≠0--x_90=0 787)x_89≠0 x_89≠0 786)x_90≠0--787)x_89≠0 788)x_89≠0 x_89≠0 786)x_90≠0--788)x_89≠0 787)x_89≠0--x_89=0 787)x_89≠0--788)x_89≠0 788)x_89≠0--x_89=0 789)x_90≠0 x_90≠0 789)x_90≠0--x_90=0 790)x_88≠0 x_88≠0 789)x_90≠0--790)x_88≠0 791)x_88≠0 x_88≠0 789)x_90≠0--791)x_88≠0 790)x_88≠0--x_88=0 790)x_88≠0--791)x_88≠0 791)x_88≠0--x_88=0 792)x_91≠1 x_91≠1 792)x_91≠1--x_91=1 793)x_84≠1 x_84≠1 792)x_91≠1--793)x_84≠1 794)x_84≠1 x_84≠1 792)x_91≠1--794)x_84≠1 793)x_84≠1--x_84=1 793)x_84≠1--794)x_84≠1 794)x_84≠1--x_84=1 795)x_91≠0 x_91≠0 795)x_91≠0--x_91=0 796)x_84≠0 x_84≠0 795)x_91≠0--796)x_84≠0 797)x_84≠0 x_84≠0 795)x_91≠0--797)x_84≠0 796)x_84≠0--x_84=0 796)x_84≠0--797)x_84≠0 797)x_84≠0--x_84=0 798)x_91≠0 x_91≠0 798)x_91≠0--x_91=0 799)x_84≠0 x_84≠0 798)x_91≠0--799)x_84≠0 800)x_84≠0 x_84≠0 798)x_91≠0--800)x_84≠0 799)x_84≠0--x_84=0 799)x_84≠0--800)x_84≠0 800)x_84≠0--x_84=0 801)x_92≠1 x_92≠1 801)x_92≠1--x_92=1 802)x_91≠1 x_91≠1 801)x_92≠1--802)x_91≠1 803)x_91≠1 x_91≠1 801)x_92≠1--803)x_91≠1 802)x_91≠1--x_91=1 802)x_91≠1--803)x_91≠1 803)x_91≠1--x_91=1 804)x_92≠0 x_92≠0 804)x_92≠0--x_92=0 805)x_91≠0 x_91≠0 804)x_92≠0--805)x_91≠0 806)x_91≠0 x_91≠0 804)x_92≠0--806)x_91≠0 805)x_91≠0--x_91=0 805)x_91≠0--806)x_91≠0 806)x_91≠0--x_91=0 807)x_92≠0 x_92≠0 807)x_92≠0--x_92=0 808)x_91≠0 x_91≠0 807)x_92≠0--808)x_91≠0 809)x_91≠0 x_91≠0 807)x_92≠0--809)x_91≠0 808)x_91≠0--x_91=0 808)x_91≠0--809)x_91≠0 809)x_91≠0--x_91=0 810)x_93≠1 x_93≠1 810)x_93≠1--x_93=1 811)x_84≠1 x_84≠1 810)x_93≠1--811)x_84≠1 812)x_84≠1 x_84≠1 810)x_93≠1--812)x_84≠1 811)x_84≠1--x_84=1 811)x_84≠1--812)x_84≠1 812)x_84≠1--x_84=1 813)x_93≠0 x_93≠0 813)x_93≠0--x_93=0 814)x_84≠0 x_84≠0 813)x_93≠0--814)x_84≠0 815)x_84≠0 x_84≠0 813)x_93≠0--815)x_84≠0 814)x_84≠0--x_84=0 814)x_84≠0--815)x_84≠0 815)x_84≠0--x_84=0 816)x_93≠0 x_93≠0 816)x_93≠0--x_93=0 817)x_84≠0 x_84≠0 816)x_93≠0--817)x_84≠0 818)x_84≠0 x_84≠0 816)x_93≠0--818)x_84≠0 817)x_84≠0--x_84=0 817)x_84≠0--818)x_84≠0 818)x_84≠0--x_84=0 819)x_94≠1 x_94≠1 819)x_94≠1--x_94=1 820)x_84≠1 x_84≠1 819)x_94≠1--820)x_84≠1 821)x_93≠1 x_93≠1 819)x_94≠1--821)x_93≠1 820)x_84≠1--x_84=1 820)x_84≠1--821)x_93≠1 821)x_93≠1--x_93=1 822)x_94≠0 x_94≠0 822)x_94≠0--x_94=0 823)x_84≠0 x_84≠0 822)x_94≠0--823)x_84≠0 824)x_84≠0 x_84≠0 822)x_94≠0--824)x_84≠0 823)x_84≠0--x_84=0 823)x_84≠0--824)x_84≠0 824)x_84≠0--x_84=0 825)x_94≠0 x_94≠0 825)x_94≠0--x_94=0 826)x_93≠0 x_93≠0 825)x_94≠0--826)x_93≠0 827)x_93≠0 x_93≠0 825)x_94≠0--827)x_93≠0 826)x_93≠0--x_93=0 826)x_93≠0--827)x_93≠0 827)x_93≠0--x_93=0 828)x_95≠1 x_95≠1 828)x_95≠1--x_95=1 829)x_94≠1 x_94≠1 828)x_95≠1--829)x_94≠1 830)x_94≠1 x_94≠1 828)x_95≠1--830)x_94≠1 829)x_94≠1--x_94=1 829)x_94≠1--830)x_94≠1 830)x_94≠1--x_94=1 831)x_95≠0 x_95≠0 831)x_95≠0--x_95=0 832)x_94≠0 x_94≠0 831)x_95≠0--832)x_94≠0 833)x_94≠0 x_94≠0 831)x_95≠0--833)x_94≠0 832)x_94≠0--x_94=0 832)x_94≠0--833)x_94≠0 833)x_94≠0--x_94=0 834)x_95≠0 x_95≠0 834)x_95≠0--x_95=0 835)x_94≠0 x_94≠0 834)x_95≠0--835)x_94≠0 836)x_94≠0 x_94≠0 834)x_95≠0--836)x_94≠0 835)x_94≠0--x_94=0 835)x_94≠0--836)x_94≠0 836)x_94≠0--x_94=0 837)x_96≠1 x_96≠1 837)x_96≠1--x_96=1 838)x_90≠1 x_90≠1 837)x_96≠1--838)x_90≠1 839)x_90≠1 x_90≠1 837)x_96≠1--839)x_90≠1 838)x_90≠1--x_90=1 838)x_90≠1--839)x_90≠1 839)x_90≠1--x_90=1 840)x_96≠0 x_96≠0 840)x_96≠0--x_96=0 841)x_90≠0 x_90≠0 840)x_96≠0--841)x_90≠0 842)x_90≠0 x_90≠0 840)x_96≠0--842)x_90≠0 841)x_90≠0--x_90=0 841)x_90≠0--842)x_90≠0 842)x_90≠0--x_90=0 843)x_96≠0 x_96≠0 843)x_96≠0--x_96=0 844)x_90≠0 x_90≠0 843)x_96≠0--844)x_90≠0 845)x_90≠0 x_90≠0 843)x_96≠0--845)x_90≠0 844)x_90≠0--x_90=0 844)x_90≠0--845)x_90≠0 845)x_90≠0--x_90=0 846)x_97≠1 x_97≠1 846)x_97≠1--x_97=1 847)x_1≠1 x_1≠1 846)x_97≠1--847)x_1≠1 848)x_1≠1 x_1≠1 846)x_97≠1--848)x_1≠1 847)x_1≠1--x_1=1 847)x_1≠1--848)x_1≠1 848)x_1≠1--x_1=1 849)x_97≠0 x_97≠0 849)x_97≠0--x_97=0 850)x_1≠0 x_1≠0 849)x_97≠0--850)x_1≠0 851)x_1≠0 x_1≠0 849)x_97≠0--851)x_1≠0 850)x_1≠0--x_1=0 850)x_1≠0--851)x_1≠0 851)x_1≠0--x_1=0 852)x_97≠0 x_97≠0 852)x_97≠0--x_97=0 853)x_1≠0 x_1≠0 852)x_97≠0--853)x_1≠0 854)x_1≠0 x_1≠0 852)x_97≠0--854)x_1≠0 853)x_1≠0--x_1=0 853)x_1≠0--854)x_1≠0 854)x_1≠0--x_1=0 855)x_98≠1 x_98≠1 855)x_98≠1--x_98=1 856)x_94≠1 x_94≠1 855)x_98≠1--856)x_94≠1 857)x_97≠1 x_97≠1 855)x_98≠1--857)x_97≠1 856)x_94≠1--x_94=1 856)x_94≠1--857)x_97≠1 857)x_97≠1--x_97=1 858)x_98≠0 x_98≠0 858)x_98≠0--x_98=0 859)x_94≠0 x_94≠0 858)x_98≠0--859)x_94≠0 860)x_94≠0 x_94≠0 858)x_98≠0--860)x_94≠0 859)x_94≠0--x_94=0 859)x_94≠0--860)x_94≠0 860)x_94≠0--x_94=0 861)x_98≠0 x_98≠0 861)x_98≠0--x_98=0 862)x_97≠0 x_97≠0 861)x_98≠0--862)x_97≠0 863)x_97≠0 x_97≠0 861)x_98≠0--863)x_97≠0 862)x_97≠0--x_97=0 862)x_97≠0--863)x_97≠0 863)x_97≠0--x_97=0 864)x_99≠1 x_99≠1 864)x_99≠1--x_99=1 865)x_90≠1 x_90≠1 864)x_99≠1--865)x_90≠1 866)x_90≠1 x_90≠1 864)x_99≠1--866)x_90≠1 865)x_90≠1--x_90=1 865)x_90≠1--866)x_90≠1 866)x_90≠1--x_90=1 867)x_99≠0 x_99≠0 867)x_99≠0--x_99=0 868)x_90≠0 x_90≠0 867)x_99≠0--868)x_90≠0 869)x_90≠0 x_90≠0 867)x_99≠0--869)x_90≠0 868)x_90≠0--x_90=0 868)x_90≠0--869)x_90≠0 869)x_90≠0--x_90=0 870)x_99≠0 x_99≠0 870)x_99≠0--x_99=0 871)x_90≠0 x_90≠0 870)x_99≠0--871)x_90≠0 872)x_90≠0 x_90≠0 870)x_99≠0--872)x_90≠0 871)x_90≠0--x_90=0 871)x_90≠0--872)x_90≠0 872)x_90≠0--x_90=0 873)x_100≠1 x_100≠1 873)x_100≠1--x_100=1 874)x_99≠1 x_99≠1 873)x_100≠1--874)x_99≠1 875)x_98≠1 x_98≠1 873)x_100≠1--875)x_98≠1 874)x_99≠1--x_99=1 874)x_99≠1--875)x_98≠1 875)x_98≠1--x_98=1 876)x_100≠0 x_100≠0 876)x_100≠0--x_100=0 877)x_99≠0 x_99≠0 876)x_100≠0--877)x_99≠0 878)x_99≠0 x_99≠0 876)x_100≠0--878)x_99≠0 877)x_99≠0--x_99=0 877)x_99≠0--878)x_99≠0 878)x_99≠0--x_99=0 879)x_100≠0 x_100≠0 879)x_100≠0--x_100=0 880)x_98≠0 x_98≠0 879)x_100≠0--880)x_98≠0 881)x_98≠0 x_98≠0 879)x_100≠0--881)x_98≠0 880)x_98≠0--x_98=0 880)x_98≠0--881)x_98≠0 881)x_98≠0--x_98=0 882)x_101≠1 x_101≠1 882)x_101≠1--x_101=1 883)x_94≠1 x_94≠1 882)x_101≠1--883)x_94≠1 884)x_94≠1 x_94≠1 882)x_101≠1--884)x_94≠1 883)x_94≠1--x_94=1 883)x_94≠1--884)x_94≠1 884)x_94≠1--x_94=1 885)x_101≠0 x_101≠0 885)x_101≠0--x_101=0 886)x_94≠0 x_94≠0 885)x_101≠0--886)x_94≠0 887)x_94≠0 x_94≠0 885)x_101≠0--887)x_94≠0 886)x_94≠0--x_94=0 886)x_94≠0--887)x_94≠0 887)x_94≠0--x_94=0 888)x_101≠0 x_101≠0 888)x_101≠0--x_101=0 889)x_94≠0 x_94≠0 888)x_101≠0--889)x_94≠0 890)x_94≠0 x_94≠0 888)x_101≠0--890)x_94≠0 889)x_94≠0--x_94=0 889)x_94≠0--890)x_94≠0 890)x_94≠0--x_94=0 891)x_102≠1 x_102≠1 891)x_102≠1--x_102=1 892)x_101≠1 x_101≠1 891)x_102≠1--892)x_101≠1 893)x_101≠1 x_101≠1 891)x_102≠1--893)x_101≠1 892)x_101≠1--x_101=1 892)x_101≠1--893)x_101≠1 893)x_101≠1--x_101=1 894)x_102≠0 x_102≠0 894)x_102≠0--x_102=0 895)x_101≠0 x_101≠0 894)x_102≠0--895)x_101≠0 896)x_101≠0 x_101≠0 894)x_102≠0--896)x_101≠0 895)x_101≠0--x_101=0 895)x_101≠0--896)x_101≠0 896)x_101≠0--x_101=0 897)x_102≠0 x_102≠0 897)x_102≠0--x_102=0 898)x_101≠0 x_101≠0 897)x_102≠0--898)x_101≠0 899)x_101≠0 x_101≠0 897)x_102≠0--899)x_101≠0 898)x_101≠0--x_101=0 898)x_101≠0--899)x_101≠0 899)x_101≠0--x_101=0 900)x_103≠1 x_103≠1 900)x_103≠1--x_103=1 901)x_94≠1 x_94≠1 900)x_103≠1--901)x_94≠1 902)x_94≠1 x_94≠1 900)x_103≠1--902)x_94≠1 901)x_94≠1--x_94=1 901)x_94≠1--902)x_94≠1 902)x_94≠1--x_94=1 903)x_103≠0 x_103≠0 903)x_103≠0--x_103=0 904)x_94≠0 x_94≠0 903)x_103≠0--904)x_94≠0 905)x_94≠0 x_94≠0 903)x_103≠0--905)x_94≠0 904)x_94≠0--x_94=0 904)x_94≠0--905)x_94≠0 905)x_94≠0--x_94=0 906)x_103≠0 x_103≠0 906)x_103≠0--x_103=0 907)x_94≠0 x_94≠0 906)x_103≠0--907)x_94≠0 908)x_94≠0 x_94≠0 906)x_103≠0--908)x_94≠0 907)x_94≠0--x_94=0 907)x_94≠0--908)x_94≠0 908)x_94≠0--x_94=0 909)x_104≠1 x_104≠1 909)x_104≠1--x_104=1 910)x_94≠1 x_94≠1 909)x_104≠1--910)x_94≠1 911)x_103≠1 x_103≠1 909)x_104≠1--911)x_103≠1 910)x_94≠1--x_94=1 910)x_94≠1--911)x_103≠1 911)x_103≠1--x_103=1 912)x_104≠0 x_104≠0 912)x_104≠0--x_104=0 913)x_94≠0 x_94≠0 912)x_104≠0--913)x_94≠0 914)x_94≠0 x_94≠0 912)x_104≠0--914)x_94≠0 913)x_94≠0--x_94=0 913)x_94≠0--914)x_94≠0 914)x_94≠0--x_94=0 915)x_104≠0 x_104≠0 915)x_104≠0--x_104=0 916)x_103≠0 x_103≠0 915)x_104≠0--916)x_103≠0 917)x_103≠0 x_103≠0 915)x_104≠0--917)x_103≠0 916)x_103≠0--x_103=0 916)x_103≠0--917)x_103≠0 917)x_103≠0--x_103=0 918)x_105≠1 x_105≠1 918)x_105≠1--x_105=1 919)x_104≠1 x_104≠1 918)x_105≠1--919)x_104≠1 920)x_104≠1 x_104≠1 918)x_105≠1--920)x_104≠1 919)x_104≠1--x_104=1 919)x_104≠1--920)x_104≠1 920)x_104≠1--x_104=1 921)x_105≠0 x_105≠0 921)x_105≠0--x_105=0 922)x_104≠0 x_104≠0 921)x_105≠0--922)x_104≠0 923)x_104≠0 x_104≠0 921)x_105≠0--923)x_104≠0 922)x_104≠0--x_104=0 922)x_104≠0--923)x_104≠0 923)x_104≠0--x_104=0 924)x_105≠0 x_105≠0 924)x_105≠0--x_105=0 925)x_104≠0 x_104≠0 924)x_105≠0--925)x_104≠0 926)x_104≠0 x_104≠0 924)x_105≠0--926)x_104≠0 925)x_104≠0--x_104=0 925)x_104≠0--926)x_104≠0 926)x_104≠0--x_104=0 927)x_106≠1 x_106≠1 927)x_106≠1--x_106=1 928)x_100≠1 x_100≠1 927)x_106≠1--928)x_100≠1 929)x_100≠1 x_100≠1 927)x_106≠1--929)x_100≠1 928)x_100≠1--x_100=1 928)x_100≠1--929)x_100≠1 929)x_100≠1--x_100=1 930)x_106≠0 x_106≠0 930)x_106≠0--x_106=0 931)x_100≠0 x_100≠0 930)x_106≠0--931)x_100≠0 932)x_100≠0 x_100≠0 930)x_106≠0--932)x_100≠0 931)x_100≠0--x_100=0 931)x_100≠0--932)x_100≠0 932)x_100≠0--x_100=0 933)x_106≠0 x_106≠0 933)x_106≠0--x_106=0 934)x_100≠0 x_100≠0 933)x_106≠0--934)x_100≠0 935)x_100≠0 x_100≠0 933)x_106≠0--935)x_100≠0 934)x_100≠0--x_100=0 934)x_100≠0--935)x_100≠0 935)x_100≠0--x_100=0 936)x_107≠1 x_107≠1 936)x_107≠1--x_107=1 937)x_0≠1 x_0≠1 936)x_107≠1--937)x_0≠1 938)x_0≠1 x_0≠1 936)x_107≠1--938)x_0≠1 937)x_0≠1--x_0=1 937)x_0≠1--938)x_0≠1 938)x_0≠1--x_0=1 939)x_107≠0 x_107≠0 939)x_107≠0--x_107=0 940)x_0≠0 x_0≠0 939)x_107≠0--940)x_0≠0 941)x_0≠0 x_0≠0 939)x_107≠0--941)x_0≠0 940)x_0≠0--x_0=0 940)x_0≠0--941)x_0≠0 941)x_0≠0--x_0=0 942)x_107≠0 x_107≠0 942)x_107≠0--x_107=0 943)x_0≠0 x_0≠0 942)x_107≠0--943)x_0≠0 944)x_0≠0 x_0≠0 942)x_107≠0--944)x_0≠0 943)x_0≠0--x_0=0 943)x_0≠0--944)x_0≠0 944)x_0≠0--x_0=0 945)x_108≠1 x_108≠1 945)x_108≠1--x_108=1 946)x_104≠1 x_104≠1 945)x_108≠1--946)x_104≠1 947)x_107≠1 x_107≠1 945)x_108≠1--947)x_107≠1 946)x_104≠1--x_104=1 946)x_104≠1--947)x_107≠1 947)x_107≠1--x_107=1 948)x_108≠0 x_108≠0 948)x_108≠0--x_108=0 949)x_104≠0 x_104≠0 948)x_108≠0--949)x_104≠0 950)x_104≠0 x_104≠0 948)x_108≠0--950)x_104≠0 949)x_104≠0--x_104=0 949)x_104≠0--950)x_104≠0 950)x_104≠0--x_104=0 951)x_108≠0 x_108≠0 951)x_108≠0--x_108=0 952)x_107≠0 x_107≠0 951)x_108≠0--952)x_107≠0 953)x_107≠0 x_107≠0 951)x_108≠0--953)x_107≠0 952)x_107≠0--x_107=0 952)x_107≠0--953)x_107≠0 953)x_107≠0--x_107=0 954)x_109≠1 x_109≠1 954)x_109≠1--x_109=1 955)x_100≠1 x_100≠1 954)x_109≠1--955)x_100≠1 956)x_100≠1 x_100≠1 954)x_109≠1--956)x_100≠1 955)x_100≠1--x_100=1 955)x_100≠1--956)x_100≠1 956)x_100≠1--x_100=1 957)x_109≠0 x_109≠0 957)x_109≠0--x_109=0 958)x_100≠0 x_100≠0 957)x_109≠0--958)x_100≠0 959)x_100≠0 x_100≠0 957)x_109≠0--959)x_100≠0 958)x_100≠0--x_100=0 958)x_100≠0--959)x_100≠0 959)x_100≠0--x_100=0 960)x_109≠0 x_109≠0 960)x_109≠0--x_109=0 961)x_100≠0 x_100≠0 960)x_109≠0--961)x_100≠0 962)x_100≠0 x_100≠0 960)x_109≠0--962)x_100≠0 961)x_100≠0--x_100=0 961)x_100≠0--962)x_100≠0 962)x_100≠0--x_100=0 963)x_110≠1 x_110≠1 963)x_110≠1--x_110=1 964)x_109≠1 x_109≠1 963)x_110≠1--964)x_109≠1 965)x_108≠1 x_108≠1 963)x_110≠1--965)x_108≠1 964)x_109≠1--x_109=1 964)x_109≠1--965)x_108≠1 965)x_108≠1--x_108=1 966)x_110≠0 x_110≠0 966)x_110≠0--x_110=0 967)x_109≠0 x_109≠0 966)x_110≠0--967)x_109≠0 968)x_109≠0 x_109≠0 966)x_110≠0--968)x_109≠0 967)x_109≠0--x_109=0 967)x_109≠0--968)x_109≠0 968)x_109≠0--x_109=0 969)x_110≠0 x_110≠0 969)x_110≠0--x_110=0 970)x_108≠0 x_108≠0 969)x_110≠0--970)x_108≠0 971)x_108≠0 x_108≠0 969)x_110≠0--971)x_108≠0 970)x_108≠0--x_108=0 970)x_108≠0--971)x_108≠0 971)x_108≠0--x_108=0 972)x_111≠1 x_111≠1 972)x_111≠1--x_111=1 973)x_104≠1 x_104≠1 972)x_111≠1--973)x_104≠1 974)x_104≠1 x_104≠1 972)x_111≠1--974)x_104≠1 973)x_104≠1--x_104=1 973)x_104≠1--974)x_104≠1 974)x_104≠1--x_104=1 975)x_111≠0 x_111≠0 975)x_111≠0--x_111=0 976)x_104≠0 x_104≠0 975)x_111≠0--976)x_104≠0 977)x_104≠0 x_104≠0 975)x_111≠0--977)x_104≠0 976)x_104≠0--x_104=0 976)x_104≠0--977)x_104≠0 977)x_104≠0--x_104=0 978)x_111≠0 x_111≠0 978)x_111≠0--x_111=0 979)x_104≠0 x_104≠0 978)x_111≠0--979)x_104≠0 980)x_104≠0 x_104≠0 978)x_111≠0--980)x_104≠0 979)x_104≠0--x_104=0 979)x_104≠0--980)x_104≠0 980)x_104≠0--x_104=0 981)x_112≠1 x_112≠1 981)x_112≠1--x_112=1 982)x_111≠1 x_111≠1 981)x_112≠1--982)x_111≠1 983)x_111≠1 x_111≠1 981)x_112≠1--983)x_111≠1 982)x_111≠1--x_111=1 982)x_111≠1--983)x_111≠1 983)x_111≠1--x_111=1 984)x_112≠0 x_112≠0 984)x_112≠0--x_112=0 985)x_111≠0 x_111≠0 984)x_112≠0--985)x_111≠0 986)x_111≠0 x_111≠0 984)x_112≠0--986)x_111≠0 985)x_111≠0--x_111=0 985)x_111≠0--986)x_111≠0 986)x_111≠0--x_111=0 987)x_112≠0 x_112≠0 987)x_112≠0--x_112=0 988)x_111≠0 x_111≠0 987)x_112≠0--988)x_111≠0 989)x_111≠0 x_111≠0 987)x_112≠0--989)x_111≠0 988)x_111≠0--x_111=0 988)x_111≠0--989)x_111≠0 989)x_111≠0--x_111=0 990)x_113≠1 x_113≠1 990)x_113≠1--x_113=1 991)x_104≠1 x_104≠1 990)x_113≠1--991)x_104≠1 992)x_104≠1 x_104≠1 990)x_113≠1--992)x_104≠1 991)x_104≠1--x_104=1 991)x_104≠1--992)x_104≠1 992)x_104≠1--x_104=1 993)x_113≠0 x_113≠0 993)x_113≠0--x_113=0 994)x_104≠0 x_104≠0 993)x_113≠0--994)x_104≠0 995)x_104≠0 x_104≠0 993)x_113≠0--995)x_104≠0 994)x_104≠0--x_104=0 994)x_104≠0--995)x_104≠0 995)x_104≠0--x_104=0 996)x_113≠0 x_113≠0 996)x_113≠0--x_113=0 997)x_104≠0 x_104≠0 996)x_113≠0--997)x_104≠0 998)x_104≠0 x_104≠0 996)x_113≠0--998)x_104≠0 997)x_104≠0--x_104=0 997)x_104≠0--998)x_104≠0 998)x_104≠0--x_104=0 999)x_114≠1 x_114≠1 999)x_114≠1--x_114=1 1000)x_104≠1 x_104≠1 999)x_114≠1--1000)x_104≠1 1001)x_113≠1 x_113≠1 999)x_114≠1--1001)x_113≠1 1000)x_104≠1--x_104=1 1000)x_104≠1--1001)x_113≠1 1001)x_113≠1--x_113=1 1002)x_114≠0 x_114≠0 1002)x_114≠0--x_114=0 1003)x_104≠0 x_104≠0 1002)x_114≠0--1003)x_104≠0 1004)x_104≠0 x_104≠0 1002)x_114≠0--1004)x_104≠0 1003)x_104≠0--x_104=0 1003)x_104≠0--1004)x_104≠0 1004)x_104≠0--x_104=0 1005)x_114≠0 x_114≠0 1005)x_114≠0--x_114=0 1006)x_113≠0 x_113≠0 1005)x_114≠0--1006)x_113≠0 1007)x_113≠0 x_113≠0 1005)x_114≠0--1007)x_113≠0 1006)x_113≠0--x_113=0 1006)x_113≠0--1007)x_113≠0 1007)x_113≠0--x_113=0 1008)x_115≠1 x_115≠1 1008)x_115≠1--x_115=1 1009)x_114≠1 x_114≠1 1008)x_115≠1--1009)x_114≠1 1010)x_114≠1 x_114≠1 1008)x_115≠1--1010)x_114≠1 1009)x_114≠1--x_114=1 1009)x_114≠1--1010)x_114≠1 1010)x_114≠1--x_114=1 1011)x_115≠0 x_115≠0 1011)x_115≠0--x_115=0 1012)x_114≠0 x_114≠0 1011)x_115≠0--1012)x_114≠0 1013)x_114≠0 x_1