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