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