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