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