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