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