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