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