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