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