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