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