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