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