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