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