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