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