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