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