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