c This Formular is generated by mcnf c c horn? no c forced? no c mixed sat? no c clause length = 3 c p cnf 100 430 58 -94 50 0 89 -23 -53 0 -62 81 16 0 -84 -60 -40 0 -23 21 63 0 -30 83 -1 0 87 91 21 0 96 -2 90 0 -39 65 -91 0 -38 -73 98 0 7 -96 5 0 6 -61 97 0 34 96 39 0 55 45 84 0 21 -60 -6 0 -41 67 -45 0 79 2 -48 0 -39 97 23 0 -16 -48 -26 0 -81 -30 65 0 -40 55 3 0 -36 8 45 0 -68 50 44 0 -31 -26 -95 0 -15 -66 -95 0 15 -5 -38 0 61 24 -74 0 -52 -74 34 0 42 95 -70 0 -1 65 -22 0 77 -58 -91 0 -81 36 4 0 -39 -94 84 0 -17 -30 -41 0 -42 -66 -56 0 50 -36 56 0 19 -32 67 0 32 -24 -1 0 62 -13 -18 0 94 42 48 0 47 -54 -43 0 -33 12 25 0 7 -65 34 0 96 42 43 0 96 -38 -83 0 -51 33 41 0 87 -68 -45 0 -21 -73 43 0 84 -75 64 0 -68 84 45 0 -38 -78 -63 0 -11 -59 65 0 -33 91 -3 0 -96 -29 57 0 67 -23 -27 0 43 -11 33 0 -3 -100 62 0 -97 -87 -22 0 82 57 95 0 81 -83 72 0 -62 36 56 0 -97 43 -44 0 90 6 84 0 -78 86 1 0 -22 4 -99 0 -38 -73 -29 0 -38 63 12 0 -79 12 27 0 6 -1 18 0 24 -95 -44 0 15 25 -27 0 13 -55 25 0 -14 87 72 0 -82 -10 -21 0 12 -76 -4 0 -49 88 -85 0 5 -60 30 0 74 -9 -91 0 -49 -66 -9 0 29 -65 67 0 -90 46 17 0 -50 -42 -83 0 -84 -44 -87 0 -75 38 -36 0 74 -34 -53 0 -70 55 97 0 -9 -78 76 0 -68 41 -90 0 -25 -91 17 0 49 -48 55 0 52 57 75 0 -82 52 81 0 -4 -11 -79 0 -73 89 -85 0 -10 -97 -5 0 -85 -49 -59 0 78 -45 -43 0 39 -97 -59 0 -4 -51 -38 0 -2 -97 -100 0 51 43 41 0 71 -17 -78 0 -93 90 61 0 4 25 -73 0 36 -19 -69 0 -28 35 5 0 -2 14 60 0 43 -20 1 0 -26 74 -46 0 71 -51 -81 0 1 -15 100 0 49 -85 -57 0 19 7 -3 0 -41 36 -46 0 50 6 -11 0 -95 45 -11 0 -37 98 79 0 -77 25 -50 0 -52 -85 96 0 -58 -21 -36 0 -64 45 -24 0 69 -75 -71 0 90 45 1 0 -99 -75 29 0 -25 -29 -21 0 -40 60 -16 0 36 3 -29 0 -83 -39 -42 0 -27 -77 40 0 -55 -96 41 0 -47 96 62 0 95 -33 45 0 -83 -21 84 0 91 74 90 0 -1 -41 76 0 92 73 -84 0 -45 35 17 0 71 -92 34 0 9 28 -52 0 51 3 -88 0 100 9 -30 0 -37 53 18 0 90 10 36 0 -31 39 -45 0 -75 98 -76 0 -42 24 9 0 -45 62 69 0 7 5 18 0 60 59 86 0 -77 -16 -31 0 -52 -19 79 0 77 -34 -66 0 -54 2 85 0 19 4 72 0 -37 85 29 0 -21 88 25 0 -3 -24 48 0 48 -22 -45 0 45 12 -91 0 -29 52 83 0 -63 38 -7 0 1 39 77 0 90 -54 -68 0 22 31 -72 0 -11 76 -38 0 12 -95 94 0 72 82 -69 0 -94 -19 28 0 -22 -74 -44 0 81 -97 -65 0 -74 2 -92 0 -97 91 -54 0 -39 -33 -100 0 80 15 25 0 -13 89 -7 0 -74 81 98 0 -38 44 8 0 -73 47 -79 0 25 94 -87 0 -60 28 -84 0 -63 79 71 0 -78 -81 -61 0 31 45 16 0 -80 -41 23 0 61 50 -66 0 34 79 -50 0 -22 16 74 0 -52 31 90 0 98 -19 47 0 58 -45 86 0 95 22 80 0 36 49 34 0 54 -83 65 0 -49 -48 21 0 32 25 50 0 -18 -43 -60 0 16 21 -34 0 -84 -48 -26 0 46 -72 70 0 -39 -26 17 0 29 22 33 0 -35 41 -98 0 -48 52 -29 0 48 96 50 0 18 47 52 0 70 -62 36 0 49 -11 -83 0 -27 -23 -39 0 -34 -45 -84 0 -10 79 -40 0 75 -82 35 0 54 -32 -21 0 -24 -5 19 0 51 -93 60 0 -28 86 99 0 -40 21 -94 0 85 84 -9 0 2 43 91 0 -35 -56 43 0 15 -17 4 0 25 -23 70 0 95 -81 84 0 -90 87 -47 0 -30 42 -7 0 -90 -50 -12 0 42 88 17 0 -11 100 -94 0 99 -92 -66 0 96 -1 13 0 -98 -61 10 0 95 -48 22 0 16 -52 28 0 -9 46 71 0 -50 -16 55 0 49 -1 -59 0 96 -8 84 0 17 -13 -45 0 -36 12 -22 0 -39 44 19 0 -39 -80 -22 0 60 -77 90 0 61 95 63 0 -56 58 -40 0 -42 -85 11 0 82 14 21 0 -85 70 -78 0 -24 -72 -49 0 -15 33 -28 0 22 53 59 0 -75 -94 -47 0 -97 -81 26 0 -30 -79 -9 0 -49 79 20 0 50 -55 -82 0 -42 -63 -88 0 -44 55 65 0 6 58 -99 0 1 -84 -43 0 50 9 31 0 25 58 81 0 -97 -89 93 0 -82 -64 79 0 -44 -80 -97 0 -62 -49 -65 0 -11 5 -40 0 29 -14 74 0 42 56 -96 0 33 -80 -53 0 -86 27 -100 0 -33 29 84 0 58 -48 -14 0 -63 10 -44 0 -32 -62 58 0 37 77 -49 0 -16 60 95 0 99 90 61 0 100 83 -38 0 -22 -73 27 0 -3 93 95 0 18 45 82 0 -26 -42 3 0 -15 -54 6 0 -18 -19 -44 0 -1 -69 -56 0 -70 -42 -60 0 -8 -26 -76 0 -9 34 4 0 78 50 69 0 83 -48 12 0 -17 68 50 0 49 -57 60 0 23 60 74 0 76 97 54 0 -88 2 49 0 -9 57 -16 0 -92 80 -22 0 -92 -26 -32 0 70 -28 -49 0 -25 -60 68 0 21 67 -64 0 100 -17 -75 0 94 59 -4 0 77 94 -83 0 -91 41 -14 0 67 -34 -40 0 26 -69 81 0 -80 83 7 0 39 84 23 0 -77 -100 -80 0 63 -26 -27 0 66 -82 -64 0 94 62 36 0 -30 83 27 0 -92 -81 -35 0 -65 33 -18 0 86 1 56 0 2 41 99 0 80 71 27 0 -42 -16 -12 0 -70 52 15 0 61 -29 -50 0 -54 80 -37 0 96 -48 -22 0 45 -86 64 0 -90 -24 60 0 -38 -95 -59 0 -8 -52 -92 0 -55 -64 -17 0 -30 10 73 0 -38 -21 69 0 -7 -35 30 0 20 -96 54 0 -81 -10 84 0 -83 16 -60 0 -100 46 10 0 2 50 42 0 -33 35 -26 0 -6 27 -91 0 -40 -6 93 0 -89 60 -47 0 5 -28 -40 0 77 -91 89 0 -83 -82 -62 0 50 11 90 0 -43 -98 9 0 79 100 63 0 -72 23 -13 0 -96 -7 71 0 41 -30 -53 0 -79 14 -60 0 -22 -80 55 0 6 69 23 0 -6 -25 54 0 -18 -22 63 0 -33 30 47 0 47 39 29 0 2 28 95 0 71 52 49 0 57 45 52 0 -53 48 33 0 -47 -86 87 0 -1 89 -37 0 -19 83 -34 0 96 -64 5 0 -50 35 67 0 30 -80 -92 0 -27 55 -67 0 -46 68 -62 0 39 -30 32 0 64 26 -48 0 36 -37 61 0 -5 80 70 0 49 -88 87 0 78 6 50 0 -23 12 -51 0 51 77 94 0 -27 -8 97 0 28 57 2 0 15 -28 -71 0 46 89 47 0 -67 7 98 0 -4 -18 71 0 16 -24 96 0 38 -76 47 0 3 -45 12 0 53 27 -49 0 -94 8 -77 0 -4 23 -97 0 -18 -77 32 0 -87 88 76 0 -39 89 -62 0 46 -32 -74 0 -95 -100 5 0 -48 -16 21 0 -11 -65 92 0 -21 -1 -16 0 48 -34 -85 0 3 52 -80 0 -51 -90 -94 0 -76 -79 -38 0 95 -85 -1 0 64 16 -22 0 29 -40 -9 0 -97 61 -80 0 43 -9 -89 0 4 58 -88 0 77 -40 -98 0 -53 -17 -5 0 47 60 -36 0 -78 -70 74 0 55 -83 4 0 19 -73 69 0 -92 49 62 0 72 -57 83 0 74 61 -80 0 -94 81 42 0 -26 -42 10 0 40 50 -55 0 25 18 21 0 -18 99 -63 0 -56 39 -71 0 -35 -62 44 0 -96 -42 -4 0 21 5 -88 0 45 -28 54 0 -98 11 13 0 -30 -8 42 0 23 -59 -76 0 -94 76 -67 0 72 -48 -24 0 % 0