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