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