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