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