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