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