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