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