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