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