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