1 files changed, 0 insertions, 6593 deletions

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