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