NOT T19,R1315;
NOT T18,T19;
NOT T17,T18;
NOT T16,T17;
NOT T15,T16;
NOT T14,T15;
NOT T13,T14;
NOT T12,T13;
NOT T11,T12;
NOT T20,T12;
AND T10,T11,T20;
NOT T23,T13;
NOT T22,T23;
NOT T24,T23;
AND T21,T22,T24;
OR T9,T10,T21;
NOT T29,T14;
NOT T28,T29;
NOT T27,T28;
NOT T30,T28;
AND T26,T27,T30;
NOT T33,T29;
NOT T32,T33;
NOT T34,T33;
AND T31,T32,T34;
AND T25,T26,T31;
AND T8,T9,T25;
NOT T41,T15;
NOT T40,T41;
NOT T39,T40;
NOT T38,T39;
NOT T42,T39;
OR T37,T38,T42;
NOT T45,T40;
NOT T44,T45;
NOT T46,T45;
AND T43,T44,T46;
AND T36,T37,T43;
NOT T51,T41;
NOT T50,T51;
NOT T49,T50;
NOT T52,T50;
AND T48,T49,T52;
NOT T55,T51;
NOT T54,T55;
NOT T56,T55;
AND T53,T54,T56;
OR T47,T48,T53;
AND T35,T36,T47;
OR T7,T8,T35;
NOT T65,T16;
NOT T64,T65;
NOT T63,T64;
NOT T62,T63;
NOT T61,T62;
NOT T66,T62;
OR T60,T61,T66;
NOT T69,T63;
NOT T68,T69;
NOT T70,T69;
OR T67,T68,T70;
OR T59,T60,T67;
NOT T75,T64;
NOT T74,T75;
NOT T73,T74;
NOT T76,T74;
AND T72,T73,T76;
NOT T79,T75;
NOT T78,T79;
NOT T80,T79;
AND T77,T78,T80;
OR T71,T72,T77;
AND T58,T59,T71;
NOT T87,T65;
NOT T86,T87;
NOT T85,T86;
NOT T84,T85;
NOT T88,T85;
OR T83,T84,T88;
NOT T91,T86;
NOT T90,T91;
NOT T92,T91;
OR T89,T90,T92;
AND T82,T83,T89;
NOT T97,T87;
NOT T96,T97;
NOT T95,T96;
NOT T98,T96;
AND T94,T95,T98;
NOT T101,T97;
NOT T100,T101;
NOT T102,T101;
OR T99,T100,T102;
AND T93,T94,T99;
OR T81,T82,T93;
OR T57,T58,T81;
OR T6,T7,T57;
NOT T113,T17;
NOT T112,T113;
NOT T111,T112;
NOT T110,T111;
NOT T109,T110;
NOT T108,T109;
NOT T114,T109;
AND T107,T108,T114;
NOT T117,T110;
NOT T116,T117;
NOT T118,T117;
AND T115,T116,T118;
AND T106,T107,T115;
NOT T123,T111;
NOT T122,T123;
NOT T121,T122;
NOT T124,T122;
OR T120,T121,T124;
NOT T127,T123;
NOT T126,T127;
NOT T128,T127;
OR T125,T126,T128;
AND T119,T120,T125;
AND T105,T106,T119;
NOT T135,T112;
NOT T134,T135;
NOT T133,T134;
NOT T132,T133;
NOT T136,T133;
OR T131,T132,T136;
NOT T139,T134;
NOT T138,T139;
NOT T140,T139;
AND T137,T138,T140;
OR T130,T131,T137;
NOT T145,T135;
NOT T144,T145;
NOT T143,T144;
NOT T146,T144;
OR T142,T143,T146;
NOT T149,T145;
NOT T148,T149;
NOT T150,T149;
AND T147,T148,T150;
AND T141,T142,T147;
OR T129,T130,T141;
AND T104,T105,T129;
NOT T159,T113;
NOT T158,T159;
NOT T157,T158;
NOT T156,T157;
NOT T155,T156;
NOT T160,T156;
OR T154,T155,T160;
NOT T163,T157;
NOT T162,T163;
NOT T164,T163;
OR T161,T162,T164;
AND T153,T154,T161;
NOT T169,T158;
NOT T168,T169;
NOT T167,T168;
NOT T170,T168;
OR T166,T167,T170;
NOT T173,T169;
NOT T172,T173;
NOT T174,T173;
OR T171,T172,T174;
OR T165,T166,T171;
OR T152,T153,T165;
NOT T181,T159;
NOT T180,T181;
NOT T179,T180;
NOT T178,T179;
NOT T182,T179;
AND T177,T178,T182;
NOT T185,T180;
NOT T184,T185;
NOT T186,T185;
OR T183,T184,T186;
AND T176,T177,T183;
NOT T191,T181;
NOT T190,T191;
NOT T189,T190;
NOT T192,T190;
AND T188,T189,T192;
NOT T195,T191;
NOT T194,T195;
NOT T196,T195;
OR T193,T194,T196;
OR T187,T188,T193;
OR T175,T176,T187;
OR T151,T152,T175;
AND T103,T104,T151;
AND T5,T6,T103;
NOT T209,T18;
NOT T208,T209;
NOT T207,T208;
NOT T206,T207;
NOT T205,T206;
NOT T204,T205;
NOT T203,T204;
NOT T210,T204;
AND T202,T203,T210;
NOT T213,T205;
NOT T212,T213;
NOT T214,T213;
OR T211,T212,T214;
OR T201,T202,T211;
NOT T219,T206;
NOT T218,T219;
NOT T217,T218;
NOT T220,T218;
AND T216,T217,T220;
NOT T223,T219;
NOT T222,T223;
NOT T224,T223;
OR T221,T222,T224;
OR T215,T216,T221;
AND T200,T201,T215;
NOT T231,T207;
NOT T230,T231;
NOT T229,T230;
NOT T228,T229;
NOT T232,T229;
AND T227,T228,T232;
NOT T235,T230;
NOT T234,T235;
NOT T236,T235;
OR T233,T234,T236;
OR T226,T227,T233;
NOT T241,T231;
NOT T240,T241;
NOT T239,T240;
NOT T242,T240;
AND T238,T239,T242;
NOT T245,T241;
NOT T244,T245;
NOT T246,T245;
AND T243,T244,T246;
OR T237,T238,T243;
AND T225,T226,T237;
AND T199,T200,T225;
NOT T255,T208;
NOT T254,T255;
NOT T253,T254;
NOT T252,T253;
NOT T251,T252;
NOT T256,T252;
OR T250,T251,T256;
NOT T259,T253;
NOT T258,T259;
NOT T260,T259;
OR T257,T258,T260;
OR T249,T250,T257;
NOT T265,T254;
NOT T264,T265;
NOT T263,T264;
NOT T266,T264;
AND T262,T263,T266;
NOT T269,T265;
NOT T268,T269;
NOT T270,T269;
OR T267,T268,T270;
AND T261,T262,T267;
AND T248,T249,T261;
NOT T277,T255;
NOT T276,T277;
NOT T275,T276;
NOT T274,T275;
NOT T278,T275;
AND T273,T274,T278;
NOT T281,T276;
NOT T280,T281;
NOT T282,T281;
OR T279,T280,T282;
AND T272,T273,T279;
NOT T287,T277;
NOT T286,T287;
NOT T285,T286;
NOT T288,T286;
OR T284,T285,T288;
NOT T291,T287;
NOT T290,T291;
NOT T292,T291;
OR T289,T290,T292;
AND T283,T284,T289;
OR T271,T272,T283;
AND T247,T248,T271;
OR T198,T199,T247;
NOT T303,T209;
NOT T302,T303;
NOT T301,T302;
NOT T300,T301;
NOT T299,T300;
NOT T298,T299;
NOT T304,T299;
OR T297,T298,T304;
NOT T307,T300;
NOT T306,T307;
NOT T308,T307;
AND T305,T306,T308;
AND T296,T297,T305;
NOT T313,T301;
NOT T312,T313;
NOT T311,T312;
NOT T314,T312;
OR T310,T311,T314;
NOT T317,T313;
NOT T316,T317;
NOT T318,T317;
OR T315,T316,T318;
AND T309,T310,T315;
AND T295,T296,T309;
NOT T325,T302;
NOT T324,T325;
NOT T323,T324;
NOT T322,T323;
NOT T326,T323;
AND T321,T322,T326;
NOT T329,T324;
NOT T328,T329;
NOT T330,T329;
AND T327,T328,T330;
OR T320,T321,T327;
NOT T335,T325;
NOT T334,T335;
NOT T333,T334;
NOT T336,T334;
OR T332,T333,T336;
NOT T339,T335;
NOT T338,T339;
NOT T340,T339;
AND T337,T338,T340;
AND T331,T332,T337;
OR T319,T320,T331;
OR T294,T295,T319;
NOT T349,T303;
NOT T348,T349;
NOT T347,T348;
NOT T346,T347;
NOT T345,T346;
NOT T350,T346;
OR T344,T345,T350;
NOT T353,T347;
NOT T352,T353;
NOT T354,T353;
AND T351,T352,T354;
OR T343,T344,T351;
NOT T359,T348;
NOT T358,T359;
NOT T357,T358;
NOT T360,T358;
AND T356,T357,T360;
NOT T363,T359;
NOT T362,T363;
NOT T364,T363;
AND T361,T362,T364;
AND T355,T356,T361;
OR T342,T343,T355;
NOT T371,T349;
NOT T370,T371;
NOT T369,T370;
NOT T368,T369;
NOT T372,T369;
AND T367,T368,T372;
NOT T375,T370;
NOT T374,T375;
NOT T376,T375;
OR T373,T374,T376;
OR T366,T367,T373;
NOT T381,T371;
NOT T380,T381;
NOT T379,T380;
NOT T382,T380;
OR T378,T379,T382;
NOT T385,T381;
NOT T384,T385;
NOT T386,T385;
AND T383,T384,T386;
AND T377,T378,T383;
AND T365,T366,T377;
OR T341,T342,T365;
OR T293,T294,T341;
OR T197,T198,T293;
AND T4,T5,T197;
NOT T401,T19;
NOT T400,T401;
NOT T399,T400;
NOT T398,T399;
NOT T397,T398;
NOT T396,T397;
NOT T395,T396;
NOT T394,T395;
NOT T402,T395;
OR T393,T394,T402;
NOT T405,T396;
NOT T404,T405;
NOT T406,T405;
OR T403,T404,T406;
AND T392,T393,T403;
NOT T411,T397;
NOT T410,T411;
NOT T409,T410;
NOT T412,T410;
OR T408,T409,T412;
NOT T415,T411;
NOT T414,T415;
NOT T416,T415;
AND T413,T414,T416;
AND T407,T408,T413;
AND T391,T392,T407;
NOT T423,T398;
NOT T422,T423;
NOT T421,T422;
NOT T420,T421;
NOT T424,T421;
OR T419,T420,T424;
NOT T427,T422;
NOT T426,T427;
NOT T428,T427;
AND T425,T426,T428;
AND T418,T419,T425;
NOT T433,T423;
NOT T432,T433;
NOT T431,T432;
NOT T434,T432;
AND T430,T431,T434;
NOT T437,T433;
NOT T436,T437;
NOT T438,T437;
OR T435,T436,T438;
AND T429,T430,T435;
OR T417,T418,T429;
OR T390,T391,T417;
NOT T447,T399;
NOT T446,T447;
NOT T445,T446;
NOT T444,T445;
NOT T443,T444;
NOT T448,T444;
AND T442,T443,T448;
NOT T451,T445;
NOT T450,T451;
NOT T452,T451;
OR T449,T450,T452;
AND T441,T442,T449;
NOT T457,T446;
NOT T456,T457;
NOT T455,T456;
NOT T458,T456;
AND T454,T455,T458;
NOT T461,T457;
NOT T460,T461;
NOT T462,T461;
OR T459,T460,T462;
AND T453,T454,T459;
OR T440,T441,T453;
NOT T469,T447;
NOT T468,T469;
NOT T467,T468;
NOT T466,T467;
NOT T470,T467;
OR T465,T466,T470;
NOT T473,T468;
NOT T472,T473;
NOT T474,T473;
AND T471,T472,T474;
AND T464,T465,T471;
NOT T479,T469;
NOT T478,T479;
NOT T477,T478;
NOT T480,T478;
OR T476,T477,T480;
NOT T483,T479;
NOT T482,T483;
NOT T484,T483;
AND T481,T482,T484;
OR T475,T476,T481;
OR T463,T464,T475;
AND T439,T440,T463;
AND T389,T390,T439;
NOT T495,T400;
NOT T494,T495;
NOT T493,T494;
NOT T492,T493;
NOT T491,T492;
NOT T490,T491;
NOT T496,T491;
OR T489,T490,T496;
NOT T499,T492;
NOT T498,T499;
NOT T500,T499;
OR T497,T498,T500;
AND T488,T489,T497;
NOT T505,T493;
NOT T504,T505;
NOT T503,T504;
NOT T506,T504;
AND T502,T503,T506;
NOT T509,T505;
NOT T508,T509;
NOT T510,T509;
OR T507,T508,T510;
OR T501,T502,T507;
AND T487,T488,T501;
NOT T517,T494;
NOT T516,T517;
NOT T515,T516;
NOT T514,T515;
NOT T518,T515;
AND T513,T514,T518;
NOT T521,T516;
NOT T520,T521;
NOT T522,T521;
AND T519,T520,T522;
OR T512,T513,T519;
NOT T527,T517;
NOT T526,T527;
NOT T525,T526;
NOT T528,T526;
AND T524,T525,T528;
NOT T531,T527;
NOT T530,T531;
NOT T532,T531;
AND T529,T530,T532;
OR T523,T524,T529;
OR T511,T512,T523;
AND T486,T487,T511;
NOT T541,T495;
NOT T540,T541;
NOT T539,T540;
NOT T538,T539;
NOT T537,T538;
NOT T542,T538;
OR T536,T537,T542;
NOT T545,T539;
NOT T544,T545;
NOT T546,T545;
OR T543,T544,T546;
AND T535,T536,T543;
NOT T551,T540;
NOT T550,T551;
NOT T549,T550;
NOT T552,T550;
AND T548,T549,T552;
NOT T555,T551;
NOT T554,T555;
NOT T556,T555;
OR T553,T554,T556;
AND T547,T548,T553;
AND T534,T535,T547;
NOT T563,T541;
NOT T562,T563;
NOT T561,T562;
NOT T560,T561;
NOT T564,T561;
AND T559,T560,T564;
NOT T567,T562;
NOT T566,T567;
NOT T568,T567;
AND T565,T566,T568;
AND T558,T559,T565;
NOT T573,T563;
NOT T572,T573;
NOT T571,T572;
NOT T574,T572;
AND T570,T571,T574;
NOT T577,T573;
NOT T576,T577;
NOT T578,T577;
OR T575,T576,T578;
OR T569,T570,T575;
AND T557,T558,T569;
OR T533,T534,T557;
OR T485,T486,T533;
OR T388,T389,T485;
NOT T591,T401;
NOT T590,T591;
NOT T589,T590;
NOT T588,T589;
NOT T587,T588;
NOT T586,T587;
NOT T585,T586;
NOT T592,T586;
AND T584,T585,T592;
NOT T595,T587;
NOT T594,T595;
NOT T596,T595;
AND T593,T594,T596;
OR T583,T584,T593;
NOT T601,T588;
NOT T600,T601;
NOT T599,T600;
NOT T602,T600;
OR T598,T599,T602;
NOT T605,T601;
NOT T604,T605;
NOT T606,T605;
AND T603,T604,T606;
OR T597,T598,T603;
OR T582,T583,T597;
NOT T613,T589;
NOT T612,T613;
NOT T611,T612;
NOT T610,T611;
NOT T614,T611;
OR T609,T610,T614;
NOT T617,T612;
NOT T616,T617;
NOT T618,T617;
OR T615,T616,T618;
OR T608,T609,T615;
NOT T623,T613;
NOT T622,T623;
NOT T621,T622;
NOT T624,T622;
OR T620,T621,T624;
NOT T627,T623;
NOT T626,T627;
NOT T628,T627;
OR T625,T626,T628;
AND T619,T620,T625;
AND T607,T608,T619;
AND T581,T582,T607;
NOT T637,T590;
NOT T636,T637;
NOT T635,T636;
NOT T634,T635;
NOT T633,T634;
NOT T638,T634;
OR T632,T633,T638;
NOT T641,T635;
NOT T640,T641;
NOT T642,T641;
OR T639,T640,T642;
AND T631,T632,T639;
NOT T647,T636;
NOT T646,T647;
NOT T645,T646;
NOT T648,T646;
OR T644,T645,T648;
NOT T651,T647;
NOT T650,T651;
NOT T652,T651;
AND T649,T650,T652;
AND T643,T644,T649;
OR T630,T631,T643;
NOT T659,T637;
NOT T658,T659;
NOT T657,T658;
NOT T656,T657;
NOT T660,T657;
AND T655,T656,T660;
NOT T663,T658;
NOT T662,T663;
NOT T664,T663;
OR T661,T662,T664;
OR T654,T655,T661;
NOT T669,T659;
NOT T668,T669;
NOT T667,T668;
NOT T670,T668;
AND T666,T667,T670;
NOT T673,T669;
NOT T672,T673;
NOT T674,T673;
OR T671,T672,T674;
AND T665,T666,T671;
OR T653,T654,T665;
OR T629,T630,T653;
AND T580,T581,T629;
NOT T685,T591;
NOT T684,T685;
NOT T683,T684;
NOT T682,T683;
NOT T681,T682;
NOT T680,T681;
NOT T686,T681;
AND T679,T680,T686;
NOT T689,T682;
NOT T688,T689;
NOT T690,T689;
OR T687,T688,T690;
AND T678,T679,T687;
NOT T695,T683;
NOT T694,T695;
NOT T693,T694;
NOT T696,T694;
OR T692,T693,T696;
NOT T699,T695;
NOT T698,T699;
NOT T700,T699;
OR T697,T698,T700;
AND T691,T692,T697;
AND T677,T678,T691;
NOT T707,T684;
NOT T706,T707;
NOT T705,T706;
NOT T704,T705;
NOT T708,T705;
AND T703,T704,T708;
NOT T711,T706;
NOT T710,T711;
NOT T712,T711;
OR T709,T710,T712;
OR T702,T703,T709;
NOT T717,T707;
NOT T716,T717;
NOT T715,T716;
NOT T718,T716;
AND T714,T715,T718;
NOT T721,T717;
NOT T720,T721;
NOT T722,T721;
OR T719,T720,T722;
AND T713,T714,T719;
AND T701,T702,T713;
OR T676,T677,T701;
NOT T731,T685;
NOT T730,T731;
NOT T729,T730;
NOT T728,T729;
NOT T727,T728;
NOT T732,T728;
OR T726,T727,T732;
NOT T735,T729;
NOT T734,T735;
NOT T736,T735;
OR T733,T734,T736;
OR T725,T726,T733;
NOT T741,T730;
NOT T740,T741;
NOT T739,T740;
NOT T742,T740;
AND T738,T739,T742;
NOT T745,T741;
NOT T744,T745;
NOT T746,T745;
OR T743,T744,T746;
OR T737,T738,T743;
OR T724,T725,T737;
NOT T753,T731;
NOT T752,T753;
NOT T751,T752;
NOT T750,T751;
NOT T754,T751;
AND T749,T750,T754;
NOT T757,T752;
NOT T756,T757;
NOT T758,T757;
AND T755,T756,T758;
OR T748,T749,T755;
NOT T763,T753;
NOT T762,T763;
NOT T761,T762;
NOT T764,T762;
OR T760,T761,T764;
NOT T767,T763;
NOT T766,T767;
NOT T768,T767;
AND T765,T766,T768;
OR T759,T760,T765;
AND T747,T748,T759;
OR T723,T724,T747;
AND T675,T676,T723;
AND T579,T580,T675;
OR T387,T388,T579;
AND T3,T4,T387;
NOT T785,R1315;
NOT T784,T785;
NOT T783,T784;
NOT T782,T783;
NOT T781,T782;
NOT T780,T781;
NOT T779,T780;
NOT T778,T779;
NOT T777,T778;
NOT T786,T778;
AND T776,T777,T786;
NOT T789,T779;
NOT T788,T789;
NOT T790,T789;
OR T787,T788,T790;
AND T775,T776,T787;
NOT T795,T780;
NOT T794,T795;
NOT T793,T794;
NOT T796,T794;
OR T792,T793,T796;
NOT T799,T795;
NOT T798,T799;
NOT T800,T799;
OR T797,T798,T800;
OR T791,T792,T797;
OR T774,T775,T791;
NOT T807,T781;
NOT T806,T807;
NOT T805,T806;
NOT T804,T805;
NOT T808,T805;
AND T803,T804,T808;
NOT T811,T806;
NOT T810,T811;
NOT T812,T811;
AND T809,T810,T812;
OR T802,T803,T809;
NOT T817,T807;
NOT T816,T817;
NOT T815,T816;
NOT T818,T816;
AND T814,T815,T818;
NOT T821,T817;
NOT T820,T821;
NOT T822,T821;
OR T819,T820,T822;
AND T813,T814,T819;
OR T801,T802,T813;
OR T773,T774,T801;
NOT T831,T782;
NOT T830,T831;
NOT T829,T830;
NOT T828,T829;
NOT T827,T828;
NOT T832,T828;
OR T826,T827,T832;
NOT T835,T829;
NOT T834,T835;
NOT T836,T835;
OR T833,T834,T836;
AND T825,T826,T833;
NOT T841,T830;
NOT T840,T841;
NOT T839,T840;
NOT T842,T840;
AND T838,T839,T842;
NOT T845,T841;
NOT T844,T845;
NOT T846,T845;
OR T843,T844,T846;
AND T837,T838,T843;
OR T824,T825,T837;
NOT T853,T831;
NOT T852,T853;
NOT T851,T852;
NOT T850,T851;
NOT T854,T851;
OR T849,T850,T854;
NOT T857,T852;
NOT T856,T857;
NOT T858,T857;
OR T855,T856,T858;
OR T848,T849,T855;
NOT T863,T853;
NOT T862,T863;
NOT T861,T862;
NOT T864,T862;
AND T860,T861,T864;
NOT T867,T863;
NOT T866,T867;
NOT T868,T867;
AND T865,T866,T868;
OR T859,T860,T865;
AND T847,T848,T859;
OR T823,T824,T847;
AND T772,T773,T823;
NOT T879,T783;
NOT T878,T879;
NOT T877,T878;
NOT T876,T877;
NOT T875,T876;
NOT T874,T875;
NOT T880,T875;
AND T873,T874,T880;
NOT T883,T876;
NOT T882,T883;
NOT T884,T883;
AND T881,T882,T884;
OR T872,T873,T881;
NOT T889,T877;
NOT T888,T889;
NOT T887,T888;
NOT T890,T888;
AND T886,T887,T890;
NOT T893,T889;
NOT T892,T893;
NOT T894,T893;
AND T891,T892,T894;
AND T885,T886,T891;
OR T871,T872,T885;
NOT T901,T878;
NOT T900,T901;
NOT T899,T900;
NOT T898,T899;
NOT T902,T899;
OR T897,T898,T902;
NOT T905,T900;
NOT T904,T905;
NOT T906,T905;
AND T903,T904,T906;
OR T896,T897,T903;
NOT T911,T901;
NOT T910,T911;
NOT T909,T910;
NOT T912,T910;
OR T908,T909,T912;
NOT T915,T911;
NOT T914,T915;
NOT T916,T915;
OR T913,T914,T916;
OR T907,T908,T913;
OR T895,T896,T907;
AND T870,T871,T895;
NOT T925,T879;
NOT T924,T925;
NOT T923,T924;
NOT T922,T923;
NOT T921,T922;
NOT T926,T922;
AND T920,T921,T926;
NOT T929,T923;
NOT T928,T929;
NOT T930,T929;
AND T927,T928,T930;
AND T919,T920,T927;
NOT T935,T924;
NOT T934,T935;
NOT T933,T934;
NOT T936,T934;
AND T932,T933,T936;
NOT T939,T935;
NOT T938,T939;
NOT T940,T939;
AND T937,T938,T940;
AND T931,T932,T937;
AND T918,T919,T931;
NOT T947,T925;
NOT T946,T947;
NOT T945,T946;
NOT T944,T945;
NOT T948,T945;
AND T943,T944,T948;
NOT T951,T946;
NOT T950,T951;
NOT T952,T951;
AND T949,T950,T952;
AND T942,T943,T949;
NOT T957,T947;
NOT T956,T957;
NOT T955,T956;
NOT T958,T956;
AND T954,T955,T958;
NOT T961,T957;
NOT T960,T961;
NOT T962,T961;
OR T959,T960,T962;
OR T953,T954,T959;
OR T941,T942,T953;
OR T917,T918,T941;
OR T869,T870,T917;
OR T771,T772,T869;
NOT T975,T784;
NOT T974,T975;
NOT T973,T974;
NOT T972,T973;
NOT T971,T972;
NOT T970,T971;
NOT T969,T970;
NOT T976,T970;
OR T968,T969,T976;
NOT T979,T971;
NOT T978,T979;
NOT T980,T979;
AND T977,T978,T980;
AND T967,T968,T977;
NOT T985,T972;
NOT T984,T985;
NOT T983,T984;
NOT T986,T984;
AND T982,T983,T986;
NOT T989,T985;
NOT T988,T989;
NOT T990,T989;
OR T987,T988,T990;
OR T981,T982,T987;
AND T966,T967,T981;
NOT T997,T973;
NOT T996,T997;
NOT T995,T996;
NOT T994,T995;
NOT T998,T995;
OR T993,T994,T998;
NOT T1001,T996;
NOT T1000,T1001;
NOT T1002,T1001;
AND T999,T1000,T1002;
OR T992,T993,T999;
NOT T1007,T997;
NOT T1006,T1007;
NOT T1005,T1006;
NOT T1008,T1006;
OR T1004,T1005,T1008;
NOT T1011,T1007;
NOT T1010,T1011;
NOT T1012,T1011;
OR T1009,T1010,T1012;
OR T1003,T1004,T1009;
AND T991,T992,T1003;
AND T965,T966,T991;
NOT T1021,T974;
NOT T1020,T1021;
NOT T1019,T1020;
NOT T1018,T1019;
NOT T1017,T1018;
NOT T1022,T1018;
AND T1016,T1017,T1022;
NOT T1025,T1019;
NOT T1024,T1025;
NOT T1026,T1025;
OR T1023,T1024,T1026;
OR T1015,T1016,T1023;
NOT T1031,T1020;
NOT T1030,T1031;
NOT T1029,T1030;
NOT T1032,T1030;
AND T1028,T1029,T1032;
NOT T1035,T1031;
NOT T1034,T1035;
NOT T1036,T1035;
AND T1033,T1034,T1036;
OR T1027,T1028,T1033;
AND T1014,T1015,T1027;
NOT T1043,T1021;
NOT T1042,T1043;
NOT T1041,T1042;
NOT T1040,T1041;
NOT T1044,T1041;
AND T1039,T1040,T1044;
NOT T1047,T1042;
NOT T1046,T1047;
NOT T1048,T1047;
OR T1045,T1046,T1048;
AND T1038,T1039,T1045;
NOT T1053,T1043;
NOT T1052,T1053;
NOT T1051,T1052;
NOT T1054,T1052;
AND T1050,T1051,T1054;
NOT T1057,T1053;
NOT T1056,T1057;
NOT T1058,T1057;
OR T1055,T1056,T1058;
AND T1049,T1050,T1055;
AND T1037,T1038,T1049;
AND T1013,T1014,T1037;
OR T964,T965,T1013;
NOT T1069,T975;
NOT T1068,T1069;
NOT T1067,T1068;
NOT T1066,T1067;
NOT T1065,T1066;
NOT T1064,T1065;
NOT T1070,T1065;
AND T1063,T1064,T1070;
NOT T1073,T1066;
NOT T1072,T1073;
NOT T1074,T1073;
OR T1071,T1072,T1074;
OR T1062,T1063,T1071;
NOT T1079,T1067;
NOT T1078,T1079;
NOT T1077,T1078;
NOT T1080,T1078;
OR T1076,T1077,T1080;
NOT T1083,T1079;
NOT T1082,T1083;
NOT T1084,T1083;
OR T1081,T1082,T1084;
AND T1075,T1076,T1081;
AND T1061,T1062,T1075;
NOT T1091,T1068;
NOT T1090,T1091;
NOT T1089,T1090;
NOT T1088,T1089;
NOT T1092,T1089;
OR T1087,T1088,T1092;
NOT T1095,T1090;
NOT T1094,T1095;
NOT T1096,T1095;
OR T1093,T1094,T1096;
OR T1086,T1087,T1093;
NOT T1101,T1091;
NOT T1100,T1101;
NOT T1099,T1100;
NOT T1102,T1100;
AND T1098,T1099,T1102;
NOT T1105,T1101;
NOT T1104,T1105;
NOT T1106,T1105;
AND T1103,T1104,T1106;
OR T1097,T1098,T1103;
AND T1085,T1086,T1097;
AND T1060,T1061,T1085;
NOT T1115,T1069;
NOT T1114,T1115;
NOT T1113,T1114;
NOT T1112,T1113;
NOT T1111,T1112;
NOT T1116,T1112;
AND T1110,T1111,T1116;
NOT T1119,T1113;
NOT T1118,T1119;
NOT T1120,T1119;
AND T1117,T1118,T1120;
AND T1109,T1110,T1117;
NOT T1125,T1114;
NOT T1124,T1125;
NOT T1123,T1124;
NOT T1126,T1124;
OR T1122,T1123,T1126;
NOT T1129,T1125;
NOT T1128,T1129;
NOT T1130,T1129;
AND T1127,T1128,T1130;
AND T1121,T1122,T1127;
OR T1108,T1109,T1121;
NOT T1137,T1115;
NOT T1136,T1137;
NOT T1135,T1136;
NOT T1134,T1135;
NOT T1138,T1135;
OR T1133,T1134,T1138;
NOT T1141,T1136;
NOT T1140,T1141;
NOT T1142,T1141;
AND T1139,T1140,T1142;
AND T1132,T1133,T1139;
NOT T1147,T1137;
NOT T1146,T1147;
NOT T1145,T1146;
NOT T1148,T1146;
AND T1144,T1145,T1148;
NOT T1151,T1147;
NOT T1150,T1151;
NOT T1152,T1151;
OR T1149,T1150,T1152;
AND T1143,T1144,T1149;
AND T1131,T1132,T1143;
AND T1107,T1108,T1131;
OR T1059,T1060,T1107;
AND T963,T964,T1059;
AND T770,T771,T963;
NOT T1167,T785;
NOT T1166,T1167;
NOT T1165,T1166;
NOT T1164,T1165;
NOT T1163,T1164;
NOT T1162,T1163;
NOT T1161,T1162;
NOT T1160,T1161;
NOT T1168,T1161;
AND T1159,T1160,T1168;
NOT T1171,T1162;
NOT T1170,T1171;
NOT T1172,T1171;
OR T1169,T1170,T1172;
OR T1158,T1159,T1169;
NOT T1177,T1163;
NOT T1176,T1177;
NOT T1175,T1176;
NOT T1178,T1176;
OR T1174,T1175,T1178;
NOT T1181,T1177;
NOT T1180,T1181;
NOT T1182,T1181;
OR T1179,T1180,T1182;
OR T1173,T1174,T1179;
AND T1157,T1158,T1173;
NOT T1189,T1164;
NOT T1188,T1189;
NOT T1187,T1188;
NOT T1186,T1187;
NOT T1190,T1187;
AND T1185,T1186,T1190;
NOT T1193,T1188;
NOT T1192,T1193;
NOT T1194,T1193;
AND T1191,T1192,T1194;
AND T1184,T1185,T1191;
NOT T1199,T1189;
NOT T1198,T1199;
NOT T1197,T1198;
NOT T1200,T1198;
OR T1196,T1197,T1200;
NOT T1203,T1199;
NOT T1202,T1203;
NOT T1204,T1203;
OR T1201,T1202,T1204;
OR T1195,T1196,T1201;
OR T1183,T1184,T1195;
OR T1156,T1157,T1183;
NOT T1213,T1165;
NOT T1212,T1213;
NOT T1211,T1212;
NOT T1210,T1211;
NOT T1209,T1210;
NOT T1214,T1210;
AND T1208,T1209,T1214;
NOT T1217,T1211;
NOT T1216,T1217;
NOT T1218,T1217;
OR T1215,T1216,T1218;
AND T1207,T1208,T1215;
NOT T1223,T1212;
NOT T1222,T1223;
NOT T1221,T1222;
NOT T1224,T1222;
AND T1220,T1221,T1224;
NOT T1227,T1223;
NOT T1226,T1227;
NOT T1228,T1227;
OR T1225,T1226,T1228;
AND T1219,T1220,T1225;
OR T1206,T1207,T1219;
NOT T1235,T1213;
NOT T1234,T1235;
NOT T1233,T1234;
NOT T1232,T1233;
NOT T1236,T1233;
OR T1231,T1232,T1236;
NOT T1239,T1234;
NOT T1238,T1239;
NOT T1240,T1239;
OR T1237,T1238,T1240;
OR T1230,T1231,T1237;
NOT T1245,T1235;
NOT T1244,T1245;
NOT T1243,T1244;
NOT T1246,T1244;
AND T1242,T1243,T1246;
NOT T1249,T1245;
NOT T1248,T1249;
NOT T1250,T1249;
OR T1247,T1248,T1250;
AND T1241,T1242,T1247;
AND T1229,T1230,T1241;
OR T1205,T1206,T1229;
OR T1155,T1156,T1205;
NOT T1261,T1166;
NOT T1260,T1261;
NOT T1259,T1260;
NOT T1258,T1259;
NOT T1257,T1258;
NOT T1256,T1257;
NOT T1262,T1257;
AND T1255,T1256,T1262;
NOT T1265,T1258;
NOT T1264,T1265;
NOT T1266,T1265;
AND T1263,T1264,T1266;
OR T1254,T1255,T1263;
NOT T1271,T1259;
NOT T1270,T1271;
NOT T1269,T1270;
NOT T1272,T1270;
AND T1268,T1269,T1272;
NOT T1275,T1271;
NOT T1274,T1275;
NOT T1276,T1275;
OR T1273,T1274,T1276;
OR T1267,T1268,T1273;
AND T1253,T1254,T1267;
NOT T1283,T1260;
NOT T1282,T1283;
NOT T1281,T1282;
NOT T1280,T1281;
NOT T1284,T1281;
AND T1279,T1280,T1284;
NOT T1287,T1282;
NOT T1286,T1287;
NOT T1288,T1287;
AND T1285,T1286,T1288;
AND T1278,T1279,T1285;
NOT T1293,T1283;
NOT T1292,T1293;
NOT T1291,T1292;
NOT T1294,T1292;
OR T1290,T1291,T1294;
NOT T1297,T1293;
NOT T1296,T1297;
NOT T1298,T1297;
OR T1295,T1296,T1298;
AND T1289,T1290,T1295;
AND T1277,T1278,T1289;
AND T1252,T1253,T1277;
NOT T1307,T1261;
NOT T1306,T1307;
NOT T1305,T1306;
NOT T1304,T1305;
NOT T1303,T1304;
NOT T1308,T1304;
OR T1302,T1303,T1308;
NOT T1311,T1305;
NOT T1310,T1311;
NOT T1312,T1311;
AND T1309,T1310,T1312;
OR T1301,T1302,T1309;
NOT T1317,T1306;
NOT T1316,T1317;
NOT T1315,T1316;
NOT T1318,T1316;
AND T1314,T1315,T1318;
NOT T1321,T1317;
NOT T1320,T1321;
NOT T1322,T1321;
AND T1319,T1320,T1322;
OR T1313,T1314,T1319;
AND T1300,T1301,T1313;
NOT T1329,T1307;
NOT T1328,T1329;
NOT T1327,T1328;
NOT T1326,T1327;
NOT T1330,T1327;
AND T1325,T1326,T1330;
NOT T1333,T1328;
NOT T1332,T1333;
NOT T1334,T1333;
OR T1331,T1332,T1334;
OR T1324,T1325,T1331;
NOT T1339,T1329;
NOT T1338,T1339;
NOT T1337,T1338;
NOT T1340,T1338;
OR T1336,T1337,T1340;
NOT T1343,T1339;
NOT T1342,T1343;
NOT T1344,T1343;
OR T1341,T1342,T1344;
AND T1335,T1336,T1341;
OR T1323,T1324,T1335;
OR T1299,T1300,T1323;
OR T1251,T1252,T1299;
OR T1154,T1155,T1251;
NOT T1357,T1167;
NOT T1356,T1357;
NOT T1355,T1356;
NOT T1354,T1355;
NOT T1353,T1354;
NOT T1352,T1353;
NOT T1351,T1352;
NOT T1358,T1352;
AND T1350,T1351,T1358;
NOT T1361,T1353;
NOT T1360,T1361;
NOT T1362,T1361;
OR T1359,T1360,T1362;
AND T1349,T1350,T1359;
NOT T1367,T1354;
NOT T1366,T1367;
NOT T1365,T1366;
NOT T1368,T1366;
AND T1364,T1365,T1368;
NOT T1371,T1367;
NOT T1370,T1371;
NOT T1372,T1371;
OR T1369,T1370,T1372;
AND T1363,T1364,T1369;
OR T1348,T1349,T1363;
NOT T1379,T1355;
NOT T1378,T1379;
NOT T1377,T1378;
NOT T1376,T1377;
NOT T1380,T1377;
OR T1375,T1376,T1380;
NOT T1383,T1378;
NOT T1382,T1383;
NOT T1384,T1383;
AND T1381,T1382,T1384;
AND T1374,T1375,T1381;
NOT T1389,T1379;
NOT T1388,T1389;
NOT T1387,T1388;
NOT T1390,T1388;
AND T1386,T1387,T1390;
NOT T1393,T1389;
NOT T1392,T1393;
NOT T1394,T1393;
AND T1391,T1392,T1394;
AND T1385,T1386,T1391;
AND T1373,T1374,T1385;
OR T1347,T1348,T1373;
NOT T1403,T1356;
NOT T1402,T1403;
NOT T1401,T1402;
NOT T1400,T1401;
NOT T1399,T1400;
NOT T1404,T1400;
OR T1398,T1399,T1404;
NOT T1407,T1401;
NOT T1406,T1407;
NOT T1408,T1407;
AND T1405,T1406,T1408;
OR T1397,T1398,T1405;
NOT T1413,T1402;
NOT T1412,T1413;
NOT T1411,T1412;
NOT T1414,T1412;
AND T1410,T1411,T1414;
NOT T1417,T1413;
NOT T1416,T1417;
NOT T1418,T1417;
AND T1415,T1416,T1418;
AND T1409,T1410,T1415;
OR T1396,T1397,T1409;
NOT T1425,T1403;
NOT T1424,T1425;
NOT T1423,T1424;
NOT T1422,T1423;
NOT T1426,T1423;
AND T1421,T1422,T1426;
NOT T1429,T1424;
NOT T1428,T1429;
NOT T1430,T1429;
OR T1427,T1428,T1430;
AND T1420,T1421,T1427;
NOT T1435,T1425;
NOT T1434,T1435;
NOT T1433,T1434;
NOT T1436,T1434;
OR T1432,T1433,T1436;
NOT T1439,T1435;
NOT T1438,T1439;
NOT T1440,T1439;
AND T1437,T1438,T1440;
OR T1431,T1432,T1437;
OR T1419,T1420,T1431;
OR T1395,T1396,T1419;
OR T1346,T1347,T1395;
NOT T1451,T1357;
NOT T1450,T1451;
NOT T1449,T1450;
NOT T1448,T1449;
NOT T1447,T1448;
NOT T1446,T1447;
NOT T1452,T1447;
OR T1445,T1446,T1452;
NOT T1455,T1448;
NOT T1454,T1455;
NOT T1456,T1455;
OR T1453,T1454,T1456;
AND T1444,T1445,T1453;
NOT T1461,T1449;
NOT T1460,T1461;
NOT T1459,T1460;
NOT T1462,T1460;
AND T1458,T1459,T1462;
NOT T1465,T1461;
NOT T1464,T1465;
NOT T1466,T1465;
OR T1463,T1464,T1466;
OR T1457,T1458,T1463;
OR T1443,T1444,T1457;
NOT T1473,T1450;
NOT T1472,T1473;
NOT T1471,T1472;
NOT T1470,T1471;
NOT T1474,T1471;
OR T1469,T1470,T1474;
NOT T1477,T1472;
NOT T1476,T1477;
NOT T1478,T1477;
OR T1475,T1476,T1478;
OR T1468,T1469,T1475;
NOT T1483,T1473;
NOT T1482,T1483;
NOT T1481,T1482;
NOT T1484,T1482;
OR T1480,T1481,T1484;
NOT T1487,T1483;
NOT T1486,T1487;
NOT T1488,T1487;
OR T1485,T1486,T1488;
OR T1479,T1480,T1485;
AND T1467,T1468,T1479;
AND T1442,T1443,T1467;
NOT T1497,T1451;
NOT T1496,T1497;
NOT T1495,T1496;
NOT T1494,T1495;
NOT T1493,T1494;
NOT T1498,T1494;
OR T1492,T1493,T1498;
NOT T1501,T1495;
NOT T1500,T1501;
NOT T1502,T1501;
OR T1499,T1500,T1502;
AND T1491,T1492,T1499;
NOT T1507,T1496;
NOT T1506,T1507;
NOT T1505,T1506;
NOT T1508,T1506;
OR T1504,T1505,T1508;
NOT T1511,T1507;
NOT T1510,T1511;
NOT T1512,T1511;
AND T1509,T1510,T1512;
AND T1503,T1504,T1509;
AND T1490,T1491,T1503;
NOT T1519,T1497;
NOT T1518,T1519;
NOT T1517,T1518;
NOT T1516,T1517;
NOT T1520,T1517;
OR T1515,T1516,T1520;
NOT T1523,T1518;
NOT T1522,T1523;
NOT T1524,T1523;
AND T1521,T1522,T1524;
AND T1514,T1515,T1521;
NOT T1529,T1519;
NOT T1528,T1529;
NOT T1527,T1528;
NOT T1530,T1528;
AND T1526,T1527,T1530;
NOT T1533,T1529;
NOT T1532,T1533;
NOT T1534,T1533;
OR T1531,T1532,T1534;
OR T1525,T1526,T1531;
AND T1513,T1514,T1525;
OR T1489,T1490,T1513;
AND T1441,T1442,T1489;
OR T1345,T1346,T1441;
AND T1153,T1154,T1345;
OR T769,T770,T1153;
AND T2,T3,T769;
NOT T1552,R81;
NOT T1551,T1552;
NOT T1550,T1551;
NOT T1549,T1550;
NOT T1548,T1549;
NOT T1547,T1548;
NOT T1546,T1547;
NOT T1545,T1546;
NOT T1544,T1545;
NOT T1553,T1545;
AND T1543,T1544,T1553;
NOT T1556,T1546;
NOT T1555,T1556;
NOT T1557,T1556;
AND T1554,T1555,T1557;
OR T1542,T1543,T1554;
NOT T1562,T1547;
NOT T1561,T1562;
NOT T1560,T1561;
NOT T1563,T1561;
AND T1559,T1560,T1563;
NOT T1566,T1562;
NOT T1565,T1566;
NOT T1567,T1566;
AND T1564,T1565,T1567;
AND T1558,T1559,T1564;
OR T1541,T1542,T1558;
NOT T1574,T1548;
NOT T1573,T1574;
NOT T1572,T1573;
NOT T1571,T1572;
NOT T1575,T1572;
AND T1570,T1571,T1575;
NOT T1578,T1573;
NOT T1577,T1578;
NOT T1579,T1578;
OR T1576,T1577,T1579;
AND T1569,T1570,T1576;
NOT T1584,T1574;
NOT T1583,T1584;
NOT T1582,T1583;
NOT T1585,T1583;
OR T1581,T1582,T1585;
NOT T1588,T1584;
NOT T1587,T1588;
NOT T1589,T1588;
AND T1586,T1587,T1589;
OR T1580,T1581,T1586;
AND T1568,T1569,T1580;
OR T1540,T1541,T1568;
NOT T1598,T1549;
NOT T1597,T1598;
NOT T1596,T1597;
NOT T1595,T1596;
NOT T1594,T1595;
NOT T1599,T1595;
AND T1593,T1594,T1599;
NOT T1602,T1596;
NOT T1601,T1602;
NOT T1603,T1602;
AND T1600,T1601,T1603;
AND T1592,T1593,T1600;
NOT T1608,T1597;
NOT T1607,T1608;
NOT T1606,T1607;
NOT T1609,T1607;
OR T1605,T1606,T1609;
NOT T1612,T1608;
NOT T1611,T1612;
NOT T1613,T1612;
OR T1610,T1611,T1613;
OR T1604,T1605,T1610;
OR T1591,T1592,T1604;
NOT T1620,T1598;
NOT T1619,T1620;
NOT T1618,T1619;
NOT T1617,T1618;
NOT T1621,T1618;
OR T1616,T1617,T1621;
NOT T1624,T1619;
NOT T1623,T1624;
NOT T1625,T1624;
OR T1622,T1623,T1625;
OR T1615,T1616,T1622;
NOT T1630,T1620;
NOT T1629,T1630;
NOT T1628,T1629;
NOT T1631,T1629;
OR T1627,T1628,T1631;
NOT T1634,T1630;
NOT T1633,T1634;
NOT T1635,T1634;
AND T1632,T1633,T1635;
OR T1626,T1627,T1632;
AND T1614,T1615,T1626;
OR T1590,T1591,T1614;
OR T1539,T1540,T1590;
NOT T1646,T1550;
NOT T1645,T1646;
NOT T1644,T1645;
NOT T1643,T1644;
NOT T1642,T1643;
NOT T1641,T1642;
NOT T1647,T1642;
OR T1640,T1641,T1647;
NOT T1650,T1643;
NOT T1649,T1650;
NOT T1651,T1650;
AND T1648,T1649,T1651;
AND T1639,T1640,T1648;
NOT T1656,T1644;
NOT T1655,T1656;
NOT T1654,T1655;
NOT T1657,T1655;
OR T1653,T1654,T1657;
NOT T1660,T1656;
NOT T1659,T1660;
NOT T1661,T1660;
OR T1658,T1659,T1661;
AND T1652,T1653,T1658;
OR T1638,T1639,T1652;
NOT T1668,T1645;
NOT T1667,T1668;
NOT T1666,T1667;
NOT T1665,T1666;
NOT T1669,T1666;
AND T1664,T1665,T1669;
NOT T1672,T1667;
NOT T1671,T1672;
NOT T1673,T1672;
OR T1670,T1671,T1673;
AND T1663,T1664,T1670;
NOT T1678,T1668;
NOT T1677,T1678;
NOT T1676,T1677;
NOT T1679,T1677;
OR T1675,T1676,T1679;
NOT T1682,T1678;
NOT T1681,T1682;
NOT T1683,T1682;
AND T1680,T1681,T1683;
OR T1674,T1675,T1680;
AND T1662,T1663,T1674;
AND T1637,T1638,T1662;
NOT T1692,T1646;
NOT T1691,T1692;
NOT T1690,T1691;
NOT T1689,T1690;
NOT T1688,T1689;
NOT T1693,T1689;
AND T1687,T1688,T1693;
NOT T1696,T1690;
NOT T1695,T1696;
NOT T1697,T1696;
OR T1694,T1695,T1697;
OR T1686,T1687,T1694;
NOT T1702,T1691;
NOT T1701,T1702;
NOT T1700,T1701;
NOT T1703,T1701;
OR T1699,T1700,T1703;
NOT T1706,T1702;
NOT T1705,T1706;
NOT T1707,T1706;
AND T1704,T1705,T1707;
AND T1698,T1699,T1704;
AND T1685,T1686,T1698;
NOT T1714,T1692;
NOT T1713,T1714;
NOT T1712,T1713;
NOT T1711,T1712;
NOT T1715,T1712;
AND T1710,T1711,T1715;
NOT T1718,T1713;
NOT T1717,T1718;
NOT T1719,T1718;
AND T1716,T1717,T1719;
OR T1709,T1710,T1716;
NOT T1724,T1714;
NOT T1723,T1724;
NOT T1722,T1723;
NOT T1725,T1723;
AND T1721,T1722,T1725;
NOT T1728,T1724;
NOT T1727,T1728;
NOT T1729,T1728;
OR T1726,T1727,T1729;
AND T1720,T1721,T1726;
AND T1708,T1709,T1720;
OR T1684,T1685,T1708;
AND T1636,T1637,T1684;
OR T1538,T1539,T1636;
NOT T1742,T1551;
NOT T1741,T1742;
NOT T1740,T1741;
NOT T1739,T1740;
NOT T1738,T1739;
NOT T1737,T1738;
NOT T1736,T1737;
NOT T1743,T1737;
AND T1735,T1736,T1743;
NOT T1746,T1738;
NOT T1745,T1746;
NOT T1747,T1746;
OR T1744,T1745,T1747;
OR T1734,T1735,T1744;
NOT T1752,T1739;
NOT T1751,T1752;
NOT T1750,T1751;
NOT T1753,T1751;
AND T1749,T1750,T1753;
NOT T1756,T1752;
NOT T1755,T1756;
NOT T1757,T1756;
AND T1754,T1755,T1757;
AND T1748,T1749,T1754;
OR T1733,T1734,T1748;
NOT T1764,T1740;
NOT T1763,T1764;
NOT T1762,T1763;
NOT T1761,T1762;
NOT T1765,T1762;
OR T1760,T1761,T1765;
NOT T1768,T1763;
NOT T1767,T1768;
NOT T1769,T1768;
OR T1766,T1767,T1769;
AND T1759,T1760,T1766;
NOT T1774,T1764;
NOT T1773,T1774;
NOT T1772,T1773;
NOT T1775,T1773;
OR T1771,T1772,T1775;
NOT T1778,T1774;
NOT T1777,T1778;
NOT T1779,T1778;
OR T1776,T1777,T1779;
AND T1770,T1771,T1776;
AND T1758,T1759,T1770;
AND T1732,T1733,T1758;
NOT T1788,T1741;
NOT T1787,T1788;
NOT T1786,T1787;
NOT T1785,T1786;
NOT T1784,T1785;
NOT T1789,T1785;
OR T1783,T1784,T1789;
NOT T1792,T1786;
NOT T1791,T1792;
NOT T1793,T1792;
OR T1790,T1791,T1793;
AND T1782,T1783,T1790;
NOT T1798,T1787;
NOT T1797,T1798;
NOT T1796,T1797;
NOT T1799,T1797;
AND T1795,T1796,T1799;
NOT T1802,T1798;
NOT T1801,T1802;
NOT T1803,T1802;
OR T1800,T1801,T1803;
OR T1794,T1795,T1800;
AND T1781,T1782,T1794;
NOT T1810,T1788;
NOT T1809,T1810;
NOT T1808,T1809;
NOT T1807,T1808;
NOT T1811,T1808;
OR T1806,T1807,T1811;
NOT T1814,T1809;
NOT T1813,T1814;
NOT T1815,T1814;
AND T1812,T1813,T1815;
OR T1805,T1806,T1812;
NOT T1820,T1810;
NOT T1819,T1820;
NOT T1818,T1819;
NOT T1821,T1819;
OR T1817,T1818,T1821;
NOT T1824,T1820;
NOT T1823,T1824;
NOT T1825,T1824;
AND T1822,T1823,T1825;
OR T1816,T1817,T1822;
OR T1804,T1805,T1816;
OR T1780,T1781,T1804;
AND T1731,T1732,T1780;
NOT T1836,T1742;
NOT T1835,T1836;
NOT T1834,T1835;
NOT T1833,T1834;
NOT T1832,T1833;
NOT T1831,T1832;
NOT T1837,T1832;
AND T1830,T1831,T1837;
NOT T1840,T1833;
NOT T1839,T1840;
NOT T1841,T1840;
AND T1838,T1839,T1841;
AND T1829,T1830,T1838;
NOT T1846,T1834;
NOT T1845,T1846;
NOT T1844,T1845;
NOT T1847,T1845;
AND T1843,T1844,T1847;
NOT T1850,T1846;
NOT T1849,T1850;
NOT T1851,T1850;
AND T1848,T1849,T1851;
AND T1842,T1843,T1848;
OR T1828,T1829,T1842;
NOT T1858,T1835;
NOT T1857,T1858;
NOT T1856,T1857;
NOT T1855,T1856;
NOT T1859,T1856;
OR T1854,T1855,T1859;
NOT T1862,T1857;
NOT T1861,T1862;
NOT T1863,T1862;
AND T1860,T1861,T1863;
AND T1853,T1854,T1860;
NOT T1868,T1858;
NOT T1867,T1868;
NOT T1866,T1867;
NOT T1869,T1867;
AND T1865,T1866,T1869;
NOT T1872,T1868;
NOT T1871,T1872;
NOT T1873,T1872;
AND T1870,T1871,T1873;
AND T1864,T1865,T1870;
OR T1852,T1853,T1864;
OR T1827,T1828,T1852;
NOT T1882,T1836;
NOT T1881,T1882;
NOT T1880,T1881;
NOT T1879,T1880;
NOT T1878,T1879;
NOT T1883,T1879;
OR T1877,T1878,T1883;
NOT T1886,T1880;
NOT T1885,T1886;
NOT T1887,T1886;
AND T1884,T1885,T1887;
AND T1876,T1877,T1884;
NOT T1892,T1881;
NOT T1891,T1892;
NOT T1890,T1891;
NOT T1893,T1891;
OR T1889,T1890,T1893;
NOT T1896,T1892;
NOT T1895,T1896;
NOT T1897,T1896;
AND T1894,T1895,T1897;
AND T1888,T1889,T1894;
AND T1875,T1876,T1888;
NOT T1904,T1882;
NOT T1903,T1904;
NOT T1902,T1903;
NOT T1901,T1902;
NOT T1905,T1902;
OR T1900,T1901,T1905;
NOT T1908,T1903;
NOT T1907,T1908;
NOT T1909,T1908;
OR T1906,T1907,T1909;
OR T1899,T1900,T1906;
NOT T1914,T1904;
NOT T1913,T1914;
NOT T1912,T1913;
NOT T1915,T1913;
AND T1911,T1912,T1915;
NOT T1918,T1914;
NOT T1917,T1918;
NOT T1919,T1918;
OR T1916,T1917,T1919;
OR T1910,T1911,T1916;
OR T1898,T1899,T1910;
OR T1874,T1875,T1898;
AND T1826,T1827,T1874;
AND T1730,T1731,T1826;
OR T1537,T1538,T1730;
NOT T1934,T1552;
NOT T1933,T1934;
NOT T1932,T1933;
NOT T1931,T1932;
NOT T1930,T1931;
NOT T1929,T1930;
NOT T1928,T1929;
NOT T1927,T1928;
NOT T1935,T1928;
OR T1926,T1927,T1935;
NOT T1938,T1929;
NOT T1937,T1938;
NOT T1939,T1938;
AND T1936,T1937,T1939;
AND T1925,T1926,T1936;
NOT T1944,T1930;
NOT T1943,T1944;
NOT T1942,T1943;
NOT T1945,T1943;
AND T1941,T1942,T1945;
NOT T1948,T1944;
NOT T1947,T1948;
NOT T1949,T1948;
OR T1946,T1947,T1949;
AND T1940,T1941,T1946;
OR T1924,T1925,T1940;
NOT T1956,T1931;
NOT T1955,T1956;
NOT T1954,T1955;
NOT T1953,T1954;
NOT T1957,T1954;
OR T1952,T1953,T1957;
NOT T1960,T1955;
NOT T1959,T1960;
NOT T1961,T1960;
OR T1958,T1959,T1961;
OR T1951,T1952,T1958;
NOT T1966,T1956;
NOT T1965,T1966;
NOT T1964,T1965;
NOT T1967,T1965;
AND T1963,T1964,T1967;
NOT T1970,T1966;
NOT T1969,T1970;
NOT T1971,T1970;
AND T1968,T1969,T1971;
AND T1962,T1963,T1968;
AND T1950,T1951,T1962;
OR T1923,T1924,T1950;
NOT T1980,T1932;
NOT T1979,T1980;
NOT T1978,T1979;
NOT T1977,T1978;
NOT T1976,T1977;
NOT T1981,T1977;
OR T1975,T1976,T1981;
NOT T1984,T1978;
NOT T1983,T1984;
NOT T1985,T1984;
AND T1982,T1983,T1985;
OR T1974,T1975,T1982;
NOT T1990,T1979;
NOT T1989,T1990;
NOT T1988,T1989;
NOT T1991,T1989;
AND T1987,T1988,T1991;
NOT T1994,T1990;
NOT T1993,T1994;
NOT T1995,T1994;
AND T1992,T1993,T1995;
AND T1986,T1987,T1992;
OR T1973,T1974,T1986;
NOT T2002,T1980;
NOT T2001,T2002;
NOT T2000,T2001;
NOT T1999,T2000;
NOT T2003,T2000;
AND T1998,T1999,T2003;
NOT T2006,T2001;
NOT T2005,T2006;
NOT T2007,T2006;
OR T2004,T2005,T2007;
OR T1997,T1998,T2004;
NOT T2012,T2002;
NOT T2011,T2012;
NOT T2010,T2011;
NOT T2013,T2011;
OR T2009,T2010,T2013;
NOT T2016,T2012;
NOT T2015,T2016;
NOT T2017,T2016;
OR T2014,T2015,T2017;
OR T2008,T2009,T2014;
AND T1996,T1997,T2008;
OR T1972,T1973,T1996;
AND T1922,T1923,T1972;
NOT T2028,T1933;
NOT T2027,T2028;
NOT T2026,T2027;
NOT T2025,T2026;
NOT T2024,T2025;
NOT T2023,T2024;
NOT T2029,T2024;
OR T2022,T2023,T2029;
NOT T2032,T2025;
NOT T2031,T2032;
NOT T2033,T2032;
AND T2030,T2031,T2033;
AND T2021,T2022,T2030;
NOT T2038,T2026;
NOT T2037,T2038;
NOT T2036,T2037;
NOT T2039,T2037;
OR T2035,T2036,T2039;
NOT T2042,T2038;
NOT T2041,T2042;
NOT T2043,T2042;
AND T2040,T2041,T2043;
AND T2034,T2035,T2040;
AND T2020,T2021,T2034;
NOT T2050,T2027;
NOT T2049,T2050;
NOT T2048,T2049;
NOT T2047,T2048;
NOT T2051,T2048;
OR T2046,T2047,T2051;
NOT T2054,T2049;
NOT T2053,T2054;
NOT T2055,T2054;
AND T2052,T2053,T2055;
OR T2045,T2046,T2052;
NOT T2060,T2050;
NOT T2059,T2060;
NOT T2058,T2059;
NOT T2061,T2059;
OR T2057,T2058,T2061;
NOT T2064,T2060;
NOT T2063,T2064;
NOT T2065,T2064;
AND T2062,T2063,T2065;
OR T2056,T2057,T2062;
OR T2044,T2045,T2056;
OR T2019,T2020,T2044;
NOT T2074,T2028;
NOT T2073,T2074;
NOT T2072,T2073;
NOT T2071,T2072;
NOT T2070,T2071;
NOT T2075,T2071;
AND T2069,T2070,T2075;
NOT T2078,T2072;
NOT T2077,T2078;
NOT T2079,T2078;
OR T2076,T2077,T2079;
AND T2068,T2069,T2076;
NOT T2084,T2073;
NOT T2083,T2084;
NOT T2082,T2083;
NOT T2085,T2083;
AND T2081,T2082,T2085;
NOT T2088,T2084;
NOT T2087,T2088;
NOT T2089,T2088;
OR T2086,T2087,T2089;
OR T2080,T2081,T2086;
AND T2067,T2068,T2080;
NOT T2096,T2074;
NOT T2095,T2096;
NOT T2094,T2095;
NOT T2093,T2094;
NOT T2097,T2094;
OR T2092,T2093,T2097;
NOT T2100,T2095;
NOT T2099,T2100;
NOT T2101,T2100;
OR T2098,T2099,T2101;
OR T2091,T2092,T2098;
NOT T2106,T2096;
NOT T2105,T2106;
NOT T2104,T2105;
NOT T2107,T2105;
OR T2103,T2104,T2107;
NOT T2110,T2106;
NOT T2109,T2110;
NOT T2111,T2110;
AND T2108,T2109,T2111;
AND T2102,T2103,T2108;
OR T2090,T2091,T2102;
AND T2066,T2067,T2090;
AND T2018,T2019,T2066;
OR T1921,T1922,T2018;
NOT T2124,T1934;
NOT T2123,T2124;
NOT T2122,T2123;
NOT T2121,T2122;
NOT T2120,T2121;
NOT T2119,T2120;
NOT T2118,T2119;
NOT T2125,T2119;
AND T2117,T2118,T2125;
NOT T2128,T2120;
NOT T2127,T2128;
NOT T2129,T2128;
AND T2126,T2127,T2129;
AND T2116,T2117,T2126;
NOT T2134,T2121;
NOT T2133,T2134;
NOT T2132,T2133;
NOT T2135,T2133;
AND T2131,T2132,T2135;
NOT T2138,T2134;
NOT T2137,T2138;
NOT T2139,T2138;
OR T2136,T2137,T2139;
AND T2130,T2131,T2136;
AND T2115,T2116,T2130;
NOT T2146,T2122;
NOT T2145,T2146;
NOT T2144,T2145;
NOT T2143,T2144;
NOT T2147,T2144;
AND T2142,T2143,T2147;
NOT T2150,T2145;
NOT T2149,T2150;
NOT T2151,T2150;
AND T2148,T2149,T2151;
AND T2141,T2142,T2148;
NOT T2156,T2146;
NOT T2155,T2156;
NOT T2154,T2155;
NOT T2157,T2155;
OR T2153,T2154,T2157;
NOT T2160,T2156;
NOT T2159,T2160;
NOT T2161,T2160;
AND T2158,T2159,T2161;
AND T2152,T2153,T2158;
AND T2140,T2141,T2152;
AND T2114,T2115,T2140;
NOT T2170,T2123;
NOT T2169,T2170;
NOT T2168,T2169;
NOT T2167,T2168;
NOT T2166,T2167;
NOT T2171,T2167;
AND T2165,T2166,T2171;
NOT T2174,T2168;
NOT T2173,T2174;
NOT T2175,T2174;
OR T2172,T2173,T2175;
AND T2164,T2165,T2172;
NOT T2180,T2169;
NOT T2179,T2180;
NOT T2178,T2179;
NOT T2181,T2179;
AND T2177,T2178,T2181;
NOT T2184,T2180;
NOT T2183,T2184;
NOT T2185,T2184;
OR T2182,T2183,T2185;
AND T2176,T2177,T2182;
OR T2163,T2164,T2176;
NOT T2192,T2170;
NOT T2191,T2192;
NOT T2190,T2191;
NOT T2189,T2190;
NOT T2193,T2190;
OR T2188,T2189,T2193;
NOT T2196,T2191;
NOT T2195,T2196;
NOT T2197,T2196;
OR T2194,T2195,T2197;
AND T2187,T2188,T2194;
NOT T2202,T2192;
NOT T2201,T2202;
NOT T2200,T2201;
NOT T2203,T2201;
AND T2199,T2200,T2203;
NOT T2206,T2202;
NOT T2205,T2206;
NOT T2207,T2206;
OR T2204,T2205,T2207;
AND T2198,T2199,T2204;
AND T2186,T2187,T2198;
OR T2162,T2163,T2186;
AND T2113,T2114,T2162;
NOT T2218,T2124;
NOT T2217,T2218;
NOT T2216,T2217;
NOT T2215,T2216;
NOT T2214,T2215;
NOT T2213,T2214;
NOT T2219,T2214;
OR T2212,T2213,T2219;
NOT T2222,T2215;
NOT T2221,T2222;
NOT T2223,T2222;
AND T2220,T2221,T2223;
OR T2211,T2212,T2220;
NOT T2228,T2216;
NOT T2227,T2228;
NOT T2226,T2227;
NOT T2229,T2227;
OR T2225,T2226,T2229;
NOT T2232,T2228;
NOT T2231,T2232;
NOT T2233,T2232;
OR T2230,T2231,T2233;
AND T2224,T2225,T2230;
OR T2210,T2211,T2224;
NOT T2240,T2217;
NOT T2239,T2240;
NOT T2238,T2239;
NOT T2237,T2238;
NOT T2241,T2238;
AND T2236,T2237,T2241;
NOT T2244,T2239;
NOT T2243,T2244;
NOT T2245,T2244;
AND T2242,T2243,T2245;
OR T2235,T2236,T2242;
NOT T2250,T2240;
NOT T2249,T2250;
NOT T2248,T2249;
NOT T2251,T2249;
AND T2247,T2248,T2251;
NOT T2254,T2250;
NOT T2253,T2254;
NOT T2255,T2254;
OR T2252,T2253,T2255;
AND T2246,T2247,T2252;
AND T2234,T2235,T2246;
AND T2209,T2210,T2234;
NOT T2264,T2218;
NOT T2263,T2264;
NOT T2262,T2263;
NOT T2261,T2262;
NOT T2260,T2261;
NOT T2265,T2261;
AND T2259,T2260,T2265;
NOT T2268,T2262;
NOT T2267,T2268;
NOT T2269,T2268;
AND T2266,T2267,T2269;
AND T2258,T2259,T2266;
NOT T2274,T2263;
NOT T2273,T2274;
NOT T2272,T2273;
NOT T2275,T2273;
OR T2271,T2272,T2275;
NOT T2278,T2274;
NOT T2277,T2278;
NOT T2279,T2278;
AND T2276,T2277,T2279;
AND T2270,T2271,T2276;
AND T2257,T2258,T2270;
NOT T2286,T2264;
NOT T2285,T2286;
NOT T2284,T2285;
NOT T2283,T2284;
NOT T2287,T2284;
OR T2282,T2283,T2287;
NOT T2290,T2285;
NOT T2289,T2290;
NOT T2291,T2290;
AND T2288,T2289,T2291;
AND T2281,T2282,T2288;
NOT T2296,T2286;
NOT T2295,T2296;
NOT T2294,T2295;
NOT T2297,T2295;
AND T2293,T2294,T2297;
NOT T2300,T2296;
NOT T2299,T2300;
NOT T2301,T2300;
OR T2298,T2299,T2301;
AND T2292,T2293,T2298;
AND T2280,T2281,T2292;
OR T2256,T2257,T2280;
AND T2208,T2209,T2256;
OR T2112,T2113,T2208;
OR T1920,T1921,T2112;
OR T1536,T1537,T1920;
NOT T2318,R81;
NOT T2317,T2318;
NOT T2316,T2317;
NOT T2315,T2316;
NOT T2314,T2315;
NOT T2313,T2314;
NOT T2312,T2313;
NOT T2311,T2312;
NOT T2310,T2311;
NOT T2319,T2311;
AND T2309,T2310,T2319;
NOT T2322,T2312;
NOT T2321,T2322;
NOT T2323,T2322;
OR T2320,T2321,T2323;
AND T2308,T2309,T2320;
NOT T2328,T2313;
NOT T2327,T2328;
NOT T2326,T2327;
NOT T2329,T2327;
OR T2325,T2326,T2329;
NOT T2332,T2328;
NOT T2331,T2332;
NOT T2333,T2332;
AND T2330,T2331,T2333;
AND T2324,T2325,T2330;
OR T2307,T2308,T2324;
NOT T2340,T2314;
NOT T2339,T2340;
NOT T2338,T2339;
NOT T2337,T2338;
NOT T2341,T2338;
AND T2336,T2337,T2341;
NOT T2344,T2339;
NOT T2343,T2344;
NOT T2345,T2344;
OR T2342,T2343,T2345;
AND T2335,T2336,T2342;
NOT T2350,T2340;
NOT T2349,T2350;
NOT T2348,T2349;
NOT T2351,T2349;
AND T2347,T2348,T2351;
NOT T2354,T2350;
NOT T2353,T2354;
NOT T2355,T2354;
OR T2352,T2353,T2355;
OR T2346,T2347,T2352;
OR T2334,T2335,T2346;
OR T2306,T2307,T2334;
NOT T2364,T2315;
NOT T2363,T2364;
NOT T2362,T2363;
NOT T2361,T2362;
NOT T2360,T2361;
NOT T2365,T2361;
AND T2359,T2360,T2365;
NOT T2368,T2362;
NOT T2367,T2368;
NOT T2369,T2368;
AND T2366,T2367,T2369;
OR T2358,T2359,T2366;
NOT T2374,T2363;
NOT T2373,T2374;
NOT T2372,T2373;
NOT T2375,T2373;
OR T2371,T2372,T2375;
NOT T2378,T2374;
NOT T2377,T2378;
NOT T2379,T2378;
AND T2376,T2377,T2379;
OR T2370,T2371,T2376;
OR T2357,T2358,T2370;
NOT T2386,T2364;
NOT T2385,T2386;
NOT T2384,T2385;
NOT T2383,T2384;
NOT T2387,T2384;
OR T2382,T2383,T2387;
NOT T2390,T2385;
NOT T2389,T2390;
NOT T2391,T2390;
AND T2388,T2389,T2391;
OR T2381,T2382,T2388;
NOT T2396,T2386;
NOT T2395,T2396;
NOT T2394,T2395;
NOT T2397,T2395;
AND T2393,T2394,T2397;
NOT T2400,T2396;
NOT T2399,T2400;
NOT T2401,T2400;
OR T2398,T2399,T2401;
OR T2392,T2393,T2398;
AND T2380,T2381,T2392;
AND T2356,T2357,T2380;
OR T2305,T2306,T2356;
NOT T2412,T2316;
NOT T2411,T2412;
NOT T2410,T2411;
NOT T2409,T2410;
NOT T2408,T2409;
NOT T2407,T2408;
NOT T2413,T2408;
OR T2406,T2407,T2413;
NOT T2416,T2409;
NOT T2415,T2416;
NOT T2417,T2416;
OR T2414,T2415,T2417;
AND T2405,T2406,T2414;
NOT T2422,T2410;
NOT T2421,T2422;
NOT T2420,T2421;
NOT T2423,T2421;
AND T2419,T2420,T2423;
NOT T2426,T2422;
NOT T2425,T2426;
NOT T2427,T2426;
OR T2424,T2425,T2427;
AND T2418,T2419,T2424;
AND T2404,T2405,T2418;
NOT T2434,T2411;
NOT T2433,T2434;
NOT T2432,T2433;
NOT T2431,T2432;
NOT T2435,T2432;
AND T2430,T2431,T2435;
NOT T2438,T2433;
NOT T2437,T2438;
NOT T2439,T2438;
OR T2436,T2437,T2439;
OR T2429,T2430,T2436;
NOT T2444,T2434;
NOT T2443,T2444;
NOT T2442,T2443;
NOT T2445,T2443;
OR T2441,T2442,T2445;
NOT T2448,T2444;
NOT T2447,T2448;
NOT T2449,T2448;
AND T2446,T2447,T2449;
AND T2440,T2441,T2446;
AND T2428,T2429,T2440;
AND T2403,T2404,T2428;
NOT T2458,T2412;
NOT T2457,T2458;
NOT T2456,T2457;
NOT T2455,T2456;
NOT T2454,T2455;
NOT T2459,T2455;
OR T2453,T2454,T2459;
NOT T2462,T2456;
NOT T2461,T2462;
NOT T2463,T2462;
AND T2460,T2461,T2463;
AND T2452,T2453,T2460;
NOT T2468,T2457;
NOT T2467,T2468;
NOT T2466,T2467;
NOT T2469,T2467;
AND T2465,T2466,T2469;
NOT T2472,T2468;
NOT T2471,T2472;
NOT T2473,T2472;
AND T2470,T2471,T2473;
AND T2464,T2465,T2470;
AND T2451,T2452,T2464;
NOT T2480,T2458;
NOT T2479,T2480;
NOT T2478,T2479;
NOT T2477,T2478;
NOT T2481,T2478;
OR T2476,T2477,T2481;
NOT T2484,T2479;
NOT T2483,T2484;
NOT T2485,T2484;
AND T2482,T2483,T2485;
AND T2475,T2476,T2482;
NOT T2490,T2480;
NOT T2489,T2490;
NOT T2488,T2489;
NOT T2491,T2489;
OR T2487,T2488,T2491;
NOT T2494,T2490;
NOT T2493,T2494;
NOT T2495,T2494;
OR T2492,T2493,T2495;
OR T2486,T2487,T2492;
AND T2474,T2475,T2486;
OR T2450,T2451,T2474;
OR T2402,T2403,T2450;
AND T2304,T2305,T2402;
NOT T2508,T2317;
NOT T2507,T2508;
NOT T2506,T2507;
NOT T2505,T2506;
NOT T2504,T2505;
NOT T2503,T2504;
NOT T2502,T2503;
NOT T2509,T2503;
AND T2501,T2502,T2509;
NOT T2512,T2504;
NOT T2511,T2512;
NOT T2513,T2512;
AND T2510,T2511,T2513;
OR T2500,T2501,T2510;
NOT T2518,T2505;
NOT T2517,T2518;
NOT T2516,T2517;
NOT T2519,T2517;
AND T2515,T2516,T2519;
NOT T2522,T2518;
NOT T2521,T2522;
NOT T2523,T2522;
AND T2520,T2521,T2523;
OR T2514,T2515,T2520;
OR T2499,T2500,T2514;
NOT T2530,T2506;
NOT T2529,T2530;
NOT T2528,T2529;
NOT T2527,T2528;
NOT T2531,T2528;
AND T2526,T2527,T2531;
NOT T2534,T2529;
NOT T2533,T2534;
NOT T2535,T2534;
OR T2532,T2533,T2535;
OR T2525,T2526,T2532;
NOT T2540,T2530;
NOT T2539,T2540;
NOT T2538,T2539;
NOT T2541,T2539;
AND T2537,T2538,T2541;
NOT T2544,T2540;
NOT T2543,T2544;
NOT T2545,T2544;
AND T2542,T2543,T2545;
AND T2536,T2537,T2542;
AND T2524,T2525,T2536;
OR T2498,T2499,T2524;
NOT T2554,T2507;
NOT T2553,T2554;
NOT T2552,T2553;
NOT T2551,T2552;
NOT T2550,T2551;
NOT T2555,T2551;
OR T2549,T2550,T2555;
NOT T2558,T2552;
NOT T2557,T2558;
NOT T2559,T2558;
OR T2556,T2557,T2559;
AND T2548,T2549,T2556;
NOT T2564,T2553;
NOT T2563,T2564;
NOT T2562,T2563;
NOT T2565,T2563;
OR T2561,T2562,T2565;
NOT T2568,T2564;
NOT T2567,T2568;
NOT T2569,T2568;
OR T2566,T2567,T2569;
OR T2560,T2561,T2566;
OR T2547,T2548,T2560;
NOT T2576,T2554;
NOT T2575,T2576;
NOT T2574,T2575;
NOT T2573,T2574;
NOT T2577,T2574;
OR T2572,T2573,T2577;
NOT T2580,T2575;
NOT T2579,T2580;
NOT T2581,T2580;
OR T2578,T2579,T2581;
OR T2571,T2572,T2578;
NOT T2586,T2576;
NOT T2585,T2586;
NOT T2584,T2585;
NOT T2587,T2585;
AND T2583,T2584,T2587;
NOT T2590,T2586;
NOT T2589,T2590;
NOT T2591,T2590;
AND T2588,T2589,T2591;
AND T2582,T2583,T2588;
AND T2570,T2571,T2582;
OR T2546,T2547,T2570;
AND T2497,T2498,T2546;
NOT T2602,T2508;
NOT T2601,T2602;
NOT T2600,T2601;
NOT T2599,T2600;
NOT T2598,T2599;
NOT T2597,T2598;
NOT T2603,T2598;
OR T2596,T2597,T2603;
NOT T2606,T2599;
NOT T2605,T2606;
NOT T2607,T2606;
AND T2604,T2605,T2607;
OR T2595,T2596,T2604;
NOT T2612,T2600;
NOT T2611,T2612;
NOT T2610,T2611;
NOT T2613,T2611;
AND T2609,T2610,T2613;
NOT T2616,T2612;
NOT T2615,T2616;
NOT T2617,T2616;
AND T2614,T2615,T2617;
OR T2608,T2609,T2614;
OR T2594,T2595,T2608;
NOT T2624,T2601;
NOT T2623,T2624;
NOT T2622,T2623;
NOT T2621,T2622;
NOT T2625,T2622;
OR T2620,T2621,T2625;
NOT T2628,T2623;
NOT T2627,T2628;
NOT T2629,T2628;
AND T2626,T2627,T2629;
AND T2619,T2620,T2626;
NOT T2634,T2624;
NOT T2633,T2634;
NOT T2632,T2633;
NOT T2635,T2633;
OR T2631,T2632,T2635;
NOT T2638,T2634;
NOT T2637,T2638;
NOT T2639,T2638;
AND T2636,T2637,T2639;
AND T2630,T2631,T2636;
OR T2618,T2619,T2630;
OR T2593,T2594,T2618;
NOT T2648,T2602;
NOT T2647,T2648;
NOT T2646,T2647;
NOT T2645,T2646;
NOT T2644,T2645;
NOT T2649,T2645;
AND T2643,T2644,T2649;
NOT T2652,T2646;
NOT T2651,T2652;
NOT T2653,T2652;
OR T2650,T2651,T2653;
AND T2642,T2643,T2650;
NOT T2658,T2647;
NOT T2657,T2658;
NOT T2656,T2657;
NOT T2659,T2657;
OR T2655,T2656,T2659;
NOT T2662,T2658;
NOT T2661,T2662;
NOT T2663,T2662;
OR T2660,T2661,T2663;
AND T2654,T2655,T2660;
AND T2641,T2642,T2654;
NOT T2670,T2648;
NOT T2669,T2670;
NOT T2668,T2669;
NOT T2667,T2668;
NOT T2671,T2668;
OR T2666,T2667,T2671;
NOT T2674,T2669;
NOT T2673,T2674;
NOT T2675,T2674;
OR T2672,T2673,T2675;
OR T2665,T2666,T2672;
NOT T2680,T2670;
NOT T2679,T2680;
NOT T2678,T2679;
NOT T2681,T2679;
AND T2677,T2678,T2681;
NOT T2684,T2680;
NOT T2683,T2684;
NOT T2685,T2684;
OR T2682,T2683,T2685;
OR T2676,T2677,T2682;
AND T2664,T2665,T2676;
OR T2640,T2641,T2664;
AND T2592,T2593,T2640;
OR T2496,T2497,T2592;
AND T2303,T2304,T2496;
NOT T2700,T2318;
NOT T2699,T2700;
NOT T2698,T2699;
NOT T2697,T2698;
NOT T2696,T2697;
NOT T2695,T2696;
NOT T2694,T2695;
NOT T2693,T2694;
NOT T2701,T2694;
AND T2692,T2693,T2701;
NOT T2704,T2695;
NOT T2703,T2704;
NOT T2705,T2704;
OR T2702,T2703,T2705;
AND T2691,T2692,T2702;
NOT T2710,T2696;
NOT T2709,T2710;
NOT T2708,T2709;
NOT T2711,T2709;
AND T2707,T2708,T2711;
NOT T2714,T2710;
NOT T2713,T2714;
NOT T2715,T2714;
OR T2712,T2713,T2715;
AND T2706,T2707,T2712;
AND T2690,T2691,T2706;
NOT T2722,T2697;
NOT T2721,T2722;
NOT T2720,T2721;
NOT T2719,T2720;
NOT T2723,T2720;
AND T2718,T2719,T2723;
NOT T2726,T2721;
NOT T2725,T2726;
NOT T2727,T2726;
AND T2724,T2725,T2727;
AND T2717,T2718,T2724;
NOT T2732,T2722;
NOT T2731,T2732;
NOT T2730,T2731;
NOT T2733,T2731;
OR T2729,T2730,T2733;
NOT T2736,T2732;
NOT T2735,T2736;
NOT T2737,T2736;
AND T2734,T2735,T2737;
OR T2728,T2729,T2734;
AND T2716,T2717,T2728;
OR T2689,T2690,T2716;
NOT T2746,T2698;
NOT T2745,T2746;
NOT T2744,T2745;
NOT T2743,T2744;
NOT T2742,T2743;
NOT T2747,T2743;
AND T2741,T2742,T2747;
NOT T2750,T2744;
NOT T2749,T2750;
NOT T2751,T2750;
OR T2748,T2749,T2751;
OR T2740,T2741,T2748;
NOT T2756,T2745;
NOT T2755,T2756;
NOT T2754,T2755;
NOT T2757,T2755;
OR T2753,T2754,T2757;
NOT T2760,T2756;
NOT T2759,T2760;
NOT T2761,T2760;
OR T2758,T2759,T2761;
OR T2752,T2753,T2758;
OR T2739,T2740,T2752;
NOT T2768,T2746;
NOT T2767,T2768;
NOT T2766,T2767;
NOT T2765,T2766;
NOT T2769,T2766;
OR T2764,T2765,T2769;
NOT T2772,T2767;
NOT T2771,T2772;
NOT T2773,T2772;
OR T2770,T2771,T2773;
OR T2763,T2764,T2770;
NOT T2778,T2768;
NOT T2777,T2778;
NOT T2776,T2777;
NOT T2779,T2777;
AND T2775,T2776,T2779;
NOT T2782,T2778;
NOT T2781,T2782;
NOT T2783,T2782;
OR T2780,T2781,T2783;
AND T2774,T2775,T2780;
OR T2762,T2763,T2774;
OR T2738,T2739,T2762;
OR T2688,T2689,T2738;
NOT T2794,T2699;
NOT T2793,T2794;
NOT T2792,T2793;
NOT T2791,T2792;
NOT T2790,T2791;
NOT T2789,T2790;
NOT T2795,T2790;
AND T2788,T2789,T2795;
NOT T2798,T2791;
NOT T2797,T2798;
NOT T2799,T2798;
OR T2796,T2797,T2799;
OR T2787,T2788,T2796;
NOT T2804,T2792;
NOT T2803,T2804;
NOT T2802,T2803;
NOT T2805,T2803;
AND T2801,T2802,T2805;
NOT T2808,T2804;
NOT T2807,T2808;
NOT T2809,T2808;
AND T2806,T2807,T2809;
AND T2800,T2801,T2806;
OR T2786,T2787,T2800;
NOT T2816,T2793;
NOT T2815,T2816;
NOT T2814,T2815;
NOT T2813,T2814;
NOT T2817,T2814;
AND T2812,T2813,T2817;
NOT T2820,T2815;
NOT T2819,T2820;
NOT T2821,T2820;
AND T2818,T2819,T2821;
AND T2811,T2812,T2818;
NOT T2826,T2816;
NOT T2825,T2826;
NOT T2824,T2825;
NOT T2827,T2825;
OR T2823,T2824,T2827;
NOT T2830,T2826;
NOT T2829,T2830;
NOT T2831,T2830;
OR T2828,T2829,T2831;
OR T2822,T2823,T2828;
OR T2810,T2811,T2822;
OR T2785,T2786,T2810;
NOT T2840,T2794;
NOT T2839,T2840;
NOT T2838,T2839;
NOT T2837,T2838;
NOT T2836,T2837;
NOT T2841,T2837;
OR T2835,T2836,T2841;
NOT T2844,T2838;
NOT T2843,T2844;
NOT T2845,T2844;
OR T2842,T2843,T2845;
AND T2834,T2835,T2842;
NOT T2850,T2839;
NOT T2849,T2850;
NOT T2848,T2849;
NOT T2851,T2849;
OR T2847,T2848,T2851;
NOT T2854,T2850;
NOT T2853,T2854;
NOT T2855,T2854;
AND T2852,T2853,T2855;
OR T2846,T2847,T2852;
OR T2833,T2834,T2846;
NOT T2862,T2840;
NOT T2861,T2862;
NOT T2860,T2861;
NOT T2859,T2860;
NOT T2863,T2860;
AND T2858,T2859,T2863;
NOT T2866,T2861;
NOT T2865,T2866;
NOT T2867,T2866;
AND T2864,T2865,T2867;
AND T2857,T2858,T2864;
NOT T2872,T2862;
NOT T2871,T2872;
NOT T2870,T2871;
NOT T2873,T2871;
AND T2869,T2870,T2873;
NOT T2876,T2872;
NOT T2875,T2876;
NOT T2877,T2876;
AND T2874,T2875,T2877;
OR T2868,T2869,T2874;
OR T2856,T2857,T2868;
AND T2832,T2833,T2856;
OR T2784,T2785,T2832;
AND T2687,T2688,T2784;
NOT T2890,T2700;
NOT T2889,T2890;
NOT T2888,T2889;
NOT T2887,T2888;
NOT T2886,T2887;
NOT T2885,T2886;
NOT T2884,T2885;
NOT T2891,T2885;
AND T2883,T2884,T2891;
NOT T2894,T2886;
NOT T2893,T2894;
NOT T2895,T2894;
OR T2892,T2893,T2895;
OR T2882,T2883,T2892;
NOT T2900,T2887;
NOT T2899,T2900;
NOT T2898,T2899;
NOT T2901,T2899;
OR T2897,T2898,T2901;
NOT T2904,T2900;
NOT T2903,T2904;
NOT T2905,T2904;
AND T2902,T2903,T2905;
AND T2896,T2897,T2902;
AND T2881,T2882,T2896;
NOT T2912,T2888;
NOT T2911,T2912;
NOT T2910,T2911;
NOT T2909,T2910;
NOT T2913,T2910;
AND T2908,T2909,T2913;
NOT T2916,T2911;
NOT T2915,T2916;
NOT T2917,T2916;
OR T2914,T2915,T2917;
OR T2907,T2908,T2914;
NOT T2922,T2912;
NOT T2921,T2922;
NOT T2920,T2921;
NOT T2923,T2921;
OR T2919,T2920,T2923;
NOT T2926,T2922;
NOT T2925,T2926;
NOT T2927,T2926;
OR T2924,T2925,T2927;
AND T2918,T2919,T2924;
OR T2906,T2907,T2918;
OR T2880,T2881,T2906;
NOT T2936,T2889;
NOT T2935,T2936;
NOT T2934,T2935;
NOT T2933,T2934;
NOT T2932,T2933;
NOT T2937,T2933;
OR T2931,T2932,T2937;
NOT T2940,T2934;
NOT T2939,T2940;
NOT T2941,T2940;
OR T2938,T2939,T2941;
AND T2930,T2931,T2938;
NOT T2946,T2935;
NOT T2945,T2946;
NOT T2944,T2945;
NOT T2947,T2945;
AND T2943,T2944,T2947;
NOT T2950,T2946;
NOT T2949,T2950;
NOT T2951,T2950;
AND T2948,T2949,T2951;
OR T2942,T2943,T2948;
OR T2929,T2930,T2942;
NOT T2958,T2936;
NOT T2957,T2958;
NOT T2956,T2957;
NOT T2955,T2956;
NOT T2959,T2956;
OR T2954,T2955,T2959;
NOT T2962,T2957;
NOT T2961,T2962;
NOT T2963,T2962;
OR T2960,T2961,T2963;
AND T2953,T2954,T2960;
NOT T2968,T2958;
NOT T2967,T2968;
NOT T2966,T2967;
NOT T2969,T2967;
OR T2965,T2966,T2969;
NOT T2972,T2968;
NOT T2971,T2972;
NOT T2973,T2972;
AND T2970,T2971,T2973;
AND T2964,T2965,T2970;
AND T2952,T2953,T2964;
OR T2928,T2929,T2952;
AND T2879,T2880,T2928;
NOT T2984,T2890;
NOT T2983,T2984;
NOT T2982,T2983;
NOT T2981,T2982;
NOT T2980,T2981;
NOT T2979,T2980;
NOT T2985,T2980;
OR T2978,T2979,T2985;
NOT T2988,T2981;
NOT T2987,T2988;
NOT T2989,T2988;
AND T2986,T2987,T2989;
OR T2977,T2978,T2986;
NOT T2994,T2982;
NOT T2993,T2994;
NOT T2992,T2993;
NOT T2995,T2993;
AND T2991,T2992,T2995;
NOT T2998,T2994;
NOT T2997,T2998;
NOT T2999,T2998;
OR T2996,T2997,T2999;
OR T2990,T2991,T2996;
AND T2976,T2977,T2990;
NOT T3006,T2983;
NOT T3005,T3006;
NOT T3004,T3005;
NOT T3003,T3004;
NOT T3007,T3004;
OR T3002,T3003,T3007;
NOT T3010,T3005;
NOT T3009,T3010;
NOT T3011,T3010;
AND T3008,T3009,T3011;
AND T3001,T3002,T3008;
NOT T3016,T3006;
NOT T3015,T3016;
NOT T3014,T3015;
NOT T3017,T3015;
AND T3013,T3014,T3017;
NOT T3020,T3016;
NOT T3019,T3020;
NOT T3021,T3020;
AND T3018,T3019,T3021;
OR T3012,T3013,T3018;
OR T3000,T3001,T3012;
AND T2975,T2976,T3000;
NOT T3030,T2984;
NOT T3029,T3030;
NOT T3028,T3029;
NOT T3027,T3028;
NOT T3026,T3027;
NOT T3031,T3027;
OR T3025,T3026,T3031;
NOT T3034,T3028;
NOT T3033,T3034;
NOT T3035,T3034;
AND T3032,T3033,T3035;
OR T3024,T3025,T3032;
NOT T3040,T3029;
NOT T3039,T3040;
NOT T3038,T3039;
NOT T3041,T3039;
AND T3037,T3038,T3041;
NOT T3044,T3040;
NOT T3043,T3044;
NOT T3045,T3044;
AND T3042,T3043,T3045;
AND T3036,T3037,T3042;
OR T3023,T3024,T3036;
NOT T3052,T3030;
NOT T3051,T3052;
NOT T3050,T3051;
NOT T3049,T3050;
NOT T3053,T3050;
AND T3048,T3049,T3053;
NOT T3056,T3051;
NOT T3055,T3056;
NOT T3057,T3056;
OR T3054,T3055,T3057;
OR T3047,T3048,T3054;
NOT T3062,T3052;
NOT T3061,T3062;
NOT T3060,T3061;
NOT T3063,T3061;
AND T3059,T3060,T3063;
NOT T3066,T3062;
NOT T3065,T3066;
NOT T3067,T3066;
AND T3064,T3065,T3067;
AND T3058,T3059,T3064;
OR T3046,T3047,T3058;
AND T3022,T3023,T3046;
AND T2974,T2975,T3022;
OR T2878,T2879,T2974;
OR T2686,T2687,T2878;
AND T2302,T2303,T2686;
OR T1535,T1536,T2302;
OR T1,T2,T1535;