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