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