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