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