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