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