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