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