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