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