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