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