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