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