path: root/test/regress/regress4/instance_1151.smt

;;; Taken from
;;; http://www.uni-ulm.de/fileadmin/website_uni_ulm/iui.inst.190/Mitarbeiter/eibach/benchmark-attack-bivium-20080519-ending.zip
;;; benchmark-attack-bivium-20080519-ending/SAT/35/instance_1151.cnf
;;; Generated using dimacs_to_smt.pl

(benchmark b
:status sat
:logic QF_UF
:extrapreds ((x1))
:extrapreds ((x2))
:extrapreds ((x3))
:extrapreds ((x4))
:extrapreds ((x5))
:extrapreds ((x6))
:extrapreds ((x7))
:extrapreds ((x8))
:extrapreds ((x9))
:extrapreds ((x10))
:extrapreds ((x11))
:extrapreds ((x12))
:extrapreds ((x13))
:extrapreds ((x14))
:extrapreds ((x15))
:extrapreds ((x16))
:extrapreds ((x17))
:extrapreds ((x18))
:extrapreds ((x19))
:extrapreds ((x20))
:extrapreds ((x21))
:extrapreds ((x22))
:extrapreds ((x23))
:extrapreds ((x24))
:extrapreds ((x25))
:extrapreds ((x26))
:extrapreds ((x27))
:extrapreds ((x28))
:extrapreds ((x29))
:extrapreds ((x30))
:extrapreds ((x31))
:extrapreds ((x32))
:extrapreds ((x33))
:extrapreds ((x34))
:extrapreds ((x35))
:extrapreds ((x36))
:extrapreds ((x37))
:extrapreds ((x38))
:extrapreds ((x39))
:extrapreds ((x40))
:extrapreds ((x41))
:extrapreds ((x42))
:extrapreds ((x43))
:extrapreds ((x44))
:extrapreds ((x45))
:extrapreds ((x46))
:extrapreds ((x47))
:extrapreds ((x48))
:extrapreds ((x49))
:extrapreds ((x50))
:extrapreds ((x51))
:extrapreds ((x52))
:extrapreds ((x53))
:extrapreds ((x54))
:extrapreds ((x55))
:extrapreds ((x56))
:extrapreds ((x57))
:extrapreds ((x58))
:extrapreds ((x59))
:extrapreds ((x60))
:extrapreds ((x61))
:extrapreds ((x62))
:extrapreds ((x63))
:extrapreds ((x64))
:extrapreds ((x65))
:extrapreds ((x66))
:extrapreds ((x67))
:extrapreds ((x68))
:extrapreds ((x69))
:extrapreds ((x70))
:extrapreds ((x71))
:extrapreds ((x72))
:extrapreds ((x73))
:extrapreds ((x74))
:extrapreds ((x75))
:extrapreds ((x76))
:extrapreds ((x77))
:extrapreds ((x78))
:extrapreds ((x79))
:extrapreds ((x80))
:extrapreds ((x81))
:extrapreds ((x82))
:extrapreds ((x83))
:extrapreds ((x84))
:extrapreds ((x85))
:extrapreds ((x86))
:extrapreds ((x87))
:extrapreds ((x88))
:extrapreds ((x89))
:extrapreds ((x90))
:extrapreds ((x91))
:extrapreds ((x92))
:extrapreds ((x93))
:extrapreds ((x94))
:extrapreds ((x95))
:extrapreds ((x96))
:extrapreds ((x97))
:extrapreds ((x98))
:extrapreds ((x99))
:extrapreds ((x100))
:extrapreds ((x101))
:extrapreds ((x102))
:extrapreds ((x103))
:extrapreds ((x104))
:extrapreds ((x105))
:extrapreds ((x106))
:extrapreds ((x107))
:extrapreds ((x108))
:extrapreds ((x109))
:extrapreds ((x110))
:extrapreds ((x111))
:extrapreds ((x112))
:extrapreds ((x113))
:extrapreds ((x114))
:extrapreds ((x115))
:extrapreds ((x116))
:extrapreds ((x117))
:extrapreds ((x118))
:extrapreds ((x119))
:extrapreds ((x120))
:extrapreds ((x121))
:extrapreds ((x122))
:extrapreds ((x123))
:extrapreds ((x124))
:extrapreds ((x125))
:extrapreds ((x126))
:extrapreds ((x127))
:extrapreds ((x128))
:extrapreds ((x129))
:extrapreds ((x130))
:extrapreds ((x131))
:extrapreds ((x132))
:extrapreds ((x133))
:extrapreds ((x134))
:extrapreds ((x135))
:extrapreds ((x136))
:extrapreds ((x137))
:extrapreds ((x138))
:extrapreds ((x139))
:extrapreds ((x140))
:extrapreds ((x141))
:extrapreds ((x142))
:extrapreds ((x143))
:extrapreds ((x144))
:extrapreds ((x145))
:extrapreds ((x146))
:extrapreds ((x147))
:extrapreds ((x148))
:extrapreds ((x149))
:extrapreds ((x150))
:extrapreds ((x151))
:extrapreds ((x152))
:extrapreds ((x153))
:extrapreds ((x154))
:extrapreds ((x155))
:extrapreds ((x156))
:extrapreds ((x157))
:extrapreds ((x158))
:extrapreds ((x159))
:extrapreds ((x160))
:extrapreds ((x161))
:extrapreds ((x162))
:extrapreds ((x163))
:extrapreds ((x164))
:extrapreds ((x165))
:extrapreds ((x166))
:extrapreds ((x167))
:extrapreds ((x168))
:extrapreds ((x169))
:extrapreds ((x170))
:extrapreds ((x171))
:extrapreds ((x172))
:extrapreds ((x173))
:extrapreds ((x174))
:extrapreds ((x175))
:extrapreds ((x176))
:extrapreds ((x177))
:extrapreds ((x178))
:extrapreds ((x179))
:extrapreds ((x180))
:extrapreds ((x181))
:extrapreds ((x182))
:extrapreds ((x183))
:extrapreds ((x184))
:extrapreds ((x185))
:extrapreds ((x186))
:extrapreds ((x187))
:extrapreds ((x188))
:extrapreds ((x189))
:extrapreds ((x190))
:extrapreds ((x191))
:extrapreds ((x192))
:extrapreds ((x193))
:extrapreds ((x194))
:extrapreds ((x195))
:extrapreds ((x196))
:extrapreds ((x197))
:extrapreds ((x198))
:extrapreds ((x199))
:extrapreds ((x200))
:extrapreds ((x201))
:extrapreds ((x202))
:extrapreds ((x203))
:extrapreds ((x204))
:extrapreds ((x205))
:extrapreds ((x206))
:extrapreds ((x207))
:extrapreds ((x208))
:extrapreds ((x209))
:extrapreds ((x210))
:extrapreds ((x211))
:extrapreds ((x212))
:extrapreds ((x213))
:extrapreds ((x214))
:extrapreds ((x215))
:extrapreds ((x216))
:extrapreds ((x217))
:extrapreds ((x218))
:extrapreds ((x219))
:extrapreds ((x220))
:extrapreds ((x221))
:extrapreds ((x222))
:extrapreds ((x223))
:extrapreds ((x224))
:extrapreds ((x225))
:extrapreds ((x226))
:extrapreds ((x227))
:extrapreds ((x228))
:extrapreds ((x229))
:extrapreds ((x230))
:extrapreds ((x231))
:extrapreds ((x232))
:extrapreds ((x233))
:extrapreds ((x234))
:extrapreds ((x235))
:extrapreds ((x236))
:extrapreds ((x237))
:extrapreds ((x238))
:extrapreds ((x239))
:extrapreds ((x240))
:extrapreds ((x241))
:extrapreds ((x242))
:extrapreds ((x243))
:extrapreds ((x244))
:extrapreds ((x245))
:extrapreds ((x246))
:extrapreds ((x247))
:extrapreds ((x248))
:extrapreds ((x249))
:extrapreds ((x250))
:extrapreds ((x251))
:extrapreds ((x252))
:extrapreds ((x253))
:extrapreds ((x254))
:extrapreds ((x255))
:extrapreds ((x256))
:extrapreds ((x257))
:extrapreds ((x258))
:extrapreds ((x259))
:extrapreds ((x260))
:extrapreds ((x261))
:extrapreds ((x262))
:extrapreds ((x263))
:extrapreds ((x264))
:extrapreds ((x265))
:extrapreds ((x266))
:extrapreds ((x267))
:extrapreds ((x268))
:extrapreds ((x269))
:extrapreds ((x270))
:extrapreds ((x271))
:extrapreds ((x272))
:extrapreds ((x273))
:extrapreds ((x274))
:extrapreds ((x275))
:extrapreds ((x276))
:extrapreds ((x277))
:extrapreds ((x278))
:extrapreds ((x279))
:extrapreds ((x280))
:extrapreds ((x281))
:extrapreds ((x282))
:extrapreds ((x283))
:extrapreds ((x284))
:extrapreds ((x285))
:extrapreds ((x286))
:extrapreds ((x287))
:extrapreds ((x288))
:extrapreds ((x289))
:extrapreds ((x290))
:extrapreds ((x291))
:extrapreds ((x292))
:extrapreds ((x293))
:extrapreds ((x294))
:extrapreds ((x295))
:extrapreds ((x296))
:extrapreds ((x297))
:extrapreds ((x298))
:extrapreds ((x299))
:extrapreds ((x300))
:extrapreds ((x301))
:extrapreds ((x302))
:extrapreds ((x303))
:extrapreds ((x304))
:extrapreds ((x305))
:extrapreds ((x306))
:extrapreds ((x307))
:extrapreds ((x308))
:extrapreds ((x309))
:extrapreds ((x310))
:extrapreds ((x311))
:extrapreds ((x312))
:extrapreds ((x313))
:extrapreds ((x314))
:extrapreds ((x315))
:extrapreds ((x316))
:extrapreds ((x317))
:extrapreds ((x318))
:extrapreds ((x319))
:extrapreds ((x320))
:extrapreds ((x321))
:extrapreds ((x322))
:extrapreds ((x323))
:extrapreds ((x324))
:extrapreds ((x325))
:extrapreds ((x326))
:extrapreds ((x327))
:extrapreds ((x328))
:extrapreds ((x329))
:extrapreds ((x330))
:extrapreds ((x331))
:extrapreds ((x332))
:extrapreds ((x333))
:extrapreds ((x334))
:extrapreds ((x335))
:extrapreds ((x336))
:extrapreds ((x337))
:extrapreds ((x338))
:extrapreds ((x339))
:extrapreds ((x340))
:extrapreds ((x341))
:extrapreds ((x342))
:extrapreds ((x343))
:extrapreds ((x344))
:extrapreds ((x345))
:extrapreds ((x346))
:extrapreds ((x347))
:extrapreds ((x348))
:extrapreds ((x349))
:extrapreds ((x350))
:extrapreds ((x351))
:extrapreds ((x352))
:extrapreds ((x353))
:extrapreds ((x354))
:extrapreds ((x355))
:extrapreds ((x356))
:extrapreds ((x357))
:extrapreds ((x358))
:extrapreds ((x359))
:extrapreds ((x360))
:extrapreds ((x361))
:extrapreds ((x362))
:extrapreds ((x363))
:extrapreds ((x364))
:extrapreds ((x365))
:extrapreds ((x366))
:extrapreds ((x367))
:extrapreds ((x368))
:extrapreds ((x369))
:extrapreds ((x370))
:extrapreds ((x371))
:extrapreds ((x372))
:extrapreds ((x373))
:extrapreds ((x374))
:extrapreds ((x375))
:extrapreds ((x376))
:extrapreds ((x377))
:extrapreds ((x378))
:extrapreds ((x379))
:extrapreds ((x380))
:extrapreds ((x381))
:extrapreds ((x382))
:extrapreds ((x383))
:extrapreds ((x384))
:extrapreds ((x385))
:extrapreds ((x386))
:extrapreds ((x387))
:extrapreds ((x388))
:extrapreds ((x389))
:extrapreds ((x390))
:extrapreds ((x391))
:extrapreds ((x392))
:extrapreds ((x393))
:extrapreds ((x394))
:extrapreds ((x395))
:extrapreds ((x396))
:extrapreds ((x397))
:extrapreds ((x398))
:extrapreds ((x399))
:extrapreds ((x400))
:extrapreds ((x401))
:extrapreds ((x402))
:extrapreds ((x403))
:extrapreds ((x404))
:extrapreds ((x405))
:extrapreds ((x406))
:extrapreds ((x407))
:extrapreds ((x408))
:extrapreds ((x409))
:extrapreds ((x410))
:extrapreds ((x411))
:extrapreds ((x412))
:extrapreds ((x413))
:extrapreds ((x414))
:extrapreds ((x415))
:extrapreds ((x416))
:extrapreds ((x417))
:extrapreds ((x418))
:extrapreds ((x419))
:extrapreds ((x420))
:extrapreds ((x421))
:extrapreds ((x422))
:extrapreds ((x423))
:extrapreds ((x424))
:extrapreds ((x425))
:extrapreds ((x426))
:extrapreds ((x427))
:extrapreds ((x428))
:extrapreds ((x429))
:extrapreds ((x430))
:extrapreds ((x431))
:extrapreds ((x432))
:extrapreds ((x433))
:extrapreds ((x434))
:extrapreds ((x435))
:extrapreds ((x436))
:extrapreds ((x437))
:extrapreds ((x438))
:extrapreds ((x439))
:extrapreds ((x440))
:extrapreds ((x441))
:extrapreds ((x442))
:extrapreds ((x443))
:extrapreds ((x444))
:extrapreds ((x445))
:extrapreds ((x446))
:extrapreds ((x447))
:extrapreds ((x448))
:extrapreds ((x449))
:extrapreds ((x450))
:extrapreds ((x451))
:extrapreds ((x452))
:extrapreds ((x453))
:extrapreds ((x454))
:extrapreds ((x455))
:extrapreds ((x456))
:extrapreds ((x457))
:extrapreds ((x458))
:extrapreds ((x459))
:extrapreds ((x460))
:extrapreds ((x461))
:extrapreds ((x462))
:extrapreds ((x463))
:extrapreds ((x464))
:extrapreds ((x465))
:extrapreds ((x466))
:extrapreds ((x467))
:extrapreds ((x468))
:extrapreds ((x469))
:extrapreds ((x470))
:extrapreds ((x471))
:extrapreds ((x472))
:extrapreds ((x473))
:extrapreds ((x474))
:extrapreds ((x475))
:extrapreds ((x476))
:extrapreds ((x477))
:extrapreds ((x478))
:extrapreds ((x479))
:extrapreds ((x480))
:extrapreds ((x481))
:extrapreds ((x482))
:extrapreds ((x483))
:extrapreds ((x484))
:extrapreds ((x485))
:extrapreds ((x486))
:extrapreds ((x487))
:extrapreds ((x488))
:extrapreds ((x489))
:extrapreds ((x490))
:extrapreds ((x491))
:extrapreds ((x492))
:extrapreds ((x493))
:extrapreds ((x494))
:extrapreds ((x495))
:extrapreds ((x496))
:extrapreds ((x497))
:extrapreds ((x498))
:extrapreds ((x499))
:extrapreds ((x500))
:extrapreds ((x501))
:extrapreds ((x502))
:extrapreds ((x503))
:extrapreds ((x504))
:extrapreds ((x505))
:extrapreds ((x506))
:extrapreds ((x507))
:extrapreds ((x508))
:extrapreds ((x509))
:extrapreds ((x510))
:extrapreds ((x511))
:extrapreds ((x512))
:extrapreds ((x513))
:extrapreds ((x514))
:extrapreds ((x515))
:extrapreds ((x516))
:extrapreds ((x517))
:extrapreds ((x518))
:extrapreds ((x519))
:extrapreds ((x520))
:extrapreds ((x521))
:extrapreds ((x522))
:extrapreds ((x523))
:extrapreds ((x524))
:extrapreds ((x525))
:extrapreds ((x526))
:extrapreds ((x527))
:extrapreds ((x528))
:extrapreds ((x529))
:extrapreds ((x530))
:extrapreds ((x531))
:extrapreds ((x532))
:extrapreds ((x533))
:extrapreds ((x534))
:extrapreds ((x535))
:extrapreds ((x536))
:extrapreds ((x537))
:extrapreds ((x538))
:extrapreds ((x539))
:extrapreds ((x540))
:extrapreds ((x541))
:extrapreds ((x542))
:extrapreds ((x543))
:extrapreds ((x544))
:extrapreds ((x545))
:extrapreds ((x546))
:extrapreds ((x547))
:extrapreds ((x548))
:extrapreds ((x549))
:extrapreds ((x550))
:extrapreds ((x551))
:extrapreds ((x552))
:extrapreds ((x553))
:extrapreds ((x554))
:extrapreds ((x555))
:extrapreds ((x556))
:extrapreds ((x557))
:extrapreds ((x558))
:extrapreds ((x559))
:extrapreds ((x560))
:extrapreds ((x561))
:extrapreds ((x562))
:extrapreds ((x563))
:extrapreds ((x564))
:extrapreds ((x565))
:extrapreds ((x566))
:extrapreds ((x567))
:extrapreds ((x568))
:extrapreds ((x569))
:extrapreds ((x570))
:extrapreds ((x571))
:extrapreds ((x572))
:extrapreds ((x573))
:extrapreds ((x574))
:extrapreds ((x575))
:extrapreds ((x576))
:extrapreds ((x577))
:extrapreds ((x578))
:extrapreds ((x579))
:extrapreds ((x580))
:extrapreds ((x581))
:extrapreds ((x582))
:extrapreds ((x583))
:extrapreds ((x584))
:extrapreds ((x585))
:extrapreds ((x586))
:extrapreds ((x587))
:extrapreds ((x588))
:extrapreds ((x589))
:extrapreds ((x590))
:extrapreds ((x591))
:extrapreds ((x592))
:extrapreds ((x593))
:extrapreds ((x594))
:extrapreds ((x595))
:extrapreds ((x596))
:extrapreds ((x597))
:extrapreds ((x598))
:extrapreds ((x599))
:extrapreds ((x600))
:extrapreds ((x601))
:extrapreds ((x602))
:extrapreds ((x603))
:extrapreds ((x604))
:extrapreds ((x605))
:extrapreds ((x606))
:extrapreds ((x607))
:extrapreds ((x608))
:extrapreds ((x609))
:extrapreds ((x610))
:extrapreds ((x611))
:extrapreds ((x612))
:extrapreds ((x613))
:extrapreds ((x614))
:extrapreds ((x615))
:extrapreds ((x616))
:extrapreds ((x617))
:extrapreds ((x618))
:extrapreds ((x619))
:extrapreds ((x620))
:extrapreds ((x621))
:extrapreds ((x622))
:extrapreds ((x623))
:extrapreds ((x624))
:extrapreds ((x625))
:extrapreds ((x626))
:extrapreds ((x627))
:extrapreds ((x628))
:extrapreds ((x629))
:extrapreds ((x630))
:extrapreds ((x631))
:extrapreds ((x632))
:extrapreds ((x633))
:extrapreds ((x634))
:extrapreds ((x635))
:extrapreds ((x636))
:extrapreds ((x637))
:extrapreds ((x638))
:extrapreds ((x639))
:extrapreds ((x640))
:extrapreds ((x641))
:extrapreds ((x642))
:extrapreds ((x643))
:extrapreds ((x644))
:extrapreds ((x645))
:extrapreds ((x646))
:extrapreds ((x647))
:extrapreds ((x648))
:extrapreds ((x649))
:extrapreds ((x650))
:extrapreds ((x651))
:extrapreds ((x652))
:extrapreds ((x653))
:extrapreds ((x654))
:extrapreds ((x655))
:extrapreds ((x656))
:extrapreds ((x657))
:extrapreds ((x658))
:extrapreds ((x659))
:extrapreds ((x660))
:extrapreds ((x661))
:extrapreds ((x662))
:extrapreds ((x663))
:extrapreds ((x664))
:extrapreds ((x665))
:extrapreds ((x666))
:extrapreds ((x667))
:extrapreds ((x668))
:extrapreds ((x669))
:extrapreds ((x670))
:extrapreds ((x671))
:extrapreds ((x672))
:extrapreds ((x673))
:extrapreds ((x674))
:extrapreds ((x675))
:extrapreds ((x676))
:extrapreds ((x677))
:extrapreds ((x678))
:extrapreds ((x679))
:extrapreds ((x680))
:extrapreds ((x681))
:extrapreds ((x682))
:extrapreds ((x683))
:extrapreds ((x684))
:extrapreds ((x685))
:extrapreds ((x686))
:extrapreds ((x687))
:extrapreds ((x688))
:extrapreds ((x689))
:extrapreds ((x690))
:extrapreds ((x691))
:extrapreds ((x692))
:extrapreds ((x693))
:extrapreds ((x694))
:extrapreds ((x695))
:extrapreds ((x696))
:extrapreds ((x697))
:extrapreds ((x698))
:extrapreds ((x699))
:extrapreds ((x700))
:extrapreds ((x701))
:extrapreds ((x702))
:extrapreds ((x703))
:extrapreds ((x704))
:extrapreds ((x705))
:extrapreds ((x706))
:extrapreds ((x707))
:extrapreds ((x708))
:extrapreds ((x709))
:extrapreds ((x710))
:extrapreds ((x711))
:extrapreds ((x712))
:extrapreds ((x713))
:extrapreds ((x714))
:extrapreds ((x715))
:extrapreds ((x716))
:extrapreds ((x717))
:extrapreds ((x718))
:extrapreds ((x719))
:extrapreds ((x720))
:extrapreds ((x721))
:extrapreds ((x722))
:extrapreds ((x723))
:extrapreds ((x724))
:extrapreds ((x725))
:extrapreds ((x726))
:extrapreds ((x727))
:extrapreds ((x728))
:extrapreds ((x729))
:extrapreds ((x730))
:extrapreds ((x731))
:extrapreds ((x732))
:extrapreds ((x733))
:extrapreds ((x734))
:extrapreds ((x735))
:extrapreds ((x736))
:extrapreds ((x737))
:extrapreds ((x738))
:extrapreds ((x739))
:extrapreds ((x740))
:extrapreds ((x741))
:extrapreds ((x742))
:extrapreds ((x743))
:extrapreds ((x744))
:extrapreds ((x745))
:extrapreds ((x746))
:extrapreds ((x747))
:extrapreds ((x748))
:extrapreds ((x749))
:extrapreds ((x750))
:extrapreds ((x751))
:extrapreds ((x752))
:extrapreds ((x753))
:extrapreds ((x754))
:extrapreds ((x755))
:extrapreds ((x756))
:extrapreds ((x757))
:extrapreds ((x758))
:extrapreds ((x759))
:extrapreds ((x760))
:extrapreds ((x761))
:extrapreds ((x762))
:extrapreds ((x763))
:extrapreds ((x764))
:extrapreds ((x765))
:extrapreds ((x766))
:extrapreds ((x767))
:extrapreds ((x768))
:extrapreds ((x769))
:extrapreds ((x770))
:extrapreds ((x771))
:extrapreds ((x772))
:extrapreds ((x773))
:extrapreds ((x774))
:extrapreds ((x775))
:extrapreds ((x776))
:extrapreds ((x777))
:extrapreds ((x778))
:extrapreds ((x779))
:extrapreds ((x780))
:extrapreds ((x781))
:extrapreds ((x782))
:extrapreds ((x783))
:extrapreds ((x784))
:extrapreds ((x785))
:extrapreds ((x786))
:extrapreds ((x787))
:extrapreds ((x788))
:extrapreds ((x789))
:extrapreds ((x790))
:extrapreds ((x791))
:extrapreds ((x792))
:extrapreds ((x793))
:extrapreds ((x794))
:extrapreds ((x795))
:extrapreds ((x796))
:extrapreds ((x797))
:extrapreds ((x798))
:extrapreds ((x799))
:extrapreds ((x800))
:extrapreds ((x801))
:extrapreds ((x802))
:extrapreds ((x803))
:extrapreds ((x804))
:extrapreds ((x805))
:extrapreds ((x806))
:extrapreds ((x807))
:extrapreds ((x808))
:extrapreds ((x809))
:extrapreds ((x810))
:extrapreds ((x811))
:extrapreds ((x812))
:extrapreds ((x813))
:extrapreds ((x814))
:extrapreds ((x815))
:extrapreds ((x816))
:extrapreds ((x817))
:extrapreds ((x818))
:extrapreds ((x819))
:extrapreds ((x820))
:extrapreds ((x821))
:extrapreds ((x822))
:extrapreds ((x823))
:extrapreds ((x824))
:extrapreds ((x825))
:extrapreds ((x826))
:extrapreds ((x827))
:extrapreds ((x828))
:extrapreds ((x829))
:extrapreds ((x830))
:extrapreds ((x831))
:extrapreds ((x832))
:extrapreds ((x833))
:extrapreds ((x834))
:extrapreds ((x835))
:extrapreds ((x836))
:extrapreds ((x837))
:extrapreds ((x838))
:extrapreds ((x839))
:extrapreds ((x840))
:extrapreds ((x841))
:extrapreds ((x842))
:extrapreds ((x843))
:extrapreds ((x844))
:extrapreds ((x845))
:extrapreds ((x846))
:extrapreds ((x847))
:extrapreds ((x848))
:extrapreds ((x849))
:extrapreds ((x850))
:extrapreds ((x851))
:extrapreds ((x852))
:extrapreds ((x853))
:extrapreds ((x854))
:extrapreds ((x855))
:extrapreds ((x856))
:extrapreds ((x857))
:extrapreds ((x858))
:extrapreds ((x859))
:extrapreds ((x860))
:extrapreds ((x861))
:extrapreds ((x862))
:extrapreds ((x863))
:extrapreds ((x864))
:extrapreds ((x865))
:extrapreds ((x866))
:extrapreds ((x867))
:extrapreds ((x868))
:extrapreds ((x869))
:extrapreds ((x870))
:extrapreds ((x871))
:extrapreds ((x872))
:extrapreds ((x873))
:extrapreds ((x874))
:extrapreds ((x875))
:extrapreds ((x876))
:extrapreds ((x877))
:extrapreds ((x878))
:extrapreds ((x879))
:extrapreds ((x880))
:extrapreds ((x881))
:extrapreds ((x882))
:extrapreds ((x883))
:extrapreds ((x884))
:extrapreds ((x885))
:extrapreds ((x886))
:extrapreds ((x887))
:extrapreds ((x888))
:extrapreds ((x889))
:extrapreds ((x890))
:extrapreds ((x891))
:extrapreds ((x892))
:extrapreds ((x893))
:extrapreds ((x894))
:extrapreds ((x895))
:extrapreds ((x896))
:extrapreds ((x897))
:extrapreds ((x898))
:extrapreds ((x899))
:extrapreds ((x900))
:extrapreds ((x901))
:extrapreds ((x902))
:extrapreds ((x903))
:extrapreds ((x904))
:extrapreds ((x905))
:extrapreds ((x906))
:extrapreds ((x907))
:extrapreds ((x908))
:extrapreds ((x909))
:extrapreds ((x910))
:extrapreds ((x911))
:extrapreds ((x912))
:extrapreds ((x913))
:extrapreds ((x914))
:extrapreds ((x915))
:extrapreds ((x916))
:extrapreds ((x917))
:extrapreds ((x918))
:extrapreds ((x919))
:extrapreds ((x920))
:extrapreds ((x921))
:extrapreds ((x922))
:extrapreds ((x923))
:extrapreds ((x924))
:extrapreds ((x925))
:extrapreds ((x926))
:extrapreds ((x927))
:extrapreds ((x928))
:extrapreds ((x929))
:extrapreds ((x930))
:extrapreds ((x931))
:extrapreds ((x932))
:extrapreds ((x933))
:extrapreds ((x934))
:extrapreds ((x935))
:extrapreds ((x936))
:extrapreds ((x937))
:extrapreds ((x938))
:extrapreds ((x939))
:extrapreds ((x940))
:extrapreds ((x941))
:extrapreds ((x942))
:extrapreds ((x943))
:extrapreds ((x944))
:extrapreds ((x945))
:extrapreds ((x946))
:extrapreds ((x947))
:extrapreds ((x948))
:extrapreds ((x949))
:extrapreds ((x950))
:extrapreds ((x951))
:extrapreds ((x952))
:extrapreds ((x953))
:extrapreds ((x954))
:extrapreds ((x955))
:extrapreds ((x956))
:extrapreds ((x957))
:extrapreds ((x958))
:extrapreds ((x959))
:extrapreds ((x960))
:extrapreds ((x961))
:extrapreds ((x962))
:extrapreds ((x963))
:extrapreds ((x964))
:extrapreds ((x965))
:extrapreds ((x966))
:extrapreds ((x967))
:extrapreds ((x968))
:extrapreds ((x969))
:extrapreds ((x970))
:extrapreds ((x971))
:extrapreds ((x972))
:extrapreds ((x973))
:extrapreds ((x974))
:extrapreds ((x975))
:extrapreds ((x976))
:extrapreds ((x977))
:extrapreds ((x978))
:extrapreds ((x979))
:extrapreds ((x980))
:extrapreds ((x981))
:extrapreds ((x982))
:extrapreds ((x983))
:extrapreds ((x984))
:extrapreds ((x985))
:extrapreds ((x986))
:extrapreds ((x987))
:extrapreds ((x988))
:extrapreds ((x989))
:extrapreds ((x990))
:extrapreds ((x991))
:extrapreds ((x992))
:extrapreds ((x993))
:extrapreds ((x994))
:extrapreds ((x995))
:extrapreds ((x996))
:extrapreds ((x997))
:extrapreds ((x998))
:extrapreds ((x999))
:extrapreds ((x1000))
:extrapreds ((x1001))
:extrapreds ((x1002))
:extrapreds ((x1003))
:extrapreds ((x1004))
:extrapreds ((x1005))
:extrapreds ((x1006))
:extrapreds ((x1007))
:extrapreds ((x1008))
:extrapreds ((x1009))
:extrapreds ((x1010))
:extrapreds ((x1011))
:extrapreds ((x1012))
:extrapreds ((x1013))
:extrapreds ((x1014))
:extrapreds ((x1015))
:extrapreds ((x1016))
:extrapreds ((x1017))
:extrapreds ((x1018))
:extrapreds ((x1019))
:extrapreds ((x1020))
:extrapreds ((x1021))
:extrapreds ((x1022))
:extrapreds ((x1023))
:extrapreds ((x1024))
:extrapreds ((x1025))
:extrapreds ((x1026))
:extrapreds ((x1027))
:extrapreds ((x1028))
:extrapreds ((x1029))
:extrapreds ((x1030))
:extrapreds ((x1031))
:extrapreds ((x1032))
:extrapreds ((x1033))
:extrapreds ((x1034))
:extrapreds ((x1035))
:extrapreds ((x1036))
:extrapreds ((x1037))
:extrapreds ((x1038))
:extrapreds ((x1039))
:extrapreds ((x1040))
:extrapreds ((x1041))
:extrapreds ((x1042))
:extrapreds ((x1043))
:extrapreds ((x1044))
:extrapreds ((x1045))
:extrapreds ((x1046))
:extrapreds ((x1047))
:extrapreds ((x1048))
:extrapreds ((x1049))
:extrapreds ((x1050))
:extrapreds ((x1051))
:extrapreds ((x1052))
:extrapreds ((x1053))
:extrapreds ((x1054))
:extrapreds ((x1055))
:extrapreds ((x1056))
:extrapreds ((x1057))
:extrapreds ((x1058))
:extrapreds ((x1059))
:extrapreds ((x1060))
:extrapreds ((x1061))
:extrapreds ((x1062))
:extrapreds ((x1063))
:extrapreds ((x1064))
:extrapreds ((x1065))
:extrapreds ((x1066))
:extrapreds ((x1067))
:extrapreds ((x1068))
:extrapreds ((x1069))
:extrapreds ((x1070))
:extrapreds ((x1071))
:extrapreds ((x1072))
:extrapreds ((x1073))
:extrapreds ((x1074))
:extrapreds ((x1075))
:extrapreds ((x1076))
:extrapreds ((x1077))
:extrapreds ((x1078))
:extrapreds ((x1079))
:extrapreds ((x1080))
:extrapreds ((x1081))
:extrapreds ((x1082))
:extrapreds ((x1083))
:extrapreds ((x1084))
:extrapreds ((x1085))
:extrapreds ((x1086))
:extrapreds ((x1087))
:extrapreds ((x1088))
:extrapreds ((x1089))
:extrapreds ((x1090))
:extrapreds ((x1091))
:extrapreds ((x1092))
:extrapreds ((x1093))
:extrapreds ((x1094))
:extrapreds ((x1095))
:extrapreds ((x1096))
:extrapreds ((x1097))
:extrapreds ((x1098))
:extrapreds ((x1099))
:extrapreds ((x1100))
:extrapreds ((x1101))
:extrapreds ((x1102))
:extrapreds ((x1103))
:extrapreds ((x1104))
:extrapreds ((x1105))
:extrapreds ((x1106))
:extrapreds ((x1107))
:extrapreds ((x1108))
:extrapreds ((x1109))
:extrapreds ((x1110))
:extrapreds ((x1111))
:extrapreds ((x1112))
:extrapreds ((x1113))
:extrapreds ((x1114))
:extrapreds ((x1115))
:extrapreds ((x1116))
:extrapreds ((x1117))
:extrapreds ((x1118))
:extrapreds ((x1119))
:extrapreds ((x1120))
:extrapreds ((x1121))
:extrapreds ((x1122))
:extrapreds ((x1123))
:extrapreds ((x1124))
:extrapreds ((x1125))
:extrapreds ((x1126))
:extrapreds ((x1127))
:extrapreds ((x1128))
:extrapreds ((x1129))
:extrapreds ((x1130))
:extrapreds ((x1131))
:extrapreds ((x1132))
:extrapreds ((x1133))
:extrapreds ((x1134))
:extrapreds ((x1135))
:extrapreds ((x1136))
:extrapreds ((x1137))
:extrapreds ((x1138))
:extrapreds ((x1139))
:extrapreds ((x1140))
:extrapreds ((x1141))
:extrapreds ((x1142))
:extrapreds ((x1143))
:extrapreds ((x1144))
:extrapreds ((x1145))
:extrapreds ((x1146))
:extrapreds ((x1147))
:extrapreds ((x1148))
:extrapreds ((x1149))
:extrapreds ((x1150))
:extrapreds ((x1151))
:extrapreds ((x1152))
:extrapreds ((x1153))
:extrapreds ((x1154))
:extrapreds ((x1155))
:extrapreds ((x1156))
:extrapreds ((x1157))
:extrapreds ((x1158))
:extrapreds ((x1159))
:extrapreds ((x1160))
:extrapreds ((x1161))
:extrapreds ((x1162))
:extrapreds ((x1163))
:extrapreds ((x1164))
:extrapreds ((x1165))
:extrapreds ((x1166))
:extrapreds ((x1167))
:extrapreds ((x1168))
:extrapreds ((x1169))
:extrapreds ((x1170))
:extrapreds ((x1171))
:extrapreds ((x1172))
:extrapreds ((x1173))
:extrapreds ((x1174))
:extrapreds ((x1175))
:extrapreds ((x1176))
:extrapreds ((x1177))
:extrapreds ((x1178))
:extrapreds ((x1179))
:extrapreds ((x1180))
:extrapreds ((x1181))
:extrapreds ((x1182))
:extrapreds ((x1183))
:extrapreds ((x1184))
:extrapreds ((x1185))
:extrapreds ((x1186))
:extrapreds ((x1187))
:extrapreds ((x1188))
:extrapreds ((x1189))
:extrapreds ((x1190))
:extrapreds ((x1191))
:extrapreds ((x1192))
:extrapreds ((x1193))
:extrapreds ((x1194))
:extrapreds ((x1195))
:extrapreds ((x1196))
:extrapreds ((x1197))
:extrapreds ((x1198))
:extrapreds ((x1199))
:extrapreds ((x1200))
:extrapreds ((x1201))
:extrapreds ((x1202))
:extrapreds ((x1203))
:extrapreds ((x1204))
:extrapreds ((x1205))
:extrapreds ((x1206))
:extrapreds ((x1207))
:extrapreds ((x1208))
:extrapreds ((x1209))
:extrapreds ((x1210))
:extrapreds ((x1211))
:extrapreds ((x1212))
:extrapreds ((x1213))
:extrapreds ((x1214))
:extrapreds ((x1215))
:extrapreds ((x1216))
:extrapreds ((x1217))
:extrapreds ((x1218))
:extrapreds ((x1219))
:extrapreds ((x1220))
:extrapreds ((x1221))
:extrapreds ((x1222))
:extrapreds ((x1223))
:extrapreds ((x1224))
:extrapreds ((x1225))
:extrapreds ((x1226))
:extrapreds ((x1227))
:extrapreds ((x1228))
:extrapreds ((x1229))
:extrapreds ((x1230))
:extrapreds ((x1231))
:extrapreds ((x1232))
:extrapreds ((x1233))
:extrapreds ((x1234))
:extrapreds ((x1235))
:extrapreds ((x1236))
:extrapreds ((x1237))
:extrapreds ((x1238))
:extrapreds ((x1239))
:extrapreds ((x1240))
:extrapreds ((x1241))
:extrapreds ((x1242))
:extrapreds ((x1243))
:extrapreds ((x1244))
:extrapreds ((x1245))
:extrapreds ((x1246))
:extrapreds ((x1247))
:extrapreds ((x1248))
:extrapreds ((x1249))
:extrapreds ((x1250))
:extrapreds ((x1251))
:extrapreds ((x1252))
:extrapreds ((x1253))
:extrapreds ((x1254))
:extrapreds ((x1255))
:extrapreds ((x1256))
:extrapreds ((x1257))
:extrapreds ((x1258))
:extrapreds ((x1259))
:extrapreds ((x1260))
:extrapreds ((x1261))
:extrapreds ((x1262))
:extrapreds ((x1263))
:extrapreds ((x1264))
:extrapreds ((x1265))
:extrapreds ((x1266))
:extrapreds ((x1267))
:extrapreds ((x1268))
:extrapreds ((x1269))
:extrapreds ((x1270))
:extrapreds ((x1271))
:extrapreds ((x1272))
:extrapreds ((x1273))
:extrapreds ((x1274))
:extrapreds ((x1275))
:extrapreds ((x1276))
:extrapreds ((x1277))
:extrapreds ((x1278))
:extrapreds ((x1279))
:extrapreds ((x1280))
:extrapreds ((x1281))
:extrapreds ((x1282))
:extrapreds ((x1283))
:extrapreds ((x1284))
:extrapreds ((x1285))
:extrapreds ((x1286))
:extrapreds ((x1287))
:extrapreds ((x1288))
:extrapreds ((x1289))
:extrapreds ((x1290))
:extrapreds ((x1291))
:extrapreds ((x1292))
:extrapreds ((x1293))
:extrapreds ((x1294))
:extrapreds ((x1295))
:extrapreds ((x1296))
:extrapreds ((x1297))
:extrapreds ((x1298))
:extrapreds ((x1299))
:extrapreds ((x1300))
:extrapreds ((x1301))
:extrapreds ((x1302))
:extrapreds ((x1303))
:extrapreds ((x1304))
:extrapreds ((x1305))
:extrapreds ((x1306))
:extrapreds ((x1307))
:extrapreds ((x1308))
:extrapreds ((x1309))
:extrapreds ((x1310))
:extrapreds ((x1311))
:extrapreds ((x1312))
:extrapreds ((x1313))
:extrapreds ((x1314))
:extrapreds ((x1315))
:extrapreds ((x1316))
:extrapreds ((x1317))
:extrapreds ((x1318))
:extrapreds ((x1319))
:extrapreds ((x1320))
:extrapreds ((x1321))
:extrapreds ((x1322))
:extrapreds ((x1323))
:extrapreds ((x1324))
:extrapreds ((x1325))
:extrapreds ((x1326))
:extrapreds ((x1327))
:extrapreds ((x1328))
:extrapreds ((x1329))
:extrapreds ((x1330))
:extrapreds ((x1331))
:extrapreds ((x1332))
:extrapreds ((x1333))
:extrapreds ((x1334))
:extrapreds ((x1335))
:extrapreds ((x1336))
:extrapreds ((x1337))
:extrapreds ((x1338))
:extrapreds ((x1339))
:extrapreds ((x1340))
:extrapreds ((x1341))
:extrapreds ((x1342))
:extrapreds ((x1343))
:extrapreds ((x1344))
:extrapreds ((x1345))
:extrapreds ((x1346))
:extrapreds ((x1347))
:extrapreds ((x1348))
:extrapreds ((x1349))
:extrapreds ((x1350))
:extrapreds ((x1351))
:extrapreds ((x1352))
:extrapreds ((x1353))
:extrapreds ((x1354))
:extrapreds ((x1355))
:extrapreds ((x1356))
:extrapreds ((x1357))
:extrapreds ((x1358))
:extrapreds ((x1359))
:extrapreds ((x1360))
:extrapreds ((x1361))
:extrapreds ((x1362))
:extrapreds ((x1363))
:extrapreds ((x1364))
:extrapreds ((x1365))
:extrapreds ((x1366))
:extrapreds ((x1367))
:extrapreds ((x1368))
:extrapreds ((x1369))
:extrapreds ((x1370))
:extrapreds ((x1371))
:extrapreds ((x1372))
:extrapreds ((x1373))
:extrapreds ((x1374))
:extrapreds ((x1375))
:extrapreds ((x1376))
:extrapreds ((x1377))
:extrapreds ((x1378))
:extrapreds ((x1379))
:extrapreds ((x1380))
:extrapreds ((x1381))
:extrapreds ((x1382))
:extrapreds ((x1383))
:extrapreds ((x1384))
:extrapreds ((x1385))
:extrapreds ((x1386))
:extrapreds ((x1387))
:extrapreds ((x1388))
:extrapreds ((x1389))
:extrapreds ((x1390))
:extrapreds ((x1391))
:extrapreds ((x1392))
:extrapreds ((x1393))
:extrapreds ((x1394))
:extrapreds ((x1395))
:extrapreds ((x1396))
:extrapreds ((x1397))
:extrapreds ((x1398))
:extrapreds ((x1399))
:extrapreds ((x1400))
:extrapreds ((x1401))
:extrapreds ((x1402))
:extrapreds ((x1403))
:extrapreds ((x1404))
:extrapreds ((x1405))
:extrapreds ((x1406))
:extrapreds ((x1407))
:extrapreds ((x1408))
:extrapreds ((x1409))
:extrapreds ((x1410))
:extrapreds ((x1411))
:extrapreds ((x1412))
:extrapreds ((x1413))
:extrapreds ((x1414))
:extrapreds ((x1415))
:extrapreds ((x1416))
:extrapreds ((x1417))
:extrapreds ((x1418))
:extrapreds ((x1419))
:extrapreds ((x1420))
:formula (and
(or (not x163))
(or x151)
(or x168)
(or (not x158))
(or (not x171))
(or x143)
(or x177)
(or (not x150))
(or (not x144))
(or x159)
(or (not x176))
(or x149)
(or (not x161))
(or (not x169))
(or x160)
(or x147)
(or x152)
(or (not x157))
(or (not x170))
(or (not x146))
(or x154)
(or (not x175))
(or x145)
(or x162)
(or x167)
(or (not x155))
(or (not x172))
(or (not x148))
(or x166)
(or (not x173))
(or x156)
(or x165)
(or (not x164))
(or (not x174))
(or (not x153))
(or (not x66) x93)
(or x66 (not x93))
(or x65 x92)
(or (not x65) (not x92))
(or x64 x91)
(or (not x64) (not x91))
(or (not x63) x90)
(or x63 (not x90))
(or (not x62) x89)
(or x62 (not x89))
(or x61 x88)
(or (not x61) (not x88))
(or (not x60) x87)
(or x60 (not x87))
(or x59 x86)
(or (not x59) (not x86))
(or (not x58) x85)
(or x58 (not x85))
(or x57 x84)
(or (not x57) (not x84))
(or (not x56) x83)
(or x56 (not x83))
(or x55 x82)
(or (not x55) (not x82))
(or x54 x81)
(or (not x54) (not x81))
(or x53 x80)
(or (not x53) (not x80))
(or (not x52) x79)
(or x52 (not x79))
(or (not x51) x78)
(or x51 (not x78))
(or x50 x77)
(or (not x50) (not x77))
(or x49 x76)
(or (not x49) (not x76))
(or (not x48) x75)
(or x48 (not x75))
(or (not x47) x74)
(or x47 (not x74))
(or (not x142) x490)
(or x142 (not x490))
(or (not x141) x491)
(or x141 (not x491))
(or (not x140) x492)
(or x140 (not x492))
(or (not x139) x493)
(or x139 (not x493))
(or x138 x494)
(or (not x138) (not x494))
(or (not x137) x495)
(or x137 (not x495))
(or (not x136) x496)
(or x136 (not x496))
(or (not x135) x497)
(or x135 (not x497))
(or (not x134) x498)
(or x134 (not x498))
(or x133 x499)
(or (not x133) (not x499))
(or (not x132) x500)
(or x132 (not x500))
(or (not x131) x501)
(or x131 (not x501))
(or (not x130) x502)
(or x130 (not x502))
(or (not x129) x503)
(or x129 (not x503))
(or (not x128) x504)
(or x128 (not x504))
(or (not x505) x506)
(or x505 (not x506))
(or x507 x508)
(or (not x507) (not x508))
(or x509 x510)
(or (not x509) (not x510))
(or (not x511) x512)
(or x511 (not x512))
(or (not x513) x514)
(or x513 (not x514))
(or (not x515) x516)
(or x515 (not x516))
(or (not x517) x518)
(or x517 (not x518))
(or x519 x520)
(or (not x519) (not x520))
(or (not x521) x522)
(or x521 (not x522))
(or (not x523) x524)
(or x523 (not x524))
(or x525 x526)
(or (not x525) (not x526))
(or x527 x528)
(or (not x527) (not x528))
(or (not x529) x530)
(or x529 (not x530))
(or (not x531) x532)
(or x531 (not x532))
(or x533 x534)
(or (not x533) (not x534))
(or x535 x536)
(or (not x535) (not x536))
(or x537 x538)
(or (not x537) (not x538))
(or (not x539) x540)
(or x539 (not x540))
(or x541 x542)
(or (not x541) (not x542))
(or (not x543) x544)
(or x543 (not x544))
(or (not x545) x546)
(or x545 (not x546))
(or x547 x548)
(or (not x547) (not x548))
(or (not x549) x550)
(or x549 (not x550))
(or (not x551) x552)
(or x551 (not x552))
(or x553 x554)
(or (not x553) (not x554))
(or (not x555) x556)
(or x555 (not x556))
(or x557 x558)
(or (not x557) (not x558))
(or (not x559) x560)
(or x559 (not x560))
(or x561 x562)
(or (not x561) (not x562))
(or x563 x564)
(or (not x563) (not x564))
(or (not x565) x566)
(or x565 (not x566))
(or x567 x568)
(or (not x567) (not x568))
(or x569 x570)
(or (not x569) (not x570))
(or (not x571) x572)
(or x571 (not x572))
(or x573 x574)
(or (not x573) (not x574))
(or (not x575) x576)
(or x575 (not x576))
(or x577 x578)
(or (not x577) (not x578))
(or (not x579) x580)
(or x579 (not x580))
(or (not x581) x582)
(or x581 (not x582))
(or (not x583) x584)
(or x583 (not x584))
(or x585 x586)
(or (not x585) (not x586))
(or x587 x588)
(or (not x587) (not x588))
(or (not x589) x590)
(or x589 (not x590))
(or x591 x592)
(or (not x591) (not x592))
(or x593 x594)
(or (not x593) (not x594))
(or (not x595) x596)
(or x595 (not x596))
(or x597 x598)
(or (not x597) (not x598))
(or (not x599) x600)
(or x599 (not x600))
(or x601 x602)
(or (not x601) (not x602))
(or (not x603) x604)
(or x603 (not x604))
(or (not x605) x606)
(or x605 (not x606))
(or (not x608) x609)
(or x608 (not x609))
(or (not x611) x612)
(or x611 (not x612))
(or x614 x615)
(or (not x614) (not x615))
(or (not x617) x618)
(or x617 (not x618))
(or x620 x621)
(or (not x620) (not x621))
(or x623 x624)
(or (not x623) (not x624))
(or x626 x627)
(or (not x626) (not x627))
(or (not x202) x628)
(or x202 (not x628))
(or x203 x629)
(or (not x203) (not x629))
(or x204 x630)
(or (not x204) (not x630))
(or (not x205) x631)
(or x205 (not x631))
(or x206 x632)
(or (not x206) (not x632))
(or x633 x634)
(or (not x633) (not x634))
(or x636 x637)
(or (not x636) (not x637))
(or x639 x640)
(or (not x639) (not x640))
(or (not x643) x644)
(or x643 (not x644))
(or x647 x648)
(or (not x647) (not x648))
(or (not x651) x652)
(or x651 (not x652))
(or (not x656) x657)
(or x656 (not x657))
(or x661 x662)
(or (not x661) (not x662))
(or x666 x667)
(or (not x666) (not x667))
(or (not x671) x672)
(or x671 (not x672))
(or (not x676) x677)
(or x676 (not x677))
(or x681 x682)
(or (not x681) (not x682))
(or x686 x687)
(or (not x686) (not x687))
(or (not x691) x692)
(or x691 (not x692))
(or (not x696) x697)
(or x696 (not x697))
(or x701 x702)
(or (not x701) (not x702))
(or (not x706) x707)
(or x706 (not x707))
(or (not x711) x712)
(or x711 (not x712))
(or x716 x717)
(or (not x716) (not x717))
(or (not x721) x722)
(or x721 (not x722))
(or (not x726) x727)
(or x726 (not x727))
(or (not x731) x732)
(or x731 (not x732))
(or (not x736) x737)
(or x736 (not x737))
(or (not x741) x742)
(or x741 (not x742))
(or x746 x747)
(or (not x746) (not x747))
(or (not x751) x752)
(or x751 (not x752))
(or (not x756) x757)
(or x756 (not x757))
(or (not x761) x762)
(or x761 (not x762))
(or x767 x768)
(or (not x767) (not x768))
(or (not x773) x774)
(or x773 (not x774))
(or (not x780) x781)
(or x780 (not x781))
(or x787 x788)
(or (not x787) (not x788))
(or x794 x795)
(or (not x794) (not x795))
(or (not x801) x802)
(or x801 (not x802))
(or x808 x809)
(or (not x808) (not x809))
(or (not x815) x816)
(or x815 (not x816))
(or (not x822) x823)
(or x822 (not x823))
(or x829 x830)
(or (not x829) (not x830))
(or (not x836) x837)
(or x836 (not x837))
(or x843 x844)
(or (not x843) (not x844))
(or (not x850) x851)
(or x850 (not x851))
(or x857 x858)
(or (not x857) (not x858))
(or x864 x865)
(or (not x864) (not x865))
(or (not x871) x872)
(or x871 (not x872))
(or x878 x879)
(or (not x878) (not x879))
(or (not x885) x886)
(or x885 (not x886))
(or (not x892) x893)
(or x892 (not x893))
(or x899 x900)
(or (not x899) (not x900))
(or x906 x907)
(or (not x906) (not x907))
(or (not x913) x914)
(or x913 (not x914))
(or (not x922) x923)
(or x922 (not x923))
(or (not x937) x938)
(or x937 (not x938))
(or x950 x951)
(or (not x950) (not x951))
(or x962 x963)
(or (not x962) (not x963))
(or (not x975) x976)
(or x975 (not x976))
(or x989 x990)
(or (not x989) (not x990))
(or (not x1003) x1004)
(or x1003 (not x1004))
(or (not x1020) x1021)
(or x1020 (not x1021))
(or (not x1036) x1037)
(or x1036 (not x1037))
(or (not x1051) x1052)
(or x1051 (not x1052))
(or x1068 x1069)
(or (not x1068) (not x1069))
(or x1083 x1084)
(or (not x1083) (not x1084))
(or x1099 x1100)
(or (not x1099) (not x1100))
(or x1116 x1117)
(or (not x1116) (not x1117))
(or (not x1133) x1134)
(or x1133 (not x1134))
(or x1150 x1151)
(or (not x1150) (not x1151))
(or x1168 x1169)
(or (not x1168) (not x1169))
(or (not x1184) x1185)
(or x1184 (not x1185))
(or x1203 x1204)
(or (not x1203) (not x1204))
(or x1221 x1222)
(or (not x1221) (not x1222))
(or (not x1242) x1243)
(or x1242 (not x1243))
(or (not x1263) x1264)
(or x1263 (not x1264))
(or x1283 x1284)
(or (not x1283) (not x1284))
(or (not x1306) x1307)
(or x1306 (not x1307))
(or x1326 x1327)
(or (not x1326) (not x1327))
(or (not x1350) x1351)
(or x1350 (not x1351))
(or (not x1370) x1371)
(or x1370 (not x1371))
(or x1394 x1395)
(or (not x1394) (not x1395))
(or x1419 x1420)
(or (not x1419) (not x1420))
(or (not x1049) x1043 x1044)
(or x1049 (not x1043) x1044)
(or x1049 x1043 (not x1044))
(or (not x1049) (not x1043) (not x1044))
(or (not x227) x51)
(or (not x227) (not x51) x52)
(or x227 (not x51) (not x52))
(or (not x328) x64)
(or (not x328) (not x64) x88)
(or x328 (not x64) (not x88) (not x89))
(or (not x328) (not x64) (not x88) x89)
(or (not x808) x806 x807)
(or x808 (not x806) x807)
(or x808 x806 (not x807))
(or (not x808) (not x806) (not x807))
(or (not x351) x85)
(or (not x351) (not x85) x86)
(or x351 (not x85) (not x86) (not x88))
(or (not x351) (not x85) (not x86) x88)
(or (not x553) x7 x34)
(or x553 (not x7) x34)
(or x553 x7 (not x34))
(or (not x553) (not x7) (not x34))
(or (not x277) x26)
(or (not x277) (not x26) x27)
(or x277 (not x26) (not x27))
(or (not x1411) x54 x64)
(or x1411 (not x54) x64)
(or x1411 x54 (not x64))
(or (not x1411) (not x54) (not x64))
(or (not x1350) x1348 x1349)
(or x1350 (not x1348) x1349)
(or x1350 x1348 (not x1349))
(or (not x1350) (not x1348) (not x1349))
(or (not x1408) x1398 x1399)
(or x1408 (not x1398) x1399)
(or x1408 x1398 (not x1399))
(or (not x1408) (not x1398) (not x1399))
(or (not x1377) x478 x479)
(or x1377 (not x478) x479)
(or x1377 x478 (not x479))
(or (not x1377) (not x478) (not x479))
(or (not x948) x942 x943)
(or x948 (not x942) x943)
(or x948 x942 (not x943))
(or (not x948) (not x942) (not x943))
(or (not x352) x5)
(or (not x352) (not x5) x6)
(or x352 (not x5) (not x6))
(or (not x690) x117 x129)
(or x690 (not x117) x129)
(or x690 x117 (not x129))
(or (not x690) (not x117) (not x129))
(or (not x1292) x1288 x1289)
(or x1292 (not x1288) x1289)
(or x1292 x1288 (not x1289))
(or (not x1292) (not x1288) (not x1289))
(or (not x766) x763 x764)
(or x766 (not x763) x764)
(or x766 x763 (not x764))
(or (not x766) (not x763) (not x764))
(or (not x1168) x1159 x1160)
(or x1168 (not x1159) x1160)
(or x1168 x1159 (not x1160))
(or (not x1168) (not x1159) (not x1160))
(or (not x969) x332 x333)
(or x969 (not x332) x333)
(or x969 x332 (not x333))
(or (not x969) (not x332) (not x333))
(or (not x1104) x301 x394)
(or x1104 (not x301) x394)
(or x1104 x301 (not x394))
(or (not x1104) (not x301) (not x394))
(or (not x952) x194 x206)
(or x952 (not x194) x206)
(or x952 x194 (not x206))
(or (not x952) (not x194) (not x206))
(or (not x1355) x219 x225)
(or x1355 (not x219) x225)
(or x1355 x219 (not x225))
(or (not x1355) (not x219) (not x225))
(or (not x947) x205 x256)
(or x947 (not x205) x256)
(or x947 x205 (not x256))
(or (not x947) (not x205) (not x256))
(or (not x1314) x1309 x1310)
(or x1314 (not x1309) x1310)
(or x1314 x1309 (not x1310))
(or (not x1314) (not x1309) (not x1310))
(or (not x1310) x70 x98)
(or x1310 (not x70) x98)
(or x1310 x70 (not x98))
(or (not x1310) (not x70) (not x98))
(or (not x1157) x417 x1152)
(or x1157 (not x417) x1152)
(or x1157 x417 (not x1152))
(or (not x1157) (not x417) (not x1152))
(or (not x1155) x229 x284)
(or x1155 (not x229) x284)
(or x1155 x229 (not x284))
(or (not x1155) (not x229) (not x284))
(or (not x341) x62)
(or (not x341) (not x62) x88)
(or x341 (not x62) (not x88))
(or (not x1114) x395 x396)
(or x1114 (not x395) x396)
(or x1114 x395 (not x396))
(or (not x1114) (not x395) (not x396))
(or (not x383) x56)
(or (not x383) (not x56) x82)
(or x383 (not x56) (not x82))
(or (not x1296) x1286 x1287)
(or x1296 (not x1286) x1287)
(or x1296 x1286 (not x1287))
(or (not x1296) (not x1286) (not x1287))
(or (not x892) x890 x891)
(or x892 (not x890) x891)
(or x892 x890 (not x891))
(or (not x892) (not x890) (not x891))
(or (not x769) x116 x210)
(or x769 (not x116) x210)
(or x769 x116 (not x210))
(or (not x769) (not x116) (not x210))
(or (not x573) x24 x93)
(or x573 (not x24) x93)
(or x573 x24 (not x93))
(or (not x573) (not x24) (not x93))
(or (not x1045) x366 x367)
(or x1045 (not x366) x367)
(or x1045 x366 (not x367))
(or (not x1045) (not x366) (not x367))
(or (not x609) x142 x180)
(or x609 (not x142) x180)
(or x609 x142 (not x180))
(or (not x609) (not x142) (not x180))
(or (not x358) x84)
(or (not x358) (not x84) x85)
(or x358 (not x84) (not x85) (not x87))
(or (not x358) (not x84) (not x85) x87)
(or (not x427) x49)
(or (not x427) (not x49) x73)
(or x427 (not x49) (not x73) (not x74))
(or (not x427) (not x49) (not x73) x74)
(or (not x679) x495 x678)
(or x679 (not x495) x678)
(or x679 x495 (not x678))
(or (not x679) (not x495) (not x678))
(or (not x1195) x427 x428)
(or x1195 (not x427) x428)
(or x1195 x427 (not x428))
(or (not x1195) (not x427) (not x428))
(or (not x673) x135 x202)
(or x673 (not x135) x202)
(or x673 x135 (not x202))
(or (not x673) (not x135) (not x202))
(or (not x920) x918 x919)
(or x920 (not x918) x919)
(or x920 x918 (not x919))
(or (not x920) (not x918) (not x919))
(or (not x1303) x213 x219)
(or x1303 (not x213) x219)
(or x1303 x213 (not x219))
(or (not x1303) (not x213) (not x219))
(or (not x989) x987 x988)
(or x989 (not x987) x988)
(or x989 x987 (not x988))
(or (not x989) (not x987) (not x988))
(or (not x357) x84)
(or (not x357) (not x84) x85)
(or x357 (not x84) (not x85) (not x86))
(or (not x357) (not x84) (not x85) x86)
(or (not x980) x341 x342)
(or x980 (not x341) x342)
(or x980 x341 (not x342))
(or (not x980) (not x341) (not x342))
(or (not x217) x56)
(or (not x217) (not x56) x57)
(or x217 (not x56) (not x57))
(or (not x729) x505 x728)
(or x729 (not x505) x728)
(or x729 x505 (not x728))
(or (not x729) (not x505) (not x728))
(or (not x946) x944 x945)
(or x946 (not x944) x945)
(or x946 x944 (not x945))
(or (not x946) (not x944) (not x945))
(or (not x912) x250 x273)
(or x912 (not x250) x273)
(or x912 x250 (not x273))
(or (not x912) (not x250) (not x273))
(or (not x1138) x305 x406)
(or x1138 (not x305) x406)
(or x1138 x305 (not x406))
(or (not x1138) (not x305) (not x406))
(or (not x1137) x203 x206)
(or x1137 (not x203) x206)
(or x1137 x203 (not x206))
(or (not x1137) (not x203) (not x206))
(or (not x566) x97 x112)
(or x566 (not x97) x112)
(or x566 x97 (not x112))
(or (not x566) (not x97) (not x112))
(or (not x830) x825 x826)
(or x830 (not x825) x826)
(or x830 x825 (not x826))
(or (not x830) (not x825) (not x826))
(or (not x356) x60)
(or (not x356) (not x60) x84)
(or x356 (not x60) (not x84) (not x85))
(or (not x356) (not x60) (not x84) x85)
(or (not x829) x827 x828)
(or x829 (not x827) x828)
(or x829 x827 (not x828))
(or (not x829) (not x827) (not x828))
(or (not x1067) x1064 x1065)
(or x1067 (not x1064) x1065)
(or x1067 x1064 (not x1065))
(or (not x1067) (not x1064) (not x1065))
(or (not x437) x46)
(or (not x437) (not x46) x74)
(or x437 (not x46) (not x74))
(or (not x1062) x1058 x1059)
(or x1062 (not x1058) x1059)
(or x1062 x1058 (not x1059))
(or (not x1062) (not x1058) (not x1059))
(or (not x723) x125 x215)
(or x723 (not x125) x215)
(or x723 x125 (not x215))
(or (not x723) (not x125) (not x215))
(or (not x1199) x1187 x1188)
(or x1199 (not x1187) x1188)
(or x1199 x1187 (not x1188))
(or (not x1199) (not x1187) (not x1188))
(or (not x866) x129 x184)
(or x866 (not x129) x184)
(or x866 x129 (not x184))
(or (not x866) (not x129) (not x184))
(or (not x515) x26 x53)
(or x515 (not x26) x53)
(or x515 x26 (not x53))
(or (not x515) (not x26) (not x53))
(or (not x579) x21 x90)
(or x579 (not x21) x90)
(or x579 x21 (not x90))
(or (not x579) (not x21) (not x90))
(or (not x1240) x1236 x1237)
(or x1240 (not x1236) x1237)
(or x1240 x1236 (not x1237))
(or (not x1240) (not x1236) (not x1237))
(or (not x199) x70)
(or (not x199) (not x70) x71)
(or x199 (not x70) (not x71))
(or (not x343) x86)
(or (not x343) (not x86) x87)
(or x343 (not x86) (not x87) (not x88))
(or (not x343) (not x86) (not x87) x88)
(or (not x471) x66)
(or (not x471) (not x66) x67)
(or x471 (not x66) (not x67) (not x69))
(or (not x471) (not x66) (not x67) x69)
(or (not x590) x100 x186)
(or x590 (not x100) x186)
(or x590 x100 (not x186))
(or (not x590) (not x100) (not x186))
(or (not x295) x17)
(or (not x295) (not x17) x18)
(or x295 (not x17) (not x18))
(or (not x957) x326 x327)
(or x957 (not x326) x327)
(or x957 x326 (not x327))
(or (not x957) (not x326) (not x327))
(or (not x1244) x8 x32)
(or x1244 (not x8) x32)
(or x1244 x8 (not x32))
(or (not x1244) (not x8) (not x32))
(or (not x556) x102 x117)
(or x556 (not x102) x117)
(or x556 x102 (not x117))
(or (not x556) (not x102) (not x117))
(or (not x264) x114)
(or (not x264) (not x114) x115)
(or x264 (not x114) (not x115))
(or (not x225) x52)
(or (not x225) (not x52) x53)
(or x225 (not x52) (not x53))
(or (not x1105) x397 x398)
(or x1105 (not x397) x398)
(or x1105 x397 (not x398))
(or (not x1105) (not x397) (not x398))
(or (not x1193) x53 x62)
(or x1193 (not x53) x62)
(or x1193 x53 (not x62))
(or (not x1193) (not x53) (not x62))
(or (not x1164) x1153 x1154)
(or x1164 (not x1153) x1154)
(or x1164 x1153 (not x1154))
(or (not x1164) (not x1153) (not x1154))
(or (not x1021) x1018 x1019)
(or x1021 (not x1018) x1019)
(or x1021 x1018 (not x1019))
(or (not x1021) (not x1018) (not x1019))
(or (not x333) x62)
(or (not x333) (not x62) x90)
(or x333 (not x62) (not x90))
(or (not x1415) x633 x1406)
(or x1415 (not x633) x1406)
(or x1415 x633 (not x1406))
(or (not x1415) (not x633) (not x1406))
(or (not x1061) x379 x1053)
(or x1061 (not x379) x1053)
(or x1061 x379 (not x1053))
(or (not x1061) (not x379) (not x1053))
(or (not x617) x198 x616)
(or x617 (not x198) x616)
(or x617 x198 (not x616))
(or (not x617) (not x198) (not x616))
(or (not x1204) x1201 x1202)
(or x1204 (not x1201) x1202)
(or x1204 x1201 (not x1202))
(or (not x1204) (not x1201) (not x1202))
(or (not x1185) x1178 x1179)
(or x1185 (not x1178) x1179)
(or x1185 x1178 (not x1179))
(or (not x1185) (not x1178) (not x1179))
(or (not x287) x21)
(or (not x287) (not x21) x22)
(or x287 (not x21) (not x22))
(or (not x1299) x58 x69)
(or x1299 (not x58) x69)
(or x1299 x58 (not x69))
(or (not x1299) (not x58) (not x69))
(or (not x1401) x486 x487)
(or x1401 (not x486) x487)
(or x1401 x486 (not x487))
(or (not x1401) (not x486) (not x487))
(or (not x607) x7 x76)
(or x607 (not x7) x76)
(or x607 x7 (not x76))
(or (not x607) (not x7) (not x76))
(or (not x1404) x1402 x1403)
(or x1404 (not x1402) x1403)
(or x1404 x1402 (not x1403))
(or (not x1404) (not x1402) (not x1403))
(or (not x510) x125 x140)
(or x510 (not x125) x140)
(or x510 x125 (not x140))
(or (not x510) (not x125) (not x140))
(or (not x1265) x7 x31)
(or x1265 (not x7) x31)
(or x1265 x7 (not x31))
(or (not x1265) (not x7) (not x31))
(or (not x815) x813 x814)
(or x815 (not x813) x814)
(or x815 x813 (not x814))
(or (not x815) (not x813) (not x814))
(or (not x1307) x1302 x1303)
(or x1307 (not x1302) x1303)
(or x1307 x1302 (not x1303))
(or (not x1307) (not x1302) (not x1303))
(or (not x1345) x1338 x1339)
(or x1345 (not x1338) x1339)
(or x1345 x1338 (not x1339))
(or (not x1345) (not x1338) (not x1339))
(or (not x593) x14 x83)
(or x593 (not x14) x83)
(or x593 x14 (not x83))
(or (not x593) (not x14) (not x83))
(or (not x932) x929 x930)
(or x932 (not x929) x930)
(or x932 x929 (not x930))
(or (not x932) (not x929) (not x930))
(or (not x289) x20)
(or (not x289) (not x20) x21)
(or x289 (not x20) (not x21))
(or (not x1173) x418 x419)
(or x1173 (not x418) x419)
(or x1173 x418 (not x419))
(or (not x1173) (not x418) (not x419))
(or (not x1294) x135 x200)
(or x1294 (not x135) x200)
(or x1294 x135 (not x200))
(or (not x1294) (not x135) (not x200))
(or (not x364) x83)
(or (not x364) (not x83) x84)
(or x364 (not x83) (not x84) (not x85))
(or (not x364) (not x83) (not x84) x85)
(or (not x1263) x1261 x1262)
(or x1263 (not x1261) x1262)
(or x1263 x1261 (not x1262))
(or (not x1263) (not x1261) (not x1262))
(or (not x763) x117 x142)
(or x763 (not x117) x142)
(or x763 x117 (not x142))
(or (not x763) (not x117) (not x142))
(or (not x677) x225 x226)
(or x677 (not x225) x226)
(or x677 x225 (not x226))
(or (not x677) (not x225) (not x226))
(or (not x1201) x324 x424)
(or x1201 (not x324) x424)
(or x1201 x324 (not x424))
(or (not x1201) (not x324) (not x424))
(or (not x517) x25 x52)
(or x517 (not x25) x52)
(or x517 x25 (not x52))
(or (not x517) (not x25) (not x52))
(or (not x450) x45)
(or (not x450) (not x45) x71)
(or x450 (not x45) (not x71))
(or (not x994) x348 x349)
(or x994 (not x348) x349)
(or x994 x348 (not x349))
(or (not x994) (not x348) (not x349))
(or (not x781) x776 x777)
(or x781 (not x776) x777)
(or x781 x776 (not x777))
(or (not x781) (not x776) (not x777))
(or (not x907) x902 x903)
(or x907 (not x902) x903)
(or x907 x902 (not x903))
(or (not x907) (not x902) (not x903))
(or (not x459) x68)
(or (not x459) (not x68) x69)
(or x459 (not x68) (not x69) (not x71))
(or (not x459) (not x68) (not x69) x71)
(or (not x269) x30)
(or (not x269) (not x30) x31)
(or x269 (not x30) (not x31))
(or (not x713) x127 x211)
(or x713 (not x127) x211)
(or x713 x127 (not x211))
(or (not x713) (not x127) (not x211))
(or (not x715) x112 x124)
(or x715 (not x112) x124)
(or x715 x112 (not x124))
(or (not x715) (not x112) (not x124))
(or (not x911) x561 x908)
(or x911 (not x561) x908)
(or x911 x561 (not x908))
(or (not x911) (not x561) (not x908))
(or (not x1090) x1087 x1088)
(or x1090 (not x1087) x1088)
(or x1090 x1087 (not x1088))
(or (not x1090) (not x1087) (not x1088))
(or (not x641) x127 x139)
(or x641 (not x127) x139)
(or x641 x127 (not x139))
(or (not x641) (not x127) (not x139))
(or (not x457) x44)
(or (not x457) (not x44) x68)
(or x457 (not x44) (not x68) (not x69))
(or (not x457) (not x44) (not x68) x69)
(or (not x800) x218 x241)
(or x800 (not x218) x241)
(or x800 x218 (not x241))
(or (not x800) (not x218) (not x241))
(or (not x801) x799 x800)
(or x801 (not x799) x800)
(or x801 x799 (not x800))
(or (not x801) (not x799) (not x800))
(or (not x330) x88)
(or (not x330) (not x88) x89)
(or x330 (not x88) (not x89) (not x91))
(or (not x330) (not x88) (not x89) x91)
(or (not x885) x883 x884)
(or x885 (not x883) x884)
(or x885 x883 (not x884))
(or (not x885) (not x883) (not x884))
(or (not x913) x911 x912)
(or x913 (not x911) x912)
(or x913 x911 (not x912))
(or (not x913) (not x911) (not x912))
(or (not x1029) x291 x359)
(or x1029 (not x291) x359)
(or x1029 x291 (not x359))
(or (not x1029) (not x291) (not x359))
(or (not x843) x841 x842)
(or x843 (not x841) x842)
(or x843 x841 (not x842))
(or (not x843) (not x841) (not x842))
(or (not x391) x55)
(or (not x391) (not x55) x79)
(or x391 (not x55) (not x79) (not x80))
(or (not x391) (not x55) (not x79) x80)
(or (not x749) x513 x748)
(or x749 (not x513) x748)
(or x749 x513 (not x748))
(or (not x749) (not x513) (not x748))
(or (not x503) x33 x60)
(or x503 (not x33) x60)
(or x503 x33 (not x60))
(or (not x503) (not x33) (not x60))
(or (not x1145) x107 x194)
(or x1145 (not x107) x194)
(or x1145 x107 (not x194))
(or (not x1145) (not x107) (not x194))
(or (not x463) x43)
(or (not x463) (not x43) x67)
(or x463 (not x43) (not x67) (not x68))
(or (not x463) (not x43) (not x67) x68)
(or (not x1117) x1114 x1115)
(or x1117 (not x1114) x1115)
(or x1117 x1114 (not x1115))
(or (not x1117) (not x1114) (not x1115))
(or (not x1309) x47 x56)
(or x1309 (not x47) x56)
(or x1309 x47 (not x56))
(or (not x1309) (not x47) (not x56))
(or (not x764) x262 x519)
(or x764 (not x262) x519)
(or x764 x262 (not x519))
(or (not x764) (not x262) (not x519))
(or (not x371) x82)
(or (not x371) (not x82) x83)
(or x371 (not x82) (not x83) (not x84))
(or (not x371) (not x82) (not x83) x84)
(or (not x541) x13 x40)
(or x541 (not x13) x40)
(or x541 x13 (not x40))
(or (not x541) (not x13) (not x40))
(or (not x943) x120 x179)
(or x943 (not x120) x179)
(or x943 x120 (not x179))
(or (not x943) (not x120) (not x179))
(or (not x1092) x299 x387)
(or x1092 (not x299) x387)
(or x1092 x299 (not x387))
(or (not x1092) (not x299) (not x387))
(or (not x1009) x356 x357)
(or x1009 (not x356) x357)
(or x1009 x356 (not x357))
(or (not x1009) (not x356) (not x357))
(or (not x949) x322 x323)
(or x949 (not x322) x323)
(or x949 x322 (not x323))
(or (not x949) (not x322) (not x323))
(or (not x760) x103 x115)
(or x760 (not x103) x115)
(or x760 x103 (not x115))
(or (not x760) (not x103) (not x115))
(or (not x187) x82)
(or (not x187) (not x82) x83)
(or x187 (not x82) (not x83))
(or (not x631) x132 x190)
(or x631 (not x132) x190)
(or x631 x132 (not x190))
(or (not x631) (not x132) (not x190))
(or (not x411) x76)
(or (not x411) (not x76) x77)
(or x411 (not x76) (not x77) (not x79))
(or (not x411) (not x76) (not x77) x79)
(or (not x670) x121 x133)
(or x670 (not x121) x133)
(or x670 x121 (not x133))
(or (not x670) (not x121) (not x133))
(or (not x1333) x466 x467)
(or x1333 (not x466) x467)
(or x1333 x466 (not x467))
(or (not x1333) (not x466) (not x467))
(or (not x845) x132 x181)
(or x845 (not x132) x181)
(or x845 x132 (not x181))
(or (not x845) (not x132) (not x181))
(or (not x549) x9 x36)
(or x549 (not x9) x36)
(or x549 x9 (not x36))
(or (not x549) (not x9) (not x36))
(or (not x410) x76)
(or (not x410) (not x76) x77)
(or x410 (not x76) (not x77) (not x78))
(or (not x410) (not x76) (not x77) x78)
(or (not x535) x16 x43)
(or x535 (not x16) x43)
(or x535 x16 (not x43))
(or (not x535) (not x16) (not x43))
(or (not x184) x85)
(or (not x184) (not x85) x86)
(or x184 (not x85) (not x86))
(or (not x1246) x101 x137)
(or x1246 (not x101) x137)
(or x1246 x101 (not x137))
(or (not x1246) (not x101) (not x137))
(or (not x789) x113 x140)
(or x789 (not x113) x140)
(or x789 x113 (not x140))
(or (not x789) (not x113) (not x140))
(or (not x245) x42)
(or (not x245) (not x42) x43)
(or x245 (not x42) (not x43))
(or (not x1073) x382 x383)
(or x1073 (not x382) x383)
(or x1073 x382 (not x383))
(or (not x1073) (not x382) (not x383))
(or (not x757) x257 x258)
(or x757 (not x257) x258)
(or x757 x257 (not x258))
(or (not x757) (not x257) (not x258))
(or (not x1361) x473 x474)
(or x1361 (not x473) x474)
(or x1361 x473 (not x474))
(or (not x1361) (not x473) (not x474))
(or (not x605) x8 x77)
(or x605 (not x8) x77)
(or x605 x8 (not x77))
(or (not x605) (not x8) (not x77))
(or (not x189) x80)
(or (not x189) (not x80) x81)
(or x189 (not x80) (not x81))
(or (not x282) x105)
(or (not x282) (not x105) x106)
(or x282 (not x105) (not x106))
(or (not x293) x18)
(or (not x293) (not x18) x19)
(or x293 (not x18) (not x19))
(or (not x945) x940 x941)
(or x945 (not x940) x941)
(or x945 x940 (not x941))
(or (not x945) (not x940) (not x941))
(or (not x1005) x22 x46)
(or x1005 (not x22) x46)
(or x1005 x22 (not x46))
(or (not x1005) (not x22) (not x46))
(or (not x568) x96 x111)
(or x568 (not x96) x111)
(or x568 x96 (not x111))
(or (not x568) (not x96) (not x111))
(or (not x899) x897 x898)
(or x899 (not x897) x898)
(or x899 x897 (not x898))
(or (not x899) (not x897) (not x898))
(or (not x741) x739 x740)
(or x741 (not x739) x740)
(or x741 x739 (not x740))
(or (not x741) (not x739) (not x740))
(or (not x770) x264 x521)
(or x770 (not x264) x521)
(or x770 x264 (not x521))
(or (not x770) (not x264) (not x521))
(or (not x399) x78)
(or (not x399) (not x78) x79)
(or x399 (not x78) (not x79) (not x81))
(or (not x399) (not x78) (not x79) x81)
(or (not x611) x196 x610)
(or x611 (not x196) x610)
(or x611 x196 (not x610))
(or (not x611) (not x196) (not x610))
(or (not x1419) x1411 x936)
(or x1419 (not x1411) x936)
(or x1419 x1411 (not x936))
(or (not x1419) (not x1411) (not x936))
(or (not x431) x47)
(or (not x431) (not x47) x75)
(or x431 (not x47) (not x75))
(or (not x491) x45 x72)
(or x491 (not x45) x72)
(or x491 x45 (not x72))
(or (not x491) (not x45) (not x72))
(or (not x449) x44)
(or (not x449) (not x44) x72)
(or x449 (not x44) (not x72))
(or (not x696) x694 x695)
(or x696 (not x694) x695)
(or x696 x694 (not x695))
(or (not x696) (not x694) (not x695))
(or (not x893) x888 x889)
(or x893 (not x888) x889)
(or x893 x888 (not x889))
(or (not x893) (not x888) (not x889))
(or (not x505) x31 x58)
(or x505 (not x31) x58)
(or x505 x31 (not x58))
(or (not x505) (not x31) (not x58))
(or (not x448) x44)
(or (not x448) (not x44) x70)
(or x448 (not x44) (not x70) (not x71))
(or (not x448) (not x44) (not x70) x71)
(or (not x1213) x433 x434)
(or x1213 (not x433) x434)
(or x1213 x433 (not x434))
(or (not x1213) (not x433) (not x434))
(or (not x1118) x15 x39)
(or x1118 (not x15) x39)
(or x1118 x15 (not x39))
(or (not x1118) (not x15) (not x39))
(or (not x527) x20 x47)
(or x527 (not x20) x47)
(or x527 x20 (not x47))
(or (not x527) (not x20) (not x47))
(or (not x320) x65)
(or (not x320) (not x65) x91)
(or x320 (not x65) (not x91))
(or (not x645) x126 x138)
(or x645 (not x126) x138)
(or x645 x126 (not x138))
(or (not x645) (not x126) (not x138))
(or (not x879) x874 x875)
(or x879 (not x874) x875)
(or x879 x874 (not x875))
(or (not x879) (not x874) (not x875))
(or (not x1003) x1001 x1002)
(or x1003 (not x1001) x1002)
(or x1003 x1001 (not x1002))
(or (not x1003) (not x1001) (not x1002))
(or (not x475) x41)
(or (not x475) (not x41) x65)
(or x475 (not x41) (not x65) (not x66))
(or (not x475) (not x41) (not x65) x66)
(or (not x530) x115 x130)
(or x530 (not x115) x130)
(or x530 x115 (not x130))
(or (not x530) (not x115) (not x130))
(or (not x1347) x204 x217)
(or x1347 (not x204) x217)
(or x1347 x204 (not x217))
(or (not x1347) (not x204) (not x217))
(or (not x276) x108)
(or (not x276) (not x108) x109)
(or x276 (not x108) (not x109))
(or (not x1304) x1298 x1299)
(or x1304 (not x1298) x1299)
(or x1304 x1298 (not x1299))
(or (not x1304) (not x1298) (not x1299))
(or (not x342) x62)
(or (not x342) (not x62) x86)
(or x342 (not x62) (not x86) (not x87))
(or (not x342) (not x62) (not x86) x87)
(or (not x798) x97 x109)
(or x798 (not x97) x109)
(or x798 x97 (not x109))
(or (not x798) (not x97) (not x109))
(or (not x408) x52)
(or (not x408) (not x52) x78)
(or x408 (not x52) (not x78))
(or (not x648) x645 x646)
(or x648 (not x645) x646)
(or x648 x645 (not x646))
(or (not x648) (not x645) (not x646))
(or (not x309) x11)
(or (not x309) (not x11) x12)
(or x309 (not x11) (not x12))
(or (not x1017) x1014 x1015)
(or x1017 (not x1014) x1015)
(or x1017 x1014 (not x1015))
(or (not x1017) (not x1014) (not x1015))
(or (not x508) x126 x141)
(or x508 (not x126) x141)
(or x508 x126 (not x141))
(or (not x508) (not x126) (not x141))
(or (not x283) x23)
(or (not x283) (not x23) x24)
(or x283 (not x23) (not x24))
(or (not x1360) x39 x41)
(or x1360 (not x39) x41)
(or x1360 x39 (not x41))
(or (not x1360) (not x39) (not x41))
(or (not x239) x45)
(or (not x239) (not x45) x46)
(or x239 (not x45) (not x46))
(or (not x305) x12)
(or (not x305) (not x12) x13)
(or x305 (not x12) (not x13))
(or (not x1044) x62 x71)
(or x1044 (not x62) x71)
(or x1044 x62 (not x71))
(or (not x1044) (not x62) (not x71))
(or (not x404) x77)
(or (not x404) (not x77) x78)
(or x404 (not x77) (not x78) (not x79))
(or (not x404) (not x77) (not x78) x79)
(or (not x859) x130 x183)
(or x859 (not x130) x183)
(or x859 x130 (not x183))
(or (not x859) (not x130) (not x183))
(or (not x956) x119 x182)
(or x956 (not x119) x182)
(or x956 x119 (not x182))
(or (not x956) (not x119) (not x182))
(or (not x414) x51)
(or (not x414) (not x51) x77)
(or x414 (not x51) (not x77))
(or (not x1116) x1108 x1109)
(or x1116 (not x1108) x1109)
(or x1116 x1108 (not x1109))
(or (not x1116) (not x1108) (not x1109))
(or (not x1172) x208 x231)
(or x1172 (not x208) x231)
(or x1172 x208 (not x231))
(or (not x1172) (not x208) (not x231))
(or (not x960) x956 x957)
(or x960 (not x956) x957)
(or x960 x956 (not x957))
(or (not x960) (not x956) (not x957))
(or (not x203) x66)
(or (not x203) (not x66) x67)
(or x203 (not x66) (not x67))
(or (not x261) x34)
(or (not x261) (not x34) x35)
(or x261 (not x34) (not x35))
(or (not x1399) x178 x201)
(or x1399 (not x178) x201)
(or x1399 x178 (not x201))
(or (not x1399) (not x178) (not x201))
(or (not x241) x44)
(or (not x241) (not x44) x45)
(or x241 (not x44) (not x45))
(or (not x1364) x55 x66)
(or x1364 (not x55) x66)
(or x1364 x55 (not x66))
(or (not x1364) (not x55) (not x66))
(or (not x1272) x1270 x1271)
(or x1272 (not x1270) x1271)
(or x1272 x1270 (not x1271))
(or (not x1272) (not x1270) (not x1271))
(or (not x228) x132)
(or (not x228) (not x132) x133)
(or x228 (not x132) (not x133))
(or (not x1109) x399 x1101)
(or x1109 (not x399) x1101)
(or x1109 x399 (not x1101))
(or (not x1109) (not x399) (not x1101))
(or (not x638) x128 x140)
(or x638 (not x128) x140)
(or x638 x128 (not x140))
(or (not x638) (not x128) (not x140))
(or (not x488) x63)
(or (not x488) (not x63) x64)
(or x488 (not x63) (not x64) (not x65))
(or (not x488) (not x63) (not x64) x65)
(or (not x314) x90)
(or (not x314) (not x90) x91)
(or x314 (not x90) (not x91) (not x92))
(or (not x314) (not x90) (not x91) x92)
(or (not x451) x45)
(or (not x451) (not x45) x69)
(or x451 (not x45) (not x69) (not x70))
(or (not x451) (not x45) (not x69) x70)
(or (not x1102) x109 x190)
(or x1102 (not x109) x190)
(or x1102 x109 (not x190))
(or (not x1102) (not x109) (not x190))
(or (not x1075) x1073 x1074)
(or x1075 (not x1073) x1074)
(or x1075 x1073 (not x1074))
(or (not x1075) (not x1073) (not x1074))
(or (not x378) x81)
(or (not x378) (not x81) x82)
(or x378 (not x81) (not x82) (not x83))
(or (not x378) (not x81) (not x82) x83)
(or (not x563) x2 x29)
(or x563 (not x2) x29)
(or x563 x2 (not x29))
(or (not x563) (not x2) (not x29))
(or (not x587) x17 x86)
(or x587 (not x17) x86)
(or x587 x17 (not x86))
(or (not x587) (not x17) (not x86))
(or (not x300) x96)
(or (not x300) (not x96) x97)
(or x300 (not x96) (not x97))
(or (not x993) x287 x345)
(or x993 (not x287) x345)
(or x993 x287 (not x345))
(or (not x993) (not x287) (not x345))
(or (not x1162) x1157 x1158)
(or x1162 (not x1157) x1158)
(or x1162 x1157 (not x1158))
(or (not x1162) (not x1157) (not x1158))
(or (not x523) x22 x49)
(or x523 (not x22) x49)
(or x523 x22 (not x49))
(or (not x523) (not x22) (not x49))
(or (not x668) x136 x201)
(or x668 (not x136) x201)
(or x668 x136 (not x201))
(or (not x668) (not x136) (not x201))
(or (not x1209) x435 x1205)
(or x1209 (not x435) x1205)
(or x1209 x435 (not x1205))
(or (not x1209) (not x435) (not x1205))
(or (not x178) x91)
(or (not x178) (not x91) x92)
(or x178 (not x91) (not x92))
(or (not x315) x90)
(or (not x315) (not x90) x91)
(or x315 (not x90) (not x91) (not x93))
(or (not x315) (not x90) (not x91) x93)
(or (not x778) x523 x775)
(or x778 (not x523) x775)
(or x778 x523 (not x775))
(or (not x778) (not x523) (not x775))
(or (not x1221) x1211 x1212)
(or x1221 (not x1211) x1212)
(or x1221 x1211 (not x1212))
(or (not x1221) (not x1211) (not x1212))
(or (not x788) x783 x784)
(or x788 (not x783) x784)
(or x788 x783 (not x784))
(or (not x788) (not x783) (not x784))
(or (not x614) x197 x613)
(or x614 (not x197) x613)
(or x614 x197 (not x613))
(or (not x614) (not x197) (not x613))
(or (not x730) x109 x121)
(or x730 (not x109) x121)
(or x730 x109 (not x121))
(or (not x730) (not x109) (not x121))
(or (not x623) x200 x622)
(or x623 (not x200) x622)
(or x623 x200 (not x622))
(or (not x623) (not x200) (not x622))
(or (not x1093) x1085 x1086)
(or x1093 (not x1085) x1086)
(or x1093 x1085 (not x1086))
(or (not x1093) (not x1085) (not x1086))
(or (not x533) x17 x44)
(or x533 (not x17) x44)
(or x533 x17 (not x44))
(or (not x533) (not x17) (not x44))
(or (not x637) x142 x193)
(or x637 (not x142) x193)
(or x637 x142 (not x193))
(or (not x637) (not x142) (not x193))
(or (not x880) x127 x186)
(or x880 (not x127) x186)
(or x880 x127 (not x186))
(or (not x880) (not x127) (not x186))
(or (not x1281) x1277 x1278)
(or x1281 (not x1277) x1278)
(or x1281 x1277 (not x1278))
(or (not x1281) (not x1277) (not x1278))
(or (not x992) x185 x197)
(or x992 (not x185) x197)
(or x992 x185 (not x197))
(or (not x992) (not x185) (not x197))
(or (not x841) x541 x838)
(or x841 (not x541) x838)
(or x841 x541 (not x838))
(or (not x841) (not x541) (not x838))
(or (not x489) x63)
(or (not x489) (not x63) x64)
(or x489 (not x63) (not x64) (not x66))
(or (not x489) (not x63) (not x64) x66)
(or (not x370) x58)
(or (not x370) (not x58) x82)
(or x370 (not x58) (not x82) (not x83))
(or (not x370) (not x58) (not x82) x83)
(or (not x452) x69)
(or (not x452) (not x69) x70)
(or x452 (not x69) (not x70) (not x71))
(or (not x452) (not x69) (not x70) x71)
(or (not x674) x494 x673)
(or x674 (not x494) x673)
(or x674 x494 (not x673))
(or (not x674) (not x494) (not x673))
(or (not x586) x102 x184)
(or x586 (not x102) x184)
(or x586 x102 (not x184))
(or (not x586) (not x102) (not x184))
(or (not x361) x58)
(or (not x361) (not x58) x86)
(or x361 (not x58) (not x86))
(or (not x1374) x95 x131)
(or x1374 (not x95) x131)
(or x1374 x95 (not x131))
(or (not x1374) (not x95) (not x131))
(or (not x238) x127)
(or (not x238) (not x127) x128)
(or x238 (not x127) (not x128))
(or (not x900) x895 x896)
(or x900 (not x895) x896)
(or x900 x895 (not x896))
(or (not x900) (not x895) (not x896))
(or (not x1020) x1012 x1013)
(or x1020 (not x1012) x1013)
(or x1020 x1012 (not x1013))
(or (not x1020) (not x1012) (not x1013))
(or (not x453) x69)
(or (not x453) (not x69) x70)
(or x453 (not x69) (not x70) (not x72))
(or (not x453) (not x69) (not x70) x72)
(or (not x1226) x208 x213)
(or x1226 (not x208) x213)
(or x1226 x208 (not x213))
(or (not x1226) (not x208) (not x213))
(or (not x1163) x1161 x1162)
(or x1163 (not x1161) x1162)
(or x1163 x1161 (not x1162))
(or (not x1163) (not x1161) (not x1162))
(or (not x498) x38 x65)
(or x498 (not x38) x65)
(or x498 x38 (not x65))
(or (not x498) (not x38) (not x65))
(or (not x684) x496 x683)
(or x684 (not x496) x683)
(or x684 x496 (not x683))
(or (not x684) (not x496) (not x683))
(or (not x889) x96 x99)
(or x889 (not x96) x99)
(or x889 x96 (not x99))
(or (not x889) (not x96) (not x99))
(or (not x1257) x446 x447)
(or x1257 (not x446) x447)
(or x1257 x446 (not x447))
(or (not x1257) (not x446) (not x447))
(or (not x602) x94 x192)
(or x602 (not x94) x192)
(or x602 x94 (not x192))
(or (not x602) (not x94) (not x192))
(or (not x1190) x425 x426)
(or x1190 (not x425) x426)
(or x1190 x425 (not x426))
(or (not x1190) (not x425) (not x426))
(or (not x842) x230 x253)
(or x842 (not x230) x253)
(or x842 x230 (not x253))
(or (not x842) (not x230) (not x253))
(or (not x910) x96 x123)
(or x910 (not x96) x123)
(or x910 x96 (not x123))
(or (not x910) (not x96) (not x123))
(or (not x944) x318 x319)
(or x944 (not x318) x319)
(or x944 x318 (not x319))
(or (not x944) (not x318) (not x319))
(or (not x1041) x368 x369)
(or x1041 (not x368) x369)
(or x1041 x368 (not x369))
(or (not x1041) (not x368) (not x369))
(or (not x1010) x1006 x1007)
(or x1010 (not x1006) x1007)
(or x1010 x1006 (not x1007))
(or (not x1010) (not x1006) (not x1007))
(or (not x1346) x1344 x1345)
(or x1346 (not x1344) x1345)
(or x1346 x1344 (not x1345))
(or (not x1346) (not x1344) (not x1345))
(or (not x824) x135 x178)
(or x824 (not x135) x178)
(or x824 x135 (not x178))
(or (not x824) (not x135) (not x178))
(or (not x756) x754 x755)
(or x756 (not x754) x755)
(or x756 x754 (not x755))
(or (not x756) (not x754) (not x755))
(or (not x622) x2 x71)
(or x622 (not x2) x71)
(or x622 x2 (not x71))
(or (not x622) (not x2) (not x71))
(or (not x675) x120 x132)
(or x675 (not x120) x132)
(or x675 x120 (not x132))
(or (not x675) (not x120) (not x132))
(or (not x628) x135 x187)
(or x628 (not x135) x187)
(or x628 x135 (not x187))
(or (not x628) (not x135) (not x187))
(or (not x1397) x43 x52)
(or x1397 (not x43) x52)
(or x1397 x43 (not x52))
(or (not x1397) (not x43) (not x52))
(or (not x1180) x196 x205)
(or x1180 (not x196) x205)
(or x1180 x196 (not x205))
(or (not x1180) (not x196) (not x205))
(or (not x1326) x1324 x1325)
(or x1326 (not x1324) x1325)
(or x1326 x1324 (not x1325))
(or (not x1326) (not x1324) (not x1325))
(or (not x1255) x1252 x1232)
(or x1255 (not x1252) x1232)
(or x1255 x1252 (not x1232))
(or (not x1255) (not x1252) (not x1232))
(or (not x1115) x1112 x1113)
(or x1115 (not x1112) x1113)
(or x1115 x1112 (not x1113))
(or (not x1115) (not x1112) (not x1113))
(or (not x474) x41)
(or (not x474) (not x41) x67)
(or x474 (not x41) (not x67))
(or (not x458) x68)
(or (not x458) (not x68) x69)
(or x458 (not x68) (not x69) (not x70))
(or (not x458) (not x68) (not x69) x70)
(or (not x1259) x1257 x1258)
(or x1259 (not x1257) x1258)
(or x1259 x1257 (not x1258))
(or (not x1259) (not x1257) (not x1258))
(or (not x540) x110 x125)
(or x540 (not x110) x125)
(or x540 x110 (not x125))
(or (not x540) (not x110) (not x125))
(or (not x180) x89)
(or (not x180) (not x89) x90)
(or x180 (not x89) (not x90))
(or (not x1320) x58 x68)
(or x1320 (not x58) x68)
(or x1320 x58 (not x68))
(or (not x1320) (not x58) (not x68))
(or (not x1154) x194 x195)
(or x1154 (not x194) x195)
(or x1154 x194 (not x195))
(or (not x1154) (not x194) (not x195))
(or (not x603) x9 x78)
(or x603 (not x9) x78)
(or x603 x9 (not x78))
(or (not x603) (not x9) (not x78))
(or (not x996) x116 x184)
(or x996 (not x116) x184)
(or x996 x116 (not x184))
(or (not x996) (not x116) (not x184))
(or (not x538) x111 x126)
(or x538 (not x111) x126)
(or x538 x111 (not x126))
(or (not x538) (not x111) (not x126))
(or (not x1283) x1281 x1282)
(or x1283 (not x1281) x1282)
(or x1283 x1281 (not x1282))
(or (not x1283) (not x1281) (not x1282))
(or (not x592) x99 x187)
(or x592 (not x99) x187)
(or x592 x99 (not x187))
(or (not x592) (not x99) (not x187))
(or (not x1120) x202 x205)
(or x1120 (not x202) x205)
(or x1120 x202 (not x205))
(or (not x1120) (not x202) (not x205))
(or (not x1139) x409 x410)
(or x1139 (not x409) x410)
(or x1139 x409 (not x410))
(or (not x1139) (not x409) (not x410))
(or (not x497) x39 x66)
(or x497 (not x39) x66)
(or x497 x39 (not x66))
(or (not x497) (not x39) (not x66))
(or (not x485) x38)
(or (not x485) (not x38) x66)
(or x485 (not x38) (not x66))
(or (not x1095) x191 x203)
(or x1095 (not x191) x203)
(or x1095 x191 (not x203))
(or (not x1095) (not x191) (not x203))
(or (not x476) x65)
(or (not x476) (not x65) x66)
(or x476 (not x65) (not x66) (not x67))
(or (not x476) (not x65) (not x66) x67)
(or (not x194) x75)
(or (not x194) (not x75) x76)
(or x194 (not x75) (not x76))
(or (not x1152) x13 x37)
(or x1152 (not x13) x37)
(or x1152 x13 (not x37))
(or (not x1152) (not x13) (not x37))
(or (not x1142) x227 x282)
(or x1142 (not x227) x282)
(or x1142 x227 (not x282))
(or (not x1142) (not x227) (not x282))
(or (not x525) x21 x48)
(or x525 (not x21) x48)
(or x525 x21 (not x48))
(or (not x525) (not x21) (not x48))
(or (not x664) x492 x663)
(or x664 (not x492) x663)
(or x664 x492 (not x663))
(or (not x664) (not x492) (not x663))
(or (not x1158) x1155 x1156)
(or x1158 (not x1155) x1156)
(or x1158 x1155 (not x1156))
(or (not x1158) (not x1155) (not x1156))
(or (not x208) x61)
(or (not x208) (not x61) x62)
(or x208 (not x61) (not x62))
(or (not x340) x61)
(or (not x340) (not x61) x89)
(or x340 (not x61) (not x89))
(or (not x270) x111)
(or (not x270) (not x111) x112)
(or x270 (not x111) (not x112))
(or (not x940) x279 x317)
(or x940 (not x279) x317)
(or x940 x279 (not x317))
(or (not x940) (not x279) (not x317))
(or (not x1407) x484 x485)
(or x1407 (not x484) x485)
(or x1407 x484 (not x485))
(or (not x1407) (not x484) (not x485))
(or (not x1198) x140 x195)
(or x1198 (not x140) x195)
(or x1198 x140 (not x195))
(or (not x1198) (not x140) (not x195))
(or (not x621) x138 x184)
(or x621 (not x138) x184)
(or x621 x138 (not x184))
(or (not x621) (not x138) (not x184))
(or (not x1097) x1095 x1096)
(or x1097 (not x1095) x1096)
(or x1097 x1095 (not x1096))
(or (not x1097) (not x1095) (not x1096))
(or (not x784) x99 x111)
(or x784 (not x99) x111)
(or x784 x99 (not x111))
(or (not x784) (not x99) (not x111))
(or (not x1129) x1121 x1122)
(or x1129 (not x1121) x1122)
(or x1129 x1121 (not x1122))
(or (not x1129) (not x1121) (not x1122))
(or (not x524) x118 x133)
(or x524 (not x118) x133)
(or x524 x118 (not x133))
(or (not x524) (not x118) (not x133))
(or (not x267) x31)
(or (not x267) (not x31) x32)
(or x267 (not x31) (not x32))
(or (not x236) x128)
(or (not x236) (not x128) x129)
(or x236 (not x128) (not x129))
(or (not x700) x115 x127)
(or x700 (not x115) x127)
(or x700 x115 (not x127))
(or (not x700) (not x115) (not x127))
(or (not x493) x43 x70)
(or x493 (not x43) x70)
(or x493 x43 (not x70))
(or (not x493) (not x43) (not x70))
(or (not x461) x42)
(or (not x461) (not x42) x70)
(or x461 (not x42) (not x70))
(or (not x777) x100 x112)
(or x777 (not x100) x112)
(or x777 x100 (not x112))
(or (not x777) (not x100) (not x112))
(or (not x1330) x67 x68)
(or x1330 (not x67) x68)
(or x1330 x67 (not x68))
(or (not x1330) (not x67) (not x68))
(or (not x518) x121 x136)
(or x518 (not x121) x136)
(or x518 x121 (not x136))
(or (not x518) (not x121) (not x136))
(or (not x691) x689 x690)
(or x691 (not x689) x690)
(or x691 x689 (not x690))
(or (not x691) (not x689) (not x690))
(or (not x827) x537 x824)
(or x827 (not x537) x824)
(or x827 x537 (not x824))
(or (not x827) (not x537) (not x824))
(or (not x1380) x1378 x1379)
(or x1380 (not x1378) x1379)
(or x1380 x1378 (not x1379))
(or (not x1380) (not x1378) (not x1379))
(or (not x302) x95)
(or (not x302) (not x95) x96)
(or x302 (not x95) (not x96))
(or (not x345) x6)
(or (not x345) (not x6) x7)
(or x345 (not x6) (not x7))
(or (not x1159) x55 x64)
(or x1159 (not x55) x64)
(or x1159 x55 (not x64))
(or (not x1159) (not x55) (not x64))
(or (not x924) x178 x180)
(or x924 (not x178) x180)
(or x924 x178 (not x180))
(or (not x924) (not x178) (not x180))
(or (not x1018) x354 x355)
(or x1018 (not x354) x355)
(or x1018 x354 (not x355))
(or (not x1018) (not x354) (not x355))
(or (not x589) x16 x85)
(or x589 (not x16) x85)
(or x589 x16 (not x85))
(or (not x589) (not x16) (not x85))
(or (not x247) x41)
(or (not x247) (not x41) x42)
(or x247 (not x41) (not x42))
(or (not x1317) x461 x462)
(or x1317 (not x461) x462)
(or x1317 x461 (not x462))
(or (not x1317) (not x461) (not x462))
(or (not x559) x4 x31)
(or x559 (not x4) x31)
(or x559 x4 (not x31))
(or (not x559) (not x4) (not x31))
(or (not x1023) x114 x185)
(or x1023 (not x114) x185)
(or x1023 x114 (not x185))
(or (not x1023) (not x114) (not x185))
(or (not x240) x126)
(or (not x240) (not x126) x127)
(or x240 (not x126) (not x127))
(or (not x1083) x1081 x1082)
(or x1083 (not x1081) x1082)
(or x1083 x1081 (not x1082))
(or (not x1083) (not x1081) (not x1082))
(or (not x312) x66)
(or (not x312) (not x66) x92)
(or x312 (not x66) (not x92))
(or (not x393) x79)
(or (not x393) (not x79) x80)
(or x393 (not x79) (not x80) (not x82))
(or (not x393) (not x79) (not x80) x82)
(or (not x484) x38)
(or (not x484) (not x38) x64)
(or x484 (not x38) (not x64) (not x65))
(or (not x484) (not x38) (not x64) x65)
(or (not x835) x228 x251)
(or x835 (not x228) x251)
(or x835 x228 (not x251))
(or (not x835) (not x228) (not x251))
(or (not x1324) x1320 x1321)
(or x1324 (not x1320) x1321)
(or x1324 x1320 (not x1321))
(or (not x1324) (not x1320) (not x1321))
(or (not x1302) x1300 x1301)
(or x1302 (not x1300) x1301)
(or x1302 x1300 (not x1301))
(or (not x1302) (not x1300) (not x1301))
(or (not x1200) x1197 x1198)
(or x1200 (not x1197) x1198)
(or x1200 x1197 (not x1198))
(or (not x1200) (not x1197) (not x1198))
(or (not x1264) x1259 x1260)
(or x1264 (not x1259) x1260)
(or x1264 x1259 (not x1260))
(or (not x1264) (not x1259) (not x1260))
(or (not x752) x255 x256)
(or x752 (not x255) x256)
(or x752 x255 (not x256))
(or (not x752) (not x255) (not x256))
(or (not x322) x89)
(or (not x322) (not x89) x90)
(or x322 (not x89) (not x90) (not x91))
(or (not x322) (not x89) (not x90) x91)
(or (not x416) x75)
(or (not x416) (not x75) x76)
(or x416 (not x75) (not x76) (not x77))
(or (not x416) (not x75) (not x76) x77)
(or (not x855) x545 x852)
(or x855 (not x545) x852)
(or x855 x545 (not x852))
(or (not x855) (not x545) (not x852))
(or (not x258) x117)
(or (not x258) (not x117) x118)
(or x258 (not x117) (not x118))
(or (not x974) x336 x337)
(or x974 (not x336) x337)
(or x974 x336 (not x337))
(or (not x974) (not x336) (not x337))
(or (not x1229) x1224 x1225)
(or x1229 (not x1224) x1225)
(or x1229 x1224 (not x1225))
(or (not x1229) (not x1224) (not x1225))
(or (not x938) x931 x932)
(or x938 (not x931) x932)
(or x938 x931 (not x932))
(or (not x938) (not x931) (not x932))
(or (not x813) x533 x810)
(or x813 (not x533) x810)
(or x813 x533 (not x810))
(or (not x813) (not x533) (not x810))
(or (not x253) x38)
(or (not x253) (not x38) x39)
(or x253 (not x38) (not x39))
(or (not x765) x102 x114)
(or x765 (not x102) x114)
(or x765 x102 (not x114))
(or (not x765) (not x102) (not x114))
(or (not x599) x11 x80)
(or x599 (not x11) x80)
(or x599 x11 (not x80))
(or (not x599) (not x11) (not x80))
(or (not x895) x299 x300)
(or x895 (not x299) x300)
(or x895 x299 (not x300))
(or (not x895) (not x299) (not x300))
(or (not x1288) x201 x202)
(or x1288 (not x201) x202)
(or x1288 x201 (not x202))
(or (not x1288) (not x201) (not x202))
(or (not x381) x55)
(or (not x381) (not x55) x81)
(or x381 (not x55) (not x81) (not x82))
(or (not x381) (not x55) (not x81) x82)
(or (not x1279) x1275 x1276)
(or x1279 (not x1275) x1276)
(or x1279 x1275 (not x1276))
(or (not x1279) (not x1275) (not x1276))
(or (not x502) x34 x61)
(or x502 (not x34) x61)
(or x502 x34 (not x61))
(or (not x502) (not x34) (not x61))
(or (not x618) x139 x183)
(or x618 (not x139) x183)
(or x618 x139 (not x183))
(or (not x618) (not x139) (not x183))
(or (not x874) x293 x294)
(or x874 (not x293) x294)
(or x874 x293 (not x294))
(or (not x874) (not x293) (not x294))
(or (not x888) x297 x298)
(or x888 (not x297) x298)
(or x888 x297 (not x298))
(or (not x888) (not x297) (not x298))
(or (not x1420) x1417 x1418)
(or x1420 (not x1417) x1418)
(or x1420 x1417 (not x1418))
(or (not x1420) (not x1417) (not x1418))
(or (not x396) x54)
(or (not x396) (not x54) x80)
(or x396 (not x54) (not x80))
(or (not x806) x531 x803)
(or x806 (not x531) x803)
(or x806 x531 (not x803))
(or (not x806) (not x531) (not x803))
(or (not x832) x281 x282)
(or x832 (not x281) x282)
(or x832 x281 (not x282))
(or (not x832) (not x281) (not x282))
(or (not x867) x291 x292)
(or x867 (not x291) x292)
(or x867 x291 (not x292))
(or (not x867) (not x291) (not x292))
(or (not x1064) x1056 x1057)
(or x1064 (not x1056) x1057)
(or x1064 x1056 (not x1057))
(or (not x1064) (not x1056) (not x1057))
(or (not x950) x948 x949)
(or x950 (not x948) x949)
(or x950 x948 (not x949))
(or (not x950) (not x948) (not x949))
(or (not x442) x45)
(or (not x442) (not x45) x71)
(or x442 (not x45) (not x71) (not x72))
(or (not x442) (not x45) (not x71) x72)
(or (not x1228) x439 x440)
(or x1228 (not x439) x440)
(or x1228 x439 (not x440))
(or (not x1228) (not x439) (not x440))
(or (not x285) x22)
(or (not x285) (not x22) x23)
(or x285 (not x22) (not x23))
(or (not x598) x96 x190)
(or x598 (not x96) x190)
(or x598 x96 (not x190))
(or (not x598) (not x96) (not x190))
(or (not x990) x985 x986)
(or x990 (not x985) x986)
(or x990 x985 (not x986))
(or (not x990) (not x985) (not x986))
(or (not x1245) x50 x59)
(or x1245 (not x50) x59)
(or x1245 x50 (not x59))
(or (not x1245) (not x50) (not x59))
(or (not x246) x123)
(or (not x246) (not x123) x124)
(or x246 (not x123) (not x124))
(or (not x402) x53)
(or (not x402) (not x53) x79)
(or x402 (not x53) (not x79))
(or (not x313) x66)
(or (not x313) (not x66) x90)
(or x313 (not x66) (not x90) (not x91))
(or (not x313) (not x66) (not x90) x91)
(or (not x205) x64)
(or (not x205) (not x64) x65)
(or x205 (not x64) (not x65))
(or (not x369) x58)
(or (not x369) (not x58) x84)
(or x369 (not x58) (not x84))
(or (not x1368) x1364 x1365)
(or x1368 (not x1364) x1365)
(or x1368 x1364 (not x1365))
(or (not x1368) (not x1364) (not x1365))
(or (not x1358) x1353 x1354)
(or x1358 (not x1353) x1354)
(or x1358 x1353 (not x1354))
(or (not x1358) (not x1353) (not x1354))
(or (not x546) x107 x122)
(or x546 (not x107) x122)
(or x546 x107 (not x122))
(or (not x546) (not x107) (not x122))
(or (not x750) x105 x117)
(or x750 (not x105) x117)
(or x750 x105 (not x117))
(or (not x750) (not x105) (not x117))
(or (not x501) x35 x62)
(or x501 (not x35) x62)
(or x501 x35 (not x62))
(or (not x501) (not x35) (not x62))
(or (not x917) x563 x915)
(or x917 (not x563) x915)
(or x917 x563 (not x915))
(or (not x917) (not x563) (not x915))
(or (not x294) x99)
(or (not x294) (not x99) x100)
(or x294 (not x99) (not x100))
(or (not x1383) x308 x387)
(or x1383 (not x308) x387)
(or x1383 x308 (not x387))
(or (not x1383) (not x308) (not x387))
(or (not x1124) x57 x66)
(or x1124 (not x57) x66)
(or x1124 x57 (not x66))
(or (not x1124) (not x57) (not x66))
(or (not x967) x571 x964)
(or x967 (not x571) x964)
(or x967 x571 (not x964))
(or (not x967) (not x571) (not x964))
(or (not x1100) x1093 x1094)
(or x1100 (not x1093) x1094)
(or x1100 x1093 (not x1094))
(or (not x1100) (not x1093) (not x1094))
(or (not x934) x927 x928)
(or x934 (not x927) x928)
(or x934 x927 (not x928))
(or (not x934) (not x927) (not x928))
(or (not x1268) x211 x217)
(or x1268 (not x211) x217)
(or x1268 x211 (not x217))
(or (not x1268) (not x211) (not x217))
(or (not x928) x925 x926)
(or x928 (not x925) x926)
(or x928 x925 (not x926))
(or (not x928) (not x925) (not x926))
(or (not x395) x53)
(or (not x395) (not x53) x81)
(or x395 (not x53) (not x81))
(or (not x483) x64)
(or (not x483) (not x64) x65)
(or x483 (not x64) (not x65) (not x67))
(or (not x483) (not x64) (not x65) x67)
(or (not x655) x124 x136)
(or x655 (not x124) x136)
(or x655 x124 (not x136))
(or (not x655) (not x124) (not x136))
(or (not x961) x330 x569)
(or x961 (not x330) x569)
(or x961 x330 (not x569))
(or (not x961) (not x330) (not x569))
(or (not x735) x108 x120)
(or x735 (not x108) x120)
(or x735 x108 (not x120))
(or (not x735) (not x108) (not x120))
(or (not x905) x248 x271)
(or x905 (not x248) x271)
(or x905 x248 (not x271))
(or (not x905) (not x248) (not x271))
(or (not x196) x73)
(or (not x196) (not x73) x74)
(or x196 (not x73) (not x74))
(or (not x1205) x10 x34)
(or x1205 (not x10) x34)
(or x1205 x10 (not x34))
(or (not x1205) (not x10) (not x34))
(or (not x853) x287 x288)
(or x853 (not x287) x288)
(or x853 x287 (not x288))
(or (not x853) (not x287) (not x288))
(or (not x507) x30 x57)
(or x507 (not x30) x57)
(or x507 x30 (not x57))
(or (not x507) (not x30) (not x57))
(or (not x231) x49)
(or (not x231) (not x49) x50)
(or x231 (not x49) (not x50))
(or (not x591) x15 x84)
(or x591 (not x15) x84)
(or x591 x15 (not x84))
(or (not x591) (not x15) (not x84))
(or (not x1046) x1039 x1040)
(or x1046 (not x1039) x1040)
(or x1046 x1039 (not x1040))
(or (not x1046) (not x1039) (not x1040))
(or (not x686) x684 x685)
(or x686 (not x684) x685)
(or x686 x684 (not x685))
(or (not x686) (not x684) (not x685))
(or (not x991) x23 x65)
(or x991 (not x23) x65)
(or x991 x23 (not x65))
(or (not x991) (not x23) (not x65))
(or (not x307) x91)
(or (not x307) (not x91) x92)
(or x307 (not x91) (not x92) (not x94))
(or (not x307) (not x91) (not x92) x94)
(or (not x627) x136 x186)
(or x627 (not x136) x186)
(or x627 x136 (not x186))
(or (not x627) (not x136) (not x186))
(or (not x422) x74)
(or (not x422) (not x74) x75)
(or x422 (not x74) (not x75) (not x76))
(or (not x422) (not x74) (not x75) x76)
(or (not x1235) x1232 x1233)
(or x1235 (not x1232) x1233)
(or x1235 x1232 (not x1233))
(or (not x1235) (not x1232) (not x1233))
(or (not x1191) x429 x1186)
(or x1191 (not x429) x1186)
(or x1191 x429 (not x1186))
(or (not x1191) (not x429) (not x1186))
(or (not x417) x75)
(or (not x417) (not x75) x76)
(or x417 (not x75) (not x76) (not x78))
(or (not x417) (not x75) (not x76) x78)
(or (not x1123) x1119 x1120)
(or x1123 (not x1119) x1120)
(or x1123 x1119 (not x1120))
(or (not x1123) (not x1119) (not x1120))
(or (not x933) x192 x204)
(or x933 (not x192) x204)
(or x933 x192 (not x204))
(or (not x933) (not x192) (not x204))
(or (not x292) x100)
(or (not x292) (not x100) x101)
(or x292 (not x100) (not x101))
(or (not x1022) x21 x45)
(or x1022 (not x21) x45)
(or x1022 x21 (not x45))
(or (not x1022) (not x21) (not x45))
(or (not x392) x79)
(or (not x392) (not x79) x80)
(or x392 (not x79) (not x80) (not x81))
(or (not x392) (not x79) (not x80) x81)
(or (not x1308) x5 x29)
(or x1308 (not x5) x29)
(or x1308 x5 (not x29))
(or (not x1308) (not x5) (not x29))
(or (not x1171) x105 x141)
(or x1171 (not x105) x141)
(or x1171 x105 (not x141))
(or (not x1171) (not x105) (not x141))
(or (not x1277) x60 x70)
(or x1277 (not x60) x70)
(or x1277 x60 (not x70))
(or (not x1277) (not x60) (not x70))
(or (not x1251) x1248 x1249)
(or x1251 (not x1248) x1249)
(or x1251 x1248 (not x1249))
(or (not x1251) (not x1248) (not x1249))
(or (not x251) x39)
(or (not x251) (not x39) x40)
(or x251 (not x39) (not x40))
(or (not x209) x60)
(or (not x209) (not x60) x61)
(or x209 (not x60) (not x61))
(or (not x1285) x6 x30)
(or x1285 (not x6) x30)
(or x1285 x6 (not x30))
(or (not x1285) (not x6) (not x30))
(or (not x212) x140)
(or (not x212) (not x140) x141)
(or x212 (not x140) (not x141))
(or (not x672) x223 x224)
(or x672 (not x223) x224)
(or x672 x223 (not x224))
(or (not x672) (not x223) (not x224))
(or (not x325) x63)
(or (not x325) (not x63) x89)
(or x325 (not x63) (not x89) (not x90))
(or (not x325) (not x63) (not x89) x90)
(or (not x372) x82)
(or (not x372) (not x82) x83)
(or x372 (not x82) (not x83) (not x85))
(or (not x372) (not x82) (not x83) x85)
(or (not x1266) x49 x58)
(or x1266 (not x49) x58)
(or x1266 x49 (not x58))
(or (not x1266) (not x49) (not x58))
(or (not x1353) x45 x54)
(or x1353 (not x45) x54)
(or x1353 x45 (not x54))
(or (not x1353) (not x45) (not x54))
(or (not x901) x124 x189)
(or x901 (not x124) x189)
(or x901 x124 (not x189))
(or (not x901) (not x124) (not x189))
(or (not x1327) x1322 x1323)
(or x1327 (not x1322) x1323)
(or x1327 x1322 (not x1323))
(or (not x1327) (not x1322) (not x1323))
(or (not x847) x102 x105)
(or x847 (not x102) x105)
(or x847 x102 (not x105))
(or (not x847) (not x102) (not x105))
(or (not x362) x59)
(or (not x362) (not x59) x85)
(or x362 (not x59) (not x85))
(or (not x844) x839 x840)
(or x844 (not x839) x840)
(or x844 x839 (not x840))
(or (not x844) (not x839) (not x840))
(or (not x403) x53)
(or (not x403) (not x53) x77)
(or x403 (not x53) (not x77) (not x78))
(or (not x403) (not x53) (not x77) x78)
(or (not x1015) x185 x186)
(or x1015 (not x185) x186)
(or x1015 x185 (not x186))
(or (not x1015) (not x185) (not x186))
(or (not x428) x73)
(or (not x428) (not x73) x74)
(or x428 (not x73) (not x74) (not x75))
(or (not x428) (not x73) (not x74) x75)
(or (not x604) x178 x193)
(or x604 (not x178) x193)
(or x604 x178 (not x193))
(or (not x604) (not x178) (not x193))
(or (not x1186) x11 x35)
(or x1186 (not x11) x35)
(or x1186 x11 (not x35))
(or (not x1186) (not x11) (not x35))
(or (not x955) x952 x953)
(or x955 (not x952) x953)
(or x955 x952 (not x953))
(or (not x955) (not x952) (not x953))
(or (not x1413) x1409 x1410)
(or x1413 (not x1409) x1410)
(or x1413 x1409 (not x1410))
(or (not x1413) (not x1409) (not x1410))
(or (not x831) x134 x179)
(or x831 (not x134) x179)
(or x831 x134 (not x179))
(or (not x831) (not x134) (not x179))
(or (not x1286) x48 x57)
(or x1286 (not x48) x57)
(or x1286 x48 (not x57))
(or (not x1286) (not x48) (not x57))
(or (not x616) x4 x73)
(or x616 (not x4) x73)
(or x616 x4 (not x73))
(or (not x616) (not x4) (not x73))
(or (not x1338) x97 x133)
(or x1338 (not x97) x133)
(or x1338 x97 (not x133))
(or (not x1338) (not x97) (not x133))
(or (not x610) x6 x75)
(or x610 (not x6) x75)
(or x610 x6 (not x75))
(or (not x610) (not x6) (not x75))
(or (not x262) x115)
(or (not x262) (not x115) x116)
(or x262 (not x115) (not x116))
(or (not x834) x539 x831)
(or x834 (not x539) x831)
(or x834 x539 (not x831))
(or (not x834) (not x539) (not x831))
(or (not x754) x515 x753)
(or x754 (not x515) x753)
(or x754 x515 (not x753))
(or (not x754) (not x515) (not x753))
(or (not x363) x59)
(or (not x363) (not x59) x83)
(or x363 (not x59) (not x83) (not x84))
(or (not x363) (not x59) (not x83) x84)
(or (not x922) x920 x921)
(or x922 (not x920) x921)
(or x922 x920 (not x921))
(or (not x922) (not x920) (not x921))
(or (not x1357) x475 x476)
(or x1357 (not x475) x476)
(or x1357 x475 (not x476))
(or (not x1357) (not x475) (not x476))
(or (not x224) x134)
(or (not x224) (not x134) x135)
(or x224 (not x134) (not x135))
(or (not x1331) x202 x203)
(or x1331 (not x202) x203)
(or x1331 x202 (not x203))
(or (not x1331) (not x202) (not x203))
(or (not x727) x245 x246)
(or x727 (not x245) x246)
(or x727 x245 (not x246))
(or (not x727) (not x245) (not x246))
(or (not x624) x137 x185)
(or x624 (not x137) x185)
(or x624 x137 (not x185))
(or (not x624) (not x137) (not x185))
(or (not x1243) x1238 x1239)
(or x1243 (not x1238) x1239)
(or x1243 x1238 (not x1239))
(or (not x1243) (not x1238) (not x1239))
(or (not x594) x98 x188)
(or x594 (not x98) x188)
(or x594 x98 (not x188))
(or (not x594) (not x98) (not x188))
(or (not x534) x113 x128)
(or x534 (not x113) x128)
(or x534 x113 (not x128))
(or (not x534) (not x113) (not x128))
(or (not x223) x53)
(or (not x223) (not x53) x54)
(or x223 (not x53) (not x54))
(or (not x297) x16)
(or (not x297) (not x16) x17)
(or x297 (not x16) (not x17))
(or (not x1375) x206 x221)
(or x1375 (not x206) x221)
(or x1375 x206 (not x221))
(or (not x1375) (not x206) (not x221))
(or (not x1036) x1034 x1035)
(or x1036 (not x1034) x1035)
(or x1036 x1034 (not x1035))
(or (not x1036) (not x1034) (not x1035))
(or (not x1042) x372 x1038)
(or x1042 (not x372) x1038)
(or x1042 x372 (not x1038))
(or (not x1042) (not x372) (not x1038))
(or (not x921) x252 x275)
(or x921 (not x252) x275)
(or x921 x252 (not x275))
(or (not x921) (not x252) (not x275))
(or (not x337) x87)
(or (not x337) (not x87) x88)
(or x337 (not x87) (not x88) (not x90))
(or (not x337) (not x87) (not x88) x90)
(or (not x278) x107)
(or (not x278) (not x107) x108)
(or x278 (not x107) (not x108))
(or (not x580) x105 x181)
(or x580 (not x105) x181)
(or x580 x105 (not x181))
(or (not x580) (not x105) (not x181))
(or (not x792) x527 x789)
(or x792 (not x527) x789)
(or x792 x527 (not x789))
(or (not x792) (not x527) (not x789))
(or (not x504) x32 x59)
(or x504 (not x32) x59)
(or x504 x32 (not x59))
(or (not x504) (not x32) (not x59))
(or (not x445) x46)
(or (not x445) (not x46) x70)
(or x445 (not x46) (not x70) (not x71))
(or (not x445) (not x46) (not x70) x71)
(or (not x1101) x16 x40)
(or x1101 (not x16) x40)
(or x1101 x16 (not x40))
(or (not x1101) (not x16) (not x40))
(or (not x1122) x403 x404)
(or x1122 (not x403) x404)
(or x1122 x403 (not x404))
(or (not x1122) (not x403) (not x404))
(or (not x964) x183 x195)
(or x964 (not x183) x195)
(or x964 x183 (not x195))
(or (not x964) (not x183) (not x195))
(or (not x1056) x373 x374)
(or x1056 (not x373) x374)
(or x1056 x373 (not x374))
(or (not x1056) (not x373) (not x374))
(or (not x894) x125 x188)
(or x894 (not x125) x188)
(or x894 x125 (not x188))
(or (not x894) (not x125) (not x188))
(or (not x761) x759 x760)
(or x761 (not x759) x760)
(or x761 x759 (not x760))
(or (not x761) (not x759) (not x760))
(or (not x659) x491 x658)
(or x659 (not x491) x658)
(or x659 x491 (not x658))
(or (not x659) (not x491) (not x658))
(or (not x311) x65)
(or (not x311) (not x65) x93)
(or x311 (not x65) (not x93))
(or (not x963) x958 x959)
(or x963 (not x958) x959)
(or x963 x958 (not x959))
(or (not x963) (not x958) (not x959))
(or (not x972) x207 x260)
(or x972 (not x207) x260)
(or x972 x207 (not x260))
(or (not x972) (not x207) (not x260))
(or (not x722) x243 x244)
(or x722 (not x243) x244)
(or x722 x243 (not x244))
(or (not x722) (not x243) (not x244))
(or (not x229) x50)
(or (not x229) (not x50) x51)
(or x229 (not x50) (not x51))
(or (not x1179) x1176 x1177)
(or x1179 (not x1176) x1177)
(or x1179 x1176 (not x1177))
(or (not x1179) (not x1176) (not x1177))
(or (not x826) x105 x108)
(or x826 (not x105) x108)
(or x826 x105 (not x108))
(or (not x826) (not x105) (not x108))
(or (not x747) x253 x254)
(or x747 (not x253) x254)
(or x747 x253 (not x254))
(or (not x747) (not x253) (not x254))
(or (not x860) x289 x290)
(or x860 (not x289) x290)
(or x860 x289 (not x290))
(or (not x860) (not x289) (not x290))
(or (not x1106) x1102 x1103)
(or x1106 (not x1102) x1103)
(or x1106 x1102 (not x1103))
(or (not x1106) (not x1102) (not x1103))
(or (not x280) x106)
(or (not x280) (not x106) x107)
(or x280 (not x106) (not x107))
(or (not x1395) x1390 x1391)
(or x1395 (not x1390) x1391)
(or x1395 x1390 (not x1391))
(or (not x1395) (not x1390) (not x1391))
(or (not x365) x83)
(or (not x365) (not x83) x84)
(or x365 (not x83) (not x84) (not x86))
(or (not x365) (not x83) (not x84) x86)
(or (not x689) x497 x688)
(or x689 (not x497) x688)
(or x689 x497 (not x688))
(or (not x689) (not x497) (not x688))
(or (not x1276) x668 x1274)
(or x1276 (not x668) x1274)
(or x1276 x668 (not x1274))
(or (not x1276) (not x668) (not x1274))
(or (not x265) x32)
(or (not x265) (not x32) x33)
(or x265 (not x32) (not x33))
(or (not x1007) x198 x211)
(or x1007 (not x198) x211)
(or x1007 x198 (not x211))
(or (not x1007) (not x198) (not x211))
(or (not x272) x110)
(or (not x272) (not x110) x111)
(or x272 (not x110) (not x111))
(or (not x958) x954 x955)
(or x958 (not x954) x955)
(or x958 x954 (not x955))
(or (not x958) (not x954) (not x955))
(or (not x303) x13)
(or (not x303) (not x13) x14)
(or x303 (not x13) (not x14))
(or (not x726) x724 x725)
(or x726 (not x724) x725)
(or x726 x724 (not x725))
(or (not x726) (not x724) (not x725))
(or (not x490) x46 x73)
(or x490 (not x46) x73)
(or x490 x46 (not x73))
(or (not x490) (not x46) (not x73))
(or (not x443) x45)
(or (not x443) (not x45) x73)
(or x443 (not x45) (not x73))
(or (not x839) x283 x284)
(or x839 (not x283) x284)
(or x839 x283 (not x284))
(or (not x839) (not x283) (not x284))
(or (not x678) x134 x203)
(or x678 (not x134) x203)
(or x678 x134 (not x203))
(or (not x678) (not x134) (not x203))
(or (not x188) x81)
(or (not x188) (not x81) x82)
(or x188 (not x81) (not x82))
(or (not x663) x137 x200)
(or x663 (not x137) x200)
(or x663 x137 (not x200))
(or (not x663) (not x137) (not x200))
(or (not x1289) x243 x298)
(or x1289 (not x243) x298)
(or x1289 x243 (not x298))
(or (not x1289) (not x243) (not x298))
(or (not x1370) x1368 x1369)
(or x1370 (not x1368) x1369)
(or x1370 x1368 (not x1369))
(or (not x1370) (not x1368) (not x1369))
(or (not x1189) x233 x288)
(or x1189 (not x233) x288)
(or x1189 x233 (not x288))
(or (not x1189) (not x233) (not x288))
(or (not x1269) x352 x448)
(or x1269 (not x352) x448)
(or x1269 x352 (not x448))
(or (not x1269) (not x352) (not x448))
(or (not x206) x63)
(or (not x206) (not x63) x64)
(or x206 (not x63) (not x64))
(or (not x878) x876 x877)
(or x878 (not x876) x877)
(or x878 x876 (not x877))
(or (not x878) (not x876) (not x877))
(or (not x657) x217 x218)
(or x657 (not x217) x218)
(or x657 x217 (not x218))
(or (not x657) (not x217) (not x218))
(or (not x1082) x384 x385)
(or x1082 (not x384) x385)
(or x1082 x384 (not x385))
(or (not x1082) (not x384) (not x385))
(or (not x1040) x270 x293)
(or x1040 (not x270) x293)
(or x1040 x270 (not x293))
(or (not x1040) (not x270) (not x293))
(or (not x339) x61)
(or (not x339) (not x61) x87)
(or x339 (not x61) (not x87) (not x88))
(or (not x339) (not x61) (not x87) x88)
(or (not x242) x125)
(or (not x242) (not x125) x126)
(or x242 (not x125) (not x126))
(or (not x890) x555 x887)
(or x890 (not x555) x887)
(or x890 x555 (not x887))
(or (not x890) (not x555) (not x887))
(or (not x1233) x437 x438)
(or x1233 (not x437) x438)
(or x1233 x437 (not x438))
(or (not x1233) (not x437) (not x438))
(or (not x350) x85)
(or (not x350) (not x85) x86)
(or x350 (not x85) (not x86) (not x87))
(or (not x350) (not x85) (not x86) x87)
(or (not x758) x118 x229)
(or x758 (not x118) x229)
(or x758 x118 (not x229))
(or (not x758) (not x118) (not x229))
(or (not x816) x811 x812)
(or x816 (not x811) x812)
(or x816 x811 (not x812))
(or (not x816) (not x811) (not x812))
(or (not x1048) x200 x215)
(or x1048 (not x200) x215)
(or x1048 x200 (not x215))
(or (not x1048) (not x200) (not x215))
(or (not x526) x117 x132)
(or x526 (not x117) x132)
(or x526 x117 (not x132))
(or (not x526) (not x117) (not x132))
(or (not x639) x210 x638)
(or x639 (not x210) x638)
(or x639 x210 (not x638))
(or (not x639) (not x210) (not x638))
(or (not x1337) x40 x41)
(or x1337 (not x40) x41)
(or x1337 x40 (not x41))
(or (not x1337) (not x40) (not x41))
(or (not x702) x235 x236)
(or x702 (not x235) x236)
(or x702 x235 (not x236))
(or (not x702) (not x235) (not x236))
(or (not x440) x71)
(or (not x440) (not x71) x72)
(or x440 (not x71) (not x72) (not x73))
(or (not x440) (not x71) (not x72) x73)
(or (not x1348) x1342 x1343)
(or x1348 (not x1342) x1343)
(or x1348 x1342 (not x1343))
(or (not x1348) (not x1342) (not x1343))
(or (not x1344) x468 x469)
(or x1344 (not x468) x469)
(or x1344 x468 (not x469))
(or (not x1344) (not x468) (not x469))
(or (not x412) x50)
(or (not x412) (not x50) x76)
(or x412 (not x50) (not x76) (not x77))
(or (not x412) (not x50) (not x76) x77)
(or (not x871) x869 x870)
(or x871 (not x869) x870)
(or x871 x869 (not x870))
(or (not x871) (not x869) (not x870))
(or (not x260) x116)
(or (not x260) (not x116) x117)
(or x260 (not x116) (not x117))
(or (not x699) x499 x698)
(or x699 (not x499) x698)
(or x699 x499 (not x698))
(or (not x699) (not x499) (not x698))
(or (not x1084) x1079 x1080)
(or x1084 (not x1079) x1080)
(or x1084 x1079 (not x1080))
(or (not x1084) (not x1079) (not x1080))
(or (not x1329) x46 x55)
(or x1329 (not x46) x55)
(or x1329 x46 (not x55))
(or (not x1329) (not x46) (not x55))
(or (not x1080) x202 x219)
(or x1080 (not x202) x219)
(or x1080 x202 (not x219))
(or (not x1080) (not x202) (not x219))
(or (not x522) x119 x134)
(or x522 (not x119) x134)
(or x522 x119 (not x134))
(or (not x522) (not x119) (not x134))
(or (not x984) x979 x980)
(or x984 (not x979) x980)
(or x984 x979 (not x980))
(or (not x984) (not x979) (not x980))
(or (not x464) x67)
(or (not x464) (not x67) x68)
(or x464 (not x67) (not x68) (not x69))
(or (not x464) (not x67) (not x68) x69)
(or (not x1128) x191 x193)
(or x1128 (not x191) x193)
(or x1128 x191 (not x193))
(or (not x1128) (not x191) (not x193))
(or (not x433) x48)
(or (not x433) (not x48) x72)
(or x433 (not x48) (not x72) (not x73))
(or (not x433) (not x48) (not x72) x73)
(or (not x927) x315 x316)
(or x927 (not x315) x316)
(or x927 x315 (not x316))
(or (not x927) (not x315) (not x316))
(or (not x235) x47)
(or (not x235) (not x47) x48)
(or x235 (not x47) (not x48))
(or (not x353) x59)
(or (not x353) (not x59) x85)
(or x353 (not x59) (not x85) (not x86))
(or (not x353) (not x59) (not x85) x86)
(or (not x495) x41 x68)
(or x495 (not x41) x68)
(or x495 x41 (not x68))
(or (not x495) (not x41) (not x68))
(or (not x473) x40)
(or (not x473) (not x40) x68)
(or x473 (not x40) (not x68))
(or (not x600) x95 x191)
(or x600 (not x95) x191)
(or x600 x95 (not x191))
(or (not x600) (not x95) (not x191))
(or (not x772) x769 x770)
(or x772 (not x769) x770)
(or x772 x769 (not x770))
(or (not x772) (not x769) (not x770))
(or (not x1016) x1008 x1009)
(or x1016 (not x1008) x1009)
(or x1016 x1008 (not x1009))
(or (not x1016) (not x1008) (not x1009))
(or (not x420) x50)
(or (not x420) (not x50) x76)
(or x420 (not x50) (not x76))
(or (not x1414) x1412 x1413)
(or x1414 (not x1412) x1413)
(or x1414 x1412 (not x1413))
(or (not x1414) (not x1412) (not x1413))
(or (not x494) x42 x69)
(or x494 (not x42) x69)
(or x494 x42 (not x69))
(or (not x494) (not x42) (not x69))
(or (not x467) x41)
(or (not x467) (not x41) x69)
(or x467 (not x41) (not x69))
(or (not x230) x131)
(or (not x230) (not x131) x132)
(or x230 (not x131) (not x132))
(or (not x574) x108 x178)
(or x574 (not x108) x178)
(or x574 x108 (not x178))
(or (not x574) (not x108) (not x178))
(or (not x595) x13 x82)
(or x595 (not x13) x82)
(or x595 x13 (not x82))
(or (not x595) (not x13) (not x82))
(or (not x745) x106 x118)
(or x745 (not x106) x118)
(or x745 x106 (not x118))
(or (not x745) (not x106) (not x118))
(or (not x776) x265 x266)
(or x776 (not x265) x266)
(or x776 x265 (not x266))
(or (not x776) (not x265) (not x266))
(or (not x384) x56)
(or (not x384) (not x56) x80)
(or x384 (not x56) (not x80) (not x81))
(or (not x384) (not x56) (not x80) x81)
(or (not x1232) x198 x199)
(or x1232 (not x198) x199)
(or x1232 x198 (not x199))
(or (not x1232) (not x198) (not x199))
(or (not x915) x179 x191)
(or x915 (not x179) x191)
(or x915 x179 (not x191))
(or (not x915) (not x179) (not x191))
(or (not x1060) x272 x295)
(or x1060 (not x272) x295)
(or x1060 x272 (not x295))
(or (not x1060) (not x272) (not x295))
(or (not x977) x24 x66)
(or x977 (not x24) x66)
(or x977 x24 (not x66))
(or (not x977) (not x24) (not x66))
(or (not x635) x129 x141)
(or x635 (not x129) x141)
(or x635 x129 (not x141))
(or (not x635) (not x129) (not x141))
(or (not x1282) x1272 x1273)
(or x1282 (not x1272) x1273)
(or x1282 x1272 (not x1273))
(or (not x1282) (not x1272) (not x1273))
(or (not x306) x66)
(or (not x306) (not x66) x94)
(or x306 (not x66) (not x94))
(or (not x1258) x1253 x1254)
(or x1258 (not x1253) x1254)
(or x1258 x1253 (not x1254))
(or (not x1258) (not x1253) (not x1254))
(or (not x423) x74)
(or (not x423) (not x74) x75)
(or x423 (not x74) (not x75) (not x77))
(or (not x423) (not x74) (not x75) x77)
(or (not x868) x99 x102)
(or x868 (not x99) x102)
(or x868 x99 (not x102))
(or (not x868) (not x99) (not x102))
(or (not x783) x267 x268)
(or x783 (not x267) x268)
(or x783 x267 (not x268))
(or (not x783) (not x267) (not x268))
(or (not x338) x7)
(or (not x338) (not x7) x8)
(or x338 (not x7) (not x8))
(or (not x931) x565 x924)
(or x931 (not x565) x924)
(or x931 x565 (not x924))
(or (not x931) (not x565) (not x924))
(or (not x1253) x442 x443)
(or x1253 (not x442) x443)
(or x1253 x442 (not x443))
(or (not x1253) (not x442) (not x443))
(or (not x1146) x1138 x1139)
(or x1146 (not x1138) x1139)
(or x1146 x1138 (not x1139))
(or (not x1146) (not x1138) (not x1139))
(or (not x976) x971 x972)
(or x976 (not x971) x972)
(or x976 x971 (not x972))
(or (not x976) (not x971) (not x972))
(or (not x211) x59)
(or (not x211) (not x59) x60)
(or x211 (not x59) (not x60))
(or (not x1169) x1166 x1167)
(or x1169 (not x1166) x1167)
(or x1169 x1166 (not x1167))
(or (not x1169) (not x1166) (not x1167))
(or (not x608) x195 x607)
(or x608 (not x195) x607)
(or x608 x195 (not x607))
(or (not x608) (not x195) (not x607))
(or (not x469) x42)
(or (not x469) (not x42) x66)
(or x469 (not x42) (not x66) (not x67))
(or (not x469) (not x42) (not x66) x67)
(or (not x1231) x45 x46)
(or x1231 (not x45) x46)
(or x1231 x45 (not x46))
(or (not x1231) (not x45) (not x46))
(or (not x1052) x1047 x1048)
(or x1052 (not x1047) x1048)
(or x1052 x1047 (not x1048))
(or (not x1052) (not x1047) (not x1048))
(or (not x1234) x1226 x1227)
(or x1234 (not x1226) x1227)
(or x1234 x1226 (not x1227))
(or (not x1234) (not x1226) (not x1227))
(or (not x1183) x420 x421)
(or x1183 (not x420) x421)
(or x1183 x420 (not x421))
(or (not x1183) (not x420) (not x421))
(or (not x281) x24)
(or (not x281) (not x24) x25)
(or x281 (not x24) (not x25))
(or (not x1335) x1330 x1331)
(or x1335 (not x1330) x1331)
(or x1335 x1330 (not x1331))
(or (not x1335) (not x1330) (not x1331))
(or (not x959) x258 x281)
(or x959 (not x258) x281)
(or x959 x258 (not x281))
(or (not x959) (not x258) (not x281))
(or (not x1212) x207 x211)
(or x1212 (not x207) x211)
(or x1212 x207 (not x211))
(or (not x1212) (not x207) (not x211))
(or (not x271) x29)
(or (not x271) (not x29) x30)
(or x271 (not x29) (not x30))
(or (not x1403) x1400 x926)
(or x1403 (not x1400) x926)
(or x1403 x1400 (not x926))
(or (not x1403) (not x1400) (not x926))
(or (not x1012) x266 x289)
(or x1012 (not x266) x289)
(or x1012 x266 (not x289))
(or (not x1012) (not x266) (not x289))
(or (not x1287) x70 x99)
(or x1287 (not x70) x99)
(or x1287 x70 (not x99))
(or (not x1287) (not x70) (not x99))
(or (not x552) x104 x119)
(or x552 (not x104) x119)
(or x552 x104 (not x119))
(or (not x552) (not x104) (not x119))
(or (not x687) x229 x230)
(or x687 (not x229) x230)
(or x687 x229 (not x230))
(or (not x687) (not x229) (not x230))
(or (not x426) x49)
(or (not x426) (not x49) x75)
(or x426 (not x49) (not x75))
(or (not x1144) x1140 x1141)
(or x1144 (not x1140) x1141)
(or x1144 x1140 (not x1141))
(or (not x1144) (not x1140) (not x1141))
(or (not x288) x102)
(or (not x288) (not x102) x103)
(or x288 (not x102) (not x103))
(or (not x324) x9)
(or (not x324) (not x9) x10)
(or x324 (not x9) (not x10))
(or (not x981) x977 x978)
(or x981 (not x977) x978)
(or x981 x977 (not x978))
(or (not x981) (not x977) (not x978))
(or (not x809) x804 x805)
(or x809 (not x804) x805)
(or x809 x804 (not x805))
(or (not x809) (not x804) (not x805))
(or (not x881) x295 x296)
(or x881 (not x295) x296)
(or x881 x295 (not x296))
(or (not x881) (not x295) (not x296))
(or (not x1094) x1091 x1092)
(or x1094 (not x1091) x1092)
(or x1094 x1091 (not x1092))
(or (not x1094) (not x1091) (not x1092))
(or (not x354) x59)
(or (not x354) (not x59) x87)
(or x354 (not x59) (not x87))
(or (not x728) x124 x217)
(or x728 (not x124) x217)
(or x728 x124 (not x217))
(or (not x728) (not x124) (not x217))
(or (not x572) x94 x109)
(or x572 (not x94) x109)
(or x572 x94 (not x109))
(or (not x572) (not x94) (not x109))
(or (not x582) x104 x182)
(or x582 (not x104) x182)
(or x582 x104 (not x182))
(or (not x582) (not x104) (not x182))
(or (not x688) x132 x205)
(or x688 (not x132) x205)
(or x688 x132 (not x205))
(or (not x688) (not x132) (not x205))
(or (not x654) x490 x653)
(or x654 (not x490) x653)
(or x654 x490 (not x653))
(or (not x654) (not x490) (not x653))
(or (not x1203) x1193 x1194)
(or x1203 (not x1193) x1194)
(or x1203 x1193 (not x1194))
(or (not x1203) (not x1193) (not x1194))
(or (not x1202) x1199 x1200)
(or x1202 (not x1199) x1200)
(or x1202 x1199 (not x1200))
(or (not x1202) (not x1199) (not x1200))
(or (not x1006) x115 x184)
(or x1006 (not x115) x184)
(or x1006 x115 (not x184))
(or (not x1006) (not x115) (not x184))
(or (not x376) x57)
(or (not x376) (not x57) x83)
(or x376 (not x57) (not x83))
(or (not x1260) x215 x239)
(or x1260 (not x215) x239)
(or x1260 x215 (not x239))
(or (not x1260) (not x215) (not x239))
(or (not x1247) x200 x209)
(or x1247 (not x200) x209)
(or x1247 x200 (not x209))
(or (not x1247) (not x200) (not x209))
(or (not x519) x24 x51)
(or x519 (not x24) x51)
(or x519 x24 (not x51))
(or (not x519) (not x24) (not x51))
(or (not x709) x501 x708)
(or x709 (not x501) x708)
(or x709 x501 (not x708))
(or (not x709) (not x501) (not x708))
(or (not x1306) x1304 x1305)
(or x1306 (not x1304) x1305)
(or x1306 x1304 (not x1305))
(or (not x1306) (not x1304) (not x1305))
(or (not x975) x973 x974)
(or x975 (not x973) x974)
(or x975 x973 (not x974))
(or (not x975) (not x973) (not x974))
(or (not x554) x103 x118)
(or x554 (not x103) x118)
(or x554 x103 (not x118))
(or (not x554) (not x103) (not x118))
(or (not x746) x744 x745)
(or x746 (not x744) x745)
(or x746 x744 (not x745))
(or (not x746) (not x744) (not x745))
(or (not x1300) x457 x458)
(or x1300 (not x457) x458)
(or x1300 x457 (not x458))
(or (not x1300) (not x457) (not x458))
(or (not x259) x35)
(or (not x259) (not x35) x36)
(or x259 (not x35) (not x36))
(or (not x1004) x999 x1000)
(or x1004 (not x999) x1000)
(or x1004 x999 (not x1000))
(or (not x1004) (not x999) (not x1000))
(or (not x500) x36 x63)
(or x500 (not x36) x63)
(or x500 x36 (not x63))
(or (not x500) (not x36) (not x63))
(or (not x865) x860 x861)
(or x865 (not x860) x861)
(or x865 x860 (not x861))
(or (not x865) (not x860) (not x861))
(or (not x578) x106 x180)
(or x578 (not x106) x180)
(or x578 x106 (not x180))
(or (not x578) (not x106) (not x180))
(or (not x1192) x1189 x1190)
(or x1192 (not x1189) x1190)
(or x1192 x1189 (not x1190))
(or (not x1192) (not x1189) (not x1190))
(or (not x308) x93)
(or (not x308) (not x93) x94)
(or x308 (not x93) (not x94))
(or (not x652) x649 x650)
(or x652 (not x649) x650)
(or x652 x649 (not x650))
(or (not x652) (not x649) (not x650))
(or (not x1133) x1125 x1126)
(or x1133 (not x1125) x1126)
(or x1133 x1125 (not x1126))
(or (not x1133) (not x1125) (not x1126))
(or (not x596) x97 x189)
(or x596 (not x97) x189)
(or x596 x97 (not x189))
(or (not x596) (not x97) (not x189))
(or (not x863) x236 x259)
(or x863 (not x236) x259)
(or x863 x236 (not x259))
(or (not x863) (not x236) (not x259))
(or (not x751) x749 x750)
(or x751 (not x749) x750)
(or x751 x749 (not x750))
(or (not x751) (not x749) (not x750))
(or (not x1393) x1376 x1377)
(or x1393 (not x1376) x1377)
(or x1393 x1376 (not x1377))
(or (not x1393) (not x1376) (not x1377))
(or (not x1323) x245 x300)
(or x1323 (not x245) x300)
(or x1323 x245 (not x300))
(or (not x1323) (not x245) (not x300))
(or (not x329) x88)
(or (not x329) (not x88) x89)
(or x329 (not x88) (not x89) (not x90))
(or (not x329) (not x88) (not x89) x90)
(or (not x480) x40)
(or (not x480) (not x40) x66)
(or x480 (not x40) (not x66))
(or (not x255) x37)
(or (not x255) (not x37) x38)
(or x255 (not x37) (not x38))
(or (not x872) x867 x868)
(or x872 (not x867) x868)
(or x872 x867 (not x868))
(or (not x872) (not x867) (not x868))
(or (not x773) x233 x263)
(or x773 (not x233) x263)
(or x773 x233 (not x263))
(or (not x773) (not x233) (not x263))
(or (not x1321) x465 x1308)
(or x1321 (not x465) x1308)
(or x1321 x465 (not x1308))
(or (not x1321) (not x465) (not x1308))
(or (not x421) x50)
(or (not x421) (not x50) x74)
(or x421 (not x50) (not x74) (not x75))
(or (not x421) (not x50) (not x74) x75)
(or (not x1140) x1136 x1137)
(or x1140 (not x1136) x1137)
(or x1140 x1136 (not x1137))
(or (not x1140) (not x1136) (not x1137))
(or (not x1182) x1180 x1181)
(or x1182 (not x1180) x1181)
(or x1182 x1180 (not x1181))
(or (not x1182) (not x1180) (not x1181))
(or (not x1325) x1315 x1316)
(or x1325 (not x1315) x1316)
(or x1325 x1315 (not x1316))
(or (not x1325) (not x1315) (not x1316))
(or (not x1402) x1396 x1397)
(or x1402 (not x1396) x1397)
(or x1402 x1396 (not x1397))
(or (not x1402) (not x1396) (not x1397))
(or (not x634) x192 x207)
(or x634 (not x192) x207)
(or x634 x192 (not x207))
(or (not x634) (not x192) (not x207))
(or (not x547) x10 x37)
(or x547 (not x10) x37)
(or x547 x10 (not x37))
(or (not x547) (not x10) (not x37))
(or (not x850) x848 x849)
(or x850 (not x848) x849)
(or x850 x848 (not x849))
(or (not x850) (not x848) (not x849))
(or (not x671) x669 x670)
(or x671 (not x669) x670)
(or x671 x669 (not x670))
(or (not x671) (not x669) (not x670))
(or (not x204) x65)
(or (not x204) (not x65) x66)
(or x204 (not x65) (not x66))
(or (not x576) x107 x179)
(or x576 (not x107) x179)
(or x576 x107 (not x179))
(or (not x576) (not x107) (not x179))
(or (not x429) x73)
(or (not x429) (not x73) x74)
(or x429 (not x73) (not x74) (not x76))
(or (not x429) (not x73) (not x74) x76)
(or (not x884) x242 x265)
(or x884 (not x242) x265)
(or x884 x242 (not x265))
(or (not x884) (not x242) (not x265))
(or (not x1055) x201 x217)
(or x1055 (not x201) x217)
(or x1055 x201 (not x217))
(or (not x1055) (not x201) (not x217))
(or (not x1126) x405 x1118)
(or x1126 (not x405) x1118)
(or x1126 x405 (not x1118))
(or (not x1126) (not x405) (not x1118))
(or (not x882) x97 x100)
(or x882 (not x97) x100)
(or x882 x97 (not x100))
(or (not x882) (not x97) (not x100))
(or (not x916) x305 x306)
(or x916 (not x305) x306)
(or x916 x305 (not x306))
(or (not x916) (not x305) (not x306))
(or (not x1217) x1206 x653)
(or x1217 (not x1206) x653)
(or x1217 x1206 (not x653))
(or (not x1217) (not x1206) (not x653))
(or (not x632) x131 x191)
(or x632 (not x131) x191)
(or x632 x131 (not x191))
(or (not x632) (not x131) (not x191))
(or (not x1150) x1142 x1143)
(or x1150 (not x1142) x1143)
(or x1150 x1142 (not x1143))
(or (not x1150) (not x1142) (not x1143))
(or (not x1178) x1170 x1171)
(or x1178 (not x1170) x1171)
(or x1178 x1170 (not x1171))
(or (not x1178) (not x1170) (not x1171))
(or (not x851) x846 x847)
(or x851 (not x846) x847)
(or x851 x846 (not x847))
(or (not x851) (not x846) (not x847))
(or (not x636) x208 x635)
(or x636 (not x208) x635)
(or x636 x208 (not x635))
(or (not x636) (not x208) (not x635))
(or (not x693) x131 x206)
(or x693 (not x131) x206)
(or x693 x131 (not x206))
(or (not x693) (not x131) (not x206))
(or (not x344) x86)
(or (not x344) (not x86) x87)
(or x344 (not x86) (not x87) (not x89))
(or (not x344) (not x86) (not x87) x89)
(or (not x1389) x1382 x1383)
(or x1389 (not x1382) x1383)
(or x1389 x1382 (not x1383))
(or (not x1389) (not x1382) (not x1383))
(or (not x1297) x1292 x1293)
(or x1297 (not x1292) x1293)
(or x1297 x1292 (not x1293))
(or (not x1297) (not x1292) (not x1293))
(or (not x837) x832 x833)
(or x837 (not x832) x833)
(or x837 x832 (not x833))
(or (not x837) (not x832) (not x833))
(or (not x1352) x3 x27)
(or x1352 (not x3) x27)
(or x1352 x3 (not x27))
(or (not x1352) (not x3) (not x27))
(or (not x812) x95 x107)
(or x812 (not x95) x107)
(or x812 x95 (not x107))
(or (not x812) (not x95) (not x107))
(or (not x1273) x43 x45)
(or x1273 (not x43) x45)
(or x1273 x43 (not x45))
(or (not x1273) (not x43) (not x45))
(or (not x432) x48)
(or (not x432) (not x48) x74)
(or x432 (not x48) (not x74))
(or (not x336) x87)
(or (not x336) (not x87) x88)
(or x336 (not x87) (not x88) (not x89))
(or (not x336) (not x87) (not x88) x89)
(or (not x736) x734 x735)
(or x736 (not x734) x735)
(or x736 x734 (not x735))
(or (not x736) (not x734) (not x735))
(or (not x1032) x187 x199)
(or x1032 (not x187) x199)
(or x1032 x187 (not x199))
(or (not x1032) (not x187) (not x199))
(or (not x1043) x1041 x1042)
(or x1043 (not x1041) x1042)
(or x1043 x1041 (not x1042))
(or (not x1043) (not x1041) (not x1042))
(or (not x1381) x38 x39)
(or x1381 (not x38) x39)
(or x1381 x38 (not x39))
(or (not x1381) (not x38) (not x39))
(or (not x1089) x392 x393)
(or x1089 (not x392) x393)
(or x1089 x392 (not x393))
(or (not x1089) (not x392) (not x393))
(or (not x409) x52)
(or (not x409) (not x52) x76)
(or x409 (not x52) (not x76) (not x77))
(or (not x409) (not x52) (not x76) x77)
(or (not x359) x4)
(or (not x359) (not x4) x5)
(or x359 (not x4) (not x5))
(or (not x1050) x370 x371)
(or x1050 (not x370) x371)
(or x1050 x370 (not x371))
(or (not x1050) (not x370) (not x371))
(or (not x575) x23 x92)
(or x575 (not x23) x92)
(or x575 x23 (not x92))
(or (not x575) (not x23) (not x92))
(or (not x1271) x1266 x1267)
(or x1271 (not x1266) x1267)
(or x1271 x1266 (not x1267))
(or (not x1271) (not x1266) (not x1267))
(or (not x1392) x1386 x1387)
(or x1392 (not x1386) x1387)
(or x1392 x1386 (not x1387))
(or (not x1392) (not x1386) (not x1387))
(or (not x630) x133 x189)
(or x630 (not x133) x189)
(or x630 x133 (not x189))
(or (not x630) (not x133) (not x189))
(or (not x626) x201 x625)
(or x626 (not x201) x625)
(or x626 x201 (not x625))
(or (not x626) (not x201) (not x625))
(or (not x389) x54)
(or (not x389) (not x54) x82)
(or x389 (not x54) (not x82))
(or (not x562) x99 x114)
(or x562 (not x99) x114)
(or x562 x99 (not x114))
(or (not x562) (not x99) (not x114))
(or (not x810) x110 x137)
(or x810 (not x110) x137)
(or x810 x110 (not x137))
(or (not x810) (not x110) (not x137))
(or (not x1236) x72 x73)
(or x1236 (not x72) x73)
(or x1236 x72 (not x73))
(or (not x1236) (not x72) (not x73))
(or (not x1390) x1388 x1389)
(or x1390 (not x1388) x1389)
(or x1390 x1388 (not x1389))
(or (not x1390) (not x1388) (not x1389))
(or (not x1039) x113 x188)
(or x1039 (not x113) x188)
(or x1039 x113 (not x188))
(or (not x1039) (not x113) (not x188))
(or (not x1019) x1016 x1017)
(or x1019 (not x1016) x1017)
(or x1019 x1016 (not x1017))
(or (not x1019) (not x1016) (not x1017))
(or (not x511) x28 x55)
(or x511 (not x28) x55)
(or x511 x28 (not x55))
(or (not x511) (not x28) (not x55))
(or (not x731) x729 x730)
(or x731 (not x729) x730)
(or x731 x729 (not x730))
(or (not x731) (not x729) (not x730))
(or (not x1132) x1129 x1130)
(or x1132 (not x1129) x1130)
(or x1132 x1129 (not x1130))
(or (not x1132) (not x1129) (not x1130))
(or (not x1394) x1392 x1393)
(or x1394 (not x1392) x1393)
(or x1394 x1392 (not x1393))
(or (not x1394) (not x1392) (not x1393))
(or (not x299) x15)
(or (not x299) (not x15) x16)
(or x299 (not x15) (not x16))
(or (not x317) x10)
(or (not x317) (not x10) x11)
(or x317 (not x10) (not x11))
(or (not x1135) x14 x38)
(or x1135 (not x14) x38)
(or x1135 x14 (not x38))
(or (not x1135) (not x14) (not x38))
(or (not x775) x115 x142)
(or x775 (not x115) x142)
(or x775 x115 (not x142))
(or (not x775) (not x115) (not x142))
(or (not x1147) x1144 x1145)
(or x1147 (not x1144) x1145)
(or x1147 x1144 (not x1145))
(or (not x1147) (not x1144) (not x1145))
(or (not x1278) x453 x1265)
(or x1278 (not x453) x1265)
(or x1278 x453 (not x1265))
(or (not x1278) (not x453) (not x1265))
(or (not x466) x41)
(or (not x466) (not x41) x67)
(or x466 (not x41) (not x67) (not x68))
(or (not x466) (not x41) (not x67) x68)
(or (not x207) x62)
(or (not x207) (not x62) x63)
(or x207 (not x62) (not x63))
(or (not x544) x108 x123)
(or x544 (not x108) x123)
(or x544 x108 (not x123))
(or (not x544) (not x108) (not x123))
(or (not x1110) x1106 x1107)
(or x1110 (not x1106) x1107)
(or x1110 x1106 (not x1107))
(or (not x1110) (not x1106) (not x1107))
(or (not x1076) x60 x69)
(or x1076 (not x60) x69)
(or x1076 x60 (not x69))
(or (not x1076) (not x60) (not x69))
(or (not x833) x104 x107)
(or x833 (not x104) x107)
(or x833 x104 (not x107))
(or (not x833) (not x104) (not x107))
(or (not x558) x101 x116)
(or x558 (not x101) x116)
(or x558 x101 (not x116))
(or (not x558) (not x101) (not x116))
(or (not x482) x64)
(or (not x482) (not x64) x65)
(or x482 (not x64) (not x65) (not x66))
(or (not x482) (not x64) (not x65) x66)
(or (not x875) x98 x101)
(or x875 (not x98) x101)
(or x875 x98 (not x101))
(or (not x875) (not x98) (not x101))
(or (not x891) x244 x267)
(or x891 (not x244) x267)
(or x891 x244 (not x267))
(or (not x891) (not x244) (not x267))
(or (not x1378) x482 x483)
(or x1378 (not x482) x483)
(or x1378 x482 (not x483))
(or (not x1378) (not x482) (not x483))
(or (not x1057) x377 x378)
(or x1057 (not x377) x378)
(or x1057 x377 (not x378))
(or (not x1057) (not x377) (not x378))
(or (not x506) x127 x142)
(or x506 (not x127) x142)
(or x506 x127 (not x142))
(or (not x506) (not x127) (not x142))
(or (not x492) x44 x71)
(or x492 (not x44) x71)
(or x492 x44 (not x71))
(or (not x492) (not x44) (not x71))
(or (not x455) x43)
(or (not x455) (not x43) x71)
(or x455 (not x43) (not x71))
(or (not x346) x60)
(or (not x346) (not x60) x86)
(or x346 (not x60) (not x86) (not x87))
(or (not x346) (not x60) (not x86) x87)
(or (not x1037) x1030 x1031)
(or x1037 (not x1030) x1031)
(or x1037 x1030 (not x1031))
(or (not x1037) (not x1030) (not x1031))
(or (not x1058) x1054 x1055)
(or x1058 (not x1054) x1055)
(or x1058 x1054 (not x1055))
(or (not x1058) (not x1054) (not x1055))
(or (not x221) x54)
(or (not x221) (not x54) x55)
(or x221 (not x54) (not x55))
(or (not x1176) x54 x63)
(or x1176 (not x54) x63)
(or x1176 x54 (not x63))
(or (not x1176) (not x54) (not x63))
(or (not x360) x58)
(or (not x360) (not x58) x84)
(or x360 (not x58) (not x84) (not x85))
(or (not x360) (not x58) (not x84) x85)
(or (not x1081) x1075 x1076)
(or x1081 (not x1075) x1076)
(or x1081 x1075 (not x1076))
(or (not x1081) (not x1075) (not x1076))
(or (not x478) x39)
(or (not x478) (not x39) x65)
(or x478 (not x39) (not x65) (not x66))
(or (not x478) (not x39) (not x65) x66)
(or (not x1063) x188 x189)
(or x1063 (not x188) x189)
(or x1063 x188 (not x189))
(or (not x1063) (not x188) (not x189))
(or (not x676) x674 x675)
(or x676 (not x674) x675)
(or x676 x674 (not x675))
(or (not x676) (not x674) (not x675))
(or (not x651) x140 x197)
(or x651 (not x140) x197)
(or x651 x140 (not x197))
(or (not x651) (not x140) (not x197))
(or (not x805) x96 x108)
(or x805 (not x96) x108)
(or x805 x96 (not x108))
(or (not x805) (not x96) (not x108))
(or (not x531) x18 x45)
(or x531 (not x18) x45)
(or x531 x18 (not x45))
(or (not x531) (not x18) (not x45))
(or (not x588) x101 x185)
(or x588 (not x101) x185)
(or x588 x101 (not x185))
(or (not x588) (not x101) (not x185))
(or (not x1141) x56 x65)
(or x1141 (not x56) x65)
(or x1141 x56 (not x65))
(or (not x1141) (not x56) (not x65))
(or (not x332) x62)
(or (not x332) (not x62) x88)
(or x332 (not x62) (not x88) (not x89))
(or (not x332) (not x62) (not x88) x89)
(or (not x1373) x44 x53)
(or x1373 (not x44) x53)
(or x1373 x44 (not x53))
(or (not x1373) (not x44) (not x53))
(or (not x1059) x61 x70)
(or x1059 (not x61) x70)
(or x1059 x61 (not x70))
(or (not x1059) (not x61) (not x70))
(or (not x434) x72)
(or (not x434) (not x72) x73)
(or x434 (not x72) (not x73) (not x74))
(or (not x434) (not x72) (not x73) x74)
(or (not x291) x19)
(or (not x291) (not x19) x20)
(or x291 (not x19) (not x20))
(or (not x550) x105 x120)
(or x550 (not x105) x120)
(or x550 x105 (not x120))
(or (not x550) (not x105) (not x120))
(or (not x472) x40)
(or (not x472) (not x40) x66)
(or x472 (not x40) (not x66) (not x67))
(or (not x472) (not x40) (not x66) x67)
(or (not x1160) x204 x207)
(or x1160 (not x204) x207)
(or x1160 x204 (not x207))
(or (not x1160) (not x204) (not x207))
(or (not x1099) x1097 x1098)
(or x1099 (not x1097) x1098)
(or x1099 x1097 (not x1098))
(or (not x1099) (not x1097) (not x1098))
(or (not x1065) x1062 x1063)
(or x1065 (not x1062) x1063)
(or x1065 x1062 (not x1063))
(or (not x1065) (not x1062) (not x1063))
(or (not x768) x765 x766)
(or x768 (not x765) x766)
(or x768 x765 (not x766))
(or (not x768) (not x765) (not x766))
(or (not x926) x311 x312)
(or x926 (not x311) x312)
(or x926 x311 (not x312))
(or (not x926) (not x311) (not x312))
(or (not x995) x991 x992)
(or x995 (not x991) x992)
(or x995 x991 (not x992))
(or (not x995) (not x991) (not x992))
(or (not x394) x53)
(or (not x394) (not x53) x79)
(or x394 (not x53) (not x79) (not x80))
(or (not x394) (not x53) (not x79) x80)
(or (not x1181) x1174 x1175)
(or x1181 (not x1174) x1175)
(or x1181 x1174 (not x1175))
(or (not x1181) (not x1174) (not x1175))
(or (not x1026) x364 x365)
(or x1026 (not x364) x365)
(or x1026 x364 (not x365))
(or (not x1026) (not x364) (not x365))
(or (not x774) x771 x772)
(or x774 (not x771) x772)
(or x774 x771 (not x772))
(or (not x774) (not x771) (not x772))
(or (not x807) x220 x243)
(or x807 (not x220) x243)
(or x807 x220 (not x243))
(or (not x807) (not x220) (not x243))
(or (not x182) x87)
(or (not x182) (not x87) x88)
(or x182 (not x87) (not x88))
(or (not x649) x125 x137)
(or x649 (not x125) x137)
(or x649 x125 (not x137))
(or (not x649) (not x125) (not x137))
(or (not x887) x126 x187)
(or x887 (not x126) x187)
(or x887 x126 (not x187))
(or (not x887) (not x126) (not x187))
(or (not x828) x226 x249)
(or x828 (not x226) x249)
(or x828 x226 (not x249))
(or (not x828) (not x226) (not x249))
(or (not x896) x95 x98)
(or x896 (not x95) x98)
(or x896 x95 (not x98))
(or (not x896) (not x95) (not x98))
(or (not x1369) x1359 x1360)
(or x1369 (not x1359) x1360)
(or x1369 x1359 (not x1360))
(or (not x1369) (not x1359) (not x1360))
(or (not x248) x122)
(or (not x248) (not x122) x123)
(or x248 (not x122) (not x123))
(or (not x326) x63)
(or (not x326) (not x63) x91)
(or x326 (not x63) (not x91))
(or (not x347) x60)
(or (not x347) (not x60) x88)
(or x347 (not x60) (not x88))
(or (not x825) x279 x280)
(or x825 (not x279) x280)
(or x825 x279 (not x280))
(or (not x825) (not x279) (not x280))
(or (not x1027) x1024 x1025)
(or x1027 (not x1024) x1025)
(or x1027 x1024 (not x1025))
(or (not x1027) (not x1024) (not x1025))
(or (not x1025) x360 x361)
(or x1025 (not x360) x361)
(or x1025 x360 (not x361))
(or (not x1025) (not x360) (not x361))
(or (not x716) x714 x715)
(or x716 (not x714) x715)
(or x716 x714 (not x715))
(or (not x716) (not x714) (not x715))
(or (not x1047) x1045 x1046)
(or x1047 (not x1045) x1046)
(or x1047 x1045 (not x1046))
(or (not x1047) (not x1045) (not x1046))
(or (not x877) x240 x263)
(or x877 (not x240) x263)
(or x877 x240 (not x263))
(or (not x877) (not x240) (not x263))
(or (not x857) x855 x856)
(or x857 (not x855) x856)
(or x857 x855 (not x856))
(or (not x857) (not x855) (not x856))
(or (not x858) x853 x854)
(or x858 (not x853) x854)
(or x858 x853 (not x854))
(or (not x858) (not x853) (not x854))
(or (not x613) x5 x74)
(or x613 (not x5) x74)
(or x613 x5 (not x74))
(or (not x613) (not x5) (not x74))
(or (not x619) x3 x72)
(or x619 (not x3) x72)
(or x619 x3 (not x72))
(or (not x619) (not x3) (not x72))
(or (not x787) x785 x786)
(or x787 (not x785) x786)
(or x787 x785 (not x786))
(or (not x787) (not x785) (not x786))
(or (not x739) x509 x738)
(or x739 (not x509) x738)
(or x739 x509 (not x738))
(or (not x739) (not x509) (not x738))
(or (not x1066) x375 x376)
(or x1066 (not x375) x376)
(or x1066 x375 (not x376))
(or (not x1066) (not x375) (not x376))
(or (not x1262) x1250 x1251)
(or x1262 (not x1250) x1251)
(or x1262 x1250 (not x1251))
(or (not x1262) (not x1250) (not x1251))
(or (not x719) x503 x718)
(or x719 (not x503) x718)
(or x719 x503 (not x718))
(or (not x719) (not x503) (not x718))
(or (not x1388) x480 x481)
(or x1388 (not x480) x481)
(or x1388 x480 (not x481))
(or (not x1388) (not x480) (not x481))
(or (not x210) x141)
(or (not x210) (not x141) x142)
(or x210 (not x141) (not x142))
(or (not x1410) x1407 x1408)
(or x1410 (not x1407) x1408)
(or x1410 x1407 (not x1408))
(or (not x1410) (not x1407) (not x1408))
(or (not x557) x5 x32)
(or x557 (not x5) x32)
(or x557 x5 (not x32))
(or (not x557) (not x5) (not x32))
(or (not x683) x133 x204)
(or x683 (not x133) x204)
(or x683 x133 (not x204))
(or (not x683) (not x133) (not x204))
(or (not x987) x981 x982)
(or x987 (not x981) x982)
(or x987 x981 (not x982))
(or (not x987) (not x981) (not x982))
(or (not x181) x88)
(or (not x181) (not x88) x89)
(or x181 (not x88) (not x89))
(or (not x852) x131 x182)
(or x852 (not x131) x182)
(or x852 x131 (not x182))
(or (not x852) (not x131) (not x182))
(or (not x567) x27 x69)
(or x567 (not x27) x69)
(or x567 x27 (not x69))
(or (not x567) (not x27) (not x69))
(or (not x705) x114 x126)
(or x705 (not x114) x126)
(or x705 x114 (not x126))
(or (not x705) (not x114) (not x126))
(or (not x1316) x41 x43)
(or x1316 (not x41) x43)
(or x1316 x41 (not x43))
(or (not x1316) (not x41) (not x43))
(or (not x220) x136)
(or (not x220) (not x136) x137)
(or x220 (not x136) (not x137))
(or (not x767) x231 x261)
(or x767 (not x231) x261)
(or x767 x231 (not x261))
(or (not x767) (not x231) (not x261))
(or (not x375) x56)
(or (not x375) (not x56) x84)
(or x375 (not x56) (not x84))
(or (not x374) x56)
(or (not x374) (not x56) x82)
(or x374 (not x56) (not x82) (not x83))
(or (not x374) (not x56) (not x82) x83)
(or (not x1216) x73 x103)
(or x1216 (not x73) x103)
(or x1216 x73 (not x103))
(or (not x1216) (not x73) (not x103))
(or (not x820) x535 x817)
(or x820 (not x535) x817)
(or x820 x535 (not x817))
(or (not x820) (not x535) (not x817))
(or (not x682) x227 x228)
(or x682 (not x227) x228)
(or x682 x227 (not x228))
(or (not x682) (not x227) (not x228))
(or (not x1214) x1209 x1210)
(or x1214 (not x1209) x1210)
(or x1214 x1209 (not x1210))
(or (not x1214) (not x1209) (not x1210))
(or (not x192) x77)
(or (not x192) (not x77) x78)
(or x192 (not x77) (not x78))
(or (not x1362) x1355 x1356)
(or x1362 (not x1355) x1356)
(or x1362 x1355 (not x1356))
(or (not x1362) (not x1355) (not x1356))
(or (not x818) x277 x278)
(or x818 (not x277) x278)
(or x818 x277 (not x278))
(or (not x818) (not x277) (not x278))
(or (not x1108) x223 x278)
(or x1108 (not x223) x278)
(or x1108 x223 (not x278))
(or (not x1108) (not x223) (not x278))
(or (not x633) x130 x142)
(or x633 (not x130) x142)
(or x633 x130 (not x142))
(or (not x633) (not x130) (not x142))
(or (not x669) x493 x668)
(or x669 (not x493) x668)
(or x669 x493 (not x668))
(or (not x669) (not x493) (not x668))
(or (not x779) x212 x235)
(or x779 (not x212) x235)
(or x779 x212 (not x235))
(or (not x779) (not x212) (not x235))
(or (not x226) x133)
(or (not x226) (not x133) x134)
(or x226 (not x133) (not x134))
(or (not x743) x121 x223)
(or x743 (not x121) x223)
(or x743 x121 (not x223))
(or (not x743) (not x121) (not x223))
(or (not x1332) x223 x247)
(or x1332 (not x223) x247)
(or x1332 x223 (not x247))
(or (not x1332) (not x223) (not x247))
(or (not x1295) x359 x454)
(or x1295 (not x359) x454)
(or x1295 x359 (not x454))
(or (not x1295) (not x359) (not x454))
(or (not x942) x567 x939)
(or x942 (not x567) x939)
(or x942 x567 (not x939))
(or (not x942) (not x567) (not x939))
(or (not x1098) x390 x391)
(or x1098 (not x390) x391)
(or x1098 x390 (not x391))
(or (not x1098) (not x390) (not x391))
(or (not x782) x114 x141)
(or x782 (not x114) x141)
(or x782 x114 (not x141))
(or (not x782) (not x114) (not x141))
(or (not x1085) x17 x41)
(or x1085 (not x17) x41)
(or x1085 x17 (not x41))
(or (not x1085) (not x17) (not x41))
(or (not x998) x993 x994)
(or x998 (not x993) x994)
(or x998 x993 (not x994))
(or (not x998) (not x993) (not x994))
(or (not x454) x43)
(or (not x454) (not x43) x69)
(or x454 (not x43) (not x69) (not x70))
(or (not x454) (not x43) (not x69) x70)
(or (not x908) x178 x190)
(or x908 (not x178) x190)
(or x908 x178 (not x190))
(or (not x908) (not x178) (not x190))
(or (not x200) x69)
(or (not x200) (not x69) x70)
(or x200 (not x69) (not x70))
(or (not x406) x51)
(or (not x406) (not x51) x77)
(or x406 (not x51) (not x77) (not x78))
(or (not x406) (not x51) (not x77) x78)
(or (not x661) x659 x660)
(or x661 (not x659) x660)
(or x661 x659 (not x660))
(or (not x661) (not x659) (not x660))
(or (not x1175) x1172 x1173)
(or x1175 (not x1172) x1173)
(or x1175 x1172 (not x1173))
(or (not x1175) (not x1172) (not x1173))
(or (not x583) x19 x88)
(or x583 (not x19) x88)
(or x583 x19 (not x88))
(or (not x583) (not x19) (not x88))
(or (not x909) x303 x304)
(or x909 (not x303) x304)
(or x909 x303 (not x304))
(or (not x909) (not x303) (not x304))
(or (not x419) x49)
(or (not x419) (not x49) x77)
(or x419 (not x49) (not x77))
(or (not x973) x967 x968)
(or x973 (not x967) x968)
(or x973 x967 (not x968))
(or (not x973) (not x967) (not x968))
(or (not x804) x273 x274)
(or x804 (not x273) x274)
(or x804 x273 (not x274))
(or (not x804) (not x273) (not x274))
(or (not x1387) x65 x66)
(or x1387 (not x65) x66)
(or x1387 x65 (not x66))
(or (not x1387) (not x65) (not x66))
(or (not x263) x33)
(or (not x263) (not x33) x34)
(or x263 (not x33) (not x34))
(or (not x846) x285 x286)
(or x846 (not x285) x286)
(or x846 x285 (not x286))
(or (not x846) (not x285) (not x286))
(or (not x1000) x209 x264)
(or x1000 (not x209) x264)
(or x1000 x209 (not x264))
(or (not x1000) (not x209) (not x264))
(or (not x447) x70)
(or (not x447) (not x70) x71)
(or x447 (not x70) (not x71) (not x73))
(or (not x447) (not x70) (not x71) x73)
(or (not x822) x820 x821)
(or x822 (not x820) x821)
(or x822 x820 (not x821))
(or (not x822) (not x820) (not x821))
(or (not x193) x76)
(or (not x193) (not x76) x77)
(or x193 (not x76) (not x77))
(or (not x477) x65)
(or (not x477) (not x65) x66)
(or x477 (not x65) (not x66) (not x68))
(or (not x477) (not x65) (not x66) x68)
(or (not x914) x909 x910)
(or x914 (not x909) x910)
(or x914 x909 (not x910))
(or (not x914) (not x909) (not x910))
(or (not x658) x138 x199)
(or x658 (not x138) x199)
(or x658 x138 (not x199))
(or (not x658) (not x138) (not x199))
(or (not x740) x107 x119)
(or x740 (not x107) x119)
(or x740 x107 (not x119))
(or (not x740) (not x107) (not x119))
(or (not x1035) x362 x363)
(or x1035 (not x362) x363)
(or x1035 x362 (not x363))
(or (not x1035) (not x362) (not x363))
(or (not x708) x128 x209)
(or x708 (not x128) x209)
(or x708 x128 (not x209))
(or (not x708) (not x128) (not x209))
(or (not x1305) x1290 x1291)
(or x1305 (not x1290) x1291)
(or x1305 x1290 (not x1291))
(or (not x1305) (not x1290) (not x1291))
(or (not x405) x77)
(or (not x405) (not x77) x78)
(or x405 (not x77) (not x78) (not x80))
(or (not x405) (not x77) (not x78) x80)
(or (not x290) x101)
(or (not x290) (not x101) x102)
(or x290 (not x101) (not x102))
(or (not x701) x699 x700)
(or x701 (not x699) x700)
(or x701 x699 (not x700))
(or (not x701) (not x699) (not x700))
(or (not x919) x307 x308)
(or x919 (not x307) x308)
(or x919 x307 (not x308))
(or (not x919) (not x307) (not x308))
(or (not x712) x239 x240)
(or x712 (not x239) x240)
(or x712 x239 (not x240))
(or (not x712) (not x239) (not x240))
(or (not x1398) x66 x94)
(or x1398 (not x66) x94)
(or x1398 x66 (not x94))
(or (not x1398) (not x66) (not x94))
(or (not x1359) x1357 x1358)
(or x1359 (not x1357) x1358)
(or x1359 x1357 (not x1358))
(or (not x1359) (not x1357) (not x1358))
(or (not x355) x60)
(or (not x355) (not x60) x86)
(or x355 (not x60) (not x86))
(or (not x1170) x12 x36)
(or x1170 (not x12) x36)
(or x1170 x12 (not x36))
(or (not x1170) (not x12) (not x36))
(or (not x1174) x422 x423)
(or x1174 (not x422) x423)
(or x1174 x422 (not x423))
(or (not x1174) (not x422) (not x423))
(or (not x1165) x1163 x637)
(or x1165 (not x1163) x637)
(or x1165 x1163 (not x637))
(or (not x1165) (not x1163) (not x637))
(or (not x864) x862 x863)
(or x864 (not x862) x863)
(or x864 x862 (not x863))
(or (not x864) (not x862) (not x863))
(or (not x1087) x221 x276)
(or x1087 (not x221) x276)
(or x1087 x221 (not x276))
(or (not x1087) (not x221) (not x276))
(or (not x1054) x112 x187)
(or x1054 (not x112) x187)
(or x1054 x112 (not x187))
(or (not x1054) (not x112) (not x187))
(or (not x1249) x444 x445)
(or x1249 (not x444) x445)
(or x1249 x444 (not x445))
(or (not x1249) (not x444) (not x445))
(or (not x487) x39)
(or (not x487) (not x39) x63)
(or x487 (not x39) (not x63) (not x64))
(or (not x487) (not x39) (not x63) x64)
(or (not x441) x71)
(or (not x441) (not x71) x72)
(or x441 (not x71) (not x72) (not x74))
(or (not x441) (not x71) (not x72) x74)
(or (not x249) x40)
(or (not x249) (not x40) x41)
(or x249 (not x40) (not x41))
(or (not x629) x134 x188)
(or x629 (not x134) x188)
(or x629 x134 (not x188))
(or (not x629) (not x134) (not x188))
(or (not x1053) x19 x43)
(or x1053 (not x19) x43)
(or x1053 x19 (not x43))
(or (not x1053) (not x19) (not x43))
(or (not x415) x51)
(or (not x415) (not x51) x75)
(or x415 (not x51) (not x75) (not x76))
(or (not x415) (not x51) (not x75) x76)
(or (not x873) x128 x185)
(or x873 (not x128) x185)
(or x873 x128 (not x185))
(or (not x873) (not x128) (not x185))
(or (not x190) x79)
(or (not x190) (not x79) x80)
(or x190 (not x79) (not x80))
(or (not x936) x313 x314)
(or x936 (not x313) x314)
(or x936 x313 (not x314))
(or (not x936) (not x313) (not x314))
(or (not x1274) x449 x450)
(or x1274 (not x449) x450)
(or x1274 x449 (not x450))
(or (not x1274) (not x449) (not x450))
(or (not x665) x122 x134)
(or x665 (not x122) x134)
(or x665 x122 (not x134))
(or (not x665) (not x122) (not x134))
(or (not x714) x502 x713)
(or x714 (not x502) x713)
(or x714 x502 (not x713))
(or (not x714) (not x502) (not x713))
(or (not x1386) x1384 x1385)
(or x1386 (not x1384) x1385)
(or x1386 x1384 (not x1385))
(or (not x1386) (not x1384) (not x1385))
(or (not x1241) x1230 x1231)
(or x1241 (not x1230) x1231)
(or x1241 x1230 (not x1231))
(or (not x1241) (not x1230) (not x1231))
(or (not x413) x50)
(or (not x413) (not x50) x78)
(or x413 (not x50) (not x78))
(or (not x1113) x1110 x1111)
(or x1113 (not x1110) x1111)
(or x1113 x1110 (not x1111))
(or (not x1113) (not x1110) (not x1111))
(or (not x1222) x1219 x1220)
(or x1222 (not x1219) x1220)
(or x1222 x1219 (not x1220))
(or (not x1222) (not x1219) (not x1220))
(or (not x1237) x441 x1223)
(or x1237 (not x441) x1223)
(or x1237 x441 (not x1223))
(or (not x1237) (not x441) (not x1223))
(or (not x997) x346 x347)
(or x997 (not x346) x347)
(or x997 x346 (not x347))
(or (not x997) (not x346) (not x347))
(or (not x983) x339 x340)
(or x983 (not x339) x340)
(or x983 x339 (not x340))
(or (not x983) (not x339) (not x340))
(or (not x456) x44)
(or (not x456) (not x44) x70)
(or x456 (not x44) (not x70))
(or (not x1207) x235 x290)
(or x1207 (not x235) x290)
(or x1207 x235 (not x290))
(or (not x1207) (not x235) (not x290))
(or (not x1070) x18 x42)
(or x1070 (not x18) x42)
(or x1070 x18 (not x42))
(or (not x1070) (not x18) (not x42))
(or (not x795) x790 x791)
(or x795 (not x790) x791)
(or x795 x790 (not x791))
(or (not x795) (not x790) (not x791))
(or (not x1366) x1362 x1363)
(or x1366 (not x1362) x1363)
(or x1366 x1362 (not x1363))
(or (not x1366) (not x1362) (not x1363))
(or (not x1071) x111 x190)
(or x1071 (not x111) x190)
(or x1071 x111 (not x190))
(or (not x1071) (not x111) (not x190))
(or (not x1184) x1182 x1183)
(or x1184 (not x1182) x1183)
(or x1184 x1182 (not x1183))
(or (not x1184) (not x1182) (not x1183))
(or (not x941) x320 x321)
(or x941 (not x320) x321)
(or x941 x320 (not x321))
(or (not x941) (not x320) (not x321))
(or (not x744) x511 x743)
(or x744 (not x511) x743)
(or x744 x511 (not x743))
(or (not x744) (not x511) (not x743))
(or (not x861) x100 x103)
(or x861 (not x100) x103)
(or x861 x100 (not x103))
(or (not x861) (not x100) (not x103))
(or (not x551) x8 x35)
(or x551 (not x8) x35)
(or x551 x8 (not x35))
(or (not x551) (not x8) (not x35))
(or (not x334) x63)
(or (not x334) (not x63) x89)
(or x334 (not x63) (not x89))
(or (not x1187) x64 x104)
(or x1187 (not x64) x104)
(or x1187 x64 (not x104))
(or (not x1187) (not x64) (not x104))
(or (not x1112) x1104 x1105)
(or x1112 (not x1104) x1105)
(or x1112 x1104 (not x1105))
(or (not x1112) (not x1104) (not x1105))
(or (not x521) x23 x50)
(or x521 (not x23) x50)
(or x521 x23 (not x50))
(or (not x521) (not x23) (not x50))
(or (not x848) x543 x845)
(or x848 (not x543) x845)
(or x848 x543 (not x845))
(or (not x848) (not x543) (not x845))
(or (not x1119) x68 x108)
(or x1119 (not x68) x108)
(or x1119 x68 (not x108))
(or (not x1119) (not x68) (not x108))
(or (not x545) x11 x38)
(or x545 (not x11) x38)
(or x545 x11 (not x38))
(or (not x545) (not x11) (not x38))
(or (not x1371) x1366 x1367)
(or x1371 (not x1366) x1367)
(or x1371 x1366 (not x1367))
(or (not x1371) (not x1366) (not x1367))
(or (not x1391) x227 x251)
(or x1391 (not x227) x251)
(or x1391 x227 (not x251))
(or (not x1391) (not x227) (not x251))
(or (not x734) x507 x733)
(or x734 (not x507) x733)
(or x734 x507 (not x733))
(or (not x734) (not x507) (not x733))
(or (not x564) x98 x113)
(or x564 (not x98) x113)
(or x564 x98 (not x113))
(or (not x564) (not x98) (not x113))
(or (not x1215) x1213 x1214)
(or x1215 (not x1213) x1214)
(or x1215 x1213 (not x1214))
(or (not x1215) (not x1213) (not x1214))
(or (not x986) x208 x262)
(or x986 (not x208) x262)
(or x986 x208 (not x262))
(or (not x986) (not x208) (not x262))
(or (not x444) x46)
(or (not x444) (not x46) x72)
(or x444 (not x46) (not x72))
(or (not x854) x101 x104)
(or x854 (not x101) x104)
(or x854 x101 (not x104))
(or (not x854) (not x101) (not x104))
(or (not x954) x328 x329)
(or x954 (not x328) x329)
(or x954 x328 (not x329))
(or (not x954) (not x328) (not x329))
(or (not x643) x142 x195)
(or x643 (not x142) x195)
(or x643 x142 (not x195))
(or (not x643) (not x142) (not x195))
(or (not x1254) x1246 x1247)
(or x1254 (not x1246) x1247)
(or x1254 x1246 (not x1247))
(or (not x1254) (not x1246) (not x1247))
(or (not x327) x64)
(or (not x327) (not x64) x90)
(or x327 (not x64) (not x90))
(or (not x755) x104 x116)
(or x755 (not x104) x116)
(or x755 x104 (not x116))
(or (not x755) (not x104) (not x116))
(or (not x1261) x1255 x1256)
(or x1261 (not x1255) x1256)
(or x1261 x1255 (not x1256))
(or (not x1261) (not x1255) (not x1256))
(or (not x215) x57)
(or (not x215) (not x57) x58)
(or x215 (not x57) (not x58))
(or (not x680) x119 x131)
(or x680 (not x119) x131)
(or x680 x119 (not x131))
(or (not x680) (not x119) (not x131))
(or (not x1223) x9 x33)
(or x1223 (not x9) x33)
(or x1223 x9 (not x33))
(or (not x1223) (not x9) (not x33))
(or (not x385) x80)
(or (not x385) (not x80) x81)
(or x385 (not x80) (not x81) (not x82))
(or (not x385) (not x80) (not x81) x82)
(or (not x286) x103)
(or (not x286) (not x103) x104)
(or x286 (not x103) (not x104))
(or (not x560) x100 x115)
(or x560 (not x100) x115)
(or x560 x100 (not x115))
(or (not x560) (not x100) (not x115))
(or (not x323) x89)
(or (not x323) (not x89) x90)
(or x323 (not x89) (not x90) (not x92))
(or (not x323) (not x89) (not x90) x92)
(or (not x856) x234 x257)
(or x856 (not x234) x257)
(or x856 x234 (not x257))
(or (not x856) (not x234) (not x257))
(or (not x1156) x413 x414)
(or x1156 (not x413) x414)
(or x1156 x413 (not x414))
(or (not x1156) (not x413) (not x414))
(or (not x296) x98)
(or (not x296) (not x98) x99)
(or x296 (not x98) (not x99))
(or (not x1130) x1127 x1128)
(or x1130 (not x1127) x1128)
(or x1130 x1127 (not x1128))
(or (not x1130) (not x1127) (not x1128))
(or (not x1072) x274 x297)
(or x1072 (not x274) x297)
(or x1072 x274 (not x297))
(or (not x1072) (not x274) (not x297))
(or (not x304) x94)
(or (not x304) (not x94) x95)
(or x304 (not x94) (not x95))
(or (not x1354) x68 x96)
(or x1354 (not x68) x96)
(or x1354 x68 (not x96))
(or (not x1354) (not x68) (not x96))
(or (not x481) x40)
(or (not x481) (not x40) x64)
(or x481 (not x40) (not x64) (not x65))
(or (not x481) (not x40) (not x64) x65)
(or (not x584) x103 x183)
(or x584 (not x103) x183)
(or x584 x103 (not x183))
(or (not x584) (not x103) (not x183))
(or (not x904) x559 x901)
(or x904 (not x559) x901)
(or x904 x559 (not x901))
(or (not x904) (not x559) (not x901))
(or (not x537) x15 x42)
(or x537 (not x15) x42)
(or x537 x15 (not x42))
(or (not x537) (not x15) (not x42))
(or (not x512) x124 x139)
(or x512 (not x124) x139)
(or x512 x124 (not x139))
(or (not x512) (not x124) (not x139))
(or (not x1313) x463 x464)
(or x1313 (not x463) x464)
(or x1313 x463 (not x464))
(or (not x1313) (not x463) (not x464))
(or (not x1131) x401 x402)
(or x1131 (not x401) x402)
(or x1131 x401 (not x402))
(or (not x1131) (not x401) (not x402))
(or (not x1011) x64 x73)
(or x1011 (not x64) x73)
(or x1011 x64 (not x73))
(or (not x1011) (not x64) (not x73))
(or (not x569) x26 x68)
(or x569 (not x26) x68)
(or x569 x26 (not x68))
(or (not x569) (not x26) (not x68))
(or (not x266) x113)
(or (not x266) (not x113) x114)
(or x266 (not x113) (not x114))
(or (not x870) x238 x261)
(or x870 (not x238) x261)
(or x870 x238 (not x261))
(or (not x870) (not x238) (not x261))
(or (not x216) x138)
(or (not x216) (not x138) x139)
(or x216 (not x138) (not x139))
(or (not x925) x254 x277)
(or x925 (not x254) x277)
(or x925 x254 (not x277))
(or (not x925) (not x254) (not x277))
(or (not x1248) x294 x345)
(or x1248 (not x294) x345)
(or x1248 x294 (not x345))
(or (not x1248) (not x294) (not x345))
(or (not x407) x51)
(or (not x407) (not x51) x79)
(or x407 (not x51) (not x79))
(or (not x966) x334 x335)
(or x966 (not x334) x335)
(or x966 x334 (not x335))
(or (not x966) (not x334) (not x335))
(or (not x1318) x1311 x1312)
(or x1318 (not x1311) x1312)
(or x1318 x1311 (not x1312))
(or (not x1318) (not x1311) (not x1312))
(or (not x1275) x1268 x1269)
(or x1275 (not x1268) x1269)
(or x1275 x1268 (not x1269))
(or (not x1275) (not x1268) (not x1269))
(or (not x486) x39)
(or (not x486) (not x39) x65)
(or x486 (not x39) (not x65))
(or (not x660) x123 x135)
(or x660 (not x123) x135)
(or x660 x123 (not x135))
(or (not x660) (not x123) (not x135))
(or (not x1416) x1414 x1160)
(or x1416 (not x1414) x1160)
(or x1416 x1414 (not x1160))
(or (not x1416) (not x1414) (not x1160))
(or (not x380) x1)
(or (not x380) (not x1) x2)
(or x380 (not x1) (not x2))
(or (not x1280) x241 x296)
(or x1280 (not x241) x296)
(or x1280 x241 (not x296))
(or (not x1280) (not x241) (not x296))
(or (not x759) x517 x758)
(or x759 (not x517) x758)
(or x759 x517 (not x758))
(or (not x759) (not x517) (not x758))
(or (not x532) x114 x129)
(or x532 (not x114) x129)
(or x532 x114 (not x129))
(or (not x532) (not x114) (not x129))
(or (not x418) x49)
(or (not x418) (not x49) x75)
(or x418 (not x49) (not x75) (not x76))
(or (not x418) (not x49) (not x75) x76)
(or (not x849) x232 x255)
(or x849 (not x232) x255)
(or x849 x232 (not x255))
(or (not x849) (not x232) (not x255))
(or (not x707) x237 x238)
(or x707 (not x237) x238)
(or x707 x237 (not x238))
(or (not x707) (not x237) (not x238))
(or (not x514) x123 x138)
(or x514 (not x123) x138)
(or x514 x123 (not x138))
(or (not x514) (not x123) (not x138))
(or (not x465) x67)
(or (not x465) (not x67) x68)
(or x465 (not x67) (not x68) (not x70))
(or (not x465) (not x67) (not x68) x70)
(or (not x738) x122 x221)
(or x738 (not x122) x221)
(or x738 x122 (not x221))
(or (not x738) (not x122) (not x221))
(or (not x254) x119)
(or (not x254) (not x119) x120)
(or x254 (not x119) (not x120))
(or (not x439) x47)
(or (not x439) (not x47) x71)
(or x439 (not x47) (not x71) (not x72))
(or (not x439) (not x47) (not x71) x72)
(or (not x367) x57)
(or (not x367) (not x57) x83)
(or x367 (not x57) (not x83) (not x84))
(or (not x367) (not x57) (not x83) x84)
(or (not x597) x12 x81)
(or x597 (not x12) x81)
(or x597 x12 (not x81))
(or (not x597) (not x12) (not x81))
(or (not x797) x271 x272)
(or x797 (not x271) x272)
(or x797 x271 (not x272))
(or (not x797) (not x271) (not x272))
(or (not x1149) x1146 x1147)
(or x1149 (not x1146) x1147)
(or x1149 x1146 (not x1147))
(or (not x1149) (not x1146) (not x1147))
(or (not x710) x113 x125)
(or x710 (not x113) x125)
(or x710 x113 (not x125))
(or (not x710) (not x113) (not x125))
(or (not x803) x111 x138)
(or x803 (not x111) x138)
(or x803 x111 (not x138))
(or (not x803) (not x111) (not x138))
(or (not x398) x78)
(or (not x398) (not x78) x79)
(or x398 (not x78) (not x79) (not x80))
(or (not x398) (not x78) (not x79) x80)
(or (not x446) x70)
(or (not x446) (not x70) x71)
(or x446 (not x70) (not x71) (not x72))
(or (not x446) (not x70) (not x71) x72)
(or (not x1210) x1207 x1208)
(or x1210 (not x1207) x1208)
(or x1210 x1207 (not x1208))
(or (not x1210) (not x1207) (not x1208))
(or (not x301) x14)
(or (not x301) (not x14) x15)
(or x301 (not x14) (not x15))
(or (not x1077) x380 x381)
(or x1077 (not x380) x381)
(or x1077 x380 (not x381))
(or (not x1077) (not x380) (not x381))
(or (not x1418) x1415 x1416)
(or x1418 (not x1415) x1416)
(or x1418 x1415 (not x1416))
(or (not x1418) (not x1415) (not x1416))
(or (not x985) x983 x984)
(or x985 (not x983) x984)
(or x985 x983 (not x984))
(or (not x985) (not x983) (not x984))
(or (not x197) x72)
(or (not x197) (not x72) x73)
(or x197 (not x72) (not x73))
(or (not x1034) x1032 x1033)
(or x1034 (not x1032) x1033)
(or x1034 x1032 (not x1033))
(or (not x1034) (not x1032) (not x1033))
(or (not x717) x241 x242)
(or x717 (not x241) x242)
(or x717 x241 (not x242))
(or (not x717) (not x241) (not x242))
(or (not x1238) x1234 x1235)
(or x1238 (not x1234) x1235)
(or x1238 x1234 (not x1235))
(or (not x1238) (not x1234) (not x1235))
(or (not x1343) x56 x57)
(or x1343 (not x56) x57)
(or x1343 x56 (not x57))
(or (not x1343) (not x56) (not x57))
(or (not x1151) x1148 x1149)
(or x1151 (not x1148) x1149)
(or x1151 x1148 (not x1149))
(or (not x1151) (not x1148) (not x1149))
(or (not x1107) x58 x67)
(or x1107 (not x58) x67)
(or x1107 x58 (not x67))
(or (not x1107) (not x58) (not x67))
(or (not x274) x109)
(or (not x274) (not x109) x110)
(or x274 (not x109) (not x110))
(or (not x581) x20 x89)
(or x581 (not x20) x89)
(or x581 x20 (not x89))
(or (not x581) (not x20) (not x89))
(or (not x883) x553 x880)
(or x883 (not x553) x880)
(or x883 x553 (not x880))
(or (not x883) (not x553) (not x880))
(or (not x1088) x388 x389)
(or x1088 (not x388) x389)
(or x1088 x388 (not x389))
(or (not x1088) (not x388) (not x389))
(or (not x1096) x1089 x1090)
(or x1096 (not x1089) x1090)
(or x1096 x1089 (not x1090))
(or (not x1096) (not x1089) (not x1090))
(or (not x536) x112 x127)
(or x536 (not x112) x127)
(or x536 x112 (not x127))
(or (not x536) (not x112) (not x127))
(or (not x1224) x51 x60)
(or x1224 (not x51) x60)
(or x1224 x51 (not x60))
(or (not x1224) (not x51) (not x60))
(or (not x1298) x1296 x1297)
(or x1298 (not x1296) x1297)
(or x1298 x1296 (not x1297))
(or (not x1298) (not x1296) (not x1297))
(or (not x183) x86)
(or (not x183) (not x86) x87)
(or x183 (not x86) (not x87))
(or (not x1382) x204 x205)
(or x1382 (not x204) x205)
(or x1382 x204 (not x205))
(or (not x1382) (not x204) (not x205))
(or (not x1409) x1404 x1405)
(or x1409 (not x1404) x1405)
(or x1409 x1404 (not x1405))
(or (not x1409) (not x1404) (not x1405))
(or (not x1068) x1060 x1061)
(or x1068 (not x1060) x1061)
(or x1068 x1060 (not x1061))
(or (not x1068) (not x1060) (not x1061))
(or (not x862) x547 x859)
(or x862 (not x547) x859)
(or x862 x547 (not x859))
(or (not x862) (not x547) (not x859))
(or (not x1078) x1071 x1072)
(or x1078 (not x1071) x1072)
(or x1078 x1071 (not x1072))
(or (not x1078) (not x1071) (not x1072))
(or (not x918) x95 x122)
(or x918 (not x95) x122)
(or x918 x95 (not x122))
(or (not x918) (not x95) (not x122))
(or (not x1188) x196 x197)
(or x1188 (not x196) x197)
(or x1188 x196 (not x197))
(or (not x1188) (not x196) (not x197))
(or (not x721) x719 x720)
(or x721 (not x719) x720)
(or x721 x719 (not x720))
(or (not x721) (not x719) (not x720))
(or (not x1367) x249 x304)
(or x1367 (not x249) x304)
(or x1367 x249 (not x304))
(or (not x1367) (not x249) (not x304))
(or (not x930) x309 x310)
(or x930 (not x309) x310)
(or x930 x309 (not x310))
(or (not x930) (not x309) (not x310))
(or (not x348) x61)
(or (not x348) (not x61) x87)
(or x348 (not x61) (not x87))
(or (not x273) x28)
(or (not x273) (not x28) x29)
(or x273 (not x28) (not x29))
(or (not x906) x904 x905)
(or x906 (not x904) x905)
(or x906 x904 (not x905))
(or (not x906) (not x904) (not x905))
(or (not x1351) x1346 x1347)
(or x1351 (not x1346) x1347)
(or x1351 x1346 (not x1347))
(or (not x1351) (not x1346) (not x1347))
(or (not x1051) x1049 x1050)
(or x1051 (not x1049) x1050)
(or x1051 x1049 (not x1050))
(or (not x1051) (not x1049) (not x1050))
(or (not x965) x283 x331)
(or x965 (not x283) x331)
(or x965 x283 (not x331))
(or (not x965) (not x283) (not x331))
(or (not x724) x504 x723)
(or x724 (not x504) x723)
(or x724 x504 (not x723))
(or (not x724) (not x504) (not x723))
(or (not x814) x222 x245)
(or x814 (not x222) x245)
(or x814 x222 (not x245))
(or (not x814) (not x222) (not x245))
(or (not x656) x654 x655)
(or x656 (not x654) x655)
(or x656 x654 (not x655))
(or (not x656) (not x654) (not x655))
(or (not x819) x94 x106)
(or x819 (not x94) x106)
(or x819 x94 (not x106))
(or (not x819) (not x94) (not x106))
(or (not x695) x116 x128)
(or x695 (not x116) x128)
(or x695 x116 (not x128))
(or (not x695) (not x116) (not x128))
(or (not x1079) x1077 x1078)
(or x1079 (not x1077) x1078)
(or x1079 x1077 (not x1078))
(or (not x1079) (not x1077) (not x1078))
(or (not x1230) x1228 x1229)
(or x1230 (not x1228) x1229)
(or x1230 x1228 (not x1229))
(or (not x1230) (not x1228) (not x1229))
(or (not x529) x19 x46)
(or x529 (not x19) x46)
(or x529 x19 (not x46))
(or (not x529) (not x19) (not x46))
(or (not x785) x525 x782)
(or x785 (not x525) x782)
(or x785 x525 (not x782))
(or (not x785) (not x525) (not x782))
(or (not x379) x81)
(or (not x379) (not x81) x82)
(or x379 (not x81) (not x82) (not x84))
(or (not x379) (not x81) (not x82) x84)
(or (not x1225) x102 x138)
(or x1225 (not x102) x138)
(or x1225 x102 (not x138))
(or (not x1225) (not x102) (not x138))
(or (not x1121) x303 x400)
(or x1121 (not x303) x400)
(or x1121 x303 (not x400))
(or (not x1121) (not x303) (not x400))
(or (not x692) x231 x232)
(or x692 (not x231) x232)
(or x692 x231 (not x232))
(or (not x692) (not x231) (not x232))
(or (not x1013) x358 x1005)
(or x1013 (not x358) x1005)
(or x1013 x358 (not x1005))
(or (not x1013) (not x358) (not x1005))
(or (not x1356) x380 x472)
(or x1356 (not x380) x472)
(or x1356 x380 (not x472))
(or (not x1356) (not x380) (not x472))
(or (not x1342) x1340 x1341)
(or x1342 (not x1340) x1341)
(or x1342 x1340 (not x1341))
(or (not x1342) (not x1340) (not x1341))
(or (not x1001) x995 x996)
(or x1001 (not x995) x996)
(or x1001 x995 (not x996))
(or (not x1001) (not x995) (not x996))
(or (not x279) x25)
(or (not x279) (not x25) x26)
(or x279 (not x25) (not x26))
(or (not x570) x95 x110)
(or x570 (not x95) x110)
(or x570 x95 (not x110))
(or (not x570) (not x95) (not x110))
(or (not x390) x55)
(or (not x390) (not x55) x81)
(or x390 (not x55) (not x81))
(or (not x179) x90)
(or (not x179) (not x90) x91)
(or x179 (not x90) (not x91))
(or (not x1134) x1131 x1132)
(or x1134 (not x1131) x1132)
(or x1134 x1131 (not x1132))
(or (not x1134) (not x1131) (not x1132))
(or (not x543) x12 x39)
(or x543 (not x12) x39)
(or x543 x12 (not x39))
(or (not x543) (not x12) (not x39))
(or (not x762) x259 x260)
(or x762 (not x259) x260)
(or x762 x259 (not x260))
(or (not x762) (not x259) (not x260))
(or (not x1341) x1336 x1337)
(or x1341 (not x1336) x1337)
(or x1341 x1336 (not x1337))
(or (not x1341) (not x1336) (not x1337))
(or (not x1208) x431 x432)
(or x1208 (not x431) x432)
(or x1208 x431 (not x432))
(or (not x1208) (not x431) (not x432))
(or (not x698) x130 x207)
(or x698 (not x130) x207)
(or x698 x130 (not x207))
(or (not x698) (not x130) (not x207))
(or (not x1293) x42 x43)
(or x1293 (not x42) x43)
(or x1293 x42 (not x43))
(or (not x1293) (not x42) (not x43))
(or (not x1372) x2 x26)
(or x1372 (not x2) x26)
(or x1372 x2 (not x26))
(or (not x1372) (not x2) (not x26))
(or (not x694) x498 x693)
(or x694 (not x498) x693)
(or x694 x498 (not x693))
(or (not x694) (not x498) (not x693))
(or (not x1033) x1026 x1027)
(or x1033 (not x1026) x1027)
(or x1033 x1026 (not x1027))
(or (not x1033) (not x1026) (not x1027))
(or (not x811) x275 x276)
(or x811 (not x275) x276)
(or x811 x275 (not x276))
(or (not x811) (not x275) (not x276))
(or (not x790) x269 x270)
(or x790 (not x269) x270)
(or x790 x269 (not x270))
(or (not x790) (not x269) (not x270))
(or (not x222) x135)
(or (not x222) (not x135) x136)
(or x222 (not x135) (not x136))
(or (not x368) x57)
(or (not x368) (not x57) x85)
(or x368 (not x57) (not x85))
(or (not x647) x141 x196)
(or x647 (not x141) x196)
(or x647 x141 (not x196))
(or (not x647) (not x141) (not x196))
(or (not x606) x179 x194)
(or x606 (not x179) x194)
(or x606 x179 (not x194))
(or (not x606) (not x179) (not x194))
(or (not x799) x529 x796)
(or x799 (not x529) x796)
(or x799 x529 (not x796))
(or (not x799) (not x529) (not x796))
(or (not x1030) x1022 x1023)
(or x1030 (not x1022) x1023)
(or x1030 x1022 (not x1023))
(or (not x1030) (not x1022) (not x1023))
(or (not x516) x122 x137)
(or x516 (not x122) x137)
(or x516 x122 (not x137))
(or (not x516) (not x122) (not x137))
(or (not x542) x109 x124)
(or x542 (not x109) x124)
(or x542 x109 (not x124))
(or (not x542) (not x109) (not x124))
(or (not x666) x664 x665)
(or x666 (not x664) x665)
(or x666 x664 (not x665))
(or (not x666) (not x664) (not x665))
(or (not x703) x129 x208)
(or x703 (not x129) x208)
(or x703 x129 (not x208))
(or (not x703) (not x129) (not x208))
(or (not x681) x679 x680)
(or x681 (not x679) x680)
(or x681 x679 (not x680))
(or (not x681) (not x679) (not x680))
(or (not x468) x42)
(or (not x468) (not x42) x68)
(or x468 (not x42) (not x68))
(or (not x886) x881 x882)
(or x886 (not x881) x882)
(or x886 x881 (not x882))
(or (not x886) (not x881) (not x882))
(or (not x1024) x213 x268)
(or x1024 (not x213) x268)
(or x1024 x213 (not x268))
(or (not x1024) (not x213) (not x268))
(or (not x577) x22 x91)
(or x577 (not x22) x91)
(or x577 x22 (not x91))
(or (not x577) (not x22) (not x91))
(or (not x1125) x225 x280)
(or x1125 (not x225) x280)
(or x1125 x225 (not x280))
(or (not x1125) (not x225) (not x280))
(or (not x625) x1 x70)
(or x625 (not x1) x70)
(or x625 x1 (not x70))
(or (not x625) (not x1) (not x70))
(or (not x316) x92)
(or (not x316) (not x92) x93)
(or x316 (not x92) (not x93))
(or (not x496) x40 x67)
(or x496 (not x40) x67)
(or x496 x40 (not x67))
(or (not x496) (not x40) (not x67))
(or (not x479) x39)
(or (not x479) (not x39) x67)
(or x479 (not x39) (not x67))
(or (not x898) x246 x269)
(or x898 (not x246) x269)
(or x898 x246 (not x269))
(or (not x898) (not x246) (not x269))
(or (not x1365) x477 x1352)
(or x1365 (not x477) x1352)
(or x1365 x477 (not x1352))
(or (not x1365) (not x477) (not x1352))
(or (not x979) x285 x338)
(or x979 (not x285) x338)
(or x979 x285 (not x338))
(or (not x979) (not x285) (not x338))
(or (not x642) x211 x212)
(or x642 (not x211) x212)
(or x642 x211 (not x212))
(or (not x642) (not x211) (not x212))
(or (not x250) x121)
(or (not x250) (not x121) x122)
(or x250 (not x121) (not x122))
(or (not x198) x71)
(or (not x198) (not x71) x72)
(or x198 (not x71) (not x72))
(or (not x838) x133 x180)
(or x838 (not x133) x180)
(or x838 x133 (not x180))
(or (not x838) (not x133) (not x180))
(or (not x650) x215 x216)
(or x650 (not x215) x216)
(or x650 x215 (not x216))
(or (not x650) (not x215) (not x216))
(or (not x1153) x65 x106)
(or x1153 (not x65) x106)
(or x1153 x65 (not x106))
(or (not x1153) (not x65) (not x106))
(or (not x1250) x1244 x1245)
(or x1250 (not x1244) x1245)
(or x1250 x1244 (not x1245))
(or (not x1250) (not x1244) (not x1245))
(or (not x430) x47)
(or (not x430) (not x47) x73)
(or x430 (not x47) (not x73) (not x74))
(or (not x430) (not x47) (not x73) x74)
(or (not x653) x139 x198)
(or x653 (not x139) x198)
(or x653 x139 (not x198))
(or (not x653) (not x139) (not x198))
(or (not x243) x43)
(or (not x243) (not x43) x44)
(or x243 (not x43) (not x44))
(or (not x970) x965 x966)
(or x970 (not x965) x966)
(or x970 x965 (not x966))
(or (not x970) (not x965) (not x966))
(or (not x1239) x237 x292)
(or x1239 (not x237) x292)
(or x1239 x237 (not x292))
(or (not x1239) (not x237) (not x292))
(or (not x1111) x191 x192)
(or x1111 (not x191) x192)
(or x1111 x191 (not x192))
(or (not x1111) (not x191) (not x192))
(or (not x520) x120 x135)
(or x520 (not x120) x135)
(or x520 x120 (not x135))
(or (not x520) (not x120) (not x135))
(or (not x1166) x309 x412)
(or x1166 (not x309) x412)
(or x1166 x309 (not x412))
(or (not x1166) (not x309) (not x412))
(or (not x275) x27)
(or (not x275) (not x27) x28)
(or x275 (not x27) (not x28))
(or (not x903) x94 x97)
(or x903 (not x94) x97)
(or x903 x94 (not x97))
(or (not x903) (not x94) (not x97))
(or (not x1396) x1 x25)
(or x1396 (not x1) x25)
(or x1396 x1 (not x25))
(or (not x1396) (not x1) (not x25))
(or (not x817) x109 x136)
(or x817 (not x109) x136)
(or x817 x109 (not x136))
(or (not x817) (not x109) (not x136))
(or (not x1074) x386 x1070)
(or x1074 (not x386) x1070)
(or x1074 x386 (not x1070))
(or (not x1074) (not x386) (not x1070))
(or (not x1014) x1010 x1011)
(or x1014 (not x1010) x1011)
(or x1014 x1010 (not x1011))
(or (not x1014) (not x1010) (not x1011))
(or (not x435) x72)
(or (not x435) (not x72) x73)
(or x435 (not x72) (not x73) (not x75))
(or (not x435) (not x72) (not x73) x75)
(or (not x1002) x350 x351)
(or x1002 (not x350) x351)
(or x1002 x350 (not x351))
(or (not x1002) (not x350) (not x351))
(or (not x1379) x1374 x1375)
(or x1379 (not x1374) x1375)
(or x1379 x1374 (not x1375))
(or (not x1379) (not x1374) (not x1375))
(or (not x1311) x215 x221)
(or x1311 (not x215) x221)
(or x1311 x215 (not x221))
(or (not x1311) (not x215) (not x221))
(or (not x1290) x455 x456)
(or x1290 (not x455) x456)
(or x1290 x455 (not x456))
(or (not x1290) (not x455) (not x456))
(or (not x1284) x1279 x1280)
(or x1284 (not x1279) x1280)
(or x1284 x1279 (not x1280))
(or (not x1284) (not x1279) (not x1280))
(or (not x1315) x1313 x1314)
(or x1315 (not x1313) x1314)
(or x1315 x1313 (not x1314))
(or (not x1315) (not x1313) (not x1314))
(or (not x1161) x415 x416)
(or x1161 (not x415) x416)
(or x1161 x415 (not x416))
(or (not x1161) (not x415) (not x416))
(or (not x191) x78)
(or (not x191) (not x78) x79)
(or x191 (not x78) (not x79))
(or (not x1227) x338 x436)
(or x1227 (not x338) x436)
(or x1227 x338 (not x436))
(or (not x1227) (not x338) (not x436))
(or (not x331) x8)
(or (not x331) (not x8) x9)
(or x331 (not x8) (not x9))
(or (not x791) x98 x110)
(or x791 (not x98) x110)
(or x791 x98 (not x110))
(or (not x791) (not x98) (not x110))
(or (not x1417) x488 x489)
(or x1417 (not x488) x489)
(or x1417 x488 (not x489))
(or (not x1417) (not x488) (not x489))
(or (not x902) x301 x302)
(or x902 (not x301) x302)
(or x902 x301 (not x302))
(or (not x902) (not x301) (not x302))
(or (not x397) x54)
(or (not x397) (not x54) x78)
(or x397 (not x54) (not x78) (not x79))
(or (not x397) (not x54) (not x78) x79)
(or (not x335) x63)
(or (not x335) (not x63) x87)
(or x335 (not x63) (not x87) (not x88))
(or (not x335) (not x63) (not x87) x88)
(or (not x1270) x451 x452)
(or x1270 (not x451) x452)
(or x1270 x451 (not x452))
(or (not x1270) (not x451) (not x452))
(or (not x1412) x927 x1401)
(or x1412 (not x927) x1401)
(or x1412 x927 (not x1401))
(or (not x1412) (not x927) (not x1401))
(or (not x1127) x1123 x1124)
(or x1127 (not x1123) x1124)
(or x1127 x1123 (not x1124))
(or (not x1127) (not x1123) (not x1124))
(or (not x548) x106 x121)
(or x548 (not x106) x121)
(or x548 x106 (not x121))
(or (not x548) (not x106) (not x121))
(or (not x1136) x66 x67)
(or x1136 (not x66) x67)
(or x1136 x66 (not x67))
(or (not x1136) (not x66) (not x67))
(or (not x1256) x71 x72)
(or x1256 (not x71) x72)
(or x1256 x71 (not x72))
(or (not x1256) (not x71) (not x72))
(or (not x796) x112 x139)
(or x796 (not x112) x139)
(or x796 x112 (not x139))
(or (not x796) (not x112) (not x139))
(or (not x1267) x72 x100)
(or x1267 (not x72) x100)
(or x1267 x72 (not x100))
(or (not x1267) (not x72) (not x100))
(or (not x771) x101 x113)
(or x771 (not x101) x113)
(or x771 x101 (not x113))
(or (not x771) (not x101) (not x113))
(or (not x685) x118 x130)
(or x685 (not x118) x130)
(or x685 x118 (not x130))
(or (not x685) (not x118) (not x130))
(or (not x321) x65)
(or (not x321) (not x65) x89)
(or x321 (not x65) (not x89) (not x90))
(or (not x321) (not x65) (not x89) x90)
(or (not x704) x500 x703)
(or x704 (not x500) x703)
(or x704 x500 (not x703))
(or (not x704) (not x500) (not x703))
(or (not x968) x118 x182)
(or x968 (not x118) x182)
(or x968 x118 (not x182))
(or (not x968) (not x118) (not x182))
(or (not x257) x36)
(or (not x257) (not x36) x37)
(or x257 (not x36) (not x37))
(or (not x201) x68)
(or (not x201) (not x68) x69)
(or x201 (not x68) (not x69))
(or (not x284) x104)
(or (not x284) (not x104) x105)
(or x284 (not x104) (not x105))
(or (not x615) x140 x182)
(or x615 (not x140) x182)
(or x615 x140 (not x182))
(or (not x615) (not x140) (not x182))
(or (not x349) x61)
(or (not x349) (not x61) x85)
(or x349 (not x61) (not x85) (not x86))
(or (not x349) (not x61) (not x85) x86)
(or (not x711) x709 x710)
(or x711 (not x709) x710)
(or x711 x709 (not x710))
(or (not x711) (not x709) (not x710))
(or (not x1242) x1240 x1241)
(or x1242 (not x1240) x1241)
(or x1242 x1240 (not x1241))
(or (not x1242) (not x1240) (not x1241))
(or (not x1103) x201 x204)
(or x1103 (not x201) x204)
(or x1103 x201 (not x204))
(or (not x1103) (not x201) (not x204))
(or (not x646) x213 x214)
(or x646 (not x213) x214)
(or x646 x213 (not x214))
(or (not x646) (not x213) (not x214))
(or (not x720) x111 x123)
(or x720 (not x111) x123)
(or x720 x111 (not x123))
(or (not x720) (not x111) (not x123))
(or (not x1086) x110 x190)
(or x1086 (not x110) x190)
(or x1086 x110 (not x190))
(or (not x1086) (not x110) (not x190))
(or (not x982) x117 x183)
(or x982 (not x117) x183)
(or x982 x117 (not x183))
(or (not x982) (not x117) (not x183))
(or (not x1301) x1294 x1295)
(or x1301 (not x1294) x1295)
(or x1301 x1294 (not x1295))
(or (not x1301) (not x1294) (not x1295))
(or (not x366) x3)
(or (not x366) (not x3) x4)
(or x366 (not x3) (not x4))
(or (not x400) x52)
(or (not x400) (not x52) x78)
(or x400 (not x52) (not x78) (not x79))
(or (not x400) (not x52) (not x78) x79)
(or (not x213) x58)
(or (not x213) (not x58) x59)
(or x213 (not x58) (not x59))
(or (not x836) x834 x835)
(or x836 (not x834) x835)
(or x836 x834 (not x835))
(or (not x836) (not x834) (not x835))
(or (not x840) x103 x106)
(or x840 (not x103) x106)
(or x840 x103 (not x106))
(or (not x840) (not x103) (not x106))
(or (not x244) x124)
(or (not x244) (not x124) x125)
(or x244 (not x124) (not x125))
(or (not x539) x14 x41)
(or x539 (not x14) x41)
(or x539 x14 (not x41))
(or (not x539) (not x14) (not x41))
(or (not x585) x18 x87)
(or x585 (not x18) x87)
(or x585 x18 (not x87))
(or (not x585) (not x18) (not x87))
(or (not x953) x324 x325)
(or x953 (not x324) x325)
(or x953 x324 (not x325))
(or (not x953) (not x324) (not x325))
(or (not x821) x224 x247)
(or x821 (not x224) x247)
(or x821 x224 (not x247))
(or (not x821) (not x224) (not x247))
(or (not x460) x42)
(or (not x460) (not x42) x68)
(or x460 (not x42) (not x68) (not x69))
(or (not x460) (not x42) (not x68) x69)
(or (not x499) x37 x64)
(or x499 (not x37) x64)
(or x499 x37 (not x64))
(or (not x499) (not x37) (not x64))
(or (not x923) x916 x917)
(or x923 (not x916) x917)
(or x923 x916 (not x917))
(or (not x923) (not x916) (not x917))
(or (not x470) x66)
(or (not x470) (not x66) x67)
(or x470 (not x66) (not x67) (not x68))
(or (not x470) (not x66) (not x67) x68)
(or (not x219) x55)
(or (not x219) (not x55) x56)
(or x219 (not x55) (not x56))
(or (not x876) x551 x873)
(or x876 (not x551) x873)
(or x876 x551 (not x873))
(or (not x876) (not x551) (not x873))
(or (not x1177) x286 x317)
(or x1177 (not x286) x317)
(or x1177 x286 (not x317))
(or (not x1177) (not x286) (not x317))
(or (not x1091) x59 x68)
(or x1091 (not x59) x68)
(or x1091 x59 (not x68))
(or (not x1091) (not x59) (not x68))
(or (not x1334) x470 x471)
(or x1334 (not x470) x471)
(or x1334 x470 (not x471))
(or (not x1334) (not x470) (not x471))
(or (not x1148) x407 x408)
(or x1148 (not x407) x408)
(or x1148 x407 (not x408))
(or (not x1148) (not x407) (not x408))
(or (not x823) x818 x819)
(or x823 (not x818) x819)
(or x823 x818 (not x819))
(or (not x823) (not x818) (not x819))
(or (not x1349) x1332 x1333)
(or x1349 (not x1332) x1333)
(or x1349 x1332 (not x1333))
(or (not x1349) (not x1332) (not x1333))
(or (not x988) x343 x344)
(or x988 (not x343) x344)
(or x988 x343 (not x344))
(or (not x988) (not x343) (not x344))
(or (not x561) x3 x30)
(or x561 (not x3) x30)
(or x561 x3 (not x30))
(or (not x561) (not x3) (not x30))
(or (not x748) x120 x225)
(or x748 (not x120) x225)
(or x748 x120 (not x225))
(or (not x748) (not x120) (not x225))
(or (not x951) x946 x947)
(or x951 (not x946) x947)
(or x951 x946 (not x947))
(or (not x951) (not x946) (not x947))
(or (not x1143) x411 x1135)
(or x1143 (not x411) x1135)
(or x1143 x411 (not x1135))
(or (not x1143) (not x411) (not x1135))
(or (not x1340) x1328 x1329)
(or x1340 (not x1328) x1329)
(or x1340 x1328 (not x1329))
(or (not x1340) (not x1328) (not x1329))
(or (not x1363) x688 x1361)
(or x1363 (not x688) x1361)
(or x1363 x688 (not x1361))
(or (not x1363) (not x688) (not x1361))
(or (not x1069) x1066 x1067)
(or x1069 (not x1066) x1067)
(or x1069 x1066 (not x1067))
(or (not x1069) (not x1066) (not x1067))
(or (not x667) x221 x222)
(or x667 (not x221) x222)
(or x667 x221 (not x222))
(or (not x667) (not x221) (not x222))
(or (not x1028) x63 x72)
(or x1028 (not x63) x72)
(or x1028 x63 (not x72))
(or (not x1028) (not x63) (not x72))
(or (not x939) x181 x193)
(or x939 (not x181) x193)
(or x939 x181 (not x193))
(or (not x939) (not x181) (not x193))
(or (not x601) x10 x79)
(or x601 (not x10) x79)
(or x601 x10 (not x79))
(or (not x601) (not x10) (not x79))
(or (not x513) x27 x54)
(or x513 (not x27) x54)
(or x513 x27 (not x54))
(or (not x513) (not x27) (not x54))
(or (not x999) x997 x998)
(or x999 (not x997) x998)
(or x999 x997 (not x998))
(or (not x999) (not x997) (not x998))
(or (not x436) x46)
(or (not x436) (not x46) x72)
(or x436 (not x46) (not x72) (not x73))
(or (not x436) (not x46) (not x72) x73)
(or (not x1197) x1195 x1196)
(or x1197 (not x1195) x1196)
(or x1197 x1195 (not x1196))
(or (not x1197) (not x1195) (not x1196))
(or (not x718) x126 x213)
(or x718 (not x126) x213)
(or x718 x126 (not x213))
(or (not x718) (not x126) (not x213))
(or (not x382) x55)
(or (not x382) (not x55) x83)
(or x382 (not x55) (not x83))
(or (not x1384) x1372 x1373)
(or x1384 (not x1372) x1373)
(or x1384 x1372 (not x1373))
(or (not x1384) (not x1372) (not x1373))
(or (not x571) x25 x67)
(or x571 (not x25) x67)
(or x571 x25 (not x67))
(or (not x571) (not x25) (not x67))
(or (not x725) x110 x122)
(or x725 (not x110) x122)
(or x725 x110 (not x122))
(or (not x725) (not x110) (not x122))
(or (not x1252) x44 x45)
(or x1252 (not x44) x45)
(or x1252 x44 (not x45))
(or (not x1252) (not x44) (not x45))
(or (not x1038) x20 x44)
(or x1038 (not x20) x44)
(or x1038 x20 (not x44))
(or (not x1038) (not x20) (not x44))
(or (not x793) x216 x239)
(or x793 (not x216) x239)
(or x793 x216 (not x239))
(or (not x793) (not x216) (not x239))
(or (not x1194) x206 x209)
(or x1194 (not x206) x209)
(or x1194 x206 (not x209))
(or (not x1194) (not x206) (not x209))
(or (not x401) x52)
(or (not x401) (not x52) x80)
(or x401 (not x52) (not x80))
(or (not x387) x1)
(or (not x387) (not x1) x69)
(or x387 (not x1) (not x69))
(or (not x644) x641 x642)
(or x644 (not x641) x642)
(or x644 x641 (not x642))
(or (not x644) (not x641) (not x642))
(or (not x462) x43)
(or (not x462) (not x43) x69)
(or x462 (not x43) (not x69))
(or (not x962) x960 x961)
(or x962 (not x960) x961)
(or x962 x960 (not x961))
(or (not x962) (not x960) (not x961))
(or (not x386) x80)
(or (not x386) (not x80) x81)
(or x386 (not x80) (not x81) (not x83))
(or (not x386) (not x80) (not x81) x83)
(or (not x1220) x1217 x1218)
(or x1220 (not x1217) x1218)
(or x1220 x1217 (not x1218))
(or (not x1220) (not x1217) (not x1218))
(or (not x1405) x37 x39)
(or x1405 (not x37) x39)
(or x1405 x37 (not x39))
(or (not x1405) (not x37) (not x39))
(or (not x373) x2)
(or (not x373) (not x2) x3)
(or x373 (not x2) (not x3))
(or (not x1219) x331 x430)
(or x1219 (not x331) x430)
(or x1219 x331 (not x430))
(or (not x1219) (not x331) (not x430))
(or (not x1319) x678 x1317)
(or x1319 (not x678) x1317)
(or x1319 x678 (not x1317))
(or (not x1319) (not x678) (not x1317))
(or (not x1196) x1191 x1192)
(or x1196 (not x1191) x1192)
(or x1196 x1191 (not x1192))
(or (not x1196) (not x1191) (not x1192))
(or (not x298) x97)
(or (not x298) (not x97) x98)
(or x298 (not x97) (not x98))
(or (not x706) x704 x705)
(or x706 (not x704) x705)
(or x706 x704 (not x705))
(or (not x706) (not x704) (not x705))
(or (not x233) x48)
(or (not x233) (not x48) x49)
(or x233 (not x48) (not x49))
(or (not x640) x194 x209)
(or x640 (not x194) x209)
(or x640 x194 (not x209))
(or (not x640) (not x194) (not x209))
(or (not x620) x199 x619)
(or x620 (not x199) x619)
(or x620 x199 (not x619))
(or (not x620) (not x199) (not x619))
(or (not x256) x118)
(or (not x256) (not x118) x119)
(or x256 (not x118) (not x119))
(or (not x897) x557 x894)
(or x897 (not x557) x894)
(or x897 x557 (not x894))
(or (not x897) (not x557) (not x894))
(or (not x971) x969 x970)
(or x971 (not x969) x970)
(or x971 x969 (not x970))
(or (not x971) (not x969) (not x970))
(or (not x388) x54)
(or (not x388) (not x54) x80)
(or x388 (not x54) (not x80) (not x81))
(or (not x388) (not x54) (not x80) x81)
(or (not x528) x116 x131)
(or x528 (not x116) x131)
(or x528 x116 (not x131))
(or (not x528) (not x116) (not x131))
(or (not x319) x64)
(or (not x319) (not x64) x92)
(or x319 (not x64) (not x92))
(or (not x1218) x1215 x1216)
(or x1218 (not x1215) x1216)
(or x1218 x1215 (not x1216))
(or (not x1218) (not x1215) (not x1216))
(or (not x252) x120)
(or (not x252) (not x120) x121)
(or x252 (not x120) (not x121))
(or (not x737) x249 x250)
(or x737 (not x249) x250)
(or x737 x249 (not x250))
(or (not x737) (not x249) (not x250))
(or (not x612) x141 x181)
(or x612 (not x141) x181)
(or x612 x141 (not x181))
(or (not x612) (not x141) (not x181))
(or (not x1336) x1334 x1335)
(or x1336 (not x1334) x1335)
(or x1336 x1334 (not x1335))
(or (not x1336) (not x1334) (not x1335))
(or (not x742) x251 x252)
(or x742 (not x251) x252)
(or x742 x251 (not x252))
(or (not x742) (not x251) (not x252))
(or (not x1206) x61 x62)
(or x1206 (not x61) x62)
(or x1206 x61 (not x62))
(or (not x1206) (not x61) (not x62))
(or (not x978) x184 x196)
(or x978 (not x184) x196)
(or x978 x184 (not x196))
(or (not x978) (not x184) (not x196))
(or (not x509) x29 x56)
(or x509 (not x29) x56)
(or x509 x29 (not x56))
(or (not x509) (not x29) (not x56))
(or (not x1328) x4 x28)
(or x1328 (not x4) x28)
(or x1328 x4 (not x28))
(or (not x1328) (not x4) (not x28))
(or (not x1008) x352 x353)
(or x1008 (not x352) x353)
(or x1008 x352 (not x353))
(or (not x1008) (not x352) (not x353))
(or (not x929) x94 x121)
(or x929 (not x94) x121)
(or x929 x94 (not x121))
(or (not x929) (not x94) (not x121))
(or (not x1167) x1164 x1165)
(or x1167 (not x1164) x1165)
(or x1167 x1164 (not x1165))
(or (not x1167) (not x1164) (not x1165))
(or (not x1031) x1028 x1029)
(or x1031 (not x1028) x1029)
(or x1031 x1028 (not x1029))
(or (not x1031) (not x1028) (not x1029))
(or (not x869) x549 x866)
(or x869 (not x549) x866)
(or x869 x549 (not x866))
(or (not x869) (not x549) (not x866))
(or (not x237) x46)
(or (not x237) (not x46) x47)
(or x237 (not x46) (not x47))
(or (not x935) x933 x934)
(or x935 (not x933) x934)
(or x935 x933 (not x934))
(or (not x935) (not x933) (not x934))
(or (not x1400) x223 x229)
(or x1400 (not x223) x229)
(or x1400 x223 (not x229))
(or (not x1400) (not x223) (not x229))
(or (not x1385) x1380 x1381)
(or x1385 (not x1380) x1381)
(or x1385 x1380 (not x1381))
(or (not x1385) (not x1380) (not x1381))
(or (not x425) x48)
(or (not x425) (not x48) x76)
(or x425 (not x48) (not x76))
(or (not x268) x112)
(or (not x268) (not x112) x113)
(or x268 (not x112) (not x113))
(or (not x377) x57)
(or (not x377) (not x57) x81)
(or x377 (not x57) (not x81) (not x82))
(or (not x377) (not x57) (not x81) x82)
(or (not x1406) x253 x310)
(or x1406 (not x253) x310)
(or x1406 x253 (not x310))
(or (not x1406) (not x253) (not x310))
(or (not x1291) x459 x1285)
(or x1291 (not x459) x1285)
(or x1291 x459 (not x1285))
(or (not x1291) (not x459) (not x1285))
(or (not x697) x233 x234)
(or x697 (not x233) x234)
(or x697 x233 (not x234))
(or (not x697) (not x233) (not x234))
(or (not x780) x778 x779)
(or x780 (not x778) x779)
(or x780 x778 (not x779))
(or (not x780) (not x778) (not x779))
(or (not x1322) x1318 x1319)
(or x1322 (not x1318) x1319)
(or x1322 x1318 (not x1319))
(or (not x1322) (not x1318) (not x1319))
(or (not x186) x83)
(or (not x186) (not x83) x84)
(or x186 (not x83) (not x84))
(or (not x234) x129)
(or (not x234) (not x129) x130)
(or x234 (not x129) (not x130))
(or (not x232) x130)
(or (not x232) (not x130) x131)
(or x232 (not x130) (not x131))
(or (not x185) x84)
(or (not x185) (not x84) x85)
(or x185 (not x84) (not x85))
(or (not x732) x247 x248)
(or x732 (not x247) x248)
(or x732 x247 (not x248))
(or (not x732) (not x247) (not x248))
(or (not x1339) x302 x373)
(or x1339 (not x302) x373)
(or x1339 x302 (not x373))
(or (not x1339) (not x302) (not x373))
(or (not x733) x123 x219)
(or x733 (not x123) x219)
(or x733 x123 (not x219))
(or (not x733) (not x123) (not x219))
(or (not x1312) x366 x460)
(or x1312 (not x366) x460)
(or x1312 x366 (not x460))
(or (not x1312) (not x366) (not x460))
(or (not x555) x6 x33)
(or x555 (not x6) x33)
(or x555 x6 (not x33))
(or (not x555) (not x6) (not x33))
(or (not x218) x137)
(or (not x218) (not x137) x138)
(or x218 (not x137) (not x138))
(or (not x802) x797 x798)
(or x802 (not x797) x798)
(or x802 x797 (not x798))
(or (not x802) (not x797) (not x798))
(or (not x438) x47)
(or (not x438) (not x47) x73)
(or x438 (not x47) (not x73))
(or (not x318) x64)
(or (not x318) (not x64) x90)
(or x318 (not x64) (not x90) (not x91))
(or (not x318) (not x64) (not x90) x91)
(or (not x195) x74)
(or (not x195) (not x74) x75)
(or x195 (not x74) (not x75))
(or (not x786) x214 x237)
(or x786 (not x214) x237)
(or x786 x214 (not x237))
(or (not x786) (not x214) (not x237))
(or (not x937) x935 x936)
(or x937 (not x935) x936)
(or x937 x935 (not x936))
(or (not x937) (not x935) (not x936))
(or (not x1211) x46 x52)
(or x1211 (not x46) x52)
(or x1211 x46 (not x52))
(or (not x1211) (not x46) (not x52))
(or (not x662) x219 x220)
(or x662 (not x219) x220)
(or x662 x219 (not x220))
(or (not x662) (not x219) (not x220))
(or (not x794) x792 x793)
(or x794 (not x792) x793)
(or x794 x792 (not x793))
(or (not x794) (not x792) (not x793))
(or (not x202) x67)
(or (not x202) (not x67) x68)
(or x202 (not x67) (not x68))
(or (not x310) x65)
(or (not x310) (not x65) x91)
(or x310 (not x65) (not x91) (not x92))
(or (not x310) (not x65) (not x91) x92)
(or (not x753) x119 x227)
(or x753 (not x119) x227)
(or x753 x119 (not x227))
(or (not x753) (not x119) (not x227))
(or (not x424) x48)
(or (not x424) (not x48) x74)
(or x424 (not x48) (not x74) (not x75))
(or (not x424) (not x48) (not x74) x75)
(or (not x214) x139)
(or (not x214) (not x139) x140)
(or x214 (not x139) (not x140))
(or (not x565) x1 x28)
(or x565 (not x1) x28)
(or x565 x1 (not x28))
(or (not x565) (not x1) (not x28))
(or (not x1376) x306 x307)
(or x1376 (not x306) x307)
(or x1376 x306 (not x307))
(or (not x1376) (not x306) (not x307))
))