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