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