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