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