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