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