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