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