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