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