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