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