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