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