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