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