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