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