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