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