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