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