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