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