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