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