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