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