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