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