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