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