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