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