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