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