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