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