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