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