;;; 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/UNSAT/45/instance_1444.cnf

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