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