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