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