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